PrettyPrint.hs

{-# LANGUAGE CPP, LambdaCase, RecordWildCards #-}
module TypeLevel.Rewrite.Internal.PrettyPrint where

import Data.List (intercalate)

-- GHC API
#if MIN_VERSION_ghc(9,0,0)
import GHC.Utils.Outputable (ppr, showSDocUnsafe)
import GHC.Plugins (TyCon)
import GHC.Plugins (TyVar, Type)
#else
import Outputable (ppr, showSDocUnsafe)
import TyCon (TyCon)
import Type (TyVar, Type)
#endif

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

import TypeLevel.Rewrite.Internal.TypeEq
import TypeLevel.Rewrite.Internal.TypeNode
import TypeLevel.Rewrite.Internal.TypeRule
import TypeLevel.Rewrite.Internal.TypeSubst
import TypeLevel.Rewrite.Internal.TypeTemplate
import TypeLevel.Rewrite.Internal.TypeTerm


pprMaybe
  :: (a -> String)
  -> Maybe a
  -> String
pprMaybe pprA = \case
  Nothing
    -> "Nothing"
  Just a
    -> "Just ("
    ++ pprA a
    ++ ")"

pprPair
  :: (a -> String)
  -> (b -> String)
  -> (a, b)
  -> String
pprPair pprA pprB (a, b)
  = "("
 ++ pprA a
 ++ ", "
 ++ pprB b
 ++ ")"

pprList
  :: (a -> String)
  -> [a]
  -> String
pprList pprA
  = ("[" ++)
  . (++ "]")
  . intercalate ", "
  . fmap pprA


pprTyCon
  :: TyCon -> String
pprTyCon
  = showSDocUnsafe . ppr

pprType
  :: Type -> String
pprType
  = showSDocUnsafe . ppr

pprTyVar
  :: TyVar -> String
pprTyVar
  = showSDocUnsafe . ppr


pprTypeEq
  :: TypeEq -> String
pprTypeEq
  = pprType . unTypeEq


pprTerm
  :: (f -> String)
  -> (v -> String)
  -> Term f v
  -> String
pprTerm pprF pprV = \case
  Var v
    -> pprV v
  Fun f args
    -> pprF f
    ++ " "
    ++ pprList (pprTerm pprF pprV) args

pprRule
  :: (f -> String)
  -> (v -> String)
  -> Rule f v
  -> String
pprRule pprF pprV (Rule {..})
  = "Rule "
 ++ "{ lhs = " ++ pprTerm pprF pprV lhs
 ++ ", rhs = " ++ pprTerm pprF pprV rhs
 ++ "}"

pprReduct
  :: (f -> String)
  -> (v -> String)
  -> (v' -> String)
  -> Reduct f v v'
  -> String
pprReduct pprF pprV pprV' (Reduct {..})
  = "Reduct "
 ++ "{ result = " ++ pprTerm pprF pprV result
 ++ ", pos = " ++ show pos
 ++ ", rule = " ++ pprRule pprF pprV' rule
 ++ ", subst = undefined"
 ++ "}"


pprTypeNode
  :: TypeNode -> String
pprTypeNode = \case
  TyCon tyCon
    -> "TyCon ("
    ++ pprTyCon tyCon
    ++ ")"
  TyLit tyLit
    -> "TyLit ("
    ++ pprTypeEq tyLit
    ++ ")"

pprTypeSubst
  :: TypeSubst -> String
pprTypeSubst
  = pprList $ pprPair pprTypeEq pprTypeTerm

pprTypeTemplate
  :: TypeTemplate -> String
pprTypeTemplate
  = pprTerm pprTypeNode pprTyVar

pprTypeTerm
  :: TypeTerm -> String
pprTypeTerm
  = pprTerm pprTypeNode pprTypeEq

pprTypeRule
  :: TypeRule -> String
pprTypeRule
  = pprRule pprTypeNode pprTyVar

pprTypeReduct
  :: Reduct TyCon TypeEq TyVar -> String
pprTypeReduct
  = pprReduct pprTyCon pprTypeEq pprTyVar