\begin{code}
module Main (main) where

import Syntax (Type(..), Func(..), Term(..), etaReduce)
import Parser (parse)
import Generate (mono, apply)
import Show ()

import System.IO


sigma :: Type
sigma = (Alpha `To` Bool) `To` ((Bool `To` Alpha) `To` (List Alpha `To` Alpha))

main :: IO ()
main = do
  hSetBuffering stdout NoBuffering
  putStr $ "function type (or Enter for default): "
  sigma <- getLine >>= \s -> return $ if s=="" then sigma else parse s
  putStrLn ""
  putStrLn $ "f :: " ++ show sigma
  putStrLn $ replicate 66 '-'
  putStrLn $ "e = " ++ show (mono sigma (Embed "pre") (Embed "post")) ++ " f"
  putStrLn $ replicate 66 '-'
  let  lhs = mono sigma Id (Embed (Var "g")) `apply` Const "f"
       rhs = mono sigma (Embed (Var "g")) Id `apply` Const "f"
  putStrLn $ "free theorem:"
  putStrLn $ " " ++ show lhs
  putStrLn "  ="
  putStrLn $ " " ++ show rhs
  putStrLn $ replicate 66 '-'
  putStrLn $ "free theorem, eta-reduced:"
  putStrLn $ " " ++ show (etaReduce lhs)
  putStrLn "  ="
  putStrLn $ " " ++ show (etaReduce rhs)
  putStrLn ""
\end{code}