src/MemTable.bend fails

type Entry source · line 10 · raw

Data

• Entry

  @key:String -> @val:Maybe<&2, String> -> Entry

type MemTable source · line 13 · raw

Data

• MT

  @entries:List<&2, Entry> -> MemTable

def empty source · line 16 · raw

MemTable

def put source · line 19 · raw

@t:MemTable -> @k:String -> @v:String -> MemTable

def del source · line 24 · raw

@t:MemTable -> @k:String -> MemTable

def count source · line 29 · raw

@t:MemTable -> Nat

def scan_step source · line 37 · raw

@done:Bool -> @eq:Bool -> @hv:Maybe<&2, String> -> @ans:Maybe<&2, String> -> Pair(Bool, Maybe<&2, String>)

def scan_go source · line 48 · raw

@fuel:Nat -> @+k:String -> @st:Pair(Bool, Maybe<&2, String>) -> @entries:List<&2, Entry> -> Maybe<&2, String>

def get source · line 61 · raw

@t:MemTable -> @+k:String -> Maybe<&2, String>

def frozen_lemma source · line 67 · raw

@fuel:Nat -> @k:String -> @ans:Maybe<&2, String> -> @entries:List<&2, Entry> -> {scan_go(fuel, k, (True{}, ans), entries) == ans : Maybe<&2, String>}

def ryw_core source · line 80 · raw

@+entries:List<&2, Entry> -> @+k:String -> @v:String -> {scan_go(List.length(&2, Entry, Entry{k, Some{v}} <> entries), k, (False{}, None{}), Entry{k, Some{v}} <> entries) == Some{v} : Maybe<&2, String>}

def ryw_bridge source · line 85 · raw

@t:MemTable -> @+k:String -> @+v:String -> {get(put(t, k, v), k) == Some{v} : Maybe<&2, String>}

def del_core source · line 91 · raw

@+entries:List<&2, Entry> -> @+k:String -> {scan_go(List.length(&2, Entry, Entry{k, None{}} <> entries), k, (False{}, None{}), Entry{k, None{}} <> entries) == None{} : Maybe<&2, String>}

def del_bridge source · line 96 · raw

@t:MemTable -> @+k:String -> @v:String -> {get(del(put(t, k, v), k), k) == None{} : Maybe<&2, String>}