more fine-grain notion of export
authorhaftmann
Sun Feb 23 10:33:43 2014 +0100 (2014-02-23)
changeset 556817714287dc044
parent 55680 bc5edc5dbf18
child 55682 def6575032df
more fine-grain notion of export
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_namespace.ML
src/Tools/Code/code_scala.ML
     1.1 --- a/src/Tools/Code/code_haskell.ML	Sun Feb 23 10:33:43 2014 +0100
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Sun Feb 23 10:33:43 2014 +0100
     1.3 @@ -379,15 +379,17 @@
     1.4          val deresolve = deresolver module_name;
     1.5          val deresolve_import = SOME o str o deresolve;
     1.6          val deresolve_import_attached = SOME o str o suffix "(..)" o deresolve;
     1.7 -        fun print_import (sym, Code_Thingol.Fun _) = deresolve_import sym
     1.8 -          | print_import (sym, Code_Thingol.Datatype _) = deresolve_import_attached sym
     1.9 -          | print_import (sym, Code_Thingol.Class _) = deresolve_import_attached sym
    1.10 -          | print_import (sym, Code_Thingol.Classinst _) = NONE;
    1.11 +        fun print_import (sym, (_, Code_Thingol.Fun _)) = deresolve_import sym
    1.12 +          | print_import (sym, (Code_Namespace.Public, Code_Thingol.Datatype _)) = deresolve_import_attached sym
    1.13 +          | print_import (sym, (Code_Namespace.Opaque, Code_Thingol.Datatype _)) = deresolve_import sym
    1.14 +          | print_import (sym, (Code_Namespace.Public, Code_Thingol.Class _)) = deresolve_import_attached sym
    1.15 +          | print_import (sym, (Code_Namespace.Opaque, Code_Thingol.Class _)) = deresolve_import sym
    1.16 +          | print_import (sym, (_, Code_Thingol.Classinst _)) = NONE;
    1.17          val import_ps = import_common_ps @ map (print_qualified_import o fst) imports;
    1.18          fun print_stmt' sym = case Code_Symbol.Graph.get_node gr sym
    1.19           of (_, NONE) => NONE
    1.20            | (_, SOME (export, stmt)) =>
    1.21 -              SOME (if export then print_import (sym, stmt) else NONE, markup_stmt sym (print_stmt deresolve (sym, stmt)));
    1.22 +              SOME (if Code_Namespace.not_private export then print_import (sym, (export, stmt)) else NONE, markup_stmt sym (print_stmt deresolve (sym, stmt)));
    1.23          val (export_ps, body_ps) = (flat o rev o Code_Symbol.Graph.strong_conn) gr
    1.24            |> map_filter print_stmt'
    1.25            |> split_list
     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 @@ -242,7 +242,7 @@
     2.4                @@ print_dicttyp (class, tyco `%% map (ITyVar o fst) vs)
     2.5              ))
     2.6            end;
     2.7 -    fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
     2.8 +    fun print_stmt _ (ML_Exc (const, (vs_ty, n))) = pair
     2.9            [print_val_decl print_typscheme (Constant const, vs_ty)]
    2.10            ((semicolon o map str) (
    2.11              (if n = 0 then "val" else "fun")
    2.12 @@ -253,14 +253,14 @@
    2.13              :: "Fail"
    2.14              @@ ML_Syntax.print_string const
    2.15            ))
    2.16 -      | print_stmt (ML_Val binding) =
    2.17 +      | print_stmt _ (ML_Val binding) =
    2.18            let
    2.19              val (sig_p, p) = print_def (K false) true "val" binding
    2.20            in pair
    2.21              [sig_p]
    2.22              (semicolon [p])
    2.23            end
    2.24 -      | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
    2.25 +      | print_stmt _ (ML_Funs (binding :: bindings, pseudo_funs)) =
    2.26            let
    2.27              val print_def' = print_def (member (op =) pseudo_funs) false;
    2.28              fun print_pseudo_fun sym = concat [
    2.29 @@ -277,24 +277,28 @@
    2.30              sig_ps
    2.31              (Pretty.chunks (ps @ semicolon [p] :: pseudo_ps))
    2.32            end
    2.33 -     | print_stmt (ML_Datas [(tyco, (vs, []))]) =
    2.34 +     | print_stmt _ (ML_Datas [(tyco, (vs, []))]) =
    2.35            let
    2.36              val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
    2.37            in
    2.38              pair
    2.39              [concat [str "type", ty_p]]
    2.40 -            (concat [str "datatype", ty_p, str "=", str "EMPTY__"])
    2.41 +            (semicolon [str "datatype", ty_p, str "=", str "EMPTY__"])
    2.42            end
    2.43 -     | print_stmt (ML_Datas (data :: datas)) = 
    2.44 +     | print_stmt export (ML_Datas (data :: datas)) = 
    2.45            let
    2.46 -            val sig_ps = print_datatype_decl "datatype" data
    2.47 +            val decl_ps = print_datatype_decl "datatype" data
    2.48                :: map (print_datatype_decl "and") datas;
    2.49 -            val (ps, p) = split_last sig_ps;
    2.50 +            val (ps, p) = split_last decl_ps;
    2.51            in pair
    2.52 -            sig_ps
    2.53 +            (if Code_Namespace.is_public export
    2.54 +              then decl_ps
    2.55 +              else map (fn (tyco, (vs, _)) =>
    2.56 +                concat [str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)])
    2.57 +                (data :: datas))
    2.58              (Pretty.chunks (ps @| semicolon [p]))
    2.59            end
    2.60 -     | print_stmt (ML_Class (class, (v, (classrels, classparams)))) =
    2.61 +     | print_stmt export (ML_Class (class, (v, (classrels, classparams)))) =
    2.62            let
    2.63              fun print_field s p = concat [str s, str ":", p];
    2.64              fun print_proj s p = semicolon
    2.65 @@ -317,12 +321,14 @@
    2.66                  (print_typscheme ([(v, [class])], ty));
    2.67            in pair
    2.68              (concat [str "type", print_dicttyp (class, ITyVar v)]
    2.69 -              :: map print_super_class_decl classrels
    2.70 -              @ map print_classparam_decl classparams)
    2.71 +              :: (if Code_Namespace.is_public export
    2.72 +                 then map print_super_class_decl classrels
    2.73 +                   @ map print_classparam_decl classparams
    2.74 +                 else []))
    2.75              (Pretty.chunks (
    2.76                concat [
    2.77 -                str ("type '" ^ v),
    2.78 -                (str o deresolve_class) class,
    2.79 +                str "type",
    2.80 +                print_dicttyp (class, ITyVar v),
    2.81                  str "=",
    2.82                  enum "," "{" "};" (
    2.83                    map print_super_class_field classrels
    2.84 @@ -582,7 +588,7 @@
    2.85                ]
    2.86              ))
    2.87            end;
    2.88 -     fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
    2.89 +     fun print_stmt _ (ML_Exc (const, (vs_ty, n))) = pair
    2.90            [print_val_decl print_typscheme (Constant const, vs_ty)]
    2.91            ((doublesemicolon o map str) (
    2.92              "let"
    2.93 @@ -592,14 +598,14 @@
    2.94              :: "failwith"
    2.95              @@ ML_Syntax.print_string const
    2.96            ))
    2.97 -      | print_stmt (ML_Val binding) =
    2.98 +      | print_stmt _ (ML_Val binding) =
    2.99            let
   2.100              val (sig_p, p) = print_def (K false) true "let" binding
   2.101            in pair
   2.102              [sig_p]
   2.103              (doublesemicolon [p])
   2.104            end
   2.105 -      | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
   2.106 +      | print_stmt _ (ML_Funs (binding :: bindings, pseudo_funs)) =
   2.107            let
   2.108              val print_def' = print_def (member (op =) pseudo_funs) false;
   2.109              fun print_pseudo_fun sym = concat [
   2.110 @@ -616,24 +622,28 @@
   2.111              sig_ps
   2.112              (Pretty.chunks (ps @ doublesemicolon [p] :: pseudo_ps))
   2.113            end
   2.114 -     | print_stmt (ML_Datas [(tyco, (vs, []))]) =
   2.115 +     | print_stmt _ (ML_Datas [(tyco, (vs, []))]) =
   2.116            let
   2.117              val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
   2.118            in
   2.119              pair
   2.120              [concat [str "type", ty_p]]
   2.121 -            (concat [str "type", ty_p, str "=", str "EMPTY__"])
   2.122 +            (doublesemicolon [str "type", ty_p, str "=", str "EMPTY__"])
   2.123            end
   2.124 -     | print_stmt (ML_Datas (data :: datas)) = 
   2.125 +     | print_stmt export (ML_Datas (data :: datas)) = 
   2.126            let
   2.127 -            val sig_ps = print_datatype_decl "type" data
   2.128 +            val decl_ps = print_datatype_decl "type" data
   2.129                :: map (print_datatype_decl "and") datas;
   2.130 -            val (ps, p) = split_last sig_ps;
   2.131 +            val (ps, p) = split_last decl_ps;
   2.132            in pair
   2.133 -            sig_ps
   2.134 +            (if Code_Namespace.is_public export
   2.135 +              then decl_ps
   2.136 +              else map (fn (tyco, (vs, _)) =>
   2.137 +                concat [str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)])
   2.138 +                (data :: datas))
   2.139              (Pretty.chunks (ps @| doublesemicolon [p]))
   2.140            end
   2.141 -     | print_stmt (ML_Class (class, (v, (classrels, classparams)))) =
   2.142 +     | print_stmt export (ML_Class (class, (v, (classrels, classparams)))) =
   2.143            let
   2.144              fun print_field s p = concat [str s, str ":", p];
   2.145              fun print_super_class_field (classrel as (_, super_class)) =
   2.146 @@ -705,7 +715,7 @@
   2.147  
   2.148  (** SML/OCaml generic part **)
   2.149  
   2.150 -fun ml_program_of_program ctxt module_name reserved identifiers program =
   2.151 +fun ml_program_of_program ctxt module_name reserved identifiers =
   2.152    let
   2.153      fun namify_const upper base (nsp_const, nsp_type) =
   2.154        let
   2.155 @@ -782,7 +792,7 @@
   2.156      Code_Namespace.hierarchical_program ctxt {
   2.157        module_name = module_name, reserved = reserved, identifiers = identifiers,
   2.158        empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,
   2.159 -      cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
   2.160 +      cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts }
   2.161    end;
   2.162  
   2.163  fun serialize_ml print_ml_module print_ml_stmt ctxt
   2.164 @@ -792,13 +802,14 @@
   2.165  
   2.166      (* build program *)
   2.167      val { deresolver, hierarchical_program = ml_program } =
   2.168 -      ml_program_of_program ctxt module_name (Name.make_context reserved_syms) identifiers program;
   2.169 +      ml_program_of_program ctxt module_name (Name.make_context reserved_syms)
   2.170 +        identifiers program;
   2.171  
   2.172      (* print statements *)
   2.173      fun print_stmt prefix_fragments (_, (export, stmt)) = print_ml_stmt
   2.174        tyco_syntax const_syntax (make_vars reserved_syms)
   2.175 -      (Code_Thingol.is_constr program) (deresolver prefix_fragments) stmt
   2.176 -      |> apfst (fn decl => if export then SOME decl else NONE);
   2.177 +      (Code_Thingol.is_constr program) (deresolver prefix_fragments) export stmt
   2.178 +      |> apfst (fn decl => if Code_Namespace.not_private export then SOME decl else NONE);
   2.179  
   2.180      (* print modules *)
   2.181      fun print_module _ base _ xs =
     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 @@ -6,6 +6,10 @@
     3.4  
     3.5  signature CODE_NAMESPACE =
     3.6  sig
     3.7 +  datatype export = Private | Opaque | Public
     3.8 +  val is_public: export -> bool
     3.9 +  val not_private: export -> bool
    3.10 +
    3.11    type flat_program
    3.12    val flat_program: Proof.context
    3.13      -> { module_prefix: string, module_name: string,
    3.14 @@ -18,7 +22,7 @@
    3.15  
    3.16    datatype ('a, 'b) node =
    3.17        Dummy
    3.18 -    | Stmt of bool * 'a
    3.19 +    | Stmt of export * 'a
    3.20      | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T)
    3.21    type ('a, 'b) hierarchical_program
    3.22    val hierarchical_program: Proof.context
    3.23 @@ -32,7 +36,7 @@
    3.24        -> { deresolver: string list -> Code_Symbol.T -> string,
    3.25             hierarchical_program: ('a, 'b) hierarchical_program }
    3.26    val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c,
    3.27 -    print_stmt: string list -> Code_Symbol.T * (bool * 'a) -> 'c,
    3.28 +    print_stmt: string list -> Code_Symbol.T * (export * 'a) -> 'c,
    3.29      lift_markup: (Pretty.T -> Pretty.T) -> 'c -> 'c }
    3.30        -> ('a, 'b) hierarchical_program -> 'c list
    3.31  end;
    3.32 @@ -40,6 +44,18 @@
    3.33  structure Code_Namespace : CODE_NAMESPACE =
    3.34  struct
    3.35  
    3.36 +(** export **)
    3.37 +
    3.38 +datatype export = Private | Opaque | Public;
    3.39 +
    3.40 +fun is_public Public = true
    3.41 +  | is_public _ = false;
    3.42 +
    3.43 +fun not_private Public = true
    3.44 +  | not_private Opaque = true
    3.45 +  | not_private _ = false;
    3.46 +
    3.47 +
    3.48  (** fundamental module name hierarchy **)
    3.49  
    3.50  fun module_fragments' { identifiers, reserved } name =
    3.51 @@ -82,7 +98,7 @@
    3.52  
    3.53  (** flat program structure **)
    3.54  
    3.55 -type flat_program = ((string * (bool * Code_Thingol.stmt) option) Code_Symbol.Graph.T * (string * Code_Symbol.T list) list) Graph.T;
    3.56 +type flat_program = ((string * (export * Code_Thingol.stmt) option) Code_Symbol.Graph.T * (string * Code_Symbol.T list) list) Graph.T;
    3.57  
    3.58  fun flat_program ctxt { module_prefix, module_name, reserved,
    3.59      identifiers, empty_nsp, namify_stmt, modify_stmt } program =
    3.60 @@ -103,7 +119,7 @@
    3.61        in
    3.62          Graph.default_node (module_name, (Code_Symbol.Graph.empty, []))
    3.63          #> (Graph.map_node module_name o apfst)
    3.64 -          (Code_Symbol.Graph.new_node (sym, (base, (true, stmt))))
    3.65 +          (Code_Symbol.Graph.new_node (sym, (base, (Public, stmt))))
    3.66        end;
    3.67      fun add_dep sym sym' =
    3.68        let
    3.69 @@ -166,7 +182,7 @@
    3.70  
    3.71  datatype ('a, 'b) node =
    3.72      Dummy
    3.73 -  | Stmt of bool * 'a
    3.74 +  | Stmt of export * 'a
    3.75    | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T);
    3.76  
    3.77  type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Code_Symbol.Graph.T;
    3.78 @@ -230,7 +246,7 @@
    3.79          val (name_fragments, base) = prep_sym sym;
    3.80        in
    3.81          (map_module name_fragments o apsnd)
    3.82 -          (Code_Symbol.Graph.new_node (sym, (base, Stmt (true, stmt))))
    3.83 +          (Code_Symbol.Graph.new_node (sym, (base, Stmt (Public, stmt))))
    3.84        end;
    3.85      fun add_edge_acyclic_error error_msg dep gr =
    3.86        Code_Symbol.Graph.add_edge_acyclic dep gr
     4.1 --- a/src/Tools/Code/code_scala.ML	Sun Feb 23 10:33:43 2014 +0100
     4.2 +++ b/src/Tools/Code/code_scala.ML	Sun Feb 23 10:33:43 2014 +0100
     4.3 @@ -145,8 +145,11 @@
     4.4              |> single
     4.5              |> enclose "(" ")"
     4.6            end;
     4.7 -    fun privatize false = concat o cons (str "private")
     4.8 -      | privatize true = concat;
     4.9 +    fun privatize Code_Namespace.Public = concat
    4.10 +      | privatize _ = concat o cons (str "private");
    4.11 +    fun privatize' Code_Namespace.Public = concat
    4.12 +      | privatize' Code_Namespace.Opaque = concat
    4.13 +      | privatize' _ = concat o cons (str "private");
    4.14      fun print_context tyvars vs sym = applify "[" "]"
    4.15        (fn (v, sort) => (Pretty.block o map str)
    4.16          (lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class class]) sort))
    4.17 @@ -224,7 +227,7 @@
    4.18                ];
    4.19            in
    4.20              Pretty.chunks (applify "[" "]" (str o lookup_tyvar tyvars)
    4.21 -              NOBR ((privatize export o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs
    4.22 +              NOBR ((privatize' export o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs
    4.23                  :: map print_co cos)
    4.24            end
    4.25        | print_stmt (Type_Class class, (export, Code_Thingol.Class (v, (classrels, classparams)))) =
    4.26 @@ -257,7 +260,7 @@
    4.27            in
    4.28              Pretty.chunks (
    4.29                (Pretty.block_enclose
    4.30 -                (privatize export ([str "trait", (add_typarg o deresolve_class) class]
    4.31 +                (privatize' export ([str "trait", (add_typarg o deresolve_class) class]
    4.32                    @ the_list (print_super_classes classrels) @ [str "{"]), str "}")
    4.33                  (map print_classparam_val classparams))
    4.34                :: map print_classparam_def classparams
    4.35 @@ -349,7 +352,8 @@
    4.36  
    4.37      (* build program *)
    4.38      val { deresolver, hierarchical_program = scala_program } =
    4.39 -      scala_program_of_program ctxt module_name (Name.make_context reserved_syms) identifiers program;
    4.40 +      scala_program_of_program ctxt module_name (Name.make_context reserved_syms)
    4.41 +        identifiers program;
    4.42  
    4.43      (* print statements *)
    4.44      fun lookup_constr tyco constr = case Code_Symbol.Graph.get_node program (Type_Constructor tyco)