{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
module Expr.Test where

import Control.Monad (Monad(..), when)
import Data.Bool
import Data.Functor.Identity (Identity(..))
import Data.Either (Either(..))
import Data.Function (($), (.))
import Data.Functor ((<$>))
import Data.Traversable (Traversable(..))
import Data.Maybe (Maybe(..))
import Data.Eq (Eq(..))
-- import Data.Tuple (fst, snd)
import qualified Data.Foldable as Foldable
import qualified Data.List as List
-- import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Monoid (Monoid(..), (<>))
import Test.Tasty
import Test.Tasty.HUnit
-- import Test.HUnit hiding (test)
import System.IO (IO)
-- import Data.Sequence (Seq)
import Data.Text (Text)
-- import Control.Monad.Trans.Class (lift)
-- import qualified Data.Text    as Text
import qualified Data.Text.IO as Text
import Text.Show (Show(..))
import Prelude (error)
-- import Debug.Trace

import qualified Language.LOL.Calculus as Calc
import qualified Language.LOL.Calculus.Read as Calc
import Language.LOL.Typing
-- import qualified Language.LOL.Typing.Collect.Grammar as Collect
import Language.LOL.Typing.Expr.Calculus
import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build
import Solver.Test (polytys_env, infer)
-- import Solver.Test (write_log, Collect_Constraints(..), Infer_Polytype(..))

tests :: TestTree
tests = testGroup "Expr"
 [ tests_Calculus
 ]

type Test_Solver
 =   Solver_Greedy_Finite Collect_Infos IO

class Calcify a where
	calcify
	 :: Bool -> a
	 -> IO (Either (Collect_Error (Info Test_Solver)
	                              (Error Test_Solver))
	               (Calc.Term TeTy_Var))
instance Calcify Expr where
	calcify logging expr = do
		ty <- infer logging expr
		case ty of
		 Left err -> return $ Left err
		 Right Solver_Result
			 { solver_result_monotypes   = monosub
			 , solver_result_polytypes   = polysub
			 , solver_result_quantifiers = quants
			 } -> do
			let monoty = monosub `substitute` Monotype_Var 0
			let foralls = subvars monoty
			let consts = Map.unions
				 ( (Map.fromList $ (, ()) <$> List.take (List.length foralls) const_pool)
				 : ((\(name, polyty) -> Map.insert name () $ monoconsts polyty) <$> polytys_env) )
			let Syn_Expr
				 { term_Syn_Expr = term
				 } = wrap_Expr (sem_Expr expr) Inh_Expr
				 { env_Inh_Expr         = mempty
				 , freshvar_Inh_Expr    = 0
				 , monoconsts_Inh_Expr  = consts
				 , monotys_Inh_Expr     = monosub
				 , polytys_Inh_Expr     = (monosub `substitute`) <$> polysub
				 , quantifiers_Inh_Expr = (monosub `substitute`) . (Monotype_Var <$>) <$> quants
				 , renames_Inh_Expr     = mempty
				 }
			return $ Right $
				Foldable.foldr
				 (\(quant, const) ->
					Calc.Term_Abst (Calc.Suggest const)
					 (Calc.Type_Sort Calc.sort_star_mono) .
					((\v -> case v of
						 TeTy_Var_Monovar m | m == quant -> Just (Calc.Suggest const)
						 _ -> Nothing) `Calc.abstract`))
				 term
				 (List.zip foralls const_pool)
instance Calcify Decl where
	calcify logging decl = do
		ty <- infer logging decl
		case ty of
		 Left err -> return $ Left err
		 Right Solver_Result
			 { solver_result_monotypes   = monosub
			 , solver_result_polytypes   = polysub
			 , solver_result_quantifiers = quants
			 } -> do
			let monoty  = monosub `substitute` Monotype_Var 1 -- NOTE: decl.freshvar
			let foralls = subvars monoty
			let consts = Map.unions
				 ( (Map.fromList $ (, ()) <$> List.take (List.length foralls) const_pool)
				 : ((\(name, polyty) -> Map.insert name () $ monoconsts polyty) <$> polytys_env) )
			let Syn_Decl
				 { term_Syn_Decl = term
				 } = wrap_Decl (sem_Decl decl) Inh_Decl
				 { env_Inh_Decl         = mempty
				 , freshvar_Inh_Decl    = 0
				 , monoconsts_Inh_Decl  = consts
				 , monotys_Inh_Decl     = monosub
				 , polytys_Inh_Decl     = (monosub `substitute`) <$> polysub
				 , quantifiers_Inh_Decl = (monosub `substitute`) . (Monotype_Var <$>) <$> quants
				 , renames_Inh_Decl     = mempty
				 }
			return $ Right $
				Foldable.foldr
				 (\(quant, const) ->
					Calc.Term_Abst (Calc.Suggest const)
					 (Calc.Type_Sort Calc.sort_star_mono) .
					((\v -> case v of
						 TeTy_Var_Monovar m | m == quant -> Just (Calc.Suggest const)
						 _ -> Nothing) `Calc.abstract`))
				 term
				 (List.zip foralls const_pool)

calc_monovar_close :: Calc.Term TeTy_Var -> Either Monovar (Calc.Term Calc.Var_Name)
calc_monovar_close te =
	traverse go te
	where
		go (TeTy_Var_Monovar v) = Left v
		go (TeTy_Var_Name n) = Right n

tests_Calculus :: TestTree
tests_Calculus = testGroup "Calculus" $
	let test logging input (expected::Text) = do
		when logging $
			Text.putStrLn ("expr: " <> Build.text input)
		let expect_term =
			case runIdentity $ Calc.read Calc.parse_term expected of
			 Left err -> error $ show err
			 Right x -> x
		got_either_term <- calcify logging input
		case got_either_term of
		 got@(Left _) -> got @?= Right (TeTy_Var_Name <$> expect_term)
		 Right got_term ->
			case calc_monovar_close got_term of
			 Left m -> Left ("Monovar remains in term: " <> show m) @?= Right expect_term
			 got -> do
				when logging $ do
					Text.putStrLn ("exp: " <> Build.text expect_term)
					case got of
					 Right ex -> Text.putStrLn ("got: " <> Build.text ex)
					 _ -> return ()
				got @?= Right expect_term in
	let (==>) = test False in
	-- let (==>>) = test True in
 [ testGroup "Expr" $
	 [ testCase "id" $ ("x".-> "x")
	    ==> "λ(a:*) (x:a) -> x"
	 , testCase "id_Int" $ (("x","Int")..-> "x")
	    ==> "λ(x:Int) -> x"
	 , testCase "id_Int" $ ("x".-> ("x".:("Int"::Monotype)))
	    ==> "λ(x:Int) -> x"
	 , testCase "twice" $ ("f".-> "x".-> "f"!("f"!"x"))
	    ==> "λ(a:*) (f:a -> a) (x:a) -> f (f x)"
	 , testCase "const" $ ("x".-> "y".-> "x")
	    ==> "λ(a:*) (b:*) (x:a) (y:b) -> x"
	 , testCase "compose" $ ("f".-> "g".-> "x".-> "f"!("g"!"x"))
	    ==> "λ(a:*) (b:*) (c:*) (f:a -> b) (g:c -> a) (x:c) -> f (g x)"
	 , testCase "equal" $ ("x".-> "f".= "x" $ "f")
	    ==> "λ(a:*) (x:a) -> (λ(f:a) -> f) x"
	 , testCase "equal" $ ("x".-> "f".= ("y".->"x") $ "pair"!("f"!"True")!("f"!"one") )
	    ==> "λ(a:*) (x:a) -> (λ(f:∀(b:*) -> b -> a) -> pair a a (f Bool True) (f Int one)) (λ(b:*) (y:b) -> x)"
	 {-
	 , testCase "equal" $ ("x".-> "f".= ("y".->"x") $ "equal"!("f"!"True")!("f"!"one") )
	    ==> "λ(a:*) (x:a) -> (λ(f:∀(b:*) -> b -> a) -> equal a (f Bool True) (f Int one)) (λ(b:*) (y:b) -> x)"
	 -}
	 ]
 , testGroup "Decl" $
	 [ testCase "equal" $ Decl_Let Nothing "test"
		("x".-> "f".= ("y".-> "x") $ "equal"!("f"!"True")!("f"!"one") )
	    ==> "λ(a:*) (x:a) -> (λ(f:∀(b:*) -> b -> a) -> equal a (f Bool True) (f Int one)) (λ(b:*) (y:b) -> x)"
	 -- , testCase "Abst rename" $ Decl_Let Nothing "test" ("Bool".-> "f".= ("y".-> "Bool") $ "equal"!("f"!"True")!("f"!"one") )
	 --    ==> "λ(a:*) (x:a) -> (λ(f:∀(b:*) -> b -> a) -> equal a (f Bool True) (f Int one)) (λ(b:*) (y:b) -> x)"
	 -- , testCase "Let rename" $ Decl_Let Nothing "test" ("x".-> "Int".= ("y".-> "x") $ "equal"!("Int"!"True")!("Int"!"one") )
	 --    ==> "λ(a:*) (x:a) -> (λ(f:∀(b:*) -> b -> a) -> equal a (f Bool True) (f Int one)) (λ(b:*) (y:b) -> x)"
	 -- , testCase "equal" $ Decl_Let Nothing "test" ("x".-> "f".= ("y".-> "g".= ("z".->"y") $ "g"!"x") $ "equal"!("f"!"True")!("f"!"True") )
	 --    ==>> "λ(a:*) (x:a) -> (λ(f:∀(b:*) -> b -> b) -> equal Bool (f Bool True) (f Bool True)) (λ(b:*) (y:b) -> (λ(g:∀(c:*) -> c -> b) -> g a x) (λ(c:*) (z:c) -> y))"
	 ]
 ]