(* Conversions from general clause to Seidl clause to h1 format, headers.
   Copyright (C) 2003 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";
open "clause_h";
open "gclause_h";

type ''var atome = string * ''var term;

datatype ''var seidl_head = SHVAR of string * ''var (* P(x) *)
       | SHFUN of string * string * ''var list (* P (f (x1, ..., xk)) *)
       | SHBOT of string; (* bot, named *)

datatype ''var seidl_clause = SEIDL of
	 ''var seidl_head
	 * ''var atome list;

exception NonDistinctVarsInHeadEvt;

extern val clause_from_seidl : ''var seidl_clause -> clause * (''var -m> int) * int;
	   (* clause_from_seidl sc
	    returns a clause (see clause_h.ml) from sc, together with an environment
	    mapping each variable (of type ''var) in sc to a clause variable (an integer),
	    and the first unused variable number.
	    Raises NonDistinctVarsInHeadEvt if some variable are repeated in the head.
	    *)

datatype ''var approx_justif =
	 AJ_START of ''var seidl_clause
       | AJ_NON_HORN of ''var approx_justif_and_clause list
	 (* current clause is of the form a1 \/ a2 \/ ... \/ an <= body
	  and is justified by the clauses ai <= body. *)
       | AJ_RESOLVE of ''var seidl_clause * ''var approx_justif_and_clause list
	 (* current clause is of the form
	  P (f (t1,...,tn)) <= body
	  and we justify it by the clause
	  P (f (x1,...,xn)) <= Q1 (x1), ..., Qn (xn)
	    where Q1, ..., Qn are fresh, together with the clauses
          Q1(t1) <= body, ..., Qn(tn) <= body. *)
       | AJ_CUT of ''var approx_justif_and_clause *
	 ''var approx_justif_and_clause
	 (* current clause is of the form h <= body, and is
	  justified by h <= A, body1 and A <= body2, where
	  A is of the form P(f(x1,...,xk)), and
	  x1, ..., xk are free both in h and in body.
	  *)
       | AJ_CUT_2 of ''var approx_justif_and_clause *
	 ''var approx_justif_and_clause list
	 (* current clause is h <= Q(g(u1,...,un)), body and
	  is justified by h <= Q1(u1), ..., Qn(un), body and
	  the list of Qi(xi) <= Q(g(x1,...,xn))
	  *)
       | AJ_FACTOR of ''var * ''var * ''var approx_justif_and_clause
	 (* current clause of the form
	  P (f (x1, ..., xn)) <= body
	  where xi=xj for some i!=j.
	  Wlog, assume i=1, j=2, ie, current clause is
	  P (f (x, x, x3, ..., xn)) <= body
	  We justify it by the clause
	  P (f (x, x', x3, ..., xn)) <= body'
	  where x' is a fresh variable (given in AJ_FACTOR (x, x', ...))
	  and body' is the list of atoms obtained from the atoms
	  A of body by taking just A if x is not free in A,
	  or A and A[x:=x'] if x is free in A.
	  *)
withtype ''var approx_justif_and_clause =
     ''var approx_justif * ''var gclause;

extern val seidl_from_gclause : (unit -> ''var)
	   * (int term list * int term -> string)
	   * bool * bool
	   -> (string * string * ''var gclause)
	   -> ''var approx_justif_and_clause * (string -m> ''var gclause);
(* Converts a general clause to list of Seidl clauses (obtainable from
 the result of this function by calling the next function,
 seidl_list_from_justif);
 In general, applies various transformations so that resulting Seidl
 clauses logically imply the argument clause, and returns these
 transformations as an object of type approx_justif_and_clause.
 (Actual ''var gclause at the top of this object may differ slightly
 from second argument: predicates are made monadic.)
 First argument is a generator of fresh variables.
 Second argument is a generator of fresh predicates.
 Given (body, t), it should create a new predicate recognizing
 all t's such that body holds.  It is safe to make them completely new
 each time.
 Third argument is true to flatten bodies until their depth<=1.
 Fourth argument monadic_proxy: see seidl.ml.
 Returns pair of a justification and a clause,
 together with a map from fresh predicate symbols introduced in
 the translation to their definition as a definite clause.
 *)

extern val seidl_list_from_justif : ''var approx_justif_and_clause
	   -> ''var seidl_clause set;

exception H1NonHornEvt;
exception H1NonLinearEvt of ''_var;
exception H1ConnectedNonSiblingEvt of ''_var * ''_var;

extern val h1_exact : ''_var gclause -> unit;
	   (* Tests whether input gclause is in Nielson, Nielson,
	    and Seidl's class H1.
	    Clause must be:
	    - Horn
	    - with linear head
	    - any two free variables in the head that are connected
	      in the body must be siblings in the head.
	      Two variables are connected in the body if and only
	      if they are free in the same atom of the body,
	      or if one is free in some atom b1 of the body,
	      the other is free in some other atom b2 of the body,
	      such that b1 and b2 have free variables in common.
	      Two variables are siblings in the head if and only
	      if their (unique since the head is linear) superterm
	      is the same.
	    *)
