open Printf
+(* cut and past from CicAst.loc_of_floc *)
+let loc_of_floc = function
+ | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } ->
+ (loc_begin, loc_end)
+
let _ =
- let ic = stdin in
- try
- while true do
- let line = input_line ic in
- let istream = Stream.of_string line in
- try
- let _ = CicNotationParser.parse_level1_pattern istream in
- print_endline "ok"
- with
- | CicNotationParser.Parse_error (floc, msg) ->
- eprintf "parse error: %s\n" msg; flush stderr
-(* let (x, y) = CicAst.loc_of_floc floc in*)
-(* let before = String.sub line 0 x in*)
-(* let error = String.sub line x (y - x) in*)
-(* let after = String.sub line y (String.length line - y) in*)
-(* eprintf "%s\e[01;31m%s\e[00m%s\n" before error after;*)
-(* prerr_endline (sprintf "at character %d-%d: %s" x y msg)*)
- done
- with End_of_file ->
- close_in ic
+ let module P = CicNotationPt in
+ let level = ref ~-1 in
+ 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.List0
+ (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 ]" (CicNotationParser.pp_env env));
+ P.Sort `Prop)
+ in
+ CicNotationParser.print_l2_pattern ()
+ end;
+ let parse_fun s =
+ match !level with
+ | 1 -> ignore (CicNotationParser.parse_syntax_pattern s)
+ | 2 ->
+ let ast = CicNotationParser.parse_ast_pattern s in
+ if ast = P.Sort `Prop then
+ prerr_endline "eureka (ma sono cazzi)"
+ else
+ prerr_endline ":-("
+ | 3 -> ignore (CicNotationParser.parse_interpretation s)
+ | _ -> Arg.usage arg_spec usage; exit 1
+ in
+ let ic = stdin in
+ try
+ printf "Parsing notation level %d\n" !level; flush stdout;
+ while true do
+ let line = input_line ic in
+ let istream = Stream.of_string line in
+ try
+ parse_fun istream;
+ print_endline ">"
+ with CicNotationParser.Parse_error (floc, msg) ->
+ let (x, y) = loc_of_floc floc in
+ let before = String.sub line 0 x in
+ let error = String.sub line x (y - x) in
+ let after = String.sub line y (String.length line - y) in
+ eprintf "%s\e[01;31m%s\e[00m%s\n" before error after;
+ prerr_endline (sprintf "at character %d-%d: %s" x y msg)
+ done
+ with End_of_file ->
+ close_in ic