content: {-# 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)
  