Make JetStream 2
[WebKit-https.git] / PerformanceTests / JetStream2 / WSL / SpecWork / WSL.ott
1 metavar x, y, z, f ::=
2 indexvar i, j, k, n, m ::=
3
4 grammar
5 td :: top_level_decl_ ::= {{com top-level declaration}}
6     | tx f <( tparam0 , .. , tparamk )> ( tx0 x0 , .. , txm xm ) { s0 .. sn } :: :: func_decl
7     | typedef x <( tparam0 , .. , tparamk )> = tx ; :: :: typedef
8
9 tparam :: type_parameter_ ::= {{com type parameter}}
10     | tx x :: :: constexpr
11     | x : y0 + .. + yn :: :: type_variable
12
13 s :: stmt_ ::= {{com statement}}
14     | if ( e ) s :: :: if_then {{com Desugared}}
15     | while ( e ) s :: :: while {{com Desugared}}
16     | for ( eOrVDecls ; eOrNothing ; eOrNothing' ) s :: :: for {{com Desugared}}
17     | tx vdecl0 , .. , vdecln ; :: :: multi_vdecls {{com partly desugared}}
18     | ; :: :: empty {{com Desugared}}
19     | if ( e ) s else s' :: :: if
20     | do s while ( e ) ; :: :: do_while
21     | switch ( e ) { sc0 : sblock0 .. scn : sblockn } :: :: switch
22     | break ; :: :: break
23     | continue ; :: :: continue
24     | fallthrough ; :: :: fallthrough
25     | return e ; :: :: return
26     | return ; :: :: return_void
27     | trap ; :: :: trap
28     | { blockAnnot s0 .. sn } :: :: block
29     | e ; :: :: effectful_expr
30     | tval x : sid ; :: :: resolved_vdecl {{com post-monomorphisation variable declaration}}
31     | Loop ( s , s' ) :: :: loop_construct {{com Special, only during execution}}
32     | Cases ( s0 , .. , sn ) :: :: cases_construct {{com Special, only during execution}}
33     | Join ( s ) :: :: join_construct {{com Special, only during execution}}
34
35 sc :: switch_case_ ::=
36     | case rval :: :: case
37     | default :: :: default
38
39 sblock :: switch_block_ ::=
40     | s0 .. sn :: :: statements
41
42 vdecl :: variable_declaration_ ::=
43     | x :: :: uninitialized
44     | x = e :: :: initialized
45
46 eOrVDecls :: expr_or_vdecl_ ::=
47     | e :: :: expr
48     | tx vdecl0 , .. , vdecln :: :: vdecl
49     | :: :: nothing
50
51 eOrNothing :: expr_or_nothing_ ::=
52     | e :: :: expr
53     | :: :: nothing
54
55 blockAnnot :: block_annotation_ ::=
56     | R :: :: exec_env {{tex _{[[R]]} }}
57     | :: :: nothing
58
59 e :: expr_ ::= {{com expression}}
60     | ( e ) :: :: parens
61     | e , e' :: :: comma
62     | e || e' :: :: or {{tex [[e]]\:{||}\:[[e']]}}
63     | e && e' :: :: and {{tex [[e]]\:{\&\&}\:[[e']]}}
64     | e0 ? e1 : e2 :: :: ternary {{tex [[e0]]\:{?}\:[[e1]]:[[e2]]}}
65     | ! e :: :: not {{tex \:![[e]]}}
66     | e == e' :: :: equals_operator
67     | e != e' :: :: not_equals_operator {{com Desugared}} {{tex [[e]]\;!\mkern-\thickmuskip=[[e']]}}
68     | e = e' :: :: assignment
69     | x :: :: variable_name
70     | * e :: :: ptr_deref
71     | & e :: :: address_taking
72     | @ e :: :: array_reference_making
73     | e [ e' stride ] :: :: array_index {{tex [[e]] [ [[e']] ]_{[[stride]]} }}
74     | x <( targ0 , .. , targm )> ( e0 , .. , en ) :: :: call
75     | fid <( rv0 , .. , rvn )> ( e0 , .. , em ) :: :: resolved_call {{com post-monomorphisation, calls are resolved, and pure type arguments are gone}}
76     | val :: :: val {{com only during exec, except literals}}
77     | Call s :: :: call_construct {{com only during exec}}
78     | JoinExpr ( e ) :: :: join_construct {{com only during exec}}
79
80 val :: val_ ::=
81     | rval :: :: rval
82     | LVal ( addr ) :: :: lval
83
84 stride :: stride_ ::=
85     | k :: :: stride {{com stride annotation added during monomorphisation}}
86     | :: :: nothing {{com no stride annotation}}
87
88 addr :: addr_ ::=
89     | addr + i * k :: :: add_multiple_stride
90     | sid :: :: sid
91
92 targ :: type_argument_ ::= {{com type argument}}
93     | x :: :: ident {{com either a type or a constexpr}}
94     | tx :: :: type {{com a type that is not just an identifier}}
95     | x . y :: :: enum_value {{com a field of an enum, for a constexpr type parameter}}
96
97 G {{tex \Gamma}} , Gglobal {{tex \Gamma_{global} }} :: env_ ::= {{com typing environment}}
98     | G [ x -> envMapping ] :: :: update {{com $\Gamma$ with the mapping for x replaced by envMapping}}
99     | { x0 -> envMapping0 , .. , xn -> envMappingn } :: :: set
100
101 envMapping :: env_mapping_ ::= 
102     | t :: :: var {{com $x$ is of type $\tau$}}
103     | SyntaxTypedef ( <( tparam0 , .. , tparamn )> -> tx ) :: :: typedef_syntax {{com resolved before local typing}}
104     | Typedef ( <( tparam0 , .. , tparamn )> -> tval ) :: :: typedef
105     | Func { sig0 , .. , sign } :: :: func {{com $x$ is a function whose signatures are $sig0$ to $sign$}}
106     | SyntaxFunc { sigx0 , .. , sigxn } :: :: func_syntax
107     | Nothing :: :: nothing {{tex \emptyset}} {{com to remove $x$ from $\Gamma$}}
108     | Protocol namedSigs :: :: protocol
109     % TODO: I now believe that this is wrong, and that protocols should live in their own namespace.
110     % Otherwise it is impossible to refer to a protocol as both a type variable (aka Self) and as a constraint on other type variables, when defining its signatures
111
112 namedSigs :: named_signatures_ ::=
113     | { x0 -> sig0 , .. , xn -> sign } :: :: explicit
114     | U namedSigs0 .. namedSigsn :: :: union
115
116 sigx :: signature_syntax_ ::=
117     | <( tparamAnon0 , .. , tparamAnonm )> ( tx0 , .. , txn ) -> tx :: :: sigx
118
119 sig :: signature_ ::=
120     | <( tparamAnon0 , .. , tparamAnonm )> ( tval0 , .. , tvaln ) -> tval :: :: sig
121     % TODO: fix these tparamAnanon, they are clearly wrong.
122
123 tparamAnon :: tparam_anon_ ::=
124     | t :: :: constexpr
125     | { y0 , .. , yn } :: :: tvar 
126
127 B :: behaviour_ ::= {{com statement behaviour}}
128     | { b0 , .. , bn } :: :: set
129     | B + B' :: :: union {{tex [[B]] \cup [[B']]}}
130     | B \ B' :: :: difference {{tex [[B]] \backslash [[B']]}}
131     | U B0 .. Bn :: :: big_union
132     | ( B ) :: :: parens
133
134 b :: single_behaviour_ ::=
135     | Return t :: :: return
136     | Break :: :: break
137     | Continue :: :: continue
138     | Fallthrough :: :: fallthrough
139     | Nothing :: :: Nothing
140
141 t {{tex \tau}} :: type_ ::= {{com type}}
142     | LVal ( tval ) :: :: lval {{com left value}}
143     | tval :: :: tval
144 tval {{tex {\tau^{val} } }} :: type_value_ ::=
145     | Ptr ( tval ) :: :: ptr {{com pointer}}
146     | Ref ( tval ) :: :: array_ref {{com array reference}}
147     | [ tval ] :: :: array {{com array}}
148     | bool :: :: bool
149     | uint32 :: :: uint32 {{tex \textbf{uint32} }}
150     | void :: :: void
151     | TVar tid namedSigs :: :: tvar
152 tx {{tex {\tau^{syntax} } }} :: type_syntactic_ ::= {{com syntactic type}}
153     | x <( targ0 , .. , targm )> :: :: base
154     | tx * addressSpace :: :: ptr
155     | tx [] addressSpace :: :: array_ref 
156     | tx [ i ] :: :: array_fixed_size
157 addressSpace :: address_space_ ::=
158     | thread :: :: thread
159     | threadgroup :: :: threadgroup
160     | device :: :: device
161     | constant :: :: constant
162 tid :: type_identifier_ ::=
163
164 rval, rv :: rval_ ::=
165     | { x0 : rval0 ; .. ; xn : rvaln } :: :: struct
166     | [ rval0 , .. , rvaln ] :: :: array
167     | Ptr ( addr ) :: :: ptr 
168     | Ref ( addr , j ) :: :: ref {{com Reference to array of size j}}
169     | null :: :: lit_null
170     | true :: :: lit_true
171     | false :: :: lit_false
172     | uint :: :: lit_uint {{com unsigned integer literal}}
173     | TrapValue :: :: trap {{com Special, represents a caught error (e.g. out-of-bounds access)}}
174     | Void :: :: void {{com Special, the return value of a void function call}}
175
176 R {{tex \rho}}, Rout {{tex \rho_{out} }} :: exec_env_ ::= {{com execution environment}}
177     | R [ x0 -> val0 , .. , xn -> valn ] :: :: update_with_vals
178     | Empty :: :: empty {{tex \emptyset}}
179
180 E :: memory_event_ ::= {{com memory event}}
181     | :: :: nothing
182     | addr <- rval :: :: store {{com store}}
183     | addr -> rval :: :: load {{com load}}
184     | Sequence ( E0 , .. , En ) :: :: multiple_events
185
186 fid :: function_identifier_ ::=
187
188 S :: stack_event_ ::= {{com stack event}}
189     | :: :: nothing
190     | push ( rval ) :: :: push
191     | pop ( ) :: :: pop
192
193 terminals :: terminals_ ::=
194     | U :: :: big_union {{tex \bigcup}}
195     | |- :: :: vdash {{tex \vdash}}
196     | <- :: :: load {{tex \leftarrow}}
197     | -> :: :: mapsto {{tex \mapsto}}
198     | --> :: :: desugars {{tex \leadsto}}
199     | <( :: :: generic_open {{tex {<} }} % For removing extraneous spaces around '<' and '>' when they are used in that position.
200     | )> :: :: generic_close {{tex {>} }}
201     | in :: :: in {{tex \in}}
202     | \/ :: :: math_or {{tex \vee}}
203     | /\ :: :: math_and {{tex \wedge}}
204     | <= :: :: math_lesser_equal {{tex \leq}}
205     | >= :: :: math_greater_equal {{tex \geq}}
206
207 formula :: formula_ ::=
208     | judgement :: :: judgement
209     | formula0 /\ .. /\ formulan :: :: several_formula
210     | formula \/ formula' :: :: or
211     | n > 0 :: :: int_positive
212     | x -> envMapping in G :: :: env_mapping_exists
213     | x not in G :: :: env_mapping_missing {{tex [[x]] \not\in [[G]]}}
214     | G |- isIntegerOrEnum ( t ) :: :: is_integer
215     | G |- sc0 .. scn fully covers t :: :: full_switch_coverage % TODO: make it explicit
216     | s != s' :: :: stmt_not_eq {{tex [[s]] \neq [[s']]}}
217     | b in B :: :: behaviour_in {{tex [[b]] \in [[B]]}}
218     | b not in B :: :: behaviour_not_in {{tex [[b]] \not\in [[B]]}}
219     | G = G' :: :: typing_env_eq
220     | B = B' :: :: behaviour_eq
221     | namedSigs = namedSigs' :: :: named_signature_eq
222     | sig = sig' :: :: sig_eq
223     | e = e' :: :: expr_eq
224     | e != e' :: :: expr_neq {{tex [[e]] \neq [[e']]}}
225     | exists i . formula :: :: exists_int
226     | tid = makeFresh()  :: :: make_fresh_tid
227     | i = uint :: :: uint_to_indexvar
228     | i <= n :: :: indexvar_leq
229     | i >= n :: :: indexvar_geq
230     | i < n :: :: indexvar_lesser
231     | x -> val in R :: :: val_in_env
232     | fid -> <( x0 , .. , xn )> ( y0 : addr0 , .. , ym : addrm ) { s0 .. sk } :: :: fid_resolving
233     | E = E' :: :: event_eq
234     | R = R' :: :: exec_env_eq
235     | s = s' :: :: stmt_eq
236     | rv not in sc0 .. scn :: :: rval_not_in_cases % TODO: fix typesetting
237     | s = { sblock } :: :: block_from_switch_block
238     | rv = Default ( tval ) :: :: default_value
239     | s is a terminator :: :: stmt_is_terminator
240
241 defns
242 desugaring :: '' ::=
243 defn
244 s --> s' :: :: desugaring_stmt :: '' {{com Desugaring statements}} by
245
246     ----------------------------- :: if_then
247     if (e) s --> if (e) s else {}
248
249     -------- :: empty_stmt
250     ; --> {}
251
252     -------------------------------------- :: while
253     while (e) s --> if (e) do s while (e);
254
255     -------------------------------------------------------------------------- :: for_empty_cond
256     for (eOrVDecls ; ; eOrNothing) s --> for (eOrVDecls ; true ; eOrNothing) s
257
258     --------------------------------------------------------------------------- :: for_empty_incr
259     for (eOrVDecls ; e ; ) s --> for (eOrVDecls ; e ; null) s
260
261     ------------------------------------------------ :: for_init_expr
262     for (e ; e' ; e'') s --> {e; while(e') {s e'';}}
263
264     ------------------------------------------------ :: for_init_empty
265     for ( ; e' ; e'') s --> while(e') {s e'';}
266
267     ------------------------------------------------------------------------------------------ :: for_init_vdecls
268     for (tx vdecl0 , .. , vdecln ; e' ; e'') s --> {tx vdecl0 , .. , vdecln; while(e') {s e'';}}
269
270     k > 0
271     -------------------------------------------------------------------------------------- :: multiple_vdecls
272     { s0..sn tx vdecl0, vdecl1, .., vdeclk; s'0..s'm} --> {s0..sn tx vdecl0; tx vdecl1, .., vdeclk; s'0..s'm}
273
274     ------------------------------------------------------------- :: initialized_vdecl
275     { s0..sn tx x = e; s'0..s'm} --> {s0..sn tx x; x = e; s'0..s'm}
276
277 % TODO: replace foo(e0,..,en) by foo<>(e0,..,en)
278 % Both in expressions, and in top-level declarations
279 % TODO: also desugar syntactic types that have an addressSpace as a prefix.
280 % Also make it an error to have an addressSpace and neither array ref nor ptr.
281 defn
282 e --> e' :: :: desugaring_expr :: '' {{com Desugaring expressions}} by
283     
284     ----------------------- :: not_equals_operator
285     e != e' --> ! (e == e')
286
287 %defns
288 %gather :: '' ::=
289 %defn
290 %G = gather ( td0 .. tdn ) :: :: gather :: '' by
291 %
292 %    G = gather (td0..tdk)
293 %    x -> SyntaxFunc{sigx0, .., sigxi} in G
294 %    G' = G[x -> SyntaxFunc{sigx0, .., sigxi, <( )>(tx0, .., txn) -> tx}]
295 %    -------------------------------------------------------------------- :: func_overload
296 %    G' = gather(tx x <( )> (tx0 x0, .., txn xn) {s0 .. sm} td0..tdk)
297
298 %    G = gather (td0..tdk)
299 %    x not in G
300 %    G' = G[x ->SyntaxFunc{<()>(tx0, .., txn) -> tx}]
301 %    ---------------------------------------------------------------- :: func_no_overload
302 %    G' = gather(tx x <( )> (tx0 x0, .., txn xn) {s0 .. sm} td0..tdk)
303
304 %    G = gather (td0..tdk)
305 %    x not in G
306 %    G' = G[x -> SyntaxTypedef(<()> -> tx)]
307 %    ------------------------------------------ :: typedef
308 %    G' = gather(typedef x <()> = tx; td0..tdk)
309 %    % TODO: add rules for the other kinds of top-level declaration, as well as the base case for an empty file
310 %    % the base case needs to add typedefs for bool/uint32 at the very least
311
312 defns
313 reduce_type :: '' ::=
314 defn
315 G |- tx : tval :: :: syntax :: '' {{com Evaluating types}} {{tex [[G]] [[|-]] [[tx]] \Downarrow [[tval]]}} by
316
317     x -> Typedef (<( )> -> tval) in G
318     ------------------------------- :: basic_typedef
319     G |- x <( )> : tval
320
321     G |- tx : tval
322     ------------------------- :: array
323     G |- tx [i] : [tval]
324
325     G |- tx : tval
326     ---------------------------------------- :: ref
327     G |- tx [] addressSpace : Ref(tval)
328
329     G |- tx : tval
330     --------------------------------------- :: ptr
331     G |- tx * addressSpace : Ptr(tval)
332
333 defns
334 well_formed :: '' ::=
335 defn
336 G |- well_formed ( td ) :: :: top_level :: '' by
337
338     G |- tx : tval
339     G |- {s0..sn} : {Return tval}
340     ---------------------------------- :: func_trivial
341     G |- well_formed(tx f<()>() {s0..sn})
342
343     G |- tx0 : tval
344     G[x0 -> LVal(tval)] |- well_formed (tx f<()>(tx1 x1, .., txm xm) {s0..sn})
345     -------------------------------------------------------------------- :: func_param
346     G |- well_formed (tx f<()>(tx0 x0, tx1 x1, .., txm xm) {s0..sn})
347
348     G |- tx' : tval'
349     G[x -> tval'] |- well_formed (tx f<(tparam0, .., tparamk)> (tx0 x0, .., txm xm) {s0..sn}) 
350     ---------------------------------------------------------------------------------------- :: func_constexpr
351     G |- well_formed (tx f<(tx' x, tparam0, .., tparamk)> (tx0 x0, .., txm xm) {s0..sn}) 
352
353     y0 -> Protocol namedSigs0 in G /\ .. /\ yi -> Protocol namedSigsi in G
354     namedSigs = U namedSigs0 .. namedSigsi
355     tid = makeFresh()
356     G[x -> TVar tid namedSigs] |- well_formed (tx f<(tparam0, .., tparamk)> (tx0 x0, .., txm xm) {s0..sn})
357     ------------------------------------------------------------------------------------------------------ :: func_tvar
358     G |- well_formed (tx f<(x : y0 + .. + yi, tparam0, .., tparamk)> (tx0 x0, .., txm xm) {s0..sn}) 
359     % TODO: maybe add some check here that the different protocols are not incompatible.
360     % Can we even have incompatible protocols?
361
362 defns
363 typing :: '' ::=
364 defn
365 G |- s : B :: :: typing_statement :: '' {{com Validating statements' behaviours}} by
366
367     G |- e : bool
368     G |- s : B
369     G |- s' : B'
370     ------------------------------ :: if
371     G |- if (e) s else s' : B + B'
372
373     G |- e : bool
374     G |- s : B
375     ---------------------------------------------------------- :: do_while
376     G |- do s while (e); : (B \ {Break, Continue}) + {Nothing}
377     % Note: we could make this rule a bit more precise in the cases where we know that s always return/trap/break.. but such a piece of code is almost certainly a bug.
378
379     G |- e : t
380     G |- isIntegerOrEnum(t)
381     G |- sc0: t /\ .. /\ G |- scn: t
382     G |- sc0 .. scn fully covers t
383     G |- sblock0: B0 /\ .. /\ G |- sblockn: Bn
384     Nothing not in B0 /\ .. /\  Nothing not in Bn
385     B = U B0 .. Bn
386     --------------------------------------------------------------------------- :: switch
387     G |- switch (e) {sc0: sblock0 .. scn : sblockn } : B \ {Break, Fallthrough}
388
389     --------------------- :: break
390     G |- break; : {Break}
391
392     --------------------------- :: continue
393     G |- continue; : {Continue}
394
395     --------------------------------- :: fallthrough
396     G |- fallthrough; : {Fallthrough}
397
398     G |- e : t
399     --------------------------- :: return
400     G |- return e; : {Return t}
401
402     ----------------------------- :: return_void
403     G |- return ; : {Return void}
404
405     ----------------------- :: trap
406     G |- trap; : {Return t}
407
408     ------------------- :: empty_block
409     G |- {} : {Nothing}
410
411     G[x -> Nothing] |- tx : tval
412     G[x -> LVal(tval)] |- {s0 .. sn} : B
413     s0 != tx' x; /\../\ sn != tx' x;
414     --------------------------------- :: variable_decl
415     G |- {tx x; s0 .. sn} : B
416     % Note: we remove x from the environment before reducing tx, to avoid a situation where x is required in the definition of tx, which gets rather weird with multiple declarations
417     % (see email from 20/06/2018).
418     % Note: there is a minor ambiguity between this rule and the next two, but it is harmless as the next two rules both fail in the next step
419     % if they are applied where s is a variable declaration.
420     % Note: the second premise prevents redeclaration of a variable in the same scope it was declared in.
421     % Implemented naively it takes O(n**2) to check, but can easily be optimized.
422
423     G |- s : B
424     ------------ :: trivial_block
425     G |- {s} : B
426
427     G |- s : B
428     G |- {s1 .. sn} : B'
429     n > 0
430     Nothing in B
431     -------------------------------------- :: block
432     G |- {s s1 .. sn} : (B \ {Nothing}) + B'
433     % Note: the last premise forbids trivially dead code. It is optional and could be removed with no consequences on the rest of the language.
434
435     G |- e : t
436     ------------------- :: expr
437     G |- e; : {Nothing}
438
439 defn
440 G |- sc : t :: :: typing_switch_case :: '' by
441
442     G |- rval : t
443     --------------- :: case
444     G |- case rval : t
445
446     ---------------- :: default
447     G |- default : t
448
449 defn
450 G |- sblock : B :: :: typing_switch_block :: '' by
451
452     G |- { s0 .. sn } : B
453     --------------------- :: switch_block
454     G |- s0 .. sn : B
455
456 defn
457 G |- e : t :: :: typing_expr :: '' {{com Typing expressions}} by
458     ------------------- :: null_lit_array_ref
459     G |- null : Ref (tval)
460
461     ------------------- :: null_lit_ptr
462     G |- null : Ptr (tval)
463
464     ---------------- :: literal_true
465     G |- true : bool
466
467     ----------------- :: literal_false
468     G |- false : bool
469
470     G |- e : t
471     ------------ :: parens
472     G |- (e) : t
473
474     G |- e : t
475     G |- e' : t'
476     --------------- :: comma
477     G |- e, e' : t'
478
479     G |- e : bool
480     G |- e' : bool
481     ------------------- :: or
482     G |- e || e' : bool
483
484     G |- e : bool
485     G |- e' : bool
486     ------------------- :: and
487     G |- e && e' : bool
488
489     G |- e0 : bool
490     G |- e1 : t
491     G |- e2 : t
492     --------------------- :: ternary
493     G |- e0 ? e1 : e2 : t
494
495     G |- e : bool
496     -------------- :: not
497     G |- !e : bool
498
499     G |- e : LVal(tval)
500     G |- e' : tval
501     ----------------- :: assignment
502     G |- e = e' : tval
503
504     x -> t in G
505     ----------- :: variable_name
506     G |- x : t
507
508     G |- e : LVal(tval)
509     ---------------- :: lval_access
510     G |- e : tval
511
512     G |- e : LVal(tval)
513     ---------------- :: address_taking
514     G |- &e : Ptr(tval)
515     % can the unary operator & be overloaded?
516     % It seems that no
517
518     G |- e : Ptr(tval)
519     ----------------- :: ptr_deref
520     G |- *e : LVal(tval)
521     % can the unary operator * be overloaded?
522     % It seems that no
523
524     % Note: We currently do not have any special interaction between pointers and array references in these rules
525     
526     G |- e : LVal(tval)
527     ---------------- :: take_ref_lval
528     G |- @e : Ref(tval)
529     % Note: in the execution rules, the behaviour depends on whether that LVal points to an array, but here we don't need to track it.
530
531     G |- e : LVal([tval])
532     G |- e' : uint32
533     -------------------- :: array_index_lval
534     G |- e[e'] : LVal(tval)
535
536     G |- e : [tval]
537     G |- e' : uint32
538     ---------------- :: array_index_rval
539     G |- e[e'] : tval
540     % There is a choice between applying array_index_lval and then lval_access, or lval_access and then array_index_rval.
541     % It is not problematic, because the rules are confluent, so either choice leads to the same result.
542     % TODO: should we refuse during validation the case where e' is a constant that falls out of the bounds of e ?
543     % I think it should be an allowed behaviour but not required of the implementation.
544
545     G |- e : Ref(tval)
546     G |- e' : uint32
547     -------------------- :: array_ref_index
548     G |- e[e'] : LVal(tval)
549
550     G |- e0 : tval0 /\../\ G |- en : tvaln
551     x -> Func{sig0, .., sigk} in G
552     exists i . sigi = <( )> (tval0, .., tvaln) -> tval
553     -------------------------------------------------- :: call_no_targ
554     G |- x <( )> (e0, .., en) : tval
555
556 defns
557 exec :: '' ::=
558 defn
559 R |- e -> e' ; E ; S :: :: exec_expr :: '' {{com Small-step reduction on expressions}} {{tex [[R]] \vdash [[e]] \xrightarrow[ [[S]] ]{[[E]]} [[e']]}} by
560
561     ------------------------------------------- :: and_true
562     R |- true && e -> JoinExpr(e) ;; push(true)
563
564     --------------------------- :: and_false
565     R |- false && e -> false ;;
566
567     R |- e0 -> e0' ; E ; S
568     ---------------------------------- :: and_reduce
569     R |- e0 && e1 -> e0' && e1 ; E ; S
570
571     e != LVal(addr)
572     R |- e -> e' ; E ; S
573     --------------------------------------- :: join_expr_reduce
574     R |- JoinExpr(e) -> JoinExpr(e'); E ; S
575
576     ---------------------------------- :: join_expr_elim
577     R |- JoinExpr(val) -> val; ; pop()
578
579     ------------------------- :: or_true
580     R |- true || e -> true ;;
581
582     --------------------------------------------- :: or_false
583     R |- false || e -> JoinExpr(e) ;; push(false)
584
585     R |- e0 -> e0' ; E ; S
586     ---------------------------------- :: or_reduce
587     R |- e0 || e1 -> e0' || e1 ; E ; S
588
589     ------------------------------------------------- :: ternary_true
590     R |- true ? e1 : e2 -> JoinExpr(e1) ;; push(true)
591
592     --------------------------------------------------- :: ternary_false
593     R |- false ? e1 : e2 -> JoinExpr(e2) ;; push(false)
594
595     R |- e0 -> e0' ; E ; S
596     ------------------------------------------ :: ternary_reduce
597     R |- e0 ? e1 : e2 -> e0' ? e1 : e2 ; E ; S
598
599     ---------------------- :: comma_next
600     R |- rval, e1 -> e1 ;;
601
602     R |- e0 -> e0' ; E ; S
603     ------------------------------ :: comma_reduce
604     R |- e0, e1 -> e0', e1 ; E ; S
605
606     ------------------ :: parens_exec
607     R |- ( e ) -> e ;;
608
609     ----------------------- :: not_true
610     R |- ! true -> false ;;
611
612     ----------------------- :: not_false
613     R |- ! false -> true ;;
614
615     --------------------------------- :: deref_ptr
616     R |- * Ptr(addr) -> LVal(addr) ;;
617
618     R |- e -> e' ; E ; S
619     ------------------------ :: deref_reduce
620     R |- * e -> * e' ; E ; S
621
622     e != LVal(addr)
623     R |- e -> e' ; E ; S
624     ------------------------ :: take_ptr_reduce
625     R |- & e -> & e' ; E ; S
626
627     -------------------------------- :: take_ptr_lval
628     R |- & LVal(addr) -> Ptr(addr);;
629
630     % TODO: add the '@' operator. It is tricky, because the monomorphisation pass must annotate it with the resulting size of the reference, basically by rerunning the type checking.
631
632     % TODO: do we want to eliminate the next few rules, and instead put them into the definition of operator[] on the default types?
633     % it would allow for nicer interaction with protocols.
634     e0 != LVal(addr)
635     R |- e0 -> e0' ; E ; S
636     -------------------------------- :: array_left_reduce
637     R |- e0 [e1] -> e0' [e1] ; E ; S
638
639     e0 = LVal(addr) \/ e0 = [rval0, .., rvaln] \/ e0 = Ref(addr, j)
640     R |- e1 -> e1' ; E ; S
641     --------------------------------------------------------------- :: array_right_reduce
642     R |- e0 [e1] -> e0 [e1'] ; E ; S
643     
644     i = uint
645     i <= n
646     ------------------------------------------ :: array_lit_access
647     R |- [rval0, .., rvaln] [uint] -> rvali ;;
648
649     i = uint
650     ----------------------------------------------- :: array_unchecked
651     R |- LVal(addr) [uint k] -> LVal(addr + i*k) ;;
652     % TODO: we will have to add a check either here, or in the local typechecking phase, or in the monomorphisation phase.
653
654     i = uint
655     i < j
656     ------------------------------------------------- :: array_ref_access_valid
657     R |- Ref(addr, j) [uint k] -> LVal(addr + i*k) ;;
658
659     i = uint
660     i >= j
661     ------------------------------------------ :: array_ref_access_invalid
662     R |- Ref(addr, j) [uint k] -> TrapValue ;;
663
664     x -> val in R
665     ---------------- :: environment_access
666     R |- x -> val ;;
667
668     --------------------------------------- :: load
669     R |- LVal(addr) -> rval ; addr -> rval;
670
671     e0 != LVal(addr)
672     R |- e0 -> e0' ; E ; S
673     -------------------------------- :: assign_left_reduce
674     R |- e0 = e1 -> e0' = e1 ; E ; S
675
676     R |- e1 -> e1' ; E ; S
677     ------------------------------------------------ :: assign_right_reduce
678     R |- LVal(addr) = e1 -> LVal(addr) = e1' ; E ; S
679
680     ---------------------------------------------- :: assign_execute
681     R |- LVal(addr) = rval -> rval ; addr <- rval;
682
683     R |- e -> e' ; E ; S
684     ---------------------------------------------------------------------------------------------------------------------- :: call_reduce
685     R |- fid<(rv0, .., rvn)>(rv'0, .., rv'm, e, e0, .., ek) -> fid<(rv0, .., rvn)>(rv'0, .., rv'm, e', e0, .., ek) ; E ; S
686
687     fid -> <(x0, .., xn)>(y0:addr0, .., ym:addrm) {s0 .. sk}
688     E = Sequence(addr0 <- rv'0, .., addrm <- rv'm)
689     R' = R[x0 -> rv0, .., xn -> rvn]
690     R'' = R'[y0 -> LVal(addr0), .., ym -> LVal(addrm)]
691     -------------------------------------------------------------------- :: call_resolve
692     R |- fid<(rv0, .., rvn)>(rv'0, .., rv'm) -> Call {R'' s0 .. sk} ; E;
693
694     R |- s -> s' ; E ; S
695     ------------------------------ :: call_construct_reduce
696     R |- Call s -> Call s' ; E ; S
697
698     --------------------------------- :: call_return
699     R |- Call return rval; -> rval ;;
700
701     ---------------------------- :: call_return_void
702     R |- Call return; -> Void ;;
703
704     ------------------------- :: call_end_function
705     R |- Call {R'} -> Void ;;
706
707 defn
708 R |- s -> s' ; E ; S :: :: exec_stmt :: '' {{com Small-step reduction on statements}} {{tex [[R]] \vdash [[s]] \xrightarrow[ [[S]] ]{[[E]]} [[s']]}} by
709
710     ----------------------------- :: block_annotate
711     R |- {s0..sn} -> {R s0..sn};;
712
713     R |- s -> s' ; E ; S
714     --------------------------------------------- :: block_reduce
715     Rout |- {R s s1..sn} -> {R s' s1..sn} ; E ; S
716
717     --------------------------------------- :: block_next_stmt
718     Rout |- {R {R'} s1..sn} -> {R s1..sn};;
719
720     s = break; \/ s = continue; \/ s = fallthrough; \/ s = return rval; \/ s = return; \/ s = trap;
721     ----------------------------------------------------------------------------------------------- :: block_terminator
722     Rout |- {R s s1..sn} -> s;;
723
724     R' = R[x -> LVal(sid)]
725     rv = Default(tval)
726     ------------------------------------------------------------ :: block_vdecl
727     Rout |- {R tval x : sid; s1..sn} -> {R' s1..sn} ; sid <- rv;
728
729     R |- e -> e' ; E ; S
730     ---------------------- :: effectful_expr_reduce
731     R |- e; -> e'; ; E ; S
732
733     ------------------- :: effectful_expr_elim
734     R |- rval; -> {} ;;
735
736     R |- e -> e' ; E ; S
737     ------------------------------------ :: return_reduce
738     R |- return e; -> return e'; ; E ; S
739
740     R |- e -> e' ; E ; S
741     -------------------------------------------------- :: if_reduce
742     R |- if (e) s else s' -> if (e') s else s' ; E ; S
743
744     ------------------------------------------------- :: if_true
745     R |- if (true) s else s' -> Join(s) ;; push(true)
746     
747     ---------------------------------------------------- :: if_false
748     R |- if (false) s else s' -> Join(s') ;; push(false)
749
750     R |- s -> s' ; E ; S
751     -------------------------------- :: join_reduce
752     R |- Join(s) -> Join(s') ; E ; S
753
754     s = {R'} \/ s is a terminator
755     ----------------------------- :: join_elim
756     R |- Join(s) -> s ;; pop()
757
758     -------------------------------------------------------------- :: do_while_loop
759     R |- do s while(e); -> Loop(s, if(e) do s while(e); else {});;
760
761     R |- s1 -> s1' ; E ; S
762     ------------------------------------------ :: loop_reduce
763     R |- Loop(s1, s2) -> Loop(s1', s2) ; E ; S
764
765     ----------------------------- :: loop_break
766     R |- Loop(break;, s2) -> {};;
767
768     s1 = {R'} \/ s1 = continue;
769     --------------------------- :: loop_next_iteration
770     R |- Loop(s1, s2) -> s2;;
771     
772     s1 = fallthrough; \/ s1 = return; \/ s1 = return rval; \/ s1 = trap;
773     -------------------------------------------------------------------- :: loop_other_terminator
774     R |- Loop(s1, s2) -> s1;;
775
776     R |- e -> e' ; E ; S
777     ---------------------------------------------------------------------------------------------- :: switch_reduce
778     R |- switch(e) {sc0:sblock0 .. scn:sblockn} -> switch(e') {sc0:sblock0 .. scn:sblockn} ; E ; S
779
780 %TODO: the next two rules don't fit on the page. I should find a way to compact them. Maybe with the </xi//i/> notation? 
781     s = {sblock} /\ s0 = {sblock'0} /\ .. /\ sm = {sblock'm}
782     ------------------------------------------------------------------------------------------------------------------------------- :: switch_case_found
783     R |- switch(rv) {sc0:sblock0 .. scn:sblockn case rv: sblock sc'0:sblock'0 .. sc'm:sblock'm} -> Cases(s, s0, .., sm) ;; push(rv)
784
785     rv not in sc0 .. scn
786     rv not in sc'0 .. sc'm
787     s = {sblock} /\ s0 = {sblock'0} /\ .. /\ sm = {sblock'm}
788     ------------------------------------------------------------------------------------------------------------------------------- :: switch_default
789     R |- switch(rv) {sc0:sblock0 .. scn:sblockn default: sblock sc'0:sblock'0 .. sc'm:sblock'm} -> Cases(s, s0, .., sm) ;; push(rv)
790
791     R |- s -> s' ; E ; S
792     ------------------------------------------------------ :: cases_reduce
793     R |- Cases(s, s0, .., sn) -> Cases(s', s0, .., sn) ; E ; S
794
795     ----------------------------------------------------------- :: cases_fallthrough
796     R |- Cases(fallthrough;, s0, .., sn) -> Cases(s0, .., sn);;
797
798     --------------------------------------------- :: cases_break
799     R |- Cases(break;, s0, .., sn) -> {} ;; pop()
800
801     s = continue; \/ s = return; \/ s = return rval; \/ s = trap;
802     ------------------------------------------------------------- :: cases_other_terminator
803     R |- Cases(s, s0, .., sn) -> s ;; pop()