(* Coq printing functions for model-checking h1 clauses in Seidl form.
   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_seidl_h";
open "coq_gclause_h";
open "verbose_h";
open "gensym_h";
open "sort_h";

fun coq_seidl_mc (fd as |[put, ...]|, fun_prefix, state_prefix,
		  varname, varsort, term_type, rem_name, mc) =
    let val pgclause = coq_print_gclause (fd, fun_prefix, state_prefix, varname, varsort, term_type)
	val sort_vars = sort (op strless);
	fun varnames vars = [varname x | x in list sortvars 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 " Intros"; pvarnames vars; put ".")
	memofun jc (AJ_START _, c) =
		mc c
	      | jc (AJ_NON_HORN jl, c) =
		let val ir = ref 0
		    val n = len jl
		    val vars = gclause_vars c
		in
		    some
		      let val rem' = gensym rem_name
		      in
			  put "\nRemark "; put rem'; put " : ";
			  pgclause c;
			  put ". (* Non Horn case. *)\nProof.\n  "; intro_vars vars;
			  put "Intros.";
			  let val fin = (!ir = n)
			  in
			      while (dec ir; !ir <> 0) do
				  put " Right.";
				  if fin
				      then ()
				  else put " Left. Apply ";
				      if empty vars
					  then put rem
				      else (put "(";
					    put rem; pvarnames vars;
					    put ")")
			  end;
			  put "; Assumption.\nQed.\n";
			  rem'
		      end
		    | j_c in list jl
		    val SOME rem = (inc ir; jc j_c)
		    end
		end
	      | jc (AJ_RESOLVE (SEIDL (h, body, _), jl), c) =
		(let val autoc = GCLAUSE ([P $ [t] | (P, t) in list body],
					  case h of
					      SHVAR (P, x) => [P $ [V x]]
					    | SHFUN (P, f, xl) => [P $ [f $ [V x | x in list xl]]]
					    | SHBOT _ => nil)
		     val SOME autorem = mc autoc (* may raise Bind *)
		     val reml = [let val SOME remj = jc j_c (* may raise Bind *)
				 in
				     remj
				 end
				| j_c in list jl]
		     val rem' = gensym rem_name
		     val vars = gclause_vars c
		 in
		     put "\nRemark "; put rem'; put " : "; pgclause c;
		     put ". (* Resolve. *)\nProof.\n  "; intro_vars vars;
		     put " Intros. Apply "; put autorem; put ".\n";
		     iterate
		       (put "  Apply ";
			if empty vars'
			    then put remj
			else (put "("; put remj; pvarnames vars'; put ")");
			    put "; Assumption.\n")
		     || remj in list reml and
			(_, cj) in list jl
			val vars' = gclause_vars cj
		     end;
		     put "Qed.\n";
		     SOME rem'
		 end handle Bind => NONE)
	      | jc (AJ_CUT (jc1, jc2), c) =
		(let val SOME rem1 = jc jc1 (* may raise Bind *)
		     val SOME rem2 = jc jc2 (* may raise Bind *)
		     val rem' = gensym rem_name
		     val vars = gclause_vars c
		     val (_, c1 as GCLAUSE (_ :: rest1, _)) = jc1 (* may raise Bind but should not. *)
		     val vars1 = gclause_vars c1
		     val (_, c2) = jc2
		     val vars2 = gclause_vars c2
		 in
		     put "\nRemark "; put rem'; put " : "; pgclause c;
		     put ". (* Cut. *)\nProof.\n  "; intro_vars vars;
		     put " Intros. Apply ";
		     if empty vars1
			 then put rem1
		     else (put "("; put rem1; pvarnames vars1; put ")");
		     put ". Apply ";
		     if empty vars2
			 then put rem2
		     else (put "("; put rem2; pvarnames vars2; put "); Assumption.");
			 if null rest1
			     then ()
			 else (put "\n  ";
			       iterate
				 put " Assumption."
			       | _ in list rest1
			       end);
		     put "\nQed.\n";
		     SOME rem'
		 end handle Bind => NONE)
	      | jc (AJ_CUT_2 (jc1, jcl), c) =
		(let val SOME rem1 = jc jc1 (* may raise Bind *)
		     val reml = [let val SOME remj = jc jcj (* may raise Bind *)
				 in
				     remj
				 end
				| jcj in list jcl]
		     val rem' = gensym rem_name
		     val vars = gclause_vars c
		     val (_, c1 as GCLAUSE (_ :: rest1, _)) = jc1 (* may raise Bind but should not. *)
		     val vars1 = gclause_vars c1
		 in
		     put "\nRemark "; put rem'; put " : "; pgclause c;
		     put ". (* Cut2. *)\nProof.\n  "; intro_vars vars;
		     put " Intro H. Exact ("; put rem1;
		     iterate put " ?" | _ in set vars1 end;
		       iterate
			 (put " ("; put remj; 
			  iterate
			    put " ?"
			  | _ in set varsj
			  end;
			  put " H)")
		       || remj in list reml and (_, cj) in list jcl
		       val varsj = gclause_vars cj
		       end;
		       put ").\nQed.\n";
		       SOME rem'
		 end handle Bind => NONE)
	      | jc (AJ_FACTOR (x, x', j_c), c) =
		(case jc j_c of
		     SOME rem =>
		     let val rem' = gensym rem_name
			 val namex = varname x
			 val namex' = varname x'
			 val vars = gclause_vars c
		     in
			 put "\nRemark "; put rem'; put " : "; pgclause c;
			 put ". (* Factor. *)\nProof.\n  "; intro_vars vars;
			 put " Intros. Apply ("; put rem;
			 iterate
			   (put " ";
			    put (if y=namex' then namex else y))
			 | y in list varnames (vars U {x'})
			 end;
			 put "); Assumption.\nQed.\n";
			 SOME rem'
		     end
		   | _ => NONE)
    in
	jc
    end;
