\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 "------------------------------------------------------------------"
           putStrLn $ "e = " ++ show (mono sigma (Embed "pre") (Embed "post")) ++ " f"
           putStrLn "------------------------------------------------------------------"
           putStrLn $ "free theorem:"
           putStrLn $ " " ++ show (mono sigma Id (Embed (Var "g")) `apply` Const "f")
           putStrLn "  ="
           putStrLn $ " " ++ show (mono sigma (Embed (Var "g")) Id `apply` Const "f")
           putStrLn "------------------------------------------------------------------"
           putStrLn $ "free theorem, eta-reduced:"
           putStrLn $ " " ++ show (etaReduce (mono sigma Id (Embed (Var "g")) `apply` Const "f"))
           putStrLn "  ="
           putStrLn $ " " ++ show (etaReduce (mono sigma (Embed (Var "g")) Id `apply` Const "f"))
           putStrLn ""
\end{code}