📝 Update documentation

src/Grisette/Internal/SymPrim/SymPrim.hs

@@ -72,7 +72,8 @@ type SymPrim a =
 -- | A type that is used as a constraint for all the basic symbolic primitive
 -- types in Grisette.
 --
--- 'SomeSymWordN' is not considered as a basic symbolic primitive type.
+-- 'Grisette.SymPrim.SomeSymWordN' is not considered as a basic symbolic
+-- primitive type.
 type BasicSymPrim a =
   ( SymPrim a,
     SimpleMergeable a,

src/Grisette/Internal/TH/GADT/Common.hs

@@ -1,5 +1,13 @@
 {-# LANGUAGE RecordWildCards #-}
 
+-- |
+-- Module      :   Grisette.Internal.TH.GADT.Common
+-- Copyright   :   (c) Sirui Lu 2024
+-- License     :   BSD-3-Clause (see the LICENSE file)
+--
+-- Maintainer  :   siruilu@cs.washington.edu
+-- Stability   :   Experimental
+-- Portability :   GHC only
 module Grisette.Internal.TH.GADT.Common
   ( CheckArgsResult (..),
     checkArgs,
@@ -25,6 +33,7 @@ import Language.Haskell.TH.Datatype
   )
 import Language.Haskell.TH.Datatype.TyVarBndr (TyVarBndr_, mapTVName)
 
+-- | Result of 'checkArgs' for a GADT.
 data CheckArgsResult = CheckArgsResult
   { constructors :: [ConstructorInfo],
     keptNewNames :: [Name],
@@ -34,6 +43,8 @@ data CheckArgsResult = CheckArgsResult
     isVarUsedInFields :: Name -> Bool
   }
 
+-- | Check if the number of type parameters is valid for a GADT, and return
+-- new names for the type variables, split into kept and arg parts.
 checkArgs ::
   String ->
   Int ->

src/Grisette/Internal/TH/GADT/DeriveMergeable.hs

@@ -313,13 +313,15 @@ genMergingInfo typName = do
           ]
     )
 
+-- | Generate 'Mergeable' instance and merging information for a GADT.
 genMergeableAndGetMergingInfoResult ::
   Name -> Int -> Q (MergingInfoResult, [Dec])
 genMergeableAndGetMergingInfoResult typName n = do
   (infoResult, infoDec) <- genMergingInfo typName
   (_, decs) <- genMergeable' infoResult typName n
   return (infoResult, infoDec ++ decs)
 
+-- | Generate 'Mergeable' instance for a GADT.
 genMergeable :: Name -> Int -> Q [Dec]
 genMergeable typName n = do
   (infoResult, infoDec) <- genMergingInfo typName
@@ -480,6 +482,8 @@ genMergingInfoFunClause' argTypes conInfoName pos oldCon = do
   -- fail $ show infoExp
   return $ Clause (strategyPats ++ [varPat]) (NormalB infoExp) []
 
+-- | Generate 'Mergeable' instance for a GADT, using a given merging info
+-- result.
 genMergeable' :: MergingInfoResult -> Name -> Int -> Q (Name, [Dec])
 genMergeable' (MergingInfoResult infoName conInfoNames pos) typName n = do
   CheckArgsResult {..} <- checkArgs "Mergeable" 3 typName n

src/Grisette/Internal/TH/GADT/UnaryOpCommon.hs

@@ -3,20 +3,37 @@
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TupleSections #-}
 
+-- |
+-- Module      :   Grisette.Internal.TH.GADT.UnaryOpCommon
+-- Copyright   :   (c) Sirui Lu 2024
+-- License     :   BSD-3-Clause (see the LICENSE file)
+--
+-- Maintainer  :   siruilu@cs.washington.edu
+-- Stability   :   Experimental
+-- Portability :   GHC only
 module Grisette.Internal.TH.GADT.UnaryOpCommon
   ( UnaryOpClassConfig (..),
     UnaryOpFieldConfig (..),
     genUnaryOpClause,
     genUnaryOpClass,
-    fieldExp,
   )
 where
 
 import Control.Monad (replicateM, zipWithM)
 import qualified Data.Map as M
 import Data.Maybe (catMaybes, mapMaybe)
 import qualified Data.Set as S
-import Grisette.Internal.TH.GADT.Common (CheckArgsResult (CheckArgsResult, argNewNames, constructors, isVarUsedInFields, keptNewNames, keptNewVars), checkArgs)
+import Grisette.Internal.TH.GADT.Common
+  ( CheckArgsResult
+      ( CheckArgsResult,
+        argNewNames,
+        constructors,
+        isVarUsedInFields,
+        keptNewNames,
+        keptNewVars
+      ),
+    checkArgs,
+  )
 import Grisette.Internal.TH.Util (occName)
 import Language.Haskell.TH
   ( Body (NormalB),
@@ -100,11 +117,13 @@ patAndExps fieldFunExpGen argTypes fields = do
   fieldEvalSymFunExps <- traverse (fieldFunExpGen argToFunPat) fields
   return (funPats, fieldEvalSymFunExps)
 
+-- | Configuration for a unary function field expression generation on a GADT.
 data UnaryOpFieldConfig = UnaryOpFieldConfig
   { extraPatNames :: [String],
     fieldCombineFun :: Exp -> [Exp] -> Q Exp
   }
 
+-- | Generate a clause for a unary function on a GADT.
 genUnaryOpClause ::
   [Name] ->
   UnaryOpFieldConfig ->
@@ -141,12 +160,14 @@ genUnaryOpClause
     resExp <- fieldCombineFun (ConE (constructorName conInfo)) fieldExps
     return $ Clause (funPats ++ extraPats ++ [fieldPats]) (NormalB resExp) []
 
+-- | Configuration for a unary operation type class generation on a GADT.
 data UnaryOpClassConfig = UnaryOpClassConfig
   { unaryOpFieldConfig :: UnaryOpFieldConfig,
     unaryOpInstanceNames :: [Name],
     unaryOpFunNames :: [Name]
   }
 
+-- | Generate a unary operation type class instance for a GADT.
 genUnaryOpClass ::
   UnaryOpClassConfig ->
   Int ->

src/Grisette/Unified/Internal/BaseMonad.hs

@@ -22,7 +22,7 @@ import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (C, S))
 
 -- | A type family that specifies the base monad for the evaluation mode.
 --
--- Resolves to 'Identity' for `Con` mode, and 'Union' for `Sym` mode.
+-- Resolves to 'Identity' for `C` mode, and 'Union' for `S` mode.
 type family
   BaseMonad (mode :: EvalModeTag) =
     (r :: Type -> Type) | r -> mode

src/Grisette/Unified/Internal/UnifiedAlgReal.hs

@@ -57,8 +57,8 @@ class
   UnifiedAlgRealImpl (mode :: EvalModeTag) r
     | mode -> r
   where
-  -- | Get a unified algebraic real type. Resolves to 'AlgReal' in 'Con' mode,
-  -- and 'SymAlgReal' in 'Sym' mode.
+  -- | Get a unified algebraic real type. Resolves to 'AlgReal' in 'C' mode,
+  -- and 'SymAlgReal' in 'S' mode.
   --
   -- 'Floating', 'Grisette.LogBaseOr' and 'Grisette.SafeLogBase' for
   -- 'SymAlgReal' are not provided as they are not available for 'AlgReal'.

src/Grisette/Unified/Internal/UnifiedBV.hs

@@ -146,11 +146,11 @@ class
       int -> intn n
   where
   -- | Get a unified unsigned size-tagged bit vector type. Resolves to 'WordN'
-  -- in 'Con' mode, and 'SymWordN' in 'Sym' mode.
+  -- in 'C' mode, and 'SymWordN' in 'S' mode.
   type GetWordN mode = (w :: Nat -> Type) | w -> mode
 
   -- | Get a unified signed size-tagged bit vector type. Resolves to 'IntN'
-  -- in 'Con' mode, and 'SymIntN' in 'Sym' mode.
+  -- in 'C' mode, and 'SymIntN' in 'S' mode.
   type GetIntN mode = (i :: Nat -> Type) | i -> mode
 
 instance
@@ -168,12 +168,12 @@ instance
   type GetIntN 'S = SymIntN
 
 -- | Get a unified unsigned dynamic bit width bit vector type. Resolves to
--- 'SomeWordN' in 'Con' mode, and 'SomeSymWordN' in 'Sym' mode.
+-- 'SomeWordN' in 'C' mode, and 'SomeSymWordN' in 'S' mode.
 type family GetSomeWordN mode = sw | sw -> mode where
   GetSomeWordN mode = SomeBV (GetWordN mode)
 
 -- | Get a unified signed dynamic bit width bit vector type. Resolves to
--- 'SomeIntN' in 'Con' mode, and 'SomeSymIntN' in 'Sym' mode.
+-- 'SomeIntN' in 'C' mode, and 'SomeSymIntN' in 'S' mode.
 type family GetSomeIntN mode = sw | sw -> mode where
   GetSomeIntN mode = SomeBV (GetIntN mode)
 

src/Grisette/Unified/Internal/UnifiedBool.hs

@@ -37,8 +37,8 @@ class
   ) =>
   UnifiedBool (mode :: EvalModeTag)
   where
-  -- | Get a unified Boolean type. Resolves to 'Bool' in 'Con' mode, and
-  -- 'SymBool' in 'Sym' mode.
+  -- | Get a unified Boolean type. Resolves to 'Bool' in 'C' mode, and
+  -- 'SymBool' in 'S' mode.
   type GetBool mode = bool | bool -> mode
 
 instance UnifiedBool 'C where

src/Grisette/Unified/Internal/UnifiedData.hs

@@ -87,8 +87,8 @@ class
   UnifiedDataImpl (mode :: EvalModeTag) v u
     | u -> mode v
   where
-  -- | Get a unified data type. Resolves to @v@ in 'Con' mode, and @'Union' v@
-  -- in 'Sym' mode.
+  -- | Get a unified data type. Resolves to @v@ in 'C' mode, and @'Union' v@
+  -- in 'S' mode.
   type GetData mode v = r | r -> mode v
 
   -- | Wraps a value into the unified data type.

src/Grisette/Unified/Internal/UnifiedFP.hs

@@ -73,12 +73,12 @@ class
       rd -> fpn,
       rd eb sb -> fp
   where
-  -- | Get a unified floating point type. Resolves to 'FP' in 'Con' mode, and
-  -- 'SymFP' in 'Sym' mode.
+  -- | Get a unified floating point type. Resolves to 'FP' in 'C' mode, and
+  -- 'SymFP' in 'S' mode.
   type GetFP mode = (f :: Nat -> Nat -> Type) | f -> mode
 
   -- | Get a unified floating point rounding mode type. Resolves to
-  -- 'FPRoundingMode' in 'Con' mode, and 'SymFPRoundingMode' in 'Sym' mode.
+  -- 'FPRoundingMode' in 'C' mode, and 'SymFPRoundingMode' in 'S' mode.
   type GetFPRoundingMode mode = r | r -> mode
 
 instance

src/Grisette/Unified/Internal/UnifiedFun.hs

@@ -103,8 +103,8 @@ type TyVarBndrVis = Language.Haskell.TH.TyVarBndr
 
 -- | Provide unified function types.
 class UnifiedFun (mode :: EvalModeTag) where
-  -- | Get a unified function type. Resolves to t'Grisette.SymPrim.=->' in 'Con'
-  -- mode, and t'Grisette.SymPrim.=~>' in 'Sym' mode.
+  -- | Get a unified function type. Resolves to t'Grisette.SymPrim.=->' in 'C'
+  -- mode, and t'Grisette.SymPrim.=~>' in 'S' mode.
   type
     GetFun mode =
       (fun :: Data.Kind.Type -> Data.Kind.Type -> Data.Kind.Type) | fun -> mode

src/Grisette/Unified/Internal/UnifiedInteger.hs

@@ -59,8 +59,8 @@ class
   UnifiedIntegerImpl (mode :: EvalModeTag) i
     | mode -> i
   where
-  -- | Get a unified Integer type. Resolves to 'Integer' in 'Con' mode, and
-  -- 'SymInteger' in 'Sym' mode.
+  -- | Get a unified Integer type. Resolves to 'Integer' in 'C' mode, and
+  -- 'SymInteger' in 'S' mode.
   type GetInteger mode = int | int -> mode
 
 instance UnifiedIntegerImpl 'C Integer where

src/Grisette/Unified/Internal/UnifiedPrim.hs

@@ -47,7 +47,8 @@ type UnifiedPrim mode a =
 -- | A type that is used as a constraint for all the basic (unified) primitive
 -- types in Grisette.
 --
--- 'GetSomeWordN' is not considered as a basic (unified) primitive type.
+-- 'Grisette.Unified.GetSomeWordN' is not considered as a basic (unified)
+-- primitive type.
 type UnifiedBasicPrim mode a =
   ( UnifiedPrim mode a,
     UnifiedSimpleMergeable mode a,