## Ref maintenance notes: Internal data structures

# Representation of logical formulae/terms

Syntax trees. All logical expressions input to Ref's inference routines are syntax trees produced by the SETL parser (invoked directly from within Ref's code). Such trees may be converted into objects of a different nature, for specific needs of the various inference mechanism; nevertheless, formulae and terms are always submitted in that form to the logical or algebraic manipulation routines which must hence perform recursive walks through them in order to exploit them directly or in order to convert them into different representations. The tags that may appear on the nodes of a syntax tree are discussed in [Click].

Restrictions to the SETL syntax. Virtually every SETL expression also belongs to the realm of Ref (not SETL instructions, although Ref's definitions bear, in their concrete external syntax, a resemblance with them). Two exceptions must be noted: Ref lacks

- tuples, save in the form of ordered pairs whose components are both defined: hence neither enumerated tuples with just one, or more than two components, nor tuple-formers involving iterators, are handled by Ref;

- multi-applications of the forms

      :
      f(E1)...(En),
      f(E1,...,En),

  with n greater than 1;

- OM, the constant representing the undefined value---actually, this may (very seldom) appear on the right-hand side of an iterator, such as in

      (FORALL x in OM | P(x)),

  but when it does it is meant to represent the universal class, so that e.g. the previous formula can be rewritten more simply as

      (FORALL x | P(x)).

Node tags. A syntax tree is represented in the form of a nested tuple, where nesting reflects the descent into subtrees. The first component of each tuple is a string tag encoding the lead operator of the expression represented by that tuple.

[TO BE COMPLETED]

# Salient global variables