--- a/etc/isabelle.css Thu Jun 30 10:15:46 2011 +0200
+++ b/etc/isabelle.css Thu Jun 30 16:07:30 2011 +0200
@@ -17,7 +17,7 @@
/* basic syntax markup */
-.hidden { font-size: 0.1pt; visibility: hidden; }
+.hidden { font-size: 1px; visibility: hidden; }
.binding { color: #336655; }
.entity_class { color: red; }
--- a/src/FOL/simpdata.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/FOL/simpdata.ML Thu Jun 30 16:07:30 2011 +0200
@@ -108,11 +108,12 @@
val triv_rls = [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @{thm notFalseI}];
-fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls @ prems),
- atac, etac @{thm FalseE}];
+fun unsafe_solver ss =
+ FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ss), atac, etac @{thm FalseE}];
+
(*No premature instantiation of variables during simplification*)
-fun safe_solver prems = FIRST'[match_tac (triv_rls @ prems),
- eq_assume_tac, ematch_tac [@{thm FalseE}]];
+fun safe_solver ss =
+ FIRST' [match_tac (triv_rls @ Simplifier.prems_of ss), eq_assume_tac, ematch_tac @{thms FalseE}];
(*No simprules, but basic infastructure for simplification*)
val FOL_basic_ss =
--- a/src/HOL/Decision_Procs/cooper_tac.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Thu Jun 30 16:07:30 2011 +0200
@@ -82,7 +82,7 @@
@{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
Suc_eq_plus1]
addsimps @{thms add_ac}
- addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
+ addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
val simpset0 = HOL_basic_ss
addsimps [mod_div_equality', Suc_eq_plus1]
addsimps comp_arith
--- a/src/HOL/Decision_Procs/mir_tac.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Thu Jun 30 16:07:30 2011 +0200
@@ -104,7 +104,7 @@
@{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
@{thm "Suc_eq_plus1"}]
addsimps @{thms add_ac}
- addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
+ addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
val simpset0 = HOL_basic_ss
addsimps [mod_div_equality', @{thm Suc_eq_plus1}]
addsimps comp_ths
--- a/src/HOL/Divides.thy Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/Divides.thy Thu Jun 30 16:07:30 2011 +0200
@@ -679,9 +679,7 @@
text {* Simproc for cancelling @{const div} and @{const mod} *}
ML {*
-local
-
-structure CancelDivMod = CancelDivModFun
+structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
(
val div_name = @{const_name div};
val mod_name = @{const_name mod};
@@ -694,17 +692,10 @@
val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
(@{thm add_0_left} :: @{thm add_0_right} :: @{thms add_ac}))
)
-
-in
-
-val cancel_div_mod_nat_proc = Simplifier.simproc_global @{theory}
- "cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc);
-
-val _ = Addsimprocs [cancel_div_mod_nat_proc];
-
-end
*}
+simproc_setup cancel_div_mod_nat ("(m::nat) + n") = {* K Cancel_Div_Mod_Nat.proc *}
+
subsubsection {* Quotient *}
@@ -1437,9 +1428,7 @@
text {* Tool setup *}
ML {*
-local
-
-structure CancelDivMod = CancelDivModFun
+structure Cancel_Div_Mod_Int = Cancel_Div_Mod
(
val div_name = @{const_name div};
val mod_name = @{const_name mod};
@@ -1452,17 +1441,10 @@
val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
(@{thm diff_minus} :: @{thms add_0s} @ @{thms add_ac}))
)
-
-in
-
-val cancel_div_mod_int_proc = Simplifier.simproc_global @{theory}
- "cancel_zdiv_zmod" ["(k::int) + l"] (K CancelDivMod.proc);
-
-val _ = Addsimprocs [cancel_div_mod_int_proc];
-
-end
*}
+simproc_setup cancel_div_mod_int ("(k::int) + l") = {* K Cancel_Div_Mod_Int.proc *}
+
lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b"
apply (cut_tac a = a and b = b in divmod_int_correct)
apply (auto simp add: divmod_int_rel_def mod_int_def)
--- a/src/HOL/HOL.thy Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/HOL.thy Thu Jun 30 16:07:30 2011 +0200
@@ -1232,7 +1232,7 @@
fun proc ss ct =
(case Thm.term_of ct of
eq $ lhs $ rhs =>
- (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of_ss ss) of
+ (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of
SOME thm => SOME (thm RS neq_to_EQ_False)
| NONE => NONE)
| _ => NONE);
--- a/src/HOL/Int.thy Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/Int.thy Thu Jun 30 16:07:30 2011 +0200
@@ -1545,9 +1545,13 @@
of_int_0 of_int_1 of_int_add of_int_mult
use "Tools/int_arith.ML"
-setup {* Int_Arith.global_setup *}
declaration {* K Int_Arith.setup *}
+simproc_setup fast_arith ("(m::'a::{linordered_idom,number_ring}) < n" |
+ "(m::'a::{linordered_idom,number_ring}) <= n" |
+ "(m::'a::{linordered_idom,number_ring}) = n") =
+ {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
+
setup {*
Reorient_Proc.add
(fn Const (@{const_name number_of}, _) $ _ => true | _ => false)
--- a/src/HOL/List.thy Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/List.thy Thu Jun 30 16:07:30 2011 +0200
@@ -726,54 +726,44 @@
- or both lists end in the same list.
*}
-ML {*
-local
-
-fun last (cons as Const(@{const_name Cons},_) $ _ $ xs) =
- (case xs of Const(@{const_name Nil},_) => cons | _ => last xs)
- | last (Const(@{const_name append},_) $ _ $ ys) = last ys
- | last t = t;
-
-fun list1 (Const(@{const_name Cons},_) $ _ $ Const(@{const_name Nil},_)) = true
- | list1 _ = false;
-
-fun butlast ((cons as Const(@{const_name Cons},_) $ x) $ xs) =
- (case xs of Const(@{const_name Nil},_) => xs | _ => cons $ butlast xs)
- | butlast ((app as Const(@{const_name append},_) $ xs) $ ys) = app $ butlast ys
- | butlast xs = Const(@{const_name Nil},fastype_of xs);
-
-val rearr_ss = HOL_basic_ss addsimps [@{thm append_assoc},
- @{thm append_Nil}, @{thm append_Cons}];
-
-fun list_eq ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
+simproc_setup list_eq ("(xs::'a list) = ys") = {*
let
- val lastl = last lhs and lastr = last rhs;
- fun rearr conv =
+ fun last (cons as Const (@{const_name Cons}, _) $ _ $ xs) =
+ (case xs of Const (@{const_name Nil}, _) => cons | _ => last xs)
+ | last (Const(@{const_name append},_) $ _ $ ys) = last ys
+ | last t = t;
+
+ fun list1 (Const(@{const_name Cons},_) $ _ $ Const(@{const_name Nil},_)) = true
+ | list1 _ = false;
+
+ fun butlast ((cons as Const(@{const_name Cons},_) $ x) $ xs) =
+ (case xs of Const (@{const_name Nil}, _) => xs | _ => cons $ butlast xs)
+ | butlast ((app as Const (@{const_name append}, _) $ xs) $ ys) = app $ butlast ys
+ | butlast xs = Const(@{const_name Nil}, fastype_of xs);
+
+ val rearr_ss =
+ HOL_basic_ss addsimps [@{thm append_assoc}, @{thm append_Nil}, @{thm append_Cons}];
+
+ fun list_eq ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
let
- val lhs1 = butlast lhs and rhs1 = butlast rhs;
- val Type(_,listT::_) = eqT
- val appT = [listT,listT] ---> listT
- val app = Const(@{const_name append},appT)
- val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
- val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
- val thm = Goal.prove (Simplifier.the_context ss) [] [] eq
- (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
- in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
-
- in
- if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}
- else if lastl aconv lastr then rearr @{thm append_same_eq}
- else NONE
- end;
-
-in
-
-val list_eq_simproc =
- Simplifier.simproc_global @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
-
-end;
-
-Addsimprocs [list_eq_simproc];
+ val lastl = last lhs and lastr = last rhs;
+ fun rearr conv =
+ let
+ val lhs1 = butlast lhs and rhs1 = butlast rhs;
+ val Type(_,listT::_) = eqT
+ val appT = [listT,listT] ---> listT
+ val app = Const(@{const_name append},appT)
+ val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
+ val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
+ val thm = Goal.prove (Simplifier.the_context ss) [] [] eq
+ (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
+ in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
+ in
+ if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}
+ else if lastl aconv lastr then rearr @{thm append_same_eq}
+ else NONE
+ end;
+ in fn _ => fn ss => fn ct => list_eq ss (term_of ct) end;
*}
--- a/src/HOL/Matrix/Compute_Oracle/am_ghc.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/Matrix/Compute_Oracle/am_ghc.ML Thu Jun 30 16:07:30 2011 +0200
@@ -210,7 +210,7 @@
string_of_int (Time.toMicroseconds (Time.now ())) ^ string_of_int c
end
-fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.make [s])));
+fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.basic s)));
fun wrap s = "\""^s^"\""
fun writeTextFile name s = File.write (Path.explode name) s
--- a/src/HOL/Matrix/Cplex_tools.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/Matrix/Cplex_tools.ML Thu Jun 30 16:07:30 2011 +0200
@@ -1129,7 +1129,7 @@
exception Execute of string;
-fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.make [s])));
+fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.basic s)));
fun wrap s = "\""^s^"\"";
fun solve_glpk prog =
--- a/src/HOL/NSA/HyperDef.thy Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/NSA/HyperDef.thy Thu Jun 30 16:07:30 2011 +0200
@@ -348,12 +348,12 @@
#> Lin_Arith.add_simps [@{thm star_of_zero}, @{thm star_of_one},
@{thm star_of_number_of}, @{thm star_of_add}, @{thm star_of_minus},
@{thm star_of_diff}, @{thm star_of_mult}]
- #> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"})
- #> Simplifier.map_ss (fn simpset => simpset addsimprocs [Simplifier.simproc_global @{theory}
- "fast_hypreal_arith" ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
- (K Lin_Arith.simproc)]))
+ #> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"}))
*}
+simproc_setup fast_arith_hypreal ("(m::hypreal) < n" | "(m::hypreal) <= n" | "(m::hypreal) = n") =
+ {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
+
subsection {* Exponentials on the Hyperreals *}
--- a/src/HOL/Nat.thy Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/Nat.thy Thu Jun 30 16:07:30 2011 +0200
@@ -1433,6 +1433,15 @@
setup {* Lin_Arith.global_setup *}
declaration {* K Lin_Arith.setup *}
+simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) <= n" | "(m::nat) = n") =
+ {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
+(* Because of this simproc, the arithmetic solver is really only
+useful to detect inconsistencies among the premises for subgoals which are
+*not* themselves (in)equalities, because the latter activate
+fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
+solver all the time rather than add the additional check. *)
+
+
lemmas [arith_split] = nat_diff_split split_min split_max
context order
--- a/src/HOL/Orderings.thy Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/Orderings.thy Thu Jun 30 16:07:30 2011 +0200
@@ -534,7 +534,7 @@
fun prp t thm = (#prop (rep_thm thm) = t);
fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) =
- let val prems = prems_of_ss ss;
+ let val prems = Simplifier.prems_of ss;
val less = Const (@{const_name less}, T);
val t = HOLogic.mk_Trueprop(le $ s $ r);
in case find_first (prp t) prems of
@@ -549,7 +549,7 @@
handle THM _ => NONE;
fun prove_antisym_less sg ss (NotC $ ((less as Const(_,T)) $ r $ s)) =
- let val prems = prems_of_ss ss;
+ let val prems = Simplifier.prems_of ss;
val le = Const (@{const_name less_eq}, T);
val t = HOLogic.mk_Trueprop(le $ r $ s);
in case find_first (prp t) prems of
@@ -570,7 +570,7 @@
fun add_solver name tac =
Simplifier.map_simpset_global (fn ss => ss addSolver
- mk_solver' name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)));
+ mk_solver name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of ss)));
in
add_simprocs [
--- a/src/HOL/Product_Type.thy Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/Product_Type.thy Thu Jun 30 16:07:30 2011 +0200
@@ -55,14 +55,10 @@
this rule directly --- it loops!
*}
-ML {*
- val unit_eq_proc =
- let val unit_meta_eq = mk_meta_eq @{thm unit_eq} in
- Simplifier.simproc_global @{theory} "unit_eq" ["x::unit"]
- (fn _ => fn _ => fn t => if HOLogic.is_unit t then NONE else SOME unit_meta_eq)
- end;
-
- Addsimprocs [unit_eq_proc];
+simproc_setup unit_eq ("x::unit") = {*
+ fn _ => fn _ => fn ct =>
+ if HOLogic.is_unit (term_of ct) then NONE
+ else SOME (mk_meta_eq @{thm unit_eq})
*}
rep_datatype "()" by simp
@@ -74,7 +70,7 @@
by (rule triv_forall_equality)
text {*
- This rewrite counters the effect of @{text unit_eq_proc} on @{term
+ This rewrite counters the effect of simproc @{text unit_eq} on @{term
[source] "%u::unit. f u"}, replacing it by @{term [source]
f} rather than by @{term [source] "%u. f ()"}.
*}
@@ -497,7 +493,7 @@
| exists_paired_all _ = false;
val ss = HOL_basic_ss
addsimps [@{thm split_paired_all}, @{thm unit_all_eq2}, @{thm unit_abs_eta_conv}]
- addsimprocs [unit_eq_proc];
+ addsimprocs [@{simproc unit_eq}];
in
val split_all_tac = SUBGOAL (fn (t, i) =>
if exists_paired_all t then safe_full_simp_tac ss i else no_tac);
@@ -560,6 +556,7 @@
if Pair_pat k i (t $ u) then incr_boundvars k arg
else (subst arg k i t $ subst arg k i u)
| subst arg k i t = t;
+in
fun beta_proc ss (s as Const (@{const_name prod_case}, _) $ Abs (_, _, t) $ arg) =
(case split_pat beta_term_pat 1 t of
SOME (i, f) => SOME (metaeq ss s (subst arg 0 i f))
@@ -570,13 +567,10 @@
SOME (_, ft) => SOME (metaeq ss s (let val (f $ arg) = ft in f end))
| NONE => NONE)
| eta_proc _ _ = NONE;
-in
- val split_beta_proc = Simplifier.simproc_global @{theory} "split_beta" ["split f z"] (K beta_proc);
- val split_eta_proc = Simplifier.simproc_global @{theory} "split_eta" ["split f"] (K eta_proc);
end;
-
-Addsimprocs [split_beta_proc, split_eta_proc];
*}
+simproc_setup split_beta ("split f z") = {* fn _ => fn ss => fn ct => beta_proc ss (term_of ct) *}
+simproc_setup split_eta ("split f") = {* fn _ => fn ss => fn ct => eta_proc ss (term_of ct) *}
lemma split_beta [mono]: "(%(x, y). P x y) z = P (fst z) (snd z)"
by (subst surjective_pairing, rule split_conv)
--- a/src/HOL/Statespace/distinct_tree_prover.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Thu Jun 30 16:07:30 2011 +0200
@@ -352,10 +352,8 @@
| NONE => no_tac)
| _ => no_tac))
-fun distinctFieldSolver names = mk_solver' "distinctFieldSolver"
- (fn ss => case try Simplifier.the_context ss of
- SOME ctxt => distinctTree_tac names ctxt
- | NONE => K no_tac)
+fun distinctFieldSolver names = mk_solver "distinctFieldSolver"
+ (distinctTree_tac names o Simplifier.the_context)
fun distinct_simproc names =
Simplifier.simproc_global @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
--- a/src/HOL/Statespace/state_space.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/Statespace/state_space.ML Thu Jun 30 16:07:30 2011 +0200
@@ -225,10 +225,8 @@
| NONE => no_tac)
| _ => no_tac));
-val distinctNameSolver = mk_solver' "distinctNameSolver"
- (fn ss => case try Simplifier.the_context ss of
- SOME ctxt => distinctTree_tac ctxt
- | NONE => K no_tac)
+val distinctNameSolver = mk_solver "distinctNameSolver"
+ (distinctTree_tac o Simplifier.the_context)
val distinct_simproc =
Simplifier.simproc_global @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Thu Jun 30 16:07:30 2011 +0200
@@ -225,7 +225,7 @@
*)
ML {*
val config_fast_solver = Attrib.setup_config_bool @{binding fast_solver} (K false);
- val fast_solver = mk_solver' "fast_solver" (fn ss =>
+ val fast_solver = mk_solver "fast_solver" (fn ss =>
if Config.get (Simplifier.the_context ss) config_fast_solver
then assume_tac ORELSE' (etac notE)
else K no_tac);
--- a/src/HOL/Tools/ATP/atp_proof.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Jun 30 16:07:30 2011 +0200
@@ -142,9 +142,7 @@
\TPTP syntax. To install it, download and extract the package \
\\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
\\"spass-3.7\" directory's absolute path to " ^
- Path.print (Path.expand (Path.appends
- (Path.variable "ISABELLE_HOME_USER" ::
- map Path.basic ["etc", "components"]))) ^
+ Path.print (Path.expand (Path.explode "$ISABELLE_HOME_USER/etc/components")) ^
" on a line of its own."
| string_for_failure VampireTooOld =
"Isabelle requires a more recent version of Vampire. To install it, follow \
--- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Jun 30 16:07:30 2011 +0200
@@ -183,9 +183,8 @@
"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.print (Path.expand (Path.appends
- (Path.variable "ISABELLE_HOME_USER" ::
- map Path.basic ["etc", "components"]))) ^ " on a line of its own."
+ Path.print (Path.expand (Path.explode "$ISABELLE_HOME_USER/etc/components")) ^
+ " on a line of its own."
val max_unsound_delay_ms = 200
val max_unsound_delay_percent = 2
--- a/src/HOL/Tools/Qelim/cooper.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Thu Jun 30 16:07:30 2011 +0200
@@ -805,7 +805,7 @@
@{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"},
@{thm "mod_1"}, @{thm "Suc_eq_plus1"}]
@ @{thms add_ac}
- addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
+ addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits
[@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"},
@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Jun 30 16:07:30 2011 +0200
@@ -206,7 +206,8 @@
fun with_overlord_dir name f =
let
- val path = Path.append (Path.explode "~/.isabelle") (Path.basic (name ^ serial_string ()))
+ val path =
+ Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
val _ = Isabelle_System.mkdirs path;
in Exn.release (Exn.capture f path) end;
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Jun 30 16:07:30 2011 +0200
@@ -55,7 +55,7 @@
REPEAT_ALL_NEW (resolve_tac (Quotient_Info.equiv_rules_get ctxt))
fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
-val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
+val equiv_solver = mk_solver "Equivalence goal solver" equiv_solver_tac
fun quotient_tac ctxt =
(REPEAT_ALL_NEW (FIRST'
@@ -63,8 +63,7 @@
resolve_tac (Quotient_Info.quotient_rules_get ctxt)]))
fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
-val quotient_solver =
- Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
+val quotient_solver = mk_solver "Quotient goal solver" quotient_solver_tac
fun solve_quotient_assm ctxt thm =
case Seq.pull (quotient_tac ctxt 1 thm) of
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Thu Jun 30 16:07:30 2011 +0200
@@ -307,7 +307,7 @@
let
val (le, r, s) = dest_binop t
val less = Const (@{const_name less}, Term.fastype_of le)
- val prems = Simplifier.prems_of_ss ss
+ val prems = Simplifier.prems_of ss
in
(case find_first (eq_prop (le $ s $ r)) prems of
NONE =>
@@ -321,7 +321,7 @@
let
val (less, r, s) = dest_binop (HOLogic.dest_not t)
val le = Const (@{const_name less_eq}, Term.fastype_of less)
- val prems = prems_of_ss ss
+ val prems = Simplifier.prems_of ss
in
(case find_first (eq_prop (le $ r $ s)) prems of
NONE =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jun 30 16:07:30 2011 +0200
@@ -703,7 +703,7 @@
|> fold maybe_run_slice actual_slices
end
else
- error ("Bad executable: " ^ Path.print command ^ ".")
+ error ("Bad executable: " ^ Path.print command)
(* If the problem file has not been exported, remove it; otherwise, export
the proof file too. *)
--- a/src/HOL/Tools/TFL/rules.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Thu Jun 30 16:07:30 2011 +0200
@@ -657,7 +657,7 @@
fun prover used ss thm =
let fun cong_prover ss thm =
let val dummy = say "cong_prover:"
- val cntxt = Simplifier.prems_of_ss ss
+ val cntxt = Simplifier.prems_of ss
val dummy = print_thms "cntxt:" cntxt
val dummy = say "cong rule:"
val dummy = say (Display.string_of_thm_without_context thm)
@@ -739,7 +739,7 @@
fun restrict_prover ss thm =
let val dummy = say "restrict_prover:"
- val cntxt = rev(Simplifier.prems_of_ss ss)
+ val cntxt = rev (Simplifier.prems_of ss)
val dummy = print_thms "cntxt:" cntxt
val thy = Thm.theory_of_thm thm
val Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ _ = Thm.prop_of thm
--- a/src/HOL/Tools/int_arith.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/Tools/int_arith.ML Thu Jun 30 16:07:30 2011 +0200
@@ -6,7 +6,6 @@
signature INT_ARITH =
sig
val setup: Context.generic -> Context.generic
- val global_setup: theory -> theory
end
structure Int_Arith : INT_ARITH =
@@ -78,16 +77,6 @@
make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
proc = sproc, identifier = []}
-val fast_int_arith_simproc =
- Simplifier.simproc_global @{theory} "fast_int_arith"
- ["(m::'a::{linordered_idom,number_ring}) < n",
- "(m::'a::{linordered_idom,number_ring}) <= n",
- "(m::'a::{linordered_idom,number_ring}) = n"] (K Lin_Arith.simproc);
-
-val global_setup =
- Simplifier.map_simpset_global (fn ss => ss addsimprocs [fast_int_arith_simproc]);
-
-
fun number_of thy T n =
if not (Sign.of_sort thy (T, @{sort number}))
then raise CTERM ("number_of", [])
--- a/src/HOL/Tools/lin_arith.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/Tools/lin_arith.ML Thu Jun 30 16:07:30 2011 +0200
@@ -897,15 +897,8 @@
val setup =
init_arith_data #>
- Simplifier.map_ss (fn ss => ss addsimprocs [Simplifier.simproc_global @{theory} "fast_nat_arith"
- ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K simproc)]
- (* Because of fast_nat_arith_simproc, the arithmetic solver is really only
- useful to detect inconsistencies among the premises for subgoals which are
- *not* themselves (in)equalities, because the latter activate
- fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
- solver all the time rather than add the additional check. *)
- addSolver (mk_solver' "lin_arith"
- (add_arith_facts #> Fast_Arith.cut_lin_arith_tac)))
+ Simplifier.map_ss (fn ss => ss
+ addSolver (mk_solver "lin_arith" (add_arith_facts #> Fast_Arith.cut_lin_arith_tac)));
val global_setup =
Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))
--- a/src/HOL/Tools/simpdata.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/Tools/simpdata.ML Thu Jun 30 16:07:30 2011 +0200
@@ -112,19 +112,19 @@
fun mksimps pairs (_: simpset) =
map_filter (try mk_eq) o mk_atomize pairs o gen_all;
-fun unsafe_solver_tac prems =
+fun unsafe_solver_tac ss =
(fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
- FIRST' [resolve_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems), atac,
- etac @{thm FalseE}];
+ FIRST' [resolve_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ss),
+ atac, etac @{thm FalseE}];
val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
(*No premature instantiation of variables during simplification*)
-fun safe_solver_tac prems =
+fun safe_solver_tac ss =
(fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
- FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems),
- eq_assume_tac, ematch_tac @{thms FalseE}];
+ FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ss),
+ eq_assume_tac, ematch_tac @{thms FalseE}];
val safe_solver = mk_solver "HOL safe" safe_solver_tac;
--- a/src/HOL/Transitive_Closure.thy Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/Transitive_Closure.thy Thu Jun 30 16:07:30 2011 +0200
@@ -1029,10 +1029,10 @@
setup {*
Simplifier.map_simpset_global (fn ss => ss
- addSolver (mk_solver' "Trancl" (Trancl_Tac.trancl_tac o Simplifier.the_context))
- addSolver (mk_solver' "Rtrancl" (Trancl_Tac.rtrancl_tac o Simplifier.the_context))
- addSolver (mk_solver' "Tranclp" (Tranclp_Tac.trancl_tac o Simplifier.the_context))
- addSolver (mk_solver' "Rtranclp" (Tranclp_Tac.rtrancl_tac o Simplifier.the_context)))
+ addSolver (mk_solver "Trancl" (Trancl_Tac.trancl_tac o Simplifier.the_context))
+ addSolver (mk_solver "Rtrancl" (Trancl_Tac.rtrancl_tac o Simplifier.the_context))
+ addSolver (mk_solver "Tranclp" (Tranclp_Tac.trancl_tac o Simplifier.the_context))
+ addSolver (mk_solver "Rtranclp" (Tranclp_Tac.rtrancl_tac o Simplifier.the_context)))
*}
--- a/src/HOL/ex/atp_export.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/HOL/ex/atp_export.ML Thu Jun 30 16:07:30 2011 +0200
@@ -112,7 +112,7 @@
fun run_some_atp ctxt problem =
let
val thy = Proof_Context.theory_of ctxt
- val prob_file = Path.explode "/tmp/prob.tptp"
+ val prob_file = Path.explode "/tmp/prob.tptp" (* FIXME File.tmp_path (?) *)
val {exec, arguments, proof_delims, known_failures, ...} =
get_atp thy spassN
val _ = problem |> tptp_lines_for_atp_problem FOF
--- a/src/Provers/Arith/cancel_div_mod.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Provers/Arith/cancel_div_mod.ML Thu Jun 30 16:07:30 2011 +0200
@@ -27,11 +27,11 @@
signature CANCEL_DIV_MOD =
sig
- val proc: simpset -> term -> thm option
+ val proc: simpset -> cterm -> thm option
end;
-functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
+functor Cancel_Div_Mod(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
struct
fun coll_div_mod (Const(@{const_name Groups.plus},_) $ s $ t) dms =
@@ -70,12 +70,16 @@
let val teqt' = Data.prove_eq_sums ss (t, rearrange t pq)
in hd (Data.div_mod_eqs RL [teqt' RS transitive_thm]) end;
-fun proc ss t =
- let val (divs,mods) = coll_div_mod t ([],[])
- in if null divs orelse null mods then NONE
- else case inter (op =) mods divs of
- pq :: _ => SOME (cancel ss t pq)
- | [] => NONE
- end
+fun proc ss ct =
+ let
+ val t = term_of ct;
+ val (divs, mods) = coll_div_mod t ([], []);
+ in
+ if null divs orelse null mods then NONE
+ else
+ (case inter (op =) mods divs of
+ pq :: _ => SOME (cancel ss t pq)
+ | [] => NONE)
+ end;
end
--- a/src/Provers/Arith/cancel_numeral_factor.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Provers/Arith/cancel_numeral_factor.ML Thu Jun 30 16:07:30 2011 +0200
@@ -47,7 +47,7 @@
fun proc ss t =
let
val ctxt = Simplifier.the_context ss;
- val prems = prems_of_ss ss;
+ val prems = Simplifier.prems_of ss;
val ([t'], ctxt') = Variable.import_terms true [t] ctxt
val export = singleton (Variable.export ctxt' ctxt)
--- a/src/Provers/Arith/cancel_numerals.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML Thu Jun 30 16:07:30 2011 +0200
@@ -68,7 +68,7 @@
fun proc ss t =
let
val ctxt = Simplifier.the_context ss
- val prems = prems_of_ss ss
+ val prems = Simplifier.prems_of ss
val ([t'], ctxt') = Variable.import_terms true [t] ctxt
val export = singleton (Variable.export ctxt' ctxt)
--- a/src/Provers/Arith/extract_common_term.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Provers/Arith/extract_common_term.ML Thu Jun 30 16:07:30 2011 +0200
@@ -49,7 +49,7 @@
fun proc ss t =
let
val ctxt = Simplifier.the_context ss;
- val prems = prems_of_ss ss;
+ val prems = Simplifier.prems_of ss;
val ([t'], ctxt') = Variable.import_terms true [t] ctxt
val export = singleton (Variable.export ctxt' ctxt)
--- a/src/Provers/Arith/fast_lin_arith.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Thu Jun 30 16:07:30 2011 +0200
@@ -844,7 +844,7 @@
end);
fun cut_lin_arith_tac ss =
- cut_facts_tac (Simplifier.prems_of_ss ss) THEN'
+ cut_facts_tac (Simplifier.prems_of ss) THEN'
simpset_lin_arith_tac ss false;
fun lin_arith_tac ctxt =
@@ -925,7 +925,7 @@
fun lin_arith_simproc ss concl =
let
val ctxt = Simplifier.the_context ss
- val thms = maps LA_Logic.atomize (Simplifier.prems_of_ss ss)
+ val thms = maps LA_Logic.atomize (Simplifier.prems_of ss)
val Hs = map Thm.prop_of thms
val Tconcl = LA_Logic.mk_Trueprop concl
in
--- a/src/Pure/General/markup.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Pure/General/markup.ML Thu Jun 30 16:07:30 2011 +0200
@@ -29,6 +29,7 @@
val position_properties': string list
val position_properties: string list
val positionN: string val position: T
+ val pathN: string val path: string -> T
val indentN: string
val blockN: string val block: int -> T
val widthN: string
@@ -195,6 +196,11 @@
val (positionN, position) = markup_elem "position";
+(* path *)
+
+val (pathN, path) = markup_string "path" nameN;
+
+
(* pretty printing *)
val indentN = "indent";
--- a/src/Pure/General/markup.scala Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Pure/General/markup.scala Thu Jun 30 16:07:30 2011 +0200
@@ -128,8 +128,21 @@
val DEF_ID = "def_id"
val POSITION_PROPERTIES = Set(LINE, COLUMN, OFFSET, END_OFFSET, FILE, ID)
+ val POSITION = "position"
- val POSITION = "position"
+
+ /* path */
+
+ val PATH = "path"
+
+ object Path
+ {
+ def unapply(markup: Markup): Option[String] =
+ markup match {
+ case Markup(PATH, Name(name)) => Some(name)
+ case _ => None
+ }
+ }
/* pretty printing */
--- a/src/Pure/General/path.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Pure/General/path.ML Thu Jun 30 16:07:30 2011 +0200
@@ -1,8 +1,8 @@
(* Title: Pure/General/path.ML
Author: Markus Wenzel, TU Muenchen
-Abstract algebra of file paths: basic POSIX notation, extended by
-named roots (e.g. //foo) and variables (e.g. $BAR).
+Algebra of file-system paths: basic POSIX notation, extended by named
+roots (e.g. //foo) and variables (e.g. $BAR).
*)
signature PATH =
@@ -20,9 +20,10 @@
val append: T -> T -> T
val appends: T list -> T
val make: string list -> T
- val print: T -> string
val implode: T -> string
val explode: string -> T
+ val pretty: T -> Pretty.T
+ val print: T -> string
val dir: T -> T
val base: T -> T
val ext: string -> T -> T
@@ -120,8 +121,6 @@
end;
-val print = quote o implode_path;
-
(* explode *)
@@ -152,10 +151,19 @@
end;
+(* print *)
+
+fun pretty path =
+ let val s = implode_path path
+ in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end;
+
+val print = Pretty.str_of o pretty;
+
+
(* base element *)
fun split_path f (Path (Basic s :: xs)) = f (Path xs, s)
- | split_path _ path = error ("Cannot split path into dir/base: " ^ quote (implode_path path));
+ | split_path _ path = error ("Cannot split path into dir/base: " ^ print path);
val dir = split_path #1;
val base = split_path (fn (_, s) => Path [Basic s]);
@@ -171,20 +179,11 @@
(* expand variables *)
-local
-
-fun eval (Variable s) =
- (case getenv s of
- "" => error ("Undefined Isabelle environment variable: " ^ quote s)
- | path => rep (explode_path path))
+fun eval (Variable s) = rep (explode_path (getenv_strict s))
| eval x = [x];
-in
-
val expand = rep #> maps eval #> norm #> Path;
-end;
-
(* source position *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/path.scala Thu Jun 30 16:07:30 2011 +0200
@@ -0,0 +1,151 @@
+/* Title: Pure/General/path.scala
+ Author: Makarius
+
+Algebra of file-system paths: basic POSIX notation, extended by named
+roots (e.g. //foo) and variables (e.g. $BAR).
+*/
+
+package isabelle
+
+
+object Path
+{
+ /* path elements */
+
+ private sealed abstract class Elem
+ private case class Root(val name: String) extends Elem
+ private case class Basic(val name: String) extends Elem
+ private case class Variable(val name: String) extends Elem
+ private case object Parent extends Elem
+
+ private def err_elem(msg: String, s: String): Nothing =
+ error (msg + " path element specification: " + Library.quote(s))
+
+ private def check_elem(s: String): String =
+ if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s)
+ else
+ s.iterator.filter(c => c == '/' || c == '\\' || c == '$' || c == ':').toList match {
+ case Nil => s
+ case bads =>
+ err_elem ("Illegal character(s) " + Library.commas_quote(bads.map(_.toString)) + " in", s)
+ }
+
+ private def root_elem(s: String): Elem = Root(check_elem(s))
+ private def basic_elem(s: String): Elem = Basic(check_elem(s))
+ private def variable_elem(s: String): Elem = Variable(check_elem(s))
+
+ private def apply_elem(y: Elem, xs: List[Elem]): List[Elem] =
+ (y, xs) match {
+ case (Root(_), _) => List(y)
+ case (Parent, Root(_) :: _) => xs
+ case (Parent, Basic(_) :: rest) => rest
+ case _ => y :: xs
+ }
+
+ private def norm_elems(elems: List[Elem]): List[Elem] =
+ (elems :\ (Nil: List[Elem]))(apply_elem)
+
+ private def implode_elem(elem: Elem): String =
+ elem match {
+ case Root("") => ""
+ case Root(s) => "//" + s
+ case Basic(s) => s
+ case Variable(s) => "$" + s
+ case Parent => ".."
+ }
+
+
+ /* path constructors */
+
+ private def apply(xs: List[Elem]): Path =
+ new Path { override val elems = xs }
+
+ val current: Path = Path(Nil)
+ val root: Path = Path(List(Root("")))
+ def named_root(s: String): Path = Path(List(root_elem(s)))
+ def basic(s: String): Path = Path(List(basic_elem(s)))
+ def variable(s: String): Path = Path(List(variable_elem(s)))
+ val parent: Path = Path(List(Parent))
+
+
+ /* explode */
+
+ private def explode_elem(s: String): Elem =
+ if (s == "..") Parent
+ else if (s == "~") Variable("HOME")
+ else if (s == "~~") Variable("ISABELLE_HOME")
+ else if (s.startsWith("$")) variable_elem(s.substring(1))
+ else basic_elem(s)
+
+ private def explode_elems(ss: List[String]): List[Elem] =
+ ss.filterNot(s => s.isEmpty || s == ".").map(explode_elem).reverse
+
+ def explode(str: String): Path =
+ {
+ val ss = Library.space_explode('/', str)
+ val r = ss.takeWhile(_.isEmpty).length
+ val es = ss.dropWhile(_.isEmpty)
+ val (roots, raw_elems) =
+ if (r == 0) (Nil, es)
+ else if (r == 1) (List(Root("")), es)
+ else if (es.isEmpty) (List(Root("")), Nil)
+ else (List(root_elem(es.head)), es.tail)
+ Path(norm_elems(explode_elems(raw_elems) ++ roots))
+ }
+}
+
+class Path
+{
+ protected val elems: List[Path.Elem] = Nil // reversed elements
+
+ def is_current: Boolean = elems.isEmpty
+ def is_absolute: Boolean = !elems.isEmpty && elems.last.isInstanceOf[Path.Root]
+ def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false }
+
+ def +(other: Path): Path = Path((other.elems :\ elems)(Path.apply_elem))
+
+
+ /* implode */
+
+ def implode: String =
+ elems match {
+ case Nil => "."
+ case List(Path.Root("")) => "/"
+ case _ => elems.map(Path.implode_elem).reverse.mkString("/")
+ }
+
+ override def toString: String = Library.quote(implode)
+
+
+ /* base element */
+
+ private def split_path: (Path, String) =
+ elems match {
+ case Path.Basic(s) :: xs => (Path(xs), s)
+ case _ => error("Cannot split path into dir/base: " + toString)
+ }
+
+ def dir: Path = split_path._1
+ def base: Path = Path(List(Path.Basic(split_path._2)))
+
+ def ext(e: String): Path =
+ if (e == "") this
+ else {
+ val (prfx, s) = split_path
+ prfx + Path.basic(s + "." + e)
+ }
+
+
+ /* expand */
+
+ def expand(env: String => String): Path =
+ {
+ def eval(elem: Path.Elem): List[Path.Elem] =
+ elem match {
+ case Path.Variable(s) => Path.explode(env(s)).elems
+ case x => List(x)
+ }
+
+ Path(Path.norm_elems(elems.map(eval).flatten))
+ }
+}
--- a/src/Pure/ML-Systems/polyml_common.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML Thu Jun 30 16:07:30 2011 +0200
@@ -73,23 +73,6 @@
-(** OS related **)
-
-(* current directory *)
-
-val cd = OS.FileSys.chDir;
-val pwd = OS.FileSys.getDir;
-
-
-(* getenv *)
-
-fun getenv var =
- (case OS.Process.getEnv var of
- NONE => ""
- | SOME txt => txt);
-
-
-
(** Runtime system **)
val exception_trace = PolyML.exception_trace;
--- a/src/Pure/ML-Systems/smlnj.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML Thu Jun 30 16:07:30 2011 +0200
@@ -159,19 +159,3 @@
use "ML-Systems/unsynchronized.ML";
-
-
-(** OS related **)
-
-(* current directory *)
-
-val cd = OS.FileSys.chDir;
-val pwd = OS.FileSys.getDir;
-
-
-(* getenv *)
-
-fun getenv var =
- (case OS.Process.getEnv var of
- NONE => ""
- | SOME txt => txt);
--- a/src/Pure/ROOT.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Pure/ROOT.ML Thu Jun 30 16:07:30 2011 +0200
@@ -44,14 +44,14 @@
use "General/balanced_tree.ML";
use "General/graph.ML";
use "General/linear_set.ML";
+use "General/buffer.ML";
+use "General/xml.ML";
+use "General/xml_data.ML";
+use "General/pretty.ML";
use "General/path.ML";
use "General/url.ML";
-use "General/buffer.ML";
use "General/file.ML";
-use "General/xml.ML";
-use "General/xml_data.ML";
use "General/yxml.ML";
-use "General/pretty.ML";
use "General/long_name.ML";
use "General/binding.ML";
--- a/src/Pure/System/isabelle_system.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Pure/System/isabelle_system.ML Thu Jun 30 16:07:30 2011 +0200
@@ -22,7 +22,7 @@
fun isabelle_tool name args =
(case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
- let val path = dir ^ "/" ^ name in
+ let val path = File.platform_path (Path.append (Path.explode dir) (Path.basic name)) in
if can OS.FileSys.modTime path andalso
not (OS.FileSys.isDir path) andalso
OS.FileSys.access (path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
--- a/src/Pure/System/isabelle_system.scala Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Pure/System/isabelle_system.scala Thu Jun 30 16:07:30 2011 +0200
@@ -92,74 +92,19 @@
- /** file path specifications **/
+ /** file-system operations **/
- /* expand_path */
-
- private val Root = new Regex("(//+[^/]*|/)(.*)")
- private val Only_Root = new Regex("//+[^/]*|/")
+ /* path specifications */
- def expand_path(isabelle_path: String): String =
- {
- val result_path = new StringBuilder
- def init(path: String): String =
- {
- path match {
- case Root(root, rest) =>
- result_path.clear
- result_path ++= root
- rest
- case _ => path
- }
- }
- def append(path: String)
- {
- val rest = init(path)
- for (p <- rest.split("/") if p != "" && p != ".") {
- if (p == "..") {
- val result = result_path.toString
- if (!Only_Root.pattern.matcher(result).matches) {
- val i = result.lastIndexOf("/")
- if (result == "")
- result_path ++= ".."
- else if (result.substring(i + 1) == "..")
- result_path ++= "/.."
- else if (i < 0)
- result_path.length = 0
- else
- result_path.length = i
- }
- }
- else {
- val len = result_path.length
- if (len > 0 && result_path(len - 1) != '/')
- result_path += '/'
- result_path ++= p
- }
- }
- }
- val rest = init(isabelle_path)
- for (p <- rest.split("/")) {
- if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
- else if (p == "~") append(getenv_strict("HOME"))
- else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
- else append(p)
- }
- result_path.toString
- }
+ def standard_path(path: Path): String = path.expand(getenv_strict).implode
-
- /* platform_path */
-
- def platform_path(isabelle_path: String): String =
- jvm_path(expand_path(isabelle_path))
-
- def platform_file(path: String) = new File(platform_path(path))
+ def platform_path(path: Path): String = jvm_path(standard_path(path))
+ def platform_file(path: Path) = new File(platform_path(path))
/* try_read */
- def try_read(paths: Seq[String]): String =
+ def try_read(paths: Seq[Path]): String =
{
val buf = new StringBuilder
for {
@@ -175,15 +120,15 @@
private def try_file(file: File) = if (file.isFile) Some(file) else None
- def source_file(path: String): Option[File] =
+ def source_file(path: Path): Option[File] =
{
- if (path.startsWith("/") || path == "")
+ if (path.is_absolute || path.is_current)
try_file(platform_file(path))
else {
- val pure_file = platform_file("$ISABELLE_HOME/src/Pure/" + path)
+ val pure_file = platform_file(Path.explode("~~/src/Pure") + path)
if (pure_file.isFile) Some(pure_file)
else if (getenv("ML_SOURCES") != "")
- try_file(platform_file("$ML_SOURCES/" + path))
+ try_file(platform_file(Path.explode("$ML_SOURCES") + path))
else None
}
}
@@ -208,7 +153,7 @@
class Managed_Process(redirect: Boolean, args: String*)
{
private val params =
- List(expand_path("$ISABELLE_HOME/lib/scripts/process"), "group", "-", "no_script")
+ List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
private val proc = execute(redirect, (params ++ args):_*)
@@ -295,7 +240,7 @@
def isabelle_tool(name: String, args: String*): (String, Int) =
{
getenv_strict("ISABELLE_TOOLS").split(":").find { dir =>
- val file = platform_file(dir + "/" + name)
+ val file = platform_file(Path.explode(dir) + Path.basic(name))
try {
file.isFile && file.canRead && file.canExecute &&
!name.endsWith("~") && !name.endsWith(".orig")
@@ -303,8 +248,8 @@
catch { case _: SecurityException => false }
} match {
case Some(dir) =>
- Standard_System.process_output(
- execute(true, (List(expand_path(dir + "/" + name)) ++ args): _*))
+ val file = standard_path(Path.explode(dir) + Path.basic(name))
+ Standard_System.process_output(execute(true, (List(file) ++ args): _*))
case None => ("Unknown Isabelle tool: " + name, 2)
}
}
@@ -336,7 +281,7 @@
def fifo_input_stream(fifo: String): InputStream =
{
if (Platform.is_windows) { // Cygwin fifo as Windows/Java input stream
- val proc = execute(false, expand_path("$ISABELLE_HOME/lib/scripts/raw_dump"), fifo, "-")
+ val proc = execute(false, standard_path(Path.explode("~~/lib/scripts/raw_dump")), fifo, "-")
proc.getOutputStream.close
proc.getErrorStream.close
proc.getInputStream
@@ -347,7 +292,7 @@
def fifo_output_stream(fifo: String): OutputStream =
{
if (Platform.is_windows) { // Cygwin fifo as Windows/Java output stream
- val proc = execute(false, expand_path("$ISABELLE_HOME/lib/scripts/raw_dump"), "-", fifo)
+ val proc = execute(false, standard_path(Path.explode("~~/lib/scripts/raw_dump")), "-", fifo)
proc.getInputStream.close
proc.getErrorStream.close
val out = proc.getOutputStream
@@ -379,7 +324,7 @@
val ml_ident = getenv_strict("ML_IDENTIFIER")
val logics = new mutable.ListBuffer[String]
for (dir <- getenv_strict("ISABELLE_PATH").split(":")) {
- val files = platform_file(dir + "/" + ml_ident).listFiles()
+ val files = platform_file(Path.explode(dir) + Path.explode(ml_ident)).listFiles()
if (files != null) {
for (file <- files if file.isFile) logics += file.getName
}
@@ -391,7 +336,8 @@
/* symbols */
val symbols = new Symbol.Interpretation(
- try_read(getenv_strict("ISABELLE_SYMBOLS").split(":").toList).split("\n").toList)
+ try_read(getenv_strict("ISABELLE_SYMBOLS").split(":").toList.map(Path.explode))
+ .split("\n").toList)
/* fonts */
@@ -403,6 +349,6 @@
{
val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
for (font <- getenv_strict("ISABELLE_FONTS").split(":"))
- ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, platform_file(font)))
+ ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, platform_file(Path.explode(font))))
}
}
--- a/src/Pure/System/session_manager.scala Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Pure/System/session_manager.scala Thu Jun 30 16:07:30 2011 +0200
@@ -42,7 +42,7 @@
def component_sessions(): List[List[String]] =
{
val toplevel_sessions =
- system.components().map(system.platform_file(_)).filter(is_session_dir)
+ system.components().map(s => system.platform_file(Path.explode(s))).filter(is_session_dir)
((Nil: List[List[String]]) /: toplevel_sessions)(find_sessions(Nil, _, _)).reverse
}
}
--- a/src/Pure/Thy/html.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Pure/Thy/html.ML Thu Jun 30 16:07:30 2011 +0200
@@ -59,8 +59,9 @@
(* symbol output *)
local
- val hidden = XML.text #> (span Markup.hiddenN |-> enclose);
+ val hidden = span Markup.hiddenN |-> enclose;
+ (* FIXME proper unicode -- produced on Scala side *)
val html_syms = Symtab.make
[("", (0, "")),
("\n", (0, "<br/>")),
@@ -205,10 +206,10 @@
("\\<longleftrightarrow>", (3, "<->")),
("\\<longrightarrow>", (3, "-->")),
("\\<rightarrow>", (2, "->")),
- ("\\<^bsub>", (0, hidden "\\<^bsub>" ^ "<sub>")),
- ("\\<^esub>", (0, hidden "\\<^esub>" ^ "</sub>")),
- ("\\<^bsup>", (0, hidden "\\<^bsup>" ^ "<sup>")),
- ("\\<^esup>", (0, hidden "\\<^esup>" ^ "</sup>"))];
+ ("\\<^bsub>", (0, hidden "⇘" ^ "<sub>")),
+ ("\\<^esub>", (0, hidden "⇙" ^ "</sub>")),
+ ("\\<^bsup>", (0, hidden "⇗" ^ "<sup>")),
+ ("\\<^esup>", (0, hidden "⇖" ^ "</sup>"))];
fun output_sym s =
if Symbol.is_raw s then (1, Symbol.decode_raw s)
@@ -224,16 +225,17 @@
val output_sub = output_markup ("<sub>", "</sub>");
val output_sup = output_markup ("<sup>", "</sup>");
val output_bold = output_markup (span "bold");
- val output_loc = output_markup (span "loc");
fun output_syms [] (result, width) = (implode (rev result), width)
| output_syms (s1 :: rest) (result, width) =
let
val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss));
val ((w, s), r) =
- if s1 = "\\<^sub>" orelse s1 = "\\<^isub>" then (output_sub s1 s2, ss)
- else if s1 = "\\<^sup>" orelse s1 = "\\<^isup>" then (output_sup s1 s2, ss)
- else if s1 = "\\<^bold>" then (output_bold s1 s2, ss)
+ if s1 = "\\<^sub>" then (output_sub "⇩" s2, ss)
+ else if s1 = "\\<^isub>" then (output_sub "⇣" s2, ss)
+ else if s1 = "\\<^sup>" then (output_sup "⇧" s2, ss)
+ else if s1 = "\\<^isup>" then (output_sup "⇡" s2, ss)
+ else if s1 = "\\<^bold>" then (output_bold "❙" s2, ss)
else (output_sym s1, rest);
in output_syms r (s :: result, width + w) end;
in
--- a/src/Pure/build-jars Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Pure/build-jars Thu Jun 30 16:07:30 2011 +0200
@@ -16,6 +16,7 @@
General/timing.scala
General/linear_set.scala
General/markup.scala
+ General/path.scala
General/position.scala
General/pretty.scala
General/scan.scala
--- a/src/Pure/library.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Pure/library.ML Thu Jun 30 16:07:30 2011 +0200
@@ -218,6 +218,10 @@
val serial: unit -> serial
val serial_string: unit -> string
structure Object: sig type T = exn end
+ val cd: string -> unit
+ val pwd: unit -> string
+ val getenv: string -> string
+ val getenv_strict: string -> string
end;
signature LIBRARY =
@@ -1079,6 +1083,25 @@
constructors at any time*)
structure Object = struct type T = exn end;
+
+(* current directory *)
+
+val cd = OS.FileSys.chDir;
+val pwd = OS.FileSys.getDir;
+
+
+(* getenv *)
+
+fun getenv x =
+ (case OS.Process.getEnv x of
+ NONE => ""
+ | SOME y => y);
+
+fun getenv_strict x =
+ (case getenv x of
+ "" => error ("Undefined Isabelle environment variable: " ^ quote x)
+ | y => y);
+
end;
structure Basic_Library: BASIC_LIBRARY = Library;
--- a/src/Pure/library.scala Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Pure/library.scala Thu Jun 30 16:07:30 2011 +0200
@@ -13,11 +13,12 @@
import scala.swing.ComboBox
import scala.swing.event.SelectionChanged
+import scala.collection.mutable
object Library
{
- /* separate */
+ /* lists */
def separate[A](s: A, list: List[A]): List[A] =
list match {
@@ -25,6 +26,27 @@
case _ => list
}
+ def space_explode(sep: Char, str: String): List[String] =
+ if (str.isEmpty) Nil
+ else {
+ val result = new mutable.ListBuffer[String]
+ var start = 0
+ var finished = false
+ while (!finished) {
+ val i = str.indexOf(sep, start)
+ if (i == -1) { result += str.substring(start); finished = true }
+ else { result += str.substring(start, i); start = i + 1 }
+ }
+ result.toList
+ }
+
+
+ /* strings */
+
+ def quote(s: String): String = "\"" + s + "\""
+ def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
+ def commas_quote(ss: Iterable[String]): String = ss.iterator.mkString("\"", ", ", "\"")
+
/* reverse CharSequence */
--- a/src/Pure/pure_setup.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Pure/pure_setup.ML Thu Jun 30 16:07:30 2011 +0200
@@ -31,7 +31,7 @@
toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
toplevel_pp ["Ast", "ast"] "Ast.pretty_ast";
-toplevel_pp ["Path", "T"] "Pretty.str o Path.print";
+toplevel_pp ["Path", "T"] "Path.pretty";
toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep";
toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
--- a/src/Pure/raw_simplifier.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Pure/raw_simplifier.ML Thu Jun 30 16:07:30 2011 +0200
@@ -20,8 +20,7 @@
type simpset
type proc
type solver
- val mk_solver': string -> (simpset -> int -> tactic) -> solver
- val mk_solver: string -> (thm list -> int -> tactic) -> solver
+ val mk_solver: string -> (simpset -> int -> tactic) -> solver
val empty_ss: simpset
val merge_ss: simpset * simpset -> simpset
val dest_ss: simpset ->
@@ -38,7 +37,6 @@
val make_simproc: {name: string, lhss: cterm list,
proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> simproc
val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc
- val prems_of_ss: simpset -> thm list
val addsimps: simpset * thm list -> simpset
val delsimps: simpset * thm list -> simpset
val addeqcongs: simpset * thm list -> simpset
@@ -98,6 +96,7 @@
subgoal_tac: simpset -> int -> tactic,
loop_tacs: (string * (simpset -> int -> tactic)) list,
solvers: solver list * solver list}
+ val prems_of: simpset -> thm list
val add_simp: thm -> simpset -> simpset
val del_simp: thm -> simpset -> simpset
val solver: simpset -> solver -> int -> tactic
@@ -236,14 +235,13 @@
fun map_simpset1 f (Simpset (r1, r2)) = Simpset (map_ss1 f r1, r2);
fun map_simpset2 f (Simpset (r1, r2)) = Simpset (r1, map_ss2 f r2);
-fun prems_of_ss (Simpset ({prems, ...}, _)) = prems;
+fun prems_of (Simpset ({prems, ...}, _)) = prems;
fun eq_procid ((s1: stamp, ths1: thm list), (s2, ths2)) =
s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2);
fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = eq_procid (id1, id2);
-fun mk_solver' name solver = Solver {name = name, solver = solver, id = stamp ()};
-fun mk_solver name solver = mk_solver' name (solver o prems_of_ss);
+fun mk_solver name solver = Solver {name = name, solver = solver, id = stamp ()};
fun solver_name (Solver {name, ...}) = name;
fun solver ss (Solver {solver = tac, ...}) = tac ss;
@@ -564,7 +562,7 @@
fun is_full_cong thm =
let
- val prems = prems_of thm and concl = concl_of thm;
+ val prems = Thm.prems_of thm and concl = Thm.concl_of thm;
val (lhs, rhs) = Logic.dest_equals concl;
val (f, xs) = strip_comb lhs and (g, ys) = strip_comb rhs;
in
@@ -1280,7 +1278,7 @@
in bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ss ct end;
val simple_prover =
- SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of_ss ss)));
+ SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of ss)));
fun rewrite _ [] ct = Thm.reflexive ct
| rewrite full thms ct = rewrite_cterm (full, false, false) simple_prover
--- a/src/Pure/simplifier.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Pure/simplifier.ML Thu Jun 30 16:07:30 2011 +0200
@@ -34,6 +34,7 @@
val pretty_ss: Proof.context -> simpset -> Pretty.T
val clear_ss: simpset -> simpset
val debug_bounds: bool Unsynchronized.ref
+ val prems_of: simpset -> thm list
val add_simp: thm -> simpset -> simpset
val del_simp: thm -> simpset -> simpset
val add_prems: thm list -> simpset -> simpset
@@ -396,11 +397,13 @@
let
val trivialities = Drule.reflexive_thm :: trivs;
- fun unsafe_solver_tac prems = FIRST' [resolve_tac (trivialities @ prems), assume_tac];
+ fun unsafe_solver_tac ss =
+ FIRST' [resolve_tac (trivialities @ Raw_Simplifier.prems_of ss), assume_tac];
val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;
(*no premature instantiation of variables during simplification*)
- fun safe_solver_tac prems = FIRST' [match_tac (trivialities @ prems), eq_assume_tac];
+ fun safe_solver_tac ss =
+ FIRST' [match_tac (trivialities @ Raw_Simplifier.prems_of ss), eq_assume_tac];
val safe_solver = mk_solver "easy safe" safe_solver_tac;
fun mk_eq thm =
--- a/src/Sequents/simpdata.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Sequents/simpdata.ML Thu Jun 30 16:07:30 2011 +0200
@@ -58,12 +58,12 @@
val triv_rls = [@{thm FalseL}, @{thm TrueR}, @{thm basic}, @{thm refl},
@{thm iff_refl}, reflexive_thm];
-fun unsafe_solver prems =
- FIRST' [resolve_tac (triv_rls @ prems), assume_tac];
+fun unsafe_solver ss =
+ FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ss), assume_tac];
(*No premature instantiation of variables during simplification*)
-fun safe_solver prems =
- FIRST' [fn i => DETERM (match_tac (triv_rls @ prems) i), eq_assume_tac];
+fun safe_solver ss =
+ FIRST' [fn i => DETERM (match_tac (triv_rls @ Simplifier.prems_of ss) i), eq_assume_tac];
(*No simprules, but basic infrastructure for simplification*)
val LK_basic_ss =
--- a/src/Tools/WWW_Find/unicode_symbols.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Tools/WWW_Find/unicode_symbols.ML Thu Jun 30 16:07:30 2011 +0200
@@ -135,11 +135,6 @@
val line = (symbol -- unicode --| font -- abbr) >> Parse.triple1;
-val symbols_path =
- [getenv "ISABELLE_HOME", "etc", "symbols"]
- |> map Path.explode
- |> Path.appends;
-
end;
local (* build tables *)
@@ -164,8 +159,7 @@
fun read_symbols path =
let
val parsed_lines =
- File.read path
- |> (fn x => Symbol_Pos.explode (x, Position.file (Path.implode path)))
+ Symbol_Pos.explode (File.read path, Path.position path)
|> tokenize
|> filter is_proper
|> Scan.finite stopper (Scan.repeat line)
@@ -179,7 +173,7 @@
end;
local
-val (fromsym, fromabbr, tosym, toabbr) = read_symbols symbols_path;
+val (fromsym, fromabbr, tosym, toabbr) = read_symbols (Path.explode "~~/etc/symbols");
in
val symbol_to_unicode = Symtab.lookup fromsym;
val abbrev_to_unicode = Symtab.lookup fromabbr;
--- a/src/Tools/jEdit/src/html_panel.scala Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Tools/jEdit/src/html_panel.scala Thu Jun 30 16:07:30 2011 +0200
@@ -96,7 +96,7 @@
<head>
<style media="all" type="text/css">
""" +
- system.try_read(system.getenv_strict("JEDIT_STYLE_SHEETS").split(":"))
+ system.try_read(system.getenv_strict("JEDIT_STYLE_SHEETS").split(":").map(Path.explode))
private val template_tail =
"""
--- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala Thu Jun 30 16:07:30 2011 +0200
@@ -28,7 +28,7 @@
extends AbstractHyperlink(start, end, line, "")
{
override def click(view: View) = {
- Isabelle.system.source_file(def_file) match {
+ Isabelle.system.source_file(Path.explode(def_file)) match {
case None =>
Library.error_dialog(view, "File not found", "Could not find source file " + def_file)
case Some(file) =>
--- a/src/Tools/jEdit/src/session_dockable.scala Thu Jun 30 10:15:46 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala Thu Jun 30 16:07:30 2011 +0200
@@ -25,7 +25,7 @@
/* main tabs */
private val readme = new HTML_Panel(Isabelle.system, "SansSerif", 14)
- readme.render_document(Isabelle.system.try_read(List("$JEDIT_HOME/README.html")))
+ readme.render_document(Isabelle.system.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
private val syslog = new TextArea(Isabelle.session.syslog())
syslog.editable = false
--- a/src/ZF/Tools/inductive_package.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/ZF/Tools/inductive_package.ML Thu Jun 30 16:07:30 2011 +0200
@@ -329,7 +329,7 @@
val min_ss = Simplifier.global_context thy empty_ss
setmksimps (K (map mk_eq o ZF_atomize o gen_all))
setSolver (mk_solver "minimal"
- (fn prems => resolve_tac (triv_rls@prems)
+ (fn ss => resolve_tac (triv_rls @ Simplifier.prems_of ss)
ORELSE' assume_tac
ORELSE' etac @{thm FalseE}));
--- a/src/ZF/Tools/typechk.ML Thu Jun 30 10:15:46 2011 +0200
+++ b/src/ZF/Tools/typechk.ML Thu Jun 30 16:07:30 2011 +0200
@@ -105,8 +105,9 @@
ORELSE (ares_tac hyps 1
APPEND typecheck_step_tac (tcset_of ctxt))));
-val type_solver = Simplifier.mk_solver' "ZF typecheck" (fn ss =>
- type_solver_tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss));
+val type_solver =
+ Simplifier.mk_solver "ZF typecheck" (fn ss =>
+ type_solver_tac (Simplifier.the_context ss) (Simplifier.prems_of ss));
(* concrete syntax *)