(loc_begin, loc_end)
let _ =
+ 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;
- let parse_fun =
+ 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 -> CicNotationParser.parse_syntax_pattern
- | 2 -> CicNotationParser.parse_ast_pattern
- | 3 -> CicNotationParser.parse_interpretation
+ | 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
let line = input_line ic in
let istream = Stream.of_string line in
try
- let _ = parse_fun istream in
- print_endline "ok"
+ 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