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

Returns a ShotDs.Data.Context struct, raising on errors. Constants are stored as type schemes (see ShotDs.Data.TypeScheme); a bare monotype declaration like p: $i>$o is recorded as a trivial scheme with no quantified variables.

Example:

iex> ~e[X : $i, p: $i>$o]
%ShotDs.Data.Context{
  vars: %{"X" => %ShotDs.Data.Type{goal: :i, args: []}},
  consts: %{
    "p" => %ShotDs.Data.TypeScheme{
      body: %ShotDs.Data.Type{
        goal: :o,
        args: [%ShotDs.Data.Type{goal: :i, args: []}]
      },
      vars: []
    }
  }
}

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

Handles the ~f sigil for parsing THF formulas. If the term's type is polymorphic, instantiates this outer polytype with type o.

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

Example:

iex> ~f<P @ X> |> ShotDs.Util.Formatter.format!(false)
"(P_T[XRRVQ]>o X_T[XRRVQ])_o"

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

Handles the ~g sigil for parsing THF formulas. Keeps outer type variables polymorphic.

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

Example:

iex> ~g<P @ X> |> ShotDs.Util.Formatter.format!(false)
"(P_T[201F47]>T[1XMEC7] X_T[201F47])_T[1XMEC7]"

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 parsing to consider some type environment.

Example:

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