--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Tue Aug 31 08:00:52 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Tue Aug 31 08:00:53 2010 +0200
@@ -10,26 +10,25 @@
"append [] ys ys"
| "append xs ys zs ==> append (x # xs) ys (x # zs)"
-ML {* Code_Prolog.options :=
- {ensure_groundness = false,
+setup {* Code_Prolog.map_code_options (K {ensure_groundness = false,
limited_types = [], limited_predicates = [], replacing = [],
- prolog_system = Code_Prolog.SWI_PROLOG} *}
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
values "{(x, y, z). append x y z}"
values 3 "{(x, y, z). append x y z}"
-ML {* Code_Prolog.options :=
+setup {* Code_Prolog.map_code_options (K
{ensure_groundness = false,
limited_types = [], limited_predicates = [], replacing = [],
- prolog_system = Code_Prolog.YAP} *}
+ prolog_system = Code_Prolog.YAP}) *}
values "{(x, y, z). append x y z}"
-ML {* Code_Prolog.options :=
+setup {* Code_Prolog.map_code_options (K
{ensure_groundness = false,
limited_types = [], limited_predicates = [], replacing = [],
- prolog_system = Code_Prolog.SWI_PROLOG} *}
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
section {* Example queens *}
@@ -192,11 +191,11 @@
where
"y \<noteq> B \<Longrightarrow> notB y"
-ML {* Code_Prolog.options := {ensure_groundness = true,
+setup {* Code_Prolog.map_code_options (K {ensure_groundness = true,
limited_types = [],
limited_predicates = [],
replacing = [],
- prolog_system = Code_Prolog.SWI_PROLOG} *}
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
values 2 "{y. notB y}"
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Tue Aug 31 08:00:52 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Tue Aug 31 08:00:53 2010 +0200
@@ -84,12 +84,12 @@
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)
-ML {* Code_Prolog.options :=
+setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
limited_types = [],
limited_predicates = [],
replacing = [],
- prolog_system = Code_Prolog.SWI_PROLOG} *}
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
values 40 "{s. hotel s}"
--- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Tue Aug 31 08:00:52 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Tue Aug 31 08:00:53 2010 +0200
@@ -81,13 +81,13 @@
setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
-ML {* Code_Prolog.options :=
+setup {* Code_Prolog.map_code_options (K
{ ensure_groundness = true,
limited_types = [(@{typ nat}, 1), (@{typ "type"}, 1), (@{typ dB}, 1), (@{typ "type list"}, 1)],
limited_predicates = [("typing", 2), ("nth_el1", 2)],
replacing = [(("typing", "limited_typing"), "quickcheck"),
(("nth_el1", "limited_nth_el1"), "lim_typing")],
- prolog_system = Code_Prolog.SWI_PROLOG} *}
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
lemma
"\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Tue Aug 31 08:00:52 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Tue Aug 31 08:00:53 2010 +0200
@@ -13,7 +13,8 @@
limited_predicates : (string * int) list,
replacing : ((string * string) * string) list,
prolog_system : prolog_system}
- val options : code_options Unsynchronized.ref
+ val code_options_of : theory -> code_options
+ val map_code_options : (code_options -> code_options) -> theory -> theory
datatype arith_op = Plus | Minus
datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list
@@ -60,9 +61,28 @@
replacing : ((string * string) * string) list,
prolog_system : prolog_system}
-val options = Unsynchronized.ref {ensure_groundness = false,
- limited_types = [], limited_predicates = [], replacing = [],
- prolog_system = SWI_PROLOG};
+structure Options = Theory_Data
+(
+ type T = code_options
+ val empty = {ensure_groundness = false,
+ limited_types = [], limited_predicates = [], replacing = [],
+ prolog_system = SWI_PROLOG}
+ val extend = I;
+ fun merge
+ ({ensure_groundness = ensure_groundness1, limited_types = limited_types1,
+ limited_predicates = limited_predicates1, replacing = replacing1, prolog_system = prolog_system1},
+ {ensure_groundness = ensure_groundness2, limited_types = limited_types2,
+ limited_predicates = limited_predicates2, replacing = replacing2, prolog_system = prolog_system2}) =
+ {ensure_groundness = ensure_groundness1 orelse ensure_groundness2,
+ limited_types = AList.merge (op =) (K true) (limited_types1, limited_types2),
+ limited_predicates = AList.merge (op =) (K true) (limited_predicates1, limited_predicates2),
+ replacing = Library.merge (op =) (replacing1, replacing2),
+ prolog_system = prolog_system1};
+);
+
+val code_options_of = Options.get
+
+val map_code_options = Options.map
(* general string functions *)
@@ -641,7 +661,7 @@
fun values ctxt soln t_compr =
let
- val options = !options
+ val options = code_options_of (ProofContext.theory_of ctxt)
val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
| _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr);
val (body, Ts, fp) = HOLogic.strip_psplits split;
@@ -741,6 +761,7 @@
fun quickcheck ctxt report t size =
let
+ val options = code_options_of (ProofContext.theory_of ctxt)
val thy = Theory.copy (ProofContext.theory_of ctxt)
val (vs, t') = strip_abs t
val vs' = Variable.variant_frees ctxt [] vs
@@ -762,11 +783,11 @@
val ctxt' = ProofContext.init_global thy3
val _ = tracing "Generating prolog program..."
val (p, constant_table) = generate true ctxt' full_constname
- |> add_ground_predicates ctxt' (#limited_types (!options))
- |> add_limited_predicates (#limited_predicates (!options))
- |> apfst (fold replace (#replacing (!options)))
+ |> add_ground_predicates ctxt' (#limited_types options)
+ |> add_limited_predicates (#limited_predicates options)
+ |> apfst (fold replace (#replacing options))
val _ = tracing "Running prolog program..."
- val [ts] = run (#prolog_system (!options))
+ val [ts] = run (#prolog_system options)
p (translate_const constant_table full_constname) (map fst vs') (SOME 1)
val _ = tracing "Restoring terms..."
val res = SOME (map (restore_term ctxt' constant_table) (ts ~~ Ts))