(* Coq printing functions for clauses.
   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_clause_h";
open "coq_auto_h";
open "coq_fun_h";
open "coq_term_h";
open "coq_kw_h";
open "sort_h";

fun coq_print_q (ver, f as |[put, ...]|, state_prefix, term_type, xname) =
    let val |[exists_prolog, exists_midlog, exists_epilog, ...]| =
	coq_keywords ver
    in
	fn q =>
	   (put exists_prolog; put xname; put ":"; put term_type;
	    put exists_midlog;
	    coq_print_block (ver, f, state_prefix) (" /\\ ", xname, q);
	    put exists_epilog)
    end

fun coq_print_head (ver, f as |[put, ...]|, bot_prefix,
		    fun_prefix, state_prefix, term_type, xname, vars) =
    let val pdterm1 = coq_print_term (f, fun_prefix, vars)
	val pq = coq_print_q (ver, f, state_prefix, term_type, xname)
	val cpname = coq_pred_name (ver, state_prefix, term_type)
	val (open_paren, close_paren) =
	    case ver of
		"7" => ("(", ")")
	      | _ => ("", "")
	fun phead (HVAR P) =
	    (put "("; put (cpname P);
	     put " "; pdterm1 (V 1); put ")")
	  | phead (HFUN (P, f, k, xs, t)) =
	    if false_fun_matches f
		then put (cpname P)
	    else if tuple_matches f
		then case xs of
			 nil => put (cpname P)
		       | _ => (put open_paren; put (cpname P);
			       iterate
				 (put " "; put (xname x)
			       | x in list xs
			       end;
			       put close_paren
			       )
	    else (put open_paren; put (cpname P);
		  put " "; pdterm1 t; put close_paren)
	  | phead (HQ q) = pq q
	  | phead (HBOT name) = (put bot_prefix; put name)
    in
	phead
    end;

fun coq_clause_var_names xname =
    let val f as |[convert, put, seek, ...]| = outstring xname
	val n = size xname
    in
	fn c =>
	   {i => (seek n;
		  print f (pack i);
		  convert ())
	   | i in set clause_vars c}
    end;

val sort_vars = sort (op <);

exception CoqPrintVarNotInEnv;

fun coq_print_clause (ver, f as |[put, ...]|, bot_prefix, fun_prefix, state_prefix, term_type, xname) =
    let val pq = coq_print_q (ver, f, state_prefix, term_type, xname)
	val pblock = coq_print_block (ver, f, state_prefix)
	val cvarnames = coq_clause_var_names xname
	val |[forall_prolog, forall_midlog, ...]| = coq_keywords ver
    in
	fn (c as CL (h, ql, al, Bs, ...)) =>
	   let val vars = cvarnames c
	       val pt = coq_print_term (f, fun_prefix, ?vars)
	   in
	       iterate
		 (put forall_prolog; put (?vars i); put ":"; put term_type;
		  put forall_midlog)
	       | i in list sort_vars vars
	       end;
	       iterate
		 (pq q; put " -> ")
	       | q in set ql
	       end;
	       iterate
		 (put "("; put P; put " "; pt t; put ") -> ")
	       | (P, t) in list al
	       end;
	       iterate
		 let val x = if i inset vars
				 then ?vars i
			     else raise CoqPrintVarNotInEnv
		 in
		     pblock (" -> ", x, B); put " -> "
		 end
	       | i => B in map Bs
	       end;
	       coq_print_head (ver, f, bot_prefix, fun_prefix, state_prefix,
			       term_type, xname, ?vars) h
	   end
    end;

fun coq_print_clause_def (ver, f as |[put, ...]|,
			  bot_prefix, state_prefix, term_type, xname) =
    let val pclause = coq_print_clause (ver, f, bot_prefix, state_prefix,
					term_type, xname)
	val cpname = coq_pred_name (ver, state_prefix, term_type)
	fun qname q =
	    let val g as |[convert, ...]| = outstring ""
	    in
		coq_print_q (g, state_prefix, term_type, xname);
		convert ()
	    end
	fun sort_clauses (nil, acc) = acc
	  | sort_clauses ((c as CL (h, ...)) :: rest, acc) =
	    let val hname = case h of
				HVAR P => (cpname P, true)
			      | HFUN (P, ...) => (cpname P, true)
			      | HQ q => (qname q, false)
			      | HBOT name => (bot_prefix ^ name, false)
	    in
		sort_clauses (rest,
			      if hname inset acc
				  then acc ++ {hname => c :: ?acc hname}
			      else acc ++ {hname => [c]})
	    end
	fun pclauses {} = ()
	  | pclauses sortedl =
	    let val delimr = ref "Inductive "
	    in
		iterate
		  (put (!delimr); delimr := "with ";
		   put hname; put " : ";
		   (if argp then (put term_type; put " -> ") else ());
	           put "Prop :=\n";
		   let val dlmr = ref "    "
		   in
		       iterate
			 (put (!dlmr); dlmr := "  | ";
			  put name; put " : "; pclause c; put "\n")
		       | c in list cl (* only print given clauses. *)
		       end
		   end
		   )
		| (hname, argp) => cl in map sortedl
		end;
		put ".\n"
	    end
    in
	fn l => pclauses (sort_clauses (l, {}))
    end;
