{-# LANGUAGE LambdaCase, ViewPatterns #-}
module TypeLevel.Rewrite.Internal.TypeTerm where

-- GHC API
import Type (Type, mkTyConApp)

-- term-rewriting API
import Data.Rewriting.Term (Term(Fun, Var))

import TypeLevel.Rewrite.Internal.TypeEq
import TypeLevel.Rewrite.Internal.TypeNode


type TypeTerm = Term TypeNode TypeEq

toTypeTerm
  :: Type -> TypeTerm
toTypeTerm :: Type -> TypeTerm
toTypeTerm (Type -> Maybe (TypeNode, [Type])
toTypeNodeApp_maybe -> Just (TypeNode
tyNode, [Type]
args))
  = TypeNode -> [TypeTerm] -> TypeTerm
forall f v. f -> [Term f v] -> Term f v
Fun TypeNode
tyNode ((Type -> TypeTerm) -> [Type] -> [TypeTerm]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> TypeTerm
toTypeTerm [Type]
args)
toTypeTerm Type
tp
  = TypeEq -> TypeTerm
forall f v. v -> Term f v
Var (Type -> TypeEq
TypeEq Type
tp)

fromTypeTerm
  :: TypeTerm -> Type
fromTypeTerm :: TypeTerm -> Type
fromTypeTerm = \case
  Var TypeEq
x
    -> TypeEq -> Type
unTypeEq TypeEq
x
  Fun (TyCon TyCon
tyCon) [TypeTerm]
args
    -> TyCon -> [Type] -> Type
mkTyConApp TyCon
tyCon ((TypeTerm -> Type) -> [TypeTerm] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeTerm -> Type
fromTypeTerm [TypeTerm]
args)
  Fun (TyLit (TypeEq Type
tyLit)) []
    -> Type
tyLit
  Fun (TyLit TypeEq
_) [TypeTerm]
_
    -> [Char] -> Type
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible: TyLit doesn't have any arguments"