(* General clauses, headers.
   Copyright (C) 2003,2008,2011 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 "term_h";

datatype ''var gclause = GCLAUSE of
	 ''var term list (* the negative atoms *)
	 * ''var term list (* the positive atoms *)
	 ;

extern val gclause_vars : ''var gclause -> ''var set;

extern val list_where : ''a * ''a list * int -> int option;
	   (* find first position (starting from 3rd argument)
	    where 1st arg occurs in 2nd arg. *)

extern val is_gtautology : ''var gclause -> int option;
	   (* returns NONE is not a tautology,
	    SOME i if a tautology, and ith positive atom
	    is also a negative atom (i starts at 0). *)

type tptp_keywords = |[input_clause : string,
		       open_bracket : string,
		       close_bracket : string,
		       delim : string,
		       neg_sign : string,
		       pos_sign : string
		       ]|;
extern val tptp_keywords : string -m> tptp_keywords;

extern val print_gclause : 'a outstream * (''var -> string)
	   * tptp_keywords
	   -> ''var gclause -> unit;
extern val print_gclause_pl : 'a outstream * (''var -> string)
	   -> ''var gclause -> unit;

extern val gclause_list_sig : ''var gclause list -> (string -m> int);
(* returns map from function symbols f occurring
 in clause list to their arities.
 Raises InconsistentSig f if f occurs with two
 different arities.
 *)

extern val gclause_list_pred_sig : ''var gclause list -> (string -m> int);

extern val gclause_list_preds : (string * string * ''var gclause) list -> string set;

extern val gclause_list_has_equality : (string * ''var gclause) list -> bool;

extern val theory_of_equality : (string -m> int) * (string -m> int) * (int -> ''var) -> (string * ''var gclause) list;

(* theory_of_equality (predsig, fsig, varname)
 returns the axiom of equality over the signature predsig, fsig;
 varname maps integers to variable names.
*)

extern val magic_template : (string * string * ''var gclause) list ->
	   (string * string * ''var gclause) list;
