(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.              
     \ /   This software is distributed as is, NO WARRANTY.              
      V_______________________________________________________________ *)

module KF = Filename
module KL = List
module KP = Printf
module KS = String
module KT = String

module U  = NUri
module C  = Cps
module L  = Log
module Y  = Time
module P  = Marks
module G  = Options
module H  = Hierarchy
module N  = Layer
module E  = Entity
module O  = Output
module DO = CrgOutput
module TD = TxtCrg
module AA = AutProcess
module AO = AutOutput
module AD = AutCrg
module XL = XmlLibrary
module XD = XmlCrg
module B  = Brg
module BD = BrgCrg
module BO = BrgOutput
module BR = BrgReduction
module BU = BrgUntrusted
module BM = BrgMatita
module BQ = BrgCoq
module BH = BrgHelena
(* module BC = BrgCC *)
module BY = BrgLYP
module ZD = BagCrg
module ZO = BagOutput
module ZT = BagType
module ZU = BagUntrusted

type status = {
   kst: N.status;
   tst: TD.status;
   pst: AA.status;
   ast: AD.status;
   ac : AO.counters;
   dc : DO.counters;
   bc : BO.counters;
   zc : ZO.counters;
   mst: B.manager option;
}

let level = 0

let bag_error st s msg =
   L.error st.kst ZO.specs (L.Warn s :: msg) 

let brg_error st s msg =
   L.error st.kst BR.specs (L.Warn s :: msg)

let initial_status () = {
   kst = N.initial_status ();
   tst = TD.initial_status ();
   pst = AA.initial_status ();
   ast = AD.initial_status ();
   ac  = AO.initial_counters;
   dc  = DO.initial_counters;
   bc  = BO.initial_counters;
   zc  = ZO.initial_counters;
   mst = None;
}

let refresh_status st = {st with
   kst = N.refresh_status st.kst;
   tst = TD.refresh_status st.tst;
   ast = AD.refresh_status st.ast;
}

(* kernel related ***********************************************************)

type kernel_entity = BrgEntity of Brg.entity
                   | BagEntity of Bag.entity
		   | CrgEntity of Crg.entity

IFDEF SUMMARY THEN

let print_counters st = function
   | G.V4 -> DO.print_counters C.start st.dc
   | G.V3 -> BO.print_counters C.start st.bc
   | G.V0 -> ZO.print_counters C.start st.zc

END

IFDEF TRACE THEN

let pp_progress e =
   let f _ na u =
      let s = U.string_of_uri u in
      L.warn 2 (KP.sprintf "[%u] <%s>" na.E.n_apix s);
   in
   Y.utime_stamp "intermediate";
   match e with
      | CrgEntity e -> E.common f e
      | BrgEntity e -> E.common f e
      | BagEntity e -> E.common f e      

END

IFDEF SUMMARY THEN

let count_entity st = function
   | BrgEntity e -> {st with bc = BO.count_entity C.start st.bc e}
   | BagEntity e -> {st with zc = ZO.count_entity C.start st.zc e}
   | CrgEntity e -> {st with dc = DO.count_entity C.start st.dc e}

END

IFDEF OBJECTS THEN

let export_entity st = function
   | CrgEntity e -> XL.export_entity (XD.export_term st.kst) e
   | BrgEntity e -> XL.export_entity (BO.export_term st.kst) e
   | BagEntity e -> XL.export_entity (ZO.export_term st.kst) e

END

IFDEF TYPE THEN

let type_check st k =
   let brg_err msg = brg_error st "Type Error" msg; failwith "Interrupted" in
   let bag_err msg = bag_error st "Type Error" msg; failwith "Interrupted" in
   let ok _ _ = st in
   match k with
      | BrgEntity entity -> BU.type_check brg_err ok st.kst entity
      | BagEntity entity -> ZU.type_check bag_err ok st.kst entity
      | CrgEntity _      -> st

END

IFDEF MANAGER THEN

let manager st output_entity = function
   | BrgEntity entity -> 
      if output_entity st.kst entity then st else
      begin L.warn level "manager exportation stopped"; {st with mst = None} end
   | BagEntity _      -> st
   | CrgEntity _      -> st

END

let xlate_entity st entity = match !G.kernel, entity with
   | G.V3, CrgEntity e -> 
      let f e = (BrgEntity e) in E.xlate f BD.brg_of_crg e
   | G.V0, CrgEntity e -> 
      let f e = (BagEntity e) in E.xlate f (ZD.bag_of_crg st.kst) e
   | _, entity         -> entity

let validate st k =
   let brg_err msg = brg_error st "Validation Error" msg; failwith "Interrupted" in
   let ok _ = st in
   match k with
      | BrgEntity entity -> BU.validate brg_err ok st.kst entity
      | BagEntity _      -> st
      | CrgEntity _      -> st

(* extended lexer ***********************************************************)

type 'token lexer = {
   parse : Lexing.lexbuf -> 'token;
   mutable tokbuf: 'token option;
   mutable unget : bool
}

let initial_lexer parse = {
   parse = parse; tokbuf = None; unget = false
}

let token xl lexbuf = match xl.tokbuf with
   | Some token when xl.unget ->   
      xl.unget <- false; token
   | _                        ->
      let token = xl.parse lexbuf in
      xl.tokbuf <- Some token; token

(* input related ************************************************************)

type input = Text | Automath

type input_entity = TxtEntity of Txt.command
                  | AutEntity of Aut.command
		  | NoEntity

let type_of_input name =
   if KF.check_suffix name ".hln" then Text 
   else if KF.check_suffix name ".aut" then 
      let _ = H.set_sorts 0 ["Set"; "Prop"] in
      assert (H.set_graph "Z2");
      Automath
   else begin
      L.warn level (KP.sprintf "Unknown file type: %s" name); exit 2
   end

let txt_xl = initial_lexer TxtLexer.token 

let aut_xl = initial_lexer AutLexer.token 

let parbuf = ref [] (* parser buffer *)

let gen_text command = 
   parbuf := TxtEntity command :: !parbuf

let entity_of_input lexbuf i = match i, !parbuf with
   | Automath, _    -> 
      begin match AutParser.entry (token aut_xl) lexbuf with
         | Some e -> aut_xl.unget <- true; AutEntity e
         | None   -> NoEntity
      end     
   | Text, []       -> 
      begin match TxtParser.entry (token txt_xl) lexbuf with
         | Some e -> txt_xl.unget <- true; TxtEntity e
         | None   -> NoEntity
      end
   | Text, hd :: tl ->
      parbuf := tl; hd

IFDEF PREPROCESS THEN

let process_input f st = function 
   | AutEntity e     ->
      let f pst e = f {st with pst = pst} (AutEntity e) in
      AA.process_command f st.pst e
   | xe              -> f st xe

END

IFDEF SUMMARY THEN

let count_input st = function
   | AutEntity e -> {st with ac = AO.count_command C.start st.ac e}
   | xe          -> st

END

(****************************************************************************)

let st = ref (initial_status ())
let streaming = ref false (* parsing style (temporary) *)

let process_2 st entity =
   let st =
IFDEF SUMMARY THEN
      if !G.summary then count_entity st entity else st
ELSE 
      st
END
   in
   let st =
IFDEF STAGE THEN
      if !G.stage >= 3 then
IFDEF TYPE THEN 
         let f = if !G.validate then validate else type_check in f st entity
ELSE
         validate st entity
END
      else st
ELSE
IFDEF TYPE THEN 
      let f = if !G.validate then validate else type_check in f st entity
ELSE
      validate st entity
END
END
   in
IFDEF OBJECTS THEN
   if !G.export then export_entity st entity
ELSE () END;
IFDEF MANAGER THEN
   match st.mst with
     | None                    -> st
     | Some (export_entity, _) -> manager st export_entity entity
ELSE
     st
END

let process_1 st entity =
IFDEF TRACE THEN
   if !G.ct >= 3 then pp_progress entity;
ELSE () END;
   let st =
IFDEF SUMMARY THEN
      if !G.summary then count_entity st entity else st
ELSE
      st
END
   in
IFDEF STAGE THEN
IFDEF OBJECTS THEN
   if !G.export && !G.stage = 1 then export_entity st entity
ELSE () END;
   if !G.stage >= 2 then process_2 st (xlate_entity st entity) else st 
ELSE
   process_2 st (xlate_entity st entity)
END

let process_0 st entity = 
   let f st entity =
IFDEF STAGE THEN
      if !G.stage = 0 then st else
      match entity with
         | AutEntity e -> 
            let err ast = {st with ast = ast} in
            let g ast e = process_1 {st with ast = ast} (CrgEntity e) in
	    AD.crg_of_aut err g st.kst st.ast e
         | TxtEntity e -> 
            let crr tst = {st with tst = tst} in
            let d tst e = process_1 {st with tst = tst} (CrgEntity e) in
	    TD.crg_of_txt crr d gen_text st.tst e
	 | NoEntity    -> assert false
ELSE
      match entity with
         | AutEntity e -> 
            let err ast = {st with ast = ast} in
            let g ast e = process_1 {st with ast = ast} (CrgEntity e) in
	    AD.crg_of_aut err g st.kst st.ast e
         | TxtEntity e -> 
            let crr tst = {st with tst = tst} in
            let d tst e = process_1 {st with tst = tst} (CrgEntity e) in
	    TD.crg_of_txt crr d gen_text st.tst e
	 | NoEntity    -> assert false
END
   in
   let st =
IFDEF SUMMARY THEN
      if !G.summary then count_input st entity else st
ELSE
      st
END
   in 
IFDEF PREPROCESS THEN
   if !G.preprocess then process_input f st entity else f st entity
ELSE
   f st entity
END

let process_nostreaming st lexbuf input =
   let id x = x in
   let rec aux1 book = match entity_of_input lexbuf input with
      | NoEntity -> List.rev book
      | e        -> aux1 (id e :: book)   
   in
   let rec aux2 st = function
      | []           -> st
      | entity :: tl -> aux2 (process_0 st entity) tl
   in
   aux2 st (aux1 [])

let process_streaming st lexbuf input =
   let rec aux st = match entity_of_input lexbuf input with
      | NoEntity -> st
      | e        -> aux (process_0 st e)
   in
   aux st

(****************************************************************************)

IFDEF PREPROCESS THEN

let set_preprocess () = 
   if !G.trace >= 2 then begin
      G.preprocess := true;
IFDEF SUMMARY THEN
      G.summary := true
ELSE () END
   end

END

IFDEF MANAGER THEN

let set_manager s = match KS.lowercase s with
   | "v8"  -> G.manager := G.Coq
   | "ma2" -> G.manager := G.Matita
   | "lp1" -> G.manager := G.LP1
   | "lp2" -> G.manager := G.LP2
   | "tj2" -> G.manager := G.TJ2
   | "tj3" -> G.manager := G.TJ3
(*
   | "cc0" -> G.manager := G.CC0
*)
   | "lyp" -> G.manager := G.LYP
   | s     -> L.warn level (KP.sprintf "Unknown manager: %s" s)

END

IFDEF SUMMARY THEN

let set_summary () =
   if !G.trace >= 2 then G.summary := true

END

let set_trace i = 
   if !G.trace = 0 && i > 0 then Y.gmtime (G.version_string false);
   if !G.trace > 0 && i = 0 then Y.utime_stamp "at exit";
   G.trace := i;
IFDEF SUMMARY THEN
   if i <= 1 then G.summary := false
ELSE () END;
IFDEF PREPROCESS THEN
   if i <= 1 then G.preprocess := false
ELSE () END

let custom_exit () =
   if !G.trace >= 1 then Y.utime_stamp "at exit"

let process st name =
   let process = if !streaming then process_streaming else process_nostreaming in
   let input = type_of_input name in
   let ich = open_in name in
   let lexbuf = Lexing.from_channel ich in 
   let st = process st lexbuf input in
   close_in ich;
   st, input

let main = 
   let print_version () =
      let features = [
(IFDEF LEXER THEN "LEXER" ELSE "" END);
(IFDEF PARSER THEN "PARSER" ELSE "" END);
(IFDEF TRACE THEN "TRACE" ELSE "" END);
(IFDEF SUMMARY THEN "SUMMARY" ELSE "" END);
(IFDEF EXPAND THEN "EXPAND" ELSE "" END);
(IFDEF MANAGER THEN "MANAGER" ELSE "" END);
(IFDEF OBJECTS THEN "OBJECTS" ELSE "" END);
(IFDEF PREPROCESS THEN "PREPROCESS" ELSE "" END);
(IFDEF QUOTE THEN "QUOTE" ELSE "" END);
(IFDEF STAGE THEN "STAGE" ELSE "" END);
(IFDEF TYPE THEN "TYPE" ELSE "" END);
(IFDEF PROFV THEN "PROFV" ELSE "" END);
      ] in
      let map s = s <> "" in
      let features_string = KT.concat " " (KL.filter map features) in
      L.warn level (KP.sprintf "%s [%s]" (G.version_string true) features_string);
      exit 0
   in
   let set_hierarchy s = 
      if H.set_graph s then () else 
         L.warn level (KP.sprintf "Unknown type hierarchy: %s" s)
   in
   let set_kernel = function
      | "V3" -> G.kernel := G.V3
      | "V0" -> G.kernel := G.V0
      | s    -> L.warn level (KP.sprintf "Unknown kernel version: %s" s)
   in
   let clear_options () =
      G.clear (); H.clear ();
IFDEF SUMMARY THEN
      O.clear_reductions ()
ELSE () END;
      streaming := false;
   in
   let undefined opt () =
      L.warn level (KP.sprintf "%s was compiled without the support for option %s" (G.version_string true) opt);
      exit 0
   in
   let arg_undefined opt = Arg.Unit (undefined opt) in
   let process_file name =
      if !G.trace >= 2 then begin
         L.warn 1 (KP.sprintf "Processing file: %s" name);
         Y.utime_stamp "started"
      end;
      let base_name = Filename.chop_extension (Filename.basename name) in
      let cover = KF.concat !G.root base_name in
      G.cover := cover;
IFDEF STAGE THEN
      if !G.stage <= 1 then G.kernel := G.V4;
ELSE () END;
IFDEF MANAGER THEN
      begin match !G.manager with
         | G.Coq    -> st := {!st with mst = Some (BQ.open_out base_name)}
         | G.Matita -> st := {!st with mst = Some (BM.open_out base_name)}
         | G.LP1    -> st := {!st with mst = Some (BH.open_out_lp1 base_name)}
         | G.LP2    -> st := {!st with mst = Some (BH.open_out_lp2 base_name)}
         | G.TJ2    -> st := {!st with mst = Some (BH.open_out_tj2 base_name)}
         | G.TJ3    -> st := {!st with mst = Some (BH.open_out_tj3 base_name)}
(*
         | G.CC0    -> st := {!st with mst = Some (BC.open_out_cc0 base_name)}
*)
         | G.LYP    -> st := {!st with mst = Some (BY.open_out_lyp2 base_name)}
         | G.Quiet  -> ()
      end
ELSE () END;
      P.clear_marks ();
      let sst, input = process (refresh_status !st) name in
      st := begin match sst.mst with 
         | None                -> sst
         | Some (_, close_out) -> close_out (); {sst with mst = None}
      end;
      if !G.trace >= 2 then Y.utime_stamp "processed";
IFDEF SUMMARY THEN
      if !G.summary then begin
         AO.print_counters C.start !st.ac;
IFDEF PREPROCESS THEN
         if !G.preprocess then AO.print_process_counters C.start !st.pst
ELSE () END;
IFDEF STAGE THEN
         if !G.stage >= 1 then print_counters !st G.V4;
         if !G.stage >= 2 then print_counters !st !G.kernel;
         if !G.stage >= 3 then O.print_reductions ()
ELSE
         print_counters !st G.V4;
         print_counters !st !G.kernel;
         O.print_reductions ()
END
      end
ELSE () END
   in
   let help = 
      "Usage: helena [ -LPVXdgilnoqtuxy01 | -Ts <number> | -MO <dir> | -p <file> | -ahkmr <string> | -be <age> ]* [ <file> ]*\n\n" ^
      "Trace levels: 0 just errors (default), 1 time stamps, 2 processed files, 3 processed objects,\n" ^
      "              4 typing information, 5 conversion information, 6 reduction information,\n" ^
      "              7 level disambiguation\n\n" ^
      "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n\n" ^
      "Supported manages: \"ma2\" (Grafite NG), \"v8\" (Gallina 8), \"lp1\" \"lp2\" \"tj2\" \"tj3\" \"lyp\" (lambda-Prolog)\n" 
   in
   let help_L = "         [lexer]     Show lexer debug information" in 
   let help_M = "<dir>    [manager]   Set location of output directory (manager) to <dir> (default: current directory)" in
   let help_O = "<dir>    [output]    Set location of output directory (XML) to <dir> (default: current directory)" in
   let help_P = "         [parser]    Show parser debug information" in 
   let help_T = "<number> [trace]     Set trace level (see above)" in
   let help_V = "         [version]   Show version information" in
   let help_X = "                     Clear options" in
   
   let help_a = "<string> [alpha]     Set prefix of numeric identifiers (default: empty)" in
   let help_b = "<age>    [begin]     Begin trace at this global constant (default: first)" in
   let help_c = "         [cast]      Anticipate cast in global definitions (Automath) (default: posticipate)" in
   let help_d = "         [data]      Show summary information (requires trace >= 2)" in
   let help_e = "<age>    [end]       End trace at this global constant (default: last)" in
   let help_g = "         [global]    Disable age-driven expansion of global definitions (default: enable)" in
   let help_h = "<string> [hierarchy] Set type hierarchy (default: \"Z1\")" in
   let help_i = "         [indexes]   Show local references by index" in
   let help_k = "<string> [kernel]    Set kernel version (default: \"V3\")" in
   let help_l = "         [layer]     Disambiguate binders layer (Automath)" in
   let help_m = "<string> [manager]   Export kernel entities for this manager (see above, default: no manager)" in
   let help_n = "         [names]     Show short constants (default: qualified constants)" in
   let help_o = "         [objects]   Export kernel entities (XML)" in
   let help_p = "<file>   [preamble]  Set preamble to this file (default: empty)" in
   let help_q = "         [quote]     Quote identifiers (default: disable)" in
   let help_r = "<string> [root]      Set initial segment of URI hierarchy (default: empty)" in
   let help_s = "<number> [stage]     Set translation stage (see above)" in
   let help_t = "         [type]      Type check (default: validate)" in
   let help_u = "         [upsilon]   Activate type comparison by sort inclusion (default: deactivate)" in
   let help_x = "         [extended]  Use extended applications (Automath)" in
   let help_y = "         [infinity]  Use ∞-abstractions in contexts" in
   let help_0 = "         [zero]      Preprocess source (Automath)" in
   let help_1 = "         [one]       parse files with streaming policy" in
   at_exit custom_exit;
   Arg.parse [
      ("-L", (IFDEF LEXER THEN Arg.Set G.debug_lexer ELSE arg_undefined "-L" END), help_L);
      ("-M", (IFDEF MANAGER THEN Arg.String ((:=) G.manager_dir) ELSE arg_undefined "-M" END), help_M);
      ("-O", (IFDEF OBJECTS THEN Arg.String ((:=) G.xdir) ELSE arg_undefined "-O" END), help_O);
      ("-P", (IFDEF PARSER THEN Arg.Set G.debug_parser ELSE arg_undefined "-P" END), help_P);
      ("-T", Arg.Int set_trace, help_T);
      ("-V", Arg.Unit print_version, help_V);
      ("-X", Arg.Unit clear_options, help_X);
      ("-a", Arg.String ((:=) G.alpha), help_a);
      ("-b", Arg.Int ((:=) G.first), help_b);
      ("-c", Arg.Set G.cast, help_c);
      ("-d", (IFDEF SUMMARY THEN Arg.Unit set_summary ELSE arg_undefined "-d" END), help_d);
      ("-e", Arg.Int ((:=) G.last), help_e);
      ("-g", (IFDEF EXPAND THEN Arg.Set G.expand ELSE arg_undefined "-g" END), help_g);
      ("-h", Arg.String set_hierarchy, help_h);
      ("-i", Arg.Set G.indexes, help_i);
      ("-k", Arg.String set_kernel, help_k);
      ("-l", Arg.Set G.cc, help_l);
      ("-m", (IFDEF MANAGER THEN Arg.String set_manager ELSE arg_undefined "-m" END), help_m);      
      ("-n", Arg.Set G.short, help_n);
      ("-o", (IFDEF OBJECTS THEN Arg.Set G.export ELSE arg_undefined "-o" END), help_o);
      ("-p", (IFDEF MANAGER THEN Arg.String ((:=) G.preamble) ELSE arg_undefined "-p" END), help_p);
      ("-q", (IFDEF QUOTE THEN Arg.Set G.quote ELSE arg_undefined "-q" END), help_q);
      ("-r", Arg.String ((:=) G.root), help_r);
      ("-s", (IFDEF STAGE THEN Arg.Int ((:=) G.stage) ELSE arg_undefined "-s" END), help_s);
      ("-t", (IFDEF TYPE THEN Arg.Clear G.validate ELSE arg_undefined "-t" END), help_t);
      ("-u", Arg.Set G.si, help_u);
      ("-x", Arg.Clear G.restricted, help_x);
      ("-y", Arg.Set G.infinity, help_y);
      ("-0", (IFDEF PREPROCESS THEN Arg.Unit set_preprocess ELSE arg_undefined "-0" END), help_0);
      ("-1", Arg.Set streaming, help_1);      
   ] process_file help;
IFDEF LEXER AND MANAGER AND OBJECTS AND PARSER AND SUMMARY AND EXPAND AND QUOTE AND STAGE AND TYPE AND PREPROCESS THEN
   if false then ignore (arg_undefined "") (* invocation of arg_undefined to make the compiler happy *)
ELSE () END