Lean.Data.Options

Lean.registerOption name decl = do let a ← Lean.initializing let _do_jp : PUnit → IO Unit := fun y => do let decls ← ST.Ref.get Lean.optionDeclsRef let _do_jp : PUnit → IO Unit := fun y => ST.Ref.set Lean.optionDeclsRef (Lean.NameMap.insert decls name decl) if Lean.NameMap.contains decls name = true then do let y ← throw (IO.userError (toString "invalid option declaration '" ++ toString name ++ toString "', option already exists")) _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← pure PUnit.unit _do_jp y else do let y ← throw (IO.userError "failed to register option, options can only be registered during initialization") _do_jp y

source

def Lean.getOptionDecls :

IO Lean.OptionDecls

Equations

Lean.getOptionDecls = ST.Ref.get Lean.optionDeclsRef

source

def Lean.getOptionDeclsArray :

IO (Array (Lean.Name × Lean.OptionDecl))

Equations

Lean.getOptionDeclsArray = do let decls ← Lean.getOptionDecls pure (Std.RBMap.fold (fun r k v => Array.push r (k, v)) #[] decls)

source

def Lean.getOptionDecl (name : Lean.Name) :

IO Lean.OptionDecl

Equations

Lean.getOptionDecl name = do let decls ← Lean.getOptionDecls let discr ← pure (Lean.NameMap.find? decls name) match discr with | some decl => pure decl | x => throw (IO.userError (toString "unknown option '" ++ toString name ++ toString "'"))

source

def Lean.getOptionDefaulValue (name : Lean.Name) :

IO Lean.DataValue

Equations

Lean.getOptionDefaulValue name = do let decl ← Lean.getOptionDecl name pure decl.defValue

source

def Lean.getOptionDescr (name : Lean.Name) :

IO String

Equations

Lean.getOptionDescr name = do let decl ← Lean.getOptionDecl name pure decl.descr

source

def Lean.setOptionFromString (opts : Lean.Options) (entry : String) :

IO Lean.Options

Equations

Lean.setOptionFromString opts entry = let ps := List.map String.trim (String.splitOn entry "="); do let discr ← pure ps match discr with | [key, val] => let key := Lean.Name.mkSimple key; do let defValue ← Lean.getOptionDefaulValue key match defValue with | Lean.DataValue.ofString v => pure (Lean.KVMap.setString opts key val) | Lean.DataValue.ofBool v => if (key == `true) = true then pure (Lean.KVMap.setBool opts key true) else if (key == `false) = true then pure (Lean.KVMap.setBool opts key false) else throw (IO.userError (toString "invalid Bool option value '" ++ toString val ++ toString "'")) | Lean.DataValue.ofName v => pure (Lean.KVMap.setName opts key (String.toName val)) | Lean.DataValue.ofNat v => match String.toNat? val with | none => throw (IO.userError (toString "invalid Nat option value '" ++ toString val ++ toString "'")) | some v => pure (Lean.KVMap.setNat opts key v) | Lean.DataValue.ofInt v => match String.toInt? val with | none => throw (IO.userError (toString "invalid Int option value '" ++ toString val ++ toString "'")) | some v => pure (Lean.KVMap.setInt opts key v) | Lean.DataValue.ofSyntax x => throw (IO.userError (toString "invalid Syntax option value")) | x => throw (IO.userError "invalid configuration option entry, it must be of the form ' = '")

source

class Lean.MonadOptions (m : Type → Type) :

Type

getOptions : m Lean.Options

Instances

source

instance Lean.instMonadOptions {m : Type → Type} {n : Type → Type} [inst : MonadLift m n] [inst : Lean.MonadOptions m] :

Lean.MonadOptions n

Equations

Lean.instMonadOptions = { getOptions := liftM Lean.getOptions }

source

def Lean.getBoolOption {m : Type → Type} [inst : Monad m] [inst : Lean.MonadOptions m] (k : Lean.Name) (defValue : optParam Bool false) :

m Bool

Equations

Lean.getBoolOption k defValue = do let opts ← Lean.getOptions pure (Lean.KVMap.getBool opts k defValue)

source

def Lean.getNatOption {m : Type → Type} [inst : Monad m] [inst : Lean.MonadOptions m] (k : Lean.Name) (defValue : optParam Nat 0) :

m Nat

Equations

Lean.getNatOption k defValue = do let opts ← Lean.getOptions pure (Lean.KVMap.getNat opts k defValue)

source

class Lean.MonadWithOptions (m : Type → Type) :

Type 1

withOptions : {α : Type} → (Lean.Options → Lean.Options) → m α → m α

Instances

source

instance Lean.instMonadWithOptions {m : Type → Type} {n : Type → Type} [inst : MonadFunctor m n] [inst : Lean.MonadWithOptions m] :

Lean.MonadWithOptions n

Equations

Lean.instMonadWithOptions = { withOptions := fun {α} f x => monadMap (fun {β} => Lean.withOptions f) x }

source

structure Lean.Option (α : Type) :

Type

name : Lean.Name
defValue : α

source

instance Lean.instInhabitedOption :

{a : Type} → [inst : Inhabited a] → Inhabited (Lean.Option a)

Equations

Lean.instInhabitedOption = { default := { name := default, defValue := default } }

source

structure Lean.Option.Decl (α : Type) :

Type

defValue : α
group : String
descr : String

source

def Lean.Option.get? {α : Type} [inst : Lean.KVMap.Value α] (opts : Lean.Options) (opt : Lean.Option α) :

Option α

Equations

Lean.Option.get? opts opt = Lean.KVMap.get? opts opt.name

source

def Lean.Option.get {α : Type} [inst : Lean.KVMap.Value α] (opts : Lean.Options) (opt : Lean.Option α) :

α

Equations

Lean.Option.get opts opt = Lean.KVMap.get opts opt.name opt.defValue

source

def Lean.Option.set {α : Type} [inst : Lean.KVMap.Value α] (opts : Lean.Options) (opt : Lean.Option α) (val : α) :

Lean.Options

Equations

Lean.Option.set opts opt val = Lean.KVMap.set opts opt.name val

source

def Lean.Option.setIfNotSet {α : Type} [inst : Lean.KVMap.Value α] (opts : Lean.Options) (opt : Lean.Option α) (val : α) :

Lean.Options

Equations

Lean.Option.setIfNotSet opts opt val = if Lean.KVMap.contains opts opt.name = true then opts else Lean.Option.set opts opt val

source

def Lean.Option.register {α : Type} [inst : Lean.KVMap.Value α] (name : Lean.Name) (decl : Lean.Option.Decl α) :

IO (Lean.Option α)

Equations

Lean.Option.register name decl = do Lean.registerOption name { defValue := Lean.KVMap.Value.toDataValue decl.defValue, group := decl.group, descr := decl.descr } pure { name := name, defValue := decl.defValue }

source

def Lean.Option.«commandRegister_builtin_option__:_:=_» :

Lean.ParserDescr

Equations

Lean.Option.«commandRegister_builtin_option__:_:=_» = Lean.ParserDescr.node `Lean.Option.«commandRegister_builtin_option__:_:=_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "register_builtin_option") (Lean.ParserDescr.const `ident)) (Lean.ParserDescr.symbol " : ")) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol " := ")) (Lean.ParserDescr.cat `term 0))

source

def Lean.Option.«commandRegister_option__:_:=_» :

Lean.ParserDescr

Equations

Lean.Option.«commandRegister_option__:_:=_» = Lean.ParserDescr.node `Lean.Option.«commandRegister_option__:_:=_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "register_option") (Lean.ParserDescr.const `ident)) (Lean.ParserDescr.symbol " : ")) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol " := ")) (Lean.ParserDescr.cat `term 0))