ghc-typelits-natnormalise-0.7.1: GHC typechecker plugin for types of kind GHC.TypeLits.Nat

Copyright(C) 2015-2016 University of Twente
2017 QBayLogic B.V.
LicenseBSD2 (see the file LICENSE)
MaintainerChristiaan Baaij <christiaan.baaij@gmail.com>
Safe HaskellNone
LanguageHaskell2010

GHC.TypeLits.Normalise.Unify

Contents

Description

 
Synopsis

Nat expressions <-> SOP terms

newtype CType Source #

Constructors

CType 

Fields

Instances
Eq CType Source # 
Instance details

Defined in GHC.TypeLits.Normalise.Unify

Methods

(==) :: CType -> CType -> Bool #

(/=) :: CType -> CType -> Bool #

Ord CType Source # 
Instance details

Defined in GHC.TypeLits.Normalise.Unify

Methods

compare :: CType -> CType -> Ordering #

(<) :: CType -> CType -> Bool #

(<=) :: CType -> CType -> Bool #

(>) :: CType -> CType -> Bool #

(>=) :: CType -> CType -> Bool #

max :: CType -> CType -> CType #

min :: CType -> CType -> CType #

Outputable CType Source # 
Instance details

Defined in GHC.TypeLits.Normalise.Unify

Methods

ppr :: CType -> SDoc #

pprPrec :: Rational -> CType -> SDoc #

type CoreSOP = SOP TyVar CType Source #

SOP with TyVar variables

normaliseNat :: Type -> Writer [(Type, Type)] CoreSOP Source #

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 (+,-,*,^)

normaliseNatEverywhere :: Type -> Writer [(Type, Type)] (Maybe Type) Source #

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.

reifySOP :: CoreSOP -> Type Source #

Convert a SOP term back to a type of kind Nat

Substitution on SOP terms

data UnifyItem v c Source #

Constructors

SubstItem 

Fields

UnifyItem 

Fields

Instances
(Eq v, Eq c) => Eq (UnifyItem v c) Source # 
Instance details

Defined in GHC.TypeLits.Normalise.Unify

Methods

(==) :: UnifyItem v c -> UnifyItem v c -> Bool #

(/=) :: UnifyItem v c -> UnifyItem v c -> Bool #

(Outputable v, Outputable c) => Outputable (UnifyItem v c) Source # 
Instance details

Defined in GHC.TypeLits.Normalise.Unify

Methods

ppr :: UnifyItem v c -> SDoc #

pprPrec :: Rational -> UnifyItem v c -> SDoc #

type CoreUnify = UnifyItem TyVar CType Source #

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.

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.

Constructors

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 # 
Instance details

Defined in GHC.TypeLits.Normalise.Unify

unifyNats :: Ct -> CoreSOP -> CoreSOP -> TcPluginM UnifyResult Source #

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.

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)

solveIneq Source #

Arguments

:: Word

Solving depth

-> Ineq

Inequality we want to solve

-> Ineq

Given/proven inequality

-> WriterT (Set CType) Maybe Bool

Solver result

  • Nothing: exhausted solver steps
  • Just True: inequality is solved
  • Just False: solver is unable to solve inequality, note that this does not mean the wanted inequality does not hold.

Try to solve inequalities

ineqToSubst :: Ineq -> Maybe CoreUnify Source #

Give the smallest solution for an inequality

instantSolveIneq Source #

Arguments

:: Word

Solving depth

-> Ineq

Inequality we want to solve

-> WriterT (Set CType) Maybe Bool 

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

Properties