# HG changeset patch # User wenzelm # Date 1277391712 -7200 # Node ID eadd8a4dfe78ff63f530551329cb9177492d0125 # Parent 70d03844b2f957f198e6e0b94ca009e8f6dd0bcd# Parent a23e8aa853eb52d3eede25f1da0346e2e1a2e5fd merged diff -r 70d03844b2f9 -r eadd8a4dfe78 Admin/CHECKLIST --- a/Admin/CHECKLIST Thu Jun 24 12:33:51 2010 +0100 +++ b/Admin/CHECKLIST Thu Jun 24 17:01:52 2010 +0200 @@ -29,3 +29,17 @@ build lib/html/library_index_content.template + +Packaging +========= + +- makedist -r DISTNAME + +- makebin (multiplatform); + +- makebin -l on fast machine; + +- makebundle (multiplatform); + +- hdiutil create -srcfolder DIR DMG (Mac OS); + diff -r 70d03844b2f9 -r eadd8a4dfe78 src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Thu Jun 24 12:33:51 2010 +0100 +++ b/src/HOL/Tools/inductive_codegen.ML Thu Jun 24 17:01:52 2010 +0200 @@ -334,10 +334,10 @@ in Pretty.block ([str "(fn ", mk_tuple out_ps, str " =>", Pretty.brk 1] @ - (Pretty.block ((if eqs=[] then [] else str "if " :: + (Pretty.block ((if null eqs then [] else str "if " :: [Pretty.block eqs, Pretty.brk 1, str "then "]) @ (success_p :: - (if eqs=[] then [] else [Pretty.brk 1, str "else DSeq.empty"]))) :: + (if null eqs then [] else [Pretty.brk 1, str "else DSeq.empty"]))) :: (if can_fail then [Pretty.brk 1, str "| _ => DSeq.empty)"] else [str ")"]))) diff -r 70d03844b2f9 -r eadd8a4dfe78 src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Thu Jun 24 12:33:51 2010 +0100 +++ b/src/Pure/General/pretty.ML Thu Jun 24 17:01:52 2010 +0200 @@ -102,10 +102,11 @@ (** printing items: compound phrases, strings, and breaks **) -datatype T = +abstype T = Block of (output * output) * T list * int * int | (*markup output, body, indentation, length*) String of output * int | (*text, length*) - Break of bool * int; (*mandatory flag, width if not taken*) + Break of bool * int (*mandatory flag, width if not taken*) +with fun length (Block (_, _, _, len)) = len | length (String (_, len)) = len @@ -323,6 +324,8 @@ | from_ML (ML_Pretty.String s) = String s | from_ML (ML_Pretty.Break b) = Break b; +end; + (** abstract pretty printing context **) diff -r 70d03844b2f9 -r eadd8a4dfe78 src/Pure/net.ML --- a/src/Pure/net.ML Thu Jun 24 12:33:51 2010 +0100 +++ b/src/Pure/net.ML Thu Jun 24 17:01:52 2010 +0200 @@ -17,6 +17,7 @@ sig type key val key_of_term: term -> key list + val encode_type: typ -> term type 'a net val empty: 'a net exception INSERT @@ -62,6 +63,11 @@ (*convert a term to a list of keys*) fun key_of_term t = add_key_of_terms (t, []); +(*encode_type -- for indexing purposes*) +fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts) + | encode_type (TFree (a, _)) = Free (a, dummyT) + | encode_type (TVar (a, _)) = Var (a, dummyT); + (*Trees indexed by key lists: each arc is labelled by a key. Each node contains a list of items, and arcs to children. diff -r 70d03844b2f9 -r eadd8a4dfe78 src/Pure/pure_setup.ML --- a/src/Pure/pure_setup.ML Thu Jun 24 12:33:51 2010 +0100 +++ b/src/Pure/pure_setup.ML Thu Jun 24 17:01:52 2010 +0200 @@ -18,6 +18,7 @@ (* ML toplevel pretty printing *) +toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"\")"; toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task"; toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group"; toplevel_pp ["Position", "T"] "Pretty.position"; diff -r 70d03844b2f9 -r eadd8a4dfe78 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Thu Jun 24 12:33:51 2010 +0100 +++ b/src/Tools/Code/code_target.ML Thu Jun 24 17:01:52 2010 +0200 @@ -142,9 +142,9 @@ name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) = if serial1 = serial2 orelse not strict then make_target ((serial1, serializer), - ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)), + ((merge (op =) (reserved1, reserved2), Symtab.merge (K true) (includes1, includes2)), (merge_name_syntax_table (name_syntax_table1, name_syntax_table2), - Symtab.join (K snd) (module_alias1, module_alias2)) + Symtab.join (K fst) (module_alias1, module_alias2)) )) else error ("Incompatible serializers: " ^ quote target); diff -r 70d03844b2f9 -r eadd8a4dfe78 src/Tools/induct.ML --- a/src/Tools/induct.ML Thu Jun 24 12:33:51 2010 +0100 +++ b/src/Tools/induct.ML Thu Jun 24 17:01:52 2010 +0200 @@ -4,7 +4,7 @@ Proof by cases, induction, and coinduction. *) -signature INDUCT_DATA = +signature INDUCT_ARGS = sig val cases_default: thm val atomize: thm list @@ -82,27 +82,17 @@ val setup: theory -> theory end; -functor Induct(Data: INDUCT_DATA): INDUCT = +functor Induct(Induct_Args: INDUCT_ARGS): INDUCT = struct - -(** misc utils **) - -(* encode_type -- for indexing purposes *) - -fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts) - | encode_type (TFree (a, _)) = Free (a, dummyT) - | encode_type (TVar (a, _)) = Var (a, dummyT); - - -(* variables -- ordered left-to-right, preferring right *) +(** variables -- ordered left-to-right, preferring right **) fun vars_of tm = rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm [])); local -val mk_var = encode_type o #2 o Term.dest_Var; +val mk_var = Net.encode_type o #2 o Term.dest_Var; fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty => raise THM ("No variables in conclusion of rule", 0, [thm]); @@ -128,14 +118,14 @@ fun conv1 0 ctxt = Conv.forall_conv (cv o snd) ctxt | conv1 k ctxt = Conv.rewr_conv @{thm swap_params} then_conv - Conv.forall_conv (conv1 (k-1) o snd) ctxt + Conv.forall_conv (conv1 (k - 1) o snd) ctxt fun conv2 0 ctxt = conv1 j ctxt - | conv2 k ctxt = Conv.forall_conv (conv2 (k-1) o snd) ctxt + | conv2 k ctxt = Conv.forall_conv (conv2 (k - 1) o snd) ctxt in conv2 i ctxt end; fun swap_prems_conv 0 = Conv.all_conv | swap_prems_conv i = - Conv.implies_concl_conv (swap_prems_conv (i-1)) then_conv + Conv.implies_concl_conv (swap_prems_conv (i - 1)) then_conv Conv.rewr_conv Drule.swap_prems_eq fun drop_judgment ctxt = Object_Logic.drop_judgment (ProofContext.theory_of ctxt); @@ -145,46 +135,51 @@ val l = length (Logic.strip_params t); val Hs = Logic.strip_assums_hyp t; fun find (i, t) = - case Data.dest_def (drop_judgment ctxt t) of + (case Induct_Args.dest_def (drop_judgment ctxt t) of SOME (Bound j, _) => SOME (i, j) | SOME (_, Bound j) => SOME (i, j) - | _ => NONE + | _ => NONE); in - case get_first find (map_index I Hs) of + (case get_first find (map_index I Hs) of NONE => NONE | SOME (0, 0) => NONE - | SOME (i, j) => SOME (i, l-j-1, j) + | SOME (i, j) => SOME (i, l - j - 1, j)) end; -fun mk_swap_rrule ctxt ct = case find_eq ctxt (term_of ct) of +fun mk_swap_rrule ctxt ct = + (case find_eq ctxt (term_of ct) of NONE => NONE - | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct); + | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct)); -val rearrange_eqs_simproc = Simplifier.simproc - (Thm.theory_of_thm Drule.swap_prems_eq) "rearrange_eqs" ["all t"] - (fn thy => fn ss => fn t => - mk_swap_rrule (Simplifier.the_context ss) (cterm_of thy t)) +val rearrange_eqs_simproc = + Simplifier.simproc + (Thm.theory_of_thm Drule.swap_prems_eq) "rearrange_eqs" ["all t"] + (fn thy => fn ss => fn t => + mk_swap_rrule (Simplifier.the_context ss) (cterm_of thy t)); + (* rotate k premises to the left by j, skipping over first j premises *) fun rotate_conv 0 j 0 = Conv.all_conv - | rotate_conv 0 j k = swap_prems_conv j then_conv rotate_conv 1 j (k-1) - | rotate_conv i j k = Conv.implies_concl_conv (rotate_conv (i-1) j k); + | rotate_conv 0 j k = swap_prems_conv j then_conv rotate_conv 1 j (k - 1) + | rotate_conv i j k = Conv.implies_concl_conv (rotate_conv (i - 1) j k); fun rotate_tac j 0 = K all_tac - | rotate_tac j k = SUBGOAL (fn (goal, i) => CONVERSION (rotate_conv - j (length (Logic.strip_assums_hyp goal) - j - k) k) i); + | rotate_tac j k = SUBGOAL (fn (goal, i) => + CONVERSION (rotate_conv + j (length (Logic.strip_assums_hyp goal) - j - k) k) i); + (* rulify operators around definition *) fun rulify_defs_conv ctxt ct = - if exists_subterm (is_some o Data.dest_def) (term_of ct) andalso - not (is_some (Data.dest_def (drop_judgment ctxt (term_of ct)))) + if exists_subterm (is_some o Induct_Args.dest_def) (term_of ct) andalso + not (is_some (Induct_Args.dest_def (drop_judgment ctxt (term_of ct)))) then (Conv.forall_conv (rulify_defs_conv o snd) ctxt else_conv Conv.implies_conv (Conv.try_conv (rulify_defs_conv ctxt)) (Conv.try_conv (rulify_defs_conv ctxt)) else_conv - Conv.first_conv (map Conv.rewr_conv Data.rulify) then_conv + Conv.first_conv (map Conv.rewr_conv Induct_Args.rulify) then_conv Conv.try_conv (rulify_defs_conv ctxt)) ct else Conv.no_conv ct; @@ -213,7 +208,7 @@ (* context data *) -structure InductData = Generic_Data +structure Data = Generic_Data ( type T = (rules * rules) * (rules * rules) * (rules * rules) * simpset; val empty = @@ -230,7 +225,7 @@ merge_ss (simpset1, simpset2)); ); -val get_local = InductData.get o Context.Proof; +val get_local = Data.get o Context.Proof; fun dest_rules ctxt = let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP), _) = get_local ctxt in @@ -272,11 +267,11 @@ fun find_rules which how ctxt x = map snd (Item_Net.retrieve (which (get_local ctxt)) (how x)); -val find_casesT = find_rules (#1 o #1) encode_type; +val find_casesT = find_rules (#1 o #1) Net.encode_type; val find_casesP = find_rules (#2 o #1) I; -val find_inductT = find_rules (#1 o #2) encode_type; +val find_inductT = find_rules (#1 o #2) Net.encode_type; val find_inductP = find_rules (#2 o #2) I; -val find_coinductT = find_rules (#1 o #3) encode_type; +val find_coinductT = find_rules (#1 o #3) Net.encode_type; val find_coinductP = find_rules (#2 o #3) I; @@ -286,10 +281,11 @@ local fun mk_att f g name arg = - let val (x, thm) = g arg in (InductData.map (f (name, thm)) x, thm) end; + let val (x, thm) = g arg in (Data.map (f (name, thm)) x, thm) end; -fun del_att which = Thm.declaration_attribute (fn th => InductData.map (which (pairself (fn rs => - fold Item_Net.remove (filter_rules rs th) rs)))); +fun del_att which = + Thm.declaration_attribute (fn th => Data.map (which (pairself (fn rs => + fold Item_Net.remove (filter_rules rs th) rs)))); fun map1 f (x, y, z, s) = (f x, y, z, s); fun map2 f (x, y, z, s) = (x, f y, z, s); @@ -320,12 +316,12 @@ val coinduct_pred = mk_att add_coinductP consumes1; val coinduct_del = del_att map3; -fun map_simpset f = InductData.map (map4 f); +fun map_simpset f = Data.map (map4 f); fun induct_simp f = Thm.declaration_attribute (fn thm => fn context => - (map_simpset - (Simplifier.with_context (Context.proof_of context) (fn ss => f (ss, [thm]))) context)); + map_simpset + (Simplifier.with_context (Context.proof_of context) (fn ss => f (ss, [thm]))) context); val induct_simp_add = induct_simp (op addsimps); val induct_simp_del = induct_simp (op delsimps); @@ -420,14 +416,15 @@ (* mark equality constraints in cases rule *) -val equal_def' = Thm.symmetric Data.equal_def; +val equal_def' = Thm.symmetric Induct_Args.equal_def; fun mark_constraints n ctxt = Conv.fconv_rule (Conv.prems_conv (~1) (Conv.params_conv ~1 (K (Conv.prems_conv n (MetaSimplifier.rewrite false [equal_def']))) ctxt)); val unmark_constraints = Conv.fconv_rule - (MetaSimplifier.rewrite true [Data.equal_def]); + (MetaSimplifier.rewrite true [Induct_Args.equal_def]); + (* simplify *) @@ -435,7 +432,7 @@ Simplifier.full_rewrite (Simplifier.context ctxt (#4 (get_local ctxt))); fun simplify_conv ctxt ct = - if exists_subterm (is_some o Data.dest_def) (term_of ct) then + if exists_subterm (is_some o Induct_Args.dest_def) (term_of ct) then (Conv.try_conv (rulify_defs_conv ctxt) then_conv simplify_conv' ctxt) ct else Conv.all_conv ct; @@ -447,7 +444,7 @@ fun simplify_tac ctxt = CONVERSION (simplify_conv ctxt); -val trivial_tac = Data.trivial_tac; +val trivial_tac = Induct_Args.trivial_tac; @@ -487,7 +484,7 @@ (case opt_rule of SOME r => Seq.single (inst_rule r) | NONE => - (get_casesP ctxt facts @ get_casesT ctxt insts @ [Data.cases_default]) + (get_casesP ctxt facts @ get_casesT ctxt insts @ [Induct_Args.cases_default]) |> tap (trace_rules ctxt casesN) |> Seq.of_list |> Seq.maps (Seq.try inst_rule)); in @@ -517,12 +514,12 @@ (* atomize *) fun atomize_term thy = - MetaSimplifier.rewrite_term thy Data.atomize [] + MetaSimplifier.rewrite_term thy Induct_Args.atomize [] #> Object_Logic.drop_judgment thy; -val atomize_cterm = MetaSimplifier.rewrite true Data.atomize; +val atomize_cterm = MetaSimplifier.rewrite true Induct_Args.atomize; -val atomize_tac = Simplifier.rewrite_goal_tac Data.atomize; +val atomize_tac = Simplifier.rewrite_goal_tac Induct_Args.atomize; val inner_atomize_tac = Simplifier.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac; @@ -531,8 +528,8 @@ (* rulify *) fun rulify_term thy = - MetaSimplifier.rewrite_term thy (Data.rulify @ conjunction_congs) [] #> - MetaSimplifier.rewrite_term thy Data.rulify_fallback []; + MetaSimplifier.rewrite_term thy (Induct_Args.rulify @ conjunction_congs) [] #> + MetaSimplifier.rewrite_term thy Induct_Args.rulify_fallback []; fun rulified_term thm = let @@ -542,8 +539,8 @@ in (thy, Logic.list_implies (map rulify As, rulify B)) end; val rulify_tac = - Simplifier.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN' - Simplifier.rewrite_goal_tac Data.rulify_fallback THEN' + Simplifier.rewrite_goal_tac (Induct_Args.rulify @ conjunction_congs) THEN' + Simplifier.rewrite_goal_tac Induct_Args.rulify_fallback THEN' Goal.conjunction_tac THEN_ALL_NEW (Simplifier.rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);