content: module Main where
  
  
  import TypesTerms
  import Preds
  import Syntax
  import PrettyPrint
  import TFFMonad
  
  import System(getArgs)
  
  
  --------------------------------------------------------------------------------
  -- Tests
  --
  
  free f@(Exp (HsId (HsVar n)) , t) = do
      { putStrLn $ "Theorem for: " ++ pp f
      ; putStrLn . pp . run $ getRel t f f
      }
  
  
  
  a = mkTyVar (UnQual "a")
  b = mkTyVar (UnQual "b")
  c = mkTyVar (UnQual "c")
  
  tint = mkTyCon (UnQual "Int")
  tchar = mkTyCon (UnQual "Char")
  
  (+->) = mkTyFun
  
  fall n t = mkTyAll (UnQual n) t
  
  mkVar = hsEVar . UnQual
  
  t0 = free (mkVar "one", tint)
  t1_0 = free (mkVar "succ", (tint +-> tint))
  t1 = free (mkVar "succN", (tint +-> tchar +-> tchar))
  t2 = free (mkVar "bottom", (fall "a" a))
  t3 = free (mkVar "const1", (fall "a" (a +-> tint)))
  t4 = free (mkVar "cast",   (fall "a" (fall "b" (a +-> b))))
  t5 = free (mkVar "const",   (fall "a" (fall "b" (a +-> (b +-> a)))))
  
  tsts = [t0, t1_0, t1, t2, t3, t4, t5]
  
  
  main = do
      a:args <- getArgs
      let x = (read a) :: Int
      tsts !! x
      return ()
  
  
  
  --
  --------------------------------------------------------------------------------
  
  
  