# HG changeset patch # User bulwahn # Date 1282748390 -7200 # Node ID 2c8a595af43e7c1ca21167ba4ca20e403a294cc8 # Parent 5bbdd9a9df6252663bfe4992d836b14241640de3 invocation of values for prolog execution does not require invocation of code_pred anymore diff -r 5bbdd9a9df62 -r 2c8a595af43e src/HOL/Library/Code_Prolog.thy --- a/src/HOL/Library/Code_Prolog.thy Wed Aug 25 16:59:49 2010 +0200 +++ b/src/HOL/Library/Code_Prolog.thy Wed Aug 25 16:59:50 2010 +0200 @@ -9,5 +9,10 @@ uses "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML" begin +section {* Setup for Numerals *} + +setup {* Predicate_Compile_Data.ignore_consts [@{const_name number_of}] *} +setup {* Predicate_Compile_Data.keep_functions [@{const_name number_of}] *} + end diff -r 5bbdd9a9df62 -r 2c8a595af43e src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Wed Aug 25 16:59:49 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Wed Aug 25 16:59:50 2010 +0200 @@ -9,8 +9,6 @@ "append [] ys ys" | "append xs ys zs ==> append (x # xs) ys (x # zs)" -code_pred append . - values 3 "{(x, y, z). append x y z}" @@ -71,9 +69,7 @@ where "queen [1,2,3,4,5,6,7,8,9] ys ==> queen_9 ys" -code_pred queen_9 . - -values 150 "{ys. queen_9 ys}" +values 10 "{ys. queen_9 ys}" section {* Example symbolic derivation *} @@ -163,11 +159,6 @@ where "d (Mult (Mult (Mult (Mult (Mult (Mult (Mult (Mult (Mult x x) x) x) x) x) x) x) x) x) x e ==> times10 e" -code_pred ops8 . -code_pred divide10 . -code_pred log10 . -code_pred times10 . - values "{e. ops8 e}" values "{e. divide10 e}" values "{e. log10 e}" @@ -181,8 +172,6 @@ where "y \ B \ notB y" -code_pred notB . - ML {* Code_Prolog.options := {ensure_groundness = true} *} values 2 "{y. notB y}" @@ -191,8 +180,6 @@ where "y \ A \ z \ B \ notAB (y, z)" -code_pred notAB . - values 5 "{y. notAB y}" end diff -r 5bbdd9a9df62 -r 2c8a595af43e src/HOL/Predicate_Compile_Examples/Hotel_Example.thy --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Wed Aug 25 16:59:49 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Wed Aug 25 16:59:50 2010 +0200 @@ -84,10 +84,10 @@ lemma [code_pred_inline]: "(op -) == (%A B x. A x \ \ B x)" by (auto simp add: Diff_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection) -code_pred [new_random_dseq inductify, skip_proof] hotel . - ML {* Code_Prolog.options := {ensure_groundness = true} *} values 10 "{s. hotel s}" + + end \ No newline at end of file diff -r 5bbdd9a9df62 -r 2c8a595af43e src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Aug 25 16:59:49 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Aug 25 16:59:50 2010 +0200 @@ -22,7 +22,7 @@ type logic_program = clause list; type constant_table = (string * string) list - val generate : code_options -> Proof.context -> string list -> (logic_program * constant_table) + val generate : code_options -> Proof.context -> string -> (logic_program * constant_table) val write_program : logic_program -> string val run : logic_program -> string -> string list -> int option -> prol_term list list @@ -190,15 +190,63 @@ in clause end in (map translate_intro intros', constant_table') end +val preprocess_options = Predicate_Compile_Aux.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 = true, + no_topmost_reordering = false, + function_flattening = true, + specialise = false, + fail_safe_function_flattening = false, + no_higher_order_predicate = [], + inductify = false, + detect_switches = true, + compilation = Predicate_Compile_Aux.Pred +} + +fun depending_preds_of (key, intros) = + fold Term.add_const_names (map Thm.prop_of intros) [] + +fun add_edges edges_of key G = + let + fun extend' key (G, visited) = + case try (Graph.get_node G) key of + SOME v => + let + val new_edges = filter (fn k => is_some (try (Graph.get_node G) k)) (edges_of (key, v)) + val (G', visited') = fold extend' + (subtract (op =) (key :: visited) new_edges) (G, key :: visited) + in + (fold (Graph.add_edge o (pair key)) new_edges G', visited') + end + | NONE => (G, visited) + in + fst (extend' key (G, [])) + end + fun generate options ctxt const = let - fun strong_conn_of gr keys = + val T = Sign.the_const_type (ProofContext.theory_of ctxt) const + val t = Const (const, T) + val ctxt' = ProofContext.theory (Context.copy_thy) ctxt + val thy' = Predicate_Compile.preprocess preprocess_options t (ProofContext.theory_of ctxt') + val ctxt'' = ProofContext.init_global thy' + fun strong_conn_of gr keys = Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr) - val gr = Predicate_Compile_Core.intros_graph_of ctxt - val scc = strong_conn_of gr const + val gr = Predicate_Compile_Core.intros_graph_of ctxt'' + val gr' = add_edges depending_preds_of const gr + val scc = strong_conn_of gr' [const] val constant_table = mk_constant_table (flat scc) in - apfst flat (fold_map (translate_intros options ctxt gr) (flat scc) constant_table) + apfst flat (fold_map (translate_intros options ctxt'' gr) (flat scc) constant_table) end (* add implementation for ground predicates *) @@ -411,7 +459,7 @@ SOME vs => vs | NONE => error ("Not only free variables in " ^ commas (map (Syntax.string_of_term ctxt) all_args)) val _ = tracing "Generating prolog program..." - val (p, constant_table) = generate options ctxt [name] + val (p, constant_table) = generate options ctxt name |> (if #ensure_groundness options then add_ground_predicates ctxt else I) val _ = tracing "Running prolog program..." val tss = run p (translate_const constant_table name) (map first_upper vnames) soln diff -r 5bbdd9a9df62 -r 2c8a595af43e src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Aug 25 16:59:49 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Aug 25 16:59:50 2010 +0200 @@ -275,7 +275,6 @@ else let val specs = get_specification options thy t - (*|> Predicate_Compile_Set.unfold_set_notation*) (*val _ = print_specification options thy constname specs*) val us = defiants_of specs in