# HG changeset patch # User wenzelm # Date 1309442850 -7200 # Node ID 20760e3608fa3426d70fd02791cd77b93c024f83 # Parent 294570668f259aca47ea4054ac8010a772f0bb0c# Parent e1a09c2a6248119ebf1e76162110069884e2e23d merged diff -r 294570668f25 -r 20760e3608fa etc/isabelle.css --- 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; } diff -r 294570668f25 -r 20760e3608fa src/FOL/simpdata.ML --- 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 = diff -r 294570668f25 -r 20760e3608fa src/HOL/Decision_Procs/cooper_tac.ML --- 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 diff -r 294570668f25 -r 20760e3608fa src/HOL/Decision_Procs/mir_tac.ML --- 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 diff -r 294570668f25 -r 20760e3608fa src/HOL/Divides.thy --- 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 \ 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) diff -r 294570668f25 -r 20760e3608fa src/HOL/HOL.thy --- 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); diff -r 294570668f25 -r 20760e3608fa src/HOL/Int.thy --- 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) diff -r 294570668f25 -r 20760e3608fa src/HOL/List.thy --- 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; *} diff -r 294570668f25 -r 20760e3608fa src/HOL/Matrix/Compute_Oracle/am_ghc.ML --- 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 diff -r 294570668f25 -r 20760e3608fa src/HOL/Matrix/Cplex_tools.ML --- 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 = diff -r 294570668f25 -r 20760e3608fa src/HOL/NSA/HyperDef.thy --- 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 \ 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 \ 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 *} diff -r 294570668f25 -r 20760e3608fa src/HOL/Nat.thy --- 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 diff -r 294570668f25 -r 20760e3608fa src/HOL/Orderings.thy --- 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 [ diff -r 294570668f25 -r 20760e3608fa src/HOL/Product_Type.thy --- 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) diff -r 294570668f25 -r 20760e3608fa src/HOL/Statespace/distinct_tree_prover.ML --- 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"] diff -r 294570668f25 -r 20760e3608fa src/HOL/Statespace/state_space.ML --- 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"] diff -r 294570668f25 -r 20760e3608fa src/HOL/TLA/Memory/MemoryImplementation.thy --- 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); diff -r 294570668f25 -r 20760e3608fa src/HOL/Tools/ATP/atp_proof.ML --- 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 \ diff -r 294570668f25 -r 20760e3608fa src/HOL/Tools/Nitpick/nitpick.ML --- 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 diff -r 294570668f25 -r 20760e3608fa src/HOL/Tools/Qelim/cooper.ML --- 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"}] diff -r 294570668f25 -r 20760e3608fa src/HOL/Tools/Quickcheck/narrowing_generators.ML --- 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; diff -r 294570668f25 -r 20760e3608fa src/HOL/Tools/Quotient/quotient_tacs.ML --- 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 diff -r 294570668f25 -r 20760e3608fa src/HOL/Tools/SMT/z3_proof_tools.ML --- 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 => diff -r 294570668f25 -r 20760e3608fa src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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. *) diff -r 294570668f25 -r 20760e3608fa src/HOL/Tools/TFL/rules.ML --- 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 diff -r 294570668f25 -r 20760e3608fa src/HOL/Tools/int_arith.ML --- 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", []) diff -r 294570668f25 -r 20760e3608fa src/HOL/Tools/lin_arith.ML --- 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)) diff -r 294570668f25 -r 20760e3608fa src/HOL/Tools/simpdata.ML --- 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; diff -r 294570668f25 -r 20760e3608fa src/HOL/Transitive_Closure.thy --- 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))) *} diff -r 294570668f25 -r 20760e3608fa src/HOL/ex/atp_export.ML --- 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 diff -r 294570668f25 -r 20760e3608fa src/Provers/Arith/cancel_div_mod.ML --- 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 diff -r 294570668f25 -r 20760e3608fa src/Provers/Arith/cancel_numeral_factor.ML --- 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) diff -r 294570668f25 -r 20760e3608fa src/Provers/Arith/cancel_numerals.ML --- 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) diff -r 294570668f25 -r 20760e3608fa src/Provers/Arith/extract_common_term.ML --- 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) diff -r 294570668f25 -r 20760e3608fa src/Provers/Arith/fast_lin_arith.ML --- 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 diff -r 294570668f25 -r 20760e3608fa src/Pure/General/markup.ML --- 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"; diff -r 294570668f25 -r 20760e3608fa src/Pure/General/markup.scala --- 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 */ diff -r 294570668f25 -r 20760e3608fa src/Pure/General/path.ML --- 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 *) diff -r 294570668f25 -r 20760e3608fa src/Pure/General/path.scala --- /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)) + } +} diff -r 294570668f25 -r 20760e3608fa src/Pure/ML-Systems/polyml_common.ML --- 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; diff -r 294570668f25 -r 20760e3608fa src/Pure/ML-Systems/smlnj.ML --- 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); diff -r 294570668f25 -r 20760e3608fa src/Pure/ROOT.ML --- 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"; diff -r 294570668f25 -r 20760e3608fa src/Pure/System/isabelle_system.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]) diff -r 294570668f25 -r 20760e3608fa src/Pure/System/isabelle_system.scala --- 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)))) } } diff -r 294570668f25 -r 20760e3608fa src/Pure/System/session_manager.scala --- 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 } } diff -r 294570668f25 -r 20760e3608fa src/Pure/Thy/html.ML --- 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, "
")), @@ -205,10 +206,10 @@ ("\\", (3, "<->")), ("\\", (3, "-->")), ("\\", (2, "->")), - ("\\<^bsub>", (0, hidden "\\<^bsub>" ^ "")), - ("\\<^esub>", (0, hidden "\\<^esub>" ^ "")), - ("\\<^bsup>", (0, hidden "\\<^bsup>" ^ "")), - ("\\<^esup>", (0, hidden "\\<^esup>" ^ ""))]; + ("\\<^bsub>", (0, hidden "⇘" ^ "")), + ("\\<^esub>", (0, hidden "⇙" ^ "")), + ("\\<^bsup>", (0, hidden "⇗" ^ "")), + ("\\<^esup>", (0, hidden "⇖" ^ ""))]; fun output_sym s = if Symbol.is_raw s then (1, Symbol.decode_raw s) @@ -224,16 +225,17 @@ val output_sub = output_markup ("", ""); val output_sup = output_markup ("", ""); 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 diff -r 294570668f25 -r 20760e3608fa src/Pure/build-jars --- 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 diff -r 294570668f25 -r 20760e3608fa src/Pure/library.ML --- 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; diff -r 294570668f25 -r 20760e3608fa src/Pure/library.scala --- 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 */ diff -r 294570668f25 -r 20760e3608fa src/Pure/pure_setup.ML --- 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 \"\")"; toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract"; diff -r 294570668f25 -r 20760e3608fa src/Pure/raw_simplifier.ML --- 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 diff -r 294570668f25 -r 20760e3608fa src/Pure/simplifier.ML --- 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 = diff -r 294570668f25 -r 20760e3608fa src/Sequents/simpdata.ML --- 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 = diff -r 294570668f25 -r 20760e3608fa src/Tools/WWW_Find/unicode_symbols.ML --- 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; diff -r 294570668f25 -r 20760e3608fa src/Tools/jEdit/src/html_panel.scala --- 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 @@