diff options
Diffstat (limited to 'parsing/extend.mli')
-rw-r--r-- | parsing/extend.mli | 153 |
1 files changed, 153 insertions, 0 deletions
diff --git a/parsing/extend.mli b/parsing/extend.mli new file mode 100644 index 00000000..761d0e04 --- /dev/null +++ b/parsing/extend.mli @@ -0,0 +1,153 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: extend.mli,v 1.19.2.1 2004/07/16 19:30:37 herbelin Exp $ i*) + +(*i*) +open Pp +open Util +open Names +open Ast +open Coqast +open Ppextend +open Topconstr +open Genarg +(*i*) + +type entry_type = argument_type + +type production_position = + | BorderProd of bool * Gramext.g_assoc option (* true=left; false=right *) + | InternalProd + +type production_level = + | NextLevel + | NumLevel of int + +type ('lev,'pos) constr_entry_key = + | ETIdent | ETReference | ETBigint + | ETConstr of ('lev * 'pos) + | ETPattern + | ETOther of string * string + | ETConstrList of ('lev * 'pos) * Token.pattern list + +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 + +(* Globalisation and type-checking of Grammar actions *) +type entry_context = identifier list + +val set_constr_globalizer : + (entry_context -> constr_expr -> constr_expr) -> unit + +type syntax_modifier = + | SetItemLevel of string list * production_level + | SetLevel of int + | SetAssoc of Gramext.g_assoc + | SetEntryType of string * simple_constr_production_entry + | 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 + +(*val subst_unparsing_hunk : + Names.substitution -> (Names.substitution -> 'pat -> 'pat) -> + 'pat unparsing_hunk -> 'pat unparsing_hunk +*) + +(* 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 |