diff options
Diffstat (limited to 'parsing/extend.mli')
| -rw-r--r-- | parsing/extend.mli | 128 |
1 files changed, 12 insertions, 116 deletions
diff --git a/parsing/extend.mli b/parsing/extend.mli index c5417649..80de7108 100644 --- a/parsing/extend.mli +++ b/parsing/extend.mli @@ -6,23 +6,17 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extend.mli,v 1.19.2.2 2005/01/21 16:42:37 herbelin Exp $ i*) +(*i $Id: extend.mli 7761 2005-12-30 10:52:19Z herbelin $ i*) -(*i*) -open Pp open Util -open Names -open Ast -open Coqast -open Ppextend -open Topconstr -open Genarg -(*i*) -type entry_type = argument_type +(**********************************************************************) +(* constr entry keys *) + +type side = Left | Right type production_position = - | BorderProd of bool * Gramext.g_assoc option (* true=left; false=right *) + | BorderProd of side * Gramext.g_assoc option (* true=left; false=right *) | InternalProd type production_level = @@ -38,41 +32,13 @@ type ('lev,'pos) constr_entry_key = type constr_production_entry = (production_level,production_position) constr_entry_key -type constr_entry = (int,unit) constr_entry_key -type simple_constr_production_entry = (production_level,unit) constr_entry_key - -type nonterm_prod = - | ProdList0 of nonterm_prod - | ProdList1 of nonterm_prod * Token.pattern list - | ProdOpt of nonterm_prod - | ProdPrimitive of constr_production_entry - -type prod_item = - | Term of Token.pattern - | NonTerm of constr_production_entry * - (Names.identifier * constr_production_entry) option - -type grammar_rule = { - gr_name : string; - gr_production : prod_item list; - gr_action : constr_expr } - -type grammar_entry = { - ge_name : constr_entry; - gl_assoc : Gramext.g_assoc option; - gl_rules : grammar_rule list } - -type grammar_command = { - gc_univ : string; - gc_entries : grammar_entry list } - -type grammar_associativity = Gramext.g_assoc option +type constr_entry = + (int,unit) constr_entry_key +type simple_constr_production_entry = + (production_level,unit) constr_entry_key -(* Globalisation and type-checking of Grammar actions *) -type entry_context = identifier list - -val set_constr_globalizer : - (entry_context -> constr_expr -> constr_expr) -> unit +(**********************************************************************) +(* syntax modifiers *) type syntax_modifier = | SetItemLevel of string list * production_level @@ -82,73 +48,3 @@ type syntax_modifier = | SetOnlyParsing | SetFormat of string located -type nonterm = - | NtShort of string - | NtQual of string * string -type grammar_production = - | VTerm of string - | VNonTerm of loc * nonterm * Names.identifier option -type raw_grammar_rule = string * grammar_production list * grammar_action -type raw_grammar_entry = string * grammar_associativity * raw_grammar_rule list - -val terminal : string -> string * string - -val rename_command_entry : string -> string - -val explicitize_entry : string -> string -> constr_entry - -val subst_grammar_command : - Names.substitution -> grammar_command -> grammar_command - -(* unparsing objects *) - -type 'pat unparsing_hunk = - | PH of 'pat * string option * parenRelation - | RO of string - | UNP_BOX of ppbox * 'pat unparsing_hunk list - | UNP_BRK of int * int - | UNP_TBRK of int * int - | UNP_TAB - | UNP_FNL - | UNP_SYMBOLIC of string option * string * 'pat unparsing_hunk - -(*i -val subst_unparsing_hunk : - Names.substitution -> (Names.substitution -> 'pat -> 'pat) -> - 'pat unparsing_hunk -> 'pat unparsing_hunk -i*) - -(* Checks if the precedence of the parent printer (None means the - highest precedence), and the child's one, follow the given - relation. *) - -val tolerable_prec : tolerability option -> precedence -> bool - -type 'pat syntax_entry = { - syn_id : string; - syn_prec: precedence; - syn_astpat : 'pat; - syn_hunks : 'pat unparsing_hunk list } - -val subst_syntax_entry : - (Names.substitution -> 'pat -> 'pat) -> - Names.substitution -> 'pat syntax_entry -> 'pat syntax_entry - - -type 'pat syntax_command = { - sc_univ : string; - sc_entries : 'pat syntax_entry list } - -val subst_syntax_command : - (Names.substitution -> 'pat -> 'pat) -> - Names.substitution -> 'pat syntax_command -> 'pat syntax_command - -type syntax_rule = string * Coqast.t * Coqast.t unparsing_hunk list -type raw_syntax_entry = precedence * syntax_rule list - -val interp_grammar_command : - string -> (string * string -> unit) -> - raw_grammar_entry list -> grammar_command - -val interp_syntax_entry : - string -> raw_syntax_entry list -> Ast.astpat syntax_command |