(* Coq printing functions for model-checking justifications, 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";
open "model_h";
open "coq_gclause_h";
open "coq_auto_h";

extern val coq_print_or_type : string * 'a outstream * string -> int -> string;
(*
 coq_print_or_type (coq_version, fd, or_prefix)
 returns a memofunction taking an integer n;
 it prints a definition for an inductive predicate '<or_prefix><n>'
 if none has been printed already, and returns '<or_prefix><n>'.
 This inductive predicate is an n-ary disjunction.
 Its constructors are '<or_prefix><n>_intro_<j>', 1<=j<=n.
 *)

extern val coq_print_inversion_P_f : string * 'a outstream * (int -> string)
	   * string * string * string * string * string * automaton * coq_auto_namer
	   -> string * string * int -> string;
(*
 coq_print_inversion_P_f (coq_version, fd, portype, fun_prefix, state_prefix,
                          rem_name, xname, term_type, auto, autonamer)
 returns a memofunction taking (P, f, k) as argument
 and printing (if not done already) a remark
 stating that (<state_prefix>P (<fun_prefix>f x1 ... xk)) is only true provided one
 of the n transitions labeled f leading to P in auto has been traversed.
 *)

extern val coq_print_ex_type : string * 'a outstream * string * string
	   -> int -> string;
(*
 coq_print_ex_type (coq_version, fd, ex_prefix, xname)
 returns a memofunction taking an integer n;
 it prints a definition for an inductive predicate '<ex_prefix><n>'
 if none has been printed already, and returns '<ex_prefix><n>'.
 This inductive predicate is an existential over n variables
 of type A given in argument to the predicate
 (the names of variables are prefixed with xname).
 Its only constructor is '<ex_prefix><n>_intro'.
 *)

(*
extern val coq_print_inversion_P : string * 'a outstream *
	   (int -> string) * (int -> string) *
	   string * string * string * string * string * automaton * coq_auto_namer
	   -> string -> string;
(*
 coq_print_inversion_P (coq_version, fd, portype, pextype,
                        fun_prefix, state_prefix, rem_name, xname, term_type,
                        auto, autonamer)
 returns a memofunction taking P as argument and printing
 (if not done already) a remark stating that if (P x) holds
 then x must be of one of the forms (f x1 ... xk) where f
 labels a transition to P in auto.
 x1 ... xk are quantified universally using a k-ary existential
 predicate computed by pextype (typically obtained through
 coq_print_ex_type);
 all possible forms are put in a multiway disjunction computed
 by portype (typically obtained through coq_print_or_type).
 *)
*)

extern val epsc_name : epsilon_gclause -> string;
(*
 computes a canonical name for an epsilon clause in argument.
 *)

extern val coq_print_justif : (automaton *
			       string * 'a outstream * string * string * string
			       * (''_var -> string) * string
			       * (''_var set -> ''_var list) * string
			       * (string -m> int)
			       * (int -> string)
			       * (string * string * int -> string)
			       (* * (string -> string) *)
			       * coq_auto_namer) ->
	   (epsilon_gclause -m> string)
	   * ''_var mc_justif
	   -> string;
(*
 coq_print_justif (auto, coq_version, f, fun_prefix, state_prefix,
                   rem_name, varname, xname, varsort, term_type, fsig,
                   portype, pinvPf, (*pinvP,*) autonamer) (history, j)
 prints Coq proof of history -> c,
 where c is the clause that j justifies.
 Returns rem, the name of the Remark proving history -> c.
 Had better be called with history={}.
 *)
