snapshot (first version with working pattern matching both 3->2 and 2->1)

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

diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml
index 5b42822c22b218d2495b4f32fe9d038f8a113ff3..77135a977d04778312c676faf984ff0beddfa04a 100644 (file)
--- a/helm/ocaml/cic_notation/test_parser.ml
+++ b/helm/ocaml/cic_notation/test_parser.ml
@@ -103,14 +103,13 @@ let _ =
             | P.Interpretation (l2, l3) ->
                 print_endline "Adding interpretation ..."; flush stdout;
                 let time1 = Unix.gettimeofday () in
-(*                 ignore (CicNotationRew.add_interpretation l2 l3); *)
+                ignore (CicNotationRew.add_interpretation l2 l3);
                 let time2 = Unix.gettimeofday () in
                 printf "done (patterns compilation took %f seconds)\n"
                   (time2 -. time1);
                 flush stdout
             | P.Render uri ->
-                assert false
-(*                 let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
                 let annobj, _, _, id_to_sort, _, _, _ =
                   Cic2acic.acic_object_of_cic_object obj
                 in
@@ -133,7 +132,7 @@ 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)