| _ -> t'
end
in
- fun s t ->
+ fun subst t ->
(* incr apply_subst_counter; *)
- apply_subst_gen ~appl_fun s t
+match subst with
+ [] -> t
+ | _ -> apply_subst_gen ~appl_fun subst t
;;
let profiler = HExtlib.profile "U/CicMetaSubst.apply_subst"
profiler.HExtlib.profile (apply_subst s) t
-let rec apply_subst_context subst context =
+let apply_subst_context subst context =
+ match subst with
+ [] -> context
+ | _ ->
(*
incr apply_subst_context_counter;
context_length := !context_length + List.length context;
incr apply_subst_metasenv_counter;
metasenv_length := !metasenv_length + List.length metasenv;
*)
+match subst with
+ [] -> metasenv
+ | _ ->
List.map
(fun (n, context, ty) ->
(n, apply_subst_context subst context, apply_subst subst ty))
let ppsubst_unfolded ~metasenv subst =
String.concat "\n"
(List.map
- (fun (idx, (c, t,_)) ->
+ (fun (idx, (c, t,ty)) ->
let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in
- sprintf "%s |- ?%d:= %s" context idx
+ sprintf "%s |- ?%d : %s := %s" context idx
+(ppterm_in_name_context ~metasenv [] ty name_context)
(ppterm_in_name_context ~metasenv subst t name_context))
subst)
(*
let ppsubst ~metasenv subst =
String.concat "\n"
(List.map
- (fun (idx, (c, t, _)) ->
+ (fun (idx, (c, t, ty)) ->
let context,name_context = ppcontext' ~metasenv ~sep:"; " [] c in
- sprintf "%s |- ?%d:= %s" context idx
+ sprintf "%s |- ?%d : %s := %s" context idx (ppterm_in_name_context ~metasenv [] ty name_context)
(ppterm_in_name_context ~metasenv [] t name_context))
subst)
;;
(!more_to_be_restricted, res)
let rec restrict subst to_be_restricted metasenv =
+ match to_be_restricted with
+ | [] -> metasenv, subst
+ | _ ->
let names_of_context_indexes context indexes =
String.concat ", "
(List.map
raise (MetaSubstFailure error_msg)))
subst ([], [])
in
- match more_to_be_restricted @ more_to_be_restricted' with
- | [] -> (metasenv, subst)
- | l -> restrict subst l metasenv
+ restrict subst (more_to_be_restricted @ more_to_be_restricted') metasenv
;;
(*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)(*Andrea: maybe not*)
let rec deliftaux k =
let module C = Cic in
function
- C.Rel m ->
+ | C.Rel m as t->
if m <=k then
- C.Rel m
+ t
else
- (try
+ (try
match List.nth context (m-k-1) with
Some (_,C.Def (t,_)) ->
(*CSC: Hmmm. This bit of reduction is not in the spirit of *)
C.Rel ((position (m-k) l) + k)
| None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis"))
with
- Failure _ ->
+ Failure _ ->
raise (MetaSubstFailure (lazy "Unbound variable found in deliftaux"))
)
| C.Var (uri,exp_named_subst) ->
let rec liftaux subst metasenv k =
let module C = Cic in
function
- C.Rel m ->
+ C.Rel m as t ->
if m < k then
- C.Rel m, subst, metasenv
+ t, subst, metasenv
else if m < k + n then
raise DeliftingARelWouldCaptureAFreeVariable
else