author | wenzelm |
Sun, 26 Aug 2018 17:28:38 +0200 | |
changeset 68813 | 78edc4bc3bd3 |
parent 68276 | cbee43ff4ceb |
child 68814 | 6a0b1357bded |
permissions | -rw-r--r-- |
31325 | 1 |
(* Title: Pure/ML/ml_env.ML |
2 |
Author: Makarius |
|
3 |
||
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
4 |
Toplevel environment for Standard ML and Isabelle/ML within the |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
5 |
implicit context. |
31325 | 6 |
*) |
7 |
||
8 |
signature ML_ENV = |
|
9 |
sig |
|
10 |
val inherit: Context.generic -> Context.generic -> Context.generic |
|
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59058
diff
changeset
|
11 |
val forget_structure: string -> Context.generic -> Context.generic |
60746 | 12 |
val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option |
62941 | 13 |
val add_breakpoints: (serial * (bool Unsynchronized.ref * Thread_Position.T)) list -> unit |
62873
2f9c8a18f832
support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
wenzelm
parents:
62839
diff
changeset
|
14 |
val init_bootstrap: Context.generic -> Context.generic |
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62889
diff
changeset
|
15 |
val SML_environment: bool Config.T |
68813 | 16 |
val set_global: bool -> Context.generic -> Context.generic |
17 |
val restore_global: Context.generic -> Context.generic -> Context.generic |
|
60858 | 18 |
val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic |
62495 | 19 |
val make_name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T |
20 |
val context: ML_Compiler0.context |
|
21 |
val name_space: ML_Name_Space.T |
|
36163
823c9400eb62
proper checking of ML functors (in Poly/ML 5.2 or later);
wenzelm
parents:
33519
diff
changeset
|
22 |
val check_functor: string -> unit |
31325 | 23 |
end |
24 |
||
25 |
structure ML_Env: ML_ENV = |
|
26 |
struct |
|
27 |
||
31328 | 28 |
(* context data *) |
29 |
||
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
30 |
type tables = |
62934 | 31 |
PolyML.NameSpace.Values.value Symtab.table * |
32 |
PolyML.NameSpace.TypeConstrs.typeConstr Symtab.table * |
|
33 |
PolyML.NameSpace.Infixes.fixity Symtab.table * |
|
34 |
PolyML.NameSpace.Structures.structureVal Symtab.table * |
|
35 |
PolyML.NameSpace.Signatures.signatureVal Symtab.table * |
|
36 |
PolyML.NameSpace.Functors.functorVal Symtab.table; |
|
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
37 |
|
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
38 |
fun merge_tables |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
39 |
((val1, type1, fixity1, structure1, signature1, functor1), |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
40 |
(val2, type2, fixity2, structure2, signature2, functor2)) : tables = |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
41 |
(Symtab.merge (K true) (val1, val2), |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
42 |
Symtab.merge (K true) (type1, type2), |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
43 |
Symtab.merge (K true) (fixity1, fixity2), |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
44 |
Symtab.merge (K true) (structure1, structure2), |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
45 |
Symtab.merge (K true) (signature1, signature2), |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
46 |
Symtab.merge (K true) (functor1, functor2)); |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
47 |
|
60746 | 48 |
type data = |
68813 | 49 |
{global: bool, |
60746 | 50 |
tables: tables, |
51 |
sml_tables: tables, |
|
52 |
breakpoints: (bool Unsynchronized.ref * Position.T) Inttab.table}; |
|
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
53 |
|
68813 | 54 |
fun make_data (global, tables, sml_tables, breakpoints) : data = |
55 |
{global = global, tables = tables, sml_tables = sml_tables, breakpoints = breakpoints}; |
|
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
56 |
|
33519 | 57 |
structure Env = Generic_Data |
31325 | 58 |
( |
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
59 |
type T = data |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
60 |
val empty = |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
61 |
make_data (true, |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
62 |
(Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty), |
62839
ea9f12e422c7
clarified SML name space: no access to structure PolyML;
wenzelm
parents:
62716
diff
changeset
|
63 |
(Symtab.make ML_Name_Space.sml_val, |
ea9f12e422c7
clarified SML name space: no access to structure PolyML;
wenzelm
parents:
62716
diff
changeset
|
64 |
Symtab.make ML_Name_Space.sml_type, |
ea9f12e422c7
clarified SML name space: no access to structure PolyML;
wenzelm
parents:
62716
diff
changeset
|
65 |
Symtab.make ML_Name_Space.sml_fixity, |
ea9f12e422c7
clarified SML name space: no access to structure PolyML;
wenzelm
parents:
62716
diff
changeset
|
66 |
Symtab.make ML_Name_Space.sml_structure, |
ea9f12e422c7
clarified SML name space: no access to structure PolyML;
wenzelm
parents:
62716
diff
changeset
|
67 |
Symtab.make ML_Name_Space.sml_signature, |
ea9f12e422c7
clarified SML name space: no access to structure PolyML;
wenzelm
parents:
62716
diff
changeset
|
68 |
Symtab.make ML_Name_Space.sml_functor), |
60746 | 69 |
Inttab.empty); |
70 |
fun extend (data : T) = make_data (false, #tables data, #sml_tables data, #breakpoints data); |
|
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
71 |
fun merge (data : T * T) = |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
72 |
make_data (false, |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
56618
diff
changeset
|
73 |
merge_tables (apply2 #tables data), |
60746 | 74 |
merge_tables (apply2 #sml_tables data), |
75 |
Inttab.merge (K true) (apply2 #breakpoints data)); |
|
31325 | 76 |
); |
77 |
||
78 |
val inherit = Env.put o Env.get; |
|
79 |
||
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59058
diff
changeset
|
80 |
fun forget_structure name = |
68813 | 81 |
Env.map (fn {global, tables, sml_tables, breakpoints} => |
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59058
diff
changeset
|
82 |
let |
68813 | 83 |
val _ = if global then ML_Name_Space.forget_structure name else (); |
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59058
diff
changeset
|
84 |
val tables' = |
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59058
diff
changeset
|
85 |
(#1 tables, #2 tables, #3 tables, Symtab.delete_safe name (#4 tables), #5 tables, #6 tables); |
68813 | 86 |
in make_data (global, tables', sml_tables, breakpoints) end); |
60746 | 87 |
|
62941 | 88 |
val get_breakpoint = Inttab.lookup o #breakpoints o Env.get; |
60746 | 89 |
|
62941 | 90 |
fun add_breakpoints more_breakpoints = |
91 |
if is_some (Context.get_generic_context ()) then |
|
92 |
Context.>> |
|
68813 | 93 |
(Env.map (fn {global, tables, sml_tables, breakpoints} => |
62941 | 94 |
let val breakpoints' = |
95 |
fold (Inttab.update_new o (apsnd o apsnd) Position.make) more_breakpoints breakpoints; |
|
68813 | 96 |
in make_data (global, tables, sml_tables, breakpoints') end)) |
62941 | 97 |
else (); |
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59058
diff
changeset
|
98 |
|
31328 | 99 |
|
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62889
diff
changeset
|
100 |
(* SML environment for Isabelle/ML *) |
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62889
diff
changeset
|
101 |
|
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62889
diff
changeset
|
102 |
val SML_environment = |
64556 | 103 |
Config.bool (Config.declare ("SML_environment", \<^here>) (fn _ => Config.Bool false)); |
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62889
diff
changeset
|
104 |
|
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62889
diff
changeset
|
105 |
fun sml_env SML = |
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62889
diff
changeset
|
106 |
SML orelse |
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62889
diff
changeset
|
107 |
(case Context.get_generic_context () of |
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62889
diff
changeset
|
108 |
NONE => false |
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62889
diff
changeset
|
109 |
| SOME context => Config.get_generic context SML_environment); |
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62889
diff
changeset
|
110 |
|
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62889
diff
changeset
|
111 |
|
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
112 |
(* name space *) |
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
113 |
|
62873
2f9c8a18f832
support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
wenzelm
parents:
62839
diff
changeset
|
114 |
val init_bootstrap = |
68813 | 115 |
Env.map (fn {global, tables, sml_tables, breakpoints} => |
62873
2f9c8a18f832
support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
wenzelm
parents:
62839
diff
changeset
|
116 |
let |
2f9c8a18f832
support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
wenzelm
parents:
62839
diff
changeset
|
117 |
val sml_tables' = |
2f9c8a18f832
support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
wenzelm
parents:
62839
diff
changeset
|
118 |
sml_tables |> (fn (val1, type1, fixity1, structure1, signature1, functor1) => |
2f9c8a18f832
support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
wenzelm
parents:
62839
diff
changeset
|
119 |
let |
2f9c8a18f832
support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
wenzelm
parents:
62839
diff
changeset
|
120 |
val val2 = |
2f9c8a18f832
support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
wenzelm
parents:
62839
diff
changeset
|
121 |
fold (fn (x, y) => |
62875 | 122 |
member (op =) ML_Name_Space.bootstrap_values x ? Symtab.update (x, y)) |
62873
2f9c8a18f832
support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
wenzelm
parents:
62839
diff
changeset
|
123 |
(#allVal ML_Name_Space.global ()) val1; |
2f9c8a18f832
support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
wenzelm
parents:
62839
diff
changeset
|
124 |
val structure2 = |
2f9c8a18f832
support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
wenzelm
parents:
62839
diff
changeset
|
125 |
fold (fn (x, y) => |
62875 | 126 |
member (op =) ML_Name_Space.bootstrap_structures x ? Symtab.update (x, y)) |
62873
2f9c8a18f832
support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
wenzelm
parents:
62839
diff
changeset
|
127 |
(#allStruct ML_Name_Space.global ()) structure1; |
62910
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
62902
diff
changeset
|
128 |
val signature2 = |
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
62902
diff
changeset
|
129 |
fold (fn (x, y) => |
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
62902
diff
changeset
|
130 |
member (op =) ML_Name_Space.bootstrap_signatures x ? Symtab.update (x, y)) |
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
62902
diff
changeset
|
131 |
(#allSig ML_Name_Space.global ()) signature1; |
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
62902
diff
changeset
|
132 |
in (val2, type1, fixity1, structure2, signature2, functor1) end); |
68813 | 133 |
in make_data (global, tables, sml_tables', breakpoints) end); |
62873
2f9c8a18f832
support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
wenzelm
parents:
62839
diff
changeset
|
134 |
|
68813 | 135 |
fun set_global global = |
68276 | 136 |
Env.map (fn {tables, sml_tables, breakpoints, ...} => |
68813 | 137 |
make_data (global, tables, sml_tables, breakpoints)); |
68276 | 138 |
|
68813 | 139 |
val restore_global = set_global o #global o Env.get; |
68276 | 140 |
|
60858 | 141 |
fun add_name_space {SML} (space: ML_Name_Space.T) = |
68813 | 142 |
Env.map (fn {global, tables, sml_tables, breakpoints} => |
60858 | 143 |
let |
144 |
val (tables', sml_tables') = |
|
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62889
diff
changeset
|
145 |
(tables, sml_tables) |> (if sml_env SML then apsnd else apfst) |
60858 | 146 |
(fn (val1, type1, fixity1, structure1, signature1, functor1) => |
147 |
let |
|
148 |
val val2 = fold Symtab.update (#allVal space ()) val1; |
|
149 |
val type2 = fold Symtab.update (#allType space ()) type1; |
|
150 |
val fixity2 = fold Symtab.update (#allFix space ()) fixity1; |
|
151 |
val structure2 = fold Symtab.update (#allStruct space ()) structure1; |
|
152 |
val signature2 = fold Symtab.update (#allSig space ()) signature1; |
|
153 |
val functor2 = fold Symtab.update (#allFunct space ()) functor1; |
|
154 |
in (val2, type2, fixity2, structure2, signature2, functor2) end); |
|
68813 | 155 |
in make_data (global, tables', sml_tables', breakpoints) end); |
60858 | 156 |
|
62495 | 157 |
fun make_name_space {SML, exchange} : ML_Name_Space.T = |
31325 | 158 |
let |
159 |
fun lookup sel1 sel2 name = |
|
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62889
diff
changeset
|
160 |
if sml_env SML then |
62876 | 161 |
Context.the_generic_context () |
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
162 |
|> (fn context => Symtab.lookup (sel1 (#sml_tables (Env.get context))) name) |
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
163 |
else |
62889 | 164 |
Context.get_generic_context () |
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
165 |
|> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name) |
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
166 |
|> (fn NONE => sel2 ML_Name_Space.global name | some => some); |
31325 | 167 |
|
168 |
fun all sel1 sel2 () = |
|
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62889
diff
changeset
|
169 |
(if sml_env SML then |
62876 | 170 |
Context.the_generic_context () |
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
171 |
|> (fn context => Symtab.dest (sel1 (#sml_tables (Env.get context)))) |
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
172 |
else |
62889 | 173 |
Context.get_generic_context () |
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
174 |
|> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context)))) |
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
175 |
|> append (sel2 ML_Name_Space.global ())) |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
56618
diff
changeset
|
176 |
|> sort_distinct (string_ord o apply2 #1); |
31325 | 177 |
|
178 |
fun enter ap1 sel2 entry = |
|
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62889
diff
changeset
|
179 |
if sml_env SML <> exchange then |
68813 | 180 |
Context.>> (Env.map (fn {global, tables, sml_tables, breakpoints} => |
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
181 |
let val sml_tables' = ap1 (Symtab.update entry) sml_tables |
68813 | 182 |
in make_data (global, tables, sml_tables', breakpoints) end)) |
62889 | 183 |
else if is_some (Context.get_generic_context ()) then |
68813 | 184 |
Context.>> (Env.map (fn {global, tables, sml_tables, breakpoints} => |
56203
76c72f4d0667
clarified bootstrap process: switch to ML with context and antiquotations earlier;
wenzelm
parents:
48992
diff
changeset
|
185 |
let |
68813 | 186 |
val _ = if global then sel2 ML_Name_Space.global entry else (); |
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
187 |
val tables' = ap1 (Symtab.update entry) tables; |
68813 | 188 |
in make_data (global, tables', sml_tables, breakpoints) end)) |
31325 | 189 |
else sel2 ML_Name_Space.global entry; |
190 |
in |
|
191 |
{lookupVal = lookup #1 #lookupVal, |
|
192 |
lookupType = lookup #2 #lookupType, |
|
193 |
lookupFix = lookup #3 #lookupFix, |
|
194 |
lookupStruct = lookup #4 #lookupStruct, |
|
195 |
lookupSig = lookup #5 #lookupSig, |
|
196 |
lookupFunct = lookup #6 #lookupFunct, |
|
197 |
enterVal = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)) #enterVal, |
|
198 |
enterType = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)) #enterType, |
|
199 |
enterFix = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)) #enterFix, |
|
200 |
enterStruct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)) #enterStruct, |
|
201 |
enterSig = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)) #enterSig, |
|
202 |
enterFunct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)) #enterFunct, |
|
203 |
allVal = all #1 #allVal, |
|
204 |
allType = all #2 #allType, |
|
205 |
allFix = all #3 #allFix, |
|
206 |
allStruct = all #4 #allStruct, |
|
207 |
allSig = all #5 #allSig, |
|
208 |
allFunct = all #6 #allFunct} |
|
209 |
end; |
|
210 |
||
62495 | 211 |
val context: ML_Compiler0.context = |
212 |
{name_space = make_name_space {SML = false, exchange = false}, |
|
62716
d80b9f4990e4
explicit print_depth for the sake of Spec_Check.determine_type;
wenzelm
parents:
62657
diff
changeset
|
213 |
print_depth = NONE, |
62493 | 214 |
here = Position.here oo Position.line_file, |
31325 | 215 |
print = writeln, |
216 |
error = error}; |
|
217 |
||
62495 | 218 |
val name_space = #name_space context; |
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
219 |
|
62495 | 220 |
val is_functor = is_some o #lookupFunct name_space; |
36163
823c9400eb62
proper checking of ML functors (in Poly/ML 5.2 or later);
wenzelm
parents:
33519
diff
changeset
|
221 |
|
823c9400eb62
proper checking of ML functors (in Poly/ML 5.2 or later);
wenzelm
parents:
33519
diff
changeset
|
222 |
fun check_functor name = |
36165 | 223 |
if not (is_functor "Table") (*mask dummy version of name_space*) orelse is_functor name then () |
36163
823c9400eb62
proper checking of ML functors (in Poly/ML 5.2 or later);
wenzelm
parents:
33519
diff
changeset
|
224 |
else error ("Unknown ML functor: " ^ quote name); |
823c9400eb62
proper checking of ML functors (in Poly/ML 5.2 or later);
wenzelm
parents:
33519
diff
changeset
|
225 |
|
31325 | 226 |
end; |