## prefix is now used for tinycals

[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 c6f4f6d9139cf1146f465791457cc800090c5712..55ccca12a0c79dc16fc84180af3dab442dc66bb3 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 _ = ();;
 
@@ -249,12 +248,17 @@ and unify hdb test_eq_only metasenv subst context t1 t2 =
  (*D*) inside 'U'; try let rc =
    let fo_unif test_eq_only metasenv subst t1 t2 =
     (*D*) inside 'F'; try let rc =  
-     pp (lazy("  " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ 
-         NCicPp.ppterm ~metasenv ~subst ~context t2));
+     pp (lazy("  " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^ 
+         NCicPp.ppterm ~metasenv ~subst ~context t2 ^ "\n" ^ NCicPp.ppmetasenv
+         ~subst metasenv));
      if t1 === t2 then
        metasenv, subst
      else
        match (t1,t2) with
+       | C.Appl [_], _ | _, C.Appl [_] | C.Appl [], _ | _, C.Appl [] 
+       | C.Appl (C.Appl _::_), _ | _, C.Appl (C.Appl _::_) -> 
+           prerr_endline "Appl [Appl _;_] or Appl [] or Appl [_] invariant";
+           assert false 
        | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only -> 
            if NCicEnvironment.universe_leq a b then metasenv, subst
            else raise (fail_exc metasenv subst context t1 t2)
@@ -314,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 
@@ -322,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 ->
@@ -434,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
@@ -519,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 ->