(* General clauses.
   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 "gclause_h";

fun gclause_vars (GCLAUSE (neg, pos)) =
    union {tvars t | t in list neg} U
    union {tvars t | t in list pos};

fun list_where (_, nil, _) = NONE
  | list_where (a, b::l, i) =
    if a=b
	then SOME i
    else list_where (a, l, i+1);

fun is_gtautology (GCLAUSE (neg, pos)) =
    some
      i
    | na in list neg
      val SOME i = list_where (na, pos, 0)
    end;

val tptp_keywords = {"1.0" =>
		|[input_clause = "input_clause",
		  open_bracket = "[",
		  close_bracket = "]",
		  delim = ", ",
		  neg_sign = "--",
		  pos_sign = "++"
		  ]|,
		  "3.3.0" =>
		  |[input_clause = "cnf",
		    open_bracket = "(",
		    close_bracket = ")",
		    delim = " | ",
		    neg_sign = "~",
		    pos_sign = ""
		    ]|
		    };

fun print_gclause (f as |[put, ...]|, varname,
		   |[delim,neg_sign,pos_sign, ...]|) =
    let val pa = print_atom (f, varname)
	fun pgclause (GCLAUSE (neg, pos)) =
	    let val delimr = ref ""
	    in
		iterate
		  (put (!delimr); delimr := delim; put neg_sign; pa a)
		| a in list neg
		end;
		iterate
		  (put (!delimr); delimr := delim; put pos_sign; pa a)
		| a in list pos
		end
	    end
    in
	pgclause
    end;

fun gclause_preds (GCLAUSE (neg, pos)) =
    {P | P $ _ in list neg} U {P | P $ _ in list pos};

fun gclause_list_preds cl = union {gclause_preds c
				  | (_, _, c) in list cl};

exception InconsistentSig of string;

fun sig_add (f, k, sigmap) =
    if f inset sigmap
	then if ?sigmap f = k
		 then sigmap
	     else raise InconsistentSig f
    else sigmap ++ {f => k};

fun t_sig (V _, acc) = acc
  | t_sig (f $ l, acc) =
    tl_sig (l, sig_add (f, len l, acc))
and tl_sig (nil, acc) = acc
  | tl_sig (t::l, acc) =
    tl_sig (l, t_sig (t, acc));

fun alt_sig (nil, acc) = acc
  | alt_sig ((P $ l)::rest, acc) =
    tl_sig (l, alt_sig (rest, acc))
  | alt_sig (_ :: rest, acc) =
    alt_sig (rest, acc);

fun gclause_sig (GCLAUSE (neg, pos), acc) =
    alt_sig (neg, alt_sig (pos, acc));

fun gclause_list_sig_1 (nil, acc) = acc
  | gclause_list_sig_1 (c :: l, acc) =
    gclause_list_sig_1 (l, gclause_sig (c, acc));

fun gclause_list_sig cl = gclause_list_sig_1 (cl, {});

fun al_sig (nil, acc) = acc
  | al_sig ((P $ l) :: rest, acc) =
    al_sig (rest, sig_add (P, len l, acc));

fun gclause_pred_sig (GCLAUSE (neg, pos), acc) =
    al_sig (neg, al_sig (pos, acc));

fun gclause_list_pred_sig_1 (nil, acc) = acc
  | gclause_list_pred_sig_1 (c :: l, acc) =
    gclause_list_pred_sig_1 (l, gclause_pred_sig (c, acc));

fun gclause_list_pred_sig cl = gclause_list_pred_sig_1 (cl, {});

fun print_gclause_pl (f as |[put, ...]|, varname) =
    let val pa = print_atom (f, varname)
	fun p_pos [a] = pa a
	  | p_pos nil = put "#false()"
	  | p_pos pos =
	    let val delimr = ref ""
	    in
		iterate
		  (put (!delimr); delimr := "; ";
		   pa a)
		| a in list pos
		end
	    end
	fun pgclause (GCLAUSE (neg, pos)) =
	    (p_pos pos;
	     (case neg of
		  nil => ()
		| _ => let val delimr = ref " :- "
		       in
			   iterate
			     (put (!delimr); delimr := ", ";
			      pa b)
			   | b in list neg
			   end
		       end);
		  put ".")
    in
	pgclause
    end;

fun gclause_list_has_equality cl =
    exists
      "equal" inset preds
      andalso ?preds "equal"=2
    | (_, c) in list cl
    val preds = gclause_pred_sig (c, {})
    end;

fun theory_of_equality (predsig, fsig, varname) =
    let val x = varname 1
	val y = varname 2
	val z = varname 3
	memofun varlist 0 = nil
	      | varlist (~1) = nil
	      | varlist k = V (varname k) :: varlist (k-2)
	fun xlist k = varlist (2*k-1)
	fun ylist k = varlist (2*k)
    in
	("eq_refl", GCLAUSE (nil, ["equal" $ [V x, V x]])) ::
	("eq_sym", GCLAUSE (["equal" $ [V x, V y]], ["equal" $ [V y, V x]])) ::
	("eq_trans", GCLAUSE (["equal" $ [V x, V y], "equal" $ [V y, V z]],
				["equal" $ [V x, V z]])) ::
	[("eq_pred_" ^ P,
	  GCLAUSE ((P $ xl) ::
		   ["equal" $ [xi, yi]
		   || xi in list xl and yi in list yl],
		   [P $ yl]))
	| P => k in map {"equal"} <-| predsig
	    val xl = xlist k and yl = ylist k] @
	[("eq_fun_" ^ f,
	  GCLAUSE (["equal" $ [xi, yi]
		   || xi in list xl and yi in list yl],
		     ["equal" $ [f $ xl, f $ yl]]))
	| f => k in map fsig
	    val xl = xlist k and yl = ylist k]
    end;

fun magic_template1 ((name, cat, GCLAUSE (neg, pos)), l) =
    (* Replace A1 \/ ...\/ Am \/ -B1 \/ ... \/ -Bn (1)
     by:
     A1 \/ ...\/ Am \/ -magic-A1 \/ ... \/ -magic-Am \/ -B1 \/ ... \/ -Bn (2)
     and
     B'i \/  -magic-A1 \/ ... \/ -magic-Am \/ -B1 \/ ... \/ -B{i-1} (3)
     for each i.

     If (1) holds in I, then (2) and (3) hold in I extended so that each
     magic-* is true.

     Conversely, if (2) and (3) hold in I', then let
     I(A) = I'(magic-A) => I'(A).  I claim that (1) holds in I.

     If there is any i such that I' does not satisfy magic-Bi, then pick
     i minimal.  Since I' satisfies (3), some magic-Aj must be false in I'.
     So Aj is true in I, and we are done.
     Else I' satisfies every magic-Bi.  To show that I satisfies (1),
     assume I satisfies B1, ..., Bn.  By definition of I(Bi), and since
     I' satisfies magic-Bi, I' satisfies Bi.  Since I' satisfies (2),
     I' satisfies the disjunction of each (Aj \/ -magic-Aj).  I.e., I
     satisfies the disjunction of each Aj.
     *)
    let fun magic_atom (f $ args) = ("magic-" ^ f) $ args
	val magic_A = [magic_atom a | a in list pos]
	val c = GCLAUSE (magic_A @ neg, pos)
	fun magic_B (nil, _, l) = l
	  | magic_B (b :: rest, firstb, l) =
	    magic_B (rest, b :: firstb,
		     let val nameb = let val f as |[put, convert, ...]| =
					     outstring "magic-"
				     in
					 put name;
					 put "-";
					 print f (pack (len firstb));
					 convert ()
				     end
		     in
			 (nameb, cat,
			  GCLAUSE (magic_A @ rev firstb, [magic_atom b]))
			 :: l
		    end)
    in
	(name, cat, c) :: magic_B (neg, nil, l)
    end;

fun magic_template gcl =
    let fun magic_tmpl (nil, l) = l
	  | magic_tmpl (gc :: rest, l) =
	    magic_tmpl (rest, magic_template1 (gc, l))
    in
	magic_tmpl (gcl, nil)
    end;
