Update for GHC 8.10.7 and more modern libraries

Language/Boogie/Environment.hs

@@ -161,7 +161,7 @@ data Memory = Memory {
 makeLenses ''Memory
 
 -- | Lens that selects a store from memory
-type StoreLens = Simple Lens Memory Store
+type StoreLens = Lens' Memory Store
 
 -- | Empty memory
 emptyMemory = Memory {
@@ -357,7 +357,7 @@ lookupMapConstraints = lookupGetter (envConstraints.conMaps) []
 
 -- Environment modifications
 addProcedureImpl name def env = over envProcedures (M.insert name (lookupProcedure name env ++ [def])) env
-addNameConstraint :: Id -> Simple Lens (Environment m) NameConstraints -> Expression -> Environment m -> Environment m
+addNameConstraint :: Id -> Lens' (Environment m) NameConstraints -> Expression -> Environment m -> Environment m
 addNameConstraint name lens c env = over lens (M.insert name (nub $ c : lookupGetter lens [] name env)) env
 addUniqueConst t name env = over (envConstraints.conUnique) (M.insert t (name : lookupUnique t env)) env
 addMapConstraint r c env = over (envConstraints.conMaps) (M.insert r (nub $ c : lookupMapConstraints r env)) env

Language/Boogie/Interpreter.hs

@@ -61,7 +61,7 @@ import Debug.Trace
 -- Execute program @p@ in type context @tc@ with solver @solver@ and non-deterministic value generator @generator@, starting from procedure @entryPoint@;
 -- concretize passing executions iff @solvePassing@;
 -- return the outcome(s) embedded into the solver's monad.
-executeProgram :: (Monad m, Functor m) => Program -> Context -> Solver m -> Maybe Int -> Maybe Int -> Bool -> Bool -> Generator m -> Id -> m (TestCase)
+executeProgram :: (MonadFail m, Functor m) => Program -> Context -> Solver m -> Maybe Int -> Maybe Int -> Bool -> Bool -> Generator m -> Id -> m (TestCase)
 executeProgram p tc solver recMax loopMax concretize_ solvePassing generator entryPoint = result <$> runStateT (runErrorT programExecution) (initEnv tc solver generator recMax loopMax concretize_)
   where
     programExecution = do
@@ -878,7 +878,7 @@ checkPostonditions sig def exitPoint = mapM_ (exec . attachPos exitPoint . Predi
 {- Evaluating constraints -}
 
 -- | 'extendNameConstraints' @lens c@ : add @c@ as a constraint for all free variables in @c@ to @envConstraints.lens@
-extendNameConstraints :: (MonadState (Environment m) s, Finalizer s) => Simple Lens ConstraintMemory NameConstraints -> Expression -> s ()
+extendNameConstraints :: (MonadState (Environment m) s, Finalizer s) => Lens' ConstraintMemory NameConstraints -> Expression -> s ()
 extendNameConstraints lens c = mapM_ (\name -> modify $ addNameConstraint name (envConstraints.lens) c) (freeVars c)
 
 -- | 'extendMapConstraints' @r c@ : add @c@ to the constraints of the map @r@
@@ -1179,7 +1179,7 @@ generate f = do
 {- Preprocessing -}
 
 -- | Collect procedure implementations, and constant/function/global variable constraints
-preprocess :: (Monad m, Functor m) => Program -> SafeExecution m ()
+preprocess :: (MonadFail m, Functor m) => Program -> SafeExecution m ()
 preprocess (Program decls) = do
   mapM_ processDecl decls
   fs <- use envFunctions

Language/Boogie/TypeChecker.hs

@@ -47,7 +47,7 @@ import qualified Data.Map as M
 import Control.Monad.Trans.Error
 import Control.Applicative hiding (empty)
 import Control.Monad.State
-import Control.Lens hiding (Context)
+import Control.Lens hiding (Context, locally)
 
 {- Interface -}
 
@@ -863,4 +863,4 @@ checkLefts vars n = if length vars /= n
           if not (null invalidGlobals)
             then throwTypeError (text "Assignment to a global variable that is not in the enclosing procedure's modifies clause:" <+> commaSep (map text invalidGlobals))
             else return ()
-
+            

Language/Boogie/Z3/Solver.hs

@@ -182,7 +182,7 @@ newConstraint soln = enot (conjunction (logicEqs ++ customEqs))
             neqFold expr = interPair neqOp expr
 
       -- Equality relation on customs.
-      customEqRel = Map.foldWithKey go Map.empty soln
+      customEqRel = Map.foldrWithKey go Map.empty soln
           where
             go ref expr m =
                 case valueType expr of