// == Prolog AST-stream term Parser for FlatZinc ==============================
// 
// (C) 2015 Salvador Abreu
//
// ----------------------------------------------------------------------------
// Based on the Parser for FlatZinc 1.1
//                      by Nick Nethercote and Julien Fischer
//
// NOTE: the parser produced by the following grammar does not ensure
// that expressions are type correct.  Further type-checking after parsing
// is required for this.
//
// This file is in the public domain, and can be used without copyright
// restrictions.

%{
#include <stdio.h>
#include <stdlib.h>

#include "types.h"

#define AST(pop, push)				\
{						\
    printf ("[%s|_T] > [", pop);		\
    printf push;				\
    printf ("|_T].\n");				\
}

#define INIT(x)					\
{						\
  printf ("_ > %s.\n", x);			\
}

#define PRE()					\
{						\
    printf ("_T > [");				\
}

#define POST()					\
{						\
    printf ("|_T].\n");				\
}

#define PUSH(x)					\
{						\
    printf ("_T > [");				\
    printf x;					\
    printf ("|_T].\n");				\
}

  // pop an item and a list, push new list (CONS)
#define CONS()  AST ("H,T", ("[H|T]"))

  // push the empty list
#define NIL()   PUSH (("[]"))

#define BINARY(op)      AST ("B,A", ("op(A,B)"))
#define UNARY(op)       AST ("X",   ("op(X)"))

%}

 
// Possible values for attributed tokens.
%union {
  UNION_DEFS ();
};

// Token kinds
%token <lit>        INT_LITERAL STRING_LITERAL FLOAT_LITERAL
       <id>         IDENT UNDERSCORE_IDENT
       ARRAY BOOL CONSTRAINT FALSE FLOAT INT MAXIMIZE MINIMIZE OF
       PREDICATE SATISFY SET SOLVE TRUE VAR DOTDOT COLONCOLON 
       
%%

//---------------------------------------------------------------------------
// Model top-level
//---------------------------------------------------------------------------

// Nb: these rules are left-recursive, which is good for Yacc as they run in
// constant stack space.  Earlier versions were right-recursive, and this
// caused stack overflows on large models.  The error recovery isn't great,
// but it's better than none.

model          :                        { INIT ("[]"); }
		 pred_decl_items        { AST ("X", ("preds(X)")); }
                 var_decl_items         { AST ("X", ("vars(X)")); }
                 constraint_items       { AST ("X", ("constrs(X)")); }
                 model_end

pred_decl_items : pred_decl_items pred_decl_item ';'   { CONS (); }
                | pred_decl_items error ';'            { yyerrok; }
		| /* empty */                          { NIL (); }

var_decl_items : var_decl_items var_decl_item ';'      { CONS (); }
               | /* empty */                           { NIL (); }
 
constraint_items: constraint_items constraint_item ';' { CONS (); }
               | /* empty */                           { NIL (); }
 
model_end      : solve_item ';'
    
    
//---------------------------------------------------------------------------
// Items
//---------------------------------------------------------------------------

pred_decl_item:
    PREDICATE IDENT '(' pred_decl_args ')'

var_decl_item:			/* -> [ var(ID,TYPE,INIT,ANNOT) | _ ] */
    VAR    non_array_ti_expr_tail ':' ident_anns var_decl_item2
    { AST ("VAL,AN,ID,T", ("var(ID, T, VAL, AN)")); }
  |        non_array_ti_expr_tail ':' ident_anns '=' expr
    { AST ("VAL,AN,ID,T", ("var(ID, T, VAL, AN)")); }
  | ARRAY '[' INT_LITERAL DOTDOT INT_LITERAL ']' OF array_decl_tail
    { AST ("VAL,AN,ID,T", ("var(ID, array(T,%d,%d), VAL, AN)", $3, $5)); }

var_decl_item2:			/* -> [ VAL | _ ] */
    '=' expr                 { }
  | /*empty*/                { NIL (); }

array_decl_tail:		/* -> [ TYPE,VAL,ANNOT,ID | _ ] */
        non_array_ti_expr_tail ':' ident_anns '=' array_literal
  | VAR non_array_ti_expr_tail ':' ident_anns array_decl_tail2
  
array_decl_tail2:		/* -> [ VAL | _ ] */
    '=' array_literal        { }
  | /*empty*/                { NIL (); }

ident_anns:			/* -> [ ANNOT,ID | _ ] */
      IDENT { PUSH (("'%s'", $1)); } annotations
    | UNDERSCORE_IDENT { PUSH (("'%s'", $1)); } annotations

constraint_item:		/* -> [ constraint(...) | ] */
    CONSTRAINT constraint_elem annotations
                             { AST ("A,C,E", ("constraint(C,E,A)")); }

constraint_elem:		/* -> [ CONSTR_ID, EXPRLIST | _ ] */
    IDENT '(' exprs ')'      { PUSH (("'%s'", $1)); }

solve_item:
    SOLVE annotations solve_kind

solve_kind:
    SATISFY                  { PUSH (("satisfy")); }
  | MINIMIZE expr            { AST ("E", ("minimize(E)")); }
  | MAXIMIZE expr            { AST ("E", ("maximize(E)")); }

//---------------------------------------------------------------------------
// Predicate parameters
//---------------------------------------------------------------------------

pred_decl_args:
    pred_decl_arg "," pred_decl_args
  | pred_decl_arg

pred_decl_arg:
     non_array_ti_expr_tail ':' IDENT
       { AST ("T", ("T:'%s'", $3)); }
   | VAR non_array_ti_expr_tail ':' IDENT
       { AST ("T", ("var(T):'%s'", $4)); }
   | ARRAY '[' pred_arg_array_index ']' OF  pred_arg_array_tail ':' IDENT
       { AST ("T,U,L", ("var(array(T,L,U)):'%s'", $8)); }

pred_arg_array_index:
    INT                             { PUSH (("_,1")); }
  | INT_LITERAL DOTDOT INT_LITERAL  { PUSH (("%d,%d", $3, $1)); }

pred_arg_array_tail:		/* -> [ TYPE | _ ] */
    non_array_ti_expr_tail          { }
  | VAR non_array_ti_expr_tail      { AST ("T", ("var(T)")); }

//---------------------------------------------------------------------------
// Type-Inst Expression Tails
//---------------------------------------------------------------------------

non_array_ti_expr_tail:
    scalar_ti_expr_tail
  | set_ti_expr_tail

scalar_ti_expr_tail:
    bool_ti_expr_tail
  | int_ti_expr_tail
  | float_ti_expr_tail

bool_ti_expr_tail:
    BOOL                                { PUSH (("bool")); }

int_ti_expr_tail:
    INT                                 { PUSH (("int")); }
  | INT_LITERAL DOTDOT INT_LITERAL      { PUSH (("int(%d,%d)", $1, $3)); }
  | '{' int_literals '}'                { AST ("Ls", ("int(Ls)")); }

int_literals:
    INT_LITERAL ',' int_literals        { AST ("Ls, L", ("[L|Ls]")); }
  | INT_LITERAL                         { PUSH (("[%d]", $1)); }

float_ti_expr_tail:
    FLOAT                               { PUSH (("float")); }
  | FLOAT_LITERAL DOTDOT FLOAT_LITERAL  { PUSH (("float(%g,%g)", $1, $3)); }

set_ti_expr_tail:
    SET OF int_ti_expr_tail             { AST ("T", ("set(T)")); }

//---------------------------------------------------------------------------
// Expressions
//---------------------------------------------------------------------------

exprs:
    expr ',' exprs               { AST ("T2:E2,T1:E1", ("(T1,T2):(E1,E2)")); }
  | expr

expr:
    bool_literal
  | INT_LITERAL                  { PUSH (("int:lit(%d)", $1.ival)); }
  | FLOAT_LITERAL                { PUSH (("float:lit(%g)", $1.rval)); }
  | STRING_LITERAL               { PUSH (("string:lit(\"%s\")", $1.sval)); }
  | set_literal
  | array_literal
  | array_access_expr
  | IDENT                        { PUSH (("_:id('%s')", $1)); }
  | UNDERSCORE_IDENT             { PUSH (("_:uid('%s')", $1)); }
  | IDENT '(' exprs ')'	/* An annotation value with > 0 arguments. */

bool_literal:
   FALSE                         { PUSH (("bool:lit(false)")); }
 | TRUE                          { PUSH (("bool:lit(true)")); }

set_literal:
    '{' exprs '}'                { AST ("Ts:Es", ("set(Ts):lit(Es)")); }
  | '{' '}'                      { PUSH (("set(_):lit([])")); }
  | INT_LITERAL DOTDOT INT_LITERAL { int i;
				     PRE();
				     printf ("set(int):lit(");
				     for (i=$1.ival; i<$3.ival; ++i)
				       printf ("%d, ", i);
				     printf ("%d)", $3.ival);
				     POST(); }

array_literal:
    '[' exprs ']'                { AST ("Es", ("array(_):alit(Es)")); }
  | '[' ']'                      { PUSH (("array(_):alit([])")); }

array_access_expr: IDENT '[' INT_LITERAL ']'
                                 { AST ("int:EI,array(T):ID",
					("T:aref(array(T):ID,int:EI)")); }
  | UNDERSCORE_IDENT '[' INT_LITERAL ']'
                                 { AST ("int:EI,array(T):ID",
					("T:aref(array(T):ID,int:EI)")); }

//---------------------------------------------------------------------------
// Annotations
//---------------------------------------------------------------------------

annotations:
    COLONCOLON expr annotations  { AST ("As, E", ("[E|As]")); }
  | /* empty */                  { NIL (); }

%%

#include "lex.yy.c"

char* filename;

int main(int argc, char *argv[])
{
    if (argc != 2) {
        fprintf(stderr, "Usage: %s <file.fzn>\n", argv[0]);
        exit(1);
    }

    filename = argv[1];
    yyin = fopen(filename, "r");
    if (yyin == NULL) {
        fprintf(stderr, "cannot open file: '%s'\n", filename);
        exit(1);
    }

    yyparse();
    return 0;
}

int yyerror(char *s)
{
    if (0 == strcmp(yytext, "")) {
        fprintf(stderr,
            "%s:%d: %s before end of file\n", filename, yylineno, s);
    } else {
        fprintf(stderr,
            "%s:%d: %s before '%s'\n", filename, yylineno, s, yytext);
    }
    return 0;
}

/*
** This is only defined so the Flex library isn't needed.
*/
int yywrap()
{
    return 1;
}