+ (match !level with
+ | -1 ->
+ (match CicNotationParser.parse_phrase istream with
+ | P.Print t ->
+ print_endline (CicNotationPp.pp_term t); flush stdout
+ | P.Notation (l1, associativity, precedence, l2) ->
+ print_endline "Extending notation ..."; flush stdout;
+ ignore
+ (CicNotationParser.extend l1 ?precedence ?associativity
+ (fun env loc ->
+ prerr_endline "ENV";
+ prerr_endline (CicNotationPp.pp_env env);
+ CicNotationFwd.instantiate_level2 env l2))
+ | P.Interpretation (l2, l3) ->
+ print_endline "Adding interpretation ..."; flush stdout;
+ let time1 = Unix.gettimeofday () in
+ ignore (CicNotationRew.add_interpretation l2 l3);
+ let time2 = Unix.gettimeofday () in
+ printf "done (patterns compilation took %f seconds)\n"
+ (time2 -. time1);
+ flush stdout
+ | P.Render uri ->
+ let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let annobj, _, _, id_to_sort, _, _, _ =
+ Cic2acic.acic_object_of_cic_object obj
+ in
+ let annterm =
+ match annobj with
+ | Cic.AConstant (_, _, _, _, ty, _, _)
+ | Cic.AVariable (_, _, _, ty, _, _) -> ty
+ | _ -> assert false
+ in
+ let time1 = Unix.gettimeofday () in
+ let t, id_to_uri =
+ CicNotationRew.ast_of_acic id_to_sort annterm
+ in
+ let time2 = Unix.gettimeofday () in
+ printf "ast creation took %f seconds\n" (time2 -. time1);
+ print_endline (CicNotationPp.pp_term t); flush stdout)
+(* CicNotationParser.print_l2_pattern ()) *)
+ | 1 -> ignore (CicNotationParser.parse_syntax_pattern istream)
+ | 2 ->
+ let ast = CicNotationParser.parse_ast_pattern istream in
+ if ast = P.Sort `Prop then
+ prerr_endline "eureka"
+ else
+ prerr_endline ":-("
+ | 3 -> ignore (CicNotationParser.parse_interpretation istream)
+ | _ -> Arg.usage arg_spec usage; exit 1);