type naif_substitution = (int * Cic.term) list
-let naif_apply_subst subst term =
+let naif_apply_subst lift subst term =
let rec aux k t =
match t with
Cic.Rel _ -> t
Cic.Var (uri, exp_named_subst')
| Cic.Meta (i, l) ->
(try
- aux k (CicSubstitution.lift k (List.assoc i subst))
+ aux k (CicSubstitution.lift (k+lift) (List.assoc i subst))
with Not_found -> t)
| Cic.Sort _
| Cic.Implicit _ -> t
| Cic.Cast (te,ty) -> Cic.Cast (aux k te, aux k ty)
| Cic.Prod (n,s,t) -> Cic.Prod (n, aux k s, aux (k+1) t)
| Cic.Lambda (n,s,t) -> Cic.Lambda (n, aux k s, aux (k+1) t)
- | Cic.LetIn (n,s,t) -> Cic.LetIn (n, aux k s, aux (k+1) t)
+ | Cic.LetIn (n,s,ty,t) -> Cic.LetIn (n, aux k s, aux k ty, aux (k+1) t)
| Cic.Appl [] -> assert false
| Cic.Appl l -> Cic.Appl (List.map (aux k) l)
| Cic.Const (uri,exp_named_subst) ->
let naif_apply_subst_metasenv subst metasenv =
List.map
(fun (n, context, ty) ->
- (n, context, naif_apply_subst subst ty))
+ (n, context, naif_apply_subst 0 subst ty))
(List.filter
(fun (i, _, _) -> not (List.mem_assoc i subst))
metasenv)
let naif_buildsubst n context t ty tail = (n,t) :: tail ;;
let naif_flatten_subst subst =
- List.map (fun (i,t) -> i, naif_apply_subst subst t ) subst
+ List.map (fun (i,t) -> i, naif_apply_subst 0 subst t ) subst
;;
let rec naif_lookup_subst meta subst =
(********** ACTUAL SUBSTITUTION IMPLEMENTATION *******************************)
type substitution = naif_substitution
-let apply_subst = naif_apply_subst
+let apply_subst = naif_apply_subst 0
+let apply_subst_lift = naif_apply_subst
let apply_subst_metasenv = naif_apply_subst_metasenv
let ppsubst ?(names=[]) l = naif_ppsubst names l
let buildsubst = naif_buildsubst
let empty_subst = [];;
-let concat_substs x y = x @ y;;
+let concat x y = x @ y;;
+