X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicSubstitution.ml;h=f312f556c9600fc3ea1179df2d1e54f72ee3867a;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=a4ca7b5cda395a3ec2923e7c263d52efc21a7777;hpb=f2ee9a17174dc0ec833d4caef7d16cdcf8c08302;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index a4ca7b5cd..f312f556c 100644
--- 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,16 +92,31 @@ 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) (*CSC ??? *)
+    | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
     | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
     | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
     | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
-    | C.Appl l -> C.Appl (List.map (substaux k) l)
+    | C.Appl (he::tl) ->
+       (* Invariant: no Appl applied to another Appl *)
+       let tl' = List.map (substaux k) tl in
+        begin
+         match substaux k he with
+            C.Appl l -> C.Appl (l@tl')
+          | _ as he' -> C.Appl (he'::tl')
+        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) ->
@@ -143,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          
+;;