{- |
  TODO: Use real pretty printer library
-}
{-# LANGUAGE OverloadedStrings #-}
module LambdaCube.SystemFw_.PrettyPrinter where

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

prettyKind :: LCKind -> Text
prettyKind = prettyKindPrec 0

prettyType :: LCType -> Text
prettyType = prettyTypePrec 0

prettyTerm :: LCTerm -> Text
prettyTerm = prettyTermPrec 0

prettyKindPrec :: Int -> LCKind -> Text
prettyKindPrec = go
  where
    go _ LCStar       = "*"
    go p (LCKArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]

prettyTypePrec :: Int -> LCType -> Text
prettyTypePrec = go
  where
    pKP = prettyKindPrec

    go _ LCBase        = "#"
    go _ (LCTVar i)    = Text.pack $ show i
    go p (LCArr a b)   = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]
    go p (LCTTLam k b) = wrapIfSpaced (p > 0) ["\\ :", pKP 0 k, ".", go 0 b]
    go p (LCTTApp f a) = wrapIfSpaced (p > 1) [go 1 f, go 2 a]

prettyTermPrec :: Int -> LCTerm -> Text
prettyTermPrec = go
  where
    pTP = prettyTypePrec

    go _ (LCVar i)   = Text.pack $ show i
    go p (LCLam t b) = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]
    go p (LCApp f a) = wrapIfSpaced (p > 1) [go 1 f, go 2 a]