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