From 4573f1fecaf83f4706f39702555d5319d132477b Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 10 Mar 2009 17:51:12 +0000
Subject: [PATCH] unification hints almost ready
---
.../software/components/grafite/grafiteAst.ml | 4 +-
.../components/grafite/grafiteAstPp.ml | 4 +-
.../grafite_engine/grafiteEngine.ml | 8 ++--
.../grafite_parser/grafiteDisambiguate.ml | 11 +++---
.../grafite_parser/grafiteParser.ml | 4 +-
.../ng_disambiguation/nCicDisambiguate.ml | 2 +-
.../components/ng_refiner/nCicUnifHint.ml | 37 +++++++++++--------
.../components/ng_refiner/nCicUnifHint.mli | 4 +-
.../components/ng_refiner/nCicUnification.ml | 30 +++++++++++++--
9 files changed, 67 insertions(+), 37 deletions(-)
diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 474294495..d114d9322 100644
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -150,14 +150,14 @@ type ('term,'lazy_term) macro =
(** To be increased each time the command type below changes, used for "safe"
* marshalling *)
-let magic = 15
+let magic = 16
type ('term,'obj) command =
| Index of loc * 'term option (* key *) * UriManager.uri (* value *)
| Coercion of loc * 'term * bool (* add_obj *) *
int (* arity *) * int (* saturations *)
| PreferCoercion of loc * 'term
- | UnificationHint of loc * 'term
+ | UnificationHint of loc * 'term * int (* term, precedence *)
| Default of loc * string * UriManager.uri list
| Drop of loc
| Include of loc * string
diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 1fdc87b41..56ac59c7a 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -317,8 +317,8 @@ let pp_command ~term_pp ~obj_pp = function
pp_coercion ~term_pp t do_composites i j
| PreferCoercion (_,t) ->
"prefer coercion " ^ term_pp t
- | UnificationHint (_,t) ->
- "unification hint " ^ term_pp t
+ | UnificationHint (_,t, n) ->
+ "unification hint " ^ string_of_int n ^ " " ^ term_pp t
| Default (_,what,uris) -> pp_default what uris
| Drop _ -> "drop"
| Include (_,path) -> "include \"" ^ path ^ "\""
diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index c6bebbc39..7f5327b56 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -470,9 +470,9 @@ let coercion_moo_statement_of (uri,arity, saturations,_) =
GrafiteAst.Coercion
(HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations)
-let eval_unification_hint status t =
+let eval_unification_hint status t n =
(* XXX no undo *)
- NCicUnifHint.add_user_provided_hint t;
+ NCicUnifHint.add_user_provided_hint t n;
status,[]
;;
@@ -597,8 +597,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
eval_prefer_coercion status coercion
| GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) ->
eval_coercion status ~add_composites uri arity saturations
- | GrafiteAst.UnificationHint (loc, t) ->
- eval_unification_hint status t
+ | GrafiteAst.UnificationHint (loc, t, n) ->
+ eval_unification_hint status t n
| GrafiteAst.Default (loc, what, uris) as cmd ->
LibraryObjects.set_default what uris;
GrafiteTypes.add_moo_content [cmd] status,[]
diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 32d666a38..23ec1770e 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -579,12 +579,12 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
OCic2NCic.clear ();
let graph =
match cic with
- | Cic.CurrentProof (_,metasenv, _, ty,_,_) ->
+ | Some (Cic.CurrentProof (_,metasenv, _, ty,_,_)) ->
let _, ugraph =
CicTypeChecker.type_of_aux' metasenv [] ty CicUniv.empty_ugraph
in
ugraph
- | Cic.Constant (_,_, ty,_,_) ->
+ | Some (Cic.Constant (_,_, ty,_,_)) ->
let _, ugraph =
CicTypeChecker.type_of_aux' [] [] ty CicUniv.empty_ugraph
in
@@ -685,7 +685,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
prerr_endline ("VECCHIA DISAMBIGUAZIONE ("^
UriManager.string_of_uri uri ^"): " ^ string_of_float time);
*)
-(* try_new cic; *)
+(* try_new (Some cic); *)
let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
@@ -694,6 +694,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
with
| Sys.Break as exn -> raise exn
| exn ->
+(* try_new None; *)
raise exn
;;
@@ -725,12 +726,12 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
disambiguate_term None text prefix_len lexicon_status_ref [] in
let metasenv,t = disambiguate_term metasenv t in
!lexicon_status_ref, metasenv, GrafiteAst.Coercion (loc,t,b,a,s)
- | GrafiteAst.UnificationHint (loc, t) ->
+ | GrafiteAst.UnificationHint (loc, t, n) ->
let lexicon_status_ref = ref lexicon_status in
let disambiguate_term =
disambiguate_term None text prefix_len lexicon_status_ref [] in
let metasenv,t = disambiguate_term metasenv t in
- !lexicon_status_ref, metasenv, GrafiteAst.UnificationHint (loc,t)
+ !lexicon_status_ref, metasenv, GrafiteAst.UnificationHint (loc,t,n)
| GrafiteAst.Default _
| GrafiteAst.Drop _
| GrafiteAst.Include _
diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 44dec6d32..28d61d9e5 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -700,8 +700,8 @@ EXTEND
(loc, t, composites, arity, saturations)
| IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
GrafiteAst.PreferCoercion (loc, t)
- | IDENT "unification"; IDENT "hint"; t = tactic_term ->
- GrafiteAst.UnificationHint (loc, t)
+ | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
+ GrafiteAst.UnificationHint (loc, t, n)
| IDENT "record" ; (params,name,ty,fields) = record_spec ->
GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
| IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index b49af2bbf..50a0c59da 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -304,7 +304,7 @@ let interpretate_term_and_interpretate_term_option
in
let cic_body = aux ~localize loc (cic_name :: context) body in
NCic.LetIn (cic_name, cic_typ, cic_def, cic_body)
- | CicNotationPt.LetRec (_kind, _defs, _body) -> assert false
+ | CicNotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term
| CicNotationPt.Ident _
| CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed
| CicNotationPt.Ident (name, subst) ->
diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml
index 1aaecbe77..dd58fa5c8 100644
--- a/helm/software/components/ng_refiner/nCicUnifHint.ml
+++ b/helm/software/components/ng_refiner/nCicUnifHint.ml
@@ -11,9 +11,9 @@
(* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *)
-module COT : Set.OrderedType with type t = NCic.term =
+module COT : Set.OrderedType with type t = int * NCic.term =
struct
- type t = NCic.term
+ type t = int * NCic.term
let compare = Pervasives.compare
end
@@ -27,7 +27,7 @@ type db = DB.t
let dummy = NCic.Const (NReference.reference_of_string "cic:/dummy_conv.dec");;
let pair t1 t2 = (NCic.Appl [dummy;t1;t2]) ;;
-let index_hint hdb context t1 t2 =
+let index_hint hdb context t1 t2 precedence =
assert (
(match t1 with
| NCic.Meta _ | NCic.Appl (NCic.Meta _ :: _) -> false | _ -> true)
@@ -41,7 +41,7 @@ let index_hint hdb context t1 t2 =
(fun t (n,e) ->
match e with
| NCic.Decl ty -> NCic.Prod (n,ty,t)
- | _ -> assert false)
+ | NCic.Def (b,ty) -> NCic.LetIn (n,ty,b,t))
pair' context in
let src =
List.fold_left
@@ -49,21 +49,22 @@ let index_hint hdb context t1 t2 =
match e with
| NCic.Decl _ ->
NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) t
- | _ -> assert false)
+ | NCic.Def _ ->
+ NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) t)
pair' context in
(*
prerr_endline ("INDEXING: " ^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " |==> " ^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] data);
*)
- DB.index hdb src data
+ DB.index hdb src (precedence, data)
;;
let empty_db = DB.empty ;;
let user_db = ref empty_db ;;
-let add_user_provided_hint t =
+let add_user_provided_hint t precedence =
let u = UriManager.uri_of_string "cic:/foo/bar.con" in
let c, a, b =
let rec aux ctx = function
@@ -73,11 +74,13 @@ let add_user_provided_hint t =
| _ -> assert false)
| NCic.Prod (n,s,t) ->
aux ((n, NCic.Decl s) :: ctx) t
+ | NCic.LetIn (n,ty,t,b) ->
+ aux ((n, NCic.Def (t,ty)) :: ctx) b
| _ -> assert false
in
aux [] (fst (OCic2NCic.convert_term u t))
in
- user_db := index_hint !user_db c a b
+ user_db := index_hint !user_db c a b precedence
;;
let db () =
@@ -138,7 +141,7 @@ let db () =
in
List.fold_left
(fun db -> function
- | (ctx,b1,b2) -> index_hint db ctx b1 b2)
+ | (ctx,b1,b2) -> index_hint db ctx b1 b2 0)
!user_db (List.flatten hints)
;;
@@ -157,23 +160,27 @@ let look_for_hint hdb metasenv subst context t1 t2 =
let candidates1 = DB.retrieve_unifiables hdb (pair t1 t2) in
let candidates2 = DB.retrieve_unifiables hdb (pair t2 t1) in
let candidates1 =
- List.map (fun ty ->
- true,NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0)
+ List.map (fun (prec,ty) ->
+ prec,true,NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0)
(HintSet.elements candidates1)
in
let candidates2 =
- List.map (fun ty ->
- false,NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0)
+ List.map (fun (prec,ty) ->
+ prec,false,NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0)
(HintSet.elements candidates2)
in
let rc =
List.map
(function
- | (true,(NCic.Appl [_; t1; t2],metasenv,_)) -> metasenv, t1, t2
- | (false,(NCic.Appl [_; t1; t2],metasenv,_)) -> metasenv, t2, t1
+ | (prec,true,(NCic.Appl [_; t1; t2],metasenv,_)) -> prec,metasenv, t1, t2
+ | (prec,false,(NCic.Appl [_; t1; t2],metasenv,_)) -> prec,metasenv, t2, t1
| _ -> assert false)
(candidates1 @ candidates2)
in
+ let rc =
+ List.sort (fun (x,_,_,_) (y,_,_,_) -> Pervasives.compare x y) rc
+ in
+ let rc = List.map (fun (_,x,y,z) -> x,y,z) rc in
(*
List.iter
(fun (metasenv, t1, t2) ->
diff --git a/helm/software/components/ng_refiner/nCicUnifHint.mli b/helm/software/components/ng_refiner/nCicUnifHint.mli
index 2e94d9c8d..076ac2f62 100644
--- a/helm/software/components/ng_refiner/nCicUnifHint.mli
+++ b/helm/software/components/ng_refiner/nCicUnifHint.mli
@@ -14,11 +14,11 @@
type db
val index_hint:
- db -> NCic.context -> NCic.term -> NCic.term -> db
+ db -> NCic.context -> NCic.term -> NCic.term -> int -> db
(* gets the old imperative coercion DB *)
val db : unit -> db
-val add_user_provided_hint : Cic.term -> unit
+val add_user_provided_hint : Cic.term -> int -> unit
val empty_db : db
diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 54b8218f5..79fe81053 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -442,18 +442,32 @@ and unify hdb test_eq_only metasenv subst context t1 t2 =
(*D*) in outside(); rc with exn -> outside (); raise exn
in
let try_hints metasenv subst t1 t2 (* exc*) =
+(*
+ prerr_endline ("\n\n\n looking for hints for : " ^
+ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^
+ NCicPp.ppterm ~metasenv ~subst ~context t2);
+*)
let candidates =
NCicUnifHint.look_for_hint hdb metasenv subst context t1 t2
in
let rec cand_iter = function
| [] -> None (* raise exc *)
| (metasenv,c1,c2)::tl ->
+(*
+ prerr_endline ("\n attempt: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^
+ NCicPp.ppterm ~metasenv ~subst ~context c1 ^ " AND " ^
+ NCicPp.ppterm ~metasenv ~subst ~context c2 ^ " ==?== " ^
+ NCicPp.ppterm ~metasenv ~subst ~context t2);
+*)
try
- let metasenv,subst = fo_unif test_eq_only metasenv subst t1 c1 in
- let metasenv,subst = fo_unif test_eq_only metasenv subst c2 t2 in
+ let metasenv,subst = unify hdb test_eq_only metasenv subst context t1 c1 in
+ let metasenv,subst = unify hdb test_eq_only metasenv subst context c2 t2 in
Some (metasenv, subst)
with
- UnificationFailure _ | Uncertain _ -> cand_iter tl
+ UnificationFailure _ | Uncertain _ ->
+ prerr_endline (" <candidate fails");
+ cand_iter tl
in
cand_iter candidates
in
@@ -527,7 +541,15 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
(*D*) in outside(); rc with exn -> outside (); raise exn
in
try fo_unif test_eq_only metasenv subst t1 t2
- with UnificationFailure msg | Uncertain msg as exn ->
+ with
+ | UnificationFailure msg as exn ->
+ (try
+ unif_machines metasenv subst
+ (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
+ with
+ | UnificationFailure _ -> raise (UnificationFailure msg)
+ | Uncertain _ -> raise exn)
+ | Uncertain msg as exn ->
match try_hints metasenv subst t1 t2 with
| Some x -> x
| None ->
--
2.39.2