author | wenzelm |
Fri, 27 Jul 2007 16:31:14 +0200 | |
changeset 24001 | 067d8e589c58 |
parent 23987 | 6d78feed74dd |
child 24004 | 8c962a9be9f2 |
permissions | -rw-r--r-- |
23987
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/config.ML |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
3 |
Author: Makarius |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
4 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
5 |
Configuration options as values within the local context. Global |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
6 |
environment of named options, with type declaration. |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
7 |
*) |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
8 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
9 |
signature CONFIG = |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
10 |
sig |
24001 | 11 |
datatype value = Bool of bool | Int of int | String of string |
23987
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
12 |
type 'a T |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
13 |
val get: Proof.context -> 'a T -> 'a |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
14 |
val get_thy: theory -> 'a T -> 'a |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
15 |
val get_generic: Context.generic -> 'a T -> 'a |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
16 |
val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
17 |
val map_thy: 'a T -> ('a -> 'a) -> theory -> theory |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
18 |
val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
19 |
val put: 'a T -> 'a -> Proof.context -> Proof.context |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
20 |
val put_thy: 'a T -> 'a -> theory -> theory |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
21 |
val put_generic: 'a T -> 'a -> Context.generic -> Context.generic |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
22 |
val print_configs: Proof.context -> unit |
24001 | 23 |
val the_config: string -> value T * value |
23987
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
24 |
val bool: string -> bool -> bool T |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
25 |
val int: string -> int -> int T |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
26 |
val string: string -> string -> string T |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
27 |
end; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
28 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
29 |
structure Config: CONFIG = |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
30 |
struct |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
31 |
|
24001 | 32 |
(* mixed values *) |
33 |
||
34 |
datatype value = |
|
35 |
Bool of bool | |
|
36 |
Int of int | |
|
37 |
String of string; |
|
38 |
||
39 |
fun print_value (Bool true) = "true" |
|
40 |
| print_value (Bool false) = "false" |
|
41 |
| print_value (Int i) = signed_string_of_int i |
|
42 |
| print_value (String s) = quote s; |
|
43 |
||
44 |
fun print_type (Bool _) = "boolean" |
|
45 |
| print_type (Int _) = "integer" |
|
46 |
| print_type (String _) = "string"; |
|
47 |
||
48 |
structure ConfigData = GenericDataFun |
|
49 |
( |
|
50 |
type T = value Inttab.table; |
|
51 |
val empty = Inttab.empty; |
|
52 |
val extend = I; |
|
53 |
fun merge _ = Inttab.merge (K true); |
|
54 |
); |
|
55 |
||
56 |
||
23987
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
57 |
(* abstract configuration options *) |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
58 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
59 |
datatype 'a T = Config of |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
60 |
{get_value: Context.generic -> 'a, |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
61 |
map_value: ('a -> 'a) -> Context.generic -> Context.generic}; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
62 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
63 |
fun get_generic context (Config {get_value, ...}) = get_value context; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
64 |
fun get_ctxt ctxt = get_generic (Context.Proof ctxt); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
65 |
fun get_thy thy = get_generic (Context.Theory thy); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
66 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
67 |
fun map_generic (Config {map_value, ...}) f context = map_value f context; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
68 |
fun map_ctxt config f = Context.proof_map (map_generic config f); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
69 |
fun map_thy config f = Context.theory_map (map_generic config f); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
70 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
71 |
fun put_generic config value = map_generic config (K value); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
72 |
fun put_ctxt config value = map_ctxt config (K value); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
73 |
fun put_thy config value = map_thy config (K value); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
74 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
75 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
76 |
(* global declarations *) |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
77 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
78 |
local val global_configs = ref (Symtab.empty: (value T * value) Symtab.table) in |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
79 |
|
24001 | 80 |
fun print_configs ctxt = |
81 |
let |
|
82 |
fun prt (name, (config, default)) = |
|
83 |
Pretty.block [Pretty.str (name ^ ": " ^ print_type default ^ " ="), Pretty.brk 1, |
|
84 |
Pretty.str (print_value (get_ctxt ctxt config))]; |
|
85 |
val configs = sort_wrt #1 (Symtab.dest (! global_configs)); |
|
86 |
in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end; |
|
87 |
||
88 |
fun the_config name = |
|
89 |
(case Symtab.lookup (! global_configs) name of SOME cfg => cfg |
|
90 |
| NONE => error ("Unknown configuration option " ^ quote name)); |
|
23987
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
91 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
92 |
fun declare make dest name default = |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
93 |
let |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
94 |
val id = serial (); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
95 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
96 |
val default_value = make default; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
97 |
fun get_value context = |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
98 |
the_default default_value (Inttab.lookup (ConfigData.get context) id); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
99 |
fun map_value f = ConfigData.map (Inttab.map_default (id, default_value) f); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
100 |
val config_value = Config {get_value = get_value, map_value = map_value}; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
101 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
102 |
val _ = CRITICAL (fn () => |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
103 |
(if Symtab.defined (! global_configs) name |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
104 |
then warning ("Hiding existing configuration option " ^ quote name) else (); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
105 |
change global_configs (Symtab.update (name, (config_value, default_value))))); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
106 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
107 |
in Config {get_value = dest o get_value, map_value = fn f => map_value (make o f o dest)} end; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
108 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
109 |
end; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
110 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
111 |
val bool = declare Bool (fn Bool b => b); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
112 |
val int = declare Int (fn Int i => i); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
113 |
val string = declare String (fn String s => s); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
114 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
115 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
116 |
(*final declarations of this structure!*) |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
117 |
val get = get_ctxt; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
118 |
val map = map_ctxt; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
119 |
val put = put_ctxt; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
120 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
121 |
end; |