# Options

| flag                                                                     | Default       | What it does?                             |
| ------------------------------------------------------------------------ | ------------- | ----------------------------------------- |
| `-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)             |

## 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`.