module Michelson.Typed.TypeLevel
(
IsPair
, CombedPairLeafCount
, CombedPairNodeCount
, CombedPairLeafCountIsAtLeast
, CombedPairNodeIndexIsValid
)
where
import Michelson.Typed.T (T(TPair))
import Util.Peano (Nat(S, Z), Peano, ToPeano)
type family IsPair (pair :: T) :: Bool where
IsPair ('TPair _ _) = 'True
IsPair _ = 'False
type family CombedPairLeafCount (t :: T) :: Peano where
CombedPairLeafCount ('TPair _ ('TPair y z)) = 'S (CombedPairLeafCount ('TPair y z))
CombedPairLeafCount ('TPair _ _) = ToPeano 2
type family CombedPairNodeCount (t :: T) :: Peano where
CombedPairNodeCount ('TPair _ ('TPair y z)) = 'S ('S (CombedPairNodeCount ('TPair y z)))
CombedPairNodeCount ('TPair _ _) = ToPeano 3
type family CombedPairLeafCountIsAtLeast (n :: Peano) (t :: T) :: Bool where
CombedPairLeafCountIsAtLeast ('S ('S 'Z)) ('TPair _ _) = 'True
CombedPairLeafCountIsAtLeast ('S n) ('TPair _ y) = CombedPairLeafCountIsAtLeast n y
CombedPairLeafCountIsAtLeast ('S _) _ = 'False
type family CombedPairNodeIndexIsValid (nodeIndex :: Peano) (pair :: T) :: Bool where
CombedPairNodeIndexIsValid 'Z _ = 'True
CombedPairNodeIndexIsValid ('S 'Z) ('TPair _ _) = 'True
CombedPairNodeIndexIsValid ('S ('S nodeIndex')) ('TPair _ right) = CombedPairNodeIndexIsValid nodeIndex' right
CombedPairNodeIndexIsValid _ _ = 'False