unification hints almost ready

[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 838fad9dedfb4288d2d4dac99326da6f693bd1d5..79fe81053e7e0d630efdc9ea947d2c64d0fa4df2 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -29,10 +29,11 @@ let fail_exc metasenv subst context t1 t2 =
   " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2));
 ;;
 
-let mk_appl hd tl =
-  match hd with
-  | NCic.Appl l -> NCic.Appl (l@tl)
-  | _ -> NCic.Appl (hd :: tl)
+let mk_appl ~upto hd tl =
+  NCicReduction.head_beta_reduce ~upto
+    (match hd with
+    | NCic.Appl l -> NCic.Appl (l@tl)
+    | _ -> NCic.Appl (hd :: tl))
 ;;
 
 let flexible l = 
@@ -72,11 +73,9 @@ let indent = ref "";;
 let inside c = indent := !indent ^ String.make 1 c;;
 let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
 
-(*
 let pp s = 
   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
 ;;  
-*)
 
 let pp _ = ();;
 
@@ -319,7 +318,8 @@ and unify hdb test_eq_only metasenv subst context t1 t2 =
              let term = NCicSubstitution.subst_meta lc term in
                unify hdb test_eq_only metasenv subst context term t
            with NCicUtils.Subst_not_found _-> 
-             instantiate hdb test_eq_only metasenv subst context n lc t false)
+             instantiate hdb test_eq_only metasenv subst context n lc 
+               (NCicReduction.head_beta_reduce ~subst t) false)
 
        | t, C.Meta (n,lc) -> 
            (try 
@@ -327,17 +327,20 @@ and unify hdb test_eq_only metasenv subst context t1 t2 =
              let term = NCicSubstitution.subst_meta lc term in
                unify hdb test_eq_only metasenv subst context t term
            with NCicUtils.Subst_not_found _-> 
-             instantiate hdb test_eq_only metasenv subst context n lc t true)
+             instantiate hdb test_eq_only metasenv subst context n lc 
+              (NCicReduction.head_beta_reduce ~subst t) true)
 
        | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
             let _,_,term,_ = NCicUtils.lookup_subst i subst in
             let term = NCicSubstitution.subst_meta l term in
-              unify hdb test_eq_only metasenv subst context (mk_appl term args) t2
+              unify hdb test_eq_only metasenv subst context 
+                (mk_appl ~upto:(List.length args) term args) t2
 
        | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
             let _,_,term,_ = NCicUtils.lookup_subst i subst in
             let term = NCicSubstitution.subst_meta l term in
-              unify hdb test_eq_only metasenv subst context t1 (mk_appl term args)
+              unify hdb test_eq_only metasenv subst context t1 
+                (mk_appl ~upto:(List.length args) term args)
 
        |  NCic.Appl (NCic.Meta (i,_)::_ as l1),
           NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
@@ -439,18 +442,32 @@ 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 ("\n\n\n looking for hints for : " ^ 
+              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 -> 
+(*
+            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);
+*)
             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 = 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
               Some (metasenv, subst)
             with
-              UnificationFailure _ | Uncertain _ -> cand_iter tl
+              UnificationFailure _ | Uncertain _ ->
+                prerr_endline (" <candidate fails");
+                cand_iter tl
       in
         cand_iter candidates
     in
@@ -524,7 +541,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 ->