aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_constr.mlg83
-rw-r--r--parsing/g_prim.mlg13
-rw-r--r--parsing/pcoq.ml5
-rw-r--r--parsing/pcoq.mli6
4 files changed, 66 insertions, 41 deletions
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 6df97609f5..79cfe33b12 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -31,8 +31,10 @@ let ldots_var = Id.of_string ".."
let constr_kw =
[ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for";
"end"; "as"; "let"; "if"; "then"; "else"; "return";
- "SProp"; "Prop"; "Set"; "Type"; ".("; "_"; "..";
- "`{"; "`("; "{|"; "|}" ]
+ "SProp"; "Prop"; "Set"; "Type";
+ ":="; "=>"; "->"; ".."; "<:"; "<<:"; ":>";
+ ".("; "()"; "`{"; "`("; "@{"; "{|";
+ "_"; "@"; "+"; "!"; "?"; ";"; ","; ":" ]
let _ = List.iter CLexer.add_keyword constr_kw
@@ -131,7 +133,8 @@ let aliasvar = function { CAst.v = CPatAlias (_, na) } -> Some na | _ -> None
}
GRAMMAR EXTEND Gram
- GLOBAL: binder_constr lconstr constr operconstr universe_level sort sort_family
+ GLOBAL: binder_constr lconstr constr operconstr
+ universe_level universe_name sort sort_family
global constr_pattern lconstr_pattern Constr.ident
closed_binder open_binders binder binders binders_fixannot
record_declaration typeclass_constraint pattern appl_arg;
@@ -151,11 +154,12 @@ GRAMMAR EXTEND Gram
[ [ c = lconstr -> { c } ] ]
;
sort:
- [ [ "Set" -> { GSet }
- | "Prop" -> { GProp }
- | "SProp" -> { GSProp }
- | "Type" -> { GType [] }
- | "Type"; "@{"; u = universe; "}" -> { GType u }
+ [ [ "Set" -> { UNamed [GSet,0] }
+ | "Prop" -> { UNamed [GProp,0] }
+ | "SProp" -> { UNamed [GSProp,0] }
+ | "Type" -> { UAnonymous {rigid=true} }
+ | "Type"; "@{"; "_"; "}" -> { UAnonymous {rigid=false} }
+ | "Type"; "@{"; u = universe; "}" -> { UNamed u }
] ]
;
sort_family:
@@ -165,11 +169,17 @@ GRAMMAR EXTEND Gram
| "Type" -> { Sorts.InType }
] ]
;
+ universe_increment:
+ [ [ "+"; n = natural -> { n }
+ | -> { 0 } ] ]
+ ;
+ universe_name:
+ [ [ id = global -> { GType id }
+ | "Set" -> { GSet }
+ | "Prop" -> { GProp } ] ]
+ ;
universe_expr:
- [ [ id = global; "+"; n = natural -> { Some (id,n) }
- | id = global -> { Some (id,0) }
- | "_" -> { None }
- ] ]
+ [ [ id = universe_name; n = universe_increment -> { (id,n) } ] ]
;
universe:
[ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> { ids }
@@ -225,11 +235,13 @@ GRAMMAR EXTEND Gram
[ c=atomic_constr -> { c }
| c=match_constr -> { c }
| "("; c = operconstr LEVEL "200"; ")" ->
- { (match c.CAst.v with
+ { (* Preserve parentheses around numerals so that constrintern does not
+ collapse -(3) into the numeral -3. *)
+ (match c.CAst.v with
| CPrim (Numeral (SPlus,n)) ->
CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"( _ )"),([c],[],[],[]))
| _ -> c) }
- | "{|"; c = record_declaration; "|}" -> { c }
+ | "{|"; c = record_declaration; bar_cbrace -> { c }
| "{"; c = binder_constr ; "}" ->
{ CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) }
| "`{"; c = operconstr LEVEL "200"; "}" ->
@@ -277,16 +289,16 @@ GRAMMAR EXTEND Gram
":="; c1 = operconstr LEVEL "200"; "in";
c2 = operconstr LEVEL "200" ->
{ CAst.make ~loc @@ CLetTuple (lb,po,c1,c2) }
- | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
+ | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200";
"in"; c2 = operconstr LEVEL "200" ->
{ CAst.make ~loc @@
CCases (LetPatternStyle, None, [c1, None, None], [CAst.make ~loc ([[p]], c2)]) }
- | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
+ | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200";
rt = case_type; "in"; c2 = operconstr LEVEL "200" ->
{ CAst.make ~loc @@
CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [CAst.make ~loc ([[p]], c2)]) }
- | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200";
+ | "let"; "'"; p = pattern LEVEL "200"; "in"; t = pattern LEVEL "200";
":="; c1 = operconstr LEVEL "200"; rt = case_type;
"in"; c2 = operconstr LEVEL "200" ->
{ CAst.make ~loc @@
@@ -324,12 +336,12 @@ GRAMMAR EXTEND Gram
| -> { None } ] ]
;
universe_level:
- [ [ "Set" -> { GSet }
+ [ [ "Set" -> { UNamed GSet }
(* no parsing SProp as a level *)
- | "Prop" -> { GProp }
- | "Type" -> { GType UUnknown }
- | "_" -> { GType UAnonymous }
- | id = global -> { GType (UNamed id) }
+ | "Prop" -> { UNamed GProp }
+ | "Type" -> { UAnonymous {rigid=true} }
+ | "_" -> { UAnonymous {rigid=false} }
+ | id = global -> { UNamed (GType id) }
] ]
;
fix_constr:
@@ -359,7 +371,7 @@ GRAMMAR EXTEND Gram
case_item:
[ [ c=operconstr LEVEL "100";
ona = OPT ["as"; id=name -> { id } ];
- ty = OPT ["in"; t=pattern -> { t } ] ->
+ ty = OPT ["in"; t = pattern LEVEL "200" -> { t } ] ->
{ (c,ona,ty) } ] ]
;
case_type:
@@ -377,14 +389,14 @@ GRAMMAR EXTEND Gram
[ [ OPT"|"; br=LIST0 eqn SEP "|" -> { br } ] ]
;
mult_pattern:
- [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> { pl } ] ]
+ [ [ pl = LIST1 pattern LEVEL "200" SEP "," -> { pl } ] ]
;
eqn:
[ [ pll = LIST1 mult_pattern SEP "|";
"=>"; rhs = lconstr -> { (CAst.make ~loc (pll,rhs)) } ] ]
;
record_pattern:
- [ [ id = global; ":="; pat = pattern -> { (id, pat) } ] ]
+ [ [ id = global; ":="; pat = pattern LEVEL "200" -> { (id, pat) } ] ]
;
record_patterns:
[ [ p = record_pattern; ";"; ps = record_patterns -> { p :: ps }
@@ -396,7 +408,10 @@ GRAMMAR EXTEND Gram
pattern:
[ "200" RIGHTA [ ]
| "100" RIGHTA
- [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> { CAst.make ~loc @@ CPatOr (p::pl) } ]
+ [ p = pattern; ":"; ty = binder_constr ->
+ {CAst.make ~loc @@ CPatCast (p, ty) }
+ | p = pattern; ":"; ty = operconstr LEVEL "100" ->
+ {CAst.make ~loc @@ CPatCast (p, ty) } ]
| "99" RIGHTA [ ]
| "90" RIGHTA [ ]
| "10" LEFTA
@@ -409,21 +424,17 @@ GRAMMAR EXTEND Gram
[ c = pattern; "%"; key=IDENT -> { CAst.make ~loc @@ CPatDelimiters (key,c) } ]
| "0"
[ r = Prim.reference -> { CAst.make ~loc @@ CPatAtom (Some r) }
- | "{|"; pat = record_patterns; "|}" -> { CAst.make ~loc @@ CPatRecord pat }
+ | "{|"; pat = record_patterns; bar_cbrace -> { CAst.make ~loc @@ CPatRecord pat }
| "_" -> { CAst.make ~loc @@ CPatAtom None }
| "("; p = pattern LEVEL "200"; ")" ->
- { (match p.CAst.v with
+ { (* Preserve parentheses around numerals so that constrintern does not
+ collapse -(3) into the numeral -3. *)
+ (match p.CAst.v with
| CPatPrim (Numeral (SPlus,n)) ->
CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
| _ -> p) }
- | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" ->
- { let p =
- match p with
- | { CAst.v = CPatPrim (Numeral (SPlus,n)) } ->
- CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
- | _ -> p
- in
- CAst.make ~loc @@ CPatCast (p, ty) }
+ | "("; p = pattern LEVEL "200"; "|" ; pl = LIST1 pattern LEVEL "200" SEP "|"; ")" ->
+ { CAst.make ~loc @@ CPatOr (p::pl) }
| n = NUMERAL-> { CAst.make ~loc @@ CPatPrim (Numeral (SPlus,n)) }
| s = string -> { CAst.make ~loc @@ CPatPrim (String s) } ] ]
;
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index 80dd997860..9653964262 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -15,7 +15,7 @@ open Libnames
open Pcoq.Prim
-let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"]
+let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"; "%"; "|"]
let _ = List.iter CLexer.add_keyword prim_kw
@@ -31,13 +31,19 @@ let my_int_of_string loc s =
with Failure _ ->
CErrors.user_err ~loc (Pp.str "This number is too large.")
+let check_nospace loc expected =
+ let (bp, ep) = Loc.unloc loc in
+ if ep = bp + String.length expected then () else
+ Gramlib.Ploc.raise loc (Stream.Error ("'" ^ expected ^ "' expected"))
+
}
GRAMMAR EXTEND Gram
GLOBAL:
bigint natural integer identref name ident var preident
fullyqualid qualid reference dirpath ne_lstring
- ne_string string lstring pattern_ident pattern_identref by_notation smart_global;
+ ne_string string lstring pattern_ident pattern_identref by_notation
+ smart_global bar_cbrace;
preident:
[ [ s = IDENT -> { s } ] ]
;
@@ -123,4 +129,7 @@ GRAMMAR EXTEND Gram
bigint: (* Negative numbers are dealt with elsewhere *)
[ [ i = NUMERAL -> { check_int loc i } ] ]
;
+ bar_cbrace:
+ [ [ "|"; "}" -> { check_nospace loc "|}" } ] ]
+ ;
END
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 8f38e437b4..b375c526ad 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -411,6 +411,8 @@ module Prim =
let ne_string = Entry.create "Prim.ne_string"
let ne_lstring = Entry.create "Prim.ne_lstring"
+ let bar_cbrace = Entry.create "'|}'"
+
end
module Constr =
@@ -425,6 +427,7 @@ module Constr =
let binder_constr = gec_constr "binder_constr"
let ident = make_gen_entry uconstr "ident"
let global = make_gen_entry uconstr "global"
+ let universe_name = make_gen_entry uconstr "universe_name"
let universe_level = make_gen_entry uconstr "universe_level"
let sort = make_gen_entry uconstr "sort"
let sort_family = make_gen_entry uconstr "sort_family"
@@ -585,7 +588,7 @@ let unfreeze (grams, lex) =
(** No need to provide an init function : the grammar state is
statically available, and already empty initially, while
- the lexer state should not be resetted, since it contains
+ the lexer state should not be reset, since it contains
keywords declared in g_*.ml4 *)
let parser_summary_tag =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 3a57c14a3b..196835f184 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -38,9 +38,9 @@ end
- dynamic rules declared at the evaluation of Coq files (using
e.g. Notation, Infix, or Tactic Notation)
- - static rules explicitly defined in files g_*.ml4
+ - static rules explicitly defined in files g_*.mlg
- static rules macro-generated by ARGUMENT EXTEND, TACTIC EXTEND and
- VERNAC EXTEND (see e.g. file extratactics.ml4)
+ VERNAC EXTEND (see e.g. file extratactics.mlg)
Note that parsing a Coq document is in essence stateful: the parser
needs to recognize commands that start proofs and use a different
@@ -170,6 +170,7 @@ module Prim :
val ne_string : string Entry.t
val ne_lstring : lstring Entry.t
val var : lident Entry.t
+ val bar_cbrace : unit Entry.t
end
module Constr :
@@ -181,6 +182,7 @@ module Constr :
val operconstr : constr_expr Entry.t
val ident : Id.t Entry.t
val global : qualid Entry.t
+ val universe_name : Glob_term.glob_sort_name Entry.t
val universe_level : Glob_term.glob_level Entry.t
val sort : Glob_term.glob_sort Entry.t
val sort_family : Sorts.family Entry.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 16:59:59 +0000