unification hints with recursive calls do work!

[helm.git] / helm / software / components / ng_refiner / nCicUnification.ml

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 54b8218f5912e08f0b805f2718db8489e37e5799..55ccca12a0c79dc16fc84180af3dab442dc66bb3 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -442,18 +442,43 @@ 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 ("\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
       in
       let rec cand_iter = function
         | [] -> None (* raise exc *)
-        | (metasenv,c1,c2)::tl -> 
+        | (metasenv,(c1,c2),premises)::tl -> 
+(*
+            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 = 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 = 
+                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 _ -> cand_iter tl
+              UnificationFailure _ | Uncertain _ ->
+                cand_iter tl
       in
         cand_iter candidates
     in
@@ -527,7 +552,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 ->