diff options
Diffstat (limited to 'API/grammar_API.mli')
| -rw-r--r-- | API/grammar_API.mli | 249 |
1 files changed, 0 insertions, 249 deletions
diff --git a/API/grammar_API.mli b/API/grammar_API.mli deleted file mode 100644 index c2115a506..000000000 --- a/API/grammar_API.mli +++ /dev/null @@ -1,249 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -module Extend : -sig - type 'a entry = 'a Pcoq.Gram.Entry.e - type ('self, 'a) symbol = ('self, 'a) Extend.symbol = - | Atoken : Tok.t -> ('self, string) symbol - | Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol - | Alist1sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol - | Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol - | Alist0sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol - | Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol - | Aself : ('self, 'self) symbol - | Anext : ('self, 'self) symbol - | Aentry : 'a entry -> ('self, 'a) symbol - | Aentryl : 'a entry * int -> ('self, 'a) symbol - | Arules : 'a rules list -> ('self, 'a) symbol - and ('self, 'a, 'r) rule = ('self, 'a, 'r) Extend.rule = - | Stop : ('self, 'r, 'r) rule - | Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule - and ('a, 'r) norec_rule = ('a, 'r) Extend.norec_rule = - { norec_rule : 's. ('s, 'a, 'r) rule } - and 'a rules = 'a Extend.rules = - | Rules : ('act, Loc.t -> 'a) norec_rule * 'act -> 'a rules - type gram_assoc = Extend.gram_assoc = NonA | RightA | LeftA - type 'a production_rule = 'a Extend.production_rule = - | Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule - type 'a single_extend_statment = string option * gram_assoc option * 'a production_rule list - type gram_position = Extend.gram_position = - | First - | Last - | Before of string - | After of string - | Level of string - type 'a extend_statment = gram_position option * 'a single_extend_statment list - type 'a user_symbol = 'a Extend.user_symbol = - | Ulist1 of 'a user_symbol - | Ulist1sep of 'a user_symbol * string - | Ulist0 of 'a user_symbol - | Ulist0sep of 'a user_symbol * string - | Uopt of 'a user_symbol - | Uentry of 'a - | Uentryl of 'a * int -end - -module Genintern : -sig - open API - module Store : module type of struct include Genintern.Store end - type glob_sign = Genintern.glob_sign = - { ltacvars : Names.Id.Set.t; - genv : Environ.env; - extra : Store.t } - type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb - type 'glb subst_fun = Mod_subst.substitution -> 'glb -> 'glb - type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Names.Id.Map.t -> 'glb -> 'glb - val empty_glob_sign : Environ.env -> glob_sign - val register_intern0 : ('raw, 'glb, 'top) Genarg.genarg_type -> - ('raw, 'glb) intern_fun -> unit - val register_subst0 : ('raw, 'glb, 'top) Genarg.genarg_type -> - 'glb subst_fun -> unit - val register_ntn_subst0 : ('raw, 'glb, 'top) Genarg.genarg_type -> - 'glb ntn_subst_fun -> unit - val generic_substitute : Genarg.glob_generic_argument subst_fun - val generic_intern : (Genarg.raw_generic_argument, Genarg.glob_generic_argument) intern_fun -end - -module Tok : -sig - type t = Tok.t = - | KEYWORD of string - | PATTERNIDENT of string - | IDENT of string - | FIELD of string - | INT of string - | STRING of string - | LEFTQMARK - | BULLET of string - | EOI -end - -module Pcoq : -sig - type gram_universe = Pcoq.gram_universe - module Gram : - sig - type te = Tok.t - module Entry : - sig - type 'a e = 'a Extend.entry - val of_parser : string -> (te Stream.t -> 'a) -> 'a e - val obj : 'a e -> te Gramext.g_entry - val create : string -> 'a e - end - type 'a entry = 'a Entry.e - val extend : 'a Pcoq.Gram.Entry.e -> Gramext.position option -> - (string option * Gramext.g_assoc option * - (Tok.t Gramext.g_symbol list * Gramext.g_action) list) list -> unit - val entry_create : string -> 'a Entry.e - end - module Prim : sig - open Names - open Loc - val preident : string Gram.Entry.e - val ident : Names.Id.t Gram.Entry.e - val name : Name.t located Gram.Entry.e - val identref : Names.Id.t located Gram.Entry.e - val pidentref : (Names.Id.t located * (Names.Id.t located list) option) Gram.Entry.e - val pattern_ident : Names.Id.t Gram.Entry.e - val pattern_identref : Names.Id.t located Gram.Entry.e - val base_ident : Names.Id.t Gram.Entry.e - val natural : int Gram.Entry.e - val bigint : Constrexpr.raw_natural_number Gram.Entry.e - val integer : int Gram.Entry.e - val string : string Gram.Entry.e - val qualid : API.Libnames.qualid located Gram.Entry.e - val fullyqualid : Names.Id.t list located Gram.Entry.e - val reference : API.Libnames.reference Gram.Entry.e - val by_notation : (string * string option) Loc.located Gram.entry - val smart_global : API.Libnames.reference API.Misctypes.or_by_notation Gram.Entry.e - val dirpath : DirPath.t Gram.Entry.e - val ne_string : string Gram.Entry.e - val ne_lstring : string located Gram.Entry.e - val var : Names.Id.t located Gram.Entry.e - end - - val eoi_entry : 'a Gram.Entry.e -> 'a Gram.Entry.e - val create_generic_entry : gram_universe -> string -> - ('a, Genarg.rlevel) Genarg.abstract_argument_type -> 'a Gram.Entry.e - val utactic : gram_universe - type gram_reinit = Extend.gram_assoc * Extend.gram_position - val grammar_extend : 'a Gram.Entry.e -> gram_reinit option -> - 'a Extend.extend_statment -> unit - val genarg_grammar : ('raw, 'glb, 'top) Genarg.genarg_type -> 'raw Gram.Entry.e - val register_grammar : ('raw, 'glb, 'top) Genarg.genarg_type -> 'raw Gram.Entry.e -> unit - module Constr : - sig - val sort : API.Misctypes.glob_sort Gram.Entry.e - val lconstr : API.Constrexpr.constr_expr Gram.Entry.e - val lconstr_pattern : API.Constrexpr.constr_expr Gram.Entry.e - val ident : API.Names.Id.t Gram.Entry.e - val constr : API.Constrexpr.constr_expr Gram.Entry.e - val closed_binder : API.Constrexpr.local_binder_expr list Gram.Entry.e - val constr_pattern : API.Constrexpr.constr_expr Gram.Entry.e - val global : API.Libnames.reference Gram.Entry.e - val binder_constr : API.Constrexpr.constr_expr Gram.Entry.e - val operconstr : API.Constrexpr.constr_expr Gram.Entry.e - val pattern : API.Constrexpr.cases_pattern_expr Gram.Entry.e - val binders : API.Constrexpr.local_binder_expr list Gram.Entry.e - end - module Vernac_ : - sig - val gallina : API.Vernacexpr.vernac_expr Gram.Entry.e - val gallina_ext : API.Vernacexpr.vernac_expr Gram.Entry.e - val red_expr : API.Genredexpr.raw_red_expr Gram.Entry.e - val noedit_mode : API.Vernacexpr.vernac_expr Gram.Entry.e - val command : API.Vernacexpr.vernac_expr Gram.Entry.e - val rec_definition : (API.Vernacexpr.fixpoint_expr * API.Vernacexpr.decl_notation list) Gram.Entry.e - val vernac : API.Vernacexpr.vernac_expr Gram.Entry.e - end - - type extend_rule = - | ExtendRule : 'a Gram.Entry.e * gram_reinit option * 'a Extend.extend_statment -> extend_rule - - module GramState : module type of struct include Pcoq.GramState end - type 'a grammar_command = 'a Pcoq.grammar_command - type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t - val create_grammar_command : string -> 'a grammar_extension -> 'a grammar_command - val extend_grammar_command : 'a grammar_command -> 'a -> unit - val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option - val parse_string : 'a Gram.Entry.e -> string -> 'a - val (!@) : Ploc.t -> Loc.t - val set_command_entry : API.Vernacexpr.vernac_expr Gram.Entry.e -> unit - val to_coqloc : Ploc.t -> Loc.t -end - -module CLexer : -sig - type keyword_state = CLexer.keyword_state - val terminal : string -> Tok.t - val add_keyword : string -> unit - val is_keyword : string -> bool - val check_ident : string -> unit - val get_keyword_state : unit -> keyword_state - val set_keyword_state : keyword_state -> unit -end - -module Egramml : -sig - type 's grammar_prod_item = 's Egramml.grammar_prod_item = - | GramTerminal of string - | GramNonTerminal : ('a Genarg.raw_abstract_argument_type option * - ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item - - - val extend_vernac_command_grammar : - API.Vernacexpr.extend_name -> Vernacexpr.vernac_expr Pcoq.Gram.Entry.e option -> - Vernacexpr.vernac_expr grammar_prod_item list -> unit - - val make_rule : - (Loc.t -> Genarg.raw_generic_argument list -> 'a) -> - 'a grammar_prod_item list -> 'a Extend.production_rule -end - -module Mltop : -sig - val add_known_module : string -> unit - val module_is_known : string -> bool - val declare_cache_obj : (unit -> unit) -> string -> unit -end -module Vernacinterp : -sig - type deprecation = bool - type vernac_command = Genarg.raw_generic_argument list -> unit -> unit - val vinterp_add : deprecation -> API.Vernacexpr.extend_name -> - vernac_command -> unit -end - -module G_vernac : -sig - val def_body : API.Vernacexpr.definition_expr Pcoq.Gram.Entry.e - val section_subset_expr : API.Vernacexpr.section_subset_expr Pcoq.Gram.Entry.e - val query_command : (Vernacexpr.goal_selector option -> Vernacexpr.vernac_expr) - Pcoq.Gram.Entry.e -end - -module G_proofs : -sig - val hint : Vernacexpr.hints_expr Pcoq.Gram.Entry.e - val hint_proof_using : 'a Pcoq.Gram.Entry.e -> 'a option -> 'a option -end - -module Egramcoq : -sig -end - -module Metasyntax : -sig - type any_entry = Metasyntax.any_entry = - | AnyEntry : 'a Pcoq.Gram.Entry.e -> any_entry - val register_grammar : string -> any_entry list -> unit - val add_token_obj : string -> unit -end |