Grade.hs

{-# LANGUAGE UndecidableInstances #-}
-- | Type-level grade operations.
module Imp.DSL.Grade
  ( Merge
  , Union
  , TagAll
  ) where

import GHC.TypeLits
  ( Symbol, AppendSymbol, CmpSymbol , TypeError, ErrorMessage(..) )

-- | Sorted merge of two sorted @[Symbol]@ lists, erroring on overlap.
type family Merge (xs :: [Symbol]) (ys :: [Symbol]) :: [Symbol] where
  Merge '[]       ys        = ys
  Merge xs        '[]       = xs
  Merge (x ': xs) (y ': ys) = MergeH (CmpSymbol x y) x xs y ys

type family MergeH (o :: Ordering) (x :: Symbol) (xs :: [Symbol])
                                   (y :: Symbol) (ys :: [Symbol]) :: [Symbol] where
  MergeH 'LT x xs y ys = x ': Merge xs (y ': ys)
  MergeH 'EQ x _  _ _  = TypeError ('Text "Duplicate Knightian name: " ':<>: 'ShowType x)
  MergeH 'GT x xs y ys = y ': Merge (x ': xs) ys

-- | Sorted union of two sorted @[Symbol]@ lists, allowing overlap.
type family Union (xs :: [Symbol]) (ys :: [Symbol]) :: [Symbol] where
  Union '[]       ys        = ys
  Union xs        '[]       = xs
  Union (x ': xs) (y ': ys) = UnionH (CmpSymbol x y) x xs y ys

type family UnionH (o :: Ordering) (x :: Symbol) (xs :: [Symbol])
                                   (y :: Symbol) (ys :: [Symbol]) :: [Symbol] where
  UnionH 'LT x xs y ys = x ': Union xs (y ': ys)
  UnionH 'EQ x xs _ ys = x ': Union xs ys
  UnionH 'GT x xs y ys = y ': Union (x ': xs) ys

-- | Prepend every symbol in a list with a tag and dot separator.
type family TagAll (tag :: Symbol) (xs :: [Symbol]) :: [Symbol] where
  TagAll _  '[]       = '[]
  TagAll "" xs        = xs
  TagAll t  (x ': xs) = AppendSymbol t (AppendSymbol "." x) ': TagAll t xs