# Demo of the ShotDs Package

```elixir
Mix.install([
  {:shot_ds, "~> 1.0"}
])
```

## Installation and Setup

This package can be installed by adding `shot_ds` to your list of dependencies
in `mix.exs`:

<!-- livebook:{"force_markdown":true} -->

```elixir
def deps do
  [
    {:shot_ds, "~> 1.0"}
  ]
end
```

__Note__: When parsing files from the TPTP problem library, it is additionally necessary to set up an environment variable `TPTP_ROOT` pointing to its root directory. This also enables parsing dependencies in TPTP files.

## Core Concepts and Architecture

This library models various data structures from classical higher-order logic (HOL) and simple type theory (STT). It relies on (but is not limited to) the two base types $o$ for booleans and $\iota$ for individuals. Internally, types are represented as a struct composed of a goal type and a list of argument types:

```elixir
alias ShotDs.Data.Type

Type.new(:i) |> IO.inspect(label: "type i")
Type.new(:o, [:i, :o]) |> IO.inspect(label: "type i->o->o")
:ok
```

Terms are stored as Elixir structs acting as directed acyclic graphs (DAGs). They are assigned a (concurrency-safe) ID which is processed by the `ShotDs.Stt.TermFactory` module. These IDs are used for a caching mechanism using the Erlang term storage (ETS) under the hood. Notice that terms are represented in $\beta\eta$-normal form and use de Bruijn indices.

```elixir
alias ShotDs.Stt.TermFactory, as: TF
import ShotDs.Util.Formatter # pretty-printing

x_id = TF.make_free_var_term("X", Type.new(:i, [:i, :o])) |> IO.inspect(label: "assigned ID")
TF.get_term!(x_id) |> IO.inspect(label: "generated term")
format!(x_id, _hide_types=false) |> IO.inspect(label: "pretty-printed")
:ok
```

## Term Construction with the DSL

The module `ShotDs.Hol.Dsl` introduces a domain-specific language for shorthand term construction. It utilizes the unused Elixir operators `&&&`, `|||`, `~>` and `<~>` as infix-constructors. Together with the module `ShotDs.Hol.Definitions`, we can build the XOR operator as follows:

```elixir
import ShotDs.Hol.Definitions
import ShotDs.Hol.Dsl

exclusive_or = lambda([type_o(), type_o()], fn p, q ->
  (p ||| q) &&& neg(p &&& q)
end)

format!(exclusive_or) |> IO.puts()
```

## Parsing TH0 Strings

The module `ShotDs.Parser` offers powerful parsing capabilities with full type inference for inputs in TPTP (TH0) format:

```elixir
alias ShotDs.Parser

Parser.parse!("?[X : $o]: X => $true")
|> format!() |> IO.puts()
```

Note that the type inference engine assumes type $o$ for the outermost type unless inferable otherwise. Other unknown types are treated as _type variables_ and are assigned a unique ID:

```elixir
Parser.parse!("X @ a")
|> format!(_hide_types = false) |> IO.puts()
```

To clear up ambiguities, we can pass in a _type environment_:

```elixir
alias ShotDs.Data.Context

ctx = Context.new() |> Context.put_const("a", type_i())

Parser.parse!("X @ a", ctx)
|> format!() |> IO.puts()
```

Parsing is also available via [Sigils](https://hexdocs.pm/elixir/sigils.html) for TH0 formula strings (`~f`), TPTP problems (`~p`) (wiht `thf(...)` tags) and type environments (`~e`), including a wrapper for providing context:

```elixir
import ShotDs.Hol.Sigils

~f(?[X : $o]: X => $true) |> format!() |> IO.puts()

with_context(~e[X : $o, p : $o>$i], fn ->
  ~f(p @ X) |> format!(false) |> IO.puts()
end)
```

## Advanced Utilities

__Error Handling__: Functions that can fail return a tuple `{:ok, result}` or `{:error, reason}` per default. There are "bang" versions (suffixed by `!`) of all functions that either return the result directly or raise an error. [`with`-clauses](https://hexdocs.pm/elixir/Kernel.SpecialForms.html#with/1) offer idiomatic error handling when processing user input and are generally preferred over exceptions:

```elixir
with {:ok, term_id} <- Parser.parse("a & b"),
     {:ok, formatted} <- format(term_id) do
  IO.puts(formatted)
else
  {:error, msg} -> IO.puts("ERROR: #{msg}")
end

with {:ok, term_id} <- Parser.parse("a &"),
     {:ok, formatted} <- format(term_id) do
  IO.puts(formatted)
else
  {:error, msg} -> IO.puts("ERROR: #{msg}")
end

try do
  Parser.parse!("a &")
rescue
  e in Parser.ParseError ->
    IO.puts(~s'Rescued Parser.ParseError with message: "#{e.message}"')
end
```

__File Parsing__: `ShotDs.Tptp` includes parsing capabilities for TPTP files. The collected information is aggregated in a `ShotDs.Data.Problem` struct.

```elixir
problem = ~p"""
thf(e_type,type,
    e: $tType).

thf(p_type,type,
    p: e>$o).

thf(lma,lemma,
    ![X : e]: p @ X).

thf(conj,conjecture,
    ?[Y : e]: p @ Y).
"""

IO.inspect(problem)

format!(problem) |> IO.puts()
```

__Term Manipulation__: Various functions regarding the semantics of STT, e.g. substitutions, are handled by the `ShotDs.Stt.Semantics` module.

```elixir
alias ShotDs.Data.Substitution
alias ShotDs.Stt.Semantics

x = var("X", type_ii())
a = const("a", type_i())
b = const("b", type_ii())

x_a = app(x, a)
x_a |> format!(true) |> IO.puts()

s = %Substitution{fvar: TF.get_term!(x).head, term_id: b}

Semantics.subst!(s, x_a) |> format!(true) |> IO.puts()
```

__Church Encoding__: `ShotDs.Stt.Numerals` provides an implementation of Church's encoding of natural numbers, adapted to simple types. This can for example be used for benchmarking. Additionally, Church's encoding of Booleans is implemented in the module `ShotDs.Stt.Booleans`.

```elixir
import ShotDs.Stt.Numerals

plus(num(5), num(2)) |> format!() |> IO.puts()
```

```elixir
import ShotDs.Stt.Booleans

b_and(tt(), b_var("P")) |> format!() |> IO.puts()
```

__Traversals and Transformation__: Transformations of terms mostly follow the same scheme. An optimized adaption of the combinators `fold` (`fold_term/2`, `fold_term!/2`) and `map` (`map_term/5`, `map_term!/5`) to the DAG representation of terms is implemented in the module `ShotDs.Util.TermTraversal`. Examples for the usage of these higher-order functions can be found in the source code of the `ShotDs.Stt.Semantics` module or in `ShotDs.Util.Formatter.format_term/2`.

<!-- livebook:{"break_markdown":true} -->

__Pattern Matching__: `ShotDs.Hol.Patterns` provides macro definitions for pattern matching on various HOL terms.

```elixir
use ShotDs.Hol.Patterns

case TF.get_term!(true_term() ||| false_term()) do
  disjunction(p, q) -> IO.puts("Disjunction of #{format!(p)} and #{format!(q)}")
  _ -> IO.puts("No match")
end
```

__Garbage Collection__: Wrapping code with `ShotDs.Stt.TermFactory.with_scratchpad/1` ensures temporary terms created by that code to be garbage collected afterwards. In this process, terms are written to a local ETS table and only the final result is (recursively) committed to the global table.