| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Utils.ProfileOptions
Synopsis
- data ProfileOption
- data ProfileOptions
- noProfileOptions :: ProfileOptions
- addProfileOption :: String -> ProfileOptions -> Either String ProfileOptions
- containsProfileOption :: ProfileOption -> ProfileOptions -> Bool
- profileOptionsToList :: ProfileOptions -> [ProfileOption]
- profileOptionsFromList :: [ProfileOption] -> ProfileOptions
- validProfileOptionStrings :: [String]
Documentation
data ProfileOption Source #
Various things that can be measured when checking an Agda development. Turned on with
the `--profile` flag, for instance `--profile=sharing` to turn on the Sharing option.
Internal, Modules, and Definitions are mutually exclusive.
NOTE: Changing this data type requires bumping the interface version number in
currentInterfaceVersion.
Constructors
| Internal | Measure time taken by various parts of the system (type checking, serialization, etc) |
| Modules | Measure time spent on individual (Agda) modules |
| Definitions | Measure time spent on individual (Agda) definitions |
| Sharing | Measure things related to sharing |
| Serialize | Collect detailed statistics about serialization |
| Constraints | Collect statistics about constraint solving |
| Metas | Count number of created metavariables |
| Interactive | Measure time of interactive commands |
| Conversion | Collect statistics about conversion checking |
| Instances | Collect statistics about instance search |
Instances
| EmbPrj ProfileOption Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: ProfileOption -> S Int32 Source # icod_ :: ProfileOption -> S Int32 Source # value :: Int32 -> R ProfileOption Source # | |||||
| NFData ProfileOption Source # | |||||
Defined in Agda.Utils.ProfileOptions Methods rnf :: ProfileOption -> () | |||||
| Bounded ProfileOption Source # | |||||
Defined in Agda.Utils.ProfileOptions | |||||
| Enum ProfileOption Source # | |||||
Defined in Agda.Utils.ProfileOptions Methods succ :: ProfileOption -> ProfileOption pred :: ProfileOption -> ProfileOption toEnum :: Int -> ProfileOption fromEnum :: ProfileOption -> Int enumFrom :: ProfileOption -> [ProfileOption] enumFromThen :: ProfileOption -> ProfileOption -> [ProfileOption] enumFromTo :: ProfileOption -> ProfileOption -> [ProfileOption] enumFromThenTo :: ProfileOption -> ProfileOption -> ProfileOption -> [ProfileOption] | |||||
| Generic ProfileOption Source # | |||||
Defined in Agda.Utils.ProfileOptions Associated Types
| |||||
| Show ProfileOption Source # | |||||
Defined in Agda.Utils.ProfileOptions Methods showsPrec :: Int -> ProfileOption -> ShowS show :: ProfileOption -> String showList :: [ProfileOption] -> ShowS | |||||
| Eq ProfileOption Source # | |||||
Defined in Agda.Utils.ProfileOptions | |||||
| Ord ProfileOption Source # | |||||
Defined in Agda.Utils.ProfileOptions Methods compare :: ProfileOption -> ProfileOption -> Ordering (<) :: ProfileOption -> ProfileOption -> Bool (<=) :: ProfileOption -> ProfileOption -> Bool (>) :: ProfileOption -> ProfileOption -> Bool (>=) :: ProfileOption -> ProfileOption -> Bool max :: ProfileOption -> ProfileOption -> ProfileOption min :: ProfileOption -> ProfileOption -> ProfileOption | |||||
| type Rep ProfileOption Source # | |||||
Defined in Agda.Utils.ProfileOptions type Rep ProfileOption = D1 ('MetaData "ProfileOption" "Agda.Utils.ProfileOptions" "Agda-2.6.20240714-inplace" 'False) (((C1 ('MetaCons "Internal" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Modules" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Definitions" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Sharing" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Serialize" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "Constraints" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Metas" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Interactive" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Conversion" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Instances" 'PrefixI 'False) (U1 :: Type -> Type))))) | |||||
data ProfileOptions Source #
A set of ProfileOptions
Instances
| EmbPrj ProfileOptions Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: ProfileOptions -> S Int32 Source # icod_ :: ProfileOptions -> S Int32 Source # value :: Int32 -> R ProfileOptions Source # | |
| Null ProfileOptions Source # | |
Defined in Agda.Utils.ProfileOptions | |
| NFData ProfileOptions Source # | |
Defined in Agda.Utils.ProfileOptions Methods rnf :: ProfileOptions -> () | |
| Show ProfileOptions Source # | |
Defined in Agda.Utils.ProfileOptions Methods showsPrec :: Int -> ProfileOptions -> ShowS show :: ProfileOptions -> String showList :: [ProfileOptions] -> ShowS | |
| Eq ProfileOptions Source # | |
Defined in Agda.Utils.ProfileOptions Methods (==) :: ProfileOptions -> ProfileOptions -> Bool (/=) :: ProfileOptions -> ProfileOptions -> Bool | |
noProfileOptions :: ProfileOptions Source #
The empty set of profiling options.
addProfileOption :: String -> ProfileOptions -> Either String ProfileOptions Source #
Parse and add a profiling option to a set of profiling options. Returns Left with a helpful
error message if the option doesn't parse or if it's incompatible with existing options.
The special string "all" adds all options compatible with the given set and prefering the first
of incompatible options. So `--profile=all` sets Internal over Modules and Definitions,
but `--profile=modules --profile=all` sets Modules and not Internal.
containsProfileOption :: ProfileOption -> ProfileOptions -> Bool Source #
Check if a given profiling option is present in a set of profiling options.
profileOptionsToList :: ProfileOptions -> [ProfileOption] Source #
Use only for serialization.
profileOptionsFromList :: [ProfileOption] -> ProfileOptions Source #
Use only for serialization.
validProfileOptionStrings :: [String] Source #
Strings accepted by addProfileOption