*)
let _ =
- let level = ref ~-1 in
+ let level = ref "2@" in
let ic = ref stdin in
- let arg_spec = [] in
- let usage = "test_lexer [ 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
in
Arg.parse arg_spec open_file usage;
- let lexer = CicNotationLexer.notation_lexer in
+ let lexer =
+ match !level with
+ "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;
+ 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;