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