src/Pure/config.ML
author wenzelm
Fri Jul 27 16:31:14 2007 +0200 (2007-07-27)
changeset 24001 067d8e589c58
parent 23987 6d78feed74dd
child 24004 8c962a9be9f2
permissions -rw-r--r--
exported datatype value;
added the_config;
removed put_generic_src -- moved value parsing to attrib.ML;
tuned;
wenzelm@23987
     1
(*  Title:      Pure/config.ML
wenzelm@23987
     2
    ID:         $Id$
wenzelm@23987
     3
    Author:     Makarius
wenzelm@23987
     4
wenzelm@23987
     5
Configuration options as values within the local context.  Global
wenzelm@23987
     6
environment of named options, with type declaration.
wenzelm@23987
     7
*)
wenzelm@23987
     8
wenzelm@23987
     9
signature CONFIG =
wenzelm@23987
    10
sig
wenzelm@24001
    11
  datatype value = Bool of bool | Int of int | String of string
wenzelm@23987
    12
  type 'a T
wenzelm@23987
    13
  val get: Proof.context -> 'a T -> 'a
wenzelm@23987
    14
  val get_thy: theory -> 'a T -> 'a
wenzelm@23987
    15
  val get_generic: Context.generic -> 'a T -> 'a
wenzelm@23987
    16
  val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
wenzelm@23987
    17
  val map_thy: 'a T -> ('a -> 'a) -> theory -> theory
wenzelm@23987
    18
  val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
wenzelm@23987
    19
  val put: 'a T -> 'a -> Proof.context -> Proof.context
wenzelm@23987
    20
  val put_thy: 'a T -> 'a -> theory -> theory
wenzelm@23987
    21
  val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
wenzelm@23987
    22
  val print_configs: Proof.context -> unit
wenzelm@24001
    23
  val the_config: string -> value T * value
wenzelm@23987
    24
  val bool: string -> bool -> bool T
wenzelm@23987
    25
  val int: string -> int -> int T
wenzelm@23987
    26
  val string: string -> string -> string T
wenzelm@23987
    27
end;
wenzelm@23987
    28
wenzelm@23987
    29
structure Config: CONFIG =
wenzelm@23987
    30
struct
wenzelm@23987
    31
wenzelm@24001
    32
(* mixed values *)
wenzelm@24001
    33
wenzelm@24001
    34
datatype value =
wenzelm@24001
    35
  Bool of bool |
wenzelm@24001
    36
  Int of int |
wenzelm@24001
    37
  String of string;
wenzelm@24001
    38
wenzelm@24001
    39
fun print_value (Bool true) = "true"
wenzelm@24001
    40
  | print_value (Bool false) = "false"
wenzelm@24001
    41
  | print_value (Int i) = signed_string_of_int i
wenzelm@24001
    42
  | print_value (String s) = quote s;
wenzelm@24001
    43
wenzelm@24001
    44
fun print_type (Bool _) = "boolean"
wenzelm@24001
    45
  | print_type (Int _) = "integer"
wenzelm@24001
    46
  | print_type (String _) = "string";
wenzelm@24001
    47
wenzelm@24001
    48
structure ConfigData = GenericDataFun
wenzelm@24001
    49
(
wenzelm@24001
    50
  type T = value Inttab.table;
wenzelm@24001
    51
  val empty = Inttab.empty;
wenzelm@24001
    52
  val extend = I;
wenzelm@24001
    53
  fun merge _ = Inttab.merge (K true);
wenzelm@24001
    54
);
wenzelm@24001
    55
wenzelm@24001
    56
wenzelm@23987
    57
(* abstract configuration options *)
wenzelm@23987
    58
wenzelm@23987
    59
datatype 'a T = Config of
wenzelm@23987
    60
 {get_value: Context.generic -> 'a,
wenzelm@23987
    61
  map_value: ('a -> 'a) -> Context.generic -> Context.generic};
wenzelm@23987
    62
wenzelm@23987
    63
fun get_generic context (Config {get_value, ...}) = get_value context;
wenzelm@23987
    64
fun get_ctxt ctxt = get_generic (Context.Proof ctxt);
wenzelm@23987
    65
fun get_thy thy = get_generic (Context.Theory thy);
wenzelm@23987
    66
wenzelm@23987
    67
fun map_generic (Config {map_value, ...}) f context = map_value f context;
wenzelm@23987
    68
fun map_ctxt config f = Context.proof_map (map_generic config f);
wenzelm@23987
    69
fun map_thy config f = Context.theory_map (map_generic config f);
wenzelm@23987
    70
wenzelm@23987
    71
fun put_generic config value = map_generic config (K value);
wenzelm@23987
    72
fun put_ctxt config value = map_ctxt config (K value);
wenzelm@23987
    73
fun put_thy config value = map_thy config (K value);
wenzelm@23987
    74
wenzelm@23987
    75
wenzelm@23987
    76
(* global declarations *)
wenzelm@23987
    77
wenzelm@23987
    78
local val global_configs = ref (Symtab.empty: (value T * value) Symtab.table) in
wenzelm@23987
    79
wenzelm@24001
    80
fun print_configs ctxt =
wenzelm@24001
    81
  let
wenzelm@24001
    82
    fun prt (name, (config, default)) =
wenzelm@24001
    83
      Pretty.block [Pretty.str (name ^ ": " ^ print_type default ^ " ="), Pretty.brk 1,
wenzelm@24001
    84
        Pretty.str (print_value (get_ctxt ctxt config))];
wenzelm@24001
    85
    val configs = sort_wrt #1 (Symtab.dest (! global_configs));
wenzelm@24001
    86
  in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
wenzelm@24001
    87
wenzelm@24001
    88
fun the_config name =
wenzelm@24001
    89
  (case Symtab.lookup (! global_configs) name of SOME cfg => cfg
wenzelm@24001
    90
  | NONE => error ("Unknown configuration option " ^ quote name));
wenzelm@23987
    91
wenzelm@23987
    92
fun declare make dest name default =
wenzelm@23987
    93
  let
wenzelm@23987
    94
    val id = serial ();
wenzelm@23987
    95
wenzelm@23987
    96
    val default_value = make default;
wenzelm@23987
    97
    fun get_value context =
wenzelm@23987
    98
      the_default default_value (Inttab.lookup (ConfigData.get context) id);
wenzelm@23987
    99
    fun map_value f = ConfigData.map (Inttab.map_default (id, default_value) f);
wenzelm@23987
   100
    val config_value = Config {get_value = get_value, map_value = map_value};
wenzelm@23987
   101
wenzelm@23987
   102
    val _ = CRITICAL (fn () =>
wenzelm@23987
   103
     (if Symtab.defined (! global_configs) name
wenzelm@23987
   104
      then warning ("Hiding existing configuration option " ^ quote name) else ();
wenzelm@23987
   105
      change global_configs (Symtab.update (name, (config_value, default_value)))));
wenzelm@23987
   106
wenzelm@23987
   107
  in Config {get_value = dest o get_value, map_value = fn f => map_value (make o f o dest)} end;
wenzelm@23987
   108
wenzelm@23987
   109
end;
wenzelm@23987
   110
wenzelm@23987
   111
val bool = declare Bool (fn Bool b => b);
wenzelm@23987
   112
val int = declare Int (fn Int i => i);
wenzelm@23987
   113
val string = declare String (fn String s => s);
wenzelm@23987
   114
wenzelm@23987
   115
wenzelm@23987
   116
(*final declarations of this structure!*)
wenzelm@23987
   117
val get = get_ctxt;
wenzelm@23987
   118
val map = map_ctxt;
wenzelm@23987
   119
val put = put_ctxt;
wenzelm@23987
   120
wenzelm@23987
   121
end;