X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2Ftest_parser.ml;h=22d5c09fff2b8f72ffce424d4cce1fa8b9674f8d;hb=619a3a478a4f6b0a50782b620009f6a141c30a53;hp=0ff7c558e119e3435d461e382998e727d5cbe1e0;hpb=256ea270b884864d0eddd1de66bae2a2cbc513ff;p=helm.git diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index 0ff7c558e..22d5c09ff 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,105 +36,130 @@ 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 - let markup = CicNotationPres.render id_to_uri t in - Xml.pp_to_outchan (xml_stream_of_markup markup) oc; + Xml.pp_to_outchan (CicNotationPres.render_to_boxml id_to_uri t) oc; close_out oc -let _ = +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 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 -> - prerr_endline "===="; - print_endline (CicNotationPp.pp_term t); flush stdout; - let t' = CicNotationRew.pp_ast t in - print_endline (CicNotationPp.pp_term t'); flush stdout; + 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" - | P.Notation (l1, associativity, precedence, l2) -> - print_endline "Extending parser ..."; flush stdout; - let time1 = Unix.gettimeofday () in - ignore - (CicNotationParser.extend l1 ?precedence ?associativity - (fun env loc -> CicNotationFwd.instantiate_level2 env l2)); + 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 (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; - let time1 = 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 (_, 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 -> - 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 + 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 - printf "ast creation took %f seconds\n" (time2 -. time1); - prerr_endline "===="; - print_endline (CicNotationPp.pp_term t); flush stdout; + 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 - printf "pretty printing took %f seconds\n" (time4 -. time3); - dump_xml t id_to_uri "out.xml"; - print_endline (CicNotationPp.pp_term t'); flush stdout - ) -(* 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 "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)