summaryrefslogtreecommitdiff
path: root/interp/topconstr.mli
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
commitcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch)
treeb7832bd5d412a5a5d69cb36ae2ded62c71124c22 /interp/topconstr.mli
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'interp/topconstr.mli')
-rw-r--r--interp/topconstr.mli32
1 files changed, 25 insertions, 7 deletions
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 2ac9da11..1dd5ec97 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: topconstr.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: topconstr.mli 11739 2009-01-02 19:33:19Z herbelin $ i*)
(*i*)
open Pp
@@ -77,11 +77,14 @@ type scope_name = string
type tmp_scope_name = scope_name
-type interpretation =
- (identifier * (tmp_scope_name option * scope_name list)) list * aconstr
+type subscopes = tmp_scope_name option * scope_name list
+
+type interpretation =
+ (* regular vars of notation / recursive parts of notation / body *)
+ ((identifier * subscopes) list * (identifier * subscopes) list) * aconstr
val match_aconstr : rawconstr -> interpretation ->
- (rawconstr * (tmp_scope_name option * scope_name list)) list
+ (rawconstr * subscopes) list * (rawconstr list * subscopes) list
(**********************************************************************)
(* Substitution of kernel names in interpretation data *)
@@ -95,18 +98,27 @@ type notation = string
type explicitation = ExplByPos of int * identifier option | ExplByName of identifier
-type binder_kind = Default of binding_kind | TypeClass of binding_kind * binding_kind
+type binder_kind =
+ | Default of binding_kind
+ | Generalized of binding_kind * binding_kind * bool
+ (* Inner binding, outer bindings, typeclass-specific flag
+ for implicit generalization of superclasses *)
+
+type abstraction_kind = AbsLambda | AbsPi
type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
type prim_token = Numeral of Bigint.bigint | String of string
+type 'a notation_substitution =
+ 'a list * (* for recursive notations: *) 'a list list
+
type cases_pattern_expr =
| CPatAlias of loc * cases_pattern_expr * identifier
| CPatCstr of loc * reference * cases_pattern_expr list
| CPatAtom of loc * reference option
| CPatOr of loc * cases_pattern_expr list
- | CPatNotation of loc * notation * cases_pattern_expr list
+ | CPatNotation of loc * notation * cases_pattern_expr notation_substitution
| CPatPrim of loc * prim_token
| CPatDelimiters of loc * string * cases_pattern_expr
@@ -121,6 +133,7 @@ type constr_expr =
| CAppExpl of loc * (proj_flag * reference) * constr_expr list
| CApp of loc * (proj_flag * constr_expr) *
(constr_expr * explicitation located option) list
+ | CRecord of loc * constr_expr option * (identifier located * constr_expr) list
| CCases of loc * case_style * constr_expr option *
(constr_expr * (name option * constr_expr option)) list *
(loc * cases_pattern_expr list located list * constr_expr) list
@@ -133,7 +146,8 @@ type constr_expr =
| CEvar of loc * existential_key * constr_expr list option
| CSort of loc * rawsort
| CCast of loc * constr_expr * constr_expr cast_type
- | CNotation of loc * notation * constr_expr list
+ | CNotation of loc * notation * constr_expr notation_substitution
+ | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr
| CPrim of loc * prim_token
| CDelimiters of loc * string * constr_expr
| CDynamic of loc * Dyn.t
@@ -158,6 +172,8 @@ type typeclass_constraint = name located * binding_kind * constr_expr
and typeclass_context = typeclass_constraint list
+type constr_pattern_expr = constr_expr
+
(**********************************************************************)
(* Utilities on constr_expr *)
@@ -240,3 +256,5 @@ type include_ast =
| CIMTE of module_type_ast
| CIME of module_ast
+val ntn_loc : Util.loc -> constr_expr list -> string -> int
+val patntn_loc : Util.loc -> cases_pattern_expr list -> string -> int