keep only identifiers public which are explicitly requested or demanded by dependencies
authorhaftmann
Sun Feb 23 10:33:43 2014 +0100 (2014-02-23)
changeset 55684ee49b4f7edc8
parent 55683 5732a55b9232
child 55685 3f8bdc5364a9
keep only identifiers public which are explicitly requested or demanded by dependencies
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_namespace.ML
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Feb 23 10:33:43 2014 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Feb 23 10:33:43 2014 +0100
     1.3 @@ -308,7 +308,7 @@
     1.4      val ctxt = Proof_Context.init_global thy
     1.5      fun evaluator program ((_, vs_ty), t) deps =
     1.6        Exn.interruptible_capture (value opts ctxt cookie)
     1.7 -        (Code_Target.evaluator thy target program deps (vs_ty, t));
     1.8 +        (Code_Target.evaluator thy target program deps true (vs_ty, t));
     1.9    in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
    1.10  
    1.11  (** counterexample generator **)
     2.1 --- a/src/Tools/Code/code_ml.ML	Sun Feb 23 10:33:43 2014 +0100
     2.2 +++ b/src/Tools/Code/code_ml.ML	Sun Feb 23 10:33:43 2014 +0100
     2.3 @@ -37,7 +37,7 @@
     2.4  datatype ml_stmt =
     2.5      ML_Exc of string * (typscheme * int)
     2.6    | ML_Val of ml_binding
     2.7 -  | ML_Funs of ml_binding list * Code_Symbol.T list
     2.8 +  | ML_Funs of (Code_Namespace.export * ml_binding) list * Code_Symbol.T list
     2.9    | ML_Datas of (string * (vname list * ((string * vname list) * itype list) list)) list
    2.10    | ML_Class of string * (vname * ((class * class) list * (string * itype) list));
    2.11  
    2.12 @@ -260,7 +260,7 @@
    2.13              [sig_p]
    2.14              (semicolon [p])
    2.15            end
    2.16 -      | print_stmt _ (ML_Funs (binding :: bindings, pseudo_funs)) =
    2.17 +      | print_stmt _ (ML_Funs ((export, binding) :: exports_bindings, pseudo_funs)) =
    2.18            let
    2.19              val print_def' = print_def (member (op =) pseudo_funs) false;
    2.20              fun print_pseudo_fun sym = concat [
    2.21 @@ -271,10 +271,11 @@
    2.22                  str "();"
    2.23                ];
    2.24              val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
    2.25 -              (print_def' "fun" binding :: map (print_def' "and") bindings);
    2.26 +              (print_def' "fun" binding :: map (print_def' "and" o snd) exports_bindings);
    2.27              val pseudo_ps = map print_pseudo_fun pseudo_funs;
    2.28            in pair
    2.29 -            sig_ps
    2.30 +            (map_filter (fn (export, p) => if Code_Namespace.not_private export then SOME p else NONE)
    2.31 +              ((export :: map fst exports_bindings) ~~ sig_ps))
    2.32              (Pretty.chunks (ps @ semicolon [p] :: pseudo_ps))
    2.33            end
    2.34       | print_stmt _ (ML_Datas [(tyco, (vs, []))]) =
    2.35 @@ -605,7 +606,7 @@
    2.36              [sig_p]
    2.37              (doublesemicolon [p])
    2.38            end
    2.39 -      | print_stmt _ (ML_Funs (binding :: bindings, pseudo_funs)) =
    2.40 +      | print_stmt _ (ML_Funs ((export, binding) :: exports_bindings, pseudo_funs)) =
    2.41            let
    2.42              val print_def' = print_def (member (op =) pseudo_funs) false;
    2.43              fun print_pseudo_fun sym = concat [
    2.44 @@ -616,10 +617,11 @@
    2.45                  str "();;"
    2.46                ];
    2.47              val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
    2.48 -              (print_def' "let rec" binding :: map (print_def' "and") bindings);
    2.49 +              (print_def' "let rec" binding :: map (print_def' "and" o snd) exports_bindings);
    2.50              val pseudo_ps = map print_pseudo_fun pseudo_funs;
    2.51            in pair
    2.52 -            sig_ps
    2.53 +            (map_filter (fn (export, p) => if Code_Namespace.not_private export then SOME p else NONE)
    2.54 +              ((export :: map fst exports_bindings) ~~ sig_ps))
    2.55              (Pretty.chunks (ps @ doublesemicolon [p] :: pseudo_ps))
    2.56            end
    2.57       | print_stmt _ (ML_Datas [(tyco, (vs, []))]) =
    2.58 @@ -667,7 +669,9 @@
    2.59                  )
    2.60                ];
    2.61            in pair
    2.62 -            (type_decl_p :: map print_classparam_decl classparams)
    2.63 +           (if Code_Namespace.is_public export
    2.64 +              then type_decl_p :: map print_classparam_decl classparams
    2.65 +              else [concat [str "type", print_dicttyp (class, ITyVar v)]])
    2.66              (Pretty.chunks (
    2.67                doublesemicolon [type_decl_p]
    2.68                :: map print_classparam_proj classparams
    2.69 @@ -733,7 +737,7 @@
    2.70        | namify_stmt (Code_Thingol.Classrel _) = namify_const false
    2.71        | namify_stmt (Code_Thingol.Classparam _) = namify_const false
    2.72        | namify_stmt (Code_Thingol.Classinst _) = namify_const false;
    2.73 -    fun ml_binding_of_stmt (sym as Constant const, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _)) =
    2.74 +    fun ml_binding_of_stmt (sym as Constant const, (export, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _))) =
    2.75            let
    2.76              val eqs = filter (snd o snd) raw_eqs;
    2.77              val (eqs', some_sym) = if null (filter_out (null o snd) vs) then case eqs
    2.78 @@ -742,49 +746,58 @@
    2.79                    else (eqs, SOME (sym, member (op =) (Code_Thingol.add_constsyms t []) sym))
    2.80                  | _ => (eqs, NONE)
    2.81                else (eqs, NONE)
    2.82 -          in (ML_Function (const, (tysm, eqs')), some_sym) end
    2.83 -      | ml_binding_of_stmt (sym as Class_Instance inst, Code_Thingol.Classinst (stmt as { vs, ... })) =
    2.84 -          (ML_Instance (inst, stmt), if forall (null o snd) vs then SOME (sym, false) else NONE)
    2.85 +          in ((export, ML_Function (const, (tysm, eqs'))), some_sym) end
    2.86 +      | ml_binding_of_stmt (sym as Class_Instance inst, (export, Code_Thingol.Classinst (stmt as { vs, ... }))) =
    2.87 +          ((export, ML_Instance (inst, stmt)),
    2.88 +            if forall (null o snd) vs then SOME (sym, false) else NONE)
    2.89        | ml_binding_of_stmt (sym, _) =
    2.90            error ("Binding block containing illegal statement: " ^ 
    2.91              Code_Symbol.quote ctxt sym)
    2.92 -    fun modify_fun (sym, stmt) =
    2.93 +    fun modify_fun (sym, (export, stmt)) =
    2.94        let
    2.95 -        val (binding, some_value_sym) = ml_binding_of_stmt (sym, stmt);
    2.96 +        val ((export', binding), some_value_sym) = ml_binding_of_stmt (sym, (export, stmt));
    2.97          val ml_stmt = case binding
    2.98           of ML_Function (const, ((vs, ty), [])) =>
    2.99                ML_Exc (const, ((vs, ty),
   2.100                  (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty))
   2.101            | _ => case some_value_sym
   2.102 -             of NONE => ML_Funs ([binding], [])
   2.103 -              | SOME (sym, true) => ML_Funs ([binding], [sym])
   2.104 +             of NONE => ML_Funs ([(export', binding)], [])
   2.105 +              | SOME (sym, true) => ML_Funs ([(export, binding)], [sym])
   2.106                | SOME (sym, false) => ML_Val binding
   2.107 -      in SOME ml_stmt end;
   2.108 +      in SOME (export, ml_stmt) end;
   2.109      fun modify_funs stmts = single (SOME
   2.110 -      (ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
   2.111 -    fun modify_datatypes stmts = single (SOME
   2.112 -      (ML_Datas (map_filter
   2.113 -        (fn (Type_Constructor tyco, Code_Thingol.Datatype stmt) => SOME (tyco, stmt) | _ => NONE) stmts)))
   2.114 -    fun modify_class stmts = single (SOME
   2.115 -      (ML_Class (the_single (map_filter
   2.116 -        (fn (Type_Class class, Code_Thingol.Class stmt) => SOME (class, stmt) | _ => NONE) stmts))))
   2.117 -    fun modify_stmts ([stmt as (_, stmt' as Code_Thingol.Fun _)]) =
   2.118 +      (Code_Namespace.Opaque, ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
   2.119 +    fun modify_datatypes stmts =
   2.120 +      map_filter
   2.121 +        (fn (Type_Constructor tyco, (export, Code_Thingol.Datatype stmt)) => SOME (export, (tyco, stmt)) | _ => NONE) stmts
   2.122 +      |> split_list
   2.123 +      |> apfst Code_Namespace.join_exports
   2.124 +      |> apsnd ML_Datas
   2.125 +      |> SOME
   2.126 +      |> single;
   2.127 +    fun modify_class stmts =
   2.128 +      the_single (map_filter
   2.129 +        (fn (Type_Class class, (export, Code_Thingol.Class stmt)) => SOME (export, (class, stmt)) | _ => NONE) stmts)
   2.130 +      |> apsnd ML_Class
   2.131 +      |> SOME
   2.132 +      |> single;
   2.133 +    fun modify_stmts ([stmt as (_, (_, stmt' as Code_Thingol.Fun _))]) =
   2.134            if Code_Thingol.is_case stmt' then [] else [modify_fun stmt]
   2.135 -      | modify_stmts ((stmts as (_, Code_Thingol.Fun _) :: _)) =
   2.136 -          modify_funs (filter_out (Code_Thingol.is_case o snd) stmts)
   2.137 -      | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _) :: _)) =
   2.138 +      | modify_stmts ((stmts as (_, (_, Code_Thingol.Fun _)) :: _)) =
   2.139 +          modify_funs (filter_out (Code_Thingol.is_case o snd o snd) stmts)
   2.140 +      | modify_stmts ((stmts as (_, (_, Code_Thingol.Datatypecons _)) :: _)) =
   2.141            modify_datatypes stmts
   2.142 -      | modify_stmts ((stmts as (_, Code_Thingol.Datatype _) :: _)) =
   2.143 +      | modify_stmts ((stmts as (_, (_, Code_Thingol.Datatype _)) :: _)) =
   2.144            modify_datatypes stmts
   2.145 -      | modify_stmts ((stmts as (_, Code_Thingol.Class _) :: _)) =
   2.146 +      | modify_stmts ((stmts as (_, (_, Code_Thingol.Class _)) :: _)) =
   2.147            modify_class stmts
   2.148 -      | modify_stmts ((stmts as (_, Code_Thingol.Classrel _) :: _)) =
   2.149 +      | modify_stmts ((stmts as (_, (_, Code_Thingol.Classrel _)) :: _)) =
   2.150            modify_class stmts
   2.151 -      | modify_stmts ((stmts as (_, Code_Thingol.Classparam _) :: _)) =
   2.152 +      | modify_stmts ((stmts as (_, (_, Code_Thingol.Classparam _)) :: _)) =
   2.153            modify_class stmts
   2.154 -      | modify_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
   2.155 +      | modify_stmts ([stmt as (_, (_, Code_Thingol.Classinst _))]) =
   2.156            [modify_fun stmt]
   2.157 -      | modify_stmts ((stmts as (_, Code_Thingol.Classinst _) :: _)) =
   2.158 +      | modify_stmts ((stmts as (_, (_, Code_Thingol.Classinst _)) :: _)) =
   2.159            modify_funs stmts
   2.160        | modify_stmts stmts = error ("Illegal mutual dependencies: " ^
   2.161            (Library.commas o map (Code_Symbol.quote ctxt o fst)) stmts);
   2.162 @@ -792,7 +805,9 @@
   2.163      Code_Namespace.hierarchical_program ctxt {
   2.164        module_name = module_name, reserved = reserved, identifiers = identifiers,
   2.165        empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,
   2.166 -      cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts }
   2.167 +      cyclic_modules = false, class_transitive = false,
   2.168 +      class_relation_public = true, empty_data = (),
   2.169 +      memorize_data = K I, modify_stmts = modify_stmts }
   2.170    end;
   2.171  
   2.172  fun serialize_ml print_ml_module print_ml_stmt ctxt
     3.1 --- a/src/Tools/Code/code_namespace.ML	Sun Feb 23 10:33:43 2014 +0100
     3.2 +++ b/src/Tools/Code/code_namespace.ML	Sun Feb 23 10:33:43 2014 +0100
     3.3 @@ -9,6 +9,7 @@
     3.4    datatype export = Private | Opaque | Public
     3.5    val is_public: export -> bool
     3.6    val not_private: export -> bool
     3.7 +  val join_exports: export list -> export
     3.8  
     3.9    type flat_program
    3.10    val flat_program: Proof.context
    3.11 @@ -30,8 +31,10 @@
    3.12      reserved: Name.context, identifiers: Code_Target.identifier_data,
    3.13      empty_nsp: 'c, namify_module: string -> 'c -> string * 'c,
    3.14      namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c,
    3.15 -    cyclic_modules: bool, empty_data: 'b, memorize_data: Code_Symbol.T -> 'b -> 'b,
    3.16 -    modify_stmts: (Code_Symbol.T * Code_Thingol.stmt) list -> 'a option list }
    3.17 +    cyclic_modules: bool,
    3.18 +    class_transitive: bool, class_relation_public: bool,
    3.19 +    empty_data: 'b, memorize_data: Code_Symbol.T -> 'b -> 'b,
    3.20 +    modify_stmts: (Code_Symbol.T * (export * Code_Thingol.stmt)) list -> (export * 'a) option list }
    3.21        -> Code_Symbol.T list -> Code_Thingol.program
    3.22        -> { deresolver: string list -> Code_Symbol.T -> string,
    3.23             hierarchical_program: ('a, 'b) hierarchical_program }
    3.24 @@ -55,6 +58,94 @@
    3.25    | not_private Opaque = true
    3.26    | not_private _ = false;
    3.27  
    3.28 +fun mark_export Public _ = Public
    3.29 +  | mark_export _ Public = Public
    3.30 +  | mark_export Opaque _ = Opaque
    3.31 +  | mark_export _ Opaque = Opaque
    3.32 +  | mark_export _ _ = Private;
    3.33 +
    3.34 +fun join_exports exports = fold mark_export exports Private;
    3.35 +
    3.36 +fun dependent_exports { program = program, class_transitive = class_transitive } =
    3.37 +  let
    3.38 +    fun is_datatype_or_class (Code_Symbol.Type_Constructor _) = true
    3.39 +      | is_datatype_or_class (Code_Symbol.Type_Class _) = true
    3.40 +      | is_datatype_or_class _ = false;
    3.41 +    fun is_relevant (Code_Symbol.Class_Relation _) = true
    3.42 +      | is_relevant sym = is_datatype_or_class sym;
    3.43 +    val proto_gr = Code_Symbol.Graph.restrict is_relevant program;
    3.44 +    val gr =
    3.45 +      proto_gr
    3.46 +      |> Code_Symbol.Graph.fold
    3.47 +          (fn (sym, (_, (_, deps))) =>
    3.48 +            if is_relevant sym
    3.49 +            then I
    3.50 +            else
    3.51 +              Code_Symbol.Graph.new_node (sym, Code_Thingol.NoStmt)
    3.52 +              #> Code_Symbol.Graph.Keys.fold
    3.53 +               (fn sym' =>
    3.54 +                if is_relevant sym'
    3.55 +                then Code_Symbol.Graph.add_edge (sym, sym')
    3.56 +                else I) deps) program
    3.57 +      |> class_transitive ?
    3.58 +          Code_Symbol.Graph.fold (fn (sym as Code_Symbol.Type_Class _, _) =>
    3.59 +            fold (curry Code_Symbol.Graph.add_edge sym)
    3.60 +              ((remove (op =) sym o Code_Symbol.Graph.all_succs proto_gr) [sym]) | _ => I) proto_gr
    3.61 +    fun deps_of sym =
    3.62 +      let
    3.63 +        val succs = Code_Symbol.Graph.Keys.dest o Code_Symbol.Graph.imm_succs gr;
    3.64 +        val deps1 = succs sym;
    3.65 +        val deps2 = if class_transitive
    3.66 +          then []
    3.67 +          else [] |> fold (union (op =)) (map succs deps1) |> subtract (op =) deps1
    3.68 +      in (deps1, deps2) end;
    3.69 +  in
    3.70 +    { is_datatype_or_class = is_datatype_or_class,
    3.71 +      deps_of = deps_of }
    3.72 +  end;
    3.73 +
    3.74 +fun mark_exports_aux { program = program, prefix_of = prefix_of, map_export = map_export,
    3.75 +    is_datatype_or_class = is_datatype_or_class, deps_of = deps_of,
    3.76 +    class_relation_public = class_relation_public } prefix sym =
    3.77 +  let
    3.78 +    val export = (if is_datatype_or_class sym then Opaque else Public);
    3.79 +    val (dependent_export1, dependent_export2) =
    3.80 +      case Code_Symbol.Graph.get_node program sym of
    3.81 +          Code_Thingol.Fun _ => (SOME Opaque, NONE)
    3.82 +        | Code_Thingol.Classinst _ => (SOME Opaque, NONE)
    3.83 +        | Code_Thingol.Datatypecons _ => (SOME Public, SOME Opaque)
    3.84 +        | Code_Thingol.Classparam _ => (SOME Public, SOME Opaque)
    3.85 +        | Code_Thingol.Classrel _ =>
    3.86 +           (if class_relation_public
    3.87 +            then (SOME Public, SOME Opaque)
    3.88 +            else (SOME Opaque, NONE))
    3.89 +        | _ => (NONE, NONE);
    3.90 +    val dependent_exports =
    3.91 +      case dependent_export1 of
    3.92 +        SOME export1 => (case dependent_export2 of
    3.93 +          SOME export2 =>
    3.94 +            let
    3.95 +              val (deps1, deps2) = deps_of sym
    3.96 +            in map (rpair export1) deps1 @ map (rpair export2) deps2 end
    3.97 +        | NONE => map (rpair export1) (fst (deps_of sym)))
    3.98 +      | NONE => [];
    3.99 +  in 
   3.100 +    map_export prefix sym (mark_export export)
   3.101 +    #> fold (fn (sym, export) => map_export (prefix_of sym) sym (mark_export export))
   3.102 +      dependent_exports
   3.103 +  end;
   3.104 +
   3.105 +fun mark_exports { program = program, prefix_of = prefix_of, map_export = map_export,
   3.106 +    class_transitive = class_transitive, class_relation_public = class_relation_public } =
   3.107 +  let
   3.108 +    val { is_datatype_or_class, deps_of } =
   3.109 +      dependent_exports { program = program, class_transitive = class_transitive };
   3.110 +  in
   3.111 +    mark_exports_aux { program = program, prefix_of = prefix_of, map_export = map_export,
   3.112 +      is_datatype_or_class = is_datatype_or_class, deps_of = deps_of,
   3.113 +      class_relation_public = class_relation_public }
   3.114 +  end;
   3.115 +
   3.116  
   3.117  (** fundamental module name hierarchy **)
   3.118  
   3.119 @@ -113,13 +204,17 @@
   3.120      val sym_priority = has_priority identifiers;
   3.121  
   3.122      (* distribute statements over hierarchy *)
   3.123 +    val mark_exports = mark_exports { program = program, prefix_of = fst o prep_sym,
   3.124 +      map_export = fn module_name => fn sym =>
   3.125 +        Graph.map_node module_name o apfst o Code_Symbol.Graph.map_node sym o apsnd o apfst,
   3.126 +        class_transitive = false, class_relation_public = false };
   3.127      fun add_stmt sym stmt =
   3.128        let
   3.129          val (module_name, base) = prep_sym sym;
   3.130        in
   3.131          Graph.default_node (module_name, (Code_Symbol.Graph.empty, []))
   3.132          #> (Graph.map_node module_name o apfst)
   3.133 -          (Code_Symbol.Graph.new_node (sym, (base, (Public, stmt))))
   3.134 +          (Code_Symbol.Graph.new_node (sym, (base, (if null exports then Public else Private, stmt))))
   3.135        end;
   3.136      fun add_dep sym sym' =
   3.137        let
   3.138 @@ -129,9 +224,11 @@
   3.139          then (Graph.map_node module_name o apfst) (Code_Symbol.Graph.add_edge (sym, sym'))
   3.140          else (Graph.map_node module_name o apsnd)
   3.141            (AList.map_default (op =) (module_name', []) (insert (op =) sym'))
   3.142 +          #> mark_exports module_name' sym'
   3.143        end;
   3.144      val proto_program = build_proto_program
   3.145 -      { empty = Graph.empty, add_stmt = add_stmt, add_dep = add_dep } program;
   3.146 +      { empty = Graph.empty, add_stmt = add_stmt, add_dep = add_dep } program
   3.147 +      |> fold (fn sym => mark_exports ((fst o prep_sym) sym) sym) exports;
   3.148  
   3.149      (* name declarations and statement modifications *)
   3.150      fun declare sym (base, (_, stmt)) (gr, nsp) = 
   3.151 @@ -200,7 +297,7 @@
   3.152    let
   3.153      val some_modules =
   3.154        sym_base_nodes
   3.155 -      |> map (fn (sym, (base, Module content)) => SOME (base, content) | _ => NONE)
   3.156 +      |> map (fn (_, (base, Module content)) => SOME (base, content) | _ => NONE)
   3.157        |> (burrow_options o map o apsnd) f_module;
   3.158      val some_export_stmts =
   3.159        sym_base_nodes
   3.160 @@ -214,7 +311,9 @@
   3.161    end;
   3.162  
   3.163  fun hierarchical_program ctxt { module_name, reserved, identifiers, empty_nsp,
   3.164 -      namify_module, namify_stmt, cyclic_modules, empty_data, memorize_data, modify_stmts }
   3.165 +      namify_module, namify_stmt, cyclic_modules,
   3.166 +      class_transitive, class_relation_public,
   3.167 +      empty_data, memorize_data, modify_stmts }
   3.168        exports program =
   3.169    let
   3.170  
   3.171 @@ -242,12 +341,17 @@
   3.172            o Code_Symbol.lookup identifiers o fst) program;
   3.173  
   3.174      (* distribute statements over hierarchy *)
   3.175 +    val mark_exports = mark_exports { program = program, prefix_of = fst o prep_sym,
   3.176 +      map_export = fn name_fragments => fn sym => fn f =>
   3.177 +        (map_module name_fragments o apsnd o Code_Symbol.Graph.map_node sym o apsnd)
   3.178 +          (fn Stmt (export, stmt) => Stmt (f export, stmt)),
   3.179 +      class_transitive = class_transitive, class_relation_public = class_relation_public };
   3.180      fun add_stmt sym stmt =
   3.181        let
   3.182          val (name_fragments, base) = prep_sym sym;
   3.183        in
   3.184          (map_module name_fragments o apsnd)
   3.185 -          (Code_Symbol.Graph.new_node (sym, (base, Stmt (Public, stmt))))
   3.186 +          (Code_Symbol.Graph.new_node (sym, (base, Stmt (if null exports then Public else Private, stmt))))
   3.187        end;
   3.188      fun add_edge_acyclic_error error_msg dep gr =
   3.189        Code_Symbol.Graph.add_edge_acyclic dep gr
   3.190 @@ -266,9 +370,13 @@
   3.191              ^ Code_Symbol.quote ctxt sym'
   3.192              ^ " would result in module dependency cycle") dep
   3.193            else Code_Symbol.Graph.add_edge dep;
   3.194 -      in (map_module name_fragments_common o apsnd) add_edge end;
   3.195 +      in
   3.196 +        (map_module name_fragments_common o apsnd) add_edge
   3.197 +        #> (if is_cross_module then mark_exports name_fragments' sym' else I)
   3.198 +      end;
   3.199      val proto_program = build_proto_program
   3.200 -      { empty = empty_program, add_stmt = add_stmt, add_dep = add_dep } program;
   3.201 +      { empty = empty_program, add_stmt = add_stmt, add_dep = add_dep } program
   3.202 +      |> fold (fn sym => mark_exports ((fst o prep_sym) sym) sym) exports;
   3.203  
   3.204      (* name declarations, data and statement modifications *)
   3.205      fun make_declarations nsps (data, nodes) =
   3.206 @@ -292,14 +400,9 @@
   3.207            let
   3.208              val stmts' = modify_stmts syms_stmts
   3.209            in stmts' @ replicate (length syms_stmts - length stmts') NONE end;
   3.210 -        fun modify_stmts'' syms_exports_stmts =
   3.211 -          syms_exports_stmts
   3.212 -          |> map (fn (sym, (export, stmt)) => ((sym, stmt), export))
   3.213 -          |> burrow_fst modify_stmts'
   3.214 -          |> map (fn (SOME stmt, export) => SOME (export, stmt) | _ => NONE);
   3.215          val nodes'' =
   3.216            nodes'
   3.217 -          |> Code_Symbol.Graph.map_strong_conn (map_module_stmts (make_declarations nsps') modify_stmts'');
   3.218 +          |> Code_Symbol.Graph.map_strong_conn (map_module_stmts (make_declarations nsps') modify_stmts');
   3.219          val data' = fold memorize_data stmt_syms data;
   3.220        in (data', nodes'') end;
   3.221      val (_, hierarchical_program) = make_declarations empty_nsp proto_program;
     4.1 --- a/src/Tools/Code/code_runtime.ML	Sun Feb 23 10:33:43 2014 +0100
     4.2 +++ b/src/Tools/Code/code_runtime.ML	Sun Feb 23 10:33:43 2014 +0100
     4.3 @@ -89,7 +89,7 @@
     4.4    in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end;
     4.5  
     4.6  fun obtain_evaluator thy some_target program consts expr =
     4.7 -  Code_Target.evaluator thy (the_default target some_target) program consts expr
     4.8 +  Code_Target.evaluator thy (the_default target some_target) program consts false expr
     4.9    |> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
    4.10  
    4.11  fun obtain_evaluator' thy some_target program =
     5.1 --- a/src/Tools/Code/code_scala.ML	Sun Feb 23 10:33:43 2014 +0100
     5.2 +++ b/src/Tools/Code/code_scala.ML	Sun Feb 23 10:33:43 2014 +0100
     5.3 @@ -249,7 +249,7 @@
     5.4                  val auxs = Name.invent (snd proto_vars) "a" (length tys);
     5.5                  val vars = intro_vars auxs proto_vars;
     5.6                in
     5.7 -                privatize export [str "def", constraint (Pretty.block [applify "(" ")"
     5.8 +                privatize' export [str "def", constraint (Pretty.block [applify "(" ")"
     5.9                    (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
    5.10                    (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_const classparam))
    5.11                    (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
    5.12 @@ -284,7 +284,7 @@
    5.13                  val aux_abstr1 = abstract_using aux_dom1;
    5.14                  val aux_abstr2 = abstract_using aux_dom2;
    5.15                in
    5.16 -                privatize export ([str "val", print_method classparam, str "="]
    5.17 +                concat ([str "val", print_method classparam, str "="]
    5.18                    @ aux_abstr1 @ aux_abstr2 @| print_app tyvars false (SOME thm) vars NOBR
    5.19                      (const, map (IVar o SOME) auxs))
    5.20                end;
    5.21 @@ -333,16 +333,17 @@
    5.22          val implicits = filter (is_classinst o Code_Symbol.Graph.get_node program)
    5.23            (Code_Symbol.Graph.immediate_succs program sym);
    5.24        in union (op =) implicits end;
    5.25 -    fun modify_stmt (_, Code_Thingol.Fun (_, SOME _)) = NONE
    5.26 -      | modify_stmt (_, Code_Thingol.Datatypecons _) = NONE
    5.27 -      | modify_stmt (_, Code_Thingol.Classrel _) = NONE
    5.28 -      | modify_stmt (_, Code_Thingol.Classparam _) = NONE
    5.29 -      | modify_stmt (_, stmt) = SOME stmt;
    5.30 +    fun modify_stmt (_, (_, Code_Thingol.Fun (_, SOME _))) = NONE
    5.31 +      | modify_stmt (_, (_, Code_Thingol.Datatypecons _)) = NONE
    5.32 +      | modify_stmt (_, (_, Code_Thingol.Classrel _)) = NONE
    5.33 +      | modify_stmt (_, (_, Code_Thingol.Classparam _)) = NONE
    5.34 +      | modify_stmt (_, export_stmt) = SOME export_stmt;
    5.35    in
    5.36      Code_Namespace.hierarchical_program ctxt
    5.37        { module_name = module_name, reserved = reserved, identifiers = identifiers,
    5.38          empty_nsp = ((reserved, reserved), reserved), namify_module = namify_module,
    5.39 -        namify_stmt = namify_stmt, cyclic_modules = true, empty_data = [],
    5.40 +        namify_stmt = namify_stmt, cyclic_modules = true,
    5.41 +        class_transitive = true, class_relation_public = false, empty_data = [],
    5.42          memorize_data = memorize_implicits, modify_stmts = map modify_stmt } exports program
    5.43    end;
    5.44  
     6.1 --- a/src/Tools/Code/code_target.ML	Sun Feb 23 10:33:43 2014 +0100
     6.2 +++ b/src/Tools/Code/code_target.ML	Sun Feb 23 10:33:43 2014 +0100
     6.3 @@ -29,7 +29,7 @@
     6.4  
     6.5    val generatedN: string
     6.6    val evaluator: theory -> string -> Code_Thingol.program
     6.7 -    -> Code_Symbol.T list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
     6.8 +    -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
     6.9      -> (string * string) list * string
    6.10  
    6.11    type serializer
    6.12 @@ -426,7 +426,7 @@
    6.13      else Isabelle_System.with_tmp_dir "Code_Test" ext_check
    6.14    end;
    6.15  
    6.16 -fun evaluation mounted_serializer prepared_program syms ((vs, ty), t) =
    6.17 +fun evaluation mounted_serializer prepared_program syms all_public ((vs, ty), t) =
    6.18    let
    6.19      val _ = if Code_Thingol.contains_dict_var t then
    6.20        error "Term to be evaluated contains free dictionaries" else ();
    6.21 @@ -439,7 +439,7 @@
    6.22        |> fold (curry (perhaps o try o
    6.23            Code_Symbol.Graph.add_edge) Code_Symbol.value) syms;
    6.24      val (program_code, deresolve) =
    6.25 -      produce (mounted_serializer program [Code_Symbol.value]);
    6.26 +      produce (mounted_serializer program (if all_public then [] else [Code_Symbol.value]));
    6.27      val value_name = the (deresolve Code_Symbol.value);
    6.28    in (program_code, value_name) end;
    6.29