(* Copyright (C) 2003, HELM Team.
+ *
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
let lookup_subst = CicUtil.lookup_subst
;;
-
(* clean_up_meta take a metasenv and a term and make every local context
of each occurrence of a metavariable consistent with its canonical context,
with respect to the hidden hipothesis *)
in
C.CoFix (i, fl')
in
- LibrarySync.merge_coercions (um_aux term)
+ um_aux term
;;
let apply_subst =
| _ -> 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 rec apply_subst_context subst context =
+let profiler = HExtlib.profile "U/CicMetaSubst.apply_subst"
+let apply_subst s t =
+ profiler.HExtlib.profile (apply_subst s) t
+
+
+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))
(***** Pretty printing functions ******)
-let ppterm subst term = CicPp.ppterm (apply_subst subst term)
+let ppterm ~metasenv subst term =
+ CicPp.ppterm ~metasenv (apply_subst subst term)
-let ppterm_in_name_context subst term name_context =
- CicPp.pp (apply_subst subst term) name_context
+let ppterm_in_name_context ~metasenv subst term name_context =
+ CicPp.pp ~metasenv (apply_subst subst term) name_context
-let ppterm_in_context subst term context =
+let ppterm_in_context ~metasenv subst term context =
let name_context =
List.map (function None -> None | Some (n,_) -> Some n) context
in
- ppterm_in_name_context subst term name_context
+ ppterm_in_name_context ~metasenv subst term name_context
+
+let ppterm_in_context_ref = ref ppterm_in_context
+let set_ppterm_in_context f =
+ ppterm_in_context_ref := f
+let use_low_level_ppterm_in_context = ref false
-let ppcontext' ?(sep = "\n") subst context =
+let ppterm_in_context ~metasenv subst term context =
+ if !use_low_level_ppterm_in_context then
+ ppterm_in_context ~metasenv subst term context
+ else
+ !ppterm_in_context_ref ~metasenv subst term context
+
+let ppcontext' ~metasenv ?(sep = "\n") subst context =
let separate s = if s = "" then "" else s ^ sep in
List.fold_right
(fun context_entry (i,name_context) ->
match context_entry with
Some (n,Cic.Decl t) ->
sprintf "%s%s : %s" (separate i) (CicPp.ppname n)
- (ppterm_in_name_context subst t name_context), (Some n)::name_context
+ (ppterm_in_name_context ~metasenv subst t name_context),
+ (Some n)::name_context
| Some (n,Cic.Def (bo,ty)) ->
sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n)
(match ty with
None -> "_"
- | Some ty -> ppterm_in_name_context subst ty name_context)
- (ppterm_in_name_context subst bo name_context), (Some n)::name_context
+ | Some ty -> ppterm_in_name_context ~metasenv subst ty name_context)
+ (ppterm_in_name_context ~metasenv subst bo name_context), (Some n)::name_context
| None ->
sprintf "%s_ :? _" (separate i), None::name_context
) context ("",[])
-let ppsubst_unfolded subst =
+let ppsubst_unfolded ~metasenv subst =
String.concat "\n"
(List.map
- (fun (idx, (c, t,_)) ->
- let context,name_context = ppcontext' ~sep:"; " subst c in
- sprintf "%s |- ?%d:= %s" context idx
- (ppterm_in_name_context subst t name_context))
+ (fun (idx, (c, t,ty)) ->
+ let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in
+ 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)
(*
Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
subst) *)
;;
-let ppsubst subst =
+let ppsubst ~metasenv subst =
String.concat "\n"
(List.map
- (fun (idx, (c, t, _)) ->
- let context,name_context = ppcontext' ~sep:"; " [] c in
- sprintf "%s |- ?%d:= %s" context idx
- (ppterm_in_name_context [] t name_context))
+ (fun (idx, (c, t, ty)) ->
+ let context,name_context = ppcontext' ~metasenv ~sep:"; " [] c in
+ sprintf "%s |- ?%d : %s := %s" context idx (ppterm_in_name_context ~metasenv [] ty name_context)
+ (ppterm_in_name_context ~metasenv [] t name_context))
subst)
;;
-let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context)
+let ppcontext ~metasenv ?sep subst context =
+ fst (ppcontext' ~metasenv ?sep subst context)
let ppmetasenv ?(sep = "\n") subst metasenv =
String.concat sep
(List.map
(fun (i, c, t) ->
- let context,name_context = ppcontext' ~sep:"; " subst c in
+ let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in
sprintf "%s |- ?%d: %s" context i
- (ppterm_in_name_context subst t name_context))
+ (ppterm_in_name_context ~metasenv subst t name_context))
(List.filter
(fun (i, _, _) -> not (List.mem_assoc i subst))
metasenv))
(!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
let error_msg = lazy (sprintf
"Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term"
n (names_of_context_indexes context to_be_restricted) n
- (ppterm subst term))
+ (ppterm ~metasenv subst term))
in
(* DEBUG
debug_print (lazy error_msg);
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 (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *)
- (*CSC: deliftato la regola per il LetIn *)
- (*CSC: FALSO! La regola per il LetIn non lo fa *)
+ 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 *)
(*CSC: first order unification. Does it help or does it harm? *)
+ (*CSC: ANSWER: it hurts performances since it is possible to *)
+ (*CSC: have an exponential explosion of the size of the proof.*)
+ (*CSC: However, without this bit of reduction some "apply" in *)
+ (*CSC: the library fail (e.g. nat/nth_prime.ma). *)
deliftaux k (S.lift m t)
| Some (_,C.Decl t) ->
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) ->
if (i = n) then
raise (MetaSubstFailure (lazy (sprintf
"Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
- i (ppterm subst t))))
+ i (ppterm ~metasenv subst t))))
else
begin
(* I do not consider the term associated to ?i in subst since *)
(List.map
(function Some t -> ppterm subst t | None -> "_") l
)))); *)
- raise (Uncertain (lazy (sprintf
+ let msg = (lazy (sprintf
"Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
- (ppterm subst t)
+ (ppterm ~metasenv subst t)
(String.concat "; "
(List.map
- (function Some t -> ppterm subst t | None -> "_")
- l)))))
+ (function Some t -> ppterm ~metasenv subst t | None -> "_")
+ l))))
+ in
+ if
+ List.exists
+ (function
+ Some t -> CicUtil.is_meta_closed (apply_subst subst t)
+ | None -> true) l
+ then
+ raise (Uncertain msg)
+ else
+ raise (MetaSubstFailure msg)
in
let (metasenv, subst) = restrict subst !to_be_restricted metasenv in
res, metasenv, 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
Format.pp_print_newline ppf ();
Format.pp_print_flush ppf ()
-let fppsubst ppf subst = fpp_gen ppf (ppsubst subst)
+let fppsubst ppf subst = fpp_gen ppf (ppsubst ~metasenv:[] subst)
let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term)
let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv [] metasenv)
-
projects / helm.git / blobdiff