src/Pure/ML/ml_env.ML
author wenzelm
Thu Aug 02 12:36:54 2012 +0200 (2012-08-02)
changeset 48646 91281e9472d8
parent 36165 310a3f2f0e7e
child 48992 0518bf89c777
permissions -rw-r--r--
more official command specifications, including source position;
wenzelm@31325
     1
(*  Title:      Pure/ML/ml_env.ML
wenzelm@31325
     2
    Author:     Makarius
wenzelm@31325
     3
wenzelm@31470
     4
Local environment of ML results.
wenzelm@31325
     5
*)
wenzelm@31325
     6
wenzelm@31325
     7
signature ML_ENV =
wenzelm@31325
     8
sig
wenzelm@31325
     9
  val inherit: Context.generic -> Context.generic -> Context.generic
wenzelm@31325
    10
  val name_space: ML_Name_Space.T
wenzelm@31325
    11
  val local_context: use_context
wenzelm@36163
    12
  val check_functor: string -> unit
wenzelm@31325
    13
end
wenzelm@31325
    14
wenzelm@31325
    15
structure ML_Env: ML_ENV =
wenzelm@31325
    16
struct
wenzelm@31325
    17
wenzelm@31328
    18
(* context data *)
wenzelm@31328
    19
wenzelm@33519
    20
structure Env = Generic_Data
wenzelm@31325
    21
(
wenzelm@31325
    22
  type T =
wenzelm@31430
    23
    ML_Name_Space.valueVal Symtab.table *
wenzelm@31430
    24
    ML_Name_Space.typeVal Symtab.table *
wenzelm@31430
    25
    ML_Name_Space.fixityVal Symtab.table *
wenzelm@31430
    26
    ML_Name_Space.structureVal Symtab.table *
wenzelm@31430
    27
    ML_Name_Space.signatureVal Symtab.table *
wenzelm@31430
    28
    ML_Name_Space.functorVal Symtab.table;
wenzelm@31430
    29
  val empty = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty);
wenzelm@31325
    30
  val extend = I;
wenzelm@33519
    31
  fun merge
wenzelm@31430
    32
   ((val1, type1, fixity1, structure1, signature1, functor1),
wenzelm@31430
    33
    (val2, type2, fixity2, structure2, signature2, functor2)) : T =
wenzelm@31328
    34
    (Symtab.merge (K true) (val1, val2),
wenzelm@31328
    35
     Symtab.merge (K true) (type1, type2),
wenzelm@31328
    36
     Symtab.merge (K true) (fixity1, fixity2),
wenzelm@31328
    37
     Symtab.merge (K true) (structure1, structure2),
wenzelm@31328
    38
     Symtab.merge (K true) (signature1, signature2),
wenzelm@31430
    39
     Symtab.merge (K true) (functor1, functor2));
wenzelm@31325
    40
);
wenzelm@31325
    41
wenzelm@31325
    42
val inherit = Env.put o Env.get;
wenzelm@31325
    43
wenzelm@31328
    44
wenzelm@31328
    45
(* results *)
wenzelm@31328
    46
wenzelm@31325
    47
val name_space: ML_Name_Space.T =
wenzelm@31325
    48
  let
wenzelm@31325
    49
    fun lookup sel1 sel2 name =
wenzelm@31325
    50
      Context.thread_data ()
wenzelm@31430
    51
      |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (Env.get context)) name)
wenzelm@31325
    52
      |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
wenzelm@31325
    53
wenzelm@31325
    54
    fun all sel1 sel2 () =
wenzelm@31325
    55
      Context.thread_data ()
wenzelm@31430
    56
      |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (Env.get context)))
wenzelm@31325
    57
      |> append (sel2 ML_Name_Space.global ())
wenzelm@31325
    58
      |> sort_distinct (string_ord o pairself #1);
wenzelm@31325
    59
wenzelm@31325
    60
    fun enter ap1 sel2 entry =
wenzelm@31325
    61
      if is_some (Context.thread_data ()) then
wenzelm@31430
    62
        Context.>> (Env.map (ap1 (Symtab.update entry)))
wenzelm@31325
    63
      else sel2 ML_Name_Space.global entry;
wenzelm@31325
    64
  in
wenzelm@31325
    65
   {lookupVal    = lookup #1 #lookupVal,
wenzelm@31325
    66
    lookupType   = lookup #2 #lookupType,
wenzelm@31325
    67
    lookupFix    = lookup #3 #lookupFix,
wenzelm@31325
    68
    lookupStruct = lookup #4 #lookupStruct,
wenzelm@31325
    69
    lookupSig    = lookup #5 #lookupSig,
wenzelm@31325
    70
    lookupFunct  = lookup #6 #lookupFunct,
wenzelm@31325
    71
    enterVal     = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)) #enterVal,
wenzelm@31325
    72
    enterType    = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)) #enterType,
wenzelm@31325
    73
    enterFix     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)) #enterFix,
wenzelm@31325
    74
    enterStruct  = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)) #enterStruct,
wenzelm@31325
    75
    enterSig     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)) #enterSig,
wenzelm@31325
    76
    enterFunct   = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)) #enterFunct,
wenzelm@31325
    77
    allVal       = all #1 #allVal,
wenzelm@31325
    78
    allType      = all #2 #allType,
wenzelm@31325
    79
    allFix       = all #3 #allFix,
wenzelm@31325
    80
    allStruct    = all #4 #allStruct,
wenzelm@31325
    81
    allSig       = all #5 #allSig,
wenzelm@31325
    82
    allFunct     = all #6 #allFunct}
wenzelm@31325
    83
  end;
wenzelm@31325
    84
wenzelm@31325
    85
val local_context: use_context =
wenzelm@31325
    86
 {tune_source = ML_Parse.fix_ints,
wenzelm@31325
    87
  name_space = name_space,
wenzelm@31325
    88
  str_of_pos = Position.str_of oo Position.line_file,
wenzelm@31325
    89
  print = writeln,
wenzelm@31325
    90
  error = error};
wenzelm@31325
    91
wenzelm@36163
    92
val is_functor = is_some o #lookupFunct name_space;
wenzelm@36163
    93
wenzelm@36163
    94
fun check_functor name =
wenzelm@36165
    95
  if not (is_functor "Table") (*mask dummy version of name_space*) orelse is_functor name then ()
wenzelm@36163
    96
  else error ("Unknown ML functor: " ^ quote name);
wenzelm@36163
    97
wenzelm@31325
    98
end;
wenzelm@31325
    99