aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_constr.ml42
-rw-r--r--parsing/g_proofs.ml46
-rw-r--r--parsing/g_vernac.ml442
-rw-r--r--parsing/pcoq.ml1
-rw-r--r--parsing/pcoq.mli1
5 files changed, 34 insertions, 18 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index ad8c1c398..844c040fd 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -301,7 +301,7 @@ GEXTEND Gram
| -> [] ] ]
;
instance:
- [ [ "@{"; l = LIST1 universe_level; "}" -> Some l
+ [ [ "@{"; l = LIST0 universe_level; "}" -> Some l
| -> None ] ]
;
universe_level:
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 42b5bfa93..e2c87bbbf 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -45,11 +45,9 @@ GEXTEND Gram
| IDENT "Existential"; n = natural; c = constr_body ->
VernacSolveExistential (n,c)
| IDENT "Admitted" -> VernacEndProof Admitted
- | IDENT "Qed" -> VernacEndProof (Proved (Opaque None,None))
- | IDENT "Qed"; IDENT "exporting"; l = LIST0 identref SEP "," ->
- VernacEndProof (Proved (Opaque (Some l),None))
+ | IDENT "Qed" -> VernacEndProof (Proved (Opaque,None))
| IDENT "Save"; id = identref ->
- VernacEndProof (Proved (Opaque None, Some id))
+ VernacEndProof (Proved (Opaque, Some id))
| IDENT "Defined" -> VernacEndProof (Proved (Transparent,None))
| IDENT "Defined"; id=identref ->
VernacEndProof (Proved (Transparent,Some id))
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 0da22fd71..819d236cd 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -131,20 +131,20 @@ let test_plural_form_types loc kwd = function
let fresh_var env c =
Namegen.next_ident_away (Id.of_string "pat")
- (env @ Id.Set.elements (Topconstr.free_vars_of_constr_expr c))
+ (List.fold_left (fun accu id -> Id.Set.add id accu) (Topconstr.free_vars_of_constr_expr c) env)
let _ = Hook.set Constrexpr_ops.fresh_var_hook fresh_var
(* Gallina declarations *)
GEXTEND Gram
GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
- record_field decl_notation rec_definition pidentref;
+ record_field decl_notation rec_definition pidentref ident_decl;
gallina:
(* Definition, Theorem, Variable, Axiom, ... *)
- [ [ thm = thm_token; id = pidentref; bl = binders; ":"; c = lconstr;
+ [ [ thm = thm_token; id = ident_decl; bl = binders; ":"; c = lconstr;
l = LIST0
- [ "with"; id = pidentref; bl = binders; ":"; c = lconstr ->
+ [ "with"; id = ident_decl; bl = binders; ":"; c = lconstr ->
(Some id,(bl,c)) ] ->
VernacStartTheoremProof (thm, (Some id,(bl,c))::l)
| stre = assumption_token; nl = inline; bl = assum_list ->
@@ -152,7 +152,7 @@ GEXTEND Gram
| (kwd,stre) = assumptions_token; nl = inline; bl = assum_list ->
test_plural_form loc kwd bl;
VernacAssumption (stre, nl, bl)
- | d = def_token; id = pidentref; b = def_body ->
+ | d = def_token; id = ident_decl; b = def_body ->
VernacDefinition (d, id, b)
| IDENT "Let"; id = identref; b = def_body ->
VernacDefinition ((Some Discharge, Definition), (id, None), b)
@@ -224,13 +224,29 @@ GEXTEND Gram
| IDENT "Inline" -> DefaultInline
| -> NoInline] ]
;
- pidentref:
- [ [ i = identref; l = OPT [ "@{" ; l = LIST0 identref; "}" -> l ] -> (i,l) ] ]
- ;
univ_constraint:
[ [ l = universe_level; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ];
r = universe_level -> (l, ord, r) ] ]
;
+ pidentref:
+ [ [ i = identref; l = OPT [ "@{" ; l = LIST0 identref; "}" -> l ] -> (i,l) ] ]
+ ;
+ univ_decl :
+ [ [ "@{" ; l = LIST0 identref; ext = [ "+" -> true | -> false ];
+ cs = [ "|"; l' = LIST0 univ_constraint SEP ",";
+ ext = [ "+" -> true | -> false ]; "}" -> (l',ext)
+ | ext = [ "}" -> true | "|}" -> false ] -> ([], ext) ]
+ ->
+ { 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)
+ ] ]
+ ;
finite_token:
[ [ IDENT "Inductive" -> (Inductive_kw,Finite)
| IDENT "CoInductive" -> (CoInductive,CoFinite)
@@ -288,7 +304,7 @@ GEXTEND Gram
| -> RecordDecl (None, []) ] ]
;
inductive_definition:
- [ [ oc = opt_coercion; id = pidentref; indpar = binders;
+ [ [ oc = opt_coercion; id = ident_decl; indpar = binders;
c = OPT [ ":"; c = lconstr -> c ];
lc=opt_constructors_or_fields; ntn = decl_notation ->
(((oc,id),indpar,c,lc),ntn) ] ]
@@ -314,14 +330,14 @@ GEXTEND Gram
;
(* (co)-fixpoints *)
rec_definition:
- [ [ id = pidentref;
+ [ [ id = ident_decl;
bl = binders_fixannot;
ty = type_cstr;
def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
let bl, annot = bl in ((id,annot,bl,ty,def),ntn) ] ]
;
corec_definition:
- [ [ id = pidentref; bl = binders; ty = type_cstr;
+ [ [ id = ident_decl; bl = binders; ty = type_cstr;
def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
((id,bl,ty,def),ntn) ] ]
;
@@ -393,7 +409,7 @@ GEXTEND Gram
[ [ "("; a = simple_assum_coe; ")" -> a ] ]
;
simple_assum_coe:
- [ [ idl = LIST1 pidentref; oc = of_type_with_opt_coercion; c = lconstr ->
+ [ [ idl = LIST1 ident_decl; oc = of_type_with_opt_coercion; c = lconstr ->
(not (Option.is_empty oc),(idl,c)) ] ]
;
@@ -796,7 +812,7 @@ GEXTEND Gram
| IDENT "transparent" -> Conv_oracle.transparent ] ]
;
instance_name:
- [ [ name = pidentref; sup = OPT binders ->
+ [ [ name = ident_decl; sup = OPT binders ->
(let ((loc,id),l) = name in ((loc, Name id),l)),
(Option.default [] sup)
| -> ((Loc.tag ~loc:!@loc Anonymous), None), [] ] ]
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 40c5da7a5..3d00b220b 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -445,6 +445,7 @@ module Prim =
let name = Gram.entry_create "Prim.name"
let identref = Gram.entry_create "Prim.identref"
let pidentref = Gram.entry_create "Prim.pidentref"
+ let ident_decl = Gram.entry_create "Prim.ident_decl"
let pattern_ident = Gram.entry_create "pattern_ident"
let pattern_identref = Gram.entry_create "pattern_identref"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 4e6bff20a..2f0375419 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -195,6 +195,7 @@ module Prim :
val name : Name.t located Gram.entry
val identref : Id.t located Gram.entry
val pidentref : (Id.t located * (Id.t located list) option) Gram.entry
+ val ident_decl : ident_decl Gram.entry
val pattern_ident : Id.t Gram.entry
val pattern_identref : Id.t located Gram.entry
val base_ident : Id.t Gram.entry
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 14:22:05 +0000