Agda-2.6.4.1: A dependently typed functional programming language and proof assistant
Safe HaskellNone
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

Bounded ProfileOption Source # 
Instance details

Defined in Agda.Utils.ProfileOptions

Enum ProfileOption Source # 
Instance details

Defined in Agda.Utils.ProfileOptions

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.6.4.1-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)))))
Show ProfileOption Source # 
Instance details

Defined in Agda.Utils.ProfileOptions

NFData ProfileOption Source # 
Instance details

Defined in Agda.Utils.ProfileOptions

Methods

rnf :: ProfileOption -> () #

Eq ProfileOption Source # 
Instance details

Defined in Agda.Utils.ProfileOptions

Ord ProfileOption Source # 
Instance details

Defined in Agda.Utils.ProfileOptions

type Rep ProfileOption Source # 
Instance details

Defined in Agda.Utils.ProfileOptions

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

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.