Added 4 modules which deal with Data independent of the ledger to the…

… directory

semantics/executable-spec/src/Data/  These can be imported using the module names
Data.CannonicalMaps.hs
Data.Coders
Data.MemoBytes
Control.SetAlgebra

semantics/executable-spec/small-steps.cabal

@@ -32,19 +32,24 @@ library
                      , Control.State.Transition.Simple
                      , Data.AbstractSize
                      , Data.Relation
-                     , Control.Iterate.Collect
+                     , Data.CannonicalMaps
+                     , Data.MemoBytes
+                     , Data.Coders
                      , Control.Iterate.SetAlgebra
-                     , Control.Iterate.SetAlgebraInternal
+                     , Control.Iterate.Collect
+                     , Control.SetAlgebra
   -- other-modules:
   -- other-extensions:
   build-depends:       base >=4.11 && <5
                      , bytestring
+                     , cardano-prelude
                      , containers
                      , cryptonite
                      , deepseq
                      , free
                      , mtl
                      , nothunks
+                     , text
                      , transformers >= 0.5
                      , ansi-wl-pprint
                      -- IOHK deps

semantics/executable-spec/src/Control/SetAlgebra.hs

@@ -0,0 +1,42 @@
+{-# LANGUAGE GADTs #-}
+
+module Control.SetAlgebra
+  (-- In addition to Data.Map.Map and Data.Set.Set, the following new types can be used in the set algegra
+   List,        -- A list type whose constructor is hidden (sorted [(key,value)] pairs, with no duplicate keys).
+                -- Use 'fromList' to constuct concrete values
+   BiMap,Bimap, -- Maps for Bijections. Use 'biMapFromList' and 'biMapEmpty' toconstruct concrete values.
+   Single(..),  -- Sets with a single pair. Visible constructors 'Singleton', 'SetSingleton', and 'Fail'.
+
+   -- Classes supporting abstract constructors of Set Algebra Expressions. These show up in the types of overloaded functions.
+   Basic(..),Iter(..),Embed(..),HasExp(..),BaseRep(..),
+
+   -- Overloaded functions acting as abstract constructors of Set Algebra Expressions. These correspond
+   -- with the operators in the specification, except here sets are thought of as a map with a Unit value. (Map k ())
+   dom, rng, dexclude, drestrict, rexclude, rrestrict, unionleft, unionright, unionplus,
+   singleton, setSingleton, intersect, subset, keyeq,
+   (◁), (⋪), (▷), (⋫), (∈), (∉), (∪), (⨃), (∪+), (∩), (⊆), (≍), (<|), (|>),
+   -- The only exported concrete Constructor of Set Algebra Expressons. Needed to make 'HasExp' and 'Embed'
+   -- instances of new kinds of sets (Basically,  Data.Map's wrapped in a newtype).
+   -- See: Shelley.Spec.Ledger.TxBody and Shelley/Spec/Ledger/UTxO.hs and helley/Spec/Ledger/Delegation/Certificates.hs
+   -- for example uses of this.
+   Exp(Base),
+
+   -- Evaluate an abstract Set Algebra Expression to the Set (Map) it represents.
+   eval,
+
+   -- Functions to build concrete Set-like things useable as Set Algebra Expressions
+   materialize, biMapFromList, biMapEmpty, fromList, keysEqual, forwards, backwards
+
+  )
+where
+
+
+import Data.Map(Map)
+import Data.Set(Set)
+import Control.Iterate.SetAlgebra
+
+forwards :: BiMap v k v -> Map k v
+forwards (MkBiMap l _r) = l
+
+backwards :: BiMap v k v -> Map v (Set k)
+backwards (MkBiMap _l r) = r

semantics/executable-spec/src/Data/CannonicalMaps.hs

@@ -0,0 +1,122 @@
+{-# LANGUAGE BangPatterns  #-}
+
+module Data.CannonicalMaps
+  ( CannonicalZero(..),
+    cannonicalInsert,
+    cannonicalMapUnion,
+    cannonicalMap,
+    pointWise,
+    Map.Map,
+  )
+  where
+
+import Data.Map.Internal
+  ( Map (..),
+    balanceL,
+    balanceR,
+    link,
+    link2,
+    singleton,
+    splitLookup,
+  )
+import qualified Data.Map.Strict as Map
+
+-- =====================================================================================
+-- Operations on Map from keys to values that are specialised to `CanonicalZero` values.
+-- A (Map k v) is (CannonicalZero v), if it never stores a zero at type v.
+-- In order to do this we need to know what 'zeroC' is, and 'joinC' has to know how to
+-- joining together two maps where one of its arguments might be 'zeroC'
+-- This class is strictly used in the implementation, and is not observable by the user.
+-- ======================================================================================
+
+class Eq t => CannonicalZero t where
+  zeroC :: t
+  joinC :: t -> t -> t
+
+instance CannonicalZero Integer where
+  zeroC = 0
+  joinC = (+)
+
+instance (Eq k, Eq v, Ord k, CannonicalZero v) => CannonicalZero (Map k v) where
+  zeroC = Map.empty
+  joinC = cannonicalMapUnion joinC
+
+-- Note that the class CannonicalZero and the function cannonicalMapUnion are mutually recursive.
+
+cannonicalMapUnion ::
+  (Ord k, CannonicalZero a) =>
+  (a -> a -> a) -> -- (\ left right -> ??) which side do you prefer?
+  Map k a ->
+  Map k a ->
+  Map k a
+cannonicalMapUnion _f t1 Tip = t1
+cannonicalMapUnion f t1 (Bin _ k x Tip Tip) = cannonicalInsert f k x t1
+cannonicalMapUnion f (Bin _ k x Tip Tip) t2 = cannonicalInsert f k x t2
+cannonicalMapUnion _f Tip t2 = t2
+cannonicalMapUnion f (Bin _ k1 x1 l1 r1) t2 = case splitLookup k1 t2 of
+  (l2, mb, r2) -> case mb of
+    Nothing ->
+      if x1 == zeroC
+        then link2 l1l2 r1r2
+        else link k1 x1 l1l2 r1r2
+    Just x2 ->
+      if new == zeroC
+        then link2 l1l2 r1r2
+        else link k1 new l1l2 r1r2
+      where
+        new = (f x1 x2)
+    where
+      !l1l2 = cannonicalMapUnion f l1 l2
+      !r1r2 = cannonicalMapUnion f r1 r2
+{-# INLINEABLE cannonicalMapUnion #-}
+
+cannonicalInsert ::
+  (Ord k, CannonicalZero a) =>
+  (a -> a -> a) ->
+  k ->
+  a ->
+  Map k a ->
+  Map k a
+cannonicalInsert = go
+  where
+    go ::
+      (Ord k, CannonicalZero a) =>
+      (a -> a -> a) ->
+      k ->
+      a ->
+      Map k a ->
+      Map k a
+    go _ !kx x Tip = if x == zeroC then Tip else singleton kx x
+    go f !kx x (Bin sy ky y l r) =
+      case compare kx ky of
+        LT -> balanceL ky y (go f kx x l) r
+        GT -> balanceR ky y l (go f kx x r)
+        EQ -> if new == zeroC then link2 l r else Bin sy kx new l r
+          where
+            new = f y x -- Apply to value in the tree, then the new value
+{-# INLINEABLE cannonicalInsert #-}
+
+cannonicalMap :: (Ord k, CannonicalZero a) => (a -> a) -> Map k a -> Map k a
+cannonicalMap f m = Map.foldrWithKey accum Map.empty m
+  where
+    accum k v ans = if new == zeroC then ans else Map.insert k new ans
+      where
+        new = f v
+{-# INLINEABLE cannonicalMap #-}
+
+-- Pointwise comparison assuming the map is CannonicalZero, and we assume semantically that
+-- the value for keys not appearing in the map is 'zeroC'
+
+pointWise ::
+  (Ord k, CannonicalZero v) =>
+  (v -> v -> Bool) ->
+  Map k v ->
+  Map k v ->
+  Bool
+pointWise _ Tip Tip = True
+pointWise p Tip (m@(Bin _ _ _ _ _)) = all (zeroC `p`) m
+pointWise p (m@(Bin _ _ _ _ _)) Tip = all (`p` zeroC) m
+pointWise p m (Bin _ k v2 ls rs) =
+  case Map.splitLookup k m of
+    (lm, Just v1, rm) -> p v1 v2 && pointWise p ls lm && pointWise p rs rm
+    _ -> False