delift moved from cicSubstitution to cicUnification

[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 28dbe24e3f40cb73964d86cbf1896fc67d8929e5..ae51f35803e20cfd6467b54983afbe6b0dd5747d 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)
@@ -65,7 +76,10 @@ let lift n =
        in
         C.CoFix (i, liftedfl)
  in
-  liftaux 1
+  if n = 0 then
+   (function t -> t)
+  else
+   liftaux 1
 ;;
 
 let subst arg =
@@ -79,14 +93,30 @@ 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
@@ -140,3 +170,66 @@ 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.Abst _ 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          
+;;