X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicSubstitution.ml;h=cd97731600dce215e08d9341ac704be529d697a1;hb=0aaed6f96b856d1181a3cd1f2ef3ea4a91990771;hp=17ee01b5333c3638e041d5cde49453123e5275c3;hpb=e626927b4c1c77bdcd6b545203a0a9c17a9ff136;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index 17ee01b53..cd9773160 100644
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -30,7 +30,7 @@ exception ReferenceToConstant;;
 exception ReferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
 
-let lift n =
+let lift_from k n =
  let rec liftaux k =
   let module C = Cic in
    function
@@ -95,12 +95,90 @@ let lift n =
        in
         C.CoFix (i, liftedfl)
  in
+ liftaux k
+
+let lift n t =
   if n = 0 then
-   (function t -> t)
+   t
   else
-   liftaux 1
+   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
+         (failwith "delifting this term whould capture free variables")
+       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
@@ -202,9 +280,10 @@ prerr_endline ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ;
         with
          Not_found ->
           let params =
-           (match CicEnvironment.get_cooked_obj ~trust:true uri with
+           let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+           (match obj with
                C.Constant _ -> raise ReferenceToConstant
-             | C.Variable (_,_,_,params) -> params
+             | C.Variable (_,_,_,params,_) -> params
              | C.CurrentProof _ -> raise ReferenceToCurrentProof
              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
            )
@@ -250,10 +329,11 @@ prerr_endline "---- END\n\n " ;
     | C.Appl _ -> assert false
     | C.Const (uri,exp_named_subst')  ->
        let params =
-        (match CicEnvironment.get_cooked_obj ~trust:true uri with
-            C.Constant (_,_,_,params) -> params
+        let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+        (match obj with
+            C.Constant (_,_,_,params,_) -> params
           | C.Variable _ -> raise ReferenceToVariable
-          | C.CurrentProof (_,_,_,_,params) -> params
+          | C.CurrentProof (_,_,_,_,params,_) -> params
           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
         )
        in
@@ -263,11 +343,12 @@ prerr_endline "---- END\n\n " ;
          C.Const (uri,exp_named_subst'')
     | C.MutInd (uri,typeno,exp_named_subst') ->
        let params =
-        (match CicEnvironment.get_cooked_obj ~trust:true uri with
+        let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+        (match obj with
             C.Constant _ -> raise ReferenceToConstant
           | C.Variable _ -> raise ReferenceToVariable
           | C.CurrentProof _ -> raise ReferenceToCurrentProof
-          | C.InductiveDefinition (_,params,_) -> params
+          | C.InductiveDefinition (_,params,_,_) -> params
         )
        in
         let exp_named_subst'' =
@@ -276,11 +357,12 @@ prerr_endline "---- END\n\n " ;
          C.MutInd (uri,typeno,exp_named_subst'')
     | C.MutConstruct (uri,typeno,consno,exp_named_subst') ->
        let params =
-        (match CicEnvironment.get_cooked_obj ~trust:true uri with
+        let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+        (match obj with
             C.Constant _ -> raise ReferenceToConstant
           | C.Variable _ -> raise ReferenceToVariable
           | C.CurrentProof _ -> raise ReferenceToCurrentProof
-          | C.InductiveDefinition (_,params,_) -> params
+          | C.InductiveDefinition (_,params,_,_) -> params
         )
        in
         let exp_named_subst'' =