Agda-2.7.0.1: 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

Collect statistics about instance search

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.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" '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

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