API Reference shot_ds v#1.0.5

This module collects the most important functions from the library. These include parsing functions as well as simple term construction.

Represents a type environment for parsing and type checking. Can also be created by using the ~e sigil from ShotDs.Hol.Sigils.

Represents free and bound variables as well as constants.

A data structure to describe a (TPTP) proof problem.

Represents a substitution.

Represents a Hol term as directed acyclic graph (DAG).

Provides a data structure for Church's simple types (monotypes).

Represents a rank-1 polymorphic type scheme

Provides definitions for common HOL types, terms and constants.

Introduces a domain specific language (DSL) for constructing HOL terms.

Contains various macros for pattern matching on HOL terms.

Provides custom Elixir sigils for inline simple type, TH0 formula parsing, TPTP problem file parsing, context parsing and a wrapper for handling context.

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.

An exception raised when parsing fails.

Church's encoding of Booleans in simple type theory (STT).

Encodes Church numerals in simple type theory.

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.

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

Contains utility to parse files from the TPTP problem library (https://tptp.org/TPTP/) as well as custom files in TPTP's TH0 syntax.

Contains functionality for formatting terms, variable names etc.

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.

Utilities for efficiently traversing and transforming Hol term DAGs.

An exception raised when type inference fails.