Agda-2.6.4: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Utils.ProfileOptions

Synopsis

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

Instances details
EmbPrj ProfileOption Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ProfileOption -> S Int32 Source #

icod_ :: ProfileOption -> S Int32 Source #

value :: Int32 -> R ProfileOption Source #

Bounded ProfileOption Source # 
Instance details

Defined in Agda.Utils.ProfileOptions

Methods

minBound :: ProfileOption

maxBound :: ProfileOption

Enum ProfileOption Source # 
Instance details

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 # 
Instance details

Defined in Agda.Utils.ProfileOptions

Associated Types

type Rep ProfileOption :: Type -> Type

Methods

from :: ProfileOption -> Rep ProfileOption x

to :: Rep ProfileOption x -> ProfileOption

Show ProfileOption Source # 
Instance details

Defined in Agda.Utils.ProfileOptions

Methods

showsPrec :: Int -> ProfileOption -> ShowS

show :: ProfileOption -> String

showList :: [ProfileOption] -> ShowS

NFData ProfileOption Source # 
Instance details

Defined in Agda.Utils.ProfileOptions

Methods

rnf :: ProfileOption -> ()

Eq ProfileOption Source # 
Instance details

Defined in Agda.Utils.ProfileOptions

Methods

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

(/=) :: ProfileOption -> ProfileOption -> Bool

Ord ProfileOption Source # 
Instance details

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 # 
Instance details

Defined in Agda.Utils.ProfileOptions

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

data ProfileOptions Source #

A set of ProfileOptions

Instances

Instances details
EmbPrj ProfileOptions Source # 
Instance details

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 # 
Instance details

Defined in Agda.Utils.ProfileOptions

Methods

empty :: ProfileOptions Source #

null :: ProfileOptions -> Bool Source #

Show ProfileOptions Source # 
Instance details

Defined in Agda.Utils.ProfileOptions

Methods

showsPrec :: Int -> ProfileOptions -> ShowS

show :: ProfileOptions -> String

showList :: [ProfileOptions] -> ShowS

NFData ProfileOptions Source # 
Instance details

Defined in Agda.Utils.ProfileOptions

Methods

rnf :: ProfileOptions -> ()

Eq ProfileOptions Source # 
Instance details

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