We no longer apply the subst to a Meta in force_does_not_occur. In this

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

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index a28b853bebabcfe3eb9be907cedd24bda2bff868..637c346b06972b7dcc747ff4298414c2824e2899 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -51,24 +51,23 @@ let rec force_does_not_occur subst to_be_restricted t =
     | C.Sort _ as t -> t
     | C.Implicit -> assert false
     | C.Meta (n, l) ->
-        (try
-          aux k (CicSubstitution.lift_meta l (List.assoc n subst))
-        with Not_found ->
-          let l' =
-            let i = ref 0 in
-            List.map
-              (function
-                | None -> None
-                | Some t ->
-                    incr i;
-                    try
-                      Some (aux k t)
-                    with Occur ->
-                      more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
-                      None)
-              l
-          in
-          C.Meta (n, l'))
+       (* we do not retrieve the term associated to ?n in subst since *)
+       (* in this way we can restrict if something goes wrong         *)
+       let l' =
+         let i = ref 0 in
+         List.map
+           (function
+             | None -> None
+             | Some t ->
+                 incr i;
+                 try
+                   Some (aux k t)
+                 with Occur ->
+                   more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
+                   None)
+           l
+       in
+        C.Meta (n, l')
     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
     | C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest)
     | C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest)
@@ -205,7 +204,7 @@ let rec restrict subst to_be_restricted metasenv =
                 "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term"
                 n (names_of_context_indexes context to_be_restricted) n
                 (CicPp.ppterm s)))
-          with Not_found -> (more @ more_to_be_restricted, metasenv', subst))
+           with Not_found -> (more @ more_to_be_restricted @ more_to_be_restricted', metasenv', subst))
         with Occur ->
           raise (MetaSubstFailure (sprintf
             "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them"
@@ -219,14 +218,6 @@ let rec restrict subst to_be_restricted metasenv =
 
 (*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)
 let delift n subst context metasenv l t =
- let l =
-  let (_, canonical_context, _) = CicUtil.lookup_meta n metasenv in
-  List.map2 (fun ct lt ->
-    match (ct, lt) with
-    | None, _ -> None
-    | Some _, _ -> lt)
-    canonical_context l
- in
  let module S = CicSubstitution in
   let to_be_restricted = ref [] in
   let rec deliftaux k =
@@ -267,24 +258,23 @@ let delift n subst context metasenv l t =
             "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
             i (CicPp.ppterm t)))
         else
-          (try
-            deliftaux k (S.lift_meta l (List.assoc i subst))
-          with Not_found ->
-            let rec deliftl j =
-             function
-                [] -> []
-              | None::tl -> None::(deliftl (j+1) tl)
-              | (Some t)::tl ->
-                 let l1' = (deliftl (j+1) tl) in
-                  try
-                   Some (deliftaux k t)::l1'
-                  with
-                     NotInTheList
-                   | MetaSubstFailure _ ->
-                      to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
-            in
-             let l' = deliftl 1 l1 in
-              C.Meta(i,l'))
+         (* I do not consider the term associated to ?i in subst since *)
+         (* in this way I can restrict if something goes wrong.        *)
+          let rec deliftl j =
+           function
+              [] -> []
+            | None::tl -> None::(deliftl (j+1) tl)
+            | (Some t)::tl ->
+               let l1' = (deliftl (j+1) tl) in
+                try
+                 Some (deliftaux k t)::l1'
+                with
+                   NotInTheList
+                 | MetaSubstFailure _ ->
+                    to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
+          in
+           let l' = deliftl 1 l1 in
+            C.Meta(i,l')
      | C.Sort _ as t -> t
      | C.Implicit as t -> t
      | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
@@ -475,6 +465,14 @@ let rec apply_subst_context subst context =
       | None -> None :: context)
     context []
 
+let apply_subst_metasenv subst metasenv =
+  List.map
+    (fun (n, context, ty) ->
+      (n, apply_subst_context subst context, apply_subst subst ty))
+    (List.filter
+      (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
+      metasenv)
+
 let ppterm subst term = CicPp.ppterm (apply_subst subst term)
 
 let ppcontext ?(sep = "\n") subst context =