(* Parser for clause lists in TPTP format.
 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 "yyerror_h";

  val tptp_version_tally = ref {} : (string -m> int ref) ref;

  fun tptp_default_version {} = "3.3.0"
    | tptp_default_version tally =
      let fun tptp_def_ver {ver => ref n} = (ver, n)
	    | tptp_def_ver tally =
	      let val (t1, t2) = split tally
		  val (ver1,n1) = tptp_def_ver t1
		  val (ver2,n2) = tptp_def_ver t2
	      in
		  if n1>n2
		      then (ver1,n1)
		  else (ver2,n2)
	      end
      in
	  #1 (tptp_def_ver tally)
      end;

  fun gclause_of_lit (true, a) = GCLAUSE (nil, [a])
    | gclause_of_lit (false, a) = GCLAUSE ([a], nil);

  fun g_add_lit ((true, a), GCLAUSE (neg, pos)) = GCLAUSE (neg, a::pos)
    | g_add_lit ((false, a), GCLAUSE (neg, pos)) = GCLAUSE (a::neg, pos)

  fun version_tally ver =
    let val cntr = if ver inset !tptp_version_tally
		       then ?(!tptp_version_tally) ver
		   else let val cr = ref 0
			in
			    tptp_version_tally :=
			    !tptp_version_tally ++ {ver => cr};
			    cr
			end
    in
	inc cntr
    end;

  %}

%header {
open "gclause_h";
%}

%union {
  yynone of unit
| clauselist of (string * string * string gclause) list
| namedclause of string * string * string gclause
| clause of string gclause
| lit of bool * string term
| term of string term
| termlist of string term list
| string of string
}

%start problem

%type <clauselist> problem clause_list
%type <namedclause> clause
%type <clause> clause_body clause_lits new_clause_body new_clause_lits
%type <lit> clause_lit new_clause_lit
%type <term> atom atomic_term term
%type <termlist> term_list

%token <string> identifier
%token kw_input_clause kw_cnf kw_open_paren kw_close_paren kw_comma kw_pipe kw_period
%token kw_open_bracket kw_close_bracket
%token kw_equal
%token kw_plus kw_minus kw_tilde
%token <string> VAR
%%

problem : clause_list { $$ (rev ($1)) }
;

clause_list : { $$ nil }
| clause_list clause { $$ ($2 :: $1) }
;

clause : kw_input_clause kw_open_paren identifier kw_comma identifier kw_comma
            clause_body kw_close_paren period
{ version_tally "1.0"; $$ ($3, $5, $7) }
|	kw_cnf kw_open_paren identifier kw_comma identifier kw_comma
	new_clause_body kw_close_paren period
{ version_tally "3.3.0"; $$ ($3, $5, $7) }
;

period : kw_period
|
;

clause_body : kw_open_bracket clause_lits kw_close_bracket { $$ ($2) };

new_clause_body : kw_open_paren new_clause_lits kw_close_paren { $$ ($2) };

clause_lits : clause_lit { $$ (gclause_of_lit $1) }
| clause_lits kw_comma clause_lit { $$ (g_add_lit ($3, $1)) }
;

new_clause_lits : new_clause_lit { $$ (gclause_of_lit $1) }
| new_clause_lits kw_pipe new_clause_lit { $$ (g_add_lit ($3, $1)) }
;

clause_lit : kw_plus atom { $$ (true, $2) }
| kw_minus atom { $$ (false, $2) }
;

new_clause_lit : atom { $$ (true, $1) }
| kw_tilde atom { $$ (false, $2) }
;

atom : atomic_term { case $1 of
			 V x => (#put stderr "Line "; print_yyloc stderr @1;
				 #put stderr ": variable ";
				 #put stderr x;
				 #put stderr " cannot be used as formula. ";
				 gyacc_error)
		       | _ => $$ $1 }
| atomic_term kw_equal atomic_term { $$ ("equal" $ [$1,$3]) }
;

atomic_term : identifier kw_open_paren term_list kw_close_paren { $$ ($1 $ (rev $3)) }
| identifier kw_open_paren kw_close_paren { $$ ($1 $ nil) }
| identifier { $$ ($1 $ nil) }
| identifier atomic_term { $$ ($1 $ [$2]) }
| VAR { $$ (V $1) }
;

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

term : atomic_term { $$ $1 }
| kw_open_paren term kw_close_paren { $$ $2 }
;

%%

val tptp_init = (tptp_version_tally := {});
