[WSL] Merge WSL_type.ott and WSL_exec.ott
authorrmorisset@apple.com <rmorisset@apple.com@268f45cc-cd09-0410-ab3c-d52691b4dbfc>
Thu, 21 Jun 2018 16:44:07 +0000 (16:44 +0000)
committerrmorisset@apple.com <rmorisset@apple.com@268f45cc-cd09-0410-ab3c-d52691b4dbfc>
Thu, 21 Jun 2018 16:44:07 +0000 (16:44 +0000)
https://bugs.webkit.org/show_bug.cgi?id=186310

Rubberstamped by Filip Pizlo.

I moved the execution rules into WSL_type.ott, that was renamed WSL.ott.
I also changed the execution judgements:
- they now emit memory events instead of having an explicit store (so they can be connected later to a memory model)
- the environment is now unchangeable (except inside blocks, which are the only place that variable declarations can appear)
- various rules were simplified.

* WebGPUShadingLanguageRI/SpecWork/WSL.ott: Copied from Tools/WebGPUShadingLanguageRI/SpecWork/WSL_type.ott.
* WebGPUShadingLanguageRI/SpecWork/WSL_exec.ott: Removed.
* WebGPUShadingLanguageRI/SpecWork/WSL_type.ott: Removed.

git-svn-id: https://svn.webkit.org/repository/webkit/trunk@233041 268f45cc-cd09-0410-ab3c-d52691b4dbfc

Tools/ChangeLog
Tools/WebGPUShadingLanguageRI/SpecWork/WSL.ott [moved from Tools/WebGPUShadingLanguageRI/SpecWork/WSL_type.ott with 60% similarity]
Tools/WebGPUShadingLanguageRI/SpecWork/WSL_exec.ott [deleted file]

index b283c49..ffcd90b 100644 (file)
@@ -1,3 +1,20 @@
+2018-06-21  Robin Morisset  <rmorisset@apple.com>
+
+        [WSL] Merge WSL_type.ott and WSL_exec.ott
+        https://bugs.webkit.org/show_bug.cgi?id=186310
+
+        Rubberstamped by Filip Pizlo.
+
+        I moved the execution rules into WSL_type.ott, that was renamed WSL.ott.
+        I also changed the execution judgements:
+        - they now emit memory events instead of having an explicit store (so they can be connected later to a memory model)
+        - the environment is now unchangeable (except inside blocks, which are the only place that variable declarations can appear)
+        - various rules were simplified.
+
+        * WebGPUShadingLanguageRI/SpecWork/WSL.ott: Copied from Tools/WebGPUShadingLanguageRI/SpecWork/WSL_type.ott.
+        * WebGPUShadingLanguageRI/SpecWork/WSL_exec.ott: Removed.
+        * WebGPUShadingLanguageRI/SpecWork/WSL_type.ott: Removed.
+
 2018-06-21  Leo Balter  <leonardo.balter@gmail.com>
 
         [test262-runner] Improve failures output
@@ -15,7 +15,6 @@ s :: stmt_ ::= {{com statement}}
     | while ( e ) s :: :: while {{com Desugared}}
     | for ( eOrVDecls ; eOrNothing ; eOrNothing' ) s :: :: for {{com Desugared}}
     | tx vdecl0 , .. , vdecln ; :: :: multi_vdecls {{com partly desugared}}
-    % TODO: instead of a type, we should have the elements of a type here, and explicitely resolve typedefs, since they can be shadowed, and need to be in the typing environment
     | ; :: :: empty {{com Desugared}}
     | if ( e ) s else s' :: :: if
     | do s while ( e ) ; :: :: do_while
@@ -26,11 +25,14 @@ s :: stmt_ ::= {{com statement}}
     | return e ; :: :: return
     | return ; :: :: return_void
     | trap ; :: :: trap
-    | { s0 .. sn } :: :: block
+    | { blockAnnot s0 .. sn } :: :: block
     | e ; :: :: effectful_expr
+    | x : sid ; :: :: resolved_vdecl {{com post-monomorphisation variable declaration}}
+    | Loop ( s , s' ) :: :: loop_construct {{com Special, only during execution}}
+    | Cases ( s0 , .. , sn ) :: :: cases_construct {{com Special, only during execution}}
 
 sc :: switch_case_ ::=
-    | case e :: :: case
+    | case rval :: :: case
     | default :: :: default
 
 sblock :: switch_block_ ::=
@@ -49,6 +51,10 @@ eOrNothing :: expr_or_nothing_ ::=
     | e :: :: expr
     | :: :: nothing
 
+blockAnnot :: block_annotation_ ::=
+    | R :: :: exec_env {{tex _{[[R]]} }}
+    | :: :: nothing
+
 e :: expr_ ::= {{com expression}}
     | ( e ) :: :: parens
     | e , e' :: :: comma
@@ -63,10 +69,23 @@ e :: expr_ ::= {{com expression}}
     | * e :: :: ptr_deref
     | & e :: :: address_taking
     | @ e :: :: array_reference_making
-    | e [ e' ] :: :: array_index
+    | e [ e' stride ] :: :: array_index {{tex [[e]] [ [[e']] ]_{[[stride]]} }}
     | x <( targ0 , .. , targm )> ( e0 , .. , en ) :: :: call
-    | rval :: :: rval {{com only during exec, except literals}}
-    | LVal ( sid ) :: :: lval {{com only during exec}}
+    | fid <( rv0 , .. , rvn )> ( e0 , .. , em ) :: :: resolved_call {{com post-monomorphisation, calls are resolved, and pure type arguments are gone}}
+    | val :: :: val {{com only during exec, except literals}}
+    | Call s :: :: call_construct {{com only during exec}}
+
+val :: val_ ::=
+    | rval :: :: rval
+    | LVal ( addr ) :: :: lval
+
+stride :: stride_ ::=
+    | k :: :: stride {{com stride annotation added during monomorphisation}}
+    | :: :: nothing {{com no stride annotation}}
+
+addr :: addr_ ::=
+    | addr + i * k :: :: add_multiple_stride
+    | sid :: :: sid
 
 targ :: type_argument_ ::= {{com type argument}}
     | x :: :: ident {{com either a type or a constexpr}}
@@ -143,22 +162,26 @@ tid :: type_identifier_ ::=
 rval, rv :: rval_ ::=
     | { x0 : rval0 ; .. ; xn : rvaln } :: :: struct
     | [ rval0 , .. , rvaln ] :: :: array
-    | Ptr ( sid ) :: :: ptr
-    | Ref ( sid , i ) :: :: ref
-    | Void :: :: void {{com Special, the value returned by calls to void functions}}
+    | Ptr ( addr ) :: :: ptr 
+    | Ref ( addr , j ) :: :: ref {{com Reference to array of size j}}
     | null :: :: lit_null
     | true :: :: lit_true
     | false :: :: lit_false
+    | uint :: :: lit_uint {{com unsigned integer literal}}
+    | TrapValue :: :: trap {{com Special, represents a caught error (e.g. out-of-bounds access)}}
+    | Void :: :: void {{com Special, the return value of a void function call}}
 
-R {{tex \rho}} :: exec_env_ ::= {{com execution environment}}
-    | R [ x -> rval ] :: :: update_with_rval
-    | R [ x -> LVal ( sid ) ] :: :: update_with_lval
+R {{tex \rho}}, Rout {{tex \rho_{out} }} :: exec_env_ ::= {{com execution environment}}
+    | R [ x0 -> val0 , .. , xn -> valn ] :: :: update_with_vals
     | Empty :: :: empty {{tex \emptyset}}
 
 E :: memory_event_ ::= {{com memory event}}
     | :: :: nothing
-    | sid <- rval :: :: store {{com store}}
-    | sid -> rval :: :: load {{com load}}
+    | addr <- rval :: :: store {{com store}}
+    | addr -> rval :: :: load {{com load}}
+    | Sequence ( E0 , .. , En ) :: :: multiple_events
+
+fid :: function_identifier_ ::=
 
 terminals :: terminals_ ::=
     | U :: :: big_union {{tex \bigcup}}
@@ -169,10 +192,15 @@ terminals :: terminals_ ::=
     | <( :: :: generic_open {{tex {<} }} % For removing extraneous spaces around '<' and '>' when they are used in that position.
     | )> :: :: generic_close {{tex {>} }}
     | in :: :: in {{tex \in}}
+    | \/ :: :: math_or {{tex \vee}}
+    | /\ :: :: math_and {{tex \wedge}}
+    | <= :: :: math_lesser_equal {{tex \leq}}
+    | >= :: :: math_greater_equal {{tex \geq}}
 
 formula :: formula_ ::=
     | judgement :: :: judgement
-    | formula0 .. formulan :: :: several_formula
+    | formula0 /\ .. /\ formulan :: :: several_formula
+    | formula \/ formula' :: :: or
     | n > 0 :: :: int_positive
     | x -> envMapping in G :: :: env_mapping_exists
     | x not in G :: :: env_mapping_missing {{tex [[x]] \not\in [[G]]}}
@@ -185,8 +213,21 @@ formula :: formula_ ::=
     | B = B' :: :: behaviour_eq
     | namedSigs = namedSigs' :: :: named_signature_eq
     | sig = sig' :: :: sig_eq
-    | exists i . ( formula ) :: :: exists_int
+    | e = e' :: :: expr_eq
+    | e != e' :: :: expr_neq {{tex [[e]] \neq [[e']]}}
+    | exists i . formula :: :: exists_int
     | tid = makeFresh()  :: :: make_fresh_tid
+    | i = uint :: :: uint_to_indexvar
+    | i <= n :: :: indexvar_leq
+    | i >= n :: :: indexvar_geq
+    | i < n :: :: indexvar_lesser
+    | x -> val in R :: :: val_in_env
+    | fid -> <( x0 , .. , xn )> ( y0 : addr0 , .. , ym : addrm ) { s0 .. sk } :: :: fid_resolving
+    | E = E' :: :: event_eq
+    | R = R' :: :: exec_env_eq
+    | s = s' :: :: stmt_eq
+    | rv not in sc0 .. scn :: :: rval_not_in_cases
+    | s = { sblock } :: :: block_from_switch_block
 
 defns
 desugaring :: '' ::=
@@ -234,35 +275,35 @@ e --> e' :: :: desugaring_expr :: '' {{com Desugaring expressions}} by
     ----------------------- :: not_equals_operator
     e != e' --> ! (e == e')
 
-defns
-gather :: '' ::=
-defn
-G = gather ( td0 .. tdn ) :: :: gather :: '' by
-
-    G = gather (td0..tdk)
-    x -> SyntaxFunc{sigx0, .., sigxi} in G
-    G' = G[x -> SyntaxFunc{sigx0, .., sigxi, <( )>(tx0, .., txn) -> tx}]
-    -------------------------------------------------------------------- :: func_overload
-    G' = gather(tx x <( )> (tx0 x0, .., txn xn) {s0 .. sm} td0..tdk)
-
-    G = gather (td0..tdk)
-    x not in G
-    G' = G[x ->SyntaxFunc{<()>(tx0, .., txn) -> tx}]
-    ---------------------------------------------------------------- :: func_no_overload
-    G' = gather(tx x <( )> (tx0 x0, .., txn xn) {s0 .. sm} td0..tdk)
-
-    G = gather (td0..tdk)
-    x not in G
-    G' = G[x -> SyntaxTypedef(<()> -> tx)]
-    ------------------------------------------ :: typedef
-    G' = gather(typedef x <()> = tx; td0..tdk)
-    % TODO: add rules for the other kinds of top-level declaration, as well as the base case for an empty file
-    % the base case needs to add typedefs for bool/uint32 at the very least
+%defns
+%gather :: '' ::=
+%defn
+%G = gather ( td0 .. tdn ) :: :: gather :: '' by
+%
+%    G = gather (td0..tdk)
+%    x -> SyntaxFunc{sigx0, .., sigxi} in G
+%    G' = G[x -> SyntaxFunc{sigx0, .., sigxi, <( )>(tx0, .., txn) -> tx}]
+%    -------------------------------------------------------------------- :: func_overload
+%    G' = gather(tx x <( )> (tx0 x0, .., txn xn) {s0 .. sm} td0..tdk)
+% 
+%    G = gather (td0..tdk)
+%    x not in G
+%    G' = G[x ->SyntaxFunc{<()>(tx0, .., txn) -> tx}]
+%    ---------------------------------------------------------------- :: func_no_overload
+%    G' = gather(tx x <( )> (tx0 x0, .., txn xn) {s0 .. sm} td0..tdk)
+% 
+%    G = gather (td0..tdk)
+%    x not in G
+%    G' = G[x -> SyntaxTypedef(<()> -> tx)]
+%    ------------------------------------------ :: typedef
+%    G' = gather(typedef x <()> = tx; td0..tdk)
+%    % TODO: add rules for the other kinds of top-level declaration, as well as the base case for an empty file
+%    % the base case needs to add typedefs for bool/uint32 at the very least
 
 defns
 reduce_type :: '' ::=
 defn
-G |- tx : tval :: :: syntax :: '' {{tex [[G]] [[|-]] [[tx]] \Downarrow [[tval]]}} by
+G |- tx : tval :: :: syntax :: '' {{com Evaluating types}} {{tex [[G]] [[|-]] [[tx]] \Downarrow [[tval]]}} by
 
     x -> Typedef (<( )> -> tval) in G
     ------------------------------- :: basic_typedef
@@ -300,7 +341,7 @@ G |- well_formed ( td ) :: :: top_level :: '' by
     ---------------------------------------------------------------------------------------- :: func_constexpr
     G |- well_formed (tx f<(tx' x, tparam0, .., tparamk)> (tx0 x0, .., txm xm) {s0..sn}) 
 
-    y0 -> Protocol namedSigs0 in G .. yi -> Protocol namedSigsi in G
+    y0 -> Protocol namedSigs0 in G /\ .. /\ yi -> Protocol namedSigsi in G
     namedSigs = U namedSigs0 .. namedSigsi
     tid = makeFresh()
     G[x -> TVar tid namedSigs] |- well_formed (tx f<(tparam0, .., tparamk)> (tx0 x0, .., txm xm) {s0..sn})
@@ -312,7 +353,7 @@ G |- well_formed ( td ) :: :: top_level :: '' by
 defns
 typing :: '' ::=
 defn
-G |- s : B :: :: typing_statement :: '' by
+G |- s : B :: :: typing_statement :: '' {{com Validating statements' behaviours}} by
 
     G |- e : bool
     G |- s : B
@@ -328,10 +369,10 @@ G |- s : B :: :: typing_statement :: '' by
 
     G |- e : t
     G |- isIntegerOrEnum(t)
-    G |- sc0: t .. G |- scn: t
+    G |- sc0: t /\ .. /\ G |- scn: t
     G |- sc0 .. scn fully covers t
-    G |- sblock0: B0 .. G |- sblockn: Bn
-    Nothing not in B0 .. Nothing not in Bn
+    G |- sblock0: B0 /\ .. /\ G |- sblockn: Bn
+    Nothing not in B0 /\ .. /\  Nothing not in Bn
     B = U B0 .. Bn
     --------------------------------------------------------------------------- :: switch
     G |- switch (e) {sc0: sblock0 .. scn : sblockn } : B \ {Break, Fallthrough}
@@ -360,7 +401,7 @@ G |- s : B :: :: typing_statement :: '' by
 
     G[x -> Nothing] |- tx : tval
     G[x -> LVal(tval)] |- {s0 .. sn} : B
-    s0 != tx' x; .. sn != tx' x;
+    s0 != tx' x; /\../\ sn != tx' x;
     --------------------------------- :: variable_decl
     G |- {tx x; s0 .. sn} : B
     % 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
@@ -389,9 +430,9 @@ G |- s : B :: :: typing_statement :: '' by
 defn
 G |- sc : t :: :: typing_switch_case :: '' by
 
-    G |- e : t
+    G |- rval : t
     --------------- :: case
-    G |- case e : t
+    G |- case rval : t
 
     ---------------- :: default
     G |- default : t
@@ -404,8 +445,7 @@ G |- sblock : B :: :: typing_switch_block :: '' by
     G |- s0 .. sn : B
 
 defn
-G |- e : t :: :: typing_expr :: '' by
-% TODO: should I split this into two judgements, one that reduces to type (and stops at LVal) and one that reduces to type_val?
+G |- e : t :: :: typing_expr :: '' {{com Typing expressions}} by
     ------------------- :: null_lit_array_ref
     G |- null : Ref (tval)
 
@@ -498,16 +538,16 @@ G |- e : t :: :: typing_expr :: '' by
     -------------------- :: array_ref_index
     G |- e[e'] : LVal(tval)
 
-    G |- e0 : tval0 .. G |- en : tvaln
+    G |- e0 : tval0 /\../\ G |- en : tvaln
     x -> Func{sig0, .., sigk} in G
-    exists i . (sigi = <( )> (tval0, .., tvaln) -> tval)
-    ---------------------------------------------------- :: call_no_targ
+    exists i . sigi = <( )> (tval0, .., tvaln) -> tval
+    -------------------------------------------------- :: call_no_targ
     G |- x <( )> (e0, .., en) : tval
 
 defns
 exec :: '' ::=
 defn
-R |- e -> e' ; E :: :: exec_expr :: '' {{tex [[R]] \vdash [[e]] \xrightarrow{[[E]]} [[e']]}} by
+R |- e -> e' ; E :: :: exec_expr :: '' {{com Small-step reduction on expressions}} {{tex [[R]] \vdash [[e]] \xrightarrow{[[E]]} [[e']]}} by
 
     --------------------- :: and_true
     R |- true && e -> e ;
@@ -523,7 +563,7 @@ R |- e -> e' ; E :: :: exec_expr :: '' {{tex [[R]] \vdash [[e]] \xrightarrow{[[E
     R |- true || e -> true ;
 
     ---------------------- :: or_false
-    R |- false && e -> e ;
+    R |- false || e -> e ;
 
     R |- e0 -> e0' ; E
     ------------------------------ :: or_reduce
@@ -555,11 +595,182 @@ R |- e -> e' ; E :: :: exec_expr :: '' {{tex [[R]] \vdash [[e]] \xrightarrow{[[E
     ---------------------- :: not_false
     R |- ! false -> true ;
 
-    ------------------------------ :: deref_ptr
-    R |- * Ptr(sid) -> LVal(sid) ;
+    -------------------------------- :: deref_ptr
+    R |- * Ptr(addr) -> LVal(addr) ;
 
     R |- e -> e' ; E
     -------------------- :: deref_reduce
     R |- * e -> * e' ; E
 
+    e != LVal(addr)
+    R |- e -> e' ; E
+    -------------------- :: take_ptr_reduce
+    R |- & e -> & e' ; E
+
+    ------------------------------- :: take_ptr_lval
+    R |- & LVal(addr) -> Ptr(addr);
+
+    % 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.
+
+    % TODO: do we want to eliminate the next few rules, and instead put them into the definition of operator[] on the default types?
+    % it would allow for nicer interaction with protocols.
+    e0 != LVal(addr)
+    R |- e0 -> e0' ; E
+    ---------------------------- :: array_left_reduce
+    R |- e0 [e1] -> e0' [e1] ; E
+
+    e0 = LVal(addr) \/ e0 = [rval0, .., rvaln] \/ e0 = Ref(addr, j)
+    R |- e1 -> e1' ; E
+    --------------------------------------------------------------- :: array_right_reduce
+    R |- e0 [e1] -> e0 [e1'] ; E
+    
+    i = uint
+    i <= n
+    ----------------------------------------- :: array_lit_access
+    R |- [rval0, .., rvaln] [uint] -> rvali ;
+
+    i = uint
+    ---------------------------------------------- :: array_unchecked
+    R |- LVal(addr) [uint k] -> LVal(addr + i*k) ;
+    % TODO: we will have to add a check either here, or in the local typechecking phase, or in the monomorphisation phase.
+
+    i = uint
+    i < j
+    ------------------------------------------------ :: array_ref_access_valid
+    R |- Ref(addr, j) [uint k] -> LVal(addr + i*k) ;
+
+    i = uint
+    i >= j
+    ----------------------------------------- :: array_ref_access_invalid
+    R |- Ref(addr, j) [uint k] -> TrapValue ;
+
+    x -> val in R
+    --------------- :: environment_access
+    R |- x -> val ;
+
+    -------------------------------------- :: load
+    R |- LVal(addr) -> rval ; addr -> rval
+
+    e0 != LVal(addr)
+    R |- e0 -> e0' ; E
+    ---------------------------- :: assign_left_reduce
+    R |- e0 = e1 -> e0' = e1 ; E
+
+    R |- e1 -> e1' ; E
+    -------------------------------------------- :: assign_right_reduce
+    R |- LVal(addr) = e1 -> LVal(addr) = e1' ; E
+
+    --------------------------------------------- :: assign_execute
+    R |- LVal(addr) = rval -> rval ; addr <- rval
+
+    R |- e -> e' ; E
+    ---------------- :: call_reduce
+    R |- fid<(rv0, .., rvn)>(rv'0, .., rv'm, e, e0, .., ek) -> fid<(rv0, .., rvn)>(rv'0, .., rv'm, e', e0, .., ek) ; E
+
+    fid -> <(x0, .., xn)>(y0:addr0, .., ym:addrm) {s0 .. sk}
+    E = Sequence(addr0 <- rv'0, .., addrm <- rv'm)
+    R' = R[x0 -> rv0, .., xn -> rvn]
+    R'' = R'[y0 -> LVal(addr0), .., ym -> LVal(addrm)]
+    ------------------------------------------------------------------- :: call_resolve
+    R |- fid<(rv0, .., rvn)>(rv'0, .., rv'm) -> Call {R'' s0 .. sk} ; E
+
+    R |- s -> s' ; E
+    -------------------------- :: call_construct_reduce
+    R |- Call s -> Call s' ; E
+
+    -------------------------------- :: call_return
+    R |- Call return rval; -> rval ;
+
+    --------------------------- :: call_return_void
+    R |- Call return; -> Void ;
+
+    ---------------------- :: call_end_function
+    R |- Call {R'} -> Void ;
+
+defn
+R |- s -> s' ; E :: :: exec_stmt :: '' {{com Small-step reduction on statements}} {{tex [[R]] \vdash [[s]] \xrightarrow{[[E]]} [[s']]}} by
+
+    ---------------------------- :: block_annotate
+    R |- {s0..sn} -> {R s0..sn};
+
+    R |- s -> s' ; E
+    ----------------------------------------- :: block_reduce
+    Rout |- {R s s1..sn} -> {R s' s1..sn} ; E
+
+    -------------------------------------- :: block_next_stmt
+    Rout |- {R {R'} s1..sn} -> {R s1..sn};
+
+    s = break; \/ s = continue; \/ s = fallthrough; \/ s = return rval; \/ s = return; \/ s = trap;
+    ---------------------------------------------------------------------------------------------- :: block_terminator
+    Rout |- {R s s1..sn} -> s;
+
+    R' = R[x -> LVal(sid)]
+    ------------------------------------------- :: block_vdecl
+    Rout |- {R x : sid; s1..sn} -> {R' s1..sn};
+
+    R |- e -> e' ; E
+    ------------------ :: effectful_expr_reduce
+    R |- e; -> e'; ; E
+
+    ------------------ :: effectful_expr_elim
+    R |- rval; -> {} ;
+
+    R |- e -> e' ; E
+    -------------------------------- :: return_reduce
+    R |- return e; -> return e'; ; E
+
+    R |- e -> e' ; E
+    ---------------------------------------------- :: if_reduce
+    R |- if (e) s else s' -> if (e') s else s' ; E
+
+    ------------------------------ :: if_true
+    R |- if (true) s else s' -> s;
+    
+    -------------------------------- :: if_false
+    R |- if (false) s else s' -> s';
+
+    ------------------------------------------------------------- :: do_while_loop
+    R |- do s while(e); -> Loop(s, if(e) do s while(e); else {});
+
+    R |- s1 -> s1' ; E
+    -------------------------------------- :: loop_reduce
+    R |- Loop(s1, s2) -> Loop(s1', s2) ; E
+
+    ---------------------------- :: loop_break
+    R |- Loop(break;, s2) -> {};
+
+    s1 = {R'} \/ s1 = continue;
+    --------------------------- :: loop_next_iteration
+    R |- Loop(s1, s2) -> s2;
+    
+    s1 = fallthrough; \/ s1 = return; \/ s1 = return rval; \/ s1 = trap;
+    -------------------------------------------------------------------- :: loop_other_terminator
+    R |- Loop(s1, s2) -> s1;
+
+    R |- e -> e' ; E
+    ------------------------------------------------------------------------------------------ :: switch_reduce
+    R |- switch(e) {sc0:sblock0 .. scn:sblockn} -> switch(e') {sc0:sblock0 .. scn:sblockn} ; E
+
+    s = {sblock} /\ s0 = {sblock'0} /\ .. /\ sm = {sblock'm}
+    -------------------------------------------------------------------------------------------------------------------- :: switch_case_found
+    R |- switch(rv) {sc0:sblock0 .. scn:sblockn case rv: sblock sc'0:sblock'0 .. sc'm:sblock'm} -> Cases(s, s0, .., sm);
+
+    rv not in sc0 .. scn
+    rv not in sc'0 .. sc'm
+    s = {sblock} /\ s0 = {sblock'0} /\ .. /\ sm = {sblock'm}
+    -------------------------------------------------------------------------------------------------------------------- :: switch_default
+    R |- switch(rv) {sc0:sblock0 .. scn:sblockn default: sblock sc'0:sblock'0 .. sc'm:sblock'm} -> Cases(s, s0, .., sm);
+
+    R |- s -> s' ; E
+    ------------------------------------------------------ :: cases_reduce
+    R |- Cases(s, s0, .., sn) -> Cases(s', s0, .., sn) ; E
+
+    --------------------------------------------------------- :: cases_fallthrough
+    R |- Cases(fallthrough;, s0, .., sn) -> Cases(s0, .., sn);
+
+    ------------------------------------ :: cases_break
+    R |- Cases(break;, s0, .., sn) -> {};
 
+    s = continue; \/ s = return; \/ s = return rval; \/ s = trap;
+    ------------------------------------------------------------- :: cases_other_terminator
+    R |- Cases(s, s0, .., sn) -> s;
diff --git a/Tools/WebGPUShadingLanguageRI/SpecWork/WSL_exec.ott b/Tools/WebGPUShadingLanguageRI/SpecWork/WSL_exec.ott
deleted file mode 100644 (file)
index 881df2e..0000000
+++ /dev/null
@@ -1,376 +0,0 @@
-metavar x, y ::= {{ com variable name }}
-indexvar index, i, j, k, n, m ::=
-
-grammar
-s :: 'stmt_' ::= {{com statement}}
-    | if ( e ) s :: :: if_then
-    | if ( e ) s else s' :: :: if_then_expr
-    | while ( e ) s :: :: while
-    | do s while ( e ) ; :: :: do_while
-    | for ( epre ; econd ; eincr ) s :: :: for_expr
-    | for ( vdecls ; econd ; eincr ) s :: :: for_vdecls
-    | switch ( e ) { se0 .. sen } :: :: switch
-    | break ; :: :: break
-    | continue ; :: :: continue
-    | fallthrough ; :: :: fallthrough
-    | return e ; :: :: return
-    | { s0 .. sn } :: :: block
-    | { G s0 .. sn } :: :: block_annotated {{com Special, annotated block}}
-    %TODO: find a clean way of making G be a subscript of the opening brace
-    | Loop ( s1 , s2 ) :: :: loop {{com Special, loop construct}}
-    | Cases ( sblock0 , .. , sblockn ) :: :: cases {{com Special, switch-cases construct}}
-    | vdecls ; :: :: variables_declaration {{com variables declaration}}
-    | e ; :: :: effectful_expr {{com effectful expr}}
-    | ; :: :: nil {{tex \emptyset ; }} {{com empty statement}}
-
-se :: 'switch_elem_' ::= {{com switch element}}
-    | case rval : sblock :: :: case
-    | default : sblock :: :: default
-
-sblock :: 'sblock_' ::= {{com Special block with no effect on scoping, used for switches}}
-    | s0 .. sn :: :: stmt_list
-
-e, epre {{tex e_{pre} }}, econd {{tex e_{cond} }}, eincr {{tex e_{incr} }} :: 'expr_' ::= {{com expression}}
-    | e || e' :: :: or
-    | e && e' :: :: and
-    | e ? e1 : e2 :: :: ternary
-    | Comma ( e0 , .. , en ) :: :: comma {{com Comma is just a way to disambiguate this in the rules}}
-    | e = e' :: :: assignment
-    | x :: :: identifier
-    | fid < rval0 , .. , rvaln > ( e0 , .. , em ) :: :: call
-    % TODO: way too much space around '<' and '>'
-    | Call s :: :: call_construct {{com Special, call construct}}
-    | e [ e' ] :: :: array_access % TODO: add the rules for that one
-    | True :: :: true
-    | False :: :: false
-    | Void :: :: void {{com Special, void value}}
-    | { x0 : rval0 ; .. ; xn : rvaln } :: :: struct
-    | [ rval0 , .. , rvaln ] :: :: array
-    | sid offset0 .. offsetn :: :: sid {{com Special, store location}}
-
-fid :: 'fid_' ::= {{com function identifier}}
-
-v :: 'val_' ::= {{com value}}
-    | True :: :: true
-    | False :: :: false
-    | Void :: :: void {{com Special, void value}}
-    | { x0 : rval0 ; .. ; xn : rvaln } :: :: struct
-    | [ rval0 , .. , rvaln ] :: :: array
-    | sid offset0 .. offsetn :: :: sid {{com Special, store location}}
-
-rval, rv :: 'rval_' ::= {{com right-side value}}
-    | True :: :: true
-    | False :: :: false
-    | Void :: :: void {{com Special, void value}}
-    | { x0 : rval0 ; .. ; xn : rvaln } :: :: struct
-    | [ rval0 , .. , rvaln ] :: :: array
-
-lval :: 'lval_' ::= {{com left-side value}}
-    | sid offset0 .. offsetn :: :: sid {{com Special, store location}}
-
-offset :: 'offset_' ::=
-    | . x :: :: field {{com field offset}}
-    | [ i ] :: :: array {{com array offset}}
-
-vdecls :: 'vdecls_' ::= {{com variables declaration}}
-    | t vdecl1 , .. , vdecln :: :: vdecls
-
-t {{tex \tau}} :: 'type_' ::= {{com type}}
-    | bool :: :: bool
-
-vdecl :: vdecl' ::=
-    | x : sid :: :: uninitialized
-    | x : sid = e :: :: initialized
-
-sid :: 'sid' ::= {{com store identifier}}
-
-G {{tex \Gamma}}, Gout {{tex \Gamma_{out} }}, Gglobal {{tex \Gamma_{global} }} :: 'gamma_' ::= {{com environment}}
-    | Empty :: :: empty {{ tex \emptyset }} 
-    | G [ envMapping0 , .. , envMappingn ] :: :: update
-
-envMapping :: 'env_mapping_' ::= {{com environment mapping}}
-    | x -> sid :: :: in_store {{com in store}} {{tex [[x]] \mapsto [[sid]]}}
-    | x -> rval :: :: constexpr {{com constexpr}} {{tex [[x]] \mapsto [[rval]]}}
-
-S {{tex \Sigma}} :: 'sigma_' ::= {{com store}}
-    | Empty :: :: empty {{ tex \emptyset }}
-    | S [ storeMapping0 , .. , storeMappingn ] :: :: update
-
-storeMapping :: 'store_mapping_' ::= {{com store mapping}}
-    | sid -> rval :: :: mapping {{tex [[sid]] \mapsto [[rval]]}}
-
-formula :: formula_ ::=  
-    | judgement :: :: judgement
-    | rval = Default ( t ) :: :: default_value
-    | rval = rval' :: :: rval_equality
-    | isNotLVal ( e ) :: :: is_not_lval
-    | sid -> rval in S :: :: mapping_in_store {{tex ([[sid]] \mapsto [[rval]]) \in [[S]] }}
-    | x -> sid in G :: :: mapping_in_env {{tex ([[x]] \mapsto [[sid]]) \in [[G]] }}
-    | n > 0 :: :: index_positive
-    | rval not found in se0 .. sen :: :: not_found_in_switch
-    | se0 = _ : sblock0 .. sen = _ : sblockn :: :: destruct_switch_elems
-    | fid -> x0 .. xn ; x'0 : sid0 .. x'm : sidm ; s0 .. sk :: :: function_resolution
-    %TODO: find a clean way of replacing -> by a \mapsto
-    | S = S' :: :: store_equality
-    | G = G' :: :: env_equality
-
-subrules
-    rval <:: v
-    lval <:: v
-    v <:: e
-
-defns
-reduction :: '' ::=
-defn
-s1 => s2 :: :: reduce_basic_stmt :: '' {{ tex [[s1]] \Rightarrow [[s2]]}} by
-
-    ------------------------------- :: if_then_desugar
-    if ( e ) s => if ( e ) s else ;
-
-    -------------------------- :: if_true
-    if ( True ) s else s' => s
-
-    ---------------------------- :: if_false
-    if ( False ) s else s' => s'
-
-    ------------------------------ :: block_next_stmt
-    {G ; s0 .. sn} => {G s0 .. sn}
-
-    ----------------------------------- :: block_break
-    {G break; s0 .. sn} => break;
-
-    ----------------------------------------- :: block_fallthrough
-    {G fallthrough; s0 .. sn} => fallthrough;
-
-    ----------------------------------- :: block_continue
-    {G continue; s0 .. sn} => continue;
-
-    ----------------------------------- :: block_return
-    {G return rval; s0 .. sn} => return rval;
-
-    --------- :: block_empty
-    {G } => ;
-
-    ---------- :: effectful_expr_value
-    rval; => ;
-
-    --------------------- :: loop_break
-    Loop(break ;, s) => ;
-
-    ------------------------ :: loop_continue
-    Loop(continue ;, s) => s
-
-    ------------------------------------- :: loop_fallthrough
-    Loop(fallthrough;, s) => fallthrough;
-
-    ------------------------------- :: loop_return
-    Loop(return e;, s) => return e;
-
-    --------------- :: loop_iteration_finished
-    Loop(;, s) => s
-
-    ----------------------------------------------- :: cases_break
-    Cases(break; s0 .. sn, sblock0, .., sblockm) => ;
-
-    ------------------------------------------------------------ :: cases_continue
-    Cases(continue; s0 .. sn, sblock0, .., sblockm) => continue;
-
-    ----------------------------------------------------------------------------- :: cases_fallthrough
-    Cases(fallthrough; s0 .. sn, sblock0, .., sblockm) => Cases(sblock0, .., sblockm)
-
-    ---------------------------------------------------------- :: cases_return
-    Cases(return e; s0 .. sn, sblock0, .., sblockm) => return e;
-
-    ----------------------------------------------------------------------------- :: cases_next_stmt
-    Cases( ; s0 .. sn, sblock0, .., sblockm) => Cases(s0 .. sn, sblock0, .., sblockm)
-
-    ------------ :: cases_empty
-    Cases() => ;
-
-    ------------------------------------------ :: while_loop
-    while (e) s => if (e) Loop(s, while (e) s)
-    % Note: this relies on the absence of variable declarations outside of blocks
-    % if this is not guaranteed by the validation phase, replace the production by if(e) Loop({s}, while (e) s)
-
-    ------------------------------------- :: do_while_loop
-    do s while(e); => Loop(s, while(e) s)
-    % Note: this relies on the absence of variable declarations outside of blocks
-    % if this is not guaranteed by the validation phase, replace the production by Loop({s}, while (e) s)
-
-    --------------------------------------------------------------- :: for_expr_loop
-    for (epre; econd; eincr) s => { epre; while(econd) {s eincr;} }
-    % Note: this relies on the absence of variable declarations outside of blocks
-    % if this is not guaranteed by the validation phase, replace {s eincr} by {{s} eincr}
-
-    --------------------------------------------------------------- :: for_decls_loop
-    for (vdecls; econd; eincr) s => { vdecls; while(econd) {s eincr;} }
-    % Note: this relies on the absence of variable declarations outside of blocks
-    % if this is not guaranteed by the validation phase, replace {s eincr} by {{s} eincr}
-
-    rval = rval'
-    se'0 = _ : sblock'0 .. se'm = _ : sblock'm
-    -------------------------------------------------------------------------------------------------- :: switch_case_found
-    switch (rval) {se0 .. sen case rval' : sblock se'0 .. se'm} => {Cases(sblock, sblock'0, .., sblock'm)}
-
-    rval not found in se0 .. sen
-    rval not found in se'0 .. se'm
-    se'0 = _ : sblock'0 .. se'm = _ : sblock'm
-    -------------------------------------------------------------------------------------------------- :: switch_case_not_found
-    switch (rval) {se0 .. sen default : sblock se'0 .. se'm} => {Cases(sblock, sblock'0, .., sblock'm)}
-
-    n > 0
-    ------------------------------------------------------------------------------------------ :: vdecls_multi
-    {G t vdecl0, vdecl1, .., vdecln; s0 .. sm} => {G t vdecl0; t vdecl1, .., vdecln; s0 .. sm}
-
-    ------------------------------------------------------------- :: vdecl_initializer
-    {G t x : sid = e; s0 .. sn} => {G t x : sid; x = e; s0 .. sn}
-
-defn
-s1 , G1 , S1 => s2 , G2 , S2 :: :: reduce_stmt :: '' {{ tex [[s1]], [[G1]], [[S1]] \Rightarrow [[s2]], [[G2]], [[S2]] }} by
-   
-    s => s'
-    -------------------- :: reduce_stmt_basic
-    s, G, S => s', G, S
-
-    ---------------------------------------------- :: annotate_block
-    {s0 .. sn}, G, S => {G s0 .. sn}, G, S
-
-    G |- e, S -> e', S'
-    ---------------------- :: effectful_expr_reduce
-    e;, G, S => e';, G, S'
-
-    G |- e, S -> e', S'
-    -------------------------------------------------- :: if_reduce
-    if (e) s else s', G, S => if (e') s else s', G, S'
-
-    G |- e, S -> e', S'
-    ------------------------------------------------------------------------------------------------ :: switch_reduce
-    switch (e) {se0 .. sen}, G, S => switch (e') {se0 .. sen}, G, S'
-
-    s, G, S => s', G', S'
-    -------------------------------------------------------- :: block_reduce
-    {G s s0 .. sn}, Gout, S => {G' s' s0 .. sn}, Gout, S'
-
-    s, G, S => s', G', S'
-    ---------------------------------------- :: loop_reduce
-    Loop(s, s2), G, S => Loop(s', s2), G', S'
-    % Note: if G and G' are not equal, something very wrong is going on.
-    % s should always be either a block (so no change to the environment), or a statement that is not a variable declaration (same)
-
-    s0, G, S => s0', G', S'
-    ----------------------------------------------------------------------------------------------- :: cases_reduce_first_stmt
-    Cases(s0 s1 .. sn, sblock0, .., sblockm), G, S => Cases(s0' s1 .. sn, sblock0, .., sblockm), G', S'
-
-    G |- e, S -> e', S'
-    ---------------------------------- :: return_reduce
-    return e;, G, S => return e';, G, S'
-
-    rval = Default(t)
-    ----------------------------------------------- :: vdecl_uninitialized
-    t x : sid;, G, S => ;, G[x -> sid], S[sid -> rval]
-
-defn
-e1 -> e2 :: :: reduce_basic_expr :: '' {{ tex [[e1]] \rightarrow [[e2]] }} by
-    
-    -------------- :: boolean_and_true
-    True && e -> e
-
-    ------------------- :: boolean_and_false
-    False && e -> False
-
-    --------------- :: boolean_or_false
-    False || e -> e
-
-    ----------------- :: boolean_or_true
-    True || e -> True
-
-    -------------------- :: ternary_true
-    True ? e1 : e2 -> e1
-
-    -------------------- :: ternary_false
-    False ? e1 : e2 -> e2
-
-    ------------------ :: comma_last_expr
-    Comma (e) -> e
-
-    -------------------------------------------------- :: comma_first_rval
-    Comma(rval, e, e0, .., en) -> Comma(e, e0, .., en)
-
-    ------------------------ :: call_construct_return
-    Call return rval; -> rval
-
-    --------------- :: call_construct_void
-    Call ; -> Void
-
-defn
-G |- e1 , S1 -> e2 , S2 :: :: reduce_expr :: '' {{ tex [[G]] \vdash [[e1]], [[S1]] \rightarrow [[e2]], [[S2]] }} by
-    e1 -> e2
-    ------------------- :: reduce_expr_basic
-    G |- e1, S -> e2, S
-
-    G |- e1, S -> e1', S'
-    ------------------------------------- :: boolean_and_reduce
-    G |- e1 && e2, S -> e1' && e2, S'
-    
-    G |- e1, S -> e1', S'
-    ------------------------------------- :: boolean_or_reduce
-    G |- e1 || e2, S -> e1' || e2, S'
-
-    G |- e, S -> e', S'
-    --------------------------------------- :: ternary_reduce
-    G |- e ? e1 : e2, S -> e' ? e1 : e2, S'
-
-    G |- e, S -> e', S'
-    ----------------------------------------------------------------- :: comma_reduce
-    G |- Comma(e, e0, e1, .., en), S -> Comma(e', e0, e1, .., en), S'
-
-    G |- e, S -> e', S'
-    ----------------------------------------------------------------------------------------------------------------- :: call_reduce
-    G |- fid<</rv // i/>>(</rval // j/>, e, </e // k/>), S -> fid<</rv // i/>>(</rval // j/>, e', </e // k/>), S'
-
-    fid -> </x//i/> ; </y : sid//j/> ; </s//k/>
-    G = Gglobal [</x -> rv//i/>, </y -> sid//j/>]
-    S' = S [</sid -> rval//j/>]
-    ----------------------------------------------------------------------- :: call_resolve
-    Gout |- fid<</rv//i/>>(</rval//j/>), S -> Call { G </s//k/> }, S'
-
-    s, G, S => s', G, S'
-    ----------------------------- :: call_construct_reduce
-    G |- Call s, S -> Call s', S'
-    % Note: the requirement that G remains the same is not that onerous or weird, since we only construct a Call with an annotated block inside it.
-
-    isNotLVal(e1)
-    G |- e1, S -> e1', S' 
-    ------------------------------- :: assign_reduce_left
-    G |- e1 = e2, S -> e1' = e2, S'
-
-    G |- e2, S -> e2', S'
-    ---------------------------------- :: assign_reduce_right
-    G |- lval = e2, S -> lval = e2', S
-
-    sid -> rv in S
-    rv[</offset // i/> := rval] = rv'
-    ------------------------------------------ :: assign_execute
-    G |- sid </offset // i/> = rval, S -> Void, S[sid -> rv']
-
-    x -> sid in G
-    ------------------- :: environment_access
-    G |- x, S -> sid, S
-
-    sid -> rval in S
-    ---------------------- :: store_access
-    G |- sid, S -> rval, S
-
-defn
-rv0 [ offset0 .. offsetn := rv1 ] = rv2 :: :: value_update :: '' by
-
-    ------------------- :: no_path
-    rv0[ := rv1] = rv1
-
-    rv[offset0 .. offsetk := rval] = rv'
-    ----------------------------------------------------------------------------------------------------------------------------------------------- :: struct
-    {</xi : rvi // i /> ; x : rv ; </ x'j : rv'j // j />}[ .x offset0 .. offsetk := rval] = {</ xi : rvi // i /> ; x : rv' ; </ x'j : rv'j // j />} 
-    
-    rv[offset0 .. offsetk := rval] = rv'
-    ------------------------------------------------------------------------------------------------------------------------------- :: array
-    [</rv//i IN 0..n-1/>, rv, </rv'//j IN 0..m/>][ [n] offset0 .. offsetk := rval] = [</rv//i IN 0..n-1/>, rv', </rv'//j IN 0..m/>]