{-# 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       #-}

{-# 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

import           Data.Singletons
import           Data.Singletons.Prelude.List
import           Data.Singletons.TypeLits

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 :: 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 (PrimS a)) -> m SVal -> m (CoreRepr (PrimS a))
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_6989586621679837482
        p1
        p2
        (Case_6989586621679837434
           p1 p2 (Compare_6989586621679394002 p1 p2)))
     (Case_6989586621679837482
        k1
        k2
        (Case_6989586621679837434
           k1 k2 (Compare_6989586621679394011 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_6989586621679837482
     p1
     p2
     (Case_6989586621679837434
        p1 p2 (Compare_6989586621679394002 p1 p2)))
  (Case_6989586621679837482
     k1
     k2
     (Case_6989586621679837434
        k1 k2 (Compare_6989586621679394011 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 (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)
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 (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 :: CoreRepr (PrimS a) -> SVal
primToVal = \case
  CRPrim (DPrim Prim p k a
_) SVal
v -> SVal
v

primFromVal :: Prim p k a -> SVal -> CoreRepr (PrimS a)
primFromVal :: Prim p k a -> SVal -> CoreRepr (PrimS a)
primFromVal Prim p k a
p SVal
v = D (PrimS a) -> SVal -> CoreRepr (PrimS a)
forall a. D (PrimS a) -> SVal -> CoreRepr (PrimS a)
CRPrim (Prim p k a -> D (PrimS a)
forall (p :: Precision) (k :: BasicType) a.
Prim p k a -> D (PrimS a)
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 :: 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 (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 (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 :: 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 (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 (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_6989586621679837482
     p1
     p2
     (Case_6989586621679837434
        p1 p2 (Compare_6989586621679394002 p1 p2)))
  (Case_6989586621679837482
     k1
     k2
     (Case_6989586621679837434
        k1 k2 (Compare_6989586621679394011 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_6989586621679837482
     p1
     p2
     (Case_6989586621679837434
        p1 p2 (Compare_6989586621679394002 p1 p2)))
  (Case_6989586621679837482
     k1
     k2
     (Case_6989586621679837434
        k1 k2 (Compare_6989586621679394011 k1 k2)))
  a
Prim (PrecMax p1 p2) (BasicTypeMax k1 k2) a
pCeil
      Maybe (MakePrim (PrecMax p1 p2) (BasicTypeMax k1 k2))
_                     -> SVal -> m SVal
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 :: 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 :: 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 :: 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 :: CoreRepr i -> D (Array i v) -> ArrRepr i v -> CoreRepr v
lookupArrRepr CoreRepr i
ixRepr (DArray ixIndex :: Index i
ixIndex@(Index Prim p 'BTInt a
_) ArrValue a
valAV) ArrRepr i v
arrRepr =
  case CoreRepr i
ixRepr of
    CRPrim D (PrimS a)
_ SVal
ixVal -> case (ArrValue a
valAV, ArrRepr i v
arrRepr) of
      (ArrPrim Prim p k a
_, ARPrim SArr
arr) ->
        D (PrimS a) -> SVal -> CoreRepr (PrimS a)
forall a. D (PrimS a) -> SVal -> CoreRepr (PrimS a)
CRPrim (ArrValue a -> D a
forall a. ArrValue a -> D a
dArrValue ArrValue a
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 a
avD = (ArrValue a -> D a
forall a. ArrValue a -> D a
dArrValue ArrValue a
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 a
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 a) a -> CoreRepr a)
-> Field ArrValue x
-> Field (ArrRepr (PrimS a)) 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 i a -> CoreRepr a)
-> (ArrValue a -> D (Array i a))
-> ArrValue a
-> ArrRepr i a
-> CoreRepr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index i -> ArrValue a -> D (Array i a)
forall i a. Index i -> ArrValue a -> D (Array i a)
DArray 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 :: CoreRepr (Array i v) -> CoreRepr i -> CoreRepr v
lookupArr (CRArray D (Array i a)
arrD ArrRepr i a
arrRepr) CoreRepr i
ixRepr = 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)
D (Array i a)
arrD ArrRepr i a
ArrRepr i a
arrRepr

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

derefData
  :: forall a fname fields i rname. RElem '(fname, a) fields i
  => SSymbol fname
  -> CoreRepr (Record rname fields)
  -> CoreRepr a
derefData :: SSymbol fname -> CoreRepr (Record rname fields) -> CoreRepr a
derefData SSymbol fname
_ (CRData D (Record name fs)
_ Rec (Field CoreRepr) fs
dataRec) =
      case Rec (Field CoreRepr) fields -> Field CoreRepr '(fname, a)
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
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