Forlan Manual


The Tab Module


Synopsis

signature TAB
structure Tab :> TAB

This module defines an abstract type of finite tables (maps).


Interface

type ('a,'btab
val lookup : 'a Sort.total_ordering -> ('a'b) tab * 'a -> 'b option
val isEmpty : ('a'b) tab -> bool
val empty : ('a'b) tab
val update : 'a Sort.total_ordering -> ('a'b) tab * ('a * 'b) list -> ('a'b) tab
val domain : 'a Sort.total_ordering -> ('a'b) tab -> 'a Set.set
val toList : ('a'b) tab -> ('a * 'b) list
val fromList : 'a Sort.total_ordering -> ('a * 'b) list -> ('a'b) tab

Description

type ('a,'b) tab
A finite table (map) sending inputs of type 'a to outputs of type 'b. A table of type ('a, 'b)tab can be understood as consisting of a finite set of bindings (x, y), for a value x of type 'a and a value y of type 'b, where, for a given value x, there is at most one binding with a left-hand side of x.

The module's values are specified with the help of the abstract proposition saying that a value tab of type ('a, 'b)tab is compatible with a value cmp of type 'a Sort.total_ordering.

lookup cmp (tab, x)
Informally, if tab is compatible with cmp, then lookup returns NONE, if tab doesn't contain a binding whose left-hand side is x, and lookup returns SOME y, if tab contains the binding (x, y). Formally, the meaning of lookup must be understood in relation to the specifications of the other values of the module.

isEmpty tab
If tab is compatible with a value cmp of type 'a Sort.total_ordering, then isEmpty tests whether tab is the table with no bindings, i.e., whether lookup cmp (tab, x) = NONE, for all values x of type 'a.

empty
If cmp is a value of type 'a Sort.total_ordering, then empty is the table that is compatible with cmp and has no bindings, i.e., the table tab such that lookup cmp (tab, x) = NONE, for all values x of type 'a.

update cmp (tab, xs)
If tab is compatible with cmp, then update returns a table that is compatible with cmp and consists of the union of the bindings of tab whose left-hand sides don't appear as left-hand sides in xs, and the bindings of xs whose left-hand sides don't appear as left-hand sides in subsequent bindings of xs, i.e., the table tab' that is compatible with cmp and such that, for all values x of type 'a:

domain cmp tab
If tab is compatible with cmp, then domain returns the set that is compatible with cmp and consists of the left-hand sides of the bindings of tab, i.e., the set xs such that, for all values x of type 'a, Set.memb cmp (xs, x) iff lookup cmp (tab, x) is not NONE.

toList tab
If tab is compatible with a value cmp of type 'a Sort.total_ordering, then toList returns the list of bindings of tab, ordered according to their left-hand sides using cmp, i.e., the list xs such that:

fromList cmp xs
returns update cmp (empty, xs).


[ Top | Parent | Root | Contents | Index ]

Forlan Version 4.12
Copyright © 2019 Alley Stoughton