TypeLevel.hs

-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

-- | A collection of type families and other type-level machinery
-- for working with Michelson types.
module Michelson.Typed.TypeLevel
  ( -- * Right-combed pairs
    IsPair
  , CombedPairLeafCount
  , CombedPairNodeCount
  , CombedPairLeafCountIsAtLeast
  , CombedPairNodeIndexIsValid
  )
  where

import Michelson.Typed.T (T(TPair))
import Util.Peano (Nat(S, Z), Peano, ToPeano)

----------------------------------------------------------------------------
-- Right-combed pairs
----------------------------------------------------------------------------

type family IsPair (pair :: T) :: Bool where
  IsPair ('TPair _ _) = 'True
  IsPair _ = 'False

-- | 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.
type family CombedPairLeafCount (t :: T) :: Peano where
  CombedPairLeafCount ('TPair _ ('TPair y z)) = 'S (CombedPairLeafCount ('TPair y z))
  CombedPairLeafCount ('TPair _ _) = ToPeano 2

-- | Returns the number of nodes in a right-combed pair.
type family CombedPairNodeCount (t :: T) :: Peano where
  CombedPairNodeCount ('TPair _ ('TPair y z)) = 'S ('S (CombedPairNodeCount ('TPair y z)))
  CombedPairNodeCount ('TPair _ _) = ToPeano 3

-- | Checks whether a pair contains at least @n@ elements.
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

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