X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2Ftest_parser.ml;h=58880b9d5b781279600bda07825dbb2cb652742d;hb=bb49c457d64878ed9611656f620548b5151e5dbd;hp=722748a96c42f896d05fce32147707017d4a723e;hpb=dbcc29c0e46454c7e31b485135900ceab38627e1;p=helm.git

diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml
index 722748a96..58880b9d5 100644
--- a/helm/ocaml/cic_notation/test_parser.ml
+++ b/helm/ocaml/cic_notation/test_parser.ml
@@ -26,8 +26,8 @@
 open Printf
 
 let _ =
-  Helm_registry.load_from "test_parser.conf.xml";
-  Http_getter.init ()
+  Helm_registry.load_from "test_parser.conf.xml"
+(*   Http_getter.init () *)
 
 let _ =
   let module P = CicNotationPt in
@@ -35,40 +35,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.Magic
-              (P.List1
-                (P.Layout (P.Box (P.H,
-                  [ P.Literal (`Symbol "|");
-                    P.Variable (P.TermVar "ugo");
-                    P.Magic (P.Opt (P.Layout (P.Box (P.H,
-                      [ P.Literal (`Symbol ",");
-                        P.Variable (P.TermVar "pino")]))));
-                    P.Literal (`Symbol "|");
-                  ])),
-                  Some (`Symbol ";")));
-(*             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 _ ->
-          prerr_endline "reducing rule" ;
-          prerr_endline (sprintf "env = [ %s ]" (CicNotationPp.pp_env env));
-          P.Sort `Prop)
-    in
-    CicNotationParser.print_l2_pattern ()
-  end;
   let ic = stdin in
   try
     printf "Parsing notation level %d\n" !level; flush stdout;
@@ -89,10 +55,7 @@ let _ =
                 let time1 = Unix.gettimeofday () in
                 ignore
                   (CicNotationParser.extend l1 ?precedence ?associativity
-                    (fun env loc ->
-                      prerr_endline "ENV";
-                      prerr_endline (CicNotationPp.pp_env env);
-                      CicNotationFwd.instantiate_level2 env l2));
+                    (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
@@ -135,7 +98,8 @@ let _ =
                 let t' = CicNotationRew.pp_ast t in
                 let time4 = Unix.gettimeofday () in
                 printf "pretty printing took %f seconds\n" (time4 -. time3);
-                print_endline (CicNotationPp.pp_term t'); flush stdout)
+                print_endline (CicNotationPp.pp_term t'); flush stdout
+                )
 (*                 CicNotationParser.print_l2_pattern ()) *)
         | 1 -> ignore (CicNotationParser.parse_syntax_pattern istream)
         | 2 ->