From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 10 Mar 2009 21:07:46 +0000 (+0000)
Subject: unificatiom hints with premises
X-Git-Tag: make_still_working~4163
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dc1902ae1e458e5120af63d880dbd08255bef238;p=helm.git

unificatiom hints with premises
---

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml
index dd58fa5c8..ae186cc63 100644
--- 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 076ac2f62..49df40bf9 100644
--- 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 79fe81053..a0cda6861 100644
--- 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 _ ->