blob: f6d274abb673cb9eef1cde01b886b8e1d3727786 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Pp
open Names
open Libnames
open Term
open Misctypes
open Decl_kinds
(** {6 Concrete syntax for terms } *)
(** [constr_expr] is the abstract syntax tree produced by the parser *)
type notation = string
type explicitation =
| ExplByPos of int * identifier option
| ExplByName of identifier
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 cases_pattern_expr =
| CPatAlias of loc * cases_pattern_expr * identifier
| CPatCstr of loc * reference * cases_pattern_expr list
| CPatCstrExpl 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_notation_substitution
| CPatPrim of loc * prim_token
| CPatRecord of loc * (reference * cases_pattern_expr) list
| CPatDelimiters of loc * string * cases_pattern_expr
and cases_pattern_notation_substitution =
cases_pattern_expr list * (** for constr subterms *)
cases_pattern_expr list list (** for recursive notations *)
type constr_expr =
| CRef of reference
| CFix of loc * identifier located * fix_expr list
| CCoFix of loc * identifier located * cofix_expr list
| CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
| CLambdaN of loc * (name located list * binder_kind * 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
| CRecord of loc * constr_expr option * (reference * constr_expr) list
| CCases of loc * case_style * constr_expr option *
(constr_expr * (name located option * cases_pattern_expr option)) list *
(loc * cases_pattern_expr list located list * constr_expr) list
| CLetTuple of loc * name located list * (name located option * constr_expr option) *
constr_expr * constr_expr
| CIf of loc * constr_expr * (name located option * constr_expr option)
* constr_expr * constr_expr
| CHole of loc * Evar_kinds.t option
| CPatVar of loc * (bool * patvar)
| CEvar of loc * existential_key * constr_expr list option
| CSort of loc * glob_sort
| CCast of loc * constr_expr * constr_expr cast_type
| CNotation of loc * notation * constr_notation_substitution
| CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr
| CPrim of loc * prim_token
| CDelimiters of loc * string * constr_expr
and fix_expr =
identifier located * (identifier located option * recursion_order_expr) *
local_binder list * constr_expr * constr_expr
and cofix_expr =
identifier located * local_binder list * constr_expr * constr_expr
and recursion_order_expr =
| CStructRec
| CWfRec of constr_expr
| CMeasureRec of constr_expr * constr_expr option (** measure, relation *)
(** Anonymous defs allowed ?? *)
and local_binder =
| LocalRawDef of name located * constr_expr
| LocalRawAssum of name located list * binder_kind * constr_expr
and constr_notation_substitution =
constr_expr list * (** for constr subterms *)
constr_expr list list * (** for recursive notations *)
local_binder list list (** for binders subexpressions *)
type typeclass_constraint = name located * binding_kind * constr_expr
and typeclass_context = typeclass_constraint list
type constr_pattern_expr = constr_expr
(** Concrete syntax for modules and module types *)
type with_declaration_ast =
| CWith_Module of identifier list located * qualid located
| CWith_Definition of identifier list located * constr_expr
type module_ast =
| CMident of qualid located
| CMapply of loc * module_ast * module_ast
| CMwith of loc * module_ast * with_declaration_ast
|
