{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TemplateHaskell       #-}

{-# OPTIONS_GHC -Wall      #-}

{-|

= Handling primitive Fortran values symbolically.

There are a few challenges that this module attempts to solve:

Fortran uses fixed-width machine integers and floating point reals. Sometimes we
might want to reason about these directly (which is supported by SBV and
therefore feasible). However, sometimes they get in the way of the logic and we
just want to pretend that they're the pure mathematical values that they
approximate. For example floating point addition obeys very few algebraic laws,
so most theorems about real numbers don't hold at all for floating point
numbers.

In addition, Fortran's boolean values are actually arbitrary signed integers. If
we treat all boolean values symbolically as bit-vectors, logic can become very
slow; so it might be best to pretend that all booleans are single bits. However,
sometimes we might want to verify properties that rely on the actual bit-vector
representation of booleans.

This module deals with these problems by abstracting over the choices: the user
should be able to choose which representation they want to use for each
primitive data type.

The user provides a 'PrimReprSpec' which specifies how each data type should be
treated. Some examples are provided: 'prsPrecise' treats all values precisely as
they are represented in the Fortran program. This makes logic slow and makes it
very difficult to prove many things, but it is most accurate. On the other hand,
'prsIdealized' treats all values as their idealized mathematical equivalents.
This makes logic fast and lots intuitive properties can be proved easily.
However, these properties often will not hold in actual running Fortran
programs: sometimes in weird edge cases and sometimes in sensible-seeming
executions. It would be interesting future work to provide an analysis that
helps to determine which of the two applies to a particular program!

-}
module Language.Fortran.Model.Repr.Prim where

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

import           Control.Lens
import           Control.Monad.Reader             (MonadReader (..))

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

import           Language.Fortran.Model.Types

--------------------------------------------------------------------------------
-- * Types

data IntRepr a = MachineInt | ArbitraryInt deriving (IntRepr a -> IntRepr a -> Bool
(IntRepr a -> IntRepr a -> Bool)
-> (IntRepr a -> IntRepr a -> Bool) -> Eq (IntRepr a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (a :: k). IntRepr a -> IntRepr a -> Bool
/= :: IntRepr a -> IntRepr a -> Bool
$c/= :: forall k (a :: k). IntRepr a -> IntRepr a -> Bool
== :: IntRepr a -> IntRepr a -> Bool
$c== :: forall k (a :: k). IntRepr a -> IntRepr a -> Bool
Eq, Eq (IntRepr a)
Eq (IntRepr a)
-> (IntRepr a -> IntRepr a -> Ordering)
-> (IntRepr a -> IntRepr a -> Bool)
-> (IntRepr a -> IntRepr a -> Bool)
-> (IntRepr a -> IntRepr a -> Bool)
-> (IntRepr a -> IntRepr a -> Bool)
-> (IntRepr a -> IntRepr a -> IntRepr a)
-> (IntRepr a -> IntRepr a -> IntRepr a)
-> Ord (IntRepr a)
IntRepr a -> IntRepr a -> Bool
IntRepr a -> IntRepr a -> Ordering
IntRepr a -> IntRepr a -> IntRepr a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k (a :: k). Eq (IntRepr a)
forall k (a :: k). IntRepr a -> IntRepr a -> Bool
forall k (a :: k). IntRepr a -> IntRepr a -> Ordering
forall k (a :: k). IntRepr a -> IntRepr a -> IntRepr a
min :: IntRepr a -> IntRepr a -> IntRepr a
$cmin :: forall k (a :: k). IntRepr a -> IntRepr a -> IntRepr a
max :: IntRepr a -> IntRepr a -> IntRepr a
$cmax :: forall k (a :: k). IntRepr a -> IntRepr a -> IntRepr a
>= :: IntRepr a -> IntRepr a -> Bool
$c>= :: forall k (a :: k). IntRepr a -> IntRepr a -> Bool
> :: IntRepr a -> IntRepr a -> Bool
$c> :: forall k (a :: k). IntRepr a -> IntRepr a -> Bool
<= :: IntRepr a -> IntRepr a -> Bool
$c<= :: forall k (a :: k). IntRepr a -> IntRepr a -> Bool
< :: IntRepr a -> IntRepr a -> Bool
$c< :: forall k (a :: k). IntRepr a -> IntRepr a -> Bool
compare :: IntRepr a -> IntRepr a -> Ordering
$ccompare :: forall k (a :: k). IntRepr a -> IntRepr a -> Ordering
$cp1Ord :: forall k (a :: k). Eq (IntRepr a)
Ord, Int -> IntRepr a -> ShowS
[IntRepr a] -> ShowS
IntRepr a -> String
(Int -> IntRepr a -> ShowS)
-> (IntRepr a -> String)
-> ([IntRepr a] -> ShowS)
-> Show (IntRepr a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (a :: k). Int -> IntRepr a -> ShowS
forall k (a :: k). [IntRepr a] -> ShowS
forall k (a :: k). IntRepr a -> String
showList :: [IntRepr a] -> ShowS
$cshowList :: forall k (a :: k). [IntRepr a] -> ShowS
show :: IntRepr a -> String
$cshow :: forall k (a :: k). IntRepr a -> String
showsPrec :: Int -> IntRepr a -> ShowS
$cshowsPrec :: forall k (a :: k). Int -> IntRepr a -> ShowS
Show)
data RealRepr a = MachineFloat | ArbitraryReal deriving (RealRepr a -> RealRepr a -> Bool
(RealRepr a -> RealRepr a -> Bool)
-> (RealRepr a -> RealRepr a -> Bool) -> Eq (RealRepr a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (a :: k). RealRepr a -> RealRepr a -> Bool
/= :: RealRepr a -> RealRepr a -> Bool
$c/= :: forall k (a :: k). RealRepr a -> RealRepr a -> Bool
== :: RealRepr a -> RealRepr a -> Bool
$c== :: forall k (a :: k). RealRepr a -> RealRepr a -> Bool
Eq, Eq (RealRepr a)
Eq (RealRepr a)
-> (RealRepr a -> RealRepr a -> Ordering)
-> (RealRepr a -> RealRepr a -> Bool)
-> (RealRepr a -> RealRepr a -> Bool)
-> (RealRepr a -> RealRepr a -> Bool)
-> (RealRepr a -> RealRepr a -> Bool)
-> (RealRepr a -> RealRepr a -> RealRepr a)
-> (RealRepr a -> RealRepr a -> RealRepr a)
-> Ord (RealRepr a)
RealRepr a -> RealRepr a -> Bool
RealRepr a -> RealRepr a -> Ordering
RealRepr a -> RealRepr a -> RealRepr a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k (a :: k). Eq (RealRepr a)
forall k (a :: k). RealRepr a -> RealRepr a -> Bool
forall k (a :: k). RealRepr a -> RealRepr a -> Ordering
forall k (a :: k). RealRepr a -> RealRepr a -> RealRepr a
min :: RealRepr a -> RealRepr a -> RealRepr a
$cmin :: forall k (a :: k). RealRepr a -> RealRepr a -> RealRepr a
max :: RealRepr a -> RealRepr a -> RealRepr a
$cmax :: forall k (a :: k). RealRepr a -> RealRepr a -> RealRepr a
>= :: RealRepr a -> RealRepr a -> Bool
$c>= :: forall k (a :: k). RealRepr a -> RealRepr a -> Bool
> :: RealRepr a -> RealRepr a -> Bool
$c> :: forall k (a :: k). RealRepr a -> RealRepr a -> Bool
<= :: RealRepr a -> RealRepr a -> Bool
$c<= :: forall k (a :: k). RealRepr a -> RealRepr a -> Bool
< :: RealRepr a -> RealRepr a -> Bool
$c< :: forall k (a :: k). RealRepr a -> RealRepr a -> Bool
compare :: RealRepr a -> RealRepr a -> Ordering
$ccompare :: forall k (a :: k). RealRepr a -> RealRepr a -> Ordering
$cp1Ord :: forall k (a :: k). Eq (RealRepr a)
Ord, Int -> RealRepr a -> ShowS
[RealRepr a] -> ShowS
RealRepr a -> String
(Int -> RealRepr a -> ShowS)
-> (RealRepr a -> String)
-> ([RealRepr a] -> ShowS)
-> Show (RealRepr a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (a :: k). Int -> RealRepr a -> ShowS
forall k (a :: k). [RealRepr a] -> ShowS
forall k (a :: k). RealRepr a -> String
showList :: [RealRepr a] -> ShowS
$cshowList :: forall k (a :: k). [RealRepr a] -> ShowS
show :: RealRepr a -> String
$cshow :: forall k (a :: k). RealRepr a -> String
showsPrec :: Int -> RealRepr a -> ShowS
$cshowsPrec :: forall k (a :: k). Int -> RealRepr a -> ShowS
Show)
data BoolRepr a = IntBool | BitBool deriving (BoolRepr a -> BoolRepr a -> Bool
(BoolRepr a -> BoolRepr a -> Bool)
-> (BoolRepr a -> BoolRepr a -> Bool) -> Eq (BoolRepr a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (a :: k). BoolRepr a -> BoolRepr a -> Bool
/= :: BoolRepr a -> BoolRepr a -> Bool
$c/= :: forall k (a :: k). BoolRepr a -> BoolRepr a -> Bool
== :: BoolRepr a -> BoolRepr a -> Bool
$c== :: forall k (a :: k). BoolRepr a -> BoolRepr a -> Bool
Eq, Eq (BoolRepr a)
Eq (BoolRepr a)
-> (BoolRepr a -> BoolRepr a -> Ordering)
-> (BoolRepr a -> BoolRepr a -> Bool)
-> (BoolRepr a -> BoolRepr a -> Bool)
-> (BoolRepr a -> BoolRepr a -> Bool)
-> (BoolRepr a -> BoolRepr a -> Bool)
-> (BoolRepr a -> BoolRepr a -> BoolRepr a)
-> (BoolRepr a -> BoolRepr a -> BoolRepr a)
-> Ord (BoolRepr a)
BoolRepr a -> BoolRepr a -> Bool
BoolRepr a -> BoolRepr a -> Ordering
BoolRepr a -> BoolRepr a -> BoolRepr a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k (a :: k). Eq (BoolRepr a)
forall k (a :: k). BoolRepr a -> BoolRepr a -> Bool
forall k (a :: k). BoolRepr a -> BoolRepr a -> Ordering
forall k (a :: k). BoolRepr a -> BoolRepr a -> BoolRepr a
min :: BoolRepr a -> BoolRepr a -> BoolRepr a
$cmin :: forall k (a :: k). BoolRepr a -> BoolRepr a -> BoolRepr a
max :: BoolRepr a -> BoolRepr a -> BoolRepr a
$cmax :: forall k (a :: k). BoolRepr a -> BoolRepr a -> BoolRepr a
>= :: BoolRepr a -> BoolRepr a -> Bool
$c>= :: forall k (a :: k). BoolRepr a -> BoolRepr a -> Bool
> :: BoolRepr a -> BoolRepr a -> Bool
$c> :: forall k (a :: k). BoolRepr a -> BoolRepr a -> Bool
<= :: BoolRepr a -> BoolRepr a -> Bool
$c<= :: forall k (a :: k). BoolRepr a -> BoolRepr a -> Bool
< :: BoolRepr a -> BoolRepr a -> Bool
$c< :: forall k (a :: k). BoolRepr a -> BoolRepr a -> Bool
compare :: BoolRepr a -> BoolRepr a -> Ordering
$ccompare :: forall k (a :: k). BoolRepr a -> BoolRepr a -> Ordering
$cp1Ord :: forall k (a :: k). Eq (BoolRepr a)
Ord, Int -> BoolRepr a -> ShowS
[BoolRepr a] -> ShowS
BoolRepr a -> String
(Int -> BoolRepr a -> ShowS)
-> (BoolRepr a -> String)
-> ([BoolRepr a] -> ShowS)
-> Show (BoolRepr a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (a :: k). Int -> BoolRepr a -> ShowS
forall k (a :: k). [BoolRepr a] -> ShowS
forall k (a :: k). BoolRepr a -> String
showList :: [BoolRepr a] -> ShowS
$cshowList :: forall k (a :: k). [BoolRepr a] -> ShowS
show :: BoolRepr a -> String
$cshow :: forall k (a :: k). BoolRepr a -> String
showsPrec :: Int -> BoolRepr a -> ShowS
$cshowsPrec :: forall k (a :: k). Int -> BoolRepr a -> ShowS
Show)

data PrimReprHandler a =
  PrimReprHandler
  { PrimReprHandler a -> Kind
_prhKind     :: !SBV.Kind
  , PrimReprHandler a -> a -> SVal
_prhLiteral  :: !(a -> SVal)
  , PrimReprHandler a -> String -> Symbolic SVal
_prhSymbolic :: !(String -> SBV.Symbolic SVal)
  }

data PrimReprSpec =
  PrimReprSpec
  { PrimReprSpec -> IntRepr Int8
_prsInt8Repr   :: !(IntRepr Int8)
  , PrimReprSpec -> IntRepr Int16
_prsInt16Repr  :: !(IntRepr Int16)
  , PrimReprSpec -> IntRepr Int32
_prsInt32Repr  :: !(IntRepr Int32)
  , PrimReprSpec -> IntRepr Int64
_prsInt64Repr  :: !(IntRepr Int64)
  , PrimReprSpec -> RealRepr Float
_prsFloatRepr  :: !(RealRepr Float)
  , PrimReprSpec -> RealRepr Double
_prsDoubleRepr :: !(RealRepr Double)
  , PrimReprSpec -> BoolRepr Bool8
_prsBool8Repr  :: !(BoolRepr Bool8)
  , PrimReprSpec -> BoolRepr Bool16
_prsBool16Repr :: !(BoolRepr Bool16)
  , PrimReprSpec -> BoolRepr Bool32
_prsBool32Repr :: !(BoolRepr Bool32)
  , PrimReprSpec -> BoolRepr Bool64
_prsBool64Repr :: !(BoolRepr Bool64)
  }

--------------------------------------------------------------------------------
-- ** Lenses

makeLenses ''PrimReprHandler
makeLenses ''PrimReprSpec

--------------------------------------------------------------------------------
-- * Standard specs

prsPrecise :: PrimReprSpec
prsPrecise :: PrimReprSpec
prsPrecise = PrimReprSpec :: IntRepr Int8
-> IntRepr Int16
-> IntRepr Int32
-> IntRepr Int64
-> RealRepr Float
-> RealRepr Double
-> BoolRepr Bool8
-> BoolRepr Bool16
-> BoolRepr Bool32
-> BoolRepr Bool64
-> PrimReprSpec
PrimReprSpec
  { _prsInt8Repr :: IntRepr Int8
_prsInt8Repr = IntRepr Int8
forall k (a :: k). IntRepr a
MachineInt
  , _prsInt16Repr :: IntRepr Int16
_prsInt16Repr = IntRepr Int16
forall k (a :: k). IntRepr a
MachineInt
  , _prsInt32Repr :: IntRepr Int32
_prsInt32Repr = IntRepr Int32
forall k (a :: k). IntRepr a
MachineInt
  , _prsInt64Repr :: IntRepr Int64
_prsInt64Repr = IntRepr Int64
forall k (a :: k). IntRepr a
MachineInt
  , _prsFloatRepr :: RealRepr Float
_prsFloatRepr = RealRepr Float
forall k (a :: k). RealRepr a
MachineFloat
  , _prsDoubleRepr :: RealRepr Double
_prsDoubleRepr = RealRepr Double
forall k (a :: k). RealRepr a
MachineFloat
  , _prsBool8Repr :: BoolRepr Bool8
_prsBool8Repr = BoolRepr Bool8
forall k (a :: k). BoolRepr a
IntBool
  , _prsBool16Repr :: BoolRepr Bool16
_prsBool16Repr = BoolRepr Bool16
forall k (a :: k). BoolRepr a
IntBool
  , _prsBool32Repr :: BoolRepr Bool32
_prsBool32Repr = BoolRepr Bool32
forall k (a :: k). BoolRepr a
IntBool
  , _prsBool64Repr :: BoolRepr Bool64
_prsBool64Repr = BoolRepr Bool64
forall k (a :: k). BoolRepr a
IntBool
  }

prsIdealized :: PrimReprSpec
prsIdealized :: PrimReprSpec
prsIdealized = PrimReprSpec :: IntRepr Int8
-> IntRepr Int16
-> IntRepr Int32
-> IntRepr Int64
-> RealRepr Float
-> RealRepr Double
-> BoolRepr Bool8
-> BoolRepr Bool16
-> BoolRepr Bool32
-> BoolRepr Bool64
-> PrimReprSpec
PrimReprSpec
  { _prsInt8Repr :: IntRepr Int8
_prsInt8Repr = IntRepr Int8
forall k (a :: k). IntRepr a
ArbitraryInt
  , _prsInt16Repr :: IntRepr Int16
_prsInt16Repr = IntRepr Int16
forall k (a :: k). IntRepr a
ArbitraryInt
  , _prsInt32Repr :: IntRepr Int32
_prsInt32Repr = IntRepr Int32
forall k (a :: k). IntRepr a
ArbitraryInt
  , _prsInt64Repr :: IntRepr Int64
_prsInt64Repr = IntRepr Int64
forall k (a :: k). IntRepr a
ArbitraryInt
  , _prsFloatRepr :: RealRepr Float
_prsFloatRepr = RealRepr Float
forall k (a :: k). RealRepr a
ArbitraryReal
  , _prsDoubleRepr :: RealRepr Double
_prsDoubleRepr = RealRepr Double
forall k (a :: k). RealRepr a
ArbitraryReal
  , _prsBool8Repr :: BoolRepr Bool8
_prsBool8Repr = BoolRepr Bool8
forall k (a :: k). BoolRepr a
BitBool
  , _prsBool16Repr :: BoolRepr Bool16
_prsBool16Repr = BoolRepr Bool16
forall k (a :: k). BoolRepr a
BitBool
  , _prsBool32Repr :: BoolRepr Bool32
_prsBool32Repr = BoolRepr Bool32
forall k (a :: k). BoolRepr a
BitBool
  , _prsBool64Repr :: BoolRepr Bool64
_prsBool64Repr = BoolRepr Bool64
forall k (a :: k). BoolRepr a
BitBool
  }

prsWithArbitraryInts :: Bool -> PrimReprSpec -> PrimReprSpec
prsWithArbitraryInts :: Bool -> PrimReprSpec -> PrimReprSpec
prsWithArbitraryInts Bool
useArbitrary
  | Bool
useArbitrary =
    ASetter PrimReprSpec PrimReprSpec (IntRepr Int8) (IntRepr Int8)
-> IntRepr Int8 -> PrimReprSpec -> PrimReprSpec
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter PrimReprSpec PrimReprSpec (IntRepr Int8) (IntRepr Int8)
Lens' PrimReprSpec (IntRepr Int8)
prsInt8Repr IntRepr Int8
forall k (a :: k). IntRepr a
ArbitraryInt (PrimReprSpec -> PrimReprSpec)
-> (PrimReprSpec -> PrimReprSpec) -> PrimReprSpec -> PrimReprSpec
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ASetter PrimReprSpec PrimReprSpec (IntRepr Int16) (IntRepr Int16)
-> IntRepr Int16 -> PrimReprSpec -> PrimReprSpec
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter PrimReprSpec PrimReprSpec (IntRepr Int16) (IntRepr Int16)
Lens' PrimReprSpec (IntRepr Int16)
prsInt16Repr IntRepr Int16
forall k (a :: k). IntRepr a
ArbitraryInt (PrimReprSpec -> PrimReprSpec)
-> (PrimReprSpec -> PrimReprSpec) -> PrimReprSpec -> PrimReprSpec
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ASetter PrimReprSpec PrimReprSpec (IntRepr Int32) (IntRepr Int32)
-> IntRepr Int32 -> PrimReprSpec -> PrimReprSpec
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter PrimReprSpec PrimReprSpec (IntRepr Int32) (IntRepr Int32)
Lens' PrimReprSpec (IntRepr Int32)
prsInt32Repr IntRepr Int32
forall k (a :: k). IntRepr a
ArbitraryInt (PrimReprSpec -> PrimReprSpec)
-> (PrimReprSpec -> PrimReprSpec) -> PrimReprSpec -> PrimReprSpec
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ASetter PrimReprSpec PrimReprSpec (IntRepr Int64) (IntRepr Int64)
-> IntRepr Int64 -> PrimReprSpec -> PrimReprSpec
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter PrimReprSpec PrimReprSpec (IntRepr Int64) (IntRepr Int64)
Lens' PrimReprSpec (IntRepr Int64)
prsInt64Repr IntRepr Int64
forall k (a :: k). IntRepr a
ArbitraryInt
  | Bool
otherwise =
    ASetter PrimReprSpec PrimReprSpec (IntRepr Int8) (IntRepr Int8)
-> IntRepr Int8 -> PrimReprSpec -> PrimReprSpec
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter PrimReprSpec PrimReprSpec (IntRepr Int8) (IntRepr Int8)
Lens' PrimReprSpec (IntRepr Int8)
prsInt8Repr IntRepr Int8
forall k (a :: k). IntRepr a
MachineInt (PrimReprSpec -> PrimReprSpec)
-> (PrimReprSpec -> PrimReprSpec) -> PrimReprSpec -> PrimReprSpec
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ASetter PrimReprSpec PrimReprSpec (IntRepr Int16) (IntRepr Int16)
-> IntRepr Int16 -> PrimReprSpec -> PrimReprSpec
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter PrimReprSpec PrimReprSpec (IntRepr Int16) (IntRepr Int16)
Lens' PrimReprSpec (IntRepr Int16)
prsInt16Repr IntRepr Int16
forall k (a :: k). IntRepr a
MachineInt (PrimReprSpec -> PrimReprSpec)
-> (PrimReprSpec -> PrimReprSpec) -> PrimReprSpec -> PrimReprSpec
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ASetter PrimReprSpec PrimReprSpec (IntRepr Int32) (IntRepr Int32)
-> IntRepr Int32 -> PrimReprSpec -> PrimReprSpec
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter PrimReprSpec PrimReprSpec (IntRepr Int32) (IntRepr Int32)
Lens' PrimReprSpec (IntRepr Int32)
prsInt32Repr IntRepr Int32
forall k (a :: k). IntRepr a
MachineInt (PrimReprSpec -> PrimReprSpec)
-> (PrimReprSpec -> PrimReprSpec) -> PrimReprSpec -> PrimReprSpec
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ASetter PrimReprSpec PrimReprSpec (IntRepr Int64) (IntRepr Int64)
-> IntRepr Int64 -> PrimReprSpec -> PrimReprSpec
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter PrimReprSpec PrimReprSpec (IntRepr Int64) (IntRepr Int64)
Lens' PrimReprSpec (IntRepr Int64)
prsInt64Repr IntRepr Int64
forall k (a :: k). IntRepr a
MachineInt

prsWithArbitraryReals :: Bool -> PrimReprSpec -> PrimReprSpec
prsWithArbitraryReals :: Bool -> PrimReprSpec -> PrimReprSpec
prsWithArbitraryReals Bool
useArbitrary
  | Bool
useArbitrary =
    ASetter PrimReprSpec PrimReprSpec (RealRepr Float) (RealRepr Float)
-> RealRepr Float -> PrimReprSpec -> PrimReprSpec
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter PrimReprSpec PrimReprSpec (RealRepr Float) (RealRepr Float)
Lens' PrimReprSpec (RealRepr Float)
prsFloatRepr RealRepr Float
forall k (a :: k). RealRepr a
ArbitraryReal (PrimReprSpec -> PrimReprSpec)
-> (PrimReprSpec -> PrimReprSpec) -> PrimReprSpec -> PrimReprSpec
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ASetter
  PrimReprSpec PrimReprSpec (RealRepr Double) (RealRepr Double)
-> RealRepr Double -> PrimReprSpec -> PrimReprSpec
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter
  PrimReprSpec PrimReprSpec (RealRepr Double) (RealRepr Double)
Lens' PrimReprSpec (RealRepr Double)
prsDoubleRepr RealRepr Double
forall k (a :: k). RealRepr a
ArbitraryReal
  | Bool
otherwise =
    ASetter PrimReprSpec PrimReprSpec (RealRepr Float) (RealRepr Float)
-> RealRepr Float -> PrimReprSpec -> PrimReprSpec
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter PrimReprSpec PrimReprSpec (RealRepr Float) (RealRepr Float)
Lens' PrimReprSpec (RealRepr Float)
prsFloatRepr RealRepr Float
forall k (a :: k). RealRepr a
MachineFloat (PrimReprSpec -> PrimReprSpec)
-> (PrimReprSpec -> PrimReprSpec) -> PrimReprSpec -> PrimReprSpec
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ASetter
  PrimReprSpec PrimReprSpec (RealRepr Double) (RealRepr Double)
-> RealRepr Double -> PrimReprSpec -> PrimReprSpec
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter
  PrimReprSpec PrimReprSpec (RealRepr Double) (RealRepr Double)
Lens' PrimReprSpec (RealRepr Double)
prsDoubleRepr RealRepr Double
forall k (a :: k). RealRepr a
MachineFloat

--------------------------------------------------------------------------------
-- * Using specs

makeSymRepr :: PrimReprSpec -> Prim p k a -> PrimReprHandler a
makeSymRepr :: PrimReprSpec -> Prim p k a -> PrimReprHandler a
makeSymRepr PrimReprSpec
spec = \case
  Prim p k a
PInt8   -> Lens' PrimReprSpec (IntRepr a) -> PrimReprHandler a
forall a.
(Integral a, SymVal a) =>
Lens' PrimReprSpec (IntRepr a) -> PrimReprHandler a
intRepr Lens' PrimReprSpec (IntRepr a)
Lens' PrimReprSpec (IntRepr Int8)
prsInt8Repr
  Prim p k a
PInt16  -> Lens' PrimReprSpec (IntRepr a) -> PrimReprHandler a
forall a.
(Integral a, SymVal a) =>
Lens' PrimReprSpec (IntRepr a) -> PrimReprHandler a
intRepr Lens' PrimReprSpec (IntRepr a)
Lens' PrimReprSpec (IntRepr Int16)
prsInt16Repr
  Prim p k a
PInt32  -> Lens' PrimReprSpec (IntRepr a) -> PrimReprHandler a
forall a.
(Integral a, SymVal a) =>
Lens' PrimReprSpec (IntRepr a) -> PrimReprHandler a
intRepr Lens' PrimReprSpec (IntRepr a)
Lens' PrimReprSpec (IntRepr Int32)
prsInt32Repr
  Prim p k a
PInt64  -> Lens' PrimReprSpec (IntRepr a) -> PrimReprHandler a
forall a.
(Integral a, SymVal a) =>
Lens' PrimReprSpec (IntRepr a) -> PrimReprHandler a
intRepr Lens' PrimReprSpec (IntRepr a)
Lens' PrimReprSpec (IntRepr Int64)
prsInt64Repr
  Prim p k a
PFloat  -> Lens' PrimReprSpec (RealRepr a) -> PrimReprHandler a
forall a.
(RealFloat a, SymVal a) =>
Lens' PrimReprSpec (RealRepr a) -> PrimReprHandler a
realRepr Lens' PrimReprSpec (RealRepr a)
Lens' PrimReprSpec (RealRepr Float)
prsFloatRepr
  Prim p k a
PDouble -> Lens' PrimReprSpec (RealRepr a) -> PrimReprHandler a
forall a.
(RealFloat a, SymVal a) =>
Lens' PrimReprSpec (RealRepr a) -> PrimReprHandler a
realRepr Lens' PrimReprSpec (RealRepr a)
Lens' PrimReprSpec (RealRepr Double)
prsDoubleRepr
  Prim p k a
PBool8  -> (Bool8 -> Int8)
-> Lens' PrimReprSpec (BoolRepr Bool8) -> PrimReprHandler Bool8
forall b a.
(Integral b, SymVal b) =>
(a -> b) -> Lens' PrimReprSpec (BoolRepr a) -> PrimReprHandler a
boolRepr Bool8 -> Int8
getBool8 Lens' PrimReprSpec (BoolRepr Bool8)
prsBool8Repr
  Prim p k a
PBool16 -> (Bool16 -> Int16)
-> Lens' PrimReprSpec (BoolRepr Bool16) -> PrimReprHandler Bool16
forall b a.
(Integral b, SymVal b) =>
(a -> b) -> Lens' PrimReprSpec (BoolRepr a) -> PrimReprHandler a
boolRepr Bool16 -> Int16
getBool16 Lens' PrimReprSpec (BoolRepr Bool16)
prsBool16Repr
  Prim p k a
PBool32 -> (Bool32 -> Int32)
-> Lens' PrimReprSpec (BoolRepr Bool32) -> PrimReprHandler Bool32
forall b a.
(Integral b, SymVal b) =>
(a -> b) -> Lens' PrimReprSpec (BoolRepr a) -> PrimReprHandler a
boolRepr Bool32 -> Int32
getBool32 Lens' PrimReprSpec (BoolRepr Bool32)
prsBool32Repr
  Prim p k a
PBool64 -> (Bool64 -> Int64)
-> Lens' PrimReprSpec (BoolRepr Bool64) -> PrimReprHandler Bool64
forall b a.
(Integral b, SymVal b) =>
(a -> b) -> Lens' PrimReprSpec (BoolRepr a) -> PrimReprHandler a
boolRepr Bool64 -> Int64
getBool64 Lens' PrimReprSpec (BoolRepr Bool64)
prsBool64Repr
  Prim p k a
PChar   -> Word8 -> (Char8 -> Word8) -> PrimReprHandler Char8
forall b a. SymVal b => b -> (a -> b) -> PrimReprHandler a
bySymWord (Word8
0 :: Word8) Char8 -> Word8
getChar8
  where
    intRepr
      :: (Integral a, SBV.SymVal a)
      => Lens' PrimReprSpec (IntRepr a) -> PrimReprHandler a
    intRepr :: Lens' PrimReprSpec (IntRepr a) -> PrimReprHandler a
intRepr Lens' PrimReprSpec (IntRepr a)
l = case PrimReprSpec
spec PrimReprSpec
-> Getting (IntRepr a) PrimReprSpec (IntRepr a) -> IntRepr a
forall s a. s -> Getting a s a -> a
^. Getting (IntRepr a) PrimReprSpec (IntRepr a)
Lens' PrimReprSpec (IntRepr a)
l of
      IntRepr a
MachineInt   -> a -> (a -> a) -> PrimReprHandler a
forall b a. SymVal b => b -> (a -> b) -> PrimReprHandler a
bySymWord a
0 a -> a
forall a. a -> a
id
      IntRepr a
ArbitraryInt -> Integer -> (a -> Integer) -> PrimReprHandler a
forall b a. SymVal b => b -> (a -> b) -> PrimReprHandler a
bySymWord (Integer
0 :: Integer) a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral

    realRepr
      :: (RealFloat a, SBV.SymVal a)
      => Lens' PrimReprSpec (RealRepr a) -> PrimReprHandler a
    realRepr :: Lens' PrimReprSpec (RealRepr a) -> PrimReprHandler a
realRepr Lens' PrimReprSpec (RealRepr a)
l = case PrimReprSpec
spec PrimReprSpec
-> Getting (RealRepr a) PrimReprSpec (RealRepr a) -> RealRepr a
forall s a. s -> Getting a s a -> a
^. Getting (RealRepr a) PrimReprSpec (RealRepr a)
Lens' PrimReprSpec (RealRepr a)
l of
      RealRepr a
MachineFloat  -> a -> (a -> a) -> PrimReprHandler a
forall b a. SymVal b => b -> (a -> b) -> PrimReprHandler a
bySymWord a
0 a -> a
forall a. a -> a
id
      RealRepr a
ArbitraryReal -> AlgReal -> (a -> AlgReal) -> PrimReprHandler a
forall b a. SymVal b => b -> (a -> b) -> PrimReprHandler a
bySymWord (AlgReal
0 :: SBV.AlgReal) a -> AlgReal
forall a b. (Real a, Fractional b) => a -> b
realToFrac

    boolRepr
      :: (Integral b, SBV.SymVal b)
      => (a -> b) -> Lens' PrimReprSpec (BoolRepr a) -> PrimReprHandler a
    boolRepr :: (a -> b) -> Lens' PrimReprSpec (BoolRepr a) -> PrimReprHandler a
boolRepr a -> b
unwrap Lens' PrimReprSpec (BoolRepr a)
l = case PrimReprSpec
spec PrimReprSpec
-> Getting (BoolRepr a) PrimReprSpec (BoolRepr a) -> BoolRepr a
forall s a. s -> Getting a s a -> a
^. Getting (BoolRepr a) PrimReprSpec (BoolRepr a)
Lens' PrimReprSpec (BoolRepr a)
l of
      BoolRepr a
IntBool -> b -> (a -> b) -> PrimReprHandler a
forall b a. SymVal b => b -> (a -> b) -> PrimReprHandler a
bySymWord b
0 a -> b
unwrap
      BoolRepr a
BitBool -> Bool -> (a -> Bool) -> PrimReprHandler a
forall b a. SymVal b => b -> (a -> b) -> PrimReprHandler a
bySymWord (Bool
False :: Bool) (b -> Bool
forall a. (Ord a, Num a) => a -> Bool
toBool (b -> Bool) -> (a -> b) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
unwrap)

    bySymWord :: (SBV.SymVal b) => b -> (a -> b) -> PrimReprHandler a
    bySymWord :: b -> (a -> b) -> PrimReprHandler a
bySymWord (b
repValue :: b) a -> b
fromPrim =
      PrimReprHandler :: forall a.
Kind
-> (a -> SVal) -> (String -> Symbolic SVal) -> PrimReprHandler a
PrimReprHandler
      { _prhKind :: Kind
_prhKind = b -> Kind
forall a. HasKind a => a -> Kind
SBV.kindOf b
repValue
      , _prhLiteral :: a -> SVal
_prhLiteral = SBV b -> SVal
forall a. SBV a -> SVal
unSBV (SBV b -> SVal) -> (a -> SBV b) -> a -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> SBV b
forall a. SymVal a => a -> SBV a
SBV.literal (b -> SBV b) -> (a -> b) -> a -> SBV b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
fromPrim
      , _prhSymbolic :: String -> Symbolic SVal
_prhSymbolic = (SBV b -> SVal) -> SymbolicT IO (SBV b) -> Symbolic SVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SBV b -> SVal
forall a. SBV a -> SVal
unSBV :: SBV b -> SVal) (SymbolicT IO (SBV b) -> Symbolic SVal)
-> (String -> SymbolicT IO (SBV b)) -> String -> Symbolic SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> SymbolicT IO (SBV b)
forall a. SymVal a => String -> Symbolic (SBV a)
SBV.symbolic
      }

    toBool :: (Ord a, Num a) => a -> Bool
    toBool :: a -> Bool
toBool a
x = a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0

--------------------------------------------------------------------------------
-- * Monadic Accessors

class HasPrimReprHandlers r where
  primReprHandlers :: r -> PrimReprHandlers
  primReprHandlers r
env = (forall (p :: Precision) (k :: BasicType) a.
 Prim p k a -> PrimReprHandler a)
-> PrimReprHandlers
PrimReprHandlers (r -> Prim p k a -> PrimReprHandler a
forall r (p :: Precision) (k :: BasicType) a.
HasPrimReprHandlers r =>
r -> Prim p k a -> PrimReprHandler a
primReprHandler r
env)

  primReprHandler :: r -> Prim p k a -> PrimReprHandler a
  primReprHandler = PrimReprHandlers -> Prim p k a -> PrimReprHandler a
PrimReprHandlers
-> forall (p :: Precision) (k :: BasicType) a.
   Prim p k a -> PrimReprHandler a
unPrimReprHandlers (PrimReprHandlers -> Prim p k a -> PrimReprHandler a)
-> (r -> PrimReprHandlers) -> r -> Prim p k a -> PrimReprHandler a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. r -> PrimReprHandlers
forall r. HasPrimReprHandlers r => r -> PrimReprHandlers
primReprHandlers

newtype PrimReprHandlers =
  PrimReprHandlers { PrimReprHandlers
-> forall (p :: Precision) (k :: BasicType) a.
   Prim p k a -> PrimReprHandler a
unPrimReprHandlers :: forall p k a. Prim p k a -> PrimReprHandler a }

instance HasPrimReprHandlers PrimReprHandlers where
  primReprHandlers :: PrimReprHandlers -> PrimReprHandlers
primReprHandlers = PrimReprHandlers -> PrimReprHandlers
forall a. a -> a
id

primSBVKind :: (MonadReader r m, HasPrimReprHandlers r) => Prim p k a -> m SBV.Kind
primSBVKind :: Prim p k a -> m Kind
primSBVKind Prim p k a
p = Getting Kind r Kind -> m Kind
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((r -> PrimReprHandler a)
-> Optic' (->) (Const Kind) r (PrimReprHandler a)
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to ((r -> Prim p k a -> PrimReprHandler a)
-> Prim p k a -> r -> PrimReprHandler a
forall a b c. (a -> b -> c) -> b -> a -> c
flip r -> Prim p k a -> PrimReprHandler a
forall r (p :: Precision) (k :: BasicType) a.
HasPrimReprHandlers r =>
r -> Prim p k a -> PrimReprHandler a
primReprHandler Prim p k a
p) Optic' (->) (Const Kind) r (PrimReprHandler a)
-> ((Kind -> Const Kind Kind)
    -> PrimReprHandler a -> Const Kind (PrimReprHandler a))
-> Getting Kind r Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Kind -> Const Kind Kind)
-> PrimReprHandler a -> Const Kind (PrimReprHandler a)
forall a. Lens' (PrimReprHandler a) Kind
prhKind)

primLit :: (MonadReader r m, HasPrimReprHandlers r) => Prim p k a -> a -> m SVal
primLit :: Prim p k a -> a -> m SVal
primLit Prim p k a
p a
a = do
  a -> SVal
lit <- Getting (a -> SVal) r (a -> SVal) -> m (a -> SVal)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((r -> PrimReprHandler a)
-> Optic' (->) (Const (a -> SVal)) r (PrimReprHandler a)
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to ((r -> Prim p k a -> PrimReprHandler a)
-> Prim p k a -> r -> PrimReprHandler a
forall a b c. (a -> b -> c) -> b -> a -> c
flip r -> Prim p k a -> PrimReprHandler a
forall r (p :: Precision) (k :: BasicType) a.
HasPrimReprHandlers r =>
r -> Prim p k a -> PrimReprHandler a
primReprHandler Prim p k a
p) Optic' (->) (Const (a -> SVal)) r (PrimReprHandler a)
-> (((a -> SVal) -> Const (a -> SVal) (a -> SVal))
    -> PrimReprHandler a -> Const (a -> SVal) (PrimReprHandler a))
-> Getting (a -> SVal) r (a -> SVal)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a -> SVal) -> Const (a -> SVal) (a -> SVal))
-> PrimReprHandler a -> Const (a -> SVal) (PrimReprHandler a)
forall a a.
Lens
  (PrimReprHandler a) (PrimReprHandler a) (a -> SVal) (a -> SVal)
prhLiteral)
  SVal -> m SVal
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> SVal
lit a
a)

primSymbolic
  :: (MonadReader r m, HasPrimReprHandlers r)
  => Prim p k a -> String -> m (SBV.Symbolic SVal)
primSymbolic :: Prim p k a -> String -> m (Symbolic SVal)
primSymbolic Prim p k a
p String
nm = do
  String -> Symbolic SVal
symbolic <- Getting (String -> Symbolic SVal) r (String -> Symbolic SVal)
-> m (String -> Symbolic SVal)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((r -> PrimReprHandler a)
-> Optic'
     (->) (Const (String -> Symbolic SVal)) r (PrimReprHandler a)
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to ((r -> Prim p k a -> PrimReprHandler a)
-> Prim p k a -> r -> PrimReprHandler a
forall a b c. (a -> b -> c) -> b -> a -> c
flip r -> Prim p k a -> PrimReprHandler a
forall r (p :: Precision) (k :: BasicType) a.
HasPrimReprHandlers r =>
r -> Prim p k a -> PrimReprHandler a
primReprHandler Prim p k a
p) Optic' (->) (Const (String -> Symbolic SVal)) r (PrimReprHandler a)
-> (((String -> Symbolic SVal)
     -> Const (String -> Symbolic SVal) (String -> Symbolic SVal))
    -> PrimReprHandler a
    -> Const (String -> Symbolic SVal) (PrimReprHandler a))
-> Getting (String -> Symbolic SVal) r (String -> Symbolic SVal)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String -> Symbolic SVal)
 -> Const (String -> Symbolic SVal) (String -> Symbolic SVal))
-> PrimReprHandler a
-> Const (String -> Symbolic SVal) (PrimReprHandler a)
forall a. Lens' (PrimReprHandler a) (String -> Symbolic SVal)
prhSymbolic)
  Symbolic SVal -> m (Symbolic SVal)
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Symbolic SVal
symbolic String
nm)