src/Tools/Code/code_namespace.ML
author haftmann
Sat, 28 Jun 2014 22:13:20 +0200
changeset 57428 47c8475e7864
parent 56826 ba18bd41e510
child 58520 a4d1f8041af0
permissions -rw-r--r--
corrected handled exception
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
     1
(*  Title:      Tools/Code/code_namespace.ML
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
     2
    Author:     Florian Haftmann, TU Muenchen
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
     3
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
     4
Mastering target language namespaces.
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
     5
*)
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
     6
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
     7
signature CODE_NAMESPACE =
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
     8
sig
55681
7714287dc044 more fine-grain notion of export
haftmann
parents: 55680
diff changeset
     9
  datatype export = Private | Opaque | Public
7714287dc044 more fine-grain notion of export
haftmann
parents: 55680
diff changeset
    10
  val is_public: export -> bool
7714287dc044 more fine-grain notion of export
haftmann
parents: 55680
diff changeset
    11
  val not_private: export -> bool
55684
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    12
  val join_exports: export list -> export
55681
7714287dc044 more fine-grain notion of export
haftmann
parents: 55680
diff changeset
    13
39208
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
    14
  type flat_program
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
    15
  val flat_program: Proof.context
52138
e21426f244aa bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents: 51930
diff changeset
    16
    -> { module_prefix: string, module_name: string,
e21426f244aa bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents: 51930
diff changeset
    17
    reserved: Name.context, identifiers: Code_Target.identifier_data, empty_nsp: 'a,
39208
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
    18
    namify_stmt: Code_Thingol.stmt -> string -> 'a -> string * 'a,
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
    19
    modify_stmt: Code_Thingol.stmt -> Code_Thingol.stmt option }
55683
5732a55b9232 explicit option for "open" code generation
haftmann
parents: 55681
diff changeset
    20
      -> Code_Symbol.T list -> Code_Thingol.program
55150
0940309ed8f1 less clumsy namespace
haftmann
parents: 55147
diff changeset
    21
      -> { deresolver: string -> Code_Symbol.T -> string,
39208
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
    22
           flat_program: flat_program }
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
    23
39017
8cd5b6d688fa generalized hierarchical data structure over statements
haftmann
parents: 38970
diff changeset
    24
  datatype ('a, 'b) node =
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
    25
      Dummy
55681
7714287dc044 more fine-grain notion of export
haftmann
parents: 55680
diff changeset
    26
    | Stmt of export * 'a
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
    27
    | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T)
39208
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
    28
  type ('a, 'b) hierarchical_program
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
    29
  val hierarchical_program: Proof.context
52138
e21426f244aa bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents: 51930
diff changeset
    30
    -> { module_name: string,
e21426f244aa bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents: 51930
diff changeset
    31
    reserved: Name.context, identifiers: Code_Target.identifier_data,
e21426f244aa bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents: 51930
diff changeset
    32
    empty_nsp: 'c, namify_module: string -> 'c -> string * 'c,
39022
ac7774a35bcf explicit modify_stmt parameter
haftmann
parents: 39018
diff changeset
    33
    namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c,
55684
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    34
    cyclic_modules: bool,
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    35
    class_transitive: bool, class_relation_public: bool,
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    36
    empty_data: 'b, memorize_data: Code_Symbol.T -> 'b -> 'b,
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    37
    modify_stmts: (Code_Symbol.T * (export * Code_Thingol.stmt)) list -> (export * 'a) option list }
55683
5732a55b9232 explicit option for "open" code generation
haftmann
parents: 55681
diff changeset
    38
      -> Code_Symbol.T list -> Code_Thingol.program
55150
0940309ed8f1 less clumsy namespace
haftmann
parents: 55147
diff changeset
    39
      -> { deresolver: string list -> Code_Symbol.T -> string,
39147
3c284a152bd6 printing combinator for hierarchical programs
haftmann
parents: 39055
diff changeset
    40
           hierarchical_program: ('a, 'b) hierarchical_program }
3c284a152bd6 printing combinator for hierarchical programs
haftmann
parents: 39055
diff changeset
    41
  val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c,
55681
7714287dc044 more fine-grain notion of export
haftmann
parents: 55680
diff changeset
    42
    print_stmt: string list -> Code_Symbol.T * (export * 'a) -> 'c,
39147
3c284a152bd6 printing combinator for hierarchical programs
haftmann
parents: 39055
diff changeset
    43
    lift_markup: (Pretty.T -> Pretty.T) -> 'c -> 'c }
3c284a152bd6 printing combinator for hierarchical programs
haftmann
parents: 39055
diff changeset
    44
      -> ('a, 'b) hierarchical_program -> 'c list
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
    45
end;
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
    46
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
    47
structure Code_Namespace : CODE_NAMESPACE =
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
    48
struct
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
    49
55681
7714287dc044 more fine-grain notion of export
haftmann
parents: 55680
diff changeset
    50
(** export **)
7714287dc044 more fine-grain notion of export
haftmann
parents: 55680
diff changeset
    51
7714287dc044 more fine-grain notion of export
haftmann
parents: 55680
diff changeset
    52
datatype export = Private | Opaque | Public;
7714287dc044 more fine-grain notion of export
haftmann
parents: 55680
diff changeset
    53
7714287dc044 more fine-grain notion of export
haftmann
parents: 55680
diff changeset
    54
fun is_public Public = true
7714287dc044 more fine-grain notion of export
haftmann
parents: 55680
diff changeset
    55
  | is_public _ = false;
7714287dc044 more fine-grain notion of export
haftmann
parents: 55680
diff changeset
    56
7714287dc044 more fine-grain notion of export
haftmann
parents: 55680
diff changeset
    57
fun not_private Public = true
7714287dc044 more fine-grain notion of export
haftmann
parents: 55680
diff changeset
    58
  | not_private Opaque = true
7714287dc044 more fine-grain notion of export
haftmann
parents: 55680
diff changeset
    59
  | not_private _ = false;
7714287dc044 more fine-grain notion of export
haftmann
parents: 55680
diff changeset
    60
55684
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    61
fun mark_export Public _ = Public
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    62
  | mark_export _ Public = Public
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    63
  | mark_export Opaque _ = Opaque
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    64
  | mark_export _ Opaque = Opaque
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    65
  | mark_export _ _ = Private;
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    66
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    67
fun join_exports exports = fold mark_export exports Private;
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    68
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    69
fun dependent_exports { program = program, class_transitive = class_transitive } =
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    70
  let
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    71
    fun is_datatype_or_class (Code_Symbol.Type_Constructor _) = true
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    72
      | is_datatype_or_class (Code_Symbol.Type_Class _) = true
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    73
      | is_datatype_or_class _ = false;
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    74
    fun is_relevant (Code_Symbol.Class_Relation _) = true
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    75
      | is_relevant sym = is_datatype_or_class sym;
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    76
    val proto_gr = Code_Symbol.Graph.restrict is_relevant program;
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    77
    val gr =
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    78
      proto_gr
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    79
      |> Code_Symbol.Graph.fold
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    80
          (fn (sym, (_, (_, deps))) =>
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    81
            if is_relevant sym
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    82
            then I
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    83
            else
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    84
              Code_Symbol.Graph.new_node (sym, Code_Thingol.NoStmt)
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    85
              #> Code_Symbol.Graph.Keys.fold
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    86
               (fn sym' =>
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    87
                if is_relevant sym'
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    88
                then Code_Symbol.Graph.add_edge (sym, sym')
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    89
                else I) deps) program
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    90
      |> class_transitive ?
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    91
          Code_Symbol.Graph.fold (fn (sym as Code_Symbol.Type_Class _, _) =>
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    92
            fold (curry Code_Symbol.Graph.add_edge sym)
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    93
              ((remove (op =) sym o Code_Symbol.Graph.all_succs proto_gr) [sym]) | _ => I) proto_gr
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    94
    fun deps_of sym =
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    95
      let
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    96
        val succs = Code_Symbol.Graph.Keys.dest o Code_Symbol.Graph.imm_succs gr;
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    97
        val deps1 = succs sym;
55776
7dd1971b39c1 amended some slips, rolling back currently dysfunctional export minimimalisation for Scala
haftmann
parents: 55684
diff changeset
    98
        val deps2 = [] |> fold (union (op =)) (map succs deps1) |> subtract (op =) deps1
55684
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
    99
      in (deps1, deps2) end;
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   100
  in
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   101
    { is_datatype_or_class = is_datatype_or_class,
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   102
      deps_of = deps_of }
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   103
  end;
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   104
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   105
fun mark_exports_aux { program = program, prefix_of = prefix_of, map_export = map_export,
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   106
    is_datatype_or_class = is_datatype_or_class, deps_of = deps_of,
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   107
    class_relation_public = class_relation_public } prefix sym =
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   108
  let
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   109
    val export = (if is_datatype_or_class sym then Opaque else Public);
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   110
    val (dependent_export1, dependent_export2) =
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   111
      case Code_Symbol.Graph.get_node program sym of
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   112
          Code_Thingol.Fun _ => (SOME Opaque, NONE)
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   113
        | Code_Thingol.Classinst _ => (SOME Opaque, NONE)
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   114
        | Code_Thingol.Datatypecons _ => (SOME Public, SOME Opaque)
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   115
        | Code_Thingol.Classparam _ => (SOME Public, SOME Opaque)
55776
7dd1971b39c1 amended some slips, rolling back currently dysfunctional export minimimalisation for Scala
haftmann
parents: 55684
diff changeset
   116
        | Code_Thingol.Class _ => (SOME Opaque, NONE)
55684
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   117
        | Code_Thingol.Classrel _ =>
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   118
           (if class_relation_public
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   119
            then (SOME Public, SOME Opaque)
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   120
            else (SOME Opaque, NONE))
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   121
        | _ => (NONE, NONE);
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   122
    val dependent_exports =
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   123
      case dependent_export1 of
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   124
        SOME export1 => (case dependent_export2 of
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   125
          SOME export2 =>
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   126
            let
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   127
              val (deps1, deps2) = deps_of sym
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   128
            in map (rpair export1) deps1 @ map (rpair export2) deps2 end
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   129
        | NONE => map (rpair export1) (fst (deps_of sym)))
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   130
      | NONE => [];
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   131
  in 
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   132
    map_export prefix sym (mark_export export)
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   133
    #> fold (fn (sym, export) => map_export (prefix_of sym) sym (mark_export export))
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   134
      dependent_exports
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   135
  end;
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   136
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   137
fun mark_exports { program = program, prefix_of = prefix_of, map_export = map_export,
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   138
    class_transitive = class_transitive, class_relation_public = class_relation_public } =
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   139
  let
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   140
    val { is_datatype_or_class, deps_of } =
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   141
      dependent_exports { program = program, class_transitive = class_transitive };
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   142
  in
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   143
    mark_exports_aux { program = program, prefix_of = prefix_of, map_export = map_export,
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   144
      is_datatype_or_class = is_datatype_or_class, deps_of = deps_of,
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   145
      class_relation_public = class_relation_public }
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   146
  end;
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   147
55681
7714287dc044 more fine-grain notion of export
haftmann
parents: 55680
diff changeset
   148
52138
e21426f244aa bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents: 51930
diff changeset
   149
(** fundamental module name hierarchy **)
e21426f244aa bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents: 51930
diff changeset
   150
55291
82780e5f7622 tuned storage of code identifiers
haftmann
parents: 55150
diff changeset
   151
fun module_fragments' { identifiers, reserved } name =
82780e5f7622 tuned storage of code identifiers
haftmann
parents: 55150
diff changeset
   152
  case Code_Symbol.lookup_module_data identifiers name of
82780e5f7622 tuned storage of code identifiers
haftmann
parents: 55150
diff changeset
   153
      SOME (fragments, _) => fragments
82780e5f7622 tuned storage of code identifiers
haftmann
parents: 55150
diff changeset
   154
    | NONE => map (fn fragment => fst (Name.variant fragment reserved)) (Long_Name.explode name);
82780e5f7622 tuned storage of code identifiers
haftmann
parents: 55150
diff changeset
   155
82780e5f7622 tuned storage of code identifiers
haftmann
parents: 55150
diff changeset
   156
fun module_fragments { module_name, identifiers, reserved } =
82780e5f7622 tuned storage of code identifiers
haftmann
parents: 55150
diff changeset
   157
  if module_name = ""
82780e5f7622 tuned storage of code identifiers
haftmann
parents: 55150
diff changeset
   158
  then module_fragments' { identifiers = identifiers, reserved = reserved }
82780e5f7622 tuned storage of code identifiers
haftmann
parents: 55150
diff changeset
   159
  else K (Long_Name.explode module_name);
39055
81e0368812ad removed namespace stuff from code_printer
haftmann
parents: 39029
diff changeset
   160
56826
ba18bd41e510 enforce case of identifiers only to accomodate strict language requirements (or clear separation of constructors from variables in the case of SML)
haftmann
parents: 55776
diff changeset
   161
fun build_module_namespace ctxt enforce_upper { module_prefix, module_name, identifiers, reserved } program =
55291
82780e5f7622 tuned storage of code identifiers
haftmann
parents: 55150
diff changeset
   162
  let
82780e5f7622 tuned storage of code identifiers
haftmann
parents: 55150
diff changeset
   163
    val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program [];
82780e5f7622 tuned storage of code identifiers
haftmann
parents: 55150
diff changeset
   164
    val module_fragments' = module_fragments
82780e5f7622 tuned storage of code identifiers
haftmann
parents: 55150
diff changeset
   165
      { module_name = module_name, identifiers = identifiers, reserved = reserved };
56826
ba18bd41e510 enforce case of identifiers only to accomodate strict language requirements (or clear separation of constructors from variables in the case of SML)
haftmann
parents: 55776
diff changeset
   166
    val adjust_case = if enforce_upper then map (Name.enforce_case true) else I;
55291
82780e5f7622 tuned storage of code identifiers
haftmann
parents: 55150
diff changeset
   167
  in
56826
ba18bd41e510 enforce case of identifiers only to accomodate strict language requirements (or clear separation of constructors from variables in the case of SML)
haftmann
parents: 55776
diff changeset
   168
    fold (fn name => Symtab.update (name, adjust_case (Long_Name.explode module_prefix @ module_fragments' name)))
55291
82780e5f7622 tuned storage of code identifiers
haftmann
parents: 55150
diff changeset
   169
      module_names Symtab.empty
82780e5f7622 tuned storage of code identifiers
haftmann
parents: 55150
diff changeset
   170
  end;
82780e5f7622 tuned storage of code identifiers
haftmann
parents: 55150
diff changeset
   171
55292
haftmann
parents: 55291
diff changeset
   172
fun prep_symbol ctxt { module_namespace, force_module, identifiers } sym =
55291
82780e5f7622 tuned storage of code identifiers
haftmann
parents: 55150
diff changeset
   173
  case Code_Symbol.lookup identifiers sym of
55292
haftmann
parents: 55291
diff changeset
   174
      NONE => ((the o Symtab.lookup module_namespace o Code_Symbol.default_prefix ctxt) sym,
haftmann
parents: 55291
diff changeset
   175
        Code_Symbol.default_base sym)
53414
dd64696d267a explicit module names have precedence over identifier declarations
haftmann
parents: 52138
diff changeset
   176
    | SOME prefix_name => if null force_module then prefix_name
dd64696d267a explicit module names have precedence over identifier declarations
haftmann
parents: 52138
diff changeset
   177
        else (force_module, snd prefix_name);
39055
81e0368812ad removed namespace stuff from code_printer
haftmann
parents: 39029
diff changeset
   178
55293
42cf5802d36a code generation: explicitly declared identifiers gain predence over implicit ones
haftmann
parents: 55292
diff changeset
   179
fun has_priority identifiers = is_some o Code_Symbol.lookup identifiers;
42cf5802d36a code generation: explicitly declared identifiers gain predence over implicit ones
haftmann
parents: 55292
diff changeset
   180
55292
haftmann
parents: 55291
diff changeset
   181
fun build_proto_program { empty, add_stmt, add_dep } program =
haftmann
parents: 55291
diff changeset
   182
  empty
haftmann
parents: 55291
diff changeset
   183
  |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program
haftmann
parents: 55291
diff changeset
   184
  |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) =>
haftmann
parents: 55291
diff changeset
   185
      Code_Symbol.Graph.Keys.fold (add_dep sym) syms) program;
haftmann
parents: 55291
diff changeset
   186
55293
42cf5802d36a code generation: explicitly declared identifiers gain predence over implicit ones
haftmann
parents: 55292
diff changeset
   187
fun prioritize has_priority = uncurry append o List.partition has_priority;
42cf5802d36a code generation: explicitly declared identifiers gain predence over implicit ones
haftmann
parents: 55292
diff changeset
   188
39055
81e0368812ad removed namespace stuff from code_printer
haftmann
parents: 39029
diff changeset
   189
39208
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   190
(** flat program structure **)
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   191
55681
7714287dc044 more fine-grain notion of export
haftmann
parents: 55680
diff changeset
   192
type flat_program = ((string * (export * Code_Thingol.stmt) option) Code_Symbol.Graph.T * (string * Code_Symbol.T list) list) Graph.T;
39208
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   193
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   194
fun flat_program ctxt { module_prefix, module_name, reserved,
55683
5732a55b9232 explicit option for "open" code generation
haftmann
parents: 55681
diff changeset
   195
    identifiers, empty_nsp, namify_stmt, modify_stmt } exports program =
39208
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   196
  let
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   197
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   198
    (* building module name hierarchy *)
56826
ba18bd41e510 enforce case of identifiers only to accomodate strict language requirements (or clear separation of constructors from variables in the case of SML)
haftmann
parents: 55776
diff changeset
   199
    val module_namespace = build_module_namespace ctxt true { module_prefix = module_prefix,
55291
82780e5f7622 tuned storage of code identifiers
haftmann
parents: 55150
diff changeset
   200
      module_name = module_name, identifiers = identifiers, reserved = reserved } program;
55292
haftmann
parents: 55291
diff changeset
   201
    val prep_sym = prep_symbol ctxt { module_namespace = module_namespace,
haftmann
parents: 55291
diff changeset
   202
      force_module = Long_Name.explode module_name, identifiers = identifiers }
52138
e21426f244aa bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents: 51930
diff changeset
   203
      #>> Long_Name.implode;
55293
42cf5802d36a code generation: explicitly declared identifiers gain predence over implicit ones
haftmann
parents: 55292
diff changeset
   204
    val sym_priority = has_priority identifiers;
39208
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   205
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   206
    (* distribute statements over hierarchy *)
55684
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   207
    val mark_exports = mark_exports { program = program, prefix_of = fst o prep_sym,
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   208
      map_export = fn module_name => fn sym =>
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   209
        Graph.map_node module_name o apfst o Code_Symbol.Graph.map_node sym o apsnd o apfst,
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   210
        class_transitive = false, class_relation_public = false };
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   211
    fun add_stmt sym stmt =
39208
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   212
      let
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   213
        val (module_name, base) = prep_sym sym;
39208
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   214
      in
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   215
        Graph.default_node (module_name, (Code_Symbol.Graph.empty, []))
55680
haftmann
parents: 55679
diff changeset
   216
        #> (Graph.map_node module_name o apfst)
55684
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   217
          (Code_Symbol.Graph.new_node (sym, (base, (if null exports then Public else Private, stmt))))
39208
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   218
      end;
55292
haftmann
parents: 55291
diff changeset
   219
    fun add_dep sym sym' =
39208
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   220
      let
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   221
        val (module_name, _) = prep_sym sym;
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   222
        val (module_name', _) = prep_sym sym';
39208
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   223
      in if module_name = module_name'
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   224
        then (Graph.map_node module_name o apfst) (Code_Symbol.Graph.add_edge (sym, sym'))
55680
haftmann
parents: 55679
diff changeset
   225
        else (Graph.map_node module_name o apsnd)
haftmann
parents: 55679
diff changeset
   226
          (AList.map_default (op =) (module_name', []) (insert (op =) sym'))
55684
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   227
          #> mark_exports module_name' sym'
39208
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   228
      end;
55292
haftmann
parents: 55291
diff changeset
   229
    val proto_program = build_proto_program
55684
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   230
      { empty = Graph.empty, add_stmt = add_stmt, add_dep = add_dep } program
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   231
      |> fold (fn sym => mark_exports ((fst o prep_sym) sym) sym) exports;
39208
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   232
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   233
    (* name declarations and statement modifications *)
55679
59244fc1a7ca formal markup for public ingredients
haftmann
parents: 55605
diff changeset
   234
    fun declare sym (base, (_, stmt)) (gr, nsp) = 
39208
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   235
      let
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   236
        val (base', nsp') = namify_stmt stmt base nsp;
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   237
        val gr' = (Code_Symbol.Graph.map_node sym o apfst) (K base') gr;
39208
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   238
      in (gr', nsp') end;
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   239
    fun declarations gr = (gr, empty_nsp)
55293
42cf5802d36a code generation: explicitly declared identifiers gain predence over implicit ones
haftmann
parents: 55292
diff changeset
   240
      |> fold (fn sym => declare sym (Code_Symbol.Graph.get_node gr sym))
42cf5802d36a code generation: explicitly declared identifiers gain predence over implicit ones
haftmann
parents: 55292
diff changeset
   241
          (prioritize sym_priority (Code_Symbol.Graph.keys gr))
39208
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   242
      |> fst
55680
haftmann
parents: 55679
diff changeset
   243
      |> Code_Symbol.Graph.map_strong_conn (fn syms_bases_exports_stmts =>
haftmann
parents: 55679
diff changeset
   244
        map snd syms_bases_exports_stmts
haftmann
parents: 55679
diff changeset
   245
        |> (map o apsnd) (fn (export, stmt) => Option.map (pair export) (modify_stmt stmt)));
39208
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   246
    val flat_program = proto_program
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   247
      |> (Graph.map o K o apfst) declarations;
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   248
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   249
    (* qualified and unqualified imports, deresolving *)
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   250
    fun base_deresolver sym = fst (Code_Symbol.Graph.get_node
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   251
      (fst (Graph.get_node flat_program (fst (prep_sym sym)))) sym);
39208
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   252
    fun classify_names gr imports =
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   253
      let
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   254
        val import_tab = maps
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   255
          (fn (module_name, syms) => map (rpair module_name) syms) imports;
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   256
        val imported_syms = map fst import_tab;
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   257
        val here_syms = Code_Symbol.Graph.keys gr;
39208
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   258
      in
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   259
        Code_Symbol.Table.empty
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   260
        |> fold (fn sym => Code_Symbol.Table.update (sym, base_deresolver sym)) here_syms
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   261
        |> fold (fn sym => Code_Symbol.Table.update (sym,
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   262
            Long_Name.append (the (AList.lookup (op =) import_tab sym))
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   263
              (base_deresolver sym))) imported_syms
39208
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   264
      end;
40630
haftmann
parents: 40629
diff changeset
   265
    val deresolver_tab = Symtab.make (AList.make
haftmann
parents: 40629
diff changeset
   266
      (uncurry classify_names o Graph.get_node flat_program)
haftmann
parents: 40629
diff changeset
   267
        (Graph.keys flat_program));
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   268
    fun deresolver "" sym =
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   269
          Long_Name.append (fst (prep_sym sym)) (base_deresolver sym)
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   270
      | deresolver module_name sym =
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   271
          the (Code_Symbol.Table.lookup (the (Symtab.lookup deresolver_tab module_name)) sym)
52138
e21426f244aa bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents: 51930
diff changeset
   272
          handle Option.Option => error ("Unknown statement name: "
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   273
            ^ Code_Symbol.quote ctxt sym);
39208
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   274
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   275
  in { deresolver = deresolver, flat_program = flat_program } end;
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   276
fc1e02735438 added flat_program; tuned signature
haftmann
parents: 39203
diff changeset
   277
39055
81e0368812ad removed namespace stuff from code_printer
haftmann
parents: 39029
diff changeset
   278
(** hierarchical program structure **)
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   279
39017
8cd5b6d688fa generalized hierarchical data structure over statements
haftmann
parents: 38970
diff changeset
   280
datatype ('a, 'b) node =
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   281
    Dummy
55681
7714287dc044 more fine-grain notion of export
haftmann
parents: 55680
diff changeset
   282
  | Stmt of export * 'a
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   283
  | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T);
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   284
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   285
type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Code_Symbol.Graph.T;
39147
3c284a152bd6 printing combinator for hierarchical programs
haftmann
parents: 39055
diff changeset
   286
55679
59244fc1a7ca formal markup for public ingredients
haftmann
parents: 55605
diff changeset
   287
fun the_stmt (Stmt (export, stmt)) = (export, stmt);
59244fc1a7ca formal markup for public ingredients
haftmann
parents: 55605
diff changeset
   288
39018
haftmann
parents: 39017
diff changeset
   289
fun map_module_content f (Module content) = Module (f content);
haftmann
parents: 39017
diff changeset
   290
haftmann
parents: 39017
diff changeset
   291
fun map_module [] = I
haftmann
parents: 39017
diff changeset
   292
  | map_module (name_fragment :: name_fragments) =
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   293
      apsnd o Code_Symbol.Graph.map_node (Code_Symbol.Module name_fragment) o apsnd o map_module_content
39018
haftmann
parents: 39017
diff changeset
   294
        o map_module name_fragments;
haftmann
parents: 39017
diff changeset
   295
55680
haftmann
parents: 55679
diff changeset
   296
fun map_module_stmts f_module f_stmts sym_base_nodes =
haftmann
parents: 55679
diff changeset
   297
  let
haftmann
parents: 55679
diff changeset
   298
    val some_modules =
haftmann
parents: 55679
diff changeset
   299
      sym_base_nodes
55684
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   300
      |> map (fn (_, (base, Module content)) => SOME (base, content) | _ => NONE)
55680
haftmann
parents: 55679
diff changeset
   301
      |> (burrow_options o map o apsnd) f_module;
haftmann
parents: 55679
diff changeset
   302
    val some_export_stmts =
haftmann
parents: 55679
diff changeset
   303
      sym_base_nodes
haftmann
parents: 55679
diff changeset
   304
      |> map (fn (sym, (base, Stmt export_stmt)) => SOME ((sym, export_stmt), base) | _ => NONE)
haftmann
parents: 55679
diff changeset
   305
      |> (burrow_options o burrow_fst) (fn [] => [] | xs => f_stmts xs)
haftmann
parents: 55679
diff changeset
   306
  in
haftmann
parents: 55679
diff changeset
   307
    map2 (fn SOME (base, content) => (K (base, Module content))
haftmann
parents: 55679
diff changeset
   308
      | NONE => fn SOME (some_export_stmt, base) =>
haftmann
parents: 55679
diff changeset
   309
          (base, case some_export_stmt of SOME export_stmt => Stmt export_stmt | NONE => Dummy))
haftmann
parents: 55679
diff changeset
   310
      some_modules some_export_stmts
haftmann
parents: 55679
diff changeset
   311
  end;
haftmann
parents: 55679
diff changeset
   312
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   313
fun hierarchical_program ctxt { module_name, reserved, identifiers, empty_nsp,
55684
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   314
      namify_module, namify_stmt, cyclic_modules,
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   315
      class_transitive, class_relation_public,
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   316
      empty_data, memorize_data, modify_stmts }
55683
5732a55b9232 explicit option for "open" code generation
haftmann
parents: 55681
diff changeset
   317
      exports program =
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   318
  let
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   319
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   320
    (* building module name hierarchy *)
56826
ba18bd41e510 enforce case of identifiers only to accomodate strict language requirements (or clear separation of constructors from variables in the case of SML)
haftmann
parents: 55776
diff changeset
   321
    val module_namespace = build_module_namespace ctxt false { module_prefix = "",
55291
82780e5f7622 tuned storage of code identifiers
haftmann
parents: 55150
diff changeset
   322
      module_name = module_name, identifiers = identifiers, reserved = reserved } program;
55292
haftmann
parents: 55291
diff changeset
   323
    val prep_sym = prep_symbol ctxt { module_namespace = module_namespace,
55293
42cf5802d36a code generation: explicitly declared identifiers gain predence over implicit ones
haftmann
parents: 55292
diff changeset
   324
      force_module = Long_Name.explode module_name, identifiers = identifiers }
42cf5802d36a code generation: explicitly declared identifiers gain predence over implicit ones
haftmann
parents: 55292
diff changeset
   325
    val sym_priority = has_priority identifiers;
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   326
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   327
    (* building empty module hierarchy *)
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   328
    val empty_module = (empty_data, Code_Symbol.Graph.empty);
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   329
    fun ensure_module name_fragment (data, nodes) =
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   330
      if can (Code_Symbol.Graph.get_node nodes) (Code_Symbol.Module name_fragment) then (data, nodes)
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   331
      else (data,
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   332
        nodes |> Code_Symbol.Graph.new_node (Code_Symbol.Module name_fragment, (name_fragment, Module empty_module)));
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   333
    fun allocate_module [] = I
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   334
      | allocate_module (name_fragment :: name_fragments) =
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   335
          ensure_module name_fragment
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   336
          #> (apsnd o Code_Symbol.Graph.map_node (Code_Symbol.Module name_fragment) o apsnd o map_module_content o allocate_module) name_fragments;
52138
e21426f244aa bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents: 51930
diff changeset
   337
    val empty_program =
e21426f244aa bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents: 51930
diff changeset
   338
      empty_module
55291
82780e5f7622 tuned storage of code identifiers
haftmann
parents: 55150
diff changeset
   339
      |> Symtab.fold (fn (_, fragments) => allocate_module fragments) module_namespace
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   340
      |> Code_Symbol.Graph.fold (allocate_module o these o Option.map fst
55291
82780e5f7622 tuned storage of code identifiers
haftmann
parents: 55150
diff changeset
   341
          o Code_Symbol.lookup identifiers o fst) program;
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   342
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   343
    (* distribute statements over hierarchy *)
55684
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   344
    val mark_exports = mark_exports { program = program, prefix_of = fst o prep_sym,
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   345
      map_export = fn name_fragments => fn sym => fn f =>
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   346
        (map_module name_fragments o apsnd o Code_Symbol.Graph.map_node sym o apsnd)
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   347
          (fn Stmt (export, stmt) => Stmt (f export, stmt)),
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   348
      class_transitive = class_transitive, class_relation_public = class_relation_public };
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   349
    fun add_stmt sym stmt =
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   350
      let
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   351
        val (name_fragments, base) = prep_sym sym;
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   352
      in
55680
haftmann
parents: 55679
diff changeset
   353
        (map_module name_fragments o apsnd)
55684
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   354
          (Code_Symbol.Graph.new_node (sym, (base, Stmt (if null exports then Public else Private, stmt))))
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   355
      end;
55680
haftmann
parents: 55679
diff changeset
   356
    fun add_edge_acyclic_error error_msg dep gr =
haftmann
parents: 55679
diff changeset
   357
      Code_Symbol.Graph.add_edge_acyclic dep gr
57428
47c8475e7864 corrected handled exception
haftmann
parents: 56826
diff changeset
   358
        handle Code_Symbol.Graph.CYCLES _ => error (error_msg ())
55292
haftmann
parents: 55291
diff changeset
   359
    fun add_dep sym sym' =
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   360
      let
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   361
        val (name_fragments, _) = prep_sym sym;
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   362
        val (name_fragments', _) = prep_sym sym';
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   363
        val (name_fragments_common, (diff, diff')) =
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   364
          chop_prefix (op =) (name_fragments, name_fragments');
55680
haftmann
parents: 55679
diff changeset
   365
        val is_cross_module = not (null diff andalso null diff');
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   366
        val dep = pairself hd (map Code_Symbol.Module diff @ [sym], map Code_Symbol.Module diff' @ [sym']);
55680
haftmann
parents: 55679
diff changeset
   367
        val add_edge = if is_cross_module andalso not cyclic_modules
haftmann
parents: 55679
diff changeset
   368
          then add_edge_acyclic_error (fn _ => "Dependency "
haftmann
parents: 55679
diff changeset
   369
            ^ Code_Symbol.quote ctxt sym ^ " -> "
haftmann
parents: 55679
diff changeset
   370
            ^ Code_Symbol.quote ctxt sym'
haftmann
parents: 55679
diff changeset
   371
            ^ " would result in module dependency cycle") dep
haftmann
parents: 55679
diff changeset
   372
          else Code_Symbol.Graph.add_edge dep;
55684
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   373
      in
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   374
        (map_module name_fragments_common o apsnd) add_edge
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   375
        #> (if is_cross_module then mark_exports name_fragments' sym' else I)
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   376
      end;
55292
haftmann
parents: 55291
diff changeset
   377
    val proto_program = build_proto_program
55684
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   378
      { empty = empty_program, add_stmt = add_stmt, add_dep = add_dep } program
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   379
      |> fold (fn sym => mark_exports ((fst o prep_sym) sym) sym) exports;
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   380
39022
ac7774a35bcf explicit modify_stmt parameter
haftmann
parents: 39018
diff changeset
   381
    (* name declarations, data and statement modifications *)
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   382
    fun make_declarations nsps (data, nodes) =
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   383
      let
55293
42cf5802d36a code generation: explicitly declared identifiers gain predence over implicit ones
haftmann
parents: 55292
diff changeset
   384
        val (module_fragments, stmt_syms) =
42cf5802d36a code generation: explicitly declared identifiers gain predence over implicit ones
haftmann
parents: 55292
diff changeset
   385
          Code_Symbol.Graph.keys nodes
42cf5802d36a code generation: explicitly declared identifiers gain predence over implicit ones
haftmann
parents: 55292
diff changeset
   386
          |> List.partition
42cf5802d36a code generation: explicitly declared identifiers gain predence over implicit ones
haftmann
parents: 55292
diff changeset
   387
              (fn sym => case Code_Symbol.Graph.get_node nodes sym
42cf5802d36a code generation: explicitly declared identifiers gain predence over implicit ones
haftmann
parents: 55292
diff changeset
   388
                of (_, Module _) => true | _ => false)
42cf5802d36a code generation: explicitly declared identifiers gain predence over implicit ones
haftmann
parents: 55292
diff changeset
   389
          |> pairself (prioritize sym_priority)
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   390
        fun declare namify sym (nsps, nodes) =
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   391
          let
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   392
            val (base, node) = Code_Symbol.Graph.get_node nodes sym;
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   393
            val (base', nsps') = namify node base nsps;
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   394
            val nodes' = Code_Symbol.Graph.map_node sym (K (base', node)) nodes;
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   395
          in (nsps', nodes') end;
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   396
        val (nsps', nodes') = (nsps, nodes)
39022
ac7774a35bcf explicit modify_stmt parameter
haftmann
parents: 39018
diff changeset
   397
          |> fold (declare (K namify_module)) module_fragments
55679
59244fc1a7ca formal markup for public ingredients
haftmann
parents: 55605
diff changeset
   398
          |> fold (declare (namify_stmt o snd o the_stmt)) stmt_syms;
55680
haftmann
parents: 55679
diff changeset
   399
        fun modify_stmts' syms_stmts =
55605
haftmann
parents: 55293
diff changeset
   400
          let
55680
haftmann
parents: 55679
diff changeset
   401
            val stmts' = modify_stmts syms_stmts
haftmann
parents: 55679
diff changeset
   402
          in stmts' @ replicate (length syms_stmts - length stmts') NONE end;
haftmann
parents: 55679
diff changeset
   403
        val nodes'' =
haftmann
parents: 55679
diff changeset
   404
          nodes'
55684
ee49b4f7edc8 keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents: 55683
diff changeset
   405
          |> Code_Symbol.Graph.map_strong_conn (map_module_stmts (make_declarations nsps') modify_stmts');
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   406
        val data' = fold memorize_data stmt_syms data;
39018
haftmann
parents: 39017
diff changeset
   407
      in (data', nodes'') end;
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   408
    val (_, hierarchical_program) = make_declarations empty_nsp proto_program;
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   409
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   410
    (* deresolving *)
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   411
    fun deresolver prefix_fragments sym =
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   412
      let
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   413
        val (name_fragments, _) = prep_sym sym;
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   414
        val (_, (_, remainder)) = chop_prefix (op =) (prefix_fragments, name_fragments);
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   415
        val nodes = fold (fn name_fragment => fn nodes => case Code_Symbol.Graph.get_node nodes (Code_Symbol.Module name_fragment)
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   416
         of (_, Module (_, nodes)) => nodes) name_fragments hierarchical_program;
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   417
        val (base', _) = Code_Symbol.Graph.get_node nodes sym;
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   418
      in Long_Name.implode (remainder @ [base']) end
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   419
        handle Code_Symbol.Graph.UNDEF _ => error ("Unknown statement name: "
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   420
          ^ Code_Symbol.quote ctxt sym);
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   421
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   422
  in { deresolver = deresolver, hierarchical_program = hierarchical_program } end;
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
diff changeset
   423
39147
3c284a152bd6 printing combinator for hierarchical programs
haftmann
parents: 39055
diff changeset
   424
fun print_hierarchical { print_module, print_stmt, lift_markup } =
3c284a152bd6 printing combinator for hierarchical programs
haftmann
parents: 39055
diff changeset
   425
  let
3c284a152bd6 printing combinator for hierarchical programs
haftmann
parents: 39055
diff changeset
   426
    fun print_node _ (_, Dummy) =
3c284a152bd6 printing combinator for hierarchical programs
haftmann
parents: 39055
diff changeset
   427
          NONE
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   428
      | print_node prefix_fragments (sym, Stmt stmt) =
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   429
          SOME (lift_markup (Code_Printer.markup_stmt sym)
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   430
            (print_stmt prefix_fragments (sym, stmt)))
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   431
      | print_node prefix_fragments (Code_Symbol.Module name_fragment, Module (data, nodes)) =
39147
3c284a152bd6 printing combinator for hierarchical programs
haftmann
parents: 39055
diff changeset
   432
          let
3c284a152bd6 printing combinator for hierarchical programs
haftmann
parents: 39055
diff changeset
   433
            val prefix_fragments' = prefix_fragments @ [name_fragment]
3c284a152bd6 printing combinator for hierarchical programs
haftmann
parents: 39055
diff changeset
   434
          in
3c284a152bd6 printing combinator for hierarchical programs
haftmann
parents: 39055
diff changeset
   435
            Option.map (print_module prefix_fragments'
3c284a152bd6 printing combinator for hierarchical programs
haftmann
parents: 39055
diff changeset
   436
              name_fragment data) (print_nodes prefix_fragments' nodes)
3c284a152bd6 printing combinator for hierarchical programs
haftmann
parents: 39055
diff changeset
   437
          end
3c284a152bd6 printing combinator for hierarchical programs
haftmann
parents: 39055
diff changeset
   438
    and print_nodes prefix_fragments nodes =
3c284a152bd6 printing combinator for hierarchical programs
haftmann
parents: 39055
diff changeset
   439
      let
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   440
        val xs = (map_filter (fn sym => print_node prefix_fragments
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   441
          (sym, snd (Code_Symbol.Graph.get_node nodes sym))) o rev o flat o Code_Symbol.Graph.strong_conn) nodes
39147
3c284a152bd6 printing combinator for hierarchical programs
haftmann
parents: 39055
diff changeset
   442
      in if null xs then NONE else SOME xs end;
3c284a152bd6 printing combinator for hierarchical programs
haftmann
parents: 39055
diff changeset
   443
  in these o print_nodes [] end;
3c284a152bd6 printing combinator for hierarchical programs
haftmann
parents: 39055
diff changeset
   444
55147
bce3dbc11f95 prefer explicit code symbol type over ad-hoc name mangling
haftmann
parents: 53414
diff changeset
   445
end;