X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2Ftest_parser.ml;h=62b0ae32bd585ca0551ca1e3d4d851ddf85b05c5;hb=cd602bc57c4ceba6188b4cac0dbf5dad8f5df7b6;hp=d39c0ff94d86526e84e206dba739b38655e9480f;hpb=e9cfecee7dd7cf8388512ffd4aa223782c728eda;p=helm.git diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index d39c0ff94..62b0ae32b 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -25,85 +25,142 @@ open Printf -let _ = +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 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 + 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; - if !level = 2 then begin - let id = - CicNotationParser.extend ~precedence:50 ~associativity:Gramext.LeftA - (P.Layout (P.Box (P.H, - [ - P.Magic - (P.List1 - (P.Layout (P.Box (P.H, - [ P.Literal (`Symbol "|"); - P.Variable (P.TermVar "ugo"); - P.Magic (P.Opt (P.Layout (P.Box (P.H, - [ P.Literal (`Symbol ","); - P.Variable (P.TermVar "pino")])))); - P.Literal (`Symbol "|"); - ])), - Some (`Symbol ";"))); -(* P.Literal (`Symbol "+"); - P.Magic (P.Opt (P.Layout (P.Box (P.H, - [ - P.Variable (P.TermVar "ugo"); - P.Literal (`Symbol "+"); - P.Variable (P.TermVar "pino") - ])))); *) -(* P.Variable (P.TermVar "a"); - P.Literal (`Symbol "+"); - P.Variable (P.TermVar "b"); *) - ]))) - (fun env _ -> - prerr_endline "reducing rule" ; - prerr_endline (sprintf "env = [ %s ]" (CicNotationPp.pp_env env)); - P.Sort `Prop) - in - CicNotationParser.print_l2_pattern () - end; - 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 -> - print_endline (CicNotationPp.pp_term t); flush stdout - | P.Notation (l1, associativity, precedence, l2) -> - prerr_endline "foo"; - print_endline "Extending notation ..."; flush stdout; - ignore - (CicNotationParser.extend l1 ?precedence ?associativity - (fun env loc -> - prerr_endline "ENV"; - prerr_endline (CicNotationPp.pp_env env); - CicNotationSubst.instantiate_level2 env l2))) -(* 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 + 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)