Allow to use (:->) on type level without a tick

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 ->

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,56 +70,56 @@ 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
 
 -- 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))))

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

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)

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))

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)

ivory-examples/examples/ClassHierarchy.hs

@@ -69,7 +69,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

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

ivory-examples/examples/ConstPtrRef.hs

@@ -8,7 +8,7 @@ import Ivory.Language
 import Prelude ()
 import Prelude.Compat
 
-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

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

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

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

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 <? r) $

ivory-examples/examples/FibLoop.hs

@@ -14,18 +14,18 @@ import Ivory.Compile.C.CmdlineFrontend
 import Ivory.Language
 
 -- Recursive implementation of fib
-fib_rec :: Def ('[Uint32] ':-> Uint64)
+fib_rec :: Def ('[Uint32] :-> Uint64)
 fib_rec  = proc "fib_rec" (\n -> body (ret =<< call fib_rec_aux 0 1 n))
 
-fib_rec_aux :: Def ('[Uint32,Uint32,Uint32] ':-> Uint64)
+fib_rec_aux :: Def ('[Uint32,Uint32,Uint32] :-> Uint64)
 fib_rec_aux  = proc "fib_rec_aux" $ \ a b n -> body $ do
   ifte_ (n ==? 0)
     (ret (safeCast a))
     (ret . safeCast =<< call fib_rec_aux b (a + b) (n - 1))
 
 -- 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)
@@ -52,7 +52,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 ])