Open MikaelMayer opened 1 year ago
Here is sample code that could be integrated, need to test if it's fast enough and relevant.
datatype Option<W> = None | Some(value: W) function MapWithFailure<U, V, W>(oldmap: map<U, V>, f: V -> Option<W>): (result: Option<map<U, W>>) { if forall k <- oldmap :: f(oldmap[k]).Some? then Some(map k <- oldmap :: k := f(oldmap[k]).value) else None } by method { var keySet := oldmap.Keys; ghost var keySetcomplement := {}; var tmp := map[]; while |keySet| > 0 invariant keySet !! keySetcomplement invariant keySet + keySetcomplement == oldmap.Keys invariant forall k <- keySetcomplement :: f(oldmap[k]).Some? invariant Some(tmp) == MapWithFailure(map k <- oldmap | k in keySetcomplement :: k := oldmap[k], f) { var x :| x in keySet; keySet := keySet - {x}; var t := f(oldmap[x]); if t.None? { return None; } ghost var oldTmp := tmp; tmp := tmp[x := t.value]; calc { tmp; oldTmp[x := t.value]; MapWithFailure(map k <- oldmap | k in keySetcomplement :: k := oldmap[k], f).value[x := t.value]; MapWithFailure(map k <- oldmap | k in keySetcomplement + {x} :: k := oldmap[k], f).value; } keySetcomplement := keySetcomplement + {x}; } result := Some(tmp); assert keySetcomplement == oldmap.Keys; assert oldmap == map k <- oldmap | k in keySetcomplement :: k := oldmap[k]; }
Here is sample code that could be integrated, need to test if it's fast enough and relevant.