(* Coq term printing functions.
   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_term_h";
open "coq_fun_h";
open "sort_h";
open "rel_h";

fun coq_print_term (f as |[put, ...]|, fun_prefix, varname) =
    let val cfname = coq_fun_name fun_prefix
	fun pterm (V x) = put (varname x)
	  | pterm (f $ nil) = put (cfname f)
	  | pterm (f $ l) =
	    (put "("; put (cfname f);
	     iterate
	       (put " "; pterm t)
	     | t in list l
	     end;
	     put ")")
    in
	pterm
    end;

fun coq_print_atom (ver, f as |[put, ...]|, fun_prefix, state_prefix,
		    varname,  term_type) =
    let val pterm = coq_print_term (f, fun_prefix, varname)
	val cpname = coq_pred_name (ver, state_prefix, term_type)
	val (open_paren, close_paren) =
	    case ver of
		"7" => ("(", ")")
	      | _ => ("", "")
	fun cpatom0 (p $ nil) = put (cpname p)
	  | cpatom0 (p $ l) =
	    (put open_paren; put (cpname p);
	     iterate
	       (put " "; pterm t)
	     | t in list l
	     end;
	     put close_paren)
    in
	fn (a as p $ [t as f $ l]) =>
	    if false_fun_matches f
		then put (cpname p)
	    else if tuple_matches f
		then cpatom0 (p $ l)
	    else cpatom0 a
	 | a => cpatom0 a
    end;

val fsort = sort (op strless);

fun coq_print_sig (f as |[put, ...]|, fun_prefix, term_type) =
    let val cfname = coq_fun_name fun_prefix
	fun psig {} = ()
	  | psig smap =
	    let val delimr = ref "    "
		val ir = ref 0
	    in
		put "Inductive "; put term_type; put " : Set :=\n";
		iterate
		  (put (!delimr); delimr := "  | ";
		   put (cfname f); put " : ";
		   ir := 0;
		   while (!ir<k) do
		       (inc ir; put term_type; put " -> ");
		       put term_type;
		       put "\n")
		| f in list fsort smap
		  val k = ?smap f
		end;
		put "."
	    end
    in
	psig
    end;

fun coq_print_pred_sig (ver, f as |[put, ...]|, decl, term_type) =
    let val cpname = coq_pred_name (ver, "", term_type)
	fun psig predsig =
	    let val invsig = invrel predsig
		fun tt_k 0 = ()
		  | tt_k n = (put term_type; put " -> ";
			      tt_k (n-1))
	    in
		iterate
		  let val delimr = ref decl
		  in
		      iterate
			(put (!delimr); delimr := ",";
			 put " "; put (cpname P))
		      | P in set pred_k
		      end;
		      put " : ";
		      tt_k k;
		      put "Prop.\n"
		  end
		| k in list sort (op <) invsig
		  val pred_k = ?invsig k
		end
	    end
    in
	psig
    end;
