# HG changeset patch # User haftmann # Date 1393148023 -3600 # Node ID 7714287dc04486febf65e46c010886bbcad622bc # Parent bc5edc5dbf184f4c8caef088a02a033096d361b2 more fine-grain notion of export diff -r bc5edc5dbf18 -r 7714287dc044 src/Tools/Code/code_haskell.ML --- 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 diff -r bc5edc5dbf18 -r 7714287dc044 src/Tools/Code/code_ml.ML --- 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 = diff -r bc5edc5dbf18 -r 7714287dc044 src/Tools/Code/code_namespace.ML --- 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 diff -r bc5edc5dbf18 -r 7714287dc044 src/Tools/Code/code_scala.ML --- 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)