(* Parser for complete deterministic automata in XML form.
 Copyright (C) 2003, 2008 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan.

   This file is part of h1.

   h1 is free software; you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2, or (at your option)
   any later version.

   h1 is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with h1; see the file COPYING.  If not, write to
   the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
*)

%{
  open "rel_h";
  open "yyerror_h";


  local
    val nfa = re_make_nfa [(re_parse "^[0-9]+$", fn (s,a) => intofstring s)]
  in
    fun match_dec s =
	nfa_run (nfa, s)
  end;

  exception ArityErrorEvt of string * int * int;
  exception ArgErrorEvt of string * string list * string * string;
  exception UndefinedFunEvt of string;
  exception UndefinedArgEvt of string * string list;
  exception XaEvalEvt of string;
  exception NoDomainSizeEvt;

  val xa_domsizer = ref (NONE : int option);
  val xa_statesr = ref ({} : states);
  val xa_tablesr = ref ({} : tables);

  fun qname s =
      if ord s=ord "!"
	  then "_q" ^ substr (s, 1, size s)
      else s;

  fun xa_vars (XV x) = {x}
    | xa_vars (XF (_, l)) = union {xa_vars t | t in list l}
    | xa_vars _ = {};

  type env = string -m> string; (* variable to value *)

  fun xa_eval (rho : env) =
      let fun xaeval (XV x) =
	      if x inset rho
		  then ?rho x
	      else raise XaEvalEvt x
	    | xaeval (XF (f, l)) =
	      if f inset !xa_tablesr
		  then let val (k, table) = ?(!xa_tablesr) f
			   val k'=len l
		       in
			   if k<>k'
			       then raise ArityErrorEvt (f,k',k)
			   else let val vl = [xaeval t | t in list l]
				in
				    if vl inset table
					then ?table vl
				    else raise UndefinedArgEvt (f, vl)
				end
		       end
	      else raise UndefinedFunEvt f
	    | xaeval (XVAL v) = v
      in
	  xaeval
      end;

  fun iter_values (f : env -> unit) =
      let val domain =
	      delay (case !xa_domsizer of
			 SOME n =>
			 let val f as |[put, convert, tell, seek, truncate, ...]|
				 = outstring "!"
			     val ir = ref 0
			     val start = tell ()
			 in
			     {(inc ir;
			       seek start;
			       truncate ();
			       print f (pack (!ir));
			       qname (convert ()))
			     |while !ir < n}
			 end
		       | NONE => raise NoDomainSizeEvt)
	  fun iterv ({}, rho) = f rho
	    | iterv ({X} U rest, rho) =
	      iterate
		iterv (rest, rho ++ {X => v})
	      | v in set force domain
	      end
      in
	  fn Xs => iterv (Xs, {})
      end;

  fun xa_print_args f =
      let val put = #put f
      in
	  fn args =>
	     if null args
		 then ()
	     else let val delimr = ref "("
		  in
		      iterate
			(put (!delimr);
			 delimr := ",";
			 put v)
		      | v in list args
		      end;
		      put ")"
		  end
      end;

  exception InsertNewEntry of xa_term * xa_term;

  fun xa_handler NoDomainSizeEvt =
      #put stderr ": cannot iterate over values of variables: \
       \no domain size given. "
    | xa_handler (ArityErrorEvt (f,k,k1)) =
      (#put stderr ": bad number of arguments, expecting ";
       print stderr (pack (k:int));
       #put stderr ", got ";
       print stderr (pack (k1:int));
       #put stderr ". ")
    | xa_handler (ArgErrorEvt (f, args, res, oldres)) =
      (#put stderr ": entry ";
       #put stderr f;
       xa_print_args stderr args;
       #put stderr " redefined as ";
       #put stderr res;
       #put stderr ", already defined as ";
       #put stderr oldres;
       #put stderr ". ")
    | xa_handler (UndefinedFunEvt f) =
      (#put stderr ": no entry has been defined for function ";
       #put stderr f;
       #put stderr " yet. ")
    | xa_handler (UndefinedArgEvt (f, args)) =
      (#put stderr ": entry ";
       #put stderr f;
       xa_print_args stderr args;
       #put stderr " is undefined. ")
    | xa_handler (XaEvalEvt x) =
      (#put stderr ": variable ";
       #put stderr x;
       #put stderr " is undefined (should not happen). ")
    | xa_handler exc = raise exc;

  fun insert_new_entry (loc, pat as XF (f, ts), t) =
      let val lvars = xa_vars pat
      val arity = len ts
      val rvars = xa_vars t
  in
      case rvars \ lvars of
	  {x, ...} => (#put stderr "Variable ";
		       #put stderr x;
		       #put stderr " occurs on the right, but not on the left of an equality. ";
		       true (* error *)
		       )
	| _ => ((iter_values (fn rho =>
				 let val xev = xa_eval rho
				     val rhs = xev t
				     val vl = [xev t | t in list ts]
				     val (k, ftable) =
					 if f inset !xa_tablesr
					     then ?(!xa_tablesr) f
					 else (arity, {})
				 in
				     if k<>arity
					 then raise ArityErrorEvt (f,k,arity)
				     else if vl inset ftable
					 then raise ArgErrorEvt (f,vl,rhs,
								 ?ftable vl)
				     else xa_tablesr := !xa_tablesr
					 ++ {f => (k, ftable ++ {vl => rhs})}
				 end
				 ) lvars;
		 false)
		 handle exc => (#put stderr "Line "; print_yyloc stderr loc;
				xa_handler exc; true)
		    )
      end
    | insert_new_entry (loc, pat, t) = raise InsertNewEntry (pat, t);

  %}

%header {
open "xmlauto_h";

datatype xa_term = XV of string (* variable *)
       | XVAL of string (* value, !1...!n *)
       | XF of string * xa_term list;
%}

%union {
  xanone of unit
| xamodel of xmodel
| xastring of string
| xadeflist of definitions
| xadef of string * definition
| xastates of states
| xastate of string * string set
| xapredset of string set
| xapred of string
| xatables of tables
| xatable of string * int * (string list -m> string)
| xatableattr of |[name:string, arity:int]|
| xaentries of string list -m> string
| xaentry of string list * string
| xastringlist of string list
| xaterm of xa_term
| xatermlist of xa_term list
| xaint of int
}

%start problem

%type <xamodel> problem
%type <xadeflist> definitions definition_list
%type <xadef> definition definition_attributes definition_attribute
%type <xastates> states state_list
%type <xastate> state
%type <xapredset> satisfies_clauses
%type <xapred> satisfies_clause
%type <xatables> tables table_list
%type <xatable> table
%type <xatableattr> table_attributes
%type <xaentries> entries
%type <xaentry> entry
%type <xastring> result arg
%type <xastringlist> args
%type <xatermlist> term_list
%type <xaterm> term non_trivial_term bang_state
%type <xanone> optional_domain_size def_list def

%token <xastring> string_constant
%token kw_open_definitions kw_close_definitions
%token kw_open_definition kw_close_definition
%token kw_open_states kw_close_states
%token kw_open_state kw_close_state
%token kw_end_tag
%token kw_short_end_tag
%token kw_open_satisfies kw_close_satisfies
%token kw_open_tables kw_close_tables
%token kw_open_table kw_close_table
%token kw_open_entry kw_close_entry
%token kw_open_result kw_close_result
%token kw_open_arg kw_close_arg
%token kw_open_paren kw_close_paren kw_comma kw_iff kw_true kw_false
%token kw_model
%token <xastring> statename identifier VAR
%token kw_name kw_arity kw_arg kw_cond kw_equal kw_result kw_xml
%token kw_domain_size
%token <xaint> intg

%%

problem : kw_xml definitions states tables { $$ ($2, $3, $4) }
| kw_model optional_domain_size def_list
  { $$ ({}, !xa_statesr, !xa_tablesr) }
  ;

definitions : kw_open_definitions kw_short_end_tag { $$ {} }
| kw_open_definitions kw_end_tag definition_list kw_close_definitions kw_end_tag
{ $$ $3 }
;

definition_list : { $$ {} }
| definition_list definition { if #1 $2 inset $1
				   then (#put stderr "Line ";
					 print_yyloc stderr @2;
					 #put stderr ": duplicate definition for state ";
					 #put stderr (#1 $2);
					 #put stderr ". ";
					 gyacc_error)
			       else $$ ($1 ++ {#1 $2 => #2 $2}) }
;

definition : kw_open_definition definition_attributes end_definition { $$ $2 }
;

definition_attributes : { $$ ("", |[arg = "", cond = ""]|) }
| definition_attributes definition_attribute
{ let val (name1, |[arg=arg1, cond=cond1]|) = $1
      val (name2, |[arg=arg2, cond=cond2]|) = $2
  in
    $$ (name1 ^ name2, |[arg = arg1 ^ arg2, cond = cond1 ^ cond2]|)
  end }
;

definition_attribute : kw_name kw_equal string_constant { $$ ($3, |[arg = "", cond = ""]|) }
| kw_arg kw_equal string_constant { $$ ("", |[arg = $3, cond = ""]|) }
| kw_cond kw_equal string_constant { $$ ("", |[arg = "", cond = $3]|) }
;

end_definition : kw_short_end_tag
| kw_end_tag kw_close_definition kw_end_tag
;

states : kw_open_states kw_short_end_tag { $$ {} }
| kw_open_states kw_end_tag state_list kw_close_states kw_end_tag { $$ $3 }

state_list : { $$ {} }
| state_list state { if #1 $2 inset $1
			 then (#put stderr "Line ";
			       print_yyloc stderr @2;
			       #put stderr ": duplicate state ";
			       #put stderr (#1 $2);
			       #put stderr ". ";
			       gyacc_error)
		     else $$ ($1 ++ {#1 $2 => #2 $2}) }
;

state : kw_open_state kw_name kw_equal string_constant kw_short_end_tag { $$ ($4, {}) }
| kw_open_state kw_name kw_equal string_constant kw_end_tag satisfies_clauses
  kw_close_state kw_end_tag
{ $$ ($4, $6) }
;

satisfies_clauses : { $$ {} }
| satisfies_clauses satisfies_clause { $$ ($1 U {$2}) }
;

satisfies_clause : kw_open_satisfies kw_name kw_equal string_constant end_satisfies { $$ $4 }
;

end_satisfies : kw_short_end_tag
| kw_end_tag kw_close_satisfies kw_end_tag
;

tables : kw_open_tables kw_end_tag table_list kw_close_tables kw_end_tag { $$ $3 }
| kw_open_tables kw_short_end_tag { $$ {} }
;

table_list : { $$ {} }
| table_list table { let val (name, arity, fmap) = $2
		     in
			 if name inset $1
			     then (#put stderr "Line ";
				   print_yyloc stderr @2;
				   #put stderr ": duplicate table for state ";
				   #put stderr name;
				   #put stderr ". ";
				   gyacc_error)
			 else case some ql
				   | ql => q in map fmap
				     such that len ql<>arity
				   end of
				   SOME ql => (#put stderr "Line ";
					       print_yyloc stderr @2;
					       #put stderr ": bad number of argument states, expecting ";
					       print stderr (pack (arity : int));
					       #put stderr ", got ";
					       print stderr (pack (len ql));
					       #put stderr ". ";
					       gyacc_error)
				| _ => $$ ($1 ++ {name => (arity, fmap)})
		     end }
;

table : kw_open_table table_attributes kw_short_end_tag { $$ (#name $2, #arity $2, {}) }
| kw_open_table table_attributes kw_end_tag entries
  kw_close_table kw_end_tag { $$ (#name $2, #arity $2, $4) }
;

table_attributes : { $$ |[name = "", arity = 0]| }
| table_attributes kw_name kw_equal string_constant { $$ ($1 ++|[name = $4]|) }
| table_attributes kw_arity kw_equal string_constant { case match_dec $4 of
							   SOME n => $$ ($1 ++|[arity = n]|)
							 | _ => gyacc_error }
;

entries : { $$ {} }
| entries entry { if #1 $2 inset $1
		      then (#put stderr "Line ";
			    print_yyloc stderr @2;
			    #put stderr ": duplicate entry. ";
			    gyacc_error)
		  else $$ ($1 ++ {#1 $2 => #2 $2}) }
;

entry : kw_open_entry result kw_short_end_tag { $$ (nil, $2) }
| kw_open_entry result kw_end_tag args kw_close_entry kw_end_tag { $$ (rev $4, $2) }
;

result : kw_result kw_equal string_constant { $$ $3 }
;

args : { $$ nil }
| args arg { $$ ($2 :: $1) }
;

arg : kw_open_arg kw_name kw_equal string_constant end_arg { $$ $4 }
;

end_arg : kw_short_end_tag
| kw_end_tag kw_close_arg kw_end_tag
;

optional_domain_size : kw_domain_size intg { xa_domsizer := SOME $2;
					    xa_statesr := {};
					    xa_tablesr := {};
					    $$ () }
|  { xa_domsizer := NONE;
    xa_statesr := {};
    xa_tablesr := {};
    $$ () }
;

def_list : def_list def { $$ () }
| { $$ () }
;

def : non_trivial_term kw_equal term
{
 if insert_new_entry (@1, $1, $3)
     then gyacc_error
 else $$ ()
}
| non_trivial_term kw_iff kw_true
{
 case $1 of
     XF (P, [t]) => (* already monadic *)
     ((iter_values (fn rho =>
		       let val v = xa_eval rho t
		       in
			   xa_statesr := !xa_statesr Urel {v => {P}}
		       end
		       ) (xa_vars $1);
       $$ ())
	  handle exc => (#put stderr "Line "; print_yyloc stderr @1;
			 xa_handler exc; gyacc_error))
   | XF (P, l) => (* make this monadic, as in monadic.ml;
	       predicate is P, new state recognizing
	       #P (l) is !P. *)
     let val pat = XF ("#" ^ P, l)
	 val qP = qname ("!" ^ P)
     in
	 if insert_new_entry (@1, pat, XVAL qP)
	     then gyacc_error
	 else (xa_statesr := !xa_statesr Urel {qP => {P}};
	       $$ ())
     end
}
| non_trivial_term kw_iff kw_false { $$ () }
;

bang_state : statename { $$ (XVAL (qname $1)) };

term : bang_state { $$ $1 }
| VAR { $$ (XV $1) }
| non_trivial_term { $$ $1 }
;

non_trivial_term : identifier { $$ (XF ($1, nil)) }
| identifier kw_open_paren kw_close_paren { $$ (XF ($1, nil)) }
| identifier kw_open_paren term_list kw_close_paren { $$ (XF ($1, rev $3)) }
;

(* term_list is reversed *)
term_list : term { $$ [$1] }
| term_list kw_comma term { $$ ($3 :: $1) }
;
