\documentstyle[11pt]{article}

\addtolength{\textheight}{0.15\textheight}
\addtolength{\textwidth}{0.15\textwidth}
\setlength{\oddsidemargin}{0.5 in}
\setlength{\evensidemargin}{0.5 in}
\begin{document}
\title{{\bf XMETOO\\User's Manual\\}}
\author{The CAMILA Group\\
        U. Minho/INESC}
\date{November 1990}
\maketitle
\newpage

\tableofcontents
\newpage
\section{Introduction}
\begin{verbatim}
   xmetoo [Pi89,Ma89] is a functional environment for prototyping formal
constructive specifications. It is the kernel prototyping language (often
referred to as the basic functional language) of a CASE system for formal
software development, still under development at the Computer Science
Group of the University of Minho.

   xmetoo has been designed for prototyping VDM [Jo80,Jo86] specifications:
functional definitions can be directly transliterated into xmetoo. On the 
other hand, to animate relational definitions the user is required to devise
a functional (high level) implementation of each operation and test the
values returned by applying to them the post-condition, codified as a 
boolean-valued function. Data type invariants can also be codified as
boolean-valued functions.

   xmetoo is basically an extension to the original Henderson's metoo
shell [HM85]. The most relevant extensions are the following:

    a) Complete implementation of the basic data algebras used in the
       VDM meta-language as well as a type-checking mechanism.

    b) Support to user type definition according to the Abstract Syntax
       rules. All the constructors, selectors and is-functions are
       automatically defined.

    c) Implementation of high-order functions (cf. lambda expressions).

    d) Implementation of an (optional) lazy-evaluator. The interest on
       laziness is mainly due to the possibility of animation of networks
       of functional communicating prototypes.

    e) Implementation of communicating primitives to connect (UNIX) processes
       running xmetoo interpreters. In particular, they allow the 
       communication of xmetoo structured objects without requiring its 
       previous decomposition. Those primitives can be used to animate
       specifications of distributed systems.

    f) Debug facilities.

    g) Available implementations for UNIX V and MS-DOS.


    A pre-processor for xmetoo (not described in this Manual) -- called
NYAGSL -- is now available [A*89]. It makes possible to write and test
the prototypes in a higher level notation, close to that of VDM, and
also use a small development shell. The new release of NYAGSL (to be
completed in April 1991) will incorporate a LaTex interface so that,
from the same NYAGSL source file, both a functional (xmetoo) prototype
and a specification document can be generated. NYAGSL is also being 
enriched with modular facilities.

\end{verbatim}
\newpage
\section{Generics}
\begin{verbatim}
2.1 CONFIGURATIONS

The basic configuration includes a metoo-like environment with high order
functions. Besides, any arrangement of the following configurations is
valid:

   USERTYPE - Supports user defined types. It is the default configuration.
   LAZY     - Includes a lazy-evaluator.
   COMM     - Includes some communication primitives to connect different
              xmetoo processes under UNIX V.


2.2 PRIMITIVE DATA TYPES 


a) Symbol - SYM
   Syntax: any sequence of characters not started with
            '  (  )  ;  "  0..9  -0..-9  +0..+9  \0..\040
            and ended by
            '  (  )  ;  "  \0..\040
            with a maximum of 99 characters.
b) String - STR
   Syntax: any sequence of characters started and ended by ", with a
           maximum of 100 characters.
           It may include special characters like:
               - \e  [escape];
               - \n  [newline];
               - \r  [return];
               - \t  [tab];
               - \ddd [character whose ascii code is the octal value "ddd']

c) Integer - INT
   Syntax: not empty sequence of digits, with a signal optional prefix 
           (+ , -) and ended by  '  (  )  ;  "  \0..\040.
           The subset of Z representable by INT is the one assigned to the
           int type on the C language (32 bits in UNIX, 16 in MS-DOS)

d) Sequences - LIST

e) Sets - SET

f) Binary Relations - REL

g) Finite Functions - FF

h) User Defined Functions - FUN

i) Shell Functions - SUBR

j) File Pointers - FPTR

k) Communication Channels - CHAN
   [Only available in the COMM configuration.]

l) TYPE
   LABEL
   User Defined Types
   [Only available in the USERTYPE configuration.]


 
2.3 EVALUATOR


Rules for the evaluation of S-expressions:


  S-Expression    |
      Type        |                 Value 
----------------------------------------------------------------------
    nil           | ()
    SYM           | value linked to the symbol in the current environment
    STR           | the same S-expression
    INT           | the same S-expression
    SET           | the same S-expression
    REL           | the same S-expression
    FUN           | the same S-expression
    FF            | the same S-expression
    SUBR          | the same S-expression
    FPTR          | the same S-expression
    CHAN          | the same S-expression
    TYPE          | error 
    LABEL         | error 
    User Defined  | error
    LIST          | case 1 - type of (head l) = SUBR :
                  |  result of evaluating the shell function applied to (tail l)
                  | case 2 - type of (head l) = FUN :
                  |  [LAZY Configuration] result of the evaluation of the
                  |   correspondent function applied to (tail l);
                  |  [Others Configurations] result of the evaluation of the
                  |   correspondent function applied to the evaluation of
                  |   each of the elements of (tail l).
                  | case 3 -  (head l) = nil
                  |  the function identifier, number of arguments and 
                  |  respective values are shown to the user; the result of the
                  |  function is the evaluation of the introduced S-expression.
                  | case 4 - error
                  |

Although the type BOOL is not defined, the boolean values "true" and "false"
are available. They evaluate for themselves.


2.4 USER INTERACTION


* Calling the Interpreter

The interpreter is called by the command "xmetoo" at the operating system
level (notice it is automatically called when using NYAGSL). Additionally,
it is possible to specify a list of text files with xmetoo source code.
In that case a "load" statement is executed for each file.


* Prompt

The interpreter prompt begins each command line. Its general form is:

   >  
or
   n>  (being n the number of brackets not yet closed)  

A command line can have more than one S-expression.


* The Trace Stack and Debug

The interpreter manages a internal stack storing the expressions whose
evaluation is not yet completed. If the evaluation fails, the stack is shown 
on the screen, starting with the expression in which the error occurred and
including all the previous calling levels.

The user can also control the step-by-step evaluation of any S-expression
by the activation of an internal flag (called the trace-flag) using the 
primitive function "trace".


2.5 RESERVED WORDS

The following symbols cannot be redefined (eg, by the primitives
"def" or "deftype"):

    - "nil"
    - "true"
    - "false"
    - "ops" and "obs"
    - "oblist"
    - "stdin" and "stdout"
    - "empty"
    - primitive data types identifiers
    - primitive functions identifiers

\end{verbatim}
\newpage
\section{Notation}

\begin{verbatim}

3.1 FUNCTION DEFINITION STRUCTURE

The general structure of a primitive function definition is the
following:

---------------------------------------
N : Function Identifier 
    [Alternative identifiers are presented between brackets.]

S : Syntax 
    [Concrete xmetoo syntax.]

F : Signature (Functionality) 
    [S-EXP is used as the sort of a polymorphic argument]

P : Pre-Condition
    [Predicate to restrict the primitive function domain. Informal descriptions
     are presented between square brackets.]

D : Description 
    [Informal or semi-formal description of the intended meaning of the
     primitive function. Informal descriptions are presented between square
     brackets. The symbol ^= means 'equal by definition'. Unless otherwise
     stated all the symbols are supposed to be evaluated before use.]

---------------------------------------


3.2 AUXILIAR NOTATION

- type( ... )
  [returns the type of the argument]

- delay( ... )
  [returns the current environment needed for the later evaluation of
   the argument]

- let ... in ...
  [local variables definition]

- if ... then ... else ...
  [conditional]

- <e1, ..., ek>
  [sequence enumeration]

- {e1, ..., ek}
  [set enumeration]

- [d1->c1, ..., dk->ck]
  [finite function enumeration]

- ... ^ ...
  [sequence concatenation]

- ... div ...
  [integer division]

- ... mod ...
  [rest of integer division]

- ... /\ ...
  [set intersection]

- ... C= ...
  [subset relation]

- el_set( ..., ... )
  [set membership relation]
 
- ... andif ...
  [if not([first argument]) then false else [second argument]]

- ... orif ...
  [if [first argument] then true else [second argument]]

- ... != ...
  [not equal relation]

- AL ...  .  ...
  [universal quantifier]

- EX ...  .  ...
  [existential quantifier]

- @ ...
  [returns the value pointed by the argument (cf. S-expression implementation)]

Note: Standard BNF notation is freely used throughout this document.

\end{verbatim}
\newpage
\section{Basic Data Models \& Operators}
\subsection{Sets}
\begin{verbatim}

N :  card
S :  (card exp1)
F :  SET  ->  INT 
D :  (card e1) ^= [number of elements in set e1 ]
---------------------------------

N :  choice
S :  (choice exp1)
F :  SET  ->  S-EXP 
D :   exp1  != {}
     (choice e1) ^= [an element of set e1, chosen non-deterministically)
---------------------------------

N :  difference
S :  (difference exp1 exp2)
F :  SET SET  ->  SET  
D :  (difference e1 e2) ^=  e1  -  e2 
---------------------------------

N :  empty
S :  empty
F :  ->  SET
D :  empty ^= {} [denoted by "nil"]
---------------------------------

N :  intersection
S :  (intersection exp1 exp2)
F :  SET SET  ->  SET 
D :  (intersection e1 e2) ^=  e1  /\  e2 
---------------------------------

N :  isempty
S :  (isempty exp1)
F :  SET  ->  BOOL 
D :  (isempty e1) ^=  e1  = {}
---------------------------------

N :  makeset
S :  (makeset exp1*)
F :  S-EXP* -> SET
D :  (makeset) ^= {}
     (makeset e1 ... ek) ^= { e1 , ...,  ek }
---------------------------------

N :  member
S :  (member exp1 exp2)
F :  S-EXP SET  ->  BOOL 
D :  (member e1 e2) ^= el_set(  e1 ,  e2 )
---------------------------------
 
N :  reduce
S :  (reduce exp1 exp2 exp3)
F :  S-EXP SYM SET  ->  S-EXP
P :  [exp2 is an identifier of a binary function] and 
     [the result, the range of the second argument and 'exp1' have the same
     type] and
     [all the elements of 'exp3' and 'exp1' have the same type] and
     ['exp3'  != <> ]
D :  (reduce e s ls) ^= s( x1, s( x2, s( ..., s( xk,  e )...)))
                        [where  ls  = <x1, ..., xk> / {x1, ..., xk}]
     Example:
     (reduce 0 add (makeset 5 1 6 8 2)) = 22 
---------------------------------

N :  rel
S :  (rel exp1 {(from exp2 exp3 [exp4]}+)
F :  S-EXP {SYM (LIST|SET|REL) [BOOL]}+  ->  REL
D :  (set e1 (from s1 ls1 b1) ... (from sk lsk bk)) ^=
          [similar to set ...]
 
           Example:

     (rel (pair x y)
          (from x (makeset 1 3 )) (from y (list 1 2 4 5 2) (not (eq x y)))) = 
      = ((1 2)(1 4)(1 5)(3 1)(3 2)(3 4)(3 5))
---------------------------------

N :  set
S :  (set exp1 {(from exp2 exp3 [exp4]}+)
F :  S-EXP {SYM (LIST|SET|REL) [BOOL]}+  ->  SET
D :  (set e1 (from s1 ls1 b1) ... (from sk lsk bk)) ^=
          [The set of elements returned by the evaluation of e1 in the
           current environment augmented by the symbols  s1..sk. The 
           expression 'e1' is evaluated only when each 'si' is bounded
           to a value from the list/set 'lsi'. Those lists/sets are
           completely traversed and the predicates 'bi' are tested for each
           arrangement of values (if omitted a 'bi' is assumed to be true).
           An arrangement of values is only valid if all 'bi' are verified.
           The expression 'e1' may be a function on all 'si' as well as 
           on other symbols non local to the "set" expression. The predicates
           are boolean-valued functions on symbols s1..si-1 and other ones
           non local to the "set" expression. An 'si' symbol may not be
           included on the  corresponding 'lsi' expression. 'lsi' and 'bi'
           expressions are partially syntax-checked if any of their sub-
           expressions define local variables.]
           
           Example:

     (set (mul x y)
          (from x (makeset 1 3 4)) (from y (list 1 2 4 5 2) (not (eq x y)))) = 
      = (2 4 5 3 6 12 15 8 20)
---------------------------------

N :  subset
S :  (subset exp1 exp2)
F :  SET SET  ->  BOOL 
D :  (subset e1 e2) ^=  e1  C=  e2 
---------------------------------

N :  the
S :  (the exp1)
F :  SET  ->  S-EXP 
P :  [ exp1  is a singleton set]
D :  (the e1) ^= [the only element of the singleton set e1 ]
---------------------------------

N :  union 
S :  (union exp1 exp2)
F :  SET SET  ->  SET
D :  (union e1 e2) ^=  e1  U  e2 
---------------------------------

N :  UNION
S :  (UNION exp1)
F :  SET  ->  SET
P :  [ all the members of 'e1' are sets]
D :  (UNION e1) ^= s1 U s2 U ... U sk
                   [where s1..sk are sets belonging to e1]
\end{verbatim}
\newpage
\subsection{Sequences}
\begin{verbatim}

N :  append
S :  (append exp1 exp2+)
F :  LIST LIST+  ->  LIST
D :  (append e1 .. en) ^=  e1  ^ .. ^  en 
---------------------------------

N :  CONC
S :  (CONC exp1)
F :  LIST  ->  LIST
P :  ['exp1' is a list of lists]
D :  (CONC e1) ^= l1 ^ l2 ^ ... ^ lk
                  [where l1..lk are lists from the list  e1 ]
---------------------------------

N :  cons
S :  (cons exp1 exp2)
F :  S-EXP LIST  ->  LIST
D :  "non LAZY" Configuration: (cons e1 e2) ^= < e1 > ^  e2 
     "LAZY" Configuration: (cons e1 e2) ^= <delay( e1 )> ^ delay( e2 )
---------------------------------

N :  el  ( nth )
S :  (el exp1 exp2)
F :  INT LIST  -> S-EXP
P :  0 <  exp1  <= [lenght of list  exp2 ]
D :  (el e1 e2) ^= [The element of e2 in position e1]
---------------------------------

N :  elems
S :  (elems exp1)
F :  LIST  ->  SET
D :  (elems e1) ^= [The set of elements of list e1]
---------------------------------

N :  head  ( hd )
S :  (head exp1)
F :  LIST  ->  S-EXP
P :   exp1  != <>
D :  Non "LAZY" Configurations: (head e1) ^= [first element of e1 ]
     "LAZY" Configuration:
        (head e1) ^= if type( e1 ) = "lazy-list"
                     then  [first element of e1] 
                     else let s1 =  e1 
                          in if type( s1 ) = "lazy-list"
                             then  [first element of s1] 
                             then  [first element of s1] 
---------------------------------

N :  inds
S :  (inds exp1)
F :  LIST  ->  LIST
D :  (inds <>) = <>
    : (inds e1) ^= [list of natural numbers from 1 to len(s)]
---------------------------------

N :  length
S :  (length exp1)
F :  LIST  ->  INT
D :  (length e1) ^= [number of elements of  e1 ]
---------------------------------

N : list ( makeseq )
S : (list exp1*)
F : S-EXP*  ->  LIST
P : (list) ^= <>
D :(list e1 ... ek) ^= < e1  ...  ek >
---------------------------------

N :  makeseq  ( list )
S :  (makeseq exp1*)
F :  S-EXP*  ->  LIST
P :  (makeseq) ^= <>
D :  (makeseq e1..ek) = < e1 , ...,  ek >
---------------------------------

N :  nil
S :  nil
F :  -> LIST 
D :  nil ^= <>
---------------------------------

N :   pair
S :  (pair exp1 exp2)
F :  S-EXP S-EXP  ->  LIST
D :  (pair e1 e2) ^= < e1 ,  e2 >
---------------------------------

N :  plusq
S :  (plusq exp1 exp2)
F :  LIST FF  ->  LIST
P :  dom(  exp2  ) C= elems( inds(  exp1 ))
D :  (plusq e1 e2) ^= [e1 is overwritten by e2(i) on the positions determined 
                       by 'i', belonging to dom( e2 )]
     Example:
     let  f = ((1 4) (5 3) (2 2))
          l = (1 2 3 4 5 6)
     (plusq l f) = (4 2 3 4 3 6)
---------------------------------

N :  reduce
S :  (reduce exp1 exp2 exp3)
F :  S-EXP SYM LIST  ->  S-EXP S-EXP SYM SET  ->  S-EXP
P :  [exp2 is an identifier of a binary function] and 
     [the result, the range of the second argument and 'exp1' have the same
     type] and
     [all the elements of 'exp3' and 'exp1' have the same type] and
     ['exp3'  != <> ]
D :  (reduce e s ls) ^= s( x1, s( x2, s( ..., s( xk,  e )...)))
                        [where  ls  = <x1, ..., xk> / {x1, ..., xk}]
     Example:
     (reduce nil cons (list 1 2 1 3 1 4 5 6)) = (1 2 1 3 1 4 5 6)
---------------------------------

N :  reverse
S :  (reverse exp1)
F :  LIST  ->  LIST  
D :  (reverse e1) ^= [e1 reversed]
---------------------------------

N :  seq
S :  (seq exp1 {(from exp2 exp3 [exp4]}+)
F :  S-EXP {SYM (LIST|SET) [BOOL]}+  ->  LIST
D :  (seq e1 (from s1 ls1 b1) ... (from sk lsk bk)) ^=
          [The list of elements returned by the evaluation of e1 in the
           current environment augmented by the symbols  s1..sk. The 
           expression 'e1' is evaluated only when each 'si' is bounded
           to a value from the list/set 'lsi'. Those lists/sets are
           completely traversed and the predicates 'bi' are tested for each
           arrangement of values (if omitted a 'bi' is assumed to be true).
           An arrangement of values is only valid if all 'bi' are verified.
           The expression 'e1' may be a function on all 'si' as well as 
           on other symbols non local to the "seq" expression. The predicates
           are boolean-valued functions on symbols s1..si-1 and other ones
           non local to the "seq" expression. An 'si' symbol may not be
           included on the  corresponding 'lsi' expression. 'lsi' and 'bi'
           expressions are partially syntax-checked if any of their sub-
           expressions define local variables.]
           
           Example:

     (seq (list y x) 
          (from x (list 1 2 3 2) (not (eq x 1))) (from y (makeset 'q 'f))) = 
     ((q 2) (f 2) (q 3) (f 3) (q 2) (f 2))
---------------------------------

N :  tail  ( tl )
S :  (tail exp1)
F :   LIST  ->  LIST
P :   exp1  != <>
D :   Non "LAZY" Configuration:
        (tail e1) ^= [ e1  without the first element]
      "LAZY" Configuration:
        (tail e1) ^= if type( e1 ) = "lazy-list"
                     then [e1 -- not evaluated -- without the first element]
                     else [e1 without the first element]
---------------------------------

N :  fifth
S :  (fifth exp1)
F :  LIST  ->  S-EXP
D :  length(  exp1 ) >= 5
     (fifth e1) ^= [fifth element of  e1 ]
---------------------------------

N :  first
S :  (first exp1)
F :  LIST  ->  S-EXP
D :  length(  exp1 ) >= 1
     (first e1) ^= [first element of  e1 ]
---------------------------------

N :  fourth
S :  (fourth exp1)
F :  LIST  ->  S-EXP
D :  length(  exp1 ) >= 4
     (fourth e1) ^= [fourth element of  e1 ]
---------------------------------

N :  second
S :  (second exp1)
F :  LIST  ->  S-EXP
P :  length(  exp1 ) >= 2
D :  (second e1) ^= [second element of e1 ]
---------------------------------

N :  third
S :  (third exp1)
F :  LIST  ->  S-EXP
D :  length(  exp1 ) >= 3
     (third e1) ^= [third element of e1 ]
---------------------------------

\end{verbatim}
\newpage
\subsection{Finite Functions}
\begin{verbatim}

N :  ap
S :  (ap exp1 exp2 [exp3])
F :  FF S-EXP [S-EXP]  ->  S-EXP
D :  (ap e1 e2 e3) ^= let f =  e1 
                          s2 =  e2 
                      in if el_set( s2, dom( f ))
                         then f(s2)
                         else  e3 ["nil" if e3 is omitted] 
---------------------------------

N :  dom
S :  (dom exp1)
F :  FF  ->  SET
D :  (dom e1) ^= [domain of  e1 ]
---------------------------------

N :  dr
S :  (dr exp1 exp2)
F :  FF SET  ->  FF
D :  (dr e1 e2) ^= [domain restriction of e1 to e2]

     Example:
     (dr ((1 b) (2 g) (8 h) (9 h)) (makeset 1 2)) = ((1 b) (2 g))
---------------------------------

N :  ds
S :  (ds exp1 exp2)
F :  FF SET  ->  FF
D :  (ds e1 e2) ^= [domain subtraction of e2 to e1]

     Example:
     (ds ((1 b) (2 g) (8 h) (9 h)) (makeset 1 2)) = ((8 h) (9 h))
---------------------------------

N :  ff
S :  (ff exp1 exp2 exp3 [exp4])
F :  SYM SET S-EXP [BOOL]  ->  FF
D :  (ff sim set e b) ^= [Finite function whose domain is the set of elements
                          'sim' from 'set' verifying 'b'. The range is 
                          generated by 'e' in the current environment
                          augmented by 'sim'. 'sim' is local to the 'ff'
                          expression, its scope being the expressions 'e'
                          and 'b'. The expressions 'set', 'e' and 'b' are
                          partially syntax-checked if they include 
                          subexpressions with local definitions.]

     Example:
     (ff x (makeset 1 2 3) (add x 1) (not (eq x 2))) = ((1 2) (3 4))
---------------------------------

N :  isempty
S :  (isempty exp1)
F :  FF  ->  BOOL
D :  (see the section on type SET)
---------------------------------

N :  makeff
S :  (makeff {(exp1 exp2)}*)
F :  {S-EXP S-EXP}*  ->  FF
P :  [there are not repeated elements in the domain]
D :  (makeff) ^= []
     (makeff (e1 e2) ... (ek ek+1)) ^=
           [ e1  ->  e2 , ...,  ek  ->  ek+1 ]
---------------------------------

N :  nil
S :  nil
F :  -> FF
D :  nil ^= [] 
---------------------------------

N :  plus
S :  (plus exp1 exp2)
F :  FF FF  ->  FF
D :  (plus f1 f2) ^= [Finite function resulting from the overwrite of 'f1' by
                      'f2'. The domain is the union of the domains of 'f1' and
                      'f2'. Each element x of the domain is mapped to f1(x),
                      if x is not member of the domain of 'f2', or to f2(x) 
                      otherwise.]

     Example:
        Let f1 = ((q 2) (w 2) (e 3))
            f2 = ((q 3) (r 5) (h 4) (j 2))
        in (plus f1 f2) = ((q 3) (w 2) (e 3) (r 5) (h 4) (j 2)) 
---------------------------------

N :  ran
S :  (ran exp1)
F :  FF  ->  SET
D :  (ran e1) ^= [range of e1 ]
---------------------------------
\end{verbatim}
\newpage
\subsection{Binary Relations}
\begin{verbatim}

N :  card
S :  (card exp1)
F :  REL  ->  INT
D :  (see the section on type SET)
---------------------------------

N :  choice
S :  (choice exp1)
F :  REL  ->  S-EXP
D :  (see the section on type SET)
---------------------------------

N :  difference
S :  (difference exp1 exp2)
F :  REL REL  ->  REL 
D :  (see the section on type SET)
---------------------------------

N :  dom
S :  (dom exp1)
F :  REL  ->  SET
D :  (see the section on type FF)
---------------------------------

N :  dr
S :  (dr exp1 exp2)
F :  REL SET  ->  REL 
D :  (see the section on type FF)
---------------------------------

N :  ds
S :  (ds exp1 exp2)
F :  REL SET  ->  REL 
D :  (see the section on type FF)
---------------------------------

N :  intersection
S :  (intersection exp1 exp2)
F :  REL REL  ->  REL
D :  (see the section on type SET)
---------------------------------

N :  isempty
S :  (isempty exp1)
F :  REL  ->  BOOL
D :  (see the section on type SET)
---------------------------------

N :  makerel
S :  (makerel {(exp1 exp2)}*)
F :  {S-EXP S-EXP}*  ->  REL
D :  (makerel) ^= {}
     (makerel (e1 e2) ... (ek ek+1)) ^=
              { < e1 ,  e2 >, ..., < ek ,  ek+1 >}
---------------------------------

N :  member
S :  (member exp1 exp2)
F :  S-EXP REL  ->  BOOL
D :  (see the section on type SET)
---------------------------------

N :  nil
S :  nil
F :  -> REL 
D :  (see the section on type SET)
---------------------------------

N :  ran
S :  (ran exp1)
F :  REL  ->  SET 
D :  (see the section on type FF)
---------------------------------

N :  subset
S :  (subset exp1 exp2)
F :  REL REL  ->  BOOL
D :  (see the section on type SET)
---------------------------------

N :  the
S :  (the exp1)
F :  REL  ->  S-EXP
D :  (see the section on type SET)
---------------------------------

N :  union 
S :  (union exp1 exp2)
F :  REL REL  ->  REL
D :  (see the section on type SET)
---------------------------------

\end{verbatim}
\newpage
\subsection{Integers \& Strings}
\begin{verbatim}

N :  abs
S :  (abs exp1)
F :  INT  ->  INT
D :  (abs e1) ^= | e1 |
---------------------------------

N :  add  
S :  (add exp1 exp2)
F :  INT INT  ->  INT
D :  (add e1 e2) ^=  e1  +  e2 
---------------------------------

N :  ascii  
S :  (ascii exp1)
F :  STR  ->  INT
D :  (ascii e1) ^= [Ascii code of the first character of 'e1'; 0 is
                    returned if e1="".]
---------------------------------

N :  atoi  
S :  (atoi exp1)
F :  STR  ->  INT
D :  [numerical string]
     (atoi e1) ^= [Integer value of the string 'exp1'. Initial spaces are 
                   ignored. Only the signal character and the digits until
                   the first no numeric character are considered. Returns 0
                   in case of error.]
---------------------------------

N :  chr 
S :  (chr exp1)
F :  INT  ->  STR
D :  (chr e1) ^= [String whose ascii code is 'e1']
---------------------------------

N :  div 
S :  (div exp1 exp2)
F :  INT INT  ->  INT
D :  (div e1 e2) ^=  e1  div  e2 
---------------------------------

N :  inseg
S :  (inseg exp1)
F :  INT  ->  SET
D :  (inseg e1) ^= [e1-initial segment of N ( = {1,2,...,e1} )]
---------------------------------

N :  itoa  
S :  (itoa exp1)
F :  INT  ->  STR
D :  (itoa e1) ^= [String built from the digits and signal of the integer 'e1']
---------------------------------

N :  mul
S :  (mul exp1 exp2)
F :  INT INT  ->  INT
D :  (mul e1 e2) ^=  e1  *  e2 
---------------------------------

N :  rem
S :  (rem exp1 exp2)
F :  INT INT  ->  INT
D :  (rem e1 e2) ^=  e1  mod  e2 
---------------------------------

N :  strcat  
S :  (strcat exp1*)
F :  STR*  ->  STR
P :  [The length of the result cannot exceed 100 characters]
D :  (strcat) ^= ""
     (strcat e1 ... ek) ^= [Concatenation of the strings 'e1' ... 'ek']
---------------------------------

N :  strlen  
S :  (strlen exp1*)
F :  STR*  ->  INT
D :  (strlen) ^= 0
     (strlen e1 ... ek) ^= [Sum of the lengths of strings 'e1' to 'ek']
---------------------------------

N :  strsym
S :  (strsym exp1)
F :  STR  ->  SYM
P :  ['exp1' is a string built only from characters used in symbol definition]
D :  (strsym e1) ^= [symbol built from the sequence of characters in string
                     'e1']
---------------------------------

N :  sub
S :  (sub exp1 exp2)
F :  INT INT  ->  INT
D :  (sub e1 e2) ^=  e1  -  e2 
---------------------------------

N :  substr  
S :  (substr exp1 exp2 [exp3])
F :  STR INT [INT]  ->  STR
D :  (substr e1 e2 e3) ^= [Substring of 'e1' beginning at position 'e2' and
                           with 'e3' characters. If 'e2' < 1 or if it exceeds
                           the length of 'e1' the result is "" . 'e3' may be
                           omitted; in that case the result will be the tail
                           of 'e1' beginning and including 'e2'.

     Example:
     (substr "abcdef" 2) = (substr "abcdef" 2 6) = "bcdef"
     (substr "abcdef" 2 -1) = ""
     (substr "abcdef" 2 3) = "bcd"
---------------------------------

N :  symstr
S :  (symstr exp1)
F :  SYM  ->  STR
D :  (symstr e1) ^= [String built from the sequence of characters defining 'e1']
---------------------------------
\end{verbatim}
\newpage
\subsection{Relational Operators}
\begin{verbatim}

N :  eq
S :  (eq exp1 exp2)
F :  S-EXP S-EXP  ->  BOOL
D :  (eq e1 e2) ^= let s1 =  e1 
                       s2 =  e2 
                   in (s1 = s2 = nil) orif
                      if (type( s1 ) = type( s2 ) = INT) or
                         (type( s1 ) = type( s2 ) = STR) or
                         (type( s1 ) = type( s2 ) = FPTR) or
                         (type( s1 ) = type( s2 ) = CHAN) or
                         (type( s1 ) = type( s2 ) = SUBR) 
                      then @s1 = @s2
                      else if type( s1 ) = type( s2 ) = SYM
                           then s1 = s2
                           else false
---------------------------------

N :  equal
S :  (equal exp1 exp2)
F :  S-EXP S-EXP  ->  BOOL
D :  (equal e1 e2) ^= (eq e1 e2) orif  e1  =  e2 
---------------------------------

N :  geq
S :  (geq exp1 exp2)
F :  INT INT  ->  BOOL 
     STR STR  ->  BOOL
D :  (geq e1 e2) ^=  e1  >=  e2 
---------------------------------

N :  gt 
S :  (gt exp1 exp2)
F :  INT INT  ->  BOOL 
     STR STR  ->  BOOL
D :  (gt e1 e2) ^=  e1  >  e2 
---------------------------------

N :  leq
S :  (leq exp1 exp2)
F :  INT INT  ->  BOOL 
     STR STR  ->  BOOL
D :  (leq e1 e2) ^=  e1  <=  e2 
---------------------------------

N :  lt 
S :  (lt exp1 exp2)
F :  INT INT  ->  BOOL 
     STR STR  ->  BOOL
D :  (lt e1 e2) ^=  e1  <  e2 
---------------------------------

N :  neq
S :  (neq exp1 exp2)
F :  S-EXP S-EXP  ->  BOOL
D :  (neq e1 e2) ^= not( eq( e1 e2 ) ) 
---------------------------------

N :  nequal
S :  (nequal exp1 exp2)
F :  S-EXP S-EXP  ->  BOOL
D :  (nequal e1 e2) ^= not( equal( e1 e2) ) 
---------------------------------
\end{verbatim}
\newpage
\subsection{Logic}
\begin{verbatim}

N :  ALL
S :  (ALL exp1 exp2 exp3)
F :  SYM SET BOOL  ->  BOOL
D :  (ALL s set pred) ^= [Implementation of the universal quantifier, being
                          's' the bounded variable, 'set' the quantification
                          domain and 'pred' the predicate. The expressions
                          'set' and 'pred' are partially syntax-checked if
                          including any local variable definition.]
---------------------------------

N :  and 
S :  (and exp1 exp2)
F :  BOOL BOOL  ->  BOOL
D :  (and e1 e2) ^=  e1  andif  e2 
---------------------------------

N :  EXIST
S :  (EXIST exp1 exp2 exp3)
F :  SYM SET BOOL  ->  BOOL
D :  (EXIST s set pred) ^= [Implementation of the existential quantifier, being
                            's' the bounded variable, 'set' the quantification
                            domain and 'pred' the predicate. The expressions
                            'set' and 'pred' are partially syntax-checked if
                            including any local variable definition.]
---------------------------------

N :  EXIST1
S :  (EXIST1 exp1 exp2 exp3)
F :  SYM SET BOOL  ->  BOOL
D :  (EXIST1 s set pred) ^= [Implementation of the exclusive existential
                             quantifier, being 's' the bounded variable,
                             'set' the quantification domain and 'pred' the
                             predicate. The expressions 'set' and 'pred' are
                             partially syntax-checked if including any local
                             variable definition.]
---------------------------------

N :  false
S :  false
F :  ->  BOOL
D :  [Boolean constant whose value is false]
---------------------------------

N :  not
S :  (not exp1)
F :  BOOL  ->  BOOL
D :  (not e1) ^= if  e1 
                 then "true"
                 else "false"
---------------------------------

N :  or 
S :  (or exp1 exp2)
F :  BOOL BOOL  ->  BOOL
D :  (or e1 e2) ^=  e1  orif  e2 
---------------------------------

N :  true
S :  true
F :  ->  BOOL
D :  [Boolean constant whose value is true]
---------------------------------
\end{verbatim}
\newpage
\section{Type Definition}
\begin{verbatim}

N :  deftype
S :  (deftype exp1 exp2)
F :  SYM <typeexp>  ->  SYM
P :  [exp1 cannot be a shell reserved word]
D :  (deftype t etipo) ^= t
       [The symbol 't' is linked to the type defined by the expression
        'etipo'. No defined type identifiers can appear in 'etipo' and
        recursive definitions are allowed. The symbol 't' can be used
        as a constructor of values of the new type. Furthermore, when
        defining a tuple the labels can be used as selectors (labels
        with the same name in different tuples are allowed.]

    NOTE: This is the syntax of type expressions:

    <typeexp>     ::= <tuple> | <alternative> | <equality> | <set> |
                      <binrel> | <list> | <finite func> | <atom>
    <typeexp1>    ::= <finite func> | <binrel> | <list> | 
                      <set> | <atom> | <type identifier>
    <tuple>       ::= 'TUP' { '(' <label> <typeexp1> ')' }+
    <alternative> ::= 'ALT' ['NIL'] <typeexp1>+
    <equality>    ::= 'EQ' <type identifier>
    <finite func> ::= 'FF' <typeexp1> <typeexp1>
    <binrel>      ::= 'REL' <typeexp1> <typeexp1>
    <list>        ::= 'LIST' <typeexp1>
    <set>         ::= 'SET' <typeexp1>
    <atom>        ::= 'SYM' | 'INT' | 'STR' | 'FPTR' | 'CHAN'  
    <label>       ::= xmetoo symbol
    <type identifier> ::= xmetoo symbol 

---------------------------------

NOTE:

   To all user defined types is associated a constructor. Its use is only
   mandatory when working with tuples (as in the VDM meta-language). In
   all the other cases it is optional, but notice that if a constructor is
   used to generate an object its value will be labeled. Also notice
   that a labeled object of type 't' is never compatible with an object
   of type 't'.

---------------------------------

N : [t - identifier of a user defined type]
S : (t exp1+)
F : S-EXP+  ->  t
D : [Construct a value of type 't'.]
---------------------------------

N :  is
S :  (is exp1 exp2)
F :  <typeexp> S-EXP  ->  BOOL 
D :  (is tipo exp) ^= [Returns true if 'exp' is of type 'tipo'.]
---------------------------------

N :  ignlab
S :  (ignlab exp1)
F :  S-EXP  ->  S-EXP 
D :  (ignlab exp) ^= [Returns 'exp' after removing the label; if 'exp'
                      has no label returns 'exp'.]
NOTE:
   In order to apply the primitive functions (namely, the ones described
   in section 4) to values of user defined types generated by constructs
   the labels must be removed using ignlab. In most cases it is much
   simpler to ignore the constructs ... 
---------------------------------

N :  type
S :  (type exp1)
F :  S-EXP  ->  SYM
D :  (type e1) ^= type(  e1 )
---------------------------------

N :  gettype
S :  (gettype exp1)
F :  SYM  ->  SYM-list
D :  (gettype e1) ^= [Returns a list of symbols containing the definition 
                      of type eval(e1).]
---------------------------------

N :  atom 
S :  (atom exp1)
F :  S-EXP  ->  BOOL
D :  (atom e1) ^= let s1 =  e1 
                  in s1 = nil orif
                     el_set( type( s1 ), {INT, STR, SYM, SUBR, FPTR, CHAN} )
---------------------------------
\end{verbatim}
\newpage
\section{Function \& Expressions}
\begin{verbatim}
---------------------------------

N :  cond
S :  (cond {(exp1 exp2*)}*)
F :  {BOOL S-EXP*}*  ->  S-EXP
D :  (cond) ^= nil
     (cond (b1 e11 ... e1k) ... (bn en1 ... enm)) ^=
          [Evaluates every 'eij' expressions for the first true 'bi'.
           Returns the last 'eij' of that list. If every 'bi' are false,
           a null value is returned]

Example:
     (cond (false (add 2 3))
           (true (def x 3) (def y 4) (add 4 5))
           ((lt 2 3) 'q)) = 9 [as side effect, 'x' and 'y' are inserted in 
                               the symbol table with values 3 and 4]
---------------------------------

N :  if
S :  (if exp1 exp2 [exp3])
F :  BOOL S-EXP [S-EXP]  ->  S-EXP
D :  (if e1 e2 e3) ^= if  e1 
                      then  e2 
                      else  e3  [If omitted, e3 will be "nil"]
---------------------------------

N :  let
S :  (let ({(exp1 exp2)}*) [exp3])
F :  {SYM S-EXP}* [S-EXP]  ->  S-EXP
D :  (let ((s1 e1) ... (sk ek)) exp) ^=
         [In the LAZY configuration each symbol 'si' is linked with
		 delay('ei') so that the evaluation of 'ei' will be postponed.
         In all the others cases, each pair ('si', 'ei') defines a 
		 symbol 'si' with value 'ei'. 'si' can then be used until the
		 end of let expression. The 'ei' expression can reference previous
		 defined symbols.  
         If omitted 'exp', "nil" will be returned. The definition of the 'si'
		 symbol does not affect the value of a global symbol with the 
		 same name.]
---------------------------------

N :  lambda
S :  (lambda (exp1*) exp2)
F :  SYM* S-EXP  ->  FUN
D :  (lambda (s1 ... sk) e1) ^=  [An user defined lambda-expression with formal 
 		                          parameters 's1 ... sk' end returning e1.]
---------------------------------

N :  def
S :  (def exp1 lambda (exp2*) exp3) 
F :  SYM SYM* S-EXP  ->  SYM 
P :  [exp1 not in the reserved symbols set]
D :  (def s lambda (s1 ... sk) e1) ^= s
         [As a side effect, 's' is defined as a function with formal
          parameters s1..sk returning 'e1'. 
          's' is added to operations list 'ops']

S :  (def exp1 exp2)
F :  SYM S-EXP  ->  SYM
P :  [exp1 not in the reserved symbols set]
D :  (def s e1) ^= s
         [As a side effect, 's' is linked to e1 and inserted in object
          list 'obs']
---------------------------------

N :  obs
S :  obs
F :  ->  LIST
D :  [List of defined objects (cf. "def")]
---------------------------------

N :  ops
S :  ops
F :  ->  LIST
D :  [List of defined functions (cf. "def")]
---------------------------------

S :  (exp1 exp2*)
F :  FUN S-EXP*  ->  S-EXP 
     SUBR S-EXP*  ->  S-EXP
P :  [The order and types of the argument must be correct]
D :  (f e1 ... ek) ^=
		[If the type of the evaluation of 'exp1' is
		  - SUBR, the associated C function is called with parameters
            e1..ek
		  - FUN and the configuration is not LAZY, the associated user defined
		    function is called with parameters e1..ek
		  - FUN and configuration is LAZY, the associated user defined
		    function is called with delayed evaluated parameters e1..ek]
---------------------------------

N :  eval
S :  (eval exp1)
F :  S-EXP  ->  S-EXP
D :  (eval e1) ^=  [Returns the evaluation of the result of expression 'e1'.]
---------------------------------

N :  quote
S :  (quote exp1) [equivalent to exp1]
F :  S-EXP  ->  S-EXP
D :  (quote e1) ^= e1  [Note that 'e1' is not evaluated]
---------------------------------

N :  sh
S :  (sh [exp1])
F :  [STR]  ->  INT
D :  (sh s) ^= 
       [Execute command included in string 's' under the operating system
        shell. The error code of the execution is returned.
	    If 's' is omitted an operating system shell will be created on the
		top of xmetoo.]
---------------------------------

N :  !
S :  (! [exp1])
F :  [INT]  ->
D :  (! e1) ^= [End a xmetoo session returning 'e1' value 
                (0 by default) to the operating system]
---------------------------------

N :  prog1
S :  (prog1 exp1*)
F :  S-EXP*  ->  S-EXP
D :  (prog1) ^= nil
     (prog1 e1 ... ek) ^= [Evaluates  e1 .. ek and returns e1]
---------------------------------

N :  progn
S :  (progn exp1*)
F :  S-EXP*  ->  S-EXP
D :  (progn) ^= nil
     (progn e1 ... ek) ^= [Evaluates  e1 .. ek and returns ek]
---------------------------------

N :  repeat
S :  (repeat exp1 exp2*)
F :  INT S-EXP*  ->  S-EXP
D :  (repeat e1 e2 ... ek) ^=
		[The expressions e2..ek are evaluated e1 times. Returns the result 
		 of the last evaluated expression. If e1 <= 0, "nil" is  returned.]
---------------------------------

N :  foreach
S :  (foreach exp1 exp2 exp3*)
F :  SYM LIST S-EXP*  ->  S-EXP
D :  (foreach s l e1 ... ek) ^=
        [Expressions e1 ... ek are evaluated foreach element 's' of the
		 list 'l'. The last evaluated expression is returned.]
---------------------------------

N :  while 
S :  (while exp1 exp2*)
F :  BOOL S-EXP*  ->  S-EXP
D :  (while e1 e2 ... ek) ^=
	   [Expression e2 ... ek are evaluated while e1 is "true".
	    The last evaluated expression is returned. If omitted e2..ek or if
		e1 is false in the first time, "nil" value is returned.]
---------------------------------

N :  PACK
S :  (PACK exp1)
F :  LIST  ->  SYM
D :  (PACK e1) ^= 
        [Returns a symbol named by the concatenation of the argument 
         list (including only symbols and positive integers)]
---------------------------------

N :  UNPACK
S :  (UNPACK exp1)
F :  SYM  ->  LIST
D :  (UNPACK e1) ^= 
        [List of one character symbols or integers whose
         concatenation is e1.]
---------------------------------

\end{verbatim}
\newpage
\section{I/O Functions}

\begin{verbatim}
N :  fclose  
S :  (fclose exp1)
F :  FPTR  ->  nil
P :  [the file pointed by 'exp1' must be open]
D :  (fclose e1) ^= nil
                    [As a side effect, closes the file pointed by 'exp1'.]
---------------------------------

N :  fgetc
S :  (fgetc [exp1])
F :  [FPTR]  ->  INT | nil
P :  [the file pointed by 'exp1' must be open]
D :  (fgetc e1) ^= [Ascii code of the next character in the file pointed by
                    'e1'; returns "nil" if eof detected.]
---------------------------------

N :  fgets
S :  (fgets [exp1])
F :  [FPTR]  ->  STR | nil
P :  [the file pointed by 'exp1' must be open]
D :  (fgets e1) ^= [Next line in the file pointed by 'e1';
                    returns "nil" if eof detected.]
---------------------------------

N :  fopen  
S :  (fopen exp1 exp2)
F :  STR STR  ->  FPTR | nil
D :  (fopen e1 e2) ^= [File pointer to the file identified by 'e1' and
                       open in mode 'e2'. The available modes are:
                          "r" - read only 
                          "w" - overwrite
                          "a" - append
                          "r+"- read/write in an old file
                          "w+"- read/write in an new  file
                          "a+"- read/write after the end of file 
                        It returns "nil" in case of error.]
---------------------------------

N :  fputc
S :  (fputc exp1 [exp2])
F :  INT [FPTR]  ->  INT
P :  [the file pointed by 'exp2' must be open]
D :  (fputc e1 e2) ^=  e1 
                       [As a side effect, writes 'e1' in file 'e2'.
                        If the second argument is omitted the current output
                        channel is used.]
---------------------------------

N :  fputs
S :  (fputs exp1 [exp2])
F :  STR [FPTR]  ->  STR
P :  [the file pointed by 'exp2' must be open]
D :  (fputs e1 e2) ^=  e1 
                       [As a side effect, writes 'e1' in file 'e2'. 
                        If the second argument is omitted the current output
                        channel is used.]
---------------------------------

N :  m2read
S :  (m2read exp1)
F :  FPTR -> S-EXP 
P :  [the file pointed by 'exp1' must be open]
D :  (m2read e1) ^= [Returns the evaluation of the S-expression read in the
                     file pointed by 'e1'. It reports error if eof reached.]
---------------------------------

N :  m2write
S :  (m2write exp1 exp2)
F :  FPTR S-EXP -> nil
P :  [the file pointed by 'exp1' must be open] and
     (el_set( type(exp2), {INT,STR,SYM,LIST,SET,REL,FF,User Defined}))
D :  (m2write e1 e2) ^= nil
                        [As a side effect writes the result of 'e2' in the
                         file pointed by 'e1'.]
---------------------------------

N :  stdin
S :  stdin
F :  ->  FPTR 
D :  [Pointer to the current standard input.]
---------------------------------

N :  stdout
S :  stdout
F :  ->  FPTR 
D :  [Pointer to the current standard output.]
---------------------------------

N :  readf
S :  (readf exp1)
F :  FPTR -> S-EXP 
P :  [the file pointed by 'exp1' must be open]
D :  (readf e1) ^= [Returns the S-expression read on file "S".
                    It reports error if eof reached.]
---------------------------------

N :  writef
S :  (writef exp1 exp2)
F :  FPTR S-EXP -> nil
P :  [the file pointed by 'exp1' must be open] and
     (el_set( type( exp2 ), {INT,STR,SYM,LIST,SET,REL,FF, User Defined types}))
D :  (writef e1 e2) ^= nil
                       [As a side effect, the result of evaluating 'e2' is
                        written in the file pointed by 'e1'.]
---------------------------------

N :  load
S :  (load exp1)
F :  STR  ->  STR
D :  (load e1) ^= [Reads and Evaluates all the S-expressions in the file.]
---------------------------------

N :  LOAD
S :  (LOAD exp1)
F :  STR  -> 
D :  (LOAD e1) ^= [The internal state is rebuilt from an object file
                   (produced by SAVE) identified by 'e1'.]
---------------------------------

N :  princ
S :  (princ exp1*)
F :  S-EXP*  ->  nil
D :  (princ e1 .. ek) ^= nil
           [As a side effect, displays 'e1', ..., 'ek'. In displaying some
            control commands are replaced:
              -  "escape" by "\e"
              -  "newline" by "\n"
              -  "return" by "\r"
              -  "tab" by "\t"
              -  non visible characters by their octal code "\ddd"
---------------------------------

N :  print
S :  (print exp1*)
F :  S-EXP*  ->  nil
D :  (print e1 .. ek) ^= nil
                         [As a side effect, displays 'e1', ..., 'ek'.]
---------------------------------

N :  read
S :  (read [exp1])
F :  [STR]  ->  S-EXP
D :  (read e1) ^= ["S"-expression in 'e1'; if 'e1' does not exist reads
                   from the keyboard.]
---------------------------------

N :  SAVE 
S :  (SAVE exp1)
F :  STR  ->  nil 
D :  (SAVE e1) ^= [The internal state of the interpreter is saved in a file 
                   identified by 'e1'.]
---------------------------------
\end{verbatim}
\newpage
\section{Communication Primitives}
\begin{verbatim}

N :  channel
S :  (channel exp1)
F :  STR  ->  CHAN 
     STR  ->  nil
P :  1 <= [length of exp1] <= 4
D :  (channel e1) ^= [Defines a new communication channel named after the
                      result of 'e1'. Returns "nil" if an error occurs.]
---------------------------------

N :  receive
S :  (receive exp1)
F :  CHAN  ->  S-EXP
D :  (receive e1) ^= [Returns the S-expression received on channel 'e1']
---------------------------------

N :  rmchannel
S :  (rmchannel exp1)
F :  CHAN  ->  nil
D :  (rmchannel e1) ^= nil
     [As a side effect closes the channel named after the result of e1.]
---------------------------------

N :  send
S :  (send exp1 exp2)
F :  CHAN S-EXP  ->  S-EXP
P :  eval( exp2 ) = nil orif
                    el_set(type(exp2),
                      {INT,STR,SYM,LIST,SET,REL,FF,FUN,User Defined Type})
D :  (send e1 e2) ^= [Returns the result of 'e2'. As a side effect sends
                      this value on channel e1.]


\end{verbatim}
\newpage
\section{System Primitives}

\begin{verbatim}
N :  alloc
S :  (alloc exp1)
F :  INT  ->  INT
P :  exp1  >= 1
D :  (alloc e1) ^= [The number of nodes in each segment is set to 'e1'; the
                    previous value is returned.]
---------------------------------

N :  expand
S :  (expand [exp1])
F :  [INT]  ->  INT
P :  exp1  >= 1
D :  (expand e1) ^= [Try to allocate 'e1' segments (1 if the argument is
                     omitted) and returns the number of segments allocated.]
---------------------------------

N :  gc
S :  (gc)
F :  -> nil
D :  (gc) ^= nil
             [As a side effect executes a garbage-collection in the heap and, 
              if needed (and possible) allocates a new segment.]
---------------------------------

N :  mem
S :  (mem)
F :  ->  nil
D :  (mem) ^= nil
             [As a side effect displays the following statistics:
             Nodes    - Number of nodes which have been allocated since
                        the process started.
             Free     - Number of free nodes in the allocated segments.
             Segments - Number of allocated segments in the current memory 
                        of the interpreter.
             Allocate - Number of nodes to allocate per segment whenever 
                        new segments are requested.
             Collections - Number of "garbage-collections" made.]
---------------------------------

N :  oblist
S :  oblist
F :  ->  LIST
D :  [List with all the symbols of objects in the current environment.]
---------------------------------

N :  trace
S :  (trace)
F :  ->  nil
D :  (trace) ^= nil
                [As a side effect switches the trace-flag.]
---------------------------------
\end{verbatim}
\newpage
\section*{References}
\begin{verbatim}
[A*89]  Almeida, J.J., Barros, J.B., Castro, P.M., Madeira, F.C.,
        "Preprocessador para YARPT", Rel. JNICT:PMCT:87.66:JJA1,
        University of Minho, October 1989.

[HM85]  Henderson, P., Minkowitz, C. 
        "The metoo Method of Software Design", Dep. of Computing
        Science, University of Stirling, Rep. FN/10, 1985.

[Jo80]  Jones, C.
        "Software Development - A Rigorous Approach"
        Prentice-Hall International, 1980.

[Jo86]  Jones, C.
        "Systematic Software Development Using VDM"
        Prentice-Hall International, 1986.

[Pi89]  Pinto, A.
        "Desenvolvimento de xmetoo Um Nucleo para Prototipagem
        Rapida de Especicacoes VDM",
        LESI Final Dissertation, University of Minho, 1989.

[Ma89]  Magalhaes, P.
        "Desenvolvimento de YARPT - Ferramenta para Prototipagem
        Rapida de Software",
        LESI Final Dissertation, University of Minho, 1989.
\end{verbatim}

\end{document}

N :  GRAMATICA GERAL DO NYAGSL CAMILA
N :  GRAMMAR
---------------------------------------------------------------------

texto -> ( deftypes | bloco ) +

deftypes : "TYPE" deftipo (";" deftipo )* "ENDTYPE'

deftipo : SIMB "=" deftp 
        | SIMB "::" deftp 

deftp : SIMB                            
      | deftp ("|" deftp)+                  {* ALTernativas *}
      | (SIMB ":" deftp)+                   {* TUPlo *}
      | deftp "->" deftp                    {* FF *}
      | deftp "<->" deftp                   {* RELacao binaria *}
      | deftp-list                          {* LISTa *}
      | deftp-set                           {* SET *}
      | "[" deftp "]"                       {* tipo opcional *}

bloco : ( elemento ";" )*

elemento : deffunccao | directivas | exp
     
directivas : "#include" file                {* preprocessa e inclui file *}
           | "#includemetoo" filemetoo      {* inclui file em xmetoo     *}
           | "#debugon"                     {*                           *}
           | "#debugoff"                    {*                           *}

deffuncao :  SIMB "(" argumentos ")" "=" exp
          |  "FUNC" SIMB "(" argum_tipos ")" ":" tipos  {* assinatura *}
             ["PRE" exp ["->" exp]]           {* precondicao          *}
             ["STATE" exp]                    {* alteracao do estado  *}
             ["RETURN" exp]                   {* valor devolvido      *}
          
argumentos : id ( "," id )*
           |                              {* vazio                *}

tipo : deftp 
     | "(" identificador_estado ")"
 
exp      : SIMB                           {* Identificador xmetoo *}
         | "(" exp ")"                    {* Alterar prioridades  *}
         | STRING                         {* string entre aspas   *}
         | defobj                         {* definicao de estado  *}
         | SIMB "(" explist ")"           {* invocacao de funcao  *}
         | "(" exp ")" "(" explist ")"    {* invocacao de funcao  *}
         | exp "[" exp "]"                {* (aply exp exp)       *}
         | seqexp                         {* Sequencia            *}
         | setexp                         {* Conjunto             *}
         | ffexp                          {* Funcao finita        *}
         | relexp                         {* Relacao binaria      *}
         | letexp                         
         | ifexp                    
         | boolexp                        {* expressao booleana   *}
         | exp "\" exp                    {* dom subtract *}
         | exp "/" exp                    {* dom restrict *}
         | exporio                        {* somatorio, func-orio *}

defobj   : SIMB  "<-" exp                 {* define/redefine estado *}

exporio  : SIMB "-orio" "("exp ","exp ")" {* add-orio(neutro,conj)  *}

intexp : INTEIRO
       | "#" exp                          {* cardinal *}
       | exp .+ exp                       {* +                     *}
       | exp .- exp                       {* -                     *}
       | exp .* exp                       {* *                     *}
       | exp ./ exp                       {* /                     *}

boolexp  : exp "in" exp                   {* member *}
         | exp "notin" exp                {* not member *}
         | exp "/\" exp                   {* and *}
         | exp "&&" exp                   {* and *}
         | exp "\/" exp                   {* or *}
         | exp "||" exp                   {* or *}
         | "~" exp                        {* not *}
         | exp "==" exp                   {* equal *}
         | exp "!=" exp                   {* diferente *}
         | "(" exp ">" exp ")"            {* gt *}
         | "(" exp "<" exp ")"            {* lt *}
         | exp ">=" exp                   {* geq *}
         | exp "<=" exp                   {* leq *}
         | exp "=>" exp                   {* =>  *}
         | "is-" SIMB "(" exp ")"         {* (is SIMB exp) *}
         | false                          {* constante falso *}
         | true                           {* constante verdade *}
         | "all(" exp "<-" exp (, ... ) ":" exp ")"  
                                          {* quantificador univ. *}
         | "exist(" exp "<-" exp (, ... ) ":" exp ")"  
                                          {* quantificador existen. *}
         | "exist1(" exp "<-" exp (, ... ) ":" exp ")"  
                                          {* quantificador existen. *}

setexp : "{" exp "|" fromlist  "}"        {* conj em compreensao *}
       | "{" exp-list "}"                 {* conj em extensao    *}
       | exp "*" exp                      {* intersection *}
       | exp "U" exp                      {* union        *}
       | exp "-" exp                      {* difference   *}

seqexp : "<" exp "|" fromlist ">"         {* seq em compreensao *} 
       | "<" exp-list ">"                 {* seq em extensao    *}
       | "<" exp ":" exp ">"              {* (cons exp exp)     *}
       | exp "^" exp                      {* (append exp exp)   *}

fromlist : from ("," from)*

from     : SIMB "<-" exp                  {* (from SIMB exp)    *}
         | SIMB "<-" exp ":" cond         {* (from SIMB exp cond) *}

ffexp  : "[" exp "->" exp "|" from "]"    {* ff em comprensao     *} 
       | "[" exppair-list "]"             {* makeff *}
       | exp "+" exp                      {* plus *}

relexp : "[*" "<" exp "," exp ">" "|" fromlist "*]"   
                                    {* Rel Binaria em compreensao *}
       | "[*" exppair-list "*]"     {* makerel                    *}

exppair : exp "->" exp

letexp   : "let" "(" deflist ")" "in" exp  
 
deflist  : def ("," def)*

def     : SIMB "=" exp 

ifexp  : "if"  exp "then" exp            
       | "if"  exp "then" exp "else" exp   
       | "if" "(" caselist ")" ["otherwise" exp]  {*comandos guardados*}

caselist : exp "->" exp ("," exp "->" exp )*

cond     : exp                         
---------------------------------------------------------------------

N :  QUANTIFICADORES
ALL     	: SYM SET BOOL ->  BOOL
all( simb1 <- set1 , simb2 <- set2 , ... : expbool)
EXIST   	: SYM SET BOOL ->  BOOL
exist( simb <- set : expbool)
EXIST1  	: SYM SET BOOL ->  BOOL
exist1( simb <- set : expbool)

---------------------------------------------------------------------

N :  LOGICAS
N :  LOGIC
and(&&)     	: BOOL BOOL  ->  BOOL
         | exp "/\" exp                   {* and *}
         | exp "&&" exp                   {* and *}
not(~)     	: BOOL  ->  BOOL
         | "~" exp                        {* not *}
or(||)      	: BOOL BOOL  ->  BOOL
         | exp "\/" exp                   {* or *}
         | exp "||" exp                   {* or *}
implica    exp "=>" exp
false   	: ->  BOOL
true    	: ->  BOOL

---------------------------------------------------------------------
N :  RELATIONAL
N :  OP RELACIONAIS
eq      	: S-EXP S-EXP  ->  BOOL
equal(==)   	: S-EXP S-EXP  ->  BOOL
geq (>=)    	: INT INT  ->  BOOL /  STR STR  ->  BOOL
gt      	: INT INT  ->  BOOL /  STR STR  ->  BOOL
lt      	: INT INT  ->  BOOL /  STR STR  ->  BOOL
neq     	: S-EXP S-EXP  ->  BOOL
nequal(!=)  	: S-EXP S-EXP  ->  BOOL

---------------------------------------------------------------------

N :  INTEIRAS
N :  INTEGER
add    		: INT INT  ->  INT
sub    		: INT INT  ->  INT
mul    		: INT INT  ->  INT
div    		: INT INT  ->  INT
rem    		: INT INT  ->  INT
max    		: INT+  ->  INT
min    		: INT+  ->  INT
abs    		: INT  ->  INT
ascii  		: STR  ->  INT
atoi   		: STR  ->  INT
card         	: SET  ->  INT /  REL  ->  INT
chr    		: INT  ->  STR
itoa   		: INT  ->  STR
length   	: LIST  ->  INT
strlen 		: STR*  ->  INT

---------------------------------------------------------------------
N :  SET
N :  CONJUNTOS
difference(-)  	: SET SET  ->  SET 
intersection(*)	: SET SET  ->  SET
union(U)       	: SET SET  ->  SET
empty        	: ->  SET
UNION        	: SET  ->  SET
makeset      	: S-EXP*  ->  SET
isempty 	: SET  ->  BOOL 
member(in)  	: S-EXP SET  ->  BOOL
       exp "notin" exp                {* not member *}
       exp "in" exp                   {* member *}
subset       	: SET SET  ->  BOOL 
card         	: SET  ->  INT 
choice       	: SET  ->  S-EXP
dom          	: REL  ->  SET /  FF  ->  SET
elems    	: LIST  ->  SET
inseg        	: INT  ->  SET
ran          	: REL  ->  SET /  FF  ->  SET
set          	: S-EXP {SYM (LIST|SET) [BOOL]}+  ->  SET
the          	: SET  ->  S-EXP 

---------------------------------------------------------------------
N :  SEQ
N :  LISTAS
CONC     	: LIST  ->  LIST
append   	: LIST LIST+  ->  LIST
cons     	: S-EXP LIST  ->  LIST
el(=nth)       	: INT LIST  ->  S-EXP
elems    	: LIST  ->  SET
head(=hd)     	: LIST  ->  S-EXP
inds     	: LIST  ->  LIST
length   	: LIST  ->  INT
makeseq(=list) 	: S-EXP*  ->  LIST
nil      	: ->  LIST
pair     	: S-EXP S-EXP  ->  LIST
plusq    	: LIST FF  ->  LIST
reduce   	: S-EXP SYM LIST  ->  S-EXP
reverse  	: LIST  ->  LIST
seq      	: S-EXP {SYM (LIST|SET) [BOOL]}+  ->  LIST
tail(=tl)     	: LIST  ->  LIST
first(=p1)  	: LIST INT  ->  S-EXP
second(=p2) 	: LIST INT  ->  S-EXP
third  		: LIST INT  ->  S-EXP
fourth 		: LIST INT  ->  S-EXP
fifth  		: LIST INT  ->  S-EXP

---------------------------------------------------------------------
N :  FF
N :  Finite Function
N :  FUNCOES FINITAS (MAPPINGS)
isempty 	: FF  ->  BOOL
ap      	: FF S-EXP [S-EXP]  ->  S-EXP
dom          	: FF  ->  SET
dr      	: FF SET  ->  FF
ds      	: FF SET  ->  FF
ff      	: SYM SET S-EXP [BOOL]  ->  FF
makeff  	: {S-EXP S-EXP}*  ->  FF
plus    	: FF FF  ->  FF
plusq    	: LIST FF  ->  LIST
ran          	: FF  ->  SET

---------------------------------------------------------------------

N :  RELACOES BINARIAS
isempty 	: REL  ->  BOOL
member  	: S-EXP REL  ->  BOOL
subset       	: REL REL  ->  BOOL
card         	: REL  ->  INT
choice       	: REL  ->  S-EXP
difference   	: REL REL  ->  REL
dom          	: REL  ->  SET
dr      	: REL SET  ->  REL
ds      	: REL SET  ->  REL
intersection 	: REL REL  ->  REL
makerel 	: {S-EXP S-EXP}*  ->  REL
ran          	: REL  ->  SET
the          	: REL  ->  S-EXP
union        	: REL REL  ->  REL
---------------------------------------------------------------------
