|
(************************************************************************)
(* * The Rocq Prover / The Rocq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
DECLARE GLOBAL PLUGIN
{
open Pp
open Util
open Names
open Glob_term
open Vernacexpr
open Constrexpr
open Constrexpr_ops
open Extend
open Decls
open Declaremods
module C = Constr
open Procq
open Procq.Prim
open Procq.Constr
open Procq.Module
open Pvernac.Vernac_
open Attributes
(* Rem: do not join the different GEXTEND into one, it breaks native *)
(* compilation on PowerPC and Sun architectures *)
let query_command = Entry.make "query_command"
let search_query = Entry.make "search_query"
let search_queries = Entry.make "search_queries"
let subprf = Entry.make "subprf"
let subprf_with_selector = Entry.make "subprf_with_selector"
let quoted_attributes = Entry.make "quoted_attributes"
let attribute_list = Entry.make "attribute_list"
let coercion_class = Entry.make "coercion_class"
let thm_token = Entry.make "thm_token"
let def_token = Entry.make "def_token"
let assumption_token = Entry.make "assumption_token"
let def_body = Entry.make "def_body"
let notation_declaration = Entry.make "notation_declaration"
let decl_notations = Entry.make "decl_notations"
let record_field = Entry.make "record_field"
let of_type = Entry.make "of_type"
let of_type_inst = Entry.make "of_type_inst"
let section_subset_expr = Entry.make "section_subset_expr"
let scope_delimiter = Entry.make "scope_delimiter"
let syntax_modifiers = Entry.make "syntax_modifiers"
let goal_selector = Entry.make "goal_selector"
let toplevel_selector = Entry.make "toplevel_selector"
let make_bullet s =
let open Proof_bullet in
let n = String.length s in
match s.[0] with
| '-' -> Dash n
| '+' -> Plus n
| '*' -> Star n
| _ -> assert false
(* For now we just keep the top-level location of the whole
vernacular, that is to say, including attributes and control flags;
this is not very convenient for advanced clients tho, so in the
future it'd be cool to actually locate the attributes and control
flags individually too. *)
let add_control_flag ~loc ~flag { CAst.v = cmd } =
CAst.make ~loc { cmd with control = flag :: cmd.control }
let test_hash_ident =
let open Procq.Lookahead in
to_entry "test_hash_ident" begin
lk_kw "#" >> lk_ident >> check_no_space
end
let test_id_colon =
let open Procq.Lookahead in
to_entry "test_id_colon" begin
lk_ident >> lk_kw ":"
end
let warn_chdir_pwd = CWarnings.create ~name:"change-dir-pwd-deprecated" ~category:Deprecation.Version.v8_20
(fun () -> strbrk "Command \"Cd\" as a synonym of \"Pwd\" is deprecated." ++ spc () ++
strbrk "Use \"Pwd\" instead.")
}
GRAMMAR EXTEND Gram
GLOBAL: vernac_control quoted_attributes attribute_list gallina_ext noedit_mode subprf subprf_with_selector qualid;
vernac_control: FIRST
[ [ IDENT "Time"; c = vernac_control ->
{ add_control_flag ~loc ~flag:ControlTime c }
| IDENT "Instructions"; c = vernac_control ->
{ add_control_flag ~loc ~flag:ControlInstructions c }
| IDENT "Profile"; f = OPT STRING; c = vernac_control ->
{ add_control_flag ~loc ~flag:(ControlProfile f) c }
| IDENT "Redirect"; s = ne_string; c = vernac_control ->
{ add_control_flag ~loc ~flag:(ControlRedirect s) c }
| IDENT "Timeout"; n = natural; c = vernac_control ->
{ add_control_flag ~loc ~flag:(ControlTimeout n) c }
| IDENT "Fail"; c = vernac_control ->
{ add_control_flag ~loc ~flag:ControlFail c }
| IDENT "Succeed"; c = vernac_control ->
{ add_control_flag ~loc ~flag:ControlSucceed c }
| v = decorated_vernac ->
{ let (attrs, expr) = v in CAst.make ~loc { control = []; attrs; expr = expr } } ]
]
;
decorated_vernac:
[ [ a = quoted_attributes ; a' = LIST0 legacy_attr; v = vernac_aux ->
{ (List.append a a', v) } ] ]
;
quoted_attributes:
[ [ l = LIST0 [ "#[" ; a = attribute_list ; "]" -> { a } ] -> { List.flatten l } ]
]
;
attribute_list:
[ [ a = LIST1 attribute SEP "," -> { a } ]
]
;
attribute:
[ [ k = ident ; v = attr_value -> { CAst.make ~loc (Names.Id.to_string k, v) }
(* Required because "ident" is declared a keyword when loading Ltac. *)
| IDENT "using" ; v = attr_value -> { CAst.make ~loc ("using", v) } ]
]
;
attr_value:
[ [ "=" ; v = string -> { VernacFlagLeaf (FlagString v) }
| "=" ; v = qualid -> { VernacFlagLeaf (FlagQualid v) }
| "(" ; a = attribute_list ; ")" -> { VernacFlagList a }
| -> { VernacFlagEmpty } ]
]
;
legacy_attr:
[ [ IDENT "Local" ->
{ CAst.make ~loc ("local", VernacFlagEmpty) }
| IDENT "Global" ->
{ CAst.make ~loc ("global", VernacFlagEmpty) }
| IDENT "Polymorphic" ->
{ Attributes.vernac_polymorphic_flag (Some loc) }
| IDENT "Monomorphic" ->
{ Attributes.vernac_monomorphic_flag (Some loc) }
| IDENT "Cumulative" ->
{ CAst.make ~loc ("universes", VernacFlagList [CAst.make ~loc ("cumulative", VernacFlagEmpty)]) }
| IDENT "NonCumulative" ->
{ CAst.make ~loc ("universes", VernacFlagList [CAst.make ~loc ("cumulative", VernacFlagLeaf (FlagQualid (Libnames.qualid_of_string "no")))]) }
| IDENT "Private" ->
{ CAst.make ~loc ("private", VernacFlagList [CAst.make ~loc ("matching", VernacFlagEmpty)]) }
| IDENT "Program" ->
{ CAst.make ~loc ("program", VernacFlagEmpty) }
] ]
;
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 *)
[ [ g = gallina; "." -> { VernacSynPure g }
| g = gallina_ext; "." -> { g }
| c = command; "." -> { c }
| c = syntax; "." -> { c }
] ]
;
vernac_aux: LAST
[ [ prfcom = command_entry -> { prfcom } ] ]
;
noedit_mode: [ [ c = query_command -> { VernacSynPure (c None) } ] ]
;
subprf:
[ [ s = BULLET -> { VernacBullet (make_bullet s) }
| "}" -> { VernacEndSubproof }
] ]
;
subprf_with_selector:
[ [ "{" -> { fun g -> VernacSubproof g }
(* query_command needs to be here to factor with VernacSubproof *)
| c = query_command -> { c }
] ]
;
END
{
let warn_plural_command =
CWarnings.create ~name:"plural-command" ~category:CWarnings.CoreCategories.pedantic ~default:CWarnings.Disabled
(fun kwd -> strbrk (Printf.sprintf "Command \"%s\" expects more than one assumption." kwd))
let test_plural_form loc kwd = function
| [(_,([_],_))] ->
warn_plural_command ~loc kwd
| _ -> ()
let test_plural_form_types loc kwd = function
| [([_],_)] ->
warn_plural_command ~loc kwd
| _ -> ()
let test_plural_form_rules loc kwd = function
| [_] ->
warn_plural_command ~loc kwd
| _ -> ()
let lname_of_lident : lident -> lname =
CAst.map (fun s -> Name s)
let name_of_ident_decl : ident_decl -> name_decl =
on_fst lname_of_lident
let test_variance_ident =
let open Procq.Lookahead in
to_entry "test_variance_ident" begin
lk_kws ["=";"+";"*"] >> lk_ident
end
let test_doublepipe_univ_decl =
let open Procq.Lookahead in
to_entry "test_doublepipe_univ_decl" (lk_ident_list >> lk_kw "|" >> lk_ident_list >> (lk_kw "+" <+> lk_empty) >> (lk_kw "|" <+> lk_kw "|}"))
let test_doublepipe_cumul_univ_decl =
let open Procq.Lookahead in
let lk_list_variance_ident = lk_list (lk_kw "+" <+> lk_kw "*" <+> lk_kw "=" <+> lk_ident) in
to_entry "test_doublepipe_cumul_univ_decl" (lk_ident_list >> lk_kw "|" >> lk_list_variance_ident >> (lk_kw "+" <+> lk_empty) >> (lk_kw "|" <+> lk_kw "|}"))
let test_semicolon_cumul_univ_decl =
let open Procq.Lookahead in
to_entry "test_semicolon_cumul_univ_decl" (lk_ident_list >> lk_kw ";")
}
(* Gallina declarations *)
GRAMMAR EXTEND Gram
GLOBAL: gallina gallina_ext thm_token def_token assumption_token def_body of_type of_type_inst
record_field notation_declaration decl_notations fix_definition ident_decl univ_decl inductive_or_record_definition;
gallina:
(* Definition, Theorem, Variable, Axiom, ... *)
[ [ thm = thm_token; id = ident_decl; bl = binders; ":"; c = lconstr;
l = LIST0
[ "with"; id = ident_decl; bl = binders; ":"; c = lconstr ->
{ (id,(bl,c)) } ] ->
{ VernacStartTheoremProof (thm, (id,(bl,c))::l) }
| stre = assumption_token; nl = inline; bl = assum_list ->
{ VernacAssumption (stre, nl, bl) }
| tk = assumptions_token; nl = inline; bl = assum_list ->
{ let (kwd,stre) = tk in
test_plural_form loc kwd bl;
VernacAssumption (stre, nl, bl) }
| d = def_token; id = ident_decl; b = def_body ->
{ VernacDefinition (d, name_of_ident_decl id, b) }
| IDENT "Symbol"; bl = assum_list ->
{ VernacSymbol bl }
| IDENT "Symbols"; bl = assum_list ->
{ test_plural_form loc "Symbols" bl;
VernacSymbol bl }
| IDENT "Let"; id = ident_decl; b = def_body ->
{ VernacDefinition ((DoDischarge, Let), name_of_ident_decl id, b) }
(* Gallina inductive declarations *)
| f = finite_token; ind = inductive_or_record_definition ->
{ VernacInductive (f, [ind]) }
| f = inductive_token; indl = LIST1 inductive_or_record_definition SEP "with" ->
{ VernacInductive (f, indl) }
| "Fixpoint"; recs = LIST1 fix_definition SEP "with" ->
{ VernacFixpoint (NoDischarge, List.split recs) }
| IDENT "Let"; "Fixpoint"; recs = LIST1 fix_definition SEP "with" ->
{ VernacFixpoint (DoDischarge, List.split recs) }
| "CoFixpoint"; corecs = LIST1 cofix_definition SEP "with" ->
{ VernacCoFixpoint (NoDischarge, corecs) }
| IDENT "Let"; "CoFixpoint"; corecs = LIST1 cofix_definition SEP "with" ->
{ VernacCoFixpoint (DoDischarge, corecs) }
| IDENT "Scheme"; l = LIST1 scheme SEP "with" -> { VernacScheme l }
| IDENT "Scheme"; IDENT "Equality"; IDENT "for" ; id = smart_global ->
{ VernacSchemeEquality (SchemeEquality,id) }
| IDENT "Scheme"; IDENT "Boolean"; IDENT "Equality"; IDENT "for" ; id = smart_global ->
{ VernacSchemeEquality (SchemeBooleanEquality,id) }
| IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
l = LIST1 identref SEP "," -> { VernacCombinedScheme (id, l) }
| IDENT "Register"; g = global; "as"; quid = qualid ->
{ VernacRegister(g, RegisterCoqlib quid) }
| IDENT "Register"; IDENT "Scheme"; g = global; "as"; qid = qualid; IDENT "for"; g' = global ->
{ VernacRegister(g, RegisterScheme {inductive = g'; scheme_kind = qid}) }
| IDENT "Register"; IDENT "Inline"; g = global ->
{ VernacRegister(g, RegisterInline) }
| IDENT "Primitive"; id = ident_decl; typopt = OPT [ ":"; typ = lconstr -> { typ } ]; ":="; r = register_token ->
{ VernacPrimitive(id, r, typopt) }
| IDENT "Universe"; l = LIST1 identref -> { VernacUniverse l }
| IDENT "Universes"; l = LIST1 identref -> { VernacUniverse l }
| IDENT "Sort"; l = LIST1 identref -> { VernacSort l }
| IDENT "Sorts"; l = LIST1 identref -> { VernacSort l }
| IDENT "Constraint"; l = LIST1 univ_constraint SEP "," -> { VernacConstraint l }
| IDENT "Rewrite"; IDENT "Rule"; id = identref; ":="; OPT"|"; rules = LIST1 rewrite_rule SEP "|" ->
{ VernacAddRewRule (id, rules) }
| IDENT "Rewrite"; IDENT "Rules"; id = identref; ":="; OPT"|"; rules = LIST1 rewrite_rule SEP "|" ->
{ test_plural_form_rules loc "Rewrite Rules" rules;
VernacAddRewRule (id, rules) }
] ]
;
register_token:
[ [ test_hash_ident; "#"; r = IDENT -> { CPrimitives.parse_op_or_type ~loc r } ] ]
;
thm_token:
[ [ "Theorem" -> { Theorem }
| IDENT "Lemma" -> { Lemma }
| IDENT "Fact" -> { Fact }
| IDENT "Remark" -> { Remark }
| IDENT "Corollary" -> { Corollary }
| IDENT "Proposition" -> { Proposition }
| IDENT "Property" -> { Property } ] ]
;
def_token:
[ [ "Definition" -> { (NoDischarge,Definition) }
| IDENT "Example" -> { (NoDischarge,Example) }
| IDENT "SubClass" -> { (NoDischarge,SubClass) } ] ]
;
assumption_token:
[ [ "Hypothesis" -> { (DoDischarge, Logical) }
| "Variable" -> { (DoDischarge, Definitional) }
| "Axiom" -> { (NoDischarge, Logical) }
| "Parameter" -> { (NoDischarge, Definitional) }
| IDENT "Conjecture" -> { (NoDischarge, Conjectural) } ] ]
;
assumptions_token:
[ [ IDENT "Hypotheses" -> { ("Hypotheses", (DoDischarge, Logical)) }
| IDENT "Variables" -> { ("Variables", (DoDischarge, Definitional)) }
| IDENT "Axioms" -> { ("Axioms", (NoDischarge, Logical)) }
| IDENT "Parameters" -> { ("Parameters", (NoDischarge, Definitional)) }
| IDENT "Conjectures" -> { ("Conjectures", (NoDischarge, Conjectural)) } ] ]
;
inline:
[ [ IDENT "Inline"; "("; i = natural; ")" -> { InlineAt i }
| IDENT "Inline" -> { DefaultInline }
| -> { NoInline } ] ]
;
univ_constraint:
[ [ l = universe_name; ord = [ "<" -> { Univ.Lt } | "=" -> { Univ.Eq } | "<=" -> { Univ.Le } ];
r = universe_name -> { (l, ord, r) } ] ]
;
univ_decl_constraints:
[ [ "|"; l' = LIST0 univ_constraint SEP ",";
ext = [ "+" -> { true } | -> { false } ]; "}" -> { (l',ext) }
| ext = [ "}" -> { true } | bar_cbrace -> { false } ] -> { ([], ext) } ] ]
;
univ_decl:
[ [ "@{" ; test_doublepipe_univ_decl; l0 = LIST0 identref; pipe_loc = [ "|" -> { loc } ]; l = LIST0 identref; ext = [ "+" -> { true } | -> { false } ];
cs = univ_decl_constraints
->
{ let open UState in
G_constr.warn_old_sort_syntax ~loc:pipe_loc ();
{ univdecl_qualities = l0;
univdecl_extensible_qualities = false;
univdecl_instance = l;
univdecl_extensible_instance = ext;
univdecl_constraints = fst cs;
univdecl_extensible_constraints = snd cs } }
| "@{" ; l0 = LIST0 identref; ";"; l = LIST0 identref; ext = [ "+" -> { true } | -> { false } ];
cs = univ_decl_constraints
->
{ let open UState in
{ univdecl_qualities = l0;
univdecl_extensible_qualities = false;
univdecl_instance = l;
univdecl_extensible_instance = ext;
univdecl_constraints = fst cs;
univdecl_extensible_constraints = snd cs } }
| "@{" ; l = LIST0 identref; ext = [ "+" -> { true } | -> { false } ];
cs = univ_decl_constraints
->
{ let open UState in
{ univdecl_qualities = [];
univdecl_extensible_qualities = false;
univdecl_instance = l;
univdecl_extensible_instance = ext;
univdecl_constraints = fst cs;
univdecl_extensible_constraints = snd cs } }
] ]
;
variance:
[ [ "+" -> { UVars.Variance.Covariant }
| "=" -> { UVars.Variance.Invariant }
| "*" -> { UVars.Variance.Irrelevant }
] ]
;
variance_identref:
[ [ id = identref -> { (id, None) }
| test_variance_ident; v = variance; id = identref -> { (id, Some v) }
(* We need this test to help the parser avoid the conflict
between "+" before ident (covariance) and trailing "+" (extra univs allowed) *)
] ]
;
cumul_univ_decl:
[ [ "@{" ; test_doublepipe_cumul_univ_decl; l0 = LIST0 identref; pipe_loc = [ "|" -> { loc } ];
l = LIST0 variance_identref; ext = [ "+" -> { true } | -> { false } ];
cs = univ_decl_constraints
->
{ let open UState in
G_constr.warn_old_sort_syntax ~loc:pipe_loc ();
{ univdecl_qualities = l0;
univdecl_extensible_qualities = false;
univdecl_instance = l;
univdecl_extensible_instance = ext;
univdecl_constraints = fst cs;
univdecl_extensible_constraints = snd cs } }
| "@{" ; test_semicolon_cumul_univ_decl; l0 = LIST0 identref; ";";
l = LIST0 variance_identref; ext = [ "+" -> { true } | -> { false } ];
cs = univ_decl_constraints
->
{ let open UState in
{ univdecl_qualities = l0;
univdecl_extensible_qualities = false;
univdecl_instance = l;
univdecl_extensible_instance = ext;
univdecl_constraints = fst cs;
univdecl_extensible_constraints = snd cs } }
| "@{" ; l = LIST0 variance_identref; ext = [ "+" -> { true } | -> { false } ];
cs = univ_decl_constraints
->
{ let open UState in
{ univdecl_qualities = [];
univdecl_extensible_qualities = false;
univdecl_instance = l;
univdecl_extensible_instance = ext;
univdecl_constraints = fst cs;
univdecl_extensible_constraints = snd cs } }
] ]
;
ident_decl:
[ [ i = identref; l = OPT univ_decl -> { (i, l) }
] ]
;
cumul_ident_decl:
[ [ i = identref; l = OPT cumul_univ_decl -> { (i, l) }
] ]
;
inductive_token:
[ [ IDENT "Inductive" -> { Inductive_kw }
| IDENT "CoInductive" -> { CoInductive } ] ]
;
finite_token:
[ [ IDENT "Variant" -> { Variant }
| IDENT "Record" -> { Record }
| IDENT "Structure" -> { Structure }
| IDENT "Class" -> { Class true } ] ]
;
(* Simple definitions *)
def_body:
[ [ bl = binders; ":="; red = reduce; c = lconstr ->
{ match c.CAst.v with
| CCast(c, Some C.DEFAULTcast, t) -> DefineBody (bl, red, c, Some t)
| _ -> DefineBody (bl, red, c, None) }
| bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
{ DefineBody (bl, red, c, Some t) }
| bl = binders; ":"; t = lconstr ->
{ ProveBody (bl, t) } ] ]
;
reduce:
[ [ IDENT "Eval"; r = red_expr; "in" -> { Some r }
| -> { None } ] ]
;
notation_declaration:
[ [ ntn = lstring; ":="; c = constr;
modl = syntax_modifiers;
scopt = OPT [ ":"; sc = IDENT -> { sc } ] ->
{ { ntn_decl_string = ntn; ntn_decl_interp = c;
ntn_decl_scope = scopt;
ntn_decl_modifiers = modl;
} } ] ]
;
decl_sep:
[ [ IDENT "and" -> { () } ] ]
;
decl_notations:
[ [ "where"; l = LIST1 notation_declaration SEP decl_sep -> { l }
| -> { [] } ] ]
;
(* Inductives and records *)
opt_constructors_or_fields:
[ [ ":="; lc = constructors_or_record -> { lc }
| ":=" -> { Constructors [] }
| -> { RecordDecl (None, [], None) } ] ]
;
inductive_or_record_definition:
[ [ oc = opt_coercion; id = cumul_ident_decl; indpar = binders;
extrapar = OPT [ "|"; p = binders -> { p } ];
c = OPT [ ":"; c = lconstr -> { c } ];
lc=opt_constructors_or_fields; ntn = decl_notations ->
{ (((oc,id),(indpar,extrapar),c,lc),ntn) } ] ]
;
constructors_or_record:
[ [ "|"; l = LIST1 constructor SEP "|" -> { Constructors l }
| attr = quoted_attributes ; id = identref ; c = constructor_type;
"|"; l = LIST1 constructor SEP "|" ->
{ Constructors ((c attr id)::l) }
| attr = quoted_attributes ; id = identref ; c = constructor_type ->
{ Constructors [ c attr id ] }
| attr = quoted_attributes ;
cstr = identref; "{"; fs = record_fields; "}"; id = default_inhabitant_ident ->
{ let () = unsupported_attributes attr in
RecordDecl (Some cstr,fs,id) }
| "{";fs = record_fields; "}"; id = default_inhabitant_ident -> { RecordDecl (None,fs,id) } ] ]
;
default_inhabitant_ident:
[ [ "as"; id = identref -> { Some id }
| -> { None } ] ]
;
(*
csort:
[ [ s = sort -> CSort (loc,s) ] ]
;
*)
opt_coercion:
[ [ ">" -> { AddCoercion }
| -> { NoCoercion } ] ]
;
(* (co)-fixpoints *)
fix_definition:
[ [ id_decl = ident_decl;
bl = binders_fixannot;
rtype = type_cstr;
body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notations ->
{ let binders, rec_order = bl in
((rec_order : Constrexpr.fixpoint_order_expr option), {fname = fst id_decl; univs = snd id_decl; binders; rtype; body_def; notations})
} ] ]
;
cofix_definition:
[ [ id_decl = ident_decl; binders = binders; rtype = type_cstr;
body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notations ->
{ {fname = fst id_decl; univs = snd id_decl; binders; rtype; body_def; notations}
} ]]
;
(* Rewrite Rules *)
rw_pattern:
[ [ p = lconstr -> { p } ] ];
rewrite_rule:
[ [ u = OPT [ u = univ_decl; "|-" -> { u }];
lhs = rw_pattern; "=>" ; rhs = lconstr ->
{ (u, lhs, rhs)
} ] ]
;
(* Inductive schemes *)
scheme:
[ [ kind = scheme_kind -> { (None,kind) }
| id = identref; ":="; kind = scheme_kind -> { (Some id,kind) } ] ]
;
scheme_kind:
[ [sch_type = scheme_type; "for"; sch_qualid = smart_global; IDENT "Sort"; sch_sort = sort_quality_or_set
-> { {sch_type; sch_qualid; sch_sort} }
] ]
;
scheme_type:
[ [ IDENT "Induction" -> { SchemeInduction }
| IDENT "Minimality" -> { SchemeMinimality }
| IDENT "Elimination" -> { SchemeElimination }
| IDENT "Case" -> { SchemeCase }
] ]
;
(* Various Binders *)
(*
(* ... without coercions *)
binder_nodef:
[ [ b = binder_let ->
(match b with
CLocalAssum(l,ty) -> (l,ty)
| CLocalDef _ ->
user_err ~loc
(Pp.str"defined binder not allowed here.")) ] ]
;
*)
(* ... with coercions *)
record_field:
[ [ rfu_attrs = quoted_attributes ;
bd = record_binder; rfu_priority = OPT [ "|"; n = natural -> { n } ];
rfu_notation = decl_notations -> {
let (rfu_coercion, rfu_instance), rf_decl = bd in
rf_decl,
{ rfu_attrs ; rfu_coercion ; rfu_instance ; rfu_priority ;
rfu_notation } } ] ]
;
record_fields:
[ [ f = record_field; ";"; fs = record_fields -> { f :: fs }
| f = record_field -> { [f] }
| -> { [] }
] ]
;
field_body:
[ [ l = binders; oc = of_type_inst;
t = lconstr -> { fun id -> (oc,AssumExpr (id,l,t)) }
| l = binders; oc = of_type_inst;
t = lconstr; ":="; b = lconstr -> { fun id ->
(oc,DefExpr (id,l,b,Some t)) }
| l = binders; ":="; b = lconstr -> { fun id ->
(* Why are we dropping cast info here? *)
match b.CAst.v with
| CCast(b', _, t) ->
((NoCoercion,NoInstance),DefExpr(id,l,b',Some t))
| _ ->
((NoCoercion,NoInstance),DefExpr(id,l,b,None)) } ] ]
;
record_binder:
[ [ id = name -> { ((NoCoercion,NoInstance),AssumExpr(id, [], CAst.make ~loc @@ CHole (None))) }
| id = name; f = field_body -> { f id } ] ]
;
assum_list:
[ [ bl = LIST1 assum_coe -> { bl } | b = assumpt -> { [b] } ] ]
;
assum_coe:
[ [ "("; a = assumpt; ")" -> { a } ] ]
;
assumpt:
[ [ idl = LIST1 ident_decl; oc = of_type; c = lconstr ->
{ (oc,(idl,c)) } ] ]
;
constructor_type:
[[ l = binders;
t= [ coe = of_type_inst; c = lconstr ->
{ fun l attr id -> ((attr, fst coe, snd coe),(id,mkProdCN ~loc l c)) }
| ->
{ fun l attr id -> ((attr,NoCoercion,NoInstance),(id,mkProdCN ~loc l (CAst.make ~loc @@ CHole (None)))) } ]
-> { t l }
]]
;
constructor:
[ [ attr = quoted_attributes ;
id = identref; c=constructor_type -> { c attr id } ] ]
;
of_type:
[ [ ":>" -> { AddCoercion }
| ":"; ">" -> { AddCoercion }
| ":" -> { NoCoercion } ] ]
;
of_type_inst:
[ [ ":>" -> { (AddCoercion, NoInstance) }
| ":"; ">" -> { (AddCoercion, NoInstance) }
| "::" -> { (NoCoercion, BackInstance) }
| "::>" -> { (AddCoercion, BackInstance) }
| ":" -> { (NoCoercion, NoInstance) } ] ]
;
END
{
let test_only_starredidentrefs =
let open Procq.Lookahead in
to_entry "test_only_starredidentrefs" begin
lk_list (lk_ident <+> lk_kws ["Type"; "*"]) >> (lk_kws [".";")"])
end
let starredidentreflist_to_expr l =
match l with
| [] -> SsEmpty
| x :: xs -> List.fold_right (fun i acc -> SsUnion(i,acc)) xs x
let warn_deprecated_include_type =
CWarnings.create ~name:"deprecated-include-type" ~category:Deprecation.Version.v8_3
(fun () -> strbrk "Include Type is deprecated; use Include instead")
let warn_deprecated_as_ident_kind =
CWarnings.create ~name:"deprecated-as-ident-kind" ~category:Deprecation.Version.v8_14
(fun () -> strbrk "grammar kind \"as ident\" no longer accepts \"_\"; use \"as name\" instead to accept \"_\", too, or silence the warning if you actually intended to accept only identifiers.")
}
(* Modules and Sections *)
GRAMMAR EXTEND Gram
GLOBAL: gallina_ext module_expr module_type section_subset_expr;
gallina_ext:
[ [ (* Interactive module declaration *)
IDENT "Module"; export = export_token; id = identref;
bl = LIST0 module_binder; sign = of_module_type;
body = is_module_expr ->
{ VernacSynterp (VernacDefineModule (export, id, bl, sign, body)) }
| IDENT "Module"; "Type"; id = identref;
bl = LIST0 module_binder; sign = check_module_types;
body = is_module_type ->
{ VernacSynterp (VernacDeclareModuleType (id, bl, sign, body)) }
| IDENT "Declare"; IDENT "Module"; export = export_token; id = identref;
bl = LIST0 module_binder; ":"; mty = module_type_inl ->
{ VernacSynterp (VernacDeclareModule (export, id, bl, mty)) }
(* Section beginning *)
| IDENT "Section"; id = identref -> { VernacSynterp (VernacBeginSection id) }
(* This end a Section a Module or a Module Type *)
| IDENT "End"; id = identref -> { VernacSynterp (VernacEndSegment id) }
(* Naming a set of section hyps *)
| IDENT "Collection"; id = identref; ":="; expr = section_subset_expr ->
{ VernacSynPure (VernacNameSectionHypSet (id, expr)) }
(* Requiring an external file *)
| IDENT "From" ; ns = global ;
IDENT "Extra"; IDENT "Dependency"; f = ne_string ;
id = OPT [ "as"; id = IDENT -> { id } ] ->
{ VernacSynterp (VernacExtraDependency (ns, f, Option.map Id.of_string id)) }
(* Requiring an already compiled module *)
| IDENT "Require"; export = export_token; qidl = LIST1 filtered_import ->
{ VernacSynterp (VernacRequire (None, export, qidl)) }
| IDENT "From" ; ns = global ; IDENT "Require"; export = export_token
; qidl = LIST1 filtered_import ->
{ VernacSynterp (VernacRequire (Some ns, export, qidl)) }
| IDENT "Import"; cats = OPT import_categories; qidl = LIST1 filtered_import ->
{ VernacSynterp (VernacImport ((Import,cats),qidl)) }
| IDENT "Export"; cats = OPT import_categories; qidl = LIST1 filtered_import ->
{ VernacSynterp (VernacImport ((Export,cats),qidl)) }
| IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_type ->
{ VernacSynterp (VernacInclude(e::l)) }
| IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type ->
{ warn_deprecated_include_type ~loc ();
VernacSynterp (VernacInclude(e::l)) } ] ]
;
import_categories:
[ [ negative = OPT "-"; "("; cats = LIST1 qualid SEP ","; ")" ->
{ let cats = List.map (fun cat -> CAst.make ?loc:cat.CAst.loc (Libnames.string_of_qualid cat)) cats in
{ negative=Option.has_some negative; import_cats = cats } }
] ]
;
filtered_import:
[ [ m = global -> { (m, ImportAll) }
| m = global; "("; ns = LIST1 one_import_filter_name SEP ","; ")" -> { (m, ImportNames ns) } ] ]
;
one_import_filter_name:
[ [ n = global; etc = OPT [ "("; ".."; ")" -> { () } ] -> { n, Option.has_some etc } ] ]
;
export_token:
[ [ IDENT "Import"; cats = OPT import_categories -> { Some (Import,cats) }
| IDENT "Export"; cats = OPT import_categories -> { Some (Export,cats) }
| -> { None } ] ]
;
ext_module_type:
[ [ "<+"; mty = module_type_inl -> { mty } ] ]
;
ext_module_expr:
[ [ "<+"; mexpr = module_expr_inl -> { mexpr } ] ]
;
check_module_type:
[ [ "<:"; mty = module_type_inl -> { mty } ] ]
;
check_module_types:
[ [ mtys = LIST0 check_module_type -> { mtys } ] ]
;
of_module_type:
[ [ ":"; mty = module_type_inl -> { Enforce mty }
| mtys = check_module_types -> { Check mtys } ] ]
;
is_module_type:
[ [ ":="; mty = module_type_inl ; l = LIST0 ext_module_type -> { (mty::l) }
| -> { [] } ] ]
;
is_module_expr:
[ [ ":="; mexpr = module_expr_inl; l = LIST0 ext_module_expr -> { (mexpr::l) }
| -> { [] } ] ]
;
functor_app_annot:
[ [ "["; IDENT "inline"; "at"; IDENT "level"; i = natural; "]" ->
{ InlineAt i }
| "["; IDENT "no"; IDENT "inline"; "]" -> { NoInline }
| -> { DefaultInline }
] ]
;
module_expr_inl:
[ [ "!"; me = module_expr -> { (me,NoInline) }
| me = module_expr; a = functor_app_annot -> { (me,a) } ] ]
;
module_type_inl:
[ [ "!"; me = module_type -> { (me,NoInline) }
| me = module_type; a = functor_app_annot -> { (me,a) } ] ]
;
(* Module binder *)
module_binder:
[ [ "("; export = export_token; idl = LIST1 identref; ":";
mty = module_type_inl; ")" -> { (export,idl,mty) } ] ]
;
(* Module expressions *)
module_expr:
[ [ me = module_expr_atom -> { CAst.make ~loc @@ CMident me }
| me1 = module_expr; me2 = module_expr_atom -> { CAst.make ~loc @@ CMapply (me1,me2) }
] ]
;
module_expr_atom:
[ [ qid = qualid -> { qid } | "("; me = module_expr_atom; ")" -> { me } ] ]
;
with_declaration:
[ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr ->
{ CWith_Definition (fqid,udecl,c) }
| IDENT "Module"; fqid = fullyqualid; ":="; qid = qualid ->
{ CWith_Module (fqid,qid) }
] ]
;
module_type:
[ [ qid = qualid -> { CAst.make ~loc @@ CMident qid }
| "("; mt = module_type; ")" -> { mt }
| mty = module_type; me = module_expr_atom ->
{ CAst.make ~loc @@ CMapply (mty,me) }
| mty = module_type; "with"; decl = with_declaration ->
{ CAst.make ~loc @@ CMwith (mty,decl) }
] ]
;
(* Proof using *)
section_subset_expr:
[ [ test_only_starredidentrefs; l = LIST0 starredidentref ->
{ starredidentreflist_to_expr l }
| e = ssexpr -> { e } ]]
;
starredidentref:
[ [ i = identref -> { SsSingl i }
| i = identref; "*" -> { SsFwdClose(SsSingl i) }
| "Type" -> { SsType }
| "Type"; "*" -> { SsFwdClose SsType } ]]
;
ssexpr:
[ "35"
[ "-"; e = ssexpr -> { SsCompl e } ]
| "50"
[ e1 = ssexpr; "-"; e2 = ssexpr-> { SsSubstr(e1,e2) }
| e1 = ssexpr; "+"; e2 = ssexpr-> { SsUnion(e1,e2) } ]
| "0"
[ i = starredidentref -> { i }
| "()" -> { SsEmpty }
| "("; test_only_starredidentrefs; l = LIST0 starredidentref; ")"->
{ starredidentreflist_to_expr l }
| "("; test_only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" ->
{ SsFwdClose(starredidentreflist_to_expr l) }
| "("; e = ssexpr; ")"-> { e }
| "("; e = ssexpr; ")"; "*" -> { SsFwdClose e } ] ]
;
END
(* Extensions: implicits, coercions, etc. *)
GRAMMAR EXTEND Gram
GLOBAL: gallina_ext hint_info scope_delimiter;
gallina_ext: TOP
[ [ (* Transparent and Opaque *)
IDENT "Transparent"; o = OPT [ "!" -> {()} ]; l = LIST1 smart_global ->
{ VernacSynPure (VernacSetOpacity ((Conv_oracle.transparent, l), o <> None)) }
| IDENT "Opaque"; o = OPT [ "!" -> {()} ]; l = LIST1 smart_global ->
{ VernacSynPure (VernacSetOpacity ((Conv_oracle.Opaque, l), o <> None)) }
| IDENT "Strategy"; l =
LIST1 [ v=strategy_level; "["; q=LIST1 smart_global; "]" -> { (v,q) } ] ->
{ VernacSynPure (VernacSetStrategy l) }
(* Canonical structure *)
| IDENT "Canonical"; OPT [ IDENT "Structure" -> {()} ]; qid = global; ud = OPT [ u = OPT univ_decl; d = def_body -> { (u,d) } ] ->
{ match ud with
| None ->
VernacSynPure (VernacCanonical CAst.(make ?loc:qid.CAst.loc @@ AN qid))
| Some (u,d) ->
let s = coerce_reference_to_id qid in
VernacSynPure (VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make ?loc:qid.CAst.loc (Name s)),u),d)) }
| IDENT "Canonical"; OPT [ IDENT "Structure" -> {()} ]; ntn = by_notation ->
{ VernacSynPure (VernacCanonical CAst.(make ~loc @@ ByNotation ntn)) }
(* Coercions *)
| IDENT "Coercion"; qid = global; ud = OPT [ u = OPT univ_decl; d = def_body -> { u, d } ] ->
{ match ud with Some (u, d) -> let s = coerce_reference_to_id qid in
VernacSynPure (VernacDefinition ((NoDischarge,Coercion),((CAst.make ?loc:qid.CAst.loc (Name s)),u),d))
| None -> VernacSynPure (VernacCoercion (CAst.make ~loc @@ AN qid, None)) }
| IDENT "Identity"; IDENT "Coercion"; f = identref; ":";
s = coercion_class; ">->"; t = coercion_class ->
{ VernacSynPure (VernacIdentityCoercion (f, s, t)) }
| IDENT "Coercion"; qid = global; ":"; s = coercion_class; ">->";
t = coercion_class ->
{ VernacSynPure (VernacCoercion (CAst.make ~loc @@ AN qid, Some(s, t))) }
| IDENT "Coercion"; ntn = by_notation; ":"; s = coercion_class; ">->";
t = coercion_class ->
{ VernacSynPure (VernacCoercion (CAst.make ~loc @@ ByNotation ntn, Some (s, t))) }
| IDENT "Context"; c = LIST1 binder ->
{ VernacSynPure (VernacContext (List.flatten c)) }
| IDENT "Instance"; namesup = instance_name; ":";
t = term LEVEL "200";
info = hint_info ;
props = [ ":="; "{"; r = record_declaration; "}" -> { Some (true,r) } |
":="; c = lconstr -> { Some (false,c) } | -> { None } ] ->
{ VernacSynPure (VernacInstance (fst namesup,snd namesup,t,props,info)) }
| IDENT "Existing"; IDENT "Instance"; id = global;
info = hint_info ->
{ VernacSynPure (VernacExistingInstance [id, info]) }
| IDENT "Existing"; IDENT "Instances"; ids = LIST1 global;
pri = OPT [ "|"; i = natural -> { i } ] ->
{ let info = { Typeclasses.hint_priority = pri; hint_pattern = None } in
let insts = List.map (fun i -> (i, info)) ids in
VernacSynPure (VernacExistingInstance insts) }
| IDENT "Existing"; IDENT "Class"; is = global -> { VernacSynPure (VernacExistingClass is) }
(* Arguments *)
| IDENT "Arguments"; qid = smart_global;
args = LIST0 arg_specs;
more_implicits = OPT
[ ","; impl = LIST1
[ impl = LIST0 implicits_alt -> { List.flatten impl } ]
SEP "," -> { impl }
];
mods = OPT [ ":"; l = LIST1 args_modifier SEP "," -> { l } ] ->
{ let mods = match mods with None -> [] | Some l -> List.flatten l in
let more_implicits = Option.default [] more_implicits in
VernacSynPure (VernacArguments (qid, List.flatten args, more_implicits, mods)) }
| IDENT "Implicit"; "Type"; bl = reserv_list ->
{ VernacSynPure (VernacReserve bl) }
| IDENT "Implicit"; IDENT "Types"; bl = reserv_list ->
{ test_plural_form_types loc "Implicit Types" bl;
VernacSynPure (VernacReserve bl) }
| IDENT "Generalizable";
gen = [IDENT "All"; IDENT "Variables" -> { Some [] }
| IDENT "No"; IDENT "Variables" -> { None }
| ["Variable" -> { () } | IDENT "Variables" -> { () } ];
idl = LIST1 identref -> { Some idl } ] ->
{ VernacSynPure (VernacGeneralizable gen) } ] ]
;
args_modifier:
[ [ IDENT "simpl"; IDENT "nomatch" -> { [`SimplDontExposeCase] }
| IDENT "simpl"; IDENT "never" -> { [`SimplNeverUnfold] }
| IDENT "clear"; IDENT "simpl" -> { [`ClearReduction] }
| IDENT "default"; IDENT "implicits" -> { [`DefaultImplicits] }
| IDENT "clear"; IDENT "implicits" -> { [`ClearImplicits] }
| IDENT "clear"; IDENT "scopes" -> { [`ClearScopes] }
| IDENT "clear"; IDENT "bidirectionality"; IDENT "hint" -> { [`ClearBidiHint] }
| IDENT "rename" -> { [`Rename] }
| IDENT "assert" -> { [`Assert] }
| IDENT "extra"; IDENT "scopes" -> { [`ExtraScopes] }
| IDENT "clear"; IDENT "scopes"; IDENT "and"; IDENT "implicits" ->
{ [`ClearImplicits; `ClearScopes] }
| IDENT "clear"; IDENT "implicits"; IDENT "and"; IDENT "scopes" ->
{ [`ClearImplicits; `ClearScopes] }
] ]
;
scope_delimiter:
[ [ "%"; key = IDENT -> { DelimUnboundedScope, key }
| "%_"; key = IDENT -> { DelimOnlyTmpScope, key } ] ]
;
argument_spec: [
[ b = OPT "!"; id = name ; s = LIST0 scope_delimiter ->
{ id.CAst.v, not (Option.is_empty b), List.map (fun x -> CAst.make ~loc x) s }
]
];
(* List of arguments implicit status, scope, modifiers *)
arg_specs: [
[ item = argument_spec ->
{ let name, recarg_like, notation_scope = item in
[RealArg { name=name; recarg_like=recarg_like;
notation_scope=notation_scope;
implicit_status = Explicit}] }
| "/" -> { [VolatileArg] }
| "&" -> { [BidiArg] }
| "("; items = LIST1 argument_spec; ")"; scl = LIST0 scope_delimiter ->
{ let scl = List.map (CAst.make ~loc) scl in
List.map (fun (name,recarg_like,notation_scope) ->
RealArg { name=name; recarg_like=recarg_like;
notation_scope = notation_scope @ scl;
implicit_status = Explicit}) items }
| "["; items = LIST1 argument_spec; "]"; scl = LIST0 scope_delimiter ->
{ let scl = List.map (CAst.make ~loc) scl in
List.map (fun (name,recarg_like,notation_scope) ->
RealArg { name=name; recarg_like=recarg_like;
notation_scope = notation_scope @ scl;
implicit_status = NonMaxImplicit}) items }
| "{"; items = LIST1 argument_spec; "}"; scl = LIST0 scope_delimiter ->
{ let scl = List.map (CAst.make ~loc) scl in
List.map (fun (name,recarg_like,notation_scope) ->
RealArg { name=name; recarg_like=recarg_like;
notation_scope = notation_scope @ scl;
implicit_status = MaxImplicit}) items }
]
];
(* Same as [arg_specs], but with only implicit status and names *)
implicits_alt: [
[ name = name -> { [(name.CAst.v, Explicit)] }
| "["; items = LIST1 name; "]" ->
{ List.map (fun name -> (name.CAst.v, NonMaxImplicit)) items }
| "{"; items = LIST1 name; "}" ->
{ List.map (fun name -> (name.CAst.v, MaxImplicit)) items }
]
];
instance_name:
[ [ name = ident_decl; bl = binders ->
{ (CAst.map (fun id -> Name id) (fst name), snd name), bl }
| -> { ((CAst.make ~loc Anonymous), None), [] } ] ]
;
hint_info:
[ [ "|"; i = OPT natural; pat = OPT constr_pattern ->
{ { Typeclasses.hint_priority = i; hint_pattern = pat } }
| -> { { Typeclasses.hint_priority = None; hint_pattern = None } } ] ]
;
reserv_list:
[ [ bl = LIST1 reserv_tuple -> { bl } | b = simple_reserv -> { [b] } ] ]
;
reserv_tuple:
[ [ "("; a = simple_reserv; ")" -> { a } ] ]
;
simple_reserv:
[ [ idl = LIST1 identref; ":"; c = lconstr -> { (idl,c) } ] ]
;
END
{
(* Hack to parse "[ id" without dropping [ *)
let test_bracket_ident =
let open Procq.Lookahead in
to_entry "test_bracket_ident" begin
lk_kw "[" >> lk_ident
end
}
GRAMMAR EXTEND Gram
GLOBAL: toplevel_selector goal_selector;
range_selector:
[ [ n = natural ; "-" ; m = natural -> { Proofview.RangeSelector (n, m) }
| n = natural -> { Proofview.NthSelector n }
| test_bracket_ident; "["; id = ident; "]" -> { Proofview.IdSelector id } ] ]
;
goal_selector:
[ [ l = LIST1 range_selector SEP "," -> { Goal_select.SelectList l } ] ]
;
toplevel_selector:
[ [ sel = goal_selector; ":" -> { sel }
| "!"; ":" -> { Goal_select.SelectAlreadyFocused }
| IDENT "all"; ":" -> { Goal_select.SelectAll } ] ]
;
END
GRAMMAR EXTEND Gram
GLOBAL: command query_command coercion_class gallina_ext search_query search_queries;
gallina_ext: TOP
[ [ IDENT "Export"; "Set"; table = setting_name; v = option_setting ->
{ VernacSynterp (VernacSetOption (true, table, v)) }
| IDENT "Export"; IDENT "Unset"; table = setting_name ->
{ VernacSynterp (VernacSetOption (true, table, OptionUnset)) }
] ];
command:
[ [ IDENT "Comments"; l = LIST0 comment -> { VernacSynPure (VernacComments l) }
| IDENT "Attributes"; attr = attribute_list ->
{ VernacSynPure (VernacAttributes attr) }
(* Hack! Should be in grammar_ext, but camlp5 factorizes badly *)
| IDENT "Declare"; IDENT "Instance"; id = ident_decl; bl = binders; ":";
t = term LEVEL "200";
info = hint_info ->
{ VernacSynPure (VernacDeclareInstance (id, bl, t, info)) }
(* Should be in syntax, but camlp5 would not factorize *)
| IDENT "Declare"; IDENT "Scope"; sc = IDENT ->
{ VernacSynPure (VernacDeclareScope sc) }
(* System directory *)
| IDENT "Pwd" -> { VernacSynterp (VernacChdir None) }
| IDENT "Cd" -> { warn_chdir_pwd (); VernacSynterp (VernacChdir None) }
| IDENT "Cd"; dir = ne_string -> { VernacSynterp (VernacChdir (Some dir)) }
| IDENT "Load"; verbosely = [ IDENT "Verbose" -> { true } | -> { false } ];
s = [ s = ne_string -> { s } | s = IDENT -> { s } ] ->
{ VernacSynterp (VernacLoad (verbosely, s)) }
| IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string ->
{ VernacSynterp (VernacDeclareMLModule l) }
| IDENT "Locate"; l = locatable -> { VernacSynPure (VernacLocate l) }
(* Type-Checking *)
| "Type"; c = lconstr -> { VernacSynPure (VernacGlobalCheck c) }
(* Printing (careful factorization of entries) *)
| IDENT "Print"; p = printable -> { VernacSynPure (VernacPrint p) }
| IDENT "Print"; qid = smart_global; l = OPT univ_name_list -> { VernacSynPure (VernacPrint (PrintName (qid,l))) }
| IDENT "Print"; IDENT "Module"; "Type"; qid = global ->
{ VernacSynPure (VernacPrint (PrintModuleType qid)) }
| IDENT "Print"; IDENT "Module"; qid = global ->
{ VernacSynPure (VernacPrint (PrintModule qid)) }
| IDENT "Print"; IDENT "Namespace" ; ns = dirpath ->
{ VernacSynPure (VernacPrint (PrintNamespace ns)) }
| IDENT "Inspect"; n = natural -> { VernacSynPure (VernacPrint (PrintInspect n)) }
(* For acting on parameter tables *)
| "Set"; table = setting_name; v = option_setting ->
{ VernacSynterp (VernacSetOption (false, table, v)) }
| IDENT "Unset"; table = setting_name ->
{ VernacSynterp (VernacSetOption (false, table, OptionUnset)) }
| IDENT "Print"; IDENT "Table"; table = setting_name ->
{ VernacSynPure (VernacPrintOption table) }
| IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 table_value
-> { VernacSynPure (VernacAddOption ([table;field], v)) }
(* A global value below will be hidden by a field above! *)
(* In fact, we give priority to secondary tables *)
(* No syntax for tertiary tables due to conflict *)
(* (but they are unused anyway) *)
| IDENT "Add"; table = IDENT; v = LIST1 table_value ->
{ VernacSynPure (VernacAddOption ([table], v)) }
| IDENT "Test"; table = setting_name; "for"; v = LIST1 table_value
-> { VernacSynPure (VernacMemOption (table, v)) }
| IDENT "Test"; table = setting_name ->
{ VernacSynPure (VernacPrintOption table) }
| IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 table_value
-> { VernacSynPure (VernacRemoveOption ([table;field], v)) }
| IDENT "Remove"; table = IDENT; v = LIST1 table_value ->
{ VernacSynPure (VernacRemoveOption ([table], v)) } ]]
;
query_command:
[ [ IDENT "Eval"; r = red_expr; "in"; c = lconstr; "." ->
{ fun g -> VernacCheckMayEval (Some r, g, c) }
| IDENT "Compute"; c = lconstr; "." ->
{ fun g -> VernacCheckMayEval (Some (Genredexpr.CbvVm None), g, c) }
| IDENT "Check"; c = lconstr; "." ->
{ fun g -> VernacCheckMayEval (None, g, c) }
(* Searching the environment *)
| IDENT "About"; qid = smart_global; l = OPT univ_name_list; "." ->
{ fun g -> VernacPrint (PrintAbout (qid,l,g)) }
| IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules; "." ->
{ fun g -> VernacSearch (SearchPattern c,g, l) }
| IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." ->
{ fun g -> VernacSearch (SearchRewrite c,g, l) }
| IDENT "Search"; s = search_query; l = search_queries; "." ->
{ let (sl,m) = l in fun g -> VernacSearch (Search (s::sl),g, m) }
] ]
;
printable:
[ [ IDENT "Term"; qid = smart_global; l = OPT univ_name_list -> { PrintName (qid,l) }
| IDENT "All" -> { PrintFullContext }
| IDENT "Section"; s = global -> { PrintSectionContext s }
| IDENT "Grammar"; ents = LIST0 IDENT ->
(* This should be in "syntax" section but is here for factorization*)
{ PrintGrammar ents }
| IDENT "Custom"; IDENT "Grammar"; ent = IDENT ->
(* Should also be in "syntax" section *)
{ PrintCustomGrammar ent }
| IDENT "Keywords" ->
{ PrintKeywords }
| IDENT "LoadPath"; dir = OPT dirpath -> { PrintLoadPath dir }
| IDENT "Libraries" -> { PrintLibraries }
| IDENT "Notation"; ntn = string ->
{ PrintNotation (Constrexpr.InConstrEntry, ntn) }
| IDENT "Notation"; ntn = string; IDENT "in"; IDENT "custom"; ent = IDENT ->
{ PrintNotation (Constrexpr.InCustomEntry ent, ntn) }
| IDENT "ML"; IDENT "Path" -> { PrintMLLoadPath }
| IDENT "ML"; IDENT "Modules" -> { PrintMLModules }
| IDENT "Debug"; IDENT "GC" -> { PrintDebugGC }
| IDENT "Graph" -> { PrintGraph }
| IDENT "Classes" -> { PrintClasses }
| IDENT "Typeclasses" -> { PrintTypeclasses }
| IDENT "Instances"; qid = smart_global -> { PrintInstances qid }
| IDENT "Coercions" -> { PrintCoercions }
| IDENT "Coercion"; IDENT "Paths"; s = coercion_class; t = coercion_class ->
{ PrintCoercionPaths (s,t) }
| IDENT "Canonical"; IDENT "Projections"; qids = LIST0 smart_global ->
{ PrintCanonicalConversions qids }
| IDENT "Typing"; IDENT "Flags" -> { PrintTypingFlags }
| IDENT "Tables" -> { PrintTables }
| IDENT "Options" -> { PrintTables (* A Synonymous to Tables *) }
| IDENT "Hint" -> { PrintHintGoal }
| IDENT "Hint"; qid = smart_global -> { PrintHint qid }
| IDENT "Hint"; "*" -> { PrintHintDb }
| IDENT "HintDb"; s = IDENT -> { PrintHintDbName s }
| IDENT "Scopes" -> { PrintScopes }
| IDENT "Scope"; s = IDENT -> { PrintScope s }
| IDENT "Visibility"; s = OPT IDENT -> { PrintVisibility s }
| IDENT "Implicit"; qid = smart_global -> { PrintImplicit qid }
| b = [ IDENT "Sorted" -> { true } | -> { false } ]; IDENT "Universes";
g = OPT printunivs_subgraph;
with_sources = OPT [
b = [ IDENT "With" -> { true } | IDENT "Without" -> { false } ];
IDENT "Constraint"; IDENT "Sources" -> { b } ];
fopt = OPT ne_string ->
{ PrintUniverses {sort=b; subgraph=g; with_sources; file=fopt;} }
| IDENT "Sorts" -> { PrintSorts }
| IDENT "Assumptions"; qid = smart_global -> { PrintAssumptions (false, false, qid) }
| IDENT "Opaque"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (true, false, qid) }
| IDENT "Transparent"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (false, true, qid) }
| IDENT "All"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (true, true, qid) }
| IDENT "Strategy"; qid = smart_global -> { PrintStrategy (Some qid) }
| IDENT "Strategies" -> { PrintStrategy None }
| IDENT "Registered" -> { PrintRegistered }
| IDENT "Registered"; IDENT "Schemes" -> { PrintRegisteredSchemes }
] ]
;
debug_univ_name:
[ [ x = reference -> { NamedUniv x }
| x = STRING -> { RawUniv (CAst.make ~loc x) }
] ]
;
printunivs_subgraph:
[ [ IDENT "Subgraph"; "("; l = LIST0 debug_univ_name; ")" -> { l } ] ]
;
coercion_class:
[ [ IDENT "Funclass" -> { FunClass }
| IDENT "Sortclass" -> { SortClass }
| qid = smart_global -> { RefClass qid } ] ]
;
locatable:
[ [ qid = smart_global -> { LocateAny qid }
| IDENT "Term"; qid = smart_global -> { LocateTerm qid }
| IDENT "File"; f = ne_string -> { LocateFile f }
| IDENT "Library"; qid = global -> { LocateLibrary qid }
| IDENT "Module"; qid = global -> { LocateModule qid } ] ]
;
option_setting:
[ [ -> { OptionSetTrue }
| n = integer -> { OptionSetInt n }
| s = STRING -> { OptionSetString s } ] ]
;
table_value:
[ [ id = global -> { Goptions.QualidRefValue id }
| s = STRING -> { Goptions.StringRefValue s } ] ]
;
setting_name:
[ [ fl = LIST1 [ x = IDENT -> { x } ] -> { fl } ]]
;
ne_in_or_out_modules:
[ [ IDENT "inside"; l = LIST1 global -> { SearchInside l }
| "in"; l = LIST1 global -> { SearchInside l }
| IDENT "outside"; l = LIST1 global -> { SearchOutside l } ] ]
;
in_or_out_modules:
[ [ m = ne_in_or_out_modules -> { m }
| -> { SearchOutside [] } ] ]
;
comment:
[ [ c = constr -> { CommentConstr c }
| s = STRING -> { CommentString s }
| n = natural -> { CommentInt n } ] ]
;
positive_search_mark:
[ [ "-" -> { false } | -> { true } ] ]
;
search_query:
[ [ b = positive_search_mark; s = search_item -> { (b, SearchLiteral s) }
| b = positive_search_mark; "["; l = LIST1 (LIST1 search_query) SEP "|"; "]" -> { (b, SearchDisjConj l) }
] ]
;
search_item:
[ [ test_id_colon; where = search_where; ":"; s = ne_string; sc = OPT scope_delimiter ->
{ SearchString (where,s,sc) }
| IDENT "is"; ":"; kl = logical_kind ->
{ SearchKind kl }
| s = ne_string; sc = OPT scope_delimiter ->
{ SearchString ((Anywhere,false),s,sc) }
| test_id_colon; where = search_where; ":"; p = constr_pattern ->
{ SearchSubPattern (where,p) }
| p = constr_pattern ->
{ SearchSubPattern ((Anywhere,false),p) }
] ]
;
logical_kind:
[ [ k = thm_token -> { IsProof k }
| k = assumption_token -> { IsAssumption (snd k) }
| k = IDENT "Context" -> { IsAssumption Context }
| k = extended_def_token -> { IsDefinition k }
| IDENT "Primitive" -> { IsPrimitive }
| IDENT "Symbol" -> { IsSymbol } ] ]
;
extended_def_token:
[ [ k = def_token -> { snd k }
| IDENT "Coercion" -> { Coercion }
| IDENT "Fixpoint" -> { Fixpoint }
| IDENT "CoFixpoint" -> { CoFixpoint }
| IDENT "Instance" -> { Instance }
| IDENT "Scheme" -> { Scheme }
| IDENT "Canonical" -> { CanonicalStructure }
| IDENT "Field" -> { StructureComponent }
| IDENT "Method" -> { Method } ] ]
;
search_where:
[ [ IDENT "head" -> { Anywhere, true }
| IDENT "hyp" -> { InHyp, false }
| IDENT "concl" -> { InConcl, false }
| IDENT "headhyp" -> { InHyp, true }
| IDENT "headconcl" -> { InConcl, true } ] ]
;
search_queries:
[ [ m = ne_in_or_out_modules -> { ([],m) }
| s = search_query; l = search_queries ->
{ let (sl,m) = l in (s::sl,m) }
| -> { ([],SearchOutside []) }
] ]
;
univ_name_list:
[ [ "@{" ; l = LIST0 name; "}" -> { [],l } ] ]
;
END
GRAMMAR EXTEND Gram
GLOBAL: command;
command: TOP
[ [
(* Resetting *)
IDENT "Reset"; IDENT "Initial" -> { VernacSynPure (VernacResetInitial) }
| IDENT "Reset"; id = identref -> { VernacSynPure (VernacResetName id) }
| IDENT "Back" -> { VernacSynPure (VernacBack 1) }
| IDENT "Back"; n = natural -> { VernacSynPure (VernacBack n) }
(* Tactic Debugger *)
| IDENT "Debug"; IDENT "On" ->
{ VernacSynterp (VernacSetOption (false, ["Ltac";"Debug"], OptionSetTrue)) }
| IDENT "Debug"; IDENT "Off" ->
{ VernacSynterp (VernacSetOption (false, ["Ltac";"Debug"], OptionUnset)) }
(* registration of a custom reduction *)
| IDENT "Declare"; IDENT "Reduction"; s = IDENT; ":=";
r = red_expr ->
{ VernacSynPure (VernacDeclareReduction (s,r)) }
(* factorized here, though relevant for syntax extensions *)
| IDENT "Declare"; IDENT "Custom"; IDENT "Entry"; s = IDENT ->
{ VernacSynterp (VernacDeclareCustomEntry s) }
] ];
END
(* Grammar extensions *)
GRAMMAR EXTEND Gram
GLOBAL: syntax syntax_modifiers;
syntax:
[ [ IDENT "Open"; IDENT "Scope"; sc = IDENT ->
{ VernacSynPure (VernacOpenCloseScope (true,sc)) }
| IDENT "Close"; IDENT "Scope"; sc = IDENT ->
{ VernacSynPure (VernacOpenCloseScope (false,sc)) }
| IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
{ VernacSynPure(VernacDelimiters (sc, Some key)) }
| IDENT "Undelimit"; IDENT "Scope"; sc = IDENT ->
{ VernacSynPure(VernacDelimiters (sc, None)) }
| IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with";
refl = LIST1 coercion_class -> { VernacSynPure (VernacBindScope (sc,refl)) }
| IDENT "Infix"; ntn_decl = notation_declaration ->
{ VernacSynterp (VernacNotation (true,ntn_decl)) }
| IDENT "Notation"; id = identref; idl = LIST0 ident;
":="; c = constr; modl = syntax_modifiers ->
{ VernacSynPure (VernacSyntacticDefinition (id,(idl,c), modl)) }
| IDENT "Notation"; ntn_decl = notation_declaration ->
{ VernacSynterp (VernacNotation (false,ntn_decl)) }
| IDENT "Reserved"; IDENT "Infix"; s = ne_lstring; l = syntax_modifiers ->
{ VernacSynterp (VernacReservedNotation (true,(s,l))) }
| IDENT "Reserved"; IDENT "Notation"; s = ne_lstring; l = syntax_modifiers ->
{ VernacSynterp (VernacReservedNotation (false,(s,l))) }
| on = enable_enable_disable; IDENT "Notation";
rule = enable_notation_rule; interp = enable_notation_interpretation;
flags = enable_notation_flags; scope = opt_scope ->
{ VernacSynPure (VernacEnableNotation (on, rule, interp, flags, scope)) }
(* "Print" "Grammar" and "Declare" "Scope" should be here but are in "command" entry in order
to factorize with other "Print"-based or "Declare"-based vernac entries *)
] ]
;
enable_enable_disable:
[ [ IDENT "Enable" -> { true }
| IDENT "Disable" -> { false } ] ]
;
enable_notation_rule:
[ [ s = ne_string -> { Some (Inl s) }
| qid = global; idl = LIST0 ident -> { Some (Inr (idl,qid)) }
| -> { None } ] ]
;
enable_notation_interpretation:
[ [ ":="; c = constr -> { Some c }
| -> { None } ] ]
;
enable_notation_flags:
[ [ "("; l = LIST1 enable_notation_flag SEP ","; ")" -> { l }
| -> { [] } ] ]
;
enable_notation_flag:
[ [ IDENT "all" -> { EnableNotationAll }
| IDENT "only"; IDENT "parsing" -> { EnableNotationOnly Notationextern.OnlyParsing }
| IDENT "only"; IDENT "printing" -> { EnableNotationOnly Notationextern.OnlyPrinting }
| "in"; IDENT "custom"; x = identref -> { EnableNotationEntry CAst.(make ?loc:x.loc (InCustomEntry (Id.to_string x.v))) }
| "in"; IDENT "constr" -> { EnableNotationEntry (CAst.make ~loc InConstrEntry) } ] ]
;
opt_scope:
[ [ ":"; sc = IDENT -> { Some (NotationInScope sc) }
| ":"; IDENT "no"; IDENT "scope" -> { Some LastLonelyNotation }
| -> { None } ] ]
;
level:
[ [ IDENT "level"; n = natural -> { NumLevel n }
| IDENT "next"; IDENT "level" -> { NextLevel } ] ]
;
syntax_modifier:
[ [ "at"; IDENT "level"; n = natural -> { SetLevel n }
| "in"; IDENT "custom"; x = IDENT -> { SetCustomEntry (x,None) }
| "in"; IDENT "custom"; x = IDENT; "at"; IDENT "level"; n = natural ->
{ SetCustomEntry (x,Some n) }
| IDENT "left"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.LeftA }
| IDENT "right"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.RightA }
| IDENT "no"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.NonA }
| IDENT "only"; IDENT "printing" -> { SetOnlyPrinting }
| IDENT "only"; IDENT "parsing" -> { SetOnlyParsing }
| IDENT "format"; s = lstring -> { SetFormat (TextFormat s) }
| x = IDENT; ","; l = LIST1 IDENT SEP ","; v =
[ "at"; lev = level -> { fun x l -> SetItemLevel (x::l,None,lev) }
| "in"; IDENT "scope"; k = IDENT -> { fun x l -> SetItemScope(x::l,k) } ] -> { v x l }
| x = IDENT; "at"; lev = level; b = OPT binder_interp ->
{ SetItemLevel ([x],b,lev) }
| x = IDENT; "in"; IDENT "scope"; k = IDENT -> { SetItemScope([x],k) }
| x = IDENT; b = binder_interp -> { SetItemLevel ([x],Some b,DefaultLevel) }
| x = IDENT; typ = explicit_subentry -> { SetEntryType (x,typ) }
] ]
;
syntax_modifiers:
[ [ "("; l = LIST1 [ s = syntax_modifier -> { CAst.make ~loc s } ] SEP ","; ")" -> { l }
| -> { [] }
] ]
;
explicit_subentry:
[ [ IDENT "ident" -> { ETIdent }
| IDENT "name" -> { ETName }
| IDENT "global" -> { ETGlobal }
| IDENT "bigint" -> { ETBigint }
| IDENT "binder" -> { ETBinder true }
| IDENT "constr" -> { ETConstr (InConstrEntry,None,DefaultLevel) }
| IDENT "constr"; n = at_level_opt; b = OPT binder_interp -> { ETConstr (InConstrEntry,b,n) }
| IDENT "pattern" -> { ETPattern (false,None) }
| IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (false,Some n) }
| IDENT "strict"; IDENT "pattern" -> { ETPattern (true,None) }
| IDENT "strict"; IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (true,Some n) }
| IDENT "closed"; IDENT "binder" -> { ETBinder false }
| IDENT "custom"; x = IDENT; n = at_level_opt; b = OPT binder_interp ->
{ ETConstr (InCustomEntry x,b,n) }
] ]
;
at_level_opt:
[ [ "at"; n = level -> { n }
| -> { DefaultLevel } ] ]
;
binder_interp:
[ [ "as"; IDENT "ident" -> { warn_deprecated_as_ident_kind (); Notation_term.AsIdent }
| "as"; IDENT "name" -> { Notation_term.AsName }
| "as"; IDENT "pattern" -> { Notation_term.AsAnyPattern }
| "as"; IDENT "strict"; IDENT "pattern" -> { Notation_term.AsStrictPattern } ] ]
;
END
[ Dauer der Verarbeitung: 0.52 Sekunden
(vorverarbeitet)
]
|
