From 62f65b3fe0aab38664e79e266a046eecd3de999c Mon Sep 17 00:00:00 2001 From: Sirui Lu Date: Wed, 11 Dec 2024 02:04:51 -0800 Subject: [PATCH] :memo: Update documentation --- src/Grisette/Internal/SymPrim/SymPrim.hs | 3 ++- src/Grisette/Internal/TH/GADT/Common.hs | 11 ++++++++ .../Internal/TH/GADT/DeriveMergeable.hs | 4 +++ .../Internal/TH/GADT/UnaryOpCommon.hs | 25 +++++++++++++++++-- src/Grisette/Unified/Internal/BaseMonad.hs | 2 +- .../Unified/Internal/UnifiedAlgReal.hs | 4 +-- src/Grisette/Unified/Internal/UnifiedBV.hs | 8 +++--- src/Grisette/Unified/Internal/UnifiedBool.hs | 4 +-- src/Grisette/Unified/Internal/UnifiedData.hs | 4 +-- src/Grisette/Unified/Internal/UnifiedFP.hs | 6 ++--- src/Grisette/Unified/Internal/UnifiedFun.hs | 4 +-- .../Unified/Internal/UnifiedInteger.hs | 4 +-- src/Grisette/Unified/Internal/UnifiedPrim.hs | 3 ++- 13 files changed, 60 insertions(+), 22 deletions(-) diff --git a/src/Grisette/Internal/SymPrim/SymPrim.hs b/src/Grisette/Internal/SymPrim/SymPrim.hs index 5402e047..af1f9b5d 100644 --- a/src/Grisette/Internal/SymPrim/SymPrim.hs +++ b/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, diff --git a/src/Grisette/Internal/TH/GADT/Common.hs b/src/Grisette/Internal/TH/GADT/Common.hs index 9b6bbe1f..2ea24e0d 100644 --- a/src/Grisette/Internal/TH/GADT/Common.hs +++ b/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 -> diff --git a/src/Grisette/Internal/TH/GADT/DeriveMergeable.hs b/src/Grisette/Internal/TH/GADT/DeriveMergeable.hs index e3c9d2d6..a3808c73 100644 --- a/src/Grisette/Internal/TH/GADT/DeriveMergeable.hs +++ b/src/Grisette/Internal/TH/GADT/DeriveMergeable.hs @@ -313,6 +313,7 @@ genMergingInfo typName = do ] ) +-- | Generate 'Mergeable' instance and merging information for a GADT. genMergeableAndGetMergingInfoResult :: Name -> Int -> Q (MergingInfoResult, [Dec]) genMergeableAndGetMergingInfoResult typName n = do @@ -320,6 +321,7 @@ genMergeableAndGetMergingInfoResult typName n = do (_, 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 diff --git a/src/Grisette/Internal/TH/GADT/UnaryOpCommon.hs b/src/Grisette/Internal/TH/GADT/UnaryOpCommon.hs index 5bdf42be..62c7bc5b 100644 --- a/src/Grisette/Internal/TH/GADT/UnaryOpCommon.hs +++ b/src/Grisette/Internal/TH/GADT/UnaryOpCommon.hs @@ -3,12 +3,19 @@ {-# 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 @@ -16,7 +23,17 @@ 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 -> diff --git a/src/Grisette/Unified/Internal/BaseMonad.hs b/src/Grisette/Unified/Internal/BaseMonad.hs index 998a5276..e31c18b7 100644 --- a/src/Grisette/Unified/Internal/BaseMonad.hs +++ b/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 diff --git a/src/Grisette/Unified/Internal/UnifiedAlgReal.hs b/src/Grisette/Unified/Internal/UnifiedAlgReal.hs index be2727a0..23c87a93 100644 --- a/src/Grisette/Unified/Internal/UnifiedAlgReal.hs +++ b/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'. diff --git a/src/Grisette/Unified/Internal/UnifiedBV.hs b/src/Grisette/Unified/Internal/UnifiedBV.hs index d56ff173..7ddeb5f1 100644 --- a/src/Grisette/Unified/Internal/UnifiedBV.hs +++ b/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) diff --git a/src/Grisette/Unified/Internal/UnifiedBool.hs b/src/Grisette/Unified/Internal/UnifiedBool.hs index 7e47d73e..fa502d5d 100644 --- a/src/Grisette/Unified/Internal/UnifiedBool.hs +++ b/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 diff --git a/src/Grisette/Unified/Internal/UnifiedData.hs b/src/Grisette/Unified/Internal/UnifiedData.hs index d5f03d6c..222cdde8 100644 --- a/src/Grisette/Unified/Internal/UnifiedData.hs +++ b/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. diff --git a/src/Grisette/Unified/Internal/UnifiedFP.hs b/src/Grisette/Unified/Internal/UnifiedFP.hs index 8626d913..e6316a9a 100644 --- a/src/Grisette/Unified/Internal/UnifiedFP.hs +++ b/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 diff --git a/src/Grisette/Unified/Internal/UnifiedFun.hs b/src/Grisette/Unified/Internal/UnifiedFun.hs index 4a912dde..822ba1a7 100644 --- a/src/Grisette/Unified/Internal/UnifiedFun.hs +++ b/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 diff --git a/src/Grisette/Unified/Internal/UnifiedInteger.hs b/src/Grisette/Unified/Internal/UnifiedInteger.hs index 1e84f527..b6db5169 100644 --- a/src/Grisette/Unified/Internal/UnifiedInteger.hs +++ b/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 diff --git a/src/Grisette/Unified/Internal/UnifiedPrim.hs b/src/Grisette/Unified/Internal/UnifiedPrim.hs index 630619e5..b0cd56d2 100644 --- a/src/Grisette/Unified/Internal/UnifiedPrim.hs +++ b/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,