]> matita.cs.unibo.it Git - helm.git/blob - components/grafite_parser/test_parser.ml
Up to absolute value
[helm.git] / components / grafite_parser / test_parser.ml
1 (* Copyright (C) 2005, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 (* $Id$ *)
27
28 open Printf
29
30 let _ = Helm_registry.load_from "test_parser.conf.xml"
31
32 let xml_stream_of_markup =
33   let rec print_box (t: CicNotationPres.boxml_markup) =
34     Box.box2xml print_mpres t
35   and print_mpres (t: CicNotationPres.mathml_markup) =
36     Mpresentation.print_mpres print_box t
37   in
38   print_mpres
39
40 let dump_xml t id_to_uri fname =
41   prerr_endline (sprintf "dumping MathML to %s ..." fname);
42   flush stdout;
43   let oc = open_out fname in
44   let markup = CicNotationPres.render id_to_uri t in
45   let xml_stream = CicNotationPres.print_xml markup in
46   Xml.pp_to_outchan xml_stream oc;
47   close_out oc
48
49 let extract_loc =
50   function
51     | GrafiteAst.Executable (loc, _)
52     | GrafiteAst.Comment (loc, _) -> loc
53
54 let pp_associativity = function
55   | Gramext.LeftA -> "left"
56   | Gramext.RightA -> "right"
57   | Gramext.NonA -> "non"
58
59 let pp_precedence = string_of_int
60
61 (* let last_rule_id = ref None *)
62
63 let process_stream istream =
64   let char_count = ref 0 in
65   let module P = CicNotationPt in
66   let module G = GrafiteAst in
67   let status =
68    ref
69     (CicNotation2.load_notation
70       ~include_paths:[] (Helm_registry.get "notation.core_file"))
71   in
72     try
73       while true do
74         try
75          match
76           GrafiteParser.parse_statement ~include_paths:[] istream !status
77          with
78             newstatus, GrafiteParser.LNone _ -> status := newstatus
79           | newstatus, GrafiteParser.LSome statement ->
80               status := newstatus;
81               let floc = extract_loc statement in
82               let (_, y) = HExtlib.loc_of_floc floc in
83               char_count := y + !char_count;
84               match statement with
85     (*           | G.Executable (_, G.Macro (_, G.Check (_,
86                 P.AttributedTerm (_, P.Ident _)))) -> 
87                   prerr_endline "mega hack";
88                   (match !last_rule_id with
89                   | None -> ()
90                   | Some id ->
91                       prerr_endline "removing last notation rule ...";
92                       CicNotationParser.delete id) *)
93               | G.Executable (_, G.Macro (_, G.Check (_, t))) -> 
94                   prerr_endline (sprintf "ast: %s" (CicNotationPp.pp_term t));
95                   let t' = TermContentPres.pp_ast t in
96                   prerr_endline (sprintf "rendered ast: %s"
97                     (CicNotationPp.pp_term t'));
98                   let tbl = Hashtbl.create 0 in
99                   dump_xml t' tbl "out.xml"
100               | statement ->
101                   prerr_endline
102                    ("Unsupported statement: " ^
103                      GrafiteAstPp.pp_statement
104                       ~term_pp:CicNotationPp.pp_term
105                       ~lazy_term_pp:(fun _ -> "_lazy_term_here_")
106                       ~obj_pp:(fun _ -> "_obj_here_")
107                       statement)
108         with
109         | End_of_file -> raise End_of_file
110         | HExtlib.Localized (floc,CicNotationParser.Parse_error msg) ->
111             let (x, y) = HExtlib.loc_of_floc floc in
112 (*             let before = String.sub line 0 x in
113             let error = String.sub line x (y - x) in
114             let after = String.sub line y (String.length line - y) in
115             eprintf "%s\e[01;31m%s\e[00m%s\n" before error after;
116             prerr_endline (sprintf "at character %d-%d: %s" x y msg) *)
117             prerr_endline (sprintf "Parse error at character %d-%d: %s"
118               (!char_count + x) (!char_count + y) msg)
119         | exn ->
120             prerr_endline
121               (sprintf "Uncaught exception: %s" (Printexc.to_string exn))
122         done
123     with End_of_file -> ()
124
125 let _ =
126   let arg_spec = [ ] in
127   let usage = "" in
128   Arg.parse arg_spec (fun _ -> raise (Arg.Bad usage)) usage;
129   print_endline "Loading builtin notation ...";
130   print_endline "done.";
131   flush stdout;
132   process_stream (Ulexing.from_utf8_channel stdin)
133