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

// -- AST stack macros: -------------------------------------------------------
// AST  (POP, (PUSH))
// ASTT (POP, (PUSH), TRANS)
// INIT (STACK)
// PUSH (ITEM)
// CONS ()
// NIL  ()

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

#define ASTT(pop, push, trans)			\
{						\
    printf ("[%s|_T] > [", pop);		\
    printf push;				\
    printf ("|_T] :- ");			\
    printf trans;				\
    printf (".\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]"))

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

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

%}

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

%right ','

%%

//---------------------------------------------------------------------------
// 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
                 { AST ("S,C,V,P", ("fzn(P, V, C, S)")); }

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", ("constraint(C,A)")); }

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

solve_item:			/* -> [ solve(S,A) | _ ] */
    SOLVE annotations solve_kind { AST ("S,A", ("solve(S, A)")); }

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:		/* -> [ UB, LB | _ ] */
    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", ("[%d|Ls]", $1)); }
  | 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               { RCONS (); }
  | expr			 { AST ("E", ("[E]")); }

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

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

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

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

array_access_expr:
    IDENT '[' INT_LITERAL ']'    { PUSH (("aref('%s',lit(%d,int),_)",$1,$3)); }
  | UNDERSCORE_IDENT '[' INT_LITERAL ']'
                                 { PUSH (("aref('%s',lit(%d,int),_)",$1,$3)); }

//---------------------------------------------------------------------------
// 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 == 1) {
    yyin = stdin;
  }
  else if (argc == 2) {
    filename = argv[1];
    yyin = fopen(filename, "r");
    if (yyin == NULL) {
      fprintf(stderr, "cannot open file: '%s'\n", filename);
      exit(1);
    }
  }
  else {
    fprintf(stderr, "Usage: %s [FILE.fzn]\n", argv[0]);
    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;
}