Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Utils.ProfileOptions

Synopsis

- data ProfileOption
  - = Internal
  - | Modules
  - | Definitions
  - | Sharing
  - | Serialize
  - | Constraints
  - | Metas
  - | Interactive
  - | Conversion
  - | Instances
- 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

Instances details

EmbPrj ProfileOption Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: ProfileOption -> S Word32 Source # icod_ :: ProfileOption -> S Word32 Source # value :: Word32 -> R ProfileOption Source #
NFData ProfileOption Source # |
Instance details Defined in Agda.Utils.ProfileOptions Methods rnf :: ProfileOption -> () Source #
Bounded ProfileOption Source # |
Instance details Defined in Agda.Utils.ProfileOptions Methods minBound :: ProfileOption Source # maxBound :: ProfileOption Source #
Enum ProfileOption Source # |

Instance details

Defined in Agda.Utils.ProfileOptions

Methods

succ :: ProfileOption -> ProfileOption Source #

pred :: ProfileOption -> ProfileOption Source #

toEnum :: Int -> ProfileOption Source #

fromEnum :: ProfileOption -> Int Source #

enumFrom :: ProfileOption -> [ProfileOption] Source #

enumFromThen :: ProfileOption -> ProfileOption -> [ProfileOption] Source #

enumFromTo :: ProfileOption -> ProfileOption -> [ProfileOption] Source #

enumFromThenTo :: ProfileOption -> ProfileOption -> ProfileOption -> [ProfileOption] Source #

Generic ProfileOption Source # |

Instance details

Defined in Agda.Utils.ProfileOptions

Associated Types

type Rep ProfileOption |

Instance details

Defined in Agda.Utils.ProfileOptions

type Rep ProfileOption = D1 ('MetaData "ProfileOption" "Agda.Utils.ProfileOptions" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))))

Methods

from :: ProfileOption -> Rep ProfileOption x Source #

to :: Rep ProfileOption x -> ProfileOption Source #

Show ProfileOption Source # |
Instance details Defined in Agda.Utils.ProfileOptions Methods showsPrec :: Int -> ProfileOption -> ShowS Source # show :: ProfileOption -> String Source # showList :: [ProfileOption] -> ShowS Source #
Eq ProfileOption Source # |
Instance details Defined in Agda.Utils.ProfileOptions Methods (==) :: ProfileOption -> ProfileOption -> Bool Source # (/=) :: ProfileOption -> ProfileOption -> Bool Source #
Ord ProfileOption Source # |

Instance details

Defined in Agda.Utils.ProfileOptions

Methods

compare :: ProfileOption -> ProfileOption -> Ordering Source #

(<) :: ProfileOption -> ProfileOption -> Bool Source #

(<=) :: ProfileOption -> ProfileOption -> Bool Source #

(>) :: ProfileOption -> ProfileOption -> Bool Source #

(>=) :: ProfileOption -> ProfileOption -> Bool Source #

max :: ProfileOption -> ProfileOption -> ProfileOption Source #

min :: ProfileOption -> ProfileOption -> ProfileOption Source #

type Rep ProfileOption Source # |

Instance details

Defined in Agda.Utils.ProfileOptions

type Rep ProfileOption = D1 ('MetaData "ProfileOption" "Agda.Utils.ProfileOptions" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 `ProfileOption`s

#### Instances

Instances details

EmbPrj ProfileOptions Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: ProfileOptions -> S Word32 Source # icod_ :: ProfileOptions -> S Word32 Source # value :: Word32 -> R ProfileOptions Source #
Null ProfileOptions Source # |
Instance details Defined in Agda.Utils.ProfileOptions Methods empty :: ProfileOptions Source # null :: ProfileOptions -> Bool Source #
NFData ProfileOptions Source # |
Instance details Defined in Agda.Utils.ProfileOptions Methods rnf :: ProfileOptions -> () Source #
Show ProfileOptions Source # |
Instance details Defined in Agda.Utils.ProfileOptions Methods showsPrec :: Int -> ProfileOptions -> ShowS Source # show :: ProfileOptions -> String Source # showList :: [ProfileOptions] -> ShowS Source #
Eq ProfileOptions Source # |
Instance details Defined in Agda.Utils.ProfileOptions Methods (==) :: ProfileOptions -> ProfileOptions -> Bool Source # (/=) :: ProfileOptions -> ProfileOptions -> Bool Source #

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`