{- |
  TODO: Use real pretty printer library
-}
{-# LANGUAGE OverloadedStrings #-}
module LambdaCube.SystemFw.PrettyPrinter
  ( prettyUnnamedTerm
  , prettyShowUnnamedTerm
  , prettyUnnamedType
  , prettyShowUnnamedType
  , prettyUnnamedKind
  , prettyShowUnnamedKind
  ) where

import           Data.Text                       (Text)
import qualified Data.Text                       as Text
import           LambdaCube.Common.PrettyPrinter
import           LambdaCube.SystemFw.Ast

prettyUnnamedTerm :: LCTerm -> Text
prettyUnnamedTerm :: LCTerm -> Text
prettyUnnamedTerm = Int -> LCTerm -> Text
prettyUnnamedTermPrec Int
0

prettyShowUnnamedTerm :: LCTerm -> String
prettyShowUnnamedTerm :: LCTerm -> String
prettyShowUnnamedTerm = Text -> String
Text.unpack (Text -> String) -> (LCTerm -> Text) -> LCTerm -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LCTerm -> Text
prettyUnnamedTerm

prettyUnnamedType :: LCType -> Text
prettyUnnamedType :: LCType -> Text
prettyUnnamedType = Int -> LCType -> Text
prettyUnnamedTypePrec Int
0

prettyShowUnnamedType :: LCType -> String
prettyShowUnnamedType :: LCType -> String
prettyShowUnnamedType = Text -> String
Text.unpack (Text -> String) -> (LCType -> Text) -> LCType -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LCType -> Text
prettyUnnamedType

prettyUnnamedKind :: LCKind -> Text
prettyUnnamedKind :: LCKind -> Text
prettyUnnamedKind = Int -> LCKind -> Text
prettyUnnamedKindPrec Int
0

prettyShowUnnamedKind :: LCKind -> String
prettyShowUnnamedKind :: LCKind -> String
prettyShowUnnamedKind = Text -> String
Text.unpack (Text -> String) -> (LCKind -> Text) -> LCKind -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LCKind -> Text
prettyUnnamedKind

prettyUnnamedTermPrec :: Int -> LCTerm -> Text
prettyUnnamedTermPrec :: Int -> LCTerm -> Text
prettyUnnamedTermPrec = Int -> LCTerm -> Text
forall t. (Ord t, Num t) => t -> LCTerm -> Text
go
  where
    pKP :: Int -> LCKind -> Text
pKP = Int -> LCKind -> Text
prettyUnnamedKindPrec
    pTP :: Int -> LCType -> Text
pTP = Int -> LCType -> Text
prettyUnnamedTypePrec

    go :: t -> LCTerm -> Text
go t
_ (LCVar Int
i)    = String -> Text
Text.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
i
    go t
p (LCLam LCType
t LCTerm
b)  = Bool -> [Text] -> Text
wrapIfSpaced (t
p t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
0) [Text
"\\ :", Int -> LCType -> Text
pTP Int
0 LCType
t, Text
".", t -> LCTerm -> Text
go t
0 LCTerm
b]
    go t
p (LCApp LCTerm
f LCTerm
a)  = Bool -> [Text] -> Text
wrapIfSpaced (t
p t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
1) [t -> LCTerm -> Text
go t
1 LCTerm
f, t -> LCTerm -> Text
go t
2 LCTerm
a]
    go t
p (LCTLam LCKind
k LCTerm
b) = Bool -> [Text] -> Text
wrapIfSpaced (t
p t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
0) [Text
"@\\ :", Int -> LCKind -> Text
pKP Int
0 LCKind
k, Text
".", t -> LCTerm -> Text
go t
0 LCTerm
b]
    go t
p (LCTApp LCTerm
f LCType
t) = Bool -> [Text] -> Text
wrapIfSpaced (t
p t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
1) [t -> LCTerm -> Text
go t
1 LCTerm
f, Text
"@" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> LCType -> Text
pTP Int
1 LCType
t]

prettyUnnamedTypePrec :: Int -> LCType -> Text
prettyUnnamedTypePrec :: Int -> LCType -> Text
prettyUnnamedTypePrec = Int -> LCType -> Text
forall t. (Ord t, Num t) => t -> LCType -> Text
go
  where
    pKP :: Int -> LCKind -> Text
pKP = Int -> LCKind -> Text
prettyUnnamedKindPrec

    go :: t -> LCType -> Text
go t
_ LCType
LCBase        = Text
"#"
    go t
_ (LCTVar Int
i)    = String -> Text
Text.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
i
    go t
p (LCArr LCType
a LCType
b)   = Bool -> [Text] -> Text
wrapIfSpaced (t
p t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
0) [t -> LCType -> Text
go t
1 LCType
a, Text
"->", t -> LCType -> Text
go t
0 LCType
b]
    go t
p (LCUniv LCKind
k LCType
b)  = Bool -> [Text] -> Text
wrapIfSpaced (t
p t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
0) [Text
"! :", Int -> LCKind -> Text
pKP Int
0 LCKind
k, Text
",", t -> LCType -> Text
go t
0 LCType
b]
    go t
p (LCTTLam LCKind
k LCType
b) = Bool -> [Text] -> Text
wrapIfSpaced (t
p t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
0) [Text
"\\ :", Int -> LCKind -> Text
pKP Int
0 LCKind
k, Text
".", t -> LCType -> Text
go t
0 LCType
b]
    go t
p (LCTTApp LCType
f LCType
a) = Bool -> [Text] -> Text
wrapIfSpaced (t
p t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
1) [t -> LCType -> Text
go t
1 LCType
f, t -> LCType -> Text
go t
2 LCType
a]

prettyUnnamedKindPrec :: Int -> LCKind -> Text
prettyUnnamedKindPrec :: Int -> LCKind -> Text
prettyUnnamedKindPrec = Int -> LCKind -> Text
forall t. (Ord t, Num t) => t -> LCKind -> Text
go
  where
    go :: t -> LCKind -> Text
go t
_ LCKind
LCStar       = Text
"*"
    go t
p (LCKArr LCKind
a LCKind
b) = Bool -> [Text] -> Text
wrapIfSpaced (t
p t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
0) [t -> LCKind -> Text
go t
1 LCKind
a, Text
"->", t -> LCKind -> Text
go t
0 LCKind
b]