Morley.Michelson.Typed.TypeLevel

A collection of type families and other type-level machinery for working with Michelson types.

Right-combed pairs

type family IsPair (pair :: T) :: Bool where ...

Equations

IsPair ('TPair _ _) = 'True

IsPair _ = 'False

type family CombedPairLeafCount (t :: T) :: Peano where ...

Returns the number of leaves in a right-combed pair.

CombedPairLeafCount ('TPair 'TInt ('TPair 'TString 'TUnit))
~
ToPeano 3

If the pair contains sub-trees to the left, they will not be accounted for. E.g. the length of pair w (pair x y) z is 3.

Equations

CombedPairLeafCount ('TPair _ ('TPair y z)) = 'S (CombedPairLeafCount ('TPair y z))

CombedPairLeafCount ('TPair _ _) = ToPeano 2

type family CombedPairNodeCount (t :: T) :: Peano where ...

Returns the number of nodes in a right-combed pair.

Equations

CombedPairNodeCount ('TPair _ ('TPair y z)) = 'S ('S (CombedPairNodeCount ('TPair y z)))

CombedPairNodeCount ('TPair _ _) = ToPeano 3

type family CombedPairLeafCountIsAtLeast (n :: Peano) (t :: T) :: Bool where ...

Checks whether a pair contains at least n elements.

Equations

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 ...

For a given node index i, this type family checks whether a pair has at least i+1 nodes.

Note that the index 0 is always valid, even if the input type is not a pair.

Equations

CombedPairNodeIndexIsValid 'Z _ = 'True

CombedPairNodeIndexIsValid ('S 'Z) ('TPair _ _) = 'True

CombedPairNodeIndexIsValid ('S ('S nodeIndex')) ('TPair _ right) = CombedPairNodeIndexIsValid nodeIndex' right

CombedPairNodeIndexIsValid _ _ = 'False