(* Coq printing functions for alternating tree automata, headers.
   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 "auto_h";

extern val coq_auto_clause_name : string * string -> (string * string * block list) -> string;
(* coq_auto_clause_name (coq_version, trans_name) (P, f, blkl)
 computes a name for an automaton clause P(f(x1,...,xk)) <= blkl.
 The idea is that you compute p = coq_auto_clause_name (coq_version, trans_name),
 then generate p (P, f, blkl) for each automaton clause you need; p is a memo function.
 *)

extern val coq_univ_clause_name : string * string -> string -> string;
(* coq_univ_clause_name (coq_version, trans_name) P
 computes a name for a universal clause P(x).
 Similar to coq_auto_clause_name.
 *)

extern val coq_print_Px : string * 'a outstream * string -> string * string -> unit;
(* coq_print_Px (coq_version, fd, state_prefix) (P, x)
 prints '(<state_prefix><P> <x>)'. *)

extern val coq_print_block : string * 'a outstream * string -> string * string * block -> unit;
(* coq_print_block (coq_version, fd, state_prefix) (delim, x, blk)
 prints block blk(x), prefixing predicates with state_prefix and separating each (P x)
 by delim.
 *)

extern val coq_print_blocks : string * 'a outstream * string -> string * string * block list -> unit;
(* coq_print_blocks (coq_version, fd, state_prefix) (delim, xname, blkl)
 where blkl = [B1, ..., Bk] prints B1(x1) ... B(xk) separated by delim;
 names x1, ..., xk are <xname>1, ..., <xname>k.
 *)

extern val coq_print_forall : string * 'a outstream -> string * string -> unit;
(* coq_print_forall (coq_version, fd) (xname, term_type)
 prints (<xname> : <term_type>) (version 7)
 or forall <xname> : <term_type>, (version 8)
 *)

extern val coq_print_vars : 'a outstream -> string * string * int -> unit;
(* coq_print_vars fd (delim, xname, k)
 prints x1, ..., xk separated by delim;
 names x1, ..., xk are <xname>1, ..., <xname>k.
 *)

extern val coq_print_foralls : string * 'a outstream -> string * string * int -> unit;
(* coq_print_foralls (coq_version, fd) (xname, term_type, k)
 prints '(x1,...,xk:<term_type>)' (version 7)
 or 'forall x1 ... xk : <term_type>, ' (version 8);
 names x1, ..., xk are <xname>1, ..., <xname>k.
 *)

extern val coq_print_f_vars : 'a outstream * string -> string * string * int -> unit;
(* coq_print_f_vars (fd, fun_prefix) (f, xname, k)
 prints '(<fun_prefix><f> x1 ... xk)';
 names x1, ..., xk are <xname>1, ..., <xname>k.
 (or nothing if f starts with #false, or 'x1 ... xk' if f
 starts with #.)
 *)

extern val coq_print_P_f_vars : string * 'a outstream * string * string
	   -> string * string * string * int -> unit;
(* coq_print_P_f_vars (coq_version, fd, fun_prefix, state_prefix) (P, f, xname, k)
 prints '(<state_prefix><P> (<fun_prefix><f> x1 ... xk))';
 names x1, ..., xk are <xname>1, ..., <xname>k.
 (or '(<state_prefix><P> x1 ... xk)' if f starts with
 #false or with #.)
 *)

datatype coq_auto_namer = CAN of
	 ((string * string * block list) -> string) * (string -> string);

extern val coq_print_auto :
	   (string * 'a outstream * string * string *
	    string * string * string * coq_auto_namer)
	   -> automaton * (string -m> int)
	   * string set * string set * string set -> unit;
(* coq_print_auto (coq_version, f, term_type, bot_prefix, fun_prefix,
                     state_prefix, xname, namer)
                  (auto, Psig, preds, truebots, falsebots)
 prints an inductive predicate definition defining the automaton auto.
 term_type is the type of terms.
 Each predicate will be printed with an additional state_prefix prefix.
 Each function will be printed with an additional fun_prefix prefix.
 Each botname is prefixed with state_prefix ^ bot_prefix.
 Quantified variables will be named xname or xname with a numeric suffix.
 namer is typically obtained by CAN (coq_auto_clause_name ..., coq_univ_clause_name ...).
 Each predicate in preds not occurring in auto will be defined using
 no constructor (hence be empty), just like botnames in falsebots.
 botnames in truebots will get one constructor (they are true).
 The intersection of truebots and falsebots should be empty.
 Psig maps each predicate to the arity under which it should be
 displayed; this is really only used for states P with no defining
 clause in auto.
 *)
