# `ShotDs.Stt.TermFactory`
[🔗](https://github.com/jcschuster/ShotDs/blob/v1.0.0/lib/shot_ds/stt/term_factory.ex#L1)

Contains functionality of creating, memoizing and accessing terms using an
ETS cache.

In HOL, terms often share sub-expressions, meaning they form Directed Acyclic
Graphs (DAGs) rather than simple abstract syntax trees (ASTs). Hence,
representing terms as nested sturctures has the big disadvantage of needing
to store the same sub-expression multiple times in memory. ETS, the Erlang
term storage offers an efficient caching mechanism which we can utilize to
ensure that a specific term is created exactly once. Furthermore, Elixir's
immutability ensures pointers to the terms being static, i.e., a term can not
be altered once it is memoized.

> #### Error Handling {: .info}
>
> All functions that can fail return a tuple `{:ok, result}` or
> `{:error, reason}` per default to facilitate error handling. These functions
> also come in a "bang" variant (with an "!") that raises errors instead of
> propagating that. This behavior can be useful for quick prototyping or when
> it is guaranteed that the function calls will succeed.

> #### Note {: .neutral}
>
> Consider using the more expressive API defined in `ShotDs.Hol.Dsl` ontop of
> this module.

# `get_term`

```elixir
@spec get_term(ShotDs.Data.Term.term_id()) ::
  {:ok, ShotDs.Data.Term.t()} | lookup_error_t()
```

Looks up and returns the concrete `ShotDs.Data.Term` struct for the given ID.

Routes to global or local ETS table based on the sign of the ID.

# `get_term!`

```elixir
@spec get_term!(ShotDs.Data.Term.term_id()) :: ShotDs.Data.Term.t()
```

Looks up and returns the concrete `ShotDs.Data.Term` struct for the given ID,
erroring out if the ID doesn't exist.

Routes to global or local ETS table based on the sign of the ID.

# `memoize`

```elixir
@spec memoize(ShotDs.Data.Term.t()) ::
  ShotDs.Data.Term.global_term_id() | ShotDs.Data.Term.local_term_id()
```

Memoizes the given term in the module's `:ets` table. Terms will be
identified if they share the same *signature*, e.g., all fields but `id`.

Returns the looked up or generated ID of the term. IDs are generated as
integers in a concurrency-safe way. Local IDs are represented by negative,
global ones by positive integers.

> #### Note {: .info}
>
> If a scratchpad is active, the term is written to the local ETS table.
> Otherwise, it writes globally.

## Example:

    iex> id = memoize(t)
    iex> match?({:ok, %{^t | id: ^id}}, get_term(id))
    true

# `commit_to_global`

```elixir
@spec commit_to_global(
  ShotDs.Data.Term.local_term_id()
  | ShotDs.Data.Term.global_term_id()
) ::
  {:ok, ShotDs.Data.Term.global_term_id()} | {:error, term()}
```

Commits the term with the given ID (which might be local) to the global ETS
table. Returns a tuple `{:ok, new_global_id}` or `{:error, reason}`.

Also ensures recursively that the arguments are memoized.

# `commit_to_global!`

```elixir
@spec commit_to_global!(
  ShotDs.Data.Term.local_term_id()
  | ShotDs.Data.Term.global_term_id()
) ::
  ShotDs.Data.Term.global_term_id()
```

Commits the term with the given ID (which might be local) to the global ETS
table. Returns the new global ID, raising on errors.

Also ensures recursively that the arguments are memoized.

# `start_scratchpad`

```elixir
@spec start_scratchpad() :: :ok
```

Creates a local "scratchpad" ETS table for the current process. Can be used to
cleanup temporary free variable terms e.g., when creating abstraction terms.

Puts the reference to the ETS table in the processes memory under the
`:term_scratchpad` key.

# `stop_scratchpad`

```elixir
@spec stop_scratchpad() :: :ok
```

Destroys the processes ephemeral ETS table explicitly.

> #### Note {: .info}
>
> The scratchpad ETS table also dies with the process automatically.

# `with_scratchpad`

```elixir
@spec with_scratchpad((-> {:ok, ShotDs.Data.Term.term_id()} | {:error, t})) ::
  {:ok, ShotDs.Data.Term.term_id()} | {:error, t}
when t: term()
```

Wraps the given function and executes it with an active scratchpad.

Commits the final result to the global ETS table Cleans up the scratchpad
afterwards if it didn't exist previously. Acts as a concurrency-safe garbage
collector.

# `with_scratchpad!`

```elixir
@spec with_scratchpad!((-> ShotDs.Data.Term.term_id())) :: ShotDs.Data.Term.term_id()
```

Wraps the given function and executes it with an active scratchpad,
propagating errors when they occur.

Commits the final result to the global ETS table Cleans up the scratchpad
afterwards if it didn't exist previously. Acts as a concurrency-safe garbage
collector.

# `fold_apply`

```elixir
@spec fold_apply(ShotDs.Data.Term.term_id(), [ShotDs.Data.Term.term_id()]) ::
  {:ok, ShotDs.Data.Term.term_id()} | lookup_error_t()
```

Applies the term corresponding to `head_id` to the list of terms corresponding
to `arg_ids`.

# `fold_apply!`

```elixir
@spec fold_apply!(ShotDs.Data.Term.term_id(), [ShotDs.Data.Term.term_id()]) ::
  ShotDs.Data.Term.term_id()
```

Applies the term corresponding to `head_id` to the list of terms corresponding
to `arg_ids`, folding left to right, erroring out if one of the terms does not
exist.

# `make_abstr_term`

```elixir
@spec make_abstr_term(
  ShotDs.Data.Term.term_id(),
  ShotDs.Data.Declaration.t() | ShotDs.Data.Term.term_id()
) ::
  {:ok, ShotDs.Data.Term.term_id()}
  | lookup_error_t()
  | {:error, :var_term_not_primitive}
```

Abstracts the term corresponding to the given id over the given variable. If
the variable is already bound, adds it to the list of bound variables.

> #### Note {: .info}
>
> Consider using `ShotDs.Hol.Dsl.lambda/2` instead as it is more expressive
> and robust.

# `make_abstr_term!`

```elixir
@spec make_abstr_term!(
  ShotDs.Data.Term.term_id(),
  ShotDs.Data.Declaration.t() | ShotDs.Data.Term.term_id()
) :: ShotDs.Data.Term.term_id()
```

Abstracts the term corresponding to the given id over the given variable (or
variable term), erroring out if either term does not exist or the given
variable term is not primitive. If the variable is already bound, adds it to
the list of bound variables.

> #### Note {: .info}
>
> Consider using `ShotDs.Hol.Dsl.lambda/2` instead as it is more expressive
> and robust.

# `make_appl_term`

```elixir
@spec make_appl_term(ShotDs.Data.Term.term_id(), ShotDs.Data.Term.term_id()) ::
  {:ok, ShotDs.Data.Term.term_id()}
  | lookup_error_t()
  | {:error, :incompatible_types}
```

Applies the term corresponding to `left_id` to the term corresponding to
`right_id`.

> #### Note {: .info}
>
> Consider using `ShotDs.Hol.Dsl.app/2` instead as it is more expressive and
> robust.

# `make_appl_term!`

```elixir
@spec make_appl_term!(ShotDs.Data.Term.term_id(), ShotDs.Data.Term.term_id()) ::
  ShotDs.Data.Term.term_id()
```

Applies the term corresponding to `left_id` to the term corresponding to
`right_id`, erroring out if either term does not exist or their types are
incompatible.

> #### Note {: .info}
>
> Consider using `ShotDs.Hol.Dsl.app/2` instead as it is more expressive and
> robust.

# `make_const_term`

```elixir
@spec make_const_term(String.t() | reference(), ShotDs.Data.Type.t()) ::
  ShotDs.Data.Term.term_id()
```

Creates a constant with the corresponding name and type and returns the ID
for its term representation. Short for
`ShotDs.Data.Declaration.new_const(name, type) |> make_term()`.

# `make_free_var_term`

```elixir
@spec make_free_var_term(String.t() | reference(), ShotDs.Data.Type.t()) ::
  ShotDs.Data.Term.term_id()
```

Creates a free variable with the corresponding name and type and returns the
ID for its term representation. Short for
`ShotDs.Data.Declaration.new_free_var(name, type) |> make_term()`.

# `make_fresh_const_term`

```elixir
@spec make_fresh_const_term(ShotDs.Data.Type.t()) :: ShotDs.Data.Term.term_id()
```

Creates a fresh constant of the given type and returns the ID for its term
representation. Short for
`ShotDs.Data.Declaration.fresh_const(type) |> make_term()`.

# `make_fresh_var_term`

```elixir
@spec make_fresh_var_term(ShotDs.Data.Type.t()) :: ShotDs.Data.Term.term_id()
```

Creates a fresh variable of the given type and returns the ID for its term
representation. Short for
`ShotDs.Data.Declaration.fresh_var(type) |> make_term()`.

> #### Note {: .info}
>
> Consider wrapping functions using this to create temporary free variables
> with `with_scratchpad/1` or `with_scratchpad!/1` for garbage collection.

# `make_term`

```elixir
@spec make_term(ShotDs.Data.Declaration.t()) :: ShotDs.Data.Term.term_id()
```

Creates and memoizes a term representing a single free variable, bound
variable or constant. Handles eta-expansion automatically.

Returns a local ID if a scratchpad is active in the caller's process.

## Example:

    iex> co = ShotDs.Data.Declaration.fresh_const(Type.new(:o))
    iex> id = make_term(co)

# `primitive_term?`

```elixir
@spec primitive_term?(ShotDs.Data.Term.term_id()) ::
  {:ok, boolean()} | lookup_error_t()
```

Checks whether the term corresponding to the given ID is a _primitive term_
i.e., if it is an eta-expanded constant or variable.

# `lookup_error_t`

```elixir
@type lookup_error_t() ::
  {:error, :invalid_id}
  | {:error, :non_existing_id}
  | {:error, :scratchpad_missing}
```

There are two error scenarios when looking up a term via its ID. The ID might
not correspond to `ShotDs.Data.Term.global_term_id()` or
`ShotDs.Data.Term.local_term_id()`. If it does, it may not be pointing to any
term. Lastly, the ID can be a _local_ ID, i.e., points to a sketchpad, but no
sketchpad may be active for the current process.

---

*Consult [api-reference.md](api-reference.md) for complete listing*