src/Pure/config.ML
author wenzelm
Thu Aug 15 16:02:47 2019 +0200 (9 months ago)
changeset 70533 031620901fcd
parent 69576 cfac69e7b962
permissions -rw-r--r--
support for (fully reconstructed) proof terms in Scala;
proper cache_typs;
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@69575
    13
  val name_of: 'a T -> string
wenzelm@69575
    14
  val pos_of: 'a T -> Position.T
wenzelm@69576
    15
  val apply: 'a T -> Proof.context -> 'a
wenzelm@24114
    16
  val get: Proof.context -> 'a T -> 'a
wenzelm@24114
    17
  val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
wenzelm@24114
    18
  val put: 'a T -> 'a -> Proof.context -> Proof.context
wenzelm@68827
    19
  val restore: 'a T -> Proof.context -> Proof.context -> Proof.context
wenzelm@69576
    20
  val apply_global: 'a T -> theory -> 'a
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@68827
    24
  val restore_global: 'a T -> theory -> theory -> theory
wenzelm@69576
    25
  val apply_generic: 'a T -> Context.generic -> 'a
wenzelm@24114
    26
  val get_generic: Context.generic -> 'a T -> 'a
wenzelm@24114
    27
  val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
wenzelm@24114
    28
  val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
wenzelm@68827
    29
  val restore_generic: 'a T -> Context.generic -> Context.generic -> Context.generic
wenzelm@69575
    30
  val bool: value T -> bool T
wenzelm@69575
    31
  val bool_value: bool T -> value T
wenzelm@69575
    32
  val int: value T -> int T
wenzelm@69575
    33
  val int_value: int T -> value T
wenzelm@69575
    34
  val real: value T -> real T
wenzelm@69575
    35
  val real_value: real T -> value T
wenzelm@69575
    36
  val string: value T -> string T
wenzelm@69575
    37
  val string_value: string T -> value T
wenzelm@69575
    38
  val declare: string * Position.T -> (Context.generic -> value) -> value T
wenzelm@69575
    39
  val declare_bool: string * Position.T -> (Context.generic -> bool) -> bool T
wenzelm@69575
    40
  val declare_int: string * Position.T -> (Context.generic -> int) -> int T
wenzelm@69575
    41
  val declare_real: string * Position.T -> (Context.generic -> real) -> real T
wenzelm@69575
    42
  val declare_string: string * Position.T -> (Context.generic -> string) -> string T
wenzelm@69575
    43
  val declare_option: string * Position.T -> value T
wenzelm@69575
    44
  val declare_option_bool: string * Position.T -> bool T
wenzelm@69575
    45
  val declare_option_int: string * Position.T -> int T
wenzelm@69575
    46
  val declare_option_real: string * Position.T -> real T
wenzelm@69575
    47
  val declare_option_string: string * Position.T -> string T
wenzelm@24114
    48
end;
wenzelm@24114
    49
wenzelm@24114
    50
structure Config: CONFIG =
wenzelm@24114
    51
struct
wenzelm@24114
    52
wenzelm@24114
    53
(* simple values *)
wenzelm@24114
    54
wenzelm@24114
    55
datatype value =
wenzelm@24114
    56
  Bool of bool |
wenzelm@24114
    57
  Int of int |
wenzelm@40291
    58
  Real of real |
wenzelm@24114
    59
  String of string;
wenzelm@24114
    60
wenzelm@24114
    61
fun print_value (Bool true) = "true"
wenzelm@24114
    62
  | print_value (Bool false) = "false"
wenzelm@69574
    63
  | print_value (Int i) = Value.print_int i
wenzelm@63806
    64
  | print_value (Real x) = Value.print_real x
wenzelm@24114
    65
  | print_value (String s) = quote s;
wenzelm@24114
    66
wenzelm@38804
    67
fun print_type (Bool _) = "bool"
wenzelm@38804
    68
  | print_type (Int _) = "int"
wenzelm@40291
    69
  | print_type (Real _) = "real"
wenzelm@24114
    70
  | print_type (String _) = "string";
wenzelm@24114
    71
wenzelm@24114
    72
fun same_type (Bool _) (Bool _) = true
wenzelm@24114
    73
  | same_type (Int _) (Int _) = true
wenzelm@40291
    74
  | same_type (Real _) (Real _) = true
wenzelm@24114
    75
  | same_type (String _) (String _) = true
wenzelm@24114
    76
  | same_type _ _ = false;
wenzelm@24114
    77
wenzelm@56438
    78
fun type_check (name, pos) f value =
wenzelm@24114
    79
  let
wenzelm@24114
    80
    val value' = f value;
wenzelm@24114
    81
    val _ = same_type value value' orelse
wenzelm@56438
    82
      error ("Ill-typed configuration option " ^ quote name ^ Position.here pos ^ ": " ^
wenzelm@24114
    83
        print_type value ^ " expected,\nbut " ^ print_type value' ^ " was found");
wenzelm@24114
    84
  in value' end;
wenzelm@24114
    85
wenzelm@24114
    86
wenzelm@24114
    87
(* abstract configuration options *)
wenzelm@24114
    88
wenzelm@24114
    89
datatype 'a T = Config of
wenzelm@24125
    90
 {name: string,
wenzelm@56438
    91
  pos: Position.T,
wenzelm@24125
    92
  get_value: Context.generic -> 'a,
wenzelm@24114
    93
  map_value: ('a -> 'a) -> Context.generic -> Context.generic};
wenzelm@24114
    94
wenzelm@69575
    95
fun name_of (Config {name, ...}) = name;
wenzelm@69575
    96
fun pos_of (Config {pos, ...}) = pos;
wenzelm@24114
    97
wenzelm@69576
    98
fun apply_generic (Config {get_value, ...}) = get_value;
wenzelm@69576
    99
fun get_generic context config = apply_generic config context;
wenzelm@24114
   100
fun map_generic (Config {map_value, ...}) f context = map_value f context;
wenzelm@24114
   101
fun put_generic config value = map_generic config (K value);
wenzelm@69576
   102
fun restore_generic config = put_generic config o apply_generic config;
wenzelm@24114
   103
wenzelm@69576
   104
fun apply_ctxt config = apply_generic config o Context.Proof;
wenzelm@24114
   105
fun get_ctxt ctxt = get_generic (Context.Proof ctxt);
wenzelm@24114
   106
fun map_ctxt config f = Context.proof_map (map_generic config f);
wenzelm@24114
   107
fun put_ctxt config value = map_ctxt config (K value);
wenzelm@69576
   108
fun restore_ctxt config = put_ctxt config o apply_ctxt config;
wenzelm@24114
   109
wenzelm@69576
   110
fun apply_global config = apply_generic config o Context.Theory;
wenzelm@36787
   111
fun get_global thy = get_generic (Context.Theory thy);
wenzelm@36787
   112
fun map_global config f = Context.theory_map (map_generic config f);
wenzelm@36787
   113
fun put_global config value = map_global config (K value);
wenzelm@69576
   114
fun restore_global config = put_global config o apply_global config;
wenzelm@24114
   115
wenzelm@24114
   116
wenzelm@69575
   117
(* coerce type *)
wenzelm@69575
   118
wenzelm@69575
   119
fun coerce make dest (Config {name, pos, get_value, map_value}) = Config
wenzelm@69575
   120
 {name = name,
wenzelm@69575
   121
  pos = pos,
wenzelm@69575
   122
  get_value = dest o get_value,
wenzelm@69575
   123
  map_value = fn f => map_value (make o f o dest)};
wenzelm@69575
   124
wenzelm@69575
   125
fun coerce_pair make dest = (coerce make dest, coerce dest make);
wenzelm@69575
   126
wenzelm@69575
   127
val (bool, bool_value) = coerce_pair Bool (fn Bool b => b);
wenzelm@69575
   128
val (int, int_value) = coerce_pair Int (fn Int i => i);
wenzelm@69575
   129
val (real, real_value) = coerce_pair Real (fn Real x => x);
wenzelm@69575
   130
val (string, string_value) = coerce_pair String (fn String s => s);
wenzelm@69575
   131
wenzelm@69575
   132
wenzelm@69575
   133
(* context data *)
wenzelm@24114
   134
wenzelm@63806
   135
structure Data = Generic_Data
wenzelm@24114
   136
(
wenzelm@24114
   137
  type T = value Inttab.table;
wenzelm@24114
   138
  val empty = Inttab.empty;
wenzelm@24114
   139
  val extend = I;
wenzelm@33519
   140
  fun merge data = Inttab.merge (K true) data;
wenzelm@24114
   141
);
wenzelm@24114
   142
wenzelm@58951
   143
fun declare (name, pos) default =
wenzelm@24114
   144
  let
wenzelm@24114
   145
    val id = serial ();
wenzelm@24114
   146
wenzelm@36000
   147
    fun get_value context =
wenzelm@63806
   148
      (case Inttab.lookup (Data.get context) id of
wenzelm@36000
   149
        SOME value => value
wenzelm@36002
   150
      | NONE => default context);
wenzelm@36000
   151
wenzelm@58951
   152
    fun map_value f context =
wenzelm@63806
   153
      Data.map (Inttab.update (id, type_check (name, pos) f (get_value context))) context;
wenzelm@58951
   154
  in
wenzelm@58951
   155
    Config {name = name, pos = pos, get_value = get_value, map_value = map_value}
wenzelm@58951
   156
  end;
wenzelm@24114
   157
wenzelm@69575
   158
fun declare_bool name default = bool (declare name (Bool o default));
wenzelm@69575
   159
fun declare_int name default = int (declare name (Int o default));
wenzelm@69575
   160
fun declare_real name default = real (declare name (Real o default));
wenzelm@69575
   161
fun declare_string name default = string (declare name (String o default));
wenzelm@69575
   162
wenzelm@69575
   163
wenzelm@69575
   164
(* system options *)
wenzelm@69575
   165
wenzelm@58951
   166
fun declare_option (name, pos) =
wenzelm@51947
   167
  let
wenzelm@51947
   168
    val typ = Options.default_typ name;
wenzelm@51947
   169
    val default =
wenzelm@51947
   170
      if typ = Options.boolT then fn _ => Bool (Options.default_bool name)
wenzelm@51947
   171
      else if typ = Options.intT then fn _ => Int (Options.default_int name)
wenzelm@51947
   172
      else if typ = Options.realT then fn _ => Real (Options.default_real name)
wenzelm@51947
   173
      else if typ = Options.stringT then fn _ => String (Options.default_string name)
wenzelm@56438
   174
      else error ("Unknown type for option " ^ quote name ^ Position.here pos ^ " : " ^ quote typ);
wenzelm@58951
   175
  in declare (name, pos) default end;
wenzelm@51947
   176
wenzelm@69575
   177
val declare_option_bool = bool o declare_option;
wenzelm@69575
   178
val declare_option_int = int o declare_option;
wenzelm@69575
   179
val declare_option_real = real o declare_option;
wenzelm@69575
   180
val declare_option_string = string o declare_option;
wenzelm@24114
   181
wenzelm@24114
   182
(*final declarations of this structure!*)
wenzelm@69576
   183
val apply = apply_ctxt;
wenzelm@24114
   184
val get = get_ctxt;
wenzelm@24114
   185
val map = map_ctxt;
wenzelm@24114
   186
val put = put_ctxt;
wenzelm@68827
   187
val restore = restore_ctxt;
wenzelm@24114
   188
wenzelm@24114
   189
end;