| C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
| C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
- | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t)
+ | C.LetIn (n,s,ty,t) ->
+ C.LetIn (n, liftaux k s, liftaux k ty, liftaux (k+1) t)
| C.Appl l -> C.Appl (List.map (liftaux k) l)
| C.Const (uri,exp_named_subst) ->
let exp_named_subst' =
lift_from 1 n t
;;
-let subst arg =
+(* subst t1 t2 *)
+(* substitutes [t1] for [Rel 1] in [t2] *)
+(* if avoid_beta_redexes is true (default: false) no new beta redexes *)
+(* are generated. WARNING: the substitution can diverge when t2 is not *)
+(* well typed and avoid_beta_redexes is true. *)
+let rec subst ?(avoid_beta_redexes=false) arg =
let rec substaux k =
let module C = Cic in
function
| 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.LetIn (n,s,ty,t) ->
+ C.LetIn (n, substaux k s, substaux k ty, substaux (k + 1) t)
| 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')
+ (* Experimental *)
+ | C.Lambda (_,_,bo) when avoid_beta_redexes ->
+ (match tl' with
+ [] -> assert false
+ | [he] -> subst ~avoid_beta_redexes he bo
+ | he::tl -> C.Appl (subst he bo::tl))
| _ as he' -> C.Appl (he'::tl')
end
| C.Appl _ -> assert false
| 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.LetIn (n,s,ty,t) ->
+ C.LetIn (n, substaux k s, substaux k ty, substaux (k + 1) t)
| C.Appl (he::tl) ->
(* Invariant: no Appl applied to another Appl *)
let tl' = List.map (substaux k) tl in
| 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.LetIn (n,s,ty,t) -> C.LetIn (n, aux k s, aux k ty, aux (k + 1) t)
| C.Appl l -> C.Appl (List.map (aux k) l)
| C.Const (uri,exp_named_subst) ->
let exp_named_subst' =
aux 0 t
;;
+Deannotate.lift := lift;;