Initial revision

[helm.git] / helm / ocaml / cic_proof_checking / cicSubstitution.ml

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index b683dd258389f93b698403ac801b787354da9a46..f312f556c9600fc3ea1179df2d1e54f72ee3867a 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -23,6 +23,9 @@
  * http://cs.unibo.it/helm/.
  *)
 
+exception CannotSubstInMeta;;
+exception RelToHiddenHypothesis;;
+
 let lift n =
  let rec liftaux k =
   let module C = Cic in
@@ -33,7 +36,15 @@ let lift n =
        else
         C.Rel (m + n)
     | C.Var _  as t -> t
-    | C.Meta _ as t -> t
+    | 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)
@@ -42,7 +53,6 @@ let lift n =
     | 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 _ as t -> t
-    | C.Abst _  as t -> t
     | C.MutInd _ as t -> t
     | C.MutConstruct _ as t -> t
     | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
@@ -82,7 +92,15 @@ let subst arg =
          | _            -> C.Rel (n - 1)
        )
     | C.Var _ as t  -> t
-    | C.Meta _ as t -> t
+    | C.Meta (i, l) as t -> 
+       let l' =
+        List.map
+         (function
+             None -> None
+           | Some t -> Some (substaux k t)
+         ) l
+       in
+        C.Meta(i,l')
     | C.Sort _ as t -> t
     | C.Implicit as t -> t
     | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
@@ -99,7 +117,6 @@ let subst arg =
         end
     | C.Appl _ -> assert false
     | C.Const _ as t -> t
-    | C.Abst _ as t -> t
     | C.MutInd _ as t -> t
     | C.MutConstruct _ as t -> t
     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
@@ -151,3 +168,65 @@ let undebrujin_inductive_def uri =
        Cic.InductiveDefinition (dl', params, n_ind_params)
   | obj -> obj
 ;;
+
+(* l is the relocation list *)
+
+let lift_meta l t = 
+    let module C = Cic in
+    if l = [] then t else 
+    let rec aux k = function
+      C.Rel n as t -> 
+       if n <= k then t else 
+         (try
+           match List.nth l (n-k-1) with
+              None -> raise RelToHiddenHypothesis
+            | Some t -> lift k t
+          with
+           (Failure _) -> assert false
+         )
+    | C.Var _ as t  -> t
+    | C.Meta (i,l) ->
+       let l' =
+        List.map
+         (function
+             None -> None
+           | Some t ->
+              try
+               Some (aux k t)
+              with
+               RelToHiddenHypothesis -> None
+         ) l
+       in
+        C.Meta(i,l')
+    | C.Sort _ as t -> t
+    | C.Implicit as t -> t
+    | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) (*CSC ??? *)
+    | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t)
+    | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t)
+    | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k + 1) t)
+    | C.Appl l -> C.Appl (List.map (aux k) l)
+    | C.Const _ as t -> t
+    | C.MutInd _ as t -> t
+    | C.MutConstruct _ as t -> t
+    | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
+       C.MutCase (sp,cookingsno,i,aux k outt, aux k t,
+        List.map (aux k) pl)
+    | C.Fix (i,fl) ->
+       let len = List.length fl in
+       let substitutedfl =
+        List.map
+         (fun (name,i,ty,bo) -> (name, i, aux k ty, aux (k+len) bo))
+          fl
+       in
+        C.Fix (i, substitutedfl)
+    | C.CoFix (i,fl) ->
+       let len = List.length fl in
+       let substitutedfl =
+        List.map
+         (fun (name,ty,bo) -> (name, aux k ty, aux (k+len) bo))
+          fl
+       in
+        C.CoFix (i, substitutedfl)
+ in
+  aux 0 t          
+;;