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
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Loc
open Names
open Libnames
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 * Id.t option
| ExplByName of Id.t
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 (** representation of integer literals that appear in Coq scripts. *)
| String of string
type raw_cases_pattern_expr =
| RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t
| RCPatCstr of Loc.t * Globnames.global_reference
* raw_cases_pattern_expr list * raw_cases_pattern_expr list
(** [CPatCstr (_, c, l1, l2)] represents ((@c l1) l2) *)
| RCPatAtom of Loc.t * Id.t option
| RCPatOr of Loc.t * raw_cases_pattern_expr list
type instance_expr = Misctypes.glob_level list
type cases_pattern_expr =
| CPatAlias of Loc.t * cases_pattern_expr * Id.t
| CPatCstr of Loc.t * reference
* cases_pattern_expr list option * cases_pattern_expr list
(** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *)
| CPatAtom of Loc.t * reference option
| CPatOr of Loc.t * cases_pattern_expr list
| CPatNotation of Loc.t * notation * cases_pattern_notation_substitution
* cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents
(notation n applied with substitution l1)
applied to arguments l2 *)
| CPatPrim of Loc.t * prim_token
| CPatRecord of Loc.t * (reference * cases_pattern_expr) list
| CPatDelimiters of Loc.t * string * cases_pattern_expr
| CPatCast of Loc.t * cases_pattern_expr * constr_expr
and cases_pattern_notation_substitution =
cases_pattern_expr list * (** for constr subterms *)
cases_pattern_expr list list (** for recursive notations *)
and constr_expr =
| CRef of reference * instance_expr option
| CFix of Loc.t * Id.t located * fix_expr list
| CCoFix of Loc.t * Id.t located * cofix_expr list
| CProdN of Loc.t * binder_expr list * constr_expr
| CLambdaN of Loc.t * binder_expr list * constr_expr
| CLetIn of Loc.t * Name.t located * constr_expr * constr_expr
| CAppExpl of Loc.t * (proj_flag * reference * instance_expr option) * constr_expr list
| CApp of Loc.t * (proj_flag * constr_expr) *
(constr_expr * explicitation located option) list
| CRecord of Loc.t * (reference * constr_expr) list
(* representation of the "let" and "match" constructs *)
| CCases of Loc.t (* position of the "match" keyword *)
* case_style (* determines whether this value represents "let" or "match" construct *)
* constr_expr option (* return-clause *)
* case_expr list
* branch_expr list (* branches *)
| CLetTuple of Loc.t * Name.t located list * (Name.t located option * constr_expr option) *
constr_expr * constr_expr
| CIf of Loc.t * constr_expr * (Name.t located option * constr_expr option)
* constr_expr * constr_expr
| CHole of Loc.t * Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option
| CPatVar of Loc.t * patvar
| CEvar of Loc.t * Glob_term.existential_name * (Id.t * constr_expr) list
| CSort of Loc.t * glob_sort
| CCast of Loc.t * constr_expr * constr_expr cast_type
| CNotation of Loc.t * notation * constr_notation_substitution
| CGeneralization of Loc.t * binding_kind * abstraction_kind option * constr_expr
| CPrim of Loc.t * prim_token
| CDelimiters of Loc.t * string * constr_expr
and case_expr = constr_expr (* expression that is being matched *)
* Name.t located option (* as-clause *)
* cases_pattern_expr option (* in-clause *)
and branch_expr =
Loc.t * cases_pattern_expr list located list * constr_expr
and binder_expr =
Name.t located list * binder_kind * constr_expr
and fix_expr =
Id.t located * (Id.t located option * recursion_order_expr) *
local_binder list * constr_expr * constr_expr
and cofix_expr =
Id.t 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.t located * constr_expr
| LocalRawAssum of Name.t located list * binder_kind * constr_expr
| LocalPattern of Loc.t * cases_pattern_expr * constr_expr option
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.t located * Id.t located list option) * 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 Id.t list located * qualid located
| CWith_Definition of Id.t list located * constr_expr
type module_ast =
| CMident of qualid located
| CMapply of Loc.t * module_ast * module_ast
| CMwith of Loc.t * module_ast * with_declaration_ast
|
