{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
module Cond where
import Ivory.Language
import Ivory.Compile.C.CmdlineFrontend
import Prelude hiding (exp)
add :: Def ('[Uint32,Uint32] ':-> Uint32)
add = proc "add"
$ \ x y -> ensures (\r -> r ==? x + y)
$ body
$ ret (x + y)
cmodule :: Module
cmodule = package "cond" $ incl add
-- Testing assertions with choice expression
foo :: Def ('[IFloat,IFloat,IFloat] ':-> IFloat)
foo = proc "foo" $ \x y z -> body $ do
let cond = 2/x ==? 5
let tCond = 6/y ==? 7
let exp = tCond ? (8/z, 9)
ret (cond ? (exp,4))
fooMod :: Module
fooMod = package "fooM" $ incl foo
runFoo :: IO ()
runFoo = runCompiler [fooMod] []
initialOpts { outDir = Nothing
, divZero = True
}