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;

Types

%ord.Key

This is existential type specifies a type and 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

Create 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

Create 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

Get number of elements in 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 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

Get value from key in map.

Todo

Use Option as return type once we have proper union types.

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

%ord.contains

Does the container conain 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

Insert key / key-value-pair into 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;