Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 172 insertions, 0 deletions

diff --git a/interp/topconstr.mli b/interp/topconstr.mli
new file mode 100644
index 00000000..f4a82a3a
--- /dev/null
+++ b/interp/topconstr.mli
@@ -0,0 +1,172 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* $Id: topconstr.mli,v 1.23.2.1 2004/07/16 19:30:23 herbelin Exp $ *)
+
+(*i*)
+open Pp
+open Util
+open Names
+open Libnames
+open Rawterm
+open Term
+(*i*)
+
+(*s This is the subtype of rawconstr allowed in syntactic extensions *)
+(* No location since intended to be substituted at any place of a text *)
+(* Complex expressions such as fixpoints and cofixpoints are excluded, *)
+(* non global expressions such as existential variables also *)
+
+type aconstr =
+  (* Part common to rawconstr and cases_pattern *)
+  | ARef of global_reference
+  | AVar of identifier
+  | AApp of aconstr * aconstr list
+  | AList of identifier * identifier * aconstr * aconstr * bool
+  (* Part only in rawconstr *)
+  | ALambda of name * aconstr * aconstr
+  | AProd of name * aconstr * aconstr
+  | ALetIn of name * aconstr * aconstr
+  | ACases of aconstr option * aconstr option *
+      (aconstr * (name * (inductive * name list) option)) list *
+      (identifier list * cases_pattern list * aconstr) list
+  | AOrderedCase of case_style * aconstr option * aconstr * aconstr array
+  | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
+  | AIf of aconstr * (name * aconstr option) * aconstr * aconstr
+  | ASort of rawsort
+  | AHole of hole_kind
+  | APatVar of patvar
+  | ACast of aconstr * aconstr
+
+val rawconstr_of_aconstr_with_binders : loc -> 
+  (identifier -> 'a -> identifier * 'a) ->
+  ('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr
+
+val subst_aconstr : Names.substitution -> aconstr -> aconstr
+
+val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr
+
+(* [match_aconstr metas] match a rawconstr against an aconstr with
+   metavariables in [metas]; it raises [No_match] if the matching fails *)
+exception No_match
+
+type scope_name = string
+type interpretation = 
+    (identifier * (scope_name option * scope_name list)) list * aconstr
+
+val match_aconstr : (* scope_name option -> *) rawconstr -> interpretation ->
+      (rawconstr * (scope_name option * scope_name list)) list
+
+(*s Concrete syntax for terms *)
+
+type notation = string
+
+type explicitation = ExplByPos of int | ExplByName of identifier
+
+type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
+
+type cases_pattern_expr =
+  | CPatAlias of loc * cases_pattern_expr * identifier
+  | CPatCstr of loc * reference * cases_pattern_expr list
+  | CPatAtom of loc * reference option
+  | CPatNotation of loc * notation * cases_pattern_expr list
+  | CPatNumeral of loc * Bignat.bigint
+  | CPatDelimiters of loc * string * cases_pattern_expr
+
+type constr_expr =
+  | CRef of reference
+  | CFix of loc * identifier located * fixpoint_expr list
+  | CCoFix of loc * identifier located * cofixpoint_expr list
+  | CArrow of loc * constr_expr * constr_expr
+  | CProdN of loc * (name located list * constr_expr) list * constr_expr
+  | CLambdaN of loc * (name located list * constr_expr) list * constr_expr
+  | CLetIn of loc * name located * constr_expr * constr_expr
+  | CAppExpl of loc * (proj_flag * reference) * constr_expr list
+  | CApp of loc * (proj_flag * constr_expr) * 
+        (constr_expr * explicitation located option) list
+  | CCases of loc * (constr_expr option * constr_expr option) *
+      (constr_expr * (name option * constr_expr option)) list *
+      (loc * cases_pattern_expr list * constr_expr) list
+  | COrderedCase of loc * case_style * constr_expr option * constr_expr
+      * constr_expr list
+  | CLetTuple of loc * name list * (name option * constr_expr option) *
+      constr_expr * constr_expr
+  | CIf of loc * constr_expr * (name option * constr_expr option)
+      * constr_expr * constr_expr
+  | CHole of loc
+  | CPatVar of loc * (bool * patvar)
+  | CEvar of loc * existential_key
+  | CSort of loc * rawsort
+  | CCast of loc * constr_expr * constr_expr
+  | CNotation of loc * notation * constr_expr list
+  | CNumeral of loc * Bignat.bigint
+  | CDelimiters of loc * string * constr_expr
+  | CDynamic of loc * Dyn.t
+
+and fixpoint_expr =
+    identifier * int * local_binder list * constr_expr * constr_expr
+
+and cofixpoint_expr =
+    identifier * local_binder list * constr_expr * constr_expr
+
+and local_binder =
+  | LocalRawDef of name located * constr_expr
+  | LocalRawAssum of name located list * constr_expr
+
+
+val constr_loc : constr_expr -> loc
+
+val cases_pattern_loc : cases_pattern_expr -> loc
+
+val replace_vars_constr_expr :
+  (identifier * identifier) list -> constr_expr -> constr_expr
+
+val occur_var_constr_expr : identifier -> constr_expr -> bool
+
+(* Specific function for interning "in indtype" syntax of "match" *)
+val names_of_cases_indtype : constr_expr -> identifier list
+
+val mkIdentC : identifier -> constr_expr
+val mkRefC : reference -> constr_expr
+val mkAppC : constr_expr * constr_expr list -> constr_expr
+val mkCastC : constr_expr * constr_expr -> constr_expr
+val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr
+val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
+val mkProdC : name located list * constr_expr * constr_expr -> constr_expr
+
+(* For binders parsing *)
+
+(* Includes let binders *)
+val local_binders_length : local_binder list -> int
+
+(* Does not take let binders into account *)
+val names_of_local_assums : local_binder list -> name located list
+
+(* Used in correctness and interface; absence of var capture not guaranteed *)
+(* in pattern-matching clauses and in binders of the form [x,y:T(x)] *)
+
+val map_constr_expr_with_binders :
+  ('a -> constr_expr -> constr_expr) ->
+      (identifier -> 'a -> 'a) -> 'a -> constr_expr -> constr_expr
+
+(* Concrete syntax for modules and modules types *)
+
+type with_declaration_ast = 
+  | CWith_Module of identifier located * qualid located
+  | CWith_Definition of identifier located * constr_expr
+
+type module_type_ast = 
+  | CMTEident of qualid located
+  | CMTEwith of module_type_ast * with_declaration_ast
+
+type module_ast = 
+  | CMEident of qualid located
+  | CMEapply of module_ast * module_ast
+
+(* Special identifier to encode recursive notations *)
+val ldots_var : identifier