{-# LANGUAGE PatternSynonyms   #-}
{-# HLINT ignore "Use camelCase" #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QualifiedDo       #-}

module TestLambdaLifter where

import           Test.Hspec

import           AnnForall                    (annotateForall)
import           Control.Monad                ((<=<))
import           Control.Monad.Error.Class    (liftEither)
import           Control.Monad.Extra          (eitherM)
import           Grammar.ErrM                 (Err, pattern Bad, pattern Ok)
import           Grammar.Layout               (resolveLayout)
import           Grammar.Par                  (myLexer, pProgram)
import           Grammar.Print                (printTree)
import           LambdaLifter
import           Renamer.Renamer              (rename)
import           ReportForall                 (reportForall)
import           TypeChecker.RemoveForall     (removeForall)
import           TypeChecker.ReportTEVar      (reportTEVar)
import           TypeChecker.TypeChecker      (TypeChecker (Bi))
import           TypeChecker.TypeCheckerBidir (typecheck)
import           TypeChecker.TypeCheckerIr


test = hspec testLambdaLifter

testLambdaLifter = describe "Test Lambda Lifter" $ do
    undefined
--  frees_exp1

-- frees_exp1 = specify "Free variables 1" $
--     freeVarsExp [] (EAbs "x" (EVar "x", TVar' "a"), TVar' "a")
--     `shouldBe` answer
--   where
--     answer = Ann { frees = []
--                  , term = (AAbs (Ident "x") (Ann { frees = [Ident "x"]
--                                                  , term = (AVar (Ident "x"),TVar (MkTVar (Ident "a")))
--                                                  }
--                                             ),TVar (MkTVar (Ident "a")))
--                  }


abs_1 = undefined
  where
    input = unlines [ "data List (a) where"
                    , "    Nil  : List (a)"
                    , "    Cons : a -> List (a) -> List (a)"
                    , "map : (a -> b) -> List (a) -> List (b)"
                    , "add : Int -> Int -> Int"

                    , "f : List (Int)"
                    , "f = (\\x.\\ys. map (\\y. add y x) ys) 4 (Cons 1 (Cons 2 Nil))"
                    ]



runFreeVars = either putStrLn print (runFree s2)
runAbstract = either putStrLn (putStrLn . printTree) (runAbs s2)
runCollect = either putStrLn (putStrLn . printTree) (run s2)


s1 = unlines [ "add : Int -> Int -> Int"
             , "f : Int -> Int -> Int"
             , "f x y = add x y"
             , "f = \\x. (\\y. add x y)"
             ]

s2 = unlines [ "data List (a) where"
             , "    Nil  : List (a)"
             , "    Cons : a -> List (a) -> List (a)"
             , "add : Int -> Int -> Int"
             , "map : (a -> b) -> List (a) -> List (b)"
          -- , "map f xs = case xs of"
          -- , "    Nil       => Nil"
          -- , "    Cons x xs => Cons (f x) (map f xs)"

             , "f : List (Int)"
             , "f = (\\x.\\ys. map (\\y. add y x) ys) 4 (Cons 1 (Cons 2 Nil))"
             ]

s3 = "main = (\\plussq. (\\f. f (f 0)) (plussq 3)) (\\x. \\y. y + x + x)"



run = fmap collectScs . runAbs

runAbs = fmap abstract . runFree

runFree s = do
  Program ds <- run' s
  pure $ freeVars [b | DBind b <- ds]

run' =   fmap removeForall
      . reportTEVar
    <=< typecheck
    <=< run''

run'' s = do
    p <- (pProgram . resolveLayout True . myLexer) s
    reportForall Bi p
    (rename <=< annotateForall) p