- let parse_fun s =
- match !level with
- | 1 -> ignore (CicNotationParser.parse_syntax_pattern s)
- | 2 -> ignore (CicNotationParser.parse_ast_pattern s)
- | 3 -> ignore (CicNotationParser.parse_interpretation s)
- | _ -> Arg.usage arg_spec usage; exit 1
- in
+ if !level = 2 then begin
+ let id =
+ CicNotationParser.extend ~precedence:50 ~associativity:Gramext.LeftA
+ (P.Layout (P.Box (P.H,
+ [
+ P.Magic
+ (P.List1
+ (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 ]" (CicNotationPp.pp_env env));
+ P.Sort `Prop)
+ in
+ CicNotationParser.print_l2_pattern ()
+ end;