# `ShotDs.Hol.Sigils`
[🔗](https://github.com/jcschuster/ShotDs/blob/v1.0.0/lib/shot_ds/hol/sigils.ex#L1)

Provides custom [Elixir sigils](`e:elixir:sigils.html`) for inline simple
type, TH0 formula parsing, TPTP problem file parsing, context parsing and a
wrapper for handling context.

> #### Note {: .info}
>
> Sigils support 8 different delimiters: `//`, `||`, `""`, `''`, `()`, `[]`,
> `{}`, `<>`. It is also possible to escape (lowercase) sigils, e.g., for
> injecting strings.

# `sigil_e`

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([])
    }

# `sigil_f`

```elixir
@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)"}

# `sigil_p`

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:

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

# `sigil_t`

```elixir
@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: []}]}
      ]
    }

# `with_context`

```elixir
@spec with_context(ShotDs.Data.Context.t(), (-&gt; 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)

---

*Consult [api-reference.md](api-reference.md) for complete listing*