import Types
import Subst
import Expr

import TypesPrelude


addt = "(+)" =: int ->: int ->: int
inct = "inc" =: int ->: int
dect = "dec" =: int ->: int

lista = "as" =: list a
listb = "bs" =: list b

(.:) :: Expr -> Expr -> Expr
e1 .: e2 = (t'dot $: e1) $: e2
infixr 3 .:


test = t'map .: t'cons

test2 = t'map -: t'cons $: "[(:)]" =: list (a ->: list a ->: list a)


test3 = t'append -: lista -: listb


workout :: Expr -> IO ()
workout e = do
  let e' = normalize . localize $ e
  let (Bind (Binding fn ft)) = reduceAll e'
  putStrLn $ "Expression: " ++ fn
  putStrLn ""

  putStrLn "Bindings (with original type variables):"
  mapM_ print $ bindings e
  putStrLn ""

  putStrLn "Bindings (with unique type variables):"
  mapM_ print $ bindings e'
  putStrLn ""

  step e' 1


step :: Expr -> Int -> IO ()
step e i = do
  case reduce e of
    Nothing -> do
       let (Bind (Binding fnn fnt)) = normalize e
       putStrLn $ "Final type:"
       putStrLn $ "  " ++ fnn ++ " :: " ++ show fnt
       return ()

    Just r@(Reduction b1@(Binding n1 t1) b2@(Binding n2 t2) subst br) -> do
       let e' = replaceRed e r
       putStrLn $ "Step #" ++ show i ++ ":"
       putStrLn $ "  " ++ n1 ++ " " ++ n2 ++ " :: " ++ show t1 ++ " `applied to` " ++ show t2
       mapM_ (\(v, t) -> putStrLn $ "    Substution: " ++ v ++ " ~> " ++ show t) subst
       putStrLn $ "  " ++ show br
       putStrLn ""
       step e' (i+1)


main = workout test3