Add support for microlens

CHANGELOG.md

@@ -14,9 +14,13 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Improved the partial evaluation for bit vectors. ([#176](https://github.com/lsrcz/grisette/pull/176))
 - Added `symRotateNegated` and `symShiftNegated`. ([#181](https://github.com/lsrcz/grisette/pull/181))
 - Added `mrg` and `sym` variants for all reasonable operations from
-  `Control.Monad`, `Control.Applicative`, `Data.Foldable`, `Data.List`, and `Data.Traversable`.
-  ([#182](https://github.com/lsrcz/grisette/pull/182))
+  `Control.Monad`, `Control.Applicative`, `Data.Foldable`, `Data.List`, `Data.Traversable`,
+  and `Data.Function`.
+  ([#182](https://github.com/lsrcz/grisette/pull/182),
+  [#186](https://github.com/lsrcz/grisette/pull/186))
 - Added `mrgIfPropagatedStrategy`. ([#184](https://github.com/lsrcz/grisette/pull/184))
+- Added instances for `Const`. ([#186](https://github.com/lsrcz/grisette/pull/186))
+- Added support for [microlens](https://hackage.haskell.org/package/microlens). ([#186](https://github.com/lsrcz/grisette/pull/186))
 - Added `freshString`. ([#188](https://github.com/lsrcz/grisette/pull/188))
 
 ### Fixed

flake.nix

@@ -8,14 +8,14 @@
       let
         pkgs = nixpkgs.legacyPackages.${system};
 
-        hPkgs = pkgs.haskell.packages."ghc982";
+        hPkgs = pkgs.haskell.packages."ghc964";
 
         myDevTools = [
           hPkgs.ghc # GHC compiler in the desired version (will be available on PATH)
           # hPkgs.ghcid # Continuous terminal Haskell compile checker
           # hPkgs.ormolu # Haskell formatter
-          # hPkgs.hlint # Haskell codestyle checker
-          # hPkgs.haskell-language-server # LSP server for editor
+          hPkgs.hlint # Haskell codestyle checker
+          hPkgs.haskell-language-server # LSP server for editor
           hPkgs.cabal-install
           stack-wrapped
           # (pkgs.ihaskell.override {

grisette.cabal

@@ -135,12 +135,15 @@ library
       Grisette.Lib.Data.Bool
       Grisette.Lib.Data.Either
       Grisette.Lib.Data.Foldable
+      Grisette.Lib.Data.Function
       Grisette.Lib.Data.Functor
+      Grisette.Lib.Data.Functor.Const
       Grisette.Lib.Data.Functor.Sum
       Grisette.Lib.Data.List
       Grisette.Lib.Data.Maybe
       Grisette.Lib.Data.Traversable
       Grisette.Lib.Data.Tuple
+      Grisette.Lib.Lens.Micro
       Grisette.Qualified.ParallelUnionDo
       Grisette.Utils
       Grisette.Utils.Parameterized
@@ -161,6 +164,8 @@ library
     , hashtables >=1.2.3.4 && <1.4
     , intern >=0.9.2 && <0.10
     , loch-th >=0.2.2 && <0.3
+    , microlens
+    , microlens-th
     , mtl >=2.2.2 && <2.4
     , parallel >=3.2.2.0 && <3.3
     , prettyprinter >=1.5.0 && <1.8
@@ -200,6 +205,8 @@ test-suite doctest
     , hashtables >=1.2.3.4 && <1.4
     , intern >=0.9.2 && <0.10
     , loch-th >=0.2.2 && <0.3
+    , microlens
+    , microlens-th
     , mtl >=2.2.2 && <2.4
     , parallel >=3.2.2.0 && <3.3
     , prettyprinter >=1.5.0 && <1.8
@@ -269,9 +276,11 @@ test-suite spec
       Grisette.Lib.Control.Monad.Trans.State.StrictTests
       Grisette.Lib.Control.MonadTests
       Grisette.Lib.Data.FoldableTests
+      Grisette.Lib.Data.FunctionTests
       Grisette.Lib.Data.FunctorTests
       Grisette.Lib.Data.ListTests
       Grisette.Lib.Data.TraversableTests
+      Grisette.Lib.Lens.MicroTests
       Grisette.TestUtil.NoMerge
       Grisette.TestUtil.PrettyPrint
       Grisette.TestUtil.SymbolicAssertion
@@ -293,6 +302,8 @@ test-suite spec
     , hashtables >=1.2.3.4 && <1.4
     , intern >=0.9.2 && <0.10
     , loch-th >=0.2.2 && <0.3
+    , microlens
+    , microlens-th
     , mtl >=2.2.2 && <2.4
     , parallel >=3.2.2.0 && <3.3
     , prettyprinter >=1.5.0 && <1.8

package.yaml

@@ -50,6 +50,8 @@ dependencies:
   - prettyprinter >= 1.5.0 && < 1.8
   - async >= 2.2.2 && < 2.3
   - stm >= 2.5 && < 2.6
+  - microlens
+  - microlens-th
 
 flags:
   {

src/Grisette/Core/Control/Monad/UnionM.hs

@@ -534,6 +534,12 @@ instance (LogicalOp a, Mergeable a) => LogicalOp (UnionM a) where
   symXor = unionMBinOp symXor
   symImplies = unionMBinOp symImplies
 
+instance (Monoid a, Mergeable a) => Monoid (UnionM a) where
+  mempty = mrgSingle mempty
+
+instance (Monoid a, Mergeable a) => Semigroup (UnionM a) where
+  (<>) = unionMBinOp (<>)
+
 instance (Solvable c t, Mergeable t) => Solvable c (UnionM t) where
   con = mrgSingle . con
   {-# INLINE con #-}

src/Grisette/Core/Data/Class/BitVector.hs

@@ -27,6 +27,7 @@ module Grisette.Core.Data.Class.BitVector
   )
 where
 
+import Data.Functor.Const (Const (Const))
 import Data.Proxy (Proxy (Proxy))
 import GHC.TypeNats (KnownNat, type (+), type (-), type (<=))
 import Grisette.Utils.Parameterized
@@ -129,6 +130,25 @@ class BV bv where
     a ->
     bv
 
+instance (BV a) => BV (Const a b) where
+  bvConcat (Const a) (Const b) = Const (bvConcat a b)
+  {-# INLINE bvConcat #-}
+
+  bvZext n (Const a) = Const (bvZext n a)
+  {-# INLINE bvZext #-}
+
+  bvSext n (Const a) = Const (bvSext n a)
+  {-# INLINE bvSext #-}
+
+  bvExt n (Const a) = Const (bvExt n a)
+  {-# INLINE bvExt #-}
+
+  bvSelect i j (Const a) = Const (bvSelect i j a)
+  {-# INLINE bvSelect #-}
+
+  bv i w = Const (bv i w)
+  {-# INLINE bv #-}
+
 -- | Slicing out a smaller bit vector from a larger one, extract a slice from
 -- bit @i@ down to @j@.
 --

src/Grisette/Core/Data/Class/EvaluateSym.hs

@@ -34,6 +34,7 @@ import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
 import qualified Control.Monad.Writer.Lazy as WriterLazy
 import qualified Control.Monad.Writer.Strict as WriterStrict
 import qualified Data.ByteString as B
+import Data.Functor.Const (Const (Const))
 import Data.Functor.Sum (Sum)
 import Data.Int (Int16, Int32, Int64, Int8)
 import Data.Maybe (fromJust)
@@ -274,3 +275,8 @@ instance (EvaluateSym' a, EvaluateSym' b) => EvaluateSym' (a :+: b) where
 
 instance (EvaluateSym' a, EvaluateSym' b) => EvaluateSym' (a :*: b) where
   evaluateSym' fillDefault model (a :*: b) = evaluateSym' fillDefault model a :*: evaluateSym' fillDefault model b
+
+-- Const
+instance (EvaluateSym a) => EvaluateSym (Const a b) where
+  evaluateSym fillDefault model (Const a) =
+    Const $ evaluateSym fillDefault model a

src/Grisette/Core/Data/Class/ExtractSymbolics.hs

@@ -33,6 +33,7 @@ import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
 import qualified Control.Monad.Writer.Lazy as WriterLazy
 import qualified Control.Monad.Writer.Strict as WriterStrict
 import qualified Data.ByteString as B
+import Data.Functor.Const (Const (Const))
 import Data.Functor.Sum (Sum)
 import Data.Int (Int16, Int32, Int64, Int8)
 import qualified Data.Text as T
@@ -311,3 +312,7 @@ instance
   ExtractSymbolics' (a :*: b)
   where
   extractSymbolics' (l :*: r) = extractSymbolics' l <> extractSymbolics' r
+
+-- Const
+instance (ExtractSymbolics a) => ExtractSymbolics (Const a b) where
+  extractSymbolics (Const v) = extractSymbolics v

src/Grisette/Core/Data/Class/GPretty.hs

@@ -28,6 +28,7 @@ import qualified Control.Monad.Writer.Lazy as WriterLazy
 import qualified Control.Monad.Writer.Strict as WriterStrict
 import qualified Data.ByteString as B
 import qualified Data.ByteString.Char8 as C
+import Data.Functor.Const (Const)
 import Data.Functor.Sum (Sum)
 import Data.Int (Int16, Int32, Int64, Int8)
 import Data.String (IsString (fromString))
@@ -322,6 +323,12 @@ instance (GPretty (m a)) => GPretty (IdentityT m a) where
             gprettyPrec 11 a
           ]
 
+-- Const
+deriving via
+  (Default (Const a b))
+  instance
+    (GPretty a) => GPretty (Const a b)
+
 -- Prettyprint
 #define GPRETTY_SYM_SIMPLE(symtype) \
 instance GPretty symtype where \

src/Grisette/Core/Data/Class/GenSym.hs

@@ -97,6 +97,7 @@ import qualified Control.Monad.Writer.Lazy as WriterLazy
 import qualified Control.Monad.Writer.Strict as WriterStrict
 import Data.Bifunctor (Bifunctor (first))
 import qualified Data.ByteString as B
+import Data.Functor.Const (Const (Const))
 import Data.Hashable (Hashable)
 import Data.Int (Int16, Int32, Int64, Int8)
 import Data.String (IsString (fromString))
@@ -1720,3 +1721,15 @@ instance
     where
       go (UnionSingle x) = fresh x
       go (UnionIf _ _ _ t f) = mrgIf <$> simpleFresh () <*> go t <*> go f
+
+instance (GenSym spec a) => GenSym spec (Const a b) where
+  fresh spec = do
+    u <- fresh spec
+    return $ do
+      a <- u
+      mrgSingle $ Const a
+  {-# INLINE fresh #-}
+
+instance (GenSymSimple spec a) => GenSymSimple spec (Const a b) where
+  simpleFresh spec = Const <$> simpleFresh spec
+  {-# INLINE simpleFresh #-}

src/Grisette/Core/Data/Class/ITEOp.hs

@@ -17,6 +17,7 @@ module Grisette.Core.Data.Class.ITEOp
   )
 where
 
+import Data.Functor.Const (Const (Const))
 import GHC.TypeNats (KnownNat, type (<=))
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
   ( LinkedRep,
@@ -75,3 +76,7 @@ ITEOP_BV(SymWordN)
 ITEOP_FUN(=~>, SymTabularFun)
 ITEOP_FUN(-~>, SymGeneralFun)
 #endif
+
+instance (ITEOp a) => ITEOp (Const a b) where
+  symIte c (Const t) (Const f) = Const $ symIte c t f
+  {-# INLINE symIte #-}

src/Grisette/Core/Data/Class/LogicalOp.hs

@@ -3,6 +3,7 @@ module Grisette.Core.Data.Class.LogicalOp
   )
 where
 
+import Data.Functor.Const (Const (Const))
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
   ( pevalAndTerm,
     pevalImplyTerm,
@@ -104,3 +105,15 @@ instance LogicalOp SymBool where
   symNot (SymBool v) = SymBool $ pevalNotTerm v
   (SymBool l) `symXor` (SymBool r) = SymBool $ pevalXorTerm l r
   (SymBool l) `symImplies` (SymBool r) = SymBool $ pevalImplyTerm l r
+
+instance (LogicalOp a) => LogicalOp (Const a b) where
+  (.||) (Const a) (Const b) = Const $ a .|| b
+  {-# INLINE (.||) #-}
+  (.&&) (Const a) (Const b) = Const $ a .&& b
+  {-# INLINE (.&&) #-}
+  symNot (Const a) = Const $ symNot a
+  {-# INLINE symNot #-}
+  symXor (Const a) (Const b) = Const $ symXor a b
+  {-# INLINE symXor #-}
+  symImplies (Const a) (Const b) = Const $ symImplies a b
+  {-# INLINE symImplies #-}

src/Grisette/Core/Data/Class/Mergeable.hs

@@ -83,6 +83,7 @@ import Data.Functor.Classes
     eq1,
     showsPrec1,
   )
+import Data.Functor.Const (Const (Const, getConst))
 import Data.Functor.Sum (Sum (InL, InR))
 import Data.Int (Int16, Int32, Int64, Int8)
 import Data.Kind (Type)
@@ -1038,3 +1039,14 @@ instance (Mergeable' a, Mergeable' b) => Mergeable' (a :+: b) where
             else wrapStrategy rootStrategy' R1 (\case (R1 v) -> v; _ -> undefined)
       )
   {-# INLINE rootStrategy' #-}
+
+deriving via
+  (Default (Const a b))
+  instance
+    (Mergeable a) => Mergeable (Const a b)
+
+deriving via (Default1 (Const a)) instance (Mergeable a) => Mergeable1 (Const a)
+
+instance Mergeable2 Const where
+  liftRootStrategy2 sa _ = wrapStrategy sa Const getConst
+  {-# INLINE liftRootStrategy2 #-}

src/Grisette/Core/Data/Class/SEq.hs

@@ -35,6 +35,7 @@ import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
 import qualified Control.Monad.Writer.Lazy as WriterLazy
 import qualified Control.Monad.Writer.Strict as WriterStrict
 import qualified Data.ByteString as B
+import Data.Functor.Const (Const)
 import Data.Functor.Sum (Sum)
 import Data.Int (Int16, Int32, Int64, Int8)
 import qualified Data.Text as T
@@ -282,3 +283,8 @@ instance (SEq' a, SEq' b) => SEq' (a :*: b) where
 instance (Generic a, SEq' (Rep a)) => SEq (Default a) where
   Default l .== Default r = from l ..== from r
   {-# INLINE (.==) #-}
+
+deriving via
+  (Default (Const a b))
+  instance
+    (SEq a) => SEq (Const a b)

src/Grisette/Core/Data/Class/SOrd.hs

@@ -39,6 +39,7 @@ import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
 import qualified Control.Monad.Writer.Lazy as WriterLazy
 import qualified Control.Monad.Writer.Strict as WriterStrict
 import qualified Data.ByteString as B
+import Data.Functor.Const (Const (Const))
 import Data.Functor.Sum (Sum)
 import Data.Int (Int16, Int32, Int64, Int8)
 import qualified Data.Text as T
@@ -390,6 +391,19 @@ instance (SOrd a, Mergeable a) => SOrd (UnionM a) where
     y1 <- tryMerge y
     x1 `symCompare` y1
 
+-- | Const
+instance (SOrd a) => SOrd (Const a b) where
+  (Const l) .<= (Const r) = l .<= r
+  {-# INLINE (.<=) #-}
+  (Const l) .< (Const r) = l .< r
+  {-# INLINE (.<) #-}
+  (Const l) .>= (Const r) = l .>= r
+  {-# INLINE (.>=) #-}
+  (Const l) .> (Const r) = l .> r
+  {-# INLINE (.>) #-}
+  (Const l) `symCompare` (Const r) = l `symCompare` r
+  {-# INLINE symCompare #-}
+
 -- | Auxiliary class for 'SOrd' instance derivation
 class (SEq' f) => SOrd' f where
   -- | Auxiliary function for '(..<) derivation

src/Grisette/Core/Data/Class/SafeDivision.hs

@@ -27,6 +27,7 @@ where
 
 import Control.Exception (ArithException (DivideByZero, Overflow, Underflow))
 import Control.Monad.Except (MonadError (throwError))
+import Data.Functor.Const (Const (Const))
 import Data.Int (Int16, Int32, Int64, Int8)
 import Data.Word (Word16, Word32, Word64, Word8)
 import GHC.TypeNats (KnownNat, type (<=))
@@ -290,3 +291,21 @@ instance
   SAFE_DIVISION_SYMBOLIC_FUNC2(safeDivMod, SymWordN, pevalDivIntegralTerm, pevalModIntegralTerm)
   SAFE_DIVISION_SYMBOLIC_FUNC2(safeQuotRem, SymWordN, pevalQuotIntegralTerm, pevalRemIntegralTerm)
 #endif
+
+instance (SafeDivision e a m) => SafeDivision e (Const a b) m where
+  safeDiv (Const c) (Const r) = mrgFmap Const $ safeDiv c r
+  {-# INLINE safeDiv #-}
+  safeMod (Const c) (Const r) = mrgFmap Const $ safeMod c r
+  {-# INLINE safeMod #-}
+  safeDivMod (Const c) (Const r) = do
+    (d, m) <- safeDivMod c r
+    mrgReturn (Const d, Const m)
+  {-# INLINE safeDivMod #-}
+  safeQuot (Const c) (Const r) = mrgFmap Const $ safeQuot c r
+  {-# INLINE safeQuot #-}
+  safeRem (Const c) (Const r) = mrgFmap Const $ safeRem c r
+  {-# INLINE safeRem #-}
+  safeQuotRem (Const c) (Const r) = do
+    (q, m) <- safeQuotRem c r
+    mrgReturn (Const q, Const m)
+  {-# INLINE safeQuotRem #-}

src/Grisette/Core/Data/Class/SafeLinearArith.hs

@@ -26,6 +26,7 @@ where
 
 import Control.Exception (ArithException (DivideByZero, Overflow, Underflow))
 import Control.Monad.Except (MonadError (throwError))
+import Data.Functor.Const (Const (Const))
 import Data.Int (Int16, Int32, Int64, Int8)
 import Data.Word (Word16, Word32, Word64, Word8)
 import GHC.TypeNats (KnownNat, type (<=))
@@ -53,7 +54,7 @@ import Grisette.IR.SymPrim.Data.SymPrim
     SymInteger,
     SymWordN,
   )
-import Grisette.Lib.Control.Monad (mrgReturn)
+import Grisette.Lib.Control.Monad (mrgFmap, mrgReturn)
 import Grisette.Lib.Control.Monad.Except (mrgThrowError)
 
 -- $setup
@@ -224,3 +225,11 @@ instance
       (mrgSingle res)
     where
       res = ls - rs
+
+instance (SafeLinearArith e a m) => SafeLinearArith e (Const a b) m where
+  safeAdd (Const a) (Const b) = mrgFmap Const $ safeAdd a b
+  {-# INLINE safeAdd #-}
+  safeNeg (Const a) = mrgFmap Const $ safeNeg a
+  {-# INLINE safeNeg #-}
+  safeSub (Const a) (Const b) = mrgFmap Const $ safeSub a b
+  {-# INLINE safeSub #-}