Remove redundant IvoryRef class

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

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,12 +119,12 @@ 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 = proc ("ivory_serialize_unpack_" ++ ty ++ "_le") $ \ buf offs base -> ensures_ (checkStored base $ \ v -> (buf !! offs) ==? v) $ importFrom serializeHeader
@@ -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)

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 <? toLen)
   assert (end      >=? 0 .&& end     <=? frLen)
-  arrayMap $ go
+  arrayMap go
   where
   -- The index is w.r.t. the from array.
   go ix =

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

ivory-stdlib/src/Ivory/Stdlib/String.hs

@@ -19,7 +19,6 @@ import Data.Char (ord)
 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
@@ -82,21 +81,13 @@ 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
@@ -135,7 +126,7 @@ do_istr_eq :: Def ('[ ConstRef s1 ('CArray ('Stored Uint8))
                     , ConstRef s2 ('CArray ('Stored Uint8))
                     , Len
                     ] ':-> IBool)
-do_istr_eq = proc "ivory_string_eq" $ \s1 len1 s2 len2 -> body $ do
+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))
@@ -218,4 +209,3 @@ stdlibStringArtifacts =
   ]
   where
   supportfile f = artifactCabalFile P.getDataDir ("support/" ++ f)
-

ivory/src/Ivory/Language.hs

@@ -1,6 +1,5 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE TypeFamilies #-}
@@ -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
 
@@ -224,6 +227,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

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

ivory/src/Ivory/Language/CArray.hs

@@ -10,8 +10,8 @@
 module Ivory.Language.CArray where
 
 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
@@ -32,10 +32,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)))

ivory/src/Ivory/Language/Cond.hs

@@ -12,9 +12,9 @@ import Prelude.Compat
 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
 
@@ -44,21 +44,18 @@ 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)
   b <- runCond $ c $ prop $ wrapVar n
   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
@@ -118,4 +115,3 @@ instance Ensures IBool where
 instance Ensures Cond where
   ensures = ensures' id
   ensures_ = ensures_' id
-

ivory/src/Ivory/Language/Ref.hs

@@ -1,5 +1,4 @@
 {-# LANGUAGE DataKinds #-}
-{-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -8,7 +7,6 @@
 
 module Ivory.Language.Ref
   ( ConstRef
-  , IvoryRef
   , IvoryStore
   , Ref
   , constRef
@@ -49,19 +47,13 @@ type ConstRef = Pointer 'Valid 'Const
 
 -- Dereferencing ---------------------------------------------------------------
 
--- | TODO remove class, leave function only
-class IvoryRef (ref :: RefScope -> Area * -> *) 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))
@@ -70,9 +62,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

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
 
@@ -36,10 +36,11 @@ instance Eq (Label (sym :: Symbol) (field :: Area *)) 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))