Skip to content

Commit

Permalink
Intermediate state messed up Scripts
Browse files Browse the repository at this point in the history
  • Loading branch information
@TimSheard
TimSheard committed Oct 26, 2020
1 parent 22ff64b commit bd45250
Show file tree
Hide file tree
Showing 3 changed files with 102 additions and 101 deletions.
181 changes: 94 additions & 87 deletions semantics/executable-spec/src/Data/Coders.hs
View file
Expand Up @@ -19,6 +19,7 @@
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeOperators #-}


{-# OPTIONS_GHC -fno-warn-orphans #-}

-- | MemoBytes is an abstration for a datetype that encodes its own seriialization.
Expand All @@ -41,10 +42,6 @@ module Data.Coders
decodeSeq,
decodeStrictSeq,
decodeSet,
encodeList,
encodeSeq,
encodeStrictSeq,
encodeSet,
decodeRecordNamed,
decodeRecordSum,
invalidKey,
Expand All @@ -56,12 +53,14 @@ module Data.Coders
roundTrip,
roundTrip',
Dual(..), -- Duals
listDual,
seqDual,
setDual,
maybeDual,
textDual,
strictSeqDual,
dualList,
dualSeq,
dualSet,
dualMaybe,
dualText,
dualStrictSeq,
Display(..),
Annotator(..),
foo,foo',defaultA,bar,bar', makeDecoder,baz,boxA,decodeA,
ok,
)
Expand Down Expand Up @@ -195,15 +194,14 @@ wrapCBORArray len contents =
-- The Encode and Decode mechanism can also be used to encode Algebraic datatypes
-- in a uniform way. (Decode t) is dual to (Encode t). A decoder can be extracted
-- from it. And it will consistently decode it's dual. We now give some examples.
-- In the examples Let Int and C have ToCBOR instances, and
-- encodeB :: B -> Encoding, and decodeB :: Decoder s B
-- In the examples Let Int and C have ToCBOR instances, and dualB :: Dual B
{-
-- An example with 1 constructor (a record) uses Rec and RecD
data A = ACon Int B C
encodeA :: A -> Encode 'Closed A
encodeA (ACon i b c) = Rec ACon !> To i !> E encodeB b !> To c
encodeA (ACon i b c) = Rec ACon !> To i !> E dualB b !> To c
decodeA :: Decode 'Closed A
decodeA = RecD ACon <! From <! D decodeB <! From
Expand All @@ -217,13 +215,13 @@ data M = M1 Int | M2 B Bool | M3 A
encodeM :: M -> Encode 'Open M
encodeM (M1 i) = Sum M1 0 !> To i
encodeM (M2 b tf) = Sum M2 1 !> E encodeB b !> To tf
encodeM (M2 b tf) = Sum M2 1 !> E dualB b !> To tf
encodeM (M3 a) = Sum M3 2 !> To a
decodeM :: Decode 'Closed M
decodeM = Summands "M" decodeMx
where decodeMx 0 = SumD M1 <! From
decodeMx 1 = SumD M2 <! D decodeB <! From
decodeMx 1 = SumD M2 <! D dualB <! From
decodeMx 3 = SumD M3 <! From
decodeMx k = Invalid k
Expand All @@ -248,17 +246,15 @@ data Wrapped = Open | Closed
deriving Typeable

-- ===========================================================
{-
class Display t where
display :: t -> String
-}


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
E :: (t -> Encoding) -> t -> Encode 'Closed t
ApplyE ::(Typeable a, Show a) => Encode w (a -> t) -> Encode 'Closed a -> Encode w t
ApplyE ::(Typeable a, Display 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
Tag :: Word -> Encode 'Closed t -> Encode 'Closed t
Expand All @@ -273,7 +269,7 @@ data Encode (w :: Wrapped) t where

infixl 4 !>

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

runE :: Encode w t -> t
Expand All @@ -282,6 +278,7 @@ runE (Rec cn) = cn
runE (ApplyE f x) = runE f (runE x)
runE (To x) = x
runE (E _ x) = x
runE (ED _ x) = x
runE (OmitC x) = x
runE (Omit _ x) = runE x
runE (Tag _ x) = runE x
Expand All @@ -292,6 +289,7 @@ gsize (Rec _) = 0
gsize (To _) = 1
gsize (E _ _) = 1
gsize (ApplyE f x) = gsize f + gsize x
gsize (ED _ _) = 1
gsize (OmitC _) = 0
gsize (Omit p x) = if p (runE x) then 0 else gsize x
gsize (Tag _ x) = gsize x
Expand All @@ -311,6 +309,7 @@ encode sym = encodeCountPrefix 0 sym
-- by design. Its left spine must end in a (Rec c). We count (gsize x)
-- the 'fields' in x, and add them to the number things we
-- must add to the prefix of the enclosing type.
encodeCountPrefix _ (ED (Dual enc _) x) = enc x
encodeCountPrefix _ (OmitC _) = mempty
encodeCountPrefix n (Omit p x) =
if p (runE x) then mempty else encodeCountPrefix n x
Expand All @@ -322,33 +321,37 @@ encode sym = encodeCountPrefix 0 sym
encodeClosed (To x) = toCBOR x
encodeClosed (E enc x) = enc x
encodeClosed (ApplyE f x) = encodeClosed f <> encodeClosed x
encodeClosed (ED (Dual enc _) x) = enc x
encodeClosed (OmitC _) = mempty
encodeClosed (Omit p x) =
if p (runE x) then mempty else encodeClosed x
encodeClosed (Tag tag x) = encodeWord tag <> encodeClosed x

-- =====================
-- ===================================================================
-- Decode
-- ===================================================================

data Decode (w :: Wrapped) t where
Summands :: String -> (Word -> Decode 'Open t) -> Decode 'Closed t
SumD :: t -> Decode 'Open t
RecD :: t -> Decode 'Closed t
From :: FromCBOR t => Decode 'Closed t
D :: (forall s. Decoder s t) -> Decode 'Closed t
ApplyD :: (Typeable a,Show a) => Decode w (a -> t) -> Decode 'Closed a -> Decode w t
ApplyD :: (Typeable a,Display 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
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 :: Show t => Decode w t -> Decode w (Annotator t)
ApplyAnn :: (Typeable a,Show a) => Decode w (Annotator(a -> t)) -> Decode 'Closed (Annotator a) -> Decode w (Annotator t)
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)

infixl 4 <!

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

(<*!) :: (Typeable a,Show a) => Decode w (Annotator(a -> t)) -> Decode 'Closed (Annotator a) -> Decode w (Annotator t)
(<*!) :: (Typeable a,Display 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 Down Expand Up @@ -454,49 +457,31 @@ unTagSeries t _ seen n | n <= 0 = pure (t, seen)
unTagSeries t pick seen n = do (transform,seen2) <- untag pick seen; unTagSeries (transform t) pick seen2 (n-1)

-- ===========================================================================================
-- These functions are the dual analogs to
-- Shelley.Spec.Ledger.Serialization(decodeList, decodeSeq, decodeStrictSeq, decodeSet)
-- It is not well documented how to use encodeFoldable.
-- They are provided here as compatible pairs for use with the (E x) and (D x) constructors
-- of the Encode and Decode types. (E encodeList xs) and (D (decodeList fromCBOR)) should be duals.

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

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

encodeSeq :: ToCBOR a => Seq a -> Encoding
encodeSeq = encodeFoldable

encodeSet :: ToCBOR a => Set a -> Encoding
encodeSet = encodeFoldable

-- ===========================================================================================
-- A Dual pairs and Encoding and Decoder with a rountrip property.
-- A Dual pairs an Encoding and a Decoder with a roundtrip property.
-- They are used with the (E and D) constructors of Encode and Decode
-- If you are trying to code something not in the CBOR classes
-- 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))

listDual :: (ToCBOR a, FromCBOR a) => Dual [a]
listDual = Dual encodeFoldable (decodeList fromCBOR)
dualList :: (ToCBOR a, FromCBOR a) => Dual [a]
dualList = Dual encodeFoldable (decodeList fromCBOR)

seqDual :: (ToCBOR a, FromCBOR a) => Dual (Seq a)
seqDual = Dual encodeFoldable (decodeSeq fromCBOR)
dualSeq :: (ToCBOR a, FromCBOR a) => Dual (Seq a)
dualSeq = Dual encodeFoldable (decodeSeq fromCBOR)

setDual :: (Ord a,ToCBOR a, FromCBOR a) => Dual (Set a)
setDual = Dual encodeFoldable (decodeSet fromCBOR)
dualSet :: (Ord a,ToCBOR a, FromCBOR a) => Dual (Set a)
dualSet = Dual encodeFoldable (decodeSet fromCBOR)

maybeDual :: (ToCBOR a, FromCBOR a) => Dual (Maybe a)
maybeDual = Dual toCBOR fromCBOR
dualMaybe :: (ToCBOR a, FromCBOR a) => Dual (Maybe a)
dualMaybe = Dual toCBOR fromCBOR

strictSeqDual :: (ToCBOR a, FromCBOR a) => Dual (StrictSeq a)
strictSeqDual = Dual encodeFoldable (decodeStrictSeq fromCBOR)
dualStrictSeq :: (ToCBOR a, FromCBOR a) => Dual (StrictSeq a)
dualStrictSeq = Dual encodeFoldable (decodeStrictSeq fromCBOR)

textDual :: Dual Text
textDual = Dual toCBOR fromCBOR
dualText :: Dual Text
dualText = Dual toCBOR fromCBOR

-- ===========================================
-- For more worked out EXAMPLES see the testfile:
Expand Down Expand Up @@ -659,6 +644,7 @@ makeDecoder sp = \ n -> if (n<0 || n>=m) then Invalid n else table ! n where
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 (Tag _ _) = [D $ defaultError "Tag has no dual"]

addTag :: [Decode w t] -> Array Word (Decode w t)
Expand Down Expand Up @@ -715,34 +701,55 @@ ok = all isRight [ test0, test1, test2, test3
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
-- we introduce our own class Display.

class Display t where
display :: t -> String

instance {-# OVERLAPPABLE #-} Show t => Display t where
display x = show x

instance Display (a -> b) where
display _f = "?"

instance Display (Annotator t) where
display (Annotator _f) = "Annotator"

instance Display (Dual t) where
display _ = "(Dual ? ?)"

instance 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
display (E d x) = "E "++display d++" "++display x
display (ED d x) = "E "++display d++" "++display x
display (ApplyE x y) = display x++" !> "++display y
display (OmitC t) = "OmitC "++display t
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
display (Summands str _) = "(Summands "++str++")"
display (SumD t) = "SumD "++display t
display (RecD t) = "RecD "++display t
display From = "From"
display (D _d) = "D ?"
display (ApplyD x y) = display x++" <! "++display y
display (Invalid n) = "(Invalid "++display n++")"
display (Map _f _x) = "Map ? ?"
display (OmitD x) = "OmitD "++display x
display (UnTag ini d required) = "(UnTag "++display ini++" "++display d++" "++display required++")"
display (Ann x) = "Ann ("++display x ++")"
display (ApplyAnn x y) = display x++" <*! "++display y

-- ===================================================
-- Show instances

instance Display t => Show (Encode w t) where
show x = display x

instance Show (a -> b) where show _ = "<fun>"

instance Show (Annotator t) where
show (Annotator _f) = "Annotator"

instance Show t => Show (Encode w t) where
show (Sum _ n) = "Sum "++show n
show (Rec t) = "Rec "++show t
show (To t) = "To "++show t
show (E _ x) = "E "++show x
show (ApplyE x y) = show x++" !> "++show y
show (OmitC t) = "OmitC "++show t
show (Omit _p x) = "Omit ? ("++show x++")"
show (Tag n x) = "Tag "++show n++"("++show x++")"

instance Show t => Show (Decode w t) where
show (Summands str _) = "(Summands "++str++")"
show (SumD t) = "SumD "++show t
show (RecD t) = "RecD "++show t
show From = "From"
show (D _) = "D"
show (ApplyD x y) = show x++" <! "++show y
show (Invalid n) = "(Invalid "++show n++")"
show (Map _f _x) = "Map"
show (OmitD x) = "OmitD "++show x
show (UnTag ini _ required) = "(UnTag "++show ini++" "++show required++")"
show (Ann x) = "Ann ("++show x ++")"
show (ApplyAnn x y) = show x++" <*! "++show y
instance Display t => Show (Decode w t) where
show x = display x
20 changes: 7 additions & 13 deletions semantics/executable-spec/src/Data/MemoBytes.hs
View file
Expand Up @@ -24,6 +24,7 @@
module Data.MemoBytes
( MemoBytes (..),
memoBytes,
memoBytesAnn,
Mem,
shorten,
showMemo,
Expand All @@ -37,6 +38,7 @@ import Cardano.Binary
ToCBOR (toCBOR),
encodePreEncoded,
withSlice,
FullByteString (Full),
)
import Data.ByteString.Short (ShortByteString, fromShort, toShort)
import qualified Data.ByteString.Lazy as Lazy
Expand All @@ -54,19 +56,6 @@ import Codec.CBOR.Read(DeserialiseFailure,deserialiseFromBytes)
data MemoBytes t = Memo {memotype :: !t, memobytes :: ShortByteString}
deriving (NoThunks) via AllowThunksIn '["memobytes"] (MemoBytes t)

{-
deriving via AllowThunksIn '["memobytes"] (MemoBytes t)
instance (Typeable t, NoThunks t) => NoThunks(MemoBytes t)
data MemoBytes t = Memo { memotype :: {-# UNPACK #-} !t, memobytes:: ShortByteString }
deriving (NoThunks) via AllowThunksIn '["memobytes"] (MemoBytes t)
instance NoThunks t => NoThunks(MemoBytes t) where
wNoThunks ctxt (Memo x _) = noThunks ("Memo":ctxt) x
-- We deliberately allow thunks in the bytes
-}

deriving instance Generic (MemoBytes t)

instance (Typeable t) => ToCBOR (MemoBytes t) where
Expand Down Expand Up @@ -105,6 +94,11 @@ printMemo x = putStrLn (showMemo x)
memoBytes :: Encode w t -> MemoBytes t
memoBytes t = Memo (runE t) (shorten (toLazyByteString (encode t)))

memoBytesAnn :: Encode w (Annotator t) -> MemoBytes t
memoBytesAnn t = Memo term (shorten bytes)
where bytes = toLazyByteString (encode t)
Annotator f = runE t
term = f (Full bytes)

roundTripMemo:: (FromCBOR t) => MemoBytes t -> Either Codec.CBOR.Read.DeserialiseFailure (Lazy.ByteString, MemoBytes t)
roundTripMemo (Memo _t bytes) =
Expand Down
2 changes: 1 addition & 1 deletion shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/Scripts.hs
View file
Expand Up @@ -110,7 +110,7 @@ pattern RequireAllOf ms <-
MultiSig (Memo (RequireAllOf' ms) _)
where
RequireAllOf ms =
MultiSig $ memoBytes (Sum RequireAllOf' 1 !> E encodeFoldable ms)
MultiSig $ memoBytesAnn (Sum RequireAllOf' 1 !> E encodeFoldable ms)

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

0 comments on commit bd45250

Please sign in to comment.