# Environment Model
The environment model, like the [substitution model][subst], is a way of
thinking about how OCaml programs evaluate. It uses a *big-step
semantics* that describes how an expression *evaluated* down to a
*value*.
[subst]: ../17-subst-model/core-ocaml.html
## Notation
- `` is a *machine configuration*. The machine's environment is `env`
and the code remaining to be evaluated is `e`.
- ` ==> v` means "`e` evaluates or big-steps 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`.
## Syntax
```
e ::= x | e1 e2 | fun x -> e
| n | b | e1 + e2
| (e1,e2) | fst e1 | snd e2
| Left e | Right e
| match e with Left x1 -> e1 | Right x2 -> e2
| if e1 then e2 else e3
| let x = e1 in e2
```
Operator `+` may be any primitive binary operator, such
as addition, multiplication, equality, or less than.
## Semantics
```
==> v
if env(x) = v
==> v'
if ==> (|fun x -> e, newenv|)
and ==> v
and v],e> ==> v'
e> ==> (|fun x -> e, env|)
==> n
==> b
==> 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 ==> true
and ==> v2
==> v3
if ==> false
and ==> v3
==> v2
if ==> v1
and v1],e2> ==> v2
```