# Options
| `-Oall` | Disabled | Enables all compiler passes |
| `-Ono-all` | Disabled | Disables all compiler passes |
| `-Oeta` `-Ono-eta` | Disabled | [eta-reduction](#eta-reduction) |
| `-Oprune` `-Ono-prune` | Disabled | [definition-pruning](#definition-pruning) |
| `-Olinearize-matches` `-Olinearize-matches-alt` `-Ono-linearize-matches` | Enabled | [linearize-matches](#linearize-matches) |
| `-Ofloat-combinators` `-Ono-float-combinators` | Enabled | [float-combinators](#float-combinators) |
| `-Omerge` `-Ono-merge` | Disabled | [definition-merging](#definition-merging) |
| `-Oinline` `-Ono-inline` | Disabled | [inline](#inline) |
| `-Ocheck-net-size` `-Ono-check-net-size` | Disabled | [check-net-size](#check-net-size) |
| `-Oadt-scott` `-Oadt-num-scott` | adt-num-scott | [adt-encoding](#adt-encoding) |
| `-Otype-check` `-Ono-type-check` | type-check | [type-checking](#type-checking) |
## Eta-reduction
Enables or disables Eta Reduction for defined functions.
Eta reduction simplifies lambda expressions, removing redundant parameters. [See also](https://wiki.haskell.org/Eta_conversion).
Example:
```py
# program
id = λx x
id_id = λx (id x)
# -Oeta
id_id = id
# -Ono-eta
id_id = λz (id z)
```
## Definition-pruning
If enabled, removes all unused definitions.
Example:
```py
# program
Id = λx x
Id2 = Id
Main = (Id 42)
# -Oprune
Id = λx x
Main = (Id 42)
# -Ono-prune
Id = λx x
Id2 = Id
Main = (Id 42)
```
## Definition-merging
If enabled, merges definitions that are identical at the term level.
Example:
```py
# Original program
id = λx x
also_id = λx x
main = (id also_id)
# After definition merging
id_$_also_id = λx x
main = (id also_id)
# -Ono-merge, compilation output
@also_id = (a a)
@id = (a a)
@main = a
& @id ~ (@also_id a)
# -Omerge, compilation output
@a = (a a)
@main = a
& @a ~ (@a a)
```
## linearize-matches
Linearizes the variables between match cases, transforming them into combinators when possible.
```py
# Linearization means going from this
@a @b switch a {
0: (Foo b)
_: (Bar a-1 b)
}
# To this
@a @b (switch a {
0: @b (Foo b)
_: @b (Bar a-1 b)
} b)
```
When the `linearize-matches` option is used, only linearizes variables that would generate an eta-reducible application.
Example:
```py
λa λb switch a { 0: b; _: b }
# Is transformed to
λa switch a { 0: λb b; _: λb b }
# But this stays the same
λa λb switch b { 0: a; _: a }
```
When the `linearize-matches-extra` option is used, it linearizes all variables used in the arms.
example:
```py
λa λb λc switch b { 0: a; _: c }
# Is transformed to (without eta-reducing 'c')
λa λb λc (switch b { 0: λa λc a; _: λa λc c } a c)
```
These automatic linearization passes are done before the manual linearization from `with` and doesn't duplicate manually linearized variables.
```py
# These variables are only linearized once
λa λb λc switch a with b c { 0: (b c); _: (a-1 b c) }
# With -Olinearize-matches becomes
λa λb λc (switch a { 0: λb λc (b c); _: λb λc (a-1 b c) } b c)
# And not
λa λb λc (switch a { 0: λb λc λb λc (b c); _: λb λc λb λc (a-1 b c) } b c b c)
```
## float-combinators
Extracts closed terms to new definitions. See [lazy definitions](lazy-definitions.md#automatic-optimization).
Since HVM-Core is an eager runtime, this pass is enabled by default to prevent infinite expansions.
Example:
```py
True = λt λf λm t
False = λt λf λm f
Maybe = λx λt λf λm (m x)
getVal = λb (b 1 0 (λx (== x 1)))
# `(λx (== x 1))` can be extracted, since there is no free variables.
Cons = λh λt λc λn (c h t)
Nil = λc λn n
fold = λinit λf λxs (xs λh λt (fold (f init h) f t) init)
# Here we need to extract `λh λt (fold (f init h) f t)` to not expand `fold` infinitely, but it will not be extracted because of the free variable `init`.
```
# Inline
If enabled, inlines terms that compile to nullary inet nodes (refs, numbers, erasures).
Example:
```py
# program
foo = 2
id = λx x
main = (id foo)
# -Ono-inline, compilation output
@foo = 2
@id = (a a)
@main = a
& @id ~ (@foo a)
# -Oinline, compilation output
@foo = 2
@id = (a a)
@main = a
& @id ~ (2 a)
```
## Check-net-size
If enabled, checks that the size of each function after compilation has at most 64 HVM nodes.
This is a memory restriction of the CUDA runtime, if you're not using the `*-cu` you can disable it.
Example:
```py
# Without -Ocheck-net-size compiles normally.
# But with -Ocheck-net-size it fails with
# `Definition is too large for hvm`
(Radix n) =
let r = Map_/Used
let r = (Swap (& n 1) r Map_/Free)
let r = (Swap (& n 2) r Map_/Free)
let r = (Swap (& n 4) r Map_/Free)
let r = (Swap (& n 8) r Map_/Free)
let r = (Swap (& n 16) r Map_/Free)
let r = (Swap (& n 32) r Map_/Free)
let r = (Swap (& n 64) r Map_/Free)
let r = (Swap (& n 128) r Map_/Free)
let r = (Swap (& n 256) r Map_/Free)
let r = (Swap (& n 512) r Map_/Free)
let r = (Swap (& n 1024) r Map_/Free)
let r = (Swap (& n 2048) r Map_/Free)
let r = (Swap (& n 4096) r Map_/Free)
let r = (Swap (& n 8192) r Map_/Free)
let r = (Swap (& n 16384) r Map_/Free)
let r = (Swap (& n 32768) r Map_/Free)
let r = (Swap (& n 65536) r Map_/Free)
let r = (Swap (& n 131072) r Map_/Free)
let r = (Swap (& n 262144) r Map_/Free)
let r = (Swap (& n 524288) r Map_/Free)
let r = (Swap (& n 1048576) r Map_/Free)
let r = (Swap (& n 2097152) r Map_/Free)
let r = (Swap (& n 4194304) r Map_/Free)
let r = (Swap (& n 8388608) r Map_/Free)
r
```
## ADT Encoding
Selects the lambda encoding for types defined with `type` and `object`.
`-Oadt-scott` uses Scott encoding.
`-Oadt-num-scott` uses a variation of Scott encoding where instead of one lambda per constructor, we use a numeric tag to indicate which constructor it is. The numeric tag is assigned to the constructors in the order they are defined and each tag is accessible as a definition by `<type>/<ctr>/tag`.
```py
# Generates functions Option/Some and Option/None
type Option:
Some { value }
None
# With -Oadt-scott they become:
Option/Some = λvalue λSome λNone (Some value)
Option/None = λSome λNone (None)
# With -Oadt-num-scott they become:
Option/Some = λvalue λx (x Option/Some/tag value)
Option/None = λx (x Option/None/tag)
# Generated -Oadt-num-scott tags:
Option/Some/tag = 0
Option/None/tag = 1
```
Pattern-matching with `match` and `fold` is generated according to the encoding.
Note: IO is **only** available with `-Oadt-num-scott`.
## Type Checking
Type checking is enabled by default and verifies and enforces the constraints of types. When enabled, verifies the type safety of the program based on the source code. If it passes the check, then the program is guaranteed to satisfy type constraints for all possible inputs.
```py
def main() -> Bool:
return 3
```
With type checking enabled, The following program will throw a type error `Expected function type 'Bool' but found 'u24'`, whereas if it is disabled, it will compile successfully and return `3`.