Copyright | (C) 2015, 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 SubstItem v c n = SubstItem {}
- type TySubst v c n = [SubstItem v c n]
- type CoreSubst = TySubst TyVar Type Ct
- substsSOP :: (Ord v, Ord c) => TySubst v c n -> SOP v c -> SOP v c
- substsSubst :: (Ord v, Ord c) => TySubst v c n -> TySubst v c n -> TySubst v c n
- data UnifyResult
- unifyNats :: Ct -> CoreSOP -> CoreSOP -> TcPluginM UnifyResult
- unifiers :: Ct -> CoreSOP -> CoreSOP -> CoreSubst
- fvSOP :: CoreSOP -> UniqSet TyVar
Nat
expressions <-> SOP
terms
normaliseNat :: Type -> CoreSOP Source
Substitution on SOP
terms
(Outputable v, Outputable c) => Outputable (SubstItem v c n) Source |
substsSOP :: (Ord v, Ord c) => TySubst v c n -> SOP v c -> SOP v c Source
Apply a substitution to a single normalised SOP
term
substsSubst :: (Ord v, Ord c) => TySubst v c n -> TySubst v c n -> TySubst 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 -> CoreSubst 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] (3 * a) ~ 0 ==> [a := 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]