1  contract Maps =
  2  
  3    record pt    = {x : int, y : int}
  4    record state = { map_i : map(int, pt),
  5                     map_s : map(string, pt) }
  6  
  7    function init() = { map_i = {}, map_s = {} }
  8  
  9    function get_state() = state
 10  
 11    // {[k] = v}
 12    function map_i() =
 13      { [1] = {x = 1, y = 2},
 14        [2] = {x = 3, y = 4},
 15        [3] = {x = 5, y = 6} }
 16    function map_s() =
 17      { ["one"]   = {x = 1, y = 2},
 18        ["two"]   = {x = 3, y = 4},
 19        ["three"] = {x = 5, y = 6} }
 20    stateful function map_state_i() = put(state{ map_i = map_i() })
 21    stateful function map_state_s() = put(state{ map_s = map_s() })
 22  
 23    // m[k]
 24    function get_i(k, m : map(int,    pt)) = m[k]
 25    function get_s(k, m : map(string, pt)) = m[k]
 26    function get_state_i(k) = get_i(k, state.map_i)
 27    function get_state_s(k) = get_s(k, state.map_s)
 28  
 29    // m[k = v]
 30    function get_def_i(k, v, m : map(int,    pt)) = m[k = v]
 31    function get_def_s(k, v, m : map(string, pt)) = m[k = v]
 32    function get_def_state_i(k, v) = get_def_i(k, v, state.map_i)
 33    function get_def_state_s(k, v) = get_def_s(k, v, state.map_s)
 34  
 35    // m{[k] = v}
 36    function set_i(k, p, m : map(int,    pt)) = m{ [k] = p }
 37    function set_s(k, p, m : map(string, pt)) = m{ [k] = p }
 38    stateful function set_state_i(k, p) = put(state{ map_i = set_i(k, p, state.map_i) })
 39    stateful function set_state_s(k, p) = put(state{ map_s = set_s(k, p, state.map_s) })
 40  
 41    // m{f[k].x = v}
 42    function setx_i(k, x, m : map(int,    pt)) = m{ [k].x = x }
 43    function setx_s(k, x, m : map(string, pt)) = m{ [k].x = x }
 44    stateful function setx_state_i(k, x) = put(state{ map_i[k].x = x })
 45    stateful function setx_state_s(k, x) = put(state{ map_s[k].x = x })
 46  
 47    // m{[k] @ x = v }
 48    function addx_i(k, d, m : map(int,    pt)) = m{ [k].x @ x = x + d }
 49    function addx_s(k, d, m : map(string, pt)) = m{ [k].x @ x = x + d }
 50    stateful function addx_state_i(k, d) = put(state{ map_i[k].x @ x = x + d })
 51    stateful function addx_state_s(k, d) = put(state{ map_s[k].x @ x = x + d })
 52  
 53    // m{[k = def] @ x = v }
 54    function addx_def_i(k, v, d, m : map(int,    pt)) = m{ [k = v].x @ x = x + d }
 55    function addx_def_s(k, v, d, m : map(string, pt)) = m{ [k = v].x @ x = x + d }
 56  
 57    // Map.member
 58    function member_i(k, m : map(int,    pt)) = Map.member(k, m)
 59    function member_s(k, m : map(string, pt)) = Map.member(k, m)
 60    function member_state_i(k) = member_i(k, state.map_i)
 61    function member_state_s(k) = member_s(k, state.map_s)
 62  
 63    // Map.lookup
 64    function lookup_i(k, m : map(int,    pt)) = Map.lookup(k, m)
 65    function lookup_s(k, m : map(string, pt)) = Map.lookup(k, m)
 66    function lookup_state_i(k) = lookup_i(k, state.map_i)
 67    function lookup_state_s(k) = lookup_s(k, state.map_s)
 68  
 69    // Map.lookup_default
 70    function lookup_def_i(k, m : map(int,    pt), def : pt) =
 71      Map.lookup_default(k, m, def)
 72    function lookup_def_s(k, m : map(string, pt), def : pt) =
 73      Map.lookup_default(k, m, def)
 74    function lookup_def_state_i(k, def) = lookup_def_i(k, state.map_i, def)
 75    function lookup_def_state_s(k, def) = lookup_def_s(k, state.map_s, def)
 76  
 77    // Map.delete
 78    function delete_i(k, m : map(int,    pt)) = Map.delete(k, m)
 79    function delete_s(k, m : map(string, pt)) = Map.delete(k, m)
 80    stateful function delete_state_i(k) = put(state{ map_i = delete_i(k, state.map_i) })
 81    stateful function delete_state_s(k) = put(state{ map_s = delete_s(k, state.map_s) })
 82  
 83    // Map.size
 84    function size_i(m : map(int,    pt)) = Map.size(m)
 85    function size_s(m : map(string, pt)) = Map.size(m)
 86    function size_state_i() = size_i(state.map_i)
 87    function size_state_s() = size_s(state.map_s)
 88  
 89    // Map.to_list
 90    function tolist_i(m : map(int,    pt)) = Map.to_list(m)
 91    function tolist_s(m : map(string, pt)) = Map.to_list(m)
 92    function tolist_state_i() = tolist_i(state.map_i)
 93    function tolist_state_s() = tolist_s(state.map_s)
 94  
 95    // Map.from_list
 96    function fromlist_i(xs : list((int,    pt))) = Map.from_list(xs)
 97    function fromlist_s(xs : list((string, pt))) = Map.from_list(xs)
 98    stateful function fromlist_state_i(xs) = put(state{ map_i = fromlist_i(xs) })
 99    stateful function fromlist_state_s(xs) = put(state{ map_s = fromlist_s(xs) })
100