src/Pure/ML/ml_env.ML
author wenzelm
Fri May 25 22:47:57 2018 +0200 (20 months ago)
changeset 68276 cbee43ff4ceb
parent 64556 851ae0e7b09c
child 68813 78edc4bc3bd3
permissions -rw-r--r--
added command 'ML_export';
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@59127
    11
  val forget_structure: string -> Context.generic -> Context.generic
wenzelm@60746
    12
  val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option
wenzelm@62941
    13
  val add_breakpoints: (serial * (bool Unsynchronized.ref * Thread_Position.T)) list -> unit
wenzelm@62873
    14
  val init_bootstrap: Context.generic -> Context.generic
wenzelm@62902
    15
  val SML_environment: bool Config.T
wenzelm@68276
    16
  val set_bootstrap: bool -> Context.generic -> Context.generic
wenzelm@68276
    17
  val restore_bootstrap: Context.generic -> Context.generic -> Context.generic
wenzelm@60858
    18
  val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic
wenzelm@62495
    19
  val make_name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
wenzelm@62495
    20
  val context: ML_Compiler0.context
wenzelm@62495
    21
  val name_space: ML_Name_Space.T
wenzelm@36163
    22
  val check_functor: string -> unit
wenzelm@31325
    23
end
wenzelm@31325
    24
wenzelm@31325
    25
structure ML_Env: ML_ENV =
wenzelm@31325
    26
struct
wenzelm@31325
    27
wenzelm@31328
    28
(* context data *)
wenzelm@31328
    29
wenzelm@56275
    30
type tables =
wenzelm@62934
    31
  PolyML.NameSpace.Values.value Symtab.table *
wenzelm@62934
    32
  PolyML.NameSpace.TypeConstrs.typeConstr Symtab.table *
wenzelm@62934
    33
  PolyML.NameSpace.Infixes.fixity Symtab.table *
wenzelm@62934
    34
  PolyML.NameSpace.Structures.structureVal Symtab.table *
wenzelm@62934
    35
  PolyML.NameSpace.Signatures.signatureVal Symtab.table *
wenzelm@62934
    36
  PolyML.NameSpace.Functors.functorVal Symtab.table;
wenzelm@56275
    37
wenzelm@56275
    38
fun merge_tables
wenzelm@56275
    39
  ((val1, type1, fixity1, structure1, signature1, functor1),
wenzelm@56275
    40
   (val2, type2, fixity2, structure2, signature2, functor2)) : tables =
wenzelm@56275
    41
  (Symtab.merge (K true) (val1, val2),
wenzelm@56275
    42
   Symtab.merge (K true) (type1, type2),
wenzelm@56275
    43
   Symtab.merge (K true) (fixity1, fixity2),
wenzelm@56275
    44
   Symtab.merge (K true) (structure1, structure2),
wenzelm@56275
    45
   Symtab.merge (K true) (signature1, signature2),
wenzelm@56275
    46
   Symtab.merge (K true) (functor1, functor2));
wenzelm@56275
    47
wenzelm@60746
    48
type data =
wenzelm@60746
    49
 {bootstrap: bool,
wenzelm@60746
    50
  tables: tables,
wenzelm@60746
    51
  sml_tables: tables,
wenzelm@60746
    52
  breakpoints: (bool Unsynchronized.ref * Position.T) Inttab.table};
wenzelm@56275
    53
wenzelm@60746
    54
fun make_data (bootstrap, tables, sml_tables, breakpoints) : data =
wenzelm@60746
    55
  {bootstrap = bootstrap, tables = tables, sml_tables = sml_tables, breakpoints = breakpoints};
wenzelm@56275
    56
wenzelm@33519
    57
structure Env = Generic_Data
wenzelm@31325
    58
(
wenzelm@56275
    59
  type T = data
wenzelm@56275
    60
  val empty =
wenzelm@56275
    61
    make_data (true,
wenzelm@56275
    62
      (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty),
wenzelm@62839
    63
      (Symtab.make ML_Name_Space.sml_val,
wenzelm@62839
    64
       Symtab.make ML_Name_Space.sml_type,
wenzelm@62839
    65
       Symtab.make ML_Name_Space.sml_fixity,
wenzelm@62839
    66
       Symtab.make ML_Name_Space.sml_structure,
wenzelm@62839
    67
       Symtab.make ML_Name_Space.sml_signature,
wenzelm@62839
    68
       Symtab.make ML_Name_Space.sml_functor),
wenzelm@60746
    69
      Inttab.empty);
wenzelm@60746
    70
  fun extend (data : T) = make_data (false, #tables data, #sml_tables data, #breakpoints data);
wenzelm@56275
    71
  fun merge (data : T * T) =
wenzelm@56275
    72
    make_data (false,
wenzelm@59058
    73
      merge_tables (apply2 #tables data),
wenzelm@60746
    74
      merge_tables (apply2 #sml_tables data),
wenzelm@60746
    75
      Inttab.merge (K true) (apply2 #breakpoints data));
wenzelm@31325
    76
);
wenzelm@31325
    77
wenzelm@31325
    78
val inherit = Env.put o Env.get;
wenzelm@31325
    79
wenzelm@59127
    80
fun forget_structure name =
wenzelm@60746
    81
  Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
wenzelm@59127
    82
    let
wenzelm@62657
    83
      val _ = if bootstrap then ML_Name_Space.forget_structure name else ();
wenzelm@59127
    84
      val tables' =
wenzelm@59127
    85
        (#1 tables, #2 tables, #3 tables, Symtab.delete_safe name (#4 tables), #5 tables, #6 tables);
wenzelm@60746
    86
    in make_data (bootstrap, tables', sml_tables, breakpoints) end);
wenzelm@60746
    87
wenzelm@62941
    88
val get_breakpoint = Inttab.lookup o #breakpoints o Env.get;
wenzelm@60746
    89
wenzelm@62941
    90
fun add_breakpoints more_breakpoints =
wenzelm@62941
    91
  if is_some (Context.get_generic_context ()) then
wenzelm@62941
    92
    Context.>>
wenzelm@62941
    93
      (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
wenzelm@62941
    94
        let val breakpoints' =
wenzelm@62941
    95
          fold (Inttab.update_new o (apsnd o apsnd) Position.make) more_breakpoints breakpoints;
wenzelm@62941
    96
        in make_data (bootstrap, tables, sml_tables, breakpoints') end))
wenzelm@62941
    97
  else ();
wenzelm@59127
    98
wenzelm@31328
    99
wenzelm@62902
   100
(* SML environment for Isabelle/ML *)
wenzelm@62902
   101
wenzelm@62902
   102
val SML_environment =
wenzelm@64556
   103
  Config.bool (Config.declare ("SML_environment", \<^here>) (fn _ => Config.Bool false));
wenzelm@62902
   104
wenzelm@62902
   105
fun sml_env SML =
wenzelm@62902
   106
  SML orelse
wenzelm@62902
   107
    (case Context.get_generic_context () of
wenzelm@62902
   108
      NONE => false
wenzelm@62902
   109
    | SOME context => Config.get_generic context SML_environment);
wenzelm@62902
   110
wenzelm@62902
   111
wenzelm@56618
   112
(* name space *)
wenzelm@56275
   113
wenzelm@62873
   114
val init_bootstrap =
wenzelm@62873
   115
  Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
wenzelm@62873
   116
    let
wenzelm@62873
   117
      val sml_tables' =
wenzelm@62873
   118
        sml_tables |> (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
wenzelm@62873
   119
            let
wenzelm@62873
   120
              val val2 =
wenzelm@62873
   121
                fold (fn (x, y) =>
wenzelm@62875
   122
                  member (op =) ML_Name_Space.bootstrap_values x ? Symtab.update (x, y))
wenzelm@62873
   123
                (#allVal ML_Name_Space.global ()) val1;
wenzelm@62873
   124
              val structure2 =
wenzelm@62873
   125
                fold (fn (x, y) =>
wenzelm@62875
   126
                  member (op =) ML_Name_Space.bootstrap_structures x ? Symtab.update (x, y))
wenzelm@62873
   127
                (#allStruct ML_Name_Space.global ()) structure1;
wenzelm@62910
   128
              val signature2 =
wenzelm@62910
   129
                fold (fn (x, y) =>
wenzelm@62910
   130
                  member (op =) ML_Name_Space.bootstrap_signatures x ? Symtab.update (x, y))
wenzelm@62910
   131
                (#allSig ML_Name_Space.global ()) signature1;
wenzelm@62910
   132
            in (val2, type1, fixity1, structure2, signature2, functor1) end);
wenzelm@62873
   133
    in make_data (bootstrap, tables, sml_tables', breakpoints) end);
wenzelm@62873
   134
wenzelm@68276
   135
fun set_bootstrap bootstrap =
wenzelm@68276
   136
  Env.map (fn {tables, sml_tables, breakpoints, ...} =>
wenzelm@68276
   137
    make_data (bootstrap, tables, sml_tables, breakpoints));
wenzelm@68276
   138
wenzelm@68276
   139
val restore_bootstrap = set_bootstrap o #bootstrap o Env.get;
wenzelm@68276
   140
wenzelm@60858
   141
fun add_name_space {SML} (space: ML_Name_Space.T) =
wenzelm@60858
   142
  Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
wenzelm@60858
   143
    let
wenzelm@60858
   144
      val (tables', sml_tables') =
wenzelm@62902
   145
        (tables, sml_tables) |> (if sml_env SML then apsnd else apfst)
wenzelm@60858
   146
          (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
wenzelm@60858
   147
            let
wenzelm@60858
   148
              val val2 = fold Symtab.update (#allVal space ()) val1;
wenzelm@60858
   149
              val type2 = fold Symtab.update (#allType space ()) type1;
wenzelm@60858
   150
              val fixity2 = fold Symtab.update (#allFix space ()) fixity1;
wenzelm@60858
   151
              val structure2 = fold Symtab.update (#allStruct space ()) structure1;
wenzelm@60858
   152
              val signature2 = fold Symtab.update (#allSig space ()) signature1;
wenzelm@60858
   153
              val functor2 = fold Symtab.update (#allFunct space ()) functor1;
wenzelm@60858
   154
            in (val2, type2, fixity2, structure2, signature2, functor2) end);
wenzelm@60858
   155
    in make_data (bootstrap, tables', sml_tables', breakpoints) end);
wenzelm@60858
   156
wenzelm@62495
   157
fun make_name_space {SML, exchange} : ML_Name_Space.T =
wenzelm@31325
   158
  let
wenzelm@31325
   159
    fun lookup sel1 sel2 name =
wenzelm@62902
   160
      if sml_env SML then
wenzelm@62876
   161
        Context.the_generic_context ()
wenzelm@56618
   162
        |> (fn context => Symtab.lookup (sel1 (#sml_tables (Env.get context))) name)
wenzelm@56618
   163
      else
wenzelm@62889
   164
        Context.get_generic_context ()
wenzelm@56618
   165
        |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
wenzelm@56618
   166
        |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
wenzelm@31325
   167
wenzelm@31325
   168
    fun all sel1 sel2 () =
wenzelm@62902
   169
      (if sml_env SML then
wenzelm@62876
   170
        Context.the_generic_context ()
wenzelm@56618
   171
        |> (fn context => Symtab.dest (sel1 (#sml_tables (Env.get context))))
wenzelm@56618
   172
      else
wenzelm@62889
   173
        Context.get_generic_context ()
wenzelm@56618
   174
        |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
wenzelm@56618
   175
        |> append (sel2 ML_Name_Space.global ()))
wenzelm@59058
   176
      |> sort_distinct (string_ord o apply2 #1);
wenzelm@31325
   177
wenzelm@31325
   178
    fun enter ap1 sel2 entry =
wenzelm@62902
   179
      if sml_env SML <> exchange then
wenzelm@60746
   180
        Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
wenzelm@56618
   181
          let val sml_tables' = ap1 (Symtab.update entry) sml_tables
wenzelm@60746
   182
          in make_data (bootstrap, tables, sml_tables', breakpoints) end))
wenzelm@62889
   183
      else if is_some (Context.get_generic_context ()) then
wenzelm@60746
   184
        Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
wenzelm@56203
   185
          let
wenzelm@56275
   186
            val _ = if bootstrap then sel2 ML_Name_Space.global entry else ();
wenzelm@56275
   187
            val tables' = ap1 (Symtab.update entry) tables;
wenzelm@60746
   188
          in make_data (bootstrap, tables', sml_tables, breakpoints) end))
wenzelm@31325
   189
      else sel2 ML_Name_Space.global entry;
wenzelm@31325
   190
  in
wenzelm@31325
   191
   {lookupVal    = lookup #1 #lookupVal,
wenzelm@31325
   192
    lookupType   = lookup #2 #lookupType,
wenzelm@31325
   193
    lookupFix    = lookup #3 #lookupFix,
wenzelm@31325
   194
    lookupStruct = lookup #4 #lookupStruct,
wenzelm@31325
   195
    lookupSig    = lookup #5 #lookupSig,
wenzelm@31325
   196
    lookupFunct  = lookup #6 #lookupFunct,
wenzelm@31325
   197
    enterVal     = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)) #enterVal,
wenzelm@31325
   198
    enterType    = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)) #enterType,
wenzelm@31325
   199
    enterFix     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)) #enterFix,
wenzelm@31325
   200
    enterStruct  = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)) #enterStruct,
wenzelm@31325
   201
    enterSig     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)) #enterSig,
wenzelm@31325
   202
    enterFunct   = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)) #enterFunct,
wenzelm@31325
   203
    allVal       = all #1 #allVal,
wenzelm@31325
   204
    allType      = all #2 #allType,
wenzelm@31325
   205
    allFix       = all #3 #allFix,
wenzelm@31325
   206
    allStruct    = all #4 #allStruct,
wenzelm@31325
   207
    allSig       = all #5 #allSig,
wenzelm@31325
   208
    allFunct     = all #6 #allFunct}
wenzelm@31325
   209
  end;
wenzelm@31325
   210
wenzelm@62495
   211
val context: ML_Compiler0.context =
wenzelm@62495
   212
 {name_space = make_name_space {SML = false, exchange = false},
wenzelm@62716
   213
  print_depth = NONE,
wenzelm@62493
   214
  here = Position.here oo Position.line_file,
wenzelm@31325
   215
  print = writeln,
wenzelm@31325
   216
  error = error};
wenzelm@31325
   217
wenzelm@62495
   218
val name_space = #name_space context;
wenzelm@56618
   219
wenzelm@62495
   220
val is_functor = is_some o #lookupFunct name_space;
wenzelm@36163
   221
wenzelm@36163
   222
fun check_functor name =
wenzelm@36165
   223
  if not (is_functor "Table") (*mask dummy version of name_space*) orelse is_functor name then ()
wenzelm@36163
   224
  else error ("Unknown ML functor: " ^ quote name);
wenzelm@36163
   225
wenzelm@31325
   226
end;