Hack in enough NFData instances to see if that helps any with

memory usage/retainment.

cryptol-saw-core/cryptol-saw-core.cabal

@@ -27,6 +27,7 @@ library
     containers,
     cryptol >= 2.3.0,
     data-inttrie >= 0.1.4,
+    deepseq,
     integer-gmp,
     modern-uri,
     mtl,

cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs

@@ -6,12 +6,15 @@ Maintainer  : huffman
 Stability   : provisional
 -}
 {-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE DeriveGeneric #-}
 module Verifier.SAW.TypedTerm where
 
+import Control.DeepSeq
 import Control.Monad (foldM)
 import Data.Map (Map)
 import qualified Data.Map as Map
 import Data.Text (Text)
+import GHC.Generics
 
 import Cryptol.ModuleSystem.Name (nameIdent)
 import qualified Cryptol.TypeCheck.AST as C
@@ -36,16 +39,18 @@ data TypedTerm =
   { ttType :: TypedTermType
   , ttTerm :: Term
   }
-  deriving Show
-
+  deriving  (Show, Generic)
+instance NFData TypedTerm
 
 -- | The different notion of Cryptol types that
 --   as SAWCore term might have.
 data TypedTermType
   = TypedTermSchema C.Schema
   | TypedTermKind   C.Kind
   | TypedTermOther  Term
- deriving Show
+ deriving (Show, Generic)
+
+instance NFData TypedTermType
 
 
 ttTermLens :: Functor f => (Term -> f Term) -> TypedTerm -> f TypedTerm
@@ -149,7 +154,9 @@ data TypedExtCns =
   { tecType :: C.Type
   , tecExt :: ExtCns Term
   }
-  deriving Show
+  deriving (Show, Generic)
+
+instance NFData TypedExtCns
 
 -- | Recognize 'TypedTerm's that are external constants.
 asTypedExtCns :: TypedTerm -> Maybe TypedExtCns

saw-core/saw-core.cabal

@@ -30,6 +30,7 @@ library
     containers,
     data-inttrie,
     data-ref,
+    deepseq,
     directory,
     filepath,
     hashable >= 1.3.4,

saw-core/src/Verifier/SAW/Name.hs

@@ -51,6 +51,7 @@ module Verifier.SAW.Name
   , bestAlias
   ) where
 
+import           Control.DeepSeq
 import           Control.Exception (assert)
 import           Data.Char
 import           Data.Hashable
@@ -79,6 +80,8 @@ newtype ModuleName = ModuleName Text
 
 instance Hashable ModuleName -- automatically derived
 
+instance NFData ModuleName
+
 instance Show ModuleName where
   show (ModuleName s) = Text.unpack s
 
@@ -110,6 +113,7 @@ data Ident =
   deriving (Eq, Ord, Generic)
 
 instance Hashable Ident -- automatically derived
+instance NFData Ident
 
 instance Show Ident where
   show (Ident m s) = shows m ('.' : Text.unpack s)
@@ -177,7 +181,9 @@ data NameInfo
       [Text]   -- ^ A collection of aliases for this name.  Sorter or "less-qualified"
                --   aliases should be nearer the front of the list
 
- deriving (Eq,Ord,Show)
+ deriving (Eq,Ord,Show,Generic)
+
+instance NFData NameInfo
 
 nameURI :: NameInfo -> URI
 nameURI =
@@ -225,7 +231,7 @@ data ExtCns e =
   , ecName :: !NameInfo
   , ecType :: !e
   }
-  deriving (Show, Functor, Foldable, Traversable)
+  deriving (Show, Functor, Foldable, Traversable, Generic)
 
 instance Eq (ExtCns e) where
   x == y = ecVarIndex x == ecVarIndex y
@@ -236,6 +242,7 @@ instance Ord (ExtCns e) where
 instance Hashable (ExtCns e) where
   hashWithSalt x ec = hashWithSalt x (ecVarIndex ec)
 
+instance NFData e => NFData (ExtCns e)
 
 -- Primitive Names ------------------------------------------------------------
 
@@ -246,7 +253,9 @@ data PrimName e =
   , primName     :: !Ident
   , primType     :: e
   }
-  deriving (Show, Functor, Foldable, Traversable)
+  deriving (Show, Functor, Foldable, Traversable, Generic)
+
+instance NFData e => NFData (PrimName e)
 
 instance Eq (PrimName e) where
   x == y = primVarIndex x == primVarIndex y

saw-core/src/Verifier/SAW/Rewriter.hs

@@ -2,6 +2,7 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE NamedFieldPuns #-}
@@ -61,6 +62,7 @@ module Verifier.SAW.Rewriter
 import Control.Applicative ((<$>), pure, (<*>))
 import Data.Foldable (Foldable)
 #endif
+import Control.DeepSeq
 import Control.Monad.Identity
 import Control.Monad.State
 import Control.Monad.Trans.Maybe
@@ -73,7 +75,7 @@ import Data.Set (Set)
 import qualified Data.Set as Set
 import Control.Monad.Trans.Writer.Strict
 import Numeric.Natural
-
+import GHC.Generics
 
 import Verifier.SAW.Cache
 import Verifier.SAW.Conversion
@@ -86,7 +88,7 @@ import Verifier.SAW.Prelude.Constants
 
 data RewriteRule a
   = RewriteRule { ctxt :: [Term], lhs :: Term, rhs :: Term, permutative :: Bool, annotation :: Maybe a }
-  deriving (Show)
+  deriving (Show, Generic)
 -- ^ Invariant: The set of loose variables in @lhs@ must be exactly
 -- @[0 .. length ctxt - 1]@. The @rhs@ may contain a subset of these.
 
@@ -95,6 +97,8 @@ instance Eq (RewriteRule a) where
   RewriteRule c1 l1 r1 p1 _a1 == RewriteRule c2 l2 r2 p2 _a2 =
     c1 == c2 && l1 == l2 && r1 == r2 && p1 == p2
 
+instance NFData a => NFData (RewriteRule a)
+
 ctxtRewriteRule :: RewriteRule a -> [Term]
 ctxtRewriteRule = ctxt
 

saw-core/src/Verifier/SAW/Term/Functor.hs

@@ -66,6 +66,7 @@ import Data.Bits
 #if !MIN_VERSION_base(4,8,0)
 import Data.Foldable (Foldable)
 #endif
+import Control.DeepSeq
 import qualified Data.Foldable as Foldable (and, foldl')
 import Data.Hashable
 import Data.Map (Map)
@@ -101,6 +102,7 @@ data Sort
   = TypeSort Natural
   | PropSort
   deriving (Eq, Generic, TH.Lift)
+instance NFData Sort
 
 -- Prop is the lowest sort
 instance Ord Sort where
@@ -216,6 +218,7 @@ data FlatTermF e
   deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Generic)
 
 instance Hashable e => Hashable (FlatTermF e) -- automatically derived
+instance NFData e => NFData (FlatTermF e)
 
 -- Capture more type information here so we can
 --  use it during evaluation time to remember the
@@ -232,6 +235,7 @@ data CompiledRecursor e =
  deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Generic)
 
 instance Hashable e => Hashable (CompiledRecursor e) -- automatically derived
+instance NFData e => NFData (CompiledRecursor e)
 
 -- | Test if the association list used in a 'RecordType' or 'RecordValue' uses
 -- precisely the given field names and no more. If so, return the values
@@ -347,7 +351,7 @@ data TermF e
   deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Generic)
 
 instance Hashable e => Hashable (TermF e) -- automatically derived.
-
+instance NFData e => NFData (TermF e)
 
 -- Term Datatype ---------------------------------------------------------------
 
@@ -360,12 +364,14 @@ data Term
      , stAppTermF    :: !(TermF Term)
      }
   | Unshared !(TermF Term)
-  deriving (Show, Typeable)
+  deriving (Show, Typeable, Generic)
 
 instance Hashable Term where
   hashWithSalt salt STApp{ stAppIndex = i } = salt `combine` 0x00000000 `hashWithSalt` hash i
   hashWithSalt salt (Unshared t) = salt `combine` 0x55555555 `hashWithSalt` hash t
 
+instance NFData Term
+
 
 -- | Combine two given hash values.  'combine' has zero as a left
 -- identity. (FNV hash, copied from Data.Hashable 1.2.1.0.)
@@ -431,6 +437,9 @@ unwrapTermF (Unshared tf) = tf
 -- Bit n is a 1 iff n is in the set.
 newtype BitSet = BitSet Integer deriving (Eq, Ord, Show)
 
+instance NFData BitSet where
+  rnf (BitSet x) = rnf x
+
 -- | The empty 'BitSet'
 emptyBitSet :: BitSet
 emptyBitSet = BitSet 0

saw-core/src/Verifier/SAW/TermNet.hs

@@ -29,6 +29,7 @@ module Verifier.SAW.TermNet
   , content      -- :: Net a -> [a]
   ) where
 
+import Control.DeepSeq
 import Data.Map (Map)
 import qualified Data.Map as Map
 import Data.Maybe (fromMaybe)
@@ -117,6 +118,11 @@ data Net a
   | Net { comb :: Net a, var :: Net a, atoms :: Map Text (Net a) }
   deriving Show
 
+-- NB, this doesn't actually force the annotations
+instance NFData (Net a) where
+  rnf (Leaf ls) = foldr seq () ls
+  rnf (Net a b c) = rnf (a,b,c)
+
 {-
 Invariant: A well-formed term net should satisfy @valid 1@.
 Every sub-net should satisfy @valid n@ for some non-negative @n@.