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 *)
(***** 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 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' ?(sep = "\n") subst 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))
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);
if m <=k then
C.Rel m
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) ->
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 *)
)))); *)
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 -> "_")
+ (function Some t -> ppterm ~metasenv subst t | None -> "_")
l))))
in
if
- (*CSC: WARNING: if we are working up to reduction (I do not think so),
- the following test should be replaced with "all the terms in l are
- meta-closed" *)
- not
- (List.exists (function Some (Cic.Meta _) -> true | _ -> false ) l)
+ List.exists
+ (function
+ Some t -> CicUtil.is_meta_closed (apply_subst subst t)
+ | None -> true) l
then
- raise (MetaSubstFailure msg)
- else
raise (Uncertain msg)
+ else
+ raise (MetaSubstFailure msg)
in
let (metasenv, subst) = restrict subst !to_be_restricted metasenv in
res, metasenv, subst
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