1.1 --- a/src/HOL/Library/AssocList.thy Fri Jun 18 20:22:06 2010 +0200
1.2 +++ b/src/HOL/Library/AssocList.thy Fri Jun 18 21:22:05 2010 +0200
1.3 @@ -5,7 +5,7 @@
1.4 header {* Map operations implemented on association lists*}
1.5
1.6 theory AssocList
1.7 -imports Main Mapping
1.8 +imports Main More_List Mapping
1.9 begin
1.10
1.11 text {*
1.12 @@ -79,7 +79,7 @@
1.13 by (simp add: update_conv' image_map_upd)
1.14
1.15 definition updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
1.16 - "updates ks vs al = foldl (\<lambda>al (k, v). update k v al) al (zip ks vs)"
1.17 + "updates ks vs = More_List.fold (prod_case update) (zip ks vs)"
1.18
1.19 lemma updates_simps [simp]:
1.20 "updates [] vs ps = ps"
1.21 @@ -94,11 +94,10 @@
1.22
1.23 lemma updates_conv': "map_of (updates ks vs al) = (map_of al)(ks[\<mapsto>]vs)"
1.24 proof -
1.25 - have "foldl (\<lambda>f (k, v). f(k \<mapsto> v)) (map_of al) (zip ks vs) =
1.26 - map_of (foldl (\<lambda>al (k, v). update k v al) al (zip ks vs))"
1.27 - by (rule foldl_apply) (auto simp add: expand_fun_eq update_conv')
1.28 - then show ?thesis
1.29 - by (simp add: updates_def map_upds_fold_map_upd)
1.30 + have "map_of \<circ> More_List.fold (prod_case update) (zip ks vs) =
1.31 + More_List.fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
1.32 + by (rule fold_apply) (auto simp add: expand_fun_eq update_conv')
1.33 + then show ?thesis by (auto simp add: updates_def expand_fun_eq map_upds_fold_map_upd foldl_fold split_def)
1.34 qed
1.35
1.36 lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
1.37 @@ -108,15 +107,14 @@
1.38 assumes "distinct (map fst al)"
1.39 shows "distinct (map fst (updates ks vs al))"
1.40 proof -
1.41 - from assms have "distinct (foldl
1.42 - (\<lambda>al (k, v). if k \<in> set al then al else al @ [k])
1.43 - (map fst al) (zip ks vs))"
1.44 - by (rule foldl_invariant) auto
1.45 - moreover have "foldl (\<lambda>al (k, v). if k \<in> set al then al else al @ [k])
1.46 - (map fst al) (zip ks vs)
1.47 - = map fst (foldl (\<lambda>al (k, v). update k v al) al (zip ks vs))"
1.48 - by (rule foldl_apply) (simp add: update_keys split_def comp_def)
1.49 - ultimately show ?thesis by (simp add: updates_def)
1.50 + have "distinct (More_List.fold
1.51 + (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k])
1.52 + (zip ks vs) (map fst al))"
1.53 + by (rule fold_invariant [of "zip ks vs" "\<lambda>_. True"]) (auto intro: assms)
1.54 + moreover have "map fst \<circ> More_List.fold (prod_case update) (zip ks vs) =
1.55 + More_List.fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
1.56 + by (rule fold_apply) (simp add: update_keys split_def prod_case_beta comp_def)
1.57 + ultimately show ?thesis by (simp add: updates_def expand_fun_eq)
1.58 qed
1.59
1.60 lemma updates_append1[simp]: "size ks < size vs \<Longrightarrow>
1.61 @@ -341,10 +339,10 @@
1.62 lemma clearjunk_updates:
1.63 "clearjunk (updates ks vs al) = updates ks vs (clearjunk al)"
1.64 proof -
1.65 - have "foldl (\<lambda>al (k, v). update k v al) (clearjunk al) (zip ks vs) =
1.66 - clearjunk (foldl (\<lambda>al (k, v). update k v al) al (zip ks vs))"
1.67 - by (rule foldl_apply) (simp add: clearjunk_update expand_fun_eq split_def)
1.68 - then show ?thesis by (simp add: updates_def)
1.69 + have "clearjunk \<circ> More_List.fold (prod_case update) (zip ks vs) =
1.70 + More_List.fold (prod_case update) (zip ks vs) \<circ> clearjunk"
1.71 + by (rule fold_apply) (simp add: clearjunk_update prod_case_beta o_def)
1.72 + then show ?thesis by (simp add: updates_def expand_fun_eq)
1.73 qed
1.74
1.75 lemma clearjunk_delete:
1.76 @@ -429,8 +427,8 @@
1.77
1.78 lemma merge_updates:
1.79 "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs"
1.80 - by (simp add: merge_def updates_def split_def
1.81 - foldr_foldl zip_rev zip_map_fst_snd)
1.82 + by (simp add: merge_def updates_def split_prod_case
1.83 + foldr_fold_rev zip_rev zip_map_fst_snd)
1.84
1.85 lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
1.86 by (induct ys arbitrary: xs) (auto simp add: dom_update)
1.87 @@ -447,11 +445,11 @@
1.88 lemma merge_conv':
1.89 "map_of (merge xs ys) = map_of xs ++ map_of ys"
1.90 proof -
1.91 - have "foldl (\<lambda>m (k, v). m(k \<mapsto> v)) (map_of xs) (rev ys) =
1.92 - map_of (foldl (\<lambda>xs (k, v). update k v xs) xs (rev ys)) "
1.93 - by (rule foldl_apply) (simp add: expand_fun_eq split_def update_conv')
1.94 + have "map_of \<circ> More_List.fold (prod_case update) (rev ys) =
1.95 + More_List.fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
1.96 + by (rule fold_apply) (simp add: update_conv' prod_case_beta split_def expand_fun_eq)
1.97 then show ?thesis
1.98 - by (simp add: merge_def map_add_map_of_foldr foldr_foldl split_def)
1.99 + by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev split_prod_case expand_fun_eq)
1.100 qed
1.101
1.102 corollary merge_conv:
2.1 --- a/src/HOL/Library/Code_Char.thy Fri Jun 18 20:22:06 2010 +0200
2.2 +++ b/src/HOL/Library/Code_Char.thy Fri Jun 18 21:22:05 2010 +0200
2.3 @@ -58,12 +58,12 @@
2.4 (SML "String.implode")
2.5 (OCaml "failwith/ \"implode\"")
2.6 (Haskell "_")
2.7 - (Scala "List.toString((_))")
2.8 + (Scala "!(\"\" ++/ _)")
2.9
2.10 code_const explode
2.11 (SML "String.explode")
2.12 (OCaml "failwith/ \"explode\"")
2.13 (Haskell "_")
2.14 - (Scala "List.fromString((_))")
2.15 + (Scala "!(_.toList)")
2.16
2.17 end
3.1 --- a/src/HOL/Library/RBT.thy Fri Jun 18 20:22:06 2010 +0200
3.2 +++ b/src/HOL/Library/RBT.thy Fri Jun 18 21:22:05 2010 +0200
3.3 @@ -143,7 +143,7 @@
3.4 by (simp add: map_def lookup_RBT lookup_map lookup_impl_of)
3.5
3.6 lemma fold_fold:
3.7 - "fold f t = (\<lambda>s. foldl (\<lambda>s (k, v). f k v s) s (entries t))"
3.8 + "fold f t = More_List.fold (prod_case f) (entries t)"
3.9 by (simp add: fold_def expand_fun_eq RBT_Impl.fold_def entries_impl_of)
3.10
3.11 lemma is_empty_empty [simp]:
4.1 --- a/src/HOL/Library/RBT_Impl.thy Fri Jun 18 20:22:06 2010 +0200
4.2 +++ b/src/HOL/Library/RBT_Impl.thy Fri Jun 18 21:22:05 2010 +0200
4.3 @@ -6,7 +6,7 @@
4.4 header {* Implementation of Red-Black Trees *}
4.5
4.6 theory RBT_Impl
4.7 -imports Main
4.8 +imports Main More_List
4.9 begin
4.10
4.11 text {*
4.12 @@ -1049,7 +1049,7 @@
4.13 subsection {* Folding over entries *}
4.14
4.15 definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
4.16 - "fold f t s = foldl (\<lambda>s (k, v). f k v s) s (entries t)"
4.17 + "fold f t = More_List.fold (prod_case f) (entries t)"
4.18
4.19 lemma fold_simps [simp, code]:
4.20 "fold f Empty = id"
4.21 @@ -1071,12 +1071,12 @@
4.22 proof -
4.23 obtain ys where "ys = rev xs" by simp
4.24 have "\<And>t. is_rbt t \<Longrightarrow>
4.25 - lookup (foldl (\<lambda>t (k, v). insert k v t) t ys) = lookup t ++ map_of (rev ys)"
4.26 - by (induct ys) (simp_all add: bulkload_def split_def lookup_insert)
4.27 + lookup (More_List.fold (prod_case insert) ys t) = lookup t ++ map_of (rev ys)"
4.28 + by (induct ys) (simp_all add: bulkload_def lookup_insert prod_case_beta)
4.29 from this Empty_is_rbt have
4.30 - "lookup (foldl (\<lambda>t (k, v). insert k v t) Empty (rev xs)) = lookup Empty ++ map_of xs"
4.31 + "lookup (More_List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs"
4.32 by (simp add: `ys = rev xs`)
4.33 - then show ?thesis by (simp add: bulkload_def foldl_foldr lookup_Empty split_def)
4.34 + then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_fold_rev prod_case_split)
4.35 qed
4.36
4.37 hide_const (open) Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
5.1 --- a/src/HOL/List.thy Fri Jun 18 20:22:06 2010 +0200
5.2 +++ b/src/HOL/List.thy Fri Jun 18 21:22:05 2010 +0200
5.3 @@ -5,7 +5,7 @@
5.4 header {* The datatype of finite lists *}
5.5
5.6 theory List
5.7 -imports Plain Presburger Sledgehammer Recdef
5.8 +imports Plain Quotient Presburger Code_Numeral Sledgehammer Recdef
5.9 uses ("Tools/list_code.ML")
5.10 begin
5.11
6.1 --- a/src/Pure/Isar/code.ML Fri Jun 18 20:22:06 2010 +0200
6.2 +++ b/src/Pure/Isar/code.ML Fri Jun 18 21:22:05 2010 +0200
6.3 @@ -146,12 +146,12 @@
6.4
6.5 (* functions *)
6.6
6.7 -datatype fun_spec = Default of (thm * bool) list
6.8 +datatype fun_spec = Default of (thm * bool) list * (thm * bool) list lazy
6.9 | Eqns of (thm * bool) list
6.10 | Proj of term * string
6.11 | Abstr of thm * string;
6.12
6.13 -val empty_fun_spec = Default [];
6.14 +val empty_fun_spec = Default ([], Lazy.value []);
6.15
6.16 fun is_default (Default _) = true
6.17 | is_default _ = false;
6.18 @@ -879,10 +879,10 @@
6.19 fun retrieve_raw thy c =
6.20 Symtab.lookup ((the_functions o the_exec) thy) c
6.21 |> Option.map (snd o fst)
6.22 - |> the_default (Default [])
6.23 + |> the_default empty_fun_spec
6.24
6.25 fun get_cert thy f c = case retrieve_raw thy c
6.26 - of Default eqns => eqns
6.27 + of Default (_, eqns_lazy) => Lazy.force eqns_lazy
6.28 |> (map o apfst) (Thm.transfer thy)
6.29 |> f
6.30 |> (map o apfst) (AxClass.unoverload thy)
6.31 @@ -958,7 +958,7 @@
6.32 (Pretty.block o Pretty.fbreaks) (
6.33 Pretty.str (string_of_const thy const) :: map (Display.pretty_thm ctxt) thms
6.34 );
6.35 - fun pretty_function (const, Default eqns) = pretty_equations const (map fst eqns)
6.36 + fun pretty_function (const, Default (_, eqns_lazy)) = pretty_equations const (map fst (Lazy.force eqns_lazy))
6.37 | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns)
6.38 | pretty_function (const, Proj (proj, _)) = Pretty.block
6.39 [Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj]
6.40 @@ -1051,21 +1051,26 @@
6.41 let
6.42 val thm = Thm.close_derivation raw_thm;
6.43 val c = const_eqn thy thm;
6.44 - fun add_eqn' true (Default eqns) = Default (eqns @ [(thm, proper)])
6.45 - | add_eqn' _ (Eqns eqns) =
6.46 - let
6.47 - val args_of = snd o strip_comb o map_types Type.strip_sorts
6.48 - o fst o Logic.dest_equals o Thm.plain_prop_of;
6.49 - val args = args_of thm;
6.50 - val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
6.51 - fun matches_args args' = length args <= length args' andalso
6.52 - Pattern.matchess thy (args, (map incr_idx o take (length args)) args');
6.53 - fun drop (thm', proper') = if (proper orelse not proper')
6.54 - andalso matches_args (args_of thm') then
6.55 - (warning ("Code generator: dropping redundant code equation\n" ^
6.56 - Display.string_of_thm_global thy thm'); true)
6.57 - else false;
6.58 - in Eqns ((thm, proper) :: filter_out drop eqns) end
6.59 + fun update_subsume thy (thm, proper) eqns =
6.60 + let
6.61 + val args_of = snd o strip_comb o map_types Type.strip_sorts
6.62 + o fst o Logic.dest_equals o Thm.plain_prop_of;
6.63 + val args = args_of thm;
6.64 + val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
6.65 + fun matches_args args' = length args <= length args' andalso
6.66 + Pattern.matchess thy (args, (map incr_idx o take (length args)) args');
6.67 + fun drop (thm', proper') = if (proper orelse not proper')
6.68 + andalso matches_args (args_of thm') then
6.69 + (warning ("Code generator: dropping subsumed code equation\n" ^
6.70 + Display.string_of_thm_global thy thm'); true)
6.71 + else false;
6.72 + in (thm, proper) :: filter_out drop eqns end;
6.73 + fun natural_order thy_ref eqns =
6.74 + (eqns, Lazy.lazy (fn () => fold (update_subsume (Theory.deref thy_ref)) eqns []))
6.75 + fun add_eqn' true (Default (eqns, _)) =
6.76 + Default (natural_order (Theory.check_thy thy) ((thm, proper) :: eqns))
6.77 + (*this restores the natural order and drops syntactic redundancies*)
6.78 + | add_eqn' _ (Eqns eqns) = Eqns (update_subsume thy (thm, proper) eqns)
6.79 | add_eqn' false _ = Eqns [(thm, proper)];
6.80 in change_fun_spec false c (add_eqn' default) thy end;
6.81
7.1 --- a/src/Tools/Code/code_scala.ML Fri Jun 18 20:22:06 2010 +0200
7.2 +++ b/src/Tools/Code/code_scala.ML Fri Jun 18 21:22:05 2010 +0200
7.3 @@ -22,7 +22,8 @@
7.4
7.5 (** Scala serializer **)
7.6
7.7 -fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved args_num is_singleton deresolve =
7.8 +fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved
7.9 + args_num is_singleton deresolve =
7.10 let
7.11 val deresolve_base = Long_Name.base_name o deresolve;
7.12 val lookup_tyvar = first_upper oo lookup_var;
7.13 @@ -61,7 +62,8 @@
7.14 then print_case tyvars some_thm vars fxy cases
7.15 else print_app tyvars is_pat some_thm vars fxy c_ts
7.16 | NONE => print_case tyvars some_thm vars fxy cases)
7.17 - and print_app tyvars is_pat some_thm vars fxy (app as ((c, ((arg_typs, _), function_typs)), ts)) =
7.18 + and print_app tyvars is_pat some_thm vars fxy
7.19 + (app as ((c, ((arg_typs, _), function_typs)), ts)) =
7.20 let
7.21 val k = length ts;
7.22 val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l;
7.23 @@ -69,10 +71,12 @@
7.24 (is_none (syntax_const c) andalso is_singleton c) then [] else arg_typs;
7.25 val (no_syntax, print') = case syntax_const c
7.26 of NONE => (true, fn ts => applify "(" ")" fxy
7.27 - (applify "[" "]" NOBR ((str o deresolve) c) (map (print_typ tyvars NOBR) arg_typs'))
7.28 - (map (print_term tyvars is_pat some_thm vars NOBR) ts))
7.29 + (applify "[" "]" NOBR ((str o deresolve) c)
7.30 + (map (print_typ tyvars NOBR) arg_typs'))
7.31 + (map (print_term tyvars is_pat some_thm vars NOBR) ts))
7.32 | SOME (_, print) => (false, fn ts =>
7.33 - print (print_term tyvars is_pat some_thm) some_thm vars fxy (ts ~~ take l function_typs));
7.34 + print (print_term tyvars is_pat some_thm) some_thm vars fxy
7.35 + (ts ~~ take l function_typs));
7.36 in if k = l then print' ts
7.37 else if k < l then
7.38 print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
7.39 @@ -82,7 +86,8 @@
7.40 Pretty.block (print' ts1 :: map (fn t => Pretty.block
7.41 [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts23)
7.42 end end
7.43 - and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars true) some_thm fxy p
7.44 + and print_bind tyvars some_thm fxy p =
7.45 + gen_print_bind (print_term tyvars true) some_thm fxy p
7.46 and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
7.47 let
7.48 val (binds, body) = Code_Thingol.unfold_let (ICase cases);
7.49 @@ -103,8 +108,9 @@
7.50 let
7.51 fun print_select (pat, body) =
7.52 let
7.53 - val (p, vars') = print_bind tyvars some_thm NOBR pat vars;
7.54 - in concat [str "case", p, str "=>", print_term tyvars false some_thm vars' NOBR body] end;
7.55 + val (p_pat, vars') = print_bind tyvars some_thm NOBR pat vars;
7.56 + val p_body = print_term tyvars false some_thm vars' NOBR body
7.57 + in concat [str "case", p_pat, str "=>", p_body] end;
7.58 in brackify_block fxy
7.59 (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"])
7.60 (map print_select clauses)
7.61 @@ -112,25 +118,17 @@
7.62 end
7.63 | print_case tyvars some_thm vars fxy ((_, []), _) =
7.64 (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];
7.65 - fun implicit_arguments tyvars vs vars =
7.66 - let
7.67 - val implicit_typ_ps = maps (fn (v, sort) => map (fn class => Pretty.block
7.68 - [(str o deresolve) class, str "[", (str o lookup_tyvar tyvars) v, str "]"]) sort) vs;
7.69 - val implicit_names = Name.variant_list [] (maps (fn (v, sort) => map (fn class =>
7.70 - lookup_tyvar tyvars v ^ "_" ^ (Long_Name.base_name o deresolve) class) sort) vs);
7.71 - val vars' = intro_vars implicit_names vars;
7.72 - val implicit_ps = map2 (fn v => fn p => concat [str (v ^ ":"), p])
7.73 - implicit_names implicit_typ_ps;
7.74 - in ((implicit_names, implicit_ps), vars') end;
7.75 fun print_defhead tyvars vars p vs params tys implicits (*FIXME simplify*) ty =
7.76 Pretty.block [str "def ", print_typed tyvars (applify "(implicit " ")" NOBR
7.77 (applify "(" ")" NOBR
7.78 (applify "[" "]" NOBR p (map (fn (v, sort) =>
7.79 - (str o implode) (lookup_tyvar tyvars v :: map (prefix ": " o deresolve) sort)) vs))
7.80 + (str o implode)
7.81 + (lookup_tyvar tyvars v :: map (prefix ": " o deresolve) sort)) vs))
7.82 (map2 (fn param => fn ty => print_typed tyvars
7.83 ((str o lookup_var vars) param) ty)
7.84 params tys)) implicits) ty, str " ="]
7.85 - fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) = (case filter (snd o snd) raw_eqs
7.86 + fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
7.87 + (case filter (snd o snd) raw_eqs
7.88 of [] =>
7.89 let
7.90 val (tys, ty') = Code_Thingol.unfold_fun ty;
7.91 @@ -157,30 +155,33 @@
7.92 val vars1 = reserved
7.93 |> intro_base_names
7.94 (is_none o syntax_const) deresolve consts
7.95 - val ((_, implicit_ps), vars2) = implicit_arguments tyvars vs vars1; (*FIXME drop*)
7.96 - val params = if simple then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
7.97 - else aux_params vars2 (map (fst o fst) eqs);
7.98 - val vars3 = intro_vars params vars2;
7.99 + val params = if simple
7.100 + then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
7.101 + else aux_params vars1 (map (fst o fst) eqs);
7.102 + val vars2 = intro_vars params vars1;
7.103 val (tys, ty1) = Code_Thingol.unfold_fun ty;
7.104 val (tys1, tys2) = chop (length params) tys;
7.105 val ty2 = Library.foldr
7.106 (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (tys2, ty1);
7.107 fun print_tuple [p] = p
7.108 | print_tuple ps = enum "," "(" ")" ps;
7.109 - fun print_rhs vars' ((_, t), (some_thm, _)) = print_term tyvars false some_thm vars' NOBR t;
7.110 + fun print_rhs vars' ((_, t), (some_thm, _)) =
7.111 + print_term tyvars false some_thm vars' NOBR t;
7.112 fun print_clause (eq as ((ts, _), (some_thm, _))) =
7.113 let
7.114 - val vars' = intro_vars ((fold o Code_Thingol.fold_varnames) (insert (op =)) ts []) vars2;
7.115 + val vars' = intro_vars ((fold o Code_Thingol.fold_varnames)
7.116 + (insert (op =)) ts []) vars1;
7.117 in
7.118 - concat [str "case", print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts),
7.119 + concat [str "case",
7.120 + print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts),
7.121 str "=>", print_rhs vars' eq]
7.122 end;
7.123 - val head = print_defhead tyvars vars3 ((str o deresolve) name) vs params tys1 [] ty2;
7.124 + val head = print_defhead tyvars vars2 ((str o deresolve) name) vs params tys1 [] ty2;
7.125 in if simple then
7.126 - concat [head, print_rhs vars3 (hd eqs)]
7.127 + concat [head, print_rhs vars2 (hd eqs)]
7.128 else
7.129 Pretty.block_enclose
7.130 - (concat [head, print_tuple (map (str o lookup_var vars3) params),
7.131 + (concat [head, print_tuple (map (str o lookup_var vars2) params),
7.132 str "match", str "{"], str "}")
7.133 (map print_clause eqs)
7.134 end)
7.135 @@ -202,7 +203,8 @@
7.136 in
7.137 concat [
7.138 applify "(" ")" NOBR
7.139 - (add_typargs2 ((concat o map str) ["final", "case", "class", deresolve_base co]))
7.140 + (add_typargs2 ((concat o map str)
7.141 + ["final", "case", "class", deresolve_base co]))
7.142 (map (uncurry (print_typed tyvars) o apfst str) fields),
7.143 str "extends",
7.144 add_typargs1 ((str o deresolve_base) name)
7.145 @@ -210,7 +212,8 @@
7.146 end
7.147 in
7.148 Pretty.chunks (
7.149 - applify "[" "]" NOBR ((concat o map str) ["sealed", "class", deresolve_base name])
7.150 + applify "[" "]" NOBR ((concat o map str)
7.151 + ["sealed", "class", deresolve_base name])
7.152 (map (str o prefix "+" o lookup_tyvar tyvars o fst) vs)
7.153 :: map print_co cos
7.154 )
7.155 @@ -222,7 +225,8 @@
7.156 fun add_typarg p = applify "[" "]" NOBR p [(str o lookup_tyvar tyvars) v];
7.157 fun print_super_classes [] = NONE
7.158 | print_super_classes classes = SOME (concat (str "extends"
7.159 - :: separate (str "with") (map (add_typarg o str o deresolve o fst) classes)));
7.160 + :: separate (str "with")
7.161 + (map (add_typarg o str o deresolve o fst) classes)));
7.162 fun print_tupled_typ ([], ty) =
7.163 print_typ tyvars NOBR ty
7.164 | print_tupled_typ ([ty1], ty2) =
7.165 @@ -231,14 +235,17 @@
7.166 concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys),
7.167 str "=>", print_typ tyvars NOBR ty];
7.168 fun print_classparam_val (classparam, ty) =
7.169 - concat [str "val", (str o Library.enclose "`" "+`:" o deresolve_base) classparam,
7.170 + concat [str "val", (str o Library.enclose "`" "+`:" o deresolve_base)
7.171 + classparam,
7.172 (print_tupled_typ o Code_Thingol.unfold_fun) ty]
7.173 fun implicit_arguments tyvars vs vars = (*FIXME simplifiy*)
7.174 let
7.175 val implicit_typ_ps = maps (fn (v, sort) => map (fn class => Pretty.block
7.176 - [(str o deresolve) class, str "[", (str o lookup_tyvar tyvars) v, str "]"]) sort) vs;
7.177 - val implicit_names = Name.variant_list [] (maps (fn (v, sort) => map (fn class =>
7.178 - lookup_tyvar tyvars v ^ "_" ^ (Long_Name.base_name o deresolve) class) sort) vs);
7.179 + [(str o deresolve) class, str "[",
7.180 + (str o lookup_tyvar tyvars) v, str "]"]) sort) vs;
7.181 + val implicit_names = Name.variant_list [] (maps (fn (v, sort) =>
7.182 + map (fn class => lookup_tyvar tyvars v ^ "_" ^
7.183 + (Long_Name.base_name o deresolve) class) sort) vs);
7.184 val vars' = intro_vars implicit_names vars;
7.185 val implicit_ps = map2 (fn v => fn p => concat [str (v ^ ":"), p])
7.186 implicit_names implicit_typ_ps;
7.187 @@ -253,7 +260,8 @@
7.188 ((map o apsnd) (K []) vs) params tys [p_implicit] ty;
7.189 in
7.190 concat [head, applify "(" ")" NOBR
7.191 - (Pretty.block [str implicit, str ".", (str o Library.enclose "`" "+`" o deresolve_base) classparam])
7.192 + (Pretty.block [str implicit, str ".",
7.193 + (str o Library.enclose "`" "+`" o deresolve_base) classparam])
7.194 (map (str o lookup_var vars') params)]
7.195 end;
7.196 in
7.197 @@ -320,7 +328,10 @@
7.198 let
7.199 val (base', nsp_common') =
7.200 mk_name_stmt (if upper then first_upper base else base) nsp_common
7.201 - in (base', ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common')) end;
7.202 + in
7.203 + (base',
7.204 + ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
7.205 + end;
7.206 val add_name = case stmt
7.207 of Code_Thingol.Fun _ => add_object
7.208 | Code_Thingol.Datatype _ => add_class
7.209 @@ -348,7 +359,8 @@
7.210
7.211 fun serialize_scala raw_module_name labelled_name
7.212 raw_reserved includes raw_module_alias
7.213 - _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
7.214 + _ syntax_tyco syntax_const (code_of_pretty, code_writeln)
7.215 + program stmt_names destination =
7.216 let
7.217 val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
7.218 val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
7.219 @@ -357,13 +369,16 @@
7.220 module_name reserved raw_module_alias program;
7.221 val reserved = make_vars reserved;
7.222 fun args_num c = case Graph.get_node program c
7.223 - of Code_Thingol.Fun (_, (((_, ty), []), _)) => (length o fst o Code_Thingol.unfold_fun) ty
7.224 + of Code_Thingol.Fun (_, (((_, ty), []), _)) =>
7.225 + (length o fst o Code_Thingol.unfold_fun) ty
7.226 | Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts
7.227 | Code_Thingol.Datatypecons (_, tyco) =>
7.228 let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
7.229 in (length o the o AList.lookup (eq_fst op =) constrs) (c, []) end (*FIXME simplify lookup*)
7.230 | Code_Thingol.Classparam (_, class) =>
7.231 - let val Code_Thingol.Class (_, (_, (_, classparams))) = Graph.get_node program class
7.232 + let
7.233 + val Code_Thingol.Class (_, (_, (_, classparams))) =
7.234 + Graph.get_node program class
7.235 in (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =) classparams) c end;
7.236 fun is_singleton c = case Graph.get_node program c
7.237 of Code_Thingol.Datatypecons (_, tyco) =>
7.238 @@ -438,12 +453,13 @@
7.239
7.240 val setup =
7.241 Code_Target.add_target (target, (isar_seri_scala, literals))
7.242 - #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
7.243 - brackify_infix (1, R) fxy (
7.244 - print_typ BR ty1 (*product type vs. tupled arguments!*),
7.245 - str "=>",
7.246 - print_typ (INFX (1, R)) ty2
7.247 - )))
7.248 + #> Code_Target.add_syntax_tyco target "fun"
7.249 + (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
7.250 + brackify_infix (1, R) fxy (
7.251 + print_typ BR ty1 (*product type vs. tupled arguments!*),
7.252 + str "=>",
7.253 + print_typ (INFX (1, R)) ty2
7.254 + )))
7.255 #> fold (Code_Target.add_reserved target) [
7.256 "abstract", "case", "catch", "class", "def", "do", "else", "extends", "false",
7.257 "final", "finally", "for", "forSome", "if", "implicit", "import", "lazy",
8.1 --- a/src/Tools/Code/code_simp.ML Fri Jun 18 20:22:06 2010 +0200
8.2 +++ b/src/Tools/Code/code_simp.ML Fri Jun 18 21:22:05 2010 +0200
8.3 @@ -46,6 +46,8 @@
8.4
8.5 val map_ss = Simpset.map;
8.6
8.7 +fun simpset_default thy = Simplifier.global_context thy o the_default (Simpset.get thy);
8.8 +
8.9
8.10 (* build simpset and conversion from program *)
8.11
8.12 @@ -58,8 +60,9 @@
8.13 val add_program = Graph.fold (add_stmt o fst o snd)
8.14
8.15 fun rewrite_modulo thy some_ss program = Simplifier.full_rewrite
8.16 - (add_program program (Simplifier.global_context thy
8.17 - (the_default (Simpset.get thy) some_ss)));
8.18 + (add_program program (simpset_default thy some_ss));
8.19 +
8.20 +fun conclude_tac thy some_ss = Simplifier.full_simp_tac (simpset_default thy some_ss);
8.21
8.22
8.23 (* evaluation with current code context *)
8.24 @@ -67,12 +70,12 @@
8.25 fun current_conv thy = no_frees_conv (Code_Thingol.eval_conv thy
8.26 (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program));
8.27
8.28 -fun current_tac thy = CONVERSION (current_conv thy);
8.29 +fun current_tac thy = CONVERSION (current_conv thy) THEN' conclude_tac thy NONE;
8.30
8.31 -fun current_value thy = snd o Logic.dest_equals o Thm.prop_of o current_conv thy o Thm.cterm_of thy
8.32 +fun current_value thy = snd o Logic.dest_equals o Thm.prop_of o current_conv thy o Thm.cterm_of thy;
8.33
8.34 val setup = Method.setup (Binding.name "code_simp")
8.35 - (Scan.succeed (SIMPLE_METHOD' o current_tac o ProofContext.theory_of))
8.36 + (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo current_tac o ProofContext.theory_of)))
8.37 "simplification with code equations"
8.38 #> Value.add_evaluator ("simp", current_value o ProofContext.theory_of);
8.39
8.40 @@ -82,6 +85,7 @@
8.41 fun make_conv thy some_ss consts = no_frees_conv (Code_Preproc.pre_post_conv thy
8.42 ((rewrite_modulo thy some_ss o snd o snd o Code_Thingol.consts_program thy false) consts));
8.43
8.44 -fun make_tac thy some_ss consts = CONVERSION (make_conv thy some_ss consts);
8.45 +fun make_tac thy some_ss consts = CONVERSION (make_conv thy some_ss consts)
8.46 + THEN' conclude_tac thy some_ss;
8.47
8.48 end;