7 signature CODE_NAMESPACE = |
7 signature CODE_NAMESPACE = |
8 sig |
8 sig |
9 datatype export = Private | Opaque | Public |
9 datatype export = Private | Opaque | Public |
10 val is_public: export -> bool |
10 val is_public: export -> bool |
11 val not_private: export -> bool |
11 val not_private: export -> bool |
|
12 val join_exports: export list -> export |
12 |
13 |
13 type flat_program |
14 type flat_program |
14 val flat_program: Proof.context |
15 val flat_program: Proof.context |
15 -> { module_prefix: string, module_name: string, |
16 -> { module_prefix: string, module_name: string, |
16 reserved: Name.context, identifiers: Code_Target.identifier_data, empty_nsp: 'a, |
17 reserved: Name.context, identifiers: Code_Target.identifier_data, empty_nsp: 'a, |
28 val hierarchical_program: Proof.context |
29 val hierarchical_program: Proof.context |
29 -> { module_name: string, |
30 -> { module_name: string, |
30 reserved: Name.context, identifiers: Code_Target.identifier_data, |
31 reserved: Name.context, identifiers: Code_Target.identifier_data, |
31 empty_nsp: 'c, namify_module: string -> 'c -> string * 'c, |
32 empty_nsp: 'c, namify_module: string -> 'c -> string * 'c, |
32 namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c, |
33 namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c, |
33 cyclic_modules: bool, empty_data: 'b, memorize_data: Code_Symbol.T -> 'b -> 'b, |
34 cyclic_modules: bool, |
34 modify_stmts: (Code_Symbol.T * Code_Thingol.stmt) list -> 'a option list } |
35 class_transitive: bool, class_relation_public: bool, |
|
36 empty_data: 'b, memorize_data: Code_Symbol.T -> 'b -> 'b, |
|
37 modify_stmts: (Code_Symbol.T * (export * Code_Thingol.stmt)) list -> (export * 'a) option list } |
35 -> Code_Symbol.T list -> Code_Thingol.program |
38 -> Code_Symbol.T list -> Code_Thingol.program |
36 -> { deresolver: string list -> Code_Symbol.T -> string, |
39 -> { deresolver: string list -> Code_Symbol.T -> string, |
37 hierarchical_program: ('a, 'b) hierarchical_program } |
40 hierarchical_program: ('a, 'b) hierarchical_program } |
38 val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c, |
41 val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c, |
39 print_stmt: string list -> Code_Symbol.T * (export * 'a) -> 'c, |
42 print_stmt: string list -> Code_Symbol.T * (export * 'a) -> 'c, |
53 |
56 |
54 fun not_private Public = true |
57 fun not_private Public = true |
55 | not_private Opaque = true |
58 | not_private Opaque = true |
56 | not_private _ = false; |
59 | not_private _ = false; |
57 |
60 |
|
61 fun mark_export Public _ = Public |
|
62 | mark_export _ Public = Public |
|
63 | mark_export Opaque _ = Opaque |
|
64 | mark_export _ Opaque = Opaque |
|
65 | mark_export _ _ = Private; |
|
66 |
|
67 fun join_exports exports = fold mark_export exports Private; |
|
68 |
|
69 fun dependent_exports { program = program, class_transitive = class_transitive } = |
|
70 let |
|
71 fun is_datatype_or_class (Code_Symbol.Type_Constructor _) = true |
|
72 | is_datatype_or_class (Code_Symbol.Type_Class _) = true |
|
73 | is_datatype_or_class _ = false; |
|
74 fun is_relevant (Code_Symbol.Class_Relation _) = true |
|
75 | is_relevant sym = is_datatype_or_class sym; |
|
76 val proto_gr = Code_Symbol.Graph.restrict is_relevant program; |
|
77 val gr = |
|
78 proto_gr |
|
79 |> Code_Symbol.Graph.fold |
|
80 (fn (sym, (_, (_, deps))) => |
|
81 if is_relevant sym |
|
82 then I |
|
83 else |
|
84 Code_Symbol.Graph.new_node (sym, Code_Thingol.NoStmt) |
|
85 #> Code_Symbol.Graph.Keys.fold |
|
86 (fn sym' => |
|
87 if is_relevant sym' |
|
88 then Code_Symbol.Graph.add_edge (sym, sym') |
|
89 else I) deps) program |
|
90 |> class_transitive ? |
|
91 Code_Symbol.Graph.fold (fn (sym as Code_Symbol.Type_Class _, _) => |
|
92 fold (curry Code_Symbol.Graph.add_edge sym) |
|
93 ((remove (op =) sym o Code_Symbol.Graph.all_succs proto_gr) [sym]) | _ => I) proto_gr |
|
94 fun deps_of sym = |
|
95 let |
|
96 val succs = Code_Symbol.Graph.Keys.dest o Code_Symbol.Graph.imm_succs gr; |
|
97 val deps1 = succs sym; |
|
98 val deps2 = if class_transitive |
|
99 then [] |
|
100 else [] |> fold (union (op =)) (map succs deps1) |> subtract (op =) deps1 |
|
101 in (deps1, deps2) end; |
|
102 in |
|
103 { is_datatype_or_class = is_datatype_or_class, |
|
104 deps_of = deps_of } |
|
105 end; |
|
106 |
|
107 fun mark_exports_aux { program = program, prefix_of = prefix_of, map_export = map_export, |
|
108 is_datatype_or_class = is_datatype_or_class, deps_of = deps_of, |
|
109 class_relation_public = class_relation_public } prefix sym = |
|
110 let |
|
111 val export = (if is_datatype_or_class sym then Opaque else Public); |
|
112 val (dependent_export1, dependent_export2) = |
|
113 case Code_Symbol.Graph.get_node program sym of |
|
114 Code_Thingol.Fun _ => (SOME Opaque, NONE) |
|
115 | Code_Thingol.Classinst _ => (SOME Opaque, NONE) |
|
116 | Code_Thingol.Datatypecons _ => (SOME Public, SOME Opaque) |
|
117 | Code_Thingol.Classparam _ => (SOME Public, SOME Opaque) |
|
118 | Code_Thingol.Classrel _ => |
|
119 (if class_relation_public |
|
120 then (SOME Public, SOME Opaque) |
|
121 else (SOME Opaque, NONE)) |
|
122 | _ => (NONE, NONE); |
|
123 val dependent_exports = |
|
124 case dependent_export1 of |
|
125 SOME export1 => (case dependent_export2 of |
|
126 SOME export2 => |
|
127 let |
|
128 val (deps1, deps2) = deps_of sym |
|
129 in map (rpair export1) deps1 @ map (rpair export2) deps2 end |
|
130 | NONE => map (rpair export1) (fst (deps_of sym))) |
|
131 | NONE => []; |
|
132 in |
|
133 map_export prefix sym (mark_export export) |
|
134 #> fold (fn (sym, export) => map_export (prefix_of sym) sym (mark_export export)) |
|
135 dependent_exports |
|
136 end; |
|
137 |
|
138 fun mark_exports { program = program, prefix_of = prefix_of, map_export = map_export, |
|
139 class_transitive = class_transitive, class_relation_public = class_relation_public } = |
|
140 let |
|
141 val { is_datatype_or_class, deps_of } = |
|
142 dependent_exports { program = program, class_transitive = class_transitive }; |
|
143 in |
|
144 mark_exports_aux { program = program, prefix_of = prefix_of, map_export = map_export, |
|
145 is_datatype_or_class = is_datatype_or_class, deps_of = deps_of, |
|
146 class_relation_public = class_relation_public } |
|
147 end; |
|
148 |
58 |
149 |
59 (** fundamental module name hierarchy **) |
150 (** fundamental module name hierarchy **) |
60 |
151 |
61 fun module_fragments' { identifiers, reserved } name = |
152 fun module_fragments' { identifiers, reserved } name = |
62 case Code_Symbol.lookup_module_data identifiers name of |
153 case Code_Symbol.lookup_module_data identifiers name of |
111 force_module = Long_Name.explode module_name, identifiers = identifiers } |
202 force_module = Long_Name.explode module_name, identifiers = identifiers } |
112 #>> Long_Name.implode; |
203 #>> Long_Name.implode; |
113 val sym_priority = has_priority identifiers; |
204 val sym_priority = has_priority identifiers; |
114 |
205 |
115 (* distribute statements over hierarchy *) |
206 (* distribute statements over hierarchy *) |
|
207 val mark_exports = mark_exports { program = program, prefix_of = fst o prep_sym, |
|
208 map_export = fn module_name => fn sym => |
|
209 Graph.map_node module_name o apfst o Code_Symbol.Graph.map_node sym o apsnd o apfst, |
|
210 class_transitive = false, class_relation_public = false }; |
116 fun add_stmt sym stmt = |
211 fun add_stmt sym stmt = |
117 let |
212 let |
118 val (module_name, base) = prep_sym sym; |
213 val (module_name, base) = prep_sym sym; |
119 in |
214 in |
120 Graph.default_node (module_name, (Code_Symbol.Graph.empty, [])) |
215 Graph.default_node (module_name, (Code_Symbol.Graph.empty, [])) |
121 #> (Graph.map_node module_name o apfst) |
216 #> (Graph.map_node module_name o apfst) |
122 (Code_Symbol.Graph.new_node (sym, (base, (Public, stmt)))) |
217 (Code_Symbol.Graph.new_node (sym, (base, (if null exports then Public else Private, stmt)))) |
123 end; |
218 end; |
124 fun add_dep sym sym' = |
219 fun add_dep sym sym' = |
125 let |
220 let |
126 val (module_name, _) = prep_sym sym; |
221 val (module_name, _) = prep_sym sym; |
127 val (module_name', _) = prep_sym sym'; |
222 val (module_name', _) = prep_sym sym'; |
128 in if module_name = module_name' |
223 in if module_name = module_name' |
129 then (Graph.map_node module_name o apfst) (Code_Symbol.Graph.add_edge (sym, sym')) |
224 then (Graph.map_node module_name o apfst) (Code_Symbol.Graph.add_edge (sym, sym')) |
130 else (Graph.map_node module_name o apsnd) |
225 else (Graph.map_node module_name o apsnd) |
131 (AList.map_default (op =) (module_name', []) (insert (op =) sym')) |
226 (AList.map_default (op =) (module_name', []) (insert (op =) sym')) |
|
227 #> mark_exports module_name' sym' |
132 end; |
228 end; |
133 val proto_program = build_proto_program |
229 val proto_program = build_proto_program |
134 { empty = Graph.empty, add_stmt = add_stmt, add_dep = add_dep } program; |
230 { empty = Graph.empty, add_stmt = add_stmt, add_dep = add_dep } program |
|
231 |> fold (fn sym => mark_exports ((fst o prep_sym) sym) sym) exports; |
135 |
232 |
136 (* name declarations and statement modifications *) |
233 (* name declarations and statement modifications *) |
137 fun declare sym (base, (_, stmt)) (gr, nsp) = |
234 fun declare sym (base, (_, stmt)) (gr, nsp) = |
138 let |
235 let |
139 val (base', nsp') = namify_stmt stmt base nsp; |
236 val (base', nsp') = namify_stmt stmt base nsp; |
198 |
295 |
199 fun map_module_stmts f_module f_stmts sym_base_nodes = |
296 fun map_module_stmts f_module f_stmts sym_base_nodes = |
200 let |
297 let |
201 val some_modules = |
298 val some_modules = |
202 sym_base_nodes |
299 sym_base_nodes |
203 |> map (fn (sym, (base, Module content)) => SOME (base, content) | _ => NONE) |
300 |> map (fn (_, (base, Module content)) => SOME (base, content) | _ => NONE) |
204 |> (burrow_options o map o apsnd) f_module; |
301 |> (burrow_options o map o apsnd) f_module; |
205 val some_export_stmts = |
302 val some_export_stmts = |
206 sym_base_nodes |
303 sym_base_nodes |
207 |> map (fn (sym, (base, Stmt export_stmt)) => SOME ((sym, export_stmt), base) | _ => NONE) |
304 |> map (fn (sym, (base, Stmt export_stmt)) => SOME ((sym, export_stmt), base) | _ => NONE) |
208 |> (burrow_options o burrow_fst) (fn [] => [] | xs => f_stmts xs) |
305 |> (burrow_options o burrow_fst) (fn [] => [] | xs => f_stmts xs) |
212 (base, case some_export_stmt of SOME export_stmt => Stmt export_stmt | NONE => Dummy)) |
309 (base, case some_export_stmt of SOME export_stmt => Stmt export_stmt | NONE => Dummy)) |
213 some_modules some_export_stmts |
310 some_modules some_export_stmts |
214 end; |
311 end; |
215 |
312 |
216 fun hierarchical_program ctxt { module_name, reserved, identifiers, empty_nsp, |
313 fun hierarchical_program ctxt { module_name, reserved, identifiers, empty_nsp, |
217 namify_module, namify_stmt, cyclic_modules, empty_data, memorize_data, modify_stmts } |
314 namify_module, namify_stmt, cyclic_modules, |
|
315 class_transitive, class_relation_public, |
|
316 empty_data, memorize_data, modify_stmts } |
218 exports program = |
317 exports program = |
219 let |
318 let |
220 |
319 |
221 (* building module name hierarchy *) |
320 (* building module name hierarchy *) |
222 val module_namespace = build_module_namespace ctxt { module_prefix = "", |
321 val module_namespace = build_module_namespace ctxt { module_prefix = "", |
240 |> Symtab.fold (fn (_, fragments) => allocate_module fragments) module_namespace |
339 |> Symtab.fold (fn (_, fragments) => allocate_module fragments) module_namespace |
241 |> Code_Symbol.Graph.fold (allocate_module o these o Option.map fst |
340 |> Code_Symbol.Graph.fold (allocate_module o these o Option.map fst |
242 o Code_Symbol.lookup identifiers o fst) program; |
341 o Code_Symbol.lookup identifiers o fst) program; |
243 |
342 |
244 (* distribute statements over hierarchy *) |
343 (* distribute statements over hierarchy *) |
|
344 val mark_exports = mark_exports { program = program, prefix_of = fst o prep_sym, |
|
345 map_export = fn name_fragments => fn sym => fn f => |
|
346 (map_module name_fragments o apsnd o Code_Symbol.Graph.map_node sym o apsnd) |
|
347 (fn Stmt (export, stmt) => Stmt (f export, stmt)), |
|
348 class_transitive = class_transitive, class_relation_public = class_relation_public }; |
245 fun add_stmt sym stmt = |
349 fun add_stmt sym stmt = |
246 let |
350 let |
247 val (name_fragments, base) = prep_sym sym; |
351 val (name_fragments, base) = prep_sym sym; |
248 in |
352 in |
249 (map_module name_fragments o apsnd) |
353 (map_module name_fragments o apsnd) |
250 (Code_Symbol.Graph.new_node (sym, (base, Stmt (Public, stmt)))) |
354 (Code_Symbol.Graph.new_node (sym, (base, Stmt (if null exports then Public else Private, stmt)))) |
251 end; |
355 end; |
252 fun add_edge_acyclic_error error_msg dep gr = |
356 fun add_edge_acyclic_error error_msg dep gr = |
253 Code_Symbol.Graph.add_edge_acyclic dep gr |
357 Code_Symbol.Graph.add_edge_acyclic dep gr |
254 handle Graph.CYCLES _ => error (error_msg ()) |
358 handle Graph.CYCLES _ => error (error_msg ()) |
255 fun add_dep sym sym' = |
359 fun add_dep sym sym' = |
264 then add_edge_acyclic_error (fn _ => "Dependency " |
368 then add_edge_acyclic_error (fn _ => "Dependency " |
265 ^ Code_Symbol.quote ctxt sym ^ " -> " |
369 ^ Code_Symbol.quote ctxt sym ^ " -> " |
266 ^ Code_Symbol.quote ctxt sym' |
370 ^ Code_Symbol.quote ctxt sym' |
267 ^ " would result in module dependency cycle") dep |
371 ^ " would result in module dependency cycle") dep |
268 else Code_Symbol.Graph.add_edge dep; |
372 else Code_Symbol.Graph.add_edge dep; |
269 in (map_module name_fragments_common o apsnd) add_edge end; |
373 in |
|
374 (map_module name_fragments_common o apsnd) add_edge |
|
375 #> (if is_cross_module then mark_exports name_fragments' sym' else I) |
|
376 end; |
270 val proto_program = build_proto_program |
377 val proto_program = build_proto_program |
271 { empty = empty_program, add_stmt = add_stmt, add_dep = add_dep } program; |
378 { empty = empty_program, add_stmt = add_stmt, add_dep = add_dep } program |
|
379 |> fold (fn sym => mark_exports ((fst o prep_sym) sym) sym) exports; |
272 |
380 |
273 (* name declarations, data and statement modifications *) |
381 (* name declarations, data and statement modifications *) |
274 fun make_declarations nsps (data, nodes) = |
382 fun make_declarations nsps (data, nodes) = |
275 let |
383 let |
276 val (module_fragments, stmt_syms) = |
384 val (module_fragments, stmt_syms) = |
290 |> fold (declare (namify_stmt o snd o the_stmt)) stmt_syms; |
398 |> fold (declare (namify_stmt o snd o the_stmt)) stmt_syms; |
291 fun modify_stmts' syms_stmts = |
399 fun modify_stmts' syms_stmts = |
292 let |
400 let |
293 val stmts' = modify_stmts syms_stmts |
401 val stmts' = modify_stmts syms_stmts |
294 in stmts' @ replicate (length syms_stmts - length stmts') NONE end; |
402 in stmts' @ replicate (length syms_stmts - length stmts') NONE end; |
295 fun modify_stmts'' syms_exports_stmts = |
|
296 syms_exports_stmts |
|
297 |> map (fn (sym, (export, stmt)) => ((sym, stmt), export)) |
|
298 |> burrow_fst modify_stmts' |
|
299 |> map (fn (SOME stmt, export) => SOME (export, stmt) | _ => NONE); |
|
300 val nodes'' = |
403 val nodes'' = |
301 nodes' |
404 nodes' |
302 |> Code_Symbol.Graph.map_strong_conn (map_module_stmts (make_declarations nsps') modify_stmts''); |
405 |> Code_Symbol.Graph.map_strong_conn (map_module_stmts (make_declarations nsps') modify_stmts'); |
303 val data' = fold memorize_data stmt_syms data; |
406 val data' = fold memorize_data stmt_syms data; |
304 in (data', nodes'') end; |
407 in (data', nodes'') end; |
305 val (_, hierarchical_program) = make_declarations empty_nsp proto_program; |
408 val (_, hierarchical_program) = make_declarations empty_nsp proto_program; |
306 |
409 |
307 (* deresolving *) |
410 (* deresolving *) |