diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 252 |
1 files changed, 111 insertions, 141 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 9f186224..e12ccaa6 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -10,85 +10,48 @@ open Names open Extend -open Vernacexpr open Genarg open Constrexpr open Libnames -open Misctypes -open Genredexpr (** The parser of Coq *) +(** DO NOT USE EXTENSION FUNCTIONS IN THIS MODULE. + We only have it here to work with Camlp5. Handwritten grammar extensions + should use the safe [Pcoq.grammar_extend] function below. *) module Gram : sig include Grammar.S with type te = Tok.t -(* Where Grammar.S is + type 'a entry = 'a Entry.e + [@@ocaml.deprecated "Use [Pcoq.Entry.t]"] -module type S = - sig - type te = 'x; - type parsable = 'x; - value parsable : Stream.t char -> parsable; - value tokens : string -> list (string * int); - value glexer : Plexing.lexer te; - value set_algorithm : parse_algorithm -> unit; - module Entry : - sig - type e 'a = 'y; - value create : string -> e 'a; - value parse : e 'a -> parsable -> 'a; - value parse_token : e 'a -> Stream.t te -> 'a; - value name : e 'a -> string; - value of_parser : string -> (Stream.t te -> 'a) -> e 'a; - value print : Format.formatter -> e 'a -> unit; - external obj : e 'a -> Gramext.g_entry te = "%identity"; - end - ; - module Unsafe : - sig - value gram_reinit : Plexing.lexer te -> unit; - value clear_entry : Entry.e 'a -> unit; - end - ; - value extend : - Entry.e 'a -> option Gramext.position -> - list - (option string * option Gramext.g_assoc * - list (list (Gramext.g_symbol te) * Gramext.g_action)) -> - unit; - value delete_rule : Entry.e 'a -> list (Gramext.g_symbol te) -> unit; - end + [@@@ocaml.warning "-3"] -*) - - type 'a entry = 'a Entry.e - type internal_entry = Tok.t Gramext.g_entry - type symbol = Tok.t Gramext.g_symbol - type action = Gramext.g_action - type production_rule = symbol list * action - type single_extend_statment = - string option * Gramext.g_assoc option * production_rule list - type extend_statment = - Gramext.position option * single_extend_statment list - - type coq_parsable - - val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable - val action : 'a -> action val entry_create : string -> 'a entry - val entry_parse : 'a entry -> coq_parsable -> 'a - val entry_print : Format.formatter -> 'a entry -> unit + [@@ocaml.deprecated "Use [Pcoq.Entry.create]"] - (* Get comment parsing information from the Lexer *) - val comment_state : coq_parsable -> ((int * int) * string) list + val gram_extend : 'a entry -> 'a Extend.extend_statement -> unit - (* Apparently not used *) - val srules' : production_rule list -> symbol - val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a + [@@@ocaml.warning "+3"] end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e +module Parsable : +sig + type t + val make : ?file:Loc.source -> char Stream.t -> t + (* Get comment parsing information from the Lexer *) + val comment_state : t -> ((int * int) * string) list +end + +module Entry : sig + type 'a t = 'a Grammar.GMake(CLexer).Entry.e + val create : string -> 'a t + val parse : 'a t -> Parsable.t -> 'a + val print : Format.formatter -> 'a t -> unit +end + (** The parser of Coq is built from three kinds of rule declarations: - dynamic rules declared at the evaluation of Coq files (using @@ -170,106 +133,88 @@ val camlp5_verbosity : bool -> ('a -> unit) -> 'a -> unit (** Parse a string *) -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 +val parse_string : 'a Entry.t -> string -> 'a +val eoi_entry : 'a Entry.t -> 'a Entry.t +val map_entry : ('a -> 'b) -> 'a Entry.t -> 'b Entry.t type gram_universe val get_univ : string -> gram_universe +val create_universe : string -> gram_universe + +val new_entry : gram_universe -> string -> 'a Entry.t val uprim : gram_universe val uconstr : gram_universe val utactic : gram_universe -val uvernac : gram_universe -val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit -val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry + +val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Entry.t -> unit +val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Entry.t val create_generic_entry : gram_universe -> string -> - ('a, rlevel) abstract_argument_type -> 'a Gram.entry + ('a, rlevel) abstract_argument_type -> 'a Entry.t module Prim : sig open Names open Libnames - val preident : string Gram.entry - val ident : Id.t Gram.entry - val name : lname Gram.entry - val identref : lident Gram.entry - val univ_decl : universe_decl_expr Gram.entry - val ident_decl : ident_decl Gram.entry - val pattern_ident : Id.t Gram.entry - val pattern_identref : lident Gram.entry - val base_ident : Id.t Gram.entry - val natural : int Gram.entry - val bigint : Constrexpr.raw_natural_number Gram.entry - val integer : int Gram.entry - val string : string Gram.entry - val lstring : lstring Gram.entry - val qualid : qualid CAst.t Gram.entry - val fullyqualid : Id.t list CAst.t Gram.entry - val reference : reference Gram.entry - val by_notation : (string * string option) Gram.entry - val smart_global : reference or_by_notation Gram.entry - val dirpath : DirPath.t Gram.entry - val ne_string : string Gram.entry - val ne_lstring : lstring Gram.entry - val var : lident Gram.entry + val preident : string Entry.t + val ident : Id.t Entry.t + val name : lname Entry.t + val identref : lident Entry.t + val univ_decl : universe_decl_expr Entry.t + val ident_decl : ident_decl Entry.t + val pattern_ident : Id.t Entry.t + val pattern_identref : lident Entry.t + val base_ident : Id.t Entry.t + val natural : int Entry.t + val bigint : Constrexpr.raw_natural_number Entry.t + val integer : int Entry.t + val string : string Entry.t + val lstring : lstring Entry.t + val reference : qualid Entry.t + val qualid : qualid Entry.t + val fullyqualid : Id.t list CAst.t Entry.t + val by_notation : (string * string option) Entry.t + val smart_global : qualid or_by_notation Entry.t + val dirpath : DirPath.t Entry.t + val ne_string : string Entry.t + val ne_lstring : lstring Entry.t + val var : lident Entry.t end module Constr : sig - val constr : constr_expr Gram.entry - val constr_eoi : constr_expr Gram.entry - val lconstr : constr_expr Gram.entry - val binder_constr : constr_expr Gram.entry - val operconstr : constr_expr Gram.entry - val ident : Id.t Gram.entry - val global : reference Gram.entry - val universe_level : glob_level Gram.entry - val sort : glob_sort Gram.entry - val sort_family : Sorts.family Gram.entry - val pattern : cases_pattern_expr Gram.entry - val constr_pattern : constr_expr Gram.entry - val lconstr_pattern : constr_expr Gram.entry - val closed_binder : local_binder_expr list Gram.entry - val binder : local_binder_expr list Gram.entry (* closed_binder or variable *) - val binders : local_binder_expr list Gram.entry (* list of binder *) - val open_binders : local_binder_expr list Gram.entry - val binders_fixannot : (local_binder_expr list * (lident option * recursion_order_expr)) Gram.entry - val typeclass_constraint : (lname * bool * constr_expr) Gram.entry - val record_declaration : constr_expr Gram.entry - val appl_arg : (constr_expr * explicitation CAst.t option) Gram.entry + val constr : constr_expr Entry.t + val constr_eoi : constr_expr Entry.t + val lconstr : constr_expr Entry.t + val binder_constr : constr_expr Entry.t + val operconstr : constr_expr Entry.t + val ident : Id.t Entry.t + val global : qualid 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 + val pattern : cases_pattern_expr Entry.t + val constr_pattern : constr_expr Entry.t + val lconstr_pattern : constr_expr Entry.t + val closed_binder : local_binder_expr list Entry.t + val binder : local_binder_expr list Entry.t (* closed_binder or variable *) + val binders : local_binder_expr list Entry.t (* list of binder *) + val open_binders : local_binder_expr list Entry.t + val binders_fixannot : (local_binder_expr list * (lident option * recursion_order_expr)) Entry.t + val typeclass_constraint : (lname * bool * constr_expr) Entry.t + val record_declaration : constr_expr Entry.t + val appl_arg : (constr_expr * explicitation CAst.t option) Entry.t end module Module : sig - val module_expr : module_ast Gram.entry - val module_type : module_ast Gram.entry - end - -module Vernac_ : - sig - val gallina : vernac_expr Gram.entry - val gallina_ext : vernac_expr Gram.entry - val command : vernac_expr Gram.entry - val syntax : vernac_expr Gram.entry - val vernac_control : vernac_control Gram.entry - val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry - val noedit_mode : vernac_expr Gram.entry - val command_entry : vernac_expr Gram.entry - val red_expr : raw_red_expr Gram.entry - val hint_info : Vernacexpr.hint_info_expr Gram.entry + val module_expr : module_ast Entry.t + val module_type : module_ast Entry.t end -(** The main entry: reads an optional vernac command *) -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 -val set_command_entry : vernac_expr Gram.entry -> unit - val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option (** {5 Extending the parser without synchronization} *) @@ -277,8 +222,8 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option type gram_reinit = gram_assoc * gram_position (** Type of reinitialization data *) -val grammar_extend : 'a Gram.entry -> gram_reinit option -> - 'a Extend.extend_statment -> unit +val grammar_extend : 'a Entry.t -> gram_reinit option -> + 'a Extend.extend_statement -> unit (** Extend the grammar of Coq, without synchronizing it with the backtracking mechanism. This means that grammar extensions defined this way will survive an undo. *) @@ -288,12 +233,14 @@ val grammar_extend : 'a Gram.entry -> gram_reinit option -> module GramState : Store.S (** Auxiliary state of the grammar. Any added data must be marshallable. *) +(** {6 Extension with parsing rules} *) + type 'a grammar_command (** Type of synchronized parsing extensions. The ['a] type should be marshallable. *) type extend_rule = -| ExtendRule : 'a Gram.entry * gram_reinit option * 'a extend_statment -> extend_rule +| ExtendRule : 'a Entry.t * gram_reinit option * 'a extend_statement -> extend_rule type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t (** Grammar extension entry point. Given some ['a] and a current grammar state, @@ -308,12 +255,35 @@ val create_grammar_command : string -> 'a grammar_extension -> 'a grammar_comman val extend_grammar_command : 'a grammar_command -> 'a -> unit (** Extend the grammar of Coq with the given data. *) -val recover_grammar_command : 'a grammar_command -> 'a list -(** Recover the current stack of grammar extensions. *) +(** {6 Extension with parsing entries} *) + +type ('a, 'b) entry_command +(** Type of synchronized entry creation. The ['a] type should be + marshallable. *) + +type ('a, 'b) entry_extension = 'a -> GramState.t -> string list * GramState.t +(** Entry extension entry point. Given some ['a] and a current grammar state, + such a function must produce the list of entry extensions that will be + created and kept synchronized w.r.t. the summary, together + with a new state. It should be pure. *) + +val create_entry_command : string -> ('a, 'b) entry_extension -> ('a, 'b) entry_command +(** Create a new entry-creating command with the given name. The extension + function is called to generate the new entries for a given data. *) + +val extend_entry_command : ('a, 'b) entry_command -> 'a -> 'b Entry.t list +(** Create new synchronized entries using the provided data. *) + +val find_custom_entry : ('a, 'b) entry_command -> string -> 'b Entry.t +(** Find an entry generated by the synchronized system in the current state. + @raise Not_found if non-existent. *) + +(** {6 Protection w.r.t. backtrack} *) val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b (** Location Utils *) +val of_coqloc : Loc.t -> Ploc.t val to_coqloc : Ploc.t -> Loc.t val (!@) : Ploc.t -> Loc.t @@ -322,7 +292,7 @@ val parser_summary_tag : frozen_t Summary.Dyn.tag (** Registering grammars by name *) -type any_entry = AnyEntry : 'a Gram.entry -> any_entry +type any_entry = AnyEntry : 'a Entry.t -> any_entry val register_grammars_by_name : string -> any_entry list -> unit val find_grammars_by_name : string -> any_entry list |