* http://cs.unibo.it/helm/.
*)
+exception CannotSubstInMeta;;
+exception RelToHiddenHypothesis;;
+
let lift n =
let rec liftaux k =
let module C = Cic in
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)
| 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) ->
in
C.CoFix (i, liftedfl)
in
- liftaux 1
+ if n = 0 then
+ (function t -> t)
+ else
+ liftaux 1
;;
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) ->
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
+;;