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