CicSubstitution.delift ==> CicMetaSubst.delift_rels

(since it will need to restrict metavariables in case of Rel capture)

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index 229da24f0fdbdf7b5183c288fe1e8d5ac05937c9..2abce6a0edc635fbfffc3df5bd40c4bf990fc78d 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -29,7 +29,6 @@ exception ReferenceToVariable;;
 exception ReferenceToConstant;;
 exception ReferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
-exception DeliftingWouldCaptureAFreeVariable;;
 
 let debug_print = fun _ -> ()
 
@@ -107,81 +106,6 @@ let lift n t =
    lift_from 1 n t
 ;;
 
-(* delifts a term t of n levels strating from k, that is changes (Rel m)
- * to (Rel (m - n)) when m > (k + n). if k <= m < k + n delift fails
- *)
-let delift_from k n =
- let rec liftaux k =
-  let module C = Cic in
-   function
-      C.Rel m ->
-       if m < k then
-        C.Rel m
-       else if m < k + n then
-         raise DeliftingWouldCaptureAFreeVariable
-       else
-        C.Rel (m - n)
-    | C.Var (uri,exp_named_subst) ->
-       let exp_named_subst' = 
-        List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
-       in
-        C.Var (uri,exp_named_subst')
-    | C.Meta (i,l) ->
-       let l' =
-        List.map
-         (function
-             None -> None
-           | Some t -> Some (liftaux k t)
-         ) l
-       in
-        C.Meta(i,l')
-    | C.Sort _ as t -> t
-    | C.Implicit _ as t -> t
-    | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
-    | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
-    | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
-    | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t)
-    | C.Appl l -> C.Appl (List.map (liftaux k) l)
-    | C.Const (uri,exp_named_subst) ->
-       let exp_named_subst' = 
-        List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
-       in
-        C.Const (uri,exp_named_subst')
-    | C.MutInd (uri,tyno,exp_named_subst) ->
-       let exp_named_subst' = 
-        List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
-       in
-        C.MutInd (uri,tyno,exp_named_subst')
-    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
-       let exp_named_subst' = 
-        List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
-       in
-        C.MutConstruct (uri,tyno,consno,exp_named_subst')
-    | C.MutCase (sp,i,outty,t,pl) ->
-       C.MutCase (sp, i, liftaux k outty, liftaux k t,
-        List.map (liftaux k) pl)
-    | C.Fix (i, fl) ->
-       let len = List.length fl in
-       let liftedfl =
-        List.map
-         (fun (name, i, ty, bo) -> (name, i, liftaux k ty, liftaux (k+len) bo))
-          fl
-       in
-        C.Fix (i, liftedfl)
-    | C.CoFix (i, fl) ->
-       let len = List.length fl in
-       let liftedfl =
-        List.map
-         (fun (name, ty, bo) -> (name, liftaux k ty, liftaux (k+len) bo))
-          fl
-       in
-        C.CoFix (i, liftedfl)
- in
- liftaux k
-
-let delift n t =
-  delift_from 1 n t
- 
 let subst arg =
  let rec substaux k =
   let module C = Cic in

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.mli b/helm/ocaml/cic_proof_checking/cicSubstitution.mli
index 5c8fa7ca59b8e31bc3019f71ef0a3cbd91ac0354..21a1f5d0e579d775c9e1ea2117b56898506f1990 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.mli
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.mli
@@ -28,17 +28,13 @@ exception RelToHiddenHypothesis;;
 exception ReferenceToVariable;;
 exception ReferenceToConstant;;
 exception ReferenceToInductiveDefinition;;
-exception DeliftingWouldCaptureAFreeVariable;;
 
 (* lift n t         *)
 (* lifts [t] of [n] *)
+(* NOTE: the opposite function (delift_rels) is defined in CicMetaSubst *)
+(* since it needs to restrict the metavariables in case of failure      *)
 val lift : int -> Cic.term -> Cic.term
 
-(** delifts t of n
- *  @raise Failure s
- *)
-val delift : int -> Cic.term -> Cic.term
- 
 
 (* lift from n t *)
 (* as lift but lifts only indexes >= from *)

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index eaa094fdcf464147727fa61a139a6c95804044a1..021e87ea5c6a6c1221566fcf42b3b0dfe6bca738 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -71,6 +71,7 @@ context length: %d (avg = %.2f)
 exception MetaSubstFailure of string
 exception Uncertain of string
 exception AssertFailure of string
+exception DeliftingARelWouldCaptureAFreeVariable;;
 
 let debug_print = fun _ -> ()
 
@@ -757,6 +758,82 @@ debug_print(sprintf
     res, metasenv, subst
 ;;
 
+(* delifts a term t of n levels strating from k, that is changes (Rel m)
+ * to (Rel (m - n)) when m > (k + n). if k <= m < k + n delift fails
+ *)
+let delift_rels_from k n =
+ let rec liftaux k =
+  let module C = Cic in
+   function
+      C.Rel m ->
+       if m < k then
+        C.Rel m
+       else if m < k + n then
+         raise DeliftingARelWouldCaptureAFreeVariable
+       else
+        C.Rel (m - n)
+    | C.Var (uri,exp_named_subst) ->
+       let exp_named_subst' = 
+        List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
+       in
+        C.Var (uri,exp_named_subst')
+    | C.Meta (i,l) ->
+       let l' =
+        List.map
+         (function
+             None -> None
+           | Some t -> Some (liftaux k t)
+         ) l
+       in
+        C.Meta(i,l')
+    | C.Sort _ as t -> t
+    | C.Implicit _ as t -> t
+    | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
+    | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
+    | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
+    | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t)
+    | C.Appl l -> C.Appl (List.map (liftaux k) l)
+    | C.Const (uri,exp_named_subst) ->
+       let exp_named_subst' = 
+        List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
+       in
+        C.Const (uri,exp_named_subst')
+    | C.MutInd (uri,tyno,exp_named_subst) ->
+       let exp_named_subst' = 
+        List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
+       in
+        C.MutInd (uri,tyno,exp_named_subst')
+    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+       let exp_named_subst' = 
+        List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
+       in
+        C.MutConstruct (uri,tyno,consno,exp_named_subst')
+    | C.MutCase (sp,i,outty,t,pl) ->
+       C.MutCase (sp, i, liftaux k outty, liftaux k t,
+        List.map (liftaux k) pl)
+    | C.Fix (i, fl) ->
+       let len = List.length fl in
+       let liftedfl =
+        List.map
+         (fun (name, i, ty, bo) -> (name, i, liftaux k ty, liftaux (k+len) bo))
+          fl
+       in
+        C.Fix (i, liftedfl)
+    | C.CoFix (i, fl) ->
+       let len = List.length fl in
+       let liftedfl =
+        List.map
+         (fun (name, ty, bo) -> (name, liftaux k ty, liftaux (k+len) bo))
+          fl
+       in
+        C.CoFix (i, liftedfl)
+ in
+ liftaux k
+
+let delift_rels n t =
+  delift_rels_from 1 n t
+ 
+
 (**** END OF DELIFT ****)
 
 

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli
index 9a0bee6ae842d2c551778843bf809ce857a422a6..04e493ec27b46fce5f0c403a4096b4e469deac82 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.mli
+++ b/helm/ocaml/cic_unification/cicMetaSubst.mli
@@ -26,6 +26,7 @@
 exception MetaSubstFailure of string
 exception Uncertain of string
 exception AssertFailure of string
+exception DeliftingARelWouldCaptureAFreeVariable;;
 
 (* The entry (i,t) in a substitution means that *)
 (* (META i) have been instantiated with t.      *)
@@ -50,6 +51,12 @@ val delift :
 val restrict :
   Cic.substitution -> (int * int) list -> Cic.metasenv -> 
   Cic.metasenv * Cic.substitution 
+
+(** delifts the Rels in t of n
+ *  @raise DeliftingARelWouldCaptureAFreeVariable
+ *)
+val delift_rels : int -> Cic.term -> Cic.term
+ 
 (** {2 Pretty printers} *)
 
 val ppsubst_unfolded: Cic.substitution -> string

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 57e4c5e9d6fff45e438c96cc7f4b3f781ee71700..e64499b3b94a819723a603fe803efab7fc067a91 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -507,7 +507,7 @@ and type_of_aux' metasenv context t ugraph =
                  | (constructor_args_no,_,instance,_)::tl -> 
                      try
                        let instance' = 
-                         CicSubstitution.delift constructor_args_no
+                         CicMetaSubst.delift_rels constructor_args_no
                            (CicMetaSubst.apply_subst subst instance)
                        in
                        let candidate,ugraph,metasenv,subst =
@@ -519,7 +519,7 @@ and type_of_aux' metasenv context t ugraph =
                                | Some ty ->
                                  try 
                                    let instance' = 
-                                     CicSubstitution.delift
+                                     CicMetaSubst.delift_rels
                                       constructor_args_no
                                        (CicMetaSubst.apply_subst subst instance)
                                    in
@@ -529,7 +529,7 @@ and type_of_aux' metasenv context t ugraph =
                                    in
                                     candidate_oty,ugraph,metasenv,subst
                                  with
-                                    CicSubstitution.DeliftingWouldCaptureAFreeVariable
+                                    CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
                                   | CicUnification.UnificationFailure _
                                   | CicUnification.Uncertain _ ->
                                      None,ugraph,metasenv,subst
@@ -549,7 +549,7 @@ and type_of_aux' metasenv context t ugraph =
                            Some
                             (add_lambdas 0 t arity_instantiated_with_left_args),
                            ugraph,metasenv,subst
-                     with CicSubstitution.DeliftingWouldCaptureAFreeVariable -> 
+                     with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
                        None,ugraph4,metasenv,subst
                in
                match candidate with