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