{-# OPTIONS_GHC -fno-warn-missing-methods #-}

{-# LANGUAGE DeriveAnyClass  #-}
{-# LANGUAGE DeriveGeneric   #-}
{-# LANGUAGE BlockArguments  #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | Represents the extended natural numbers in the solver
module Language.Granule.Checker.Constraints.SNatX where

-- import Control.Monad ((<=<))
import Data.SBV
import GHC.Generics (Generic)

newtype SNatX = SNatX { xVal  :: SInteger }
  deriving (Generic, Mergeable)

instance Show SNatX where
  show (SNatX val) = case unliteral val of
    Just (-1) -> "∞"
    Just n    -> show n
    _         -> "<symbolic>"

inf :: SNatX
inf = SNatX $ (literal (-1))

isInf :: SNatX -> SBool
isInf (SNatX n) = n .== -1

instance Num SNatX where
  x + y = ite (isInf x .|| isInf y)
              inf
              (SNatX (xVal x + xVal y))
  x * y = ite ((isInf x .&& y ./= 0) .|| (isInf y .&& x ./= 0)) -- 0 * ∞ = ∞ * 0 = 0
              inf
              (SNatX (xVal x * xVal y))
  x - y = ite (isInf x .|| isInf y)  -- ???
              inf
              (ite (x .< y)          -- monus
                   0
                   (SNatX (xVal x - xVal y)))
  fromInteger = SNatX . literal

instance EqSymbolic SNatX where
  (SNatX a) .== (SNatX b) = a .== b

instance OrdSymbolic SNatX where
  a .< b = ite (isInf b) (ite (isInf a) sFalse sTrue)
         $ ite (isInf a) sFalse
         $ xVal a .< xVal b

representationConstraint :: SInteger -> SBool
representationConstraint v = v .>= -1

freeSNatX :: String -> Symbolic SNatX
freeSNatX nm = do
  v <- sInteger $ nm <> "_xVal"
  constrain $ representationConstraint v
  return $ SNatX v

existsSNatX :: String -> Symbolic SNatX
existsSNatX nm = do
  v <- exists $ nm <> "_xVal"
  constrain $ representationConstraint v
  return $ SNatX v

forallSNatX :: String -> Symbolic SNatX
forallSNatX nm = do
  v <- forall $ nm <> "_xVal"
  constrain $ representationConstraint v
  return $ SNatX v

-- main :: IO ()
-- main = print =<< sat do
--   [x, y, z] <- mapM freeSNatX ["x", "y", "z"]
--   return $ sAnd
--     [ x .== x+1 -- x = ∞
--     , x .== x*y -- y ≠ 0
--     , y .< x    -- y ≠ ∞
--     , z*x .== 0 -- z = 0
--     ]

-- main :: IO ()
-- main = print =<< prove do
--   -- [x, y, z] <- mapM freeSNatX ["x", "y", "z"]
--   y <- existsSNatX_
--   z <- forallSNatX_
--   return $ z .<= y

-- data NatX = NatX (Maybe Integer) deriving Show
--
-- queryNatX :: SNatX -> Query NatX
-- queryNatX (SNatX {isInf, xVal}) = do
--   b <- getValue isInf
--   v <- getValue xVal
--   return $ NatX if b then Nothing else Just v

-- main :: IO ()
-- main = runSMT do
--   [x, y, z] <- mapM freeSNatX ["x", "y", "z"]
--   constrain $ sAnd
--     [ x .== x*y -- x must be 0 or oo, if x |-> oo, then y can't be 0
--     , y .< x    -- nothing smaller than 0, so x |-> oo, and y > 0
--     , z*x .== 0 -- what times oo is 0? z |-> 0
--     ]
--   query do
--     cs <- checkSat
--     case cs of
--       Unk   -> error "Solver said Unknown!"
--       Unsat -> error "Solver said Unsatisfiable!"
--       Sat   -> do
--         mapM_ (io . print <=< queryNatX) [x, y, z]
