ShotDs.Util.LatexFormatter (shot_ds v1.2.6)

Copy Markdown View Source

Renders HOL objects as LaTeX.

Types are printed as subscripts. Logical constants of the signature (⊤, ⊥, ¬, ∧, ∨, ⊃, ≡, =, ∀, ∃) are rendered as their standard LaTeX symbols without any type annotation. Bound variables are reconstructed with fresh names drawn from a type-specific pool, avoiding capture with free variables and outer binders. Duplicates are disambiguated with running superscripts (subscripts are reserved for the type annotation).

Examples

iex> import ShotDs.Hol.Dsl
iex> import ShotDs.Hol.Definitions
iex> alias ShotDs.Util.LatexFormatter
iex> t = forall(x_i(), &(x_i() &&& &1))
...> # etc.

Summary

Types

formattable()

HOL objects understood by the formatter.

opts()

Options accepted by format/2 and format!/2.

Functions

format(obj, opts \\ [])

Renders the given HOL object as a LaTeX string. Returns {:ok, result} or {:error, reason}.

format!(obj, opts \\ [])

Renders the given HOL object as a LaTeX string. Raises on error.

with_latex_aliases(aliases, fun)

Runs fun with a LaTeX alias map active. Unlike ShotDs.Util.Formatter.with_aliases/2 — whose values go through escape_name/1 before being spliced into the output — values here are used verbatim as LaTeX for the corresponding reference() variable name or type goal. That lets callers hand out proper LaTeX identifiers (e.g. "H^{1}", "\hat{F}_{2}") for fresh metas.

Types

formattable()

@type formattable() ::
  ShotDs.Data.Type.t()
  | ShotDs.Data.Declaration.t()
  | ShotDs.Data.Term.t()
  | ShotDs.Data.Term.term_id()
  | ShotDs.Data.Substitution.t()
  | ShotDs.Data.Problem.t()

HOL objects understood by the formatter.

opts()

@type opts() :: [
  hide_types: boolean(),
  merge_binder: boolean(),
  reconstruct_names: boolean(),
  math_mode: :raw | :inline | :display
]

Options accepted by format/2 and format!/2.

  • :hide_types — omit type subscripts on non-logical symbols (default false).
  • :merge_binder — collapse ∀(λx. body) into ∀ x.\, body (default true; ignored when :reconstruct_names is false).
  • :reconstruct_names — pick fresh names for bound variables (default true). When false, binders are rendered as \lambda_{τ} and bound references as \mathtt{k}_{τ}, preserving the raw de Bruijn structure.
  • :math_mode — one of :raw (default), :inline ($…$) or :display ($$…$$).

Functions

format(obj, opts \\ [])

@spec format(formattable(), opts()) ::
  {:ok, String.t()}
  | ShotDs.Stt.TermFactory.lookup_error_t()
  | {:error, :unknown_argument}

Renders the given HOL object as a LaTeX string. Returns {:ok, result} or {:error, reason}.

format!(obj, opts \\ [])

@spec format!(formattable(), opts()) :: String.t()

Renders the given HOL object as a LaTeX string. Raises on error.

with_latex_aliases(aliases, fun)

@spec with_latex_aliases(%{required(reference()) => String.t()}, (-> a)) :: a
when a: var

Runs fun with a LaTeX alias map active. Unlike ShotDs.Util.Formatter.with_aliases/2 — whose values go through escape_name/1 before being spliced into the output — values here are used verbatim as LaTeX for the corresponding reference() variable name or type goal. That lets callers hand out proper LaTeX identifiers (e.g. "H^{1}", "\hat{F}_{2}") for fresh metas.

Falls back through :hol_aliases (plain-text nicknames) and finally to the V^{short_ref}/\mathrm{c}^{short_ref}/\tau_{short_ref} defaults for any ref not listed in this map (free variable, constant, and type-goal, respectively). Restores the previous binding on exit.

Only LatexFormatter consults :hol_latex_aliases — the plain-text Formatter and Declaration.format/2 ignore it entirely, so the two alias mechanisms don't interfere.