# HG changeset patch # User wenzelm # Date 1185980137 -7200 # Node ID 4ab3084e311c973ac2a236bba49968c9a04a1655 # Parent 952efb77cf9130e2f4feb626144a5a3c65d8d712 tuned config options: eliminated separate attribute "option"; diff -r 952efb77cf91 -r 4ab3084e311c NEWS --- a/NEWS Wed Aug 01 16:50:16 2007 +0200 +++ b/NEWS Wed Aug 01 16:55:37 2007 +0200 @@ -164,19 +164,21 @@ * Configuration options are maintained within the theory or proof context (with name and type bool/int/string), providing a very simple interface to a poor-man's version of general context data. Tools may -declare options in ML (e.g. using ConfigOption.int) and then refer to -these values using ConfigOption.get etc. Users may change options via -the "option" attribute, which works particularly well with commands -'declare' or 'using', for example ``declare [[option foo = 42]]''. -Thus global reference variables are easily avoided, which do not -observe Isar toplevel undo/redo and fail to work with multithreading. +declare options in ML (e.g. using Attrib.config_int) and then refer to +these values using Config.get etc. Users may change options via an +associated attribute of the same name. This form of context +declaration works particularly well with commands 'declare' or +'using', for example ``declare [[foo = 42]]''. Thus it has become +very easy to avoid global references, which would not observe Isar +toplevel undo/redo and fail to work with multithreading. * Named collections of theorems may be easily installed as context data using the functor NamedThmsFun (see src/Pure/Tools/named_thms.ML). The user may add or delete facts via -attributes. This is just a common case of general context data, which -is the preferred way for anything more complex than just a list of -facts in canonical order. +attributes; there is also a toplevel print command. This facility is +just a common case of general context data, which is the preferred way +for anything more complex than just a list of facts in canonical +order. * Isar: command 'declaration' augments a local theory by generic declaration functions written in ML. This enables arbitrary content diff -r 952efb77cf91 -r 4ab3084e311c doc-src/IsarImplementation/Thy/ML.thy --- a/doc-src/IsarImplementation/Thy/ML.thy Wed Aug 01 16:50:16 2007 +0200 +++ b/doc-src/IsarImplementation/Thy/ML.thy Wed Aug 01 16:55:37 2007 +0200 @@ -196,8 +196,9 @@ \secref{sec:context-data}) there are drop-in replacements that emulate primitive references for common cases of \emph{configuration options} for type @{ML_type "bool"}/@{ML_type "int"}/@{ML_type - "string"} (see structure @{ML_struct ConfigOption}) and lists of - theorems (see functor @{ML_functor NamedThmsFun}). + "string"} (see structure @{ML_struct Config} and @{ML + Attrib.config_bool} etc.), and lists of theorems (see functor + @{ML_functor NamedThmsFun}). \item Keep components with local state information \emph{re-entrant}. Instead of poking initial values into (private) diff -r 952efb77cf91 -r 4ab3084e311c doc-src/IsarImplementation/Thy/document/ML.tex --- a/doc-src/IsarImplementation/Thy/document/ML.tex Wed Aug 01 16:50:16 2007 +0200 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex Wed Aug 01 16:55:37 2007 +0200 @@ -217,8 +217,8 @@ from the fully general functors for theory and proof data (see \secref{sec:context-data}) there are drop-in replacements that emulate primitive references for common cases of \emph{configuration - options} for type \verb|bool|/\verb|int|/\verb|string| (see structure \verb|ConfigOption|) and lists of - theorems (see functor \verb|NamedThmsFun|). + 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 + \verb|NamedThmsFun|). \item Keep components with local state information \emph{re-entrant}. Instead of poking initial values into (private) diff -r 952efb77cf91 -r 4ab3084e311c doc-src/IsarRef/generic.tex --- a/doc-src/IsarRef/generic.tex Wed Aug 01 16:50:16 2007 +0200 +++ b/doc-src/IsarRef/generic.tex Wed Aug 01 16:55:37 2007 +0200 @@ -631,13 +631,13 @@ \subsection{Configuration options} -Isabelle/Pure maintains a record of named configuration options within -the theory or proof context, with values of type $bool$, $int$, or -$string$. Tools may declare options in ML, and then refer to these -values (relative to the context). Thus global reference variables are -easily avoided. The user may change the values of configuration -options by means of the $option$ attribute, which works particularly -well with commands such as $\isarkeyword{declare}$ or +Isabelle/Pure maintains a record of named configuration options within the +theory or proof context, with values of type $bool$, $int$, or $string$. +Tools may declare options in ML, and then refer to these values (relative to +the context). Thus global reference variables are easily avoided. The user +may change the value of a configuration option by means of an associated +attribute of the same name. This form of context declaration works +particularly well with commands such as $\isarkeyword{declare}$ or $\isarkeyword{using}$. For historical reasons, some tools cannot take the full proof context @@ -645,25 +645,24 @@ accommodated by configuration options being declared as ``global'', which may not be changed within a local context. -\indexisaratt{option}\indexisarcmd{print-options} +\indexisarcmd{print-configs} \begin{matharray}{rcll} - \isarcmd{print_options} & : & \isarkeep{theory~|~proof} \\ - option & : & \isaratt \\ + \isarcmd{print_configs} & : & \isarkeep{theory~|~proof} \\ \end{matharray} \begin{rail} - 'option' name ('=' ('true' | 'false' | int | name))? + name ('=' ('true' | 'false' | int | name))? \end{rail} \begin{descr} - -\item [$\isarkeyword{print_options}$] prints the available - configuration options, with names, types, and current values. - -\item [$option~name = value$] modifies the named option, with the - syntax of the value depending on the option's type. For $bool$ the - default value is $true$. Any attempt to change a global option - locally is ignored. + +\item [$\isarkeyword{print_configs}$] prints the available configuration + options, with names, types, and current values. + +\item [$name = value$] as an attribute expression modifies the named option, + with the syntax of the value depending on the option's type. For $bool$ the + default value is $true$. Any attempt to change a global option in a local + context is ignored. \end{descr} diff -r 952efb77cf91 -r 4ab3084e311c src/HOL/HoareParallel/Graph.thy --- a/src/HOL/HoareParallel/Graph.thy Wed Aug 01 16:50:16 2007 +0200 +++ b/src/HOL/HoareParallel/Graph.thy Wed Aug 01 16:55:37 2007 +0200 @@ -173,9 +173,9 @@ prefer 2 apply arith apply(drule_tac n = "Suc nata" in Compl_lemma) apply clarify - using [[option fast_arith_split_limit = 0]] + using [[fast_arith_split_limit = 0]] apply force - using [[option fast_arith_split_limit = 9]] + using [[fast_arith_split_limit = 9]] apply(drule leI) apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)") apply(erule_tac x = "m - (Suc nata)" in allE) diff -r 952efb77cf91 -r 4ab3084e311c src/HOL/MicroJava/Comp/CorrCompTp.thy --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Aug 01 16:50:16 2007 +0200 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Aug 01 16:55:37 2007 +0200 @@ -454,7 +454,7 @@ apply (simp add: max_of_list_def) apply (induct xs) apply simp -using [[option fast_arith_split_limit = 0]] +using [[fast_arith_split_limit = 0]] apply simp apply arith done diff -r 952efb77cf91 -r 4ab3084e311c src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Wed Aug 01 16:50:16 2007 +0200 +++ b/src/HOL/Nominal/nominal_package.ML Wed Aug 01 16:55:37 2007 +0200 @@ -880,10 +880,10 @@ (* prove distinctness theorems *) - val distinctness_limit = ConfigOption.get_thy thy8 DatatypeProp.distinctness_limit; - val thy8' = ConfigOption.put_thy DatatypeProp.distinctness_limit 1000 thy8; + val distinctness_limit = Config.get_thy thy8 DatatypeProp.distinctness_limit; + val thy8' = Config.put_thy DatatypeProp.distinctness_limit 1000 thy8; val distinct_props = DatatypeProp.make_distincts new_type_names descr' sorts' thy8'; - val thy8 = ConfigOption.put_thy DatatypeProp.distinctness_limit distinctness_limit thy8'; + val thy8 = Config.put_thy DatatypeProp.distinctness_limit distinctness_limit thy8'; val dist_rewrites = map (fn (rep_thms, dist_lemma) => dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0])) diff -r 952efb77cf91 -r 4ab3084e311c src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Wed Aug 01 16:50:16 2007 +0200 +++ b/src/Pure/Isar/attrib.ML Wed Aug 01 16:55:37 2007 +0200 @@ -26,6 +26,14 @@ (('c * 'att list) * ('d * 'att list) list) list val crude_closure: Proof.context -> src -> src val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory + val print_configs: Proof.context -> unit + val register_config: bstring -> Config.value Config.T -> theory -> theory + val config_bool: bstring -> bool -> bool Config.T * (theory -> theory) + val config_int: bstring -> int -> int Config.T * (theory -> theory) + val config_string: bstring -> string -> string Config.T * (theory -> theory) + val config_bool_global: bstring -> bool -> bool Config.T * (theory -> theory) + val config_int_global: bstring -> int -> int Config.T * (theory -> theory) + val config_string_global: bstring -> string -> string Config.T * (theory -> theory) val thm: Context.generic * Args.T list -> thm * (Context.generic * Args.T list) val thms: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list) val multi_thm: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list) @@ -46,7 +54,7 @@ (* theory data *) -structure AttributesData = TheoryDataFun +structure Attributes = TheoryDataFun ( type T = (((src -> attribute) * string) * stamp) NameSpace.table; val empty = NameSpace.empty_table; @@ -58,7 +66,7 @@ fun print_attributes thy = let - val attribs = AttributesData.get thy; + val attribs = Attributes.get thy; fun prt_attr (name, ((_, comment), _)) = Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; in @@ -69,10 +77,10 @@ (* name space *) -val intern = NameSpace.intern o #1 o AttributesData.get; +val intern = NameSpace.intern o #1 o Attributes.get; val intern_src = Args.map_name o intern; -val extern = NameSpace.extern o #1 o AttributesData.get o ProofContext.theory_of; +val extern = NameSpace.extern o #1 o Attributes.get o ProofContext.theory_of; (* pretty printing *) @@ -87,7 +95,7 @@ fun attribute_i thy = let - val attrs = #2 (AttributesData.get thy); + val attrs = #2 (Attributes.get thy); fun attr src = let val ((name, _), pos) = Args.dest_src src in (case Symtab.lookup attrs name of @@ -125,7 +133,7 @@ raw_attrs |> map (fn (name, att, comment) => (name, ((att, comment), stamp ()))); fun add attrs = NameSpace.extend_table (Sign.naming_of thy) new_attrs attrs handle Symtab.DUP dup => error ("Duplicate declaration of attributes " ^ quote dup); - in AttributesData.map add thy end; + in Attributes.map add thy end; @@ -188,39 +196,76 @@ -(** basic attributes **) +(** configuration options **) + +(* naming *) + +structure Configs = TheoryDataFun +(struct + type T = Config.value Config.T Symtab.table; + val empty = Symtab.empty; + val copy = I; + val extend = I; + fun merge _ = Symtab.merge (K true); +end); -(* configuration options *) +fun print_configs ctxt = + let + val thy = ProofContext.theory_of ctxt; + fun prt (name, config) = + let val value = Config.get ctxt config in + Pretty.block [Pretty.str (name ^ ": " ^ Config.print_type value ^ " ="), Pretty.brk 1, + Pretty.str (Config.print_value value)] + end; + val configs = NameSpace.extern_table (#1 (Attributes.get thy), Configs.get thy); + in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end; + + +(* concrete syntax *) local val equals = Args.$$$ "="; -fun scan_value (ConfigOption.Bool _) = - (equals -- Args.$$$ "false") >> K (ConfigOption.Bool false) || - (equals -- Args.$$$ "true") >> K (ConfigOption.Bool true) || - (Scan.succeed (ConfigOption.Bool true)) - | scan_value (ConfigOption.Int _) = (equals |-- Args.int) >> ConfigOption.Int - | scan_value (ConfigOption.String _) = (equals |-- Args.name) >> ConfigOption.String; +fun scan_value (Config.Bool _) = + equals -- Args.$$$ "false" >> K (Config.Bool false) || + equals -- Args.$$$ "true" >> K (Config.Bool true) || + Scan.succeed (Config.Bool true) + | scan_value (Config.Int _) = equals |-- Args.int >> Config.Int + | scan_value (Config.String _) = equals |-- Args.name >> Config.String; -fun scan_config thy = - (Args.name >> ConfigOption.the_option thy) :|-- (fn (config, config_type) => - scan_value config_type >> (fn value => - K (Thm.declaration_attribute (K (ConfigOption.put_generic config value))))); - -fun scan_att thy = - (Args.internal_attribute || - (Scan.ahead (scan_config thy --| Args.terminator) :|-- - (fn att => Args.named_attribute (K att)))); +fun scan_config thy config = + let val config_type = Config.get_thy thy config + in scan_value config_type >> (K o Thm.declaration_attribute o K o Config.put_generic config) end; in -fun option x = syntax (Scan.peek (fn context => - (scan_att (Context.theory_of context) >> Morphism.form) --| Scan.many Args.not_eof)) x; +fun register_config name config thy = + thy + |> add_attributes + [(name, syntax (Scan.lift (scan_config thy config) >> Morphism.form), "configuration option")] + |> Configs.map (Symtab.update (Sign.full_name thy name, config)); + +fun declare_config make coerce global name default = + let + val config_value = Config.declare global name (make default); + val config = coerce config_value; + in (config, register_config name config_value) end; + +val config_bool = declare_config Config.Bool Config.bool false; +val config_int = declare_config Config.Int Config.int false; +val config_string = declare_config Config.String Config.string false; + +val config_bool_global = declare_config Config.Bool Config.bool true; +val config_int_global = declare_config Config.Int Config.int true; +val config_string_global = declare_config Config.String Config.string true; end; + +(** basic attributes **) + (* tags *) fun tagged x = syntax (tag >> PureThy.tag) x; @@ -300,8 +345,7 @@ val _ = Context.add_setup (add_attributes - [("option", option, "named configuration option"), - ("tagged", tagged, "tagged theorem"), + [("tagged", tagged, "tagged theorem"), ("untagged", untagged, "untagged theorem"), ("kind", kind, "theorem kind"), ("COMP", COMP_att, "direct composition with rules (no lifting)"),