From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 27 Jan 2004 17:30:09 +0000 (+0000)
Subject: - occur check test anticipated to the delift phase
X-Git-Tag: V_0_2_3~128
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=04ca589d65bcef6bd46cf4d277a748a12e09234b;p=helm.git

- occur check test anticipated to the delift phase
- uses CicUtil.lookup_meta
---

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index f8a73f2f5..a3b27c3e7 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,9 @@ 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 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 +492,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 =
diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli
index 5f29b9bdf..986a595ce 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.mli
+++ b/helm/ocaml/cic_unification/cicMetaSubst.mli
@@ -26,14 +26,14 @@
 exception AssertFailure of string
 exception MetaSubstFailure of string
 
-val delift : 
- Cic.context -> Cic.metasenv -> (Cic.term option) list -> Cic.term ->
-   Cic.term * Cic.metasenv
-
 (* The entry (i,t) in a substitution means that *)
 (* (META i) have been instantiated with t.      *)
 type substitution = (int * Cic.term) list
 
+val delift : 
+  int -> substitution -> Cic.context -> Cic.metasenv -> (Cic.term option) list -> Cic.term ->
+   Cic.term * Cic.metasenv
+
 (* unwind_subst metasenv subst                         *)
 (* unwinds [subst] w.r.t. itself.                      *)
 (* It can restrict some metavariable in the [metasenv] *)
@@ -69,10 +69,10 @@ val ppsubst: substitution -> string
  * From now on we recreate a kernel abstraction where substitutions are part of
  * the calculus *)
 
-val whd: substitution -> Cic.context -> Cic.term -> Cic.term
+val whd: Cic.metasenv -> substitution -> Cic.context -> Cic.term -> Cic.term
 
 val are_convertible:
-  substitution -> Cic.context -> Cic.term -> Cic.term ->
+  Cic.metasenv -> substitution -> Cic.context -> Cic.term -> Cic.term ->
     bool
 
 val type_of_aux':
diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index e3086c801..54fde9a45 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -35,7 +35,6 @@ exception WrongUriToMutualInductiveDefinitions of string;;
 exception RelToHiddenHypothesis;;
 exception MetasenvInconsistency;;
 exception MutCaseFixAndCofixRefineNotImplemented;;
-exception FreeMetaFound of int;;
 exception WrongArgumentNumber;;
 
 let fdebug = ref 0;;
@@ -111,7 +110,7 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt
   let module C = Cic in
   let module R = CicMetaSubst in
   let module Un = CicUnification in 
-  match R.whd subst context expectedtype with
+  match R.whd metasenv subst context expectedtype with
      C.MutInd (_,_,_) ->
        (n,context,actualtype, [term]), subst, metasenv
    | C.Appl (C.MutInd (_,_,_)::tl) ->
@@ -120,7 +119,7 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt
    | C.Prod (name,so,de) ->
       (* we expect that the actual type of the branch has the due 
          number of Prod *)
-      (match R.whd subst context actualtype with
+      (match R.whd metasenv subst context actualtype with
            C.Prod (name',so',de') ->
              let subst, metasenv = 
                 Un.fo_unif_subst subst context metasenv so so' in
@@ -162,12 +161,7 @@ and type_of_aux' metasenv context t =
        decr fdebug ;
        ty,subst',metasenv'
     | C.Meta (n,l) -> 
-       let (_,canonical_context,ty) =
-        try
-         List.find (function (m,_,_) -> n = m) metasenv
-        with
-         Not_found -> raise (FreeMetaFound n)
-       in
+       let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
         let subst',metasenv' =
          check_metasenv_consistency subst metasenv context canonical_context l
         in
@@ -267,7 +261,7 @@ and type_of_aux' metasenv context t =
             raise
              (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
        let rec count_prod t =
-         match CicMetaSubst.whd subst context t with
+         match CicMetaSubst.whd metasenv subst context t with
              C.Prod (_, _, t) -> 1 + (count_prod t)
            | _ -> 0 in 
        let no_args = count_prod arity in
@@ -292,7 +286,7 @@ and type_of_aux' metasenv context t =
        let _, subst, metasenv =
          type_of_aux subst metasenv context expected_type
        in
-       let actual_type = CicMetaSubst.whd subst context actual_type in
+       let actual_type = CicMetaSubst.whd metasenv subst context actual_type in
        let subst,metasenv =
          Un.fo_unif_subst subst context metasenv expected_type actual_type
        in
@@ -342,11 +336,11 @@ and type_of_aux' metasenv context t =
                   type_of_aux subst metasenv context appl
                 in
 *)
-                CicMetaSubst.whd subst context appl
+                CicMetaSubst.whd metasenv subst context appl
               in
                Un.fo_unif_subst subst context metasenv instance instance')
              (subst,metasenv) outtypeinstances in
-        CicMetaSubst.whd subst
+        CicMetaSubst.whd metasenv subst
           context (C.Appl(outtype::right_args@[term])),subst,metasenv
    | C.Fix _
    | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented
@@ -427,8 +421,10 @@ and type_of_aux' metasenv context t =
    let subst',metasenv' = CicMetaSubst.unwind_subst metasenv subst in
    let t1' = CicMetaSubst.apply_subst subst' t1 in
    let t2' = CicMetaSubst.apply_subst subst' t2 in
-    let t1'' = CicMetaSubst.whd subst' context t1' in
-    let t2'' = CicMetaSubst.whd subst' ((Some (name,C.Decl s))::context) t2' in
+    let t1'' = CicMetaSubst.whd metasenv subst' context t1' in
+    let t2'' =
+      CicMetaSubst.whd metasenv subst' ((Some (name,C.Decl s))::context) t2'
+    in
     match (t1'', t2'') with
        (C.Sort s1, C.Sort s2)
          when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
@@ -452,7 +448,7 @@ and type_of_aux' metasenv context t =
   function
      [] -> hetype,subst,metasenv
    | (hete, hety)::tl ->
-    (match (CicMetaSubst.whd subst context hetype) with
+    (match (CicMetaSubst.whd metasenv subst context hetype) with
         Cic.Prod (n,s,t) ->
          let subst',metasenv' =
            CicUnification.fo_unif_subst subst context metasenv s hety
diff --git a/helm/ocaml/cic_unification/cicRefine.mli b/helm/ocaml/cic_unification/cicRefine.mli
index 2d4c0214a..12a4bb98b 100644
--- a/helm/ocaml/cic_unification/cicRefine.mli
+++ b/helm/ocaml/cic_unification/cicRefine.mli
@@ -29,7 +29,6 @@ exception WrongUriToConstant of string
 exception WrongUriToVariable of string
 exception WrongUriToMutualInductiveDefinitions of string
 exception MutCaseFixAndCofixRefineNotImplemented;;
-exception FreeMetaFound of int;;
 
 (* type_of_aux' metasenv context term                        *)
 (* refines [term] and returns the refined form of [term],    *)
diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index e0ec5cb44..704eecb46 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -66,7 +66,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
                 (* First possibility:  restriction    *)
                 (* Second possibility: unification    *)
                 (* Third possibility:  convertibility *)
-                R.are_convertible subst context t1' t2'
+                R.are_convertible metasenv subst context t1' t2'
          ) true ln lm
        in
         if ok then
@@ -85,11 +85,10 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
          let lifted_oldt = S.lift_meta l oldt in
           fo_unif_subst subst context metasenv lifted_oldt t
         with Not_found ->
-         let t',metasenv' = CicMetaSubst.delift context metasenv l t in
+         let t',metasenv' = CicMetaSubst.delift n subst context metasenv l t in
           (n, t')::subst, metasenv'
        in
-        let (_,_,meta_type) = 
-         List.find (function (m,_,_) -> m=n) metasenv' in
+        let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv' in
         let tyt = type_of_aux' metasenv' subst' context t in
          fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt
    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
@@ -165,14 +164,14 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
    | (C.MutConstruct _, _) | (_, C.MutConstruct _)
    | (C.Fix _, _) | (_, C.Fix _) 
    | (C.CoFix _, _) | (_, C.CoFix _) -> 
-       if R.are_convertible subst context t1 t2 then
+       if R.are_convertible metasenv subst context t1 t2 then
         subst, metasenv
        else
         raise (UnificationFailure (sprintf
           "Can't unify %s with %s because they are not convertible"
           (CicPp.ppterm t1) (CicPp.ppterm t2)))
    | (_,_) ->
-       if R.are_convertible subst context t1 t2 then
+       if R.are_convertible metasenv subst context t1 t2 then
         subst, metasenv
        else
         raise (UnificationFailure (sprintf