invocation of values for prolog execution does not require invocation of code_pred anymore
--- 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
--- 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 \<noteq> B \<Longrightarrow> notB y"
-code_pred notB .
-
ML {* Code_Prolog.options := {ensure_groundness = true} *}
values 2 "{y. notB y}"
@@ -191,8 +180,6 @@
where
"y \<noteq> A \<Longrightarrow> z \<noteq> B \<Longrightarrow> notAB (y, z)"
-code_pred notAB .
-
values 5 "{y. notAB y}"
end
--- 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 \<and> \<not> 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
--- 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
--- 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