{-# language Rank2Types #-}
{-# language ScopedTypeVariables #-}
{-# language DataKinds #-}
{-# language TypeOperators #-}
{-# language TypeFamilies #-}
{-# language FlexibleInstances #-}
{-# language FlexibleContexts #-}
{-# language MultiParamTypeClasses #-}
{-# language PolyKinds #-}
{-# language GADTs #-}
{-# language ConstraintKinds #-}
{-# language GeneralizedNewtypeDeriving #-}

module Feldspar.Software.Verify.Primitive where

import Feldspar.Sugar
import Feldspar.Representation
import Feldspar.Software.Primitive
import Feldspar.Software.Expression
import Feldspar.Software.Representation hiding (Nil)
import Feldspar.Software.Verify.Command
import Feldspar.Verify.Arithmetic

import Feldspar.Verify.Monad (Verify)
import qualified Feldspar.Verify.FirstOrder as FO
import qualified Feldspar.Verify.Monad as V
import qualified Feldspar.Verify.SMT as SMT
import qualified Feldspar.Verify.Abstract as A

import Data.Struct
import qualified Data.Map.Strict as Map

import qualified Control.Monad.RWS.Strict as S

import qualified SimpleSMT as SMT hiding (not, declareFun)

import qualified Language.Embedded.Expression as Imp
import qualified Language.Embedded.Imperative.CMD as Imp

import qualified Data.Bits as Bits
import qualified Data.Complex as Complex
import Data.Constraint hiding (Sub)
import Data.Int
import Data.Word
import Data.Typeable

import Language.Syntactic

import GHC.Stack

--------------------------------------------------------------------------------
-- *
--------------------------------------------------------------------------------

newtype Symbolic a = Symbolic { unSymbolic :: Rat }
  deriving (Eq, Ord, Show, V.TypedSExpr, V.SMTOrd)

instance V.Fresh (Symbolic a)
  where
    fresh = V.freshSExpr

symbCast :: Symbolic a -> Symbolic b
symbCast = Symbolic . unSymbolic

symbFun :: SymbParam a => String -> [Symbolic a] -> Symbolic a
symbFun name (args :: [Symbolic a]) = V.fromSMT $
  SMT.fun (symbType (undefined :: a) ++ "-" ++ name) (map V.toSMT args)

fromComplexConstant :: (RealFrac a, SymbParam b) => Complex.Complex a -> Symbolic b
fromComplexConstant c = symbFun "complex" [real, imag]
  where
    real = Symbolic $ fromRational $ toRational $ Complex.realPart c
    imag = Symbolic $ fromRational $ toRational $ Complex.imagPart c

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

data SymbFloat
data SymbDouble
data SymbComplexFloat
data SymbComplexDouble

class SymbParam a
  where
    symbType :: a -> String

instance SymbParam SymbFloat  where symbType _ = "float"
instance SymbParam SymbDouble where symbType _ = "double"
instance SymbParam SymbComplexFloat  where symbType _ = "cfloat"
instance SymbParam SymbComplexDouble where symbType _ = "cdouble"

instance SymbParam a => Num (Symbolic a)
  where
    fromInteger = Symbolic . fromInteger
    x + y  = symbFun "+" [x, y]
    x - y  = symbFun "-" [x, y]
    x * y  = symbFun "*" [x, y]
    abs    = smtAbs
    signum = smtSignum

instance SymbParam a => Fractional (Symbolic a) where
  fromRational = Symbolic . fromRational
  x / y = symbFun "/" [x, y]

instance SymbParam a => Floating (Symbolic a) where
  pi      = fromRational (toRational pi)
  exp x   = symbFun "exp" [x]
  log x   = symbFun "log" [x]
  sqrt x  = symbFun "sqrt" [x]
  x ** y  = symbFun "pow" [x, y]
  sin x   = symbFun "sin" [x]
  cos x   = symbFun "cos" [x]
  tan x   = symbFun "tan" [x]
  asin x  = symbFun "asin" [x]
  acos x  = symbFun "acos" [x]
  atan x  = symbFun "atan" [x]
  sinh x  = symbFun "sinh" [x]
  cosh x  = symbFun "cosh" [x]
  tanh x  = symbFun "tanh" [x]
  asinh x = symbFun "asinh" [x]
  acosh x = symbFun "acosh" [x]
  atanh x = symbFun "atanh" [x]

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

class Floating a => Complex a
  where
    type RealPart a
    complex   :: RealPart a -> RealPart a -> a
    polar     :: RealPart a -> RealPart a -> a
    real      :: a -> RealPart a
    imag      :: a -> RealPart a
    magnitude :: a -> RealPart a
    phase     :: a -> RealPart a
    conjugate :: a -> a

instance Complex (V.SMTExpr Prim (Complex.Complex Float))
  where
    type RealPart (V.SMTExpr Prim (Complex.Complex Float)) = V.SMTExpr Prim Float
    complex   (Float x) (Float y) = ComplexFloat (complex x y)
    polar     (Float x) (Float y) = ComplexFloat (polar x y)
    real      (ComplexFloat x)    = Float (real x)
    imag      (ComplexFloat x)    = Float (imag x)
    magnitude (ComplexFloat x)    = Float (magnitude x)
    phase     (ComplexFloat x)    = Float (phase x)
    conjugate (ComplexFloat x)    = ComplexFloat (conjugate x)

instance Complex (V.SMTExpr Prim (Complex.Complex Double))
  where
    type RealPart (V.SMTExpr Prim (Complex.Complex Double)) = V.SMTExpr Prim Double
    complex   (Double x) (Double y) = ComplexDouble (complex x y)
    polar     (Double x) (Double y) = ComplexDouble (polar x y)
    real      (ComplexDouble x)     = Double (real x)
    imag      (ComplexDouble x)     = Double (imag x)
    magnitude (ComplexDouble x)     = Double (magnitude x)
    phase     (ComplexDouble x)     = Double (phase x)
    conjugate (ComplexDouble x)     = ComplexDouble (conjugate x)

witnessComplex :: (SoftwarePrimType a, SoftwarePrimType (Complex.Complex a)) =>
  Prim (Complex.Complex a) ->
  Dict ( Floating (V.SMTExpr Prim a)
       , Complex  (V.SMTExpr Prim (Complex.Complex a))
       , RealPart (V.SMTExpr Prim (Complex.Complex a)) ~ V.SMTExpr Prim a)
witnessComplex (_ :: Prim (Complex.Complex a)) =
  case softwareRep :: SoftwarePrimTypeRep (Complex.Complex a) of
    ComplexFloatST  -> Dict
    ComplexDoubleST -> Dict

witnessFractional :: (SoftwarePrimType a, Fractional a) =>
  Prim a ->
  Dict (Floating (V.SMTExpr Prim a))
witnessFractional (_ :: Prim a) = case softwareRep :: SoftwarePrimTypeRep a of
    FloatST         -> Dict
    DoubleST        -> Dict
    ComplexFloatST  -> Dict
    ComplexDoubleST -> Dict

witnessIntegral :: (SoftwarePrimType a, Integral a) =>
  Prim a ->
  Dict (Integral (V.SMTExpr Prim a), Bits (V.SMTExpr Prim a))
witnessIntegral (_ :: Prim a) = case softwareRep :: SoftwarePrimTypeRep a of
  Int8ST   -> Dict
  Int16ST  -> Dict
  Int32ST  -> Dict
  Int64ST  -> Dict
  Word8ST  -> Dict
  Word16ST -> Dict
  Word32ST -> Dict
  Word64ST -> Dict

witnessBits :: (SoftwarePrimType a, Bits.Bits a) =>
  Prim a ->
  Dict ( Num a
       , Integral (V.SMTExpr Prim a)
       , Bits (V.SMTExpr Prim a))
witnessBits (_ :: Prim a) = case softwareRep :: SoftwarePrimTypeRep a of
  Int8ST   -> Dict
  Int16ST  -> Dict
  Int32ST  -> Dict
  Int64ST  -> Dict
  Word8ST  -> Dict
  Word16ST -> Dict
  Word32ST -> Dict
  Word64ST -> Dict

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

toRat :: (SoftwarePrimType a, Fractional a) => V.SMTExpr Prim a -> Rat
toRat (x :: V.SMTExpr Prim a) = case softwareRep :: SoftwarePrimTypeRep a of
  FloatST         -> let Float         (Symbolic y) = x in y
  DoubleST        -> let Double        (Symbolic y) = x in y
  ComplexFloatST  -> let ComplexFloat  (Symbolic y) = x in y
  ComplexDoubleST -> let ComplexDouble (Symbolic y) = x in y

fromRat :: forall a. (SoftwarePrimType a, Num a) => Rat -> V.SMTExpr Prim a
fromRat x = case softwareRep :: SoftwarePrimTypeRep a of Int8ST -> Int8 (f2i x)
  where
    f2i :: forall s w. (Sign s, Width w) => Rat -> BV s w
    f2i (Rat x) = BV $ SMT.List [SMT.fam "int2bv" [width (undefined :: w)], SMT.fun "to_int" [x]]

i2n :: forall a b.
  ( V.SMTEval Prim a, SoftwarePrimType a, Integral a
  , V.SMTEval Prim b, SoftwarePrimType b, Num b) =>
  V.SMTExpr Prim a ->
  V.SMTExpr Prim b
i2n x = toBV x $ case softwareRep :: SoftwarePrimTypeRep b of
  Int8ST   -> Int8   . i2i
  Int16ST  -> Int16  . i2i
  Int32ST  -> Int32  . i2i
  Int64ST  -> Int64  . i2i
  Word8ST  -> Word8  . i2i
  Word16ST -> Word16 . i2i
  Word32ST -> Word32 . i2i
  Word64ST -> Word64 . i2i
  FloatST  -> Float  . Symbolic . i2f
  DoubleST -> Double . Symbolic . i2f
  ComplexFloatST  -> ComplexFloat  . Symbolic . i2f
  ComplexDoubleST -> ComplexDouble . Symbolic . i2f
  where
    toBV :: forall a b. (V.SMTEval Prim a, SoftwarePrimType a, Integral a) =>
      V.SMTExpr Prim a -> (forall s w. (Sign s, Width w) => BV s w -> b) -> b
    toBV (x :: V.SMTExpr Prim a) k = case softwareRep :: SoftwarePrimTypeRep a of
      Int8ST   -> let Int8   y = x in k y
      Int16ST  -> let Int16  y = x in k y
      Int32ST  -> let Int32  y = x in k y
      Int64ST  -> let Int64  y = x in k y
      Word8ST  -> let Word8  y = x in k y
      Word16ST -> let Word16 y = x in k y
      Word32ST -> let Word32 y = x in k y
      Word64ST -> let Word64 y = x in k y

    i2f :: (Sign s, Width w) => BV s w -> Rat
    i2f (BV x) = Rat (SMT.fun "to_real" [SMT.fun "bv2int" [x]])

    i2i :: forall s1 w1 s2 w2. (Sign s1, Width w1, Sign s2, Width w2) => BV s1 w1 -> BV s2 w2
    i2i x = case compare m n of
      LT | isSigned x -> V.fromSMT (SMT.signExtend (n-m) (V.toSMT x))
         | otherwise  -> V.fromSMT (SMT.zeroExtend (n-m) (V.toSMT x))
      EQ -> V.fromSMT (V.toSMT x)
      GT -> V.fromSMT (SMT.extract (V.toSMT x) (n-1) 0)
      where
        m = width (undefined :: w1)
        n = width (undefined :: w2)

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

class SymbParam a => SymbComplex a
  where
    type SymbRealPart a

instance SymbComplex SymbComplexFloat
  where
    type SymbRealPart SymbComplexFloat  = SymbFloat

instance SymbComplex SymbComplexDouble
  where
    type SymbRealPart SymbComplexDouble = SymbDouble

instance SymbComplex a => Complex (Symbolic a)
  where
    type RealPart (Symbolic a) = Symbolic (SymbRealPart a)
    complex x y = symbFun "complex" [symbCast x, symbCast y]
    polar x y   = symbFun "polar" [symbCast x, symbCast y]
    real x      = symbCast (symbFun "real" [x])
    imag x      = symbCast (symbFun "imag" [x])
    magnitude x = symbCast (symbFun "magnitude" [x])
    phase x     = symbCast (symbFun "phase" [x])
    conjugate x = symbFun "conjugate" [x]

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

declareSymbFun :: SymbParam a => String -> a ->
  [SMT.SExpr] -> SMT.SExpr -> SMT.SMT ()
declareSymbFun name (_ :: a) args res =
  S.void $ SMT.declareFun (symbType (undefined :: a) ++ "-" ++ name) args res

declareSymbArith :: SymbParam a => a -> SMT.SMT ()
declareSymbArith x = do
  declareSymbFun "+" x     [SMT.tReal, SMT.tReal] SMT.tReal
  declareSymbFun "-" x     [SMT.tReal, SMT.tReal] SMT.tReal
  declareSymbFun "*" x     [SMT.tReal, SMT.tReal] SMT.tReal
  declareSymbFun "/" x     [SMT.tReal, SMT.tReal] SMT.tReal
  declareSymbFun "exp" x   [SMT.tReal] SMT.tReal
  declareSymbFun "log" x   [SMT.tReal] SMT.tReal
  declareSymbFun "sqrt" x  [SMT.tReal] SMT.tReal
  declareSymbFun "pow" x   [SMT.tReal, SMT.tReal] SMT.tReal
  declareSymbFun "sin" x   [SMT.tReal] SMT.tReal
  declareSymbFun "cos" x   [SMT.tReal] SMT.tReal
  declareSymbFun "tan" x   [SMT.tReal] SMT.tReal
  declareSymbFun "asin" x  [SMT.tReal] SMT.tReal
  declareSymbFun "acos" x  [SMT.tReal] SMT.tReal
  declareSymbFun "atan" x  [SMT.tReal] SMT.tReal
  declareSymbFun "sinh" x  [SMT.tReal] SMT.tReal
  declareSymbFun "cosh" x  [SMT.tReal] SMT.tReal
  declareSymbFun "tanh" x  [SMT.tReal] SMT.tReal
  declareSymbFun "asinh" x [SMT.tReal] SMT.tReal
  declareSymbFun "acosh" x [SMT.tReal] SMT.tReal
  declareSymbFun "atanh" x [SMT.tReal] SMT.tReal

declareSymbComplex :: SymbParam a => a -> SMT.SMT ()
declareSymbComplex x = do
  declareSymbArith x
  declareSymbFun "complex" x   [SMT.tReal, SMT.tReal] SMT.tReal
  declareSymbFun "polar" x     [SMT.tReal, SMT.tReal] SMT.tReal
  declareSymbFun "real" x      [SMT.tReal] SMT.tReal
  declareSymbFun "imag" x      [SMT.tReal] SMT.tReal
  declareSymbFun "magnitude" x [SMT.tReal] SMT.tReal
  declareSymbFun "phase" x     [SMT.tReal] SMT.tReal
  declareSymbFun "conjugate" x [SMT.tReal] SMT.tReal

declareFeldsparGlobals :: SMT.SMT ()
declareFeldsparGlobals = do
  declareSymbArith   (undefined :: SymbFloat)
  declareSymbArith   (undefined :: SymbDouble)
  declareSymbComplex (undefined :: SymbComplexFloat)
  declareSymbComplex (undefined :: SymbComplexDouble)
  SMT.declareFun "skolem-int8"   [] (SMT.tBits 8)
  SMT.declareFun "skolem-int16"  [] (SMT.tBits 16)
  SMT.declareFun "skolem-int32"  [] (SMT.tBits 32)
  SMT.declareFun "skolem-int64"  [] (SMT.tBits 64)
  SMT.declareFun "skolem-word8"  [] (SMT.tBits 8)
  SMT.declareFun "skolem-word16" [] (SMT.tBits 16)
  SMT.declareFun "skolem-word32" [] (SMT.tBits 32)
  SMT.declareFun "skolem-word64" [] (SMT.tBits 64)
  return ()

instance FO.Substitute Prim
  where
    type SubstPred Prim = SoftwarePrimType
    subst sub (Prim exp) = Prim (everywhereUp f exp)
      where
        f :: ASTF SoftwarePrimDomain a -> ASTF SoftwarePrimDomain a
        f (Sym (FreeVar x :&: ty)) = case FO.lookupSubst sub (Imp.ValComp x) of
          Imp.ValComp y -> Sym (FreeVar y :&: ty)
          Imp.ValRun  z -> Sym (Lit z :&: ty)
        f (Sym (ArrIx iarr :&: ty) :$ i) = Sym (ArrIx iarr' :&: ty) :$ i
          where iarr' = FO.lookupSubst sub iarr
        f x = x

instance FO.TypeablePred SoftwarePrimType
  where
    witnessTypeable Dict = Dict

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

instance V.SMTEval Prim Bool where
  fromConstant = Bool . SMT.bool
  witnessOrd _ = Dict

instance V.SMTEval Prim Int8 where
  fromConstant = Int8 . fromIntegral
  witnessNum _ = Dict
  witnessOrd _ = Dict
  skolemIndex  = V.fromSMT (SMT.fun "skolem-int8" [])

instance V.SMTEval Prim Int16 where
  fromConstant = Int16 . fromIntegral
  witnessNum _ = Dict
  witnessOrd _ = Dict
  skolemIndex  = V.fromSMT (SMT.fun "skolem-int16" [])

instance V.SMTEval Prim Int32 where
  fromConstant = Int32 . fromIntegral
  witnessNum _ = Dict
  witnessOrd _ = Dict
  skolemIndex  = V.fromSMT (SMT.fun "skolem-int32" [])

instance V.SMTEval Prim Int64 where
  fromConstant = Int64 . fromIntegral
  witnessNum _ = Dict
  witnessOrd _ = Dict
  skolemIndex  = V.fromSMT (SMT.fun "skolem-int64" [])

instance V.SMTEval Prim Word8 where
  fromConstant = Word8 . fromIntegral
  witnessNum _ = Dict
  witnessOrd _ = Dict
  skolemIndex  = V.fromSMT (SMT.fun "skolem-word8" [])

instance V.SMTEval Prim Word16 where
  fromConstant = Word16 . fromIntegral
  witnessNum _ = Dict
  witnessOrd _ = Dict
  skolemIndex  = V.fromSMT (SMT.fun "skolem-word16" [])

instance V.SMTEval Prim Word32 where
  fromConstant = Word32 . fromIntegral
  witnessNum _ = Dict
  witnessOrd _ = Dict
  skolemIndex  = V.fromSMT (SMT.fun "skolem-word32" [])

instance V.SMTEval Prim Word64 where
  fromConstant = Word64 . fromIntegral
  witnessNum _ = Dict
  witnessOrd _ = Dict
  skolemIndex  = V.fromSMT (SMT.fun "skolem-word64" [])

instance V.SMTEval Prim Float where
  fromConstant = Float . fromRational . toRational
  witnessOrd _ = Dict
  witnessNum _ = Dict

instance V.SMTEval Prim Double where
  fromConstant = Double . fromRational . toRational
  witnessOrd _ = Dict
  witnessNum _ = Dict

instance V.SMTEval Prim (Complex.Complex Float) where
  fromConstant = ComplexFloat . fromComplexConstant
  witnessNum _ = Dict

instance V.SMTEval Prim (Complex.Complex Double) where
  fromConstant = ComplexDouble . fromComplexConstant
  witnessNum _ = Dict

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

instance V.SMTEval1 Prim where
  type Pred Prim = SoftwarePrimType
  newtype SMTExpr Prim Bool   = Bool SMT.SExpr
    deriving (Typeable)
  newtype SMTExpr Prim Float  = Float  (Symbolic SymbFloat)
    deriving (Typeable, Num, Fractional, Floating, V.SMTOrd, V.TypedSExpr)
  newtype SMTExpr Prim Double = Double (Symbolic SymbDouble)
    deriving (Typeable, Num, Fractional, Floating, V.SMTOrd, V.TypedSExpr)
  newtype SMTExpr Prim (Complex.Complex Float) =
      ComplexFloat (Symbolic SymbComplexFloat)
    deriving (Typeable, Num, Fractional, Floating, V.TypedSExpr)
  newtype SMTExpr Prim (Complex.Complex Double) =
      ComplexDouble (Symbolic SymbComplexDouble)
    deriving (Typeable, Num, Fractional, Floating, V.TypedSExpr)
  newtype SMTExpr Prim Int8   = Int8   (BV Signed W8)
    deriving (Typeable, Num, Real, Enum, Integral, Bits, V.SMTOrd, V.TypedSExpr)
  newtype SMTExpr Prim Int16  = Int16  (BV Signed W16)
    deriving (Typeable, Num, Real, Enum, Integral, Bits, V.SMTOrd, V.TypedSExpr)
  newtype SMTExpr Prim Int32  = Int32  (BV Signed W32)
    deriving (Typeable, Num, Real, Enum, Integral, Bits, V.SMTOrd, V.TypedSExpr)
  newtype SMTExpr Prim Int64  = Int64  (BV Signed W64)
    deriving (Typeable, Num, Real, Enum, Integral, Bits, V.SMTOrd, V.TypedSExpr)
  newtype SMTExpr Prim Word8  = Word8  (BV Unsigned W8)
    deriving (Typeable, Num, Real, Enum, Integral, Bits, V.SMTOrd, V.TypedSExpr)
  newtype SMTExpr Prim Word16 = Word16 (BV Unsigned W16)
    deriving (Typeable, Num, Real, Enum, Integral, Bits, V.SMTOrd, V.TypedSExpr)
  newtype SMTExpr Prim Word32 = Word32 (BV Unsigned W32)
    deriving (Typeable, Num, Real, Enum, Integral, Bits, V.SMTOrd, V.TypedSExpr)
  newtype SMTExpr Prim Word64 = Word64 (BV Unsigned W64)
    deriving (Typeable, Num, Real, Enum, Integral, Bits, V.SMTOrd, V.TypedSExpr)

  eval (Prim exp :: Prim a) =
    simpleMatch (\(exp :&: ty) -> case softwarePrimWitType ty of
      Dict -> case V.witnessPred (undefined :: Prim a) of
        Dict -> verifyPrim exp) exp

  witnessPred (_ :: Prim a) = case softwareRep :: SoftwarePrimTypeRep a of
    BoolST   -> Dict
    Int8ST   -> Dict
    Int16ST  -> Dict
    Int32ST  -> Dict
    Int64ST  -> Dict
    Word8ST  -> Dict
    Word16ST -> Dict
    Word32ST -> Dict
    Word64ST -> Dict
    FloatST  -> Dict
    DoubleST -> Dict
    ComplexFloatST  -> Dict
    ComplexDoubleST -> Dict

instance V.SMTOrd (V.SMTExpr Prim Bool) where
  Bool x .<.  Bool y = SMT.not x SMT..&&. y
  Bool x .>.  Bool y = x SMT..&&. SMT.not y
  Bool x .<=. Bool y = SMT.not x SMT..||. y
  Bool x .>=. Bool y = x SMT..||. SMT.not y

instance V.TypedSExpr (V.SMTExpr Prim Bool) where
  smtType _ = SMT.tBool
  toSMT (Bool x) = x
  fromSMT x = Bool x

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

verifyPrim :: forall a .
  (SoftwarePrimType (DenResult a), V.SMTEval Prim (DenResult a), HasCallStack) =>
  SoftwarePrim a ->
  Args (AST SoftwarePrimDomain) a ->
  V.Verify (V.SMTExpr Prim (DenResult a))
verifyPrim (FreeVar x) _ = peekValue x
verifyPrim (Lit x) _     = return (V.fromConstant x)
verifyPrim Add (x :* y :* Nil)
  | Dict <- V.witnessNum (undefined :: Prim (DenResult a)) =
    S.liftM2 (+) (V.eval (Prim x)) (V.eval (Prim y))
verifyPrim Sub (x :* y :* Nil)
  | Dict <- V.witnessNum (undefined :: Prim (DenResult a)) =
    S.liftM2 (-) (V.eval (Prim x)) (V.eval (Prim y))
verifyPrim Mul (x :* y :* Nil)
  | Dict <- V.witnessNum (undefined :: Prim (DenResult a)) =
    S.liftM2 (*) (V.eval (Prim x)) (V.eval (Prim y))
verifyPrim Neg (x :* Nil)
  | Dict <- V.witnessNum (undefined :: Prim (DenResult a)) =
    fmap negate (V.eval (Prim x))
verifyPrim Abs (x :* Nil)
  | Dict <- V.witnessNum (undefined :: Prim (DenResult a)) =
    fmap abs (V.eval (Prim x))
verifyPrim Sign (x :* Nil)
  | Dict <- V.witnessNum (undefined :: Prim (DenResult a)) =
    fmap signum (V.eval (Prim x))
verifyPrim Div (x :* y :* Nil)
  | Dict <- witnessIntegral (undefined :: Prim (DenResult a)) =
    S.liftM2 div (V.eval (Prim x)) (V.eval (Prim y))
verifyPrim Mod (x :* y :* Nil)
  | Dict <- witnessIntegral (undefined :: Prim (DenResult a)) =
    S.liftM2 mod (V.eval (Prim x)) (V.eval (Prim y))
verifyPrim Quot (x :* y :* Nil)
  | Dict <- witnessIntegral (undefined :: Prim (DenResult a)) =
    S.liftM2 quot (V.eval (Prim x)) (V.eval (Prim y))
verifyPrim Rem (x :* y :* Nil)
  | Dict <- witnessIntegral (undefined :: Prim (DenResult a)) =
    S.liftM2 rem (V.eval (Prim x)) (V.eval (Prim y))
verifyPrim FDiv (x :* y :* Nil)
  | Dict <- witnessFractional (undefined :: Prim (DenResult a)) =
    S.liftM2 (/) (V.eval (Prim x)) (V.eval (Prim y))
verifyPrim Pi Nil
  | Dict <- witnessFractional (undefined :: Prim (DenResult a)) =
    return pi
verifyPrim Exp (x :* Nil)
  | Dict <- witnessFractional (undefined :: Prim (DenResult a)) =
    fmap exp (V.eval (Prim x))
verifyPrim Log (x :* Nil)
  | Dict <- witnessFractional (undefined :: Prim (DenResult a)) =
    fmap log (V.eval (Prim x))
verifyPrim Sqrt (x :* Nil)
  | Dict <- witnessFractional (undefined :: Prim (DenResult a)) =
    fmap sqrt (V.eval (Prim x))
verifyPrim Pow (x :* y :* Nil)
  | Dict <- witnessFractional (undefined :: Prim (DenResult a)) =
    S.liftM2 (**) (V.eval (Prim x)) (V.eval (Prim y))
verifyPrim Sin (x :* Nil)
  | Dict <- witnessFractional (undefined :: Prim (DenResult a)) =
    fmap sin (V.eval (Prim x))
verifyPrim Cos (x :* Nil)
  | Dict <- witnessFractional (undefined :: Prim (DenResult a)) =
    fmap cos (V.eval (Prim x))
verifyPrim Tan (x :* Nil)
  | Dict <- witnessFractional (undefined :: Prim (DenResult a)) =
    fmap tan (V.eval (Prim x))
verifyPrim Asin (x :* Nil)
  | Dict <- witnessFractional (undefined :: Prim (DenResult a)) =
    fmap asin (V.eval (Prim x))
verifyPrim Acos (x :* Nil)
  | Dict <- witnessFractional (undefined :: Prim (DenResult a)) =
    fmap acos (V.eval (Prim x))
verifyPrim Atan (x :* Nil)
  | Dict <- witnessFractional (undefined :: Prim (DenResult a)) =
    fmap atan (V.eval (Prim x))
verifyPrim Sinh (x :* Nil)
  | Dict <- witnessFractional (undefined :: Prim (DenResult a)) =
    fmap sinh (V.eval (Prim x))
verifyPrim Cosh (x :* Nil)
  | Dict <- witnessFractional (undefined :: Prim (DenResult a)) =
    fmap cosh (V.eval (Prim x))
verifyPrim Tanh (x :* Nil)
  | Dict <- witnessFractional (undefined :: Prim (DenResult a)) =
    fmap tanh (V.eval (Prim x))
verifyPrim Asinh (x :* Nil)
  | Dict <- witnessFractional (undefined :: Prim (DenResult a)) =
    fmap asinh (V.eval (Prim x))
verifyPrim Acosh (x :* Nil)
  | Dict <- witnessFractional (undefined :: Prim (DenResult a)) =
    fmap acosh (V.eval (Prim x))
verifyPrim Atanh (x :* Nil)
  | Dict <- witnessFractional (undefined :: Prim (DenResult a)) =
    fmap atanh (V.eval (Prim x))
verifyPrim Complex (x :* y :* Nil)
  | Dict <- witnessComplex (undefined :: Prim (DenResult a)) =
    S.liftM2 complex (V.eval (Prim x)) (V.eval (Prim y))
verifyPrim Polar (x :* y :* Nil)
  | Dict <- witnessComplex (undefined :: Prim (DenResult a)) =
    S.liftM2 polar (V.eval (Prim x)) (V.eval (Prim y))
verifyPrim Real ((x :: ASTF SoftwarePrimDomain b) :* Nil)
  | Dict <- witnessComplex (undefined :: Prim b) =
    fmap real (V.eval (Prim x))
verifyPrim Imag ((x :: ASTF SoftwarePrimDomain b) :* Nil)
  | Dict <- witnessComplex (undefined :: Prim b) =
    fmap imag (V.eval (Prim x))
verifyPrim Magnitude ((x :: ASTF SoftwarePrimDomain b) :* Nil)
  | Dict <- witnessComplex (undefined :: Prim b) =
    fmap magnitude (V.eval (Prim x))
verifyPrim Phase ((x :: ASTF SoftwarePrimDomain b) :* Nil)
  | Dict <- witnessComplex (undefined :: Prim b) =
    fmap phase (V.eval (Prim x))
verifyPrim Conjugate ((x :: ASTF SoftwarePrimDomain b) :* Nil)
  | Dict <- witnessComplex (undefined :: Prim b) =
    fmap conjugate (V.eval (Prim x))
verifyPrim I2N ((x :: ASTF SoftwarePrimDomain b) :* Nil)
  | Dict <- V.witnessPred (undefined :: Prim b),
    Dict <- V.witnessNum (undefined :: Prim b) = do
    fmap i2n (V.eval (Prim x))
verifyPrim I2B ((x :: ASTF SoftwarePrimDomain b) :* Nil)
  | Dict <- V.witnessPred (undefined :: Prim b),
    Dict <- V.witnessNum (undefined :: Prim b) = do
    x <- V.eval (Prim x)
    return (V.fromSMT (SMT.not (x V..==. 0)))
verifyPrim B2I (x :* Nil)
  | Dict <- V.witnessNum (undefined :: Prim (DenResult a)) = do
    x <- V.eval (Prim x)
    return (V.smtIte (V.toSMT x) 1 0)
verifyPrim Round ((x :: ASTF SoftwarePrimDomain b) :* Nil) = do
  x <- V.eval (Prim x)
  return (fromRat (toRat x))
verifyPrim Not (x :* Nil) =
  fmap (V.fromSMT . SMT.not . V.toSMT) (V.eval (Prim x))
verifyPrim And (x :* y :* Nil) = do
  x <- V.eval (Prim x)
  y <- V.eval (Prim y)
  return (V.fromSMT (V.toSMT x SMT..&&. V.toSMT y))
verifyPrim Or (x :* y :* Nil) = do
  x <- V.eval (Prim x)
  y <- V.eval (Prim y)
  return (V.fromSMT (V.toSMT x SMT..||. V.toSMT y))
verifyPrim Eq ((x :: ASTF SoftwarePrimDomain b) :* y :* Nil)
  | Dict <- V.witnessPred (undefined :: Prim b) =
    fmap V.fromSMT (S.liftM2 (V..==.) (V.eval (Prim x)) (V.eval (Prim y)))
verifyPrim Neq ((x :: ASTF SoftwarePrimDomain b) :* y :* Nil)
  | Dict <- V.witnessPred (undefined :: Prim b) =
    fmap V.fromSMT (S.liftM2 (./=.) (V.eval (Prim x)) (V.eval (Prim y)))
  where
    x ./=. y = SMT.not (x V..==. y)
verifyPrim Lt ((x :: ASTF SoftwarePrimDomain b) :* y :* Nil)
  | Dict <- V.witnessPred (undefined :: Prim b),
    Dict <- V.witnessOrd  (undefined :: Prim b) =
    fmap V.fromSMT (S.liftM2 (V..<.) (V.eval (Prim x)) (V.eval (Prim y)))
verifyPrim Gt ((x :: ASTF SoftwarePrimDomain b) :* y :* Nil)
  | Dict <- V.witnessPred (undefined :: Prim b),
    Dict <- V.witnessOrd  (undefined :: Prim b) =
    fmap V.fromSMT (S.liftM2 (V..>.) (V.eval (Prim x)) (V.eval (Prim y)))
verifyPrim Lte ((x :: ASTF SoftwarePrimDomain b) :* y :* Nil)
  | Dict <- V.witnessPred (undefined :: Prim b),
    Dict <- V.witnessOrd  (undefined :: Prim b) =
    fmap V.fromSMT (S.liftM2 (V..<=.) (V.eval (Prim x)) (V.eval (Prim y)))
verifyPrim Gte ((x :: ASTF SoftwarePrimDomain b) :* y :* Nil)
  | Dict <- V.witnessPred (undefined :: Prim b),
    Dict <- V.witnessOrd  (undefined :: Prim b) =
    fmap V.fromSMT (S.liftM2 (V..>=.) (V.eval (Prim x)) (V.eval (Prim y)))
verifyPrim BitAnd (x :* y :* Nil)
  | Dict <- witnessBits (undefined :: Prim (DenResult a)) =
    S.liftM2 (.&.) (V.eval (Prim x)) (V.eval (Prim y))
verifyPrim BitOr (x :* y :* Nil)
  | Dict <- witnessBits (undefined :: Prim (DenResult a)) =
    S.liftM2 (.|.) (V.eval (Prim x)) (V.eval (Prim y))
verifyPrim BitXor (x :* y :* Nil)
  | Dict <- witnessBits (undefined :: Prim (DenResult a)) =
    S.liftM2 xor (V.eval (Prim x)) (V.eval (Prim y))
verifyPrim BitCompl (x :* Nil)
  | Dict <- witnessBits (undefined :: Prim (DenResult a)) =
    fmap complement (V.eval (Prim x))
verifyPrim ShiftL (x :* (y :: ASTF SoftwarePrimDomain b) :* Nil)
  | Dict <- witnessBits (undefined :: Prim (DenResult a)),
    Dict <- V.witnessPred (undefined :: Prim b),
    Dict <- witnessIntegral (undefined :: Prim b) = do
    -- todo: should check for undefined behaviour
    x <- V.eval (Prim x)
    y <- V.eval (Prim y)
    return (shiftL x (i2n y))
verifyPrim ShiftR (x :* (y :: ASTF SoftwarePrimDomain b) :* Nil)
  | Dict <- witnessBits (undefined :: Prim (DenResult a)),
    Dict <- V.witnessPred (undefined :: Prim b),
    Dict <- witnessIntegral (undefined :: Prim b) = do
    -- todo: should check for undefined behaviour
    x <- V.eval (Prim x)
    y <- V.eval (Prim y)
    return (shiftR x (i2n y))
verifyPrim (ArrIx (Imp.IArrComp name :: Imp.IArr Index b)) (i :* Nil) = do
  i <- V.eval (Prim i)
  readArray name i
verifyPrim Cond (cond :* x :* y :* Nil) =
  S.liftM3 V.smtIte
    (fmap V.toSMT (V.eval (Prim cond)))
    (V.eval (Prim x))
    (V.eval (Prim y))
verifyPrim exp _ = error ("Unimplemented: " ++ show exp)

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