# `ShotTo.Parameters`
[🔗](https://github.com/jcschuster/ShotTo/blob/v0.1.0/lib/shot_to/parameters.ex#L1)

Parameters that define a concrete instance of NCPO-LNF.

NCPO-LNF is parameterised by the following data (see Definition 8 and the
surrounding text in Niederhauser & Middeldorp, *NCPO goes Beta-Eta-Long
Normal Form*, 2025):

  * A well-founded strict order `≻_S` on base sorts (atoms). The
    admissible type order `≻_T` used inside NCPO is derived from this by
    Lemma 4.
  * A precedence `≿_F` on function symbols (constants) with a well-founded
    strict part `≻_F` and equivalence `≃_F`.
  * A status `stat(f) ∈ {:mul, :lex}` for each constant.
  * A predicate `basic(a)` selecting which base sorts are *basic*.
  * An accessibility predicate `Acc(f, i)` selecting which argument
    positions of each constant are *accessible*.

For the Haskell reference, these are unknowns decided by an SMT solver so
that termination of an entire rewrite system can be proven. In `ShotTo`
we take them as fixed inputs and obtain a decidable boolean predicate on
pairs of terms, which is what a tableau prover or equational-reasoning
engine typically needs.

## Defaults

The default parameter set is deliberately *permissive*: all sorts are
basic and equivalent, all positions are accessible, all constants are
equivalent in precedence with `:lex` status. Under these defaults NCPO
reduces to the simple argument-subterm order together with lexicographic
comparison inside shared heads, which is rarely what a user wants — the
point is to make the API usable out of the box and to make it explicit
that *every* meaningful orientation requires the user to supply at least
a constant precedence.

## Validity of parameters

Soundness of NCPO-LNF depends on `Acc` and `basic` satisfying the
compatibility conditions of Definitions 5 & 6 with respect to the chosen
type precedence. `ShotTo` does not currently check these conditions — it
trusts the caller. `ShotTo.Parameters.validate/2` gives a best-effort
check for a given set of constants; callers who need a soundness
guarantee should either invoke it or default to `accessible: :all` and
`basic_sorts: :all`, which are vacuously sound (the compatibility
conditions become trivial when every position is accessible and every
sort is basic).

# `accessible`

```elixir
@type accessible() ::
  :all
  | MapSet.t({const_id(), arg_index()})
  | (const_id(), arg_index() -> boolean())
```

Which argument positions of which constants are accessible. `:all`
treats every position as accessible. A MapSet contains `{const_id,
index}` tuples. A predicate function is also accepted.

# `arg_index`

```elixir
@type arg_index() :: pos_integer()
```

Argument position, counted from 1.

# `basic_sorts`

```elixir
@type basic_sorts() :: :all | MapSet.t(sort_id()) | (sort_id() -> boolean())
```

Which sorts are basic. `:all` treats every sort as basic. A MapSet
explicitly lists the basic sorts. A predicate function is also accepted.

# `const_id`

```elixir
@type const_id() :: String.t() | reference()
```

Identifier for a constant as used in `ShotDs.Data.Declaration.name`. In
practice either a binary name or an Erlang reference (for generated
constants).

# `const_precedence`

```elixir
@type const_precedence() ::
  %{optional(const_id()) => integer()} | (const_id() -> integer())
```

Constant precedence. Either a map from constant identifiers to integers
(larger integer means greater in `≻_F`; equal integers mean `≃_F`), or a
one-argument function with the same meaning.

# `sort_id`

```elixir
@type sort_id() :: atom()
```

Identifier for a base sort, corresponding to `ShotDs.Data.Type.type_id`
with the type-variable case excluded: an atom such as `:i`, `:o`, etc.

# `sort_precedence`

```elixir
@type sort_precedence() ::
  %{optional(sort_id()) => integer()} | (sort_id() -> integer())
```

Sort precedence. Either a map from sort identifiers to integers or a
one-argument function with the same meaning.

# `status`

```elixir
@type status() :: :lex | :mul
```

Symbol status.

# `status_map`

```elixir
@type status_map() :: %{optional(const_id()) => status()} | (const_id() -> status())
```

Status assignment. Either a map or a one-argument function.

# `t`

```elixir
@type t() :: %ShotTo.Parameters{
  accessible: accessible(),
  basic_sorts: basic_sorts(),
  const_precedence: const_precedence(),
  sort_precedence: sort_precedence(),
  status: status_map()
}
```

# `accessible?`

```elixir
@spec accessible?(t(), const_id(), arg_index()) :: boolean()
```

Returns `true` if the 1-based argument position `i` of the constant
identified by `name` is declared accessible.

# `basic?`

```elixir
@spec basic?(t(), sort_id()) :: boolean()
```

Returns `true` if the given base sort is declared basic.

# `equiv?`

```elixir
@spec equiv?(t(), const_id(), const_id()) :: boolean()
```

Returns `true` if `name1` and `name2` are equivalent in `≃_F`.

# `from_precedence_list`

```elixir
@spec from_precedence_list(
  [[const_id()]],
  keyword()
) :: t()
```

Convenience: builds parameters from a *total* precedence given as an
ordered list, most-greater first. Each constant is placed at the rank
corresponding to its position (so the first element in the list is
strictly greater than the rest). Constants not listed are assigned rank
`0` by default lookup.

Inner lists group equivalent constants.

    iex> alias ShotTo.Parameters
    iex> p = Parameters.from_precedence_list([["f"], ["g", "h"], ["c"]])
    iex> Parameters.gt?(p, "f", "g")
    true
    iex> Parameters.equiv?(p, "g", "h")
    true
    iex> Parameters.gt?(p, "h", "c")
    true

# `gt?`

```elixir
@spec gt?(t(), const_id(), const_id()) :: boolean()
```

Returns `true` if `name1` is strictly greater than `name2` in `≻_F`.

# `new`

```elixir
@spec new(keyword()) :: t()
```

Builds a parameter struct. All keys are optional; unspecified fields fall
back to the permissive defaults described in the module docs.

## Example

    iex> alias ShotTo.Parameters
    iex> params = Parameters.new(
    ...>   const_precedence: %{"f" => 2, "g" => 1, "c" => 0},
    ...>   status: %{"f" => :lex, "g" => :mul}
    ...> )
    iex> Parameters.prec(params, "f")
    2

# `prec`

```elixir
@spec prec(t(), const_id()) :: integer()
```

Looks up the precedence rank of a constant. Defaults to `0` for unknown
constants, which makes unknown constants equivalent to each other and to
any other rank-0 constant.

# `sort_prec`

```elixir
@spec sort_prec(t(), sort_id()) :: integer()
```

Looks up the precedence rank of a sort. Defaults to `0` for unknown sorts.

# `status`

```elixir
@spec status(t(), const_id()) :: status()
```

Looks up the status of a constant. Defaults to `:lex` for unknown constants.

# `validate`

```elixir
@spec validate(t(), %{optional(const_id()) => ShotDs.Data.Type.t()}) ::
  :ok | {:error, [String.t()]}
```

Best-effort validity check for `Acc` and `basic` against the types of a
given set of constants. Returns `:ok` if no violations were found, or
`{:error, violations}` with a list of human-readable strings describing
the issues.

The checks performed:

  * For each accessible `{f, i}` where `f : T_1 → … → T_n → a`, the base
    sort `a` must appear only at positive positions of `T_i` (approximated
    here as: every base sort that appears in `T_i` must be `a` or less
    than `a` in the sort precedence).
  * For each basic sort `a`, every smaller-or-equal sort appearing in an
    accessible argument type (whose host constant returns `a`) must also
    be basic.

These are the implementation-level approximations of the conditions
sketched in Definition 5 and following in the NCPO-LNF paper. They are
*best-effort*: they cover the common cases without attempting the full
positive-sort-position analysis of [2, Definition 7.2].

---

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