unification hints almost ready

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 4742944959cada0c3437005ccb9b676e2d293bdb..d114d9322785ec15cba42c1ce1c010b26bb3c62e 100644 (file)
--- 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 1fdc87b416b367861d3d6af32fb5b06247b7f769..56ac59c7a5d956a456e04139e47af682b80b6858 100644 (file)
--- 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 c6bebbc397e00cf5dfad8a7645e5fbb3078ff670..7f5327b56e81a5f1c1244f4cbfb6eff0f7bf6609 100644 (file)
--- 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 32d666a384eaa69a04310f9f2dfa6ecadaa91593..23ec1770edc387d5ea7f0fd0663264b1114564e5 100644 (file)
--- 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 44dec6d32bf6adfc4aef459977bb26c861fe26cb..28d61d9e577a7ded0b59da5f7a3664736b8bc897 100644 (file)
--- 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 b49af2bbf5999b69f693293c5bb7f7a462345487..50a0c59da2da3973feffe89da6ee7451575e9e98 100644 (file)
--- 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 1aaecbe778ce4c01d250c34ec9a6f317831da1dc..dd58fa5c84660d1346caeb6250416e0bf5ae6bae 100644 (file)
--- 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 2e94d9c8d0d65b0642d8f0a6b127ae6fb20e8a03..076ac2f628cc175eaf022a3b43820fdd0fbed877 100644 (file)
--- 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 54b8218f5912e08f0b805f2718db8489e37e5799..79fe81053e7e0d630efdc9ea947d2c64d0fa4df2 100644 (file)
--- 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 ->