# HG changeset patch
# User bulwahn
# Date 1283234453 -7200
# Node ID 62578950e748c547184c297b298da0261280248b
# Parent  1afa9e89c8850cd477cec9dfba3c65836a08deea
storing options for prolog code generation in the theory

diff -r 1afa9e89c885 -r 62578950e748 src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
--- 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}"
 
diff -r 1afa9e89c885 -r 62578950e748 src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
--- 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}"
 
diff -r 1afa9e89c885 -r 62578950e748 src/HOL/Predicate_Compile_Examples/Lambda_Example.thy
--- 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"
diff -r 1afa9e89c885 -r 62578950e748 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- 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))