--------------------------------------------------------------------------------

{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -Wall -Wcompat
                -fwarn-incomplete-uni-patterns
                -fno-warn-type-defaults -fno-warn-missing-signatures #-}

import Control.Exception (Exception, catch, throw)
import Language.Haskell.TH

--------------------------------------------------------------------------------


-- Натуральные числа и списки
------------------------------

data Nat = Zero | Succ Nat
  deriving (Eq, Show)

fromInt :: Int -> Nat
fromInt 0 = Zero
fromInt n = Succ $ fromInt (n - 1)

toInt :: Nat -> Int
toInt Zero = 0
toInt (Succ n) = 1 + toInt n

plus :: Nat -> Nat -> Nat
plus Zero m = m
plus (Succ n) m = Succ (plus n m)


-- Реализуйте умножение натуральных чисел (не используя стандартные функции).

mult :: Nat -> Nat -> Nat
mult = (??)

tests_mult = test <$> [0 .. 50] <*> [0 .. 50]
 where
  test x y = toInt (fromInt x `mult` fromInt y) == x * y


-- Реализуйте вычитание натуральных чисел (не используя стандартные функции).
-- Если первое число меньше второго, возвращайте ноль.

minus :: Nat -> Nat -> Nat
minus = (??)

tests_minus = test <$> [0 .. 50] <*> [0 .. 50]
 where
  test x y =
    toInt (fromInt x `minus` fromInt y) == until (>=0) (const 0) (x - y)



data List a = Nil | Cons a (List a)
  deriving (Eq, Show)

fromMyList :: List a -> [a]
fromMyList Nil = []
fromMyList (Cons x xs) = x : fromMyList xs

toMyList :: [a] -> List a
toMyList [] = Nil
toMyList (x : xs) = Cons x $ toMyList xs


-- Реализуйте конкатенацию списков (не используя стандартные функции).

listConcat :: List a -> List a -> List a
listConcat = (??)

tests_listConcat =
  [ test [] ([] :: [Bool])
  , test [1,2,3] [4,5,6]
  , test "hello, " "world!"
  , take 5 (fromMyList $ toMyList [1,2,3] `listConcat` toMyList [4 ..]) == [1 .. 5]
  ]
 where
  test xs ys = fromMyList (toMyList xs `listConcat` toMyList ys) == xs ++ ys



-- Реализуйте функцию.
mapMaybe :: (a -> Maybe b) -> [a] -> [b]
mapMaybe = (??)

tests_mapMaybe =
  [ mapMaybe div2Even [1,2,3,6,15,16,4,5,8] == [1,3,8,2,4]
  ]
 where
  div2Even x
    | even x    = Just $ x `div` 2
    | otherwise = Nothing


-- На занятии мы реализовали очень плохую функцию `mFilter`.
-- Реализуйте очень хорошую.
-- (Подсказка: см. выше.)
mFilter :: [Maybe a] -> [a]
mFilter = (??)

tests_mFilter =
  [ mFilter [Just 1, Nothing, Just 3, Just 4, Nothing] == [1,3,4]
  , mFilter [Nothing, Just 'h', Nothing, Nothing, Just 'i', Nothing] == "hi"
  ]



-- Деревья
-----------

-- Творческое задание.
-- Определите сами тип бинарных деревьев, и реализуйте пару функций.
-- Тесты тоже придумайте сами ;).

data Tree a


height :: Tree a -> Integer
height = (??)

tests_height = (??)


size :: Tree a -> Integer
size = (??)

tests_size = (??)



-- Лямбда-исчисление
---------------------

type Variable = String

data Term
  = Var Variable
  | Lam Variable Term
  | Term :@: Term
  deriving (Eq)

instance Show Term where
  show (Var v) = v
  show (Lam v t) = "(\\" ++ v ++ "." ++ show t ++ ")"
  show (f :@: x) = "(" ++ show f ++ " " ++ show x ++ ")"

free :: Term -> [Variable]
free (Var v) = [v]
free (Lam v t) = filter (/= v) . free $ t
free (f :@: x) = free f ++ free x


-- Придумывает имя переменной, не встречающееся в `fs`.
-- (Если исходное имя там не встречается, то оставляет как есть.)
newVar :: Variable -> [Variable] -> Variable
newVar v fs = head . filter (not . (`elem` fs)) . iterate (++"'") $ v


-- Выполните подстановку m [v -> n].
subst :: Variable -> Term -> Term -> Term
subst v n m = (??)

tests_subst =
  [ subst "x" (Var "z") (Var "y") == Var "y"
  , subst "x" (Var "z") (Var "x") == Var "z"
  , subst "x" (Var "x") (Var "x") == Var "x"

  , subst "x" (Var "z") (Lam "x" $ Var "x") == (Lam "x" $ Var "x")
  , subst "x" (Var "z") (Lam "y" $ Var "x") == (Lam "y" $ Var "z")
  , subst "x" (Var "y") (Lam "y" $ Var "x") == (Lam "y'" $ Var "y")
  ]


-- Проверьте, что два терма альфа-эквивалентны.
alphaEq :: Term -> Term -> Bool
m `alphaEq` n = (??)

tests_alphaEq =
  [ Var "x" `alphaEq` Var "x"
  , not $ Var "x" `alphaEq` Var "x'"

  , (Lam "x" $ Var "x") `alphaEq` (Lam "y" $ Var "y")
  , not $ (Lam "x" $ Var "y") `alphaEq` (Lam "y" $ Var "y")
  , (Lam "x" $ Var "y") `alphaEq` (Lam "z" $ Var "y")

  , (termI :@: termK) `alphaEq` ((Lam "z" $ Var "z") :@: (Lam "u" $ Lam "v" $ Var "u"))
  , (termI :@: termK) `alphaEq` ((Lam "z" $ Var "z") :@: (Lam "x" $ Lam "y" $ Var "x"))
  , not $ (termI :@: termK) `alphaEq` ((Lam "z" $ Var "z") :@: (Lam "u" $ Lam "v" $ Var "x"))
  ]


-- Как вы знаете, есть несколько стратегий редукции. Но у них у всех одна суть:
-- каждая стратегия, руководствуясь каким-то своим принципом, выбирает в терме
-- один редекс и редуцирует его; и делает так до тех пор, пока редексов больше
-- не останется.

-- Принимает терм, выбирает редекс, редуцирует его, возвращает получившийся
-- новый терм. А если редексов не было, то, ну, возвращает ничего.
type ReductionStrategy = Term -> Maybe Term


-- «Нормальный» порядок редукции.
-- Редуцирует левый верхний редекс (т.е. на развилках всегда идет влево,
-- до тех пор, пока не наткнется на редекс).
-- Иными словами, вычиясляет самое верхнее применение функции, не вычисляя
-- предварительно её аргументы.
normalOrder :: ReductionStrategy
normalOrder = (??)

tests_normalOrder =
  [ normalOrder termI == Nothing
  , normalOrder termK == Nothing

  , normalOrder (termI :@: termK) == Just termK

  , normalOrder (termK :@: termI) == Just (Lam "b" termI)
  , normalOrder (termK :@: termLoop) == Just (Lam "b" termLoop)

  , normalOrder (termK :@: termI :@: termLoop) == Just (Lam "b" termI :@: termLoop)
  , normalOrder (termK :@: termLoop :@: termI) == Just (Lam "b" termLoop :@: termI)

  , normalOrder ((termI :@: termK) :@: (termI :@: termK))
      == Just (termK :@: (termI :@: termK))
  , normalOrder (Lam "z" (termI :@: termK) :@: (termI :@: termK))
      == Just (termI :@: termK)
  ]

-- «Аппликативный» порядок редукции.
-- Редуцирует левый нижний редекс (т.е. сначала редуцирует все редексы в
-- обоих детях (слева направо), а потом уже, возможно, саму вершину, если
-- в ней есть редекс).
-- Иными словами, сначала вычисляет аргументы функции, а потом уже
-- применяет функцию к аргументами.
applicativeOrder :: ReductionStrategy
applicativeOrder = (??)

tests_applicativeOrder =
  [ applicativeOrder termI == Nothing
  , applicativeOrder termK == Nothing

  , applicativeOrder (termI :@: termK) == Just termK

  , applicativeOrder (termK :@: termI) == Just (Lam "b" termI)
  , applicativeOrder (termK :@: (termI :@: termK)) == Just (termK :@: termK)

  , applicativeOrder ((termI :@: termK) :@: (termI :@: termK))
      == Just (termK :@: (termI :@: termK))
  , applicativeOrder ((termI :@: termK) :@: termK)
      == Just (termK :@: termK)
  , applicativeOrder (termI :@: (termI :@: termK) :@: (termI :@: termK))
      == Just (termI :@: termK :@: (termI :@: termK))
  , applicativeOrder (Lam "z" (termI :@: termK) :@: (termI :@: termK))
      == Just (Lam "z" (termI :@: termK) :@: termK)
  ]



-- Применяет указанную стратегию редукции, пока это возможно.
reduceUsing :: ReductionStrategy -> Term -> Term
reduceUsing = (??)

tests_reduceUsing =
  [ reduceUsing normalOrder (Var "x") == Var "x"
  , reduceUsing normalOrder termI == termI
  , reduceUsing normalOrder termK == termK

  , reduceUsing normalOrder (termK :@: termI :@: termLoop) == termI
  , reduceUsing normalOrder (termK' :@: termLoop :@: termK) == termK
  , reduceUsing normalOrder (termW :@: termI) == termI
  , reduceUsing normalOrder (termW :@: termK :@: termLoop) == termK
  , reduceUsing normalOrder (termW :@: termK' :@: term3) == term3
  ]


-- Проверка β-эквивалентности.
betaEq :: Term -> Term -> Bool
betaEq = (??)

tests_betaEq =
  [ termI `betaEq` termI
  , termI `betaEq` (Lam "z" $ Var "z")
  , (termK :@: termI :@: termLoop) `betaEq` termI
  , (termW :@: termI) `betaEq` termI
  , (termW :@: termK) `betaEq` (Lam "y" $ termK)
  , termK :@: termI `betaEq` termK'
  , not $ termK' :@: termI `betaEq` termK
  , termK' :@: termI `betaEq` termI
  , termK' :@: termLoop `betaEq` termI

  , (term1 :@: termI :@: termK) `betaEq` (term2 :@: termI :@: termK)
  , (term1 :@: termK :@: termI) `betaEq` (term2 :@: termI :@: termK)
  , (term1 :@: termK :@: termI) `betaEq` (term2 :@: termI :@: termK)
  , not $ (term1 :@: termK :@: termI) `betaEq` (term2 :@: termK :@: termI)

  , (term3 :@: termI :@: termK :@: termI :@: Var"_b") `betaEq` (term2 :@: termI :@: termK)
  ]
  ++ map not
  [ termI `betaEq` termK
  , termK `betaEq` termI
  , termK `betaEq` termK'
  , termI `betaEq` termK'
  ]


--------------------------------------------------------------------------------

-- Просто несколько термов для тестов и вам для экспериментов.

termI = Lam "x" $ Var "x"
termK = Lam "a" $ Lam "b" $ Var "a"
termK' = Lam "a" $ Lam "b" $ Var "b"
termB = Lam "f" $ Lam "g" $ Lam "x" $ Var "f" :@: (Var "g" :@: Var "x")
termS = Lam "f" $ Lam "g" $ Lam "x" $ Var "f" :@: Var "x" :@: (Var "g" :@: Var "x")
termW = Lam "x" (Var "x" :@: Var "x")
termLoop = termW :@: termW

term1 = Lam "a" $ Lam "b" $ Var "a" :@: (Var "b" :@: Var "_b")
term2 = Lam "a" $ Lam "b" $ (Var "a" :@: Var "b") :@: Var "_b"
term3 = Lam "a" $ Lam "b" $ Lam "c" $ Lam "d" $ (Var "a" :@: Var "b") :@: (Var "c" :@: Var "d")



------------------------------------ ~fin~ -------------------------------------


{- сюда смотреть не надо -}


data Skipped = Skipped
instance Exception Skipped where
instance Show Skipped where
  show Skipped = "skipped"

(??) = throw Skipped

ok_if_defined x = seq x True

main :: IO ()
main = sequence_ $ map (uncurry runTests) tests
  where
    tests =
      $(let
          tpref = "tests_"
          extractTestNames l
              = map (takeWhile (/= ' ') . snd)
              . filter ((== tpref) . fst)
              . map (splitAt (length tpref))
              . lines
            <$> runIO (readFile (loc_filename l))
          genTest n = tupE [stringE n, varE (mkName (tpref ++ n))]
        in map genTest <$> (location >>= extractTestNames) >>= listE
       )

    runTests :: String -> [Bool] -> IO ()
    runTests n ts = do
      putStr $ "Running tests " ++ show n ++ "... "
      catch (putStr $ if (and ts) then "OK" else "FAIL") (\e -> putStr . show $ (e :: Skipped))
      putStrLn ""