open Misc
open Ast

(* Main program *)

let parse ic =
  let lb = Lexing.from_channel ic in
  try
    Parser.character Lexer.token lb
  with Parsing.Parse_error ->
         Printf.printf "Syntax error near character %d\n"
                       (Lexing.lexeme_start lb);
         flush stdout; exit 2
     | Lexer.Error n ->
         Printf.printf "Lexical error near character %d\n" n;
         flush stdout; exit 2

let main() =
  let timeout = ref (30 * 60) in
  Arg.parse
    ["-test_duration", Arg.Float(fun f -> Randomtest.test_duration := f),
       "<secs>  set duration of random equivalence tests"]
    (fun s ->
      try timeout := int_of_string s with Failure _ -> ())
    "Usage: opti <options> [duration in seconds]\nOptions are:";
  Sys.set_signal Sys.sigalrm
    (Sys.Signal_handle (fun _ -> prerr_endline "Time is up!"; raise Timeout));
  ignore(Unix.alarm (max 60 (!timeout - 60)));
  Synthmain.opti_duration := float !timeout *. 0.5;
  let c = parse stdin in
  (* Optimization passes *)
  begin try
    Results.init c;
    Cuoq_schmitt.main (Syntax.from_ast c);
    Simplif.simpl_character c;
    let dd = Synthmain.optimize (Results.get_best_character()) in
    Cuoq_schmitt.main (Syntax.from_ast dd);
    Simplif.simpl_character dd;
    Simplif.simpl_character (Results.get_best_character())
  with x ->
    ()
  end;
  (* Print result *)
  ignore(Unix.alarm 0);
  let c' = Results.get_best_character() in
  pretty_character c';
  Format.print_newline();
  Printf.eprintf "Original size: %d, new size: %d\n"
                 (size_character c) (size_character c');
  flush stderr

let _ = main()