{-# LANGUAGE ViewPatterns #-}
module TypeLevel.Rewrite.Internal.TypeNode where

-- GHC API
import TyCon (TyCon)
import Type (Type, isNumLitTy, isStrLitTy, mkTyConApp, splitTyConApp_maybe)

import TypeLevel.Rewrite.Internal.TypeEq


-- A 'Type' is a tree whose internal nodes are 'TypeNode's and whose leaves are
-- type variables.
data TypeNode
  = TyCon TyCon
  | TyLit TypeEq
  deriving TypeNode -> TypeNode -> Bool
(TypeNode -> TypeNode -> Bool)
-> (TypeNode -> TypeNode -> Bool) -> Eq TypeNode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypeNode -> TypeNode -> Bool
$c/= :: TypeNode -> TypeNode -> Bool
== :: TypeNode -> TypeNode -> Bool
$c== :: TypeNode -> TypeNode -> Bool
Eq

toTypeNodeApp_maybe
  :: Type
  -> Maybe (TypeNode, [Type])
toTypeNodeApp_maybe :: Type -> Maybe (TypeNode, [Type])
toTypeNodeApp_maybe (HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe -> Just (TyCon
tyCon, [Type]
args))
  = (TypeNode, [Type]) -> Maybe (TypeNode, [Type])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyCon -> TypeNode
TyCon TyCon
tyCon, [Type]
args)
toTypeNodeApp_maybe tyLit :: Type
tyLit@(Type -> Maybe Integer
isNumLitTy -> Just Integer
_)
  = (TypeNode, [Type]) -> Maybe (TypeNode, [Type])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeEq -> TypeNode
TyLit (Type -> TypeEq
TypeEq Type
tyLit), [])
toTypeNodeApp_maybe tyLit :: Type
tyLit@(Type -> Maybe FastString
isStrLitTy -> Just FastString
_)
  = (TypeNode, [Type]) -> Maybe (TypeNode, [Type])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeEq -> TypeNode
TyLit (Type -> TypeEq
TypeEq Type
tyLit), [])
toTypeNodeApp_maybe Type
_
  = Maybe (TypeNode, [Type])
forall a. Maybe a
Nothing

fromTypeNode
  :: TypeNode
  -> [Type]
  -> Type
fromTypeNode :: TypeNode -> [Type] -> Type
fromTypeNode (TyCon TyCon
tyCon) [Type]
args = TyCon -> [Type] -> Type
mkTyConApp TyCon
tyCon [Type]
args
fromTypeNode (TyLit (TypeEq Type
tyLit)) [Type]
_ = Type
tyLit