{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE DataKinds #-}
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 ()
type TypeRep = Struct PrimType' PrimTypeRep
class (Eq a, Show a, Typeable a, Inhabited a) => Type a
where
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
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')
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)
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
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
data TypeRepFun a
where
ValT :: TypeRep a -> TypeRepFun a
FunT :: TypeRep a -> TypeRepFun b -> TypeRepFun (a -> b)
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
newtype Ref a = Ref { Ref a -> Struct PrimType' Ref (Internal a)
unRef :: Struct PrimType' Imp.Ref (Internal a) }
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
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)
}
type DArr a = Arr (Data a)
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)
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)
}
type DIArr a = IArr (Data a)
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
data AssertionLabel
= InternalAssertion
| LibraryAssertion String
| UserAssertion String
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)
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 sig
where
DivBalanced :: (Integral a, PrimType' a) =>
ExtraPrimitive (a :-> a :-> Full a)
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
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..]
data Unsafe sig
where
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
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 }
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)
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)
class (Syntactic a, Domain a ~ FeldDomain, Type (Internal a)) => Syntax a
instance (Syntactic a, Domain a ~ FeldDomain, Type (Internal a)) => Syntax a
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
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
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
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)
deriveSymbol ''ExtraPrimitive
deriveRender id ''ExtraPrimitive
deriveSymbol ''ForLoop
deriveRender id ''ForLoop
deriveEquality ''ForLoop
deriveSymbol ''Unsafe
instance EvalEnv ExtraPrimitive env
instance StringTree ExtraPrimitive
instance EvalEnv ForLoop env
instance StringTree ForLoop
instance EvalEnv Unsafe env
instance StringTree Unsafe
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
instance Imp.EvalExp Data
where
evalExp :: Data a -> a
evalExp = Data a -> a
forall a. (Syntactic a, Domain a ~ FeldDomain) => a -> Internal a
eval