diff -r 7d01480cc8e3 -r 3c7c4372f9ad src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Oct 24 16:55:42 2009 +0200 @@ -4,7 +4,7 @@ signature PREDICATE_COMPILE = sig val setup : theory -> theory - val preprocess : string -> theory -> theory + val preprocess : Predicate_Compile_Aux.options -> string -> theory -> theory end; structure Predicate_Compile : PREDICATE_COMPILE = @@ -89,6 +89,8 @@ [] else [intro] +fun tracing s = () + fun print_intross thy msg intross = tracing (msg ^ (space_implode "; " (map @@ -98,13 +100,14 @@ map (fn (c, thms) => "Constant " ^ c ^ " has specification:\n" ^ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs -fun process_specification specs thy' = +fun process_specification options specs thy' = let - val specs = map (apsnd (map - (fn th => if is_equationlike th then Pred_Compile_Data.normalize_equation thy' th else th))) specs + val _ = print_step options "Compiling predicates to flat introrules..." + val specs = map (apsnd (map + (fn th => if is_equationlike th then Pred_Compile_Data.normalize_equation thy' th else th))) specs val (intross1, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess specs thy') val _ = print_intross thy'' "Flattened introduction rules: " intross1 - val _ = priority "Replacing functions in introrules..." + val _ = "Replacing functions in introrules..." val intross2 = if fail_safe_mode then case try (burrow (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross1 of @@ -112,77 +115,94 @@ | NONE => let val _ = warning "Function replacement failed!" in intross1 end else burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross1 val _ = print_intross thy'' "Introduction rules with replaced functions: " intross2 - val _ = priority "Introducing new constants for abstractions at higher-order argument positions..." + val _ = print_step options "Introducing new constants for abstractions at higher-order argument positions..." val (intross3, (new_defs, thy''')) = Predicate_Compile_Pred.flat_higher_order_arguments (intross2, thy'') - val _ = tracing ("Now derive introduction rules for new_defs: " - ^ space_implode "\n" - (map (fn (c, ths) => c ^ ": " ^ - commas (map (Display.string_of_thm_global thy''') ths)) new_defs)) - val (new_intross, thy'''') = if not (null new_defs) then - process_specification new_defs thy''' + val (new_intross, thy'''') = + if not (null new_defs) then + let + val _ = print_step options "Recursively obtaining introduction rules for new definitions..." + in process_specification options new_defs thy''' end else ([], thy''') in (intross3 @ new_intross, thy'''') end -fun preprocess_strong_conn_constnames gr constnames thy = +fun preprocess_strong_conn_constnames options gr constnames thy = let val get_specs = map (fn k => (k, Graph.get_node gr k)) - val _ = priority ("Preprocessing scc of " ^ commas constnames) + val _ = print_step options ("Preprocessing scc of " ^ commas constnames) val (prednames, funnames) = List.partition (is_pred thy) constnames (* untangle recursion by defining predicates for all functions *) - val _ = priority "Compiling functions to predicates..." - val _ = Output.tracing ("funnames: " ^ commas funnames) + val _ = print_step options + ("Compiling functions (" ^ commas funnames ^ ") to predicates...") val (fun_pred_specs, thy') = if not (null funnames) then Predicate_Compile_Fun.define_predicates (get_specs funnames) thy else ([], thy) val _ = print_specs thy' fun_pred_specs - val _ = priority "Compiling predicates to flat introrules..." val specs = (get_specs prednames) @ fun_pred_specs - val (intross3, thy''') = process_specification specs thy' + val (intross3, thy''') = process_specification options specs thy' val _ = print_intross thy''' "Introduction rules with new constants: " intross3 val intross4 = map (maps remove_pointless_clauses) intross3 val _ = print_intross thy''' "After removing pointless clauses: " intross4 val intross5 = burrow (map (AxClass.overload thy''')) intross4 val intross6 = burrow (map (simplify_fst_snd o expand_tuples thy''')) intross5 val _ = print_intross thy''' "introduction rules before registering: " intross6 - val _ = priority "Registering intro rules..." + val _ = print_step options "Registering introduction rules..." val thy'''' = fold Predicate_Compile_Core.register_intros intross6 thy''' in thy'''' end; -fun preprocess const thy = +fun preprocess options const thy = let - val _ = Output.tracing ("Fetching definitions from theory...") + val _ = print_step options "Fetching definitions from theory..." val table = Pred_Compile_Data.make_const_spec_table thy val gr = Pred_Compile_Data.obtain_specification_graph thy table const - val _ = Output.tracing (commas (Graph.all_succs gr [const])) val gr = Graph.subgraph (member (op =) (Graph.all_succs gr [const])) gr - in fold_rev (preprocess_strong_conn_constnames gr) + in fold_rev (preprocess_strong_conn_constnames options gr) (Graph.strong_conn gr) thy end -fun code_pred_cmd (((modes, inductify_all), rpred), raw_const) lthy = - if inductify_all then - let - val thy = ProofContext.theory_of lthy - val const = Code.read_const thy raw_const - val lthy' = LocalTheory.theory (preprocess const) lthy - |> LocalTheory.checkpoint - - val const = case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of - SOME c => c - | NONE => const - val _ = tracing "Starting Predicate Compile Core..." - in Predicate_Compile_Core.code_pred modes rpred const lthy' end - else - Predicate_Compile_Core.code_pred_cmd modes rpred raw_const lthy +fun extract_options ((modes, raw_options), raw_const) = + let + fun chk s = member (op =) raw_options s + in + Options { + show_steps = chk "show_steps", + show_mode_inference = chk "show_mode_inference", + inductify = chk "inductify", + rpred = chk "rpred" + } + end + +fun code_pred_cmd ((modes, raw_options), raw_const) lthy = + let + val options = extract_options ((modes, raw_options), raw_const) + in + if (is_inductify options) then + let + val thy = ProofContext.theory_of lthy + val const = Code.read_const thy raw_const + val lthy' = LocalTheory.theory (preprocess options const) lthy + |> LocalTheory.checkpoint + + val const = case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of + SOME c => c + | NONE => const + val _ = print_step options "Starting Predicate Compile Core..." + in + Predicate_Compile_Core.code_pred options modes (is_rpred options) const lthy' + end + else + Predicate_Compile_Core.code_pred_cmd options modes (is_rpred options) raw_const lthy + end val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup -val _ = List.app OuterKeyword.keyword ["inductify_all", "rpred", "mode"] +val bool_options = ["show_steps", "show_mode_inference", "inductify", "rpred"] + +val _ = List.app OuterKeyword.keyword ("mode" :: bool_options) local structure P = OuterParse in @@ -192,10 +212,17 @@ P.enum1 "," (P.$$$ "[" |-- P.enum "," P.nat --| P.$$$ "]") --| P.$$$ ")" >> SOME) NONE +val scan_params = + let + val scan_bool_param = foldl1 (op ||) (map P.$$$ bool_options) + in + Scan.optional (P.$$$ "[" |-- P.enum1 "," scan_bool_param --| P.$$$ "]") [] + end + val _ = OuterSyntax.local_theory_to_proof "code_pred" "prove equations for predicate specified by intro/elim rules" - OuterKeyword.thy_goal (opt_modes -- - P.opt_keyword "inductify_all" -- P.opt_keyword "rpred" -- P.term_group >> code_pred_cmd) + OuterKeyword.thy_goal (opt_modes -- scan_params -- P.term_group >> + code_pred_cmd) end