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

import Data.List (intercalate)

-- GHC API
import Outputable (ppr, showSDocUnsafe)
import TyCon (TyCon)
import Type (TyVar, Type)

-- 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 :: (a -> String) -> Maybe a -> String
pprMaybe a -> String
pprA = \case
  Maybe a
Nothing
    -> String
"Nothing"
  Just a
a
    -> String
"Just ("
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
pprA a
a
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

pprPair
  :: (a -> String)
  -> (b -> String)
  -> (a, b)
  -> String
pprPair :: (a -> String) -> (b -> String) -> (a, b) -> String
pprPair a -> String
pprA b -> String
pprB (a
a, b
b)
  = String
"("
 String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
pprA a
a
 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", "
 String -> String -> String
forall a. [a] -> [a] -> [a]
++ b -> String
pprB b
b
 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

pprList
  :: (a -> String)
  -> [a]
  -> String
pprList :: (a -> String) -> [a] -> String
pprList a -> String
pprA
  = (String
"[" String -> String -> String
forall a. [a] -> [a] -> [a]
++)
  (String -> String) -> ([a] -> String) -> [a] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]")
  (String -> String) -> ([a] -> String) -> [a] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", "
  ([String] -> String) -> ([a] -> [String]) -> [a] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> String) -> [a] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> String
pprA


pprTyCon
  :: TyCon -> String
pprTyCon :: TyCon -> String
pprTyCon
  = SDoc -> String
showSDocUnsafe (SDoc -> String) -> (TyCon -> SDoc) -> TyCon -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr

pprType
  :: Type -> String
pprType :: Type -> String
pprType
  = SDoc -> String
showSDocUnsafe (SDoc -> String) -> (Type -> SDoc) -> Type -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr

pprTyVar
  :: TyVar -> String
pprTyVar :: TyVar -> String
pprTyVar
  = SDoc -> String
showSDocUnsafe (SDoc -> String) -> (TyVar -> SDoc) -> TyVar -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr


pprTypeEq
  :: TypeEq -> String
pprTypeEq :: TypeEq -> String
pprTypeEq
  = Type -> String
pprType (Type -> String) -> (TypeEq -> Type) -> TypeEq -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeEq -> Type
unTypeEq


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

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

pprReduct
  :: (f -> String)
  -> (v -> String)
  -> (v' -> String)
  -> Reduct f v v'
  -> String
pprReduct :: (f -> String)
-> (v -> String) -> (v' -> String) -> Reduct f v v' -> String
pprReduct f -> String
pprF v -> String
pprV v' -> String
pprV' (Reduct {Pos
Term f v
Rule f v'
GSubst v' f v
subst :: forall f v v'. Reduct f v v' -> GSubst v' f v
rule :: forall f v v'. Reduct f v v' -> Rule f v'
result :: forall f v v'. Reduct f v v' -> Term f v
pos :: forall f v v'. Reduct f v v' -> Pos
subst :: GSubst v' f v
rule :: Rule f v'
pos :: Pos
result :: Term f v
..})
  = String
"Reduct "
 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"{ result = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (f -> String) -> (v -> String) -> Term f v -> String
forall f v. (f -> String) -> (v -> String) -> Term f v -> String
pprTerm f -> String
pprF v -> String
pprV Term f v
result
 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", pos = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Pos -> String
forall a. Show a => a -> String
show Pos
pos
 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", rule = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (f -> String) -> (v' -> String) -> Rule f v' -> String
forall f v. (f -> String) -> (v -> String) -> Rule f v -> String
pprRule f -> String
pprF v' -> String
pprV' Rule f v'
rule
 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", subst = undefined"
 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"


pprTypeNode
  :: TypeNode -> String
pprTypeNode :: TypeNode -> String
pprTypeNode = \case
  TyCon TyCon
tyCon
    -> String
"TyCon ("
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ TyCon -> String
pprTyCon TyCon
tyCon
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
  TyLit TypeEq
tyLit
    -> String
"TyLit ("
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeEq -> String
pprTypeEq TypeEq
tyLit
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

pprTypeSubst
  :: TypeSubst -> String
pprTypeSubst :: TypeSubst -> String
pprTypeSubst
  = ((TypeEq, TypeTerm) -> String) -> TypeSubst -> String
forall a. (a -> String) -> [a] -> String
pprList (((TypeEq, TypeTerm) -> String) -> TypeSubst -> String)
-> ((TypeEq, TypeTerm) -> String) -> TypeSubst -> String
forall a b. (a -> b) -> a -> b
$ (TypeEq -> String)
-> (TypeTerm -> String) -> (TypeEq, TypeTerm) -> String
forall a b. (a -> String) -> (b -> String) -> (a, b) -> String
pprPair TypeEq -> String
pprTypeEq TypeTerm -> String
pprTypeTerm

pprTypeTemplate
  :: TypeTemplate -> String
pprTypeTemplate :: TypeTemplate -> String
pprTypeTemplate
  = (TypeNode -> String) -> (TyVar -> String) -> TypeTemplate -> String
forall f v. (f -> String) -> (v -> String) -> Term f v -> String
pprTerm TypeNode -> String
pprTypeNode TyVar -> String
pprTyVar

pprTypeTerm
  :: TypeTerm -> String
pprTypeTerm :: TypeTerm -> String
pprTypeTerm
  = (TypeNode -> String) -> (TypeEq -> String) -> TypeTerm -> String
forall f v. (f -> String) -> (v -> String) -> Term f v -> String
pprTerm TypeNode -> String
pprTypeNode TypeEq -> String
pprTypeEq

pprTypeRule
  :: TypeRule -> String
pprTypeRule :: TypeRule -> String
pprTypeRule
  = (TypeNode -> String) -> (TyVar -> String) -> TypeRule -> String
forall f v. (f -> String) -> (v -> String) -> Rule f v -> String
pprRule TypeNode -> String
pprTypeNode TyVar -> String
pprTyVar

pprTypeReduct
  :: Reduct TyCon TypeEq TyVar -> String
pprTypeReduct :: Reduct TyCon TypeEq TyVar -> String
pprTypeReduct
  = (TyCon -> String)
-> (TypeEq -> String)
-> (TyVar -> String)
-> Reduct TyCon TypeEq TyVar
-> String
forall f v v'.
(f -> String)
-> (v -> String) -> (v' -> String) -> Reduct f v v' -> String
pprReduct TyCon -> String
pprTyCon TypeEq -> String
pprTypeEq TyVar -> String
pprTyVar