--- a/src/HOL/Divides.thy Fri Dec 07 16:38:25 2012 +0100
+++ b/src/HOL/Divides.thy Fri Dec 07 17:00:40 2012 +0100
@@ -9,8 +9,6 @@
imports Nat_Transfer
begin
-ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
-
subsection {* Syntactic division operations *}
class div = dvd +
--- a/src/HOL/List.thy Fri Dec 07 16:38:25 2012 +0100
+++ b/src/HOL/List.thy Fri Dec 07 17:00:40 2012 +0100
@@ -504,7 +504,228 @@
*)
-ML_file "Tools/list_to_set_comprehension.ML"
+ML {*
+(* Simproc for rewriting list comprehensions applied to List.set to set
+ comprehension. *)
+
+signature LIST_TO_SET_COMPREHENSION =
+sig
+ val simproc : simpset -> cterm -> thm option
+end
+
+structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION =
+struct
+
+(* conversion *)
+
+fun all_exists_conv cv ctxt ct =
+ (case Thm.term_of ct of
+ Const (@{const_name HOL.Ex}, _) $ Abs _ =>
+ Conv.arg_conv (Conv.abs_conv (all_exists_conv cv o #2) ctxt) ct
+ | _ => cv ctxt ct)
+
+fun all_but_last_exists_conv cv ctxt ct =
+ (case Thm.term_of ct of
+ Const (@{const_name HOL.Ex}, _) $ Abs (_, _, Const (@{const_name HOL.Ex}, _) $ _) =>
+ Conv.arg_conv (Conv.abs_conv (all_but_last_exists_conv cv o #2) ctxt) ct
+ | _ => cv ctxt ct)
+
+fun Collect_conv cv ctxt ct =
+ (case Thm.term_of ct of
+ Const (@{const_name Set.Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct
+ | _ => raise CTERM ("Collect_conv", [ct]))
+
+fun Trueprop_conv cv ct =
+ (case Thm.term_of ct of
+ Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
+ | _ => raise CTERM ("Trueprop_conv", [ct]))
+
+fun eq_conv cv1 cv2 ct =
+ (case Thm.term_of ct of
+ Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
+ | _ => raise CTERM ("eq_conv", [ct]))
+
+fun conj_conv cv1 cv2 ct =
+ (case Thm.term_of ct of
+ Const (@{const_name HOL.conj}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
+ | _ => raise CTERM ("conj_conv", [ct]))
+
+fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th)
+
+fun conjunct_assoc_conv ct =
+ Conv.try_conv
+ (rewr_conv' @{thm conj_assoc} then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct
+
+fun right_hand_set_comprehension_conv conv ctxt =
+ Trueprop_conv (eq_conv Conv.all_conv
+ (Collect_conv (all_exists_conv conv o #2) ctxt))
+
+
+(* term abstraction of list comprehension patterns *)
+
+datatype termlets = If | Case of (typ * int)
+
+fun simproc ss redex =
+ let
+ val ctxt = Simplifier.the_context ss
+ val thy = Proof_Context.theory_of ctxt
+ val set_Nil_I = @{thm trans} OF [@{thm set.simps(1)}, @{thm empty_def}]
+ val set_singleton = @{lemma "set [a] = {x. x = a}" by simp}
+ val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp}
+ val del_refl_eq = @{lemma "(t = t & P) == P" by simp}
+ fun mk_set T = Const (@{const_name List.set}, HOLogic.listT T --> HOLogic.mk_setT T)
+ fun dest_set (Const (@{const_name List.set}, _) $ xs) = xs
+ fun dest_singleton_list (Const (@{const_name List.Cons}, _)
+ $ t $ (Const (@{const_name List.Nil}, _))) = t
+ | dest_singleton_list t = raise TERM ("dest_singleton_list", [t])
+ (* We check that one case returns a singleton list and all other cases
+ return [], and return the index of the one singleton list case *)
+ fun possible_index_of_singleton_case cases =
+ let
+ fun check (i, case_t) s =
+ (case strip_abs_body case_t of
+ (Const (@{const_name List.Nil}, _)) => s
+ | _ => (case s of NONE => SOME i | SOME _ => NONE))
+ in
+ fold_index check cases NONE
+ end
+ (* returns (case_expr type index chosen_case) option *)
+ fun dest_case case_term =
+ let
+ val (case_const, args) = strip_comb case_term
+ in
+ (case try dest_Const case_const of
+ SOME (c, T) =>
+ (case Datatype.info_of_case thy c of
+ SOME _ =>
+ (case possible_index_of_singleton_case (fst (split_last args)) of
+ SOME i =>
+ let
+ val (Ts, _) = strip_type T
+ val T' = List.last Ts
+ in SOME (List.last args, T', i, nth args i) end
+ | NONE => NONE)
+ | NONE => NONE)
+ | NONE => NONE)
+ end
+ (* returns condition continuing term option *)
+ fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) =
+ SOME (cond, then_t)
+ | dest_if _ = NONE
+ fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1
+ | tac ctxt (If :: cont) =
+ Splitter.split_tac [@{thm split_if}] 1
+ THEN rtac @{thm conjI} 1
+ THEN rtac @{thm impI} 1
+ THEN Subgoal.FOCUS (fn {prems, context, ...} =>
+ CONVERSION (right_hand_set_comprehension_conv (K
+ (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv
+ then_conv
+ rewr_conv' @{lemma "(True & P) = P" by simp})) context) 1) ctxt 1
+ THEN tac ctxt cont
+ THEN rtac @{thm impI} 1
+ THEN Subgoal.FOCUS (fn {prems, context, ...} =>
+ CONVERSION (right_hand_set_comprehension_conv (K
+ (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv
+ then_conv rewr_conv' @{lemma "(False & P) = False" by simp})) context) 1) ctxt 1
+ THEN rtac set_Nil_I 1
+ | tac ctxt (Case (T, i) :: cont) =
+ let
+ val info = Datatype.the_info thy (fst (dest_Type T))
+ in
+ (* do case distinction *)
+ Splitter.split_tac [#split info] 1
+ THEN EVERY (map_index (fn (i', _) =>
+ (if i' < length (#case_rewrites info) - 1 then rtac @{thm conjI} 1 else all_tac)
+ THEN REPEAT_DETERM (rtac @{thm allI} 1)
+ THEN rtac @{thm impI} 1
+ THEN (if i' = i then
+ (* continue recursively *)
+ Subgoal.FOCUS (fn {prems, context, ...} =>
+ CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K
+ ((conj_conv
+ (eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv
+ (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq (#inject info)))))
+ Conv.all_conv)
+ then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))
+ then_conv conjunct_assoc_conv)) context
+ then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
+ Conv.repeat_conv
+ (all_but_last_exists_conv
+ (K (rewr_conv'
+ @{lemma "(EX x. x = t & P x) = P t" by simp})) ctxt)) context)))) 1) ctxt 1
+ THEN tac ctxt cont
+ else
+ Subgoal.FOCUS (fn {prems, context, ...} =>
+ CONVERSION
+ (right_hand_set_comprehension_conv (K
+ (conj_conv
+ ((eq_conv Conv.all_conv
+ (rewr_conv' (List.last prems))) then_conv
+ (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info))))
+ Conv.all_conv then_conv
+ (rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv
+ Trueprop_conv
+ (eq_conv Conv.all_conv
+ (Collect_conv (fn (_, ctxt) =>
+ Conv.repeat_conv
+ (Conv.bottom_conv
+ (K (rewr_conv'
+ @{lemma "(EX x. P) = P" by simp})) ctxt)) context))) 1) ctxt 1
+ THEN rtac set_Nil_I 1)) (#case_rewrites info))
+ end
+ fun make_inner_eqs bound_vs Tis eqs t =
+ (case dest_case t of
+ SOME (x, T, i, cont) =>
+ let
+ val (vs, body) = strip_abs (Pattern.eta_long (map snd bound_vs) cont)
+ val x' = incr_boundvars (length vs) x
+ val eqs' = map (incr_boundvars (length vs)) eqs
+ val (constr_name, _) = nth (the (Datatype.get_constrs thy (fst (dest_Type T)))) i
+ val constr_t =
+ list_comb
+ (Const (constr_name, map snd vs ---> T), map Bound (((length vs) - 1) downto 0))
+ val constr_eq = Const (@{const_name HOL.eq}, T --> T --> @{typ bool}) $ constr_t $ x'
+ in
+ make_inner_eqs (rev vs @ bound_vs) (Case (T, i) :: Tis) (constr_eq :: eqs') body
+ end
+ | NONE =>
+ (case dest_if t of
+ SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont
+ | NONE =>
+ if eqs = [] then NONE (* no rewriting, nothing to be done *)
+ else
+ let
+ val Type (@{type_name List.list}, [rT]) = fastype_of1 (map snd bound_vs, t)
+ val pat_eq =
+ (case try dest_singleton_list t of
+ SOME t' =>
+ Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool}) $
+ Bound (length bound_vs) $ t'
+ | NONE =>
+ Const (@{const_name Set.member}, rT --> HOLogic.mk_setT rT --> @{typ bool}) $
+ Bound (length bound_vs) $ (mk_set rT $ t))
+ val reverse_bounds = curry subst_bounds
+ ((map Bound ((length bound_vs - 1) downto 0)) @ [Bound (length bound_vs)])
+ val eqs' = map reverse_bounds eqs
+ val pat_eq' = reverse_bounds pat_eq
+ val inner_t =
+ fold (fn (_, T) => fn t => HOLogic.exists_const T $ absdummy T t)
+ (rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq')
+ val lhs = term_of redex
+ val rhs = HOLogic.mk_Collect ("x", rT, inner_t)
+ val rewrite_rule_t = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ in
+ SOME
+ ((Goal.prove ctxt [] [] rewrite_rule_t
+ (fn {context, ...} => tac context (rev Tis))) RS @{thm eq_reflection})
+ end))
+ in
+ make_inner_eqs [] [] [] (dest_set (term_of redex))
+ end
+
+end
+*}
simproc_setup list_to_set_comprehension ("set xs") = {* K List_to_Set_Comprehension.simproc *}
@@ -5664,7 +5885,57 @@
subsubsection {* Pretty lists *}
-ML_file "Tools/list_code.ML"
+ML {*
+(* Code generation for list literals. *)
+
+signature LIST_CODE =
+sig
+ val implode_list: string -> string -> Code_Thingol.iterm -> Code_Thingol.iterm list option
+ val default_list: int * string
+ -> (Code_Printer.fixity -> Code_Thingol.iterm -> Pretty.T)
+ -> Code_Printer.fixity -> Code_Thingol.iterm -> Code_Thingol.iterm -> Pretty.T
+ val add_literal_list: string -> theory -> theory
+end;
+
+structure List_Code : LIST_CODE =
+struct
+
+open Basic_Code_Thingol;
+
+fun implode_list nil' cons' t =
+ let
+ fun dest_cons (IConst { name = c, ... } `$ t1 `$ t2) =
+ if c = cons'
+ then SOME (t1, t2)
+ else NONE
+ | dest_cons _ = NONE;
+ val (ts, t') = Code_Thingol.unfoldr dest_cons t;
+ in case t'
+ of IConst { name = c, ... } => if c = nil' then SOME ts else NONE
+ | _ => NONE
+ end;
+
+fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
+ Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy (
+ pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
+ Code_Printer.str target_cons,
+ pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
+ );
+
+fun add_literal_list target =
+ let
+ fun pretty literals [nil', cons'] pr thm vars fxy [(t1, _), (t2, _)] =
+ case Option.map (cons t1) (implode_list nil' cons' t2)
+ of SOME ts =>
+ Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
+ | NONE =>
+ default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
+ in Code_Target.add_const_syntax target @{const_name Cons}
+ (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
+ end
+
+end;
+*}
code_type list
(SML "_ list")
--- a/src/HOL/Nat_Transfer.thy Fri Dec 07 16:38:25 2012 +0100
+++ b/src/HOL/Nat_Transfer.thy Fri Dec 07 17:00:40 2012 +0100
@@ -420,4 +420,8 @@
return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
cong: setsum_cong setprod_cong]
+
+(*belongs to Divides.thy, but slows down dependency discovery*)
+ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
+
end
--- a/src/HOL/Tools/list_code.ML Fri Dec 07 16:38:25 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-(* Title: HOL/Tools/list_code.ML
- Author: Florian Haftmann, TU Muenchen
-
-Code generation for list literals.
-*)
-
-signature LIST_CODE =
-sig
- val implode_list: string -> string -> Code_Thingol.iterm -> Code_Thingol.iterm list option
- val default_list: int * string
- -> (Code_Printer.fixity -> Code_Thingol.iterm -> Pretty.T)
- -> Code_Printer.fixity -> Code_Thingol.iterm -> Code_Thingol.iterm -> Pretty.T
- val add_literal_list: string -> theory -> theory
-end;
-
-structure List_Code : LIST_CODE =
-struct
-
-open Basic_Code_Thingol;
-
-fun implode_list nil' cons' t =
- let
- fun dest_cons (IConst { name = c, ... } `$ t1 `$ t2) =
- if c = cons'
- then SOME (t1, t2)
- else NONE
- | dest_cons _ = NONE;
- val (ts, t') = Code_Thingol.unfoldr dest_cons t;
- in case t'
- of IConst { name = c, ... } => if c = nil' then SOME ts else NONE
- | _ => NONE
- end;
-
-fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
- Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy (
- pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
- Code_Printer.str target_cons,
- pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
- );
-
-fun add_literal_list target =
- let
- fun pretty literals [nil', cons'] pr thm vars fxy [(t1, _), (t2, _)] =
- case Option.map (cons t1) (implode_list nil' cons' t2)
- of SOME ts =>
- Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
- | NONE =>
- default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
- in Code_Target.add_const_syntax target @{const_name Cons}
- (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
- end
-
-end;
--- a/src/HOL/Tools/list_to_set_comprehension.ML Fri Dec 07 16:38:25 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,224 +0,0 @@
-(* Title: HOL/Tools/list_to_set_comprehension.ML
- Author: Lukas Bulwahn, TU Muenchen
-
-Simproc for rewriting list comprehensions applied to List.set to set
-comprehension.
-*)
-
-signature LIST_TO_SET_COMPREHENSION =
-sig
- val simproc : simpset -> cterm -> thm option
-end
-
-structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION =
-struct
-
-(* conversion *)
-
-fun all_exists_conv cv ctxt ct =
- (case Thm.term_of ct of
- Const (@{const_name HOL.Ex}, _) $ Abs _ =>
- Conv.arg_conv (Conv.abs_conv (all_exists_conv cv o #2) ctxt) ct
- | _ => cv ctxt ct)
-
-fun all_but_last_exists_conv cv ctxt ct =
- (case Thm.term_of ct of
- Const (@{const_name HOL.Ex}, _) $ Abs (_, _, Const (@{const_name HOL.Ex}, _) $ _) =>
- Conv.arg_conv (Conv.abs_conv (all_but_last_exists_conv cv o #2) ctxt) ct
- | _ => cv ctxt ct)
-
-fun Collect_conv cv ctxt ct =
- (case Thm.term_of ct of
- Const (@{const_name Set.Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct
- | _ => raise CTERM ("Collect_conv", [ct]))
-
-fun Trueprop_conv cv ct =
- (case Thm.term_of ct of
- Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
- | _ => raise CTERM ("Trueprop_conv", [ct]))
-
-fun eq_conv cv1 cv2 ct =
- (case Thm.term_of ct of
- Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
- | _ => raise CTERM ("eq_conv", [ct]))
-
-fun conj_conv cv1 cv2 ct =
- (case Thm.term_of ct of
- Const (@{const_name HOL.conj}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
- | _ => raise CTERM ("conj_conv", [ct]))
-
-fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th)
-
-fun conjunct_assoc_conv ct =
- Conv.try_conv
- (rewr_conv' @{thm conj_assoc} then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct
-
-fun right_hand_set_comprehension_conv conv ctxt =
- Trueprop_conv (eq_conv Conv.all_conv
- (Collect_conv (all_exists_conv conv o #2) ctxt))
-
-
-(* term abstraction of list comprehension patterns *)
-
-datatype termlets = If | Case of (typ * int)
-
-fun simproc ss redex =
- let
- val ctxt = Simplifier.the_context ss
- val thy = Proof_Context.theory_of ctxt
- val set_Nil_I = @{thm trans} OF [@{thm set.simps(1)}, @{thm empty_def}]
- val set_singleton = @{lemma "set [a] = {x. x = a}" by simp}
- val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp}
- val del_refl_eq = @{lemma "(t = t & P) == P" by simp}
- fun mk_set T = Const (@{const_name List.set}, HOLogic.listT T --> HOLogic.mk_setT T)
- fun dest_set (Const (@{const_name List.set}, _) $ xs) = xs
- fun dest_singleton_list (Const (@{const_name List.Cons}, _)
- $ t $ (Const (@{const_name List.Nil}, _))) = t
- | dest_singleton_list t = raise TERM ("dest_singleton_list", [t])
- (* We check that one case returns a singleton list and all other cases
- return [], and return the index of the one singleton list case *)
- fun possible_index_of_singleton_case cases =
- let
- fun check (i, case_t) s =
- (case strip_abs_body case_t of
- (Const (@{const_name List.Nil}, _)) => s
- | _ => (case s of NONE => SOME i | SOME _ => NONE))
- in
- fold_index check cases NONE
- end
- (* returns (case_expr type index chosen_case) option *)
- fun dest_case case_term =
- let
- val (case_const, args) = strip_comb case_term
- in
- (case try dest_Const case_const of
- SOME (c, T) =>
- (case Datatype.info_of_case thy c of
- SOME _ =>
- (case possible_index_of_singleton_case (fst (split_last args)) of
- SOME i =>
- let
- val (Ts, _) = strip_type T
- val T' = List.last Ts
- in SOME (List.last args, T', i, nth args i) end
- | NONE => NONE)
- | NONE => NONE)
- | NONE => NONE)
- end
- (* returns condition continuing term option *)
- fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) =
- SOME (cond, then_t)
- | dest_if _ = NONE
- fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1
- | tac ctxt (If :: cont) =
- Splitter.split_tac [@{thm split_if}] 1
- THEN rtac @{thm conjI} 1
- THEN rtac @{thm impI} 1
- THEN Subgoal.FOCUS (fn {prems, context, ...} =>
- CONVERSION (right_hand_set_comprehension_conv (K
- (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv
- then_conv
- rewr_conv' @{lemma "(True & P) = P" by simp})) context) 1) ctxt 1
- THEN tac ctxt cont
- THEN rtac @{thm impI} 1
- THEN Subgoal.FOCUS (fn {prems, context, ...} =>
- CONVERSION (right_hand_set_comprehension_conv (K
- (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv
- then_conv rewr_conv' @{lemma "(False & P) = False" by simp})) context) 1) ctxt 1
- THEN rtac set_Nil_I 1
- | tac ctxt (Case (T, i) :: cont) =
- let
- val info = Datatype.the_info thy (fst (dest_Type T))
- in
- (* do case distinction *)
- Splitter.split_tac [#split info] 1
- THEN EVERY (map_index (fn (i', _) =>
- (if i' < length (#case_rewrites info) - 1 then rtac @{thm conjI} 1 else all_tac)
- THEN REPEAT_DETERM (rtac @{thm allI} 1)
- THEN rtac @{thm impI} 1
- THEN (if i' = i then
- (* continue recursively *)
- Subgoal.FOCUS (fn {prems, context, ...} =>
- CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K
- ((conj_conv
- (eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv
- (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq (#inject info)))))
- Conv.all_conv)
- then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))
- then_conv conjunct_assoc_conv)) context
- then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
- Conv.repeat_conv
- (all_but_last_exists_conv
- (K (rewr_conv'
- @{lemma "(EX x. x = t & P x) = P t" by simp})) ctxt)) context)))) 1) ctxt 1
- THEN tac ctxt cont
- else
- Subgoal.FOCUS (fn {prems, context, ...} =>
- CONVERSION
- (right_hand_set_comprehension_conv (K
- (conj_conv
- ((eq_conv Conv.all_conv
- (rewr_conv' (List.last prems))) then_conv
- (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info))))
- Conv.all_conv then_conv
- (rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv
- Trueprop_conv
- (eq_conv Conv.all_conv
- (Collect_conv (fn (_, ctxt) =>
- Conv.repeat_conv
- (Conv.bottom_conv
- (K (rewr_conv'
- @{lemma "(EX x. P) = P" by simp})) ctxt)) context))) 1) ctxt 1
- THEN rtac set_Nil_I 1)) (#case_rewrites info))
- end
- fun make_inner_eqs bound_vs Tis eqs t =
- (case dest_case t of
- SOME (x, T, i, cont) =>
- let
- val (vs, body) = strip_abs (Pattern.eta_long (map snd bound_vs) cont)
- val x' = incr_boundvars (length vs) x
- val eqs' = map (incr_boundvars (length vs)) eqs
- val (constr_name, _) = nth (the (Datatype.get_constrs thy (fst (dest_Type T)))) i
- val constr_t =
- list_comb
- (Const (constr_name, map snd vs ---> T), map Bound (((length vs) - 1) downto 0))
- val constr_eq = Const (@{const_name HOL.eq}, T --> T --> @{typ bool}) $ constr_t $ x'
- in
- make_inner_eqs (rev vs @ bound_vs) (Case (T, i) :: Tis) (constr_eq :: eqs') body
- end
- | NONE =>
- (case dest_if t of
- SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont
- | NONE =>
- if eqs = [] then NONE (* no rewriting, nothing to be done *)
- else
- let
- val Type (@{type_name List.list}, [rT]) = fastype_of1 (map snd bound_vs, t)
- val pat_eq =
- (case try dest_singleton_list t of
- SOME t' =>
- Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool}) $
- Bound (length bound_vs) $ t'
- | NONE =>
- Const (@{const_name Set.member}, rT --> HOLogic.mk_setT rT --> @{typ bool}) $
- Bound (length bound_vs) $ (mk_set rT $ t))
- val reverse_bounds = curry subst_bounds
- ((map Bound ((length bound_vs - 1) downto 0)) @ [Bound (length bound_vs)])
- val eqs' = map reverse_bounds eqs
- val pat_eq' = reverse_bounds pat_eq
- val inner_t =
- fold (fn (_, T) => fn t => HOLogic.exists_const T $ absdummy T t)
- (rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq')
- val lhs = term_of redex
- val rhs = HOLogic.mk_Collect ("x", rT, inner_t)
- val rewrite_rule_t = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
- in
- SOME
- ((Goal.prove ctxt [] [] rewrite_rule_t
- (fn {context, ...} => tac context (rev Tis))) RS @{thm eq_reflection})
- end))
- in
- make_inner_eqs [] [] [] (dest_set (term_of redex))
- end
-
-end
--- a/src/Pure/General/exn.scala Fri Dec 07 16:38:25 2012 +0100
+++ b/src/Pure/General/exn.scala Fri Dec 07 17:00:40 2012 +0100
@@ -45,5 +45,23 @@
def message(exn: Throwable): String =
user_message(exn) getOrElse exn.toString
+
+
+ /* recover from spurious crash */
+
+ def recover[A](e: => A): A =
+ {
+ capture(e) match {
+ case Res(x) => x
+ case Exn(exn) =>
+ capture(e) match {
+ case Res(x) =>
+ java.lang.System.err.println("Recovered from spurious crash after retry!")
+ exn.printStackTrace()
+ x
+ case Exn(_) => throw exn
+ }
+ }
+ }
}
--- a/src/Pure/System/build.scala Fri Dec 07 16:38:25 2012 +0100
+++ b/src/Pure/System/build.scala Fri Dec 07 17:00:40 2012 +0100
@@ -376,9 +376,10 @@
val syntax = thy_deps.make_syntax
val all_files =
- (thy_deps.deps.map({ case (n, h) =>
- val thy = Path.explode(n.node)
- val uses = h.uses.map(p => Path.explode(n.dir) + Path.explode(p._1))
+ (thy_deps.deps.map({ case dep =>
+ val thy = Path.explode(dep.name.node)
+ val uses = dep.join_header.uses.map(p =>
+ Path.explode(dep.name.dir) + Path.explode(p._1))
thy :: uses
}).flatten ::: info.files.map(file => info.dir + file)).map(_.expand)
@@ -392,7 +393,7 @@
error(msg + "\nThe error(s) above occurred in session " +
quote(name) + Position.here(info.pos))
}
- val errors = parent_errors ::: thy_deps.deps.map(d => d._2.errors).flatten
+ val errors = parent_errors ::: thy_deps.deps.map(dep => dep.join_header.errors).flatten
deps + (name -> Session_Content(loaded_theories, syntax, sources, errors))
}))
--- a/src/Pure/Thy/thy_info.scala Fri Dec 07 16:38:25 2012 +0100
+++ b/src/Pure/Thy/thy_info.scala Fri Dec 07 17:00:40 2012 +0100
@@ -7,6 +7,9 @@
package isabelle
+import java.util.concurrent.{Future => JFuture}
+
+
class Thy_Info(thy_load: Thy_Load)
{
/* messages */
@@ -24,7 +27,13 @@
/* dependencies */
- type Dep = (Document.Node.Name, Document.Node.Header)
+ sealed case class Dep(
+ name: Document.Node.Name,
+ header0: Document.Node.Header,
+ future_header: JFuture[Exn.Result[Document.Node.Header]])
+ {
+ def join_header: Document.Node.Header = Exn.release(future_header.get)
+ }
object Dependencies
{
@@ -37,7 +46,7 @@
val seen: Set[Document.Node.Name])
{
def :: (dep: Dep): Dependencies =
- new Dependencies(dep :: rev_deps, dep._2.keywords ::: keywords, seen)
+ new Dependencies(dep :: rev_deps, dep.header0.keywords ::: keywords, seen)
def + (name: Document.Node.Name): Dependencies =
new Dependencies(rev_deps, keywords, seen = seen + name)
@@ -45,7 +54,7 @@
def deps: List[Dep] = rev_deps.reverse
def loaded_theories: Set[String] =
- (thy_load.loaded_theories /: rev_deps) { case (loaded, (name, _)) => loaded + name.theory }
+ (thy_load.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
def make_syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
}
@@ -60,24 +69,48 @@
if (required.seen(name)) required
else if (thy_load.loaded_theories(name.theory)) required + name
else {
+ def err(msg: String): Nothing =
+ cat_error(msg, "The error(s) above occurred while examining theory " +
+ quote(name.theory) + required_by(initiators))
+
try {
if (initiators.contains(name)) error(cycle_msg(initiators))
val syntax = required.make_syntax
- val header =
- try {
- if (files) thy_load.check_thy_files(syntax, name)
- else thy_load.check_thy(name)
+
+ val header0 =
+ try { thy_load.check_thy(name) }
+ catch { case ERROR(msg) => err(msg) }
+
+ val future_header: JFuture[Exn.Result[Document.Node.Header]] =
+ if (files) {
+ val string = thy_load.with_thy_text(name, _.toString)
+ val syntax0 = syntax.add_keywords(header0.keywords)
+
+ if (thy_load.body_files_test(syntax0, string)) {
+ /* FIXME
+ unstable in scala-2.9.2 on multicore hardware -- spurious NPE
+ OK in scala-2.10.0.RC3 */
+ // default_thread_pool.submit(() =>
+ Library.future_value(Exn.capture {
+ try {
+ val files = thy_load.body_files(syntax0, string)
+ header0.copy(uses = header0.uses ::: files.map((_, false)))
+ }
+ catch { case ERROR(msg) => err(msg) }
+ })
+ //)
+ }
+ else Library.future_value(Exn.Res(header0))
}
- catch {
- case ERROR(msg) =>
- cat_error(msg, "The error(s) above occurred while examining theory " +
- quote(name.theory) + required_by(initiators))
- }
- (name, header) :: require_thys(files, name :: initiators, required + name, header.imports)
+ else Library.future_value(Exn.Res(header0))
+
+ Dep(name, header0, future_header) ::
+ require_thys(files, name :: initiators, required + name, header0.imports)
}
catch {
case e: Throwable =>
- (name, Document.Node.bad_header(Exn.message(e))) :: (required + name)
+ val bad_header = Document.Node.bad_header(Exn.message(e))
+ Dep(name, bad_header, Library.future_value(Exn.Res(bad_header))) :: (required + name)
}
}
}
--- a/src/Pure/Thy/thy_load.scala Fri Dec 07 16:38:25 2012 +0100
+++ b/src/Pure/Thy/thy_load.scala Fri Dec 07 17:00:40 2012 +0100
@@ -80,53 +80,47 @@
clean_tokens.reverse.find(_.is_name).map(_.content)
}
- def find_files(syntax: Outer_Syntax, text: String): List[String] =
+ def body_files_test(syntax: Outer_Syntax, text: String): Boolean =
+ syntax.thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
+
+ def body_files(syntax: Outer_Syntax, text: String): List[String] =
{
val thy_load_commands = syntax.thy_load_commands
- if (thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })) {
- val spans = Thy_Syntax.parse_spans(syntax.scan(text))
- spans.iterator.map({
- case toks @ (tok :: _) if tok.is_command =>
- thy_load_commands.find({ case (cmd, _) => cmd == tok.content }) match {
- case Some((_, exts)) =>
- find_file(toks) match {
- case Some(file) =>
- if (exts.isEmpty) List(file)
- else exts.map(ext => file + "." + ext)
- case None => Nil
- }
- case None => Nil
- }
- case _ => Nil
- }).flatten.toList
- }
- else Nil
+ val spans = Thy_Syntax.parse_spans(syntax.scan(text))
+ spans.iterator.map({
+ case toks @ (tok :: _) if tok.is_command =>
+ thy_load_commands.find({ case (cmd, _) => cmd == tok.content }) match {
+ case Some((_, exts)) =>
+ find_file(toks) match {
+ case Some(file) =>
+ if (exts.isEmpty) List(file)
+ else exts.map(ext => file + "." + ext)
+ case None => Nil
+ }
+ case None => Nil
+ }
+ case _ => Nil
+ }).flatten.toList
}
def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header =
{
- val header = Thy_Header.read(text)
+ try {
+ val header = Thy_Header.read(text)
- val name1 = header.name
- if (name.theory != name1)
- error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
- " for theory " + quote(name1))
+ val name1 = header.name
+ if (name.theory != name1)
+ error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
+ " for theory " + quote(name1))
- val imports = header.imports.map(import_name(name.dir, _))
- val uses = header.uses
- Document.Node.Header(imports, header.keywords, uses)
+ val imports = header.imports.map(import_name(name.dir, _))
+ val uses = header.uses
+ Document.Node.Header(imports, header.keywords, uses)
+ }
+ catch { case e: Throwable => Document.Node.bad_header(Exn.message(e)) }
}
def check_thy(name: Document.Node.Name): Document.Node.Header =
with_thy_text(name, check_thy_text(name, _))
-
- def check_thy_files(syntax: Outer_Syntax, name: Document.Node.Name): Document.Node.Header =
- with_thy_text(name, text =>
- {
- val string = text.toString
- val header = check_thy_text(name, string)
- val more_uses = find_files(syntax.add_keywords(header.keywords), string)
- header.copy(uses = header.uses ::: more_uses.map((_, false)))
- })
}
--- a/src/Pure/library.scala Fri Dec 07 16:38:25 2012 +0100
+++ b/src/Pure/library.scala Fri Dec 07 17:00:40 2012 +0100
@@ -10,6 +10,7 @@
import java.lang.System
import java.util.Locale
+import java.util.concurrent.{Future => JFuture, TimeUnit}
import java.awt.Component
import javax.swing.JOptionPane
@@ -187,6 +188,18 @@
selection.index = 3
prototypeDisplayValue = Some("00000%")
}
+
+
+ /* Java futures */
+
+ def future_value[A](x: A) = new JFuture[A]
+ {
+ def cancel(may_interrupt: Boolean): Boolean = false
+ def isCancelled(): Boolean = false
+ def isDone(): Boolean = true
+ def get(): A = x
+ def get(timeout: Long, time_unit: TimeUnit): A = x
+ }
}
--- a/src/Tools/jEdit/lib/Tools/jedit Fri Dec 07 16:38:25 2012 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Fri Dec 07 17:00:40 2012 +0100
@@ -316,21 +316,18 @@
fi
-# build logic
-
-if [ "$NO_BUILD" = false ]; then
- "$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}" -L jedit_logic "$JEDIT_LOGIC"
- RC="$?"
- [ "$RC" = 0 ] || exit "$RC"
-fi
-
-
# main
-[ "$BUILD_ONLY" = true ] || {
+if [ "$BUILD_ONLY" = false ]; then
+ if [ "$NO_BUILD" = false ]; then
+ "$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}" -L jedit_logic "$JEDIT_LOGIC"
+ RC="$?"
+ [ "$RC" = 0 ] || exit "$RC"
+ fi
+
export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE
exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
-jar "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" \
"-settings=$(jvmpath "$JEDIT_SETTINGS")" "${ARGS[@]}"
-}
+fi
--- a/src/Tools/jEdit/src/plugin.scala Fri Dec 07 16:38:25 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Fri Dec 07 17:00:40 2012 +0100
@@ -157,7 +157,7 @@
val thy_info = new Thy_Info(PIDE.thy_load)
// FIXME avoid I/O in Swing thread!?!
- val files = thy_info.dependencies(true, thys).deps.map(_._1.node).
+ val files = thy_info.dependencies(true, thys).deps.map(_.name.node).
filter(file => !loaded_buffer(file) && PIDE.thy_load.check_file(view, file))
if (!files.isEmpty) {