Skip to content

Commit

Permalink
Cleaned of Coders, just before attempting to redo TxBody
Browse files Browse the repository at this point in the history
  • Loading branch information
TimSheard committed Oct 26, 2020
1 parent bd45250 commit 9a81f23
Show file tree
Hide file tree
Showing 4 changed files with 86 additions and 42 deletions.
93 changes: 59 additions & 34 deletions semantics/executable-spec/src/Data/Coders.hs
Expand Up @@ -52,14 +52,15 @@ module Data.Coders
encodeFoldableEncoder,
roundTrip,
roundTrip',
to,
from,
Dual(..), -- Duals
dualList,
dualSeq,
dualSet,
dualMaybe,
dualText,
dualStrictSeq,
Display(..),
Annotator(..),
foo,foo',defaultA,bar,bar', makeDecoder,baz,boxA,decodeA,
ok,
Expand Down Expand Up @@ -251,9 +252,9 @@ data Wrapped = Open | Closed
data Encode (w :: Wrapped) t where
Sum :: t -> Word -> Encode 'Open t
Rec :: t -> Encode 'Closed t
To :: (FromCBOR a,ToCBOR a) => a -> Encode 'Closed a
To :: ToCBOR a => a -> Encode 'Closed a
E :: (t -> Encoding) -> t -> Encode 'Closed t
ApplyE ::(Typeable a, Display a) => Encode w (a -> t) -> Encode 'Closed a -> Encode w t
ApplyE ::Typeable a => Encode w (a -> t) -> Encode 'Closed a -> Encode w t
ED :: Dual t -> t -> Encode 'Closed t
OmitC :: (Eq t,FromCBOR t) => t -> Encode 'Closed t
Omit:: (t -> Bool) -> Encode 'Closed t -> Encode 'Closed t
Expand All @@ -269,7 +270,7 @@ data Encode (w :: Wrapped) t where

infixl 4 !>

(!>) :: (Typeable a,Display a) => Encode w (a -> t) -> Encode 'Closed a -> Encode w t
(!>) :: Typeable a => Encode w (a -> t) -> Encode 'Closed a -> Encode w t
x !> y = ApplyE x y

runE :: Encode w t -> t
Expand Down Expand Up @@ -337,21 +338,22 @@ data Decode (w :: Wrapped) t where
RecD :: t -> Decode 'Closed t
From :: FromCBOR t => Decode 'Closed t
D :: (forall s. Decoder s t) -> Decode 'Closed t
ApplyD :: (Typeable a,Display a) => Decode w (a -> t) -> Decode 'Closed a -> Decode w t
ApplyD :: Typeable a => Decode w (a -> t) -> Decode 'Closed a -> Decode w t
Invalid :: Word -> Decode w t
Map :: (a -> b) -> Decode w a -> Decode w b
DD :: Dual t -> Decode 'Closed t
OmitD :: t -> Decode 'Closed t
UnTag :: Typeable t => t -> (Word -> Box t) -> [Word] -> Decode 'Closed t
-- The next two could be generalized to any (Applicative f) rather than Annotator
Ann :: Display t => Decode w t -> Decode w (Annotator t)
ApplyAnn :: (Typeable a,Display a) => Decode w (Annotator(a -> t)) -> Decode 'Closed (Annotator a) -> Decode w (Annotator t)
Ann :: Decode w t -> Decode w (Annotator t)
ApplyAnn :: Typeable a => Decode w (Annotator(a -> t)) -> Decode 'Closed (Annotator a) -> Decode w (Annotator t)

infixl 4 <!

(<!) :: (Typeable a,Display a) => Decode w (a -> t) -> Decode 'Closed a -> Decode w t
(<!) :: Typeable a => Decode w (a -> t) -> Decode 'Closed a -> Decode w t
x <! y = ApplyD x y

(<*!) :: (Typeable a,Display a) => Decode w (Annotator(a -> t)) -> Decode 'Closed (Annotator a) -> Decode w (Annotator t)
(<*!) :: Typeable a => Decode w (Annotator(a -> t)) -> Decode 'Closed (Annotator a) -> Decode w (Annotator t)
x <*! y = ApplyAnn x y

hsize :: Decode w t -> Int
Expand All @@ -360,6 +362,7 @@ hsize (SumD _) = 0
hsize (RecD _) = 0
hsize From = 1
hsize (D _) = 1
hsize (DD _) = 1
hsize (ApplyD f x) = hsize f + hsize x
hsize (Invalid _) = 0
hsize (Map _ x) = hsize x
Expand All @@ -378,14 +381,15 @@ decodeCount :: Decode w t -> Int -> Decoder s (Int, t)
decodeCount (Summands nm f) n = (n + 1,) <$> decodeRecordSum nm (\x -> decodE (f x))
decodeCount (SumD cn) n = pure (n + 1, cn)
decodeCount (RecD cn) n = decodeRecordNamed "RecD" (const n) (pure (n, cn))
decodeCount From n = do x <- fromCBOR; pure (n, x)
decodeCount (D dec) n = do x <- dec; pure (n, x)
decodeCount From n = (n,) <$> fromCBOR
decodeCount (D dec) n = (n,) <$> dec
decodeCount (ApplyD cn g) n = do
(i, f) <- decodeCount cn (n + hsize g)
y <- decodeClosed g
pure (i, f y)
decodeCount (Invalid k) _ = invalidKey k
decodeCount (Map f x) n = do (m, y) <- decodeCount x n; pure (m, f y)
decodeCount (DD (Dual _enc dec)) n = (n,) <$> dec
decodeCount (OmitD x) n = pure(n,x)
decodeCount (u@(UnTag _ _ _)) n = (n+1,) <$> decodeClosed u
decodeCount (Ann x) n = do (m,y) <- decodeCount x n; pure(m,pure y)
Expand All @@ -399,13 +403,14 @@ decodeClosed (Summands nm f) = decodeRecordSum nm (\x -> decodE (f x))
-- decodeClosed (SumD _) = undefined -- This case, by design, is unreachable by type considerations
decodeClosed (RecD cn) = pure cn
decodeClosed From = do x <- fromCBOR; pure x
decodeClosed (D dec) = do x <- dec; pure x
decodeClosed (D dec) = dec
decodeClosed (ApplyD cn g) = do
f <- decodeClosed cn
y <- decodeClosed g
pure (f y)
decodeClosed (Invalid k) = invalidKey k
decodeClosed (Map f x) = f <$> decodeClosed x
decodeClosed (DD (Dual _enc dec)) = dec
decodeClosed (OmitD n) = pure n
decodeClosed (UnTag initial pick required) = do
lenOrIndef <- decodeListLenOrIndef
Expand Down Expand Up @@ -463,7 +468,6 @@ unTagSeries t pick seen n = do (transform,seen2) <- untag pick seen; unTagSeries
-- or you want something not traditional, make you own Dual and use E or D

data Dual t = Dual (t -> Encoding) (forall s . Decoder s t)
| AnnDual (t -> Encoding) (forall s. Decoder s (Annotator s))

dualList :: (ToCBOR a, FromCBOR a) => Dual [a]
dualList = Dual encodeFoldable (decodeList fromCBOR)
Expand All @@ -483,6 +487,9 @@ dualStrictSeq = Dual encodeFoldable (decodeStrictSeq fromCBOR)
dualText :: Dual Text
dualText = Dual toCBOR fromCBOR

dualCBOR :: (ToCBOR a, FromCBOR a) => Dual a
dualCBOR = Dual toCBOR fromCBOR

-- ===========================================
-- For more worked out EXAMPLES see the testfile:
-- cardano-ledger-specs/shelley-ma/impl/test/Test/Cardano/Ledger/ShelleyMA/Timelocks.hs
Expand Down Expand Up @@ -568,7 +575,7 @@ instance FromCBOR A where
-- ^tag ^tag ^tag
-- So the user supplies a function, that encodes every field, each field must use a unique
-- tag, and fields with default values have Omit wrapped around the Tag encoding.
-- The user must ensure that there is NOT an Omit on a required field.
-- The user must ensure that there is NOT an Omit on a required field. 'baz' is an example.

baz:: A -> Encode 'Closed A
baz (A n xs t) = Rec A !> Omit (==0) (Tag 0 (To n)) !> Omit null (Tag 1 (To xs)) !> Tag 2 (To t)
Expand Down Expand Up @@ -601,16 +608,33 @@ decodeA = UnTag (A 0 [] (pack "a")) boxA [2] -- Only the field with Tag 2 is re

-- ===============================================================================
-- We can generate things like foo and bar in the first approach using 1 liners
-- First we write a one line Encode that uses Omit with predicates, rather than OmitC.
-- wrapped around every field with default values. This tells us 3 things
-- 1) Which fields can be omitted
-- 2) How to test if a value should be omitted
-- 3) The value to supply if they are omitted
-- This is a much more compact way of writing foo, where we don't have to enumerate all
-- 2^k different patterns of what should be defaulted, the prediates do this dynamically.
-- First we write a one line Encode (see foo' below) that uses 'Omit' with
-- predicates, rather than 'OmitC', and 'to', rather than 'To'. This ensures that
-- the one liner can be dualized (see 'choices'). Wrap 'Omit' around every field
-- with default values. This tells us 3 things
-- 1) Which fields can be omitted
-- 2) How to test if a value should be omitted
-- 3) The value to supply if they are omitted
-- This is a much more compact way of writing foo, where we don't have to
-- enumerate all 2^k different patterns of what should be defaulted, the predicates
-- in 'Omit' do this dynamically.
--
-- We need to use these dual versions of To and From, Since 'choices' cannot
-- work on 'To' and 'From' because they each only supply one of 'ToCBOR' or
-- 'FromCBOR'. Both ('to' vs 'To') and ('from' vs 'From') have their uses. It
-- depends upon the context. If you only have one of ToCBOR or FromCBOR use To
-- or From, If the current context has both, then use to or from. In foo'
-- we need 'to' because we can compute its dual. We can't daulize To and From
-- because they require different CBOR instances.

to :: (ToCBOR t, FromCBOR t) => t -> Encode 'Closed t
to xs = ED dualCBOR xs

from :: (ToCBOR t, FromCBOR t) => Decode 'Closed t
from = DD dualCBOR

foo' :: Word -> A -> (Encode 'Open A)
foo' tag (A n xs t) = (Sum A tag !> Omit (==0) (To n) !> Omit null (To xs) !> To t)
foo' tag (A n xs t) = (Sum A tag !> Omit (==0) (to n) !> Omit null (to xs) !> to t)

-- Second we construct a default value. Use the correct defaults in every field
-- specified in foo' above. Non-default fields can have anything with the right type.
Expand Down Expand Up @@ -640,18 +664,16 @@ makeDecoder sp = \ n -> if (n<0 || n>=m) then Invalid n else table ! n where
choices (ApplyE f x) = [ApplyD g y | g <- choices f, y <- choices x]
choices (Omit _ e) = (OmitD (runE e)) : choices e
choices (OmitC n) = [OmitD n,From]
choices (To _) = [From]
choices (Sum cn _) = [SumD cn]
choices (Rec cn) = [RecD cn]
choices (E _ _) = [D $ defaultError "E has no dual"]
choices (ED _ _) = [D $ defaultError "E has no dual"]
choices (ED dual _) = [DD dual]
choices (E _ _) = [D $ defaultError "E has no dual"]
choices (To _) = [D $ defaultError "To has no dual"]
choices (Tag _ _) = [D $ defaultError "Tag has no dual"]

addTag :: [Decode w t] -> Array Word (Decode w t)
addTag xs = array (0,n) (label 0 xs)
where n = fromIntegral (length xs) - 1
label i (y:ys) = (i,y) : label (i+1) ys
label _ [] = []
addTag xs = array (0,fromIntegral (length xs) - 1) (zip [0::Word ..] xs)

table = addTag choicelist
choicelist = (choices sp)
m = fromIntegral (length choicelist)
Expand Down Expand Up @@ -700,6 +722,7 @@ ok = all isRight [ test0, test1, test2, test3
where isRight (Right _) = True
isRight (Left _) = False

{-
-- ===================================================================
-- Display instances. We can't make Show instances directly because we
-- can't make Show instances for functions (a -> b) or Annotator. so
Expand All @@ -711,16 +734,16 @@ class Display t where
instance {-# OVERLAPPABLE #-} Show t => Display t where
display x = show x
instance Display (a -> b) where
instance {-# INCOHERENT #-} Display (a -> b) where
display _f = "?"
instance Display (Annotator t) where
instance {-# INCOHERENT #-} Display (Annotator t) where
display (Annotator _f) = "Annotator"
instance Display (Dual t) where
display _ = "(Dual ? ?)"
instance Display t => Display (Encode w t) where
instance {-# INCOHERENT #-} Display t => Display (Encode w t) where
display (Sum c n) = "Sum "++display c++" "++display n
display (Rec t) = "Rec "++display t
display (To t) = "To "++display t
Expand All @@ -731,7 +754,7 @@ instance Display t => Display (Encode w t) where
display (Omit p x) = "Omit "++display p++" ("++display x++")"
display (Tag n x) = "Tag "++display n++"("++display x++")"
instance Display t => Display (Decode w t) where
instance {-# INCOHERENT #-} Display t => Display (Decode w t) where
display (Summands str _) = "(Summands "++str++")"
display (SumD t) = "SumD "++display t
display (RecD t) = "RecD "++display t
Expand All @@ -752,4 +775,6 @@ instance Display t => Show (Encode w t) where
show x = display x
instance Display t => Show (Decode w t) where
show x = display x
show x = display x
-}
23 changes: 18 additions & 5 deletions shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Timelocks.hs
Expand Up @@ -44,7 +44,7 @@ import Cardano.Ledger.Era
import qualified Cardano.Ledger.Shelley as Shelley
import Cardano.Slotting.Slot (SlotNo (..))
import qualified Data.ByteString as BS
import Data.Coders (Decode (..), Encode (..), Wrapped (..), decode, encode, (!>), (<!))
import Data.Coders (Decode (..), Encode (..), Wrapped (..), decode, encode, (!>), (<!),(<*!))
import Data.MemoBytes
( Mem,
MemoBytes (..),
Expand All @@ -56,15 +56,14 @@ import qualified Data.Set as Set
import GHC.Generics (Generic)
import GHC.Records
import NoThunks.Class (NoThunks (..))
import Shelley.Spec.Ledger.BaseTypes (StrictMaybe (SJust, SNothing), invalidKey)
import Shelley.Spec.Ledger.BaseTypes (StrictMaybe (SJust, SNothing))
import Shelley.Spec.Ledger.Keys (KeyHash (..), KeyRole (Witness))
import Shelley.Spec.Ledger.Scripts
( MultiSig,
ScriptHash (..),
)
import Shelley.Spec.Ledger.Serialization
( decodeRecordSum,
decodeStrictSeq,
( decodeStrictSeq,
encodeFoldable,
)
import Shelley.Spec.Ledger.Tx
Expand Down Expand Up @@ -112,6 +111,17 @@ data Timelock' era
| TimelockOr' !(StrictSeq (Timelock era))
deriving (Show, Eq, Ord, Generic, NoThunks)

decTimelock' :: Era era => Word -> Decode 'Open (Annotator (Timelock' era))
decTimelock' 0 = Ann(SumD Interval' <! From)
decTimelock' 1 = Ann(SumD Multi') <*! From
decTimelock' 2 = Ann(SumD TimelockAnd') <*! D (sequence <$> decodeStrictSeq fromCBOR)
decTimelock' 3 = Ann(SumD TimelockOr') <*! D (sequence <$> decodeStrictSeq fromCBOR)
decTimelock' k = Invalid k

instance Era era => FromCBOR (Annotator (Timelock' era))
where fromCBOR = decode (Summands "Annotator(Timelock' era)" decTimelock')

{- The decTimelok' function replaces things like this:
instance
Era era =>
FromCBOR (Annotator (Timelock' era))
Expand All @@ -133,6 +143,7 @@ instance
timelks <- sequence <$> decodeStrictSeq fromCBOR
pure (2, TimelockOr' <$> timelks)
k -> invalidKey k
-}

-- ==============================================================================
-- Now all the problematic Timelock instances are derived. No thinking required
Expand Down Expand Up @@ -164,7 +175,7 @@ pattern Multi :: Era era => MultiSig era -> Timelock era
pattern Multi m <-
Timelock (Memo (Multi' m) _)
where
Multi m = Timelock $ memoBytes $ Sum Multi' 1 !> To m
Multi m = Timelock $ memoBytes $ (Sum Multi' 1) !> To m

pattern TimelockAnd :: Era era => StrictSeq (Timelock era) -> Timelock era
pattern TimelockAnd ms <-
Expand Down Expand Up @@ -248,6 +259,8 @@ hashTimelockScript =
. Hash.hashWith (\x -> nativeTimelockTag <> serialize' x)

{-
-- At some point we will need a class, analogous to MultiSignatureScript
-- which relates scripts and their validators.
instance
( Era era,
HasField "vldt" (Core.TxBody era) ValidityInterval,
Expand Down
10 changes: 8 additions & 2 deletions shelley-ma/impl/test/Test/Cardano/Ledger/ShelleyMA/Timelocks.hs
Expand Up @@ -15,6 +15,7 @@ import Cardano.Binary
ToCBOR (toCBOR),
encodeListLen,
encodeWord,
Encoding,
)
import Cardano.Ledger.ShelleyMA.Timelocks
import Cardano.Slotting.Slot (SlotNo (..))
Expand All @@ -30,8 +31,7 @@ import Data.Coders
decodeList,
decodeStrictSeq,
encode,
encodeList,
encodeStrictSeq,
encodeFoldable,
runE,
(!>),
(<!),
Expand Down Expand Up @@ -87,6 +87,12 @@ sG = Sum G 2 !> To [3, 4, 5] -- Tag for G is 2
sGa = Sum G 2 !> E encodeList [2, 5] -- Tag for G is 2
sH = Sum H 3 !> E encodeStrictSeq (fromList [False, True]) -- Tag for H is 3

encodeList :: ToCBOR t => [t] -> Encoding
encodeList = encodeFoldable

encodeStrictSeq :: ToCBOR t => StrictSeq t -> Encoding
encodeStrictSeq = encodeFoldable

-- ===============================================================

-- ===================================
Expand Down
Expand Up @@ -110,7 +110,7 @@ pattern RequireAllOf ms <-
MultiSig (Memo (RequireAllOf' ms) _)
where
RequireAllOf ms =
MultiSig $ memoBytesAnn (Sum RequireAllOf' 1 !> E encodeFoldable ms)
MultiSig $ memoBytes (Sum RequireAllOf' 1 !> E encodeFoldable ms)

pattern RequireAnyOf :: Era era => [MultiSig era] -> MultiSig era
pattern RequireAnyOf ms <-
Expand Down

0 comments on commit 9a81f23

Please sign in to comment.