# HG changeset patch # User bulwahn # Date 1266928575 -3600 # Node ID c9f428269b3826dd470e22dd8ec2f00dbe92807a # Parent 997aa3a3e4bbfcfd4fab9c3508241774d6bcaf9c adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening diff -r 997aa3a3e4bb -r c9f428269b38 src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Tue Feb 23 10:02:14 2010 +0100 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Tue Feb 23 13:36:15 2010 +0100 @@ -10,9 +10,11 @@ val take_random : int -> 'a list -> 'a list datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error -type mtd = string * (theory -> term -> outcome) +type timing = (string * int) list -type mutant_subentry = term * (string * outcome) list +type mtd = string * (theory -> term -> outcome * timing) + +type mutant_subentry = term * (string * (outcome * timing)) list type detailed_entry = string * bool * term * mutant_subentry list type subentry = string * int * int * int * int * int * int @@ -52,7 +54,7 @@ (* quickcheck options *) (*val quickcheck_generator = "SML"*) -val iterations = 100 +val iterations = 1 val size = 5 exception RANDOM; @@ -75,12 +77,13 @@ else l + Real.floor (rmod (random ()) (real (h - l + 1))); datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error -type mtd = string * (theory -> term -> outcome) +type timing = (string * int) list -type mutant_subentry = term * (string * outcome) list +type mtd = string * (theory -> term -> outcome * timing) + +type mutant_subentry = term * (string * (outcome * timing)) list type detailed_entry = string * bool * term * mutant_subentry list - type subentry = string * int * int * int * int * int * int type entry = string * bool * subentry list type report = entry list @@ -94,11 +97,11 @@ fun invoke_quickcheck quickcheck_generator thy t = TimeLimit.timeLimit (Time.fromSeconds (! Auto_Counterexample.time_limit)) (fn _ => - case Quickcheck.test_term (ProofContext.init thy) false (SOME quickcheck_generator) + case Quickcheck.timed_test_term (ProofContext.init thy) false (SOME quickcheck_generator) size iterations (preprocess thy [] t) of - NONE => NoCex - | SOME _ => GenuineCex) () - handle TimeLimit.TimeOut => Timeout + (NONE, time_report) => (NoCex, time_report) + | (SOME _, time_report) => (GenuineCex, time_report)) () + handle TimeLimit.TimeOut => (Timeout, [("timelimit", !Auto_Counterexample.time_limit)]) fun quickcheck_mtd quickcheck_generator = ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck quickcheck_generator) @@ -245,17 +248,26 @@ Library.nth xs j :: take_random (n - 1) (nth_drop j xs) end +fun cpu_time description f = + let + val start = start_timing () + val result = Exn.capture f () + val time = Time.toMilliseconds (#cpu (end_timing start)) + in (Exn.release result, (description, time)) end + fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t = let val _ = priority ("Invoking " ^ mtd_name) - val res = case try (invoke_mtd thy) t of - SOME res => res - | NONE => (priority ("**** PROBLEMS WITH " ^ - Syntax.string_of_term_global thy t); Error) + val ((res, timing), time) = cpu_time "total time" + (fn () => case try (invoke_mtd thy) t of + SOME (res, timing) => (res, timing) + | NONE => (priority ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t); + (Error , []))) val _ = priority (" Done") - in res end + in (res, time :: timing) end (* theory -> term list -> mtd -> subentry *) +(* fun test_mutants_using_one_method thy mutants (mtd_name, invoke_mtd) = let val res = map (safe_invoke_mtd thy (mtd_name, invoke_mtd)) mutants @@ -266,7 +278,7 @@ fun create_entry thy thm exec mutants mtds = (Thm.get_name thm, exec, map (test_mutants_using_one_method thy mutants) mtds) - +*) fun create_detailed_entry thy thm exec mutants mtds = let fun create_mutant_subentry mutant = (mutant, @@ -322,15 +334,22 @@ | string_of_outcome Timeout = "Timeout" | string_of_outcome Error = "Error" -fun string_of_mutant_subentry thy (t, results) = +fun string_of_mutant_subentry thy thm_name (t, results) = "mutant: " ^ Syntax.string_of_term_global thy t ^ "\n" ^ - space_implode "; " (map (fn (mtd_name, outcome) => mtd_name ^ ": " ^ string_of_outcome outcome) results) ^ + space_implode "; " + (map (fn (mtd_name, (outcome, timing)) => mtd_name ^ ": " ^ string_of_outcome outcome) results) ^ "\n" +fun string_of_mutant_subentry' thy thm_name (t, results) = + "mutant of " ^ thm_name ^ ":" ^ + cat_lines (map (fn (mtd_name, (outcome, timing)) => + mtd_name ^ ": " ^ string_of_outcome outcome ^ "; " ^ + space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing)) results) + fun string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) = thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ": " ^ Syntax.string_of_term_global thy t ^ "\n" ^ - cat_lines (map (string_of_mutant_subentry thy) mutant_subentries) ^ "\n" + cat_lines (map (string_of_mutant_subentry' thy thm_name) mutant_subentries) ^ "\n" (* subentry -> string *) fun string_for_subentry (mtd_name, genuine_cex, potential_cex, no_cex, donno, diff -r 997aa3a3e4bb -r c9f428269b38 src/HOL/Tools/Datatype/datatype_prop.ML --- a/src/HOL/Tools/Datatype/datatype_prop.ML Tue Feb 23 10:02:14 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML Tue Feb 23 13:36:15 2010 +0100 @@ -22,6 +22,8 @@ (string * sort) list -> theory -> term list list val make_splits : string list -> descr list -> (string * sort) list -> theory -> (term * term) list + val make_case_combs : string list -> descr list -> + (string * sort) list -> theory -> string -> term list val make_weak_case_congs : string list -> descr list -> (string * sort) list -> theory -> term list val make_case_congs : string list -> descr list -> diff -r 997aa3a3e4bb -r c9f428269b38 src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Tue Feb 23 10:02:14 2010 +0100 +++ b/src/HOL/Tools/Function/function.ML Tue Feb 23 13:36:15 2010 +0100 @@ -97,6 +97,7 @@ |> addsmps (conceal_partial o Binding.qualify false "partial") "psimps" conceal_partial psimp_attribs psimps ||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps + ||> fold_option (Spec_Rules.add Spec_Rules.Equational o (pair fs)) trsimps ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"), [Attrib.internal (K (Rule_Cases.case_names cnames)), Attrib.internal (K (Rule_Cases.consumes 1)), @@ -126,7 +127,7 @@ val add_function = gen_add_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS) val add_function_cmd = gen_add_function true Specification.read_spec "_::type" - + fun gen_termination_proof prep_term raw_term_opt lthy = let val term_opt = Option.map (prep_term lthy) raw_term_opt diff -r 997aa3a3e4bb -r c9f428269b38 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Tue Feb 23 10:02:14 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Tue Feb 23 13:36:15 2010 +0100 @@ -8,13 +8,13 @@ sig val setup : theory -> theory val preprocess : Predicate_Compile_Aux.options -> string -> theory -> theory + val present_graph : bool Unsynchronized.ref end; structure Predicate_Compile (*: PREDICATE_COMPILE*) = struct -(* options *) -val fail_safe_mode = true +val present_graph = Unsynchronized.ref false open Predicate_Compile_Aux; @@ -33,10 +33,12 @@ commas (map (Display.string_of_thm_global thy) intros)) intross))) else () -fun print_specs thy specs = - map (fn (c, thms) => "Constant " ^ c ^ " has specification:\n" - ^ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs - +fun print_specs options thy specs = + if show_intermediate_results options then + map (fn (c, thms) => "Constant " ^ c ^ " has specification:\n" + ^ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs + |> space_implode "\n" |> tracing + else () fun overload_const thy s = the_default s (Option.map fst (AxClass.inst_of_param thy s)) fun map_specs f specs = @@ -47,15 +49,21 @@ val _ = print_step options "Compiling predicates to flat introrules..." val specs = map (apsnd (map (fn th => if is_equationlike th then Predicate_Compile_Data.normalize_equation thy' th else th))) specs - val (intross1, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess specs thy') + val (intross1, thy'') = + apfst flat (fold_map (Predicate_Compile_Pred.preprocess options) specs thy') val _ = print_intross options thy'' "Flattened introduction rules: " intross1 val _ = print_step options "Replacing functions in introrules..." val intross2 = - if fail_safe_mode then - case try (map_specs (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross1 of - SOME intross => intross - | NONE => let val _ = warning "Function replacement failed!" in intross1 end - else map_specs (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross1 + if function_flattening options then + if fail_safe_function_flattening options then + case try (map_specs (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross1 of + SOME intross => intross + | NONE => + (if show_caught_failures options then tracing "Function replacement failed!" else (); + intross1) + else map_specs (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross1 + else + intross1 val _ = print_intross options thy'' "Introduction rules with replaced functions: " intross2 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'') @@ -70,35 +78,45 @@ end fun preprocess_strong_conn_constnames options gr ts thy = - let - fun get_specs ts = map_filter (fn t => - TermGraph.get_node gr t |> - (fn ths => if null ths then NONE else SOME (fst (dest_Const t), ths))) - ts - val _ = print_step options ("Preprocessing scc of " ^ - commas (map (Syntax.string_of_term_global thy) ts)) - val (prednames, funnames) = List.partition (fn t => body_type (fastype_of t) = @{typ bool}) ts - (* untangle recursion by defining predicates for all functions *) - val _ = print_step options - ("Compiling functions (" ^ commas (map (Syntax.string_of_term_global thy) 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 specs = (get_specs prednames) @ fun_pred_specs - val (intross3, thy''') = process_specification options specs thy' - val _ = print_intross options thy''' "Introduction rules with new constants: " intross3 - val intross4 = map_specs (maps remove_pointless_clauses) intross3 - val _ = print_intross options thy''' "After removing pointless clauses: " intross4 - val intross5 = map (fn (s, ths) => (overload_const thy''' s, map (AxClass.overload thy''') ths)) intross4 - val intross6 = map_specs (map (expand_tuples thy''')) intross5 - val _ = print_intross options thy''' "introduction rules before registering: " intross6 - val _ = print_step options "Registering introduction rules..." - val thy'''' = fold Predicate_Compile_Core.register_intros intross6 thy''' - in - thy'''' - end; + if forall (fn (Const (c, _)) => Predicate_Compile_Core.is_registered thy c) ts then + thy + else + let + fun get_specs ts = map_filter (fn t => + TermGraph.get_node gr t |> + (fn ths => if null ths then NONE else SOME (fst (dest_Const t), ths))) + ts + val _ = print_step options ("Preprocessing scc of " ^ + commas (map (Syntax.string_of_term_global thy) ts)) + val (prednames, funnames) = List.partition (fn t => body_type (fastype_of t) = @{typ bool}) ts + (* untangle recursion by defining predicates for all functions *) + val _ = print_step options + ("Compiling functions (" ^ commas (map (Syntax.string_of_term_global thy) funnames) ^ + ") to predicates...") + val (fun_pred_specs, thy') = + (if function_flattening options andalso (not (null funnames)) then + if fail_safe_function_flattening options then + case try (Predicate_Compile_Fun.define_predicates (get_specs funnames)) thy of + SOME (intross, thy) => (intross, thy) + | NONE => ([], thy) + else Predicate_Compile_Fun.define_predicates (get_specs funnames) thy + else ([], thy)) + (*||> Theory.checkpoint*) + val _ = print_specs options thy' fun_pred_specs + val specs = (get_specs prednames) @ fun_pred_specs + val (intross3, thy''') = process_specification options specs thy' + val _ = print_intross options thy''' "Introduction rules with new constants: " intross3 + val intross4 = map_specs (maps remove_pointless_clauses) intross3 + val _ = print_intross options thy''' "After removing pointless clauses: " intross4 + val intross5 = + map (fn (s, ths) => (overload_const thy''' s, map (AxClass.overload thy''') ths)) intross4 + val intross6 = map_specs (map (expand_tuples thy''')) intross5 + val _ = print_intross options thy''' "introduction rules before registering: " intross6 + val _ = print_step options "Registering introduction rules..." + val thy'''' = fold Predicate_Compile_Core.register_intros intross6 thy''' + in + thy'''' + end; fun preprocess options t thy = let @@ -106,6 +124,7 @@ val gr = Output.cond_timeit (!Quickcheck.timing) "preprocess-obtain graph" (fn () => Predicate_Compile_Data.obtain_specification_graph options thy t |> (fn gr => TermGraph.subgraph (member (op =) (TermGraph.all_succs gr [t])) gr)) + val _ = if !present_graph then Predicate_Compile_Data.present_graph gr else () in Output.cond_timeit (!Quickcheck.timing) "preprocess-process" (fn () => (fold_rev (preprocess_strong_conn_constnames options gr) @@ -128,7 +147,12 @@ show_modes = chk "show_modes", show_mode_inference = chk "show_mode_inference", show_compilation = chk "show_compilation", + show_caught_failures = false, skip_proof = chk "skip_proof", + function_flattening = not (chk "no_function_flattening"), + fail_safe_function_flattening = false, + no_topmost_reordering = false, + no_higher_order_predicate = [], inductify = chk "inductify", compilation = compilation } diff -r 997aa3a3e4bb -r c9f428269b38 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue Feb 23 10:02:14 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue Feb 23 13:36:15 2010 +0100 @@ -29,6 +29,7 @@ fun find_indices f xs = map_filter (fn (i, true) => SOME i | (i, false) => NONE) (map_index (apsnd f) xs) +fun assert check = if check then () else error "Assertion failed!" (* mode *) datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode @@ -57,21 +58,47 @@ fun dest_tuple_mode (Pair (mode, mode')) = mode :: dest_tuple_mode mode' | dest_tuple_mode _ = [] -fun all_modes_of_typ (T as Type ("fun", _)) = + +fun all_modes_of_typ' (T as Type ("fun", _)) = + let + val (S, U) = strip_type T + in + if U = HOLogic.boolT then + fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2) + (map all_modes_of_typ' S) [Bool] + else + [Input, Output] + end + | all_modes_of_typ' (Type ("*", [T1, T2])) = + map_product (curry Pair) (all_modes_of_typ' T1) (all_modes_of_typ' T2) + | all_modes_of_typ' _ = [Input, Output] + +fun all_modes_of_typ (T as Type ("fun", _)) = let val (S, U) = strip_type T in if U = HOLogic.boolT then fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2) - (map all_modes_of_typ S) [Bool] + (map all_modes_of_typ' S) [Bool] else [Input, Output] end - | all_modes_of_typ (Type ("*", [T1, T2])) = - map_product (curry Pair) (all_modes_of_typ T1) (all_modes_of_typ T2) | all_modes_of_typ (Type ("bool", [])) = [Bool] - | all_modes_of_typ _ = [Input, Output] + | all_modes_of_typ T = all_modes_of_typ' T +fun all_smodes_of_typ (T as Type ("fun", _)) = + let + val (S, U) = strip_type T + fun all_smodes (Type ("*", [T1, T2])) = + map_product (curry Pair) (all_smodes T1) (all_smodes T2) + | all_smodes _ = [Input, Output] + in + if U = HOLogic.boolT then + fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2) (map all_smodes S) [Bool] + else + error "all_smodes_of_typ: invalid type for predicate" + end +(* fun extract_params arg = case fastype_of arg of (T as Type ("fun", _)) => @@ -86,7 +113,7 @@ extract_params t1 @ extract_params t2 end | _ => [] - +*) fun ho_arg_modes_of mode = let fun ho_arg_mode (m as Fun _) = [m] @@ -144,9 +171,10 @@ in (comb_option HOLogic.mk_prod (i1, i2), comb_option HOLogic.mk_prod (o1, o2)) end - | split_arg_mode' Input t = (SOME t, NONE) - | split_arg_mode' Output t = (NONE, SOME t) - | split_arg_mode' _ _ = error "split_map_mode: mode and term do not match" + | split_arg_mode' m t = + if eq_mode (m, Input) then (SOME t, NONE) + else if eq_mode (m, Output) then (NONE, SOME t) + else error "split_map_mode: mode and term do not match" in (pairself (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) ts) end @@ -269,7 +297,6 @@ let val T = (Sign.the_const_type thy constname) in body_type T = @{typ "bool"} end; - fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = HOLogic.boolT) | is_predT _ = false @@ -373,7 +400,60 @@ in Logic.list_implies (maps f premises, head) end + + +(* split theorems of case expressions *) + +(* +fun has_split_rule_cname @{const_name "nat_case"} = true + | has_split_rule_cname @{const_name "list_case"} = true + | has_split_rule_cname _ = false +fun has_split_rule_term thy (Const (@{const_name "nat_case"}, _)) = true + | has_split_rule_term thy (Const (@{const_name "list_case"}, _)) = true + | has_split_rule_term thy _ = false + +fun has_split_rule_term' thy (Const (@{const_name "If"}, _)) = true + | has_split_rule_term' thy (Const (@{const_name "Let"}, _)) = true + | has_split_rule_term' thy c = has_split_rule_term thy c + +*) +fun prepare_split_thm ctxt split_thm = + (split_thm RS @{thm iffD2}) + |> LocalDefs.unfold ctxt [@{thm atomize_conjL[symmetric]}, + @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}] + +fun find_split_thm thy (Const (name, typ)) = + let + fun split_name str = + case first_field "." str + of (SOME (field, rest)) => field :: split_name rest + | NONE => [str] + val splitted_name = split_name name + in + if length splitted_name > 0 andalso + String.isSuffix "_case" (List.last splitted_name) + then + (List.take (splitted_name, length splitted_name - 1)) @ ["split"] + |> space_implode "." + |> PureThy.get_thm thy + |> SOME + handle ERROR msg => NONE + else NONE + end + | find_split_thm _ _ = NONE + + +(* TODO: split rules for let and if are different *) +fun find_split_thm' thy (Const (@{const_name "If"}, _)) = SOME @{thm split_if} + | find_split_thm' thy (Const (@{const_name "Let"}, _)) = SOME @{thm refl} (* TODO *) + | find_split_thm' thy c = find_split_thm thy c + +fun has_split_thm thy t = is_some (find_split_thm thy t) + +fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t) + + (* lifting term operations to theorems *) fun map_term thy f th = @@ -388,7 +468,16 @@ (* Different options for compiler *) -datatype compilation = Pred | Random | Depth_Limited | DSeq | Annotated | Random_DSeq +datatype compilation = Pred | Random | Depth_Limited | DSeq | Annotated + | Pos_Random_DSeq | Neg_Random_DSeq + + +fun negative_compilation_of Pos_Random_DSeq = Neg_Random_DSeq + | negative_compilation_of Neg_Random_DSeq = Pos_Random_DSeq + | negative_compilation_of c = c + +fun compilation_for_polarity false Pos_Random_DSeq = Neg_Random_DSeq + | compilation_for_polarity _ c = c fun string_of_compilation c = case c of Pred => "" @@ -396,8 +485,9 @@ | Depth_Limited => "depth limited" | DSeq => "dseq" | Annotated => "annotated" - | Random_DSeq => "random dseq" - + | Pos_Random_DSeq => "pos_random dseq" + | Neg_Random_DSeq => "neg_random_dseq" + (*datatype compilation_options = Pred | Random of int | Depth_Limited of int | DSeq of int | Annotated*) @@ -411,8 +501,12 @@ show_mode_inference : bool, show_modes : bool, show_compilation : bool, + show_caught_failures : bool, skip_proof : bool, - + no_topmost_reordering : bool, + function_flattening : bool, + fail_safe_function_flattening : bool, + no_higher_order_predicate : string list, inductify : bool, compilation : compilation }; @@ -428,8 +522,15 @@ fun show_modes (Options opt) = #show_modes opt fun show_mode_inference (Options opt) = #show_mode_inference opt fun show_compilation (Options opt) = #show_compilation opt +fun show_caught_failures (Options opt) = #show_caught_failures opt + fun skip_proof (Options opt) = #skip_proof opt +fun function_flattening (Options opt) = #function_flattening opt +fun fail_safe_function_flattening (Options opt) = #fail_safe_function_flattening opt +fun no_topmost_reordering (Options opt) = #no_topmost_reordering opt +fun no_higher_order_predicate (Options opt) = #no_higher_order_predicate opt + fun is_inductify (Options opt) = #inductify opt fun compilation (Options opt) = #compilation opt @@ -444,18 +545,22 @@ show_modes = false, show_mode_inference = false, show_compilation = false, + show_caught_failures = false, skip_proof = true, - + no_topmost_reordering = false, + function_flattening = false, + fail_safe_function_flattening = false, + no_higher_order_predicate = [], inductify = false, compilation = Pred } val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes", - "show_mode_inference", "show_compilation", "skip_proof", "inductify"] + "show_mode_inference", "show_compilation", "skip_proof", "inductify", "no_function_flattening"] val compilation_names = [("pred", Pred), (*("random", Random), ("depth_limited", Depth_Limited), ("annotated", Annotated),*) - ("dseq", DSeq), ("random_dseq", Random_DSeq)] + ("dseq", DSeq), ("random_dseq", Pos_Random_DSeq)] fun print_step options s = if show_steps options then tracing s else () diff -r 997aa3a3e4bb -r c9f428269b38 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Feb 23 10:02:14 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Feb 23 13:36:15 2010 +0100 @@ -16,7 +16,7 @@ val register_intros : string * thm list -> theory -> theory val is_registered : theory -> string -> bool val function_name_of : Predicate_Compile_Aux.compilation -> theory - -> string -> Predicate_Compile_Aux.mode -> string + -> string -> bool * Predicate_Compile_Aux.mode -> string val predfun_intro_of: theory -> string -> Predicate_Compile_Aux.mode -> thm val predfun_elim_of: theory -> string -> Predicate_Compile_Aux.mode -> thm val all_preds_of : theory -> string list @@ -153,7 +153,7 @@ | mode_of (Term m) = m | mode_of (Mode_App (d1, d2)) = (case mode_of d1 of Fun (m, m') => - (if m = mode_of d2 then m' else error "mode_of") + (if eq_mode (m, mode_of d2) then m' else error "mode_of") | _ => error "mode_of2") | mode_of (Mode_Pair (d1, d2)) = Pair (mode_of d1, mode_of d2) @@ -182,7 +182,7 @@ type moded_clause = term list * (indprem * mode_derivation) list -type 'a pred_mode_table = (string * (mode * 'a) list) list +type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list (* book-keeping *) @@ -257,8 +257,9 @@ ^ "functions defined for predicate " ^ quote name) | SOME fun_names => fun_names -fun function_name_of compilation thy name mode = - case AList.lookup (op =) (function_names_of compilation thy name) mode of +fun function_name_of compilation thy name (pol, mode) = + case AList.lookup eq_mode + (function_names_of (compilation_for_polarity pol compilation) thy name) mode of NONE => error ("No " ^ string_of_compilation compilation ^ "function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name) | SOME function_name => function_name @@ -296,12 +297,12 @@ if show_modes options then tracing ("Inferred modes:\n" ^ cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map - string_of_mode ms)) modes)) + (fn (p, m) => string_of_mode m ^ (if p then "pos" else "neg")) ms)) modes)) else () fun print_pred_mode_table string_of_entry thy pred_mode_table = let - fun print_mode pred (mode, entry) = "mode : " ^ string_of_mode mode + fun print_mode pred ((pol, mode), entry) = "mode : " ^ string_of_mode mode ^ string_of_entry pred mode entry fun print_pred (pred, modes) = "predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes) @@ -364,7 +365,7 @@ SOME (s, ms) => (case AList.lookup (op =) modes s of SOME modes => let - val modes' = modes + val modes' = map snd modes in if not (eq_set eq_mode (ms, modes')) then error ("expected modes were not inferred:\n" @@ -381,7 +382,7 @@ SOME inferred_ms => let val preds_without_modes = map fst (filter (null o snd) (modes @ extra_modes)) - val modes' = inferred_ms + val modes' = map snd inferred_ms in if not (eq_set eq_mode (ms, modes')) then error ("expected modes were not inferred:\n" @@ -880,8 +881,6 @@ Random_Sequence_CompFuns.mk_random_dseqT T) $ random end; - - (* for external use with interactive mode *) val pred_compfuns = PredicateCompFuns.compfuns val randompred_compfuns = Random_Sequence_CompFuns.compfuns; @@ -898,6 +897,8 @@ (** mode analysis **) +(* options for mode analysis are: #use_random, #reorder_premises *) + fun is_constrt thy = let val cnstrs = flat (maps @@ -935,7 +936,7 @@ in merge (map (fn ks => i::ks) is) is end else [[]]; -fun print_failed_mode options thy modes p m rs is = +fun print_failed_mode options thy modes p (pol, m) rs is = if show_mode_inference options then let val _ = tracing ("Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^ @@ -943,7 +944,7 @@ in () end else () -fun error_of p m is = +fun error_of p (pol, m) is = (" Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^ p ^ " violates mode " ^ string_of_mode m) @@ -992,7 +993,7 @@ fun is_invertible_function thy (Const (f, _)) = is_constr thy f | is_invertible_function thy _ = false -fun non_invertible_subterms thy (Free _) = [] +fun non_invertible_subterms thy (t as Free _) = [] | non_invertible_subterms thy t = case (strip_comb t) of (f, args) => if is_invertible_function thy f then @@ -1029,6 +1030,9 @@ forall (fn t => is_eqT (fastype_of t) andalso forall (member (op =) vs) (term_vs t)) (non_invertible_subterms thy t) + andalso + (forall (is_eqT o snd) + (inter (fn ((f', _), f) => f = f') vs (Term.add_frees t []))) fun vars_of_destructable_term thy (Free (x, _)) = [x] | vars_of_destructable_term thy t = @@ -1042,18 +1046,52 @@ fun missing_vars vs t = subtract (op =) vs (term_vs t) -fun derivations_of thy modes vs t Input = - [(Term Input, missing_vars vs t)] - | derivations_of thy modes vs t Output = - if is_possible_output thy vs t then [(Term Output, [])] else [] - | derivations_of thy modes vs (Const ("Pair", _) $ t1 $ t2) (Pair (m1, m2)) = +fun output_terms (Const ("Pair", _) $ t1 $ t2, Mode_Pair (d1, d2)) = + output_terms (t1, d1) @ output_terms (t2, d2) + | output_terms (t1 $ t2, Mode_App (d1, d2)) = + output_terms (t1, d1) @ output_terms (t2, d2) + | output_terms (t, Term Output) = [t] + | output_terms _ = [] + +fun lookup_mode modes (Const (s, T)) = + (case (AList.lookup (op =) modes s) of + SOME ms => SOME (map (fn m => (Context m, [])) ms) + | NONE => NONE) + | lookup_mode modes (Free (x, _)) = + (case (AList.lookup (op =) modes x) of + SOME ms => SOME (map (fn m => (Context m , [])) ms) + | NONE => NONE) + +fun derivations_of thy modes vs (Const ("Pair", _) $ t1 $ t2) (Pair (m1, m2)) = map_product (fn (m1, mvars1) => fn (m2, mvars2) => (Mode_Pair (m1, m2), union (op =) mvars1 mvars2)) (derivations_of thy modes vs t1 m1) (derivations_of thy modes vs t2 m2) + | derivations_of thy modes vs t (m as Fun _) = + (*let + val (p, args) = strip_comb t + in + (case lookup_mode modes p of + SOME ms => map_filter (fn (Context m, []) => let + val ms = strip_fun_mode m + val (argms, restms) = chop (length args) ms + val m' = fold_rev (curry Fun) restms Bool + in + if forall (fn m => eq_mode (Input, m)) argms andalso eq_mode (m', mode) then + SOME (fold (curry Mode_App) (map Term argms) (Context m), missing_vars vs t) + else NONE + end) ms + | NONE => (if is_all_input mode then [(Context mode, [])] else [])) + end*) + (case try (all_derivations_of thy modes vs) t of + SOME derivs => + filter (fn (d, mvars) => eq_mode (mode_of d, m) andalso null (output_terms (t, d))) derivs + | NONE => (if is_all_input m then [(Context m, [])] else [])) | derivations_of thy modes vs t m = - (case try (all_derivations_of thy modes vs) t of - SOME derivs => filter (fn (d, mvars) => mode_of d = m) derivs - | NONE => (if is_all_input m then [(Context m, [])] else [])) + if eq_mode (m, Input) then + [(Term Input, missing_vars vs t)] + else if eq_mode (m, Output) then + (if is_possible_output thy vs t then [(Term Output, [])] else []) + else [] and all_derivations_of thy modes vs (Const ("Pair", _) $ t1 $ t2) = let val derivs1 = all_derivations_of thy modes vs t1 @@ -1073,14 +1111,8 @@ (Mode_App (d1, d2), union (op =) mvars1 mvars2)) (derivations_of thy modes vs t2 m') | _ => error "Something went wrong") derivs1 end - | all_derivations_of thy modes vs (Const (s, T)) = - (case (AList.lookup (op =) modes s) of - SOME ms => map (fn m => (Context m, [])) ms - | NONE => error ("No mode for constant " ^ s)) - | all_derivations_of _ modes vs (Free (x, _)) = - (case (AList.lookup (op =) modes x) of - SOME ms => map (fn m => (Context m , [])) ms - | NONE => error ("No mode for parameter variable " ^ x)) + | all_derivations_of thy modes vs (Const (s, T)) = the (lookup_mode modes (Const (s, T))) + | all_derivations_of thy modes vs (Free (x, T)) = the (lookup_mode modes (Free (x, T))) | all_derivations_of _ modes vs _ = error "all_derivations_of" fun rev_option_ord ord (NONE, NONE) = EQUAL @@ -1097,7 +1129,7 @@ SOME (s, _) => (case AList.lookup (op =) modes s of SOME ms => - (case AList.lookup (op =) ms (head_mode_of deriv) of + (case AList.lookup (op =) (map (fn ((p, m), r) => (m, r)) ms) (head_mode_of deriv) of SOME r => r | NONE => false) | NONE => false) @@ -1146,51 +1178,56 @@ tracing ("modes: " ^ (commas (map (fn (s, ms) => s ^ ": " ^ commas (map (fn (m, r) => string_of_mode m ^ (if r then " random " else " not ")) ms)) modes))) -fun select_mode_prem' thy modes vs ps = +fun select_mode_prem mode_analysis_options thy pol (modes, (pos_modes, neg_modes)) vs ps = let - val modes' = map (fn (s, ms) => (s, map fst ms)) modes + fun choose_mode_of_prem (Prem t) = partial_hd + (sort (deriv_ord2 thy modes t) (all_derivations_of thy pos_modes vs t)) + | choose_mode_of_prem (Sidecond t) = SOME (Context Bool, missing_vars vs t) + | choose_mode_of_prem (Negprem t) = partial_hd + (sort (deriv_ord2 thy modes t) (filter (fn (d, missing_vars) => is_all_input (head_mode_of d)) + (all_derivations_of thy neg_modes vs t))) + | choose_mode_of_prem p = error ("choose_mode_of_prem: " ^ string_of_prem thy p) in - partial_hd (sort (premise_ord thy modes) (ps ~~ map - (fn Prem t => - partial_hd - (sort (deriv_ord2 thy modes t) (all_derivations_of thy modes' vs t)) - | Sidecond t => SOME (Context Bool, missing_vars vs t) - | Negprem t => - partial_hd - (sort (deriv_ord2 thy modes t) (filter (fn (d, missing_vars) => is_all_input (head_mode_of d)) - (all_derivations_of thy modes' vs t))) - | p => error (string_of_prem thy p)) - ps)) + if #reorder_premises mode_analysis_options then + partial_hd (sort (premise_ord thy modes) (ps ~~ map choose_mode_of_prem ps)) + else + SOME (hd ps, choose_mode_of_prem (hd ps)) end -fun check_mode_clause' use_random thy param_vs modes mode (ts, ps) = +fun check_mode_clause' mode_analysis_options thy param_vs (modes : + (string * ((bool * mode) * bool) list) list) ((pol, mode) : bool * mode) (ts, ps) = let val vTs = distinct (op =) (fold Term.add_frees (map term_of_prem ps) (fold Term.add_frees ts [])) - val modes' = modes @ (param_vs ~~ map (fn x => [(x, false)]) (ho_arg_modes_of mode)) - val (in_ts, out_ts) = split_mode mode ts + val modes' = modes @ (param_vs ~~ map (fn x => [((true, x), false), ((false, x), false)]) (ho_arg_modes_of mode)) + fun retrieve_modes_of_pol pol = map (fn (s, ms) => + (s, map_filter (fn ((p, m), r) => if p = pol then SOME m else NONE | _ => NONE) ms)) + val (pos_modes', neg_modes') = + if #infer_pos_and_neg_modes mode_analysis_options then + (retrieve_modes_of_pol pol modes', retrieve_modes_of_pol (not pol) modes') + else + let + val modes = map (fn (s, ms) => (s, map (fn ((p, m), r) => m) ms)) modes' + in (modes, modes) end + val (in_ts, out_ts) = split_mode mode ts val in_vs = maps (vars_of_destructable_term thy) in_ts val out_vs = terms_vs out_ts + fun known_vs_after p vs = (case p of + Prem t => union (op =) vs (term_vs t) + | Sidecond t => union (op =) vs (term_vs t) + | Negprem t => union (op =) vs (term_vs t) + | _ => error "I do not know") fun check_mode_prems acc_ps rnd vs [] = SOME (acc_ps, vs, rnd) | check_mode_prems acc_ps rnd vs ps = - (case select_mode_prem' thy modes' vs ps of - SOME (p, SOME (deriv, [])) => check_mode_prems ((p, deriv) :: acc_ps) rnd (*TODO: uses random? *) - (case p of - Prem t => union (op =) vs (term_vs t) - | Sidecond t => vs - | Negprem t => union (op =) vs (term_vs t) - | _ => error "I do not know") - (filter_out (equal p) ps) + (case + (select_mode_prem mode_analysis_options thy pol (modes', (pos_modes', neg_modes')) vs ps) of + SOME (p, SOME (deriv, [])) => check_mode_prems ((p, deriv) :: acc_ps) rnd + (known_vs_after p vs) (filter_out (equal p) ps) | SOME (p, SOME (deriv, missing_vars)) => - if use_random then + if #use_random mode_analysis_options andalso pol then check_mode_prems ((p, deriv) :: (map - (fn v => (Generator (v, the (AList.lookup (op =) vTs v)), Term Output)) missing_vars) - @ acc_ps) true - (case p of - Prem t => union (op =) vs (term_vs t) - | Sidecond t => union (op =) vs (term_vs t) - | Negprem t => union (op =) vs (term_vs t) - | _ => error "I do not know") - (filter_out (equal p) ps) + (fn v => (Generator (v, the (AList.lookup (op =) vTs v)), Term Output)) + (distinct (op =) missing_vars)) + @ acc_ps) true (known_vs_after p vs) (filter_out (equal p) ps) else NONE | SOME (p, NONE) => NONE | NONE => NONE) @@ -1201,11 +1238,11 @@ if forall (is_constructable thy vs) (in_ts @ out_ts) then SOME (ts, rev acc_ps, rnd) else - if use_random then + if #use_random mode_analysis_options andalso pol then let - val generators = map + val generators = map (fn v => (Generator (v, the (AList.lookup (op =) vTs v)), Term Output)) - (subtract (op =) vs (terms_vs out_ts)) + (subtract (op =) vs (terms_vs (in_ts @ out_ts))) in SOME (ts, rev (generators @ acc_ps), true) end @@ -1215,66 +1252,120 @@ datatype result = Success of bool | Error of string -fun check_modes_pred' use_random options thy param_vs clauses modes (p, ms) = +fun check_modes_pred' mode_analysis_options options thy param_vs clauses modes (p, (ms : ((bool * mode) * bool) list)) = let fun split xs = let fun split' [] (ys, zs) = (rev ys, rev zs) | split' ((m, Error z) :: xs) (ys, zs) = split' xs (ys, z :: zs) - | split' ((m, Success rnd) :: xs) (ys, zs) = split' xs ((m, rnd) :: ys, zs) + | split' (((m : bool * mode), Success rnd) :: xs) (ys, zs) = split' xs ((m, rnd) :: ys, zs) in split' xs ([], []) end val rs = these (AList.lookup (op =) clauses p) fun check_mode m = let - val res = map (check_mode_clause' use_random thy param_vs modes m) rs + val res = Output.cond_timeit false "work part of check_mode for one mode" (fn _ => + map (check_mode_clause' mode_analysis_options thy param_vs modes m) rs) in + Output.cond_timeit false "aux part of check_mode for one mode" (fn _ => case find_indices is_none res of [] => Success (exists (fn SOME (_, _, true) => true | _ => false) res) - | is => (print_failed_mode options thy modes p m rs is; Error (error_of p m is)) + | is => (print_failed_mode options thy modes p m rs is; Error (error_of p m is))) end - val res = map (fn (m, _) => (m, check_mode m)) ms + val _ = if show_mode_inference options then + tracing ("checking " ^ string_of_int (length ms) ^ " modes ...") + else () + val res = Output.cond_timeit false "check_mode" (fn _ => map (fn (m, _) => (m, check_mode m)) ms) val (ms', errors) = split res in - ((p, ms'), errors) + ((p, (ms' : ((bool * mode) * bool) list)), errors) end; -fun get_modes_pred' use_random thy param_vs clauses modes (p, ms) = +fun get_modes_pred' mode_analysis_options thy param_vs clauses modes (p, ms) = let val rs = these (AList.lookup (op =) clauses p) in (p, map (fn (m, rnd) => - (m, map ((fn (ts, ps, rnd) => (ts, ps)) o the o check_mode_clause' use_random thy param_vs modes m) rs)) ms) + (m, map + ((fn (ts, ps, rnd) => (ts, ps)) o the o + check_mode_clause' mode_analysis_options thy param_vs modes m) rs)) ms) end; -fun fixp f x = +fun fixp f (x : (string * ((bool * mode) * bool) list) list) = let val y = f x in if x = y then x else fixp f y end; -fun fixp_with_state f (x, state) = +fun fixp_with_state f (x : (string * ((bool * mode) * bool) list) list, state) = let val (y, state') = f (x, state) in if x = y then (y, state') else fixp_with_state f (y, state') end -fun infer_modes use_random options preds extra_modes param_vs clauses thy = +fun string_of_ext_mode ((pol, mode), rnd) = + string_of_mode mode ^ "(" ^ (if pol then "pos" else "neg") ^ ", " + ^ (if rnd then "rnd" else "nornd") ^ ")" + +fun print_extra_modes options modes = + if show_mode_inference options then + tracing ("Modes of inferred predicates: " ^ + cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map string_of_ext_mode ms)) modes)) + else () + +fun infer_modes mode_analysis_options options compilation preds all_modes param_vs clauses thy = let - val all_modes = map (fn (s, T) => (s, map (rpair false) (all_modes_of_typ T))) preds - fun needs_random s m = (m, member (op =) (#needs_random (the_pred_data thy s)) m) - val extra_modes = map (fn (s, ms) => (s, map (needs_random s) ms)) extra_modes - val (modes, errors) = - fixp_with_state (fn (modes, errors) => + val collect_errors = false + fun appair f (x1, x2) (y1, y2) = (f x1 y1, f x2 y2) + fun needs_random s (false, m) = ((false, m), false) + | needs_random s (true, m) = ((true, m), member (op =) (#needs_random (the_pred_data thy s)) m) + fun add_polarity_and_random_bit s b ms = map (fn m => needs_random s (b, m)) ms + val prednames = map fst preds + (* extramodes contains all modes of all constants, should we only use the necessary ones + - what is the impact on performance? *) + val extra_modes = + if #infer_pos_and_neg_modes mode_analysis_options then let - val res = map - (check_modes_pred' use_random options thy param_vs clauses (modes @ extra_modes)) modes - in (map fst res, errors @ maps snd res) end) - (all_modes, []) + val pos_extra_modes = + all_modes_of compilation thy |> filter_out (fn (name, _) => member (op =) prednames name) + val neg_extra_modes = + all_modes_of (negative_compilation_of compilation) thy + |> filter_out (fn (name, _) => member (op =) prednames name) + in + map (fn (s, ms) => (s, (add_polarity_and_random_bit s true ms) + @ add_polarity_and_random_bit s false (the (AList.lookup (op =) neg_extra_modes s)))) + pos_extra_modes + end + else + map (fn (s, ms) => (s, (add_polarity_and_random_bit s true ms))) + (all_modes_of compilation thy |> filter_out (fn (name, _) => member (op =) prednames name)) + val _ = print_extra_modes options extra_modes + val start_modes = + if #infer_pos_and_neg_modes mode_analysis_options then + map (fn (s, ms) => (s, map (fn m => ((true, m), false)) ms @ + (map (fn m => ((false, m), false)) ms))) all_modes + else + map (fn (s, ms) => (s, map (fn m => ((true, m), false)) ms)) all_modes + fun iteration modes = map + (check_modes_pred' mode_analysis_options options thy param_vs clauses (modes @ extra_modes)) + modes + val ((modes : (string * ((bool * mode) * bool) list) list), errors) = + Output.cond_timeit false "Fixpount computation of mode analysis" (fn () => + if collect_errors then + fixp_with_state (fn (modes, errors) => + let + val (modes', new_errors) = split_list (iteration modes) + in (modes', errors @ flat new_errors) end) (start_modes, []) + else + (fixp (fn modes => map fst (iteration modes)) start_modes, [])) + val moded_clauses = map (get_modes_pred' mode_analysis_options thy param_vs clauses + (modes @ extra_modes)) modes val thy' = fold (fn (s, ms) => if member (op =) (map fst preds) s then - set_needs_random s (map fst (filter (fn (_, rnd) => rnd = true) ms)) else I) modes thy + set_needs_random s (map_filter (fn ((true, m), true) => SOME m | _ => NONE) ms) else I) + modes thy + in - ((map (get_modes_pred' use_random thy param_vs clauses (modes @ extra_modes)) modes, errors), thy') + ((moded_clauses, errors), thy') end; (* term construction *) @@ -1414,14 +1505,25 @@ (v', mk_bot compfuns U')])) end; -fun compile_expr compilation_modifiers compfuns thy (t, deriv) additional_arguments = +fun string_of_tderiv thy (t, deriv) = + (case (t, deriv) of + (t1 $ t2, Mode_App (deriv1, deriv2)) => + string_of_tderiv thy (t1, deriv1) ^ " $ " ^ string_of_tderiv thy (t2, deriv2) + | (Const ("Pair", _) $ t1 $ t2, Mode_Pair (deriv1, deriv2)) => + "(" ^ string_of_tderiv thy (t1, deriv1) ^ ", " ^ string_of_tderiv thy (t2, deriv2) ^ ")" + | (t, Term Input) => Syntax.string_of_term_global thy t ^ "[Input]" + | (t, Term Output) => Syntax.string_of_term_global thy t ^ "[Output]" + | (t, Context m) => Syntax.string_of_term_global thy t ^ "[" ^ string_of_mode m ^ "]") + +fun compile_expr compilation_modifiers compfuns thy pol (t, deriv) additional_arguments = let fun expr_of (t, deriv) = (case (t, deriv) of (t, Term Input) => SOME t | (t, Term Output) => NONE | (Const (name, T), Context mode) => - SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers) thy name mode, + SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers) thy name + (pol, mode), Comp_Mod.funT_of compilation_modifiers mode T)) | (Free (s, T), Context m) => SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T)) @@ -1446,7 +1548,7 @@ end fun compile_clause compilation_modifiers compfuns thy all_vs param_vs additional_arguments - mode inp (ts, moded_ps) = + (pol, mode) inp (ts, moded_ps) = let val iss = ho_arg_modes_of mode val compile_match = compile_match compilation_modifiers compfuns @@ -1479,7 +1581,7 @@ let val u = compile_expr compilation_modifiers compfuns thy - (t, deriv) additional_arguments' + pol (t, deriv) additional_arguments' val (_, out_ts''') = split_mode mode (snd (strip_comb t)) val rest = compile_prems out_ts''' vs' names'' ps in @@ -1489,7 +1591,7 @@ let val u = mk_not compfuns (compile_expr compilation_modifiers compfuns thy - (t, deriv) additional_arguments') + (not pol) (t, deriv) additional_arguments') val (_, out_ts''') = split_mode mode (snd (strip_comb t)) val rest = compile_prems out_ts''' vs' names'' ps in @@ -1506,6 +1608,7 @@ | Generator (v, T) => let val u = mk_random T + val rest = compile_prems [Free (v, T)] vs' names'' ps; in (u, rest) @@ -1519,7 +1622,7 @@ mk_bind compfuns (mk_single compfuns inp, prem_t) end -fun compile_pred compilation_modifiers thy all_vs param_vs s T mode moded_cls = +fun compile_pred compilation_modifiers thy all_vs param_vs s T (pol, mode) moded_cls = let (* TODO: val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers (all_vs @ param_vs) @@ -1547,14 +1650,14 @@ (fn t as Free (x, _) => if member (op =) param_vs x then NONE else SOME t | t => SOME t)) in_ts val cl_ts = map (compile_clause compilation_modifiers compfuns - thy all_vs param_vs additional_arguments mode (HOLogic.mk_tuple in_ts')) moded_cls; + thy all_vs param_vs additional_arguments (pol, mode) (HOLogic.mk_tuple in_ts')) moded_cls; val compilation = Comp_Mod.wrap_compilation compilation_modifiers compfuns s T mode additional_arguments (if null cl_ts then mk_bot compfuns (HOLogic.mk_tupleT outTs) else foldr1 (mk_sup compfuns) cl_ts) val fun_const = - Const (function_name_of (Comp_Mod.compilation compilation_modifiers) thy s mode, funT) + Const (function_name_of (Comp_Mod.compilation compilation_modifiers) thy s (pol, mode), funT) in HOLogic.mk_Trueprop (HOLogic.mk_eq (list_comb (fun_const, in_ts @ additional_arguments), compilation)) @@ -1583,13 +1686,20 @@ | strip_split_abs (Abs (_, _, t)) = strip_split_abs t | strip_split_abs t = t -fun mk_args is_eval (Pair (m1, m2), Type ("*", [T1, T2])) names = - let - val (t1, names') = mk_args is_eval (m1, T1) names - val (t2, names'') = mk_args is_eval (m2, T2) names' - in - (HOLogic.mk_prod (t1, t2), names'') - end +fun mk_args is_eval (m as Pair (m1, m2), T as Type ("*", [T1, T2])) names = + if eq_mode (m, Input) orelse eq_mode (m, Output) then + let + val x = Name.variant names "x" + in + (Free (x, T), x :: names) + end + else + let + val (t1, names') = mk_args is_eval (m1, T1) names + val (t2, names'') = mk_args is_eval (m2, T2) names' + in + (HOLogic.mk_prod (t1, t2), names'') + end | mk_args is_eval ((m as Fun _), T) names = let val funT = funT_of PredicateCompFuns.compfuns m T @@ -1828,11 +1938,11 @@ (* corresponds to compile_fun -- maybe call that also compile_sidecond? *) -fun prove_sidecond thy modes t = +fun prove_sidecond thy t = let fun preds_of t nameTs = case strip_comb t of (f as Const (name, T), args) => - if AList.defined (op =) modes name then (name, T) :: nameTs + if is_registered thy name then (name, T) :: nameTs else fold preds_of args nameTs | _ => nameTs val preds = preds_of t [] @@ -1847,7 +1957,7 @@ (* need better control here! *) end -fun prove_clause options thy nargs modes mode (_, clauses) (ts, moded_ps) = +fun prove_clause options thy nargs mode (_, clauses) (ts, moded_ps) = let val (in_ts, clause_out_ts) = split_mode mode ts; fun prove_prems out_ts [] = @@ -1911,7 +2021,7 @@ | Sidecond t => rtac @{thm if_predI} 1 THEN print_tac' options "before sidecond:" - THEN prove_sidecond thy modes t + THEN prove_sidecond thy t THEN print_tac' options "after sidecond:" THEN prove_prems [] ps) in (prove_match options thy out_ts) @@ -1929,7 +2039,7 @@ | select_sup _ 1 = [rtac @{thm supI1}] | select_sup n i = (rtac @{thm supI2})::(select_sup (n - 1) (i - 1)); -fun prove_one_direction options thy clauses preds modes pred mode moded_clauses = +fun prove_one_direction options thy clauses preds pred mode moded_clauses = let val T = the (AList.lookup (op =) preds pred) val nargs = length (binder_types T) @@ -1942,7 +2052,7 @@ THEN (EVERY (map (fn i => EVERY' (select_sup (length moded_clauses) i) i) (1 upto (length moded_clauses)))) - THEN (EVERY (map2 (prove_clause options thy nargs modes mode) clauses moded_clauses)) + THEN (EVERY (map2 (prove_clause options thy nargs mode) clauses moded_clauses)) THEN print_tac' options "proved one direction" end; @@ -2026,10 +2136,10 @@ (* FIXME: what is this for? *) (* replace defined by has_mode thy pred *) (* TODO: rewrite function *) -fun prove_sidecond2 thy modes t = let +fun prove_sidecond2 thy t = let fun preds_of t nameTs = case strip_comb t of (f as Const (name, T), args) => - if AList.defined (op =) modes name then (name, T) :: nameTs + if is_registered thy name then (name, T) :: nameTs else fold preds_of args nameTs | _ => nameTs val preds = preds_of t [] @@ -2044,7 +2154,7 @@ THEN print_tac "after sidecond2 simplification" end -fun prove_clause2 thy modes pred mode (ts, ps) i = +fun prove_clause2 thy pred mode (ts, ps) i = let val pred_intro_rule = nth (intros_of thy pred) (i - 1) val (in_ts, clause_out_ts) = split_mode mode ts; @@ -2102,7 +2212,7 @@ | Sidecond t => etac @{thm bindE} 1 THEN etac @{thm if_predE} 1 - THEN prove_sidecond2 thy modes t + THEN prove_sidecond2 thy t THEN prove_prems2 [] ps) in print_tac "before prove_match2:" THEN prove_match2 thy out_ts @@ -2119,11 +2229,11 @@ THEN prems_tac end; -fun prove_other_direction options thy modes pred mode moded_clauses = +fun prove_other_direction options thy pred mode moded_clauses = let fun prove_clause clause i = (if i < length moded_clauses then etac @{thm supE} 1 else all_tac) - THEN (prove_clause2 thy modes pred mode clause i) + THEN (prove_clause2 thy pred mode clause i) in (DETERM (TRY (rtac @{thm unit.induct} 1))) THEN (REPEAT_DETERM (CHANGED (rewtac @{thm split_paired_all}))) @@ -2136,7 +2246,7 @@ (** proof procedure **) -fun prove_pred options thy clauses preds modes pred mode (moded_clauses, compiled_term) = +fun prove_pred options thy clauses preds pred (pol, mode) (moded_clauses, compiled_term) = let val ctxt = ProofContext.init thy val clauses = case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => [] @@ -2146,9 +2256,9 @@ (fn _ => rtac @{thm pred_iffI} 1 THEN print_tac' options "after pred_iffI" - THEN prove_one_direction options thy clauses preds modes pred mode moded_clauses + THEN prove_one_direction options thy clauses preds pred mode moded_clauses THEN print_tac' options "proved one direction" - THEN prove_other_direction options thy modes pred mode moded_clauses + THEN prove_other_direction options thy pred mode moded_clauses THEN print_tac' options "proved other direction") else (fn _ => Skip_Proof.cheat_tac thy)) end; @@ -2173,11 +2283,11 @@ map_preds_modes (fn pred => compile_pred comp_modifiers thy all_vs param_vs pred (the (AList.lookup (op =) preds pred))) moded_clauses -fun prove options thy clauses preds modes moded_clauses compiled_terms = - map_preds_modes (prove_pred options thy clauses preds modes) +fun prove options thy clauses preds moded_clauses compiled_terms = + map_preds_modes (prove_pred options thy clauses preds) (join_preds_modes moded_clauses compiled_terms) -fun prove_by_skip options thy _ _ _ _ compiled_terms = +fun prove_by_skip options thy _ _ _ compiled_terms = map_preds_modes (fn pred => fn mode => fn t => Drule.export_without_context (Skip_Proof.make_thm thy t)) compiled_terms @@ -2204,9 +2314,13 @@ val ([preds, intrs], _) = fold_burrow (Variable.import_terms false) [preds, intrs] (ProofContext.init thy) val preds = map dest_Const preds - val extra_modes = - all_modes_of compilation thy |> filter_out (fn (name, _) => member (op =) prednames name) val all_vs = terms_vs intrs + val all_modes = + map (fn (s, T) => + (s, + (if member (op =) (no_higher_order_predicate options) s then + (all_smodes_of_typ T) + else (all_modes_of_typ T)))) preds val params = case intrs of [] => @@ -2219,8 +2333,12 @@ in map2 (curry Free) param_names paramTs end - | (intr :: _) => maps extract_params - (snd (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr)))) + | (intr :: _) => + let + val (p, args) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr)) + in + ho_args_of (hd (the (AList.lookup (op =) all_modes (fst (dest_Const p))))) args + end val param_vs = map (fst o dest_Free) params fun add_clause intr clauses = let @@ -2232,7 +2350,7 @@ end; val clauses = fold add_clause intrs [] in - (preds, all_vs, param_vs, extra_modes, clauses) + (preds, all_vs, param_vs, all_modes, clauses) end; (* sanity check of introduction rules *) @@ -2294,7 +2412,7 @@ val arg_names = Name.variant_list [] (map (fn i => "x" ^ string_of_int i) (1 upto length Ts)) val args = map2 (curry Free) arg_names Ts - val predfun = Const (function_name_of Pred thy predname full_mode, + val predfun = Const (function_name_of Pred thy predname (true, full_mode), Ts ---> PredicateCompFuns.mk_predT @{typ unit}) val rhs = @{term Predicate.holds} $ (list_comb (predfun, args)) val eq_term = HOLogic.mk_Trueprop @@ -2317,20 +2435,20 @@ datatype steps = Steps of { - define_functions : options -> (string * typ) list -> string * mode list -> theory -> theory, - infer_modes : options -> (string * typ) list -> (string * mode list) list + define_functions : options -> (string * typ) list -> string * (bool * mode) list -> theory -> theory, + (*infer_modes : options -> (string * typ) list -> (string * mode list) list -> string list -> (string * (term list * indprem list) list) list - -> theory -> ((moded_clause list pred_mode_table * string list) * theory), - prove : options -> theory -> (string * (term list * indprem list) list) list - -> (string * typ) list -> (string * mode list) list + -> theory -> ((moded_clause list pred_mode_table * string list) * theory),*) + prove : options -> theory -> (string * (term list * indprem list) list) list -> (string * typ) list -> moded_clause list pred_mode_table -> term pred_mode_table -> thm pred_mode_table, add_code_equations : theory -> (string * typ) list -> (string * thm list) list -> (string * thm list) list, comp_modifiers : Comp_Mod.comp_modifiers, + use_random : bool, qname : bstring } -fun add_equations_of steps options prednames thy = +fun add_equations_of steps mode_analysis_options options prednames thy = let fun dest_steps (Steps s) = s val _ = print_step options @@ -2338,14 +2456,20 @@ (*val _ = check_intros_elim_match thy prednames*) (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*) val compilation = Comp_Mod.compilation (#comp_modifiers (dest_steps steps)) - val (preds, all_vs, param_vs, extra_modes, clauses) = + val _ = + if show_intermediate_results options then + tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames))) + else () + val (preds, all_vs, param_vs, all_modes, clauses) = prepare_intrs options compilation thy prednames (maps (intros_of thy) prednames) val _ = print_step options "Infering modes..." val ((moded_clauses, errors), thy') = - #infer_modes (dest_steps steps) options preds extra_modes param_vs clauses thy + (*Output.cond_timeit true "Infering modes" + (fn _ =>*) infer_modes mode_analysis_options + options compilation preds all_modes param_vs clauses thy val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses val _ = check_expected_modes preds options modes - val _ = check_proposed_modes preds options modes extra_modes errors + (*val _ = check_proposed_modes preds options modes (fst extra_modes) errors*) val _ = print_modes options thy' modes val _ = print_step options "Defining executable functions..." val thy'' = fold (#define_functions (dest_steps steps) options preds) modes thy' @@ -2355,8 +2479,8 @@ compile_preds (#comp_modifiers (dest_steps steps)) thy'' all_vs param_vs preds moded_clauses val _ = print_compiled_terms options thy'' compiled_terms val _ = print_step options "Proving equations..." - val result_thms = #prove (dest_steps steps) options thy'' clauses preds (extra_modes @ modes) - moded_clauses compiled_terms + val result_thms = + #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms val result_thms' = #add_code_equations (dest_steps steps) thy'' preds (maps_modes result_thms) val qname = #qname (dest_steps steps) @@ -2398,7 +2522,14 @@ val thy'' = fold_rev (fn preds => fn thy => if not (forall (defined thy) preds) then - add_equations_of steps options preds thy + let + val mode_analysis_options = {use_random = #use_random (dest_steps steps), + reorder_premises = + not (no_topmost_reordering options andalso not (null (inter (op =) preds names))), + infer_pos_and_neg_modes = #use_random (dest_steps steps)} + in + add_equations_of steps mode_analysis_options options preds thy + end else thy) scc thy' |> Theory.checkpoint in thy'' end @@ -2468,11 +2599,15 @@ } val add_equations = gen_add_equations - (Steps {infer_modes = infer_modes false, - define_functions = create_definitions, + (Steps { + define_functions = + fn options => fn preds => fn (s, modes) => + create_definitions + options preds (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes), prove = prove, add_code_equations = add_code_equations, comp_modifiers = predicate_comp_modifiers, + use_random = false, qname = "equation"}) val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers @@ -2499,9 +2634,9 @@ transform_additional_arguments = K I : (indprem -> term list -> term list) } -val random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers +val pos_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers { - compilation = Random_DSeq, + compilation = Pos_Random_DSeq, function_name_prefix = "random_dseq_", compfuns = Random_Sequence_CompFuns.compfuns, additional_arguments = K [], @@ -2510,6 +2645,17 @@ transform_additional_arguments = K I : (indprem -> term list -> term list) } +val neg_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers + { + compilation = Neg_Random_DSeq, + function_name_prefix = "random_dseq_neg_", + compfuns = Random_Sequence_CompFuns.compfuns, + additional_arguments = K [], + wrap_compilation = K (K (K (K (K I)))) + : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), + transform_additional_arguments = K I : (indprem -> term list -> term list) + } + (* val add_depth_limited_equations = gen_add_equations (Steps {infer_modes = infer_modes, @@ -2521,11 +2667,15 @@ qname = "depth_limited_equation"}) *) val add_annotated_equations = gen_add_equations - (Steps {infer_modes = infer_modes false, - define_functions = define_functions annotated_comp_modifiers PredicateCompFuns.compfuns, + (Steps { + define_functions = + fn options => fn preds => fn (s, modes) => + define_functions annotated_comp_modifiers PredicateCompFuns.compfuns options preds + (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes), prove = prove_by_skip, add_code_equations = K (K I), comp_modifiers = annotated_comp_modifiers, + use_random = false, qname = "annotated_equation"}) (* val add_quickcheck_equations = gen_add_equations @@ -2538,19 +2688,33 @@ qname = "random_equation"}) *) val add_dseq_equations = gen_add_equations - (Steps {infer_modes = infer_modes false, - define_functions = define_functions dseq_comp_modifiers DSequence_CompFuns.compfuns, + (Steps { + define_functions = + fn options => fn preds => fn (s, modes) => + define_functions dseq_comp_modifiers DSequence_CompFuns.compfuns + options preds (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes), prove = prove_by_skip, add_code_equations = K (K I), comp_modifiers = dseq_comp_modifiers, + use_random = false, qname = "dseq_equation"}) val add_random_dseq_equations = gen_add_equations - (Steps {infer_modes = infer_modes true, - define_functions = define_functions random_dseq_comp_modifiers Random_Sequence_CompFuns.compfuns, + (Steps { + define_functions = + fn options => fn preds => fn (s, modes) => + let + val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes + val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes + in define_functions pos_random_dseq_comp_modifiers Random_Sequence_CompFuns.compfuns + options preds (s, pos_modes) + #> define_functions neg_random_dseq_comp_modifiers Random_Sequence_CompFuns.compfuns + options preds (s, neg_modes) + end, prove = prove_by_skip, add_code_equations = K (K I), - comp_modifiers = random_dseq_comp_modifiers, + comp_modifiers = pos_random_dseq_comp_modifiers, + use_random = true, qname = "random_dseq_equation"}) @@ -2700,8 +2864,8 @@ | Depth_Limited => depth_limited_comp_modifiers | Annotated => annotated_comp_modifiers*) | DSeq => dseq_comp_modifiers - | Random_DSeq => random_dseq_comp_modifiers - val t_pred = compile_expr comp_modifiers compfuns thy (body, deriv) additional_arguments; + | Random_DSeq => pos_random_dseq_comp_modifiers + val t_pred = compile_expr comp_modifiers compfuns thy true (body, deriv) additional_arguments; val T_pred = dest_predT compfuns (fastype_of t_pred) val arrange = split_lambda (HOLogic.mk_tuple outargs) output_tuple in @@ -2717,7 +2881,7 @@ case compilation of Random => RandomPredCompFuns.compfuns | DSeq => DSequence_CompFuns.compfuns - | Random_DSeq => Random_Sequence_CompFuns.compfuns + | Pos_Random_DSeq => Random_Sequence_CompFuns.compfuns | _ => PredicateCompFuns.compfuns val t = analyze_compr thy compfuns param_user_modes options t_compr; val T = dest_predT compfuns (fastype_of t); @@ -2729,7 +2893,7 @@ (Code_Eval.eval NONE ("Predicate_Compile_Core.random_eval_ref", random_eval_ref) (fn proc => fn g => fn s => g s |>> Predicate.map proc) thy t' [] |> Random_Engine.run)) - | Random_DSeq => + | Pos_Random_DSeq => let val [nrandom, size, depth] = arguments in diff -r 997aa3a3e4bb -r c9f428269b38 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Tue Feb 23 10:02:14 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Tue Feb 23 13:36:15 2010 +0100 @@ -6,11 +6,17 @@ signature PREDICATE_COMPILE_DATA = sig - type specification_table; - (*val make_const_spec_table : Predicate_Compile_Aux.options -> theory -> specification_table*) - val get_specification : theory -> term -> thm list + val ignore_consts : string list -> theory -> theory + val keep_functions : string list -> theory -> theory + val keep_function : theory -> string -> bool + val processed_specs : theory -> string -> (string * thm list) list option + val store_processed_specs : (string * (string * thm list) list) -> theory -> theory + + val get_specification : Predicate_Compile_Aux.options -> theory -> term -> thm list val obtain_specification_graph : Predicate_Compile_Aux.options -> theory -> term -> thm list TermGraph.T + + val present_graph : thm list TermGraph.T -> unit val normalize_equation : theory -> thm -> thm end; @@ -22,20 +28,39 @@ structure Data = Theory_Data ( type T = - {const_spec_table : thm list Symtab.table}; + {ignore_consts : unit Symtab.table, + keep_functions : unit Symtab.table, + processed_specs : ((string * thm list) list) Symtab.table}; val empty = - {const_spec_table = Symtab.empty}; + {ignore_consts = Symtab.empty, + keep_functions = Symtab.empty, + processed_specs = Symtab.empty}; val extend = I; fun merge - ({const_spec_table = const_spec_table1}, - {const_spec_table = const_spec_table2}) = - {const_spec_table = Symtab.merge (K true) (const_spec_table1, const_spec_table2)} + ({ignore_consts = c1, keep_functions = k1, processed_specs = s1}, + {ignore_consts = c2, keep_functions = k2, processed_specs = s2}) = + {ignore_consts = Symtab.merge (K true) (c1, c2), + keep_functions = Symtab.merge (K true) (k1, k2), + processed_specs = Symtab.merge (K true) (s1, s2)} ); -fun mk_data c = {const_spec_table = c} -fun map_data f {const_spec_table = c} = mk_data (f c) + + +fun mk_data (c, k, s) = {ignore_consts = c, keep_functions = k, processed_specs = s} +fun map_data f {ignore_consts = c, keep_functions = k, processed_specs = s} = mk_data (f (c, k, s)) + +fun ignore_consts cs = Data.map (map_data (apfst3 (fold (fn c => Symtab.insert (op =) (c, ())) cs))) + +fun keep_functions cs = Data.map (map_data (apsnd3 (fold (fn c => Symtab.insert (op =) (c, ())) cs))) -type specification_table = thm list Symtab.table +fun keep_function thy = Symtab.defined (#keep_functions (Data.get thy)) + +fun processed_specs thy = Symtab.lookup (#processed_specs (Data.get thy)) + +fun store_processed_specs (constname, specs) = + Data.map (map_data (aptrd3 (Symtab.update_new (constname, specs)))) +(* *) + fun defining_term_of_introrule_term t = let @@ -120,17 +145,11 @@ val t' = Pattern.rewrite_term thy rewr [] t val tac = Skip_Proof.cheat_tac thy val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn _ => tac) - val th''' = LocalDefs.unfold ctxt [@{thm split_conv}] th'' + val th''' = LocalDefs.unfold ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th'' in th''' end; -fun normalize_equation thy th = - mk_meta_equation th - |> Predicate_Compile_Set.unfold_set_notation - |> full_fun_cong_expand - |> split_all_pairs thy - |> tap check_equation_format fun inline_equations thy th = let @@ -143,69 +162,58 @@ in th' end -(* -fun store_thm_in_table options ignore thy th= - let - val th = th - |> inline_equations options thy - |> Predicate_Compile_Set.unfold_set_notation - |> AxClass.unoverload thy - val (const, th) = - if is_equationlike th then - let - val eq = normalize_equation thy th - in - (defining_const_of_equation eq, eq) - end - else if is_introlike th then (defining_const_of_introrule th, th) - else error "store_thm: unexpected definition format" - in - if ignore const then I else Symtab.cons_list (const, th) - end + +fun normalize_equation thy th = + mk_meta_equation th + |> full_fun_cong_expand + |> split_all_pairs thy + |> tap check_equation_format + |> inline_equations thy -fun make_const_spec_table options thy = +fun normalize_intros thy th = + split_all_pairs thy th + |> inline_equations thy + +fun normalize thy th = + if is_equationlike th then + normalize_equation thy th + else + normalize_intros thy th + +fun get_specification options thy t = let - fun store ignore f = - fold (store_thm_in_table options ignore thy) - (map (Thm.transfer thy) (f )) - val table = Symtab.empty - |> store (K false) Predicate_Compile_Alternative_Defs.get - val ignore = Symtab.defined table - in - table - |> store ignore (fn ctxt => maps - else []) - - |> store ignore Nitpick_Simps.get - |> store ignore Nitpick_Intros.get - end - -fun get_specification table constname = - case Symtab.lookup table constname of - SOME thms => thms - | NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed") -*) - -fun get_specification thy t = - Output.cond_timeit true "get_specification" (fn () => - let + (*val (c, T) = dest_Const t + val t = Const (AxClass.unoverload_const thy (c, T), T)*) + val _ = if show_steps options then + tracing ("getting specification of " ^ Syntax.string_of_term_global thy t ^ + " with type " ^ Syntax.string_of_typ_global thy (fastype_of t)) + else () val ctxt = ProofContext.init thy fun filtering th = if is_equationlike th andalso - defining_const_of_equation (normalize_equation thy th) = (fst (dest_Const t)) then + defining_const_of_equation (normalize_equation thy th) = fst (dest_Const t) then SOME (normalize_equation thy th) else if is_introlike th andalso defining_term_of_introrule th = t then SOME th else NONE - in - case map_filter filtering (map (Thm.transfer thy) (Predicate_Compile_Alternative_Defs.get ctxt)) + val spec = case map_filter filtering (map (normalize thy o Thm.transfer thy) (Predicate_Compile_Alternative_Defs.get ctxt)) of [] => (case Spec_Rules.retrieve ctxt t - of [] => rev (map_filter filtering (map (Thm.transfer thy) (Nitpick_Intros.get ctxt))) + of [] => (case rev ( + (map_filter filtering (map (normalize_intros thy o Thm.transfer thy) + (Nitpick_Intros.get ctxt)))) + of [] => error ("No specification for " ^ (Syntax.string_of_term_global thy t)) + | ths => ths) | ((_, (_, ths)) :: _) => map (normalize_equation thy o Thm.transfer thy) ths) | ths => rev ths - end) + val _ = + if show_intermediate_results options then + Output.tracing (commas (map (Display.string_of_thm_global thy) spec)) + else () + in + spec + end val logic_operator_names = [@{const_name "=="}, @@ -216,7 +224,8 @@ @{const_name "op -->"}, @{const_name "All"}, @{const_name "Ex"}, - @{const_name "op &"}] + @{const_name "op &"}, + @{const_name "op |"}] fun special_cases (c, T) = member (op =) [ @{const_name Product_Type.Unity}, @@ -233,7 +242,11 @@ @{const_name Int.Bit1}, @{const_name Int.Pls}, @{const_name Int.zero_int_inst.zero_int}, - @{const_name List.filter}] c + @{const_name List.filter}, + @{const_name HOL.If}, + @{const_name Groups.minus} + ] c + fun print_specification options thy constname specs = if show_intermediate_results options then @@ -254,19 +267,43 @@ |> filter_out has_code_pred_intros |> filter_out case_consts |> filter_out special_cases + |> filter_out (fn (c, _) => Symtab.defined (#ignore_consts (Data.get thy)) c) + |> map (fn (c, _) => (c, Sign.the_const_constraint thy c)) |> map Const (* |> filter is_defining_constname*) fun extend t = let - val specs = get_specification thy t - |> map (inline_equations thy) + val specs = get_specification options thy t (*|> Predicate_Compile_Set.unfold_set_notation*) (*val _ = print_specification options thy constname specs*) in (specs, defiants_of specs) end; in TermGraph.extend extend t TermGraph.empty end; - + + +fun present_graph gr = + let + fun eq_cname (Const (c1, _), Const (c2, _)) = (c1 = c2) + fun string_of_const (Const (c, _)) = c + | string_of_const _ = error "string_of_const: unexpected term" + val constss = TermGraph.strong_conn gr; + val mapping = Termtab.empty |> fold (fn consts => fold (fn const => + Termtab.update (const, consts)) consts) constss; + fun succs consts = consts + |> maps (TermGraph.imm_succs gr) + |> subtract eq_cname consts + |> map (the o Termtab.lookup mapping) + |> distinct (eq_list eq_cname); + val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss; + + fun namify consts = map string_of_const consts + |> commas; + val prgr = map (fn (consts, constss) => + { name = namify consts, ID = namify consts, dir = "", unfold = true, + path = "", parents = map namify constss }) conn; + in Present.display_graph prgr end; + end; diff -r 997aa3a3e4bb -r c9f428269b38 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Tue Feb 23 10:02:14 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Tue Feb 23 13:36:15 2010 +0100 @@ -9,6 +9,8 @@ val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory val rewrite_intro : theory -> thm -> thm list val pred_of_function : theory -> string -> string option + + val add_function_predicate_translation : (term * term) -> theory -> theory end; structure Predicate_Compile_Fun : PREDICATE_COMPILE_FUN = @@ -16,19 +18,36 @@ open Predicate_Compile_Aux; -(* Table from constant name (string) to term of inductive predicate *) -structure Pred_Compile_Preproc = Theory_Data +(* Table from function to inductive predicate *) +structure Fun_Pred = Theory_Data ( - type T = string Symtab.table; - val empty = Symtab.empty; + type T = (term * term) Item_Net.T; + val empty = Item_Net.init (op aconv o pairself fst) (single o fst); val extend = I; - fun merge data : T = Symtab.merge (op =) data; (* FIXME handle Symtab.DUP ?? *) + val merge = Item_Net.merge; ) -fun pred_of_function thy name = Symtab.lookup (Pred_Compile_Preproc.get thy) name +fun lookup thy net t = + case Item_Net.retrieve net t of + [] => NONE + | [(f, p)] => + let + val subst = Pattern.match thy (f, t) (Vartab.empty, Vartab.empty) + in + SOME (Envir.subst_term subst p) + end + | _ => error ("Multiple matches possible for lookup of " ^ Syntax.string_of_term_global thy t) -fun defined thy = Symtab.defined (Pred_Compile_Preproc.get thy) +fun pred_of_function thy name = + case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, Term.dummyT)) of + [] => NONE + | [(f, p)] => SOME (fst (dest_Const p)) + | _ => error ("Multiple matches possible for lookup of constant " ^ name) +fun defined_const thy name = is_some (pred_of_function thy name) + +fun add_function_predicate_translation (f, p) = + Fun_Pred.map (Item_Net.update (f, p)) fun transform_ho_typ (T as Type ("fun", _)) = let @@ -63,27 +82,6 @@ (Free (Long_Name.base_name name ^ "P", pred_type T)) end -fun mk_param thy lookup_pred (t as Free (v, _)) = lookup_pred t - | mk_param thy lookup_pred t = - if Predicate_Compile_Aux.is_predT (fastype_of t) then - t - else - let - val (vs, body) = strip_abs t - val names = Term.add_free_names body [] - val vs_names = Name.variant_list names (map fst vs) - val vs' = map2 (curry Free) vs_names (map snd vs) - val body' = subst_bounds (rev vs', body) - val (f, args) = strip_comb body' - val resname = Name.variant (vs_names @ names) "res" - val resvar = Free (resname, body_type (fastype_of body')) - (*val P = case try lookup_pred f of SOME P => P | NONE => error "mk_param" - val pred_body = list_comb (P, args @ [resvar]) - *) - val pred_body = HOLogic.mk_eq (body', 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) *) @@ -92,22 +90,6 @@ val (func, args) = strip_comb lhs in ((func, args), rhs) end; -fun string_of_typ T = Syntax.string_of_typ_global @{theory} T - -fun string_of_term t = - case t of - Const (c, T) => "Const (" ^ c ^ ", " ^ string_of_typ T ^ ")" - | Free (c, T) => "Free (" ^ c ^ ", " ^ string_of_typ T ^ ")" - | Var ((c, i), T) => "Var ((" ^ c ^ ", " ^ string_of_int i ^ "), " ^ string_of_typ T ^ ")" - | Bound i => "Bound " ^ string_of_int i - | Abs (x, T, t) => "Abs (" ^ x ^ ", " ^ string_of_typ T ^ ", " ^ string_of_term t ^ ")" - | t1 $ t2 => "(" ^ string_of_term t1 ^ ") $ (" ^ string_of_term t2 ^ ")" - -fun ind_package_get_nparams thy name = - case try (Inductive.the_inductive (ProofContext.init thy)) name of - SOME (_, result) => length (Inductive.params_of (#raw_induct result)) - | NONE => error ("No such predicate: " ^ quote name) - (* TODO: does not work with higher order functions yet *) fun mk_rewr_eq (func, pred) = let @@ -122,49 +104,6 @@ (HOLogic.mk_eq (res, list_comb (func, args)), list_comb (pred, args @ [res])) end; -fun has_split_rule_cname @{const_name "nat_case"} = true - | has_split_rule_cname @{const_name "list_case"} = true - | has_split_rule_cname _ = false - -fun has_split_rule_term thy (Const (@{const_name "nat_case"}, _)) = true - | has_split_rule_term thy (Const (@{const_name "list_case"}, _)) = true - | has_split_rule_term thy _ = false - -fun has_split_rule_term' thy (Const (@{const_name "If"}, _)) = true - | has_split_rule_term' thy (Const (@{const_name "Let"}, _)) = true - | has_split_rule_term' thy c = has_split_rule_term thy c - -fun prepare_split_thm ctxt split_thm = - (split_thm RS @{thm iffD2}) - |> LocalDefs.unfold ctxt [@{thm atomize_conjL[symmetric]}, - @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}] - -fun find_split_thm thy (Const (name, typ)) = - let - fun split_name str = - case first_field "." str - of (SOME (field, rest)) => field :: split_name rest - | NONE => [str] - val splitted_name = split_name name - in - if length splitted_name > 0 andalso - String.isSuffix "_case" (List.last splitted_name) - then - (List.take (splitted_name, length splitted_name - 1)) @ ["split"] - |> space_implode "." - |> PureThy.get_thm thy - |> SOME - handle ERROR msg => NONE - else NONE - end - | find_split_thm _ _ = NONE - -fun find_split_thm' thy (Const (@{const_name "If"}, _)) = SOME @{thm split_if} - | find_split_thm' thy (Const (@{const_name "Let"}, _)) = SOME @{thm refl} (* TODO *) - | find_split_thm' thy c = find_split_thm thy c - -fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t) - fun folds_map f xs y = let fun folds_map' acc [] y = [(rev acc, y)] @@ -174,23 +113,91 @@ folds_map' [] xs y end; -fun mk_prems thy (lookup_pred, get_nparams) t (names, prems) = +fun keep_functions thy t = + case try dest_Const (fst (strip_comb t)) of + SOME (c, _) => Predicate_Compile_Data.keep_function thy c + | _ => false + +fun mk_prems thy lookup_pred t (names, prems) = let fun mk_prems' (t as Const (name, T)) (names, prems) = - if is_constr thy name orelse (is_none (try lookup_pred t)) then + (if is_constr thy name orelse (is_none (lookup_pred t)) then [(t, (names, prems))] - else [(lookup_pred t, (names, prems))] + else + (*(if is_none (try lookup_pred t) then + [(Abs ("uu", fastype_of t, HOLogic.mk_eq (t, Bound 0)), (names, prems))] + else*) [(the (lookup_pred t), (names, prems))]) | mk_prems' (t as Free (f, T)) (names, prems) = - [(lookup_pred t, (names, prems))] + (case lookup_pred t of + SOME t' => [(t', (names, prems))] + | NONE => [(t, (names, prems))]) | mk_prems' (t as Abs _) (names, prems) = if Predicate_Compile_Aux.is_predT (fastype_of t) then - [(t, (names, prems))] else error "mk_prems': Abs " - (* mk_param *) + ([(Envir.eta_contract t, (names, prems))]) + else + let + val (vars, body) = strip_abs t + val _ = assert (fastype_of body = body_type (fastype_of body)) + val absnames = Name.variant_list names (map fst vars) + val frees = map2 (curry Free) absnames (map snd vars) + val body' = subst_bounds (rev frees, body) + val resname = Name.variant (absnames @ names) "res" + val resvar = Free (resname, fastype_of body) + val t = mk_prems' body' ([], []) + |> map (fn (res, (inner_names, inner_prems)) => + let + fun mk_exists (x, T) t = HOLogic.mk_exists (x, T, t) + val vTs = + fold Term.add_frees inner_prems [] + |> filter (fn (x, T) => member (op =) inner_names x) + val t = + fold mk_exists vTs + (foldr1 HOLogic.mk_conj (HOLogic.mk_eq (resvar, res) :: + map HOLogic.dest_Trueprop inner_prems)) + in + t + end) + |> foldr1 HOLogic.mk_disj + |> fold lambda (resvar :: rev frees) + in + [(t, (names, prems))] + end | mk_prems' t (names, prems) = - if Predicate_Compile_Aux.is_constrt thy t then + if Predicate_Compile_Aux.is_constrt thy t orelse keep_functions thy t then [(t, (names, prems))] else - if has_split_rule_term' thy (fst (strip_comb t)) then + case (fst (strip_comb t)) of + Const (@{const_name "If"}, _) => + (let + val (_, [B, x, y]) = strip_comb t + in + (mk_prems' x (names, prems) + |> map (fn (res, (names, prems)) => (res, (names, (HOLogic.mk_Trueprop B) :: prems)))) + @ (mk_prems' y (names, prems) + |> map (fn (res, (names, prems)) => + (res, (names, (HOLogic.mk_Trueprop (HOLogic.mk_not B)) :: prems)))) + end) + | Const (@{const_name "Let"}, _) => + (let + val (_, [f, g]) = strip_comb t + in + mk_prems' f (names, prems) + |> maps (fn (res, (names, prems)) => + mk_prems' (betapply (g, res)) (names, prems)) + end) + | Const (@{const_name "split"}, _) => + (let + val (_, [g, res]) = strip_comb t + val [res1, res2] = Name.variant_list names ["res1", "res2"] + val (T1, T2) = HOLogic.dest_prodT (fastype_of res) + val (resv1, resv2) = (Free (res1, T1), Free (res2, T2)) + in + mk_prems' (betapplys (g, [resv1, resv2])) + (res1 :: res2 :: names, + HOLogic.mk_Trueprop (HOLogic.mk_eq (res, HOLogic.mk_prod (resv1, resv2))) :: prems) + end) + | _ => + if has_split_thm thy (fst (strip_comb t)) then let val (f, args) = strip_comb t val split_thm = prepare_split_thm (ProofContext.init thy) (the (find_split_thm' thy f)) @@ -208,8 +215,15 @@ val vars = map Free (var_names ~~ (map snd vTs)) val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm')) val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res) + val (lhss : term list, rhss) = + split_list (map (HOLogic.dest_eq o HOLogic.dest_Trueprop) prems') in - mk_prems' inner_t (var_names @ names, prems' @ prems) + folds_map mk_prems' lhss (var_names @ names, prems) + |> map (fn (ress, (names, prems)) => + let + val prems' = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (ress ~~ rhss) + in (names, prems' @ prems) end) + |> maps (mk_prems' inner_t) end in maps mk_prems_of_assm assms @@ -219,53 +233,77 @@ val (f, args) = strip_comb t (* TODO: special procedure for higher-order functions: split arguments in simple types and function types *) + val args = map (Pattern.eta_long []) args val resname = Name.variant names "res" val resvar = Free (resname, body_type (fastype_of t)) + val _ = assert (fastype_of t = body_type (fastype_of t)) val names' = resname :: names fun mk_prems'' (t as Const (c, _)) = - if is_constr thy c orelse (is_none (try lookup_pred t)) then + if is_constr thy c orelse (is_none (lookup_pred t)) then + let + val _ = ()(*tracing ("not translating function " ^ Syntax.string_of_term_global thy t)*) + in folds_map mk_prems' args (names', prems) |> map (fn (argvs, (names'', prems')) => let val prem = HOLogic.mk_Trueprop (HOLogic.mk_eq (resvar, list_comb (f, argvs))) in (names'', prem :: prems') end) + end else let - val pred = lookup_pred t - val nparams = get_nparams pred - val (params, args) = chop nparams args - val params' = map (mk_param thy lookup_pred) params + (* lookup_pred is falsch für polymorphe Argumente und bool. *) + val pred = the (lookup_pred t) + val Ts = binder_types (fastype_of pred) in folds_map mk_prems' args (names', prems) |> map (fn (argvs, (names'', prems')) => let - val prem = HOLogic.mk_Trueprop (list_comb (pred, params' @ argvs @ [resvar])) + fun lift_arg T t = + if (fastype_of t) = T then t + else + let + val _ = assert (T = + (binder_types (fastype_of t) @ [@{typ bool}] ---> @{typ bool})) + fun mk_if T (b, t, e) = + Const (@{const_name If}, @{typ bool} --> T --> T --> T) $ b $ t $ e + val Ts = binder_types (fastype_of t) + val t = + list_abs (map (pair "x") Ts @ [("b", @{typ bool})], + mk_if @{typ bool} (list_comb (t, map Bound (length Ts downto 1)), + HOLogic.mk_eq (@{term True}, Bound 0), + HOLogic.mk_eq (@{term False}, Bound 0))) + in + t + end + (*val _ = tracing ("Ts: " ^ commas (map (Syntax.string_of_typ_global thy) Ts)) + val _ = map2 check_arity Ts (map fastype_of (argvs @ [resvar]))*) + val argvs' = map2 lift_arg (fst (split_last Ts)) argvs + val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs' @ [resvar])) in (names'', prem :: prems') end) end | mk_prems'' (t as Free (_, _)) = - let - (* higher order argument call *) - val pred = lookup_pred t - in - folds_map mk_prems' args (resname :: names, prems) - |> map (fn (argvs, (names', prems')) => - let - val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs @ [resvar])) - in (names', prem :: prems') end) - end + folds_map mk_prems' args (names', prems) |> + map + (fn (argvs, (names'', prems')) => + let + val prem = + case lookup_pred t of + NONE => HOLogic.mk_Trueprop (HOLogic.mk_eq (resvar, list_comb (f, argvs))) + | SOME p => HOLogic.mk_Trueprop (list_comb (p, argvs @ [resvar])) + in (names'', prem :: prems') end) | mk_prems'' t = error ("Invalid term: " ^ Syntax.string_of_term_global thy t) in map (pair resvar) (mk_prems'' f) end in - mk_prems' t (names, prems) + mk_prems' (Pattern.eta_long [] t) (names, prems) end; (* assumption: mutual recursive predicates all have the same parameters. *) fun define_predicates specs thy = - if forall (fn (const, _) => member (op =) (Symtab.keys (Pred_Compile_Preproc.get thy)) const) specs then + if forall (fn (const, _) => defined_const thy const) specs then ([], thy) else let @@ -275,36 +313,20 @@ (* create prednames *) val ((funs, argss), rhss) = map_split dest_code_eqn eqns |>> split_list val argss' = map (map transform_ho_arg) argss - val pnames = map dest_Free (distinct (op =) (maps (filter (is_funtype o fastype_of)) argss')) + (* TODO: higher order arguments also occur in tuples! *) + val ho_argss = distinct (op =) (maps (filter (is_funtype o fastype_of)) argss) + val params = distinct (op =) (maps (filter (is_funtype o fastype_of)) argss') + val pnames = map dest_Free params val preds = map pred_of funs val prednames = map (fst o dest_Free) preds val funnames = map (fst o dest_Const) funs val fun_pred_names = (funnames ~~ prednames) (* mapping from term (Free or Const) to term *) - fun lookup_pred (Const (name, T)) = - (case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of - SOME c => Const (c, pred_type T) - | NONE => - (case AList.lookup op = fun_pred_names name of - SOME f => Free (f, pred_type T) - | NONE => Const (name, T))) - | lookup_pred (Free (name, T)) = - if member op = (map fst pnames) name then - Free (name, transform_ho_typ T) - else - Free (name, T) - | lookup_pred t = - error ("lookup function is not defined for " ^ Syntax.string_of_term_global thy t) - - (* mapping from term (predicate term, not function term!) to int *) - fun get_nparams (Const (name, _)) = - the_default 0 (try (ind_package_get_nparams thy) name) - | get_nparams (Free (name, _)) = - (if member op = prednames name then - length pnames - else 0) - | get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy t)) - + fun map_Free f = Free o f o dest_Free + val net = fold Item_Net.update + ((funs ~~ preds) @ (ho_argss ~~ params)) + (Fun_Pred.get thy) + fun lookup_pred t = lookup thy net t (* create intro rules *) fun mk_intros ((func, pred), (args, rhs)) = @@ -314,14 +336,15 @@ else let val names = Term.add_free_names rhs [] - in mk_prems thy (lookup_pred, get_nparams) rhs (names, []) + in mk_prems thy lookup_pred rhs (names, []) |> map (fn (resultt, (names', prems)) => Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt])))) end fun mk_rewr_thm (func, pred) = @{thm refl} in - case try (maps mk_intros) ((funs ~~ preds) ~~ (argss' ~~ rhss)) of - NONE => ([], thy) + case (*try *)SOME (maps mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss))) of + NONE => + let val _ = tracing "error occured!" in ([], thy) end | SOME intr_ts => if is_some (try (map (cterm_of thy)) intr_ts) then let @@ -333,53 +356,59 @@ no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds))) - pnames + [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] ||> Sign.restore_naming thy val prednames = map (fst o dest_Const) (#preds ind_result) (* val rewr_thms = map mk_rewr_eq ((distinct (op =) funs) ~~ (#preds ind_result)) *) (* add constants to my table *) + val specs = map (fn predname => (predname, filter (Predicate_Compile_Aux.is_intro predname) (#intrs ind_result))) prednames + (* val thy'' = Pred_Compile_Preproc.map (fold Symtab.update_new (consts ~~ prednames)) thy' + *) + + val thy'' = Fun_Pred.map + (fold Item_Net.update (map (apfst Logic.varify) + (distinct (op =) funs ~~ (#preds ind_result)))) thy' + (*val _ = print_specs thy'' specs*) in (specs, thy'') end else let - val _ = tracing "Introduction rules of function_predicate are not welltyped" + val _ = Output.tracing ( + "Introduction rules of function_predicate are not welltyped: " ^ + commas (map (Syntax.string_of_term_global thy) intr_ts)) in ([], thy) end end fun rewrite_intro thy intro = let - fun lookup_pred (Const (name, T)) = + (*val _ = tracing ("Rewriting intro with registered mapping for: " ^ + commas (Symtab.keys (Pred_Compile_Preproc.get thy)))*) + (*fun lookup_pred (Const (name, T)) = (case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of - SOME c => Const (c, pred_type T) - | NONE => error ("Function " ^ name ^ " is not inductified")) - | lookup_pred (Free (name, T)) = Free (name, T) - | lookup_pred _ = error "lookup function is not defined!" - - fun get_nparams (Const (name, _)) = - the_default 0 (try (ind_package_get_nparams thy) name) - | get_nparams (Free _) = 0 - | get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy t)) - + SOME c => SOME (Const (c, pred_type T)) + | NONE => NONE) + | lookup_pred _ = NONE + *) + fun lookup_pred t = lookup thy (Fun_Pred.get thy) t val intro_t = (Logic.unvarify o prop_of) intro val (prems, concl) = Logic.strip_horn intro_t val frees = map fst (Term.add_frees intro_t []) fun rewrite prem names = let + (*val _ = tracing ("Rewriting premise " ^ Syntax.string_of_term_global thy prem ^ "...")*) val t = (HOLogic.dest_Trueprop prem) val (lit, mk_lit) = case try HOLogic.dest_not t of SOME t => (t, HOLogic.mk_not) | NONE => (t, I) - val (P, args) = (strip_comb lit) + val (P, args) = (strip_comb lit) in - folds_map ( - fn t => if (is_funtype (fastype_of t)) then (fn x => [(t, x)]) - else mk_prems thy (lookup_pred, get_nparams) t) args (names, []) + folds_map (mk_prems thy lookup_pred) args (names, []) |> map (fn (resargs, (names', prems')) => let val prem' = HOLogic.mk_Trueprop (mk_lit (list_comb (P, resargs))) diff -r 997aa3a3e4bb -r c9f428269b38 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Tue Feb 23 10:02:14 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Tue Feb 23 13:36:15 2010 +0100 @@ -7,23 +7,85 @@ signature PREDICATE_COMPILE_PRED = sig (* preprocesses an equation to a set of intro rules; defines new constants *) - (* - val preprocess_pred_equation : thm -> theory -> thm list * theory - *) - val preprocess : string -> theory -> (thm list list * theory) - (* output is the term list of clauses of an unknown predicate *) - val preprocess_term : term -> theory -> (term list * theory) - - (*val rewrite : thm -> thm*) - + val preprocess : Predicate_Compile_Aux.options -> (string * thm list) -> theory + -> ((string * thm list) list * theory) + val flat_higher_order_arguments : ((string * thm list) list * theory) + -> ((string * thm list) list * ((string * thm list) list * theory)) end; -(* : PREDICATE_COMPILE_PREPROC_PRED *) (* FIXME *) -structure Predicate_Compile_Pred = + +structure Predicate_Compile_Pred : PREDICATE_COMPILE_PRED = struct open Predicate_Compile_Aux + +fun datatype_names_of_case_name thy case_name = + map (#1 o #2) (#descr (the (Datatype_Data.info_of_case thy case_name))) + +fun make_case_rewrites new_type_names descr sorts thy = + let + val case_combs = Datatype_Prop.make_case_combs new_type_names descr sorts thy "f"; + fun make comb = + let + val Type ("fun", [T, T']) = fastype_of comb; + val (Const (case_name, _), fs) = strip_comb comb + val used = Term.add_tfree_names comb [] + val U = TFree (Name.variant used "'t", HOLogic.typeS) + val x = Free ("x", T) + val f = Free ("f", T' --> U) + fun apply_f f' = + let + val Ts = binder_types (fastype_of f') + val bs = map Bound ((length Ts - 1) downto 0) + in + fold (curry absdummy) (rev Ts) (f $ (list_comb (f', bs))) + end + val fs' = map apply_f fs + val case_c' = Const (case_name, (map fastype_of fs') @ [T] ---> U) + in + HOLogic.mk_eq (f $ (comb $ x), list_comb (case_c', fs') $ x) + end + in + map make case_combs + end + +fun case_rewrites thy Tcon = + let + val info = Datatype.the_info thy Tcon + val descr = #descr info + val sorts = #sorts info + val typ_names = the_default [Tcon] (#alt_names info) + in + map (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop) + (make_case_rewrites typ_names [descr] sorts thy) + end + +fun instantiated_case_rewrites thy Tcon = + let + val rew_ths = case_rewrites thy Tcon + val ctxt = ProofContext.init thy + fun instantiate th = + let + val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th)))))) + val Type ("fun", [uninst_T, uninst_T']) = fastype_of f + val ([tname, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt + val T = TFree (tname, HOLogic.typeS) + val T' = TFree (tname', HOLogic.typeS) + val U = TFree (uname, HOLogic.typeS) + val y = Free (yname, U) + val f' = absdummy (U --> T', Bound 0 $ y) + val th' = Thm.certify_instantiate + ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')], + [((fst (dest_Var f), (U --> T') --> T'), f')]) th + val [th'] = Variable.export ctxt' ctxt [th'] + in + th' + end + in + map instantiate rew_ths + end + fun is_compound ((Const ("Not", _)) $ t) = error "is_compound: Negation should not occur; preprocessing is defect" | is_compound ((Const ("Ex", _)) $ _) = true @@ -35,6 +97,7 @@ fun flatten constname atom (defs, thy) = if is_compound atom then let + val atom = Envir.beta_norm (Pattern.eta_long [] atom) val constname = Name.variant (map (Long_Name.base_name o fst) defs) ((Long_Name.base_name constname) ^ "_aux") val full_constname = Sign.full_bname thy constname @@ -50,7 +113,82 @@ (lhs, ((full_constname, [definition]) :: defs, thy')) end else - (atom, (defs, thy)) + (case (fst (strip_comb atom)) of + (Const (@{const_name If}, _)) => let + val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp} + val atom' = MetaSimplifier.rewrite_term thy + (map (fn th => th RS @{thm eq_reflection}) [@{thm if_bool_eq_disj}, if_beta]) [] atom + val _ = assert (not (atom = atom')) + in + flatten constname atom' (defs, thy) + end + | _ => + if (has_split_thm thy (fst (strip_comb atom))) then + let + val (f, args) = strip_comb atom + val split_thm = prepare_split_thm (ProofContext.init thy) (the (find_split_thm' thy f)) + (* TODO: contextify things - this line is to unvarify the split_thm *) + (*val ((_, [isplit_thm]), _) = Variable.import true [split_thm] (ProofContext.init thy)*) + val (assms, concl) = Logic.strip_horn (Thm.prop_of split_thm) + val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) + val Tcons = datatype_names_of_case_name thy (fst (dest_Const f)) + val ths = maps (instantiated_case_rewrites thy) Tcons + val atom = MetaSimplifier.rewrite_term thy + (map (fn th => th RS @{thm eq_reflection}) ths) [] atom + val (f, args) = strip_comb atom + val subst = Pattern.match thy (split_t, atom) (Vartab.empty, Vartab.empty) + val (_, split_args) = strip_comb split_t + val match = split_args ~~ args + + (* + fun mk_prems_of_assm assm = + let + val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm)) + val names = [] (* TODO *) + val var_names = Name.variant_list names (map fst vTs) + val vars = map Free (var_names ~~ (map snd vTs)) + val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm')) + val (HOLogic.dest_eq (HOLogic.dest_Trueprop prem)) + val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res) + in + (*mk_prems' inner_t (var_names @ names, prems' @ prems)*) error "asda" + end + *) + val names = Term.add_free_names atom [] + val frees = map Free (Term.add_frees atom []) + val constname = Name.variant (map (Long_Name.base_name o fst) defs) + ((Long_Name.base_name constname) ^ "_aux") + val full_constname = Sign.full_bname thy constname + val constT = map fastype_of frees ---> HOLogic.boolT + val lhs = list_comb (Const (full_constname, constT), frees) + fun new_def assm = + let + val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm)) + val var_names = Name.variant_list names (map fst vTs) + val vars = map Free (var_names ~~ (map snd vTs)) + val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm')) + fun mk_subst prem = + let + val (Free (x, T), r) = HOLogic.dest_eq (HOLogic.dest_Trueprop prem) + in + ((x, T), r) + end + val subst = map mk_subst prems' + val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res) + val def = Logic.mk_equals (lhs, inner_t) + in + Envir.expand_term_frees subst def + end + val new_defs = map new_def assms + val (definition, thy') = thy + |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] + |> PureThy.add_axioms (map_index + (fn (i, t) => ((Binding.name (constname ^ "_def" ^ string_of_int i), t), [])) new_defs) + in + (lhs, ((full_constname, definition) :: defs, thy')) + end + else + (atom, (defs, thy))) fun flatten_intros constname intros thy = let @@ -107,30 +245,60 @@ val rewrite = Simplifier.simplify (HOL_basic_ss addsimps [@{thm Ball_def}, @{thm Bex_def}]) - #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm all_not_ex}]) + #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm all_not_ex}]) #> Conv.fconv_rule nnf_conv #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm ex_disj_distrib}]) -val rewrite_intros = -(* Simplifier.simplify (HOL_basic_ss addsimps @{thms HOL.simp_thms(9)}) *) - Simplifier.full_simplify (HOL_basic_ss addsimps [@{thm not_not}]) - -fun preprocess (constname, specs) thy = +fun split_conjs thy t = + let + fun split_conjunctions (Const (@{const_name "op &"}, _) $ t1 $ t2) = + (split_conjunctions t1) @ (split_conjunctions t2) + | split_conjunctions t = [t] + in + map HOLogic.mk_Trueprop (split_conjunctions (HOLogic.dest_Trueprop t)) + end + +fun rewrite_intros thy = + Simplifier.full_simplify (HOL_basic_ss addsimps [@{thm all_not_ex}]) + #> Simplifier.full_simplify (HOL_basic_ss addsimps @{thms bool_simps} addsimps @{thms nnf_simps}) + #> map_term thy (maps_premises (split_conjs thy)) + +fun print_specs options thy msg ths = + if show_intermediate_results options then + (tracing (msg); tracing (commas (map (Display.string_of_thm_global thy) ths))) + else + () +(* +fun split_cases thy th = let - val ctxt = ProofContext.init thy + + in + map_term thy th + end +*) +fun preprocess options (constname, specs) thy = +(* case Predicate_Compile_Data.processed_specs thy constname of + SOME specss => (specss, thy) + | NONE =>*) + let + val ctxt = ProofContext.init thy val intros = - if forall is_pred_equation specs then - introrulify thy (map rewrite specs) - else if forall (is_intro constname) specs then - map rewrite_intros specs - else - error ("unexpected specification for constant " ^ quote constname ^ ":\n" - ^ commas (map (quote o Display.string_of_thm_global thy) specs)) - val (intros', (local_defs, thy')) = flatten_intros constname intros thy - val (intross, thy'') = fold_map preprocess local_defs thy' - in - ((constname, intros') :: flat intross,thy'') - end; + if forall is_pred_equation specs then + map (map_term thy (maps_premises (split_conjs thy))) (introrulify thy (map rewrite specs)) + else if forall (is_intro constname) specs then + map (rewrite_intros thy) specs + else + error ("unexpected specification for constant " ^ quote constname ^ ":\n" + ^ commas (map (quote o Display.string_of_thm_global thy) specs)) + val _ = print_specs options thy "normalized intros" intros + (*val intros = maps (split_cases thy) intros*) + val (intros', (local_defs, thy')) = flatten_intros constname intros thy + val (intross, thy'') = fold_map (preprocess options) local_defs thy' + val full_spec = (constname, intros') :: flat intross + (*val thy''' = Predicate_Compile_Data.store_processed_specs (constname, full_spec) thy''*) + in + (full_spec, thy'') + end; fun preprocess_term t thy = error "preprocess_pred_term: to implement" @@ -166,7 +334,8 @@ else (arg, (new_defs, thy)) - val (args', (new_defs', thy')) = fold_map replace_abs_arg args (new_defs, thy) + val (args', (new_defs', thy')) = fold_map replace_abs_arg + (map Envir.beta_eta_contract args) (new_defs, thy) in (list_comb (pred, args'), (new_defs', thy')) end diff -r 997aa3a3e4bb -r c9f428269b38 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Tue Feb 23 10:02:14 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Tue Feb 23 13:36:15 2010 +0100 @@ -6,10 +6,18 @@ signature PREDICATE_COMPILE_QUICKCHECK = sig - val quickcheck : Proof.context -> term -> int -> term list option + (*val quickcheck : Proof.context -> term -> int -> term list option*) val test_ref : ((unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option) Unsynchronized.ref val tracing : bool Unsynchronized.ref; + val quickcheck_compile_term : bool -> bool -> Proof.context -> term -> int -> term list option +(* val test_term : Proof.context -> bool -> int -> int -> int -> int -> term -> *) + val quiet : bool Unsynchronized.ref; + val nrandom : int Unsynchronized.ref; + val depth : int Unsynchronized.ref; + val debug : bool Unsynchronized.ref; + val function_flattening : bool Unsynchronized.ref; + val no_higher_order_predicate : string list Unsynchronized.ref; end; structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK = @@ -24,21 +32,106 @@ val target = "Quickcheck" +val quiet = Unsynchronized.ref false; + +val nrandom = Unsynchronized.ref 2; + +val depth = Unsynchronized.ref 8; + +val debug = Unsynchronized.ref false; +val function_flattening = Unsynchronized.ref true; + + +val no_higher_order_predicate = Unsynchronized.ref []; + val options = Options { expected_modes = NONE, proposed_modes = NONE, proposed_names = [], + show_steps = false, + show_intermediate_results = false, + show_proof_trace = false, + show_modes = false, + show_mode_inference = false, + show_compilation = false, + show_caught_failures = false, + skip_proof = false, + compilation = Random, + inductify = true, + function_flattening = true, + fail_safe_function_flattening = false, + no_higher_order_predicate = [], + no_topmost_reordering = true +} + +val debug_options = Options { + expected_modes = NONE, + proposed_modes = NONE, + proposed_names = [], show_steps = true, show_intermediate_results = true, show_proof_trace = false, - show_modes = false, - show_mode_inference = false, + show_modes = true, + show_mode_inference = true, show_compilation = false, + show_caught_failures = true, skip_proof = false, compilation = Random, - inductify = false + inductify = true, + function_flattening = true, + fail_safe_function_flattening = false, + no_higher_order_predicate = [], + no_topmost_reordering = true } + +fun set_function_flattening b + (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s, + show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m, + show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p, + compilation = c, inductify = i, function_flattening = f_f, + fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho, + no_topmost_reordering = re}) = + (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s, + show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m, + show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p, + compilation = c, inductify = i, function_flattening = b, + fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho, + no_topmost_reordering = re}) + +fun set_fail_safe_function_flattening b + (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s, + show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m, + show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p, + compilation = c, inductify = i, function_flattening = f_f, + fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho, + no_topmost_reordering = re}) = + (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s, + show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m, + show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p, + compilation = c, inductify = i, function_flattening = f_f, + fail_safe_function_flattening = b, no_higher_order_predicate = no_ho, + no_topmost_reordering = re}) + +fun set_no_higher_order_predicate ss + (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s, + show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m, + show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p, + compilation = c, inductify = i, function_flattening = f_f, + fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho, + no_topmost_reordering = re}) = + (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s, + show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m, + show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p, + compilation = c, inductify = i, function_flattening = f_f, + fail_safe_function_flattening = fs_ff, no_higher_order_predicate = ss, no_topmost_reordering = re}) + + +fun get_options () = + set_no_higher_order_predicate (!no_higher_order_predicate) + (set_function_flattening (!function_flattening) + (if !debug then debug_options else options)) + fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs val mk_predT = #mk_predT (dest_compfuns Predicate_Compile_Core.pred_compfuns) val mk_randompredT = #mk_predT (dest_compfuns Predicate_Compile_Core.randompred_compfuns) @@ -63,13 +156,15 @@ fun strip_horn A = (strip_imp_prems A, strip_imp_concl A); -fun quickcheck ctxt t = +fun cpu_time description f = let - (*val () = - if !tracing then - tracing ("Starting quickcheck with " ^ (Syntax.string_of_term ctxt t)) - else - ()*) + val start = start_timing () + val result = Exn.capture f () + val time = Time.toMilliseconds (#cpu (end_timing start)) + in (Exn.release result, (description, time)) end + +fun compile_term options ctxt t = + let val ctxt' = ProofContext.theory (Context.copy_thy) ctxt val thy = (ProofContext.theory_of ctxt') val (vs, t') = strip_abs t @@ -82,44 +177,73 @@ val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy val const = Const (full_constname, constT) val t = Logic.list_implies - (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]), + (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]), HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs'))) val tac = fn _ => Skip_Proof.cheat_tac thy1 val intro = Goal.prove (ProofContext.init thy1) (map fst vs') [] t tac - (*val _ = tracing (Display.string_of_thm ctxt' intro)*) - val thy2 = (*Output.cond_timeit (!Quickcheck.timing) "predicate intros" - (fn () => *)(Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1) - val thy3 = (*Output.cond_timeit (!Quickcheck.timing) "predicate preprocessing" - (fn () =>*) (Predicate_Compile.preprocess options const thy2) - val thy4 = Output.cond_timeit (!Quickcheck.timing) "random_dseq compilation" + val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1 + val (thy3, preproc_time) = cpu_time "predicate preprocessing" + (fn () => Predicate_Compile.preprocess options const thy2) + val (thy4, core_comp_time) = cpu_time "random_dseq core compilation" (fn () => Predicate_Compile_Core.add_random_dseq_equations options [full_constname] thy3) - (*val depth_limited_modes = Predicate_Compile_Core.modes_of Depth_Limited thy'' full_constname*) - val modes = Predicate_Compile_Core.modes_of Random_DSeq thy4 full_constname + val _ = Predicate_Compile_Core.print_all_modes Pos_Random_DSeq thy4 + val modes = Predicate_Compile_Core.modes_of Pos_Random_DSeq thy4 full_constname val output_mode = fold_rev (curry Fun) (map (K Output) (binder_types constT)) Bool val prog = if member eq_mode modes output_mode then let - val name = Predicate_Compile_Core.function_name_of Random_DSeq thy4 full_constname output_mode + val name = Predicate_Compile_Core.function_name_of Pos_Random_DSeq thy4 + full_constname (true, output_mode) val T = (mk_randompredT (HOLogic.mk_tupleT (map snd vs'))) in Const (name, T) end - (*else if member (op =) depth_limited_modes ([], []) then - let - val name = Predicate_Compile_Core.depth_limited_function_name_of thy'' full_constname ([], []) - val T = @{typ code_numeral} --> (mk_predT (HOLogic.mk_tupleT (map snd vs'))) - in lift_pred (Const (name, T) $ Bound 0) end*) - else error "Predicate Compile Quickcheck failed" + else error ("Predicate Compile Quickcheck failed: " ^ commas (map string_of_mode modes)) val qc_term = mk_bind (prog, mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term} (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))) val compilation = - Code_Eval.eval NONE ("Predicate_Compile_Quickcheck.test_ref", test_ref) + Code_Eval.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref) (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (DSequence.map o map) proc) thy4 qc_term [] in - (fn size => - Option.map fst (DSequence.yield (compilation size size |> Random_Engine.run) size true)) + (fn size => fn nrandom => fn depth => + Option.map fst (DSequence.yield (compilation nrandom size |> Random_Engine.run) depth true)) + end + +fun try_upto quiet f i = + let + fun try' j = + if j <= i then + let + val _ = priority ("Executing depth " ^ string_of_int j) + in + case f j handle Match => (if quiet then () + else warning "Exception Match raised during quickcheck"; NONE) + of NONE => try' (j + 1) | SOME q => SOME q + end + else + NONE + in + try' 0 + end + +(* quickcheck interface functions *) + +fun compile_term' options ctxt t = + let + val c = compile_term options ctxt t + in + (fn size => try_upto (!quiet) (c size (!nrandom)) (!depth)) + end + +fun quickcheck_compile_term function_flattening fail_safe_function_flattening ctxt t = + let + val options = + set_fail_safe_function_flattening fail_safe_function_flattening + (set_function_flattening function_flattening (get_options ())) + in + compile_term' options ctxt t end end; diff -r 997aa3a3e4bb -r c9f428269b38 src/HOL/ex/Predicate_Compile_Alternative_Defs.thy --- a/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Tue Feb 23 10:02:14 2010 +0100 +++ b/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Tue Feb 23 13:36:15 2010 +0100 @@ -2,6 +2,21 @@ imports "../Predicate_Compile" begin +section {* Common constants *} + +declare HOL.if_bool_eq_disj[code_pred_inline] + +setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *} + +section {* Pairs *} + +setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name split}] *} + +section {* Bounded quantifiers *} + +declare Ball_def[code_pred_inline] +declare Bex_def[code_pred_inline] + section {* Set operations *} declare Collect_def[code_pred_inline] @@ -9,13 +24,37 @@ declare eq_reflection[OF empty_def, code_pred_inline] declare insert_code[code_pred_def] + +declare subset_iff[code_pred_inline] + +declare Int_def[code_pred_inline] declare eq_reflection[OF Un_def, code_pred_inline] declare eq_reflection[OF UNION_def, code_pred_inline] +lemma Diff[code_pred_inline]: + "(A - B) = (%x. A x \ \ B x)" +by (auto simp add: mem_def) +lemma set_equality[code_pred_inline]: + "(A = B) = ((\x. A x \ B x) \ (\x. B x \ A x))" +by (fastsimp simp add: mem_def) + +section {* Setup for Numerals *} + +setup {* Predicate_Compile_Data.ignore_consts [@{const_name number_of}] *} +setup {* Predicate_Compile_Data.keep_functions [@{const_name number_of}] *} + +setup {* Predicate_Compile_Data.ignore_consts [@{const_name div}, @{const_name mod}, @{const_name times}] *} section {* Alternative list definitions *} + +text {* size simps are not yet added to the Spec_Rules interface. So they are just added manually here! *} +lemma [code_pred_def]: + "length [] = 0" + "length (x # xs) = Suc (length xs)" +by auto + subsection {* Alternative rules for set *} lemma set_ConsI1 [code_pred_intro]: diff -r 997aa3a3e4bb -r c9f428269b38 src/HOL/ex/Predicate_Compile_Quickcheck.thy --- a/src/HOL/ex/Predicate_Compile_Quickcheck.thy Tue Feb 23 10:02:14 2010 +0100 +++ b/src/HOL/ex/Predicate_Compile_Quickcheck.thy Tue Feb 23 13:36:15 2010 +0100 @@ -3,11 +3,14 @@ header {* A Prototype of Quickcheck based on the Predicate Compiler *} theory Predicate_Compile_Quickcheck -imports "../Predicate_Compile" +imports "../Predicate_Compile" Quickcheck Predicate_Compile_Alternative_Defs uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML" begin -setup {* Quickcheck.add_generator ("predicate_compile", Predicate_Compile_Quickcheck.quickcheck) *} +setup {* Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term false true) *} +setup {* Quickcheck.add_generator ("predicate_compile_ff_fs", Predicate_Compile_Quickcheck.quickcheck_compile_term true true) *} +setup {* Quickcheck.add_generator ("predicate_compile_ff_nofs", Predicate_Compile_Quickcheck.quickcheck_compile_term true false) *} + (* datatype alphabet = a | b diff -r 997aa3a3e4bb -r c9f428269b38 src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy --- a/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy Tue Feb 23 10:02:14 2010 +0100 +++ b/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy Tue Feb 23 13:36:15 2010 +0100 @@ -1,45 +1,39 @@ theory Predicate_Compile_Quickcheck_ex imports Predicate_Compile_Quickcheck - Predicate_Compile_Alternative_Defs begin -ML {* Predicate_Compile_Alternative_Defs.get *} - section {* Sets *} -(* + lemma "x \ {(1::nat)} ==> False" -quickcheck[generator=predicate_compile, iterations=10] +quickcheck[generator=predicate_compile_wo_ff, iterations=10] oops -*) -(* TODO: some error with doubled negation *) -(* + lemma "x \ {Suc 0, Suc (Suc 0)} ==> x \ Suc 0" -quickcheck[generator=predicate_compile] +quickcheck[generator=predicate_compile_wo_ff] oops -*) -(* + lemma "x \ {Suc 0, Suc (Suc 0)} ==> x = Suc 0" -quickcheck[generator=predicate_compile] +quickcheck[generator=predicate_compile_wo_ff] oops -*) + lemma "x \ {Suc 0, Suc (Suc 0)} ==> x <= Suc 0" -(*quickcheck[generator=predicate_compile]*) +quickcheck[generator=predicate_compile_wo_ff] oops section {* Numerals *} -(* + lemma "x \ {1, 2, (3::nat)} ==> x = 1 \ x = 2" -quickcheck[generator=predicate_compile] +quickcheck[generator=predicate_compile_wo_ff] oops -*) + lemma "x \ {1, 2, (3::nat)} ==> x < 3" -(*quickcheck[generator=predicate_compile]*) +quickcheck[generator=predicate_compile_wo_ff] oops lemma "x \ {1, 2} \ {3, 4} ==> x = (1::nat) \ x = (2::nat)" -(*quickcheck[generator=predicate_compile]*) +quickcheck[generator=predicate_compile_wo_ff] oops section {* Context Free Grammar *} @@ -53,33 +47,15 @@ | "w \ S\<^isub>1 \ a # w \ A\<^isub>1" | "w \ S\<^isub>1 \ b # w \ S\<^isub>1" | "\v \ B\<^isub>1; v \ B\<^isub>1\ \ a # v @ w \ B\<^isub>1" -(* -code_pred [random_dseq inductify] "S\<^isub>1p" . -*) -(*thm B\<^isub>1p.random_dseq_equation*) -(* -values [random_dseq 2, 2, 4] 10 "{x. S\<^isub>1p x}" -values [random_dseq 1, 1, 5] 20 "{x. S\<^isub>1p x}" -ML {* set ML_Context.trace *} -*) -ML {* set Toplevel.debug *} -(* -quickcheck[generator = predicate_compile, size = 10, iterations = 1] -oops -*) -ML {* Spec_Rules.get *} -ML {* Item_Net.retrieve *} -local_setup {* Local_Theory.checkpoint *} -ML {* Predicate_Compile_Data.get_specification @{theory} @{term "append"} *} lemma - "w \ S\<^isub>1p \ w = []" -quickcheck[generator = predicate_compile, iterations=1] + "w \ S\<^isub>1 \ w = []" +quickcheck[generator = predicate_compile_ff_nofs, iterations=1] oops theorem S\<^isub>1_sound: -"w \ S\<^isub>1p \ length [x \ w. x = a] = length [x \ w. x = b]" -quickcheck[generator=predicate_compile, size=15] +"w \ S\<^isub>1 \ length [x \ w. x = a] = length [x \ w. x = b]" +quickcheck[generator=predicate_compile_ff_nofs, size=15] oops @@ -90,7 +66,7 @@ | "w \ S\<^isub>2 \ a # w \ A\<^isub>2" | "w \ S\<^isub>2 \ b # w \ B\<^isub>2" | "\v \ B\<^isub>2; v \ B\<^isub>2\ \ a # v @ w \ B\<^isub>2" - +(* code_pred [random_dseq inductify] S\<^isub>2 . thm S\<^isub>2.random_dseq_equation thm A\<^isub>2.random_dseq_equation @@ -118,10 +94,10 @@ "w \ S\<^isub>2 ==> length [x \ w. x = a] <= Suc (Suc 0)" quickcheck[generator=predicate_compile, size = 10, iterations = 1] oops - +*) theorem S\<^isub>2_sound: "w \ S\<^isub>2 \ length [x \ w. x = a] = length [x \ w. x = b]" -quickcheck[generator=predicate_compile, size=15, iterations=1] +quickcheck[generator=predicate_compile_ff_nofs, size=5, iterations=10] oops inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where @@ -141,17 +117,17 @@ lemma S\<^isub>3_sound: "w \ S\<^isub>3 \ length [x \ w. x = a] = length [x \ w. x = b]" -quickcheck[generator=predicate_compile, size=10, iterations=10] +quickcheck[generator=predicate_compile_ff_fs, size=10, iterations=10] oops lemma "\ (length w > 2) \ \ (length [x \ w. x = a] = length [x \ w. x = b])" -quickcheck[size=10, generator = predicate_compile] +quickcheck[size=10, generator = predicate_compile_ff_fs] oops theorem S\<^isub>3_complete: "length [x \ w. x = a] = length [x \ w. b = x] \ w \ S\<^isub>3" (*quickcheck[generator=SML]*) -quickcheck[generator=predicate_compile, size=10, iterations=100] +quickcheck[generator=predicate_compile_ff_fs, size=10, iterations=100] oops @@ -166,20 +142,23 @@ theorem S\<^isub>4_sound: "w \ S\<^isub>4 \ length [x \ w. x = a] = length [x \ w. x = b]" -quickcheck[generator = predicate_compile, size=5, iterations=1] +quickcheck[generator = predicate_compile_ff_nofs, size=5, iterations=1] oops theorem S\<^isub>4_complete: "length [x \ w. x = a] = length [x \ w. x = b] \ w \ S\<^isub>4" -quickcheck[generator = predicate_compile, size=5, iterations=1] +quickcheck[generator = predicate_compile_ff_nofs, size=5, iterations=1] oops -hide const b +hide const a b subsection {* Lexicographic order *} +(* TODO *) +(* lemma "(u, v) : lexord r ==> (x @ u, y @ v) : lexord r" - +oops +*) subsection {* IMP *} types @@ -208,7 +187,7 @@ lemma "exec c s s' ==> exec (Seq c c) s s'" -quickcheck[generator = predicate_compile, size=3, iterations=1] +(*quickcheck[generator = predicate_compile_wo_ff, size=2, iterations=10]*) oops subsection {* Lambda *} @@ -263,28 +242,9 @@ lemma "\ \ t : U \ t \\<^sub>\ t' \ \ \ t' : U" -quickcheck[generator = predicate_compile, size = 7, iterations = 10] +quickcheck[generator = predicate_compile_ff_fs, size = 7, iterations = 10] oops -(* -code_pred (expected_modes: i => i => o => bool, i => i => i => bool) typing . -thm typing.equation - -code_pred (modes: i => i => bool, i => o => bool as reduce') beta . -thm beta.equation - -values "{x. App (Abs (Atom 0) (Var 0)) (Var 1) \\<^sub>\ x}" - -definition "reduce t = Predicate.the (reduce' t)" - -value "reduce (App (Abs (Atom 0) (Var 0)) (Var 1))" - -code_pred [random] typing . -code_pred [random_dseq] typing . - -(*values [random] 1 "{(\, t, T). \ \ t : T}" -*)*) - subsection {* JAD *} definition matrix :: "('a :: semiring_0) list list \ nat \ nat \ bool" where @@ -300,9 +260,17 @@ lemma [code_pred_intro]: "matrix [] 0 m" "matrix xss n m ==> length xs = m ==> matrix (xs # xss) (Suc n) m" -sorry +proof - + show "matrix [] 0 m" unfolding matrix_def by auto +next + show "matrix xss n m ==> length xs = m ==> matrix (xs # xss) (Suc n) m" + unfolding matrix_def by auto +qed -code_pred [random_dseq inductify] matrix sorry +code_pred [random_dseq inductify] matrix + apply (cases x) + unfolding matrix_def apply fastsimp + apply fastsimp done values [random_dseq 2, 2, 15] 6 "{(M::int list list, n, m). matrix M n m}" @@ -344,10 +312,10 @@ definition "length_permutate M = (unzip o sort (length o snd)) (zip [0 ..< length M] M)" - +(* definition "transpose M = [map (\ xs. xs ! i) (takeWhile (\ xs. i < length xs) M). i \ [0 ..< length (M ! 0)]]" - +*) definition "inflate upds = foldr (\ (i, x) upds. upds[i := x]) upds (replicate (length upds) 0)" @@ -356,15 +324,14 @@ definition "jad_mv v = inflate o split zip o apsnd (map listsum o transpose o map (map (\ (i, x). v ! i * x)))" -ML {* ML_Context.trace := false *} lemma "matrix (M::int list list) rs cs \ False" -quickcheck[generator = predicate_compile, size = 6] +quickcheck[generator = predicate_compile_ff_nofs, size = 6] oops lemma "\ matrix M rs cs ; length v = cs \ \ jad_mv v (jad M) = mv M v" -(*quickcheck[generator = predicate_compile]*) +quickcheck[generator = predicate_compile_wo_ff] oops end \ No newline at end of file diff -r 997aa3a3e4bb -r c9f428269b38 src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Tue Feb 23 10:02:14 2010 +0100 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Tue Feb 23 13:36:15 2010 +0100 @@ -252,10 +252,12 @@ "one_or_two = {Suc 0, (Suc (Suc 0))}" code_pred [inductify] one_or_two . + code_pred [dseq] one_or_two . -(*code_pred [random_dseq] one_or_two .*) +code_pred [random_dseq] one_or_two . +thm one_or_two.dseq_equation values [expected "{Suc 0::nat, 2::nat}"] "{x. one_or_two x}" -(*values [random_dseq 1,1,2] "{x. one_or_two x}"*) +values [random_dseq 0,0,10] 3 "{x. one_or_two x}" inductive one_or_two' :: "nat => bool" where @@ -269,12 +271,12 @@ definition one_or_two'': "one_or_two'' == {1, (2::nat)}" -ML {* prop_of @{thm one_or_two''} *} -(*code_pred [inductify] one_or_two'' . + +code_pred [inductify] one_or_two'' . thm one_or_two''.equation values "{x. one_or_two'' x}" -*) + subsection {* even predicate *} inductive even :: "nat \ bool" and odd :: "nat \ bool" where @@ -779,6 +781,25 @@ thm divmod_rel.equation value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)" +subsection {* Transforming predicate logic into logic programs *} + +subsection {* Transforming functions into logic programs *} +definition + "case_f xs ys = (case (xs @ ys) of [] => [] | (x # xs) => xs)" + +code_pred [inductify] case_f . +thm case_fP.equation +thm case_fP.intros + +fun fold_map_idx where + "fold_map_idx f i y [] = (y, [])" +| "fold_map_idx f i y (x # xs) = + (let (y', x') = f i y x; (y'', xs') = fold_map_idx f (Suc i) y' xs + in (y'', x' # xs'))" + +text {* mode analysis explores thousand modes - this is infeasible at the moment... *} +(*code_pred [inductify, show_steps] fold_map_idx .*) + subsection {* Minimum *} definition Min @@ -883,9 +904,16 @@ values [random_dseq 1, 2, 5] 10 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}" - - -code_pred [inductify] lenlex . +thm lenlex_conv +thm lex_conv +declare list.size(3,4)[code_pred_def] +(*code_pred [inductify, show_steps, show_intermediate_results] length .*) +setup {* Predicate_Compile_Data.ignore_consts [@{const_name Orderings.top_class.top}] *} +code_pred [inductify] lex . +thm lex.equation +thm lex_def +declare lenlex_conv[code_pred_def] +code_pred [inductify, show_steps, show_intermediate_results] lenlex . thm lenlex.equation code_pred [random_dseq inductify] lenlex . @@ -893,10 +921,10 @@ values [random_dseq 4, 2, 4] 100 "{(xs, ys::int list). lenlex (%(x, y). x <= y) (xs, ys)}" thm lists.intros -(* + code_pred [inductify] lists . -*) -(*thm lists.equation*) + +thm lists.equation subsection {* AVL Tree *} @@ -974,13 +1002,17 @@ (o * o => bool) => i => bool, (i * o => bool) => i => bool) [inductify] Domain . thm Domain.equation +thm Range_def + code_pred (modes: (o * o => bool) => o => bool, (o * o => bool) => i => bool, (o * i => bool) => i => bool) [inductify] Range . thm Range.equation + code_pred [inductify] Field . thm Field.equation + (*thm refl_on_def code_pred [inductify] refl_on . thm refl_on.equation*) @@ -992,9 +1024,10 @@ thm trans.equation code_pred [inductify] single_valued . thm single_valued.equation -code_pred [inductify] inv_image . +thm inv_image_def +(*code_pred [inductify] inv_image . thm inv_image.equation - +*) subsection {* Inverting list functions *} (*code_pred [inductify] length . diff -r 997aa3a3e4bb -r c9f428269b38 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Tue Feb 23 10:02:14 2010 +0100 +++ b/src/Tools/quickcheck.ML Tue Feb 23 13:36:15 2010 +0100 @@ -10,6 +10,8 @@ val timing : bool Unsynchronized.ref val test_term: Proof.context -> bool -> string option -> int -> int -> term -> (string * term) list option + val timed_test_term: Proof.context -> bool -> string option -> int -> int -> term -> + ((string * term) list option * (string * int) list) val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory val setup: theory -> theory val quickcheck: (string * string) list -> int -> Proof.state -> (string * term) list option @@ -97,13 +99,20 @@ val frees = Term.add_frees t []; in (map fst frees, list_abs_free (frees, t)) end -fun test_term ctxt quiet generator_name size i t = +fun cpu_time description f = + let + val start = start_timing () + val result = Exn.capture f () + val time = Time.toMilliseconds (#cpu (end_timing start)) + in (Exn.release result, (description, time)) end + +fun timed_test_term ctxt quiet generator_name size i t = let val (names, t') = prep_test_term t; - val testers = (*cond_timeit (!timing) "quickcheck compilation" - (fn () => *)(case generator_name + val (testers, comp_time) = cpu_time "quickcheck compilation" + (fn () => (case generator_name of NONE => if quiet then mk_testers ctxt t' else mk_testers_strict ctxt t' - | SOME name => [mk_tester_select name ctxt t']); + | SOME name => [mk_tester_select name ctxt t'])); fun iterate f 0 = NONE | iterate f j = case f () handle Match => (if quiet then () else warning "Exception Match raised during quickcheck"; NONE) @@ -117,13 +126,17 @@ else (if quiet then () else priority ("Test data size: " ^ string_of_int k); case with_testers k testers of NONE => with_size (k + 1) | SOME q => SOME q); + val (result, exec_time) = cpu_time "quickcheck execution" + (fn () => case with_size 1 + of NONE => NONE + | SOME ts => SOME (names ~~ ts)) in - cond_timeit (!timing) "quickcheck execution" - (fn () => case with_size 1 - of NONE => NONE - | SOME ts => SOME (names ~~ ts)) + (result, [exec_time, comp_time]) end; +fun test_term ctxt quiet generator_name size i t = + fst (timed_test_term ctxt quiet generator_name size i t) + fun monomorphic_term thy insts default_T = let fun subst (T as TFree (v, S)) =