diff --git a/examples/BitData.hs b/examples/BitData.hs --- a/examples/BitData.hs +++ b/examples/BitData.hs @@ -81,7 +81,7 @@ |] test1 :: Def ('[Uint16] ':-> Uint16) -test1 = proc "test1" $ \x -> body $ do +test1 = proc "test1" $ \x -> body $ ret $ withBits x $ do clearBit spi_cr1_cpha setBit spi_cr1_cpol @@ -105,7 +105,7 @@ , ANat (ArraySize n a) ) => BitArray n a -> (a -> Ivory eff ()) -> Ivory eff () forBitArray_ arr f = - forM_ [0..bitLength arr] $ \i -> + forM_ [0 .. bitLength arr - 1] $ \i -> f (arr #! i) -- | Test looping over the elements of a bit array: @@ -134,7 +134,7 @@ |] cmodule :: Module -cmodule = package "hw" $ do +cmodule = package "BitData" $ do incl get_baud incl test1 incl test2 diff --git a/examples/ClassHierarchy.hs b/examples/ClassHierarchy.hs new file mode 100644 --- /dev/null +++ b/examples/ClassHierarchy.hs @@ -0,0 +1,84 @@ +{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ExistentialQuantification #-} + +module ClassHierarchy where + +import Ivory.Language + +-------------------------------------------------------------------------------- + +[ivory| + +-- Three structs defined in the quasiquoter, a base struct and two that'll +-- extend it. +struct StanagBase + { paramA :: Stored IBool } + +-- Annoyingly, the fields are in the same global namespace, so we give unique names to the fields pointing to the base struct. +struct StanagBaseMsg1 + { base1 :: Struct StanagBase + ; paramC :: Stored IFloat + } + +struct StanagBaseMsg2 + { base2 :: Struct StanagBase + ; paramD :: Stored IFloat + } + +|] + +-- A Haskell class that has a method 'getBase'. Given a reference to a struct, +-- getBase returns the base state. +-- +-- XXX This is boilerplate that might be generated... +class (IvoryStruct sym) => ExtendBase sym where + getBase :: forall ref s + . ( IvoryExpr (ref s ('Struct sym)) + , IvoryExpr (ref s ('Struct "StanagBase")) + , IvoryRef ref + ) + => ref s ('Struct sym) -> ref s ('Struct "StanagBase") + +-- For the parent, it's just a noop (identity). +instance ExtendBase "StanagBase" where + getBase = id + +-- Otherwise, we dereference the base field. +instance ExtendBase "StanagBaseMsg1" where + getBase ref = ref ~> base1 + +instance ExtendBase "StanagBaseMsg2" where + getBase ref = ref ~> base2 + +-- A polymorphic procedure Ivory macro for references to objects in the +-- hierachy. Note: this cannot be a C function (or we'd have to specialize it +-- for each use type). +getBaseVal :: ExtendBase sym => Ref s ('Struct sym) -> Ivory eff IBool +getBaseVal ref = do + let r = getBase ref + deref (r ~> paramA) + +-- A procedure that makes use of the polymorphism. Regardless of whehter the +-- reference is to a parent or child, we can use the 'getBaseVal' Ivory +-- function. +bar :: Def ([ Ref s ('Struct "StanagBase") + , Ref s ('Struct "StanagBaseMsg1") + , Ref s ('Struct "StanagBaseMsg2") + ] ':-> IBool) +bar = proc "bar" $ \r0 r1 r2 -> body $ do + b0 <- getBaseVal r0 + b1 <- getBaseVal r1 + b2 <- getBaseVal r2 + ret (b0 .&& b1 .&& b2) + +cmodule :: Module +cmodule = package "ClassHierarchy" $ do + defStruct (Proxy :: Proxy "StanagBase") + defStruct (Proxy :: Proxy "StanagBaseMsg1") + defStruct (Proxy :: Proxy "StanagBaseMsg2") + incl bar diff --git a/examples/ConstPtrRef.hs b/examples/ConstPtrRef.hs new file mode 100644 --- /dev/null +++ b/examples/ConstPtrRef.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeOperators #-} + +module ConstPtrRef where + +import Control.Applicative (pure) +import Ivory.Language + +test :: Def ('[ConstRef s ('Stored (Ptr 'Global ('Stored Uint8)))] ':-> ()) +test = proc "ConstPtrRef_test" $ \refptr -> body $ do + ptr <- deref refptr + withRef ptr + (\ref -> do + val <- deref ref + store ref $ val + 1) + (pure ()) + +cmodule :: Module +cmodule = package "ConstPtrRef" $ incl test diff --git a/examples/ConstRef.hs b/examples/ConstRef.hs new file mode 100644 --- /dev/null +++ b/examples/ConstRef.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} + +module ConstRef where + +import Ivory.Language + +test :: Def ('[ConstRef s ('Stored Uint8)] ':-> Uint8) +test = proc "test" $ \r -> body $ ret =<< deref r + +cmodule :: Module +cmodule = package "ConstRef" $ incl test diff --git a/examples/Extern.hs b/examples/Extern.hs new file mode 100644 --- /dev/null +++ b/examples/Extern.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeOperators #-} + +module Extern where + +import Ivory.Language +import Ivory.Compile.C.CmdlineFrontend + +x :: Uint8 +x = extern "SOME_CONST" "some_other_header.h" + +putchar :: Def ('[Uint8] ':-> ()) +putchar = importProc "putchar" "some_header.h" + +test :: Def ('[Uint8] ':-> ()) +test = proc "test" $ \ c -> body $ + call_ putchar c + >> call_ putchar x + >> retVoid + +runExtern :: IO () +runExtern = runCompiler [cmodule] [] initialOpts { outDir = Nothing, scErrors = True } + +cmodule :: Module +cmodule = package "Extern" $ do + incl test + incl putchar + inclSym x diff --git a/examples/FibTutorial.hs b/examples/FibTutorial.hs new file mode 100644 --- /dev/null +++ b/examples/FibTutorial.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeOperators #-} + +module FibTutorial where + +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 ] [] diff --git a/examples/TestExamples.hs b/examples/TestExamples.hs --- a/examples/TestExamples.hs +++ b/examples/TestExamples.hs @@ -1,24 +1,30 @@ 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 AddrOfRegression 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 BitData +import qualified Bits +import qualified ClassHierarchy import qualified ConcreteFile +import qualified Cond +import qualified ConstPtrRef +import qualified ConstRef import qualified Coroutine +import qualified Extern +import qualified Factorial +import qualified FibLoop +import qualified FibTutorial +import qualified Float +import qualified Forever +import qualified FunPtr import qualified Loop +import qualified Overflow +import qualified PID +import qualified PublicPrivate +import qualified SizeOf +import qualified String import Control.Monad (when) import Ivory.Compile.C.CmdlineFrontend @@ -39,26 +45,31 @@ compileExample opts ms = runCompiler ms stdlibStringArtifacts opts modules :: [Module] -modules = [ PID.cmodule - , FibLoop.cmodule - , Factorial.cmodule - , String.cmodule - , FunPtr.cmodule - , Overflow.cmodule - , Float.cmodule +modules = [ AddrOfRegression.cmodule , Alloc.cmodule , Area.cmodule - , Cond.cmodule - , Forever.cmodule - , PublicPrivate.cmodule - , Bits.cmodule - , SizeOf.cmodule - , AddrOfRegression.cmodule , Array.cmodule - , Overflow.cmodule - , Coroutine.cmodule + , BitData.cmodule + , Bits.cmodule + , ClassHierarchy.cmodule , ConcreteFile.concreteIvory , ConcreteFile.examplesfile + , Cond.cmodule + , ConstPtrRef.cmodule + , ConstRef.cmodule + , Coroutine.cmodule + , Extern.cmodule + , Factorial.cmodule + , FibLoop.cmodule + , FibTutorial.fib_tutorial_module + , Float.cmodule + , Forever.cmodule + , FunPtr.cmodule , Loop.cmodule - , stdlibStringModule - ] ++ stdlibModules + , Overflow.cmodule + , PID.cmodule + , PublicPrivate.cmodule + , SizeOf.cmodule + , String.cmodule + ] + ++ stdlibModules diff --git a/examples/file.ivory b/examples/file.ivory --- a/examples/file.ivory +++ b/examples/file.ivory @@ -59,7 +59,7 @@ 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"); - if (0>i) { foostr(i-1, s0); } else {} + 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; diff --git a/ivory-examples.cabal b/ivory-examples.cabal --- a/ivory-examples.cabal +++ b/ivory-examples.cabal @@ -1,5 +1,5 @@ name: ivory-examples -version: 0.1.0.4 +version: 0.1.0.5 author: Galois, Inc maintainer: trevor@galois.com, leepike@galois.com copyright: 2013 Galois, Inc. @@ -15,37 +15,42 @@ source-repository this type: git location: https://github.com/GaloisInc/ivory - tag: hackage-examples-0.1.0.4 + tag: hackage-0.1.0.4 executable ivory-c-clang-test main-is: TestExamples.hs - other-modules: PID, - FibLoop, - Factorial, - String, - FunPtr, - Overflow, - Float, - Alloc, - Area, - Cond, - Forever, - PublicPrivate, - Bits, - SizeOf, - AddrOfRegression, - Array, - BitData, - BitDataTypes, - ConcreteFile, - Coroutine, - Loop + other-modules: AddrOfRegression + , Alloc + , Area + , Array + , BitData + , BitDataTypes + , Bits + , ClassHierarchy + , ConcreteFile + , Cond + , ConstPtrRef + , ConstRef + , Coroutine + , Extern + , Factorial + , FibLoop + , FibTutorial + , Float + , Forever + , FunPtr + , Loop + , Overflow + , PID + , PublicPrivate + , SizeOf + , String hs-source-dirs: examples - build-depends: base >= 4.6 && < 5, + build-depends: base >= 4.7 && < 5, base-compat, pretty >= 1.1, monadLib >= 3.7, - template-haskell >= 2.8, + template-haskell >= 2.8 && <2.11, ivory, ivory-opts, ivory-backend-c,