{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE KindSignatures         #-}
{-# LANGUAGE LambdaCase             #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE UndecidableInstances   #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE CPP                    #-}

{-# OPTIONS_GHC -Wall #-}

module Language.Fortran.Model.Op.Core.Eval
  ( MonadEvalFortran
  , evalCoreOp
  ) where

import           Control.Applicative                  (liftA2)

import           Data.SBV.Dynamic                     (SVal)
import qualified Data.SBV.Dynamic                     as SBV

#if MIN_VERSION_singletons(3,0,0)
import           Data.List.Singletons
import           GHC.TypeLits.Singletons
#else
import           Data.Singletons
import           Data.Singletons.Prelude.List
import           Data.Singletons.TypeLits
#endif

import           Data.Vinyl                           hiding (Field)
import           Data.Vinyl.Curry

import           Language.Fortran.Model.Op.Core.Core
import           Language.Fortran.Model.Op.Core.Match
import           Language.Fortran.Model.Op.Eval
import           Language.Fortran.Model.Repr
import           Language.Fortran.Model.Repr.Prim
import           Language.Fortran.Model.Singletons
import           Language.Fortran.Model.Types
import           Language.Fortran.Model.Types.Match

--------------------------------------------------------------------------------
--  Evaluation
--------------------------------------------------------------------------------

evalCoreOp
  :: (MonadEvalFortran r m)
  => Op (Length args) ok -> OpSpec ok args result -> Rec CoreRepr args -> m (CoreRepr result)
evalCoreOp :: forall r (m :: * -> *) (args :: [*]) (ok :: OpKind) result.
MonadEvalFortran r m =>
Op (Length args) ok
-> OpSpec ok args result
-> Rec CoreRepr args
-> m (CoreRepr result)
evalCoreOp Op (Length args) ok
op = \case
  OSLit Prim p k a
px a
x -> \Rec CoreRepr args
_ -> Prim p k a -> SVal -> CoreRepr (PrimS a)
forall (p :: Precision) (k :: BasicType) a.
Prim p k a -> SVal -> CoreRepr (PrimS a)
primFromVal Prim p k a
px (SVal -> CoreRepr result) -> m SVal -> m (CoreRepr result)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Prim p k a -> a -> m SVal
forall r (m :: * -> *) (p :: Precision) (k :: BasicType) a.
(MonadReader r m, HasPrimReprHandlers r) =>
Prim p k a -> a -> m SVal
primLit Prim p k a
px a
x

  OSNum1 NumericBasicType k1
_ Prim p1 k1 a
_ Prim p2 k2 b
p2 ->
    Bool
-> Prim p2 k2 b
-> (SVal -> SVal)
-> Rec CoreRepr '[PrimS a]
-> m (CoreRepr (PrimS b))
forall r (m :: * -> *) (p2 :: Precision) (k2 :: BasicType) b a.
MonadEvalFortran r m =>
Bool
-> Prim p2 k2 b
-> (SVal -> SVal)
-> Rec CoreRepr '[PrimS a]
-> m (CoreRepr (PrimS b))
primUnop Bool
True Prim p2 k2 b
p2 (Op 1 'OKNum -> SVal -> SVal
numUnop Op 1 'OKNum
Op (Length args) ok
op)
  OSNum2 NumericBasicType k1
nk1 NumericBasicType k2
nk2 Prim p1 k1 a
p1 Prim p2 k2 b
p2 Prim (PrecMax p1 p2) (BasicTypeMax k1 k2) c
p3 ->
    Bool
-> Prim p1 k1 a
-> Prim p2 k2 b
-> Prim
     (Case_6989586621679173660
        p1
        p2
        (Case_6989586621679173612
           p1 p2 (Compare_6989586621679449533 p1 p2)))
     (Case_6989586621679173660
        k1
        k2
        (Case_6989586621679173612
           k1 k2 (Compare_6989586621679449551 k1 k2)))
     c
-> (SVal -> SVal -> SVal)
-> Rec CoreRepr '[PrimS a, PrimS b]
-> m (CoreRepr (PrimS c))
forall r (m :: * -> *) (p1 :: Precision) (k1 :: BasicType) a
       (p2 :: Precision) (k2 :: BasicType) b (p3 :: Precision)
       (k3 :: BasicType) c.
MonadEvalFortran r m =>
Bool
-> Prim p1 k1 a
-> Prim p2 k2 b
-> Prim p3 k3 c
-> (SVal -> SVal -> SVal)
-> Rec CoreRepr '[PrimS a, PrimS b]
-> m (CoreRepr (PrimS c))
primBinop Bool
True Prim p1 k1 a
p1 Prim p2 k2 b
p2 Prim
  (Case_6989586621679173660
     p1
     p2
     (Case_6989586621679173612
        p1 p2 (Compare_6989586621679449533 p1 p2)))
  (Case_6989586621679173660
     k1
     k2
     (Case_6989586621679173612
        k1 k2 (Compare_6989586621679449551 k1 k2)))
  c
Prim (PrecMax p1 p2) (BasicTypeMax k1 k2) c
p3 (Bool -> Op 2 'OKNum -> SVal -> SVal -> SVal
numBinop (NumericBasicType k1 -> NumericBasicType k2 -> Bool
forall (k1 :: BasicType) (k2 :: BasicType).
NumericBasicType k1 -> NumericBasicType k2 -> Bool
nkBothInts NumericBasicType k1
nk1 NumericBasicType k2
nk2) Op 2 'OKNum
Op (Length args) ok
op)

  OSLogical1 Prim p1 'BTLogical a
_ Prim 'P8 'BTLogical b
p2 -> Bool
-> Prim 'P8 'BTLogical b
-> (SVal -> SVal)
-> Rec CoreRepr '[PrimS a]
-> m (CoreRepr (PrimS b))
forall r (m :: * -> *) (p2 :: Precision) (k2 :: BasicType) b a.
MonadEvalFortran r m =>
Bool
-> Prim p2 k2 b
-> (SVal -> SVal)
-> Rec CoreRepr '[PrimS a]
-> m (CoreRepr (PrimS b))
primUnop Bool
True Prim 'P8 'BTLogical b
p2 (Op 1 'OKLogical -> SVal -> SVal
logicalUnop Op 1 'OKLogical
Op (Length args) ok
op)
  OSLogical2 Prim p1 'BTLogical a
p1 Prim p2 'BTLogical b
p2 Prim 'P8 'BTLogical c
p3 -> Bool
-> Prim p1 'BTLogical a
-> Prim p2 'BTLogical b
-> Prim 'P8 'BTLogical c
-> (SVal -> SVal -> SVal)
-> Rec CoreRepr '[PrimS a, PrimS b]
-> m (CoreRepr (PrimS c))
forall r (m :: * -> *) (p1 :: Precision) (k1 :: BasicType) a
       (p2 :: Precision) (k2 :: BasicType) b (p3 :: Precision)
       (k3 :: BasicType) c.
MonadEvalFortran r m =>
Bool
-> Prim p1 k1 a
-> Prim p2 k2 b
-> Prim p3 k3 c
-> (SVal -> SVal -> SVal)
-> Rec CoreRepr '[PrimS a, PrimS b]
-> m (CoreRepr (PrimS c))
primBinop Bool
True Prim p1 'BTLogical a
p1 Prim p2 'BTLogical b
p2 Prim 'P8 'BTLogical c
p3 (Op 2 'OKLogical -> SVal -> SVal -> SVal
logicalBinop Op 2 'OKLogical
Op (Length args) ok
op)

  OSEq ComparableBasicTypes k1 k2
cmp Prim p1 k1 a
p1 Prim p2 k2 b
p2 Prim 'P8 'BTLogical c
p3 -> Bool
-> Prim p1 k1 a
-> Prim p2 k2 b
-> Prim 'P8 'BTLogical c
-> (SVal -> SVal -> SVal)
-> Rec CoreRepr '[PrimS a, PrimS b]
-> m (CoreRepr (PrimS c))
forall r (m :: * -> *) (p1 :: Precision) (k1 :: BasicType) a
       (p2 :: Precision) (k2 :: BasicType) b (p3 :: Precision)
       (k3 :: BasicType) c.
MonadEvalFortran r m =>
Bool
-> Prim p1 k1 a
-> Prim p2 k2 b
-> Prim p3 k3 c
-> (SVal -> SVal -> SVal)
-> Rec CoreRepr '[PrimS a, PrimS b]
-> m (CoreRepr (PrimS c))
primBinop Bool
False Prim p1 k1 a
p1 Prim p2 k2 b
p2 Prim 'P8 'BTLogical c
p3 (ComparableBasicTypes k1 k2 -> Op 2 'OKEq -> SVal -> SVal -> SVal
forall (k1 :: BasicType) (k2 :: BasicType).
ComparableBasicTypes k1 k2 -> Op 2 'OKEq -> SVal -> SVal -> SVal
eqBinop ComparableBasicTypes k1 k2
cmp Op 2 'OKEq
Op (Length args) ok
op)
  OSRel ComparableBasicTypes k1 k2
cmp Prim p1 k1 a
p1 Prim p2 k2 b
p2 Prim 'P8 'BTLogical c
p3 -> Bool
-> Prim p1 k1 a
-> Prim p2 k2 b
-> Prim 'P8 'BTLogical c
-> (SVal -> SVal -> SVal)
-> Rec CoreRepr '[PrimS a, PrimS b]
-> m (CoreRepr (PrimS c))
forall r (m :: * -> *) (p1 :: Precision) (k1 :: BasicType) a
       (p2 :: Precision) (k2 :: BasicType) b (p3 :: Precision)
       (k3 :: BasicType) c.
MonadEvalFortran r m =>
Bool
-> Prim p1 k1 a
-> Prim p2 k2 b
-> Prim p3 k3 c
-> (SVal -> SVal -> SVal)
-> Rec CoreRepr '[PrimS a, PrimS b]
-> m (CoreRepr (PrimS c))
primBinop Bool
False Prim p1 k1 a
p1 Prim p2 k2 b
p2 Prim 'P8 'BTLogical c
p3 (ComparableBasicTypes k1 k2 -> Op 2 'OKRel -> SVal -> SVal -> SVal
forall (k1 :: BasicType) (k2 :: BasicType).
ComparableBasicTypes k1 k2 -> Op 2 'OKRel -> SVal -> SVal -> SVal
relBinop ComparableBasicTypes k1 k2
cmp Op 2 'OKRel
Op (Length args) ok
op)

  OSLookup D (Array i result)
_ -> CoreRepr result -> m (CoreRepr result)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (CoreRepr result -> m (CoreRepr result))
-> (Rec CoreRepr args -> CoreRepr result)
-> Rec CoreRepr args
-> m (CoreRepr result)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CurriedF CoreRepr args (CoreRepr result)
-> Rec CoreRepr args -> CoreRepr result
forall {u} (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry CurriedF CoreRepr args (CoreRepr result)
CoreRepr (Array i result) -> CoreRepr i -> CoreRepr result
forall i v. CoreRepr (Array i v) -> CoreRepr i -> CoreRepr v
lookupArr

  OSDeref D (Record rname fields)
_ SSymbol fname
s -> CoreRepr result -> m (CoreRepr result)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (CoreRepr result -> m (CoreRepr result))
-> (Rec CoreRepr args -> CoreRepr result)
-> Rec CoreRepr args
-> m (CoreRepr result)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CurriedF CoreRepr args (CoreRepr result)
-> Rec CoreRepr args -> CoreRepr result
forall {u} (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry (SSymbol fname -> CoreRepr (Record rname fields) -> CoreRepr result
forall a (fname :: Symbol) (fields :: [(Symbol, *)]) (i :: Nat)
       (rname :: Symbol).
RElem '(fname, a) fields i =>
SSymbol fname -> CoreRepr (Record rname fields) -> CoreRepr a
derefData SSymbol fname
s)

--------------------------------------------------------------------------------
--  General
--------------------------------------------------------------------------------

primToVal :: CoreRepr (PrimS a) -> SVal
primToVal :: forall a. CoreRepr (PrimS a) -> SVal
primToVal = \case
  CRPrim (DPrim Prim p k a1
_) SVal
v -> SVal
v

primFromVal :: Prim p k a -> SVal -> CoreRepr (PrimS a)
primFromVal :: forall (p :: Precision) (k :: BasicType) a.
Prim p k a -> SVal -> CoreRepr (PrimS a)
primFromVal Prim p k a
p SVal
v = D (PrimS a) -> SVal -> CoreRepr (PrimS a)
forall a1. D (PrimS a1) -> SVal -> CoreRepr (PrimS a1)
CRPrim (Prim p k a -> D (PrimS a)
forall (p :: Precision) (k :: BasicType) a1.
Prim p k a1 -> D (PrimS a1)
DPrim Prim p k a
p) SVal
v

primUnop
  :: (MonadEvalFortran r m)
  => Bool
  -> Prim p2 k2 b -- ^ The target type
  -> (SVal -> SVal)
  -> Rec CoreRepr '[PrimS a] -> m (CoreRepr (PrimS b))
primUnop :: forall r (m :: * -> *) (p2 :: Precision) (k2 :: BasicType) b a.
MonadEvalFortran r m =>
Bool
-> Prim p2 k2 b
-> (SVal -> SVal)
-> Rec CoreRepr '[PrimS a]
-> m (CoreRepr (PrimS b))
primUnop Bool
shouldCoerce Prim p2 k2 b
p2 SVal -> SVal
f = CurriedF CoreRepr '[PrimS a] (m (CoreRepr (PrimS b)))
-> Rec CoreRepr '[PrimS a] -> m (CoreRepr (PrimS b))
forall {u} (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry (CurriedF CoreRepr '[PrimS a] (m (CoreRepr (PrimS b)))
 -> Rec CoreRepr '[PrimS a] -> m (CoreRepr (PrimS b)))
-> CurriedF CoreRepr '[PrimS a] (m (CoreRepr (PrimS b)))
-> Rec CoreRepr '[PrimS a]
-> m (CoreRepr (PrimS b))
forall a b. (a -> b) -> a -> b
$ (SVal -> CoreRepr (PrimS b)) -> m SVal -> m (CoreRepr (PrimS b))
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Prim p2 k2 b -> SVal -> CoreRepr (PrimS b)
forall (p :: Precision) (k :: BasicType) a.
Prim p k a -> SVal -> CoreRepr (PrimS a)
primFromVal Prim p2 k2 b
p2 (SVal -> CoreRepr (PrimS b))
-> (SVal -> SVal) -> SVal -> CoreRepr (PrimS b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SVal -> SVal
f) (m SVal -> m (CoreRepr (PrimS b)))
-> (CoreRepr (PrimS a) -> m SVal)
-> CoreRepr (PrimS a)
-> m (CoreRepr (PrimS b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SVal -> m SVal
maybeCoerce (SVal -> m SVal)
-> (CoreRepr (PrimS a) -> SVal) -> CoreRepr (PrimS a) -> m SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreRepr (PrimS a) -> SVal
forall a. CoreRepr (PrimS a) -> SVal
primToVal
  where
    maybeCoerce :: SVal -> m SVal
maybeCoerce
      | Bool
shouldCoerce = Prim p2 k2 b -> SVal -> m SVal
forall r (m :: * -> *) (p :: Precision) (k :: BasicType) a.
MonadEvalFortran r m =>
Prim p k a -> SVal -> m SVal
coercePrimSVal Prim p2 k2 b
p2
      | Bool
otherwise = SVal -> m SVal
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return

primBinop
  :: (MonadEvalFortran r m)
  => Bool
  -- ^ True to coerce arguments to result value. False to coerce arguments to
  -- ceiling of each.
  -> Prim p1 k1 a -> Prim p2 k2 b -> Prim p3 k3 c
  -> (SVal -> SVal -> SVal)
  -> Rec CoreRepr '[PrimS a, PrimS b] -> m (CoreRepr (PrimS c))
primBinop :: forall r (m :: * -> *) (p1 :: Precision) (k1 :: BasicType) a
       (p2 :: Precision) (k2 :: BasicType) b (p3 :: Precision)
       (k3 :: BasicType) c.
MonadEvalFortran r m =>
Bool
-> Prim p1 k1 a
-> Prim p2 k2 b
-> Prim p3 k3 c
-> (SVal -> SVal -> SVal)
-> Rec CoreRepr '[PrimS a, PrimS b]
-> m (CoreRepr (PrimS c))
primBinop Bool
takesResultVal Prim p1 k1 a
p1 Prim p2 k2 b
p2 Prim p3 k3 c
p3 SVal -> SVal -> SVal
(.*.) =
  (SVal -> CoreRepr (PrimS c)) -> m SVal -> m (CoreRepr (PrimS c))
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Prim p3 k3 c -> SVal -> CoreRepr (PrimS c)
forall (p :: Precision) (k :: BasicType) a.
Prim p k a -> SVal -> CoreRepr (PrimS a)
primFromVal Prim p3 k3 c
p3) (m SVal -> m (CoreRepr (PrimS c)))
-> (Rec CoreRepr '[PrimS a, PrimS b] -> m SVal)
-> Rec CoreRepr '[PrimS a, PrimS b]
-> m (CoreRepr (PrimS c))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  CurriedF CoreRepr '[PrimS a, PrimS b] (m SVal)
-> Rec CoreRepr '[PrimS a, PrimS b] -> m SVal
forall {u} (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry (\CoreRepr (PrimS a)
x CoreRepr (PrimS b)
y -> (SVal -> SVal -> SVal) -> m SVal -> m SVal -> m SVal
forall a b c. (a -> b -> c) -> m a -> m b -> m c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 SVal -> SVal -> SVal
(.*.) (SVal -> m SVal
coerceArg (CoreRepr (PrimS a) -> SVal
forall a. CoreRepr (PrimS a) -> SVal
primToVal CoreRepr (PrimS a)
x)) (SVal -> m SVal
coerceArg (CoreRepr (PrimS b) -> SVal
forall a. CoreRepr (PrimS a) -> SVal
primToVal CoreRepr (PrimS b)
y)))

  where
    coerceToCeil :: SVal -> m SVal
coerceToCeil = case Prim p1 k1 a
-> Prim p2 k2 b
-> Maybe (MakePrim (PrecMax p1 p2) (BasicTypeMax k1 k2))
forall (p1 :: Precision) (k1 :: BasicType) a (p2 :: Precision)
       (k2 :: BasicType) b.
Prim p1 k1 a
-> Prim p2 k2 b
-> Maybe (MakePrim (PrecMax p1 p2) (BasicTypeMax k1 k2))
primCeil Prim p1 k1 a
p1 Prim p2 k2 b
p2 of
      Just (MakePrim Prim (PrecMax p1 p2) (BasicTypeMax k1 k2) a
pCeil) -> Prim
  (Case_6989586621679173660
     p1
     p2
     (Case_6989586621679173612
        p1 p2 (Compare_6989586621679449533 p1 p2)))
  (Case_6989586621679173660
     k1
     k2
     (Case_6989586621679173612
        k1 k2 (Compare_6989586621679449551 k1 k2)))
  a
-> SVal -> m SVal
forall r (m :: * -> *) (p :: Precision) (k :: BasicType) a.
MonadEvalFortran r m =>
Prim p k a -> SVal -> m SVal
coercePrimSVal Prim
  (Case_6989586621679173660
     p1
     p2
     (Case_6989586621679173612
        p1 p2 (Compare_6989586621679449533 p1 p2)))
  (Case_6989586621679173660
     k1
     k2
     (Case_6989586621679173612
        k1 k2 (Compare_6989586621679449551 k1 k2)))
  a
Prim (PrecMax p1 p2) (BasicTypeMax k1 k2) a
pCeil
      Maybe (MakePrim (PrecMax p1 p2) (BasicTypeMax k1 k2))
_                     -> SVal -> m SVal
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return

    coerceArg :: SVal -> m SVal
coerceArg
      | Bool
takesResultVal = Prim p3 k3 c -> SVal -> m SVal
forall r (m :: * -> *) (p :: Precision) (k :: BasicType) a.
MonadEvalFortran r m =>
Prim p k a -> SVal -> m SVal
coercePrimSVal Prim p3 k3 c
p3
      | Bool
otherwise = SVal -> m SVal
coerceToCeil

--------------------------------------------------------------------------------
--  Numeric
--------------------------------------------------------------------------------

-- TODO: Worry about what happens when LHS and RHS have different types

nkBothInts :: NumericBasicType k1 -> NumericBasicType k2 -> Bool
nkBothInts :: forall (k1 :: BasicType) (k2 :: BasicType).
NumericBasicType k1 -> NumericBasicType k2 -> Bool
nkBothInts NumericBasicType k1
NBTInt NumericBasicType k2
NBTInt = Bool
True
nkBothInts NumericBasicType k1
_ NumericBasicType k2
_           = Bool
False

numUnop :: Op 1 'OKNum -> SVal -> SVal
numUnop :: Op 1 'OKNum -> SVal -> SVal
numUnop = \case
  Op 1 'OKNum
OpNeg -> SVal -> SVal
SBV.svUNeg
  Op 1 'OKNum
OpPos -> SVal -> SVal
forall a. a -> a
id

numBinop :: Bool -> Op 2 'OKNum -> SVal -> SVal -> SVal
numBinop :: Bool -> Op 2 'OKNum -> SVal -> SVal -> SVal
numBinop Bool
isInt = \case
  Op 2 'OKNum
OpAdd -> SVal -> SVal -> SVal
SBV.svPlus
  Op 2 'OKNum
OpSub -> SVal -> SVal -> SVal
SBV.svMinus
  Op 2 'OKNum
OpMul -> SVal -> SVal -> SVal
SBV.svTimes
  Op 2 'OKNum
OpDiv -> if Bool
isInt then SVal -> SVal -> SVal
SBV.svQuot else SVal -> SVal -> SVal
SBV.svDivide

--------------------------------------------------------------------------------
--  Logical
--------------------------------------------------------------------------------

-- TODO: Always return single bits, special-case when inputs are not single bits.
-- TODO: Worry about what happens when LHS and RHS have different types

logicalUnop :: Op 1 'OKLogical -> SVal -> SVal
logicalUnop :: Op 1 'OKLogical -> SVal -> SVal
logicalUnop = \case
  Op 1 'OKLogical
OpNot -> SVal -> SVal
SBV.svNot

logicalBinop :: Op 2 'OKLogical -> SVal -> SVal -> SVal
logicalBinop :: Op 2 'OKLogical -> SVal -> SVal -> SVal
logicalBinop = \case
  Op 2 'OKLogical
OpAnd -> SVal -> SVal -> SVal
SBV.svAnd
  Op 2 'OKLogical
OpOr -> SVal -> SVal -> SVal
SBV.svOr
  Op 2 'OKLogical
OpEquiv -> SVal -> SVal -> SVal
svEquiv
  Op 2 'OKLogical
OpNotEquiv -> SVal -> SVal -> SVal
svNotEquiv
  where
    svEquiv :: SVal -> SVal -> SVal
svEquiv SVal
x SVal
y = (SVal
x SVal -> SVal -> SVal
`SBV.svAnd` SVal
y) SVal -> SVal -> SVal
`SBV.svOr` (SVal -> SVal
SBV.svNot SVal
x SVal -> SVal -> SVal
`SBV.svAnd` SVal -> SVal
SBV.svNot SVal
y)
    svNotEquiv :: SVal -> SVal -> SVal
svNotEquiv SVal
x SVal
y = SVal -> SVal
SBV.svNot (SVal
x SVal -> SVal -> SVal
`svEquiv` SVal
y)

--------------------------------------------------------------------------------
--  Equality
--------------------------------------------------------------------------------

-- TODO: Worry about what happens when LHS and RHS have different types

eqBinop :: ComparableBasicTypes k1 k2 -> Op 2 'OKEq -> SVal -> SVal -> SVal
eqBinop :: forall (k1 :: BasicType) (k2 :: BasicType).
ComparableBasicTypes k1 k2 -> Op 2 'OKEq -> SVal -> SVal -> SVal
eqBinop ComparableBasicTypes k1 k2
_ = \case
  Op 2 'OKEq
OpEq -> SVal -> SVal -> SVal
SBV.svEqual
  Op 2 'OKEq
OpNE -> SVal -> SVal -> SVal
SBV.svNotEqual

--------------------------------------------------------------------------------
--  Relational
--------------------------------------------------------------------------------

-- TODO: Worry about what happens when LHS and RHS have different types

relBinop :: ComparableBasicTypes k1 k2 -> Op 2 'OKRel -> SVal -> SVal -> SVal
relBinop :: forall (k1 :: BasicType) (k2 :: BasicType).
ComparableBasicTypes k1 k2 -> Op 2 'OKRel -> SVal -> SVal -> SVal
relBinop ComparableBasicTypes k1 k2
_ = \case
  Op 2 'OKRel
OpLT -> SVal -> SVal -> SVal
SBV.svLessThan
  Op 2 'OKRel
OpLE -> SVal -> SVal -> SVal
SBV.svLessEq
  Op 2 'OKRel
OpGT -> SVal -> SVal -> SVal
SBV.svGreaterThan
  Op 2 'OKRel
OpGE -> SVal -> SVal -> SVal
SBV.svGreaterEq

--------------------------------------------------------------------------------
--  Lookup
--------------------------------------------------------------------------------

lookupArrRepr
  :: CoreRepr i
  -> D (Array i v)
  -> ArrRepr i v
  -> CoreRepr v
lookupArrRepr :: forall i v.
CoreRepr i -> D (Array i v) -> ArrRepr i v -> CoreRepr v
lookupArrRepr CoreRepr i
ixRepr (DArray ixIndex :: Index i
ixIndex@(Index Prim p 'BTInt a1
_) ArrValue a1
valAV) ArrRepr i v
arrRepr =
  case CoreRepr i
ixRepr of
    CRPrim D (PrimS a1)
_ SVal
ixVal -> case (ArrValue a1
valAV, ArrRepr i v
arrRepr) of
      (ArrPrim Prim p k a1
_, ARPrim SArr
arr) ->
        D (PrimS a1) -> SVal -> CoreRepr (PrimS a1)
forall a1. D (PrimS a1) -> SVal -> CoreRepr (PrimS a1)
CRPrim (ArrValue (PrimS a1) -> D (PrimS a1)
forall a. ArrValue a -> D a
dArrValue ArrValue a1
ArrValue (PrimS a1)
valAV) (SArr -> SVal -> SVal
SBV.readSArr SArr
arr SVal
ixVal)
      (ArrData SSymbol name
_ Rec (Field ArrValue) fs
dfields, ARData Rec (Field (ArrRepr i)) fs
afields) ->
        let avD :: D a1
avD = (ArrValue a1 -> D a1
forall a. ArrValue a -> D a
dArrValue ArrValue a1
valAV)
        in D (Record name fs)
-> Rec (Field CoreRepr) fs -> CoreRepr (Record name fs)
forall (name :: Symbol) (fs :: [(Symbol, *)]).
D (Record name fs)
-> Rec (Field CoreRepr) fs -> CoreRepr (Record name fs)
CRData D a1
D (Record name fs)
avD (
          (forall (x :: (Symbol, *)).
 Field ArrValue x -> Field (ArrRepr i) x -> Field CoreRepr x)
-> Rec (Field ArrValue) fs
-> Rec (Field (ArrRepr i)) fs
-> Rec (Field CoreRepr) fs
forall {u} (xs :: [u]) (f :: u -> *) (g :: u -> *) (h :: u -> *).
(RMap xs, RApply xs) =>
(forall (x :: u). f x -> g x -> h x)
-> Rec f xs -> Rec g xs -> Rec h xs
rzipWith
          ((forall a. ArrValue a -> ArrRepr (PrimS a1) a -> CoreRepr a)
-> Field ArrValue x
-> Field (ArrRepr (PrimS a1)) x
-> Field CoreRepr x
forall {k} (f :: k -> *) (g :: k -> *) (h :: k -> *)
       (nv :: (Symbol, k)).
(forall (a :: k). f a -> g a -> h a)
-> Field f nv -> Field g nv -> Field h nv
zipFieldsWith (CoreRepr i -> D (Array i a) -> ArrRepr i a -> CoreRepr a
forall i v.
CoreRepr i -> D (Array i v) -> ArrRepr i v -> CoreRepr v
lookupArrRepr CoreRepr i
ixRepr (D (Array i a) -> ArrRepr (PrimS a1) a -> CoreRepr a)
-> (ArrValue a -> D (Array i a))
-> ArrValue a
-> ArrRepr (PrimS a1) a
-> CoreRepr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index i -> ArrValue a -> D (Array i a)
forall i a1. Index i -> ArrValue a1 -> D (Array i a1)
DArray Index i
Index i
ixIndex))
          Rec (Field ArrValue) fs
dfields
          Rec (Field (ArrRepr i)) fs
Rec (Field (ArrRepr i)) fs
afields)

lookupArr
  :: CoreRepr (Array i v)
  -> CoreRepr i
  -> CoreRepr v
lookupArr :: forall i v. CoreRepr (Array i v) -> CoreRepr i -> CoreRepr v
lookupArr (CRArray D (Array i a1)
arrD ArrRepr i a1
arrRepr) CoreRepr i
ixRepr = CoreRepr i -> D (Array i v) -> ArrRepr i v -> CoreRepr v
forall i v.
CoreRepr i -> D (Array i v) -> ArrRepr i v -> CoreRepr v
lookupArrRepr CoreRepr i
ixRepr D (Array i a1)
D (Array i v)
arrD ArrRepr i a1
ArrRepr i v
arrRepr

--------------------------------------------------------------------------------
--  Deref
--------------------------------------------------------------------------------

derefData
  :: forall a fname fields i rname. RElem '(fname, a) fields i
  => SSymbol fname
  -> CoreRepr (Record rname fields)
  -> CoreRepr a
derefData :: forall a (fname :: Symbol) (fields :: [(Symbol, *)]) (i :: Nat)
       (rname :: Symbol).
RElem '(fname, a) fields i =>
SSymbol fname -> CoreRepr (Record rname fields) -> CoreRepr a
derefData SSymbol fname
_ (CRData D (Record name fs)
_ Rec (Field CoreRepr) fs
dataRec) =
      case forall {k} (r :: k) (rs :: [k]) (f :: k -> *)
       (record :: (k -> *) -> [k] -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f) =>
record f rs -> f r
forall (r :: (Symbol, *)) (rs :: [(Symbol, *)])
       (f :: (Symbol, *) -> *)
       (record :: ((Symbol, *) -> *) -> [(Symbol, *)] -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f) =>
record f rs -> f r
rget @'(fname, a) @fields Rec (Field CoreRepr) fields
Rec (Field CoreRepr) fs
dataRec of
    Field SSymbol name
_ CoreRepr a
x -> CoreRepr a
CoreRepr a
x

--------------------------------------------------------------------------------
--  Equality of operators
--------------------------------------------------------------------------------

-- eqOpRArgs
--   :: (forall x y. (x -> y -> Bool) -> f x -> g y -> Bool)
--   -> OpSpec ok1 args1 r1
--   -> OpSpec ok2 args2 r2
--   -> Rec f args1
--   -> Rec g args2
--   -> Bool
-- eqOpRArgs le opr1 opr2 =
--   case (opr1, opr2) of
--     (OSLit _ _, OSLit _ _) -> \_ _ -> True
--     (OSNum1 _ px _, OSNum1 _ py _) -> runcurry $ runcurry . le (eqPrimS px py)
--     (OSNum2 _ _ px1 px2 _, OSNum2 _ _ py1 py2 _) ->
--       runcurry $ \x1 x2 -> runcurry $ \y1 y2 ->
--       le (eqPrimS px1 py1) x1 y1 && le (eqPrimS px2 py2) x2 y2
--     (OSLogical1 px _, OSLogical1 py _) -> runcurry $ runcurry . le (eqPrimS px py)
--     (OSLogical2 px1 px2 _, OSLogical2 py1 py2 _) ->
--       runcurry $ \x1 x2 -> runcurry $ \y1 y2 ->
--       le (eqPrimS px1 py1) x1 y1 && le (eqPrimS px2 py2) x2 y2
--     (OSEq _ px1 px2 _, OSEq _ py1 py2 _) ->
--       runcurry $ \x1 x2 -> runcurry $ \y1 y2 ->
--       le (eqPrimS px1 py1) x1 y1 && le (eqPrimS px2 py2) x2 y2
--     (OSRel _ px1 px2 _, OSRel _ py1 py2 _) ->
--       runcurry $ \x1 x2 -> runcurry $ \y1 y2 ->
--       le (eqPrimS px1 py1) x1 y1 && le (eqPrimS px2 py2) x2 y2
--     (OSLookup (DArray (Index pi1) _), OSLookup (DArray (Index pi2) _)) ->
--       runcurry $ \arr1 i1 -> runcurry $ \arr2 i2 ->
--       le _ arr1 arr2 && le (eqPrimS pi1 pi2) i1 i2
--       -- le ()

-- liftEqRec
--   :: (forall a b. f a -> g b -> Bool)
--   -> Rec f xs -> Rec g ys
--   -> Bool
-- liftEqRec f r1 r2 = case (r1, r2) of
--   (RNil, RNil) -> True
--   (h1 :& t1, h2 :& t2) -> f h1 h2 && liftEqRec f t1 t2
--   _ -> False