(* Copyright (C) 2004, HELM Team.
 * 
 * This file is part of HELM, an Hypertextual, Electronic
 * Library of Mathematics, developed at the Computer Science
 * Department, University of Bologna, Italy.
 * 
 * HELM 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
 * of the License, or (at your option) any later version.
 * 
 * HELM 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 HELM; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 * MA  02111-1307, USA.
 * 
 * For details, see the HELM World-Wide-Web page,
 * http://helm.cs.unibo.it/
 *)

open Printf

open MatitaTypes

let message s = printf  "** MatitaC: %s\n" s; flush stdout
let warn s =    eprintf "** MatitaC WARNING: %s\n" s; flush stdout
let error s =   eprintf "** MatitaC ERROR: %s\n" s; flush stderr

  (** console which prints on stdout/stderr *)
class tty_console =
  object (self)
    method clear () = ()
    method echo_message s = message s
    method echo_error s =  error s
      (* TODO Zack: this method is similar to omonymous method in console,
      * factorize it in a common super class *)
    method wrap_exn: 'a. (unit -> 'a) -> 'a option =
      fun f ->
      try
        Some (f ())
      with exn ->
        self#echo_error (explain exn);
        None
  end

(** {2 Initialization} *)

let arg_spec = [
(*   "-opt", Arg...., "set bla bla bla"; *)
]
let usage =
  sprintf "MatitaC v%s\nUsage: matitac [option ...] file ...\nOptions:"
    BuildTimeConf.version

let _ = Helm_registry.load_from "matita.conf.xml"

let scripts =
  let acc = ref [] in
  let add_script fname = acc := fname :: !acc in
  Arg.parse arg_spec add_script usage;
  List.rev !acc

let parserr = new MatitaDisambiguator.parserr ()
let dbd =
  Mysql.quick_connect
    ~host:(Helm_registry.get "db.host")
    ~user:(Helm_registry.get "db.user")
    ~database:(Helm_registry.get "db.database")
    ()
let _ = MetadataDb.clean ~dbd ~owner:(Helm_registry.get "matita.owner")
let disambiguator =
  new MatitaDisambiguator.disambiguator ~parserr ~dbd
    ~chooseUris:mono_uris_callback ~chooseInterp:mono_interp_callback
    ()
let console = new tty_console
let interpreter = MatitaInterpreter.interpreter ~disambiguator ~console ()

let run_script fname =
  message (sprintf "execution of %s started:" fname);
  let script =
    let ic = open_in fname in
    let ast = 
      try 
        snd (CicTextualParser2.parse_script (Stream.of_channel ic)) 
      with
        exn -> 
          error (explain exn); 
          assert false (* should be something like (Unix.exit 1) *)
    in
    close_in ic;
    ast
  in
  let rec aux = function
    | [] -> ()  (* script is over *)
    | DisambiguateTypes.Comment _ :: tl -> aux tl
    | DisambiguateTypes.Command ast :: tl ->
        let loc =
          match ast with
          | TacticAst.LocatedTactical (loc, _) -> loc
          | _ -> assert false
        in
        let (success, _) = interpreter#evalAst ast in
        if not success then
          error (sprintf "%s: error at %s, aborting." fname
            (CicAst.pp_location loc))
        else
          aux tl
  in
  aux script;
  message (sprintf "execution of %s completed." fname)

let _ = List.iter run_script scripts