src/Tools/Code/code_namespace.ML
changeset 39017 8cd5b6d688fa
parent 38970 53d1ee3d98b8
child 39018 5681d7cfabce
equal deleted inserted replaced
38971:5d49165a192e 39017:8cd5b6d688fa
     4 Mastering target language namespaces.
     4 Mastering target language namespaces.
     5 *)
     5 *)
     6 
     6 
     7 signature CODE_NAMESPACE =
     7 signature CODE_NAMESPACE =
     8 sig
     8 sig
     9   datatype 'a node =
     9   datatype ('a, 'b) node =
    10       Dummy
    10       Dummy
    11     | Stmt of Code_Thingol.stmt
    11     | Stmt of 'a
    12     | Module of ('a * (string * 'a node) Graph.T);
    12     | Module of ('b * (string * ('a, 'b) node) Graph.T);
    13   val hierarchical_program: (string -> string) -> { module_alias: string -> string option,
    13   val hierarchical_program: (string -> string) -> { module_alias: string -> string option,
    14     reserved: Name.context, empty_nsp: 'b, namify_module: string -> 'b -> string * 'b,
    14     reserved: Name.context, empty_nsp: 'a, namify_module: string -> 'a -> string * 'a,
    15     namify_stmt: Code_Thingol.stmt -> string -> 'b -> string * 'b,
    15     namify_stmt: Code_Thingol.stmt -> string -> 'a -> string * 'a,
    16     cyclic_modules: bool, empty_data: 'a, memorize_data: string -> 'a -> 'a }
    16     cyclic_modules: bool, empty_data: 'b, memorize_data: string -> 'b -> 'b }
    17       -> Code_Thingol.program
    17       -> Code_Thingol.program
    18       -> { deresolver: string list -> string -> string,
    18       -> { deresolver: string list -> string -> string,
    19            hierarchical_program: (string * 'a node) Graph.T }
    19            hierarchical_program: (string * (Code_Thingol.stmt, 'b) node) Graph.T }
    20 end;
    20 end;
    21 
    21 
    22 structure Code_Namespace : CODE_NAMESPACE =
    22 structure Code_Namespace : CODE_NAMESPACE =
    23 struct
    23 struct
    24 
    24 
    25 (* hierarchical program structure *)
    25 (* hierarchical program structure *)
    26 
    26 
    27 datatype 'a node =
    27 datatype ('a, 'b) node =
    28     Dummy
    28     Dummy
    29   | Stmt of Code_Thingol.stmt
    29   | Stmt of 'a
    30   | Module of ('a * (string * 'a node) Graph.T);
    30   | Module of ('b * (string * ('a, 'b) node) Graph.T);
    31 
    31 
    32 fun hierarchical_program labelled_name { module_alias, reserved, empty_nsp,
    32 fun hierarchical_program labelled_name { module_alias, reserved, empty_nsp,
    33       namify_module, namify_stmt, cyclic_modules, empty_data, memorize_data } program =
    33       namify_module, namify_stmt, cyclic_modules, empty_data, memorize_data } program =
    34   let
    34   let
    35 
    35