ivory-examples (empty) → 0.1.0.0
raw patch · 19 files changed
+860/−0 lines, 19 filesdep +QuickCheckdep +basedep +ivorysetup-changed
Dependencies added: QuickCheck, base, ivory, ivory-backend-c, ivory-opts, ivory-quickcheck, ivory-stdlib, mainland-pretty, monadLib, pretty, template-haskell, wl-pprint
Files
- LICENSE +30/−0
- Setup.hs +2/−0
- examples/AddrOfRegression.hs +86/−0
- examples/Area.hs +41/−0
- examples/Bits.hs +78/−0
- examples/Cond.hs +34/−0
- examples/Factorial.hs +25/−0
- examples/FibLoop.hs +71/−0
- examples/FibTutorial.hs +26/−0
- examples/Float.hs +21/−0
- examples/Forever.hs +37/−0
- examples/FunPtr.hs +25/−0
- examples/PID.hs +82/−0
- examples/PublicPrivate.hs +46/−0
- examples/QC.hs +72/−0
- examples/SizeOf.hs +28/−0
- examples/String.hs +28/−0
- examples/TestClang.hs +60/−0
- ivory-examples.cabal +68/−0
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c)2013, Galois, Inc++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Galois, Inc nor the names of its contributors+ may be used to endorse or promote products derived from this software+ without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ examples/AddrOfRegression.hs view
@@ -0,0 +1,86 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}++module AddrOfRegression where++import Ivory.Language++[ivory|+struct param_info+ { param_requested :: Stored Uint8+ ; other :: Stored Uint16+ }+|]++test1 :: ModuleDef+test1 = do+ defMemArea param_info_area+ incl t1+ where+ param_info_area :: MemArea (Array 512 (Struct "param_info"))+ param_info_area = area "g_param_info" Nothing++ param_info_ref :: Ref Global (Array 512 (Struct "param_info"))+ param_info_ref = addrOf param_info_area++ t1 :: Def ('[]:->())+ t1 = proc "t1" $ body $ do+ arrayMap $ \ix ->+ store ((param_info_ref ! ix) ~> param_requested) 1++test1_noarray :: ModuleDef+test1_noarray = do+ defMemArea param_info_area+ incl t1+ where+ param_info_area :: MemArea (Struct "param_info")+ param_info_area = area "single_param_info" Nothing++ param_info_ref :: Ref Global (Struct "param_info")+ param_info_ref = addrOf param_info_area++ t1 :: Def ('[]:->())+ t1 = proc "t1_noarray" $ body $ do+ store (param_info_ref ~> param_requested) 1++test2 :: ModuleDef+test2 = do+ defMemArea atom_array_area+ incl t2+ where+ atom_array_area :: MemArea (Array 512 (Stored IFloat))+ atom_array_area = area "atom_array" Nothing++ atom_array_ref :: Ref Global (Array 512 (Stored IFloat))+ atom_array_ref = addrOf atom_array_area++ t2 :: Def ('[]:->())+ t2 = proc "t2" $ body $ do+ arrayMap $ \ix ->+ store (atom_array_ref ! ix) 1++test3 :: ModuleDef+test3 = do+ incl t3+ where+ t3 :: Def ('[]:->())+ t3 = proc "t3" $ body $ do+ (stack_array :: Ref (Stack s) (Array 512 (Stored IFloat))) <- local izero+ arrayMap $ \ix ->+ store (stack_array ! ix) 1+++cmodule :: Module+cmodule = package "AddrOfRegression" $ do+ defStruct (Proxy :: Proxy "param_info")+ test1+ test1_noarray+ test2+ test3+++
+ examples/Area.hs view
@@ -0,0 +1,41 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE QuasiQuotes #-}++module Area where++import Ivory.Language+++[ivory|++struct val {+ field :: Stored Uint32+}++|]++val :: MemArea (Struct "val")+val = area "val" (Just (istruct [field .= ival 0]))++cval :: ConstMemArea (Struct "val")+cval = constArea "cval" (istruct [field .= ival 10])++getVal :: Def ('[] :-> Uint32)+getVal = proc "getVal" $ body $ do+ ret =<< deref (addrOf val ~> field)++setVal :: Def ('[Uint32] :-> ())+setVal = proc "setVal" $ \ n -> body $ do+ store (addrOf val ~> field) n+ retVoid++cmodule :: Module+cmodule = package "Area" $ do+ incl getVal+ incl setVal+ defMemArea val+ defConstMemArea cval+ defStruct (Proxy :: Proxy "val")
+ examples/Bits.hs view
@@ -0,0 +1,78 @@+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE DataKinds #-}++module Bits (runBits, cmodule) where++import Ivory.Compile.C.CmdlineFrontend+import Ivory.Language+import MonadLib.Monads (runState, sets)++runBits :: IO ()+runBits = runCompiler [cmodule] initialOpts {stdOut = True}++cmodule :: Module+cmodule = package "Bits" $ do+ incl test1+ incl test2+ incl test3+ incl test4++test1 :: Def ('[Uint8, Uint16, Uint32, Uint64] :-> Uint64)+test1 = proc "test1" $ \u8 u16 u32 u64 -> body $ do+ a <- assign $ u8 .& 0xFF+ b <- assign $ u16 .& 0xFF00+ c <- assign $ u32 .& 0xFF0000+ d <- assign $ u64 .& 0xFF000000+ ret $ (safeCast a) .| (safeCast b) .| (safeCast c) .| d++-- | Convert an array of four 8-bit integers into a 32-bit integer.+test2 :: Def ('[Ref s (Array 4 (Stored Uint8))] :-> Uint32)+test2 = proc "test2" $ \arr -> body $ do+ a <- deref (arr ! 0)+ b <- deref (arr ! 1)+ c <- deref (arr ! 2)+ d <- deref (arr ! 3)+ ret $ ((safeCast a) `iShiftL` 24) .|+ ((safeCast b) `iShiftL` 16) .|+ ((safeCast c) `iShiftL` 8) .|+ ((safeCast d) `iShiftL` 0)++-- | Example of using "extractByte" with a state monad.+extractUint32 :: Uint32 -> (Uint8, Uint8, Uint8, Uint8)+extractUint32 x = fst $ runState x $ do+ a <- sets extractByte+ b <- sets extractByte+ c <- sets extractByte+ d <- sets extractByte+ return (a, b, c, d)++-- | Convert a 32-bit integer to an array of 8-bit integers.+test3 :: Def ('[Uint32, Ref s (Array 4 (Stored Uint8))] :-> ())+test3 = proc "test3" $ \n arr -> body $ do+ let (a, b, c, d) = extractUint32 n+ store (arr ! 0) d+ store (arr ! 1) c+ store (arr ! 2) b+ store (arr ! 3) a++setBit :: (IvoryBits a, IvoryStore a)+ => (Ref s (Stored a)) -> Int -> Ivory eff ()+setBit ref bit = do+ val <- deref ref+ store ref (val .| (1 `iShiftL` (fromIntegral bit)))++clearBit :: (IvoryBits a, IvoryStore a)+ => (Ref s (Stored a)) -> Int -> Ivory eff ()+clearBit ref bit = do+ val <- deref ref+ store ref (val .& (iComplement (1 `iShiftL` (fromIntegral bit))))++test4 :: Def ('[] :-> Uint32)+test4 = proc "test4" $ body $ do+ n <- local (ival 0)+ setBit n 1+ setBit n 3+ setBit n 5+ setBit n 8+ clearBit n 3+ ret =<< deref n
+ examples/Cond.hs view
@@ -0,0 +1,34 @@+{-# 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 { stdOut = True+ , divZero = True+ }
+ examples/Factorial.hs view
@@ -0,0 +1,25 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeOperators #-}++module Factorial where++import Ivory.Language+import Ivory.Compile.C.CmdlineFrontend++factorial :: Def ('[Sint32] :-> Sint32)+factorial = proc "factorial" $ \ n ->+ -- These are made up requires/ensures for testing purposes.+ ensures (\r -> n <? r) $+ body $+ ifte_ (n >? 1)+ (do n' <- call factorial (n - 1)+ ret (n' * n)+ )+ (do ret n+ )++cmodule :: Module+cmodule = package "Factorial" $ incl factorial++runFactorial :: IO ()+runFactorial = runCompiler [cmodule] initialOpts { stdOut = True }
+ examples/FibLoop.hs view
@@ -0,0 +1,71 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeOperators #-}++module FibLoop where++import Ivory.Compile.C.CmdlineFrontend+import Ivory.Language++import Control.Applicative ((<$>),(<*>))++-- Recursive implementation of fib+fib_rec :: Def ('[Uint32] :-> Uint64)+fib_rec = proc "fib_rec" (\n -> body (ret =<< call fib_rec_aux 0 1 n))++fib_rec_aux :: Def ('[Uint32,Uint32,Uint32] :-> Uint64)+fib_rec_aux = proc "fib_rec_aux" $ \ a b n -> body $ do+ ifte_ (n ==? 0)+ (ret (safeCast a))+ (ret . safeCast =<< call fib_rec_aux b (a + b) (n - 1))++-- Loop implementation of fib.++fib_loop :: Def ('[Ix 1000] :-> Uint32)+fib_loop = proc "fib_loop" $ \ n -> body $ do+ a <- local (ival 0)+ b <- local (ival 0)++ n `times` \ _ -> do+ a' <- deref a+ b' <- deref b+ store a b'+ store b (a' + b')++ result <- deref a+ ret result++-- Loop implementation of fib, using a structure instead+-- of two discrete variables.+[ivory|+struct Fibstate+ { sa :: Stored Uint32+ ; sb :: Stored Uint32+ }+|]++fib_struct_loop :: Def ('[Ix 1000] :-> Uint32)+fib_struct_loop = proc "fib_struct_loop" $ \ n -> body $ do+ state <- local (istruct [ sa .= ival 0 , sb .= ival 0 ])++ let update = (+) <$> deref (state ~> sa) <*> deref (state ~> sb)++ n `times` \ _ -> do+ store (state ~> sa) =<< deref (state ~> sb)+ store (state ~> sb) =<< update++ ret =<< deref (state ~> sa)++cmodule :: Module+cmodule = package "FibLoop" $ do+ incl fib_rec+ incl fib_rec_aux+ incl fib_loop++ defStruct (Proxy :: Proxy "Fibstate")+ incl fib_struct_loop++runFibLoop :: IO ()+runFibLoop = runCompiler [cmodule] initialOpts { stdOut = True, constFold = True }
+ examples/FibTutorial.hs view
@@ -0,0 +1,26 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeOperators #-}++import Ivory.Language+import qualified Ivory.Compile.C.CmdlineFrontend as C (compile)++fib_loop :: Def ('[Ix 1000] :-> Uint32)+fib_loop = proc "fib_loop" $ \ n -> body $ do+ a <- local (ival 0)+ b <- local (ival 1)++ n `times` \ _ -> do+ a' <- deref a+ b' <- deref b+ store a b'+ store b (a' + b')++ result <- deref a+ ret result++fib_tutorial_module :: Module+fib_tutorial_module = package "fib_tutorial" $ do+ incl fib_loop++main :: IO ()+main = C.compile [ fib_tutorial_module ]
+ examples/Float.hs view
@@ -0,0 +1,21 @@+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE DataKinds #-}++module Float (runFloat,cmodule) where++import Ivory.Compile.C.CmdlineFrontend+import Ivory.Language++runFloat :: IO ()+runFloat = runCompiler [cmodule] initialOpts { stdOut = True }++cmodule :: Module+cmodule = package "Float" $ do+ incl test1+ incl test2++test1 :: Def ('[IFloat] :-> Sint32)+test1 = proc "test1" (\ f -> body (ret (castDefault f)))++test2 :: Def ('[Sint32] :-> IFloat)+test2 = proc "test2" (\ i -> body (ret (safeCast i)))
+ examples/Forever.hs view
@@ -0,0 +1,37 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeOperators #-}++module Forever where++import Ivory.Language+import Ivory.Compile.C.CmdlineFrontend++factorial :: Def ('[Sint32] :-> Sint32)+factorial = proc "factorial" $ \ n ->+ -- These are made up requires/ensures for testing purposes.+ ensures (\r -> n <? r) $ body $ do+ ifte_ (n >? 1)+ (do n' <- call factorial (n - 1)+ ret (n' * n)+ )+ (do ret n+ )++printResult :: Def ('[Sint32] :-> ())+printResult = proc "print_result" $ \_ -> body retVoid++foreverFactorial :: Def ('[Sint32] :-> ())+foreverFactorial = proc "forever_factorial" $ \ n -> body $ do+ forever $ do+ res <- call factorial n+ call_ printResult res++cmodule :: Module+cmodule = package "Forever" $ do+ incl factorial+ incl printResult+ incl foreverFactorial++runFactorial :: IO ()+runFactorial = runCompiler [cmodule] initialOpts { stdOut = True }+
+ examples/FunPtr.hs view
@@ -0,0 +1,25 @@+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE DataKinds #-}++module FunPtr where++import Ivory.Compile.C.CmdlineFrontend+import Ivory.Language++f :: Def ('[Sint32] :-> Sint32)+f = proc "f" (\ n -> body (ret (n + 1)))++invoke :: Def ('[ ProcPtr ('[Sint32] :-> Sint32), Sint32] :-> Sint32)+invoke = proc "invoke" (\ k n -> body (ret =<< indirect k n))++test :: Def ('[] :-> Sint32)+test = proc "test" (body (ret =<< call invoke (procPtr f) 10))++runFunPtr :: IO ()+runFunPtr = runCompiler [cmodule] initialOpts { stdOut = True }++cmodule :: Module+cmodule = package "FunPtr" $ do+ incl f+ incl test+ incl invoke
+ examples/PID.hs view
@@ -0,0 +1,82 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE FlexibleInstances #-}++module PID where++import Ivory.Compile.C.CmdlineFrontend+import Ivory.Language++[ivory|++struct PID+ { pid_mv :: Stored IFloat+ ; pid_i :: Stored IFloat+ ; pid_err :: Stored IFloat+ }++|]++type SP = IFloat -- Set point+type PV = IFloat -- Process (measured) value+type Time = IFloat++{-+void pid_update(struct PID * pid,+ sp_t sp,+ pv_t pv,+ timeinc_t dt+ )+{+ float err = sp - pv;+ float i = pid->i + err*dt;+ float d = (err - pid->err) / dt;+ pid->i = ki*i;+ pid->mv = kp*err + pid->i + kd*d;+ pid->err = err;+ return;+}+-}++kp, ki, kd :: IFloat+kp = 1.0+ki = 0.1+kd = 0.1++pidUpdate :: Def ('[ Ref s (Struct "PID")+ , SP+ , PV+ , Time ]+ :-> IFloat)+pidUpdate = proc "pid_update" $+ \ pid sp pv dt ->+ -- These are made up requires/ensures for testing purposes.+ requires (checkStored (pid ~> pid_err) (\err -> err <? 1))+ $ ensures (\res -> checkStored (pid ~> pid_err) (\err -> err <? res))+ $ body+ $ do+ err <- assign (sp - pv)+ i <- deref $ pid ~> pid_i+ i' <- assign $ ki * (i + err*dt)+ prevErr <- deref $ pid ~> pid_err+ d <- assign $ (err - prevErr) / dt+ store (pid ~> pid_i) i'+ store (pid ~> pid_mv) (kp*err + i' + kd*d)+ store (pid ~> pid_err) err+ ret err++runPID :: IO ()+runPID = runCompiler [cmodule] initialOpts { stdOut = True }++cmodule :: Module+cmodule = package "PID" $ do+ defStruct (Proxy :: Proxy "PID")+ incl pidUpdate+ incl alloc_test++alloc_test :: Def ('[] :-> IFloat)+alloc_test = proc "alloc_test" $ body $ do+ pid <- local (istruct [pid_i .= ival 1])+ ret =<< deref (pid ~> pid_i)
+ examples/PublicPrivate.hs view
@@ -0,0 +1,46 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE OverloadedStrings #-}++module PublicPrivate where++import Ivory.Language+import Ivory.Compile.C.CmdlineFrontend+++[ivory|+struct Foo { i :: Stored Uint32 }+struct Bar { name :: Array 32 (Stored IChar) }+|]++privateHelper1 :: Def ('[Ref s (Struct "Foo")] :-> Ref s (Stored Uint32))+privateHelper1 = proc "private_helper1" (\s -> body (ret (s ~> i)))++privateHelper2 :: Def ('[] :-> ())+privateHelper2 = proc "private_helper2" $ body retVoid++publicFunction :: Def ('[Ref s (Struct "Bar")] :-> Uint32)+publicFunction = proc "public_function" $ \_ -> body $ do+ a <- call privateHelper1 (addrOf privateFoo)+ call_ privateHelper2+ ret =<< deref a++privateFoo :: MemArea (Struct "Foo")+privateFoo = area "private_foo" Nothing++cmodule :: Module+cmodule = package "PublicPrivate" $ do+ private $ do+ defStruct (Proxy :: Proxy "Foo")+ defMemArea privateFoo+ incl privateHelper1+ incl privateHelper2+ public $ do+ defStruct (Proxy :: Proxy "Bar")+ incl publicFunction++runPublicPrivate :: IO ()+runPublicPrivate = runCompiler [cmodule] initialOpts { stdOut = True, constFold = True }
+ examples/QC.hs view
@@ -0,0 +1,72 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE FlexibleInstances #-}++module QC where++import Ivory.Compile.C.CmdlineFrontend+import Ivory.Language+import Ivory.QuickCheck+import Test.QuickCheck.Arbitrary++[ivory|+struct foo+ { foo_a :: Stored IFloat+ ; foo_b :: Stored Uint8+ }+|]++-- Function we want to generate inputs for.+func :: Def ('[Uint8+ , Ref s (Array 3 (Stored Uint8))+ , Ref s (Struct "foo")+ ] :-> ())+func = proc "func" $ \u arr str -> body $+ arrayMap $ \ix -> do+ a <- deref (arr ! ix)+ b <- deref (str ~> foo_b)+ store (arr ! ix) (a + b + u)++type DriverDef = Def ('[] :-> ())++-- Driver function. Takes lists of the arguments we'll pass to the function+-- test.+driver :: [Uint8]+ -> [Init (Array 3 (Stored Uint8))]+ -> [Init (Struct "foo")]+ -> DriverDef+driver as0 as1 as2 = proc "main" $ body $ do+ mapM_ oneCall (zip3 as0 as1 as2)++ where+ oneCall (a0, a1, a2) = do+ a1' <- local a1+ a2' <- local a2+ call_ func a0 a1' a2'++-- Generate the random values to pass.+runTest :: IvoryGen DriverDef+runTest = do+ args0 <- samples num arbitrary+ args1 <- samples num arbitrary+ aFoos <- samples num foo_a+ bFoos <- samples num foo_b+ return $ driver args0 args1 (zipWith foo aFoos bFoos)+ where+ foo a b = istruct [ a, b ]+ num = 10++-- Compile!+runTests :: IO ()+runTests = do+ d <- runIO runTest+ runCompiler [cmodule d] initialOpts { includeDir = "test"+ , srcDir = "test"+ , constFold = True+ }+ where+ cmodule d = package "qc" $ do+ incl d+ incl func
+ examples/SizeOf.hs view
@@ -0,0 +1,28 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE DataKinds #-}++{-# OPTIONS_GHC -fno-warn-orphans #-}++module SizeOf where++import Ivory.Language++[ivory|++struct foo+ { f1 :: Stored Uint8+ ; f2 :: Stored Uint32+ }++|]+++test :: Def ('[] :-> Uint8)+test = proc "test" (body (ret (sizeOf (Proxy :: Proxy (Struct "foo")))))++cmodule :: Module+cmodule = package "SizeOf" $ do+ defStruct (Proxy :: Proxy "foo")+ incl test
+ examples/String.hs view
@@ -0,0 +1,28 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeOperators #-}++module String where++import Ivory.Language+import Ivory.Compile.C.CmdlineFrontend++printf :: Def ('[IString] :-> Sint32)+printf = importProc "printf" "stdio.h"++printf2 :: Def ('[IString,Sint32] :-> Sint32)+printf2 = importProc "printf" "stdio.h"++test :: Def ('[] :-> ())+test = proc "test" $ body $ do+ call_ printf "Hello, world\n"+ call_ printf2 "howdy, %i \n" 3+ retVoid++runString :: IO ()+runString = runCompiler [cmodule] initialOpts { stdOut = True }++cmodule :: Module+cmodule = package "String" $ do+ incl printf+ incl test
+ examples/TestClang.hs view
@@ -0,0 +1,60 @@+import System.Environment++import qualified PID+import qualified FibLoop+import qualified Factorial+import qualified String+import qualified FunPtr+import qualified Overflow+import qualified Float+import qualified Alloc+import qualified Area+import qualified Cond+import qualified Forever+import qualified PublicPrivate+import qualified Bits+import qualified SizeOf+import qualified AddrOfRegression+import qualified Array++import Ivory.Compile.C.CmdlineFrontend+import Ivory.Language (Module(),moduleName)+import Ivory.Stdlib (stdlibModules)++import qualified Ivory.Stdlib.SearchDir as S++main :: IO ()+main = do+ args <- getArgs+ let path = head args+ let opts = initialOpts { includeDir = path, srcDir = path+ , rtIncludeDir = Nothing }++ mapM_ (compileExample opts) modules++ putStrLn "Compiling: Overflow"+ Overflow.writeOverflow opts++compileExample :: Opts -> Module -> IO ()+compileExample opts m = do+ putStrLn ("Compiling: " ++ moduleName m)+ runCompilerWith Nothing (Just [S.searchDir]) [m] opts++modules :: [Module]+modules = [ PID.cmodule+ , FibLoop.cmodule+ , Factorial.cmodule+ , String.cmodule+ , FunPtr.cmodule+ , Overflow.cmodule+ , Float.cmodule+ , Alloc.cmodule+ , Area.cmodule+ , Cond.cmodule+ , Forever.cmodule+ , PublicPrivate.cmodule+ , Bits.cmodule+ , SizeOf.cmodule+ , AddrOfRegression.cmodule+ , Array.cmodule+ ] ++ stdlibModules
+ ivory-examples.cabal view
@@ -0,0 +1,68 @@+name: ivory-examples+version: 0.1.0.0+author: Galois, Inc+maintainer: trevor@galois.com+copyright: 2013 Galois, Inc.+category: Language+synopsis: Ivory examples.+description: Various examples demonstrating the use of Ivory.+homepage: http://smaccmpilot.org/languages/ivory-introduction.html+build-type: Simple+cabal-version: >= 1.10+license: BSD3+license-file: LICENSE+source-repository this+ type: git+ location: https://github.com/GaloisInc/ivory+ tag: hackage-examples-0100+++executable ivory-fibtutorial+ main-is: FibTutorial.hs+ hs-source-dirs: examples+ build-depends: base >= 4.6,+ pretty >= 1.1,+ monadLib >= 3.7,+ template-haskell >= 2.8,+ mainland-pretty >= 0.2.4,+ wl-pprint,+ ivory,+ ivory-opts,+ ivory-backend-c,+ ivory-quickcheck,+ ivory-stdlib,+ QuickCheck+ default-language: Haskell2010+ ghc-options: -Wall++executable ivory-c-clang-test+ main-is: TestClang.hs+ other-modules: Factorial,+ FibLoop,+ PID,+ String,+ FunPtr,+ Float,+ Area,+ Cond,+ Forever,+ PublicPrivate,+ Bits,+ SizeOf,+ AddrOfRegression,+ QC+ hs-source-dirs: examples+ build-depends: base >= 4.6 && < 4.7,+ pretty >= 1.1,+ monadLib >= 3.7,+ template-haskell >= 2.8,+ mainland-pretty >= 0.2.4,+ wl-pprint,+ ivory,+ ivory-opts,+ ivory-quickcheck,+ ivory-backend-c,+ ivory-stdlib,+ QuickCheck+ default-language: Haskell2010+ ghc-options: -Wall