(* Coq term printing functions, headers.
   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 "term_h";

extern val coq_print_term : ('a outstream * string * (''var -> string)) -> ''var term -> unit;
(*
 coq_print_term (f, fun_prefix, varname) t
 prints t as a Coq term on file f;
 fun_prefix is prepended to each function name in t;
 varname is used to give a printable name to each ''var.
 *)

extern val coq_print_atom : (string * 'a outstream * string * string
			     * (''var -> string) * string)
	   -> ''var term -> unit;
(*
 coq_print_atom (coq_version, f, fun_prefix, state_prefix, varname, term_type) t
 prints t as a Coq atom on file f;
 state_prefix is prepended to the head predicate symbol;
 fun_prefix is prepended to each function name in t;
 varname is used to give a printable name to each ''var.
 *)

extern val fsort : (string -m> 'a) -> string list;
(* sorts a given signature in some ordering.
 The ordering is currently given by strless. *)

extern val coq_print_sig : ('a outstream * string * string) ->
	   (string -m> int) -> unit;
(*
 coq_print_sig (f, fun_prefix, term_type) sig
 prints the signature sig as a Coq datatype.
 Elements of the signature are listed in the order
 given by fsort.
 *)

extern val coq_print_pred_sig : (string * 'a outstream * string * string) ->
	   (string -m> int) -> unit;
(*
 coq_print_pred_sig (coq_version, f, decl, term_type) sig
 prints the predicate signature sig as a series of declarations.
 *)
