author | wenzelm |
Fri, 17 Jul 2015 17:17:39 +0200 | |
changeset 60746 | 8cf877aca29a |
parent 59127 | 723b11f8ffbf |
child 60858 | 7bf2188a0998 |
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 add_breakpoint: serial * (bool Unsynchronized.ref * Position.T) -> |
13 |
Context.generic -> Context.generic |
|
14 |
val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option |
|
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
15 |
val name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T |
31325 | 16 |
val local_context: use_context |
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
17 |
val local_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
|
18 |
val check_functor: string -> unit |
31325 | 19 |
end |
20 |
||
21 |
structure ML_Env: ML_ENV = |
|
22 |
struct |
|
23 |
||
31328 | 24 |
(* context data *) |
25 |
||
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
26 |
type tables = |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
27 |
ML_Name_Space.valueVal Symtab.table * |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
28 |
ML_Name_Space.typeVal Symtab.table * |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
29 |
ML_Name_Space.fixityVal Symtab.table * |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
30 |
ML_Name_Space.structureVal Symtab.table * |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
31 |
ML_Name_Space.signatureVal Symtab.table * |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
32 |
ML_Name_Space.functorVal Symtab.table; |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
33 |
|
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
34 |
fun merge_tables |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
35 |
((val1, type1, fixity1, structure1, signature1, functor1), |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
36 |
(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
|
37 |
(Symtab.merge (K true) (val1, val2), |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
38 |
Symtab.merge (K true) (type1, type2), |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
39 |
Symtab.merge (K true) (fixity1, fixity2), |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
40 |
Symtab.merge (K true) (structure1, structure2), |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
41 |
Symtab.merge (K true) (signature1, signature2), |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
42 |
Symtab.merge (K true) (functor1, functor2)); |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
43 |
|
60746 | 44 |
type data = |
45 |
{bootstrap: bool, |
|
46 |
tables: tables, |
|
47 |
sml_tables: tables, |
|
48 |
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
|
49 |
|
60746 | 50 |
fun make_data (bootstrap, tables, sml_tables, breakpoints) : data = |
51 |
{bootstrap = bootstrap, 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
|
52 |
|
33519 | 53 |
structure Env = Generic_Data |
31325 | 54 |
( |
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
55 |
type T = data |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
56 |
val empty = |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
57 |
make_data (true, |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
58 |
(Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty), |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
59 |
(Symtab.make ML_Name_Space.initial_val, |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
60 |
Symtab.make ML_Name_Space.initial_type, |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
61 |
Symtab.make ML_Name_Space.initial_fixity, |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
62 |
Symtab.make ML_Name_Space.initial_structure, |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
63 |
Symtab.make ML_Name_Space.initial_signature, |
60746 | 64 |
Symtab.make ML_Name_Space.initial_functor), |
65 |
Inttab.empty); |
|
66 |
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
|
67 |
fun merge (data : T * T) = |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
68 |
make_data (false, |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
56618
diff
changeset
|
69 |
merge_tables (apply2 #tables data), |
60746 | 70 |
merge_tables (apply2 #sml_tables data), |
71 |
Inttab.merge (K true) (apply2 #breakpoints data)); |
|
31325 | 72 |
); |
73 |
||
74 |
val inherit = Env.put o Env.get; |
|
75 |
||
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59058
diff
changeset
|
76 |
fun forget_structure name = |
60746 | 77 |
Env.map (fn {bootstrap, tables, sml_tables, breakpoints} => |
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59058
diff
changeset
|
78 |
let |
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59058
diff
changeset
|
79 |
val _ = if bootstrap then ML_Name_Space.forget_global_structure name else (); |
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59058
diff
changeset
|
80 |
val tables' = |
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59058
diff
changeset
|
81 |
(#1 tables, #2 tables, #3 tables, Symtab.delete_safe name (#4 tables), #5 tables, #6 tables); |
60746 | 82 |
in make_data (bootstrap, tables', sml_tables, breakpoints) end); |
83 |
||
84 |
fun add_breakpoint breakpoint = |
|
85 |
Env.map (fn {bootstrap, tables, sml_tables, breakpoints} => |
|
86 |
let val breakpoints' = Inttab.update_new breakpoint breakpoints; |
|
87 |
in make_data (bootstrap, tables, sml_tables, breakpoints') end); |
|
88 |
||
89 |
val get_breakpoint = Inttab.lookup o #breakpoints o Env.get; |
|
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59058
diff
changeset
|
90 |
|
31328 | 91 |
|
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
92 |
(* name space *) |
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
93 |
|
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
94 |
fun name_space {SML, exchange} : ML_Name_Space.T = |
31325 | 95 |
let |
96 |
fun lookup sel1 sel2 name = |
|
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
97 |
if SML then |
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
98 |
Context.the_thread_data () |
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
99 |
|> (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
|
100 |
else |
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
101 |
Context.thread_data () |
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
102 |
|> (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
|
103 |
|> (fn NONE => sel2 ML_Name_Space.global name | some => some); |
31325 | 104 |
|
105 |
fun all sel1 sel2 () = |
|
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
106 |
(if SML then |
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
107 |
Context.the_thread_data () |
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
108 |
|> (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
|
109 |
else |
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
110 |
Context.thread_data () |
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
111 |
|> (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
|
112 |
|> append (sel2 ML_Name_Space.global ())) |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
56618
diff
changeset
|
113 |
|> sort_distinct (string_ord o apply2 #1); |
31325 | 114 |
|
115 |
fun enter ap1 sel2 entry = |
|
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
116 |
if SML <> exchange then |
60746 | 117 |
Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} => |
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
118 |
let val sml_tables' = ap1 (Symtab.update entry) sml_tables |
60746 | 119 |
in make_data (bootstrap, tables, sml_tables', breakpoints) end)) |
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
120 |
else if is_some (Context.thread_data ()) then |
60746 | 121 |
Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} => |
56203
76c72f4d0667
clarified bootstrap process: switch to ML with context and antiquotations earlier;
wenzelm
parents:
48992
diff
changeset
|
122 |
let |
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
123 |
val _ = if bootstrap then sel2 ML_Name_Space.global entry else (); |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
124 |
val tables' = ap1 (Symtab.update entry) tables; |
60746 | 125 |
in make_data (bootstrap, tables', sml_tables, breakpoints) end)) |
31325 | 126 |
else sel2 ML_Name_Space.global entry; |
127 |
in |
|
128 |
{lookupVal = lookup #1 #lookupVal, |
|
129 |
lookupType = lookup #2 #lookupType, |
|
130 |
lookupFix = lookup #3 #lookupFix, |
|
131 |
lookupStruct = lookup #4 #lookupStruct, |
|
132 |
lookupSig = lookup #5 #lookupSig, |
|
133 |
lookupFunct = lookup #6 #lookupFunct, |
|
134 |
enterVal = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)) #enterVal, |
|
135 |
enterType = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)) #enterType, |
|
136 |
enterFix = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)) #enterFix, |
|
137 |
enterStruct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)) #enterStruct, |
|
138 |
enterSig = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)) #enterSig, |
|
139 |
enterFunct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)) #enterFunct, |
|
140 |
allVal = all #1 #allVal, |
|
141 |
allType = all #2 #allType, |
|
142 |
allFix = all #3 #allFix, |
|
143 |
allStruct = all #4 #allStruct, |
|
144 |
allSig = all #5 #allSig, |
|
145 |
allFunct = all #6 #allFunct} |
|
146 |
end; |
|
147 |
||
148 |
val local_context: use_context = |
|
149 |
{tune_source = ML_Parse.fix_ints, |
|
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
150 |
name_space = name_space {SML = false, exchange = false}, |
48992 | 151 |
str_of_pos = Position.here oo Position.line_file, |
31325 | 152 |
print = writeln, |
153 |
error = error}; |
|
154 |
||
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
155 |
val local_name_space = #name_space local_context; |
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
156 |
|
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
157 |
val is_functor = is_some o #lookupFunct local_name_space; |
36163
823c9400eb62
proper checking of ML functors (in Poly/ML 5.2 or later);
wenzelm
parents:
33519
diff
changeset
|
158 |
|
823c9400eb62
proper checking of ML functors (in Poly/ML 5.2 or later);
wenzelm
parents:
33519
diff
changeset
|
159 |
fun check_functor name = |
36165 | 160 |
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
|
161 |
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
|
162 |
|
31325 | 163 |
end; |