X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2Ftest_parser.ml;h=1585f43e28df6f1da4f06bee1e2be4bb2dcd943f;hb=3d63cb9ed38f05c679fc3284a5b3bb4d92e52296;hp=a8e2c45b0c6231901e2ce4fe131146609ad7cfd8;hpb=29aacd800408d16b9cb58dd58e603e31aa2ad511;p=helm.git diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index a8e2c45b0..1585f43e2 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -25,10 +25,24 @@ open Printf -(* cut and past from CicAst.loc_of_floc *) -let loc_of_floc = function - | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } -> - (loc_begin, loc_end) +let _ = + Helm_registry.load_from "test_parser.conf.xml" +(* Http_getter.init () *) + +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 = + print_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 _ = let module P = CicNotationPt in @@ -36,53 +50,6 @@ let _ = 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; - if !level = 2 then begin - let id = - CicNotationParser.extend ~precedence:50 ~associativity:Gramext.LeftA - (P.Layout (P.Box (P.H, - [ 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 _ -> - begin - prerr_endline "reducing rule" ; - prerr_endline (sprintf "env = [ %s ]" (CicNotationParser.pp_env env)); -(* match env with - [(_, (_, P.OptValue v))] -> - begin - match v with - | Some x -> - printf "Ugo c'e'? %s\n" (CicNotationParser.pp_value x); - flush stdout - | None -> prerr_endline "nooooo" - end - | _ -> assert false *) - end ; - P.Sort `Prop) - in - CicNotationParser.print_l2_pattern () - end; - let parse_fun s = - match !level with - | 1 -> ignore (CicNotationParser.parse_syntax_pattern s) - | 2 -> - let ast = CicNotationParser.parse_ast_pattern s in - if ast = P.Sort `Prop then - prerr_endline "eureka (ma sono cazzi)" - else - prerr_endline ":-(" - | 3 -> ignore (CicNotationParser.parse_interpretation s) - | _ -> Arg.usage arg_spec usage; exit 1 - in let ic = stdin in try printf "Parsing notation level %d\n" !level; flush stdout; @@ -90,10 +57,79 @@ let _ = let line = input_line ic in let istream = Stream.of_string line in try - parse_fun istream; - print_endline ">" + (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 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)); + 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 + 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 + | 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; + 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) = loc_of_floc floc in + 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