tuned config options: eliminated separate attribute "option";
authorwenzelm
Wed Aug 01 16:55:37 2007 +0200 (2007-08-01)
changeset 241104ab3084e311c
parent 24109 952efb77cf91
child 24111 20e74aa5f56b
tuned config options: eliminated separate attribute "option";
NEWS
doc-src/IsarImplementation/Thy/ML.thy
doc-src/IsarImplementation/Thy/document/ML.tex
doc-src/IsarRef/generic.tex
src/HOL/HoareParallel/Graph.thy
src/HOL/MicroJava/Comp/CorrCompTp.thy
src/HOL/Nominal/nominal_package.ML
src/Pure/Isar/attrib.ML
     1.1 --- a/NEWS	Wed Aug 01 16:50:16 2007 +0200
     1.2 +++ b/NEWS	Wed Aug 01 16:55:37 2007 +0200
     1.3 @@ -164,19 +164,21 @@
     1.4  * Configuration options are maintained within the theory or proof
     1.5  context (with name and type bool/int/string), providing a very simple
     1.6  interface to a poor-man's version of general context data.  Tools may
     1.7 -declare options in ML (e.g. using ConfigOption.int) and then refer to
     1.8 -these values using ConfigOption.get etc.  Users may change options via
     1.9 -the "option" attribute, which works particularly well with commands
    1.10 -'declare' or 'using', for example ``declare [[option foo = 42]]''.
    1.11 -Thus global reference variables are easily avoided, which do not
    1.12 -observe Isar toplevel undo/redo and fail to work with multithreading.
    1.13 +declare options in ML (e.g. using Attrib.config_int) and then refer to
    1.14 +these values using Config.get etc.  Users may change options via an
    1.15 +associated attribute of the same name.  This form of context
    1.16 +declaration works particularly well with commands 'declare' or
    1.17 +'using', for example ``declare [[foo = 42]]''.  Thus it has become
    1.18 +very easy to avoid global references, which would not observe Isar
    1.19 +toplevel undo/redo and fail to work with multithreading.
    1.20  
    1.21  * Named collections of theorems may be easily installed as context
    1.22  data using the functor NamedThmsFun (see
    1.23  src/Pure/Tools/named_thms.ML).  The user may add or delete facts via
    1.24 -attributes.  This is just a common case of general context data, which
    1.25 -is the preferred way for anything more complex than just a list of
    1.26 -facts in canonical order.
    1.27 +attributes; there is also a toplevel print command.  This facility is
    1.28 +just a common case of general context data, which is the preferred way
    1.29 +for anything more complex than just a list of facts in canonical
    1.30 +order.
    1.31  
    1.32  * Isar: command 'declaration' augments a local theory by generic
    1.33  declaration functions written in ML.  This enables arbitrary content
     2.1 --- a/doc-src/IsarImplementation/Thy/ML.thy	Wed Aug 01 16:50:16 2007 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/ML.thy	Wed Aug 01 16:55:37 2007 +0200
     2.3 @@ -196,8 +196,9 @@
     2.4    \secref{sec:context-data}) there are drop-in replacements that
     2.5    emulate primitive references for common cases of \emph{configuration
     2.6    options} for type @{ML_type "bool"}/@{ML_type "int"}/@{ML_type
     2.7 -  "string"} (see structure @{ML_struct ConfigOption}) and lists of
     2.8 -  theorems (see functor @{ML_functor NamedThmsFun}).
     2.9 +  "string"} (see structure @{ML_struct Config} and @{ML
    2.10 +  Attrib.config_bool} etc.), and lists of theorems (see functor
    2.11 +  @{ML_functor NamedThmsFun}).
    2.12  
    2.13    \item Keep components with local state information
    2.14    \emph{re-entrant}.  Instead of poking initial values into (private)
     3.1 --- a/doc-src/IsarImplementation/Thy/document/ML.tex	Wed Aug 01 16:50:16 2007 +0200
     3.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Wed Aug 01 16:55:37 2007 +0200
     3.3 @@ -217,8 +217,8 @@
     3.4    from the fully general functors for theory and proof data (see
     3.5    \secref{sec:context-data}) there are drop-in replacements that
     3.6    emulate primitive references for common cases of \emph{configuration
     3.7 -  options} for type \verb|bool|/\verb|int|/\verb|string| (see structure \verb|ConfigOption|) and lists of
     3.8 -  theorems (see functor \verb|NamedThmsFun|).
     3.9 +  options} for type \verb|bool|/\verb|int|/\verb|string| (see structure \verb|Config| and \verb|Attrib.config_bool| etc.), and lists of theorems (see functor
    3.10 +  \verb|NamedThmsFun|).
    3.11  
    3.12    \item Keep components with local state information
    3.13    \emph{re-entrant}.  Instead of poking initial values into (private)
     4.1 --- a/doc-src/IsarRef/generic.tex	Wed Aug 01 16:50:16 2007 +0200
     4.2 +++ b/doc-src/IsarRef/generic.tex	Wed Aug 01 16:55:37 2007 +0200
     4.3 @@ -631,13 +631,13 @@
     4.4  
     4.5  \subsection{Configuration options}
     4.6  
     4.7 -Isabelle/Pure maintains a record of named configuration options within
     4.8 -the theory or proof context, with values of type $bool$, $int$, or
     4.9 -$string$.  Tools may declare options in ML, and then refer to these
    4.10 -values (relative to the context).  Thus global reference variables are
    4.11 -easily avoided.  The user may change the values of configuration
    4.12 -options by means of the $option$ attribute, which works particularly
    4.13 -well with commands such as $\isarkeyword{declare}$ or
    4.14 +Isabelle/Pure maintains a record of named configuration options within the
    4.15 +theory or proof context, with values of type $bool$, $int$, or $string$.
    4.16 +Tools may declare options in ML, and then refer to these values (relative to
    4.17 +the context).  Thus global reference variables are easily avoided.  The user
    4.18 +may change the value of a configuration option by means of an associated
    4.19 +attribute of the same name.  This form of context declaration works
    4.20 +particularly well with commands such as $\isarkeyword{declare}$ or
    4.21  $\isarkeyword{using}$.
    4.22  
    4.23  For historical reasons, some tools cannot take the full proof context
    4.24 @@ -645,25 +645,24 @@
    4.25  accommodated by configuration options being declared as ``global'',
    4.26  which may not be changed within a local context.
    4.27  
    4.28 -\indexisaratt{option}\indexisarcmd{print-options}
    4.29 +\indexisarcmd{print-configs}
    4.30  \begin{matharray}{rcll}
    4.31 -  \isarcmd{print_options} & : & \isarkeep{theory~|~proof} \\
    4.32 -  option & : & \isaratt \\
    4.33 +  \isarcmd{print_configs} & : & \isarkeep{theory~|~proof} \\
    4.34  \end{matharray}
    4.35  
    4.36  \begin{rail}
    4.37 -  'option' name ('=' ('true' | 'false' | int | name))?
    4.38 +  name ('=' ('true' | 'false' | int | name))?
    4.39  \end{rail}
    4.40  
    4.41  \begin{descr}
    4.42 -
    4.43 -\item [$\isarkeyword{print_options}$] prints the available
    4.44 -  configuration options, with names, types, and current values.
    4.45 -
    4.46 -\item [$option~name = value$] modifies the named option, with the
    4.47 -  syntax of the value depending on the option's type.  For $bool$ the
    4.48 -  default value is $true$.  Any attempt to change a global option
    4.49 -  locally is ignored.
    4.50 +  
    4.51 +\item [$\isarkeyword{print_configs}$] prints the available configuration
    4.52 +  options, with names, types, and current values.
    4.53 +  
    4.54 +\item [$name = value$] as an attribute expression modifies the named option,
    4.55 +  with the syntax of the value depending on the option's type.  For $bool$ the
    4.56 +  default value is $true$.  Any attempt to change a global option in a local
    4.57 +  context is ignored.
    4.58  
    4.59  \end{descr}
    4.60  
     5.1 --- a/src/HOL/HoareParallel/Graph.thy	Wed Aug 01 16:50:16 2007 +0200
     5.2 +++ b/src/HOL/HoareParallel/Graph.thy	Wed Aug 01 16:55:37 2007 +0200
     5.3 @@ -173,9 +173,9 @@
     5.4   prefer 2 apply arith
     5.5   apply(drule_tac n = "Suc nata" in Compl_lemma)
     5.6   apply clarify
     5.7 - using [[option fast_arith_split_limit = 0]]
     5.8 + using [[fast_arith_split_limit = 0]]
     5.9   apply force
    5.10 - using [[option fast_arith_split_limit = 9]]
    5.11 + using [[fast_arith_split_limit = 9]]
    5.12  apply(drule leI)
    5.13  apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)")
    5.14   apply(erule_tac x = "m - (Suc nata)" in allE)
     6.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Aug 01 16:50:16 2007 +0200
     6.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Aug 01 16:55:37 2007 +0200
     6.3 @@ -454,7 +454,7 @@
     6.4  apply (simp add: max_of_list_def)
     6.5  apply (induct xs)
     6.6  apply simp
     6.7 -using [[option fast_arith_split_limit = 0]]
     6.8 +using [[fast_arith_split_limit = 0]]
     6.9  apply simp
    6.10  apply arith
    6.11  done
     7.1 --- a/src/HOL/Nominal/nominal_package.ML	Wed Aug 01 16:50:16 2007 +0200
     7.2 +++ b/src/HOL/Nominal/nominal_package.ML	Wed Aug 01 16:55:37 2007 +0200
     7.3 @@ -880,10 +880,10 @@
     7.4  
     7.5      (* prove distinctness theorems *)
     7.6  
     7.7 -    val distinctness_limit = ConfigOption.get_thy thy8 DatatypeProp.distinctness_limit;
     7.8 -    val thy8' = ConfigOption.put_thy DatatypeProp.distinctness_limit 1000 thy8;
     7.9 +    val distinctness_limit = Config.get_thy thy8 DatatypeProp.distinctness_limit;
    7.10 +    val thy8' = Config.put_thy DatatypeProp.distinctness_limit 1000 thy8;
    7.11      val distinct_props = DatatypeProp.make_distincts new_type_names descr' sorts' thy8';
    7.12 -    val thy8 = ConfigOption.put_thy DatatypeProp.distinctness_limit distinctness_limit thy8';
    7.13 +    val thy8 = Config.put_thy DatatypeProp.distinctness_limit distinctness_limit thy8';
    7.14  
    7.15      val dist_rewrites = map (fn (rep_thms, dist_lemma) =>
    7.16        dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
     8.1 --- a/src/Pure/Isar/attrib.ML	Wed Aug 01 16:50:16 2007 +0200
     8.2 +++ b/src/Pure/Isar/attrib.ML	Wed Aug 01 16:55:37 2007 +0200
     8.3 @@ -26,6 +26,14 @@
     8.4      (('c * 'att list) * ('d * 'att list) list) list
     8.5    val crude_closure: Proof.context -> src -> src
     8.6    val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
     8.7 +  val print_configs: Proof.context -> unit
     8.8 +  val register_config: bstring -> Config.value Config.T -> theory -> theory
     8.9 +  val config_bool: bstring -> bool -> bool Config.T * (theory -> theory)
    8.10 +  val config_int: bstring -> int -> int Config.T * (theory -> theory)
    8.11 +  val config_string: bstring -> string -> string Config.T * (theory -> theory)
    8.12 +  val config_bool_global: bstring -> bool -> bool Config.T * (theory -> theory)
    8.13 +  val config_int_global: bstring -> int -> int Config.T * (theory -> theory)
    8.14 +  val config_string_global: bstring -> string -> string Config.T * (theory -> theory)
    8.15    val thm: Context.generic * Args.T list -> thm * (Context.generic * Args.T list)
    8.16    val thms: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
    8.17    val multi_thm: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
    8.18 @@ -46,7 +54,7 @@
    8.19  
    8.20  (* theory data *)
    8.21  
    8.22 -structure AttributesData = TheoryDataFun
    8.23 +structure Attributes = TheoryDataFun
    8.24  (
    8.25    type T = (((src -> attribute) * string) * stamp) NameSpace.table;
    8.26    val empty = NameSpace.empty_table;
    8.27 @@ -58,7 +66,7 @@
    8.28  
    8.29  fun print_attributes thy =
    8.30    let
    8.31 -    val attribs = AttributesData.get thy;
    8.32 +    val attribs = Attributes.get thy;
    8.33      fun prt_attr (name, ((_, comment), _)) = Pretty.block
    8.34        [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    8.35    in
    8.36 @@ -69,10 +77,10 @@
    8.37  
    8.38  (* name space *)
    8.39  
    8.40 -val intern = NameSpace.intern o #1 o AttributesData.get;
    8.41 +val intern = NameSpace.intern o #1 o Attributes.get;
    8.42  val intern_src = Args.map_name o intern;
    8.43  
    8.44 -val extern = NameSpace.extern o #1 o AttributesData.get o ProofContext.theory_of;
    8.45 +val extern = NameSpace.extern o #1 o Attributes.get o ProofContext.theory_of;
    8.46  
    8.47  
    8.48  (* pretty printing *)
    8.49 @@ -87,7 +95,7 @@
    8.50  
    8.51  fun attribute_i thy =
    8.52    let
    8.53 -    val attrs = #2 (AttributesData.get thy);
    8.54 +    val attrs = #2 (Attributes.get thy);
    8.55      fun attr src =
    8.56        let val ((name, _), pos) = Args.dest_src src in
    8.57          (case Symtab.lookup attrs name of
    8.58 @@ -125,7 +133,7 @@
    8.59        raw_attrs |> map (fn (name, att, comment) => (name, ((att, comment), stamp ())));
    8.60      fun add attrs = NameSpace.extend_table (Sign.naming_of thy) new_attrs attrs
    8.61        handle Symtab.DUP dup => error ("Duplicate declaration of attributes " ^ quote dup);
    8.62 -  in AttributesData.map add thy end;
    8.63 +  in Attributes.map add thy end;
    8.64  
    8.65  
    8.66  
    8.67 @@ -188,39 +196,76 @@
    8.68  
    8.69  
    8.70  
    8.71 -(** basic attributes **)
    8.72 +(** configuration options **)
    8.73 +
    8.74 +(* naming *)
    8.75 +
    8.76 +structure Configs = TheoryDataFun
    8.77 +(struct
    8.78 +  type T = Config.value Config.T Symtab.table;
    8.79 +  val empty = Symtab.empty;
    8.80 +  val copy = I;
    8.81 +  val extend = I;
    8.82 +  fun merge _ = Symtab.merge (K true);
    8.83 +end);
    8.84  
    8.85 -(* configuration options *)
    8.86 +fun print_configs ctxt =
    8.87 +  let
    8.88 +    val thy = ProofContext.theory_of ctxt;
    8.89 +    fun prt (name, config) =
    8.90 +      let val value = Config.get ctxt config in
    8.91 +        Pretty.block [Pretty.str (name ^ ": " ^ Config.print_type value ^ " ="), Pretty.brk 1,
    8.92 +          Pretty.str (Config.print_value value)]
    8.93 +      end;
    8.94 +    val configs = NameSpace.extern_table (#1 (Attributes.get thy), Configs.get thy);
    8.95 +  in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
    8.96 +
    8.97 +
    8.98 +(* concrete syntax *)
    8.99  
   8.100  local
   8.101  
   8.102  val equals = Args.$$$ "=";
   8.103  
   8.104 -fun scan_value (ConfigOption.Bool _) =
   8.105 -      (equals -- Args.$$$ "false") >> K (ConfigOption.Bool false) ||
   8.106 -      (equals -- Args.$$$ "true") >> K (ConfigOption.Bool true) ||
   8.107 -      (Scan.succeed (ConfigOption.Bool true))
   8.108 -  | scan_value (ConfigOption.Int _) = (equals |-- Args.int) >> ConfigOption.Int
   8.109 -  | scan_value (ConfigOption.String _) = (equals |-- Args.name) >> ConfigOption.String;
   8.110 +fun scan_value (Config.Bool _) =
   8.111 +      equals -- Args.$$$ "false" >> K (Config.Bool false) ||
   8.112 +      equals -- Args.$$$ "true" >> K (Config.Bool true) ||
   8.113 +      Scan.succeed (Config.Bool true)
   8.114 +  | scan_value (Config.Int _) = equals |-- Args.int >> Config.Int
   8.115 +  | scan_value (Config.String _) = equals |-- Args.name >> Config.String;
   8.116  
   8.117 -fun scan_config thy =
   8.118 -  (Args.name >> ConfigOption.the_option thy) :|-- (fn (config, config_type) =>
   8.119 -    scan_value config_type >> (fn value =>
   8.120 -      K (Thm.declaration_attribute (K (ConfigOption.put_generic config value)))));
   8.121 -
   8.122 -fun scan_att thy =
   8.123 -  (Args.internal_attribute ||
   8.124 -    (Scan.ahead (scan_config thy --| Args.terminator) :|--
   8.125 -      (fn att => Args.named_attribute (K att))));
   8.126 +fun scan_config thy config =
   8.127 +  let val config_type = Config.get_thy thy config
   8.128 +  in scan_value config_type >> (K o Thm.declaration_attribute o K o Config.put_generic config) end;
   8.129  
   8.130  in
   8.131  
   8.132 -fun option x = syntax (Scan.peek (fn context =>
   8.133 -  (scan_att (Context.theory_of context) >> Morphism.form) --| Scan.many Args.not_eof)) x;
   8.134 +fun register_config name config thy =
   8.135 +  thy
   8.136 +  |> add_attributes
   8.137 +    [(name, syntax (Scan.lift (scan_config thy config) >> Morphism.form), "configuration option")]
   8.138 +  |> Configs.map (Symtab.update (Sign.full_name thy name, config));
   8.139 +
   8.140 +fun declare_config make coerce global name default =
   8.141 +  let
   8.142 +    val config_value = Config.declare global name (make default);
   8.143 +    val config = coerce config_value;
   8.144 +  in (config, register_config name config_value) end;
   8.145 +
   8.146 +val config_bool   = declare_config Config.Bool Config.bool false;
   8.147 +val config_int    = declare_config Config.Int Config.int false;
   8.148 +val config_string = declare_config Config.String Config.string false;
   8.149 +
   8.150 +val config_bool_global   = declare_config Config.Bool Config.bool true;
   8.151 +val config_int_global    = declare_config Config.Int Config.int true;
   8.152 +val config_string_global = declare_config Config.String Config.string true;
   8.153  
   8.154  end;
   8.155  
   8.156  
   8.157 +
   8.158 +(** basic attributes **)
   8.159 +
   8.160  (* tags *)
   8.161  
   8.162  fun tagged x = syntax (tag >> PureThy.tag) x;
   8.163 @@ -300,8 +345,7 @@
   8.164  
   8.165  val _ = Context.add_setup
   8.166   (add_attributes
   8.167 -   [("option", option, "named configuration option"),
   8.168 -    ("tagged", tagged, "tagged theorem"),
   8.169 +   [("tagged", tagged, "tagged theorem"),
   8.170      ("untagged", untagged, "untagged theorem"),
   8.171      ("kind", kind, "theorem kind"),
   8.172      ("COMP", COMP_att, "direct composition with rules (no lifting)"),