author | wenzelm |
Thu, 03 Jan 2019 14:12:44 +0100 | |
changeset 69575 | f77cc54f6d47 |
parent 69574 | b4ea943ce0b7 |
child 69576 | cfac69e7b962 |
permissions | -rw-r--r-- |
24114 | 1 |
(* Title: Pure/config.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Configuration options as values within the local context. |
|
5 |
*) |
|
6 |
||
7 |
signature CONFIG = |
|
8 |
sig |
|
40291 | 9 |
datatype value = Bool of bool | Int of int | Real of real | String of string |
24114 | 10 |
val print_value: value -> string |
11 |
val print_type: value -> string |
|
12 |
type 'a T |
|
69575 | 13 |
val name_of: 'a T -> string |
14 |
val pos_of: 'a T -> Position.T |
|
24114 | 15 |
val get: Proof.context -> 'a T -> 'a |
16 |
val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context |
|
17 |
val put: 'a T -> 'a -> Proof.context -> Proof.context |
|
68827 | 18 |
val restore: 'a T -> Proof.context -> Proof.context -> Proof.context |
36787
f60e4dd6d76f
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
wenzelm
parents:
36002
diff
changeset
|
19 |
val get_global: theory -> 'a T -> 'a |
f60e4dd6d76f
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
wenzelm
parents:
36002
diff
changeset
|
20 |
val map_global: 'a T -> ('a -> 'a) -> theory -> theory |
f60e4dd6d76f
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
wenzelm
parents:
36002
diff
changeset
|
21 |
val put_global: 'a T -> 'a -> theory -> theory |
68827 | 22 |
val restore_global: 'a T -> theory -> theory -> theory |
24114 | 23 |
val get_generic: Context.generic -> 'a T -> 'a |
24 |
val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic |
|
25 |
val put_generic: 'a T -> 'a -> Context.generic -> Context.generic |
|
68827 | 26 |
val restore_generic: 'a T -> Context.generic -> Context.generic -> Context.generic |
69575 | 27 |
val bool: value T -> bool T |
28 |
val bool_value: bool T -> value T |
|
29 |
val int: value T -> int T |
|
30 |
val int_value: int T -> value T |
|
31 |
val real: value T -> real T |
|
32 |
val real_value: real T -> value T |
|
33 |
val string: value T -> string T |
|
34 |
val string_value: string T -> value T |
|
35 |
val declare: string * Position.T -> (Context.generic -> value) -> value T |
|
36 |
val declare_bool: string * Position.T -> (Context.generic -> bool) -> bool T |
|
37 |
val declare_int: string * Position.T -> (Context.generic -> int) -> int T |
|
38 |
val declare_real: string * Position.T -> (Context.generic -> real) -> real T |
|
39 |
val declare_string: string * Position.T -> (Context.generic -> string) -> string T |
|
40 |
val declare_option: string * Position.T -> value T |
|
41 |
val declare_option_bool: string * Position.T -> bool T |
|
42 |
val declare_option_int: string * Position.T -> int T |
|
43 |
val declare_option_real: string * Position.T -> real T |
|
44 |
val declare_option_string: string * Position.T -> string T |
|
24114 | 45 |
end; |
46 |
||
47 |
structure Config: CONFIG = |
|
48 |
struct |
|
49 |
||
50 |
(* simple values *) |
|
51 |
||
52 |
datatype value = |
|
53 |
Bool of bool | |
|
54 |
Int of int | |
|
40291 | 55 |
Real of real | |
24114 | 56 |
String of string; |
57 |
||
58 |
fun print_value (Bool true) = "true" |
|
59 |
| print_value (Bool false) = "false" |
|
69574 | 60 |
| print_value (Int i) = Value.print_int i |
63806 | 61 |
| print_value (Real x) = Value.print_real x |
24114 | 62 |
| print_value (String s) = quote s; |
63 |
||
38804 | 64 |
fun print_type (Bool _) = "bool" |
65 |
| print_type (Int _) = "int" |
|
40291 | 66 |
| print_type (Real _) = "real" |
24114 | 67 |
| print_type (String _) = "string"; |
68 |
||
69 |
fun same_type (Bool _) (Bool _) = true |
|
70 |
| same_type (Int _) (Int _) = true |
|
40291 | 71 |
| same_type (Real _) (Real _) = true |
24114 | 72 |
| same_type (String _) (String _) = true |
73 |
| same_type _ _ = false; |
|
74 |
||
56438 | 75 |
fun type_check (name, pos) f value = |
24114 | 76 |
let |
77 |
val value' = f value; |
|
78 |
val _ = same_type value value' orelse |
|
56438 | 79 |
error ("Ill-typed configuration option " ^ quote name ^ Position.here pos ^ ": " ^ |
24114 | 80 |
print_type value ^ " expected,\nbut " ^ print_type value' ^ " was found"); |
81 |
in value' end; |
|
82 |
||
83 |
||
84 |
(* abstract configuration options *) |
|
85 |
||
86 |
datatype 'a T = Config of |
|
24125 | 87 |
{name: string, |
56438 | 88 |
pos: Position.T, |
24125 | 89 |
get_value: Context.generic -> 'a, |
24114 | 90 |
map_value: ('a -> 'a) -> Context.generic -> Context.generic}; |
91 |
||
69575 | 92 |
fun name_of (Config {name, ...}) = name; |
93 |
fun pos_of (Config {pos, ...}) = pos; |
|
24114 | 94 |
|
95 |
fun get_generic context (Config {get_value, ...}) = get_value context; |
|
96 |
fun map_generic (Config {map_value, ...}) f context = map_value f context; |
|
97 |
fun put_generic config value = map_generic config (K value); |
|
68827 | 98 |
fun restore_generic config context = put_generic config (get_generic context config); |
24114 | 99 |
|
100 |
fun get_ctxt ctxt = get_generic (Context.Proof ctxt); |
|
101 |
fun map_ctxt config f = Context.proof_map (map_generic config f); |
|
102 |
fun put_ctxt config value = map_ctxt config (K value); |
|
68827 | 103 |
fun restore_ctxt config ctxt = put_ctxt config (get_ctxt ctxt config); |
24114 | 104 |
|
36787
f60e4dd6d76f
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
wenzelm
parents:
36002
diff
changeset
|
105 |
fun get_global thy = get_generic (Context.Theory thy); |
f60e4dd6d76f
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
wenzelm
parents:
36002
diff
changeset
|
106 |
fun map_global config f = Context.theory_map (map_generic config f); |
f60e4dd6d76f
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
wenzelm
parents:
36002
diff
changeset
|
107 |
fun put_global config value = map_global config (K value); |
68827 | 108 |
fun restore_global config thy = put_global config (get_global thy config); |
24114 | 109 |
|
110 |
||
69575 | 111 |
(* coerce type *) |
112 |
||
113 |
fun coerce make dest (Config {name, pos, get_value, map_value}) = Config |
|
114 |
{name = name, |
|
115 |
pos = pos, |
|
116 |
get_value = dest o get_value, |
|
117 |
map_value = fn f => map_value (make o f o dest)}; |
|
118 |
||
119 |
fun coerce_pair make dest = (coerce make dest, coerce dest make); |
|
120 |
||
121 |
val (bool, bool_value) = coerce_pair Bool (fn Bool b => b); |
|
122 |
val (int, int_value) = coerce_pair Int (fn Int i => i); |
|
123 |
val (real, real_value) = coerce_pair Real (fn Real x => x); |
|
124 |
val (string, string_value) = coerce_pair String (fn String s => s); |
|
125 |
||
126 |
||
127 |
(* context data *) |
|
24114 | 128 |
|
63806 | 129 |
structure Data = Generic_Data |
24114 | 130 |
( |
131 |
type T = value Inttab.table; |
|
132 |
val empty = Inttab.empty; |
|
133 |
val extend = I; |
|
33519 | 134 |
fun merge data = Inttab.merge (K true) data; |
24114 | 135 |
); |
136 |
||
58951
8b7caf447357
removed obsolete global-only options, which did not work out anyway (due to complexity of local_theory sandwich);
wenzelm
parents:
57858
diff
changeset
|
137 |
fun declare (name, pos) default = |
24114 | 138 |
let |
139 |
val id = serial (); |
|
140 |
||
36000
5560b2437789
configuration options admit dynamic default values;
wenzelm
parents:
33519
diff
changeset
|
141 |
fun get_value context = |
63806 | 142 |
(case Inttab.lookup (Data.get context) id of |
36000
5560b2437789
configuration options admit dynamic default values;
wenzelm
parents:
33519
diff
changeset
|
143 |
SOME value => value |
36002
f4f343500249
pass raw Context.generic, to avoid wasteful Context.proof_of -- Config.get_thy is often used in performance critical spots like unify.ML;
wenzelm
parents:
36000
diff
changeset
|
144 |
| NONE => default context); |
36000
5560b2437789
configuration options admit dynamic default values;
wenzelm
parents:
33519
diff
changeset
|
145 |
|
58951
8b7caf447357
removed obsolete global-only options, which did not work out anyway (due to complexity of local_theory sandwich);
wenzelm
parents:
57858
diff
changeset
|
146 |
fun map_value f context = |
63806 | 147 |
Data.map (Inttab.update (id, type_check (name, pos) f (get_value context))) context; |
58951
8b7caf447357
removed obsolete global-only options, which did not work out anyway (due to complexity of local_theory sandwich);
wenzelm
parents:
57858
diff
changeset
|
148 |
in |
8b7caf447357
removed obsolete global-only options, which did not work out anyway (due to complexity of local_theory sandwich);
wenzelm
parents:
57858
diff
changeset
|
149 |
Config {name = name, pos = pos, get_value = get_value, map_value = map_value} |
8b7caf447357
removed obsolete global-only options, which did not work out anyway (due to complexity of local_theory sandwich);
wenzelm
parents:
57858
diff
changeset
|
150 |
end; |
24114 | 151 |
|
69575 | 152 |
fun declare_bool name default = bool (declare name (Bool o default)); |
153 |
fun declare_int name default = int (declare name (Int o default)); |
|
154 |
fun declare_real name default = real (declare name (Real o default)); |
|
155 |
fun declare_string name default = string (declare name (String o default)); |
|
156 |
||
157 |
||
158 |
(* system options *) |
|
159 |
||
58951
8b7caf447357
removed obsolete global-only options, which did not work out anyway (due to complexity of local_theory sandwich);
wenzelm
parents:
57858
diff
changeset
|
160 |
fun declare_option (name, pos) = |
51947
3301612c4893
support for system options as context-sensitive config options;
wenzelm
parents:
47814
diff
changeset
|
161 |
let |
3301612c4893
support for system options as context-sensitive config options;
wenzelm
parents:
47814
diff
changeset
|
162 |
val typ = Options.default_typ name; |
3301612c4893
support for system options as context-sensitive config options;
wenzelm
parents:
47814
diff
changeset
|
163 |
val default = |
3301612c4893
support for system options as context-sensitive config options;
wenzelm
parents:
47814
diff
changeset
|
164 |
if typ = Options.boolT then fn _ => Bool (Options.default_bool name) |
3301612c4893
support for system options as context-sensitive config options;
wenzelm
parents:
47814
diff
changeset
|
165 |
else if typ = Options.intT then fn _ => Int (Options.default_int name) |
3301612c4893
support for system options as context-sensitive config options;
wenzelm
parents:
47814
diff
changeset
|
166 |
else if typ = Options.realT then fn _ => Real (Options.default_real name) |
3301612c4893
support for system options as context-sensitive config options;
wenzelm
parents:
47814
diff
changeset
|
167 |
else if typ = Options.stringT then fn _ => String (Options.default_string name) |
56438 | 168 |
else error ("Unknown type for option " ^ quote name ^ Position.here pos ^ " : " ^ quote typ); |
58951
8b7caf447357
removed obsolete global-only options, which did not work out anyway (due to complexity of local_theory sandwich);
wenzelm
parents:
57858
diff
changeset
|
169 |
in declare (name, pos) default end; |
51947
3301612c4893
support for system options as context-sensitive config options;
wenzelm
parents:
47814
diff
changeset
|
170 |
|
69575 | 171 |
val declare_option_bool = bool o declare_option; |
172 |
val declare_option_int = int o declare_option; |
|
173 |
val declare_option_real = real o declare_option; |
|
174 |
val declare_option_string = string o declare_option; |
|
24114 | 175 |
|
176 |
(*final declarations of this structure!*) |
|
177 |
val get = get_ctxt; |
|
178 |
val map = map_ctxt; |
|
179 |
val put = put_ctxt; |
|
68827 | 180 |
val restore = restore_ctxt; |
24114 | 181 |
|
182 |
end; |