Next: The Rules Up: System Description Previous: Invoking Transformation Tactics

Definitions and Definition Objects

In text is used to represent proof rules, theorem goals and and ML tactic bodies. This text is made up of characters and calls to text macros. Since internally pieces of text are stored as trees of characters and macro references, they are also called text trees or T-trees .

Text macros are used mainly to improve the readability of terms and formulas. For example, since there is no relation built into , a formula like might be represented by ((x<y) -> void). Instead of always doing this translation one may define

        <x>>=<y>==((<x><<y>) -> void)

and then use x>=y instead of ((x<y) -> void), thereby effectively adding

as a new relation. (Note that for the definition to be used it must be instantiated (see section 4 above) --- one cannot just type `` x>=y''.) Since most macros are used to extend the notation available for terms and formulas, they are also known as definitions, or defs, and the library objects that contain them are called definition objects.

The left--hand side of a definition specifies its formal parameters and also shows how to display a call to it. The right--hand side shows what the definition stands for. In the example above the two formal parameters are <x> and <y>. (Formal parameters are always specified between angle brackets.)

The left--hand side of definitions should contain zero or more formal parameters plus whatever other characters one wants displayed. For instance,

        <x> greater than or equal to <y>
        (ge <x> <y>)
        <x>>=<y>

are all perfectly valid left--hand sides. A formal parameter is an identifier enclosed in angle brackets or an

enclosed in angle brackets, where a description is a piece of text that does not include an unescaped >. (The escape mechanism is explained below.) After the def object has been checked the description is used to help display the object in the library window, as

is inserted in place of the formal parameter. For example, given the following def of GE,

        <x:int1>>=<y:int2>==((<x><<y>) -> void)

the library window would show the following:

,-------------------------------------------------------,
| Library                                               |
|-------------------------------------------------------|
| * GE                                                  |
|   DEF: <int1>>=<int2>                                 |
|                                                       |
'-------------------------------------------------------'

If the description is omitted or void, the empty string is used, so that formal parameter is displayed as `` <>''.

Sometimes one wishes to use > and > as something other than angle brackets on the left--hand side of definitions. Backslash is used to suppress the normal meanings of < and >. To keep a < from being part of a formal parameter or to make a > part of a description, precede it with a backslash, as in

        <x>\<=<y>==((<y><<x>) -> void)

and

        square root(<x: any int\>0 >)== ... .

To get a backslash on the left--hand side, escape it with another backslash:

        <x>\\ 

The right--hand side of a definition shows what the definition stands for.
Besides arbitrary characters it can contain formal references to the parameters
(identifiers enclosed in angle brackets) and uses of checked defs.
(Note: defs may not refer to each other recursively.)
Every formal reference must be to a parameter defined on the left--hand side;
no nonlocal references are allowed.

Here is an example of a def that uses another def:
        <x>>=<y>>=<z>==<x>>=<y> & <y>>=<z>.

An example of a use of this def is  3>=2>=1, which expands ultimately
into  ((3<2) -> void) & ((2<1) -> void).
Blanks are  very significant on the right--hand sides of defs;
the three characters  <x> are considered to be a formal reference,
but the four characters  <x > are not.

Extra backslashes on the right--hand side do not affect parsing, although
they do affect the readability of the generated text.
For example, the (unnecessary) backslash in
        <x>>=<y>==((<x>\<<y>) -> void)

is displayed whenever the generated text is displayed.
For better readability it is best to avoid backslashes on the right--hand
side whenever possible.

The routine that parses the right--hand side of defs does backtracking to
reduce the number of backslashes needed on right--hand sides.
The only time a backslash is absolutely required is when there is a  <
followed by what looks like an identifier followed by a  >,
all with no intervening spaces.
For example, the right--hand side below requires its backslash, since
 <x> looks like a parameter reference:
        ... == <f1>, 0\
If the def were rewritten as
        ... == <f1>, 0<x >> <f2>

then it would no longer need a backslash.

Notice that the right--hand side does not have to refer to all of the formal
parameters and
can even be empty, as in the ``comment'' def.
        (* <string:comment> *)== .

A use of such a def might be the following.
    ,-------------------------------------------------------,
    | EDIT main goal of thm                                 |
    |-------------------------------------------------------|
    | >> x:int # ( ... )      (* This text is ignored *)    |
    |                                                       |
    |                                                       |
    '-------------------------------------------------------'


{	

 
               

 Next:  The Rules
Up:  System Description
 Previous:  Invoking Transformation Tactics

 
 

 


Richard Eaton 

Thu Sep 14 08:45:18 EDT 1995