N :  GRAMATICA GERAL DO NYAGSL
---------------------------------------------------------------------

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                     {* add *}
       | exp ".-" exp                     {* sub *}
       | exp ".*" exp                     {* mul *}
       | exp "./" exp                     {* div *}

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 *}
         | "is-" SIMB "(" exp ")"         {* (is SIMB exp) *}
         | false                          {* constante falso *}
         | true                           {* constante verdade *}
         | all( simb1 <- set1 , simb2 <- set2 , ... : expbool)
         | exist( simb <- set : boolexp)
         | exist1( simb <- set : boolexp)

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 "|" fromlist "]"{* 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
and(&&)     	: BOOL BOOL  ->  BOOL
         | exp "&&" exp                   {* and *}
not(~)     	: BOOL  ->  BOOL
         | "~" exp                        {* not *}
or(||)      	: BOOL BOOL  ->  BOOL
         | exp "||" exp                   {* or *}
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
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  		: LIST INT  ->  S-EXP
second 		: LIST INT  ->  S-EXP
third  		: LIST INT  ->  S-EXP
fourth 		: LIST INT  ->  S-EXP
fifth  		: LIST INT  ->  S-EXP

---------------------------------------------------------------------
N :  FF
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
---------------------------------------------------------------------

N :  ALL
S :  all( simb1 <- set1 , simb2 <- set2 , ... : expbool)
     (ALL exp1 exp2 exp3)
F :  SYM SET BOOL  ->  BOOL
     (ALL s set pred) ^= [Implementa o quantificador universal, sendo 's' a 
                          variavel quantificada, 'set' o dominio da
                          quantificacao e 'pred' o predicado;
                          o resultado e' "false" e o calculo termina quando,
                          para um dos elementos, eval( pred ) = "false";
                          o resultado e' "true" se se obtiver sucesso na  
                          quantificacao;
                          as expressoes 'set' e 'pred' sao parcialmente 
                          validadas sintaticamente, no caso de conterem
                          subexpressoes que definam variaveis locais ("let", 
                          "lambda", "ALL", "EXIST", "EXIST1", "ff", "set", 
                          "seq", "foreach")]
---------------------------------
N :  abs
S :  abs( exp1)
     (abs exp1)
F :  INT  ->  INT
     (abs e1) ^= | e1 |
---------------------------------
N :  add  
S :  add( exp1 exp2)
     (add exp1 exp2)
F :  INT INT  ->  INT
     (add e1 e2) ^= eval( e1 ) + eval( e2 )
---------------------------------
N :  and 
S :  exp "&&" exp                   {* and *}
     (and exp1 exp2)
F :  BOOL BOOL  ->  BOOL
     (and e1 e2) ^= eval( e1 ) andif eval( e2 )
---------------------------------
N :  ap
N :  aply
S :  exp "[" exp "]"                {* (aply exp exp)       *}
     (ap exp1 exp2 [exp3])
F :  FF S-EXP [S-EXP]  ->  S-EXP
     (ap e1 e2 e3) ^= let f = eval( e1 )
                          s2 = eval( e2 )
                      in if el_set( s2, dom( f ))
                         then f(s2)
                         else eval( e3 )
                              ["nil" caso nao exista e3]
---------------------------------
N :  append
S :  exp "^" exp                      {* (append exp exp)   *}
     (append exp1 exp2+)
F :  LIST LIST+  ->  LIST
     (append e1 .. en) ^= eval( e1 ) ^ .. ^ eval( en )
---------------------------------
N :  ascii  
S :  ascii( exp1)
     (ascii exp1)
F :  STR  ->  INT
     (ascii e1) ^= [codigo ascii do primeiro caracter de eval( e1 );
                    se eval( e1 ) for "" o resultado e' 0]
---------------------------------
N :  atoi  
S :  atoi( exp1)
     (atoi exp1)
F :  STR  ->  INT
P :  [string numerica]
     (atoi e1) ^= [inteiro representado pela "string" eval( e1 ); os espacos
                   iniciais sao desprezados; sao considerados apenas o sinal
                   (opcional) e os digitos ate' ao primeiro caracter nao nu-
                   merico; em caso de erro e' retornado o valor 0]
---------------------------------
N :  atom 
S :  atom( exp1)
     (atom exp1)
F :  S-EXP  ->  BOOL
     (atom e1) ^= let s1 = eval( e1 )
                  in s1 = nil orif
                     el_set( type( s1 ),
                             {INT, STR, SYM, SUBR, FPTR, CHAN(Config. "COMM")} )
---------------------------------
N :  card
S :  card( exp1)
     (card exp1)
F :  SET  ->  INT
     REL  ->  INT
     (card e1) ^= [numero de elementos do conjunto/relacao eval( e1 )]
---------------------------------
N :  choice
S :  choice( exp1)
     (choice exp1)
F :  SET  ->  S-EXP
     REL  ->  S-EXP
P :  eval( exp1 ) != {}
     (choice e1) ^= [um elemento do conjunto/relacao eval( e1 );
                     implementado de forma a dar o primeiro da lista que
                     representa o conjunto]
---------------------------------
N :  chr 
S :  chr( exp1)
     (chr exp1)
F :  INT  ->  STR
     (chr e1) ^= ["string" com o caracter cujo codigo ascii e' eval( e1 )]
---------------------------------
N :  CONC
S :  CONC( exp1)
     (CONC exp1)
F :  LIST  ->  LIST
P :  [os elementos de eval( exp1 ) sao listas]
     (CONC e1) ^= l1 ^ l2 ^ ... ^ lk
                  [em que l1..lk sao as listas elementos da lista eval( e1 )]
---------------------------------
N :  cons
S :  "<" exp ":" exp ">"              {* (cons exp exp)     *}
     (cons exp1 exp2)
F :  S-EXP LIST  ->  LIST
     Configs "nao LAZY": (cons e1 e2) ^= <eval( e1 )> ^ eval( e2 )
     Config. "LAZY": (cons e1 e2) ^= <delay( e1 )> ^ delay( e2 )
---------------------------------
N :  difference
S :  exp "-" exp                      {* difference   *}
     (difference exp1 exp2)
F :  SET SET  ->  SET
     REL REL  ->  REL 
     (difference e1 e2) ^= eval( e1 ) - eval( e2 )
---------------------------------
N :  div 
S :  div( exp1 exp2)
     (div exp1 exp2)
F :  INT INT  ->  INT
     (div e1 e2) ^= eval( e1 ) div eval( e2 )
---------------------------------
N :  dom
S :  dom( exp1)
     (dom exp1)
F :  REL  ->  SET
     FF  ->  SET
     (dom e1) ^= [dominio da relacao/funcao finita eval( e1 )]
---------------------------------
N :  dr
S :  exp "/" exp                    {* dom restrict *}
     (dr exp1 exp2)
F :  REL SET  ->  REL
     FF SET  ->  FF
     (dr e1 e2) ^= [restringe o dominio da relacao/funcao finita eval( e1 )
                    ao conjunto eval( e2 )]
     seja rf = ((1 b) (2 g) (8 h) (9 h))
     (dr rf (makeset 1 2)) = ((1 b) (2 g))
---------------------------------
N :  ds
S :  exp "\" exp                    {* dom subtract *}
     (ds exp1 exp2)
F :  REL SET  ->  REL
     FF SET  ->  FF
     (ds e1 e2) ^= [elimina do dominio da relacao/funcao finita eval( e1 )
                    os elementos do conjunto eval( e2 )]
     seja rf = ((1 b) (2 g) (8 h) (9 h))
     (ds rf (makeset 1 2)) = ((8 h) (9 h))
---------------------------------
N :  el  ( nth )
S :  el( exp1 exp2)
     (el exp1 exp2)
F :  INT LIST  -> S-EXP
P :  0 < eval( exp1 ) <= [comprimento da lista eval( exp2 )]
     (el e1 e2) ^= [eval( e1 )-esimo elemento da lista eval( e2 )]
---------------------------------
N :  elems
S :  elems( exp1)
     (elems exp1)
F :  LIST  ->  SET
     (elems e1) ^= [conjunto dos elementos da lista eval( e1 )]
---------------------------------
N :  empty
S :  empty
F :  ->  SET
     empty ^= {} [representado por "nil"]
---------------------------------
N :  eq
S :  eq( exp1 exp2)
     (eq exp1 exp2)
F :  S-EXP S-EXP  ->  BOOL
     (eq e1 e2) ^= let s1 = eval( e1 )
                       s2 = eval( 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(Config. "COMM")) or
                         (type( s1 ) = type( s2 ) = SUBR) 
                      then @s1 = @s2
                      else if type( s1 ) = type( s2 ) = SYM
                           then s1 = s2
                           else false
---------------------------------
N :  equal
S :  exp "==" exp                   {* equal *}
     (equal exp1 exp2)
F :  S-EXP S-EXP  ->  BOOL
     (equal e1 e2) ^= (eq e1 e2) orif eval( e1 ) = eval( e2 )
---------------------------------
N :  EXIST
S :  EXIST( exp1 exp2 exp3)
     (EXIST exp1 exp2 exp3)
F :  SYM SET BOOL  ->  BOOL
     (EXIST s set pred) ^= [Implementa o quantificador existencial, sendo 's' a 
                            variavel quantificada, 'set' o dominio da
                            quantificacao e 'pred' o predicado;
                            o resultado e' "true" se se obtiver sucesso na  
                            quantificacao;
                            as expressoes 'set' e 'pred' sao parcialmente 
                            validadas sintaticamente, no caso de conterem
                            subexpressoes que definam variaveis locais ("let", 
                            "lambda", "ALL", "EXIST", "EXIST1", "ff", "set", 
                            "seq", "foreach")]
---------------------------------
N :  EXIST1
S :  EXIST1( exp1 exp2 exp3)
     (EXIST1 exp1 exp2 exp3)
F :  SYM SET BOOL  ->  BOOL
     (EXIST1 s set pred) ^= [Implementa o quantificador existencial exclusivo,
                             sendo 's' a variavel quantificada, 'set' o 
                             dominio da quantificacao e 'pred' o predicado;
                             o resultado e' "false" e a quantificacao termina se
                             se encontrar um "segundo" 's' para o qual 
                             eval( pred ) = "true" ou se eval( pred ) = "false"
                             para todos os 's';
                             as expressoes 'set' e 'pred' sao parcialmente 
                             validadas sintaticamente, no caso de conterem
                             subexpressoes que definam variaveis locais ("let",
                             "lambda", "ALL", "EXIST", "EXIST1", "ff", "set", 
                             "seq", "foreach")]
---------------------------------
N :  false
S :  false
F :  ->  BOOL
     [constante booleana cujo valor e' o simbolo "false"]
---------------------------------
N :  ff
S :  ff( exp1 exp2 exp3 [exp4])
     (ff exp1 exp2 exp3 [exp4])
F :  SYM SET S-EXP [BOOL]  ->  FF
     (ff sim set e b) ^= [funcao finita cujo dominio e' formado pelos
                          elementos 'sim' do conjunto eval( set ) que verifi-
                          cam eval( b ); o contra-dominio e' formado por 
                          eval( e ) no ambiente aumentado por 'sim'; 
                          'sim' e' local a "ff" e o seu ambito sao as expressoes
                          'e' e 'b', nao fazendo sentido o seu uso em 'set';
                          as expressoes 'set', 'e' e 'b' sao parcialmente 
                          validadas sintaticamente, no caso de conterem
                          subexpressoes que definam variaveis locais ("let", 
                          "lambda", "ALL", "EXIST", "EXIST1", "ff", "set", 
                          "seq", "foreach")]
     (ff x (makeset 1 2 3) (add x 1) (not (eq x 2))) = ((1 2) (3 4))
---------------------------------
N :  geq
S :  exp ">=" exp                   {* geq *}
     (geq exp1 exp2)
F :  INT INT  ->  BOOL
     STR STR  ->  BOOL
     (geq e1 e2) ^= eval( e1 ) >= eval( e2 )
---------------------------------
N :  gt 
S :  "(" exp ">" exp ")"            {* gt *}
     (gt exp1 exp2)
F :  INT INT  ->  BOOL
     STR STR  ->  BOOL
     (gt e1 e2) ^= eval( e1 ) > eval( e2 )
---------------------------------
N :  head  ( hd )
S :  head( exp1)
     (head exp1)
F :  LIST  ->  S-EXP
P :  eval( exp1 ) != <>
     Configs "nao LAZY": (head e1) ^= [primeiro elemento de eval( e1 )]
     Config "LAZY":
        (head e1) ^= if type( e1 ) = "lazy-list"
                     then eval( [primeiro elemento de e1] )
                     else let s1 = eval( e1 )
                          in if type( s1 ) = "lazy-list"
                             then eval( [primeiro elemento de s1] )
                             else [primeiro elemento de s1]
---------------------------------
N :  inds
S :  inds( exp1)
     (inds exp1)
F :  LIST  ->  LIST
     (inds <>) = <>
     (inds e1) ^= [lista constituida pelos naturais 1..comprimento da
                   lista eval( e1 )]
    
---------------------------------
N :  inseg
S :  inseg( exp1)
     (inseg exp1)
F :  INT  ->  SET
     (inseg e1) ^= [conjunto formado pelos naturais 1..eval( e1 )] 
---------------------------------
N :  intersection
S :  exp "*" exp                      {* intersection *}
     (intersection exp1 exp2)
F :  SET SET  ->  SET
     REL REL  ->  REL
     (intersection e1 e2) ^= eval( e1 ) /\ eval( e2 )
---------------------------------
N :  isempty
S :  isempty( exp1)
     (isempty exp1)
F :  SET  ->  BOOL
     REL  ->  BOOL
     FF  ->  BOOL
     (isempty e1) ^= eval( e1 ) = {}/[]
---------------------------------
N :  itoa  
S :  itoa( exp1)
     (itoa exp1)
F :  INT  ->  STR
     (itoa e1) ^= ["string" formada pelos digitos (e sinal) do inteiro
                   eval( e1 )]
---------------------------------
N :  length
S :  length( exp1)
     (length exp1)
F :  LIST  ->  INT
     (length e1) ^= [comprimento de eval( e1 )]
---------------------------------
N :  leq
S :  exp "<=" exp                   {* leq *}
     (leq exp1 exp2)
F :  INT INT  ->  BOOL
     STR STR  ->  BOOL
     (leq e1 e2) ^= eval( e1 ) <= eval( e2 )
---------------------------------
N : list ( makeseq )
S : (list exp1*)
F : S-EXP*  ->  LIST
    (list) ^= <>
    (list e1 ... ek) ^= <eval( e1 ) ... eval( ek )>
---------------------------------
N :  lt 
S :  "(" exp "<" exp ")"            {* lt *}
     (lt exp1 exp2)
F :  INT INT  ->  BOOL
     STR STR  ->  BOOL
     (lt e1 e2) ^= eval( e1 ) < eval( e2 )
---------------------------------
N :  makeff
S :  "[" exppair-list "]"             {* makeff *}
     (makeff {(exp1 exp2)}*)
F :  {S-EXP S-EXP}*  ->  FF
P :  [nao ha elementos repetidos no dominio]
     (makeff) ^= []
     (makeff (e1 e2) ... (ek ek+1)) ^=
           [eval( e1 ) -> eval( e2 ), ..., eval( ek ) -> eval( ek+1 )]
---------------------------------
N :  makerel
S :  "[*" exppair-list "*]"     {* makerel                    *}
     (makerel {(exp1 exp2)}*)
F :  {S-EXP S-EXP}*  ->  REL
     (makerel) ^= {}
     (makerel (e1 e2) ... (ek ek+1)) ^=
              { <eval( e1 ), eval( e2 )>, ..., <eval( ek ), eval( ek+1 )>}
---------------------------------
N :  makeseq  ( list )
S :  "<" exp-list ">"                 {* seq em extensao    *}
     (makeseq exp1*)
F :  S-EXP*  ->  LIST
     (makeseq) ^= <>
     (makeseq e1..ek) = <eval( e1 ), ..., eval( ek )>
---------------------------------
N :  makeset
S :  "{" exp-list "}"                 {* conj em extensao    *}
     (makeset exp1*)
F :  S-EXP* -> SET
     (makeset) ^= {}
     (makeset e1 ... ek) ^= {eval( e1 ), ..., eval( ek )}
---------------------------------
N :  max
S :  max( exp1+)
     (max exp1+)
F :  INT+  ->  INT ou
     STR+  ->  STR
     (max e1..ek) ^= ei [maior valor de { e1, ..., ek }]
---------------------------------
N :  member
S :  member( exp1 exp2)
     (member exp1 exp2)
F :  S-EXP SET  ->  BOOL
     S-EXP REL  ->  BOOL
     (member e1 e2) ^= el_set( eval( e1 ), eval( e2 ))
---------------------------------
N :  min
S :  min( exp1+)
     (min exp1+)
F :  INT+  ->  INT ou
     STR+  ->  STR
     (min e1..ek) ^= ei (menor valor de { e1, ..., ek })
---------------------------------
N :  mul
S :  mul( exp1 exp2)
     (mul exp1 exp2)
F :  INT INT  ->  INT
     (mul e1 e2) ^= eval( e1 ) * eval( e2 )
---------------------------------
N :  neq
S :  neq( exp1 exp2)
     (neq exp1 exp2)
F :  S-EXP S-EXP  ->  BOOL
     (neq e1 e2) ^= not( eq( e1 e2 ) ) [ver funcao "eq"]
---------------------------------
N :  nequal
S :  exp "!=" exp                   {* diferente *}
     (nequal exp1 exp2)
F :  S-EXP S-EXP  ->  BOOL
     (nequal e1 e2) ^= not( equal( e1 e2) ) [ver funcao "equal"]
---------------------------------
N :  nil
S :  nil
F :  -> S-EXP
     nil ^= <>
---------------------------------
N :  not
S :  "~" exp                        {* not *}
     (not exp1)
F :  BOOL  ->  BOOL
     (not e1) ^= if eval( e1 )
                 then "true"
                 else "false"
---------------------------------
N :  null  
S :  null( exp1)
     (null exp1)
F :  S-EXP  ->  BOOL
     (null e1) ^= eval( e1 ) = nil
---------------------------------
N :  or 
S :  exp "||" exp                   {* or *}
     (or exp1 exp2)
F :  BOOL BOOL  ->  BOOL
     (or e1 e2) ^= eval( e1 ) orif eval( e2 )
---------------------------------
N :  pair
S :  pair( exp1 exp2)
     (pair exp1 exp2)
F :  S-EXP S-EXP  ->  LIST
     (pair e1 e2) ^= <eval( e1 ), eval( e2 )>
---------------------------------
N :  plus
S :  exp "+" exp                      {* plus *}
     (plus exp1 exp2)
F :  FF FF  ->  FF
     (plus f1 f2) ^= [funcao finita cujo dominio e' a uniao dos dominios de
                      eval( f1 ) e eval( f2 ); a cada elemento do dominio
                      e' associado o elemento do contra-dominio da funcao que
                      lhe diz respeito; no caso de um elemento pertencer aos
                      dois dominios e'-lhe associado o elemento do contra-
                      -dominio de eval( f2 )]
     sejam f1 = ((q 2) (w 2) (e 3))
           f2 = ((q 3) (r 5) (h 4) (j 2))
     (plus f1 f2) = ((q 3) (w 2) (e 3) (r 5) (h 4) (j 2)) 
---------------------------------
N :  plusq
S :  plusq( exp1 exp2)
     (plusq exp1 exp2)
P :  dom( eval( exp2 ) ) C= elems( inds( eval( exp1 )))
F :  LIST FF  ->  LIST
     (plusq e1 e2) ^= [lista eval( e1 ) reescrita nas posicoes determinadas
                       por 'i' pertencente a dom( eval( e2 )) pelo elemento
                       eval( e2 )(i)]
     seja f = ((1 4) (5 3) (2 2))
          l = (1 2 3 4 5 6)
     (plusq l f) = (4 2 3 4 3 6)
---------------------------------
N :  ran
S :  ran( exp1)
     (ran exp1)
F :  REL  ->  SET
     FF  ->  SET
     (ran e1) ^= [contra-dominio da relacao/funcao finita eval( e1 )]
---------------------------------
N :  reduce
S :  reduce( exp1 exp2 exp3)
     (reduce exp1 exp2 exp3)
F :  S-EXP SYM LIST  ->  S-EXP
     S-EXP SYM SET  ->  S-EXP
 
P :  [exp2 e' o nome de uma funcao binaria] and 
     [o tipo do resultado e' o mesmo do segundo argumento] and
     [o tipo de eval( exp1 ) e' o mesmo do segundo argumento] and
     [os elementos de eval( exp3 ) sao do tipo do primeiro argumento] and
     eval( exp3 ) != <> / {}
                 
     (reduce e s ls) ^= s( x1, s( x2, s( ..., s( xk, eval( e ))...)))
                        [em que eval( ls ) = <x1, ..., xk> / {x1, ..., xk}]
     (reduce nil cons (list 1 2 1 3 1 4 5 6)) = (1 2 1 3 1 4 5 6)
     (reduce 0 add (makeset 5 1 6 8 2)) = 22 
---------------------------------
N :  rem
S :  rem( exp1 exp2)
     (rem exp1 exp2)
F :  INT INT  ->  INT
     (rem e1 e2) ^= eval( e1 ) mod eval( e2 )
---------------------------------
N :  reverse
S :  reverse( exp1)
     (reverse exp1)
F :  LIST  ->  LIST  
     (reverse e1) ^= [lista eval( e1 ) invertida na ordem dos seus elementos]
---------------------------------
N :  seq
S :  seq( exp1 {(from exp2 exp3 [exp4]}+)
     (seq exp1 {(from exp2 exp3 [exp4]}+)
F :  S-EXP {SYM (LIST|SET) [BOOL]}+  ->  LIST
     (seq e1 (from s1 ls1 b1) ... (from sk lsk bk)) ^=
          [lista dos elementos resultantes de eval( e1 ) no ambiente aumentado
           pelos simbolos s1..sk; 'e1' e' calculado apenas quando a cada 'si'
           esta' associado um valor da lista/conjunto eval( lsi ); as listas/
           conjuntos sao totalmente percorridas/os e os predicados 'bi' sao
           testados para cada combinacao de valores; caso nao exista um 'bi'
           ele e' considerado "true"; uma combinacao so' e' valida quando 
           todos os 'bi' sao verificados; 'e1' pode ser funcao de todos os
           'si' para alem de outros simbolos nao locais a "seq"; os 'bi' podem
           ser funcao dos simbolos s1..si-1 para alem de outros simbolos nao 
           locais a "seq"; os simbolos 'si' sao mudos e locais a "seq"; um 
           simbolo 'si' nao deve ser incluido na expressao 'lsi' correspondente;
           as expressoes 'lsi' e 'bi' sao parcialmente validadas sintaticamente,
           no caso de conterem subexpressoes que definam variaveis locais 
           ("let", "lambda", "ALL", "EXIST", "EXIST1", "ff", "set", "seq", 
            "foreach")]
     (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 :  set
S :  set( exp1 {(from exp2 exp3 [exp4]}+)
     (set exp1 {(from exp2 exp3 [exp4]}+)
F :  S-EXP {SYM (LIST|SET) [BOOL]}+  ->  SET
     (set e1 (from s1 ls1 b1) ... (from sk lsk bk)) ^=
          [conj. dos elementos resultantes de eval( e1 ) no ambiente aumentado
           pelos simbolos s1..sk; 'e1' e' calculado apenas quando a cada 'si'
           esta' associado um valor da lista/conjunto eval( lsi ); as listas/
           conjuntos sao totalmente percorridas/os e os predicados 'bi' sao
           testados para cada combinacao de valores; caso nao exista um 'bi'
           ele e' considerado "true"; uma combinacao so' e' valida quando 
           todos os 'bi' sao verificados; 'e1' pode ser funcao de todos os
           'si' para alem de outros simbolos nao locais a "set"; os 'bi' podem
           ser funcao dos simbolos s1..si-1 para alem de outros simbolos nao 
           locais a "set"; os simbolos 'si' sao mudos e locais a "set"; um
           simbolo 'si' nao deve ser incluido na expressao 'lsi' correspondente;
           as expressoes 'lsi' e 'bi' sao parcialmente validadas sintaticamente,
           no caso de conterem subexpressoes que definam variaveis locais 
           ("let", "lambda", "ALL", "EXIST", "EXIST1", "ff", "set", "seq", 
            "foreach")]
     (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 :  strcat  
S :  strcat( exp1*)
     (strcat exp1*)
F :  STR*  ->  STR
P :  [o somatorio dos comprimentos das "strings"] <= 100
     (strcat) ^= ""
     (strcat e1 ... ek) ^= [concatenacao das "strings" 
                            eval( e1 ) ... eval( ek )]
---------------------------------
N :  strlen  
S :  strlen( exp1*)
     (strlen exp1*)
F :  STR*  ->  INT
     (strlen) ^= 0
     (strlen e1 ... ek) ^= [somatorio dos comprimentos das "strings" 
                            eval( e1 ) ... eval( ek )]
---------------------------------
N :  sub
S :  sub( exp1 exp2)
     (sub exp1 exp2)
F :  INT INT  ->  INT
     (sub e1 e2) ^= eval( e1 ) - eval( e2 )
---------------------------------
N :  subset
S :  subset( exp1 exp2)
     (subset exp1 exp2)
F :  SET SET  ->  BOOL
     REL REL  ->  BOOL
     (subset e1 e2) ^= eval( e1 ) C= eval( e2 )
---------------------------------
N :  substr  
S :  substr( exp1 exp2 [exp3])
     (substr exp1 exp2 [exp3])
F :  STR INT [INT]  ->  STR
     (substr e1 e2 e3) ^= ["substring" de eval( e1 ) iniciada na posicao
                            eval( e2 ) e formada por eval( e3 ) caracteres;
                            se eval( e2 ) < 1 ou eval( e2 ) > comprimento
                            da "string" eval( e1 ) o resultado e' ""; 
                            se nao existir o argumento 'e3' ou
                            se eval( e2 ) + eval( e3 ) > comprimento da 
                            "string" eval( e1 ) o resultado e' a "string" 
                            formada pelos caracteres seguintes a eval( e2 )
                            inclusive']
     (substr "abcdef" 2) = (substr "abcdef" 2 6) = "bcdef"
     (substr "abcdef" 2 -1) = ""
     (substr "abcdef" 2 3) = "bcd"
---------------------------------
N :  the
S :  the( exp1)
     (the exp1)
F :  SET  ->  S-EXP
     REL  ->  S-EXP
P :  [eval( exp1 ) contem um e um so' elemento]
     (the e1) ^= [o unico elemento do conjunto/relacao eval( e1 )]
---------------------------------
N :  true
S :  true
F :  ->  BOOL
     [constante booleana cujo valor e' o simbolo "true"]
---------------------------------
N :  tail  ( tl )
S :  tail( exp1)
     (tail exp1)
F :  LIST  ->  LIST
P :  eval( exp1 ) != <>
     Configs. "nao LAZY":
        (tail e1) ^= [eval( e1 ) retirando-lhe o primeiro elemento]
     Config. LAZY:
        (tail e1) ^= if type( e1 ) = "lazy-list"
                     then [e1 retirando-lhe o primeiro elemento]
                     else [eval( e1 ) retirando-lhe o primeiro elemento]
---------------------------------
N :  union 
S :  exp "U" exp                      {* union        *}
     (union exp1 exp2)
F :  SET SET  ->  SET
     REL REL  ->  REL
     (union e1 e2) ^= eval( e1 ) U eval( e2 )
---------------------------------
N :  UNION
S :  UNION( exp1)
     (UNION exp1)
F :  SET  ->  SET
P :  [os elementos de eval( exp1 ) sao conjuntos]
     (UNION e1) ^= s1 U s2 U ... U sk
                   [em que s1..sk sao os conjuntos elementos do conjunto
                    eval( e1 )]

8.2 Funcoes para comunicacao sincrona (Config. "COMM")
---------------------------------
N :  chanel
S :  chanel( exp1)
     (chanel exp1)
F :  STR  ->  CHAN 
     STR  ->  nil
P :  1 <= [comprimento de eval( exp1 )] <= 4
     (chanel e1) ^= [criacao de um canal de comunicacao de nome eval( exp1 );
                      da' "nil" como resultado caso nao consiga cria'-lo]
---------------------------------
N :  receive
S :  receive( exp1)
     (receive exp1)
F :  CHAN  ->  S-EXP
     (receive e1) ^= [expressao-S recebida pelo canal eval( e1 )]
---------------------------------
N :  send
S :  send( exp1 exp2)
     (send exp1 exp2)
F :  CHAN S-EXP  ->  S-EXP
P :  eval( exp2 ) = nil orif
     el_set( type( eval( exp2 )), {INT, STR, SYM, LIST, SET, REL, FF, FUN,
                                tipos def. pelo utilizador (Config. USERTYPE")})
     (send e1 e2) ^= eval( e2 )
                     [como efeito lateral, envia eval( e2 ) atraves do canal
                      eval( e1 )]

8.3 Funcoes condicionais
---------------------------------
N :  cond
S :  cond( {(exp1 exp2*)}*)
     (cond {(exp1 exp2*)}*)
F :  {BOOL S-EXP*}*  ->  S-EXP
     (cond) ^= nil
     (cond (b1 e1 ... ek) ... (bn en ... en+m)) ^=
          [calcula todas as expressoes 'ej' associadas ao primeiro 'bi' cujo 
           valor e' "true"; da' como resultado eval( [ultima expressao dessa 
           serie]); no caso de todos os 'bi' serem falsos o resultado e' "nil"]
     (cond (false (add 2 3))
           (true (def x 3) (def y 4) (add 4 5))
           ((lt 2 3) 'q)) = 9 ['x' e 'y' sao inseridos na tabela de simbolos
                              com os valores 3 e 4 respectivamente]
  
---------------------------------
N :  if
S :  "if"  exp "then" exp            
     "if"  exp "then" exp "else" exp   
     "if" "(" caselist ")" ["otherwise" exp]  {*comandos guardados*}
     (if exp1 exp2 [exp3])
F :  BOOL S-EXP [S-EXP]  ->  S-EXP
     (if e1 e2 e3) ^= if eval( e1 )
                      then eval( e2 )
                      else eval( e3 )
                           [e3 e' "nil" por defeito]
8.4 Aplicacao de funcoes definidas pelo utilizador
---------------------------------
S :  exp1( exp2*)
     (exp1 exp2*)
F :  FUN S-EXP*  ->  S-EXP
     SUBR S-EXP*  ->  S-EXP
P :  [tomar atencao `a ordem, tipo e numero de argumentos]
     (f e1 ... ek) ^=
        [E feito o calculo de f, "eval( f )"; 
         Testa-se o tipo do resultado:
          - se for SUBR, a funcao correspondente e' invocada com os parametros
            e1..ek
          - se for FUN, na config. "nao LAZY", e' invocada a funcao definida
            pelo utilizador apos serem ligados aos seus parametros formais os
            valores resultantes do calculo de e1..ek
          - se for FUN, na config. "LAZY", e' invocada a funcao definida pelo
            utilizador apos serem ligados aos seus parametros formais o resul-
            tado dos "delay" de e1..ek]
8.5 Definicoes locais
---------------------------------
N :  let
S :  "let" "(" deflist ")" "in" exp  
     (let ({(exp1 exp2)}*) exp3*)
F :  {SYM S-EXP}* S-EXP*  ->  S-EXP
     (let ((s1 e1) ... (sk ek)) exp1 ... expn) ^=
      [Config. "nao LAZY": para cada par ('si, 'ei') e' feito o eval( ei ) apos
      o que o ambiente e' alargado com o valor de 'si'; o processamento dos
      pares e' sequencial de 1 a k; 
      Config. "LAZY": sao ligados aos simbolos 'si' os valores respectivos 
      resultantes de delay( e1 )..delay( ek );
	  
      e' feito o "eval" das exp1..expn; o resultado de "let" e' eval( expn );
      caso nao existam 'expi' o resultado e' "nil";
      os simbolos s1..sk sao mudos nao tendo qualquer ligacao com simbolos
      com o mesmo nome definidos noutras expressoes; o ambito do simbolo 'si' e'
      exp1..expn;
      as expressoes 'ei' e 'expi' sao parcialmente validadas sintaticamente, no
      caso de conterem subexpressoes que definam variaveis locais ("let",
      "lambda", "ALL", "EXIST", "EXIST1", "ff", "set", "seq", "foreach")]

8.6 Definicao de funcoes e simbolos
---------------------------------
N :  def
S :  def( exp1 lambda (exp2*) exp3)
     (def exp1 lambda (exp2*) exp3)
     (def exp1 exp2)
F :  SYM SYM* S-EXP  ->  SYM
     SYM S-EXP  ->  SYM
P :  [exp1 nao pode ser um dos simbolos reservados da "shell"]
     (def s lambda (s1 ... sk) e1) ^= s
         [como efeito lateral faz a ligacao de 's' `a funcao definida pelo 
          utilizador com nome 's', parametros formais s1..sk e corpo 'e1'; os 
          parametros formais sao mudos nao tendo qualquer ligacao com simbolos
          com o mesmo nome definidos noutras expressoes; o simbolo 's' e' 
          inserido na lista de operadores associada ao simbolo "ops" (8.8.3)]
     (def s e1) ^= s
         [como efeito lateral liga 's' a eval( e1 ); o simbolo 's' e' inserido
          na lista de objectos associada ao simbolo "obs" (8.8.3)]
---------------------------------
N :  lambda
S :  lambda( (exp1*) exp2)
     (lambda (exp1*) exp2)
F :  SYM* S-EXP  ->  FUN
     (lambda (s1 ... sk) e1) ^=
        [funcao anonima definida pelo utilizador cujos parametros formais sao
         os simbolos 'si' e cujo corpo e' 'e1'; os parametros formais sao mudos
         nao tendo qualquer ligacao com simbolos com o mesmo nome definidos
         noutras expressoes; o ambito deles e' 'e1';
         a expressao 'e1' e' parcialmente validada sintaticamente, no caso de 
         conter subexpressoes que definam variaveis locais ("let", "lambda", 
         "ALL", "EXIST", "EXIST1", "ff", "set", "seq", "foreach");]

8.7 Definicao de tipos pelo utilizador (Config. "USERTYPE")

8.7.1 Relacao com a Sintaxe Abstracta VDM
Esta configuracao extende o "metoo" base permitindo ao utilizador a definicao de
tipos a um nivel de abstraccao identico ao da Sintaxe Abstracta VDM.
Numa clausula de "Sintaxe Abstracta Metoo" podem ser definidos tuplos, alter-
nativas, igualdades, funcoes finitas, relacoes binarias, listas, conjuntos e os
tipos atomicos simbolos, inteiros, "strings", "file pointers" e  canais (Config.
"COMM").

8.7.2 BNF das "expressoes de tipo"
    <exp tipo>    ::= <tuplo> | <alternativa> | <igualdade> | <funcao finita> |
                      <relacao binaria> | <lista> | <conjunto> | <atomico>
    <exp tipo1>   ::= <funcao finita> | <relacao binaria> | <lista> | 
                      <conjunto> | <atomico> | <identificador de tipo>
    <tuplo>       ::= 'TUP' { '(' <etiqueta> <exp tipo1> ')' }+
    <alternativa> ::= 'ALT' ['NIL'] <exp tipo1>+
    <igualdade>   ::= 'EQ' <identificador de tipo>
    <func finita> ::= 'FF' <exp tipo1> <exp tipo1>
    <relacao bin> ::= 'REL' <exp tipo1> <exp tipo1>
    <lista>       ::= 'LIST' <exp tipo1>
    <conjunto>    ::= 'SET' <exp tipo1>
    <atomico>     ::= 'SYM' | 'INT' | 'STR' | 'FPTR' | 'CHAN' (Config. "COMM") 
    <etiqueta>    ::= simbolo "metoo"
    <identificador de tipo> ::= simbolo "metoo"
8.7.3 Funcoes
8.7.3.1 Definicao
---------------------------------
N :  deftype
S :  deftype( exp1 exp2)
     (deftype exp1 exp2)
F :  SYM <exp tipo>  ->  SYM
P :  [exp1 nao pode ser um dos simbolos reservados da "shell"]
     (deftype t etipo) ^= t
                          [associa ao simbolo 't' o tipo definido pela expressao
                          'etipo'; em 'etipo' podem existir identificadores de
                          tipos ainda nao definidos; nao sao postas restricoes
                          a definicoes directa ou indirectamente recursivas;
                          o simbolo 't' passa a ser utilizavel como construtor
                          de objectos do seu tipo; no caso deste ser um tuplo as
                          etiquetas podem ser utilizadas como selectores - a
                          existencia de etiquetas com o mesmo nome em tuplos 
                          diferentes nao introduz confusao; no caso dos tuplos
                          os simbolos correspondentes `as etiquetas nao podem
                          ser reservados e o seu valor e' redefinido]
8.7.3.2 Construcao/Interrogacao
8.7.3.2.1 Compatibilidade expressoes - tipos
Considere-se "exp" uma expressao com valor de um dos seguintes tipos:
   tipo                 definicao                      "exp compativel t" se
------------------------------------------------------------------------------
 tuplo         (deftype t TUP (et1 c1) .. (etm cm))     exp e' do tipo t
 alternativa   (deftype t ALT a1 .. am)                EX i. exp compativel ai
 igualdade     (deftype t EQ t1)                        exp compativel t1
 lista         (deftype t LIST t1)                     exp e' do tipo t ou
 conjunto      (deftype t SET t1)        exp e' uma lista/conjunto constituida/o
                                             por elementos compativeis com t1
 relacao bin   (deftype t REL t1 t2)                   exp e' do tipo t ou
 funcao finita (deftype t FF t1 t2)       exp e' uma relacao/funcao com dominio/
                                       contra-dominio constituidos por elementos
                                                       compativeis com t1/t2
 atomicos      (deftype t ...)                         exp e' do tipo t ou
 (INT, SYM, ...)                             exp e' do tipo atomico que t define
------------------------------------------------------------------------------
A todos os tipos definidos pelo utilizador e' associado um construtor.
Estabelecendo um paralelo com o VDM, observa-se que este construtor so' e' 
obrigatorio na construcao de valores de tipo tuplo associando-lhes uma etiqueta.
Os construtores de alternativas nunca etiquetam os valores.
No caso dos tipos das algebras "metoo" e dos tipos atomicos o uso de construtor
e' facultativo. Se para a definicao de um valor for usado um construtor, o valor
sera' etiquetado. Note-se que um objecto etiquetado nunca e' compativel com o 
tipo de um objecto nao etiquetado.
8.7.3.2.2 Construcao
---------------------------------
N : [t - nome do tipo definido pelo utilizador atraves de "deftype"]
S :  t( exp1+)
     (t exp1+)
F :  S-EXP+  ->  t
     hipoteses:
       1: t define um tuplo -- TUP (et1 c1) .. (etm cm)
          construtor -- (t e1 .. en)
          pre'-condicao : (n = m) and (AL i. eval( ei ) compativel ci)
       2: t define uma alternativa -- ALT a1 .. am
          construtor -- (t e1)
          pre'-condicao : EX i. eval( e1 ) compativel ai
       3: t define uma igualdade -- EQ b
          construtor -- (t e1)
          pre'-condicao : eval( e1 ) compativel b
       4: t define uma lista/conjunto -- LIST/SET b
          construtor -- (t e1)
          pre'-condicao : [eval( e1 ) e' uma lista/conjunto cujos elementos sao 
                           compativeis com b]
       5: t define uma relacao bin./funcao finita -- REL/FF b c
          construtor -- (t e1)
          pre'-condicao : [eval( e1 ) e' uma relacao bin./funcao finita cujos 
                           elementos do dominio sao compativeis com b e os
                           elementos do contra-dominio sao compativeis com c] 
       6: t define um  tipo atomico -- INT/STR/SYM/FPTR/CHAN(Config. "COMM")
          construtor -- (t e1)
          pre'-condicao : [eval( e1 ) e' do tipo correspondente]
8.7.3.2.3 Interrogacao
---------------------------------
N :  is
S :  "is-" SIMB "(" exp ")"         {* (is SIMB exp) *}
     (is exp1 exp2)
F :  <exp tipo> S-EXP  ->  BOOL
     MACTYPE S-EXP  ->  BOOL
     (is tipo exp) ^= [se tipo e' uma macro de tipos ("MACTYPE") 
                          da' eval( exp ) compativel tipo representado pela
                                                     macro
                       senao eval( exp ) compativel 'tipo']
A definicao de uma macro e' feita pela funcao:
---------------------------------
N :  mactype
S :  mactype( exp1 exp2+)
     (mactype exp1 exp2+)
F :  SYM SYM+  ->  SYM
P :  [exp1 nao pode ser um dos simbolos reservados da "shell"]
     (mactype s slist) ^= s
                          [cria uma expressao do tipo "MACTYPE" associando-a
                           ao simbolo 's'; o valor de 's' na tabela de simbolos
                           e' redefinido;
                           a validacao sintatica da expressao de tipo 
                           representada por 'slist' sera' feita aquando do seu 
                           uso em "is"]
8.7.3.3 Eliminacao de etiquetas de um valor
Representacao interna de um valor de tipo definido pelo utilizador
  tuplos :  um valor e' representado por uma lista etiquetada com o nome do tipo
            correspondente;
  alternativas :  o nome de uma alternativa nunca e' usado como etiqueta;
  igualdades :  o valor e' sempre etiquetado com o nome da igualdade excepto
                quando o tipo final da cadeia de igualdades for uma alternativa;
  algebras "metoo"
  e atomicos :  o valor (representado da mesma forma que valores de tipos
                "xmetoo" correspondentes) e' etiquetado com o nome do tipo
                definido pelo utilizador.
Para que os valores de tipos definidos pelo utilizador possam ser operados por
funcoes da "shell", as etiquetas terao que ser removidas. Isso tera que ser
feito pela funcao:
---------------------------------
N :  ignlab
S :  ignlab( exp1)
     (ignlab exp1)
F :  S-EXP  ->  S-EXP 
     (ignlab exp) ^= [se exp nao e' um valor etiquetado
                         eval( exp ) seguido da remocao de etiquetas
                      senao da' exp sem as etiquetas]
8.8 Funcoes da "Shell"
8.8.1 Memoria
---------------------------------
N :  alloc
S :  alloc( exp1)
     (alloc exp1)
F :  INT  ->  INT
P :  eval( exp1 ) >= 1
     (alloc e1) ^= [altera o numero de nodos a alocar por segmento para 
                    eval( e1 ), retornando o valor anterior]
---------------------------------
N :  expand
S :  expand( [exp1])
     (expand [exp1])
F :  [INT]  ->  INT
P :  eval( exp1 ) >= 1
     (expand e1) ^= [tenta alocar eval( e1 ) segmentos (1 no caso de e1 nao
                     existir; retorna o numero de segmentos realmente alocados]
---------------------------------
N :  gc
S :  gc()
     (gc)
F :  -> nil
     (gc) ^= nil
           [como efeito lateral executa uma "garbage-collection"; se neces-
            sario e possivel aloca novo segmento]
---------------------------------
N :  mem
S :  mem()
     (mem)
F :  ->  nil
     (mem) ^= nil
            [como efeito lateral imprime no ecran as estatisticas:
             Nodes - numero de nodos alocados desde o inicio do processo ate'
                     ao momento
             Free nodes - numero de nodos livres nos segmentos que compoem a
                     memoria actual do interpretador
             Segments - numero de segmentos alocados ate' ao momento
             Allocate - numero de nodos a alocar por segmento quando for
                     necessario reservar novos segmentos
             Collections - numero de "garbage-collections" efectuadas ate' ao
                     momento]
8.8.2 "I/O" sobre Ficheiros
---------------------------------
N :  fclose  
S :  fclose( exp1)
     (fclose exp1)
F :  FPTR  ->  nil
P :  [o ficheiro apontado por eval( exp1 ) tem que estar aberto]
     (fclose e1) ^= nil
          [fecha o ficheiro apontado por eval( e1 )]
---------------------------------
N :  fgetc
S :  fgetc( [exp1])
     (fgetc [exp1])
F :  [FPTR]  ->  INT | nil
P :  [o ficheiro apontado por eval( exp1 ) tem que estar aberto]
     (fgetc e1) ^= [codigo ASCII do proximo caracter do ficheiro apontado por
                    eval( e1 ) (teclado por defeito); retorna "nil" caso se
                    atinja o fim do ficheiro]
---------------------------------
N :  fgets
S :  fgets( [exp1])
     (fgets [exp1])
F :  [FPTR]  ->  STR | nil
P :  [o ficheiro apontado por eval( exp1 ) tem que estar aberto]
     (fgets e1) ^= [proxima linha do ficheiro apontado por eval( e1 )
                    (teclado por defeito); retorna "nil" caso se atinja 
                    o fim do ficheiro]
---------------------------------
N :  fopen  
S :  fopen( exp1 exp2)
     (fopen exp1 exp2)
F :  STR STR  ->  FPTR | nil
     (fopen e1 e2) ^= ["file pointer" para o ficheiro de nome eval( e1 )
                        aberto em modo eval( e2 ); modos possiveis:
                          "r" - leitura de um ficheiro ja existente
                          "w" - escrita num ficheiro (re)criado
                          "a" - escrita apos fim de ficheiro 
                          "r+"- leitura/escrita num fich. ja existente
                          "w+"- leitura/escrita num ficheiro (re)criado
                          "a+"- leitura/escrita apos fim do ficheiro
                        caso nao consiga a abertura, retorna "nil"]
---------------------------------
N :  fputc
S :  fputc( exp1 [exp2])
     (fputc exp1 [exp2])
F :  INT [FPTR]  ->  INT
P :  [o ficheiro apontado por eval( exp2 ) tem que estar aberto]
     (fputc e1 e2) ^= eval( e1 )
        [como efeito lateral escreve no ficheiro eval( e2 ) (ecran por defeito)
         o caracter de codigo ASCII eval( e1 )]
---------------------------------
N :  fputs
S :  fputs( exp1 [exp2])
     (fputs exp1 [exp2])
F :  STR [FPTR]  ->  STR
P :  [o ficheiro apontado por eval( exp2 ) tem que estar aberto]
     (fputs e1 e2) ^= eval( e1 )
        [como efeito lateral escreve no ficheiro eval( e2 ) (ecran por defeito)
         a "string" eval( e1 )]
---------------------------------
N :  m2read
S :  m2read( exp1)
     (m2read exp1)
P : [o ficheiro apontado por eval( e1 ) tem que estar aberto para leitura]
F :  FPTR -> S-EXP
     (m2read e1) ^= [retorna "eval" da " expressao "S" lida do ficheiro apontado
                     por eval( e1 ); no caso de ser encontrado EOF termina em
                     erro] 
---------------------------------
N :  m2write
S :  m2write( exp1 exp2)
     (m2write exp1 exp2)
P : [o ficheiro apontado por eval( e1 ) tem que estar aberto para escrita] and
    (el_set( type( eval( exp2 )), {INT, STR, SYM, LIST, SET, REL, FF,
                               tipos def. pelo utilizador (Config. USERTYPE")}))
F :  FPTR S-EXP -> nil
     (m2write e1 e2) ^= nil
                        [como efeito lateral escreve o resultado de eval( e2 )
                         no ficheiro apontado por eval( e1 ) de forma que 
                         m2read( fp m2write( fp exp ) = exp]
 
---------------------------------
N :  stdin
S :  stdin
F :  ->  FPTR 
     [apontador para o "standard input" actual]
---------------------------------
N :  stdout
S :  stdout
F :  ->  FPTR 
     [apontador para o "standard output" actual]
---------------------------------
N :  readf
S :  readf( exp1)
     (readf exp1)
P : [o ficheiro apontado por eval( e1 ) tem que estar aberto para leitura]
F :  FPTR -> S-EXP
     (readf e1) ^= [retorna a expressao "S" lida do ficheiro apontado por
                    eval( e1 ); no caso de ser encontrado EOF termina em erro] 
---------------------------------
N :  writef
S :  writef( exp1 exp2)
     (writef exp1 exp2)
P : [o ficheiro apontado por eval( e1 ) tem que estar aberto para escrita] and
    (el_set( type( eval( exp2 )), {INT, STR, SYM, LIST, SET, REL, FF,
                               tipos def. pelo utilizador (Config. USERTYPE")}))
F :  FPTR S-EXP -> nil
     (writef e1 e2) ^= nil
                        [como efeito lateral escreve o resultado de eval( e2 )
                        no ficheiro apontado por eval( e1 )]
 
8.8.3 Diversas
---------------------------------
N :  eval
S :  eval( exp1)
     (eval exp1)
F :  S-EXP  ->  S-EXP
     (eval e1) ^= eval( eval( e1 ))
---------------------------------
N :  !
S :  (! [exp1])
     (! [exp1])
F :  [INT]  ->
     (! e1) ^= [unica forma de terminar a execucao do processo retornando 
                   eval( e1 ) (0 por defeito) ao sistema operativo]
---------------------------------
N :  foreach
S :  foreach( exp1 exp2 exp3*)
     (foreach exp1 exp2 exp3*)
F :  SYM LIST S-EXP*  ->  S-EXP
     (foreach s l e1 ... ek) ^=
        [liga-se sucessivamente "s" a todos os elementos de eval( l ) e calcu-
         lam-se as expressoes e1..ek em cada ambiente resultante; o resultado
         e' o valor da ultima expressao calculada; e' retornado "nil" caso 
         eval( l ) seja "nil" ou caso nao existam expressoes e1..ek;
         as expressoes 'l' e 'ei' sao parcialmente validadas sintaticamente, no
         caso de conterem subexpressoes que definam variaveis locais ("let",
         "lambda", "ALL", "EXIST", "EXIST1", "ff", "set", "seq", "foreach")]
---------------------------------
N :  load
S :  load( exp1)
     (load exp1)
F :  STR  ->  STR
     (load e1) ^= [le e calcula todas as expressoes "S" contidas no ficheiro
                   de nome eval( e1 ); retorna eval( e1 ); os resultados do
                   calculo das expressoes contidas no ficheiro nao sao 
                   visualizadas]
---------------------------------
N :  LOAD
S :  LOAD( exp1)
     (LOAD exp1)
F :  STR  -> 
     (LOAD e1) ^= [reinicializa o estado (guardado por "SAVE") carregando-o
                   do ficheiro com nome eval( e1 )]
---------------------------------
N :  oblist
S :  oblist
F :  ->  LIST
     [lista com todos os simbolos que constituem o estado]
---------------------------------
N :  obs
S :  obs
F :  ->  LIST
     [lista com os simbolos definidos atraves da funcao "def" usada na forma 
      "(def exp1 exp2)" (8.6)]
---------------------------------
N :  ops
S :  ops
F :  ->  LIST
     [lista com os simbolos (nomes de funcoes) definidos atraves da funcao "def"
     usada na forma "(def exp1 lambda (exp2*) exp3)" (8.6)]
---------------------------------
N :  PACK
S :  PACK( exp1)
     (PACK exp1)
F :  LIST  ->  SYM
     (PACK e1) ^= [simbolo cujo nome e' a concatenacao dos nomes dos simbolos 
                   e/ou inteiros positivos elementos da lista eval( e1 )]
---------------------------------
N :  princ
S :  princ( exp1*)
     (princ exp1*)
F :  S-EXP*  ->  nil
     (princ e1 .. ek) ^= nil
           [como efeito lateral imprime no ecran o eval( e1 ) .. eval( ek )]
---------------------------------
N :  print
S :  print( exp1*)
     (print exp1*)
F :  S-EXP*  ->  nil
     (print e1 .. ek) ^= nil
           [como efeito lateral imprime no ecran o eval( e1 ) .. eval( ek );
            ao imprimir uma "string", sao substituidos:
              -  "escape" por "\e"
              -  "newline" por "\n"
              -  "return" por "\r"
              -  "tab" por "\t"
              -  caracteres nao visiveis pelo seu codigo octal "\ddd"]
---------------------------------
N :  prog1
S :  prog1( exp1*)
     (prog1 exp1*)
F :  S-EXP*  ->  S-EXP
     (prog1) ^= nil
     (prog1 e1 ... ek) ^= [faz eval( e1 )..eval( ek );
                           retorna o valor eval( e1 )]
---------------------------------
N :  progn
S :  progn( exp1*)
     (progn exp1*)
F :  S-EXP*  ->  S-EXP
     (progn) ^= nil
     (progn e1 ... ek) ^= [faz eval( e1 )..eval( ek );
                           retorna o valor eval( ek )]
---------------------------------
N :  quote
S :  quote( exp1)
     (quote exp1)
     [equivalente a 'exp1]
F :  S-EXP  ->  S-EXP
     (quote e1) ^= e1
---------------------------------
N :  read
S :  read( [exp1])
     (read [exp1])
F :  [STR]  ->  S-EXP
     (read e1) ^= [expressao "S" contida em eval( e1 ); no caso de "e1" nao 
                   existir, a leitura e' feita do teclado]
---------------------------------
N :  repeat
S :  repeat( exp1 exp2*)
     (repeat exp1 exp2*)
F :  INT S-EXP*  ->  S-EXP
     (repeat e1 e2 ... ek) ^=
         [retorna o valor da ultima expressao calculada; o calculo das expres-
          soes e2..ek e' feito eval( e1 ) vezes ; e' retornado "nil" no caso de 
          eval( e1 ) ser menor ou igual a 0 ou no caso de nao existirem 
          expressoes e2..ek]
---------------------------------
N :  SAVE 
S :  SAVE( exp1)
     (SAVE exp1)
F :  STR  ->  nil 
     (SAVE e1) ^= [guarda o estado no ficheiro com nome eval( e1 ); o estado
                   podera' ser recuperado por "LOAD"]
---------------------------------
N :  sh
S :  sh( [exp1])
     (sh [exp1])
F :  [STR]  ->  INT
 (sh s) ^= [passa o controlo ao sistema operativo para execucao do comando 
              na "string" eval( s );
            no caso de nao existir argumento e' criada uma "shell" do 
            sistema sobre o "xmetoo";

            UNIX: e' retornado o codigo de erro resultado da execucao do
            comando;
            MS/DOS: e' retornado o estado na saida do "COMMAND.COM"]
---------------------------------
N :  type
S :  type( exp1)
     (type exp1)
F :  S-EXP  ->  SYM
     (type e1) ^= type( eval( e1 ))
---------------------------------
N :  trace
S :  trace()
     (trace)
F :  ->  nil
     (trace) ^= nil
              [como efeito lateral nega a "trace-flag"(5.3)]
---------------------------------
N :  UNPACK
S :  UNPACK( exp1)
     (UNPACK exp1)
F :  SYM  ->  LIST
     (UNPACK e1) ^= [lista de simbolos (constituidos por um caracter) ou 
                     inteiros (0..9) que concatenados dao o simbolo eval( e1 )] 
---------------------------------
N :  while 
S :  while( exp1 exp2*)
     (while exp1 exp2*)
F :  BOOL S-EXP*  ->  S-EXP
     (while e1 e2 ... ek) ^=
         [retorna o valor da ultima expressao calculada; o calculo das expres-
          soes e2..ek e' feito enquanto eval( e1 ) for "true"; no caso de
          eval( e1 ) = "false" `a partida e' retornado "nil";
          no caso de nao existirem expressoes e2..ek a calcular o resultado 
          sera' "nil" quando eval( e1 ) = "false"]
