Documentation

Lean.Data.KVMap

inductive Lean.DataValue :

Value stored in a key-value map.

ofString (v : String) : DataValue
ofBool (v : Bool) : DataValue
ofName (v : Name) : DataValue
ofNat (v : Nat) : DataValue
ofInt (v : Int) : DataValue
ofSyntax (v : Syntax) : DataValue

Instances For

instance Lean.instInhabitedDataValue :

Inhabited DataValue

Equations

Lean.instInhabitedDataValue = { default := Lean.DataValue.ofString default }

instance Lean.instBEqDataValue :

Equations

Lean.instBEqDataValue = { beq := Lean.beqDataValue✝ }

instance Lean.instReprDataValue :

Equations

Lean.instReprDataValue = { reprPrec := Lean.reprDataValue✝ }

@[export lean_data_value_beq]

def Lean.DataValue.beqExp (a b : DataValue) :

Equations

a.beqExp b = (a == b)

@[export lean_mk_bool_data_value]

def Lean.mkBoolDataValueEx (b : Bool) :

Equations

Lean.mkBoolDataValueEx b = Lean.DataValue.ofBool b

@[export lean_data_value_bool]

def Lean.DataValue.getBoolEx :

DataValue → Bool

Equations

(Lean.DataValue.ofBool b).getBoolEx = b
x✝.getBoolEx = false

def Lean.DataValue.sameCtor :

DataValue → DataValue → Bool

Equations

(Lean.DataValue.ofString a).sameCtor (Lean.DataValue.ofString b) = true
(Lean.DataValue.ofBool a).sameCtor (Lean.DataValue.ofBool b) = true
(Lean.DataValue.ofName a).sameCtor (Lean.DataValue.ofName b) = true
(Lean.DataValue.ofNat a).sameCtor (Lean.DataValue.ofNat b) = true
(Lean.DataValue.ofInt a).sameCtor (Lean.DataValue.ofInt b) = true
(Lean.DataValue.ofSyntax a).sameCtor (Lean.DataValue.ofSyntax b) = true
x✝¹.sameCtor x✝ = false

@[export lean_data_value_to_string]

def Lean.DataValue.str :

DataValue → String

Equations

(Lean.DataValue.ofString a).str = a
(Lean.DataValue.ofBool a).str = toString a
(Lean.DataValue.ofName a).str = toString a
(Lean.DataValue.ofNat a).str = toString a
(Lean.DataValue.ofInt a).str = toString a
(Lean.DataValue.ofSyntax a).str = toString a

instance Lean.instToStringDataValue :

ToString DataValue

Equations

Lean.instToStringDataValue = { toString := Lean.DataValue.str }

instance Lean.instCoeStringDataValue :

Coe String DataValue

Equations

Lean.instCoeStringDataValue = { coe := Lean.DataValue.ofString }

instance Lean.instCoeBoolDataValue :

Coe Bool DataValue

Equations

Lean.instCoeBoolDataValue = { coe := Lean.DataValue.ofBool }

instance Lean.instCoeNameDataValue :

Coe Name DataValue

Equations

Lean.instCoeNameDataValue = { coe := Lean.DataValue.ofName }

instance Lean.instCoeNatDataValue :

Coe Nat DataValue

Equations

Lean.instCoeNatDataValue = { coe := Lean.DataValue.ofNat }

instance Lean.instCoeIntDataValue :

Coe Int DataValue

Equations

Lean.instCoeIntDataValue = { coe := Lean.DataValue.ofInt }

instance Lean.instCoeSyntaxDataValue :

Coe Syntax DataValue

Equations

Lean.instCoeSyntaxDataValue = { coe := Lean.DataValue.ofSyntax }

structure Lean.KVMap :

A key-value map. We use it to represent user-selected options and Expr.mdata.

Remark: we do not use RBMap here because we need to manipulate KVMap objects in C++ and RBMap is implemented in Lean. So, we use just a List until we can generate C++ code from Lean code.

entries : List (Name × DataValue)

Instances For

instance Lean.instInhabitedKVMap :

Inhabited KVMap

Equations

Lean.instInhabitedKVMap = { default := { entries := default } }

instance Lean.instReprKVMap :

Equations

Lean.instReprKVMap = { reprPrec := Lean.reprKVMap✝ }

instance Lean.KVMap.instToString :

Equations

Lean.KVMap.instToString = { toString := fun (m : Lean.KVMap) => toString m.entries }

def Lean.KVMap.empty :

Equations

Lean.KVMap.empty = { entries := [] }

def Lean.KVMap.isEmpty :

Equations

{ entries := m }.isEmpty = m.isEmpty

def Lean.KVMap.size (m : KVMap) :

Equations

m.size = m.entries.length

def Lean.KVMap.findCore :

List (Name × DataValue) → Name → Option DataValue

Equations

Lean.KVMap.findCore [] x✝ = none
Lean.KVMap.findCore ((k, v) :: m) x✝ = if (k == x✝) = true then some v else Lean.KVMap.findCore m x✝

def Lean.KVMap.find :

KVMap → Name → Option DataValue

Equations

{ entries := m }.find x✝ = Lean.KVMap.findCore m x✝

def Lean.KVMap.findD (m : KVMap) (k : Name) (d₀ : DataValue) :

Equations

m.findD k d₀ = (m.find k).getD d₀

def Lean.KVMap.insertCore :

List (Name × DataValue) → Name → DataValue → List (Name × DataValue)

Equations

Lean.KVMap.insertCore [] x✝¹ x✝ = [(x✝¹, x✝)]
Lean.KVMap.insertCore ((k, v) :: m) x✝¹ x✝ = if (k == x✝¹) = true then (k, x✝) :: m else (k, v) :: Lean.KVMap.insertCore m x✝¹ x✝

def Lean.KVMap.insert :

KVMap → Name → DataValue → KVMap

Equations

{ entries := m }.insert x✝¹ x✝ = { entries := Lean.KVMap.insertCore m x✝¹ x✝ }

def Lean.KVMap.contains (m : KVMap) (n : Name) :

Equations

m.contains n = (m.find n).isSome

def Lean.KVMap.erase :

KVMap → Name → KVMap

Erase an entry from the map

Equations

{ entries := m }.erase x✝ = { entries := List.filter (fun (a : Lean.Name × Lean.DataValue) => decide (a.fst ≠ x✝)) m }

def Lean.KVMap.getString (m : KVMap) (k : Name) (defVal : String := "") :

Equations

m.getString k defVal = match m.find k with | some (Lean.DataValue.ofString v) => v | x => defVal

def Lean.KVMap.getNat (m : KVMap) (k : Name) (defVal : Nat := 0) :

Equations

m.getNat k defVal = match m.find k with | some (Lean.DataValue.ofNat v) => v | x => defVal

def Lean.KVMap.getInt (m : KVMap) (k : Name) (defVal : Int := 0) :

Equations

m.getInt k defVal = match m.find k with | some (Lean.DataValue.ofInt v) => v | x => defVal

def Lean.KVMap.getBool (m : KVMap) (k : Name) (defVal : Bool := false) :

Equations

m.getBool k defVal = match m.find k with | some (Lean.DataValue.ofBool v) => v | x => defVal

def Lean.KVMap.getName (m : KVMap) (k : Name) (defVal : Name := Name.anonymous) :

Equations

m.getName k defVal = match m.find k with | some (Lean.DataValue.ofName v) => v | x => defVal

def Lean.KVMap.getSyntax (m : KVMap) (k : Name) (defVal : Syntax := Syntax.missing) :

Equations

m.getSyntax k defVal = match m.find k with | some (Lean.DataValue.ofSyntax v) => v | x => defVal

def Lean.KVMap.setString (m : KVMap) (k : Name) (v : String) :

Equations

m.setString k v = m.insert k (Lean.DataValue.ofString v)

def Lean.KVMap.setNat (m : KVMap) (k : Name) (v : Nat) :

Equations

m.setNat k v = m.insert k (Lean.DataValue.ofNat v)

def Lean.KVMap.setInt (m : KVMap) (k : Name) (v : Int) :

Equations

m.setInt k v = m.insert k (Lean.DataValue.ofInt v)

def Lean.KVMap.setBool (m : KVMap) (k : Name) (v : Bool) :

Equations

m.setBool k v = m.insert k (Lean.DataValue.ofBool v)

def Lean.KVMap.setName (m : KVMap) (k v : Name) :

Equations

m.setName k v = m.insert k (Lean.DataValue.ofName v)

def Lean.KVMap.setSyntax (m : KVMap) (k : Name) (v : Syntax) :

Equations

m.setSyntax k v = m.insert k (Lean.DataValue.ofSyntax v)

def Lean.KVMap.updateString (m : KVMap) (k : Name) (f : String → String) :

Update a String entry based on its current value.

Equations

m.updateString k f = m.insert k (Lean.DataValue.ofString (f (m.getString k)))

def Lean.KVMap.updateNat (m : KVMap) (k : Name) (f : Nat → Nat) :

Update a Nat entry based on its current value.

Equations

m.updateNat k f = m.insert k (Lean.DataValue.ofNat (f (m.getNat k)))

def Lean.KVMap.updateInt (m : KVMap) (k : Name) (f : Int → Int) :

Update an Int entry based on its current value.

Equations

m.updateInt k f = m.insert k (Lean.DataValue.ofInt (f (m.getInt k)))

def Lean.KVMap.updateBool (m : KVMap) (k : Name) (f : Bool → Bool) :

Update a Bool entry based on its current value.

Equations

m.updateBool k f = m.insert k (Lean.DataValue.ofBool (f (m.getBool k)))

def Lean.KVMap.updateName (m : KVMap) (k : Name) (f : Name → Name) :

Update a Name entry based on its current value.

Equations

m.updateName k f = m.insert k (Lean.DataValue.ofName (f (m.getName k)))

def Lean.KVMap.updateSyntax (m : KVMap) (k : Name) (f : Syntax → Syntax) :

Update a Syntax entry based on its current value.

Equations

m.updateSyntax k f = m.insert k (Lean.DataValue.ofSyntax (f (m.getSyntax k)))

@[inline]

def Lean.KVMap.forIn {δ : Type w} {m : Type w → Type w'} [Monad m] (kv : KVMap) (init : δ) (f : Name × DataValue → δ → m (ForInStep δ)) :

m δ

Equations

kv.forIn init f = forIn kv.entries init f

instance Lean.KVMap.instForInProdNameDataValue {m : Type u_1 → Type u_2} :

ForIn m KVMap (Name × DataValue)

Equations

Lean.KVMap.instForInProdNameDataValue = { forIn := fun {β : Type ?u.14} [Monad m] => Lean.KVMap.forIn }

def Lean.KVMap.subsetAux :

List (Name × DataValue) → KVMap → Bool

Equations

Lean.KVMap.subsetAux [] x✝ = true
Lean.KVMap.subsetAux ((k, v₁) :: m₁) x✝ = match x✝.find k with | some v₂ => v₁ == v₂ && Lean.KVMap.subsetAux m₁ x✝ | none => false

def Lean.KVMap.subset :

KVMap → KVMap → Bool

Equations

{ entries := m₁ }.subset x✝ = Lean.KVMap.subsetAux m₁ x✝

def Lean.KVMap.mergeBy (mergeFn : Name → DataValue → DataValue → DataValue) (l r : KVMap) :

Equations

One or more equations did not get rendered due to their size.

def Lean.KVMap.eqv (m₁ m₂ : KVMap) :

Equations

m₁.eqv m₂ = (m₁.subset m₂ && m₂.subset m₁)

instance Lean.KVMap.instBEq :

Equations

Lean.KVMap.instBEq = { beq := Lean.KVMap.eqv }

class Lean.KVMap.Value (α : Type) :

toDataValue : α → DataValue
ofDataValue? : DataValue → Option α

Instances

@[inline]

def Lean.KVMap.get? {α : Type} [Value α] (m : KVMap) (k : Name) :

Equations

m.get? k = (m.find k).bind Lean.KVMap.Value.ofDataValue?

@[inline]

def Lean.KVMap.get {α : Type} [Value α] (m : KVMap) (k : Name) (defVal : α) :

α

Equations

m.get k defVal = (m.get? k).getD defVal

@[inline]

def Lean.KVMap.set {α : Type} [Value α] (m : KVMap) (k : Name) (v : α) :

Equations

m.set k v = m.insert k (Lean.KVMap.Value.toDataValue v)

@[inline]

def Lean.KVMap.update {α : Type} [Value α] (m : KVMap) (k : Name) (f : Option α → Option α) :

Equations

m.update k f = match f (m.get? k) with | some a => m.set k a | none => m.erase k

instance Lean.KVMap.instValueDataValue :

Value DataValue

Equations

Lean.KVMap.instValueDataValue = { toDataValue := id, ofDataValue? := some }

instance Lean.KVMap.instValueBool :

Equations

Lean.KVMap.instValueBool = { toDataValue := Lean.DataValue.ofBool, ofDataValue? := fun (x : Lean.DataValue) => match x with | Lean.DataValue.ofBool b => some b | x => none }

instance Lean.KVMap.instValueNat :

Equations

Lean.KVMap.instValueNat = { toDataValue := Lean.DataValue.ofNat, ofDataValue? := fun (x : Lean.DataValue) => match x with | Lean.DataValue.ofNat n => some n | x => none }

instance Lean.KVMap.instValueInt :

Equations

Lean.KVMap.instValueInt = { toDataValue := Lean.DataValue.ofInt, ofDataValue? := fun (x : Lean.DataValue) => match x with | Lean.DataValue.ofInt i => some i | x => none }

instance Lean.KVMap.instValueName :

Equations

Lean.KVMap.instValueName = { toDataValue := Lean.DataValue.ofName, ofDataValue? := fun (x : Lean.DataValue) => match x with | Lean.DataValue.ofName n => some n | x => none }

instance Lean.KVMap.instValueString :

Equations

One or more equations did not get rendered due to their size.

instance Lean.KVMap.instValueSyntax :

Equations

One or more equations did not get rendered due to their size.