--- 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