diff options
Diffstat (limited to 'parsing/ast.mli')
-rwxr-xr-x | parsing/ast.mli | 123 |
1 files changed, 0 insertions, 123 deletions
diff --git a/parsing/ast.mli b/parsing/ast.mli deleted file mode 100755 index 7bc0b607..00000000 --- a/parsing/ast.mli +++ /dev/null @@ -1,123 +0,0 @@ -(************************************************************************) -(* 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: ast.mli,v 1.17.2.1 2004/07/16 19:30:37 herbelin Exp $ i*) - -(*i*) -open Pp -open Util -open Names -open Libnames -open Coqast -open Topconstr -open Genarg -(*i*) - -(* Abstract syntax trees. *) - -val loc : Coqast.t -> loc - -(* ast constructors with dummy location *) -val ope : string * Coqast.t list -> Coqast.t -val slam : identifier option * Coqast.t -> Coqast.t -val nvar : identifier -> Coqast.t -val ide : string -> Coqast.t -val num : int -> Coqast.t -val string : string -> Coqast.t -val path : kernel_name -> Coqast.t -val dynamic : Dyn.t -> Coqast.t - -val set_loc : loc -> Coqast.t -> Coqast.t - -val path_section : loc -> kernel_name -> Coqast.t -val section_path : kernel_name -> kernel_name - -(* ast destructors *) -val num_of_ast : Coqast.t -> int -val id_of_ast : Coqast.t -> string -val nvar_of_ast : Coqast.t -> identifier -val meta_of_ast : Coqast.t -> string - -(* patterns of ast *) -type astpat = - | Pquote of t - | Pmeta of string * tok_kind - | Pnode of string * patlist - | Pslam of identifier option * astpat - | Pmeta_slam of string * astpat - -and patlist = - | Pcons of astpat * patlist - | Plmeta of string - | Pnil - -and tok_kind = Tnum | Tid | Tstr | Tpath | Tvar | Tany | Tlist - -type pat = - | AstListPat of patlist - | PureAstPat of astpat - -(* semantic actions of grammar rules *) -type act = - | Act of constr_expr - | ActCase of act * (pat * act) list - | ActCaseList of act * (pat * act) list - -(* values associated to variables *) -type typed_ast = - | AstListNode of Coqast.t list - | PureAstNode of Coqast.t - -type ast_action_type = ETast | ETastl - -type dynamic_grammar = - | ConstrNode of constr_expr - | CasesPatternNode of cases_pattern_expr - -type grammar_action = - | SimpleAction of loc * dynamic_grammar - | CaseAction of - loc * grammar_action * ast_action_type * (t list * grammar_action) list - -type env = (string * typed_ast) list - -val coerce_to_id : constr_expr -> identifier located - -val coerce_global_to_id : reference -> identifier -val coerce_reference_to_id : reference -> identifier - -exception No_match of string - -val isMeta : string -> bool - -val print_ast : Coqast.t -> std_ppcmds -val print_astl : Coqast.t list -> std_ppcmds -val print_astpat : astpat -> std_ppcmds -val print_astlpat : patlist -> std_ppcmds - -(* Meta-syntax operations: matching and substitution *) - -type entry_env = (string * ast_action_type) list - -val grammar_type_error : loc * string -> 'a - -(* Converting and checking free meta-variables *) - -(* For old ast printer *) -val pat_sub : loc -> env -> astpat -> Coqast.t -val val_of_ast : entry_env -> Coqast.t -> astpat -val alpha_eq : Coqast.t * Coqast.t -> bool -val alpha_eq_val : typed_ast * typed_ast -> bool -val occur_var_ast : identifier -> Coqast.t -> bool -val find_all_matches : ('a -> astpat) -> env -> t -> 'a list -> ('a * env) list -val first_matchl : ('a -> patlist) -> env -> Coqast.t list -> 'a list -> - ('a * env) option -val to_pat : entry_env -> Coqast.t -> (astpat * entry_env) - -(* Object substitution in modules *) -val subst_astpat : Names.substitution -> astpat -> astpat |