diff --git a/ivory-backend-c/ivory-backend-c.cabal b/ivory-backend-c/ivory-backend-c.cabal index e8a52e61..f0b7857c 100644 --- a/ivory-backend-c/ivory-backend-c.cabal +++ b/ivory-backend-c/ivory-backend-c.cabal @@ -30,15 +30,16 @@ library other-modules: Paths_ivory_backend_c build-depends: base >= 4.7 && < 5, + ivory, + ivory-artifact, + ivory-opts, + directory, + filepath, language-c-quote >= 0.13, - srcloc, mainland-pretty >= 0.6, monadLib >= 3.7, - directory, - filepath, - ivory, - ivory-opts, - ivory-artifact + pretty >= 1.1, + srcloc, hs-source-dirs: src default-language: Haskell2010 diff --git a/ivory-backend-c/src/Ivory/Compile/C/CmdlineFrontend.hs b/ivory-backend-c/src/Ivory/Compile/C/CmdlineFrontend.hs index b4e58c65..a62743bb 100644 --- a/ivory-backend-c/src/Ivory/Compile/C/CmdlineFrontend.hs +++ b/ivory-backend-c/src/Ivory/Compile/C/CmdlineFrontend.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE FlexibleContexts #-} + module Ivory.Compile.C.CmdlineFrontend ( compile , compileWith @@ -9,11 +11,9 @@ module Ivory.Compile.C.CmdlineFrontend , outputCompiler ) where -import Data.List (intercalate, nub, - (\\)) -import qualified Ivory.Compile.C as C import qualified Paths_ivory_backend_c as P +import qualified Ivory.Compile.C as C import Ivory.Compile.C.CmdlineFrontend.Options import Ivory.Artifact @@ -31,11 +31,16 @@ import qualified Ivory.Opts.TypeCheck as T import Control.Monad (when) -import Data.List (foldl') +import Data.List (foldl', intercalate, + nub, (\\)) import Data.Maybe (catMaybes, mapMaybe) +import MonadLib (WriterM, put, + runWriterT) import System.Directory (createDirectoryIfMissing) import System.Environment (getArgs) import System.FilePath (addExtension, ()) +import System.IO (hPutStrLn, stderr) +import Text.PrettyPrint (Doc, render, vcat) import qualified Data.Maybe @@ -56,7 +61,8 @@ runCompiler ms as os = runCompilerWith ms as os -- | Main compile function. runCompilerWith :: [Module] -> [Located Artifact] -> Opts -> IO () runCompilerWith modules artifacts opts = do - cmodules <- compileUnits modules opts + (cmodules, errors) <- runWriterT $ compileUnits modules opts + hPutStrLn stderr $ render $ vcat errors if outProcSyms opts then C.outputProcSyms modules else outputCompiler cmodules artifacts opts @@ -106,7 +112,7 @@ outputmodules opts cmodules user_artifacts = do output :: FilePath -> FilePath -> (C.CompileUnits -> String) -> C.CompileUnits -> IO () - output dir ext render m = outputHelper fout (render m) + output dir ext renderUnits m = outputHelper fout (renderUnits m) where fout = addExtension (dir (C.unitName m)) ext renderHeader cu = C.renderHdr (C.headers cu) (C.unitName cu) @@ -123,21 +129,21 @@ outputmodules opts cmodules user_artifacts = do out = writeFile fname contents -- | Compile, type-check, and optimize modules, but don't generate C files. -compileUnits ::[Module] -> Opts -> IO [C.CompileUnits] +compileUnits :: WriterM m [Doc] => [Module] -> Opts -> m [C.CompileUnits] compileUnits modules opts = do when (tcErrors opts) $ do let ts = map T.typeCheck modules let anyTs = or (map T.existErrors ts) let b = tcWarnings opts - mapM_ (T.showTyChkModule b) ts + mapM_ (\t -> put [T.showTyChkModule b t]) ts when anyTs (error "Type-checking failed!") when (scErrors opts) $ do let ds = S.dupDefs modules - S.showDupDefs ds + put [S.showDupDefs ds] let ss = S.sanityCheck modules - mapM_ S.showSanityChkModule ss + mapM_ (\s -> put [S.showSanityChkModule s]) ss let anySs = or (map S.existErrors ss) when anySs (error "Sanity-check failed!") diff --git a/ivory-examples/examples/AddrOfRegression.hs b/ivory-examples/examples/AddrOfRegression.hs index 92910952..b5381fdc 100644 --- a/ivory-examples/examples/AddrOfRegression.hs +++ b/ivory-examples/examples/AddrOfRegression.hs @@ -27,7 +27,7 @@ test1 = do 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 @@ -43,7 +43,7 @@ test1_noarray = do 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 @@ -58,7 +58,7 @@ test2 = do 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,7 +67,7 @@ test3 :: ModuleDef 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 arrayMap $ \ix -> diff --git a/ivory-examples/examples/Alloc.hs b/ivory-examples/examples/Alloc.hs index 59a7b671..c158324c 100644 --- a/ivory-examples/examples/Alloc.hs +++ b/ivory-examples/examples/Alloc.hs @@ -26,27 +26,27 @@ struct Str { |] -test :: Def ('[Ref s ('Struct "Foo")] ':-> Ref s ('Stored Uint32)) +test :: Def ('[Ref s ('Struct "Foo")] :-> Ref s ('Stored Uint32)) test = proc "alloc_test" (\ pid -> body (ret (pid ~> i))) -get_p :: Def ('[] ':-> Uint32) +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)) ] ':-> ()) + , 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 @@ -70,7 +70,7 @@ bad_alloc = proc "bad_alloc" $ body $ do 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 @@ -78,48 +78,48 @@ arrMap = proc "arrMap" $ \ arr -> body $ do -- String copy test ------------------------- ptrstrcpy :: Def ('[ Ref s ('CArray ('Stored IChar)) , IString - , Uint32] ':-> ()) + , 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 :: 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) 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)) +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) @@ -130,12 +130,12 @@ arrayTest = area "arrayTest" $ Just $ iarray ] -- 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) -- 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) @@ -144,12 +144,12 @@ foo2 = proc "foo2" $ \str -> body $ do --------------------------------------------- -- Testing matrices -mat1 :: Def ('[ConstRef s ('Array 1 ('Array 2 ('Stored Uint32)))] ':-> Uint32) +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 :: 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)))) diff --git a/ivory-examples/examples/Area.hs b/ivory-examples/examples/Area.hs index 9e5dff71..069118c2 100644 --- a/ivory-examples/examples/Area.hs +++ b/ivory-examples/examples/Area.hs @@ -23,11 +23,11 @@ val = area "value" (Just (istruct [field .= ival 0])) 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 diff --git a/ivory-examples/examples/Array.hs b/ivory-examples/examples/Array.hs index e64cc7d5..c0ea68b8 100644 --- a/ivory-examples/examples/Array.hs +++ b/ivory-examples/examples/Array.hs @@ -14,14 +14,14 @@ cmodule = package "Array" $ do runArrayExample :: IO () 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 :: Def('[IBool] :-> IFloat) arrayTernary = proc "arrayTernary" $ \b -> body $ do a1 <- local (vs 1) a2 <- local (vs 2) diff --git a/ivory-examples/examples/BitData.hs b/ivory-examples/examples/BitData.hs index 7bdb0148..a9521736 100644 --- a/ivory-examples/examples/BitData.hs +++ b/ivory-examples/examples/BitData.hs @@ -80,14 +80,14 @@ import Ivory.Language.BitData.BitData (BitType) } |] -test1 :: Def ('[Uint16] ':-> Uint16) +test1 :: Def ('[Uint16] :-> Uint16) test1 = proc "test1" $ \x -> body $ 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 :: Def ('[Uint32] :-> Uint8) test2 = proc "test2" $ \x -> body $ do let d = fromRep x :: NVIC_ISER ret $ toRep (d #. nvic_iser_setena #! 0) @@ -109,7 +109,7 @@ forBitArray_ arr f = f (arr #! i) -- | Test looping over the elements of a bit array: -test3 :: Def ('[Uint32] ':-> Uint32) +test3 :: Def ('[Uint32] :-> Uint32) test3 = proc "test3" $ \x -> body $ do let d = fromRep x total <- local (ival 0) @@ -119,7 +119,7 @@ test3 = proc "test3" $ \x -> body $ do store total (x' + y) ret =<< deref total -get_baud :: Def ('[Uint16] ':-> Uint8) +get_baud :: Def ('[Uint16] :-> Uint8) get_baud = proc "get_baud" $ \x -> body $ do let d = fromRep x ret (toRep (d #. spi_cr1_br)) diff --git a/ivory-examples/examples/Bits.hs b/ivory-examples/examples/Bits.hs index 2842a79e..2c486770 100644 --- a/ivory-examples/examples/Bits.hs +++ b/ivory-examples/examples/Bits.hs @@ -19,7 +19,7 @@ cmodule = package "Bits" $ do 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 @@ -28,7 +28,7 @@ test1 = proc "test1" $ \u8 u16 u32 u64 -> body $ do 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) @@ -49,7 +49,7 @@ extractUint32 x = fst $ runState x $ do 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 @@ -69,7 +69,7 @@ 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 @@ -79,10 +79,10 @@ test4 = proc "test4" $ body $ do clearBit n 3 ret =<< deref n -test5 :: Def ('[Sint8] ':-> Uint8) +test5 :: Def ('[Sint8] :-> Uint8) test5 = proc "test5" $ \s -> body $ ret (twosComplementRep s) -test6 :: Def ('[Uint8] ':-> Sint8) +test6 :: Def ('[Uint8] :-> Sint8) test6 = proc "test6" $ \s -> body $ ret (twosComplementCast s) diff --git a/ivory-examples/examples/ClassHierarchy.hs b/ivory-examples/examples/ClassHierarchy.hs index 52d809c8..3d746c63 100644 --- a/ivory-examples/examples/ClassHierarchy.hs +++ b/ivory-examples/examples/ClassHierarchy.hs @@ -37,12 +37,10 @@ struct StanagBaseMsg2 -- -- 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") + getBase :: forall c s + . (KnownConstancy c) + => Pointer 'Valid c s ('Struct sym) + -> Pointer 'Valid c s ('Struct "StanagBase") -- For the parent, it's just a noop (identity). instance ExtendBase "StanagBase" where @@ -69,7 +67,7 @@ getBaseVal ref = do bar :: Def ([ Ref s ('Struct "StanagBase") , Ref s ('Struct "StanagBaseMsg1") , Ref s ('Struct "StanagBaseMsg2") - ] ':-> IBool) + ] :-> IBool) bar = proc "bar" $ \r0 r1 r2 -> body $ do b0 <- getBaseVal r0 b1 <- getBaseVal r1 diff --git a/ivory-examples/examples/Cond.hs b/ivory-examples/examples/Cond.hs index 464f40e7..98022aec 100644 --- a/ivory-examples/examples/Cond.hs +++ b/ivory-examples/examples/Cond.hs @@ -7,7 +7,7 @@ import Ivory.Language 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 @@ cmodule = package "cond" $ incl add -- 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 diff --git a/ivory-examples/examples/ConstPtrRef.hs b/ivory-examples/examples/ConstPtrRef.hs index 2a79c8b0..ab8da56a 100644 --- a/ivory-examples/examples/ConstPtrRef.hs +++ b/ivory-examples/examples/ConstPtrRef.hs @@ -5,7 +5,7 @@ module ConstPtrRef where import Ivory.Language -test :: Def ('[ConstRef s ('Stored (Ptr 'Global ('Stored Uint8)))] ':-> ()) +test :: Def ('[ConstRef s ('Stored (Ptr 'Global ('Stored Uint8)))] :-> ()) test = proc "ConstPtrRef_test" $ \refptr -> body $ do ptr <- deref refptr withRef ptr diff --git a/ivory-examples/examples/ConstRef.hs b/ivory-examples/examples/ConstRef.hs index 0eaf911a..e9c1a5a9 100644 --- a/ivory-examples/examples/ConstRef.hs +++ b/ivory-examples/examples/ConstRef.hs @@ -5,7 +5,7 @@ module ConstRef where import Ivory.Language -test :: Def ('[ConstRef s ('Stored Uint8)] ':-> Uint8) +test :: Def ('[ConstRef s ('Stored Uint8)] :-> Uint8) test = proc "test" $ \r -> body $ ret =<< deref r cmodule :: Module diff --git a/ivory-examples/examples/Coroutine.hs b/ivory-examples/examples/Coroutine.hs index 8376f3eb..fa0265b7 100644 --- a/ivory-examples/examples/Coroutine.hs +++ b/ivory-examples/examples/Coroutine.hs @@ -7,7 +7,7 @@ import Ivory.Language import Ivory.Compile.C.CmdlineFrontend -- No-op "action" for the coroutine to trigger -emit :: Def ('[Sint32] ':-> ()) +emit :: Def ('[Sint32] :-> ()) emit = proc "emit" $ \ _ -> body $ retVoid sequenced :: Coroutine ('Stored Sint32) @@ -23,7 +23,7 @@ sequenced = coroutine "sequenced" $ CoroutineBody $ \ yield -> do (call_ emit 3) (call_ emit 2) -run :: Def ('[IBool, ConstRef s ('Stored Sint32)] ':-> ()) +run :: Def ('[IBool, ConstRef s ('Stored Sint32)] :-> ()) run = proc "run" $ \ doInit arg -> body $ coroutineRun sequenced doInit arg cmodule :: Module diff --git a/ivory-examples/examples/Extern.hs b/ivory-examples/examples/Extern.hs index f79c620d..d5b36fc3 100644 --- a/ivory-examples/examples/Extern.hs +++ b/ivory-examples/examples/Extern.hs @@ -9,10 +9,10 @@ import Ivory.Compile.C.CmdlineFrontend x :: Uint8 x = extern "SOME_CONST" "some_other_header.h" -putchar :: Def ('[Uint8] ':-> ()) +putchar :: Def ('[Uint8] :-> ()) putchar = importProc "putchar" "some_header.h" -test :: Def ('[Uint8] ':-> ()) +test :: Def ('[Uint8] :-> ()) test = proc "test" $ \ c -> body $ call_ putchar c >> call_ putchar x diff --git a/ivory-examples/examples/Factorial.hs b/ivory-examples/examples/Factorial.hs index 238d0428..c6045d2f 100644 --- a/ivory-examples/examples/Factorial.hs +++ b/ivory-examples/examples/Factorial.hs @@ -6,7 +6,7 @@ module Factorial where 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 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)) @@ -22,7 +22,7 @@ fib_rec_aux = proc "fib_rec_aux" $ \ a b n -> body $ do -- 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 1) @@ -49,7 +49,7 @@ struct Fibstate } |] -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 ]) diff --git a/ivory-examples/examples/FibTutorial.hs b/ivory-examples/examples/FibTutorial.hs index e83a6fe4..747a79bf 100644 --- a/ivory-examples/examples/FibTutorial.hs +++ b/ivory-examples/examples/FibTutorial.hs @@ -6,7 +6,7 @@ module FibTutorial where import Ivory.Language import qualified Ivory.Compile.C.CmdlineFrontend as C (compile) -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 1) diff --git a/ivory-examples/examples/Float.hs b/ivory-examples/examples/Float.hs index 5e0c27cb..8407fb25 100644 --- a/ivory-examples/examples/Float.hs +++ b/ivory-examples/examples/Float.hs @@ -14,8 +14,8 @@ 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))) diff --git a/ivory-examples/examples/Forever.hs b/ivory-examples/examples/Forever.hs index 7339bac5..fce82964 100644 --- a/ivory-examples/examples/Forever.hs +++ b/ivory-examples/examples/Forever.hs @@ -6,7 +6,7 @@ module Forever where 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 (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 @@ -34,4 +34,3 @@ cmodule = package "Forever" $ do runFactorial :: IO () runFactorial = runCompiler [cmodule] [] initialOpts { outDir = Nothing } - diff --git a/ivory-examples/examples/FunPtr.hs b/ivory-examples/examples/FunPtr.hs index 1dbc368e..0e8570cd 100644 --- a/ivory-examples/examples/FunPtr.hs +++ b/ivory-examples/examples/FunPtr.hs @@ -6,13 +6,13 @@ module FunPtr where 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 :: Def ('[] :-> Sint32) test = proc "fun_ptr_test" (body (ret =<< call invoke (procPtr f) 10)) runFunPtr :: IO () diff --git a/ivory-examples/examples/Loop.hs b/ivory-examples/examples/Loop.hs index 0bb7b0ef..27b15d4d 100644 --- a/ivory-examples/examples/Loop.hs +++ b/ivory-examples/examples/Loop.hs @@ -13,7 +13,7 @@ cmodule = package "Loop" $ do runLoopExample :: IO () runLoopExample = runCompiler [cmodule] [] initialOpts { outDir = Nothing } -loopTest0 :: Def ('[] ':-> ()) +loopTest0 :: Def ('[] :-> ()) loopTest0 = proc "loopTest" $ body $ do (0 :: Ix 1) `times` \ _ -> return () retVoid diff --git a/ivory-examples/examples/Overflow.hs b/ivory-examples/examples/Overflow.hs index 66d2ebb2..9d4e69ba 100644 --- a/ivory-examples/examples/Overflow.hs +++ b/ivory-examples/examples/Overflow.hs @@ -6,18 +6,18 @@ module Overflow where import Ivory.Language import Ivory.Compile.C.CmdlineFrontend -ovf1 :: Def ('[Sint8] ':-> Sint8) +ovf1 :: Def ('[Sint8] :-> Sint8) ovf1 = proc "ovf1" $ \ n -> body $ ifte_ (n Sint8) +ovf2 :: Def ('[Sint8] :-> Sint8) ovf2 = proc "ovf2" $ \ n -> requires (n IFloat) +ovf3 :: Def ('[IFloat, IFloat, IBool] :-> IFloat) ovf3 = proc "ovf3" $ \ n m o -> body $ do -- x <- assign (n / m / o) ret $ (o ? (n / m, m / n)) diff --git a/ivory-examples/examples/PID.hs b/ivory-examples/examples/PID.hs index 2ba7ea99..4e56093d 100644 --- a/ivory-examples/examples/PID.hs +++ b/ivory-examples/examples/PID.hs @@ -49,7 +49,7 @@ 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. @@ -68,7 +68,7 @@ pidUpdate = proc "pid_update" $ ret err foo :: Def ('[ Ref s ('Array 3 ('Stored Uint32)) - , 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) @@ -88,11 +88,11 @@ cmodule = package "PID" $ do -- incl pidUpdate -- incl alloc_test -foobar :: Def ('[Uint8] ':-> Uint8) +foobar :: Def ('[Uint8] :-> Uint8) foobar = proc "foobar" $ \x -> body $ do ret (x `iShiftR` (3 `iDiv` 2)) -alloc_test :: Def ('[] ':-> IFloat) +alloc_test :: Def ('[] :-> IFloat) alloc_test = proc "alloc_test" $ body $ do pid <- local (istruct [pid_i .= ival 1]) ret =<< deref (pid ~> pid_i) diff --git a/ivory-examples/examples/PublicPrivate.hs b/ivory-examples/examples/PublicPrivate.hs index aa8f02a5..60c8554d 100644 --- a/ivory-examples/examples/PublicPrivate.hs +++ b/ivory-examples/examples/PublicPrivate.hs @@ -23,14 +23,14 @@ privateFoo :: MemArea ('Struct "Foo") privateFoo = area "private_foo" $ Just (istruct [foo_i .= ival 0, foo_cnt .= ival 0]) -privUpdate :: Def ('[Sint32] ':-> ()) +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) -pubUpdate :: Def ('[Sint32] ':-> ()) +pubUpdate :: Def ('[Sint32] :-> ()) pubUpdate = proc "pubUpdate" $ \v -> body $ do call_ privUpdate v diff --git a/ivory-examples/examples/SizeOf.hs b/ivory-examples/examples/SizeOf.hs index a8beb873..a7430c70 100644 --- a/ivory-examples/examples/SizeOf.hs +++ b/ivory-examples/examples/SizeOf.hs @@ -19,7 +19,7 @@ struct foo |] -test :: Def ('[] ':-> Uint8) +test :: Def ('[] :-> Uint8) test = proc "sizeof_test" (body (ret (sizeOf (Proxy :: Proxy ('Struct "foo"))))) cmodule :: Module diff --git a/ivory-examples/examples/String.hs b/ivory-examples/examples/String.hs index e48deac1..080d7a49 100644 --- a/ivory-examples/examples/String.hs +++ b/ivory-examples/examples/String.hs @@ -7,13 +7,13 @@ module String where 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 diff --git a/ivory-hw/src/Ivory/HW/Prim.hs b/ivory-hw/src/Ivory/HW/Prim.hs index a967a1be..0eceea1b 100644 --- a/ivory-hw/src/Ivory/HW/Prim.hs +++ b/ivory-hw/src/Ivory/HW/Prim.hs @@ -22,13 +22,13 @@ hw_moduledef = do class IvoryBits a => IvoryIOReg a where ioRegSize :: a -> Integer - ioRegRead :: Def ('[Uint32] ':-> a) - ioRegWrite :: Def ('[Uint32, a] ':-> ()) + ioRegRead :: Def ('[Uint32] :-> a) + ioRegWrite :: Def ('[Uint32, a] :-> ()) -ioRegReadU8 :: Def ('[Uint32] ':-> Uint8) +ioRegReadU8 :: Def ('[Uint32] :-> Uint8) ioRegReadU8 = importProc "ivory_hw_io_read_u8" "ivory_hw_prim.h" -ioRegWriteU8 :: Def ('[Uint32, Uint8] ':-> ()) +ioRegWriteU8 :: Def ('[Uint32, Uint8] :-> ()) ioRegWriteU8 = importProc "ivory_hw_io_write_u8" "ivory_hw_prim.h" instance IvoryIOReg Uint8 where @@ -36,10 +36,10 @@ instance IvoryIOReg Uint8 where ioRegRead = ioRegReadU8 ioRegWrite = ioRegWriteU8 -ioRegReadU16 :: Def ('[Uint32] ':-> Uint16) +ioRegReadU16 :: Def ('[Uint32] :-> Uint16) ioRegReadU16 = importProc "ivory_hw_io_read_u16" "ivory_hw_prim.h" -ioRegWriteU16 :: Def ('[Uint32, Uint16] ':-> ()) +ioRegWriteU16 :: Def ('[Uint32, Uint16] :-> ()) ioRegWriteU16 = importProc "ivory_hw_io_write_u16" "ivory_hw_prim.h" instance IvoryIOReg Uint16 where @@ -47,10 +47,10 @@ instance IvoryIOReg Uint16 where ioRegRead = ioRegReadU16 ioRegWrite = ioRegWriteU16 -ioRegReadU32 :: Def ('[Uint32] ':-> Uint32) +ioRegReadU32 :: Def ('[Uint32] :-> Uint32) ioRegReadU32 = importProc "ivory_hw_io_read_u32" "ivory_hw_prim.h" -ioRegWriteU32 :: Def ('[Uint32, Uint32] ':-> ()) +ioRegWriteU32 :: Def ('[Uint32, Uint32] :-> ()) ioRegWriteU32 = importProc "ivory_hw_io_write_u32" "ivory_hw_prim.h" instance IvoryIOReg Uint32 where diff --git a/ivory-model-check/test/Heartbeat.hs b/ivory-model-check/test/Heartbeat.hs index 6feb1ff5..b2a4bf00 100644 --- a/ivory-model-check/test/Heartbeat.hs +++ b/ivory-model-check/test/Heartbeat.hs @@ -50,7 +50,7 @@ heartbeatWrapper = wrapPackRep "mavlink_heartbeat" $ packStruct , packLabel mavlink_version ] -packUnpack :: Def ('[Ref s1 ('Struct "heartbeat_msg")] ':-> ()) +packUnpack :: Def ('[Ref s1 ('Struct "heartbeat_msg")] :-> ()) packUnpack = proc "heartbeat_pack_unpack" $ \ msg -> body $ do let rep = wrappedPackRep heartbeatWrapper buf <- local (iarray [] :: Init ('Array 9 ('Stored Uint8))) diff --git a/ivory-model-check/test/PPM.hs b/ivory-model-check/test/PPM.hs index 69f0946b..0f3c5465 100644 --- a/ivory-model-check/test/PPM.hs +++ b/ivory-model-check/test/PPM.hs @@ -133,7 +133,7 @@ invalidate = do -- ms_no_sample modeswitch -- am_no_sample armingmachine -new_sample_proc :: Def('[Ref s PPMs, ITime ] ':-> ()) +new_sample_proc :: Def('[Ref s PPMs, ITime ] :-> ()) new_sample_proc = proc "ppm_new_sample_proc" $ \ppms tm -> body $ do all_good <- local (ival true) arrayMap $ \ix -> when (ix IBool valid_ppm p = p >=? minBound .&& p <=? maxBound -scale_proc :: Def ('[PPM, Uint16, IFloat, IFloat, PPM] ':-> IFloat) +scale_proc :: Def ('[PPM, Uint16, IFloat, IFloat, PPM] :-> IFloat) scale_proc = proc "ppm_scale_proc" $ \center range outmin outmax input -> requires ( (range /=? 0) .&& valid_ppm input @@ -210,7 +210,7 @@ valid_ui f = f >=? (-1.0) .&& f <=? (1.0) ppm_decode_ui_proc :: Def ('[ Ref s0 ('Array 8 ('Stored PPM)) , Ref s1 ('Struct "userinput_result") , ITime - ] ':-> ()) + ] :-> ()) ppm_decode_ui_proc = proc "ppm_decode_userinput" $ \ppms ui now -> requires (checkStored (ppms ! 0) valid_ppm) $ requires (checkStored (ppms ! 1) valid_ppm) $ diff --git a/ivory-model-check/test/RingBuffer.hs b/ivory-model-check/test/RingBuffer.hs index 2fc7312e..50cb35b9 100644 --- a/ivory-model-check/test/RingBuffer.hs +++ b/ivory-model-check/test/RingBuffer.hs @@ -77,7 +77,7 @@ ringBuffer s = RingBuffer r <- deref remove' return (i ==? r) - push_proc :: Def('[ConstRef s a] ':-> IBool) + push_proc :: Def('[ConstRef s a] :-> IBool) push_proc = proc (named "push") $ \v -> -- requires/ensures in terms of hidden state? body $ do @@ -88,7 +88,7 @@ ringBuffer s = RingBuffer incr insert' >>= store insert' ret true - pop_proc :: Def('[Ref s a] ':-> IBool) + pop_proc :: Def('[Ref s a] :-> IBool) pop_proc = proc (named "pop") $ \v -> body $ do e <- isEmpty' ifte_ e (ret false) $ do @@ -126,7 +126,7 @@ isEmpty i r = i' ==? r' i' = fromIx i r' = fromIx r -push_pop_inv :: Def('[ConstRef s ('Stored Uint8), ConstRef s ('Stored Uint8)] ':-> ()) +push_pop_inv :: Def('[ConstRef s ('Stored Uint8), ConstRef s ('Stored Uint8)] :-> ()) push_pop_inv = proc "push_pop_inv" $ \x y -> -- assume buffer is empty to start requires (checkStored insert (\i -> checkStored remove (\r -> diff --git a/ivory-model-check/test/Test.hs b/ivory-model-check/test/Test.hs index 06665ab5..bf36332d 100644 --- a/ivory-model-check/test/Test.hs +++ b/ivory-model-check/test/Test.hs @@ -113,7 +113,7 @@ mkNotError _ _ = error "Absurd" -------------------------------------------------------------------------------- -- test modules -foo1 :: Def ('[Uint8, Uint8] ':-> ()) +foo1 :: Def ('[Uint8, Uint8] :-> ()) foo1 = L.proc "foo1" $ \y x -> body $ do ifte_ (y ()) +foo2 :: Def ('[] :-> ()) foo2 = L.proc "foo2" $ body $ do x <- local (ival (0 :: Uint8)) store x 3 @@ -143,7 +143,7 @@ m2 = package "foo2" (incl foo2) ----------------------- -foo3 :: Def ('[] ':-> ()) +foo3 :: Def ('[] :-> ()) foo3 = L.proc "foo3" $ body $ do x <- local (ival (1 :: Sint32)) -- since ivory loops are bounded, we can just unroll the whole thing! @@ -157,7 +157,7 @@ m3 = package "foo3" (incl foo3) ----------------------- -foo4 :: Def ('[] ':-> ()) +foo4 :: Def ('[] :-> ()) foo4 = L.proc "foo4" $ body $ do x <- local (ival (1 :: Sint32)) -- store x (7 .% 2) @@ -172,7 +172,7 @@ m4 = package "foo4" (incl foo4) ----------------------- -foo5 :: Def ('[] ':-> ()) +foo5 :: Def ('[] :-> ()) foo5 = L.proc "foo5" $ body $ do x <- local (ival (1 :: Sint32)) -- for loops from 0 to n-1, inclusive @@ -188,7 +188,7 @@ m5 = package "foo5" (incl foo5) ----------------------- -foo6 :: Def ('[Uint8] ':-> ()) +foo6 :: Def ('[Uint8] :-> ()) foo6 = L.proc "foo6" $ \x -> body $ do y <- local (ival (0 :: Uint8)) ifte_ (x Uint8) +foo7 :: Def ('[Uint8, Uint8] :-> Uint8) foo7 = L.proc "foo7" $ \x y -> requires (x + y <=? 255) $ body $ do @@ -220,7 +220,7 @@ m7 = package "foo7" (incl foo7) ----------------------- -foo8 :: Def ('[Uint8] ':-> Uint8) +foo8 :: Def ('[Uint8] :-> Uint8) foo8 = L.proc "foo8" $ \x -> body $ do let y = x .% 3 L.assert (y ()) +foo9 :: Def ('[Ref s ('L.Struct "foo2")] :-> ()) foo9 = L.proc "foo9" $ \f -> body $ do st <- local (istruct [aFoo .= ival 0]) a <- deref (st ~> aFoo) @@ -257,7 +257,7 @@ m9 = package "foo9" $ do ----------------------- -foo10 :: Def ('[Uint8] ':-> Uint8) +foo10 :: Def ('[Uint8] :-> Uint8) foo10 = L.proc "foo10" $ \x -> requires (x r ==? x + 1) @@ -270,7 +270,7 @@ m10 = package "foo10" (incl foo10) ----------------------- -foo11 :: Def ('[Ix 10] ':-> ()) +foo11 :: Def ('[Ix 10] :-> ()) foo11 = L.proc "foo11" $ \n -> requires (n >=? 1) $ body $ do @@ -284,7 +284,7 @@ m11 = package "foo11" (incl foo11) ----------------------- -foo12 :: Def ('[Uint8] ':-> Uint8) +foo12 :: Def ('[Uint8] :-> Uint8) foo12 = L.proc "foo12" $ \n -> ensures (\r -> r ==? n) $ body $ do @@ -298,7 +298,7 @@ m12 = package "foo12" (incl foo12) ----------------------- -foo13 :: Def ('[Uint8, Uint8] ':-> Uint8) +foo13 :: Def ('[Uint8, Uint8] :-> Uint8) foo13 = L.proc "foo13" $ \x y -> requires (x <=? 15) $ requires (y <=? 15) @@ -309,7 +309,7 @@ m13 = package "foo13" (incl foo13) ----------------------- -foo14 :: Def ('[Uint8, Uint8] ':-> Uint8) +foo14 :: Def ('[Uint8, Uint8] :-> Uint8) foo14 = L.proc "foo14" $ \x y -> body $ ret (x * y) @@ -318,7 +318,7 @@ m14 = package "foo14" (incl foo14) ----------------------- -foo15 :: Def ('[Ix 10] ':-> Uint8) +foo15 :: Def ('[Ix 10] :-> Uint8) foo15 = L.proc "foo15" $ \n -> requires (n >=? 1) $ ensures (\r -> r <=? 5) @@ -331,7 +331,7 @@ m15 = package "foo15" (incl foo15) ----------------------- -foo16 :: Def ('[] ':-> ()) +foo16 :: Def ('[] :-> ()) foo16 = L.proc "foo16" $ body $ do (stack_array :: Ref ('Stack s) ('Array 10 ('Stored IFloat))) <- local (iarray []) store (stack_array ! 0) 5 @@ -343,7 +343,7 @@ m16 = package "foo16" (incl foo16) ----------------------- -foo17 :: Def ('[ Ref 'Global ('Array 10 ('Stored Uint32))] ':-> ()) +foo17 :: Def ('[ Ref 'Global ('Array 10 ('Stored Uint32))] :-> ()) foo17 = L.proc "foo17" $ \a -> body $ do b <- local (iarray [ival 0, ival 1]) refCopy b a @@ -355,7 +355,7 @@ m17 = package "foo17" (incl foo17) ----------------------- -foo18 :: Def ('[Ref s ('L.Struct "foo2")] ':-> Ref s ('L.Struct "foo2")) +foo18 :: Def ('[Ref s ('L.Struct "foo2")] :-> Ref s ('L.Struct "foo2")) foo18 = L.proc "foo18" $ \f -> requires (checkStored (f ~> aFoo) (\a -> a >? 0)) $ requires (checkStored (f ~> aFoo) (\a -> a ()) +foo19 :: Def('[Ref s ('Array 1 ('Stored Uint32))] :-> ()) foo19 = L.proc "foo19" $ \ppms -> body $ do all_good <- local (ival L.true) ppm_last <- local (iarray []) diff --git a/ivory-opts/src/Ivory/Opts/SanityCheck.hs b/ivory-opts/src/Ivory/Opts/SanityCheck.hs index f6eab69c..b6637910 100644 --- a/ivory-opts/src/Ivory/Opts/SanityCheck.hs +++ b/ivory-opts/src/Ivory/Opts/SanityCheck.hs @@ -23,8 +23,6 @@ module Ivory.Opts.SanityCheck , showDupDefs ) where -import System.IO (hPutStrLn, stderr) - import Control.Monad (unless) import qualified Data.List as L import qualified Data.Map as M @@ -33,7 +31,6 @@ import MonadLib (Id, StateM (..), WriterT, runId, runStateT, runWriterT, sets_) - import Text.PrettyPrint hiding ((<>)) import qualified Ivory.Language.Array as I @@ -71,7 +68,7 @@ showError err = case err of $$ text "but is used with type:" $$ nest 4 (quotes (pretty expected)) -showSanityChkModule :: ModResult Result -> IO () +showSanityChkModule :: ModResult Result -> Doc showSanityChkModule res = showModErrs go res where go :: Result -> Doc @@ -171,10 +168,11 @@ sanityCheck ms = map goMod ms | m <- ms ] -showDupDefs :: [String] -> IO () +showDupDefs :: [String] -> Doc showDupDefs dups = - if null dups then return () - else hPutStrLn stderr $ render (vcat (map docDups dups) $$ empty) + case dups of + [] -> empty + _ -> vcat (map docDups dups) where docDups x = (text "*** WARNING" <> colon) <+> quotes (text x) diff --git a/ivory-opts/src/Ivory/Opts/TypeCheck.hs b/ivory-opts/src/Ivory/Opts/TypeCheck.hs index 37b13ceb..dca4ee6d 100644 --- a/ivory-opts/src/Ivory/Opts/TypeCheck.hs +++ b/ivory-opts/src/Ivory/Opts/TypeCheck.hs @@ -106,8 +106,10 @@ showWarning w = -> "Array contains unused initializers." ) --- Boolean says whether to show warnings (True) or not. -showTyChkModule :: Bool -> ModResult Result -> IO () +showTyChkModule + :: Bool -- ^ show warnings + -> ModResult Result + -> Doc showTyChkModule b res = showModErrs go res where go :: Result -> Doc diff --git a/ivory-opts/src/Ivory/Opts/Utils.hs b/ivory-opts/src/Ivory/Opts/Utils.hs index 52add370..fa78a57a 100644 --- a/ivory-opts/src/Ivory/Opts/Utils.hs +++ b/ivory-opts/src/Ivory/Opts/Utils.hs @@ -15,8 +15,6 @@ import Ivory.Language.Syntax.Concrete.Location import Ivory.Language.Syntax.Concrete.Pretty (pretty, prettyPrint) import qualified Ivory.Language.Syntax.Type as I -import System.IO (hPutStrLn, stderr) - -------------------------------------------------------------------------------- -- | Type of the expression's arguments. @@ -42,16 +40,13 @@ data ModResult a = ModResult String [SymResult a] deriving (Show, Read, Eq) -- Show the errors for a module. -showModErrs :: Show a => (a -> Doc) -> ModResult a -> IO () +showModErrs :: Show a => (a -> Doc) -> ModResult a -> Doc showModErrs doc (ModResult m errs) = case errs of - [] -> return () + [] -> empty _ -> - hPutStrLn stderr - $ render - $ text "***" <+> text "Module" <+> (text m <> colon) + text "***" <+> text "Module" <+> (text m <> colon) $$ nest 2 (vcat (map (showSymErrs doc) errs)) - $$ empty -- Show the errors for a symbol (area or procedure). showSymErrs :: (a -> Doc) -> SymResult a -> Doc @@ -61,7 +56,6 @@ showSymErrs doc (SymResult sym errs) = _ -> text "***" <+> text "Symbol" <+> (text sym <> colon) $$ nest 2 (vcat (map doc errs)) - $$ empty showWithLoc :: (a -> Doc) -> Located a -> Doc showWithLoc sh (Located loc a) = diff --git a/ivory-quickcheck/src/Ivory/QuickCheck.hs b/ivory-quickcheck/src/Ivory/QuickCheck.hs index d45b1ca5..8680bdfe 100644 --- a/ivory-quickcheck/src/Ivory/QuickCheck.hs +++ b/ivory-quickcheck/src/Ivory/QuickCheck.hs @@ -66,7 +66,7 @@ checkWith :: Int -- ^ The number of inputs to generate. -> Opts -- ^ Options to pass to the Ivory compiler. -> [Module] -- ^ Modules we need to have in scope. -> Module -- ^ The defining module. - -> Def (args ':-> IBool) -- ^ The property to check. + -> Def (args :-> IBool) -- ^ The property to check. -> IO () checkWith n opts deps m prop@(DefProc p) = do inputs <- sampleProc m p n @@ -89,14 +89,14 @@ checkWith _ _ _ _ _ = error "I can only check normal Ivory procs!" check :: Int -- ^ The number of inputs to generate. -> [Module] -- ^ Modules we need to have in scope. -> Module -- ^ The defining module. - -> Def (args ':-> IBool) -- ^ The property to check. + -> Def (args :-> IBool) -- ^ The property to check. -> IO () check n deps m p = checkWith n (initialOpts { outDir = Just "test"}) deps m p -- | Make a @check@able property from an arbitrary Ivory procedure. The -- property will simply check that the contracts are satisfied. -contract :: Def (args ':-> res) -> Def (args ':-> IBool) -contract (DefProc (I.Proc {..})) +contract :: Def (args :-> res) -> Def (args :-> IBool) +contract (DefProc I.Proc{..}) = DefProc I.Proc { I.procSym = procSym ++ "__contract_check" , I.procRetTy = I.TyBool @@ -117,7 +117,7 @@ mkUnique = do return i sampleProc :: Module -> I.Proc -> Int -> IO [I.Block] -sampleProc m@(I.Module {..}) p@(I.Proc {..}) n +sampleProc m@I.Module{..} p@I.Proc{..} n = do c <- newIORef 0 let ?counter = c allInits <- fmap transpose $ forM procArgs $ \ (I.Typed t _) -> @@ -154,7 +154,7 @@ getVisible xs = I.public xs ++ I.private xs mkCheck :: (?counter :: IORef Integer) => I.Proc -> [I.Var] -> IO I.Block -mkCheck (I.Proc {..}) args = do +mkCheck I.Proc{..} args = do n <- mkUnique let b = mkVar n let c = [ I.Call I.TyBool (Just b) (I.NameSym procSym) @@ -269,7 +269,7 @@ sampleDouble = do sampleStruct :: (?counter :: IORef Integer) => I.Module -> String -> IO [(I.Var, I.Block)] -sampleStruct m@(I.Module {..}) ty +sampleStruct m@I.Module{..} ty = case find (\s -> ty == I.structName s) structs of Just (I.Struct _ fields) -> repeatIO $ do (vars, blcks) <- fmap unzip $ forM fields $ \ (I.Typed t _) -> diff --git a/ivory-quickcheck/test/Test.hs b/ivory-quickcheck/test/Test.hs index 3da26a36..072eef10 100644 --- a/ivory-quickcheck/test/Test.hs +++ b/ivory-quickcheck/test/Test.hs @@ -59,20 +59,20 @@ shouldFail = testGroup "should be unsafe" , mkFailure foo14 m14 ] -mkSuccess :: Def (args ':-> res) -> Module -> TestTree +mkSuccess :: Def (args :-> res) -> Module -> TestTree mkSuccess d@(I.DefProc p) m = testCase (I.procSym p) $ do (o, r) <- quickCheck d m assertBool ("Expected quickcheck to pass: output:\n" ++ o) r mkSuccess x _ = error $ "Expected I.DefProc but got " <> show x -mkFailure :: Def (args ':-> res) -> Module -> TestTree +mkFailure :: Def (args :-> res) -> Module -> TestTree mkFailure d@(I.DefProc p) m = testCase (I.procSym p) $ do (o, r) <- quickCheck d m assertBool ("Expected quickcheck to fail: output:\n" ++ o) (not r) mkFailure x _ = error $ "Expected I.DefProc but got " <> show x -quickCheck :: Def (args ':-> res) -> Module -> IO (String, Bool) +quickCheck :: Def (args :-> res) -> Module -> IO (String, Bool) quickCheck d@(I.DefProc p) m = do tmpDir <- getTemporaryDirectory let testDir = tmpDir "ivory-quickcheck" I.procSym p @@ -90,7 +90,7 @@ quickCheck x _ = error $ "Expected I.DefProc but got " <> show x -------------------------------------------------------------------------------- -- test modules -foo1 :: Def ('[Ix 10, Ix 10] ':-> ()) +foo1 :: Def ('[Ix 10, Ix 10] :-> ()) foo1 = L.proc "foo1" $ \y x -> body $ do ifte_ (y ()) +foo6 :: Def ('[Uint8] :-> ()) foo6 = L.proc "foo6" $ \x -> body $ do y <- local (ival (0 :: Uint8)) ifte_ (x Uint8) +foo7 :: Def ('[Uint8, Uint8] :-> Uint8) foo7 = L.proc "foo7" $ \x y -> requires (x + y <=? 255) $ body $ do @@ -138,7 +138,7 @@ m7 = package "foo7" (incl foo7) ----------------------- -foo8 :: Def ('[Uint8] ':-> Uint8) +foo8 :: Def ('[Uint8] :-> Uint8) foo8 = L.proc "foo8" $ \x -> body $ do let y = x .% 3 L.assert (y ()) +foo9 :: Def ('[Ref s ('L.Struct "foo2")] :-> ()) foo9 = L.proc "foo9" $ \f -> body $ do st <- local (istruct [aFoo .= ival 0]) a <- deref (st ~> aFoo) @@ -175,7 +175,7 @@ m9 = package "foo9" $ do ----------------------- -foo10 :: Def ('[Uint8] ':-> Uint8) +foo10 :: Def ('[Uint8] :-> Uint8) foo10 = L.proc "foo10" $ \x -> requires (x r ==? x + 1) @@ -188,7 +188,7 @@ m10 = package "foo10" (incl foo10) ----------------------- -foo11 :: Def ('[Ix 10] ':-> ()) +foo11 :: Def ('[Ix 10] :-> ()) foo11 = L.proc "foo11" $ \n -> requires (n >=? 0) $ body $ do @@ -202,7 +202,7 @@ m11 = package "foo11" (incl foo11) ----------------------- -foo12 :: Def ('[Uint8] ':-> Uint8) +foo12 :: Def ('[Uint8] :-> Uint8) foo12 = L.proc "foo12" $ \n -> ensures (\r -> r ==? n) $ body $ do @@ -216,7 +216,7 @@ m12 = package "foo12" (incl foo12) ----------------------- -foo13 :: Def ('[Uint8, Uint8] ':-> Uint8) +foo13 :: Def ('[Uint8, Uint8] :-> Uint8) foo13 = L.proc "foo13" $ \x y -> requires (x <=? 15) $ requires (y <=? 15) @@ -227,7 +227,7 @@ m13 = package "foo13" (incl foo13) ----------------------- -foo14 :: Def ('[Uint8, Uint8] ':-> Uint8) +foo14 :: Def ('[Uint8, Uint8] :-> Uint8) foo14 = L.proc "foo14" $ \x y -> ensures (\r -> r >=? x L..&& r >=? y) $ body $ ret (x * y) @@ -237,7 +237,7 @@ m14 = package "foo14" (incl foo14) ----------------------- -foo15 :: Def ('[Ix 10] ':-> Uint8) +foo15 :: Def ('[Ix 10] :-> Uint8) foo15 = L.proc "foo15" $ \n -> requires (n >=? 0) $ ensures (\r -> r <=? 5) @@ -251,7 +251,7 @@ m15 = package "foo15" (incl foo15) ----------------------- -foo17 :: Def ('[ Ref 'Global ('Array 10 ('Stored Uint32))] ':-> ()) +foo17 :: Def ('[ Ref 'Global ('Array 10 ('Stored Uint32))] :-> ()) foo17 = L.proc "foo17" $ \a -> body $ do b <- local (iarray [ival 0, ival 1]) refCopy b a @@ -263,7 +263,7 @@ m17 = package "foo17" (incl foo17) ----------------------- -foo18 :: Def ('[Ref s ('L.Struct "foo2")] ':-> Ref s ('L.Struct "foo2")) +foo18 :: Def ('[Ref s ('L.Struct "foo2")] :-> Ref s ('L.Struct "foo2")) foo18 = L.proc "foo18" $ \f -> requires (checkStored (f ~> aFoo) (\a -> a >? 0)) $ requires (checkStored (f ~> aFoo) (\a -> a ()) +foo19 :: Def('[Ref s ('Array 1 ('Stored Uint32))] :-> ()) foo19 = L.proc "foo19" $ \ppms -> body $ do all_good <- local (ival L.true) ppm_last <- local (iarray []) @@ -300,7 +300,7 @@ foo19 = L.proc "foo19" $ \ppms -> body $ do L.when b $ do (arrayMap $ \ix -> (deref (ppms ! ix) >>= store (ppm_last ! ix))) store ppm_valid L.true - + valid <- deref ppm_valid ppm <- deref (ppm_last ! 0) L.assert (L.iNot valid .|| (ppm >=? 800 L..&& ppm <=? 2000)) diff --git a/ivory-serialize/src/Ivory/Serialize/Atoms.hs b/ivory-serialize/src/Ivory/Serialize/Atoms.hs index c0c9b9d3..dee8a7a9 100644 --- a/ivory-serialize/src/Ivory/Serialize/Atoms.hs +++ b/ivory-serialize/src/Ivory/Serialize/Atoms.hs @@ -61,7 +61,7 @@ serializeArtifacts = [ Incl $ a serializeHeader ] a f = artifactCabalFile P.getDataDir ("support/" ++ f) ibool :: WrappedPackRep ('Stored IBool) -ibool = wrapPackRep "ibool" (repackV (/=? 0) (? ((1 :: Uint8), 0)) (packRep :: PackRep ('Stored Uint8))) +ibool = wrapPackRep "ibool" (repackV (/=? 0) (? (1 :: Uint8, 0)) (packRep :: PackRep ('Stored Uint8))) instance Packable ('Stored IBool) where packRep = wrappedPackRep ibool @@ -119,23 +119,23 @@ instance Packable ('Stored IDouble) where mkPackRep :: forall a. (IvoryArea ('Stored a), IvoryEq a) => String -> Integer -> WrappedPackRep ('Stored a) mkPackRep ty sz = WrappedPackRep - (PackRep { packGetLE = call_ doGetLE + PackRep { packGetLE = call_ doGetLE , packGetBE = call_ doGetBE , packSetLE = call_ doSetLE , packSetBE = call_ doSetBE - , packSize = sz }) - defs + , packSize = sz } + defs where - doGetLE :: Def ('[ConstRef s1 ('CArray ('Stored Uint8)), Uint32, Ref s2 ('Stored a)] ':-> ()) + doGetLE :: Def ('[ConstRef s1 ('CArray ('Stored Uint8)), Uint32, Ref s2 ('Stored a)] :-> ()) doGetLE = proc ("ivory_serialize_unpack_" ++ ty ++ "_le") $ \ buf offs base -> ensures_ (checkStored base $ \ v -> (buf !! offs) ==? v) $ importFrom serializeHeader - doGetBE :: Def ('[ConstRef s1 ('CArray ('Stored Uint8)), Uint32, Ref s2 ('Stored a)] ':-> ()) + doGetBE :: Def ('[ConstRef s1 ('CArray ('Stored Uint8)), Uint32, Ref s2 ('Stored a)] :-> ()) doGetBE = proc ("ivory_serialize_unpack_" ++ ty ++ "_be") $ \ buf offs base -> ensures_ (checkStored base $ \ v -> (buf !! offs) ==? v) $ importFrom serializeHeader - doSetLE :: Def ('[Ref s1 ('CArray ('Stored Uint8)), Uint32, ConstRef s2 ('Stored a)] ':-> ()) + doSetLE :: Def ('[Ref s1 ('CArray ('Stored Uint8)), Uint32, ConstRef s2 ('Stored a)] :-> ()) doSetLE = proc ("ivory_serialize_pack_" ++ ty ++ "_le") $ \ buf offs base -> ensures_ (checkStored base $ \ v -> (buf !! offs) ==? v) $ importFrom serializeHeader - doSetBE :: Def ('[Ref s1 ('CArray ('Stored Uint8)), Uint32, ConstRef s2 ('Stored a)] ':-> ()) + doSetBE :: Def ('[Ref s1 ('CArray ('Stored Uint8)), Uint32, ConstRef s2 ('Stored a)] :-> ()) doSetBE = proc ("ivory_serialize_pack_" ++ ty ++ "_be") $ \ buf offs base -> ensures_ (checkStored base $ \ v -> (buf !! offs) ==? v) $ importFrom serializeHeader defs = do @@ -144,8 +144,8 @@ mkPackRep ty sz = WrappedPackRep incl doSetLE incl doSetBE -(!!) :: (IvoryRef ref, IvoryExpr (ref s ('CArray ('Stored Uint8))), IvoryExpr a) - => ref s ('CArray ('Stored Uint8)) -> Uint32 -> a +(!!) :: (KnownConstancy c, IvoryExpr a) + => Pointer 'Valid c s ('CArray ('Stored Uint8)) -> Uint32 -> a arr !! ix = I.wrapExpr (I.ExpIndex ty (I.unwrapExpr arr) I.ixRep (I.getUint32 ix)) where ty = I.TyCArray (I.TyWord I.Word8) diff --git a/ivory-serialize/src/Ivory/Serialize/PackRep.hs b/ivory-serialize/src/Ivory/Serialize/PackRep.hs index ac0dacc1..bbf10735 100644 --- a/ivory-serialize/src/Ivory/Serialize/PackRep.hs +++ b/ivory-serialize/src/Ivory/Serialize/PackRep.hs @@ -76,16 +76,16 @@ wrapPackRep name rep = WrappedPackRep , packSetBE = call_ doSetBE }) defs where - doGetLE :: Def ('[ConstRef s1 ('CArray ('Stored Uint8)), Uint32, Ref s2 a] ':-> ()) + doGetLE :: Def ('[ConstRef s1 ('CArray ('Stored Uint8)), Uint32, Ref s2 a] :-> ()) doGetLE = proc (name ++ "_get_le") $ \ buf offs base -> body $ packGetLE rep buf offs base - doGetBE :: Def ('[ConstRef s1 ('CArray ('Stored Uint8)), Uint32, Ref s2 a] ':-> ()) + doGetBE :: Def ('[ConstRef s1 ('CArray ('Stored Uint8)), Uint32, Ref s2 a] :-> ()) doGetBE = proc (name ++ "_get_be") $ \ buf offs base -> body $ packGetBE rep buf offs base - doSetLE :: Def ('[Ref s1 ('CArray ('Stored Uint8)), Uint32, ConstRef s2 a] ':-> ()) + doSetLE :: Def ('[Ref s1 ('CArray ('Stored Uint8)), Uint32, ConstRef s2 a] :-> ()) doSetLE = proc (name ++ "_set_le") $ \ buf offs base -> body $ packSetLE rep buf offs base - doSetBE :: Def ('[Ref s1 ('CArray ('Stored Uint8)), Uint32, ConstRef s2 a] ':-> ()) + doSetBE :: Def ('[Ref s1 ('CArray ('Stored Uint8)), Uint32, ConstRef s2 a] :-> ()) doSetBE = proc (name ++ "_set_be") $ \ buf offs base -> body $ packSetBE rep buf offs base defs = do diff --git a/ivory-stdlib/src/Ivory/Stdlib/Memory.hs b/ivory-stdlib/src/Ivory/Stdlib/Memory.hs index 8be83482..8b0e82ac 100644 --- a/ivory-stdlib/src/Ivory/Stdlib/Memory.hs +++ b/ivory-stdlib/src/Ivory/Stdlib/Memory.hs @@ -29,21 +29,16 @@ into a b = store b =<< deref a -- is fully copied, the @to@ array is full, or index @end@ in the @from@ array -- is reached (index @end@ is not copied). to copy the full @from@ array, let -- @end@ equal 'arrayLen from'. -arrayCopy :: - ( ANat n, ANat m, IvoryRef r - , IvoryExpr (r s2 ('Array m ('Stored t))) - , IvoryExpr (r s2 ('Stored t)) - , IvoryStore t - ) +arrayCopy :: (ANat n, ANat m, IvoryStore t, KnownConstancy c) => Ref s1 ('Array n ('Stored t)) - -> r s2 ('Array m ('Stored t)) + -> Pointer 'Valid c s2 ('Array m ('Stored t)) -> Sint32 -> Sint32 -> Ivory eff () arrayCopy to from toOffset end = do assert (toOffset >=? 0 .&& toOffset =? 0 .&& end <=? frLen) - arrayMap $ go + arrayMap go where -- The index is w.r.t. the from array. go ix = diff --git a/ivory-stdlib/src/Ivory/Stdlib/Operators.hs b/ivory-stdlib/src/Ivory/Stdlib/Operators.hs index 1130566a..c26476b2 100644 --- a/ivory-stdlib/src/Ivory/Stdlib/Operators.hs +++ b/ivory-stdlib/src/Ivory/Stdlib/Operators.hs @@ -8,10 +8,10 @@ import Ivory.Language -- | Infix structure field access and dereference. -- This is a shorthand for 'deref $ s~>x'. -(~>*) :: (IvoryVar a, IvoryStruct sym, IvoryRef ref, IvoryStore a, - IvoryExpr (ref s ('Stored a)), - IvoryExpr (ref s ('Struct sym))) => - ref s ('Struct sym) -> Label sym ('Stored a) -> Ivory eff a +(~>*) :: (IvoryVar a, IvoryStruct sym, IvoryStore a, KnownConstancy c) + => Pointer 'Valid c s ('Struct sym) + -> Label sym ('Stored a) + -> Ivory eff a struct ~>* label = deref (struct~>label) infixl 8 ~>* @@ -36,4 +36,3 @@ ref %=! mf = do (+=) :: (Num a, IvoryStore a) => Ref s ('Stored a) -> a -> Ivory eff () ref += x = ref %= (+ x) - diff --git a/ivory-stdlib/src/Ivory/Stdlib/String.hs b/ivory-stdlib/src/Ivory/Stdlib/String.hs index da82e1e5..ab04cfbb 100644 --- a/ivory-stdlib/src/Ivory/Stdlib/String.hs +++ b/ivory-stdlib/src/Ivory/Stdlib/String.hs @@ -22,7 +22,6 @@ import Data.Char (ord, toLower) import Ivory.Language import Ivory.Language.Array (IxRep) import Ivory.Artifact -import Ivory.Language.Struct import qualified Control.Monad as M import qualified Paths_ivory_stdlib as P @@ -115,35 +114,27 @@ stringArray = map (fromIntegral . ord) ---------------------------------------------------------------------- -- Generic Functions -stringCapacity :: ( IvoryString str - , IvoryRef ref - , IvoryExpr (ref s ('Struct (StructName str))) - , IvoryExpr (ref s ('Array (Capacity ('Struct (StructName str))) ('Stored Uint8))) - , Num n - ) - => ref s str -> n +stringCapacity :: (IvoryString str, Num n, KnownConstancy c) + => Pointer 'Valid c s str -> n stringCapacity str = arrayLen (str ~> stringDataL) -stringData :: ( IvoryString str - , IvoryRef ref - , IvoryExpr (ref s ('Array (Capacity str) ('Stored Uint8))) - , IvoryExpr (ref s ('CArray ('Stored Uint8))) - , IvoryExpr (ref s str)) - => ref s str -> ref s ('CArray ('Stored Uint8)) +stringData :: (IvoryString str, KnownConstancy c) + => Pointer 'Valid c s str + -> Pointer 'Valid c s ('CArray ('Stored Uint8)) stringData x = toCArray (x ~> stringDataL) -- XXX don't export -- | Binding to the C "memcmp" function. memcmp :: Def ('[ ConstRef s1 ('CArray ('Stored Uint8)) , ConstRef s2 ('CArray ('Stored Uint8)) - , Len] ':-> Len) + , Len] :-> Len) memcmp = importProc "memcmp" "string.h" -- XXX don't export -- | Binding to the C "memcpy" function. memcpy :: Def ('[ Ref s1 ('CArray ('Stored Uint8)) , ConstRef s2 ('CArray ('Stored Uint8)) - , Len] ':-> Len) + , Len] :-> Len) memcpy = importProc "memcpy" "string.h" -- | Return the length of a string. @@ -167,8 +158,8 @@ do_istr_eq :: Def ('[ ConstRef s1 ('CArray ('Stored Uint8)) , Len , ConstRef s2 ('CArray ('Stored Uint8)) , Len - ] ':-> IBool) -do_istr_eq = proc "ivory_string_eq" $ \s1 len1 s2 len2 -> body $ do + ] :-> IBool) +do_istr_eq = proc "ivory_string_eq" $ \s1 len1 s2 len2 -> body $ ifte_ (len1 ==? len2) (do r <- call memcmp s1 s2 len1 ret (r ==? 0)) @@ -192,7 +183,7 @@ istr_eq s1 s2 = do string_copy_z :: Def ('[ Ref s1 ('CArray ('Stored Uint8)) , Len , ConstRef s2 ('CArray ('Stored Uint8)) - , Len] ':-> Len) + , Len] :-> Len) string_copy_z = importProc "ivory_stdlib_string_copy_z" "ivory_stdlib_string_prim.h" @@ -251,4 +242,3 @@ stdlibStringArtifacts = ] where supportfile f = artifactCabalFile P.getDataDir ("support/" ++ f) - diff --git a/ivory-tasty/src/Ivory/Tasty.hs b/ivory-tasty/src/Ivory/Tasty.hs index 8a886773..9dff8fbc 100644 --- a/ivory-tasty/src/Ivory/Tasty.hs +++ b/ivory-tasty/src/Ivory/Tasty.hs @@ -16,7 +16,7 @@ -- > someArtifacts :: [Located Artifact] -- > someArtifacts = serializeArtifacts -- --- > someTestedFunction :: Def ('[] ':-> Sint32) +-- > someTestedFunction :: Def ('[] :-> Sint32) -- > someTestedFunction = proc "main" $ body $ do -- > assert false -- > ret 0 @@ -68,7 +68,7 @@ import Test.Tasty.HUnit (assertBool, testCase) data IvoryTestCase = IvoryTestCase { itcName :: String - , itcFun :: Def ('[] ':-> Sint32) + , itcFun :: Def ('[] :-> Sint32) , itcDeps :: ModuleDef , itcExpectSuccess :: Bool } @@ -77,7 +77,7 @@ data IvoryTestCase = IvoryTestCase { -- expecting 0 exit code. mkSuccess :: String - -> Def ('[] ':-> Sint32) + -> Def ('[] :-> Sint32) -> IvoryTestCase mkSuccess name f = IvoryTestCase name f (pure ()) True @@ -85,7 +85,7 @@ mkSuccess name f = IvoryTestCase name f (pure ()) True -- expecting non-0 exit code. mkFailure :: String - -> Def ('[] ':-> Sint32) + -> Def ('[] :-> Sint32) -> IvoryTestCase mkFailure name f = IvoryTestCase name f (pure ()) False diff --git a/ivory-tasty/test/Test.hs b/ivory-tasty/test/Test.hs index 5e7ddeb3..5ce7ea27 100644 --- a/ivory-tasty/test/Test.hs +++ b/ivory-tasty/test/Test.hs @@ -22,20 +22,20 @@ main = defaultMain $ ivoryTestGroup [uartTypes] [] , setDeps (depend uartTypes) $ mkSuccess "test with dependencies" testDeps ] -testSmoke :: Def ('[] ':-> Sint32) +testSmoke :: Def ('[] :-> Sint32) testSmoke = proc "main" $ body $ do ret 0 -testSmokeFailing :: Def ('[] ':-> Sint32) +testSmokeFailing :: Def ('[] :-> Sint32) testSmokeFailing = proc "main" $ body $ do ret 1 -testAssertFailing :: Def ('[] ':-> Sint32) +testAssertFailing :: Def ('[] :-> Sint32) testAssertFailing = proc "main" $ body $ do assert false ret 0 -testDeps :: Def ('[] ':-> Sint32) +testDeps :: Def ('[] :-> Sint32) testDeps = proc "main" $ body $ do (a :: Ref s UARTBuffer) <- local $ stringInit "yolo" lA <- deref (a ~> stringLengthL) diff --git a/ivory/src/Ivory/Language.hs b/ivory/src/Ivory/Language.hs index e1d8696e..5da61c00 100644 --- a/ivory/src/Ivory/Language.hs +++ b/ivory/src/Ivory/Language.hs @@ -1,6 +1,5 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TypeFamilies #-} @@ -9,7 +8,7 @@ module Ivory.Language ( -- * Kinds Area(..) - , Proc(..) + , Proc((:->)), (:->) -- * Types , IvoryType(), IvoryArea() @@ -18,12 +17,19 @@ module Ivory.Language ( , OpaqueType() - -- ** Non-null References - , IvoryRef() + -- ** Pointers + , Pointer() + , Nullability(Nullable, Valid) + , KnownConstancy + + -- *** Non-null References , ConstRef() , IvoryStore() , Ref(), refToPtr, constRef, deref, store, refCopy, refZero + -- *** Nullable Pointers + , Ptr(), nullPtr + -- ** Stack Allocation , IvoryInit(..), Init() , IvoryZeroVal(izeroval) @@ -35,9 +41,6 @@ module Ivory.Language ( -- ** SizeOf , IvorySizeOf, sizeOf - -- ** Nullable Pointers - , Ptr(), nullPtr - -- ** Booleans , IBool(), true, false @@ -226,6 +229,7 @@ import Ivory.Language.Loop import Ivory.Language.MemArea import Ivory.Language.Module import Ivory.Language.Monad +import Ivory.Language.Pointer import Ivory.Language.Proc import Ivory.Language.Proxy import Ivory.Language.Ptr diff --git a/ivory/src/Ivory/Language/Array.hs b/ivory/src/Ivory/Language/Array.hs index cf3d63d6..ce4b2db7 100644 --- a/ivory/src/Ivory/Language/Array.hs +++ b/ivory/src/Ivory/Language/Array.hs @@ -17,6 +17,7 @@ module Ivory.Language.Array ( import Ivory.Language.IBool import Ivory.Language.Area +import Ivory.Language.Pointer import Ivory.Language.Proxy import Ivory.Language.Ref import Ivory.Language.Sint @@ -124,16 +125,15 @@ rawIxVal n = case unwrapExpr n of -- Arrays ---------------------------------------------------------------------- -arrayLen :: forall s len area n ref. - (Num n, ANat len, IvoryArea area, IvoryRef ref) - => ref s ('Array len area) -> n +arrayLen :: forall s len area n c. + (Num n, ANat len, IvoryArea area) + => Pointer 'Valid c s ('Array len area) -> n arrayLen _ = fromInteger (fromTypeNat (aNat :: NatType len)) -- | Array indexing. -(!) :: forall s len area ref. - ( ANat len, IvoryArea area, IvoryRef ref - , IvoryExpr (ref s ('Array len area)), IvoryExpr (ref s area)) - => ref s ('Array len area) -> Ix len -> ref s area +(!) :: forall s len area c. + (ANat len, IvoryArea area, KnownConstancy c) + => Pointer 'Valid c s ('Array len area) -> Ix len -> Pointer 'Valid c s area arr ! ix = wrapExpr (I.ExpIndex ty (unwrapExpr arr) ixRep (getIx ix)) where ty = ivoryArea (Proxy :: Proxy ('Array len area)) diff --git a/ivory/src/Ivory/Language/Bits.hs b/ivory/src/Ivory/Language/Bits.hs index eaaa158b..b0aa8fe7 100644 --- a/ivory/src/Ivory/Language/Bits.hs +++ b/ivory/src/Ivory/Language/Bits.hs @@ -182,11 +182,11 @@ instance TwosComplementCast Uint64 Sint64 -- the two values (x & 0xFF, x >> 8), with the first value safely -- casted to an 8-bit integer. -- --- This is convenient to use with a state monad and "sets", such as: +-- This is convenient to use with a state monad and 'Control.Monad.State.state', such as: -- --- > fst $ runState x $ do --- > a <- sets extractByte --- > b <- sets extractByte +-- > evalState x $ do +-- > a <- state extractByte +-- > b <- state extractByte -- > return (a, b) extractByte :: (BitCast a Uint8) => a -> (Uint8, a) extractByte x = (bitCast x, x `iShiftR` 8) diff --git a/ivory/src/Ivory/Language/CArray.hs b/ivory/src/Ivory/Language/CArray.hs index 7129958e..0e4346aa 100644 --- a/ivory/src/Ivory/Language/CArray.hs +++ b/ivory/src/Ivory/Language/CArray.hs @@ -11,8 +11,8 @@ module Ivory.Language.CArray where import Data.Kind (Type) import Ivory.Language.Area +import Ivory.Language.Pointer import Ivory.Language.Proxy -import Ivory.Language.Ref import Ivory.Language.Struct import Ivory.Language.Type import qualified Ivory.Language.Syntax as I @@ -33,10 +33,9 @@ instance IvoryType a => ToCArray ('Stored a) ('Stored a) instance IvoryStruct sym => ToCArray ('Struct sym) ('Struct sym) -- | Convert from a checked array to one that can be given to a c function. -toCArray :: forall s len area rep ref. - ( ANat len, ToCArray area rep, IvoryRef ref - , IvoryExpr (ref s ('Array len area)) - , IvoryExpr (ref s ('CArray rep))) - => ref s ('Array len area) -> ref s ('CArray rep) +toCArray :: forall s len area rep c. + (ANat len, KnownConstancy c, ToCArray area rep) + => Pointer 'Valid c s ('Array len area) + -> Pointer 'Valid c s ('CArray rep) toCArray ref = wrapExpr $ I.ExpSafeCast ty (unwrapExpr ref) - where ty = ivoryType (Proxy :: Proxy (ref s ('CArray rep))) + where ty = ivoryType (Proxy :: Proxy (Pointer 'Valid c s ('CArray rep))) diff --git a/ivory/src/Ivory/Language/Cond.hs b/ivory/src/Ivory/Language/Cond.hs index d93621ac..96359a04 100644 --- a/ivory/src/Ivory/Language/Cond.hs +++ b/ivory/src/Ivory/Language/Cond.hs @@ -9,9 +9,9 @@ module Ivory.Language.Cond where import Ivory.Language.Area import Ivory.Language.IBool import Ivory.Language.Monad +import Ivory.Language.Pointer import Ivory.Language.Proc import Ivory.Language.Proxy -import Ivory.Language.Ref import Ivory.Language.Type import qualified Ivory.Language.Syntax as I @@ -41,12 +41,9 @@ newtype Cond = Cond check :: IBool -> Cond check bool = Cond (return (I.CondBool (unwrapExpr bool))) -checkStored' :: forall ref s a c. - ( CheckStored c - , IvoryVar a - , IvoryRef ref - , IvoryVar (ref s ('Stored a)) - ) => (c -> Cond) -> ref s ('Stored a) -> (a -> c) -> Cond +checkStored' :: forall co s a c. + (CheckStored c, IvoryVar a, KnownConstancy co) + => (c -> Cond) -> Pointer 'Valid co s ('Stored a) -> (a -> c) -> Cond checkStored' c ref prop = Cond $ do n <- freshVar "pre" let ty = ivoryType (Proxy :: Proxy a) @@ -54,8 +51,8 @@ checkStored' c ref prop = Cond $ do return (I.CondDeref ty (unwrapExpr ref) n b) class CheckStored c where - checkStored :: (IvoryVar a, IvoryRef ref, IvoryVar (ref s ('Stored a))) - => ref s ('Stored a) -> (a -> c) -> Cond + checkStored :: (IvoryVar a, KnownConstancy co) + => Pointer 'Valid co s ('Stored a) -> (a -> c) -> Cond instance CheckStored IBool where checkStored = checkStored' check @@ -115,4 +112,3 @@ instance Ensures IBool where instance Ensures Cond where ensures = ensures' id ensures_ = ensures_' id - diff --git a/ivory/src/Ivory/Language/Proc.hs b/ivory/src/Ivory/Language/Proc.hs index be58a394..949198bb 100644 --- a/ivory/src/Ivory/Language/Proc.hs +++ b/ivory/src/Ivory/Language/Proc.hs @@ -28,6 +28,9 @@ import qualified Ivory.Language.Syntax as AST -- | The kind of procedures. data Proc k = [k] :-> k +-- | Allow to use (:->) on type level without a tick +type (:->) = '(:->) + -- | Typeclass for procedure types, parametrized over the C procedure's -- signature, to produce a value representing their signature. class ProcType (sig :: Proc Type) where @@ -38,16 +41,16 @@ class ProcType (sig :: Proc Type) where -- Base case: C procedure taking no arguments and returning an -- 'IvoryType'. -instance IvoryType r => ProcType ('[] ':-> r) where +instance IvoryType r => ProcType ('[] :-> r) where procType _ = (ivoryType (Proxy :: Proxy r),[]) -- Inductive case: Anything in 'ProcType' is still in 'ProcType' if it -- has another 'IvoryType' argument prepended to its signature. -instance (IvoryType a, ProcType (args ':-> r)) - => ProcType ((a ': args) ':-> r) where +instance (IvoryType a, ProcType (args :-> r)) + => ProcType ((a ': args) :-> r) where procType _ = (r, ivoryType (Proxy :: Proxy a) : args) where - (r,args) = procType (Proxy :: Proxy (args ':-> r)) + (r,args) = procType (Proxy :: Proxy (args :-> r)) -- Function Pointers ----------------------------------------------------------- @@ -120,8 +123,8 @@ proc name impl = defproc -- procedure, but for void procedures there's often nothing to constrain -- the return type. This function is a type-constrained version of -- 'proc' that just forces the return type to be '()'. -voidProc :: IvoryProcDef (args ':-> ()) impl => - AST.Sym -> impl -> Def (args ':-> ()) +voidProc :: IvoryProcDef (args :-> ()) impl => + AST.Sym -> impl -> Def (args :-> ()) voidProc = proc @@ -161,14 +164,14 @@ class ProcType proc => IvoryProcDef (proc :: Proc Type) impl | impl -> proc wher procDef :: Closure -> Proxy proc -> impl -> ([AST.Var], Definition) -- Base case: No arguments in C signature -instance IvoryType ret => IvoryProcDef ('[] ':-> ret) (Body ret) where +instance IvoryType ret => IvoryProcDef ('[] :-> ret) (Body ret) where procDef env _ b = (getEnv env, Defined (snd (primRunIvory (runBody b)))) -- Inductive case: Remove first argument from C signature, and -- parametrize 'impl' over another argument of the same type. -instance (IvoryVar a, IvoryProcDef (args ':-> ret) k) - => IvoryProcDef ((a ': args) ':-> ret) (a -> k) where - procDef env _ k = procDef env' (Proxy :: Proxy (args ':-> ret)) (k arg) +instance (IvoryVar a, IvoryProcDef (args :-> ret) k) + => IvoryProcDef ((a ': args) :-> ret) (a -> k) where + procDef env _ k = procDef env' (Proxy :: Proxy (args :-> ret)) (k arg) where (var,env') = genVar env arg = wrapVar var @@ -230,7 +233,7 @@ instance WrapIvory ImportFrom where importFrom :: String -> ImportFrom a importFrom h = ImportFrom (return h) -instance IvoryType ret => IvoryProcDef ('[] ':-> ret) (ImportFrom ret) where +instance IvoryType ret => IvoryProcDef ('[] :-> ret) (ImportFrom ret) where procDef env _ b = (getEnv env, Imported header reqs ens) where (header, block) = primRunIvory (runImportFrom b) @@ -259,7 +262,7 @@ class IvoryCall (proc :: Proc Type) (eff :: E.Effects) impl -- | Recursive helper call. 'proc' encodes a C procedure type, and -- this call has two main parts: - -- + -- -- * If 'proc' contains arguments, then 'impl' must be a function -- type causing this whole call to expect an Ivory value that was -- passed in to apply to the C procedure. In this case, 'proc' is @@ -271,7 +274,7 @@ class IvoryCall (proc :: Proc Type) (eff :: E.Effects) impl -- list applied to it, and captures and returns the result. callAux :: AST.Name -> Proxy proc -> [AST.Typed AST.Expr] -> impl -instance IvoryVar r => IvoryCall ('[] ':-> r) eff (Ivory eff r) where +instance IvoryVar r => IvoryCall ('[] :-> r) eff (Ivory eff r) where -- Base case ('proc' takes no arguments, 'impl' is just an Ivory -- effect): callAux sym _ args = do @@ -279,14 +282,14 @@ instance IvoryVar r => IvoryCall ('[] ':-> r) eff (Ivory eff r) where emit (AST.Call (ivoryType (Proxy :: Proxy r)) (Just r) sym (reverse args)) return (wrapVar r) -instance (IvoryVar a, IvoryVar r, IvoryCall (args ':-> r) eff impl) - => IvoryCall ((a ': args) ':-> r) eff (a -> impl) where - -- Inductive case: note that 'proc' reduces from ((a ': args) ':-> r) - -- down to (args ':-> r) in the proxy, and that 'impl' is (a -> impl) - -- and we put that 'a' onto the list of arguments. +instance (IvoryVar a, IvoryVar r, IvoryCall (args :-> r) eff impl) + => IvoryCall ((a ': args) :-> r) eff (a -> impl) where + -- Inductive case: note that 'proc' reduces from ((a ': args) :-> r) + -- down to (args :-> r) in the proxy, and that 'impl' is (a -> impl) + -- and we put that 'a' onto the list of arguments. callAux sym _ args a = callAux sym rest args' where - rest = Proxy :: Proxy (args ':-> r) + rest = Proxy :: Proxy (args :-> r) args' = typedExpr a : args @@ -308,15 +311,15 @@ class IvoryCall_ (proc :: Proc Type) (eff :: E.Effects) impl where callAux_ :: AST.Name -> Proxy proc -> [AST.Typed AST.Expr] -> impl -instance IvoryType r => IvoryCall_ ('[] ':-> r) eff (Ivory eff ()) where +instance IvoryType r => IvoryCall_ ('[] :-> r) eff (Ivory eff ()) where callAux_ sym _ args = do emit (AST.Call (ivoryType (Proxy :: Proxy r)) Nothing sym (reverse args)) -instance (IvoryVar a, IvoryType r, IvoryCall_ (args ':-> r) eff impl) - => IvoryCall_ ((a ': args) ':-> r) eff (a -> impl) where +instance (IvoryVar a, IvoryType r, IvoryCall_ (args :-> r) eff impl) + => IvoryCall_ ((a ': args) :-> r) eff (a -> impl) where callAux_ sym _ args a = callAux_ sym rest args' where - rest = Proxy :: Proxy (args ':-> r) + rest = Proxy :: Proxy (args :-> r) args' = typedExpr a : args -- Return ---------------------------------------------------------------------- diff --git a/ivory/src/Ivory/Language/Ref.hs b/ivory/src/Ivory/Language/Ref.hs index e434f814..e27ed7bc 100644 --- a/ivory/src/Ivory/Language/Ref.hs +++ b/ivory/src/Ivory/Language/Ref.hs @@ -1,7 +1,8 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} -{-# LANGUAGE KindSignatures #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-} @@ -13,7 +14,6 @@ module Ivory.Language.Ref ( ConstRef - , IvoryRef , IvoryStore , Ref , constRef @@ -37,8 +37,6 @@ import Ivory.Language.Scope import qualified Ivory.Language.Syntax as I import Ivory.Language.Type -import Data.Kind (Type) - -- References ------------------------------------------------------------------ -- | A non-null pointer to a memory area. @@ -55,19 +53,16 @@ type ConstRef = Pointer 'Valid 'Const -- Dereferencing --------------------------------------------------------------- --- | TODO remove class, leave function only -class IvoryRef (ref :: RefScope -> Area Type -> Type) where - unwrapRef - :: IvoryVar a - => ref s ('Stored a) -> I.Expr - -instance IvoryRef (Pointer 'Valid c) where - unwrapRef = getPointer +unwrapRef + :: IvoryVar a + => Pointer 'Valid c s ('Stored a) + -> I.Expr +unwrapRef = getPointer -- | Dereferenceing. -deref :: forall eff ref s a. - (IvoryStore a, IvoryVar a, IvoryVar (ref s ('Stored a)), IvoryRef ref) - => ref s ('Stored a) -> Ivory eff a +deref :: forall eff c s a. + (IvoryStore a, IvoryVar a) + => Pointer 'Valid c s ('Stored a) -> Ivory eff a deref ref = do r <- freshVar "deref" emit (I.Deref (ivoryType (Proxy :: Proxy a)) r (unwrapRef ref)) @@ -76,9 +71,9 @@ deref ref = do -- Copying --------------------------------------------------------------------- -- | Memory copy. Emits an assertion that the two references are unequal. -refCopy :: forall eff sTo ref sFrom a. - ( IvoryRef ref, IvoryVar (Ref sTo a), IvoryVar (ref sFrom a), IvoryArea a) - => Ref sTo a -> ref sFrom a -> Ivory eff () +refCopy :: forall eff sTo c sFrom a. + (IvoryArea a, KnownConstancy c) + => Ref sTo a -> Pointer 'Valid c sFrom a -> Ivory eff () refCopy destRef srcRef = emit (I.RefCopy @@ -109,5 +104,5 @@ instance IvoryStore Sint32 instance IvoryStore Sint64 -- Only allow global nullable pointers to be stored in structures. -instance (KnownConstancy c, IvoryArea a) => - IvoryStore (Pointer 'Nullable c 'Global a) +instance (KnownConstancy c, IvoryArea a, n ~ 'Nullable, s ~ 'Global) => + IvoryStore (Pointer n c s a) diff --git a/ivory/src/Ivory/Language/Struct.hs b/ivory/src/Ivory/Language/Struct.hs index aafa6d67..140bf589 100644 --- a/ivory/src/Ivory/Language/Struct.hs +++ b/ivory/src/Ivory/Language/Struct.hs @@ -9,8 +9,8 @@ module Ivory.Language.Struct where import Ivory.Language.Area +import Ivory.Language.Pointer import Ivory.Language.Proxy -import Ivory.Language.Ref import Ivory.Language.Type(IvoryExpr(..), IvoryVar(..)) import qualified Ivory.Language.Syntax as I @@ -37,10 +37,11 @@ instance Eq (Label (sym :: Symbol) (field :: Area Type)) where l0 == l1 = getLabel l0 == getLabel l1 -- | Label indexing in a structure. -(~>) :: forall ref s sym field. - ( IvoryStruct sym, IvoryRef ref - , IvoryExpr (ref s ('Struct sym)), IvoryExpr (ref s field) ) - => ref s ('Struct sym) -> Label sym field -> ref s field +(~>) :: forall c s sym field. + (IvoryStruct sym, KnownConstancy c, IvoryArea field) + => Pointer 'Valid c s ('Struct sym) + -> Label sym field + -> Pointer 'Valid c s field s ~> l = wrapExpr (I.ExpLabel ty (unwrapExpr s) (getLabel l)) where ty = ivoryArea (Proxy :: Proxy ('Struct sym))