1 files changed, 123 insertions, 0 deletions
diff --git a/parsing/ast.mli b/parsing/ast.mli
new file mode 100755
index 00000000..7bc0b607
--- /dev/null
+++ b/parsing/ast.mli
@@ -0,0 +1,123 @@
+(************************************************************************)
+(*  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