aboutsummaryrefslogtreecommitdiff
path: root/plugins/decl_mode
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/decl_mode')
-rw-r--r--plugins/decl_mode/decl_expr.mli36
-rw-r--r--plugins/decl_mode/decl_interp.ml22
-rw-r--r--plugins/decl_mode/decl_interp.mli2
-rw-r--r--plugins/decl_mode/decl_mode.ml32
-rw-r--r--plugins/decl_mode/decl_mode.mli6
-rw-r--r--plugins/decl_mode/decl_mode_plugin.mlpack (renamed from plugins/decl_mode/decl_mode_plugin.mllib)1
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml187
-rw-r--r--plugins/decl_mode/decl_proof_instr.mli2
-rw-r--r--plugins/decl_mode/g_decl_mode.ml493
-rw-r--r--plugins/decl_mode/ppdecl_proof.ml173
-rw-r--r--plugins/decl_mode/ppdecl_proof.mli14
11 files changed, 339 insertions, 229 deletions
diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli
index 7467604a60..29ecb94ca8 100644
--- a/plugins/decl_mode/decl_expr.mli
+++ b/plugins/decl_mode/decl_expr.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -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
@@ -99,4 +99,4 @@ type proof_instr =
(Term.constr statement,
Term.constr,
proof_pattern,
- Tacexpr.glob_tactic_expr) gen_proof_instr
+ Geninterp.Val.t) gen_proof_instr
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 1c56586cea..f68c01b18b 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Names
open Constrexpr
@@ -90,13 +90,13 @@ let rec add_vars_of_simple_pattern globs = function
(* Loc.raise loc
(UserError ("simple_pattern",str "\"as\" is not allowed here"))*)
| CPatOr (loc, _)->
- Loc.raise loc
- (UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here"))
+ Loc.raise ~loc
+ (UserError (Some "simple_pattern",str "\"(_ | _)\" is not allowed here"))
| CPatDelimiters (_,_,p) ->
add_vars_of_simple_pattern globs p
| CPatCstr (_,_,pl1,pl2) ->
List.fold_left add_vars_of_simple_pattern
- (List.fold_left add_vars_of_simple_pattern globs pl1) pl2
+ (Option.fold_left (List.fold_left add_vars_of_simple_pattern) globs pl1) pl2
| CPatNotation(_,_,(pl,pll),pl') ->
List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pl'::pll))
| CPatAtom (_,Some (Libnames.Ident (_,id))) -> add_var id globs
@@ -153,8 +153,8 @@ let interp_constr check_sort env sigma c =
fst (understand env sigma (fst c))
let special_whd env =
- let infos=Closure.create_clos_infos Closure.betadeltaiota env in
- (fun t -> Closure.whd_val infos (Closure.inject t))
+ let infos=CClosure.create_clos_infos CClosure.all env in
+ (fun t -> CClosure.whd_val infos (CClosure.inject t))
let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq))
@@ -328,7 +328,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
let _ =
let expected = mib.Declarations.mind_nparams - num_params in
if not (Int.equal (List.length params) expected) then
- errorlabstrm "suppose it is"
+ user_err ~hdr:"suppose it is"
(str "Wrong number of extra arguments: " ++
(if Int.equal expected 0 then str "none" else int expected) ++ spc () ++
str "expected.") in
@@ -348,7 +348,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
Thesis (Plain) -> Glob_term.GSort(Loc.ghost,GProp)
| Thesis (For rec_occ) ->
if not (Id.List.mem rec_occ pat_vars) then
- errorlabstrm "suppose it is"
+ user_err ~hdr:"suppose it is"
(str "Variable " ++ Nameops.pr_id rec_occ ++
str " does not occur in pattern.");
Glob_term.GSort(Loc.ghost,GProp)
@@ -384,7 +384,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
let interp_cut interp_it env sigma cut=
let nenv,nstat = interp_it env sigma cut.cut_stat in
- {cut with
+ { cut_using=Option.map (Tacinterp.Value.of_closure (Tacinterp.default_ist ())) cut.cut_using;
cut_stat=nstat;
cut_by=interp_justification_items nenv sigma cut.cut_by}
@@ -403,7 +403,7 @@ let interp_suffices_clause env sigma (hyps,cot)=
match hyp with
(Hprop st | Hvar st) ->
match st.st_label with
- Name id -> Environ.push_named (id,None,st.st_it) env0
+ Name id -> Environ.push_named (Context.Named.Declaration.LocalAssum (id,st.st_it)) env0
| _ -> env in
let nenv = List.fold_right push_one locvars env in
nenv,res
diff --git a/plugins/decl_mode/decl_interp.mli b/plugins/decl_mode/decl_interp.mli
index b3d6f82bd9..4303ecdb42 100644
--- a/plugins/decl_mode/decl_interp.mli
+++ b/plugins/decl_mode/decl_interp.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index d169dc1372..92d4089015 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -9,7 +9,7 @@
open Names
open Term
open Evd
-open Errors
+open CErrors
open Util
let daimon_flag = ref false
@@ -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
+ | decl :: _ -> Context.Named.Declaration.get_id decl
| [] -> 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 2864ba18ee..dfeee833cb 100644
--- a/plugins/decl_mode/decl_mode.mli
+++ b/plugins/decl_mode/decl_mode.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -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_mode_plugin.mllib b/plugins/decl_mode/decl_mode_plugin.mlpack
index 39342dbd1c..1b84a0790f 100644
--- a/plugins/decl_mode/decl_mode_plugin.mllib
+++ b/plugins/decl_mode/decl_mode_plugin.mlpack
@@ -3,4 +3,3 @@ Decl_interp
Decl_proof_instr
Ppdecl_proof
G_decl_mode
-Decl_mode_plugin_mod
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 9d25681dcf..e19dc86c45 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Pp
open Evd
@@ -29,9 +29,30 @@ open Termops
open Namegen
open Goptions
open Misctypes
+open Sigma.Notations
+open Context.Named.Declaration
+
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
(* Strictness option *)
+let clear ids { it = goal; sigma } =
+ let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in
+ let env = Goal.V82.env sigma goal in
+ let sign = Goal.V82.hyps sigma goal in
+ let cl = Goal.V82.concl sigma goal in
+ let evdref = ref (Evd.clear_metas sigma) in
+ let (hyps, concl) =
+ try Evarutil.clear_hyps_in_evi env evdref sign cl ids
+ with Evarutil.ClearDependencyError (id, _) ->
+ user_err (str "Cannot clear " ++ pr_id id)
+ in
+ let sigma = !evdref in
+ let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in
+ let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
+ { it = [gl]; sigma }
+
let get_its_info gls = get_info gls.sigma gls.it
let get_strictness,set_strictness =
@@ -42,7 +63,7 @@ let _ =
declare_bool_option
{ optsync = true;
optdepr = false;
- optname = "strict mode";
+ optname = "strict proofs";
optkey = ["Strict";"Proofs"];
optread = get_strictness;
optwrite = set_strictness }
@@ -66,12 +87,12 @@ let tcl_erase_info gls =
tcl_change_info_gen info_gen gls
let special_whd gl=
- let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in
- (fun t -> Closure.whd_val infos (Closure.inject t))
+ let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in
+ (fun t -> CClosure.whd_val infos (CClosure.inject t))
let special_nf gl=
- let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in
- (fun t -> Closure.norm_val infos (Closure.inject t))
+ let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in
+ (fun t -> CClosure.norm_val infos (CClosure.inject t))
let is_good_inductive env ind =
let mib,oib = Inductive.lookup_mind_specif env ind in
@@ -86,7 +107,7 @@ Please \"suppose\" something or \"end\" it now."
| _ -> ()
let mk_evd metalist gls =
- let evd0= create_goal_evar_defs (sig_sig gls) in
+ let evd0= clear_metas (sig_sig gls) in
let add_one (meta,typ) evd =
meta_declare meta typ evd in
List.fold_right add_one metalist evd0
@@ -125,25 +146,50 @@ let go_to_proof_mode () =
(* closing gaps *)
+(* spiwack: should use [Proofview.give_up] but that would require
+ moving the whole declarative mode into the new proof engine. It
+ will eventually have to be done.
+
+ As far as I can tell, [daimon_tac] is used after a [thus thesis],
+ it will leave uninstantiated variables instead of giving a relevant
+ message at [Qed]. *)
let daimon_tac gls =
set_daimon_flag ();
{it=[];sigma=sig_sig gls;}
+let daimon_instr env p =
+ let (p,(status,_)) =
+ Proof.run_tactic env begin
+ Proofview.tclINDEPENDENT Proofview.give_up
+ end p
+ in
+ p,status
+
+let do_daimon () =
+ let env = Global.env () in
+ let status =
+ Proof_global.with_current_proof begin fun _ p ->
+ daimon_instr env p
+ end
+ in
+ if not status then Feedback.feedback Feedback.AddedAxiom else ()
+
(* 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 ()
(* return *)
let close_tactic_mode () =
- try goto_current_focus ()
+ try do_daimon ();goto_current_focus ()
with Not_found ->
error "\"return\" cannot be used outside of Declarative Proof Mode."
@@ -164,7 +210,7 @@ let close_block bt pts =
in
match bt,stack with
B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] ->
- (goto_current_focus ())
+ do_daimon ();goto_current_focus ()
| _, Claim::_ ->
error "\"end claim\" expected."
| _, Focus_claim::_ ->
@@ -187,7 +233,7 @@ let close_previous_case pts =
Proof.is_done pts
then
match get_top_stack pts with
- Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occured ...")
+ Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occurred ...")
| Suppose_case :: Per (et,_,_,_) :: _ ->
goto_current_focus ()
| _ -> error "Not inside a proof per cases or induction."
@@ -195,7 +241,7 @@ let close_previous_case pts =
match get_stack pts with
Per (et,_,_,_) :: _ -> ()
| Suppose_case :: Per (et,_,_,_) :: _ ->
- goto_current_focus ()
+ do_daimon ();goto_current_focus ()
| _ -> error "Not inside a proof per cases or induction."
(* Proof instructions *)
@@ -203,7 +249,8 @@ let close_previous_case pts =
(* automation *)
let filter_hyps f gls =
- let filter_aux (id,_,_) =
+ let filter_aux id =
+ let id = NamedDecl.get_id id in
if f id then
tclIDTAC
else
@@ -233,12 +280,16 @@ let prepare_goal items gls =
filter_hyps (let keep = !tokeep in fun id -> Id.Set.mem id keep)] gls
let my_automation_tac = ref
- (Proofview.tclZERO (Errors.make_anomaly (Pp.str"No automation registered")))
+ (Proofview.tclZERO (CErrors.make_anomaly (Pp.str"No automation registered")))
let register_automation_tac tac = my_automation_tac:= tac
let automation_tac = Proofview.tclBIND (Proofview.tclUNIT ()) (fun () -> !my_automation_tac)
+let warn_insufficient_justification =
+ CWarnings.create ~name:"declmode-insufficient-justification" ~category:"declmode"
+ (fun () -> strbrk "Insufficient justification.")
+
let justification tac gls=
tclORELSE
(tclSOLVE [tclTHEN tac (Proofview.V82.of_tactic assumption)])
@@ -247,7 +298,7 @@ let justification tac gls=
error "Insufficient justification."
else
begin
- msg_warning (str "Insufficient justification.");
+ warn_insufficient_justification ();
daimon_tac gls
end) gls
@@ -305,11 +356,11 @@ let enstack_subsubgoals env se stack gls=
let rc,_ = Reduction.dest_prod env apptype in
let rec meta_aux last lenv = function
[] -> (last,lenv,[])
- | (nam,_,typ)::q ->
+ | decl::q ->
let nlast=succ last in
let (llast,holes,metas) =
meta_aux nlast (mkMeta nlast :: lenv) q in
- (llast,holes,(nlast,special_nf gls (substl lenv typ))::metas) in
+ (llast,holes,(nlast,special_nf gls (substl lenv (RelDecl.get_type decl)))::metas) in
let (nlast,holes,nmetas) =
meta_aux se.se_last_meta [] (List.rev rc) in
let refiner = applist (appterm,List.rev holes) in
@@ -366,7 +417,7 @@ let find_subsubgoal c ctyp skip submetas gls =
se.se_meta submetas se.se_meta_list}
else
dfs (pred n)
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
begin
enstack_subsubgoals env se stack gls;
dfs n
@@ -378,15 +429,15 @@ let concl_refiner metas body gls =
let concl = pf_concl gls in
let evd = sig_sig gls in
let env = pf_env gls in
- let sort = family_of_sort (Typing.sort_of env (ref evd) concl) in
+ let sort = family_of_sort (Typing.e_sort_of env (ref evd) concl) in
let rec aux env avoid subst = function
[] -> anomaly ~label:"concl_refiner" (Pp.str "cannot happen")
| (n,typ)::rest ->
let _A = subst_meta subst typ in
let x = id_of_name_using_hdchar env _A Anonymous in
let _x = fresh_id avoid x gls in
- let nenv = Environ.push_named (_x,None,_A) env in
- let asort = family_of_sort (Typing.sort_of nenv (ref evd) _A) in
+ let nenv = Environ.push_named (LocalAssum (_x,_A)) env in
+ let asort = family_of_sort (Typing.e_sort_of nenv (ref evd) _A) in
let nsubst = (n,mkVar _x)::subst in
if List.is_empty rest then
asort,_A,mkNamedLambda _x _A (subst_meta nsubst body)
@@ -440,7 +491,7 @@ let thus_tac c ctyp submetas gls =
Proofview.V82.of_tactic (exact_check proof) gls
else
let refiner = concl_refiner list proof gls in
- Tactics.refine refiner gls
+ Tacmach.refine refiner gls
(* general forward step *)
@@ -467,7 +518,7 @@ let just_tac _then cut info gls0 =
None ->
Proofview.V82.of_tactic automation_tac gls
| Some tac ->
- Proofview.V82.of_tactic (Tacinterp.eval_tactic tac) gls in
+ Proofview.V82.of_tactic (Tacinterp.tactic_of_value (Tacinterp.default_ist ()) tac) gls in
justification (tclTHEN items_tac method_tac) gls0
let instr_cut mkstat _thus _then cut gls0 =
@@ -517,7 +568,7 @@ let instr_rew _thus rew_side cut gls0 =
None ->
Proofview.V82.of_tactic automation_tac gls
| Some tac ->
- Proofview.V82.of_tactic (Tacinterp.eval_tactic tac) gls in
+ Proofview.V82.of_tactic (Tacinterp.tactic_of_value (Tacinterp.default_ist ()) tac) gls in
let just_tac gls =
justification (tclTHEN items_tac method_tac) gls in
let (c_id,_) = match cut.cut_stat.st_label with
@@ -580,7 +631,7 @@ let assume_tac hyps gls =
tclTHEN
(push_intro_tac
(fun id ->
- Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) st.st_label))
+ Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it)))) st.st_label))
hyps tclIDTAC gls
let assume_hyps_or_theses hyps gls =
@@ -590,7 +641,7 @@ let assume_hyps_or_theses hyps gls =
tclTHEN
(push_intro_tac
(fun id ->
- Proofview.V82.of_tactic (convert_hyp (id,None,c))) nam)
+ Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,c)))) nam)
| Hprop {st_label=nam;st_it=Thesis (tk)} ->
tclTHEN
(push_intro_tac
@@ -602,7 +653,7 @@ let assume_st hyps gls =
(fun st ->
tclTHEN
(push_intro_tac
- (fun id -> Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) st.st_label))
+ (fun id -> Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it)))) st.st_label))
hyps tclIDTAC gls
let assume_st_letin hyps gls =
@@ -611,7 +662,7 @@ let assume_st_letin hyps gls =
tclTHEN
(push_intro_tac
(fun id ->
- Proofview.V82.of_tactic (convert_hyp (id,Some (fst st.st_it),snd st.st_it))) st.st_label))
+ Proofview.V82.of_tactic (convert_hyp (LocalDef (id, fst st.st_it, snd st.st_it)))) st.st_label))
hyps tclIDTAC gls
(* suffices *)
@@ -705,7 +756,7 @@ let rec consider_match may_intro introduced available expected gls =
error "Not enough sub-hypotheses to match statements."
(* should tell which ones *)
| id::rest_ids,(Hvar st | Hprop st)::rest ->
- tclIFTHENELSE (Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it)))
+ tclIFTHENELSE (Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it))))
begin
match st.st_label with
Anonymous ->
@@ -748,7 +799,7 @@ let rec take_tac wits gls =
match wits with
[] -> tclIDTAC gls
| wit::rest ->
- let typ = pf_type_of gls wit in
+ let typ = pf_unsafe_type_of gls wit in
tclTHEN (thus_tac wit typ []) (take_tac rest) gls
@@ -772,9 +823,8 @@ let define_tac id args body gls =
let cast_tac id_or_thesis typ gls =
match id_or_thesis with
- This id ->
- let (_,body,_) = pf_get_hyp gls id in
- Proofview.V82.of_tactic (convert_hyp (id,body,typ)) gls
+ | This id ->
+ Proofview.V82.of_tactic (id |> pf_get_hyp gls |> NamedDecl.set_id id |> NamedDecl.set_type typ |> convert_hyp) gls
| Thesis (For _ ) ->
error "\"thesis for ...\" is not applicable here."
| Thesis Plain ->
@@ -829,7 +879,7 @@ let start_tree env ind rp =
let build_per_info etype casee gls =
let concl=pf_concl gls in
let env=pf_env gls in
- let ctyp=pf_type_of gls casee in
+ let ctyp=pf_unsafe_type_of gls casee in
let is_dep = dependent casee concl in
let hd,args = decompose_app (special_whd gls ctyp) in
let (ind,u) =
@@ -844,7 +894,7 @@ let build_per_info etype casee gls =
| _ -> mind.mind_nparams,None in
let params,real_args = List.chop nparams args in
let abstract_obj c body =
- let typ=pf_type_of gls c in
+ let typ=pf_unsafe_type_of gls c in
lambda_create env (typ,subst_term c body) in
let pred= List.fold_right abstract_obj
real_args (lambda_create env (ctyp,subst_term casee concl)) in
@@ -1033,12 +1083,12 @@ let thesis_for obj typ per_info env=
let cind,all_args=decompose_app typ in
let ind,u = destInd cind in
let _ = if not (eq_ind ind per_info.per_ind) then
- errorlabstrm "thesis_for"
+ user_err ~hdr:"thesis_for"
((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++
str"cannot give an induction hypothesis (wrong inductive type).") in
let params,args = List.chop per_info.per_nparams all_args in
let _ = if not (List.for_all2 eq_constr params per_info.per_params) then
- errorlabstrm "thesis_for"
+ user_err ~hdr:"thesis_for"
((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++
str "cannot give an induction hypothesis (wrong parameters).") in
let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in
@@ -1174,6 +1224,9 @@ let hrec_for fix_id per_info gls obj_id =
let hd2 = applist (mkVar fix_id,args@[obj]) in
compose_lam rc (Reductionops.whd_beta gls.sigma hd2)
+let warn_missing_case =
+ CWarnings.create ~name:"declmode-missing-case" ~category:"declmode"
+ (fun () -> strbrk "missing case")
let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
match tree, objs with
@@ -1203,13 +1256,13 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
let nparams = mind.mind_nparams in
let concl=pf_concl gls in
let env=pf_env gls in
- let ctyp=pf_type_of gls casee in
+ let ctyp=pf_unsafe_type_of gls casee in
let hd,all_args = decompose_app (special_whd gls ctyp) in
let ind', u = destInd hd in
let _ = assert (eq_ind ind' ind) in (* just in case *)
let params,real_args = List.chop nparams all_args in
let abstract_obj c body =
- let typ=pf_type_of gls c in
+ let typ=pf_unsafe_type_of gls c in
lambda_create env (typ,subst_term c body) in
let elim_pred = List.fold_right abstract_obj
real_args (lambda_create env (ctyp,subst_term casee concl)) in
@@ -1244,12 +1297,12 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
(fun id ->
hrec_for (out_name fix_name) per_info gls1 id)
recs in
- generalize hrecs gls1
+ Proofview.V82.of_tactic (generalize hrecs) gls1
end;
match bro with
None ->
- msg_warning (str "missing case");
- tacnext (mkMeta 1)
+ warn_missing_case ();
+ tacnext (mkMeta 1)
| Some (sub_ids,tree) ->
let br_args =
List.filter
@@ -1280,7 +1333,11 @@ let understand_my_constr env sigma c concl =
Pretyping.understand_tcc env sigma ~expected_type:(Pretyping.OfType concl) (frob rawc)
let my_refine c gls =
- let oc sigma = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in
+ let oc = { run = begin fun sigma ->
+ let sigma = Sigma.to_evar_map sigma in
+ let (sigma, c) = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in
+ Sigma.Unsafe.of_pair (c, sigma)
+ end } in
Proofview.V82.of_tactic (Tactics.New.refine oc) gls
(* end focus/claim *)
@@ -1316,7 +1373,7 @@ let end_tac et2 gls =
(default_justification (List.map mkVar clauses))
| ET_Induction,EK_nodep ->
tclTHENLIST
- [generalize (pi.per_args@[pi.per_casee]);
+ [Proofview.V82.of_tactic (generalize (pi.per_args@[pi.per_casee]));
Proofview.V82.of_tactic (simple_induct (AnonHyp (succ (List.length pi.per_args))));
default_justification (List.map mkVar clauses)]
| ET_Case_analysis,EK_dep tree ->
@@ -1328,7 +1385,7 @@ let end_tac et2 gls =
(initial_instance_stack clauses) [pi.per_casee] 0 tree
| ET_Induction,EK_dep tree ->
let nargs = (List.length pi.per_args) in
- tclTHEN (generalize (pi.per_args@[pi.per_casee]))
+ tclTHEN (Proofview.V82.of_tactic (generalize (pi.per_args@[pi.per_casee])))
begin
fun gls0 ->
let fix_id =
@@ -1336,7 +1393,7 @@ let end_tac et2 gls =
let c_id =
pf_get_new_id (Id.of_string "_main_arg") gls0 in
tclTHENLIST
- [fix (Some fix_id) (succ nargs);
+ [Proofview.V82.of_tactic (fix (Some fix_id) (succ nargs));
tclDO nargs (Proofview.V82.of_tactic introf);
Proofview.V82.of_tactic (intro_mustbe_force c_id);
execute_cases (Name fix_id) pi
@@ -1444,27 +1501,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/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli
index f86bfea712..325969dadb 100644
--- a/plugins/decl_mode/decl_proof_instr.mli
+++ b/plugins/decl_mode/decl_proof_instr.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 03929b3b86..18a35c6cfb 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,7 +8,8 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
-open Util
+DECLARE PLUGIN "decl_mode_plugin"
+
open Compat
open Pp
open Decl_expr
@@ -18,39 +19,35 @@ open Vernacexpr
open Tok (* necessary for camlp4 *)
open Pcoq.Constr
-open Pcoq.Tactic
+open Pltac
+open Ppdecl_proof
let pr_goal gs =
let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in
let env = Goal.V82.env sigma g in
- let preamb,thesis,penv,pc =
- (str " *** Declarative Mode ***" ++ fnl ()++fnl ()),
- (str "thesis := " ++ fnl ()),
- Printer.pr_context_of env sigma,
- Printer.pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g)
- in
- preamb ++
- str" " ++ hv 0 (penv ++ fnl () ++
- str (Printer.emacs_str "") ++
- 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 concl = Goal.V82.concl sigma g in
+ let goal =
+ Printer.pr_context_of env sigma ++ cut () ++
+ str "============================" ++ cut () ++
+ str "thesis :=" ++ cut () ++
+ Printer.pr_goal_concl_style_env env sigma concl in
+ str " *** Declarative Mode ***" ++ fnl () ++ fnl () ++
+ str " " ++ v 0 goal
-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
@@ -61,27 +58,22 @@ let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }=
let vernac_decl_proof () =
let pf = Proof_global.give_me_the_proof () in
if Proof.is_done pf then
- Errors.error "Nothing left to prove here."
+ CErrors.error "Nothing left to prove here."
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,8 +84,8 @@ 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 =
- Genarg.make0 None "proof_instr"
+let wit_proof_instr : (raw_proof_instr, glob_proof_instr, proof_instr) Genarg.genarg_type =
+ Genarg.make0 "proof_instr"
(* We create a new parser entry [proof_mode]. The Declarative proof mode
will replace the normal parser entry for tactics with this one. *)
@@ -101,19 +93,21 @@ let proof_mode : vernac_expr Gram.entry =
Gram.entry_create "vernac:proof_command"
(* Auxiliary grammar entry. *)
let proof_instr : raw_proof_instr Gram.entry =
- Pcoq.create_generic_entry "proof_instr" (Genarg.rawwit wit_proof_instr)
+ Pcoq.create_generic_entry Pcoq.utactic "proof_instr" (Genarg.rawwit wit_proof_instr)
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
+ | _ -> Vernac_classifier.classify_as_proofstep
(* 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
@@ -139,18 +133,19 @@ let _ =
set = begin fun () ->
(* We set the command non terminal to
[proof_mode] (which we just defined). *)
- G_vernac.set_command_entry proof_mode ;
+ Pcoq.set_command_entry proof_mode ;
(* 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 *)
reset = begin fun () ->
(* We restore the command non terminal to
[noedit_mode]. *)
- G_vernac.set_command_entry G_vernac.noedit_mode ;
+ Pcoq.set_command_entry Pcoq.Vernac_.noedit_mode ;
(* We restore the goal printer to default *)
Printer.set_printer_pr Printer.default_printer_pr
end
@@ -160,7 +155,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 27308666d2..59a0bb5a2d 100644
--- a/plugins/decl_mode/ppdecl_proof.ml
+++ b/plugins/decl_mode/ppdecl_proof.ml
@@ -1,52 +1,46 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Pp
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 fd6fb66376..678fc07688 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.25.1) at 2026-04-29 20:01:51 +0000