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