Huge reorganization of matita and ocaml.

[helm.git] / helm / ocaml / grafite_parser / test_parser.ml

diff --git a/helm/ocaml/grafite_parser/test_parser.ml b/helm/ocaml/grafite_parser/test_parser.ml
index 76463f81441a1b952fad20c4b5f14df40cf68d3e..3b5c8f3751a986865747fe41056a4e34f99dc8ab 100644 (file)
--- a/helm/ocaml/grafite_parser/test_parser.ml
+++ b/helm/ocaml/grafite_parser/test_parser.ml
@@ -62,76 +62,47 @@ let process_stream istream =
   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) ->
@@ -154,7 +125,6 @@ let _ =
   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)