storing options for prolog code generation in the theory
authorbulwahn
Tue Aug 31 08:00:53 2010 +0200 (2010-08-31)
changeset 3895062578950e748
parent 38949 1afa9e89c885
child 38951 a16ee2b38db2
storing options for prolog code generation in the theory
src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
src/HOL/Predicate_Compile_Examples/Lambda_Example.thy
src/HOL/Tools/Predicate_Compile/code_prolog.ML
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Tue Aug 31 08:00:52 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Tue Aug 31 08:00:53 2010 +0200
     1.3 @@ -10,26 +10,25 @@
     1.4    "append [] ys ys"
     1.5  | "append xs ys zs ==> append (x # xs) ys (x # zs)"
     1.6  
     1.7 -ML {* Code_Prolog.options :=
     1.8 -  {ensure_groundness = false,
     1.9 +setup {* Code_Prolog.map_code_options (K {ensure_groundness = false,
    1.10     limited_types = [], limited_predicates = [], replacing = [],
    1.11 -   prolog_system = Code_Prolog.SWI_PROLOG} *}
    1.12 +   prolog_system = Code_Prolog.SWI_PROLOG}) *}
    1.13  
    1.14  values "{(x, y, z). append x y z}"
    1.15  
    1.16  values 3 "{(x, y, z). append x y z}"
    1.17  
    1.18 -ML {* Code_Prolog.options :=
    1.19 +setup {* Code_Prolog.map_code_options (K
    1.20    {ensure_groundness = false,
    1.21     limited_types = [], limited_predicates = [], replacing = [],
    1.22 -   prolog_system = Code_Prolog.YAP} *}
    1.23 +   prolog_system = Code_Prolog.YAP}) *}
    1.24  
    1.25  values "{(x, y, z). append x y z}"
    1.26  
    1.27 -ML {* Code_Prolog.options :=
    1.28 +setup {* Code_Prolog.map_code_options (K
    1.29    {ensure_groundness = false,
    1.30     limited_types = [], limited_predicates = [], replacing = [],
    1.31 -   prolog_system = Code_Prolog.SWI_PROLOG} *}
    1.32 +   prolog_system = Code_Prolog.SWI_PROLOG}) *}
    1.33  
    1.34  
    1.35  section {* Example queens *}
    1.36 @@ -192,11 +191,11 @@
    1.37  where
    1.38    "y \<noteq> B \<Longrightarrow> notB y"
    1.39  
    1.40 -ML {* Code_Prolog.options := {ensure_groundness = true,
    1.41 +setup {* Code_Prolog.map_code_options (K {ensure_groundness = true,
    1.42    limited_types = [],
    1.43    limited_predicates = [],
    1.44    replacing = [], 
    1.45 -  prolog_system = Code_Prolog.SWI_PROLOG} *}
    1.46 +  prolog_system = Code_Prolog.SWI_PROLOG}) *}
    1.47  
    1.48  values 2 "{y. notB y}"
    1.49  
     2.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Aug 31 08:00:52 2010 +0200
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Aug 31 08:00:53 2010 +0200
     2.3 @@ -84,12 +84,12 @@
     2.4  lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
     2.5  by (auto simp add: Diff_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection)
     2.6  
     2.7 -ML {* Code_Prolog.options :=
     2.8 +setup {* Code_Prolog.map_code_options (K
     2.9    {ensure_groundness = true,
    2.10    limited_types = [],
    2.11    limited_predicates = [],
    2.12    replacing = [],
    2.13 -  prolog_system = Code_Prolog.SWI_PROLOG} *}
    2.14 +  prolog_system = Code_Prolog.SWI_PROLOG}) *}
    2.15  
    2.16  values 40 "{s. hotel s}"
    2.17  
     3.1 --- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Tue Aug 31 08:00:52 2010 +0200
     3.2 +++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Tue Aug 31 08:00:53 2010 +0200
     3.3 @@ -81,13 +81,13 @@
     3.4  
     3.5  setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
     3.6  
     3.7 -ML {* Code_Prolog.options :=
     3.8 +setup {* Code_Prolog.map_code_options (K 
     3.9    { ensure_groundness = true,
    3.10      limited_types = [(@{typ nat}, 1), (@{typ "type"}, 1), (@{typ dB}, 1), (@{typ "type list"}, 1)],
    3.11      limited_predicates = [("typing", 2), ("nth_el1", 2)],
    3.12      replacing = [(("typing", "limited_typing"), "quickcheck"),
    3.13                   (("nth_el1", "limited_nth_el1"), "lim_typing")],
    3.14 -    prolog_system = Code_Prolog.SWI_PROLOG} *}
    3.15 +    prolog_system = Code_Prolog.SWI_PROLOG}) *}
    3.16  
    3.17  lemma
    3.18    "\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
     4.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Tue Aug 31 08:00:52 2010 +0200
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Tue Aug 31 08:00:53 2010 +0200
     4.3 @@ -13,7 +13,8 @@
     4.4       limited_predicates : (string * int) list,
     4.5       replacing : ((string * string) * string) list,
     4.6       prolog_system : prolog_system}
     4.7 -  val options : code_options Unsynchronized.ref
     4.8 +  val code_options_of : theory -> code_options 
     4.9 +  val map_code_options : (code_options -> code_options) -> theory -> theory
    4.10  
    4.11    datatype arith_op = Plus | Minus
    4.12    datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list
    4.13 @@ -60,9 +61,28 @@
    4.14     replacing : ((string * string) * string) list,
    4.15     prolog_system : prolog_system}
    4.16  
    4.17 -val options = Unsynchronized.ref {ensure_groundness = false,
    4.18 -  limited_types = [], limited_predicates = [], replacing = [],
    4.19 -  prolog_system = SWI_PROLOG};
    4.20 +structure Options = Theory_Data
    4.21 +(
    4.22 +  type T = code_options
    4.23 +  val empty = {ensure_groundness = false,
    4.24 +    limited_types = [], limited_predicates = [], replacing = [],
    4.25 +    prolog_system = SWI_PROLOG}
    4.26 +  val extend = I;
    4.27 +  fun merge
    4.28 +    ({ensure_groundness = ensure_groundness1, limited_types = limited_types1,
    4.29 +      limited_predicates = limited_predicates1, replacing = replacing1, prolog_system = prolog_system1},
    4.30 +     {ensure_groundness = ensure_groundness2, limited_types = limited_types2,
    4.31 +      limited_predicates = limited_predicates2, replacing = replacing2, prolog_system = prolog_system2}) =
    4.32 +    {ensure_groundness = ensure_groundness1 orelse ensure_groundness2,
    4.33 +     limited_types = AList.merge (op =) (K true) (limited_types1, limited_types2),
    4.34 +     limited_predicates = AList.merge (op =) (K true) (limited_predicates1, limited_predicates2),
    4.35 +     replacing = Library.merge (op =) (replacing1, replacing2),
    4.36 +     prolog_system = prolog_system1};
    4.37 +);
    4.38 +
    4.39 +val code_options_of = Options.get
    4.40 +
    4.41 +val map_code_options = Options.map
    4.42  
    4.43  (* general string functions *)
    4.44  
    4.45 @@ -641,7 +661,7 @@
    4.46  
    4.47  fun values ctxt soln t_compr =
    4.48    let
    4.49 -    val options = !options
    4.50 +    val options = code_options_of (ProofContext.theory_of ctxt)
    4.51      val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
    4.52        | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr);
    4.53      val (body, Ts, fp) = HOLogic.strip_psplits split;
    4.54 @@ -741,6 +761,7 @@
    4.55  
    4.56  fun quickcheck ctxt report t size =
    4.57    let
    4.58 +    val options = code_options_of (ProofContext.theory_of ctxt)
    4.59      val thy = Theory.copy (ProofContext.theory_of ctxt)
    4.60      val (vs, t') = strip_abs t
    4.61      val vs' = Variable.variant_frees ctxt [] vs
    4.62 @@ -762,11 +783,11 @@
    4.63      val ctxt' = ProofContext.init_global thy3
    4.64      val _ = tracing "Generating prolog program..."
    4.65      val (p, constant_table) = generate true ctxt' full_constname
    4.66 -      |> add_ground_predicates ctxt' (#limited_types (!options))
    4.67 -      |> add_limited_predicates (#limited_predicates (!options))
    4.68 -      |> apfst (fold replace (#replacing (!options)))      
    4.69 +      |> add_ground_predicates ctxt' (#limited_types options)
    4.70 +      |> add_limited_predicates (#limited_predicates options)
    4.71 +      |> apfst (fold replace (#replacing options))     
    4.72      val _ = tracing "Running prolog program..."
    4.73 -    val [ts] = run (#prolog_system (!options))
    4.74 +    val [ts] = run (#prolog_system options)
    4.75        p (translate_const constant_table full_constname) (map fst vs') (SOME 1)
    4.76      val _ = tracing "Restoring terms..."
    4.77      val res = SOME (map (restore_term ctxt' constant_table) (ts ~~ Ts))