src/Pure/General/properties.ML
author wenzelm
Wed, 12 Mar 2025 11:39:00 +0100
changeset 82265 4b875a4c83b0
parent 81557 8dc9453889ca
permissions -rw-r--r--
update for release;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28019
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/properties.ML
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
     3
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
     4
Property lists.
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
     5
*)
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
     6
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
     7
signature PROPERTIES =
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
     8
sig
50842
777c6026ca93 tuned signature;
wenzelm
parents: 46830
diff changeset
     9
  type entry = string * string
777c6026ca93 tuned signature;
wenzelm
parents: 46830
diff changeset
    10
  type T = entry list
80504
7ea69c26524b tuned signature: more operations;
wenzelm
parents: 77777
diff changeset
    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
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    14
  val defined: T -> string -> bool
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    15
  val get: T -> string -> string option
50842
777c6026ca93 tuned signature;
wenzelm
parents: 46830
diff changeset
    16
  val put: entry -> T -> T
28019
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    17
  val remove: string -> T -> T
77777
13cee8c2ed8d clarified signature;
wenzelm
parents: 77772
diff changeset
    18
  val make_string: string -> string -> T
13cee8c2ed8d clarified signature;
wenzelm
parents: 77772
diff changeset
    19
  val make_int: string -> int -> T
77772
7e0d920b4e6e tuned signature;
wenzelm
parents: 71465
diff changeset
    20
  val get_string: T -> string -> string
81557
8dc9453889ca tuned signature: more operations;
wenzelm
parents: 80504
diff changeset
    21
  val get_bool: T -> string -> bool
77772
7e0d920b4e6e tuned signature;
wenzelm
parents: 71465
diff changeset
    22
  val get_int: T -> string -> int
7e0d920b4e6e tuned signature;
wenzelm
parents: 71465
diff changeset
    23
  val get_seconds: T -> string -> Time.time
28019
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    24
end;
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    25
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    26
structure Properties: PROPERTIES =
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    27
struct
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    28
50842
777c6026ca93 tuned signature;
wenzelm
parents: 46830
diff changeset
    29
type entry = string * string;
80504
7ea69c26524b tuned signature: more operations;
wenzelm
parents: 77777
diff changeset
    30
50842
777c6026ca93 tuned signature;
wenzelm
parents: 46830
diff changeset
    31
type T = entry list;
28019
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    32
80504
7ea69c26524b tuned signature: more operations;
wenzelm
parents: 77777
diff changeset
    33
fun print_eq (a, b) = a ^ "=" ^ b;
7ea69c26524b tuned signature: more operations;
wenzelm
parents: 77777
diff changeset
    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
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    38
fun defined (props: T) name = AList.defined (op =) props name;
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    39
fun get (props: T) name = AList.lookup (op =) props name;
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 29606
diff changeset
    40
fun put entry (props: T) = AList.update (op =) entry props;
28019
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    41
fun remove name (props: T) = AList.delete (op =) name props;
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    42
77777
13cee8c2ed8d clarified signature;
wenzelm
parents: 77772
diff changeset
    43
fun make_string k s = if s = "" then [] else [(k, s)];
13cee8c2ed8d clarified signature;
wenzelm
parents: 77772
diff changeset
    44
fun make_int k i = if i = 0 then [] else [(k, Value.print_int i)];
13cee8c2ed8d clarified signature;
wenzelm
parents: 77772
diff changeset
    45
77772
7e0d920b4e6e tuned signature;
wenzelm
parents: 71465
diff changeset
    46
val get_string = the_default "" oo get;
7e0d920b4e6e tuned signature;
wenzelm
parents: 71465
diff changeset
    47
81557
8dc9453889ca tuned signature: more operations;
wenzelm
parents: 80504
diff changeset
    48
fun get_bool props name =
8dc9453889ca tuned signature: more operations;
wenzelm
parents: 80504
diff changeset
    49
  (case get props name of
8dc9453889ca tuned signature: more operations;
wenzelm
parents: 80504
diff changeset
    50
    NONE => false
8dc9453889ca tuned signature: more operations;
wenzelm
parents: 80504
diff changeset
    51
  | SOME s => Value.parse_bool s);
8dc9453889ca tuned signature: more operations;
wenzelm
parents: 80504
diff changeset
    52
77772
7e0d920b4e6e tuned signature;
wenzelm
parents: 71465
diff changeset
    53
fun get_int props name =
7e0d920b4e6e tuned signature;
wenzelm
parents: 71465
diff changeset
    54
  (case get props name of
7e0d920b4e6e tuned signature;
wenzelm
parents: 71465
diff changeset
    55
    NONE => 0
7e0d920b4e6e tuned signature;
wenzelm
parents: 71465
diff changeset
    56
  | SOME s => Value.parse_int s);
7e0d920b4e6e tuned signature;
wenzelm
parents: 71465
diff changeset
    57
7e0d920b4e6e tuned signature;
wenzelm
parents: 71465
diff changeset
    58
fun get_seconds props name =
7e0d920b4e6e tuned signature;
wenzelm
parents: 71465
diff changeset
    59
  (case get props name of
51665
cba83c9f72b9 tuned signature;
wenzelm
parents: 50842
diff changeset
    60
    NONE => Time.zeroTime
cba83c9f72b9 tuned signature;
wenzelm
parents: 50842
diff changeset
    61
  | SOME s => Time.fromReal (the_default 0.0 (Real.fromString s)));
cba83c9f72b9 tuned signature;
wenzelm
parents: 50842
diff changeset
    62
28019
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    63
end;