-- terpret.hs: Benchmark execution-model problems from TerpreT
--
-- Copyright (C) 2021 Rudy Matela
-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
--
-- You can find the description of these exercises on:
--
-- 1. https://dl.acm.org/doi/pdf/10.1145/3067695.3082533
-- 2. https://www.microsoft.com/en-us/research/uploads/prod/2017/03/1608.04428.pdf
--
-- Here, we prefer the simplified definitions found in 1.
import Conjure
import System.Environment (getArgs)


-- TerpreT #1 -- invert --

t1p :: [Bool] -> [Bool]
t1p [False]  =  [True]
t1p [True]   =  [False]
t1p [False,True]  =  [True,False]
t1p [True,False]  =  [False,True]

t1g :: [Bool] -> [Bool]
t1g ps  =  map not ps

t1c :: IO ()
t1c  =  do
  putStrLn "TerpreT benchmark #1: invert\n"

  conjure "invert" t1p primitives123

-- the same primitives are used for TerpreT #1, #2 and #3
primitives123 :: [Prim]
primitives123  =
  [ pr False
  , pr True
  , prim "not" not
  , prim "&&" (&&)
  , prim "||" (||)
  , pr ([] :: [Bool])
  , prim ":" ((:) :: Bool -> [Bool] -> [Bool])
--, prim "map" (map :: (Bool -> Bool) -> [Bool] -> [Bool])
  , prif (undefined :: [Bool])
  ]


-- TerpreT #2 -- prepend zero --
t2p :: [Bool] -> [Bool]
t2p [True]  =  [False,True]
t2p [False]  =  [False,False]
t2p [True,True]  =  [False,True,True]

t2g :: [Bool] -> [Bool]
t2g ps  =  False:ps

t2c :: IO ()
t2c  =  do
  putStrLn "TerpreT benchmark #2: prepend zero\n"

  conjure "prependZero" t2p primitives123


-- TerpreT #3 -- binary decrement --
-- here we choose to represent with little-endian notation

t3p :: [Bool] -> [Bool]
-- t3p [True]  =  [False]
t3p [True,True]  =  [False,True]             -- 3-1=2
t3p [False,True]  =  [True,False]            -- 2-1=1
t3p [False,True,True]  =  [True,False,True]  -- 6-1=5

t3g :: [Bool] -> [Bool]
t3g []  =  []
t3g (p:ps)  =  if p
               then False : ps
               else True : t3g ps
-- hah!  Conjure surprised me again:
-- decrement []  =  []
-- decrement (p:ps)  =  not p:(if p then ps else decrement ps)

t3c :: IO ()
t3c  =  do
  putStrLn "TerpreT benchmark #3: binary decrement\n"

  conjure "decrement" t3p primitives123


-- TerpreT #4 -- 2-bit controlled shift register --

t4p1 :: (Bool,Bool,Bool) -> (Bool,Bool,Bool)
t4p1 (False, True, False)  =  (False, True, False)
t4p1 (False, False, True)  =  (False, False, True)
t4p1 (True, True, False)  =  (True, False, True)
t4p1 (True, False, True)  =  (True, True, False)

t4p2 :: Bool -> Bool -> Bool -> (Bool,Bool,Bool)
t4p2 False  True   False   =  (False, True, False)
t4p2 False  False  True    =  (False, False, True)
t4p2 True   True   False   =  (True, False, True)
t4p2 True   False  True    =  (True, True, False)

t4g :: (Bool,Bool,Bool) -> (Bool,Bool,Bool)
t4g (False,p,q)  =  (False,p,q)
t4g (True,p,q)  =  (True,q,p)

t4c :: IO ()
t4c  =  do
  putStrLn "TerpreT benchmark #4: controlled shift\n"

  conjure "cshift" t4p1 $ primitives123 ++
    [ prim ",," ((,,) :: Bool -> Bool -> Bool -> (Bool,Bool,Bool))
    , prif (undefined :: (Bool,Bool,Bool))
    ]

  conjure "cshift" t4p2 $ primitives123 ++
    [ prim ",," ((,,) :: Bool -> Bool -> Bool -> (Bool,Bool,Bool))
    , prif (undefined :: (Bool,Bool,Bool))
    ]


-- TerpreT #5 -- Full adder --

t5p :: Bool -> Bool -> Bool -> (Bool,Bool)
t5p False False False  =  (False,False)
t5p False False True   =  (False,True )
t5p False True  False  =  (False,True )
t5p True  False False  =  (False,True )
t5p False True  True   =  (True ,False)
t5p True  False True   =  (True ,False)
t5p True  True  False  =  (True ,False)
t5p True  True  True   =  (True ,True )

t5c :: IO ()
t5c  =  do
  putStrLn "TerpreT benchmark #5: full adder\n"

  -- using primitives123 below works, but increases the runtime to 18 seconds
  -- let's leave it commented out so runtime is faster when running automated tests
  -- BENCHMARK: uncomment primitives123
  conjure "fadder" t5p $ -- primitives123 ++
    [ prim "not" not
    , prim "," ((,) :: Bool -> Bool -> (Bool,Bool))
    , prim "==" ((==) :: Bool -> Bool -> Bool)
--  , prim "^^" ((/=) :: Bool -> Bool -> Bool) -- poor man's xor
    , prif (undefined :: (Bool,Bool))
    ]
-- the printed function is weird, but correct
-- fadder p q r  =  if p == q then (p,r) else (r,not r)


-- TerpreT #6 -- 2-bit adder --
t6p :: (Bool,Bool) -> (Bool,Bool) -> (Bool,Bool,Bool)
t6p (False,False) (False,False)  =  (False,False,False)
t6p (True ,False) (False,True )  =  (False,True ,True )
t6p (True ,True ) (False,True )  =  (True ,False,False)
t6p (True ,True ) (True ,False)  =  (True ,False,True )
t6p (True ,True ) (True ,True )  =  (True ,True ,False)

t6c :: IO ()
t6c  =  do
  putStrLn "TerpreT benchmark #6: 2-bit adder\n"
  conjureWith args{maxSize=6} "adder2" t6p $ primitives123 ++
    [ prim ",," ((,,) :: Bool -> Bool -> Bool -> (Bool,Bool,Bool))
    , prim "==" ((==) :: Bool -> Bool -> Bool)
    , prim "^^" ((/=) :: Bool -> Bool -> Bool) -- poor man's xor
    , prif (undefined :: (Bool,Bool,Bool))
    ]


-- TerpreT #7 -- Access --
t7p :: [A] -> Int -> A
t7p [1,0] 0  =  1
t7p [1,0] 1  =  0
t7p [0,2,1]  0  =  0
t7p [0,2,1]  1  =  2
t7p [0,2,1]  2  =  1

t7g :: [A] -> Int -> A
t7g [] _  =  undefined
t7g (x:xs) 0  =  x
t7g (x:xs) i  =  t7g xs (i-1)

t7c :: IO ()
t7c  =  do
  putStrLn "TerpreT benchmark #7: access\n"
  -- yes, one can implement index with index...
  conjure "`access`" t7p
    [ prim "!!" ((!!) :: [A] -> Int -> A)
    ]

  conjure "`access`" t7p
    [ pr (0 :: Int)
    , pr (1 :: Int)
    , pr ([] :: [A])
    , prim ":" ((:) :: A -> [A] -> [A])
    , prim "-" ((-) :: Int -> Int -> Int)
    , prim "undefined" (undefined :: A)
    ]


-- TerpreT #8 -- Decrement Elements --
t8p :: [Int] -> [Int]
t8p [2]  =  [1]
t8p [1,0]  =  [0,-1]
t8p [0,1,2]  =  [-1,0,1]

t8c :: IO ()
t8c  =  do
  putStrLn "TerpreT benchmark #8: decrement elements\n"

  conjure "decrelements" t8p
    [ pr (1 :: Int)
    , pr ([] :: [Int])
    , prim ":" ((:) :: Int -> [Int] -> [Int])
    , prim "-" ((-) :: Int -> Int -> Int)
    , prim "map" (map :: (Int -> Int) -> [Int] -> [Int])
    ]
  -- above, even though map is provided, Conjure cannot use it as it cannot
  -- introduce lambdas

  conjure "decrelements" t8p
    [ pr (1 :: Int)
    , pr ([] :: [Int])
    , prim ":" ((:) :: Int -> [Int] -> [Int])
    , prim "-" ((-) :: Int -> Int -> Int)
    , prim "map" (map :: (Int -> Int) -> [Int] -> [Int])
    , prim "subtract" (subtract :: Int -> Int -> Int)
    ]
  -- now above, the story changes because of subtract, map is used


main :: IO ()
main  =  do
  as <- getArgs
  case as of
    [] -> sequence_ ts
    (n:_) -> ts !! (read n - 1)


ts :: [IO ()]
ts  =  [ t1c
       , t2c
       , t3c
       , t4c
       , t5c
       , t6c
       , t7c
       , t8c
       ]