src/Pure/config.ML
author wenzelm
Fri Apr 12 14:54:14 2013 +0200 (2013-04-12)
changeset 51700 c8f2bad67dbb
parent 47814 53668571d300
child 51947 3301612c4893
permissions -rw-r--r--
tuned signature;
tuned comments;
     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 | Real of real | 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 real: raw -> real T
    17   val string: raw -> string T
    18   val get: Proof.context -> 'a T -> 'a
    19   val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
    20   val put: 'a T -> 'a -> Proof.context -> Proof.context
    21   val get_global: theory -> 'a T -> 'a
    22   val map_global: 'a T -> ('a -> 'a) -> theory -> theory
    23   val put_global: 'a T -> 'a -> theory -> theory
    24   val get_generic: Context.generic -> 'a T -> 'a
    25   val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
    26   val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
    27   val declare_generic: {global: bool} -> string -> (Context.generic -> value) -> raw
    28   val declare_global: string -> (Context.generic -> value) -> raw
    29   val declare: string -> (Context.generic -> value) -> raw
    30   val name_of: 'a T -> string
    31 end;
    32 
    33 structure Config: CONFIG =
    34 struct
    35 
    36 (* simple values *)
    37 
    38 datatype value =
    39   Bool of bool |
    40   Int of int |
    41   Real of real |
    42   String of string;
    43 
    44 fun print_value (Bool true) = "true"
    45   | print_value (Bool false) = "false"
    46   | print_value (Int i) = signed_string_of_int i
    47   | print_value (Real x) = signed_string_of_real x
    48   | print_value (String s) = quote s;
    49 
    50 fun print_type (Bool _) = "bool"
    51   | print_type (Int _) = "int"
    52   | print_type (Real _) = "real"
    53   | print_type (String _) = "string";
    54 
    55 fun same_type (Bool _) (Bool _) = true
    56   | same_type (Int _) (Int _) = true
    57   | same_type (Real _) (Real _) = true
    58   | same_type (String _) (String _) = true
    59   | same_type _ _ = false;
    60 
    61 fun type_check name f value =
    62   let
    63     val value' = f value;
    64     val _ = same_type value value' orelse
    65       error ("Ill-typed configuration option " ^ quote name ^ ": " ^
    66         print_type value ^ " expected,\nbut " ^ print_type value' ^ " was found");
    67   in value' end;
    68 
    69 
    70 (* abstract configuration options *)
    71 
    72 datatype 'a T = Config of
    73  {name: string,
    74   get_value: Context.generic -> 'a,
    75   map_value: ('a -> 'a) -> Context.generic -> Context.generic};
    76 
    77 type raw = value T;
    78 
    79 fun coerce make dest (Config {name, get_value, map_value}) = Config
    80  {name = name,
    81   get_value = dest o get_value,
    82   map_value = fn f => map_value (make o f o dest)};
    83 
    84 val bool = coerce Bool (fn Bool b => b);
    85 val int = coerce Int (fn Int i => i);
    86 val real = coerce Real (fn Real x => x);
    87 val string = coerce String (fn String s => s);
    88 
    89 fun get_generic context (Config {get_value, ...}) = get_value context;
    90 fun map_generic (Config {map_value, ...}) f context = map_value f context;
    91 fun put_generic config value = map_generic config (K value);
    92 
    93 fun get_ctxt ctxt = get_generic (Context.Proof ctxt);
    94 fun map_ctxt config f = Context.proof_map (map_generic config f);
    95 fun put_ctxt config value = map_ctxt config (K value);
    96 
    97 fun get_global thy = get_generic (Context.Theory thy);
    98 fun map_global config f = Context.theory_map (map_generic config f);
    99 fun put_global config value = map_global config (K value);
   100 
   101 
   102 (* context information *)
   103 
   104 structure Value = Generic_Data
   105 (
   106   type T = value Inttab.table;
   107   val empty = Inttab.empty;
   108   val extend = I;
   109   fun merge data = Inttab.merge (K true) data;
   110 );
   111 
   112 fun declare_generic {global} name default =
   113   let
   114     val id = serial ();
   115 
   116     fun get_value context =
   117       (case Inttab.lookup (Value.get context) id of
   118         SOME value => value
   119       | NONE => default context);
   120 
   121     fun update_value f context =
   122       Value.map (Inttab.update (id, type_check name f (get_value context))) context;
   123 
   124     fun map_value f (context as Context.Proof ctxt) =
   125           let val context' = update_value f context in
   126             if global andalso
   127               Context_Position.is_visible ctxt andalso
   128               print_value (get_value (Context.Theory (Context.theory_of context'))) <>
   129                 print_value (get_value context')
   130             then
   131               (Context_Position.if_visible ctxt warning
   132                 ("Ignoring local change of global option " ^ quote name); context)
   133             else context'
   134           end
   135       | map_value f context = update_value f context;
   136   in Config {name = name, get_value = get_value, map_value = map_value} end;
   137 
   138 val declare_global = declare_generic {global = true};
   139 val declare = declare_generic {global = false};
   140 
   141 fun name_of (Config {name, ...}) = name;
   142 
   143 
   144 (*final declarations of this structure!*)
   145 val get = get_ctxt;
   146 val map = map_ctxt;
   147 val put = put_ctxt;
   148 
   149 end;