Admissible type order ≻_T and related predicates used by NCPO-LNF.
The order implemented here is the concrete admissible order of Lemma 4
in the NCPO-LNF paper (Niederhauser & Middeldorp, 2025), which is in
turn Lemma 2.3 of the CPO paper [Blanqui/Jouannaud/Rubio, 2015]. It is
the smallest order ≻_T on ShotDs.Data.Type.t that contains:
- the strict part of the user-supplied sort precedence
≻_S, and - the right-argument relation
▷_r(i.e.T → U ▷_r U),
and is closed under right-congruence (V ≻_T V' implies
U → V ≻_T U → V' for every U).
Note: ShotDs.Data.Type represents function types in uncurried form, so
T_1 → T_2 → … → T_n → a corresponds to
%Type{goal: a, args: [T_1, …, T_n]}. The implementation is written
directly on this representation rather than on a curried view.
Summary
Functions
Returns true if the argument type is a base type (no function arrows).
Returns true if the base sort a occurs anywhere within the given
type. This is the boolean version of the Pos_a(T) ≠ ∅ predicate used
by the structurally-smaller rule: the paper's requirement
Pos_a(T_i) = ∅ translates to not occurs_in?/2.
Reflexive closure: t ⪰_T u iff t = u or t ≻_T u.
Returns true if lhs ≻_T rhs in the admissible type order derived
from the sort precedence in params.
Functions
@spec base?(ShotDs.Data.Type.t()) :: boolean()
Returns true if the argument type is a base type (no function arrows).
@spec occurs_in?(atom(), ShotDs.Data.Type.t()) :: boolean()
Returns true if the base sort a occurs anywhere within the given
type. This is the boolean version of the Pos_a(T) ≠ ∅ predicate used
by the structurally-smaller rule: the paper's requirement
Pos_a(T_i) = ∅ translates to not occurs_in?/2.
iex> alias ShotDs.Data.Type
iex> alias ShotTo.TypeOrder
iex> TypeOrder.occurs_in?(:i, Type.new(:o, [:i, :o]))
true
iex> TypeOrder.occurs_in?(:i, Type.new(:o))
false@spec type_geq?(ShotDs.Data.Type.t(), ShotDs.Data.Type.t(), ShotTo.Parameters.t()) :: boolean()
Reflexive closure: t ⪰_T u iff t = u or t ≻_T u.
@spec type_gt?(ShotDs.Data.Type.t(), ShotDs.Data.Type.t(), ShotTo.Parameters.t()) :: boolean()
Returns true if lhs ≻_T rhs in the admissible type order derived
from the sort precedence in params.
Strict order: type_gt?(t, t, _) is always false.