# HG changeset patch # User blanchet # Date 1400724726 -7200 # Node ID df3a26987a8dbf6b8dbb8a31a029696f928cc1a8 # Parent fed0329ea8e2b1b446245afe13ea59f1127a2ed4 reverted '|' features in MaSh -- these sounded like a good idea but never really worked diff -r fed0329ea8e2 -r df3a26987a8d src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Thu May 22 03:29:36 2014 +0200 +++ b/src/HOL/TPTP/mash_export.ML Thu May 22 04:12:06 2014 +0200 @@ -52,18 +52,22 @@ let val path = file_name |> Path.explode val _ = File.write path "" + fun do_fact (parents, fact) prevs = let val parents = if linearize then prevs else parents val s = encode_str fact ^ ": " ^ encode_strs parents ^ "\n" val _ = File.append path s in [fact] end + val facts = all_facts ctxt |> filter_out (has_thys thys o snd) |> attach_parents_to_facts [] |> map (apsnd (nickname_of_thm o snd)) - in fold do_fact facts []; () end + in + fold do_fact facts []; () + end fun generate_features ctxt thys file_name = let @@ -74,10 +78,12 @@ let val name = nickname_of_thm th val feats = - features_of ctxt (theory_of_thm th) 0 Symtab.empty stature false [prop_of th] |> map fst - val s = encode_str name ^ ": " ^ encode_unweighted_features (sort_wrt hd feats) ^ "\n" + features_of ctxt (theory_of_thm th) 0 Symtab.empty stature [prop_of th] |> map fst + val s = encode_str name ^ ": " ^ encode_strs (sort string_ord feats) ^ "\n" in File.append path s end - in List.app do_fact facts end + in + List.app do_fact facts + end val prover_marker = "$a" val isar_marker = "$i" @@ -88,21 +94,21 @@ fun smart_dependencies_of ctxt params_opt facts name_tabs th isar_deps_opt = let val (marker, deps) = - case params_opt of + (case params_opt of SOME (params as {provers = prover :: _, ...}) => prover_dependencies_of ctxt params prover 0 facts name_tabs th |>> (fn true => prover_marker | false => prover_failed_marker) | NONE => let val deps = - case isar_deps_opt of + (case isar_deps_opt of SOME deps => deps - | NONE => isar_dependencies_of name_tabs th - in (if null deps then unprovable_marker else isar_marker, deps) end + | NONE => isar_dependencies_of name_tabs th) + in (if null deps then unprovable_marker else isar_marker, deps) end) in - case trim_dependencies deps of + (case trim_dependencies deps of SOME deps => (marker, deps) - | NONE => (omitted_marker, []) + | NONE => (omitted_marker, [])) end fun generate_isar_or_prover_dependencies ctxt params_opt range thys linearize @@ -111,6 +117,7 @@ val path = file_name |> Path.explode val facts = all_facts ctxt |> filter_out (has_thys thys o snd) val name_tabs = build_name_tables nickname_of_thm facts + fun do_fact (j, (_, th)) = if in_range range j then let @@ -124,8 +131,11 @@ in encode_str name ^ ": " ^ marker ^ " " ^ encode_strs deps ^ "\n" end else "" + val lines = Par_List.map do_fact (tag_list 1 facts) - in File.write_list path lines end + in + File.write_list path lines + end fun generate_isar_dependencies ctxt = generate_isar_or_prover_dependencies ctxt NONE @@ -139,8 +149,8 @@ null isar_deps orelse is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th) -fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys - linearize max_suggs file_name = +fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys linearize max_suggs + file_name = let val ho_atp = is_ho_atp ctxt prover val path = file_name |> Path.explode @@ -148,13 +158,16 @@ val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd) val num_old_facts = length old_facts val name_tabs = build_name_tables nickname_of_thm facts - fun do_fact (j, - (((name, (parents, ((_, stature), th))), prevs), const_tab)) = + + fun do_fact (j, (((name, (parents, ((_, stature), th))), prevs), const_tab)) = if in_range range j then let val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name) val isar_deps = isar_dependencies_of name_tabs th val do_query = not (is_bad_query ctxt ho_atp step j th isar_deps) + val goal_feats = + features_of ctxt (theory_of_thm th) (num_old_facts + j) const_tab stature [prop_of th] + |> sort_wrt fst val access_facts = (if linearize then take (j - 1) new_facts else new_facts |> filter_accessible_from th) @ old_facts @@ -164,15 +177,11 @@ val parents = if linearize then prevs else parents fun extra_features_of (((_, stature), th), weight) = [prop_of th] - |> features_of ctxt (theory_of_thm th) (num_old_facts + j) const_tab stature false + |> features_of ctxt (theory_of_thm th) (num_old_facts + j) const_tab stature |> map (apsnd (fn r => weight * extra_feature_factor * r)) val query = if do_query then let - val goal_feats = - features_of ctxt (theory_of_thm th) (num_old_facts + j) const_tab stature true - [prop_of th] - |> sort_wrt (hd o fst) val query_feats = new_facts |> drop (j - num_extra_feature_facts) @@ -188,30 +197,24 @@ end else "" - val nongoal_feats = - features_of ctxt (theory_of_thm th) (num_old_facts + j) const_tab stature false - [prop_of th] - |> map fst |> sort_wrt hd val update = "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^ - encode_unweighted_features nongoal_feats ^ "; " ^ marker ^ " " ^ encode_strs deps ^ "\n" + encode_strs (map fst goal_feats) ^ "; " ^ marker ^ " " ^ encode_strs deps ^ "\n" in query ^ update end else "" val new_facts = new_facts |> attach_parents_to_facts old_facts |> map (`(nickname_of_thm o snd o snd)) - val hd_prevs = - map (nickname_of_thm o snd) (the_list (try List.last old_facts)) + val hd_prevs = map (nickname_of_thm o snd) (the_list (try List.last old_facts)) val prevss = hd_prevs :: map (single o fst) new_facts |> split_last |> fst - val hd_const_tabs = - fold (add_const_counts o prop_of o snd) old_facts Symtab.empty + val hd_const_tabs = fold (add_const_counts o prop_of o snd) old_facts Symtab.empty val (const_tabs, _) = - fold_map (`I oo add_const_counts o prop_of o snd o snd o snd) new_facts - hd_const_tabs - val lines = - Par_List.map do_fact (tag_list 1 (new_facts ~~ prevss ~~ const_tabs)) - in File.write_list path lines end + fold_map (`I oo add_const_counts o prop_of o snd o snd o snd) new_facts hd_const_tabs + val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ prevss ~~ const_tabs)) + in + File.write_list path lines + end fun generate_isar_commands ctxt prover = generate_isar_or_prover_commands ctxt prover NONE @@ -219,14 +222,15 @@ fun generate_prover_commands ctxt (params as {provers = prover :: _, ...}) = generate_isar_or_prover_commands ctxt prover (SOME params) -fun generate_mepo_suggestions ctxt (params as {provers = prover :: _, ...}) - (range, step) thys linearize max_suggs file_name = +fun generate_mepo_suggestions ctxt (params as {provers = prover :: _, ...}) (range, step) thys + linearize max_suggs file_name = let val ho_atp = is_ho_atp ctxt prover val path = file_name |> Path.explode val facts = all_facts ctxt val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd) val name_tabs = build_name_tables nickname_of_thm facts + fun do_fact (j, ((_, th), old_facts)) = if in_range range j then let @@ -250,16 +254,19 @@ end else "" + fun accum x (yss as ys :: _) = (x :: ys) :: yss val old_factss = tl (fold accum new_facts [old_facts]) val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ rev old_factss)) - in File.write_list path lines end + in + File.write_list path lines + end -fun generate_mesh_suggestions max_suggs mash_file_name mepo_file_name - mesh_file_name = +fun generate_mesh_suggestions max_suggs mash_file_name mepo_file_name mesh_file_name = let val mesh_path = Path.explode mesh_file_name val _ = File.write mesh_path "" + fun do_fact (mash_line, mepo_line) = let val (name, mash_suggs) = @@ -275,6 +282,7 @@ val mesh_suggs = mesh_facts (op =) max_suggs mess val mesh_line = encode_str name ^ ": " ^ encode_strs mesh_suggs ^ "\n" in File.append mesh_path mesh_line end + val mash_lines = Path.explode mash_file_name |> File.read_lines val mepo_lines = Path.explode mepo_file_name |> File.read_lines in diff -r fed0329ea8e2 -r df3a26987a8d src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Thu May 22 03:29:36 2014 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Thu May 22 04:12:06 2014 +0200 @@ -170,8 +170,10 @@ "indices unordered or out of range") in aux 0 js xs end -fun n_fold_cartesian_product xss = - Sledgehammer_Util.n_fold_cartesian_product xss +fun cartesian_product [] _ = [] + | cartesian_product (x :: xs) yss = map (cons x) yss @ cartesian_product xs yss + +fun n_fold_cartesian_product xss = fold_rev cartesian_product xss [[]] fun all_distinct_unordered_pairs_of [] = [] | all_distinct_unordered_pairs_of (x :: xs) = diff -r fed0329ea8e2 -r df3a26987a8d src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu May 22 03:29:36 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu May 22 04:12:06 2014 +0200 @@ -31,8 +31,7 @@ val encode_strs : string list -> string val decode_str : string -> string val decode_strs : string -> string list - val encode_unweighted_features : string list list -> string - val encode_features : (string list * real) list -> string + val encode_features : (string * real) list -> string val extract_suggestions : string -> string * string list val mash_unlearn : Proof.context -> params -> unit @@ -44,8 +43,8 @@ val goal_of_thm : theory -> thm -> thm val run_prover_for_mash : Proof.context -> params -> string -> string -> fact list -> thm -> prover_result - val features_of : Proof.context -> theory -> int -> int Symtab.table -> stature -> bool -> - term list -> (string list * real) list + val features_of : Proof.context -> theory -> int -> int Symtab.table -> stature -> term list -> + (string * real) list val trim_dependencies : string list -> string list option val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list val prover_dependencies_of : Proof.context -> params -> string -> int -> raw_fact list -> @@ -213,26 +212,20 @@ else if r >= 1000000.0 then "1000000" else Markup.print_real r -val encode_unweighted_feature = map encode_str #> space_implode "|" -val decode_unweighted_feature = space_explode "|" #> map decode_str - fun encode_feature (names, weight) = - encode_unweighted_feature names ^ - (if Real.== (weight, 1.0) then "" else "=" ^ safe_str_of_real weight) + encode_str names ^ (if Real.== (weight, 1.0) then "" else "=" ^ safe_str_of_real weight) fun decode_feature s = (case space_explode "=" s of - [feat, weight] => (decode_unweighted_feature feat, Real.fromString weight |> the_default 1.0) - | _ => (decode_unweighted_feature s, 1.0)) - -val encode_unweighted_features = map encode_unweighted_feature #> space_implode " " + [feat, weight] => (decode_str feat, Real.fromString weight |> the_default 1.0) + | _ => (decode_str s, 1.0)) val encode_features = map encode_feature #> space_implode " " val decode_features = space_explode " " #> map decode_feature fun str_of_learn (name, parents, feats, deps) = - "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^ - encode_unweighted_features feats ^ "; " ^ encode_strs deps ^ "\n" + "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^ encode_strs feats ^ "; " ^ + encode_strs deps ^ "\n" fun str_of_relearn (name, deps) = "p " ^ encode_str name ^ ": " ^ encode_strs deps ^ "\n" @@ -509,8 +502,6 @@ fun query ctxt engine parents access_G max_suggs hints feats = let - val str_of_feat = space_implode "|" - val visible_facts = Graph.all_preds access_G parents val visible_fact_set = Symtab.make_set visible_facts @@ -528,7 +519,7 @@ SOME i => ((i, weight), xtab) | NONE => ((n, weight), add_to_xtab feat xtab)) - val (feats', feat_xtab') = fold_map (add_feat o apfst str_of_feat) feats feat_xtab + val (feats', feat_xtab') = fold_map add_feat feats feat_xtab in (map_filter (Symtab.lookup fact_tab) deps :: rev_depss, feats' :: rev_featss, add_to_xtab fact fact_xtab, feat_xtab') @@ -547,18 +538,18 @@ elide_string 1000 (space_implode " " (take num_visible_facts facts)) ^ "}"); (if engine = MaSh_SML_kNN then let - val facts_ary = Array.array (num_feats, []) - val _ = - fold (fn feats => fn fact => - let val fact' = fact - 1 in - List.app (fn (feat, weight) => map_array_at facts_ary (cons (fact', weight)) feat) - feats; - fact' - end) - rev_featss num_facts + val facts_ary = Array.array (num_feats, []) + val _ = + fold (fn feats => fn fact => + let val fact' = fact - 1 in + List.app (fn (feat, weight) => map_array_at facts_ary (cons (fact', weight)) feat) + feats; + fact' + end) + rev_featss num_facts val get_facts = curry Array.sub facts_ary val syms = map_filter (fn (feat, weight) => - Option.map (rpair weight) (Symtab.lookup feat_tab (str_of_feat feat))) feats + Option.map (rpair weight) (Symtab.lookup feat_tab feat)) feats in k_nearest_neighbors num_facts num_visible_facts get_deps get_facts knns max_suggs syms end @@ -566,7 +557,7 @@ let val unweighted_feats_ary = Vector.fromList (map (map fst) (rev rev_featss)) val get_unweighted_feats = curry Vector.sub unweighted_feats_ary - val unweighted_syms = map_filter (Symtab.lookup feat_tab o str_of_feat o fst) feats + val unweighted_syms = map_filter (Symtab.lookup feat_tab o fst) feats in naive_bayes num_facts num_visible_facts get_deps get_unweighted_feats num_feats ess prior max_suggs unweighted_syms @@ -620,7 +611,7 @@ string_of_int (length (Graph.maximals G)) ^ " maximal" type mash_state = - {access_G : (proof_kind * (string list * real) list * string list) Graph.T, + {access_G : (proof_kind * (string * real) list * string list) Graph.T, num_known_facts : int, dirty : string list option} @@ -784,12 +775,11 @@ end val default_weight = 1.0 -fun free_feature_of s = (["f" ^ s], 40.0 (* FUDGE *)) -fun thy_feature_of s = (["y" ^ s], 8.0 (* FUDGE *)) -fun type_feature_of s = (["t" ^ s], 4.0 (* FUDGE *)) -fun var_feature_of s = ([s], 1.0 (* FUDGE *)) -fun class_feature_of s = (["s" ^ s], 1.0 (* FUDGE *)) -val local_feature = (["local"], 16.0 (* FUDGE *)) +fun free_feature_of s = ("f" ^ s, 40.0 (* FUDGE *)) +fun thy_feature_of s = ("y" ^ s, 8.0 (* FUDGE *)) +fun type_feature_of s = ("t" ^ s, 4.0 (* FUDGE *)) +fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *)) +val local_feature = ("local", 16.0 (* FUDGE *)) fun crude_theory_ord p = if Theory.subthy p then @@ -843,7 +833,7 @@ val pat_var_prefix = "_" (* try "Long_Name.base_name" for shorter names *) -fun massage_long_name s = if s = @{class type} then "T" else s +fun massage_long_name s = s val crude_str_of_sort = space_implode ":" o map massage_long_name o subtract (op =) @{sort type} @@ -857,33 +847,9 @@ val max_pat_breadth = 10 (* FUDGE *) -fun keep m xs = - let val n = length xs in - if n <= m then xs else take (m div 2) xs @ drop (n - (m + 1) div 2) xs - end - -fun sort_of_type alg T = - let - val G = Sorts.classes_of alg - - fun cls_of S [] = S - | cls_of S (cl :: cls) = - if Sorts.of_sort alg (T, [cl]) then - cls_of (insert (op =) cl S) cls - else - let val cls' = Sorts.minimize_sort alg (Sorts.super_classes alg cl) in - cls_of S (union (op =) cls' cls) - end - in - cls_of [] (Graph.maximals G) - end - -val generalize_goal = false - -fun term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth in_goal ts = +fun term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth ts = let val thy = Proof_Context.theory_of ctxt - val alg = Sign.classes_of thy val fixes = map snd (Variable.dest_fixes ctxt) val classes = Sign.classes_of thy @@ -902,8 +868,8 @@ | pattify_type depth (Type (s, U :: Ts)) = let val T = Type (s, Ts) - val ps = keep max_pat_breadth (pattify_type depth T) - val qs = keep max_pat_breadth ("" :: pattify_type (depth - 1) U) + val ps = take max_pat_breadth (pattify_type depth T) + val qs = take max_pat_breadth ("" :: pattify_type (depth - 1) U) in map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs end @@ -935,64 +901,37 @@ Real.fromInt num_facts / Real.fromInt count (* FUDGE *) end) - fun pattify_term _ 0 _ = ([] : (string list * real) list) - | pattify_term _ _ (Const (x as (s, _))) = - if is_widely_irrelevant_const s then - [] - else - let - val strs_of_sort = - (if generalize_goal andalso in_goal then Sorts.complete_sort alg - else single o hd) - #> map massage_long_name - fun strs_of_type_arg (T as Type (s, _)) = - massage_long_name s :: - (if generalize_goal andalso in_goal then strs_of_sort (sort_of_type alg T) else []) - | strs_of_type_arg (TFree (_, S)) = strs_of_sort S - | strs_of_type_arg (TVar (_, S)) = strs_of_sort S - - val typargss = - these (try (Sign.const_typargs thy) x) - |> map strs_of_type_arg - |> n_fold_cartesian_product - |> keep max_pat_breadth - val s' = massage_long_name s - val w = weight_of_const s - - fun str_of_type_args [] = "" - | str_of_type_args ss = "(" ^ space_implode "," ss ^ ")" - in - [(map (curry (op ^) s' o str_of_type_args) typargss, w)] - end + fun pattify_term _ 0 _ = [] + | pattify_term _ _ (Const (s, _)) = + if is_widely_irrelevant_const s then [] else [(massage_long_name s, weight_of_const s)] | pattify_term _ _ (Free (s, T)) = maybe_singleton_str pat_var_prefix (crude_str_of_typ T) - |> map var_feature_of + |> map (rpair 1.0) |> (if member (op =) fixes s then - cons (free_feature_of (massage_long_name (thy_name ^ Long_Name.separator ^ s))) + cons (free_feature_of (massage_long_name + (thy_name ^ Long_Name.separator ^ s))) else I) | pattify_term _ _ (Var (_, T)) = - maybe_singleton_str pat_var_prefix (crude_str_of_typ T) - |> map var_feature_of + maybe_singleton_str pat_var_prefix (crude_str_of_typ T) |> map (rpair default_weight) | pattify_term Ts _ (Bound j) = maybe_singleton_str pat_var_prefix (crude_str_of_typ (nth Ts j)) - |> map var_feature_of + |> map (rpair default_weight) | pattify_term Ts depth (t $ u) = let - val ps = keep max_pat_breadth (pattify_term Ts depth t) - val qs = keep max_pat_breadth (([], default_weight) :: pattify_term Ts (depth - 1) u) + val ps = take max_pat_breadth (pattify_term Ts depth t) + val qs = take max_pat_breadth (("", default_weight) :: pattify_term Ts (depth - 1) u) in - map_product (fn ppw as (p :: _, pw) => - fn ([], _) => ppw - | (q :: _, qw) => ([p ^ "(" ^ q ^ ")"], pw + qw)) ps qs + map_product (fn ppw as (p, pw) => + fn ("", _) => ppw + | (q, qw) => (p ^ "(" ^ q ^ ")", pw + qw)) ps qs end | pattify_term _ _ _ = [] fun add_term_pat Ts = union (eq_fst (op =)) oo pattify_term Ts fun add_term_pats _ 0 _ = I - | add_term_pats Ts depth t = - add_term_pat Ts depth t #> add_term_pats Ts (depth - 1) t + | add_term_pats Ts depth t = add_term_pat Ts depth t #> add_term_pats Ts (depth - 1) t fun add_term Ts = add_term_pats Ts term_max_depth @@ -1017,10 +956,10 @@ val type_max_depth = 1 (* TODO: Generate type classes for types? *) -fun features_of ctxt thy num_facts const_tab (scope, _) in_goal ts = +fun features_of ctxt thy num_facts const_tab (scope, _) ts = let val thy_name = Context.theory_name thy in thy_feature_of thy_name :: - term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth in_goal ts + term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth ts |> scope <> Global ? cons local_feature end @@ -1268,7 +1207,7 @@ fun chained_or_extra_features_of factor (((_, stature), th), weight) = [prop_of th] - |> features_of ctxt (theory_of_thm th) num_facts const_tab stature false + |> features_of ctxt (theory_of_thm th) num_facts const_tab stature |> map (apsnd (fn r => weight * factor * r)) fun query_args access_G = @@ -1279,7 +1218,7 @@ |> map (nickname_of_thm o snd) val goal_feats = - features_of ctxt thy num_facts const_tab (Local, General) true (concl_t :: hyp_ts) + features_of ctxt thy num_facts const_tab (Local, General) (concl_t :: hyp_ts) val chained_feats = chained |> map (rpair 1.0) |> map (chained_or_extra_features_of chained_feature_factor) @@ -1375,7 +1314,7 @@ launch_thread timeout (fn () => let val thy = Proof_Context.theory_of ctxt - val feats = features_of ctxt thy 0 Symtab.empty (Local, General) false [t] + val feats = features_of ctxt thy 0 Symtab.empty (Local, General) [t] in map_state ctxt overlord (fn state as {access_G, num_known_facts, dirty} => let @@ -1477,8 +1416,7 @@ (learns, (n, next_commit, _)) = let val name = nickname_of_thm th - val feats = - features_of ctxt (theory_of_thm th) 0 Symtab.empty stature false [prop_of th] + val feats = features_of ctxt (theory_of_thm th) 0 Symtab.empty stature [prop_of th] val deps = deps_of status th |> these val n = n |> not (null deps) ? Integer.add 1 val learns = (name, parents, feats, deps) :: learns diff -r fed0329ea8e2 -r df3a26987a8d src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu May 22 03:29:36 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu May 22 04:12:06 2014 +0200 @@ -10,7 +10,6 @@ val log2 : real -> real val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list val app_hd : ('a -> 'a) -> 'a list -> 'a list - val n_fold_cartesian_product : 'a list list -> 'a list list val plural_s : int -> string val serial_commas : string -> string list -> string list val simplify_spaces : string -> string @@ -43,12 +42,6 @@ fun app_hd f (x :: xs) = f x :: xs -fun cartesian_product [] _ = [] - | cartesian_product (x :: xs) yss = - map (cons x) yss @ cartesian_product xs yss - -fun n_fold_cartesian_product xss = fold_rev cartesian_product xss [[]] - fun plural_s n = if n = 1 then "" else "s" val serial_commas = Try.serial_commas