aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/g_vernac.mlg19
-rw-r--r--vernac/ppvernac.ml16
-rw-r--r--vernac/pvernac.ml2
-rw-r--r--vernac/pvernac.mli4
-rw-r--r--vernac/record.ml15
-rw-r--r--vernac/record.mli2
-rw-r--r--vernac/topfmt.ml4
-rw-r--r--vernac/topfmt.mli2
-rw-r--r--vernac/vernacentries.ml7
-rw-r--r--vernac/vernacentries.mli2
-rw-r--r--vernac/vernacexpr.ml22
-rw-r--r--vernac/vernacprop.ml35
12 files changed, 67 insertions, 63 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 3f491d1dd4..59d2a66259 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -77,11 +77,11 @@ let parse_compat_version = let open Flags in function
GRAMMAR EXTEND Gram
GLOBAL: vernac_control gallina_ext noedit_mode subprf;
vernac_control: FIRST
- [ [ IDENT "Time"; c = located_vernac -> { VernacTime (false,c) }
- | IDENT "Redirect"; s = ne_string; c = located_vernac -> { VernacRedirect (s, c) }
- | IDENT "Timeout"; n = natural; v = located_vernac -> { VernacTimeout(n,v) }
- | IDENT "Fail"; v = located_vernac -> { VernacFail v }
- | v = decorated_vernac -> { let (f, v) = v in VernacExpr(f, v) } ]
+ [ [ IDENT "Time"; c = vernac_control -> { CAst.make ~loc @@ VernacTime (false,c) }
+ | IDENT "Redirect"; s = ne_string; c = vernac_control -> { CAst.make ~loc @@ VernacRedirect (s, c) }
+ | IDENT "Timeout"; n = natural; v = vernac_control -> { CAst.make ~loc @@ VernacTimeout(n,v) }
+ | IDENT "Fail"; v = vernac_control -> { CAst.make ~loc @@ VernacFail v }
+ | v = decorated_vernac -> { let (f, v) = v in CAst.make ~loc @@ VernacExpr(f, v) } ]
]
;
decorated_vernac:
@@ -147,9 +147,6 @@ GRAMMAR EXTEND Gram
] ]
;
- located_vernac:
- [ [ v = vernac_control -> { CAst.make ~loc v } ] ]
- ;
END
{
@@ -450,8 +447,10 @@ GRAMMAR EXTEND Gram
*)
(* ... with coercions *)
record_field:
- [ [ bd = record_binder; pri = OPT [ "|"; n = natural -> { n } ];
- ntn = decl_notation -> { (bd,pri),ntn } ] ]
+ [ [ bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ];
+ rf_notation = decl_notation -> {
+ let rf_subclass, rf_decl = bd in
+ rf_decl, { rf_subclass ; rf_priority ; rf_notation } } ] ]
;
record_fields:
[ [ f = record_field; ";"; fs = record_fields -> { f :: fs }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 4e4d431e89..889dbafabd 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -446,15 +446,15 @@ open Pputils
| Some true -> str" :>"
| Some false -> str" :>>"
- let pr_record_field ((x, pri), ntn) =
+ let pr_record_field (x, { rf_subclass = oc ; rf_priority = pri ; rf_notation = ntn }) =
let env = Global.env () in
let sigma = Evd.from_env env in
let prx = match x with
- | (oc,AssumExpr (id,t)) ->
+ | AssumExpr (id,t) ->
hov 1 (pr_lname id ++
pr_oc oc ++ spc() ++
pr_lconstr_expr env sigma t)
- | (oc,DefExpr(id,b,opt)) -> (match opt with
+ | DefExpr(id,b,opt) -> (match opt with
| Some t ->
hov 1 (pr_lname id ++
pr_oc oc ++ spc() ++
@@ -1262,15 +1262,15 @@ let pr_vernac_attributes =
let rec pr_vernac_control v =
let return = tag_vernac v in
- match v with
+ match v.v with
| VernacExpr (f, v') -> pr_vernac_attributes f ++ pr_vernac_expr v' ++ sep_end v'
- | VernacTime (_,{v}) ->
+ | VernacTime (_,v) ->
return (keyword "Time" ++ spc() ++ pr_vernac_control v)
- | VernacRedirect (s, {v}) ->
+ | VernacRedirect (s, v) ->
return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v)
- | VernacTimeout(n,{v}) ->
+ | VernacTimeout(n,v) ->
return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_control v)
- | VernacFail {v} ->
+ | VernacFail v->
return (keyword "Fail" ++ spc() ++ pr_vernac_control v)
let pr_vernac v =
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index d474ef8637..4d9157089c 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -52,7 +52,7 @@ module Vernac_ =
let () =
let open Extend in
- let act_vernac v loc = Some CAst.(make ~loc v) in
+ let act_vernac v loc = Some v in
let act_eoi _ loc = None in
let rule = [
Rule (Next (Stop, Atoken Tok.PEOI), act_eoi);
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index 4bf7c9f7bd..41a2e7fd6f 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -26,7 +26,7 @@ module Vernac_ :
val rec_definition : (fixpoint_expr * decl_notation list) Entry.t
val noedit_mode : vernac_expr Entry.t
val command_entry : vernac_expr Entry.t
- val main_entry : vernac_control CAst.t option Entry.t
+ val main_entry : vernac_control option Entry.t
val red_expr : raw_red_expr Entry.t
val hint_info : Hints.hint_info_expr Entry.t
end
@@ -40,7 +40,7 @@ module Unsafe : sig
end
(** The main entry: reads an optional vernac command *)
-val main_entry : proof_mode option -> vernac_control CAst.t option Entry.t
+val main_entry : proof_mode option -> vernac_control option Entry.t
(** Grammar entry for tactics: proof mode(s).
By default Coq's grammar has an empty entry (non-terminal) for
diff --git a/vernac/record.ml b/vernac/record.ml
index 74e5a03659..f489707eb3 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -634,7 +634,7 @@ let declare_existing_class g =
open Vernacexpr
let check_unique_names records =
- let extract_name acc (((_, bnd), _), _) = match bnd with
+ let extract_name acc (rf_decl, _) = match rf_decl with
Vernacexpr.AssumExpr({CAst.v=Name id},_) -> id::acc
| Vernacexpr.DefExpr ({CAst.v=Name id},_,_) -> id::acc
| _ -> acc in
@@ -649,15 +649,15 @@ let check_unique_names records =
let check_priorities kind records =
let isnot_class = match kind with Class false -> false | _ -> true in
let has_priority (_, _, _, cfs, _, _) =
- List.exists (fun ((_, pri), _) -> not (Option.is_empty pri)) cfs
+ List.exists (fun (_, { rf_priority }) -> not (Option.is_empty rf_priority)) cfs
in
if isnot_class && List.exists has_priority records then
user_err Pp.(str "Priorities only allowed for type class substructures")
let extract_record_data records =
let map (is_coe, id, _, cfs, idbuild, s) =
- let fs = List.map (fun (((_, f), _), _) -> f) cfs in
- id.CAst.v, s, List.map snd cfs, fs
+ let fs = List.map fst cfs in
+ id.CAst.v, s, List.map (fun (_, { rf_notation }) -> rf_notation) cfs, fs
in
let data = List.map map records in
let pss = List.map (fun (_, _, ps, _, _, _) -> ps) records in
@@ -691,16 +691,15 @@ let definition_structure udecl kind ~template cum poly finite records =
| [r], [d] -> r, d
| _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled")
in
- let priorities = List.map (fun ((_, id), _) -> {hint_priority = id; hint_pattern = None}) cfs in
- let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in
+ let priorities = List.map (fun (_, { rf_priority }) -> {hint_priority = rf_priority ; hint_pattern = None}) cfs in
+ let coers = List.map (fun (_, { rf_subclass }) -> rf_subclass) cfs in
declare_class def cum ubinders univs id.CAst.v idbuild
implpars params arity template implfs fields coers priorities
| _ ->
let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in
let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in
let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
- let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in
- let coe = List.map (fun coe -> not (Option.is_empty coe)) coers in
+ let coe = List.map (fun (_, { rf_subclass }) -> not (Option.is_empty rf_subclass)) cfs in
id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe
in
let data = List.map2 map data records in
diff --git a/vernac/record.mli b/vernac/record.mli
index 12a2a765b5..d6e63901cd 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -33,7 +33,7 @@ val definition_structure :
(coercion_flag *
Names.lident *
local_binder_expr list *
- (local_decl_expr with_instance with_priority with_notation) list *
+ (local_decl_expr * record_field_attr) list *
Id.t * constr_expr option) list ->
GlobRef.t list
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 7bc3264968..118c126970 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -425,7 +425,7 @@ let with_output_to_file fname func input =
(* For coqtop -time, we display the position in the file,
and a glimpse of the executed command *)
-let pr_cmd_header {CAst.loc;v=com} =
+let pr_cmd_header com =
let shorten s =
if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s
in
@@ -435,7 +435,7 @@ let pr_cmd_header {CAst.loc;v=com} =
| x -> x
) s
in
- let (start,stop) = Option.cata Loc.unloc (0,0) loc in
+ let (start,stop) = Option.cata Loc.unloc (0,0) com.CAst.loc in
let safe_pr_vernac x =
try Ppvernac.pr_vernac x
with e -> str (Printexc.to_string e) in
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index a1e289cd5a..3d522a9e0f 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -73,4 +73,4 @@ val print_err_exn : exn -> unit
redirected to a file [file] *)
val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
-val pr_cmd_header : Vernacexpr.vernac_control CAst.t -> Pp.t
+val pr_cmd_header : Vernacexpr.vernac_control -> Pp.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index fa170e4104..388f6957cf 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -684,7 +684,7 @@ let vernac_record ~template udecl cum k poly finite records =
let () =
if Dumpglob.dump () then
let () = Dumpglob.dump_definition id false "rec" in
- let iter (((_, x), _), _) = match x with
+ let iter (x, _) = match x with
| Vernacexpr.AssumExpr ({loc;v=Name id}, _) ->
Dumpglob.dump_definition (make ?loc id) false "proj"
| _ -> ()
@@ -743,7 +743,8 @@ let vernac_inductive ~atts cum lo finite indl =
let (id, bl, c, l) = Option.get is_defclass in
let (coe, (lid, ce)) = l in
let coe' = if coe then Some true else None in
- let f = (((coe', AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce)), None), []) in
+ let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce),
+ { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] } in
vernac_record ~template udecl cum (Class true) poly finite [id, bl, c, None, [f]]
else if List.for_all is_record indl then
(* Mutual record case *)
@@ -2599,7 +2600,7 @@ and vernac_load ?proof ~verbosely ~st fname =
CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.");
pstate
-and interp_control ?proof ~st = function
+and interp_control ?proof ~st v = match v with
| { v=VernacExpr (atts, cmd) } ->
interp_expr ?proof ~atts ~st cmd
| { v=VernacFail v } ->
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 71cc29b6e1..12451370c8 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -23,7 +23,7 @@ val vernac_require :
val interp :
?verbosely:bool ->
?proof:Proof_global.closed_proof ->
- st:Vernacstate.t -> Vernacexpr.vernac_control CAst.t -> Vernacstate.t
+ st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t
(** Prepare a "match" template for a given inductive type.
For each branch of the match, we list the constructor name
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index d0dae1aa53..34a9b9394a 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -143,13 +143,16 @@ type decl_notation = lstring * constr_expr * scope_name option
type simple_binder = lident list * constr_expr
type class_binder = lident * constr_expr list
type 'a with_coercion = coercion_flag * 'a
-type 'a with_instance = instance_flag * 'a
-type 'a with_notation = 'a * decl_notation list
-type 'a with_priority = 'a * int option
+(* Attributes of a record field declaration *)
+type record_field_attr = {
+ rf_subclass: instance_flag; (* the projection is an implicit coercion or an instance *)
+ rf_priority: int option; (* priority of the instance, if relevant *)
+ rf_notation: decl_notation list;
+ }
type constructor_expr = (lident * constr_expr) with_coercion
type constructor_list_or_record_decl_expr =
| Constructors of constructor_expr list
- | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list
+ | RecordDecl of lident option * (local_decl_expr * record_field_attr) list
type inductive_expr =
ident_decl with_coercion * local_binder_expr list * constr_expr option * inductive_kind *
constructor_list_or_record_decl_expr
@@ -398,11 +401,12 @@ type nonrec vernac_expr =
(* For extension *)
| VernacExtend of extend_name * Genarg.raw_generic_argument list
-type vernac_control =
+type vernac_control_r =
| VernacExpr of Attributes.vernac_flags * 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 CAst.t
- | VernacRedirect of string * vernac_control CAst.t
- | VernacTimeout of int * vernac_control CAst.t
- | VernacFail of vernac_control CAst.t
+ | VernacTime of bool * vernac_control
+ | VernacRedirect of string * vernac_control
+ | VernacTimeout of int * vernac_control
+ | VernacFail of vernac_control
+and vernac_control = vernac_control_r CAst.t
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 704c5b2170..b3490c7dc6 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -13,19 +13,20 @@
open Vernacexpr
-let rec under_control = function
+let rec under_control v = v |> CAst.with_val (function
| VernacExpr (_, c) -> c
- | VernacRedirect (_,{CAst.v=c})
- | VernacTime (_,{CAst.v=c})
- | VernacFail {CAst.v=c}
- | VernacTimeout (_,{CAst.v=c}) -> under_control c
+ | VernacRedirect (_,c)
+ | VernacTime (_,c)
+ | VernacFail c
+ | VernacTimeout (_,c) -> under_control c
+ )
-let rec has_Fail = function
+let rec has_Fail v = v |> CAst.with_val (function
| VernacExpr _ -> false
- | VernacRedirect (_,{CAst.v=c})
- | VernacTime (_,{CAst.v=c})
- | VernacTimeout (_,{CAst.v=c}) -> has_Fail c
- | VernacFail _ -> true
+ | 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 is_navigation_vernac_expr = function
@@ -38,17 +39,17 @@ let is_navigation_vernac_expr = function
let is_navigation_vernac c =
is_navigation_vernac_expr (under_control c)
-let rec is_deep_navigation_vernac = function
- | VernacTime (_,{CAst.v=c}) -> is_deep_navigation_vernac c
- | VernacRedirect (_, {CAst.v=c})
- | VernacTimeout (_,{CAst.v=c}) | VernacFail {CAst.v=c} -> is_navigation_vernac c
- | VernacExpr _ -> false
+let rec is_deep_navigation_vernac v = v |> CAst.with_val (function
+ | VernacTime (_,c) -> is_deep_navigation_vernac c
+ | VernacRedirect (_, c)
+ | VernacTimeout (_, c) | VernacFail c -> is_navigation_vernac c
+ | VernacExpr _ -> false)
(* NB: Reset is now allowed again as asked by A. Chlipala *)
-let is_reset = function
+let is_reset = CAst.with_val (function
| VernacExpr ( _, VernacResetInitial)
| VernacExpr (_, VernacResetName _) -> true
- | _ -> false
+ | _ -> false)
let is_debug cmd = match under_control cmd with
| VernacSetOption (_, ["Ltac";"Debug"], _) -> true
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 00:16:27 +0000