From dfe522a764ad6d6ca0f0d1010ed669d33f2a5c99 Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Mon, 4 Jan 2021 11:55:44 -0800
Subject: [PATCH] Actually, I think it makes more sense to just put SeqMap
 directly into the `Cryptol.Backend` module.

---
 cryptol.cabal                   |   1 -
 src/Cryptol/Backend.hs          | 148 ++++++++++++++++++++++++++++++--
 src/Cryptol/Backend/Concrete.hs |   1 -
 src/Cryptol/Backend/SeqMap.hs   | 140 ------------------------------
 src/Cryptol/Eval.hs             |   1 -
 src/Cryptol/Eval/Concrete.hs    |   1 -
 src/Cryptol/Eval/Generic.hs     |   1 -
 src/Cryptol/Eval/SBV.hs         |   1 -
 src/Cryptol/Eval/Value.hs       |   1 -
 src/Cryptol/Eval/What4.hs       |   1 -
 src/Cryptol/REPL/Command.hs     |   2 +-
 src/Cryptol/Symbolic.hs         |   1 -
 src/Cryptol/Testing/Random.hs   |   3 +-
 13 files changed, 141 insertions(+), 161 deletions(-)
 delete mode 100644 src/Cryptol/Backend/SeqMap.hs

diff --git a/cryptol.cabal b/cryptol.cabal
index 2605a11c1..a737c0d32 100644
--- a/cryptol.cabal
+++ b/cryptol.cabal
@@ -160,7 +160,6 @@ library
 
                        Cryptol.Backend,
                        Cryptol.Backend.Arch,
-                       Cryptol.Backend.SeqMap,
                        Cryptol.Backend.Concrete,
                        Cryptol.Backend.FloatHelpers,
                        Cryptol.Backend.Monad,
diff --git a/src/Cryptol/Backend.hs b/src/Cryptol/Backend.hs
index 052d1feed..586932b1f 100644
--- a/src/Cryptol/Backend.hs
+++ b/src/Cryptol/Backend.hs
@@ -7,7 +7,22 @@ module Cryptol.Backend
   , cryUserError
   , cryNoPrimError
   , FPArith2
-  , SeqMap(..)
+
+    -- * Sequence Maps
+  , SeqMap (..)
+  , lookupSeqMap
+  , finiteSeqMap
+  , infiniteSeqMap
+  , enumerateSeqMap
+  , streamSeqMap
+  , reverseSeqMap
+  , updateSeqMap
+  , dropSeqMap
+  , concatSeqMap
+  , splitSeqMap
+  , memoMap
+  , zipSeqMap
+  , mapSeqMap
 
     -- * Rationals
   , SRational(..)
@@ -31,14 +46,19 @@ module Cryptol.Backend
   ) where
 
 import Control.Monad.IO.Class
+import Data.IORef
 import Data.Kind (Type)
+import Data.List (genericIndex)
 import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
 
 import Cryptol.Backend.FloatHelpers (BF)
 import Cryptol.Backend.Monad
   ( EvalError(..), CallStack, pushCallFrame )
 import Cryptol.ModuleSystem.Name(Name)
 import Cryptol.Parser.Position
+import Cryptol.Utils.Panic(panic)
+
 
 invalidIndex :: Backend sym => sym -> Integer -> SEval sym a
 invalidIndex sym i = raiseError sym (InvalidIndex (Just i))
@@ -193,13 +213,6 @@ iteRational :: Backend sym => sym -> SBit sym -> SRational sym -> SRational sym
 iteRational sym p (SRational a b) (SRational c d) =
   SRational <$> iteInteger sym p a c <*> iteInteger sym p b d
 
--- | A sequence map represents a mapping from nonnegative integer indices
---   to values.  These are used to represent both finite and infinite sequences.
-data SeqMap sym a
-  = IndexSeqMap  !(Integer -> SEval sym a)
-  | UpdateSeqMap !(Map Integer (SEval sym a))
-                 !(Integer -> SEval sym a)
-
 -- | This type class defines a collection of operations on bits, words and integers that
 --   are necessary to define generic evaluator primitives that operate on both concrete
 --   and symbolic values uniformly.
@@ -277,7 +290,7 @@ class (MonadIO (SEval sym), Monad (SGen sym)) => Backend sym where
 
   sGenerateBit         :: sym -> SGen sym (SBit sym)
 
-  sUnboundedWord       :: sym -> Integer -> SGen sym (SWord sym)  
+  sUnboundedWord       :: sym -> Integer -> SGen sym (SWord sym)
   sBoundedWord         :: sym -> (SWord sym, SWord sym) -> SGen sym (SWord sym)
   sBoundedSignedWord   :: sym -> (SWord sym, SWord sym) -> SGen sym (SWord sym)
 
@@ -733,3 +746,120 @@ type FPArith2 sym =
   SFloat sym ->
   SFloat sym ->
   SEval sym (SFloat sym)
+
+
+
+
+-- | A sequence map represents a mapping from nonnegative integer indices
+--   to values.  These are used to represent both finite and infinite sequences.
+data SeqMap sym a
+  = IndexSeqMap  !(Integer -> SEval sym a)
+  | UpdateSeqMap !(Map Integer (SEval sym a))
+                 !(Integer -> SEval sym a)
+
+
+lookupSeqMap :: SeqMap sym a -> Integer -> SEval sym a
+lookupSeqMap (IndexSeqMap f) i = f i
+lookupSeqMap (UpdateSeqMap m f) i =
+  case Map.lookup i m of
+    Just x  -> x
+    Nothing -> f i
+
+-- | Generate a finite sequence map from a list of values
+finiteSeqMap :: [SEval sym a] -> SeqMap sym a
+finiteSeqMap xs =
+   UpdateSeqMap
+      (Map.fromList (zip [0..] xs))
+      (\i -> panic "finiteSeqMap" ["Out of bounds access of finite seq map", "length: " ++ show (length xs), show i])
+
+-- | Generate an infinite sequence map from a stream of values
+infiniteSeqMap :: Backend sym => sym -> [SEval sym a] -> SEval sym (SeqMap sym a)
+infiniteSeqMap sym xs =
+   -- TODO: use an int-trie?
+   memoMap sym (IndexSeqMap $ \i -> genericIndex xs i)
+
+-- | Create a finite list of length @n@ of the values from @[0..n-1]@ in
+--   the given the sequence emap.
+enumerateSeqMap :: (Integral n) => n -> SeqMap sym a -> [SEval sym a]
+enumerateSeqMap n m = [ lookupSeqMap m  i | i <- [0 .. (toInteger n)-1] ]
+
+-- | Create an infinite stream of all the values in a sequence map
+streamSeqMap :: SeqMap sym a -> [SEval sym a]
+streamSeqMap m = [ lookupSeqMap m i | i <- [0..] ]
+
+-- | Reverse the order of a finite sequence map
+reverseSeqMap :: Integer     -- ^ Size of the sequence map
+              -> SeqMap sym a
+              -> SeqMap sym a
+reverseSeqMap n vals = IndexSeqMap $ \i -> lookupSeqMap vals (n - 1 - i)
+
+updateSeqMap :: SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
+updateSeqMap (UpdateSeqMap m sm) i x = UpdateSeqMap (Map.insert i x m) sm
+updateSeqMap (IndexSeqMap f) i x = UpdateSeqMap (Map.singleton i x) f
+
+-- | Concatenate the first @n@ values of the first sequence map onto the
+--   beginning of the second sequence map.
+concatSeqMap :: Integer -> SeqMap sym  a -> SeqMap sym a -> SeqMap sym a
+concatSeqMap n x y =
+    IndexSeqMap $ \i ->
+       if i < n
+         then lookupSeqMap x i
+         else lookupSeqMap y (i-n)
+
+-- | Given a number @n@ and a sequence map, return two new sequence maps:
+--   the first containing the values from @[0..n-1]@ and the next containing
+--   the values from @n@ onward.
+splitSeqMap :: Integer -> SeqMap sym a -> (SeqMap sym a, SeqMap sym a)
+splitSeqMap n xs = (hd,tl)
+  where
+  hd = xs
+  tl = IndexSeqMap $ \i -> lookupSeqMap xs (i+n)
+
+-- | Drop the first @n@ elements of the given 'SeqMap'.
+dropSeqMap :: Integer -> SeqMap sym a -> SeqMap sym a
+dropSeqMap 0 xs = xs
+dropSeqMap n xs = IndexSeqMap $ \i -> lookupSeqMap xs (i+n)
+
+-- | Given a sequence map, return a new sequence map that is memoized using
+--   a finite map memo table.
+memoMap :: Backend sym => sym -> SeqMap sym a -> SEval sym (SeqMap sym a)
+memoMap sym x = do
+  stk <- sGetCallStack sym
+  cache <- liftIO $ newIORef $ Map.empty
+  return $ IndexSeqMap (memo cache stk)
+
+  where
+  memo cache stk i = do
+    mz <- liftIO (Map.lookup i <$> readIORef cache)
+    case mz of
+      Just z  -> return z
+      Nothing -> sWithCallStack sym stk (doEval cache i)
+
+  doEval cache i = do
+    v <- lookupSeqMap x i
+    liftIO $ atomicModifyIORef' cache (\m -> (Map.insert i v m, ()))
+    return v
+
+-- | Apply the given evaluation function pointwise to the two given
+--   sequence maps.
+zipSeqMap ::
+  Backend sym =>
+  sym ->
+  (a -> a -> SEval sym a) ->
+  SeqMap sym a ->
+  SeqMap sym a ->
+  SEval sym (SeqMap sym a)
+zipSeqMap sym f x y =
+  memoMap sym (IndexSeqMap $ \i ->
+    do xi <- lookupSeqMap x i
+       yi <- lookupSeqMap y i
+       f xi yi)
+
+-- | Apply the given function to each value in the given sequence map
+mapSeqMap ::
+  Backend sym =>
+  sym ->
+  (a -> SEval sym a) ->
+  SeqMap sym a -> SEval sym (SeqMap sym a)
+mapSeqMap sym f x =
+  memoMap sym (IndexSeqMap $ \i -> f =<< lookupSeqMap x i)
diff --git a/src/Cryptol/Backend/Concrete.hs b/src/Cryptol/Backend/Concrete.hs
index af1d60596..03ae7718e 100644
--- a/src/Cryptol/Backend/Concrete.hs
+++ b/src/Cryptol/Backend/Concrete.hs
@@ -51,7 +51,6 @@ import qualified Cryptol.Backend.Arch as Arch
 import qualified Cryptol.Backend.FloatHelpers as FP
 import Cryptol.Backend
 import Cryptol.Backend.Monad
-import Cryptol.Backend.SeqMap
 import Cryptol.TypeCheck.Solver.InfNat (genLog)
 import Cryptol.Utils.Panic (panic)
 import Cryptol.Utils.PP
diff --git a/src/Cryptol/Backend/SeqMap.hs b/src/Cryptol/Backend/SeqMap.hs
deleted file mode 100644
index 69e356a9b..000000000
--- a/src/Cryptol/Backend/SeqMap.hs
+++ /dev/null
@@ -1,140 +0,0 @@
--- |
--- Module      :  Cryptol.Eval.SeqMap
--- Copyright   :  (c) 2020 Galois, Inc.
--- License     :  BSD3
--- Maintainer  :  cryptol@galois.com
--- Stability   :  provisional
--- Portability :  portable
---
-
-module Cryptol.Backend.SeqMap
-  ( SeqMap (..)
-  , lookupSeqMap
-  , finiteSeqMap
-  , infiniteSeqMap
-  , enumerateSeqMap
-  , streamSeqMap
-  , reverseSeqMap
-  , updateSeqMap
-  , dropSeqMap
-  , concatSeqMap
-  , splitSeqMap
-  , memoMap
-  , zipSeqMap
-  , mapSeqMap
-  ) where
-
-import Control.Monad.IO.Class
-import Data.IORef
-import Data.List (genericIndex)
-import qualified Data.Map.Strict as Map
-
-import Cryptol.Backend
-import Cryptol.Utils.Panic(panic)
-
-
-lookupSeqMap :: SeqMap sym a -> Integer -> SEval sym a
-lookupSeqMap (IndexSeqMap f) i = f i
-lookupSeqMap (UpdateSeqMap m f) i =
-  case Map.lookup i m of
-    Just x  -> x
-    Nothing -> f i
-
--- | Generate a finite sequence map from a list of values
-finiteSeqMap :: [SEval sym a] -> SeqMap sym a
-finiteSeqMap xs =
-   UpdateSeqMap
-      (Map.fromList (zip [0..] xs))
-      (\i -> panic "finiteSeqMap" ["Out of bounds access of finite seq map", "length: " ++ show (length xs), show i])
-
--- | Generate an infinite sequence map from a stream of values
-infiniteSeqMap :: Backend sym => sym -> [SEval sym a] -> SEval sym (SeqMap sym a)
-infiniteSeqMap sym xs =
-   -- TODO: use an int-trie?
-   memoMap sym (IndexSeqMap $ \i -> genericIndex xs i)
-
--- | Create a finite list of length @n@ of the values from @[0..n-1]@ in
---   the given the sequence emap.
-enumerateSeqMap :: (Integral n) => n -> SeqMap sym a -> [SEval sym a]
-enumerateSeqMap n m = [ lookupSeqMap m  i | i <- [0 .. (toInteger n)-1] ]
-
--- | Create an infinite stream of all the values in a sequence map
-streamSeqMap :: SeqMap sym a -> [SEval sym a]
-streamSeqMap m = [ lookupSeqMap m i | i <- [0..] ]
-
--- | Reverse the order of a finite sequence map
-reverseSeqMap :: Integer     -- ^ Size of the sequence map
-              -> SeqMap sym a
-              -> SeqMap sym a
-reverseSeqMap n vals = IndexSeqMap $ \i -> lookupSeqMap vals (n - 1 - i)
-
-updateSeqMap :: SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
-updateSeqMap (UpdateSeqMap m sm) i x = UpdateSeqMap (Map.insert i x m) sm
-updateSeqMap (IndexSeqMap f) i x = UpdateSeqMap (Map.singleton i x) f
-
--- | Concatenate the first @n@ values of the first sequence map onto the
---   beginning of the second sequence map.
-concatSeqMap :: Integer -> SeqMap sym  a -> SeqMap sym a -> SeqMap sym a
-concatSeqMap n x y =
-    IndexSeqMap $ \i ->
-       if i < n
-         then lookupSeqMap x i
-         else lookupSeqMap y (i-n)
-
--- | Given a number @n@ and a sequence map, return two new sequence maps:
---   the first containing the values from @[0..n-1]@ and the next containing
---   the values from @n@ onward.
-splitSeqMap :: Integer -> SeqMap sym a -> (SeqMap sym a, SeqMap sym a)
-splitSeqMap n xs = (hd,tl)
-  where
-  hd = xs
-  tl = IndexSeqMap $ \i -> lookupSeqMap xs (i+n)
-
--- | Drop the first @n@ elements of the given 'SeqMap'.
-dropSeqMap :: Integer -> SeqMap sym a -> SeqMap sym a
-dropSeqMap 0 xs = xs
-dropSeqMap n xs = IndexSeqMap $ \i -> lookupSeqMap xs (i+n)
-
--- | Given a sequence map, return a new sequence map that is memoized using
---   a finite map memo table.
-memoMap :: Backend sym => sym -> SeqMap sym a -> SEval sym (SeqMap sym a)
-memoMap sym x = do
-  stk <- sGetCallStack sym
-  cache <- liftIO $ newIORef $ Map.empty
-  return $ IndexSeqMap (memo cache stk)
-
-  where
-  memo cache stk i = do
-    mz <- liftIO (Map.lookup i <$> readIORef cache)
-    case mz of
-      Just z  -> return z
-      Nothing -> sWithCallStack sym stk (doEval cache i)
-
-  doEval cache i = do
-    v <- lookupSeqMap x i
-    liftIO $ atomicModifyIORef' cache (\m -> (Map.insert i v m, ()))
-    return v
-
--- | Apply the given evaluation function pointwise to the two given
---   sequence maps.
-zipSeqMap ::
-  Backend sym =>
-  sym ->
-  (a -> a -> SEval sym a) ->
-  SeqMap sym a ->
-  SeqMap sym a ->
-  SEval sym (SeqMap sym a)
-zipSeqMap sym f x y =
-  memoMap sym (IndexSeqMap $ \i ->
-    do xi <- lookupSeqMap x i
-       yi <- lookupSeqMap y i
-       f xi yi)
-
--- | Apply the given function to each value in the given sequence map
-mapSeqMap ::
-  Backend sym =>
-  sym ->
-  (a -> SEval sym a) ->
-  SeqMap sym a -> SEval sym (SeqMap sym a)
-mapSeqMap sym f x =
-  memoMap sym (IndexSeqMap $ \i -> f =<< lookupSeqMap x i)
diff --git a/src/Cryptol/Eval.hs b/src/Cryptol/Eval.hs
index 343fd5879..e9ad2a223 100644
--- a/src/Cryptol/Eval.hs
+++ b/src/Cryptol/Eval.hs
@@ -40,7 +40,6 @@ module Cryptol.Eval (
 import Cryptol.Backend
 import Cryptol.Backend.Concrete( Concrete(..) )
 import Cryptol.Backend.Monad
-import Cryptol.Backend.SeqMap
 import Cryptol.Eval.Generic ( iteValue )
 import Cryptol.Eval.Env
 import Cryptol.Eval.Prims
diff --git a/src/Cryptol/Eval/Concrete.hs b/src/Cryptol/Eval/Concrete.hs
index 4dadd2f13..20093f72c 100644
--- a/src/Cryptol/Eval/Concrete.hs
+++ b/src/Cryptol/Eval/Concrete.hs
@@ -42,7 +42,6 @@ import Cryptol.Backend
 import Cryptol.Backend.Concrete
 import Cryptol.Backend.FloatHelpers
 import Cryptol.Backend.Monad
-import Cryptol.Backend.SeqMap
 
 import Cryptol.Eval.Generic hiding (logicShift)
 import Cryptol.Eval.Prims
diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs
index 5d51b92fd..849a58095 100644
--- a/src/Cryptol/Eval/Generic.hs
+++ b/src/Cryptol/Eval/Generic.hs
@@ -39,7 +39,6 @@ import Cryptol.Backend
 import Cryptol.Backend.Concrete (Concrete(..))
 import Cryptol.Backend.Monad( Eval, evalPanic, EvalError(..), Unsupported(..) )
 import Cryptol.Testing.Random( randomValue )
-import Cryptol.Backend.SeqMap
 
 import Cryptol.Eval.Prims
 import Cryptol.Eval.Type
diff --git a/src/Cryptol/Eval/SBV.hs b/src/Cryptol/Eval/SBV.hs
index 819ce41ba..1fd6afa71 100644
--- a/src/Cryptol/Eval/SBV.hs
+++ b/src/Cryptol/Eval/SBV.hs
@@ -32,7 +32,6 @@ import Data.SBV.Dynamic as SBV
 import Cryptol.Backend
 import Cryptol.Backend.Monad ( EvalError(..), Unsupported(..) )
 import Cryptol.Backend.SBV
-import Cryptol.Backend.SeqMap
 
 import Cryptol.Eval.Type (TValue(..))
 import Cryptol.Eval.Generic
diff --git a/src/Cryptol/Eval/Value.hs b/src/Cryptol/Eval/Value.hs
index e3c5f4521..828a30fce 100644
--- a/src/Cryptol/Eval/Value.hs
+++ b/src/Cryptol/Eval/Value.hs
@@ -82,7 +82,6 @@ import Data.Ratio
 import Numeric (showIntAtBase)
 
 import Cryptol.Backend
-import Cryptol.Backend.SeqMap
 import qualified Cryptol.Backend.Arch as Arch
 import Cryptol.Backend.Monad
   ( evalPanic, wordTooWide, CallStack, combineCallStacks )
diff --git a/src/Cryptol/Eval/What4.hs b/src/Cryptol/Eval/What4.hs
index 3323700e5..797102798 100644
--- a/src/Cryptol/Eval/What4.hs
+++ b/src/Cryptol/Eval/What4.hs
@@ -42,7 +42,6 @@ import qualified What4.Utils.AbstractDomains as W4
 
 import Cryptol.Backend
 import Cryptol.Backend.Monad ( EvalError(..), Unsupported(..) )
-import Cryptol.Backend.SeqMap
 import Cryptol.Backend.What4
 import qualified Cryptol.Backend.What4.SFloat as W4
 
diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
index 0a7f2372a..445827802 100644
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@@ -63,8 +63,8 @@ import qualified Cryptol.ModuleSystem.Renamer as M (RenamerWarning(SymbolShadowe
 import qualified Cryptol.Utils.Ident as M
 import qualified Cryptol.ModuleSystem.Env as M
 
+import qualified Cryptol.Backend as E
 import qualified Cryptol.Backend.Monad as E
-import qualified Cryptol.Backend.SeqMap as E
 import           Cryptol.Eval.Concrete( Concrete(..) )
 import qualified Cryptol.Eval.Concrete as Concrete
 import qualified Cryptol.Eval.Env as E
diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs
index 1c2687940..0b7973724 100644
--- a/src/Cryptol/Symbolic.hs
+++ b/src/Cryptol/Symbolic.hs
@@ -50,7 +50,6 @@ import qualified LibBF as FP
 
 import           Cryptol.Backend
 import           Cryptol.Backend.FloatHelpers(bfValue)
-import           Cryptol.Backend.SeqMap
 
 import qualified Cryptol.Eval.Concrete as Concrete
 import           Cryptol.Eval.Value
diff --git a/src/Cryptol/Testing/Random.hs b/src/Cryptol/Testing/Random.hs
index 59b1ee3f9..3e063bdd3 100644
--- a/src/Cryptol/Testing/Random.hs
+++ b/src/Cryptol/Testing/Random.hs
@@ -39,10 +39,9 @@ import qualified Data.Sequence as Seq
 import System.Random          (split, random, randomR)
 import System.Random.TF.Gen   (TFGen) 
 
-import Cryptol.Backend        (Backend(..), SRational(..))
+import Cryptol.Backend        (Backend(..), SRational(..), SeqMap(..), finiteSeqMap)
 import Cryptol.Backend.Monad  (runEval,Eval,EvalErrorEx(..))
 import Cryptol.Backend.Concrete
-import Cryptol.Backend.SeqMap
 
 import Cryptol.Eval.Type      (TValue(..))
 import Cryptol.Eval.Value     (GenValue(..), WordValue(..),