Documentation

Lean.Data.KVMap

inductive Lean.DataValue :

Value stored in a key-value map.

ofString: String → Lean.DataValue
ofBool: Bool → Lean.DataValue
ofName: Lake.Name → Lean.DataValue
ofNat: Nat → Lean.DataValue
ofInt: Int → Lean.DataValue
ofSyntax: Lean.Syntax → Lean.DataValue

Instances For

instance Lean.instInhabitedDataValue :

Inhabited Lean.DataValue

Equations

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

instance Lean.instBEqDataValue :

BEq Lean.DataValue

Equations

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

instance Lean.instReprDataValue :

Repr Lean.DataValue

Equations

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

@[export lean_data_value_beq]

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

Equations

Lean.DataValue.beqExp a 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 :

Lean.DataValue → Bool

Equations

Lean.DataValue.getBoolEx x = match x with | Lean.DataValue.ofBool b => b | x => false

def Lean.DataValue.sameCtor :

Lean.DataValue → Lean.DataValue → Bool

Equations

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

@[export lean_data_value_to_string]

def Lean.DataValue.str :

Lean.DataValue → String

Equations

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

instance Lean.instToStringDataValue :

ToString Lean.DataValue

Equations

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

instance Lean.instCoeStringDataValue :

Coe String Lean.DataValue

Equations

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

instance Lean.instCoeBoolDataValue :

Coe Bool Lean.DataValue

Equations

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

instance Lean.instCoeNameDataValue :

Coe Lake.Name Lean.DataValue

Equations

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

instance Lean.instCoeNatDataValue :

Coe Nat Lean.DataValue

Equations

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

instance Lean.instCoeIntDataValue :

Coe Int Lean.DataValue

Equations

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

instance Lean.instCoeSyntaxDataValue :

Coe Lean.Syntax Lean.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 (Lake.Name × Lean.DataValue)

Instances For

instance Lean.instInhabitedKVMap :

Inhabited Lean.KVMap

Equations

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

instance Lean.instReprKVMap :

Repr Lean.KVMap

Equations

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

instance Lean.KVMap.instToStringKVMap :

ToString Lean.KVMap

Equations

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

def Lean.KVMap.empty :

Equations

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

def Lean.KVMap.isEmpty :

Lean.KVMap → Bool

Equations

Lean.KVMap.isEmpty x = match x with | { entries := m } => List.isEmpty m

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

Equations

Lean.KVMap.size m = List.length m.entries

def Lean.KVMap.findCore :

List (Lake.Name × Lean.DataValue) → Lake.Name → Option Lean.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 :

Lean.KVMap → Lake.Name → Option Lean.DataValue

Equations

Lean.KVMap.find x✝ x = match x✝, x with | { entries := m }, k => Lean.KVMap.findCore m k

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

Equations

Lean.KVMap.findD m k d₀ = Option.getD (Lean.KVMap.find m k) d₀

def Lean.KVMap.insertCore :

List (Lake.Name × Lean.DataValue) → Lake.Name → Lean.DataValue → List (Lake.Name × Lean.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 :

Lean.KVMap → Lake.Name → Lean.DataValue → Lean.KVMap

Equations

Lean.KVMap.insert x✝¹ x✝ x = match x✝¹, x✝, x with | { entries := m }, k, v => { entries := Lean.KVMap.insertCore m k v }

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

Equations

Lean.KVMap.contains m n = Option.isSome (Lean.KVMap.find m n)

def Lean.KVMap.erase :

Lean.KVMap → Lake.Name → Lean.KVMap

Erase an entry from the map

Equations

Lean.KVMap.erase x✝ x = match x✝, x with | { entries := m }, k => { entries := List.filter (fun (a : Lake.Name × Lean.DataValue) => decide (a.fst ≠ k)) m }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Update a String entry based on its current value.

Equations

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

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

Update a Nat entry based on its current value.

Equations

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

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

Update an Int entry based on its current value.

Equations

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

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

Update a Bool entry based on its current value.

Equations

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

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

Update a Name entry based on its current value.

Equations

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

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

Update a Syntax entry based on its current value.

Equations

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

@[inline]

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

m δ

Equations

Lean.KVMap.forIn kv init f = List.forIn kv.entries init f

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

ForIn m Lean.KVMap (Lake.Name × Lean.DataValue)

Equations

Lean.KVMap.instForInKVMapProdNameDataValue = { forIn := fun {β : Type u_1} [Monad m] => Lean.KVMap.forIn }

def Lean.KVMap.subsetAux :

List (Lake.Name × Lean.DataValue) → Lean.KVMap → Bool

Equations

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

def Lean.KVMap.subset :

Lean.KVMap → Lean.KVMap → Bool

Equations

Lean.KVMap.subset x✝ x = match x✝, x with | { entries := m₁ }, m₂ => Lean.KVMap.subsetAux m₁ m₂

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

Equations

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

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

Equations

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

instance Lean.KVMap.instBEqKVMap :

Equations

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

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

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

Instances

@[inline]

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

Equations

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

@[inline]

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

α

Equations

Lean.KVMap.get m k defVal = Option.getD (Lean.KVMap.get? m k) defVal

@[inline]

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

Equations

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

@[inline]

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

Equations

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

instance Lean.KVMap.instValueDataValue :

Lean.KVMap.Value Lean.DataValue

Equations

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

instance Lean.KVMap.instValueBool :

Lean.KVMap.Value Bool

Equations

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

instance Lean.KVMap.instValueNat :

Lean.KVMap.Value Nat

Equations

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

instance Lean.KVMap.instValueInt :

Lean.KVMap.Value Int

Equations

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

instance Lean.KVMap.instValueName :

Lean.KVMap.Value Lake.Name

Equations

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

instance Lean.KVMap.instValueString :

Lean.KVMap.Value String

Equations

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

instance Lean.KVMap.instValueSyntax :

Lean.KVMap.Value Lean.Syntax

Equations

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