# HG changeset patch # User bulwahn # Date 1256396142 -7200 # Node ID 3c7c4372f9adbcfe94496dc45b85bd1173da10a6 # Parent 7d01480cc8e366b22260412ee9cda528093b5ff2 cleaned up debugging messages; added options to code_pred command diff -r 7d01480cc8e3 -r 3c7c4372f9ad src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML --- 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; diff -r 7d01480cc8e3 -r 3c7c4372f9ad src/HOL/Tools/Predicate_Compile/pred_compile_data.ML --- 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 diff -r 7d01480cc8e3 -r 3c7c4372f9ad src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML --- 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; diff -r 7d01480cc8e3 -r 3c7c4372f9ad src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML --- 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 diff -r 7d01480cc8e3 -r 3c7c4372f9ad src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML --- 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 = 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 diff -r 7d01480cc8e3 -r 3c7c4372f9ad src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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'' diff -r 7d01480cc8e3 -r 3c7c4372f9ad src/HOL/ex/Predicate_Compile_ex.thy --- 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 \ set_of r)" -fun is_ord + +fun is_ord :: "nat tree => bool" where "is_ord ET = True" | "is_ord (MKT n l r h) = ((\n' \ set_of l. n' < n) \ (\n' \ set_of r. n < n') \ is_ord l \ 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 (\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 \ S\<^isub>1 \ length [x \ w. x = a] = length [x \ w. x = b]" quickcheck[generator=pred_compile] oops - +*) inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where "[] \ S\<^isub>2" | "w \ A\<^isub>2 \ b # w \ S\<^isub>2" @@ -465,7 +480,7 @@ theorem S\<^isub>2_sound: "w \ S\<^isub>2 \ length [x \ w. x = a] = length [x \ 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 \ S\<^isub>3 \ length [x \ w. x = a] = length [x \ w. x = b]" -quickcheck[generator=pred_compile, size=10, iterations=1] +(*quickcheck[generator=pred_compile, size=10, iterations=1]*) oops lemma "\ (length w > 2) \ \ (length [x \ w. x = a] = length [x \ w. x = b])" -quickcheck[size=10, generator = pred_compile] +(*quickcheck[size=10, generator = pred_compile]*) oops - +(* inductive test where - "length [x \ w. x = a] = length [x \ w. x = b] ==> test w" + "length [x \ w. a = x] = length [x \ w. x = b] ==> test w" ML {* @{term "[x \ w. x = a]"} *} code_pred (inductify_all) test . thm test.equation +*) (* theorem S\<^isub>3_complete: -"length [x \ w. x = a] = length [x \ w. x = b] \ w \ S\<^isub>3" +"length [x \ w. x = a] = length [x \ w. b = x] \ w \ S\<^isub>3" (*quickcheck[generator=SML]*) quickcheck[generator=pred_compile, size=10, iterations=100] oops @@ -509,15 +525,15 @@ | "\v \ A\<^isub>4; w \ A\<^isub>4\ \ b # v @ w \ A\<^isub>4" | "w \ S\<^isub>4 \ b # w \ B\<^isub>4" | "\v \ B\<^isub>4; w \ B\<^isub>4\ \ a # v @ w \ B\<^isub>4" - +(* theorem S\<^isub>4_sound: "w \ S\<^isub>4 \ length [x \ w. x = a] = length [x \ w. x = b]" quickcheck[generator = pred_compile, size=2, iterations=1] oops - +*) theorem S\<^isub>4_complete: "length [x \ w. x = a] = length [x \ w. x = b] \ w \ 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 \\<^sub>\ t ==> Abs T s \\<^sub>\ Abs T t" lemma "Gamma \ t : T \ t \\<^sub>\ t' \ Gamma \ 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 .