module Feldspar.Frontend where



import Prelude (Integral, Ord, RealFloat, RealFrac)
import qualified Prelude as P
import Prelude.EDSL

import Control.Monad.Identity
import Data.Bits (Bits, FiniteBits)
import qualified Data.Bits as Bits
import Data.Complex (Complex)
import Data.Int
import Data.List (genericLength)

import Language.Syntactic (Internal)
import Language.Syntactic.Functional
import qualified Language.Syntactic as Syntactic

import qualified Control.Monad.Operational.Higher as Oper
import Language.Embedded.Imperative (IxRange)
import qualified Language.Embedded.Imperative as Imp

import qualified Data.Inhabited as Inhabited
import Data.TypedStruct
import Feldspar.Primitive.Representation
import Feldspar.Representation
import Feldspar.Sugar ()



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

----------------------------------------
-- ** General constructs
----------------------------------------

-- | Force evaluation of a value and share the result. Note that due to common
-- sub-expression elimination, this function is rarely needed in practice.
share :: (Syntax a, Syntax b)
    => a         -- ^ Value to share
    -> (a -> b)  -- ^ Body in which to share the value
    -> b
share :: a -> (a -> b) -> b
share = String -> a -> (a -> b) -> b
forall a b. (Syntax a, Syntax b) => String -> a -> (a -> b) -> b
shareTag String
""
  -- Explicit sharing can be useful e.g. when the value to share contains a
  -- function or when the code motion algorithm for some reason doesn't work
  -- find opportunities for sharing.

-- | Explicit tagged sharing
shareTag :: (Syntax a, Syntax b)
    => String    -- ^ A tag (that may be empty). May be used by a back end to
                 --   generate a sensible variable name.
    -> a         -- ^ Value to share
    -> (a -> b)  -- ^ Body in which to share the value
    -> b
shareTag :: String -> a -> (a -> b) -> b
shareTag String
tag = Let
  (Internal a :-> ((Internal a -> Internal b) :-> Full (Internal b)))
-> a -> (a -> b) -> b
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld (String
-> Let
     (Internal a :-> ((Internal a -> Internal b) :-> Full (Internal b)))
forall a b. String -> Let (a :-> ((a -> b) :-> Full b))
Let String
tag)

-- | For loop
forLoop :: Syntax st => Data Length -> st -> (Data Index -> st -> st) -> st
forLoop :: Data Length -> st -> (Data Length -> st -> st) -> st
forLoop = ForLoop
  (Length
   :-> (Internal st
        :-> ((Length -> Internal st -> Internal st)
             :-> Full (Internal st))))
-> Data Length -> st -> (Data Length -> st -> st) -> st
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld ForLoop
  (Length
   :-> (Internal st
        :-> ((Length -> Internal st -> Internal st)
             :-> Full (Internal st))))
forall st.
Type st =>
ForLoop (Length :-> (st :-> ((Length -> st -> st) :-> Full st)))
ForLoop

-- | Conditional expression
cond :: Syntax a
    => Data Bool  -- ^ Condition
    -> a          -- ^ True branch
    -> a          -- ^ False branch
    -> a
cond :: Data Bool -> a -> a -> a
cond = Primitive
  (Bool :-> (Internal a :-> (Internal a :-> Full (Internal a))))
-> Data Bool -> a -> a -> a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive
  (Bool :-> (Internal a :-> (Internal a :-> Full (Internal a))))
forall a. Primitive (Bool :-> (a :-> (a :-> Full a)))
Cond

-- | Condition operator; use as follows:
--
-- @
-- cond1 `?` a $
-- cond2 `?` b $
-- cond3 `?` c $
--         default
-- @
(?) :: Syntax a
    => Data Bool  -- ^ Condition
    -> a          -- ^ True branch
    -> a          -- ^ False branch
    -> a
? :: Data Bool -> a -> a -> a
(?) = Data Bool -> a -> a -> a
forall a. Syntax a => Data Bool -> a -> a -> a
cond

infixl 1 ?

-- | Multi-way conditional expression
--
-- The first association @(a,b)@ in the list of cases for which @a@ is equal to
-- the scrutinee is selected, and the associated @b@ is returned as the result.
-- If no case matches, the default value is returned.
switch :: (Syntax a, Syntax b, PrimType (Internal a))
    => b        -- ^ Default result
    -> [(a,b)]  -- ^ Cases (match, result)
    -> a        -- ^ Scrutinee
    -> b        -- ^ Result
switch :: b -> [(a, b)] -> a -> b
switch b
def [] a
_ = b
def
switch b
def [(a, b)]
cs a
s = ((a, b) -> b -> b) -> b -> [(a, b)] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
P.foldr
    (\(a
c,b
a) b
b -> a -> Data (Internal a)
forall a. Syntax a => a -> Data (Internal a)
desugar a
c Data (Internal a) -> Data (Internal a) -> Data Bool
forall a. PrimType a => Data a -> Data a -> Data Bool
== a -> Data (Internal a)
forall a. Syntax a => a -> Data (Internal a)
desugar a
s Data Bool -> b -> b -> b
forall a. Syntax a => Data Bool -> a -> a -> a
? b
a (b -> b) -> b -> b
forall a b. (a -> b) -> a -> b
$ b
b)
    b
def
    [(a, b)]
cs



----------------------------------------
-- ** Literals
----------------------------------------

-- | Literal
value :: Syntax a => Internal a -> a
value :: Internal a -> a
value = Primitive (Full (Internal a)) -> a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld (Primitive (Full (Internal a)) -> a)
-> (Internal a -> Primitive (Full (Internal a))) -> Internal a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Internal a -> Primitive (Full (Internal a))
forall a. (Eq a, Show a) => a -> Primitive (Full a)
Lit

false :: Data Bool
false :: Data Bool
false = Internal (Data Bool) -> Data Bool
forall a. Syntax a => Internal a -> a
value Bool
Internal (Data Bool)
False

true :: Data Bool
true :: Data Bool
true = Internal (Data Bool) -> Data Bool
forall a. Syntax a => Internal a -> a
value Bool
Internal (Data Bool)
True

instance Syntactic.Syntactic ()
  where
    type Domain ()   = FeldDomain
    type Internal () = Int32
    desugar :: () -> ASTF (Domain ()) (Internal ())
desugar () = Data Int32 -> ASTF FeldDomain Int32
forall a. Data a -> ASTF FeldDomain a
unData Data Int32
0
    sugar :: ASTF (Domain ()) (Internal ()) -> ()
sugar   ASTF (Domain ()) (Internal ())
_  = ()

-- | Example value
--
-- 'example' can be used similarly to 'undefined' in normal Haskell, i.e. to
-- create an expression whose value is irrelevant.
--
-- Note that it is generally not possible to use 'undefined' in Feldspar
-- expressions, as this will crash the compiler.
example :: Syntax a => a
example :: a
example = Internal a -> a
forall a. Syntax a => Internal a -> a
value Internal a
forall a. Inhabited a => a
Inhabited.example



----------------------------------------
-- ** Primitive functions
----------------------------------------

instance (Bounded a, Type a) => Bounded (Data a)
  where
    minBound :: Data a
minBound = Internal (Data a) -> Data a
forall a. Syntax a => Internal a -> a
value Internal (Data a)
forall a. Bounded a => a
minBound
    maxBound :: Data a
maxBound = Internal (Data a) -> Data a
forall a. Syntax a => Internal a -> a
value Internal (Data a)
forall a. Bounded a => a
maxBound

instance (Num a, PrimType a) => Num (Data a)
  where
    fromInteger :: Integer -> Data a
fromInteger = a -> Data a
forall a. Syntax a => Internal a -> a
value (a -> Data a) -> (Integer -> a) -> Integer -> Data a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> a
forall a. Num a => Integer -> a
fromInteger
    + :: Data a -> Data a -> Data a
(+)         = Primitive (a :-> (a :-> Full a)) -> Data a -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> (a :-> Full a))
forall a. (Num a, PrimType' a) => Primitive (a :-> (a :-> Full a))
Add
    (-)         = Primitive (a :-> (a :-> Full a)) -> Data a -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> (a :-> Full a))
forall a. (Num a, PrimType' a) => Primitive (a :-> (a :-> Full a))
Sub
    * :: Data a -> Data a -> Data a
(*)         = Primitive (a :-> (a :-> Full a)) -> Data a -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> (a :-> Full a))
forall a. (Num a, PrimType' a) => Primitive (a :-> (a :-> Full a))
Mul
    negate :: Data a -> Data a
negate      = Primitive (a :-> Full a) -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> Full a)
forall a. (Num a, PrimType' a) => Primitive (a :-> Full a)
Neg
    abs :: Data a -> Data a
abs         = Primitive (a :-> Full a) -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> Full a)
forall a. (Num a, PrimType' a) => Primitive (a :-> Full a)
Abs
    signum :: Data a -> Data a
signum      = Primitive (a :-> Full a) -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> Full a)
forall a. (Num a, PrimType' a) => Primitive (a :-> Full a)
Sign

instance (Fractional a, PrimType a) => Fractional (Data a)
  where
    fromRational :: Rational -> Data a
fromRational = a -> Data a
forall a. Syntax a => Internal a -> a
value (a -> Data a) -> (Rational -> a) -> Rational -> Data a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> a
forall a. Fractional a => Rational -> a
fromRational
    / :: Data a -> Data a -> Data a
(/) = Primitive (a :-> (a :-> Full a)) -> Data a -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> (a :-> Full a))
forall a.
(Fractional a, PrimType' a) =>
Primitive (a :-> (a :-> Full a))
FDiv

instance (Floating a, PrimType a) => Floating (Data a)
  where
    pi :: Data a
pi    = Primitive (Full a) -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (Full a)
forall a. (Floating a, PrimType' a) => Primitive (Full a)
Pi
    exp :: Data a -> Data a
exp   = Primitive (a :-> Full a) -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> Full a)
forall a. (Floating a, PrimType' a) => Primitive (a :-> Full a)
Exp
    log :: Data a -> Data a
log   = Primitive (a :-> Full a) -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> Full a)
forall a. (Floating a, PrimType' a) => Primitive (a :-> Full a)
Log
    sqrt :: Data a -> Data a
sqrt  = Primitive (a :-> Full a) -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> Full a)
forall a. (Floating a, PrimType' a) => Primitive (a :-> Full a)
Sqrt
    ** :: Data a -> Data a -> Data a
(**)  = Primitive (a :-> (a :-> Full a)) -> Data a -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> (a :-> Full a))
forall a.
(Floating a, PrimType' a) =>
Primitive (a :-> (a :-> Full a))
Pow
    sin :: Data a -> Data a
sin   = Primitive (a :-> Full a) -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> Full a)
forall a. (Floating a, PrimType' a) => Primitive (a :-> Full a)
Sin
    cos :: Data a -> Data a
cos   = Primitive (a :-> Full a) -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> Full a)
forall a. (Floating a, PrimType' a) => Primitive (a :-> Full a)
Cos
    tan :: Data a -> Data a
tan   = Primitive (a :-> Full a) -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> Full a)
forall a. (Floating a, PrimType' a) => Primitive (a :-> Full a)
Tan
    asin :: Data a -> Data a
asin  = Primitive (a :-> Full a) -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> Full a)
forall a. (Floating a, PrimType' a) => Primitive (a :-> Full a)
Asin
    acos :: Data a -> Data a
acos  = Primitive (a :-> Full a) -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> Full a)
forall a. (Floating a, PrimType' a) => Primitive (a :-> Full a)
Acos
    atan :: Data a -> Data a
atan  = Primitive (a :-> Full a) -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> Full a)
forall a. (Floating a, PrimType' a) => Primitive (a :-> Full a)
Atan
    sinh :: Data a -> Data a
sinh  = Primitive (a :-> Full a) -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> Full a)
forall a. (Floating a, PrimType' a) => Primitive (a :-> Full a)
Sinh
    cosh :: Data a -> Data a
cosh  = Primitive (a :-> Full a) -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> Full a)
forall a. (Floating a, PrimType' a) => Primitive (a :-> Full a)
Cosh
    tanh :: Data a -> Data a
tanh  = Primitive (a :-> Full a) -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> Full a)
forall a. (Floating a, PrimType' a) => Primitive (a :-> Full a)
Tanh
    asinh :: Data a -> Data a
asinh = Primitive (a :-> Full a) -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> Full a)
forall a. (Floating a, PrimType' a) => Primitive (a :-> Full a)
Asinh
    acosh :: Data a -> Data a
acosh = Primitive (a :-> Full a) -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> Full a)
forall a. (Floating a, PrimType' a) => Primitive (a :-> Full a)
Acosh
    atanh :: Data a -> Data a
atanh = Primitive (a :-> Full a) -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> Full a)
forall a. (Floating a, PrimType' a) => Primitive (a :-> Full a)
Atanh

-- | Alias for 'pi'
π :: (Floating a, PrimType a) => Data a
π :: Data a
π = Data a
forall a. Floating a => a
pi

-- | Integer division truncated toward zero
quot :: (Integral a, PrimType a) => Data a -> Data a -> Data a
quot :: Data a -> Data a -> Data a
quot = Primitive (a :-> (a :-> Full a)) -> Data a -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> (a :-> Full a))
forall a.
(Integral a, PrimType' a) =>
Primitive (a :-> (a :-> Full a))
Quot

-- | Integer remainder satisfying
--
-- > (x `quot` y)*y + (x `rem` y) == x
rem :: (Integral a, PrimType a) => Data a -> Data a -> Data a
rem :: Data a -> Data a -> Data a
rem = Primitive (a :-> (a :-> Full a)) -> Data a -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> (a :-> Full a))
forall a.
(Integral a, PrimType' a) =>
Primitive (a :-> (a :-> Full a))
Rem

-- | Simultaneous @quot@ and @rem@
quotRem :: (Integral a, PrimType a) => Data a -> Data a -> (Data a, Data a)
quotRem :: Data a -> Data a -> (Data a, Data a)
quotRem Data a
a Data a
b = (Data a
q,Data a
r)
  where
    q :: Data a
q = Data a -> Data a -> Data a
forall a. (Integral a, PrimType a) => Data a -> Data a -> Data a
quot Data a
a Data a
b
    r :: Data a
r = Data a
a Data a -> Data a -> Data a
forall a. Num a => a -> a -> a
- Data a
b Data a -> Data a -> Data a
forall a. Num a => a -> a -> a
* Data a
q

-- | Integer division truncated toward negative infinity
div :: (Integral a, PrimType a) => Data a -> Data a -> Data a
div :: Data a -> Data a -> Data a
div = Primitive (a :-> (a :-> Full a)) -> Data a -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> (a :-> Full a))
forall a.
(Integral a, PrimType' a) =>
Primitive (a :-> (a :-> Full a))
Div

-- | Integer modulus, satisfying
--
-- > (x `div` y)*y + (x `mod` y) == x
mod :: (Integral a, PrimType a) => Data a -> Data a -> Data a
mod :: Data a -> Data a -> Data a
mod = Primitive (a :-> (a :-> Full a)) -> Data a -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> (a :-> Full a))
forall a.
(Integral a, PrimType' a) =>
Primitive (a :-> (a :-> Full a))
Mod

-- | Integer division assuming `unsafeBalancedDiv x y * y == x` (i.e. no
-- remainder)
--
-- The advantage of using 'unsafeBalancedDiv' over 'quot' or 'div' is that the
-- above assumption can be used for simplifying the expression.
unsafeBalancedDiv :: (Integral a, PrimType a) => Data a -> Data a -> Data a
unsafeBalancedDiv :: Data a -> Data a -> Data a
unsafeBalancedDiv Data a
a Data a
b = AssertionLabel -> Data Bool -> String -> Data a -> Data a
forall a.
Syntax a =>
AssertionLabel -> Data Bool -> String -> a -> a
guardValLabel
    AssertionLabel
InternalAssertion
    (Data a -> Data a -> Data a
forall a. (Integral a, PrimType a) => Data a -> Data a -> Data a
rem Data a
a Data a
b Data a -> Data a -> Data Bool
forall a. PrimType a => Data a -> Data a -> Data Bool
== Data a
0)
    String
"unsafeBalancedDiv: division not balanced"
    (ExtraPrimitive (a :-> (a :-> Full a)) -> Data a -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld ExtraPrimitive (a :-> (a :-> Full a))
forall a.
(Integral a, PrimType' a) =>
ExtraPrimitive (a :-> (a :-> Full a))
DivBalanced Data a
a Data a
b)
  -- Note: We can't check that `result * b == a`, because `result * b` gets
  -- simplified to `a`.

-- | Construct a complex number
complex :: (Num a, PrimType a, PrimType (Complex a))
    => Data a  -- ^ Real part
    -> Data a  -- ^ Imaginary part
    -> Data (Complex a)
complex :: Data a -> Data a -> Data (Complex a)
complex = Primitive (a :-> (a :-> Full (Complex a)))
-> Data a -> Data a -> Data (Complex a)
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> (a :-> Full (Complex a)))
forall a.
(Num a, PrimType' a, PrimType' (Complex a)) =>
Primitive (a :-> (a :-> Full (Complex a)))
Complex

-- | Construct a complex number
polar :: (Floating a, PrimType a, PrimType (Complex a))
    => Data a  -- ^ Magnitude
    -> Data a  -- ^ Phase
    -> Data (Complex a)
polar :: Data a -> Data a -> Data (Complex a)
polar = Primitive (a :-> (a :-> Full (Complex a)))
-> Data a -> Data a -> Data (Complex a)
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> (a :-> Full (Complex a)))
forall a.
(Floating a, PrimType' a, PrimType' (Complex a)) =>
Primitive (a :-> (a :-> Full (Complex a)))
Polar

-- | Extract the real part of a complex number
realPart :: (PrimType a, PrimType (Complex a)) => Data (Complex a) -> Data a
realPart :: Data (Complex a) -> Data a
realPart = Primitive (Complex a :-> Full a) -> Data (Complex a) -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (Complex a :-> Full a)
forall a.
(PrimType' a, PrimType' (Complex a)) =>
Primitive (Complex a :-> Full a)
Real

-- | Extract the imaginary part of a complex number
imagPart :: (PrimType a, PrimType (Complex a)) => Data (Complex a) -> Data a
imagPart :: Data (Complex a) -> Data a
imagPart = Primitive (Complex a :-> Full a) -> Data (Complex a) -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (Complex a :-> Full a)
forall a.
(PrimType' a, PrimType' (Complex a)) =>
Primitive (Complex a :-> Full a)
Imag

-- | Extract the magnitude of a complex number's polar form
magnitude :: (RealFloat a, PrimType a, PrimType (Complex a)) =>
    Data (Complex a) -> Data a
magnitude :: Data (Complex a) -> Data a
magnitude = Primitive (Complex a :-> Full a) -> Data (Complex a) -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (Complex a :-> Full a)
forall a.
(RealFloat a, PrimType' a, PrimType' (Complex a)) =>
Primitive (Complex a :-> Full a)
Magnitude

-- | Extract the phase of a complex number's polar form
phase :: (RealFloat a, PrimType a, PrimType (Complex a)) =>
    Data (Complex a) -> Data a
phase :: Data (Complex a) -> Data a
phase = Primitive (Complex a :-> Full a) -> Data (Complex a) -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (Complex a :-> Full a)
forall a.
(RealFloat a, PrimType' a, PrimType' (Complex a)) =>
Primitive (Complex a :-> Full a)
Phase

-- | Complex conjugate
conjugate :: (RealFloat a, PrimType (Complex a)) =>
    Data (Complex a) -> Data (Complex a)
conjugate :: Data (Complex a) -> Data (Complex a)
conjugate = Primitive (Complex a :-> Full (Complex a))
-> Data (Complex a) -> Data (Complex a)
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (Complex a :-> Full (Complex a))
forall a.
(Num a, PrimType' (Complex a)) =>
Primitive (Complex a :-> Full (Complex a))
Conjugate
  -- `RealFloat` could be replaced by `Num` here, but it seems more consistent
  -- to use `RealFloat` for all functions.

-- | Integral type casting
i2n :: (Integral i, Num n, PrimType i, PrimType n) => Data i -> Data n
i2n :: Data i -> Data n
i2n = Primitive (i :-> Full n) -> Data i -> Data n
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (i :-> Full n)
forall a a.
(Integral a, Num a, PrimType' a, PrimType' a) =>
Primitive (a :-> Full a)
I2N

-- | Cast integer to 'Bool'
i2b :: (Integral a, PrimType a) => Data a -> Data Bool
i2b :: Data a -> Data Bool
i2b = Primitive (a :-> Full Bool) -> Data a -> Data Bool
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> Full Bool)
forall a. (Integral a, PrimType' a) => Primitive (a :-> Full Bool)
I2B

-- | Cast 'Bool' to integer
b2i :: (Integral a, PrimType a) => Data Bool -> Data a
b2i :: Data Bool -> Data a
b2i = Primitive (Bool :-> Full a) -> Data Bool -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (Bool :-> Full a)
forall a. (Integral a, PrimType' a) => Primitive (Bool :-> Full a)
B2I

-- | Round a floating-point number to an integer
round :: (RealFrac a, Num b, PrimType a, PrimType b) => Data a -> Data b
round :: Data a -> Data b
round = Primitive (a :-> Full b) -> Data a -> Data b
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> Full b)
forall a a.
(RealFrac a, Num a, PrimType' a, PrimType' a) =>
Primitive (a :-> Full a)
Round

-- | Boolean negation
not :: Data Bool -> Data Bool
not :: Data Bool -> Data Bool
not = Primitive (Bool :-> Full Bool) -> Data Bool -> Data Bool
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (Bool :-> Full Bool)
Not

-- | Boolean conjunction
(&&) :: Data Bool -> Data Bool -> Data Bool
&& :: Data Bool -> Data Bool -> Data Bool
(&&) = Primitive (Bool :-> (Bool :-> Full Bool))
-> Data Bool -> Data Bool -> Data Bool
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (Bool :-> (Bool :-> Full Bool))
And

infixr 3 &&

-- | Boolean disjunction
(||) :: Data Bool -> Data Bool -> Data Bool
|| :: Data Bool -> Data Bool -> Data Bool
(||) = Primitive (Bool :-> (Bool :-> Full Bool))
-> Data Bool -> Data Bool -> Data Bool
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (Bool :-> (Bool :-> Full Bool))
Or

infixr 2 ||


-- | Equality
(==) :: PrimType a => Data a -> Data a -> Data Bool
== :: Data a -> Data a -> Data Bool
(==) = Primitive (a :-> (a :-> Full Bool))
-> Data a -> Data a -> Data Bool
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> (a :-> Full Bool))
forall a.
(Eq a, PrimType' a) =>
Primitive (a :-> (a :-> Full Bool))
Eq

-- | Inequality
(/=) :: PrimType a => Data a -> Data a -> Data Bool
Data a
a /= :: Data a -> Data a -> Data Bool
/= Data a
b = Data Bool -> Data Bool
not (Data a
aData a -> Data a -> Data Bool
forall a. PrimType a => Data a -> Data a -> Data Bool
==Data a
b)

-- | Less than
(<) :: (Ord a, PrimType a) => Data a -> Data a -> Data Bool
< :: Data a -> Data a -> Data Bool
(<) = Primitive (a :-> (a :-> Full Bool))
-> Data a -> Data a -> Data Bool
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> (a :-> Full Bool))
forall a.
(Ord a, PrimType' a) =>
Primitive (a :-> (a :-> Full Bool))
Lt

-- | Greater than
(>) :: (Ord a, PrimType a) => Data a -> Data a -> Data Bool
> :: Data a -> Data a -> Data Bool
(>) = Primitive (a :-> (a :-> Full Bool))
-> Data a -> Data a -> Data Bool
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> (a :-> Full Bool))
forall a.
(Ord a, PrimType' a) =>
Primitive (a :-> (a :-> Full Bool))
Gt

-- | Less than or equal
(<=) :: (Ord a, PrimType a) => Data a -> Data a -> Data Bool
<= :: Data a -> Data a -> Data Bool
(<=) = Primitive (a :-> (a :-> Full Bool))
-> Data a -> Data a -> Data Bool
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> (a :-> Full Bool))
forall a.
(Ord a, PrimType' a) =>
Primitive (a :-> (a :-> Full Bool))
Le

-- | Greater than or equal
(>=) :: (Ord a, PrimType a) => Data a -> Data a -> Data Bool
>= :: Data a -> Data a -> Data Bool
(>=) = Primitive (a :-> (a :-> Full Bool))
-> Data a -> Data a -> Data Bool
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> (a :-> Full Bool))
forall a.
(Ord a, PrimType' a) =>
Primitive (a :-> (a :-> Full Bool))
Ge

infix 4 ==, /=, <, >, <=, >=

-- | Return the smallest of two values
min :: (Ord a, PrimType a) => Data a -> Data a -> Data a
min :: Data a -> Data a -> Data a
min Data a
a Data a
b = Data a
aData a -> Data a -> Data Bool
forall a. (Ord a, PrimType a) => Data a -> Data a -> Data Bool
<=Data a
b Data Bool -> Data a -> Data a -> Data a
forall a. Syntax a => Data Bool -> a -> a -> a
? Data a
a (Data a -> Data a) -> Data a -> Data a
forall a b. (a -> b) -> a -> b
$ Data a
b
  -- There's no standard definition of min/max in C:
  -- <http://stackoverflow.com/questions/3437404/min-and-max-in-c>
  --
  -- There is `fmin`/`fminf` for floating-point numbers, but these are
  -- implemented essentially as above (except that they handle `NaN`
  -- specifically:
  -- <https://sourceware.org/git/?p=glibc.git;a=blob;f=math/s_fmin.c;hb=HEAD>

-- | Return the greatest of two values
max :: (Ord a, PrimType a) => Data a -> Data a -> Data a
max :: Data a -> Data a -> Data a
max Data a
a Data a
b = Data a
aData a -> Data a -> Data Bool
forall a. (Ord a, PrimType a) => Data a -> Data a -> Data Bool
>=Data a
b Data Bool -> Data a -> Data a -> Data a
forall a. Syntax a => Data Bool -> a -> a -> a
? Data a
a (Data a -> Data a) -> Data a -> Data a
forall a b. (a -> b) -> a -> b
$ Data a
b



----------------------------------------
-- ** Bit manipulation
----------------------------------------

-- | Bit-wise \"and\"
(.&.) :: (Bits a, PrimType a) => Data a -> Data a -> Data a
.&. :: Data a -> Data a -> Data a
(.&.) = Primitive (a :-> (a :-> Full a)) -> Data a -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> (a :-> Full a))
forall a. (Bits a, PrimType' a) => Primitive (a :-> (a :-> Full a))
BitAnd

-- | Bit-wise \"or\"
(.|.) :: (Bits a, PrimType a) => Data a -> Data a -> Data a
.|. :: Data a -> Data a -> Data a
(.|.) = Primitive (a :-> (a :-> Full a)) -> Data a -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> (a :-> Full a))
forall a. (Bits a, PrimType' a) => Primitive (a :-> (a :-> Full a))
BitOr

-- | Bit-wise \"xor\"
xor :: (Bits a, PrimType a) => Data a -> Data a -> Data a
xor :: Data a -> Data a -> Data a
xor = Primitive (a :-> (a :-> Full a)) -> Data a -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> (a :-> Full a))
forall a. (Bits a, PrimType' a) => Primitive (a :-> (a :-> Full a))
BitXor

-- | Bit-wise \"xor\"
(⊕) :: (Bits a, PrimType a) => Data a -> Data a -> Data a
⊕ :: Data a -> Data a -> Data a
(⊕) = Data a -> Data a -> Data a
forall a. (Bits a, PrimType a) => Data a -> Data a -> Data a
xor

-- | Bit-wise complement
complement :: (Bits a, PrimType a) => Data a -> Data a
complement :: Data a -> Data a
complement = Primitive (a :-> Full a) -> Data a -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> Full a)
forall a. (Bits a, PrimType' a) => Primitive (a :-> Full a)
BitCompl

-- | Left shift
shiftL :: (Bits a, PrimType a)
    => Data a      -- ^ Value to shift
    -> Data Int32  -- ^ Shift amount (negative value gives right shift)
    -> Data a
shiftL :: Data a -> Data Int32 -> Data a
shiftL = Primitive (a :-> (Int32 :-> Full a))
-> Data a -> Data Int32 -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> (Int32 :-> Full a))
forall a b.
(Bits a, PrimType' a, Integral b, PrimType' b) =>
Primitive (a :-> (b :-> Full a))
ShiftL

-- | Right shift
shiftR :: (Bits a, PrimType a)
    => Data a      -- ^ Value to shift
    -> Data Int32  -- ^ Shift amount (negative value gives left shift)
    -> Data a
shiftR :: Data a -> Data Int32 -> Data a
shiftR = Primitive (a :-> (Int32 :-> Full a))
-> Data a -> Data Int32 -> Data a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld Primitive (a :-> (Int32 :-> Full a))
forall a b.
(Bits a, PrimType' a, Integral b, PrimType' b) =>
Primitive (a :-> (b :-> Full a))
ShiftR

-- | Left shift
(.<<.) :: (Bits a, PrimType a)
    => Data a      -- ^ Value to shift
    -> Data Int32  -- ^ Shift amount (negative value gives right shift)
    -> Data a
.<<. :: Data a -> Data Int32 -> Data a
(.<<.) = Data a -> Data Int32 -> Data a
forall a. (Bits a, PrimType a) => Data a -> Data Int32 -> Data a
shiftL

-- | Right shift
(.>>.) :: (Bits a, PrimType a)
    => Data a      -- ^ Value to shift
    -> Data Int32  -- ^ Shift amount (negative value gives left shift)
    -> Data a
.>>. :: Data a -> Data Int32 -> Data a
(.>>.) = Data a -> Data Int32 -> Data a
forall a. (Bits a, PrimType a) => Data a -> Data Int32 -> Data a
shiftR

infixl 8 `shiftL`, `shiftR`, .<<., .>>.
infixl 7 .&.
infixl 6 `xor`
infixl 5 .|.

bitSize :: forall a . FiniteBits a => Data a -> Length
bitSize :: Data a -> Length
bitSize Data a
_ = Int -> Length
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral (Int -> Length) -> Int -> Length
forall a b. (a -> b) -> a -> b
$ a -> Int
forall b. FiniteBits b => b -> Int
Bits.finiteBitSize (a
forall a. a
a :: a)
  where
    a :: a
a = String -> a
forall a. HasCallStack => String -> a
P.error String
"finiteBitSize evaluates its argument"

-- | Set all bits to one
allOnes :: (Bits a, Num a, PrimType a) => Data a
allOnes :: Data a
allOnes = Data a -> Data a
forall a. (Bits a, PrimType a) => Data a -> Data a
complement Data a
0

-- | Set the @n@ lowest bits to one
oneBits :: (Bits a, Num a, PrimType a) => Data Int32 -> Data a
oneBits :: Data Int32 -> Data a
oneBits Data Int32
n = Data a -> Data a
forall a. (Bits a, PrimType a) => Data a -> Data a
complement (Data a
forall a. (Bits a, Num a, PrimType a) => Data a
allOnes Data a -> Data Int32 -> Data a
forall a. (Bits a, PrimType a) => Data a -> Data Int32 -> Data a
.<<. Data Int32
n)

-- | Extract the @k@ lowest bits
lsbs :: (Bits a, Num a, PrimType a) => Data Int32 -> Data a -> Data a
lsbs :: Data Int32 -> Data a -> Data a
lsbs Data Int32
k Data a
i = Data a
i Data a -> Data a -> Data a
forall a. (Bits a, PrimType a) => Data a -> Data a -> Data a
.&. Data Int32 -> Data a
forall a. (Bits a, Num a, PrimType a) => Data Int32 -> Data a
oneBits Data Int32
k

-- | Integer logarithm in base 2. Returns \(\lfloor log_2(x) \rfloor\).
-- Assumes \(x>0\).
ilog2 :: (FiniteBits a, Integral a, PrimType a) => Data a -> Data a
ilog2 :: Data a -> Data a
ilog2 Data a
a = AssertionLabel -> Data Bool -> String -> Data a -> Data a
forall a.
Syntax a =>
AssertionLabel -> Data Bool -> String -> a -> a
guardValLabel AssertionLabel
InternalAssertion (Data a
a Data a -> Data a -> Data Bool
forall a. (Ord a, PrimType a) => Data a -> Data a -> Data Bool
>= Data a
1) String
"ilog2: argument < 1" (Data a -> Data a) -> Data a -> Data a
forall a b. (a -> b) -> a -> b
$
    (Data a, Data a) -> Data a
forall a b. (a, b) -> b
snd ((Data a, Data a) -> Data a) -> (Data a, Data a) -> Data a
forall a b. (a -> b) -> a -> b
$ ((Integer, Int32) -> (Data a, Data a) -> (Data a, Data a))
-> (Data a, Data a) -> [(Integer, Int32)] -> (Data a, Data a)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
P.foldr (\(Integer, Int32)
ffi (Data a, Data a)
vr -> (Data a, Data a)
-> ((Data a, Data a) -> (Data a, Data a)) -> (Data a, Data a)
forall a b. (Syntax a, Syntax b) => a -> (a -> b) -> b
share (Data a, Data a)
vr ((Integer, Int32) -> (Data a, Data a) -> (Data a, Data a)
forall a a.
(Type a, Type a, Integral a, PrimType' a, PrimType' a, Bits a,
 Bits a, Num a, Ord a) =>
(Integer, Int32) -> (Data a, Data a) -> (Data a, Data a)
step (Integer, Int32)
ffi)) (Data a
a,Data a
0) [(Integer, Int32)]
ffis
  where
    step :: (Integer, Int32) -> (Data a, Data a) -> (Data a, Data a)
step (Integer
ff,Int32
i) (Data a
v,Data a
r) =
        Data a -> (Data a -> (Data a, Data a)) -> (Data a, Data a)
forall a b. (Syntax a, Syntax b) => a -> (a -> b) -> b
share (Data Bool -> Data a
forall a. (Integral a, PrimType a) => Data Bool -> Data a
b2i (Data a
v Data a -> Data a -> Data Bool
forall a. (Ord a, PrimType a) => Data a -> Data a -> Data Bool
> Integer -> Data a
forall a. Num a => Integer -> a
fromInteger Integer
ff) Data a -> Data Int32 -> Data a
forall a. (Bits a, PrimType a) => Data a -> Data Int32 -> Data a
.<<. Internal (Data Int32) -> Data Int32
forall a. Syntax a => Internal a -> a
value Int32
Internal (Data Int32)
i) ((Data a -> (Data a, Data a)) -> (Data a, Data a))
-> (Data a -> (Data a, Data a)) -> (Data a, Data a)
forall a b. (a -> b) -> a -> b
$ \Data a
shift ->
          (Data a
v Data a -> Data Int32 -> Data a
forall a. (Bits a, PrimType a) => Data a -> Data Int32 -> Data a
.>>. Data a -> Data Int32
forall i n.
(Integral i, Num n, PrimType i, PrimType n) =>
Data i -> Data n
i2n Data a
shift, Data a
r Data a -> Data a -> Data a
forall a. (Bits a, PrimType a) => Data a -> Data a -> Data a
.|. Data a
shift)

    -- [(0x1, 0), (0x3, 1), (0xF, 2), (0xFF, 3), (0xFFFF, 4), ...]
    ffis :: [(Integer, Int32)]
ffis
        = ([Integer] -> [Int32] -> [(Integer, Int32)]
forall a b. [a] -> [b] -> [(a, b)]
`P.zip` [Int32
0..])
        ([Integer] -> [(Integer, Int32)])
-> [Integer] -> [(Integer, Int32)]
forall a b. (a -> b) -> a -> b
$ (Integer -> Bool) -> [Integer] -> [Integer]
forall a. (a -> Bool) -> [a] -> [a]
P.takeWhile (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
P.<= (Integer
2 Integer -> Length -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
P.^ (Data a -> Length
forall a. FiniteBits a => Data a -> Length
bitSize Data a
a Length -> Length -> Length
forall a. Integral a => a -> a -> a
`P.div` Length
2) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1 :: Integer))
        ([Integer] -> [Integer]) -> [Integer] -> [Integer]
forall a b. (a -> b) -> a -> b
$ (Integer -> Integer) -> [Integer] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
P.map ((Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
subtract Integer
1) (Integer -> Integer) -> (Integer -> Integer) -> Integer -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
P.^) (Integer -> Integer) -> (Integer -> Integer) -> Integer -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
P.^))
        ([Integer] -> [Integer]) -> [Integer] -> [Integer]
forall a b. (a -> b) -> a -> b
$ [(Integer
0::Integer)..]
  -- Based on this algorithm:
  -- <http://graphics.stanford.edu/~seander/bithacks.html#IntegerLog>



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

-- | Index into an array
arrIx :: Syntax a => IArr a -> Data Index -> a
arrIx :: IArr a -> Data Length -> a
arrIx IArr a
arr Data Length
i = Struct PrimType' Data (Internal a) -> a
forall a b. (Syntax a, Syntax b, Internal a ~ Internal b) => a -> b
resugar (Struct PrimType' Data (Internal a) -> a)
-> Struct PrimType' Data (Internal a) -> a
forall a b. (a -> b) -> a -> b
$ (forall a. PrimType' a => IArr Length a -> Data a)
-> Struct PrimType' (IArr Length) (Internal a)
-> Struct PrimType' Data (Internal a)
forall (pred :: * -> Constraint) (c1 :: * -> *) (c2 :: * -> *) b.
(forall a. pred a => c1 a -> c2 a)
-> Struct pred c1 b -> Struct pred c2 b
mapStruct forall a. PrimType' a => IArr Length a -> Data a
ix (Struct PrimType' (IArr Length) (Internal a)
 -> Struct PrimType' Data (Internal a))
-> Struct PrimType' (IArr Length) (Internal a)
-> Struct PrimType' Data (Internal a)
forall a b. (a -> b) -> a -> b
$ IArr a -> Struct PrimType' (IArr Length) (Internal a)
forall a. IArr a -> Struct PrimType' (IArr Length) (Internal a)
unIArr IArr a
arr
  where
    ix :: forall b . PrimType' b => Imp.IArr Index b -> Data b
    ix :: IArr Length b -> Data b
ix IArr Length b
arr' = ExtraPrimitive (Bool :-> (b :-> Full b))
-> Data Bool -> Data b -> Data b
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 PrimType' (DenResult sig)) =>
sub sig -> f
sugarSymFeldPrim
      (AssertionLabel
-> String -> ExtraPrimitive (Bool :-> (b :-> Full b))
forall a.
AssertionLabel
-> String -> ExtraPrimitive (Bool :-> (a :-> Full a))
GuardVal AssertionLabel
InternalAssertion String
"arrIx: index out of bounds")
      (Data Length
i Data Length -> Data Length -> Data Bool
forall a. (Ord a, PrimType a) => Data a -> Data a -> Data Bool
< IArr a -> Data Length
forall a. Finite a => a -> Data Length
length IArr a
arr)
      (Primitive (Length :-> Full b) -> Data Length -> Data b
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 PrimType' (DenResult sig)) =>
sub sig -> f
sugarSymFeldPrim (IArr Length b -> Primitive (Length :-> Full b)
forall a.
PrimType' a =>
IArr Length a -> Primitive (Length :-> Full a)
ArrIx IArr Length b
arr') (Data Length
i Data Length -> Data Length -> Data Length
forall a. Num a => a -> a -> a
+ IArr a -> Data Length
forall a. IArr a -> Data Length
iarrOffset IArr a
arr) :: Data b)

class Indexed a
  where
    type IndexedElem a

    -- | Indexing operator. If @a@ is 'Finite', it is assumed that
    -- @i < `length` a@ in any expression @a `!` i@.
    (!) :: a -> Data Index -> IndexedElem a

infixl 9 !

-- | Linear structures with a length. If the type is also 'Indexed', the length
-- is the successor of the maximal allowed index.
class Finite a
  where
    -- | The length of a finite structure
    length :: a -> Data Length

instance Finite (Arr a)  where length :: Arr a -> Data Length
length = Arr a -> Data Length
forall a. Arr a -> Data Length
arrLength
instance Finite (IArr a) where length :: IArr a -> Data Length
length = IArr a -> Data Length
forall a. IArr a -> Data Length
iarrLength

-- | Linear structures that can be sliced
class Slicable a
  where
    -- | Take a slice of a structure
    slice
        :: Data Index   -- ^ Start index
        -> Data Length  -- ^ Slice length
        -> a            -- ^ Structure to slice
        -> a

instance Syntax a => Indexed (IArr a)
  where
    type IndexedElem (IArr a) = a
    (!) = IArr a -> Data Length -> IndexedElem (IArr a)
forall a. Syntax a => IArr a -> Data Length -> a
arrIx

instance Slicable (Arr a)
  where
    slice :: Data Length -> Data Length -> Arr a -> Arr a
slice Data Length
from Data Length
len (Arr Data Length
o Data Length
l Struct PrimType' (Arr Length) (Internal a)
arr) = Data Length
-> Data Length
-> Struct PrimType' (Arr Length) (Internal a)
-> Arr a
forall a.
Data Length
-> Data Length
-> Struct PrimType' (Arr Length) (Internal a)
-> Arr a
Arr Data Length
o' Data Length
l' Struct PrimType' (Arr Length) (Internal a)
arr
      where
        o' :: Data Length
o' = AssertionLabel -> Data Bool -> String -> Data Length -> Data Length
forall a.
Syntax a =>
AssertionLabel -> Data Bool -> String -> a -> a
guardValLabel AssertionLabel
InternalAssertion (Data Length
fromData Length -> Data Length -> Data Bool
forall a. (Ord a, PrimType a) => Data a -> Data a -> Data Bool
<=Data Length
l) String
"invalid Arr slice" (Data Length
oData Length -> Data Length -> Data Length
forall a. Num a => a -> a -> a
+Data Length
from)
        l' :: Data Length
l' = AssertionLabel -> Data Bool -> String -> Data Length -> Data Length
forall a.
Syntax a =>
AssertionLabel -> Data Bool -> String -> a -> a
guardValLabel AssertionLabel
InternalAssertion (Data Length
fromData Length -> Data Length -> Data Length
forall a. Num a => a -> a -> a
+Data Length
lenData Length -> Data Length -> Data Bool
forall a. (Ord a, PrimType a) => Data a -> Data a -> Data Bool
<=Data Length
l) String
"invalid Arr slice" Data Length
len

instance Slicable (IArr a)
  where
    slice :: Data Length -> Data Length -> IArr a -> IArr a
slice Data Length
from Data Length
len (IArr Data Length
o Data Length
l Struct PrimType' (IArr Length) (Internal a)
arr) = Data Length
-> Data Length
-> Struct PrimType' (IArr Length) (Internal a)
-> IArr a
forall a.
Data Length
-> Data Length
-> Struct PrimType' (IArr Length) (Internal a)
-> IArr a
IArr Data Length
o' Data Length
l' Struct PrimType' (IArr Length) (Internal a)
arr
      where
        o' :: Data Length
o' = AssertionLabel -> Data Bool -> String -> Data Length -> Data Length
forall a.
Syntax a =>
AssertionLabel -> Data Bool -> String -> a -> a
guardValLabel AssertionLabel
InternalAssertion (Data Length
fromData Length -> Data Length -> Data Bool
forall a. (Ord a, PrimType a) => Data a -> Data a -> Data Bool
<=Data Length
l) String
"invalid IArr slice" (Data Length
oData Length -> Data Length -> Data Length
forall a. Num a => a -> a -> a
+Data Length
from)
        l' :: Data Length
l' = AssertionLabel -> Data Bool -> String -> Data Length -> Data Length
forall a.
Syntax a =>
AssertionLabel -> Data Bool -> String -> a -> a
guardValLabel AssertionLabel
InternalAssertion (Data Length
fromData Length -> Data Length -> Data Length
forall a. Num a => a -> a -> a
+Data Length
lenData Length -> Data Length -> Data Bool
forall a. (Ord a, PrimType a) => Data a -> Data a -> Data Bool
<=Data Length
l) String
"invalid IArr slice" Data Length
len



----------------------------------------
-- ** Syntactic conversion
----------------------------------------

desugar :: Syntax a => a -> Data (Internal a)
desugar :: a -> Data (Internal a)
desugar = ASTF FeldDomain (Internal a) -> Data (Internal a)
forall a. ASTF FeldDomain a -> Data a
Data (ASTF FeldDomain (Internal a) -> Data (Internal a))
-> (a -> ASTF FeldDomain (Internal a)) -> a -> Data (Internal a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ASTF FeldDomain (Internal a)
forall a. Syntactic a => a -> ASTF (Domain a) (Internal a)
Syntactic.desugar

sugar :: Syntax a => Data (Internal a) -> a
sugar :: Data (Internal a) -> a
sugar = AST FeldDomain (Full (Internal a)) -> a
forall a. Syntactic a => ASTF (Domain a) (Internal a) -> a
Syntactic.sugar (AST FeldDomain (Full (Internal a)) -> a)
-> (Data (Internal a) -> AST FeldDomain (Full (Internal a)))
-> Data (Internal a)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Data (Internal a) -> AST FeldDomain (Full (Internal a))
forall a. Data a -> ASTF FeldDomain a
unData

-- | Cast between two values that have the same syntactic representation
resugar :: (Syntax a, Syntax b, Internal a ~ Internal b) => a -> b
resugar :: a -> b
resugar = a -> b
forall a b.
(Syntactic a, Syntactic b, Domain a ~ Domain b,
 Internal a ~ Internal b) =>
a -> b
Syntactic.resugar



----------------------------------------
-- ** Assertions
----------------------------------------

-- | Guard a value by an assertion (with implicit label @`UserAssertion` ""@)
guardVal :: Syntax a
    => Data Bool  -- ^ Condition that is expected to be true
    -> String     -- ^ Error message
    -> a          -- ^ Value to attach the assertion to
    -> a
guardVal :: Data Bool -> String -> a -> a
guardVal = AssertionLabel -> Data Bool -> String -> a -> a
forall a.
Syntax a =>
AssertionLabel -> Data Bool -> String -> a -> a
guardValLabel (AssertionLabel -> Data Bool -> String -> a -> a)
-> AssertionLabel -> Data Bool -> String -> a -> a
forall a b. (a -> b) -> a -> b
$ String -> AssertionLabel
UserAssertion String
""

-- | Like 'guardVal' but with an explicit assertion label
guardValLabel :: Syntax a
    => AssertionLabel  -- ^ Assertion label
    -> Data Bool       -- ^ Condition that is expected to be true
    -> String          -- ^ Error message
    -> a               -- ^ Value to attach the assertion to
    -> a
guardValLabel :: AssertionLabel -> Data Bool -> String -> a -> a
guardValLabel AssertionLabel
c Data Bool
cond String
msg = ExtraPrimitive (Bool :-> (Internal a :-> Full (Internal a)))
-> Data Bool -> a -> a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld (AssertionLabel
-> String
-> ExtraPrimitive (Bool :-> (Internal a :-> Full (Internal a)))
forall a.
AssertionLabel
-> String -> ExtraPrimitive (Bool :-> (a :-> Full a))
GuardVal AssertionLabel
c String
msg) Data Bool
cond



----------------------------------------
-- ** Unsafe operations
----------------------------------------

-- | Turn a 'Comp' computation into a pure value. For this to be safe, the
-- computation should be free of side effects and independent of its
-- environment.
unsafePerform :: Syntax a => Comp a -> a
unsafePerform :: Comp a -> a
unsafePerform = Unsafe (Full (Internal a)) -> a
forall sig fi f (sub :: * -> *).
(Signature sig, fi ~ SmartFun FeldDomain sig, sig ~ SmartSig fi,
 FeldDomain ~ SmartSym fi, SyntacticN f fi, sub :<: FeldConstructs,
 Type (DenResult sig)) =>
sub sig -> f
sugarSymFeld (Unsafe (Full (Internal a)) -> a)
-> (Comp a -> Unsafe (Full (Internal a))) -> Comp a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Comp (Data (Internal a)) -> Unsafe (Full (Internal a))
forall a. Comp (Data a) -> Unsafe (Full a)
UnsafePerform (Comp (Data (Internal a)) -> Unsafe (Full (Internal a)))
-> (Comp a -> Comp (Data (Internal a)))
-> Comp a
-> Unsafe (Full (Internal a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Data (Internal a)) -> Comp a -> Comp (Data (Internal a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Data (Internal a)
forall a. Syntax a => a -> Data (Internal a)
desugar



--------------------------------------------------------------------------------
-- * Programs with computational effects
--------------------------------------------------------------------------------

-- | Monads that support computational effects: mutable data structures and
-- control flow
class Monad m => MonadComp m
  where
    -- | Lift a 'Comp' computation
    liftComp :: Comp a -> m a
    -- | Conditional statement
    iff :: Data Bool -> m () -> m () -> m ()
    -- | For loop
    for :: (Integral n, PrimType n) =>
        IxRange (Data n) -> (Data n -> m ()) -> m ()
    -- | While loop
    while :: m (Data Bool) -> m () -> m ()

instance MonadComp Comp
  where
    liftComp :: Comp a -> Comp a
liftComp        = Comp a -> Comp a
forall a. a -> a
id
    iff :: Data Bool -> Comp () -> Comp () -> Comp ()
iff Data Bool
c Comp ()
t Comp ()
f       = Program CompCMD (Param2 Data PrimType') () -> Comp ()
forall a. Program CompCMD (Param2 Data PrimType') a -> Comp a
Comp (Program CompCMD (Param2 Data PrimType') () -> Comp ())
-> Program CompCMD (Param2 Data PrimType') () -> Comp ()
forall a b. (a -> b) -> a -> b
$ Data Bool
-> Program CompCMD (Param2 Data PrimType') ()
-> Program CompCMD (Param2 Data PrimType') ()
-> Program CompCMD (Param2 Data PrimType') ()
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 ()
Imp.iff Data Bool
c (Comp () -> Program CompCMD (Param2 Data PrimType') ()
forall a. Comp a -> Program CompCMD (Param2 Data PrimType') a
unComp Comp ()
t) (Comp () -> Program CompCMD (Param2 Data PrimType') ()
forall a. Comp a -> Program CompCMD (Param2 Data PrimType') a
unComp Comp ()
f)
    for :: IxRange (Data n) -> (Data n -> Comp ()) -> Comp ()
for IxRange (Data n)
range Data n -> Comp ()
body  = Program CompCMD (Param2 Data PrimType') () -> Comp ()
forall a. Program CompCMD (Param2 Data PrimType') a -> Comp a
Comp (Program CompCMD (Param2 Data PrimType') () -> Comp ())
-> Program CompCMD (Param2 Data PrimType') () -> Comp ()
forall a b. (a -> b) -> a -> b
$ IxRange (Data n)
-> (Data n -> Program CompCMD (Param2 Data PrimType') ())
-> Program CompCMD (Param2 Data PrimType') ()
forall (exp :: * -> *)
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *) n
       (pred :: * -> Constraint) (m :: * -> *).
(FreeExp exp, ControlCMD :<: instr, Integral n, pred n,
 FreePred exp n) =>
IxRange (exp n)
-> (exp n -> ProgramT instr (Param2 exp pred) m ())
-> ProgramT instr (Param2 exp pred) m ()
Imp.for IxRange (Data n)
range (Comp () -> Program CompCMD (Param2 Data PrimType') ()
forall a. Comp a -> Program CompCMD (Param2 Data PrimType') a
unComp (Comp () -> Program CompCMD (Param2 Data PrimType') ())
-> (Data n -> Comp ())
-> Data n
-> Program CompCMD (Param2 Data PrimType') ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Data n -> Comp ()
body)
    while :: Comp (Data Bool) -> Comp () -> Comp ()
while Comp (Data Bool)
cont Comp ()
body = Program CompCMD (Param2 Data PrimType') () -> Comp ()
forall a. Program CompCMD (Param2 Data PrimType') a -> Comp a
Comp (Program CompCMD (Param2 Data PrimType') () -> Comp ())
-> Program CompCMD (Param2 Data PrimType') () -> Comp ()
forall a b. (a -> b) -> a -> b
$ ProgramT CompCMD (Param2 Data PrimType') Identity (Data Bool)
-> Program CompCMD (Param2 Data PrimType') ()
-> Program CompCMD (Param2 Data PrimType') ()
forall (instr :: (* -> *, (* -> *, (* -> Constraint, *)))
                 -> * -> *)
       (exp :: * -> *) (pred :: * -> Constraint) (m :: * -> *).
(ControlCMD :<: instr) =>
ProgramT instr (Param2 exp pred) m (exp Bool)
-> ProgramT instr (Param2 exp pred) m ()
-> ProgramT instr (Param2 exp pred) m ()
Imp.while (Comp (Data Bool)
-> ProgramT CompCMD (Param2 Data PrimType') Identity (Data Bool)
forall a. Comp a -> Program CompCMD (Param2 Data PrimType') a
unComp Comp (Data Bool)
cont) (Comp () -> Program CompCMD (Param2 Data PrimType') ()
forall a. Comp a -> Program CompCMD (Param2 Data PrimType') a
unComp Comp ()
body)



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

-- | Create an uninitialized reference
newRef :: (Syntax a, MonadComp m) => m (Ref a)
newRef :: m (Ref a)
newRef = String -> m (Ref a)
forall a (m :: * -> *).
(Syntax a, MonadComp m) =>
String -> 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 :: (Syntax a, MonadComp m)
    => String  -- ^ Base name
    -> m (Ref a)
newNamedRef :: String -> m (Ref a)
newNamedRef String
base = Comp (Ref a) -> m (Ref a)
forall (m :: * -> *) a. MonadComp m => Comp a -> m a
liftComp (Comp (Ref a) -> m (Ref a)) -> Comp (Ref a) -> m (Ref a)
forall a b. (a -> b) -> a -> b
$ (Struct PrimType' Ref (Internal a) -> Ref a)
-> Comp (Struct PrimType' Ref (Internal a)) -> Comp (Ref a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Struct PrimType' Ref (Internal a) -> Ref a
forall a. Struct PrimType' Ref (Internal a) -> Ref a
Ref (Comp (Struct PrimType' Ref (Internal a)) -> Comp (Ref a))
-> Comp (Struct PrimType' Ref (Internal a)) -> Comp (Ref a)
forall a b. (a -> b) -> a -> b
$
    (forall a. PrimType' a => PrimTypeRep a -> Comp (Ref a))
-> Struct PrimType' PrimTypeRep (Internal a)
-> Comp (Struct PrimType' Ref (Internal a))
forall (m :: * -> *) (pred :: * -> Constraint) (c1 :: * -> *)
       (c2 :: * -> *) b.
Applicative m =>
(forall a. pred a => c1 a -> m (c2 a))
-> Struct pred c1 b -> m (Struct pred c2 b)
mapStructA (Comp (Ref a) -> PrimTypeRep a -> Comp (Ref a)
forall a b. a -> b -> a
const (Comp (Ref a) -> PrimTypeRep a -> Comp (Ref a))
-> Comp (Ref a) -> PrimTypeRep a -> Comp (Ref a)
forall a b. (a -> b) -> a -> b
$ Program CompCMD (Param2 Data PrimType') (Ref a) -> Comp (Ref a)
forall a. Program CompCMD (Param2 Data PrimType') a -> Comp a
Comp (Program CompCMD (Param2 Data PrimType') (Ref a) -> Comp (Ref a))
-> Program CompCMD (Param2 Data PrimType') (Ref a) -> Comp (Ref a)
forall a b. (a -> b) -> a -> b
$ String -> Program CompCMD (Param2 Data PrimType') (Ref a)
forall (pred :: * -> Constraint) a
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (exp :: * -> *) (m :: * -> *).
(pred a, RefCMD :<: instr) =>
String -> ProgramT instr (Param2 exp pred) m (Ref a)
Imp.newNamedRef String
base) Struct PrimType' PrimTypeRep (Internal a)
forall a. Type a => TypeRep a
typeRep

-- | Create an initialized named reference
initRef :: (Syntax a, MonadComp m) => a -> m (Ref a)
initRef :: a -> m (Ref a)
initRef = String -> a -> m (Ref a)
forall a (m :: * -> *).
(Syntax a, MonadComp m) =>
String -> a -> m (Ref a)
initNamedRef String
"r"

-- | Create an initialized reference
--
-- The provided base name may be appended with a unique identifier to avoid name
-- collisions.
initNamedRef :: (Syntax a, MonadComp m)
    => String  -- ^ Base name
    -> a       -- ^ Initial value
    -> m (Ref a)
initNamedRef :: String -> a -> m (Ref a)
initNamedRef String
base =
    Comp (Ref a) -> m (Ref a)
forall (m :: * -> *) a. MonadComp m => Comp a -> m a
liftComp (Comp (Ref a) -> m (Ref a))
-> (a -> Comp (Ref a)) -> a -> m (Ref a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Struct PrimType' Ref (Internal a) -> Ref a)
-> Comp (Struct PrimType' Ref (Internal a)) -> Comp (Ref a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Struct PrimType' Ref (Internal a) -> Ref a
forall a. Struct PrimType' Ref (Internal a) -> Ref a
Ref (Comp (Struct PrimType' Ref (Internal a)) -> Comp (Ref a))
-> (a -> Comp (Struct PrimType' Ref (Internal a)))
-> a
-> Comp (Ref a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. PrimType' a => Data a -> Comp (Ref a))
-> Struct PrimType' Data (Internal a)
-> Comp (Struct PrimType' Ref (Internal a))
forall (m :: * -> *) (pred :: * -> Constraint) (c1 :: * -> *)
       (c2 :: * -> *) b.
Applicative m =>
(forall a. pred a => c1 a -> m (c2 a))
-> Struct pred c1 b -> m (Struct pred c2 b)
mapStructA (Program CompCMD (Param2 Data PrimType') (Ref a) -> Comp (Ref a)
forall a. Program CompCMD (Param2 Data PrimType') a -> Comp a
Comp (Program CompCMD (Param2 Data PrimType') (Ref a) -> Comp (Ref a))
-> (Data a -> Program CompCMD (Param2 Data PrimType') (Ref a))
-> Data a
-> Comp (Ref a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Data a -> Program CompCMD (Param2 Data PrimType') (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)
Imp.initNamedRef String
base) (Struct PrimType' Data (Internal a)
 -> Comp (Struct PrimType' Ref (Internal a)))
-> (a -> Struct PrimType' Data (Internal a))
-> a
-> Comp (Struct PrimType' Ref (Internal a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Struct PrimType' Data (Internal a)
forall a b. (Syntax a, Syntax b, Internal a ~ Internal b) => a -> b
resugar

-- | Get the contents of a reference.
getRef :: (Syntax a, MonadComp m) => Ref a -> m a
getRef :: Ref a -> m a
getRef = Comp a -> m a
forall (m :: * -> *) a. MonadComp m => Comp a -> m a
liftComp (Comp a -> m a) -> (Ref a -> Comp a) -> Ref a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Struct PrimType' Data (Internal a) -> a)
-> Comp (Struct PrimType' Data (Internal a)) -> Comp a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Struct PrimType' Data (Internal a) -> a
forall a b. (Syntax a, Syntax b, Internal a ~ Internal b) => a -> b
resugar (Comp (Struct PrimType' Data (Internal a)) -> Comp a)
-> (Ref a -> Comp (Struct PrimType' Data (Internal a)))
-> Ref a
-> Comp a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. PrimType' a => Ref a -> Comp (Data a))
-> Struct PrimType' Ref (Internal a)
-> Comp (Struct PrimType' Data (Internal a))
forall (m :: * -> *) (pred :: * -> Constraint) (c1 :: * -> *)
       (c2 :: * -> *) b.
Applicative m =>
(forall a. pred a => c1 a -> m (c2 a))
-> Struct pred c1 b -> m (Struct pred c2 b)
mapStructA (Program CompCMD (Param2 Data PrimType') (Data a) -> Comp (Data a)
forall a. Program CompCMD (Param2 Data PrimType') a -> Comp a
Comp (Program CompCMD (Param2 Data PrimType') (Data a) -> Comp (Data a))
-> (Ref a -> Program CompCMD (Param2 Data PrimType') (Data a))
-> Ref a
-> Comp (Data a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ref a -> Program CompCMD (Param2 Data PrimType') (Data 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)
Imp.getRef) (Struct PrimType' Ref (Internal a)
 -> Comp (Struct PrimType' Data (Internal a)))
-> (Ref a -> Struct PrimType' Ref (Internal a))
-> Ref a
-> Comp (Struct PrimType' Data (Internal a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ref a -> Struct PrimType' Ref (Internal a)
forall a. Ref a -> Struct PrimType' Ref (Internal a)
unRef

-- | Set the contents of a reference.
setRef :: (Syntax a, MonadComp m) => Ref a -> a -> m ()
setRef :: Ref a -> a -> m ()
setRef Ref a
r
    = Comp () -> m ()
forall (m :: * -> *) a. MonadComp m => Comp a -> m a
liftComp
    (Comp () -> m ()) -> (a -> Comp ()) -> a -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Comp ()] -> Comp ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_
    ([Comp ()] -> Comp ()) -> (a -> [Comp ()]) -> a -> Comp ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. PrimType' a => Ref a -> Data a -> Comp ())
-> Struct PrimType' Ref (Internal a)
-> Struct PrimType' Data (Internal a)
-> [Comp ()]
forall (pred :: * -> Constraint) (c1 :: * -> *) (c2 :: * -> *) b r.
(forall a. pred a => c1 a -> c2 a -> r)
-> Struct pred c1 b -> Struct pred c2 b -> [r]
zipListStruct (\Ref a
r' Data a
a' -> Program CompCMD (Param2 Data PrimType') () -> Comp ()
forall a. Program CompCMD (Param2 Data PrimType') a -> Comp a
Comp (Program CompCMD (Param2 Data PrimType') () -> Comp ())
-> Program CompCMD (Param2 Data PrimType') () -> Comp ()
forall a b. (a -> b) -> a -> b
$ Ref a -> Data a -> Program CompCMD (Param2 Data PrimType') ()
forall (pred :: * -> Constraint) a
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (exp :: * -> *) (m :: * -> *).
(pred a, RefCMD :<: instr) =>
Ref a -> exp a -> ProgramT instr (Param2 exp pred) m ()
Imp.setRef Ref a
r' Data a
a') (Ref a -> Struct PrimType' Ref (Internal a)
forall a. Ref a -> Struct PrimType' Ref (Internal a)
unRef Ref a
r)
    (Struct PrimType' Data (Internal a) -> [Comp ()])
-> (a -> Struct PrimType' Data (Internal a)) -> a -> [Comp ()]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Struct PrimType' Data (Internal a)
forall a b. (Syntax a, Syntax b, Internal a ~ Internal b) => a -> b
resugar

-- | Modify the contents of reference.
modifyRef :: (Syntax a, MonadComp m) => Ref a -> (a -> a) -> m ()
modifyRef :: Ref a -> (a -> a) -> m ()
modifyRef Ref a
r a -> a
f = Ref a -> a -> m ()
forall a (m :: * -> *).
(Syntax a, MonadComp m) =>
Ref a -> a -> m ()
setRef Ref a
r (a -> m ()) -> (a -> a) -> a -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
f (a -> m ()) -> m a -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Ref a -> m a
forall a (m :: * -> *). (Syntax a, MonadComp m) => Ref a -> m 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 :: (Syntax a, MonadComp m) => Ref a -> m a
unsafeFreezeRef :: Ref a -> m a
unsafeFreezeRef
    = Comp a -> m a
forall (m :: * -> *) a. MonadComp m => Comp a -> m a
liftComp
    (Comp a -> m a) -> (Ref a -> Comp a) -> Ref a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Struct PrimType' Data (Internal a) -> a)
-> Comp (Struct PrimType' Data (Internal a)) -> Comp a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Struct PrimType' Data (Internal a) -> a
forall a b. (Syntax a, Syntax b, Internal a ~ Internal b) => a -> b
resugar
    (Comp (Struct PrimType' Data (Internal a)) -> Comp a)
-> (Ref a -> Comp (Struct PrimType' Data (Internal a)))
-> Ref a
-> Comp a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. PrimType' a => Ref a -> Comp (Data a))
-> Struct PrimType' Ref (Internal a)
-> Comp (Struct PrimType' Data (Internal a))
forall (m :: * -> *) (pred :: * -> Constraint) (c1 :: * -> *)
       (c2 :: * -> *) b.
Applicative m =>
(forall a. pred a => c1 a -> m (c2 a))
-> Struct pred c1 b -> m (Struct pred c2 b)
mapStructA (Program CompCMD (Param2 Data PrimType') (Data a) -> Comp (Data a)
forall a. Program CompCMD (Param2 Data PrimType') a -> Comp a
Comp (Program CompCMD (Param2 Data PrimType') (Data a) -> Comp (Data a))
-> (Ref a -> Program CompCMD (Param2 Data PrimType') (Data a))
-> Ref a
-> Comp (Data a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ref a -> Program CompCMD (Param2 Data PrimType') (Data 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)
Imp.unsafeFreezeRef)
    (Struct PrimType' Ref (Internal a)
 -> Comp (Struct PrimType' Data (Internal a)))
-> (Ref a -> Struct PrimType' Ref (Internal a))
-> Ref a
-> Comp (Struct PrimType' Data (Internal a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ref a -> Struct PrimType' Ref (Internal a)
forall a. Ref a -> Struct PrimType' Ref (Internal a)
unRef



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

-- | Create an uninitialized array
newArr :: (Type (Internal a), MonadComp m) => Data Length -> m (Arr a)
newArr :: Data Length -> m (Arr a)
newArr = String -> Data Length -> m (Arr a)
forall a (m :: * -> *).
(Type (Internal a), MonadComp m) =>
String -> Data Length -> m (Arr 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 :: (Type (Internal a), MonadComp m)
    => String  -- ^ Base name
    -> Data Length
    -> m (Arr a)
newNamedArr :: String -> Data Length -> m (Arr a)
newNamedArr String
base Data Length
l = Comp (Arr a) -> m (Arr a)
forall (m :: * -> *) a. MonadComp m => Comp a -> m a
liftComp (Comp (Arr a) -> m (Arr a)) -> Comp (Arr a) -> m (Arr a)
forall a b. (a -> b) -> a -> b
$ (Struct PrimType' (Arr Length) (Internal a) -> Arr a)
-> Comp (Struct PrimType' (Arr Length) (Internal a))
-> Comp (Arr a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Data Length
-> Data Length
-> Struct PrimType' (Arr Length) (Internal a)
-> Arr a
forall a.
Data Length
-> Data Length
-> Struct PrimType' (Arr Length) (Internal a)
-> Arr a
Arr Data Length
0 Data Length
l) (Comp (Struct PrimType' (Arr Length) (Internal a)) -> Comp (Arr a))
-> Comp (Struct PrimType' (Arr Length) (Internal a))
-> Comp (Arr a)
forall a b. (a -> b) -> a -> b
$
    (forall a. PrimType' a => PrimTypeRep a -> Comp (Arr Length a))
-> Struct PrimType' PrimTypeRep (Internal a)
-> Comp (Struct PrimType' (Arr Length) (Internal a))
forall (m :: * -> *) (pred :: * -> Constraint) (c1 :: * -> *)
       (c2 :: * -> *) b.
Applicative m =>
(forall a. pred a => c1 a -> m (c2 a))
-> Struct pred c1 b -> m (Struct pred c2 b)
mapStructA (Comp (Arr Length a) -> PrimTypeRep a -> Comp (Arr Length a)
forall a b. a -> b -> a
const (Program CompCMD (Param2 Data PrimType') (Arr Length a)
-> Comp (Arr Length a)
forall a. Program CompCMD (Param2 Data PrimType') a -> Comp a
Comp (Program CompCMD (Param2 Data PrimType') (Arr Length a)
 -> Comp (Arr Length a))
-> Program CompCMD (Param2 Data PrimType') (Arr Length a)
-> Comp (Arr Length a)
forall a b. (a -> b) -> a -> b
$ String
-> Data Length
-> Program CompCMD (Param2 Data PrimType') (Arr Length 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)
Imp.newNamedArr String
base Data Length
l)) Struct PrimType' PrimTypeRep (Internal a)
forall a. Type a => TypeRep a
typeRep

-- | Create an array and initialize it with a constant list
constArr :: (PrimType (Internal a), MonadComp m)
    => [Internal a]  -- ^ Initial contents
    -> m (Arr a)
constArr :: [Internal a] -> m (Arr a)
constArr = String -> [Internal a] -> m (Arr a)
forall a (m :: * -> *).
(PrimType (Internal a), MonadComp m) =>
String -> [Internal a] -> m (Arr 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 :: (PrimType (Internal a), MonadComp m)
    => String        -- ^ Base name
    -> [Internal a]  -- ^ Initial contents
    -> m (Arr a)
constNamedArr :: String -> [Internal a] -> m (Arr a)
constNamedArr String
base [Internal a]
as =
    Comp (Arr a) -> m (Arr a)
forall (m :: * -> *) a. MonadComp m => Comp a -> m a
liftComp (Comp (Arr a) -> m (Arr a)) -> Comp (Arr a) -> m (Arr a)
forall a b. (a -> b) -> a -> b
$ (Arr Length (Internal a) -> Arr a)
-> Comp (Arr Length (Internal a)) -> Comp (Arr a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Data Length
-> Data Length
-> Struct PrimType' (Arr Length) (Internal a)
-> Arr a
forall a.
Data Length
-> Data Length
-> Struct PrimType' (Arr Length) (Internal a)
-> Arr a
Arr Data Length
0 Data Length
len (Struct PrimType' (Arr Length) (Internal a) -> Arr a)
-> (Arr Length (Internal a)
    -> Struct PrimType' (Arr Length) (Internal a))
-> Arr Length (Internal a)
-> Arr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arr Length (Internal a)
-> Struct PrimType' (Arr Length) (Internal a)
forall (pred :: * -> Constraint) a (con :: * -> *).
pred a =>
con a -> Struct pred con a
Single) (Comp (Arr Length (Internal a)) -> Comp (Arr a))
-> Comp (Arr Length (Internal a)) -> Comp (Arr a)
forall a b. (a -> b) -> a -> b
$ Program CompCMD (Param2 Data PrimType') (Arr Length (Internal a))
-> Comp (Arr Length (Internal a))
forall a. Program CompCMD (Param2 Data PrimType') a -> Comp a
Comp (Program CompCMD (Param2 Data PrimType') (Arr Length (Internal a))
 -> Comp (Arr Length (Internal a)))
-> Program
     CompCMD (Param2 Data PrimType') (Arr Length (Internal a))
-> Comp (Arr Length (Internal a))
forall a b. (a -> b) -> a -> b
$ String
-> [Internal a]
-> Program
     CompCMD (Param2 Data PrimType') (Arr Length (Internal 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)
Imp.constNamedArr String
base [Internal a]
as
  where
    len :: Data Length
len = Internal (Data Length) -> Data Length
forall a. Syntax a => Internal a -> a
value (Internal (Data Length) -> Data Length)
-> Internal (Data Length) -> Data Length
forall a b. (a -> b) -> a -> b
$ [Internal a] -> Length
forall i a. Num i => [a] -> i
genericLength [Internal a]
as

-- | Get an element of an array
getArr :: (Syntax a, MonadComp m) => Arr a -> Data Index -> m a
getArr :: Arr a -> Data Length -> m a
getArr Arr a
arr Data Length
i = do
    AssertionLabel -> Data Bool -> String -> m ()
forall (m :: * -> *).
MonadComp m =>
AssertionLabel -> Data Bool -> String -> m ()
assertLabel
      AssertionLabel
InternalAssertion
      (Data Length
i Data Length -> Data Length -> Data Bool
forall a. (Ord a, PrimType a) => Data a -> Data a -> Data Bool
< Arr a -> Data Length
forall a. Finite a => a -> Data Length
length Arr a
arr)
      String
"getArr: index out of bounds"
    Comp a -> m a
forall (m :: * -> *) a. MonadComp m => Comp a -> m a
liftComp
      (Comp a -> m a) -> Comp a -> m a
forall a b. (a -> b) -> a -> b
$ (Struct PrimType' Data (Internal a) -> a)
-> Comp (Struct PrimType' Data (Internal a)) -> Comp a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Struct PrimType' Data (Internal a) -> a
forall a b. (Syntax a, Syntax b, Internal a ~ Internal b) => a -> b
resugar
      (Comp (Struct PrimType' Data (Internal a)) -> Comp a)
-> Comp (Struct PrimType' Data (Internal a)) -> Comp a
forall a b. (a -> b) -> a -> b
$ (forall a. PrimType' a => Arr Length a -> Comp (Data a))
-> Struct PrimType' (Arr Length) (Internal a)
-> Comp (Struct PrimType' Data (Internal a))
forall (m :: * -> *) (pred :: * -> Constraint) (c1 :: * -> *)
       (c2 :: * -> *) b.
Applicative m =>
(forall a. pred a => c1 a -> m (c2 a))
-> Struct pred c1 b -> m (Struct pred c2 b)
mapStructA (Program CompCMD (Param2 Data PrimType') (Data a) -> Comp (Data a)
forall a. Program CompCMD (Param2 Data PrimType') a -> Comp a
Comp (Program CompCMD (Param2 Data PrimType') (Data a) -> Comp (Data a))
-> (Arr Length a
    -> Program CompCMD (Param2 Data PrimType') (Data a))
-> Arr Length a
-> Comp (Data a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arr Length a
 -> Data Length -> Program CompCMD (Param2 Data PrimType') (Data a))
-> Data Length
-> Arr Length a
-> Program CompCMD (Param2 Data PrimType') (Data a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Arr Length a
-> Data Length -> Program CompCMD (Param2 Data PrimType') (Data a)
forall (pred :: * -> Constraint) a i (exp :: * -> *)
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (m :: * -> *).
(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)
Imp.getArr (Data Length
i Data Length -> Data Length -> Data Length
forall a. Num a => a -> a -> a
+ Arr a -> Data Length
forall a. Arr a -> Data Length
arrOffset Arr a
arr))
      (Struct PrimType' (Arr Length) (Internal a)
 -> Comp (Struct PrimType' Data (Internal a)))
-> Struct PrimType' (Arr Length) (Internal a)
-> Comp (Struct PrimType' Data (Internal a))
forall a b. (a -> b) -> a -> b
$ Arr a -> Struct PrimType' (Arr Length) (Internal a)
forall a. Arr a -> Struct PrimType' (Arr Length) (Internal a)
unArr Arr a
arr

-- | Set an element of an array
setArr :: forall m a . (Syntax a, MonadComp m) =>
    Arr a -> Data Index -> a -> m ()
setArr :: Arr a -> Data Length -> a -> m ()
setArr Arr a
arr Data Length
i a
a = do
    AssertionLabel -> Data Bool -> String -> m ()
forall (m :: * -> *).
MonadComp m =>
AssertionLabel -> Data Bool -> String -> m ()
assertLabel
      AssertionLabel
InternalAssertion
      (Data Length
i Data Length -> Data Length -> Data Bool
forall a. (Ord a, PrimType a) => Data a -> Data a -> Data Bool
< Arr a -> Data Length
forall a. Finite a => a -> Data Length
length Arr a
arr)
      String
"setArr: index out of bounds"
    Comp () -> m ()
forall (m :: * -> *) a. MonadComp m => Comp a -> m a
liftComp
      (Comp () -> m ()) -> Comp () -> m ()
forall a b. (a -> b) -> a -> b
$ [Comp ()] -> Comp ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_
      ([Comp ()] -> Comp ()) -> [Comp ()] -> Comp ()
forall a b. (a -> b) -> a -> b
$ (forall a. PrimType' a => Data a -> Arr Length a -> Comp ())
-> Struct PrimType' Data (Internal a)
-> Struct PrimType' (Arr Length) (Internal a)
-> [Comp ()]
forall (pred :: * -> Constraint) (c1 :: * -> *) (c2 :: * -> *) b r.
(forall a. pred a => c1 a -> c2 a -> r)
-> Struct pred c1 b -> Struct pred c2 b -> [r]
zipListStruct
          (\Data a
a' Arr Length a
arr' -> Program CompCMD (Param2 Data PrimType') () -> Comp ()
forall a. Program CompCMD (Param2 Data PrimType') a -> Comp a
Comp (Program CompCMD (Param2 Data PrimType') () -> Comp ())
-> Program CompCMD (Param2 Data PrimType') () -> Comp ()
forall a b. (a -> b) -> a -> b
$ Arr Length a
-> Data Length
-> Data a
-> Program CompCMD (Param2 Data PrimType') ()
forall (pred :: * -> Constraint) a i
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (exp :: * -> *) (m :: * -> *).
(pred a, pred i, Integral i, Ix i, ArrCMD :<: instr) =>
Arr i a -> exp i -> exp a -> ProgramT instr (Param2 exp pred) m ()
Imp.setArr Arr Length a
arr' (Data Length
i Data Length -> Data Length -> Data Length
forall a. Num a => a -> a -> a
+ Arr a -> Data Length
forall a. Arr a -> Data Length
arrOffset Arr a
arr) Data a
a') Struct PrimType' Data (Internal a)
rep
      (Struct PrimType' (Arr Length) (Internal a) -> [Comp ()])
-> Struct PrimType' (Arr Length) (Internal a) -> [Comp ()]
forall a b. (a -> b) -> a -> b
$ Arr a -> Struct PrimType' (Arr Length) (Internal a)
forall a. Arr a -> Struct PrimType' (Arr Length) (Internal a)
unArr Arr a
arr
  where
    rep :: Struct PrimType' Data (Internal a)
rep = a -> Struct PrimType' Data (Internal a)
forall a b. (Syntax a, Syntax b, Internal a ~ Internal b) => a -> b
resugar a
a :: Struct PrimType' Data (Internal a)

-- | Copy the contents of an array to another array. The length of the
-- destination array must not be less than that of the source array.
--
-- In order to copy only a part of an array, use 'slice' before calling
-- 'copyArr'.
copyArr :: MonadComp m
    => Arr a  -- ^ Destination
    -> Arr a  -- ^ Source
    -> m ()
copyArr :: Arr a -> Arr a -> m ()
copyArr Arr a
arr1 Arr a
arr2 = do
    AssertionLabel -> Data Bool -> String -> m ()
forall (m :: * -> *).
MonadComp m =>
AssertionLabel -> Data Bool -> String -> m ()
assertLabel
      AssertionLabel
InternalAssertion
      (Arr a -> Data Length
forall a. Finite a => a -> Data Length
length Arr a
arr1 Data Length -> Data Length -> Data Bool
forall a. (Ord a, PrimType a) => Data a -> Data a -> Data Bool
>= Arr a -> Data Length
forall a. Finite a => a -> Data Length
length Arr a
arr2)
      String
"copyArr: destination too small"
    Comp () -> m ()
forall (m :: * -> *) a. MonadComp m => Comp a -> m a
liftComp (Comp () -> m ()) -> Comp () -> m ()
forall a b. (a -> b) -> a -> b
$ [Comp ()] -> Comp ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ ([Comp ()] -> Comp ()) -> [Comp ()] -> Comp ()
forall a b. (a -> b) -> a -> b
$
      (forall a. PrimType' a => Arr Length a -> Arr Length a -> Comp ())
-> Struct PrimType' (Arr Length) (Internal a)
-> Struct PrimType' (Arr Length) (Internal a)
-> [Comp ()]
forall (pred :: * -> Constraint) (c1 :: * -> *) (c2 :: * -> *) b r.
(forall a. pred a => c1 a -> c2 a -> r)
-> Struct pred c1 b -> Struct pred c2 b -> [r]
zipListStruct
        (\Arr Length a
a1 Arr Length a
a2 ->
            Program CompCMD (Param2 Data PrimType') () -> Comp ()
forall a. Program CompCMD (Param2 Data PrimType') a -> Comp a
Comp (Program CompCMD (Param2 Data PrimType') () -> Comp ())
-> Program CompCMD (Param2 Data PrimType') () -> Comp ()
forall a b. (a -> b) -> a -> b
$ (Arr Length a, Data Length)
-> (Arr Length a, Data Length)
-> Data Length
-> Program CompCMD (Param2 Data PrimType') ()
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 ()
Imp.copyArr
              (Arr Length a
a1, Arr a -> Data Length
forall a. Arr a -> Data Length
arrOffset Arr a
arr1)
              (Arr Length a
a2, Arr a -> Data Length
forall a. Arr a -> Data Length
arrOffset Arr a
arr2)
              (Arr a -> Data Length
forall a. Finite a => a -> Data Length
length Arr a
arr2)
        )
        (Arr a -> Struct PrimType' (Arr Length) (Internal a)
forall a. Arr a -> Struct PrimType' (Arr Length) (Internal a)
unArr Arr a
arr1)
        (Arr a -> Struct PrimType' (Arr Length) (Internal a)
forall a. Arr a -> Struct PrimType' (Arr Length) (Internal a)
unArr Arr a
arr2)

-- | Freeze a mutable array to an immutable one. This involves copying the array
-- to a newly allocated one.
freezeArr :: (Type (Internal a), MonadComp m) => Arr a -> m (IArr a)
freezeArr :: Arr a -> m (IArr a)
freezeArr Arr a
arr = Comp (IArr a) -> m (IArr a)
forall (m :: * -> *) a. MonadComp m => Comp a -> m a
liftComp (Comp (IArr a) -> m (IArr a)) -> Comp (IArr a) -> m (IArr a)
forall a b. (a -> b) -> a -> b
$ do
    Arr a
arr2 <- Data Length -> Comp (Arr a)
forall a (m :: * -> *).
(Type (Internal a), MonadComp m) =>
Data Length -> m (Arr a)
newArr (Arr a -> Data Length
forall a. Finite a => a -> Data Length
length Arr a
arr)
    Arr a -> Arr a -> Comp ()
forall (m :: * -> *) a. MonadComp m => Arr a -> Arr a -> m ()
copyArr Arr a
arr2 Arr a
arr
    Arr a -> Comp (IArr a)
forall (m :: * -> *) a. MonadComp m => Arr a -> m (IArr a)
unsafeFreezeArr Arr a
arr2
  -- This is better than calling `freezeArr` from imperative-edsl, since that
  -- one copies without offset.

-- | A version of 'freezeArr' that slices the array from 0 to the given length
freezeSlice :: (Type (Internal a), MonadComp m) =>
    Data Length -> Arr a -> m (IArr a)
freezeSlice :: Data Length -> Arr a -> m (IArr a)
freezeSlice Data Length
len = (IArr a -> IArr a) -> m (IArr a) -> m (IArr a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Data Length -> Data Length -> IArr a -> IArr a
forall a. Slicable a => Data Length -> Data Length -> a -> a
slice Data Length
0 Data Length
len) (m (IArr a) -> m (IArr a))
-> (Arr a -> m (IArr a)) -> Arr a -> m (IArr a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arr a -> m (IArr a)
forall a (m :: * -> *).
(Type (Internal a), MonadComp m) =>
Arr a -> m (IArr a)
freezeArr

-- | 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 :: MonadComp m => Arr a -> m (IArr a)
unsafeFreezeArr :: Arr a -> m (IArr a)
unsafeFreezeArr Arr a
arr
    = Comp (IArr a) -> m (IArr a)
forall (m :: * -> *) a. MonadComp m => Comp a -> m a
liftComp
    (Comp (IArr a) -> m (IArr a)) -> Comp (IArr a) -> m (IArr a)
forall a b. (a -> b) -> a -> b
$ (Struct PrimType' (IArr Length) (Internal a) -> IArr a)
-> Comp (Struct PrimType' (IArr Length) (Internal a))
-> Comp (IArr a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Data Length
-> Data Length
-> Struct PrimType' (IArr Length) (Internal a)
-> IArr a
forall a.
Data Length
-> Data Length
-> Struct PrimType' (IArr Length) (Internal a)
-> IArr a
IArr (Arr a -> Data Length
forall a. Arr a -> Data Length
arrOffset Arr a
arr) (Arr a -> Data Length
forall a. Finite a => a -> Data Length
length Arr a
arr))
    (Comp (Struct PrimType' (IArr Length) (Internal a))
 -> Comp (IArr a))
-> Comp (Struct PrimType' (IArr Length) (Internal a))
-> Comp (IArr a)
forall a b. (a -> b) -> a -> b
$ (forall a. PrimType' a => Arr Length a -> Comp (IArr Length a))
-> Struct PrimType' (Arr Length) (Internal a)
-> Comp (Struct PrimType' (IArr Length) (Internal a))
forall (m :: * -> *) (pred :: * -> Constraint) (c1 :: * -> *)
       (c2 :: * -> *) b.
Applicative m =>
(forall a. pred a => c1 a -> m (c2 a))
-> Struct pred c1 b -> m (Struct pred c2 b)
mapStructA (Program CompCMD (Param2 Data PrimType') (IArr Length a)
-> Comp (IArr Length a)
forall a. Program CompCMD (Param2 Data PrimType') a -> Comp a
Comp (Program CompCMD (Param2 Data PrimType') (IArr Length a)
 -> Comp (IArr Length a))
-> (Arr Length a
    -> Program CompCMD (Param2 Data PrimType') (IArr Length a))
-> Arr Length a
-> Comp (IArr Length a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arr Length a
-> Program CompCMD (Param2 Data PrimType') (IArr Length 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)
Imp.unsafeFreezeArr)
    (Struct PrimType' (Arr Length) (Internal a)
 -> Comp (Struct PrimType' (IArr Length) (Internal a)))
-> Struct PrimType' (Arr Length) (Internal a)
-> Comp (Struct PrimType' (IArr Length) (Internal a))
forall a b. (a -> b) -> a -> b
$ Arr a -> Struct PrimType' (Arr Length) (Internal a)
forall a. Arr a -> Struct PrimType' (Arr Length) (Internal a)
unArr Arr a
arr

-- | A version of 'unsafeFreezeArr' that slices the array from 0 to the given
-- length
unsafeFreezeSlice :: MonadComp m => Data Length -> Arr a -> m (IArr a)
unsafeFreezeSlice :: Data Length -> Arr a -> m (IArr a)
unsafeFreezeSlice Data Length
len = (IArr a -> IArr a) -> m (IArr a) -> m (IArr a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Data Length -> Data Length -> IArr a -> IArr a
forall a. Slicable a => Data Length -> Data Length -> a -> a
slice Data Length
0 Data Length
len) (m (IArr a) -> m (IArr a))
-> (Arr a -> m (IArr a)) -> Arr a -> m (IArr a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arr a -> m (IArr a)
forall (m :: * -> *) a. MonadComp m => Arr a -> m (IArr a)
unsafeFreezeArr

-- | Thaw an immutable array to a mutable one. This involves copying the array
-- to a newly allocated one.
thawArr :: (Type (Internal a), MonadComp m) => IArr a -> m (Arr a)
thawArr :: IArr a -> m (Arr a)
thawArr IArr a
arr = Comp (Arr a) -> m (Arr a)
forall (m :: * -> *) a. MonadComp m => Comp a -> m a
liftComp (Comp (Arr a) -> m (Arr a)) -> Comp (Arr a) -> m (Arr a)
forall a b. (a -> b) -> a -> b
$ do
    Arr a
arr2 <- IArr a -> Comp (Arr a)
forall (m :: * -> *) a. MonadComp m => IArr a -> m (Arr a)
unsafeThawArr IArr a
arr
    Arr a
arr3 <- Data Length -> Comp (Arr a)
forall a (m :: * -> *).
(Type (Internal a), MonadComp m) =>
Data Length -> m (Arr a)
newArr (IArr a -> Data Length
forall a. Finite a => a -> Data Length
length IArr a
arr)
    Arr a -> Arr a -> Comp ()
forall (m :: * -> *) a. MonadComp m => Arr a -> Arr a -> m ()
copyArr Arr a
arr3 Arr a
arr2
    Arr a -> Comp (Arr a)
forall (m :: * -> *) a. Monad m => a -> m a
return Arr 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 :: MonadComp m => IArr a -> m (Arr a)
unsafeThawArr :: IArr a -> m (Arr a)
unsafeThawArr IArr a
arr
    = Comp (Arr a) -> m (Arr a)
forall (m :: * -> *) a. MonadComp m => Comp a -> m a
liftComp
    (Comp (Arr a) -> m (Arr a)) -> Comp (Arr a) -> m (Arr a)
forall a b. (a -> b) -> a -> b
$ (Struct PrimType' (Arr Length) (Internal a) -> Arr a)
-> Comp (Struct PrimType' (Arr Length) (Internal a))
-> Comp (Arr a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Data Length
-> Data Length
-> Struct PrimType' (Arr Length) (Internal a)
-> Arr a
forall a.
Data Length
-> Data Length
-> Struct PrimType' (Arr Length) (Internal a)
-> Arr a
Arr (IArr a -> Data Length
forall a. IArr a -> Data Length
iarrOffset IArr a
arr) (IArr a -> Data Length
forall a. Finite a => a -> Data Length
length IArr a
arr))
    (Comp (Struct PrimType' (Arr Length) (Internal a)) -> Comp (Arr a))
-> Comp (Struct PrimType' (Arr Length) (Internal a))
-> Comp (Arr a)
forall a b. (a -> b) -> a -> b
$ (forall a. PrimType' a => IArr Length a -> Comp (Arr Length a))
-> Struct PrimType' (IArr Length) (Internal a)
-> Comp (Struct PrimType' (Arr Length) (Internal a))
forall (m :: * -> *) (pred :: * -> Constraint) (c1 :: * -> *)
       (c2 :: * -> *) b.
Applicative m =>
(forall a. pred a => c1 a -> m (c2 a))
-> Struct pred c1 b -> m (Struct pred c2 b)
mapStructA (Program CompCMD (Param2 Data PrimType') (Arr Length a)
-> Comp (Arr Length a)
forall a. Program CompCMD (Param2 Data PrimType') a -> Comp a
Comp (Program CompCMD (Param2 Data PrimType') (Arr Length a)
 -> Comp (Arr Length a))
-> (IArr Length a
    -> Program CompCMD (Param2 Data PrimType') (Arr Length a))
-> IArr Length a
-> Comp (Arr Length a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IArr Length a
-> Program CompCMD (Param2 Data PrimType') (Arr Length 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)
Imp.unsafeThawArr)
    (Struct PrimType' (IArr Length) (Internal a)
 -> Comp (Struct PrimType' (Arr Length) (Internal a)))
-> Struct PrimType' (IArr Length) (Internal a)
-> Comp (Struct PrimType' (Arr Length) (Internal a))
forall a b. (a -> b) -> a -> b
$ IArr a -> Struct PrimType' (IArr Length) (Internal a)
forall a. IArr a -> Struct PrimType' (IArr Length) (Internal a)
unIArr IArr a
arr

-- | Create an immutable array and initialize it with a constant list
constIArr :: (PrimType (Internal a), MonadComp m) =>
    [Internal a] -> m (IArr a)
constIArr :: [Internal a] -> m (IArr a)
constIArr = [Internal a] -> m (Arr a)
forall a (m :: * -> *).
(PrimType (Internal a), MonadComp m) =>
[Internal a] -> m (Arr a)
constArr ([Internal a] -> m (Arr a))
-> (Arr a -> m (IArr a)) -> [Internal a] -> m (IArr a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Arr a -> m (IArr a)
forall (m :: * -> *) a. MonadComp m => Arr a -> m (IArr a)
unsafeFreezeArr



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

-- | Conditional statement that returns an expression
ifE :: (Syntax a, MonadComp m)
    => Data Bool  -- ^ Condition
    -> m a        -- ^ True branch
    -> m a        -- ^ False branch
    -> m a
ifE :: Data Bool -> m a -> m a -> m a
ifE Data Bool
c m a
t m a
f = do
    Ref a
res <- m (Ref a)
forall a (m :: * -> *). (Syntax a, MonadComp m) => m (Ref a)
newRef
    Data Bool -> m () -> m () -> m ()
forall (m :: * -> *).
MonadComp m =>
Data Bool -> m () -> m () -> m ()
iff Data Bool
c (m a
t m a -> (a -> m ()) -> m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Ref a -> a -> m ()
forall a (m :: * -> *).
(Syntax a, MonadComp m) =>
Ref a -> a -> m ()
setRef Ref a
res) (m a
f m a -> (a -> m ()) -> m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Ref a -> a -> m ()
forall a (m :: * -> *).
(Syntax a, MonadComp m) =>
Ref a -> a -> m ()
setRef Ref a
res)
    Ref a -> m a
forall a (m :: * -> *). (Syntax a, MonadComp m) => Ref a -> m a
unsafeFreezeRef Ref a
res

-- | Break out from a loop
break :: MonadComp m => m ()
break :: m ()
break = Comp () -> m ()
forall (m :: * -> *) a. MonadComp m => Comp a -> m a
liftComp (Comp () -> m ()) -> Comp () -> m ()
forall a b. (a -> b) -> a -> b
$ Program CompCMD (Param2 Data PrimType') () -> Comp ()
forall a. Program CompCMD (Param2 Data PrimType') a -> Comp a
Comp Program CompCMD (Param2 Data PrimType') ()
forall (instr :: (* -> *, (* -> *, (* -> Constraint, *)))
                 -> * -> *)
       (exp :: * -> *) (pred :: * -> Constraint) (m :: * -> *).
(ControlCMD :<: instr) =>
ProgramT instr (Param2 exp pred) m ()
Imp.break

-- | Assertion (with implicit label @`UserAssertion` ""@)
assert :: MonadComp m
    => Data Bool  -- ^ Expression that should be true
    -> String     -- ^ Message in case of failure
    -> m ()
assert :: Data Bool -> String -> m ()
assert = AssertionLabel -> Data Bool -> String -> m ()
forall (m :: * -> *).
MonadComp m =>
AssertionLabel -> Data Bool -> String -> m ()
assertLabel (AssertionLabel -> Data Bool -> String -> m ())
-> AssertionLabel -> Data Bool -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String -> AssertionLabel
UserAssertion String
""

-- | Like 'assert' but tagged with an explicit assertion label
assertLabel :: MonadComp m
    => AssertionLabel  -- ^ Assertion label
    -> Data Bool       -- ^ Expression that should be true
    -> String          -- ^ Message in case of failure
    -> m ()
assertLabel :: AssertionLabel -> Data Bool -> String -> m ()
assertLabel AssertionLabel
c Data Bool
cond String
msg =
    Comp () -> m ()
forall (m :: * -> *) a. MonadComp m => Comp a -> m a
liftComp (Comp () -> m ()) -> Comp () -> m ()
forall a b. (a -> b) -> a -> b
$ Program CompCMD (Param2 Data PrimType') () -> Comp ()
forall a. Program CompCMD (Param2 Data PrimType') a -> Comp a
Comp (Program CompCMD (Param2 Data PrimType') () -> Comp ())
-> Program CompCMD (Param2 Data PrimType') () -> Comp ()
forall a b. (a -> b) -> a -> b
$ AssertCMD
  '(ProgramT CompCMD (Param2 Data PrimType') Identity,
    Param2 Data PrimType')
  ()
-> Program CompCMD (Param2 Data PrimType') ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
Oper.singleInj (AssertCMD
   '(ProgramT CompCMD (Param2 Data PrimType') Identity,
     Param2 Data PrimType')
   ()
 -> Program CompCMD (Param2 Data PrimType') ())
-> AssertCMD
     '(ProgramT CompCMD (Param2 Data PrimType') Identity,
       Param2 Data PrimType')
     ()
-> Program CompCMD (Param2 Data PrimType') ()
forall a b. (a -> b) -> a -> b
$ AssertionLabel
-> Data Bool
-> String
-> AssertCMD
     '(ProgramT CompCMD (Param2 Data PrimType') Identity,
       Param2 Data PrimType')
     ()
forall k k2 (exp :: * -> *) (prog :: k) (pred :: k2).
AssertionLabel
-> exp Bool -> String -> AssertCMD (Param3 prog exp pred) ()
Assert AssertionLabel
c Data Bool
cond String
msg



----------------------------------------
-- ** Misc.
----------------------------------------

-- | Force evaluation of a value and share the result (monadic version of
-- 'share')
shareM :: (Syntax a, MonadComp m) => a -> m a
shareM :: a -> m a
shareM = a -> m (Ref a)
forall a (m :: * -> *). (Syntax a, MonadComp m) => a -> m (Ref a)
initRef (a -> m (Ref a)) -> (Ref a -> m a) -> a -> m a
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Ref a -> m a
forall a (m :: * -> *). (Syntax a, MonadComp m) => Ref a -> m a
unsafeFreezeRef
  -- This function is more commonly needed than `share`, since code motion
  -- doesn't work across monadic binds.