(* h1 clauses and definitions for the h1 resolution prover.
   Copyright (C) 2003, 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 "auto_h";
open "term_h";

(* Horn clauses: we code them as definite clauses,
 using a fake atom \bot, which is less than any other.
 We represent \bot by so-called bottoms.
 *)

(* Clauses
 P(t) [or q] <= P1(t1), ..., Pn(tn), q1, ..., qm
 with t either a variable or a flat term f(x1, ..., xk) [all variables distinct]
 with selection:
 - selects q1 if m>=1;
 - otherwise, consider one among P(t), P1(t1), ..., Pn(tn) of maximal depth;
 select one which is negative if any, otherwise select nothing.

 Clauses in which nothing is selected must then be of the form:
 P(f(x1, ..., xk)) <= B1(x1), ..., Bk(xk)
 where the Bis are blocks,
 or just q.
 These are just alternating automata transitions (or unit clauses q).
 *)

datatype head = HVAR of string (* P (x1) *)
       | HFUN of string * string * int * int set * int term
       (* P, f, k, [1...k], f(x1,...,xk) *)
       | HQ of block (* q = \cname{P1, ..., Pn} *)
       | HBOT of string (* \bot; each bottom comes with a name *)
	 ;

type atom = string * int term;

    (* Clauses in which something is selected (i.e., outside the 'automaton' part. *)
datatype clause = CL of head
	 * block set (* set of q's in body, ordered in a suitable way. *)
	 * atom list
	 (* rest of body, ordered in a suitable way.
	  In this list, we only find terms of depth >= 1.
	  Terms of depth 0 are grouped in the next structure:
	  *)
	 * (int -m> block)
	 (* maps each variable x to the block B={P1, ..., Pk} such that P_1(x), ..., P_k(x)
	  are in body (k>=1). *)
	 ;

datatype automaton_clause = AC_UNIV of string (* P(x) *)
  | AC_Q of block (* q *)
  | AC_POP of string * string * block list
    (* P, f, [B1, ..., Bk] *)
  | AC_POP_RAW of clause (* automaton clause, but unprocessed,
			  i.e., could have been converted to
			  AC_POP format. *)

datatype resolve_mgu = 
    MGU_AUTO_X1_IS of int term (* {x1 => t}, where x1 is variable 1 from
			      the automaton clause and t is a term from
			      the other clause. *)
  | MGU_AUTO_Xs_ARE of int term list (* {x1 => t1, ..., xk => tk},
				      where x1, ..., xk are the variables
				      free in the head of the automaton clause
				      and t1, ..., tk are terms from the
				      other clause. *);

type automaton_pop_trans = string -m> string -m> (block list set)
    * int * int set;
    (* maps P, f, to (blkls, k, {1, ..., k}, f(x1,...,xk))
     where blkls is the set of possible bodies, each mapped to
     a proof of the corresponding pop clause;
     each body is a list of blocks,
     one for each variable argument (1, ..., k) to f. *)
type automaton_univ_trans = string set;
    (* set of universal clauses P(x), together with proofs. *)

extern val atom_sort : atom set -> atom list;

exception BotFoundEvt of clause;
extern val default_do_bot : clause -> unit;
	   (* the default behavior when deriving a bot clause. *)
extern val resolver : (clause -> unit) * int * int * automaton option
	   * bool * bool * bool * bool
	   * |[put : string -> unit, flush : unit -> unit, ... : 'a]| option
	   * |[put : string -> unit, flush : unit -> unit, ... : 'b]| option ->
	   |[ new_clause : clause -> unit,
	      resolve : unit -> unit,
	      get_automaton : unit -> automaton_pop_trans * automaton_univ_trans,
	      get_clauses : unit -> clause list,
	      get_true_botnames : unit -> string set
	      ]|;

extern val is_tautology : clause -> bool;

extern val clause_vars : clause -> int set;
extern val clause_from_automaton_clause : automaton_clause -> clause;

extern val clean_automaton : automaton_pop_trans * automaton_univ_trans
	   -> automaton;
(* Recall from auto_h.ml that an automaton is a cleaned up version
 of an automaton_pop_trans and an automaton_univ_trans;
 proofs are removed, there are no ref's left.
 *)

extern val print_clause : 'a outstream * string -> clause -> unit;

extern val clause_list_preds : clause list -> string set;
(* returns set of ordinary, unary predicate symbols
 occurring in clause list.
 *)
extern val clause_list_bots : clause list -> string set;
(* returns set of botnames occurring in clause list.
 *)
