{-# LANGUAGE
  TypeOperators
, FlexibleContexts #-}

module Render.Simple where

import Calculus.Connectives.Simple
import Calculus.Connectives.Linear
import Calculus.Expr

import Auxiliary.List

import Control.Monad.State
import Data.List


type UniqNames = String
initUniqNames = ['a'..'z']

type NameSupply a = State UniqNames a

freshName :: NameSupply Char
freshName = do xs <- get
               put $ tail xs
               return $ head xs


{- Simple rendering to String -}

class Render f where
  -- not realy need state for list of names.
  -- but I may use this type later with better
  -- unique names set.
  render :: Render g => f (Expr g) -> NameSupply String

instance (Render f, Render g) => Render (f :+: g) where
  render (Inl f) = render f
  render (Inr f) = render f

pretty :: Render f => Expr f -> String
pretty f = evalState (render $ out f) initUniqNames  --render . out

{- Connectives rendering -}

binOpRender f g op =
  do lft <- render (out f)
     rht <- render (out g)
     return $ "(" ++ lft ++ op ++ rht ++ ")"

instance Render SimConj where
  render (SimConj f g) = binOpRender f g " & "

instance Render AltConj where
  render (AltConj f g) = binOpRender f g " $ "

instance Render Disj where
  render (Disj f g)    = binOpRender f g " | "

instance Render ResImpl where
  render (ResImpl f g) = binOpRender f g " -> "

instance Render ValImpl where
  render (ValImpl f g) = binOpRender f g " => "

instance Render Unit where
  render Unit = return "1"

instance Render Top where
  render Top = return "T"
  
instance Render Zero where
  render Zero = return "0"

instance Render Modal where
  render (Modal f) = do inner <- (render $ out f)
                        return $ "!" ++ inner
  
{- Base rendering -}

showArgs :: [Term] -> String
showArgs = between "(" ")" . intercalate ", " . map showTerm    

showTerm (Func name [])   = name
showTerm (Func name args) = name ++ showArgs args
showTerm (Var name)       = "Var " ++ name

instance Render Atom where
  render (Atom name args) = return $ name ++ showArgs args
  
-- quantifiers

instance Render Exists where
  render (Exists f) = 
    do uniq <- freshName
       let var = Var [uniq]
       body <- render (out $ f var)
       return $ "Exists " ++ showTerm var ++ " . " ++ "[" ++ body ++ "]"
  
instance Render ForAll where
  render (ForAll f) =
    do uniq <- freshName
       let var = Var [uniq]
       body <- render (out $ f var)
       return $ "ForAll " ++ showTerm var ++ " . " ++ "[" ++ body ++ "]"

