X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2Ftest_parser.ml;h=1673db6f474a2ef1e7961bcc14ca4f6f39c99a45;hb=ba2dfe6409e95bf9e558dc0d4be382b068671409;hp=ce87368bf7ae54e8e937db11cbec27a37ba0caa9;hpb=5d5e328a05ed70fcf565aef8f92b7ec87b2740f2;p=helm.git diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index ce87368bf..1673db6f4 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -25,9 +25,7 @@ open Printf -let _ = - Helm_registry.load_from "test_parser.conf.xml" -(* Http_getter.init () *) +let _ = Helm_registry.load_from "test_parser.conf.xml" let xml_stream_of_markup = let rec print_box (t: CicNotationPres.boxml_markup) = @@ -38,7 +36,7 @@ let xml_stream_of_markup = print_mpres let dump_xml t id_to_uri fname = - print_endline (sprintf "dumping MathML to %s ..." 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; @@ -46,95 +44,84 @@ let dump_xml t id_to_uri fname = let _ = let module P = CicNotationPt in - let level = ref ~-1 in - let arg_spec = [ "-level", Arg.Set_int level, "set the notation level" ] in - let usage = "test_parser -level { 1 | 2 | 3 }" in - Arg.parse arg_spec (fun _ -> raise (Arg.Bad usage)) usage; - let ic = stdin in - try - printf "Parsing notation level %d\n" !level; flush stdout; - while true do - let line = input_line ic in - let istream = Stream.of_string line in - try - (match !level with - | -1 -> - (match CicNotationParser.parse_phrase istream with - | P.Print t -> + let arg_spec = [ ] in + let usage = "" in + Arg.parse arg_spec (fun _ -> raise (Arg.Bad usage)) usage; + try + let istream = Stream.of_channel stdin in + while Stream.peek istream <> None do + try + match CicNotationParser.parse_phrase istream with + | P.Print t -> prerr_endline "===="; - print_endline (CicNotationPp.pp_term t); flush stdout; + prerr_endline (CicNotationPp.pp_term t); flush stdout; let t' = CicNotationRew.pp_ast t in - print_endline (CicNotationPp.pp_term t'); flush stdout; - let tbl = Hashtbl.create 0 in - dump_xml t' tbl "out.xml" - | P.Notation (l1, associativity, precedence, l2) -> - print_endline "Extending parser ..."; flush stdout; + prerr_endline (CicNotationPp.pp_term t'); flush stdout; + let tbl = Hashtbl.create 0 in + dump_xml t' tbl "out.xml" + | P.Notation (l1, associativity, precedence, l2) -> + prerr_endline "Extending parser ..."; flush stdout; + prerr_endline (CicNotationPp.pp_term l1) ; + 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 - print_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 - | P.Interpretation (l2, l3) -> - print_endline "Adding interpretation ..."; flush stdout; + 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 + | P.Interpretation (l2, l3) -> + prerr_endline "Adding interpretation ..."; flush stdout; let time1 = Unix.gettimeofday () in - ignore (CicNotationRew.add_interpretation l2 l3); - let time2 = Unix.gettimeofday () in - printf "done (patterns compilation took %f seconds)\n" - (time2 -. time1); - flush stdout - | P.Render uri -> + ignore (CicNotationRew.add_interpretation l2 l3); + let time2 = Unix.gettimeofday () in + printf "done (patterns compilation took %f seconds)\n" + (time2 -. time1); + flush stdout + | P.Dump -> CicNotationParser.print_l2_pattern (); print_newline () + | P.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 + | 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") -(* CicNotationParser.print_l2_pattern ()) *) - | 1 -> ignore (CicNotationParser.parse_syntax_pattern istream) - | 2 -> - let ast = CicNotationParser.parse_ast_pattern istream in - if ast = P.Sort `Prop then - prerr_endline "eureka" - else - prerr_endline ":-(" - | 3 -> ignore (CicNotationParser.parse_interpretation istream) - | _ -> Arg.usage arg_spec usage; exit 1); - with 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) - done - with End_of_file -> - close_in ic - + 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" + (* 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) *) + with + | End_of_file -> raise End_of_file + | exn -> + prerr_endline + (sprintf "Uncaught exception: %s" (Printexc.to_string exn)) + done + with End_of_file -> + ()