(* h1 model-checker main loop.
   Copyright (C) 2003,2005,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 "tptp_h";
open "plauto_h";
open "proof_h";
open "yyerror_h";
open "monadic_h";
open "gensym_h";
open "verbose_h";
open "model_h";
open "coq_fun_h";
open "coq_term_h";
open "coq_auto_h";
open "coq_model_h";
open "coq_kw_h";
open "natded_h";
open "pfcprinttree_h";
open "pfcprintcoq_h";
open "sort_h";
open "rel_h";
open "topsort_h";
open "scc_h";

val version = "1.4 - Dec 13, 2008";
    (* "1.3 - Feb 15, 2008"; *)
    (* "1.2 - Feb 11, 2008"; *)
    (* "1.1 - Jan 24, 2008"; *)
    (* "1.0"; date inconnue *)

val print_type = ref "tree";
val coq_version = ref "8";
val create_axioms = ref false;
val exact_sig = ref false;

val Xsort = sort (op strless);

datatype 'a llist = NIL
       | CONS of 'a * 'a llist promise;

fun ll_enum_set (f, {}) = NIL
  | ll_enum_set (f, {x} U rest) =
    case f x of
        SOME y => CONS (y, delay (ll_enum_set (f, rest)))
      | _ => ll_enum_set (f, rest);

fun iter_ll (f, NIL) = ()
  | iter_ll (f, CONS (y, rest)) =
    (f y;
     iter_ll (f, force rest));

fun justif_orandl (MC_DISTR_POS (c, orandl, ...)) = orandl
  | justif_orandl (MC_SUBSUMED_SUPER (c, orandl, ...)) = orandl
  | justif_orandl (MC_CUT_HISTORY (_, j)) = justif_orandl j
  | justif_orandl j = nil;

fun print_case (fd as |[put, ...]|) =
    let val prt = print fd
    in
	fn i => (prt (pack (i:int));
		 put ".")
    end;
	    (*
			       put (if i<10
					then chr (48 + i)
				    else chr (87 + i));
			       put "."
	     *)

fun mc_justif_possible (MC_ELIM_NEG (_, _, _, _, jl)) =
    exists
      mc_justif_possible j
    | j in list jl
    end
  | mc_justif_possible (MC_ELIM_EPSILON_NEG (_, _, qjl)) =
    exists
      mc_justif_possible j
    | (_, j) in list qjl
    end
  | mc_justif_possible _ = true;

exception McPrintTree;
exception POrl;

fun mc_print_tree (fd as |[put, ...]|, AUTO (auto, univ)) =
    let val pt = print_term (fd, identity)
	val pa = print_atom (fd, identity)
	val pgc = print_gclause_pl (fd, identity)
	val pa_clauses = print_auto_clauses (fd, "X", "")
	fun pspaces 0 = ()
	  | pspaces n = (put " "; pspaces (n-1))
	fun spaces n =
	    let val |[put, convert, ...]| = outstring ""
		val ir = ref n
	    in
		while !ir<>0 do
		    (dec ir;
		     put " ");
		    convert ()
	    end
	fun gclause_from_epsc (neg, pos) =
	    GCLAUSE ([P $ [V "X1"] | P in set neg],
		       [P $ [V "X1"] | P in set pos])
	fun psigma sigma =
	    let val f as |[convert, seek, truncate, ...]| = outstring "X"
		val sigma' = {X => t
			     | k => t in map sigma
			       val X = (seek 1; truncate ();
					print f (pack (k:int));
					convert ())
				   such that t<>V X}
		val delimr = ref "{"
	    in
		if empty sigma'
		    then ()
		else (put " ";
		      iterate
			(put (!delimr); delimr := ",";
			 put X; put "="; pt t)
		      | X => t in map sigma'
		      end;
		      put "}")
	    end
	val mc_pr_done = table ()
	val mc_pr_get = t_get mc_pr_done
	val mc_pr_put = t_put mc_pr_done
	fun mc_pr (j, dewey) =
	    case mc_pr_get j of
		SOME dewey' => (put dewey; put " "; pgc (justif_gclause j);
				put ": see "; put dewey';
				put "\n")
	      | NONE => (if justif_has_gclause j
			     then mc_pr_put (j, dewey)
			 else ();
			 do_mc_pr (j, dewey))
	and do_mc_pr (MC_TAUTO (c, i), dewey) =
	    (put dewey; put " "; pgc c;
	     put " is a tautology.\n")
	  | do_mc_pr (MC_CUT_HISTORY (h, i), dewey) =
	    (put dewey; put " "; pgc (justif_gclause i);
	     put "\n"; pspaces (size dewey+2);
	     (case h of
		  {} => put "Without any induction hypothesis:\n"
		| {epsc} => (put "Using only the induction hypothesis ";
			     pgc (gclause_from_epsc epsc);
			     put ":\n")
		| _ => (put "Using only the induction hypotheses";
			let val delimr = ref ""
			in
			    iterate
			      (put (!delimr); delimr := ",";
			       put "\n"; pspaces (size dewey+2);
			       pgc (gclause_from_epsc epsc))
			    | epsc in set h
			    end
			end;
			put ":\n"));
	     mc_pr (i, dewey ^ "1."))
	  | do_mc_pr (MC_NORMALIZE (c, sigma, i), dewey) =
	    (put dewey; put " "; pgc c;
	     put "\n"; pspaces (size dewey+2);
	     put "Equivalent to:\n";
	     mc_pr (i, dewey ^ "1."))
	  | do_mc_pr (MC_SUBSUMED_UNIV (c, P, i), dewey) =
	    (put dewey; put " "; pgc c;
	     put "\n"; pspaces (size dewey+2);
	     put "Obvious from the universal clause ";
	     put P;
	     put "(X) in the model.\n")
(*
	  | do_mc_pr (MC_SUBSUMED_AUTO (c, P, f, k, sigma, blkl, i), dewey) =
	    (put dewey; put " "; pgc c;
	     put "\n"; pspaces (size dewey+2);
	     put "Obvious from the automaton clause ";
	     pa_clauses (P, f, {blkl}, k);
	     psigma sigma;
	     put ".\n")
*)
	  | do_mc_pr (MC_SUBSUMED_HISTORY (c, epsc, t), dewey) =
	    (put dewey; put " "; pgc c;
	     put "\n"; pspaces (size dewey+2);
	     put "By induction hypothesis ";
	     pgc (gclause_from_epsc epsc);
 	     put ".\n")
	  | do_mc_pr (MC_SUBSUMED_EPSC (c, t, i), dewey) =
	    (put dewey; put " "; pgc c;
	     put "\n"; pspaces (size dewey+2);
	     put "Special case of:\n";
	     mc_pr (i, dewey ^ "1."))
	  | do_mc_pr (MC_ELIM_UNIV_NEG (c as GCLAUSE (neg, _), P, i, j), dewey) =
	    (put dewey; put " "; pgc c;
	     put "\n"; pspaces (size dewey+2);
	     put "Eliminate "; put P; put " "; pt (neg nth i);
	     put ", which holds since "; put P; put "(X) is a universal clause.\n";
	     mc_pr (j, dewey ^ "1."))
	  | do_mc_pr (MC_ELIM_NEG (c as GCLAUSE (neg, _),
				a as P $ [f $ _], k, sigma, jl), dewey) =
	    let val sp = spaces (size dewey+2)
		val fmap = if P inset auto then ?auto P else {}
		val (blkls, k, _) = if f inset fmap then ?fmap f else ({}, 0, {})
		val elems_neg = elems neg \ {a}
		val ir = ref 0
		val resolved_negs = {blkl => elems_neg U
				     (ir := 0;
				      union {let val til = [(inc ir;
							     ?sigma (!ir))]
					     in
						 {P $ til
						 | P in set blk}
					     end
					    | blk in list blkl})
				    | blkl in set blkls}
		val justifs = {elems neg' => j
			      | j in list jl
				  val GCLAUSE (neg', _) = justif_gclause j
				      such that mc_justif_possible j
				      }
		val pruned_blkls = justifs O resolved_negs
	    in
		put dewey; put " "; pgc c;
		put "\n"; put sp;
		case pruned_blkls of
		    {} => (pa a; put " is impossible.\n")
		  | {blkl => j} =>
			   (pa a; put " must be by ";
			    print_auto_clauses (fd, "X", "") (P, f, {blkl}, k);
			    put ".\n";
			    mc_pr (j, dewey ^ "1."))
		  | _ =>
			   (put "Examine all ways of building "; pa a;
			    put " in the body.";
			    put "\n"; put sp; put "The ";
			    print fd (pack (card pruned_blkls));
			    put " possibilities are:\n"; put sp;
			    print_auto_clauses (fd, "X", ".\n" ^ sp) (P, f,
								      dom pruned_blkls, k);
			    put ".\n";
			    let val ir = ref 0
				val f as |[put, convert, tell, seek, truncate,
					   ...]|
				    = outstring dewey
				val n = tell ()
			    in
				iterate
				  (inc ir; seek n; truncate ();
				   print_case f (!ir);
				   mc_pr (j, convert ()))
				| blkl => j in map pruned_blkls
				end
			    end
			    )
	    end
	  | do_mc_pr (MC_ELIM_EPSILON_NEG (c, a as P $ [t], qjl), dewey) =
	    let val sp = spaces (size dewey+2)
		    
	    in
		put dewey; put " "; pgc c;
		put "\n"; put sp;
		case qjl of
		    nil => (pa a; put " is impossible.\n")
		  | _ => (put "for all X, in particular X=";
			  pt t; put ", ";
			  pa (P $ [V "X"]); put " is equivalent to ";
			  let val delimr = ref ""
			  in
			      iterate
				(put (!delimr);
				 delimr := " \\/ ";
				 pa (q $ [V "X"]))
			      | (q, _) in list qjl
			      end
			  end;
			  put ".\n";
			  let val ir = ref 0
			      val f as |[put, convert, tell, seek, truncate,
					 ...]|
				  = outstring dewey
			      val n = tell ()
			  in
			      iterate
				(inc ir; seek n; truncate ();
				 print_case f (!ir);
				 mc_pr (j, convert ()))
			      | (_, j) in list qjl
			      end
			  end
			  )
	    end
	  | do_mc_pr (MC_DEDUCE_POS (c, a as P $ [f $ l], i, blkls, j), dewey) =
	    let val sp = spaces (size dewey+2)
		fun p_andl nil = put "true"
		  | p_andl [a] = pa a
		  | p_andl (a::al) = (pa a; put " & "; p_andl al)
		fun p_orandl nil = put "false"
		  | p_orandl [andl] = p_andl andl
		  | p_orandl (andl::rest) =
		    (p_andl andl; put "\n"; put sp; put "  or "; p_orandl rest)
	    in
		put dewey; put " "; pgc c;
		put "\n"; put sp;
		(case blkls of
		     {} => (put "There is no way to infer "; pa a;
			    put ", so the body must be false.\n";
			    mc_pr (j, dewey))
		   | {blkl} =>
		     (put "Infer "; pa a;
		      put " using ";
		      print_auto_clauses (fd, "X", "") (P, f, blkls, len l);
		      put ".\n";
		      mc_pr (j, dewey))
		   | _ =>
		     (put "Examine the following ways of inferring "; pa a;
		      put ".\n"; put sp;
		      print_auto_clauses (fd, "X", ".\n" ^ sp) (P, f, blkls, len l);
		      put ".\n";
		      put sp; put "So "; pa a; put " will be implied by ";
		      p_orandl (justif_orandl j); put ".\n";
		      mc_pr (j, dewey)
		      )
		     )
	    end
	  | do_mc_pr (MC_SUBSUMED (c, j), dewey) =
	    (put dewey; put " "; pgc c;
	     put "\n"; pspaces (size dewey+2);
	     put "Because the following simpler clause holds:\n";
	     mc_pr (j, dewey ^ "1."))
	  | do_mc_pr (MC_SPLIT (c, j), dewey) =
	    (put dewey; put " "; pgc c;
	     put "\n"; pspaces (size dewey+2);
	     put "This is implied by:\n";
	     mc_pr (j, dewey ^ "1."))
	  | do_mc_pr (MC_EXPLICIT_UNIV (x, qs, info), dewey) =
	    (put dewey; put " "; pgc (gclause_from_epsc ({}, qs));
	     put "\n"; pspaces (size dewey+2);
	     put "By an easy induction on ";
	     put x; put ".\n")
	  | do_mc_pr (MC_VS (x,q,q',sm), dewey) =
	    (put dewey; put " "; pgc (gclause_from_epsc ({q,q'}, {}));
	     put "\n"; pspaces (size dewey+2);
	     put "By inspection, no ground term is recognized both by ";
	     put q; put " and "; put q'; put ".\n")
(* OBSOLETE
	  | do_mc_pr (MC_VS_NEG1 (c, t, vcj, sm, rho), dewey) =
	    (put dewey; put " "; pgc c;
	     put "\n"; pspaces (size dewey+2);
	     put "By inspection, using a suitable finite model.\n")
*)
	  | do_mc_pr (MC_CUT (c, j, jal), dewey) =
	    let val ir = ref 0
		val f as |[put=p, convert, tell, seek, truncate, ...]| =
		    outstring dewey
		val n = tell ()
	    in
		put dewey; put " "; pgc c;
		put "\n"; pspaces (size dewey+2);
		put "Do a case analysis on ";
		pgc (GCLAUSE (nil, [ai | (_, ai) in list jal]));
		put ", because:\n";
		mc_pr (j, dewey ^ "0.");
		iterate
		  (inc ir; seek n; truncate ();
		   print_case f (!ir);
		   mc_pr (ji, convert ()))
		| (ji, ai) in list jal
		end
	    end
	  | do_mc_pr (MC_INDUCT (x, epsc, optP, jl), dewey) =
	     (put dewey; put " "; pgc (gclause_from_epsc epsc);
	      put "\n"; pspaces (size dewey+2);
	      put "By induction on "; put x;
	      (case optP of
		   SOME P => (put " satisfying "; put P)
		 | NONE => ());
	      case jl of
		  nil => put ": none.\n"
		| [(f, ...)] => if invisible_fun f
				    then put ", must be a tuple.\n"
				else (put ", must start with ";
				      put f;
				      put ".\n")
		| _ => (put ", "; put x;
			put " must start with ";
			put (#1 (hd jl));
			let val jlr = ref (tl jl)
			in
			    while not (null (tl (!jlr))) do
				(put ", ";
				 put (#1 (hd (!jlr)));
				 jlr := tl (!jlr));
				put " or ";
				put (#1 (hd (!jlr)));
				put ".\n"
			end);
	      let val ir = ref 0
		  val f as |[put, convert, tell, seek, truncate,
			      ...]|
		      = outstring dewey
		  val n = tell ()
	      in
		  iterate
		    (inc ir; seek n; truncate ();
		     print_case f (!ir);
		     mc_pr (j, convert ())
		     )
		  | (fi, ki, j) in list jl
		  end
	      end)
	  | do_mc_pr (MC_DISTR_POS (c, [nil], jl), dewey) =
	    () (* true: ... obvious, don't print anything. *)
	  | do_mc_pr (MC_DISTR_POS (c, [andl], jl), dewey) =
	    (* conjunction, do not say "By distributing disjunctions over conjunctions". *)
	    let val ir = ref 0
		val f as |[convert, tell, seek, truncate,
			    ...]|
		    = outstring dewey
		val n = tell ()
	    in
		iterate
		  (inc ir; seek n; truncate ();
		   print_case f (!ir);
		   mc_pr (j, convert ())
		   )
		| j in list jl
		end
	    end
	  | do_mc_pr (MC_DISTR_POS (c, orandl, jl), dewey) =
	    let val ir = ref 0
		val f as |[convert, tell, seek, truncate,
			    ...]|
		    = outstring dewey
		val n = tell ()
		fun p_orl nil = put "false"
		  | p_orl [[a]] = pa a
		  | p_orl ([a]::al) = (pa a; put " \\/ "; p_orl al)
		  | p_orl (_ :: al) = p_orl al
	    in
		pspaces (size dewey+2);
		if exists true | [_, _, ...] in list orandl end
		    then (pretty fd (pack orandl);
			  put "By distributing disjunctions over conjunctions:\n")
		else (put "It remains to prove ";
		      p_orl orandl;
		      put ".\n");
		    iterate
		      (inc ir; seek n; truncate ();
		       print_case f (!ir);
		       mc_pr (j, convert ())
		       )
		    | j in list jl
		    end
	    end
	  | do_mc_pr (MC_SUBSUMED_SUPER (c, orandl, j), dewey) =
	    (pspaces (size dewey+2);
	     put "By selecting one of the disjuncts:\n";
	     mc_pr (j, dewey ^ "1."))
	  | do_mc_pr arg = raise McPrintTree
    in
	fn (j, dewey) => (mc_pr (j, dewey))
    end;

fun definitions_dependencies (definitions : string gclause set) : string -m> int =
    let val g = union_rel {{P => {Q | Q $ _ in list neg}}
			  | GCLAUSE (neg, [P $ _]) in set definitions}
	val g' = g ++ {"" => dom g}
	val deps = revtopsort (g', "")
    in
	{""} <-| deps
    end;

exception IndexDefinitions;

fun index_definitions (definitions : string gclause set,
		       deps : string -m> int) : string -m> string gclause set =
    union_rel {{P => {c}}
	      | c as GCLAUSE (neg, [P $ _]) in set definitions
		  val Pn = ?deps P
		      such that
			  all
			    ?deps Q < Pn
			  | Q $ _ in list neg
			  end}
    handle MapGet => raise IndexDefinitions;

fun expand_definitions (id : string -m> string gclause set) =
    let fun newdef (c as GCLAUSE (neg, pos)) =
	    let val vars = gclause_vars c
		val ren = {x => V (gensym "_X")
			  | x in set vars}
		val rename = tsubst ren
	    in
		GCLAUSE ([rename t | t in list neg],
			   [rename t | t in list pos])
	    end
	fun occurs (x, sigma) =
	    let fun occ (V y) =
		    if y inset sigma
			then occ (?sigma y)
		    else x=y
		  | occ (_ $ l) =
		    exists
		      occ t
		    | t in list l
		    end
	    in
		occ
	    end
	fun subst sigma =
	    let fun subs (V y) =
		    if y inset sigma
			then subs (?sigma y)
		    else V y
		  | subs (f $ l) =
		    f $ [subs t | t in list l]
	    in
		subs
	    end
	fun unify (t, t', sigma) =
	    if t=t'
		then SOME sigma
	    else case t of
		     f $ l =>
		     (case t' of
			  f' $ l' =>
			  if f=f'
			      then unify_list (l, l', sigma)
			  else NONE
			| V x' =>
			  if x' inset sigma
			      then unify (t, ?sigma x', sigma)
			  else if occurs (x', sigma) t
			      then NONE
			  else SOME (sigma ++ {x' => t})
			  )
		   | V x =>
		     if x inset sigma
			 then unify (?sigma x, t', sigma)
		     else if occurs (x, sigma) t'
			 then NONE
		     else SOME (sigma ++ {x => t'})
	and unify_list (nil, nil, sigma) = SOME sigma
	  | unify_list (t::rest, t' :: rest', sigma) =
	    (case unify (t, t', sigma) of
		 SOME sigma' => unify_list (rest, rest', sigma')
	       | _ => NONE)
	  | unify_list _ = NONE
	fun dexpand ({}, acc, sigma) =
	    {(acc, sigma)}
	  | dexpand ({a as (P $ l)} U rest, acc, sigma) =
	    if P inset id
		then union {dexpand (rest U elems neg', acc, sigma')
			   | c in set ?id P
			       val c' as GCLAUSE (neg', [_ $ l']) = newdef c
			       val SOME sigma' = unify_list (l, l', sigma)}
	    else dexpand (rest, acc U {a}, sigma)
	fun candef (c as GCLAUSE (neg, pos)) =
	    let val ir = ref 0
		val vars = gclause_vars c
		val f as |[put, convert, tell, seek, truncate, ...]| = outstring "X"
		val n = tell ()
		val ren = {x => V (seek n; truncate ();
				   inc ir; print f (pack (!ir));
				   convert ())
			  | x in set vars}
		val rename = tsubst ren
	    in
		GCLAUSE ([rename t | t in list neg],
			   [rename t | t in list pos])
	    end
	fun gclause_expand (GCLAUSE (neg, pos)) =
	    {candef (GCLAUSE ([subs t | t in set neg'],
				[subs t | t in list pos]))
	    | (neg', sigma) in set dexpand (elems neg, {}, {})
		val subs = subst sigma}
    in
	|[ gclause_expand = gclause_expand,
	   gclauses_expand = fn clauses => union {gclause_expand c
						 | c in set clauses},
	   blkls_expand = (fn (P, f, blkls) =>
			      union {gclause_expand (GCLAUSE (neg, [h]))
				    | blkl in set blkls
					val ir = ref 0
					val fd as |[put, convert, tell, seek, truncate, ...]|
					    = outstring "X"
					val n = tell ()
					val xl = [(seek n; truncate ();
						   inc ir; print fd (pack (!ir));
						   convert ())
						 | _ in list blkl]
					val h = P $ [f $ [V x | x in list xl]]
					val neg = append [[P $ [V x]
							  | P in set blk]
							 || blk in list blkl and
							    x in list xl]
					    })
	   ]|
    end;

fun coq_print_fsig_inclusion (ver, fd as |[put, ...]|,
			      fun_prefix0, fun_prefix, term_type0, term_type,
			      fsig0) =
    (* Assume fsig0 is a sub-signature of fsig. *)
    let val |[rec_def, plain_def, param_prolog, param_epilog,
	      case_prolog, case_of, case_midlog, case_epilog, ...]|
	    = coq_keywords ver
	val evalfun = "eval_" ^ term_type ^ "_of_" ^ term_type0
	val cfname0 = coq_fun_name fun_prefix0
	val cfname = coq_fun_name fun_prefix
	val ir = ref 0
	val delimr = ref "    "
	val rec_p = exists k<>0
		    | f => k in map fsig0
		    end
    in
	put (if rec_p then rec_def else plain_def); put evalfun;
	put " "; put param_prolog;
	put "t : "; put term_type0;
	put param_epilog;
	(case ver of
	     "7" => () (* nothing to do here *)
	   | _ => if rec_p (* Coq v8 is pesky when distinguishing
			    recursive from non-recursive functions. *)
		      then put " {struct t}"
		  else ());
	put " : "; put term_type;
	put " :=\n  ";
	put case_prolog; put "t "; put case_of; put "\n";
	iterate
	  (put (!delimr); delimr := "  | ";
	   if k=0
	       then put (cfname0 f)
	   else (put "("; put (cfname0 f);
		 ir := 0;
		 while !ir<k do
		     (inc ir; put " x";
		      print fd (pack (!ir)));
		 put ")");
	       put case_midlog;
	       if k=0
		   then put (cfname f)
	       else (put "("; put (cfname f);
		     ir := 0;
		     while !ir<k do
			 (inc ir; put " ("; put evalfun;
			  put " x"; print fd (pack (!ir));
			  put ")");
		     put ")");
		   put "\n")
	| f => k in map fsig0
	end;
	put "  "; put case_epilog; put ".\n";
	evalfun
    end;

fun coq_print_source (ver, fd as |[put, ...]|,
		      clause_prefix0, fun_prefix0, state_prefix0,
		      varname, varsort, term_type) =
    let val cpgc = coq_print_gclause (ver, fd, fun_prefix0, state_prefix0,
				      varname, varsort, term_type)
	val cpname = coq_pred_name (ver, state_prefix0, term_type)
	fun cpsource source =
	    let val Ps =
		    union_rel {{P => {name_c}}
			      | name_c as (name, GCLAUSE (_, pos))
				 in list source
				  val SOME P =
				      (case pos of
					   nil => (#put stderr "Warning: source clause [";
						   #put stderr name;
						   #put stderr "] has empty head, ignored \
						    \(use '#false(<name>)' as head \
						    \instead).\n";
						   #flush stderr ();
						   NONE)
					 | [P $ _] => SOME P
					 | _ => (#put stderr "Warning: source clause [";
						 #put stderr name;
						 #put stderr "] is not Horn, ignored \
						  \(unimplemented).\n";
						 #flush stderr ();
						 NONE))
				      }
		val Pl = Xsort Ps
		val delimr = ref "Inductive "
	    in
		iterate
		  (put (!delimr); delimr := "\nwith ";
		   put (cpname P); put " : ";
		   iterate
		     (put term_type; put " -> ")
		   | _ in list args
		   end;
		   put "Prop :=\n";
		   let val dr = ref "    "
		   in
		       iterate
			 (put (!dr); dr := "  | ";
			  put clause_prefix0; put name; put " : ";
			  cpgc c; put "\n"
			  )
		       | name in list names
		       val c = ?constrs name
		       end
		   end
		   )
		| P in list Pl
		val cs as {(_, GCLAUSE (_, [_ $ l0])), ...} = ?Ps P
		val constrs = {name => c
			      | (name, c) in set cs}
		val names = Xsort constrs
		val args = case l0 of
			       [f $ l] => if false_fun_matches f orelse tuple_matches f
					      then l (* revert effect of make_monadic *)
					  else l0
			     | _ => l0
		end;
		put ".\n"
	    end
    in
	cpsource
    end;

fun coq_print_source_eval (ver, fd as |[put, ...]|,
			   clause_prefix0, fun_prefix0, state_prefix0,
			   clause_prefix, fun_prefix, state_prefix,
			   varname, evalfun, term_type0, term_type) =
    let val |[rec_def, plain_def, param_prolog, param_delim, param_epilog,
	      case_prolog, case_delim,
	      case_of, case_midlog, case_epilog,
	      ...]|
	    = coq_keywords ver
	val cpname0 = coq_pred_name (ver, state_prefix0, term_type0)
	val cpname = coq_pred_name (ver, state_prefix, term_type)
	val cpatom0 = coq_print_atom (ver, fd, fun_prefix0, state_prefix0, varname, term_type0)
	val cpterm0 = coq_print_term (fd, fun_prefix0, varname)
	fun coq_trans_fun P = "translate_" ^ (cpname P) ^ "_from_" ^ (cpname0 P)
	fun cpdeps source =
	    let val G = union_rel {{P => {Q | Q $ _ in list neg}}
				  | (_, GCLAUSE (neg, [P $ _])) in list source
				      such that not (null neg)}
	    in
		G Urel {"" => dom G U union {succ | _ => succ in map G}}
	    end
	fun cpsource_eval (source, cc, recp) =
	    (* print translation for source clauses,
	     provided they define predicates in the set cc;
	     recp=true iff definition should be recursive. *)
	    let val Ps = union_rel {{P => {name_c}}
				   | name_c as (_, GCLAUSE (_, [P $ _])) in list source
				      such that P inset cc}
		val Pl = Xsort Ps
		val delimr = ref (if recp then rec_def else plain_def);
		val ir = ref 0
		val cpatom = coq_print_atom (ver, fd, fun_prefix, state_prefix,
					     if evalfun=""
						 then varname
					     else
						 fn x => let val f as |[put, convert, ...]|
								 = outstring "("
							 in
							     put evalfun;
							     put " ";
							     put (varname x);
							     put ")";
							     convert ()
							 end,
							 term_type)
	    in
		iterate
		  (put (!delimr); delimr := "\nwith ";
		   put (coq_trans_fun P); put " "; put param_prolog;
		   iterate
		     (put (varname x); put " : "; put term_type0;
		      put param_delim)
		   | x in list xl
		   end;
		   put "pi : "; cpatom0 head0;
		   put param_epilog;
		   (case ver of
			"7" => () (* that's all *)
		      | _ => if recp then put " {struct pi}" else ());
		   put " : "; 
		   cpatom head;
		   put " :=\n  ";
		   (case ver of
			"7" => (* put dependency information here. *)
			(put "<[";
			 iterate
			   (put (varname x); put " : ";
			    put term_type0; put "; ")
			 | x in list xl
			 end;
			 put "pi : "; cpatom0 head0;
			 put "] ";
			 cpatom head;
			 put ">")
		      | _ => ());
		   put case_prolog; put "pi ";
		   (case ver of
			"7" => ()
		      | _ => (* in version 8, put dependency info here. *)
			(* However, is there is no actual dependency, refrain
			 from doing so: Coq v8 would complain... *)
			if null xl
			    then ()
			else (put "as pi in ";
			      cpatom0 head0;
			      put " return "; cpatom head
			      )
			);
		   put case_of; put "\n";
		   let val dr = ref "    "
		       val jr = ref 0
		   in
		       iterate
			 (put (!dr); dr := "  | ";
			  put "("; put clause_prefix0; put name;
			  iterate
			    (put " "; put x)
			  | x in list varl
			  end;
			  jr := 0;
			  iterate
			    (inc jr; put " H"; print fd (pack (!jr)))
			  | _ in list neg
			  end;
			  put ")"; put case_midlog; put "\n      (";
			  put clause_prefix; put name;
			  if evalfun=""
			      then iterate
				  (put " "; put x)
				   | x in list varl
				   end
			  else
			      iterate
				(put "\n        ("; put evalfun;
				 put " "; put x; put ")")
			      | x in list varl
			      end;
			  jr := 0;
			  iterate
			    (inc jr; put "\n        ("; put (coq_trans_fun Q);
			     iterate
			       (put " ";
				cpterm0 arg)
			     | arg in list args
			     end;
			     put " H"; print fd (pack (!jr)); put ")")
			  | Q $ args in list neg
			  end;
			  put ")\n"
			  )
		       | name in list names
			 val c as GCLAUSE (neg, [_ $ l]) = ?constrs name
			 val vars = gclause_vars c
			 val varl = [varname x | x in list Xsort vars]
			     (* Xsort {varname x | x in set vars} *)
		       end
		   end;
		   put "  "; put case_epilog; put "\n"
		   )
		| P in list Pl
		val cs as {(_ , GCLAUSE (_, [_ $ l0])), ...} = ?Ps P
		val xl = let val f as |[put, convert, seek, tell, truncate, ...]| = outstring "x"
			     val n = tell ()
			     val ir = ref 0
			 in
			     [(seek n; truncate (); inc ir; print f (pack (!ir));
			       convert ())
			     | _ in list l0]
			 end
		val vxl = [V x | x in list xl]
		val head0 = P $ vxl
		val head = make_monadic head0
		val constrs = {name => c
			      | (name, c) in set cs}
		val names = Xsort constrs
		end;
		put ".\n"
	    end
    in
	fn source =>
	   let val G = cpdeps source
	       val (_, ccs) = scc (G, "")
	       val (condensed, root) = scc_condense (G, "", ccs)
	       val numbering = {root} <-| revtopsort (condensed, root)
	       val nodesl =
		   sort (fn (i,j) => ?numbering i < ?numbering j) numbering
	   in
(*
#put stderr "G = ";
pretty stderr (pack G);
#put stderr "numl = ";
pretty stderr (pack nodesl);
#put stderr "ccs = ";
pretty stderr (pack ccs);
#flush stderr ();
*)
	       iterate
		 cpsource_eval (source, cc, recp)
	       | node in list nodesl
	       val cc = ?ccs node
	       val recp = (case cc of
			       {P} => P inset G
			       andalso P inset ?G P (* simple recursion *)
			     | _ => true (* mutual recursion *)
			       )
	       end
	   end
    end;

local
    val nfa = re_make_nfa [(re_parse "^#false\\(([^()]*)\\)",
			    fn (s,a) => re_subst(s,a,1))]
in
    fun matches_bot P =
	nfa_run (nfa, P)
end;

fun source_list_bots source =
    {s
    | (_, GCLAUSE (_, [P $ _]), ...) in list source
      val SOME s = matches_bot P};

fun usage () =
    (#put stderr "Usage: h1mc <flags>* model-file log-file.\n\
     \  Version ";
     #put stderr version;
     #put stderr ", Copyright (C) Jean Goubault-Larrecq;\n\
     \     see file COPYRIGHT.\n\
     \  h1mc comes with ABSOLUTELY NO WARRANTY; see file COPYING, sections 11, 12.\n\
     \  This is free software, and you are welcome to redistribute it\n\
     \  under certain conditions; see TERMS AND CONDITIONS in file COPYING.\n\
     \    Use '-' instead of model-file or log-file to read from stdin.\n\
     \    Usual model-file ends in '.pl'.\n\
     \    Usual log-file ends in '.p' or in '.log'.\n\
     \  Flags are:\n\
     \    -h prints this help.\n\
     \    -v0 runs silently, -v1 (aka., -v) prints clauses as they are checked.\n\
     \        -v2 prints more detailed info, -v3 even more.\n\
     \       Default: -v0.\n\
     \    -exact-sig: model-checks using exact first-order signature given\n\
     \        in model-file and log-file.  Less efficient than -no-exact-sig,\n\
     \        which is enough for checking models produced by h1.\n\
     \       Default: -no-exact-sig.\n\
     \    -type <fmt>: outputs proof using format <fmt>. Supported formats:\n\
     \        tree : prints proof in tree form, usable in Emacs outline-mode.\n\
     \        coq  : prints proof in Coq format (default: version 8).\n\
     \        coq8 : prints proof in Coq v8 format.\n\
     \        coq7 : prints proof in Coq v7 format (obsolescent).\n\
     \        none : does not print proof.\n\
     \       Default: -type tree.\n\
     \    -axioms: introduce unproved assumptions (Axiom declarations in Coq)\n\
     \        so as to be able to prove all clauses in model-file,\n\
     \        even unprovable ones.\n\
     \       Default: -no-axioms.\n";
     #flush stderr ());

fun infile_or_stdin "-" = stdin
  | infile_or_stdin name =
    let val |[get, getline, ...]| = infile name
    in
	|[get=get, getline=getline]|
    end;

datatype logfile = SOURCE | LOG;

local
    val nfa = re_make_nfa [(re_parse ".log$", fn _ => ())]
in
    fun logtype name =
	case nfa_run (nfa, name) of
	    SOME _ => LOG
	  | _ => SOURCE
end

fun open_log "-" = (stdin, SOURCE)
  | open_log name =
    let val |[get, getline, ...]| = infile name
	val f = |[get=get, getline=getline]|
    in
	(f, logtype name)
    end;

exception QuitEvt of int;

val bot_prefix = ref "reach_";
val rem_name = ref "rem_";
val term_type = ref "term"; (* "extterm"; *)
val xname = ref "X";
val lemma_prefix = ref "lem_";
val fun_prefix = ref ""; (* "ext_"; *)
val state_prefix = ref "auto_";
val trans_name = ref "trans_";

exception PrintType;
exception Pfc;

fun do_args ["-h"] = usage ()
  | do_args ("-h"::l) = (usage (); do_args l)
  | do_args ("-exact-sig"::l) = (exact_sig := true; do_args l)
  | do_args ("-no-exact-sig"::l) = (exact_sig := false; do_args l)
  | do_args ("-type"::"coq7"::l) = (print_type := "coq";
				    coq_version := "7";
				    do_args l)
  | do_args ("-type"::"coq8"::l) = (print_type := "coq";
				    coq_version := "8";
				    do_args l)
  | do_args ("-type"::"coq"::l) = (print_type := "coq";
				    coq_version := "8";
				    do_args l)
  | do_args ("-type"::fmt::l) = (print_type := fmt; do_args l)
  | do_args ("-axioms"::l) = (create_axioms := true; do_args l)
  | do_args ("-no-axioms"::l) = (create_axioms := false; do_args l)
  | do_args ("-v0" :: l) = (verbosity := 0; do_args l)
  | do_args ("-v1" :: l) = (verbosity := 1; do_args l)
  | do_args ("-v2" :: l) = (verbosity := 2; do_args l)
  | do_args ("-v3" :: l) = (verbosity := 3; do_args l)
  | do_args ("-v" :: l) = (verbosity := 1; do_args l)
  | do_args (modelfile :: logfile :: l) =
    (if not (null l)
	 then (#put stderr "ignored junk after log-file (";
	       #put stderr logfile;
	       #put stderr ")\n";
	       #flush stderr ())
     else ();
	 let val f = infile_or_stdin modelfile
	     val yyd = glex_data (f, fn _ => true)
	     val yyloc = glex_loc yyd
	     val hyd = gyacc_data (yyd, plautolex, aplnone (), plauto_value,
				   yyloc, yyerror yyloc)
	 in
	     case plautoparse hyd of
		 SOME (aplauto a) =>
		 (let val (f, log_cat) = open_log logfile
		      val yyd = glex_data (f, fn _ => true)
		      val yyloc = glex_loc yyd
		      val res =
			  case log_cat of
			      LOG =>
			      let val hyd = gyacc_data (yyd, prooflex,
							prnone (), proof_value,
							yyloc, yyerror yyloc)
			      in
				  proofparse hyd
			      end
			    | SOURCE =>
			      let val hyd = gyacc_data (yyd, tptplex,
							yynone (), tptp_value,
							yyloc, yyerror yyloc)
			      in
				  case tptpparse hyd of
				      SOME (clauselist cl) =>
				      let val cl' =
					      [(case c of
						    GCLAUSE (neg, nil) =>
						    (name, kw,
						     GCLAUSE (neg,
							      [("#false(" ^
								name ^ ")")
								   $ nil]))
						  | _ => (name, kw, c))
					      | (name, kw, c) in list cl]
				      in
					  SOME (proofinfo
						|[source=[(name, c)
							 | (name, _, c)
							      in list cl'],
						  definitions={},
						  approximation={c
								| (_, _, c)
								  in list cl'},
						  justifications={},
						  deductions={}
						  ]|)
				      end
				    | NONE => NONE
			      end
		  in
		      case res of
			  SOME (proofinfo |[ source = source0,
					     definitions = definitions0,
					     approximation = approximation0,
					     justifications = justifications0,
					     ... ]|) =>
			  let val has_eq = gclause_list_has_equality source0
			      val eq_th = if has_eq
					      then let val s = [c
							       | (_, c) in list
								 source0]
						       val psig = gclause_list_pred_sig s
						       val fsig = gclause_list_sig s
						       memofun varname i =
							       let val f as |[convert, ...]| = outstring "X"
							       in
								   print f (pack (i:int));
								   convert ()
							       end
						   in
						       theory_of_equality (psig, fsig, varname)
						   end
					  else nil
			      val source1 = if has_eq
						then source0
					    else eq_th @ source0
			      val source = [(name, c, gclause_make_monadic c)
					   | (name, c) in list source1]
			      val definitions = {gclause_make_monadic c
						| c in set definitions0}
			      val approximation =
				  {gclause_make_monadic c
				  | (_, c) in list eq_th} U
				  {gclause_make_monadic c
				  | c in set approximation0}
			      val justifications = {gclause_make_monadic c =>
						     (rulename,
						      [(gclause_make_monadic c, sigma)
						      | (c, sigma) in list premises])
						   | c => (rulename, premises) in map
						     justifications0}
			      val |[block_incl, ...]| = auto_simple_inclusions a
			      val a1 = auto_simplify (auto_trim a, block_incl)
				  (* changed JGL 15 mar 2008. *)
			      val a' = if has_eq
					   then enrich_auto_eq a1
				       else a1
			      fun xi (i : int) =
				  let val f as |[put, convert, ...]| = outstring (!xname)
				  in
				      print f (pack i);
				      convert ()
				  end
			      val clauses = [c | c in set definitions U approximation]
			      val Psig0 = overwrite [{P => len l
						     | P $ l in list neg} ++
						       {P => len l
						       | P $ l in list pos}
						    | GCLAUSE (neg, pos)
						      in set definitions0
							  U approximation0]
			      val fsig = let val AUTO (auto, _) = a'
						 (* was a; JGL 15 mar 2008 *)
					     val fsigr = ref (gclause_list_sig clauses)
					 in
					     iterate
					       iterate
						 if f inset !fsigr
						     then () (* !!!should raise smth. *)
						 else fsigr := !fsigr ++ {f => k}
					       | f => (_, k, ...) in map fmap
					       end
					     | P => fmap in map auto
					     end;
					     !fsigr
					 end
			      val xfsig =
				  if !exact_sig
				      then SOME {f => k
						| f => k in map fsig
						    such that not
							(false_fun_matches f
							 orelse
							 tuple_matches f)}
				  else NONE
			      val |[mc, reset = mc_reset, ...]| =
				  model_check (a', xi, xfsig)
			      val pgc = print_gclause_pl (stderr, identity)
			      fun mcheck c =
				  (do_verbose (1, fn () =>
					       (#put stderr "Checking clause ";
						pgc c;
						#put stderr ".."; #flush stderr ()));
				   (*mc_reset ();*)
				   case mc c of
				       SOME j =>
				       (
					(* mc_reset ();
					 to save space; *)
					do_verbose (2, fn () =>
						    #put stderr "\n ...");
					do_verbose (1, fn () =>
						    (#put stderr " OK.\n";
						     #flush stderr ()));
					SOME j
					)
				     | _ =>
				       (do_verbose (1, fn () =>
						    (#put stderr " failed.\n";
						     #flush stderr ()));
					NONE))
			      val abbrv_table = ref {}
			      val make_lam = make_natded (definitions, approximation,
							  justifications,
							  abbrv_table)
			      fun make_lambda c =
				  (SOME (make_lam c)
				   handle PfcMakeNatdedEvt msg =>
				   (do_verbose (1, fn () => #put stderr "\n  ");
				    #put stderr "Error: ";
				    #put stderr msg;
				    #put stderr "\n";
				    #flush stderr ();
				    NONE))
			      val def_jl = ll_enum_set (mcheck, definitions)
			      val app_jl = ll_enum_set (mcheck, approximation)
				  (*
			      val def_jl = [j
					   | c in set definitions
					     val SOME j = mcheck c]
			      val app_jl = [j
					   | c in set approximation
					     val SOME j = mcheck c]
				   *)
			      val def_names = ref {}
			      val app_names = ref {}
			      val pfal =
				  [(do_verbose (1, fn () =>
						(#put stderr " OK.\n";
						 #flush stderr ()));
				    (name, c0, c, pfa))
				  | (name, c0, c) in list source
				      val SOME pfa =
					  (do_verbose (1, fn () =>
						       (#put stderr "Checking source clause ";
							#put stderr name;
							#put stderr "."));
					   make_lambda c)]
			  in
			      (case !print_type of
				   "none" =>
				   (iter_ll (fn _ => (), def_jl);
				    iter_ll (fn _ => (), app_jl)
				    )
				 | "tree" =>
				   (let val mcprd = mc_print_tree (stdout, a')
					    (* was a; JGL 15 mar 2008 *)
					val cntr = ref 0
					fun mcpr j =
					    let val f as |[put, convert, ...]|
						    = outstring ""
					    in
						inc cntr;
						print f (pack (!cntr));
						put ".";
						mcprd (j, convert ())
					    end
					val AUTO (auto, univ) = a'
					    (* was a; JGL 15 mar 2008 *)
					val funs = union {dom fmap
							 | P => fmap in map auto}
					val deps = definitions_dependencies definitions
					val id = index_definitions (definitions, deps)
					val |[gclauses_expand, ...]| = expand_definitions id
					val pac = print_auto_clauses (stdout, "X", "\n  ")
					val jr = ref 0
				    in
					#put stdout "%-*-mode:outline;\
					 \outline-regexp:\"[0-9a-z.]+\"-*-\n";
					iterate
					  (#put stdout ". Semantics of ";
					   #put stdout f;
					   #put stdout "\n";
					   jr := 0;
					   iterate
					     let val (blkls, k, ...) = ?fmap f
					     in
						 iterate
						   (inc jr;
						    print_case stdout (!jr);
						    #put stdout " ";
						    pac (P, f, {blkl}, k);
						    if k=0
							then (if P inset id
								  then let val dr = ref "\n      [where "
								       in
									   iterate
									     (#put stdout (!dr);
									      dr := "\n             ";
									      print_gclause_pl (stdout, identity) c)
									   | c in set
									     gclauses_expand
									     (?id P)
									   end;
									   #put stdout "]"
								       end
							      else ())
						    else let val ir = ref 0
							     val delimr = ref "\n    If  "
							 in
							     iterate
							       (inc ir;
								iterate
								  (#put stdout (!delimr);
								   delimr := "\n    and ";
								   #put stdout P;
								   #put stdout " X";
								   if k=1
								       then ()
								   else print stdout (pack (!ir));
								   if P inset id
								       then let val dr = ref "\n      [where "
									    in
										iterate
										  (#put stdout (!dr);
										   dr := "\n             ";
										   print_gclause_pl (stdout, identity) c)
										| c in set
										  gclauses_expand
										  (?id P)
										end;
										#put stdout "]"
									    end
								   else ())
								| P in set blk
								end)
							     | blk in list blkl
							     end;
							     #put stdout "\n    then ";
							     pac (P, f, {[{} | _ in list blkl]},
								  k);
							     if P inset id
								 then let val dr = ref "\n      [where "
								      in
									  iterate
									    (#put stdout (!dr);
									     dr := "\n             ";
									     print_gclause_pl (stdout, identity) c)
									  | c in set
									    gclauses_expand
									    (?id P)
									  end;
									  #put stdout "]"
								      end
							     else ()
							 end;
							 #put stdout "\n"
						     )
						 | blkl in set blkls
						 end
					     end
					   | P => fmap in map auto
					     such that f inset fmap
					   end)
					| f in set funs
					  such that not (invisible_fun f)
					end;
					iter_ll (fn j =>
						    let val c = justif_gclause j
						    in
							if c inset !def_names
							    then ()
							else let val name = gensym "lemma "
							     in
								 #put stdout ". ";
								 #put stdout name;
								 #put stdout ":\n";
								 def_names := !def_names ++ {c => name};
								 mcpr j
							     end
						    end,
						    def_jl);
					(*
					iterate
					  if c inset !def_names
					      then ()
					  else let val name = gensym "lemma "
					       in
						   #put stdout ". ";
						   #put stdout name;
						   #put stdout ":";
						   def_names := !def_names ++ {c => name};
						   mcpr j
					       end
					| j in list def_jl
					val c = justif_gclause j
					end;
					 *)
					iter_ll (fn j =>
						    let val c = justif_gclause j
						    in
							if c inset !app_names
							    then ()
							else let val name = gensym "lemma "
							     in
								 #put stdout ". ";
								 #put stdout name;
								 #put stdout ":";
								 app_names := !app_names ++ {c => name};
								 mcpr j
							     end
						    end,
						    app_jl)
					(*
					iterate
					  if c inset !app_names
					      then ()
					  else let val name = gensym "lemma "
					       in
						   #put stdout ". ";
						   #put stdout name;
						   #put stdout ":";
						   app_names := !app_names ++ {c => name};
						   mcpr j
					       end
					| j in list app_jl
					val c = justif_gclause j
					end
					 *)
				    end;
				    iterate
					(let val Xs = Xsort (gclause_vars c)
					     val ts = [("$" ^ x) $ nil
						      | x in list Xs]
					     val tsub = tsubst {x => t
							       || x in list Xs and
								  t in list ts}
					     val negs = [GCLAUSE (nil, [tsub a])
							| a in list neg]
					     val assums =
						 [let val PF_L0 pfc =
							  pfc_from_clause (PFC_INPUT, n)
						  in
						      pfc
						  end
						 | n in list negs]
					     val negss = elems negs
					     val PF_L0 pfc =
						 pfc_apply_l_2 (pfc_apply_l_1 (pfa, ts),
								assums)
					     val pgc = print_gclause_pl (stdout, identity)
					     val unproved = ref false
					     val out as |[seek = out_seek,
							   truncate = out_truncate, ...]|
						 = outstring ""
					     fun by_def c =
						 (#put out (if c inset !def_names
								then ?(!def_names) c
							    else (unproved := true;
								  "*unproved assumption*")))
					     fun by_app c =
						 (#put out (if c inset !app_names
								then ?(!app_names) c
							    else if c inset negss
								then "assumption"
							    else (unproved := true;
								  "*unproved assumption*")))
					 in
					     #put stdout ". [";
					     #put stdout name;
					     #put stdout "] ";
					     pgc c;
					     out_seek 0; out_truncate ();
					     if null neg
						 then ()
					     else (#put out "\n  Assume";
						   iterate
						     (#put out " ";
						      print_gclause_pl (out, identity) n)
						   | n in list negs
						   end
						   );
						 pfc_print_tree (out, "\n  Show ",
								 by_def, by_app) [pfc];
						 if !unproved
						     then (#put stderr "Warning: clause ";
							   #put stderr name;
							   #put stderr " remains unproved.\n";
							   #flush stderr ();
							   if !create_axioms
							       then #put stdout (#convert out ())
							   else #put stdout " ***WRONG***.\n")
						 else (#put stdout (#convert out ()))
					 end handle Bind => raise Pfc)
				    | (name, _, c as GCLAUSE (neg, pos), pfa) in list pfal
				    end;
				    #flush stdout ())
				 | "coq" =>
				   let val namer = CAN (coq_auto_clause_name (!coq_version, !trans_name),
							coq_univ_clause_name (!coq_version, !trans_name))
				       val clauses0 = [c | c in set definitions0 U approximation0]
				       val fsig0 = gclause_list_sig clauses0
				       val preds = dom (gclause_list_pred_sig clauses)
				       val portype = coq_print_or_type (!coq_version, stdout,
									"or_")
				       val pextype = coq_print_ex_type (!coq_version, stdout,
									"ex_", "x")
				       val pinvPf = coq_print_inversion_P_f (!coq_version,
									     stdout,
									     portype,
									     !fun_prefix,
									     !state_prefix,
									     !rem_name,
									     !xname,
									     !term_type,
									     a', namer)
					   (*
				       val pinvP = coq_print_inversion_P (!coq_version,
									  stdout,
									  portype, pextype,
									  !fun_prefix,
									  !state_prefix,
									  !rem_name,
									  !xname,
									  !term_type,
									  auto, namer)
					    *)

				       fun var_name "" = "__dummy__"
					 | var_name s =
					   let val n = ord s
					   in
					       if n>=ord "A" andalso n<ord "X"
						   then ("_big_" ^ chr (ord s+32)
							 ^ substr (s, 1, size s))
					       else if n=ord "_" (* ensure var_name is injective. *)
						   then "_" ^ s
					       else s
					   end
				       val pj = coq_print_justif (a', !coq_version, stdout,
								  !fun_prefix, !state_prefix,
								  !rem_name, var_name, !xname,
								  Xsort,
								  !term_type, fsig0,
								  portype,
								  pinvPf,
								  (*pinvP,*)
								  namer)
				       fun mcj j = pj ({}, j)
				       val def_rems = ref {}
				       val ass_rems = ref {}
				       fun by_def c =
					   if c inset !def_rems
					       then ?(!def_rems) c
					   else if !create_axioms
					       then (#put stderr "Warning: clause ";
						     print_gclause_pl (stderr, identity) c;
						     #put stderr " remains unproved, and will be \
						      \postulated as an axiom.\n";
						     #flush stderr ();
						     raise PfcCoqNoNameEvt)
					   else raise PfcCoqAbortEvt
				       fun by_ass c =
					   if c inset !ass_rems
					       then ?(!ass_rems) c
					   else if !create_axioms
					       then (#put stderr "Warning: clause ";
						     print_gclause_pl (stderr, identity) c;
						     #put stderr " remains unproved, and will be \
						      \postulated as an axiom.\n";
						     #flush stderr ();
						     raise PfcCoqNoNameEvt)
					   else raise PfcCoqAbortEvt
				       val unproved_clauses = ref {}
				       fun do_abort (name, c) =
					   (#put stderr "Warning: clause ";
					    #put stderr name;
					    #put stderr " remains unproved.\n";
					    unproved_clauses := !unproved_clauses U {c};
					    #flush stderr ())
					   (*
				       val evalfun =
					   (#put stdout "(* [sigd] Signature definition. *)\n\n";
					    coq_print_sig (stdout,
							   !fun_prefix (*""*),
							   !term_type (*"term"*)
							   ) fsig0;
					    #put stdout "\n\n(* [extd] Extended signature \
					    \definition. *)\n\n";
					    coq_print_sig (stdout, !fun_prefix, !term_type) fsig;
					    #put stdout "\n\n";
					    coq_print_fsig_inclusion (!coq_version,
								      stdout, "", !fun_prefix,
								      "term", !term_type,
								      fsig0)
					     )
					   *)
				   in
				       #put stdout "(* [sigd] Signature definition. *)\n\n";
				       coq_print_sig (stdout,
						      !fun_prefix,
						      !term_type) fsig0;
					    (* we should have fsig=fsig0,
					     or in any case ... it may be
					     that fsig0 is smaller. *)
				       #put stdout "\n\n(* [modd] Model definition. *)\n\n";
				       (case !coq_version of
					    "7" => #put stdout "Require Refine.\n\n"
					  | _ => ());
				       coq_print_auto (!coq_version, stdout, !term_type,
						       !bot_prefix, !fun_prefix, !state_prefix,
						       !xname, namer) (a',
								       Psig0,
								       preds,
								       {}, {}
								       (*truebots, falsebots*)
								       );
				       #put stdout "\n(* [defp] Proofs that all definitions \
							\hold. *)\n\n";
				       iter_ll (fn j =>
						   let val c = justif_gclause j
						   in
						       if c inset !def_rems
							   then ()
						       else def_rems := !def_rems ++ {c => mcj j}
						   end,
						   def_jl);
				       (*
				       iterate
					 if c inset !def_rems
					     then ()
					 else def_rems := !def_rems ++ {c => mcj j}
				       | j in list def_jl
				       val c = justif_gclause j
				       end;
					*)
				       #put stdout "\n(* [appp] Proofs that all \
                                                        \approximation clauses \
							\hold. *)\n\n";
				       iter_ll (fn j =>
						   let val c = justif_gclause j
						   in
						       if c inset !ass_rems
							   then ()
						       else ass_rems := !ass_rems ++ {c => mcj j}
						   end,
						   app_jl);
				       (*
				       iterate
					 if c inset !ass_rems
					     then ()
					 else ass_rems := !ass_rems ++ {c => mcj j}
				       | j in list app_jl
				       val c = justif_gclause j
				       end;
					*)
				       #put stdout "\n(* [trnp] Proofs of translated \
                                                    \source clauses. *)\n\n";
				       pfc_print_coq_proofs (!coq_version,
							     stdout, "Lemma",
							     !lemma_prefix,
							     !fun_prefix, !state_prefix,
							     by_def, by_ass, do_abort,
							     var_name,
							     Xsort,
							     !term_type,
							     [(name, c, pfa)
							     | (name, _, c, pfa) in list pfal]);
				       let val true_source0 =
					       [(name, c0)
					       | (name, c0, c, ...) in list pfal
						 such that not (c inset !unproved_clauses)]
				       in
					   #put stdout "\n\n(* [srcc] Source clauses. *)\n\n";
					   coq_print_source (!coq_version, stdout, "", "", "",
							     var_name, Xsort, "term") true_source0;
					   #put stdout "\n(* [srct] Translation from \
                                                        \source clauses. *)\n\n";
					   coq_print_source_eval (!coq_version, stdout, "", "", "",
								  !lemma_prefix, !fun_prefix,
								  !state_prefix,
								  var_name,
								  "" (* evalfun *),
								  "term", !term_type) true_source0;
					   #put stdout "\n\n(* [conp] Consistency proofs. *)\n\n";
					   let val cpname0 = coq_pred_name (!coq_version, "", "term")
					       val cpname = coq_pred_name (!coq_version, !state_prefix,
									   !term_type)
					       val |[unfold_tac, dot_tac,
						     intro_tac, elim_tac, ...]|
						   = coq_keywords (!coq_version)
					   in
					       iterate
						 (#put stdout "Theorem thm_";
						  #put stdout botname;
						  #put stdout " : ~";
						  #put stdout (cpname0 P);
						  #put stdout ".\nProof.\n  ";
						  #put stdout unfold_tac;
						  #put stdout "not";
						  #put stdout dot_tac;
						  #put stdout " ";
						  #put stdout intro_tac;
						  #put stdout "H";
						  #put stdout dot_tac;
						  #put stdout "\n  ";
						  #put stdout elim_tac;
						  #put stdout "(translate_";
						  #put stdout (cpname P);
						  #put stdout "_from_";
						  #put stdout (cpname0 P);
						  #put stdout " H)";
						  #put stdout dot_tac;
						  #put stdout "\nQed.\n\n")
					       | botname in list Xsort (source_list_bots
									true_source0)
					       val P = "#false(" ^ botname ^ ")"
					       end
					   end
				       end;
				       #flush stdout ()
				   end
				 | s => (#put stderr "Error: unrecognized -type option: ";
					 #put stderr s;
					 #put stderr ".\n";
					 #flush stderr ();
					 raise QuitEvt 2))
			  end
			| _ => (#put stderr "Parsing failed in log-file: stop.\n";
				#flush stderr ();
				raise QuitEvt 2)
		  end handle IO n => (#put stderr logfile;
				      #put stderr ": ";
				      #put stderr (iomsg n);
				      #put stderr "\n";
				      #flush stderr ();
				      raise QuitEvt 2))
	       | _ => (#put stderr "Parsing failed in model-file: stop.\n"; #flush stderr ();
		       raise QuitEvt 2)
	 end handle IO n => (#put stderr modelfile;
			     #put stderr ": ";
			     #put stderr (iomsg n);
			     #put stderr "\n";
			     #flush stderr ();
			     raise QuitEvt 2))
  | do_args nil = (#put stderr "Missing filename.\n"; usage (); raise QuitEvt 2)
  | do_args _ = (usage ();
		 raise QuitEvt 2)
    ;

fun main () =
    (
     (*
      benign_exception_regexp := "^.*";
      *)
    do_args (args ()) handle QuitEvt n => quit n);
