support for real valued configuration options;
authorwenzelm
Sat Oct 30 16:33:58 2010 +0200 (2010-10-30)
changeset 40291012ed4426fda
parent 40290 47f572aff50a
child 40292 ba13793594f0
child 40328 ae8d187600e7
support for real valued configuration options;
NEWS
doc-src/IsarImplementation/Thy/Prelim.thy
doc-src/IsarImplementation/Thy/document/Prelim.tex
doc-src/IsarRef/Thy/Generic.thy
doc-src/IsarRef/Thy/Outer_Syntax.thy
doc-src/IsarRef/Thy/document/Generic.tex
doc-src/IsarRef/Thy/document/Outer_Syntax.tex
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/config.ML
src/Pure/library.ML
     1.1 --- a/NEWS	Sat Oct 30 15:26:40 2010 +0200
     1.2 +++ b/NEWS	Sat Oct 30 16:33:58 2010 +0200
     1.3 @@ -56,6 +56,10 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* Support for real valued configuration options, using simplistic
     1.8 +floating-point notation that coincides with the inner syntax for
     1.9 +float_token.
    1.10 +
    1.11  * Interpretation command 'interpret' accepts a list of equations like
    1.12  'interpretation' does.
    1.13  
     2.1 --- a/doc-src/IsarImplementation/Thy/Prelim.thy	Sat Oct 30 15:26:40 2010 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Sat Oct 30 16:33:58 2010 +0200
     2.3 @@ -597,6 +597,8 @@
     2.4    bool Config.T * (theory -> theory)"} \\
     2.5    @{index_ML Attrib.config_int: "string -> (Context.generic -> int) ->
     2.6    int Config.T * (theory -> theory)"} \\
     2.7 +  @{index_ML Attrib.config_real: "string -> (Context.generic -> real) ->
     2.8 +  real Config.T * (theory -> theory)"} \\
     2.9    @{index_ML Attrib.config_string: "string -> (Context.generic -> string) ->
    2.10    string Config.T * (theory -> theory)"} \\
    2.11    \end{mldecls}
    2.12 @@ -617,9 +619,9 @@
    2.13    needs to be applied to the theory initially, in order to make
    2.14    concrete declaration syntax available to the user.
    2.15  
    2.16 -  \item @{ML Attrib.config_int} and @{ML Attrib.config_string} work
    2.17 -  like @{ML Attrib.config_bool}, but for types @{ML_type int} and
    2.18 -  @{ML_type string}, respectively.
    2.19 +  \item @{ML Attrib.config_int}, @{ML Attrib.config_real}, and @{ML
    2.20 +  Attrib.config_string} work like @{ML Attrib.config_bool}, but for
    2.21 +  types @{ML_type int} and @{ML_type string}, respectively.
    2.22  
    2.23    \end{description}
    2.24  *}
    2.25 @@ -652,6 +654,17 @@
    2.26    ML_val {* @{assert} (Config.get @{context} my_flag = true) *}
    2.27  qed
    2.28  
    2.29 +text {* Here is another example involving ML type @{ML_type real}
    2.30 +  (floating-point numbers). *}
    2.31 +
    2.32 +ML {*
    2.33 +  val (airspeed_velocity, airspeed_velocity_setup) =
    2.34 +    Attrib.config_real "airspeed_velocity" (K 0.0)
    2.35 +*}
    2.36 +setup airspeed_velocity_setup
    2.37 +
    2.38 +declare [[airspeed_velocity = 9.9]]
    2.39 +
    2.40  
    2.41  section {* Names \label{sec:names} *}
    2.42  
     3.1 --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sat Oct 30 15:26:40 2010 +0200
     3.2 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sat Oct 30 16:33:58 2010 +0200
     3.3 @@ -794,6 +794,8 @@
     3.4  \verb|  bool Config.T * (theory -> theory)| \\
     3.5    \indexdef{}{ML}{Attrib.config\_int}\verb|Attrib.config_int: string -> (Context.generic -> int) ->|\isasep\isanewline%
     3.6  \verb|  int Config.T * (theory -> theory)| \\
     3.7 +  \indexdef{}{ML}{Attrib.config\_real}\verb|Attrib.config_real: string -> (Context.generic -> real) ->|\isasep\isanewline%
     3.8 +\verb|  real Config.T * (theory -> theory)| \\
     3.9    \indexdef{}{ML}{Attrib.config\_string}\verb|Attrib.config_string: string -> (Context.generic -> string) ->|\isasep\isanewline%
    3.10  \verb|  string Config.T * (theory -> theory)| \\
    3.11    \end{mldecls}
    3.12 @@ -813,9 +815,8 @@
    3.13    needs to be applied to the theory initially, in order to make
    3.14    concrete declaration syntax available to the user.
    3.15  
    3.16 -  \item \verb|Attrib.config_int| and \verb|Attrib.config_string| work
    3.17 -  like \verb|Attrib.config_bool|, but for types \verb|int| and
    3.18 -  \verb|string|, respectively.
    3.19 +  \item \verb|Attrib.config_int|, \verb|Attrib.config_real|, and \verb|Attrib.config_string| work like \verb|Attrib.config_bool|, but for
    3.20 +  types \verb|int| and \verb|string|, respectively.
    3.21  
    3.22    \end{description}%
    3.23  \end{isamarkuptext}%
    3.24 @@ -1019,6 +1020,34 @@
    3.25  %
    3.26  \endisadelimproof
    3.27  %
    3.28 +\begin{isamarkuptext}%
    3.29 +Here is another example involving ML type \verb|real|
    3.30 +  (floating-point numbers).%
    3.31 +\end{isamarkuptext}%
    3.32 +\isamarkuptrue%
    3.33 +%
    3.34 +\isadelimML
    3.35 +%
    3.36 +\endisadelimML
    3.37 +%
    3.38 +\isatagML
    3.39 +\isacommand{ML}\isamarkupfalse%
    3.40 +\ {\isacharverbatimopen}\isanewline
    3.41 +\ \ val\ {\isacharparenleft}airspeed{\isacharunderscore}velocity{\isacharcomma}\ airspeed{\isacharunderscore}velocity{\isacharunderscore}setup{\isacharparenright}\ {\isacharequal}\isanewline
    3.42 +\ \ \ \ Attrib{\isachardot}config{\isacharunderscore}real\ {\isachardoublequote}airspeed{\isacharunderscore}velocity{\isachardoublequote}\ {\isacharparenleft}K\ {\isadigit{0}}{\isachardot}{\isadigit{0}}{\isacharparenright}\isanewline
    3.43 +{\isacharverbatimclose}\isanewline
    3.44 +\isacommand{setup}\isamarkupfalse%
    3.45 +\ airspeed{\isacharunderscore}velocity{\isacharunderscore}setup%
    3.46 +\endisatagML
    3.47 +{\isafoldML}%
    3.48 +%
    3.49 +\isadelimML
    3.50 +%
    3.51 +\endisadelimML
    3.52 +\isanewline
    3.53 +\isanewline
    3.54 +\isacommand{declare}\isamarkupfalse%
    3.55 +\ {\isacharbrackleft}{\isacharbrackleft}airspeed{\isacharunderscore}velocity\ {\isacharequal}\ {\isadigit{9}}{\isachardot}{\isadigit{9}}{\isacharbrackright}{\isacharbrackright}%
    3.56  \isamarkupsection{Names \label{sec:names}%
    3.57  }
    3.58  \isamarkuptrue%
     4.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Sat Oct 30 15:26:40 2010 +0200
     4.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Sat Oct 30 16:33:58 2010 +0200
     4.3 @@ -6,16 +6,15 @@
     4.4  
     4.5  section {* Configuration options *}
     4.6  
     4.7 -text {*
     4.8 -  Isabelle/Pure maintains a record of named configuration options
     4.9 -  within the theory or proof context, with values of type @{ML_type
    4.10 -  bool}, @{ML_type int}, or @{ML_type string}.  Tools may declare
    4.11 -  options in ML, and then refer to these values (relative to the
    4.12 -  context).  Thus global reference variables are easily avoided.  The
    4.13 -  user may change the value of a configuration option by means of an
    4.14 -  associated attribute of the same name.  This form of context
    4.15 -  declaration works particularly well with commands such as @{command
    4.16 -  "declare"} or @{command "using"}.
    4.17 +text {* Isabelle/Pure maintains a record of named configuration
    4.18 +  options within the theory or proof context, with values of type
    4.19 +  @{ML_type bool}, @{ML_type int}, @{ML_type real}, or @{ML_type
    4.20 +  string}.  Tools may declare options in ML, and then refer to these
    4.21 +  values (relative to the context).  Thus global reference variables
    4.22 +  are easily avoided.  The user may change the value of a
    4.23 +  configuration option by means of an associated attribute of the same
    4.24 +  name.  This form of context declaration works particularly well with
    4.25 +  commands such as @{command "declare"} or @{command "using"}.
    4.26  
    4.27    For historical reasons, some tools cannot take the full proof
    4.28    context into account and merely refer to the background theory.
    4.29 @@ -27,7 +26,7 @@
    4.30    \end{matharray}
    4.31  
    4.32    \begin{rail}
    4.33 -    name ('=' ('true' | 'false' | int | name))?
    4.34 +    name ('=' ('true' | 'false' | int | float | name))?
    4.35    \end{rail}
    4.36  
    4.37    \begin{description}
     5.1 --- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Sat Oct 30 15:26:40 2010 +0200
     5.2 +++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Sat Oct 30 16:33:58 2010 +0200
     5.3 @@ -366,7 +366,7 @@
     5.4  
     5.5    \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
     5.6    \begin{rail}
     5.7 -    atom: nameref | typefree | typevar | var | nat | keyword
     5.8 +    atom: nameref | typefree | typevar | var | nat | float | keyword
     5.9      ;
    5.10      arg: atom | '(' args ')' | '[' args ']'
    5.11      ;
     6.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Sat Oct 30 15:26:40 2010 +0200
     6.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Sat Oct 30 16:33:58 2010 +0200
     6.3 @@ -27,13 +27,14 @@
     6.4  \isamarkuptrue%
     6.5  %
     6.6  \begin{isamarkuptext}%
     6.7 -Isabelle/Pure maintains a record of named configuration options
     6.8 -  within the theory or proof context, with values of type \verb|bool|, \verb|int|, or \verb|string|.  Tools may declare
     6.9 -  options in ML, and then refer to these values (relative to the
    6.10 -  context).  Thus global reference variables are easily avoided.  The
    6.11 -  user may change the value of a configuration option by means of an
    6.12 -  associated attribute of the same name.  This form of context
    6.13 -  declaration works particularly well with commands such as \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} or \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}.
    6.14 +Isabelle/Pure maintains a record of named configuration
    6.15 +  options within the theory or proof context, with values of type
    6.16 +  \verb|bool|, \verb|int|, \verb|real|, or \verb|string|.  Tools may declare options in ML, and then refer to these
    6.17 +  values (relative to the context).  Thus global reference variables
    6.18 +  are easily avoided.  The user may change the value of a
    6.19 +  configuration option by means of an associated attribute of the same
    6.20 +  name.  This form of context declaration works particularly well with
    6.21 +  commands such as \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} or \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}.
    6.22  
    6.23    For historical reasons, some tools cannot take the full proof
    6.24    context into account and merely refer to the background theory.
    6.25 @@ -45,7 +46,7 @@
    6.26    \end{matharray}
    6.27  
    6.28    \begin{rail}
    6.29 -    name ('=' ('true' | 'false' | int | name))?
    6.30 +    name ('=' ('true' | 'false' | int | float | name))?
    6.31    \end{rail}
    6.32  
    6.33    \begin{description}
     7.1 --- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Sat Oct 30 15:26:40 2010 +0200
     7.2 +++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Sat Oct 30 16:33:58 2010 +0200
     7.3 @@ -392,7 +392,7 @@
     7.4  
     7.5    \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
     7.6    \begin{rail}
     7.7 -    atom: nameref | typefree | typevar | var | nat | keyword
     7.8 +    atom: nameref | typefree | typevar | var | nat | float | keyword
     7.9      ;
    7.10      arg: atom | '(' args ')' | '[' args ']'
    7.11      ;
     8.1 --- a/src/Pure/Isar/args.ML	Sat Oct 30 15:26:40 2010 +0200
     8.2 +++ b/src/Pure/Isar/args.ML	Sat Oct 30 16:33:58 2010 +0200
     8.3 @@ -224,7 +224,7 @@
     8.4    let
     8.5      val keyword_symid = token (Parse.keyword_with is_symid);
     8.6      fun atom blk = Parse.group "argument"
     8.7 -      (ident || keyword_symid || string || alt_string ||
     8.8 +      (ident || keyword_symid || string || alt_string || token Parse.float_number ||
     8.9          (if blk then token (Parse.$$$ ",") else Scan.fail));
    8.10  
    8.11      fun args blk x = Scan.optional (args1 blk) [] x
     9.1 --- a/src/Pure/Isar/attrib.ML	Sat Oct 30 15:26:40 2010 +0200
     9.2 +++ b/src/Pure/Isar/attrib.ML	Sat Oct 30 16:33:58 2010 +0200
     9.3 @@ -38,10 +38,13 @@
     9.4    val internal: (morphism -> attribute) -> src
     9.5    val config_bool: bstring -> (Context.generic -> bool) -> bool Config.T * (theory -> theory)
     9.6    val config_int: bstring -> (Context.generic -> int) -> int Config.T * (theory -> theory)
     9.7 +  val config_real: bstring -> (Context.generic -> real) -> real Config.T * (theory -> theory)
     9.8    val config_string: bstring -> (Context.generic -> string) -> string Config.T * (theory -> theory)
     9.9    val config_bool_global: bstring -> (Context.generic -> bool) -> bool Config.T * (theory -> theory)
    9.10    val config_int_global: bstring -> (Context.generic -> int) -> int Config.T * (theory -> theory)
    9.11 -  val config_string_global: bstring -> (Context.generic -> string) -> string Config.T * (theory -> theory)
    9.12 +  val config_real_global: bstring -> (Context.generic -> real) -> real Config.T * (theory -> theory)
    9.13 +  val config_string_global:
    9.14 +    bstring -> (Context.generic -> string) -> string Config.T * (theory -> theory)
    9.15  end;
    9.16  
    9.17  structure Attrib: ATTRIB =
    9.18 @@ -353,6 +356,7 @@
    9.19        equals -- Args.$$$ "true" >> K (Config.Bool true) ||
    9.20        Scan.succeed (Config.Bool true)
    9.21    | scan_value (Config.Int _) = equals |-- Parse.int >> Config.Int
    9.22 +  | scan_value (Config.Real _) = equals |-- Parse.real >> Config.Real
    9.23    | scan_value (Config.String _) = equals |-- Args.name >> Config.String;
    9.24  
    9.25  fun scan_config thy config =
    9.26 @@ -380,10 +384,12 @@
    9.27  
    9.28  val config_bool   = declare_config Config.Bool Config.bool false;
    9.29  val config_int    = declare_config Config.Int Config.int false;
    9.30 +val config_real   = declare_config Config.Real Config.real false;
    9.31  val config_string = declare_config Config.String Config.string false;
    9.32  
    9.33  val config_bool_global   = declare_config Config.Bool Config.bool true;
    9.34  val config_int_global    = declare_config Config.Int Config.int true;
    9.35 +val config_real_global   = declare_config Config.Real Config.real true;
    9.36  val config_string_global = declare_config Config.String Config.string true;
    9.37  
    9.38  end;
    10.1 --- a/src/Pure/config.ML	Sat Oct 30 15:26:40 2010 +0200
    10.2 +++ b/src/Pure/config.ML	Sat Oct 30 16:33:58 2010 +0200
    10.3 @@ -6,13 +6,14 @@
    10.4  
    10.5  signature CONFIG =
    10.6  sig
    10.7 -  datatype value = Bool of bool | Int of int | String of string
    10.8 +  datatype value = Bool of bool | Int of int | Real of real | String of string
    10.9    val print_value: value -> string
   10.10    val print_type: value -> string
   10.11    type 'a T
   10.12    type raw = value T
   10.13    val bool: raw -> bool T
   10.14    val int: raw -> int T
   10.15 +  val real: raw -> real T
   10.16    val string: raw -> string T
   10.17    val get: Proof.context -> 'a T -> 'a
   10.18    val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
   10.19 @@ -37,19 +38,23 @@
   10.20  datatype value =
   10.21    Bool of bool |
   10.22    Int of int |
   10.23 +  Real of real |
   10.24    String of string;
   10.25  
   10.26  fun print_value (Bool true) = "true"
   10.27    | print_value (Bool false) = "false"
   10.28    | print_value (Int i) = signed_string_of_int i
   10.29 +  | print_value (Real x) = signed_string_of_real x
   10.30    | print_value (String s) = quote s;
   10.31  
   10.32  fun print_type (Bool _) = "bool"
   10.33    | print_type (Int _) = "int"
   10.34 +  | print_type (Real _) = "real"
   10.35    | print_type (String _) = "string";
   10.36  
   10.37  fun same_type (Bool _) (Bool _) = true
   10.38    | same_type (Int _) (Int _) = true
   10.39 +  | same_type (Real _) (Real _) = true
   10.40    | same_type (String _) (String _) = true
   10.41    | same_type _ _ = false;
   10.42  
   10.43 @@ -78,6 +83,7 @@
   10.44  
   10.45  val bool = coerce Bool (fn Bool b => b);
   10.46  val int = coerce Int (fn Int i => i);
   10.47 +val real = coerce Real (fn Real x => x);
   10.48  val string = coerce String (fn String s => s);
   10.49  
   10.50  fun get_generic context (Config {get_value, ...}) = get_value context;
   10.51 @@ -118,7 +124,8 @@
   10.52      fun map_value f (context as Context.Proof _) =
   10.53            let val context' = update_value f context in
   10.54              if global andalso
   10.55 -              get_value (Context.Theory (Context.theory_of context')) <> get_value context'
   10.56 +              print_value (get_value (Context.Theory (Context.theory_of context'))) <>
   10.57 +                print_value (get_value context')
   10.58              then (warning ("Ignoring local change of global option " ^ quote name); context)
   10.59              else context'
   10.60            end
    11.1 --- a/src/Pure/library.ML	Sat Oct 30 15:26:40 2010 +0200
    11.2 +++ b/src/Pure/library.ML	Sat Oct 30 16:33:58 2010 +0200
    11.3 @@ -130,6 +130,10 @@
    11.4    val read_int: string list -> int * string list
    11.5    val oct_char: string -> string
    11.6  
    11.7 +  (*reals*)
    11.8 +  val string_of_real: real -> string
    11.9 +  val signed_string_of_real: real -> string
   11.10 +
   11.11    (*strings*)
   11.12    val nth_string: string -> int -> string
   11.13    val fold_string: (string -> 'a -> 'a) -> string -> 'a -> 'a
   11.14 @@ -668,6 +672,15 @@
   11.15  
   11.16  
   11.17  
   11.18 +(** reals **)
   11.19 +
   11.20 +val string_of_real = Real.fmt (StringCvt.GEN NONE);
   11.21 +
   11.22 +fun signed_string_of_real x =
   11.23 +  if x < 0.0 then "-" ^ string_of_real (~ x) else string_of_real x;
   11.24 +
   11.25 +
   11.26 +
   11.27  (** strings **)
   11.28  
   11.29  (* functions tuned for strings, avoiding explode *)