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