--- 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
@@ -379,15 +379,17 @@
val deresolve = deresolver 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;
+ fun print_import (sym, (_, Code_Thingol.Fun _)) = deresolve_import sym
+ | print_import (sym, (Code_Namespace.Public, Code_Thingol.Datatype _)) = deresolve_import_attached sym
+ | print_import (sym, (Code_Namespace.Opaque, Code_Thingol.Datatype _)) = deresolve_import sym
+ | print_import (sym, (Code_Namespace.Public, Code_Thingol.Class _)) = deresolve_import_attached sym
+ | print_import (sym, (Code_Namespace.Opaque, Code_Thingol.Class _)) = deresolve_import 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 (export, stmt)) =>
- SOME (if export then print_import (sym, stmt) else NONE, markup_stmt sym (print_stmt deresolve (sym, stmt)));
+ SOME (if Code_Namespace.not_private export then print_import (sym, (export, 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
--- 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
@@ -242,7 +242,7 @@
@@ print_dicttyp (class, tyco `%% map (ITyVar o fst) vs)
))
end;
- fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
+ fun print_stmt _ (ML_Exc (const, (vs_ty, n))) = pair
[print_val_decl print_typscheme (Constant const, vs_ty)]
((semicolon o map str) (
(if n = 0 then "val" else "fun")
@@ -253,14 +253,14 @@
:: "Fail"
@@ ML_Syntax.print_string const
))
- | print_stmt (ML_Val binding) =
+ | print_stmt _ (ML_Val binding) =
let
val (sig_p, p) = print_def (K false) true "val" binding
in pair
[sig_p]
(semicolon [p])
end
- | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
+ | print_stmt _ (ML_Funs (binding :: bindings, pseudo_funs)) =
let
val print_def' = print_def (member (op =) pseudo_funs) false;
fun print_pseudo_fun sym = concat [
@@ -277,24 +277,28 @@
sig_ps
(Pretty.chunks (ps @ semicolon [p] :: pseudo_ps))
end
- | print_stmt (ML_Datas [(tyco, (vs, []))]) =
+ | print_stmt _ (ML_Datas [(tyco, (vs, []))]) =
let
val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
in
pair
[concat [str "type", ty_p]]
- (concat [str "datatype", ty_p, str "=", str "EMPTY__"])
+ (semicolon [str "datatype", ty_p, str "=", str "EMPTY__"])
end
- | print_stmt (ML_Datas (data :: datas)) =
+ | print_stmt export (ML_Datas (data :: datas)) =
let
- val sig_ps = print_datatype_decl "datatype" data
+ val decl_ps = print_datatype_decl "datatype" data
:: map (print_datatype_decl "and") datas;
- val (ps, p) = split_last sig_ps;
+ val (ps, p) = split_last decl_ps;
in pair
- sig_ps
+ (if Code_Namespace.is_public export
+ then decl_ps
+ else map (fn (tyco, (vs, _)) =>
+ concat [str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)])
+ (data :: datas))
(Pretty.chunks (ps @| semicolon [p]))
end
- | print_stmt (ML_Class (class, (v, (classrels, classparams)))) =
+ | print_stmt export (ML_Class (class, (v, (classrels, classparams)))) =
let
fun print_field s p = concat [str s, str ":", p];
fun print_proj s p = semicolon
@@ -317,12 +321,14 @@
(print_typscheme ([(v, [class])], ty));
in pair
(concat [str "type", print_dicttyp (class, ITyVar v)]
- :: map print_super_class_decl classrels
- @ map print_classparam_decl classparams)
+ :: (if Code_Namespace.is_public export
+ then map print_super_class_decl classrels
+ @ map print_classparam_decl classparams
+ else []))
(Pretty.chunks (
concat [
- str ("type '" ^ v),
- (str o deresolve_class) class,
+ str "type",
+ print_dicttyp (class, ITyVar v),
str "=",
enum "," "{" "};" (
map print_super_class_field classrels
@@ -582,7 +588,7 @@
]
))
end;
- fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
+ fun print_stmt _ (ML_Exc (const, (vs_ty, n))) = pair
[print_val_decl print_typscheme (Constant const, vs_ty)]
((doublesemicolon o map str) (
"let"
@@ -592,14 +598,14 @@
:: "failwith"
@@ ML_Syntax.print_string const
))
- | print_stmt (ML_Val binding) =
+ | print_stmt _ (ML_Val binding) =
let
val (sig_p, p) = print_def (K false) true "let" binding
in pair
[sig_p]
(doublesemicolon [p])
end
- | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
+ | print_stmt _ (ML_Funs (binding :: bindings, pseudo_funs)) =
let
val print_def' = print_def (member (op =) pseudo_funs) false;
fun print_pseudo_fun sym = concat [
@@ -616,24 +622,28 @@
sig_ps
(Pretty.chunks (ps @ doublesemicolon [p] :: pseudo_ps))
end
- | print_stmt (ML_Datas [(tyco, (vs, []))]) =
+ | print_stmt _ (ML_Datas [(tyco, (vs, []))]) =
let
val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
in
pair
[concat [str "type", ty_p]]
- (concat [str "type", ty_p, str "=", str "EMPTY__"])
+ (doublesemicolon [str "type", ty_p, str "=", str "EMPTY__"])
end
- | print_stmt (ML_Datas (data :: datas)) =
+ | print_stmt export (ML_Datas (data :: datas)) =
let
- val sig_ps = print_datatype_decl "type" data
+ val decl_ps = print_datatype_decl "type" data
:: map (print_datatype_decl "and") datas;
- val (ps, p) = split_last sig_ps;
+ val (ps, p) = split_last decl_ps;
in pair
- sig_ps
+ (if Code_Namespace.is_public export
+ then decl_ps
+ else map (fn (tyco, (vs, _)) =>
+ concat [str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)])
+ (data :: datas))
(Pretty.chunks (ps @| doublesemicolon [p]))
end
- | print_stmt (ML_Class (class, (v, (classrels, classparams)))) =
+ | print_stmt export (ML_Class (class, (v, (classrels, classparams)))) =
let
fun print_field s p = concat [str s, str ":", p];
fun print_super_class_field (classrel as (_, super_class)) =
@@ -705,7 +715,7 @@
(** SML/OCaml generic part **)
-fun ml_program_of_program ctxt module_name reserved identifiers program =
+fun ml_program_of_program ctxt module_name reserved identifiers =
let
fun namify_const upper base (nsp_const, nsp_type) =
let
@@ -782,7 +792,7 @@
Code_Namespace.hierarchical_program ctxt {
module_name = module_name, reserved = reserved, identifiers = identifiers,
empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,
- cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
+ cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts }
end;
fun serialize_ml print_ml_module print_ml_stmt ctxt
@@ -792,13 +802,14 @@
(* build program *)
val { deresolver, hierarchical_program = ml_program } =
- ml_program_of_program ctxt module_name (Name.make_context reserved_syms) identifiers program;
+ ml_program_of_program ctxt module_name (Name.make_context reserved_syms)
+ identifiers program;
(* print statements *)
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 (fn decl => if export then SOME decl else NONE);
+ (Code_Thingol.is_constr program) (deresolver prefix_fragments) export stmt
+ |> apfst (fn decl => if Code_Namespace.not_private 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
@@ -6,6 +6,10 @@
signature CODE_NAMESPACE =
sig
+ datatype export = Private | Opaque | Public
+ val is_public: export -> bool
+ val not_private: export -> bool
+
type flat_program
val flat_program: Proof.context
-> { module_prefix: string, module_name: string,
@@ -18,7 +22,7 @@
datatype ('a, 'b) node =
Dummy
- | Stmt of bool * 'a
+ | Stmt of export * 'a
| Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T)
type ('a, 'b) hierarchical_program
val hierarchical_program: Proof.context
@@ -32,7 +36,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 * (bool * 'a) -> 'c,
+ print_stmt: string list -> Code_Symbol.T * (export * 'a) -> 'c,
lift_markup: (Pretty.T -> Pretty.T) -> 'c -> 'c }
-> ('a, 'b) hierarchical_program -> 'c list
end;
@@ -40,6 +44,18 @@
structure Code_Namespace : CODE_NAMESPACE =
struct
+(** export **)
+
+datatype export = Private | Opaque | Public;
+
+fun is_public Public = true
+ | is_public _ = false;
+
+fun not_private Public = true
+ | not_private Opaque = true
+ | not_private _ = false;
+
+
(** fundamental module name hierarchy **)
fun module_fragments' { identifiers, reserved } name =
@@ -82,7 +98,7 @@
(** flat program structure **)
-type flat_program = ((string * (bool * Code_Thingol.stmt) option) Code_Symbol.Graph.T * (string * Code_Symbol.T list) list) Graph.T;
+type flat_program = ((string * (export * 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 =
@@ -103,7 +119,7 @@
in
Graph.default_node (module_name, (Code_Symbol.Graph.empty, []))
#> (Graph.map_node module_name o apfst)
- (Code_Symbol.Graph.new_node (sym, (base, (true, stmt))))
+ (Code_Symbol.Graph.new_node (sym, (base, (Public, stmt))))
end;
fun add_dep sym sym' =
let
@@ -166,7 +182,7 @@
datatype ('a, 'b) node =
Dummy
- | Stmt of bool * 'a
+ | Stmt of export * '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;
@@ -230,7 +246,7 @@
val (name_fragments, base) = prep_sym sym;
in
(map_module name_fragments o apsnd)
- (Code_Symbol.Graph.new_node (sym, (base, Stmt (true, stmt))))
+ (Code_Symbol.Graph.new_node (sym, (base, Stmt (Public, stmt))))
end;
fun add_edge_acyclic_error error_msg dep gr =
Code_Symbol.Graph.add_edge_acyclic dep gr
--- 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,8 +145,11 @@
|> single
|> enclose "(" ")"
end;
- fun privatize false = concat o cons (str "private")
- | privatize true = concat;
+ fun privatize Code_Namespace.Public = concat
+ | privatize _ = concat o cons (str "private");
+ fun privatize' Code_Namespace.Public = concat
+ | privatize' Code_Namespace.Opaque = concat
+ | privatize' _ = concat o cons (str "private");
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))
@@ -224,7 +227,7 @@
];
in
Pretty.chunks (applify "[" "]" (str o lookup_tyvar tyvars)
- NOBR ((privatize export 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, (export, Code_Thingol.Class (v, (classrels, classparams)))) =
@@ -257,7 +260,7 @@
in
Pretty.chunks (
(Pretty.block_enclose
- (privatize export ([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
@@ -349,7 +352,8 @@
(* build program *)
val { deresolver, hierarchical_program = scala_program } =
- scala_program_of_program ctxt module_name (Name.make_context reserved_syms) identifiers program;
+ scala_program_of_program ctxt module_name (Name.make_context reserved_syms)
+ identifiers program;
(* print statements *)
fun lookup_constr tyco constr = case Code_Symbol.Graph.get_node program (Type_Constructor tyco)