{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans -fno-warn-name-shadowing #-}

module Main where

import qualified Ivory.Language        as L
import           Ivory.Language        hiding (Struct, assert, true, false, proc)
import qualified Ivory.Language.Proc   as I
import qualified Ivory.Language.Syntax as I
import qualified Ivory.Stdlib          as L
import           Ivory.Compile.C.CmdlineFrontend

import           Control.Monad (when)
import           System.Directory
import           System.Exit
import           System.FilePath.Posix
import           System.IO
import           System.Process

import           Ivory.QuickCheck (checkWith,contract)

import           Text.Printf

import           Test.Tasty (TestTree,defaultMain,testGroup)
import           Test.Tasty.HUnit (assertBool,testCase)


main :: IO ()
main = defaultMain tests

tests :: TestTree
tests = testGroup "Tests" [ shouldPass, shouldFail ]

shouldPass :: TestTree
shouldPass = testGroup "should be safe"
             [ mkSuccess foo6 m6
             , mkSuccess foo7 m7
             , mkSuccess foo8 m8
             , mkSuccess foo9 m9
             , mkSuccess foo10 m10
             , mkSuccess foo11 m11
             , mkSuccess foo12 m12
             , mkSuccess foo13 m13
             , mkSuccess foo15 m15
             , mkSuccess foo17 m17
             , mkSuccess foo18 m18
             , mkSuccess foo19 m19
             , mkSuccess test_max mmax
             ]

shouldFail :: TestTree
shouldFail = testGroup "should be unsafe"
             [ mkFailure foo1 m1
             , mkFailure foo14 m14
             ]

mkSuccess :: Def (args ':-> res) -> Module -> TestTree
mkSuccess d@(~(I.DefProc p)) m = testCase (I.procSym p) $ do
  (o, r) <- quickCheck d m
  assertBool ("Expected quickcheck to pass: output:\n" ++ o) r

mkFailure :: Def (args ':-> res) -> Module -> TestTree
mkFailure d@(~(I.DefProc p)) m = testCase (I.procSym p) $ do
  (o, r) <- quickCheck d m
  assertBool ("Expected quickcheck to fail: output:\n" ++ o) (not r)


quickCheck :: Def (args ':-> res) -> Module -> IO (String, Bool)
quickCheck d@(~(I.DefProc p)) m = do
  tmpDir <- getTemporaryDirectory
  let testDir = tmpDir </> "ivory-quickcheck" </> I.procSym p
  b <- doesDirectoryExist testDir
  when b $ removeDirectoryRecursive testDir
  checkWith 100 (initialOpts { outDir = Just testDir }) [] m (contract d)
  let cmd = printf "(cd %s && cc -std=c99 -DIVORY_TEST *.c && ./a.out)" testDir
  (_,oh,eh,pid) <- runInteractiveCommand cmd
  code <- waitForProcess pid
  out <- hGetContents oh
  err <- hGetContents eh
  return (out ++ "\n" ++ err, code == ExitSuccess)

--------------------------------------------------------------------------------
-- test modules

foo1 :: Def ('[Ix 10, Ix 10] ':-> ())
foo1 = L.proc "foo1" $ \y x -> body $ do
  ifte_ (y <? 3)
    (do ifte_ (y ==? 3)
              (L.assert $ y ==? 0)
              retVoid)
    (do z <- assign x
        -- this *should* fail
        L.assert (z >=? 3))
  retVoid

m1 :: Module
m1 = package "foo1" (incl foo1)

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

foo6 :: Def ('[Uint8] ':-> ())
foo6 = L.proc "foo6" $ \x -> body $ do
  y <- local (ival (0 :: Uint8))
  ifte_ (x <? 3)
        (do a <- local (ival (9 :: Uint8))
            b <- deref a
            store y b
        )
        (do a <- local (ival (7 :: Uint8))
            b <- deref a
            store y b
        )
  z <- deref y
  L.assert (z <=? 9)
  L.assert (z >=? 7)

m6 :: Module
m6 = package "foo6" (incl foo6)

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

foo7 :: Def ('[Uint8, Uint8] ':-> Uint8)
foo7 = L.proc "foo7" $ \x y ->
       requires (x + y <=? 255)
     $ body $ do
         ret (x + y)

m7 :: Module
m7 = package "foo7" (incl foo7)

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

foo8 :: Def ('[Uint8] ':-> Uint8)
foo8 = L.proc "foo8" $ \x -> body $ do
  let y = x .% 3
  L.assert (y <? 4)
  ret y

m8 :: Module
m8 = package "foo8" (incl foo8)

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

[ivory|
struct foo2
{ aFoo :: Stored Uint8
; bFoo :: (Array 4 Uint8)
}
|]

foo9 :: Def ('[Ref s ('L.Struct "foo2")] ':-> ())
foo9 = L.proc "foo9" $ \f -> body $ do
  st <- local (istruct [aFoo .= ival 0])
  a  <- deref (st ~> aFoo)
  L.assert (a ==? 0)
  store (f ~> aFoo) 3
  store (f ~> bFoo ! 0) 1
  store (f ~> aFoo) 4
  x <- deref (f ~> aFoo)
  y <- deref (f ~> bFoo ! 0)
  L.assert (x ==? 4 L..&& y ==? 1)

m9 :: Module
m9 = package "foo9" $ do
  defStruct (Proxy :: Proxy "foo2")
  incl foo9

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

foo10 :: Def ('[Uint8] ':-> Uint8)
foo10 = L.proc "foo10" $ \x ->
        requires (x <? 10)
      $ ensures (\r -> r ==? x + 1)
      $ body $ do
        r <- assign $ x + 1
        ret r

m10 :: Module
m10 = package "foo10" (incl foo10)

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

foo11 :: Def ('[Ix 10] ':-> ())
foo11 = L.proc "foo11" $ \n ->
          requires (n >=? 0)
        $ body $ do
          x <- local (ival (0 :: Sint8))
          0 `upTo` n $ \i -> do
            x' <- deref x
            store x $ x' + safeCast i

m11 :: Module
m11 = package "foo11" (incl foo11)

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

foo12 :: Def ('[Uint8] ':-> Uint8)
foo12 = L.proc "foo12" $ \n ->
        ensures (\r -> r ==? n)
      $ body $ do
          ifte_ (n ==? 0)
            (ret n)
            (do n' <- L.call foo12 (n-1)
                ret (n' + 1))

m12 :: Module
m12 = package "foo12" (incl foo12)

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

foo13 :: Def ('[Uint8, Uint8] ':-> Uint8)
foo13 = L.proc "foo13" $ \x y ->
        requires (x <=? 15)
      $ requires (y <=? 15)
      $ body $ ret (x * y)

m13 :: Module
m13 = package "foo13" (incl foo13)

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

foo14 :: Def ('[Uint8, Uint8] ':-> Uint8)
foo14 = L.proc "foo14" $ \x y ->
        ensures (\r -> r >=? x L..&& r >=? y) $
        body $ ret (x * y)

m14 :: Module
m14 = package "foo14" (incl foo14)

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

foo15 :: Def ('[Ix 10] ':-> Uint8)
foo15 = L.proc "foo15" $ \n ->
    requires (n >=? 0)
  $ ensures (\r -> r <=? 5)
  $ body $ do
    n `downTo` 0 $ \i -> do
      ifte_ (i >? 5) (ret 5) (ret $ safeCast i)
    ret 4 -- FIXME: Ivory.Opts.TypeCheck doesn't see above `ret`s

m15 :: Module
m15 = package "foo15" (incl foo15)

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

foo17 :: Def ('[ Ref 'Global ('Array 10 ('Stored Uint32))] ':-> ())
foo17 = L.proc "foo17" $ \a -> body $ do
  b <- local (iarray [ival 0, ival 1])
  refCopy b a
  arrayMap (\ix -> store (a ! (ix :: Ix 10)) 1)
  retVoid

m17 :: Module
m17 = package "foo17" (incl foo17)

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

foo18 :: Def ('[Ref s ('L.Struct "foo2")] ':-> Ref s ('L.Struct "foo2"))
foo18 = L.proc "foo18" $ \f ->
    requires (checkStored (f ~> aFoo) (\a -> a >? 0))
  $ requires (checkStored (f ~> aFoo) (\a -> a <? 10))
  $ ensures (\r -> checkStored (r ~> aFoo) (\a -> a >? 1))
  $ body $ do
    a <- deref (f ~> aFoo)
    L.assert (a >? 0)

    store (f ~> aFoo) (a + 1)
    ret f

m18 :: Module
m18 = package "foo18" $ do
  defStruct (Proxy :: Proxy "foo2")
  incl foo18

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

ppm_valid_area :: MemArea ('Stored IBool)
ppm_valid_area = area "ppm_valid" Nothing

foo19 :: Def('[Ref s ('Array 1 ('Stored Uint32))] ':-> ())
foo19 = L.proc "foo19" $ \ppms -> body $ do
  all_good <- local (ival L.true)
  ppm_last <- local (iarray [])
  let ppm_valid = addrOf ppm_valid_area
  arrayMap $ \ix -> do
    x <- deref (ppms ! ix)
    L.unless (x >=? 800 L..&& x <=? 2000)
      (store all_good L.false)

  b <- deref all_good
  L.unless b (store ppm_valid L.false)
  L.when b $ do
    (arrayMap $ \ix -> (deref (ppms ! ix) >>= store (ppm_last ! ix)))
    store ppm_valid L.true
  
  valid <- deref ppm_valid
  ppm <- deref (ppm_last ! 0)
  L.assert (L.iNot valid .|| (ppm >=? 800 L..&& ppm <=? 2000))
  retVoid

m19 :: Module
m19 = package "foo19" $ do
  defMemArea ppm_valid_area
  incl foo19

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

[ivory|
int32_t test_max(int32_t a, int32_t b) {
  return (a > b) ? a : b;
}
{
  post(return >= a && return >= b);
  post(return == a || return == b);
}
|]

mmax :: Module
mmax = package "max" (incl test_max)