+type input = Text | Automath
+
+type input_entity = TxtEntity of Txt.command
+ | AutEntity of Aut.command
+
+let type_of_input name =
+ if F.check_suffix name ".hln" then Text
+ else if F.check_suffix name ".aut" then
+ let _ = H.set_sorts 0 ["Set"; "Prop"] in
+ assert (H.set_graph "Z2");
+ Automath
+ else begin
+ L.warn (P.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
+ | Text, [] ->
+ begin match TxtParser.entry (token txt_xl) lexbuf with
+ | Some e, unget -> txt_xl.unget <- unget; Some (TxtEntity e)
+ | None, _ -> None
+ end
+ | Text, hd :: tl ->
+ parbuf := tl; Some hd
+ | Automath, _ ->
+ begin match AutParser.entry (token aut_xl) lexbuf with
+ | Some e, unget -> aut_xl.unget <- unget; Some (AutEntity e)
+ | None, _ -> None
+ end
+
+let process_input f st = function
+ | AutEntity e ->
+ let f ast e = f {st with ast = ast} (AutEntity e) in
+ AP.process_command f st.ast e
+ | xe -> f st xe
+
+let count_input st = function
+ | AutEntity e -> {st with ac = AO.count_command C.start st.ac e}
+ | xe -> st
+
+(****************************************************************************)
+
+let stage = ref 3
+let moch = ref None
+let meta = ref false
+let progress = ref false
+let preprocess = ref false
+let root = ref ""
+let cc = ref false
+let export = ref ""
+let old = ref false
+let st = ref (initial_status ())
+
+let process_2 st entity =
+ let st = if !L.level > 2 then count_entity st entity else st in
+ if !export <> "" then export_entity !O.si !export !moch entity;
+ if !stage > 2 then type_check st entity else st
+
+let process_1 st entity =
+ if !progress then pp_progress entity;
+ let st = if !L.level > 2 then count_entity st entity else st in
+ if !export <> "" && !stage = 1 then export_entity !O.si !export !moch entity;
+ if !stage > 1 then process_2 st (xlate_entity entity) else st
+
+let process_0 st entity =
+ let f st entity =
+ if !stage = 0 then st else
+ let frr mst = {st with mst = mst} in
+ let h mst e = process_1 {st with mst = mst} (MetaEntity e) in
+ let err dst = {st with dst = dst} in
+ let g dst e = process_1 {st with dst = dst} (CrgEntity e) in
+ let crr tst = {st with tst = tst} in
+ let d tst e = process_1 {st with tst = tst} (CrgEntity e) in
+ match entity, !old with
+ | AutEntity e, true -> MA.meta_of_aut frr h st.mst e
+ | AutEntity e, false -> DA.crg_of_aut err g st.dst e
+ | TxtEntity e, false -> DT.crg_of_txt crr d gen_text st.tst e
+ | _ -> assert false
+ in
+ let st = if !L.level > 2 then count_input st entity else st in
+ if !preprocess then process_input f st entity else f st entity
+
+let process st name =
+ let input = type_of_input name in
+ let ich = open_in name in
+ let lexbuf = Lexing.from_channel ich in
+ let rec aux st = match entity_of_input lexbuf input with
+ | None -> close_in ich; st, input
+ | Some e -> aux (process_0 st e)
+ in
+ aux st