]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/test_lexer.ml
ocaml 3.09 transition
[helm.git] / helm / ocaml / cic_notation / test_lexer.ml
index b41f7f6b8e34355f31d290840eb497b95fae9dba..569e86e442ae20383cb7b63a6ce1769391f1fa23 100644 (file)
  *)
 
 let _ =
-  let level = ref ~-1 in
+  let level = ref "2@" in
   let ic = ref stdin in
-  let arg_spec = [ "-level", Arg.Set_int level, "set the notation level" ] in
-  let usage = "test_lexer -level { 1 | 2 | 3 } [ file ]" in
+  let arg_spec = [ "-level", Arg.Set_string level, "set the notation level" ] in
+  let usage = "test_lexer [ -level level ] [ file ]" in
   let open_file fname =
     if !ic <> stdin then close_in !ic;
     ic := open_in fname
@@ -35,12 +35,17 @@ let _ =
   Arg.parse arg_spec open_file usage;
   let lexer =
     match !level with
-    | 1 -> CicNotationLexer.syntax_pattern_lexer
-    | 2 -> CicNotationLexer.ast_pattern_lexer
-    | _ -> Arg.usage arg_spec usage; exit 1
+       "1" -> CicNotationLexer.level1_pattern_lexer
+      | "2@" -> CicNotationLexer.level2_ast_lexer
+      | "2$" -> CicNotationLexer.level2_meta_lexer
+      | l ->
+         prerr_endline (Printf.sprintf "Unsupported level %s" l);
+         exit 2
   in
-  let token_stream = fst (lexer.Token.tok_func (Stream.of_channel !ic)) in
-  Printf.printf "Lexing notation level %d\n" !level; flush stdout;
+  let token_stream =
+    fst (lexer.Token.tok_func (Obj.magic (Ulexing.from_utf8_channel !ic)))
+  in
+  Printf.printf "Lexing notation level %s\n" !level; flush stdout;
   let rec dump () =
     let (a,b) = Stream.next token_stream in
     if a = "EOI" then raise Stream.Failure;