summaryrefslogtreecommitdiff
path: root/parsing/printer.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/printer.ml')
-rw-r--r--parsing/printer.ml156
1 files changed, 80 insertions, 76 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 0c673fbd..7f5087a8 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: printer.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id$ *)
open Pp
open Util
@@ -20,7 +20,6 @@ open Global
open Declare
open Libnames
open Nametab
-open Ppconstr
open Evd
open Proof_type
open Decl_mode
@@ -30,11 +29,11 @@ open Ppconstr
open Constrextern
open Tacexpr
-let emacs_str s alts =
+let emacs_str s alts =
match !Flags.print_emacs, !Flags.print_emacs_safechar with
| true, true -> alts
| true , false -> s
- | false,_ -> ""
+ | false,_ -> ""
(**********************************************************************)
(** Terms *)
@@ -59,6 +58,19 @@ let pr_constr t = pr_constr_env (Global.env()) t
let pr_open_lconstr (_,c) = pr_lconstr c
let pr_open_constr (_,c) = pr_constr c
+let pr_constr_under_binders_env_gen pr env (ids,c) =
+ (* Warning: clashes can occur with variables of same name in env but *)
+ (* we also need to preserve the actual names of the patterns *)
+ (* So what to do? *)
+ let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) ids in
+ pr (push_rels_assum assums env) c
+
+let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_constr_env
+let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_env
+
+let pr_constr_under_binders c = pr_constr_under_binders_env (Global.env()) c
+let pr_lconstr_under_binders c = pr_lconstr_under_binders_env (Global.env()) c
+
let pr_type_core at_top env t =
pr_constr_expr (extern_type at_top env t)
let pr_ltype_core at_top env t =
@@ -78,7 +90,7 @@ let pr_ljudge j = pr_ljudge_env (Global.env()) j
let pr_lrawconstr_env env c =
pr_lconstr_expr (extern_rawconstr (vars_of_env env) c)
-let pr_rawconstr_env env c =
+let pr_rawconstr_env env c =
pr_constr_expr (extern_rawconstr (vars_of_env env) c)
let pr_lrawconstr c =
@@ -115,10 +127,7 @@ let pr_inductive env ind = pr_lconstr_env env (mkInd ind)
let pr_constructor env cstr = pr_lconstr_env env (mkConstruct cstr)
let pr_evaluable_reference ref =
- let ref' = match ref with
- | EvalConstRef const -> ConstRef const
- | EvalVarRef sp -> VarRef sp in
- pr_global ref'
+ pr_global (Tacred.global_of_evaluable_reference ref)
(*let pr_rawterm t =
pr_lconstr (Constrextern.extern_rawconstr Idset.empty t)*)
@@ -134,7 +143,7 @@ let pr_var_decl env (id,c,typ) =
let pbody = match c with
| None -> (mt ())
| Some c ->
- (* Force evaluation *)
+ (* Force evaluation *)
let pb = pr_lconstr_env env c in
let pb = if isCast c then surround pb else pb in
(str" := " ++ pb ++ cut () ) in
@@ -146,7 +155,7 @@ let pr_rel_decl env (na,c,typ) =
let pbody = match c with
| None -> mt ()
| Some c ->
- (* Force evaluation *)
+ (* Force evaluation *)
let pb = pr_lconstr_env env c in
let pb = if isCast c then surround pb else pb in
(str":=" ++ spc () ++ pb ++ spc ()) in
@@ -166,7 +175,7 @@ let pr_named_context_of env =
let psl = List.rev (fold_named_context make_decl_list env ~init:[]) in
hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl)
-let pr_named_context env ne_context =
+let pr_named_context env ne_context =
hv 0 (Sign.fold_named_context
(fun d pps -> pps ++ ws 2 ++ pr_var_decl env d)
ne_context ~init:(mt ()))
@@ -183,14 +192,14 @@ let pr_context_unlimited env =
fold_named_context
(fun env d pps ->
let pidt = pr_var_decl env d in (pps ++ fnl () ++ pidt))
- env ~init:(mt ())
+ env ~init:(mt ())
in
let db_env =
fold_rel_context
(fun env d pps ->
let pnat = pr_rel_decl env d in (pps ++ fnl () ++ pnat))
env ~init:(mt ())
- in
+ in
(sign_env ++ db_env)
let pr_ne_context_of header env =
@@ -201,21 +210,21 @@ let pr_ne_context_of header env =
let pr_context_limit n env =
let named_context = Environ.named_context env in
let lgsign = List.length named_context in
- if n >= lgsign then
+ if n >= lgsign then
pr_context_unlimited env
else
let k = lgsign-n in
let _,sign_env =
fold_named_context
(fun env d (i,pps) ->
- if i < k then
+ if i < k then
(i+1, (pps ++str "."))
else
let pidt = pr_var_decl env d in
(i+1, (pps ++ fnl () ++
str (emacs_str (String.make 1 (Char.chr 253)) "") ++
pidt)))
- env ~init:(0,(mt ()))
+ env ~init:(0,(mt ()))
in
let db_env =
fold_rel_context
@@ -225,10 +234,10 @@ let pr_context_limit n env =
str (emacs_str (String.make 1 (Char.chr 253)) "") ++
pnat))
env ~init:(mt ())
- in
+ in
(sign_env ++ db_env)
-let pr_context_of env = match Flags.print_hyps_limit () with
+let pr_context_of env = match Flags.print_hyps_limit () with
| None -> hv 0 (pr_context_unlimited env)
| Some n -> hv 0 (pr_context_limit n env)
@@ -238,33 +247,33 @@ let pr_restricted_named_context among env =
hv 0 (fold_named_context
(fun env ((id,_,_) as d) pps ->
if true || Idset.mem id among then
- pps ++
+ pps ++
fnl () ++ str (emacs_str (String.make 1 (Char.chr 253)) "") ++
pr_var_decl env d
- else
+ else
pps)
env ~init:(mt ()))
-let pr_predicate pr_elt (b, elts) =
+let pr_predicate pr_elt (b, elts) =
let pr_elts = prlist_with_sep spc pr_elt elts in
if b then
- str"all" ++
+ str"all" ++
(if elts = [] then mt () else str" except: " ++ pr_elts)
else
if elts = [] then str"none" else pr_elts
-
+
let pr_cpred p = pr_predicate pr_con (Cpred.elements p)
let pr_idpred p = pr_predicate Nameops.pr_id (Idpred.elements p)
-let pr_transparent_state (ids, csts) =
+let pr_transparent_state (ids, csts) =
hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++
str"CONSTANTS: " ++ pr_cpred csts ++ fnl ())
let pr_subgoal_metas metas env=
- let pr_one (meta,typ) =
- str "?" ++ int meta ++ str " : " ++
- hov 0 (pr_ltype_env_at_top env typ) ++ fnl () ++
+ let pr_one (meta,typ) =
+ str "?" ++ int meta ++ str " : " ++
+ hov 0 (pr_ltype_env_at_top env typ) ++ fnl () ++
str (emacs_str (String.make 1 (Char.chr 253)) "") in
hv 0 (prlist_with_sep mt pr_one metas)
@@ -276,9 +285,9 @@ let default_pr_goal g =
mt (), mt (),
pr_context_of env,
pr_ltype_env_at_top env g.evar_concl
- else
+ else
(str " *** Declarative Mode ***" ++ fnl ()++fnl ()),
- (str"thesis := " ++ fnl ()),
+ (str "thesis := " ++ fnl ()),
pr_context_of env,
pr_ltype_env_at_top env g.evar_concl
in
@@ -287,7 +296,7 @@ let default_pr_goal g =
str (emacs_str (String.make 1 (Char.chr 253)) "") ++
str "============================" ++ fnl () ++
thesis ++ str " " ++ pc) ++ fnl ()
-
+
(* display the conclusion of a goal *)
let pr_concl n g =
let env = evar_env g in
@@ -296,13 +305,13 @@ let pr_concl n g =
str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" " ++ pc
(* display evar type: a context and a type *)
-let pr_evgl_sign gl =
+let pr_evgl_sign gl =
let ps = pr_named_context_of (evar_unfiltered_env gl) in
let _,l = list_filter2 (fun b c -> not b) (evar_filter gl,evar_context gl) in
let ids = List.rev (List.map pi1 l) in
let warn =
if ids = [] then mt () else
- (str "(" ++ prlist_with_sep pr_coma pr_id ids ++ str " cannot be used)")
+ (str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)")
in
let pc = pr_lconstr gl.evar_concl in
hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]" ++ spc () ++ warn)
@@ -311,10 +320,10 @@ let pr_evgl_sign gl =
let rec pr_evars_int i = function
| [] -> (mt ())
| (ev,evd)::rest ->
- let pegl = pr_evgl_sign evd in
+ let pegl = pr_evgl_sign evd in
let pei = pr_evars_int (i+1) rest in
(hov 0 (str "Existential " ++ int i ++ str " =" ++ spc () ++
- str (string_of_existential ev) ++ str " : " ++ pegl)) ++
+ str (string_of_existential ev) ++ str " : " ++ pegl)) ++
fnl () ++ pei
let default_pr_subgoal n =
@@ -324,27 +333,27 @@ let default_pr_subgoal n =
if p = 1 then
let pg = default_pr_goal g in
v 0 (str "subgoal " ++ int n ++ str " is:" ++ cut () ++ pg)
- else
+ else
prrec (p-1) rest
- in
+ in
prrec n
(* Print open subgoals. Checks for uninstantiated existential variables *)
-let default_pr_subgoals close_cmd sigma = function
- | [] ->
+let default_pr_subgoals close_cmd sigma = function
+ | [] ->
begin
match close_cmd with
Some cmd ->
- (str "Subproof completed, now type " ++ str cmd ++
+ (str "Subproof completed, now type " ++ str cmd ++
str "." ++ fnl ())
| None ->
- let exl = Evarutil.non_instantiated sigma in
- if exl = [] then
- (str"Proof completed." ++ fnl ())
+ let exl = Evarutil.non_instantiated sigma in
+ if exl = [] then
+ (str"Proof completed." ++ fnl ())
else
let pei = pr_evars_int 1 exl in
(str "No more subgoals but non-instantiated existential " ++
- str "variables :" ++fnl () ++ (hov 0 pei))
+ str "variables:" ++ fnl () ++ (hov 0 pei))
end
| [g] ->
let pg = default_pr_goal g in
@@ -355,11 +364,11 @@ let default_pr_subgoals close_cmd sigma = function
| g::rest ->
let pc = pr_concl n g in
let prest = pr_rec (n+1) rest in
- (cut () ++ pc ++ prest)
+ (cut () ++ pc ++ prest)
in
let pg1 = default_pr_goal g1 in
let prest = pr_rec 2 rest in
- v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut ()
+ v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut ()
++ pg1 ++ prest ++ fnl ())
@@ -390,24 +399,19 @@ let pr_goal x = !printer_pr.pr_goal x
(* End abstraction layer *)
(**********************************************************************)
-let pr_subgoals_of_pfts pfts =
- let close_cmd = Decl_mode.get_end_command pfts in
- let gls = fst (Refiner.frontier (proof_of_pftreestate pfts)) in
- let sigma = (top_goal_of_pftreestate pfts).sigma in
- pr_subgoals close_cmd sigma gls
-
let pr_open_subgoals () =
let pfts = get_pftreestate () in
+ let gls = fst (frontier (proof_of_pftreestate pfts)) in
match focus() with
- | 0 ->
- pr_subgoals_of_pfts pfts
- | n ->
- let pf = proof_of_pftreestate pfts in
- let gls = fst (frontier pf) in
+ | 0 ->
+ let sigma = (top_goal_of_pftreestate pfts).sigma in
+ let close_cmd = Decl_mode.get_end_command pfts in
+ pr_subgoals close_cmd sigma gls
+ | n ->
assert (n > List.length gls);
- if List.length gls < 2 then
+ if List.length gls < 2 then
pr_subgoal n gls
- else
+ else
(* LEM TODO: this way of saying how many subgoals has to be abstracted out*)
v 0 (int(List.length gls) ++ str" subgoals" ++ cut () ++
pr_subgoal n gls)
@@ -419,25 +423,25 @@ let pr_nth_open_subgoal n =
(* Elementary tactics *)
let pr_prim_rule = function
- | Intro id ->
+ | Intro id ->
str"intro " ++ pr_id id
-
+
| Cut (b,replace,id,t) ->
if b then
(* TODO: express "replace" *)
(str"assert " ++ str"(" ++ pr_id id ++ str":" ++ pr_lconstr t ++ str")")
else
let cl = if replace then str"clear " ++ pr_id id ++ str"; " else mt() in
- (str"cut " ++ pr_constr t ++
+ (str"cut " ++ pr_constr t ++
str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]")
-
+
| FixRule (f,n,[],_) ->
(str"fix " ++ pr_id f ++ str"/" ++ int n)
-
- | FixRule (f,n,others,j) ->
+
+ | FixRule (f,n,others,j) ->
if j<>0 then warning "Unsupported printing of \"fix\"";
let rec print_mut = function
- | (f,n,ar)::oth ->
+ | (f,n,ar)::oth ->
pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth
| [] -> mt () in
(str"fix " ++ pr_id f ++ str"/" ++ int n ++
@@ -453,26 +457,26 @@ let pr_prim_rule = function
(pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth)
| [] -> mt () in
(str"cofix " ++ pr_id f ++ str" with " ++ print_mut others)
- | Refine c ->
+ | Refine c ->
str(if occur_meta c then "refine " else "exact ") ++
Constrextern.with_meta_as_hole pr_constr c
-
+
| Convert_concl (c,_) ->
(str"change " ++ pr_constr c)
-
+
| Convert_hyp (id,None,t) ->
(str"change " ++ pr_constr t ++ spc () ++ str"in " ++ pr_id id)
| Convert_hyp (id,Some c,t) ->
(str"change " ++ pr_constr c ++ spc () ++ str"in "
++ pr_id id ++ str" (type of " ++ pr_id id ++ str ")")
-
+
| Thin ids ->
(str"clear " ++ prlist_with_sep pr_spc pr_id ids)
-
+
| ThinBody ids ->
(str"clearbody " ++ prlist_with_sep pr_spc pr_id ids)
-
+
| Move (withdep,id1,id2) ->
(str (if withdep then "dependent " else "") ++
str"move " ++ pr_id id1 ++ pr_move_location pr_id id2)
@@ -497,7 +501,7 @@ let prterm = pr_lconstr
(* spiwack: printer function for sets of Environ.assumption.
It is used primarily by the Print Assumption command. *)
-let pr_assumptionset env s =
+let pr_assumptionset env s =
if (Environ.ContextObjectMap.is_empty s) then
str "Closed under the global context"
else
@@ -506,7 +510,7 @@ let pr_assumptionset env s =
let (v,a,o) = r in
match t with
| Variable id -> ( Some (
- Option.default (fnl ()) v
+ Option.default (fnl ()) v
++ str (string_of_id id)
++ str " : "
++ pr_ltype typ
@@ -536,7 +540,7 @@ let pr_assumptionset env s =
)
s (None,None,None)
in
- let (vars,axioms,opaque) =
+ let (vars,axioms,opaque) =
( Option.map (fun p -> str "Section Variables:" ++ p) vars ,
Option.map (fun p -> str "Axioms:" ++ p) axioms ,
Option.map (fun p -> str "Opaque constants:" ++ p) opaque
@@ -550,7 +554,7 @@ let cmap_to_list m = Cmap.fold (fun k v acc -> v :: acc) m []
open Typeclasses
let pr_instance i =
- pr_global (ConstRef (instance_impl i))
+ pr_global (instance_impl i)
let pr_instance_gmap insts =
prlist_with_sep fnl (fun (gr, insts) ->
generated by cgit v1.2.3 (git 2.39.1) at 2025-02-03 00:28:29 +0000