Core.Options.Log

Reexports

Definitions

knownTopics : List (String, Maybe String)

  Log levels are characterised by two things:
  * a dot-separated path of ever finer topics of interest e.g. scope.let
  * a natural number corresponding to the verbosity level e.g. 5
  
  If the user asks for some logs by writing
  
      %log scope 5
  
  they will get all of the logs whose path starts with `scope` and whose
  verbosity level is less or equal to `5`. By combining different logging
  directives, users can request information about everything (with a low
  level of details) and at the same time focus on a particular subsystem
  they want to get a lot of information about. For instance:
  
      %log 1
      %log scope.let 10
  
  will deliver basic information about the various phases the compiler goes
  through and deliver a lot of information about scope-checking let binders.

Totality: total
Visibility: public export

helpTopics : String

Totality: total
Visibility: export

data KnownTopic : String -> Type

Totality: total
Visibility: public export
Constructor: 

IsKnownTopic : IsJust (lookup s knownTopics) => KnownTopic s

record LogTopic : Type

Totality: total
Visibility: public export
Constructor: 

MkLogTopic : (topic : String) -> {auto 0 _ : KnownTopic topic} -> LogTopic

Projections:

0 .known : ({rec:0} : LogTopic) -> KnownTopic (topic {rec:0})

.topic : LogTopic -> String

.topic : LogTopic -> String

Totality: total
Visibility: public export

topic : LogTopic -> String

Totality: total
Visibility: public export

0 .known : ({rec:0} : LogTopic) -> KnownTopic (topic {rec:0})

Totality: total
Visibility: public export

0 known : ({rec:0} : LogTopic) -> KnownTopic (topic {rec:0})

Totality: total
Visibility: public export

fromString : (s : String) -> {auto 0 _ : KnownTopic s} -> LogTopic

Totality: total
Visibility: export

data LogLevel : Type

  An individual log level is a pair of a list of non-empty strings and a number.
  We keep the representation opaque to force users to call the smart constructor

Totality: total
Visibility: export
Constructor: 

MkLogLevel : List String -> Nat -> LogLevel

Hint: 

Show LogLevel

mkLogLevel' : Maybe (List1 String) -> Nat -> LogLevel

  If we have already processed the input string into (maybe) a non-empty list of
  non-empty topics we can safely make a `LogLevel`.

Totality: total
Visibility: export

mkUnverifiedLogLevel : String -> Nat -> LogLevel

  The smart constructor makes sure that the empty string is mapped to the empty
  list. This bypasses the fact that the function `split` returns a non-empty
  list no matter what.
  
  However, invoking this function comes without guarantees that
  the passed string corresponds to a known topic. For this,
  use `mkLogLevel`.
  
  Use this function to create user defined loglevels, for instance, during
  elaborator reflection.

Totality: total
Visibility: export

mkLogLevel : LogTopic -> Nat -> LogLevel

  Like `mkUnverifiedLogLevel` but with a compile time check that
  the passed string is a known topic.

Totality: total
Visibility: export

unsafeMkLogLevel : List String -> Nat -> LogLevel

  The unsafe constructor should only be used in places where the topic has already
  been appropriately processed.

Totality: total
Visibility: export

topics : LogLevel -> List String

  The topics attached to a `LogLevel` can be reconstructed from the list of strings.

Totality: total
Visibility: export

verbosity : LogLevel -> Nat

  The verbosity is provided by the natural number

Totality: total
Visibility: export

withVerbosity : Nat -> LogLevel -> LogLevel

  When writing generic functions we sometimes want to keep the same topic but
  change the verbosity.

Totality: total
Visibility: export

parseLogLevel : String -> Maybe LogLevel

Totality: total
Visibility: export

LogLevels : Type

  We store the requested log levels in a Trie which makes it easy to check
  whether a given log level is captured by the user's request for information.

Totality: total
Visibility: export

defaultLogLevel : LogLevels

  By default we log everything but with very few details (i.e. next to nothing)

Totality: total
Visibility: export

insertLogLevel : LogLevel -> LogLevels -> LogLevels

Totality: total
Visibility: export

keepLog : LogLevel -> LogLevels -> Bool

  We keep a log if there is a prefix of its path associated to a larger number
  in the LogLevels.

Totality: total
Visibility: export