src/Pure/config.ML
author blanchet
Mon May 19 23:43:53 2014 +0200 (2014-05-19)
changeset 57008 10f68b83b474
parent 56438 7f6b2634d853
child 57858 39d9c7f175e0
permissions -rw-r--r--
use E 1.8's auto scheduler option
wenzelm@24114
     1
(*  Title:      Pure/config.ML
wenzelm@24114
     2
    Author:     Makarius
wenzelm@24114
     3
wenzelm@24114
     4
Configuration options as values within the local context.
wenzelm@24114
     5
*)
wenzelm@24114
     6
wenzelm@24114
     7
signature CONFIG =
wenzelm@24114
     8
sig
wenzelm@40291
     9
  datatype value = Bool of bool | Int of int | Real of real | String of string
wenzelm@24114
    10
  val print_value: value -> string
wenzelm@24114
    11
  val print_type: value -> string
wenzelm@24114
    12
  type 'a T
wenzelm@39163
    13
  type raw = value T
wenzelm@39163
    14
  val bool: raw -> bool T
wenzelm@39163
    15
  val int: raw -> int T
wenzelm@40291
    16
  val real: raw -> real T
wenzelm@39163
    17
  val string: raw -> string T
wenzelm@24114
    18
  val get: Proof.context -> 'a T -> 'a
wenzelm@24114
    19
  val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
wenzelm@24114
    20
  val put: 'a T -> 'a -> Proof.context -> Proof.context
wenzelm@36787
    21
  val get_global: theory -> 'a T -> 'a
wenzelm@36787
    22
  val map_global: 'a T -> ('a -> 'a) -> theory -> theory
wenzelm@36787
    23
  val put_global: 'a T -> 'a -> theory -> theory
wenzelm@24114
    24
  val get_generic: Context.generic -> 'a T -> 'a
wenzelm@24114
    25
  val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
wenzelm@24114
    26
  val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
wenzelm@56438
    27
  val declare: string * Position.T -> (Context.generic -> value) -> raw
wenzelm@56438
    28
  val declare_global: string * Position.T -> (Context.generic -> value) -> raw
wenzelm@56438
    29
  val declare_option: string * Position.T -> raw
wenzelm@56438
    30
  val declare_option_global: string * Position.T -> raw
wenzelm@24125
    31
  val name_of: 'a T -> string
wenzelm@56438
    32
  val pos_of: 'a T -> Position.T
wenzelm@24114
    33
end;
wenzelm@24114
    34
wenzelm@24114
    35
structure Config: CONFIG =
wenzelm@24114
    36
struct
wenzelm@24114
    37
wenzelm@24114
    38
(* simple values *)
wenzelm@24114
    39
wenzelm@24114
    40
datatype value =
wenzelm@24114
    41
  Bool of bool |
wenzelm@24114
    42
  Int of int |
wenzelm@40291
    43
  Real of real |
wenzelm@24114
    44
  String of string;
wenzelm@24114
    45
wenzelm@24114
    46
fun print_value (Bool true) = "true"
wenzelm@24114
    47
  | print_value (Bool false) = "false"
wenzelm@24114
    48
  | print_value (Int i) = signed_string_of_int i
wenzelm@51990
    49
  | print_value (Real x) = Markup.print_real x
wenzelm@24114
    50
  | print_value (String s) = quote s;
wenzelm@24114
    51
wenzelm@38804
    52
fun print_type (Bool _) = "bool"
wenzelm@38804
    53
  | print_type (Int _) = "int"
wenzelm@40291
    54
  | print_type (Real _) = "real"
wenzelm@24114
    55
  | print_type (String _) = "string";
wenzelm@24114
    56
wenzelm@24114
    57
fun same_type (Bool _) (Bool _) = true
wenzelm@24114
    58
  | same_type (Int _) (Int _) = true
wenzelm@40291
    59
  | same_type (Real _) (Real _) = true
wenzelm@24114
    60
  | same_type (String _) (String _) = true
wenzelm@24114
    61
  | same_type _ _ = false;
wenzelm@24114
    62
wenzelm@56438
    63
fun type_check (name, pos) f value =
wenzelm@24114
    64
  let
wenzelm@24114
    65
    val value' = f value;
wenzelm@24114
    66
    val _ = same_type value value' orelse
wenzelm@56438
    67
      error ("Ill-typed configuration option " ^ quote name ^ Position.here pos ^ ": " ^
wenzelm@24114
    68
        print_type value ^ " expected,\nbut " ^ print_type value' ^ " was found");
wenzelm@24114
    69
  in value' end;
wenzelm@24114
    70
wenzelm@24114
    71
wenzelm@24114
    72
(* abstract configuration options *)
wenzelm@24114
    73
wenzelm@24114
    74
datatype 'a T = Config of
wenzelm@24125
    75
 {name: string,
wenzelm@56438
    76
  pos: Position.T,
wenzelm@24125
    77
  get_value: Context.generic -> 'a,
wenzelm@24114
    78
  map_value: ('a -> 'a) -> Context.generic -> Context.generic};
wenzelm@24114
    79
wenzelm@39163
    80
type raw = value T;
wenzelm@39163
    81
wenzelm@56438
    82
fun coerce make dest (Config {name, pos, get_value, map_value}) = Config
wenzelm@24125
    83
 {name = name,
wenzelm@56438
    84
  pos = pos,
wenzelm@24125
    85
  get_value = dest o get_value,
wenzelm@24125
    86
  map_value = fn f => map_value (make o f o dest)};
wenzelm@24114
    87
wenzelm@24114
    88
val bool = coerce Bool (fn Bool b => b);
wenzelm@24114
    89
val int = coerce Int (fn Int i => i);
wenzelm@40291
    90
val real = coerce Real (fn Real x => x);
wenzelm@24114
    91
val string = coerce String (fn String s => s);
wenzelm@24114
    92
wenzelm@24114
    93
fun get_generic context (Config {get_value, ...}) = get_value context;
wenzelm@24114
    94
fun map_generic (Config {map_value, ...}) f context = map_value f context;
wenzelm@24114
    95
fun put_generic config value = map_generic config (K value);
wenzelm@24114
    96
wenzelm@24114
    97
fun get_ctxt ctxt = get_generic (Context.Proof ctxt);
wenzelm@24114
    98
fun map_ctxt config f = Context.proof_map (map_generic config f);
wenzelm@24114
    99
fun put_ctxt config value = map_ctxt config (K value);
wenzelm@24114
   100
wenzelm@36787
   101
fun get_global thy = get_generic (Context.Theory thy);
wenzelm@36787
   102
fun map_global config f = Context.theory_map (map_generic config f);
wenzelm@36787
   103
fun put_global config value = map_global config (K value);
wenzelm@24114
   104
wenzelm@24114
   105
wenzelm@24114
   106
(* context information *)
wenzelm@24114
   107
wenzelm@33519
   108
structure Value = Generic_Data
wenzelm@24114
   109
(
wenzelm@24114
   110
  type T = value Inttab.table;
wenzelm@24114
   111
  val empty = Inttab.empty;
wenzelm@24114
   112
  val extend = I;
wenzelm@33519
   113
  fun merge data = Inttab.merge (K true) data;
wenzelm@24114
   114
);
wenzelm@24114
   115
wenzelm@52469
   116
local
wenzelm@52469
   117
wenzelm@56438
   118
fun declare_generic global (name, pos) default =
wenzelm@24114
   119
  let
wenzelm@24114
   120
    val id = serial ();
wenzelm@24114
   121
wenzelm@36000
   122
    fun get_value context =
wenzelm@36000
   123
      (case Inttab.lookup (Value.get context) id of
wenzelm@36000
   124
        SOME value => value
wenzelm@36002
   125
      | NONE => default context);
wenzelm@36000
   126
wenzelm@36000
   127
    fun update_value f context =
wenzelm@56438
   128
      Value.map (Inttab.update (id, type_check (name, pos) f (get_value context))) context;
wenzelm@24114
   129
wenzelm@47814
   130
    fun map_value f (context as Context.Proof ctxt) =
wenzelm@36000
   131
          let val context' = update_value f context in
wenzelm@24114
   132
            if global andalso
wenzelm@47814
   133
              Context_Position.is_visible ctxt andalso
wenzelm@40291
   134
              print_value (get_value (Context.Theory (Context.theory_of context'))) <>
wenzelm@40291
   135
                print_value (get_value context')
wenzelm@47814
   136
            then
wenzelm@56294
   137
             (if Context_Position.is_visible ctxt then
wenzelm@56294
   138
                warning ("Ignoring local change of global option " ^ quote name)
wenzelm@56294
   139
              else (); context)
wenzelm@24114
   140
            else context'
wenzelm@24114
   141
          end
wenzelm@36000
   142
      | map_value f context = update_value f context;
wenzelm@56438
   143
  in Config {name = name, pos = pos, get_value = get_value, map_value = map_value} end;
wenzelm@24125
   144
wenzelm@56438
   145
fun declare_option_generic global (name, pos) =
wenzelm@51947
   146
  let
wenzelm@51947
   147
    val typ = Options.default_typ name;
wenzelm@51947
   148
    val default =
wenzelm@51947
   149
      if typ = Options.boolT then fn _ => Bool (Options.default_bool name)
wenzelm@51947
   150
      else if typ = Options.intT then fn _ => Int (Options.default_int name)
wenzelm@51947
   151
      else if typ = Options.realT then fn _ => Real (Options.default_real name)
wenzelm@51947
   152
      else if typ = Options.stringT then fn _ => String (Options.default_string name)
wenzelm@56438
   153
      else error ("Unknown type for option " ^ quote name ^ Position.here pos ^ " : " ^ quote typ);
wenzelm@56438
   154
  in declare_generic global (name, pos) default end;
wenzelm@52469
   155
wenzelm@52469
   156
in
wenzelm@52469
   157
wenzelm@52469
   158
val declare = declare_generic false;
wenzelm@52469
   159
val declare_global = declare_generic true;
wenzelm@52469
   160
val declare_option = declare_option_generic false;
wenzelm@52469
   161
val declare_option_global = declare_option_generic true;
wenzelm@52469
   162
wenzelm@52469
   163
end;
wenzelm@51947
   164
wenzelm@24125
   165
fun name_of (Config {name, ...}) = name;
wenzelm@56438
   166
fun pos_of (Config {pos, ...}) = pos;
wenzelm@24114
   167
wenzelm@24114
   168
wenzelm@24114
   169
(*final declarations of this structure!*)
wenzelm@24114
   170
val get = get_ctxt;
wenzelm@24114
   171
val map = map_ctxt;
wenzelm@24114
   172
val put = put_ctxt;
wenzelm@24114
   173
wenzelm@24114
   174
end;