Anubis / Anubis

/* grammar.y *****************************************************************

                                    Anubis
                             The language grammar. 

*****************************************************************************/ 
 
/* 
    This YACC/BISON file contains the grammar for the Anubis compiler. 

*/ 


%{

  //#line 16 "grammar.y"

#include <string.h>   
#include <stddef.h>
#include <stdio.h>
#include <stdlib.h>
#include "compil.h"
#include "polish.h"
#include "grammar_tools.h"
   
static int yyerror(char *);
extern int yylex(void);

int more = 0; 
int is_global = 0; 

   
%}

/* types of data in the parser stack --------------------------*/
%union {
  Expr   expr; 
  int integer; 
       }




/* all (non one char) tokens begin by a double underscore -----------------------------*/ 
%token<expr>     yy__if yy__is yy__then yy__type yy__operation yy__variable yy__utvar yy__float yy__alert
%token<expr>     yy__theorem yy__p_theorem yy__proof yy__read yy__exchange
%token<expr>     yy__symbol yy__Symbol yy__lpar yy__lbracket yy__dot yy__rbracket yy__comma yy__bit_width
%token<expr>     yy__semicolon yy__plus yy__minus yy__star yy__carret yy__ampersand yy__vbar 
%token<expr>     yy__equals yy__write yy__percent
%token<expr>     yy__rbrace yy__lbrace yy__rpar yy__colon yy__implies yy__forall yy__exists yy__exists_unique
%token<expr>     yy__decimal_digit yy__anb_string yy__type_String yy__type_ByteArray yy__description
%token<expr>     yy__arrow yy__ndarrow yy__with yy__type_Int32 yy__type_Float yy__type_Listener yy__indirect
%token<expr>     yy__serialize yy__unserialize yy__vcopy yy__non_equal yy__load_module
%token<expr>     yy__wait_for yy__delegate yy__tilde yy__type_Omega yy__type_Proof
%token<expr>     yy__checking_every 
%token<expr>     yy__rpar_arrow yy__rpar_ndarrow yy__dots yy__g_operation
%token<expr>     yy__less yy__greater yy__lessoreq yy__greateroreq yy__mod yy__slash yy__else
%token<expr>     yy__RAddr yy__WAddr yy__RWAddr yy__succeeds yy__succeeds_as yy__connect_to_file 
%token<expr>     yy__C_constr_for yy__connect_to_IP yy__GAddr yy__Var yy__MVar yy__StructPtr
%token<expr>     yy__debug_avm yy__terminal yy__avm
%token<expr>     yy__left_shift yy__right_shift yy__since
%token<expr>     yy__p_operation yy__p_type yy__p_variable yy__protect yy__lock yy__alt_number
%token<expr>     yy__config_file yy__verbose yy__stop_after yy__mapsto yy__rec_mapsto yy__language
%token<expr>     yy__mapstoo yy__rec_mapstoo yy__arroww   
%token<expr>     yy__djed yy__conf_int yy__conf_string yy__conf_symbol
%token<expr>     yy__we_have yy__enough yy__let yy__assume yy__indeed yy__hence
   
%token<integer>  yy__integer yy__char



/* valued non terminals ----------------------------------------------------------------*/
%type<expr>      Alternatives1 Alternatives Alternative AltOperands1 AltOperand 
%type<expr>      FArgs1 FArg OpArgs OpArgs1 OpArg Term AppTerm Terms Terms1 Terms2
%type<expr>      Conditional Clauses Clause Head ResurSym1 ResurSym2 ResurSym Type
%type<expr>      TypeVars1 Types1 TypesArgs1 Types2 List SymbolOrDecimalDigit 
%type<expr>      WithTerm SimpleBinaryOp SimpleUnaryOp
%type<expr>      AVM AVM_Instr IntMCons 
%type<expr>      Justif
   
%type<integer>   OpKW TypeKW VarKW ThKW



/* precedence and associations rules ---------------------------------------------------*/
%right yy__protect yy__lock
%right yy__debug_avm yy__terminal
%right yy__assume yy__let yy__enough yy__we_have yy__hence
%right yy__comma
%right yy__mapsto yy__rec_mapsto  
%right yy__colon
%right yy__is yy__with
%right yy__then yy__else
%right yy__semicolon
%right prec_symbol yy__symbol
%right yy__rpar
%right prec_par_term
%right prec_of_type
%right prec_sym_type
%right yy__vbar
%right yy__ampersand
%right yy__implies yy__left_shift yy__right_shift
%right yy__tilde   
%right yy__less yy__greater yy__lessoreq yy__greateroreq yy__equals yy__write yy__non_equal yy__exchange
%right yy__connect_to_file yy__connect_to_IP 
%right yy__mod
%right yy__plus
%left  yy__minus
%right yy__star
%right yy__percent   
%left  yy__slash yy__dot
%right yy__carret
%right unaryminus
%right yy__arrow yy__ndarrow yy__rpar_arrow yy__rpar_ndarrow
%right yy__lpar yy__lbrace yy__lbracket






%% /* begining of grammar */ 





/* Texts are sequences of paragraphs -------------------------------------------------*/ 
Start:            Text                                  { }
;

Text:             Paragraphs                            { if (polish) dump_polish(source_file_name); }
|                 yy__config_file ConfCommands            { }
; 

Paragraphs:       /* empty */                           { }
|                 Paragraphs Paragraph                  { }
; 



/* reading configuration commands */ 
ConfCommands:                                           { }
|                 ConfC ConfCommands                    { }
;
   
ConfC:            ConfCommand                           { }
; 
   
ConfCommand:      
    yy__verbose                              { verbose = 1; }
|   yy__language yy__conf_symbol               { if (!strcmp(string_content($2),"english")) language = 1; 
                                             else language = 0; }
|   yy__stop_after yy__conf_int yy__conf_symbol  { stop_after = integer_value($2); }
|   yy__djed yy__conf_string                   { /* djed = string_content($2); */ }
|   error                                  { fprintf(errfile,
                                                     msgtext_parse_error_config_file[language]); 
                                             yyerrok; }
;  
   


/* after each paragraph, some work is to be done ---------------------------------------*/ 
Paragraph:        Par  { 
                         end_of_par();  /* return to 'out of paragraph comment mode' */ 
                       }
;





/* sorts of paragraphs -----------------------------------------------------*/ 
Par:     TypeDefinition                        { }
|        OperationDefinition                   { }
|        OperationDeclaration                  { }
|        VariableDeclaration                   { }
|        Theorem                               { }
|        C_constr                              { }
|        yy__read yy__anb_string                   { polish_print_U8(pol_read);
                                                 polish_print_U8((U8)strlen(string_content($2)));
                                                 polish_print_str(string_content($2)); }  
|        error yy__dot                           { yyerrok; }
;  


C_constr:   yy__C_constr_for yy__Symbol yy__equals Type yy__dot    
       { make_C_constr($1,new_string(source_file_name),$2,$4);}
;

OpKW:      
    yy__operation                                   { $$ = $1; is_global = op_private; }
|   yy__p_operation                                 { $$ = $1; is_global = op_public; }
|   yy__g_operation                                 { $$ = $1; is_global = op_adm; }
; 
   
ThKW:
    yy__theorem                                     { $$ = $1; is_global = op_private; }
|   yy__p_theorem                                   { $$ = $1; is_global = op_public; }
;   
   
VarKW:     
    yy__variable                                    { $$ = $1; is_global = op_private; }
|   yy__p_variable                                  { $$ = $1; is_global = op_public; }
;    
   
TypeKW:    yy__type     { $$ = $1; is_global = op_private; }
|          yy__p_type   { $$ = $1; is_global = op_public; }
;
   
/* type (and type scheme) definitions -----------------------------------------*/ 
TypeDefinition:   TypeKW yy__Symbol yy__equals Type yy__dot
{ new_type_name($1,0,$2,$4); }
;


TypeDefinition:   TypeKW yy__Symbol yy__colon Alternatives
{ new_type_scheme($1,0, $2,  nil, $4, more, is_global == op_public ? 1 : 0); } 
; 
TypeDefinition:   TypeKW yy__Symbol yy__lpar TypeVars1 yy__rpar yy__colon Alternatives
{ new_type_scheme($1,       /* <lc> */
                  0,
		  $2,       /* <type name> */ 
		  $4,       /* <user type variables> */ 
		  $7,more, is_global == op_public ? 1 : 0); } /* <alternatives 1> and end */ 


TypeVars1:       yy__utvar                                { $$ = cons($1,nil); }
|                yy__utvar yy__comma TypeVars1              { $$ = cons($1,$3); }
; 

SymbolOrDecimalDigit:     yy__symbol                  { $$ = cons($1,nil); }
|                         yy__decimal_digit           { $$ = list1($1); }
; 






/* alternatives --------------------------------------------------------------*/
Alternatives:   yy__dot                                  { $$ = nil; }
|               yy__dots                                 { $$ = nil; more = 1; }
|               Alternatives1                          { $$ = $1; }
;   
   
Alternatives1:  
    Alternative yy__dot                                  { $$ = cons($1,nil); }
|   Alternative yy__comma yy__dots                         { $$ = cons($1,nil); more = 1; }
|   Alternative yy__comma Alternatives1                  { $$ = cons($1,$3); }
;

Alternative:  
    yy__symbol                                           { $$ = cons(cons($1,nil),nil); }
|   yy__decimal_digit                                    { $$ = cons(list1($1),nil); }
|   yy__lbracket yy__rbracket                              { $$ = cons(list1(pdstr_nil),nil); }
|   yy__symbol yy__lpar AltOperands1 yy__rpar                { $$ = cons(cons($1,nil),$3); }
|   yy__lbracket AltOperand yy__dot AltOperand yy__rbracket  { $$ = list3(list1(pdstr_cons),$2,$4); }
|   AltOperand yy__plus AltOperand                       { $$ = list3(list1(pdstr_plus),$1,$3); }
|   AltOperand yy__star AltOperand                       { $$ = list3(list1(pdstr_star),$1,$3); }
|   AltOperand yy__percent AltOperand                    { $$ = list3(list1(pdstr_percent),$1,$3); }
|   AltOperand yy__carret AltOperand                     { $$ = list3(list1(pdstr_caret),$1,$3); }
|   AltOperand yy__vbar AltOperand                       { $$ = list3(list1(pdstr_or),$1,$3); }
|   AltOperand yy__ampersand AltOperand                  { $$ = list3(list1(pdstr_and),$1,$3); }
|   AltOperand yy__arrow AltOperand                      { $$ = list3(list1(pdstr_arrow),$1,$3); }
|   AltOperand yy__equals AltOperand                     { $$ = list3(list1(pdstr_eq),$1,$3); }
|   AltOperand yy__implies AltOperand                    { $$ = list3(list1(pdstr_implies),$1,$3); }
|   AltOperand yy__left_shift AltOperand                 { $$ = list3(list1(pdstr_left_shift),$1,$3); }
|   AltOperand yy__right_shift AltOperand                { $$ = list3(list1(pdstr_right_shift),$1,$3); }
|   AltOperand yy__minus AltOperand                      { $$ = list3(list1(pdstr_minus),$1,$3); }
|   AltOperand yy__slash AltOperand                      { $$ = list3(list1(pdstr_slash),$1,$3); }
|   AltOperand yy__mod AltOperand yy__rpar                 { $$ = list3(list1(pdstr_mod),$1,$3); }
|   AltOperand yy__less AltOperand                       { $$ = list3(list1(pdstr_less),$1,$3); }
|   AltOperand yy__non_equal AltOperand                  { $$ = list3(list1(pdstr_non_equal),$1,$3); }
|   AltOperand yy__lessoreq AltOperand                   { $$ = list3(list1(pdstr_lessoreq),$1,$3); }
|   yy__tilde AltOperand                                 { $$ = list2(list1(pdstr_tilde),$2); }
|   yy__star  AltOperand                                 { $$ = list2(list1(pdstr_star),$2); }
;

AltOperands1:     
    AltOperand                                         { $$ = cons($1,nil); }
|   AltOperand yy__comma AltOperands1                    { $$ = cons($1,$3); }
; 

AltOperand:   
    Type yy__symbol                                      { $$ = cons($1,$2); }
|   Type              %prec yy__comma                    { $$ = cons($1,noname); } 
; 







/* types ---------------------------------------------------------------*/
Type:             
    yy__lpar Type yy__rpar                                 { $$ = $2; }
|   yy__Symbol    %prec prec_sym_type                    { $$ = $1; }
|   yy__utvar                                            { $$ = $1; }
|   yy__type_String                                      { $$ = type_String; }
|   yy__type_ByteArray                                   { $$ = type_ByteArray; }
|   yy__type_Int32                                       { $$ = type_Int32; }
|   yy__type_Proof yy__lpar Term yy__rpar                    { $$ = cons(type_Proof,$3); }
|   yy__type_Float                                       { $$ = type_Float; }
|   yy__type_Listener                                    { $$ = type_Listener; }
   
|   yy__RAddr yy__lpar Type yy__rpar                     { $$ = cons(type_RAddr,$3); }
|   yy__WAddr yy__lpar Type yy__rpar                     { $$ = cons(type_WAddr,$3); }
|   yy__RWAddr yy__lpar Type yy__rpar                    { $$ = cons(type_RWAddr,$3); }
   
|   yy__GAddr yy__lpar Type yy__rpar                     { $$ = cons(type_GAddr,$3); }
|   yy__Var yy__lpar Type yy__rpar                       { $$ = cons(type_Var,$3); }
|   yy__MVar yy__lpar Type yy__rpar                      { $$ = cons(type_MVar,$3); }
|   yy__Symbol yy__lpar Types1 yy__rpar                  { $$ = mcons3(app_ts,$1,$3); }
|   yy__StructPtr yy__lpar yy__Symbol yy__rpar           { $$ = cons(type_struct_ptr,
                                                                 new_integer(C_struct_id($3))); }
|   Type yy__arrow Type                                  { $$ = mcons3(functype,list1($1),$3); }
|   yy__Symbol yy__lpar Types1 yy__rpar_arrow Type  { $$ = mcons3(functype,list1(mcons3(app_ts,$1,$3)),$5); }
|   yy__lpar TypesArgs1 yy__rpar_arrow Type                { $$ = mcons3(functype,$2,$4); }
|   yy__lpar Types2 yy__rpar                               { $$ = mcons3(app_ts,tuple_type_name($2),$2); }
|   yy__lbrace Type yy__rbrace                             { $$ = cons(power_type,$2); }
//|   yy__lpar TypesArgs1 yy__rpar {}
; 

Types1:      
    Type                                               { $$ = cons($1,nil); }
|   Type yy__comma Types1                                { $$ = cons($1,$3); }
;  

TypesArgs1:      
    Type                                               { $$ = cons($1,nil); }
|   Type yy__symbol                                      { $$ = cons($1,nil); }
|   Type yy__comma TypesArgs1                            { $$ = cons($1,$3); }
|   Type yy__symbol yy__comma TypesArgs1                   { $$ = cons($1,$4); }
;  

Types2:        
    Type yy__comma Type                                  { $$ = list2($1,$3); }
|   Type yy__comma Types2                                { $$ = cons($1,$3); }
;
 






/* declaration of global variable -------------------------------------------------*/ 
VariableDeclaration: VarKW Type yy__symbol yy__equals Term yy__dot 
{ new_variable($1,       /* <lc> */ 	
               is_global, 
               $2,       /* <type> */
	       $3,       /* name */ 
               $5); }    /* <init> */
; 





/* definition of operation ------------------------------------------------------*/
OperationDefinition: OpKW Type SymbolOrDecimalDigit yy__equals Term yy__dot
{ new_op_scheme($1,       /* <lc>                  */ 
		is_global,
		$2,       /* <type>                */
		$3,       /* <operation names 1>   */ 
		nil,      /* <operation arguments> */ 
		$5); }    /* <term>                */
;

OperationDefinition: OpKW Type yy__symbol yy__lpar OpArgs yy__rpar yy__equals Term yy__dot
{ new_op_scheme($1,       /* <lc>                  */ 
		is_global,
		$2,       /* <type>                */
       cons($3,nil),      /* <operation name>      */ 
		$5,       /* <operation arguments> */ 
		$8); }    /* <term>                */
;


OperationDeclaration: OpKW Type yy__symbol yy__lpar OpArgs yy__rpar yy__dot
{ new_op_scheme($1,       /* <lc>                  */ 
		is_global,
		$2,       /* <type>                */
       cons($3,nil),      /* <operation name>      */ 
		$5,       /* <operation arguments> */ 
		no_term); }    /* <term>                */
;


OperationDeclaration: OpKW Type yy__symbol yy__dot
{ new_op_scheme($1,       /* <lc>                  */ 
		is_global,
		$2,       /* <type>                */
       cons($3,nil),      /* <operation name>      */ 
		nil,      /* <operation arguments> */ 
		no_term); }    /* <term>                */
;


SimpleBinaryOp:     yy__plus { $$ = pdstr_plus; }
|                   yy__star { $$ = pdstr_star; }
|                   yy__percent { $$ = pdstr_percent; }
|                   yy__carret { $$ = pdstr_caret; }
|                   yy__vbar { $$ = pdstr_or; }
|                   yy__ampersand { $$ = pdstr_and; }
|                   yy__arrow { $$ = pdstr_arrow; }
|                   yy__equals { $$ = pdstr_eq; }
|                   yy__implies { $$ = pdstr_implies; }
|                   yy__left_shift { $$ = pdstr_left_shift; }
|                   yy__right_shift { $$ = pdstr_right_shift; }
|                   yy__minus { $$ = pdstr_minus; }
|                   yy__slash { $$ = pdstr_slash; }
|                   yy__less { $$ = pdstr_less; }
|                   yy__non_equal { $$ = pdstr_non_equal; }
|                   yy__lessoreq { $$ = pdstr_lessoreq; }
; 

SimpleUnaryOp:      yy__minus { $$ = pdstr_minus; }
|                   yy__tilde { $$ = pdstr_tilde; }
; 

OperationDefinition: OpKW Type  OpArg SimpleBinaryOp OpArg  yy__equals Term yy__dot
{ new_op_scheme($1,       /* <lc>                  */ 
		is_global,
		$2,       /* <type>                */
		list1($4),             /* <operation name>      */ 
		list2($3,$5),          /* <operation arguments> */ 
		$7); }    /* <term>                */
;


OperationDefinition: OpKW Type SimpleUnaryOp OpArg  yy__equals Term yy__dot
{ new_op_scheme($1,       /* <lc>                  */ 
		is_global,
		$2,       /* <type>                */
		list1($3),             /* <operation name>     */ 
		list1($4),             /* <operation argument> */ 
		$6); }    /* <term>                */
;


OperationDefinition: OpKW Type  OpArg yy__mod OpArg yy__rpar yy__equals Term yy__dot
{ new_op_scheme($1,       /* <lc>                  */ 
		is_global,
		$2,       /* <type>                */
		list1(pdstr_mod),      /* <operation name>      */ 
		list2($3,$5),          /* <operation arguments> */ 
		$8); }    /* <term>                */
;


OperationDefinition: OpKW Type  OpArg SimpleBinaryOp OpArg  yy__dot
{ new_op_scheme($1,       /* <lc>                  */ 
		is_global,
		$2,       /* <type>                */
		list1($4),             /* <operation name>      */ 
		list2($3,$5),          /* <operation arguments> */ 
		no_term); }    /* <term>                */
;


OperationDefinition: OpKW Type SimpleUnaryOp OpArg  yy__dot
{ new_op_scheme($1,       /* <lc>                  */ 
		is_global,
		$2,       /* <type>                */
		list1($3),             /* <operation name>     */ 
		list1($4),             /* <operation argument> */ 
		no_term); }    /* <term>                */
;


OperationDefinition: OpKW Type  OpArg yy__mod OpArg yy__rpar yy__dot
{ new_op_scheme($1,       /* <lc>                  */ 
		is_global,
		$2,       /* <type>                */
		list1(pdstr_mod),      /* <operation name>      */ 
		list2($3,$5),          /* <operation arguments> */ 
		no_term); }    /* <term>                */
;







/* arguments of operations ----------------------------------------------------*/
OpArgs:   /* empty */                      { $$ = nil; }
|           OpArgs1                        { $$ = $1; }
; 

OpArgs1:    OpArg                          { $$ = cons($1,nil); }
|           OpArg yy__comma OpArgs1              { $$ = cons($1,$3); }
; 

OpArg:      Type yy__symbol                  { $$ = cons($1,$2); }
; 



/* arguments of (non top level) functions */ 
/*
FArgs:                                     { $$ = nil; }
|          FArgs1                          { $$ = $1; }
;
*/
   
FArgs1:    FArg                            { $$ = cons($1,nil); }
|          FArg yy__comma FArgs1             { $$ = cons($1,$3); }
;
   
FArg:      Type yy__symbol                   { $$ = cons($1,$2); }
//|          yy__symbol  %prec prec_symbol     { $$ = cons(fresh_unknown(),$1); }
;    


/* terms ---------------------------------------------------------------------------*/
Term: yy__alert                         { $$ = mcons3(alert,$1,new_string(source_file_name)); }
|     yy__alt_number yy__lpar Term yy__rpar               { $$ = mcons3(alt_number,$1,$3); }
|     yy__protect Term                                { $$ = mcons3(protect,$1,$2); }
|     yy__lock Term yy__comma Term                      { $$ = mcons4(lock,$1,$2,$4); }
|     yy__debug_avm Term                              { $$ = mcons3(debug_avm,$1,$2); }
|     yy__avm yy__lbrace AVM yy__rbrace                   { $$ = mcons3(avm,$1,$3); }
|     yy__terminal Term                               { $$ = mcons3(terminal,$1,$2); }
|     yy__symbol                %prec prec_symbol     { $$ = mcons3(symbol,linecol(),$1); }
//|     yy__Symbol                %prec prec_symbol     { $$ = mcons3(symbol,linecol(),$1); }
|     yy__lpar yy__rpar           %prec prec_symbol     { $$ = mcons3(symbol,linecol(),pdstr_voidpars); }
|     yy__integer               %prec prec_symbol     { $$ = mcons3(integer,linecol(),$1); }
|     yy__char                  %prec prec_symbol     { $$ = mcons3(integer,linecol(),$1); }
|     yy__float                 %prec prec_symbol     { $$ = mcons3(fpnum,linecol(),
                                                                  mantissa_and_exponent(linecol(),$1)); }
|     yy__lpar Term yy__rpar            %prec prec_par_term   { $$ = $2; }
|     yy__lpar Terms2 yy__rpar          %prec prec_par_term   
               { tuple_type_name($2); $$ = mcons4(app,$1,mcons3(symbol,$1,pdstr_sharp_tuple),$2); }
|     yy__lpar Type yy__rpar Term           %prec prec_of_type  { $$ = mcons4(of_type,$1,$2,$4); }
|     yy__lpar yy__colon Term yy__rpar Term %prec prec_of_type  { $$ = mcons4(of_type,$1,$3,$5); }
|     yy__lpar yy__colon Type yy__rpar Term %prec prec_of_type  { $$ = mcons4(of_type,$1,$3,$5); }
|     AppTerm                                       { $$ = $1; }
|     Conditional                                   { $$ = $1; }
//|     Term                                     { $$ = $1; }
|     yy__lbracket List                               { $$ = $2; }
|     yy__star Term                                   { $$ = mcons3(anb_read,$1,$2); }
//|     yy__star Type                                   { $$ = mcons3(type_rep,$1,$2); }
|     Term yy__write Term                             { $$ = mcons4(anb_write,$2,$1,$3); }
|     Term yy__exchange Term                          { $$ = mcons4(anb_exchange,$2,$1,$3); }
|     Term yy__semicolon Term                    
      /* 'a; t' translates to 'if (One)a is unique then t' */ 
             { $$ = mcons4(cond,
                           $2,
                           mcons4(of_type,$2,pdstr_One,$1),
                           list1(mcons3(list1(pdstr_unique),$2,$3))); }
|     yy__load_module yy__lpar Term yy__rpar              { $$ = mcons3(load_module,$1,$3); }
|     yy__serialize yy__lpar Term yy__rpar                { $$ = mcons3(serialize,$1,$3); }
|     yy__unserialize yy__lpar Term yy__rpar              { $$ = mcons3(unserialize,$1,$3); }
|     yy__bit_width yy__lpar Type yy__rpar                { $$ = mcons3(bit_width,$1,$3); }
|     yy__indirect yy__lpar Type yy__rpar                 { $$ = mcons3(indirect_type,$1,$3); }
|     yy__vcopy yy__lpar Term yy__comma Term yy__rpar       { $$ = mcons4(vcopy,$1,$3,$5); }
|     yy__lpar Type yy__rpar yy__connect_to_file Term           { $$ = mcons4(connect_to_file,$4,$2,$5); }
|     yy__lpar Type yy__rpar yy__connect_to_IP Term yy__colon Term    { $$ = mcons5(connect_to_IP,$4,$2,$5,$7); }
|     yy__anb_string                             { $$ = mcons3(string,linecol(),$1); }  
|     yy__with yy__symbol yy__equals Term yy__comma WithTerm         { $$ = mcons5(with,$3,$2,$4,$6); }
|     yy__checking_every Term yy__milliseconds yy__comma yy__wait_for Term yy__then Term  
                                                        { $$ = mcons5(wait_for,$1,$6,$2,$8); }
|     yy__delegate Term yy__comma Term                      { $$ = mcons4(delegate,$1,$2,$4); }
|     yy__lbrace yy__symbol yy__colon Type yy__comma Term yy__rbrace { $$ = mcons5(set,$1,$2,$4,$6); }
|     yy__lpar FArgs1 yy__rpar yy__mapsto Term                   { $$ = mcons4(lambda,$4,$2,$5); }
|     yy__lpar FArgs1 yy__rpar yy__rec_mapsto Term               { $$ = mcons5(rec_lambda,$3,$4,$2,$5); }
|     yy__forall yy__symbol yy__colon Type yy__comma Term { $$ = mcons5(forall,$1,$2,$4,$6); } 
|     yy__forall yy__symbol yy__colon Term yy__comma Term { $$ = mcons5(forall,$1,$2,$4,$6); } 
|     yy__exists yy__symbol yy__colon Type yy__comma Term { $$ = mcons5(exists,$1,$2,$4,$6); } 
|     yy__exists_unique yy__symbol yy__colon Type yy__comma Term { $$ = mcons5(exists_unique,$1,$2,$4,$6); } 
|     yy__description yy__symbol yy__colon Type yy__comma Term { $$ = mcons5(description,$1,$2,$4,$6); } 
; 

Terms2:         Term yy__comma Term               { $$ = list2($1,$3); }
|               Term yy__comma Terms2             { $$ = cons($1,$3); }
; 



/* 'with' terms ------------------------------------------------------------------*/ 
WithTerm:       Term   %prec yy__comma                    { $$ = $1; }
|               yy__symbol yy__equals Term yy__comma WithTerm      { $$ = mcons5(with,$2,$1,$3,$5); }
; 

   
   
/* lists -----------------------------------------------------------------------------*/
List:      yy__rbracket                       { $$ = mcons3(symbol,$1,pdstr_nil); }
|          Term yy__rbracket                  { $$ = mcons4(app,$2,mcons3(symbol,$2,pdstr_cons),
                                                list2($1,mcons3(symbol,0,pdstr_nil))); }
|          Term yy__comma List                 
               { $$ = mcons4(app,$2,mcons3(symbol,$2,pdstr_cons),list2($1,$3)); }
/*
{ Expr u = fresh_unknown(); 
 $$ = mcons4(of_type,$2,u,mcons4(app,$2,mcons3(symbol,$2,pdstr_cons),
        list2($1,mcons4(of_type,$2,u,$3)))); }
   */
|          Term yy__dot Term yy__rbracket
               { $$ = mcons4(app,$2,mcons3(symbol,$2,pdstr_cons),list2($1,$3)); }
;




/* applicative terms ------------------------------------------------------------------*/
AppTerm:    Term yy__lpar Terms yy__rpar        { $$ = mcons4(app, $2,  $1,      $3); }
                                                   /* (app  <lc> <term> . <terms>) */
|           Term yy__lbracket List { $$ = list4(app,$2,$1,$3); }
;

AppTerm:  Term yy__plus        Term { $$ = mcons4(app,$2,mcons3(symbol,$2,pdstr_plus),list2($1,$3)); }
|         Term yy__star        Term { $$ = mcons4(app,$2,mcons3(symbol,$2,pdstr_star),list2($1,$3)); }
|         Term yy__percent     Term { $$ = mcons4(app,$2,mcons3(symbol,$2,pdstr_percent),list2($1,$3)); }
|         Term yy__carret      Term { $$ = mcons4(app,$2,mcons3(symbol,$2,pdstr_caret),list2($1,$3)); }
|         Term yy__vbar        Term { $$ = mcons4(app,$2,mcons3(symbol,$2,pdstr_or),list2($1,$3)); }
|         Term yy__ampersand   Term { $$ = mcons4(app,$2,mcons3(symbol,$2,pdstr_and),list2($1,$3)); }
|         Term yy__arrow       Term { $$ = mcons4(app,$2,mcons3(symbol,$2,pdstr_arrow),list2($1,$3)); }
|         Term yy__equals      Term { $$ = list5(app,$2,mcons3(symbol,$2,pdstr_eq),$1,$3); }
|         Term yy__implies     Term { $$ = mcons4(app,$2,mcons3(symbol,$2,pdstr_implies),list2($1,$3)); }
|         Term yy__left_shift  Term { $$ = mcons4(app,$2,mcons3(symbol,$2,pdstr_left_shift),list2($1,$3)); }
|         Term yy__right_shift Term { $$ = mcons4(app,$2,mcons3(symbol,$2,pdstr_right_shift),list2($1,$3)); }
|         Term yy__minus       Term { $$ = mcons4(app,$2,mcons3(symbol,$2,pdstr_minus),list2($1,$3)); }
|         Term yy__slash       Term { $$ = mcons4(app,$2,mcons3(symbol,$2,pdstr_slash),list2($1,$3)); }
|         Term yy__less        Term { $$ = mcons4(app,$2,mcons3(symbol,$2,pdstr_less),list2($1,$3)); }
|         Term yy__non_equal   Term { $$ = mcons4(app,$2,mcons3(symbol,$2,pdstr_non_equal),list2($1,$3)); }
|         Term yy__greater     Term { $$ = mcons4(app,$2,mcons3(symbol,$2,pdstr_less),list2($3,$1)); }
|         Term yy__lessoreq    Term { $$ = mcons4(app,$2,mcons3(symbol,$2,pdstr_lessoreq),list2($1,$3)); }
|         Term yy__greateroreq Term { $$ = mcons4(app,$2,mcons3(symbol,$2,pdstr_lessoreq),list2($3,$1)); }
|         Term yy__mod Term yy__rpar { $$ = mcons4(app,$2,mcons3(symbol,$2,pdstr_mod),list2($1,$3)); }
|         yy__minus Term %prec unaryminus { $$ = mcons4(app,$1,mcons3(symbol,$1,pdstr_minus),list1($2)); }
|         yy__tilde Term  { $$ = mcons4(app,$1,mcons3(symbol,$1,pdstr_tilde),list1($2)); }
; 

Terms:      /* empty */                    { $$ = nil; }
|           Terms1                         { $$ = $1; }
; 

Terms1:     Term                           { $$ = cons($1,nil); }
|           Term yy__comma Terms1                { $$ = cons($1,$3); }
; 




/* conditional terms -------------------------------------------------------------------*/
Conditional:   yy__if Term yy__is yy__lbrace Clauses yy__rbrace 
{ $$ = mcons4(cond, $1,  $2,      $5); }
          /* (cond  <lc> <term> . <clauses>) */ 
; 

Conditional:   yy__if Term yy__succeeds_as yy__symbol yy__then Term
{ $$ = mcons4(cond, $1, $2, list2(mcons3(list1(pdstr_failure),0,mcons3(symbol,$3,pdstr_failure)),
                                  mcons3(list2(pdstr_success,$4),0,$6))); }
;

Conditional:   yy__if Term yy__succeeds yy__then Term
{ $$ = mcons4(cond, $1, $2, list2(mcons3(list1(pdstr_failure),0,mcons3(symbol,$4,pdstr_failure)),
                                  mcons3(list2(pdstr_success,pdstr__),0,$5))); }
;

Conditional:   yy__if Term yy__is Clause 
{ $$ = mcons4(cond, $1, $2, list1($4)); }
; 

Conditional:   yy__since Term yy__is Head yy__comma Term 
{ $$ = mcons4(cond, $1, $2, list1(mcons3($4,$5,$6))); }
; 

Conditional:   yy__if Term yy__then Term yy__else Term
{ $$ = mcons4(cond,
              $1,
	      mcons4(of_type,$1,pdstr_Bool,$2),
	      list2(mcons3(list1(pdstr_false),$5,$6),
                    mcons3(list1(pdstr_true),$3,$4))); }

Conditional:   yy__if Term yy__is Clause yy__else Term  
{ $$ = mcons5(select_cond,$1,$2,$4,$6); }    
 



/* clauses in conditionals ------------------------------------------------*/
/*   
Clauses1:      Clause                       { $$ = cons($1,nil); }
|              Clause yy__comma Clauses1      { $$ = cons($1,$3);  }
|              Clause Clauses1              { $$ = cons($1,$2);  }
;
*/ 
   
Clauses:       /* empty */                  { $$ = nil; }
|              Clause Clauses               { $$ = cons($1,$2); }
|              Clause yy__comma Clauses       { $$ = cons($1,$3); }
;
   
Clause:       Head yy__then Term             
         { $$ = mcons3($1,           $2,    $3); }
; 

Head:         yy__symbol                             { $$ = cons($1,nil); }
|             yy__decimal_digit                      { $$ = cons($1,nil); }
|             yy__lbracket yy__rbracket                { $$ = cons(pdstr_nil,nil); }
|             yy__symbol yy__lpar yy__rpar               { $$ = cons($1,nil); }
|             yy__symbol yy__lpar ResurSym1 yy__rpar     { $$ = cons($1,$3); }
|             yy__lbracket ResurSym yy__dot ResurSym yy__rbracket { $$ = list3(pdstr_cons,$2,$4); }
|              ResurSym yy__plus ResurSym            { $$ = list3(pdstr_plus,$1,$3); }
|              ResurSym yy__star ResurSym            { $$ = list3(pdstr_star,$1,$3); }
|              ResurSym yy__percent ResurSym         { $$ = list3(pdstr_percent,$1,$3); }
|              ResurSym yy__carret ResurSym          { $$ = list3(pdstr_caret,$1,$3); }
|              ResurSym yy__vbar ResurSym            { $$ = list3(pdstr_or,$1,$3); }
|              ResurSym yy__ampersand ResurSym       { $$ = list3(pdstr_and,$1,$3); }
|              ResurSym yy__arrow ResurSym           { $$ = list3(pdstr_arrow,$1,$3); }
|              ResurSym yy__equals ResurSym          { $$ = list3(pdstr_eq,$1,$3); }
|              ResurSym yy__implies ResurSym         { $$ = list3(pdstr_implies,$1,$3); }
|              ResurSym yy__left_shift ResurSym      { $$ = list3(pdstr_left_shift,$1,$3); }
|              ResurSym yy__right_shift ResurSym     { $$ = list3(pdstr_right_shift,$1,$3); }
|              ResurSym yy__minus ResurSym           { $$ = list3(pdstr_minus,$1,$3); }
|              ResurSym yy__slash ResurSym           { $$ = list3(pdstr_slash,$1,$3); }
|              ResurSym yy__mod ResurSym yy__rpar      { $$ = list3(pdstr_mod,$1,$3); }
|              ResurSym yy__less ResurSym            { $$ = list3(pdstr_less,$1,$3); }
|              ResurSym yy__non_equal ResurSym       { $$ = list3(pdstr_non_equal,$1,$3); }
|              ResurSym yy__lessoreq ResurSym        { $$ = list3(pdstr_lessoreq,$1,$3); }
|              yy__tilde ResurSym                    { $$ = list2(pdstr_tilde,$2); }
|              yy__lpar ResurSym2 yy__rpar             { $$ = cons(pdstr_sharp_tuple,$2); }
;

ResurSym:      yy__symbol                     { $$ = $1; }
|              Type yy__symbol                { $$ = cons($1,$2); }
;

ResurSym1:     ResurSym                     { $$ = cons($1,nil); }
|              ResurSym yy__comma ResurSym1       { $$ = cons($1,$3); }
; 

ResurSym2:     ResurSym yy__comma ResurSym      { $$ = list2($1,$3); }
|              ResurSym yy__comma ResurSym2     { $$ = cons($1,$3); }
;

   
/* virtual machine instructions ---------------------------------------------------------*/    
AVM:                 { $$ = nil; }
|      AVM_Instr AVM { $$ = cons($1,$2); }
; 

AVM_Instr:     yy__symbol { $$ = string_to_tag($1); }
|              yy__lpar yy__symbol IntMCons { $$ = cons(string_to_tag($2),$3); } 
;

IntMCons:      yy__rpar                   { $$ = nil; }
|              yy__dot yy__integer yy__rpar   { $$ = new_integer($2); }
|              yy__integer IntMCons       { $$ = cons(new_integer($1),$2); }
|              yy__anb_string IntMCons    { $$ = cons($1,$2); }
;

   
/* pseudo keywords */ 
   
yy__milliseconds:    yy__symbol 
   { if ($1 != pdstr_millisecond && $1 != pdstr_milliseconds) yyerror(""); }
; 
   
/* Syntax for theorems:
   
Theorem <name>:
   <statement>.
Proof:   
   <proof>.
   
 */
Theorem:       ThKW yy__symbol yy__colon Term yy__dot yy__proof yy__colon Term yy__dot 
{ new_op_scheme($1,      /* <lc> */ 
                is_global,
                cons(proof_type,$4),   /* type of operation */
                cons($2,nil),          /* name of operation */ 
                nil,
                $8); }
;
   


Term:     yy__we_have Term yy__dot Justif Term %prec yy__we_have  { $$ = mcons5(we_have,$1,$2,$4,$5); }
|              yy__enough Term yy__dot Justif Term  %prec yy__enough  { $$ = mcons5(enough,$1,$2,$4,$5); }
|              yy__assume Term yy__dot Term    %prec yy__assume   { $$ = mcons4(assume,$1,$2,$4); }
|              yy__let yy__symbol yy__colon Term yy__dot Term %prec yy__let  { $$ = mcons5(let,$1,$2,$4,$6); }
|              Hence Term                  %prec yy__hence  { $$ = $2; }
;    
  
Hence:         yy__hence              { }
|              yy__hence yy__comma      { }
;    
   
Justif:                    { $$ = mcons3(symbol,linecol(),pdstr_nil); }
|              yy__indeed Term yy__dot  { $$ = $1; }
;    

   
%% /* end of grammar */ 


/* sending syntax error messages -------------------------------------------------------*/ 
static int yyerror (char *s)
{
  err_line_col(linecol()); 
  fprintf(errfile,
	  msgtext_parse_error[language]);
  return 0; 
}