# shot_ds v1.0.0 - Table of Contents

Data structures for various HOL objects and TH0 parser.

## Pages

- [ShotDs](readme.md)
- [Demo of the ShotDs Package](demo.md)

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

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

  - [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 TH0 syntax or a TPTP TH0 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.

- 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 TH0 syntax with full type
inference. The algorithm is similar to Hindley-Milner type systems but for
simplicity reasons without the optimizations found in algorithms J or W.
Uses Robinson's first-order unification algorithm for type inference. A
context can be specified to clear up unknown types. If terms still have
unknown type after parsing, unifies 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.