summaryrefslogtreecommitdiff
path: root/plugins/decl_mode
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/decl_mode')
-rw-r--r--plugins/decl_mode/decl_expr.mli32
-rw-r--r--plugins/decl_mode/decl_mode.ml26
-rw-r--r--plugins/decl_mode/decl_mode.mli4
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml39
-rw-r--r--plugins/decl_mode/g_decl_mode.ml457
-rw-r--r--plugins/decl_mode/ppdecl_proof.ml169
-rw-r--r--plugins/decl_mode/ppdecl_proof.mli14
7 files changed, 199 insertions, 142 deletions
diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli
index 7467604a..3c4cacbc 100644
--- a/plugins/decl_mode/decl_expr.mli
+++ b/plugins/decl_mode/decl_expr.mli
@@ -46,23 +46,23 @@ type ('constr,'tac) casee =
Real of 'constr
| Virtual of ('constr statement,'constr,'tac) cut
-type ('hyp,'constr,'pat,'tac) bare_proof_instr =
- | Pthen of ('hyp,'constr,'pat,'tac) bare_proof_instr
- | Pthus of ('hyp,'constr,'pat,'tac) bare_proof_instr
- | Phence of ('hyp,'constr,'pat,'tac) bare_proof_instr
+type ('var,'constr,'pat,'tac) bare_proof_instr =
+ | Pthen of ('var,'constr,'pat,'tac) bare_proof_instr
+ | Pthus of ('var,'constr,'pat,'tac) bare_proof_instr
+ | Phence of ('var,'constr,'pat,'tac) bare_proof_instr
| Pcut of ('constr or_thesis statement,'constr,'tac) cut
| Prew of side * ('constr statement,'constr,'tac) cut
- | Psuffices of ((('hyp,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut
- | Passume of ('hyp,'constr) hyp list
- | Plet of ('hyp,'constr) hyp list
- | Pgiven of ('hyp,'constr) hyp list
- | Pconsider of 'constr*('hyp,'constr) hyp list
+ | Psuffices of ((('var,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut
+ | Passume of ('var,'constr) hyp list
+ | Plet of ('var,'constr) hyp list
+ | Pgiven of ('var,'constr) hyp list
+ | Pconsider of 'constr*('var,'constr) hyp list
| Pclaim of 'constr statement
| Pfocus of 'constr statement
- | Pdefine of Id.t * 'hyp list * 'constr
+ | Pdefine of Id.t * 'var list * 'constr
| Pcast of Id.t or_thesis * 'constr
- | Psuppose of ('hyp,'constr) hyp list
- | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list)
+ | Psuppose of ('var,'constr) hyp list
+ | Pcase of 'var list*'pat*(('var,'constr or_thesis) hyp list)
| Ptake of 'constr list
| Pper of elim_type * ('constr,'tac) casee
| Pend of block_type
@@ -70,19 +70,19 @@ type ('hyp,'constr,'pat,'tac) bare_proof_instr =
type emphasis = int
-type ('hyp,'constr,'pat,'tac) gen_proof_instr=
+type ('var,'constr,'pat,'tac) gen_proof_instr=
{emph: emphasis;
- instr: ('hyp,'constr,'pat,'tac) bare_proof_instr }
+ instr: ('var,'constr,'pat,'tac) bare_proof_instr }
type raw_proof_instr =
- ((Id.t*(Constrexpr.constr_expr option)) Loc.located,
+ ((Id.t * (Constrexpr.constr_expr option)) Loc.located,
Constrexpr.constr_expr,
Constrexpr.cases_pattern_expr,
raw_tactic_expr) gen_proof_instr
type glob_proof_instr =
- ((Id.t*(Tacexpr.glob_constr_and_expr option)) Loc.located,
+ ((Id.t * (Tacexpr.glob_constr_and_expr option)) Loc.located,
Tacexpr.glob_constr_and_expr,
Constrexpr.cases_pattern_expr,
Tacexpr.glob_tactic_expr) gen_proof_instr
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index d169dc13..774c20c9 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -89,25 +89,22 @@ let get_info sigma gl=
let try_get_info sigma gl =
Store.get (Goal.V82.extra sigma gl) info
-let get_stack pts =
+let get_goal_stack pts =
let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in
let info = get_info sigma (List.hd goals) in
info.pm_stack
let proof_focus = Proof.new_focus_kind ()
-let proof_cond = Proof.no_cond proof_focus
+let proof_cond = Proof.done_cond proof_focus
let focus p =
- let inf = get_stack p in
+ let inf = get_goal_stack p in
Proof_global.simple_with_current_proof (fun _ -> Proof.focus proof_cond inf 1)
let unfocus () =
Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus proof_focus p ())
-let maximal_unfocus () =
- Proof_global.simple_with_current_proof (fun _ -> Proof.maximal_unfocus proof_focus)
-
let get_top_stack pts =
try
Proof.get_at_focus proof_focus pts
@@ -116,7 +113,24 @@ let get_top_stack pts =
let info = get_info sigma gl in
info.pm_stack
+let get_stack pts = Proof.get_at_focus proof_focus pts
+
let get_last env = match Environ.named_context env with
| (id,_,_)::_ -> id
| [] -> error "no previous statement to use"
+
+let get_end_command pts =
+ match get_top_stack pts with
+ | [] -> "\"end proof\""
+ | Claim::_ -> "\"end claim\""
+ | Focus_claim::_-> "\"end focus\""
+ | Suppose_case :: Per (et,_,_,_) :: _ | Per (et,_,_,_) :: _ ->
+ begin
+ match et with
+ Decl_expr.ET_Case_analysis ->
+ "\"end cases\" or start a new case"
+ | Decl_expr.ET_Induction ->
+ "\"end induction\" or start a new case"
+ end
+ | _ -> anomaly (Pp.str"lonely suppose")
diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli
index 2864ba18..fd7e15c1 100644
--- a/plugins/decl_mode/decl_mode.mli
+++ b/plugins/decl_mode/decl_mode.mli
@@ -72,8 +72,8 @@ val get_last: Environ.env -> Id.t
(** [get_last] raises a [UserError] when it cannot find a previous
statement in the environment. *)
+val get_end_command : Proof.proof -> string
+
val focus : Proof.proof -> unit
val unfocus : unit -> unit
-
-val maximal_unfocus : unit -> unit
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 9d25681d..9d0b7f34 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -131,12 +131,13 @@ let daimon_tac gls =
(* post-instruction focus management *)
-(* spiwack: This used to fail if there was no focusing command
- above, but I don't think it ever happened. I hope it doesn't mess
- things up*)
let goto_current_focus () =
- Decl_mode.maximal_unfocus ()
+ Decl_mode.unfocus ()
+(* spiwack: used to catch errors indicating lack of "focusing command"
+ in the proof tree. In the current implementation, however, entering
+ the declarative mode puts a focus first, there should, therefore,
+ never be exception raised here. *)
let goto_current_focus_or_top () =
goto_current_focus ()
@@ -1444,27 +1445,35 @@ let rec postprocess pts instr =
Type_errors.IllFormedRecBody(_,_,_,_,_)) ->
anomaly (Pp.str "\"end induction\" generated an ill-formed fixpoint")
end
- | Pend _ ->
- goto_current_focus_or_top ()
+ | Pend (B_elim ET_Case_analysis) -> goto_current_focus ()
+ | Pend B_proof -> Proof_global.set_proof_mode "Classic"
+ | Pend _ -> ()
let do_instr raw_instr pts =
let has_tactic = preprocess pts raw_instr.instr in
- begin
+ (* spiwack: hack! [preprocess] assumes that the [pts] is indeed the
+ current proof (and, actually so does [do_instr] later one, so
+ it's ok to do the same here. Ideally the proof should be properly
+ threaded through the commands here, but since the are interleaved
+ with actions on the proof mode, which is attached to the global
+ proof environment, it is not possible without heavy lifting. *)
+ let pts = Proof_global.give_me_the_proof () in
+ let pts =
if has_tactic then
let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in
let gl = { it=List.hd gls ; sigma=sigma; } in
let env= pf_env gl in
- let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; genv = env} in
+ let ist = {ltacvars = Id.Set.empty; genv = env} in
let glob_instr = intern_proof_instr ist raw_instr in
let instr =
interp_proof_instr (get_its_info gl) env sigma glob_instr in
- ignore (Pfedit.by (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp)))
- else () end;
- postprocess pts raw_instr.instr;
- (* spiwack: this should restore a compatible semantics with
- v8.3 where we never stayed focused on 0 goal. *)
- Proof_global.set_proof_mode "Declarative" ;
- Decl_mode.maximal_unfocus ()
+ let (pts',_) = Proof.run_tactic (Global.env())
+ (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp)) pts in
+ pts'
+ else pts
+ in
+ Proof_global.simple_with_current_proof (fun _ _ -> pts);
+ postprocess pts raw_instr.instr
let proof_instr raw_instr =
let p = Proof_global.give_me_the_proof () in
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 03929b3b..d598e7c3 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -19,6 +19,7 @@ open Tok (* necessary for camlp4 *)
open Pcoq.Constr
open Pcoq.Tactic
+open Ppdecl_proof
let pr_goal gs =
let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in
@@ -35,22 +36,20 @@ let pr_goal gs =
str "============================" ++ fnl () ++
thesis ++ str " " ++ pc) ++ fnl ()
-(* arnaud: rebrancher ça ?
-let pr_open_subgoals () =
- let p = Proof_global.give_me_the_proof () in
- let { Evd.it = goals ; sigma = sigma } = Proof.V82.subgoals p in
- let close_cmd = Decl_mode.get_end_command p in
- pr_subgoals close_cmd sigma goals
-*)
-
-let pr_raw_proof_instr _ _ _ instr =
- Errors.anomaly (Pp.str "Cannot print a proof_instr")
- (* arnaud: Il nous faut quelque chose de type extr_genarg_printer si on veut aller
- dans cette direction
- Ppdecl_proof.pr_proof_instr (Global.env()) instr
- *)
-let pr_proof_instr _ _ _ instr = Empty.abort instr
-let pr_glob_proof_instr _ _ _ instr = Empty.abort instr
+let pr_subgoals ?(pr_first=true) _ sigma _ _ _ gll =
+ match gll with
+ | [goal] when pr_first ->
+ pr_goal { Evd.it = goal ; sigma = sigma }
+ | _ ->
+ (* spiwack: it's not very nice to have to call proof global
+ here, a more robust solution would be to add a hook for
+ [Printer.pr_open_subgoals] in proof modes, in order to
+ compute the end command. Yet a more robust solution would be
+ to have focuses give explanations of their unfocusing
+ behaviour. *)
+ let p = Proof_global.give_me_the_proof () in
+ let close_cmd = Decl_mode.get_end_command p in
+ str "Subproof completed, now type " ++ str close_cmd ++ str "."
let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }=
Decl_interp.interp_proof_instr
@@ -65,23 +64,18 @@ let vernac_decl_proof () =
else
begin
Decl_proof_instr.go_to_proof_mode () ;
- Proof_global.set_proof_mode "Declarative" ;
- Vernacentries.print_subgoals ()
+ Proof_global.set_proof_mode "Declarative"
end
(* spiwack: some bureaucracy is not performed here *)
let vernac_return () =
begin
Decl_proof_instr.return_from_tactic_mode () ;
- Proof_global.set_proof_mode "Declarative" ;
- Vernacentries.print_subgoals ()
+ Proof_global.set_proof_mode "Declarative"
end
let vernac_proof_instr instr =
- begin
- Decl_proof_instr.proof_instr instr;
- Vernacentries.print_subgoals ()
- end
+ Decl_proof_instr.proof_instr instr
(* Before we can write an new toplevel command (see below)
which takes a [proof_instr] as argument, we need to declare
@@ -92,7 +86,7 @@ let vernac_proof_instr instr =
(* spiwack: proposal: doing that directly from argextend.ml4, maybe ? *)
(* Only declared at raw level, because only used in vernac commands. *)
-let wit_proof_instr : (raw_proof_instr, Empty.t, Empty.t) Genarg.genarg_type =
+let wit_proof_instr : (raw_proof_instr, glob_proof_instr, proof_instr) Genarg.genarg_type =
Genarg.make0 None "proof_instr"
(* We create a new parser entry [proof_mode]. The Declarative proof mode
@@ -106,14 +100,16 @@ let proof_instr : raw_proof_instr Gram.entry =
let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr
pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr
-let classify_proof_instr _ = VtProofStep false, VtLater
+let classify_proof_instr = function
+ | { instr = Pescape |Pend B_proof } -> VtProofMode "Classic", VtNow
+ | _ -> VtProofStep false, VtLater
(* We use the VERNAC EXTEND facility with a custom non-terminal
to populate [proof_mode] with a new toplevel interpreter.
The "-" indicates that the rule does not start with a distinguished
string. *)
-VERNAC proof_mode EXTEND ProofInstr CLASSIFIED BY classify_proof_instr
- [ - proof_instr(instr) ] -> [ vernac_proof_instr instr ]
+VERNAC proof_mode EXTEND ProofInstr
+ [ - proof_instr(instr) ] => [classify_proof_instr instr] -> [ vernac_proof_instr instr ]
END
(* It is useful to use GEXTEND directly to call grammar entries that have been
@@ -143,7 +139,8 @@ let _ =
(* We substitute the goal printer, by the one we built
for the proof mode. *)
Printer.set_printer_pr { Printer.default_printer_pr with
- Printer.pr_goal = pr_goal }
+ Printer.pr_goal = pr_goal;
+ pr_subgoals = pr_subgoals; }
end ;
(* function [reset] goes back to No Proof Mode from
Declarative Proof Mode *)
@@ -160,7 +157,7 @@ VERNAC COMMAND EXTEND DeclProof
[ "proof" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_decl_proof () ]
END
VERNAC COMMAND EXTEND DeclReturn
-[ "return" ] => [ VtProofMode "Classic", VtNow ] -> [ vernac_return () ]
+[ "return" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_return () ]
END
let none_is_empty = function
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
index 27308666..b3198dbf 100644
--- a/plugins/decl_mode/ppdecl_proof.ml
+++ b/plugins/decl_mode/ppdecl_proof.ml
@@ -12,41 +12,35 @@ open Decl_expr
open Names
open Nameops
-let pr_constr = Printer.pr_constr_env
-let pr_tac = Pptactic.pr_glob_tactic
-let pr_pat mpat = Ppconstr.pr_cases_pattern_expr mpat.pat_expr
-
let pr_label = function
Anonymous -> mt ()
| Name id -> pr_id id ++ spc () ++ str ":" ++ spc ()
-let pr_constr env c = pr_constr env Evd.empty c
-
-let pr_justification_items env = function
+let pr_justification_items pr_constr = function
Some [] -> mt ()
| Some (_::_ as l) ->
spc () ++ str "by" ++ spc () ++
- prlist_with_sep (fun () -> str ",") (pr_constr env) l
+ prlist_with_sep (fun () -> str ",") pr_constr l
| None -> spc () ++ str "by *"
-let pr_justification_method env = function
+let pr_justification_method pr_tac = function
None -> mt ()
| Some tac ->
- spc () ++ str "using" ++ spc () ++ pr_tac env tac
+ spc () ++ str "using" ++ spc () ++ pr_tac tac
-let pr_statement pr_it env st =
- pr_label st.st_label ++ pr_it env st.st_it
+let pr_statement pr_constr st =
+ pr_label st.st_label ++ pr_constr st.st_it
-let pr_or_thesis pr_this env = function
+let pr_or_thesis pr_this = function
Thesis Plain -> str "thesis"
| Thesis (For id) ->
str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id
- | This c -> pr_this env c
+ | This c -> pr_this c
-let pr_cut pr_it env c =
- hov 1 (pr_it env c.cut_stat) ++
- pr_justification_items env c.cut_by ++
- pr_justification_method env c.cut_using
+let pr_cut pr_constr pr_tac pr_it c =
+ hov 1 (pr_it c.cut_stat) ++
+ pr_justification_items pr_constr c.cut_by ++
+ pr_justification_method pr_tac c.cut_using
let type_or_thesis = function
Thesis _ -> Term.mkProp
@@ -54,128 +48,127 @@ let type_or_thesis = function
let _I x = x
-let rec print_hyps pconstr gtyp env sep _be _have hyps =
+let rec pr_hyps pr_var pr_constr gtyp sep _be _have hyps =
let pr_sep = if sep then str "and" ++ spc () else mt () in
match hyps with
(Hvar _ ::_) as rest ->
spc () ++ pr_sep ++ str _have ++
- print_vars pconstr gtyp env false _be _have rest
+ pr_vars pr_var pr_constr gtyp false _be _have rest
| Hprop st :: rest ->
begin
- let nenv =
- match st.st_label with
- Anonymous -> env
- | Name id -> Environ.push_named (id,None,gtyp st.st_it) env in
- spc() ++ pr_sep ++ pr_statement pconstr env st ++
- print_hyps pconstr gtyp nenv true _be _have rest
+ (* let npr_constr env = pr_constr (Environ.push_named (id,None,gtyp st.st_it) env)*)
+ spc() ++ pr_sep ++ pr_statement pr_constr st ++
+ pr_hyps pr_var pr_constr gtyp true _be _have rest
end
| [] -> mt ()
-and print_vars pconstr gtyp env sep _be _have vars =
+and pr_vars pr_var pr_constr gtyp sep _be _have vars =
match vars with
Hvar st :: rest ->
begin
- let nenv =
- match st.st_label with
- Anonymous -> anomaly (Pp.str "anonymous variable")
- | Name id -> Environ.push_named (id,None,st.st_it) env in
+ (* let npr_constr env = pr_constr (Environ.push_named (id,None,gtyp st.st_it) env)*)
let pr_sep = if sep then pr_comma () else mt () in
spc() ++ pr_sep ++
- pr_statement pr_constr env st ++
- print_vars pconstr gtyp nenv true _be _have rest
+ pr_var st ++
+ pr_vars pr_var pr_constr gtyp true _be _have rest
end
| (Hprop _ :: _) as rest ->
let _st = if _be then
str "be such that"
else
str "such that" in
- spc() ++ _st ++ print_hyps pconstr gtyp env false _be _have rest
+ spc() ++ _st ++ pr_hyps pr_var pr_constr gtyp false _be _have rest
| [] -> mt ()
-let pr_suffices_clause env (hyps,c) =
- print_hyps pr_constr _I env false false "to have" hyps ++ spc () ++
- str "to show" ++ spc () ++ pr_or_thesis pr_constr env c
+let pr_suffices_clause pr_var pr_constr (hyps,c) =
+ pr_hyps pr_var pr_constr _I false false "to have" hyps ++ spc () ++
+ str "to show" ++ spc () ++ pr_or_thesis pr_constr c
let pr_elim_type = function
ET_Case_analysis -> str "cases"
| ET_Induction -> str "induction"
-let pr_casee env =function
- Real c -> str "on" ++ spc () ++ pr_constr env c
- | Virtual cut -> str "of" ++ spc () ++ pr_cut (pr_statement pr_constr) env cut
+let pr_block_type = function
+ B_elim et -> pr_elim_type et
+ | B_proof -> str "proof"
+ | B_claim -> str "claim"
+ | B_focus -> str "focus"
+
+let pr_casee pr_constr pr_tac =function
+ Real c -> str "on" ++ spc () ++ pr_constr c
+ | Virtual cut -> str "of" ++ spc () ++ pr_cut pr_constr pr_tac (pr_statement pr_constr) cut
let pr_side = function
Lhs -> str "=~"
| Rhs -> str "~="
-let rec pr_bare_proof_instr _then _thus env = function
+let rec pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac _then _thus = function
| Pescape -> str "escape"
- | Pthen i -> pr_bare_proof_instr true _thus env i
- | Pthus i -> pr_bare_proof_instr _then true env i
- | Phence i -> pr_bare_proof_instr true true env i
+ | Pthen i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac true _thus i
+ | Pthus i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac _then true i
+ | Phence i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac true true i
| Pcut c ->
begin
match _then,_thus with
false,false -> str "have" ++ spc () ++
- pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
+ pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
| false,true -> str "thus" ++ spc () ++
- pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
+ pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
| true,false -> str "then" ++ spc () ++
- pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
+ pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
| true,true -> str "hence" ++ spc () ++
- pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
+ pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
end
| Psuffices c ->
- str "suffices" ++ pr_cut pr_suffices_clause env c
+ str "suffices" ++ pr_cut pr_constr pr_tac (pr_suffices_clause pr_var pr_constr) c
| Prew (sid,c) ->
(if _thus then str "thus" else str " ") ++ spc () ++
- pr_side sid ++ spc () ++ pr_cut (pr_statement pr_constr) env c
+ pr_side sid ++ spc () ++ pr_cut pr_constr pr_tac (pr_statement pr_constr) c
| Passume hyps ->
- str "assume" ++ print_hyps pr_constr _I env false false "we have" hyps
+ str "assume" ++ pr_hyps pr_var pr_constr _I false false "we have" hyps
| Plet hyps ->
- str "let" ++ print_vars pr_constr _I env false true "let" hyps
+ str "let" ++ pr_vars pr_var pr_constr _I false true "let" hyps
| Pclaim st ->
- str "claim" ++ spc () ++ pr_statement pr_constr env st
+ str "claim" ++ spc () ++ pr_statement pr_constr st
| Pfocus st ->
- str "focus on" ++ spc () ++ pr_statement pr_constr env st
+ str "focus on" ++ spc () ++ pr_statement pr_constr st
| Pconsider (id,hyps) ->
- str "consider" ++ print_vars pr_constr _I env false false "consider" hyps
- ++ spc () ++ str "from " ++ pr_constr env id
+ str "consider" ++ pr_vars pr_var pr_constr _I false false "consider" hyps
+ ++ spc () ++ str "from " ++ pr_constr id
| Pgiven hyps ->
- str "given" ++ print_vars pr_constr _I env false false "given" hyps
+ str "given" ++ pr_vars pr_var pr_constr _I false false "given" hyps
| Ptake witl ->
str "take" ++ spc () ++
- prlist_with_sep pr_comma (pr_constr env) witl
+ prlist_with_sep pr_comma pr_constr witl
| Pdefine (id,args,body) ->
str "define" ++ spc () ++ pr_id id ++ spc () ++
prlist_with_sep spc
(fun st -> str "(" ++
- pr_statement pr_constr env st ++ str ")") args ++ spc () ++
- str "as" ++ (pr_constr env body)
+ pr_var st ++ str ")") args ++ spc () ++
+ str "as" ++ (pr_constr body)
| Pcast (id,typ) ->
str "reconsider" ++ spc () ++
- pr_or_thesis (fun _ -> pr_id) env id ++ spc () ++
- str "as" ++ spc () ++ (pr_constr env typ)
+ pr_or_thesis pr_id id ++ spc () ++
+ str "as" ++ spc () ++ (pr_constr typ)
| Psuppose hyps ->
str "suppose" ++
- print_hyps pr_constr _I env false false "we have" hyps
+ pr_hyps pr_var pr_constr _I false false "we have" hyps
| Pcase (params,pat,hyps) ->
str "suppose it is" ++ spc () ++ pr_pat pat ++
(if params = [] then mt () else
(spc () ++ str "with" ++ spc () ++
prlist_with_sep spc
(fun st -> str "(" ++
- pr_statement pr_constr env st ++ str ")") params ++ spc ()))
+ pr_var st ++ str ")") params ++ spc ()))
++
(if hyps = [] then mt () else
(spc () ++ str "and" ++
- print_hyps (pr_or_thesis pr_constr) type_or_thesis
- env false false "we have" hyps))
- | Pper (et,c) ->
+ pr_hyps pr_var (pr_or_thesis pr_constr) type_or_thesis
+ false false "we have" hyps))
+ | Pper (et,c) ->
str "per" ++ spc () ++ pr_elim_type et ++ spc () ++
- pr_casee env c
- | Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et
- | _ -> anomaly (Pp.str "unprintable instruction")
+ pr_casee pr_constr pr_tac c
+ | Pend blk -> str "end" ++ spc () ++ pr_block_type blk
let pr_emph = function
0 -> str " "
@@ -184,7 +177,39 @@ let pr_emph = function
| 3 -> str "*** "
| _ -> anomaly (Pp.str "unknown emphasis")
-let pr_proof_instr env instr =
+let pr_gen_proof_instr pr_var pr_constr pr_pat pr_tac instr =
pr_emph instr.emph ++ spc () ++
- pr_bare_proof_instr false false env instr.instr
+ pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac false false instr.instr
+
+
+let pr_raw_proof_instr pconstr1 pconstr2 ptac (instr : raw_proof_instr) =
+ pr_gen_proof_instr
+ (fun (_,(id,otyp)) ->
+ match otyp with
+ None -> pr_id id
+ | Some typ -> str "(" ++ pr_id id ++ str ":" ++ pconstr1 typ ++str ")"
+ )
+ pconstr2
+ Ppconstr.pr_cases_pattern_expr
+ (ptac Pptactic.ltop)
+ instr
+
+let pr_glob_proof_instr pconstr1 pconstr2 ptac (instr : glob_proof_instr) =
+ pr_gen_proof_instr
+ (fun (_,(id,otyp)) ->
+ match otyp with
+ None -> pr_id id
+ | Some typ -> str "(" ++ pr_id id ++ str ":" ++ pconstr1 typ ++str ")")
+ pconstr2
+ Ppconstr.pr_cases_pattern_expr
+ (ptac Pptactic.ltop)
+ instr
+
+let pr_proof_instr pconstr1 pconstr2 ptac (instr : proof_instr) =
+ pr_gen_proof_instr
+ (fun st -> pr_statement pconstr1 st)
+ pconstr2
+ (fun mpat -> Ppconstr.pr_cases_pattern_expr mpat.pat_expr)
+ (ptac Pptactic.ltop)
+ instr
diff --git a/plugins/decl_mode/ppdecl_proof.mli b/plugins/decl_mode/ppdecl_proof.mli
index fd6fb663..678fc076 100644
--- a/plugins/decl_mode/ppdecl_proof.mli
+++ b/plugins/decl_mode/ppdecl_proof.mli
@@ -1,2 +1,14 @@
-val pr_proof_instr : Environ.env -> Decl_expr.proof_instr -> Pp.std_ppcmds
+open Decl_expr
+open Pptactic
+
+val pr_gen_proof_instr :
+ ('var -> Pp.std_ppcmds) ->
+ ('constr -> Pp.std_ppcmds) ->
+ ('pat -> Pp.std_ppcmds) ->
+ ('tac -> Pp.std_ppcmds) ->
+ ('var,'constr,'pat,'tac) gen_proof_instr -> Pp.std_ppcmds
+
+val pr_raw_proof_instr : raw_proof_instr raw_extra_genarg_printer
+val pr_glob_proof_instr : glob_proof_instr glob_extra_genarg_printer
+val pr_proof_instr : proof_instr extra_genarg_printer
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 03:33:40 +0000