From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jul 2015 10:36:12 +0200 Subject: Imported Upstream version 8.5~beta2+dfsg --- plugins/decl_mode/decl_expr.mli | 32 +++---- plugins/decl_mode/decl_mode.ml | 26 ++++-- plugins/decl_mode/decl_mode.mli | 4 +- plugins/decl_mode/decl_proof_instr.ml | 39 +++++--- plugins/decl_mode/g_decl_mode.ml4 | 57 ++++++------ plugins/decl_mode/ppdecl_proof.ml | 169 +++++++++++++++++++--------------- plugins/decl_mode/ppdecl_proof.mli | 14 ++- 7 files changed, 199 insertions(+), 142 deletions(-) (limited to 'plugins/decl_mode') 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 -- cgit v1.2.3