{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE DataKinds #-}

-- | Internal representation of Feldspar programs

module Feldspar.Representation where



import Control.Monad.Reader
import Data.Complex
import Data.Hash (hashInt)
import Data.Int
import Data.List (genericTake)
import Data.Proxy
import Data.Typeable (Typeable)
import Data.Word

import Data.Constraint (Dict (..))

import Language.Syntactic
import Language.Syntactic.Functional
import Language.Syntactic.Functional.Tuple
import Language.Syntactic.TH

import qualified Control.Monad.Operational.Higher as Operational

import qualified Language.Embedded.Expression as Imp
import qualified Language.Embedded.Imperative.CMD as Imp
import qualified Language.Embedded.Backend.C.Expression as Imp

import Data.Inhabited
import Data.Selection
import Data.TypedStruct
import Feldspar.Primitive.Representation
import Feldspar.Primitive.Backend.C ()



--------------------------------------------------------------------------------
-- * Object-language types
--------------------------------------------------------------------------------

-- | Representation of all supported types
type TypeRep = Struct PrimType' PrimTypeRep

-- | Supported types
class (Eq a, Show a, Typeable a, Inhabited a) => Type a
  where
    -- | Reify a type
    typeRep :: TypeRep a

instance Type Bool             where typeRep :: TypeRep Bool
typeRep = PrimTypeRep Bool -> TypeRep Bool
forall (pred :: * -> Constraint) a (con :: * -> *).
pred a =>
con a -> Struct pred con a
Single PrimTypeRep Bool
BoolT
instance Type Int8             where typeRep :: TypeRep Int8
typeRep = PrimTypeRep Int8 -> TypeRep Int8
forall (pred :: * -> Constraint) a (con :: * -> *).
pred a =>
con a -> Struct pred con a
Single PrimTypeRep Int8
Int8T
instance Type Int16            where typeRep :: TypeRep Int16
typeRep = PrimTypeRep Int16 -> TypeRep Int16
forall (pred :: * -> Constraint) a (con :: * -> *).
pred a =>
con a -> Struct pred con a
Single PrimTypeRep Int16
Int16T
instance Type Int32            where typeRep :: TypeRep Int32
typeRep = PrimTypeRep Int32 -> TypeRep Int32
forall (pred :: * -> Constraint) a (con :: * -> *).
pred a =>
con a -> Struct pred con a
Single PrimTypeRep Int32
Int32T
instance Type Int64            where typeRep :: TypeRep Int64
typeRep = PrimTypeRep Int64 -> TypeRep Int64
forall (pred :: * -> Constraint) a (con :: * -> *).
pred a =>
con a -> Struct pred con a
Single PrimTypeRep Int64
Int64T
instance Type Word8            where typeRep :: TypeRep Word8
typeRep = PrimTypeRep Word8 -> TypeRep Word8
forall (pred :: * -> Constraint) a (con :: * -> *).
pred a =>
con a -> Struct pred con a
Single PrimTypeRep Word8
Word8T
instance Type Word16           where typeRep :: TypeRep Word16
typeRep = PrimTypeRep Word16 -> TypeRep Word16
forall (pred :: * -> Constraint) a (con :: * -> *).
pred a =>
con a -> Struct pred con a
Single PrimTypeRep Word16
Word16T
instance Type Word32           where typeRep :: TypeRep Word32
typeRep = PrimTypeRep Word32 -> TypeRep Word32
forall (pred :: * -> Constraint) a (con :: * -> *).
pred a =>
con a -> Struct pred con a
Single PrimTypeRep Word32
Word32T
instance Type Word64           where typeRep :: TypeRep Word64
typeRep = PrimTypeRep Word64 -> TypeRep Word64
forall (pred :: * -> Constraint) a (con :: * -> *).
pred a =>
con a -> Struct pred con a
Single PrimTypeRep Word64
Word64T
instance Type Float            where typeRep :: TypeRep Float
typeRep = PrimTypeRep Float -> TypeRep Float
forall (pred :: * -> Constraint) a (con :: * -> *).
pred a =>
con a -> Struct pred con a
Single PrimTypeRep Float
FloatT
instance Type Double           where typeRep :: TypeRep Double
typeRep = PrimTypeRep Double -> TypeRep Double
forall (pred :: * -> Constraint) a (con :: * -> *).
pred a =>
con a -> Struct pred con a
Single PrimTypeRep Double
DoubleT
instance Type (Complex Float)  where typeRep :: TypeRep (Complex Float)
typeRep = PrimTypeRep (Complex Float) -> TypeRep (Complex Float)
forall (pred :: * -> Constraint) a (con :: * -> *).
pred a =>
con a -> Struct pred con a
Single PrimTypeRep (Complex Float)
ComplexFloatT
instance Type (Complex Double) where typeRep :: TypeRep (Complex Double)
typeRep = PrimTypeRep (Complex Double) -> TypeRep (Complex Double)
forall (pred :: * -> Constraint) a (con :: * -> *).
pred a =>
con a -> Struct pred con a
Single PrimTypeRep (Complex Double)
ComplexDoubleT
instance (Type a, Type b) => Type (a,b) where typeRep :: TypeRep (a, b)
typeRep = Struct PrimType' PrimTypeRep a
-> Struct PrimType' PrimTypeRep b -> TypeRep (a, b)
forall (pred :: * -> Constraint) (con :: * -> *) a b.
Struct pred con a -> Struct pred con b -> Struct pred con (a, b)
Two Struct PrimType' PrimTypeRep a
forall a. Type a => TypeRep a
typeRep Struct PrimType' PrimTypeRep b
forall a. Type a => TypeRep a
typeRep

-- | Alias for the conjunction of 'PrimType'' and 'Type'
class    (PrimType' a, Type a) => PrimType a
instance (PrimType' a, Type a) => PrimType a

instance Imp.CompTypeClass PrimType
  where
    compType :: proxy1 PrimType -> proxy2 a -> m Type
compType proxy1 PrimType
_ = Proxy PrimType' -> proxy2 a -> m Type
forall (ct :: * -> Constraint) a (m :: * -> *)
       (proxy1 :: (* -> Constraint) -> *) (proxy2 :: * -> *).
(CompTypeClass ct, ct a, MonadC m) =>
proxy1 ct -> proxy2 a -> m Type
Imp.compType (Proxy PrimType'
forall k (t :: k). Proxy t
Proxy :: Proxy PrimType')
    compLit :: proxy PrimType -> a -> m Exp
compLit proxy PrimType
_  = Proxy PrimType' -> a -> m Exp
forall (ct :: * -> Constraint) a (m :: * -> *)
       (proxy :: (* -> Constraint) -> *).
(CompTypeClass ct, ct a, MonadC m) =>
proxy ct -> a -> m Exp
Imp.compLit (Proxy PrimType'
forall k (t :: k). Proxy t
Proxy :: Proxy PrimType')
  -- This instance is used by <https://github.com/kmate/raw-feldspar-mcs>

-- | Convert any 'Struct' with a 'PrimType' constraint to a 'TypeRep'
toTypeRep :: Struct PrimType' c a -> TypeRep a
toTypeRep :: Struct PrimType' c a -> TypeRep a
toTypeRep = (forall a. PrimType' a => c a -> PrimTypeRep a)
-> Struct PrimType' c a -> TypeRep a
forall (pred :: * -> Constraint) (c1 :: * -> *) (c2 :: * -> *) b.
(forall a. pred a => c1 a -> c2 a)
-> Struct pred c1 b -> Struct pred c2 b
mapStruct (PrimTypeRep a -> c a -> PrimTypeRep a
forall a b. a -> b -> a
const PrimTypeRep a
forall a. PrimType' a => PrimTypeRep a
primTypeRep)

-- | Check whether two type representations are equal
typeEq :: TypeRep a -> TypeRep b -> Maybe (Dict (a ~ b))
typeEq :: TypeRep a -> TypeRep b -> Maybe (Dict (a ~ b))
typeEq (Single PrimTypeRep a
t) (Single PrimTypeRep b
u) = PrimTypeRep a -> PrimTypeRep b -> Maybe (Dict (a ~ b))
forall a b. PrimTypeRep a -> PrimTypeRep b -> Maybe (Dict (a ~ b))
primTypeEq PrimTypeRep a
t PrimTypeRep b
u
typeEq (Two Struct PrimType' PrimTypeRep a
t1 Struct PrimType' PrimTypeRep b
t2) (Two Struct PrimType' PrimTypeRep a
u1 Struct PrimType' PrimTypeRep b
u2) = do
    Dict (a ~ a)
Dict <- Struct PrimType' PrimTypeRep a
-> Struct PrimType' PrimTypeRep a -> Maybe (Dict (a ~ a))
forall a b. TypeRep a -> TypeRep b -> Maybe (Dict (a ~ b))
typeEq Struct PrimType' PrimTypeRep a
t1 Struct PrimType' PrimTypeRep a
u1
    Dict (b ~ b)
Dict <- Struct PrimType' PrimTypeRep b
-> Struct PrimType' PrimTypeRep b -> Maybe (Dict (b ~ b))
forall a b. TypeRep a -> TypeRep b -> Maybe (Dict (a ~ b))
typeEq Struct PrimType' PrimTypeRep b
t2 Struct PrimType' PrimTypeRep b
u2
    Dict (a ~ b) -> Maybe (Dict (a ~ b))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (a ~ b)
forall (a :: Constraint). a => Dict a
Dict
typeEq TypeRep a
_ TypeRep b
_ = Maybe (Dict (a ~ b))
forall a. Maybe a
Nothing

-- | Reflect a 'TypeRep' to a 'Typeable' constraint
witTypeable :: TypeRep a -> Dict (Typeable a)
witTypeable :: TypeRep a -> Dict (Typeable a)
witTypeable (Single PrimTypeRep a
t)
    | Dict (PrimType' a)
Dict <- PrimTypeRep a -> Dict (PrimType' a)
forall a. PrimTypeRep a -> Dict (PrimType' a)
witPrimType PrimTypeRep a
t
    = Dict (Typeable a)
forall (a :: Constraint). a => Dict a
Dict
witTypeable (Two Struct PrimType' PrimTypeRep a
ta Struct PrimType' PrimTypeRep b
tb)
    | Dict (Typeable a)
Dict <- Struct PrimType' PrimTypeRep a -> Dict (Typeable a)
forall a. TypeRep a -> Dict (Typeable a)
witTypeable Struct PrimType' PrimTypeRep a
ta
    , Dict (Typeable b)
Dict <- Struct PrimType' PrimTypeRep b -> Dict (Typeable b)
forall a. TypeRep a -> Dict (Typeable a)
witTypeable Struct PrimType' PrimTypeRep b
tb
    = Dict (Typeable a)
forall (a :: Constraint). a => Dict a
Dict

-- | Representation of supported value types + N-ary functions over such types
data TypeRepFun a
  where
    ValT :: TypeRep a -> TypeRepFun a
    FunT :: TypeRep a -> TypeRepFun b -> TypeRepFun (a -> b)
  -- Another option would have been to make `FunT` a constructor in `TypeRep`.
  -- That would have got rid of the extra layer at the expense of less accurate
  -- types (functions would be allowed in pairs, etc.). The current design was
  -- chosen in order to be able to reuse `Struct` instead of making `TypeRep` a
  -- new data type.

-- | Check whether two type representations are equal
typeEqFun :: TypeRepFun a -> TypeRepFun b -> Maybe (Dict (a ~ b))
typeEqFun :: TypeRepFun a -> TypeRepFun b -> Maybe (Dict (a ~ b))
typeEqFun (ValT TypeRep a
t)     (ValT TypeRep b
u)     = TypeRep a -> TypeRep b -> Maybe (Dict (a ~ b))
forall a b. TypeRep a -> TypeRep b -> Maybe (Dict (a ~ b))
typeEq TypeRep a
t TypeRep b
u
typeEqFun (FunT TypeRep a
ta TypeRepFun b
tb) (FunT TypeRep a
ua TypeRepFun b
ub) = do
    Dict (a ~ a)
Dict <- TypeRep a -> TypeRep a -> Maybe (Dict (a ~ a))
forall a b. TypeRep a -> TypeRep b -> Maybe (Dict (a ~ b))
typeEq TypeRep a
ta TypeRep a
ua
    Dict (b ~ b)
Dict <- TypeRepFun b -> TypeRepFun b -> Maybe (Dict (b ~ b))
forall a b. TypeRepFun a -> TypeRepFun b -> Maybe (Dict (a ~ b))
typeEqFun TypeRepFun b
tb TypeRepFun b
ub
    Dict (a ~ b) -> Maybe (Dict (a ~ b))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (a ~ b)
forall (a :: Constraint). a => Dict a
Dict
typeEqFun TypeRepFun a
_ TypeRepFun b
_ = Maybe (Dict (a ~ b))
forall a. Maybe a
Nothing

-- | Mutable variable
newtype Ref a = Ref { Ref a -> Struct PrimType' Ref (Internal a)
unRef :: Struct PrimType' Imp.Ref (Internal a) }
  -- A reference to a tuple is a struct of smaller references. This means that
  -- creating a reference to a tuple will generate several calls to generate new
  -- references. This must be done already in the front end, which means that
  -- the work in the back end becomes simpler.
  --
  -- Another option would be to allow a single reference to refer to a tuple,
  -- and then turn that into smaller references in the back end. However, this
  -- would complicate the back end for no obvious reason. (One way to do it
  -- would be to run the back end in a store that maps each front end reference
  -- to a struct of small references. Among other things, that would require
  -- dynamic typing.)

-- | Reference specialized to 'Data' elements
type DRef a = Ref (Data a)

instance Eq (Ref a)
  where
    Ref Struct PrimType' Ref (Internal a)
a == :: Ref a -> Ref a -> Bool
== Ref Struct PrimType' Ref (Internal a)
b = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (forall a. PrimType' a => Ref a -> Ref a -> Bool)
-> Struct PrimType' Ref (Internal a)
-> Struct PrimType' Ref (Internal a)
-> [Bool]
forall (pred :: * -> Constraint) (c1 :: * -> *) (c2 :: * -> *) b r.
(forall a. pred a => c1 a -> c2 a -> r)
-> Struct pred c1 b -> Struct pred c2 b -> [r]
zipListStruct forall a. Eq a => a -> a -> Bool
forall a. PrimType' a => Ref a -> Ref a -> Bool
(==) Struct PrimType' Ref (Internal a)
a Struct PrimType' Ref (Internal a)
b

-- | Mutable array
data Arr a = Arr
    { Arr a -> Data Word32
arrOffset :: Data Index
    , Arr a -> Data Word32
arrLength :: Data Length
    , Arr a -> Struct PrimType' (Arr Word32) (Internal a)
unArr     :: Struct PrimType' (Imp.Arr Index) (Internal a)
    }
  -- `arrOffset` gives the offset into the internal arrays. The user should not
  -- be able to access the offset or the internal arrays.
  --
  -- `arrLength` gives the maximum index+1 according to the view provided by
  -- `arrIx`. Thus, the maximum index in the internal arrays is
  -- `arrLength + arrOffset - 1`.
  -- `arrLength` should not be exported directly to prevent the user from using
  -- record syntax to change the length of an array. But an equivalent function
  -- can be exported.

  -- An array of tuples is represented as a struct of smaller arrays. See
  -- comment to `Ref`.

-- | Array specialized to 'Data' elements
type DArr a = Arr (Data a)

-- | '==' checks if two 'Arr' use the same physical array. The length and offset
-- are ignored.
instance Eq (Arr a)
  where
    Arr Data Word32
_ Data Word32
_ Struct PrimType' (Arr Word32) (Internal a)
arr1 == :: Arr a -> Arr a -> Bool
== Arr Data Word32
_ Data Word32
_ Struct PrimType' (Arr Word32) (Internal a)
arr2 = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((forall a. PrimType' a => Arr Word32 a -> Arr Word32 a -> Bool)
-> Struct PrimType' (Arr Word32) (Internal a)
-> Struct PrimType' (Arr Word32) (Internal a)
-> [Bool]
forall (pred :: * -> Constraint) (c1 :: * -> *) (c2 :: * -> *) b r.
(forall a. pred a => c1 a -> c2 a -> r)
-> Struct pred c1 b -> Struct pred c2 b -> [r]
zipListStruct forall a. Eq a => a -> a -> Bool
forall a. PrimType' a => Arr Word32 a -> Arr Word32 a -> Bool
(==) Struct PrimType' (Arr Word32) (Internal a)
arr1 Struct PrimType' (Arr Word32) (Internal a)
arr2)

-- | Immutable array
data IArr a = IArr
    { IArr a -> Data Word32
iarrOffset :: Data Index
    , IArr a -> Data Word32
iarrLength :: Data Length
    , IArr a -> Struct PrimType' (IArr Word32) (Internal a)
unIArr     :: Struct PrimType' (Imp.IArr Index) (Internal a)
    }

-- | Immutable array specialized to 'Data' elements
type DIArr a = IArr (Data a)

-- | Check if an 'Arr' and and 'IArr' use the same physical array. The length
-- and offset are ignored. This operation may give false negatives, but never
-- false positives. Whether or not false negatives occur may also depend on the
-- interpretation of the program.
--
-- Due to this unreliability, the function should only be used to affect the
-- non-functional properties of a program (e.g. to avoid unnecessary array
-- copying).
unsafeEqArrIArr :: Arr a -> IArr a -> Bool
unsafeEqArrIArr :: Arr a -> IArr a -> Bool
unsafeEqArrIArr (Arr Data Word32
_ Data Word32
_ Struct PrimType' (Arr Word32) (Internal a)
arr1) (IArr Data Word32
_ Data Word32
_ Struct PrimType' (IArr Word32) (Internal a)
arr2) =
    [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((forall a. PrimType' a => Arr Word32 a -> IArr Word32 a -> Bool)
-> Struct PrimType' (Arr Word32) (Internal a)
-> Struct PrimType' (IArr Word32) (Internal a)
-> [Bool]
forall (pred :: * -> Constraint) (c1 :: * -> *) (c2 :: * -> *) b r.
(forall a. pred a => c1 a -> c2 a -> r)
-> Struct pred c1 b -> Struct pred c2 b -> [r]
zipListStruct forall a. Arr Word32 a -> IArr Word32 a -> Bool
forall a. PrimType' a => Arr Word32 a -> IArr Word32 a -> Bool
sameId Struct PrimType' (Arr Word32) (Internal a)
arr1 Struct PrimType' (IArr Word32) (Internal a)
arr2)
  where
    sameId :: Imp.Arr Index a -> Imp.IArr Index a -> Bool
    sameId :: Arr Word32 a -> IArr Word32 a -> Bool
sameId (Imp.ArrComp VarId
a) (Imp.IArrComp VarId
i) = VarId
aVarId -> VarId -> Bool
forall a. Eq a => a -> a -> Bool
==VarId
i
    sameId Arr Word32 a
_ IArr Word32 a
_ = Bool
False



--------------------------------------------------------------------------------
-- * Pure expressions
--------------------------------------------------------------------------------

-- | Assertion labels
data AssertionLabel
    = InternalAssertion
        -- ^ Internal assertion to guarantee meaningful results
    | LibraryAssertion String
        -- ^ Assertion related to a specific library
    | UserAssertion String
        -- ^ Assertion in user code. The default label for user assertions is
        --   @`UserAssertion` ""@
  deriving (AssertionLabel -> AssertionLabel -> Bool
(AssertionLabel -> AssertionLabel -> Bool)
-> (AssertionLabel -> AssertionLabel -> Bool) -> Eq AssertionLabel
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AssertionLabel -> AssertionLabel -> Bool
$c/= :: AssertionLabel -> AssertionLabel -> Bool
== :: AssertionLabel -> AssertionLabel -> Bool
$c== :: AssertionLabel -> AssertionLabel -> Bool
Eq, Int -> AssertionLabel -> ShowS
[AssertionLabel] -> ShowS
AssertionLabel -> VarId
(Int -> AssertionLabel -> ShowS)
-> (AssertionLabel -> VarId)
-> ([AssertionLabel] -> ShowS)
-> Show AssertionLabel
forall a.
(Int -> a -> ShowS) -> (a -> VarId) -> ([a] -> ShowS) -> Show a
showList :: [AssertionLabel] -> ShowS
$cshowList :: [AssertionLabel] -> ShowS
show :: AssertionLabel -> VarId
$cshow :: AssertionLabel -> VarId
showsPrec :: Int -> AssertionLabel -> ShowS
$cshowsPrec :: Int -> AssertionLabel -> ShowS
Show)

-- | A selection that includes all labels defined as 'UserAssertion'
onlyUserAssertions :: Selection AssertionLabel
onlyUserAssertions :: Selection AssertionLabel
onlyUserAssertions = (AssertionLabel -> Bool) -> Selection AssertionLabel
forall a. (a -> Bool) -> Selection a
selectBy ((AssertionLabel -> Bool) -> Selection AssertionLabel)
-> (AssertionLabel -> Bool) -> Selection AssertionLabel
forall a b. (a -> b) -> a -> b
$ \AssertionLabel
l -> case AssertionLabel
l of
    UserAssertion VarId
_ -> Bool
True
    AssertionLabel
_ -> Bool
False

data ExtraPrimitive sig
  where
    -- Integer division assuming `divBalanced x y * y == x` (i.e. no remainder).
    -- The purpose of the assumption is to use it in simplifications.
    DivBalanced :: (Integral a, PrimType' a) =>
        ExtraPrimitive (a :-> a :-> Full a)

    -- Guard a value by an assertion
    GuardVal ::
        AssertionLabel -> String -> ExtraPrimitive (Bool :-> a :-> Full a)

instance Eval ExtraPrimitive
  where
    evalSym :: ExtraPrimitive sig -> Denotation sig
evalSym ExtraPrimitive sig
DivBalanced = \a
a a
b -> if a
a a -> a -> a
forall a. Integral a => a -> a -> a
`mod` a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
0
      then VarId -> a
forall a. HasCallStack => VarId -> a
error (VarId -> a) -> VarId -> a
forall a b. (a -> b) -> a -> b
$ [VarId] -> VarId
unwords [VarId
"divBalanced", a -> VarId
forall a. Show a => a -> VarId
show a
a, a -> VarId
forall a. Show a => a -> VarId
show a
b, VarId
"is not balanced"]
      else a -> a -> a
forall a. Integral a => a -> a -> a
div a
a a
b
    evalSym (GuardVal AssertionLabel
_ VarId
msg) = \Bool
cond a
a ->
        if Bool
cond then a
a else VarId -> a
forall a. HasCallStack => VarId -> a
error (VarId -> a) -> VarId -> a
forall a b. (a -> b) -> a -> b
$ VarId
"Feldspar assertion failure: " VarId -> ShowS
forall a. [a] -> [a] -> [a]
++ VarId
msg

instance Equality ExtraPrimitive
  where
    equal :: ExtraPrimitive a -> ExtraPrimitive b -> Bool
equal ExtraPrimitive a
DivBalanced    ExtraPrimitive b
DivBalanced    = Bool
True
    equal (GuardVal AssertionLabel
_ VarId
_) (GuardVal AssertionLabel
_ VarId
_) = Bool
True
    equal ExtraPrimitive a
_ ExtraPrimitive b
_ = Bool
False

    hash :: ExtraPrimitive a -> Hash
hash ExtraPrimitive a
DivBalanced    = Int -> Hash
hashInt Int
1
    hash (GuardVal AssertionLabel
_ VarId
_) = Int -> Hash
hashInt Int
2

-- | For loop
data ForLoop sig
  where
    ForLoop :: Type st =>
        ForLoop (Length :-> st :-> (Index -> st -> st) :-> Full st)

instance Eval ForLoop
  where
    evalSym :: ForLoop sig -> Denotation sig
evalSym ForLoop sig
ForLoop = \Word32
len st
init Word32 -> st -> st
body ->
        (st -> Word32 -> st) -> st -> [Word32] -> st
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Word32 -> st -> st) -> st -> Word32 -> st
forall a b c. (a -> b -> c) -> b -> a -> c
flip Word32 -> st -> st
body) st
init ([Word32] -> st) -> [Word32] -> st
forall a b. (a -> b) -> a -> b
$ Word32 -> [Word32] -> [Word32]
forall i a. Integral i => i -> [a] -> [a]
genericTake Word32
len [Word32
0..]

-- | Interaction with the IO layer
data Unsafe sig
  where
    -- Turn a program into a pure value
    UnsafePerform :: Comp (Data a) -> Unsafe (Full a)

instance Render Unsafe
  where
    renderSym :: Unsafe sig -> VarId
renderSym (UnsafePerform Comp (Data a)
_) = VarId
"UnsafePerform ..."

instance Eval Unsafe
  where
    evalSym :: Unsafe sig -> Denotation sig
evalSym Unsafe sig
s = VarId -> Denotation sig
forall a. HasCallStack => VarId -> a
error (VarId -> Denotation sig) -> VarId -> Denotation sig
forall a b. (a -> b) -> a -> b
$ VarId
"eval: cannot evaluate unsafe operation " VarId -> ShowS
forall a. [a] -> [a] -> [a]
++ Unsafe sig -> VarId
forall (sym :: * -> *) sig. Render sym => sym sig -> VarId
renderSym Unsafe sig
s

-- | 'equal' always returns 'False'
instance Equality Unsafe
  where
    equal :: Unsafe a -> Unsafe b -> Bool
equal Unsafe a
_ Unsafe b
_ = Bool
False

type FeldConstructs
    =   BindingT
    :+: Let
    :+: Tuple
    :+: Primitive
    :+: ExtraPrimitive
    :+: ForLoop
    :+: Unsafe

type FeldDomain = FeldConstructs :&: TypeRepFun

newtype Data a = Data { Data a -> ASTF FeldDomain a
unData :: ASTF FeldDomain a }

-- | Declaring 'Data' as syntactic sugar
instance Syntactic (Data a)
  where
    type Domain (Data a)   = FeldDomain
    type Internal (Data a) = a
    desugar :: Data a -> ASTF (Domain (Data a)) (Internal (Data a))
desugar = Data a -> ASTF (Domain (Data a)) (Internal (Data a))
forall a. Data a -> ASTF FeldDomain a
unData
    sugar :: ASTF (Domain (Data a)) (Internal (Data a)) -> Data a
sugar   = ASTF (Domain (Data a)) (Internal (Data a)) -> Data a
forall a. ASTF FeldDomain a -> Data a
Data

instance Syntactic (Struct PrimType' Data a)
    -- Note that this instance places no constraints on `a`. This is crucial in
    -- the way it is used in the rest of the code. It would be possible to
    -- define `desugar` and `sugar` in terms of the instance for pairs; however,
    -- that would require constraining `a`.
  where
    type Domain   (Struct PrimType' Data a) = FeldDomain
    type Internal (Struct PrimType' Data a) = a

    desugar :: Struct PrimType' Data a
-> ASTF
     (Domain (Struct PrimType' Data a))
     (Internal (Struct PrimType' Data a))
desugar (Single Data a
a) = Data a -> ASTF FeldDomain a
forall a. Data a -> ASTF FeldDomain a
unData Data a
a
    desugar (Two Struct PrimType' Data a
a Struct PrimType' Data b
b)  = TypeRepFun (DenResult (a :-> (b :-> Full (a, b))))
-> Tuple (a :-> (b :-> Full (a, b)))
-> AST FeldDomain (Full a)
-> AST FeldDomain (Full b)
-> AST FeldDomain (Full (a, b))
forall sig fi (sup :: * -> *) (info :: * -> *) f (sub :: * -> *).
(Signature sig, fi ~ SmartFun (sup :&: info) sig,
 sig ~ SmartSig fi, (sup :&: info) ~ SmartSym fi, SyntacticN f fi,
 sub :<: sup) =>
info (DenResult sig) -> sub sig -> f
sugarSymDecor (TypeRep (a, b) -> TypeRepFun (a, b)
forall a. TypeRep a -> TypeRepFun a
ValT (TypeRep (a, b) -> TypeRepFun (a, b))
-> TypeRep (a, b) -> TypeRepFun (a, b)
forall a b. (a -> b) -> a -> b
$ Struct PrimType' PrimTypeRep a
-> Struct PrimType' PrimTypeRep b -> TypeRep (a, b)
forall (pred :: * -> Constraint) (con :: * -> *) a b.
Struct pred con a -> Struct pred con b -> Struct pred con (a, b)
Two Struct PrimType' PrimTypeRep a
ta Struct PrimType' PrimTypeRep b
tb) Tuple (a :-> (b :-> Full (a, b)))
forall a1 b. Tuple (a1 :-> (b :-> Full (a1, b)))
Pair AST FeldDomain (Full a)
ASTF
  (Domain (Struct PrimType' Data a))
  (Internal (Struct PrimType' Data a))
a' AST FeldDomain (Full b)
ASTF
  (Domain (Struct PrimType' Data b))
  (Internal (Struct PrimType' Data b))
b'
      where
        a' :: ASTF
  (Domain (Struct PrimType' Data a))
  (Internal (Struct PrimType' Data a))
a' = Struct PrimType' Data a
-> ASTF
     (Domain (Struct PrimType' Data a))
     (Internal (Struct PrimType' Data a))
forall a. Syntactic a => a -> ASTF (Domain a) (Internal a)
desugar Struct PrimType' Data a
a
        b' :: ASTF
  (Domain (Struct PrimType' Data b))
  (Internal (Struct PrimType' Data b))
b' = Struct PrimType' Data b
-> ASTF
     (Domain (Struct PrimType' Data b))
     (Internal (Struct PrimType' Data b))
forall a. Syntactic a => a -> ASTF (Domain a) (Internal a)
desugar Struct PrimType' Data b
b
        ValT Struct PrimType' PrimTypeRep a
ta = AST FeldDomain (Full a) -> TypeRepFun (DenResult (Full a))
forall (sym :: * -> *) (info :: * -> *) sig.
AST (sym :&: info) sig -> info (DenResult sig)
getDecor AST FeldDomain (Full a)
ASTF
  (Domain (Struct PrimType' Data a))
  (Internal (Struct PrimType' Data a))
a'
        ValT Struct PrimType' PrimTypeRep b
tb = AST FeldDomain (Full b) -> TypeRepFun (DenResult (Full b))
forall (sym :: * -> *) (info :: * -> *) sig.
AST (sym :&: info) sig -> info (DenResult sig)
getDecor AST FeldDomain (Full b)
ASTF
  (Domain (Struct PrimType' Data b))
  (Internal (Struct PrimType' Data b))
b'

    sugar :: ASTF
  (Domain (Struct PrimType' Data a))
  (Internal (Struct PrimType' Data a))
-> Struct PrimType' Data a
sugar ASTF
  (Domain (Struct PrimType' Data a))
  (Internal (Struct PrimType' Data a))
a = case ASTF FeldDomain a -> TypeRepFun (DenResult (Full a))
forall (sym :: * -> *) (info :: * -> *) sig.
AST (sym :&: info) sig -> info (DenResult sig)
getDecor ASTF FeldDomain a
ASTF
  (Domain (Struct PrimType' Data a))
  (Internal (Struct PrimType' Data a))
a of
        ValT (Single _)  -> Data a -> Struct PrimType' Data a
forall (pred :: * -> Constraint) a (con :: * -> *).
pred a =>
con a -> Struct pred con a
Single (Data a -> Struct PrimType' Data a)
-> Data a -> Struct PrimType' Data a
forall a b. (a -> b) -> a -> b
$ ASTF FeldDomain a -> Data a
forall a. ASTF FeldDomain a -> Data a
Data ASTF FeldDomain a
ASTF
  (Domain (Struct PrimType' Data a))
  (Internal (Struct PrimType' Data a))
a
        ValT (Two ta tb) ->
            Struct PrimType' Data a
-> Struct PrimType' Data b -> Struct PrimType' Data (a, b)
forall (pred :: * -> Constraint) (con :: * -> *) a b.
Struct pred con a -> Struct pred con b -> Struct pred con (a, b)
Two (TypeRepFun (DenResult ((a, b) :-> Full a))
-> Tuple ((a, b) :-> Full a)
-> AST FeldDomain (Full (a, b))
-> Struct PrimType' Data a
forall sig fi (sup :: * -> *) (info :: * -> *) f (sub :: * -> *).
(Signature sig, fi ~ SmartFun (sup :&: info) sig,
 sig ~ SmartSig fi, (sup :&: info) ~ SmartSym fi, SyntacticN f fi,
 sub :<: sup) =>
info (DenResult sig) -> sub sig -> f
sugarSymDecor (TypeRep a -> TypeRepFun a
forall a. TypeRep a -> TypeRepFun a
ValT TypeRep a
ta) Tuple ((a, b) :-> Full a)
forall a1 b. Tuple ((a1, b) :-> Full a1)
Fst AST FeldDomain (Full (a, b))
ASTF
  (Domain (Struct PrimType' Data a))
  (Internal (Struct PrimType' Data a))
a) (TypeRepFun (DenResult ((a, b) :-> Full b))
-> Tuple ((a, b) :-> Full b)
-> AST FeldDomain (Full (a, b))
-> Struct PrimType' Data b
forall sig fi (sup :: * -> *) (info :: * -> *) f (sub :: * -> *).
(Signature sig, fi ~ SmartFun (sup :&: info) sig,
 sig ~ SmartSig fi, (sup :&: info) ~ SmartSym fi, SyntacticN f fi,
 sub :<: sup) =>
info (DenResult sig) -> sub sig -> f
sugarSymDecor (TypeRep b -> TypeRepFun b
forall a. TypeRep a -> TypeRepFun a
ValT TypeRep b
tb) Tuple ((a, b) :-> Full b)
forall a1 b. Tuple ((a1, b) :-> Full b)
Snd AST FeldDomain (Full (a, b))
ASTF
  (Domain (Struct PrimType' Data a))
  (Internal (Struct PrimType' Data a))
a)

-- | Specialization of the 'Syntactic' class for the Feldspar domain
class    (Syntactic a, Domain a ~ FeldDomain, Type (Internal a)) => Syntax a
instance (Syntactic a, Domain a ~ FeldDomain, Type (Internal a)) => Syntax a

-- | Make a smart constructor for a symbol
sugarSymFeld
    :: ( Signature sig
       , fi         ~ SmartFun FeldDomain sig
       , sig        ~ SmartSig fi
       , FeldDomain ~ SmartSym fi
       , SyntacticN f fi
       , sub :<: FeldConstructs
       , Type (DenResult sig)
       )
    => sub sig -> f
sugarSymFeld :: sub sig -> f
sugarSymFeld = TypeRepFun (DenResult sig) -> sub sig -> f
forall sig fi (sup :: * -> *) (info :: * -> *) f (sub :: * -> *).
(Signature sig, fi ~ SmartFun (sup :&: info) sig,
 sig ~ SmartSig fi, (sup :&: info) ~ SmartSym fi, SyntacticN f fi,
 sub :<: sup) =>
info (DenResult sig) -> sub sig -> f
sugarSymDecor (TypeRepFun (DenResult sig) -> sub sig -> f)
-> TypeRepFun (DenResult sig) -> sub sig -> f
forall a b. (a -> b) -> a -> b
$ TypeRep (DenResult sig) -> TypeRepFun (DenResult sig)
forall a. TypeRep a -> TypeRepFun a
ValT TypeRep (DenResult sig)
forall a. Type a => TypeRep a
typeRep

-- | Make a smart constructor for a symbol
sugarSymFeldPrim
    :: ( Signature sig
       , fi         ~ SmartFun FeldDomain sig
       , sig        ~ SmartSig fi
       , FeldDomain ~ SmartSym fi
       , SyntacticN f fi
       , sub :<: FeldConstructs
       , PrimType' (DenResult sig)
       )
    => sub sig -> f
sugarSymFeldPrim :: sub sig -> f
sugarSymFeldPrim = TypeRepFun (DenResult sig) -> sub sig -> f
forall sig fi (sup :: * -> *) (info :: * -> *) f (sub :: * -> *).
(Signature sig, fi ~ SmartFun (sup :&: info) sig,
 sig ~ SmartSig fi, (sup :&: info) ~ SmartSym fi, SyntacticN f fi,
 sub :<: sup) =>
info (DenResult sig) -> sub sig -> f
sugarSymDecor (TypeRepFun (DenResult sig) -> sub sig -> f)
-> TypeRepFun (DenResult sig) -> sub sig -> f
forall a b. (a -> b) -> a -> b
$ TypeRep (DenResult sig) -> TypeRepFun (DenResult sig)
forall a. TypeRep a -> TypeRepFun a
ValT (TypeRep (DenResult sig) -> TypeRepFun (DenResult sig))
-> TypeRep (DenResult sig) -> TypeRepFun (DenResult sig)
forall a b. (a -> b) -> a -> b
$ PrimTypeRep (DenResult sig) -> TypeRep (DenResult sig)
forall (pred :: * -> Constraint) a (con :: * -> *).
pred a =>
con a -> Struct pred con a
Single PrimTypeRep (DenResult sig)
forall a. PrimType' a => PrimTypeRep a
primTypeRep

instance Imp.FreeExp Data
  where
    type FreePred Data = PrimType'
    constExp :: a -> Data a
constExp = Primitive (Full a) -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 PrimType' (DenResult sig)) =>
sub sig -> f
sugarSymFeldPrim (Primitive (Full a) -> Data a)
-> (a -> Primitive (Full a)) -> a -> Data a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Primitive (Full a)
forall a. (Eq a, Show a) => a -> Primitive (Full a)
Lit
    varExp :: VarId -> Data a
varExp   = Primitive (Full a) -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 PrimType' (DenResult sig)) =>
sub sig -> f
sugarSymFeldPrim (Primitive (Full a) -> Data a)
-> (VarId -> Primitive (Full a)) -> VarId -> Data a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarId -> Primitive (Full a)
forall a. PrimType' a => VarId -> Primitive (Full a)
FreeVar



--------------------------------------------------------------------------------
-- * Monadic computations
--------------------------------------------------------------------------------

data AssertCMD fs a
  where
    Assert
        :: AssertionLabel
        -> exp Bool
        -> String
        -> AssertCMD (Operational.Param3 prog exp pred) ()

instance Operational.HFunctor AssertCMD
  where
    hfmap :: (forall (b :: k). f b -> g b)
-> AssertCMD '(f, fs) a -> AssertCMD '(g, fs) a
hfmap forall (b :: k). f b -> g b
_ (Assert AssertionLabel
c exp Bool
cond VarId
msg) = AssertionLabel
-> exp Bool -> VarId -> AssertCMD (Param3 g exp pred) ()
forall k k2 (exp :: * -> *) (prog :: k) (pred :: k2).
AssertionLabel
-> exp Bool -> VarId -> AssertCMD (Param3 prog exp pred) ()
Assert AssertionLabel
c exp Bool
cond VarId
msg

instance Operational.HBifunctor AssertCMD
  where
    hbimap :: (forall b. f b -> g b)
-> (forall b. i b -> j b)
-> AssertCMD '(f, '(i, fs)) a
-> AssertCMD '(g, '(j, fs)) a
hbimap forall b. f b -> g b
_ forall b. i b -> j b
g (Assert AssertionLabel
c exp Bool
cond VarId
msg) = AssertionLabel -> j Bool -> VarId -> AssertCMD (Param3 g j pred) ()
forall k k2 (exp :: * -> *) (prog :: k) (pred :: k2).
AssertionLabel
-> exp Bool -> VarId -> AssertCMD (Param3 prog exp pred) ()
Assert AssertionLabel
c (i Bool -> j Bool
forall b. i b -> j b
g i Bool
exp Bool
cond) VarId
msg

instance Operational.InterpBi AssertCMD IO (Operational.Param1 PrimType')
  where
    interpBi :: AssertCMD '(IO, '(IO, Param1 PrimType')) a -> IO a
interpBi (Assert AssertionLabel
_ exp Bool
cond VarId
msg) = do
        Bool
cond' <- exp Bool
IO Bool
cond
        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
cond' (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ VarId -> IO ()
forall a. HasCallStack => VarId -> a
error (VarId -> IO ()) -> VarId -> IO ()
forall a b. (a -> b) -> a -> b
$ VarId
"Assertion failed: " VarId -> ShowS
forall a. [a] -> [a] -> [a]
++ VarId
msg

type CompCMD
  =               Imp.RefCMD
  Operational.:+: Imp.ArrCMD
  Operational.:+: Imp.ControlCMD
  Operational.:+: AssertCMD

-- | Monad for computational effects: mutable data structures and control flow
newtype Comp a = Comp
    { Comp a -> Program CompCMD (Param2 Data PrimType') a
unComp ::
        Operational.Program CompCMD (Operational.Param2 Data PrimType') a
    }
  deriving (a -> Comp b -> Comp a
(a -> b) -> Comp a -> Comp b
(forall a b. (a -> b) -> Comp a -> Comp b)
-> (forall a b. a -> Comp b -> Comp a) -> Functor Comp
forall a b. a -> Comp b -> Comp a
forall a b. (a -> b) -> Comp a -> Comp b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Comp b -> Comp a
$c<$ :: forall a b. a -> Comp b -> Comp a
fmap :: (a -> b) -> Comp a -> Comp b
$cfmap :: forall a b. (a -> b) -> Comp a -> Comp b
Functor, Functor Comp
a -> Comp a
Functor Comp
-> (forall a. a -> Comp a)
-> (forall a b. Comp (a -> b) -> Comp a -> Comp b)
-> (forall a b c. (a -> b -> c) -> Comp a -> Comp b -> Comp c)
-> (forall a b. Comp a -> Comp b -> Comp b)
-> (forall a b. Comp a -> Comp b -> Comp a)
-> Applicative Comp
Comp a -> Comp b -> Comp b
Comp a -> Comp b -> Comp a
Comp (a -> b) -> Comp a -> Comp b
(a -> b -> c) -> Comp a -> Comp b -> Comp c
forall a. a -> Comp a
forall a b. Comp a -> Comp b -> Comp a
forall a b. Comp a -> Comp b -> Comp b
forall a b. Comp (a -> b) -> Comp a -> Comp b
forall a b c. (a -> b -> c) -> Comp a -> Comp b -> Comp c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: Comp a -> Comp b -> Comp a
$c<* :: forall a b. Comp a -> Comp b -> Comp a
*> :: Comp a -> Comp b -> Comp b
$c*> :: forall a b. Comp a -> Comp b -> Comp b
liftA2 :: (a -> b -> c) -> Comp a -> Comp b -> Comp c
$cliftA2 :: forall a b c. (a -> b -> c) -> Comp a -> Comp b -> Comp c
<*> :: Comp (a -> b) -> Comp a -> Comp b
$c<*> :: forall a b. Comp (a -> b) -> Comp a -> Comp b
pure :: a -> Comp a
$cpure :: forall a. a -> Comp a
$cp1Applicative :: Functor Comp
Applicative, Applicative Comp
a -> Comp a
Applicative Comp
-> (forall a b. Comp a -> (a -> Comp b) -> Comp b)
-> (forall a b. Comp a -> Comp b -> Comp b)
-> (forall a. a -> Comp a)
-> Monad Comp
Comp a -> (a -> Comp b) -> Comp b
Comp a -> Comp b -> Comp b
forall a. a -> Comp a
forall a b. Comp a -> Comp b -> Comp b
forall a b. Comp a -> (a -> Comp b) -> Comp b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> Comp a
$creturn :: forall a. a -> Comp a
>> :: Comp a -> Comp b -> Comp b
$c>> :: forall a b. Comp a -> Comp b -> Comp b
>>= :: Comp a -> (a -> Comp b) -> Comp b
$c>>= :: forall a b. Comp a -> (a -> Comp b) -> Comp b
$cp1Monad :: Applicative Comp
Monad)



--------------------------------------------------------------------------------
-- Template Haskell instances
--------------------------------------------------------------------------------

deriveSymbol    ''ExtraPrimitive
deriveRender id ''ExtraPrimitive

deriveSymbol    ''ForLoop
deriveRender id ''ForLoop
deriveEquality  ''ForLoop

deriveSymbol ''Unsafe



--------------------------------------------------------------------------------
-- * Interpretation
--------------------------------------------------------------------------------

-- The stuff below depends on the TH-generated instances. From GHC 9, it seems
-- that generated instances are only in scope after the splice. The alternative
-- to move the splices up into the code is not possible (at least not easily)
-- because of the mutual dependencies between the different types. (Definitions
-- that occur after a splice are not in scope before the splice.)

instance EvalEnv ExtraPrimitive env
instance StringTree ExtraPrimitive

instance EvalEnv ForLoop env
instance StringTree ForLoop

instance EvalEnv Unsafe env
instance StringTree Unsafe

-- | Evaluate a closed expression
eval :: (Syntactic a, Domain a ~ FeldDomain) => a -> Internal a
eval :: a -> Internal a
eval = ASTF FeldDomain (Internal a) -> Internal a
forall (sym :: * -> *) a. EvalEnv sym RunEnv => ASTF sym a -> a
evalClosed (ASTF FeldDomain (Internal a) -> Internal a)
-> (a -> ASTF FeldDomain (Internal a)) -> a -> Internal a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ASTF FeldDomain (Internal a)
forall a. Syntactic a => a -> ASTF (Domain a) (Internal a)
desugar
  -- Note that a `Syntax` constraint would rule out evaluating functions

instance Imp.EvalExp Data
  where
    evalExp :: Data a -> a
evalExp = Data a -> a
forall a. (Syntactic a, Domain a ~ FeldDomain) => a -> Internal a
eval