--- 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.
--- 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}
--- 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]
--- 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
--- 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 \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> '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 (\<lambda>y. bind (f y) g)"
+by (cases x) auto
+
+lemma bind_rzero[simp]: "bind x (\<lambda>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) \<longleftrightarrow> False"
unfolding is_none_def by simp_all
-lemma is_none_none:
- "is_none x \<longleftrightarrow> x = None"
- by (simp add: is_none_def)
-
lemma [code_unfold]:
"HOL.equal x None \<longleftrightarrow> is_none x"
- by (simp add: equal is_none_none)
+ by (simp add: equal is_none_def)
hide_const (open) is_none
--- 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);
--- 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 "\<And>y. cont (\<lambda>x. g x y)"
+ shows "cont (\<lambda>x. let y = t in g x y)"
+unfolding Let_def using assms .
+
end
--- 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 \
--- 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
--- /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 \<sqsubseteq> ys \<longleftrightarrow> list_all2 (op \<sqsubseteq>) xs ys"
+
+instance proof
+ fix xs :: "'a list"
+ from below_refl show "xs \<sqsubseteq> xs"
+ unfolding below_list_def
+ by (rule list_all2_refl)
+next
+ fix xs ys zs :: "'a list"
+ assume "xs \<sqsubseteq> ys" and "ys \<sqsubseteq> zs"
+ with below_trans show "xs \<sqsubseteq> zs"
+ unfolding below_list_def
+ by (rule list_all2_trans)
+next
+ fix xs ys zs :: "'a list"
+ assume "xs \<sqsubseteq> ys" and "ys \<sqsubseteq> xs"
+ with below_antisym show "xs = ys"
+ unfolding below_list_def
+ by (rule list_all2_antisym)
+qed
+
+end
+
+lemma below_list_simps [simp]:
+ "[] \<sqsubseteq> []"
+ "x # xs \<sqsubseteq> y # ys \<longleftrightarrow> x \<sqsubseteq> y \<and> xs \<sqsubseteq> ys"
+ "\<not> [] \<sqsubseteq> y # ys"
+ "\<not> x # xs \<sqsubseteq> []"
+by (simp_all add: below_list_def)
+
+lemma Nil_below_iff [simp]: "[] \<sqsubseteq> xs \<longleftrightarrow> xs = []"
+by (cases xs, simp_all)
+
+lemma below_Nil_iff [simp]: "xs \<sqsubseteq> [] \<longleftrightarrow> xs = []"
+by (cases xs, simp_all)
+
+text "Thanks to Joachim Breitner"
+
+lemma list_Cons_below:
+ assumes "a # as \<sqsubseteq> xs"
+ obtains b and bs where "a \<sqsubseteq> b" and "as \<sqsubseteq> bs" and "xs = b # bs"
+ using assms by (cases xs, auto)
+
+lemma list_below_Cons:
+ assumes "xs \<sqsubseteq> b # bs"
+ obtains a and as where "a \<sqsubseteq> b" and "as \<sqsubseteq> bs" and "xs = a # as"
+ using assms by (cases xs, auto)
+
+lemma hd_mono: "xs \<sqsubseteq> ys \<Longrightarrow> hd xs \<sqsubseteq> hd ys"
+by (cases xs, simp, cases ys, simp, simp)
+
+lemma tl_mono: "xs \<sqsubseteq> ys \<Longrightarrow> tl xs \<sqsubseteq> tl ys"
+by (cases xs, simp, cases ys, simp, simp)
+
+lemma ch2ch_hd [simp]: "chain (\<lambda>i. S i) \<Longrightarrow> chain (\<lambda>i. hd (S i))"
+by (rule chainI, rule hd_mono, erule chainE)
+
+lemma ch2ch_tl [simp]: "chain (\<lambda>i. S i) \<Longrightarrow> chain (\<lambda>i. tl (S i))"
+by (rule chainI, rule tl_mono, erule chainE)
+
+lemma below_same_length: "xs \<sqsubseteq> ys \<Longrightarrow> length xs = length ys"
+unfolding below_list_def by (rule list_all2_lengthD)
+
+lemma list_chain_cases:
+ assumes S: "chain S"
+ obtains "\<forall>i. S i = []" |
+ A B where "chain A" and "chain B" and "\<forall>i. S i = A i # B i"
+proof (cases "S 0")
+ case Nil
+ have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF S])
+ with Nil have "\<forall>i. S i = []" by simp
+ thus ?thesis ..
+next
+ case (Cons x xs)
+ have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF S])
+ hence *: "\<forall>i. S i \<noteq> []" by (rule all_forward) (auto simp add: Cons)
+ let ?A = "\<lambda>i. hd (S i)"
+ let ?B = "\<lambda>i. tl (S i)"
+ from S have "chain ?A" and "chain ?B" by simp_all
+ moreover have "\<forall>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 (\<lambda>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 \<Rightarrow> 'a::cpo list"
+ assumes "chain S" and "\<forall>i. length (S i) = n"
+ shows "\<exists>x. range S <<| x"
+using assms
+ apply (induct n arbitrary: S)
+ apply (subgoal_tac "S = (\<lambda>i. [])")
+ apply (fast intro: lub_const)
+ apply (simp add: expand_fun_eq)
+ apply (drule_tac x="\<lambda>i. tl (S i)" in meta_spec, clarsimp)
+ apply (rule_tac x="(\<Squnion>i. hd (S i)) # x" in exI)
+ apply (subgoal_tac "range (\<lambda>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="\<lambda>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 \<Rightarrow> 'a list"
+ assume "chain S"
+ hence "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono)
+ hence "\<forall>i. length (S i) = length (S 0)"
+ by (fast intro: below_same_length [symmetric])
+ with `chain S` show "\<exists>x. range S <<| x"
+ by (rule list_cpo_lemma)
+qed
+
+subsection {* Continuity of list operations *}
+
+lemma cont2cont_Cons [simp, cont2cont]:
+ assumes f: "cont (\<lambda>x. f x)"
+ assumes g: "cont (\<lambda>x. g x)"
+ shows "cont (\<lambda>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 \<Rightarrow> 'a::cpo"
+ assumes A: "chain A" and B: "chain B"
+ shows "(\<Squnion>i. A i # B i) = (\<Squnion>i. A i) # (\<Squnion>i. B i)"
+by (intro thelubI is_lub_Cons cpo_lubI A B)
+
+lemma cont2cont_list_case:
+ assumes f: "cont (\<lambda>x. f x)"
+ assumes g: "cont (\<lambda>x. g x)"
+ assumes h1: "\<And>y ys. cont (\<lambda>x. h x y ys)"
+ assumes h2: "\<And>x ys. cont (\<lambda>y. h x y ys)"
+ assumes h3: "\<And>x y. cont (\<lambda>ys. h x y ys)"
+ shows "cont (\<lambda>x. case f x of [] \<Rightarrow> g x | y # ys \<Rightarrow> 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 (\<lambda>x. f x)"
+ assumes g: "cont (\<lambda>x. g x)"
+ assumes h: "cont (\<lambda>p. h (fst p) (fst (snd p)) (snd (snd p)))"
+ shows "cont (\<lambda>x. case f x of [] \<Rightarrow> g x | y # ys \<Rightarrow> h x y ys)"
+proof -
+ have "\<And>y ys. cont (\<lambda>x. h x (fst (y, ys)) (snd (y, ys)))"
+ by (rule h [THEN cont_fst_snd_D1])
+ hence h1: "\<And>y ys. cont (\<lambda>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 (\<lambda>x. f1 x)"
+ assumes "\<And>y ys. cont (\<lambda>x. f2 x y ys)"
+ shows "cont (\<lambda>x. case l of [] \<Rightarrow> f1 x | y # ys \<Rightarrow> 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
--- 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: "\<And>x b. cont (\<lambda>a. f x a b)"
assumes f3: "\<And>x a. cont (\<lambda>b. f x a b)"
assumes g: "cont (\<lambda>x. g x)"
- shows "cont (\<lambda>x. split (\<lambda>a b. f x a b) (g x))"
+ shows "cont (\<lambda>x. case g x of (a, b) \<Rightarrow> 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 "\<And>a b. cont (\<lambda>x. f x a b)"
+ shows "cont (\<lambda>x. case p of (a, b) \<Rightarrow> f x a b)"
+using assms by (cases p) auto
+
subsection {* Compactness and chain-finiteness *}
lemma fst_below_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"
--- 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
--- 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
--- 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
--- 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
--- 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 =