SOP with TyVar variables

Convert a type of kind Nat to an SOP term, but only when the type is constructed out of:

• literals
• type variables
• Applications of the arithmetic operators (+,-,*,^)

Applies normaliseNat and simplifySOP to type or predicats to reduce any occurence of sub-terms of kind Nat. If the result is the same as input, returns Nothing.

Convert a SOP term back to a type of kind Nat

A substitution is essentially a list of (variable, SOP) pairs, but we keep the original Ct that lead to the substitution being made, for use when turning the substitution back into constraints.

Apply a substitution to a single normalised SOP term

Apply a substitution to a substitution

Result of comparing two SOP terms, returning a potential substitution list under which the two terms are equal.

Given two SOPs u and v, when their free variables (fvSOP) are the same, then we Win if u and v are equal, and Lose otherwise.

If u and v do not have the same free variables, we result in a Draw, ware u and v are only equal when the returned CoreSubst holds.

Find unifiers for two SOP terms

Can find the following unifiers:

t ~ a + b          ==>  [t := a + b]
a + b ~ t          ==>  [t := a + b]
(a + c) ~ (b + c)  ==>  \[a := b\]
(2*a) ~ (2*b)      ==>  [a := b]
(2 + a) ~ 5        ==>  [a := 3]
(i * a) ~ j        ==>  [a := div j i], when (mod j i == 0)

However, given a wanted:

[W] t ~ a + b

this function returns [], or otherwise we "solve" the constraint by finding a unifier equal to the constraint.

However, given a wanted:

[W] (a + c) ~ (b + c)

we do return the unifier:

[a := b]

Find the TyVar in a CoreSOP

Subtract an inequality, in order to either:

• See if the smallest solution is a natural number
• Cancel sums, i.e. monotonicity of addition

subtractIneq (2*y <=? 3*x ~ True)  = (-2*y + 3*x)
subtractIneq (2*y <=? 3*x ~ False) = (-3*x + (-1) + 2*y)

Try to solve inequalities

Give the smallest solution for an inequality

Try to instantly solve an inequality by using the inequality solver using 1 <=? 1 ~ True as the given constraint.