{-# 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 = Single BoolT
instance Type Int8 where typeRep = Single Int8T
instance Type Int16 where typeRep = Single Int16T
instance Type Int32 where typeRep = Single Int32T
instance Type Int64 where typeRep = Single Int64T
instance Type Word8 where typeRep = Single Word8T
instance Type Word16 where typeRep = Single Word16T
instance Type Word32 where typeRep = Single Word32T
instance Type Word64 where typeRep = Single Word64T
instance Type Float where typeRep = Single FloatT
instance Type Double where typeRep = Single DoubleT
instance Type (Complex Float) where typeRep = Single ComplexFloatT
instance Type (Complex Double) where typeRep = Single ComplexDoubleT
instance (Type a, Type b) => Type (a,b) where typeRep = Two typeRep typeRep
class (PrimType' a, Type a) => PrimType a
instance (PrimType' a, Type a) => PrimType a
instance Imp.CompTypeClass PrimType
where
compType _ = Imp.compType (Proxy :: Proxy PrimType')
compLit _ = Imp.compLit (Proxy :: Proxy PrimType')
toTypeRep :: Struct PrimType' c a -> TypeRep a
toTypeRep = mapStruct (const primTypeRep)
typeEq :: TypeRep a -> TypeRep b -> Maybe (Dict (a ~ b))
typeEq (Single t) (Single u) = primTypeEq t u
typeEq (Two t1 t2) (Two u1 u2) = do
Dict <- typeEq t1 u1
Dict <- typeEq t2 u2
return Dict
typeEq _ _ = Nothing
witTypeable :: TypeRep a -> Dict (Typeable a)
witTypeable (Single t)
| Dict <- witPrimType t
= Dict
witTypeable (Two ta tb)
| Dict <- witTypeable ta
, Dict <- witTypeable tb
= 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 (ValT t) (ValT u) = typeEq t u
typeEqFun (FunT ta tb) (FunT ua ub) = do
Dict <- typeEq ta ua
Dict <- typeEqFun tb ub
return Dict
typeEqFun _ _ = Nothing
newtype Ref a = Ref { unRef :: Struct PrimType' Imp.Ref (Internal a) }
type DRef a = Ref (Data a)
instance Eq (Ref a)
where
Ref a == Ref b = and $ zipListStruct (==) a b
data Arr a = Arr
{ arrOffset :: Data Index
, arrLength :: Data Length
, unArr :: Struct PrimType' (Imp.Arr Index) (Internal a)
}
type DArr a = Arr (Data a)
instance Eq (Arr a)
where
Arr _ _ arr1 == Arr _ _ arr2 = and (zipListStruct (==) arr1 arr2)
data IArr a = IArr
{ iarrOffset :: Data Index
, iarrLength :: Data Length
, unIArr :: Struct PrimType' (Imp.IArr Index) (Internal a)
}
type DIArr a = IArr (Data a)
unsafeEqArrIArr :: Arr a -> IArr a -> Bool
unsafeEqArrIArr (Arr _ _ arr1) (IArr _ _ arr2) =
and (zipListStruct sameId arr1 arr2)
where
sameId :: Imp.Arr Index a -> Imp.IArr Index a -> Bool
sameId (Imp.ArrComp a) (Imp.IArrComp i) = a==i
sameId _ _ = False
data AssertionLabel
= InternalAssertion
| LibraryAssertion String
| UserAssertion String
deriving (Eq, Show)
onlyUserAssertions :: Selection AssertionLabel
onlyUserAssertions = selectBy $ \l -> case l of
UserAssertion _ -> True
_ -> False
data ExtraPrimitive 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 DivBalanced = \a b -> if a `mod` b /= 0
then error $ unwords ["divBalanced", show a, show b, "is not balanced"]
else div a b
evalSym (GuardVal _ msg) = \cond a ->
if cond then a else error $ "Feldspar assertion failure: " ++ msg
instance EvalEnv ExtraPrimitive env
instance Equality ExtraPrimitive
where
equal DivBalanced DivBalanced = True
equal (GuardVal _ _) (GuardVal _ _) = True
equal _ _ = False
hash DivBalanced = hashInt 1
hash (GuardVal _ _) = hashInt 2
instance StringTree ExtraPrimitive
data ForLoop sig
where
ForLoop :: Type st =>
ForLoop (Length :-> st :-> (Index -> st -> st) :-> Full st)
instance Eval ForLoop
where
evalSym ForLoop = \len init body ->
foldl (flip body) init $ genericTake len [0..]
instance EvalEnv ForLoop env
instance StringTree ForLoop
data Unsafe sig
where
UnsafePerform :: Comp (Data a) -> Unsafe (Full a)
instance Render Unsafe
where
renderSym (UnsafePerform _) = "UnsafePerform ..."
instance StringTree Unsafe
instance Eval Unsafe
where
evalSym s = error $ "eval: cannot evaluate unsafe operation " ++ renderSym s
instance EvalEnv Unsafe env
instance Equality Unsafe
where
equal _ _ = False
type FeldConstructs
= BindingT
:+: Let
:+: Tuple
:+: Primitive
:+: ExtraPrimitive
:+: ForLoop
:+: Unsafe
type FeldDomain = FeldConstructs :&: TypeRepFun
newtype Data a = Data { unData :: ASTF FeldDomain a }
instance Syntactic (Data a)
where
type Domain (Data a) = FeldDomain
type Internal (Data a) = a
desugar = unData
sugar = Data
instance Syntactic (Struct PrimType' Data a)
where
type Domain (Struct PrimType' Data a) = FeldDomain
type Internal (Struct PrimType' Data a) = a
desugar (Single a) = unData a
desugar (Two a b) = sugarSymDecor (ValT $ Two ta tb) Pair a' b'
where
a' = desugar a
b' = desugar b
ValT ta = getDecor a'
ValT tb = getDecor b'
sugar a = case getDecor a of
ValT (Single _) -> Single $ Data a
ValT (Two ta tb) ->
Two (sugarSymDecor (ValT ta) Fst a) (sugarSymDecor (ValT tb) Snd 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 = sugarSymDecor $ ValT 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 = sugarSymDecor $ ValT $ Single primTypeRep
eval :: (Syntactic a, Domain a ~ FeldDomain) => a -> Internal a
eval = evalClosed . desugar
instance Imp.FreeExp Data
where
type FreePred Data = PrimType'
constExp = sugarSymFeldPrim . Lit
varExp = sugarSymFeldPrim . FreeVar
instance Imp.EvalExp Data
where
evalExp = eval
data AssertCMD fs a
where
Assert
:: AssertionLabel
-> exp Bool
-> String
-> AssertCMD (Operational.Param3 prog exp pred) ()
instance Operational.HFunctor AssertCMD
where
hfmap _ (Assert c cond msg) = Assert c cond msg
instance Operational.HBifunctor AssertCMD
where
hbimap _ g (Assert c cond msg) = Assert c (g cond) msg
instance Operational.InterpBi AssertCMD IO (Operational.Param1 PrimType')
where
interpBi (Assert _ cond msg) = do
cond' <- cond
unless cond' $ error $ "Assertion failed: " ++ msg
type CompCMD
= Imp.RefCMD
Operational.:+: Imp.ArrCMD
Operational.:+: Imp.ControlCMD
Operational.:+: AssertCMD
newtype Comp a = Comp
{ unComp ::
Operational.Program CompCMD (Operational.Param2 Data PrimType') a
}
deriving (Functor, Applicative, Monad)
deriveSymbol ''ExtraPrimitive
deriveRender id ''ExtraPrimitive
deriveSymbol ''ForLoop
deriveRender id ''ForLoop
deriveEquality ''ForLoop
deriveSymbol ''Unsafe