(* Linear main loop.
   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 "linear_h";
open "linproto_h";
open "gensym_h";
open "yyerror_h";

val version = "1.0 - Jul 13, 2003";

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

local
    val nfa = re_make_nfa [(re_parse "^[0-9]+$", fn (s,a) => intofstring s)]
in
    fun match_dec s =
	nfa_run (nfa, s)
end;

val prefix = ref "q";
val epsilon = ref "epsilon";
val final = ref "final";
val cycle = ref "__cycle_";
val base = ref 2;
val extravarlist = ref ({} : string -m> lintype);

fun usage () =
    (#put stderr "Usage: linauto <flags>* filename.\n\
     \  Version ";
     #put stderr version;
     #put stderr ", Copyright (C) Jean Goubault-Larrecq;\n\
      \     see file COPYRIGHT.\n\
      \  linauto 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.\n\
      \  Flags are:\n\
      \    -h prints this help.\n\
      \    -base <n> produces an automaton in base <n> (n>=2); default: 2.\n\
      \    -var <name> declares variable <name> (only needed if <name> is not\n\
      \           free in system of equations given in <filename>);\n\
      \    -prefix <name> builds state names as <name>1, <name>2, ... default: q.\n\
      \    -epsilon <name> uses <name> for the empty word; default: epsilon.\n\
      \    -final <name> uses <name> as final predicate name; default: final.\n\
      \    -cycle <name> builds intermediate predicates <name>1, ..., <name>k,\n\
      \           where k is number of variables; each state satisfies\n\
      \           exactly one of these, and transitions go from a state satisfying\n\
      \           <name>i to <name>i-1 (mod k);   default: __cycle_.\n";
     #flush stderr ());

fun do_args ("-prefix" :: name :: l) =
    (prefix := name; do_args l)
  | do_args ("-epsilon" :: name :: l) =
    (epsilon := name; do_args l)
  | do_args ("-final" :: name :: l) =
    (final := name; do_args l)
  | do_args ("-cycle" :: name :: l) =
    (cycle := name; do_args l)
  | do_args ("-base" :: s :: l) =
    (case match_dec s of
	 SOME b => if b>=2
		       then (base := b; do_args l)
		   else (#put stderr "Base should be at least 2.\n";
			 #flush stderr ();
			 quit 2)
       | _ => (#put stderr "Expected number after -base.\n";
	       #flush stderr ();
	       quit 2))
  | do_args ("-var" :: name :: l) =
    (extravarlist := !extravarlist ++ {name => LIN_NAT};
     do_args l)
  | do_args ["-h"] = usage ()
  | do_args ("-h"::l) = (usage (); 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, linearlex, linearnone (), linear_value, yyloc, yyerror yyloc)
	 in
	     case linearparse hyd of
		 SOME (linearproblem lsys) =>
		 let val lauto = linsys_to_auto (!extravarlist, LIN_NAT, op strless, !base, lsys)
		 in
		     print_lin_table (stdout, !prefix, !epsilon, !final, !cycle, !base, lauto);
		     #flush stdout ();
		     quit 0
		 end
	       | _ =>
		 (#put stderr "Parsing failed: stop.\n"; #flush stderr ();
		  quit 2)
	 end handle IO n => (#put stderr filename;
			     #put stderr ": ";
			     #put stderr (iomsg n);
			     #put stderr "\n";
			     #flush stderr ();
			     quit 2)
		  | LinearUnterminatedCommentEvt => (#put stderr "Unterminated comment: stop.\n";
						     #flush stderr ();
						     quit 2))
  | do_args nil = (#put stderr "Missing filename.\n"; usage (); quit 2)
  | do_args _ = (usage ();
		 quit 2)
    ;

fun main () =
    do_args (args ());
