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
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
|
(* generated by Ott 0.23 from: l2.ott *)
open import Pervasives
open import Map
open import Maybe
open import Set_extra
type l =
| Unknown
| Trans of string * maybe l
| Range of nat * nat
val duplicates : forall 'a. list 'a -> list 'a
val set_from_list : forall 'a. list 'a -> set 'a
val subst : forall 'a. list 'a -> list 'a -> bool
type x = string (* identifier *)
type ix = string (* infix identifier *)
type kid = (* variables with kind, ticked to differntiate from program variables *)
| Var of x
type base_kind = (* base kind *)
| BK_type (* kind of types *)
| BK_nat (* kind of natural number size expressions *)
| BK_order (* kind of vector order specifications *)
| BK_effect (* kind of effect sets *)
type nexp = (* expression of kind Nat, for vector sizes and origins *)
| Nexp_var of kid (* variable *)
| Nexp_constant of natural (* constant *)
| Nexp_times of nexp * nexp (* product *)
| Nexp_sum of nexp * nexp (* sum *)
| Nexp_exp of nexp (* exponential *)
type kind = (* kinds *)
| K_kind of list base_kind
type base_effect = (* effect *)
| BE_rreg (* read register *)
| BE_wreg (* write register *)
| BE_rmem (* read memory *)
| BE_wmem (* write memory *)
| BE_undef (* undefined-instruction exception *)
| BE_unspec (* unspecified values *)
| BE_nondet (* nondeterminism from intra-instruction parallelism *)
type order = (* vector order specifications, of kind Order *)
| Ord_var of kid (* variable *)
| Ord_inc (* increasing (little-endian) *)
| Ord_dec (* decreasing (big-endian) *)
type effect = (* effect set, of kind Effects *)
| Effect_var of kid
| Effect_set of list base_effect (* effect set *)
type id = (* Identifier *)
| Id of x
| DeIid of x (* remove infix status *)
let effect_union e1 e2 =
match (e1,e2) with
| (Effect_set els,Effect_set els2) -> Effect_set (els++els2)
end
type n_constraint = (* constraint over kind $Nat$ *)
| NC_fixed of nexp * nexp
| NC_bounded_ge of nexp * nexp
| NC_bounded_le of nexp * nexp
| NC_nat_set_bounded of kid * list natural
type kinded_id = (* optionally kind-annotated identifier *)
| KOpt_none of kid (* identifier *)
| KOpt_kind of kind * kid (* kind-annotated variable *)
type quant_item = (* Either a kinded identifier or a nexp constraint for a typquant *)
| QI_id of kinded_id (* An optionally kinded identifier *)
| QI_const of n_constraint (* A constraint for this type *)
type lit = (* Literal constant *)
| L_unit (* $() : unit$ *)
| L_zero (* $bitzero : bit$ *)
| L_one (* $bitone : bit$ *)
| L_true (* $true : bool$ *)
| L_false (* $false : bool$ *)
| L_num of natural (* natural number constant *)
| L_hex of string (* bit vector constant, C-style *)
| L_bin of string (* bit vector constant, C-style *)
| L_undef (* constant representing undefined values *)
| L_string of string (* string constant *)
type typ = (* Type expressions, of kind $Type$ *)
| Typ_wild (* Unspecified type *)
| Typ_id of id (* Defined type *)
| Typ_var of kid (* Type variable *)
| Typ_fn of typ * typ * effect (* Function type (first-order only in user code) *)
| Typ_tup of list typ (* Tuple type *)
| Typ_app of id * list typ_arg (* type constructor application *)
and typ_arg = (* Type constructor arguments of all kinds *)
| Typ_arg_nexp of nexp
| Typ_arg_typ of typ
| Typ_arg_order of order
| Typ_arg_effect of effect
type typquant = (* type quantifiers and constraints *)
| TypQ_tq of list quant_item
| TypQ_no_forall (* sugar, omitting quantifier and constraints *)
type pat = (* Pattern *)
| P_lit of lit (* literal constant pattern *)
| P_wild (* wildcard *)
| P_as of pat * id (* named pattern *)
| P_typ of typ * pat (* typed pattern *)
| P_id of id (* identifier *)
| P_app of id * list pat (* union constructor pattern *)
| P_record of list fpat * bool (* struct pattern *)
| P_vector of list pat (* vector pattern *)
| P_vector_indexed of list (natural * pat) (* vector pattern (with explicit indices) *)
| P_vector_concat of list pat (* concatenated vector pattern *)
| P_tup of list pat (* tuple pattern *)
| P_list of list pat (* list pattern *)
and fpat = (* Field pattern *)
| FP_Fpat of id * pat
type typschm = (* type scheme *)
| TypSchm_ts of typquant * typ
type exp = (* Expression *)
| E_block of list exp (* block (parsing conflict with structs?) *)
| E_id of id (* identifier *)
| E_lit of lit (* literal constant *)
| E_cast of typ * exp (* cast *)
| E_app of id * list exp (* function application *)
| E_app_infix of exp * id * exp (* infix function application *)
| E_tuple of list exp (* tuple *)
| E_if of exp * exp * exp (* conditional *)
| E_for of id * exp * exp * exp * exp (* loop *)
| E_vector of list exp (* vector (indexed from 0) *)
| E_vector_indexed of list (natural * exp) (* vector (indexed consecutively) *)
| E_vector_access of exp * exp (* vector access *)
| E_vector_subrange of exp * exp * exp (* subvector extraction *)
| E_vector_update of exp * exp * exp (* vector functional update *)
| E_vector_update_subrange of exp * exp * exp * exp (* vector subrange update (with vector) *)
| E_list of list exp (* list *)
| E_cons of exp * exp (* cons *)
| E_record of fexps (* struct *)
| E_record_update of exp * fexps (* functional update of struct *)
| E_field of exp * id (* field projection from struct *)
| E_case of exp * list pexp (* pattern matching *)
| E_let of letbind * exp (* let expression *)
| E_assign of lexp * exp (* imperative assignment *)
and lexp = (* lvalue expression *)
| LEXP_id of id (* identifier *)
| LEXP_memory of id * list exp (* memory write via function call *)
| LEXP_vector of lexp * exp (* vector element *)
| LEXP_vector_range of lexp * exp * exp (* subvector *)
| LEXP_field of lexp * id (* struct field *)
and fexp = (* Field-expression *)
| FE_Fexp of id * exp
and fexps = (* Field-expression list *)
| FES_Fexps of list fexp * bool
and pexp = (* Pattern match *)
| Pat_exp of pat * exp
and letbind = (* Let binding *)
| LB_val_explicit of typschm * pat * exp (* value binding, explicit type (pat must be total) *)
| LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *)
type type_union = (* Type union constructors *)
| Tu_id of id
| Tu_ty_id of typ * id
type funcl = (* Function clause *)
| FCL_Funcl of id * pat * exp
type effect_opt = (* Optional effect annotation for functions *)
| Effect_opt_pure (* sugar for empty effect set *)
| Effect_opt_effect of effect
type name_scm_opt = (* Optional variable-naming-scheme specification for variables of defined type *)
| Name_sect_none
| Name_sect_some of string
type rec_opt = (* Optional recursive annotation for functions *)
| Rec_nonrec (* non-recursive *)
| Rec_rec (* recursive *)
type tannot_opt = (* Optional type annotation for functions *)
| Typ_annot_opt_some of typquant * typ
type index_range = (* index specification, for bitfields in register types *)
| BF_single of natural (* single index *)
| BF_range of natural * natural (* index range *)
| BF_concat of index_range * index_range (* concatenation of index ranges *)
type val_spec = (* Value type specification *)
| VS_val_spec of typschm * id
| VS_extern_no_rename of typschm * id
| VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *)
type scattered_def = (* Function and type union definitions that can be spread across
a file. Each one must end in $id$ *)
| SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *)
| SD_scattered_funcl of funcl (* scattered function definition clause *)
| SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *)
| SD_scattered_unioncl of id * type_union (* scattered union definition member *)
| SD_scattered_end of id (* scattered definition end *)
type fundef = (* Function definition *)
| FD_function of rec_opt * tannot_opt * effect_opt * list funcl
type default_spec = (* Default kinding or typing assumption *)
| DT_kind of base_kind * kid
| DT_typ of typschm * id
type type_def = (* Type definition body *)
| TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *)
| TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *)
| TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *)
| TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *)
| TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
type def = (* Top-level definition *)
| DEF_type of type_def (* type definition *)
| DEF_fundef of fundef (* function definition *)
| DEF_val of letbind (* value definition *)
| DEF_spec of val_spec (* top-level type constraint *)
| DEF_default of default_spec (* default kind and type assumptions *)
| DEF_scattered of scattered_def (* scattered function and type definition *)
| DEF_reg_dec of typ * id (* register declaration *)
type defs = (* Definition sequence *)
| Defs of list def
|
