unificatiom hints with premises

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml
index dd58fa5c84660d1346caeb6250416e0bf5ae6bae..ae186cc6317b2901f998ef55c5c77fb4c5b82782 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnifHint.ml
+++ b/helm/software/components/ng_refiner/nCicUnifHint.ml
@@ -145,6 +145,27 @@ let db () =
     !user_db (List.flatten hints)
 ;;
 
+let saturate ?(delta=0) metasenv subst context ty goal_arity =
+ assert (goal_arity >= 0);
+  let rec aux metasenv = function
+   | NCic.Prod (name,s,t) as ty ->
+       let metasenv1, arg,_ = 
+          NCicMetaSubst.mk_meta ~name:name metasenv context (`WithType s) in
+       let t, metasenv1, args, pno = 
+           aux metasenv1 (NCicSubstitution.subst arg t) 
+       in
+       if pno + 1 = goal_arity then
+         ty, metasenv, [], goal_arity+1
+       else
+         t, metasenv1, arg::args, pno+1
+   | ty ->
+        match NCicReduction.whd ~subst context ty ~delta with
+        | NCic.Prod _ as ty -> aux metasenv ty
+        | _ -> ty, metasenv, [], 0 (* differs from the other impl in this line*)
+  in
+  let res, newmetasenv, arguments, _ = aux metasenv ty in
+  res, newmetasenv, arguments
+;;
 
 let look_for_hint hdb metasenv subst context t1 t2 =
 (*
@@ -161,21 +182,36 @@ let look_for_hint hdb metasenv subst context t1 t2 =
   let candidates2 = DB.retrieve_unifiables hdb (pair t2 t1) in
   let candidates1 = 
     List.map (fun (prec,ty) -> 
-       prec,true,NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0) 
+       prec,true,saturate ~delta:max_int metasenv subst context ty 0) 
     (HintSet.elements candidates1) 
   in
   let candidates2 = 
     List.map (fun (prec,ty) -> 
-       prec,false,NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0) 
+       prec,false,saturate ~delta:max_int metasenv subst context ty 0) 
     (HintSet.elements candidates2) 
   in
+  let rc = 
+    List.map
+      (fun (p,b,(t,m,_)) ->
+         let rec aux () (m,l as acc) = function
+           | NCic.Meta _ as t -> acc, t
+           | NCic.LetIn (name,ty,bo,t) ->
+               let m,i,_=NCicMetaSubst.mk_meta ~name m context (`WithType ty)in
+               let t = NCicSubstitution.subst i t in
+               aux () (m, (i,bo)::l) t
+           | t -> NCicUntrusted.map_term_fold_a (fun _ () -> ()) () aux acc t
+         in
+         let (m,l), t = aux () (m,[]) t in
+         p,b,(t,m,l))
+   (candidates1 @ candidates2)
+  in
   let rc = 
   List.map
    (function 
-    | (prec,true,(NCic.Appl [_; t1; t2],metasenv,_)) -> prec,metasenv, t1, t2
-    | (prec,false,(NCic.Appl [_; t1; t2],metasenv,_)) -> prec,metasenv, t2, t1
+    | (prec,true,(NCic.Appl [_; t1; t2],metasenv,l))-> prec,metasenv, (t1,t2),l
+    | (prec,false,(NCic.Appl [_; t1; t2],metasenv,l))-> prec,metasenv, (t2,t1),l
     | _ -> assert false)
-   (candidates1 @ candidates2)
+    rc
   in
   let rc = 
     List.sort (fun (x,_,_,_) (y,_,_,_) -> Pervasives.compare x y) rc
@@ -183,10 +219,16 @@ let look_for_hint hdb metasenv subst context t1 t2 =
   let rc = List.map (fun (_,x,y,z) -> x,y,z) rc in
 (*
     List.iter 
-      (fun (metasenv, t1, t2) ->
+      (fun (metasenv, (t1, t2), premises) ->
           prerr_endline 
-            ("CAND: "^NCicPp.ppterm ~metasenv ~subst ~context t1 ^
-            " == "^NCicPp.ppterm ~metasenv ~subst ~context t2))
+            (String.concat "\n"
+                (List.map (fun (a,b) ->
+                   NCicPp.ppterm ~metasenv ~subst ~context a ^
+                   " =?= "^NCicPp.ppterm ~metasenv ~subst ~context b)
+                premises) ^     
+              "\n--------------------------------------------------"^
+              "\n"^NCicPp.ppterm ~metasenv ~subst ~context t1 ^
+              " = "^NCicPp.ppterm ~metasenv ~subst ~context t2 ^ "\n\n"))
       rc;
 *)
   rc

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.mli b/helm/software/components/ng_refiner/nCicUnifHint.mli
index 076ac2f628cc175eaf022a3b43820fdd0fbed877..49df40bf9bd203b8f7aef5abecd1a0eb4d9fef10 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnifHint.mli
+++ b/helm/software/components/ng_refiner/nCicUnifHint.mli
@@ -26,4 +26,5 @@ val look_for_hint:
     db ->
     NCic.metasenv -> NCic.substitution -> NCic.context -> 
     NCic.term -> NCic.term -> 
-      (NCic.metasenv * NCic.term * NCic.term) list
+      (NCic.metasenv * 
+        (NCic.term * NCic.term) * (NCic.term * NCic.term) list) list

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 79fe81053e7e0d630efdc9ea947d2c64d0fa4df2..a0cda6861c512ef8e31e0974a14af5d7768457ad 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -452,7 +452,7 @@ and unify hdb test_eq_only metasenv subst context t1 t2 =
       in
       let rec cand_iter = function
         | [] -> None (* raise exc *)
-        | (metasenv,c1,c2)::tl -> 
+        | (metasenv,(c1,c2),premises)::tl -> 
 (*
             prerr_endline ("\n attempt: " ^ 
               NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^
@@ -461,8 +461,16 @@ and unify hdb test_eq_only metasenv subst context t1 t2 =
               NCicPp.ppterm ~metasenv ~subst ~context t2);
 *)
             try 
-              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
+              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 = 
+                List.fold_left 
+                  (fun (metasenv, subst) (x,y) ->
+                     unify hdb test_eq_only metasenv subst context x y)
+                  (metasenv, subst) premises
+              in
               Some (metasenv, subst)
             with
               UnificationFailure _ | Uncertain _ ->