This document contains the evaluation rules for the big-step environment model
evaluation of a core subset of OCaml. The small-step substitution model
evaluation rules for the same core subset are given
[here](../13-semantics/core-ocaml.html).
Notation
--------
- ` ==> v` means "`e` evaluates to `v` in environment `env`"
- `{fun x -> e | env}` denotes a closure with environment `env`.
- `[x1->v1, x2->v2, ...]` denotes the environment with `x1` bound to `v1`, `x2`
bound to `v2` and so on.
- `env[x->v]` denotes the environment `env` extended with a
binding from `x` to `v`. If `env` already has a binding for
`x` then it is replaced.
- `env(x)` denotes the value associated with `x` in `env`.
- we use `+` in the semantics to stand in for any basic arithmetic operation
like `+`, `*`, `<`, etc.
Syntax
------
```
e ::= x | e1 e2 | fun x -> e
| n | e1 + e2
| (e1,e2) | fst e1 | snd e2
| Left e | Right e
| match e with Left x1 -> e1 | Right x2 -> e2
| let x = e1 in e2
```
Semantics
---------
```
==> v
if env(x) = v
==> v'
if ==> {fun x -> e | newenv}
and ==> v
and v],e> ==> v'
e> ==> {fun x -> e | env}
==> n
==> n
if ==> n1
and ==> n2
and n is the result of applying the primitive operation + to n1 and n2
==> (v1,v2)
if ==> v1
and ==> v2
==> v1
if ==> (v1,v2)
==> v2
if ==> (v1,v2)
==> Left v
if ==> v
==> Right v
if ==> v
e1 | Right x2 -> e2> ==> v1
if ==> Left v
and v], e1> ==> v1
e1 | Right x2 -> e2> ==> v2
if ==> Right v
and v], e2> ==> v2
==> v2
if ==> v1
and v1],e2> ==> v2
```