{-# LANGUAGE LambdaCase, ViewPatterns #-}
module TypeLevel.Rewrite.Internal.TypeTerm where
import TyCon (TyCon)
import Type (Type, mkTyConApp, splitTyConApp_maybe)
import Data.Rewriting.Term (Term(Fun, Var))
import TypeLevel.Rewrite.Internal.TypeEq
type TypeTerm = Term TyCon TypeEq
toTypeTerm
:: Type -> TypeTerm
toTypeTerm (splitTyConApp_maybe -> Just (tyCon, args))
= Fun tyCon (fmap toTypeTerm args)
toTypeTerm tp
= Var (TypeEq tp)
fromTypeTerm
:: TypeTerm -> Type
fromTypeTerm = \case
Var x
-> unTypeEq x
Fun tyCon args
-> mkTyConApp tyCon (fmap fromTypeTerm args)