mirror of
https://github.com/dart-lang/sdk
synced 2024-10-14 17:40:04 +00:00
71 lines
4.6 KiB
Markdown
71 lines
4.6 KiB
Markdown
|
> [!IMPORTANT]
|
||
|
|
> This page was copied from https://github.com/dart-lang/sdk/wiki and needs review.
|
||
|
|
> Please [contribute](../CONTRIBUTING.md) changes to bring it up-to-date -
|
||
|
|
> removing this header - or send a CL to delete the file.
|
||
|
|
|
||
|
|
---
|
||
|
|
|
||
|
|
The small-step operational semantics of Dart Kernel is given by an abstract machine in the style of the CEK machine. The machine is defined by a single step transition function where each step of the machine starts in a configuration and deterministically gives a next configuration. There are several different configurations defined below.
|
||
|
|
|
||
|
|
_x_ ranges over variables, ρ ranges over environments, _K_ ranges over expression continuations, _A_ ranges over application continuations, _E_ ranges over expressions, _S_ ranges over statements, _V_ ranges over values.
|
||
|
|
|
||
|
|
Environments are finite functions from variables to values. _ρ_[_x_ → _V_] denotes the environment that maps _x_ to _V_ and _y_ to _ρ_(_y_) for all _y_ ≠ _x_.
|
||
|
|
|
||
|
|
#### Expression configuration
|
||
|
|
|
||
|
|
An expression configuration indicates the evaluation of an expression with respect to an environment and an expression continuation.
|
||
|
|
|
||
|
|
Expression configuration | Next configuration
|
||
|
|
-- | --
|
||
|
|
<_x_, _ρ_, _K_><sub>_expr_</sub> | <_K_, _ρ_(_x_), _ρ_><sub>_cont_</sub>
|
||
|
|
<_x = E_, _ρ_, _K_><sub>_expr_</sub> | <_E_, _ρ_, **VarSetK**(_x_, _K_)><sub>_expr_</sub>
|
||
|
|
<_!E_, _ρ_, _K_><sub>_expr_</sub> | <_E_, _ρ_, **NotK**(_K_)><sub>_expr_</sub>
|
||
|
|
<_E<sub>1</sub> **and** E<sub>2</sub>_, _ρ_, _K_><sub>_expr_</sub> | <_E<sub>1</sub>_, _ρ_, **AndK**(_E<sub>2</sub>_, _K_)><sub>_expr_</sub>
|
||
|
|
<_E<sub>1</sub> **or** E<sub>2</sub>_, _ρ_, _K_><sub>_expr_</sub> | <_E<sub>1</sub>_, _ρ_, **OrK**(_E<sub>2</sub>_, _K_)><sub>_expr_</sub>
|
||
|
|
<_E<sub>1</sub>? E<sub>2</sub> : E<sub>3</sub>_, _ρ_, _K_><sub>_expr_</sub> | <_E<sub>1</sub>_, _ρ_, **ConditionalK**(_E<sub>2</sub>_, _E<sub>3</sub>_, _K_)><sub>_expr_</sub>
|
||
|
|
<_StringConcat(exprList)_, _ρ_, _K_><sub>_expr_</sub> | <_exprList_, _ρ_, **StringConcatenationA**(_K_)><sub>_exprList_</sub>
|
||
|
|
<_print(E)_, _ρ_, _K_><sub>_expr_</sub> | <_E_, _ρ_, **PrintK**</sub>(_K_)><sub>_expr_</sub>
|
||
|
|
<_f(exprList)_, _ρ_, _K_><sub>_expr_</sub> | <_exprList_, _ρ_, **StaticInvocationA**(_S : f.body_, _K_)><sub>_exprList_</sub>
|
||
|
|
<_BasicLiteral_, _ρ_, _K_><sub>_expr_</sub> | <_K_, _BasicLiteral_, _ρ_><sub>_cont_</sub>
|
||
|
|
<_**Let** x = E<sub>1</sub> **in** E<sub>2</sub>_, _ρ_, _K_><sub>_expr_</sub> | <_E<sub>1</sub>_, _ρ_, **LetK**(_x_, E<sub>2</sub>, _ρ_, _K_)><sub>_expr_</sub>
|
||
|
|
|
||
|
|
|
||
|
|
#### Expression continuation configuration
|
||
|
|
|
||
|
|
An expression continuation configuration indicates the application of an expression continuation __K__ to a value and an environment. The environment is threaded to the continuation because expressions can mutate the environment.
|
||
|
|
|
||
|
|
Expression continuation configuration | Next configuration
|
||
|
|
-- | --
|
||
|
|
<**VarSetK**(_x_, _K_), _V_, _ρ_><sub>_cont_</sub> | <_K_, _V_, _ρ_[_x_ → _V_]><sub>cont</sub>
|
||
|
|
<**PrintK**(_K_), _V_, _ρ_><sub>_cont_</sub> | <_K_, _∅_, _ρ_><sub>cont</sub>
|
||
|
|
<**ExpressionListK**(_exprList_, _A_), _V_, _ρ_><sub>_cont_</sub> | <_exprList_, _ρ_, **ValueApplicationA**(_V_, _A_)><sub>_exprList_</sub>
|
||
|
|
<**ExpressionK**(_C_), _V_, _ρ_ ><sub>_cont_</sub> | _C_
|
||
|
|
|
||
|
|
#### Expression list configuration
|
||
|
|
|
||
|
|
An expression list configuration indicates the evaluation of a list of expressions with respect to an environment and an application continuation.
|
||
|
|
|
||
|
|
Expression list configuration | Next configuration
|
||
|
|
--|--
|
||
|
|
<_∅_, _ρ_, _A_><sub>_exprList_</sub> | <_A_, _∅_><sub>_acont_</sub>
|
||
|
|
<_E :: tail_, _ρ_, _A_><sub>_exprList_</sub> | <_E_, _ρ_, **ExpressionListK**(_tail_, _A_)><sub>_expr_</sub>
|
||
|
|
|
||
|
|
#### Application continuation configuration
|
||
|
|
|
||
|
|
An application continuation configuration indicates the application of __A__ to a list of values.
|
||
|
|
|
||
|
|
Application continuation configuration | Next configuration
|
||
|
|
--|--
|
||
|
|
<**StaticInvocationA**(_S_, _K_), _valList_><sub>_acont_</sub> | <_S_, _ρ_[_formalList_ → _valList_], _∅_, **ExitC**(_K_), _K_><sub>_exec_</sub>
|
||
|
|
<**ValueApplicationA**(V, _A_), _valList_><sub>_acont_</sub> | <_A_, _V :: valList_><sub>_acont_</sub>
|
||
|
|
|
||
|
|
#### Statement configuration
|
||
|
|
|
||
|
|
A statement configuration indicates the execution of a statement with respect to an environment.
|
||
|
|
|
||
|
|
_S_ ranges over statements, _L_ ranges over labels, _C_ ranges over statement configurations.
|
||
|
|
|
||
|
|
Statement configuration | Next configuration
|
||
|
|
--|--
|
||
|
|
<**Expression**(_E_), _ρ_, _L_, _C_, _K_><sub>_exec_</sub> | <_E_, _ρ_, **ExpressionK**(_C_)><sub>_expr_</sub>
|