X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnifHint.ml;h=b7d2b67d7642c87e5a30bed87eead2d74a7fd85f;hb=6b0a195b180e3526af7b55771b2df7b10acd7c30;hp=dd58fa5c84660d1346caeb6250416e0bf5ae6bae;hpb=4573f1fecaf83f4706f39702555d5319d132477b;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml
index dd58fa5c8..b7d2b67d7 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,32 +182,56 @@ 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
   in 
   let rc = List.map (fun (_,x,y,z) -> x,y,z) rc in
 (*
+    prerr_endline "Hints:";
     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))
+          ("\t" ^ String.concat ";  "
+                (List.map (fun (a,b) -> 
+                   NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context a ^
+                   " =?= "^
+                   NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context b)
+                premises) ^     
+              "  ==> "^
+              NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context t1 ^
+              " = "^NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context t2))
       rc;
 *)
   rc