(* Parser for .log files, C version.
   Copyright (C) 2004 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 clause_index : (int, string gclause) table = table ();
 val ci_put = t_put clause_index;
 val ci_get = t_get clause_index;
  %}

%header {
  open "proof_aux_h";
  %}

%union {
  prnone of unit
| proofinfo of proof_info
| prnamedclauselist of (string * string gclause) list
| prnamedclause of string * string gclause
| prdeductionlist of deduction_tree
| prdeduction of deduction
| prclauselist of string gclause set
| prclause of string gclause
| prpremiselist of premise list
| prpremise of premise
| prsubst of subst
| prterm of string term
| prtermlist of string term list
| prstring of string
| pri of int
}

%start problem

%type <proofinfo> problem
%type <prnamedclauselist> source named_clause_list
%type <prnamedclause> named_clause
%type <prclauselist> clause_list definitions approximation
%type <prdeductionlist> justifications deductions deduction_list
%type <prdeduction> deduction
%type <prpremiselist> premise_list
%type <prpremise> premise
%type <prclause> clause raw_clause
%type <prsubst> substitution binding_list
%type <prtermlist> clause_body non_empty_clause_body head
%type <prterm> atom term application atomhead
%type <prtermlist> term_list

%token <prstring> identifier
%token kw_open_paren kw_close_paren kw_provided kw_comma kw_semicolon
%token kw_period kw_question_mark kw_equal kw_open_brace kw_close_brace
%token kw_open_source kw_close_source kw_open_clause kw_close_clause kw_end_tag
%token kw_open_definitions kw_close_definitions
%token kw_open_approximation kw_close_approximation
%token kw_open_justifications kw_close_justifications
%token <prstring> VAR kw_ne kw_false string_constant kw_axiom kw_open_rule
%token <pri> kw_clause_def kw_clause_use
%token kw_close_rule

%%

problem : source definitions approximation justifications deductions
{ $$ |[ source = $1,
	definitions = $2,
	approximation = $3,
	justifications = $4,
	deductions = $5
	]| }
;

source : kw_open_source named_clause_list kw_close_source { $$ $2 }
;

definitions : kw_open_definitions clause_list kw_close_definitions { $$ $2 }
;

approximation : kw_open_approximation clause_list kw_close_approximation { $$ $2 }
;

justifications : kw_open_justifications deduction_list kw_close_justifications { $$ $2 }
;

deductions : deduction_list { $$ $1 }
;

named_clause_list : { $$ nil }
| named_clause_list named_clause { $$ ($2 :: $1) }
;

named_clause : kw_open_clause string_constant kw_end_tag clause kw_close_clause
  { $$ ($2, $4) }
;

deduction_list : { $$ {} }
| deduction_list deduction { let val (conc, rulename, premises) = $2
			     in
				 $$ ({conc => (rulename, premises)} ++ $1)
			     end }
;

deduction : clause kw_axiom { $$ ($1, $2, nil) }
| clause kw_open_rule premise_list kw_close_rule { $$ ($1, $2, rev $3) }
;

premise_list : premise { $$ [$1] }
| premise_list premise { $$ ($2 :: $1) }
;

premise : clause substitution { $$ ($1, $2) }
;

substitution : { $$ {} }
| kw_open_brace binding_list kw_close_brace { $$ $2 }
;

binding_list : VAR kw_equal term { $$ {$1 => $3} }
| binding_list kw_comma VAR kw_equal term
{ if $3 inset $1
      then (#put stderr "Warning, line ";
	    print_yyloc stderr @3;
	    #put stderr ": variable ";
	    #put stderr $3;
	    #put stderr " bound twice.\n";
	    #flush stderr ())
  else ();
      $$ ($1 ++ {$3 => $5}) }
;

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

clause : raw_clause { $$ $1 }
| kw_clause_def raw_clause { ci_put ($1, $2); $$ $2 }
| kw_clause_use { case ci_get $1 of
		    SOME c => $$ c
		    | _ => (#put stderr "Unknown clause ;";
			    print stderr (pack $1);
			    #put stderr ". ";
			    gyacc_error) }
;

raw_clause : kw_question_mark clause_body kw_period
{ $$ (GCLAUSE (rev $2, nil)) }
| head kw_provided clause_body kw_period
{ $$ (GCLAUSE (rev $3, rev $1)) }
| head kw_period
{ $$ (GCLAUSE (nil, rev $1)) }
;

head : atomhead { $$ [$1] }
| head kw_semicolon atomhead { $$ ($3 :: $1) }
;

atomhead : atom { $$ $1 }
| kw_false { $$ ($1 $ nil) }
;

clause_body : { $$ nil }
| non_empty_clause_body { $$ $1 }
;

non_empty_clause_body : atom { $$ [$1] }
| non_empty_clause_body kw_comma atom { $$ ($3::$1) }
;

atom : identifier kw_open_paren term_list kw_close_paren { $$ ($1 $ (rev $3)) }
| identifier term { $$ ($1 $ [$2]) }
| identifier { $$ ($1 $ nil) }
| kw_ne { $$ ($1 $ nil) }
;

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

term : VAR { $$ (V $1) }
| application { $$ $1 }
;

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