\documentclass{article}
\usepackage[T1]{fontenc}

\author{Camila Team}

\title{Camila --- Gramática}

\newcommand{\ENDMODEL}{\hbox{\textsc{EndModel}}}
\newcommand{\SIMB}{\hbox{\textsc{Simb}}}
\newcommand{\MODEL}{\hbox{\textsc{Model}}}

\newcommand{\htt}[1]{\hbox{\texttt{`#1'}}}

\begin{document}

\maketitle

$$especificacao \longrightarrow \left\{ 
  \matrix{
    especificacao\ elemento\star    \hfill\cr
    especificacao\ typesMod         \hfill\cr
    especificacao\ \ENDMODEL         \hfill\cr
    especificacao\ \MODEL\ \SIMB       \hfill\cr
    \epsilon\hfill
         } \right.$$

$$defTipo \longrightarrow \left\{
   \matrix{
     ID-SIMB\ \htt{=}\ defTp\ inv?\ \htt{;}   \hfill\cr
     ID-SIMB\ \htt{::}\ defTp\ inv?\ \htt{;}  \hfill\cr
     error\ \htt{;}                        \hfill
   }
   \right.$$


% inv : 'inv' '(' SIMB ')' '='  expressao
$$inv \longrightarrow \htt{inv}\ \htt{(}\ \SIMB\ \htt{)}\ \htt{=}\ expressao $$

%% defTp: simpleType    
%%      | alternativa2  
%%      | alternativa
%%      | tuplo         
%%      ;

$$defTp \longrightarrow \left\{
   \matrix{
     simpleType\hfill\cr
     alternativa2\hfill\cr
     alternativa\hfill\cr
     tuplo\hfill\cr
     \epsilon\hfill
     }
   \right.$$

\begin{verbatim}

simpleType: SIMB               
          | NIL                
          | simpleType '<->' simpleType   // Relacao
          | simpleType  '->' simpleType   // Funcao finita
          | lista              
          | conjunto           
          | INTEGER     // Segmento Inicial
          | '(' simpleType ')' 
          ;

tuplo: simpleType INTER rtuplo2  
     | itemtuplo rtuplo          
     ;

rtuplo2: simpleType                
       | rtuplo2 INTER simpleType  
       ;

rtuplo: itemtuplo rtuplo       
      |                        
      ;

itemtuplo: SIMB ':' simpleType %prec minima 

lista: SIMB LIST                   
     | '(' simpleType ')' LIST     
     | segmentoInicial LIST        
     ;

conjunto: SIMB SET                
        | '(' simpleType ')' SET  
        | segmentoInicial SET     
        ;

alternativa :      '[' simpleType ']'   
  | simpleType '|' simpleType           
  | alternativa '|' '[' simpleType ']'  					
  | alternativa '|' simpleType          
  ;

alternativa2: simpleType PLUS simpleType   
            | alternativa2 PLUS simpleType 
            ;

typesMod: TYPE defTipo restDefTypesMod ENDTYPE

restDefTypesMod: defTipo restDefTypesMod
               |
               ;

elemento: expressao ';'  
        | include        
        | ESTADO SIMB ':' defTp ';' 
        | directiva
        | deffuncao ';'            
        | error ';'  elemento
        | QUIT      
        ;

directiva : DEBUGON   
  | DEBUGOFF          
  ;


include : INCLUDE SIMB '.' SIMB 
  | INCLUDE STRING 
  | INCLUDE SIMB 
  | INCLUDEM STRING 
  | INCLUDEM SIMB '.' SIMB 
  | INCLUDEM SIMB 


deffuncao : SIMB '(' explist ')' '=' expressao  
  | FUNCAO SIMB assinatura precond # mensagem
  poscondicao 

poscondicao : ESTADO expressao RETUR expressao  
  | RETUR expressao ESTADO expressao
  | RETUR expressao
  | ESTADO expressao
  | LET '(' deflist ')' IN poscondicao

assinatura : '(' explist2 ')' resultado  
  ;

resultado : ':' resultado1 
  |               
  ;

resultado1 : resultado1 defTp
  |                
  ;

explist2  : SIMB ':' defTp ',' explist2   
  | SIMB ':' defTp
  | SIMB ',' explist2            
  | SIMB        
  | '(' SIMB ')'  ',' explist2    
  | '(' SIMB ')'                 
  |                             
  ;

precond  : PRE expressao 
  | PRE expressao SETA expressao 
  |        
  ;

defobj   : SIMB  '<-' expressao    
  | SIMB '.' SIMB  '<-' expressao  
  ;

expressao: SIMB                    
   | '(' expressao ')'             
   | CONSTANTE                 
   | expressao '(' explist ')' 
   | FUNCAO assinatura precond #/* mensagem */ 
     poscondicao 
   | LAMBDA '(' explist ')' '.' expressao    
   | SIMB '(' explist ')'    
   | QUOTE '(' explist ')'   
   | op_orio ORIO '(' expressao ',' expressao ')'     
   | NIL                      
   | defobj                   
   | strexpressao             
   | intexpressao             
   | ffexpressao              
   | relexpressao             
   | seqexpressao             
   | setexpressao             
   | letexpressao             
   | ifexpressao              
   | boolexpressao            
   | expressao '\\ ' expressao 
   | expressao '/' expressao   
   | expressao '[' expressao ']'
   | SIMB '.' SIMB            
   | FunctExp
   ;

strexp: STRING            
      | expressao STRCAT expressao
      ;

op_orio: SIMB
       | UNION
       | ADD  
       | STRCAT
       | MUL   
       | OR    
       | '^'   
       | PLUS  
       ;

intexp: INTEGER      
      | '#' expressao 
      | expressao ADD expressao
      | expressao SUB expressao
      | expressao DIV expressao
      | expressao MUL expressao
      ;

boolexp: expressao IN expressao       
       | expressao NOTIN expressao    
       | expressao EQ expressao       
       | expressao AND expressao      
       | expressao '=>' expressao    // Implica
       | expressao OR expressao       
       | NOT expressao               
       | expressao '<' expressao     
       | expressao '>' expressao     
       | expressao '<=' expressao     
       | expressao '>=' expressao     
       | expressao '!=' expressao     
       | IS defTp '(' expressao ')'  
       | ALL '(' all ')'       
       | EXIST '(' exist ')'   
       | EXIST1 '(' exist1 ')' 
       | BOOL                  
       ;

FunctExpressao : expressao SET 
  | expressao LIST 
  | expressao FSETA 
  | FSETA2 expressao 
  | expressao COMP expressao 
  | ID expressao  
  | CONSF expressao 
  | expFAlist  
  | expFPlist  
  ;

expFAlist: expressao FADD expressao         
         | expFAlist FADD expressao  
         ;

expFPlist: expressao FPROD expressao 
         | expFPlist FPROD expressao 
         ;

all: SIMB '<-' expressao ',' all 
   | SIMB '<-' expressao ':' expressao 
   ;

exist: SIMB '<-' expressao ',' exist 
     | SIMB '<-' expressao ':'  expressao 
     ;

exist1: SIMB '<-' expressao ',' exist1 
      | SIMB '<-' expressao ':'  expressao 
      ;

setexpressao : '{' compreensao '}'  
       | '{' extensao '}' 
       | '{' '}'          
       | expressao INTER expressao 
       | expressao UNION expressao 
       | expressao '-' expressao   
       ;

compreensao:   expressao '|' fromlist 
compreensao2:  expressao '|' fromlist2 

extensao: extensao ',' expressao       
        | expressao                    
        ;

seqexp2: compreensao2          
  | extensao ',' expressao '>' 
  | expressao '>'              
  | '>'                   
  | expressao ':' expressao '>' 
  ;

seqexp: '<'    seqexp2 
  | expressao '^' expressao
  ;

fromlist : from ',' fromlist
  | from                    
  ;

fromlist2: from ',' fromlist2 
  | from2                     
  ;

from     : SIMB '<-' expressao
  | SIMB '<-' expressao ':' expressao 
  ;

from2     : SIMB '<-' expressao '>'   
  | SIMB '<-' expressao ':' expressao '>' 
  ;

ffexp: '[' ffcompreensao ']'    
     | '[' exppairlist ']'      
     | expressao PLUS expressao  
     ;

ffcompreensao:  expressao SETA expressao '|' fromlist  

exppairlist: exppairlist ',' exppair     
           | exppair                     
           |                             
           ;

exppair: expressao SETA expressao   

relexp: RELBEGIN ffcompreensao RELEND  
      | RELBEGIN exppairlist RELEND    
      ;

explist: expressao ',' explist             
       | expressao                         
       |                      
       ;

letexp: LET '(' deflist ')' IN expressao 

deflist: def ',' deflist        
       | def                    
       | comdef ',' deflist     
       | comdef                 
       ;

comdef   : '<' SIMB ',' SIMB '>' '=' expressao 
  ;

def: SIMB '=' expressao 
   | '=' expressao      
   ;

ifexp: IF  expressao THEN expressao
     | IF '(' expcaselist
     | IF  expressao THEN expressao ELSE expressao
     ;

expcaselist: casepair ',' expcaselist
           | casepair ')'            
           | ELSE SETA expressao ')' 
           | casepair ')' OTHER expressao
           ;

casepair: expressao SETA expressao
        | is_expressao
        ;

is_exp: expressao IS '<' SIMB ':' SIMB '>' SETA expressao
  | expressao IS '<' '>' SETA expressao  
  | expressao IS '{' SIMB ':' SIMB '}'  SETA expressao 
  | expressao IS '{' '}' SETA expressao 
  | expressao IS '[' SIMB SETA SIMB ':' SIMB ']' SETA expressao 
  | expressao IS '[' ']' SETA expressao
  | expressao IS tag ':' SIMB SETA expressao
  ;


tag: INTEGER
   | SIMB
   ;
\end{verbatim}
\end{document}