module Main where

import qualified Data.Map.Strict as Map

import Types ( TermInContext, Type(Arrow, BaseType), emptyContext )
import Terms ( Term(..) )
import TypeInference ( inferType )

-- some base types
int :: Type
int = BaseType "int"
string :: Type
string = BaseType "string"

-- ThProg: sheet 07, exercise 2, 1.
term1 :: Term
term1 = Abs "x" $ Abs "y" $ Abs "z" $ App (Var "x") (App (Var "y") (Var "z"))
exercise1 :: Maybe TermInContext
exercise1 = inferType emptyContext term1

-- ThProg: sheet 07, exercise 2, 2.
term2 :: Term
term2 = Abs "x" $ App (Var "add") (App (Var "length") (Var "x"))
exercise2 :: Maybe TermInContext
exercise2 = inferType (Map.fromList [("add", Arrow int (Arrow int int)), ("length", Arrow string int)]) term2

omega :: Term
omega = Abs "x" $ App (Var "x") (Var "x")

main :: IO ()
main = do 
    print exercise1
    print exercise2

    putStrLn "Trying to type '\\x.xx' in empty context:"
    print $ inferType emptyContext omega