Predicates that classify a unification problem into one of the decidable
fragments handled by ShotUn.Pattern (Miller patterns) and
ShotUn.Matching (Huet second-order matching), plus a helper for
computing the order of a simple type.
Summary
Functions
Returns true when every free variable, constant and bound variable
appearing in the term has a type of order at most max_order.
Returns true when the term has no free variables.
Returns true when every right-hand side is ground and every type in
the problem has order at most 2 (Huet's second-order fragment).
If the term is the eta-long primitive of a single bound variable whose
binder lies in the surrounding context (i.e. above the term's own
abstractions), returns the index of that binder relative to the
surrounding context. Otherwise returns :not_bvar.
Returns true when the term is a higher-order pattern: every
occurrence of a free variable is applied to a list of pairwise distinct
bound-variable arguments.
Returns true when every side of every pair is a higher-order pattern.
Returns the order of a simple type.
Functions
@spec bounded_order?(ShotDs.Data.Term.term_id(), non_neg_integer()) :: boolean()
Returns true when every free variable, constant and bound variable
appearing in the term has a type of order at most max_order.
@spec ground?(ShotDs.Data.Term.term_id()) :: boolean()
Returns true when the term has no free variables.
@spec matching_problem?([term_pair()]) :: boolean()
Returns true when every right-hand side is ground and every type in
the problem has order at most 2 (Huet's second-order fragment).
@spec outer_bvar_index(ShotDs.Data.Term.term_id()) :: pos_integer() | :not_bvar
If the term is the eta-long primitive of a single bound variable whose
binder lies in the surrounding context (i.e. above the term's own
abstractions), returns the index of that binder relative to the
surrounding context. Otherwise returns :not_bvar.
@spec pattern?(ShotDs.Data.Term.term_id()) :: boolean()
Returns true when the term is a higher-order pattern: every
occurrence of a free variable is applied to a list of pairwise distinct
bound-variable arguments.
@spec pattern_problem?([term_pair()]) :: boolean()
Returns true when every side of every pair is a higher-order pattern.
@spec type_order(ShotDs.Data.Type.t()) :: non_neg_integer()
Returns the order of a simple type.
$$ \text{order}(\beta) = 0 \quad\text{for base } \beta $$ $$ \text{order}(\tau_1 \to \dots \to \tau_n \to \beta) = \max_{i}(\text{order}(\tau_i) + 1) $$