author | wenzelm |
Wed, 25 Jul 2007 22:20:49 +0200 | |
changeset 23987 | 6d78feed74dd |
child 24001 | 067d8e589c58 |
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 |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
11 |
type 'a T |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
12 |
val get: Proof.context -> 'a T -> 'a |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
13 |
val get_thy: theory -> 'a T -> 'a |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
14 |
val get_generic: Context.generic -> 'a T -> 'a |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
15 |
val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
16 |
val map_thy: 'a T -> ('a -> 'a) -> theory -> theory |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
17 |
val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
18 |
val put: 'a T -> 'a -> Proof.context -> Proof.context |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
19 |
val put_thy: 'a T -> 'a -> theory -> theory |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
20 |
val put_generic: 'a T -> 'a -> Context.generic -> Context.generic |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
21 |
val put_generic_src: string -> string -> Context.generic -> Context.generic |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
22 |
val print_configs: Proof.context -> unit |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
23 |
val bool: string -> bool -> bool T |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
24 |
val int: string -> int -> int T |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
25 |
val string: string -> string -> string T |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
26 |
end; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
27 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
28 |
structure Config: CONFIG = |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
29 |
struct |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
30 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
31 |
(* abstract configuration options *) |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
32 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
33 |
datatype 'a T = Config of |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
34 |
{get_value: Context.generic -> 'a, |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
35 |
map_value: ('a -> 'a) -> Context.generic -> Context.generic}; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
36 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
37 |
fun get_generic context (Config {get_value, ...}) = get_value context; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
38 |
fun get_ctxt ctxt = get_generic (Context.Proof ctxt); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
39 |
fun get_thy thy = get_generic (Context.Theory thy); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
40 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
41 |
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
|
42 |
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
|
43 |
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
|
44 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
45 |
fun put_generic config value = map_generic config (K value); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
46 |
fun put_ctxt config value = map_ctxt config (K value); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
47 |
fun put_thy config value = map_thy config (K value); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
48 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
49 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
50 |
(* mixed values *) |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
51 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
52 |
datatype value = |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
53 |
Bool of bool | |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
54 |
Int of int | |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
55 |
String of string; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
56 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
57 |
fun read_value (Bool _) "true" = SOME (Bool true) |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
58 |
| read_value (Bool _) "false" = SOME (Bool false) |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
59 |
| read_value (Int _) s = Option.map Int (Syntax.read_int s) |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
60 |
| read_value (String _) s = SOME (String s); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
61 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
62 |
fun print_value (Bool true) = "true" |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
63 |
| print_value (Bool false) = "false" |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
64 |
| print_value (Int i) = signed_string_of_int i |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
65 |
| print_value (String s) = quote s; |
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 print_type (Bool _) = "boolean" |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
68 |
| print_type (Int _) = "integer" |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
69 |
| print_type (String _) = "string"; |
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 |
structure ConfigData = GenericDataFun |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
72 |
( |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
73 |
type T = value Inttab.table; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
74 |
val empty = Inttab.empty; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
75 |
val extend = I; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
76 |
fun merge _ = Inttab.merge (K true); |
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 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
79 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
80 |
(* global declarations *) |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
81 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
82 |
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
|
83 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
84 |
fun put_generic_src name src_value context = |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
85 |
(case Symtab.lookup (! global_configs) name of |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
86 |
NONE => error ("Unknown configuration option " ^ quote name) |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
87 |
| SOME (config, default) => |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
88 |
(case read_value default src_value of |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
89 |
SOME value => put_generic config value context |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
90 |
| NONE => error ("Malformed " ^ print_type default ^ |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
91 |
" value for configuration option " ^ quote name))); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
92 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
93 |
fun declare make dest name default = |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
94 |
let |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
95 |
val id = serial (); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
96 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
97 |
val default_value = make default; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
98 |
fun get_value context = |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
99 |
the_default default_value (Inttab.lookup (ConfigData.get context) id); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
100 |
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
|
101 |
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
|
102 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
103 |
val _ = CRITICAL (fn () => |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
104 |
(if Symtab.defined (! global_configs) name |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
105 |
then warning ("Hiding existing configuration option " ^ quote name) else (); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
106 |
change global_configs (Symtab.update (name, (config_value, default_value))))); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
107 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
108 |
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
|
109 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
110 |
fun print_configs ctxt = |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
111 |
let |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
112 |
fun prt (name, (config, default)) = |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
113 |
Pretty.block [Pretty.str (name ^ ": " ^ print_type default ^ " ="), Pretty.brk 1, |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
114 |
Pretty.str (print_value (get_ctxt ctxt config))]; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
115 |
val configs = sort_wrt #1 (Symtab.dest (! global_configs)); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
116 |
in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
117 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
118 |
end; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
119 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
120 |
val bool = declare Bool (fn Bool b => b); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
121 |
val int = declare Int (fn Int i => i); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
122 |
val string = declare String (fn String s => s); |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
123 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
124 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
125 |
(*final declarations of this structure!*) |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
126 |
val get = get_ctxt; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
127 |
val map = map_ctxt; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
128 |
val put = put_ctxt; |
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
129 |
|
6d78feed74dd
Configuration options as values within the local context.
wenzelm
parents:
diff
changeset
|
130 |
end; |