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=df94eaa6f3c320e38cacfc4cfcb6725d22bda50b;hpb=e20f3963028a966fc93ba0d611c4aa8341d20e2c;p=helm.git diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index df94eaa6f..b3685232e 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -39,7 +39,9 @@ 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; + 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 = @@ -47,58 +49,66 @@ let extract_loc = | 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 pp_associativity = function + | Gramext.LeftA -> "left" + | Gramext.RightA -> "right" + | Gramext.NonA -> "non" -let process_stream ?(ignore_exn = false) istream = +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 Stream.peek istream <> None do + 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 "===="; - prerr_endline (CicNotationPp.pp_term t); flush stdout; + prerr_endline (sprintf "ast: %s" (CicNotationPp.pp_term t)); 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" + 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 (_, 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 - 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.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 "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 + 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))) -> @@ -112,25 +122,16 @@ let process_stream ?(ignore_exn = false) istream = | 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" + 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) -> @@ -141,25 +142,20 @@ let process_stream ?(ignore_exn = false) istream = 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 + (!char_count + x) (!char_count + y) msg) | exn -> prerr_endline - (sprintf "Uncaught exception: %s" (Printexc.to_string exn)); - errquit ignore_exn + (sprintf "Uncaught exception: %s" (Printexc.to_string exn)) done - with End_of_file -> - () + 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; + CicNotation.load_notation (Helm_registry.get "notation.core_file"); print_endline "done."; flush stdout; - process_stream ~ignore_exn:false (Stream.of_channel stdin) + process_stream (Ulexing.from_utf8_channel stdin)