-- Copyright 2022 University of Freiburg
-- Janek Spaderna <janek.spaderna@pluto.uni-freiburg.de>
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE TemplateHaskell #-}

module Main where

import Control.Monad (when)
import System.IO
import Test.QuickCheck

main :: IO ()
main = go []
  where
    go :: Stack -> IO ()
    go stack = do
      putStr "> "
      -- Flush stdout before we read the next command.
      hFlush stdout
      cmd <- getLine
      -- When the command is not "exit" we evaluate it and call `go` recursively.
      when (cmd /= "exit") do
        let stack' = readCommand cmd stack
        print stack'
        go stack'

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

type Stack = [Integer]

type StackOp = Stack -> Stack

push :: Integer -> StackOp --   ≡ Integer -> [Integer] -> [Integer]
push i stack = i : stack

pop :: StackOp --   ≡ [Integer] -> [Integer]
pop [] = []
pop (_ : rest) = rest

dup :: StackOp --   ≡ [Integer] -> [Integer]
dup [] = [0]
dup (top : rest) = top : top : rest

add :: StackOp --   ≡ [Integer] -> [Integer]
add (x : y : rest) = (x + y) : rest
-- Instead of the single clause below we can give two clauses
--    add []  = add []
--    add [x] = add [x]   (since x+0 == x, infinitely many zeros below x)
-- but both just return their argument.
add stack = stack

sub :: StackOp --   ≡ [Integer] -> [Integer]
sub (x : y : rest) = (x - y) : rest
sub stack = stack

neg :: StackOp --   ≡ [Integer] -> [Integer]
-- Explicit alternative version:
--    neg [] = []
--    neg (x : rest) = negate x : rest
neg stack = sub (push 0 stack)

mul :: StackOp --   ≡ [Integer] -> [Integer]
mul (x : y : rest) = (x * y) : rest
mul [_] = [0] -- important since x*0 == 0, [0] is possible as well
mul [] = []

prop_push_top :: Integer -> Stack -> Bool
prop_push_top n stack = head (push n stack) == n

prop_push_tail :: Integer -> Stack -> Bool
prop_push_tail n stack = tail (push n stack) == stack

prop_dup_add_is_mul_2 :: Stack -> Bool
prop_dup_add_is_mul_2 stack = add (dup stack) == mul (push 2 stack)

prop_mul_minus1_is_neg :: Stack -> Bool
prop_mul_minus1_is_neg stack = mul (push (-1) stack) == neg stack

readCommand :: String -> StackOp --   ≡ String -> [Integer] -> [Integer]
readCommand ('p' : 'u' : 's' : 'h' : ' ' : s) = push (read s)
readCommand "add" = add
readCommand "subtract" = sub
readCommand "multiply" = mul
readCommand "negate" = neg
readCommand "dup" = dup
readCommand "pop" = pop
readCommand _ = id -- identity function, like `readCommand _ stack = stack`

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

return []

checkAll :: IO Bool
checkAll = $quickCheckAll