1(*  Title:      Pure/ML/ml_env.ML
2    Author:     Makarius
3
4Toplevel environment for Standard ML and Isabelle/ML within the
5implicit context.
6*)
7
8signature ML_ENV =
9sig
10  val inherit: Context.generic -> Context.generic -> Context.generic
11  val forget_structure: string -> Context.generic -> Context.generic
12  val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option
13  val add_breakpoints: (serial * (bool Unsynchronized.ref * Thread_Position.T)) list -> unit
14  val init_bootstrap: Context.generic -> Context.generic
15  val SML_environment: bool Config.T
16  val set_bootstrap: bool -> Context.generic -> Context.generic
17  val restore_bootstrap: Context.generic -> Context.generic -> Context.generic
18  val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic
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
22  val check_functor: string -> unit
23end
24
25structure ML_Env: ML_ENV =
26struct
27
28(* context data *)
29
30type tables =
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;
37
38fun merge_tables
39  ((val1, type1, fixity1, structure1, signature1, functor1),
40   (val2, type2, fixity2, structure2, signature2, functor2)) : tables =
41  (Symtab.merge (K true) (val1, val2),
42   Symtab.merge (K true) (type1, type2),
43   Symtab.merge (K true) (fixity1, fixity2),
44   Symtab.merge (K true) (structure1, structure2),
45   Symtab.merge (K true) (signature1, signature2),
46   Symtab.merge (K true) (functor1, functor2));
47
48type data =
49 {bootstrap: bool,
50  tables: tables,
51  sml_tables: tables,
52  breakpoints: (bool Unsynchronized.ref * Position.T) Inttab.table};
53
54fun make_data (bootstrap, tables, sml_tables, breakpoints) : data =
55  {bootstrap = bootstrap, tables = tables, sml_tables = sml_tables, breakpoints = breakpoints};
56
57structure Env = Generic_Data
58(
59  type T = data
60  val empty =
61    make_data (true,
62      (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty),
63      (Symtab.make ML_Name_Space.sml_val,
64       Symtab.make ML_Name_Space.sml_type,
65       Symtab.make ML_Name_Space.sml_fixity,
66       Symtab.make ML_Name_Space.sml_structure,
67       Symtab.make ML_Name_Space.sml_signature,
68       Symtab.make ML_Name_Space.sml_functor),
69      Inttab.empty);
70  fun extend (data : T) = make_data (false, #tables data, #sml_tables data, #breakpoints data);
71  fun merge (data : T * T) =
72    make_data (false,
73      merge_tables (apply2 #tables data),
74      merge_tables (apply2 #sml_tables data),
75      Inttab.merge (K true) (apply2 #breakpoints data));
76);
77
78val inherit = Env.put o Env.get;
79
80fun forget_structure name =
81  Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
82    let
83      val _ = if bootstrap then ML_Name_Space.forget_structure name else ();
84      val tables' =
85        (#1 tables, #2 tables, #3 tables, Symtab.delete_safe name (#4 tables), #5 tables, #6 tables);
86    in make_data (bootstrap, tables', sml_tables, breakpoints) end);
87
88val get_breakpoint = Inttab.lookup o #breakpoints o Env.get;
89
90fun add_breakpoints more_breakpoints =
91  if is_some (Context.get_generic_context ()) then
92    Context.>>
93      (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
94        let val breakpoints' =
95          fold (Inttab.update_new o (apsnd o apsnd) Position.make) more_breakpoints breakpoints;
96        in make_data (bootstrap, tables, sml_tables, breakpoints') end))
97  else ();
98
99
100(* SML environment for Isabelle/ML *)
101
102val SML_environment =
103  Config.bool (Config.declare ("SML_environment", \<^here>) (fn _ => Config.Bool false));
104
105fun sml_env SML =
106  SML orelse
107    (case Context.get_generic_context () of
108      NONE => false
109    | SOME context => Config.get_generic context SML_environment);
110
111
112(* name space *)
113
114val init_bootstrap =
115  Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
116    let
117      val sml_tables' =
118        sml_tables |> (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
119            let
120              val val2 =
121                fold (fn (x, y) =>
122                  member (op =) ML_Name_Space.bootstrap_values x ? Symtab.update (x, y))
123                (#allVal ML_Name_Space.global ()) val1;
124              val structure2 =
125                fold (fn (x, y) =>
126                  member (op =) ML_Name_Space.bootstrap_structures x ? Symtab.update (x, y))
127                (#allStruct ML_Name_Space.global ()) structure1;
128              val signature2 =
129                fold (fn (x, y) =>
130                  member (op =) ML_Name_Space.bootstrap_signatures x ? Symtab.update (x, y))
131                (#allSig ML_Name_Space.global ()) signature1;
132            in (val2, type1, fixity1, structure2, signature2, functor1) end);
133    in make_data (bootstrap, tables, sml_tables', breakpoints) end);
134
135fun set_bootstrap bootstrap =
136  Env.map (fn {tables, sml_tables, breakpoints, ...} =>
137    make_data (bootstrap, tables, sml_tables, breakpoints));
138
139val restore_bootstrap = set_bootstrap o #bootstrap o Env.get;
140
141fun add_name_space {SML} (space: ML_Name_Space.T) =
142  Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
143    let
144      val (tables', sml_tables') =
145        (tables, sml_tables) |> (if sml_env SML then apsnd else apfst)
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);
155    in make_data (bootstrap, tables', sml_tables', breakpoints) end);
156
157fun make_name_space {SML, exchange} : ML_Name_Space.T =
158  let
159    fun lookup sel1 sel2 name =
160      if sml_env SML then
161        Context.the_generic_context ()
162        |> (fn context => Symtab.lookup (sel1 (#sml_tables (Env.get context))) name)
163      else
164        Context.get_generic_context ()
165        |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
166        |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
167
168    fun all sel1 sel2 () =
169      (if sml_env SML then
170        Context.the_generic_context ()
171        |> (fn context => Symtab.dest (sel1 (#sml_tables (Env.get context))))
172      else
173        Context.get_generic_context ()
174        |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
175        |> append (sel2 ML_Name_Space.global ()))
176      |> sort_distinct (string_ord o apply2 #1);
177
178    fun enter ap1 sel2 entry =
179      if sml_env SML <> exchange then
180        Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
181          let val sml_tables' = ap1 (Symtab.update entry) sml_tables
182          in make_data (bootstrap, tables, sml_tables', breakpoints) end))
183      else if is_some (Context.get_generic_context ()) then
184        Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
185          let
186            val _ = if bootstrap then sel2 ML_Name_Space.global entry else ();
187            val tables' = ap1 (Symtab.update entry) tables;
188          in make_data (bootstrap, tables', sml_tables, breakpoints) end))
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
211val context: ML_Compiler0.context =
212 {name_space = make_name_space {SML = false, exchange = false},
213  print_depth = NONE,
214  here = Position.here oo Position.line_file,
215  print = writeln,
216  error = error};
217
218val name_space = #name_space context;
219
220val is_functor = is_some o #lookupFunct name_space;
221
222fun check_functor name =
223  if not (is_functor "Table") (*mask dummy version of name_space*) orelse is_functor name then ()
224  else error ("Unknown ML functor: " ^ quote name);
225
226end;
227