aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-11-23 11:38:55 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-20 16:52:43 +0100
commit28d45c2413ad24c758fca5cfb00ec4ba20935f39 (patch)
tree50f60424aac3c9e898bb9f9192416c58f44aa7b6 /stm
parente2d1c676b23a335b4fb8a528c99dfca2b82a1a39 (diff)
Separate vernac controls and regular commands.
Virtually all classifications of vernacular commands (the STM classifier, "filtered commands", "navigation commands", etc.) were broken in presence of control vernaculars like Time, Timeout, Fail. Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac Debug in CoqIDE. This change introduces a type separation between vernacular controls and vernacular commands, together with an "under_control" combinator.
Diffstat (limited to 'stm')
-rw-r--r--stm/proofBlockDelimiter.ml25
-rw-r--r--stm/stm.ml146
-rw-r--r--stm/stm.mli10
-rw-r--r--stm/vernac_classifier.ml74
-rw-r--r--stm/vernac_classifier.mli2
5 files changed, 139 insertions, 118 deletions
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 77642946c..01b5b9a01 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -23,8 +23,8 @@ val crawl :
val unit_val : Stm.DynBlockData.t
val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t
val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet
-val of_vernac_expr_val : Vernacexpr.vernac_expr -> Stm.DynBlockData.t
-val to_vernac_expr_val : Stm.DynBlockData.t -> Vernacexpr.vernac_expr
+val of_vernac_control_val : Vernacexpr.vernac_control -> Stm.DynBlockData.t
+val to_vernac_control_val : Stm.DynBlockData.t -> Vernacexpr.vernac_control
end = struct
@@ -32,7 +32,7 @@ let unit_tag = DynBlockData.create "unit"
let unit_val = DynBlockData.Easy.inj () unit_tag
let of_bullet_val, to_bullet_val = DynBlockData.Easy.make_dyn "bullet"
-let of_vernac_expr_val, to_vernac_expr_val = DynBlockData.Easy.make_dyn "vernac_expr"
+let of_vernac_control_val, to_vernac_control_val = DynBlockData.Easy.make_dyn "vernac_control"
let simple_goal sigma g gs =
let open Evar in
@@ -74,14 +74,16 @@ include Util
(* ****************** - foo - bar - baz *********************************** *)
let static_bullet ({ entry_point; prev_node } as view) =
- match entry_point.ast with
+ assert (not (Vernacprop.has_Fail entry_point.ast));
+ match Vernacprop.under_control entry_point.ast with
| Vernacexpr.VernacBullet b ->
let base = entry_point.indentation in
let last_tac = prev_node entry_point in
crawl view ~init:last_tac (fun prev node ->
if node.indentation < base then `Stop else
if node.indentation > base then `Cont node else
- match node.ast with
+ if Vernacprop.has_Fail node.ast then `Stop
+ else match Vernacprop.under_control node.ast with
| Vernacexpr.VernacBullet b' when b = b' ->
`Found { block_stop = entry_point.id; block_start = prev.id;
dynamic_switch = node.id; carry_on_data = of_bullet_val b }
@@ -94,7 +96,7 @@ let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } =
`ValidBlock {
base_state = id;
goals_to_admit = focused;
- recovery_command = Some (Vernacexpr.VernacBullet (to_bullet_val b))
+ recovery_command = Some (Vernacexpr.VernacExpr(Vernacexpr.VernacBullet (to_bullet_val b)))
}
| `Not -> `Leaks
@@ -104,9 +106,10 @@ let () = register_proof_block_delimiter
(* ******************** { block } ***************************************** *)
let static_curly_brace ({ entry_point; prev_node } as view) =
- assert(entry_point.ast = Vernacexpr.VernacEndSubproof);
+ assert(Vernacprop.under_control entry_point.ast = Vernacexpr.VernacEndSubproof);
crawl view (fun (nesting,prev) node ->
- match node.ast with
+ if Vernacprop.has_Fail node.ast then `Cont (nesting,node)
+ else match Vernacprop.under_control node.ast with
| Vernacexpr.VernacSubproof _ when nesting = 0 ->
`Found { block_stop = entry_point.id; block_start = prev.id;
dynamic_switch = node.id; carry_on_data = unit_val }
@@ -122,7 +125,7 @@ let dynamic_curly_brace doc { dynamic_switch = id } =
`ValidBlock {
base_state = id;
goals_to_admit = focused;
- recovery_command = Some Vernacexpr.VernacEndSubproof
+ recovery_command = Some (Vernacexpr.VernacExpr Vernacexpr.VernacEndSubproof)
}
| `Not -> `Leaks
@@ -164,7 +167,7 @@ let static_indent ({ entry_point; prev_node } as view) =
else
`Found { block_stop = entry_point.id; block_start = node.id;
dynamic_switch = node.id;
- carry_on_data = of_vernac_expr_val entry_point.ast }
+ carry_on_data = of_vernac_control_val entry_point.ast }
) last_tac
let dynamic_indent doc { dynamic_switch = id; carry_on_data = e } =
@@ -176,7 +179,7 @@ let dynamic_indent doc { dynamic_switch = id; carry_on_data = e } =
`ValidBlock {
base_state = id;
goals_to_admit = but_last;
- recovery_command = Some (to_vernac_expr_val e);
+ recovery_command = Some (to_vernac_control_val e);
}
| `Not -> `Leaks
diff --git a/stm/stm.ml b/stm/stm.ml
index 1d46e0833..36fc015ef 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -20,6 +20,7 @@ let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else
open Pp
open CErrors
+open Names
open Feedback
open Vernacexpr
@@ -111,7 +112,7 @@ type aast = {
loc : Loc.t option;
indentation : int;
strlen : int;
- mutable expr : vernac_expr; (* mutable: Proof using hinted by aux file *)
+ mutable expr : vernac_control; (* mutable: Proof using hinted by aux file *)
}
let pr_ast { expr; indentation } = Pp.(int indentation ++ str " " ++ Ppvernac.pr_vernac expr)
@@ -119,14 +120,14 @@ let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.
(* Commands piercing opaque *)
let may_pierce_opaque = function
- | { expr = VernacPrint _ } -> true
- | { expr = VernacExtend (("Extraction",_), _) } -> true
- | { expr = VernacExtend (("SeparateExtraction",_), _) } -> true
- | { expr = VernacExtend (("ExtractionLibrary",_), _) } -> true
- | { expr = VernacExtend (("RecursiveExtractionLibrary",_), _) } -> true
- | { expr = VernacExtend (("ExtractionConstant",_), _) } -> true
- | { expr = VernacExtend (("ExtractionInlinedConstant",_), _) } -> true
- | { expr = VernacExtend (("ExtractionInductive",_), _) } -> true
+ | VernacPrint _
+ | VernacExtend (("Extraction",_), _)
+ | VernacExtend (("SeparateExtraction",_), _)
+ | VernacExtend (("ExtractionLibrary",_), _)
+ | VernacExtend (("RecursiveExtractionLibrary",_), _)
+ | VernacExtend (("ExtractionConstant",_), _)
+ | VernacExtend (("ExtractionInlinedConstant",_), _)
+ | VernacExtend (("ExtractionInductive",_), _) -> true
| _ -> false
let update_global_env () =
@@ -545,12 +546,10 @@ end = struct (* {{{ *)
vcs := rewrite_merge !vcs id ~ours ~theirs:Noop ~at branch
let reachable id = reachable !vcs id
let mk_branch_name { expr = x } = Branch.make
- (let rec aux x = match x with
- | VernacDefinition (_,((_,i),_),_) -> Names.Id.to_string i
- | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Names.Id.to_string i
- | VernacTime (_, e)
- | VernacTimeout (_, e) -> aux e
- | _ -> "branch" in aux x)
+ (match Vernacprop.under_control x with
+ | VernacDefinition (_,((_,i),_),_) -> Id.to_string i
+ | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Id.to_string i
+ | _ -> "branch")
let edit_branch = Branch.make "edit"
let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
let get_info id =
@@ -984,7 +983,7 @@ let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) =
in
(* Some special handling of bullets and { }, to get a nicer display *)
let pred n = max 0 (n-1) in
- let ind, nl, new_beginend = match cmd with
+ let ind, nl, new_beginend = match Vernacprop.under_control cmd with
| VernacSubproof _ -> pred ind, nl, (pred ind)::beginend
| VernacEndSubproof -> List.hd beginend, false, List.tl beginend
| VernacBullet _ -> pred ind, nl, beginend
@@ -1049,25 +1048,26 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t
(* We need to check if a command should be filtered from
* vernac_entries, as it cannot handle it. This should go away in
* future refactorings.
- *)
- let rec is_filtered_command = function
- | VernacResetName _ | VernacResetInitial | VernacBack _
- | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
- | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
- | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> is_filtered_command e
- | _ -> false
+ *)
+ let is_filtered_command = function
+ | VernacResetName _ | VernacResetInitial | VernacBack _
+ | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
+ | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
+ | _ -> false
in
- let aux_interp st cmd =
- if is_filtered_command cmd then
- (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st)
- else match cmd with
- | VernacShow ShowScript -> ShowScript.show_script (); st
- | expr ->
- stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr);
- try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (Loc.tag ?loc expr)
- with e ->
- let e = CErrors.push e in
- Exninfo.iraise Hooks.(call_process_error_once e)
+ let aux_interp st expr =
+ let cmd = Vernacprop.under_control expr in
+ if is_filtered_command cmd then
+ (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st)
+ else
+ match cmd with
+ | VernacShow ShowScript -> ShowScript.show_script (); st (** XX we are ignoring control here *)
+ | _ ->
+ stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr);
+ try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (Loc.tag ?loc expr)
+ with e ->
+ let e = CErrors.push e in
+ Exninfo.iraise Hooks.(call_process_error_once e)
in aux_interp st expr
(****************************** CRUFT *****************************************)
@@ -1083,7 +1083,7 @@ module Backtrack : sig
val branches_of : Stateid.t -> backup
(* Returns the state that the command should backtract to *)
- val undo_vernac_classifier : vernac_expr -> Stateid.t * vernac_when
+ val undo_vernac_classifier : vernac_control -> Stateid.t * vernac_when
end = struct (* {{{ *)
@@ -1131,7 +1131,11 @@ end = struct (* {{{ *)
match VCS.visit id with
| { step = `Fork ((_,_,_,l),_) } -> l, false,0
| { step = `Cmd { cids = l; ctac } } -> l, ctac,0
- | { step = `Alias (_,{ expr = VernacUndo n}) } -> [], false, n
+ | { step = `Alias (_,{ expr }) } when not (Vernacprop.has_Fail expr) ->
+ begin match Vernacprop.under_control expr with
+ | VernacUndo n -> [], false, n
+ | _ -> [],false,0
+ end
| _ -> [],false,0 in
match f acc (id, vcs, ids, tactic, undo) with
| `Stop x -> x
@@ -1149,7 +1153,7 @@ end = struct (* {{{ *)
if VCS.is_interactive () = `No && !async_proofs_cache <> Some Force
then undo_costly_in_batch_mode v;
try
- match v with
+ match Vernacprop.under_control v with
| VernacResetInitial ->
Stateid.initial, VtNow
| VernacResetName (_,name) ->
@@ -1242,7 +1246,7 @@ let _ = CErrors.register_handler (function
type document_node = {
indentation : int;
- ast : Vernacexpr.vernac_expr;
+ ast : Vernacexpr.vernac_control;
id : Stateid.t;
}
@@ -1257,7 +1261,7 @@ type static_block_detection =
type recovery_action = {
base_state : Stateid.t;
goals_to_admit : Goal.goal list;
- recovery_command : Vernacexpr.vernac_expr option;
+ recovery_command : Vernacexpr.vernac_control option;
}
type dynamic_block_error_recovery =
@@ -1494,7 +1498,7 @@ end = struct (* {{{ *)
stm_vernac_interp stop
~proof:(pobject, terminator) st
{ verbose = false; loc; indentation = 0; strlen = 0;
- expr = (VernacEndProof (Proved (Opaque,None))) }) in
+ expr = VernacExpr (VernacEndProof (Proved (Opaque,None))) }) in
ignore(Future.join checked_proof);
end;
(* STATE: Restore the state XXX: handle exn *)
@@ -1642,7 +1646,7 @@ end = struct (* {{{ *)
let st = Vernacstate.freeze_interp_state `No in
ignore(stm_vernac_interp stop ~proof st
{ verbose = false; loc; indentation = 0; strlen = 0;
- expr = (VernacEndProof (Proved (Opaque,None))) });
+ expr = VernacExpr (VernacEndProof (Proved (Opaque,None))) });
`OK proof
end
with e ->
@@ -2107,30 +2111,43 @@ let collect_proof keep cur hd brkind id =
| [] -> no_name
| id :: _ -> Names.Id.to_string id in
let loc = (snd cur).loc in
- let rec is_defined_expr = function
+ let is_defined_expr = function
| VernacEndProof (Proved (Transparent,_)) -> true
- | VernacTime (_, e) -> is_defined_expr e
- | VernacRedirect (_, (_, e)) -> is_defined_expr e
- | VernacTimeout (_, e) -> is_defined_expr e
| _ -> false in
let is_defined = function
- | _, { expr = e } -> is_defined_expr e in
+ | _, { expr = e } -> is_defined_expr (Vernacprop.under_control e)
+ && (not (Vernacprop.has_Fail e)) in
+ let proof_using_ast = function
+ | VernacProof(_,Some _) -> true
+ | _ -> false
+ in
let proof_using_ast = function
- | Some (_, ({ expr = VernacProof(_,Some _) } as v)) -> Some v
+ | Some (_, v) when proof_using_ast (Vernacprop.under_control v.expr)
+ && (not (Vernacprop.has_Fail v.expr)) -> Some v
| _ -> None in
let has_proof_using x = proof_using_ast x <> None in
let proof_no_using = function
- | Some (_, ({ expr = VernacProof(t,None) } as v)) -> t,v
+ | VernacProof(t,None) -> t
+ | _ -> assert false
+ in
+ let proof_no_using = function
+ | Some (_, v) -> proof_no_using (Vernacprop.under_control v.expr), v
| _ -> assert false in
let has_proof_no_using = function
- | Some (_, { expr = VernacProof(_,None) }) -> true
+ | VernacProof(_,None) -> true
+ | _ -> false
+ in
+ let has_proof_no_using = function
+ | Some (_, v) -> has_proof_no_using (Vernacprop.under_control v.expr)
+ && (not (Vernacprop.has_Fail v.expr))
| _ -> false in
let too_complex_to_delegate = function
- | { expr = (VernacDeclareModule _
- | VernacDefineModule _
- | VernacDeclareModuleType _
- | VernacInclude _) } -> true
- | { expr = (VernacRequire _ | VernacImport _) } -> true
+ | VernacDeclareModule _
+ | VernacDefineModule _
+ | VernacDeclareModuleType _
+ | VernacInclude _
+ | VernacRequire _
+ | VernacImport _ -> true
| ast -> may_pierce_opaque ast in
let parent = function Some (p, _) -> p | None -> assert false in
let is_empty = function `Async(_,[],_,_) | `MaybeASync(_,[],_,_) -> true | _ -> false in
@@ -2138,7 +2155,8 @@ let collect_proof keep cur hd brkind id =
let view = VCS.visit id in
match view.step with
| (`Sideff (ReplayCommand x,_) | `Cmd { cast = x })
- when too_complex_to_delegate x -> `Sync(no_name,`Print)
+ when too_complex_to_delegate (Vernacprop.under_control x.expr) ->
+ `Sync(no_name,`Print)
| `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next
| `Sideff (ReplayCommand x,_) -> collect (Some (id,x)) (id::accn) view.next
(* An Alias could jump everywhere... we hope we can ignore it*)
@@ -2158,7 +2176,7 @@ let collect_proof keep cur hd brkind id =
(try
let name, hint = name ids, get_hint_ctx loc in
let t, v = proof_no_using last in
- v.expr <- VernacProof(t, Some hint);
+ v.expr <- VernacExpr(VernacProof(t, Some hint));
`ASync (parent last,accn,name,delegate name)
with Not_found ->
let name = name ids in
@@ -2177,9 +2195,13 @@ let collect_proof keep cur hd brkind id =
| `ASync(_,_,name,_) -> `Sync (name,why) in
let check_policy rc = if async_policy () then rc else make_sync `Policy rc in
+ let is_vernac_exact = function
+ | VernacExactProof _ -> true
+ | _ -> false
+ in
match cur, (VCS.visit id).step, brkind with
- | (parent, { expr = VernacExactProof _ }), `Fork _, _
- | (parent, { expr = VernacTime (_, VernacExactProof _) }), `Fork _, _ ->
+ | (parent, x), `Fork _, _ when is_vernac_exact (Vernacprop.under_control x.expr)
+ && (not (Vernacprop.has_Fail x.expr)) ->
`Sync (no_name,`Immediate)
| _, _, { VCS.kind = `Edit _ } -> check_policy (collect (Some cur) [] id)
| _ ->
@@ -2752,7 +2774,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
if !async_proofs_full then `QueryQueue (ref false)
else if VCS.is_vio_doc () &&
VCS.((get_branch head).kind = `Master) &&
- may_pierce_opaque x
+ may_pierce_opaque (Vernacprop.under_control x.expr)
then `SkipQueue
else `MainQueue in
VCS.commit id (mkTransCmd x [] false queue);
@@ -2814,7 +2836,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
rc
(* Side effect on all branches *)
- | VtUnknown, _ when expr = VernacToplevelControl Drop ->
+ | VtUnknown, _ when Vernacprop.under_control expr = VernacToplevelControl Drop ->
let st = Vernacstate.freeze_interp_state `No in
ignore(stm_vernac_interp (VCS.get_branch_pos head) st x);
`Ok
@@ -2826,7 +2848,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
VCS.commit id (mkTransCmd x l in_proof `MainQueue);
(* We can't replay a Definition since universes may be differently
* inferred. This holds in Coq >= 8.5 *)
- let action = match x.expr with
+ let action = match Vernacprop.under_control x.expr with
| VernacDefinition(_, _, DefineBody _) -> CherryPickEnv
| _ -> ReplayCommand x in
VCS.propagate_sideff ~action;
@@ -2854,7 +2876,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
| VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity
| VernacLocal (_,e) -> opacity_of_produced_term e
| _ -> Doesn'tGuaranteeOpacity in
- VCS.commit id (Fork (x,bname,opacity_of_produced_term x.expr,[]));
+ VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[]));
let proof_mode = default_proof_mode () in
VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1));
Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"];
diff --git a/stm/stm.mli b/stm/stm.mli
index ef95be0e4..587b75642 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -39,7 +39,7 @@ val new_doc : stm_init_options -> doc * Stateid.t
(* [parse_sentence sid pa] Reads a sentence from [pa] with parsing
state [sid] Returns [End_of_input] if the stream ends *)
val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable ->
- Vernacexpr.vernac_expr Loc.located
+ Vernacexpr.vernac_control Loc.located
(* Reminder: A parsable [pa] is constructed using
[Pcoq.Gram.coq_parsable stream], where [stream : char Stream.t]. *)
@@ -53,7 +53,7 @@ exception End_of_input
If [newtip] is provided, then the returned state id is guaranteed
to be [newtip] *)
val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t ->
- bool -> Vernacexpr.vernac_expr Loc.located ->
+ bool -> Vernacexpr.vernac_control Loc.located ->
doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
(* [query at ?report_with cmd] Executes [cmd] at a given state [at],
@@ -111,7 +111,7 @@ val get_current_state : doc:doc -> Stateid.t
val get_ldir : doc:doc -> Names.DirPath.t
(* This returns the node at that position *)
-val get_ast : doc:doc -> Stateid.t -> (Vernacexpr.vernac_expr Loc.located) option
+val get_ast : doc:doc -> Stateid.t -> (Vernacexpr.vernac_control Loc.located) option
(* Filename *)
val set_compilation_hints : string -> unit
@@ -174,7 +174,7 @@ type static_block_declaration = {
type document_node = {
indentation : int;
- ast : Vernacexpr.vernac_expr;
+ ast : Vernacexpr.vernac_control;
id : Stateid.t;
}
@@ -189,7 +189,7 @@ type static_block_detection =
type recovery_action = {
base_state : Stateid.t;
goals_to_admit : Goal.goal list;
- recovery_command : Vernacexpr.vernac_expr option;
+ recovery_command : Vernacexpr.vernac_control option;
}
type dynamic_block_error_recovery =
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index c5ae27a11..1291b7642 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -8,6 +8,7 @@
open Vernacexpr
open CErrors
+open Util
open Pp
let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"]
@@ -47,36 +48,18 @@ let declare_vernac_classifier
=
classifiers := !classifiers @ [s,f]
-let make_polymorphic (a, b as x) =
- match a with
- | VtStartProof (x, _, ids) ->
- VtStartProof (x, Doesn'tGuaranteeOpacity, ids), b
- | _ -> x
-
-let rec classify_vernac e =
- let static_classifier e = match e with
+let classify_vernac e =
+ let rec static_classifier ~poly e = match e with
(* Univ poly compatibility: we run it now, so that we can just
* look at Flags in stm.ml. Would be nicer to have the stm
* look at the entire dag to detect this option. *)
- | VernacSetOption (["Universe"; "Polymorphism"],_)
- | VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow
+ | ( VernacSetOption (l,_) | VernacUnsetOption l)
+ when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name ->
+ VtSideff [], VtNow
(* Nested vernac exprs *)
- | VernacProgram e -> classify_vernac e
- | VernacLocal (_,e) -> classify_vernac e
- | VernacPolymorphic (b, e) ->
- if b || Flags.is_universe_polymorphism () (* Ok or not? *) then
- make_polymorphic (classify_vernac e)
- else classify_vernac e
- | VernacTimeout (_,e) -> classify_vernac e
- | VernacTime (_,e) | VernacRedirect (_, (_,e)) -> classify_vernac e
- | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
- (match classify_vernac e with
- | ( VtQuery _ | VtProofStep _ | VtSideff _
- | VtProofMode _ | VtMeta), _ as x -> x
- | VtQed _, _ ->
- VtProofStep { parallel = `No; proof_block_detection = None },
- VtNow
- | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow)
+ | VernacProgram e -> static_classifier ~poly e
+ | VernacLocal (_,e) -> static_classifier ~poly e
+ | VernacPolymorphic (b, e) -> static_classifier ~poly:b e
(* Qed *)
| VernacAbort _ -> VtQed VtDrop, VtLater
| VernacEndProof Admitted -> VtQed VtKeepAsAxiom, VtLater
@@ -106,17 +89,20 @@ let rec classify_vernac e =
| VernacDefinition ((Decl_kinds.DoDischarge,_),((_,i),_),ProveBody _) ->
VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater
| VernacDefinition (_,((_,i),_),ProveBody _) ->
- VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater
+ let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+ VtStartProof(default_proof_mode (),guarantee,[i]), VtLater
| VernacStartTheoremProof (_,l) ->
let ids =
CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in
- VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
- | VernacGoal _ -> VtStartProof (default_proof_mode (),GuaranteesOpacity,[]), VtLater
+ let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+ VtStartProof (default_proof_mode (),guarantee,ids), VtLater
+ | VernacGoal _ ->
+ let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+ VtStartProof (default_proof_mode (),guarantee,[]), VtLater
| VernacFixpoint (discharge,l) ->
let guarantee =
- match discharge with
- | Decl_kinds.NoDischarge -> GuaranteesOpacity
- | Decl_kinds.DoDischarge -> Doesn'tGuaranteeOpacity
+ if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity
+ else GuaranteesOpacity
in
let ids, open_proof =
List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) ->
@@ -126,9 +112,8 @@ let rec classify_vernac e =
else VtSideff ids, VtLater
| VernacCoFixpoint (discharge,l) ->
let guarantee =
- match discharge with
- | Decl_kinds.NoDischarge -> GuaranteesOpacity
- | Decl_kinds.DoDischarge -> Doesn'tGuaranteeOpacity
+ if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity
+ else GuaranteesOpacity
in
let ids, open_proof =
List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) ->
@@ -207,10 +192,21 @@ let rec classify_vernac e =
try List.assoc s !classifiers l ()
with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
in
- let res = static_classifier e in
- if Flags.is_universe_polymorphism () then
- make_polymorphic res
- else res
+ let rec static_control_classifier ~poly = function
+ | VernacExpr e -> static_classifier ~poly e
+ | VernacTimeout (_,e) -> static_control_classifier ~poly e
+ | VernacTime (_,e) | VernacRedirect (_, (_,e)) ->
+ static_control_classifier ~poly e
+ | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
+ (match static_control_classifier ~poly e with
+ | ( VtQuery _ | VtProofStep _ | VtSideff _
+ | VtProofMode _ | VtMeta), _ as x -> x
+ | VtQed _, _ ->
+ VtProofStep { parallel = `No; proof_block_detection = None },
+ VtNow
+ | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow)
+ in
+ static_control_classifier ~poly:(Flags.is_universe_polymorphism ()) e
let classify_as_query = VtQuery (true,Feedback.default_route), VtLater
let classify_as_sideeff = VtSideff [], VtLater
diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli
index fe42a03a3..c0571c1d6 100644
--- a/stm/vernac_classifier.mli
+++ b/stm/vernac_classifier.mli
@@ -12,7 +12,7 @@ open Genarg
val string_of_vernac_classification : vernac_classification -> string
(** What does a vernacular do *)
-val classify_vernac : vernac_expr -> vernac_classification
+val classify_vernac : vernac_control -> vernac_classification
(** Install a vernacular classifier for VernacExtend *)
val declare_vernac_classifier :