# HG changeset patch # User blanchet # Date 1391641392 -3600 # Node ID 1bd9e637ac9f49b059cb1ccd27e36d71cecf8111 # Parent 3d2c97392e256eb2944ef10825b6a69cdb05eddf tuning diff -r 3d2c97392e25 -r 1bd9e637ac9f src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Feb 05 23:30:02 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Feb 06 00:03:12 2014 +0100 @@ -186,15 +186,16 @@ ctr_sugars co_iterss mapss co_inducts co_iter_thmsss disc_co_itersss sel_co_iterssss lthy = (0, lthy) |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1, - register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, - nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, fp_res = fp_res, - ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, - co_inducts = co_inducts, co_iter_thmsss = co_iter_thmsss, disc_co_itersss = disc_co_itersss, + register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs, + nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss, + ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts, + co_iter_thmsss = co_iter_thmsss, disc_co_itersss = disc_co_itersss, sel_co_iterssss = sel_co_iterssss} lthy)) Ts |> snd; -(* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *) +(* This function could produce (fairly harmless) clashes in contrived examples (e.g., "x.A", + "x.x_A", "y.A"). *) fun quasi_unambiguous_case_names names = let val ps = map (`Long_Name.base_name) names; @@ -501,7 +502,7 @@ if fp = Least_FP then mk_iters_args_types ctr_Tsss Cs ns mss xtor_co_iter_fun_Tss lthy |>> (rpair NONE o SOME) else - mk_coiters_args_types ctr_Tsss Cs ns xtor_co_iter_fun_Tss lthy |>> (pair NONE o SOME) + mk_coiters_args_types ctr_Tsss Cs ns xtor_co_iter_fun_Tss lthy |>> (pair NONE o SOME); in ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy') end; diff -r 3d2c97392e25 -r 1bd9e637ac9f src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Feb 05 23:30:02 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Feb 06 00:03:12 2014 +0100 @@ -165,7 +165,7 @@ else f conds t end - | _ => f conds t) + | _ => f conds t); in fld [] end; @@ -224,7 +224,7 @@ end | NONE => massage_leaf bound_Ts t) | _ => massage_leaf bound_Ts t) - end + end; in massage_rec end; @@ -490,11 +490,14 @@ val abs_tuple = HOLogic.tupled_lambda o HOLogic.mk_tuple; fun abstract vs = - let fun a n (t $ u) = a n t $ a n u - | a n (Abs (v, T, b)) = Abs (v, T, a (n + 1) b) - | a n t = let val idx = find_index (curry (op =) t) vs in - if idx < 0 then t else Bound (n + idx) end - in a 0 end; + let + fun abs n (t $ u) = abs n t $ abs n u + | abs n (Abs (v, T, b)) = Abs (v, T, abs (n + 1) b) + | abs n t = + let val j = find_index (curry (op =) t) vs in + if j < 0 then t else Bound (n + j) + end; + in abs 0 end; fun mk_prod1 bound_Ts (t, u) = HOLogic.pair_const (fastype_of1 (bound_Ts, t)) (fastype_of1 (bound_Ts, u)) $ t $ u; @@ -849,7 +852,7 @@ ((c, c', a orelse a'), (x, s_not (s_conjs y))) ||> apfst (map HOLogic.mk_Trueprop) o apsnd HOLogic.mk_Trueprop ||> Logic.list_implies - ||> curry Logic.list_all (map dest_Free fun_args)))) + ||> curry Logic.list_all (map dest_Free fun_args)))); in map (list_comb o rpair corec_args) corecs |> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss @@ -868,7 +871,7 @@ else let val n = 0 upto length ctr_specs - |> the o find_first (fn idx => not (exists (curry (op =) idx o #ctr_no) disc_eqns)); + |> the o find_first (fn j => not (exists (curry (op =) j o #ctr_no) disc_eqns)); val {ctr, disc, ...} = nth ctr_specs n; val fun_args = (try (#fun_args o hd) disc_eqns, try (#fun_args o hd) sel_eqns) |> the_default (map (curry Free Name.uu) arg_Ts) o merge_options; @@ -985,9 +988,9 @@ space_implode "\n \ " (maps (map (Syntax.string_of_term lthy o snd)) excludess')); *) - val excludess'' = map3 (fn tac_opt => fn sequential => map (fn (idx, goal) => - (idx, (Option.map (Goal.prove_sorry lthy [] [] goal #> Thm.close_derivation) - (exclude_tac tac_opt sequential idx), goal)))) + val excludess'' = map3 (fn tac_opt => fn sequential => map (fn (j, goal) => + (j, (Option.map (Goal.prove_sorry lthy [] [] goal #> Thm.close_derivation) + (exclude_tac tac_opt sequential j), goal)))) tac_opts sequentials excludess'; val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) excludess''; val (goal_idxss, exclude_goalss) = excludess'' diff -r 3d2c97392e25 -r 1bd9e637ac9f src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Wed Feb 05 23:30:02 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Thu Feb 06 00:03:12 2014 +0100 @@ -162,7 +162,7 @@ fun raw_code_single_tac ctxt distincts discIs splits split_asms m fun_ctr = let val splits' = - map (fn th => th RS iffD2) (@{thm split_if_eq2} :: map (inst_split_eq ctxt) splits) + map (fn th => th RS iffD2) (@{thm split_if_eq2} :: map (inst_split_eq ctxt) splits); in HEADGOAL (REPEAT o (resolve_tac (splits' @ split_connectI))) THEN prelude_tac ctxt [] (fun_ctr RS trans) THEN diff -r 3d2c97392e25 -r 1bd9e637ac9f src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Feb 05 23:30:02 2014 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Thu Feb 06 00:03:12 2014 +0100 @@ -205,12 +205,9 @@ fun mk_half_pairss p = mk_half_pairss' [[]] p; fun join_halves n half_xss other_half_xss = - let - val xsss = - map2 (map2 append) (Library.chop_groups n half_xss) - (transpose (Library.chop_groups n other_half_xss)) - val xs = splice (flat half_xss) (flat other_half_xss); - in (xs, xsss) end; + (splice (flat half_xss) (flat other_half_xss), + map2 (map2 append) (Library.chop_groups n half_xss) + (transpose (Library.chop_groups n other_half_xss))); fun mk_undefined T = Const (@{const_name undefined}, T); @@ -252,9 +249,7 @@ val base_name_of_ctr = Long_Name.base_name o name_of_ctr; fun dest_ctr ctxt s t = - let - val (f, args) = Term.strip_comb t; - in + let val (f, args) = Term.strip_comb t in (case ctr_sugar_of ctxt s of SOME {ctrs, ...} => (case find_first (can (fo_match ctxt f)) ctrs of