{-# LANGUAGE CPP #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Imperative commands. These commands can be used with the 'Program' monad,
-- and different command types can be combined using (':+:').
--
-- These commands are general imperative constructs independent of the back end,
-- except for 'C_CMD' which is C-specific.

module Language.Embedded.Imperative.CMD
  ( -- * References
    Ref (..)
  , RefCMD (..)
    -- * Arrays
  , Arr (..)
  , IArr (..)
  , ArrCMD (..)
    -- * Control flow
  , Border (..)
  , borderVal
  , borderIncl
  , IxRange
  , ControlCMD (..)
    -- * Generic pointer manipulation
  , IsPointer (..)
  , PtrCMD (..)
    -- * File handling
  , Handle (..)
  , stdin
  , stdout
  , PrintfArg (..)
  , mapPrintfArg
  , mapPrintfArgM
  , Formattable (..)
  , FileCMD (..)
    -- * C-specific commands
  , Ptr (..)
  , Object (..)
  , Arg (..)
  , FunArg (..)
  , mapFunArg
  , mapFunArgM
  , Assignable
  , C_CMD (..)
  ) where



import Control.Monad.Reader
import Data.Array
import Data.Array.IO
import Data.Char (isSpace)
import Data.Int
import Data.IORef
import Data.List
import Data.Typeable
import Data.Word
import System.IO (IOMode (..))
import qualified System.IO as IO
import qualified Text.Printf as Printf

#if __GLASGOW_HASKELL__ < 710
import Control.Applicative
import Data.Foldable hiding (sequence_)
import Data.Traversable (Traversable, traverse)
#endif

import Control.Monad.Operational.Higher

import Control.Monads
import Language.Embedded.Expression
import Language.Embedded.Traversal

-- C-specific imports:
import qualified Language.C.Syntax as C
import Language.C.Quote.C
import Language.C.Monad (CGen)
import Language.Embedded.Backend.C.Expression



--------------------------------------------------------------------------------
-- * References
--------------------------------------------------------------------------------

-- | Mutable reference
data Ref a
    = RefComp VarId
    | RefRun (IORef a)
  deriving (Ref a -> Ref a -> Bool
(Ref a -> Ref a -> Bool) -> (Ref a -> Ref a -> Bool) -> Eq (Ref a)
forall a. Ref a -> Ref a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ref a -> Ref a -> Bool
$c/= :: forall a. Ref a -> Ref a -> Bool
== :: Ref a -> Ref a -> Bool
$c== :: forall a. Ref a -> Ref a -> Bool
Eq, Typeable)

instance ToIdent (Ref a) where toIdent :: Ref a -> SrcLoc -> Id
toIdent (RefComp VarId
r) = VarId -> SrcLoc -> Id
C.Id VarId
r

-- | Commands for mutable references
data RefCMD fs a
  where
    NewRef  :: pred a => String -> RefCMD (Param3 prog exp pred) (Ref a)
    InitRef :: pred a => String -> exp a -> RefCMD (Param3 prog exp pred) (Ref a)
    GetRef  :: pred a => Ref a -> RefCMD (Param3 prog exp pred) (Val a)
    SetRef  :: pred a => Ref a -> exp a -> RefCMD (Param3 prog exp pred) ()
      -- `pred a` for `SetRef` is not needed for code generation, but it can be
      -- useful when interpreting with a dynamically typed store. It can then be
      -- used e.g. to supply a `Typeable` constraint for casting.
    UnsafeFreezeRef :: pred a => Ref a -> RefCMD (Param3 prog exp pred) (Val a)
      -- Like `GetRef` but without using a fresh variable for the result. This
      -- is only safe if the reference is never written to after the freezing.
#if  __GLASGOW_HASKELL__>=708
  deriving Typeable
#endif

instance HFunctor RefCMD
  where
    hfmap :: (forall (b :: k). f b -> g b)
-> RefCMD '(f, fs) a -> RefCMD '(g, fs) a
hfmap forall (b :: k). f b -> g b
_ (NewRef VarId
base)       = VarId -> RefCMD (Param3 g exp pred) (Ref a)
forall k (pred :: * -> Constraint) a (pred :: k) (a :: * -> *).
pred a =>
VarId -> RefCMD (Param3 pred a pred) (Ref a)
NewRef VarId
base
    hfmap forall (b :: k). f b -> g b
_ (InitRef VarId
base exp a
a)    = VarId -> exp a -> RefCMD (Param3 g exp pred) (Ref a)
forall k (pred :: * -> Constraint) a (pred :: * -> *) (a :: k).
pred a =>
VarId -> pred a -> RefCMD (Param3 a pred pred) (Ref a)
InitRef VarId
base exp a
a
    hfmap forall (b :: k). f b -> g b
_ (GetRef Ref a
r)          = Ref a -> RefCMD (Param3 g exp pred) (Val a)
forall k (pred :: * -> Constraint) a (pred :: k) (a :: * -> *).
pred a =>
Ref a -> RefCMD (Param3 pred a pred) (Val a)
GetRef Ref a
r
    hfmap forall (b :: k). f b -> g b
_ (SetRef Ref a
r exp a
a)        = Ref a -> exp a -> RefCMD (Param3 g exp pred) ()
forall k (pred :: * -> Constraint) a (exp :: * -> *) (prog :: k).
pred a =>
Ref a -> exp a -> RefCMD (Param3 prog exp pred) ()
SetRef Ref a
r exp a
a
    hfmap forall (b :: k). f b -> g b
_ (UnsafeFreezeRef Ref a
r) = Ref a -> RefCMD (Param3 g exp pred) (Val a)
forall k (pred :: * -> Constraint) a (pred :: k) (a :: * -> *).
pred a =>
Ref a -> RefCMD (Param3 pred a pred) (Val a)
UnsafeFreezeRef Ref a
r

instance HBifunctor RefCMD
  where
    hbimap :: (forall b. f b -> g b)
-> (forall b. i b -> j b)
-> RefCMD '(f, '(i, fs)) a
-> RefCMD '(g, '(j, fs)) a
hbimap forall b. f b -> g b
_ forall b. i b -> j b
_ (NewRef VarId
base)       = VarId -> RefCMD (Param3 g j pred) (Ref a)
forall k (pred :: * -> Constraint) a (pred :: k) (a :: * -> *).
pred a =>
VarId -> RefCMD (Param3 pred a pred) (Ref a)
NewRef VarId
base
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
f (InitRef VarId
base exp a
a)    = VarId -> j a -> RefCMD (Param3 g j pred) (Ref a)
forall k (pred :: * -> Constraint) a (pred :: * -> *) (a :: k).
pred a =>
VarId -> pred a -> RefCMD (Param3 a pred pred) (Ref a)
InitRef VarId
base (i a -> j a
forall b. i b -> j b
f i a
exp a
a)
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
_ (GetRef Ref a
r)          = Ref a -> RefCMD (Param3 g j pred) (Val a)
forall k (pred :: * -> Constraint) a (pred :: k) (a :: * -> *).
pred a =>
Ref a -> RefCMD (Param3 pred a pred) (Val a)
GetRef Ref a
r
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
f (SetRef Ref a
r exp a
a)        = Ref a -> j a -> RefCMD (Param3 g j pred) ()
forall k (pred :: * -> Constraint) a (exp :: * -> *) (prog :: k).
pred a =>
Ref a -> exp a -> RefCMD (Param3 prog exp pred) ()
SetRef Ref a
r (i a -> j a
forall b. i b -> j b
f i a
exp a
a)
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
_ (UnsafeFreezeRef Ref a
r) = Ref a -> RefCMD (Param3 g j pred) (Val a)
forall k (pred :: * -> Constraint) a (pred :: k) (a :: * -> *).
pred a =>
Ref a -> RefCMD (Param3 pred a pred) (Val a)
UnsafeFreezeRef Ref a
r

instance (RefCMD :<: instr) => Reexpressible RefCMD instr env
  where
    reexpressInstrEnv :: (forall b.
 exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b))
-> RefCMD
     '(ReaderT env (ProgramT instr '(exp2, fs) m), '(exp1, fs)) a
-> ReaderT env (ProgramT instr '(exp2, fs) m) a
reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (NewRef VarId
base)       = ProgramT instr (Param2 exp2 pred) m (Ref a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Ref a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m (Ref a)
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Ref a))
-> ProgramT instr (Param2 exp2 pred) m (Ref a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Ref a)
forall a b. (a -> b) -> a -> b
$ RefCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Ref a)
-> ProgramT instr (Param2 exp2 pred) m (Ref a)
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (RefCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Ref a)
 -> ProgramT instr (Param2 exp2 pred) m (Ref a))
-> RefCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Ref a)
-> ProgramT instr (Param2 exp2 pred) m (Ref a)
forall a b. (a -> b) -> a -> b
$ VarId
-> RefCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Ref a)
forall k (pred :: * -> Constraint) a (pred :: k) (a :: * -> *).
pred a =>
VarId -> RefCMD (Param3 pred a pred) (Ref a)
NewRef VarId
base
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (InitRef VarId
base exp a
a)    = ProgramT instr (Param2 exp2 pred) m (Ref a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Ref a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m (Ref a)
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Ref a))
-> (exp2 a -> ProgramT instr (Param2 exp2 pred) m (Ref a))
-> exp2 a
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Ref a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RefCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Ref a)
-> ProgramT instr (Param2 exp2 pred) m (Ref a)
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (RefCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Ref a)
 -> ProgramT instr (Param2 exp2 pred) m (Ref a))
-> (exp2 a
    -> RefCMD
         '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Ref a))
-> exp2 a
-> ProgramT instr (Param2 exp2 pred) m (Ref a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarId
-> exp2 a
-> RefCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Ref a)
forall k (pred :: * -> Constraint) a (pred :: * -> *) (a :: k).
pred a =>
VarId -> pred a -> RefCMD (Param3 a pred pred) (Ref a)
InitRef VarId
base (exp2 a
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Ref a))
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (exp2 a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Ref a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< exp1 a -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 a)
forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp exp1 a
exp a
a
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (GetRef Ref a
r)          = ProgramT instr (Param2 exp2 pred) m (Val a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m (Val a)
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val a))
-> ProgramT instr (Param2 exp2 pred) m (Val a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val a)
forall a b. (a -> b) -> a -> b
$ RefCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a)
-> ProgramT instr (Param2 exp2 pred) m (Val a)
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (RefCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a)
 -> ProgramT instr (Param2 exp2 pred) m (Val a))
-> RefCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a)
-> ProgramT instr (Param2 exp2 pred) m (Val a)
forall a b. (a -> b) -> a -> b
$ Ref a
-> RefCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a)
forall k (pred :: * -> Constraint) a (pred :: k) (a :: * -> *).
pred a =>
Ref a -> RefCMD (Param3 pred a pred) (Val a)
GetRef Ref a
r
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (SetRef Ref a
r exp a
a)        = ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m ()
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> (exp2 a -> ProgramT instr (Param2 exp2 pred) m ())
-> exp2 a
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RefCMD '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (RefCMD '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
 -> ProgramT instr (Param2 exp2 pred) m ())
-> (exp2 a
    -> RefCMD
         '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ())
-> exp2 a
-> ProgramT instr (Param2 exp2 pred) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ref a
-> exp2 a
-> RefCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall k (pred :: * -> Constraint) a (exp :: * -> *) (prog :: k).
pred a =>
Ref a -> exp a -> RefCMD (Param3 prog exp pred) ()
SetRef Ref a
r (exp2 a -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (exp2 a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< exp1 a -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 a)
forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp exp1 a
exp a
a
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (UnsafeFreezeRef Ref a
r) = ProgramT instr (Param2 exp2 pred) m (Val a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m (Val a)
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val a))
-> ProgramT instr (Param2 exp2 pred) m (Val a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val a)
forall a b. (a -> b) -> a -> b
$ RefCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a)
-> ProgramT instr (Param2 exp2 pred) m (Val a)
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (RefCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a)
 -> ProgramT instr (Param2 exp2 pred) m (Val a))
-> RefCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a)
-> ProgramT instr (Param2 exp2 pred) m (Val a)
forall a b. (a -> b) -> a -> b
$ Ref a
-> RefCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a)
forall k (pred :: * -> Constraint) a (pred :: k) (a :: * -> *).
pred a =>
Ref a -> RefCMD (Param3 pred a pred) (Val a)
UnsafeFreezeRef Ref a
r

instance DryInterp RefCMD
  where
    dryInterp :: RefCMD '(m, fs) a -> m a
dryInterp (NewRef VarId
base)    = (VarId -> Ref a) -> m VarId -> m (Ref a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM VarId -> Ref a
forall a. VarId -> Ref a
RefComp (m VarId -> m (Ref a)) -> m VarId -> m (Ref a)
forall a b. (a -> b) -> a -> b
$ VarId -> m VarId
forall (m :: * -> *). MonadSupply m => VarId -> m VarId
freshStr VarId
base
    dryInterp (InitRef VarId
base exp a
_) = (VarId -> Ref a) -> m VarId -> m (Ref a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM VarId -> Ref a
forall a. VarId -> Ref a
RefComp (m VarId -> m (Ref a)) -> m VarId -> m (Ref a)
forall a b. (a -> b) -> a -> b
$ VarId -> m VarId
forall (m :: * -> *). MonadSupply m => VarId -> m VarId
freshStr VarId
base
    dryInterp (GetRef Ref a
_)       = (VarId -> Val a) -> m VarId -> m (Val a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM VarId -> Val a
forall a. VarId -> Val a
ValComp (m VarId -> m (Val a)) -> m VarId -> m (Val a)
forall a b. (a -> b) -> a -> b
$ VarId -> m VarId
forall (m :: * -> *). MonadSupply m => VarId -> m VarId
freshStr VarId
"v"
    dryInterp (SetRef Ref a
_ exp a
_)     = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    dryInterp (UnsafeFreezeRef (RefComp VarId
v)) = Val a -> m (Val a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Val a -> m (Val a)) -> Val a -> m (Val a)
forall a b. (a -> b) -> a -> b
$ VarId -> Val a
forall a. VarId -> Val a
ValComp VarId
v



--------------------------------------------------------------------------------
-- * Arrays
--------------------------------------------------------------------------------

-- | Mutable array
data Arr i a
    = ArrComp VarId
    | ArrRun (IORef (IOArray i a))
        -- The `IORef` is needed in order to make the `IsPointer` instance
  deriving (Arr i a -> Arr i a -> Bool
(Arr i a -> Arr i a -> Bool)
-> (Arr i a -> Arr i a -> Bool) -> Eq (Arr i a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall i a. Arr i a -> Arr i a -> Bool
/= :: Arr i a -> Arr i a -> Bool
$c/= :: forall i a. Arr i a -> Arr i a -> Bool
== :: Arr i a -> Arr i a -> Bool
$c== :: forall i a. Arr i a -> Arr i a -> Bool
Eq, Typeable)

-- | Immutable array
data IArr i a
    = IArrComp VarId
    | IArrRun (Array i a)
  deriving (Int -> IArr i a -> ShowS
[IArr i a] -> ShowS
IArr i a -> VarId
(Int -> IArr i a -> ShowS)
-> (IArr i a -> VarId) -> ([IArr i a] -> ShowS) -> Show (IArr i a)
forall a.
(Int -> a -> ShowS) -> (a -> VarId) -> ([a] -> ShowS) -> Show a
forall i a. (Ix i, Show i, Show a) => Int -> IArr i a -> ShowS
forall i a. (Ix i, Show i, Show a) => [IArr i a] -> ShowS
forall i a. (Ix i, Show i, Show a) => IArr i a -> VarId
showList :: [IArr i a] -> ShowS
$cshowList :: forall i a. (Ix i, Show i, Show a) => [IArr i a] -> ShowS
show :: IArr i a -> VarId
$cshow :: forall i a. (Ix i, Show i, Show a) => IArr i a -> VarId
showsPrec :: Int -> IArr i a -> ShowS
$cshowsPrec :: forall i a. (Ix i, Show i, Show a) => Int -> IArr i a -> ShowS
Show, Typeable)

-- In a way, it's not terribly useful to have `Arr` parameterized on the index
-- type, since it's required to be an integer type, and it doesn't really matter
-- which integer type is used since we can always cast between them.
--
-- Another option would be to remove the parameter and allow any integer type
-- when indexing (and use e.g. `IOArray Word32` for running). However this has
-- the big downside of losing type inference. E.g. the statement `getArr arr 0`
-- would be ambiguously typed.
--
-- Yet another option is to hard-code a specific index type. But this would
-- limit the use of arrays to specific platforms.
--
-- So in the end, the above representation seems like a good trade-off. A client
-- of `imperative-edsl` may always chose to make a wrapper interface that uses
-- a specific index type.

instance ToIdent (Arr i a)  where toIdent :: Arr i a -> SrcLoc -> Id
toIdent (ArrComp VarId
arr)  = VarId -> SrcLoc -> Id
C.Id VarId
arr
instance ToIdent (IArr i a) where toIdent :: IArr i a -> SrcLoc -> Id
toIdent (IArrComp VarId
arr) = VarId -> SrcLoc -> Id
C.Id VarId
arr

-- | Commands for mutable arrays
data ArrCMD fs a
  where
    NewArr   :: (pred a, pred i, Integral i, Ix i) => String -> exp i -> ArrCMD (Param3 prog exp pred) (Arr i a)
    ConstArr :: (pred a, pred i, Integral i, Ix i) => String -> [a] -> ArrCMD (Param3 prog exp pred) (Arr i a)
    GetArr   :: (pred a, pred i, Integral i, Ix i) => Arr i a -> exp i -> ArrCMD (Param3 prog exp pred) (Val a)
    SetArr   :: (pred a, pred i, Integral i, Ix i) => Arr i a -> exp i -> exp a -> ArrCMD (Param3 prog exp pred) ()
    CopyArr  :: (pred a, pred i, Integral i, Ix i) => (Arr i a, exp i) -> (Arr i a, exp i) -> exp i -> ArrCMD (Param3 prog exp pred) ()
      -- The arrays are paired with their offset
    UnsafeFreezeArr :: (pred a, pred i, Integral i, Ix i) => Arr i a -> ArrCMD (Param3 prog exp pred) (IArr i a)
    UnsafeThawArr   :: (pred a, pred i, Integral i, Ix i) => IArr i a -> ArrCMD (Param3 prog exp pred) (Arr i a)
#if  __GLASGOW_HASKELL__>=708
  deriving Typeable
#endif
  -- Not all `pred` constraints are needed by the back ends in imperative-edsl,
  -- but they may still be useful for other back ends.

instance HFunctor ArrCMD
  where
    hfmap :: (forall (b :: k). f b -> g b)
-> ArrCMD '(f, fs) a -> ArrCMD '(g, fs) a
hfmap forall (b :: k). f b -> g b
_ (NewArr VarId
base exp i
n)       = VarId -> exp i -> ArrCMD (Param3 g exp pred) (Arr i a)
forall k (pred :: * -> Constraint) a i (exp :: * -> *) (prog :: k).
(pred a, pred i, Integral i, Ix i) =>
VarId -> exp i -> ArrCMD (Param3 prog exp pred) (Arr i a)
NewArr VarId
base exp i
n
    hfmap forall (b :: k). f b -> g b
_ (ConstArr VarId
base [a]
as)    = VarId -> [a] -> ArrCMD (Param3 g exp pred) (Arr i a)
forall k (pred :: * -> Constraint) a i (prog :: k) (exp :: * -> *).
(pred a, pred i, Integral i, Ix i) =>
VarId -> [a] -> ArrCMD (Param3 prog exp pred) (Arr i a)
ConstArr VarId
base [a]
as
    hfmap forall (b :: k). f b -> g b
_ (GetArr Arr i a
i exp i
arr)        = Arr i a -> exp i -> ArrCMD (Param3 g exp pred) (Val a)
forall k (pred :: * -> Constraint) a i (exp :: * -> *) (prog :: k).
(pred a, pred i, Integral i, Ix i) =>
Arr i a -> exp i -> ArrCMD (Param3 prog exp pred) (Val a)
GetArr Arr i a
i exp i
arr
    hfmap forall (b :: k). f b -> g b
_ (SetArr Arr i a
i exp i
a exp a
arr)      = Arr i a -> exp i -> exp a -> ArrCMD (Param3 g exp pred) ()
forall k (pred :: * -> Constraint) a i (exp :: * -> *) (prog :: k).
(pred a, pred i, Integral i, Ix i) =>
Arr i a -> exp i -> exp a -> ArrCMD (Param3 prog exp pred) ()
SetArr Arr i a
i exp i
a exp a
arr
    hfmap forall (b :: k). f b -> g b
_ (CopyArr (Arr i a, exp i)
a1 (Arr i a, exp i)
a2 exp i
l)     = (Arr i a, exp i)
-> (Arr i a, exp i) -> exp i -> ArrCMD (Param3 g exp pred) ()
forall k (pred :: * -> Constraint) a i (exp :: * -> *) (prog :: k).
(pred a, pred i, Integral i, Ix i) =>
(Arr i a, exp i)
-> (Arr i a, exp i) -> exp i -> ArrCMD (Param3 prog exp pred) ()
CopyArr (Arr i a, exp i)
a1 (Arr i a, exp i)
a2 exp i
l
    hfmap forall (b :: k). f b -> g b
_ (UnsafeFreezeArr Arr i a
arr) = Arr i a -> ArrCMD (Param3 g exp pred) (IArr i a)
forall k (pred :: * -> Constraint) a i (prog :: k) (exp :: * -> *).
(pred a, pred i, Integral i, Ix i) =>
Arr i a -> ArrCMD (Param3 prog exp pred) (IArr i a)
UnsafeFreezeArr Arr i a
arr
    hfmap forall (b :: k). f b -> g b
_ (UnsafeThawArr IArr i a
arr)   = IArr i a -> ArrCMD (Param3 g exp pred) (Arr i a)
forall k (pred :: * -> Constraint) a i (prog :: k) (exp :: * -> *).
(pred a, pred i, Integral i, Ix i) =>
IArr i a -> ArrCMD (Param3 prog exp pred) (Arr i a)
UnsafeThawArr IArr i a
arr

instance HBifunctor ArrCMD
  where
    hbimap :: (forall b. f b -> g b)
-> (forall b. i b -> j b)
-> ArrCMD '(f, '(i, fs)) a
-> ArrCMD '(g, '(j, fs)) a
hbimap forall b. f b -> g b
_ forall b. i b -> j b
f (NewArr VarId
base exp i
n)             = VarId -> j i -> ArrCMD (Param3 g j pred) (Arr i a)
forall k (pred :: * -> Constraint) a i (exp :: * -> *) (prog :: k).
(pred a, pred i, Integral i, Ix i) =>
VarId -> exp i -> ArrCMD (Param3 prog exp pred) (Arr i a)
NewArr VarId
base (i i -> j i
forall b. i b -> j b
f i i
exp i
n)
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
_ (ConstArr VarId
base [a]
as)          = VarId -> [a] -> ArrCMD (Param3 g j pred) (Arr i a)
forall k (pred :: * -> Constraint) a i (prog :: k) (exp :: * -> *).
(pred a, pred i, Integral i, Ix i) =>
VarId -> [a] -> ArrCMD (Param3 prog exp pred) (Arr i a)
ConstArr VarId
base [a]
as
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
f (GetArr Arr i a
arr exp i
i)              = Arr i a -> j i -> ArrCMD (Param3 g j pred) (Val a)
forall k (pred :: * -> Constraint) a i (exp :: * -> *) (prog :: k).
(pred a, pred i, Integral i, Ix i) =>
Arr i a -> exp i -> ArrCMD (Param3 prog exp pred) (Val a)
GetArr Arr i a
arr (i i -> j i
forall b. i b -> j b
f i i
exp i
i)
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
f (SetArr Arr i a
arr exp i
i exp a
a)            = Arr i a -> j i -> j a -> ArrCMD (Param3 g j pred) ()
forall k (pred :: * -> Constraint) a i (exp :: * -> *) (prog :: k).
(pred a, pred i, Integral i, Ix i) =>
Arr i a -> exp i -> exp a -> ArrCMD (Param3 prog exp pred) ()
SetArr Arr i a
arr (i i -> j i
forall b. i b -> j b
f i i
exp i
i) (i a -> j a
forall b. i b -> j b
f i a
exp a
a)
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
f (CopyArr (Arr i a
a1,exp i
o1) (Arr i a
a2,exp i
o2) exp i
l) = (Arr i a, j i)
-> (Arr i a, j i) -> j i -> ArrCMD (Param3 g j pred) ()
forall k (pred :: * -> Constraint) a i (exp :: * -> *) (prog :: k).
(pred a, pred i, Integral i, Ix i) =>
(Arr i a, exp i)
-> (Arr i a, exp i) -> exp i -> ArrCMD (Param3 prog exp pred) ()
CopyArr (Arr i a
a1, i i -> j i
forall b. i b -> j b
f i i
exp i
o1) (Arr i a
a2, i i -> j i
forall b. i b -> j b
f i i
exp i
o2) (i i -> j i
forall b. i b -> j b
f i i
exp i
l)
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
_ (UnsafeFreezeArr Arr i a
arr)       = Arr i a -> ArrCMD (Param3 g j pred) (IArr i a)
forall k (pred :: * -> Constraint) a i (prog :: k) (exp :: * -> *).
(pred a, pred i, Integral i, Ix i) =>
Arr i a -> ArrCMD (Param3 prog exp pred) (IArr i a)
UnsafeFreezeArr Arr i a
arr
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
_ (UnsafeThawArr IArr i a
arr)         = IArr i a -> ArrCMD (Param3 g j pred) (Arr i a)
forall k (pred :: * -> Constraint) a i (prog :: k) (exp :: * -> *).
(pred a, pred i, Integral i, Ix i) =>
IArr i a -> ArrCMD (Param3 prog exp pred) (Arr i a)
UnsafeThawArr IArr i a
arr

instance (ArrCMD :<: instr) => Reexpressible ArrCMD instr env
  where
    reexpressInstrEnv :: (forall b.
 exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b))
-> ArrCMD
     '(ReaderT env (ProgramT instr '(exp2, fs) m), '(exp1, fs)) a
-> ReaderT env (ProgramT instr '(exp2, fs) m) a
reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (NewArr VarId
base exp i
n)       = ProgramT instr (Param2 exp2 pred) m (Arr i a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Arr i a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m (Arr i a)
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Arr i a))
-> (exp2 i -> ProgramT instr (Param2 exp2 pred) m (Arr i a))
-> exp2 i
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Arr i a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArrCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a)
-> ProgramT instr (Param2 exp2 pred) m (Arr i a)
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (ArrCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a)
 -> ProgramT instr (Param2 exp2 pred) m (Arr i a))
-> (exp2 i
    -> ArrCMD
         '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a))
-> exp2 i
-> ProgramT instr (Param2 exp2 pred) m (Arr i a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarId
-> exp2 i
-> ArrCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a)
forall k (pred :: * -> Constraint) a i (exp :: * -> *) (prog :: k).
(pred a, pred i, Integral i, Ix i) =>
VarId -> exp i -> ArrCMD (Param3 prog exp pred) (Arr i a)
NewArr VarId
base (exp2 i
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Arr i a))
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (exp2 i)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Arr i a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< exp1 i -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 i)
forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp exp1 i
exp i
n
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (ConstArr VarId
base [a]
as)    = ProgramT instr (Param2 exp2 pred) m (Arr i a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Arr i a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m (Arr i a)
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Arr i a))
-> ProgramT instr (Param2 exp2 pred) m (Arr i a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Arr i a)
forall a b. (a -> b) -> a -> b
$ ArrCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a)
-> ProgramT instr (Param2 exp2 pred) m (Arr i a)
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (ArrCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a)
 -> ProgramT instr (Param2 exp2 pred) m (Arr i a))
-> ArrCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a)
-> ProgramT instr (Param2 exp2 pred) m (Arr i a)
forall a b. (a -> b) -> a -> b
$ VarId
-> [a]
-> ArrCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a)
forall k (pred :: * -> Constraint) a i (prog :: k) (exp :: * -> *).
(pred a, pred i, Integral i, Ix i) =>
VarId -> [a] -> ArrCMD (Param3 prog exp pred) (Arr i a)
ConstArr VarId
base [a]
as
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (GetArr Arr i a
arr exp i
i)        = ProgramT instr (Param2 exp2 pred) m (Val a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m (Val a)
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val a))
-> (exp2 i -> ProgramT instr (Param2 exp2 pred) m (Val a))
-> exp2 i
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArrCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a)
-> ProgramT instr (Param2 exp2 pred) m (Val a)
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (ArrCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a)
 -> ProgramT instr (Param2 exp2 pred) m (Val a))
-> (exp2 i
    -> ArrCMD
         '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a))
-> exp2 i
-> ProgramT instr (Param2 exp2 pred) m (Val a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arr i a
-> exp2 i
-> ArrCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a)
forall k (pred :: * -> Constraint) a i (exp :: * -> *) (prog :: k).
(pred a, pred i, Integral i, Ix i) =>
Arr i a -> exp i -> ArrCMD (Param3 prog exp pred) (Val a)
GetArr Arr i a
arr (exp2 i
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val a))
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (exp2 i)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< exp1 i -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 i)
forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp exp1 i
exp i
i
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (SetArr Arr i a
arr exp i
i exp a
a)      = do exp2 i
i' <- exp1 i -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 i)
forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp exp1 i
exp i
i; exp2 a
a' <- exp1 a -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 a)
forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp exp1 a
exp a
a; ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m ()
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall a b. (a -> b) -> a -> b
$ ArrCMD '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (ArrCMD '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
 -> ProgramT instr (Param2 exp2 pred) m ())
-> ArrCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall a b. (a -> b) -> a -> b
$ Arr i a
-> exp2 i
-> exp2 a
-> ArrCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall k (pred :: * -> Constraint) a i (exp :: * -> *) (prog :: k).
(pred a, pred i, Integral i, Ix i) =>
Arr i a -> exp i -> exp a -> ArrCMD (Param3 prog exp pred) ()
SetArr Arr i a
arr exp2 i
i' exp2 a
a'
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (UnsafeFreezeArr Arr i a
arr) = ProgramT instr (Param2 exp2 pred) m (IArr i a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (IArr i a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m (IArr i a)
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (IArr i a))
-> ProgramT instr (Param2 exp2 pred) m (IArr i a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (IArr i a)
forall a b. (a -> b) -> a -> b
$ ArrCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (IArr i a)
-> ProgramT instr (Param2 exp2 pred) m (IArr i a)
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (ArrCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (IArr i a)
 -> ProgramT instr (Param2 exp2 pred) m (IArr i a))
-> ArrCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (IArr i a)
-> ProgramT instr (Param2 exp2 pred) m (IArr i a)
forall a b. (a -> b) -> a -> b
$ Arr i a
-> ArrCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (IArr i a)
forall k (pred :: * -> Constraint) a i (prog :: k) (exp :: * -> *).
(pred a, pred i, Integral i, Ix i) =>
Arr i a -> ArrCMD (Param3 prog exp pred) (IArr i a)
UnsafeFreezeArr Arr i a
arr
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (UnsafeThawArr IArr i a
arr)   = ProgramT instr (Param2 exp2 pred) m (Arr i a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Arr i a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m (Arr i a)
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Arr i a))
-> ProgramT instr (Param2 exp2 pred) m (Arr i a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Arr i a)
forall a b. (a -> b) -> a -> b
$ ArrCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a)
-> ProgramT instr (Param2 exp2 pred) m (Arr i a)
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (ArrCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a)
 -> ProgramT instr (Param2 exp2 pred) m (Arr i a))
-> ArrCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a)
-> ProgramT instr (Param2 exp2 pred) m (Arr i a)
forall a b. (a -> b) -> a -> b
$ IArr i a
-> ArrCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a)
forall k (pred :: * -> Constraint) a i (prog :: k) (exp :: * -> *).
(pred a, pred i, Integral i, Ix i) =>
IArr i a -> ArrCMD (Param3 prog exp pred) (Arr i a)
UnsafeThawArr IArr i a
arr
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (CopyArr (Arr i a
a1,exp i
o1) (Arr i a
a2,exp i
o2) exp i
l) = do
        exp2 i
o1' <- exp1 i -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 i)
forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp exp1 i
exp i
o1
        exp2 i
o2' <- exp1 i -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 i)
forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp exp1 i
exp i
o2
        exp2 i
l'  <- exp1 i -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 i)
forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp exp1 i
exp i
l
        ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m ()
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall a b. (a -> b) -> a -> b
$ ArrCMD '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (ArrCMD '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
 -> ProgramT instr (Param2 exp2 pred) m ())
-> ArrCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall a b. (a -> b) -> a -> b
$ (Arr i a, exp2 i)
-> (Arr i a, exp2 i)
-> exp2 i
-> ArrCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall k (pred :: * -> Constraint) a i (exp :: * -> *) (prog :: k).
(pred a, pred i, Integral i, Ix i) =>
(Arr i a, exp i)
-> (Arr i a, exp i) -> exp i -> ArrCMD (Param3 prog exp pred) ()
CopyArr (Arr i a
a1,exp2 i
o1') (Arr i a
a2,exp2 i
o2') exp2 i
l'

instance DryInterp ArrCMD
  where
    dryInterp :: ArrCMD '(m, fs) a -> m a
dryInterp (NewArr VarId
base exp i
_)   = (VarId -> Arr i a) -> m VarId -> m (Arr i a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM VarId -> Arr i a
forall i a. VarId -> Arr i a
ArrComp (m VarId -> m (Arr i a)) -> m VarId -> m (Arr i a)
forall a b. (a -> b) -> a -> b
$ VarId -> m VarId
forall (m :: * -> *). MonadSupply m => VarId -> m VarId
freshStr VarId
base
    dryInterp (ConstArr VarId
base [a]
_) = (VarId -> Arr i a) -> m VarId -> m (Arr i a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM VarId -> Arr i a
forall i a. VarId -> Arr i a
ArrComp (m VarId -> m (Arr i a)) -> m VarId -> m (Arr i a)
forall a b. (a -> b) -> a -> b
$ VarId -> m VarId
forall (m :: * -> *). MonadSupply m => VarId -> m VarId
freshStr VarId
base
    dryInterp (GetArr Arr i a
_ exp i
_)      = (VarId -> Val a) -> m VarId -> m (Val a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM VarId -> Val a
forall a. VarId -> Val a
ValComp (m VarId -> m (Val a)) -> m VarId -> m (Val a)
forall a b. (a -> b) -> a -> b
$ VarId -> m VarId
forall (m :: * -> *). MonadSupply m => VarId -> m VarId
freshStr VarId
"v"
    dryInterp (SetArr Arr i a
_ exp i
_ exp a
_)    = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    dryInterp (CopyArr (Arr i a, exp i)
_ (Arr i a, exp i)
_ exp i
_)   = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    dryInterp (UnsafeFreezeArr (ArrComp VarId
arr)) = IArr i a -> m (IArr i a)
forall (m :: * -> *) a. Monad m => a -> m a
return (VarId -> IArr i a
forall i a. VarId -> IArr i a
IArrComp VarId
arr)
    dryInterp (UnsafeThawArr (IArrComp VarId
arr))  = Arr i a -> m (Arr i a)
forall (m :: * -> *) a. Monad m => a -> m a
return (VarId -> Arr i a
forall i a. VarId -> Arr i a
ArrComp VarId
arr)



--------------------------------------------------------------------------------
-- * Control flow
--------------------------------------------------------------------------------

data Border i = Incl i | Excl i
  deriving (Border i -> Border i -> Bool
(Border i -> Border i -> Bool)
-> (Border i -> Border i -> Bool) -> Eq (Border i)
forall i. Eq i => Border i -> Border i -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Border i -> Border i -> Bool
$c/= :: forall i. Eq i => Border i -> Border i -> Bool
== :: Border i -> Border i -> Bool
$c== :: forall i. Eq i => Border i -> Border i -> Bool
Eq, Int -> Border i -> ShowS
[Border i] -> ShowS
Border i -> VarId
(Int -> Border i -> ShowS)
-> (Border i -> VarId) -> ([Border i] -> ShowS) -> Show (Border i)
forall i. Show i => Int -> Border i -> ShowS
forall i. Show i => [Border i] -> ShowS
forall i. Show i => Border i -> VarId
forall a.
(Int -> a -> ShowS) -> (a -> VarId) -> ([a] -> ShowS) -> Show a
showList :: [Border i] -> ShowS
$cshowList :: forall i. Show i => [Border i] -> ShowS
show :: Border i -> VarId
$cshow :: forall i. Show i => Border i -> VarId
showsPrec :: Int -> Border i -> ShowS
$cshowsPrec :: forall i. Show i => Int -> Border i -> ShowS
Show, a -> Border b -> Border a
(a -> b) -> Border a -> Border b
(forall a b. (a -> b) -> Border a -> Border b)
-> (forall a b. a -> Border b -> Border a) -> Functor Border
forall a b. a -> Border b -> Border a
forall a b. (a -> b) -> Border a -> Border b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Border b -> Border a
$c<$ :: forall a b. a -> Border b -> Border a
fmap :: (a -> b) -> Border a -> Border b
$cfmap :: forall a b. (a -> b) -> Border a -> Border b
Functor, Border a -> Bool
(a -> m) -> Border a -> m
(a -> b -> b) -> b -> Border a -> b
(forall m. Monoid m => Border m -> m)
-> (forall m a. Monoid m => (a -> m) -> Border a -> m)
-> (forall m a. Monoid m => (a -> m) -> Border a -> m)
-> (forall a b. (a -> b -> b) -> b -> Border a -> b)
-> (forall a b. (a -> b -> b) -> b -> Border a -> b)
-> (forall b a. (b -> a -> b) -> b -> Border a -> b)
-> (forall b a. (b -> a -> b) -> b -> Border a -> b)
-> (forall a. (a -> a -> a) -> Border a -> a)
-> (forall a. (a -> a -> a) -> Border a -> a)
-> (forall a. Border a -> [a])
-> (forall a. Border a -> Bool)
-> (forall a. Border a -> Int)
-> (forall a. Eq a => a -> Border a -> Bool)
-> (forall a. Ord a => Border a -> a)
-> (forall a. Ord a => Border a -> a)
-> (forall a. Num a => Border a -> a)
-> (forall a. Num a => Border a -> a)
-> Foldable Border
forall a. Eq a => a -> Border a -> Bool
forall a. Num a => Border a -> a
forall a. Ord a => Border a -> a
forall m. Monoid m => Border m -> m
forall a. Border a -> Bool
forall a. Border a -> Int
forall a. Border a -> [a]
forall a. (a -> a -> a) -> Border a -> a
forall m a. Monoid m => (a -> m) -> Border a -> m
forall b a. (b -> a -> b) -> b -> Border a -> b
forall a b. (a -> b -> b) -> b -> Border a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Border a -> a
$cproduct :: forall a. Num a => Border a -> a
sum :: Border a -> a
$csum :: forall a. Num a => Border a -> a
minimum :: Border a -> a
$cminimum :: forall a. Ord a => Border a -> a
maximum :: Border a -> a
$cmaximum :: forall a. Ord a => Border a -> a
elem :: a -> Border a -> Bool
$celem :: forall a. Eq a => a -> Border a -> Bool
length :: Border a -> Int
$clength :: forall a. Border a -> Int
null :: Border a -> Bool
$cnull :: forall a. Border a -> Bool
toList :: Border a -> [a]
$ctoList :: forall a. Border a -> [a]
foldl1 :: (a -> a -> a) -> Border a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Border a -> a
foldr1 :: (a -> a -> a) -> Border a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Border a -> a
foldl' :: (b -> a -> b) -> b -> Border a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Border a -> b
foldl :: (b -> a -> b) -> b -> Border a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Border a -> b
foldr' :: (a -> b -> b) -> b -> Border a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Border a -> b
foldr :: (a -> b -> b) -> b -> Border a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Border a -> b
foldMap' :: (a -> m) -> Border a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Border a -> m
foldMap :: (a -> m) -> Border a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Border a -> m
fold :: Border m -> m
$cfold :: forall m. Monoid m => Border m -> m
Foldable, Functor Border
Foldable Border
Functor Border
-> Foldable Border
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Border a -> f (Border b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Border (f a) -> f (Border a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Border a -> m (Border b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Border (m a) -> m (Border a))
-> Traversable Border
(a -> f b) -> Border a -> f (Border b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Border (m a) -> m (Border a)
forall (f :: * -> *) a.
Applicative f =>
Border (f a) -> f (Border a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Border a -> m (Border b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Border a -> f (Border b)
sequence :: Border (m a) -> m (Border a)
$csequence :: forall (m :: * -> *) a. Monad m => Border (m a) -> m (Border a)
mapM :: (a -> m b) -> Border a -> m (Border b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Border a -> m (Border b)
sequenceA :: Border (f a) -> f (Border a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Border (f a) -> f (Border a)
traverse :: (a -> f b) -> Border a -> f (Border b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Border a -> f (Border b)
$cp2Traversable :: Foldable Border
$cp1Traversable :: Functor Border
Traversable)

-- | 'fromInteger' gives an inclusive border. No other methods defined.
instance Num i => Num (Border i)
  where
    fromInteger :: Integer -> Border i
fromInteger = i -> Border i
forall i. i -> Border i
Incl (i -> Border i) -> (Integer -> i) -> Integer -> Border i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> i
forall a. Num a => Integer -> a
fromInteger
    + :: Border i -> Border i -> Border i
(+) = VarId -> Border i -> Border i -> Border i
forall a. HasCallStack => VarId -> a
error VarId
"(+) not defined for Border"
    (-) = VarId -> Border i -> Border i -> Border i
forall a. HasCallStack => VarId -> a
error VarId
"(-) not defined for Border"
    * :: Border i -> Border i -> Border i
(*) = VarId -> Border i -> Border i -> Border i
forall a. HasCallStack => VarId -> a
error VarId
"(*) not defined for Border"
    abs :: Border i -> Border i
abs    = VarId -> Border i -> Border i
forall a. HasCallStack => VarId -> a
error VarId
"abs not defined for Border"
    signum :: Border i -> Border i
signum = VarId -> Border i -> Border i
forall a. HasCallStack => VarId -> a
error VarId
"signum not defined for Border"

borderVal :: Border i -> i
borderVal :: Border i -> i
borderVal (Incl i
i) = i
i
borderVal (Excl i
i) = i
i

borderIncl :: Border i -> Bool
borderIncl :: Border i -> Bool
borderIncl (Incl i
_) = Bool
True
borderIncl Border i
_        = Bool
False

-- | Index range
--
-- @(lo,step,hi)@
--
-- @lo@ gives the start index; @step@ gives the step length; @hi@ gives the stop
-- index which may be inclusive or exclusive.
type IxRange i = (i, Int, Border i)

data ControlCMD fs a
  where
    If      :: exp Bool -> prog () -> prog () -> ControlCMD (Param3 prog exp pred) ()
    While   :: prog (exp Bool) -> prog () -> ControlCMD (Param3 prog exp pred) ()
    For     :: (pred i, Integral i) => IxRange (exp i) -> (Val i -> prog ()) -> ControlCMD (Param3 prog exp pred) ()
    Break   :: ControlCMD (Param3 prog exp pred) ()
    Assert  :: exp Bool -> String -> ControlCMD (Param3 prog exp pred) ()
    Hint    :: pred a => exp a -> ControlCMD (Param3 prog exp pred) ()
    Comment :: String -> ControlCMD (Param3 prog exp pred) ()

instance HFunctor ControlCMD
  where
    hfmap :: (forall b. f b -> g b)
-> ControlCMD '(f, fs) a -> ControlCMD '(g, fs) a
hfmap forall b. f b -> g b
f (If exp Bool
c prog ()
thn prog ()
els)    = exp Bool -> g () -> g () -> ControlCMD (Param3 g exp pred) ()
forall (exp :: * -> *) (prog :: * -> *) (pred :: * -> Constraint).
exp Bool
-> prog () -> prog () -> ControlCMD (Param3 prog exp pred) ()
If exp Bool
c (f () -> g ()
forall b. f b -> g b
f f ()
prog ()
thn) (f () -> g ()
forall b. f b -> g b
f f ()
prog ()
els)
    hfmap forall b. f b -> g b
f (While prog (exp Bool)
cont prog ()
body) = g (exp Bool) -> g () -> ControlCMD (Param3 g exp pred) ()
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
prog (exp Bool) -> prog () -> ControlCMD (Param3 prog exp pred) ()
While (f (exp Bool) -> g (exp Bool)
forall b. f b -> g b
f f (exp Bool)
prog (exp Bool)
cont) (f () -> g ()
forall b. f b -> g b
f f ()
prog ()
body)
    hfmap forall b. f b -> g b
f (For IxRange (exp i)
rng Val i -> prog ()
body)    = IxRange (exp i)
-> (Val i -> g ()) -> ControlCMD (Param3 g exp pred) ()
forall (pred :: * -> Constraint) i (prog :: * -> *)
       (exp :: * -> *).
(pred i, Integral i) =>
IxRange (prog i)
-> (Val i -> exp ()) -> ControlCMD (Param3 exp prog pred) ()
For IxRange (exp i)
rng (f () -> g ()
forall b. f b -> g b
f (f () -> g ()) -> (Val i -> f ()) -> Val i -> g ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Val i -> f ()
Val i -> prog ()
body)
    hfmap forall b. f b -> g b
_ ControlCMD '(f, fs) a
Break             = ControlCMD '(g, fs) a
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
ControlCMD (Param3 prog exp pred) ()
Break
    hfmap forall b. f b -> g b
_ (Assert exp Bool
cond VarId
msg) = exp Bool -> VarId -> ControlCMD (Param3 g exp pred) ()
forall (exp :: * -> *) (prog :: * -> *) (pred :: * -> Constraint).
exp Bool -> VarId -> ControlCMD (Param3 prog exp pred) ()
Assert exp Bool
cond VarId
msg
    hfmap forall b. f b -> g b
_ (Hint exp a
exp)        = exp a -> ControlCMD (Param3 g exp pred) ()
forall (pred :: * -> Constraint) a (prog :: * -> *)
       (exp :: * -> *).
pred a =>
prog a -> ControlCMD (Param3 exp prog pred) ()
Hint exp a
exp
    hfmap forall b. f b -> g b
_ (Comment VarId
msg)     = VarId -> ControlCMD (Param3 g exp pred) ()
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
VarId -> ControlCMD (Param3 prog exp pred) ()
Comment VarId
msg

instance HBifunctor ControlCMD
  where
    hbimap :: (forall b. f b -> g b)
-> (forall b. i b -> j b)
-> ControlCMD '(f, '(i, fs)) a
-> ControlCMD '(g, '(j, fs)) a
hbimap forall b. f b -> g b
f forall b. i b -> j b
g (If exp Bool
c prog ()
thn prog ()
els)          = j Bool -> g () -> g () -> ControlCMD (Param3 g j pred) ()
forall (exp :: * -> *) (prog :: * -> *) (pred :: * -> Constraint).
exp Bool
-> prog () -> prog () -> ControlCMD (Param3 prog exp pred) ()
If (i Bool -> j Bool
forall b. i b -> j b
g i Bool
exp Bool
c) (f () -> g ()
forall b. f b -> g b
f f ()
prog ()
thn) (f () -> g ()
forall b. f b -> g b
f f ()
prog ()
els)
    hbimap forall b. f b -> g b
f forall b. i b -> j b
g (While prog (exp Bool)
cont prog ()
body)       = g (j Bool) -> g () -> ControlCMD (Param3 g j pred) ()
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
prog (exp Bool) -> prog () -> ControlCMD (Param3 prog exp pred) ()
While (f (j Bool) -> g (j Bool)
forall b. f b -> g b
f (f (j Bool) -> g (j Bool)) -> f (j Bool) -> g (j Bool)
forall a b. (a -> b) -> a -> b
$ (i Bool -> j Bool) -> prog (i Bool) -> prog (j Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap i Bool -> j Bool
forall b. i b -> j b
g prog (i Bool)
prog (exp Bool)
cont) (f () -> g ()
forall b. f b -> g b
f f ()
prog ()
body)
    hbimap forall b. f b -> g b
f forall b. i b -> j b
g (For (exp i
lo,Int
step,Border (exp i)
hi) Val i -> prog ()
body) = IxRange (j i) -> (Val i -> g ()) -> ControlCMD (Param3 g j pred) ()
forall (pred :: * -> Constraint) i (prog :: * -> *)
       (exp :: * -> *).
(pred i, Integral i) =>
IxRange (prog i)
-> (Val i -> exp ()) -> ControlCMD (Param3 exp prog pred) ()
For (i i -> j i
forall b. i b -> j b
g i i
exp i
lo, Int
step, (i i -> j i) -> Border (i i) -> Border (j i)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap i i -> j i
forall b. i b -> j b
g Border (i i)
Border (exp i)
hi) (f () -> g ()
forall b. f b -> g b
f (f () -> g ()) -> (Val i -> f ()) -> Val i -> g ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Val i -> f ()
Val i -> prog ()
body)
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
_ ControlCMD '(f, '(i, fs)) a
Break                   = ControlCMD '(g, '(j, fs)) a
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
ControlCMD (Param3 prog exp pred) ()
Break
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
g (Assert exp Bool
cond VarId
msg)       = j Bool -> VarId -> ControlCMD (Param3 g j pred) ()
forall (exp :: * -> *) (prog :: * -> *) (pred :: * -> Constraint).
exp Bool -> VarId -> ControlCMD (Param3 prog exp pred) ()
Assert (i Bool -> j Bool
forall b. i b -> j b
g i Bool
exp Bool
cond) VarId
msg
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
g (Hint exp a
exp)              = j a -> ControlCMD (Param3 g j pred) ()
forall (pred :: * -> Constraint) a (prog :: * -> *)
       (exp :: * -> *).
pred a =>
prog a -> ControlCMD (Param3 exp prog pred) ()
Hint (i a -> j a
forall b. i b -> j b
g i a
exp a
exp)
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
_ (Comment VarId
msg)           = VarId -> ControlCMD (Param3 g j pred) ()
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
VarId -> ControlCMD (Param3 prog exp pred) ()
Comment VarId
msg

instance (ControlCMD :<: instr) => Reexpressible ControlCMD instr env
  where
    reexpressInstrEnv :: (forall b.
 exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b))
-> ControlCMD
     '(ReaderT env (ProgramT instr '(exp2, fs) m), '(exp1, fs)) a
-> ReaderT env (ProgramT instr '(exp2, fs) m) a
reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (If exp Bool
c prog ()
thn prog ()
els) = do
        exp2 Bool
c' <- exp1 Bool -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 Bool)
forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp exp1 Bool
exp Bool
c
        (env -> ProgramT instr (Param2 exp2 pred) m ())
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((env -> ProgramT instr (Param2 exp2 pred) m ())
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> (env -> ProgramT instr (Param2 exp2 pred) m ())
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall a b. (a -> b) -> a -> b
$ \env
env ->
          ControlCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (ControlCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
 -> ProgramT instr (Param2 exp2 pred) m ())
-> ControlCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall a b. (a -> b) -> a -> b
$ exp2 Bool
-> ProgramT instr (Param2 exp2 pred) m ()
-> ProgramT instr (Param2 exp2 pred) m ()
-> ControlCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall (exp :: * -> *) (prog :: * -> *) (pred :: * -> Constraint).
exp Bool
-> prog () -> prog () -> ControlCMD (Param3 prog exp pred) ()
If exp2 Bool
c' (ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
-> env -> ProgramT instr (Param2 exp2 pred) m ()
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT prog ()
ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
thn env
env) (ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
-> env -> ProgramT instr (Param2 exp2 pred) m ()
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT prog ()
ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
els env
env)
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (While prog (exp Bool)
cont prog ()
body) = (env -> ProgramT instr (Param2 exp2 pred) m ())
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((env -> ProgramT instr (Param2 exp2 pred) m ())
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> (env -> ProgramT instr (Param2 exp2 pred) m ())
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall a b. (a -> b) -> a -> b
$ \env
env ->
        ControlCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (ControlCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
 -> ProgramT instr (Param2 exp2 pred) m ())
-> ControlCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall a b. (a -> b) -> a -> b
$ ProgramT instr (Param2 exp2 pred) m (exp2 Bool)
-> ProgramT instr (Param2 exp2 pred) m ()
-> ControlCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
prog (exp Bool) -> prog () -> ControlCMD (Param3 prog exp pred) ()
While
            (ReaderT env (ProgramT instr (Param2 exp2 pred) m) (exp2 Bool)
-> env -> ProgramT instr (Param2 exp2 pred) m (exp2 Bool)
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (prog (exp Bool)
cont prog (exp Bool)
-> (exp Bool -> prog (exp2 Bool)) -> prog (exp2 Bool)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= exp Bool -> prog (exp2 Bool)
forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp) env
env)
            (ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
-> env -> ProgramT instr (Param2 exp2 pred) m ()
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT prog ()
ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
body env
env)
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (For (exp i
lo,Int
step,Border (exp i)
hi) Val i -> prog ()
body) = do
        exp2 i
lo' <- exp1 i -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 i)
forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp exp1 i
exp i
lo
        Border (exp2 i)
hi' <- (exp1 i -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 i))
-> Border (exp1 i)
-> ReaderT env (ProgramT instr '(exp2, fs) m) (Border (exp2 i))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse exp1 i -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 i)
forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp Border (exp1 i)
Border (exp i)
hi
        (env -> ProgramT instr (Param2 exp2 pred) m ())
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((env -> ProgramT instr (Param2 exp2 pred) m ())
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> (env -> ProgramT instr (Param2 exp2 pred) m ())
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall a b. (a -> b) -> a -> b
$ \env
env -> ControlCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (ControlCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
 -> ProgramT instr (Param2 exp2 pred) m ())
-> ControlCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall a b. (a -> b) -> a -> b
$
            IxRange (exp2 i)
-> (Val i -> ProgramT instr (Param2 exp2 pred) m ())
-> ControlCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall (pred :: * -> Constraint) i (prog :: * -> *)
       (exp :: * -> *).
(pred i, Integral i) =>
IxRange (prog i)
-> (Val i -> exp ()) -> ControlCMD (Param3 exp prog pred) ()
For (exp2 i
lo',Int
step,Border (exp2 i)
hi') ((ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
 -> env -> ProgramT instr (Param2 exp2 pred) m ())
-> env
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
-> env -> ProgramT instr (Param2 exp2 pred) m ()
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT env
env (ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
 -> ProgramT instr (Param2 exp2 pred) m ())
-> (Val i -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> Val i
-> ProgramT instr (Param2 exp2 pred) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Val i -> prog ()
Val i -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
body)
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp ControlCMD
  '(ReaderT env (ProgramT instr '(exp2, fs) m), '(exp1, fs)) a
Break             = ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m ()
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall a b. (a -> b) -> a -> b
$ ControlCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj ControlCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
ControlCMD (Param3 prog exp pred) ()
Break
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (Assert exp Bool
cond VarId
msg) = ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m ()
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> (exp2 Bool -> ProgramT instr (Param2 exp2 pred) m ())
-> exp2 Bool
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ControlCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (ControlCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
 -> ProgramT instr (Param2 exp2 pred) m ())
-> (exp2 Bool
    -> ControlCMD
         '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ())
-> exp2 Bool
-> ProgramT instr (Param2 exp2 pred) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (exp2 Bool
 -> VarId
 -> ControlCMD
      '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ())
-> VarId
-> exp2 Bool
-> ControlCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip exp2 Bool
-> VarId
-> ControlCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall (exp :: * -> *) (prog :: * -> *) (pred :: * -> Constraint).
exp Bool -> VarId -> ControlCMD (Param3 prog exp pred) ()
Assert VarId
msg (exp2 Bool -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (exp2 Bool)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< exp1 Bool -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 Bool)
forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp exp1 Bool
exp Bool
cond
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (Hint exp a
exp)        = ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m ()
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> (exp2 a -> ProgramT instr (Param2 exp2 pred) m ())
-> exp2 a
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ControlCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (ControlCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
 -> ProgramT instr (Param2 exp2 pred) m ())
-> (exp2 a
    -> ControlCMD
         '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ())
-> exp2 a
-> ProgramT instr (Param2 exp2 pred) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. exp2 a
-> ControlCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall (pred :: * -> Constraint) a (prog :: * -> *)
       (exp :: * -> *).
pred a =>
prog a -> ControlCMD (Param3 exp prog pred) ()
Hint (exp2 a -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (exp2 a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< exp1 a -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 a)
forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp exp1 a
exp a
exp
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (Comment VarId
msg)     = ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m ()
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall a b. (a -> b) -> a -> b
$ ControlCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (VarId
-> ControlCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
VarId -> ControlCMD (Param3 prog exp pred) ()
Comment VarId
msg)

instance DryInterp ControlCMD
  where
    dryInterp :: ControlCMD '(m, fs) a -> m a
dryInterp (If exp Bool
_ prog ()
_ prog ()
_)   = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    dryInterp (While prog (exp Bool)
_ prog ()
_)  = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    dryInterp (For IxRange (exp i)
_ Val i -> prog ()
_)    = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    dryInterp ControlCMD '(m, fs) a
Break        = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    dryInterp (Assert exp Bool
_ VarId
_) = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    dryInterp (Hint exp a
_)     = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    dryInterp (Comment VarId
_)  = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    


--------------------------------------------------------------------------------
-- * Generic pointer manipulation
--------------------------------------------------------------------------------

-- The reason for not implementing `SwapPtr` using the `Ptr` type is that it's
-- (currently) not possible to interpret `Ptr` in `IO`.

-- | Types that are represented as a pointers in C
class ToIdent a => IsPointer a
  where
    runSwapPtr :: a -> a -> IO ()

instance IsPointer (Arr i a)
  where
    runSwapPtr :: Arr i a -> Arr i a -> IO ()
runSwapPtr (ArrRun IORef (IOArray i a)
arr1) (ArrRun IORef (IOArray i a)
arr2) = do
        IOArray i a
arr1' <- IORef (IOArray i a) -> IO (IOArray i a)
forall a. IORef a -> IO a
readIORef IORef (IOArray i a)
arr1
        IOArray i a
arr2' <- IORef (IOArray i a) -> IO (IOArray i a)
forall a. IORef a -> IO a
readIORef IORef (IOArray i a)
arr2
        IORef (IOArray i a) -> IOArray i a -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (IOArray i a)
arr1 IOArray i a
arr2'
        IORef (IOArray i a) -> IOArray i a -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (IOArray i a)
arr2 IOArray i a
arr1'

instance IsPointer (Ptr a)
  where
    runSwapPtr :: Ptr a -> Ptr a -> IO ()
runSwapPtr = VarId -> Ptr a -> Ptr a -> IO ()
forall a. HasCallStack => VarId -> a
error VarId
"cannot run SwapPtr for Ptr"

data PtrCMD fs a
  where
    SwapPtr :: Ptr a -> Ptr a -> PtrCMD (Param3 prog exp pred) ()
    SwapArr :: (Typeable i, Typeable a, pred i, pred a)
      => Arr i a -> Arr i a -> PtrCMD (Param3 prog exp pred) ()

instance HFunctor   PtrCMD
  where
    hfmap :: (forall (b :: k). f b -> g b)
-> PtrCMD '(f, fs) a -> PtrCMD '(g, fs) a
hfmap forall (b :: k). f b -> g b
_    (SwapPtr Ptr a
a Ptr a
b) = Ptr a -> Ptr a -> PtrCMD (Param3 g exp pred) ()
forall k k1 a (prog :: k) (i :: k1) (a :: * -> Constraint).
Ptr a -> Ptr a -> PtrCMD (Param3 prog i a) ()
SwapPtr Ptr a
a Ptr a
b
    hfmap forall (b :: k). f b -> g b
_    (SwapArr Arr i a
a Arr i a
b) = Arr i a -> Arr i a -> PtrCMD (Param3 g exp pred) ()
forall k k1 i a (pred :: * -> Constraint) (prog :: k) (exp :: k1).
(Typeable i, Typeable a, pred i, pred a) =>
Arr i a -> Arr i a -> PtrCMD (Param3 prog exp pred) ()
SwapArr Arr i a
a Arr i a
b
    
instance HBifunctor PtrCMD
  where
    hbimap :: (forall b. f b -> g b)
-> (forall (b :: k). i b -> j b)
-> PtrCMD '(f, '(i, fs)) a
-> PtrCMD '(g, '(j, fs)) a
hbimap forall b. f b -> g b
_ forall (b :: k). i b -> j b
_ (SwapPtr Ptr a
a Ptr a
b) = Ptr a -> Ptr a -> PtrCMD (Param3 g j pred) ()
forall k k1 a (prog :: k) (i :: k1) (a :: * -> Constraint).
Ptr a -> Ptr a -> PtrCMD (Param3 prog i a) ()
SwapPtr Ptr a
a Ptr a
b
    hbimap forall b. f b -> g b
_ forall (b :: k). i b -> j b
_ (SwapArr Arr i a
a Arr i a
b) = Arr i a -> Arr i a -> PtrCMD (Param3 g j pred) ()
forall k k1 i a (pred :: * -> Constraint) (prog :: k) (exp :: k1).
(Typeable i, Typeable a, pred i, pred a) =>
Arr i a -> Arr i a -> PtrCMD (Param3 prog exp pred) ()
SwapArr Arr i a
a Arr i a
b

instance (PtrCMD :<: instr) => Reexpressible PtrCMD instr env
  where
    reexpressInstrEnv :: (forall (b :: k).
 exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b))
-> PtrCMD
     '(ReaderT env (ProgramT instr '(exp2, fs) m), '(exp1, fs)) a
-> ReaderT env (ProgramT instr '(exp2, fs) m) a
reexpressInstrEnv forall (b :: k).
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (SwapPtr Ptr a
a Ptr a
b) = ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m ()
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall a b. (a -> b) -> a -> b
$ PtrCMD '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (Ptr a
-> Ptr a
-> PtrCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall k k1 a (prog :: k) (i :: k1) (a :: * -> Constraint).
Ptr a -> Ptr a -> PtrCMD (Param3 prog i a) ()
SwapPtr Ptr a
a Ptr a
b)
    reexpressInstrEnv forall (b :: k).
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (SwapArr Arr i a
a Arr i a
b) = ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m ()
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall a b. (a -> b) -> a -> b
$ PtrCMD '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (Arr i a
-> Arr i a
-> PtrCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall k k1 i a (pred :: * -> Constraint) (prog :: k) (exp :: k1).
(Typeable i, Typeable a, pred i, pred a) =>
Arr i a -> Arr i a -> PtrCMD (Param3 prog exp pred) ()
SwapArr Arr i a
a Arr i a
b)

instance DryInterp PtrCMD
  where
    dryInterp :: PtrCMD '(m, fs) a -> m a
dryInterp (SwapPtr Ptr a
_ Ptr a
_) = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    dryInterp (SwapArr Arr i a
_ Arr i a
_) = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()



--------------------------------------------------------------------------------
-- * File handling
--------------------------------------------------------------------------------

-- | File handle
data Handle
    = HandleComp VarId
    | HandleRun IO.Handle
  deriving (Handle -> Handle -> Bool
(Handle -> Handle -> Bool)
-> (Handle -> Handle -> Bool) -> Eq Handle
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Handle -> Handle -> Bool
$c/= :: Handle -> Handle -> Bool
== :: Handle -> Handle -> Bool
$c== :: Handle -> Handle -> Bool
Eq, Int -> Handle -> ShowS
[Handle] -> ShowS
Handle -> VarId
(Int -> Handle -> ShowS)
-> (Handle -> VarId) -> ([Handle] -> ShowS) -> Show Handle
forall a.
(Int -> a -> ShowS) -> (a -> VarId) -> ([a] -> ShowS) -> Show a
showList :: [Handle] -> ShowS
$cshowList :: [Handle] -> ShowS
show :: Handle -> VarId
$cshow :: Handle -> VarId
showsPrec :: Int -> Handle -> ShowS
$cshowsPrec :: Int -> Handle -> ShowS
Show, Typeable)

instance ToIdent Handle where toIdent :: Handle -> SrcLoc -> Id
toIdent (HandleComp VarId
h) = VarId -> SrcLoc -> Id
C.Id VarId
h

-- | Handle to stdin
stdin :: Handle
stdin :: Handle
stdin = VarId -> Handle
HandleComp VarId
"stdin"

-- | Handle to stdout
stdout :: Handle
stdout :: Handle
stdout = VarId -> Handle
HandleComp VarId
"stdout"

data PrintfArg exp pred
  where
    PrintfArg :: (Printf.PrintfArg a, pred a) => exp a -> PrintfArg exp pred

mapPrintfArg
    :: (forall a . pred a => exp1 a -> exp2 a)
    -> PrintfArg exp1 pred -> PrintfArg exp2 pred
mapPrintfArg :: (forall a. pred a => exp1 a -> exp2 a)
-> PrintfArg exp1 pred -> PrintfArg exp2 pred
mapPrintfArg forall a. pred a => exp1 a -> exp2 a
f (PrintfArg exp1 a
exp) = exp2 a -> PrintfArg exp2 pred
forall a (pred :: * -> Constraint) (exp :: * -> *).
(PrintfArg a, pred a) =>
exp a -> PrintfArg exp pred
PrintfArg (exp1 a -> exp2 a
forall a. pred a => exp1 a -> exp2 a
f exp1 a
exp)

mapPrintfArgM :: Monad m
    => (forall a . pred a => exp1 a -> m (exp2 a))
    -> PrintfArg exp1 pred -> m (PrintfArg exp2 pred)
mapPrintfArgM :: (forall a. pred a => exp1 a -> m (exp2 a))
-> PrintfArg exp1 pred -> m (PrintfArg exp2 pred)
mapPrintfArgM forall a. pred a => exp1 a -> m (exp2 a)
f (PrintfArg exp1 a
exp) = (exp2 a -> PrintfArg exp2 pred)
-> m (exp2 a) -> m (PrintfArg exp2 pred)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM exp2 a -> PrintfArg exp2 pred
forall a (pred :: * -> Constraint) (exp :: * -> *).
(PrintfArg a, pred a) =>
exp a -> PrintfArg exp pred
PrintfArg (exp1 a -> m (exp2 a)
forall a. pred a => exp1 a -> m (exp2 a)
f exp1 a
exp)

-- | Values that can be printed\/scanned using @printf@\/@scanf@
class (Typeable a, Read a, Printf.PrintfArg a) => Formattable a
  where
    -- | Format specifier for `printf`
    formatSpecPrint :: Proxy a -> String
    -- | Format specifier for `scanf`
    formatSpecScan  :: Proxy a -> String
    formatSpecScan = Proxy a -> VarId
forall a. Formattable a => Proxy a -> VarId
formatSpecPrint

instance Formattable Int    where formatSpecPrint :: Proxy Int -> VarId
formatSpecPrint Proxy Int
_ = VarId
"%d"
instance Formattable Int8   where formatSpecPrint :: Proxy Int8 -> VarId
formatSpecPrint Proxy Int8
_ = VarId
"%hhd"
instance Formattable Int16  where formatSpecPrint :: Proxy Int16 -> VarId
formatSpecPrint Proxy Int16
_ = VarId
"%hd"
instance Formattable Int32  where formatSpecPrint :: Proxy Int32 -> VarId
formatSpecPrint Proxy Int32
_ = VarId
"%d"
instance Formattable Int64  where formatSpecPrint :: Proxy Int64 -> VarId
formatSpecPrint Proxy Int64
_ = VarId
"%ld"
instance Formattable Word   where formatSpecPrint :: Proxy Word -> VarId
formatSpecPrint Proxy Word
_ = VarId
"%u"
instance Formattable Word8  where formatSpecPrint :: Proxy Word8 -> VarId
formatSpecPrint Proxy Word8
_ = VarId
"%hhu"
instance Formattable Word16 where formatSpecPrint :: Proxy Word16 -> VarId
formatSpecPrint Proxy Word16
_ = VarId
"%hu"
instance Formattable Word32 where formatSpecPrint :: Proxy Word32 -> VarId
formatSpecPrint Proxy Word32
_ = VarId
"%u"
instance Formattable Word64 where formatSpecPrint :: Proxy Word64 -> VarId
formatSpecPrint Proxy Word64
_ = VarId
"%lu"

instance Formattable Float
  where
    formatSpecPrint :: Proxy Float -> VarId
formatSpecPrint Proxy Float
_ = VarId
"%.9g"
      -- See <http://stackoverflow.com/a/21162120/1105347>
    formatSpecScan :: Proxy Float -> VarId
formatSpecScan Proxy Float
_ = VarId
"%g"

instance Formattable Double
  where
    formatSpecPrint :: Proxy Double -> VarId
formatSpecPrint Proxy Double
_ = VarId
"%.17g"
      -- See <http://stackoverflow.com/a/21162120/1105347>
    formatSpecScan :: Proxy Double -> VarId
formatSpecScan Proxy Double
_ = VarId
"%lg"
      -- See <http://stackoverflow.com/q/210590/1105347>

data FileCMD fs a
  where
    FOpen   :: FilePath -> IOMode -> FileCMD (Param3 prog exp pred) Handle
    FClose  :: Handle -> FileCMD (Param3 prog exp pred) ()
    FEof    :: Handle -> FileCMD (Param3 prog exp pred) (Val Bool)
    FPrintf :: Handle -> String -> [PrintfArg exp pred] -> FileCMD (Param3 prog exp pred) ()
    FGet    :: (pred a, Formattable a) => Handle   -> FileCMD (Param3 prog exp pred) (Val a)

instance HFunctor FileCMD
  where
    hfmap :: (forall (b :: k). f b -> g b)
-> FileCMD '(f, fs) a -> FileCMD '(g, fs) a
hfmap forall (b :: k). f b -> g b
_ (FOpen VarId
file IOMode
mode)     = VarId -> IOMode -> FileCMD (Param3 g exp pred) Handle
forall k (prog :: k) (exp :: * -> *) (pred :: * -> Constraint).
VarId -> IOMode -> FileCMD (Param3 prog exp pred) Handle
FOpen VarId
file IOMode
mode
    hfmap forall (b :: k). f b -> g b
_ (FClose Handle
hdl)          = Handle -> FileCMD (Param3 g exp pred) ()
forall k (prog :: k) (exp :: * -> *) (pred :: * -> Constraint).
Handle -> FileCMD (Param3 prog exp pred) ()
FClose Handle
hdl
    hfmap forall (b :: k). f b -> g b
_ (FPrintf Handle
hdl VarId
form [PrintfArg exp pred]
as) = Handle
-> VarId -> [PrintfArg exp pred] -> FileCMD (Param3 g exp pred) ()
forall k (exp :: * -> *) (pred :: * -> Constraint) (prog :: k).
Handle
-> VarId
-> [PrintfArg exp pred]
-> FileCMD (Param3 prog exp pred) ()
FPrintf Handle
hdl VarId
form [PrintfArg exp pred]
as
    hfmap forall (b :: k). f b -> g b
_ (FGet Handle
hdl)            = Handle -> FileCMD (Param3 g exp pred) (Val a)
forall k (pred :: * -> Constraint) a (prog :: k) (exp :: * -> *).
(pred a, Formattable a) =>
Handle -> FileCMD (Param3 prog exp pred) (Val a)
FGet Handle
hdl
    hfmap forall (b :: k). f b -> g b
_ (FEof Handle
hdl)            = Handle -> FileCMD (Param3 g exp pred) (Val Bool)
forall k (prog :: k) (exp :: * -> *) (pred :: * -> Constraint).
Handle -> FileCMD (Param3 prog exp pred) (Val Bool)
FEof Handle
hdl

instance HBifunctor FileCMD
  where
    hbimap :: (forall b. f b -> g b)
-> (forall b. i b -> j b)
-> FileCMD '(f, '(i, fs)) a
-> FileCMD '(g, '(j, fs)) a
hbimap forall b. f b -> g b
_ forall b. i b -> j b
_ (FOpen VarId
file IOMode
mode)     = VarId -> IOMode -> FileCMD (Param3 g j pred) Handle
forall k (prog :: k) (exp :: * -> *) (pred :: * -> Constraint).
VarId -> IOMode -> FileCMD (Param3 prog exp pred) Handle
FOpen VarId
file IOMode
mode
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
_ (FClose Handle
hdl)          = Handle -> FileCMD (Param3 g j pred) ()
forall k (prog :: k) (exp :: * -> *) (pred :: * -> Constraint).
Handle -> FileCMD (Param3 prog exp pred) ()
FClose Handle
hdl
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
f (FPrintf Handle
hdl VarId
form [PrintfArg exp pred]
as) = Handle
-> VarId -> [PrintfArg j pred] -> FileCMD (Param3 g j pred) ()
forall k (exp :: * -> *) (pred :: * -> Constraint) (prog :: k).
Handle
-> VarId
-> [PrintfArg exp pred]
-> FileCMD (Param3 prog exp pred) ()
FPrintf Handle
hdl VarId
form ((PrintfArg exp pred -> PrintfArg j pred)
-> [PrintfArg exp pred] -> [PrintfArg j pred]
forall a b. (a -> b) -> [a] -> [b]
map ((forall a. pred a => exp a -> j a)
-> PrintfArg exp pred -> PrintfArg j pred
forall (pred :: * -> Constraint) (exp1 :: * -> *) (exp2 :: * -> *).
(forall a. pred a => exp1 a -> exp2 a)
-> PrintfArg exp1 pred -> PrintfArg exp2 pred
mapPrintfArg forall b. i b -> j b
forall a. pred a => exp a -> j a
f) [PrintfArg exp pred]
as)
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
_ (FGet Handle
hdl)            = Handle -> FileCMD (Param3 g j pred) (Val a)
forall k (pred :: * -> Constraint) a (prog :: k) (exp :: * -> *).
(pred a, Formattable a) =>
Handle -> FileCMD (Param3 prog exp pred) (Val a)
FGet Handle
hdl
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
_ (FEof Handle
hdl)            = Handle -> FileCMD (Param3 g j pred) (Val Bool)
forall k (prog :: k) (exp :: * -> *) (pred :: * -> Constraint).
Handle -> FileCMD (Param3 prog exp pred) (Val Bool)
FEof Handle
hdl

instance (FileCMD :<: instr) => Reexpressible FileCMD instr env
  where
    reexpressInstrEnv :: (forall b.
 exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b))
-> FileCMD
     '(ReaderT env (ProgramT instr '(exp2, fs) m), '(exp1, fs)) a
-> ReaderT env (ProgramT instr '(exp2, fs) m) a
reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (FOpen VarId
file IOMode
mode)   = ProgramT instr (Param2 exp2 pred) m Handle
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) Handle
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m Handle
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) Handle)
-> ProgramT instr (Param2 exp2 pred) m Handle
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) Handle
forall a b. (a -> b) -> a -> b
$ FileCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) Handle
-> ProgramT instr (Param2 exp2 pred) m Handle
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (FileCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) Handle
 -> ProgramT instr (Param2 exp2 pred) m Handle)
-> FileCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) Handle
-> ProgramT instr (Param2 exp2 pred) m Handle
forall a b. (a -> b) -> a -> b
$ VarId
-> IOMode
-> FileCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) Handle
forall k (prog :: k) (exp :: * -> *) (pred :: * -> Constraint).
VarId -> IOMode -> FileCMD (Param3 prog exp pred) Handle
FOpen VarId
file IOMode
mode
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (FClose Handle
h)          = ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m ()
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall a b. (a -> b) -> a -> b
$ FileCMD '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (FileCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
 -> ProgramT instr (Param2 exp2 pred) m ())
-> FileCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall a b. (a -> b) -> a -> b
$ Handle
-> FileCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall k (prog :: k) (exp :: * -> *) (pred :: * -> Constraint).
Handle -> FileCMD (Param3 prog exp pred) ()
FClose Handle
h
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (FEof Handle
h)            = ProgramT instr (Param2 exp2 pred) m (Val Bool)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val Bool)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m (Val Bool)
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val Bool))
-> ProgramT instr (Param2 exp2 pred) m (Val Bool)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val Bool)
forall a b. (a -> b) -> a -> b
$ FileCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val Bool)
-> ProgramT instr (Param2 exp2 pred) m (Val Bool)
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (FileCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val Bool)
 -> ProgramT instr (Param2 exp2 pred) m (Val Bool))
-> FileCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val Bool)
-> ProgramT instr (Param2 exp2 pred) m (Val Bool)
forall a b. (a -> b) -> a -> b
$ Handle
-> FileCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val Bool)
forall k (prog :: k) (exp :: * -> *) (pred :: * -> Constraint).
Handle -> FileCMD (Param3 prog exp pred) (Val Bool)
FEof Handle
h
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (FPrintf Handle
h VarId
form [PrintfArg exp pred]
as) = ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m ()
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ([PrintfArg exp2 pred]
    -> ProgramT instr (Param2 exp2 pred) m ())
-> [PrintfArg exp2 pred]
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FileCMD '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (FileCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
 -> ProgramT instr (Param2 exp2 pred) m ())
-> ([PrintfArg exp2 pred]
    -> FileCMD
         '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ())
-> [PrintfArg exp2 pred]
-> ProgramT instr (Param2 exp2 pred) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle
-> VarId
-> [PrintfArg exp2 pred]
-> FileCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall k (exp :: * -> *) (pred :: * -> Constraint) (prog :: k).
Handle
-> VarId
-> [PrintfArg exp pred]
-> FileCMD (Param3 prog exp pred) ()
FPrintf Handle
h VarId
form ([PrintfArg exp2 pred]
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ReaderT
     env (ProgramT instr (Param2 exp2 pred) m) [PrintfArg exp2 pred]
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (PrintfArg exp pred
 -> ReaderT
      env (ProgramT instr (Param2 exp2 pred) m) (PrintfArg exp2 pred))
-> [PrintfArg exp pred]
-> ReaderT
     env (ProgramT instr (Param2 exp2 pred) m) [PrintfArg exp2 pred]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((forall a.
 pred a =>
 exp a
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (exp2 a))
-> PrintfArg exp pred
-> ReaderT
     env (ProgramT instr (Param2 exp2 pred) m) (PrintfArg exp2 pred)
forall (m :: * -> *) (pred :: * -> Constraint) (exp1 :: * -> *)
       (exp2 :: * -> *).
Monad m =>
(forall a. pred a => exp1 a -> m (exp2 a))
-> PrintfArg exp1 pred -> m (PrintfArg exp2 pred)
mapPrintfArgM forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
forall a.
pred a =>
exp a -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (exp2 a)
reexp) [PrintfArg exp pred]
as
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (FGet Handle
h)            = ProgramT instr (Param2 exp2 pred) m (Val a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m (Val a)
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val a))
-> ProgramT instr (Param2 exp2 pred) m (Val a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val a)
forall a b. (a -> b) -> a -> b
$ FileCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a)
-> ProgramT instr (Param2 exp2 pred) m (Val a)
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (FileCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a)
 -> ProgramT instr (Param2 exp2 pred) m (Val a))
-> FileCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a)
-> ProgramT instr (Param2 exp2 pred) m (Val a)
forall a b. (a -> b) -> a -> b
$ Handle
-> FileCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a)
forall k (pred :: * -> Constraint) a (prog :: k) (exp :: * -> *).
(pred a, Formattable a) =>
Handle -> FileCMD (Param3 prog exp pred) (Val a)
FGet Handle
h

instance DryInterp FileCMD
  where
    dryInterp :: FileCMD '(m, fs) a -> m a
dryInterp (FOpen VarId
_ IOMode
_)     = (VarId -> Handle) -> m VarId -> m Handle
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM VarId -> Handle
HandleComp (m VarId -> m Handle) -> m VarId -> m Handle
forall a b. (a -> b) -> a -> b
$ VarId -> m VarId
forall (m :: * -> *). MonadSupply m => VarId -> m VarId
freshStr VarId
"h"
    dryInterp (FClose Handle
_)      = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    dryInterp (FPrintf Handle
_ VarId
_ [PrintfArg exp pred]
_) = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    dryInterp (FGet Handle
_)        = (VarId -> Val a) -> m VarId -> m (Val a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM VarId -> Val a
forall a. VarId -> Val a
ValComp (m VarId -> m (Val a)) -> m VarId -> m (Val a)
forall a b. (a -> b) -> a -> b
$ VarId -> m VarId
forall (m :: * -> *). MonadSupply m => VarId -> m VarId
freshStr VarId
"v"
    dryInterp (FEof Handle
_)        = (VarId -> Val Bool) -> m VarId -> m (Val Bool)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM VarId -> Val Bool
forall a. VarId -> Val a
ValComp (m VarId -> m (Val Bool)) -> m VarId -> m (Val Bool)
forall a b. (a -> b) -> a -> b
$ VarId -> m VarId
forall (m :: * -> *). MonadSupply m => VarId -> m VarId
freshStr VarId
"v"



--------------------------------------------------------------------------------
-- * C-specific commands
--------------------------------------------------------------------------------

-- | Pointer
newtype Ptr (a :: *) = PtrComp {Ptr a -> VarId
ptrId :: VarId}
  deriving (Ptr a -> Ptr a -> Bool
(Ptr a -> Ptr a -> Bool) -> (Ptr a -> Ptr a -> Bool) -> Eq (Ptr a)
forall a. Ptr a -> Ptr a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ptr a -> Ptr a -> Bool
$c/= :: forall a. Ptr a -> Ptr a -> Bool
== :: Ptr a -> Ptr a -> Bool
$c== :: forall a. Ptr a -> Ptr a -> Bool
Eq, Int -> Ptr a -> ShowS
[Ptr a] -> ShowS
Ptr a -> VarId
(Int -> Ptr a -> ShowS)
-> (Ptr a -> VarId) -> ([Ptr a] -> ShowS) -> Show (Ptr a)
forall a. Int -> Ptr a -> ShowS
forall a. [Ptr a] -> ShowS
forall a. Ptr a -> VarId
forall a.
(Int -> a -> ShowS) -> (a -> VarId) -> ([a] -> ShowS) -> Show a
showList :: [Ptr a] -> ShowS
$cshowList :: forall a. [Ptr a] -> ShowS
show :: Ptr a -> VarId
$cshow :: forall a. Ptr a -> VarId
showsPrec :: Int -> Ptr a -> ShowS
$cshowsPrec :: forall a. Int -> Ptr a -> ShowS
Show, Typeable)

instance ToIdent (Ptr a) where toIdent :: Ptr a -> SrcLoc -> Id
toIdent = VarId -> SrcLoc -> Id
C.Id (VarId -> SrcLoc -> Id)
-> (Ptr a -> VarId) -> Ptr a -> SrcLoc -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ptr a -> VarId
forall a. Ptr a -> VarId
ptrId

-- | Abstract object
data Object = Object
    { Object -> Bool
pointed    :: Bool
    , Object -> VarId
objectType :: String
    , Object -> VarId
objectId   :: VarId
    }
  deriving (Object -> Object -> Bool
(Object -> Object -> Bool)
-> (Object -> Object -> Bool) -> Eq Object
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Object -> Object -> Bool
$c/= :: Object -> Object -> Bool
== :: Object -> Object -> Bool
$c== :: Object -> Object -> Bool
Eq, Int -> Object -> ShowS
[Object] -> ShowS
Object -> VarId
(Int -> Object -> ShowS)
-> (Object -> VarId) -> ([Object] -> ShowS) -> Show Object
forall a.
(Int -> a -> ShowS) -> (a -> VarId) -> ([a] -> ShowS) -> Show a
showList :: [Object] -> ShowS
$cshowList :: [Object] -> ShowS
show :: Object -> VarId
$cshow :: Object -> VarId
showsPrec :: Int -> Object -> ShowS
$cshowsPrec :: Int -> Object -> ShowS
Show, Typeable)

instance ToIdent Object where toIdent :: Object -> SrcLoc -> Id
toIdent (Object Bool
_ VarId
_ VarId
o) = VarId -> SrcLoc -> Id
C.Id VarId
o

class Arg arg pred
  where
    mkArg   :: arg pred -> CGen C.Exp
    mkParam :: arg pred -> CGen C.Param

data FunArg exp pred
  where
    ValArg    :: pred a => exp a -> FunArg exp pred
    AddrArg   :: FunArg exp pred -> FunArg exp pred
    DerefArg  :: FunArg exp pred -> FunArg exp pred
    OffsetArg :: FunArg exp pred -> exp i -> FunArg exp pred
    FunArg    :: Arg arg pred => arg pred -> FunArg exp pred

instance (CompExp exp, CompTypeClass ct) => Arg (FunArg exp) ct
  where
    mkArg :: FunArg exp ct -> CGen Exp
mkArg (ValArg exp a
a) = exp a -> CGen Exp
forall (exp :: * -> *) (m :: * -> *) a.
(CompExp exp, MonadC m) =>
exp a -> m Exp
compExp exp a
a
    mkArg (AddrArg FunArg exp ct
arg) = do
        Exp
e <- FunArg exp ct -> CGen Exp
forall k (arg :: k -> *) (pred :: k).
Arg arg pred =>
arg pred -> CGen Exp
mkArg FunArg exp ct
arg
        Exp -> CGen Exp
forall (m :: * -> *) a. Monad m => a -> m a
return [cexp| &$e |]
    mkArg (DerefArg FunArg exp ct
arg) = do
        Exp
e <- FunArg exp ct -> CGen Exp
forall k (arg :: k -> *) (pred :: k).
Arg arg pred =>
arg pred -> CGen Exp
mkArg FunArg exp ct
arg
        Exp -> CGen Exp
forall (m :: * -> *) a. Monad m => a -> m a
return [cexp| *$e |]
    mkArg (OffsetArg FunArg exp ct
arg exp i
i) = do
        Exp
e  <- FunArg exp ct -> CGen Exp
forall k (arg :: k -> *) (pred :: k).
Arg arg pred =>
arg pred -> CGen Exp
mkArg FunArg exp ct
arg
        Exp
i' <- exp i -> CGen Exp
forall (exp :: * -> *) (m :: * -> *) a.
(CompExp exp, MonadC m) =>
exp a -> m Exp
compExp exp i
i
        Exp -> CGen Exp
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> CGen Exp) -> Exp -> CGen Exp
forall a b. (a -> b) -> a -> b
$ case Exp
i' of
          (C.Const (C.IntConst VarId
_ Signed
_ Integer
0 SrcLoc
_) SrcLoc
_) -> Exp
e
          (C.Const (C.IntConst VarId
_ Signed
_ Integer
c SrcLoc
_) SrcLoc
_) | Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 -> [cexp| $e - $(negate c) |]
          Exp
_ -> [cexp| $e + $i' |]
    mkArg (FunArg arg ct
a) = arg ct -> CGen Exp
forall k (arg :: k -> *) (pred :: k).
Arg arg pred =>
arg pred -> CGen Exp
mkArg arg ct
a

    mkParam :: FunArg exp ct -> CGen Param
mkParam (ValArg (exp a
a :: exp a)) = do
        Type
t <- Proxy ct -> Proxy a -> CGenT Identity Type
forall (ct :: * -> Constraint) a (m :: * -> *)
       (proxy1 :: (* -> Constraint) -> *) (proxy2 :: * -> *).
(CompTypeClass ct, ct a, MonadC m) =>
proxy1 ct -> proxy2 a -> m Type
compType (Proxy ct
forall k (t :: k). Proxy t
Proxy :: Proxy ct) (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a)
        Param -> CGen Param
forall (m :: * -> *) a. Monad m => a -> m a
return [cparam| $ty:t |]
    mkParam (AddrArg FunArg exp ct
arg) = do
      Param
p <- FunArg exp ct -> CGen Param
forall k (arg :: k -> *) (pred :: k).
Arg arg pred =>
arg pred -> CGen Param
mkParam FunArg exp ct
arg
      case Param
p of
         C.Param Maybe Id
mid DeclSpec
spec Decl
decl SrcLoc
loc -> Param -> CGen Param
forall (m :: * -> *) a. Monad m => a -> m a
return (Param -> CGen Param) -> Param -> CGen Param
forall a b. (a -> b) -> a -> b
$ Maybe Id -> DeclSpec -> Decl -> SrcLoc -> Param
C.Param Maybe Id
mid DeclSpec
spec ([TypeQual] -> Decl -> SrcLoc -> Decl
C.Ptr [] Decl
decl SrcLoc
loc) SrcLoc
loc
         Param
_ -> VarId -> CGen Param
forall a. HasCallStack => VarId -> a
error VarId
"mkParam for Addr: cannot deal with antiquotes"
    mkParam (DerefArg FunArg exp ct
arg) = do
      Param
p <- FunArg exp ct -> CGen Param
forall k (arg :: k -> *) (pred :: k).
Arg arg pred =>
arg pred -> CGen Param
mkParam FunArg exp ct
arg
      case Param
p of
         C.Param Maybe Id
mid DeclSpec
spec (C.Ptr [] Decl
decl SrcLoc
_) SrcLoc
loc -> Param -> CGen Param
forall (m :: * -> *) a. Monad m => a -> m a
return (Param -> CGen Param) -> Param -> CGen Param
forall a b. (a -> b) -> a -> b
$ Maybe Id -> DeclSpec -> Decl -> SrcLoc -> Param
C.Param Maybe Id
mid DeclSpec
spec Decl
decl SrcLoc
loc
         C.Param Maybe Id
_ DeclSpec
_ Decl
_ SrcLoc
_ -> VarId -> CGen Param
forall a. HasCallStack => VarId -> a
error VarId
"mkParam for Deref: cannot dereference non-pointer parameter"
         Param
_ -> VarId -> CGen Param
forall a. HasCallStack => VarId -> a
error VarId
"mkParam for Deref: cannot deal with antiquotes"
    mkParam (OffsetArg FunArg exp ct
a exp i
_) = FunArg exp ct -> CGen Param
forall k (arg :: k -> *) (pred :: k).
Arg arg pred =>
arg pred -> CGen Param
mkParam FunArg exp ct
a
    mkParam (FunArg arg ct
a)      = arg ct -> CGen Param
forall k (arg :: k -> *) (pred :: k).
Arg arg pred =>
arg pred -> CGen Param
mkParam arg ct
a

mapFunArg ::
    (forall a . exp1 a -> exp2 a) -> FunArg exp1 pred -> FunArg exp2 pred
mapFunArg :: (forall (a :: k). exp1 a -> exp2 a)
-> FunArg exp1 pred -> FunArg exp2 pred
mapFunArg forall (a :: k). exp1 a -> exp2 a
f (ValArg exp1 a
a)      = exp2 a -> FunArg exp2 pred
forall k (pred :: k -> Constraint) (a :: k) (exp :: k -> *).
pred a =>
exp a -> FunArg exp pred
ValArg (exp1 a -> exp2 a
forall (a :: k). exp1 a -> exp2 a
f exp1 a
a)
mapFunArg forall (a :: k). exp1 a -> exp2 a
f (AddrArg FunArg exp1 pred
a)     = FunArg exp2 pred -> FunArg exp2 pred
forall k (exp :: k -> *) (pred :: k -> Constraint).
FunArg exp pred -> FunArg exp pred
AddrArg (FunArg exp2 pred -> FunArg exp2 pred)
-> FunArg exp2 pred -> FunArg exp2 pred
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). exp1 a -> exp2 a)
-> FunArg exp1 pred -> FunArg exp2 pred
forall k (exp1 :: k -> *) (exp2 :: k -> *)
       (pred :: k -> Constraint).
(forall (a :: k). exp1 a -> exp2 a)
-> FunArg exp1 pred -> FunArg exp2 pred
mapFunArg forall (a :: k). exp1 a -> exp2 a
f FunArg exp1 pred
a
mapFunArg forall (a :: k). exp1 a -> exp2 a
f (OffsetArg FunArg exp1 pred
a exp1 i
i) = FunArg exp2 pred -> exp2 i -> FunArg exp2 pred
forall k (exp :: k -> *) (pred :: k -> Constraint) (i :: k).
FunArg exp pred -> exp i -> FunArg exp pred
OffsetArg ((forall (a :: k). exp1 a -> exp2 a)
-> FunArg exp1 pred -> FunArg exp2 pred
forall k (exp1 :: k -> *) (exp2 :: k -> *)
       (pred :: k -> Constraint).
(forall (a :: k). exp1 a -> exp2 a)
-> FunArg exp1 pred -> FunArg exp2 pred
mapFunArg forall (a :: k). exp1 a -> exp2 a
f FunArg exp1 pred
a) (exp1 i -> exp2 i
forall (a :: k). exp1 a -> exp2 a
f exp1 i
i)
mapFunArg forall (a :: k). exp1 a -> exp2 a
f (DerefArg FunArg exp1 pred
a)    = FunArg exp2 pred -> FunArg exp2 pred
forall k (exp :: k -> *) (pred :: k -> Constraint).
FunArg exp pred -> FunArg exp pred
DerefArg (FunArg exp2 pred -> FunArg exp2 pred)
-> FunArg exp2 pred -> FunArg exp2 pred
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). exp1 a -> exp2 a)
-> FunArg exp1 pred -> FunArg exp2 pred
forall k (exp1 :: k -> *) (exp2 :: k -> *)
       (pred :: k -> Constraint).
(forall (a :: k). exp1 a -> exp2 a)
-> FunArg exp1 pred -> FunArg exp2 pred
mapFunArg forall (a :: k). exp1 a -> exp2 a
f FunArg exp1 pred
a
mapFunArg forall (a :: k). exp1 a -> exp2 a
f (FunArg arg pred
a)      = arg pred -> FunArg exp2 pred
forall k (arg :: (k -> Constraint) -> *) (pred :: k -> Constraint)
       (exp :: k -> *).
Arg arg pred =>
arg pred -> FunArg exp pred
FunArg arg pred
a

mapFunArgM :: Monad m
    => (forall a . exp1 a -> m (exp2 a))
    -> FunArg exp1 pred
    -> m (FunArg exp2 pred)
mapFunArgM :: (forall (a :: k). exp1 a -> m (exp2 a))
-> FunArg exp1 pred -> m (FunArg exp2 pred)
mapFunArgM forall (a :: k). exp1 a -> m (exp2 a)
f (ValArg exp1 a
a)      = (exp2 a -> FunArg exp2 pred) -> m (exp2 a) -> m (FunArg exp2 pred)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM exp2 a -> FunArg exp2 pred
forall k (pred :: k -> Constraint) (a :: k) (exp :: k -> *).
pred a =>
exp a -> FunArg exp pred
ValArg (exp1 a -> m (exp2 a)
forall (a :: k). exp1 a -> m (exp2 a)
f exp1 a
a)
mapFunArgM forall (a :: k). exp1 a -> m (exp2 a)
f (AddrArg FunArg exp1 pred
a)     = (FunArg exp2 pred -> FunArg exp2 pred)
-> m (FunArg exp2 pred) -> m (FunArg exp2 pred)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM FunArg exp2 pred -> FunArg exp2 pred
forall k (exp :: k -> *) (pred :: k -> Constraint).
FunArg exp pred -> FunArg exp pred
AddrArg (m (FunArg exp2 pred) -> m (FunArg exp2 pred))
-> m (FunArg exp2 pred) -> m (FunArg exp2 pred)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). exp1 a -> m (exp2 a))
-> FunArg exp1 pred -> m (FunArg exp2 pred)
forall k (m :: * -> *) (exp1 :: k -> *) (exp2 :: k -> *)
       (pred :: k -> Constraint).
Monad m =>
(forall (a :: k). exp1 a -> m (exp2 a))
-> FunArg exp1 pred -> m (FunArg exp2 pred)
mapFunArgM forall (a :: k). exp1 a -> m (exp2 a)
f FunArg exp1 pred
a
mapFunArgM forall (a :: k). exp1 a -> m (exp2 a)
f (OffsetArg FunArg exp1 pred
a exp1 i
i) = do FunArg exp2 pred
a' <- (forall (a :: k). exp1 a -> m (exp2 a))
-> FunArg exp1 pred -> m (FunArg exp2 pred)
forall k (m :: * -> *) (exp1 :: k -> *) (exp2 :: k -> *)
       (pred :: k -> Constraint).
Monad m =>
(forall (a :: k). exp1 a -> m (exp2 a))
-> FunArg exp1 pred -> m (FunArg exp2 pred)
mapFunArgM forall (a :: k). exp1 a -> m (exp2 a)
f FunArg exp1 pred
a; exp2 i
i' <- exp1 i -> m (exp2 i)
forall (a :: k). exp1 a -> m (exp2 a)
f exp1 i
i; FunArg exp2 pred -> m (FunArg exp2 pred)
forall (m :: * -> *) a. Monad m => a -> m a
return (FunArg exp2 pred -> m (FunArg exp2 pred))
-> FunArg exp2 pred -> m (FunArg exp2 pred)
forall a b. (a -> b) -> a -> b
$ FunArg exp2 pred -> exp2 i -> FunArg exp2 pred
forall k (exp :: k -> *) (pred :: k -> Constraint) (i :: k).
FunArg exp pred -> exp i -> FunArg exp pred
OffsetArg FunArg exp2 pred
a' exp2 i
i'
mapFunArgM forall (a :: k). exp1 a -> m (exp2 a)
f (DerefArg FunArg exp1 pred
a)    = (FunArg exp2 pred -> FunArg exp2 pred)
-> m (FunArg exp2 pred) -> m (FunArg exp2 pred)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM FunArg exp2 pred -> FunArg exp2 pred
forall k (exp :: k -> *) (pred :: k -> Constraint).
FunArg exp pred -> FunArg exp pred
DerefArg (m (FunArg exp2 pred) -> m (FunArg exp2 pred))
-> m (FunArg exp2 pred) -> m (FunArg exp2 pred)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). exp1 a -> m (exp2 a))
-> FunArg exp1 pred -> m (FunArg exp2 pred)
forall k (m :: * -> *) (exp1 :: k -> *) (exp2 :: k -> *)
       (pred :: k -> Constraint).
Monad m =>
(forall (a :: k). exp1 a -> m (exp2 a))
-> FunArg exp1 pred -> m (FunArg exp2 pred)
mapFunArgM forall (a :: k). exp1 a -> m (exp2 a)
f FunArg exp1 pred
a
mapFunArgM forall (a :: k). exp1 a -> m (exp2 a)
f (FunArg arg pred
a)      = FunArg exp2 pred -> m (FunArg exp2 pred)
forall (m :: * -> *) a. Monad m => a -> m a
return (arg pred -> FunArg exp2 pred
forall k (arg :: (k -> Constraint) -> *) (pred :: k -> Constraint)
       (exp :: k -> *).
Arg arg pred =>
arg pred -> FunArg exp pred
FunArg arg pred
a)

class ToIdent obj => Assignable obj

instance Assignable (Ref a)
instance Assignable (Arr i a)
instance Assignable (IArr i a)
instance Assignable (Ptr a)
instance Assignable Object

data C_CMD fs a
  where
    NewCArr   :: (pred a, pred i, Integral i, Ix i) => String -> Maybe i -> exp i -> C_CMD (Param3 prog exp pred) (Arr i a)
    ConstCArr :: (pred a, pred i, Integral i, Ix i) => String -> Maybe i -> [a] -> C_CMD (Param3 prog exp pred) (Arr i a)
    NewPtr    :: pred a => String -> C_CMD (Param3 prog exp pred) (Ptr a)
    PtrToArr  :: Ptr a -> C_CMD (Param3 prog exp pred) (Arr i a)
    NewObject
        :: String  -- Base name
        -> String  -- Type
        -> Bool    -- Pointed?
        -> C_CMD (Param3 prog exp pred) Object
    AddInclude    :: String       -> C_CMD (Param3 prog exp pred) ()
    AddDefinition :: C.Definition -> C_CMD (Param3 prog exp pred) ()
    AddExternFun  :: pred res => String -> proxy res -> [FunArg exp pred] -> C_CMD (Param3 prog exp pred) ()
    AddExternProc :: String -> [FunArg exp pred] -> C_CMD (Param3 prog exp pred) ()
    CallFun       :: pred a => String -> [FunArg exp pred] -> C_CMD (Param3 prog exp pred) (Val a)
    CallProc      :: Assignable obj => Maybe obj -> String -> [FunArg exp pred] -> C_CMD (Param3 prog exp pred) ()
    InModule      :: String -> prog () -> C_CMD (Param3 prog exp pred) ()

instance HFunctor C_CMD
  where
    hfmap :: (forall b. f b -> g b) -> C_CMD '(f, fs) a -> C_CMD '(g, fs) a
hfmap forall b. f b -> g b
_ (NewCArr VarId
base Maybe i
al exp i
n)       = VarId -> Maybe i -> exp i -> C_CMD (Param3 g exp pred) (Arr i a)
forall (pred :: * -> Constraint) a i (exp :: * -> *)
       (prog :: * -> *).
(pred a, pred i, Integral i, Ix i) =>
VarId -> Maybe i -> exp i -> C_CMD (Param3 prog exp pred) (Arr i a)
NewCArr VarId
base Maybe i
al exp i
n
    hfmap forall b. f b -> g b
_ (ConstCArr VarId
base Maybe i
al [a]
as)    = VarId -> Maybe i -> [a] -> C_CMD (Param3 g exp pred) (Arr i a)
forall (pred :: * -> Constraint) a i (prog :: * -> *)
       (exp :: * -> *).
(pred a, pred i, Integral i, Ix i) =>
VarId -> Maybe i -> [a] -> C_CMD (Param3 prog exp pred) (Arr i a)
ConstCArr VarId
base Maybe i
al [a]
as
    hfmap forall b. f b -> g b
_ (NewPtr VarId
base)             = VarId -> C_CMD (Param3 g exp pred) (Ptr a)
forall (pred :: * -> Constraint) a (a :: * -> *) (prog :: * -> *).
pred a =>
VarId -> C_CMD (Param3 a prog pred) (Ptr a)
NewPtr VarId
base
    hfmap forall b. f b -> g b
_ (PtrToArr Ptr a
p)              = Ptr a -> C_CMD (Param3 g exp pred) (Arr i a)
forall a (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint)
       prog.
Ptr a -> C_CMD (Param3 prog exp pred) (Arr prog a)
PtrToArr Ptr a
p
    hfmap forall b. f b -> g b
_ (NewObject VarId
base VarId
p Bool
t)      = VarId -> VarId -> Bool -> C_CMD (Param3 g exp pred) Object
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
VarId -> VarId -> Bool -> C_CMD (Param3 prog exp pred) Object
NewObject VarId
base VarId
p Bool
t
    hfmap forall b. f b -> g b
_ (AddInclude VarId
incl)         = VarId -> C_CMD (Param3 g exp pred) ()
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
VarId -> C_CMD (Param3 prog exp pred) ()
AddInclude VarId
incl
    hfmap forall b. f b -> g b
_ (AddDefinition Definition
def)       = Definition -> C_CMD (Param3 g exp pred) ()
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
Definition -> C_CMD (Param3 prog exp pred) ()
AddDefinition Definition
def
    hfmap forall b. f b -> g b
_ (AddExternFun VarId
fun proxy res
p [FunArg exp pred]
args) = VarId
-> proxy res -> [FunArg exp pred] -> C_CMD (Param3 g exp pred) ()
forall (pred :: * -> Constraint) res (proxy :: * -> *)
       (exp :: * -> *) (pred :: * -> *).
pred res =>
VarId
-> proxy res
-> [FunArg exp pred]
-> C_CMD (Param3 pred exp pred) ()
AddExternFun VarId
fun proxy res
p [FunArg exp pred]
args
    hfmap forall b. f b -> g b
_ (AddExternProc VarId
proc [FunArg exp pred]
args) = VarId -> [FunArg exp pred] -> C_CMD (Param3 g exp pred) ()
forall (exp :: * -> *) (pred :: * -> Constraint) (prog :: * -> *).
VarId -> [FunArg exp pred] -> C_CMD (Param3 prog exp pred) ()
AddExternProc VarId
proc [FunArg exp pred]
args
    hfmap forall b. f b -> g b
_ (CallFun VarId
fun [FunArg exp pred]
args)        = VarId -> [FunArg exp pred] -> C_CMD (Param3 g exp pred) (Val a)
forall (pred :: * -> Constraint) a (obj :: * -> *) (exp :: * -> *).
pred a =>
VarId -> [FunArg obj pred] -> C_CMD (Param3 exp obj pred) (Val a)
CallFun VarId
fun [FunArg exp pred]
args
    hfmap forall b. f b -> g b
_ (CallProc Maybe obj
obj VarId
proc [FunArg exp pred]
args)  = Maybe obj
-> VarId -> [FunArg exp pred] -> C_CMD (Param3 g exp pred) ()
forall obj (exp :: * -> *) (prog :: * -> Constraint)
       (exp :: * -> *).
Assignable obj =>
Maybe obj
-> VarId -> [FunArg exp prog] -> C_CMD (Param3 exp exp prog) ()
CallProc Maybe obj
obj VarId
proc [FunArg exp pred]
args
    hfmap forall b. f b -> g b
f (InModule VarId
mod prog ()
prog)       = VarId -> g () -> C_CMD (Param3 g exp pred) ()
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
VarId -> prog () -> C_CMD (Param3 prog exp pred) ()
InModule VarId
mod (f () -> g ()
forall b. f b -> g b
f f ()
prog ()
prog)

instance HBifunctor C_CMD
  where
    hbimap :: (forall b. f b -> g b)
-> (forall b. i b -> j b)
-> C_CMD '(f, '(i, fs)) a
-> C_CMD '(g, '(j, fs)) a
hbimap forall b. f b -> g b
_ forall b. i b -> j b
f (NewCArr VarId
base Maybe i
al exp i
n)       = VarId -> Maybe i -> j i -> C_CMD (Param3 g j pred) (Arr i a)
forall (pred :: * -> Constraint) a i (exp :: * -> *)
       (prog :: * -> *).
(pred a, pred i, Integral i, Ix i) =>
VarId -> Maybe i -> exp i -> C_CMD (Param3 prog exp pred) (Arr i a)
NewCArr VarId
base Maybe i
al (i i -> j i
forall b. i b -> j b
f i i
exp i
n)
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
_ (ConstCArr VarId
base Maybe i
al [a]
as)    = VarId -> Maybe i -> [a] -> C_CMD (Param3 g j pred) (Arr i a)
forall (pred :: * -> Constraint) a i (prog :: * -> *)
       (exp :: * -> *).
(pred a, pred i, Integral i, Ix i) =>
VarId -> Maybe i -> [a] -> C_CMD (Param3 prog exp pred) (Arr i a)
ConstCArr VarId
base Maybe i
al [a]
as
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
_ (NewPtr VarId
base)             = VarId -> C_CMD (Param3 g j pred) (Ptr a)
forall (pred :: * -> Constraint) a (a :: * -> *) (prog :: * -> *).
pred a =>
VarId -> C_CMD (Param3 a prog pred) (Ptr a)
NewPtr VarId
base
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
_ (PtrToArr Ptr a
p)              = Ptr a -> C_CMD (Param3 g j pred) (Arr i a)
forall a (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint)
       prog.
Ptr a -> C_CMD (Param3 prog exp pred) (Arr prog a)
PtrToArr Ptr a
p
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
_ (NewObject VarId
base VarId
p Bool
t)      = VarId -> VarId -> Bool -> C_CMD (Param3 g j pred) Object
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
VarId -> VarId -> Bool -> C_CMD (Param3 prog exp pred) Object
NewObject VarId
base VarId
p Bool
t
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
_ (AddInclude VarId
incl)         = VarId -> C_CMD (Param3 g j pred) ()
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
VarId -> C_CMD (Param3 prog exp pred) ()
AddInclude VarId
incl
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
_ (AddDefinition Definition
def)       = Definition -> C_CMD (Param3 g j pred) ()
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
Definition -> C_CMD (Param3 prog exp pred) ()
AddDefinition Definition
def
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
f (AddExternFun VarId
fun proxy res
p [FunArg exp pred]
args) = VarId -> proxy res -> [FunArg j pred] -> C_CMD (Param3 g j pred) ()
forall (pred :: * -> Constraint) res (proxy :: * -> *)
       (exp :: * -> *) (pred :: * -> *).
pred res =>
VarId
-> proxy res
-> [FunArg exp pred]
-> C_CMD (Param3 pred exp pred) ()
AddExternFun VarId
fun proxy res
p ((FunArg exp pred -> FunArg j pred)
-> [FunArg exp pred] -> [FunArg j pred]
forall a b. (a -> b) -> [a] -> [b]
map ((forall a. exp a -> j a) -> FunArg exp pred -> FunArg j pred
forall k (exp1 :: k -> *) (exp2 :: k -> *)
       (pred :: k -> Constraint).
(forall (a :: k). exp1 a -> exp2 a)
-> FunArg exp1 pred -> FunArg exp2 pred
mapFunArg forall b. i b -> j b
forall a. exp a -> j a
f) [FunArg exp pred]
args)
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
f (AddExternProc VarId
proc [FunArg exp pred]
args) = VarId -> [FunArg j pred] -> C_CMD (Param3 g j pred) ()
forall (exp :: * -> *) (pred :: * -> Constraint) (prog :: * -> *).
VarId -> [FunArg exp pred] -> C_CMD (Param3 prog exp pred) ()
AddExternProc VarId
proc ((FunArg exp pred -> FunArg j pred)
-> [FunArg exp pred] -> [FunArg j pred]
forall a b. (a -> b) -> [a] -> [b]
map ((forall a. exp a -> j a) -> FunArg exp pred -> FunArg j pred
forall k (exp1 :: k -> *) (exp2 :: k -> *)
       (pred :: k -> Constraint).
(forall (a :: k). exp1 a -> exp2 a)
-> FunArg exp1 pred -> FunArg exp2 pred
mapFunArg forall b. i b -> j b
forall a. exp a -> j a
f) [FunArg exp pred]
args)
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
f (CallFun VarId
fun [FunArg exp pred]
args)        = VarId -> [FunArg j pred] -> C_CMD (Param3 g j pred) (Val a)
forall (pred :: * -> Constraint) a (obj :: * -> *) (exp :: * -> *).
pred a =>
VarId -> [FunArg obj pred] -> C_CMD (Param3 exp obj pred) (Val a)
CallFun VarId
fun ((FunArg exp pred -> FunArg j pred)
-> [FunArg exp pred] -> [FunArg j pred]
forall a b. (a -> b) -> [a] -> [b]
map ((forall a. exp a -> j a) -> FunArg exp pred -> FunArg j pred
forall k (exp1 :: k -> *) (exp2 :: k -> *)
       (pred :: k -> Constraint).
(forall (a :: k). exp1 a -> exp2 a)
-> FunArg exp1 pred -> FunArg exp2 pred
mapFunArg forall b. i b -> j b
forall a. exp a -> j a
f) [FunArg exp pred]
args)
    hbimap forall b. f b -> g b
_ forall b. i b -> j b
f (CallProc Maybe obj
obj VarId
proc [FunArg exp pred]
args)  = Maybe obj -> VarId -> [FunArg j pred] -> C_CMD (Param3 g j pred) ()
forall obj (exp :: * -> *) (prog :: * -> Constraint)
       (exp :: * -> *).
Assignable obj =>
Maybe obj
-> VarId -> [FunArg exp prog] -> C_CMD (Param3 exp exp prog) ()
CallProc Maybe obj
obj VarId
proc ((FunArg exp pred -> FunArg j pred)
-> [FunArg exp pred] -> [FunArg j pred]
forall a b. (a -> b) -> [a] -> [b]
map ((forall a. exp a -> j a) -> FunArg exp pred -> FunArg j pred
forall k (exp1 :: k -> *) (exp2 :: k -> *)
       (pred :: k -> Constraint).
(forall (a :: k). exp1 a -> exp2 a)
-> FunArg exp1 pred -> FunArg exp2 pred
mapFunArg forall b. i b -> j b
forall a. exp a -> j a
f) [FunArg exp pred]
args)
    hbimap forall b. f b -> g b
f forall b. i b -> j b
_ (InModule VarId
mod prog ()
prog)       = VarId -> g () -> C_CMD (Param3 g j pred) ()
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
VarId -> prog () -> C_CMD (Param3 prog exp pred) ()
InModule VarId
mod (f () -> g ()
forall b. f b -> g b
f f ()
prog ()
prog)

instance (C_CMD :<: instr) => Reexpressible C_CMD instr env
  where
    reexpressInstrEnv :: (forall b.
 exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b))
-> C_CMD
     '(ReaderT env (ProgramT instr '(exp2, fs) m), '(exp1, fs)) a
-> ReaderT env (ProgramT instr '(exp2, fs) m) a
reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (NewCArr VarId
base Maybe i
al exp i
n)       = ProgramT instr (Param2 exp2 pred) m (Arr i a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Arr i a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m (Arr i a)
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Arr i a))
-> (exp2 i -> ProgramT instr (Param2 exp2 pred) m (Arr i a))
-> exp2 i
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Arr i a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. C_CMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a)
-> ProgramT instr (Param2 exp2 pred) m (Arr i a)
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (C_CMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a)
 -> ProgramT instr (Param2 exp2 pred) m (Arr i a))
-> (exp2 i
    -> C_CMD
         '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a))
-> exp2 i
-> ProgramT instr (Param2 exp2 pred) m (Arr i a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarId
-> Maybe i
-> exp2 i
-> C_CMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a)
forall (pred :: * -> Constraint) a i (exp :: * -> *)
       (prog :: * -> *).
(pred a, pred i, Integral i, Ix i) =>
VarId -> Maybe i -> exp i -> C_CMD (Param3 prog exp pred) (Arr i a)
NewCArr VarId
base Maybe i
al (exp2 i
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Arr i a))
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (exp2 i)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Arr i a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< exp1 i -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 i)
forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp exp1 i
exp i
n
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (ConstCArr VarId
base Maybe i
al [a]
as)    = ProgramT instr (Param2 exp2 pred) m (Arr i a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Arr i a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m (Arr i a)
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Arr i a))
-> ProgramT instr (Param2 exp2 pred) m (Arr i a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Arr i a)
forall a b. (a -> b) -> a -> b
$ C_CMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a)
-> ProgramT instr (Param2 exp2 pred) m (Arr i a)
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (C_CMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a)
 -> ProgramT instr (Param2 exp2 pred) m (Arr i a))
-> C_CMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a)
-> ProgramT instr (Param2 exp2 pred) m (Arr i a)
forall a b. (a -> b) -> a -> b
$ VarId
-> Maybe i
-> [a]
-> C_CMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a)
forall (pred :: * -> Constraint) a i (prog :: * -> *)
       (exp :: * -> *).
(pred a, pred i, Integral i, Ix i) =>
VarId -> Maybe i -> [a] -> C_CMD (Param3 prog exp pred) (Arr i a)
ConstCArr VarId
base Maybe i
al [a]
as
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (NewPtr VarId
base)             = ProgramT instr (Param2 exp2 pred) m (Ptr a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Ptr a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m (Ptr a)
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Ptr a))
-> ProgramT instr (Param2 exp2 pred) m (Ptr a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Ptr a)
forall a b. (a -> b) -> a -> b
$ C_CMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Ptr a)
-> ProgramT instr (Param2 exp2 pred) m (Ptr a)
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (C_CMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Ptr a)
 -> ProgramT instr (Param2 exp2 pred) m (Ptr a))
-> C_CMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Ptr a)
-> ProgramT instr (Param2 exp2 pred) m (Ptr a)
forall a b. (a -> b) -> a -> b
$ VarId
-> C_CMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Ptr a)
forall (pred :: * -> Constraint) a (a :: * -> *) (prog :: * -> *).
pred a =>
VarId -> C_CMD (Param3 a prog pred) (Ptr a)
NewPtr VarId
base
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (PtrToArr Ptr a
p)              = ProgramT instr (Param2 exp2 pred) m (Arr i a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Arr i a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m (Arr i a)
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Arr i a))
-> ProgramT instr (Param2 exp2 pred) m (Arr i a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Arr i a)
forall a b. (a -> b) -> a -> b
$ C_CMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a)
-> ProgramT instr (Param2 exp2 pred) m (Arr i a)
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (C_CMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a)
 -> ProgramT instr (Param2 exp2 pred) m (Arr i a))
-> C_CMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a)
-> ProgramT instr (Param2 exp2 pred) m (Arr i a)
forall a b. (a -> b) -> a -> b
$ Ptr a
-> C_CMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Arr i a)
forall a (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint)
       prog.
Ptr a -> C_CMD (Param3 prog exp pred) (Arr prog a)
PtrToArr Ptr a
p
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (NewObject VarId
base VarId
p Bool
t)      = ProgramT instr (Param2 exp2 pred) m Object
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) Object
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m Object
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) Object)
-> ProgramT instr (Param2 exp2 pred) m Object
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) Object
forall a b. (a -> b) -> a -> b
$ C_CMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) Object
-> ProgramT instr (Param2 exp2 pred) m Object
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (C_CMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) Object
 -> ProgramT instr (Param2 exp2 pred) m Object)
-> C_CMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) Object
-> ProgramT instr (Param2 exp2 pred) m Object
forall a b. (a -> b) -> a -> b
$ VarId
-> VarId
-> Bool
-> C_CMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) Object
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
VarId -> VarId -> Bool -> C_CMD (Param3 prog exp pred) Object
NewObject VarId
base VarId
p Bool
t
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (AddInclude VarId
incl)         = ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m ()
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall a b. (a -> b) -> a -> b
$ C_CMD '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (C_CMD '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
 -> ProgramT instr (Param2 exp2 pred) m ())
-> C_CMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall a b. (a -> b) -> a -> b
$ VarId
-> C_CMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
VarId -> C_CMD (Param3 prog exp pred) ()
AddInclude VarId
incl
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (AddDefinition Definition
def)       = ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m ()
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall a b. (a -> b) -> a -> b
$ C_CMD '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (C_CMD '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
 -> ProgramT instr (Param2 exp2 pred) m ())
-> C_CMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall a b. (a -> b) -> a -> b
$ Definition
-> C_CMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
Definition -> C_CMD (Param3 prog exp pred) ()
AddDefinition Definition
def
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (AddExternFun VarId
fun proxy res
p [FunArg exp pred]
args) = ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m ()
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ([FunArg exp2 pred] -> ProgramT instr (Param2 exp2 pred) m ())
-> [FunArg exp2 pred]
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. C_CMD '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (C_CMD '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
 -> ProgramT instr (Param2 exp2 pred) m ())
-> ([FunArg exp2 pred]
    -> C_CMD
         '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ())
-> [FunArg exp2 pred]
-> ProgramT instr (Param2 exp2 pred) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarId
-> proxy res
-> [FunArg exp2 pred]
-> C_CMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall (pred :: * -> Constraint) res (proxy :: * -> *)
       (exp :: * -> *) (pred :: * -> *).
pred res =>
VarId
-> proxy res
-> [FunArg exp pred]
-> C_CMD (Param3 pred exp pred) ()
AddExternFun VarId
fun proxy res
p ([FunArg exp2 pred]
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ReaderT
     env (ProgramT instr (Param2 exp2 pred) m) [FunArg exp2 pred]
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (FunArg exp pred
 -> ReaderT
      env (ProgramT instr (Param2 exp2 pred) m) (FunArg exp2 pred))
-> [FunArg exp pred]
-> ReaderT
     env (ProgramT instr (Param2 exp2 pred) m) [FunArg exp2 pred]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((forall a.
 exp a
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (exp2 a))
-> FunArg exp pred
-> ReaderT
     env (ProgramT instr (Param2 exp2 pred) m) (FunArg exp2 pred)
forall k (m :: * -> *) (exp1 :: k -> *) (exp2 :: k -> *)
       (pred :: k -> Constraint).
Monad m =>
(forall (a :: k). exp1 a -> m (exp2 a))
-> FunArg exp1 pred -> m (FunArg exp2 pred)
mapFunArgM forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
forall a.
exp a -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (exp2 a)
reexp) [FunArg exp pred]
args
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (AddExternProc VarId
proc [FunArg exp pred]
args) = ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m ()
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ([FunArg exp2 pred] -> ProgramT instr (Param2 exp2 pred) m ())
-> [FunArg exp2 pred]
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. C_CMD '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (C_CMD '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
 -> ProgramT instr (Param2 exp2 pred) m ())
-> ([FunArg exp2 pred]
    -> C_CMD
         '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ())
-> [FunArg exp2 pred]
-> ProgramT instr (Param2 exp2 pred) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarId
-> [FunArg exp2 pred]
-> C_CMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall (exp :: * -> *) (pred :: * -> Constraint) (prog :: * -> *).
VarId -> [FunArg exp pred] -> C_CMD (Param3 prog exp pred) ()
AddExternProc VarId
proc ([FunArg exp2 pred]
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ReaderT
     env (ProgramT instr (Param2 exp2 pred) m) [FunArg exp2 pred]
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (FunArg exp pred
 -> ReaderT
      env (ProgramT instr (Param2 exp2 pred) m) (FunArg exp2 pred))
-> [FunArg exp pred]
-> ReaderT
     env (ProgramT instr (Param2 exp2 pred) m) [FunArg exp2 pred]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((forall a.
 exp a
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (exp2 a))
-> FunArg exp pred
-> ReaderT
     env (ProgramT instr (Param2 exp2 pred) m) (FunArg exp2 pred)
forall k (m :: * -> *) (exp1 :: k -> *) (exp2 :: k -> *)
       (pred :: k -> Constraint).
Monad m =>
(forall (a :: k). exp1 a -> m (exp2 a))
-> FunArg exp1 pred -> m (FunArg exp2 pred)
mapFunArgM forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
forall a.
exp a -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (exp2 a)
reexp) [FunArg exp pred]
args
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (CallFun VarId
fun [FunArg exp pred]
args)        = ProgramT instr (Param2 exp2 pred) m (Val a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m (Val a)
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val a))
-> ([FunArg exp2 pred]
    -> ProgramT instr (Param2 exp2 pred) m (Val a))
-> [FunArg exp2 pred]
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. C_CMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a)
-> ProgramT instr (Param2 exp2 pred) m (Val a)
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (C_CMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a)
 -> ProgramT instr (Param2 exp2 pred) m (Val a))
-> ([FunArg exp2 pred]
    -> C_CMD
         '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a))
-> [FunArg exp2 pred]
-> ProgramT instr (Param2 exp2 pred) m (Val a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarId
-> [FunArg exp2 pred]
-> C_CMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a)
forall (pred :: * -> Constraint) a (obj :: * -> *) (exp :: * -> *).
pred a =>
VarId -> [FunArg obj pred] -> C_CMD (Param3 exp obj pred) (Val a)
CallFun VarId
fun ([FunArg exp2 pred]
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val a))
-> ReaderT
     env (ProgramT instr (Param2 exp2 pred) m) [FunArg exp2 pred]
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (FunArg exp pred
 -> ReaderT
      env (ProgramT instr (Param2 exp2 pred) m) (FunArg exp2 pred))
-> [FunArg exp pred]
-> ReaderT
     env (ProgramT instr (Param2 exp2 pred) m) [FunArg exp2 pred]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((forall a.
 exp a
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (exp2 a))
-> FunArg exp pred
-> ReaderT
     env (ProgramT instr (Param2 exp2 pred) m) (FunArg exp2 pred)
forall k (m :: * -> *) (exp1 :: k -> *) (exp2 :: k -> *)
       (pred :: k -> Constraint).
Monad m =>
(forall (a :: k). exp1 a -> m (exp2 a))
-> FunArg exp1 pred -> m (FunArg exp2 pred)
mapFunArgM forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
forall a.
exp a -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (exp2 a)
reexp) [FunArg exp pred]
args
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (CallProc Maybe obj
obj VarId
proc [FunArg exp pred]
args)  = ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m ()
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ([FunArg exp2 pred] -> ProgramT instr (Param2 exp2 pred) m ())
-> [FunArg exp2 pred]
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. C_CMD '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (C_CMD '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
 -> ProgramT instr (Param2 exp2 pred) m ())
-> ([FunArg exp2 pred]
    -> C_CMD
         '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ())
-> [FunArg exp2 pred]
-> ProgramT instr (Param2 exp2 pred) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe obj
-> VarId
-> [FunArg exp2 pred]
-> C_CMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall obj (exp :: * -> *) (prog :: * -> Constraint)
       (exp :: * -> *).
Assignable obj =>
Maybe obj
-> VarId -> [FunArg exp prog] -> C_CMD (Param3 exp exp prog) ()
CallProc Maybe obj
obj VarId
proc ([FunArg exp2 pred]
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ReaderT
     env (ProgramT instr (Param2 exp2 pred) m) [FunArg exp2 pred]
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (FunArg exp pred
 -> ReaderT
      env (ProgramT instr (Param2 exp2 pred) m) (FunArg exp2 pred))
-> [FunArg exp pred]
-> ReaderT
     env (ProgramT instr (Param2 exp2 pred) m) [FunArg exp2 pred]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((forall a.
 exp a
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (exp2 a))
-> FunArg exp pred
-> ReaderT
     env (ProgramT instr (Param2 exp2 pred) m) (FunArg exp2 pred)
forall k (m :: * -> *) (exp1 :: k -> *) (exp2 :: k -> *)
       (pred :: k -> Constraint).
Monad m =>
(forall (a :: k). exp1 a -> m (exp2 a))
-> FunArg exp1 pred -> m (FunArg exp2 pred)
mapFunArgM forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
forall a.
exp a -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (exp2 a)
reexp) [FunArg exp pred]
args
    reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (InModule VarId
mod prog ()
prog)       = (env -> ProgramT instr (Param2 exp2 pred) m ())
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((env -> ProgramT instr (Param2 exp2 pred) m ())
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> (env -> ProgramT instr (Param2 exp2 pred) m ())
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall a b. (a -> b) -> a -> b
$ \env
env -> C_CMD '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (C_CMD '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
 -> ProgramT instr (Param2 exp2 pred) m ())
-> C_CMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall a b. (a -> b) -> a -> b
$ VarId
-> ProgramT instr (Param2 exp2 pred) m ()
-> C_CMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
VarId -> prog () -> C_CMD (Param3 prog exp pred) ()
InModule VarId
mod (ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
-> env -> ProgramT instr (Param2 exp2 pred) m ()
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT prog ()
ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
prog env
env)

instance DryInterp C_CMD
  where
    dryInterp :: C_CMD '(m, fs) a -> m a
dryInterp (NewCArr VarId
base Maybe i
_ exp i
_)     = (VarId -> Arr i a) -> m VarId -> m (Arr i a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM VarId -> Arr i a
forall i a. VarId -> Arr i a
ArrComp (m VarId -> m (Arr i a)) -> m VarId -> m (Arr i a)
forall a b. (a -> b) -> a -> b
$ VarId -> m VarId
forall (m :: * -> *). MonadSupply m => VarId -> m VarId
freshStr VarId
base
    dryInterp (ConstCArr VarId
base Maybe i
_ [a]
_)   = (VarId -> Arr i a) -> m VarId -> m (Arr i a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM VarId -> Arr i a
forall i a. VarId -> Arr i a
ArrComp (m VarId -> m (Arr i a)) -> m VarId -> m (Arr i a)
forall a b. (a -> b) -> a -> b
$ VarId -> m VarId
forall (m :: * -> *). MonadSupply m => VarId -> m VarId
freshStr VarId
base
    dryInterp (NewPtr VarId
base)          = (VarId -> Ptr a) -> m VarId -> m (Ptr a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM VarId -> Ptr a
forall a. VarId -> Ptr a
PtrComp (m VarId -> m (Ptr a)) -> m VarId -> m (Ptr a)
forall a b. (a -> b) -> a -> b
$ VarId -> m VarId
forall (m :: * -> *). MonadSupply m => VarId -> m VarId
freshStr VarId
base
    dryInterp (PtrToArr (PtrComp VarId
p)) = Arr i a -> m (Arr i a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Arr i a -> m (Arr i a)) -> Arr i a -> m (Arr i a)
forall a b. (a -> b) -> a -> b
$ VarId -> Arr i a
forall i a. VarId -> Arr i a
ArrComp VarId
p
    dryInterp (NewObject VarId
base VarId
t Bool
p)   = (VarId -> Object) -> m VarId -> m Object
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Bool -> VarId -> VarId -> Object
Object Bool
p VarId
t) (m VarId -> m Object) -> m VarId -> m Object
forall a b. (a -> b) -> a -> b
$ VarId -> m VarId
forall (m :: * -> *). MonadSupply m => VarId -> m VarId
freshStr VarId
base
    dryInterp (AddInclude VarId
_)         = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    dryInterp (AddDefinition Definition
_)      = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    dryInterp (AddExternFun VarId
_ proxy res
_ [FunArg exp pred]
_)   = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    dryInterp (AddExternProc VarId
_ [FunArg exp pred]
_)    = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    dryInterp (CallFun VarId
_ [FunArg exp pred]
_)          = (VarId -> Val a) -> m VarId -> m (Val a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM VarId -> Val a
forall a. VarId -> Val a
ValComp (m VarId -> m (Val a)) -> m VarId -> m (Val a)
forall a b. (a -> b) -> a -> b
$ VarId -> m VarId
forall (m :: * -> *). MonadSupply m => VarId -> m VarId
freshStr VarId
"v"
    dryInterp (CallProc Maybe obj
_ VarId
_ [FunArg exp pred]
_)       = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    dryInterp (InModule VarId
_ prog ()
_)         = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()



--------------------------------------------------------------------------------
-- * Running commands
--------------------------------------------------------------------------------

runRefCMD :: RefCMD (Param3 IO IO pred) a -> IO a
runRefCMD :: RefCMD (Param3 IO IO pred) a -> IO a
runRefCMD (NewRef VarId
_)              = (IORef a -> Ref a) -> IO (IORef a) -> IO (Ref a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap IORef a -> Ref a
forall a. IORef a -> Ref a
RefRun (IO (IORef a) -> IO (Ref a)) -> IO (IORef a) -> IO (Ref a)
forall a b. (a -> b) -> a -> b
$ a -> IO (IORef a)
forall a. a -> IO (IORef a)
newIORef (a -> IO (IORef a)) -> a -> IO (IORef a)
forall a b. (a -> b) -> a -> b
$ VarId -> a
forall a. HasCallStack => VarId -> a
error VarId
"reading uninitialized reference"
runRefCMD (InitRef VarId
_ exp a
a)           = (IORef a -> Ref a) -> IO (IORef a) -> IO (Ref a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap IORef a -> Ref a
forall a. IORef a -> Ref a
RefRun (IO (IORef a) -> IO (Ref a))
-> (a -> IO (IORef a)) -> a -> IO (Ref a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> IO (IORef a)
forall a. a -> IO (IORef a)
newIORef (a -> IO (Ref a)) -> IO a -> IO (Ref a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< exp a
IO a
a
runRefCMD (SetRef (RefRun IORef a
r) exp a
a)   = IORef a -> a -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef a
r (a -> IO ()) -> IO a -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< exp a
IO a
a
runRefCMD (GetRef (RefRun IORef a
r))     = a -> Val a
forall a. a -> Val a
ValRun (a -> Val a) -> IO a -> IO (Val a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef a -> IO a
forall a. IORef a -> IO a
readIORef IORef a
r
runRefCMD cmd :: RefCMD (Param3 IO IO pred) a
cmd@(UnsafeFreezeRef Ref a
r) = RefCMD (Param3 IO IO pred) (Val a) -> IO (Val a)
forall (pred :: * -> Constraint) a.
RefCMD (Param3 IO IO pred) a -> IO a
runRefCMD (Ref a -> RefCMD (Param3 IO IO pred) (Val a)
forall k (pred :: * -> Constraint) a (pred :: k) (a :: * -> *).
pred a =>
Ref a -> RefCMD (Param3 pred a pred) (Val a)
GetRef Ref a
r RefCMD (Param3 IO IO pred) (Val a)
-> RefCMD (Param3 IO IO pred) (Val a)
-> RefCMD (Param3 IO IO pred) (Val a)
forall a. a -> a -> a
`asTypeOf` RefCMD (Param3 IO IO pred) a
RefCMD (Param3 IO IO pred) (Val a)
cmd)

runArrCMD :: ArrCMD (Param3 IO IO pred) a -> IO a
runArrCMD :: ArrCMD (Param3 IO IO pred) a -> IO a
runArrCMD (NewArr VarId
_ exp i
n) = do
    i
n'  <- exp i
IO i
n
    IOArray i a
arr <- (i, i) -> IO (IOArray i a)
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (i
0, i -> i
forall a b. (Integral a, Num b) => a -> b
fromIntegral i
n'i -> i -> i
forall a. Num a => a -> a -> a
-i
1)
    IORef (IOArray i a) -> Arr i a
forall i a. IORef (IOArray i a) -> Arr i a
ArrRun (IORef (IOArray i a) -> Arr i a)
-> IO (IORef (IOArray i a)) -> IO (Arr i a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IOArray i a -> IO (IORef (IOArray i a))
forall a. a -> IO (IORef a)
newIORef IOArray i a
arr
runArrCMD (ConstArr VarId
_ [a]
as) =
    (IORef (IOArray i a) -> Arr i a)
-> IO (IORef (IOArray i a)) -> IO (Arr i a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap IORef (IOArray i a) -> Arr i a
forall i a. IORef (IOArray i a) -> Arr i a
ArrRun (IO (IORef (IOArray i a)) -> IO (Arr i a))
-> (IOArray i a -> IO (IORef (IOArray i a)))
-> IOArray i a
-> IO (Arr i a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IOArray i a -> IO (IORef (IOArray i a))
forall a. a -> IO (IORef a)
newIORef (IOArray i a -> IO (Arr i a)) -> IO (IOArray i a) -> IO (Arr i a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (i, i) -> [a] -> IO (IOArray i a)
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> [e] -> m (a i e)
newListArray (i
0, [a] -> i
forall i a. Num i => [a] -> i
genericLength [a]
as i -> i -> i
forall a. Num a => a -> a -> a
- i
1) [a]
as
runArrCMD (GetArr (ArrRun IORef (IOArray i a)
arr) exp i
i) = do
    IOArray i a
arr'  <- IORef (IOArray i a) -> IO (IOArray i a)
forall a. IORef a -> IO a
readIORef IORef (IOArray i a)
arr
    i
i'    <- exp i
IO i
i
    (i
l,i
h) <- IOArray i a -> IO (i, i)
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> m (i, i)
getBounds IOArray i a
arr'
    if i
i'i -> i -> Bool
forall a. Ord a => a -> a -> Bool
<i
l Bool -> Bool -> Bool
|| i
i'i -> i -> Bool
forall a. Ord a => a -> a -> Bool
>i
h
      then VarId -> IO a
forall a. HasCallStack => VarId -> a
error (VarId -> IO a) -> VarId -> IO a
forall a b. (a -> b) -> a -> b
$ VarId
"getArr: index "
                VarId -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> VarId
forall a. Show a => a -> VarId
show (i -> Integer
forall a. Integral a => a -> Integer
toInteger i
i')
                VarId -> ShowS
forall a. [a] -> [a] -> [a]
++ VarId
" out of bounds "
                VarId -> ShowS
forall a. [a] -> [a] -> [a]
++ (Integer, Integer) -> VarId
forall a. Show a => a -> VarId
show (i -> Integer
forall a. Integral a => a -> Integer
toInteger i
l, i -> Integer
forall a. Integral a => a -> Integer
toInteger i
h)
      else a -> Val a
forall a. a -> Val a
ValRun (a -> Val a) -> IO a -> IO (Val a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IOArray i a -> i -> IO a
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> m e
readArray IOArray i a
arr' i
i'
runArrCMD (SetArr (ArrRun IORef (IOArray i a)
arr) exp i
i exp a
a) = do
    IOArray i a
arr'  <- IORef (IOArray i a) -> IO (IOArray i a)
forall a. IORef a -> IO a
readIORef IORef (IOArray i a)
arr
    i
i'    <- exp i
IO i
i
    a
a'    <- exp a
IO a
a
    (i
l,i
h) <- IOArray i a -> IO (i, i)
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> m (i, i)
getBounds IOArray i a
arr'
    if i
i'i -> i -> Bool
forall a. Ord a => a -> a -> Bool
<i
l Bool -> Bool -> Bool
|| i
i'i -> i -> Bool
forall a. Ord a => a -> a -> Bool
>i
h
      then VarId -> IO a
forall a. HasCallStack => VarId -> a
error (VarId -> IO a) -> VarId -> IO a
forall a b. (a -> b) -> a -> b
$ VarId
"setArr: index "
                VarId -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> VarId
forall a. Show a => a -> VarId
show (i -> Integer
forall a. Integral a => a -> Integer
toInteger i
i')
                VarId -> ShowS
forall a. [a] -> [a] -> [a]
++ VarId
" out of bounds "
                VarId -> ShowS
forall a. [a] -> [a] -> [a]
++ (Integer, Integer) -> VarId
forall a. Show a => a -> VarId
show (i -> Integer
forall a. Integral a => a -> Integer
toInteger i
l, i -> Integer
forall a. Integral a => a -> Integer
toInteger i
h)
      else IOArray i a -> i -> a -> IO ()
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOArray i a
arr' (i -> i
forall a b. (Integral a, Num b) => a -> b
fromIntegral i
i') a
a'
runArrCMD (CopyArr (ArrRun IORef (IOArray i a)
arr1, exp i
o1) (ArrRun IORef (IOArray i a)
arr2, exp i
o2) exp i
l) = do
    IOArray i a
arr1'  <- IORef (IOArray i a) -> IO (IOArray i a)
forall a. IORef a -> IO a
readIORef IORef (IOArray i a)
arr1
    IOArray i a
arr2'  <- IORef (IOArray i a) -> IO (IOArray i a)
forall a. IORef a -> IO a
readIORef IORef (IOArray i a)
arr2
    i
o1'    <- exp i
IO i
o1
    i
o2'    <- exp i
IO i
o2
    i
l'     <- exp i
IO i
l
    (i
0,i
h1) <- IOArray i a -> IO (i, i)
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> m (i, i)
getBounds IOArray i a
arr1'
    (i
0,i
h2) <- IOArray i a -> IO (i, i)
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> m (i, i)
getBounds IOArray i a
arr2'
    let l1 :: i
l1 = i
h1i -> i -> i
forall a. Num a => a -> a -> a
+i
1i -> i -> i
forall a. Num a => a -> a -> a
-i
o1'
        l2 :: i
l2 = i
h2i -> i -> i
forall a. Num a => a -> a -> a
+i
1i -> i -> i
forall a. Num a => a -> a -> a
-i
o2'
    if i
l'i -> i -> Bool
forall a. Ord a => a -> a -> Bool
>i
l2
    then VarId -> IO a
forall a. HasCallStack => VarId -> a
error (VarId -> IO a) -> VarId -> IO a
forall a b. (a -> b) -> a -> b
$ VarId
"copyArr: cannot copy "
              VarId -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> VarId
forall a. Show a => a -> VarId
show (i -> Integer
forall a. Integral a => a -> Integer
toInteger i
l')
              VarId -> ShowS
forall a. [a] -> [a] -> [a]
++ VarId
" elements from array with "
              VarId -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> VarId
forall a. Show a => a -> VarId
show (i -> Integer
forall a. Integral a => a -> Integer
toInteger i
l2)
              VarId -> ShowS
forall a. [a] -> [a] -> [a]
++ VarId
" allocated elements"
    else if i
l'i -> i -> Bool
forall a. Ord a => a -> a -> Bool
>i
l1
    then VarId -> IO a
forall a. HasCallStack => VarId -> a
error (VarId -> IO a) -> VarId -> IO a
forall a b. (a -> b) -> a -> b
$ VarId
"copyArr: cannot copy "
              VarId -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> VarId
forall a. Show a => a -> VarId
show (i -> Integer
forall a. Integral a => a -> Integer
toInteger i
l')
              VarId -> ShowS
forall a. [a] -> [a] -> [a]
++ VarId
" elements to array with "
              VarId -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> VarId
forall a. Show a => a -> VarId
show (i -> Integer
forall a. Integral a => a -> Integer
toInteger i
l1)
              VarId -> ShowS
forall a. [a] -> [a] -> [a]
++ VarId
" allocated elements"
    else [IO ()] -> IO ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_
      [ IOArray i a -> i -> IO a
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> m e
readArray IOArray i a
arr2' (i
ii -> i -> i
forall a. Num a => a -> a -> a
+i
o2') IO a -> (a -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IOArray i a -> i -> a -> IO ()
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOArray i a
arr1' (i
ii -> i -> i
forall a. Num a => a -> a -> a
+i
o1')
          | i
i <- i -> [i] -> [i]
forall i a. Integral i => i -> [a] -> [a]
genericTake i
l' [i
0..]
      ]
runArrCMD (UnsafeFreezeArr (ArrRun IORef (IOArray i a)
arr)) =
    (Array i a -> IArr i a) -> IO (Array i a) -> IO (IArr i a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Array i a -> IArr i a
forall i a. Array i a -> IArr i a
IArrRun (IO (Array i a) -> IO (IArr i a))
-> (IOArray i a -> IO (Array i a)) -> IOArray i a -> IO (IArr i a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IOArray i a -> IO (Array i a)
forall i (a :: * -> * -> *) e (m :: * -> *) (b :: * -> * -> *).
(Ix i, MArray a e m, IArray b e) =>
a i e -> m (b i e)
freeze (IOArray i a -> IO (IArr i a)) -> IO (IOArray i a) -> IO (IArr i a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IORef (IOArray i a) -> IO (IOArray i a)
forall a. IORef a -> IO a
readIORef IORef (IOArray i a)
arr
runArrCMD (UnsafeThawArr (IArrRun Array i a
arr)) =
    (IORef (IOArray i a) -> Arr i a)
-> IO (IORef (IOArray i a)) -> IO (Arr i a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap IORef (IOArray i a) -> Arr i a
forall i a. IORef (IOArray i a) -> Arr i a
ArrRun (IO (IORef (IOArray i a)) -> IO (Arr i a))
-> (IOArray i a -> IO (IORef (IOArray i a)))
-> IOArray i a
-> IO (Arr i a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IOArray i a -> IO (IORef (IOArray i a))
forall a. a -> IO (IORef a)
newIORef (IOArray i a -> IO (Arr i a)) -> IO (IOArray i a) -> IO (Arr i a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Array i a -> IO (IOArray i a)
forall i (a :: * -> * -> *) e (b :: * -> * -> *) (m :: * -> *).
(Ix i, IArray a e, MArray b e m) =>
a i e -> m (b i e)
thaw Array i a
arr
  -- Could use `unsafeFreeze` and `unsafeThaw` here. The downside would be that
  -- incorrect use could lead to crash of the Haskell runtime (I think).

runControlCMD :: ControlCMD (Param3 IO IO pred) a -> IO a
runControlCMD :: ControlCMD (Param3 IO IO pred) a -> IO a
runControlCMD (If exp Bool
c prog ()
t prog ()
f)        = exp Bool
c exp Bool -> (Bool -> exp ()) -> exp ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Bool
c' -> if Bool
c' then exp ()
prog ()
t else exp ()
prog ()
f
runControlCMD (While prog (exp Bool)
cont prog ()
body) = prog ()
IO a
loop
  where loop :: prog ()
loop = do
          Bool
c <- prog (prog Bool) -> prog Bool
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join prog (prog Bool)
prog (exp Bool)
cont
          Bool -> prog () -> prog ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
c (prog ()
body prog () -> prog () -> prog ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> prog ()
loop)
runControlCMD (For (exp i
lo,Int
step,Border (exp i)
hi) Val i -> prog ()
body) = do
    i
lo' <- exp i
IO i
lo
    i
hi' <- Border (exp i) -> exp i
forall i. Border i -> i
borderVal Border (exp i)
hi
    i -> i -> prog ()
loop i
lo' i
hi'
  where
    incl :: Bool
incl = Border (exp i) -> Bool
forall a. Border a -> Bool
borderIncl Border (exp i)
hi
    cont :: i -> i -> Bool
cont i
i i
h
      | Bool
incl Bool -> Bool -> Bool
&& (Int
stepInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>=Int
0) = i
i i -> i -> Bool
forall a. Ord a => a -> a -> Bool
<= i
h
      | Bool
incl Bool -> Bool -> Bool
&& (Int
stepInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<Int
0)  = i
i i -> i -> Bool
forall a. Ord a => a -> a -> Bool
>= i
h
      | Int
step Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0         = i
i i -> i -> Bool
forall a. Ord a => a -> a -> Bool
<  i
h
      | Int
step Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0          = i
i i -> i -> Bool
forall a. Ord a => a -> a -> Bool
>  i
h
    loop :: i -> i -> prog ()
loop i
i i
h
      | i -> i -> Bool
cont i
i i
h  = Val i -> prog ()
body (i -> Val i
forall a. a -> Val a
ValRun i
i) prog () -> prog () -> prog ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> i -> i -> prog ()
loop (i
i i -> i -> i
forall a. Num a => a -> a -> a
+ Int -> i
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
step) i
h
      | Bool
otherwise = () -> prog ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
runControlCMD ControlCMD (Param3 IO IO pred) a
Break = VarId -> IO a
forall a. HasCallStack => VarId -> a
error VarId
"cannot run programs involving break"
runControlCMD (Assert 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

runPtrCMD :: PtrCMD (Param3 IO IO pred) a -> IO a
runPtrCMD :: PtrCMD (Param3 IO IO pred) a -> IO a
runPtrCMD (SwapPtr Ptr a
a Ptr a
b) = Ptr a -> Ptr a -> IO ()
forall a. IsPointer a => a -> a -> IO ()
runSwapPtr Ptr a
a Ptr a
b
runPtrCMD (SwapArr Arr i a
a Arr i a
b) = Arr i a -> Arr i a -> IO ()
forall a. IsPointer a => a -> a -> IO ()
runSwapPtr Arr i a
a Arr i a
b

runHandle :: Handle -> IO.Handle
runHandle :: Handle -> Handle
runHandle (HandleRun Handle
h)         = Handle
h
runHandle (HandleComp VarId
"stdin")  = Handle
IO.stdin
runHandle (HandleComp VarId
"stdout") = Handle
IO.stdout

readWord :: IO.Handle -> IO String
readWord :: Handle -> IO VarId
readWord Handle
h = do
    Bool
eof <- Handle -> IO Bool
IO.hIsEOF Handle
h
    if Bool
eof
    then VarId -> IO VarId
forall (m :: * -> *) a. Monad m => a -> m a
return VarId
""
    else do
      Char
c  <- Handle -> IO Char
IO.hGetChar Handle
h
      if Char -> Bool
isSpace Char
c
      then VarId -> IO VarId
forall (m :: * -> *) a. Monad m => a -> m a
return VarId
""
      else do
        VarId
cs <- Handle -> IO VarId
readWord Handle
h
        VarId -> IO VarId
forall (m :: * -> *) a. Monad m => a -> m a
return (Char
cChar -> ShowS
forall a. a -> [a] -> [a]
:VarId
cs)

runFPrintf :: [PrintfArg IO pred] -> (forall r . Printf.HPrintfType r => r) -> IO ()
runFPrintf :: [PrintfArg IO pred] -> (forall r. HPrintfType r => r) -> IO ()
runFPrintf []               forall r. HPrintfType r => r
pf = IO ()
forall r. HPrintfType r => r
pf
runFPrintf (PrintfArg IO a
a:[PrintfArg IO pred]
as) forall r. HPrintfType r => r
pf = IO a
a IO a -> (a -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
a' -> [PrintfArg IO pred] -> (forall r. HPrintfType r => r) -> IO ()
forall (pred :: * -> Constraint).
[PrintfArg IO pred] -> (forall r. HPrintfType r => r) -> IO ()
runFPrintf [PrintfArg IO pred]
as (a -> r
forall r. HPrintfType r => r
pf a
a')

runFileCMD :: FileCMD (Param3 IO IO pred) a -> IO a
runFileCMD :: FileCMD (Param3 IO IO pred) a -> IO a
runFileCMD (FOpen VarId
file IOMode
mode)              = Handle -> Handle
HandleRun (Handle -> Handle) -> IO Handle -> IO Handle
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VarId -> IOMode -> IO Handle
IO.openFile VarId
file IOMode
mode
runFileCMD (FClose (HandleRun Handle
h))         = Handle -> IO ()
IO.hClose Handle
h
runFileCMD (FClose (HandleComp VarId
"stdin"))  = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
runFileCMD (FClose (HandleComp VarId
"stdout")) = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
runFileCMD (FPrintf Handle
h VarId
format [PrintfArg exp pred]
as)          = [PrintfArg IO pred] -> (forall r. HPrintfType r => r) -> IO ()
forall (pred :: * -> Constraint).
[PrintfArg IO pred] -> (forall r. HPrintfType r => r) -> IO ()
runFPrintf [PrintfArg exp pred]
[PrintfArg IO pred]
as (Handle -> VarId -> r
forall r. HPrintfType r => Handle -> VarId -> r
Printf.hPrintf (Handle -> Handle
runHandle Handle
h) VarId
format)
runFileCMD (FGet Handle
h)   = do
    VarId
w <- Handle -> IO VarId
readWord (Handle -> IO VarId) -> Handle -> IO VarId
forall a b. (a -> b) -> a -> b
$ Handle -> Handle
runHandle Handle
h
    case ReadS a
forall a. Read a => ReadS a
reads VarId
w of
        [(a
f,VarId
"")] -> Val a -> IO (Val a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Val a -> IO (Val a)) -> Val a -> IO (Val a)
forall a b. (a -> b) -> a -> b
$ a -> Val a
forall a. a -> Val a
ValRun a
f
        [(a, VarId)]
_        -> VarId -> IO a
forall a. HasCallStack => VarId -> a
error (VarId -> IO a) -> VarId -> IO a
forall a b. (a -> b) -> a -> b
$ VarId
"fget: no parse (input " VarId -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> VarId
show VarId
w VarId -> ShowS
forall a. [a] -> [a] -> [a]
++ VarId
")"
runFileCMD (FEof Handle
h) = (Bool -> Val Bool) -> IO Bool -> IO (Val Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> Val Bool
forall a. a -> Val a
ValRun (IO Bool -> IO (Val Bool)) -> IO Bool -> IO (Val Bool)
forall a b. (a -> b) -> a -> b
$ Handle -> IO Bool
IO.hIsEOF (Handle -> IO Bool) -> Handle -> IO Bool
forall a b. (a -> b) -> a -> b
$ Handle -> Handle
runHandle Handle
h

runC_CMD :: forall pred a. C_CMD (Param3 IO IO pred) a -> IO a
runC_CMD :: C_CMD (Param3 IO IO pred) a -> IO a
runC_CMD (NewCArr VarId
base Maybe i
_ exp i
n)    = ArrCMD (Param3 IO IO pred) a -> IO a
forall (pred :: * -> Constraint) a.
ArrCMD (Param3 IO IO pred) a -> IO a
runArrCMD (VarId -> exp i -> ArrCMD (Param3 IO exp pred) (Arr i a)
forall k (pred :: * -> Constraint) a i (exp :: * -> *) (prog :: k).
(pred a, pred i, Integral i, Ix i) =>
VarId -> exp i -> ArrCMD (Param3 prog exp pred) (Arr i a)
NewArr VarId
base exp i
n    :: ArrCMD (Param3 IO IO pred) a)
runC_CMD (ConstCArr VarId
base Maybe i
_ [a]
as) = ArrCMD (Param3 IO IO pred) a -> IO a
forall (pred :: * -> Constraint) a.
ArrCMD (Param3 IO IO pred) a -> IO a
runArrCMD (VarId -> [a] -> ArrCMD (Param3 IO IO pred) (Arr i a)
forall k (pred :: * -> Constraint) a i (prog :: k) (exp :: * -> *).
(pred a, pred i, Integral i, Ix i) =>
VarId -> [a] -> ArrCMD (Param3 prog exp pred) (Arr i a)
ConstArr VarId
base [a]
as :: ArrCMD (Param3 IO IO pred) a)
runC_CMD (NewPtr VarId
base)         = VarId -> IO a
forall a. HasCallStack => VarId -> a
error (VarId -> IO a) -> VarId -> IO a
forall a b. (a -> b) -> a -> b
$ VarId
"cannot run programs involving newPtr (base name " VarId -> ShowS
forall a. [a] -> [a] -> [a]
++ VarId
base VarId -> ShowS
forall a. [a] -> [a] -> [a]
++ VarId
")"
runC_CMD (PtrToArr Ptr a
p)          = VarId -> IO a
forall a. HasCallStack => VarId -> a
error VarId
"cannot run programs involving ptrToArr"
runC_CMD (NewObject VarId
base VarId
_ Bool
_)  = VarId -> IO a
forall a. HasCallStack => VarId -> a
error (VarId -> IO a) -> VarId -> IO a
forall a b. (a -> b) -> a -> b
$ VarId
"cannot run programs involving newObject (base name " VarId -> ShowS
forall a. [a] -> [a] -> [a]
++ VarId
base VarId -> ShowS
forall a. [a] -> [a] -> [a]
++ VarId
")"
runC_CMD (AddInclude VarId
_)        = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
runC_CMD (AddDefinition Definition
_)     = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
runC_CMD (AddExternFun VarId
_ proxy res
_ [FunArg exp pred]
_)  = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
runC_CMD (AddExternProc VarId
_ [FunArg exp pred]
_)   = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
runC_CMD (CallFun VarId
_ [FunArg exp pred]
_)         = VarId -> IO a
forall a. HasCallStack => VarId -> a
error VarId
"cannot run programs involving callFun"
runC_CMD (CallProc Maybe obj
_ VarId
_ [FunArg exp pred]
_)      = VarId -> IO a
forall a. HasCallStack => VarId -> a
error VarId
"cannot run programs involving callProc"
runC_CMD (InModule VarId
_ prog ()
prog)     = prog ()
IO a
prog

instance InterpBi RefCMD     IO (Param1 pred) where interpBi :: RefCMD '(IO, '(IO, Param1 pred)) a -> IO a
interpBi = RefCMD '(IO, '(IO, Param1 pred)) a -> IO a
forall (pred :: * -> Constraint) a.
RefCMD (Param3 IO IO pred) a -> IO a
runRefCMD
instance InterpBi ArrCMD     IO (Param1 pred) where interpBi :: ArrCMD '(IO, '(IO, Param1 pred)) a -> IO a
interpBi = ArrCMD '(IO, '(IO, Param1 pred)) a -> IO a
forall (pred :: * -> Constraint) a.
ArrCMD (Param3 IO IO pred) a -> IO a
runArrCMD
instance InterpBi ControlCMD IO (Param1 pred) where interpBi :: ControlCMD '(IO, '(IO, Param1 pred)) a -> IO a
interpBi = ControlCMD '(IO, '(IO, Param1 pred)) a -> IO a
forall (pred :: * -> Constraint) a.
ControlCMD '(IO, '(IO, Param1 pred)) a -> IO a
runControlCMD
instance InterpBi PtrCMD     IO (Param1 pred) where interpBi :: PtrCMD '(IO, '(IO, Param1 pred)) a -> IO a
interpBi = PtrCMD '(IO, '(IO, Param1 pred)) a -> IO a
forall (pred :: * -> Constraint) a.
PtrCMD '(IO, '(IO, Param1 pred)) a -> IO a
runPtrCMD
instance InterpBi FileCMD    IO (Param1 pred) where interpBi :: FileCMD '(IO, '(IO, Param1 pred)) a -> IO a
interpBi = FileCMD '(IO, '(IO, Param1 pred)) a -> IO a
forall (pred :: * -> Constraint) a.
FileCMD '(IO, '(IO, Param1 pred)) a -> IO a
runFileCMD
instance InterpBi C_CMD      IO (Param1 pred) where interpBi :: C_CMD '(IO, '(IO, Param1 pred)) a -> IO a
interpBi = C_CMD '(IO, '(IO, Param1 pred)) a -> IO a
forall (pred :: * -> Constraint) a.
C_CMD '(IO, '(IO, Param1 pred)) a -> IO a
runC_CMD