aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/vernacexpr.ml30
-rw-r--r--parsing/g_vernac.ml432
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--plugins/funind/glob_term_to_relation.ml4
-rw-r--r--plugins/ssr/ssrvernac.ml44
-rw-r--r--printing/ppvernac.ml53
-rw-r--r--stm/proofBlockDelimiter.ml4
-rw-r--r--stm/stm.ml9
-rw-r--r--stm/vernac_classifier.ml14
-rw-r--r--vernac/vernacentries.ml56
-rw-r--r--vernac/vernacinterp.ml1
-rw-r--r--vernac/vernacinterp.mli1
-rw-r--r--vernac/vernacprop.ml8
13 files changed, 110 insertions, 108 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index bc7b0585d..8bd2da2f1 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -314,7 +314,16 @@ type cumulative_inductive_parsing_flag =
(** {6 The type of vernacular expressions} *)
-type vernac_expr =
+type vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit
+
+type vernac_argument_status = {
+ name : Name.t;
+ recarg_like : bool;
+ notation_scope : string Loc.located option;
+ implicit_status : vernac_implicit_status;
+}
+
+type nonrec vernac_expr =
| VernacLoad of verbose_flag * string
(* Syntax *)
@@ -463,22 +472,13 @@ type vernac_expr =
(* For extension *)
| VernacExtend of extend_name * Genarg.raw_generic_argument list
- (* Flags *)
- | VernacProgram of vernac_expr
- | VernacPolymorphic of bool * vernac_expr
- | VernacLocal of bool * vernac_expr
-
-and vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit
-
-and vernac_argument_status = {
- name : Name.t;
- recarg_like : bool;
- notation_scope : string Loc.located option;
- implicit_status : vernac_implicit_status;
-}
+type nonrec vernac_flag =
+ | VernacProgram
+ | VernacPolymorphic of bool
+ | VernacLocal of bool
type vernac_control =
- | VernacExpr of vernac_expr
+ | VernacExpr of vernac_flag list * vernac_expr
(* boolean is true when the `-time` batch-mode command line flag was set.
the flag is used to print differently in `-time` vs `Time foo` *)
| VernacTime of bool * vernac_control located
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 92e60f465..d498bda34 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -72,36 +72,36 @@ GEXTEND Gram
| IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c)
| IDENT "Timeout"; n = natural; v = vernac_control -> VernacTimeout(n,v)
| IDENT "Fail"; v = vernac_control -> VernacFail v
- | v = vernac -> VernacExpr(v) ]
+ | (f, v) = vernac -> VernacExpr(f, v) ]
]
;
vernac:
- [ [ IDENT "Local"; v = vernac_poly -> VernacLocal (true, v)
- | IDENT "Global"; v = vernac_poly -> VernacLocal (false, v)
+ [ [ IDENT "Local"; (f, v) = vernac_poly -> (VernacLocal true :: f, v)
+ | IDENT "Global"; (f, v) = vernac_poly -> (VernacLocal false :: f, v)
| v = vernac_poly -> v ]
]
;
vernac_poly:
- [ [ IDENT "Polymorphic"; v = vernac_aux -> VernacPolymorphic (true, v)
- | IDENT "Monomorphic"; v = vernac_aux -> VernacPolymorphic (false, v)
+ [ [ IDENT "Polymorphic"; (f, v) = vernac_aux -> (VernacPolymorphic true :: f, v)
+ | IDENT "Monomorphic"; (f, v) = vernac_aux -> (VernacPolymorphic false :: f, v)
| v = vernac_aux -> v ]
]
;
vernac_aux:
(* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
(* "." is still in the stream and discard_to_dot works correctly *)
- [ [ IDENT "Program"; g = gallina; "." -> VernacProgram g
- | IDENT "Program"; g = gallina_ext; "." -> VernacProgram g
- | g = gallina; "." -> g
- | g = gallina_ext; "." -> g
- | c = command; "." -> c
- | c = syntax; "." -> c
- | c = subprf -> c
+ [ [ IDENT "Program"; g = gallina; "." -> ([VernacProgram], g)
+ | IDENT "Program"; g = gallina_ext; "." -> ([VernacProgram], g)
+ | g = gallina; "." -> ([], g)
+ | g = gallina_ext; "." -> ([], g)
+ | c = command; "." -> ([], c)
+ | c = syntax; "." -> ([], c)
+ | c = subprf -> ([], c)
] ]
;
vernac_aux: LAST
- [ [ prfcom = command_entry -> prfcom ] ]
+ [ [ prfcom = command_entry -> ([], prfcom) ] ]
;
noedit_mode:
[ [ c = query_command -> c None] ]
@@ -621,11 +621,9 @@ GEXTEND Gram
VernacCanonical (AN qid)
| IDENT "Canonical"; IDENT "Structure"; ntn = by_notation ->
VernacCanonical (ByNotation ntn)
- | IDENT "Canonical"; IDENT "Structure"; qid = global;
- d = def_body ->
+ | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body ->
let s = coerce_reference_to_id qid in
- VernacLocal(false,
- VernacDefinition ((NoDischarge,CanonicalStructure),((Loc.tag s),None),d))
+ VernacDefinition ((NoDischarge,CanonicalStructure),((Loc.tag s),None),d)
(* Coercions *)
| IDENT "Coercion"; qid = global; d = def_body ->
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 2fd6f53c4..4b828a702 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -154,7 +154,7 @@ VERNAC COMMAND EXTEND Function
| _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in
match
Vernac_classifier.classify_vernac
- (Vernacexpr.(VernacExpr(VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
+ (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
with
| Vernacexpr.VtSideff ids, _ when hard ->
Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index b4e17c5d1..0b929b8ca 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1509,7 +1509,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds)))
+ Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds)))
++ fnl () ++
msg
in
@@ -1524,7 +1524,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds)))
+ Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds)))
++ fnl () ++
CErrors.print reraise
in
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 4f530a0ae..c0479dd24 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -551,9 +551,9 @@ GEXTEND Gram
| IDENT "Canonical"; qid = Constr.global;
d = G_vernac.def_body ->
let s = coerce_reference_to_id qid in
- Vernacexpr.VernacLocal(false,Vernacexpr.VernacDefinition
+ Vernacexpr.VernacDefinition
((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure),
- ((Loc.tag s),None),(d )))
+ ((Loc.tag s),None), d)
]];
END
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 27c46fe4e..96e39e89a 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -535,17 +535,25 @@ open Decl_kinds
| SsFwdClose e -> "("^aux e^")*"
in Pp.str (aux e)
- let rec pr_vernac_expr v =
+ let pr_extend s cl =
+ let pr_arg a =
+ try pr_gen a
+ with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in
+ try
+ let rl = Egramml.get_extend_vernac_rule s in
+ let rec aux rl cl =
+ match rl, cl with
+ | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl
+ | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl
+ | [], [] -> []
+ | _ -> assert false in
+ hov 1 (pr_sequence identity (aux rl cl))
+ with Not_found ->
+ hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")")
+
+ let pr_vernac_expr v =
let return = tag_vernac v in
match v with
- | VernacPolymorphic (poly, v) ->
- let s = if poly then keyword "Polymorphic" else keyword "Monomorphic" in
- return (s ++ spc () ++ pr_vernac_expr v)
- | VernacProgram v ->
- return (keyword "Program" ++ spc() ++ pr_vernac_expr v)
- | VernacLocal (local, v) ->
- return (pr_locality local ++ spc() ++ pr_vernac_expr v)
-
| VernacLoad (f,s) ->
return (
keyword "Load"
@@ -1203,26 +1211,21 @@ open Decl_kinds
| VernacEndSubproof ->
return (str "}")
- and pr_extend s cl =
- let pr_arg a =
- try pr_gen a
- with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in
- try
- let rl = Egramml.get_extend_vernac_rule s in
- let rec aux rl cl =
- match rl, cl with
- | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl
- | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl
- | [], [] -> []
- | _ -> assert false in
- hov 1 (pr_sequence identity (aux rl cl))
- with Not_found ->
- hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")")
+let pr_vernac_flag =
+ function
+ | VernacPolymorphic true -> keyword "Polymorphic"
+ | VernacPolymorphic false -> keyword "Monomorphic"
+ | VernacProgram -> keyword "Program"
+ | VernacLocal local -> pr_locality local
let rec pr_vernac_control v =
let return = tag_vernac v in
match v with
- | VernacExpr v' -> pr_vernac_expr v' ++ sep_end v'
+ | VernacExpr (f, v') ->
+ List.fold_right
+ (fun f a -> pr_vernac_flag f ++ spc() ++ a)
+ f
+ (pr_vernac_expr v' ++ sep_end v')
| VernacTime (_,(_,v)) ->
return (keyword "Time" ++ spc() ++ pr_vernac_control v)
| VernacRedirect (s, (_,v)) ->
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 01b5b9a01..bebc4d5d5 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -96,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.VernacExpr(Vernacexpr.VernacBullet (to_bullet_val b)))
+ recovery_command = Some (Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b)))
}
| `Not -> `Leaks
@@ -125,7 +125,7 @@ let dynamic_curly_brace doc { dynamic_switch = id } =
`ValidBlock {
base_state = id;
goals_to_admit = focused;
- recovery_command = Some (Vernacexpr.VernacExpr Vernacexpr.VernacEndSubproof)
+ recovery_command = Some (Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof))
}
| `Not -> `Leaks
diff --git a/stm/stm.ml b/stm/stm.ml
index 7045df0ed..5f4fe6565 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1498,7 +1498,7 @@ end = struct (* {{{ *)
stm_vernac_interp stop
~proof:(pobject, terminator) st
{ verbose = false; loc; indentation = 0; strlen = 0;
- expr = VernacExpr (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 *)
@@ -1646,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 = VernacExpr (VernacEndProof (Proved (Opaque,None))) });
+ expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) });
`OK proof
end
with e ->
@@ -2177,7 +2177,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 <- VernacExpr(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
@@ -2872,10 +2872,9 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
if not in_proof && Proof_global.there_are_pending_proofs () then
begin
let bname = VCS.mk_branch_name x in
- let rec opacity_of_produced_term = function
+ let opacity_of_produced_term = function
(* This AST is ambiguous, hence we check it dynamically *)
| VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity
- | VernacLocal (_,e) -> opacity_of_produced_term e
| _ -> Doesn'tGuaranteeOpacity in
VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[]));
let proof_mode = default_proof_mode () in
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 2fa47ba43..99b56d484 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -49,17 +49,13 @@ let declare_vernac_classifier
classifiers := !classifiers @ [s,f]
let classify_vernac e =
- let rec static_classifier ~poly e = match e with
+ let 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 (l,_) | VernacUnsetOption l)
when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name ->
VtSideff [], VtNow
- (* Nested vernac exprs *)
- | 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
@@ -193,7 +189,13 @@ let classify_vernac e =
with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
in
let rec static_control_classifier ~poly = function
- | VernacExpr e -> static_classifier ~poly e
+ | VernacExpr (f, e) ->
+ let poly = List.fold_left (fun poly f ->
+ match f with
+ | VernacPolymorphic b -> b
+ | (VernacProgram | VernacLocal _) -> poly
+ ) poly f in
+ static_classifier ~poly e
| VernacTimeout (_,e) -> static_control_classifier ~poly e
| VernacTime (_,(_,e)) | VernacRedirect (_, (_,e)) ->
static_control_classifier ~poly e
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index bccde169f..3358951f4 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1958,11 +1958,6 @@ let interp ?proof ~atts ~st c =
(* This one is possible to handle here *)
| VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command")
- (* Handled elsewhere *)
- | VernacProgram _
- | VernacPolymorphic _
- | VernacLocal _ -> assert false
-
(* Syntax *)
| VernacSyntaxExtension (infix, sl) ->
vernac_syntax_extension atts infix sl
@@ -2199,10 +2194,30 @@ let with_fail st b f =
let interp ?(verbosely=true) ?proof ~st (loc,c) =
let orig_univ_poly = Flags.is_universe_polymorphism () in
let orig_program_mode = Flags.is_program_mode () in
+ let flags f atts =
+ List.fold_left
+ (fun (polymorphism, atts) f ->
+ match f with
+ | VernacProgram when not atts.program ->
+ (polymorphism, { atts with program = true })
+ | VernacProgram ->
+ user_err Pp.(str "Program mode specified twice")
+ | VernacPolymorphic b when polymorphism = None ->
+ (Some b, atts)
+ | VernacPolymorphic _ ->
+ user_err Pp.(str "Polymorphism specified twice")
+ | VernacLocal b when Option.is_empty atts.locality ->
+ (polymorphism, { atts with locality = Some b })
+ | VernacLocal _ ->
+ user_err Pp.(str "Locality specified twice")
+ )
+ (None, atts)
+ f
+ in
let rec control = function
- | VernacExpr v ->
- let atts = { loc; locality = None; polymorphic = false; } in
- aux ~atts orig_program_mode v
+ | VernacExpr (f, v) ->
+ let (polymorphism, atts) = flags f { loc; locality = None; polymorphic = false; program = orig_program_mode; } in
+ aux ~polymorphism ~atts v
| VernacFail v -> with_fail st true (fun () -> control v)
| VernacTimeout (n,v) ->
current_timeout := Some n;
@@ -2212,25 +2227,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
| VernacTime (batch, (_loc,v)) ->
System.with_time ~batch control v;
- and aux ?polymorphism ~atts isprogcmd = function
-
- | VernacProgram c when not isprogcmd ->
- aux ?polymorphism ~atts true c
-
- | VernacProgram _ ->
- user_err Pp.(str "Program mode specified twice")
-
- | VernacPolymorphic (b, c) when polymorphism = None ->
- aux ~polymorphism:b ~atts:atts isprogcmd c
-
- | VernacPolymorphic (b, c) ->
- user_err Pp.(str "Polymorphism specified twice")
-
- | VernacLocal (b, c) when Option.is_empty atts.locality ->
- aux ?polymorphism ~atts:{atts with locality = Some b} isprogcmd c
-
- | VernacLocal _ ->
- user_err Pp.(str "Locality specified twice")
+ and aux ~polymorphism ~atts : _ -> unit =
+ function
| VernacLoad (_,fname) -> vernac_load control fname
@@ -2239,7 +2237,7 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
check_vernac_supports_polymorphism c polymorphism;
let polymorphic = Option.default (Flags.is_universe_polymorphism ()) polymorphism in
Flags.make_universe_polymorphism polymorphic;
- Obligations.set_program_mode isprogcmd;
+ Obligations.set_program_mode atts.program;
try
vernac_timeout begin fun () ->
let atts = { atts with polymorphic } in
@@ -2248,7 +2246,7 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
else Flags.silently (interp ?proof ~atts ~st) c;
(* If the command is `(Un)Set Program Mode` or `(Un)Set Universe Polymorphism`,
we should not restore the previous state of the flag... *)
- if orig_program_mode || not !Flags.program_mode || isprogcmd then
+ if orig_program_mode || not !Flags.program_mode || atts.program then
Flags.program_mode := orig_program_mode;
if (Flags.is_universe_polymorphism() = polymorphic) then
Flags.make_universe_polymorphism orig_univ_poly;
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index c0b93c163..c40ca27db 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -16,6 +16,7 @@ type atts = {
loc : Loc.t option;
locality : bool option;
polymorphic : bool;
+ program : bool;
}
type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index ab3d4bfc5..c5e610f89 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -14,6 +14,7 @@ type atts = {
loc : Loc.t option;
locality : bool option;
polymorphic : bool;
+ program : bool;
}
type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 4fdc78dd2..3932d1c7b 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -12,14 +12,14 @@
open Vernacexpr
let rec under_control = function
- | VernacExpr c -> c
+ | VernacExpr (_, c) -> c
| VernacRedirect (_,(_,c))
| VernacTime (_,(_,c))
| VernacFail c
| VernacTimeout (_,c) -> under_control c
let rec has_Fail = function
- | VernacExpr c -> false
+ | VernacExpr _ -> false
| VernacRedirect (_,(_,c))
| VernacTime (_,(_,c))
| VernacTimeout (_,c) -> has_Fail c
@@ -45,8 +45,8 @@ let rec is_deep_navigation_vernac = function
(* NB: Reset is now allowed again as asked by A. Chlipala *)
let is_reset = function
- | VernacExpr VernacResetInitial
- | VernacExpr (VernacResetName _) -> true
+ | VernacExpr ( _, VernacResetInitial)
+ | VernacExpr (_, VernacResetName _) -> true
| _ -> false
let is_debug cmd = match under_control cmd with
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 15:54:56 +0000