(* Conversions from general clause to Seidl clause to h1 format.
   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 "seidl_h";
open "monadic_h";
open "gensym_h";
open "sort_h";

fun head_from_seidl (SHVAR (P, x)) = (HVAR P, {x => 1}, 2)
  | head_from_seidl (SHFUN (P, f, varl)) =
    let val k = len varl
	val ir = ref 0
	val argl = [(inc ir; !ir)
		   | _ in list varl]
	val env = {x => arg
		  || x in list varl and arg in list argl}
    in
	if card env<>k
	    then raise NonDistinctVarsInHeadEvt
	else (HFUN (P, f, k, 1 to k,
		    f $ [V arg
			| arg in list argl]),
	      env, k+1)
    end
  | head_from_seidl (SHBOT botname) =
    (HBOT botname, {}, 1);

fun dterm_from_term (V x, env, nextx) =
    if x inset env
	then (V (?env x), env, nextx)
    else (V nextx, env ++ {x => nextx}, nextx+1)
  | dterm_from_term (f $ l, env, nextx) =
    let val (dargs, env', nextx') = dterml_from_terml (l, env, nextx)
    in
	(f $ dargs, env', nextx')
    end
and dterml_from_terml (nil, env, nextx) = (nil, env, nextx)
  | dterml_from_terml (t::l, env, nextx) =
    let val (dt, env', nextx') = dterm_from_term (t, env, nextx)
	val (ll, env'', nextx'') = dterml_from_terml (l, env', nextx')
    in
	(dt::ll, env'', nextx'')
    end;

fun atom_from_seidl ((P, t), env, nextx) =
    let val (dt1, env', nextx') = dterm_from_term (t, env, nextx)
    in
	((P, dt1), env', nextx')
    end;

fun clause_from_seidl (SEIDL (sh, body)) =
    let val (h, env, nextx) = head_from_seidl (sh)
	fun from_body (nil, al, Bs, env, nextx) =
	    (CL (h, {}, atom_sort al, Bs), env, nextx)
	  | from_body (atm::rest, al, Bs, env, nextx) =
	    (case atom_from_seidl (atm, env, nextx) of
		 ((P, V x), env', nextx') =>
		 from_body (rest, al,
			    if x inset Bs
				then Bs ++ {x => ?Bs x U {P}}
			    else Bs ++ {x => {P}},
				env', nextx')
	       | (at, env', nextx') =>
		 from_body (rest, al U {at}, Bs, env', nextx'))
    in
	from_body (body, {}, {}, env, nextx)
    end;

fun complex_head (V _) = false
  | complex_head (f $ l) = exists true | _ $ _ in list l end;

fun find_complex ((a as (_, t)) :: body, acc) =
    if complex_head t
	then SOME (a, revappend (acc, body))
    else find_complex (body, a::acc)
  | find_complex (nil, acc) = NONE;

fun uniformize_term (V x : ''var term, env : ''var -m> int term, nvars : int)
    : int term * (''var -m> int term) * int =
    if x inset env
	then (?env x, env, nvars)
    else (V nvars, env ++ {x => V nvars}, nvars+1)
  | uniformize_term (f $ l, env, nvars) =
    let val (l', env', nvars') = uniformize_term_list (l, env, nvars)
    in
	(f $ l', env', nvars')
    end
and uniformize_term_list (t::l, env, nvars) =
    let val (t', env', nvars') = uniformize_term (t, env, nvars)
	val (l', env'', nvars'') = uniformize_term_list (l, env', nvars')
    in
	(t'::l', env'', nvars'')
    end
  | uniformize_term_list (nil, env, nvars) = (nil, env, nvars);

fun term_less (V _, V _) = false
  | term_less (V _, _) = true
  | term_less (_, V _) = false
  | term_less (f $ l, f' $ l') =
    f strless f' orelse
    (f=f' andalso term_list_less (l, l'))
and term_list_less (_, nil) = false
  | term_list_less (nil, _) = true
  | term_list_less (t::l, t'::l') =
    term_less (t, t') orelse
    t=t' andalso term_list_less (l, l');

val term_sort = sort term_less;

fun uniformize_body_t (body, t, env, nvars) =
    let val (t', env', nvars') = uniformize_term (t, env, nvars)
	val body_aux = term_sort (elems body)
	val (body', env'', nvars'') = uniformize_term_list (body_aux, env', nvars')
    in
	(body', t', env'', nvars'')
    end;

fun complex_lits_in_body nil = 0
  | complex_lits_in_body ((_, _ $ _) :: l) = 1 + complex_lits_in_body l
  | complex_lits_in_body (_ :: l) = complex_lits_in_body l;

fun complex_body body = complex_lits_in_body body>=2;

fun gaifman_merge ({}, gaif) =
    ({}, nil, gaif)
  | gaifman_merge (vars : ''var set, gaif : (''var set * ''var term list) list) =
    let fun gmerge ((xs, tl) :: rest, vars', tll, gaif') =
	    if xs intersects vars
		then gmerge (rest, vars' U xs, tl::tll, gaif')
	    else gmerge (rest, vars', tll, (xs, tl)::gaif')
	  | gmerge (_, vars', tll, gaif') =
	    (vars', append tll, gaif')
    in
	gmerge (gaif, {}, nil, nil)
    end;

fun gaifman_sort (terms : ''var term list, gaif : (''var set * ''var term list) list) =
    case terms of
	t :: rest =>
	let val vars = tvars t
	    val (vars', tl', gaif') = gaifman_merge (vars, gaif)
	in
	    gaifman_sort (rest, (vars U vars', t::tl')::gaif')
	end
      | _ => gaif;

exception SeidlFromGclause;
exception SeidlNotFound;

local
    val nfa = re_make_nfa [(re_parse "^#false\\(([^()]*)\\)",
			    fn (s,a) => re_subst(s,a,1))]
in
    fun match_false P =
	nfa_run (nfa, P)
end;

fun seidl_from_gclause (genvar : unit -> ''var, newP_aux, flatten_body : bool,
			monadic_proxy : bool) =
    let fun newP (body : ''var term list, ti : ''var term) =
	    let val (body', t', ...) = uniformize_body_t (body, ti, {}, 0)
	    in
		case body' of
		    [Q $ [u]] =>
		      if u=t'
			  then Q
		      else newP_aux (body', t')
		  | _ => newP_aux (body', t')
	    end
	fun find_repeated_variable (nil, ...) = NONE
	  | find_repeated_variable (V x::l : ''var term list, first : ''var term list, h : ''var set) =
	    if x inset h
		then let val x' = genvar ()
		     in
			 SOME (x, x', revappend (first, V x'::l))
		     end
	    else find_repeated_variable (l, V x::first, h U {x})
	fun s_from_g (c as GCLAUSE (neg, [falseP $ nil])) =
	    (case match_false falseP of
		 SOME name => let val sc = SEIDL (SHBOT name, [(P, t) | P $ [t] in list neg])
			      in
				  ((AJ_START sc, c), {})
			      end
	       | _ => raise SeidlFromGclause)
	  | s_from_g (GCLAUSE (neg, [a as P $ [t]])) =
	    let val body = [(P', t') | P' $ [t'] in list neg]
		fun cvt_body body =
		    [P $ [t] | (P, t) in list body]
		fun flatten (P, V x, body) =
		    let val sc = SEIDL (SHVAR (P, x), body)
		    in
			((AJ_START sc, GCLAUSE (cvt_body body, [P $ [V x]])), {})
		    end
		  | flatten (P, t as (f $ l), body) =
		    if exists true | _ $ _ in list l end
			then let val body' = cvt_body body
				 val gaif = gaifman_sort (body', nil)
				 val bodyl = [bodyi
					     | ti in list l
					       val varsi = tvars ti
					       val (_, bodyi, _) = gaifman_merge (varsi, gaif)]
				 val Pl = [newP (body', ti)
					  || ti in list l and
					     bodyi in list bodyl]
				 val newdefs = {Q => c
					       || Q in list Pl and ti in list l
					       and bodyi in list bodyl
						   val pos = [Q $ [ti]]
						   val c = GCLAUSE (bodyi, pos)
						       such that pos<>bodyi}
				 val xl = [genvar () | _ in list l]
				 val rl = [flatten (Q, t, [(P, t) | P $ [t] in list bodyi])
					    (* does the converse of cvt_body... not very clever! *)
					  || Q in list Pl and t in list l and bodyi in list bodyl
					     such that bodyi<>[Q $[t]]]
				 val bodyrest = elems body' \ union {elems bodyi
								    | bodyi in list bodyl}
			     in
				 ((AJ_RESOLVE (SEIDL (SHFUN (P, f, xl),
						      [(Q, V x) || Q in list Pl and x in list xl]
							@ [(P, t) | P $ [t] in set bodyrest]
							(* does the converse of cvt_body...
							 not very clever! *)
							),
					       [#1 r | r in list rl]),
				   GCLAUSE (body', [P $ [t]])),
				      overwrite [#2 r | r in list rl] ++ newdefs)
			     end
		    else case find_repeated_variable (l, nil, {}) of
			     SOME (x, x', l') =>
			     let val (r, defs) =
				     flatten (P, f $ l',
					      append [if x inset tvars u
							  then [b, (Q, tsubst {x => V x'} u)]
						      else [b]
						     | b as (Q, u) in list body])
			     in
				 ((AJ_FACTOR (x, x', r),
				   GCLAUSE (cvt_body body, [P $ [t]])),
				  defs)
			     end
			   | _ =>
			     let val sc = SEIDL (SHFUN (P, f, [x | V x in list l]), body)
			     in
				 ((AJ_START sc, GCLAUSE (cvt_body body, [P $ [t]])), {})
			     end
		fun body_flatten (P, t, body) =
		    if flatten_body
			then (* h <= Q(u), body, where u=g(u1,...,un), is compiled as
			      h <= Q1(u1), ..., Qn(un), body
			      Qi(xi) <= Q(g(x1,...,xn))
			      provided u is of depth at least 2. *)
			    case find_complex (body, nil) of
				SOME ((Q, u as (g $ l)), body') =>
				let val xs = [V (genvar ()) | _ in list l] : ''var term list
				    val gx = g $ xs
				    val Qgx = Q $ [gx]
				    val Qbody = [Qgx]
				    val Ql = [newP (Qbody, xi) | xi in list xs]
				    val ir = ref 0
				    val defs = {Qi => GCLAUSE (Qbody, pos)
					       || Qi in list Ql and xi in list xs
						  val pos = [Qi $ [xi]]}
				    val (r1, defs1) = body_flatten (P, t,
								    [(Qi, ui)
								    || Qi in list Ql
								    and ui in list l] @ body')
				    val rl = [(AJ_START (SEIDL (SHVAR (Qi, xi), [(Q, gx)])),
					       ?defs Qi)
					     || Qi in list Ql and V xi in list xs]
				in
				    ((AJ_CUT_2 (r1, rl),
				      GCLAUSE (cvt_body body, [P $ [t]])),
				     defs1 ++ defs)
				end
			      | _ => flatten (P, t, body)
		    else flatten (P, t, body)
		fun shallow_flatten (P, t, body) =
		    if flatten_body
			then body_flatten (P, t, body)
		    else (* h <= Q(u), body is compiled as
			  h <= Q(x1,...,xk), body and
			  Q(x1,...,xk) <= Q(u)
			  provided u is of depth at least 2, and
			  where x1,...,xk are the free variables of u. *)
			case find_complex (body, nil) of
			    SOME ((Q, u), body') =>
			    let val (a', env, nvars) = uniformize_term (Q $ [u], {}, 0)
				val neg' = [a']
				val argl = [V x | x in set env]
				val argl' = [(?env x handle MapGet => raise SeidlNotFound)
					    | V x in list argl]
				val P' = newP_aux (neg', "*" $ argl')
				val h' as (_ $ [t']) = make_monadic (P' $ argl)
				val Qbody = [Q $ [u]]
				val def = GCLAUSE (Qbody, [h'])
				val newdef = {P' => def}
				val (r1, defs1) = shallow_flatten (P, t, (P', t') :: body')
				val r2 =
				    (AJ_START (SEIDL (case t' of
							  f' $ l =>
							  SHFUN (P', f', [x | V x in list l])
							| V x => SHVAR (P', x),
							  [(Q, u)])),
				     def)
			    in
				((AJ_CUT (r1, r2), GCLAUSE (cvt_body body, [P $ [t]])),
				     defs1 ++ newdef)
			    end
			  | _ => flatten (P, t, body)
	    in
		if complex_head t andalso
		    (*(case body of [_, _, ...] => true | _ => false)*)
		    complex_body body
		    then if monadic_proxy
			     then (* h <= body is compiled as
				   h <= Q1(x1),...,Qk(xk) and Qi(xi) <= body for each i,
				   as soon as body contains at least two literals
				   and h is of depth at least 2. *)
				 let val common_vars = tvars t & union {tvars s | s in list neg}
				     val body' = cvt_body body
				     val Ql = [newP (body', V x) | x in set common_vars]
				     val newdef = {Qi => GCLAUSE (body', [Qi $ [V x]])
						  || Qi in list Ql and x in set common_vars}
				     val (r1, defs1) = flatten (P, t, [(Qi, V x)
								      || Qi in list Ql
								      and x in set common_vars])
				     val rdefl = [body_flatten (Qi, V x, body)
						 || Qi in list Ql and x in set common_vars]
				     val rl = [r | (r, _) in list rdefl]
				     val defs2 = overwrite [defs | (_, defs) in list rdefl]
				 in
				     ((AJ_CUT_2 (r1, rl),
				       GCLAUSE (body', [P $ [t]])),
					  defs1 ++ defs2 ++ newdef)
				 end
			 else (* h <= body is compiled as
			       h <= Q(x1,...,xk) and Q(x1,...,xk) <= body
			       as soon as body contains at least two literals
			       and h is of depth at least 2. *)
			     let val common_vars = tvars t & union {tvars s | s in list neg}
				 val (neg_u, env, ...) = uniformize_term_list (neg, {}, 0)
				 val argl = [V x | x in set common_vars]
				 val argl' = [(?env x handle MapGet => raise SeidlNotFound)
					     | V x in list argl] : int term list
				 val P' = newP_aux (neg_u, "*" $ argl')
				 val h' as (_ $ [t']) = make_monadic (P' $ argl)
				 val body' = cvt_body body
				 val newdef = {P' => GCLAUSE (body', [h'])}
				 val (r1, defs1) = flatten (P, t, [(P', t')])
				 val (r2, defs2) = body_flatten (P', t', body)
			     in
				 ((AJ_CUT (r1, r2), GCLAUSE (body', [P $ [t]])),
				      defs1 ++ defs2 ++ newdef)
			     end
		else shallow_flatten (P, t, body)
	    end
	  | s_from_g (GCLAUSE (neg, [a, ...])) =
	    let val l = [s_from_g (GCLAUSE (neg, [a]))]
		val ((_, GCLAUSE (body, [a])), _) = hd l
		val pos = a :: [b
			       | ((_, GCLAUSE (_, [b])), _) in list tl l]
	    in
		((AJ_NON_HORN [#1 r | r in list l],
		  GCLAUSE (body, pos)),
		     overwrite [#2 r | r in list l])
	    end
	  | s_from_g arg = raise SeidlFromGclause
    in
	fn (name, _, c) => s_from_g (case gclause_make_monadic c of
					 GCLAUSE (neg, nil) =>
					 GCLAUSE (neg,
						  [("#false(" ^ name ^ ")")
						       $ nil])
				       | c => c
					 )
    end;

fun seidl_list_from_justif (AJ_START sc, _) = {sc}
  | seidl_list_from_justif (AJ_NON_HORN l, _) =
    union {seidl_list_from_justif j
	  | j in list l}
  | seidl_list_from_justif (AJ_RESOLVE (sc, l), _) =
    {sc} U union {seidl_list_from_justif j
		 | j in list l}
  | seidl_list_from_justif (AJ_CUT (j1, j2), _) =
    seidl_list_from_justif j1 U seidl_list_from_justif j2
  | seidl_list_from_justif (AJ_CUT_2 (j, jl), _) =
    seidl_list_from_justif j U union {seidl_list_from_justif j'
				     | j' in list jl}
  | seidl_list_from_justif (AJ_FACTOR (_, _, j), _) =
    seidl_list_from_justif j;

fun h1_exact (GCLAUSE (neg, [_, _, ...])) = raise H1NonHornEvt
  | h1_exact (GCLAUSE (neg, nil)) = ()
  | h1_exact (GCLAUSE (neg, [a])) =
    let fun siblings (V x, super) = {x => super}
	  | siblings (t as (f $ l), _) =
	    siblingsl (l, t)
	and siblingsl (nil, super) = {}
	  | siblingsl (t::l, super) =
	    let val sibt = siblings (t, super)
		val sibl = siblingsl (l, super)
	    in
		case sibl <| sibt of
		    {x => _, ...} => raise H1NonLinearEvt x
		  | _ => sibt ++ sibl
	    end
	val sibl = siblings (a, "" $ nil)
    in
	iterate
	  iterate
	    if super1=super2
		then ()
	    else raise H1ConnectedNonSiblingEvt (x1, x2)
	  | x1 => super1 in map vars1 <| sibl
	  and x2 => super2 in map vars2 <| sibl
	  end
	| b1 in list neg and b2 in list neg
	(*$V-*)
	val true = b1=b2 orelse system_less (b1, b2)
	(*$V+*)
	val vars1 = tvars b1
	val vars2 = tvars b2
	    such that vars1 intersects vars2
	end
    end;
