(* Coq printing functions for resolution proofs.
   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 "coq_term_h";
open "coq_clause_h";
open "coq_proof_h";
open "gensym_h";
open "sort_h";

val sort_vars = sort (op <);

(* Translate proof (as object of type 'proof', see clause_h.ml),
 into a Coq proof.
 Each proof step is translated as a separate \nRemark (this allows one to mask
 them: a series of \nRemarks in a Section are just removed from the Coq
 environment when one closes the Section).
 Assumes each clause CL (..., P_GIVEN name, ...) is given as:
 Definition name : clause.
 *)

fun coq_atom_Bs_length {} = 0
  | coq_atom_Bs_length ({_ => B} U rest) = card B + coq_atom_Bs_length rest;

fun coq_clause_body_length (CL (_, ql, al, Bs, ...)) =
    card ql + len al + coq_atom_Bs_length Bs;

(* !!! Don't forget to 'Require Refine' ! *)

exception AcHead;
exception AcP;
exception AcQ;
exception CoqPproof;

fun coq_print_proof (f as |[put, ...]|, rem_name, bot_prefix, prefix, term_type, xname) =
    let val pclause = coq_print_clause (f, bot_prefix, prefix, term_type, xname)
	val wit = "__" ^ term_type ^ "_witness"
	val p_uterm = coq_print_term (f, "", fn () => wit)
	val varnames = coq_clause_var_names xname
	fun pques 0 = ()
	  | pques n = (put " ?"; pques (n-1))
	fun intros {} = ()
	  | intros cvars =
	    (put "Intros";
	     iterate
	       (put " "; put (?cvars x))
	     | x in list sort_vars cvars
	     end;
	     put ".")
	fun spaces 0 = ()
	  | spaces n = (put " "; spaces (n-1))
	fun p_uproof (UP (c, sigma, upl), c_s, margin) =
	    (spaces margin;
	     put "Apply ";
	     if empty sigma
		 then ()
	     else put "(";
	     put (?c_s c);
	     iterate
	       (put " ";
		p_uterm (?sigma x))
	     | x in list sort_vars sigma
	     end;
	     if empty sigma
		 then ()
	     else put ")";
	     put ".\n";
	     iterate
	       p_uproof (up, c_s, margin+2)
	     | up in list upl
	     end)
	memofun pproof (CL (_, _, _, _, P_GIVEN s, ...)) = s
	      | pproof (c as CL (_, _, _, _, P_UNIT up, ...)) =
		let val rem = gensym rem_name
		    val c_s = uproofs_of up
		in
		    put "\nRemark "; put rem; put " : ";
		    pclause c; put ".\nProof.\n";
		    p_uproof (up, c_s, 2);
		    put "Qed.\n";
		    rem
		end
	      | pproof (c as CL (_, _, _, _, P_AUTO_RESOLVE (c', pi_l), ...)) =
		let val acc_l = [clause_from_automaton_clause ac
				| (ac, _) in list pi_l]
		    val ac_s_l = [pproof acc
				 | acc in list acc_l]
		    val CL (_, _, al', Bs', ...) = c'
		    val c'_s = pproof c'
		    val c'_vars = varnames c'
		    val c_vars = varnames c
		    val rem = gensym rem_name
		    fun p_witness () = put wit
		    fun ac_head (AC_UNIV (P, _), MGU_AUTO_X1_IS t) = (P, t)
		      | ac_head (AC_POP (P, f, ...), MGU_AUTO_Xs_ARE l) = (P, f $ l)
		      | ac_head (AC_POP_RAW (CL (HFUN (P, f, ...), ...)),
				 MGU_AUTO_Xs_ARE l) =
			(P, f $ l)
		      | ac_head _ = raise AcHead
		in
		    put "\nRemark "; put rem; put " : ";
		    pclause c; put ".\nProof.\n  ";
		    intros c_vars;
		    put " Intros.\n  Refine (";
		    put c'_s;
		    iterate
		      (put " ";
		       if x inset c_vars
			   then put (?c'_vars x)
		       else p_witness ())
		    | x in list sort_vars c'_vars
		    end;
		    iterate
		      (case some (acc, ac_s)
			    || acc in list acc_l and
			       ac_s in list ac_s_l and
			       ac_mgu in list pi_l
				 such that ac_head ac_mgu = a'
			    end of
			    SOME (acc, ac_s) =>
			    let val ac_vars = varnames acc
				val ac_n = coq_clause_body_length acc
				val ac_paren = ac_n<>0 orelse not (empty ac_vars)
			    in
				if ac_paren then put " (" else put " ";
				    put ac_s;
				    pques (card ac_vars);
				    pques ac_n;
				    if ac_paren then put ")" else ()
			    end
			 | _ => put " ?")
		    | a' in list al'
		    end;
		    iterate
		      pques (card B)
		    | _ => B in map Bs'
		    end;
		    put "); Assumption.\nQed.\n";
		    rem
		end
	      | pproof (c as CL (_, _, _, _, P_EPS_RESOLVE (c' as CL (_, _, _, {_ => B}, ...),
							    ac, t),
				 ...)) =
		let val acc = clause_from_automaton_clause ac
		    val ac_s = pproof acc
		    val c'_s = pproof c'
		    val ac_vars = varnames acc
		    val c'_vars = varnames c'
		    val c_vars = varnames c
		    val rem = gensym rem_name
		    val ac_n = coq_clause_body_length acc
		    val ac_paren = ac_n<>0 orelse not (empty ac_vars)
		    val ac_P = case ac of
			AC_UNIV (P, _) => P
		      | AC_POP (P, ...) => P
		      | AC_POP_RAW (CL (HFUN (P, ...), ...)) => P
		      | _ => raise AcP
		in
		    put "\nRemark "; put rem; put " : ";
		    pclause c; put ".\nProof.\n  ";
		    intros c_vars;
		    put " Intros.\n  Refine (";
		    put c'_s;
		    if 1 inset c'_vars
			then (put " "; coq_print_term (f, "", ?ac_vars) t)
		    else ();
			iterate
			  if P=ac_P
			      then (put (if ac_paren then " (" else " ");
				    put ac_s;
				    iterate
				      (put " "; put (?ac_vars x))
				    | x in list sort_vars ac_vars
				    end;
				    pques ac_n;
				    put (if ac_paren then ")" else "")
				    )
			  else put " ?"
			| P in set B
			end;
		    put "); Assumption.\nQed.\n";
		    rem
		end
	      | pproof (c as CL (_, _, _, _, P_Q_RESOLVE (c' as CL (_, ql, al, Bs, ...),
							  ac), ...)) =
		let val c'_s = pproof c'
		    val acc = clause_from_automaton_clause ac
		    val ac_s = pproof acc
		    val rem = gensym rem_name
		    val c_vars = varnames c
		    val ac_q = case ac of
				   AC_Q (q, ...) => q
				 | _ => raise AcQ
		in
		    put "\nRemark "; put rem; put " : ";
		    pclause c; put ".\nProof.\n  ";
		    intros c_vars; put " Intros. Refine ("; put c'_s;
		    iterate
		      (put " "; put (?c_vars x))
		    | x in list sort_vars c_vars
		    end;
		    iterate
		      if ac_q=q'
			  then (put " "; put ac_s)
		      else put " ?"
		    | q' in set ql
		    end;
		    pques (len al + coq_atom_Bs_length Bs);
		    put "); Assumption.\nQed.\n";
		    rem
		end
	      | pproof (c as CL (_, ql, _, _, P_SPLIT_USE (c', splitBs), ...)) =
		let val c'_s = pproof c'
		    val rem = gensym rem_name
		    val c_vars = varnames c
		    val c'_vars = varnames c'
		    val c'_paren = not (empty c'_vars)
		    val splitinv = inv splitBs (* map each q in ql to set of variables x
						such that x => q is in splitBs.
						This works because c' has no q in its body. *)
		in
		    put "\nRemark "; put rem; put " : ";
		    pclause c; put ".\nProof.\n  ";
		    intros (c_vars <| c'_vars);
		    (* put "\n  "; *)
		    iterate
		      if q inset splitinv
			  then let val x = ?splitinv q
			       in
				   put " Intro hyp; Elim hyp; Clear hyp; Intro ";
				   put (?c'_vars x);
				   put "; Intro.\n  "
			       end
		      else put " Intro."
		    | q in set ql
		    end;
		    put " Intros. Apply ";
		    put (if c'_paren then "(" else "");
		    put c'_s;
		    iterate
		      let val x' = if x inset splitBs
				       then ?splitinv (?splitBs x)
				   else x
		      in
			  put " "; put (?c'_vars x')
		      end
		    | x in list sort_vars c'_vars
		    end;
		    put (if c'_paren then ")" else "");
		    put "; Tauto.\nQed.\n";
		    rem
		end
	      | pproof (c as CL (_, _, _, _, P_SPLIT_DEF, ...)) =
		let val rem = gensym rem_name
		in
		    put "\nRemark "; put rem; put " : ";
		    pclause c; put ".\nProof.\n  Intro Z. Intros. Exists Z; Tauto.\nQed.\n";
		    rem
		end
	      | pproof (c as CL (_, _, _, _, P_SPLIT_SPLIT c', ...)) =
		let val c'_s = pproof c'
		    val rem = gensym rem_name
		in
		    put "\nRemark "; put rem; put " : ";
		    pclause c; put ".\nProof.\n  Elim ";
		    put c'_s; put ". Intro ";
		    put xname; put ". Intros. Exists "; put xname;
		    put ". Tauto.\nQed.\n";
		    rem
		end
	      | pproof c = raise CoqPproof
	with uproofs_of (UP (c, sigma, upl)) =
	     overwrite [uproofs_of up
		       | up in list upl] ++ {c => pproof c}
    in
	pproof
    end
