merged changes from the svn fork by me and Enrico

[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 4cfc796606650dfc22216c0dea6f8baf2fd51059..130799ea432a7ee1426d7645099c0c40e6a4c5d4 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -65,7 +65,7 @@ let rec deref subst =
       Cic.Meta(n,l) as t -> 
        (try 
           deref subst
-            (CicSubstitution.lift_meta 
+            (CicSubstitution.subst_meta 
                l (snd (CicUtil.lookup_subst n subst))) 
         with 
           CicUtil.Subst_not_found _ -> t)
@@ -99,7 +99,7 @@ let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
         | C.Meta (i,l) as t->
            (try
              let (_, t') = CicMetaSubst.lookup_subst i subst in
-             aux metasenv subst n context (CicSubstitution.lift_meta l t')
+             aux metasenv subst n context (CicSubstitution.subst_meta l t')
                ugraph
             with CicMetaSubst.SubstNotFound _ ->
               let (subst, metasenv, context, local_context,ugraph1) =
@@ -417,7 +417,7 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str
         begin
         try
           let (_, oldt) = CicMetaSubst.lookup_subst n subst in
-          let lifted_oldt = S.lift_meta l oldt in
+          let lifted_oldt = S.subst_meta l oldt in
           let ty_lifted_oldt,ugraph1 =
             type_of_aux' metasenv subst context lifted_oldt ugraph
           in
@@ -436,7 +436,7 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str
             let tyt,ugraph1 = type_of_aux' metasenv subst context t ugraph in
              fo_unif_subst 
               test_equality_only 
-               subst context metasenv tyt (S.lift_meta l meta_type) ugraph1
+               subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
           with AssertFailure _ ->
             (* TODO huge hack!!!!
              * we keep on unifying/refining in the hope that the problem will be
@@ -471,7 +471,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
             (* Unifying the types may have already instantiated n. Let's check *)
             try
              let (_, oldt) = CicMetaSubst.lookup_subst n subst in
-             let lifted_oldt = S.lift_meta l oldt in
+             let lifted_oldt = S.subst_meta l oldt in
               fo_unif_subst_ordered 
                test_equality_only subst context metasenv t lifted_oldt ugraph2
             with
@@ -495,7 +495,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
              in
                fo_unif_subst 
                  test_equality_only 
-                 subst context metasenv tyt (S.lift_meta l meta_type) ugraph1
+                 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
             with 
                UnificationFailure msg 
              | Uncertain msg ->
@@ -532,7 +532,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
         (* Unifying the types may have already instantiated n. Let's check *)
         try
           let (_, oldt,_) = CicUtil.lookup_subst n subst in
-          let lifted_oldt = S.lift_meta l oldt in
+          let lifted_oldt = S.subst_meta l oldt in
             fo_unif_subst_ordered 
               test_equality_only subst context metasenv t lifted_oldt ugraph2
         with
@@ -616,61 +616,50 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
                  else
                    beta_reduce (Cic.Appl(he''::tl'))
            | t -> t in
+       let exists_a_meta l = 
+            List.exists (function Cic.Meta _ -> true | _ -> false) l
+       in
         (match l1,l2 with
-(* andrea : this was too powerful. It works very bad with f_equal and
-   similar terms, try and see 
            C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
              (try 
                List.fold_left2 
-                (fun (subst,metasenv) ->
-                   fo_unif_subst test_equality_only subst context metasenv)
-                 (subst,metasenv) l1 l2
+                (fun (subst,metasenv,ugraph) t1 t2 ->
+                   fo_unif_subst 
+                     test_equality_only subst context metasenv t1 t2 ugraph)
+                 (subst,metasenv,ugraph) l1 l2 
              with (Invalid_argument msg) -> raise (UnificationFailure msg)) 
-         | C.Meta (i,l)::args, _ ->
-<<<<<<< cicUnification.ml
-            let subst,metasenv,t2',ugraph1 =
-             beta_expand_many test_equality_only metasenv subst context t2 args
-               ugraph
-            in
-             subst,metasenv,t1,t2',ugraph1
-=======
+         | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
+        (* we verify that none of the args is a Meta, since beta expanding 
+           with respoect to a metavariable makes no sense 
+         *)
             (try 
               let (_,t,_) = CicUtil.lookup_subst i subst in
-              let lifted = S.lift_meta l t in
+              let lifted = S.subst_meta l t in
                let reduced = beta_reduce (Cic.Appl (lifted::args)) in
               fo_unif_subst 
                 test_equality_only 
-                subst context metasenv reduced t2
+                subst context metasenv reduced t2 ugraph
             with CicUtil.Subst_not_found _ ->
-               let subst,metasenv,beta_expanded =
+               let subst,metasenv,beta_expanded,ugraph1 =
                 beta_expand_many 
-                  test_equality_only metasenv subst context t2 args in
-               fo_unif_subst test_equality_only subst context metasenv 
-                (C.Meta (i,l)) beta_expanded) 
->>>>>>> 1.40
-         | _, C.Meta (i,l)::args ->
-<<<<<<< cicUnification.ml
-            let subst,metasenv,t1',ugraph1 =
-             beta_expand_many test_equality_only metasenv subst context t1 args
-               ugraph
-            in
-             subst,metasenv,t1',t2,ugraph1
-=======
+                  test_equality_only metasenv subst context t2 args ugraph 
+              in
+                 fo_unif_subst test_equality_only subst context metasenv 
+                  (C.Meta (i,l)) beta_expanded ugraph1)
+         | _, C.Meta (i,l)::args when not(exists_a_meta args)  ->
             (try 
               let (_,t,_) = CicUtil.lookup_subst i subst in
-              let lifted = S.lift_meta l t in
+              let lifted = S.subst_meta l t in
                let reduced = beta_reduce (Cic.Appl (lifted::args)) in
               fo_unif_subst 
                 test_equality_only 
-                subst context metasenv t1 reduced
+                subst context metasenv t1 reduced ugraph
             with CicUtil.Subst_not_found _ ->
-               let subst,metasenv,beta_expanded =
+               let subst,metasenv,beta_expanded,ugraph1 =
                 beta_expand_many 
-                  test_equality_only metasenv subst context t1 args in
+                  test_equality_only metasenv subst context t1 args ugraph in
                fo_unif_subst test_equality_only subst context metasenv 
-                (C.Meta (i,l)) beta_expanded)
-*)
-
+                (C.Meta (i,l)) beta_expanded ugraph1)
          | _,_ ->
 (* WAS BEFORE -----
 <<<<<<< cicUnification.ml
@@ -705,7 +694,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
                     test_equality_only subst' metasenv' (l1,l2) ugraph1
              in
                fo_unif_l 
-                test_equality_only subst metasenv (lr1, lr2) ) ugraph(*1*)
+                test_equality_only subst metasenv (lr1, lr2)  ugraph)(**)
    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
        let subst', metasenv',ugraph1 = 
         fo_unif_subst test_equality_only subst context metasenv outt1 outt2