src/Tools/Code/code_namespace.ML
changeset 55681 7714287dc044
parent 55680 bc5edc5dbf18
child 55683 5732a55b9232
     1.1 --- a/src/Tools/Code/code_namespace.ML	Sun Feb 23 10:33:43 2014 +0100
     1.2 +++ b/src/Tools/Code/code_namespace.ML	Sun Feb 23 10:33:43 2014 +0100
     1.3 @@ -6,6 +6,10 @@
     1.4  
     1.5  signature CODE_NAMESPACE =
     1.6  sig
     1.7 +  datatype export = Private | Opaque | Public
     1.8 +  val is_public: export -> bool
     1.9 +  val not_private: export -> bool
    1.10 +
    1.11    type flat_program
    1.12    val flat_program: Proof.context
    1.13      -> { module_prefix: string, module_name: string,
    1.14 @@ -18,7 +22,7 @@
    1.15  
    1.16    datatype ('a, 'b) node =
    1.17        Dummy
    1.18 -    | Stmt of bool * 'a
    1.19 +    | Stmt of export * 'a
    1.20      | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T)
    1.21    type ('a, 'b) hierarchical_program
    1.22    val hierarchical_program: Proof.context
    1.23 @@ -32,7 +36,7 @@
    1.24        -> { deresolver: string list -> Code_Symbol.T -> string,
    1.25             hierarchical_program: ('a, 'b) hierarchical_program }
    1.26    val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c,
    1.27 -    print_stmt: string list -> Code_Symbol.T * (bool * 'a) -> 'c,
    1.28 +    print_stmt: string list -> Code_Symbol.T * (export * 'a) -> 'c,
    1.29      lift_markup: (Pretty.T -> Pretty.T) -> 'c -> 'c }
    1.30        -> ('a, 'b) hierarchical_program -> 'c list
    1.31  end;
    1.32 @@ -40,6 +44,18 @@
    1.33  structure Code_Namespace : CODE_NAMESPACE =
    1.34  struct
    1.35  
    1.36 +(** export **)
    1.37 +
    1.38 +datatype export = Private | Opaque | Public;
    1.39 +
    1.40 +fun is_public Public = true
    1.41 +  | is_public _ = false;
    1.42 +
    1.43 +fun not_private Public = true
    1.44 +  | not_private Opaque = true
    1.45 +  | not_private _ = false;
    1.46 +
    1.47 +
    1.48  (** fundamental module name hierarchy **)
    1.49  
    1.50  fun module_fragments' { identifiers, reserved } name =
    1.51 @@ -82,7 +98,7 @@
    1.52  
    1.53  (** flat program structure **)
    1.54  
    1.55 -type flat_program = ((string * (bool * Code_Thingol.stmt) option) Code_Symbol.Graph.T * (string * Code_Symbol.T list) list) Graph.T;
    1.56 +type flat_program = ((string * (export * Code_Thingol.stmt) option) Code_Symbol.Graph.T * (string * Code_Symbol.T list) list) Graph.T;
    1.57  
    1.58  fun flat_program ctxt { module_prefix, module_name, reserved,
    1.59      identifiers, empty_nsp, namify_stmt, modify_stmt } program =
    1.60 @@ -103,7 +119,7 @@
    1.61        in
    1.62          Graph.default_node (module_name, (Code_Symbol.Graph.empty, []))
    1.63          #> (Graph.map_node module_name o apfst)
    1.64 -          (Code_Symbol.Graph.new_node (sym, (base, (true, stmt))))
    1.65 +          (Code_Symbol.Graph.new_node (sym, (base, (Public, stmt))))
    1.66        end;
    1.67      fun add_dep sym sym' =
    1.68        let
    1.69 @@ -166,7 +182,7 @@
    1.70  
    1.71  datatype ('a, 'b) node =
    1.72      Dummy
    1.73 -  | Stmt of bool * 'a
    1.74 +  | Stmt of export * 'a
    1.75    | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T);
    1.76  
    1.77  type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Code_Symbol.Graph.T;
    1.78 @@ -230,7 +246,7 @@
    1.79          val (name_fragments, base) = prep_sym sym;
    1.80        in
    1.81          (map_module name_fragments o apsnd)
    1.82 -          (Code_Symbol.Graph.new_node (sym, (base, Stmt (true, stmt))))
    1.83 +          (Code_Symbol.Graph.new_node (sym, (base, Stmt (Public, stmt))))
    1.84        end;
    1.85      fun add_edge_acyclic_error error_msg dep gr =
    1.86        Code_Symbol.Graph.add_edge_acyclic dep gr