# HG changeset patch # User wenzelm # Date 1283769525 -7200 # Node ID 14b16b380ca18c5535eb9cd811e2635d65a0b885 # Parent b1c2c03fd9d702a3f9640258dde2578d6abe726e# Parent 8a2fb4ce1f3907d0fed63b4ad74a073ec65560dd merged; diff -r 8a2fb4ce1f39 -r 14b16b380ca1 NEWS --- a/NEWS Mon Sep 06 00:08:47 2010 +0200 +++ b/NEWS Mon Sep 06 12:38:45 2010 +0200 @@ -169,6 +169,9 @@ (class eq) carry proper names and are treated as default code equations. +* Removed lemma Option.is_none_none (Duplicate of is_none_def). +INCOMPATIBILITY. + * List.thy: use various operations from the Haskell prelude when generating Haskell code. diff -r 8a2fb4ce1f39 -r 14b16b380ca1 doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Mon Sep 06 00:08:47 2010 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Mon Sep 06 12:38:45 2010 +0200 @@ -159,7 +159,16 @@ \S\ref{first-steps}. Remote ATP invocation via the SystemOnTPTP web service requires Perl with the -World Wide Web Library (\texttt{libwww-perl}) installed. +World Wide Web Library (\texttt{libwww-perl}) installed. If you must use a proxy +server to access the Internet, set the \texttt{http\_proxy} environment variable +to the proxy, either in the environment in which Isabelle is launched or in your +\texttt{\char`\~/.isabelle/etc/settings} file. Here are a few examples: + +\prew +\texttt{http\_proxy=http://proxy.example.org} \\ +\texttt{http\_proxy=http://proxy.example.org:8080} \\ +\texttt{http\_proxy=http://joeblow:pAsSwRd@proxy.example.org} +\postw \section{First Steps} \label{first-steps} diff -r 8a2fb4ce1f39 -r 14b16b380ca1 src/HOL/Library/Executable_Set.thy --- a/src/HOL/Library/Executable_Set.thy Mon Sep 06 00:08:47 2010 +0200 +++ b/src/HOL/Library/Executable_Set.thy Mon Sep 06 12:38:45 2010 +0200 @@ -9,6 +9,12 @@ imports More_Set begin +text {* + This is just an ad-hoc hack which will rarely give you what you want. + For the moment, whenever you need executable sets, consider using + type @{text fset} from theory @{text Fset}. +*} + declare mem_def [code del] declare Collect_def [code del] declare insert_code [code del] diff -r 8a2fb4ce1f39 -r 14b16b380ca1 src/HOL/Library/Monad_Syntax.thy --- a/src/HOL/Library/Monad_Syntax.thy Mon Sep 06 00:08:47 2010 +0200 +++ b/src/HOL/Library/Monad_Syntax.thy Mon Sep 06 12:38:45 2010 +0200 @@ -73,6 +73,7 @@ setup {* Adhoc_Overloading.add_overloaded @{const_name bind} #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Predicate.bind} + #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Option.bind} *} end diff -r 8a2fb4ce1f39 -r 14b16b380ca1 src/HOL/Option.thy --- a/src/HOL/Option.thy Mon Sep 06 00:08:47 2010 +0200 +++ b/src/HOL/Option.thy Mon Sep 06 12:38:45 2010 +0200 @@ -81,8 +81,20 @@ "map f o sum_case g h = sum_case (map f o g) (map f o h)" by (rule ext) (simp split: sum.split) +primrec bind :: "'a option \ ('a \ 'b option) \ 'b option" where +bind_lzero: "bind None f = None" | +bind_lunit: "bind (Some x) f = f x" -hide_const (open) set map +lemma bind_runit[simp]: "bind x Some = x" +by (cases x) auto + +lemma bind_assoc[simp]: "bind (bind x f) g = bind x (\y. bind (f y) g)" +by (cases x) auto + +lemma bind_rzero[simp]: "bind x (\x. None) = None" +by (cases x) auto + +hide_const (open) set map bind subsubsection {* Code generator setup *} @@ -94,13 +106,9 @@ and "is_none (Some x) \ False" unfolding is_none_def by simp_all -lemma is_none_none: - "is_none x \ x = None" - by (simp add: is_none_def) - lemma [code_unfold]: "HOL.equal x None \ is_none x" - by (simp add: equal is_none_none) + by (simp add: equal is_none_def) hide_const (open) is_none diff -r 8a2fb4ce1f39 -r 14b16b380ca1 src/HOL/Tools/ATP/scripts/remote_atp --- a/src/HOL/Tools/ATP/scripts/remote_atp Mon Sep 06 00:08:47 2010 +0200 +++ b/src/HOL/Tools/ATP/scripts/remote_atp Mon Sep 06 12:38:45 2010 +0200 @@ -86,6 +86,7 @@ # Query Server my $Agent = LWP::UserAgent->new; +$Agent->env_proxy; if (exists($Options{'t'})) { # give server more time to respond $Agent->timeout($Options{'t'} + 10); diff -r 8a2fb4ce1f39 -r 14b16b380ca1 src/HOLCF/Cfun.thy --- a/src/HOLCF/Cfun.thy Mon Sep 06 00:08:47 2010 +0200 +++ b/src/HOLCF/Cfun.thy Mon Sep 06 12:38:45 2010 +0200 @@ -597,4 +597,12 @@ using g by (rule cont_fst_snd_D1) qed +text {* The simple version (suggested by Joachim Breitner) is needed if + the type of the defined term is not a cpo. *} + +lemma cont2cont_Let_simple [simp, cont2cont]: + assumes "\y. cont (\x. g x y)" + shows "cont (\x. let y = t in g x y)" +unfolding Let_def using assms . + end diff -r 8a2fb4ce1f39 -r 14b16b380ca1 src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Mon Sep 06 00:08:47 2010 +0200 +++ b/src/HOLCF/IsaMakefile Mon Sep 06 12:38:45 2010 +0200 @@ -103,6 +103,7 @@ HOLCF-Library: HOLCF $(LOG)/HOLCF-Library.gz $(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \ + Library/List_Cpo.thy \ Library/Stream.thy \ Library/Strict_Fun.thy \ Library/Sum_Cpo.thy \ diff -r 8a2fb4ce1f39 -r 14b16b380ca1 src/HOLCF/Library/HOLCF_Library.thy --- a/src/HOLCF/Library/HOLCF_Library.thy Mon Sep 06 00:08:47 2010 +0200 +++ b/src/HOLCF/Library/HOLCF_Library.thy Mon Sep 06 12:38:45 2010 +0200 @@ -1,5 +1,6 @@ theory HOLCF_Library imports + List_Cpo Stream Strict_Fun Sum_Cpo diff -r 8a2fb4ce1f39 -r 14b16b380ca1 src/HOLCF/Library/List_Cpo.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Library/List_Cpo.thy Mon Sep 06 12:38:45 2010 +0200 @@ -0,0 +1,210 @@ +(* Title: HOLCF/Library/List_Cpo.thy + Author: Brian Huffman +*) + +header {* Lists as a complete partial order *} + +theory List_Cpo +imports HOLCF +begin + +subsection {* Lists are a partial order *} + +instantiation list :: (po) po +begin + +definition + "xs \ ys \ list_all2 (op \) xs ys" + +instance proof + fix xs :: "'a list" + from below_refl show "xs \ xs" + unfolding below_list_def + by (rule list_all2_refl) +next + fix xs ys zs :: "'a list" + assume "xs \ ys" and "ys \ zs" + with below_trans show "xs \ zs" + unfolding below_list_def + by (rule list_all2_trans) +next + fix xs ys zs :: "'a list" + assume "xs \ ys" and "ys \ xs" + with below_antisym show "xs = ys" + unfolding below_list_def + by (rule list_all2_antisym) +qed + +end + +lemma below_list_simps [simp]: + "[] \ []" + "x # xs \ y # ys \ x \ y \ xs \ ys" + "\ [] \ y # ys" + "\ x # xs \ []" +by (simp_all add: below_list_def) + +lemma Nil_below_iff [simp]: "[] \ xs \ xs = []" +by (cases xs, simp_all) + +lemma below_Nil_iff [simp]: "xs \ [] \ xs = []" +by (cases xs, simp_all) + +text "Thanks to Joachim Breitner" + +lemma list_Cons_below: + assumes "a # as \ xs" + obtains b and bs where "a \ b" and "as \ bs" and "xs = b # bs" + using assms by (cases xs, auto) + +lemma list_below_Cons: + assumes "xs \ b # bs" + obtains a and as where "a \ b" and "as \ bs" and "xs = a # as" + using assms by (cases xs, auto) + +lemma hd_mono: "xs \ ys \ hd xs \ hd ys" +by (cases xs, simp, cases ys, simp, simp) + +lemma tl_mono: "xs \ ys \ tl xs \ tl ys" +by (cases xs, simp, cases ys, simp, simp) + +lemma ch2ch_hd [simp]: "chain (\i. S i) \ chain (\i. hd (S i))" +by (rule chainI, rule hd_mono, erule chainE) + +lemma ch2ch_tl [simp]: "chain (\i. S i) \ chain (\i. tl (S i))" +by (rule chainI, rule tl_mono, erule chainE) + +lemma below_same_length: "xs \ ys \ length xs = length ys" +unfolding below_list_def by (rule list_all2_lengthD) + +lemma list_chain_cases: + assumes S: "chain S" + obtains "\i. S i = []" | + A B where "chain A" and "chain B" and "\i. S i = A i # B i" +proof (cases "S 0") + case Nil + have "\i. S 0 \ S i" by (simp add: chain_mono [OF S]) + with Nil have "\i. S i = []" by simp + thus ?thesis .. +next + case (Cons x xs) + have "\i. S 0 \ S i" by (simp add: chain_mono [OF S]) + hence *: "\i. S i \ []" by (rule all_forward) (auto simp add: Cons) + let ?A = "\i. hd (S i)" + let ?B = "\i. tl (S i)" + from S have "chain ?A" and "chain ?B" by simp_all + moreover have "\i. S i = ?A i # ?B i" by (simp add: *) + ultimately show ?thesis .. +qed + +subsection {* Lists are a complete partial order *} + +lemma is_lub_Cons: + assumes A: "range A <<| x" + assumes B: "range B <<| xs" + shows "range (\i. A i # B i) <<| x # xs" +using assms +unfolding is_lub_def is_ub_def Ball_def [symmetric] +by (clarsimp, case_tac u, simp_all) + +lemma list_cpo_lemma: + fixes S :: "nat \ 'a::cpo list" + assumes "chain S" and "\i. length (S i) = n" + shows "\x. range S <<| x" +using assms + apply (induct n arbitrary: S) + apply (subgoal_tac "S = (\i. [])") + apply (fast intro: lub_const) + apply (simp add: expand_fun_eq) + apply (drule_tac x="\i. tl (S i)" in meta_spec, clarsimp) + apply (rule_tac x="(\i. hd (S i)) # x" in exI) + apply (subgoal_tac "range (\i. hd (S i) # tl (S i)) = range S") + apply (erule subst) + apply (rule is_lub_Cons) + apply (rule thelubE [OF _ refl]) + apply (erule ch2ch_hd) + apply assumption + apply (rule_tac f="\S. range S" in arg_cong) + apply (rule ext) + apply (rule hd_Cons_tl) + apply (drule_tac x=i in spec, auto) +done + +instance list :: (cpo) cpo +proof + fix S :: "nat \ 'a list" + assume "chain S" + hence "\i. S 0 \ S i" by (simp add: chain_mono) + hence "\i. length (S i) = length (S 0)" + by (fast intro: below_same_length [symmetric]) + with `chain S` show "\x. range S <<| x" + by (rule list_cpo_lemma) +qed + +subsection {* Continuity of list operations *} + +lemma cont2cont_Cons [simp, cont2cont]: + assumes f: "cont (\x. f x)" + assumes g: "cont (\x. g x)" + shows "cont (\x. f x # g x)" +apply (rule contI) +apply (rule is_lub_Cons) +apply (erule contE [OF f]) +apply (erule contE [OF g]) +done + +lemma lub_Cons: + fixes A :: "nat \ 'a::cpo" + assumes A: "chain A" and B: "chain B" + shows "(\i. A i # B i) = (\i. A i) # (\i. B i)" +by (intro thelubI is_lub_Cons cpo_lubI A B) + +lemma cont2cont_list_case: + assumes f: "cont (\x. f x)" + assumes g: "cont (\x. g x)" + assumes h1: "\y ys. cont (\x. h x y ys)" + assumes h2: "\x ys. cont (\y. h x y ys)" + assumes h3: "\x y. cont (\ys. h x y ys)" + shows "cont (\x. case f x of [] \ g x | y # ys \ h x y ys)" +apply (rule cont_apply [OF f]) +apply (rule contI) +apply (erule list_chain_cases) +apply (simp add: lub_const) +apply (simp add: lub_Cons) +apply (simp add: cont2contlubE [OF h2]) +apply (simp add: cont2contlubE [OF h3]) +apply (simp add: diag_lub ch2ch_cont [OF h2] ch2ch_cont [OF h3]) +apply (rule cpo_lubI, rule chainI, rule below_trans) +apply (erule cont2monofunE [OF h2 chainE]) +apply (erule cont2monofunE [OF h3 chainE]) +apply (case_tac y, simp_all add: g h1) +done + +lemma cont2cont_list_case' [simp, cont2cont]: + assumes f: "cont (\x. f x)" + assumes g: "cont (\x. g x)" + assumes h: "cont (\p. h (fst p) (fst (snd p)) (snd (snd p)))" + shows "cont (\x. case f x of [] \ g x | y # ys \ h x y ys)" +proof - + have "\y ys. cont (\x. h x (fst (y, ys)) (snd (y, ys)))" + by (rule h [THEN cont_fst_snd_D1]) + hence h1: "\y ys. cont (\x. h x y ys)" by simp + note h2 = h [THEN cont_fst_snd_D2, THEN cont_fst_snd_D1] + note h3 = h [THEN cont_fst_snd_D2, THEN cont_fst_snd_D2] + from f g h1 h2 h3 show ?thesis by (rule cont2cont_list_case) +qed + +text {* The simple version (due to Joachim Breitner) is needed if the + element type of the list is not a cpo. *} + +lemma cont2cont_list_case_simple [simp, cont2cont]: + assumes "cont (\x. f1 x)" + assumes "\y ys. cont (\x. f2 x y ys)" + shows "cont (\x. case l of [] \ f1 x | y # ys \ f2 x y ys)" +using assms by (cases l) auto + +text {* There are probably lots of other list operations that also +deserve to have continuity lemmas. I'll add more as they are +needed. *} + +end diff -r 8a2fb4ce1f39 -r 14b16b380ca1 src/HOLCF/Product_Cpo.thy --- a/src/HOLCF/Product_Cpo.thy Mon Sep 06 00:08:47 2010 +0200 +++ b/src/HOLCF/Product_Cpo.thy Mon Sep 06 12:38:45 2010 +0200 @@ -239,7 +239,7 @@ assumes f2: "\x b. cont (\a. f x a b)" assumes f3: "\x a. cont (\b. f x a b)" assumes g: "cont (\x. g x)" - shows "cont (\x. split (\a b. f x a b) (g x))" + shows "cont (\x. case g x of (a, b) \ f x a b)" unfolding split_def apply (rule cont_apply [OF g]) apply (rule cont_apply [OF cont_fst f2]) @@ -274,6 +274,14 @@ done qed +text {* The simple version (due to Joachim Breitner) is needed if + either element type of the pair is not a cpo. *} + +lemma cont2cont_split_simple [simp, cont2cont]: + assumes "\a b. cont (\x. f x a b)" + shows "cont (\x. case p of (a, b) \ f x a b)" +using assms by (cases p) auto + subsection {* Compactness and chain-finiteness *} lemma fst_below_iff: "fst (x::'a \ 'b) \ y \ x \ (y, snd x)" diff -r 8a2fb4ce1f39 -r 14b16b380ca1 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Mon Sep 06 00:08:47 2010 +0200 +++ b/src/Tools/Code/code_haskell.ML Mon Sep 06 12:38:45 2010 +0200 @@ -331,10 +331,8 @@ handle Option => error ("Unknown statement name: " ^ labelled_name name); in (deresolver, hs_program) end; -fun serialize_haskell module_prefix string_classes { labelled_name, - reserved_syms, includes, module_alias, - class_syntax, tyco_syntax, const_syntax, program, - names } = +fun serialize_haskell module_prefix string_classes { labelled_name, reserved_syms, + includes, module_alias, class_syntax, tyco_syntax, const_syntax, program } = let val reserved = fold (insert (op =) o fst) includes reserved_syms; val (deresolver, hs_program) = haskell_program_of_program labelled_name diff -r 8a2fb4ce1f39 -r 14b16b380ca1 src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Mon Sep 06 00:08:47 2010 +0200 +++ b/src/Tools/Code/code_ml.ML Mon Sep 06 12:38:45 2010 +0200 @@ -785,31 +785,33 @@ cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program end; -fun serialize_ml target print_module print_stmt with_signatures { labelled_name, - reserved_syms, includes, module_alias, class_syntax, tyco_syntax, - const_syntax, program, names } = +fun serialize_ml target print_ml_module print_ml_stmt with_signatures + { labelled_name, reserved_syms, includes, module_alias, + class_syntax, tyco_syntax, const_syntax, program } = let - val is_cons = Code_Thingol.is_cons program; + + (* build program *) val { deresolver, hierarchical_program = ml_program } = ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program; - val print_stmt = print_stmt labelled_name tyco_syntax const_syntax - (make_vars reserved_syms) is_cons; - fun print_node _ (_, Code_Namespace.Dummy) = - NONE - | print_node prefix_fragments (name, Code_Namespace.Stmt stmt) = - SOME (apsnd (markup_stmt name) (print_stmt (deresolver prefix_fragments) stmt)) - | print_node prefix_fragments (name_fragment, Code_Namespace.Module (_, nodes)) = - let - val (decls, body) = print_nodes (prefix_fragments @ [name_fragment]) nodes; - val p = print_module name_fragment - (if with_signatures then SOME decls else NONE) body; - in SOME ([], p) end - and print_nodes prefix_fragments nodes = (map_filter - (fn name => print_node prefix_fragments (name, snd (Graph.get_node nodes name))) - o rev o flat o Graph.strong_conn) nodes - |> split_list - |> (fn (decls, body) => (flat decls, body)) - val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] ml_program)); + + (* print statements *) + fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt + labelled_name tyco_syntax const_syntax (make_vars reserved_syms) + (Code_Thingol.is_cons program) (deresolver prefix_fragments) stmt + |> apfst SOME; + + (* print modules *) + fun print_module prefix_fragments base _ xs = + let + val (raw_decls, body) = split_list xs; + val decls = if with_signatures then SOME (maps these raw_decls) else NONE + in (NONE, print_ml_module base decls body) end; + + (* serialization *) + val p = Pretty.chunks2 (map snd includes + @ map snd (Code_Namespace.print_hierarchical { + print_module = print_module, print_stmt = print_stmt, + lift_markup = apsnd } ml_program)); fun write width NONE = writeln o format [] width | write width (SOME p) = File.write p o format [] width; in diff -r 8a2fb4ce1f39 -r 14b16b380ca1 src/Tools/Code/code_namespace.ML --- a/src/Tools/Code/code_namespace.ML Mon Sep 06 00:08:47 2010 +0200 +++ b/src/Tools/Code/code_namespace.ML Mon Sep 06 12:38:45 2010 +0200 @@ -10,7 +10,8 @@ datatype ('a, 'b) node = Dummy | Stmt of 'a - | Module of ('b * (string * ('a, 'b) node) Graph.T); + | Module of ('b * (string * ('a, 'b) node) Graph.T) + type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Graph.T val hierarchical_program: (string -> string) -> { module_alias: string -> string option, reserved: Name.context, empty_nsp: 'c, namify_module: string -> 'c -> string * 'c, namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c, @@ -18,7 +19,11 @@ modify_stmts: (string * Code_Thingol.stmt) list -> 'a option list } -> Code_Thingol.program -> { deresolver: string list -> string -> string, - hierarchical_program: (string * ('a, 'b) node) Graph.T } + hierarchical_program: ('a, 'b) hierarchical_program } + val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c, + print_stmt: string list -> string * 'a -> 'c, + lift_markup: (Pretty.T -> Pretty.T) -> 'c -> 'c } + -> ('a, 'b) hierarchical_program -> 'c list end; structure Code_Namespace : CODE_NAMESPACE = @@ -37,6 +42,8 @@ | Stmt of 'a | Module of ('b * (string * ('a, 'b) node) Graph.T); +type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Graph.T; + fun map_module_content f (Module content) = Module (f content); fun map_module [] = I @@ -140,4 +147,25 @@ in { deresolver = deresolver, hierarchical_program = hierarchical_program } end; +fun print_hierarchical { print_module, print_stmt, lift_markup } = + let + fun print_node _ (_, Dummy) = + NONE + | print_node prefix_fragments (name, Stmt stmt) = + SOME (lift_markup (Code_Printer.markup_stmt name) + (print_stmt prefix_fragments (name, stmt))) + | print_node prefix_fragments (name_fragment, Module (data, nodes)) = + let + val prefix_fragments' = prefix_fragments @ [name_fragment] + in + Option.map (print_module prefix_fragments' + name_fragment data) (print_nodes prefix_fragments' nodes) + end + and print_nodes prefix_fragments nodes = + let + val xs = (map_filter (fn name => print_node prefix_fragments + (name, snd (Graph.get_node nodes name))) o rev o flat o Graph.strong_conn) nodes + in if null xs then NONE else SOME xs end; + in these o print_nodes [] end; + end; \ No newline at end of file diff -r 8a2fb4ce1f39 -r 14b16b380ca1 src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Mon Sep 06 00:08:47 2010 +0200 +++ b/src/Tools/Code/code_scala.ML Mon Sep 06 12:38:45 2010 +0200 @@ -329,12 +329,11 @@ end; fun serialize_scala { labelled_name, reserved_syms, includes, - module_alias, class_syntax, tyco_syntax, const_syntax, program, - names } = + module_alias, class_syntax, tyco_syntax, const_syntax, program } = let (* build program *) - val { deresolver, hierarchical_program = sca_program } = + val { deresolver, hierarchical_program = scala_program } = scala_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program; (* print statements *) @@ -354,38 +353,27 @@ fun is_singleton_constr c = case Graph.get_node program c of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c) | _ => false; - val print_stmt = print_scala_stmt labelled_name tyco_syntax const_syntax - (make_vars reserved_syms) args_num is_singleton_constr; + fun print_stmt prefix_fragments = print_scala_stmt labelled_name + tyco_syntax const_syntax (make_vars reserved_syms) args_num + is_singleton_constr (deresolver prefix_fragments, deresolver []); - (* print nodes *) - fun print_module base implicit_ps p = Pretty.chunks2 - ([str ("object " ^ base ^ " {")] - @ (if null implicit_ps then [] else (single o Pretty.block) - (str "import /*implicits*/" :: Pretty.brk 1 :: commas implicit_ps)) - @ [p, str ("} /* object " ^ base ^ " */")]); + (* print modules *) fun print_implicit prefix_fragments implicit = let val s = deresolver prefix_fragments implicit; in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end; - fun print_node _ (_, Code_Namespace.Dummy) = NONE - | print_node prefix_fragments (name, Code_Namespace.Stmt stmt) = - SOME (markup_stmt name (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt))) - | print_node prefix_fragments (name_fragment, Code_Namespace.Module (implicits, nodes)) = - let - val prefix_fragments' = prefix_fragments @ [name_fragment]; - in - Option.map (print_module name_fragment - (map_filter (print_implicit prefix_fragments') implicits)) - (print_nodes prefix_fragments' nodes) - end - and print_nodes prefix_fragments nodes = let - val ps = map_filter (fn name => print_node prefix_fragments (name, - snd (Graph.get_node nodes name))) - ((rev o flat o Graph.strong_conn) nodes); - in if null ps then NONE else SOME (Pretty.chunks2 ps) end; + fun print_module prefix_fragments base implicits ps = Pretty.chunks2 + ([str ("object " ^ base ^ " {")] + @ (case map_filter (print_implicit prefix_fragments) implicits + of [] => [] | implicit_ps => (single o Pretty.block) + (str "import /*implicits*/" :: Pretty.brk 1 :: commas implicit_ps)) + @ ps @ [str ("} /* object " ^ base ^ " */")]); (* serialization *) - val p = Pretty.chunks2 (map snd includes @ the_list (print_nodes [] sca_program)); + val p = Pretty.chunks2 (map snd includes + @ Code_Namespace.print_hierarchical { + print_module = print_module, print_stmt = print_stmt, + lift_markup = I } scala_program); fun write width NONE = writeln o format [] width | write width (SOME p) = File.write p o format [] width; in diff -r 8a2fb4ce1f39 -r 14b16b380ca1 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Mon Sep 06 00:08:47 2010 +0200 +++ b/src/Tools/Code/code_target.ML Mon Sep 06 12:38:45 2010 +0200 @@ -105,7 +105,8 @@ Symtab.join (K snd) (const1, const2)) ); -type serializer = Token.T list (*arguments*) -> { +type serializer = Token.T list + -> { labelled_name: string -> string, reserved_syms: string list, includes: (string * Pretty.T) list, @@ -113,8 +114,7 @@ class_syntax: string -> string option, tyco_syntax: string -> Code_Printer.tyco_syntax option, const_syntax: string -> Code_Printer.activated_const_syntax option, - program: Code_Thingol.program, - names: string list } + program: Code_Thingol.program } -> serialization; datatype description = Fundamental of { serializer: serializer, @@ -321,8 +321,7 @@ class_syntax = Symtab.lookup class_syntax, tyco_syntax = Symtab.lookup tyco_syntax, const_syntax = Symtab.lookup const_syntax, - program = program, - names = names } + program = program } end; fun mount_serializer thy target some_width module_name args naming proto_program names =