--- a/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML Sat Oct 24 16:55:42 2009 +0200
@@ -69,11 +69,14 @@
in ((ps', t''), nctxt') end;
+(* introduction rule combinators *)
+(* combinators to apply a function to all literals of an introduction rules *)
(*
fun map_atoms f intro =
*)
+
fun fold_atoms f intro s =
let
val (literals, head) = Logic.strip_horn intro
@@ -103,5 +106,35 @@
| _ => error "equals_conv"
*)
+(* Different options for compiler *)
+
+datatype options = Options of {
+ (*check_modes : (string * int list list) list,*)
+ show_steps : bool,
+ show_mode_inference : bool,
+
+ (*
+ inductify_functions : bool,
+ *)
+ inductify : bool,
+ rpred : bool
+};
+
+fun is_show_steps (Options opt) = #show_steps opt
+fun is_inductify (Options opt) = #inductify opt
+fun is_rpred (Options opt) = #rpred opt
+
+
+val default_options = Options {
+ show_steps = false,
+ show_mode_inference = false,
+ inductify = false,
+ rpred = false
+}
+
+
+fun print_step options s =
+ if is_show_steps options then tracing s else ()
+
end;
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML Sat Oct 24 16:55:42 2009 +0200
@@ -136,7 +136,6 @@
val (const, th) =
if is_equationlike th then
let
- val _ = priority "Normalizing definition..."
val eq = normalize_equation thy th
in
(defining_const_of_equation eq, eq)
@@ -149,18 +148,6 @@
else I
end
-(*
-fun make_const_spec_table_warning thy =
- fold
- (fn th => fn thy => case try (store_thm th) thy of
- SOME thy => thy
- | NONE => (warning ("store_thm fails for " ^ Display.string_of_thm_global thy th) ; thy))
- (Predicate_Compile_Preproc_Const_Defs.get (ProofContext.init thy)) thy
-
-fun make_const_spec_table thy =
- fold store_thm (Predicate_Compile_Preproc_Const_Defs.get (ProofContext.init thy)) thy
- |> (fn thy => fold store_thm (Nitpick_Const_Simps.get (ProofContext.init thy)) thy)
-*)
fun make_const_spec_table thy =
let
fun store ignore_const f = fold (store_thm_in_table ignore_const thy) (map (Thm.transfer thy) (f (ProofContext.init thy)))
@@ -173,23 +160,15 @@
|> store ignore_consts Nitpick_Const_Simps.get
|> store ignore_consts Nitpick_Ind_Intros.get
end
- (*
-fun get_specification thy constname =
- case Symtab.lookup (#const_spec_table (Data.get thy)) constname of
- SOME thms => thms
- | NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed")
- *)
+
fun get_specification table constname =
case Symtab.lookup table constname of
- SOME thms =>
- let
- val _ = tracing ("Looking up specification of " ^ constname ^ ": "
- ^ (commas (map Display.string_of_thm_without_context thms)))
- in thms end
+ SOME thms => thms
| NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed")
val logic_operator_names =
- [@{const_name "=="}, @{const_name "op ="}, @{const_name "op -->"}, @{const_name "All"}, @{const_name "op &"}]
+ [@{const_name "=="}, @{const_name "op ="}, @{const_name "op -->"}, @{const_name "All"}, @{const_name "Ex"},
+ @{const_name "op &"}]
val special_cases = member (op =) [
@{const_name "False"},
@@ -215,6 +194,7 @@
fun defiants_of specs =
fold (Term.add_const_names o prop_of) specs []
|> filter is_defining_constname
+ |> filter_out is_nondefining_constname
|> filter_out has_code_pred_intros
|> filter_out (case_consts thy)
|> filter_out special_cases
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Sat Oct 24 16:55:42 2009 +0200
@@ -107,8 +107,6 @@
if Predicate_Compile_Aux.is_predT (fastype_of t) then
t
else
- error "not implemented"
- (*
let
val (vs, body) = strip_abs t
val names = Term.add_free_names body []
@@ -122,7 +120,6 @@
val pred_body = list_comb (P, args @ [resvar])
val param = fold_rev lambda (vs' @ [resvar]) pred_body
in param end;
- *)
(* creates the list of premises for every intro rule *)
(* theory -> term -> (string list, term list list) *)
@@ -256,7 +253,6 @@
end
else
let
- val _ = tracing ("Flattening term " ^ (Syntax.string_of_term_global thy t))
val (f, args) = strip_comb t
(* TODO: special procedure for higher-order functions: split arguments in
simple types and function types *)
@@ -276,7 +272,6 @@
val pred = lookup_pred t
val nparams = get_nparams pred
val (params, args) = chop nparams args
- val _ = tracing ("mk_prems'': " ^ (Syntax.string_of_term_global thy t) ^ " has " ^ string_of_int nparams ^ " parameters.")
val params' = map (mk_param lookup_pred) params
in
folds_map mk_prems' args (names', prems)
@@ -366,10 +361,7 @@
in
case try (maps mk_intros) ((funs ~~ preds) ~~ (argss' ~~ rhss)) of
NONE => ([], thy)
- | SOME intr_ts => let
- val _ = map (tracing o (Syntax.string_of_term_global thy)) intr_ts
- val _ = map (cterm_of thy) intr_ts
- in
+ | SOME intr_ts =>
if is_some (try (map (cterm_of thy)) intr_ts) then
let
val (ind_result, thy') =
@@ -391,12 +383,8 @@
end
else
let
- val (p, _) = strip_comb (HOLogic.dest_Trueprop (hd (Logic.strip_imp_prems (hd intr_ts))))
- val (_, T) = dest_Const p
- val _ = tracing (Syntax.string_of_typ_global thy T)
val _ = tracing "Introduction rules of function_predicate are not welltyped"
in ([], thy) end
- end
end
(* preprocessing intro rules - uses oracle *)
@@ -417,7 +405,6 @@
| get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy t))
val intro_t = (Logic.unvarify o prop_of) intro
- val _ = tracing (Syntax.string_of_term_global thy intro_t)
val (prems, concl) = Logic.strip_horn intro_t
val frees = map fst (Term.add_frees intro_t [])
fun rewrite prem names =
@@ -441,8 +428,6 @@
rewrite concl frees'
|> map (fn (concl'::conclprems, _) =>
Logic.list_implies ((flat prems') @ conclprems, concl')))
- val _ = Output.tracing ("intro_ts': " ^
- commas (map (Syntax.string_of_term_global thy) intro_ts'))
in
map (Drule.standard o the_oracle () o cterm_of thy) intro_ts'
end;
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML Sat Oct 24 16:55:42 2009 +0200
@@ -123,9 +123,6 @@
else
error ("unexpected specification for constant " ^ quote constname ^ ":\n"
^ commas (map (quote o Display.string_of_thm_global thy) specs))
- val _ = tracing ("Introduction rules of definitions before flattening: "
- ^ commas (map (Display.string_of_thm ctxt) intros))
- val _ = tracing "Defining local predicates and their intro rules..."
val (intros', (local_defs, thy')) = flatten_intros constname intros thy
val (intross, thy'') = fold_map preprocess local_defs thy'
in
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Sat Oct 24 16:55:42 2009 +0200
@@ -63,10 +63,10 @@
val _ = tracing (Display.string_of_thm ctxt' intro)
val thy'' = thy'
|> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro)
- |> Predicate_Compile.preprocess full_constname
- |> Predicate_Compile_Core.add_equations NONE [full_constname]
- |> Predicate_Compile_Core.add_sizelim_equations NONE [full_constname]
- |> Predicate_Compile_Core.add_quickcheck_equations NONE [full_constname]
+ |> Predicate_Compile.preprocess Predicate_Compile_Aux.default_options full_constname
+ |> Predicate_Compile_Core.add_equations Predicate_Compile_Aux.default_options NONE [full_constname]
+ |> Predicate_Compile_Core.add_sizelim_equations Predicate_Compile_Aux.default_options NONE [full_constname]
+ |> Predicate_Compile_Core.add_quickcheck_equations Predicate_Compile_Aux.default_options NONE [full_constname]
val sizelim_modes = Predicate_Compile_Core.sizelim_modes_of thy'' full_constname
val modes = Predicate_Compile_Core.generator_modes_of thy'' full_constname
val prog =
--- 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
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 24 16:55:42 2009 +0200
@@ -7,8 +7,8 @@
signature PREDICATE_COMPILE_CORE =
sig
val setup: theory -> theory
- val code_pred: int list list option -> bool -> string -> Proof.context -> Proof.state
- val code_pred_cmd: int list list option -> bool -> string -> Proof.context -> Proof.state
+ val code_pred: Predicate_Compile_Aux.options -> int list list option -> bool -> string -> Proof.context -> Proof.state
+ val code_pred_cmd: Predicate_Compile_Aux.options -> int list list option -> bool -> string -> Proof.context -> Proof.state
type smode = (int * int list option) list
type mode = smode option list * smode
datatype tmode = Mode of mode * smode * tmode option list;
@@ -39,7 +39,7 @@
val mk_casesrule : Proof.context -> int -> thm list -> term
val analyze_compr: theory -> term -> term
val eval_ref: (unit -> term Predicate.pred) option Unsynchronized.ref
- val add_equations : int list list option -> string list -> theory -> theory
+ val add_equations : Predicate_Compile_Aux.options -> int list list option -> string list -> theory -> theory
val code_pred_intros_attrib : attribute
(* used by Quickcheck_Generator *)
(*val funT_of : mode -> typ -> typ
@@ -90,8 +90,8 @@
val rpred_compfuns : compilation_funs
val dest_funT : typ -> typ * typ
(* val depending_preds_of : theory -> thm list -> string list *)
- val add_quickcheck_equations : int list list option -> string list -> theory -> theory
- val add_sizelim_equations : int list list option -> string list -> theory -> theory
+ val add_quickcheck_equations : Predicate_Compile_Aux.options -> int list list option -> string list -> theory -> theory
+ val add_sizelim_equations : Predicate_Compile_Aux.options -> int list list option -> string list -> theory -> theory
val is_inductive_predicate : theory -> string -> bool
val terms_vs : term list -> string list
val subsets : int -> int -> int list list
@@ -273,7 +273,7 @@
error "Trying to instantiate another predicate" else ()
val subst = Sign.typ_match thy
(fastype_of pred', fastype_of pred) Vartab.empty
- val _ = Output.tracing (commas (map (fn ((x, i), (s, T)) => x ^ " instantiate to " ^ (Syntax.string_of_typ ctxt' T))
+ val _ = tracing (commas (map (fn ((x, i), (s, T)) => x ^ " instantiate to " ^ (Syntax.string_of_typ ctxt' T))
(Vartab.dest subst)))
val subst' = map (fn (indexname, (s, T)) => ((indexname, s), T))
(Vartab.dest subst)
@@ -453,7 +453,7 @@
(* diagnostic display functions *)
-fun print_modes modes = Output.tracing ("Inferred modes:\n" ^
+fun print_modes modes = tracing ("Inferred modes:\n" ^
cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
string_of_mode ms)) modes));
@@ -463,7 +463,7 @@
^ (string_of_entry pred mode entry)
fun print_pred (pred, modes) =
"predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes)
- val _ = Output.tracing (cat_lines (map print_pred pred_mode_table))
+ val _ = tracing (cat_lines (map print_pred pred_mode_table))
in () end;
fun string_of_moded_prem thy (Prem (ts, p), tmode) =
@@ -544,7 +544,7 @@
fun preprocess_elim thy nparams elimrule =
let
- val _ = Output.tracing ("Preprocessing elimination rule "
+ val _ = tracing ("Preprocessing elimination rule "
^ (Display.string_of_thm_global thy elimrule))
fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
@@ -568,7 +568,7 @@
(cterm_of thy elimrule')))
val tac = (fn _ => setmp quick_and_dirty true (SkipProof.cheat_tac thy))
val eq = Goal.prove ctxt' [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) tac
- val _ = Output.tracing "Preprocessed elimination rule"
+ val _ = tracing "Preprocessed elimination rule"
in
Thm.equal_elim eq elimrule |> singleton (Variable.export ctxt' ctxt)
end;
@@ -700,8 +700,8 @@
fun constname_of_intro intr = fst (dest_Const (fst (strip_intro_concl 0 (prop_of intr))))
val _ = if not (forall (fn intr => constname_of_intro intr = c) pre_intros) then
error "register_intros: Introduction rules of different constants are used" else ()
- val _ = Output.tracing ("Registering introduction rules of " ^ c)
- val _ = Output.tracing (commas (map (Display.string_of_thm_global thy) pre_intros))
+ val _ = tracing ("Registering introduction rules of " ^ c ^ "...")
+ val _ = tracing (commas (map (Display.string_of_thm_global thy) pre_intros))
val nparams = guess_nparams T
val pre_elim =
(Drule.standard o (setmp quick_and_dirty true (SkipProof.make_thm thy)))
@@ -1071,11 +1071,6 @@
fun check_mode_clause with_generator thy param_vs modes gen_modes (iss, is) (ts, ps) =
let
- (*
- val _ = Output.tracing ("param_vs:" ^ commas param_vs)
- val _ = Output.tracing ("iss:" ^
- commas (map (fn is => case is of SOME is => string_of_smode is | NONE => "NONE") iss))
- *)
val modes' = modes @ List.mapPartial
(fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
(param_vs ~~ iss);
@@ -1101,7 +1096,7 @@
SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
(vs union generator_vs) ps
| NONE => let
- val _ = Output.tracing ("ps:" ^ (commas
+ val _ = tracing ("ps:" ^ (commas
(map (fn p => string_of_moded_prem thy (p, Mode (([], []), [], []))) ps)))
in (*error "mode analysis failed"*)NONE end
end)
@@ -1131,9 +1126,9 @@
in (p, List.filter (fn m => case find_index
(is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of
~1 => true
- | i => (Output.tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
+ | i => (tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
p ^ " violates mode " ^ string_of_mode m);
- Output.tracing (commas (map (Syntax.string_of_term_global thy) (fst (nth rs i)))); false)) ms)
+ tracing (commas (map (Syntax.string_of_term_global thy) (fst (nth rs i)))); false)) ms)
end;
fun get_modes_pred with_generator thy param_vs clauses modes gen_modes (p, ms) =
@@ -2252,14 +2247,14 @@
(** main function of predicate compiler **)
-fun add_equations_of steps expected_modes prednames thy =
+fun add_equations_of steps options expected_modes prednames thy =
let
- val _ = Output.tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
- val _ = Output.tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
+ val _ = print_step options ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
+ val _ = tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
(*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) =
prepare_intrs thy prednames (maps (intros_of thy) prednames)
- val _ = Output.tracing "Infering modes..."
+ val _ = print_step options "Infering modes..."
val moded_clauses = #infer_modes steps thy extra_modes all_modes param_vs clauses
val modes : (string * ((int * int list option) list option list * (int * int list option) list) list) list = map (fn (p, mps) => (p, map fst mps)) moded_clauses
val all_smodes : (((int * int list option) list) list) list = map (map snd) (map snd modes)
@@ -2269,14 +2264,14 @@
| NONE => ()
val _ = print_modes modes
val _ = print_moded_clauses thy moded_clauses
- val _ = Output.tracing "Defining executable functions..."
+ val _ = print_step options "Defining executable functions..."
val thy' = fold (#create_definitions steps preds) modes thy
|> Theory.checkpoint
- val _ = Output.tracing "Compiling equations..."
+ val _ = print_step options "Compiling equations..."
val compiled_terms =
(#compile_preds steps) thy' all_vs param_vs preds moded_clauses
val _ = print_compiled_terms thy' compiled_terms
- val _ = Output.tracing "Proving equations..."
+ val _ = print_step options "Proving equations..."
val result_thms = #prove steps thy' clauses preds (extra_modes @ modes)
moded_clauses compiled_terms
val qname = #qname steps
@@ -2305,7 +2300,7 @@
fun extend value_of edges_of key G = fst (extend' value_of edges_of key (G, []))
-fun gen_add_equations steps expected_modes names thy =
+fun gen_add_equations steps options expected_modes names thy =
let
val thy' = PredData.map (fold (extend (fetch_pred_data thy) (depending_preds_of thy)) names) thy
|> Theory.checkpoint;
@@ -2314,7 +2309,8 @@
val scc = strong_conn_of (PredData.get thy') names
val thy'' = fold_rev
(fn preds => fn thy =>
- if #are_not_defined steps thy preds then add_equations_of steps expected_modes preds thy else thy)
+ if #are_not_defined steps thy preds then
+ add_equations_of steps options expected_modes preds thy else thy)
scc thy' |> Theory.checkpoint
in thy'' end
@@ -2370,7 +2366,7 @@
(*FIXME why distinguished attribute for cases?*)
(* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *)
-fun generic_code_pred prep_const modes rpred raw_const lthy =
+fun generic_code_pred prep_const options modes rpred raw_const lthy =
let
val thy = ProofContext.theory_of lthy
val const = prep_const thy raw_const
@@ -2400,9 +2396,9 @@
in
goal_ctxt |> LocalTheory.theory (fold set_elim global_thms #>
(if rpred then
- (add_equations NONE [const] #>
- add_sizelim_equations NONE [const] #> add_quickcheck_equations NONE [const])
- else add_equations modes [const]))
+ (add_equations options NONE [const] #>
+ add_sizelim_equations options NONE [const] #> add_quickcheck_equations options NONE [const])
+ else add_equations options modes [const]))
end
in
Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy''
--- a/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:42 2009 +0200
@@ -322,13 +322,13 @@
code_pred (inductify_all) Min .
subsection {* Examples with lists *}
-
+(*
inductive filterP for Pa where
"(filterP::('a => bool) => 'a list => 'a list => bool) (Pa::'a => bool) [] []"
| "[| (res::'a list) = (y::'a) # (resa::'a list); (filterP::('a => bool) => 'a list => 'a list => bool) (Pa::'a => bool) (xt::'a list) resa; Pa y |]
==> filterP Pa (y # xt) res"
| "[| (filterP::('a => bool) => 'a list => 'a list => bool) (Pa::'a => bool) (xt::'a list) (res::'a list); ~ Pa (y::'a) |] ==> filterP Pa (y # xt) res"
-
+*)
(*
code_pred (inductify_all) (rpred) filterP .
thm filterP.rpred_equation
@@ -371,20 +371,23 @@
code_pred (inductify_all) avl .
thm avl.equation
-
+(*
fun set_of
where
"set_of ET = {}"
| "set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)"
-fun is_ord
+
+fun is_ord :: "nat tree => bool"
where
"is_ord ET = True"
| "is_ord (MKT n l r h) =
((\<forall>n' \<in> set_of l. n' < n) \<and> (\<forall>n' \<in> set_of r. n < n') \<and> is_ord l \<and> is_ord r)"
+ML {* *}
code_pred (inductify_all) set_of .
thm set_of.equation
+*)
text {* expected mode: [1], [1, 2] *}
(* FIXME *)
(*
@@ -426,6 +429,18 @@
code_pred (inductify_all) List.rev .
thm revP.equation
+code_pred (inductify_all) foldl .
+thm foldlP.equation
+
+code_pred (inductify_all) filter .
+
+definition test where "test xs = filter (\<lambda>x. x = (1::nat)) xs"
+term "one_nat_inst.one_nat"
+code_pred (inductify_all) test .
+thm testP.equation
+(*
+code_pred (inductify_all) (rpred) test .
+*)
section {* Handling set operations *}
@@ -445,12 +460,12 @@
code_pred (inductify_all) S\<^isub>1p .
thm S\<^isub>1p.equation
-
+(*
theorem S\<^isub>1_sound:
"w \<in> S\<^isub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
quickcheck[generator=pred_compile]
oops
-
+*)
inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
"[] \<in> S\<^isub>2"
| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
@@ -465,7 +480,7 @@
theorem S\<^isub>2_sound:
"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
(*quickcheck[generator=SML]*)
-quickcheck[generator=pred_compile, size=15, iterations=100]
+(*quickcheck[generator=pred_compile, size=15, iterations=100]*)
oops
inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
@@ -480,23 +495,24 @@
theorem S\<^isub>3_sound:
"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator=pred_compile, size=10, iterations=1]
+(*quickcheck[generator=pred_compile, size=10, iterations=1]*)
oops
lemma "\<not> (length w > 2) \<or> \<not> (length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b])"
-quickcheck[size=10, generator = pred_compile]
+(*quickcheck[size=10, generator = pred_compile]*)
oops
-
+(*
inductive test
where
- "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] ==> test w"
+ "length [x \<leftarrow> w. a = x] = length [x \<leftarrow> w. x = b] ==> test w"
ML {* @{term "[x \<leftarrow> w. x = a]"} *}
code_pred (inductify_all) test .
thm test.equation
+*)
(*
theorem S\<^isub>3_complete:
-"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
+"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. b = x] \<longrightarrow> w \<in> S\<^isub>3"
(*quickcheck[generator=SML]*)
quickcheck[generator=pred_compile, size=10, iterations=100]
oops
@@ -509,15 +525,15 @@
| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
-
+(*
theorem S\<^isub>4_sound:
"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
quickcheck[generator = pred_compile, size=2, iterations=1]
oops
-
+*)
theorem S\<^isub>4_complete:
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
-quickcheck[generator = pred_compile, size=5, iterations=1]
+(*quickcheck[generator = pred_compile, size=5, iterations=1]*)
oops
theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
@@ -580,16 +596,17 @@
| abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t"
lemma "Gamma \<turnstile> t : T \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> Gamma \<turnstile> t' : T"
-quickcheck[generator = pred_compile, size = 10, iterations = 1000]
+quickcheck[generator = pred_compile, size = 10, iterations = 100]
oops
(* FIXME *)
-(*
-inductive test for P where
+
+inductive test' for P where
"[| filter P vs = res |]
-==> test P vs res"
+==> test' P vs res"
-code_pred test .
-*)
+code_pred (inductify_all) test' .
+thm test'.equation
+
(*
export_code test_for_1_yields_1_2 in SML file -
code_pred (inductify_all) (rpred) test .