{-# LANGUAGE FlexibleContexts #-}
module Printer where

import Syntax
import Text.Printf

class Pretty a where
  pretty :: a -> String

instance Pretty Base where
  pretty = printBase

instance Pretty Type where
  pretty = printType False

instance Pretty Term where
  pretty = printTerm False

instance Pretty Constant where
  pretty = printConstant False

-- Print AST ------------------------------------------------------------------

parens :: (PrintfType (t -> t)) => Bool -> t -> t
parens b s = if b then printf "(%s)" s else s

printBase :: Base -> String
printBase BInt  = "Int"
printBase BBool = "Bool"

printType :: Bool -> Type -> String
printType atom t = case t of
  Fun vname vtype rtype -> parens atom $ printf "%s: %s -> %s" vname vts rts
    where
      vts = printType True vtype
      rts = printType True rtype

--  Ref vname btype (Con Ctrue) -> printBase btype

  Ref vname btype term -> printf "{%s: %s | %s}" vname (pretty btype)
                                                       (pretty term)

printTerm :: Bool -> Term -> String
printTerm atom te = case te of

  Var vname -> vname

  Con c -> printConstant atom c

  Lam vname vtype term -> printf "(\\%s: %s . %s)" vname (pretty vtype) tes
    where tes = printTerm True term

  App te1 te2 -> parens atom $ printf "%s %s" te1s te2s
    where
      te1s = printTerm True te1
      te2s = printTerm True te2

  Cast t1 t2 term -> printf "<%s |> %s> %s" t1s t2s tes
    where
      t1s = pretty t1
      t2s = pretty t2
      tes = printTerm True term

printConstant :: Bool -> Constant -> String
printConstant atom c = case c of
  Ctrue    -> "true"
  Cfalse   -> "false"
  Cimpl    -> "<=>"
  Cimplb b -> parens atom $ printf "<=># %s" (if b then "true" else "false")
  Cnot     -> "not"
  Cint n   -> show n
  Cplus    -> "+"
  Cdiv     -> "/"
  Cplusn n -> parens atom $ printf "+# %s" (show n)
  Cdivn  n -> parens atom $ printf "/# %s" (show n)
  Ceq      -> "="
  Ceqn n   -> parens atom $ printf "=# %s" (show n)
  Cif t    -> printf "if [%s]" (pretty t)
  Cfix t   -> printf "fix [%s]" (pretty t)