* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
let _ = Helm_registry.load_from "test_parser.conf.xml"
let char_count = ref 0 in
let module P = CicNotationPt in
let module G = GrafiteAst in
+ let status =
+ ref
+ (CicNotation2.load_notation
+ ~include_paths:[] (Helm_registry.get "notation.core_file"))
+ in
try
while true do
try
- let statement = GrafiteParser.parse_statement istream in
- let floc = extract_loc statement in
- let (_, y) = HExtlib.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' = TermContentPres.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 -> TermContentPres.instantiate_level2 env l2));
-(* last_rule_id := Some rule_id; *)
- if dir <> Some `LeftToRight then
- ignore (TermContentPres.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 (TermAcicContent.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 =
- TermAcicContent.ast_of_acic id_to_sort annterm
- in
- prerr_endline "Raw AST";
- prerr_endline (CicNotationPp.pp_term t);
- let t' = TermContentPres.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"
+ match
+ GrafiteParser.parse_statement ~include_paths:[] istream !status
+ with
+ newstatus, GrafiteParser.LNone _ -> status := newstatus
+ | newstatus, GrafiteParser.LSome statement ->
+ status := newstatus;
+ let floc = extract_loc statement in
+ let (_, y) = HExtlib.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' = TermContentPres.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"
+ | statement ->
+ prerr_endline
+ ("Unsupported statement: " ^
+ GrafiteAstPp.pp_statement
+ ~term_pp:CicNotationPp.pp_term
+ ~lazy_term_pp:(fun _ -> "_lazy_term_here_")
+ ~obj_pp:(fun _ -> "_obj_here_")
+ statement)
with
| End_of_file -> raise End_of_file
| HExtlib.Localized (floc,CicNotationParser.Parse_error msg) ->
let usage = "" in
Arg.parse arg_spec (fun _ -> raise (Arg.Bad usage)) usage;
print_endline "Loading builtin notation ...";
- CicNotation2.load_notation (Helm_registry.get "notation.core_file");
print_endline "done.";
flush stdout;
process_stream (Ulexing.from_utf8_channel stdin)