# shot_ds v1.1.1 - API Reference

## Modules

- [ShotDs](ShotDs.md): This module collects the most important functions from the library. These
include parsing functions as well as simple term construction.

- Core Data Structures
  - [ShotDs.Data.Declaration](ShotDs.Data.Declaration.md): Represents free and bound variables as well as constants.

  - [ShotDs.Data.Substitution](ShotDs.Data.Substitution.md): Represents a substitution.

  - [ShotDs.Data.Term](ShotDs.Data.Term.md): Represents a Hol term as directed acyclic graph (DAG).
  - [ShotDs.Data.Type](ShotDs.Data.Type.md): Provides a data structure for Church's simple types (monotypes).
  - [ShotDs.Data.TypeScheme](ShotDs.Data.TypeScheme.md): Represents a rank-1 polymorphic type scheme

- Data Structures for Parsing
  - [ShotDs.Data.Context](ShotDs.Data.Context.md): Represents a type environment for parsing and type checking. Can also be
created by using the `~e` sigil from `ShotDs.Hol.Sigils`.
  - [ShotDs.Data.Problem](ShotDs.Data.Problem.md): A data structure to describe a (TPTP) proof problem.

- Simple Type Theory
  - [ShotDs.Stt.Booleans](ShotDs.Stt.Booleans.md): Church's encoding of Booleans in simple type theory (STT).
  - [ShotDs.Stt.Numerals](ShotDs.Stt.Numerals.md): Encodes Church numerals in simple type theory.
  - [ShotDs.Stt.Semantics](ShotDs.Stt.Semantics.md): Implements the semantics of Church's simple type theory. The most important
functions are `subst/2` and `subst!/2`, which apply substitutions to a given
term, and `unfold_defs/2` and `unfold_defs!/2`, which unfold (possibly
polymorphic) constant definitions while instantiating their type variables
according to each occurrence's monotype.

  - [ShotDs.Stt.TermFactory](ShotDs.Stt.TermFactory.md): Contains functionality of creating, memoizing and accessing terms using an
ETS cache.

- Higher-Order Logic
  - [ShotDs.Hol.Definitions](ShotDs.Hol.Definitions.md): Provides definitions for common HOL types, terms and constants.
  - [ShotDs.Hol.Dsl](ShotDs.Hol.Dsl.md): Introduces a domain specific language (DSL) for constructing HOL terms.
  - [ShotDs.Hol.Patterns](ShotDs.Hol.Patterns.md): Contains various macros for pattern matching on HOL terms.

- Utilities
  - [ShotDs.Util.Formatter](ShotDs.Util.Formatter.md): Contains functionality for formatting terms, variable names etc.

  - [ShotDs.Util.Lexer](ShotDs.Util.Lexer.md): Contains a `tokenize/1` function for tokenizing a string representing a
formula in THF syntax or a TPTP TH0/TH1 problem file using `NimbleParsec`.
This is mainly used as a preprocessing step for parsing. For information about
the returned structure, see
https://hexdocs.pm/nimble_parsec/NimbleParsec.html.
  - [ShotDs.Util.TermTraversal](ShotDs.Util.TermTraversal.md): Utilities for efficiently traversing and transforming Hol term DAGs.

  - [ShotDs.Util.TypeInference](ShotDs.Util.TypeInference.md): Robinson first-order unification for the rank-1 HM type system.

- Parsing
  - [ShotDs.Hol.Sigils](ShotDs.Hol.Sigils.md): Provides custom [Elixir sigils](`e:elixir:sigils.html`) for inline simple
type, TH0 formula parsing, TPTP problem file parsing, context parsing and a
wrapper for handling context.
  - [ShotDs.Parser](ShotDs.Parser.md): Contains functionality to parse a formula in THF syntax with full type
inference. The algorithm uses Hindley-Milner rank-1 polymorphism and
implements algorithm W for type inference. The resulting constraints are
resolved via Robinson's first-order unification algorithm. A context can be
specified to clear up unknown types. If terms still have unknown/polymorphic
type after parsing, it can be specified to unify their type with type o. The
main entry point is the `parse/2` function.
  - [ShotDs.Tptp](ShotDs.Tptp.md): Contains utility to parse files from the TPTP problem library
(https://tptp.org/TPTP/) as well as custom files in TPTP's TH0 syntax.

- Exceptions
  - [ShotDs.Parser.ParseError](ShotDs.Parser.ParseError.md): An exception raised when parsing fails.

  - [ShotDs.Util.TypeInference.TypeError](ShotDs.Util.TypeInference.TypeError.md): An exception raised when type inference fails.