X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2Ftest_parser.ml;h=b3685232e8e96e3a898e6a361bc9dd940cb63601;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=53ee4f8eb268a7c8f7829a637ab6e7a7e4dabb51;hpb=2007173e83a5001053c2946b59d6827cc080f1c4;p=helm.git diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index 53ee4f8eb..b3685232e 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -25,40 +25,137 @@ 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" + +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 + let markup = CicNotationPres.render id_to_uri t in + let xml_stream = CicNotationPres.print_xml markup in + Xml.pp_to_outchan xml_stream oc; + close_out oc + +let extract_loc = + function + | GrafiteAst.Executable (loc, _) + | GrafiteAst.Comment (loc, _) -> loc + +let pp_associativity = function + | Gramext.LeftA -> "left" + | Gramext.RightA -> "right" + | Gramext.NonA -> "non" + +let pp_precedence = string_of_int + +(* let last_rule_id = ref None *) + +let process_stream istream = + let char_count = ref 0 in + let module P = CicNotationPt in + let module G = GrafiteAst in + try + while true 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 (_, + P.AttributedTerm (_, P.Ident _)))) -> + prerr_endline "mega hack"; + (match !last_rule_id with + | None -> () + | Some id -> + prerr_endline "removing last notation rule ..."; + CicNotationParser.delete id) *) + | G.Executable (_, G.Macro (_, G.Check (_, t))) -> + prerr_endline (sprintf "ast: %s" (CicNotationPp.pp_term t)); + let t' = CicNotationRew.pp_ast t in + prerr_endline (sprintf "rendered ast: %s" + (CicNotationPp.pp_term t')); + let tbl = Hashtbl.create 0 in + dump_xml t' tbl "out.xml" + | G.Executable (_, G.Command (_, + G.Notation (_, dir, l1, associativity, precedence, l2))) -> + prerr_endline "notation"; + prerr_endline (sprintf "l1: %s" (CicNotationPp.pp_term l1)); + prerr_endline (sprintf "l2: %s" (CicNotationPp.pp_term l2)); + prerr_endline (sprintf "prec: %s" (pp_precedence precedence)); + prerr_endline (sprintf "assoc: %s" (pp_associativity associativity)); + let keywords = CicNotationUtil.keywords_of_term l1 in + if keywords <> [] then + prerr_endline (sprintf "keywords: %s" + (String.concat " " keywords)); + if dir <> Some `RightToLeft then + ignore + (CicNotationParser.extend l1 ?precedence ?associativity + (fun env loc -> CicNotationFwd.instantiate_level2 env l2)); +(* last_rule_id := Some rule_id; *) + if dir <> Some `LeftToRight then + ignore (CicNotationRew.add_pretty_printer + ?precedence ?associativity l2 l1) + | G.Executable (_, G.Command (_, G.Interpretation (_, id, l2, l3))) -> + prerr_endline "interpretation"; + prerr_endline (sprintf "dsc: %s" id); + ignore (CicNotationRew.add_interpretation id l2 l3); + 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 t, id_to_uri = + CicNotationRew.ast_of_acic id_to_sort annterm + in + prerr_endline "Raw AST"; + prerr_endline (CicNotationPp.pp_term t); + let t' = CicNotationRew.pp_ast t in + prerr_endline "Rendered AST"; + 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) + | exn -> + prerr_endline + (sprintf "Uncaught exception: %s" (Printexc.to_string exn)) + done + with End_of_file -> () let _ = - 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 arg_spec = [ ] in + let usage = "" in Arg.parse arg_spec (fun _ -> raise (Arg.Bad usage)) usage; - let parse_fun = - match !level with - | 1 -> CicNotationParser.parse_syntax_pattern - | 2 -> CicNotationParser.parse_ast_pattern - | 3 -> CicNotationParser.parse_interpretation - | _ -> Arg.usage arg_spec usage; exit 1 - in - 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 - let _ = parse_fun istream in - print_endline "ok" - with CicNotationParser.Parse_error (floc, msg) -> - let (x, y) = 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 ..."; + CicNotation.load_notation (Helm_registry.get "notation.core_file"); + print_endline "done."; + flush stdout; + process_stream (Ulexing.from_utf8_channel stdin)