(* Coq printing routines for alternating tree automata.
   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_auto_h";
open "coq_fun_h";
open "coq_kw_h";
open "gensym_h";

fun coq_auto_clause_name (ver, trans_name) =
    let val cpname = coq_pred_name (ver, "", "*")
	val cfname = coq_fun_name ""
	memofun auto_clause_name (P, f, blkl) =
		let val |[put, convert, ...]| = outstring trans_name
		in
		    put (cpname P);
		    if false_fun_or_tuple_matches f
			then ()
		    else (put "_"; put (cfname f));
		    put "_";
		    gensym (convert ())
		end
    in
	auto_clause_name
    end;

fun coq_univ_clause_name (ver, trans_name) =
    let val cpname = coq_pred_name (ver, trans_name, "*")
	memofun univ_clause_name P =
		gensym (cpname P ^ "_")
    in
	univ_clause_name
    end;

fun coq_print_Px (ver, |[put, ...]|, prefix) =
    let val cpname = coq_pred_name (ver, prefix, "*")
    in
	case ver of
	    "7" => (
		    fn (P, x) =>
		       (put "("; put (cpname P); put " "; put x; put ")")
		       )
	  | _ => (
		  fn (P, x) =>
		     (put (cpname P); put " "; put x)
		     )
    end;

fun coq_print_block (ver, f as |[put, ...]|, prefix) =
    let val pPx = coq_print_Px (ver, f, prefix)
    in
	fn (_, _, {}) => put "True"
	 | (delim, x, blk) =>
	   let val delimr = ref ""
	   in
	       iterate
		 (put (!delimr);
		  delimr := delim;
		  pPx (P, x))
	       | P in set blk
	       end
	   end
    end;

fun coq_print_blocks (ver, f as |[put, ...]|, prefix) =
    let val pblock = coq_print_block (ver, f, prefix)
    in
	fn (_, _, nil) => ()
	 | (delim, xname, blkl) =>
	   let val ir = ref 1
	       val delimr = ref ""
	       val g as |[tell, seek, convert, ...]| = outstring xname
	       val n = tell ()
	   in
	       iterate
		 (if empty blk
		      then ()
		  else (put (!delimr);
			delimr := delim;
			seek n; print g (pack (!ir));
			pblock (delim, convert (), blk));
		  inc ir)
	       | blk in list blkl
	       end
	   end
    end;

fun coq_print_forall (ver, f as |[put, ...]|) =
    let val |[forall_prolog, forall_midlog, ...]| = coq_keywords ver
    in
	fn (xname, term_type) =>
	   (put forall_prolog; put xname; put ":"; put term_type;
	    put forall_midlog)
    end;

fun coq_print_vars (f as |[put, ...]|) =
    let fun print_vars (delim, xname, k) =
	    let val ir = ref 0
		val dr = ref ""
	    in
		while (inc ir; !ir<=k) do
		    (put (!dr);
		     dr := delim;
		     put xname;
		     print f (pack (!ir)))
	    end
    in
	print_vars
    end;

fun coq_print_foralls (ver, f as |[put, ...]|) =
    let val pvars = coq_print_vars f
	val |[forall_prolog, forall_midlog, var_delim, ...]| =
	    coq_keywords ver
    in
	fn (xname, term_type, k) =>
	   if k>=1
	       then (put forall_prolog; pvars (var_delim, xname, k);
		     put ":"; put term_type; put forall_midlog)
	   else ()
    end;

fun coq_print_f_vars (fd as |[put, ...]|, fun_prefix) =
    let val pvars = coq_print_vars fd
	val cfname = coq_fun_name fun_prefix
    in
	fn (f, xname, k) =>
	   if false_fun_or_tuple_matches f (* andalso k=0 *)
	       then pvars (" ", xname, k)
	   else if k>=1
	       then (put "("; put (cfname f); put " ";
		     pvars (" ", xname, k);
		     put ")")
	   else put (cfname f)
    end;

fun coq_print_P_f_vars (ver, fd as |[put, ...]|, fun_prefix, state_prefix) =
    let val pfvars = coq_print_f_vars (fd, fun_prefix)
	val cpname = coq_pred_name (ver, state_prefix, "*")
    in
	case ver of
	    "7" => (
		    fn (P, f, xname, k) =>
		       (put "("; put (cpname P); put " ";
			pfvars (f, xname, k);
			put ")")
		       )
	  | _ => (
		  fn (P, f, xname, k) =>
		     (put (cpname P); put " ";
		      pfvars (f, xname, k))
		     )
    end;

fun coq_print_auto (ver, fd as |[put, ...]|, term_type, bot_prefix,
		    fun_prefix, state_prefix, xname, CAN (auto_namer, univ_namer)) =
    let val pPx = coq_print_Px (ver, fd, state_prefix)
	val cpname = coq_pred_name (ver, state_prefix, term_type)
	val pforall = coq_print_forall (ver, fd)
	val pforalls = coq_print_foralls (ver, fd)
	val pblocks = coq_print_blocks (ver, fd, state_prefix)
	val pPfvars = coq_print_P_f_vars (ver, fd, fun_prefix, state_prefix)
	fun put_term_types 0 = ()
	  | put_term_types k =
	    (put term_type; put " -> ";
	     put_term_types (k-1))
	fun print_auto (AUTO (auto, univ), Psig, preds, truebots, falsebots) =
	    let val delimr = ref "Inductive "
		fun p_arity P =
		    if P inset auto
			then case ?auto P of
				 {f => (blkls, k, vars)} =>
				 if false_fun_matches f
				     then 0
				 else if tuple_matches f
				     then k
				 else 1
			       | _ => 1
		    else if matches_false P
			then 0
		    else if P inset Psig
			then ?Psig P
		    else 1
		fun print_auto_1 P =
		    let val P' = cpname P
			val k = p_arity P
		    in
			put (!delimr);
			put P';
			put " : "; put_term_types k; put "Prop :=\n";
			delimr := "    ";
			if P inset univ
			    then (put (!delimr); delimr := "  | ";
				  put (univ_namer P); put " : ";
				  pforall (xname, term_type);
				  pPx (P, xname); put "\n")
			else ();
			    if P inset auto
				then
				    iterate
				      iterate
					(put (!delimr); delimr := "  | ";
					 put (auto_namer (P, f, blkl)); put " : ";
					 pforalls (xname, term_type, k);
					 pblocks (" -> ", xname, blkl);
					 if all empty blk | blk in list blkl end
					     then ()
					 else put " -> ";
					     pPfvars (P, f, xname, k);
					     put "\n")
				      | blkl in set blkls
				      end
				    | f => (blkls, k, vars) in map ?auto P
				    end
			    else ();
				delimr := "with "
		    end
	    in
		iterate
		  print_auto_1 P
		| P in set univ
		end;
		iterate
		  print_auto_1 P
		| P in set univ <-| auto
		end;
		iterate
		  (put (!delimr); delimr := "with ";
		   put (cpname P); put " : "; put_term_types k; put "Prop :=\n")
		| P in set univ <-| (auto <-| preds)
		  val k = p_arity P
		end;
		iterate
		  (put (!delimr); delimr := "with ";
		   put state_prefix; put bot_prefix; put botname; put " : Prop :=\n    ";
		   put botname; put "_intro : "; put state_prefix; put bot_prefix; put botname; put "\n")
		| botname in set truebots
		end;
		iterate
		  (put (!delimr); delimr := "with ";
		   put state_prefix; put bot_prefix; put botname; put " : Prop :=\n")
		| botname in set falsebots
		end;
		put ".\n"
	    end
    in
	print_auto
    end;
