aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/compat.ml471
-rw-r--r--parsing/egramcoq.ml38
-rw-r--r--parsing/egramcoq.mli4
-rw-r--r--parsing/egramml.ml73
-rw-r--r--parsing/egramml.mli18
-rw-r--r--parsing/entry.ml63
-rw-r--r--parsing/entry.mli50
-rw-r--r--parsing/lexer.ml411
-rw-r--r--parsing/parsing.mllib1
-rw-r--r--parsing/pcoq.ml (renamed from parsing/pcoq.ml4)389
-rw-r--r--parsing/pcoq.mli81
11 files changed, 514 insertions, 285 deletions
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index eba1d2b8f..4208fd364 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -238,6 +238,69 @@ end
END
+(** Some definitions are grammar-specific in Camlp4, so we use a functor to
+ depend on it while taking a dummy argument in Camlp5. *)
+
+module GramextMake (G : GrammarSig) :
+sig
+ val stoken : Tok.t -> G.symbol
+ val sself : G.symbol
+ val snext : G.symbol
+ val slist0 : G.symbol -> G.symbol
+ val slist0sep : G.symbol * G.symbol -> G.symbol
+ val slist1 : G.symbol -> G.symbol
+ val slist1sep : G.symbol * G.symbol -> G.symbol
+ val sopt : G.symbol -> G.symbol
+ val snterml : G.internal_entry * string -> G.symbol
+ val snterm : G.internal_entry -> G.symbol
+ val snterml_level : G.symbol -> string
+end =
+struct
+
+IFDEF CAMLP5 THEN
+ let stoken tok =
+ let pattern = match tok with
+ | Tok.KEYWORD s -> "", s
+ | Tok.IDENT s -> "IDENT", s
+ | Tok.METAIDENT s -> "METAIDENT", s
+ | Tok.PATTERNIDENT s -> "PATTERNIDENT", s
+ | Tok.FIELD s -> "FIELD", s
+ | Tok.INT s -> "INT", s
+ | Tok.STRING s -> "STRING", s
+ | Tok.LEFTQMARK -> "LEFTQMARK", ""
+ | Tok.BULLET s -> "BULLET", s
+ | Tok.EOI -> "EOI", ""
+ in
+ Gramext.Stoken pattern
+ELSE
+ module Gramext = G
+ let stoken tok = match tok with
+ | Tok.KEYWORD s -> Gramext.Skeyword s
+ | tok -> Gramext.Stoken ((=) tok, G.Token.to_string tok)
+END
+
+IFDEF CAMLP5_6_00 THEN
+ let slist0sep (x, y) = Gramext.Slist0sep (x, y, false)
+ let slist1sep (x, y) = Gramext.Slist1sep (x, y, false)
+ELSE
+ let slist0sep (x, y) = Gramext.Slist0sep (x, y)
+ let slist1sep (x, y) = Gramext.Slist1sep (x, y)
+END
+
+ let snterml (x, y) = Gramext.Snterml (x, y)
+ let snterm x = Gramext.Snterm x
+ let sself = Gramext.Sself
+ let snext = Gramext.Snext
+ let slist0 x = Gramext.Slist0 x
+ let slist1 x = Gramext.Slist1 x
+ let sopt x = Gramext.Sopt x
+
+ let snterml_level = function
+ | Gramext.Snterml (_, l) -> l
+ | _ -> failwith "snterml_level"
+
+end
+
(** Misc functional adjustments *)
@@ -323,3 +386,11 @@ let qualified_name loc path name =
let path = List.fold_right fold path (Ast.IdLid (loc, name)) in
Ast.ExId (loc, path)
END
+
+IFDEF CAMLP5 THEN
+let warning_verbose = Gramext.warning_verbose
+ELSE
+(* TODO: this is a workaround, since there isn't such
+ [warning_verbose] in new camlp4. *)
+let warning_verbose = ref true
+END
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 01194c60d..84736f8ab 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -167,10 +167,9 @@ let rec make_constr_prod_item assoc from forpat = function
[]
let prepare_empty_levels forpat (pos,p4assoc,name,reinit) =
- let entry =
- if forpat then weaken_entry Constr.pattern
- else weaken_entry Constr.operconstr in
- grammar_extend entry reinit (pos,[(name, p4assoc, [])])
+ let empty = (pos, [(name, p4assoc, [])]) in
+ if forpat then grammar_extend Constr.pattern reinit empty
+ else grammar_extend Constr.operconstr reinit empty
let pure_sublevels level symbs =
let filter s =
@@ -189,13 +188,10 @@ let extend_constr (entry,level) (n,assoc) mkact forpat rules =
let symbs = make_constr_prod_item assoc n forpat pt in
let pure_sublevels = pure_sublevels level symbs in
let needed_levels = register_empty_levels forpat pure_sublevels in
- let map_level (pos, ass1, name, ass2) =
- (Option.map of_coq_position pos, Option.map of_coq_assoc ass1, name, ass2) in
- let needed_levels = List.map map_level needed_levels in
let pos,p4assoc,name,reinit = find_position forpat assoc level in
let nb_decls = List.length needed_levels + 1 in
List.iter (prepare_empty_levels forpat) needed_levels;
- grammar_extend entry reinit (Option.map of_coq_position pos,
+ unsafe_grammar_extend entry reinit (Option.map of_coq_position pos,
[(name, Option.map of_coq_assoc p4assoc, [symbs, mkact pt])]);
nb_decls) 0 rules
@@ -233,11 +229,11 @@ let extend_constr_notation ng =
let get_tactic_entry n =
if Int.equal n 0 then
- weaken_entry Tactic.simple_tactic, None
+ Tactic.simple_tactic, None
else if Int.equal n 5 then
- weaken_entry Tactic.binder_tactic, None
+ Tactic.binder_tactic, None
else if 1<=n && n<5 then
- weaken_entry Tactic.tactic_expr, Some (Extend.Level (string_of_int n))
+ Tactic.tactic_expr, Some (Extend.Level (string_of_int n))
else
error ("Invalid Tactic Notation level: "^(string_of_int n)^".")
@@ -246,22 +242,26 @@ let get_tactic_entry n =
type tactic_grammar = {
tacgram_level : int;
- tacgram_prods : grammar_prod_item list;
+ tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list;
}
type all_grammar_command =
| Notation of Notation.level * notation_grammar
| TacticGrammar of KerName.t * tactic_grammar
- | MLTacticGrammar of ml_tactic_name * grammar_prod_item list list
+ | MLTacticGrammar of ml_tactic_name * Tacexpr.raw_tactic_expr grammar_prod_item list list
(** ML Tactic grammar extensions *)
let add_ml_tactic_entry name prods =
- let entry = weaken_entry Tactic.simple_tactic in
- let mkact loc l : raw_tactic_expr = Tacexpr.TacML (loc, name, List.map snd l) in
- let rules = List.map (make_rule mkact) prods in
+ let entry = Tactic.simple_tactic in
+ let mkact i loc l : raw_tactic_expr =
+ let open Tacexpr in
+ let entry = { mltac_name = name; mltac_index = i } in
+ TacML (loc, entry, List.map snd l)
+ in
+ let rules = List.map_i (fun i p -> make_rule (mkact i) p) 0 prods in
synchronize_level_positions ();
- grammar_extend entry None (None ,[(None, None, List.rev rules)]);
+ grammar_extend entry None (None, [(None, None, List.rev rules)]);
1
(* Declaration of the tactic grammar rule *)
@@ -281,7 +281,7 @@ let add_tactic_entry kn tg =
in
let rules = make_rule mkact tg.tacgram_prods in
synchronize_level_positions ();
- grammar_extend entry None (Option.map of_coq_position pos,[(None, None, List.rev [rules])]);
+ grammar_extend entry None (pos, [(None, None, List.rev [rules])]);
1
let (grammar_state : (int * all_grammar_command) list ref) = ref []
@@ -374,7 +374,7 @@ let create_ltac_quotation name cast wit e =
let rule = [
gram_token_of_string name;
gram_token_of_string ":";
- symbol_of_prod_entry_key (Agram (Gram.Entry.name e));
+ symbol_of_prod_entry_key (Aentry (name_of_entry e));
] in
let action v _ _ loc =
let loc = !@loc in
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 2b0f7da8c..cdd5fbd0f 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -38,7 +38,7 @@ type notation_grammar = {
type tactic_grammar = {
tacgram_level : int;
- tacgram_prods : grammar_prod_item list;
+ tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list;
}
(** {5 Adding notations} *)
@@ -50,7 +50,7 @@ val extend_tactic_grammar : KerName.t -> tactic_grammar -> unit
(** Add a tactic notation rule to the parsing system. This produces a TacAlias
tactic with the provided kernel name. *)
-val extend_ml_tactic_grammar : Tacexpr.ml_tactic_name -> grammar_prod_item list list -> unit
+val extend_ml_tactic_grammar : Tacexpr.ml_tactic_name -> Tacexpr.raw_tactic_expr grammar_prod_item list list -> unit
(** Add a ML tactic notation rule to the parsing system. This produces a
TacML tactic with the provided string as name. *)
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index 8fe03b363..984027b81 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -13,35 +13,58 @@ open Pcoq
open Genarg
open Vernacexpr
-(** Making generic actions in type generic_argument *)
-
-let make_generic_action
- (f:Loc.t -> ('b * raw_generic_argument) list -> 'a) pil =
- let rec make env = function
- | [] ->
- Gram.action (fun loc -> f (to_coqloc loc) env)
- | None :: tl -> (* parse a non-binding item *)
- Gram.action (fun _ -> make env tl)
- | Some (p, t) :: tl -> (* non-terminal *)
- Gram.action (fun v -> make ((p, Unsafe.inj t v) :: env) tl) in
- make [] (List.rev pil)
-
(** Grammar extensions declared at ML level *)
-type grammar_prod_item =
+type 's grammar_prod_item =
| GramTerminal of string
- | GramNonTerminal of
- Loc.t * argument_type * prod_entry_key * Id.t option
+ | GramNonTerminal :
+ Loc.t * 'a raw_abstract_argument_type * ('s, 'a) entry_key * Id.t option -> 's grammar_prod_item
+
+type 'a ty_arg = Id.t * ('a -> raw_generic_argument)
+
+type ('self, _, 'r) ty_rule =
+| TyStop : ('self, 'r, 'r) ty_rule
+| TyNext : ('self, 'a, 'r) ty_rule * ('self, 'b) Extend.symbol * 'b ty_arg option ->
+ ('self, 'b -> 'a, 'r) ty_rule
+
+type ('self, 'r) any_ty_rule =
+| AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule
+
+let rec ty_rule_of_gram = function
+| [] -> AnyTyRule TyStop
+| GramTerminal s :: rem ->
+ let AnyTyRule rem = ty_rule_of_gram rem in
+ let tok = Atoken (Lexer.terminal s) in
+ let r = TyNext (rem, tok, None) in
+ AnyTyRule r
+| GramNonTerminal (_, t, tok, idopt) :: rem ->
+ let AnyTyRule rem = ty_rule_of_gram rem in
+ let inj = match idopt with
+ | None -> None
+ | Some id -> Some (id, fun obj -> Genarg.in_gen t obj)
+ in
+ let r = TyNext (rem, tok, inj) in
+ AnyTyRule r
+
+let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) Extend.rule = function
+| TyStop -> Extend.Stop
+| TyNext (rem, tok, _) -> Extend.Next (ty_erase rem, tok)
+
+type 'r gen_eval = Loc.t -> (Id.t * raw_generic_argument) list -> 'r
-let make_prod_item = function
- | GramTerminal s -> (gram_token_of_string s, None)
- | GramNonTerminal (_,t,e,po) ->
- (symbol_of_prod_entry_key e, Option.map (fun p -> (p,t)) po)
+let rec ty_eval : type s a r. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> a = function
+| TyStop -> fun f loc -> f loc []
+| TyNext (rem, tok, None) -> fun f _ -> ty_eval rem f
+| TyNext (rem, tok, Some (id, inj)) -> fun f x ->
+ let f loc args = f loc ((id, inj x) :: args) in
+ ty_eval rem f
-let make_rule mkact pt =
- let (symbs,ntl) = List.split (List.map make_prod_item pt) in
- let act = make_generic_action mkact ntl in
- (symbs, act)
+let make_rule f prod =
+ let AnyTyRule ty_rule = ty_rule_of_gram (List.rev prod) in
+ let symb = ty_erase ty_rule in
+ let f loc l = f loc (List.rev l) in
+ let act = ty_eval ty_rule f in
+ Extend.Rule (symb, act)
(** Vernac grammar extensions *)
@@ -60,4 +83,4 @@ let extend_vernac_command_grammar s nt gl =
vernac_exts := (s,gl) :: !vernac_exts;
let mkact loc l = VernacExtend (s,List.map snd l) in
let rules = [make_rule mkact gl] in
- maybe_uncurry (Gram.extend nt) (None,[(None, None, List.rev rules)])
+ grammar_extend nt None (None, [None, None, rules])
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
index 9ebb5b83b..e3ae4e011 100644
--- a/parsing/egramml.mli
+++ b/parsing/egramml.mli
@@ -6,24 +6,26 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Vernacexpr
+
(** Mapping of grammar productions to camlp4 actions. *)
(** This is the part specific to vernac extensions.
For the Coq-level Notation and Tactic Notation, see Egramcoq. *)
-type grammar_prod_item =
+type 's grammar_prod_item =
| GramTerminal of string
- | GramNonTerminal of Loc.t * Genarg.argument_type *
- Pcoq.prod_entry_key * Names.Id.t option
+ | GramNonTerminal : Loc.t * 'a Genarg.raw_abstract_argument_type *
+ ('s, 'a) Pcoq.entry_key * Names.Id.t option -> 's grammar_prod_item
val extend_vernac_command_grammar :
- Vernacexpr.extend_name -> Vernacexpr.vernac_expr Pcoq.Gram.entry option ->
- grammar_prod_item list -> unit
+ Vernacexpr.extend_name -> vernac_expr Pcoq.Gram.entry option ->
+ vernac_expr grammar_prod_item list -> unit
-val get_extend_vernac_rule : Vernacexpr.extend_name -> grammar_prod_item list
+val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list
(** Utility function reused in Egramcoq : *)
val make_rule :
- (Loc.t -> (Names.Id.t * Genarg.raw_generic_argument) list -> 'b) ->
- grammar_prod_item list -> Pcoq.Gram.symbol list * Pcoq.Gram.action
+ (Loc.t -> (Names.Id.t * Genarg.raw_generic_argument) list -> 'a) ->
+ 'a grammar_prod_item list -> 'a Extend.production_rule
diff --git a/parsing/entry.ml b/parsing/entry.ml
new file mode 100644
index 000000000..97d601320
--- /dev/null
+++ b/parsing/entry.ml
@@ -0,0 +1,63 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Errors
+open Util
+
+type 'a t = string * string
+
+type repr =
+| Static of string * string
+| Dynamic of string
+
+type universe = string
+
+(* The univ_tab is not part of the state. It contains all the grammars that
+ exist or have existed before in the session. *)
+
+let univ_tab = (Hashtbl.create 7 : (string, unit) Hashtbl.t)
+
+let create_univ s =
+ Hashtbl.add univ_tab s (); s
+
+let univ_name s = s
+
+let uprim = create_univ "prim"
+let uconstr = create_univ "constr"
+let utactic = create_univ "tactic"
+let uvernac = create_univ "vernac"
+
+let get_univ s =
+ try
+ Hashtbl.find univ_tab s; s
+ with Not_found ->
+ anomaly (Pp.str ("Unknown grammar universe: "^s))
+
+(** Entries are registered with a unique name *)
+
+let entries = ref String.Set.empty
+
+let create u name =
+ let uname = u ^ ":" ^ name in
+ let () =
+ if String.Set.mem uname !entries then
+ anomaly (Pp.str ("Entry " ^ uname ^ " already defined"))
+ in
+ let () = entries := String.Set.add uname !entries in
+ (u, name)
+
+let dynamic name = ("", name)
+
+let unsafe_of_name (u, s) =
+ let uname = u ^ ":" ^ s in
+ assert (String.Set.mem uname !entries);
+ (u, s)
+
+let repr = function
+| ("", u) -> Dynamic u
+| (u, s) -> Static (u, s)
diff --git a/parsing/entry.mli b/parsing/entry.mli
new file mode 100644
index 000000000..6854a5cb4
--- /dev/null
+++ b/parsing/entry.mli
@@ -0,0 +1,50 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Typed grammar entries *)
+
+type 'a t
+(** Typed grammar entries. We need to defined them here so that they are
+ marshallable and defined before the Pcoq.Gram module. They are basically
+ unique names made of a universe and an entry name. They should be kept
+ synchronized with the {!Pcoq} entries though. *)
+
+type repr =
+| Static of string * string
+| Dynamic of string
+(** Representation of entries. *)
+
+(** Table of Coq statically defined grammar entries *)
+
+type universe
+
+(** There are four predefined universes: "prim", "constr", "tactic", "vernac" *)
+
+val get_univ : string -> universe
+val univ_name : universe -> string
+
+val uprim : universe
+val uconstr : universe
+val utactic : universe
+val uvernac : universe
+
+(** {5 Uniquely defined entries} *)
+
+val create : universe -> string -> 'a t
+(** Create an entry. They should be synchronized with the entries defined in
+ {!Pcoq}. *)
+
+(** {5 Meta-programming} *)
+
+val dynamic : string -> 'a t
+(** Dynamic entries. They refer to entries defined in the code source and may
+ only be used in meta-programming definitions from the grammar directory. *)
+
+val repr : 'a t -> repr
+
+val unsafe_of_name : (string * string) -> 'a t
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index c6d5f3b92..23bd74da9 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -8,7 +8,6 @@
open Pp
open Util
-open Compat
open Tok
(* Dictionaries: trees annotated with string options, each node being a map
@@ -565,7 +564,7 @@ let loct_add loct i loc = Hashtbl.add loct i loc
let current_location_table = ref (loct_create ())
-type location_table = (int, CompatLoc.t) Hashtbl.t
+type location_table = (int, Compat.CompatLoc.t) Hashtbl.t
let location_table () = !current_location_table
let restore_location_table t = current_location_table := t
@@ -602,7 +601,7 @@ let func cs =
Stream.from
(fun i ->
let (tok, loc) = next_token cs in
- loct_add loct i (make_loc loc); Some tok)
+ loct_add loct i (Compat.make_loc loc); Some tok)
in
current_location_table := loct;
(ts, loct_func loct)
@@ -622,10 +621,10 @@ ELSE (* official camlp4 for ocaml >= 3.10 *)
module M_ = Camlp4.ErrorHandler.Register (Error)
-module Loc = CompatLoc
+module Loc = Compat.CompatLoc
module Token = struct
include Tok (* Cf. tok.ml *)
- module Loc = CompatLoc
+ module Loc = Compat.CompatLoc
module Error = Camlp4.Struct.EmptyError
module Filter = struct
type token_filter = (Tok.t * Loc.t) Stream.t -> (Tok.t * Loc.t) Stream.t
@@ -643,7 +642,7 @@ let mk () _init_loc(*FIXME*) cs =
let rec self =
parser i
[< (tok, loc) = next_token; s >] ->
- let loc = make_loc loc in
+ let loc = Compat.make_loc loc in
loct_add loct i loc;
[< '(tok, loc); self s >]
| [< >] -> [< >]
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index a0cb83193..024d8607f 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,6 +1,7 @@
Tok
Compat
Lexer
+Entry
Pcoq
Egramml
Egramcoq
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml
index 2e47e07a3..4565b87a0 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml
@@ -20,37 +20,11 @@ open Tok (* necessary for camlp4 *)
module G = GrammarMake (Lexer)
-(* TODO: this is a workaround, since there isn't such
- [warning_verbose] in new camlp4. In camlp5, this ref
- gets hidden by [Gramext.warning_verbose] *)
-let warning_verbose = ref true
-
-IFDEF CAMLP5 THEN
-open Gramext
-ELSE
-open PcamlSig.Grammar
-open G
-END
-
-(** Compatibility with Camlp5 6.x *)
-
-IFDEF CAMLP5_6_00 THEN
-let slist0sep x y = Slist0sep (x, y, false)
-let slist1sep x y = Slist1sep (x, y, false)
-ELSE
-let slist0sep x y = Slist0sep (x, y)
-let slist1sep x y = Slist1sep (x, y)
-END
-
-let gram_token_of_token tok =
-IFDEF CAMLP5 THEN
- Stoken (Tok.to_pattern tok)
-ELSE
- match tok with
- | KEYWORD s -> Skeyword s
- | tok -> Stoken ((=) tok, to_string tok)
-END
+let warning_verbose = Compat.warning_verbose
+module Symbols = GramextMake(G)
+
+let gram_token_of_token = Symbols.stoken
let gram_token_of_string s = gram_token_of_token (Lexer.terminal s)
let camlp4_verbosity silent f x =
@@ -62,26 +36,6 @@ let camlp4_verbosity silent f x =
let camlp4_verbose f x = camlp4_verbosity (Flags.is_verbose ()) f x
-(** General entry keys *)
-
-(** This intermediate abstract representation of entries can
- both be reified into mlexpr for the ML extensions and
- dynamically interpreted as entries for the Coq level extensions
-*)
-
-type prod_entry_key =
- | Alist1 of prod_entry_key
- | Alist1sep of prod_entry_key * string
- | Alist0 of prod_entry_key
- | Alist0sep of prod_entry_key * string
- | Aopt of prod_entry_key
- | Amodifiers of prod_entry_key
- | Aself
- | Anext
- | Atactic of int
- | Agram of string
- | Aentry of string * string
-
(** [grammar_object] is the superclass of all grammar entries *)
module type Gramobj =
@@ -98,7 +52,6 @@ end
(** Grammar entries with associated types *)
-type entry_type = argument_type
type grammar_object = Gramobj.grammar_object
type typed_entry = argument_type * grammar_object G.entry
let in_typed_entry t e = (t,Gramobj.weaken_entry e)
@@ -106,6 +59,29 @@ let type_of_typed_entry (t,e) = t
let object_of_typed_entry (t,e) = e
let weaken_entry x = Gramobj.weaken_entry x
+(** General entry keys *)
+
+(** This intermediate abstract representation of entries can
+ both be reified into mlexpr for the ML extensions and
+ dynamically interpreted as entries for the Coq level extensions
+*)
+
+type ('self, 'a) entry_key = ('self, 'a) Extend.symbol =
+| Atoken : Tok.t -> ('self, string) entry_key
+| Alist1 : ('self, 'a) entry_key -> ('self, 'a list) entry_key
+| Alist1sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key
+| Alist0 : ('self, 'a) entry_key -> ('self, 'a list) entry_key
+| Alist0sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key
+| Aopt : ('self, 'a) entry_key -> ('self, 'a option) entry_key
+| Amodifiers : ('self, 'a) entry_key -> ('self, 'a list) entry_key
+| Aself : ('self, 'self) entry_key
+| Anext : ('self, 'self) entry_key
+| Aentry : 'a Entry.t -> ('self, 'a) entry_key
+| Aentryl : 'a Entry.t * int -> ('self, 'a) entry_key
+
+type 's entry_name = EntryName :
+ 'a raw_abstract_argument_type * ('s, 'a) entry_key -> 's entry_name
+
module type Gramtypes =
sig
val inGramObj : 'a raw_abstract_argument_type -> 'a G.entry -> typed_entry
@@ -158,7 +134,10 @@ let grammar_delete e reinit (pos,rls) =
(List.rev rls);
match reinit with
| Some (a,ext) ->
- let lev = match pos with Some (Level n) -> n | _ -> assert false in
+ let lev = match Option.map Compat.to_coq_position pos with
+ | Some (Level n) -> n
+ | _ -> assert false
+ in
maybe_uncurry (G.extend e) (Some ext, [Some lev,Some a,[]])
| None -> ()
@@ -190,7 +169,7 @@ module Gram =
(** This extension command is used by the Grammar constr *)
-let grammar_extend e reinit ext =
+let unsafe_grammar_extend e reinit ext =
camlp4_state := ByGrammar (weaken_entry e,reinit,ext) :: !camlp4_state;
camlp4_verbose (maybe_uncurry (G.extend e)) ext
@@ -215,22 +194,22 @@ let rec remove_grammars n =
redo();
camlp4_state := ByEXTEND (undo,redo) :: !camlp4_state)
+let make_rule r = [None, None, r]
+
(** An entry that checks we reached the end of the input. *)
let eoi_entry en =
let e = Gram.entry_create ((Gram.Entry.name en) ^ "_eoi") in
- GEXTEND Gram
- e: [ [ x = en; EOI -> x ] ]
- ;
- END;
+ let symbs = [Symbols.snterm (Gram.Entry.obj en); Symbols.stoken Tok.EOI] in
+ let act = Gram.action (fun _ x loc -> x) in
+ maybe_uncurry (Gram.extend e) (None, make_rule [symbs, act]);
e
let map_entry f en =
let e = Gram.entry_create ((Gram.Entry.name en) ^ "_map") in
- GEXTEND Gram
- e: [ [ x = en -> f x ] ]
- ;
- END;
+ let symbs = [Symbols.snterm (Gram.Entry.obj en)] in
+ let act = Gram.action (fun x loc -> f x) in
+ maybe_uncurry (Gram.extend e) (None, make_rule [symbs, act]);
e
(* Parse a string, does NOT check if the entire string was read
@@ -239,45 +218,58 @@ let map_entry f en =
let parse_string f x =
let strm = Stream.of_string x in Gram.entry_parse f (Gram.parsable strm)
-type gram_universe = string * (string, typed_entry) Hashtbl.t
+type gram_universe = Entry.universe
let trace = ref false
-(* The univ_tab is not part of the state. It contains all the grammars that
- exist or have existed before in the session. *)
-
-let univ_tab = (Hashtbl.create 7 : (string, gram_universe) Hashtbl.t)
-
-let create_univ s =
- let u = s, Hashtbl.create 29 in Hashtbl.add univ_tab s u; u
+let uprim = Entry.uprim
+let uconstr = Entry.uconstr
+let utactic = Entry.utactic
+let uvernac = Entry.uvernac
+let get_univ = Entry.get_univ
-let uprim = create_univ "prim"
-let uconstr = create_univ "constr"
-let utactic = create_univ "tactic"
-let uvernac = create_univ "vernac"
+let utables : (string, (string, typed_entry) Hashtbl.t) Hashtbl.t =
+ Hashtbl.create 97
-let get_univ s =
- try
- Hashtbl.find univ_tab s
+let get_utable u =
+ let u = Entry.univ_name u in
+ try Hashtbl.find utables u
with Not_found ->
- anomaly (Pp.str ("Unknown grammar universe: "^s))
-
-let get_entry (u, utab) s = Hashtbl.find utab s
-
-let new_entry etyp (u, utab) s =
- if !trace then (Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr);
- let ename = u ^ ":" ^ s in
+ let table = Hashtbl.create 97 in
+ Hashtbl.add utables u table;
+ table
+
+let get_entry u s =
+ let utab = get_utable u in
+ Hashtbl.find utab s
+
+let get_typed_entry e =
+ let (u, s) = match Entry.repr e with
+ | Entry.Dynamic _ -> assert false
+ | Entry.Static (u, s) -> (u, s)
+ in
+ let u = Entry.get_univ u in
+ get_entry u s
+
+let new_entry etyp u s =
+ let utab = get_utable u in
+ let uname = Entry.univ_name u in
+ if !trace then (Printf.eprintf "[Creating entry %s:%s]\n" uname s; flush stderr);
+ let _ = Entry.create u s in
+ let ename = uname ^ ":" ^ s in
let e = in_typed_entry etyp (Gram.entry_create ename) in
Hashtbl.add utab s e; e
-let create_entry (u, utab) s etyp =
+let create_entry u s etyp =
+ let utab = get_utable u in
try
let e = Hashtbl.find utab s in
+ let u = Entry.univ_name u in
if not (argument_type_eq (type_of_typed_entry e) etyp) then
failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists with another type");
e
with Not_found ->
- new_entry etyp (u, utab) s
+ new_entry etyp u s
let create_constr_entry s =
outGramObj (rawwit wit_constr) (create_entry uconstr s ConstrArgType)
@@ -288,8 +280,11 @@ let create_generic_entry s wit =
(* [make_gen_entry] builds entries extensible by giving its name (a string) *)
(* For entries extensible only via the ML name, Gram.entry_create is enough *)
-let make_gen_entry (u,univ) rawwit s =
- let e = Gram.entry_create (u ^ ":" ^ s) in
+let make_gen_entry u rawwit s =
+ let univ = get_utable u in
+ let uname = Entry.univ_name u in
+ let e = Gram.entry_create (uname ^ ":" ^ s) in
+ let _ = Entry.create u s in
Hashtbl.add univ s (inGramObj rawwit e); e
(* Initial grammar entries *)
@@ -377,7 +372,7 @@ module Tactic =
make_gen_entry utactic (rawwit wit_bindings) "bindings"
let hypident = Gram.entry_create "hypident"
let constr_may_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval"
- let constr_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval"
+ let constr_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_eval"
let uconstr =
make_gen_entry utactic (rawwit wit_uconstr) "uconstr"
let quantified_hypothesis =
@@ -392,8 +387,8 @@ module Tactic =
(* Main entries for ltac *)
let tactic_arg = Gram.entry_create "tactic:tactic_arg"
- let tactic_expr = Gram.entry_create "tactic:tactic_expr"
- let binder_tactic = Gram.entry_create "tactic:binder_tactic"
+ let tactic_expr = make_gen_entry utactic (rawwit wit_tactic) "tactic_expr"
+ let binder_tactic = make_gen_entry utactic (rawwit wit_tactic) "binder_tactic"
let tactic = make_gen_entry utactic (rawwit wit_tactic) "tactic"
@@ -420,11 +415,14 @@ module Vernac_ =
(* Main vernac entry *)
let main_entry = Gram.entry_create "vernac"
- GEXTEND Gram
- main_entry:
- [ [ a = vernac -> Some (!@loc, a) | EOI -> None ] ]
- ;
- END
+ let () =
+ let act_vernac = Gram.action (fun v loc -> Some (!@loc, v)) in
+ 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 );
+ ] in
+ maybe_uncurry (Gram.extend main_entry) (None, make_rule rule)
end
@@ -679,77 +677,85 @@ let make_sep_rules tkl =
let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
if is_binder_level from typ then
if forpat then
- Snterml (Gram.Entry.obj Constr.pattern,"200")
+ Symbols.snterml (Gram.Entry.obj Constr.pattern,"200")
else
- Snterml (Gram.Entry.obj Constr.operconstr,"200")
+ Symbols.snterml (Gram.Entry.obj Constr.operconstr,"200")
else if is_self from typ then
- Sself
+ Symbols.sself
else
match typ with
| ETConstrList (typ',[]) ->
- Slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
+ Symbols.slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
| ETConstrList (typ',tkl) ->
- slist1sep
- (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
- (make_sep_rules tkl)
+ Symbols.slist1sep
+ (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'),
+ make_sep_rules tkl)
| ETBinderList (false,[]) ->
- Slist1
+ Symbols.slist1
(symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false))
| ETBinderList (false,tkl) ->
- slist1sep
- (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false))
- (make_sep_rules tkl)
+ Symbols.slist1sep
+ (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false),
+ make_sep_rules tkl)
| _ ->
match interp_constr_prod_entry_key assoc from forpat typ with
- | (eobj,None,_) -> Snterm (Gram.Entry.obj eobj)
- | (eobj,Some None,_) -> Snext
+ | (eobj,None,_) -> Symbols.snterm (Gram.Entry.obj eobj)
+ | (eobj,Some None,_) -> Symbols.snext
| (eobj,Some (Some (lev,cur)),_) ->
- Snterml (Gram.Entry.obj eobj,constr_level lev)
+ Symbols.snterml (Gram.Entry.obj eobj,constr_level lev)
(** Binding general entry keys to symbol *)
-let rec symbol_of_prod_entry_key = function
- | Alist1 s -> Slist1 (symbol_of_prod_entry_key s)
+let rec symbol_of_prod_entry_key : type s a. (s, a) entry_key -> _ = function
+ | Atoken t -> Symbols.stoken t
+ | Alist1 s -> Symbols.slist1 (symbol_of_prod_entry_key s)
| Alist1sep (s,sep) ->
- slist1sep (symbol_of_prod_entry_key s) (gram_token_of_string sep)
- | Alist0 s -> Slist0 (symbol_of_prod_entry_key s)
+ Symbols.slist1sep (symbol_of_prod_entry_key s, gram_token_of_string sep)
+ | Alist0 s -> Symbols.slist0 (symbol_of_prod_entry_key s)
| Alist0sep (s,sep) ->
- slist0sep (symbol_of_prod_entry_key s) (gram_token_of_string sep)
- | Aopt s -> Sopt (symbol_of_prod_entry_key s)
+ Symbols.slist0sep (symbol_of_prod_entry_key s, gram_token_of_string sep)
+ | Aopt s -> Symbols.sopt (symbol_of_prod_entry_key s)
| Amodifiers s ->
Gram.srules'
[([], Gram.action (fun _loc -> []));
([gram_token_of_string "(";
- slist1sep (symbol_of_prod_entry_key s) (gram_token_of_string ",");
+ Symbols.slist1sep (symbol_of_prod_entry_key s, gram_token_of_string ",");
gram_token_of_string ")"],
Gram.action (fun _ l _ _loc -> l))]
- | Aself -> Sself
- | Anext -> Snext
- | Atactic 5 -> Snterm (Gram.Entry.obj Tactic.binder_tactic)
- | Atactic n ->
- Snterml (Gram.Entry.obj Tactic.tactic_expr, string_of_int n)
- | Agram s ->
- let e =
- try
- (** ppedrot: we should always generate Agram entries which have already
- been registered, so this should not fail. *)
- let (u, s) = match String.split ':' s with
- | u :: s :: [] -> (u, s)
- | _ -> raise Not_found
- in
- get_entry (get_univ u) s
- with Not_found ->
- Errors.anomaly (str "Unregistered grammar entry: " ++ str s)
- in
- Snterm (Gram.Entry.obj (object_of_typed_entry e))
- | Aentry (u,s) ->
- let e = get_entry (get_univ u) s in
- Snterm (Gram.Entry.obj (object_of_typed_entry e))
+ | Aself -> Symbols.sself
+ | Anext -> Symbols.snext
+ | Aentry e ->
+ let e = get_typed_entry e in
+ Symbols.snterm (Gram.Entry.obj (object_of_typed_entry e))
+ | Aentryl (e, n) ->
+ let e = get_typed_entry e in
+ Symbols.snterml (Gram.Entry.obj (object_of_typed_entry e), string_of_int n)
+
+let level_of_snterml e = int_of_string (Symbols.snterml_level e)
-let level_of_snterml = function
- | Snterml (_,l) -> int_of_string l
- | _ -> failwith "level_of_snterml"
+let rec of_coq_rule : type self a r. (self, a, r) Extend.rule -> _ = function
+| Stop -> fun accu -> accu
+| Next (r, tok) -> fun accu ->
+ let symb = symbol_of_prod_entry_key tok in
+ of_coq_rule r (symb :: accu)
+
+let rec of_coq_action : type a r. (r, a, Loc.t -> r) Extend.rule -> a -> Gram.action = function
+| Stop -> fun f -> Gram.action (fun loc -> f (to_coqloc loc))
+| Next (r, _) -> fun f -> Gram.action (fun x -> of_coq_action r (f x))
+
+let of_coq_production_rule : type a. a Extend.production_rule -> _ = function
+| Rule (toks, act) -> (of_coq_rule toks [], of_coq_action toks act)
+
+let of_coq_single_extend_statement (lvl, assoc, rule) =
+ (lvl, Option.map of_coq_assoc assoc, List.map of_coq_production_rule rule)
+
+let of_coq_extend_statement (pos, st) =
+ (Option.map of_coq_position pos, List.map of_coq_single_extend_statement st)
+
+let grammar_extend e reinit ext =
+ let ext = of_coq_extend_statement ext in
+ unsafe_grammar_extend e reinit ext
(**********************************************************************)
(* Interpret entry names of the form "ne_constr_list" as entry keys *)
@@ -775,62 +781,83 @@ let tactic_level s =
let type_of_entry u s =
type_of_typed_entry (get_entry u s)
+let name_of_entry e = match String.split ':' (Gram.Entry.name e) with
+| u :: s :: [] -> Entry.unsafe_of_name (u, s)
+| _ -> assert false
+
+let atactic n =
+ if n = 5 then Aentry (name_of_entry Tactic.binder_tactic)
+ else Aentryl (name_of_entry Tactic.tactic_expr, n)
+
+let unsafe_of_genarg : argument_type -> 'a raw_abstract_argument_type =
+ (** FIXME *)
+ Obj.magic
+
+let try_get_entry u s =
+ (** Order the effects: type_of_entry can raise Not_found *)
+ let typ = type_of_entry u s in
+ let typ = unsafe_of_genarg typ in
+ EntryName (typ, Aentry (Entry.unsafe_of_name (Entry.univ_name u, s)))
+
+let wit_list : 'a raw_abstract_argument_type -> 'a list raw_abstract_argument_type =
+ fun t -> unsafe_of_genarg (ListArgType (unquote t))
+
+let wit_opt : 'a raw_abstract_argument_type -> 'a option raw_abstract_argument_type =
+ fun t -> unsafe_of_genarg (OptArgType (unquote t))
+
+type _ target =
+| TgAny : 's target
+| TgTactic : int -> Tacexpr.raw_tactic_expr target
+
+(** Quite ad-hoc *)
+let get_tacentry (type s) (n : int) (t : s target) : s entry_name = match t with
+| TgAny -> EntryName (rawwit wit_tactic, atactic n)
+| TgTactic m ->
+ let check_lvl n =
+ Int.equal m n
+ && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
+ && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
+ in
+ if check_lvl n then EntryName (rawwit wit_tactic, Aself)
+ else if check_lvl (n + 1) then EntryName (rawwit wit_tactic, Anext)
+ else EntryName (rawwit wit_tactic, atactic n)
+
let rec interp_entry_name static up_level s sep =
let l = String.length s in
if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
- let t, g = interp_entry_name static up_level (String.sub s 3 (l-8)) "" in
- ListArgType t, Alist1 g
+ let EntryName (t, g) = interp_entry_name static up_level (String.sub s 3 (l-8)) "" in
+ EntryName (wit_list t, Alist1 g)
else if l > 12 && coincide s "ne_" 0 &&
coincide s "_list_sep" (l-9) then
- let t, g = interp_entry_name static up_level (String.sub s 3 (l-12)) "" in
- ListArgType t, Alist1sep (g,sep)
+ let EntryName (t, g) = interp_entry_name static up_level (String.sub s 3 (l-12)) "" in
+ EntryName (wit_list t, Alist1sep (g,sep))
else if l > 5 && coincide s "_list" (l-5) then
- let t, g = interp_entry_name static up_level (String.sub s 0 (l-5)) "" in
- ListArgType t, Alist0 g
+ let EntryName (t, g) = interp_entry_name static up_level (String.sub s 0 (l-5)) "" in
+ EntryName (wit_list t, Alist0 g)
else if l > 9 && coincide s "_list_sep" (l-9) then
- let t, g = interp_entry_name static up_level (String.sub s 0 (l-9)) "" in
- ListArgType t, Alist0sep (g,sep)
+ let EntryName (t, g) = interp_entry_name static up_level (String.sub s 0 (l-9)) "" in
+ EntryName (wit_list t, Alist0sep (g,sep))
else if l > 4 && coincide s "_opt" (l-4) then
- let t, g = interp_entry_name static up_level (String.sub s 0 (l-4)) "" in
- OptArgType t, Aopt g
+ let EntryName (t, g) = interp_entry_name static up_level (String.sub s 0 (l-4)) "" in
+ EntryName (wit_opt t, Aopt g)
else if l > 5 && coincide s "_mods" (l-5) then
- let t, g = interp_entry_name static up_level (String.sub s 0 (l-1)) "" in
- ListArgType t, Amodifiers g
+ let EntryName (t, g) = interp_entry_name static up_level (String.sub s 0 (l-1)) "" in
+ EntryName (wit_list t, Amodifiers g)
else
let s = match s with "hyp" -> "var" | _ -> s in
- let check_lvl n = match up_level with
- | None -> false
- | Some m -> Int.equal m n
- && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
- && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
- in
- let t, se =
match tactic_level s with
- | Some n ->
- (** Quite ad-hoc *)
- let t = unquote (rawwit wit_tactic) in
- let se =
- if check_lvl n then Aself
- else if check_lvl (n + 1) then Anext
- else Atactic n
- in
- (Some t, se)
+ | Some n -> get_tacentry n up_level
| None ->
- try Some (type_of_entry uprim s), Aentry ("prim",s) with Not_found ->
- try Some (type_of_entry uconstr s), Aentry ("constr",s) with Not_found ->
- try Some (type_of_entry utactic s), Aentry ("tactic",s) with Not_found ->
+ try try_get_entry uprim s with Not_found ->
+ try try_get_entry uconstr s with Not_found ->
+ try try_get_entry utactic s with Not_found ->
if static then
error ("Unknown entry "^s^".")
else
- None, Aentry ("",s) in
- let t =
- match t with
- | Some t -> t
- | None -> ExtraArgType s in
- t, se
+ EntryName (unsafe_of_genarg (ExtraArgType s), Aentry (Entry.dynamic s))
let list_entry_names () =
let add_entry key (entry, _) accu = (key, entry) :: accu in
- let ans = Hashtbl.fold add_entry (snd uprim) [] in
- let ans = Hashtbl.fold add_entry (snd uconstr) ans in
- Hashtbl.fold add_entry (snd utactic) ans
+ let ans = Hashtbl.fold add_entry (get_utable uprim) [] in
+ let ans = Hashtbl.fold add_entry (get_utable uconstr) ans in
+ Hashtbl.fold add_entry (get_utable utactic) ans
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 2146ad964..c224dbad9 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -14,13 +14,12 @@ open Genarg
open Constrexpr
open Tacexpr
open Libnames
-open Compat
open Misctypes
open Genredexpr
(** The parser of Coq *)
-module Gram : GrammarSig
+module Gram : Compat.GrammarSig
(** The parser of Coq is built from three kinds of rule declarations:
@@ -106,28 +105,40 @@ type grammar_object
(** Type of reinitialization data *)
type gram_reinit = gram_assoc * gram_position
+(** General entry keys *)
+
+(** This intermediate abstract representation of entries can
+ both be reified into mlexpr for the ML extensions and
+ dynamically interpreted as entries for the Coq level extensions
+*)
+
+type ('self, 'a) entry_key = ('self, 'a) Extend.symbol =
+| Atoken : Tok.t -> ('self, string) entry_key
+| Alist1 : ('self, 'a) entry_key -> ('self, 'a list) entry_key
+| Alist1sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key
+| Alist0 : ('self, 'a) entry_key -> ('self, 'a list) entry_key
+| Alist0sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key
+| Aopt : ('self, 'a) entry_key -> ('self, 'a option) entry_key
+| Amodifiers : ('self, 'a) entry_key -> ('self, 'a list) entry_key
+| Aself : ('self, 'self) entry_key
+| Anext : ('self, 'self) entry_key
+| Aentry : 'a Entry.t -> ('self, 'a) entry_key
+| Aentryl : 'a Entry.t * int -> ('self, 'a) entry_key
+
(** Add one extension at some camlp4 position of some camlp4 entry *)
-val grammar_extend :
+val unsafe_grammar_extend :
grammar_object Gram.entry ->
gram_reinit option (** for reinitialization if ever needed *) ->
Gram.extend_statment -> unit
+val grammar_extend :
+ 'a Gram.entry ->
+ gram_reinit option (** for reinitialization if ever needed *) ->
+ 'a Extend.extend_statment -> unit
+
(** Remove the last n extensions *)
val remove_grammars : int -> unit
-
-
-
-(** The type of typed grammar objects *)
-type typed_entry
-
-(** The possible types for extensible grammars *)
-type entry_type = argument_type
-
-val type_of_typed_entry : typed_entry -> entry_type
-val object_of_typed_entry : typed_entry -> grammar_object Gram.entry
-val weaken_entry : 'a Gram.entry -> grammar_object Gram.entry
-
(** Temporary activate camlp4 verbosity *)
val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit
@@ -138,11 +149,7 @@ val parse_string : 'a Gram.entry -> string -> 'a
val eoi_entry : 'a Gram.entry -> 'a Gram.entry
val map_entry : ('a -> 'b) -> 'a Gram.entry -> 'b Gram.entry
-(** Table of Coq statically defined grammar entries *)
-
-type gram_universe
-
-(** There are four predefined universes: "prim", "constr", "tactic", "vernac" *)
+type gram_universe = Entry.universe
val get_univ : string -> gram_universe
@@ -151,7 +158,6 @@ val uconstr : gram_universe
val utactic : gram_universe
val uvernac : gram_universe
-val create_entry : gram_universe -> string -> entry_type -> typed_entry
val create_generic_entry : string -> ('a, rlevel) abstract_argument_type ->
'a Gram.entry
@@ -258,38 +264,25 @@ val symbol_of_constr_prod_entry_key : gram_assoc option ->
constr_entry_key -> bool -> constr_prod_entry_key ->
Gram.symbol
-(** General entry keys *)
-
-(** This intermediate abstract representation of entries can
- both be reified into mlexpr for the ML extensions and
- dynamically interpreted as entries for the Coq level extensions
-*)
-
-type prod_entry_key =
- | Alist1 of prod_entry_key
- | Alist1sep of prod_entry_key * string
- | Alist0 of prod_entry_key
- | Alist0sep of prod_entry_key * string
- | Aopt of prod_entry_key
- | Amodifiers of prod_entry_key
- | Aself
- | Anext
- | Atactic of int
- | Agram of string
- | Aentry of string * string
+val name_of_entry : 'a Gram.entry -> 'a Entry.t
(** Binding general entry keys to symbols *)
val symbol_of_prod_entry_key :
- prod_entry_key -> Gram.symbol
+ ('self, 'a) entry_key -> Gram.symbol
+
+type 's entry_name = EntryName :
+ 'a raw_abstract_argument_type * ('s, 'a) entry_key -> 's entry_name
(** Interpret entry names of the form "ne_constr_list" as entry keys *)
+type _ target = TgAny : 's target | TgTactic : int -> raw_tactic_expr target
+
val interp_entry_name : bool (** true to fail on unknown entry *) ->
- int option -> string -> string -> entry_type * prod_entry_key
+ 's target -> string -> string -> 's entry_name
(** Recover the list of all known tactic notation entries. *)
-val list_entry_names : unit -> (string * entry_type) list
+val list_entry_names : unit -> (string * argument_type) list
(** Registering/resetting the level of a constr entry *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 08:18:32 +0000