(* Copyright (C) 2005, 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 let _ = Helm_registry.load_from "test_parser.conf.xml" let xml_stream_of_markup = let rec print_box (t: CicNotationPres.boxml_markup) = Box.box2xml print_mpres t and print_mpres (t: CicNotationPres.mathml_markup) = Mpresentation.print_mpres print_box t in print_mpres let dump_xml t id_to_uri fname = prerr_endline (sprintf "dumping MathML to %s ..." fname); flush stdout; let oc = open_out fname in Xml.pp_to_outchan (CicNotationPres.render_to_boxml id_to_uri t) oc; close_out oc let extract_loc = function | GrafiteAst.Executable (loc, _) | GrafiteAst.Comment (loc, _) -> loc let errquit ignore_exn = if not ignore_exn then begin prerr_endline "Error, exiting!"; exit 2 end let process_stream ?(ignore_exn = false) istream = let char_count = ref 0 in let module P = CicNotationPt in let module G = GrafiteAst in try while Stream.peek istream <> None do try let statement = GrafiteParser.parse_statement istream in let floc = extract_loc statement in let (_, y) = P.loc_of_floc floc in char_count := y + !char_count; match statement with | G.Executable (_, G.Macro (_, G.Check (_, t))) -> prerr_endline "===="; prerr_endline (CicNotationPp.pp_term t); flush stdout; let t' = CicNotationRew.pp_ast t in prerr_endline (CicNotationPp.pp_term t'); flush stdout; let tbl = Hashtbl.create 0 in dump_xml t' tbl "out.xml" | G.Executable (_, G.Command (_, G.Notation (_, l1, associativity, precedence, l2))) -> prerr_endline "Extending parser ..."; flush stdout; prerr_endline (CicNotationPp.pp_term l1) ; prerr_endline (CicNotationPp.pp_term l2) ; prerr_endline (sprintf "Found keywords: %s" (String.concat " " (CicNotationUtil.keywords_of_term l1))); let time1 = Unix.gettimeofday () in ignore (CicNotationParser.extend l1 ?precedence ?associativity (fun env loc -> CicNotationFwd.instantiate_level2 env l2)); let time2 = Unix.gettimeofday () in prerr_endline "Extending pretty printer ..."; flush stdout; let time3 = Unix.gettimeofday () in ignore (CicNotationRew.add_pretty_printer ?precedence ?associativity l2 l1); let time4 = Unix.gettimeofday () in printf ("done (extending parser took %f, " ^^ "extending pretty printer took %f)\n") (time2 -. time1) (time4 -. time3); flush stdout | G.Executable (_, G.Command (_, G.Interpretation (_, id, l2, l3))) -> prerr_endline "Adding interpretation ..."; flush stdout; let time1 = Unix.gettimeofday () in ignore (CicNotationRew.add_interpretation id l2 l3); let time2 = Unix.gettimeofday () in printf "done (patterns compilation took %f seconds)\n" (time2 -. time1); flush stdout | G.Executable (_, G.Command (_, G.Dump _)) -> CicNotationParser.print_l2_pattern (); print_newline () | G.Executable (_, G.Command (_, G.Render (_, uri))) -> let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in let annobj, _, _, id_to_sort, _, _, _ = Cic2acic.acic_object_of_cic_object obj in let annterm = match annobj with | Cic.AConstant (_, _, _, _, ty, _, _) | Cic.AVariable (_, _, _, ty, _, _) -> ty | _ -> assert false in let time1 = Unix.gettimeofday () in let t, id_to_uri = CicNotationRew.ast_of_acic id_to_sort annterm in let time2 = Unix.gettimeofday () in prerr_endline (sprintf "ast creation took %f seconds\n" (time2 -. time1)); prerr_endline "AST"; prerr_endline (CicNotationPp.pp_term t); flush stdout; let time3 = Unix.gettimeofday () in let t' = CicNotationRew.pp_ast t in let time4 = Unix.gettimeofday () in prerr_endline (sprintf "pretty printing took %f seconds\n" (time4 -. time3)); prerr_endline (CicNotationPp.pp_term t'); dump_xml t' id_to_uri "out.xml" | _ -> prerr_endline "Unsupported statement" with | End_of_file -> raise End_of_file | CicNotationParser.Parse_error (floc, msg) -> let (x, y) = P.loc_of_floc floc in (* let before = String.sub line 0 x in let error = String.sub line x (y - x) in let after = String.sub line y (String.length line - y) in eprintf "%s%s%s\n" before error after; prerr_endline (sprintf "at character %d-%d: %s" x y msg) *) prerr_endline (sprintf "Parse error at character %d-%d: %s" (!char_count + x) (!char_count + y) msg); errquit ignore_exn | exn -> prerr_endline (sprintf "Uncaught exception: %s" (Printexc.to_string exn)); errquit ignore_exn done with End_of_file -> () let _ = let arg_spec = [ ] in let usage = "" in Arg.parse arg_spec (fun _ -> raise (Arg.Bad usage)) usage; print_endline "Loading builtin notation ..."; let ic = open_in (Helm_registry.get "notation.core_file") in process_stream ~ignore_exn:true (Stream.of_channel ic); close_in ic; print_endline "done."; flush stdout; process_stream ~ignore_exn:false (Stream.of_channel stdin)