unification hints with recursive calls do work!

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml
index ae186cc6317b2901f998ef55c5c77fb4c5b82782..3b6d163f4bf5e94d73360ca1181996497ed1f59c 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnifHint.ml
+++ b/helm/software/components/ng_refiner/nCicUnifHint.ml
@@ -208,8 +208,8 @@ let look_for_hint hdb metasenv subst context t1 t2 =
   let rc = 
   List.map
    (function 
-    | (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
+    | (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)
     rc
   in
@@ -218,17 +218,19 @@ let look_for_hint hdb metasenv subst context t1 t2 =
   in 
   let rc = List.map (fun (_,x,y,z) -> x,y,z) rc in
 (*
+    prerr_endline "Hints:";
     List.iter 
       (fun (metasenv, (t1, t2), premises) ->
           prerr_endline 
-            (String.concat "\n"
-                (List.map (fun (a,b) ->
-                   NCicPp.ppterm ~metasenv ~subst ~context a ^
-                   " =?= "^NCicPp.ppterm ~metasenv ~subst ~context b)
+          ("\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) ^     
-              "\n--------------------------------------------------"^
-              "\n"^NCicPp.ppterm ~metasenv ~subst ~context t1 ^
-              " = "^NCicPp.ppterm ~metasenv ~subst ~context t2 ^ "\n\n"))
+              "  ==> "^
+              NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context t1 ^
+              " = "^NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context t2))
       rc;
 *)
   rc

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index a0cda6861c512ef8e31e0974a14af5d7768457ad..55ccca12a0c79dc16fc84180af3dab442dc66bb3 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -443,9 +443,9 @@ and unify hdb test_eq_only metasenv subst context t1 t2 =
     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);
+      prerr_endline ("\nProblema:\n" ^
+        NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^
+        NCicPp.ppterm ~metasenv ~subst ~context t2);
 *)
       let candidates = 
         NCicUnifHint.look_for_hint hdb metasenv subst context t1 t2
@@ -454,11 +454,15 @@ and unify hdb test_eq_only metasenv subst context t1 t2 =
         | [] -> None (* raise exc *)
         | (metasenv,(c1,c2),premises)::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);
+            prerr_endline ("\nProvo il candidato:\n" ^ 
+              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 c1 ^  " = " ^
+              NCicPp.ppterm ~metasenv ~subst ~context c2);
 *)
             try 
               let metasenv,subst = 
@@ -474,7 +478,6 @@ and unify hdb test_eq_only metasenv subst context t1 t2 =
               Some (metasenv, subst)
             with
               UnificationFailure _ | Uncertain _ ->
-                prerr_endline (" <candidate fails");
                 cand_iter tl
       in
         cand_iter candidates