# HG changeset patch
# User wenzelm
# Date 1738753214 -3600
# Node ID d72a4ecf8c2030d353b0cf346cf522375ea2c41f
# Parent  794bf73e100f31ee5aec2d9c81b08c11339d1af7
tuned Isabelle/ML: more uniform semicolons;

diff -r 794bf73e100f -r d72a4ecf8c20 src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Wed Feb 05 11:55:51 2025 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Wed Feb 05 12:00:14 2025 +0100
@@ -63,7 +63,7 @@
 
   (*setup*)
   val print_setup: Proof.context -> unit
-end;
+end
 
 structure SMT_Config: SMT_CONFIG =
 struct
@@ -74,7 +74,7 @@
   name: string,
   class: Proof.context -> SMT_Util.class,
   avail: unit -> bool,
-  options: Proof.context -> string list}
+  options: Proof.context -> string list};
 
 structure Data = Generic_Data
 (
@@ -100,7 +100,7 @@
 
 fun set_solver_options (name, options) =
   let val opts = String.tokens (Symbol.is_ascii_blank o str) options
-  in map_solvers (Symtab.map_entry name (apsnd (K opts))) end
+  in map_solvers (Symtab.map_entry name (apsnd (K opts))) end;
 
 fun add_solver (info as {name, ...} : solver_info) context =
   if defined_solvers context name then
@@ -111,7 +111,7 @@
     |> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options"))
         (Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >>
           (Thm.declaration_attribute o K o set_solver_options o pair name))
-        ("additional command-line options for SMT solver " ^ quote name))
+        ("additional command-line options for SMT solver " ^ quote name));
 
 val all_solvers_of' = Symtab.keys o get_solvers';
 val all_solvers_of = all_solvers_of' o Context.Proof;
@@ -130,7 +130,7 @@
       if Context_Position.is_visible ctxt then
         warning ("The SMT solver " ^ quote name ^ " is not installed")
       else ()
-  | warn_solver _ _ = ()
+  | warn_solver _ _ = ();
 
 fun select_solver name context =
   if not (defined_solvers context name) then
@@ -139,79 +139,79 @@
     (warn_solver context name; put_solver name context)
   else put_solver name context;
 
-fun no_solver_err () = error "No SMT solver selected"
+fun no_solver_err () = error "No SMT solver selected";
 
 fun solver_of ctxt =
   (case get_solver ctxt of
     SOME name => name
-  | NONE => no_solver_err ())
+  | NONE => no_solver_err ());
 
 fun solver_info_of default select ctxt =
   (case get_solver ctxt of
     NONE => default ()
-  | SOME name => select (Symtab.lookup (get_solvers ctxt) name))
+  | SOME name => select (Symtab.lookup (get_solvers ctxt) name));
 
 fun solver_class_of ctxt =
   let fun class_of ({class, ...}: solver_info, _) = class ctxt
-  in solver_info_of no_solver_err (class_of o the) ctxt end
+  in solver_info_of no_solver_err (class_of o the) ctxt end;
 
 fun solver_options_of ctxt =
   let
     fun all_options NONE = []
       | all_options (SOME ({options, ...} : solver_info, opts)) =
           opts @ options ctxt
-  in solver_info_of (K []) all_options ctxt end
+  in solver_info_of (K []) all_options ctxt end;
 
 val setup_solver =
   Attrib.setup \<^binding>\<open>smt_solver\<close>
     (Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >>
       (Thm.declaration_attribute o K o select_solver))
-    "SMT solver configuration"
+    "SMT solver configuration";
 
 
 (* options *)
 
-val oracle = Attrib.setup_config_bool \<^binding>\<open>smt_oracle\<close> (K true)
-val timeout = Attrib.setup_config_real \<^binding>\<open>smt_timeout\<close> (K 0.0)
-val reconstruction_step_timeout = Attrib.setup_config_real \<^binding>\<open>smt_reconstruction_step_timeout\<close> (K 10.0)
-val random_seed = Attrib.setup_config_int \<^binding>\<open>smt_random_seed\<close> (K 1)
-val read_only_certificates = Attrib.setup_config_bool \<^binding>\<open>smt_read_only_certificates\<close> (K false)
-val verbose = Attrib.setup_config_bool \<^binding>\<open>smt_verbose\<close> (K true)
-val trace = Attrib.setup_config_bool \<^binding>\<open>smt_trace\<close> (K false)
-val trace_verit = Attrib.setup_config_bool \<^binding>\<open>smt_debug_verit\<close> (K false)
-val spy_verit_attr = Attrib.setup_config_bool \<^binding>\<open>smt_spy_verit\<close> (K false)
-val spy_z3 = Attrib.setup_config_bool \<^binding>\<open>smt_spy_z3\<close> (K false)
-val trace_arith_verit = Attrib.setup_config_bool \<^binding>\<open>smt_debug_arith_verit\<close> (K false)
-val trace_verit_compression = Attrib.setup_config_bool \<^binding>\<open>verit_compress_proofs\<close> (K true)
-val statistics = Attrib.setup_config_bool \<^binding>\<open>smt_statistics\<close> (K false)
-val monomorph_limit = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_limit\<close> (K 10)
-val monomorph_instances = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_instances\<close> (K 500)
-val explicit_application = Attrib.setup_config_int \<^binding>\<open>smt_explicit_application\<close> (K 1)
-val higher_order = Attrib.setup_config_bool \<^binding>\<open>smt_higher_order\<close> (K false)
-val native_bv = Attrib.setup_config_bool \<^binding>\<open>native_bv\<close> (K true)
-val nat_as_int = Attrib.setup_config_bool \<^binding>\<open>smt_nat_as_int\<close> (K false)
-val infer_triggers = Attrib.setup_config_bool \<^binding>\<open>smt_infer_triggers\<close> (K false)
-val debug_files = Attrib.setup_config_string \<^binding>\<open>smt_debug_files\<close> (K "")
-val sat_solver = Attrib.setup_config_string \<^binding>\<open>smt_sat_solver\<close> (K "cdclite")
-val cvc_experimental_lethe = Attrib.setup_config_bool \<^binding>\<open>smt_cvc_lethe\<close> (K false)
+val oracle = Attrib.setup_config_bool \<^binding>\<open>smt_oracle\<close> (K true);
+val timeout = Attrib.setup_config_real \<^binding>\<open>smt_timeout\<close> (K 0.0);
+val reconstruction_step_timeout = Attrib.setup_config_real \<^binding>\<open>smt_reconstruction_step_timeout\<close> (K 10.0);
+val random_seed = Attrib.setup_config_int \<^binding>\<open>smt_random_seed\<close> (K 1);
+val read_only_certificates = Attrib.setup_config_bool \<^binding>\<open>smt_read_only_certificates\<close> (K false);
+val verbose = Attrib.setup_config_bool \<^binding>\<open>smt_verbose\<close> (K true);
+val trace = Attrib.setup_config_bool \<^binding>\<open>smt_trace\<close> (K false);
+val trace_verit = Attrib.setup_config_bool \<^binding>\<open>smt_debug_verit\<close> (K false);
+val spy_verit_attr = Attrib.setup_config_bool \<^binding>\<open>smt_spy_verit\<close> (K false);
+val spy_z3 = Attrib.setup_config_bool \<^binding>\<open>smt_spy_z3\<close> (K false);
+val trace_arith_verit = Attrib.setup_config_bool \<^binding>\<open>smt_debug_arith_verit\<close> (K false);
+val trace_verit_compression = Attrib.setup_config_bool \<^binding>\<open>verit_compress_proofs\<close> (K true);
+val statistics = Attrib.setup_config_bool \<^binding>\<open>smt_statistics\<close> (K false);
+val monomorph_limit = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_limit\<close> (K 10);
+val monomorph_instances = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_instances\<close> (K 500);
+val explicit_application = Attrib.setup_config_int \<^binding>\<open>smt_explicit_application\<close> (K 1);
+val higher_order = Attrib.setup_config_bool \<^binding>\<open>smt_higher_order\<close> (K false);
+val native_bv = Attrib.setup_config_bool \<^binding>\<open>native_bv\<close> (K true);
+val nat_as_int = Attrib.setup_config_bool \<^binding>\<open>smt_nat_as_int\<close> (K false);
+val infer_triggers = Attrib.setup_config_bool \<^binding>\<open>smt_infer_triggers\<close> (K false);
+val debug_files = Attrib.setup_config_string \<^binding>\<open>smt_debug_files\<close> (K "");
+val sat_solver = Attrib.setup_config_string \<^binding>\<open>smt_sat_solver\<close> (K "cdclite");
+val cvc_experimental_lethe = Attrib.setup_config_bool \<^binding>\<open>smt_cvc_lethe\<close> (K false);
 
 
 (* diagnostics *)
 
-fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else ()
+fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else ();
 
-fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose)
-fun trace_msg ctxt = cond_trace (Config.get ctxt trace)
-fun statistics_msg ctxt = cond_trace (Config.get ctxt statistics)
+fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose);
+fun trace_msg ctxt = cond_trace (Config.get ctxt trace);
+fun statistics_msg ctxt = cond_trace (Config.get ctxt statistics);
 
-fun verit_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_verit) then ignore(x ()) else ()
-fun verit_arith_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_arith_verit) then ignore(x ()) else ()
+fun verit_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_verit) then ignore(x ()) else ();
+fun verit_arith_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_arith_verit) then ignore(x ()) else ();
 
-fun spy_verit ctxt  = Config.get ctxt spy_verit_attr
-fun spy_Z3 ctxt  = Config.get ctxt spy_z3
-fun compress_verit_proofs ctxt  = Config.get ctxt trace_verit_compression
+fun spy_verit ctxt  = Config.get ctxt spy_verit_attr;
+fun spy_Z3 ctxt  = Config.get ctxt spy_z3;
+fun compress_verit_proofs ctxt  = Config.get ctxt trace_verit_compression;
 
-fun use_lethe_proof_from_cvc ctxt  = Config.get ctxt cvc_experimental_lethe
+fun use_lethe_proof_from_cvc ctxt  = Config.get ctxt cvc_experimental_lethe;
 
 
 (* tools *)
@@ -222,9 +222,9 @@
 
 fun with_time_limit ctxt timeout_config f x =
   Timeout.apply (seconds (Config.get ctxt timeout_config)) f x
-    handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out
+    handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out;
 
-fun with_timeout ctxt = with_time_limit ctxt timeout
+fun with_timeout ctxt = with_time_limit ctxt timeout;
 
 
 (* certificates *)
@@ -241,30 +241,30 @@
   Attrib.setup \<^binding>\<open>smt_certificates\<close>
     (Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >>
       (Thm.declaration_attribute o K o select_certificates))
-    "SMT certificates configuration"
+    "SMT certificates configuration";
 
 
 (* setup *)
 
 val _ = Theory.setup (
   setup_solver #>
-  setup_certificates)
+  setup_certificates);
 
 fun print_setup ctxt =
   let
-    fun string_of_bool b = if b then "true" else "false"
+    fun string_of_bool b = if b then "true" else "false";
 
-    val names = available_solvers_of ctxt
-    val ns = if null names then ["(none)"] else sort_strings names
-    val n = the_default "(none)" (get_solver ctxt)
-    val opts = solver_options_of ctxt
+    val names = available_solvers_of ctxt;
+    val ns = if null names then ["(none)"] else sort_strings names;
+    val n = the_default "(none)" (get_solver ctxt);
+    val opts = solver_options_of ctxt;
 
-    val t = string_of_real (Config.get ctxt timeout)
+    val t = string_of_real (Config.get ctxt timeout);
 
     val certs_filename =
       (case get_certificates_path ctxt of
         SOME path => Path.print path
-      | NONE => "(disabled)")
+      | NONE => "(disabled)");
   in
     Pretty.writeln (Pretty.big_list "SMT setup:" [
       Pretty.str ("Current SMT solver: " ^ n),
@@ -276,7 +276,7 @@
       Pretty.str ("Certificates cache: " ^ certs_filename),
       Pretty.str ("Fixed certificates: " ^
         string_of_bool (Config.get ctxt read_only_certificates))])
-  end
+  end;
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>smt_status\<close>
@@ -284,4 +284,4 @@
     \and the values of SMT configuration options"
     (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
 
-end;
+end