New handling of substitution:

[helm.git] / helm / ocaml / cic_unification / cicUnification.ml

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 81e794c8c6f6709c873f6a6b49802b234ec6d7dc..c8ed004775bdf9d86dfd61fbbe1cdd408864ded0 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -47,7 +47,6 @@ let rec beta_expand test_equality_only metasenv subst context t arg =
  let module S = CicSubstitution in
  let module C = Cic in
   let rec aux metasenv subst n context t' =
-(*prerr_endline ("1 ciclo di beta_expand arg=" ^ CicMetaSubst.ppterm subst arg ^ " ; term=" ^ CicMetaSubst.ppterm subst t') ;*)
    try
     let subst,metasenv =
      fo_unif_subst test_equality_only subst context metasenv arg t'
@@ -65,10 +64,10 @@ let rec beta_expand test_equality_only metasenv subst context t arg =
             subst,metasenv,C.Var (uri,exp_named_subst')
         | C.Meta (i,l) as t->
            (try
-             let t' = List.assoc i subst in
-              aux metasenv subst n context t'
+             let (_, t') = CicMetaSubst.lookup_subst i subst in
+              aux metasenv subst n context (CicSubstitution.lift_meta l t')
             with
-             Not_found -> subst,metasenv,t)
+             CicMetaSubst.SubstNotFound _ -> subst,metasenv,t)
         | C.Sort _
         | C.Implicit _ as t -> subst,metasenv,t
         | C.Cast (te,ty) ->
@@ -155,15 +154,13 @@ let rec beta_expand test_equality_only metasenv subst context t arg =
       let subst,metasenv,t' = aux metasenv subst n context t in
        subst,metasenv,(uri,t')::l) ens (subst,metasenv,[])
   in
-   let argty =
-    type_of_aux' metasenv subst context arg
- in
+  let argty = type_of_aux' metasenv subst context arg in
   let fresh_name =
    FreshNamesGenerator.mk_fresh_name
     metasenv context (Cic.Name "Heta") ~typ:argty
   in
    let subst,metasenv,t' = aux metasenv subst 0 context t in
-    subst,metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg]
+    subst, metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg]
 
 and beta_expand_many test_equality_only metasenv subst context t =
  List.fold_left
@@ -240,18 +237,24 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 =
        in
         begin
         try
-         let oldt = (List.assoc n subst) in
-         let lifted_oldt = S.lift_meta l oldt in
+          let (_, oldt) = CicMetaSubst.lookup_subst n subst in
+          let lifted_oldt = S.lift_meta l oldt in
+          let ty_lifted_oldt =
+            type_of_aux' metasenv subst context lifted_oldt
+          in
+          let tyt = type_of_aux' metasenv subst context t in
+          let (subst, metasenv) =
+            fo_unif_subst_ordered test_equality_only subst context metasenv
+              tyt ty_lifted_oldt
+          in
           fo_unif_subst_ordered 
-           test_equality_only subst context metasenv t lifted_oldt
-        with Not_found ->
+            test_equality_only subst context metasenv t lifted_oldt
+        with CicMetaSubst.SubstNotFound _ ->
          (* First of all we unify the type of the meta with the type of the term *)
          let subst,metasenv =
           let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv in
           (try
-            let tyt =
-              type_of_aux' metasenv subst context t
-            in
+            let tyt = type_of_aux' metasenv subst context t in
              fo_unif_subst 
               test_equality_only 
                subst context metasenv tyt (S.lift_meta l meta_type)
@@ -286,13 +289,20 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
            in
             (* Unifying the types may have already instantiated n. Let's check *)
             try
-             let oldt = (List.assoc n subst) in
+             let (_, oldt) = CicMetaSubst.lookup_subst n subst in
              let lifted_oldt = S.lift_meta l oldt in
               fo_unif_subst_ordered 
                test_equality_only subst context metasenv t lifted_oldt
             with
-             Not_found -> 
-              (n,t'')::subst, metasenv
+             CicMetaSubst.SubstNotFound _ -> 
+               let (_, context, _) = CicUtil.lookup_meta n metasenv in
+               let subst = (n, (context, t'')) :: subst in
+               let metasenv =
+(*                 CicMetaSubst.apply_subst_metasenv [n,(context, t'')] metasenv *)
+                CicMetaSubst.apply_subst_metasenv subst metasenv
+               in
+               subst, metasenv
+(*               (n,t'')::subst, metasenv *)
         end
    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
    | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
@@ -401,14 +411,20 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
          Invalid_argument _ ->
           raise (UnificationFailure (sprintf
             "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))))
-   | (C.Rel _, _) | (_,  C.Rel _)
+   | (C.Rel _, _) | (_,  C.Rel _) ->
+       if t1 = t2 then
+         subst, metasenv
+       else
+        raise (UnificationFailure (sprintf
+          "Can't unify %s with %s because they are not convertible"
+          (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
    | (C.Sort _ ,_) | (_, C.Sort _)
    | (C.Const _, _) | (_, C.Const _)
    | (C.MutInd  _, _) | (_, C.MutInd _)
    | (C.MutConstruct _, _) | (_, C.MutConstruct _)
    | (C.Fix _, _) | (_, C.Fix _) 
    | (C.CoFix _, _) | (_, C.CoFix _) -> 
-       if R.are_convertible subst context t1 t2 then
+       if t1 = t2 || R.are_convertible subst context t1 t2 then
         subst, metasenv
        else
         raise (UnificationFailure (sprintf