module Data.Typical where
import Data.Typical.Misc
data a :#: b = a :#: b
infixr :#:
data HNil = HNil
class HHead a h | a -> h where
hHead :: a -> h
instance HHead (a :#: b) a where
hHead (a :#: _) = a
class HTail a t | a -> t where
hTail :: a -> t
instance HTail (a :#: b) b where
hTail (_ :#: b) = b
class HSplitAt a n h t | a n -> h t where
hSplitAt :: a -> n -> (h, t)
instance HSplitAt HNil n HNil HNil where
hSplitAt HNil _ = (HNil, HNil)
instance HSplitAt (a :#: b) HNil (a :#: HNil) b where
hSplitAt (a :#: b) HNil = (a :#: HNil, b)
instance (HSub (d :#: d') HNil predD, HSplitAt b predD a' b')
=> HSplitAt (a :#: b) (d :#: d') (a :#: a') b' where
hSplitAt (a :#: b) d = let (a', b') = hSplitAt b (hSub d HNil) in (a :#: a' , b')
class HMergeBy f a b c | f a b -> c where
hMergeBy :: f -> a -> b -> c
instance HMergeBy f HNil HNil HNil where
hMergeBy _ HNil HNil = HNil
instance HMergeBy f HNil (a :#: b) (a :#: b) where
hMergeBy _ HNil (a :#: b) = a :#: b
instance HMergeBy f (a :#: b) HNil (a :#: b) where
hMergeBy _ (a :#: b) HNil = a :#: b
instance (HApply f (a, c) cmp, HOrd cmp (a :#: b) (c :#: d) h a' b', HMergeBy f a' b' e)
=> HMergeBy f (a :#: b) (c :#: d) (h :#: e) where
hMergeBy f (a :#: b) (c :#: d) = let
cmp = hApply f (a, c)
(h, a', b') = hOrd cmp (a :#: b) (c :#: d)
e = hMergeBy f a' b'
in (h :#: e)
class HApply f parameter result | f parameter -> result where
hApply :: f -> parameter -> result
data B0 = B0
data B1 = B1
class HNat a
instance HNat (B1 :#: HNil)
instance HNat a => HNat (B1 :#: a)
instance HNat a => HNat (B0 :#: a)
type N1 = HNil
type N2 = B0 :#: HNil
type N3 = B1 :#: HNil
type N4 = B0 :#: N2
n1 :: N1
n1 = HNil
n2 :: N2
n2 = B0 :#: HNil
n3 :: N3
n3 = B1 :#: HNil
n4 :: N4
n4 = B0 :#: n2
class HAdd n1 n2 r | n1 n2 -> r where
hAdd :: n1 -> n2 -> r
instance HAdd HNil HNil (B0 :#: HNil) where
hAdd HNil HNil = (B0 :#: HNil)
instance HAdd HNil (B0 :#: b) (B1 :#: b) where
hAdd HNil (B0 :#: b) = B1 :#: b
instance HAdd (B0 :#: a) HNil (B1 :#: a) where
hAdd (B0 :#: a) HNil = B1 :#: a
instance HAdd HNil b b' => HAdd HNil (B1 :#: b) (B0 :#: b') where
hAdd HNil (B1 :#: b) = B0 :#: hAdd HNil b
instance HAdd HNil a a' => HAdd (B1 :#: a) HNil (B0 :#: a') where
hAdd (B1 :#: a) HNil = B0 :#: hAdd HNil a
instance HAdd a b c => HAdd (B0 :#: a) (B0 :#: b) (B0 :#: c) where
hAdd (B0 :#: a) (B0 :#: b) = B0 :#: hAdd a b
instance HAdd a b c => HAdd (B0 :#: a) (B1 :#: b) (B1 :#: c) where
hAdd (B0 :#: a) (B1 :#: b) = B1 :#: hAdd a b
instance HAdd a b c => HAdd (B1 :#: a) (B0 :#: b) (B1 :#: c) where
hAdd (B1 :#: a) (B0 :#: b) = B1 :#: hAdd a b
instance (HAdd a b c, HAdd HNil c c') => HAdd (B1 :#: a) (B1 :#: b) (B0 :#: c') where
hAdd (B1 :#: a) (B1 :#: b) = B0 :#: hAdd HNil (hAdd a b)
class HSub n1 n2 r | n1 n2 -> r where
hSub :: n1 -> n2 -> r
instance HSub (B1 :#: b) HNil (B0 :#: b) where
hSub (B1 :#: b) HNil = B0 :#: b
instance HSub (B0 :#: HNil) HNil HNil where
hSub (B0 :#: HNil) HNil = HNil
instance HSub (B1 :#: HNil) (B0 :#: HNil) HNil where
hSub (B1 :#: HNil) (B0 :#: HNil) = HNil
instance HSub (b :#: c) HNil d => HSub (B0 :#: b :#: c) HNil (B1 :#: d) where
hSub (B0 :#: b :#: c) HNil = B1 :#: hSub (b :#: c) HNil
instance HSub a b c => HSub (B0 :#: a) (B0 :#: b) (B0 :#: c) where
hSub (B0 :#: a) (B0 :#: b) = B0 :#: hSub a b
instance HSub (a :#: b) c d => HSub (B1 :#: a :#: b) (B0 :#: c) (B1 :#: d) where
hSub (B1 :#: a :#: b) (B0 :#: c) = B1 :#: hSub (a :#: b) c
instance (HAdd b N1 b', HSub a b' c) => HSub (B0 :#: a) (B1 :#: b) (B1 :#: c) where
hSub (B0 :#: a) (B1 :#: b) = B1 :#: hSub a (hAdd b HNil)
instance HSub a b c => HSub (B1 :#: a) (B1 :#: b) (B0 :#: c) where
hSub (B1 :#: a) (B1 :#: b) = B0 :#: hSub a b
class HMul a b c | a b -> c where
hMul :: a -> b -> c
class HMulSub a b c | a b -> c where
hMulSub :: a -> b -> c
instance HMulSub HNil a (a :#: HNil) where
hMulSub HNil a = (a :#: HNil)
instance HMulSub b (B0 :#: c) r => HMulSub (B0 :#: b) c r where
hMulSub (B0 :#: b) c = hMulSub b (B0 :#: c)
instance HMulSub b (B0 :#: c) r => HMulSub (B1 :#: b) c (c :#: r) where
hMulSub (B1 :#: b) c = let r = hMulSub b (B0 :#: c) in (c :#: r)
instance HCompare B0 B0 HEQ where
hCompare B0 B0 = HEQ
instance HCompare B0 B1 HLT where
hCompare B0 B1 = HLT
instance HCompare B1 B0 HGT where
hCompare B1 B0 = HGT
instance HCompare B1 B1 HEQ where
hCompare B1 B1 = HEQ
instance HCompare HNil HNil HEQ where
hCompare HNil HNil = HEQ
instance HCompare HNil (c :#: d) HLT where
hCompare HNil (_ :#: _) = HLT
instance HCompare (a :#: b) HNil HGT where
hCompare (_ :#: _) HNil = HGT
instance (HCompare a c res1, HCompare b d res2, CalcRes res1 res2 res)
=> HCompare (a :#: b) (c :#: d) res where
hCompare (a :#: b) (c :#: d) = calcRes (hCompare a c) (hCompare b d)
class CalcRes a b c | a b -> c where
calcRes :: a -> b -> c
instance CalcRes a HLT HLT where
calcRes _ HLT = HLT
instance CalcRes a HGT HGT where
calcRes _ HGT = HGT
instance CalcRes HLT HEQ HLT where
calcRes HLT HEQ = HLT
instance CalcRes HGT HEQ HGT where
calcRes HGT HEQ = HGT
instance CalcRes HEQ HEQ HEQ where
calcRes HEQ HEQ = HEQ
class HOrd cmp a b h a' b' | cmp a b -> h a' b' where
hOrd :: cmp -> a -> b -> (h, a', b')
instance HOrd HLT (ha :#: ta) (hb :#: tb) ha ta (hb :#: tb) where
hOrd HLT (ha :#: ta) (hb :#: tb) = (ha, ta, hb :#: tb)
instance HOrd HGT (ha :#: ta) (hb :#: tb) hb (ha :#: ta) tb where
hOrd HGT (ha :#: ta) (hb :#: tb) = (hb, ha :#: ta, tb)
instance HOrd HEQ (ha :#: ta) (hb :#: tb) ha ta (hb :#: tb) where
hOrd HEQ (ha :#: ta) (hb :#: tb) = (ha, ta, hb :#: tb)
class HDiv2 a b | a -> b where
hDiv2 :: a -> b
instance HDiv2 HNil HNil where
hDiv2 HNil = HNil
instance HDiv2 (a :#: b) b where
hDiv2 (_ :#: b) = b
data HCmpHNat = HCmpHNat
instance HCompare a b cmp => HApply HCmpHNat (a, b) cmp where
hApply HCmpHNat (a, b) = hCompare a b
x :: (N2 :#: N2 :#: N3 :#: N4 :#: HNil)
x = hMergeBy HCmpHNat (n2 :#: n3 :#: HNil) ((n4 `hSub` n2) :#: n4 :#: HNil)