1(* Title: Tools/Code/code_namespace.ML 2 Author: Florian Haftmann, TU Muenchen 3 4Mastering target language namespaces. 5*) 6 7signature CODE_NAMESPACE = 8sig 9 val variant_case_insensitive: string -> Name.context -> string * Name.context 10 11 datatype export = Private | Opaque | Public 12 val is_public: export -> bool 13 val not_private: export -> bool 14 val join_exports: export list -> export 15 16 type flat_program 17 val flat_program: Proof.context 18 -> { module_prefix: string, module_name: string, 19 reserved: Name.context, identifiers: Code_Printer.identifiers, empty_nsp: 'a, 20 namify_stmt: Code_Thingol.stmt -> string -> 'a -> string * 'a, 21 modify_stmt: Code_Thingol.stmt -> Code_Thingol.stmt option } 22 -> Code_Symbol.T list -> Code_Thingol.program 23 -> { deresolver: string -> Code_Symbol.T -> string, 24 flat_program: flat_program } 25 26 datatype ('a, 'b) node = 27 Dummy 28 | Stmt of export * 'a 29 | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T) 30 type ('a, 'b) hierarchical_program 31 val hierarchical_program: Proof.context 32 -> { module_name: string, 33 reserved: Name.context, identifiers: Code_Printer.identifiers, 34 empty_nsp: 'c, namify_module: string -> 'c -> string * 'c, 35 namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c, 36 cyclic_modules: bool, 37 class_transitive: bool, class_relation_public: bool, 38 empty_data: 'b, memorize_data: Code_Symbol.T -> 'b -> 'b, 39 modify_stmts: (Code_Symbol.T * (export * Code_Thingol.stmt)) list -> (export * 'a) option list } 40 -> Code_Symbol.T list -> Code_Thingol.program 41 -> { deresolver: string list -> Code_Symbol.T -> string, 42 hierarchical_program: ('a, 'b) hierarchical_program } 43 val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c, 44 print_stmt: string list -> Code_Symbol.T * (export * 'a) -> 'c, 45 lift_markup: (Pretty.T -> Pretty.T) -> 'c -> 'c } 46 -> ('a, 'b) hierarchical_program -> 'c list 47end; 48 49structure Code_Namespace : CODE_NAMESPACE = 50struct 51 52(** name handling on case-insensitive file systems **) 53 54fun restore_for cs = 55 if forall Symbol.is_ascii_upper cs then map Symbol.to_ascii_upper 56 else if Symbol.is_ascii_upper (nth cs 0) then nth_map 0 Symbol.to_ascii_upper 57 else I; 58 59fun variant_case_insensitive s ctxt = 60 let 61 val cs = Symbol.explode s; 62 val s_lower = implode (map Symbol.to_ascii_lower cs); 63 val restore = implode o restore_for cs o Symbol.explode; 64 in 65 ctxt 66 |> Name.variant s_lower 67 |>> restore 68 end; 69 70 71(** export **) 72 73datatype export = Private | Opaque | Public; 74 75fun is_public Public = true 76 | is_public _ = false; 77 78fun not_private Public = true 79 | not_private Opaque = true 80 | not_private _ = false; 81 82fun mark_export Public _ = Public 83 | mark_export _ Public = Public 84 | mark_export Opaque _ = Opaque 85 | mark_export _ Opaque = Opaque 86 | mark_export _ _ = Private; 87 88fun join_exports exports = fold mark_export exports Private; 89 90fun dependent_exports { program = program, class_transitive = class_transitive } = 91 let 92 fun is_datatype_or_class (Code_Symbol.Type_Constructor _) = true 93 | is_datatype_or_class (Code_Symbol.Type_Class _) = true 94 | is_datatype_or_class _ = false; 95 fun is_relevant (Code_Symbol.Class_Relation _) = true 96 | is_relevant sym = is_datatype_or_class sym; 97 val proto_gr = Code_Symbol.Graph.restrict is_relevant program; 98 val gr = 99 proto_gr 100 |> Code_Symbol.Graph.fold 101 (fn (sym, (_, (_, deps))) => 102 if is_relevant sym 103 then I 104 else 105 Code_Symbol.Graph.new_node (sym, Code_Thingol.NoStmt) 106 #> Code_Symbol.Graph.Keys.fold 107 (fn sym' => 108 if is_relevant sym' 109 then Code_Symbol.Graph.add_edge (sym, sym') 110 else I) deps) program 111 |> class_transitive ? 112 Code_Symbol.Graph.fold (fn (sym as Code_Symbol.Type_Class _, _) => 113 fold (curry Code_Symbol.Graph.add_edge sym) 114 ((remove (op =) sym o Code_Symbol.Graph.all_succs proto_gr) [sym]) | _ => I) proto_gr 115 fun deps_of sym = 116 let 117 val succs = Code_Symbol.Graph.Keys.dest o Code_Symbol.Graph.imm_succs gr; 118 val deps1 = succs sym; 119 val deps2 = [] |> fold (union (op =)) (map succs deps1) |> subtract (op =) deps1 120 in (deps1, deps2) end; 121 in 122 { is_datatype_or_class = is_datatype_or_class, 123 deps_of = deps_of } 124 end; 125 126fun mark_exports_aux { program = program, prefix_of = prefix_of, map_export = map_export, 127 is_datatype_or_class = is_datatype_or_class, deps_of = deps_of, 128 class_relation_public = class_relation_public } prefix sym = 129 let 130 val export = (if is_datatype_or_class sym then Opaque else Public); 131 val (dependent_export1, dependent_export2) = 132 case Code_Symbol.Graph.get_node program sym of 133 Code_Thingol.Fun _ => (SOME Opaque, NONE) 134 | Code_Thingol.Classinst _ => (SOME Opaque, NONE) 135 | Code_Thingol.Datatypecons _ => (SOME Public, SOME Opaque) 136 | Code_Thingol.Classparam _ => (SOME Public, SOME Opaque) 137 | Code_Thingol.Class _ => (SOME Opaque, NONE) 138 | Code_Thingol.Classrel _ => 139 (if class_relation_public 140 then (SOME Public, SOME Opaque) 141 else (SOME Opaque, NONE)) 142 | _ => (NONE, NONE); 143 val dependent_exports = 144 case dependent_export1 of 145 SOME export1 => (case dependent_export2 of 146 SOME export2 => 147 let 148 val (deps1, deps2) = deps_of sym 149 in map (rpair export1) deps1 @ map (rpair export2) deps2 end 150 | NONE => map (rpair export1) (fst (deps_of sym))) 151 | NONE => []; 152 in 153 map_export prefix sym (mark_export export) 154 #> fold (fn (sym, export) => map_export (prefix_of sym) sym (mark_export export)) 155 dependent_exports 156 end; 157 158fun mark_exports { program = program, prefix_of = prefix_of, map_export = map_export, 159 class_transitive = class_transitive, class_relation_public = class_relation_public } = 160 let 161 val { is_datatype_or_class, deps_of } = 162 dependent_exports { program = program, class_transitive = class_transitive }; 163 in 164 mark_exports_aux { program = program, prefix_of = prefix_of, map_export = map_export, 165 is_datatype_or_class = is_datatype_or_class, deps_of = deps_of, 166 class_relation_public = class_relation_public } 167 end; 168 169 170(** fundamental module name hierarchy **) 171 172fun module_fragments' { identifiers, reserved } name = 173 case Code_Symbol.lookup_module_data identifiers name of 174 SOME (fragments, _) => fragments 175 | NONE => map (fn fragment => fst (Name.variant fragment reserved)) (Long_Name.explode name); 176 177fun module_fragments { module_name, identifiers, reserved } = 178 if module_name = "" 179 then module_fragments' { identifiers = identifiers, reserved = reserved } 180 else K (Long_Name.explode module_name); 181 182fun build_module_namespace ctxt enforce_upper { module_prefix, module_name, identifiers, reserved } program = 183 let 184 val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program []; 185 val module_fragments' = module_fragments 186 { module_name = module_name, identifiers = identifiers, reserved = reserved }; 187 val adjust_case = if enforce_upper then map (Name.enforce_case true) else I; 188 in 189 fold (fn name => Symtab.update (name, adjust_case (Long_Name.explode module_prefix @ module_fragments' name))) 190 module_names Symtab.empty 191 end; 192 193fun prep_symbol ctxt { module_namespace, force_module, identifiers } sym = 194 case Code_Symbol.lookup identifiers sym of 195 NONE => ((the o Symtab.lookup module_namespace o Code_Symbol.default_prefix ctxt) sym, 196 Code_Symbol.default_base sym) 197 | SOME prefix_name => if null force_module then prefix_name 198 else (force_module, snd prefix_name); 199 200fun has_priority identifiers = is_some o Code_Symbol.lookup identifiers; 201 202fun build_proto_program { empty, add_stmt, add_dep } program = 203 empty 204 |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program 205 |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) => 206 Code_Symbol.Graph.Keys.fold (add_dep sym) syms) program; 207 208fun prioritize has_priority = uncurry append o List.partition has_priority; 209 210 211(** flat program structure **) 212 213type flat_program = ((string * (export * Code_Thingol.stmt) option) Code_Symbol.Graph.T * (string * Code_Symbol.T list) list) Graph.T; 214 215fun flat_program ctxt { module_prefix, module_name, reserved, 216 identifiers, empty_nsp, namify_stmt, modify_stmt } exports program = 217 let 218 219 (* building module name hierarchy *) 220 val module_namespace = build_module_namespace ctxt true { module_prefix = module_prefix, 221 module_name = module_name, identifiers = identifiers, reserved = reserved } program; 222 val prep_sym = prep_symbol ctxt { module_namespace = module_namespace, 223 force_module = Long_Name.explode module_name, identifiers = identifiers } 224 #>> Long_Name.implode; 225 val sym_priority = has_priority identifiers; 226 227 (* distribute statements over hierarchy *) 228 val mark_exports = mark_exports { program = program, prefix_of = fst o prep_sym, 229 map_export = fn module_name => fn sym => 230 Graph.map_node module_name o apfst o Code_Symbol.Graph.map_node sym o apsnd o apfst, 231 class_transitive = false, class_relation_public = false }; 232 fun add_stmt sym stmt = 233 let 234 val (module_name, base) = prep_sym sym; 235 in 236 Graph.default_node (module_name, (Code_Symbol.Graph.empty, [])) 237 #> (Graph.map_node module_name o apfst) 238 (Code_Symbol.Graph.new_node (sym, (base, (if null exports then Public else Private, stmt)))) 239 end; 240 fun add_dep sym sym' = 241 let 242 val (module_name, _) = prep_sym sym; 243 val (module_name', _) = prep_sym sym'; 244 in if module_name = module_name' 245 then (Graph.map_node module_name o apfst) (Code_Symbol.Graph.add_edge (sym, sym')) 246 else (Graph.map_node module_name o apsnd) 247 (AList.map_default (op =) (module_name', []) (insert (op =) sym')) 248 #> mark_exports module_name' sym' 249 end; 250 val proto_program = build_proto_program 251 { empty = Graph.empty, add_stmt = add_stmt, add_dep = add_dep } program 252 |> fold (fn sym => mark_exports ((fst o prep_sym) sym) sym) exports; 253 254 (* name declarations and statement modifications *) 255 fun declare sym (base, (_, stmt)) (gr, nsp) = 256 let 257 val (base', nsp') = namify_stmt stmt base nsp; 258 val gr' = (Code_Symbol.Graph.map_node sym o apfst) (K base') gr; 259 in (gr', nsp') end; 260 fun declarations gr = (gr, empty_nsp) 261 |> fold (fn sym => declare sym (Code_Symbol.Graph.get_node gr sym)) 262 (prioritize sym_priority (Code_Symbol.Graph.keys gr)) 263 |> fst 264 |> Code_Symbol.Graph.map_strong_conn (fn syms_bases_exports_stmts => 265 map snd syms_bases_exports_stmts 266 |> (map o apsnd) (fn (export, stmt) => Option.map (pair export) (modify_stmt stmt))); 267 val flat_program = proto_program 268 |> (Graph.map o K o apfst) declarations; 269 270 (* qualified and unqualified imports, deresolving *) 271 fun base_deresolver sym = fst (Code_Symbol.Graph.get_node 272 (fst (Graph.get_node flat_program (fst (prep_sym sym)))) sym); 273 fun classify_names gr imports = 274 let 275 val import_tab = maps 276 (fn (module_name, syms) => map (rpair module_name) syms) imports; 277 val imported_syms = map fst import_tab; 278 val here_syms = Code_Symbol.Graph.keys gr; 279 in 280 Code_Symbol.Table.empty 281 |> fold (fn sym => Code_Symbol.Table.update (sym, base_deresolver sym)) here_syms 282 |> fold (fn sym => Code_Symbol.Table.update (sym, 283 Long_Name.append (the (AList.lookup (op =) import_tab sym)) 284 (base_deresolver sym))) imported_syms 285 end; 286 val deresolver_tab = Symtab.make (AList.make 287 (uncurry classify_names o Graph.get_node flat_program) 288 (Graph.keys flat_program)); 289 fun deresolver "" sym = 290 Long_Name.append (fst (prep_sym sym)) (base_deresolver sym) 291 | deresolver module_name sym = 292 the (Code_Symbol.Table.lookup (the (Symtab.lookup deresolver_tab module_name)) sym) 293 handle Option.Option => error ("Unknown statement name: " 294 ^ Code_Symbol.quote ctxt sym); 295 296 in { deresolver = deresolver, flat_program = flat_program } end; 297 298 299(** hierarchical program structure **) 300 301datatype ('a, 'b) node = 302 Dummy 303 | Stmt of export * 'a 304 | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T); 305 306type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Code_Symbol.Graph.T; 307 308fun the_stmt (Stmt (export, stmt)) = (export, stmt); 309 310fun map_module_content f (Module content) = Module (f content); 311 312fun map_module [] = I 313 | map_module (name_fragment :: name_fragments) = 314 apsnd o Code_Symbol.Graph.map_node (Code_Symbol.Module name_fragment) o apsnd o map_module_content 315 o map_module name_fragments; 316 317fun map_module_stmts f_module f_stmts sym_base_nodes = 318 let 319 val some_modules = 320 sym_base_nodes 321 |> map (fn (_, (base, Module content)) => SOME (base, content) | _ => NONE) 322 |> (burrow_options o map o apsnd) f_module; 323 val some_export_stmts = 324 sym_base_nodes 325 |> map (fn (sym, (base, Stmt export_stmt)) => SOME ((sym, export_stmt), base) | _ => NONE) 326 |> (burrow_options o burrow_fst) (fn [] => [] | xs => f_stmts xs) 327 in 328 map2 (fn SOME (base, content) => (K (base, Module content)) 329 | NONE => fn SOME (some_export_stmt, base) => 330 (base, case some_export_stmt of SOME export_stmt => Stmt export_stmt | NONE => Dummy)) 331 some_modules some_export_stmts 332 end; 333 334fun hierarchical_program ctxt { module_name, reserved, identifiers, empty_nsp, 335 namify_module, namify_stmt, cyclic_modules, 336 class_transitive, class_relation_public, 337 empty_data, memorize_data, modify_stmts } 338 exports program = 339 let 340 341 (* building module name hierarchy *) 342 val module_namespace = build_module_namespace ctxt false { module_prefix = "", 343 module_name = module_name, identifiers = identifiers, reserved = reserved } program; 344 val prep_sym = prep_symbol ctxt { module_namespace = module_namespace, 345 force_module = Long_Name.explode module_name, identifiers = identifiers } 346 val sym_priority = has_priority identifiers; 347 348 (* building empty module hierarchy *) 349 val empty_module = (empty_data, Code_Symbol.Graph.empty); 350 fun ensure_module name_fragment (data, nodes) = 351 if can (Code_Symbol.Graph.get_node nodes) (Code_Symbol.Module name_fragment) then (data, nodes) 352 else (data, 353 nodes |> Code_Symbol.Graph.new_node (Code_Symbol.Module name_fragment, (name_fragment, Module empty_module))); 354 fun allocate_module [] = I 355 | allocate_module (name_fragment :: name_fragments) = 356 ensure_module name_fragment 357 #> (apsnd o Code_Symbol.Graph.map_node (Code_Symbol.Module name_fragment) o apsnd o map_module_content o allocate_module) name_fragments; 358 val empty_program = 359 empty_module 360 |> Symtab.fold (fn (_, fragments) => allocate_module fragments) module_namespace 361 |> Code_Symbol.Graph.fold (allocate_module o these o Option.map fst 362 o Code_Symbol.lookup identifiers o fst) program; 363 364 (* distribute statements over hierarchy *) 365 val mark_exports = mark_exports { program = program, prefix_of = fst o prep_sym, 366 map_export = fn name_fragments => fn sym => fn f => 367 (map_module name_fragments o apsnd o Code_Symbol.Graph.map_node sym o apsnd) 368 (fn Stmt (export, stmt) => Stmt (f export, stmt)), 369 class_transitive = class_transitive, class_relation_public = class_relation_public }; 370 fun add_stmt sym stmt = 371 let 372 val (name_fragments, base) = prep_sym sym; 373 in 374 (map_module name_fragments o apsnd) 375 (Code_Symbol.Graph.new_node (sym, (base, Stmt (if null exports then Public else Private, stmt)))) 376 end; 377 fun add_edge_acyclic_error error_msg dep gr = 378 Code_Symbol.Graph.add_edge_acyclic dep gr 379 handle Code_Symbol.Graph.CYCLES _ => error (error_msg ()) 380 fun add_dep sym sym' = 381 let 382 val (name_fragments, _) = prep_sym sym; 383 val (name_fragments', _) = prep_sym sym'; 384 val (name_fragments_common, (diff, diff')) = 385 chop_common_prefix (op =) (name_fragments, name_fragments'); 386 val is_cross_module = not (null diff andalso null diff'); 387 val dep = apply2 hd (map Code_Symbol.Module diff @ [sym], map Code_Symbol.Module diff' @ [sym']); 388 val add_edge = if is_cross_module andalso not cyclic_modules 389 then add_edge_acyclic_error (fn _ => "Dependency " 390 ^ Code_Symbol.quote ctxt sym ^ " -> " 391 ^ Code_Symbol.quote ctxt sym' 392 ^ " would result in module dependency cycle") dep 393 else Code_Symbol.Graph.add_edge dep; 394 in 395 (map_module name_fragments_common o apsnd) add_edge 396 #> (if is_cross_module then mark_exports name_fragments' sym' else I) 397 end; 398 val proto_program = build_proto_program 399 { empty = empty_program, add_stmt = add_stmt, add_dep = add_dep } program 400 |> fold (fn sym => mark_exports ((fst o prep_sym) sym) sym) exports; 401 402 (* name declarations, data and statement modifications *) 403 fun make_declarations nsps (data, nodes) = 404 let 405 val (module_fragments, stmt_syms) = 406 Code_Symbol.Graph.keys nodes 407 |> List.partition 408 (fn sym => case Code_Symbol.Graph.get_node nodes sym 409 of (_, Module _) => true | _ => false) 410 |> apply2 (prioritize sym_priority) 411 fun declare namify sym (nsps, nodes) = 412 let 413 val (base, node) = Code_Symbol.Graph.get_node nodes sym; 414 val (base', nsps') = namify node base nsps; 415 val nodes' = Code_Symbol.Graph.map_node sym (K (base', node)) nodes; 416 in (nsps', nodes') end; 417 val (nsps', nodes') = (nsps, nodes) 418 |> fold (declare (K namify_module)) module_fragments 419 |> fold (declare (namify_stmt o snd o the_stmt)) stmt_syms; 420 fun modify_stmts' syms_stmts = 421 let 422 val stmts' = modify_stmts syms_stmts 423 in stmts' @ replicate (length syms_stmts - length stmts') NONE end; 424 val nodes'' = 425 nodes' 426 |> Code_Symbol.Graph.map_strong_conn (map_module_stmts (make_declarations nsps') modify_stmts'); 427 val data' = fold memorize_data stmt_syms data; 428 in (data', nodes'') end; 429 val (_, hierarchical_program) = make_declarations empty_nsp proto_program; 430 431 (* deresolving *) 432 fun deresolver prefix_fragments sym = 433 let 434 val (name_fragments, _) = prep_sym sym; 435 val (_, (_, remainder)) = chop_common_prefix (op =) (prefix_fragments, name_fragments); 436 val nodes = fold (fn name_fragment => fn nodes => case Code_Symbol.Graph.get_node nodes (Code_Symbol.Module name_fragment) 437 of (_, Module (_, nodes)) => nodes) name_fragments hierarchical_program; 438 val (base', _) = Code_Symbol.Graph.get_node nodes sym; 439 in Long_Name.implode (remainder @ [base']) end 440 handle Code_Symbol.Graph.UNDEF _ => error ("Unknown statement name: " 441 ^ Code_Symbol.quote ctxt sym); 442 443 in { deresolver = deresolver, hierarchical_program = hierarchical_program } end; 444 445fun print_hierarchical { print_module, print_stmt, lift_markup } = 446 let 447 fun print_node _ (_, Dummy) = 448 NONE 449 | print_node prefix_fragments (sym, Stmt stmt) = 450 SOME (lift_markup (Code_Printer.markup_stmt sym) 451 (print_stmt prefix_fragments (sym, stmt))) 452 | print_node prefix_fragments (Code_Symbol.Module name_fragment, Module (data, nodes)) = 453 let 454 val prefix_fragments' = prefix_fragments @ [name_fragment] 455 in 456 Option.map (print_module prefix_fragments' 457 name_fragment data) (print_nodes prefix_fragments' nodes) 458 end 459 and print_nodes prefix_fragments nodes = 460 let 461 val xs = (map_filter (fn sym => print_node prefix_fragments 462 (sym, snd (Code_Symbol.Graph.get_node nodes sym))) o rev o flat o Code_Symbol.Graph.strong_conn) nodes 463 in if null xs then NONE else SOME xs end; 464 in these o print_nodes [] end; 465 466end; 467