src/Pure/ML/ml_env.ML
author wenzelm
Sat Apr 19 17:23:05 2014 +0200 (2014-04-19)
changeset 56618 874bdedb2313
parent 56275 600f432ab556
child 59058 a78612c67ec0
permissions -rw-r--r--
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
     1 (*  Title:      Pure/ML/ml_env.ML
     2     Author:     Makarius
     3 
     4 Toplevel environment for Standard ML and Isabelle/ML within the
     5 implicit context.
     6 *)
     7 
     8 signature ML_ENV =
     9 sig
    10   val inherit: Context.generic -> Context.generic -> Context.generic
    11   val name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
    12   val local_context: use_context
    13   val local_name_space: ML_Name_Space.T
    14   val check_functor: string -> unit
    15 end
    16 
    17 structure ML_Env: ML_ENV =
    18 struct
    19 
    20 (* context data *)
    21 
    22 type tables =
    23   ML_Name_Space.valueVal Symtab.table *
    24   ML_Name_Space.typeVal Symtab.table *
    25   ML_Name_Space.fixityVal Symtab.table *
    26   ML_Name_Space.structureVal Symtab.table *
    27   ML_Name_Space.signatureVal Symtab.table *
    28   ML_Name_Space.functorVal Symtab.table;
    29 
    30 fun merge_tables
    31   ((val1, type1, fixity1, structure1, signature1, functor1),
    32    (val2, type2, fixity2, structure2, signature2, functor2)) : tables =
    33   (Symtab.merge (K true) (val1, val2),
    34    Symtab.merge (K true) (type1, type2),
    35    Symtab.merge (K true) (fixity1, fixity2),
    36    Symtab.merge (K true) (structure1, structure2),
    37    Symtab.merge (K true) (signature1, signature2),
    38    Symtab.merge (K true) (functor1, functor2));
    39 
    40 type data = {bootstrap: bool, tables: tables, sml_tables: tables};
    41 
    42 fun make_data (bootstrap, tables, sml_tables) : data =
    43   {bootstrap = bootstrap, tables = tables, sml_tables = sml_tables};
    44 
    45 structure Env = Generic_Data
    46 (
    47   type T = data
    48   val empty =
    49     make_data (true,
    50       (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty),
    51       (Symtab.make ML_Name_Space.initial_val,
    52        Symtab.make ML_Name_Space.initial_type,
    53        Symtab.make ML_Name_Space.initial_fixity,
    54        Symtab.make ML_Name_Space.initial_structure,
    55        Symtab.make ML_Name_Space.initial_signature,
    56        Symtab.make ML_Name_Space.initial_functor));
    57   fun extend (data : T) = make_data (false, #tables data, #sml_tables data);
    58   fun merge (data : T * T) =
    59     make_data (false,
    60       merge_tables (pairself #tables data),
    61       merge_tables (pairself #sml_tables data));
    62 );
    63 
    64 val inherit = Env.put o Env.get;
    65 
    66 
    67 (* name space *)
    68 
    69 fun name_space {SML, exchange} : ML_Name_Space.T =
    70   let
    71     fun lookup sel1 sel2 name =
    72       if SML then
    73         Context.the_thread_data ()
    74         |> (fn context => Symtab.lookup (sel1 (#sml_tables (Env.get context))) name)
    75       else
    76         Context.thread_data ()
    77         |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
    78         |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
    79 
    80     fun all sel1 sel2 () =
    81       (if SML then
    82         Context.the_thread_data ()
    83         |> (fn context => Symtab.dest (sel1 (#sml_tables (Env.get context))))
    84       else
    85         Context.thread_data ()
    86         |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
    87         |> append (sel2 ML_Name_Space.global ()))
    88       |> sort_distinct (string_ord o pairself #1);
    89 
    90     fun enter ap1 sel2 entry =
    91       if SML <> exchange then
    92         Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
    93           let val sml_tables' = ap1 (Symtab.update entry) sml_tables
    94           in make_data (bootstrap, tables, sml_tables') end))
    95       else if is_some (Context.thread_data ()) then
    96         Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
    97           let
    98             val _ = if bootstrap then sel2 ML_Name_Space.global entry else ();
    99             val tables' = ap1 (Symtab.update entry) tables;
   100           in make_data (bootstrap, tables', sml_tables) end))
   101       else sel2 ML_Name_Space.global entry;
   102   in
   103    {lookupVal    = lookup #1 #lookupVal,
   104     lookupType   = lookup #2 #lookupType,
   105     lookupFix    = lookup #3 #lookupFix,
   106     lookupStruct = lookup #4 #lookupStruct,
   107     lookupSig    = lookup #5 #lookupSig,
   108     lookupFunct  = lookup #6 #lookupFunct,
   109     enterVal     = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)) #enterVal,
   110     enterType    = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)) #enterType,
   111     enterFix     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)) #enterFix,
   112     enterStruct  = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)) #enterStruct,
   113     enterSig     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)) #enterSig,
   114     enterFunct   = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)) #enterFunct,
   115     allVal       = all #1 #allVal,
   116     allType      = all #2 #allType,
   117     allFix       = all #3 #allFix,
   118     allStruct    = all #4 #allStruct,
   119     allSig       = all #5 #allSig,
   120     allFunct     = all #6 #allFunct}
   121   end;
   122 
   123 val local_context: use_context =
   124  {tune_source = ML_Parse.fix_ints,
   125   name_space = name_space {SML = false, exchange = false},
   126   str_of_pos = Position.here oo Position.line_file,
   127   print = writeln,
   128   error = error};
   129 
   130 val local_name_space = #name_space local_context;
   131 
   132 val is_functor = is_some o #lookupFunct local_name_space;
   133 
   134 fun check_functor name =
   135   if not (is_functor "Table") (*mask dummy version of name_space*) orelse is_functor name then ()
   136   else error ("Unknown ML functor: " ^ quote name);
   137 
   138 end;
   139