author | wenzelm |
Thu, 03 Mar 2016 11:12:02 +0100 | |
changeset 62501 | 98fa1f9a292f |
parent 62494 | b90109b2487c |
child 62503 | 19afb533028e |
permissions | -rw-r--r-- |
62077 | 1 |
(* Title: Pure/RAW/ROOT_polyml.ML |
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
2 |
Author: Makarius |
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
3 |
|
50910 | 4 |
Compatibility wrapper for Poly/ML. |
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
5 |
*) |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
6 |
|
60953
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset
|
7 |
(* initial ML name space *) |
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset
|
8 |
|
61925 | 9 |
use "RAW/ml_system.ML"; |
62501 | 10 |
use "RAW/ml_name_space.ML"; |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
60993
diff
changeset
|
11 |
|
62387
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset
|
12 |
if List.exists (fn (a, _) => a = "FixedInt") (#allStruct ML_Name_Space.global ()) then () |
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset
|
13 |
else use "RAW/fixed_int_dummy.ML"; |
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset
|
14 |
|
60953
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset
|
15 |
structure ML_Name_Space = |
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset
|
16 |
struct |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
60993
diff
changeset
|
17 |
open ML_Name_Space; |
60953
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset
|
18 |
val initial_val = |
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset
|
19 |
List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit") |
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset
|
20 |
(#allVal global ()); |
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset
|
21 |
val initial_type = #allType global (); |
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset
|
22 |
val initial_fixity = #allFix global (); |
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset
|
23 |
val initial_structure = #allStruct global (); |
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset
|
24 |
val initial_signature = #allSig global (); |
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset
|
25 |
val initial_functor = #allFunct global (); |
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset
|
26 |
end; |
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
54723
diff
changeset
|
27 |
|
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
54723
diff
changeset
|
28 |
|
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
29 |
(* exceptions *) |
30673 | 30 |
|
31427
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
31318
diff
changeset
|
31 |
fun reraise exn = |
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
31318
diff
changeset
|
32 |
(case PolyML.exceptionLocation exn of |
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
31318
diff
changeset
|
33 |
NONE => raise exn |
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
31318
diff
changeset
|
34 |
| SOME location => PolyML.raiseWithLocation (exn, location)); |
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
31318
diff
changeset
|
35 |
|
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
36 |
exception Interrupt = SML90.Interrupt; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
37 |
|
61925 | 38 |
use "RAW/exn.ML"; |
62501 | 39 |
use "RAW/exn_trace.ML"; |
59470 | 40 |
|
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
41 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
42 |
(* multithreading *) |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
43 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
44 |
val seconds = Time.fromReal; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
45 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
46 |
open Thread; |
61925 | 47 |
use "RAW/multithreading.ML"; |
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
48 |
|
61925 | 49 |
use "RAW/unsynchronized.ML"; |
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38470
diff
changeset
|
50 |
val _ = PolyML.Compiler.forgetValue "ref"; |
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38470
diff
changeset
|
51 |
val _ = PolyML.Compiler.forgetType "ref"; |
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
52 |
|
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
53 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
54 |
(* pervasive environment *) |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
55 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
56 |
val _ = PolyML.Compiler.forgetValue "isSome"; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
57 |
val _ = PolyML.Compiler.forgetValue "getOpt"; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
58 |
val _ = PolyML.Compiler.forgetValue "valOf"; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
59 |
val _ = PolyML.Compiler.forgetValue "foldl"; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
60 |
val _ = PolyML.Compiler.forgetValue "foldr"; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
61 |
val _ = PolyML.Compiler.forgetValue "print"; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
62 |
val _ = PolyML.Compiler.forgetValue "explode"; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
63 |
val _ = PolyML.Compiler.forgetValue "concat"; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
64 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
65 |
val ord = SML90.ord; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
66 |
val chr = SML90.chr; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
67 |
val raw_explode = SML90.explode; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
68 |
val implode = SML90.implode; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
69 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
70 |
fun quit () = exit 0; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
71 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
72 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
73 |
(* ML runtime system *) |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
74 |
|
62501 | 75 |
use "RAW/ml_heap.ML"; |
76 |
use "RAW/ml_profiling.ML"; |
|
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
77 |
|
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
78 |
val pointer_eq = PolyML.pointerEq; |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
79 |
|
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
80 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
81 |
(* ML toplevel pretty printing *) |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
82 |
|
61925 | 83 |
use "RAW/ml_pretty.ML"; |
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
84 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
85 |
local |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
86 |
val depth = Unsynchronized.ref 10; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
87 |
in |
56281 | 88 |
fun get_default_print_depth () = ! depth; |
56285 | 89 |
fun default_print_depth n = (depth := n; PolyML.print_depth n); |
90 |
val _ = default_print_depth 10; |
|
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
91 |
end; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
92 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
93 |
val error_depth = PolyML.error_depth; |
30626 | 94 |
|
30676
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
95 |
val pretty_ml = |
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
96 |
let |
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61794
diff
changeset
|
97 |
fun convert _ (PolyML.PrettyBreak (width, offset)) = ML_Pretty.Break (false, width, offset) |
54718 | 98 |
| convert _ (PolyML.PrettyBlock (_, _, |
51638
1275716f395b
more defensive representation of forced break within PolyML.PrettyBreak -- avoid accidental blowup if low-level operations are used, notably PolyML.makestring or its variant General.exnMessage;
wenzelm
parents:
50911
diff
changeset
|
99 |
[PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) = |
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61794
diff
changeset
|
100 |
ML_Pretty.Break (true, 1, 0) |
61864 | 101 |
| convert len (PolyML.PrettyBlock (ind, consistent, context, prts)) = |
30676
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
102 |
let |
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
103 |
fun property name default = |
31318 | 104 |
(case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of |
105 |
SOME (PolyML.ContextProperty (_, b)) => b |
|
54718 | 106 |
| _ => default); |
30676
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
107 |
val bg = property "begin" ""; |
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
108 |
val en = property "end" ""; |
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
109 |
val len' = property "length" len; |
61869 | 110 |
in ML_Pretty.Block ((bg, en), consistent, ind, map (convert len') prts) end |
31318 | 111 |
| convert len (PolyML.PrettyString s) = |
62387
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset
|
112 |
ML_Pretty.String |
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset
|
113 |
(s, FixedInt.fromInt (case Int.fromString len of SOME i => i | NONE => size s)) |
30676
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
114 |
in convert "" end; |
30638 | 115 |
|
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61794
diff
changeset
|
116 |
fun ml_pretty (ML_Pretty.Break (false, width, offset)) = PolyML.PrettyBreak (width, offset) |
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61794
diff
changeset
|
117 |
| ml_pretty (ML_Pretty.Break (true, _, _)) = |
51638
1275716f395b
more defensive representation of forced break within PolyML.PrettyBreak -- avoid accidental blowup if low-level operations are used, notably PolyML.makestring or its variant General.exnMessage;
wenzelm
parents:
50911
diff
changeset
|
118 |
PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")], |
1275716f395b
more defensive representation of forced break within PolyML.PrettyBreak -- avoid accidental blowup if low-level operations are used, notably PolyML.makestring or its variant General.exnMessage;
wenzelm
parents:
50911
diff
changeset
|
119 |
[PolyML.PrettyString " "]) |
61869 | 120 |
| ml_pretty (ML_Pretty.Block ((bg, en), consistent, ind, prts)) = |
30679 | 121 |
let val context = |
31318 | 122 |
(if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @ |
123 |
(if en = "" then [] else [PolyML.ContextProperty ("end", en)]) |
|
61864 | 124 |
in PolyML.PrettyBlock (ind, consistent, context, map ml_pretty prts) end |
30676
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
125 |
| ml_pretty (ML_Pretty.String (s, len)) = |
62387
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset
|
126 |
if len = FixedInt.fromInt (size s) then PolyML.PrettyString s |
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset
|
127 |
else |
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset
|
128 |
PolyML.PrettyBlock |
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset
|
129 |
(0, false, |
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset
|
130 |
[PolyML.ContextProperty ("length", FixedInt.toString len)], [PolyML.PrettyString s]); |
30626 | 131 |
|
60897 | 132 |
|
133 |
(* ML compiler *) |
|
134 |
||
62493 | 135 |
use "RAW/secure.ML"; |
136 |
||
60897 | 137 |
structure ML_Name_Space = |
138 |
struct |
|
60953
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset
|
139 |
open ML_Name_Space; |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
60993
diff
changeset
|
140 |
val display_val = pretty_ml o displayVal; |
60897 | 141 |
end; |
142 |
||
61925 | 143 |
use "RAW/ml_positions.ML"; |
62494 | 144 |
use "RAW/ml_compiler0.ML"; |
60897 | 145 |
|
146 |
PolyML.Compiler.reportUnreferencedIds := true; |
|
147 |
PolyML.Compiler.printInAlphabeticalOrder := false; |
|
148 |
PolyML.Compiler.maxInlineSize := 80; |
|
62472 | 149 |
PolyML.Compiler.prompt1 := "ML> "; |
150 |
PolyML.Compiler.prompt2 := "ML# "; |
|
60897 | 151 |
|
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59055
diff
changeset
|
152 |
fun ml_make_string struct_name = |
62387
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset
|
153 |
"(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^ |
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset
|
154 |
struct_name ^ ".ML_print_depth ()))))))"; |
60897 | 155 |
|
156 |
||
157 |
(* ML debugger *) |
|
158 |
||
62501 | 159 |
use_no_debug "RAW/ml_debugger.ML"; |