1.1 --- a/src/HOL/Divides.thy Fri Dec 07 16:38:25 2012 +0100
1.2 +++ b/src/HOL/Divides.thy Fri Dec 07 17:00:40 2012 +0100
1.3 @@ -9,8 +9,6 @@
1.4 imports Nat_Transfer
1.5 begin
1.6
1.7 -ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
1.8 -
1.9 subsection {* Syntactic division operations *}
1.10
1.11 class div = dvd +
2.1 --- a/src/HOL/List.thy Fri Dec 07 16:38:25 2012 +0100
2.2 +++ b/src/HOL/List.thy Fri Dec 07 17:00:40 2012 +0100
2.3 @@ -504,7 +504,228 @@
2.4 *)
2.5
2.6
2.7 -ML_file "Tools/list_to_set_comprehension.ML"
2.8 +ML {*
2.9 +(* Simproc for rewriting list comprehensions applied to List.set to set
2.10 + comprehension. *)
2.11 +
2.12 +signature LIST_TO_SET_COMPREHENSION =
2.13 +sig
2.14 + val simproc : simpset -> cterm -> thm option
2.15 +end
2.16 +
2.17 +structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION =
2.18 +struct
2.19 +
2.20 +(* conversion *)
2.21 +
2.22 +fun all_exists_conv cv ctxt ct =
2.23 + (case Thm.term_of ct of
2.24 + Const (@{const_name HOL.Ex}, _) $ Abs _ =>
2.25 + Conv.arg_conv (Conv.abs_conv (all_exists_conv cv o #2) ctxt) ct
2.26 + | _ => cv ctxt ct)
2.27 +
2.28 +fun all_but_last_exists_conv cv ctxt ct =
2.29 + (case Thm.term_of ct of
2.30 + Const (@{const_name HOL.Ex}, _) $ Abs (_, _, Const (@{const_name HOL.Ex}, _) $ _) =>
2.31 + Conv.arg_conv (Conv.abs_conv (all_but_last_exists_conv cv o #2) ctxt) ct
2.32 + | _ => cv ctxt ct)
2.33 +
2.34 +fun Collect_conv cv ctxt ct =
2.35 + (case Thm.term_of ct of
2.36 + Const (@{const_name Set.Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct
2.37 + | _ => raise CTERM ("Collect_conv", [ct]))
2.38 +
2.39 +fun Trueprop_conv cv ct =
2.40 + (case Thm.term_of ct of
2.41 + Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
2.42 + | _ => raise CTERM ("Trueprop_conv", [ct]))
2.43 +
2.44 +fun eq_conv cv1 cv2 ct =
2.45 + (case Thm.term_of ct of
2.46 + Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
2.47 + | _ => raise CTERM ("eq_conv", [ct]))
2.48 +
2.49 +fun conj_conv cv1 cv2 ct =
2.50 + (case Thm.term_of ct of
2.51 + Const (@{const_name HOL.conj}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
2.52 + | _ => raise CTERM ("conj_conv", [ct]))
2.53 +
2.54 +fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th)
2.55 +
2.56 +fun conjunct_assoc_conv ct =
2.57 + Conv.try_conv
2.58 + (rewr_conv' @{thm conj_assoc} then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct
2.59 +
2.60 +fun right_hand_set_comprehension_conv conv ctxt =
2.61 + Trueprop_conv (eq_conv Conv.all_conv
2.62 + (Collect_conv (all_exists_conv conv o #2) ctxt))
2.63 +
2.64 +
2.65 +(* term abstraction of list comprehension patterns *)
2.66 +
2.67 +datatype termlets = If | Case of (typ * int)
2.68 +
2.69 +fun simproc ss redex =
2.70 + let
2.71 + val ctxt = Simplifier.the_context ss
2.72 + val thy = Proof_Context.theory_of ctxt
2.73 + val set_Nil_I = @{thm trans} OF [@{thm set.simps(1)}, @{thm empty_def}]
2.74 + val set_singleton = @{lemma "set [a] = {x. x = a}" by simp}
2.75 + val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp}
2.76 + val del_refl_eq = @{lemma "(t = t & P) == P" by simp}
2.77 + fun mk_set T = Const (@{const_name List.set}, HOLogic.listT T --> HOLogic.mk_setT T)
2.78 + fun dest_set (Const (@{const_name List.set}, _) $ xs) = xs
2.79 + fun dest_singleton_list (Const (@{const_name List.Cons}, _)
2.80 + $ t $ (Const (@{const_name List.Nil}, _))) = t
2.81 + | dest_singleton_list t = raise TERM ("dest_singleton_list", [t])
2.82 + (* We check that one case returns a singleton list and all other cases
2.83 + return [], and return the index of the one singleton list case *)
2.84 + fun possible_index_of_singleton_case cases =
2.85 + let
2.86 + fun check (i, case_t) s =
2.87 + (case strip_abs_body case_t of
2.88 + (Const (@{const_name List.Nil}, _)) => s
2.89 + | _ => (case s of NONE => SOME i | SOME _ => NONE))
2.90 + in
2.91 + fold_index check cases NONE
2.92 + end
2.93 + (* returns (case_expr type index chosen_case) option *)
2.94 + fun dest_case case_term =
2.95 + let
2.96 + val (case_const, args) = strip_comb case_term
2.97 + in
2.98 + (case try dest_Const case_const of
2.99 + SOME (c, T) =>
2.100 + (case Datatype.info_of_case thy c of
2.101 + SOME _ =>
2.102 + (case possible_index_of_singleton_case (fst (split_last args)) of
2.103 + SOME i =>
2.104 + let
2.105 + val (Ts, _) = strip_type T
2.106 + val T' = List.last Ts
2.107 + in SOME (List.last args, T', i, nth args i) end
2.108 + | NONE => NONE)
2.109 + | NONE => NONE)
2.110 + | NONE => NONE)
2.111 + end
2.112 + (* returns condition continuing term option *)
2.113 + fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) =
2.114 + SOME (cond, then_t)
2.115 + | dest_if _ = NONE
2.116 + fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1
2.117 + | tac ctxt (If :: cont) =
2.118 + Splitter.split_tac [@{thm split_if}] 1
2.119 + THEN rtac @{thm conjI} 1
2.120 + THEN rtac @{thm impI} 1
2.121 + THEN Subgoal.FOCUS (fn {prems, context, ...} =>
2.122 + CONVERSION (right_hand_set_comprehension_conv (K
2.123 + (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv
2.124 + then_conv
2.125 + rewr_conv' @{lemma "(True & P) = P" by simp})) context) 1) ctxt 1
2.126 + THEN tac ctxt cont
2.127 + THEN rtac @{thm impI} 1
2.128 + THEN Subgoal.FOCUS (fn {prems, context, ...} =>
2.129 + CONVERSION (right_hand_set_comprehension_conv (K
2.130 + (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv
2.131 + then_conv rewr_conv' @{lemma "(False & P) = False" by simp})) context) 1) ctxt 1
2.132 + THEN rtac set_Nil_I 1
2.133 + | tac ctxt (Case (T, i) :: cont) =
2.134 + let
2.135 + val info = Datatype.the_info thy (fst (dest_Type T))
2.136 + in
2.137 + (* do case distinction *)
2.138 + Splitter.split_tac [#split info] 1
2.139 + THEN EVERY (map_index (fn (i', _) =>
2.140 + (if i' < length (#case_rewrites info) - 1 then rtac @{thm conjI} 1 else all_tac)
2.141 + THEN REPEAT_DETERM (rtac @{thm allI} 1)
2.142 + THEN rtac @{thm impI} 1
2.143 + THEN (if i' = i then
2.144 + (* continue recursively *)
2.145 + Subgoal.FOCUS (fn {prems, context, ...} =>
2.146 + CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K
2.147 + ((conj_conv
2.148 + (eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv
2.149 + (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq (#inject info)))))
2.150 + Conv.all_conv)
2.151 + then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))
2.152 + then_conv conjunct_assoc_conv)) context
2.153 + then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
2.154 + Conv.repeat_conv
2.155 + (all_but_last_exists_conv
2.156 + (K (rewr_conv'
2.157 + @{lemma "(EX x. x = t & P x) = P t" by simp})) ctxt)) context)))) 1) ctxt 1
2.158 + THEN tac ctxt cont
2.159 + else
2.160 + Subgoal.FOCUS (fn {prems, context, ...} =>
2.161 + CONVERSION
2.162 + (right_hand_set_comprehension_conv (K
2.163 + (conj_conv
2.164 + ((eq_conv Conv.all_conv
2.165 + (rewr_conv' (List.last prems))) then_conv
2.166 + (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info))))
2.167 + Conv.all_conv then_conv
2.168 + (rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv
2.169 + Trueprop_conv
2.170 + (eq_conv Conv.all_conv
2.171 + (Collect_conv (fn (_, ctxt) =>
2.172 + Conv.repeat_conv
2.173 + (Conv.bottom_conv
2.174 + (K (rewr_conv'
2.175 + @{lemma "(EX x. P) = P" by simp})) ctxt)) context))) 1) ctxt 1
2.176 + THEN rtac set_Nil_I 1)) (#case_rewrites info))
2.177 + end
2.178 + fun make_inner_eqs bound_vs Tis eqs t =
2.179 + (case dest_case t of
2.180 + SOME (x, T, i, cont) =>
2.181 + let
2.182 + val (vs, body) = strip_abs (Pattern.eta_long (map snd bound_vs) cont)
2.183 + val x' = incr_boundvars (length vs) x
2.184 + val eqs' = map (incr_boundvars (length vs)) eqs
2.185 + val (constr_name, _) = nth (the (Datatype.get_constrs thy (fst (dest_Type T)))) i
2.186 + val constr_t =
2.187 + list_comb
2.188 + (Const (constr_name, map snd vs ---> T), map Bound (((length vs) - 1) downto 0))
2.189 + val constr_eq = Const (@{const_name HOL.eq}, T --> T --> @{typ bool}) $ constr_t $ x'
2.190 + in
2.191 + make_inner_eqs (rev vs @ bound_vs) (Case (T, i) :: Tis) (constr_eq :: eqs') body
2.192 + end
2.193 + | NONE =>
2.194 + (case dest_if t of
2.195 + SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont
2.196 + | NONE =>
2.197 + if eqs = [] then NONE (* no rewriting, nothing to be done *)
2.198 + else
2.199 + let
2.200 + val Type (@{type_name List.list}, [rT]) = fastype_of1 (map snd bound_vs, t)
2.201 + val pat_eq =
2.202 + (case try dest_singleton_list t of
2.203 + SOME t' =>
2.204 + Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool}) $
2.205 + Bound (length bound_vs) $ t'
2.206 + | NONE =>
2.207 + Const (@{const_name Set.member}, rT --> HOLogic.mk_setT rT --> @{typ bool}) $
2.208 + Bound (length bound_vs) $ (mk_set rT $ t))
2.209 + val reverse_bounds = curry subst_bounds
2.210 + ((map Bound ((length bound_vs - 1) downto 0)) @ [Bound (length bound_vs)])
2.211 + val eqs' = map reverse_bounds eqs
2.212 + val pat_eq' = reverse_bounds pat_eq
2.213 + val inner_t =
2.214 + fold (fn (_, T) => fn t => HOLogic.exists_const T $ absdummy T t)
2.215 + (rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq')
2.216 + val lhs = term_of redex
2.217 + val rhs = HOLogic.mk_Collect ("x", rT, inner_t)
2.218 + val rewrite_rule_t = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
2.219 + in
2.220 + SOME
2.221 + ((Goal.prove ctxt [] [] rewrite_rule_t
2.222 + (fn {context, ...} => tac context (rev Tis))) RS @{thm eq_reflection})
2.223 + end))
2.224 + in
2.225 + make_inner_eqs [] [] [] (dest_set (term_of redex))
2.226 + end
2.227 +
2.228 +end
2.229 +*}
2.230
2.231 simproc_setup list_to_set_comprehension ("set xs") = {* K List_to_Set_Comprehension.simproc *}
2.232
2.233 @@ -5664,7 +5885,57 @@
2.234
2.235 subsubsection {* Pretty lists *}
2.236
2.237 -ML_file "Tools/list_code.ML"
2.238 +ML {*
2.239 +(* Code generation for list literals. *)
2.240 +
2.241 +signature LIST_CODE =
2.242 +sig
2.243 + val implode_list: string -> string -> Code_Thingol.iterm -> Code_Thingol.iterm list option
2.244 + val default_list: int * string
2.245 + -> (Code_Printer.fixity -> Code_Thingol.iterm -> Pretty.T)
2.246 + -> Code_Printer.fixity -> Code_Thingol.iterm -> Code_Thingol.iterm -> Pretty.T
2.247 + val add_literal_list: string -> theory -> theory
2.248 +end;
2.249 +
2.250 +structure List_Code : LIST_CODE =
2.251 +struct
2.252 +
2.253 +open Basic_Code_Thingol;
2.254 +
2.255 +fun implode_list nil' cons' t =
2.256 + let
2.257 + fun dest_cons (IConst { name = c, ... } `$ t1 `$ t2) =
2.258 + if c = cons'
2.259 + then SOME (t1, t2)
2.260 + else NONE
2.261 + | dest_cons _ = NONE;
2.262 + val (ts, t') = Code_Thingol.unfoldr dest_cons t;
2.263 + in case t'
2.264 + of IConst { name = c, ... } => if c = nil' then SOME ts else NONE
2.265 + | _ => NONE
2.266 + end;
2.267 +
2.268 +fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
2.269 + Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy (
2.270 + pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
2.271 + Code_Printer.str target_cons,
2.272 + pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
2.273 + );
2.274 +
2.275 +fun add_literal_list target =
2.276 + let
2.277 + fun pretty literals [nil', cons'] pr thm vars fxy [(t1, _), (t2, _)] =
2.278 + case Option.map (cons t1) (implode_list nil' cons' t2)
2.279 + of SOME ts =>
2.280 + Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
2.281 + | NONE =>
2.282 + default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
2.283 + in Code_Target.add_const_syntax target @{const_name Cons}
2.284 + (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
2.285 + end
2.286 +
2.287 +end;
2.288 +*}
2.289
2.290 code_type list
2.291 (SML "_ list")
3.1 --- a/src/HOL/Nat_Transfer.thy Fri Dec 07 16:38:25 2012 +0100
3.2 +++ b/src/HOL/Nat_Transfer.thy Fri Dec 07 17:00:40 2012 +0100
3.3 @@ -420,4 +420,8 @@
3.4 return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
3.5 cong: setsum_cong setprod_cong]
3.6
3.7 +
3.8 +(*belongs to Divides.thy, but slows down dependency discovery*)
3.9 +ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
3.10 +
3.11 end
4.1 --- a/src/HOL/Tools/list_code.ML Fri Dec 07 16:38:25 2012 +0100
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,53 +0,0 @@
4.4 -(* Title: HOL/Tools/list_code.ML
4.5 - Author: Florian Haftmann, TU Muenchen
4.6 -
4.7 -Code generation for list literals.
4.8 -*)
4.9 -
4.10 -signature LIST_CODE =
4.11 -sig
4.12 - val implode_list: string -> string -> Code_Thingol.iterm -> Code_Thingol.iterm list option
4.13 - val default_list: int * string
4.14 - -> (Code_Printer.fixity -> Code_Thingol.iterm -> Pretty.T)
4.15 - -> Code_Printer.fixity -> Code_Thingol.iterm -> Code_Thingol.iterm -> Pretty.T
4.16 - val add_literal_list: string -> theory -> theory
4.17 -end;
4.18 -
4.19 -structure List_Code : LIST_CODE =
4.20 -struct
4.21 -
4.22 -open Basic_Code_Thingol;
4.23 -
4.24 -fun implode_list nil' cons' t =
4.25 - let
4.26 - fun dest_cons (IConst { name = c, ... } `$ t1 `$ t2) =
4.27 - if c = cons'
4.28 - then SOME (t1, t2)
4.29 - else NONE
4.30 - | dest_cons _ = NONE;
4.31 - val (ts, t') = Code_Thingol.unfoldr dest_cons t;
4.32 - in case t'
4.33 - of IConst { name = c, ... } => if c = nil' then SOME ts else NONE
4.34 - | _ => NONE
4.35 - end;
4.36 -
4.37 -fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
4.38 - Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy (
4.39 - pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
4.40 - Code_Printer.str target_cons,
4.41 - pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
4.42 - );
4.43 -
4.44 -fun add_literal_list target =
4.45 - let
4.46 - fun pretty literals [nil', cons'] pr thm vars fxy [(t1, _), (t2, _)] =
4.47 - case Option.map (cons t1) (implode_list nil' cons' t2)
4.48 - of SOME ts =>
4.49 - Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
4.50 - | NONE =>
4.51 - default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
4.52 - in Code_Target.add_const_syntax target @{const_name Cons}
4.53 - (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
4.54 - end
4.55 -
4.56 -end;
5.1 --- a/src/HOL/Tools/list_to_set_comprehension.ML Fri Dec 07 16:38:25 2012 +0100
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,224 +0,0 @@
5.4 -(* Title: HOL/Tools/list_to_set_comprehension.ML
5.5 - Author: Lukas Bulwahn, TU Muenchen
5.6 -
5.7 -Simproc for rewriting list comprehensions applied to List.set to set
5.8 -comprehension.
5.9 -*)
5.10 -
5.11 -signature LIST_TO_SET_COMPREHENSION =
5.12 -sig
5.13 - val simproc : simpset -> cterm -> thm option
5.14 -end
5.15 -
5.16 -structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION =
5.17 -struct
5.18 -
5.19 -(* conversion *)
5.20 -
5.21 -fun all_exists_conv cv ctxt ct =
5.22 - (case Thm.term_of ct of
5.23 - Const (@{const_name HOL.Ex}, _) $ Abs _ =>
5.24 - Conv.arg_conv (Conv.abs_conv (all_exists_conv cv o #2) ctxt) ct
5.25 - | _ => cv ctxt ct)
5.26 -
5.27 -fun all_but_last_exists_conv cv ctxt ct =
5.28 - (case Thm.term_of ct of
5.29 - Const (@{const_name HOL.Ex}, _) $ Abs (_, _, Const (@{const_name HOL.Ex}, _) $ _) =>
5.30 - Conv.arg_conv (Conv.abs_conv (all_but_last_exists_conv cv o #2) ctxt) ct
5.31 - | _ => cv ctxt ct)
5.32 -
5.33 -fun Collect_conv cv ctxt ct =
5.34 - (case Thm.term_of ct of
5.35 - Const (@{const_name Set.Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct
5.36 - | _ => raise CTERM ("Collect_conv", [ct]))
5.37 -
5.38 -fun Trueprop_conv cv ct =
5.39 - (case Thm.term_of ct of
5.40 - Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
5.41 - | _ => raise CTERM ("Trueprop_conv", [ct]))
5.42 -
5.43 -fun eq_conv cv1 cv2 ct =
5.44 - (case Thm.term_of ct of
5.45 - Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
5.46 - | _ => raise CTERM ("eq_conv", [ct]))
5.47 -
5.48 -fun conj_conv cv1 cv2 ct =
5.49 - (case Thm.term_of ct of
5.50 - Const (@{const_name HOL.conj}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
5.51 - | _ => raise CTERM ("conj_conv", [ct]))
5.52 -
5.53 -fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th)
5.54 -
5.55 -fun conjunct_assoc_conv ct =
5.56 - Conv.try_conv
5.57 - (rewr_conv' @{thm conj_assoc} then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct
5.58 -
5.59 -fun right_hand_set_comprehension_conv conv ctxt =
5.60 - Trueprop_conv (eq_conv Conv.all_conv
5.61 - (Collect_conv (all_exists_conv conv o #2) ctxt))
5.62 -
5.63 -
5.64 -(* term abstraction of list comprehension patterns *)
5.65 -
5.66 -datatype termlets = If | Case of (typ * int)
5.67 -
5.68 -fun simproc ss redex =
5.69 - let
5.70 - val ctxt = Simplifier.the_context ss
5.71 - val thy = Proof_Context.theory_of ctxt
5.72 - val set_Nil_I = @{thm trans} OF [@{thm set.simps(1)}, @{thm empty_def}]
5.73 - val set_singleton = @{lemma "set [a] = {x. x = a}" by simp}
5.74 - val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp}
5.75 - val del_refl_eq = @{lemma "(t = t & P) == P" by simp}
5.76 - fun mk_set T = Const (@{const_name List.set}, HOLogic.listT T --> HOLogic.mk_setT T)
5.77 - fun dest_set (Const (@{const_name List.set}, _) $ xs) = xs
5.78 - fun dest_singleton_list (Const (@{const_name List.Cons}, _)
5.79 - $ t $ (Const (@{const_name List.Nil}, _))) = t
5.80 - | dest_singleton_list t = raise TERM ("dest_singleton_list", [t])
5.81 - (* We check that one case returns a singleton list and all other cases
5.82 - return [], and return the index of the one singleton list case *)
5.83 - fun possible_index_of_singleton_case cases =
5.84 - let
5.85 - fun check (i, case_t) s =
5.86 - (case strip_abs_body case_t of
5.87 - (Const (@{const_name List.Nil}, _)) => s
5.88 - | _ => (case s of NONE => SOME i | SOME _ => NONE))
5.89 - in
5.90 - fold_index check cases NONE
5.91 - end
5.92 - (* returns (case_expr type index chosen_case) option *)
5.93 - fun dest_case case_term =
5.94 - let
5.95 - val (case_const, args) = strip_comb case_term
5.96 - in
5.97 - (case try dest_Const case_const of
5.98 - SOME (c, T) =>
5.99 - (case Datatype.info_of_case thy c of
5.100 - SOME _ =>
5.101 - (case possible_index_of_singleton_case (fst (split_last args)) of
5.102 - SOME i =>
5.103 - let
5.104 - val (Ts, _) = strip_type T
5.105 - val T' = List.last Ts
5.106 - in SOME (List.last args, T', i, nth args i) end
5.107 - | NONE => NONE)
5.108 - | NONE => NONE)
5.109 - | NONE => NONE)
5.110 - end
5.111 - (* returns condition continuing term option *)
5.112 - fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) =
5.113 - SOME (cond, then_t)
5.114 - | dest_if _ = NONE
5.115 - fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1
5.116 - | tac ctxt (If :: cont) =
5.117 - Splitter.split_tac [@{thm split_if}] 1
5.118 - THEN rtac @{thm conjI} 1
5.119 - THEN rtac @{thm impI} 1
5.120 - THEN Subgoal.FOCUS (fn {prems, context, ...} =>
5.121 - CONVERSION (right_hand_set_comprehension_conv (K
5.122 - (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv
5.123 - then_conv
5.124 - rewr_conv' @{lemma "(True & P) = P" by simp})) context) 1) ctxt 1
5.125 - THEN tac ctxt cont
5.126 - THEN rtac @{thm impI} 1
5.127 - THEN Subgoal.FOCUS (fn {prems, context, ...} =>
5.128 - CONVERSION (right_hand_set_comprehension_conv (K
5.129 - (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv
5.130 - then_conv rewr_conv' @{lemma "(False & P) = False" by simp})) context) 1) ctxt 1
5.131 - THEN rtac set_Nil_I 1
5.132 - | tac ctxt (Case (T, i) :: cont) =
5.133 - let
5.134 - val info = Datatype.the_info thy (fst (dest_Type T))
5.135 - in
5.136 - (* do case distinction *)
5.137 - Splitter.split_tac [#split info] 1
5.138 - THEN EVERY (map_index (fn (i', _) =>
5.139 - (if i' < length (#case_rewrites info) - 1 then rtac @{thm conjI} 1 else all_tac)
5.140 - THEN REPEAT_DETERM (rtac @{thm allI} 1)
5.141 - THEN rtac @{thm impI} 1
5.142 - THEN (if i' = i then
5.143 - (* continue recursively *)
5.144 - Subgoal.FOCUS (fn {prems, context, ...} =>
5.145 - CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K
5.146 - ((conj_conv
5.147 - (eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv
5.148 - (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq (#inject info)))))
5.149 - Conv.all_conv)
5.150 - then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))
5.151 - then_conv conjunct_assoc_conv)) context
5.152 - then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
5.153 - Conv.repeat_conv
5.154 - (all_but_last_exists_conv
5.155 - (K (rewr_conv'
5.156 - @{lemma "(EX x. x = t & P x) = P t" by simp})) ctxt)) context)))) 1) ctxt 1
5.157 - THEN tac ctxt cont
5.158 - else
5.159 - Subgoal.FOCUS (fn {prems, context, ...} =>
5.160 - CONVERSION
5.161 - (right_hand_set_comprehension_conv (K
5.162 - (conj_conv
5.163 - ((eq_conv Conv.all_conv
5.164 - (rewr_conv' (List.last prems))) then_conv
5.165 - (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info))))
5.166 - Conv.all_conv then_conv
5.167 - (rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv
5.168 - Trueprop_conv
5.169 - (eq_conv Conv.all_conv
5.170 - (Collect_conv (fn (_, ctxt) =>
5.171 - Conv.repeat_conv
5.172 - (Conv.bottom_conv
5.173 - (K (rewr_conv'
5.174 - @{lemma "(EX x. P) = P" by simp})) ctxt)) context))) 1) ctxt 1
5.175 - THEN rtac set_Nil_I 1)) (#case_rewrites info))
5.176 - end
5.177 - fun make_inner_eqs bound_vs Tis eqs t =
5.178 - (case dest_case t of
5.179 - SOME (x, T, i, cont) =>
5.180 - let
5.181 - val (vs, body) = strip_abs (Pattern.eta_long (map snd bound_vs) cont)
5.182 - val x' = incr_boundvars (length vs) x
5.183 - val eqs' = map (incr_boundvars (length vs)) eqs
5.184 - val (constr_name, _) = nth (the (Datatype.get_constrs thy (fst (dest_Type T)))) i
5.185 - val constr_t =
5.186 - list_comb
5.187 - (Const (constr_name, map snd vs ---> T), map Bound (((length vs) - 1) downto 0))
5.188 - val constr_eq = Const (@{const_name HOL.eq}, T --> T --> @{typ bool}) $ constr_t $ x'
5.189 - in
5.190 - make_inner_eqs (rev vs @ bound_vs) (Case (T, i) :: Tis) (constr_eq :: eqs') body
5.191 - end
5.192 - | NONE =>
5.193 - (case dest_if t of
5.194 - SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont
5.195 - | NONE =>
5.196 - if eqs = [] then NONE (* no rewriting, nothing to be done *)
5.197 - else
5.198 - let
5.199 - val Type (@{type_name List.list}, [rT]) = fastype_of1 (map snd bound_vs, t)
5.200 - val pat_eq =
5.201 - (case try dest_singleton_list t of
5.202 - SOME t' =>
5.203 - Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool}) $
5.204 - Bound (length bound_vs) $ t'
5.205 - | NONE =>
5.206 - Const (@{const_name Set.member}, rT --> HOLogic.mk_setT rT --> @{typ bool}) $
5.207 - Bound (length bound_vs) $ (mk_set rT $ t))
5.208 - val reverse_bounds = curry subst_bounds
5.209 - ((map Bound ((length bound_vs - 1) downto 0)) @ [Bound (length bound_vs)])
5.210 - val eqs' = map reverse_bounds eqs
5.211 - val pat_eq' = reverse_bounds pat_eq
5.212 - val inner_t =
5.213 - fold (fn (_, T) => fn t => HOLogic.exists_const T $ absdummy T t)
5.214 - (rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq')
5.215 - val lhs = term_of redex
5.216 - val rhs = HOLogic.mk_Collect ("x", rT, inner_t)
5.217 - val rewrite_rule_t = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
5.218 - in
5.219 - SOME
5.220 - ((Goal.prove ctxt [] [] rewrite_rule_t
5.221 - (fn {context, ...} => tac context (rev Tis))) RS @{thm eq_reflection})
5.222 - end))
5.223 - in
5.224 - make_inner_eqs [] [] [] (dest_set (term_of redex))
5.225 - end
5.226 -
5.227 -end
6.1 --- a/src/Pure/General/exn.scala Fri Dec 07 16:38:25 2012 +0100
6.2 +++ b/src/Pure/General/exn.scala Fri Dec 07 17:00:40 2012 +0100
6.3 @@ -45,5 +45,23 @@
6.4
6.5 def message(exn: Throwable): String =
6.6 user_message(exn) getOrElse exn.toString
6.7 +
6.8 +
6.9 + /* recover from spurious crash */
6.10 +
6.11 + def recover[A](e: => A): A =
6.12 + {
6.13 + capture(e) match {
6.14 + case Res(x) => x
6.15 + case Exn(exn) =>
6.16 + capture(e) match {
6.17 + case Res(x) =>
6.18 + java.lang.System.err.println("Recovered from spurious crash after retry!")
6.19 + exn.printStackTrace()
6.20 + x
6.21 + case Exn(_) => throw exn
6.22 + }
6.23 + }
6.24 + }
6.25 }
6.26
7.1 --- a/src/Pure/System/build.scala Fri Dec 07 16:38:25 2012 +0100
7.2 +++ b/src/Pure/System/build.scala Fri Dec 07 17:00:40 2012 +0100
7.3 @@ -376,9 +376,10 @@
7.4 val syntax = thy_deps.make_syntax
7.5
7.6 val all_files =
7.7 - (thy_deps.deps.map({ case (n, h) =>
7.8 - val thy = Path.explode(n.node)
7.9 - val uses = h.uses.map(p => Path.explode(n.dir) + Path.explode(p._1))
7.10 + (thy_deps.deps.map({ case dep =>
7.11 + val thy = Path.explode(dep.name.node)
7.12 + val uses = dep.join_header.uses.map(p =>
7.13 + Path.explode(dep.name.dir) + Path.explode(p._1))
7.14 thy :: uses
7.15 }).flatten ::: info.files.map(file => info.dir + file)).map(_.expand)
7.16
7.17 @@ -392,7 +393,7 @@
7.18 error(msg + "\nThe error(s) above occurred in session " +
7.19 quote(name) + Position.here(info.pos))
7.20 }
7.21 - val errors = parent_errors ::: thy_deps.deps.map(d => d._2.errors).flatten
7.22 + val errors = parent_errors ::: thy_deps.deps.map(dep => dep.join_header.errors).flatten
7.23
7.24 deps + (name -> Session_Content(loaded_theories, syntax, sources, errors))
7.25 }))
8.1 --- a/src/Pure/Thy/thy_info.scala Fri Dec 07 16:38:25 2012 +0100
8.2 +++ b/src/Pure/Thy/thy_info.scala Fri Dec 07 17:00:40 2012 +0100
8.3 @@ -7,6 +7,9 @@
8.4 package isabelle
8.5
8.6
8.7 +import java.util.concurrent.{Future => JFuture}
8.8 +
8.9 +
8.10 class Thy_Info(thy_load: Thy_Load)
8.11 {
8.12 /* messages */
8.13 @@ -24,7 +27,13 @@
8.14
8.15 /* dependencies */
8.16
8.17 - type Dep = (Document.Node.Name, Document.Node.Header)
8.18 + sealed case class Dep(
8.19 + name: Document.Node.Name,
8.20 + header0: Document.Node.Header,
8.21 + future_header: JFuture[Exn.Result[Document.Node.Header]])
8.22 + {
8.23 + def join_header: Document.Node.Header = Exn.release(future_header.get)
8.24 + }
8.25
8.26 object Dependencies
8.27 {
8.28 @@ -37,7 +46,7 @@
8.29 val seen: Set[Document.Node.Name])
8.30 {
8.31 def :: (dep: Dep): Dependencies =
8.32 - new Dependencies(dep :: rev_deps, dep._2.keywords ::: keywords, seen)
8.33 + new Dependencies(dep :: rev_deps, dep.header0.keywords ::: keywords, seen)
8.34
8.35 def + (name: Document.Node.Name): Dependencies =
8.36 new Dependencies(rev_deps, keywords, seen = seen + name)
8.37 @@ -45,7 +54,7 @@
8.38 def deps: List[Dep] = rev_deps.reverse
8.39
8.40 def loaded_theories: Set[String] =
8.41 - (thy_load.loaded_theories /: rev_deps) { case (loaded, (name, _)) => loaded + name.theory }
8.42 + (thy_load.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
8.43
8.44 def make_syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
8.45 }
8.46 @@ -60,24 +69,48 @@
8.47 if (required.seen(name)) required
8.48 else if (thy_load.loaded_theories(name.theory)) required + name
8.49 else {
8.50 + def err(msg: String): Nothing =
8.51 + cat_error(msg, "The error(s) above occurred while examining theory " +
8.52 + quote(name.theory) + required_by(initiators))
8.53 +
8.54 try {
8.55 if (initiators.contains(name)) error(cycle_msg(initiators))
8.56 val syntax = required.make_syntax
8.57 - val header =
8.58 - try {
8.59 - if (files) thy_load.check_thy_files(syntax, name)
8.60 - else thy_load.check_thy(name)
8.61 +
8.62 + val header0 =
8.63 + try { thy_load.check_thy(name) }
8.64 + catch { case ERROR(msg) => err(msg) }
8.65 +
8.66 + val future_header: JFuture[Exn.Result[Document.Node.Header]] =
8.67 + if (files) {
8.68 + val string = thy_load.with_thy_text(name, _.toString)
8.69 + val syntax0 = syntax.add_keywords(header0.keywords)
8.70 +
8.71 + if (thy_load.body_files_test(syntax0, string)) {
8.72 + /* FIXME
8.73 + unstable in scala-2.9.2 on multicore hardware -- spurious NPE
8.74 + OK in scala-2.10.0.RC3 */
8.75 + // default_thread_pool.submit(() =>
8.76 + Library.future_value(Exn.capture {
8.77 + try {
8.78 + val files = thy_load.body_files(syntax0, string)
8.79 + header0.copy(uses = header0.uses ::: files.map((_, false)))
8.80 + }
8.81 + catch { case ERROR(msg) => err(msg) }
8.82 + })
8.83 + //)
8.84 + }
8.85 + else Library.future_value(Exn.Res(header0))
8.86 }
8.87 - catch {
8.88 - case ERROR(msg) =>
8.89 - cat_error(msg, "The error(s) above occurred while examining theory " +
8.90 - quote(name.theory) + required_by(initiators))
8.91 - }
8.92 - (name, header) :: require_thys(files, name :: initiators, required + name, header.imports)
8.93 + else Library.future_value(Exn.Res(header0))
8.94 +
8.95 + Dep(name, header0, future_header) ::
8.96 + require_thys(files, name :: initiators, required + name, header0.imports)
8.97 }
8.98 catch {
8.99 case e: Throwable =>
8.100 - (name, Document.Node.bad_header(Exn.message(e))) :: (required + name)
8.101 + val bad_header = Document.Node.bad_header(Exn.message(e))
8.102 + Dep(name, bad_header, Library.future_value(Exn.Res(bad_header))) :: (required + name)
8.103 }
8.104 }
8.105 }
9.1 --- a/src/Pure/Thy/thy_load.scala Fri Dec 07 16:38:25 2012 +0100
9.2 +++ b/src/Pure/Thy/thy_load.scala Fri Dec 07 17:00:40 2012 +0100
9.3 @@ -80,53 +80,47 @@
9.4 clean_tokens.reverse.find(_.is_name).map(_.content)
9.5 }
9.6
9.7 - def find_files(syntax: Outer_Syntax, text: String): List[String] =
9.8 + def body_files_test(syntax: Outer_Syntax, text: String): Boolean =
9.9 + syntax.thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
9.10 +
9.11 + def body_files(syntax: Outer_Syntax, text: String): List[String] =
9.12 {
9.13 val thy_load_commands = syntax.thy_load_commands
9.14 - if (thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })) {
9.15 - val spans = Thy_Syntax.parse_spans(syntax.scan(text))
9.16 - spans.iterator.map({
9.17 - case toks @ (tok :: _) if tok.is_command =>
9.18 - thy_load_commands.find({ case (cmd, _) => cmd == tok.content }) match {
9.19 - case Some((_, exts)) =>
9.20 - find_file(toks) match {
9.21 - case Some(file) =>
9.22 - if (exts.isEmpty) List(file)
9.23 - else exts.map(ext => file + "." + ext)
9.24 - case None => Nil
9.25 - }
9.26 - case None => Nil
9.27 - }
9.28 - case _ => Nil
9.29 - }).flatten.toList
9.30 - }
9.31 - else Nil
9.32 + val spans = Thy_Syntax.parse_spans(syntax.scan(text))
9.33 + spans.iterator.map({
9.34 + case toks @ (tok :: _) if tok.is_command =>
9.35 + thy_load_commands.find({ case (cmd, _) => cmd == tok.content }) match {
9.36 + case Some((_, exts)) =>
9.37 + find_file(toks) match {
9.38 + case Some(file) =>
9.39 + if (exts.isEmpty) List(file)
9.40 + else exts.map(ext => file + "." + ext)
9.41 + case None => Nil
9.42 + }
9.43 + case None => Nil
9.44 + }
9.45 + case _ => Nil
9.46 + }).flatten.toList
9.47 }
9.48
9.49 def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header =
9.50 {
9.51 - val header = Thy_Header.read(text)
9.52 + try {
9.53 + val header = Thy_Header.read(text)
9.54
9.55 - val name1 = header.name
9.56 - if (name.theory != name1)
9.57 - error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
9.58 - " for theory " + quote(name1))
9.59 + val name1 = header.name
9.60 + if (name.theory != name1)
9.61 + error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
9.62 + " for theory " + quote(name1))
9.63
9.64 - val imports = header.imports.map(import_name(name.dir, _))
9.65 - val uses = header.uses
9.66 - Document.Node.Header(imports, header.keywords, uses)
9.67 + val imports = header.imports.map(import_name(name.dir, _))
9.68 + val uses = header.uses
9.69 + Document.Node.Header(imports, header.keywords, uses)
9.70 + }
9.71 + catch { case e: Throwable => Document.Node.bad_header(Exn.message(e)) }
9.72 }
9.73
9.74 def check_thy(name: Document.Node.Name): Document.Node.Header =
9.75 with_thy_text(name, check_thy_text(name, _))
9.76 -
9.77 - def check_thy_files(syntax: Outer_Syntax, name: Document.Node.Name): Document.Node.Header =
9.78 - with_thy_text(name, text =>
9.79 - {
9.80 - val string = text.toString
9.81 - val header = check_thy_text(name, string)
9.82 - val more_uses = find_files(syntax.add_keywords(header.keywords), string)
9.83 - header.copy(uses = header.uses ::: more_uses.map((_, false)))
9.84 - })
9.85 }
9.86
10.1 --- a/src/Pure/library.scala Fri Dec 07 16:38:25 2012 +0100
10.2 +++ b/src/Pure/library.scala Fri Dec 07 17:00:40 2012 +0100
10.3 @@ -10,6 +10,7 @@
10.4
10.5 import java.lang.System
10.6 import java.util.Locale
10.7 +import java.util.concurrent.{Future => JFuture, TimeUnit}
10.8 import java.awt.Component
10.9 import javax.swing.JOptionPane
10.10
10.11 @@ -187,6 +188,18 @@
10.12 selection.index = 3
10.13 prototypeDisplayValue = Some("00000%")
10.14 }
10.15 +
10.16 +
10.17 + /* Java futures */
10.18 +
10.19 + def future_value[A](x: A) = new JFuture[A]
10.20 + {
10.21 + def cancel(may_interrupt: Boolean): Boolean = false
10.22 + def isCancelled(): Boolean = false
10.23 + def isDone(): Boolean = true
10.24 + def get(): A = x
10.25 + def get(timeout: Long, time_unit: TimeUnit): A = x
10.26 + }
10.27 }
10.28
10.29
11.1 --- a/src/Tools/jEdit/lib/Tools/jedit Fri Dec 07 16:38:25 2012 +0100
11.2 +++ b/src/Tools/jEdit/lib/Tools/jedit Fri Dec 07 17:00:40 2012 +0100
11.3 @@ -316,21 +316,18 @@
11.4 fi
11.5
11.6
11.7 -# build logic
11.8 -
11.9 -if [ "$NO_BUILD" = false ]; then
11.10 - "$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}" -L jedit_logic "$JEDIT_LOGIC"
11.11 - RC="$?"
11.12 - [ "$RC" = 0 ] || exit "$RC"
11.13 -fi
11.14 -
11.15 -
11.16 # main
11.17
11.18 -[ "$BUILD_ONLY" = true ] || {
11.19 +if [ "$BUILD_ONLY" = false ]; then
11.20 + if [ "$NO_BUILD" = false ]; then
11.21 + "$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}" -L jedit_logic "$JEDIT_LOGIC"
11.22 + RC="$?"
11.23 + [ "$RC" = 0 ] || exit "$RC"
11.24 + fi
11.25 +
11.26 export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE
11.27
11.28 exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
11.29 -jar "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" \
11.30 "-settings=$(jvmpath "$JEDIT_SETTINGS")" "${ARGS[@]}"
11.31 -}
11.32 +fi
12.1 --- a/src/Tools/jEdit/src/plugin.scala Fri Dec 07 16:38:25 2012 +0100
12.2 +++ b/src/Tools/jEdit/src/plugin.scala Fri Dec 07 17:00:40 2012 +0100
12.3 @@ -157,7 +157,7 @@
12.4
12.5 val thy_info = new Thy_Info(PIDE.thy_load)
12.6 // FIXME avoid I/O in Swing thread!?!
12.7 - val files = thy_info.dependencies(true, thys).deps.map(_._1.node).
12.8 + val files = thy_info.dependencies(true, thys).deps.map(_.name.node).
12.9 filter(file => !loaded_buffer(file) && PIDE.thy_load.check_file(view, file))
12.10
12.11 if (!files.isEmpty) {