Copyright  (C) 20152016 University of Twente 2017 QBayLogic B.V. 

License  BSD2 (see the file LICENSE) 
Maintainer  Christiaan Baaij <christiaan.baaij@gmail.com> 
Safe Haskell  None 
Language  Haskell2010 
Synopsis
 newtype CType = CType {}
 type CoreSOP = SOP TyVar CType
 normaliseNat :: Type > Writer [(Type, Type)] CoreSOP
 normaliseNatEverywhere :: Type > Writer [(Type, Type)] (Maybe Type)
 normaliseSimplifyNat :: Type > Writer [(Type, Type)] Type
 reifySOP :: CoreSOP > Type
 data UnifyItem v c
 type CoreUnify = UnifyItem TyVar CType
 substsSOP :: (Ord v, Ord c) => [UnifyItem v c] > SOP v c > SOP v c
 substsSubst :: (Ord v, Ord c) => [UnifyItem v c] > [UnifyItem v c] > [UnifyItem v c]
 data UnifyResult
 unifyNats :: Ct > CoreSOP > CoreSOP > TcPluginM UnifyResult
 unifiers :: Ct > CoreSOP > CoreSOP > [CoreUnify]
 fvSOP :: CoreSOP > UniqSet TyVar
 subtractIneq :: (CoreSOP, CoreSOP, Bool) > CoreSOP
 solveIneq :: Word > Ineq > Ineq > WriterT (Set CType) Maybe Bool
 ineqToSubst :: Ineq > Maybe CoreUnify
 subtractionToPred :: (Type, Type) > (PredType, Kind)
 instantSolveIneq :: Word > Ineq > WriterT (Set CType) Maybe Bool
 solvedInEqSmallestConstraint :: [(Bool, Set a)] > (Bool, Set a)
 isNatural :: CoreSOP > WriterT (Set CType) Maybe Bool
Nat
expressions <> SOP
terms
normaliseNatEverywhere :: Type > Writer [(Type, Type)] (Maybe Type) Source #
Applies normaliseNat
and simplifySOP
to type or predicates to reduce
any occurrences of subterms of kind Nat
. If the result is
the same as input, returns
.Nothing
Substitution on SOP
terms
Instances
(Eq v, Eq c) => Eq (UnifyItem v c) Source #  
(Outputable v, Outputable c) => Outputable (UnifyItem v c) Source #  
substsSOP :: (Ord v, Ord c) => [UnifyItem v c] > SOP v c > SOP v c Source #
Apply a substitution to a single normalised SOP
term
substsSubst :: (Ord v, Ord c) => [UnifyItem v c] > [UnifyItem v c] > [UnifyItem v c] Source #
Apply a substitution to a substitution
Find unifiers
data UnifyResult Source #
Result of comparing two SOP
terms, returning a potential substitution
list under which the two terms are equal.
Win  Two terms are equal 
Lose  Two terms are not equal 
Draw [CoreUnify]  Two terms are only equal if the given substitution holds 
Instances
Outputable UnifyResult Source #  
Defined in GHC.TypeLits.Normalise.Unify ppr :: UnifyResult > SDoc # pprPrec :: Rational > UnifyResult > SDoc # 
unifiers :: Ct > CoreSOP > CoreSOP > [CoreUnify] Source #
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]
Free variables in SOP
terms
Inequalities
subtractIneq :: (CoreSOP, CoreSOP, Bool) > CoreSOP Source #
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)
:: Word  Solving depth 
> Ineq  Inequality we want to solve 
> Ineq  Given/proven inequality 
> WriterT (Set CType) Maybe Bool  Solver result

Try to solve inequalities
ineqToSubst :: Ineq > Maybe CoreUnify Source #
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.