/* Parser for untyped lambda terms */
/* generates parser.ml and parser.mli */
/* $Id: parser.mly,v 1.25 2000/06/27 19:28:55 alamstei Exp $ */

%{

open Lambda

let well_formed injlist =
  match injlist with
    (i,j,x,m)::tl -> 
      List.for_all (fun (a,b,c,d) -> (b=j)) injlist
  | [] -> true

%}

/* terminal sybols (tokens) */
%token <string> IDENT
%token <int> INT
%token <bool> BOOL
%token <int*int> PROJ INJ
%token LPAR RPAR DOT CASEOR ARROW
%token ABS LET REC EQUALS IN CASE OF COMMA SLASH
%token EOF     /* this is needed, but why? */

/* precedences: IDENT and LPAR bind stronger than DOT */
/* This means in the situation "\x.x IDENT" or "\x.x (", the parser
    will shift, and not reduce. */

%nonassoc DOT IN ARROW            /* all rules that end in a term */
%nonassoc IDENT LPAR ABS LET CASE PROJ INT BOOL INJ CASEOR 
                                  /* all tokens that could start a term */

/* the entry point */
%start term
%type <Lambda.lambdaterm> term

%%

term:
  | nonappterm				{ $1 }
  | term nonappterm			{ App($1,$2) }
  | PROJ nonappterm                     { let (i,j)=$1 in Proj(i,j,$2) } 
  | INJ nonappterm                      { let (i,j)=$1 in Inj(i,j,$2) }

multiident:
  | IDENT multiident                    { Uservar($1)::($2) }
  | IDENT                               { [Uservar($1)] }

tuplelist:
  | term COMMA tuplelist                { $1::$3 }
  | term COMMA term                     { [$1; $3] }

casedist:
  | INJ IDENT ARROW term CASEOR casedist { let (i,j)=$1 in 
                                             (i,j,Uservar($2),$4)::($6) }
  | INJ IDENT ARROW term                 { let (i,j)=$1 in 
                                             [(i,j,Uservar($2),$4)] }

nonappterm:
  | LPAR term RPAR                      { $2 }
  | IDENT				{ Var(Uservar($1)) }
  | ABS multiident DOT term             { multiabs $2 $4 }
  | BOOL                                { Boollit($1) }
  | INT                                 { Intlit($1) }
  | LET IDENT EQUALS term IN term       { Let(Uservar($2), $4, $6) }
  | LET IDENT multiident EQUALS term IN term  
                                        { Let(Uservar($2),
					     (multiabs $3 $5), $7) } 
  | LET REC IDENT EQUALS term IN term   { Letrec(Uservar($3), $5, $7) }
  | LET REC IDENT multiident EQUALS term IN term  
                                        { Letrec(Uservar($3),
					     (multiabs $4 $6), $8) } 
  | LPAR tuplelist RPAR                 { Tuple($2) }
  | LPAR RPAR                           { Tuple([]) }
  | CASE term OF casedist               { if (well_formed $4) then
                                            Case($2,$4)
 	                                  else 
                                            raise (Exn.Illegal_casedist ($4)) }