src/Pure/config.ML
author wenzelm
Sat Dec 13 15:00:39 2008 +0100 (2008-12-13)
changeset 29091 b81fe045e799
parent 24125 454a0c895735
child 29606 fedb8be05f24
permissions -rw-r--r--
Context.display_names;
     1 (*  Title:      Pure/config.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Configuration options as values within the local context.
     6 *)
     7 
     8 signature CONFIG =
     9 sig
    10   datatype value = Bool of bool | Int of int | String of string
    11   val print_value: value -> string
    12   val print_type: value -> string
    13   type 'a T
    14   val bool: value T -> bool T
    15   val int: value T -> int T
    16   val string: value T -> 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_thy: theory -> 'a T -> 'a
    21   val map_thy: 'a T -> ('a -> 'a) -> theory -> theory
    22   val put_thy: '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: bool -> string -> value -> value T
    27   val name_of: 'a T -> string
    28 end;
    29 
    30 structure Config: CONFIG =
    31 struct
    32 
    33 (* simple values *)
    34 
    35 datatype value =
    36   Bool of bool |
    37   Int of int |
    38   String of string;
    39 
    40 fun print_value (Bool true) = "true"
    41   | print_value (Bool false) = "false"
    42   | print_value (Int i) = signed_string_of_int i
    43   | print_value (String s) = quote s;
    44 
    45 fun print_type (Bool _) = "boolean"
    46   | print_type (Int _) = "integer"
    47   | print_type (String _) = "string";
    48 
    49 fun same_type (Bool _) (Bool _) = true
    50   | same_type (Int _) (Int _) = true
    51   | same_type (String _) (String _) = true
    52   | same_type _ _ = false;
    53 
    54 fun type_check name f value =
    55   let
    56     val value' = f value;
    57     val _ = same_type value value' orelse
    58       error ("Ill-typed configuration option " ^ quote name ^ ": " ^
    59         print_type value ^ " expected,\nbut " ^ print_type value' ^ " was found");
    60   in value' end;
    61 
    62 
    63 (* abstract configuration options *)
    64 
    65 datatype 'a T = Config of
    66  {name: string,
    67   get_value: Context.generic -> 'a,
    68   map_value: ('a -> 'a) -> Context.generic -> Context.generic};
    69 
    70 fun coerce make dest (Config {name, get_value, map_value}) = Config
    71  {name = name,
    72   get_value = dest o get_value,
    73   map_value = fn f => map_value (make o f o dest)};
    74 
    75 val bool = coerce Bool (fn Bool b => b);
    76 val int = coerce Int (fn Int i => i);
    77 val string = coerce String (fn String s => s);
    78 
    79 fun get_generic context (Config {get_value, ...}) = get_value context;
    80 fun map_generic (Config {map_value, ...}) f context = map_value f context;
    81 fun put_generic config value = map_generic config (K value);
    82 
    83 fun get_ctxt ctxt = get_generic (Context.Proof ctxt);
    84 fun map_ctxt config f = Context.proof_map (map_generic config f);
    85 fun put_ctxt config value = map_ctxt config (K value);
    86 
    87 fun get_thy thy = get_generic (Context.Theory thy);
    88 fun map_thy config f = Context.theory_map (map_generic config f);
    89 fun put_thy config value = map_thy config (K value);
    90 
    91 
    92 (* context information *)
    93 
    94 structure Value = GenericDataFun
    95 (
    96   type T = value Inttab.table;
    97   val empty = Inttab.empty;
    98   val extend = I;
    99   fun merge _ = Inttab.merge (K true);
   100 );
   101 
   102 fun declare global name default =
   103   let
   104     val id = serial ();
   105 
   106     fun get_value context = the_default default (Inttab.lookup (Value.get context) id);
   107     fun modify_value f = Value.map (Inttab.map_default (id, default) (type_check name f));
   108 
   109     fun map_value f (context as Context.Proof _) =
   110           let val context' = modify_value f context in
   111             if global andalso
   112               get_value (Context.Theory (Context.theory_of context')) <> get_value context'
   113             then (warning ("Ignoring local change of global option " ^ quote name); context)
   114             else context'
   115           end
   116       | map_value f context = modify_value f context;
   117   in Config {name = name, get_value = get_value, map_value = map_value} end;
   118 
   119 fun name_of (Config {name, ...}) = name;
   120 
   121 
   122 (*final declarations of this structure!*)
   123 val get = get_ctxt;
   124 val map = map_ctxt;
   125 val put = put_ctxt;
   126 
   127 end;