diff options
| -rw-r--r-- | coqpp/coqpp_ast.mli | 1 | ||||
| -rw-r--r-- | coqpp/coqpp_lex.mll | 1 | ||||
| -rw-r--r-- | coqpp/coqpp_main.ml | 13 | ||||
| -rw-r--r-- | coqpp/coqpp_parse.mly | 21 | ||||
| -rw-r--r-- | plugins/cc/ccalgo.mli | 2 | ||||
| -rw-r--r-- | plugins/ltac/extratactics.mlg | 16 | ||||
| -rw-r--r-- | plugins/ltac/g_ltac.mlg | 35 | ||||
| -rw-r--r-- | plugins/ltac/g_obligations.mlg | 16 | ||||
| -rw-r--r-- | plugins/ltac/g_rewrite.mlg | 63 | ||||
| -rw-r--r-- | plugins/ltac/pptactic.ml | 1 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 121 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.mli | 14 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 16 | ||||
| -rw-r--r-- | plugins/ltac/tactic_debug.ml | 5 | ||||
| -rw-r--r-- | plugins/syntax/g_numeral.mlg | 21 | ||||
| -rw-r--r-- | plugins/syntax/g_string.mlg | 20 | ||||
| -rw-r--r-- | vernac/obligations.ml | 10 | ||||
| -rw-r--r-- | vernac/obligations.mli | 15 |
18 files changed, 220 insertions, 171 deletions
diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli index 8e10ec49ce..81109887ba 100644 --- a/coqpp/coqpp_ast.mli +++ b/coqpp/coqpp_ast.mli @@ -103,6 +103,7 @@ type classification = type vernac_rule = { vernac_atts : (string * string) list option; + vernac_state: string option; vernac_toks : ext_token list; vernac_class : code option; vernac_depr : bool; diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll index c38755943a..81ba8ad98c 100644 --- a/coqpp/coqpp_lex.mll +++ b/coqpp/coqpp_lex.mll @@ -130,6 +130,7 @@ rule extend = parse | space { extend lexbuf } | '\"' { string lexbuf } | '\n' { newline lexbuf; extend lexbuf } +| "![" { BANGBRACKET } | "#[" { HASHBRACKET } | '[' { LBRACKET } | ']' { RBRACKET } diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index d33eef135f..90158c3aa3 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -347,9 +347,18 @@ let print_atts_right fmt = function let nota = match atts with [_] -> "" | _ -> "Attributes.Notations." in fprintf fmt "(Attributes.parse %s%a atts)" nota aux atts +let print_body_wrapper fmt r = + match r.vernac_state with + | Some "proof" -> + fprintf fmt "let proof = (%a) ~pstate:st.Vernacstate.proof in { st with Vernacstate.proof }" print_code r.vernac_body + | None -> + fprintf fmt "let () = %a in st" print_code r.vernac_body + | Some x -> + fatal ("unsupported state specifier: " ^ x) + let print_body_fun fmt r = - fprintf fmt "let coqpp_body %a%a ~st = let () = %a in st in " - print_binders r.vernac_toks print_atts_left r.vernac_atts print_code r.vernac_body + fprintf fmt "let coqpp_body %a%a ~st = @[%a@] in " + print_binders r.vernac_toks print_atts_left r.vernac_atts print_body_wrapper r let print_body fmt r = fprintf fmt "@[(%afun %a~atts@ ~st@ -> coqpp_body %a%a ~st)@]" diff --git a/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly index abe52ab46b..43ba990f6a 100644 --- a/coqpp/coqpp_parse.mly +++ b/coqpp/coqpp_parse.mly @@ -65,7 +65,7 @@ let parse_user_entry s sep = %token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN DEPRECATED ARGUMENT %token RAW_PRINTED GLOB_PRINTED %token COMMAND CLASSIFIED PRINTED TYPED INTERPRETED GLOBALIZED SUBSTITUTED BY AS -%token HASHBRACKET LBRACKET RBRACKET PIPE ARROW FUN COMMA EQUAL STAR +%token BANGBRACKET HASHBRACKET LBRACKET RBRACKET PIPE ARROW FUN COMMA EQUAL STAR %token LPAREN RPAREN COLON SEMICOLON %token GLOBAL FIRST LAST BEFORE AFTER LEVEL LEFTA RIGHTA NONA %token EOF @@ -209,13 +209,14 @@ vernac_rules: ; vernac_rule: -| PIPE vernac_attributes_opt LBRACKET ext_tokens RBRACKET rule_deprecation rule_classifier ARROW CODE +| PIPE vernac_attributes_opt vernac_state_opt LBRACKET ext_tokens RBRACKET rule_deprecation rule_classifier ARROW CODE { { vernac_atts = $2; - vernac_toks = $4; - vernac_depr = $6; - vernac_class= $7; - vernac_body = $9; + vernac_state= $3; + vernac_toks = $5; + vernac_depr = $7; + vernac_class= $8; + vernac_body = $10; } } ; @@ -235,6 +236,14 @@ vernac_attribute: | qualid_or_ident { ($1, $1) } ; +vernac_state_opt: +| { None } +| BANGBRACKET vernac_state RBRACKET { Some $2 } +; + +vernac_state: +| qualid_or_ident { $1 } + rule_deprecation: | { false } | DEPRECATED { true } diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 978969bf59..5066c3931d 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -255,5 +255,3 @@ val find_contradiction : UF.t -> (Names.Id.t * (int * int)) list -> (Names.Id.t * (int * int)) *) - - diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 0428f08138..8bcf85b04a 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -813,9 +813,9 @@ END TACTIC EXTEND transparent_abstract | [ "transparent_abstract" tactic3(t) ] -> { Proofview.Goal.enter begin fun gl -> - Abstract.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end } + Abstract.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end; } | [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> { Proofview.Goal.enter begin fun gl -> - Abstract.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end } + Abstract.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end; } END (* ********************************************************************* *) @@ -913,9 +913,9 @@ END the semantics of the LCF-style tactics, hence with the classic tactic mode. *) VERNAC COMMAND EXTEND GrabEvars -| [ "Grab" "Existential" "Variables" ] +| ![ proof ] [ "Grab" "Existential" "Variables" ] => { classify_as_proofstep } - -> { Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p) } + -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p)) pstate } END (* Shelves all the goals under focus. *) @@ -945,9 +945,9 @@ END (* Command to add every unshelved variables to the focus *) VERNAC COMMAND EXTEND Unshelve -| [ "Unshelve" ] +| ![ proof ] [ "Unshelve" ] => { classify_as_proofstep } - -> { Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p) } + -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p)) pstate } END (* Gives up on the goals under focus: the goals are considered solved, @@ -1098,8 +1098,8 @@ END VERNAC COMMAND EXTEND OptimizeProof -| [ "Optimize" "Proof" ] => { classify_as_proofstep } -> - { Proof_global.compact_the_proof () } +| ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } -> + { fun ~pstate -> Option.map Proof_global.compact_the_proof pstate } | [ "Optimize" "Heap" ] => { classify_as_proofstep } -> { Gc.compact () } END diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index a348e2cea4..7eb34158e8 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -374,20 +374,21 @@ let () = declare_int_option { optwrite = fun n -> print_info_trace := n; } -let vernac_solve n info tcom b = +let vernac_solve ~pstate n info tcom b = let open Goal_select in - let status = Proof_global.with_current_proof (fun etac p -> - let with_end_tac = if b then Some etac else None in - let global = match n with SelectAll | SelectList _ -> true | _ -> false in - let info = Option.append info !print_info_trace in - let (p,status) = - Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p - in - (* in case a strict subtree was completed, - go back to the top of the prooftree *) - let p = Proof.maximal_unfocus Vernacentries.command_focus p in - p,status) in - if not status then Feedback.feedback Feedback.AddedAxiom + let pstate, status = Proof_global.with_current_proof (fun etac p -> + let with_end_tac = if b then Some etac else None in + let global = match n with SelectAll | SelectList _ -> true | _ -> false in + let info = Option.append info !print_info_trace in + let (p,status) = + Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p + in + (* in case a strict subtree was completed, + go back to the top of the prooftree *) + let p = Proof.maximal_unfocus Vernacentries.command_focus p in + p,status) pstate in + if not status then Feedback.feedback Feedback.AddedAxiom; + Some pstate let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s @@ -434,12 +435,12 @@ let is_explicit_terminator = function TacSolve _ -> true | _ -> false } VERNAC { tactic_mode } EXTEND VernacSolve -| [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => +| ![ proof ] [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => { classify_as_proofstep } -> { let g = Option.default (Goal_select.get_default_goal_selector ()) g in - vernac_solve g n t def + Vernacentries.vernac_require_open_proof vernac_solve g n t def } -| [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => +| ![ proof ] [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => { let anon_abstracting_tac = is_anonymous_abstract t in let solving_tac = is_explicit_terminator t in @@ -449,7 +450,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve VtLater } -> { let t = rm_abstract t in - vernac_solve Goal_select.SelectAll n t def + Vernacentries.vernac_require_open_proof vernac_solve Goal_select.SelectAll n t def } END diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index a12dee48a8..de3a9c9fa9 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -80,25 +80,25 @@ GRAMMAR EXTEND Gram open Obligations -let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac -let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac +let obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.obligation ~ontop:pstate obl t) tac) +let next_obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.next_obligation ~ontop:pstate obl t) tac) let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater) } VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } -| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> +| ![ proof ] [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> { obligation (num, Some name, Some t) tac } -| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> +| ![ proof ] [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> { obligation (num, Some name, None) tac } -| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> +| ![ proof ] [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> { obligation (num, None, Some t) tac } -| [ "Obligation" integer(num) withtac(tac) ] -> +| ![ proof ] [ "Obligation" integer(num) withtac(tac) ] -> { obligation (num, None, None) tac } -| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> +| ![ proof ] [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> { next_obligation (Some name) tac } -| [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac } +| ![ proof ] [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac } END VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 86a227415a..469551809c 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -180,34 +180,34 @@ TACTIC EXTEND setoid_rewrite END VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> { declare_relation atts a aeq n (Some lemma1) (Some lemma2) None } - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "as" ident(n) ] -> { declare_relation atts a aeq n (Some lemma1) None None } - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> { declare_relation atts a aeq n None None None } END VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> { declare_relation atts a aeq n None (Some lemma2) None } - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts a aeq n None (Some lemma2) (Some lemma3) } END VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts a aeq n (Some lemma1) None (Some lemma3) } - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts a aeq n None None (Some lemma3) } END @@ -234,64 +234,64 @@ GRAMMAR EXTEND Gram END VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) None } - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n (Some lemma1) None None } - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n None None None } END VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n None (Some lemma2) None } - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n None (Some lemma2) (Some lemma3) } END VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n (Some lemma1) None (Some lemma3) } - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n None None (Some lemma3) } END VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> { - add_setoid atts [] a aeq t n; + add_setoid atts [] a aeq t n } - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> { - add_setoid atts binders a aeq t n; + add_setoid atts binders a aeq t n } - | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) ":" ident(n) ] + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ] (* This command may or may not open a goal *) => { VtUnknown, VtNow } -> { - add_morphism_infer atts m n; + add_morphism_infer atts m n } - | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => { VtStartProof(GuaranteesOpacity,[n]), VtLater } -> { - add_morphism atts [] m s n; + add_morphism atts [] m s n } - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => { VtStartProof(GuaranteesOpacity,[n]), VtLater } -> { - add_morphism atts binders m s n; + add_morphism atts binders m s n } END @@ -310,7 +310,12 @@ TACTIC EXTEND setoid_transitivity END VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY -| [ "Print" "Rewrite" "HintDb" preident(s) ] -> - { let sigma, env = Pfedit.get_current_context () in - Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s) } +| ![ proof ] [ "Print" "Rewrite" "HintDb" preident(s) ] -> + { (* This command should not use the proof env, keeping previous + behavior as requested in review. *) + fun ~pstate -> + let sigma, env = Option.cata Pfedit.get_current_context + (let e = Global.env () in Evd.from_env e, e) pstate in + Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s); + pstate } END diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 1bdba699f7..80070a7493 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1307,7 +1307,6 @@ let lift_top f a = Genprint.TopPrinterBasic (fun () -> f a) let register_basic_print0 wit f g h = Genprint.register_print0 wit (lift f) (lift g) (lift_top h) - let pr_glob_constr_pptac env sigma c = pr_glob_constr_env env c diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index b1d5c0252f..06d7d86dc6 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1790,15 +1790,15 @@ let declare_an_instance n s args = let declare_instance a aeq n s = declare_an_instance n s [a;aeq] -let anew_instance atts binders instance fields = +let anew_instance ~pstate atts binders instance fields = let program_mode = atts.program in - new_instance ~program_mode atts.polymorphic + new_instance ~pstate ~program_mode atts.polymorphic binders instance (Some (true, CAst.make @@ CRecord (fields))) ~global:atts.global ~generalize:false ~refine:false Hints.empty_hint_info -let declare_instance_refl atts binders a aeq n lemma = +let declare_instance_refl ~pstate atts binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" - in anew_instance atts binders instance + in anew_instance ~pstate atts binders instance [(qualid_of_ident (Id.of_string "reflexivity"),lemma)] let declare_instance_sym atts binders a aeq n lemma = @@ -1811,47 +1811,44 @@ let declare_instance_trans atts binders a aeq n lemma = in anew_instance atts binders instance [(qualid_of_ident (Id.of_string "transitivity"),lemma)] -let declare_relation atts ?(binders=[]) a aeq n refl symm trans = +let declare_relation ~pstate atts ?(binders=[]) a aeq n refl symm trans = init_setoid (); - let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" - in ignore(anew_instance atts binders instance []); + let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" in + let _, pstate = anew_instance ~pstate atts binders instance [] in match (refl,symm,trans) with - (None, None, None) -> () + (None, None, None) -> pstate | (Some lemma1, None, None) -> - ignore (declare_instance_refl atts binders a aeq n lemma1) + snd @@ declare_instance_refl ~pstate atts binders a aeq n lemma1 | (None, Some lemma2, None) -> - ignore (declare_instance_sym atts binders a aeq n lemma2) + snd @@ declare_instance_sym ~pstate atts binders a aeq n lemma2 | (None, None, Some lemma3) -> - ignore (declare_instance_trans atts binders a aeq n lemma3) + snd @@ declare_instance_trans ~pstate atts binders a aeq n lemma3 | (Some lemma1, Some lemma2, None) -> - ignore (declare_instance_refl atts binders a aeq n lemma1); - ignore (declare_instance_sym atts binders a aeq n lemma2) + let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in + snd @@ declare_instance_sym ~pstate atts binders a aeq n lemma2 | (Some lemma1, None, Some lemma3) -> - let _lemma_refl = declare_instance_refl atts binders a aeq n lemma1 in - let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in - let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" - in ignore( - anew_instance atts binders instance + let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in + let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in + snd @@ anew_instance ~pstate atts binders instance [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1); - (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)]) + (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)] | (None, Some lemma2, Some lemma3) -> - let _lemma_sym = declare_instance_sym atts binders a aeq n lemma2 in - let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in - let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" - in ignore( - anew_instance atts binders instance + let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in + let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in + snd @@ anew_instance ~pstate atts binders instance [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2); - (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)]) + (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)] | (Some lemma1, Some lemma2, Some lemma3) -> - let _lemma_refl = declare_instance_refl atts binders a aeq n lemma1 in - let _lemma_sym = declare_instance_sym atts binders a aeq n lemma2 in - let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in - let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" - in ignore( - anew_instance atts binders instance + let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in + let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in + let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in + snd @@ anew_instance ~pstate atts binders instance [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1); (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2); - (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)]) + (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)] let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) @@ -1947,18 +1944,18 @@ let warn_add_setoid_deprecated = CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () -> Pp.(str "Add Setoid is deprecated, please use Add Parametric Relation.")) -let add_setoid atts binders a aeq t n = +let add_setoid ~pstate atts binders a aeq t n = warn_add_setoid_deprecated ?loc:a.CAst.loc (); init_setoid (); - let _lemma_refl = declare_instance_refl atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in - let _lemma_sym = declare_instance_sym atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in - let _lemma_trans = declare_instance_trans atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in + let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in + let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in + let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" - in ignore( - anew_instance atts binders instance + in + snd @@ anew_instance ~pstate atts binders instance [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); - (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]) + (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])] let make_tactic name = @@ -1970,7 +1967,7 @@ let warn_add_morphism_deprecated = CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () -> Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id")) -let add_morphism_infer atts m n = +let add_morphism_infer ~pstate atts m n : Proof_global.t option = warn_add_morphism_deprecated ?loc:m.CAst.loc (); init_setoid (); (* NB: atts.program is ignored, program mode automatically set by vernacentries *) @@ -1981,45 +1978,47 @@ let add_morphism_infer atts m n = if Lib.is_modtype () then let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id - (Entries.ParameterEntry - (None,(instance,uctx),None), - Decl_kinds.IsAssumption Decl_kinds.Logical) + (Entries.ParameterEntry + (None,(instance,uctx),None), + Decl_kinds.IsAssumption Decl_kinds.Logical) in - add_instance (Typeclasses.new_instance - (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info atts.global (ConstRef cst)); - declare_projection n instance_id (ConstRef cst) + add_instance (Typeclasses.new_instance + (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info atts.global (ConstRef cst)); + declare_projection n instance_id (ConstRef cst); + pstate else let kind = Decl_kinds.Global, atts.polymorphic, - Decl_kinds.DefinitionBody Decl_kinds.Instance + Decl_kinds.DefinitionBody Decl_kinds.Instance in let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in let hook _ _ _ = function - | Globnames.ConstRef cst -> - add_instance (Typeclasses.new_instance - (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info + | Globnames.ConstRef cst -> + add_instance (Typeclasses.new_instance + (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info atts.global (ConstRef cst)); - declare_projection n instance_id (ConstRef cst) - | _ -> assert false + declare_projection n instance_id (ConstRef cst) + | _ -> assert false in let hook = Lemmas.mk_hook hook in - Flags.silently - (fun () -> - Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance); - ignore (Pfedit.by (Tacinterp.interp tac))) () + Flags.silently + (fun () -> + let pstate = Lemmas.start_proof ~ontop:pstate ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in + Some (fst Pfedit.(by (Tacinterp.interp tac) pstate))) () -let add_morphism atts binders m s n = +let add_morphism ~pstate atts binders m s n = init_setoid (); let instance_id = add_suffix n "_Proper" in let instance = (((CAst.make @@ Name instance_id),None), Explicit, CAst.make @@ CAppExpl ( (None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None), - [cHole; s; m])) + [cHole; s; m])) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - ignore(new_instance ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance - None - ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) + let _, pstate = new_instance ~pstate ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance + None + ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info in + pstate (** Bind to "rewrite" too *) diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 2457b265f0..a200cb5ced 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -81,18 +81,18 @@ val cl_rewrite_clause : val is_applied_rewrite_relation : env -> evar_map -> rel_context -> constr -> types option -val declare_relation : rewrite_attributes -> +val declare_relation : pstate:Proof_global.t option -> rewrite_attributes -> ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> - constr_expr option -> constr_expr option -> constr_expr option -> unit + constr_expr option -> constr_expr option -> constr_expr option -> Proof_global.t option -val add_setoid : +val add_setoid : pstate:Proof_global.t option -> rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr -> - Id.t -> unit + Id.t -> Proof_global.t option -val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> unit +val add_morphism_infer : pstate:Proof_global.t option -> rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t option -val add_morphism : - rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit +val add_morphism : pstate:Proof_global.t option -> + rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> Proof_global.t option val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index eac84f0543..e0fa46bd87 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -544,12 +544,7 @@ let interp_gen kind ist pattern_mode flags env sigma c = let (_, dummy_proofview) = Proofview.init sigma [] in (* Again this is called at times with no open proof! *) - let name, poly = - try - let Proof.{ name; poly } = Proof.data Proof_global.(give_me_the_proof ()) in - name, poly - with | Proof_global.NoCurrentProof -> Id.of_string "tacinterp", false - in + let name, poly = Id.of_string "tacinterp", false in let (trace,_,_,_) = Proofview.apply ~name ~poly env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in let (evd,c) = catch_error trace (understand_ltac flags env sigma vars kind) term @@ -2063,14 +2058,7 @@ let _ = let tac = interp_tactic ist tac in (* XXX: This depends on the global state which is bad; the hooking mechanism should be modified. *) - let name, poly = - try - let (_, poly, _) = Proof_global.get_current_persistence () in - let name = Proof_global.get_current_proof_name () in - name, poly - with | Proof_global.NoCurrentProof -> - Id.of_string "ltac_gen", false - in + let name, poly = Id.of_string "ltac_gen", false in let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in (EConstr.of_constr c, sigma) in diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 52a83a038f..04f3116664 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -370,7 +370,10 @@ let explain_ltac_call_trace last trace loc = strbrk " (with " ++ prlist_with_sep pr_comma (fun (id,c) -> - let sigma, env = Pfedit.get_current_context () in + (* XXX: This hooks into the ExplainErr extension API + so it is tricky to provide the right env for now. *) + let env = Global.env () in + let sigma = Evd.from_env env in Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders_env env sigma c) (List.rev (Id.Map.bindings vars)) ++ str ")" else mt()) diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index 73a2b99434..baa4ae0306 100644 --- a/plugins/syntax/g_numeral.mlg +++ b/plugins/syntax/g_numeral.mlg @@ -35,8 +35,23 @@ ARGUMENT EXTEND numnotoption END VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF - | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + | #[ locality = Attributes.locality; ] ![proof][ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" ident(sc) numnotoption(o) ] -> - { let (sigma, env) = Pfedit.get_current_context () in - vernac_numeral_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } + + { (* It is a bug to use the proof context here, but at the request of + * the reviewers we keep this broken behavior for now. The Global env + * should be used instead, and the `env, sigma` parameteter to the + * numeral notation command removed. + *) + fun ~pstate -> + let sigma, env = match pstate with + | None -> + let env = Global.env () in + let sigma = Evd.from_env env in + sigma, env + | Some pstate -> + Pfedit.get_current_context pstate + in + vernac_numeral_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc) o; + pstate } END diff --git a/plugins/syntax/g_string.mlg b/plugins/syntax/g_string.mlg index 171e0e213d..cc8c13a84b 100644 --- a/plugins/syntax/g_string.mlg +++ b/plugins/syntax/g_string.mlg @@ -19,8 +19,22 @@ open Stdarg } VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF - | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":" + | #[ locality = Attributes.locality; ] ![proof] [ "String" "Notation" reference(ty) reference(f) reference(g) ":" ident(sc) ] -> - { let (sigma, env) = Pfedit.get_current_context () in - vernac_string_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc) } + { (* It is a bug to use the proof context here, but at the request of + * the reviewers we keep this broken behavior for now. The Global env + * should be used instead, and the `env, sigma` parameteter to the + * numeral notation command removed. + *) + fun ~pstate -> + let sigma, env = match pstate with + | None -> + let env = Global.env () in + let sigma = Evd.from_env env in + sigma, env + | Some pstate -> + Pfedit.get_current_context pstate + in + vernac_string_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc); + pstate } END diff --git a/vernac/obligations.ml b/vernac/obligations.ml index dc7d8ec1f0..07194578c1 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -946,7 +946,7 @@ let obligation_hook prg obl num auto ctx' _ _ gr = ignore (auto (Some prg.prg_name) None deps) end -let rec solve_obligation ?ontop prg num tac = +let rec solve_obligation ~ontop prg num tac = let user_num = succ num in let obls, rem = prg.prg_obligations in let obl = obls.(num) in @@ -972,14 +972,14 @@ let rec solve_obligation ?ontop prg num tac = let pstate = Option.cata (fun tac -> Proof_global.set_endline_tactic tac pstate) pstate tac in pstate -and obligation ?ontop (user_num, name, typ) tac = +and obligation ~ontop (user_num, name, typ) tac = let num = pred user_num in let prg = get_prog_err name in let obls, rem = prg.prg_obligations in if num >= 0 && num < Array.length obls then let obl = obls.(num) in match obl.obl_body with - | None -> solve_obligation ?ontop prg num tac + | None -> solve_obligation ~ontop prg num tac | Some r -> error "Obligation already solved" else error (sprintf "Unknown obligation number %i" (succ num)) @@ -1179,7 +1179,7 @@ let admit_obligations n = let prg = get_prog_err n in admit_prog prg -let next_obligation ?ontop n tac = +let next_obligation ~ontop n tac = let prg = match n with | None -> get_any_prog_err () | Some _ -> get_prog_err n @@ -1190,7 +1190,7 @@ let next_obligation ?ontop n tac = | Some i -> i | None -> anomaly (Pp.str "Could not find a solvable obligation.") in - solve_obligation ?ontop prg i tac + solve_obligation ~ontop prg i tac let check_program_libraries () = Coqlib.check_required_library Coqlib.datatypes_module_name; diff --git a/vernac/obligations.mli b/vernac/obligations.mli index eed3906a6a..b1b7b1ec90 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -85,10 +85,17 @@ val add_mutual_definitions : notations -> fixpoint_kind -> unit -val obligation : ?ontop:Proof_global.t -> int * Names.Id.t option * Constrexpr.constr_expr option -> - Genarg.glob_generic_argument option -> Proof_global.t - -val next_obligation : ?ontop:Proof_global.t -> Names.Id.t option -> Genarg.glob_generic_argument option -> Proof_global.t +val obligation + : ontop:Proof_global.t option + -> int * Names.Id.t option * Constrexpr.constr_expr option + -> Genarg.glob_generic_argument option + -> Proof_global.t + +val next_obligation + : ontop:Proof_global.t option + -> Names.Id.t option + -> Genarg.glob_generic_argument option + -> Proof_global.t val solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> progress (* Number of remaining obligations to be solved for this program *) |