// == 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 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]"))

  // pop one thing, push it as a 1-element list
#define TAIL()  AST ("T",   ("[T]"))

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

  // pop one thing, push an open-ended list headed with that thing
#define TAIL_OPEN()     AST ("T",   ("[T|_]"))

  // push an unbound variable
#define NIL_OPEN()      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    non_array_ti_expr_tail ':' ident_anns var_decl_item2
  |        non_array_ti_expr_tail ':' ident_anns '=' expr
  | ARRAY '[' INT_LITERAL DOTDOT INT_LITERAL ']' OF array_decl_tail

var_decl_item2:
    '=' expr
  | /*empty*/

array_decl_tail:
        non_array_ti_expr_tail ':' ident_anns '=' array_literal
  | VAR non_array_ti_expr_tail ':' ident_anns array_decl_tail2
  
array_decl_tail2:
    '=' array_literal
  | /*empty*/

ident_anns:
    IDENT annotations
    | UNDERSCORE_IDENT annotations

constraint_item:
    CONSTRAINT constraint_elem annotations
                                        { AST ("A, C", ("constraint(C, A)")); }

constraint_elem:
    IDENT '(' exprs ')'

solve_item:
    SOLVE annotations solve_kind

solve_kind:
    SATISFY
  | MINIMIZE expr
  | MAXIMIZE expr

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

pred_decl_args:
    pred_decl_arg "," pred_decl_args
  | pred_decl_arg

pred_decl_arg:
     non_array_ti_expr_tail ':' IDENT
   | VAR non_array_ti_expr_tail ':' IDENT
   | ARRAY '[' pred_arg_array_index ']' OF  pred_arg_array_tail ':' IDENT

pred_arg_array_index:
    INT
  | INT_LITERAL DOTDOT INT_LITERAL

pred_arg_array_tail:
    non_array_ti_expr_tail
  | VAR non_array_ti_expr_tail

//---------------------------------------------------------------------------
// 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

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

exprs:
    expr ',' exprs
  | expr

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

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

set_literal:
    '{' exprs '}'                { AST ("Es", ("lit(set(_), Es)")); }
  | '{' '}'                      { PUSH (("lit(set(_), [])")); }
  | INT_LITERAL DOTDOT INT_LITERAL { PUSH (("lit(set(%d, %d)", $1, $3)); }

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

array_access_expr: IDENT '[' INT_LITERAL ']'
  | UNDERSCORE_IDENT '[' INT_LITERAL ']'

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

annotations:
    COLONCOLON expr annotations  { CONS (); }
  | /* 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;
}