ivory-examples 0.1.0.3.1 → 0.1.0.4
raw patch · 4 files changed
+105/−76 lines, 4 filesdep ~basedep ~template-haskell
Dependency ranges changed: base, template-haskell
Files
- examples/Alloc.hs +36/−43
- examples/ConcreteFile.hs +12/−14
- examples/file.ivory +54/−16
- ivory-examples.cabal +3/−3
examples/Alloc.hs view
@@ -1,15 +1,15 @@ {-# OPTIONS_GHC -fno-warn-orphans #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE TypeOperators #-} module Alloc where -import Ivory.Language-import Ivory.Compile.C.CmdlineFrontend-import Ivory.Compile.C.Modules+import Ivory.Compile.C.CmdlineFrontend+import Ivory.Compile.C.Modules+import Ivory.Language [ivory|@@ -53,16 +53,16 @@ arrayMap (\ix -> store (a ! (ix :: Ix 10)) 1) retVoid +{- -- Can't do this! (Which is good.)--- memcpy4 :: Def ('[ Ref Global (Array 1 (Stored (Ref (Stack s) (Stored Uint32))))] :-> ())--- memcpy4 = proc "memcpy3" $ \a -> body $ do--- val <- local (ival 2)--- larr <- local (iarray [ival val])--- refCopy a larr--- arrayMap (\ix -> store (a ! (ix :: Ix 1)) 1)--- retVoid+memcpy4 :: Def ('[ Ref Global (Array 1 (Stored (Ref (Stack s) (Stored Uint32))))] :-> ())+memcpy4 = proc "memcpy3" $ \a -> body $ do+ val <- local (ival 2)+ larr <- local (iarray [ival val])+ refCopy a larr+ arrayMap (\ix -> store (a ! (ix :: Ix 1)) 1)+ retVoid -{- -- The type system prevents this. bad_alloc :: Def ('[] :-> Ref s (Stored Uint32)) bad_alloc = proc "bad_alloc" $ body $ do@@ -114,9 +114,9 @@ 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)+ arrayMap (\ix -> store (arr ! (ix :: Ix 15)) 1)+ 2 `downTo` 0 $ (\ix -> store (arr ! (ix :: Ix 15)) 1)+ 0 `upTo` 2 $ (\ix -> store (arr ! (ix :: Ix 15)) 1) retVoid testToIx :: Def ('[Sint32, Ref s ('Array 10 ('Stored Uint32))] ':-> Ref s ('Stored Uint32))@@ -129,31 +129,11 @@ [ istruct [ i .= ival 10 ] ] --- DefProc (Proc {procSym = "foo", procRetTy = TyWord Word32, procArgs = [Typed--- {tType = TyRef (TyStruct "Foo"), tValue = VarName "var0"}], procBody = [---- Deref (TyWord Word32) (VarName "deref0") (ExpLabel (TyStruct "Foo") (ExpVar--- (VarName "var0")) "i")--- , Return (Typed {tType = TyWord Word32, tValue = ExpVar--- (VarName "deref0")})--- ], procRequires = [], procEnsures = Nothing})- -- uint32_t n_deref0 = *&n_var0->i; foo :: Def ('[Ref s ('Struct "Foo")] ':-> Uint32) foo = proc "foo" $ \str -> body $ do ret =<< deref (str ~> i) --- DefProc (Proc {procSym = "foo2", procRetTy = TyWord Word32, procArgs = [Typed--- {tType = TyRef (TyStruct "Foo"), tValue = VarName "var0"}], procBody = [---- Deref (TyWord Word32) (VarName "deref0") (ExpIndex (TyArr 10 (TyWord Word32))--- (ExpLabel (TyStruct "Foo") (ExpVar (VarName "var0")) "p") (TyInt Int32)--- (ExpOp ExpMod [ExpLit (LitInteger 0),ExpLit (LitInteger 10)]))---- ,Return (Typed--- {tType = TyWord Word32, tValue = ExpVar (VarName "deref0")})], procRequires =--- [], procEnsures = Nothing})- -- uint32_t n_deref0 = *&n_var0->p[0 % 10]; foo2 :: Def ('[Ref s ('Struct "Foo")] ':-> Uint32) foo2 = proc "foo2" $ \str -> body $ do@@ -161,13 +141,24 @@ let x = arr ! (0 :: Ix 10) ret =<< deref x --deref (arr ! 0) --- foo3 :: Def ('[Ref s (Struct "Bar")] :-> Uint32)--- foo3 = proc "foo3" $ \str -> body $ do--- v <- deref (str ~> aa)--- ret =<< deref v- --------------------------------------------- +-- Testing matrices+mat1 :: Def ('[ConstRef s ('Array 1 ('Array 2 ('Stored Uint32)))] ':-> Uint32)+mat1 = proc "mat1" $ \arr -> body $ do+ v <- deref (arr ! 1 ! 0)+ ret v++mat2 :: Def ('[] ':-> Uint32)+mat2 = proc "mat2" $ body $ do+ arr <- local ((iarray [iarray [ival 0, ival 1]]) :: Init ('Array 1 ('Array 2 ('Stored Uint32))))+ arr2 <- local ((iarray [iarray [ival 3, ival 3]]) :: Init ('Array 1 ('Array 2 ('Stored Uint32))))+ v' <- assign arr+ refCopy arr2 v'+ refZero arr2+ v <- call mat1 (constRef arr)+ ret v+ cmodule :: Module cmodule = package "Alloc" $ do defStruct (Proxy :: Proxy "Foo")@@ -187,9 +178,11 @@ incl testToIx incl memcpy3 defMemArea arrayTest+ incl mat1+ incl mat2 runAlloc :: IO () runAlloc = runCompiler [cmodule] [] initialOpts { outDir = Nothing } test2 :: String-test2 = showModule (compileModule cmodule)+test2 = showModule (compileModule Nothing cmodule)
examples/ConcreteFile.hs view
@@ -1,10 +1,10 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE QuasiQuotes #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -fno-warn-orphans -fno-warn-unused-binds -fno-warn-unused-matches #-} {-# OPTIONS_GHC -fno-warn-name-shadowing -fno-warn-missing-signatures #-}@@ -18,13 +18,14 @@ module ConcreteFile where -import Ivory.Language-import Ivory.Stdlib-import Ivory.Compile.C.CmdlineFrontend+import Ivory.Compile.C.CmdlineFrontend+import Ivory.Language+import Ivory.Stdlib e :: IBool e = (4::Sint32) >? 3 +-- Currently, type synonyms can *only* be for base (non=stored) typed. type SomeInt = Uint32 macroStmts ::@@ -40,11 +41,10 @@ macroStmtsRet x y = do a <- local (ival 0) store a (x + y)- return =<< deref a+ deref a macroExp :: IvoryOrd a => a -> a -> IBool-macroExp x y = do- x <? y+macroExp x y = x <? y toIx' :: ANat n => Uint32 -> Ix n toIx' ix = toIx (twosComplementCast ix)@@ -59,5 +59,3 @@ main :: IO () main = runCompiler [concreteIvory, examplesfile, stdlibStringModule] stdlibStringArtifacts initialOpts {outDir = Just "concrete-ivory", constFold = True}--
examples/file.ivory view
@@ -1,13 +1,34 @@ -- # -*- mode: haskell -*- +-- For any imported header files, you can also provide paths, e.g., "foo/stdio.h". import (stdio.h, printf) int32_t printf(string x) import (stdio.h, printf) int32_t printf2(string x, int32_t y) include concreteIvory --for printf definitions in ConcreteFile.hs include stdlibStringModule --- extern foo.h G* uint8_t myptr+-- Define a struct. A base type is turned into a memory area by adding a+-- '&'. Note this is a type-level operator. Arrays and structs are always memory+-- areas.+struct Bar00 {+ &int32_t aBar00;+} +-- Import global memory areas from `foo.h`.+import foo.h &int32_t *anArea1+import foo.h &int32_t const *anArea2+import foo.h int32_t[4] const anArea3[]++-- Declare some global memory areas. They may be initizlied (otherwise, are initialized to zero).+&int32_t alloc *myArea1;+&int32_t const alloc *myArea2 = 3;+struct Bar00 alloc myArea3{} = { aBar00 = 3 };+int32_t[3] alloc myArea4[] = {1,2,3};+struct Bar00 alloc myArea5{};+struct Bar00 const alloc myArea6{};++extern foo.h G* uint8_t myptr+ -- A top level definition. bar = 3 + 2; @@ -16,20 +37,12 @@ -- (Both of the above can be done on Haskell and you can use antiquotation.) --- Define a struct. A base type is turned into a memory area by adding a--- '&'. Note this is a type-level operator. Arrays and structs are always memory--- areas.-struct Bar00 {- &int32_t aBar00;-}- struct Foo { -- When context makes apparent and we can syntactically check the type, a -- base type is promoted to a memory area (i.e., bool is rewritten to &bool). bool aFoo- -- '&' at the type level binds most tightly and is right-associative. When- -- we use a type alias, the '&' must be added explicitly.- ; &SomeInt[4] aBar+ -- To use synonyms (`SomeInt`), you have to use Haskell syntax.+ ; aBar :: Array 4 (Stored SomeInt) } -- Safe string structs: strings of max length 16 bytes Generates two field@@ -43,10 +56,10 @@ { struct Foo foo2f } -r* struct ivory_string_FooStr foostr(r* struct ivory_string_FooStr s) {+r* struct ivory_string_FooStr foostr(uint8_t i, r* struct ivory_string_FooStr s) { -- Allocate a new string dynamic string. Fails if the string is too large. alloc s0{} = $stringInit("foo");- foostr(s0);+ if (0>i) { foostr(i-1, s0); } else {} -- Store a new string into the dynamic string data structure. $string_lit_store("foos", s); return s;@@ -103,7 +116,6 @@ return *x + 4; } - -- Global allocation (G), stack allocation (S), and undetermined scope (var c) uint8_t foo12(* uint8_t a, G*uint8_t b, * uint8_t c, S* uint8_t d) { store b as *a;@@ -261,7 +273,7 @@ } void fizzbuzzUpFrom() {- upFromTo 50 100 ix {+ upFromTo (50, 100) ix { -- for typechecking let (ix_t 101) ix' = ix; let i = fromIx(ix);@@ -299,7 +311,7 @@ } void fizzbuzzDownFromTo() {- downFromTo 100 50 ix {+ downFromTo (100, 50) ix { -- for typechecking let (ix_t 101) ix' = ix; let i = fromIx(ix);@@ -388,4 +400,30 @@ , const * struct ivory_string_Astr s ) { $sz_from_istr(arr, s);+}++int16_t return_negative() { return -32767; }+int16_t return_negative2() { return -32768; }++struct x {+ int32_t a;+ int32_t b;+}++void test() {+ alloc myref{};+ $refZero (myref);+ store myref.a as 1;+}++-- A 3 dimensional matrix declaration+struct X+{+ float[3][4][5] matrix;+}++void myfunc(* struct X myx)+{+ let m = myx.matrix;+ store m@2@3@4 as 0.0; }
ivory-examples.cabal view
@@ -1,12 +1,12 @@ name: ivory-examples-version: 0.1.0.3.1+version: 0.1.0.4 author: Galois, Inc maintainer: trevor@galois.com, leepike@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+homepage: http://ivorylang.org/ build-type: Simple cabal-version: >= 1.10 license: BSD3@@ -15,7 +15,7 @@ source-repository this type: git location: https://github.com/GaloisInc/ivory- tag: hackage-examples-0103+ tag: hackage-examples-0.1.0.4 executable ivory-c-clang-test main-is: TestExamples.hs