--- a/src/Pure/ML/ml_env.ML Tue Mar 25 10:37:10 2014 +0100
+++ b/src/Pure/ML/ml_env.ML Tue Mar 25 13:18:10 2014 +0100
@@ -1,12 +1,14 @@
(* Title: Pure/ML/ml_env.ML
Author: Makarius
-Local environment of ML results.
+Toplevel environment for Standard ML and Isabelle/ML within the
+implicit context.
*)
signature ML_ENV =
sig
val inherit: Context.generic -> Context.generic -> Context.generic
+ val SML_name_space: ML_Name_Space.T
val name_space: ML_Name_Space.T
val local_context: use_context
val check_functor: string -> unit
@@ -17,56 +19,112 @@
(* context data *)
+type tables =
+ ML_Name_Space.valueVal Symtab.table *
+ ML_Name_Space.typeVal Symtab.table *
+ ML_Name_Space.fixityVal Symtab.table *
+ ML_Name_Space.structureVal Symtab.table *
+ ML_Name_Space.signatureVal Symtab.table *
+ ML_Name_Space.functorVal Symtab.table;
+
+fun merge_tables
+ ((val1, type1, fixity1, structure1, signature1, functor1),
+ (val2, type2, fixity2, structure2, signature2, functor2)) : tables =
+ (Symtab.merge (K true) (val1, val2),
+ Symtab.merge (K true) (type1, type2),
+ Symtab.merge (K true) (fixity1, fixity2),
+ Symtab.merge (K true) (structure1, structure2),
+ Symtab.merge (K true) (signature1, signature2),
+ Symtab.merge (K true) (functor1, functor2));
+
+type data = {bootstrap: bool, tables: tables, sml_tables: tables};
+
+fun make_data (bootstrap, tables, sml_tables) : data =
+ {bootstrap = bootstrap, tables = tables, sml_tables = sml_tables};
+
structure Env = Generic_Data
(
- type T =
- bool * (*global bootstrap environment*)
- (ML_Name_Space.valueVal Symtab.table *
- ML_Name_Space.typeVal Symtab.table *
- ML_Name_Space.fixityVal Symtab.table *
- ML_Name_Space.structureVal Symtab.table *
- ML_Name_Space.signatureVal Symtab.table *
- ML_Name_Space.functorVal Symtab.table);
- val empty : T =
- (true, (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty));
- fun extend (_, tabs) : T = (false, tabs);
- fun merge
- ((_, (val1, type1, fixity1, structure1, signature1, functor1)),
- (_, (val2, type2, fixity2, structure2, signature2, functor2))) : T =
- (false,
- (Symtab.merge (K true) (val1, val2),
- Symtab.merge (K true) (type1, type2),
- Symtab.merge (K true) (fixity1, fixity2),
- Symtab.merge (K true) (structure1, structure2),
- Symtab.merge (K true) (signature1, signature2),
- Symtab.merge (K true) (functor1, functor2)));
+ type T = data
+ val empty =
+ make_data (true,
+ (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty),
+ (Symtab.make ML_Name_Space.initial_val,
+ Symtab.make ML_Name_Space.initial_type,
+ Symtab.make ML_Name_Space.initial_fixity,
+ Symtab.make ML_Name_Space.initial_structure,
+ Symtab.make ML_Name_Space.initial_signature,
+ Symtab.make ML_Name_Space.initial_functor));
+ fun extend (data : T) = make_data (false, #tables data, #sml_tables data);
+ fun merge (data : T * T) =
+ make_data (false,
+ merge_tables (pairself #tables data),
+ merge_tables (pairself #sml_tables data));
);
val inherit = Env.put o Env.get;
-(* results *)
+(* SML name space *)
+
+val SML_name_space: ML_Name_Space.T =
+ let
+ fun lookup which name =
+ Context.the_thread_data ()
+ |> (fn context => Symtab.lookup (which (#sml_tables (Env.get context))) name);
+
+ fun all which () =
+ Context.the_thread_data ()
+ |> (fn context => Symtab.dest (which (#sml_tables (Env.get context))))
+ |> sort_distinct (string_ord o pairself #1);
+
+ fun enter which entry =
+ Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
+ let val sml_tables' = which (Symtab.update entry) sml_tables
+ in make_data (bootstrap, tables, sml_tables') end));
+ in
+ {lookupVal = lookup #1,
+ lookupType = lookup #2,
+ lookupFix = lookup #3,
+ lookupStruct = lookup #4,
+ lookupSig = lookup #5,
+ lookupFunct = lookup #6,
+ enterVal = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)),
+ enterType = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)),
+ enterFix = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)),
+ enterStruct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)),
+ enterSig = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)),
+ enterFunct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)),
+ allVal = all #1,
+ allType = all #2,
+ allFix = all #3,
+ allStruct = all #4,
+ allSig = all #5,
+ allFunct = all #6}
+ end;
+
+
+(* Isabelle/ML name space *)
val name_space: ML_Name_Space.T =
let
fun lookup sel1 sel2 name =
Context.thread_data ()
- |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#2 (Env.get context))) name)
+ |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
|> (fn NONE => sel2 ML_Name_Space.global name | some => some);
fun all sel1 sel2 () =
Context.thread_data ()
- |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#2 (Env.get context))))
+ |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
|> append (sel2 ML_Name_Space.global ())
|> sort_distinct (string_ord o pairself #1);
fun enter ap1 sel2 entry =
if is_some (Context.thread_data ()) then
- Context.>> (Env.map (fn (global, tabs) =>
+ Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
let
- val _ = if global then sel2 ML_Name_Space.global entry else ();
- val tabs' = ap1 (Symtab.update entry) tabs;
- in (global, tabs') end))
+ val _ = if bootstrap then sel2 ML_Name_Space.global entry else ();
+ val tables' = ap1 (Symtab.update entry) tables;
+ in make_data (bootstrap, tables', sml_tables) end))
else sel2 ML_Name_Space.global entry;
in
{lookupVal = lookup #1 #lookupVal,