src/Pure/config.ML
changeset 23987 6d78feed74dd
child 24001 067d8e589c58
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/config.ML	Wed Jul 25 22:20:49 2007 +0200
     1.3 @@ -0,0 +1,130 @@
     1.4 +(*  Title:      Pure/config.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Configuration options as values within the local context.  Global
     1.9 +environment of named options, with type declaration.
    1.10 +*)
    1.11 +
    1.12 +signature CONFIG =
    1.13 +sig
    1.14 +  type 'a T
    1.15 +  val get: Proof.context -> 'a T -> 'a
    1.16 +  val get_thy: theory -> 'a T -> 'a
    1.17 +  val get_generic: Context.generic -> 'a T -> 'a
    1.18 +  val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
    1.19 +  val map_thy: 'a T -> ('a -> 'a) -> theory -> theory
    1.20 +  val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
    1.21 +  val put: 'a T -> 'a -> Proof.context -> Proof.context
    1.22 +  val put_thy: 'a T -> 'a -> theory -> theory
    1.23 +  val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
    1.24 +  val put_generic_src: string -> string -> Context.generic -> Context.generic
    1.25 +  val print_configs: Proof.context -> unit
    1.26 +  val bool: string -> bool -> bool T
    1.27 +  val int: string -> int -> int T
    1.28 +  val string: string -> string -> string T
    1.29 +end;
    1.30 +
    1.31 +structure Config: CONFIG =
    1.32 +struct
    1.33 +
    1.34 +(* abstract configuration options *)
    1.35 +
    1.36 +datatype 'a T = Config of
    1.37 + {get_value: Context.generic -> 'a,
    1.38 +  map_value: ('a -> 'a) -> Context.generic -> Context.generic};
    1.39 +
    1.40 +fun get_generic context (Config {get_value, ...}) = get_value context;
    1.41 +fun get_ctxt ctxt = get_generic (Context.Proof ctxt);
    1.42 +fun get_thy thy = get_generic (Context.Theory thy);
    1.43 +
    1.44 +fun map_generic (Config {map_value, ...}) f context = map_value f context;
    1.45 +fun map_ctxt config f = Context.proof_map (map_generic config f);
    1.46 +fun map_thy config f = Context.theory_map (map_generic config f);
    1.47 +
    1.48 +fun put_generic config value = map_generic config (K value);
    1.49 +fun put_ctxt config value = map_ctxt config (K value);
    1.50 +fun put_thy config value = map_thy config (K value);
    1.51 +
    1.52 +
    1.53 +(* mixed values *)
    1.54 +
    1.55 +datatype value =
    1.56 +  Bool of bool |
    1.57 +  Int of int |
    1.58 +  String of string;
    1.59 +
    1.60 +fun read_value (Bool _) "true" = SOME (Bool true)
    1.61 +  | read_value (Bool _) "false" = SOME (Bool false)
    1.62 +  | read_value (Int _) s = Option.map Int (Syntax.read_int s)
    1.63 +  | read_value (String _) s = SOME (String s);
    1.64 +
    1.65 +fun print_value (Bool true) = "true"
    1.66 +  | print_value (Bool false) = "false"
    1.67 +  | print_value (Int i) = signed_string_of_int i
    1.68 +  | print_value (String s) = quote s;
    1.69 +
    1.70 +fun print_type (Bool _) = "boolean"
    1.71 +  | print_type (Int _) = "integer"
    1.72 +  | print_type (String _) = "string";
    1.73 +
    1.74 +structure ConfigData = GenericDataFun
    1.75 +(
    1.76 +  type T = value Inttab.table;
    1.77 +  val empty = Inttab.empty;
    1.78 +  val extend = I;
    1.79 +  fun merge _ = Inttab.merge (K true);
    1.80 +);
    1.81 +
    1.82 +
    1.83 +(* global declarations *)
    1.84 +
    1.85 +local val global_configs = ref (Symtab.empty: (value T * value) Symtab.table) in
    1.86 +
    1.87 +fun put_generic_src name src_value context =
    1.88 +  (case Symtab.lookup (! global_configs) name of
    1.89 +    NONE => error ("Unknown configuration option " ^ quote name)
    1.90 +  | SOME (config, default) =>
    1.91 +      (case read_value default src_value of
    1.92 +        SOME value => put_generic config value context
    1.93 +      | NONE => error ("Malformed " ^ print_type default ^
    1.94 +          " value for configuration option " ^ quote name)));
    1.95 +
    1.96 +fun declare make dest name default =
    1.97 +  let
    1.98 +    val id = serial ();
    1.99 +
   1.100 +    val default_value = make default;
   1.101 +    fun get_value context =
   1.102 +      the_default default_value (Inttab.lookup (ConfigData.get context) id);
   1.103 +    fun map_value f = ConfigData.map (Inttab.map_default (id, default_value) f);
   1.104 +    val config_value = Config {get_value = get_value, map_value = map_value};
   1.105 +
   1.106 +    val _ = CRITICAL (fn () =>
   1.107 +     (if Symtab.defined (! global_configs) name
   1.108 +      then warning ("Hiding existing configuration option " ^ quote name) else ();
   1.109 +      change global_configs (Symtab.update (name, (config_value, default_value)))));
   1.110 +
   1.111 +  in Config {get_value = dest o get_value, map_value = fn f => map_value (make o f o dest)} end;
   1.112 +
   1.113 +fun print_configs ctxt =
   1.114 +  let
   1.115 +    fun prt (name, (config, default)) =
   1.116 +      Pretty.block [Pretty.str (name ^ ": " ^ print_type default ^ " ="), Pretty.brk 1,
   1.117 +        Pretty.str (print_value (get_ctxt ctxt config))];
   1.118 +    val configs = sort_wrt #1 (Symtab.dest (! global_configs));
   1.119 +  in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
   1.120 +
   1.121 +end;
   1.122 +
   1.123 +val bool = declare Bool (fn Bool b => b);
   1.124 +val int = declare Int (fn Int i => i);
   1.125 +val string = declare String (fn String s => s);
   1.126 +
   1.127 +
   1.128 +(*final declarations of this structure!*)
   1.129 +val get = get_ctxt;
   1.130 +val map = map_ctxt;
   1.131 +val put = put_ctxt;
   1.132 +
   1.133 +end;