copilot-theorem: Add explicit imports for Control.Monad. Refs #491.

The modules in Control.Monad.* in mtl >= 2.3 no longer re-export
Control.Monad, leading to a number of compilation errors in
copilot-theorem. Since mtl >= 2.3 is required for Copilot to work with
GHC 9.6 and above, this issue prevents Copilot from compiling with
current versions of GHC, including the one in hackage.

This commit updates copilot-theorem so that any imports from
Control.Monad are explicit and not via re-exports from other modules.

Author: ivanperez-keera

copilot-theorem/src/Copilot/Theorem/IL/Translate.hs

@@ -14,6 +14,7 @@ import qualified Copilot.Core as C
 
 import qualified Data.Map.Strict as Map
 
+import Control.Monad       (forM, liftM2, when)
 import Control.Monad.State
 
 import Data.Char

copilot-theorem/src/Copilot/Theorem/Prove.hs

@@ -22,6 +22,7 @@ import qualified Copilot.Core as Core
 
 import Data.List (intercalate)
 import Control.Applicative (liftA2)
+import Control.Monad        (ap, liftM)
 import Control.Monad.Writer
 
 -- | Output produced by a prover, containing the 'Status' of the proof and

copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs

@@ -47,6 +47,7 @@ import Copilot.Theorem.TransSys.Spec
 import Copilot.Theorem.TransSys.Cast
 import Copilot.Theorem.Misc.Utils
 
+import Control.Monad            (liftM, liftM2, unless)
 import Control.Monad.State.Lazy
 
 import Data.Char (isNumber)

copilot-theorem/src/Copilot/Theorem/What4.hs

@@ -57,6 +57,7 @@ import qualified What4.InterpretedFloatingPoint as WFP
 import qualified What4.Solver                   as WS
 import qualified What4.Solver.DReal             as WS
 
+import Control.Monad (forM)
 import Control.Monad.State
 import qualified Data.BitVector.Sized as BV
 import Data.Foldable (foldrM)