Safe Haskell | None |
---|
- class LessGen a b
- class LeastGen a b c
- class Analyze a b | a -> b
- class (Substitution sin, Substitution sout) => LeastGen' a b c sin sout | sin a b c -> sout
- data SubstEmpty
Documentation
If LessGen a b, then b is less general than a. That is, there exists substitution s such that (s b = a).
(Analyze a _a, Analyze b _b, LeastGen' _a _b b SubstEmpty sout, Unifies sout a b) => LessGen a b |
If LeastGen a b c holds then there exists a substitution s and type c such that (s c = (a, b)).
(Analyze a _a, Analyze b _b, LeastGen' _a _b c SubstEmpty sout) => LeastGen a b c |
class Analyze a b | a -> bSource
~ * r (TCon0 Bool) => Analyze Bool r | |
~ * r (TCon0 Char) => Analyze Char r | |
~ * r (TCon0 Double) => Analyze Double r | |
~ * r (TCon0 Float) => Analyze Float r | |
~ * r (TCon0 Int) => Analyze Int r | |
~ * r (TCon0 Int8) => Analyze Int8 r | |
~ * r (TCon0 Int16) => Analyze Int16 r | |
~ * r (TCon0 Int32) => Analyze Int32 r | |
~ * r (TCon0 Int64) => Analyze Int64 r | |
~ * r (TCon0 Integer) => Analyze Integer r | |
~ * r (TCon0 Ordering) => Analyze Ordering r | |
~ * r (TCon0 Word8) => Analyze Word8 r | |
~ * r (TCon0 Word16) => Analyze Word16 r | |
~ * r (TCon0 Word32) => Analyze Word32 r | |
~ * r (TCon0 Word64) => Analyze Word64 r | |
~ * r (TCon0 ()) => Analyze () r | |
(Analyze (W a1) ra1, ~ * r (TCon1 (c ()) ra1)) => Analyze (c a1) r | |
~ * r (TCon0 Bool) => Analyze (W Bool) r | |
~ * r (TCon0 Char) => Analyze (W Char) r | |
~ * r (TCon0 Double) => Analyze (W Double) r | |
~ * r (TCon0 Float) => Analyze (W Float) r | |
~ * r (TCon0 Int) => Analyze (W Int) r | |
~ * r (TCon0 Int8) => Analyze (W Int8) r | |
~ * r (TCon0 Int16) => Analyze (W Int16) r | |
~ * r (TCon0 Int32) => Analyze (W Int32) r | |
~ * r (TCon0 Int64) => Analyze (W Int64) r | |
~ * r (TCon0 Integer) => Analyze (W Integer) r | |
~ * r (TCon0 Ordering) => Analyze (W Ordering) r | |
~ * r (TCon0 Word8) => Analyze (W Word8) r | |
~ * r (TCon0 Word16) => Analyze (W Word16) r | |
~ * r (TCon0 Word32) => Analyze (W Word32) r | |
~ * r (TCon0 Word64) => Analyze (W Word64) r | |
~ * r (TCon0 ()) => Analyze (W ()) r | |
~ * r (TVar a) => Analyze (W a) r | |
(Analyze (W a1) ra1, Analyze (W a2) ra2, Analyze (W a3) ra3, Analyze (W a4) ra4, Analyze (W a5) ra5, ~ * r (TCon5 (c () () () () ()) ra1 ra2 ra3 ra4 ra5)) => Analyze (W (c a1 a2 a3 a4 a5)) r | |
(Analyze (W a1) ra1, Analyze (W a2) ra2, Analyze (W a3) ra3, Analyze (W a4) ra4, ~ * r (TCon4 (c () () () ()) ra1 ra2 ra3 ra4)) => Analyze (W (c a1 a2 a3 a4)) r | |
(Analyze (W a1) ra1, Analyze (W a2) ra2, Analyze (W a3) ra3, ~ * r (TCon3 (c () () ()) ra1 ra2 ra3)) => Analyze (W (c a1 a2 a3)) r | |
(Analyze (W a1) ra1, Analyze (W a2) ra2, ~ * r (TCon2 (c () ()) ra1 ra2)) => Analyze (W (c a1 a2)) r | |
(Analyze (W a1) ra1, ~ * r (TCon1 (c ()) ra1)) => Analyze (W (c a1)) r | |
(Analyze (W a1) ra1, Analyze (W a2) ra2, ~ * r (TCon2 (c () ()) ra1 ra2)) => Analyze (c a1 a2) r | |
(Analyze (W a1) ra1, Analyze (W a2) ra2, Analyze (W a3) ra3, ~ * r (TCon3 (c () () ()) ra1 ra2 ra3)) => Analyze (c a1 a2 a3) r | |
(Analyze (W a1) ra1, Analyze (W a2) ra2, Analyze (W a3) ra3, Analyze (W a4) ra4, ~ * r (TCon4 (c () () () ()) ra1 ra2 ra3 ra4)) => Analyze (c a1 a2 a3 a4) r | |
(Analyze (W a1) ra1, Analyze (W a2) ra2, Analyze (W a3) ra3, Analyze (W a4) ra4, Analyze (W a5) ra5, ~ * r (TCon5 (c () () () () ()) ra1 ra2 ra3 ra4 ra5)) => Analyze (c a1 a2 a3 a4 a5) r |
class (Substitution sin, Substitution sout) => LeastGen' a b c sin sout | sin a b c -> soutSource
(Substitution sin, Substitution sout, MapsTo sin (a, b) c', VarCase c' (a, b) c sin sout, Analyze (W c) (TVar c)) => LeastGen' a b c sin sout | |
(Substitution s0, ~ * a c) => LeastGen' (TCon0 a) (TCon0 a) c s0 s0 | |
(LeastGen' a1 b1 c1 s0 s1, ~ (* -> *) d d', ~ * (d c1) c) => LeastGen' (TCon1 (d ()) a1) (TCon1 (d' ()) b1) c s0 s1 | |
(LeastGen' a1 b1 c1 s0 s1, LeastGen' a2 b2 c2 s1 s2, ~ (* -> * -> *) d d', ~ * (d c1 c2) c) => LeastGen' (TCon2 (d () ()) a1 a2) (TCon2 (d' () ()) b1 b2) c s0 s2 | |
(LeastGen' a1 b1 c1 s0 s1, LeastGen' a2 b2 c2 s1 s2, LeastGen' a3 b3 c3 s2 s3, ~ (* -> * -> * -> *) d d', ~ * (d c1 c2 c3) c) => LeastGen' (TCon3 (d () () ()) a1 a2 a3) (TCon3 (d' () () ()) b1 b2 b3) c s0 s3 | |
(LeastGen' a1 b1 c1 s0 s1, LeastGen' a2 b2 c2 s1 s2, LeastGen' a3 b3 c3 s2 s3, LeastGen' a4 b4 c4 s3 s4, ~ (* -> * -> * -> * -> *) d d', ~ * (d c1 c2 c3 c4) c) => LeastGen' (TCon4 (d () () () ()) a1 a2 a3 a4) (TCon4 (d' () () () ()) b1 b2 b3 b4) c s0 s4 | |
(LeastGen' a1 b1 c1 s0 s1, LeastGen' a2 b2 c2 s1 s2, LeastGen' a3 b3 c3 s2 s3, LeastGen' a4 b4 c4 s3 s4, LeastGen' a5 b5 c5 s4 s5, ~ (* -> * -> * -> * -> * -> *) d d', ~ * (d c1 c2 c3 c4 c5) c) => LeastGen' (TCon5 (d () () () () ()) a1 a2 a3 a4 a5) (TCon5 (d' () () () () ()) b1 b2 b3 b4 b5) c s0 s5 |
data SubstEmpty Source
Encoding of substitutions as partial maps