API Reference shot_ds v#1.0.2

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.

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

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

Utilities for efficiently traversing and transforming Hol term DAGs.

An exception raised when type inference fails.