Move WHLSL spec work to the W3C GPUWeb GitHub repository
authormmaxfield@apple.com <mmaxfield@apple.com@268f45cc-cd09-0410-ab3c-d52691b4dbfc>
Thu, 12 Jul 2018 01:35:16 +0000 (01:35 +0000)
committermmaxfield@apple.com <mmaxfield@apple.com@268f45cc-cd09-0410-ab3c-d52691b4dbfc>
Thu, 12 Jul 2018 01:35:16 +0000 (01:35 +0000)
See https://github.com/gpuweb/WHLSL

* WebGPUShadingLanguageRI/SpecWork/Makefile: Removed.
* WebGPUShadingLanguageRI/SpecWork/WSL.g4: Removed.
* WebGPUShadingLanguageRI/SpecWork/WSL.ott: Removed.
* WebGPUShadingLanguageRI/SpecWork/source/conf.py: Removed.
* WebGPUShadingLanguageRI/SpecWork/source/index.rst: Removed.

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

Tools/ChangeLog
Tools/WebGPUShadingLanguageRI/SpecWork/Makefile [deleted file]
Tools/WebGPUShadingLanguageRI/SpecWork/WSL.g4 [deleted file]
Tools/WebGPUShadingLanguageRI/SpecWork/WSL.ott [deleted file]
Tools/WebGPUShadingLanguageRI/SpecWork/source/conf.py [deleted file]
Tools/WebGPUShadingLanguageRI/SpecWork/source/index.rst [deleted file]

index 3ddf852..9cf1838 100644 (file)
@@ -1,3 +1,15 @@
+2018-07-11  Myles C. Maxfield  <mmaxfield@apple.com>
+
+        Move WHLSL spec work to the W3C GPUWeb GitHub repository
+
+        See https://github.com/gpuweb/WHLSL
+
+        * WebGPUShadingLanguageRI/SpecWork/Makefile: Removed.
+        * WebGPUShadingLanguageRI/SpecWork/WSL.g4: Removed.
+        * WebGPUShadingLanguageRI/SpecWork/WSL.ott: Removed.
+        * WebGPUShadingLanguageRI/SpecWork/source/conf.py: Removed.
+        * WebGPUShadingLanguageRI/SpecWork/source/index.rst: Removed.
+
 2018-07-11  Dean Jackson  <dino@apple.com>
 
         Force WKTR to use the light appearance
diff --git a/Tools/WebGPUShadingLanguageRI/SpecWork/Makefile b/Tools/WebGPUShadingLanguageRI/SpecWork/Makefile
deleted file mode 100644 (file)
index 0559365..0000000
+++ /dev/null
@@ -1,20 +0,0 @@
-# Minimal makefile for Sphinx documentation
-#
-
-# You can set these variables from the command line.
-SPHINXOPTS    =
-SPHINXBUILD   = sphinx-build
-SPHINXPROJ    = WSL
-SOURCEDIR     = source
-BUILDDIR      = build
-
-# Put it first so that "make" without argument is like "make help".
-help:
-       @$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
-
-.PHONY: help Makefile
-
-# Catch-all target: route all unknown targets to Sphinx using the new
-# "make mode" option.  $(O) is meant as a shortcut for $(SPHINXOPTS).
-%: Makefile
-       @$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
\ No newline at end of file
diff --git a/Tools/WebGPUShadingLanguageRI/SpecWork/WSL.g4 b/Tools/WebGPUShadingLanguageRI/SpecWork/WSL.g4
deleted file mode 100644 (file)
index 9506886..0000000
+++ /dev/null
@@ -1,239 +0,0 @@
-grammar WSL;
-
-/*
- * Lexer
- */
-Whitespace: [ \t\r\n]+ -> skip ;
-LineComment: '//'[^\r\n] -> skip ;
-LongComment: '/*'.*?'*/' -> skip ;
-
-// Note: we forbid leading 0s in decimal integers. to bikeshed.
-fragment CoreDecimalIntLiteral: [1-9] [0-9]* ;
-// Note: we allow a leading '-' but not a leading '+' in all kind of numeric literals. to bikeshed.
-fragment DecimalIntLiteral: '-'? CoreDecimalIntLiteral ;
-fragment DecimalUIntLiteral: CoreDecimalIntLiteral 'u' ;
-fragment CoreHexadecimalIntLiteral: '0x' [0-9a-fA-F]+ ;
-fragment HexadecimalIntLiteral: '-'? CoreHexadecimalIntLiteral;
-fragment HexadecimalUIntLiteral: CoreHexadecimalIntLiteral 'u';
-IntLiteral: DecimalIntLiteral | DecimalUIntLiteral | HexadecimalIntLiteral | HexadecimalUIntLiteral ;
-// Do we want to allow underscores in the middle of numbers for readability?
-
-fragment CoreFloatLiteral: [0-9]+'.'[0-9]* | [0-9]*'.'[0-9]+ ;
-FloatLiteral: '-'? CoreFloatLiteral [fd]? ;
-// TODO: what to do about floats that are too big or too small to represent?
-// TODO: what is the default precision? double?
-// IDEA: add Nan, +infinity, -infinity
-// IDEA: add half-precision literals
-
-// One rule per keyword, to prevent them from being recognized as identifiers
-STRUCT: 'struct';
-PROTOCOL: 'protocol';
-TYPEDEF: 'typedef';
-ENUM: 'enum';
-OPERATOR: 'operator';
-
-IF: 'if';
-ELSE: 'else';
-CONTINUE: 'continue';
-BREAK: 'break';
-SWITCH: 'switch';
-CASE: 'case';
-DEFAULT: 'default';
-FALLTHROUGH: 'fallthrough';
-FOR: 'for';
-WHILE: 'while';
-DO: 'do';
-RETURN: 'return';
-TRAP: 'trap';
-
-NULL: 'null';
-TRUE: 'true';
-FALSE: 'false';
-// Note: We could make these three fully case sensitive or insensitive. to bikeshed.
-
-CONSTANT: 'constant';
-DEVICE: 'device';
-THREADGROUP: 'threadgroup';
-THREAD: 'thread';
-
-VERTEX: 'vertex';
-FRAGMENT: 'fragment';
-
-NATIVE: 'native';
-RESTRICTED: 'restricted';
-// Note: these could be only keyword in the native mode, but I decided to make them always reserved. to bikeshed.
-
-UNDERSCORE: '_';
-AUTO: 'auto';
-// Note: these are currently not used by the grammar, but I would like to make them reserved keywords for future expansion of the language. to bikeshed
-
-fragment ValidIdentifier: [a-zA-Z_] [a-zA-Z0-9_]* ;
-Identifier: ValidIdentifier ;
-// Note: this currently excludes unicode, but allows digits in the middle of identifiers. We could easily restrict or extend this definition. to bikeshed
-
-OperatorName
-    : 'operator' ('>>' | '<<' | '+' | '-' | '*' | '/' | '%' | '&&' | '||' | '&' | '^' | '|' | '>=' | '<=' | '==' | '<' | '>' | '++' | '--' | '!' | '~' | '[]' | '[]=' | '&[]')
-    | 'operator&.' ValidIdentifier
-    | 'operator.' ValidIdentifier '='
-    | 'operator.' ValidIdentifier ;
-// Note: operator!= is not user-definable, it is automatically derived from operator==
-
-/*
- * Parser: Top-level
- */
-file: topLevelDecl* EOF ;
-topLevelDecl
-    : ';'
-    | variableDecls ';'
-    | typeDef
-    | structDef
-    | enumDef
-    | funcDef
-    | nativeFuncDecl
-    | nativeTypeDecl
-    | protocolDecl ;
-
-typeDef: TYPEDEF Identifier typeParameters '=' type ';' ;
-
-structDef: STRUCT Identifier typeParameters '{' structElement* '}' ;
-structElement: type Identifier ';' ;
-
-enumDef: ENUM Identifier (':' type)? '{' enumMember (',' enumMember)* '}' ;
-// Note: we could allow an extra ',' at the end of the list of enumMembers, ala Rust, to make it easier to reorder the members. to bikeshed
-enumMember: Identifier ('=' constexpr)? ;
-
-funcDef: RESTRICTED? funcDecl block;
-funcDecl
-    : (VERTEX | FRAGMENT) type Identifier parameters
-    | type (Identifier | OperatorName) typeParameters parameters
-    | OPERATOR typeParameters type parameters ;
-// Note: the return type is moved in a different place for operator casts, as a hint that it plays a role in overload resolution. to bikeshed
-parameters
-    : '(' ')'
-    | '(' parameter (',' parameter)* ')' ;
-parameter: type Identifier? ;
-
-nativeFuncDecl: RESTRICTED? NATIVE funcDecl ';' ;
-nativeTypeDecl: NATIVE TYPEDEF Identifier typeParameters ';' ;
-
-protocolDecl: PROTOCOL Identifier (':' protocolRef (',' protocolRef)*)? '{' (funcDecl ';')* '}' ;
-// Note: I forbid empty extensions lists in protocol declarations, while the original js parser allowed them. to bikeshed
-protocolRef: Identifier ;
-
-/*
- * Parser: Types 
- */
-typeParameters
-    : '<' typeParameter (',' typeParameter)* '>'
-    | ('<' '>')?;
-// Note: contrary to C++ for example, we allow '<>' and consider it equivalent to having no type parameters at all. to bikeshed
-typeParameter
-    : type Identifier
-    | Identifier (':' protocolRef ('+' protocolRef)*)? ;
-
-type
-    : addressSpace Identifier typeArguments typeSuffixAbbreviated+
-    | Identifier typeArguments typeSuffixNonAbbreviated* ;
-addressSpace: CONSTANT | DEVICE | THREADGROUP | THREAD ;
-typeSuffixAbbreviated: '*' | '[]' | '[' IntLiteral ']';
-typeSuffixNonAbbreviated: '*' addressSpace | '[]' addressSpace | '[' IntLiteral ']' ;
-// Note: in this formulation of typeSuffix*, we don't allow whitespace between the '[' and the ']' in '[]'. We easily could at the cost of a tiny more bit of lookahead. to bikeshed
-
-typeArguments
-    : '<' (typeArgument ',')* addressSpace? Identifier '<' (typeArgument (',' typeArgument)*)? '>>'
-    //Note: this first alternative is a horrible hack to deal with nested generics that end with '>>'. As far as I can tell it works fine, but requires arbitrary lookahead.
-    | '<' typeArgument (',' typeArgument)* '>'
-    | ('<' '>')? ;
-typeArgument: constexpr | type ;
-
-/* 
- * Parser: Statements 
- */
-block: '{' blockBody '}' ;
-blockBody: stmt* ;
-
-stmt
-    : block
-    | ifStmt
-    | switchStmt
-    | forStmt
-    | whileStmt
-    | doStmt ';'
-    | BREAK ';'
-    | CONTINUE ';'
-    | FALLTHROUGH ';'
-    | TRAP ';'
-    | RETURN expr? ';'
-    | variableDecls ';'
-    | effectfulExpr ';' ;
-
-ifStmt: IF '(' expr ')' stmt (ELSE stmt)? ;
-
-switchStmt: SWITCH '(' expr ')' '{' switchCase* '}' ;
-switchCase: (CASE constexpr | DEFAULT) ':' blockBody ;
-
-forStmt: FOR '(' (variableDecls | effectfulExpr) ';' expr? ';' expr? ')' stmt ;
-whileStmt: WHILE '(' expr ')' stmt ;
-doStmt: DO stmt WHILE '(' expr ')' ;
-
-variableDecls: type variableDecl (',' variableDecl)* ;
-variableDecl: Identifier ('=' expr)? ;
-
-/* 
- * Parser: Expressions
- */
-constexpr
-    : literal 
-    | Identifier // to get the (constexpr) value of a type variable
-    | Identifier '.' Identifier; // to get a value out of an enum
-
-// Note: we separate effectful expressions from normal expressions, and only allow the former in statement positions, to disambiguate the following:
-// "x * y;". Without this trick, it would look like both an expression and a variable declaration, and could not be disambiguated until name resolution.
-effectfulExpr: ((effAssignment ',')* effAssignment)? ; 
-effAssignment
-    : possiblePrefix assignOperator possibleTernaryConditional
-    | effPrefix ;
-assignOperator: '=' | '+=' | '-=' | '*=' | '/=' | '%=' | '^=' | '&=' | '|=' | '>>=' | '<<=' ;
-effPrefix
-    : ('++' | '--') possiblePrefix
-    | effSuffix ;
-effSuffix
-    : possibleSuffix ('++' | '--')
-    | callExpression
-    | '(' expr ')' ;
-// Note: this last case is to allow craziness like "(x < y ? z += 42 : w += 13);" 
-// TODO: Not sure at all how useful it is, I also still have to double check that it introduces no ambiguity.
-limitedSuffixOperator
-    : '.' Identifier 
-    | '->' Identifier 
-    | '[' expr ']' ;
-
-expr: (possibleTernaryConditional ',')* possibleTernaryConditional;
-// TODO: I tried to mimic https://en.cppreference.com/w/cpp/language/operator_precedence with regards to assignment and ternary conditionals, but it still needs some testing
-possibleTernaryConditional
-    : possibleLogicalBinop '?' expr ':' possibleTernaryConditional
-    | possiblePrefix assignOperator possibleTernaryConditional
-    | possibleLogicalBinop ;
-possibleLogicalBinop: possibleRelationalBinop (logicalBinop possibleRelationallBinop)*;
-logicalBinop: '||' | '&&' | '|' | '^' | '&' ;
-// Note: the list above may need some manipulation to get the proper left-to-right associativity
-possibleRelationalBinop: possibleShift (relationalBinop possibleShift)?;
-relationalBinop: '<' | '>' | '<=' | '>=' | '==' | '!=' ; 
-// Note: we made relational binops non-associative to better disambiguate "x<y>(z)" into a call expression and not a comparison of comparison
-// Idea: https://en.cppreference.com/w/cpp/language/operator_comparison#Three-way_comparison
-possibleShift: possibleAdd (('>>' | '<<') possibleAdd)* ;
-possibleAdd: possibleMult (('+' | '-') possibleMult)* ;
-possibleMult: possiblePrefix (('*' | '/' | '%') possiblePrefix)* ;
-possiblePrefix: prefixOp* possibleSuffix ;
-prefixOp: '++' | '--' | '+' | '-' | '~' | '!' | '&' | '@' | '*' ;
-possibleSuffix
-    : callExpression limitedSuffixOperator*
-    | term (limitedSuffixOperator | '++' | '--')* ;
-callExpression: Identifier typeArguments '(' (possibleTernaryConditional (',' possibleTernaryConditional)*)? ')';
-term
-    : literal
-    | Identifier
-    | '(' expr ')' ;
-
-literal: IntLiteral | FloatLiteral | NULL | TRUE | FALSE;
-
diff --git a/Tools/WebGPUShadingLanguageRI/SpecWork/WSL.ott b/Tools/WebGPUShadingLanguageRI/SpecWork/WSL.ott
deleted file mode 100644 (file)
index c1fe489..0000000
+++ /dev/null
@@ -1,837 +0,0 @@
-metavar x, y, z, f ::=
-indexvar i, j, k, n, m ::=
-
-grammar
-td :: top_level_decl_ ::= {{com top-level declaration}}
-    | tx f <( tparam0 , .. , tparamk )> ( tx0 x0 , .. , txm xm ) { s0 .. sn } :: :: func_decl
-    | typedef x <( tparam0 , .. , tparamk )> = tx ; :: :: typedef
-
-tparam :: type_parameter_ ::= {{com type parameter}}
-    | tx x :: :: constexpr
-    | x : y0 + .. + yn :: :: type_variable
-
-s :: stmt_ ::= {{com statement}}
-    | if ( e ) s :: :: if_then {{com Desugared}}
-    | while ( e ) s :: :: while {{com Desugared}}
-    | for ( eOrVDecls ; eOrNothing ; eOrNothing' ) s :: :: for {{com Desugared}}
-    | tx vdecl0 , .. , vdecln ; :: :: multi_vdecls {{com partly desugared}}
-    | ; :: :: empty {{com Desugared}}
-    | 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
-    | { blockAnnot s0 .. sn } :: :: block
-    | e ; :: :: effectful_expr
-    | tval x : sid ; :: :: resolved_vdecl {{com post-monomorphisation variable declaration}}
-    | tval x : sid = e ; :: :: resolved_init_vdecl {{com post-monomorphisation}}
-    | Loop ( s , s' ) :: :: loop_construct {{com Special, only during execution}}
-    | Cases ( s0 , .. , sn ) :: :: cases_construct {{com Special, only during execution}}
-    | Join ( s ) :: :: join_construct {{com Special, only during execution}}
-
-sc :: switch_case_ ::=
-    | case rval :: :: case
-    | default :: :: default
-
-sblock :: switch_block_ ::=
-    | s0 .. sn :: :: statements
-
-vdecl :: variable_declaration_ ::=
-    | x :: :: uninitialized
-    | x = e :: :: initialized
-
-eOrVDecls :: expr_or_vdecl_ ::=
-    | e :: :: expr
-    | tx vdecl0 , .. , vdecln :: :: vdecl
-    | :: :: nothing
-
-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
-    | e || e' :: :: or {{tex [[e]]\:{||}\:[[e']]}}
-    | e && e' :: :: and {{tex [[e]]\:{\&\&}\:[[e']]}}
-    | e0 ? e1 : e2 :: :: ternary {{tex [[e0]]\:{?}\:[[e1]]:[[e2]]}}
-    | ! e :: :: not {{tex \:![[e]]}}
-    | e == e' :: :: equals_operator
-    | e != e' :: :: not_equals_operator {{com Desugared}} {{tex [[e]]\;!\mkern-\thickmuskip=[[e']]}}
-    | e = e' :: :: assignment
-    | x :: :: variable_name
-    | * e :: :: ptr_deref
-    | & e :: :: address_taking
-    | @ e :: :: array_reference_making
-    | e [ e' stride ] :: :: array_index {{tex [[e]] [ [[e']] ]_{[[stride]]} }}
-    | x <( targ0 , .. , targm )> ( e0 , .. , en ) :: :: call
-    | 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}}
-    | JoinExpr ( e ) :: :: join_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}}
-    | tx :: :: type {{com a type that is not just an identifier}}
-    | x . y :: :: enum_value {{com a field of an enum, for a constexpr type parameter}}
-
-G {{tex \Gamma}} , Gglobal {{tex \Gamma_{global} }} :: env_ ::= {{com typing environment}}
-    | G [ x -> envMapping ] :: :: update {{com $\Gamma$ with the mapping for x replaced by envMapping}}
-    | { x0 -> envMapping0 , .. , xn -> envMappingn } :: :: set
-
-envMapping :: env_mapping_ ::= 
-    | t :: :: var {{com $x$ is of type $\tau$}}
-    | SyntaxTypedef ( <( tparam0 , .. , tparamn )> -> tx ) :: :: typedef_syntax {{com resolved before local typing}}
-    | Typedef ( <( tparam0 , .. , tparamn )> -> tval ) :: :: typedef
-    | Func { sig0 , .. , sign } :: :: func {{com $x$ is a function whose signatures are $sig0$ to $sign$}}
-    | SyntaxFunc { sigx0 , .. , sigxn } :: :: func_syntax
-    | Nothing :: :: nothing {{tex \emptyset}} {{com to remove $x$ from $\Gamma$}}
-    | Protocol namedSigs :: :: protocol
-    % TODO: I now believe that this is wrong, and that protocols should live in their own namespace.
-    % 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
-
-namedSigs :: named_signatures_ ::=
-    | { x0 -> sig0 , .. , xn -> sign } :: :: explicit
-    | U namedSigs0 .. namedSigsn :: :: union
-
-sigx :: signature_syntax_ ::=
-    | <( tparamAnon0 , .. , tparamAnonm )> ( tx0 , .. , txn ) -> tx :: :: sigx
-
-sig :: signature_ ::=
-    | <( tparamAnon0 , .. , tparamAnonm )> ( tval0 , .. , tvaln ) -> tval :: :: sig
-    % TODO: fix these tparamAnanon, they are clearly wrong.
-
-tparamAnon :: tparam_anon_ ::=
-    | t :: :: constexpr
-    | { y0 , .. , yn } :: :: tvar 
-
-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
-
-b :: single_behaviour_ ::=
-    | Return tval :: :: return
-    | Break :: :: break
-    | Continue :: :: continue
-    | Fallthrough :: :: fallthrough
-    | Nothing :: :: Nothing
-
-t {{tex \tau}} :: type_ ::= {{com type}}
-    | LVal ( tval , addressSpace ) :: :: lval {{com left value}}
-    | tval :: :: tval
-tval {{tex {\tau^{val} } }} :: type_value_ ::=
-    | Ptr ( tval , addressSpace ) :: :: ptr {{com pointer}}
-    | Ref ( tval , addressSpace ) :: :: array_ref {{com array reference}}
-    | [ tval ] :: :: array {{com array}}
-    | bool :: :: bool
-    | uint32 :: :: uint32 {{tex \textbf{uint32} }}
-    | void :: :: void
-    | TVar tid namedSigs :: :: tvar
-tx {{tex {\tau^{syntax} } }} :: type_syntactic_ ::= {{com syntactic type}}
-    | x <( targ0 , .. , targm )> :: :: base
-    | tx * addressSpace :: :: ptr
-    | tx [] addressSpace :: :: array_ref 
-    | tx [ i ] :: :: array_fixed_size
-addressSpace, as :: address_space_ ::=
-    | thread :: :: thread
-    | threadgroup :: :: threadgroup
-    | device :: :: device
-    | constant :: :: constant
-tid :: type_identifier_ ::=
-
-rval, rv :: rval_ ::=
-    | { x0 : rval0 ; .. ; xn : rvaln } :: :: struct
-    | [ rval0 , .. , rvaln ] :: :: array
-    | 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}}, 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
-    | addr <- rval :: :: store {{com store}}
-    | addr -> rval :: :: load {{com load}}
-    | Sequence ( E0 , .. , En ) :: :: multiple_events
-
-fid :: function_identifier_ ::=
-
-S :: stack_event_ ::= {{com stack event}}
-    | :: :: nothing
-    | push ( rval ) :: :: push
-    | pop ( ) :: :: pop
-
-terminals :: terminals_ ::=
-    | U :: :: big_union {{tex \bigcup}}
-    | |- :: :: vdash {{tex \vdash}}
-    | <- :: :: load {{tex \leftarrow}}
-    | -> :: :: mapsto {{tex \mapsto}}
-    | --> :: :: desugars {{tex \leadsto}}
-    | <( :: :: 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
-    | 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]]}}
-    | G |- isIntegerOrEnum ( t ) :: :: is_integer
-    | G |- sc0 .. scn fully covers t :: :: full_switch_coverage % TODO: make it explicit
-    | s != s' :: :: stmt_not_eq {{tex [[s]] \neq [[s']]}}
-    | tval != tval' :: :: tval_not_eq {{tex [[tval]] \neq [[tval']]}}
-    | as != as' :: :: address_space_not_eq {{tex [[as]] \neq [[as']]}}
-    | b in B :: :: behaviour_in {{tex [[b]] \in [[B]]}}
-    | b not in B :: :: behaviour_not_in {{tex [[b]] \not\in [[B]]}}
-    | G = G' :: :: typing_env_eq
-    | B = B' :: :: behaviour_eq
-    | namedSigs = namedSigs' :: :: named_signature_eq
-    | sig = sig' :: :: sig_eq
-    | 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 % TODO: fix typesetting
-    | s = { sblock } :: :: block_from_switch_block
-    | rv = Default ( tval ) :: :: default_value
-    | s is a terminator :: :: stmt_is_terminator
-
-defns
-desugaring :: '' ::=
-defn
-s --> s' :: :: desugaring_stmt :: '' {{com Desugaring statements}} by
-
-    ----------------------------- :: if_then
-    if (e) s --> if (e) s else {}
-
-    -------- :: empty_stmt
-    ; --> {}
-
-    -------------------------------------- :: while
-    while (e) s --> if (e) do s while (e);
-
-    -------------------------------------------------------------------------- :: for_empty_cond
-    for (eOrVDecls ; ; eOrNothing) s --> for (eOrVDecls ; true ; eOrNothing) s
-
-    --------------------------------------------------------------------------- :: for_empty_incr
-    for (eOrVDecls ; e ; ) s --> for (eOrVDecls ; e ; null) s
-
-    ------------------------------------------------ :: for_init_expr
-    for (e ; e' ; e'') s --> {e; while(e') {s e'';}}
-
-    ------------------------------------------------ :: for_init_empty
-    for ( ; e' ; e'') s --> while(e') {s e'';}
-
-    ------------------------------------------------------------------------------------------ :: for_init_vdecls
-    for (tx vdecl0 , .. , vdecln ; e' ; e'') s --> {tx vdecl0 , .. , vdecln; while(e') {s e'';}}
-
-    k > 0
-    -------------------------------------------------------------------------------------- :: multiple_vdecls
-    { s0..sn tx vdecl0, vdecl1, .., vdeclk; s'0..s'm} --> {s0..sn tx vdecl0; tx vdecl1, .., vdeclk; s'0..s'm}
-
-    ------------------------------------------------------------- :: initialized_vdecl
-    { s0..sn tx x = e; s'0..s'm} --> {s0..sn tx x; x = e; s'0..s'm}
-
-% TODO: replace foo(e0,..,en) by foo<>(e0,..,en)
-% Both in expressions, and in top-level declarations
-% TODO: also desugar syntactic types that have an addressSpace as a prefix.
-% Also make it an error to have an addressSpace and neither array ref nor ptr.
-defn
-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
-reduce_type :: '' ::=
-defn
-G |- tx : tval :: :: syntax :: '' {{com Evaluating types}} {{tex [[G]] [[|-]] [[tx]] \Downarrow [[tval]]}} by
-
-    x -> Typedef (<( )> -> tval) in G
-    ------------------------------- :: basic_typedef
-    G |- x <( )> : tval
-
-    G |- tx : tval
-    ------------------------- :: array
-    G |- tx [i] : [tval]
-
-    G |- tx : tval
-    ---------------------------------------- :: ref
-    G |- tx [] addressSpace : Ref(tval, addressSpace)
-
-    G |- tx : tval
-    --------------------------------------- :: ptr
-    G |- tx * addressSpace : Ptr(tval, addressSpace)
-
-defns
-well_formed :: '' ::=
-defn
-G |- well_formed ( td ) :: :: top_level :: '' by
-
-    G |- tx : tval
-    G |- {s0..sn} : {Return tval}
-    ---------------------------------- :: func_trivial
-    G |- well_formed(tx f<()>() {s0..sn})
-
-    G |- tx0 : tval
-    G[x0 -> LVal(tval, thread)] |- well_formed (tx f<()>(tx1 x1, .., txm xm) {s0..sn})
-    -------------------------------------------------------------------- :: func_param
-    G |- well_formed (tx f<()>(tx0 x0, tx1 x1, .., txm xm) {s0..sn})
-
-    G |- tx' : tval'
-    G[x -> tval'] |- well_formed (tx f<(tparam0, .., tparamk)> (tx0 x0, .., txm xm) {s0..sn}) 
-    ---------------------------------------------------------------------------------------- :: 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
-    namedSigs = U namedSigs0 .. namedSigsi
-    tid = makeFresh()
-    G[x -> TVar tid namedSigs] |- well_formed (tx f<(tparam0, .., tparamk)> (tx0 x0, .., txm xm) {s0..sn})
-    ------------------------------------------------------------------------------------------------------ :: func_tvar
-    G |- well_formed (tx f<(x : y0 + .. + yi, tparam0, .., tparamk)> (tx0 x0, .., txm xm) {s0..sn}) 
-    % TODO: maybe add some check here that the different protocols are not incompatible.
-    % Can we even have incompatible protocols?
-
-defns
-typing :: '' ::=
-defn
-G |- s : B :: :: typing_statement :: '' {{com Validating statements' behaviours}} by
-
-    G |- e : bool
-    G |- s : B
-    G |- s' : B'
-    Return Ptr(tval, as) not in B
-    Return Ptr(tval, as) not in B'
-    Return Ref(tval, as) not in B
-    Return Ref(tval, as) not in B'
-    ------------------------------ :: if
-    G |- if (e) s else s' : B + B'
-    % The last 4 premises are useful for compiling to SpirV
-
-    G |- e : bool
-    G |- s : B
-    Return Ptr(tval, as) not in B
-    Return Ref(tval, as) not in 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 : tval
-    G |- isIntegerOrEnum(tval)
-    G |- sc0: tval /\ .. /\ G |- scn: tval
-    G |- sc0 .. scn fully covers tval
-    G |- sblock0: B0 /\ .. /\ G |- sblockn: Bn
-    B = U B0 .. Bn
-    Nothing not in B
-    Return Ptr(tval, as) not in B
-    Return Ref(tval, as) not in B
-    --------------------------------------------------------------------------- :: 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 : tval
-    ------------------------------ :: return
-    G |- return e; : {Return tval}
-
-    ----------------------------- :: return_void
-    G |- return ; : {Return void}
-
-    -------------------------- :: trap
-    G |- trap; : {Return tval}
-
-    ------------------- :: empty_block
-    G |- {} : {Nothing}
-
-    G[x -> Nothing] |- tx : tval
-    tval != Ptr(tval', as)
-    G[x -> LVal(tval, thread)] |- {s0 .. sn} : B
-    s0 != tx' x; /\../\ sn != tx' x;
-    s0 != tx' x = e'; /\../\ sn != tx' x = e';
-    -------------------------------------------- :: 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
-    % (see email from 20/06/2018).
-    % TODO: we can maybe put types in a different namespace instead.
-    % if they are applied where s is a variable declaration.
-    % Note: the last two premises prevent redeclaration of a variable in the same scope it was declared in.
-    % Implemented naively it takes O(n**2) to check, but can easily be optimized.
-
-    G[x -> Nothing] |- tx : tval
-    G[x -> LVal(tval, thread)] |- e : tval
-    G[x -> LVal(tval, thread)] |- {s0 .. sn} : B
-    s0 != tx' x; /\../\ sn != tx' x;
-    s0 != tx' x = e'; /\../\ sn != tx' x = e';
-    -------------------------------------------- :: variable_decl_init
-    G |- {tx x = e; s0 .. sn} : B
-
-    G |- s : B
-    ------------ :: trivial_block
-    G |- {s} : B
-
-    G |- s : B
-    G |- {s1 .. sn} : B'
-    n > 0
-    Fallthrough not in B
-    Nothing in B
-    -------------------------------------- :: block
-    G |- {s s1 .. 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.
-    % Note: the penultimate premise makes it a bit easier to compile to MSL, could be relaxed in future versions of the language.
-
-    G |- e : t
-    ------------------- :: expr
-    G |- e; : {Nothing}
-
-defn
-G |- sc : tval :: :: typing_switch_case :: '' by
-
-    G |- rval : tval
-    --------------------- :: case
-    G |- case rval : tval
-
-    ------------------- :: default
-    G |- default : tval
-
-defn
-G |- sblock : B :: :: typing_switch_block :: '' by
-
-    G |- { s0 .. sn } : B
-    --------------------- :: switch_block
-    G |- s0 .. sn : B
-
-defn
-G |- e : t :: :: typing_expr :: '' {{com Typing expressions}} by
-
-    -------------------------- :: null_lit_array_ref
-    G |- null : Ref (tval, as)
-
-    -------------------------- :: null_lit_ptr
-    G |- null : Ptr (tval, as)
-
-    ---------------- :: literal_true
-    G |- true : bool
-
-    ----------------- :: literal_false
-    G |- false : bool
-
-    G |- e : t
-    ------------ :: parens
-    G |- (e) : t
-
-    G |- e : t
-    G |- e' : t'
-    --------------- :: comma
-    G |- e, e' : t'
-
-    G |- e : bool
-    G |- e' : bool
-    ------------------- :: or
-    G |- e || e' : bool
-
-    G |- e : bool
-    G |- e' : bool
-    ------------------- :: and
-    G |- e && e' : bool
-
-    G |- e0 : bool
-    G |- e1 : t
-    G |- e2 : t
-    --------------------- :: ternary
-    G |- e0 ? e1 : e2 : t
-
-    G |- e : bool
-    -------------- :: not
-    G |- !e : bool
-
-    G |- e : LVal(tval, as)
-    G |- e' : tval
-    as != constant
-    ----------------------- :: assignment
-    G |- e = e' : tval
-
-    x -> t in G
-    ----------- :: variable_name
-    G |- x : t
-
-    G |- e : LVal(tval, as)
-    ----------------------- :: lval_access
-    G |- e : tval
-
-    G |- e : LVal(tval, as)
-    ----------------------- :: address_taking
-    G |- &e : Ptr(tval, as)
-    % can the unary operator & be overloaded?
-    % It seems that no
-
-    G |- e : Ptr(tval, as)
-    ------------------------ :: ptr_deref
-    G |- *e : LVal(tval, as)
-    % 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(tval, as)
-    ------------------------ :: take_ref_lval
-    G |- @e : Ref(tval, as)
-    % 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([tval], as)
-    G |- e' : uint32
-    --------------------------- :: array_index_lval
-    G |- e[e'] : LVal(tval, as)
-
-    G |- e : [tval]
-    G |- e' : uint32
-    ---------------- :: array_index_rval
-    G |- e[e'] : tval
-    % 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(tval, as)
-    G |- e' : uint32
-    --------------------------- :: array_ref_index
-    G |- e[e'] : LVal(tval, as)
-
-    G |- e0 : tval0 /\../\ G |- en : tvaln
-    x -> Func{sig0, .., sigk} in G
-    exists i . sigi = <( )> (tval0, .., tvaln) -> tval
-    -------------------------------------------------- :: call_no_targ
-    G |- x <( )> (e0, .., en) : tval
-
-defns
-exec :: '' ::=
-defn
-R |- e -> e' ; E ; S :: :: exec_expr :: '' {{com Small-step reduction on expressions}} {{tex [[R]] \vdash [[e]] \xrightarrow[ [[S]] ]{[[E]]} [[e']]}} by
-
-    ------------------------------------------- :: and_true
-    R |- true && e -> JoinExpr(e) ;; push(true)
-
-    --------------------------- :: and_false
-    R |- false && e -> false ;;
-
-    R |- e0 -> e0' ; E ; S
-    ---------------------------------- :: and_reduce
-    R |- e0 && e1 -> e0' && e1 ; E ; S
-
-    e != LVal(addr)
-    R |- e -> e' ; E ; S
-    --------------------------------------- :: join_expr_reduce
-    R |- JoinExpr(e) -> JoinExpr(e'); E ; S
-
-    ---------------------------------- :: join_expr_elim
-    R |- JoinExpr(val) -> val; ; pop()
-
-    ------------------------- :: or_true
-    R |- true || e -> true ;;
-
-    --------------------------------------------- :: or_false
-    R |- false || e -> JoinExpr(e) ;; push(false)
-
-    R |- e0 -> e0' ; E ; S
-    ---------------------------------- :: or_reduce
-    R |- e0 || e1 -> e0' || e1 ; E ; S
-
-    ------------------------------------------------- :: ternary_true
-    R |- true ? e1 : e2 -> JoinExpr(e1) ;; push(true)
-
-    --------------------------------------------------- :: ternary_false
-    R |- false ? e1 : e2 -> JoinExpr(e2) ;; push(false)
-
-    R |- e0 -> e0' ; E ; S
-    ------------------------------------------ :: ternary_reduce
-    R |- e0 ? e1 : e2 -> e0' ? e1 : e2 ; E ; S
-
-    ---------------------- :: comma_next
-    R |- rval, e1 -> e1 ;;
-
-    R |- e0 -> e0' ; E ; S
-    ------------------------------ :: comma_reduce
-    R |- e0, e1 -> e0', e1 ; E ; S
-
-    ------------------ :: parens_exec
-    R |- ( e ) -> e ;;
-
-    ----------------------- :: not_true
-    R |- ! true -> false ;;
-
-    ----------------------- :: not_false
-    R |- ! false -> true ;;
-
-    --------------------------------- :: deref_ptr
-    R |- * Ptr(addr) -> LVal(addr) ;;
-
-    R |- e -> e' ; E ; S
-    ------------------------ :: deref_reduce
-    R |- * e -> * e' ; E ; S
-
-    e != LVal(addr)
-    R |- e -> e' ; E ; S
-    ------------------------ :: take_ptr_reduce
-    R |- & e -> & e' ; E ; S
-
-    -------------------------------- :: 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 ; S
-    -------------------------------- :: array_left_reduce
-    R |- e0 [e1] -> e0' [e1] ; E ; S
-
-    e0 = LVal(addr) \/ e0 = [rval0, .., rvaln] \/ e0 = Ref(addr, j)
-    R |- e1 -> e1' ; E ; S
-    --------------------------------------------------------------- :: array_right_reduce
-    R |- e0 [e1] -> e0 [e1'] ; E ; S
-    
-    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 ; S
-    -------------------------------- :: assign_left_reduce
-    R |- e0 = e1 -> e0' = e1 ; E ; S
-
-    R |- e1 -> e1' ; E ; S
-    ------------------------------------------------ :: assign_right_reduce
-    R |- LVal(addr) = e1 -> LVal(addr) = e1' ; E ; S
-
-    ---------------------------------------------- :: assign_execute
-    R |- LVal(addr) = rval -> rval ; addr <- rval;
-
-    R |- e -> e' ; E ; S
-    ---------------------------------------------------------------------------------------------------------------------- :: call_reduce
-    R |- fid<(rv0, .., rvn)>(rv'0, .., rv'm, e, e0, .., ek) -> fid<(rv0, .., rvn)>(rv'0, .., rv'm, e', e0, .., ek) ; E ; S
-
-    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 ; S
-    ------------------------------ :: call_construct_reduce
-    R |- Call s -> Call s' ; E ; S
-
-    --------------------------------- :: 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 ; S :: :: exec_stmt :: '' {{com Small-step reduction on statements}} {{tex [[R]] \vdash [[s]] \xrightarrow[ [[S]] ]{[[E]]} [[s']]}} by
-
-    ----------------------------- :: block_annotate
-    R |- {s0..sn} -> {R s0..sn};;
-
-    R |- s -> s' ; E ; S
-    --------------------------------------------- :: block_reduce
-    Rout |- {R s s1..sn} -> {R s' s1..sn} ; E ; S
-
-    --------------------------------------- :: 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)]
-    rv = Default(tval)
-    ------------------------------------------------------------ :: block_vdecl
-    Rout |- {R tval x : sid; s1..sn} -> {R' s1..sn} ; sid <- rv;
-
-    R[x -> LVal(sid)] |- e -> e';;
-    ------------------------------------------------------------ :: block_vdecl_init_reduce
-    Rout |- {R tval x : sid = e; s1..sn} -> {R tval x : sid = e'; s1..sn} ;;
-
-    R' = R[x -> LVal(sid)]
-    ------------------------------------------------------------ :: block_vdecl_init_complete
-    Rout |- {R tval x : sid = rv; s1..sn} -> {R' s1..sn} ; sid <- rv;
-
-    R |- e -> e' ; E ; S
-    ---------------------- :: effectful_expr_reduce
-    R |- e; -> e'; ; E ; S
-
-    ------------------- :: effectful_expr_elim
-    R |- rval; -> {} ;;
-
-    R |- e -> e' ; E ; S
-    ------------------------------------ :: return_reduce
-    R |- return e; -> return e'; ; E ; S
-
-    R |- e -> e' ; E ; S
-    -------------------------------------------------- :: if_reduce
-    R |- if (e) s else s' -> if (e') s else s' ; E ; S
-
-    ------------------------------------------------- :: if_true
-    R |- if (true) s else s' -> Join(s) ;; push(true)
-    
-    ---------------------------------------------------- :: if_false
-    R |- if (false) s else s' -> Join(s') ;; push(false)
-
-    R |- s -> s' ; E ; S
-    -------------------------------- :: join_reduce
-    R |- Join(s) -> Join(s') ; E ; S
-
-    s = {R'} \/ s is a terminator
-    ----------------------------- :: join_elim
-    R |- Join(s) -> s ;; pop()
-
-    -------------------------------------------------------------- :: do_while_loop
-    R |- do s while(e); -> Loop(s, if(e) do s while(e); else {});;
-
-    R |- s1 -> s1' ; E ; S
-    ------------------------------------------ :: loop_reduce
-    R |- Loop(s1, s2) -> Loop(s1', s2) ; E ; S
-
-    ----------------------------- :: 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 ; S
-    ---------------------------------------------------------------------------------------------- :: switch_reduce
-    R |- switch(e) {sc0:sblock0 .. scn:sblockn} -> switch(e') {sc0:sblock0 .. scn:sblockn} ; E ; S
-
-%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? 
-    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) ;; push(rv)
-
-    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) ;; push(rv)
-
-    R |- s -> s' ; E ; S
-    ------------------------------------------------------ :: cases_reduce
-    R |- Cases(s, s0, .., sn) -> Cases(s', s0, .., sn) ; E ; S
-
-    ----------------------------------------------------------- :: cases_fallthrough
-    R |- Cases(fallthrough;, s0, .., sn) -> Cases(s0, .., sn);;
-
-    --------------------------------------------- :: cases_break
-    R |- Cases(break;, s0, .., sn) -> {} ;; pop()
-
-    s = continue; \/ s = return; \/ s = return rval; \/ s = trap;
-    ------------------------------------------------------------- :: cases_other_terminator
-    R |- Cases(s, s0, .., sn) -> s ;; pop()
diff --git a/Tools/WebGPUShadingLanguageRI/SpecWork/source/conf.py b/Tools/WebGPUShadingLanguageRI/SpecWork/source/conf.py
deleted file mode 100644 (file)
index 6bda789..0000000
+++ /dev/null
@@ -1,166 +0,0 @@
-# -*- 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 = 'nature'
-
-# 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
diff --git a/Tools/WebGPUShadingLanguageRI/SpecWork/source/index.rst b/Tools/WebGPUShadingLanguageRI/SpecWork/source/index.rst
deleted file mode 100644 (file)
index 12922a8..0000000
+++ /dev/null
@@ -1,463 +0,0 @@
-.. WSL documentation master file, created by
-   sphinx-quickstart on Thu Jun  7 15:53:54 2018.
-   You can adapt this file completely to your liking, but it should at least
-   contain the root `toctree` directive.
-
-WSL Specification
-#################
-
-Grammar
-=======
-
-Lexical analysis
-----------------
-
-Before parsing, the text of a WSL program is first turned into a list of tokens, removing comments and whitespace along the way.
-Tokens are built greedily, in other words each token is as long as possible.
-If the program cannot be transformed into a list of tokens by following these rules, the program is invalid and must be rejected.
-
-A token can be either of:
-
-- An integer literal
-- A float literal
-- Punctuation
-- A keyword
-- A normal identifier
-- An operator name
-
-Literals
-""""""""
-
-An integer literal can either be decimal or hexadecimal, and either signed or unsigned, giving 4 possibilities.
-
-- A signed decimal integer literal starts with an optional ``-``, then a number without leading 0.
-- An unsigned decimal integer literal starts with a number without leading 0, then ``u``.
-- A signed hexadecimal integer literal starts with an optional ``-``, then the string ``0x``, then a non-empty sequence of elements of [0-9a-fA-F] (non-case sensitive, leading 0s are allowed).
-- An unsigned hexadecimal inter literal starts with the string ``0x``, then a non-empty sequence of elements of [0-9a-fA-F] (non-case sensitive, leading 0s are allowed), and finally the character ``u``.
-
-.. todo:: I chose rather arbitrarily to allow leading 0s in hexadecimal, but not in decimal integer literals. This can obviously be changed either way.
-
-A float literal is made of the following elements in sequence:
-
-- an optional ``-`` character
-- a sequence of 0 or more digits (in [0-9])
-- a ``.`` character
-- a sequence of 0 or more digits (in [0-9]). This sequence must instead have 1 or more elements, if the last sequence was empty.
-- optionally a ``f`` or ``d`` character
-
-In regexp form: '-'? ([0-9]+ '.' [0-9]* | [0-9]* '.' [0-9]+) [fd]?
-
-Keywords and punctuation
-""""""""""""""""""""""""
-
-The following strings are reserved keywords of the language:
-
-+-------------------------------+---------------------------------------------------------------------------------+
-| Top level                     | struct typedef enum operator vertex fragment native restricted                  |
-+-------------------------------+---------------------------------------------------------------------------------+
-| Control flow                  | if else switch case default while do for break continue fallthrough return trap |
-+-------------------------------+---------------------------------------------------------------------------------+
-| Literals                      | null true false                                                                 |
-+-------------------------------+---------------------------------------------------------------------------------+
-| Address space                 | constant device threadgroup thread                                              |
-+-------------------------------+---------------------------------------------------------------------------------+
-| Reserved for future extension | protocol auto                                                                   |
-+-------------------------------+---------------------------------------------------------------------------------+
-
-``null``, ``true`` and ``false`` are keywords, but they are considered literals in the grammar rules later.
-
-Similarily, the following elements of punctuation are valid tokens:
-
-+----------------------+-----------------------------------------------------------------------------------------------+
-| Relational operators | ``==`` ``!=`` ``<=`` ``=>`` ``<`` ``>``                                                       |
-+----------------------+-----------------------------------------------------------------------------------------------+
-| Assignment operators | ``=`` ``++`` ``--`` ``+=`` ``-=`` ``*=`` ``/=`` ``%=`` ``^=`` ``&=``  ``|=`` ``>>=``  ``<<=`` |
-+----------------------+-----------------------------------------------------------------------------------------------+
-| Arithmetic operators | ``+``  ``-`` ``*`` ``/`` ``%``                                                                |
-+----------------------+-----------------------------------------------------------------------------------------------+
-| Logic operators      | ``&&`` ``||`` ``&``  ``|``  ``^`` ``>>`` ``<<`` ``!`` ``~``                                   |
-+----------------------+-----------------------------------------------------------------------------------------------+
-| Memory operators     | ``->`` ``.`` ``&`` ``@``                                                                      |
-+----------------------+-----------------------------------------------------------------------------------------------+
-| Other                | ``?`` ``:`` ``;`` ``,`` ``[`` ``]`` ``{`` ``}`` ``(`` ``)``                                   |
-+----------------------+-----------------------------------------------------------------------------------------------+
-
-Identifiers and operator names
-""""""""""""""""""""""""""""""
-
-An identifier is any sequence of alphanumeric characters or underscores, that does not start by a digit, that is not a single underscore (the single underscore is reserved for future extension), and that is not a reserved keyword.
-TODO: decide if we only accept [_a-zA-Z][_a-zA-Z0-9], or whether we also accept unicode characters.
-
-Operator names can be either of the 4 following possibilities:
-
-- the string ``operator``, followed immediately with one of the following strings: ``>>``, ``<<``, ``+``, ``-``, ``*``, ``/``, ``%``, ``&&``, ``||``, ``&``, ``|``, ``^``, ``>=``, ``<=``, ``>``, ``<``, ``++``, ``--``, ``!``, ``~``, ``[]``, ``[]=``, ``&[]``.
-- the string ``operator.`` followed immediately with what would be a valid identifier x. We call this token a 'getter for x'.
-- the string ``operator.`` followed immediately with what would be a valid identifier x, followed immediately with the character ``=``. We call this token 'a setter for x'.
-- the string ``operator&.`` followed immediately with what would be a valid identifier x. We call this token an 'address taker for x'.
-
-.. note:: Thanks to the rule that token are read greedily, the string "operator.foo" is a single token (a getter for foo), and not the keyword "operator" followed by the punctuation "." followed by the identifier "foo".
-
-Whitespace and comments
-"""""""""""""""""""""""
-
-Any of the following characters are considered whitespace, and ignored after this phase: space, tabulation (``\t``), carriage return (``\r``), new line(``\n``).
-
-.. todo:: do we want to also allow other unicode whitespace characters?
-
-We also allow two kinds of comments, that are treated like whitespace (i.e. ignored during parsing).
-The first kind is a line comment, that starts with the string ``//`` and continues until the next end of line character.
-The second kind is a multi-line comment, that starts with the string ``/*`` and ends as soon as the string ``*/`` is read.
-
-.. note:: Multi-line comments cannot be nested, as the first ``*/`` closes the outermost ``/*``
-
-Parsing
--------
-
-.. todo:: add here a quick explanation of BNF syntax and our conventions.
-
-Top-level declarations
-""""""""""""""""""""""
-
-A valid file is made of a sequence of 0 or more top-level declarations, followed by the special End-Of-File token.
-
-.. productionlist::
-    topLevelDecl: ";" | `typedef` | `structDef` | `enumDef` | `funcDef`
-
-.. todo:: We may want to also allow variable declarations at the top-level if it can easily be supported by all of our targets.
-.. todo:: Decide whether we put native/restricted in the spec or not.
-
-.. productionlist::
-    typedef: "typedef" `Identifier` "=" `type` ";"
-
-.. productionlist::
-    structDef: "struct" `Identifier` "{" `structElement`* "}"
-    structElement: `type` `Identifier` ";"
-
-.. productionlist::
-    enumDef: "enum" `Identifier` (":" `type`)? "{" `enumElement` ("," `enumElement`)* "}"
-    enumElement: `Identifier` ("=" `constexpr`)?
-
-.. productionlist::
-    funcDef: `funcDecl` "{" `stmt`* "}"
-    funcDecl: `entryPointDecl` | `normalFuncDecl` | `castOperatorDecl`
-    entryPointDecl: ("vertex" | "fragment") `type` `Identifier` `parameters`
-    normalFuncDecl: `type` (`Identifier` | `OperatorName`) `parameters`
-    castOperatorDecl: "operator" `type` `parameters`
-    parameters: "(" ")" | "(" `parameter` ("," `parameter`)* ")"
-    parameter: `type` `Identifier`
-
-.. note:: the return type is put after the "operator" keyword when declaring a cast operator, mostly because it is also the name of the created function. 
-
-Statements
-""""""""""
-
-.. productionlist::
-    stmt: "{" `stmt`* "}"
-        : | `compoundStmt` 
-        : | `terminatorStmt` ";" 
-        : | `variableDecls` ";" 
-        : | `maybeEffectfulExpr` ";"
-    compoundStmt: `ifStmt` | `ifElseStmt` | `whileStmt` | `doWhileStmt` | `forStmt` | `switchStmt`
-    terminatorStmt: "break" | "continue" | "fallthrough" | "return" `expr`? | "trap"
-
-.. productionlist::
-    ifStmt: "if" "(" `expr` ")" `stmt`
-    ifElseStmt: "if" "(" `expr` ")" `stmt` "else" `stmt`
-
-.. todo:: should I forbid assignments (without parentheses) inside the conditions of if/while to avoid the common mistaking of "=" for "==" ? 
-
-The first of these two productions is merely syntactic sugar for the second:
-
-.. math:: \textbf{if}(e) \,s \leadsto \textbf{if}(e) \,s\, \textbf{else} \,\{\}
-
-.. productionlist::
-    whileStmt: "while" "(" `expr` ")" `stmt`
-    forStmt: "for" "(" (`maybeEffectfulExpr` | `variableDecls`) ";" `expr`? ";" `expr`? ")" `stmt`
-    doWhileStmt: "do" `stmt` "while" "(" `expr` ")" ";"
-
-Similarily, we desugar first for loops into while loops, and then all while loops into do while loops.
-First, if the second element of the for is empty we replace it by "true".
-Then, we apply the following two rules:
-
-.. math::
-    \textbf{for} (X_{pre} ; e_{cond} ; e_{iter}) \, s \leadsto \{ X_{pre} ; \textbf{while} (e_{cond}) \{ s \, e_{iter} ; \} \}
-
-.. math::
-    \textbf{while} (e)\, s \leadsto \textbf{if} (e) \textbf{do}\, s\, \textbf{while}(e)
-
-.. productionlist::
-    switchStmt: "switch" "(" `expr` ")" "{" `switchCase`* "}"
-    switchCase: ("case" `constexpr` | "default") ":" `stmt`*
-
-.. productionlist::
-    variableDecls: `type` `variableDecl` ("," `variableDecl`)*
-    variableDecl: `Identifier` ("=" `expr`)?
-
-Complex variable declarations are also mere syntactic sugar.
-Several variable declarations separated by commas are the same as separating them with semicolons and repeating the type for each one.
-This transformation can always be done because variable declarations are only allowed inside blocks (and for loops, but these get desugared into a block, see above).
-
-.. todo:: should I make the requirement that variableDecls only appear in blocks be part of the syntax, or should it just be part of the validation rules?
-
-Types
-"""""
-
-.. productionlist::
-    type: `addressSpace` `Identifier` `typeArguments` `typeSuffixAbbreviated`+
-        : | `Identifier` `typeArguments` `typeSuffixNonAbbreviated`*
-    addressSpace: "constant" | "device" | "threadgroup" | "thread"
-    typeSuffixAbbreviated: "*" | "[" "]" | "[" `IntLiteral` "]"
-    typeSuffixNonAbbreviated: "*" `addressSpace` | "[" "]" `addressSpace` | "[" `IntLiteral` "]"
-
-
-Putting the address space before the identifier is just syntactic sugar for having that same address space applied to all type suffixes.
-``thread int *[]*[42]`` is for example the same as ``int *thread []thread *thread [42]``.
-
-.. productionlist::
-    typeArguments: "<" (`typeArgument` ",")* `addressSpace`? `Identifier` "<" 
-                 : (`typeArgument` ("," `typeArgument`)*)? ">>"
-                 : | "<" (`typeArgument` ("," `typeArgument`)* ">"
-                 : | ("<" ">")?
-    typeArgument: `constepxr` | `type`
-
-The first production rule for typeArguments is a way to say that `>>` can be parsed as two `>` closing delimiters, in the case of nested typeArguments.
-
-Expressions
-"""""""""""
-
-We accept three different kinds of expressions, in different places in the grammar.
-
-- ``expr`` is the most generic, and includes all expressions.
-- ``maybeEffectfulExpr`` is used in places where a variable declaration would also be allowed. It forbids some expressions that are clearly effect-free, such as ``x*y`` or ``x < y``.
-  As the name indicates, it may be empty. In that case it is equivalent to "null" (any other effect-free expression would be fine, as the result of such an expression is always discarded).
-- ``constexpr`` is limited to literals and the elements of an enum. It is used in switch cases, and in type arguments.
-
-.. productionlist::
-    expr: (`expr` ",")? `ternaryConditional`
-    ternaryConditional: `exprLogicalOr` "?" `expr` ":" `ternaryConditional`
-                      : | `exprPrefix` `assignOperator` `ternaryConditional`
-                      : | `exprLogicalOr`
-    assignOperator: "=" | "+=" | "-=" | "*=" | "/=" | "%=" | "&=" | "|=" | "^=" | ">>=" | "<<="
-    exprLogicalOr: (`exprLogicalOr` "||")? `exprLogicalAnd`
-    exprLogicalAnd: (`exprLogicalAnd` "&&")? `exprBitwiseOr`
-    exprBitwiseOr: (`exprBitwiseOr` "|")? `exprBitwiseXor`
-    exprBitwiseXor: (`exprBitwiseXor` "^")? `exprBitwiseAnd`
-    exprBitwiseAnd: (`exprBitwiseAnd` "&")? `exprRelational`
-    exprRelational: `exprShift` (`relationalBinop` `exprShift`)?
-    relationalBinop: "<" | ">" | "<=" | ">=" | "==" | "!="
-    exprShift: (`exprShift` ("<<" | ">>"))? `exprAdd`
-    exprAdd: (`exprMult` ("*" | "/" | "%"))? `exprPrefix`
-    exprPrefix: `prefixOp` `exprPrefix` | `exprSuffix`
-    prefixOp: "++" | "--" | "+" | "-" | "~" | "!" | "*" | "&" | "@"
-    exprSuffix: `callExpression` `limitedSuffixOp`*
-              : | `term` (`limitedSuffixOp` | "++" | "--")*
-    limitedSuffixOp: "." `Identifier` | "->" `Identifier` | "[" `expr` "]"
-    callExpression: `Identifier` "(" (`ternaryConditional` ("," `ternaryConditional`)*)? ")"
-    term: `Literal` | `Identifier` | "(" `expr` ")"
-
-We match the precedence and associativity of operators from C++, with one exception: we made relational operators non-associative,
-so that they cannot be chained. Chaining them has sufficiently surprising results that it is not a clear reduction in usability, and it should make it a lot easier to extend the syntax in the future to accept generics.
-
-There is exactly one piece of syntactic sugar in the above rules: the ``!=`` operator.
-``e0 != e1`` is equivalent with ``! (e0 == e1)``.
-
-.. productionlist::
-    maybeEffectfulExpr: (`effAssignment` ("," `effAssignment`)*)?
-    effAssignment: `exprPrefix` `assignOperator` `expr` | `effPrefix`
-    effPrefix: ("++" | "--") `exprPrefix` | `effSuffix`
-    effSuffix: `exprSuffix` ("++" | "--") | `callExpression` | "(" `expr` ")"
-
-The structure of maybeEffectfulExpr roughly match the structure of normal expressions, just with normally effect-free operators left off.
-
-If the programmer still wants to use them in such a position (for example due to having overloaded an operator with an effectful operation),
-it can be done just by wrapping the expression in parentheses (see the last alternative for effSuffix).
-
-.. productionlist::
-    constexpr: `Literal` | `Identifier` "." `Identifier`
-
-Validation
-===========
-
-Phase 1: Gathering declarations
--------------------------------
-
-the goal is to build the global typing environment, as well as the global execution environment.
-I am afraid it may require several steps.
-The first step would do most of the work, gathering all function signatures, as well as typedefs, etc..
-The second step would go through the resulting environment, resolving all types, in particular all typedefs (as well as connecting function parameters to the corresponding type variables, etc..)
-
-Phase 2: Local typing and early validation
-------------------------------------------
-
-Notations and definitions
-"""""""""""""""""""""""""
-
-- Definition of the typing environment
-- Definition of the type hierarchy
-- Definition of the type evaluation judgement
-
-Validating top-level declarations
-"""""""""""""""""""""""""""""""""
-
-Typedefs and structs:
-
-- checking no recursive types (both structs and typedefs.. maybe as part of the computation of the size of each type)
-  No, the computation of the size of each type will necessarily happen during monomorphisation
-  And we cannot defer this check until then, because we will need to eliminate all typedefs during the local typing phase.
-
-Structs:
-
-- checking that structs have distinct names for different fields, and that the type of their fields are well-defined (and non-void)
-
-Enums:
-
-- check that enums do not have duplicate values, and have one zero-valued element.
-- check that enums have an integer base type (not another enum in particular).
-- check that every value given to an enum element fits in the base type.
-
-Protocols:
-
-- check that each signature inside a protocol refers to the protocol name (aka type variable).
-- check that the extension relation on protocols is sane (at the very least acyclic, maybe also no incompatible signatures for the same function name).
-
-Functions:
-
-- check that operator.field, operator.field=, operator[] and operator[]= are not defined for pointer types, nor declared for pointer types in a protocol.
-- check that operator.field= is only defined if operator.field is as well, and that they agree on their return type in that case.
-- check that operator[]= is only defined if operator[] is as well, and that they agree on their return type in that case.
-- check that all of the type parameters of each operator declaration/definition are inferrable from their arguments (and from its return type in the case of cast operators).
-- check that no argument is of type void
-- finally, check that the function body can only end with a return of the right type, or with Nothing if it is a void function
-
-Typing statements
-"""""""""""""""""
-
-Typing expressions
-""""""""""""""""""
-
-- typing rules (this and everything that follows can be managed by just a pair of judgements that type stmts/exprs)
-- checking returns
-- check that every variable declaration is in a block or at the top-level
-- check that no variable declaration shadows another one at the same scope
-- check that no variable is declared of type void
-- check that switch statements treat all cases
-- check that every case in a switch statement ends in a terminator (fallthrough/break/return/continue/trap)
-- check that literals fit into the type they are stored into (optional?)
-
-Phase 3: Monomorphisation and late validation
----------------------------------------------
-
-- monomorphisation itself
-- resolving function calls (probably done as part of monomorphisation)
-- checking no recursive functions (seems very hard to do before that step, as it requires resolving overloaded functions)
-- allocating a unique store identifier to each function parameter and variable declaration
-- annotating each array access with the stride used by that array type? If we do it here and not at runtime, then each assignment would also need a size annotation..
-- checks of proper use of address spaces
-
-Dynamic rules
-=============
-
-Definitions
------------
-
-We split the semantics in two parts: a per-thread execution semantics that does not know anything about concurrency or the memory, and a global set of rules for
-loads, stores, barriers and the like.
-
-The per-thread semantics is a fairly classic small-step operational semantics, meaning that it describes what a list of possible transitions that the program can
-take in one step.
-The per-thread state is made of a few element:
-
-- The program being executed. Each transition transforms it.
-- A control-flow stack. This is a stack of values, which tracks whether we are in a branch, and is used by the rules for barriers to check that control-flow is uniform.
-- A (constant) environment. This is a mapping from variable names to values and is used to keep track of arguments and variables declared in the function.
-
-Each transition is a statement of the form "With environment :math:`\rho`, if some conditions are respected, the program may be transformed into the following, modifing
-the control-flow stack in the following way, and emitting the following memory events."
-
-Execution of statements
------------------------
-
-Blocks and variable declarations
-""""""""""""""""""""""""""""""""
-
-The program fragments that we use to define our semantics are richer than just the syntactically correct programs. In particular, we allow annotating blocks
-(sequences of statements between braces) with an environment.
-
-Here is how to reduce a block by one step:
-
-#. If the block is not annotated, annotate it with the environment
-#. If the first statement of the block is an empty block, remove it
-#. Else if the first statement of the block is a terminator (break, continue, fallthrough, return or trap), replace the entire block by it.
-#. Else if the first statement of the block is a variable declaration:
-
-   #. Make a new environment from the one that annotates the block, mapping the variable name to its store identifier.
-   #. If the variable declaration has an initializing expression that can be reduced, reduce it using the new environment
-   #. Else:
-
-      #. Change the annotation of the block to the new environment.
-      #. Emit a store to the store identifier of the declaration, of a value that is either the initializing value (if available) or the default value for the type (otherwise)
-      #. Remove this variable declaration from the block
-
-#. Else reduce the first statement of the block, using the environment that the block was annotated with (not the top-level environment)
-
-.. todo:: Specify this "default value for the type". It should be very simple (null for ptrs/refs, false for booleans, 0/0. for ints/floats, and the natural extension for arrays/structs).
-
-Branches
-""""""""
-
-We add another kind of statement: the ``Join(s)`` construct, that takes as argument another statement ``s``.
-
-Here is how to reduce a branch (if-then-else construct, remember that if-then is just syntactic sugar that was eliminated during parsing) by one step:
-
-#. If the expression in the if is ``true`` or ``false``.
-
-   #. Push that value on the control flow stack
-   #. Replace the branch by the statement in the then (for ``true``) or else (for ``false``) branch, wrapped in the ``Join`` construct
-
-#. Else reduce that expression
-
-Here is how to reduce a ``Join(s)`` statement:
-
-#. If the argument of the ``Join`` is a terminator (``break;``, ``continue;``, ``fallthrough;``, ``return e?;`` or ``trap;``) or an empty block
-
-   #. Pop the last value from the control flow stack
-   #. Replace the ``Join`` statement by its argument
-
-#. Else reduce its argument
-
-.. note:: Popping the last value from the control flow stack never fails, as a Join only appears when eliminating a branch, which pushes a value on it.
-
-Switches
-""""""""
-
-We add another kind of statement: the ``Cases(..)`` construct that takes as argument a sequence.
-
-Loops
-"""""
-
-Barriers and uniform control flow
-"""""""""""""""""""""""""""""""""
-
-Other
-"""""
-
-TODO: return reduce, and effectful expr.
-
-Execution of expressions
-------------------------
-
-Memory model
-------------
-
-Standard library
-================
-
-Interface with JavaScript
-=========================
-
-Indices and tables
-##################
-
-* :ref:`genindex`
-* :ref:`modindex`
-* :ref:`search`