Dictionaries

Author(s): The CLIP Group.

This module provides predicates for implementing dictionaries. Such dictionaries are currently implemented as ordered binary trees of key-value pairs.

Usage and interface

Documentation on exports

REGTYPE

Usage: dictionary(D)

  • Description: D is a dictionary.

PREDICATE

Usage: dictionary(D,K,V,L,R)

  • Description: The dictionary node D has key K, value V, left child L, and right child R.
  • The following properties should hold upon exit:
    (dict:non_empty_dictionary/1)D is a non-empty dictionary.

PREDICATE

Usage: dic_node(D,N)

  • Description: N is a sub-dictionary of D.
  • The following properties should hold at call time:
    (dict:non_empty_dictionary/1)D is a non-empty dictionary.
  • The following properties should hold upon exit:
    (dict:dictionary/1)N is a dictionary.

PREDICATE

Usage: dic_lookup(D,K,V)

  • Description: D contains value V at key K. If it was not already in D it is added.
  • The following properties should hold upon exit:
    (dict:non_empty_dictionary/1)D is a non-empty dictionary.

PREDICATE

Usage: dic_lookup(D,K,V,O)

  • Description: Same as dic_lookup(D,K,V). O indicates if it was already in D (old) or not (new).
  • The following properties should hold upon exit:
    (dict:non_empty_dictionary/1)D is a non-empty dictionary.
    (dict:old_or_new/1)dict:old_or_new(O)

PREDICATE

Usage: dic_get(D,K,V)

  • Description: D contains value V at key K. Fails if it is not already in D.
  • The following properties should hold at call time:
    (term_typing:nonvar/1)D is currently a term which is not a free variable.
    (dict:dictionary/1)D is a dictionary.
  • The following properties should hold upon exit:
    (dict:non_empty_dictionary/1)D is a non-empty dictionary.

PREDICATE

Usage: dic_replace(D,K,V,D1)

  • Description: D and D1 are identical except for the element at key K, which in D1 contains value V, whatever has (or whether it is) in D.
  • The following properties should hold at call time:
    (dict:dictionary/1)D is a dictionary.
    (dict:dictionary/1)D1 is a dictionary.
  • The following properties should hold upon exit:
    (dict:dictionary/1)D is a dictionary.
    (dict:dictionary/1)D1 is a dictionary.

REGTYPE
A regular type, defined as follows:
old_or_new(old).
old_or_new(new).

REGTYPE

Usage: non_empty_dictionary(D)

  • Description: D is a non-empty dictionary.

Known bugs and planned improvements

  • Run-time checks have been reported not to work with this code. That means that either the assertions here, or the code that implements the run-time checks are erroneous.