renamed config.ML to config_option.ML;
authorwenzelm
Fri Jul 27 21:55:17 2007 +0200 (2007-07-27)
changeset 240078f40e6fdb376
parent 24006 60ac90b795be
child 24008 63ff2445ce1e
renamed config.ML to config_option.ML;
src/Pure/IsaMakefile
src/Pure/ROOT.ML
src/Pure/config.ML
src/Pure/config_option.ML
     1.1 --- a/src/Pure/IsaMakefile	Fri Jul 27 20:11:49 2007 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Fri Jul 27 21:55:17 2007 +0200
     1.3 @@ -63,13 +63,13 @@
     1.4    Tools/codegen_package.ML Tools/codegen_serializer.ML Tools/codegen_thingol.ML	\
     1.5    Tools/invoke.ML Tools/nbe.ML Tools/nbe_codegen.ML Tools/nbe_eval.ML		\
     1.6    Tools/xml.ML Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML		\
     1.7 -  compress.ML config.ML conjunction.ML consts.ML context.ML context_position.ML \
     1.8 -  conv.ML defs.ML display.ML drule.ML envir.ML fact_index.ML goal.ML 		\
     1.9 -  install_pp.ML library.ML logic.ML meta_simplifier.ML more_thm.ML morphism.ML 	\
    1.10 -  name.ML net.ML old_goals.ML pattern.ML proofterm.ML pure_setup.ML pure_thy.ML \
    1.11 -  search.ML sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML 	\
    1.12 -  term.ML term_subst.ML theory.ML thm.ML type.ML type_infer.ML unify.ML 	\
    1.13 -  variable.ML
    1.14 +  compress.ML config_option.ML conjunction.ML consts.ML context.ML		\
    1.15 +  context_position.ML conv.ML defs.ML display.ML drule.ML envir.ML		\
    1.16 +  fact_index.ML goal.ML install_pp.ML library.ML logic.ML meta_simplifier.ML	\
    1.17 +  more_thm.ML morphism.ML name.ML net.ML old_goals.ML pattern.ML proofterm.ML	\
    1.18 +  pure_setup.ML pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML	\
    1.19 +  tactic.ML tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML		\
    1.20 +  type_infer.ML unify.ML variable.ML
    1.21  	@./mk
    1.22  
    1.23  
     2.1 --- a/src/Pure/ROOT.ML	Fri Jul 27 20:11:49 2007 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Fri Jul 27 21:55:17 2007 +0200
     2.3 @@ -41,7 +41,7 @@
     2.4  use "Syntax/printer.ML";
     2.5  use "Syntax/syntax.ML";
     2.6  
     2.7 -use "config.ML";
     2.8 +use "config_option.ML";
     2.9  use "General/ml_syntax.ML";
    2.10  
    2.11  (*core of tactical proof system*)
     3.1 --- a/src/Pure/config.ML	Fri Jul 27 20:11:49 2007 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,134 +0,0 @@
     3.4 -(*  Title:      Pure/config.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Makarius
     3.7 -
     3.8 -Configuration options as values within the local context.  Global
     3.9 -environment of named options, with type declaration.
    3.10 -*)
    3.11 -
    3.12 -signature CONFIG =
    3.13 -sig
    3.14 -  datatype value = Bool of bool | Int of int | String of string
    3.15 -  type 'a T
    3.16 -  val get: Proof.context -> 'a T -> 'a
    3.17 -  val get_thy: theory -> 'a T -> 'a
    3.18 -  val get_generic: Context.generic -> 'a T -> 'a
    3.19 -  val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
    3.20 -  val map_thy: 'a T -> ('a -> 'a) -> theory -> theory
    3.21 -  val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
    3.22 -  val put: 'a T -> 'a -> Proof.context -> Proof.context
    3.23 -  val put_thy: 'a T -> 'a -> theory -> theory
    3.24 -  val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
    3.25 -  val print_configs: Proof.context -> unit
    3.26 -  val the_config: string -> value T * value
    3.27 -  val bool: string -> bool -> bool T
    3.28 -  val int: string -> int -> int T
    3.29 -  val string: string -> string -> string T
    3.30 -end;
    3.31 -
    3.32 -structure Config: CONFIG =
    3.33 -struct
    3.34 -
    3.35 -(* mixed values *)
    3.36 -
    3.37 -datatype value =
    3.38 -  Bool of bool |
    3.39 -  Int of int |
    3.40 -  String of string;
    3.41 -
    3.42 -fun print_value (Bool true) = "true"
    3.43 -  | print_value (Bool false) = "false"
    3.44 -  | print_value (Int i) = signed_string_of_int i
    3.45 -  | print_value (String s) = quote s;
    3.46 -
    3.47 -fun print_type (Bool _) = "boolean"
    3.48 -  | print_type (Int _) = "integer"
    3.49 -  | print_type (String _) = "string";
    3.50 -
    3.51 -fun same_type (Bool _) (Bool _) = true
    3.52 -  | same_type (Int _) (Int _) = true
    3.53 -  | same_type (String _) (String _) = true
    3.54 -  | same_type _ _ = false;
    3.55 -
    3.56 -fun type_check f value =
    3.57 -  let
    3.58 -    val value' = f value;
    3.59 -    val _ = same_type value value' orelse
    3.60 -      error ("Ill-typed configuration option: " ^ print_type value ^
    3.61 -        " expected,\nbut " ^ print_type value' ^ " was found");
    3.62 -  in value' end;
    3.63 -
    3.64 -structure ConfigData = GenericDataFun
    3.65 -(
    3.66 -  type T = value Inttab.table;
    3.67 -  val empty = Inttab.empty;
    3.68 -  val extend = I;
    3.69 -  fun merge _ = Inttab.merge (K true);
    3.70 -);
    3.71 -
    3.72 -
    3.73 -(* abstract configuration options *)
    3.74 -
    3.75 -datatype 'a T = Config of
    3.76 - {get_value: Context.generic -> 'a,
    3.77 -  map_value: ('a -> 'a) -> Context.generic -> Context.generic};
    3.78 -
    3.79 -fun get_generic context (Config {get_value, ...}) = get_value context;
    3.80 -fun get_ctxt ctxt = get_generic (Context.Proof ctxt);
    3.81 -fun get_thy thy = get_generic (Context.Theory thy);
    3.82 -
    3.83 -fun map_generic (Config {map_value, ...}) f context = map_value f context;
    3.84 -fun map_ctxt config f = Context.proof_map (map_generic config f);
    3.85 -fun map_thy config f = Context.theory_map (map_generic config f);
    3.86 -
    3.87 -fun put_generic config value = map_generic config (K value);
    3.88 -fun put_ctxt config value = map_ctxt config (K value);
    3.89 -fun put_thy config value = map_thy config (K value);
    3.90 -
    3.91 -
    3.92 -(* global declarations *)
    3.93 -
    3.94 -local val global_configs = ref (Symtab.empty: (value T * value) Symtab.table) in
    3.95 -
    3.96 -fun print_configs ctxt =
    3.97 -  let
    3.98 -    fun prt (name, (config, default)) =
    3.99 -      Pretty.block [Pretty.str (name ^ ": " ^ print_type default ^ " ="), Pretty.brk 1,
   3.100 -        Pretty.str (print_value (get_ctxt ctxt config))];
   3.101 -    val configs = sort_wrt #1 (Symtab.dest (! global_configs));
   3.102 -  in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
   3.103 -
   3.104 -fun the_config name =
   3.105 -  (case Symtab.lookup (! global_configs) name of SOME cfg => cfg
   3.106 -  | NONE => error ("Unknown configuration option " ^ quote name));
   3.107 -
   3.108 -fun declare make dest name default =
   3.109 -  let
   3.110 -    val id = serial ();
   3.111 -
   3.112 -    val default_value = make default;
   3.113 -    fun get_value context =
   3.114 -      the_default default_value (Inttab.lookup (ConfigData.get context) id);
   3.115 -    fun map_value f = ConfigData.map (Inttab.map_default (id, default_value) (type_check f));
   3.116 -    val config_value = Config {get_value = get_value, map_value = map_value};
   3.117 -
   3.118 -    val _ = CRITICAL (fn () =>
   3.119 -     (if Symtab.defined (! global_configs) name
   3.120 -      then warning ("Hiding existing configuration option " ^ quote name) else ();
   3.121 -      change global_configs (Symtab.update (name, (config_value, default_value)))));
   3.122 -
   3.123 -  in Config {get_value = dest o get_value, map_value = fn f => map_value (make o f o dest)} end;
   3.124 -
   3.125 -end;
   3.126 -
   3.127 -val bool = declare Bool (fn Bool b => b);
   3.128 -val int = declare Int (fn Int i => i);
   3.129 -val string = declare String (fn String s => s);
   3.130 -
   3.131 -
   3.132 -(*final declarations of this structure!*)
   3.133 -val get = get_ctxt;
   3.134 -val map = map_ctxt;
   3.135 -val put = put_ctxt;
   3.136 -
   3.137 -end;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/config_option.ML	Fri Jul 27 21:55:17 2007 +0200
     4.3 @@ -0,0 +1,136 @@
     4.4 +(*  Title:      Pure/config_option.ML
     4.5 +    ID:         $Id$
     4.6 +    Author:     Makarius
     4.7 +
     4.8 +Configuration options as values within the local context.  Global
     4.9 +environment of named options, with type declaration.
    4.10 +*)
    4.11 +
    4.12 +signature CONFIG_OPTION =
    4.13 +sig
    4.14 +  datatype value = Bool of bool | Int of int | String of string
    4.15 +  type 'a T
    4.16 +  val get: Proof.context -> 'a T -> 'a
    4.17 +  val get_thy: theory -> 'a T -> 'a
    4.18 +  val get_generic: Context.generic -> 'a T -> 'a
    4.19 +  val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
    4.20 +  val map_thy: 'a T -> ('a -> 'a) -> theory -> theory
    4.21 +  val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
    4.22 +  val put: 'a T -> 'a -> Proof.context -> Proof.context
    4.23 +  val put_thy: 'a T -> 'a -> theory -> theory
    4.24 +  val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
    4.25 +  val print_options: Proof.context -> unit
    4.26 +  val the_option: string -> value T * value
    4.27 +  val bool: string -> bool -> bool T
    4.28 +  val int: string -> int -> int T
    4.29 +  val string: string -> string -> string T
    4.30 +end;
    4.31 +
    4.32 +structure ConfigOption: CONFIG_OPTION =
    4.33 +struct
    4.34 +
    4.35 +(* mixed values *)
    4.36 +
    4.37 +datatype value =
    4.38 +  Bool of bool |
    4.39 +  Int of int |
    4.40 +  String of string;
    4.41 +
    4.42 +fun print_value (Bool true) = "true"
    4.43 +  | print_value (Bool false) = "false"
    4.44 +  | print_value (Int i) = signed_string_of_int i
    4.45 +  | print_value (String s) = quote s;
    4.46 +
    4.47 +fun print_type (Bool _) = "boolean"
    4.48 +  | print_type (Int _) = "integer"
    4.49 +  | print_type (String _) = "string";
    4.50 +
    4.51 +fun same_type (Bool _) (Bool _) = true
    4.52 +  | same_type (Int _) (Int _) = true
    4.53 +  | same_type (String _) (String _) = true
    4.54 +  | same_type _ _ = false;
    4.55 +
    4.56 +fun type_check f value =
    4.57 +  let
    4.58 +    val value' = f value;
    4.59 +    val _ = same_type value value' orelse
    4.60 +      error ("Ill-typed configuration option: " ^ print_type value ^
    4.61 +        " expected,\nbut " ^ print_type value' ^ " was found");
    4.62 +  in value' end;
    4.63 +
    4.64 +structure ConfigOptionData = GenericDataFun
    4.65 +(
    4.66 +  type T = value Inttab.table;
    4.67 +  val empty = Inttab.empty;
    4.68 +  val extend = I;
    4.69 +  fun merge _ = Inttab.merge (K true);
    4.70 +);
    4.71 +
    4.72 +
    4.73 +(* abstract configuration options *)
    4.74 +
    4.75 +datatype 'a T = ConfigOption of
    4.76 + {get_value: Context.generic -> 'a,
    4.77 +  map_value: ('a -> 'a) -> Context.generic -> Context.generic};
    4.78 +
    4.79 +fun get_generic context (ConfigOption {get_value, ...}) = get_value context;
    4.80 +fun get_ctxt ctxt = get_generic (Context.Proof ctxt);
    4.81 +fun get_thy thy = get_generic (Context.Theory thy);
    4.82 +
    4.83 +fun map_generic (ConfigOption {map_value, ...}) f context = map_value f context;
    4.84 +fun map_ctxt config f = Context.proof_map (map_generic config f);
    4.85 +fun map_thy config f = Context.theory_map (map_generic config f);
    4.86 +
    4.87 +fun put_generic config value = map_generic config (K value);
    4.88 +fun put_ctxt config value = map_ctxt config (K value);
    4.89 +fun put_thy config value = map_thy config (K value);
    4.90 +
    4.91 +
    4.92 +(* global declarations *)
    4.93 +
    4.94 +local val global_configs = ref (Symtab.empty: (value T * value) Symtab.table) in
    4.95 +
    4.96 +fun print_options ctxt =
    4.97 +  let
    4.98 +    fun prt (name, (config, default)) =
    4.99 +      Pretty.block [Pretty.str (name ^ ": " ^ print_type default ^ " ="), Pretty.brk 1,
   4.100 +        Pretty.str (print_value (get_ctxt ctxt config))];
   4.101 +    val configs = sort_wrt #1 (Symtab.dest (! global_configs));
   4.102 +  in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
   4.103 +
   4.104 +fun the_option name =
   4.105 +  (case Symtab.lookup (! global_configs) name of SOME cfg => cfg
   4.106 +  | NONE => error ("Unknown configuration option " ^ quote name));
   4.107 +
   4.108 +fun declare make dest name default =
   4.109 +  let
   4.110 +    val id = serial ();
   4.111 +
   4.112 +    val default_value = make default;
   4.113 +    fun get_value context =
   4.114 +      the_default default_value (Inttab.lookup (ConfigOptionData.get context) id);
   4.115 +    fun map_value f = ConfigOptionData.map (Inttab.map_default (id, default_value) (type_check f));
   4.116 +    val config_value = ConfigOption {get_value = get_value, map_value = map_value};
   4.117 +
   4.118 +    val _ = CRITICAL (fn () =>
   4.119 +     (if Symtab.defined (! global_configs) name
   4.120 +      then warning ("Hiding existing configuration option " ^ quote name) else ();
   4.121 +      change global_configs (Symtab.update (name, (config_value, default_value)))));
   4.122 +
   4.123 +  in
   4.124 +    ConfigOption {get_value = dest o get_value, map_value = fn f => map_value (make o f o dest)}
   4.125 +  end;
   4.126 +
   4.127 +end;
   4.128 +
   4.129 +val bool = declare Bool (fn Bool b => b);
   4.130 +val int = declare Int (fn Int i => i);
   4.131 +val string = declare String (fn String s => s);
   4.132 +
   4.133 +
   4.134 +(*final declarations of this structure!*)
   4.135 +val get = get_ctxt;
   4.136 +val map = map_ctxt;
   4.137 +val put = put_ctxt;
   4.138 +
   4.139 +end;