diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,3 @@
+## [0.0.1] - 2023-11-05
+
+Initial version
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,30 @@
+# Mappings
+
+## What's it do?
+
+This package does two jobs:
+
+* It offers a general typeclass [`Mapping`](src/Data/Mapping.hs) for
+  types which represent functions `k -> v` (for fixed `k`, but
+  arbitrary ordered `v`).
+
+  There are some fairly straightforward examples which build up
+  mappings where `k` is `Either`, or a pair, or `Maybe`, or `Bool`.
+
+* Three less trivial implementations are provided:
+
+    * [Decision diagrams](src/Data/Mapping/Decision.hs), with nodes
+       which may themselves be an arbitrary `Mapping` (there is some
+       code for viewing these in the `examples` directory);
+
+    * [Piecewise constant maps](src/Data/Mapping/Piecewise.hs) on an
+       ordered domain `k`;
+
+    * [Maps equipped with a default value](src/Data/Mapping/MapWithDefault.hs).
+
+
+## Why did I bother?
+
+The aim is to use decision diagrams with nodes that are piecewise
+constant maps to store monomials for Grobner basis algorithms.
+
diff --git a/examples/View.hs b/examples/View.hs
new file mode 100644
--- /dev/null
+++ b/examples/View.hs
@@ -0,0 +1,53 @@
+module Main where
+
+import Prelude hiding ((&&), (||), not, all)
+import Data.Algebra.Boolean ((&&), (||), not, all)
+import Data.Mapping
+import Data.Mapping.Decision
+
+
+main :: IO ()
+main = do
+  do
+    let x = test "x" :: AlgebraWrapper (String -> Bool) (Decision Bool OnBool String) Bool
+    let y = test "y"
+
+    putStrLn "  x"
+    putStrLn "-----"
+    putStrLn . debugShow $ algebraUnwrap x
+    putStrLn ""
+
+    putStrLn "  not x"
+    putStrLn "---------"
+    putStrLn . debugShow $ algebraUnwrap (not x)
+    putStrLn ""
+
+    putStrLn "  x && y"
+    putStrLn "----------"
+    putStrLn . debugShow $ algebraUnwrap (x && y)
+    putStrLn ""
+
+    putStrLn "  y && x"
+    putStrLn "----------"
+    putStrLn . debugShow $ algebraUnwrap (y && x)
+    putStrLn ""
+
+    putStrLn "  x || y"
+    putStrLn "----------"
+    putStrLn . debugShow $ algebraUnwrap (x || y)
+    putStrLn ""
+
+    putStrLn "  y || x"
+    putStrLn "----------"
+    putStrLn . debugShow $ algebraUnwrap (y || x)
+    putStrLn ""
+
+  do
+    putStrLn "  independent sets in C_100"
+    putStrLn "-----------------------------"
+    let l2 = (100,1):[(n,n+1) | n <- [1..99]]
+    let l3 = (99,100,1):(100,1,2):[(n,n+1,n+2) | n <- [1..98]]
+    let independent = all (\(i,j) -> not (test i && test j)) l2
+    let maximal = all (\(i,j,k) -> test i || test j || test k) l3
+    let AlgebraWrapper t = independent && maximal :: AlgebraWrapper (Int -> Bool) (Decision Bool OnBool Int) Bool
+    putStrLn $ debugShow t
diff --git a/mappings.cabal b/mappings.cabal
new file mode 100644
--- /dev/null
+++ b/mappings.cabal
@@ -0,0 +1,89 @@
+cabal-version: 2.2
+
+-- This file has been generated from package.yaml by hpack version 0.36.0.
+--
+-- see: https://github.com/sol/hpack
+
+name:           mappings
+version:        0.0.1.0
+synopsis:       Types which represent functions k -> v
+description:    Please read README.md on github
+category:       Data structures
+homepage:       https://github.com/jcranch/mapping#readme
+bug-reports:    https://github.com/jcranch/mapping/issues
+author:         James Cranch
+maintainer:     j.d.cranch@sheffield.ac.uk
+copyright:      2023 James Cranch
+license:        BSD-3-Clause
+build-type:     Simple
+extra-source-files:
+    README.md
+    CHANGELOG.md
+
+source-repository head
+  type: git
+  location: https://github.com/jcranch/mapping
+
+library
+  exposed-modules:
+      Data.Bijection
+      Data.Mapping
+      Data.Mapping.Decision
+      Data.Mapping.MapWithDefault
+      Data.Mapping.Piecewise
+      Data.Mapping.Util
+  other-modules:
+      Paths_mappings
+  autogen-modules:
+      Paths_mappings
+  hs-source-dirs:
+      src
+  ghc-options: -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns -Wredundant-constraints
+  build-depends:
+      base >=4.18 && <4.20
+    , cond ==0.4.*
+    , containers >=0.6.6 && <0.7
+    , formatting >=7.0.0 && <7.3
+    , partialord >=0.0.2 && <0.1
+  default-language: GHC2021
+
+executable view
+  main-is: View.hs
+  other-modules:
+      Paths_mappings
+  autogen-modules:
+      Paths_mappings
+  hs-source-dirs:
+      examples
+  ghc-options: -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      base >=4.18 && <4.20
+    , cond ==0.4.*
+    , containers >=0.6.6 && <0.7
+    , formatting >=7.0.0 && <7.3
+    , mappings
+    , partialord >=0.0.2 && <0.1
+  default-language: GHC2021
+
+test-suite mapping
+  type: exitcode-stdio-1.0
+  main-is: Spec.hs
+  other-modules:
+      Data.Mapping.DecisionSpec
+      Data.Mapping.MapWithDefaultSpec
+      Data.Mapping.PiecewiseSpec
+      Paths_mappings
+  autogen-modules:
+      Paths_mappings
+  hs-source-dirs:
+      test
+  ghc-options: -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      base >=4.18 && <4.20
+    , cond ==0.4.*
+    , containers >=0.6.6 && <0.7
+    , formatting >=7.0.0 && <7.3
+    , hspec ==2.11.*
+    , mappings
+    , partialord >=0.0.2 && <0.1
+  default-language: GHC2021
diff --git a/src/Data/Bijection.hs b/src/Data/Bijection.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Bijection.hs
@@ -0,0 +1,77 @@
+module Data.Bijection where
+
+import Data.IntMap.Strict (IntMap)
+import qualified Data.IntMap.Strict as IM
+import qualified Data.IntMap.Merge.Strict as IM
+
+
+compatibleInsert :: (Eq a) => Int -> a -> IntMap a -> Maybe (IntMap a)
+compatibleInsert x y = let
+  f (Just z) = if y == z then Just (Just y) else Nothing
+  f Nothing  = Just (Just y)
+  in IM.alterF f x
+
+compatibleUnion :: (Eq a) => IntMap a -> IntMap a -> Maybe (IntMap a)
+compatibleUnion = let
+  f _ x y = if x == y then Just x else Nothing
+  in IM.mergeA IM.preserveMissing IM.preserveMissing (IM.zipWithAMatched f)
+
+data Bij = Bij {
+  rightwards :: IntMap Int,
+  leftwards :: IntMap Int
+} deriving (Eq, Ord)
+
+empty :: Bij
+empty = Bij IM.empty IM.empty
+
+singleton :: Int -> Int -> Bij
+singleton x y = Bij (IM.singleton x y) (IM.singleton y x)
+
+match :: Int -> Int -> Bij -> Maybe Bij
+match x y (Bij r l) = liftA2 Bij (compatibleInsert x y r) (compatibleInsert y x l)
+
+combine :: Bij -> Bij -> Maybe Bij
+combine (Bij r1 l1) (Bij r2 l2) = liftA2 Bij (compatibleUnion r1 r2) (compatibleUnion l1 l2)
+
+pop :: Bij -> Maybe ((Int, Int), Bij)
+pop (Bij r l) = case IM.minViewWithKey r of
+  Nothing -> Nothing
+  Just ((i, j), r') -> Just ((i, j), Bij r' (IM.delete j l))
+
+-- | Don't check consistency, just take a union
+unsafeUnion :: Bij -> Bij -> Bij
+unsafeUnion (Bij r1 l1) (Bij r2 l2) = Bij (IM.union r1 r2) (IM.union l1 l2)
+
+-- | Don't check consistency, just take a diff
+unsafeDifference :: Bij -> Bij -> Bij
+unsafeDifference (Bij r1 l1) (Bij r2 l2) = Bij (IM.difference r1 r2) (IM.difference l1 l2)
+
+
+-- | A newtype, just to get a partial monoidal structure representing consistent
+-- unions.
+newtype MaybeBij = MaybeBij {
+  getMaybeBij :: Maybe Bij
+} deriving (Eq, Ord)
+
+instance Semigroup MaybeBij where
+  MaybeBij Nothing <> _ = MaybeBij Nothing
+  _ <> MaybeBij Nothing = MaybeBij Nothing
+  MaybeBij (Just a) <> MaybeBij (Just b) = MaybeBij (combine a b)
+
+instance Monoid MaybeBij where
+  mempty = MaybeBij (Just empty)
+
+msingleton :: Int -> Int -> MaybeBij
+msingleton i j = MaybeBij . Just $ singleton i j
+
+
+closeBijection :: (Int -> Int -> Maybe Bij) -> Bij -> Maybe Bij
+closeBijection f s = let
+  inner a n = case pop n of
+    Nothing -> Just a
+    Just ((i,j), n') -> case f i j of
+      Nothing -> Nothing
+      Just b -> case combine a b of
+        Nothing -> Nothing
+        Just a' -> inner a' (unsafeUnion n' (unsafeDifference b a))
+  in inner s s
diff --git a/src/Data/Mapping.hs b/src/Data/Mapping.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Mapping.hs
@@ -0,0 +1,282 @@
+{-# LANGUAGE
+    DeriveFunctor,
+    DerivingVia,
+    FlexibleInstances,
+    FunctionalDependencies,
+    QuantifiedConstraints,
+    ScopedTypeVariables
+  #-}
+
+module Data.Mapping where
+
+import Prelude hiding (not, (&&), (||))
+import Data.Algebra.Boolean (Boolean(..))
+import Data.Function (on)
+import Data.Functor.Const (Const(..))
+import Data.Functor.Identity (Identity(..))
+import Data.Monoid (All(..))
+import Data.PartialOrd
+import Data.Set (Set)
+import qualified Data.Set as S
+import Data.Void (Void)
+
+
+-- | If @Mapping k m@, then @m v@ represents a function @k -> v@.
+--
+-- `Mapping` requires an instance of `Foldable`, folding over the
+-- values that appear. Given that a value can be associated with a
+-- very large collection of keys, the only folds that normally make
+-- sense are those over idempotent monoids.
+class Foldable m => Mapping k m | m -> k where
+  cst :: v -> m v
+
+  act :: m v -> k -> v
+
+  isConst :: Ord v => m v -> Maybe v
+
+  mtraverse :: (Applicative f, Ord v) => (u -> f v) -> m u -> f (m v)
+
+  mmap :: Ord v => (u -> v) -> m u -> m v
+  mmap p = runIdentity . mtraverse (Identity . p)
+
+  mergeA :: (Applicative f, Ord w) => (u -> v -> f w) -> m u -> m v -> f (m w)
+
+  merge :: Ord w => (u -> v -> w) -> m u -> m v -> m w
+  merge p m n = let
+    q x y = Identity $ p x y
+    in runIdentity $ mergeA q m n
+
+
+-- | A simultaneous foldMap over two maps
+pairMappings :: forall k m u v a. (Mapping k m, Monoid a) => (u -> v -> a) -> m u -> m v -> a
+pairMappings p m n = let
+  q :: u -> v -> Const a Void
+  q x y = Const $ p x y
+  in getConst (mergeA q m n)
+
+-- | What values can these two take simultaneously?
+mutualValues :: (Ord u, Ord v, Mapping k m) => m u -> m v -> Set (u, v)
+mutualValues = pairMappings $ curry S.singleton
+
+
+
+-- | A class representing data structures which have a concept of neighbouring
+-- values
+class Neighbourly m where
+  neighbours :: Ord v => m v -> Set (v, v)
+
+
+-- | A wrapper for representing pointwise algebraic structures on a Mapping
+--
+-- Eventually would like to use this only for "deriving via"
+newtype AlgebraWrapper k m a = AlgebraWrapper { algebraUnwrap :: m a }
+
+instance (Mapping k m, Ord a, Semigroup a) => Semigroup (AlgebraWrapper k m a) where
+  (<>) = (AlgebraWrapper .) . merge (<>) `on` algebraUnwrap
+
+instance (Mapping k m, Ord a, Monoid a) => Monoid (AlgebraWrapper k m a) where
+  mempty = AlgebraWrapper $ cst mempty
+
+instance (Mapping k m, Ord a, Num a) => Num (AlgebraWrapper k m a) where
+  (+) =  (AlgebraWrapper .) . merge (+) `on` algebraUnwrap
+  (-) =  (AlgebraWrapper .) . merge (-) `on` algebraUnwrap
+  (*) =  (AlgebraWrapper .) . merge (*) `on` algebraUnwrap
+  fromInteger = AlgebraWrapper . cst . fromInteger
+  abs = AlgebraWrapper . mmap abs . algebraUnwrap
+  negate = AlgebraWrapper . mmap negate . algebraUnwrap
+  signum = AlgebraWrapper . mmap signum . algebraUnwrap
+
+instance (Mapping k m, Ord a, Boolean a) => Boolean (AlgebraWrapper k m a) where
+  true = AlgebraWrapper $ cst true
+  false = AlgebraWrapper $ cst false
+  not = AlgebraWrapper . mmap not . algebraUnwrap
+  (&&) = (AlgebraWrapper .) . merge (&&) `on` algebraUnwrap
+  (||) = (AlgebraWrapper .) . merge (||) `on` algebraUnwrap
+  xor = (AlgebraWrapper .) . merge xor `on` algebraUnwrap
+  (-->) = (AlgebraWrapper .) . merge (-->) `on` algebraUnwrap
+  (<-->) = (AlgebraWrapper .) . merge (<-->) `on` algebraUnwrap
+
+
+-- | Constant functions (on any domain)
+newtype Constant k v = Constant { constantValue :: v }
+
+instance Foldable (Constant k) where
+  foldMap f (Constant a) = f a
+
+instance Mapping k (Constant k) where
+  cst = Constant
+  act (Constant x) _ = x
+  mmap f (Constant x) = Constant $ f x
+  mtraverse f (Constant x) = Constant <$> f x
+  isConst (Constant x) = Just x
+  merge f (Constant x) (Constant y) = Constant $ f x y
+  mergeA f (Constant x) (Constant y) = Constant <$> f x y
+
+instance Neighbourly (Constant k) where
+  neighbours = const S.empty
+
+{-
+deriving via (AlgebraWrapper k (Constant k) v)
+  instance (Ord v, Semigroup v) => Semigroup (Constant k v)
+
+deriving via (AlgebraWrapper k (Constant k) v)
+  instance (Ord v, Monoid v) => Monoid (Constant k v)
+
+deriving via (AlgebraWrapper k (Constant k) v)
+  instance (Ord v, Num v) => Num (Constant k v)
+-}
+
+
+-- | Binary decisions, as functions defined on Bool
+data OnBool a = OnBool {
+  onFalse :: a,
+  onTrue :: a
+} deriving (Eq, Ord, Show, Functor)
+
+instance Foldable OnBool where
+  foldMap p (OnBool x y) = p x <> p y
+
+instance Traversable OnBool where
+  traverse f (OnBool x y) = liftA2 OnBool (f x) (f y)
+
+instance Mapping Bool OnBool where
+  cst x = OnBool x x
+  mmap = fmap
+  mtraverse = traverse
+  act (OnBool x _) False = x
+  act (OnBool _ x) True = x
+  isConst (OnBool x y)
+    | x == y    = Just x
+    | otherwise = Nothing
+  mergeA h (OnBool x1 y1) (OnBool x2 y2) = liftA2 OnBool (h x1 x2) (h y1 y2)
+  merge h (OnBool x1 y1) (OnBool x2 y2) = OnBool (h x1 x2) (h y1 y2)
+
+instance Neighbourly OnBool where
+  neighbours (OnBool x y)
+    | x == y    = S.empty
+    | otherwise = S.singleton (x, y)
+
+{-
+-- May work with a future version of cond
+deriving via (AlgebraWrapper Bool OnBool b)
+  instance (Ord b, Boolean b) => Boolean (OnBool b)
+-}
+
+
+-- | Maps on Maybe
+data OnMaybe k m v = OnMaybe {
+  onNothing :: v,
+  onJust :: m v
+}
+
+instance Foldable m => Foldable (OnMaybe k m) where
+  foldMap f (OnMaybe x a) = f x <> foldMap f a
+
+instance Mapping k m => Mapping (Maybe k) (OnMaybe k m) where
+  cst x = OnMaybe x $ cst x
+  mmap p (OnMaybe x a) = OnMaybe (p x) (mmap p a)
+  mtraverse p (OnMaybe x a) = liftA2 OnMaybe (p x) (mtraverse p a)
+  act (OnMaybe x _) Nothing = x
+  act (OnMaybe _ a) (Just y) = act a y
+  isConst (OnMaybe x a) = do
+    y <- isConst a
+    if x == y then Just x else Nothing
+  merge h (OnMaybe x a) (OnMaybe y b) = OnMaybe (h x y) (merge h a b)
+  mergeA h (OnMaybe x a) (OnMaybe y b) = liftA2 OnMaybe (h x y) (mergeA h a b)
+
+
+-- | Maps on Either
+data OnEither k l m n v = OnEither {
+  onLeft :: m v,
+  onRight :: n v
+} deriving (Eq, Ord)
+
+instance (Foldable m, Foldable n) => Foldable (OnEither k l m n) where
+  foldMap p (OnEither f g) = foldMap p f <> foldMap p g
+
+instance (Mapping k m,
+          Mapping l n)
+       => Mapping (Either k l) (OnEither k l m n) where
+  cst x = OnEither (cst x) (cst x)
+  mmap p (OnEither f g) = OnEither (mmap p f) (mmap p g)
+  mtraverse p (OnEither f g) = liftA2 OnEither (mtraverse p f) (mtraverse p g)
+  act (OnEither f _) (Left x) = act f x
+  act (OnEither _ g) (Right y) = act g y
+  isConst (OnEither f g) = do
+    x <- isConst f
+    y <- isConst g
+    if x == y then Just x else Nothing
+  mergeA h (OnEither f1 g1) (OnEither f2 g2) = liftA2 OnEither (mergeA h f1 f2) (mergeA h g1 g2)
+  merge h (OnEither f1 g1) (OnEither f2 g2) = OnEither (merge h f1 f2) (merge h g1 g2)
+
+{-
+-- May work with a future version of cond
+deriving via (AlgebraWrapper (Either k l) (OnEither k l m n) b)
+  instance (Mapping k m, Mapping l n, Ord b, Boolean b) => Boolean (OnEither k l m n b)
+-}
+
+
+-- | Maps on pairs
+newtype OnPair k l m n v = OnPair {
+  asComposite :: m (n v)
+} deriving (Eq, Ord)
+
+instance (Foldable m, Foldable n) => Foldable (OnPair k l m n) where
+  foldMap p (OnPair f) = foldMap (foldMap p) f
+
+instance (Mapping k m,
+          Mapping l n,
+          forall v. Ord v => Ord (n v))
+       => Mapping (k, l) (OnPair k l m n) where
+  cst x = OnPair . cst $ cst x
+  mmap p (OnPair f) = OnPair (mmap (mmap p) f)
+  mtraverse p (OnPair f) = OnPair <$> mtraverse (mtraverse p) f
+  act (OnPair f) (x, y) = act (act f x) y
+  isConst (OnPair f) = isConst =<< isConst f
+  mergeA h (OnPair f) (OnPair g) = OnPair <$> mergeA (mergeA h) f g
+  merge h (OnPair f) (OnPair g) = OnPair $ merge (merge h) f g
+
+{-
+-- May work with a future version of cond
+deriving via (AlgebraWrapper (k, l) (OnPair k l m n) b)
+  instance (Mapping k m, Mapping l n, Ord b, Boolean b) => Boolean (OnPair k l m n b)
+-}
+
+
+-- Is the first a subset of the second?
+--
+-- With a future version of cond, we should be able to generalise this
+isSubset :: Mapping k m => m Bool -> m Bool -> Bool
+isSubset m n = let
+  p True False = All False
+  p _ _        = All True
+  in getAll $ pairMappings p m n
+
+-- Are the two true on distinct values?
+--
+-- Again, with a future version of cond, we should be able to generalise this
+isDisjoint :: Mapping k m => m Bool -> m Bool -> Bool
+isDisjoint m n = let
+  p True True = All False
+  p _ _       = All True
+  in getAll $ pairMappings p m n
+
+
+-- | A wrapper to allow defining `PartialOrd` instances on mappings whose keys
+-- have an `Ord` instance.
+newtype OrdWrapper k m v = OrdWrapper {
+  getOrdMapping :: m v
+}
+
+instance (Mapping k m, Ord v) => PartialOrd (OrdWrapper k m v) where
+  compare' (OrdWrapper u) (OrdWrapper v) = pairMappings fromCompare u v
+
+
+  -- | A wrapper to allow defining `PartialOrd` instances on mappings whose keys
+  -- have a `PartialOrd` instance.
+newtype PartialOrdWrapper k m v = PartialOrdWrapper {
+  getPartialOrdMapping :: m v
+}
+
+instance (Mapping k m, PartialOrd v) => PartialOrd (PartialOrdWrapper k m v) where
+  compare' (PartialOrdWrapper u) (PartialOrdWrapper v) = pairMappings compare' u v
diff --git a/src/Data/Mapping/Decision.hs b/src/Data/Mapping/Decision.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Mapping/Decision.hs
@@ -0,0 +1,558 @@
+{-# LANGUAGE
+      MultiParamTypeClasses,
+      OverloadedStrings,
+      RankNTypes,
+      StandaloneDeriving,
+      TupleSections
+  #-}
+
+-- | Decision diagrams, parametric in the mapping type for the decisions.
+--
+-- This is inspired by binary decision diagrams (as described in detail in
+-- Knuth's The Art of Computer Programming, volume 4A); these are the specific
+-- case where m is `BoolMapping` and v is `Bool`. Our algorithms are mostly
+-- straightforward generalisations of those considered there.
+--
+-- TODO
+--  * Decisions go upwards in order currently, I believe; should they go
+--    downwards, to coincide with lexicographical orderings on maps and hence
+--    maybe make smaller decision diagrams?
+--    We can use Down if necessary to amend this
+--  * Increase test coverage
+--  * Examples:
+--     - finding optima
+--     - finding random elements
+--    (as examples of the more general functions, already coded, I hope)
+--  * Separate out various stuff into other modules?
+--  * Reformat types
+--  * Refactor by changing order of arguments of addLeaf and addNode and simplifying
+--    Might even want a more general Node, for even greater simplicity
+--    Could use a pair instead of node.
+--  * Documentation
+--  * Tidy out any commented-out code
+--
+-- MAYBE TO DO
+--  * Implement the two monadic algorithms?
+--  * Comment on a more efficient mapping algorithm
+--  * Composition algorithm?
+--      composite :: (a -> Decision k m v w) -> Decision k m a v -> Decision k m a w ???
+--  * Optimisation by reordering
+module Data.Mapping.Decision where
+
+import Data.Algebra.Boolean (Boolean(..))
+import Data.Bijection (Bij)
+import qualified Data.Bijection as B
+import Data.Bits (complement)
+import Data.Bool (bool)
+import Data.Foldable (toList)
+import Data.Functor.Identity (Identity(..))
+import Data.IntSet (IntSet)
+import qualified Data.IntSet as IS
+import Data.Ord (comparing)
+import Data.Sequence (Seq, (|>))
+import qualified Data.Sequence as Q
+import Data.Set (Set)
+import qualified Data.Set as S
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as M
+import Data.Mapping.Util (insertIfAbsent)
+import Formatting ((%))
+import qualified Formatting as F
+
+import Data.Mapping
+
+
+-- | A node of a decision diagram: which value do we scrutinise, and what do we
+-- do with it?
+data Node k m a = Node {
+  nodeDecision :: !a,
+  nodeBranch :: !(m Int)
+}
+
+deriving instance (Eq a, Eq (m Int)) => Eq (Node k m a)
+
+deriving instance (Ord a, Ord (m Int)) => Ord (Node k m a)
+
+
+-- | A decision diagram (with no preferred starting point), containing
+-- leaves (representing final values of the decision process) indexed
+-- from -1 downwards, and nodes (representing the need to scrutinise a
+-- value) indexed from 0 upwards
+data Base k m a v = Base {
+  leaves :: Seq v,
+  nodes :: Seq (Node k m a)
+}
+
+-- | A decision diagram with a starting point
+data Decision k m a v = Decision {
+  base :: !(Base k m a v),
+  start :: !Int
+}
+
+-- | A value for every node of a base
+data BaseMap v = BaseMap {
+  onLeaves :: Seq v,
+  onNodes :: Seq v
+}
+
+-- | Index a BaseMap
+bindex :: BaseMap v -> Int -> v
+bindex (BaseMap l m) x
+  | x < 0     = Q.index l $ complement x
+  | otherwise = Q.index m x
+
+
+-- | Close a set under an operation
+closure :: (Int -> IntSet) -> IntSet -> IntSet
+closure f = let
+  inner old new = case IS.minView new of
+    Nothing -> old
+    Just (x, new') -> let
+      old' = IS.insert x old
+      in inner old' (new' `IS.union` (f x `IS.difference` old'))
+  in inner IS.empty
+
+
+-- | A general kind of recursive function on a Base
+baseRecurse :: (Ord c,
+                Mapping k m)
+            => (v -> c)
+               -- ^ What to do on a value
+            -> (a -> m c -> c)
+               -- ^ What do do on a node
+            -> Base k m a v
+               -- ^ Input base
+            -> BaseMap c
+baseRecurse p q (Base l m) = let
+  l' = p <$> l
+  f v (Node x n) = v |> q x (mmap (bindex (BaseMap l' v)) n)
+  in BaseMap l' $ foldl f Q.empty m
+
+-- | A general kind of recursive function on a Decision
+decisionRecurse :: (Ord c,
+                    Mapping k m)
+                 => (v -> c)
+                 -- ^ What to do on a value
+                 -> (a -> m c -> c)
+                 -- ^ What do do on a node
+                 -> Decision k m a v
+                 -- ^ Input decision
+                 -> c
+decisionRecurse p q (Decision b s) = bindex (baseRecurse p q b) s
+
+
+-- | A general counting function
+--
+-- Not sure if this is the best way of laying this out
+genCounts :: (Ord a, Ord n, Mapping k m) => (v -> n) -> (a -> a -> n -> n) -> (m n -> n) -> a -> a -> Decision k m a v -> n
+genCounts onValue promote combine x0 x1 = let
+  p = uncurry . promote
+  f x = (x1, onValue x)
+  g y m = (y, combine $ mmap (p y) m)
+  in p x0 . decisionRecurse f g
+
+-- | How many values are True in a binary decision diagram?
+numberTrue :: (Integral a) => a -> a -> Decision Bool OnBool a Bool -> Integer
+numberTrue x0 x1 = let
+  f a = if a then 1 else 0
+  g y x n = n * (2 ^ (x-y-1))
+  h (OnBool u v) = u + v
+  in genCounts f g h (x0-1) (x1+1)
+
+
+-- | Build a sequence from key-value pairs; we take on trust that all
+-- values are represented once.
+fromKeyVals :: (Foldable f) => f (Int,a) -> Seq a
+fromKeyVals = fmap snd . Q.sortBy (comparing fst) . Q.fromList . toList
+
+
+-- | A data structure for work-in-progress decision diagrams
+data Builder o k m a v = Builder {
+  leavesMap :: Map v Int,
+  nodesMap :: Map (Node k m a) Int,
+  fromOld :: Map o Int
+}
+
+emptyBuilder :: Builder o k m a v
+emptyBuilder = Builder M.empty M.empty M.empty
+
+addLeaf :: (Ord o, Ord v) => v -> o -> Builder o k m a v -> Builder o k m a v
+addLeaf x y (Builder l m o) = let
+  i = complement (M.size l)
+  (j, s) = insertIfAbsent x i l
+  o' = M.insert y j o
+  in case s of
+    Nothing -> Builder l m o'
+    Just l' -> Builder l' m o'
+
+addNode :: (Ord o, Ord (m Int), Ord a, Mapping k m) => a -> m o -> o -> Builder o k m a v -> Builder o k m a v
+addNode r a y (Builder l m o) = let
+  b = mmap (o M.!) a
+  in case isConst b of
+    Just j -> Builder l m (M.insert y j o)
+    Nothing -> let
+      i = M.size m
+      (j, s) = insertIfAbsent (Node r b) i m
+      o' = M.insert y j o
+      in case s of
+        Nothing -> Builder l m o'
+        Just m' -> Builder l m' o'
+
+makeBuilder :: (Mapping k m,
+                Ord o,
+                Ord (m Int),
+                Ord a,
+                Ord v)
+             => Map o v
+             -> Map o (a, m o)
+             -> Builder o k m a v
+makeBuilder l m = let
+  b0 = emptyBuilder
+  makeL b i x = addLeaf x i b
+  b1 = M.foldlWithKey' makeL b0 l
+  makeN b i (r, o) = addNode r o i b
+  b2 = M.foldlWithKey' makeN b1 m
+  in b2
+
+buildBase :: Builder o k m a v -> Base k m a v
+buildBase (Builder l m _) = let
+  l' = fromKeyVals . fmap (\(x,i) -> (complement i,x)) $ M.toList l
+  m' = fromKeyVals . fmap (\(x,i) -> (i,x)) $ M.toList m
+  in Base l' m'
+
+buildDecision :: Ord o => o -> Builder o k m a v -> Decision k m a v
+buildDecision s b@(Builder _ _ o) = Decision (buildBase b) (o M.! s)
+
+singleNode :: (Ord v, Mapping k m) => a -> m v -> Decision k m a v
+singleNode r n = let
+  f b x = addLeaf x x b
+  Builder l _ o = foldl f emptyBuilder n
+  m = M.singleton (Node r $ mmap (o M.!) n) 0
+  in Decision (buildBase $ Builder l m o) 0
+
+-- | A building block for BDD's - tests if a variable is true
+--
+-- Again, would be nice to remove the AlgebraWrapper
+genTest :: Boolean b => a -> AlgebraWrapper (a -> Bool) (Decision Bool OnBool a) b
+genTest r = let
+  l = Q.fromList [false, true]
+  m = pure . Node r $ OnBool (-1) (-2)
+  s = 0
+  in AlgebraWrapper $ Decision (Base l m) s
+
+-- | Test if a variable is true (specialised to `Bool`)
+test :: a -> AlgebraWrapper (a -> Bool) (Decision Bool OnBool a) Bool
+test = genTest
+
+-- | Rapidly take the conjunction of the inputs
+buildAll :: Mapping k m => Map a (m Bool) -> Decision k m a Bool
+buildAll d = let
+  l = Q.fromList [true, false]
+  s = M.size d
+  m = Q.fromList $ do
+    (i,(r,n)) <- zip [0..] (M.toDescList d)
+    pure (Node r (mmap (bool (-2) (i-1)) n))
+  in Decision (Base l m) (s-1)
+
+-- | Rapidly take the disjunction of the inputs
+buildAny :: Mapping k m => Map a (m Bool) -> Decision k m a Bool
+buildAny d = let
+  l = Q.fromList [false, true]
+  s = M.size d
+  m = Q.fromList $ do
+    (i,(r,n)) <- zip [0..] (M.toDescList d)
+    pure (Node r (mmap (bool (i-1) (-2)) n))
+  in Decision (Base l m) (s-1)
+
+
+-- | Traverse bases
+baseTraverse :: (Applicative f, Ord a, Ord (m Int), Ord w, Mapping k m) => (v -> f w) -> Base k m a v -> f (Builder Int k m a w)
+baseTraverse p (Base l m) = let
+  t0 = pure emptyBuilder
+
+  t1 = let
+    f b i x = liftA2 (\b' px' -> addLeaf px' (complement i) b') b (p x)
+    in Q.foldlWithIndex f t0 l
+
+  t2 = let
+    f b i (Node r d) = addNode r d i <$> b
+    in Q.foldlWithIndex f t1 m
+
+  in t2
+
+
+-- | Map bases
+baseMap :: (Ord a, Ord (m Int), Ord w, Mapping k m) => (v -> w) -> Base k m a v -> Builder Int k m a w
+baseMap p = runIdentity . baseTraverse (Identity . p)
+
+
+-- | A more general map for `Base`, where the shape of nodes can change
+baseTransform ::    (Ord a, Ord (n Int), Mapping l n, Ord w)
+                 => (v -> w)
+                 -> (forall x. a -> m x -> n x)
+                 -> Base k m a v
+                 -> IntSet
+                 -> Builder Int l n a w
+baseTransform p q (Base l m) = let
+
+  close aL aN s = case IS.maxView s of
+   Nothing -> makeBuilder aL aN
+   Just (i, s') -> if i < 0
+     then let
+       x = p (Q.index l $ complement i)
+       in close (M.insert i x aL) aN s'
+     else let
+       Node r n = Q.index m i
+       o = q r n
+       s'' = IS.union s' . IS.fromList $ toList o
+       in close aL (M.insert i (r, o) aN) s''
+
+  in close M.empty M.empty
+
+
+-- | A more general map for `Decision`, where the shape of nodes can change
+decisionTransform :: (Mapping l n,
+                      Ord (n Int),
+                      Ord a,
+                      Ord w)
+                   => (v -> w)
+                   -> (forall x. a -> m x -> n x)
+                   -> Decision k m a v
+                   -> Decision l n a w
+decisionTransform p q (Decision b s) = let
+  in buildDecision s $ baseTransform p q b (IS.singleton s)
+
+
+-- | Fill in some values of a map
+-- > act (restrict h d) f = let
+-- >   f' x = case h x of
+-- >     Just y  -> y
+-- >     Nothing -> f x
+-- >   in act d f'
+restrict :: (Ord (m Int), Ord v, Ord a, Mapping k m) => (a -> Maybe k) -> Decision k m a v -> Decision k m a v
+restrict f = let
+  g x m = case f x of
+    Nothing -> m
+    Just c -> cst (act m c)
+  in decisionTransform id g
+
+
+-- | A general function for merging bases
+baseGenMerge ::    (Ord a, Ord w, Ord (o Int), Mapping l o)
+                => (u -> v -> w)
+                -> (forall x . Ord x => a -> m x -> o x)
+                -> (forall y . Ord y => a -> n y -> o y)
+                -> (forall x y. (Ord x, Ord y) => a -> m x -> n y -> o (x, y))
+                -> Base h m a u -> Base k n a v -> Set (Int, Int) -> Builder (Int, Int) l o a w
+baseGenMerge pLL pNL pLN pNN (Base l1 m1) (Base l2 m2) = let
+
+  close aLL aNL aLN aNN s = case S.maxView s of
+    Nothing -> make aLL aNL aLN aNN
+    Just ((i1, i2), s') -> case (i1 < 0, i2 < 0) of
+      ( True,  True) -> let
+        x = pLL (Q.index l1 $ complement i1) (Q.index l2 $ complement i2)
+        in close (M.insert (i1, i2) x aLL) aNL aLN aNN s'
+      ( True, False) -> let
+        Node r2 n2 = Q.index m2 i2
+        o = mmap (i1,) $ pLN r2 n2
+        s'' = S.union s' . S.fromList $ toList o
+        in close aLL aNL (M.insert (i1, i2) (r2, o) aLN) aNN s''
+      (False,  True) -> let
+        Node r1 n1 = Q.index m1 i1
+        o = mmap (,i2) $ pNL r1 n1
+        s'' = S.union s' . S.fromList $ toList o
+        in close aLL (M.insert (i1, i2) (r1, o) aNL) aLN aNN s''
+      (False, False) -> let
+        Node r1 n1 = Q.index m1 i1
+        Node r2 n2 = Q.index m2 i2
+        (r, o) = case compare r1 r2 of
+          LT -> (r1, mmap (,i2) $ pNL r1 n1)
+          GT -> (r2, mmap (i1,) $ pLN r2 n2)
+          EQ -> (r1, pNN r1 n1 n2)
+        s'' = S.union s' . S.fromList $ toList o
+        in close aLL aNL aLN (M.insert (i1, i2) (r, o) aNN) s''
+
+  make aLL aNL aLN aNN = let
+
+    b0 = emptyBuilder
+
+    makeL b (i, j) x = addLeaf x (i, j) b
+    b1 = M.foldlWithKey' makeL b0 aLL
+
+    makeN b (i, j) (r, o) = addNode r o (i, j) b
+    b2 = M.foldlWithKey' makeN b1 aNL
+    b3 = M.foldlWithKey' makeN b2 aLN
+    b4 = M.foldlWithKey' makeN b3 aNN
+    in b4
+
+  in close M.empty M.empty M.empty M.empty
+
+
+-- | Merge two bases in an applicative functor
+baseMergeA ::    (Applicative f, Ord a, Ord w, Ord (m Int), Mapping k m)
+              => (u -> v -> f w)
+              -> Base k m a u -> Base k m a v -> Set (Int, Int) -> f (Builder (Int, Int) k m a w)
+baseMergeA p (Base l1 m1) (Base l2 m2) = let
+
+  close aLL aNL aLN aNN s = case S.maxView s of
+    Nothing -> make aLL aNL aLN aNN
+    Just ((i1, i2), s') -> case (i1 < 0, i2 < 0) of
+      ( True,  True) -> let
+        x = p (Q.index l1 $ complement i1) (Q.index l2 $ complement i2)
+        in close (M.insert (i1, i2) x aLL) aNL aLN aNN s'
+      ( True, False) -> let
+        Node r2 n2 = Q.index m2 i2
+        o = mmap (i1,) n2
+        s'' = S.union s' . S.fromList $ toList o
+        in close aLL aNL (M.insert (i1, i2) (r2, o) aLN) aNN s''
+      (False,  True) -> let
+        Node r1 n1 = Q.index m1 i1
+        o = mmap (,i2) n1
+        s'' = S.union s' . S.fromList $ toList o
+        in close aLL (M.insert (i1, i2) (r1, o) aNL) aLN aNN s''
+      (False, False) -> let
+        Node r1 n1 = Q.index m1 i1
+        Node r2 n2 = Q.index m2 i2
+        (r,o) = case compare r1 r2 of
+          LT -> (r1, mmap (,i2) n1)
+          GT -> (r2, mmap (i1,) n2)
+          EQ -> (r1, merge (,) n1 n2)
+        s'' = S.union s' . S.fromList $ toList o
+        in close aLL aNL aLN (M.insert (i1, i2) (r, o) aNN) s''
+
+  make aLL aNL aLN aNN = let
+
+    b0 = pure emptyBuilder
+
+    makeL b (i, j) = liftA2 (\b' x'-> addLeaf x' (i, j) b') b
+    b1 = M.foldlWithKey' makeL b0 aLL
+
+    makeN b (i, j) (r, o) = addNode r o (i, j) <$> b
+    b2 = M.foldlWithKey' makeN b1 aNL
+    b3 = M.foldlWithKey' makeN b2 aLN
+    b4 = M.foldlWithKey' makeN b3 aNN
+    in b4
+
+  in close M.empty M.empty M.empty M.empty
+
+
+-- | Merge two bases
+baseMerge ::    (Ord a, Ord w, Ord (m Int), Mapping k m)
+             => (u -> v -> w)
+             -> Base k m a u -> Base k m a v -> Set (Int, Int) -> Builder (Int, Int) k m a w
+baseMerge p b1 b2 = let
+  p' x y = Identity $ p x y
+  in runIdentity . baseMergeA p' b1 b2
+
+
+-- | Folds over *all* the leaves; not something you want to do to an
+-- arbitrary base
+instance Foldable (Base k m a) where
+  foldMap p = foldMap p . leaves
+
+instance Foldable m => Foldable (Decision k m a) where
+  foldMap p (Decision (Base l m) s) = let
+    inner x old new = case IS.minView new of
+      Nothing        -> x
+      Just (i, new') -> if i < 0
+        then inner (x <> p (Q.index l (complement i))) (IS.insert i old) new'
+        else let
+          old' = IS.insert i old
+          extra = IS.difference (IS.fromList . toList . nodeBranch $ Q.index m i) old'
+          in inner x old' (IS.union new' extra)
+    in inner mempty IS.empty $ IS.singleton s
+
+instance (Ord a, Ord (m Int), Mapping k m) => Mapping (a -> k) (Decision k m a) where
+
+  cst x = Decision (Base (Q.singleton x) Q.empty) (-1)
+
+  act (Decision (Base l n) s) f = let
+    inner i
+      | i < 0 = Q.index l $ complement i
+      | otherwise = let
+          Node a m = Q.index n i
+          in inner . act m $ f a
+    in inner s
+
+  -- We assume the diagram is optimised, so it is constant only if it starts
+  -- with a leaf.
+  isConst (Decision (Base l _) s)
+    | s < 0     = Just . Q.index l $ complement s
+    | otherwise = Nothing
+
+  mtraverse p (Decision (Base l m) s) = buildDecision s <$> baseTraverse p (Base l m)
+
+  mmap p (Decision b s) = buildDecision s $ baseMap p b
+
+  merge p (Decision b1 s1) (Decision b2 s2) = buildDecision (s1, s2) $ baseMerge p b1 b2 (S.singleton (s1, s2))
+
+  mergeA p (Decision b1 s1) (Decision b2 s2) = buildDecision (s1, s2) <$> baseMergeA p b1 b2 (S.singleton (s1, s2))
+
+
+-- | Attempt to extend to a bijection
+checkBijection :: (Eq a, Eq v, Mapping k m) => Base k m a v -> Base k m a v -> Bij -> Maybe Bij
+checkBijection (Base l1 m1) (Base l2 m2) = let
+  consequences i j = case (i < 0, j < 0) of
+    (True, True) -> if Q.index l1 (complement i) == Q.index l2 (complement j)
+      then Just B.empty
+      else Nothing
+    (False, False) -> let
+      Node r1 o1 = Q.index m1 i
+      Node r2 o2 = Q.index m2 j
+      in if r1 == r2
+        then B.getMaybeBij $ pairMappings B.msingleton o1 o2
+        else Nothing
+    _ -> Nothing
+  in B.closeBijection consequences
+
+-- | Are these Decisions isomorphic?
+findBijection :: (Eq a, Eq v, Mapping k m) => Decision k m a v -> Decision k m a v -> Maybe Bij
+findBijection (Decision b1 s1) (Decision b2 s2) = checkBijection b1 b2 (B.singleton s1 s2)
+
+instance (Eq a, Eq v, Mapping k m) => Eq (Decision k m a v) where
+  u == v = case findBijection u v of
+    Just _ -> True
+    Nothing -> False
+
+
+-- | A ludicrously short definition!
+instance (Ord a, Ord v, Ord (m Int), Mapping k m) => Ord (Decision k m a v) where
+  compare = pairMappings compare
+
+
+-- | Output the structure of a Decision
+debugShow :: (Show a, Show v, Show (m Int)) => Decision k m a v -> String
+debugShow (Decision (Base l m) s) = let
+
+  p = 1 + max (1 + length (show (Q.length l))) (length (show (1 + Q.length m)))
+
+  prefix i = ((if i == s then "->" else "  ") <>)
+
+  leafLine t i x = let
+    j = complement i
+    in prefix j (F.formatToString (F.left p ' ' % ": " % F.shown % "\n") j x) <> t
+
+  nodeLine i (Node r n) t =
+    prefix i (F.formatToString (F.left p ' ' % ": " % F.shown % "; " % F.shown % "\n") i r n) <> t
+
+  in Q.foldlWithIndex leafLine (Q.foldrWithIndex nodeLine "" m) l
+
+
+instance (Mapping k m,
+          Neighbourly m,
+          Ord a,
+          Ord (m Int))
+       => Neighbourly (Decision k m a) where
+  neighbours (Decision (Base l m) s) = let
+    f v (Node _ n) = let
+      here = let
+        b = Base l m
+        e (i, j) = S.filter (uncurry (/=)) $ mutualValues (Decision b i) (Decision b j)
+        in foldMap e $ neighbours n
+      there = let
+        g i
+          | i < 0     = mempty
+          | otherwise = Q.index v i
+        in foldMap g n
+      in v |> (here <> there)
+    in Q.index (foldl f Q.empty m) s
diff --git a/src/Data/Mapping/MapWithDefault.hs b/src/Data/Mapping/MapWithDefault.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Mapping/MapWithDefault.hs
@@ -0,0 +1,87 @@
+module Data.Mapping.MapWithDefault where
+
+import Data.List (foldl', groupBy)
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as M
+import qualified Data.Map.Merge.Strict as M
+import Data.Mapping
+import Data.Maybe (fromMaybe, mapMaybe)
+import qualified Data.Set as S
+import Data.Mapping.Util
+
+
+-- | Mappings constant except on an enumerated set of values
+data MapWithDefault k v = MapWithDefault {
+  common :: v,
+  exceptions :: Map k v
+} deriving (Eq, Ord)
+
+fromList :: (Ord k, Eq v) => v -> [(k,v)] -> MapWithDefault k v
+fromList a = MapWithDefault a . M.fromList . mapMaybe (traverse (nonDefault a))
+
+instance (Show k, Show v) => Show (MapWithDefault k v) where
+  showsPrec d (MapWithDefault x l) =
+    ("fromList " <>) .
+    showsPrec d x .
+    showList (M.toList l)
+
+fromListWithKey :: (Ord k, Eq v) => v -> (k -> u -> v -> v) -> [(k, u)] -> MapWithDefault k v
+fromListWithKey a f = let
+  g m (k, x) = M.alter (nonDefault a . f k x . fromMaybe a) k m
+  in MapWithDefault a . foldl' g M.empty
+
+instance Foldable (MapWithDefault k) where
+  foldMap p (MapWithDefault a f) = p a <> foldMap p f
+
+instance Ord k => Mapping k (MapWithDefault k) where
+  cst x = MapWithDefault x M.empty
+  mmap p (MapWithDefault a f) = let
+    b = p a
+    q x = let
+      y = p x
+      in if b == y then Nothing else Just y
+    in MapWithDefault b $ M.mapMaybe q f
+  mtraverse p (MapWithDefault a f) = let
+    b = p a
+    e x y = if x == y then Nothing else Just y
+    g _ x = liftA2 e b (p x)
+    in liftA2 MapWithDefault b $ M.traverseMaybeWithKey g f
+  act (MapWithDefault a f) x = fromMaybe a (M.lookup x f)
+  isConst (MapWithDefault a f) = if M.null f then Just a else Nothing
+  mergeA h (MapWithDefault a f) (MapWithDefault b g) = let
+    e x y = if x == y then Just x else Nothing
+    c = h a b
+    l = M.traverseMissing (\_ x -> h x b)
+    r = M.traverseMissing (\_ y -> h a y)
+    h' _ x y = liftA2 e c $ h x y
+    t = M.zipWithMaybeAMatched h'
+    combine = M.mergeA l r t
+    in liftA2 MapWithDefault c $ combine f g
+  merge h (MapWithDefault a f) (MapWithDefault b g) = let
+    c = h a b
+    l = M.mapMissing (\_ x -> h x b)
+    r = M.mapMissing (\_ y -> h a y)
+    h' _ x y = let
+      z = h x y
+      in if z == c then Nothing else Just z
+    t = M.zipWithMaybeMatched h'
+    combine = M.merge l r t
+    in MapWithDefault c $ combine f g
+
+-- | This instance assumes that k is unbounded
+
+-- It would be possible to do something valid in greater generality (for
+-- example, a MaybeBounded class), which might be a good idea.
+instance (Enum k, Eq k) => Neighbourly (MapWithDefault k) where
+  neighbours (MapWithDefault a f) = let
+    c (x,_) (y,_) = succ x == y
+    d l = zip ([a] <> l) (l <> [a])
+    in S.fromList . concatMap (d . fmap snd) . groupBy c $ M.toAscList f
+
+
+
+{-
+-- May work with a future version of cond
+deriving via (AlgebraWrapper k (MapWithDefault k) b)
+  instance (Ord k, Ord b, Boolean b) => Boolean (MapWithDefault k b)
+-}
diff --git a/src/Data/Mapping/Piecewise.hs b/src/Data/Mapping/Piecewise.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Mapping/Piecewise.hs
@@ -0,0 +1,137 @@
+module Data.Mapping.Piecewise where
+
+import Control.Applicative (liftA3)
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as M
+import qualified Data.Set as S
+import Data.Mapping
+
+
+-- | A data structure storing mappings that are constant on
+-- intervals.
+--
+-- If the space of keys not discrete, then these mappings are
+-- right-continuous: values are in general defined on intervals $a
+-- \leq x < b$ which are closed on the left and open on the right.
+data Piecewise k v = Piecewise {
+  leftEnd :: v,
+  starts :: Map k v
+} deriving (Eq, Ord)
+
+piecewiseFromAsc :: Eq k => v -> [(k,v)] -> Piecewise k v
+piecewiseFromAsc k = Piecewise k . M.fromAscList
+
+instance (Show k, Show v) => Show (Piecewise k v) where
+  showsPrec d (Piecewise k m) =
+    ("piecewiseFromAsc " <>) .
+    showsPrec d k .
+    (" " <>) .
+    showList (M.toList m)
+
+changeAt :: v -> k -> v -> Piecewise k v
+changeAt a x b = Piecewise a $ M.singleton x b
+
+atLeast :: k -> Piecewise k Bool
+atLeast k = changeAt False k True
+
+lessThan :: k -> Piecewise k Bool
+lessThan k = changeAt True k False
+
+fromAscList :: (Ord k, Eq v) => v -> [(k,v)] -> Piecewise k v
+fromAscList = let
+  inner _ [] = []
+  inner a ((y,b):r)
+    | a == b    = inner a r
+    | otherwise = (y,b):inner b r
+  run x = Piecewise x . M.fromAscList . inner x
+  in run
+
+values :: Piecewise k v -> [v]
+values (Piecewise x m) = x : M.elems m
+
+instance Foldable (Piecewise k) where
+  foldMap f (Piecewise a m) = f a <> foldMap f m
+
+instance Ord k => Mapping k (Piecewise k) where
+
+  cst x = Piecewise x M.empty
+
+  act (Piecewise a f) x = case M.lookupLE x f of
+    Nothing -> a
+    Just (_,b) -> b
+
+  isConst (Piecewise a f) = if M.null f then Just a else Nothing
+
+  mmap p (Piecewise a f) = fromAscList (p a) (fmap p <$> M.toList f)
+
+  mtraverse p (Piecewise a f) = liftA2 fromAscList (p a) (traverse (traverse p) $ M.toList f)
+
+  merge p = let
+
+    inner a b c r@((x,a'):r') s@((y,b'):s') = case compare x y of
+      LT -> let
+        c' = p a' b
+        in if c' == c then inner a' b c r' s else (x,c'):inner a' b c' r' s
+      GT -> let
+        c' = p a b'
+        in if c' == c then inner a b' c r s' else (y,c'):inner a b' c' r s'
+      EQ -> let
+        c' = p a' b'
+        in if c' == c then inner a' b' c r' s' else (x,c'):inner a' b' c' r' s'
+    inner a _ c [] ((y,b'):s') = let
+      c' = p a b'
+      in if c' == c then inner a b' c [] s' else (y,c'):inner a b' c' [] s'
+    inner _ b c ((x,a'):r') [] = let
+      c' = p a' b
+      in if c' == c then inner a' b c r' [] else (x,c'):inner a' b c' r' []
+    inner _ _ _ [] [] = []
+
+    run (Piecewise a f) (Piecewise b g) = let
+      c = p a b
+      l = inner a b c (M.toList f) (M.toList g)
+      in Piecewise c $ M.fromList l
+
+    in run
+
+  mergeA p = let
+
+    maybePrepend x u v l
+      | u == v    = l
+      | otherwise = (x,v):l
+
+    inner a b c r@((x,a'):r') s@((y,b'):s') = case compare x y of
+      LT -> let
+        c' = p a' b
+        in liftA3 (maybePrepend x) c c' $ inner a' b c' r' s
+      GT -> let
+        c' = p a b'
+        in liftA3 (maybePrepend y) c c' $ inner a b' c' r s'
+      EQ -> let
+        c' = p a' b'
+        in liftA3 (maybePrepend x) c c' $ inner a' b' c' r' s'
+    inner a _ c [] ((y,b'):s') = let
+      c' = p a b'
+      in liftA3 (maybePrepend y) c c' $ inner a b' c' [] s'
+    inner _ b c ((x,a'):r') [] = let
+      c' = p a' b
+      in liftA3 (maybePrepend x) c c' $ inner a' b c' r' []
+    inner _ _ _ [] [] = pure []
+
+    run (Piecewise a f) (Piecewise b g) = let
+      c = p a b
+      l = inner a b c (M.toList f) (M.toList g)
+      in liftA2 Piecewise c (M.fromList <$> l)
+
+    in run
+
+instance Neighbourly (Piecewise k) where
+  neighbours m = let
+    v = values m
+    in S.fromList $ zip v (tail v)
+
+
+{-
+-- May work with a future version of cond
+deriving via (AlgebraWrapper k (Piecewise k) b)
+  instance (Ord k, Ord b, Boolean b) => Boolean (Piecewise k b)
+-}
diff --git a/src/Data/Mapping/Util.hs b/src/Data/Mapping/Util.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Mapping/Util.hs
@@ -0,0 +1,25 @@
+module Data.Mapping.Util where
+
+import Data.Functor.Compose (Compose(..))
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as M
+
+
+-- | inserts key with value only if absent, returns map if changed
+insertIfAbsent :: Ord k => k -> v -> Map k v -> (v, Maybe (Map k v))
+insertIfAbsent k v = let
+  f (Just x) = (x, Nothing)
+  f Nothing  = (v, Just (Just v))
+  in getCompose . M.alterF (Compose . f) k
+
+
+-- | For use in maps where we don't want to store default values
+nonDefault :: Eq a => a -> a -> Maybe a
+nonDefault d x
+  | d == x    = Nothing
+  | otherwise = Just x
+
+
+-- | Helper function (not exported)
+equating :: Eq a => (b -> a) -> b -> b -> Bool
+equating f x y = f x == f y
diff --git a/test/Data/Mapping/DecisionSpec.hs b/test/Data/Mapping/DecisionSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Data/Mapping/DecisionSpec.hs
@@ -0,0 +1,113 @@
+module Data.Mapping.DecisionSpec where
+
+import Prelude hiding ((&&), (||), not, all)
+import qualified Data.Map as M
+import qualified Data.Set as S
+import Test.Hspec
+import Data.Algebra.Boolean ((&&), (||), not, all)
+import Data.Mapping
+import Data.Mapping.Decision
+import Data.Mapping.Piecewise
+
+
+boolAct ::    Ord a
+           => AlgebraWrapper (a -> Bool) (Decision Bool OnBool a) Bool
+           -> [a]
+           -> Bool
+boolAct (AlgebraWrapper a) s = act a (`S.member` S.fromList s)
+
+
+spec :: Spec
+spec = do
+
+  let x = test "x"
+  let y = test "y"
+
+  describe "Basic tests of act" $ do
+
+    it "x false on {}" $ do
+      boolAct x []    `shouldBe` False
+    it "x true on {x}" $ do
+      boolAct x ["x"] `shouldBe` True
+
+  describe "Basic tests of mmap" $ do
+
+    it "not x true on {}" $ do
+      boolAct (not x) []    `shouldBe` True
+    it "not x false on {x}" $ do
+      boolAct (not x) ["x"] `shouldBe` False
+
+  describe "Basic tests of merge" $ do
+
+    it "x && y true on {}" $ do
+      boolAct (x && y) []         `shouldBe` False
+    it "x && y true on {x}" $ do
+      boolAct (x && y) ["x"]      `shouldBe` False
+    it "x && y true on {y}" $ do
+      boolAct (x && y) ["y"]      `shouldBe` False
+    it "x && y true on {x,y}" $ do
+      boolAct (x && y) ["x", "y"] `shouldBe` True
+
+    it "x || y true on {}" $ do
+      boolAct (x || y) []         `shouldBe` False
+    it "x || y true on {x}" $ do
+      boolAct (x || y) ["x"]      `shouldBe` True
+    it "x || y true on {y}" $ do
+      boolAct (x || y) ["y"]      `shouldBe` True
+    it "x || y true on {x,y}" $ do
+      boolAct (x || y) ["x", "y"] `shouldBe` True
+
+    it "y && x true on {}" $ do
+      boolAct (y && x) []         `shouldBe` False
+    it "y && x true on {x}" $ do
+      boolAct (y && x) ["x"]      `shouldBe` False
+    it "y && x true on {y}" $ do
+      boolAct (y && x) ["y"]      `shouldBe` False
+    it "y && x true on {x,y}" $ do
+      boolAct (y && x) ["x", "y"] `shouldBe` True
+
+    it "y || x true on {}" $ do
+      boolAct (y || x) []         `shouldBe` False
+    it "y || x true on {x}" $ do
+      boolAct (y || x) ["x"]      `shouldBe` True
+    it "y || x true on {y}" $ do
+      boolAct (y || x) ["y"]      `shouldBe` True
+    it "y || x true on {x,y}" $ do
+      boolAct (y || x) ["x", "y"] `shouldBe` True
+
+  describe "Properties of independent sets in C_100" $ do
+
+    let l2 = (100,1):[(n,n+1) | n <- [1..99]]
+    let l3 = (99,100,1):(100,1,2):[(n,n+1,n+2) | n <- [1..98]]
+    let independent = all (\(i,j) -> not (test i && test j)) l2
+    let maximal = all (\(i,j,k) -> test i || test j || test k) l3
+    let AlgebraWrapper t = independent && maximal
+
+    -- Mentioned in Knuth
+    it "should have the right count" $ do
+      numberTrue (1::Int) 100 t `shouldBe` 1630580875002
+  
+  describe "Decision trees for monomial divisibility" $ do
+
+    let xy2 = M.fromList [("X", 1::Int), ("Y", 2)]
+    let x2y = M.fromList [("X", 2), ("Y", 1)]
+    let xyz = M.fromList [("X", 1), ("Y", 1), ("Z", 1)]
+    let monomials = M.fromList [(xy2, 1::Int), (x2y, 2), (xyz, 3)]
+    let f i b = if b then i else 0
+    let d = M.foldlWithKey' (\t m i -> merge max t (mmap (f i) . buildAll $ fmap atLeast m)) (cst 0) monomials
+    let mapAct m = act d (\a -> M.findWithDefault 0 a $ M.fromList m)
+
+    it "should get the right monomial for w^2y^4" $ do
+      mapAct [("W", 2), ("Y", 4)] `shouldBe` 0
+
+    it "should get the right monomial for w^3xy^2" $ do
+      mapAct [("W", 3), ("X", 1), ("Y", 2)] `shouldBe` 1
+
+    it "should get the right monomial for w^2x^2y^2" $ do
+      mapAct [("W", 2), ("X", 2), ("Y", 2)] `shouldBe` 2
+
+    it "should get the right monomial for w^2x^2y^2z^2" $ do
+      mapAct [("W", 2), ("X", 2), ("Y", 2), ("Z", 2)] `shouldBe` 3
+
+    it "should calculate neighbours correctly" $ do
+      neighbours d `shouldBe` S.fromList [(0,1),(0,2),(0,3),(1,2),(1,3),(2,3)]
diff --git a/test/Data/Mapping/MapWithDefaultSpec.hs b/test/Data/Mapping/MapWithDefaultSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Data/Mapping/MapWithDefaultSpec.hs
@@ -0,0 +1,17 @@
+module Data.Mapping.MapWithDefaultSpec where
+
+import Data.Mapping
+import Data.Mapping.MapWithDefault
+
+import Test.Hspec
+
+
+spec :: Spec
+spec = do
+
+  describe "MapWithDefault" $ do
+    let m = fromList (1 :: Int) [('a',1), ('b',2), ('c',3)]
+    let n = fromList (2 :: Int) [('b',1), ('c',1), ('d',3)]
+
+    it "merges correctly" $ do
+      merge (+) m n `shouldBe` fromList 3 [('c',4), ('d',4)]
diff --git a/test/Data/Mapping/PiecewiseSpec.hs b/test/Data/Mapping/PiecewiseSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Data/Mapping/PiecewiseSpec.hs
@@ -0,0 +1,23 @@
+module Data.Mapping.PiecewiseSpec where
+
+import Data.Mapping
+import Data.Mapping.Piecewise
+
+import Test.Hspec
+
+
+spec :: Spec
+spec = do
+
+  describe "Piecewise" $ do
+    let a = changeAt (0 :: Int) (3 :: Int) 1
+    let b = changeAt (0 :: Int) (6 :: Int) 1
+    let c = merge (+) a b
+    it "has right value at 0" $ do
+      act c 0 `shouldBe` 0
+    it "has right value at 3" $ do
+      act c 3 `shouldBe` 1
+    it "has right value at 6" $ do
+      act c 6 `shouldBe` 2
+    it "has right value at 9" $ do
+      act c 9 `shouldBe` 2
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,1 @@
+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}