module FullSession.Base where
data Z = Z deriving Show
data S n = S n deriving Show
data P n = P n
class Nat n where
nat :: n
instance Nat Z where
nat = Z
instance Nat n => Nat (S n) where
nat = S nat
data T = T
data F = F
class And b1 b2 b | b1 b2 -> b
class EqNat x y b | x y -> b
instance EqNat Z Z T
instance EqNat (S n) Z F
instance EqNat Z (S n) F
instance EqNat n n' b => EqNat (S n) (S n') b
class Sub n n' where
sub :: n -> n' -> SubT n n'
sub_ :: Either n n' -> SubT n n'
instance Sub n n where { sub _ _ = Z; sub_ _ = Z }
instance Sub (S n) n where { sub _ _ = S Z; sub_ _ = S Z }
instance Sub (S (S n)) n where { sub _ _ = S (S Z); sub_ _ = S (S Z) }
instance Sub (S (S (S n))) n where { sub _ _ = S (S (S Z)); sub_ _ = S (S (S Z)) }
instance Sub (S (S (S (S n)))) n where { sub _ _ = S (S (S (S Z))); sub_ _ = S (S (S (S Z))) }
instance Sub (S (S (S (S (S n))))) n where { sub _ _ = S (S (S (S (S Z)))); sub_ _ = S (S (S (S (S Z)))) }
instance Sub (S (S (S (S (S (S n)))))) n where { sub _ _ = S (S (S (S (S (S Z))))); sub_ _ = S (S (S (S (S (S Z))))) }
instance Sub (S (S (S (S (S (S (S n))))))) n where { sub _ _ = S (S (S (S (S (S (S Z)))))); sub_ _ = S (S (S (S (S (S (S Z)))))) }
instance Sub (S (S (S (S (S (S (S (S n)))))))) n where { sub _ _ = S (S (S (S (S (S (S (S Z))))))); sub_ _ = S (S (S (S (S (S (S (S Z))))))) }
instance Sub (S (S (S (S (S (S (S (S (S n))))))))) n where { sub _ _ = S (S (S (S (S (S (S (S (S Z)))))))); sub_ _ = S (S (S (S (S (S (S (S (S Z)))))))) }
instance Sub n (S n) where { sub _ _ = P Z; sub_ _ = P Z }
instance Sub n (S (S n)) where { sub _ _ = P (P Z); sub_ _ = P (P Z) }
instance Sub n (S (S (S n))) where { sub _ _ = P (P (P Z)); sub_ _ = P (P (P Z)) }
instance Sub n (S (S (S (S n)))) where { sub _ _ = P (P (P (P Z))); sub_ _ = P (P (P (P Z))) }
instance Sub n (S (S (S (S (S n))))) where { sub _ _ = P (P (P (P (P Z)))); sub_ _ = P (P (P (P (P Z)))) }
instance Sub n (S (S (S (S (S (S n)))))) where { sub _ _ = P (P (P (P (P (P Z))))); sub_ _ = P (P (P (P (P (P Z))))) }
instance Sub n (S (S (S (S (S (S (S n))))))) where { sub _ _ = P (P (P (P (P (P (P Z)))))); sub_ _ = P (P (P (P (P (P (P Z)))))) }
instance Sub n (S (S (S (S (S (S (S (S n)))))))) where { sub _ _ = P (P (P (P (P (P (P (P Z))))))); sub_ _ = P (P (P (P (P (P (P (P Z))))))) }
instance Sub n (S (S (S (S (S (S (S (S (S n))))))))) where { sub _ _ = P (P (P (P (P (P (P (P (P Z)))))))); sub_ _ = P (P (P (P (P (P (P (P (P Z)))))))) }
type family SubT n n' :: *
type instance SubT n n = Z
type instance SubT (S n) n = S Z
type instance SubT (S (S n)) n = S (S Z)
type instance SubT (S (S (S n))) n = S (S (S Z))
type instance SubT (S (S (S (S n)))) n = S (S (S (S Z)))
type instance SubT (S (S (S (S (S n))))) n = S (S (S (S (S Z))))
type instance SubT (S (S (S (S (S (S n)))))) n = S (S (S (S (S (S Z)))))
type instance SubT (S (S (S (S (S (S (S n))))))) n = S (S (S (S (S (S (S Z))))))
type instance SubT (S (S (S (S (S (S (S (S n)))))))) n = S (S (S (S (S (S (S (S Z)))))))
type instance SubT (S (S (S (S (S (S (S (S (S n))))))))) n = S (S (S (S (S (S (S (S (S Z))))))))
type instance SubT n (S n) = P Z
type instance SubT n (S (S n)) = P (P Z)
type instance SubT n (S (S (S n))) = P (P (P Z))
type instance SubT n (S (S (S (S n)))) = P (P (P (P Z)))
type instance SubT n (S (S (S (S (S n))))) = P (P (P (P (P Z))))
type instance SubT n (S (S (S (S (S (S n)))))) = P (P (P (P (P (P Z)))))
type instance SubT n (S (S (S (S (S (S (S n))))))) = P (P (P (P (P (P (P Z))))))
type instance SubT n (S (S (S (S (S (S (S (S n)))))))) = P (P (P (P (P (P (P (P Z)))))))
type instance SubT n (S (S (S (S (S (S (S (S (S n))))))))) = P (P (P (P (P (P (P (P (P Z))))))))
data ss :> s = ss :> s
data Nil = Nil
class SList ss l | ss -> l where
len_ :: ss -> l
instance SList ss l => SList (ss :> s) (S l) where
len_ ~(ss :> s) = S (len_ ss)
instance SList Nil Z where
len_ _ = Z
class
Pickup ss n s | ss n -> s where
pickup :: ss -> n -> s
class PickupR ss n s | ss n -> s where
pickupR :: ss -> n -> s
instance ss ~ (ss':>t) => PickupR ss Z t where
pickupR (_ :> t) _ = t
instance (PickupR ss' n t, ss ~ (ss':>s')) => PickupR ss (S n) t where
pickupR (ss' :> _) (S n) = pickupR ss' n
class
Update ss n t ss' | ss n t -> ss' where
update :: ss -> n -> t -> ss'
class UpdateR ss n t ss' | ss n t -> ss' where
updateR :: ss -> n -> t -> ss'
instance UpdateR (ss:>s) Z t (ss:>t) where
updateR (ss:>_) _ t = ss :> t
instance UpdateR ss n t ss' => UpdateR (ss:>s) (S n) t (ss':>s) where
updateR (ss:>s) (S n) t = updateR ss n t :> s