Added: trunk/Tools/WebGPUShadingLanguageRI/SpecWork/WSL_exec.ott (0 => 232955)
--- trunk/Tools/WebGPUShadingLanguageRI/SpecWork/WSL_exec.ott (rev 0)
+++ trunk/Tools/WebGPUShadingLanguageRI/SpecWork/WSL_exec.ott 2018-06-19 07:14:49 UTC (rev 232955)
@@ -0,0 +1,376 @@
+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/>]
Added: trunk/Tools/WebGPUShadingLanguageRI/SpecWork/WSL_type.ott (0 => 232955)
--- trunk/Tools/WebGPUShadingLanguageRI/SpecWork/WSL_type.ott (rev 0)
+++ trunk/Tools/WebGPUShadingLanguageRI/SpecWork/WSL_type.ott 2018-06-19 07:14:49 UTC (rev 232955)
@@ -0,0 +1,298 @@
+metavar x, y ::=
+indexvar i, j, k, n, m ::=
+
+grammar
+s :: stmt_ ::= {{com statement}}
+ | if ( e ) s else s' :: :: if
+ | do s while ( e ) ; :: :: do_while
+ | switch ( e ) { sc0 : sblock0 .. scn : sblockn } :: :: switch
+ | break ; :: :: break
+ | continue ; :: :: continue
+ | fallthrough ; :: :: fallthrough
+ | return e ; :: :: return
+ | return ; :: :: return_void
+ | trap ; :: :: trap
+ | { s0 .. sn } :: :: block
+ | t x ; :: :: variable_decl
+ % 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
+ | e ; :: :: effectful_expr
+
+sc :: switch_case_ ::=
+ | case e :: :: case
+ | default :: :: default
+
+sblock :: switch_block_ ::=
+ | s0 .. sn :: :: statements
+
+fs :: full_statement_ ::= {{com full statement (pre-desugaring)}}
+ | if ( e ) fs :: :: if_then
+ | if ( e ) fs else fs' :: :: if_then_else
+ | do fs while ( e ) ; :: :: do_while
+ | for ( e ; e' ; e'' ) fs :: :: for_three_expr
+ | while ( e ) fs :: :: while
+ | switch ( e ) { sc0 : fsblock0 .. scn : fsblockn } :: :: switch
+ | break ; :: :: break
+ | continue ; :: :: continue
+ | fallthrough ; :: :: fallthrough
+ | return e ; :: :: return
+ | return ; :: :: return_void
+ | trap ; :: :: trap
+ | { fs0 .. fsn } :: :: block
+ | ; :: :: empty_stmt
+ | t vdecl0 , .. , vdecln ; :: :: vdecls
+ % 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
+ | e ; :: :: effectful_expr
+
+fsblock :: full_switch_block_ ::=
+ | fs0 .. fsn :: :: statements
+
+vdecl :: variable_declaration_ ::=
+ | x :: :: uninitialized
+ | x = e :: :: initialized
+
+e :: expr_ ::= {{com _expression_}}
+ | true :: :: lit_true
+ | false :: :: lit_false
+ | e || e' :: :: or
+ | e && e' :: :: and
+ | e = e' :: :: assignment
+ | x :: :: variable_name
+ | * e :: :: ptr_deref
+ | & e :: :: address_taking
+ | @ e :: :: array_reference_making
+ | e [ e' ] :: :: array_index
+
+G {{tex \Gamma}} :: env_ ::= {{com typing environment}}
+ | G [ x : t ] :: :: update_with_var {{com update the environment with "x is of type t"}}
+ | G [ x = t ] :: :: update_with_typedef {{com update the environment with "x is a typedef of type t"}}
+
+B :: behaviour_ ::= {{com statement behaviour}}
+ | { b0 , .. , bn } :: :: set
+ | B + B' :: :: union {{tex [[B]] \cup [[B']]}}
+ | B \ B' :: :: difference {{tex [[B]] \backslash [[B']]}}
+ | U B0 .. Bn :: :: big_union
+ | ( B ) :: :: parens {{tex [[B]]}} {{com artificial, teaches ott the precedence of previous rules}}
+
+b :: single_behaviour_ ::=
+ | Return t :: :: return
+ | Break :: :: break
+ | Continue :: :: continue
+ | Fallthrough :: :: fallthrough
+ | Nothing :: :: Nothing
+
+t {{tex \tau}} :: type_ ::= {{com type}}
+ | LVal ( t ) :: :: lval {{com left value}}
+ | Ptr ( t ) :: :: ptr {{com pointer}}
+ | Ref ( t ) :: :: array_ref {{com array reference}}
+ | [ t ] :: :: array {{com array}}
+ | bool :: :: bool
+ | uint32 :: :: uint32 % TODO: fix typesetting
+ | void :: :: void
+ % TODO: should I make it explicit that nested LVal are forbidden in a valid type?
+
+terminals :: terminals_ ::=
+ | U :: :: big_union {{tex \bigcup}}
+ | |- :: :: vdash {{tex \vdash}}
+ | --> :: :: desugars {{tex \leadsto}}
+
+formula :: formula_ ::=
+ | judgement :: :: judgement
+ | formula0 .. formulan :: :: several_formula
+ | n > 0 :: :: int_positive
+ | n > 1 :: :: int_greater_than_one
+ | x : t in G :: :: env_mapping_exists {{tex [[x]] : [[t]] \in [[G]]}}
+ | G |- isInteger ( t ) :: :: is_integer
+ | s != s' :: :: stmt_not_eq {{tex [[s]] \neq [[s']]}}
+ | b in B :: :: behaviour_in {{tex [[b]] \in [[B]]}}
+ | b not in B :: :: behaviour_not_in {{tex [[b]] \not\in [[B]]}}
+ | B = B' :: :: behaviour_eq
+
+defns
+desugaring :: '' ::=
+defn
+fs --> fs' :: :: desugaring :: '' {{com Desugaring statements}} by
+% TODO: decide whether I even want to make the desugaring so formal.
+
+ ----------------------------- :: if_then
+ if (e) fs --> if (e) fs else {}
+
+ -------- :: empty_stmt
+ ; --> {}
+
+ -------------------------------------- :: while
+ while (e) fs --> if (e) do fs while (e);
+
+ ------------------------------------------------- :: for_three_exprs
+ for (e ; e' ; e'') fs --> {e; while(e') {fs e'';}}
+ % TODO: cover all variations of for loops: if the condition is empty, if the increment is empty, if the initialization is empty,
+ % if two of the three are empty, if all three are empty, if the initialization is a vdecl and not an _expression_,
+ % etc..
+
+ k > 1
+ -------------------------------------------------------------------------------------- :: multiple_vdecls
+ { fs0..fsn t vdecl0, vdecl1, .., vdeclk; fs'0..fs'm} --> {fs0..fsn t vdecl0; t vdecl1, .., vdeclk; fs'0..fs'm}
+
+ ------------------------------------------------------------- :: initialized_vdecl
+ { fs0..fsn t x = e; fs'0..fs'm} --> {fs0..fsn t x; x = e; fs'0..fs'm}
+
+% TODO: desugar expressions, namely replace e != e' by ! (e == e'); and replace foo(e0,..,en) by foo<>(e0,..,en)
+
+defns
+typing :: '' ::=
+defn
+G |- s : B :: :: typing_statement :: '' by
+
+ G |- e : bool
+ G |- s : B
+ G |- s' : B'
+ ------------------------------ :: if
+ G |- if (e) s else s' : B + B'
+
+ G |- e : bool
+ G |- s : B
+ ---------------------------------------------------------- :: do_while
+ G |- do s while (e); : (B \ {Break, Continue}) + {Nothing}
+ % 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.
+
+ G |- e : t
+ G |- isInteger(t)
+ G |- sc0: t .. G |- scn: t
+ 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}
+
+ --------------------- :: break
+ G |- break; : {Break}
+
+ --------------------------- :: continue
+ G |- continue; : {Continue}
+
+ --------------------------------- :: fallthrough
+ G |- fallthrough; : {Fallthrough}
+
+ G |- e : t
+ --------------------------- :: return
+ G |- return e; : {Return t}
+
+ ----------------------------- :: return_void
+ G |- return ; : {Return void}
+
+ ----------------------- :: trap
+ G |- trap; : {Return t}
+
+ ------------------- :: empty_block
+ G |- {} : {Nothing}
+
+ G[x : LVal(t)] |- {s0 .. sn} : B
+ s0 != t' x; .. sn != t' x;
+ --------------------------------- :: variable_decl
+ G |- {t x; s0 .. sn} : B
+ % 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
+ % if they are applied where s is a variable declaration.
+ % Note: the second premise prevents redeclaration of a variable in the same scope it was declared in.
+ % Implemented naively it takes O(n**2) to check, but can trivially be optimized.
+
+ G |- s : B
+ ------------ :: trivial_block
+ G |- {s} : B
+
+ G |- s : B
+ G |- {s0 .. sn} : B'
+ n > 0
+ Nothing in B
+ -------------------------------------- :: block
+ G |- {s s0 .. sn} : (B \ {Nothing}) + B'
+ % Note: the last premise forbids trivially dead code. It is optional and could be removed with no consequences on the rest of the language.
+
+ G |- e : t
+ ------------------- :: expr
+ G |- e; : {Nothing}
+
+defn
+G |- sc : t :: :: typing_switch_case :: '' by
+
+ G |- e : t
+ --------------- :: case
+ G |- case e : t
+
+ ---------------- :: default
+ G |- default : t
+
+defn
+G |- sblock : B :: :: typing_switch_block :: '' by
+
+ G |- { s0 .. sn } : B
+ --------------------- :: switch_block
+ G |- s0 .. sn : B
+
+defn
+G |- e : t :: :: typing_rval :: '' by
+
+ ---------------- :: literal_true
+ G |- true : bool
+
+ ----------------- :: literal_false
+ G |- false : bool
+
+ G |- e : bool
+ G |- e' : bool
+ ------------------- :: or
+ G |- e || e' : bool
+
+ G |- e : bool
+ G |- e' : bool
+ ------------------- :: and
+ G |- e && e' : bool
+
+ G |- e : LVal(t)
+ G |- e' : t
+ ----------------- :: assignment
+ G |- e = e' : t
+
+ x : t in G
+ ----------- :: variable_name
+ G |- x : t
+
+ G |- e : LVal(t)
+ ---------------- :: lval_access
+ G |- e : t
+
+ G |- e : LVal(t)
+ ---------------- :: address_taking
+ G |- &e : Ptr(t)
+ % can the unary operator & be overloaded?
+ % It seems that no
+
+ G |- e : Ptr(t)
+ ----------------- :: ptr_deref
+ G |- *e : LVal(t)
+ % can the unary operator * be overloaded?
+ % It seems that no
+
+ % Note: We currently do not have any special interaction between pointers and array references in these rules
+
+ G |- e : LVal(t)
+ ---------------- :: take_ref_lval
+ G |- @e : Ref(t)
+ % 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.
+
+ G |- e : LVal([t])
+ G |- e' : uint32
+ -------------------- :: array_index_lval
+ G |- e[e'] : LVal(t)
+
+ G |- e : [t]
+ G |- e' : uint32
+ ---------------- :: array_index_rval
+ G |- e[e'] : t
+ % There is a choice between applying array_index_lval and then lval_access, or lval_access and then array_index_rval.
+ % It is not problematic, because the rules are confluent, so either choice leads to the same result.
+ % TODO: should we refuse during validation the case where e' is a constant that falls out of the bounds of e ?
+ % I think it should be an allowed behaviour but not required of the implementation.
+
+ G |- e : Ref(t)
+ G |- e' : uint32
+ -------------------- :: array_ref_index
+ G |- e[e'] : LVal(t)
Added: trunk/Tools/WebGPUShadingLanguageRI/SpecWork/source/conf.py (0 => 232955)
--- trunk/Tools/WebGPUShadingLanguageRI/SpecWork/source/conf.py (rev 0)
+++ trunk/Tools/WebGPUShadingLanguageRI/SpecWork/source/conf.py 2018-06-19 07:14:49 UTC (rev 232955)
@@ -0,0 +1,166 @@
+# -*- coding: utf-8 -*-
+#
+# Configuration file for the Sphinx documentation builder.
+#
+# This file does only contain a selection of the most common options. For a
+# full list see the documentation:
+# http://www.sphinx-doc.org/en/master/config
+
+# -- Path setup --------------------------------------------------------------
+
+# If extensions (or modules to document with autodoc) are in another directory,
+# add these directories to sys.path here. If the directory is relative to the
+# documentation root, use os.path.abspath to make it absolute, like shown here.
+#
+# import os
+# import sys
+# sys.path.insert(0, os.path.abspath('.'))
+
+
+# -- Project information -----------------------------------------------------
+
+project = u'WSL'
+copyright = u'2018, Robin Morisset, Filip Pizlo, Myles C. Maxfield'
+author = u'Robin Morisset, Filip Pizlo, Myles C. Maxfield'
+
+# The short X.Y version
+version = u''
+# The full version, including alpha/beta/rc tags
+release = u''
+
+
+# -- General configuration ---------------------------------------------------
+
+# If your documentation needs a minimal Sphinx version, state it here.
+#
+# needs_sphinx = '1.0'
+
+# Add any Sphinx extension module names here, as strings. They can be
+# extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
+# ones.
+extensions = [
+ 'sphinx.ext.todo',
+ 'sphinx.ext.mathjax',
+ 'sphinx.ext.ifconfig',
+]
+
+# Add any paths that contain templates here, relative to this directory.
+templates_path = ['_templates']
+
+# The suffix(es) of source filenames.
+# You can specify multiple suffix as a list of string:
+#
+# source_suffix = ['.rst', '.md']
+source_suffix = '.rst'
+
+# The master toctree document.
+master_doc = 'index'
+
+# The language for content autogenerated by Sphinx. Refer to documentation
+# for a list of supported languages.
+#
+# This is also used if you do content translation via gettext catalogs.
+# Usually you set "language" from the command line for these cases.
+language = None
+
+# List of patterns, relative to source directory, that match files and
+# directories to ignore when looking for source files.
+# This pattern also affects html_static_path and html_extra_path .
+exclude_patterns = []
+
+# The name of the Pygments (syntax highlighting) style to use.
+pygments_style = 'sphinx'
+
+
+# -- Options for HTML output -------------------------------------------------
+
+# The theme to use for HTML and HTML Help pages. See the documentation for
+# a list of builtin themes.
+#
+html_theme = 'alabaster'
+
+# Theme options are theme-specific and customize the look and feel of a theme
+# further. For a list of options available for each theme, see the
+# documentation.
+#
+# html_theme_options = {}
+
+# Add any paths that contain custom static files (such as style sheets) here,
+# relative to this directory. They are copied after the builtin static files,
+# so a file named "default.css" will overwrite the builtin "default.css".
+html_static_path = ['_static']
+
+# Custom sidebar templates, must be a dictionary that maps document names
+# to template names.
+#
+# The default sidebars (for documents that don't match any pattern) are
+# defined by theme itself. Builtin themes are using these templates by
+# default: ``['localtoc.html', 'relations.html', 'sourcelink.html',
+# 'searchbox.html']``.
+#
+# html_sidebars = {}
+
+
+# -- Options for HTMLHelp output ---------------------------------------------
+
+# Output file base name for HTML help builder.
+htmlhelp_basename = 'WSLdoc'
+
+
+# -- Options for LaTeX output ------------------------------------------------
+
+latex_elements = {
+ # The paper size ('letterpaper' or 'a4paper').
+ #
+ # 'papersize': 'letterpaper',
+
+ # The font size ('10pt', '11pt' or '12pt').
+ #
+ # 'pointsize': '10pt',
+
+ # Additional stuff for the LaTeX preamble.
+ #
+ # 'preamble': '',
+
+ # Latex figure (float) alignment
+ #
+ # 'figure_align': 'htbp',
+}
+
+# Grouping the document tree into LaTeX files. List of tuples
+# (source start file, target name, title,
+# author, documentclass [howto, manual, or own class]).
+latex_documents = [
+ (master_doc, 'WSL.tex', u'WSL Documentation',
+ u'Robin Morisset, Filip Pizlo, Myles C. Maxfield', 'manual'),
+]
+
+
+# -- Options for manual page output ------------------------------------------
+
+# One entry per manual page. List of tuples
+# (source start file, name, description, authors, manual section).
+man_pages = [
+ (master_doc, 'wsl', u'WSL Documentation',
+ [author], 1)
+]
+
+
+# -- Options for Texinfo output ----------------------------------------------
+
+# Grouping the document tree into Texinfo files. List of tuples
+# (source start file, target name, title, author,
+# dir menu entry, description, category)
+texinfo_documents = [
+ (master_doc, 'WSL', u'WSL Documentation',
+ author, 'WSL', 'One line description of project.',
+ 'Miscellaneous'),
+]
+
+
+# -- Extension configuration -------------------------------------------------
+
+# -- Options for todo extension ----------------------------------------------
+
+# If true, `todo` and `todoList` produce output, else they produce nothing.
+todo_include_todos = True
\ No newline at end of file
