The ord Plugin

Table of Contents

• Dependencies
• Types
  • %ord.Key
  • %ord.Set / %ord.Map
• Constructors
  • %ord.init
  • %ord.create
• Capacity
  • %ord.size
  • %ord.is_empty
• Lookup
  • %ord.get
  • %ord.contains
• Modifiers
  • %ord.insert

See also

mim::plug::ord

Ordered Set and Map.

Warning

This is still WIP!

Dependencies

plugin core;
plugin option;

Types

%ord.Key

This existential-style type specifies a type together with a less-than function.

let %ord.Key = [T: *, lt: [T, T] → Bool];

%ord.Set / %ord.Map

Type constructors for set / map.

• First argument must be of type %ord.Key.
• %ord.Map needs a second argument: the value type.

axm %ord.Set: %ord.Key     → *;
axm %ord.Map: %ord.Key → * → *;

Constructors

%ord.init

Creates a set / map from a list of values / key-value pairs.

axm %ord.init(set): [K: %ord.Key] →          {n: Nat} → «n;  K#T    » → %ord.Set K  , normalize_init;
axm %ord.init(map): [K: %ord.Key] → {V: *} → {n: Nat} → «n; [K#T, V]» → %ord.Map K V, normalize_init;

%ord.create

Creates an empty set / map.

lam %ord.create_set [K: %ord.Key]        : %ord.Set K   = %ord.init.set K    @0 ();
lam %ord.create_map [K: %ord.Key] (V: *) : %ord.Map K V = %ord.init.map K @V @0 ();

Capacity

%ord.size

Yields the number of elements in the container.

axm %ord.size(set): {K: %ord.Key} →          %ord.Set K   → Nat, normalize_size;
axm %ord.size(map): {K: %ord.Key} → {V: *} → %ord.Map K V → Nat, normalize_size;

%ord.is_empty

Is the container empty?

lam %ord.is_empty_set {K: %ord.Key}        (set: %ord.Set K  ): Bool = %core.ncmp.e (%ord.size.set set, 0);
lam %ord.is_empty_map {K: %ord.Key} {V: *} (map: %ord.Map K V): Bool = %core.ncmp.e (%ord.size.map map, 0);

Lookup

%ord.get

Looks up the given key in the map. Returns an optional value (%option.Opt V).

axm %ord.get: {K: %ord.Key} → {V: *} → [%ord.Map K V, K#T] → %option.Opt V, normalize_get;

%ord.contains

Does the container contain the given key?

axm %ord.contains(set): {K: %ord.Key} →          [%ord.Set K  , K#T] → Bool, normalize_contains;
axm %ord.contains(map): {K: %ord.Key} → {V: *} → [%ord.Map K V, K#T] → Bool, normalize_contains;

Modifiers

%ord.insert

Inserts a key / key-value pair into the container.

axm %ord.insert(set): {K: %ord.Key} →          [%ord.Set K  ,  K#T    ] → %ord.Set K  , normalize_insert;
axm %ord.insert(map): {K: %ord.Key} → {V: *} → [%ord.Map K V, [K#T, V]] → %ord.Map K V, normalize_insert;