| author | haftmann |
| Fri, 18 Jun 2010 21:22:05 +0200 | |
| changeset 37465 | fcc2c36b3770 |
| parent 37456 | 0a1cc2675958 (current diff) |
| parent 37464 | 9250ad1b98e0 (diff) |
| child 37467 | 13328f8853c7 |
| child 37468 | a2a3b62fc819 |
| src/HOL/List.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Library/AssocList.thy Fri Jun 18 20:22:06 2010 +0200 +++ b/src/HOL/Library/AssocList.thy Fri Jun 18 21:22:05 2010 +0200 @@ -5,7 +5,7 @@ header {* Map operations implemented on association lists*} theory AssocList -imports Main Mapping +imports Main More_List Mapping begin text {* @@ -79,7 +79,7 @@ by (simp add: update_conv' image_map_upd) definition updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where - "updates ks vs al = foldl (\<lambda>al (k, v). update k v al) al (zip ks vs)" + "updates ks vs = More_List.fold (prod_case update) (zip ks vs)" lemma updates_simps [simp]: "updates [] vs ps = ps" @@ -94,11 +94,10 @@ lemma updates_conv': "map_of (updates ks vs al) = (map_of al)(ks[\<mapsto>]vs)" proof - - have "foldl (\<lambda>f (k, v). f(k \<mapsto> v)) (map_of al) (zip ks vs) = - map_of (foldl (\<lambda>al (k, v). update k v al) al (zip ks vs))" - by (rule foldl_apply) (auto simp add: expand_fun_eq update_conv') - then show ?thesis - by (simp add: updates_def map_upds_fold_map_upd) + have "map_of \<circ> More_List.fold (prod_case update) (zip ks vs) = + More_List.fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of" + by (rule fold_apply) (auto simp add: expand_fun_eq update_conv') + then show ?thesis by (auto simp add: updates_def expand_fun_eq map_upds_fold_map_upd foldl_fold split_def) qed lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k" @@ -108,15 +107,14 @@ assumes "distinct (map fst al)" shows "distinct (map fst (updates ks vs al))" proof - - from assms have "distinct (foldl - (\<lambda>al (k, v). if k \<in> set al then al else al @ [k]) - (map fst al) (zip ks vs))" - by (rule foldl_invariant) auto - moreover have "foldl (\<lambda>al (k, v). if k \<in> set al then al else al @ [k]) - (map fst al) (zip ks vs) - = map fst (foldl (\<lambda>al (k, v). update k v al) al (zip ks vs))" - by (rule foldl_apply) (simp add: update_keys split_def comp_def) - ultimately show ?thesis by (simp add: updates_def) + have "distinct (More_List.fold + (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) + (zip ks vs) (map fst al))" + by (rule fold_invariant [of "zip ks vs" "\<lambda>_. True"]) (auto intro: assms) + moreover have "map fst \<circ> More_List.fold (prod_case update) (zip ks vs) = + More_List.fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst" + by (rule fold_apply) (simp add: update_keys split_def prod_case_beta comp_def) + ultimately show ?thesis by (simp add: updates_def expand_fun_eq) qed lemma updates_append1[simp]: "size ks < size vs \<Longrightarrow> @@ -341,10 +339,10 @@ lemma clearjunk_updates: "clearjunk (updates ks vs al) = updates ks vs (clearjunk al)" proof - - have "foldl (\<lambda>al (k, v). update k v al) (clearjunk al) (zip ks vs) = - clearjunk (foldl (\<lambda>al (k, v). update k v al) al (zip ks vs))" - by (rule foldl_apply) (simp add: clearjunk_update expand_fun_eq split_def) - then show ?thesis by (simp add: updates_def) + have "clearjunk \<circ> More_List.fold (prod_case update) (zip ks vs) = + More_List.fold (prod_case update) (zip ks vs) \<circ> clearjunk" + by (rule fold_apply) (simp add: clearjunk_update prod_case_beta o_def) + then show ?thesis by (simp add: updates_def expand_fun_eq) qed lemma clearjunk_delete: @@ -429,8 +427,8 @@ lemma merge_updates: "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs" - by (simp add: merge_def updates_def split_def - foldr_foldl zip_rev zip_map_fst_snd) + by (simp add: merge_def updates_def split_prod_case + foldr_fold_rev zip_rev zip_map_fst_snd) lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys" by (induct ys arbitrary: xs) (auto simp add: dom_update) @@ -447,11 +445,11 @@ lemma merge_conv': "map_of (merge xs ys) = map_of xs ++ map_of ys" proof - - have "foldl (\<lambda>m (k, v). m(k \<mapsto> v)) (map_of xs) (rev ys) = - map_of (foldl (\<lambda>xs (k, v). update k v xs) xs (rev ys)) " - by (rule foldl_apply) (simp add: expand_fun_eq split_def update_conv') + have "map_of \<circ> More_List.fold (prod_case update) (rev ys) = + More_List.fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of" + by (rule fold_apply) (simp add: update_conv' prod_case_beta split_def expand_fun_eq) then show ?thesis - by (simp add: merge_def map_add_map_of_foldr foldr_foldl split_def) + by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev split_prod_case expand_fun_eq) qed corollary merge_conv:
--- a/src/HOL/Library/Code_Char.thy Fri Jun 18 20:22:06 2010 +0200 +++ b/src/HOL/Library/Code_Char.thy Fri Jun 18 21:22:05 2010 +0200 @@ -58,12 +58,12 @@ (SML "String.implode") (OCaml "failwith/ \"implode\"") (Haskell "_") - (Scala "List.toString((_))") + (Scala "!(\"\" ++/ _)") code_const explode (SML "String.explode") (OCaml "failwith/ \"explode\"") (Haskell "_") - (Scala "List.fromString((_))") + (Scala "!(_.toList)") end
--- a/src/HOL/Library/RBT.thy Fri Jun 18 20:22:06 2010 +0200 +++ b/src/HOL/Library/RBT.thy Fri Jun 18 21:22:05 2010 +0200 @@ -143,7 +143,7 @@ by (simp add: map_def lookup_RBT lookup_map lookup_impl_of) lemma fold_fold: - "fold f t = (\<lambda>s. foldl (\<lambda>s (k, v). f k v s) s (entries t))" + "fold f t = More_List.fold (prod_case f) (entries t)" by (simp add: fold_def expand_fun_eq RBT_Impl.fold_def entries_impl_of) lemma is_empty_empty [simp]:
--- a/src/HOL/Library/RBT_Impl.thy Fri Jun 18 20:22:06 2010 +0200 +++ b/src/HOL/Library/RBT_Impl.thy Fri Jun 18 21:22:05 2010 +0200 @@ -6,7 +6,7 @@ header {* Implementation of Red-Black Trees *} theory RBT_Impl -imports Main +imports Main More_List begin text {* @@ -1049,7 +1049,7 @@ subsection {* Folding over entries *} definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where - "fold f t s = foldl (\<lambda>s (k, v). f k v s) s (entries t)" + "fold f t = More_List.fold (prod_case f) (entries t)" lemma fold_simps [simp, code]: "fold f Empty = id" @@ -1071,12 +1071,12 @@ proof - obtain ys where "ys = rev xs" by simp have "\<And>t. is_rbt t \<Longrightarrow> - lookup (foldl (\<lambda>t (k, v). insert k v t) t ys) = lookup t ++ map_of (rev ys)" - by (induct ys) (simp_all add: bulkload_def split_def lookup_insert) + lookup (More_List.fold (prod_case insert) ys t) = lookup t ++ map_of (rev ys)" + by (induct ys) (simp_all add: bulkload_def lookup_insert prod_case_beta) from this Empty_is_rbt have - "lookup (foldl (\<lambda>t (k, v). insert k v t) Empty (rev xs)) = lookup Empty ++ map_of xs" + "lookup (More_List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs" by (simp add: `ys = rev xs`) - then show ?thesis by (simp add: bulkload_def foldl_foldr lookup_Empty split_def) + then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_fold_rev prod_case_split) qed hide_const (open) Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
--- a/src/HOL/List.thy Fri Jun 18 20:22:06 2010 +0200 +++ b/src/HOL/List.thy Fri Jun 18 21:22:05 2010 +0200 @@ -5,7 +5,7 @@ header {* The datatype of finite lists *} theory List -imports Plain Presburger Sledgehammer Recdef +imports Plain Quotient Presburger Code_Numeral Sledgehammer Recdef uses ("Tools/list_code.ML") begin
--- a/src/Pure/Isar/code.ML Fri Jun 18 20:22:06 2010 +0200 +++ b/src/Pure/Isar/code.ML Fri Jun 18 21:22:05 2010 +0200 @@ -146,12 +146,12 @@ (* functions *) -datatype fun_spec = Default of (thm * bool) list +datatype fun_spec = Default of (thm * bool) list * (thm * bool) list lazy | Eqns of (thm * bool) list | Proj of term * string | Abstr of thm * string; -val empty_fun_spec = Default []; +val empty_fun_spec = Default ([], Lazy.value []); fun is_default (Default _) = true | is_default _ = false; @@ -879,10 +879,10 @@ fun retrieve_raw thy c = Symtab.lookup ((the_functions o the_exec) thy) c |> Option.map (snd o fst) - |> the_default (Default []) + |> the_default empty_fun_spec fun get_cert thy f c = case retrieve_raw thy c - of Default eqns => eqns + of Default (_, eqns_lazy) => Lazy.force eqns_lazy |> (map o apfst) (Thm.transfer thy) |> f |> (map o apfst) (AxClass.unoverload thy) @@ -958,7 +958,7 @@ (Pretty.block o Pretty.fbreaks) ( Pretty.str (string_of_const thy const) :: map (Display.pretty_thm ctxt) thms ); - fun pretty_function (const, Default eqns) = pretty_equations const (map fst eqns) + fun pretty_function (const, Default (_, eqns_lazy)) = pretty_equations const (map fst (Lazy.force eqns_lazy)) | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns) | pretty_function (const, Proj (proj, _)) = Pretty.block [Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj] @@ -1051,21 +1051,26 @@ let val thm = Thm.close_derivation raw_thm; val c = const_eqn thy thm; - fun add_eqn' true (Default eqns) = Default (eqns @ [(thm, proper)]) - | add_eqn' _ (Eqns eqns) = - let - val args_of = snd o strip_comb o map_types Type.strip_sorts - o fst o Logic.dest_equals o Thm.plain_prop_of; - val args = args_of thm; - val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1); - fun matches_args args' = length args <= length args' andalso - Pattern.matchess thy (args, (map incr_idx o take (length args)) args'); - fun drop (thm', proper') = if (proper orelse not proper') - andalso matches_args (args_of thm') then - (warning ("Code generator: dropping redundant code equation\n" ^ - Display.string_of_thm_global thy thm'); true) - else false; - in Eqns ((thm, proper) :: filter_out drop eqns) end + fun update_subsume thy (thm, proper) eqns = + let + val args_of = snd o strip_comb o map_types Type.strip_sorts + o fst o Logic.dest_equals o Thm.plain_prop_of; + val args = args_of thm; + val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1); + fun matches_args args' = length args <= length args' andalso + Pattern.matchess thy (args, (map incr_idx o take (length args)) args'); + fun drop (thm', proper') = if (proper orelse not proper') + andalso matches_args (args_of thm') then + (warning ("Code generator: dropping subsumed code equation\n" ^ + Display.string_of_thm_global thy thm'); true) + else false; + in (thm, proper) :: filter_out drop eqns end; + fun natural_order thy_ref eqns = + (eqns, Lazy.lazy (fn () => fold (update_subsume (Theory.deref thy_ref)) eqns [])) + fun add_eqn' true (Default (eqns, _)) = + Default (natural_order (Theory.check_thy thy) ((thm, proper) :: eqns)) + (*this restores the natural order and drops syntactic redundancies*) + | add_eqn' _ (Eqns eqns) = Eqns (update_subsume thy (thm, proper) eqns) | add_eqn' false _ = Eqns [(thm, proper)]; in change_fun_spec false c (add_eqn' default) thy end;
--- a/src/Tools/Code/code_scala.ML Fri Jun 18 20:22:06 2010 +0200 +++ b/src/Tools/Code/code_scala.ML Fri Jun 18 21:22:05 2010 +0200 @@ -22,7 +22,8 @@ (** Scala serializer **) -fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved args_num is_singleton deresolve = +fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved + args_num is_singleton deresolve = let val deresolve_base = Long_Name.base_name o deresolve; val lookup_tyvar = first_upper oo lookup_var; @@ -61,7 +62,8 @@ then print_case tyvars some_thm vars fxy cases else print_app tyvars is_pat some_thm vars fxy c_ts | NONE => print_case tyvars some_thm vars fxy cases) - and print_app tyvars is_pat some_thm vars fxy (app as ((c, ((arg_typs, _), function_typs)), ts)) = + and print_app tyvars is_pat some_thm vars fxy + (app as ((c, ((arg_typs, _), function_typs)), ts)) = let val k = length ts; val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l; @@ -69,10 +71,12 @@ (is_none (syntax_const c) andalso is_singleton c) then [] else arg_typs; val (no_syntax, print') = case syntax_const c of NONE => (true, fn ts => applify "(" ")" fxy - (applify "[" "]" NOBR ((str o deresolve) c) (map (print_typ tyvars NOBR) arg_typs')) - (map (print_term tyvars is_pat some_thm vars NOBR) ts)) + (applify "[" "]" NOBR ((str o deresolve) c) + (map (print_typ tyvars NOBR) arg_typs')) + (map (print_term tyvars is_pat some_thm vars NOBR) ts)) | SOME (_, print) => (false, fn ts => - print (print_term tyvars is_pat some_thm) some_thm vars fxy (ts ~~ take l function_typs)); + print (print_term tyvars is_pat some_thm) some_thm vars fxy + (ts ~~ take l function_typs)); in if k = l then print' ts else if k < l then print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app) @@ -82,7 +86,8 @@ Pretty.block (print' ts1 :: map (fn t => Pretty.block [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts23) end end - and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars true) some_thm fxy p + and print_bind tyvars some_thm fxy p = + gen_print_bind (print_term tyvars true) some_thm fxy p and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) = let val (binds, body) = Code_Thingol.unfold_let (ICase cases); @@ -103,8 +108,9 @@ let fun print_select (pat, body) = let - val (p, vars') = print_bind tyvars some_thm NOBR pat vars; - in concat [str "case", p, str "=>", print_term tyvars false some_thm vars' NOBR body] end; + val (p_pat, vars') = print_bind tyvars some_thm NOBR pat vars; + val p_body = print_term tyvars false some_thm vars' NOBR body + in concat [str "case", p_pat, str "=>", p_body] end; in brackify_block fxy (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"]) (map print_select clauses) @@ -112,25 +118,17 @@ end | print_case tyvars some_thm vars fxy ((_, []), _) = (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"]; - fun implicit_arguments tyvars vs vars = - let - val implicit_typ_ps = maps (fn (v, sort) => map (fn class => Pretty.block - [(str o deresolve) class, str "[", (str o lookup_tyvar tyvars) v, str "]"]) sort) vs; - val implicit_names = Name.variant_list [] (maps (fn (v, sort) => map (fn class => - lookup_tyvar tyvars v ^ "_" ^ (Long_Name.base_name o deresolve) class) sort) vs); - val vars' = intro_vars implicit_names vars; - val implicit_ps = map2 (fn v => fn p => concat [str (v ^ ":"), p]) - implicit_names implicit_typ_ps; - in ((implicit_names, implicit_ps), vars') end; fun print_defhead tyvars vars p vs params tys implicits (*FIXME simplify*) ty = Pretty.block [str "def ", print_typed tyvars (applify "(implicit " ")" NOBR (applify "(" ")" NOBR (applify "[" "]" NOBR p (map (fn (v, sort) => - (str o implode) (lookup_tyvar tyvars v :: map (prefix ": " o deresolve) sort)) vs)) + (str o implode) + (lookup_tyvar tyvars v :: map (prefix ": " o deresolve) sort)) vs)) (map2 (fn param => fn ty => print_typed tyvars ((str o lookup_var vars) param) ty) params tys)) implicits) ty, str " ="] - fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) = (case filter (snd o snd) raw_eqs + fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) = + (case filter (snd o snd) raw_eqs of [] => let val (tys, ty') = Code_Thingol.unfold_fun ty; @@ -157,30 +155,33 @@ val vars1 = reserved |> intro_base_names (is_none o syntax_const) deresolve consts - val ((_, implicit_ps), vars2) = implicit_arguments tyvars vs vars1; (*FIXME drop*) - val params = if simple then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs - else aux_params vars2 (map (fst o fst) eqs); - val vars3 = intro_vars params vars2; + val params = if simple + then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs + else aux_params vars1 (map (fst o fst) eqs); + val vars2 = intro_vars params vars1; val (tys, ty1) = Code_Thingol.unfold_fun ty; val (tys1, tys2) = chop (length params) tys; val ty2 = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (tys2, ty1); fun print_tuple [p] = p | print_tuple ps = enum "," "(" ")" ps; - fun print_rhs vars' ((_, t), (some_thm, _)) = print_term tyvars false some_thm vars' NOBR t; + fun print_rhs vars' ((_, t), (some_thm, _)) = + print_term tyvars false some_thm vars' NOBR t; fun print_clause (eq as ((ts, _), (some_thm, _))) = let - val vars' = intro_vars ((fold o Code_Thingol.fold_varnames) (insert (op =)) ts []) vars2; + val vars' = intro_vars ((fold o Code_Thingol.fold_varnames) + (insert (op =)) ts []) vars1; in - concat [str "case", print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts), + concat [str "case", + print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts), str "=>", print_rhs vars' eq] end; - val head = print_defhead tyvars vars3 ((str o deresolve) name) vs params tys1 [] ty2; + val head = print_defhead tyvars vars2 ((str o deresolve) name) vs params tys1 [] ty2; in if simple then - concat [head, print_rhs vars3 (hd eqs)] + concat [head, print_rhs vars2 (hd eqs)] else Pretty.block_enclose - (concat [head, print_tuple (map (str o lookup_var vars3) params), + (concat [head, print_tuple (map (str o lookup_var vars2) params), str "match", str "{"], str "}") (map print_clause eqs) end) @@ -202,7 +203,8 @@ in concat [ applify "(" ")" NOBR - (add_typargs2 ((concat o map str) ["final", "case", "class", deresolve_base co])) + (add_typargs2 ((concat o map str) + ["final", "case", "class", deresolve_base co])) (map (uncurry (print_typed tyvars) o apfst str) fields), str "extends", add_typargs1 ((str o deresolve_base) name) @@ -210,7 +212,8 @@ end in Pretty.chunks ( - applify "[" "]" NOBR ((concat o map str) ["sealed", "class", deresolve_base name]) + applify "[" "]" NOBR ((concat o map str) + ["sealed", "class", deresolve_base name]) (map (str o prefix "+" o lookup_tyvar tyvars o fst) vs) :: map print_co cos ) @@ -222,7 +225,8 @@ fun add_typarg p = applify "[" "]" NOBR p [(str o lookup_tyvar tyvars) v]; fun print_super_classes [] = NONE | print_super_classes classes = SOME (concat (str "extends" - :: separate (str "with") (map (add_typarg o str o deresolve o fst) classes))); + :: separate (str "with") + (map (add_typarg o str o deresolve o fst) classes))); fun print_tupled_typ ([], ty) = print_typ tyvars NOBR ty | print_tupled_typ ([ty1], ty2) = @@ -231,14 +235,17 @@ concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys), str "=>", print_typ tyvars NOBR ty]; fun print_classparam_val (classparam, ty) = - concat [str "val", (str o Library.enclose "`" "+`:" o deresolve_base) classparam, + concat [str "val", (str o Library.enclose "`" "+`:" o deresolve_base) + classparam, (print_tupled_typ o Code_Thingol.unfold_fun) ty] fun implicit_arguments tyvars vs vars = (*FIXME simplifiy*) let val implicit_typ_ps = maps (fn (v, sort) => map (fn class => Pretty.block - [(str o deresolve) class, str "[", (str o lookup_tyvar tyvars) v, str "]"]) sort) vs; - val implicit_names = Name.variant_list [] (maps (fn (v, sort) => map (fn class => - lookup_tyvar tyvars v ^ "_" ^ (Long_Name.base_name o deresolve) class) sort) vs); + [(str o deresolve) class, str "[", + (str o lookup_tyvar tyvars) v, str "]"]) sort) vs; + val implicit_names = Name.variant_list [] (maps (fn (v, sort) => + map (fn class => lookup_tyvar tyvars v ^ "_" ^ + (Long_Name.base_name o deresolve) class) sort) vs); val vars' = intro_vars implicit_names vars; val implicit_ps = map2 (fn v => fn p => concat [str (v ^ ":"), p]) implicit_names implicit_typ_ps; @@ -253,7 +260,8 @@ ((map o apsnd) (K []) vs) params tys [p_implicit] ty; in concat [head, applify "(" ")" NOBR - (Pretty.block [str implicit, str ".", (str o Library.enclose "`" "+`" o deresolve_base) classparam]) + (Pretty.block [str implicit, str ".", + (str o Library.enclose "`" "+`" o deresolve_base) classparam]) (map (str o lookup_var vars') params)] end; in @@ -320,7 +328,10 @@ let val (base', nsp_common') = mk_name_stmt (if upper then first_upper base else base) nsp_common - in (base', ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common')) end; + in + (base', + ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common')) + end; val add_name = case stmt of Code_Thingol.Fun _ => add_object | Code_Thingol.Datatype _ => add_class @@ -348,7 +359,8 @@ fun serialize_scala raw_module_name labelled_name raw_reserved includes raw_module_alias - _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination = + _ syntax_tyco syntax_const (code_of_pretty, code_writeln) + program stmt_names destination = let val presentation_stmt_names = Code_Target.stmt_names_of_destination destination; val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code"; @@ -357,13 +369,16 @@ module_name reserved raw_module_alias program; val reserved = make_vars reserved; fun args_num c = case Graph.get_node program c - of Code_Thingol.Fun (_, (((_, ty), []), _)) => (length o fst o Code_Thingol.unfold_fun) ty + of Code_Thingol.Fun (_, (((_, ty), []), _)) => + (length o fst o Code_Thingol.unfold_fun) ty | Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts | Code_Thingol.Datatypecons (_, tyco) => let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco in (length o the o AList.lookup (eq_fst op =) constrs) (c, []) end (*FIXME simplify lookup*) | Code_Thingol.Classparam (_, class) => - let val Code_Thingol.Class (_, (_, (_, classparams))) = Graph.get_node program class + let + val Code_Thingol.Class (_, (_, (_, classparams))) = + Graph.get_node program class in (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =) classparams) c end; fun is_singleton c = case Graph.get_node program c of Code_Thingol.Datatypecons (_, tyco) => @@ -438,12 +453,13 @@ val setup = Code_Target.add_target (target, (isar_seri_scala, literals)) - #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => - brackify_infix (1, R) fxy ( - print_typ BR ty1 (*product type vs. tupled arguments!*), - str "=>", - print_typ (INFX (1, R)) ty2 - ))) + #> Code_Target.add_syntax_tyco target "fun" + (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => + brackify_infix (1, R) fxy ( + print_typ BR ty1 (*product type vs. tupled arguments!*), + str "=>", + print_typ (INFX (1, R)) ty2 + ))) #> fold (Code_Target.add_reserved target) [ "abstract", "case", "catch", "class", "def", "do", "else", "extends", "false", "final", "finally", "for", "forSome", "if", "implicit", "import", "lazy",
--- a/src/Tools/Code/code_simp.ML Fri Jun 18 20:22:06 2010 +0200 +++ b/src/Tools/Code/code_simp.ML Fri Jun 18 21:22:05 2010 +0200 @@ -46,6 +46,8 @@ val map_ss = Simpset.map; +fun simpset_default thy = Simplifier.global_context thy o the_default (Simpset.get thy); + (* build simpset and conversion from program *) @@ -58,8 +60,9 @@ val add_program = Graph.fold (add_stmt o fst o snd) fun rewrite_modulo thy some_ss program = Simplifier.full_rewrite - (add_program program (Simplifier.global_context thy - (the_default (Simpset.get thy) some_ss))); + (add_program program (simpset_default thy some_ss)); + +fun conclude_tac thy some_ss = Simplifier.full_simp_tac (simpset_default thy some_ss); (* evaluation with current code context *) @@ -67,12 +70,12 @@ fun current_conv thy = no_frees_conv (Code_Thingol.eval_conv thy (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program)); -fun current_tac thy = CONVERSION (current_conv thy); +fun current_tac thy = CONVERSION (current_conv thy) THEN' conclude_tac thy NONE; -fun current_value thy = snd o Logic.dest_equals o Thm.prop_of o current_conv thy o Thm.cterm_of thy +fun current_value thy = snd o Logic.dest_equals o Thm.prop_of o current_conv thy o Thm.cterm_of thy; val setup = Method.setup (Binding.name "code_simp") - (Scan.succeed (SIMPLE_METHOD' o current_tac o ProofContext.theory_of)) + (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo current_tac o ProofContext.theory_of))) "simplification with code equations" #> Value.add_evaluator ("simp", current_value o ProofContext.theory_of); @@ -82,6 +85,7 @@ fun make_conv thy some_ss consts = no_frees_conv (Code_Preproc.pre_post_conv thy ((rewrite_modulo thy some_ss o snd o snd o Code_Thingol.consts_program thy false) consts)); -fun make_tac thy some_ss consts = CONVERSION (make_conv thy some_ss consts); +fun make_tac thy some_ss consts = CONVERSION (make_conv thy some_ss consts) + THEN' conclude_tac thy some_ss; end;