(* Coq printing functions for model-checking justifications.
   Copyright (C) 2003, 2008 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 "coq_fun_h";
open "coq_term_h";
open "coq_model_h";
open "coq_kw_h";
open "gensym_h";
open "sort_h";

(*
fun coq_print_and_type (f as |[put, ...]|, and_prefix, n : int) =
    let fun pind () =
	    (put and_prefix; print f (pack n))
	val delimr = ref "["
	val ir = ref 0
    in
	put "\nInductive "; pind ();
	if n<>0
	    then (iterate
		    (put (!delimr);
		     delimr := ",";
		     put "H";
		     inc ir; print f (pack (!ir)))
		  |while !ir<n
		  end;
		    put ":Prop]")
	else ();
	    put " : Prop :=\n    "; put and_prefix; put "_intro : ";
	    ir := 0;
	    iterate
	      (put "H"; print f (pack (!ir)); put " -> ")
	    |while !ir<n
	    end;
	    if n<>0
		then (delimr := "("; ir := 0;
		      iterate
			(put (!delimr); delimr := " H";
			 print f (pack (!ir)))
		      |while !ir<n
		      end;
		      put ")")
	    else pind ();
		put ".\n"
    end;
*)

fun coq_print_or_type (ver, f as |[put, ...]|, or_prefix) =
    let val |[param_prolog, param_epilog, var_delim, ...]| =
	coq_keywords ver
	val pfvars = coq_print_f_vars (f, "")
	val pvars = coq_print_vars f
	memofun portype (n : int) =
		let val or_n = let val g as |[convert, ...]| =
				       outstring or_prefix
			       in
				   print g (pack n);
				   convert ()
			       end
		    val delimr = ref "    "
		    val ir = ref 0
		in
		    put "\nInductive "; put or_n;
		    (if n=0 then () else (put param_prolog;
					  pvars (var_delim, "H", n);
					  put ":Prop";
					  put param_epilog));
			 put " : Prop :=\n";
			 iterate
			   (put (!delimr); delimr := "  | ";
			    put or_n; put "_intro_"; inc ir; print f (pack (!ir));
			    put " : H"; print f (pack (!ir));
			    put " -> "; pfvars (or_n, "H", n); put "\n"
			    )
			 |while !ir<n
			 end;
			 put ".\n";
			 or_n
		end
    in
	portype
    end;

fun coq_print_inversion_P_f (ver, fd as |[put, ...]|,
			     portype (* typically coq_print_or_type (ver, fd, or_prefix) *),
			     fun_prefix, state_prefix,
			     rem_name, xname, term_type,
			     AUTO (auto, univ), CAN (autonamer, _)) =
    let val |[intros_tac, inversion_tac, apply_tac, trivial_tac, tauto_tac,
	      dot_tac, semi_tac, ...]|
	    = coq_keywords ver
	val pblocks = coq_print_blocks (ver, fd, state_prefix)
	val pPfvars = coq_print_P_f_vars (ver, fd, fun_prefix, state_prefix)
	memofun pinvPf (P, f, k) =
		if P inset univ
		    then let val rem = gensym rem_name
			 in
			     put "\nRemark "; put rem; put " : ";
			     coq_print_foralls (ver, fd) (xname, term_type, k);
			     pPfvars (P, f, xname, k);
			     put " -> True.\nProof.\n  ";
			     put intros_tac; put dot_tac; put " ";
			     put trivial_tac; put dot_tac;
			     put "\nQed.\n";
			     rem
			 end
		else let val blkls = if P inset auto
					 then let val fmap = ?auto P
					      in
						  if f inset fmap
						      then #1 (?fmap f)
						  else {}
					      end
				     else {}
			 val n = card blkls
			 val or_n = portype n
			 val rem = gensym rem_name
			 val ir = ref 0
			 val lispian = (case ver of
					    "7" => true
					  | _ => false)
		     in
			 put "\nRemark "; put rem; put " : ";
			 coq_print_foralls (ver, fd) (xname, term_type, k);
			 pPfvars (P, f, xname, k);
			 put " -> ";
			 if n=0
			     then put or_n
			 else (if lispian then put "(" else ();
			       put or_n;
			       put "\n";
			       iterate
				 (case [blk | blk in list blkl
						such that not (empty blk)] of
				      nil => put "    True"
				    | [{_}] => (put "    ";
						if lispian then ()
						    else put "(";
						pblocks ("", xname, blkl);
						if lispian then ()
						    else put ")"
						)
				    | _ => (put "    (";
					    pblocks (" /\\ ", xname, blkl);
					    put ")\n"))
			       | blkl in set blkls
			       end;
			       if lispian then put ")" else ());
			     put ".\nProof.\n  ";
			     put intros_tac; put dot_tac; put " ";
			     put inversion_tac; put " H"; put dot_tac;
			     put "\n";
			     iterate
			       (put "  "; put intros_tac; put dot_tac; put " ";
				put apply_tac; put or_n; put "_intro_";
				inc ir; print fd (pack (!ir));
				put semi_tac; put tauto_tac; put dot_tac;
				put "\n")
			     | blkl in set blkls
			     end;
			     put "Qed.\n";
			     rem
		     end
    in
	pinvPf
    end;

fun coq_print_ex_type (ver, f as |[put, ...]|, ex_prefix, xname) =
    let val |[param_prolog, param_delim, param_epilog,
	      forall_prolog, forall_midlog, ...]|
	= coq_keywords ver
	val pvars = coq_print_vars f
	memofun pextype (n : int) =
		let val ex_n = let val g as |[convert, ...]| = outstring ex_prefix
			       in
				   print g (pack n);
				   convert ()
			       end
		    val ir = ref 0
		in
		    put "\nInductive "; put ex_n;
		    put " "; put param_prolog;
		    put "A: Set"; put param_delim; put "P : ";
		    iterate
		      (inc ir; put " A -> ")
		    |while !ir<n
		    end;
		    put "Prop"; put param_epilog;
		    put " : Prop :=\n    "; put ex_n; put "_intro : ";
		    ir := 0;
		    iterate
		      (put forall_prolog;
		       put xname; inc ir; print f (pack (!ir));
		       put ":A"; put forall_midlog)
		    |while !ir<n
		    end;
		    ir := 0;
		    if n=0
			then put "P"
		    else (put "(P";
			  iterate
			    (put " "; put xname; inc ir; print f (pack (!ir)))
			  |while !ir<n
			  end;
			  put ")");
			put " -> ("; put ex_n; put " A P).\n";
			ex_n
		end
    in
	pextype
    end;

fun coq_print_inversion_P (ver, fd as |[put, ...]|, portype, pextype,
			   fun_prefix, state_prefix, rem_name, xname, term_type,
			   AUTO (auto, univ), CAN (autonamer, _)) =
    let val |[fun_paren_prolog, var_delim, fun_midlog, fun_paren_epilog,
	      intros_tac, trivial_tac, inversion_tac,
	      apply_tac, eapply_tac, refl_tac, dot_tac, ...]|
	= coq_keywords ver
	val pblocks = coq_print_blocks (ver, fd, state_prefix)
	val pforall = coq_print_forall (ver, fd)
	val pPx = coq_print_Px (ver, fd, state_prefix)
	val pvars = coq_print_vars fd
	val pfvars = coq_print_f_vars (fd, fun_prefix)
	memofun pinvP P =
		if P inset univ
		    then let val rem = gensym rem_name
			 in
			     put "\nRemark "; put rem; put " : ";
			     pforall (xname, term_type);
			     pPx (P, xname);
			     put " -> True.\nProof.\n  ";
			     put intros_tac; put dot_tac; put " ";
			     put trivial_tac; put dot_tac;
			     put "\nQed.\n";
			     rem
			 end
		else let val fmap = if P inset auto
					then ?auto P
				    else {}
			 val n = card fmap
			 val or_n = portype n
			 val ex_ns = {f => pextype k
				     | f => (_, k, _) in map fmap}
			 val rem = gensym rem_name
			 val ir = ref 0
			 val lispian = (case ver of
					    "7" => true
					  | _ => false)
		     in
			 put "\nRemark "; put rem; put " : ";
			 pforall (xname, term_type);
			 pPx (P, xname);
			 put " -> ";
			 if n=0
			     then put or_n
			 else (if lispian then put "(" else ();
			       put or_n; put "\n";
			       iterate
				 (put "  ("; put (?ex_ns f); put " "; put term_type;
				  if k=0
				      then (put " "; put xname; put "="; put f)
				  else (put " "; put fun_paren_prolog;
					pvars (var_delim, xname, k); put ":";
					put term_type; put fun_midlog; put " ";
					put xname; put "=";
					pfvars (f, xname, k);
					put fun_paren_epilog
					);
				      put ")\n"
				      )
			       | f => (blkls, k, _) in map fmap
			       end;
			       if lispian then put "  )" else put "  ");
			     put ".\nProof.\n  ";
			     put intros_tac; put dot_tac; put " ";
			     put inversion_tac; put " H"; put dot_tac;
			     put "\n";
			     iterate
			       (inc ir;
				iterate
				  (put "  "; put apply_tac;
				   put or_n; put "_intro_";
				   print fd (pack (!ir));
				   put dot_tac; put " ";
				   put eapply_tac;
				   put "("; put (?ex_ns f); put "_intro ";
				   put term_type; put ")";
				   put dot_tac; put " ";
				   put refl_tac; put dot_tac; put "\n")
				| blkl in set blkls
				end)
			     | f => (blkls, k, _) in map fmap
			     end;
			     put "Defined.\n";
			     rem
		     end
    in
	pinvP
    end;

exception CoqPrintSuperclause;
exception McSubsumedDone;

fun superclause_vars (c, orandl) =
    gclause_vars c U union {union {tvars a
				  | a in list andl}
			   | andl in list orandl};

fun coq_print_superclause (ver, f as |[put, ...]|, fun_prefix, state_prefix, varname, term_type) =
    let val pvars = coq_print_gclause_vars (ver, f, varname, term_type)
	val pneg = coq_print_gclause_neg (ver, f, fun_prefix, state_prefix, varname, term_type)
	val ppos = coq_print_gclause_pos (ver, f, fun_prefix, state_prefix, varname, term_type)
	val patom = coq_print_atom (ver, f, fun_prefix, state_prefix, varname, term_type)
	val delimr = ref ""
	fun pandl nil = put "True"
	  | pandl [a] = patom a
	  | pandl (a::l) = (patom a; put " /\\ "; pandl l)
	fun pandl0 (andl as [_, _, ...]) =
	    (put "("; pandl andl; put ")")
	  | pandl0 andl = pandl andl
	fun psc (gc, orandl) =
	    (pvars gc; pneg gc;
	     iterate
	       (pandl0 andl; put " \\/ ")
	     | andl in list orandl
	     end;
	     ppos gc)
    in
	psc
    end;

fun justif_superclause (MC_DISTR_POS (c, orandl, ...)) = (c, orandl)
  | justif_superclause (MC_SUBSUMED_SUPER (c, orandl, ...)) = (c, orandl)
  | justif_superclause (MC_CUT_HISTORY (_, j)) = justif_superclause j
  | justif_superclause j = (justif_gclause j, nil)
	    ;

fun epsc_name (neg, pos) =
    let val f as |[put, convert, ...]| = outstring "epsilon"
    in
	iterate
	  (put "_m"; put P)
	| P in set neg
	end;
	iterate
	  (put "_p"; put P)
	| P in set pos
	end;
	convert ()
    end;

exception HeadSelect;
exception FindP;
exception FindFromNeg;
exception PJustif;

fun find_from_neg (a, nil) = raise FindFromNeg
  | find_from_neg (a, b::l) =
    if a=b then 0 else 1+find_from_neg (a, l)

fun coq_print_justif (AUTO (auto, univ),
		      ver,
		      fd as |[put, ...]|,
		      fun_prefix, state_prefix,
		      rem_name, varname, xname, term_type,
		      portype,
		      pinvPf, (* typically coq_print_inversion_P_f (fd, portype, fun_prefix, state_prefix, rem_name,
			      varname, term_type, AUTO (auto, univ), CAN (autonamer, univnamer)) *)
		      pinvP, (* typically coq_print_inversion_P (fd, portype, pextype, fun_prefix, state_prefix, rem_name,
			      xname, term_type, CAN (autonamer, univnamer)) *)
		      CAN (autonamer, univnamer)) =
    let val |[left_tac, right_tac, forall_prolog, forall_midlog,
	      intro_tac, clear_tac, intros_tac, tauto_tac,
	      apply_tac, assum_tac, cut_tac, cut_end, exact_tac,
	      elim_tac, case_tac, fix_tac,
	      first_tac, inversion_tac,
	      dot_tac, semi_tac, ...]|
	= coq_keywords ver
	val lispian = (case ver of
			   "7" => true
			 | _ => false)
	val pgclause = coq_print_gclause (ver, fd, fun_prefix, state_prefix, varname, term_type)
	val ppos = coq_print_gclause_pos (ver, fd, fun_prefix, state_prefix, varname, term_type)
	val plits = coq_print_gclause_lits (ver, fd, fun_prefix, state_prefix, varname, term_type)
	val psc = coq_print_superclause (ver, fd, fun_prefix, state_prefix, varname, term_type)
	val pP = coq_pred_name (state_prefix, term_type)
	val pterm = coq_print_term (fd, fun_prefix, varname)
	val pvars = coq_print_vars fd
	fun hsel (0, [a]) = ()
	  | hsel (0, [a, ...]) = (put " "; put left_tac; put dot_tac)
	  | hsel (_, nil) = raise HeadSelect
	  | hsel (i, a::l) = (put " "; put right_tac; put dot_tac;
			      hsel (i-1, l))
	fun head_select (i, GCLAUSE (_, pos)) =
	    hsel (i, pos)
	val popen = if lispian then fn () => put "(" else fn () => ()
	val pclose = if lispian then fn () => put ")" else fn () => ()
	fun print_epsc (neg, pos) =
	    (put forall_prolog; put xname; put ":"; put term_type;
	     put forall_midlog;
	     iterate
	       (popen ();
		put (pP P); put " "; put xname;
		pclose ();
		put " -> ")
	     | P in set neg
	     end;
	     case pos of
		 {} => put "False"
	       | _ => let val delimr = ref ""
		      in
			  iterate
			    (put (!delimr);
			     delimr := " \\/ ";
			     popen (); put (pP P); put " "; put xname; pclose ())
			  | P in set pos
			  end
		      end)
	fun print_epsc_t ((neg, pos), t) =
	    (iterate
	       (popen (); put (pP P); put " "; pterm t; pclose (); put " -> ")
	     | P in set neg
	     end;
	       case pos of
		   {} => put "False"
		 | _ => let val delimr = ref ""
			in
			    iterate
			      (put (!delimr);
			       delimr := " \\/ ";
			       popen (); put (pP P); put " "; pterm t; pclose ())
			    | P in set pos
			    end
			end)
	fun phistory {} = ()
	  | phistory ({epsc => _} U rest) =
	    (put "("; print_epsc epsc; put ")\n    -> "; phistory rest)
	fun clear_history h =
	    iterate
	      (put " "; put intro_tac; put "H"; put dot_tac; put " ";
	       put clear_tac; put "H"; put dot_tac)
	    | _ in set h
	    end
	fun names_history h =
	     iterate
	       (put " "; put Hname)
	     | epsc => Hname in map h
	     end
	fun intro_history {} = ()
	  | intro_history h =
	    (put " "; put intros_tac;
	     names_history h;
	     put dot_tac)
	fun intro_from_history (epsc, h) =
	    iterate
	      if epsc=epsc'
		  then (put " "; put intro_tac; put "Hrec"; put dot_tac)
	      else (put " "; put intro_tac; put "H"; put dot_tac; put " ";
		    put clear_tac; put "H"; put dot_tac)
	    | epsc' in set h
	    end
	fun intro_impls impls =
	    if impls=""
		    then ()
		else (put " "; put intros_tac; put impls; put dot_tac;
		      put "\n")
	val sort_vars = sort (op strless);
	fun varnames vars = sort_vars {varname x | x in set vars}
	fun pvarnames {} = ()
	  | pvarnames vars =
	    iterate
	      (put " "; put x)
	    | x in list varnames vars
	    end
	fun intro_vars {} = ()
	  | intro_vars vars =
	    (put " "; put intros_tac; pvarnames vars; put dot_tac)
	fun imply_names (H, GCLAUSE (neg, _)) =
	    let val f as |[put, convert, ...]| = outstring ""
		val ir = ref 0
	    in
		iterate
		  (put " "; put H; inc ir; print f (pack (!ir)))
		| _ in list neg
		end;
		convert ()
	    end
	fun intros_until_i (n, Hname, GCLAUSE (neg, _)) =
	    let val ir = ref 0
	    in
		(if n=0
		    then ()
		else (put " "; put intros_tac;
		      iterate
			(inc ir; put " "; put Hname; print fd (pack (!ir)))
		      |while !ir<n
		      end;
		      put dot_tac));
		    put " "; put intro_tac; put Hname; put dot_tac
	    end
	fun intros_from_neg (a, Hname, c as GCLAUSE (neg, _)) =
	    let val n = find_from_neg (a, neg)
	    in
		intros_until_i (n, Hname, c)
	    end
	val done_clauses = ref {}
	fun find_done_clauses (j, history) =
	    if j inset !done_clauses
		then let val hs = ?(!done_clauses) j
		     in
			 if history inset hs
			     then SOME (?hs history, history)
			 (* prefer exact match *)
			 else
			     some
			       (res, history')
			     | history' => res in map hs
				 such that history' subset history
			     end
		     end
	    else NONE
	fun add_done_clauses (j,history,res) =
	    if j inset !done_clauses
		then done_clauses := !done_clauses
		    ++ {j => ?(!done_clauses) j ++ {history => res}}
	    else done_clauses := !done_clauses ++ {j => {history => res}}
	fun pjustif (h, epsdone, MC_DONE j) =
	    (case find_done_clauses (j,h) of
		 SOME (res,h') =>
		 if h=h'
		     then res (* nothing to do *)
		 else let val (newdone, remj) = pjustif (h',epsdone,j)
			  val rem = gensym rem_name
			  val donerem = (newdone,rem)
			  val c = justif_gclause j
		      in
			  put "\nRemark "; put rem; put " : ";
			  phistory h; pgclause c;
			  put ". (* Already proved, with different history. *)\nProof.  ";
			  intro_history h; put " ";
			  put exact_tac; put "(";
			  put remj; names_history h';
			  put ")"; put dot_tac; put "\nDefined.\n";
			  add_done_clauses(j,h,donerem);
			  donerem
		      end
	       | _ =>
		 (*raise PJustif*)
		 (*!!!should still check those cases where this happens...*)
		 pjustif (h, epsdone, j))
	  | pjustif (h, epsdone, j) =
	    let val rem = pjustif_1 (h, epsdone, j)
	    in
		add_done_clauses(j,h,rem);
		rem
	    end
	and pjustif_1 (h : epsilon_gclause -m> string,
		       epsdone : epsilon_gclause -m> string promise,
		       MC_TAUTO (c, i)) =
	    let val rem = gensym rem_name
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; pgclause c;
		put ". (* Tautology. *)\nProof.";
		clear_history h; put " "; put tauto_tac;
		put dot_tac; put " Defined.\n";
		(epsdone, rem)
	    end
	  | pjustif_1 (h, epsdone, MC_CUT_HISTORY (h', j)) =
	    if h=h'
		then pjustif_1 (h, epsdone, j)
	    else if h' subset h
		then let val (newdone, remj) = pjustif (h',epsdone,j)
			 val rem = gensym rem_name
			 val donerem = (newdone,rem)
			 val c = justif_gclause j
		     in
			 put "\nRemark "; put rem; put " : ";
			 phistory h; pgclause c;
			 put ". (* Cut history. *)\nProof.  ";
			 intro_history h; put " ";
			 put exact_tac; put "(";
			 put remj; names_history h';
			 put ")"; put dot_tac; put "\nDefined.\n";
			 donerem
		      end
	    else raise CutHistory
	  | pjustif_1 (h, epsdone, MC_SUBSUMED_UNIV (c, P, i)) =
	    let val rem = gensym rem_name
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; pgclause c;
		put ". (* Subsumed by universal clause. *)\nProof. ";
		put intros_tac; put dot_tac;
		head_select (i, c);
		put " "; put apply_tac; put (univnamer P);
		put dot_tac; put " Defined.\n";
		(epsdone, rem)
	    end
	  | pjustif_1 (h, epsdone, MC_SUBSUMED_AUTO (c, P, f, k, sigma, blkl, i)) =
	    let val rem = gensym rem_name
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; pgclause c;
		put ". (* Subsumed by automaton clause. *)\nProof. ";
		put intros_tac; put dot_tac;
		head_select (i, c);
		put " "; put apply_tac;
		put (autonamer (P, f, blkl));
		put semi_tac; put " "; put assum_tac; put dot_tac;
		put " Defined.\n";
		(epsdone, rem)
	    end
	  | pjustif_1 (h, epsdone, MC_SUBSUMED_HISTORY (c, epsc, t)) =
	    let val rem = gensym rem_name
		val vars = gclause_vars c
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; pgclause c;
		put ". (* Recursive call to history. *)\nProof.\n  ";
		intro_from_history (epsc, h); intro_vars vars;
		put "\n  "; put cut_tac; print_epsc_t (epsc, t); put cut_end;
		put dot_tac; put " "; put tauto_tac; put dot_tac; put " ";
		put exact_tac; put "(Hrec "; pterm t; put ")";
		put dot_tac; put "\nDefined.\n";
		(epsdone, rem)
	    end
	  | pjustif_1 (h, epsdone, MC_SUBSUMED_DONE (c, epsc, t)) =
	    let val remeps = force (?epsdone epsc) handle MapGet => raise McSubsumedDone
		val rem = gensym rem_name
		val vars = gclause_vars c
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; pgclause c;
		put ". (* Subsumed by epsilon clause proved earlier. *)\nProof.  ";
		intro_history h; intro_vars vars;
		put " "; put intros_tac; put dot_tac;
		put "\n  "; put cut_tac; print_epsc_t (epsc, t); put cut_end;
		put dot_tac; put " ";
		put tauto_tac; put dot_tac; put " ";
		put exact_tac; put "("; put remeps; put " "; pterm t;
		put ")"; put dot_tac; put "\nDefined.\n";
		(epsdone, rem)
	    end
	  | pjustif_1 (h, epsdone, MC_ELIM_UNIV_NEG (c, P, i, j)) =
	    let val doner = ref epsdone
		val (newdone, remj) = pjustif (h, !doner, j)
		val vars = gclause_vars c
		val cj = justif_gclause j
		val vars' = gclause_vars cj
		val rem = gensym rem_name
	    in
		doner := newdone;
		put "\nRemark "; put rem; put " : ";
		phistory h; pgclause c;
		put ". (* Eliminate negative atom by universal clause. *)\nProof.\n  ";
		intro_history h; intro_vars vars;
		put " "; put intros_tac; put dot_tac; put " ";
		put apply_tac;
		if empty h andalso empty vars'
		    then put remj
		else (put "("; put remj; names_history h;
		      pvarnames vars'; put ")");
		    put semi_tac; put " ";
		    put assum_tac; put dot_tac;
		    put "\nDefined.\n";
		(!doner, rem)
	    end
	  | pjustif_1 (h, epsdone, MC_ELIM_NEG (c, a, k, sigma, jl)) =
	    let val doner = ref epsdone
		val reml = [(doner := newdone; remj)
			   | j in list jl
			       val (newdone, remj) = pjustif (h, !doner, j)]
		val vars = gclause_vars c
		val P $ [f $ l] = a
		val invPf = pinvPf (P, f, k)
		val rem = gensym rem_name
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; pgclause c;
		put ". (* Eliminate negative atom. *)\nProof.\n  ";
		intro_history h; intro_vars vars;
		intros_from_neg (a, "H", c); (* H : a, where a = P(f(t1,...,tk)) *)
		put "\n  "; put elim_tac; put "("; put invPf;
		iterate
		  (put " "; pterm t)
		| t in list l
		end;
		put " H)"; put semi_tac; put " "; put intros_tac;
		put dot_tac; put "\n";
		iterate
		  (put "  "; put apply_tac;
		   let val vars' = gclause_vars (justif_gclause j)
		   in
		       if empty h andalso empty vars'
			   then put remj
		       else (put "("; put remj; names_history h;
			     pvarnames vars';
			     put ")");
			   put semi_tac; put " "; put tauto_tac;
			   put dot_tac; put "\n"
		   end)
		|| remj in list reml and j in list jl
		end;
		put "Defined.\n";
		(!doner, rem)
	    end
	  | pjustif_1 (h, epsdone, MC_DEDUCE_POS (c, a, i, blkls, j)) =
	    let val (newdone, remj) = pjustif (h, epsdone, j)
		val vars = gclause_vars c
		val P $ [f $ l] = a
		val rem = gensym rem_name
		val firstr = ref true
		val impls = imply_names ("A", c)
		val sc = justif_superclause j
		val scvars = superclause_vars sc
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; pgclause c;
		put ". (* Deduce positive atom. *)\nProof.\n  ";
		intro_history h; intro_vars vars;
		intro_impls impls;
		if empty blkls
		    then let val cj = justif_gclause j
			 (* although j is usually a justification
			  for a superclause, since blkls is empty,
			  j will in fact be the justification of
			  a gclause. *)
			 in
			     put "  "; put cut_tac; ppos cj; put cut_end;
			     put dot_tac; put " ";
			     put tauto_tac; put dot_tac; put "\n";
			     if empty h andalso empty vars andalso impls=""
				 then put remj
			     else (put "  "; put exact_tac;
				   put "("; put remj; names_history h;
				   pvarnames scvars;
				   put impls; put ")";
				   put dot_tac; put "\n")
			 end
		else
		    (iterate
		       (if !firstr
			    then (firstr := false;
				  put "  "; put case_tac;
				  if empty h andalso empty vars
				      andalso impls=""
				      then put remj
				  else (put "("; put remj; names_history h;
					pvarnames scvars;
					put impls; put ")"))
			else (put "  "; put intro_tac; put "H";
			      put semi_tac; put " ";
			      put case_tac; put "H";
			      put semi_tac; put " ";
			      put clear_tac; put "H");
			    put dot_tac; (* was not added if !firstr, empty h andalso empty vars; corrected Jan 24, 2008 JGL. *)
			    (if empty h andalso impls=""
				 then ()
			     else (put " "; put clear_tac; names_history h;
				   put impls; put dot_tac));
			    put " ";
			    put intros_tac; put dot_tac;
			    head_select (i, c);
			    put " "; put apply_tac;
			    put (autonamer (P, f, blkl));
			    put semi_tac; put " "; put tauto_tac;
			    put dot_tac; put "\n")
		     | blkl in set blkls
		     end;
		       (if empty h andalso impls=""
			    then ()
			else (put " "; put clear_tac; names_history h;
			      put impls; put dot_tac));
		       put " "; put tauto_tac;
		       put dot_tac; put "\n");
		       put "Defined.\n";
		       (newdone, rem)
	    end
	  | pjustif_1 (h, epsdone, MC_DISTR_POS (c, orandl, jl)) =
	    let val doner = ref epsdone
		val reml = [(doner := newdone; remj)
			   | j in list jl
			       val (newdone, remj) = pjustif (h, !doner, j)]
		val vars = superclause_vars (c, orandl)
		val impls = imply_names ("A", c)
		val rem  = gensym rem_name
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; psc (c, orandl);
		put ". (* Distribute disjunctions over conjunctions. *)\nProof.\n  ";
		intro_history h; intro_vars vars;
		intro_impls impls;
		iterate
		  let val cj = justif_gclause j
		  in
		      put "  "; put cut_tac; ppos cj; put cut_end;
		      put dot_tac; put " 2:";
		      put apply_tac;
		      if empty h andalso empty vars
			  then put remj
		      else (put "("; put remj; names_history h;
			    pvarnames (gclause_vars cj);
			    put ")"; put semi_tac; put " "; put assum_tac);
			  put dot_tac; put "\n"
		  end
		|| remj in list reml and j in list jl
		end;
		put "  "; put tauto_tac; put dot_tac; put "\nDefined.\n";
		(!doner, rem)
	    end
	  | pjustif_1 (h, epsdone, MC_SUBSUMED_SUPER (c, orandl, j)) =
	    let val (newdone, remj) = pjustif (h, epsdone, j)
		val vars = superclause_vars (c, orandl)
		val impls = imply_names ("A", c)
		val sc = justif_superclause j
		val scvars = superclause_vars sc
		val rem = gensym rem_name
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; psc (c, orandl);
		put ". (* Prove a smaller disjunction. *)\nProof.\n  ";
		intro_history h; intro_vars vars; intro_impls impls;
		put "  "; put case_tac;
		if empty h andalso empty scvars andalso impls=""
		    then put remj
		else (put "("; put remj; names_history h;
		      pvarnames scvars;
		      put impls; put ")");
		    put semi_tac; put " "; put tauto_tac;
		    put dot_tac; put "\nDefined.\n";
		(newdone, rem)
	    end
	  | pjustif_1 (h, epsdone, MC_SUBSUMED (c, j)) =
	    let val (newdone, remj) = pjustif (h, epsdone, j)
		val rem = gensym rem_name
		val vars = gclause_vars c
		val jc = justif_gclause j
		val vars' = gclause_vars jc
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; pgclause c;
		put ". (* Subsumption by simpler clause. *)\nProof.\n  ";
		intro_history h; intro_vars vars;
		put "\n  "; put cut_tac; plits jc; put cut_end;
		put dot_tac; put " "; put tauto_tac;
		put dot_tac; put " "; put exact_tac;
		if empty h andalso empty vars'
		    then put remj
		else (put "("; put remj; names_history h;
		      pvarnames vars'; put ")");
		    put dot_tac; put "\nDefined.\n";
		(epsdone, rem)
	    end
	  | pjustif_1 (h, epsdone, MC_SPLIT (c, j)) =
	    let val (newdone, remj) = pjustif (h, epsdone, j)
		val cj = justif_gclause j
		val vars = gclause_vars c
		val varsj = gclause_vars cj
		val rem = gensym rem_name
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; pgclause c;
		put ". (* Split. *)\nProof.\n  ";
		intro_history h; intro_vars vars; put "\n";
		put "  "; put cut_tac; plits cj; put cut_end; put dot_tac;
		if empty h
		    then ()
		else (put " "; put clear_tac; names_history h; put dot_tac);
		    put " "; put tauto_tac; put dot_tac; put "\n";
		    put "  "; put exact_tac;
		    if empty h andalso empty vars
			then put remj
		    else (put "("; put remj; names_history h;
			  pvarnames varsj;
			  put ")");
			put dot_tac; put "\nDefined.\n";
			(newdone, rem)
	    end
	  | pjustif_1 (h, epsdone, MC_INDUCT (x, epsc as (neg, pos), P, jl)) =
	    let val Hname = epsc_name epsc
		val h' = h ++ {epsc => Hname}
		val doner = ref epsdone
		val reml = [(doner := newdone; remj)
			   | (_, _, j) in list jl
			       val (newdone, remj) = pjustif (h', !doner, j)]
		(*val invP = pinvP P*)
		val i = let fun findP (i, {Q} U rest) =
				if P=Q
				    then i
				else findP (i+1, rest)
			      | findP _ = raise FindP
			in
			    findP (1, neg)
			end
		val rem = gensym rem_name
		val newdone = {epsc' =>
				delay let val rem1 = force future_rem
					  val rem2 = gensym rem_name
				      in
					  put "\nRemark "; put rem2; put " : ";
					  phistory h;
					  put forall_prolog;
					  put (varname x); put ":";
					  put term_type;
					  put forall_midlog;
					  print_epsc_t (epsc', V x);
					  put ". (* Pop history. *)\nProof.\n  ";
					  intro_history h;
					  put " "; put exact_tac;
					  put "("; put rem1;
					  iterate
					    (put " ";
					     if e = epsc
						 then if empty h
							  then put rem
						      else (put "("; put rem;
							    names_history h;
							    put ")")
					     else put H)
					  | e => H in map h'
					  end;
					  put ")"; put dot_tac;
					  put "\nDefined.\n";
					  rem2
				      end
			      | epsc' => future_rem in map epsdone <-| !doner}
		    ++ epsdone
		    ++ {epsc => delay rem}
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h;
		put forall_prolog;
		put (varname x); put ":"; put term_type;
		put forall_midlog;
		print_epsc_t (epsc, V x);
		put ". (* Induct. *)\nProof.\n  "; intro_history h;
		put " "; put fix_tac; put Hname; put " 1";
		(* print fd (pack (card h+1));*) (* print fd (pack (i+1)); *)
		put dot_tac; put "\n  ";
		put intro_tac; put xname; put dot_tac; put " ";
		put case_tac; put xname; put semi_tac; put " ";
		put first_tac;
		let val delimr = ref "["
		in
		    iterate
		      (put (!delimr); delimr := "\n  | ";
		       if k<>0
			   then (put " "; put intros_tac; put " ";
				 pvars (" ", xname, k);
				 put semi_tac; put " ")
		       else ();
			   put exact_tac;
			   put "("; put remj; names_history h'; put " ";
			   pvars (" ", xname, k); put ")")
		    || remj in list reml and (_, k, j) in list jl
		    end;
		    put (!delimr);
		    put " "; put intros_tac;
		    put " until 1";
		    put semi_tac; put " ";
		    put inversion_tac; put "H]";
		    put dot_tac; put "\nDefined.\n"
		end;
		(newdone, rem)
	    end
    in
	pjustif
    end;

(*
fun std_coq_memos fd =
    let val std_portype = coq_print_or_type (fd, "or_")
	val std_pextype = coq_print_ex_type (fd, "ex_", "x")
	val std_autonamer = CAN (coq_auto_clause_name "trans_", coq_univ_clause_name "univ_")
    in
	(std_portype, std_pextype, std_autonamer)
    end;

fun std_coq_print_justif (A, fd, fun_prefix, state_prefix, rem_name, varname, xname, term_type) =
    let val (portype, pextype, autonamer) = std_coq_memos fd
	val pinvPf = coq_print_inversion_P_f (fd, portype, fun_prefix, state_prefix, rem_name, xname, term_type,
					      A, autonamer)
	val pinvP = coq_print_inversion_P (fd, portype, pextype, fun_prefix, state_prefix, rem_name, xname, term_type,
					   A, autonamer)
	val pjustif = coq_print_justif (A, fd, fun_prefix, state_prefix, rem_name, varname, xname, term_type,
					portype, pinvPf, pinvP, autonamer)
    in
	fn j => pjustif ({}, j)
    end;
*)
