(* print natural deduction proof in Coq format.
   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 "pfcprintcoq_h";
open "coq_fun_h";
open "coq_term_h";
open "coq_gclause_h";
open "coq_kw_h";
open "sort_h";
open "topsort_h";
open "gensym_h";

(*
val Xsort = sort (op strless);
*)

exception PfcCName;
exception PfcPrintCoq;

fun pfc_print_coq_proofs (ver, f as |[put, ...]|,
			  thm_kwd, thm_prefix,
			  fun_prefix, state_prefix, by_def, by_app,
			  do_abort,
			  varname, varsort, term_type, pfal) =
    let val |[dot_tac, intros_tac, tauto_tac, exact_tac, ...]| =
	    coq_keywords ver
	val cpt = coq_print_term (f, fun_prefix, varname)
	val cpgc = coq_print_gclause (ver, f,
				      fun_prefix, state_prefix,
				      varname, varsort, term_type)
	fun cname (PFC_DEF, c) = by_def c
	  | cname (PFC_INPUT, c) = by_app c
	  | cname _ = raise PfcCName
	fun pspaces 0 = ()
	  | pspaces n = (put " "; pspaces (n-1))
	val axioms = ref {}
	fun pfc_pr_axioms (PFC (PFC_AXIOM axkind, (Xs, c), _, pfs), assums) =
	    (iterate
	       pfc_pr_axioms (pfc, assums)
	     | pfc in list pfs
	     end;
	       if c inset !axioms orelse c inset assums
		   then ()
	       else let val rem_name = gensym "rem_"
		    in
			axioms := !axioms ++ {c => rem_name};
			put "Remark "; put rem_name; put " : ";
			cpgc c; put ".\nProof. ";
			put intros_tac; put dot_tac; put " ";
			put tauto_tac; put dot_tac; put " ";
			put "Qed.\n\n"
		    end
		)
	  | pfc_pr_axioms (PFC (kind, (_, c), _, pfs), assums) =
	    (iterate
	       pfc_pr_axioms (pfc, assums)
	     | pfc in list pfs
	     end;
	       if c inset !axioms orelse c inset assums
		   then ()
	       else (cname (kind, c); ()) handle PfcCoqNoNameEvt =>
		   let val rem_name = gensym "rem_"
		   in
			axioms := !axioms ++ {c => rem_name};
			put "Axiom "; put rem_name; put " : ";
			cpgc c; put ". (* UNPROVED! *)\n"
		   end)
	fun pfc_pr (PFC (PFC_AXIOM "inj", ax as (Xs, c), ts, pfs),
		    lmargin, assums) =
	    (let val ax = ?(!axioms) c
	     in
		 if null ts andalso null pfs
		     then put ax
		 else let val lmargin' = lmargin+2
		      in
			  put "("; put ax;
			  iterate
			    (put " "; cpt t)
			  | t in list ts
			  end;
			  iterate
			    (put "\n"; pspaces lmargin';
			     pfc_pr (pf, lmargin', assums))
			  | pf in list pfs
			  end;
			  put ")"
		      end
	     end handle Bind => raise PfcPrintCoq)
	  | pfc_pr (PFC (kind, (Xs, c), ts, pfs), lmargin, assums) =
	    if null ts andalso null pfs
		then put (if c inset assums then ?assums c
			  else if c inset !axioms then ?(!axioms) c
			  else cname (kind, c))
	    else let val lmargin' = lmargin+2
		 in
		     put "("; put (if c inset assums then ?assums c
				   else if c inset !axioms then ?(!axioms) c
				   else cname (kind, c));
		     iterate
		       (put " "; cpt t)
		     | t in list ts
		     end;
		     iterate
		       (put "\n"; pspaces lmargin';
			pfc_pr (pf, lmargin', assums))
		     | pf in list pfs
		     end;
		     put ")"
		 end
	  | pfc_pr arg = raise PfcPrintCoq
	val pfcl = [(name, pfc, assums, c, Xs)
		   | (name, c as GCLAUSE (neg, pos), pfa) in list pfal
		       val Xs = varsort (gclause_vars c)
		       val pi_l = [pfc'
				  | a in list neg
				      val pfc' = PFC (PFC_INPUT,
						      (nil, GCLAUSE (nil, [a])),
						      nil, nil)]
		       val PF_L0 pfc =
			   pfc_apply_l_2 (pfc_apply_l_1 (pfa, [V X | X in list Xs]),
					    pi_l)
		       val f as |[convert, tell, seek, truncate, ...]| =
			     outstring "H"
		       val n = tell ()
		       val ir = ref 0
		       val assums = {GCLAUSE (nil, [a]) =>
				      (seek n; truncate ();
				       inc ir;
				       print f (pack (!ir));
				       convert ())
				    | a in list neg}
			such that (pfc_pr_axioms (pfc, assums); true)
			    handle PfcCoqAbortEvt => (do_abort (name, c);
						      false)
			   ]
    in
	iterate
	  (put "\n"; put thm_kwd; put " "; put thm_prefix; put name;
	   put " : "; cpgc c;
	   put dot_tac;
	   put "\nProof.\n  ";
	   if null Xs'
	       then ()
	   else (put " "; put intros_tac;
		 iterate
		   (put " "; put X)
		 | X in list Xs'
		 end;
		 put dot_tac);
	   if null neg
	       then ()
	   else (put " "; put intros_tac;
		 iterate
		   (put " "; put H)
		 | a in list neg
		   val H = ?assums (GCLAUSE (nil, [a]))
		       handle MapGet => raise PfcPrintCoq
		 end;
		 put dot_tac);
	   put "\n  "; put exact_tac;
	   pfc_pr (pfc, 8, assums);
	   put dot_tac;
	   put "\nQed.\n")
	| (name, pfc, assums, c as GCLAUSE (neg, _), Xs) in list pfcl
	  val Xs' = [varname x | x in list varsort (gclause_vars c)]
	      (* Xsort {varname x | x in set gclause_vars c}
	       (* may not be in the same order as Xs. *)
	      *)
	end
    end;

fun pfc_print_coq (ver, f as |[put, ...]|, thm_kwd, thm_prefix,
		   fun_prefix, state_prefix,
		   definitions, approximation,
		   varname, varsort, term_type, pfcl) =
    let val |[exists_prolog, exists_midlog, exists_epilog,
	      fun_prolog, fun_midlog,
	      case_prolog, case_delim,
	      case_of, case_midlog, case_epilog,
	      var_delim, dot_tac,
	      intros_tac, unfold_tac, exists_tac, tauto_tac, ...]| =
	coq_keywords ver
	val apprx = [c | c in set approximation U definitions]
	val fsig0 = gclause_list_sig apprx
	val preds0 = gclause_list_pred_sig apprx
	val def_preds = {P => {Q
			      | Q $ _ in list neg}
			| GCLAUSE (neg, [P $ _]) in set definitions}
	val def_topsort = revtopsort (def_preds ++ {"" => dom def_preds}, "")
	val def_list = sort (fn (GCLAUSE (_, [P $ _]), GCLAUSE (_, [Q $ _])) =>
				?def_topsort P < ?def_topsort Q) definitions
	val cpt = coq_print_term (f, fun_prefix, varname)
	val cpgc = coq_print_gclause (ver, f, fun_prefix, state_prefix, varname, varsort, term_type)
	val defs = ref ({} : string gclause -m> string)
	val apps = ref ({} : string gclause -m> string)
    in
	put "(* Signature definition. *)\n\n";
	coq_print_sig (f, fun_prefix, term_type) fsig0;
	put "\n";
	coq_print_pred_sig (ver, f, "\nParameter", term_type) (def_preds <-| preds0);
	put "\nParameter __star__ : term. (* Used to show that term is not empty. *)\n";
	put "\n(* Definitions. *)\n\n";
	iterate
	  let val ir = ref 0
	      val f' as |[convert, tell, seek, truncate, ...]| = outstring "_x"
	      val n = tell ()
	      val xs = [(inc ir; seek n; truncate (); print f' (pack (!ir)); convert ())
		       | t in list l]
	      fun pr_ex nil = (case neg of
				   nil => put "True"
				 | _ => let val delimr = ref ""
					in
					    iterate
					      (put (!delimr); delimr := " /\\ ";
					       cpt t)
					    | t in list neg
					    end
					end)
		| pr_ex (X :: rest) =
		  (put exists_prolog; put X; put ":term";
		   put exists_midlog;
		   pr_ex rest;
		   put exists_epilog)
	      val rem_name = gensym "_rem_"
	      val vars_neg = [varname x | x in list varsort (gclause_vars c \ tvars a)]
		  (* Xsort {varname x | x in set gclause_vars c \ tvars a} *)
	  in
	      put "Definition "; put P; put " := ";
	      if null l
		  then ()
	      else let val delimr = ref fun_prolog
		   in
		       iterate
			 (put (!delimr); delimr := var_delim; put x)
		       | x in list xs
		       end;
		       put ":term"; put fun_midlog;
		       put " "; put case_prolog;
		       iterate
			 (put (!delimr); delimr := case_delim; put x)
		       | x in list xs
		       end;
		       put case_of;
		       delimr := "\n    ";
		       iterate
			 (put (!delimr); delimr := case_delim; cpt t)
		       | t in list l
		       end;
		       put case_midlog
		   end;
		   pr_ex vars_neg;
		   if null l
		       then (put dot_tac; put "\n")
		   else if card {x
				| V x in list l} = len l
		       then (put "\n  "; put case_epilog;
			     put dot_tac; put "\n")
		   else (put "\n  | ";
			 iterate
			   (put "_"; put case_delim)
			 | _ in list l
			 end;
			 put "=> False\n  ";
			 put case_epilog; put dot_tac; put "\n");
		   (* Now output a proof of c, using the definition. *)
		   defs := !defs ++ {c => rem_name};
		   put "Remark "; put rem_name; put " : ";
		   cpgc c; put ".\nProof.\n  ";
		   put intros_tac; put unfold_tac;
		   put P; put dot_tac;
		   iterate
		     (put " "; put exists_tac; put X; put dot_tac)
		   | X in list vars_neg
		   end;
		   put " "; put tauto_tac; put dot_tac;
		   put "\nQed.\n\n"
	  end
	| c as GCLAUSE (neg, [a as P $ l]) in list def_list
	end;
	put "\n(* Approximation. *)\n\n";
	iterate
	  let val rem_name = gensym "_rem_"
	  in
	      apps := !apps ++ {c => rem_name};
	      put "Axiom "; put rem_name; put " : ";
	      cpgc c; put ".\n"
	  end
	| c in set approximation
	end;
	(* Output proof. *)
	put "\n(* Proofs. *)\n";
	pfc_print_coq_proofs (ver, f,
			      thm_kwd, thm_prefix, fun_prefix, state_prefix,
			      fn c =>
				 if c inset !defs
				     then ?(!defs) c
				 else raise PfcCoqNoNameEvt,
			      fn c =>
				 if c inset !apps
				     then ?(!apps) c
				 else raise PfcCoqNoNameEvt,
			      fn _ => (),
			      varname, varsort,
			      term_type,
			      [(coq_pred_name (ver, "_thm", term_type) P,
				GCLAUSE (nil, [P $ nil]), PF_L0 pfc)
			      | pfc as PFC (_, (_, c as GCLAUSE (_, [P $ nil])), ...)
				in list pfcl])
    end;
