author | wenzelm |
Wed, 12 Mar 2025 11:39:00 +0100 | |
changeset 82265 | 4b875a4c83b0 |
parent 81557 | 8dc9453889ca |
permissions | -rw-r--r-- |
28019 | 1 |
(* Title: Pure/General/properties.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Property lists. |
|
5 |
*) |
|
6 |
||
7 |
signature PROPERTIES = |
|
8 |
sig |
|
50842 | 9 |
type entry = string * string |
10 |
type T = entry list |
|
80504 | 11 |
val print_eq: entry -> string |
71465
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
51665
diff
changeset
|
12 |
val entry_ord: entry ord |
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
51665
diff
changeset
|
13 |
val ord: T ord |
28019 | 14 |
val defined: T -> string -> bool |
15 |
val get: T -> string -> string option |
|
50842 | 16 |
val put: entry -> T -> T |
28019 | 17 |
val remove: string -> T -> T |
77777 | 18 |
val make_string: string -> string -> T |
19 |
val make_int: string -> int -> T |
|
77772 | 20 |
val get_string: T -> string -> string |
81557 | 21 |
val get_bool: T -> string -> bool |
77772 | 22 |
val get_int: T -> string -> int |
23 |
val get_seconds: T -> string -> Time.time |
|
28019 | 24 |
end; |
25 |
||
26 |
structure Properties: PROPERTIES = |
|
27 |
struct |
|
28 |
||
50842 | 29 |
type entry = string * string; |
80504 | 30 |
|
50842 | 31 |
type T = entry list; |
28019 | 32 |
|
80504 | 33 |
fun print_eq (a, b) = a ^ "=" ^ b; |
34 |
||
71465
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
51665
diff
changeset
|
35 |
val entry_ord = prod_ord string_ord string_ord; |
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
51665
diff
changeset
|
36 |
val ord = list_ord entry_ord; |
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
51665
diff
changeset
|
37 |
|
28019 | 38 |
fun defined (props: T) name = AList.defined (op =) props name; |
39 |
fun get (props: T) name = AList.lookup (op =) props name; |
|
43780 | 40 |
fun put entry (props: T) = AList.update (op =) entry props; |
28019 | 41 |
fun remove name (props: T) = AList.delete (op =) name props; |
42 |
||
77777 | 43 |
fun make_string k s = if s = "" then [] else [(k, s)]; |
44 |
fun make_int k i = if i = 0 then [] else [(k, Value.print_int i)]; |
|
45 |
||
77772 | 46 |
val get_string = the_default "" oo get; |
47 |
||
81557 | 48 |
fun get_bool props name = |
49 |
(case get props name of |
|
50 |
NONE => false |
|
51 |
| SOME s => Value.parse_bool s); |
|
52 |
||
77772 | 53 |
fun get_int props name = |
54 |
(case get props name of |
|
55 |
NONE => 0 |
|
56 |
| SOME s => Value.parse_int s); |
|
57 |
||
58 |
fun get_seconds props name = |
|
59 |
(case get props name of |
|
51665 | 60 |
NONE => Time.zeroTime |
61 |
| SOME s => Time.fromReal (the_default 0.0 (Real.fromString s))); |
|
62 |
||
28019 | 63 |
end; |