--- a/src/Tools/Code/code_haskell.ML Sun Feb 23 10:33:43 2014 +0100
+++ b/src/Tools/Code/code_haskell.ML Sun Feb 23 10:33:43 2014 +0100
@@ -355,13 +355,19 @@
deresolve (if string_classes then deriving_show else K false);
(* print modules *)
- fun print_module_frame module_name ps =
+ fun print_module_frame module_name exports ps =
(module_name, Pretty.chunks2 (
- str ("module " ^ module_name ^ " where {")
+ concat [str "module",
+ case exports of
+ SOME ps => Pretty.block [str module_name, enclose "(" ")" (commas ps)]
+ | NONE => str module_name,
+ str "where {"
+ ]
:: ps
@| str "}"
));
- fun print_qualified_import module_name = semicolon [str "import qualified", str module_name];
+ fun print_qualified_import module_name =
+ semicolon [str "import qualified", str module_name];
val import_common_ps =
enclose "import Prelude (" ");" (commas (map str
(map (Library.enclose "(" ")") prelude_import_operators @ prelude_import_unqualified)
@@ -371,14 +377,23 @@
fun print_module module_name (gr, imports) =
let
val deresolve = deresolver module_name;
- fun print_import module_name = (semicolon o map str) ["import qualified", module_name];
+ val deresolve_import = SOME o str o deresolve;
+ val deresolve_import_attached = SOME o str o suffix "(..)" o deresolve;
+ fun print_import (sym, Code_Thingol.Fun _) = deresolve_import sym
+ | print_import (sym, Code_Thingol.Datatype _) = deresolve_import_attached sym
+ | print_import (sym, Code_Thingol.Class _) = deresolve_import_attached sym
+ | print_import (sym, Code_Thingol.Classinst _) = NONE;
val import_ps = import_common_ps @ map (print_qualified_import o fst) imports;
fun print_stmt' sym = case Code_Symbol.Graph.get_node gr sym
of (_, NONE) => NONE
- | (_, SOME stmt) => SOME (markup_stmt sym (print_stmt deresolve (sym, stmt)));
- val body_ps = map_filter print_stmt' ((flat o rev o Code_Symbol.Graph.strong_conn) gr);
+ | (_, SOME (export, stmt)) =>
+ SOME (if export then print_import (sym, stmt) else NONE, markup_stmt sym (print_stmt deresolve (sym, stmt)));
+ val (export_ps, body_ps) = (flat o rev o Code_Symbol.Graph.strong_conn) gr
+ |> map_filter print_stmt'
+ |> split_list
+ |> apfst (map_filter I);
in
- print_module_frame module_name
+ print_module_frame module_name (SOME export_ps)
((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps)
end;
@@ -399,7 +414,7 @@
(fn width => fn destination => K () o map (write_module width destination))
(fn present => fn width => rpair (try (deresolver ""))
o (map o apsnd) (format present width))
- (map (uncurry print_module_frame o apsnd single) includes
+ (map (fn (module_name, content) => print_module_frame module_name NONE [content]) includes
@ map (fn module_name => print_module module_name (Graph.get_node haskell_program module_name))
((flat o rev o Graph.strong_conn) haskell_program))
end;
--- a/src/Tools/Code/code_ml.ML Sun Feb 23 10:33:43 2014 +0100
+++ b/src/Tools/Code/code_ml.ML Sun Feb 23 10:33:43 2014 +0100
@@ -795,10 +795,10 @@
ml_program_of_program ctxt module_name (Name.make_context reserved_syms) identifiers program;
(* print statements *)
- fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt
+ fun print_stmt prefix_fragments (_, (export, stmt)) = print_ml_stmt
tyco_syntax const_syntax (make_vars reserved_syms)
(Code_Thingol.is_constr program) (deresolver prefix_fragments) stmt
- |> apfst SOME;
+ |> apfst (fn decl => if export then SOME decl else NONE);
(* print modules *)
fun print_module _ base _ xs =
--- a/src/Tools/Code/code_namespace.ML Sun Feb 23 10:33:43 2014 +0100
+++ b/src/Tools/Code/code_namespace.ML Sun Feb 23 10:33:43 2014 +0100
@@ -18,7 +18,7 @@
datatype ('a, 'b) node =
Dummy
- | Stmt of 'a
+ | Stmt of bool * 'a
| Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T)
type ('a, 'b) hierarchical_program
val hierarchical_program: Proof.context
@@ -32,7 +32,7 @@
-> { deresolver: string list -> Code_Symbol.T -> string,
hierarchical_program: ('a, 'b) hierarchical_program }
val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c,
- print_stmt: string list -> Code_Symbol.T * 'a -> 'c,
+ print_stmt: string list -> Code_Symbol.T * (bool * 'a) -> 'c,
lift_markup: (Pretty.T -> Pretty.T) -> 'c -> 'c }
-> ('a, 'b) hierarchical_program -> 'c list
end;
@@ -82,7 +82,7 @@
(** flat program structure **)
-type flat_program = ((string * Code_Thingol.stmt option) Code_Symbol.Graph.T * (string * Code_Symbol.T list) list) Graph.T;
+type flat_program = ((string * (bool * Code_Thingol.stmt) option) Code_Symbol.Graph.T * (string * Code_Symbol.T list) list) Graph.T;
fun flat_program ctxt { module_prefix, module_name, reserved,
identifiers, empty_nsp, namify_stmt, modify_stmt } program =
@@ -102,7 +102,7 @@
val (module_name, base) = prep_sym sym;
in
Graph.default_node (module_name, (Code_Symbol.Graph.empty, []))
- #> (Graph.map_node module_name o apfst) (Code_Symbol.Graph.new_node (sym, (base, stmt)))
+ #> (Graph.map_node module_name o apfst) (Code_Symbol.Graph.new_node (sym, (base, (true, stmt))))
end;
fun add_dep sym sym' =
let
@@ -116,7 +116,7 @@
{ empty = Graph.empty, add_stmt = add_stmt, add_dep = add_dep } program;
(* name declarations and statement modifications *)
- fun declare sym (base, stmt) (gr, nsp) =
+ fun declare sym (base, (_, stmt)) (gr, nsp) =
let
val (base', nsp') = namify_stmt stmt base nsp;
val gr' = (Code_Symbol.Graph.map_node sym o apfst) (K base') gr;
@@ -125,7 +125,8 @@
|> fold (fn sym => declare sym (Code_Symbol.Graph.get_node gr sym))
(prioritize sym_priority (Code_Symbol.Graph.keys gr))
|> fst
- |> (Code_Symbol.Graph.map o K o apsnd) modify_stmt;
+ |> (Code_Symbol.Graph.map o K o apsnd)
+ (fn (export, stmt) => Option.map (pair export) (modify_stmt stmt));
val flat_program = proto_program
|> (Graph.map o K o apfst) declarations;
@@ -162,11 +163,13 @@
datatype ('a, 'b) node =
Dummy
- | Stmt of 'a
+ | Stmt of bool * 'a
| Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T);
type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Code_Symbol.Graph.T;
+fun the_stmt (Stmt (export, stmt)) = (export, stmt);
+
fun map_module_content f (Module content) = Module (f content);
fun map_module [] = I
@@ -206,7 +209,7 @@
let
val (name_fragments, base) = prep_sym sym;
in
- (map_module name_fragments o apsnd) (Code_Symbol.Graph.new_node (sym, (base, Stmt stmt)))
+ (map_module name_fragments o apsnd) (Code_Symbol.Graph.new_node (sym, (base, Stmt (true, stmt))))
end;
fun add_dep sym sym' =
let
@@ -244,18 +247,18 @@
in (nsps', nodes') end;
val (nsps', nodes') = (nsps, nodes)
|> fold (declare (K namify_module)) module_fragments
- |> fold (declare (namify_stmt o (fn Stmt stmt => stmt))) stmt_syms;
+ |> fold (declare (namify_stmt o snd o the_stmt)) stmt_syms;
fun select_syms syms = case filter (member (op =) stmt_syms) syms
of [] => NONE
| syms => SOME syms;
- fun select_stmt (sym, SOME stmt) = SOME (sym, stmt)
+ fun select_stmt (sym, (export, SOME stmt)) = SOME (sym, (export, stmt))
| select_stmt _ = NONE;
fun modify_stmts' syms =
let
- val stmts = map ((fn Stmt stmt => stmt) o snd o Code_Symbol.Graph.get_node nodes) syms;
+ val (exports, stmts) = map_split (the_stmt o snd o Code_Symbol.Graph.get_node nodes) syms;
val stmts' = modify_stmts (syms ~~ stmts);
val stmts'' = stmts' @ replicate (length syms - length stmts') NONE;
- in map_filter select_stmt (syms ~~ stmts'') end;
+ in map_filter select_stmt (syms ~~ (exports ~~ stmts'')) end;
val stmtss' = (maps modify_stmts' o map_filter select_syms o Code_Symbol.Graph.strong_conn) nodes;
val nodes'' = Code_Symbol.Graph.map (fn sym => apsnd (fn Module content => Module (make_declarations nsps' content)
| _ => case AList.lookup (op =) stmtss' sym of SOME stmt => Stmt stmt | _ => Dummy)) nodes';
--- a/src/Tools/Code/code_scala.ML Sun Feb 23 10:33:43 2014 +0100
+++ b/src/Tools/Code/code_scala.ML Sun Feb 23 10:33:43 2014 +0100
@@ -145,26 +145,28 @@
|> single
|> enclose "(" ")"
end;
+ fun privatize false = concat o cons (str "private")
+ | privatize true = concat;
fun print_context tyvars vs sym = applify "[" "]"
(fn (v, sort) => (Pretty.block o map str)
(lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class class]) sort))
NOBR ((str o deresolve) sym) vs;
- fun print_defhead tyvars vars const vs params tys ty =
- Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) =>
+ fun print_defhead export tyvars vars const vs params tys ty =
+ privatize export [str "def", constraint (applify "(" ")" (fn (param, ty) =>
constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
NOBR (print_context tyvars vs (Constant const)) (params ~~ tys)) (print_typ tyvars NOBR ty),
- str " ="];
- fun print_def const (vs, ty) [] =
+ str "="];
+ fun print_def export const (vs, ty) [] =
let
val (tys, ty') = Code_Thingol.unfold_fun ty;
val params = Name.invent (snd reserved) "a" (length tys);
val tyvars = intro_tyvars vs reserved;
val vars = intro_vars params reserved;
in
- concat [print_defhead tyvars vars const vs params tys ty',
+ concat [print_defhead export tyvars vars const vs params tys ty',
str ("sys.error(\"" ^ const ^ "\")")]
end
- | print_def const (vs, ty) eqs =
+ | print_def export const (vs, ty) eqs =
let
val tycos = fold (fn ((ts, t), _) =>
fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
@@ -196,7 +198,7 @@
tuplify (map (print_term tyvars true some_thm vars' NOBR) ts),
str "=>", print_rhs vars' eq]
end;
- val head = print_defhead tyvars vars2 const vs params tys' ty';
+ val head = print_defhead export tyvars vars2 const vs params tys' ty';
in if simple then
concat [head, print_rhs vars2 (hd eqs)]
else
@@ -206,14 +208,14 @@
(map print_clause eqs)
end;
val print_method = str o Library.enclose "`" "`" o deresolve_full o Constant;
- fun print_stmt (Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
- print_def const (vs, ty) (filter (snd o snd) raw_eqs)
- | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, cos)) =
+ fun print_stmt (Constant const, (export, Code_Thingol.Fun (((vs, ty), raw_eqs), _))) =
+ print_def export const (vs, ty) (filter (snd o snd) raw_eqs)
+ | print_stmt (Type_Constructor tyco, (export, Code_Thingol.Datatype (vs, cos))) =
let
val tyvars = intro_tyvars (map (rpair []) vs) reserved;
fun print_co ((co, vs_args), tys) =
concat [Pretty.block ((applify "[" "]" (str o lookup_tyvar tyvars) NOBR
- ((concat o map str) ["final", "case", "class", deresolve_const co]) vs_args)
+ ((privatize export o map str) ["final", "case", "class", deresolve_const co]) vs_args)
@@ enum "," "(" ")" (map (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg))
(Name.invent_names (snd reserved) "a" tys))),
str "extends",
@@ -222,10 +224,10 @@
];
in
Pretty.chunks (applify "[" "]" (str o lookup_tyvar tyvars)
- NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs
+ NOBR ((privatize export o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs
:: map print_co cos)
end
- | print_stmt (Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
+ | print_stmt (Type_Class class, (export, Code_Thingol.Class (v, (classrels, classparams)))) =
let
val tyvars = intro_tyvars [(v, [class])] reserved;
fun add_typarg s = Pretty.block
@@ -244,7 +246,7 @@
val auxs = Name.invent (snd proto_vars) "a" (length tys);
val vars = intro_vars auxs proto_vars;
in
- concat [str "def", constraint (Pretty.block [applify "(" ")"
+ privatize export [str "def", constraint (Pretty.block [applify "(" ")"
(fn (aux, ty) => constraint ((str o lookup_var vars) aux)
(print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_const classparam))
(auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
@@ -255,14 +257,14 @@
in
Pretty.chunks (
(Pretty.block_enclose
- (concat ([str "trait", (add_typarg o deresolve_class) class]
+ (privatize export ([str "trait", (add_typarg o deresolve_class) class]
@ the_list (print_super_classes classrels) @ [str "{"]), str "}")
(map print_classparam_val classparams))
:: map print_classparam_def classparams
)
end
- | print_stmt (sym, Code_Thingol.Classinst
- { class, tyco, vs, inst_params, superinst_params, ... }) =
+ | print_stmt (sym, (export, Code_Thingol.Classinst
+ { class, tyco, vs, inst_params, superinst_params, ... })) =
let
val tyvars = intro_tyvars vs reserved;
val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
@@ -279,12 +281,12 @@
val aux_abstr1 = abstract_using aux_dom1;
val aux_abstr2 = abstract_using aux_dom2;
in
- concat ([str "val", print_method classparam, str "="]
+ privatize export ([str "val", print_method classparam, str "="]
@ aux_abstr1 @ aux_abstr2 @| print_app tyvars false (SOME thm) vars NOBR
(const, map (IVar o SOME) auxs))
end;
in
- Pretty.block_enclose (concat [str "implicit def",
+ Pretty.block_enclose (privatize export [str "implicit def",
constraint (print_context tyvars vs sym) (print_dicttyp tyvars classtyp),
str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
(map print_classparam_instance (inst_params @ superinst_params))