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