ivory-examples 0.1.0.2 → 0.1.0.3
raw patch · 26 files changed
+547/−315 lines, 26 filesdep +base-compatdep −ivory-quickcheckdep −mainland-prettydep −wl-pprintdep ~base
Dependencies added: base-compat
Dependencies removed: ivory-quickcheck, mainland-pretty, wl-pprint
Dependency ranges changed: base
Files
- examples/AddrOfRegression.hs +11/−11
- examples/Alloc.hs +27/−29
- examples/Area.hs +9/−6
- examples/Array.hs +16/−3
- examples/BitData.hs +144/−0
- examples/BitDataTypes.hs +29/−0
- examples/Bits.hs +18/−8
- examples/ConcreteFile.hs +63/−0
- examples/Cond.hs +6/−5
- examples/Coroutine.hs +36/−0
- examples/Factorial.hs +2/−2
- examples/FibLoop.hs +16/−10
- examples/FibTutorial.hs +0/−26
- examples/Float.hs +3/−3
- examples/Forever.hs +4/−4
- examples/FunPtr.hs +5/−5
- examples/Loop.hs +19/−0
- examples/Overflow.hs +10/−8
- examples/PID.hs +23/−7
- examples/PublicPrivate.hs +22/−20
- examples/QC.hs +0/−72
- examples/SizeOf.hs +2/−2
- examples/String.hs +6/−5
- examples/TestClang.hs +0/−60
- examples/TestExamples.hs +64/−0
- ivory-examples.cabal +12/−29
examples/AddrOfRegression.hs view
@@ -21,13 +21,13 @@ defMemArea param_info_area incl t1 where- param_info_area :: MemArea (Array 512 (Struct "param_info"))+ 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 :: Ref 'Global ('Array 512 ('Struct "param_info")) param_info_ref = addrOf param_info_area - t1 :: Def ('[]:->())+ t1 :: Def ('[] ':-> ()) t1 = proc "t1" $ body $ do arrayMap $ \ix -> store ((param_info_ref ! ix) ~> param_requested) 1@@ -37,13 +37,13 @@ defMemArea param_info_area incl t1 where- param_info_area :: MemArea (Struct "param_info")+ 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 :: Ref 'Global ('Struct "param_info") param_info_ref = addrOf param_info_area - t1 :: Def ('[]:->())+ t1 :: Def ('[] ':-> ()) t1 = proc "t1_noarray" $ body $ do store (param_info_ref ~> param_requested) 1 @@ -52,13 +52,13 @@ defMemArea atom_array_area incl t2 where- atom_array_area :: MemArea (Array 512 (Stored IFloat))+ 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 :: Ref 'Global ('Array 512 ('Stored IFloat)) atom_array_ref = addrOf atom_array_area - t2 :: Def ('[]:->())+ t2 :: Def ('[] ':-> ()) t2 = proc "t2" $ body $ do arrayMap $ \ix -> store (atom_array_ref ! ix) 1@@ -67,9 +67,9 @@ test3 = do incl t3 where- t3 :: Def ('[]:->())+ t3 :: Def ('[] ':-> ()) t3 = proc "t3" $ body $ do- (stack_array :: Ref (Stack s) (Array 512 (Stored IFloat))) <- local izero+ (stack_array :: Ref ('Stack s) ('Array 512 ('Stored IFloat))) <- local izero arrayMap $ \ix -> store (stack_array ! ix) 1
examples/Alloc.hs view
@@ -26,26 +26,27 @@ |] -test :: Def ('[Ref s (Struct "Foo")] :-> Ref s (Stored Uint32))-test = proc "test" (\ pid -> body (ret (pid ~> i)))+test :: Def ('[Ref s ('Struct "Foo")] ':-> Ref s ('Stored Uint32))+test = proc "alloc_test" (\ pid -> body (ret (pid ~> i))) -alloc_test :: Def ('[] :-> Uint32)-alloc_test = proc "alloc_test" $ body $ do+get_p :: Def ('[] ':-> Uint32)+get_p = proc "get_p" $ body $ do pid <- local (istruct []) ret =<< deref (pid ~> d) -memcpy1 :: Def ('[ Ref a (Struct "Foo"), Ref a (Struct "Foo") ] :-> Uint32)+memcpy1 :: Def ('[ Ref a ('Struct "Foo"), Ref a ('Struct "Foo") ] ':-> Uint32) memcpy1 = proc "memcpy1" $ \a b -> body $ do refCopy b a ret =<< deref (b ~> i) -memcpy2 :: Def ('[ Ref a (Array 10 (Stored Uint32)), Ref a (Array 10 (Stored Uint32)) ] :-> ())+memcpy2 :: Def ('[ Ref a ('Array 10 ('Stored Uint32))+ , Ref a ('Array 10 ('Stored Uint32)) ] ':-> ()) memcpy2 = proc "memcpy2" $ \a b -> body $ do refCopy b a arrayMap (\ix -> store (a ! (ix :: Ix 10)) 1) retVoid -memcpy3 :: Def ('[ Ref Global (Array 10 (Stored Uint32))] :-> ())+memcpy3 :: Def ('[ Ref 'Global ('Array 10 ('Stored Uint32))] ':-> ()) memcpy3 = proc "memcpy3" $ \a -> body $ do b <- local (iarray $ replicate 10 (ival $ 0)) refCopy b a@@ -69,59 +70,61 @@ ret (pid~>i) -} -arrMap :: Def ('[Ref s (Array 15 (Stored Sint32))] :-> ())+arrMap :: Def ('[Ref s ('Array 15 ('Stored Sint32))] ':-> ()) arrMap = proc "arrMap" $ \ arr -> body $ do arrayMap (\ix -> store (arr ! (ix :: Ix 15)) 1) retVoid -- String copy test --------------------------ptrstrcpy :: Def ('[Ref s (CArray (Stored IChar)), IString, Uint32] :-> ())+ptrstrcpy :: Def ('[ Ref s ('CArray ('Stored IChar))+ , IString+ , Uint32] ':-> ()) ptrstrcpy = proc "ptrstrcpy" $ \ _ _ _ -> body $ do retVoid -callstrcpy :: Def ('[] :-> ())+callstrcpy :: Def ('[] ':-> ()) callstrcpy = proc "callstrcpy" $ body $ do buf' <- local (iarray []) call_ mystrcpy buf' "hello" retVoid -- | Safely copy a string literal into a character array.-mystrcpy :: Def ('[Ref s (Array 10 (Stored IChar)), IString] :-> ())+mystrcpy :: Def ('[Ref s ('Array 10 ('Stored IChar)), IString] ':-> ()) mystrcpy = proc "mystrcpy" $ \ buf s -> body $ do buf' <- assign $ toCArray buf call_ ptrstrcpy buf' s (arrayLen buf) retVoid -assign_test :: Def ('[] :-> ())+assign_test :: Def ('[] ':-> ()) assign_test = proc "assign_test" $ body $ do val <- local (istruct []) _ <- assign (val ~> p) retVoid -bar :: Def ('[] :-> ())-bar = proc "var" $ body $ do- pid <- local $ istruct [i .= ival 3, i .= ival 7]+bar :: Def ('[] ':-> ())+bar = proc "bar" $ body $ do+ pid <- local $ istruct [i .= ival 3] arr <- local $ iarray [ ival c | c <- replicate 10 (char 'a') ] call_ mystrcpy arr "hello" store (pid~>i) 4 -castIx :: Def ('[Ix 253] :-> Uint8)+castIx :: Def ('[Ix 253] ':-> Uint8) castIx = proc "castIx" $ \ix -> body $ do ret $ safeCast (ix :: Ix 253) -loopTest :: Def ('[Ref s (Array 15 (Stored Sint32))] :-> ())+loopTest :: Def ('[Ref s ('Array 15 ('Stored Sint32))] ':-> ()) loopTest = proc "loopTest" $ \ arr -> body $ do arrayMap (\ix -> store (arr ! (ix :: Ix 15)) 1) times 3 (\ix -> store (arr ! (ix :: Ix 15)) 1) for 0 (\ix -> store (arr ! (ix :: Ix 15)) 1) retVoid -testToIx :: Def ('[Sint32, Ref s (Array 10 (Stored Uint32))] :-> Ref s (Stored Uint32))+testToIx :: Def ('[Sint32, Ref s ('Array 10 ('Stored Uint32))] ':-> Ref s ('Stored Uint32)) testToIx = proc "testToIx" $ \ ind arr -> body $ do let idx = toIx ind :: Ix 10 ret (arr ! idx) -arrayTest :: MemArea (Array 10 (Struct "Foo"))+arrayTest :: MemArea ('Array 10 ('Struct "Foo")) arrayTest = area "arrayTest" $ Just $ iarray [ istruct [ i .= ival 10 ] ]@@ -136,7 +139,7 @@ -- ], procRequires = [], procEnsures = Nothing}) -- uint32_t n_deref0 = *&n_var0->i;-foo :: Def ('[Ref s (Struct "Foo")] :-> Uint32)+foo :: Def ('[Ref s ('Struct "Foo")] ':-> Uint32) foo = proc "foo" $ \str -> body $ do ret =<< deref (str ~> i) @@ -152,7 +155,7 @@ -- [], procEnsures = Nothing}) -- uint32_t n_deref0 = *&n_var0->p[0 % 10];-foo2 :: Def ('[Ref s (Struct "Foo")] :-> Uint32)+foo2 :: Def ('[Ref s ('Struct "Foo")] ':-> Uint32) foo2 = proc "foo2" $ \str -> body $ do let arr = (str ~> p) let x = arr ! (0 :: Ix 10)@@ -170,16 +173,12 @@ defStruct (Proxy :: Proxy "Foo") defStruct (Proxy :: Proxy "Str") incl test- incl alloc_test+ incl get_p incl arrMap- incl ptrstrcpy incl mystrcpy- incl callstrcpy- incl assign_test- incl bar incl castIx incl loopTest@@ -187,11 +186,10 @@ incl memcpy2 incl testToIx incl memcpy3- defMemArea arrayTest runAlloc :: IO ()-runAlloc = runCompiler [cmodule] initialOpts { stdOut = True }+runAlloc = runCompiler [cmodule] [] initialOpts { outDir = Nothing } -test2 :: [[String]]+test2 :: String test2 = showModule (compileModule cmodule)
examples/Area.hs view
@@ -7,7 +7,7 @@ module Area where import Ivory.Language-+import Ivory.Compile.C.CmdlineFrontend [ivory| @@ -17,17 +17,17 @@ |] -val :: MemArea (Struct "val")-val = area "val" (Just (istruct [field .= ival 0]))+val :: MemArea ('Struct "val")+val = area "value" (Just (istruct [field .= ival 0])) -cval :: ConstMemArea (Struct "val")+cval :: ConstMemArea ('Struct "val") cval = constArea "cval" (istruct [field .= ival 10]) -getVal :: Def ('[] :-> Uint32)+getVal :: Def ('[] ':-> Uint32) getVal = proc "getVal" $ body $ do ret =<< deref (addrOf val ~> field) -setVal :: Def ('[Uint32] :-> ())+setVal :: Def ('[Uint32] ':-> ()) setVal = proc "setVal" $ \ n -> body $ do store (addrOf val ~> field) n retVoid@@ -39,3 +39,6 @@ defMemArea val defConstMemArea cval defStruct (Proxy :: Proxy "val")++main :: IO ()+main = runCompiler [cmodule] [] initialOpts { outDir = Nothing, constFold = True }
examples/Array.hs view
@@ -7,13 +7,26 @@ import Ivory.Compile.C.CmdlineFrontend cmodule :: Module-cmodule = package "Array" $ incl arrayExample+cmodule = package "Array" $ do+ incl arrayExample+ incl arrayTernary runArrayExample :: IO ()-runArrayExample = runCompiler [cmodule] initialOpts { stdOut = True }+runArrayExample = runCompiler [cmodule] [] initialOpts { outDir = Nothing } -arrayExample :: Def('[Ref s (Array 4 (Stored Uint8)), Uint8] :-> ())+arrayExample :: Def('[Ref s ('Array 4 ('Stored Uint8)), Uint8] ':-> ()) arrayExample = proc "arrayExample" $ \arr n -> body $ do arrayMap $ \ ix -> do v <- deref (arr ! ix) store (arr ! ix) (v + n)+++arrayTernary :: Def('[IBool] ':-> IFloat)+arrayTernary = proc "arrayTernary" $ \b -> body $ do+ a1 <- local (vs 1)+ a2 <- local (vs 2)+ ares <- assign (b ? (a1, a2))+ deref (ares ! 3) >>= ret+ where+ vs :: IFloat -> Init ('Array 4 ('Stored IFloat))+ vs v = iarray (map ival [v, v, v, v])
+ examples/BitData.hs view
@@ -0,0 +1,144 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++{-# OPTIONS_GHC -fno-warn-missing-signatures #-}++module BitData where++import Control.Monad++import Ivory.Language+import Ivory.Compile.C.CmdlineFrontend++import BitDataTypes+import Ivory.Language.BitData.Array (ArraySize)+import Ivory.Language.BitData.Bits (BitSize)+import Ivory.Language.BitData.BitData (BitType)++[ivory|++ bitdata SPI_CR1 :: Bits 16 = spi_cr1+ { spi_cr1_bidimode :: Bit+ , spi_cr1_bidioe :: Bit+ , spi_cr1_crcen :: Bit+ , spi_cr1_crcnext :: Bit+ , spi_cr1_dff :: Bit+ , spi_cr1_rxonly :: Bit+ , spi_cr1_ssm :: Bit+ , spi_cr1_ssi :: Bit+ , spi_cr1_lsbfirst :: Bit+ , spi_cr1_spe :: Bit+ , spi_cr1_br :: SPIBaud+ , spi_cr1_mstr :: Bit+ , spi_cr1_cpol :: Bit+ , spi_cr1_cpha :: Bit+ }++ -- The "SPI_CR2" register defined using a layout clause.+ bitdata SPI_CR2 :: Bits 16 = spi_cr2+ { spi_cr2_txeie :: Bit+ , spi_cr2_rxneie :: Bit+ , spi_cr2_errie :: Bit+ , spi_cr2_frf :: Bit+ , spi_cr2_ssoe :: Bit+ , spi_cr2_txdmaen :: Bit+ , spi_cr2_rxdmaen :: Bit+ } as 8b0 # spi_cr2_txeie # spi_cr2_rxneie # spi_cr2_errie # spi_cr2_frf+ # 1b0 # spi_cr2_ssoe # spi_cr2_txdmaen # spi_cr2_rxdmaen++ -- The "SPI_CR2" register defined using the default layout and+ -- padding fields.+ bitdata Alt_SPI_CR2 :: Bits 16 = alt_spi_cr2+ { _ :: Bits 8+ , alt_spi_cr2_txeie :: Bit+ , alt_spi_cr2_rxneie :: Bit+ , alt_spi_cr2_errie :: Bit+ , alt_spi_cr2_frf :: Bit+ , _ :: Bit+ , alt_spi_cr2_ssoe :: Bit+ , alt_spi_cr2_txdmaen :: Bit+ , alt_spi_cr2_rxdmaen :: Bit+ }++ -- The "NVIC_ISER" register is an array of 32 bits.+ --+ -- We will want to access the array both at Ivory run-time using an+ -- "Ix 32" and at code generation time using a Haskell integer.+ bitdata NVIC_ISER :: Bits 32 = nvic_iser+ { nvic_iser_setena :: BitArray 32 Bit+ }++ -- A bit data type with an array of 4-bit integers.+ bitdata ArrayTest :: Bits 32 = array_test+ { at_4bits :: BitArray 8 (Bits 4)+ }+|]++test1 :: Def ('[Uint16] ':-> Uint16)+test1 = proc "test1" $ \x -> body $ do+ ret $ withBits x $ do+ clearBit spi_cr1_cpha+ setBit spi_cr1_cpol+ setField spi_cr1_br spi_baud_div_8++test2 :: Def ('[Uint32] ':-> Uint8)+test2 = proc "test2" $ \x -> body $ do+ let d = fromRep x :: NVIC_ISER+ ret $ toRep (d #. nvic_iser_setena #! 0)++-- | Iterate over the elements of a bit array.+forBitArray_ ::+ ( ANat n+ , BitCast (BitRep (ArraySize n a)) (BitRep (BitSize (BitType a)))+ , IvoryStore (BitRep (ArraySize n a))+ , IvoryOrd (BitRep (ArraySize n a))+ , IvoryZeroVal (BitRep (ArraySize n a))+ , IvoryInit (BitRep (ArraySize n a))+ , BitData a+ , ANat (BitSize a)+ , ANat (ArraySize n a)+ ) => BitArray n a -> (a -> Ivory eff ()) -> Ivory eff ()+forBitArray_ arr f =+ forM_ [0..bitLength arr] $ \i ->+ f (arr #! i)++-- | Test looping over the elements of a bit array:+test3 :: Def ('[Uint32] ':-> Uint32)+test3 = proc "test3" $ \x -> body $ do+ let d = fromRep x+ total <- local (ival 0)+ forBitArray_ (d #. at_4bits) $ \i -> do+ x' <- deref total+ let y = safeCast (toRep i)+ store total (x' + y)+ ret =<< deref total++get_baud :: Def ('[Uint16] ':-> Uint8)+get_baud = proc "get_baud" $ \x -> body $ do+ let d = fromRep x+ ret (toRep (d #. spi_cr1_br))++-- | Examples from Ivory paper:+[ivory|+ bitdata CtrlReg :: Bits 8 = ctrl_reg+ { ctrl_tx_enable :: Bit+ , ctrl_rx_enable :: Bit+ , ctrl_baud_rate :: BaudRate+ } as 0b0000 # ctrl_tx_enable # ctrl_rx_enable # ctrl_baud_rate+|]++cmodule :: Module+cmodule = package "hw" $ do+ incl get_baud+ incl test1+ incl test2+ incl test3++main :: IO ()+main = runCompiler [cmodule] [] (initialOpts {outDir = Nothing, constFold = True})
+ examples/BitDataTypes.hs view
@@ -0,0 +1,29 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++module BitDataTypes where++import Ivory.Language++[ivory|+ bitdata SPIBaud :: Bits 3+ = spi_baud_div_2 as 0+ | spi_baud_div_4 as 1+ | spi_baud_div_8 as 2+ | spi_baud_div_16 as 3+ | spi_baud_div_32 as 4+ | spi_baud_div_64 as 5+ | spi_baud_div_128 as 6+ | spi_baud_div_256 as 7+|]++-- | Examples from Ivory paper.+[ivory|+ bitdata BaudRate :: Bits 2+ = baud_9600 as 0b00+ | baud_19200 as 0b01+ | baud_38400 as 0b10+ -- bit pattern 0b11 is invalid+|]
examples/Bits.hs view
@@ -4,11 +4,11 @@ module Bits (runBits, cmodule) where import Ivory.Compile.C.CmdlineFrontend-import Ivory.Language+import Ivory.Language hiding (setBit, clearBit, runBits) import MonadLib.Monads (runState, sets) runBits :: IO ()-runBits = runCompiler [cmodule] initialOpts {stdOut = True}+runBits = runCompiler [cmodule] [] initialOpts {outDir = Nothing} cmodule :: Module cmodule = package "Bits" $ do@@ -16,8 +16,10 @@ incl test2 incl test3 incl test4+ incl test5+ incl test6 -test1 :: Def ('[Uint8, Uint16, Uint32, Uint64] :-> Uint64)+test1 :: Def ('[Uint8, Uint16, Uint32, Uint64] ':-> Uint64) test1 = proc "test1" $ \u8 u16 u32 u64 -> body $ do a <- assign $ u8 .& 0xFF b <- assign $ u16 .& 0xFF00@@ -26,7 +28,7 @@ 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 :: Def ('[Ref s ('Array 4 ('Stored Uint8))] ':-> Uint32) test2 = proc "test2" $ \arr -> body $ do a <- deref (arr ! 0) b <- deref (arr ! 1)@@ -47,7 +49,7 @@ 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 :: 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@@ -56,18 +58,18 @@ store (arr ! 3) a setBit :: (IvoryBits a, IvoryStore a)- => (Ref s (Stored a)) -> Int -> Ivory eff ()+ => (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 ()+ => (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 :: Def ('[] ':-> Uint32) test4 = proc "test4" $ body $ do n <- local (ival 0) setBit n 1@@ -76,3 +78,11 @@ setBit n 8 clearBit n 3 ret =<< deref n++test5 :: Def ('[Sint8] ':-> Uint8)+test5 = proc "test5" $ \s -> body $+ ret (twosComplementRep s)++test6 :: Def ('[Uint8] ':-> Sint8)+test6 = proc "test6" $ \s -> body $+ ret (twosComplementCast s)
+ examples/ConcreteFile.hs view
@@ -0,0 +1,63 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE OverloadedStrings #-}++{-# OPTIONS_GHC -fno-warn-orphans -fno-warn-unused-binds -fno-warn-unused-matches #-}+{-# OPTIONS_GHC -fno-warn-name-shadowing -fno-warn-missing-signatures #-}++--+-- C-like syntax for Ivory, parsed from a file.+--+-- Copyright (C) 2014, Galois, Inc.+-- All rights reserved.+--++module ConcreteFile where++import Ivory.Language+import Ivory.Stdlib+import Ivory.Compile.C.CmdlineFrontend++e :: IBool+e = (4::Sint32) >? 3++type SomeInt = Uint32++macroStmts ::+ (Num a, IvoryStore a, IvoryInit a, GetAlloc eff ~ 'Scope s)+ => a -> a -> Ivory eff ()+macroStmts x y = do+ a <- local (ival 0)+ store a (x + y)++macroStmtsRet ::+ (Num a, IvoryStore a, IvoryInit a, GetAlloc eff ~ 'Scope s)+ => a -> a -> Ivory eff a+macroStmtsRet x y = do+ a <- local (ival 0)+ store a (x + y)+ return =<< deref a++macroExp :: IvoryOrd a => a -> a -> IBool+macroExp x y = do+ x <? y++toIx' :: ANat n => Uint32 -> Ix n+toIx' ix = toIx (twosComplementCast ix)++concreteIvory :: Module+concreteIvory = package "concreteIvory" $ do+ incl printf+ incl printf2++[ivoryFile|examples/file.ivory|]++main :: IO ()+main = runCompiler [concreteIvory, examplesfile, stdlibStringModule] stdlibStringArtifacts+ initialOpts {outDir = Just "concrete-ivory", constFold = True}++
examples/Cond.hs view
@@ -7,7 +7,7 @@ import Ivory.Compile.C.CmdlineFrontend import Prelude hiding (exp) -add :: Def ('[Uint32,Uint32] :-> Uint32)+add :: Def ('[Uint32,Uint32] ':-> Uint32) add = proc "add" $ \ x y -> ensures (\r -> r ==? x + y) $ body@@ -18,7 +18,7 @@ -- Testing assertions with choice expression -foo :: Def ('[IFloat,IFloat,IFloat] :-> IFloat)+foo :: Def ('[IFloat,IFloat,IFloat] ':-> IFloat) foo = proc "foo" $ \x y z -> body $ do let cond = 2/x ==? 5 let tCond = 6/y ==? 7@@ -29,6 +29,7 @@ fooMod = package "fooM" $ incl foo runFoo :: IO ()-runFoo = runCompiler [fooMod] initialOpts { stdOut = True- , divZero = True- }+runFoo = runCompiler [fooMod] []+ initialOpts { outDir = Nothing+ , divZero = True+ }
+ examples/Coroutine.hs view
@@ -0,0 +1,36 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeOperators #-}++module Coroutine where++import Ivory.Language+import Ivory.Compile.C.CmdlineFrontend++-- No-op "action" for the coroutine to trigger+emit :: Def ('[Sint32] ':-> ())+emit = proc "emit" $ \ _ -> body $ retVoid++sequenced :: Coroutine ('Stored Sint32)+sequenced = coroutine "sequenced" $ CoroutineBody $ \ yield -> do+ forever $ do+ call_ emit 1+ v <- yield >>= deref+ ifte_ (v ==? 1) breakOut (return ())+ call_ emit 2+ forever $ do+ v <- yield >>= deref+ ifte_ (v ==? 2)+ (call_ emit 3)+ (call_ emit 2)++run :: Def ('[IBool, ConstRef s ('Stored Sint32)] ':-> ())+run = proc "run" $ \ doInit arg -> body $ coroutineRun sequenced doInit arg++cmodule :: Module+cmodule = package "sequenced" $ do+ incl emit+ incl run+ coroutineDef sequenced++main :: IO ()+main = compile [cmodule] []
examples/Factorial.hs view
@@ -6,7 +6,7 @@ import Ivory.Language import Ivory.Compile.C.CmdlineFrontend -factorial :: Def ('[Sint32] :-> Sint32)+factorial :: Def ('[Sint32] ':-> Sint32) factorial = proc "factorial" $ \ n -> -- These are made up requires/ensures for testing purposes. ensures (\r -> n <? r) $@@ -22,4 +22,4 @@ cmodule = package "Factorial" $ incl factorial runFactorial :: IO ()-runFactorial = runCompiler [cmodule] initialOpts { stdOut = True }+runFactorial = runCompiler [cmodule] [] initialOpts { outDir = Nothing }
examples/FibLoop.hs view
@@ -3,19 +3,21 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators #-}+{-# LANGUAGE CPP #-} module FibLoop where +import Prelude ()+import Prelude.Compat+ import Ivory.Compile.C.CmdlineFrontend import Ivory.Language -import Control.Applicative ((<$>),(<*>))- -- Recursive implementation of fib-fib_rec :: Def ('[Uint32] :-> Uint64)+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 :: Def ('[Uint32,Uint32,Uint32] ':-> Uint64) fib_rec_aux = proc "fib_rec_aux" $ \ a b n -> body $ do ifte_ (n ==? 0) (ret (safeCast a))@@ -23,19 +25,23 @@ -- Loop implementation of fib. -fib_loop :: Def ('[Ix 1000] :-> Uint32)+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+ b <- local (ival 1)+ comment "before loop"+ n `times` \ _ix -> do+ comment "inside top of loop" a' <- deref a b' <- deref b store a b' store b (a' + b')+ comment "inside end of loop"+ comment "after end of loop" result <- deref a ret result+ -- comment "after return" -- Loop implementation of fib, using a structure instead -- of two discrete variables.@@ -46,7 +52,7 @@ } |] -fib_struct_loop :: Def ('[Ix 1000] :-> 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 ]) @@ -68,4 +74,4 @@ incl fib_struct_loop runFibLoop :: IO ()-runFibLoop = runCompiler [cmodule] initialOpts { stdOut = True, constFold = True }+runFibLoop = runCompiler [cmodule] [] initialOpts { outDir = Nothing, constFold = True }
− examples/FibTutorial.hs
@@ -1,26 +0,0 @@-{-# 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
@@ -7,15 +7,15 @@ import Ivory.Language runFloat :: IO ()-runFloat = runCompiler [cmodule] initialOpts { stdOut = True }+runFloat = runCompiler [cmodule] [] initialOpts { outDir = Nothing } cmodule :: Module cmodule = package "Float" $ do incl test1 incl test2 -test1 :: Def ('[IFloat] :-> Sint32)+test1 :: Def ('[IFloat] ':-> Sint32) test1 = proc "test1" (\ f -> body (ret (castDefault f))) -test2 :: Def ('[Sint32] :-> IFloat)+test2 :: Def ('[Sint32] ':-> IFloat) test2 = proc "test2" (\ i -> body (ret (safeCast i)))
examples/Forever.hs view
@@ -6,7 +6,7 @@ import Ivory.Language import Ivory.Compile.C.CmdlineFrontend -factorial :: Def ('[Sint32] :-> Sint32)+factorial :: Def ('[Sint32] ':-> Sint32) factorial = proc "factorial" $ \ n -> -- These are made up requires/ensures for testing purposes. ensures (\r -> n <? r) $ body $ do@@ -17,10 +17,10 @@ (do ret n ) -printResult :: Def ('[Sint32] :-> ())+printResult :: Def ('[Sint32] ':-> ()) printResult = proc "print_result" $ \_ -> body retVoid -foreverFactorial :: Def ('[Sint32] :-> ())+foreverFactorial :: Def ('[Sint32] ':-> ()) foreverFactorial = proc "forever_factorial" $ \ n -> body $ do forever $ do res <- call factorial n@@ -33,5 +33,5 @@ incl foreverFactorial runFactorial :: IO ()-runFactorial = runCompiler [cmodule] initialOpts { stdOut = True }+runFactorial = runCompiler [cmodule] [] initialOpts { outDir = Nothing }
examples/FunPtr.hs view
@@ -6,17 +6,17 @@ import Ivory.Compile.C.CmdlineFrontend import Ivory.Language -f :: Def ('[Sint32] :-> Sint32)+f :: Def ('[Sint32] ':-> Sint32) f = proc "f" (\ n -> body (ret (n + 1))) -invoke :: Def ('[ ProcPtr ('[Sint32] :-> Sint32), Sint32] :-> Sint32)+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))+test :: Def ('[] ':-> Sint32)+test = proc "fun_ptr_test" (body (ret =<< call invoke (procPtr f) 10)) runFunPtr :: IO ()-runFunPtr = runCompiler [cmodule] initialOpts { stdOut = True }+runFunPtr = runCompiler [cmodule] [] initialOpts { outDir = Nothing } cmodule :: Module cmodule = package "FunPtr" $ do
+ examples/Loop.hs view
@@ -0,0 +1,19 @@+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE DataKinds #-}++module Loop where++import Ivory.Language+import Ivory.Compile.C.CmdlineFrontend++cmodule :: Module+cmodule = package "Loop" $ do+ incl loopTest0++runLoopExample :: IO ()+runLoopExample = runCompiler [cmodule] [] initialOpts { outDir = Nothing }++loopTest0 :: Def ('[] ':-> ())+loopTest0 = proc "loopTest" $ body $+ do (0 :: Ix 1) `times` \ _ -> return ()+ retVoid
examples/Overflow.hs view
@@ -6,25 +6,27 @@ import Ivory.Language import Ivory.Compile.C.CmdlineFrontend -ovf1 :: Def ('[Sint8] :-> Sint8)+ovf1 :: Def ('[Sint8] ':-> Sint8) ovf1 = proc "ovf1" $ \ n -> body $ ifte_ (n <? maxBound - 20) (ret (n + 15)) (ret (n .% 2)) -ovf2 :: Def ('[Sint8] :-> Sint8)+ovf2 :: Def ('[Sint8] ':-> Sint8) ovf2 = proc "ovf2" $ \ n -> requires (n <? 1) $ body $ ret (n + 15) -ovf3 :: Def ('[IFloat, IFloat, IFloat] :-> IBool)+ovf3 :: Def ('[IFloat, IFloat, IBool] ':-> IFloat) ovf3 = proc "ovf3" $ \ n m o -> body $ do- x <- assign (n / m / o)- ret $ x >? (n / m)+-- x <- assign (n / m / o)+ ret $ (o ? (n / m, m / n)) cmodule :: Module-cmodule = package "Overflow" $ incl ovf1 >> incl ovf2 >> incl ovf3+cmodule = package "Overflow" $ --incl ovf1 >> incl ovf2 >> + incl ovf3 writeOverflow :: Opts -> IO ()-writeOverflow opts = runCompiler [cmodule]- opts { constFold = True, overflow = True, divZero = True }+writeOverflow opts = runCompiler [cmodule] []+ opts { constFold = False, overflow = False, divZero = True, outDir = Nothing }+
examples/PID.hs view
@@ -45,11 +45,11 @@ ki = 0.1 kd = 0.1 -pidUpdate :: Def ('[ Ref s (Struct "PID")+pidUpdate :: Def ('[ Ref s ('Struct "PID") , SP , PV , Time ]- :-> IFloat)+ ':-> IFloat) pidUpdate = proc "pid_update" $ \ pid sp pv dt -> -- These are made up requires/ensures for testing purposes.@@ -67,16 +67,32 @@ store (pid ~> pid_err) err ret err +foo :: Def ('[ Ref s ('Array 3 ('Stored Uint32))+ , Ref s ('Array 3 ('Stored Uint32)) ] ':-> ())+foo = proc "foo" $ \a b ->+-- requires (*a!0 < *b!0)+ requires (checkStored (a ! 0)+ (\v -> (checkStored (b ! 0)+ (\v1 -> v <? v1))))+ $ body $ do+ retVoid+ runPID :: IO ()-runPID = runCompiler [cmodule] initialOpts { stdOut = True }+runPID = runCompiler [cmodule] []+ initialOpts { outDir = Nothing, bitShiftCheck = True, divZero = True } cmodule :: Module cmodule = package "PID" $ do- defStruct (Proxy :: Proxy "PID")- incl pidUpdate- incl alloc_test+ incl foobar+ -- defStruct (Proxy :: Proxy "PID")+ -- incl pidUpdate+ -- incl alloc_test -alloc_test :: Def ('[] :-> IFloat)+foobar :: Def ('[Uint8] ':-> Uint8)+foobar = proc "foobar" $ \x -> body $ do+ ret (x `iShiftR` (3 `iDiv` 2))++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
@@ -5,42 +5,44 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverloadedStrings #-} +-- | Example of a private struct, defined as a global memory area, with a public+-- access function.+ module PublicPrivate where import Ivory.Language import Ivory.Compile.C.CmdlineFrontend - [ivory|-struct Foo { i :: Stored Uint32 }-struct Bar { name :: Array 32 (Stored IChar) }+struct Foo { foo_i :: Stored Sint32+ ; foo_cnt :: Stored Uint32+ } |] -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+privateFoo :: MemArea ('Struct "Foo")+privateFoo = area "private_foo" $+ Just (istruct [foo_i .= ival 0, foo_cnt .= ival 0]) -publicFunction :: Def ('[Ref s (Struct "Bar")] :-> Uint32)-publicFunction = proc "public_function" $ \_ -> body $ do- a <- call privateHelper1 (addrOf privateFoo)- call_ privateHelper2- ret =<< deref a+privUpdate :: Def ('[Sint32] ':-> ())+privUpdate = proc "privUpdate" $ \v -> body $ do+ let foo = addrOf privateFoo+ curr <- deref (foo ~> foo_cnt)+ store (foo ~> foo_i) v+ store (foo~> foo_cnt) (curr+1) -privateFoo :: MemArea (Struct "Foo")-privateFoo = area "private_foo" Nothing+pubUpdate :: Def ('[Sint32] ':-> ())+pubUpdate = proc "pubUpdate" $ \v -> body $ do+ call_ privUpdate v cmodule :: Module cmodule = package "PublicPrivate" $ do private $ do defStruct (Proxy :: Proxy "Foo") defMemArea privateFoo- incl privateHelper1- incl privateHelper2+ incl privUpdate public $ do- defStruct (Proxy :: Proxy "Bar")- incl publicFunction+ incl pubUpdate runPublicPrivate :: IO ()-runPublicPrivate = runCompiler [cmodule] initialOpts { stdOut = True, constFold = True }+runPublicPrivate = runCompiler [cmodule] []+ initialOpts { outDir = Nothing, constFold = True }
− examples/QC.hs
@@ -1,72 +0,0 @@-{-# 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
@@ -19,8 +19,8 @@ |] -test :: Def ('[] :-> Uint8)-test = proc "test" (body (ret (sizeOf (Proxy :: Proxy (Struct "foo")))))+test :: Def ('[] ':-> Uint8)+test = proc "sizeof_test" (body (ret (sizeOf (Proxy :: Proxy ('Struct "foo"))))) cmodule :: Module cmodule = package "SizeOf" $ do
examples/String.hs view
@@ -7,22 +7,23 @@ import Ivory.Language import Ivory.Compile.C.CmdlineFrontend -printf :: Def ('[IString] :-> Sint32)+printf :: Def ('[IString] ':-> Sint32) printf = importProc "printf" "stdio.h" -printf2 :: Def ('[IString,Sint32] :-> Sint32)+printf2 :: Def ('[IString,Sint32] ':-> Sint32) printf2 = importProc "printf" "stdio.h" -test :: Def ('[] :-> ())+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 }+runString = runCompiler [cmodule] [] initialOpts { outDir = Nothing } +-- Don't collide with string.h (case-insensitive on Mac) cmodule :: Module-cmodule = package "String" $ do+cmodule = package "String_ex" $ do incl printf incl test
− examples/TestClang.hs
@@ -1,60 +0,0 @@-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
+ examples/TestExamples.hs view
@@ -0,0 +1,64 @@+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 qualified ConcreteFile+import qualified Coroutine+import qualified Loop++import Control.Monad (when)+import Ivory.Compile.C.CmdlineFrontend+import Ivory.Stdlib.String+import Ivory.Language (Module())+import Ivory.Stdlib (stdlibModules)++main :: IO ()+main = do+ args <- getArgs+ when (null args)+ (error "Binary takes a path to srcs and headers as an argument")+ let path = head args+ let opts = initialOpts { outDir = Just path, srcLocs = True }+ compileExample opts modules++compileExample :: Opts -> [Module] -> IO ()+compileExample opts ms = runCompiler ms stdlibStringArtifacts 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+ , Overflow.cmodule+ , Coroutine.cmodule+ , ConcreteFile.concreteIvory+ , ConcreteFile.examplesfile+ , Loop.cmodule+ , stdlibStringModule+ ] ++ stdlibModules
ivory-examples.cabal view
@@ -1,7 +1,7 @@ name: ivory-examples-version: 0.1.0.2+version: 0.1.0.3 author: Galois, Inc-maintainer: trevor@galois.com+maintainer: trevor@galois.com, leepike@galois.com copyright: 2013 Galois, Inc. category: Language synopsis: Ivory examples.@@ -14,29 +14,10 @@ source-repository this type: git location: https://github.com/GaloisInc/ivory- tag: hackage-examples-0102---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+ tag: hackage-examples-0103 executable ivory-c-clang-test- main-is: TestClang.hs+ main-is: TestExamples.hs other-modules: PID, FibLoop, Factorial,@@ -53,19 +34,21 @@ SizeOf, AddrOfRegression, Array,- QC+ BitData,+ BitDataTypes,+ ConcreteFile,+ Coroutine,+ Loop hs-source-dirs: examples- build-depends: base >= 4.6 && < 4.7,+ build-depends: base >= 4.6 && < 5,+ base-compat, 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+ ghc-options: -Wall