1 (* Title: Pure/ML-Systems/polyml.ML |
|
2 Author: Makarius |
|
3 |
|
4 Compatibility wrapper for Poly/ML. |
|
5 *) |
|
6 |
|
7 (* initial ML name space *) |
|
8 |
|
9 use "ML-Systems/ml_system.ML"; |
|
10 |
|
11 if ML_System.name = "polyml-5.6" |
|
12 then use "ML-Systems/ml_name_space_polyml-5.6.ML" |
|
13 else use "ML-Systems/ml_name_space_polyml.ML"; |
|
14 |
|
15 structure ML_Name_Space = |
|
16 struct |
|
17 open ML_Name_Space; |
|
18 val initial_val = |
|
19 List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit") |
|
20 (#allVal global ()); |
|
21 val initial_type = #allType global (); |
|
22 val initial_fixity = #allFix global (); |
|
23 val initial_structure = #allStruct global (); |
|
24 val initial_signature = #allSig global (); |
|
25 val initial_functor = #allFunct global (); |
|
26 end; |
|
27 |
|
28 |
|
29 (* ML system operations *) |
|
30 |
|
31 if ML_System.name = "polyml-5.3.0" |
|
32 then use "ML-Systems/share_common_data_polyml-5.3.0.ML" |
|
33 else (); |
|
34 |
|
35 fun ml_platform_path (s: string) = s; |
|
36 fun ml_standard_path (s: string) = s; |
|
37 |
|
38 if ML_System.platform_is_windows then use "ML-Systems/windows_path.ML" else (); |
|
39 |
|
40 structure ML_System = |
|
41 struct |
|
42 open ML_System; |
|
43 fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; |
|
44 val save_state = PolyML.SaveState.saveState o ml_platform_path; |
|
45 end; |
|
46 |
|
47 |
|
48 (* exceptions *) |
|
49 |
|
50 fun reraise exn = |
|
51 (case PolyML.exceptionLocation exn of |
|
52 NONE => raise exn |
|
53 | SOME location => PolyML.raiseWithLocation (exn, location)); |
|
54 |
|
55 exception Interrupt = SML90.Interrupt; |
|
56 |
|
57 use "General/exn.ML"; |
|
58 |
|
59 fun print_exception_trace (_: exn -> string) (_: string -> unit) = PolyML.exception_trace; |
|
60 |
|
61 if ML_System.name = "polyml-5.5.1" |
|
62 orelse ML_System.name = "polyml-5.5.2" |
|
63 orelse ML_System.name = "polyml-5.6" |
|
64 then use "ML-Systems/exn_trace_polyml-5.5.1.ML" |
|
65 else (); |
|
66 |
|
67 |
|
68 (* multithreading *) |
|
69 |
|
70 val seconds = Time.fromReal; |
|
71 |
|
72 if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ()) |
|
73 then () |
|
74 else use "ML-Systems/single_assignment_polyml.ML"; |
|
75 |
|
76 open Thread; |
|
77 use "ML-Systems/multithreading.ML"; |
|
78 use "ML-Systems/multithreading_polyml.ML"; |
|
79 |
|
80 if ML_System.name = "polyml-5.6" |
|
81 then use "ML-Systems/ml_stack_polyml-5.6.ML" |
|
82 else use "ML-Systems/ml_stack_dummy.ML"; |
|
83 |
|
84 use "ML-Systems/unsynchronized.ML"; |
|
85 val _ = PolyML.Compiler.forgetValue "ref"; |
|
86 val _ = PolyML.Compiler.forgetType "ref"; |
|
87 |
|
88 |
|
89 (* pervasive environment *) |
|
90 |
|
91 val _ = PolyML.Compiler.forgetValue "isSome"; |
|
92 val _ = PolyML.Compiler.forgetValue "getOpt"; |
|
93 val _ = PolyML.Compiler.forgetValue "valOf"; |
|
94 val _ = PolyML.Compiler.forgetValue "foldl"; |
|
95 val _ = PolyML.Compiler.forgetValue "foldr"; |
|
96 val _ = PolyML.Compiler.forgetValue "print"; |
|
97 val _ = PolyML.Compiler.forgetValue "explode"; |
|
98 val _ = PolyML.Compiler.forgetValue "concat"; |
|
99 |
|
100 val ord = SML90.ord; |
|
101 val chr = SML90.chr; |
|
102 val raw_explode = SML90.explode; |
|
103 val implode = SML90.implode; |
|
104 |
|
105 val io_buffer_size = 4096; |
|
106 |
|
107 fun quit () = exit 0; |
|
108 |
|
109 |
|
110 (* ML runtime system *) |
|
111 |
|
112 if ML_System.name = "polyml-5.6" |
|
113 then use "ML-Systems/ml_profiling_polyml-5.6.ML" |
|
114 else use "ML-Systems/ml_profiling_polyml.ML"; |
|
115 |
|
116 val pointer_eq = PolyML.pointerEq; |
|
117 |
|
118 |
|
119 (* ML toplevel pretty printing *) |
|
120 |
|
121 use "ML-Systems/ml_pretty.ML"; |
|
122 |
|
123 local |
|
124 val depth = Unsynchronized.ref 10; |
|
125 in |
|
126 fun get_default_print_depth () = ! depth; |
|
127 fun default_print_depth n = (depth := n; PolyML.print_depth n); |
|
128 val _ = default_print_depth 10; |
|
129 end; |
|
130 |
|
131 val error_depth = PolyML.error_depth; |
|
132 |
|
133 val pretty_ml = |
|
134 let |
|
135 fun convert _ (PolyML.PrettyBreak (width, offset)) = ML_Pretty.Break (false, width, offset) |
|
136 | convert _ (PolyML.PrettyBlock (_, _, |
|
137 [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) = |
|
138 ML_Pretty.Break (true, 1, 0) |
|
139 | convert len (PolyML.PrettyBlock (ind, consistent, context, prts)) = |
|
140 let |
|
141 fun property name default = |
|
142 (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of |
|
143 SOME (PolyML.ContextProperty (_, b)) => b |
|
144 | _ => default); |
|
145 val bg = property "begin" ""; |
|
146 val en = property "end" ""; |
|
147 val len' = property "length" len; |
|
148 in ML_Pretty.Block ((bg, en), consistent, ind, map (convert len') prts) end |
|
149 | convert len (PolyML.PrettyString s) = |
|
150 ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s) |
|
151 in convert "" end; |
|
152 |
|
153 fun ml_pretty (ML_Pretty.Break (false, width, offset)) = PolyML.PrettyBreak (width, offset) |
|
154 | ml_pretty (ML_Pretty.Break (true, _, _)) = |
|
155 PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")], |
|
156 [PolyML.PrettyString " "]) |
|
157 | ml_pretty (ML_Pretty.Block ((bg, en), consistent, ind, prts)) = |
|
158 let val context = |
|
159 (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @ |
|
160 (if en = "" then [] else [PolyML.ContextProperty ("end", en)]) |
|
161 in PolyML.PrettyBlock (ind, consistent, context, map ml_pretty prts) end |
|
162 | ml_pretty (ML_Pretty.String (s, len)) = |
|
163 if len = size s then PolyML.PrettyString s |
|
164 else PolyML.PrettyBlock |
|
165 (0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s]); |
|
166 |
|
167 |
|
168 (* ML compiler *) |
|
169 |
|
170 structure ML_Name_Space = |
|
171 struct |
|
172 open ML_Name_Space; |
|
173 val display_val = pretty_ml o displayVal; |
|
174 end; |
|
175 |
|
176 use "ML-Systems/ml_compiler_parameters.ML"; |
|
177 if ML_System.name = "polyml-5.6" |
|
178 then use "ML-Systems/ml_compiler_parameters_polyml-5.6.ML" else (); |
|
179 |
|
180 use "ML-Systems/use_context.ML"; |
|
181 use "ML-Systems/ml_positions.ML"; |
|
182 use "ML-Systems/compiler_polyml.ML"; |
|
183 |
|
184 PolyML.Compiler.reportUnreferencedIds := true; |
|
185 PolyML.Compiler.printInAlphabeticalOrder := false; |
|
186 PolyML.Compiler.maxInlineSize := 80; |
|
187 |
|
188 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2); |
|
189 |
|
190 use "ML-Systems/ml_parse_tree.ML"; |
|
191 if ML_System.name = "polyml-5.6" |
|
192 then use "ML-Systems/ml_parse_tree_polyml-5.6.ML" else (); |
|
193 |
|
194 fun toplevel_pp context (_: string list) pp = |
|
195 use_text context {line = 1, file = "pp", verbose = false, debug = false} |
|
196 ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))"); |
|
197 |
|
198 fun ml_make_string struct_name = |
|
199 "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, " ^ |
|
200 struct_name ^ ".ML_print_depth ())))))"; |
|
201 |
|
202 |
|
203 (* ML debugger *) |
|
204 |
|
205 if ML_System.name = "polyml-5.6" |
|
206 then use "ML-Systems/ml_debugger_polyml-5.6.ML" |
|
207 else use "ML-Systems/ml_debugger.ML"; |
|