From 3d5f658ef58259a6137fc0de4c672e66c8023b11 Mon Sep 17 00:00:00 2001 From: Yuriy Syrovetskiy Date: Thu, 19 Oct 2017 15:17:00 +0300 Subject: [PATCH] Remove redundant IvoryRef class --- ivory-examples/examples/ClassHierarchy.hs | 11 ++++----- ivory-serialize/src/Ivory/Serialize/Atoms.hs | 12 +++++----- ivory-stdlib/src/Ivory/Stdlib/Memory.hs | 11 +++------ ivory-stdlib/src/Ivory/Stdlib/Operators.hs | 9 ++++---- ivory-stdlib/src/Ivory/Stdlib/String.hs | 22 +++++------------- ivory/src/Ivory/Language.hs | 16 ++++++++----- ivory/src/Ivory/Language/Array.hs | 14 ++++++------ ivory/src/Ivory/Language/CArray.hs | 13 +++++------ ivory/src/Ivory/Language/Cond.hs | 16 +++++-------- ivory/src/Ivory/Language/Ref.hs | 24 +++++++------------- ivory/src/Ivory/Language/Struct.hs | 11 +++++---- 11 files changed, 67 insertions(+), 92 deletions(-) diff --git a/ivory-examples/examples/ClassHierarchy.hs b/ivory-examples/examples/ClassHierarchy.hs index 52d809c8..6e3b537c 100644 --- a/ivory-examples/examples/ClassHierarchy.hs +++ b/ivory-examples/examples/ClassHierarchy.hs @@ -1,5 +1,6 @@ {-# OPTIONS_GHC -fno-warn-orphans #-} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE QuasiQuotes #-} @@ -37,12 +38,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 diff --git a/ivory-serialize/src/Ivory/Serialize/Atoms.hs b/ivory-serialize/src/Ivory/Serialize/Atoms.hs index a72943a5..ab7ec26e 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,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) 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 5665a39e..d8503395 100644 --- a/ivory-stdlib/src/Ivory/Stdlib/String.hs +++ b/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) - diff --git a/ivory/src/Ivory/Language.hs b/ivory/src/Ivory/Language.hs index 8559097f..82ee643d 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 #-} @@ -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 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/CArray.hs b/ivory/src/Ivory/Language/CArray.hs index 7d777263..51d9760a 100644 --- a/ivory/src/Ivory/Language/CArray.hs +++ b/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))) diff --git a/ivory/src/Ivory/Language/Cond.hs b/ivory/src/Ivory/Language/Cond.hs index d1aae82c..d6880b03 100644 --- a/ivory/src/Ivory/Language/Cond.hs +++ b/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,12 +44,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) @@ -57,8 +54,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 @@ -118,4 +115,3 @@ instance Ensures IBool where instance Ensures Cond where ensures = ensures' id ensures_ = ensures_' id - diff --git a/ivory/src/Ivory/Language/Ref.hs b/ivory/src/Ivory/Language/Ref.hs index 7f6b3e62..3469d573 100644 --- a/ivory/src/Ivory/Language/Ref.hs +++ b/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 diff --git a/ivory/src/Ivory/Language/Struct.hs b/ivory/src/Ivory/Language/Struct.hs index f334b5c3..59947fa0 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 @@ -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))