ShotDs.Hol.Dsl (shot_ds v1.0.0)

Copy Markdown View Source

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

The DSL utilizes unused Elixir operators with the following precedence:

  (Highest)    ~>, <~>    [Implication, Equivalence]
               &&&        [Conjunction]
  (Lowest)     |||        [Disjunction]

Note

All operators are left-associative, so a ~> b ~> c parses as (a ~> b) ~> c.

Warning

The operator &&& and ||| will clash with the operators defined in the Bitwise module. Consider hiding these definitions when importing Bitwise.

Summary

Primitive

const(name, type)

Primitive term representing a constant symbol of the given type.

var(name, type)

Primitive term representing a variable symbol of the given type.

Unary

neg(a)

Logical Negation

Binary (infix)

a &&& b

Logical Conjunction

a <~> b

Logical Equivalence

a ||| b

Logical Disjunction

a ~> b

Logical Implication

Binary (prefix)

eq(a, b)

Logical Equality.

neq(a, b)

Logical Inequality.

Application

app(head_id, arg_ids)

Applies a term to a single argument term or list of argument terms.

Binders

exists(var_types, body_fn)

Existential quantification. Supports single or multiple variables.

forall(var_types, body_fn)

Universal quantification. Supports single or multiple variables.

lambda(var_types, body_fn)

Constructs a lambda abstraction over a list of variable types.

Primitive

const(name, type)

Primitive term representing a constant symbol of the given type.

var(name, type)

Primitive term representing a variable symbol of the given type.

Unary

neg(a)

@spec neg(ShotDs.Data.Term.term_id()) :: ShotDs.Data.Term.term_id()

Logical Negation

Binary (infix)

a &&& b

@spec ShotDs.Data.Term.term_id() &&& ShotDs.Data.Term.term_id() ::
  ShotDs.Data.Term.term_id()

Logical Conjunction

a <~> b

@spec ShotDs.Data.Term.term_id() <~> ShotDs.Data.Term.term_id() ::
  ShotDs.Data.Term.term_id()

Logical Equivalence

a ||| b

@spec ShotDs.Data.Term.term_id() ||| ShotDs.Data.Term.term_id() ::
  ShotDs.Data.Term.term_id()

Logical Disjunction

a ~> b

@spec ShotDs.Data.Term.term_id() ~> ShotDs.Data.Term.term_id() ::
  ShotDs.Data.Term.term_id()

Logical Implication

Binary (prefix)

eq(a, b)

@spec eq(ShotDs.Data.Term.term_id(), ShotDs.Data.Term.term_id()) ::
  ShotDs.Data.Term.term_id()

Logical Equality.

Automatically infers the Hol type by inspecting the left argument's term in the ETS cache.

neq(a, b)

@spec neq(ShotDs.Data.Term.term_id(), ShotDs.Data.Term.term_id()) ::
  ShotDs.Data.Term.term_id()

Logical Inequality.

Automatically infers the Hol type by inspecting the left argument's term in the ETS cache.

Application

app(head_id, arg_ids)

@spec app(
  ShotDs.Data.Term.term_id(),
  [ShotDs.Data.Term.term_id()] | ShotDs.Data.Term.term_id()
) ::
  ShotDs.Data.Term.term_id()

Applies a term to a single argument term or list of argument terms.

Temporary fresh free variables will be generated corresponding to the types. Passes the generated variable term IDs to the provided body_fn. The arity of body_fn must correspond to the number of given variables.

Binders

exists(var_types, body_fn)

@spec exists([ShotDs.Data.Type.t()] | ShotDs.Data.Type.t(), (... ->
                                                         ShotDs.Data.Term.term_id())) ::
  ShotDs.Data.Term.term_id()

Existential quantification. Supports single or multiple variables.

Temporary fresh free variables will be generated corresponding to the types. Passes the generated variable term IDs to the provided body_fn. The arity of body_fn must correspond to the number of given variables.

Examples

iex> exists(Type.new(:i), fn x -> ... end)

iex> exists([Type.new(:o, [:o, :o]), Type.new(:o), Type.new(:o)], fn r, x, y -> ... end)

forall(var_types, body_fn)

@spec forall([ShotDs.Data.Type.t()] | ShotDs.Data.Type.t(), (... ->
                                                         ShotDs.Data.Term.term_id())) ::
  ShotDs.Data.Term.term_id()

Universal quantification. Supports single or multiple variables.

Examples

iex> forall(Type.new(:i), fn x -> ... end)

iex> forall([Type.new(:o, [:o, :o]), Type.new(:o), Type.new(:o)], fn r, x, y -> ... end)

lambda(var_types, body_fn)

@spec lambda([ShotDs.Data.Type.t()] | ShotDs.Data.Type.t(), (... ->
                                                         ShotDs.Data.Term.term_id())) ::
  ShotDs.Data.Term.term_id()

Constructs a lambda abstraction over a list of variable types.

Temporary fresh free variables will be generated corresponding to the types. Passes the generated variable term IDs to the provided body_fn. The arity of body_fn must correspond to the number of given variables.

Examples:

iex> lambda(Type.new(:i), fn x -> ... end)

iex> lambda([Type.new(:o), Type.new(:o), Type.new(:o)], fn x, y, z -> ... end)