makeGlobal packs toplevel definitions into Global. This assumes doesntHaveLeakOfLoopCounters.

evalExpr evaluates exprs of our restricted Python-like language.

Rules for \(e_1 \operatorname{boolop} e_2\)

\[ \cfrac{e_1 \mid \mu \Downarrow \mathbf{false}}{e_1 ~\mathbf{and}~ e_2 \mid \mu \Downarrow \mathbf{false}} \] \[ \cfrac{e_1 \mid \mu \Downarrow \mathbf{true} \qquad e_2 \mid \mu \Downarrow v}{e_1 ~\mathbf{and}~ e_2 \mid \mu \Downarrow v} \] \[ \vdots \]

Rules for \(e_1 \operatorname{binop} e_2\)

\[ \cfrac{e_1 \mid \mu \Downarrow v_1 \qquad e_2 \mid \mu \Downarrow v_2}{e_1 + e_2 \mid \mu \Downarrow (v_1 + v_2)} \] \[ \vdots \]

Rules for \(\operatorname{unaryop} e\)

Rules for \(\lambda x _ \tau x _ \tau \dots x _ \tau. e\)

\[ \lambda {x_0} _ {\tau _ 0} {x_1} _ {\tau _ 1} \dots {x _ {n - 1}} _ {\tau _ {n - 1}}. e \mid \mu \Downarrow \lambda _ {\mu} x_0 x_1 \dots x _ {n - 1}. e \]

Rules for \(\mathbf{if}~ e ~\mathbf{then}~ e ~\mathbf{else}~ e\)

Rules for \(\lbrack e ~\mathbf{for}~ y ~\mathbf{in}~ e ~(\mathbf{if}~ e)? \rbrack\)

Rules for \(e \operatorname{cmpop} e\)

Rules for \(e (e, e, \dots, e)\)

\[ \cfrac{ e \mid \mu \Downarrow \lambda _ {\mu'} x_0 x_1 \dots x _ {n - 1}. e' \qquad e_0 \mid \mu \Downarrow v_0 \qquad e_1 \mid \mu \Downarrow v_1 \qquad \dots \qquad e _ {n - 1} \mid \mu \Downarrow v _ {n - 1} \qquad e' \mid (x_0 \mapsto v_0; x_1 \mapsto v_1; \dots; x _ {n - 1} \mapsto v _ {n - 1}; \mu') \Downarrow v }{ e(e_0, e_1, \dots, e _ {n - 1}) \mid \mu \Downarrow v } \]

\[ \cfrac{ e \mid \mu \Downarrow b \qquad e_0 \mid \mu \Downarrow v_0 \qquad e_1 \mid \mu \Downarrow v_1 \qquad \dots \qquad e _ {n - 1} \mid \mu \Downarrow v _ {n - 1} }{ e(e_0, e_1, \dots, e _ {n - 1}) \mid \mu \Downarrow b(e_0, e_1, \dots, e _ {n - 1}) } \qquad{(b ~\text{is a builtin function})} \]

Rules for \(\operatorname{constant}\)

Rules for \(e \lbrack e \rbrack\)

Rules for \(x\)

\[ x \mid \mu \Downarrow \mu(x) \]

Rules for \(\lbrack e, e, \dots, e \rbrack _ \tau\)

Rules for \(e \lbrack e? \colon e? \colon e? \rbrack\)

evalStatement evaluates statements of our restricted Python-like language. When a statement is evaluated, it returns a value \(v\), doesn't return anything \(\mathbf{stop}\), or fails \(\mathbf{err}\). Also it updates the environment function \(\mu\) from variables to values.

Rules for \(\mathbf{return}~ e\)

\[ \cfrac{ e \mid \mu \Downarrow v }{ \mathbf{return}~ e \mid \mu \Downarrow v \mid \mu } \]

Rules for \(y \operatorname{binop} = e\)

\[ \cfrac{ y \operatorname{binop} e \mid \mu \Downarrow v }{ y \operatorname{binop} = e \mid \mu \Downarrow \mathbf{stop} \mid (y \mapsto v; \mu) } \]

Rules for \(y := e\)

\[ \cfrac{ e \mid \mu \Downarrow v }{ y \operatorname{binop} = e \mid \mu \Downarrow \mathbf{stop} \mid (y \mapsto v; \mu) } \]

Rules for \(\mathbf{for}~ y ~\mathbf{in}~ e \colon\quad \mathrm{stmt}; \mathrm{stmt}; \dots; \mathrm{stmt}\)

\[ \cfrac{ e \mid \mu \Downarrow \mathbf{nil} }{ (\mathbf{for}~ y ~\mathbf{in}~ e \colon~ \vec{\mathrm{stmt}}) \mid \mu \Downarrow \mathbf{stop} \mid \mu } \]

\[ \cfrac{ e \mid \mu \Downarrow \mathbf{cons}(v_1, v_2) \qquad \vec{\mathrm{stmt}} \mid (y \mapsto v_1; \mu) \Downarrow v \mid \mu' }{ (\mathbf{for}~ y ~\mathbf{in}~ e \colon~ \vec{\mathrm{stmt}}) \mid \mu \Downarrow v \mid \mu' } \]

\[ \cfrac{ e \mid \mu \Downarrow \mathbf{cons}(v_1, v_2) \qquad \vec{\mathrm{stmt}} \mid (y \mapsto v_1; \mu) \Downarrow \mathbf{stop} \mid \mu' \qquad (\mathbf{for}~ y ~\mathbf{in}~ v_2 \colon~ \vec{\mathrm{stmt}}) \mid \mu' \Downarrow a \mid \mu'' }{ (\mathbf{for}~ y ~\mathbf{in}~ e \colon~ \vec{\mathrm{stmt}}) \mid \mu \Downarrow a \mid \mu'' } \qquad{(a \in \lbrace v, \mathbf{stop} \rbrace)} \]

It assumes the program is properly alpha-converted, i.e. doesntHaveLeakOfLoopCounters. So it leaks loop counters to out of loops.

Rules for \(\mathbf{if}~ e \colon\quad \mathrm{stmt}; \mathrm{stmt}; \dots; \mathrm{stmt};\quad \mathbf{else}\colon\quad \mathrm{stmt}; \mathrm{stmt}; \dots; \mathrm{stmt}\)

\[ \cfrac{ e \mid \mu \Downarrow \mathbf{true} \qquad \vec{\mathrm{stmt}} _ 1 \mid \mu \Downarrow a \mid \mu' }{ (\mathbf{if}~ e \colon~ \vec{\mathrm{stmt}} _ 1 ~\mathbf{else}\colon~ \vec{\mathrm{stmt}} _ 2) \mid \mu \Downarrow a \mid \mu' } \qquad{(a \in \lbrace v, \mathbf{stop} \rbrace)} \]

\[ \cfrac{ e \mid \mu \Downarrow \mathbf{false} \qquad \vec{\mathrm{stmt}} _ 2 \mid \mu \Downarrow a \mid \mu' }{ (\mathbf{if}~ e \colon~ \vec{\mathrm{stmt}} _ 1 ~\mathbf{else}\colon~ \vec{\mathrm{stmt}} _ 2) \mid \mu \Downarrow a \mid \mu' } \qquad{(a \in \lbrace v, \mathbf{stop} \rbrace)} \]

Rules for \(\mathbf{assert}~ e\)

\[ \cfrac{ e \mid \mu \Downarrow \mathbf{true} }{ \mathbf{assert}~ e \mid \mu \Downarrow \mathbf{stop} } \]

\[ \cfrac{ e \mid \mu \Downarrow \mathbf{false} }{ \mathbf{assert}~ e \mid \mu \Downarrow \mathbf{err} } \]

Rules for \(e\)

\[ \cfrac{ e \mid \mu \Downarrow v }{ x.\mathrm{append}(e) \mid \mu \Downarrow \mathbf{stop} \mid (x \mapsto \mathrm{snoc}(\mu(x), v); \mu) } \]

evalStatements evaluates sequences of statements of our restricted Python-like language.

\[ \cfrac{\mathrm{stmt} _ 0 \mid \mu \Downarrow v \mid \mu'}{\mathrm{stmt} _ 0; \mathrm{stmt} _ 1; \dots; \mathrm{stmt} _ {n-1} \mid \mu \Downarrow v \mid \mu'} \]

\[ \cfrac{\mathrm{stmt} _ 0 \mid \mu \Downarrow \mathbf{stop} \mid \mu' \qquad \mathrm{stmt} _ 1; \dots; \mathrm{stmt} _ {n-1} \mid \mu' \Downarrow a \mid \mu''}{\mathrm{stmt} _ 0; \mathrm{stmt} _ 1; \dots; \mathrm{stmt} _ {n-1} \mid \mu \Downarrow a \mid \mu''} \qquad{(a \in \lbrace v, \mathbf{stop} \rbrace)} \]

\[ \epsilon \mid \mu \Downarrow \mathbf{stop} \mid \mu \]