aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/egramcoq.ml76
-rw-r--r--parsing/egramcoq.mli2
-rw-r--r--parsing/egramml.mli2
-rw-r--r--parsing/g_constr.ml445
-rw-r--r--parsing/g_proofs.ml412
-rw-r--r--parsing/g_vernac.ml4165
-rw-r--r--parsing/pcoq.ml63
-rw-r--r--parsing/pcoq.mli21
-rw-r--r--parsing/tok.ml2
-rw-r--r--parsing/tok.mli2
10 files changed, 205 insertions, 185 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 9c2766187e..a3d2571549 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -21,11 +21,11 @@ open Names
a reference to the current level (to be translated into "SELF" on the
left border and into "constr LEVEL n" elsewhere), to the level below
(to be translated into "NEXT") or to an below wrt associativity (to be
- translated in camlp4 into "constr" without level) or to another level
+ translated in camlp5 into "constr" without level) or to another level
(to be translated into "constr LEVEL n")
The boolean is true if the entry was existing _and_ empty; this to
- circumvent a weakness of camlp4/camlp5 whose undo mechanism is not the
+ circumvent a weakness of camlp5 whose undo mechanism is not the
converse of the extension mechanism *)
let constr_level = string_of_int
@@ -144,11 +144,11 @@ let find_position accu forpat assoc level =
(**************************************************************************)
(*
- * --- Note on the mapping of grammar productions to camlp4 actions ---
+ * --- Note on the mapping of grammar productions to camlp5 actions ---
*
* Translation of environments: a production
* [ nt1(x1) ... nti(xi) ] -> act(x1..xi)
- * is written (with camlp4 conventions):
+ * is written (with camlp5 conventions):
* (fun vi -> .... (fun v1 -> act(v1 .. vi) )..)
* where v1..vi are the values generated by non-terminals nt1..nti.
* Since the actions are executed by substituting an environment,
@@ -172,8 +172,8 @@ let find_position accu forpat assoc level =
(**********************************************************************)
(* Binding constr entry keys to entries *)
-(* Camlp4 levels do not treat NonA: use RightA with a NEXT on the left *)
-let camlp4_assoc = function
+(* Camlp5 levels do not treat NonA: use RightA with a NEXT on the left *)
+let camlp5_assoc = function
| Some NonA | Some RightA -> RightA
| None | Some LeftA -> LeftA
@@ -205,7 +205,7 @@ let adjust_level assoc from = function
(* If NonA on the left-hand side, adopt the current assoc ?? *)
| (NumLevel n,BorderProd (Left,Some NonA)) -> None
(* If the expected assoc is the current one, set to SELF *)
- | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp4_assoc assoc) ->
+ | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp5_assoc assoc) ->
None
(* Otherwise, force the level, n or n-1, according to expected assoc *)
| (NumLevel n,BorderProd (Left,Some a)) ->
@@ -229,11 +229,11 @@ type (_, _) entry =
| TTName : ('self, Name.t Loc.located) entry
| TTReference : ('self, reference) entry
| TTBigint : ('self, Constrexpr.raw_natural_number) entry
-| TTBinder : ('self, local_binder_expr list) entry
| TTConstr : prod_info * 'r target -> ('r, 'r) entry
| TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
-| TTBinderListT : ('self, local_binder_expr list) entry
-| TTBinderListF : Tok.t list -> ('self, local_binder_expr list list) entry
+| TTPattern : int -> ('self, cases_pattern_expr) entry
+| TTOpenBinderList : ('self, local_binder_expr list) entry
+| TTClosedBinderList : Tok.t list -> ('self, local_binder_expr list list) entry
type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry
@@ -289,31 +289,24 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun as
Alist1 (symbol_of_target typ' assoc from forpat)
| TTConstrList (typ', tkl, forpat) ->
Alist1sep (symbol_of_target typ' assoc from forpat, make_sep_rules tkl)
-| TTBinderListF [] -> Alist1 (Aentry Constr.binder)
-| TTBinderListF tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl)
+| TTPattern p -> Aentryl (Constr.pattern, p)
+| TTClosedBinderList [] -> Alist1 (Aentry Constr.binder)
+| TTClosedBinderList tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl)
| TTName -> Aentry Prim.name
-| TTBinder -> Aentry Constr.binder
-| TTBinderListT -> Aentry Constr.open_binders
+| TTOpenBinderList -> Aentry Constr.open_binders
| TTBigint -> Aentry Prim.bigint
| TTReference -> Aentry Constr.global
let interp_entry forpat e = match e with
-| ETName -> TTAny TTName
-| ETReference -> TTAny TTReference
-| ETBigint -> TTAny TTBigint
-| ETBinder true -> anomaly (Pp.str "Should occur only as part of BinderList.")
-| ETBinder false -> TTAny TTBinder
-| ETConstr p -> TTAny (TTConstr (p, forpat))
-| ETPattern -> assert false (** not used *)
-| ETOther _ -> assert false (** not used *)
-| ETConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat))
-| ETBinderList (true, []) -> TTAny TTBinderListT
-| ETBinderList (true, _) -> assert false
-| ETBinderList (false, tkl) -> TTAny (TTBinderListF tkl)
-
-let constr_expr_of_name (loc,na) = CAst.make ?loc @@ match na with
- | Anonymous -> CHole (None,Misctypes.IntroAnonymous,None)
- | Name id -> CRef (Ident (Loc.tag ?loc id), None)
+| ETProdName -> TTAny TTName
+| ETProdReference -> TTAny TTReference
+| ETProdBigint -> TTAny TTBigint
+| ETProdConstr p -> TTAny (TTConstr (p, forpat))
+| ETProdPattern p -> TTAny (TTPattern p)
+| ETProdOther _ -> assert false (** not used *)
+| ETProdConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat))
+| ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList
+| ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl)
let cases_pattern_expr_of_name (loc,na) = CAst.make ?loc @@ match na with
| Anonymous -> CPatAtom None
@@ -322,7 +315,8 @@ let cases_pattern_expr_of_name (loc,na) = CAst.make ?loc @@ match na with
type 'r env = {
constrs : 'r list;
constrlists : 'r list list;
- binders : (local_binder_expr list * bool) list;
+ binders : cases_pattern_expr list;
+ binderlists : local_binder_expr list list;
}
let push_constr subst v = { subst with constrs = v :: subst.constrs }
@@ -332,12 +326,16 @@ match e with
| TTConstr _ -> push_constr subst v
| TTName ->
begin match forpat with
- | ForConstr -> push_constr subst (constr_expr_of_name v)
+ | ForConstr -> { subst with binders = cases_pattern_expr_of_name v :: subst.binders }
| ForPattern -> push_constr subst (cases_pattern_expr_of_name v)
end
-| TTBinder -> { subst with binders = (v, true) :: subst.binders }
-| TTBinderListT -> { subst with binders = (v, true) :: subst.binders }
-| TTBinderListF _ -> { subst with binders = (List.flatten v, false) :: subst.binders }
+| TTPattern _ ->
+ begin match forpat with
+ | ForConstr -> { subst with binders = v :: subst.binders }
+ | ForPattern -> push_constr subst v
+ end
+| TTOpenBinderList -> { subst with binderlists = v :: subst.binderlists }
+| TTClosedBinderList _ -> { subst with binderlists = List.flatten v :: subst.binderlists }
| TTBigint ->
begin match forpat with
| ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (v,true)))
@@ -437,11 +435,9 @@ let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list =
let make_act : type r. r target -> _ -> r gen_eval = function
| ForConstr -> fun notation loc env ->
- let env = (env.constrs, env.constrlists, List.map fst env.binders) in
- CAst.make ~loc @@ CNotation (notation , env)
+ let env = (env.constrs, env.constrlists, env.binders, env.binderlists) in
+ CAst.make ~loc @@ CNotation (notation, env)
| ForPattern -> fun notation loc env ->
- let invalid = List.exists (fun (_, b) -> not b) env.binders in
- let () = if invalid then Constrexpr_ops.error_invalid_pattern_notation ~loc () in
let env = (env.constrs, env.constrlists) in
CAst.make ~loc @@ CPatNotation (notation, env, [])
@@ -457,7 +453,7 @@ let extend_constr state forpat ng =
let needed_levels, state = register_empty_levels state isforpat pure_sublevels in
let (pos,p4assoc,name,reinit), state = find_position state isforpat assoc level in
let empty_rules = List.map (prepare_empty_levels isforpat) needed_levels in
- let empty = { constrs = []; constrlists = []; binders = [] } in
+ let empty = { constrs = []; constrlists = []; binders = []; binderlists = [] } in
let act = ty_eval r (make_act forpat ng.notgram_notation) empty in
let rule = (name, p4assoc, [Rule (symbs, act)]) in
let r = ExtendRule (entry, reinit, (pos, [rule])) in
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 8e0469275c..1e38698184 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(** Mapping of grammar productions to camlp4 actions *)
+(** Mapping of grammar productions to camlp5 actions *)
(** This is the part specific to Coq-level Notation and Tactic Notation.
For the ML-level tactic and vernac extensions, see Egramml. *)
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
index 7414773d37..74dd95a200 100644
--- a/parsing/egramml.mli
+++ b/parsing/egramml.mli
@@ -8,7 +8,7 @@
open Vernacexpr
-(** Mapping of grammar productions to camlp4 actions. *)
+(** Mapping of grammar productions to camlp5 actions. *)
(** This is the part specific to vernac extensions.
For the Coq-level Notation and Tactic Notation, see Egramcoq. *)
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 7e5933cea2..9f12db649b 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -120,7 +120,7 @@ let name_colon =
| _ -> err ())
| _ -> err ())
-let aliasvar = function { CAst.loc = loc; CAst.v = CPatAlias (_, id) } -> Some (loc,Name id) | _ -> None
+let aliasvar = function { CAst.v = CPatAlias (_, na) } -> Some na | _ -> None
GEXTEND Gram
GLOBAL: binder_constr lconstr constr operconstr universe_level sort sort_family
@@ -155,9 +155,15 @@ GEXTEND Gram
| "Type" -> Sorts.InType
] ]
;
+ universe_expr:
+ [ [ id = global; "+"; n = natural -> Some (id,n)
+ | id = global -> Some (id,0)
+ | "_" -> None
+ ] ]
+ ;
universe:
- [ [ IDENT "max"; "("; ids = LIST1 name SEP ","; ")" -> ids
- | id = name -> [id]
+ [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> ids
+ | u = universe_expr -> [u]
] ]
;
lconstr:
@@ -210,9 +216,11 @@ GEXTEND Gram
| "("; c = operconstr LEVEL "200"; ")" ->
(match c.CAst.v with
| CPrim (Numeral (n,true)) ->
- CAst.make ~loc:(!@loc) @@ CNotation("( _ )",([c],[],[]))
+ CAst.make ~loc:(!@loc) @@ CNotation("( _ )",([c],[],[],[]))
| _ -> c)
| "{|"; c = record_declaration; "|}" -> c
+ | "{"; c = binder_constr ; "}" ->
+ CAst.make ~loc:(!@loc) @@ CNotation(("{ _ }"),([c],[],[],[]))
| "`{"; c = operconstr LEVEL "200"; "}" ->
CAst.make ~loc:(!@loc) @@ CGeneralization (Implicit, None, c)
| "`("; c = operconstr LEVEL "200"; ")" ->
@@ -261,17 +269,17 @@ GEXTEND Gram
| "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
"in"; c2 = operconstr LEVEL "200" ->
CAst.make ~loc:!@loc @@
- CCases (LetPatternStyle, None, [c1, None, None], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)])
+ CCases (LetPatternStyle, None, [c1, None, None], [Loc.tag ~loc:!@loc ([[p]], c2)])
| "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
rt = case_type; "in"; c2 = operconstr LEVEL "200" ->
CAst.make ~loc:!@loc @@
- CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)])
+ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([[p]], c2)])
| "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200";
":="; c1 = operconstr LEVEL "200"; rt = case_type;
"in"; c2 = operconstr LEVEL "200" ->
CAst.make ~loc:!@loc @@
- CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)])
+ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([[p]], c2)])
| "if"; c=operconstr LEVEL "200"; po = return_type;
"then"; b1=operconstr LEVEL "200";
"else"; b2=operconstr LEVEL "200" ->
@@ -307,8 +315,9 @@ GEXTEND Gram
universe_level:
[ [ "Set" -> GSet
| "Prop" -> GProp
- | "Type" -> GType None
- | id = name -> GType (Some id)
+ | "Type" -> GType UUnknown
+ | "_" -> GType UAnonymous
+ | id = global -> GType (UNamed id)
] ]
;
fix_constr:
@@ -355,7 +364,7 @@ GEXTEND Gram
[ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ]
;
mult_pattern:
- [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> (Loc.tag ~loc:!@loc pl) ] ]
+ [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> pl ] ]
;
eqn:
[ [ pll = LIST1 mult_pattern SEP "|";
@@ -378,19 +387,9 @@ GEXTEND Gram
| "99" RIGHTA [ ]
| "90" RIGHTA [ ]
| "10" LEFTA
- [ p = pattern; "as"; id = ident ->
- CAst.make ~loc:!@loc @@ CPatAlias (p, id)
- | p = pattern; lp = LIST1 NEXT ->
- (let open CAst in match p with
- | { v = CPatAtom (Some r) } -> CAst.make ~loc:!@loc @@ CPatCstr (r, None, lp)
- | { v = CPatCstr (r, None, l2); loc } ->
- CErrors.user_err ?loc ~hdr:"compound_pattern"
- (Pp.str "Nested applications not supported.")
- | { v = CPatCstr (r, l1, l2) } -> CAst.make ~loc:!@loc @@ CPatCstr (r, l1 , l2@lp)
- | { v = CPatNotation (n, s, l) } -> CAst.make ~loc:!@loc @@ CPatNotation (n , s, l@lp)
- | _ -> CErrors.user_err
- ?loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern"
- (Pp.str "Such pattern cannot have arguments."))
+ [ p = pattern; "as"; na = name ->
+ CAst.make ~loc:!@loc @@ CPatAlias (p, na)
+ | p = pattern; lp = LIST1 NEXT -> mkAppPattern ~loc:!@loc p lp
| "@"; r = Prim.reference; lp = LIST0 NEXT ->
CAst.make ~loc:!@loc @@ CPatCstr (r, Some lp, []) ]
| "1" LEFTA
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index f10d746770..1c3ba78376 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -28,7 +28,8 @@ GEXTEND Gram
| ":"; l = LIST1 [id = IDENT -> id ] -> l ] ]
;
command:
- [ [ IDENT "Goal"; c = lconstr -> VernacGoal c
+ [ [ IDENT "Goal"; c = lconstr ->
+ VernacDefinition (Decl_kinds.(NoDischarge, Definition), ((Loc.tag ~loc:!@loc Names.Anonymous), None), ProveBody ([], c))
| IDENT "Proof" -> VernacProof (None,None)
| IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn
| IDENT "Proof"; c = lconstr -> VernacExactProof c
@@ -70,19 +71,16 @@ GEXTEND Gram
VernacCreateHintDb (id, b)
| IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases ->
VernacRemoveHints (dbnames, ids)
- | IDENT "Hint"; local = obsolete_locality; h = hint;
+ | IDENT "Hint"; h = hint;
dbnames = opt_hintbases ->
- VernacHints (local,dbnames, h)
+ VernacHints (dbnames, h)
(* Declare "Resolve" explicitly so as to be able to later extend with
"Resolve ->" and "Resolve <-" *)
| IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr;
info = hint_info; dbnames = opt_hintbases ->
- VernacHints (false,dbnames,
+ VernacHints (dbnames,
HintsResolve (List.map (fun x -> (info, true, x)) lc))
] ];
- obsolete_locality:
- [ [ IDENT "Local" -> true | -> false ] ]
- ;
reference_or_constr:
[ [ r = global -> HintsReference r
| c = constr -> HintsConstr c ] ]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 0e585cff77..d90fd3eb70 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -15,8 +15,9 @@ open Constrexpr_ops
open Extend
open Vernacexpr
open Decl_kinds
+open Declarations
open Misctypes
-open Tok (* necessary for camlp4 *)
+open Tok (* necessary for camlp5 *)
open Pcoq
open Pcoq.Prim
@@ -65,39 +66,42 @@ let parse_compat_version ?(allow_old = true) = let open Flags in function
Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".")
GEXTEND Gram
- GLOBAL: vernac gallina_ext noedit_mode subprf;
- vernac: FIRST
- [ [ IDENT "Time"; c = located_vernac -> VernacTime c
+ 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 = vernac -> VernacTimeout(n,v)
- | IDENT "Fail"; v = vernac -> VernacFail v
-
- | IDENT "Local"; v = vernac_poly -> VernacLocal (true, v)
- | IDENT "Global"; v = vernac_poly -> VernacLocal (false, v)
+ | IDENT "Timeout"; n = natural; v = vernac_control -> VernacTimeout(n,v)
+ | IDENT "Fail"; v = vernac_control -> VernacFail v
+ | (f, v) = vernac -> VernacExpr(f, v) ]
+ ]
+ ;
+ vernac:
+ [ [ 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] ]
@@ -111,7 +115,7 @@ GEXTEND Gram
;
located_vernac:
- [ [ v = vernac -> Loc.tag ~loc:!@loc v ] ]
+ [ [ v = vernac_control -> Loc.tag ~loc:!@loc v ] ]
;
END
@@ -129,6 +133,12 @@ let test_plural_form_types loc kwd = function
warn_plural_command ~loc:!@loc kwd
| _ -> ()
+let lname_of_lident : lident -> lname =
+ Loc.map (fun s -> Name s)
+
+let name_of_ident_decl : ident_decl -> name_decl =
+ on_fst lname_of_lident
+
(* Gallina declarations *)
GEXTEND Gram
GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
@@ -139,17 +149,17 @@ GEXTEND Gram
[ [ thm = thm_token; id = ident_decl; bl = binders; ":"; c = lconstr;
l = LIST0
[ "with"; id = ident_decl; bl = binders; ":"; c = lconstr ->
- (Some id,(bl,c)) ] ->
- VernacStartTheoremProof (thm, (Some id,(bl,c))::l)
+ (id,(bl,c)) ] ->
+ VernacStartTheoremProof (thm, (id,(bl,c))::l)
| stre = assumption_token; nl = inline; bl = assum_list ->
VernacAssumption (stre, nl, bl)
| (kwd,stre) = assumptions_token; nl = inline; bl = assum_list ->
test_plural_form loc kwd bl;
VernacAssumption (stre, nl, bl)
| d = def_token; id = ident_decl; b = def_body ->
- VernacDefinition (d, id, b)
+ VernacDefinition (d, name_of_ident_decl id, b)
| IDENT "Let"; id = identref; b = def_body ->
- VernacDefinition ((Some Discharge, Definition), (id, None), b)
+ VernacDefinition ((DoDischarge, Let), (lname_of_lident id, None), b)
(* Gallina inductive declarations *)
| cum = cumulativity_token; priv = private_token; f = finite_token;
indl = LIST1 inductive_definition SEP "with" ->
@@ -167,13 +177,13 @@ GEXTEND Gram
in
VernacInductive (cum, priv,f,indl)
| "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
- VernacFixpoint (None, recs)
+ VernacFixpoint (NoDischarge, recs)
| IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
- VernacFixpoint (Some Discharge, recs)
+ VernacFixpoint (DoDischarge, recs)
| "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
- VernacCoFixpoint (None, corecs)
+ VernacCoFixpoint (NoDischarge, corecs)
| IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
- VernacCoFixpoint (Some Discharge, corecs)
+ VernacCoFixpoint (DoDischarge, corecs)
| IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l
| IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l)
@@ -195,23 +205,23 @@ GEXTEND Gram
| IDENT "Property" -> Property ] ]
;
def_token:
- [ [ "Definition" -> (None, Definition)
- | IDENT "Example" -> (None, Example)
- | IDENT "SubClass" -> (None, SubClass) ] ]
+ [ [ "Definition" -> (NoDischarge,Definition)
+ | IDENT "Example" -> (NoDischarge,Example)
+ | IDENT "SubClass" -> (NoDischarge,SubClass) ] ]
;
assumption_token:
- [ [ "Hypothesis" -> (Some Discharge, Logical)
- | "Variable" -> (Some Discharge, Definitional)
- | "Axiom" -> (None, Logical)
- | "Parameter" -> (None, Definitional)
- | IDENT "Conjecture" -> (None, Conjectural) ] ]
+ [ [ "Hypothesis" -> (DoDischarge, Logical)
+ | "Variable" -> (DoDischarge, Definitional)
+ | "Axiom" -> (NoDischarge, Logical)
+ | "Parameter" -> (NoDischarge, Definitional)
+ | IDENT "Conjecture" -> (NoDischarge, Conjectural) ] ]
;
assumptions_token:
- [ [ IDENT "Hypotheses" -> ("Hypotheses", (Some Discharge, Logical))
- | IDENT "Variables" -> ("Variables", (Some Discharge, Definitional))
- | IDENT "Axioms" -> ("Axioms", (None, Logical))
- | IDENT "Parameters" -> ("Parameters", (None, Definitional))
- | IDENT "Conjectures" -> ("Conjectures", (None, Conjectural)) ] ]
+ [ [ 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 = INT; ")" -> InlineAt (int_of_string i)
@@ -617,37 +627,23 @@ 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
- VernacDefinition
- ((Some Global,CanonicalStructure),((Loc.tag s),None),d)
+ VernacDefinition ((NoDischarge,CanonicalStructure),((Loc.tag (Name s)),None),d)
(* Coercions *)
| IDENT "Coercion"; qid = global; d = def_body ->
let s = coerce_reference_to_id qid in
- VernacDefinition ((None,Coercion),((Loc.tag s),None),d)
- | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
- let s = coerce_reference_to_id qid in
- VernacDefinition ((Some Decl_kinds.Local,Coercion),((Loc.tag s),None),d)
- | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref;
- ":"; s = class_rawexpr; ">->"; t = class_rawexpr ->
- VernacIdentityCoercion (true, f, s, t)
+ VernacDefinition ((NoDischarge,Coercion),((Loc.tag (Name s)),None),d)
| IDENT "Identity"; IDENT "Coercion"; f = identref; ":";
s = class_rawexpr; ">->"; t = class_rawexpr ->
- VernacIdentityCoercion (false, f, s, t)
- | IDENT "Coercion"; IDENT "Local"; qid = global; ":";
- s = class_rawexpr; ">->"; t = class_rawexpr ->
- VernacCoercion (true, AN qid, s, t)
- | IDENT "Coercion"; IDENT "Local"; ntn = by_notation; ":";
- s = class_rawexpr; ">->"; t = class_rawexpr ->
- VernacCoercion (true, ByNotation ntn, s, t)
+ VernacIdentityCoercion (f, s, t)
| IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->";
t = class_rawexpr ->
- VernacCoercion (false, AN qid, s, t)
+ VernacCoercion (AN qid, s, t)
| IDENT "Coercion"; ntn = by_notation; ":"; s = class_rawexpr; ">->";
t = class_rawexpr ->
- VernacCoercion (false, ByNotation ntn, s, t)
+ VernacCoercion (ByNotation ntn, s, t)
| IDENT "Context"; c = binders ->
VernacContext c
@@ -831,7 +827,7 @@ GEXTEND Gram
command:
[ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l
- (* Hack! Should be in grammar_ext, but camlp4 factorize badly *)
+ (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *)
| IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":";
expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200";
info = hint_info ->
@@ -1106,11 +1102,11 @@ GEXTEND Gram
GLOBAL: syntax;
syntax:
- [ [ IDENT "Open"; local = obsolete_locality; IDENT "Scope"; sc = IDENT ->
- VernacOpenCloseScope (local,(true,sc))
+ [ [ IDENT "Open"; IDENT "Scope"; sc = IDENT ->
+ VernacOpenCloseScope (true,sc)
- | IDENT "Close"; local = obsolete_locality; IDENT "Scope"; sc = IDENT ->
- VernacOpenCloseScope (local,(false,sc))
+ | IDENT "Close"; IDENT "Scope"; sc = IDENT ->
+ VernacOpenCloseScope (false,sc)
| IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
VernacDelimiters (sc, Some key)
@@ -1120,32 +1116,31 @@ GEXTEND Gram
| IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with";
refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl)
- | IDENT "Infix"; local = obsolete_locality;
- op = ne_lstring; ":="; p = constr;
+ | IDENT "Infix"; op = ne_lstring; ":="; p = constr;
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
sc = OPT [ ":"; sc = IDENT -> sc ] ->
- VernacInfix (local,(op,modl),p,sc)
- | IDENT "Notation"; local = obsolete_locality; id = identref;
+ VernacInfix ((op,modl),p,sc)
+ | IDENT "Notation"; id = identref;
idl = LIST0 ident; ":="; c = constr; b = only_parsing ->
VernacSyntacticDefinition
- (id,(idl,c),local,b)
- | IDENT "Notation"; local = obsolete_locality; s = lstring; ":=";
+ (id,(idl,c),b)
+ | IDENT "Notation"; s = lstring; ":=";
c = constr;
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
sc = OPT [ ":"; sc = IDENT -> sc ] ->
- VernacNotation (local,c,(s,modl),sc)
+ VernacNotation (c,(s,modl),sc)
| IDENT "Format"; IDENT "Notation"; n = STRING; s = STRING; fmt = STRING ->
VernacNotationAddFormat (n,s,fmt)
| IDENT "Reserved"; IDENT "Infix"; s = ne_lstring;
l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] ->
let (loc,s) = s in
- VernacSyntaxExtension (true, false,((loc,"x '"^s^"' y"),l))
+ VernacSyntaxExtension (true,((loc,"x '"^s^"' y"),l))
- | IDENT "Reserved"; IDENT "Notation"; local = obsolete_locality;
+ | IDENT "Reserved"; IDENT "Notation";
s = ne_lstring;
l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
- -> VernacSyntaxExtension (false, local,(s,l))
+ -> VernacSyntaxExtension (false, (s,l))
(* "Print" "Grammar" should be here but is in "command" entry in order
to factorize with other "Print"-based vernac entries *)
@@ -1158,9 +1153,6 @@ GEXTEND Gram
Some (parse_compat_version s)
| -> None ] ]
;
- obsolete_locality:
- [ [ IDENT "Local" -> true | -> false ] ]
- ;
level:
[ [ IDENT "level"; n = natural -> NumLevel n
| IDENT "next"; IDENT "level" -> NextLevel ] ]
@@ -1182,6 +1174,8 @@ GEXTEND Gram
| x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at";
lev = level -> SetItemLevel (x::l,lev)
| x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev)
+ | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,Some lev)
+ | x = IDENT; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,None)
| x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ)
] ]
;
@@ -1189,7 +1183,20 @@ GEXTEND Gram
[ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference
| IDENT "bigint" -> ETBigint
| IDENT "binder" -> ETBinder true
+ | IDENT "constr"; n = OPT at_level; b = constr_as_binder_kind -> ETConstrAsBinder (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
] ]
;
+ at_level:
+ [ [ "at"; n = level -> n ] ]
+ ;
+ constr_as_binder_kind:
+ [ [ "as"; IDENT "ident" -> AsIdent
+ | "as"; IDENT "pattern" -> AsIdentOrPattern
+ | "as"; IDENT "strict"; IDENT "pattern" -> AsStrictPattern ] ]
+ ;
END
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 8e6a01aa3b..ddb26d7717 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -202,7 +202,7 @@ end = struct
end
-let camlp4_verbosity silent f x =
+let camlp5_verbosity silent f x =
let a = !warning_verbose in
warning_verbose := silent;
f x;
@@ -274,7 +274,7 @@ type ext_kind =
(** The list of extensions *)
-let camlp4_state = ref []
+let camlp5_state = ref []
(** Deletion *)
@@ -299,13 +299,13 @@ let grammar_delete e reinit (pos,rls) =
let grammar_extend e reinit ext =
let ext = of_coq_extend_statement ext in
let undo () = grammar_delete e reinit ext in
- let redo () = camlp4_verbosity false (uncurry (G.extend e)) ext in
- camlp4_state := ByEXTEND (undo, redo) :: !camlp4_state;
+ let redo () = camlp5_verbosity false (uncurry (G.extend e)) ext in
+ camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state;
redo ()
let grammar_extend_sync e reinit ext =
- camlp4_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp4_state;
- camlp4_verbosity false (uncurry (G.extend e)) (of_coq_extend_statement ext)
+ camlp5_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp5_state;
+ camlp5_verbosity false (uncurry (G.extend e)) (of_coq_extend_statement ext)
(** The apparent parser of Coq; encapsulate G to keep track
of the extensions. *)
@@ -315,20 +315,20 @@ module Gram =
include G
let extend e =
curry
- (fun ext ->
- camlp4_state :=
- (ByEXTEND ((fun () -> grammar_delete e None ext),
- (fun () -> uncurry (G.extend e) ext)))
- :: !camlp4_state;
- uncurry (G.extend e) ext)
+ (fun ext ->
+ camlp5_state :=
+ (ByEXTEND ((fun () -> grammar_delete e None ext),
+ (fun () -> uncurry (G.extend e) ext)))
+ :: !camlp5_state;
+ uncurry (G.extend e) ext)
let delete_rule e pil =
(* spiwack: if you use load an ML module which contains GDELETE_RULE
- in a section, God kills a kitty. As it would corrupt remove_grammars.
+ in a section, God kills a kitty. As it would corrupt remove_grammars.
There does not seem to be a good way to undo a delete rule. As deleting
- takes fewer arguments than extending. The production rule isn't returned
- by delete_rule. If we could retrieve the necessary information, then
- ByEXTEND provides just the framework we need to allow this in section.
- I'm not entirely sure it makes sense, but at least it would be more correct.
+ takes fewer arguments than extending. The production rule isn't returned
+ by delete_rule. If we could retrieve the necessary information, then
+ ByEXTEND provides just the framework we need to allow this in section.
+ I'm not entirely sure it makes sense, but at least it would be more correct.
*)
G.delete_rule e pil
end
@@ -340,18 +340,18 @@ module Gram =
let rec remove_grammars n =
if n>0 then
- (match !camlp4_state with
+ (match !camlp5_state with
| [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove.")
| ByGrammar (ExtendRule (g, reinit, ext)) :: t ->
grammar_delete g reinit (of_coq_extend_statement ext);
- camlp4_state := t;
+ camlp5_state := t;
remove_grammars (n-1)
| ByEXTEND (undo,redo)::t ->
undo();
- camlp4_state := t;
+ camlp5_state := t;
remove_grammars n;
redo();
- camlp4_state := ByEXTEND (undo,redo) :: !camlp4_state)
+ camlp5_state := ByEXTEND (undo,redo) :: !camlp5_state)
let make_rule r = [None, None, r]
@@ -503,8 +503,7 @@ module Vernac_ =
let gallina_ext = gec_vernac "gallina_ext"
let command = gec_vernac "command"
let syntax = gec_vernac "syntax_command"
- let vernac = gec_vernac "Vernac.vernac"
- let vernac_eoi = eoi_entry vernac
+ let vernac_control = gec_vernac "Vernac.vernac_control"
let rec_definition = gec_vernac "Vernac.rec_definition"
let red_expr = make_gen_entry utactic "red_expr"
let hint_info = gec_vernac "hint_info"
@@ -517,7 +516,7 @@ module Vernac_ =
let act_eoi = Gram.action (fun _ loc -> None) in
let rule = [
([ Symbols.stoken Tok.EOI ], act_eoi);
- ([ Symbols.snterm (Gram.Entry.obj vernac) ], act_vernac );
+ ([ Symbols.snterm (Gram.Entry.obj vernac_control) ], act_vernac );
] in
uncurry (Gram.extend main_entry) (None, make_rule rule)
@@ -611,8 +610,8 @@ let unfreeze (grams, lex) =
the lexer state should not be resetted, since it contains
keywords declared in g_*.ml4 *)
-let _ =
- Summary.declare_summary "GRAMMAR_LEXER"
+let parser_summary_tag =
+ Summary.declare_summary_tag "GRAMMAR_LEXER"
{ Summary.freeze_function = freeze;
Summary.unfreeze_function = unfreeze;
Summary.init_function = Summary.nop }
@@ -639,3 +638,15 @@ let () =
Grammar.register0 wit_constr (Constr.constr);
Grammar.register0 wit_red_expr (Vernac_.red_expr);
()
+
+(** Registering extra grammar *)
+
+type any_entry = AnyEntry : 'a Gram.entry -> any_entry
+
+let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty
+
+let register_grammars_by_name name grams =
+ grammar_names := String.Map.add name grams !grammar_names
+
+let find_grammars_by_name name =
+ String.Map.find name !grammar_names
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d17ccb0b41..accb51366b 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -124,7 +124,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e
|
| Egrammar.make_constr_prod_item
V
- Gramext.g_symbol list which is sent to camlp4
+ Gramext.g_symbol list which is sent to camlp5
For user level tactic notations, dynamic addition of new rules is
also done in several steps:
@@ -161,9 +161,9 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e
*)
-(** Temporarily activate camlp4 verbosity *)
+(** Temporarily activate camlp5 verbosity *)
-val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit
+val camlp5_verbosity : bool -> ('a -> unit) -> 'a -> unit
(** Parse a string *)
@@ -251,9 +251,8 @@ module Vernac_ :
val gallina_ext : vernac_expr Gram.entry
val command : vernac_expr Gram.entry
val syntax : vernac_expr Gram.entry
- val vernac : vernac_expr Gram.entry
+ val vernac_control : vernac_control Gram.entry
val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry
- val vernac_eoi : vernac_expr Gram.entry
val noedit_mode : vernac_expr Gram.entry
val command_entry : vernac_expr Gram.entry
val red_expr : raw_red_expr Gram.entry
@@ -261,7 +260,7 @@ module Vernac_ :
end
(** The main entry: reads an optional vernac command *)
-val main_entry : (Loc.t * vernac_expr) option Gram.entry
+val main_entry : (Loc.t * vernac_control) option Gram.entry
(** Handling of the proof mode entry *)
val get_command_entry : unit -> vernac_expr Gram.entry
@@ -313,3 +312,13 @@ val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
(** Location Utils *)
val to_coqloc : Ploc.t -> Loc.t
val (!@) : Ploc.t -> Loc.t
+
+type frozen_t
+val parser_summary_tag : frozen_t Summary.Dyn.tag
+
+(** Registering grammars by name *)
+
+type any_entry = AnyEntry : 'a Gram.entry -> any_entry
+
+val register_grammars_by_name : string -> any_entry list -> unit
+val find_grammars_by_name : string -> any_entry list
diff --git a/parsing/tok.ml b/parsing/tok.ml
index 0917e8d6dc..fafad2779c 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -60,7 +60,7 @@ let match_keyword kwd = function
| KEYWORD kwd' when kwd = kwd' -> true
| _ -> false
-(* Needed to fix Camlp4 signature.
+(* Needed to fix Camlp5 signature.
Cannot use Pp because of silly Tox -> Compat -> Pp dependency *)
let print ppf tok = Format.pp_print_string ppf (to_string tok)
diff --git a/parsing/tok.mli b/parsing/tok.mli
index 59a79dcd22..162310e2a1 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -22,7 +22,7 @@ type t =
val equal : t -> t -> bool
val extract_string : t -> string
val to_string : t -> string
-(* Needed to fit Camlp4 signature *)
+(* Needed to fit Camlp5 signature *)
val print : Format.formatter -> t -> unit
val match_keyword : string -> t -> bool
(** for camlp5 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 01:02:11 +0000