(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;
+ if !level = 2 then begin
+ let id =
+ CicNotationParser.extend ~precedence:50 ~associativity:Gramext.LeftA
+ (P.Layout (P.Box (P.H,
+ [ P.Literal (`Symbol "+");
+ P.Magic (P.Opt (P.Variable (P.TermVar "ugo"))) ]
+(* [ P.Variable (P.TermVar "a");
+ P.Literal (`Symbol "+");
+ P.Variable (P.TermVar "b");
+ ] *)
+ )))
+ (fun env _ ->
+ begin
+ prerr_endline "reducing rule" ;
+ prerr_endline (sprintf "env = [ %s ]" (CicNotationParser.pp_env env));
+(* match env with
+ [(x, (_, P.OptValue v))] ->
+ begin
+ match v with
+ Some _ -> Printf.printf "Ugo c'e'? %s\n" x; flush stdout
+ | None -> prerr_endline "nooooo"
+ end
+ | _ -> assert false *)
+ end ;
+ P.Sort `Prop)
+ in
+ CicNotationParser.print_l2_pattern ()
+ end;
let parse_fun s =
match !level with
| 1 -> ignore (CicNotationParser.parse_syntax_pattern s)
- | 2 -> ignore (CicNotationParser.parse_ast_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 istream = Stream.of_string line in
try
parse_fun istream;
- print_endline "ok"
+ print_endline ">"
with CicNotationParser.Parse_error (floc, msg) ->
let (x, y) = loc_of_floc floc in
let before = String.sub line 0 x in