author | wenzelm |
Thu, 07 Apr 2016 22:09:23 +0200 | |
changeset 62912 | 745d31e63c21 |
parent 62910 | f37878ebba65 |
child 62923 | 3a122e1e352a |
permissions | -rw-r--r-- |
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62504
diff
changeset
|
1 |
(* Title: Pure/ML/ml_name_space.ML |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
3 |
|
62853 | 4 |
ML name space, with initial entries for strict Standard ML. |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
5 |
*) |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
6 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
7 |
structure ML_Name_Space = |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
8 |
struct |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
9 |
open PolyML.NameSpace; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
10 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
11 |
type T = PolyML.NameSpace.nameSpace; |
62819
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
12 |
|
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
13 |
val global = PolyML.globalNameSpace; |
62819
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
14 |
fun global_values values : T = |
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
15 |
{lookupVal = #lookupVal global, |
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
16 |
lookupType = #lookupType global, |
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
17 |
lookupStruct = #lookupStruct global, |
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
18 |
lookupFix = #lookupFix global, |
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
19 |
lookupSig = #lookupSig global, |
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
20 |
lookupFunct = #lookupFunct global, |
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
21 |
enterVal = |
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
22 |
fn (x, value) => |
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
23 |
(case List.find (fn (y, _) => x = y) values of |
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
24 |
SOME (_, x') => #enterVal global (x', value) |
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
25 |
| NONE => ()), |
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
26 |
enterType = fn _ => (), |
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
27 |
enterFix = fn _ => (), |
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
28 |
enterStruct = fn _ => (), |
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
29 |
enterSig = fn _ => (), |
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
30 |
enterFunct = fn _ => (), |
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
31 |
allVal = #allVal global, |
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
32 |
allType = #allType global, |
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
33 |
allFix = #allFix global, |
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
34 |
allStruct = #allStruct global, |
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
35 |
allSig = #allSig global, |
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62659
diff
changeset
|
36 |
allFunct = #allFunct global}; |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
37 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
38 |
type valueVal = Values.value; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
39 |
fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space); |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
40 |
fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space); |
62657 | 41 |
val forget_val = PolyML.Compiler.forgetValue; |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
42 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
43 |
type typeVal = TypeConstrs.typeConstr; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
44 |
fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space); |
62657 | 45 |
val forget_type = PolyML.Compiler.forgetType; |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
46 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
47 |
type fixityVal = Infixes.fixity; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
48 |
fun displayFix (_: string, x) = Infixes.print x; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
49 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
50 |
type structureVal = Structures.structureVal; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
51 |
fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space); |
62657 | 52 |
val forget_structure = PolyML.Compiler.forgetStructure; |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
53 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
54 |
type signatureVal = Signatures.signatureVal; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
55 |
fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space); |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
56 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
57 |
type functorVal = Functors.functorVal; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
58 |
fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space); |
62839
ea9f12e422c7
clarified SML name space: no access to structure PolyML;
wenzelm
parents:
62819
diff
changeset
|
59 |
|
ea9f12e422c7
clarified SML name space: no access to structure PolyML;
wenzelm
parents:
62819
diff
changeset
|
60 |
|
62875 | 61 |
(* bootstrap environment *) |
62839
ea9f12e422c7
clarified SML name space: no access to structure PolyML;
wenzelm
parents:
62819
diff
changeset
|
62 |
|
62875 | 63 |
val bootstrap_values = |
62912 | 64 |
["use", "exit", "ML_file", "ML_system_pretty", "ML_system_pp", "ML_system_overload", |
65 |
"chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph"]; |
|
62875 | 66 |
val bootstrap_structures = |
62910
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
62902
diff
changeset
|
67 |
["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal", "Thread_Data", |
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
62902
diff
changeset
|
68 |
"ML_Recursive"]; |
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
62902
diff
changeset
|
69 |
val bootstrap_signatures = |
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
62902
diff
changeset
|
70 |
["THREAD_DATA", "ML_RECURSIVE"]; |
62875 | 71 |
|
72 |
||
73 |
(* Standard ML environment *) |
|
62860 | 74 |
|
62872 | 75 |
val sml_val = |
62875 | 76 |
List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_values) (#allVal global ()); |
62839
ea9f12e422c7
clarified SML name space: no access to structure PolyML;
wenzelm
parents:
62819
diff
changeset
|
77 |
val sml_type = #allType global (); |
ea9f12e422c7
clarified SML name space: no access to structure PolyML;
wenzelm
parents:
62819
diff
changeset
|
78 |
val sml_fixity = #allFix global (); |
ea9f12e422c7
clarified SML name space: no access to structure PolyML;
wenzelm
parents:
62819
diff
changeset
|
79 |
val sml_structure = |
62875 | 80 |
List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_structures) (#allStruct global ()); |
62910
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
62902
diff
changeset
|
81 |
val sml_signature = |
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
62902
diff
changeset
|
82 |
List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_signatures) (#allSig global ()); |
62839
ea9f12e422c7
clarified SML name space: no access to structure PolyML;
wenzelm
parents:
62819
diff
changeset
|
83 |
val sml_functor = #allFunct global (); |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
84 |
end; |