(* print natural deduction proof in tree format, abbreviated.
   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 "pfcprinttreeabbrv_h";
open "sort_h";
open "rel_h";

fun print_case (fd as |[put, ...]|) =
    let val prt = print fd
    in
	fn i => (prt (pack (i:int));
		 put ".")
    end;

exception AssumptionNames;

fun assumption_names (source : (string * string gclause) list,
		      definitions : string gclause set,
		      input : string gclause set,
		      justifications : deduction_tree) =
    let val assnames = ref {}
    in
	iterate
	  let fun get_assnames c =
		  if c inset definitions
		      then ()
		  else if c inset input
		      then assnames := !assnames Urel {c => {name}}
		  else (let val (_, premises) = ?justifications c
			in
			    iterate
			      get_assnames ci
			    | (ci, _) in list premises
			    end
			end handle MapGet => raise AssumptionNames)
	  in
	      get_assnames c0
	  end
	| (name, c0) in list source
	end;
	!assnames
    end;

exception PfcPrintTreeAbbrv;

fun pfc_print_tree_abbrv (f as |[put, ...]|, prompt, pdef, pass, assnames) =
    let val pt = print_term (f, identity)
	val pa = print_atom (f, identity)
	val pgc = print_gclause_pl (f, identity)
	fun pspaces 0 = ()
	  | pspaces n = (put " "; pspaces (n-1))
	(*
	fun pstars 0 = ()
	  | pstars n = (put "*"; pstars (n-1))
	 *)
	fun psigma (_, {}) = ()
	  | psigma (n, sigma) =
	    let val delimr = ref "{"
	    in
		put "\n";
		pspaces n;
		iterate
		  (put (!delimr); delimr := ",";
		   put X; put "="; pt t)
		| X => t in map sigma
		end;
		put "}"
	    end
	fun pfc_getdefs (PFC (PFC_DEF, (Xs, c), ts, pfs)) =
	    (c, {X => t
		|| X in list Xs and t in list ts
		     such that t<>V X}
	     handle ParSweep => raise PfcPrintTreeAbbrv)
	    :: append [pfc_getdefs pf
		      | pf in list pfs]
	  | pfc_getdefs _ = nil
	fun pfc_get_pfs (PFC (PFC_DEF, _, _, pfs)) =
	    append [pfc_get_pfs pf
		   | pf in list pfs]
	  | pfc_get_pfs pf = [pf]

	memofun pfc_conc (PFC (_, (Xs, GCLAUSE (_, pos)), ts, ...)) =
		let val sigma = {X => t
				|| X in list Xs and t in list ts
				     such that t<>V X}
			handle ParSweep => raise PfcPrintTreeAbbrv
		    val tsub = tsubst sigma
		    val pos' = [tsub a | a in list pos]
		in
		    pos'
		end
	fun pfc_pr (pfc as PFC (PFC_AXIOM "inj", _, _, [pfc']),
		    dewey) =
	    let val pos' = pfc_conc pfc
	    in
		put dewey; put " "; pgc (GCLAUSE (nil, pos'));
		put " by weakening.\n";
		pfc_pr (pfc', dewey ^ "1.")
	    end
	  | pfc_pr (PFC (kind, (Xs, c as GCLAUSE (_, [a])), ts, pfs),
		    dewey) =
	    let val sigma = {X => t
			    || X in list Xs and t in list ts
				 such that t<>V X}
		    handle ParSweep => raise PfcPrintTreeAbbrv
		val fact = tsubst sigma a
	    in
		put dewey; put " "; pa fact;
		if c inset assnames
		    then let val delimr = ref "  ["
			 in
			     iterate
			       (put (!delimr); delimr := ", ";
				put name)
			     | name in list sort (op strless) (?assnames c)
			     end;
			     put "]"
			 end
		else ();
		case pfs of
		    nil => (case kind of
				PFC_DEF => (put " by "; pdef c; put ".\n")
			      | PFC_INPUT => (put " by "; pass c; put ".\n")
			      | _ => raise PfcPrintTreeAbbrv)
		  | _ => (put ".\n";
			  pspaces (size dewey+2); put "using ";
			  (case kind of
			       PFC_DEF => pdef c
			     | PFC_INPUT => pass c
			     | _ => raise PfcPrintTreeAbbrv);
			  put " ";
			  pgc c; psigma (size dewey + 5, sigma);
			  iterate
			    iterate
			      (put "\n"; pspaces (size dewey+2); put "and definition ";
			       pgc def; psigma (size dewey + 5, defsigma))
			    | (def, defsigma) in list pfc_getdefs pf
			    end
			  | pf in list pfs
			  end;
			  put "\n";
			  let val ir = ref 0
			      val f as |[put, convert, tell, seek, truncate,
					  ...]|
				  = outstring dewey
			      val n = tell ()
			      val seen = ref {}
			  in
			      iterate
				iterate
				  (seen := !seen U {conc};
				   inc ir; seek n; truncate ();
				   print_case f (!ir);
				   pfc_pr (pf, convert ()))
				| pf in list pfc_get_pfs pf1
				val conc = pfc_conc pf
				    such that not (conc inset !seen)
				end
			      | pf1 in list pfs
			      end
			  end)
	    end
	  | pfc_pr arg = raise PfcPrintTreeAbbrv
    in
	fn pfcl => iterate (put prompt; pfc_pr (pfc, ""))
		   | pfc in list pfcl end
    end;
