# HG changeset patch # User wenzelm # Date 1167491280 -3600 # Node ID 279b129498b6f609633e9e639ddcfa6c605c43eb # Parent 8d34e64eeaf631e622edf829a254b85a33e74cef removed conditional combinator; diff -r 8d34e64eeaf6 -r 279b129498b6 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Sat Dec 30 12:41:59 2006 +0100 +++ b/src/HOL/Tools/record_package.ML Sat Dec 30 16:08:00 2006 +0100 @@ -475,6 +475,7 @@ val get_fieldext = Symtab.lookup o #fieldext o RecordsData.get; + (* parent records *) fun add_parents thy NONE parents = parents @@ -490,6 +491,7 @@ fun bad_inst ((x, S), T) = if Sign.of_sort sign (T, S) then NONE else SOME x val bads = List.mapPartial bad_inst (args ~~ types); + val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in"); val inst = map fst args ~~ types; val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst); @@ -497,13 +499,12 @@ val fields' = map (apsnd subst) fields; val extension' = apsnd (map subst) extension; in - conditional (not (null bads)) (fn () => - err ("Ill-sorted instantiation of " ^ commas bads ^ " in")); add_parents thy parent' - (make_parent_info name fields' extension' induct::parents) + (make_parent_info name fields' extension' induct :: parents) end; + (** concrete syntax for records **) (* parse translations *) diff -r 8d34e64eeaf6 -r 279b129498b6 src/HOL/ex/svc_funcs.ML --- a/src/HOL/ex/svc_funcs.ML Sat Dec 30 12:41:59 2006 +0100 +++ b/src/HOL/ex/svc_funcs.ML Sat Dec 30 16:08:00 2006 +0100 @@ -243,8 +243,7 @@ (*The oracle proves the given formula t, if possible*) fun oracle thy t = - (conditional (! trace) (fn () => - tracing ("SVC oracle: problem is\n" ^ Sign.string_of_term thy t)); - if valid (expr_of false t) then t else fail t); + (if ! trace then tracing ("SVC oracle: problem is\n" ^ Sign.string_of_term thy t) else (); + if valid (expr_of false t) then t else fail t); end; diff -r 8d34e64eeaf6 -r 279b129498b6 src/Pure/General/file.ML --- a/src/Pure/General/file.ML Sat Dec 30 12:41:59 2006 +0100 +++ b/src/Pure/General/file.ML Sat Dec 30 16:08:00 2006 +0100 @@ -137,12 +137,15 @@ SOME ids => OS.FileSys.compare ids = EQUAL | NONE => false); -fun copy src dst = conditional (not (eq (src, dst))) (fn () => - let val target = if is_dir dst then Path.append dst (Path.base src) else dst - in write target (read src) end); +fun copy src dst = + if eq (src, dst) then () + else + let val target = if is_dir dst then Path.append dst (Path.base src) else dst + in write target (read src) end; -fun copy_dir src dst = conditional (not (eq (src, dst))) (fn () => - (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ())) +fun copy_dir src dst = + if eq (src, dst) then () + else (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ()); (* use ML files *) diff -r 8d34e64eeaf6 -r 279b129498b6 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Sat Dec 30 12:41:59 2006 +0100 +++ b/src/Pure/General/name_space.ML Sat Dec 30 16:08:00 2006 +0100 @@ -232,11 +232,11 @@ if is_hidden name then error ("Attempt to declare hidden name " ^ quote name) else - let val names = explode_name name in - conditional (null names orelse exists (fn s => s = "") names) (fn () => - error ("Bad name declaration " ^ quote name)); - fold (add_name name) (map implode_name (accs names)) space - end; + let + val names = explode_name name; + val _ = (null names orelse exists (fn s => s = "") names) andalso + error ("Bad name declaration " ^ quote name); + in fold (add_name name) (map implode_name (accs names)) space end; (* manipulate namings *) diff -r 8d34e64eeaf6 -r 279b129498b6 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Sat Dec 30 12:41:59 2006 +0100 +++ b/src/Pure/Isar/locale.ML Sat Dec 30 16:08:00 2006 +0100 @@ -1070,10 +1070,10 @@ val th = abstract_thm (ProofContext.theory_of ctxt) eq; fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)]; in - conditional (exists (equal y o #1) xs) (fn () => - err "Attempt to define previously specified variable"); - conditional (exists (fn (Free (y', _), _) => y = y' | _ => false) env) (fn () => - err "Attempt to redefine variable"); + exists (equal y o #1) xs andalso + err "Attempt to define previously specified variable"; + exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso + err "Attempt to redefine variable"; (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths) end; @@ -1763,8 +1763,8 @@ do_predicate bname raw_import raw_body thy = let val name = Sign.full_name thy bname; - val _ = conditional (is_some (get_locale thy name)) (fn () => - error ("Duplicate definition of locale " ^ quote name)); + val _ = is_some (get_locale thy name) andalso + error ("Duplicate definition of locale " ^ quote name); val thy_ctxt = ProofContext.init thy; val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)), diff -r 8d34e64eeaf6 -r 279b129498b6 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Sat Dec 30 12:41:59 2006 +0100 +++ b/src/Pure/Isar/method.ML Sat Dec 30 16:08:00 2006 +0100 @@ -246,9 +246,10 @@ val trace_rules = ref false; fun trace ctxt rules = - conditional (! trace_rules andalso not (null rules)) (fn () => + if ! trace_rules andalso not (null rules) then Pretty.big_list "rules:" (map (ProofContext.pretty_thm ctxt) rules) - |> Pretty.string_of |> tracing); + |> Pretty.string_of |> tracing + else (); local diff -r 8d34e64eeaf6 -r 279b129498b6 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Sat Dec 30 12:41:59 2006 +0100 +++ b/src/Pure/Isar/toplevel.ML Sat Dec 30 16:08:00 2006 +0100 @@ -661,8 +661,9 @@ fun app int (tr as Transition {trans, int_only, print, no_timing, ...}) state = let - val _ = conditional (not int andalso int_only) (fn () => - warning (command_msg "Interactive-only " tr)); + val _ = + if not int andalso int_only then warning (command_msg "Interactive-only " tr) + else (); fun do_timing f x = (Output.info (command_msg "" tr); timeap f x); fun do_profiling f x = profile (! profiling) f x; @@ -671,9 +672,9 @@ state |> (apply_trans int trans |> (if ! profiling > 0 then do_profiling else I) |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I)); - val _ = conditional (int andalso not (! quiet) andalso - exists (member (op =) print) ("" :: ! print_mode)) - (fn () => print_state false result); + val _ = + if int andalso not (! quiet) andalso exists (member (op =) print) ("" :: ! print_mode) + then print_state false result else (); in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) opt_exn) end; in diff -r 8d34e64eeaf6 -r 279b129498b6 src/Pure/Syntax/ast.ML --- a/src/Pure/Syntax/ast.ML Sat Dec 30 12:41:59 2006 +0100 +++ b/src/Pure/Syntax/ast.ML Sat Dec 30 16:08:00 2006 +0100 @@ -205,8 +205,9 @@ | rewrite ast = try_headless_rules ast; fun rewrote old_ast new_ast = - conditional trace (fn () => - tracing ("rewrote: " ^ str_of_ast old_ast ^ " -> " ^ str_of_ast new_ast)); + if trace then + tracing ("rewrote: " ^ str_of_ast old_ast ^ " -> " ^ str_of_ast new_ast) + else (); fun norm_root ast = (case rewrite ast of @@ -234,17 +235,16 @@ end; - val _ = conditional trace (fn () => tracing ("pre: " ^ str_of_ast pre_ast)); - + val _ = if trace then tracing ("pre: " ^ str_of_ast pre_ast) else (); val post_ast = normal pre_ast; - in - conditional (trace orelse stat) (fn () => - tracing ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^ - string_of_int (! passes) ^ " passes, " ^ - string_of_int (! changes) ^ " changes, " ^ - string_of_int (! failed_matches) ^ " matches failed")); - post_ast - end; + val _ = + if trace orelse stat then + tracing ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^ + string_of_int (! passes) ^ " passes, " ^ + string_of_int (! changes) ^ " changes, " ^ + string_of_int (! failed_matches) ^ " matches failed") + else (); + in post_ast end; (* normalize_ast *) diff -r 8d34e64eeaf6 -r 279b129498b6 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Sat Dec 30 12:41:59 2006 +0100 +++ b/src/Pure/Syntax/syntax.ML Sat Dec 30 16:08:00 2006 +0100 @@ -394,11 +394,12 @@ fun show_pt pt = Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts ctxt (K NONE) [pt]))); in - conditional (length pts > ! ambiguity_level) (fn () => + if length pts > ! ambiguity_level then if ! ambiguity_is_error then error ("Ambiguous input " ^ quote str) else (warning ("Ambiguous input " ^ quote str ^ "\n" ^ "produces " ^ string_of_int (length pts) ^ " parse trees."); - List.app (warning o show_pt) pts)); + List.app (warning o show_pt) pts) + else (); SynTrans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts end; diff -r 8d34e64eeaf6 -r 279b129498b6 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Sat Dec 30 12:41:59 2006 +0100 +++ b/src/Pure/Thy/present.ML Sat Dec 30 16:08:00 2006 +0100 @@ -305,8 +305,8 @@ val (doc_prefix1, documents) = if doc = "" then (NONE, []) - else if not (File.exists document_path) then (conditional verbose (fn () => - std_error "Warning: missing document directory\n"); (NONE, [])) + else if not (File.exists document_path) then + (if verbose then std_error "Warning: missing document directory\n" else (); (NONE, [])) else (SOME (Path.append html_prefix document_path, html_prefix), read_versions doc_versions); @@ -341,10 +341,10 @@ " 2>&1" ^ (if verbose then "" else " >/dev/null"); val doc_path = Path.append result_path (Path.ext format (Path.basic name)); in - conditional verbose (fn () => writeln s); + if verbose then writeln s else (); system s; - conditional (not (File.exists doc_path)) (fn () => - error ("No document: " ^ quote (show_path doc_path))); + File.exists doc_path orelse + error ("No document: " ^ quote (show_path doc_path)); doc_path end; @@ -399,7 +399,7 @@ write_tex_index tex_index path; List.app (finish_tex path) thys); in - conditional info (fn () => + if info then (File.mkdir (Path.append html_prefix session_path); Buffer.write (Path.append html_prefix pre_index_path) html_index; File.write (Path.append html_prefix session_entries_path) ""; @@ -413,12 +413,12 @@ File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix; List.app finish_html thys; List.app (uncurry File.write) files; - conditional verbose (fn () => - std_error ("Browser info at " ^ show_path html_prefix ^ "\n")))); + if verbose then std_error ("Browser info at " ^ show_path html_prefix ^ "\n") else ()) + else (); (case doc_prefix2 of NONE => () | SOME (cp, path) => (prepare_sources cp path; - conditional verbose (fn () => std_error ("Document sources at " ^ show_path path ^ "\n")))); + if verbose then std_error ("Document sources at " ^ show_path path ^ "\n") else ())); (case doc_prefix1 of NONE => () | SOME (path, result_path) => documents |> List.app (fn (name, tags) => @@ -426,7 +426,7 @@ val _ = prepare_sources true path; val doc_path = isatool_document true doc_format name tags path result_path; in - conditional verbose (fn () => std_error ("Document at " ^ show_path doc_path ^ "\n")) + if verbose then std_error ("Document at " ^ show_path doc_path ^ "\n") else () end)); browser_info := empty_browser_info; diff -r 8d34e64eeaf6 -r 279b129498b6 src/Pure/Tools/codegen_data.ML --- a/src/Pure/Tools/codegen_data.ML Sat Dec 30 12:41:59 2006 +0100 +++ b/src/Pure/Tools/codegen_data.ML Sat Dec 30 16:08:00 2006 +0100 @@ -426,8 +426,10 @@ let val k = serial (); val kind = {name = name, empty = empty, merge = merge, purge = purge}; - val _ = conditional (Datatab.exists (equal name o #name o #2) (! kinds)) (fn () => - warning ("Duplicate declaration of code data " ^ quote name)); + val _ = + if Datatab.exists (equal name o #name o #2) (! kinds) then + warning ("Duplicate declaration of code data " ^ quote name) + else (); val _ = change kinds (Datatab.update (k, kind)); in k end; diff -r 8d34e64eeaf6 -r 279b129498b6 src/Pure/context.ML --- a/src/Pure/context.ML Sat Dec 30 12:41:59 2006 +0100 +++ b/src/Pure/context.ML Sat Dec 30 16:08:00 2006 +0100 @@ -145,8 +145,10 @@ let val k = serial (); val kind = {name = name, empty = empty, copy = copy, extend = extend, merge = merge}; - val _ = conditional (Datatab.exists (equal name o #name o #2) (! kinds)) (fn () => - warning ("Duplicate declaration of theory data " ^ quote name)); + val _ = + if Datatab.exists (equal name o #name o #2) (! kinds) then + warning ("Duplicate declaration of theory data " ^ quote name) + else (); val _ = change kinds (Datatab.update (k, kind)); in k end; @@ -554,8 +556,10 @@ let val k = serial (); val kind = {name = name, init = init}; - val _ = conditional (Datatab.exists (equal name o #name o #2) (! kinds)) (fn () => - warning ("Duplicate declaration of proof data " ^ quote name)); + val _ = + if Datatab.exists (equal name o #name o #2) (! kinds) then + warning ("Duplicate declaration of proof data " ^ quote name) + else (); val _ = change kinds (Datatab.update (k, kind)); in k end; diff -r 8d34e64eeaf6 -r 279b129498b6 src/Pure/library.ML --- a/src/Pure/library.ML Sat Dec 30 12:41:59 2006 +0100 +++ b/src/Pure/library.ML Sat Dec 30 16:08:00 2006 +0100 @@ -75,7 +75,6 @@ val toggle: bool ref -> bool val change: 'a ref -> ('a -> 'a) -> unit val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c - val conditional: bool -> (unit -> unit) -> unit (*lists*) exception UnequalLengths @@ -395,11 +394,6 @@ in release result end; -(* conditional execution *) - -fun conditional b f = if b then f () else (); - - (** lists **) diff -r 8d34e64eeaf6 -r 279b129498b6 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Sat Dec 30 12:41:59 2006 +0100 +++ b/src/Pure/meta_simplifier.ML Sat Dec 30 16:08:00 2006 +0100 @@ -993,8 +993,10 @@ val b = Name.bound (#1 bounds); val (v, t') = Thm.dest_abs (SOME b) t0; val b' = #1 (Term.dest_Free (Thm.term_of v)); - val _ = conditional (b <> b') (fn () => - warning ("Simplifier: renamed bound variable " ^ quote b ^ " to " ^ quote b')); + val _ = + if b <> b' then + warning ("Simplifier: renamed bound variable " ^ quote b ^ " to " ^ quote b') + else (); val ss' = add_bound ((b', T), a) ss; val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0; in case botc skel' ss' t' of @@ -1171,18 +1173,20 @@ val debug_bounds = ref false; -fun check_bounds ss ct = conditional (! debug_bounds) (fn () => - let - val Simpset ({bounds = (_, bounds), ...}, _) = ss; - val bs = fold_aterms (fn Free (x, _) => - if Name.is_bound x andalso not (AList.defined eq_bound bounds x) - then insert (op =) x else I - | _ => I) (term_of ct) []; - in - if null bs then () - else print_term true ("Simplifier: term contains loose bounds: " ^ commas_quote bs) ss - (Thm.theory_of_cterm ct) (Thm.term_of ct) - end); +fun check_bounds ss ct = + if ! debug_bounds then + let + val Simpset ({bounds = (_, bounds), ...}, _) = ss; + val bs = fold_aterms (fn Free (x, _) => + if Name.is_bound x andalso not (AList.defined eq_bound bounds x) + then insert (op =) x else I + | _ => I) (term_of ct) []; + in + if null bs then () + else print_term true ("Simplifier: term contains loose bounds: " ^ commas_quote bs) ss + (Thm.theory_of_cterm ct) (Thm.term_of ct) + end + else (); fun rewrite_cterm mode prover raw_ss raw_ct = let @@ -1190,8 +1194,10 @@ val {thy, t, maxidx, ...} = Thm.rep_cterm ct; val ss = fallback_context thy raw_ss; val _ = inc simp_depth; - val _ = conditional (!simp_depth mod 20 = 0) (fn () => - warning ("Simplification depth " ^ string_of_int (! simp_depth))); + val _ = + if ! simp_depth mod 20 = 0 then + warning ("Simplification depth " ^ string_of_int (! simp_depth)) + else (); val _ = trace_cterm false "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" ss ct; val _ = check_bounds ss ct; val res = bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ss ct diff -r 8d34e64eeaf6 -r 279b129498b6 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Sat Dec 30 12:41:59 2006 +0100 +++ b/src/ZF/Tools/inductive_package.ML Sat Dec 30 16:08:00 2006 +0100 @@ -148,8 +148,10 @@ val big_rec_name = Sign.intern_const thy big_rec_base_name; - val dummy = conditional verbose (fn () => - writeln ((if coind then "Coind" else "Ind") ^ "uctive definition " ^ quote big_rec_name)); + val _ = + if verbose then + writeln ((if coind then "Coind" else "Ind") ^ "uctive definition " ^ quote big_rec_name) + else (); (*Forbid the inductive definition structure from clashing with a theory name. This restriction may become obsolete as ML is de-emphasized.*)