Modules
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, 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.
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.
Robinson first-order unification for the rank-1 HM type system.
An exception raised when type inference fails.