<commit_before>(*  Title:      Pure/System/options.ML
    Author:     Makarius

Stand-alone options with external string representation.
*)

signature OPTIONS =
sig
  type T
  val empty: T
  val typ: T -> string -> string
  val bool: T -> string -> bool
  val int: T -> string -> int
  val real: T -> string -> real
  val string: T -> string -> string
  val declare: {name: string, typ: string, value: string} -> T -> T
  val decode: XML.body -> T
  val default: unit -> T
  val default_bool: string -> bool
  val default_int: string -> int
  val default_real: string -> real
  val default_string: string -> string
  val set_default: T -> unit
  val reset_default: unit -> unit
  val load_default: unit -> unit
end;

structure Options: OPTIONS =
struct

(* representation *)

val boolT = "bool";
val intT = "int";
val realT = "real";
val stringT = "string";

datatype T = Options of {typ: string, value: string} Symtab.table;

val empty = Options Symtab.empty;


(* typ *)

fun typ (Options tab) name =
  (case Symtab.lookup tab name of
    SOME opt => #typ opt
  | NONE => error ("Unknown option " ^ quote name));


(* get *)

fun get T parse (Options tab) name =
  (case Symtab.lookup tab name of
    SOME {typ, value} =>
      if typ = T then
        (case parse value of
          SOME x => x
        | NONE =>
            error ("Malformed value for option " ^ quote name ^ " : " ^ T ^ " =\n" ^ quote value))
      else error ("Ill-typed option " ^ quote name ^ " : " ^ typ ^ " vs. " ^ T)
  | NONE => error ("Unknown option " ^ quote name));

val bool = get boolT Bool.fromString;
val int = get intT Int.fromString;
val real = get realT Real.fromString;
val string = get stringT SOME;


(* declare *)

fun declare {name, typ, value} (Options tab) =
  let
    val check_value =
      if typ = boolT then ignore oo bool
      else if typ = intT then ignore oo int
      else if typ = realT then ignore oo real
      else if typ = stringT then ignore oo string
      else error ("Unknown type for option " ^ quote name ^ " : " ^ quote typ);
    val options' = Options (Symtab.update_new (name, {typ = typ, value = value}) tab)
      handle Symtab.DUP _ => error ("Duplicate declaration of option " ^ quote name);
    val _ = check_value options' name;
  in options' end;


(* decode *)

fun decode body =
  fold (declare o (fn (name, typ, value) => {name = name, typ = typ, value = value}))
    (let open XML.Decode in list (triple string string string) end body) empty;



(** global default **)

val global_default = Synchronized.var "Options.default" (NONE: T option);

fun default () =
  (case Synchronized.value global_default of
    SOME options => options
  | NONE => error "No global default options");

fun default_bool name = bool (default ()) name;
fun default_int name = int (default ()) name;
fun default_real name = real (default ()) name;
fun default_string name = string (default ()) name;

fun set_default options = Synchronized.change global_default (K (SOME options));
fun reset_default () = Synchronized.change global_default (K NONE);

fun load_default () =
  (case getenv "ISABELLE_PROCESS_OPTIONS" of
    "" => ()
  | name =>
      let val path = Path.explode name in
        (case try File.read path of
          SOME s => (set_default (decode (YXML.parse_body s)); ignore (try File.rm path))
        | NONE => ())
      end);

val _ = load_default ();

end;<commit_msg>more operations in accordance to Scala version;<commit_after>(*  Title:      Pure/System/options.ML
    Author:     Makarius

Stand-alone options with external string representation.
*)

signature OPTIONS =
sig
  val boolT: string
  val intT: string
  val realT: string
  val stringT: string
  val unknownT: string
  type T
  val empty: T
  val typ: T -> string -> string
  val bool: T -> string -> bool
  val int: T -> string -> int
  val real: T -> string -> real
  val string: T -> string -> string
  val put_bool: string -> bool -> T -> T
  val put_int: string -> int -> T -> T
  val put_real: string -> real -> T -> T
  val put_string: string -> string -> T -> T
  val declare: {name: string, typ: string, value: string} -> T -> T
  val update: string -> string -> T -> T
  val decode: XML.body -> T
  val default: unit -> T
  val default_bool: string -> bool
  val default_int: string -> int
  val default_real: string -> real
  val default_string: string -> string
  val default_put_bool: string -> bool -> unit
  val default_put_int: string -> int -> unit
  val default_put_real: string -> real -> unit
  val default_put_string: string -> string -> unit
  val get_default: string -> string
  val put_default: string -> string -> unit
  val set_default: T -> unit
  val reset_default: unit -> unit
  val load_default: unit -> unit
end;

structure Options: OPTIONS =
struct

(* representation *)

val boolT = "bool";
val intT = "int";
val realT = "real";
val stringT = "string";
val unknownT = "unknown";

datatype T = Options of {typ: string, value: string} Symtab.table;

val empty = Options Symtab.empty;


(* check *)

fun check_name (Options tab) name =
  let val opt = Symtab.lookup tab name in
    if is_some opt andalso #typ (the opt) <> unknownT then the opt
    else error ("Unknown option " ^ quote name)
  end;

fun check_type options name typ =
  let val opt = check_name options name in
    if #typ opt = typ then opt
    else error ("Ill-typed option " ^ quote name ^ " : " ^ #typ opt ^ " vs. " ^ typ)
  end;


(* typ *)

fun typ options name = #typ (check_name options name);


(* basic operations *)

fun put T print name x (options as Options tab) =
  let val opt = check_type options name T
  in Options (Symtab.update (name, {typ = #typ opt, value = print x}) tab) end;

fun get T parse options name =
  let val opt = check_type options name T in
    (case parse (#value opt) of
      SOME x => x
    | NONE =>
        error ("Malformed value for option " ^ quote name ^
          " : " ^ T ^ " =\n" ^ quote (#value opt)))
  end;


(* internal lookup and update *)

val bool = get boolT Bool.fromString;
val int = get intT Int.fromString;
val real = get realT Real.fromString;
val string = get stringT SOME;

val put_bool = put boolT Bool.toString;
val put_int = put intT signed_string_of_int;
val put_real = put realT signed_string_of_real;
val put_string = put stringT I;


(* external updates *)

fun check_value options name =
  let val opt = check_name options name in
    if #typ opt = boolT then ignore (bool options name)
    else if #typ opt = intT then ignore (int options name)
    else if #typ opt = realT then ignore (real options name)
    else if #typ opt = stringT then ignore (string options name)
    else ()
  end;

fun declare {name, typ, value} (Options tab) =
  let
    val options' = Options (Symtab.update_new (name, {typ = typ, value = value}) tab)
      handle Symtab.DUP _ => error ("Duplicate declaration of option " ^ quote name);
    val _ =
      typ = boolT orelse typ = intT orelse typ = realT orelse typ = stringT orelse
        error ("Unknown type for option " ^ quote name ^ " : " ^ quote typ);
    val _ = check_value options' name;
  in options' end;

fun update name value (options as Options tab) =
  let
    val opt = check_name options name;
    val options' = Options (Symtab.update (name, {typ = #typ opt, value = value}) tab);
    val _ = check_value options' name;
  in options' end;


(* decode *)

fun decode body =
  fold (declare o (fn (name, typ, value) => {name = name, typ = typ, value = value}))
    (let open XML.Decode in list (triple string string string) end body) empty;



(** global default **)

val global_default = Synchronized.var "Options.default" (NONE: T option);

fun err_no_default () = error "No global default options";

fun change_default f x y =
  Synchronized.change global_default
    (fn SOME options => SOME (f x y options)
      | NONE => err_no_default ());

fun default () =
  (case Synchronized.value global_default of
    SOME options => options
  | NONE => err_no_default ());

fun default_bool name = bool (default ()) name;
fun default_int name = int (default ()) name;
fun default_real name = real (default ()) name;
fun default_string name = string (default ()) name;

val default_put_bool = change_default put_bool;
val default_put_int = change_default put_int;
val default_put_real = change_default put_real;
val default_put_string = change_default put_string;

fun get_default name =
  let val options = default () in get (typ options name) SOME options name end;
val put_default = change_default update;

fun set_default options = Synchronized.change global_default (K (SOME options));
fun reset_default () = Synchronized.change global_default (K NONE);

fun load_default () =
  (case getenv "ISABELLE_PROCESS_OPTIONS" of
    "" => ()
  | name =>
      let val path = Path.explode name in
        (case try File.read path of
          SOME s => (set_default (decode (YXML.parse_body s)); ignore (try File.rm path))
        | NONE => ())
      end);

val _ = load_default ();

end;
{'fraction_non_alphanumeric': 0.11107404936624417, 'fraction_numerical': 0.0, 'mean_word_length': 3.0960837887067396, 'pattern_counts': {'":': 0, '<': 4, '<?xml version=': 0, '>': 98, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 1, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '328878', 'n_tokens_mistral': 2821, 'n_tokens_neox': 2787, 'n_words': 1123}