src/Pure/config.ML
author wenzelm
Mon Sep 06 21:33:19 2010 +0200 (2010-09-06)
changeset 39163 4d701c0388c3
parent 39116 f14735a88886
child 40291 012ed4426fda
permissions -rw-r--r--
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
     1 (*  Title:      Pure/config.ML
     2     Author:     Makarius
     3 
     4 Configuration options as values within the local context.
     5 *)
     6 
     7 signature CONFIG =
     8 sig
     9   datatype value = Bool of bool | Int of int | String of string
    10   val print_value: value -> string
    11   val print_type: value -> string
    12   type 'a T
    13   type raw = value T
    14   val bool: raw -> bool T
    15   val int: raw -> int T
    16   val string: raw -> string T
    17   val get: Proof.context -> 'a T -> 'a
    18   val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
    19   val put: 'a T -> 'a -> Proof.context -> Proof.context
    20   val get_global: theory -> 'a T -> 'a
    21   val map_global: 'a T -> ('a -> 'a) -> theory -> theory
    22   val put_global: 'a T -> 'a -> theory -> theory
    23   val get_generic: Context.generic -> 'a T -> 'a
    24   val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
    25   val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
    26   val declare_generic: {global: bool} -> string -> (Context.generic -> value) -> raw
    27   val declare_global: string -> (Context.generic -> value) -> raw
    28   val declare: string -> (Context.generic -> value) -> raw
    29   val name_of: 'a T -> string
    30 end;
    31 
    32 structure Config: CONFIG =
    33 struct
    34 
    35 (* simple values *)
    36 
    37 datatype value =
    38   Bool of bool |
    39   Int of int |
    40   String of string;
    41 
    42 fun print_value (Bool true) = "true"
    43   | print_value (Bool false) = "false"
    44   | print_value (Int i) = signed_string_of_int i
    45   | print_value (String s) = quote s;
    46 
    47 fun print_type (Bool _) = "bool"
    48   | print_type (Int _) = "int"
    49   | print_type (String _) = "string";
    50 
    51 fun same_type (Bool _) (Bool _) = true
    52   | same_type (Int _) (Int _) = true
    53   | same_type (String _) (String _) = true
    54   | same_type _ _ = false;
    55 
    56 fun type_check name f value =
    57   let
    58     val value' = f value;
    59     val _ = same_type value value' orelse
    60       error ("Ill-typed configuration option " ^ quote name ^ ": " ^
    61         print_type value ^ " expected,\nbut " ^ print_type value' ^ " was found");
    62   in value' end;
    63 
    64 
    65 (* abstract configuration options *)
    66 
    67 datatype 'a T = Config of
    68  {name: string,
    69   get_value: Context.generic -> 'a,
    70   map_value: ('a -> 'a) -> Context.generic -> Context.generic};
    71 
    72 type raw = value T;
    73 
    74 fun coerce make dest (Config {name, get_value, map_value}) = Config
    75  {name = name,
    76   get_value = dest o get_value,
    77   map_value = fn f => map_value (make o f o dest)};
    78 
    79 val bool = coerce Bool (fn Bool b => b);
    80 val int = coerce Int (fn Int i => i);
    81 val string = coerce String (fn String s => s);
    82 
    83 fun get_generic context (Config {get_value, ...}) = get_value context;
    84 fun map_generic (Config {map_value, ...}) f context = map_value f context;
    85 fun put_generic config value = map_generic config (K value);
    86 
    87 fun get_ctxt ctxt = get_generic (Context.Proof ctxt);
    88 fun map_ctxt config f = Context.proof_map (map_generic config f);
    89 fun put_ctxt config value = map_ctxt config (K value);
    90 
    91 fun get_global thy = get_generic (Context.Theory thy);
    92 fun map_global config f = Context.theory_map (map_generic config f);
    93 fun put_global config value = map_global config (K value);
    94 
    95 
    96 (* context information *)
    97 
    98 structure Value = Generic_Data
    99 (
   100   type T = value Inttab.table;
   101   val empty = Inttab.empty;
   102   val extend = I;
   103   fun merge data = Inttab.merge (K true) data;
   104 );
   105 
   106 fun declare_generic {global} name default =
   107   let
   108     val id = serial ();
   109 
   110     fun get_value context =
   111       (case Inttab.lookup (Value.get context) id of
   112         SOME value => value
   113       | NONE => default context);
   114 
   115     fun update_value f context =
   116       Value.map (Inttab.update (id, type_check name f (get_value context))) context;
   117 
   118     fun map_value f (context as Context.Proof _) =
   119           let val context' = update_value f context in
   120             if global andalso
   121               get_value (Context.Theory (Context.theory_of context')) <> get_value context'
   122             then (warning ("Ignoring local change of global option " ^ quote name); context)
   123             else context'
   124           end
   125       | map_value f context = update_value f context;
   126   in Config {name = name, get_value = get_value, map_value = map_value} end;
   127 
   128 val declare_global = declare_generic {global = true};
   129 val declare = declare_generic {global = false};
   130 
   131 fun name_of (Config {name, ...}) = name;
   132 
   133 
   134 (*final declarations of this structure!*)
   135 val get = get_ctxt;
   136 val map = map_ctxt;
   137 val put = put_ctxt;
   138 
   139 end;