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