Handles the ~e sigil for parsing type environment (context).

Returns a ShotDs.Data.Context struct, raising on errors.

Example:

iex> ~e[X : $i, p: $i>$o]
%ShotDs.Data.Context{
  vars: %{"X" => %ShotDs.Data.Type{goal: :i, args: []}},
  consts: %{
    "p" => %ShotDs.Data.Type{
      goal: :o,
      args: [%ShotDs.Data.Type{goal: :i, args: []}]
    }
  },
  constraints: MapSet.new([])
}

@spec sigil_f(String.t(), [char()]) :: ShotDs.Data.Term.term_id()

Handles the ~f sigil for parsing TH0 formulas.

Returns the assigned global or local term ID. Raises a ShotDs.Parser.ParseError if the syntax is invalid.

Example:

iex> ~f(P => P | Q) |> ShotDs.Util.Formatter.format()
{:ok, "P ⊃ (P ∨ Q)"}

Handles the ~p sigil for parsing TPTP strings describing a TPTP proof problem with thf(...) components.

Returns a ShotDs.Data.Problem struct describing the proof problem, raising on errors.

Example:

iex> ~p"""
...> thf(my_conj,conjecture,
...>     $false => $true).
...> """

@spec sigil_t(String.t(), [char()]) :: ShotDs.Data.Type.t()

Handles the ~t sigil for parsing types in TPTP syntax.

Returns the parsed ShotDs.Data.Type struct. Raises a ShotDs.Parser.ParseError if the syntax is invalid.

Example:

iex> ~t"($i>e)>$o"
%ShotDs.Data.Type{
  goal: :o,
  args: [
    %ShotDs.Data.Type{goal: :e, args: [%ShotDs.Data.Type{goal: :i, args: []}]}
  ]
}

@spec with_context(ShotDs.Data.Context.t(), (-> res)) :: res when res: any()

Provides a wrapper for the ~f sigil to consider some type environment.

Example:

iex> term_id = with_context(~e[p: $i>$o], fn -> ~f(p @ X) end)