{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
--
-- |
-- Module      : F2_Pretty
-- Authors     : Sean Seefried (http://www.cse.unsw.edu.au/~sseefried)
-- Copyright   : (c) 2007
-- License     : BSD3
-- Created     : 18 Jun 2007
--
module F2_Pretty
where

import F0_Alpha
import F1_Eval

-- This file is written in a more idiomatic style, eschewing the long
-- winded nature of the formal translation.

-- This type synonym is used to shorten contexts.
type PrettyCxt cxt = EvalD (PrettyD cxt)

class  ( Sat (PrettyCxt cxt  b)
       , Eval (PrettyD cxt) b) => Pretty cxt b where
  pretty :: P (PrettyCxt cxt) -> b -> String

data PrettyD cxt b =
  PrettyD { pretty' :: P (PrettyCxt cxt) -> b 
                    -> String 
          , prettyExt :: cxt b 
          }

instance Sat (PrettyCxt cxt (Exp (PrettyCxt cxt)))
         => Pretty cxt (Exp (PrettyCxt cxt)) where
  pretty (_::P (PrettyCxt cxt)) (MkExp e) =
          pretty' (evalExt dict) 
                  (u:: P (PrettyCxt cxt)) e

instance  ( Sat (PrettyCxt cxt (Exp   (PrettyCxt cxt)))
          , Sat (PrettyCxt cxt (Exp_0 (PrettyCxt cxt)))
          , Sat (PrettyCxt cxt (Exp_1 (PrettyCxt cxt)))
          ) => Pretty cxt (Exp_0 (PrettyCxt cxt)) where
    pretty (_::P (PrettyCxt cxt)) (Var v) = v
    pretty (_::P (PrettyCxt cxt)) (Lam v body) = 
       let p = u :: P (PrettyCxt cxt) 
           pretty'' = pretty' (evalExt dict)
       in  "\\" ++ v ++ " -> " ++ pretty'' p body
    pretty (_::P (PrettyCxt cxt)) (App a b) = 
        let p = u :: P (PrettyCxt cxt) 
            pretty'' = pretty' (evalExt dict) 
        in "App (" ++ pretty'' p a ++ ")(" ++ 
           pretty'' p b ++ ")" 

instance  ( Sat (PrettyCxt cxt (Exp   (PrettyCxt cxt)))
          , Sat (PrettyCxt cxt (Exp_0 (PrettyCxt cxt)))
          , Sat (PrettyCxt cxt (Exp_1 (PrettyCxt cxt)))
          ) => Pretty cxt (Exp_1 (PrettyCxt cxt)) where
    pretty (_::P (PrettyCxt cxt)) (LetE v body exp) = 
      let p = u :: P (PrettyCxt cxt)
          pretty'' = pretty' (evalExt dict)
      in "let " ++ v ++ " = " ++ pretty'' p body 
          ++ " in " ++ pretty'' p exp

data PrettyEnd b

class Pretty PrettyEnd b => PrettyCap b

instance PrettyCap (Exp    (PrettyCxt PrettyEnd))
instance PrettyCap (Exp_0  (PrettyCxt PrettyEnd))
instance PrettyCap (Exp_1  (PrettyCxt PrettyEnd))

instance PrettyCap b 
         => Sat (PrettyCxt PrettyEnd b) where
  dict = EvalD { eval'   = eval
               , apply'  = apply
               , evalExt = 
                   PrettyD { pretty'   = pretty
                           , prettyExt = 
                               error "Capped at Pretty" 
                           }
               }
        
ptest0, ptest1, ptest2, ptest3, ptest4, ptest5 :: Exp (PrettyCxt PrettyEnd)
ptest0 = test0
ptest1 = test1
ptest2 = test2
ptest3 = test3
ptest4 = test4
ptest5 = test5      

type ExpPretty = Exp (PrettyCxt PrettyEnd)
type EnvPretty = Env (PrettyCxt PrettyEnd)

peval :: ExpPretty -> EnvPretty -> ExpPretty
peval = eval (u:: P (PrettyCxt PrettyEnd))

ppretty :: Exp (PrettyCxt PrettyEnd) -> String
ppretty = pretty (u:: P (PrettyCxt PrettyEnd))

pNil :: EnvPretty
pNil = []