diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/metasyntax.ml | 4 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 49 | ||||
| -rw-r--r-- | vernac/vernacentries.mli | 4 | ||||
| -rw-r--r-- | vernac/vernacprop.ml | 39 | ||||
| -rw-r--r-- | vernac/vernacprop.mli | 19 |
5 files changed, 67 insertions, 48 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 6c3dfec7d..1bb9e0da1 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -80,8 +80,8 @@ let pr_grammar = function | "pattern" -> pr_entry Pcoq.Constr.pattern | "vernac" -> - str "Entry vernac is" ++ fnl () ++ - pr_entry Pcoq.Vernac_.vernac ++ + str "Entry vernac_control is" ++ fnl () ++ + pr_entry Pcoq.Vernac_.vernac_control ++ str "Entry command is" ++ fnl () ++ pr_entry Pcoq.Vernac_.command ++ str "Entry syntax is" ++ fnl () ++ diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index a581043ac..aa6121c39 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1380,11 +1380,13 @@ let _ = optread = (fun () -> !Flags.program_mode); optwrite = (fun b -> Flags.program_mode:=b) } +let universe_polymorphism_option_name = ["Universe"; "Polymorphism"] + let _ = declare_bool_option { optdepr = false; optname = "universe polymorphism"; - optkey = ["Universe"; "Polymorphism"]; + optkey = universe_polymorphism_option_name; optread = Flags.is_universe_polymorphism; optwrite = Flags.make_universe_polymorphism } @@ -1933,19 +1935,11 @@ let vernac_load interp fname = * loc is the Loc.t of the vernacular command being interpreted. *) let interp ?proof ~atts ~st c = let open Vernacinterp in - vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac c); + vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c); match c with - (* The below vernac are candidates for removal from the main type - and to be put into a new doc_command datatype: *) | VernacLoad _ -> assert false - (* Done later in this file *) - | VernacFail _ -> assert false - | VernacTime _ -> assert false - | VernacRedirect _ -> assert false - | VernacTimeout _ -> assert false - (* The STM should handle that, but LOAD bypasses the STM... *) | VernacAbortAll -> CErrors.user_err (str "AbortAll cannot be used through the Load command") | VernacRestart -> CErrors.user_err (str "Restart cannot be used through the Load command") @@ -2209,7 +2203,20 @@ let with_fail st b f = let interp ?(verbosely=true) ?proof ~st (loc,c) = let orig_program_mode = Flags.is_program_mode () in - let rec aux ?polymorphism ~atts isprogcmd = function + let rec control = function + | VernacExpr v -> + let atts = { loc; locality = None; polymorphic = false; } in + aux ~atts orig_program_mode v + | VernacFail v -> with_fail st true (fun () -> control v) + | VernacTimeout (n,v) -> + current_timeout := Some n; + control v + | VernacRedirect (s, (_,v)) -> + Topfmt.with_output_to_file s control v + | VernacTime (_,v) -> + System.with_time !Flags.time control v; + + and aux ?polymorphism ~atts isprogcmd = function | VernacProgram c when not isprogcmd -> aux ?polymorphism ~atts true c @@ -2229,20 +2236,7 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = | VernacLocal _ -> user_err Pp.(str "Locality specified twice") - | VernacFail v -> - with_fail st true (fun () -> aux ?polymorphism ~atts isprogcmd v) - - | VernacTimeout (n,v) -> - current_timeout := Some n; - aux ?polymorphism ~atts isprogcmd v - - | VernacRedirect (s, (_,v)) -> - Topfmt.with_output_to_file s (aux ?polymorphism ~atts isprogcmd) v - - | VernacTime (_,v) -> - System.with_time !Flags.time (aux ?polymorphism ~atts isprogcmd) v; - - | VernacLoad (_,fname) -> vernac_load (aux ?polymorphism ~atts false) fname + | VernacLoad (_,fname) -> vernac_load control fname | c -> check_vernac_supports_locality c atts.locality; @@ -2272,10 +2266,9 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = ignore (Flags.use_polymorphic_flag ()); iraise e in - let atts = { loc; locality = None; polymorphic = false; } in if verbosely - then Flags.verbosely (aux ~atts orig_program_mode) c - else aux ~atts orig_program_mode c + then Flags.verbosely control c + else control c (* XXX: There is a bug here in case of an exception, see @gares comments on the PR *) diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index a559912a0..e99a62fe6 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -18,7 +18,7 @@ val vernac_require : val interp : ?verbosely:bool -> ?proof:Proof_global.closed_proof -> - st:Vernacstate.t -> Vernacexpr.vernac_expr Loc.located -> Vernacstate.t + st:Vernacstate.t -> Vernacexpr.vernac_control Loc.located -> Vernacstate.t (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name @@ -36,3 +36,5 @@ val command_focus : unit Proof.focus_kind val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr -> Evd.evar_map * Redexpr.red_expr) Hook.t + +val universe_polymorphism_option_name : string list diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index 3cff1f14c..4a01ef2ef 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -11,32 +11,49 @@ open Vernacexpr +let rec under_control = function + | VernacExpr c -> c + | VernacRedirect (_,(_,c)) + | VernacTime (_,c) + | VernacFail c + | VernacTimeout (_,c) -> under_control c + +let rec has_Fail = function + | VernacExpr c -> false + | VernacRedirect (_,(_,c)) + | VernacTime (_,c) + | VernacTimeout (_,c) -> has_Fail c + | VernacFail _ -> true + (* Navigation commands are allowed in a coqtop session but not in a .v file *) -let rec is_navigation_vernac = function +let is_navigation_vernac_expr = function | VernacResetInitial | VernacResetName _ | VernacBacktrack _ | VernacBackTo _ | VernacBack _ -> true - | VernacRedirect (_, (_,c)) - | VernacTime (_,c) -> - is_navigation_vernac c (* Time Back* is harmless *) - | c -> is_deep_navigation_vernac c + | _ -> false -and is_deep_navigation_vernac = function +let is_navigation_vernac c = + is_navigation_vernac_expr (under_control c) + +let rec is_deep_navigation_vernac = function + | VernacTime (_,c) -> is_deep_navigation_vernac c + | VernacRedirect (_, (_,c)) | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c - | _ -> false + | VernacExpr _ -> false (* NB: Reset is now allowed again as asked by A. Chlipala *) let is_reset = function - | VernacResetInitial | VernacResetName _ -> true + | VernacExpr VernacResetInitial + | VernacExpr (VernacResetName _) -> true | _ -> false -let is_debug cmd = match cmd with +let is_debug cmd = match under_control cmd with | VernacSetOption (["Ltac";"Debug"], _) -> true | _ -> false -let is_query cmd = match cmd with +let is_query cmd = match under_control cmd with | VernacChdir None | VernacMemOption _ | VernacPrintOption _ @@ -47,6 +64,6 @@ let is_query cmd = match cmd with | VernacLocate _ -> true | _ -> false -let is_undo cmd = match cmd with +let is_undo cmd = match under_control cmd with | VernacUndo _ | VernacUndoTo _ -> true | _ -> false diff --git a/vernac/vernacprop.mli b/vernac/vernacprop.mli index fbdba6bac..eb7c7055a 100644 --- a/vernac/vernacprop.mli +++ b/vernac/vernacprop.mli @@ -11,9 +11,16 @@ open Vernacexpr -val is_navigation_vernac : vernac_expr -> bool -val is_deep_navigation_vernac : vernac_expr -> bool -val is_reset : vernac_expr -> bool -val is_query : vernac_expr -> bool -val is_debug : vernac_expr -> bool -val is_undo : vernac_expr -> bool +(* Return the vernacular command below control (Time, Timeout, Redirect, Fail). + Beware that Fail can change many properties of the underlying command, since + a success of Fail means the command was backtracked over. *) +val under_control : vernac_control -> vernac_expr + +val has_Fail : vernac_control -> bool + +val is_navigation_vernac : vernac_control -> bool +val is_deep_navigation_vernac : vernac_control -> bool +val is_reset : vernac_control -> bool +val is_query : vernac_control -> bool +val is_debug : vernac_control -> bool +val is_undo : vernac_control -> bool |