--- a/src/HOL/Library/Code_Char.thy Tue Oct 27 16:01:38 2009 +0100
+++ b/src/HOL/Library/Code_Char.thy Tue Oct 27 16:47:27 2009 +0100
@@ -35,4 +35,28 @@
code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"
(Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
+
+definition implode :: "string \<Rightarrow> String.literal" where
+ "implode = STR"
+
+primrec explode :: "String.literal \<Rightarrow> string" where
+ "explode (STR s) = s"
+
+lemma [code]:
+ "literal_case f s = f (explode s)"
+ "literal_rec f s = f (explode s)"
+ by (cases s, simp)+
+
+code_reserved SML String
+
+code_const implode
+ (SML "String.implode")
+ (OCaml "failwith/ \"implode\"")
+ (Haskell "_")
+
+code_const explode
+ (SML "String.explode")
+ (OCaml "failwith/ \"explode\"")
+ (Haskell "_")
+
end
--- a/src/HOL/Nitpick.thy Tue Oct 27 16:01:38 2009 +0100
+++ b/src/HOL/Nitpick.thy Tue Oct 27 16:47:27 2009 +0100
@@ -28,7 +28,6 @@
typedecl bisim_iterator
-(* FIXME: use axiomatization (here and elsewhere) *)
axiomatization unknown :: 'a
and undefined_fast_The :: 'a
and undefined_fast_Eps :: 'a
--- a/src/HOL/Random.thy Tue Oct 27 16:01:38 2009 +0100
+++ b/src/HOL/Random.thy Tue Oct 27 16:47:27 2009 +0100
@@ -12,15 +12,15 @@
subsection {* Auxiliary functions *}
+fun log :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
+ "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
+
definition inc_shift :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
"inc_shift v k = (if v = k then 1 else k + 1)"
definition minus_shift :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
"minus_shift r k l = (if k < l then r + k - l else k - l)"
-fun log :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
- "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
-
subsection {* Random seeds *}
@@ -29,28 +29,19 @@
primrec "next" :: "seed \<Rightarrow> code_numeral \<times> seed" where
"next (v, w) = (let
k = v div 53668;
- v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211);
+ v' = minus_shift 2147483563 ((v mod 53668) * 40014) (k * 12211);
l = w div 52774;
- w' = minus_shift 2147483399 (40692 * (w mod 52774)) (l * 3791);
+ w' = minus_shift 2147483399 ((w mod 52774) * 40692) (l * 3791);
z = minus_shift 2147483562 v' (w' + 1) + 1
in (z, (v', w')))"
-lemma next_not_0:
- "fst (next s) \<noteq> 0"
- by (cases s) (auto simp add: minus_shift_def Let_def)
-
-primrec seed_invariant :: "seed \<Rightarrow> bool" where
- "seed_invariant (v, w) \<longleftrightarrow> 0 < v \<and> v < 9438322952 \<and> 0 < w \<and> True"
-
definition split_seed :: "seed \<Rightarrow> seed \<times> seed" where
"split_seed s = (let
(v, w) = s;
(v', w') = snd (next s);
v'' = inc_shift 2147483562 v;
- s'' = (v'', w');
- w'' = inc_shift 2147483398 w;
- s''' = (v', w'')
- in (s'', s'''))"
+ w'' = inc_shift 2147483398 w
+ in ((v'', w'), (v', w'')))"
subsection {* Base selectors *}
@@ -175,7 +166,7 @@
*}
hide (open) type seed
-hide (open) const inc_shift minus_shift log "next" seed_invariant split_seed
+hide (open) const inc_shift minus_shift log "next" split_seed
iterate range select pick select_weight
no_notation fcomp (infixl "o>" 60)
--- a/src/HOL/Statespace/state_space.ML Tue Oct 27 16:01:38 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML Tue Oct 27 16:47:27 2009 +0100
@@ -297,7 +297,7 @@
val tt' = tt |> fold upd all_names;
val activate_simproc =
- Output.no_warnings_CRITICAL
+ Output.no_warnings_CRITICAL (* FIXME !?! *)
(Simplifier.map_ss (fn ss => ss addsimprocs [distinct_simproc]));
val ctxt' =
ctxt
--- a/src/HOL/String.thy Tue Oct 27 16:01:38 2009 +0100
+++ b/src/HOL/String.thy Tue Oct 27 16:47:27 2009 +0100
@@ -155,7 +155,7 @@
datatype literal = STR string
-lemmas [code del] = literal.recs literal.cases
+declare literal.cases [code del] literal.recs [code del]
lemma [code]: "size (s\<Colon>literal) = 0"
by (cases s) simp_all
@@ -168,6 +168,9 @@
use "Tools/string_code.ML"
+code_reserved SML string
+code_reserved OCaml string
+
code_type literal
(SML "string")
(OCaml "string")
@@ -185,9 +188,6 @@
(OCaml "!((_ : string) = _)")
(Haskell infixl 4 "==")
-code_reserved SML string
-code_reserved OCaml string
-
types_code
"char" ("string")
--- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Oct 27 16:01:38 2009 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Oct 27 16:47:27 2009 +0100
@@ -157,6 +157,7 @@
type raw_bound = n_ary_index * int list list
datatype outcome =
+ NotInstalled |
Normal of (int * raw_bound list) list * int list |
TimedOut of int list |
Interrupted of int list option |
@@ -301,6 +302,7 @@
type raw_bound = n_ary_index * int list list
datatype outcome =
+ NotInstalled |
Normal of (int * raw_bound list) list * int list |
TimedOut of int list |
Interrupted of int list option |
@@ -1069,6 +1071,10 @@
if null ps then
if code = 2 then
TimedOut js
+ else if first_error |> Substring.full
+ |> Substring.position "NoClassDefFoundError" |> snd
+ |> Substring.isEmpty |> not then
+ NotInstalled
else if first_error <> "" then
Error (first_error |> perhaps (try (unsuffix "."))
|> perhaps (try (unprefix "Error: ")), js)
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Oct 27 16:01:38 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Oct 27 16:47:27 2009 +0100
@@ -626,7 +626,18 @@
else
case Kodkod.solve_any_problem overlord deadline max_threads
max_solutions (map fst problems) of
- Kodkod.Normal ([], unsat_js) =>
+ Kodkod.NotInstalled =>
+ (print_m (fn () =>
+ "Nitpick requires the external Java program Kodkodi. \
+ \To install it, download the package from Isabelle's \
+ \web page and add the \"kodkodi-x.y.z\" directory's \
+ \full path to \"" ^
+ Path.implode (Path.expand (Path.appends
+ (Path.variable "ISABELLE_HOME" ::
+ (map Path.basic ["etc", "components"])))) ^
+ "\".");
+ (max_potential, max_genuine, donno + 1))
+ | Kodkod.Normal ([], unsat_js) =>
(update_checked_problems problems unsat_js;
(max_potential, max_genuine, donno))
| Kodkod.Normal (sat_ps, unsat_js) =>
@@ -785,7 +796,7 @@
(* int -> int -> scope list -> int * int * int -> Kodkod.outcome *)
fun run_batches _ _ [] (max_potential, max_genuine, donno) =
if donno > 0 andalso max_genuine > 0 then
- (print_m (fn () => excipit "ran out of resources"); "unknown")
+ (print_m (fn () => excipit "ran into difficulties"); "unknown")
else if max_genuine = original_max_genuine then
if max_potential = original_max_potential then
(print_m (K ("Nitpick found no " ^ word_model ^ ".")); "none")
--- a/src/HOL/Tools/meson.ML Tue Oct 27 16:01:38 2009 +0100
+++ b/src/HOL/Tools/meson.ML Tue Oct 27 16:47:27 2009 +0100
@@ -323,7 +323,7 @@
Strips universal quantifiers and breaks up conjunctions.
Eliminates existential quantifiers using skoths: Skolemization theorems.*)
fun cnf skoths ctxt (th,ths) =
- let val ctxtr = Unsynchronized.ref ctxt
+ let val ctxtr = Unsynchronized.ref ctxt (* FIXME ??? *)
fun cnf_aux (th,ths) =
if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
else if not (has_conns ["All","Ex","op &"] (prop_of th))
--- a/src/HOL/Tools/res_axioms.ML Tue Oct 27 16:01:38 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML Tue Oct 27 16:47:27 2009 +0100
@@ -71,7 +71,7 @@
prefix for the Skolem constant.*)
fun declare_skofuns s th =
let
- val nref = Unsynchronized.ref 0
+ val nref = Unsynchronized.ref 0 (* FIXME ??? *)
fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) =
(*Existential: declare a Skolem function, then insert into body and continue*)
let
@@ -87,7 +87,8 @@
val (c, thy') =
Sign.declare_const ((Binding.conceal (Binding.name cname), cT), NoSyn) thy
val cdef = cname ^ "_def"
- val thy'' = Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
+ val thy'' =
+ Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef)
in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
| dec_sko (Const ("All", _) $ (Abs (a, T, p))) thx =
@@ -102,7 +103,7 @@
(*Traverse a theorem, accumulating Skolem function definitions.*)
fun assume_skofuns s th =
- let val sko_count = Unsynchronized.ref 0
+ let val sko_count = Unsynchronized.ref 0 (* FIXME ??? *)
fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
(*Existential: declare a Skolem function, then insert into body and continue*)
let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*)
--- a/src/HOLCF/Tools/pcpodef.ML Tue Oct 27 16:01:38 2009 +0100
+++ b/src/HOLCF/Tools/pcpodef.ML Tue Oct 27 16:47:27 2009 +0100
@@ -90,6 +90,7 @@
fun make_cpo admissible (type_def, below_def, set_def) theory =
let
+ (* FIXME fold_rule might fold user input inintentionally *)
val admissible' = fold_rule (the_list set_def) admissible;
val cpo_thms = map (Thm.transfer theory) [type_def, below_def, admissible'];
val theory' = theory
@@ -112,6 +113,7 @@
fun make_pcpo UU_mem (type_def, below_def, set_def) theory =
let
+ (* FIXME fold_rule might fold user input inintentionally *)
val UU_mem' = fold_rule (the_list set_def) UU_mem;
val pcpo_thms = map (Thm.transfer theory) [type_def, below_def, UU_mem'];
val theory' = theory
--- a/src/Pure/General/file.ML Tue Oct 27 16:01:38 2009 +0100
+++ b/src/Pure/General/file.ML Tue Oct 27 16:47:27 2009 +0100
@@ -90,10 +90,10 @@
Unsynchronized.ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
in
-fun check_cache (path, time) = CRITICAL (fn () =>
+fun check_cache (path, time) =
(case Symtab.lookup (! ident_cache) path of
NONE => NONE
- | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE));
+ | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE);
fun update_cache (path, (time, id)) = CRITICAL (fn () =>
Unsynchronized.change ident_cache
--- a/src/Pure/General/print_mode.ML Tue Oct 27 16:01:38 2009 +0100
+++ b/src/Pure/General/print_mode.ML Tue Oct 27 16:47:27 2009 +0100
@@ -35,7 +35,7 @@
let val modes =
(case Thread.getLocal tag of
SOME (SOME modes) => modes
- | _ => NAMED_CRITICAL "print_mode" (fn () => ! print_mode))
+ | _ => ! print_mode)
in subtract (op =) [input, internal] modes end;
fun print_mode_active mode = member (op =) (print_mode_value ()) mode;
--- a/src/Pure/Isar/isar_cmd.ML Tue Oct 27 16:01:38 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Tue Oct 27 16:47:27 2009 +0100
@@ -333,14 +333,14 @@
Toplevel.keep (ProofContext.print_abbrevs o Toplevel.context_of);
val print_facts = Toplevel.unknown_context o Toplevel.keep (fn state =>
- ProofContext.setmp_verbose
+ ProofContext.setmp_verbose_CRITICAL
ProofContext.print_lthms (Toplevel.context_of state));
val print_configs = Toplevel.unknown_context o Toplevel.keep (fn state =>
Attrib.print_configs (Toplevel.context_of state));
val print_theorems_proof = Toplevel.keep (fn state =>
- ProofContext.setmp_verbose
+ ProofContext.setmp_verbose_CRITICAL
ProofContext.print_lthms (Proof.context_of (Toplevel.proof_of state)));
val print_theorems_theory = Toplevel.keep (fn state =>
@@ -431,10 +431,10 @@
(* print proof context contents *)
val print_binds = Toplevel.unknown_context o Toplevel.keep (fn state =>
- ProofContext.setmp_verbose ProofContext.print_binds (Toplevel.context_of state));
+ ProofContext.setmp_verbose_CRITICAL ProofContext.print_binds (Toplevel.context_of state));
val print_cases = Toplevel.unknown_context o Toplevel.keep (fn state =>
- ProofContext.setmp_verbose ProofContext.print_cases (Toplevel.context_of state));
+ ProofContext.setmp_verbose_CRITICAL ProofContext.print_cases (Toplevel.context_of state));
(* print theorems, terms, types etc. *)
--- a/src/Pure/Isar/isar_document.ML Tue Oct 27 16:01:38 2009 +0100
+++ b/src/Pure/Isar/isar_document.ML Tue Oct 27 16:47:27 2009 +0100
@@ -119,13 +119,13 @@
in
fun change_states f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_states f);
-fun get_states () = NAMED_CRITICAL "Isar" (fn () => ! global_states);
+fun get_states () = ! global_states;
fun change_commands f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_commands f);
-fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
+fun get_commands () = ! global_commands;
fun change_documents f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_documents f);
-fun get_documents () = NAMED_CRITICAL "Isar" (fn () => ! global_documents);
+fun get_documents () = ! global_documents;
fun init () = NAMED_CRITICAL "Isar" (fn () =>
(global_states := Symtab.empty;
--- a/src/Pure/Isar/outer_keyword.ML Tue Oct 27 16:01:38 2009 +0100
+++ b/src/Pure/Isar/outer_keyword.ML Tue Oct 27 16:47:27 2009 +0100
@@ -121,8 +121,8 @@
in
-fun get_commands () = CRITICAL (fn () => ! global_commands);
-fun get_lexicons () = CRITICAL (fn () => ! global_lexicons);
+fun get_commands () = ! global_commands;
+fun get_lexicons () = ! global_lexicons;
fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);
fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);
--- a/src/Pure/Isar/outer_syntax.ML Tue Oct 27 16:01:38 2009 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Tue Oct 27 16:47:27 2009 +0100
@@ -101,8 +101,8 @@
(* access current syntax *)
-fun get_commands () = CRITICAL (fn () => ! global_commands);
-fun get_markups () = CRITICAL (fn () => ! global_markups);
+fun get_commands () = ! global_commands;
+fun get_markups () = ! global_markups;
fun get_command () = Symtab.lookup (get_commands ());
fun get_syntax () = CRITICAL (fn () => (OuterKeyword.get_lexicons (), get_command ()));
--- a/src/Pure/Isar/proof_context.ML Tue Oct 27 16:01:38 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Tue Oct 27 16:47:27 2009 +0100
@@ -122,7 +122,7 @@
val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context
val revert_abbrev: string -> string -> Proof.context -> Proof.context
val verbose: bool Unsynchronized.ref
- val setmp_verbose: ('a -> 'b) -> 'a -> 'b
+ val setmp_verbose_CRITICAL: ('a -> 'b) -> 'a -> 'b
val print_syntax: Proof.context -> unit
val print_abbrevs: Proof.context -> unit
val print_binds: Proof.context -> unit
@@ -1200,7 +1200,7 @@
val verbose = Unsynchronized.ref false;
fun verb f x = if ! verbose then f (x ()) else [];
-fun setmp_verbose f x = setmp_CRITICAL verbose true f x;
+fun setmp_verbose_CRITICAL f x = setmp_CRITICAL verbose true f x;
(* local syntax *)
--- a/src/Pure/Isar/toplevel.ML Tue Oct 27 16:01:38 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML Tue Oct 27 16:47:27 2009 +0100
@@ -552,7 +552,7 @@
local val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list) in
fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
-fun get_hooks () = CRITICAL (fn () => ! hooks);
+fun get_hooks () = ! hooks;
end;
--- a/src/Pure/ML/ml_context.ML Tue Oct 27 16:01:38 2009 +0100
+++ b/src/Pure/ML/ml_context.ML Tue Oct 27 16:47:27 2009 +0100
@@ -54,7 +54,7 @@
(* theorem bindings *)
-val stored_thms: thm list Unsynchronized.ref = Unsynchronized.ref [];
+val stored_thms: thm list Unsynchronized.ref = Unsynchronized.ref []; (* FIXME via context!? *)
fun ml_store sel (name, ths) =
let
@@ -195,6 +195,7 @@
fun eval_in ctxt verbose pos txt =
Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval verbose pos txt) ();
+(* FIXME not thread-safe -- reference can be accessed directly *)
fun evaluate ctxt verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () =>
let
val _ = r := NONE;
--- a/src/Pure/System/isabelle_process.ML Tue Oct 27 16:01:38 2009 +0100
+++ b/src/Pure/System/isabelle_process.ML Tue Oct 27 16:47:27 2009 +0100
@@ -61,9 +61,6 @@
else message_pos ts
| _ => NONE);
-fun output out_stream s = NAMED_CRITICAL "IO" (fn () =>
- (TextIO.output (out_stream, s); TextIO.output (out_stream, "\n")));
-
in
fun message _ _ "" = ()
@@ -74,14 +71,16 @@
Position.properties_of (Position.thread_data ())
|> Position.default_properties pos;
val txt = clean_string [Symbol.STX] body;
- in output out_stream (special ch ^ message_props props ^ txt ^ special_end) end;
+ val msg = special ch ^ message_props props ^ txt ^ special_end ^ "\n";
+ in TextIO.output (out_stream, msg) end;
fun init_message out_stream =
let
val pid = (Markup.pidN, process_id ());
val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
val text = Session.welcome ();
- in output out_stream (special "A" ^ message_props [pid, session] ^ text ^ special_end) end;
+ val msg = special "A" ^ message_props [pid, session] ^ text ^ special_end ^ "\n";
+ in TextIO.output (out_stream, msg) end;
end;
--- a/src/Pure/System/isar.ML Tue Oct 27 16:01:38 2009 +0100
+++ b/src/Pure/System/isar.ML Tue Oct 27 16:47:27 2009 +0100
@@ -47,10 +47,10 @@
| edit n (st, hist) = edit (n - 1) (f st hist);
in edit count (! global_state, ! global_history) end);
-fun state () = NAMED_CRITICAL "Isar" (fn () => ! global_state);
+fun state () = ! global_state;
-fun exn () = NAMED_CRITICAL "Isar" (fn () => ! global_exn);
-fun set_exn exn = NAMED_CRITICAL "Isar" (fn () => global_exn := exn);
+fun exn () = ! global_exn;
+fun set_exn exn = global_exn := exn;
end;
--- a/src/Pure/Thy/html.ML Tue Oct 27 16:01:38 2009 +0100
+++ b/src/Pure/Thy/html.ML Tue Oct 27 16:47:27 2009 +0100
@@ -267,7 +267,7 @@
(* document *)
val charset = Unsynchronized.ref "ISO-8859-1";
-fun with_charset s = setmp_noncritical charset s; (* FIXME *)
+fun with_charset s = setmp_noncritical charset s; (* FIXME unreliable *)
fun begin_document title =
let val cs = ! charset in
--- a/src/Pure/Thy/thy_load.ML Tue Oct 27 16:01:38 2009 +0100
+++ b/src/Pure/Thy/thy_load.ML Tue Oct 27 16:47:27 2009 +0100
@@ -41,16 +41,22 @@
fun show_path () = map Path.implode (! load_path);
-fun del_path s = CRITICAL (fn () =>
- Unsynchronized.change load_path (remove (op =) (Path.explode s)));
-fun add_path s = CRITICAL (fn () =>
- (del_path s; Unsynchronized.change load_path (cons (Path.explode s))));
-fun path_add s = CRITICAL (fn () =>
+fun del_path s =
+ CRITICAL (fn () => Unsynchronized.change load_path (remove (op =) (Path.explode s)));
+
+fun add_path s =
+ CRITICAL (fn () => (del_path s; Unsynchronized.change load_path (cons (Path.explode s))));
+
+fun path_add s =
+ CRITICAL (fn () =>
(del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s])));
+
fun reset_path () = load_path := [Path.current];
fun with_paths ss f x =
- CRITICAL (fn () => setmp_CRITICAL load_path (! load_path @ map Path.explode ss) f x);
+ CRITICAL (fn () =>
+ setmp_CRITICAL load_path (! load_path @ map Path.explode ss) f x);
+
fun with_path s f x = with_paths [s] f x;
fun search_path dir path =
--- a/src/Pure/codegen.ML Tue Oct 27 16:01:38 2009 +0100
+++ b/src/Pure/codegen.ML Tue Oct 27 16:47:27 2009 +0100
@@ -105,7 +105,7 @@
val quiet_mode = Unsynchronized.ref true;
fun message s = if !quiet_mode then () else writeln s;
-val mode = Unsynchronized.ref ([] : string list);
+val mode = Unsynchronized.ref ([] : string list); (* FIXME proper functional argument *)
val margin = Unsynchronized.ref 80;
@@ -928,7 +928,7 @@
[str "(result ())"],
str ");"]) ^
"\n\nend;\n";
- val _ = NAMED_CRITICAL "codegen" (fn () =>
+ val _ = NAMED_CRITICAL "codegen" (fn () => (* FIXME ??? *)
ML_Context.eval_in (SOME ctxt) false Position.none s);
in !eval_result end;
in e () end;