src/Pure/ML/ml_env.ML
author wenzelm
Tue Mar 25 13:18:10 2014 +0100 (2014-03-25 ago)
changeset 56275 600f432ab556
parent 56203 76c72f4d0667
child 56618 874bdedb2313
permissions -rw-r--r--
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
     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 SML_name_space: ML_Name_Space.T
    12   val name_space: ML_Name_Space.T
    13   val local_context: use_context
    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 (* SML name space *)
    68 
    69 val SML_name_space: ML_Name_Space.T =
    70   let
    71     fun lookup which name =
    72       Context.the_thread_data ()
    73       |> (fn context => Symtab.lookup (which (#sml_tables (Env.get context))) name);
    74 
    75     fun all which () =
    76       Context.the_thread_data ()
    77       |> (fn context => Symtab.dest (which (#sml_tables (Env.get context))))
    78       |> sort_distinct (string_ord o pairself #1);
    79 
    80     fun enter which entry =
    81       Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
    82         let val sml_tables' = which (Symtab.update entry) sml_tables
    83         in make_data (bootstrap, tables, sml_tables') end));
    84   in
    85    {lookupVal    = lookup #1,
    86     lookupType   = lookup #2,
    87     lookupFix    = lookup #3,
    88     lookupStruct = lookup #4,
    89     lookupSig    = lookup #5,
    90     lookupFunct  = lookup #6,
    91     enterVal     = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)),
    92     enterType    = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)),
    93     enterFix     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)),
    94     enterStruct  = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)),
    95     enterSig     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)),
    96     enterFunct   = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)),
    97     allVal       = all #1,
    98     allType      = all #2,
    99     allFix       = all #3,
   100     allStruct    = all #4,
   101     allSig       = all #5,
   102     allFunct     = all #6}
   103   end;
   104 
   105 
   106 (* Isabelle/ML name space *)
   107 
   108 val name_space: ML_Name_Space.T =
   109   let
   110     fun lookup sel1 sel2 name =
   111       Context.thread_data ()
   112       |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
   113       |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
   114 
   115     fun all sel1 sel2 () =
   116       Context.thread_data ()
   117       |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
   118       |> append (sel2 ML_Name_Space.global ())
   119       |> sort_distinct (string_ord o pairself #1);
   120 
   121     fun enter ap1 sel2 entry =
   122       if is_some (Context.thread_data ()) then
   123         Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
   124           let
   125             val _ = if bootstrap then sel2 ML_Name_Space.global entry else ();
   126             val tables' = ap1 (Symtab.update entry) tables;
   127           in make_data (bootstrap, tables', sml_tables) end))
   128       else sel2 ML_Name_Space.global entry;
   129   in
   130    {lookupVal    = lookup #1 #lookupVal,
   131     lookupType   = lookup #2 #lookupType,
   132     lookupFix    = lookup #3 #lookupFix,
   133     lookupStruct = lookup #4 #lookupStruct,
   134     lookupSig    = lookup #5 #lookupSig,
   135     lookupFunct  = lookup #6 #lookupFunct,
   136     enterVal     = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)) #enterVal,
   137     enterType    = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)) #enterType,
   138     enterFix     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)) #enterFix,
   139     enterStruct  = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)) #enterStruct,
   140     enterSig     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)) #enterSig,
   141     enterFunct   = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)) #enterFunct,
   142     allVal       = all #1 #allVal,
   143     allType      = all #2 #allType,
   144     allFix       = all #3 #allFix,
   145     allStruct    = all #4 #allStruct,
   146     allSig       = all #5 #allSig,
   147     allFunct     = all #6 #allFunct}
   148   end;
   149 
   150 val local_context: use_context =
   151  {tune_source = ML_Parse.fix_ints,
   152   name_space = name_space,
   153   str_of_pos = Position.here oo Position.line_file,
   154   print = writeln,
   155   error = error};
   156 
   157 val is_functor = is_some o #lookupFunct name_space;
   158 
   159 fun check_functor name =
   160   if not (is_functor "Table") (*mask dummy version of name_space*) orelse is_functor name then ()
   161   else error ("Unknown ML functor: " ^ quote name);
   162 
   163 end;
   164