diff options
Diffstat (limited to 'coqpp/coqpp_ast.mli')
-rw-r--r-- | coqpp/coqpp_ast.mli | 96 |
1 files changed, 96 insertions, 0 deletions
diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli new file mode 100644 index 00000000..181c4361 --- /dev/null +++ b/coqpp/coqpp_ast.mli @@ -0,0 +1,96 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +type loc = { + loc_start : Lexing.position; + loc_end : Lexing.position; +} + +type code = { code : string } + +type user_symbol = +| Ulist1 of user_symbol +| Ulist1sep of user_symbol * string +| Ulist0 of user_symbol +| Ulist0sep of user_symbol * string +| Uopt of user_symbol +| Uentry of string +| Uentryl of string * int + +type token_data = +| TokNone +| TokName of string + +type ext_token = +| ExtTerminal of string +| ExtNonTerminal of user_symbol * token_data + +type tactic_rule = { + tac_toks : ext_token list; + tac_body : code; +} + +type level = string + +type position = +| First +| Last +| Before of level +| After of level +| Level of level + +type assoc = +| LeftA +| RightA +| NonA + +type gram_symbol = +| GSymbString of string +| GSymbQualid of string * level option +| GSymbParen of gram_symbol list +| GSymbProd of gram_prod list + +and gram_prod = { + gprod_symbs : (string option * gram_symbol list) list; + gprod_body : code; +} + +type gram_rule = { + grule_label : string option; + grule_assoc : assoc option; + grule_prods : gram_prod list; +} + +type grammar_entry = { + gentry_name : string; + gentry_pos : position option; + gentry_rules : gram_rule list; +} + +type grammar_ext = { + gramext_name : string; + gramext_globals : string list; + gramext_entries : grammar_entry list; +} + +type tactic_ext = { + tacext_name : string; + tacext_level : int option; + tacext_deprecated : code option; + tacext_rules : tactic_rule list; +} + +type node = +| Code of code +| Comment of string +| DeclarePlugin of string +| GramExt of grammar_ext +| VernacExt +| TacticExt of tactic_ext + +type t = node list |