Copyright | (C) 2015-2016, University of Twente |
---|---|
License | BSD2 (see the file LICENSE) |
Maintainer | Christiaan Baaij <christiaan.baaij@gmail.com> |
Safe Haskell | None |
Language | Haskell2010 |
- type CoreSOP = SOP TyVar Type
- normaliseNat :: Type -> CoreSOP
- reifySOP :: CoreSOP -> Type
- data UnifyItem v c n
- type TyUnify v c n = [UnifyItem v c n]
- type CoreUnify a = TyUnify TyVar Type a
- substsSOP :: (Ord v, Ord c) => TyUnify v c n -> SOP v c -> SOP v c
- substsSubst :: (Ord v, Ord c) => TyUnify v c n -> TyUnify v c n -> TyUnify v c n
- data UnifyResult
- unifyNats :: Ct -> CoreSOP -> CoreSOP -> TcPluginM UnifyResult
- unifiers :: Ct -> CoreSOP -> CoreSOP -> CoreUnify Ct
- fvSOP :: CoreSOP -> UniqSet TyVar
Nat
expressions <-> SOP
terms
normaliseNat :: Type -> CoreSOP Source
Substitution on SOP
terms
(Outputable v, Outputable c) => Outputable (UnifyItem v c n) Source |
substsSOP :: (Ord v, Ord c) => TyUnify v c n -> SOP v c -> SOP v c Source
Apply a substitution to a single normalised SOP
term
substsSubst :: (Ord v, Ord c) => TyUnify v c n -> TyUnify v c n -> TyUnify v c n 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.
unifiers :: Ct -> CoreSOP -> CoreSOP -> CoreUnify Ct 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]