# Demo of the ShotDs Package

```elixir
Mix.install([
  {:shot_ds, "~> 1.3"},
  {:kino, "~> 0.19.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.3"}
  ]
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. This can also be done from a Livebook cell as follows:

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

```elixir
System.put_env("TPTP_ROOT", "/path/to/tptp/root/directory")
```

## 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_var("X", type_iii()) |> Context.put_const("a", type_i())

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

Parsing is also available via [Sigils](https://hexdocs.pm/elixir/sigils.html) for TH0/TH1 formula strings (`~f` to force type $o$, `~g` otherwise), TPTP problems (`~p`) (wiht `thf(...)` tags), types (`~t`), 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)
```

## LaTeX Pretty-Printing

The module `ShotDs.Util.LatexFormatter` renders HOL objects as LaTeX. Types are printed as subscripts; logical constants of the signature ($\top, \bot, \neg, \wedge, \vee, \supset, \equiv, =, \forall, \exists$) print as their standard LaTeX symbols with no type annotation.

Below we define a small helper that returns a `Kino.Markdown` showing both the LaTeX source and its rendered form, so Livebook can typeset the output.

```elixir
alias ShotDs.Util.LatexFormatter, as: LF

show = fn latex ->
  Kino.Markdown.new("`#{latex}`\n\n$$#{latex}$$")
end

# Arrow types are right-associative; the LHS is parenthesised when itself an arrow.
Kino.Layout.grid([
  Type.new(:o, [:i, :i])         |> LF.format!() |> show.(),
  Type.new(:o, Type.new(:o, :i)) |> LF.format!() |> show.()
], columns: 2)
```

Bound variables get freshly reconstructed names drawn from a **type-specific pool** — individuals `X, Y, Z, U, V, W`; propositions and predicates `P, Q, R, S`; relations `R, S, T, U`; functions `F, G, H, K`. All variables are uppercase by TPTP convention; constants are lowercase. Duplicates are disambiguated with a _superscript_ (subscripts are reserved for the type annotation).

Function application uses `~` (LaTeX non-breaking space) to keep a head glued to its arguments, and binders are followed by `\,` (thin space).

```elixir
# Church numeral 2: \f c. f (f c). f is a function i->i, c is an individual.
church2 =
  lambda([type_ii(), type_i()], fn f, c ->
    app(f, app(f, c))
  end)

church2 |> LF.format!() |> show.()
```

Quantifiers merge with their bound abstraction and chain across nested binders, so `∀(λx. ∀(λy. x = y))` collapses into a single line:

```elixir
forall([type_i(), type_i()], fn x, y -> eq(x, y) end)
|> LF.format!()
|> show.()
```

Reconstructed names avoid capture with free variables already appearing in the term. Here the outer name `F` is taken, so the binder picks `G`:

```elixir
f_free = var("F", type_ii())

lambda(type_ii(), fn g -> app(f_free, app(g, const("a", type_i()))) end)
|> LF.format!()
|> show.()
```

Set `reconstruct_names: false` to see the raw de Bruijn structure. Binders render as $\lambda_{\tau}$ (no name) and references use the `\mathtt` font. Quantifier–binder merging is suppressed in this mode so the constructor structure remains visible.

```elixir
church2 |> LF.format!(reconstruct_names: false) |> show.()
```

Other options: `hide_types` drops the subscripts, and `math_mode` wraps the result in `$…$` (`:inline`) or `$$…$$` (`:display`).

```elixir
Kino.Layout.grid([
  church2 |> LF.format!(hide_types: true)    |> show.(),
  church2 |> LF.format!(math_mode: :inline)  |> Kino.Markdown.new()
])
```

Substitutions format as well:

```elixir
alias ShotDs.Data.{Declaration, Substitution}

Substitution.new(
  Declaration.new_free_var("X", type_i()),
  const("a", type_i())
)
|> LF.format!()
|> show.()
```

## 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()
```

```elixir
with {:ok, str} <- ShotDs.Tptp.unparse_problem(problem) do
  IO.puts str
end
```

**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)
pp_x_a = x_a |> LF.format!()

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

pp_b_a = ("(" <> pp_x_a <> ")~" <> LF.format!(s) <> ~S(\Longrightarrow)) <>
  (Semantics.subst!(s, x_a) |> LF.format!())

Kino.Markdown.new("$\n" <> pp_x_a <> "\n$\n\n$\n" <> pp_b_a <> "\n$")
```

**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))
|> LF.format!(math_mode: :inline) |> Kino.Markdown.new()
```

```elixir
import ShotDs.Stt.Booleans

b_and(tt(), b_var("P"))
|> LF.format!(math_mode: :inline) |> Kino.Markdown.new()
```

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