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
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
Consider using the more expressive API defined in ShotDs.Hol.Dsl ontop of
this module.
Summary
Term Cache
Looks up and returns the concrete ShotDs.Data.Term struct for the given ID.
Looks up and returns the concrete ShotDs.Data.Term struct for the given ID,
erroring out if the ID doesn't exist.
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.
Term Scratchpad
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}.
Commits the term with the given ID (which might be local) to the global ETS table. Returns the new global ID, raising on errors.
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.
Destroys the processes ephemeral ETS table explicitly.
Wraps the given function and executes it with an active scratchpad.
Wraps the given function and executes it with an active scratchpad, propagating errors when they occur.
Term Construction API
Applies the term corresponding to head_id to the list of terms corresponding
to arg_ids.
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.
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.
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.
Applies the term corresponding to left_id to the term corresponding to
right_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.
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().
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().
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().
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().
Creates and memoizes a term representing a single free variable, bound variable or constant. Handles eta-expansion automatically.
Checks whether the term corresponding to the given ID is a primitive term i.e., if it is an eta-expanded constant or variable.
Types
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.
Term Cache
@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.
@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.
@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
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))
trueTerm Scratchpad
@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.
@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.
@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.
@spec stop_scratchpad() :: :ok
Destroys the processes ephemeral ETS table explicitly.
Note
The scratchpad ETS table also dies with the process automatically.
@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.
@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.
Term Construction API
@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.
@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.
@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
Consider using ShotDs.Hol.Dsl.lambda/2 instead as it is more expressive
and robust.
@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
Consider using ShotDs.Hol.Dsl.lambda/2 instead as it is more expressive
and robust.
@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
Consider using ShotDs.Hol.Dsl.app/2 instead as it is more expressive and
robust.
@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
Consider using ShotDs.Hol.Dsl.app/2 instead as it is more expressive and
robust.
@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().
@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().
@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().
@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
Consider wrapping functions using this to create temporary free variables
with with_scratchpad/1 or with_scratchpad!/1 for garbage collection.
@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)@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.
Types
@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.