X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=6d8b03ddb4c4d73832553ed172670b8ca2b00780;hb=8b8606be3b086e20ead16ca7417da5f1c4e02e79;hp=f8a73f2f53b0fd4e00cfb3e73f4d832def6a2fd3;hpb=6696898978f86977863429cc3a8690d2546a918b;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index f8a73f2f5..6d8b03ddb 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -3,7 +3,8 @@ open Printf
 
 exception AssertFailure of string
 exception MetaSubstFailure of string
-exception RelToHiddenHypothesis
+
+exception RelToHiddenHypothesis (* TODO remove this exception *)
 
 let debug_print = prerr_endline
 
@@ -16,17 +17,19 @@ let ppsubst subst =
       subst)
 
 (**** DELIFT ****)
-
-(* the delift function takes in input an ordered list of optional terms       *)
-(* [t1,...,tn] and a term t, and substitutes every tk = Some (rel(nk)) with   *)
-(* rel(k). Typically, the list of optional terms is the explicit substitution *)
-(* that is applied to a metavariable occurrence and the result of the delift  *)
-(* function is a term the implicit variable can be substituted with to make   *)
-(* the term [t] unifiable with the metavariable occurrence.                   *)
-(* In general, the problem is undecidable if we consider equivalence in place *)
-(* of alpha convertibility. Our implementation, though, is even weaker than   *)
-(* alpha convertibility, since it replace the term [tk] if and only if [tk]   *)
-(* is a Rel (missing all the other cases). Does this matter in practice?      *)
+(* the delift function takes in input a metavariable index, an ordered list of
+ * optional terms [t1,...,tn] and a term t, and substitutes every tk = Some
+ * (rel(nk)) with rel(k).  Typically, the list of optional terms is the explicit
+ * substitution that is applied to a metavariable occurrence and the result of
+ * the delift function is a term the implicit variable can be substituted with
+ * to make the term [t] unifiable with the metavariable occurrence.  In general,
+ * the problem is undecidable if we consider equivalence in place of alpha
+ * convertibility. Our implementation, though, is even weaker than alpha
+ * convertibility, since it replace the term [tk] if and only if [tk] is a Rel
+ * (missing all the other cases). Does this matter in practice?
+ * The metavariable index is the index of the metavariable that must not occur
+ * in the term (for occur check).
+ *)
 
 exception NotInTheList;;
 
@@ -60,7 +63,7 @@ let restrict to_be_restricted =
 ;;
 
 (*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)
-let delift context metasenv l t =
+let delift n subst context metasenv l t =
  let module S = CicSubstitution in
   let to_be_restricted = ref [] in
   let rec deliftaux k =
@@ -96,21 +99,30 @@ let delift context metasenv l t =
         in
          C.Var (uri,exp_named_subst')
      | C.Meta (i, l1) as t -> 
-        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
-                 RelToHiddenHypothesis
-               | NotInTheList ->
-                  to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
-        in
-         let l' = deliftl 1 l1 in
-          C.Meta(i,l')
+        if i = n then
+          raise (MetaSubstFailure (sprintf
+            "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
+                     RelToHiddenHypothesis
+                   | 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)
@@ -201,15 +213,12 @@ let rec unwind metasenv subst unwinded t =
               let t = List.assoc i subst in
               let t',metasenv' = um_aux metasenv t in
               let _,metasenv'' =
-               let (_,canonical_context,_) = 
-                List.find (function (m,_,_) -> m=i) metasenv
-               in
-                delift canonical_context metasenv' l t'
+               let (_,canonical_context,_) = CicUtil.lookup_meta i metasenv in
+                delift i subst canonical_context metasenv' l t'
               in
                unwinded := (i,t')::!unwinded ;
                S.lift_meta l t', metasenv'
-             with
-              Not_found ->
+             with Not_found ->
                (* not constrained variable, i.e. free in subst*)
                let l',metasenv' =
                 List.fold_right
@@ -459,9 +468,7 @@ let ppmetasenv ?(sep = "\n") subst metasenv =
 let unwind_subst metasenv subst =
   List.fold_left
    (fun (unwinded,metasenv) (i,_) ->
-     let (_,canonical_context,_) =
-       List.find (function (m,_,_) -> m=i) metasenv
-     in
+     let (_,canonical_context,_) = CicUtil.lookup_meta i metasenv in
      let identity_relocation_list =
       CicMkImplicit.identity_relocation_list_for_metavariable canonical_context
      in
@@ -474,7 +481,19 @@ let unwind_subst metasenv subst =
 (* From now on we recreate a kernel abstraction where substitutions are part of
  * the calculus *)
 
-let whd subst context term =
+let lift metasenv subst n term =
+  (* TODO unwind's result is thrown away :-( *)
+  let (subst, _) = unwind_subst metasenv subst in
+  let term = apply_subst subst term in
+  try
+    CicSubstitution.lift n term
+  with e ->
+    raise (MetaSubstFailure ("Lift failure: " ^
+      Printexc.to_string e))
+
+let whd metasenv subst context term =
+  (* TODO unwind's result is thrown away :-( *)
+  let (subst, _) = unwind_subst metasenv subst in
   let term = apply_subst subst term in
   let context = apply_subst_context subst context in
   try
@@ -483,12 +502,16 @@ let whd subst context term =
     raise (MetaSubstFailure ("Weak head reduction failure: " ^
       Printexc.to_string e))
 
-let are_convertible subst context t1 t2 =
+let are_convertible metasenv subst context t1 t2 =
+  (* TODO unwind's result is thrown away :-( *)
+  let (subst, _) = unwind_subst metasenv subst in
   let context = apply_subst_context subst context in
   let (t1, t2) = (apply_subst subst t1, apply_subst subst t2) in
   CicReduction.are_convertible context t1 t2
 
 let type_of_aux' metasenv subst context term =
+  (* TODO unwind's result is thrown away :-( *)
+  let (subst, _) = unwind_subst metasenv subst in
   let term = apply_subst subst term in
   let context = apply_subst_context subst context in
   let metasenv =