(* h1trace proof explainer main loop.
   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 "proof_h";
open "yyerror_h";
open "ne_h";
open "natded_h";
open "pfcprint_h";
open "pfcprinttree_h";
open "pfcprinttreeabbrv_h";
open "pfcprintcoq_h";
open "coq_term_h";
open "coq_gclause_h";
open "coq_fun_h";
open "sort_h";

val version = "1.1 - Jan 24, 2008";
    (* "1.0"; date inconnue *)

val print_type = ref "tree-abbrv";

fun usage () =
    (#put stderr "Usage: h1trace <flags>* filename.\n\
     \  Version ";
     #put stderr version;
     #put stderr ", 1.0, Copyright (C) Jean Goubault-Larrecq;\n\
      \     see file COPYRIGHT.\n\
      \  h1trace 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 filename to read from stdin. Usual filename ends in '.log'.\n\
      \  Flags are:\n\
      \    -h prints this help.\n\
      \    -type <fmt>: outputs proofs using format <fmt>. Supported formats:\n\
      \        tree : prints proof in tree form, usable in Emacs outline-mode.\n\
      \        tree-abbrv : prints proof in tree form, with definitions abbreviated,\n\
      \                     usable in Emacs outline-mode.\n\
      \        log  : prints proof in same format as input.\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\
      \       Default: -type tree-abbrv.\n";
     #flush stderr ());

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

exception QuitEvt of int;

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

exception Pfc;

fun do_args ["-h"] = usage ()
  | do_args ("-h"::l) = (usage (); do_args l)
  | do_args ("-type"::"coq"::l) = (print_type := "coq8"; do_args l)
  | do_args ("-type"::fmt::l) = (print_type := fmt; do_args l)
  | do_args (filename :: l) =
    (if not (null l)
	 then (#put stderr "ignored junk after filename (";
	       #put stderr filename;
	      #put stderr ")\n";
	       #flush stderr ())
     else ();
	 let val f = infile_or_stdin filename
	     val yyd = glex_data (f, fn _ => true)
	     val yyloc = glex_loc yyd
	     val hyd = gyacc_data (yyd, prooflex, prnone (), proof_value, yyloc, yyerror yyloc)
	 in
	     case proofparse hyd of
		 SOME (proofinfo |[ source,
				    definitions, approximation, justifications,
				    deductions, ...]|) =>
		 (iterate
		    (case c of
			 GCLAUSE (neg, [P $ _]) =>
			 if matches_ne P
			     then
				 (#put stderr "Input clause ";
				  print_gclause_pl (stderr, identity) c;
				  #put stderr " derives a non-emptiness fact (not supported).\n";
				  #flush stderr ();
				  raise QuitEvt 2)
			 else ()
		       | _ => (#put stderr "Input clause ";
			       print_gclause_pl (stderr, identity) c;
			       #put stderr " is not definite.\n";
			       #flush stderr ();
			       raise QuitEvt 2))
		  | c in set definitions U approximation
		  end;
		  let val abbrv_table = ref {}
		      val make_lam = make_natded (definitions,
						  approximation,
						  deductions,
						  abbrv_table)
		      fun make_lambda c =
			  (make_lam c
			   handle PfcMakeNatdedEvt msg =>
			   (#put stderr "Error: ";
			    #put stderr msg;
			    #put stderr "\n";
			    #flush stderr ();
			    raise QuitEvt 2))
		      val assnames = assumption_names (source, definitions,
						       approximation, justifications)
		      val pr = case !print_type of
				   "tree" =>
				   (fn pfl => (#put stdout "%-*-mode:outline;\
						  \outline-regexp:\"[0-9a-z.]+\"-*-\n";
					      pfc_print_tree (stdout, ".",
							      fn _ =>
								 #put stdout "definition",
							      fn _ =>
								 #put stdout "assumption"
								 )
					       pfl))
				 | "tree-abbrv" =>
				   (fn pfl => (#put stdout "%-*-mode:outline;\
						  \outline-regexp:\"[0-9a-z.]+\"-*-\n";
					       pfc_print_tree_abbrv (stdout, ".",
							      fn _ =>
								 #put stdout "definition",
							      fn _ =>
								 #put stdout "assumption",
								     assnames) pfl))
				 | "log" => pfc_print stdout
				 | "coq8" => (fn pfl =>
						 pfc_print_coq ("8", stdout,
								"Theorem",
								"", "", "",
								definitions,
								approximation,
								identity,
								sort (op strless),
								"term", pfl))
				 | "coq7" => (fn pfl =>
						 pfc_print_coq ("7", stdout,
								"Theorem",
								"", "", "",
								definitions,
								approximation,
								identity,
								sort (op strless),
								"term", pfl))
				 | s => (#put stderr "Error: unrecognized -type option: ";
					 #put stderr s;
					 #put stderr ".\n";
					 #flush stderr ();
					 raise QuitEvt 2)
		      val pfcl = [(case make_lambda c of
				       PF_L0 pfc =>
				       pfc
				     | _ => raise Pfc)
				 | c as GCLAUSE (nil, [P $ nil]) in set deductions
				     val SOME _ = matches_bot P]
		  in
		      pr pfcl;
		      #flush stdout ()
		  end)
	       | _ => (#put stderr "Parsing failed: stop.\n"; #flush stderr ();
		       raise QuitEvt 2)
	 end handle IO n => (#put stderr filename;
			     #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 () =
    do_args (args ()) handle QuitEvt n => quit n;
