{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE EmptyCase                  #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE FunctionalDependencies     #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures             #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE PolyKinds                  #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE ScopedTypeVariables        #-}

{-# OPTIONS_GHC -Wall #-}


{-|

Symbolic representations of Fortran values, for symbolic reasoning.

There is a distinction between core representations ('CoreRepr') and high-level
representations ('HighRepr'). 'CoreRepr' represents any @a@ such that @'D' a@
exists; i.e. anything with a corresponding Fortran type. 'HighRepr' is a
superset of 'CoreRepr'. It represents Fortran types, and also higher-level types
that facilitate reasoning. There is more information about this distinction in
"Language.Fortran.Model.Op".

-}
module Language.Fortran.Model.Repr where

import           Data.Int                        (Int16, Int32, Int64, Int8)
import           Data.Word                       (Word8)

import           Data.Functor.Compose

import           Data.SBV
import           Data.SBV.Dynamic
import           Data.SBV.Internals              (SBV (..))

import           Data.Vinyl                      hiding (Field)

import           Language.Expression
import           Language.Expression.Prop

import           Language.Fortran.Model.Repr.Prim
import           Language.Fortran.Model.Types

--------------------------------------------------------------------------------
-- * Core Fortran Representations

{-|

Symbolic representations of Fortran values, using "Data.SBV.Dynamic".

-}
data CoreRepr a where
  CRPrim
    :: D (PrimS a)
    -> SVal
    -> CoreRepr (PrimS a)

  CRArray
    :: D (Array i a)
    -> ArrRepr i a
    -> CoreRepr (Array i a)

  CRData
    :: D (Record name fs)
    -> Rec (Field CoreRepr) fs
    -> CoreRepr (Record name fs)

{-|

Symbolic respresentations of Fortran arrays. SBV arrays can only contain basic
values, so in order to represent arrays of derived data types, we use multiple
flat arrays, one for each basic field. Nested derived data types are recursively
expanded.

Arrays of arrays are not yet supported.

-}
data ArrRepr i a where
  -- | A primitive type is represented by a flat 'SArr'.
  ARPrim :: SArr -> ArrRepr i (PrimS a)

  -- | A derived data type is represented by a record of 'ArrRepr's over the
  -- record's fields.
  ARData :: Rec (Field (ArrRepr i)) fs -> ArrRepr i (Record name fs)


--------------------------------------------------------------------------------
-- * High-level data representations

{-|

Symbolic representations of Fortran values plus types in the higher-level
meta-language (see "Language.Fortran.Op" for more information).

-}
data HighRepr a where
  HRCore :: CoreRepr a -> HighRepr a
  HRHigh :: SBV a -> HighRepr a

instance HFoldableAt HighRepr LogicOp where
  hfoldMap :: (forall b. t b -> HighRepr b) -> LogicOp t a -> HighRepr a
hfoldMap = (LogicOp HighRepr a -> HighRepr a)
-> (forall b. t b -> HighRepr b) -> LogicOp t a -> HighRepr a
forall u (h :: (u -> *) -> u -> *) (k :: u -> *) (a :: u)
       (t :: u -> *).
HFunctor h =>
(h k a -> k a) -> (forall (b :: u). t b -> k b) -> h t a -> k a
implHfoldMap ((LogicOp HighRepr a -> HighRepr a)
 -> (forall b. t b -> HighRepr b) -> LogicOp t a -> HighRepr a)
-> (LogicOp HighRepr a -> HighRepr a)
-> (forall b. t b -> HighRepr b)
-> LogicOp t a
-> HighRepr a
forall a b. (a -> b) -> a -> b
$ \case
    LogLit Bool
x     -> SBV Bool -> HighRepr Bool
forall a. SBV a -> HighRepr a
HRHigh (Bool -> SBV Bool
fromBool Bool
x)
    LogNot HighRepr Bool
x     -> SBV Bool -> HighRepr Bool
forall a. SBV a -> HighRepr a
HRHigh (SBV Bool -> HighRepr Bool)
-> (HighRepr Bool -> SBV Bool) -> HighRepr Bool -> HighRepr Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV Bool -> SBV Bool
sNot (SBV Bool -> SBV Bool)
-> (HighRepr Bool -> SBV Bool) -> HighRepr Bool -> SBV Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HighRepr Bool -> SBV Bool
getHrBool (HighRepr Bool -> HighRepr Bool) -> HighRepr Bool -> HighRepr Bool
forall a b. (a -> b) -> a -> b
$ HighRepr Bool
x
    LogAnd HighRepr Bool
x HighRepr Bool
y   -> (SBV Bool -> SBV Bool -> SBV Bool)
-> HighRepr Bool -> HighRepr Bool -> HighRepr Bool
appBinop SBV Bool -> SBV Bool -> SBV Bool
(.&&) HighRepr Bool
x HighRepr Bool
y
    LogOr HighRepr Bool
x HighRepr Bool
y    -> (SBV Bool -> SBV Bool -> SBV Bool)
-> HighRepr Bool -> HighRepr Bool -> HighRepr Bool
appBinop SBV Bool -> SBV Bool -> SBV Bool
(.||) HighRepr Bool
x HighRepr Bool
y
    LogImpl HighRepr Bool
x HighRepr Bool
y  -> (SBV Bool -> SBV Bool -> SBV Bool)
-> HighRepr Bool -> HighRepr Bool -> HighRepr Bool
appBinop SBV Bool -> SBV Bool -> SBV Bool
(.=>) HighRepr Bool
x HighRepr Bool
y
    LogEquiv HighRepr Bool
x HighRepr Bool
y -> (SBV Bool -> SBV Bool -> SBV Bool)
-> HighRepr Bool -> HighRepr Bool -> HighRepr Bool
appBinop SBV Bool -> SBV Bool -> SBV Bool
(.<=>) HighRepr Bool
x HighRepr Bool
y

    where
      appBinop :: (SBV Bool -> SBV Bool -> SBV Bool)
-> HighRepr Bool -> HighRepr Bool -> HighRepr Bool
appBinop (SBV Bool -> SBV Bool -> SBV Bool
g :: SBool -> SBool -> SBool) HighRepr Bool
x HighRepr Bool
y =
        SBV Bool -> HighRepr Bool
forall a. SBV a -> HighRepr a
HRHigh (SBV Bool -> HighRepr Bool) -> SBV Bool -> HighRepr Bool
forall a b. (a -> b) -> a -> b
$ SBV Bool -> SBV Bool -> SBV Bool
g (HighRepr Bool -> SBV Bool
getHrBool HighRepr Bool
x) (HighRepr Bool -> SBV Bool
getHrBool HighRepr Bool
y)
      getHrBool :: HighRepr Bool -> SBool
      getHrBool :: HighRepr Bool -> SBV Bool
getHrBool (HRHigh SBV Bool
x) = SBV Bool
x
      getHrBool (HRCore CoreRepr Bool
x) = case CoreRepr Bool
x of -- I.e. absurd

instance (Monad m) => HFoldableAt (Compose m HighRepr) LogicOp where
  hfoldMap :: (forall b. t b -> Compose m HighRepr b)
-> LogicOp t a -> Compose m HighRepr a
hfoldMap = (LogicOp HighRepr a -> m (HighRepr a))
-> (forall b. t b -> Compose m HighRepr b)
-> LogicOp t a
-> Compose m HighRepr a
forall k1 (h :: (k1 -> *) -> k1 -> *) (m :: * -> *) (k :: k1 -> *)
       (a :: k1) (t :: k1 -> *).
(HTraversable h, Monad m) =>
(h k a -> m (k a))
-> (forall (b :: k1). t b -> Compose m k b)
-> h t a
-> Compose m k a
implHfoldMapCompose (HighRepr a -> m (HighRepr a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HighRepr a -> m (HighRepr a))
-> (LogicOp HighRepr a -> HighRepr a)
-> LogicOp HighRepr a
-> m (HighRepr a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LogicOp HighRepr a -> HighRepr a
forall k (t :: k -> *) (h :: (k -> *) -> k -> *) (a :: k).
HFoldableAt t h =>
h t a -> t a
hfold)

--------------------------------------------------------------------------------
-- *  Lifting Fortran types to high-level representations

-- | Provides conversions between symbolic representations of core Fortran
-- values and their corresponding high-level types.
class (SymVal a) => LiftD b a | b -> a where
  -- | Go from a core value to the corresponding high-level value.
  liftD :: b -> a
  -- | Go from a symbolic core value to the corresponding symbolic high-level
  -- value.
  liftDRepr :: PrimReprHandlers -> HighRepr b -> HighRepr a

liftDInt :: PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr Integer
liftDInt :: PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr Integer
liftDInt PrimReprHandlers
_ (HRCore (CRPrim D (PrimS a)
_ SVal
x)) = SBV Integer -> HighRepr Integer
forall a. SBV a -> HighRepr a
HRHigh (SVal -> SBV Integer
forall a. SVal -> SBV a
SBV (Kind -> SVal -> SVal
svFromIntegral Kind
KUnbounded SVal
x))
liftDInt PrimReprHandlers
_ HighRepr (PrimS a)
_ = [Char] -> HighRepr Integer
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible"


liftDReal :: PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr AlgReal
liftDReal :: PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr AlgReal
liftDReal PrimReprHandlers
env (HRCore (CRPrim (DPrim Prim p k a
prim) SVal
x)) =
  SBV AlgReal -> HighRepr AlgReal
forall a. SBV a -> HighRepr a
HRHigh (SBV AlgReal -> HighRepr AlgReal)
-> SBV AlgReal -> HighRepr AlgReal
forall a b. (a -> b) -> a -> b
$ case Prim p k a -> PrimReprHandlers -> Kind
forall r (m :: * -> *) (p :: Precision) (k :: BasicType) a.
(MonadReader r m, HasPrimReprHandlers r) =>
Prim p k a -> m Kind
primSBVKind Prim p k a
prim PrimReprHandlers
env of
              Kind
KFloat -> SRoundingMode -> SFloat -> SBV AlgReal
forall a.
IEEEFloatConvertible a =>
SRoundingMode -> SFloat -> SBV a
fromSFloat SRoundingMode
sRTZ (SVal -> SFloat
forall a. SVal -> SBV a
SBV SVal
x)
              Kind
KDouble -> SRoundingMode -> SDouble -> SBV AlgReal
forall a.
IEEEFloatConvertible a =>
SRoundingMode -> SDouble -> SBV a
fromSDouble SRoundingMode
sRTZ (SVal -> SDouble
forall a. SVal -> SBV a
SBV SVal
x)
              Kind
KReal -> SVal -> SBV AlgReal
forall a. SVal -> SBV a
SBV SVal
x
              Kind
k -> [Char] -> SBV AlgReal
forall a. HasCallStack => [Char] -> a
error ([Char] -> SBV AlgReal) -> [Char] -> SBV AlgReal
forall a b. (a -> b) -> a -> b
$ [Char]
"liftDReal: can't convert something of kind " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                   Kind -> [Char]
forall a. Show a => a -> [Char]
show Kind
k [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" to a real"
liftDReal PrimReprHandlers
_ HighRepr (PrimS a)
_ = [Char] -> HighRepr AlgReal
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible"

liftDBool :: PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr Bool
liftDBool :: PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr Bool
liftDBool PrimReprHandlers
_ (HRCore (CRPrim D (PrimS a)
_ SVal
x)) = SBV Bool -> HighRepr Bool
forall a. SBV a -> HighRepr a
HRHigh (SVal -> SBV Bool
forall a. SVal -> SBV a
SBV (SVal
x SVal -> SVal -> SVal
`svGreaterThan` SVal
svFalse))
liftDBool PrimReprHandlers
_ HighRepr (PrimS a)
_ = [Char] -> HighRepr Bool
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible"


instance LiftD (PrimS Int8) Integer where
  liftD :: PrimS Int8 -> Integer
liftD = Int8 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int8 -> Integer) -> (PrimS Int8 -> Int8) -> PrimS Int8 -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimS Int8 -> Int8
forall a. PrimS a -> a
getPrimS
  liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Int8) -> HighRepr Integer
liftDRepr = PrimReprHandlers -> HighRepr (PrimS Int8) -> HighRepr Integer
forall a.
PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr Integer
liftDInt
instance LiftD (PrimS Int16) Integer where
  liftD :: PrimS Int16 -> Integer
liftD = Int16 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int16 -> Integer)
-> (PrimS Int16 -> Int16) -> PrimS Int16 -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimS Int16 -> Int16
forall a. PrimS a -> a
getPrimS
  liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Int16) -> HighRepr Integer
liftDRepr = PrimReprHandlers -> HighRepr (PrimS Int16) -> HighRepr Integer
forall a.
PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr Integer
liftDInt
instance LiftD (PrimS Int32) Integer where
  liftD :: PrimS Int32 -> Integer
liftD = Int32 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int32 -> Integer)
-> (PrimS Int32 -> Int32) -> PrimS Int32 -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimS Int32 -> Int32
forall a. PrimS a -> a
getPrimS
  liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Int32) -> HighRepr Integer
liftDRepr = PrimReprHandlers -> HighRepr (PrimS Int32) -> HighRepr Integer
forall a.
PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr Integer
liftDInt
instance LiftD (PrimS Int64) Integer where
  liftD :: PrimS Int64 -> Integer
liftD = Int64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int64 -> Integer)
-> (PrimS Int64 -> Int64) -> PrimS Int64 -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimS Int64 -> Int64
forall a. PrimS a -> a
getPrimS
  liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Int64) -> HighRepr Integer
liftDRepr = PrimReprHandlers -> HighRepr (PrimS Int64) -> HighRepr Integer
forall a.
PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr Integer
liftDInt

instance LiftD (PrimS Float) AlgReal where
  liftD :: PrimS Float -> AlgReal
liftD = Float -> AlgReal
forall a b. (Real a, Fractional b) => a -> b
realToFrac (Float -> AlgReal)
-> (PrimS Float -> Float) -> PrimS Float -> AlgReal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimS Float -> Float
forall a. PrimS a -> a
getPrimS
  liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Float) -> HighRepr AlgReal
liftDRepr = PrimReprHandlers -> HighRepr (PrimS Float) -> HighRepr AlgReal
forall a.
PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr AlgReal
liftDReal
instance LiftD (PrimS Double) AlgReal where
  liftD :: PrimS Double -> AlgReal
liftD = Double -> AlgReal
forall a b. (Real a, Fractional b) => a -> b
realToFrac (Double -> AlgReal)
-> (PrimS Double -> Double) -> PrimS Double -> AlgReal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimS Double -> Double
forall a. PrimS a -> a
getPrimS
  liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Double) -> HighRepr AlgReal
liftDRepr = PrimReprHandlers -> HighRepr (PrimS Double) -> HighRepr AlgReal
forall a.
PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr AlgReal
liftDReal

instance LiftD (PrimS Bool8) Bool where
  liftD :: PrimS Bool8 -> Bool
liftD = (Int8 -> Int8 -> Bool
forall a. Ord a => a -> a -> Bool
> Int8
0) (Int8 -> Bool) -> (PrimS Bool8 -> Int8) -> PrimS Bool8 -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool8 -> Int8
getBool8 (Bool8 -> Int8) -> (PrimS Bool8 -> Bool8) -> PrimS Bool8 -> Int8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimS Bool8 -> Bool8
forall a. PrimS a -> a
getPrimS
  liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Bool8) -> HighRepr Bool
liftDRepr = PrimReprHandlers -> HighRepr (PrimS Bool8) -> HighRepr Bool
forall a. PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr Bool
liftDBool
instance LiftD (PrimS Bool16) Bool where
  liftD :: PrimS Bool16 -> Bool
liftD = (Int16 -> Int16 -> Bool
forall a. Ord a => a -> a -> Bool
> Int16
0) (Int16 -> Bool) -> (PrimS Bool16 -> Int16) -> PrimS Bool16 -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool16 -> Int16
getBool16 (Bool16 -> Int16)
-> (PrimS Bool16 -> Bool16) -> PrimS Bool16 -> Int16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimS Bool16 -> Bool16
forall a. PrimS a -> a
getPrimS
  liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Bool16) -> HighRepr Bool
liftDRepr = PrimReprHandlers -> HighRepr (PrimS Bool16) -> HighRepr Bool
forall a. PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr Bool
liftDBool
instance LiftD (PrimS Bool32) Bool where
  liftD :: PrimS Bool32 -> Bool
liftD = (Int32 -> Int32 -> Bool
forall a. Ord a => a -> a -> Bool
> Int32
0) (Int32 -> Bool) -> (PrimS Bool32 -> Int32) -> PrimS Bool32 -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool32 -> Int32
getBool32 (Bool32 -> Int32)
-> (PrimS Bool32 -> Bool32) -> PrimS Bool32 -> Int32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimS Bool32 -> Bool32
forall a. PrimS a -> a
getPrimS
  liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Bool32) -> HighRepr Bool
liftDRepr = PrimReprHandlers -> HighRepr (PrimS Bool32) -> HighRepr Bool
forall a. PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr Bool
liftDBool
instance LiftD (PrimS Bool64) Bool where
  liftD :: PrimS Bool64 -> Bool
liftD = (Int64 -> Int64 -> Bool
forall a. Ord a => a -> a -> Bool
> Int64
0) (Int64 -> Bool) -> (PrimS Bool64 -> Int64) -> PrimS Bool64 -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool64 -> Int64
getBool64 (Bool64 -> Int64)
-> (PrimS Bool64 -> Bool64) -> PrimS Bool64 -> Int64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimS Bool64 -> Bool64
forall a. PrimS a -> a
getPrimS
  liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Bool64) -> HighRepr Bool
liftDRepr = PrimReprHandlers -> HighRepr (PrimS Bool64) -> HighRepr Bool
forall a. PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr Bool
liftDBool

instance LiftD (PrimS Char8) Word8 where
  liftD :: PrimS Char8 -> Word8
liftD = Char8 -> Word8
getChar8 (Char8 -> Word8) -> (PrimS Char8 -> Char8) -> PrimS Char8 -> Word8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimS Char8 -> Char8
forall a. PrimS a -> a
getPrimS
  liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Char8) -> HighRepr Word8
liftDRepr PrimReprHandlers
_ (HRCore (CRPrim D (PrimS a)
_ SVal
x)) = SBV Word8 -> HighRepr Word8
forall a. SBV a -> HighRepr a
HRHigh (SBV Word8 -> SBV Word8
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral (SVal -> SBV Word8
forall a. SVal -> SBV a
SBV SVal
x :: SBV Word8))
  liftDRepr PrimReprHandlers
_ HighRepr (PrimS Char8)
_ =
    [Char] -> HighRepr Word8
forall a. HasCallStack => [Char] -> a
error [Char]
"liftDRepr: a 'PrimS Char8' has a non-primitive representation"

--------------------------------------------------------------------------------
-- * Combinators

-- | Any type that has a core representation has a corresponding Fortran type.
coreReprD :: CoreRepr a -> D a
coreReprD :: CoreRepr a -> D a
coreReprD = \case
  CRPrim D (PrimS a)
d SVal
_  -> D a
D (PrimS a)
d
  CRArray D (Array i a)
d ArrRepr i a
_ -> D a
D (Array i a)
d
  CRData D (Record name fs)
d Rec (Field CoreRepr) fs
_  -> D a
D (Record name fs)
d