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

-- Front end for imperative programs

module Language.Embedded.Imperative.Frontend where



import Prelude hiding (break)

import Data.Array.IO
import Data.IORef
import Data.Kind (Constraint)
import Data.Typeable
import System.IO.Unsafe

import Control.Monad.Operational.Higher
import System.IO.Fake
import Language.Embedded.Expression
import Language.Embedded.Imperative.CMD
import Language.Embedded.Imperative.Args
import Language.Embedded.Imperative.Frontend.General



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

-- | Create an uninitialized reference
newRef :: (pred a, RefCMD :<: instr) =>
    ProgramT instr (Param2 exp pred) m (Ref a)
newRef :: ProgramT instr (Param2 exp pred) m (Ref a)
newRef = String -> ProgramT instr (Param2 exp pred) m (Ref a)
forall (pred :: * -> Constraint) a
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (exp :: * -> *) (m :: * -> *).
(pred a, RefCMD :<: instr) =>
String -> ProgramT instr (Param2 exp pred) m (Ref a)
newNamedRef String
"r"

-- | Create an uninitialized named reference
--
-- The provided base name may be appended with a unique identifier to avoid name
-- collisions.
newNamedRef :: (pred a, RefCMD :<: instr)
    => String  -- ^ Base name
    -> ProgramT instr (Param2 exp pred) m (Ref a)
newNamedRef :: String -> ProgramT instr (Param2 exp pred) m (Ref a)
newNamedRef = RefCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Ref a)
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) (Ref a)
 -> ProgramT instr (Param2 exp pred) m (Ref a))
-> (String
    -> RefCMD
         '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Ref a))
-> String
-> ProgramT instr (Param2 exp pred) m (Ref a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String
-> RefCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Ref a)
forall k (pred :: * -> Constraint) a (pred :: k) (a :: * -> *).
pred a =>
String -> RefCMD (Param3 pred a pred) (Ref a)
NewRef

-- | Create an initialized reference
initRef :: (pred a, RefCMD :<: instr)
    => exp a  -- ^ Initial value
    -> ProgramT instr (Param2 exp pred) m (Ref a)
initRef :: exp a -> ProgramT instr (Param2 exp pred) m (Ref a)
initRef = String -> exp a -> ProgramT instr (Param2 exp pred) m (Ref a)
forall (pred :: * -> Constraint) a
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (exp :: * -> *) (m :: * -> *).
(pred a, RefCMD :<: instr) =>
String -> exp a -> ProgramT instr (Param2 exp pred) m (Ref a)
initNamedRef String
"r"

-- | Create an initialized named reference
--
-- The provided base name may be appended with a unique identifier to avoid name
-- collisions.
initNamedRef :: (pred a, RefCMD :<: instr)
    => String  -- ^ Base name
    -> exp a   -- ^ Initial value
    -> ProgramT instr (Param2 exp pred) m (Ref a)
initNamedRef :: String -> exp a -> ProgramT instr (Param2 exp pred) m (Ref a)
initNamedRef String
base exp a
a = RefCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Ref a)
-> ProgramT instr (Param2 exp 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 (String
-> exp a
-> RefCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Ref a)
forall k (pred :: * -> Constraint) a (pred :: * -> *) (a :: k).
pred a =>
String -> pred a -> RefCMD (Param3 a pred pred) (Ref a)
InitRef String
base exp a
a)

-- | Get the contents of a reference
getRef :: (pred a, FreeExp exp, FreePred exp a, RefCMD :<: instr, Monad m) =>
    Ref a -> ProgramT instr (Param2 exp pred) m (exp a)
getRef :: Ref a -> ProgramT instr (Param2 exp pred) m (exp a)
getRef = (Val a -> exp a)
-> ProgramT instr (Param2 exp pred) m (Val a)
-> ProgramT instr (Param2 exp pred) m (exp a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Val a -> exp a
forall (exp :: * -> *) a.
(FreeExp exp, FreePred exp a) =>
Val a -> exp a
valToExp (ProgramT instr (Param2 exp pred) m (Val a)
 -> ProgramT instr (Param2 exp pred) m (exp a))
-> (Ref a -> ProgramT instr (Param2 exp pred) m (Val a))
-> Ref a
-> ProgramT instr (Param2 exp pred) m (exp a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RefCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val a)
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) (Val a)
 -> ProgramT instr (Param2 exp pred) m (Val a))
-> (Ref a
    -> RefCMD
         '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val a))
-> Ref a
-> ProgramT instr (Param2 exp pred) m (Val a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ref a
-> RefCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val a)
forall k (pred :: * -> Constraint) a (pred :: k) (a :: * -> *).
pred a =>
Ref a -> RefCMD (Param3 pred a pred) (Val a)
GetRef

-- | Set the contents of a reference
setRef :: (pred a, RefCMD :<: instr) =>
    Ref a -> exp a -> ProgramT instr (Param2 exp pred) m ()
setRef :: Ref a -> exp a -> ProgramT instr (Param2 exp pred) m ()
setRef Ref a
r = RefCMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> (exp a
    -> RefCMD
         '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ())
-> exp a
-> ProgramT instr (Param2 exp pred) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ref a
-> exp a
-> RefCMD '(ProgramT instr (Param2 exp pred) m, Param2 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

-- | Modify the contents of reference
modifyRef :: (pred a, FreeExp exp, FreePred exp a, RefCMD :<: instr, Monad m) =>
    Ref a -> (exp a -> exp a) -> ProgramT instr (Param2 exp pred) m ()
modifyRef :: Ref a -> (exp a -> exp a) -> ProgramT instr (Param2 exp pred) m ()
modifyRef Ref a
r exp a -> exp a
f = Ref a -> exp a -> ProgramT instr (Param2 exp pred) m ()
forall (pred :: * -> Constraint) a
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (exp :: * -> *) (m :: * -> *).
(pred a, RefCMD :<: instr) =>
Ref a -> exp a -> ProgramT instr (Param2 exp pred) m ()
setRef Ref a
r (exp a -> ProgramT instr (Param2 exp pred) m ())
-> (exp a -> exp a)
-> exp a
-> ProgramT instr (Param2 exp pred) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. exp a -> exp a
f (exp a -> ProgramT instr (Param2 exp pred) m ())
-> ProgramT instr (Param2 exp pred) m (exp a)
-> ProgramT instr (Param2 exp pred) m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Ref a -> ProgramT instr (Param2 exp pred) m (exp a)
forall (pred :: * -> Constraint) a (exp :: * -> *)
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (m :: * -> *).
(pred a, FreeExp exp, FreePred exp a, RefCMD :<: instr, Monad m) =>
Ref a -> ProgramT instr (Param2 exp pred) m (exp a)
unsafeFreezeRef Ref a
r

-- | Freeze the contents of reference (only safe if the reference is not updated
-- as long as the resulting value is alive)
unsafeFreezeRef
    :: (pred a, FreeExp exp, FreePred exp a, RefCMD :<: instr, Monad m)
    => Ref a -> ProgramT instr (Param2 exp pred) m (exp a)
unsafeFreezeRef :: Ref a -> ProgramT instr (Param2 exp pred) m (exp a)
unsafeFreezeRef = (Val a -> exp a)
-> ProgramT instr (Param2 exp pred) m (Val a)
-> ProgramT instr (Param2 exp pred) m (exp a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Val a -> exp a
forall (exp :: * -> *) a.
(FreeExp exp, FreePred exp a) =>
Val a -> exp a
valToExp (ProgramT instr (Param2 exp pred) m (Val a)
 -> ProgramT instr (Param2 exp pred) m (exp a))
-> (Ref a -> ProgramT instr (Param2 exp pred) m (Val a))
-> Ref a
-> ProgramT instr (Param2 exp pred) m (exp a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RefCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val a)
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) (Val a)
 -> ProgramT instr (Param2 exp pred) m (Val a))
-> (Ref a
    -> RefCMD
         '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val a))
-> Ref a
-> ProgramT instr (Param2 exp pred) m (Val a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ref a
-> RefCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val a)
forall k (pred :: * -> Constraint) a (pred :: k) (a :: * -> *).
pred a =>
Ref a -> RefCMD (Param3 pred a pred) (Val a)
UnsafeFreezeRef

-- | Read the value of a reference without returning in the monad
--
-- WARNING: Don't use this function unless you really know what you are doing.
-- It is almost always better to use 'unsafeFreezeRef' instead.
--
-- 'veryUnsafeFreezeRef' behaves predictably when doing code generation, but it
-- can give strange results when running in 'IO', as explained here:
--
-- <http://fun-discoveries.blogspot.se/2015/09/strictness-can-fix-non-termination.html>
veryUnsafeFreezeRef :: (FreeExp exp, FreePred exp a) => Ref a -> exp a
veryUnsafeFreezeRef :: Ref a -> exp a
veryUnsafeFreezeRef (RefRun IORef a
r)  = a -> exp a
forall (exp :: * -> *) a.
(FreeExp exp, FreePred exp a) =>
a -> exp a
constExp (a -> exp a) -> a -> exp a
forall a b. (a -> b) -> a -> b
$! IO a -> a
forall a. IO a -> a
unsafePerformIO (IO a -> a) -> IO a -> a
forall a b. (a -> b) -> a -> b
$! IORef a -> IO a
forall a. IORef a -> IO a
readIORef IORef a
r
veryUnsafeFreezeRef (RefComp String
v) = String -> exp a
forall (exp :: * -> *) a.
(FreeExp exp, FreePred exp a) =>
String -> exp a
varExp String
v



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

-- | Create an uninitialized array
newArr :: (pred a, pred i, Integral i, Ix i, ArrCMD :<: instr)
    => exp i  -- ^ Length
    -> ProgramT instr (Param2 exp pred) m (Arr i a)
newArr :: exp i -> ProgramT instr (Param2 exp pred) m (Arr i a)
newArr = String -> exp i -> ProgramT instr (Param2 exp pred) m (Arr i a)
forall (pred :: * -> Constraint) a i
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (exp :: * -> *) (m :: * -> *).
(pred a, pred i, Integral i, Ix i, ArrCMD :<: instr) =>
String -> exp i -> ProgramT instr (Param2 exp pred) m (Arr i a)
newNamedArr String
"a"

-- | Create an uninitialized named array
--
-- The provided base name may be appended with a unique identifier to avoid name
-- collisions.
newNamedArr :: (pred a, pred i, Integral i, Ix i, ArrCMD :<: instr)
    => String -- ^ Base name
    -> exp i  -- ^ Length
    -> ProgramT instr (Param2 exp pred) m (Arr i a)
newNamedArr :: String -> exp i -> ProgramT instr (Param2 exp pred) m (Arr i a)
newNamedArr String
base exp i
len = ArrCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Arr i a)
-> ProgramT instr (Param2 exp 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 (String
-> exp i
-> ArrCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Arr i a)
forall k (pred :: * -> Constraint) a i (exp :: * -> *) (prog :: k).
(pred a, pred i, Integral i, Ix i) =>
String -> exp i -> ArrCMD (Param3 prog exp pred) (Arr i a)
NewArr String
base exp i
len)

-- | Create an array and initialize it with a constant list
constArr :: (pred a, pred i, Integral i, Ix i, ArrCMD :<: instr)
    => [a]  -- ^ Initial contents
    -> ProgramT instr (Param2 exp pred) m (Arr i a)
constArr :: [a] -> ProgramT instr (Param2 exp pred) m (Arr i a)
constArr = String -> [a] -> ProgramT instr (Param2 exp pred) m (Arr i a)
forall (pred :: * -> Constraint) a i
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (exp :: * -> *) (m :: * -> *).
(pred a, pred i, Integral i, Ix i, ArrCMD :<: instr) =>
String -> [a] -> ProgramT instr (Param2 exp pred) m (Arr i a)
constNamedArr String
"a"

-- | Create a named array and initialize it with a constant list
--
-- The provided base name may be appended with a unique identifier to avoid name
-- collisions.
constNamedArr :: (pred a, pred i, Integral i, Ix i, ArrCMD :<: instr)
    => String  -- ^ Base name
    -> [a]     -- ^ Initial contents
    -> ProgramT instr (Param2 exp pred) m (Arr i a)
constNamedArr :: String -> [a] -> ProgramT instr (Param2 exp pred) m (Arr i a)
constNamedArr String
base [a]
init = ArrCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Arr i a)
-> ProgramT instr (Param2 exp 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 (String
-> [a]
-> ArrCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Arr i a)
forall k (pred :: * -> Constraint) a i (prog :: k) (exp :: * -> *).
(pred a, pred i, Integral i, Ix i) =>
String -> [a] -> ArrCMD (Param3 prog exp pred) (Arr i a)
ConstArr String
base [a]
init)

-- | Get an element of an array
getArr
    :: ( pred a
       , pred i
       , FreeExp exp
       , FreePred exp a
       , Integral i
       , Ix i
       , ArrCMD :<: instr
       , Monad m
       )
    => Arr i a -> exp i -> ProgramT instr (Param2 exp pred) m (exp a)
getArr :: Arr i a -> exp i -> ProgramT instr (Param2 exp pred) m (exp a)
getArr Arr i a
arr exp i
i = (Val a -> exp a)
-> ProgramT instr (Param2 exp pred) m (Val a)
-> ProgramT instr (Param2 exp pred) m (exp a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Val a -> exp a
forall (exp :: * -> *) a.
(FreeExp exp, FreePred exp a) =>
Val a -> exp a
valToExp (ProgramT instr (Param2 exp pred) m (Val a)
 -> ProgramT instr (Param2 exp pred) m (exp a))
-> ProgramT instr (Param2 exp pred) m (Val a)
-> ProgramT instr (Param2 exp pred) m (exp a)
forall a b. (a -> b) -> a -> b
$ ArrCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val a)
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) (Val a)
 -> ProgramT instr (Param2 exp pred) m (Val a))
-> ArrCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val a)
-> ProgramT instr (Param2 exp pred) m (Val a)
forall a b. (a -> b) -> a -> b
$ Arr i a
-> exp i
-> ArrCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 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
arr exp i
i

-- | Set an element of an array
setArr :: (pred a, pred i, Integral i, Ix i, ArrCMD :<: instr) =>
    Arr i a -> exp i -> exp a -> ProgramT instr (Param2 exp pred) m ()
setArr :: Arr i a -> exp i -> exp a -> ProgramT instr (Param2 exp pred) m ()
setArr Arr i a
arr exp i
i exp a
a = ArrCMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp 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
-> exp i
-> exp a
-> ArrCMD '(ProgramT instr (Param2 exp pred) m, Param2 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
arr exp i
i exp a
a)

-- | Copy the contents of an array to another array. The number of elements to
-- copy must not be greater than the number of allocated elements in either
-- array.
copyArr :: (pred a, pred i, Integral i, Ix i, ArrCMD :<: instr)
    => (Arr i a, exp i)  -- ^ (destination,offset)
    -> (Arr i a, exp i)  -- ^ (source,offset
    -> exp i             -- ^ Number of elements
    -> ProgramT instr (Param2 exp pred) m ()
copyArr :: (Arr i a, exp i)
-> (Arr i a, exp i)
-> exp i
-> ProgramT instr (Param2 exp pred) m ()
copyArr (Arr i a, exp i)
arr1 (Arr i a, exp i)
arr2 exp i
len = ArrCMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> ArrCMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp pred) m ()
forall a b. (a -> b) -> a -> b
$ (Arr i a, exp i)
-> (Arr i a, exp i)
-> exp i
-> ArrCMD '(ProgramT instr (Param2 exp pred) m, Param2 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)
arr1 (Arr i a, exp i)
arr2 exp i
len

-- | Freeze a mutable array to an immutable one. This involves copying the array
-- to a newly allocated one.
freezeArr :: (pred a, pred i, Integral i, Ix i, Num (exp i), ArrCMD :<: instr, Monad m)
    => Arr i a
    -> exp i  -- ^ Length of new array
    -> ProgramT instr (Param2 exp pred) m (IArr i a)
freezeArr :: Arr i a -> exp i -> ProgramT instr (Param2 exp pred) m (IArr i a)
freezeArr Arr i a
arr exp i
n = do
    Arr i a
arr2 <- exp i -> ProgramT instr (Param2 exp pred) m (Arr i a)
forall (pred :: * -> Constraint) a i
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (exp :: * -> *) (m :: * -> *).
(pred a, pred i, Integral i, Ix i, ArrCMD :<: instr) =>
exp i -> ProgramT instr (Param2 exp pred) m (Arr i a)
newArr exp i
n
    (Arr i a, exp i)
-> (Arr i a, exp i)
-> exp i
-> ProgramT instr (Param2 exp pred) m ()
forall (pred :: * -> Constraint) a i
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (exp :: * -> *) (m :: * -> *).
(pred a, pred i, Integral i, Ix i, ArrCMD :<: instr) =>
(Arr i a, exp i)
-> (Arr i a, exp i)
-> exp i
-> ProgramT instr (Param2 exp pred) m ()
copyArr (Arr i a
arr2,exp i
0) (Arr i a
arr,exp i
0) exp i
n
    Arr i a -> ProgramT instr (Param2 exp pred) m (IArr i a)
forall (pred :: * -> Constraint) a i
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (exp :: * -> *) (m :: * -> *).
(pred a, pred i, Integral i, Ix i, ArrCMD :<: instr) =>
Arr i a -> ProgramT instr (Param2 exp pred) m (IArr i a)
unsafeFreezeArr Arr i a
arr2

-- | Freeze a mutable array to an immutable one without making a copy. This is
-- generally only safe if the the mutable array is not updated as long as the
-- immutable array is alive.
unsafeFreezeArr :: (pred a, pred i, Integral i, Ix i, ArrCMD :<: instr) =>
    Arr i a -> ProgramT instr (Param2 exp pred) m (IArr i a)
unsafeFreezeArr :: Arr i a -> ProgramT instr (Param2 exp pred) m (IArr i a)
unsafeFreezeArr Arr i a
arr = ArrCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (IArr i a)
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) (IArr i a)
 -> ProgramT instr (Param2 exp pred) m (IArr i a))
-> ArrCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (IArr i a)
-> ProgramT instr (Param2 exp pred) m (IArr i a)
forall a b. (a -> b) -> a -> b
$ Arr i a
-> ArrCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 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

-- | Thaw an immutable array to a mutable one. This involves copying the array
-- to a newly allocated one.
thawArr :: (pred a, pred i, Integral i, Ix i, Num (exp i), ArrCMD :<: instr, Monad m)
    => IArr i a
    -> exp i  -- ^ Number of elements to copy
    -> ProgramT instr (Param2 exp pred) m (Arr i a)
thawArr :: IArr i a -> exp i -> ProgramT instr (Param2 exp pred) m (Arr i a)
thawArr IArr i a
arr exp i
n = do
    Arr i a
arr2 <- IArr i a -> ProgramT instr (Param2 exp pred) m (Arr i a)
forall (pred :: * -> Constraint) a i
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (exp :: * -> *) (m :: * -> *).
(pred a, pred i, Integral i, Ix i, ArrCMD :<: instr) =>
IArr i a -> ProgramT instr (Param2 exp pred) m (Arr i a)
unsafeThawArr IArr i a
arr
    Arr i a
arr3 <- exp i -> ProgramT instr (Param2 exp pred) m (Arr i a)
forall (pred :: * -> Constraint) a i
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (exp :: * -> *) (m :: * -> *).
(pred a, pred i, Integral i, Ix i, ArrCMD :<: instr) =>
exp i -> ProgramT instr (Param2 exp pred) m (Arr i a)
newArr exp i
n
    (Arr i a, exp i)
-> (Arr i a, exp i)
-> exp i
-> ProgramT instr (Param2 exp pred) m ()
forall (pred :: * -> Constraint) a i
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (exp :: * -> *) (m :: * -> *).
(pred a, pred i, Integral i, Ix i, ArrCMD :<: instr) =>
(Arr i a, exp i)
-> (Arr i a, exp i)
-> exp i
-> ProgramT instr (Param2 exp pred) m ()
copyArr (Arr i a
arr3,exp i
0) (Arr i a
arr2,exp i
0) exp i
n
    Arr i a -> ProgramT instr (Param2 exp pred) m (Arr i a)
forall (m :: * -> *) a. Monad m => a -> m a
return Arr i a
arr3

-- | Thaw an immutable array to a mutable one without making a copy. This is
-- generally only safe if the the mutable array is not updated as long as the
-- immutable array is alive.
unsafeThawArr :: (pred a, pred i, Integral i, Ix i, ArrCMD :<: instr) =>
    IArr i a -> ProgramT instr (Param2 exp pred) m (Arr i a)
unsafeThawArr :: IArr i a -> ProgramT instr (Param2 exp pred) m (Arr i a)
unsafeThawArr IArr i a
arr = ArrCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Arr i a)
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) (Arr i a)
 -> ProgramT instr (Param2 exp pred) m (Arr i a))
-> ArrCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Arr i a)
-> ProgramT instr (Param2 exp pred) m (Arr i a)
forall a b. (a -> b) -> a -> b
$ IArr i a
-> ArrCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 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



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

-- | Conditional statement
iff :: (ControlCMD :<: instr)
    => exp Bool      -- ^ Condition
    -> ProgramT instr (Param2 exp pred) m ()  -- ^ True branch
    -> ProgramT instr (Param2 exp pred) m ()  -- ^ False branch
    -> ProgramT instr (Param2 exp pred) m ()
iff :: exp Bool
-> ProgramT instr (Param2 exp pred) m ()
-> ProgramT instr (Param2 exp pred) m ()
-> ProgramT instr (Param2 exp pred) m ()
iff exp Bool
b ProgramT instr (Param2 exp pred) m ()
t ProgramT instr (Param2 exp pred) m ()
f = ControlCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> ControlCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp pred) m ()
forall a b. (a -> b) -> a -> b
$ exp Bool
-> ProgramT instr (Param2 exp pred) m ()
-> ProgramT instr (Param2 exp pred) m ()
-> ControlCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall (exp :: * -> *) (prog :: * -> *) (pred :: * -> Constraint).
exp Bool
-> prog () -> prog () -> ControlCMD (Param3 prog exp pred) ()
If exp Bool
b ProgramT instr (Param2 exp pred) m ()
t ProgramT instr (Param2 exp pred) m ()
f

-- | Conditional statement that returns an expression
ifE
    :: ( pred a
       , FreeExp exp
       , FreePred exp a
       , ControlCMD :<: instr
       , RefCMD     :<: instr
       , Monad m
       )
    => exp Bool                                    -- ^ Condition
    -> ProgramT instr (Param2 exp pred) m (exp a)  -- ^ True branch
    -> ProgramT instr (Param2 exp pred) m (exp a)  -- ^ False branch
    -> ProgramT instr (Param2 exp pred) m (exp a)
ifE :: exp Bool
-> ProgramT instr (Param2 exp pred) m (exp a)
-> ProgramT instr (Param2 exp pred) m (exp a)
-> ProgramT instr (Param2 exp pred) m (exp a)
ifE exp Bool
b ProgramT instr (Param2 exp pred) m (exp a)
t ProgramT instr (Param2 exp pred) m (exp a)
f = do
    Ref a
r <- ProgramT instr (Param2 exp pred) m (Ref a)
forall (pred :: * -> Constraint) a
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (exp :: * -> *) (m :: * -> *).
(pred a, RefCMD :<: instr) =>
ProgramT instr (Param2 exp pred) m (Ref a)
newRef
    exp Bool
-> ProgramT instr (Param2 exp pred) m ()
-> ProgramT instr (Param2 exp pred) m ()
-> ProgramT instr (Param2 exp pred) m ()
forall (instr :: (* -> *, (* -> *, (* -> Constraint, *)))
                 -> * -> *)
       (exp :: * -> *) (pred :: * -> Constraint) (m :: * -> *).
(ControlCMD :<: instr) =>
exp Bool
-> ProgramT instr (Param2 exp pred) m ()
-> ProgramT instr (Param2 exp pred) m ()
-> ProgramT instr (Param2 exp pred) m ()
iff exp Bool
b (ProgramT instr (Param2 exp pred) m (exp a)
t ProgramT instr (Param2 exp pred) m (exp a)
-> (exp a -> ProgramT instr (Param2 exp pred) m ())
-> ProgramT instr (Param2 exp pred) m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Ref a -> exp a -> ProgramT instr (Param2 exp pred) m ()
forall (pred :: * -> Constraint) a
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (exp :: * -> *) (m :: * -> *).
(pred a, RefCMD :<: instr) =>
Ref a -> exp a -> ProgramT instr (Param2 exp pred) m ()
setRef Ref a
r) (ProgramT instr (Param2 exp pred) m (exp a)
f ProgramT instr (Param2 exp pred) m (exp a)
-> (exp a -> ProgramT instr (Param2 exp pred) m ())
-> ProgramT instr (Param2 exp pred) m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Ref a -> exp a -> ProgramT instr (Param2 exp pred) m ()
forall (pred :: * -> Constraint) a
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (exp :: * -> *) (m :: * -> *).
(pred a, RefCMD :<: instr) =>
Ref a -> exp a -> ProgramT instr (Param2 exp pred) m ()
setRef Ref a
r)
    Ref a -> ProgramT instr (Param2 exp pred) m (exp a)
forall (pred :: * -> Constraint) a (exp :: * -> *)
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (m :: * -> *).
(pred a, FreeExp exp, FreePred exp a, RefCMD :<: instr, Monad m) =>
Ref a -> ProgramT instr (Param2 exp pred) m (exp a)
getRef Ref a
r

-- | While loop
while :: (ControlCMD :<: instr)
    => ProgramT instr (Param2 exp pred) m (exp Bool)  -- ^ Continue condition
    -> ProgramT instr (Param2 exp pred) m ()          -- ^ Loop body
    -> ProgramT instr (Param2 exp pred) m ()
while :: ProgramT instr (Param2 exp pred) m (exp Bool)
-> ProgramT instr (Param2 exp pred) m ()
-> ProgramT instr (Param2 exp pred) m ()
while ProgramT instr (Param2 exp pred) m (exp Bool)
b ProgramT instr (Param2 exp pred) m ()
t = ControlCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> ControlCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp pred) m ()
forall a b. (a -> b) -> a -> b
$ ProgramT instr (Param2 exp pred) m (exp Bool)
-> ProgramT instr (Param2 exp pred) m ()
-> ControlCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
prog (exp Bool) -> prog () -> ControlCMD (Param3 prog exp pred) ()
While ProgramT instr (Param2 exp pred) m (exp Bool)
b ProgramT instr (Param2 exp pred) m ()
t

-- | For loop
for
    :: ( FreeExp exp
       , ControlCMD :<: instr
       , Integral n
       , pred n
       , FreePred exp n
       )
    => IxRange (exp n)                                   -- ^ Index range
    -> (exp n -> ProgramT instr (Param2 exp pred) m ())  -- ^ Loop body
    -> ProgramT instr (Param2 exp pred) m ()
for :: IxRange (exp n)
-> (exp n -> ProgramT instr (Param2 exp pred) m ())
-> ProgramT instr (Param2 exp pred) m ()
for IxRange (exp n)
range exp n -> ProgramT instr (Param2 exp pred) m ()
body = ControlCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> ControlCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp pred) m ()
forall a b. (a -> b) -> a -> b
$ IxRange (exp n)
-> (Val n -> ProgramT instr (Param2 exp pred) m ())
-> ControlCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 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 n)
range (exp n -> ProgramT instr (Param2 exp pred) m ()
body (exp n -> ProgramT instr (Param2 exp pred) m ())
-> (Val n -> exp n)
-> Val n
-> ProgramT instr (Param2 exp pred) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Val n -> exp n
forall (exp :: * -> *) a.
(FreeExp exp, FreePred exp a) =>
Val a -> exp a
valToExp)

-- | Break out from a loop
break :: (ControlCMD :<: instr) => ProgramT instr (Param2 exp pred) m ()
break :: ProgramT instr (Param2 exp pred) m ()
break = ControlCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) ()
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
ControlCMD (Param3 prog exp pred) ()
Break

-- | Assertion
assert :: (ControlCMD :<: instr)
    => exp Bool  -- ^ Expression that should be true
    -> String    -- ^ Message in case of failure
    -> ProgramT instr (Param2 exp pred) m ()
assert :: exp Bool -> String -> ProgramT instr (Param2 exp pred) m ()
assert exp Bool
cond String
msg = ControlCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> ControlCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp pred) m ()
forall a b. (a -> b) -> a -> b
$ exp Bool
-> String
-> ControlCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall (exp :: * -> *) (prog :: * -> *) (pred :: * -> Constraint).
exp Bool -> String -> ControlCMD (Param3 prog exp pred) ()
Assert exp Bool
cond String
msg

-- | Hint that an expression may be used in an invariant
hint :: (ControlCMD :<: instr, pred a)
  => exp a -- ^ Expression to be used in invariant
  -> ProgramT instr (Param2 exp pred) m ()
hint :: exp a -> ProgramT instr (Param2 exp pred) m ()
hint exp a
exp = ControlCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> ControlCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp pred) m ()
forall a b. (a -> b) -> a -> b
$ exp a
-> ControlCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall (pred :: * -> Constraint) a (exp :: * -> *)
       (prog :: * -> *).
pred a =>
exp a -> ControlCMD (Param3 prog exp pred) ()
Hint exp a
exp

--------------------------------------------------------------------------------
-- * Pointer operations
--------------------------------------------------------------------------------

-- | Swap two pointers
--
-- This is generally an unsafe operation. E.g. it can be used to make a
-- reference to a data structure escape the scope of the data.
--
-- The 'IsPointer' class ensures that the operation is only possible for types
-- that are represented as pointers in C.
unsafeSwap :: (PtrCMD :<: instr) =>
    Ptr a -> Ptr a -> ProgramT instr (Param2 exp pred) m ()
unsafeSwap :: Ptr a -> Ptr a -> ProgramT instr (Param2 exp pred) m ()
unsafeSwap Ptr a
a Ptr a
b = PtrCMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp 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 (PtrCMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> PtrCMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp pred) m ()
forall a b. (a -> b) -> a -> b
$ Ptr a
-> Ptr a
-> PtrCMD '(ProgramT instr (Param2 exp pred) m, Param2 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

unsafeSwapArr :: (Typeable i, Typeable a, pred i, pred a, PtrCMD :<: instr) =>
    Arr i a -> Arr i a -> ProgramT instr (Param2 exp pred) m ()
unsafeSwapArr :: Arr i a -> Arr i a -> ProgramT instr (Param2 exp pred) m ()
unsafeSwapArr Arr i a
a Arr i a
b = PtrCMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp 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 (PtrCMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> PtrCMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp pred) m ()
forall a b. (a -> b) -> a -> b
$ Arr i a
-> Arr i a
-> PtrCMD '(ProgramT instr (Param2 exp pred) m, Param2 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


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

-- | Open a file
fopen :: (FileCMD :<: instr) =>
    FilePath -> IOMode -> ProgramT instr (Param2 exp pred) m Handle
fopen :: String -> IOMode -> ProgramT instr (Param2 exp pred) m Handle
fopen String
file = FileCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) Handle
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) Handle
 -> ProgramT instr (Param2 exp pred) m Handle)
-> (IOMode
    -> FileCMD
         '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) Handle)
-> IOMode
-> ProgramT instr (Param2 exp pred) m Handle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String
-> IOMode
-> FileCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) Handle
forall k (prog :: k) (exp :: * -> *) (pred :: * -> Constraint).
String -> IOMode -> FileCMD (Param3 prog exp pred) Handle
FOpen String
file

-- | Close a file
fclose :: (FileCMD :<: instr) => Handle -> ProgramT instr (Param2 exp pred) m ()
fclose :: Handle -> ProgramT instr (Param2 exp pred) m ()
fclose = FileCMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> (Handle
    -> FileCMD
         '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ())
-> Handle
-> ProgramT instr (Param2 exp pred) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle
-> FileCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall k (prog :: k) (exp :: * -> *) (pred :: * -> Constraint).
Handle -> FileCMD (Param3 prog exp pred) ()
FClose

-- | Check for end of file
feof :: (FreeExp exp, FreePred exp Bool, FileCMD :<: instr, Monad m) =>
    Handle -> ProgramT instr (Param2 exp pred) m (exp Bool)
feof :: Handle -> ProgramT instr (Param2 exp pred) m (exp Bool)
feof = (Val Bool -> exp Bool)
-> ProgramT instr (Param2 exp pred) m (Val Bool)
-> ProgramT instr (Param2 exp pred) m (exp Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Val Bool -> exp Bool
forall (exp :: * -> *) a.
(FreeExp exp, FreePred exp a) =>
Val a -> exp a
valToExp (ProgramT instr (Param2 exp pred) m (Val Bool)
 -> ProgramT instr (Param2 exp pred) m (exp Bool))
-> (Handle -> ProgramT instr (Param2 exp pred) m (Val Bool))
-> Handle
-> ProgramT instr (Param2 exp pred) m (exp Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FileCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val Bool)
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) (Val Bool)
 -> ProgramT instr (Param2 exp pred) m (Val Bool))
-> (Handle
    -> FileCMD
         '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val Bool))
-> Handle
-> ProgramT instr (Param2 exp pred) m (Val Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle
-> FileCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val Bool)
forall k (prog :: k) (exp :: * -> *) (pred :: * -> Constraint).
Handle -> FileCMD (Param3 prog exp pred) (Val Bool)
FEof

class PrintfType r
  where
    type PrintfExp r :: * -> *
    type PrintfPred r :: * -> Constraint
    fprf :: Handle -> String -> [PrintfArg (PrintfExp r) (PrintfPred r)] -> r

instance (FileCMD :<: instr, a ~ ()) =>
    PrintfType (ProgramT instr (Param2 exp pred) m a)
  where
    type PrintfExp (ProgramT instr (Param2 exp pred) m a) = exp
    type PrintfPred (ProgramT instr (Param2 exp pred) m a) = pred
    fprf :: Handle
-> String
-> [PrintfArg
      (PrintfExp (ProgramT instr (Param2 exp pred) m a))
      (PrintfPred (ProgramT instr (Param2 exp pred) m a))]
-> ProgramT instr (Param2 exp pred) m a
fprf Handle
h String
form [PrintfArg
   (PrintfExp (ProgramT instr (Param2 exp pred) m a))
   (PrintfPred (ProgramT instr (Param2 exp pred) m a))]
as = FileCMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> FileCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp pred) m ()
forall a b. (a -> b) -> a -> b
$ Handle
-> String
-> [PrintfArg exp pred]
-> FileCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall k (exp :: * -> *) (pred :: * -> Constraint) (prog :: k).
Handle
-> String
-> [PrintfArg exp pred]
-> FileCMD (Param3 prog exp pred) ()
FPrintf Handle
h String
form ([PrintfArg exp pred] -> [PrintfArg exp pred]
forall a. [a] -> [a]
reverse [PrintfArg exp pred]
[PrintfArg
   (PrintfExp (ProgramT instr (Param2 exp pred) m a))
   (PrintfPred (ProgramT instr (Param2 exp pred) m a))]
as)

instance (Formattable a, PrintfType r, exp ~ PrintfExp r, PrintfPred r a) =>
    PrintfType (exp a -> r)
  where
    type PrintfExp  (exp a -> r) = exp
    type PrintfPred (exp a -> r) = PrintfPred r
    fprf :: Handle
-> String
-> [PrintfArg (PrintfExp (exp a -> r)) (PrintfPred (exp a -> r))]
-> exp a
-> r
fprf Handle
h String
form [PrintfArg (PrintfExp (exp a -> r)) (PrintfPred (exp a -> r))]
as = \exp a
a -> Handle -> String -> [PrintfArg (PrintfExp r) (PrintfPred r)] -> r
forall r.
PrintfType r =>
Handle -> String -> [PrintfArg (PrintfExp r) (PrintfPred r)] -> r
fprf Handle
h String
form (exp a -> PrintfArg exp (PrintfPred r)
forall a (pred :: * -> Constraint) (exp :: * -> *).
(PrintfArg a, pred a) =>
exp a -> PrintfArg exp pred
PrintfArg exp a
a PrintfArg exp (PrintfPred r)
-> [PrintfArg exp (PrintfPred r)] -> [PrintfArg exp (PrintfPred r)]
forall a. a -> [a] -> [a]
: [PrintfArg exp (PrintfPred r)]
[PrintfArg (PrintfExp (exp a -> r)) (PrintfPred (exp a -> r))]
as)

-- | Print to a handle. Accepts a variable number of arguments.
fprintf :: PrintfType r => Handle -> String -> r
fprintf :: Handle -> String -> r
fprintf Handle
h String
format = Handle -> String -> [PrintfArg (PrintfExp r) (PrintfPred r)] -> r
forall r.
PrintfType r =>
Handle -> String -> [PrintfArg (PrintfExp r) (PrintfPred r)] -> r
fprf Handle
h String
format []

-- | Put a single value to a handle
fput :: forall instr exp pred a m
    .  (Formattable a, FreePred exp a, FileCMD :<: instr, pred a)
    => Handle
    -> String  -- ^ Prefix
    -> exp a   -- ^ Expression to print
    -> String  -- ^ Suffix
    -> ProgramT instr (Param2 exp pred) m ()
fput :: Handle
-> String
-> exp a
-> String
-> ProgramT instr (Param2 exp pred) m ()
fput Handle
hdl String
prefix exp a
a String
suffix =
    Handle -> String -> exp a -> ProgramT instr (Param2 exp pred) m ()
forall r. PrintfType r => Handle -> String -> r
fprintf Handle
hdl (String
prefix String -> String -> String
forall a. [a] -> [a] -> [a]
++ Proxy a -> String
forall a. Formattable a => Proxy a -> String
formatSpecPrint (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
suffix) exp a
a

-- | Get a single value from a handle
fget
    :: ( Formattable a
       , pred a
       , FreeExp exp
       , FreePred exp a
       , FileCMD :<: instr
       , Monad m
       )
    => Handle -> ProgramT instr (Param2 exp pred) m (exp a)
fget :: Handle -> ProgramT instr (Param2 exp pred) m (exp a)
fget = (Val a -> exp a)
-> ProgramT instr (Param2 exp pred) m (Val a)
-> ProgramT instr (Param2 exp pred) m (exp a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Val a -> exp a
forall (exp :: * -> *) a.
(FreeExp exp, FreePred exp a) =>
Val a -> exp a
valToExp (ProgramT instr (Param2 exp pred) m (Val a)
 -> ProgramT instr (Param2 exp pred) m (exp a))
-> (Handle -> ProgramT instr (Param2 exp pred) m (Val a))
-> Handle
-> ProgramT instr (Param2 exp pred) m (exp a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FileCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val a)
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) (Val a)
 -> ProgramT instr (Param2 exp pred) m (Val a))
-> (Handle
    -> FileCMD
         '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val a))
-> Handle
-> ProgramT instr (Param2 exp pred) m (Val a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle
-> FileCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 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

-- | Print to @stdout@. Accepts a variable number of arguments.
printf :: PrintfType r => String -> r
printf :: String -> r
printf = Handle -> String -> r
forall r. PrintfType r => Handle -> String -> r
fprintf Handle
stdout



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

-- | Create a null pointer
newPtr :: (pred a, C_CMD :<: instr) => ProgramT instr (Param2 exp pred) m (Ptr a)
newPtr :: ProgramT instr (Param2 exp pred) m (Ptr a)
newPtr = String -> ProgramT instr (Param2 exp pred) m (Ptr a)
forall (pred :: * -> Constraint) a
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (exp :: * -> *) (m :: * -> *).
(pred a, C_CMD :<: instr) =>
String -> ProgramT instr (Param2 exp pred) m (Ptr a)
newNamedPtr String
"p"

-- | Create a named null pointer
--
-- The provided base name may be appended with a unique identifier to avoid name
-- collisions.
newNamedPtr :: (pred a, C_CMD :<: instr)
    => String  -- ^ Base name
    -> ProgramT instr (Param2 exp pred) m (Ptr a)
newNamedPtr :: String -> ProgramT instr (Param2 exp pred) m (Ptr a)
newNamedPtr = C_CMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Ptr a)
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) (Ptr a)
 -> ProgramT instr (Param2 exp pred) m (Ptr a))
-> (String
    -> C_CMD
         '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Ptr a))
-> String
-> ProgramT instr (Param2 exp pred) m (Ptr a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String
-> C_CMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Ptr a)
forall (pred :: * -> Constraint) a (a :: * -> *) (prog :: * -> *).
pred a =>
String -> C_CMD (Param3 a prog pred) (Ptr a)
NewPtr

-- | Cast a pointer to an array
ptrToArr :: (C_CMD :<: instr) => Ptr a -> ProgramT instr (Param2 exp pred) m (Arr i a)
ptrToArr :: Ptr a -> ProgramT instr (Param2 exp pred) m (Arr i a)
ptrToArr = C_CMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Arr i a)
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) (Arr i a)
 -> ProgramT instr (Param2 exp pred) m (Arr i a))
-> (Ptr a
    -> C_CMD
         '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Arr i a))
-> Ptr a
-> ProgramT instr (Param2 exp pred) m (Arr i a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ptr a
-> C_CMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Arr i a)
forall a (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint)
       prog.
Ptr a -> C_CMD (Param3 prog exp pred) (Arr prog a)
PtrToArr

-- | Create a pointer to an abstract object. The only thing one can do with such
-- objects is to pass them to 'callFun' or 'callProc'.
newObject :: (C_CMD :<: instr)
    => String  -- ^ Object type
    -> Bool    -- ^ Pointed?
    -> ProgramT instr (Param2 exp pred) m Object
newObject :: String -> Bool -> ProgramT instr (Param2 exp pred) m Object
newObject String
t Bool
p = String
-> String -> Bool -> ProgramT instr (Param2 exp pred) m Object
forall (instr :: (* -> *, (* -> *, (* -> Constraint, *)))
                 -> * -> *)
       (exp :: * -> *) (pred :: * -> Constraint) (m :: * -> *).
(C_CMD :<: instr) =>
String
-> String -> Bool -> ProgramT instr (Param2 exp pred) m Object
newNamedObject String
"obj" String
t Bool
p

-- | Create a pointer to a named abstract object. The only thing one can do with
-- such objects is to pass them to 'callFun' or 'callProc'.
--
-- The provided base name may be appended with a unique identifier to avoid name
-- collisions.
newNamedObject :: (C_CMD :<: instr)
    => String  -- ^ Base name
    -> String  -- ^ Object type
    -> Bool    -- ^ Pointed?
    -> ProgramT instr (Param2 exp pred) m Object
newNamedObject :: String
-> String -> Bool -> ProgramT instr (Param2 exp pred) m Object
newNamedObject String
base String
t Bool
p = C_CMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) Object
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) Object
 -> ProgramT instr (Param2 exp pred) m Object)
-> C_CMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) Object
-> ProgramT instr (Param2 exp pred) m Object
forall a b. (a -> b) -> a -> b
$ String
-> String
-> Bool
-> C_CMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) Object
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
String -> String -> Bool -> C_CMD (Param3 prog exp pred) Object
NewObject String
base String
t Bool
p

-- | Add an @#include@ statement to the generated code
addInclude :: (C_CMD :<: instr) => String -> ProgramT instr (Param2 exp pred) m ()
addInclude :: String -> ProgramT instr (Param2 exp pred) m ()
addInclude = C_CMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> (String
    -> C_CMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ())
-> String
-> ProgramT instr (Param2 exp pred) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String
-> C_CMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
String -> C_CMD (Param3 prog exp pred) ()
AddInclude

-- | Add a global definition to the generated code
--
-- Can be used conveniently as follows:
--
-- > {-# LANGUAGE QuasiQuotes #-}
-- >
-- > import Language.Embedded.Imperative
-- > import Language.C.Quote.C
-- >
-- > prog = do
-- >     ...
-- >     addDefinition myCFunction
-- >     ...
-- >   where
-- >     myCFunction = [cedecl|
-- >       void my_C_function( ... )
-- >       {
-- >           // C code
-- >           // goes here
-- >       }
-- >       |]
addDefinition :: (C_CMD :<: instr) => Definition -> ProgramT instr (Param2 exp pred) m ()
addDefinition :: Definition -> ProgramT instr (Param2 exp pred) m ()
addDefinition = C_CMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> (Definition
    -> C_CMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ())
-> Definition
-> ProgramT instr (Param2 exp pred) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition
-> C_CMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
Definition -> C_CMD (Param3 prog exp pred) ()
AddDefinition

-- | Declare an external function
addExternFun :: (pred res, C_CMD :<: instr)
    => String             -- ^ Function name
    -> proxy res          -- ^ Proxy for result type
    -> [FunArg exp pred]  -- ^ Arguments (only used to determine types)
    -> ProgramT instr (Param2 exp pred) m ()
addExternFun :: String
-> proxy res
-> [FunArg exp pred]
-> ProgramT instr (Param2 exp pred) m ()
addExternFun String
fun proxy res
res [FunArg exp pred]
args = C_CMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> C_CMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp pred) m ()
forall a b. (a -> b) -> a -> b
$ String
-> proxy res
-> [FunArg exp pred]
-> C_CMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall (pred :: * -> Constraint) res (proxy :: * -> *)
       (exp :: * -> *) (pred :: * -> *).
pred res =>
String
-> proxy res
-> [FunArg exp pred]
-> C_CMD (Param3 pred exp pred) ()
AddExternFun String
fun proxy res
res [FunArg exp pred]
args

-- | Declare an external procedure
addExternProc :: (C_CMD :<: instr)
    => String             -- ^ Procedure name
    -> [FunArg exp pred]  -- ^ Arguments (only used to determine types)
    -> ProgramT instr (Param2 exp pred) m ()
addExternProc :: String
-> [FunArg exp pred] -> ProgramT instr (Param2 exp pred) m ()
addExternProc String
proc [FunArg exp pred]
args = C_CMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> C_CMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp pred) m ()
forall a b. (a -> b) -> a -> b
$ String
-> [FunArg exp pred]
-> C_CMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall (exp :: * -> *) (pred :: * -> Constraint) (prog :: * -> *).
String -> [FunArg exp pred] -> C_CMD (Param3 prog exp pred) ()
AddExternProc String
proc [FunArg exp pred]
args

-- | Call a function
callFun :: (pred a, FreeExp exp, FreePred exp a, C_CMD :<: instr, Monad m)
    => String             -- ^ Function name
    -> [FunArg exp pred]  -- ^ Arguments
    -> ProgramT instr (Param2 exp pred) m (exp a)
callFun :: String
-> [FunArg exp pred] -> ProgramT instr (Param2 exp pred) m (exp a)
callFun String
fun [FunArg exp pred]
as = (Val a -> exp a)
-> ProgramT instr (Param2 exp pred) m (Val a)
-> ProgramT instr (Param2 exp pred) m (exp a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Val a -> exp a
forall (exp :: * -> *) a.
(FreeExp exp, FreePred exp a) =>
Val a -> exp a
valToExp (ProgramT instr (Param2 exp pred) m (Val a)
 -> ProgramT instr (Param2 exp pred) m (exp a))
-> ProgramT instr (Param2 exp pred) m (Val a)
-> ProgramT instr (Param2 exp pred) m (exp a)
forall a b. (a -> b) -> a -> b
$ C_CMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val a)
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) (Val a)
 -> ProgramT instr (Param2 exp pred) m (Val a))
-> C_CMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val a)
-> ProgramT instr (Param2 exp pred) m (Val a)
forall a b. (a -> b) -> a -> b
$ String
-> [FunArg exp pred]
-> C_CMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val a)
forall (pred :: * -> Constraint) a (obj :: * -> *) (exp :: * -> *).
pred a =>
String -> [FunArg obj pred] -> C_CMD (Param3 exp obj pred) (Val a)
CallFun String
fun [FunArg exp pred]
as

-- | Call a procedure
callProc :: (C_CMD :<: instr)
    => String             -- ^ Procedure name
    -> [FunArg exp pred]  -- ^ Arguments
    -> ProgramT instr (Param2 exp pred) m ()
callProc :: String
-> [FunArg exp pred] -> ProgramT instr (Param2 exp pred) m ()
callProc String
fun [FunArg exp pred]
as = C_CMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> C_CMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp pred) m ()
forall a b. (a -> b) -> a -> b
$ Maybe Object
-> String
-> [FunArg exp pred]
-> C_CMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall obj (exp :: * -> *) (prog :: * -> Constraint)
       (exp :: * -> *).
Assignable obj =>
Maybe obj
-> String -> [FunArg exp prog] -> C_CMD (Param3 exp exp prog) ()
CallProc (Maybe Object
forall a. Maybe a
Nothing :: Maybe Object) String
fun [FunArg exp pred]
as

-- | Call a procedure and assign its result
callProcAssign :: (Assignable obj, C_CMD :<: instr)
    => obj                -- ^ Object to which the result should be assigned
    -> String             -- ^ Procedure name
    -> [FunArg exp pred]  -- ^ Arguments
    -> ProgramT instr (Param2 exp pred) m ()
callProcAssign :: obj
-> String
-> [FunArg exp pred]
-> ProgramT instr (Param2 exp pred) m ()
callProcAssign obj
obj String
fun [FunArg exp pred]
as = C_CMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> C_CMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp pred) m ()
forall a b. (a -> b) -> a -> b
$ Maybe obj
-> String
-> [FunArg exp pred]
-> C_CMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall obj (exp :: * -> *) (prog :: * -> Constraint)
       (exp :: * -> *).
Assignable obj =>
Maybe obj
-> String -> [FunArg exp prog] -> C_CMD (Param3 exp exp prog) ()
CallProc (obj -> Maybe obj
forall a. a -> Maybe a
Just obj
obj) String
fun [FunArg exp pred]
as
  -- The reason for having both `callProc` and `callProcAssign` instead of a
  -- single one with a `Maybe obj` is that the caller would have to resolve the
  -- overloading when passing `Nothing` (as currently done in `callProc`).

-- | Declare and call an external function
externFun :: forall instr m exp pred res
    .  (pred res, FreeExp exp, FreePred exp res, C_CMD :<: instr, Monad m)
    => String             -- ^ Function name
    -> [FunArg exp pred]  -- ^ Arguments
    -> ProgramT instr (Param2 exp pred) m (exp res)
externFun :: String
-> [FunArg exp pred]
-> ProgramT instr (Param2 exp pred) m (exp res)
externFun String
fun [FunArg exp pred]
args = do
    String
-> Proxy res
-> [FunArg exp pred]
-> ProgramT instr (Param2 exp pred) m ()
forall (pred :: * -> Constraint) res
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (proxy :: * -> *) (exp :: * -> *) (m :: * -> *).
(pred res, C_CMD :<: instr) =>
String
-> proxy res
-> [FunArg exp pred]
-> ProgramT instr (Param2 exp pred) m ()
addExternFun String
fun (Proxy res
forall k (t :: k). Proxy t
Proxy :: Proxy res) [FunArg exp pred]
args
    String
-> [FunArg exp pred]
-> ProgramT instr (Param2 exp pred) m (exp res)
forall (pred :: * -> Constraint) a (exp :: * -> *)
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (m :: * -> *).
(pred a, FreeExp exp, FreePred exp a, C_CMD :<: instr, Monad m) =>
String
-> [FunArg exp pred] -> ProgramT instr (Param2 exp pred) m (exp a)
callFun String
fun [FunArg exp pred]
args

-- | Declare and call an external procedure
externProc :: (C_CMD :<: instr, Monad m)
    => String        -- ^ Procedure name
    -> [FunArg exp pred]  -- ^ Arguments
    -> ProgramT instr (Param2 exp pred) m ()
externProc :: String
-> [FunArg exp pred] -> ProgramT instr (Param2 exp pred) m ()
externProc String
proc [FunArg exp pred]
args = do
    String
-> [FunArg exp pred] -> ProgramT instr (Param2 exp pred) m ()
forall (instr :: (* -> *, (* -> *, (* -> Constraint, *)))
                 -> * -> *)
       (exp :: * -> *) (pred :: * -> Constraint) (m :: * -> *).
(C_CMD :<: instr) =>
String
-> [FunArg exp pred] -> ProgramT instr (Param2 exp pred) m ()
addExternProc String
proc [FunArg exp pred]
args
    String
-> [FunArg exp pred] -> ProgramT instr (Param2 exp pred) m ()
forall (instr :: (* -> *, (* -> *, (* -> Constraint, *)))
                 -> * -> *)
       (exp :: * -> *) (pred :: * -> Constraint) (m :: * -> *).
(C_CMD :<: instr) =>
String
-> [FunArg exp pred] -> ProgramT instr (Param2 exp pred) m ()
callProc String
proc [FunArg exp pred]
args

-- | Generate code into another translation unit
inModule :: (C_CMD :<: instr)
    => String
    -> ProgramT instr (Param2 exp pred) m ()
    -> ProgramT instr (Param2 exp pred) m ()
inModule :: String
-> ProgramT instr (Param2 exp pred) m ()
-> ProgramT instr (Param2 exp pred) m ()
inModule String
mod ProgramT instr (Param2 exp pred) m ()
prog = C_CMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> C_CMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp pred) m ()
forall a b. (a -> b) -> a -> b
$ String
-> ProgramT instr (Param2 exp pred) m ()
-> C_CMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall (prog :: * -> *) (exp :: * -> *) (pred :: * -> Constraint).
String -> prog () -> C_CMD (Param3 prog exp pred) ()
InModule String
mod ProgramT instr (Param2 exp pred) m ()
prog

-- | Get current time as number of seconds passed today
getTime
    :: (pred Double, FreeExp exp, FreePred exp Double, C_CMD :<: instr, Monad m)
    => ProgramT instr (Param2 exp pred) m (exp Double)
getTime :: ProgramT instr (Param2 exp pred) m (exp Double)
getTime = do
    String -> ProgramT instr (Param2 exp pred) m ()
forall (instr :: (* -> *, (* -> *, (* -> Constraint, *)))
                 -> * -> *)
       (exp :: * -> *) (pred :: * -> Constraint) (m :: * -> *).
(C_CMD :<: instr) =>
String -> ProgramT instr (Param2 exp pred) m ()
addInclude String
"<sys/time.h>"
    String -> ProgramT instr (Param2 exp pred) m ()
forall (instr :: (* -> *, (* -> *, (* -> Constraint, *)))
                 -> * -> *)
       (exp :: * -> *) (pred :: * -> Constraint) (m :: * -> *).
(C_CMD :<: instr) =>
String -> ProgramT instr (Param2 exp pred) m ()
addInclude String
"<sys/resource.h>"
    Definition -> ProgramT instr (Param2 exp pred) m ()
forall (instr :: (* -> *, (* -> *, (* -> Constraint, *)))
                 -> * -> *)
       (exp :: * -> *) (pred :: * -> Constraint) (m :: * -> *).
(C_CMD :<: instr) =>
Definition -> ProgramT instr (Param2 exp pred) m ()
addDefinition Definition
getTimeDef
    String
-> [FunArg exp pred]
-> ProgramT instr (Param2 exp pred) m (exp Double)
forall (pred :: * -> Constraint) a (exp :: * -> *)
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (m :: * -> *).
(pred a, FreeExp exp, FreePred exp a, C_CMD :<: instr, Monad m) =>
String
-> [FunArg exp pred] -> ProgramT instr (Param2 exp pred) m (exp a)
callFun String
"get_time" []
  where
    getTimeDef :: Definition
getTimeDef = [cedecl|
      double get_time()
      {
          struct timeval t;
          struct timezone tzp;
          gettimeofday(&t, &tzp);
          return t.tv_sec + t.tv_usec*1e-6;
      }
      |]
      -- From http://stackoverflow.com/questions/2349776/how-can-i-benchmark-c-code-easily

-- Arguments

-- | Value argument
valArg :: pred a => exp a -> FunArg exp pred
valArg :: exp a -> FunArg exp pred
valArg = exp a -> FunArg exp pred
forall k (pred :: k -> Constraint) (a :: k) (exp :: k -> *).
pred a =>
exp a -> FunArg exp pred
ValArg

-- | Reference argument
refArg :: (pred a, Arg RefArg pred) => Ref a -> FunArg exp pred
refArg :: Ref a -> FunArg exp pred
refArg = RefArg pred -> FunArg exp pred
forall k (arg :: (k -> Constraint) -> *) (pred :: k -> Constraint)
       (exp :: k -> *).
Arg arg pred =>
arg pred -> FunArg exp pred
FunArg (RefArg pred -> FunArg exp pred)
-> (Ref a -> RefArg pred) -> Ref a -> FunArg exp pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ref a -> RefArg pred
forall (pred :: * -> Constraint) a. pred a => Ref a -> RefArg pred
RefArg

-- | Mutable array argument
arrArg :: (pred a, Arg ArrArg pred) => Arr i a -> FunArg exp pred
arrArg :: Arr i a -> FunArg exp pred
arrArg = ArrArg pred -> FunArg exp pred
forall k (arg :: (k -> Constraint) -> *) (pred :: k -> Constraint)
       (exp :: k -> *).
Arg arg pred =>
arg pred -> FunArg exp pred
FunArg (ArrArg pred -> FunArg exp pred)
-> (Arr i a -> ArrArg pred) -> Arr i a -> FunArg exp pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arr i a -> ArrArg pred
forall (pred :: * -> Constraint) a i.
pred a =>
Arr i a -> ArrArg pred
ArrArg

-- | Immutable array argument
iarrArg :: (pred a, Arg IArrArg pred) => IArr i a -> FunArg exp pred
iarrArg :: IArr i a -> FunArg exp pred
iarrArg = IArrArg pred -> FunArg exp pred
forall k (arg :: (k -> Constraint) -> *) (pred :: k -> Constraint)
       (exp :: k -> *).
Arg arg pred =>
arg pred -> FunArg exp pred
FunArg (IArrArg pred -> FunArg exp pred)
-> (IArr i a -> IArrArg pred) -> IArr i a -> FunArg exp pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IArr i a -> IArrArg pred
forall (pred :: * -> Constraint) a i.
pred a =>
IArr i a -> IArrArg pred
IArrArg

-- | Pointer argument
ptrArg :: (pred a, Arg PtrArg pred) => Ptr a -> FunArg exp pred
ptrArg :: Ptr a -> FunArg exp pred
ptrArg = PtrArg pred -> FunArg exp pred
forall k (arg :: (k -> Constraint) -> *) (pred :: k -> Constraint)
       (exp :: k -> *).
Arg arg pred =>
arg pred -> FunArg exp pred
FunArg (PtrArg pred -> FunArg exp pred)
-> (Ptr a -> PtrArg pred) -> Ptr a -> FunArg exp pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ptr a -> PtrArg pred
forall (pred :: * -> Constraint) a. pred a => Ptr a -> PtrArg pred
PtrArg

-- | Abstract object argument
objArg :: Object -> FunArg exp pred
objArg :: Object -> FunArg exp pred
objArg = ObjArg pred -> FunArg exp pred
forall k (arg :: (k -> Constraint) -> *) (pred :: k -> Constraint)
       (exp :: k -> *).
Arg arg pred =>
arg pred -> FunArg exp pred
FunArg (ObjArg pred -> FunArg exp pred)
-> (Object -> ObjArg pred) -> Object -> FunArg exp pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Object -> ObjArg pred
forall k (pred :: k). Object -> ObjArg pred
ObjArg

-- | Constant string argument
strArg :: String -> FunArg exp pred
strArg :: String -> FunArg exp pred
strArg = StrArg pred -> FunArg exp pred
forall k (arg :: (k -> Constraint) -> *) (pred :: k -> Constraint)
       (exp :: k -> *).
Arg arg pred =>
arg pred -> FunArg exp pred
FunArg (StrArg pred -> FunArg exp pred)
-> (String -> StrArg pred) -> String -> FunArg exp pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> StrArg pred
forall k (pred :: k). String -> StrArg pred
StrArg

-- | Named constant argument
constArg
    :: String  -- ^ Type
    -> String  -- ^ Named constant
    -> FunArg exp pred
constArg :: String -> String -> FunArg exp pred
constArg String
t String
n = ConstArg pred -> FunArg exp pred
forall k (arg :: (k -> Constraint) -> *) (pred :: k -> Constraint)
       (exp :: k -> *).
Arg arg pred =>
arg pred -> FunArg exp pred
FunArg (ConstArg pred -> FunArg exp pred)
-> ConstArg pred -> FunArg exp pred
forall a b. (a -> b) -> a -> b
$ String -> String -> ConstArg pred
forall k (pred :: k). String -> String -> ConstArg pred
ConstArg String
t String
n

-- | Modifier that takes the address of another argument
addr :: FunArg exp pred -> FunArg exp pred
addr :: FunArg exp pred -> FunArg exp pred
addr = FunArg exp pred -> FunArg exp pred
forall k (exp :: k -> *) (pred :: k -> Constraint).
FunArg exp pred -> FunArg exp pred
AddrArg

-- | Modifier that dereferences another argument
deref :: FunArg exp pred -> FunArg exp pred
deref :: FunArg exp pred -> FunArg exp pred
deref = FunArg exp pred -> FunArg exp pred
forall k (exp :: k -> *) (pred :: k -> Constraint).
FunArg exp pred -> FunArg exp pred
DerefArg

-- | Add an offset to another argument
offset :: Integral i => FunArg exp pred -> exp i -> FunArg exp pred
offset :: FunArg exp pred -> exp i -> FunArg exp pred
offset = FunArg exp pred -> exp i -> FunArg exp pred
forall k (exp :: k -> *) (pred :: k -> Constraint) (i :: k).
FunArg exp pred -> exp i -> FunArg exp pred
OffsetArg
  -- The `Integral` constraint isn't needed, but it makes sense, since the
  -- intention of `offset` is to add an offset to a pointer.



--------------------------------------------------------------------------------
-- * Running programs
--------------------------------------------------------------------------------

-- | Run a program in 'IO'. Note that not all instructions are supported for
-- running in 'IO'. For example, calls to external C functions are not
-- supported.
runIO :: (EvalExp exp, InterpBi instr IO (Param1 pred), HBifunctor instr) =>
    Program instr (Param2 exp pred) a -> IO a
runIO :: Program instr (Param2 exp pred) a -> IO a
runIO = (forall b. exp b -> IO b)
-> Program instr (Param2 exp pred) a -> IO a
forall k (i :: (* -> *, (* -> *, k)) -> * -> *) (m :: * -> *)
       (fs :: k) (exp :: * -> *) a.
(InterpBi i m fs, HBifunctor i, Functor m, Monad m) =>
(forall b. exp b -> m b) -> Program i '(exp, fs) a -> m a
interpretBi (b -> IO b
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> IO b) -> (exp b -> b) -> exp b -> IO b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. exp b -> b
forall (exp :: * -> *) a. EvalExp exp => exp a -> a
evalExp)

-- | Like 'runIO' but with explicit input/output connected to @stdin@/@stdout@
captureIO :: (EvalExp exp, InterpBi instr IO (Param1 pred), HBifunctor instr)
    => Program instr (Param2 exp pred) a  -- ^ Program to run
    -> String                             -- ^ Input to send to @stdin@
    -> IO String                          -- ^ Result from @stdout@
captureIO :: Program instr (Param2 exp pred) a -> String -> IO String
captureIO = IO a -> String -> IO String
forall a. IO a -> String -> IO String
fakeIO (IO a -> String -> IO String)
-> (Program instr (Param2 exp pred) a -> IO a)
-> Program instr (Param2 exp pred) a
-> String
-> IO String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Program instr (Param2 exp pred) a -> IO a
forall k1 (exp :: * -> *)
       (instr :: (* -> *, (* -> *, (k1, *))) -> * -> *) (pred :: k1) a.
(EvalExp exp, InterpBi instr IO (Param1 pred), HBifunctor instr) =>
Program instr (Param2 exp pred) a -> IO a
runIO