src/Pure/ML/ml_env.ML
author wenzelm
Wed Apr 06 16:33:33 2016 +0200 (2016-04-06)
changeset 62889 99c7f31615c2
parent 62876 507c90523113
child 62902 3c0f53eae166
permissions -rw-r--r--
clarified modules;
tuned signature;
     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 forget_structure: string -> Context.generic -> Context.generic
    12   val add_breakpoint: serial * (bool Unsynchronized.ref * Position.T) ->
    13     Context.generic -> Context.generic
    14   val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option
    15   val init_bootstrap: Context.generic -> Context.generic
    16   val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic
    17   val make_name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
    18   val context: ML_Compiler0.context
    19   val name_space: ML_Name_Space.T
    20   val check_functor: string -> unit
    21 end
    22 
    23 structure ML_Env: ML_ENV =
    24 struct
    25 
    26 (* context data *)
    27 
    28 type tables =
    29   ML_Name_Space.valueVal Symtab.table *
    30   ML_Name_Space.typeVal Symtab.table *
    31   ML_Name_Space.fixityVal Symtab.table *
    32   ML_Name_Space.structureVal Symtab.table *
    33   ML_Name_Space.signatureVal Symtab.table *
    34   ML_Name_Space.functorVal Symtab.table;
    35 
    36 fun merge_tables
    37   ((val1, type1, fixity1, structure1, signature1, functor1),
    38    (val2, type2, fixity2, structure2, signature2, functor2)) : tables =
    39   (Symtab.merge (K true) (val1, val2),
    40    Symtab.merge (K true) (type1, type2),
    41    Symtab.merge (K true) (fixity1, fixity2),
    42    Symtab.merge (K true) (structure1, structure2),
    43    Symtab.merge (K true) (signature1, signature2),
    44    Symtab.merge (K true) (functor1, functor2));
    45 
    46 type data =
    47  {bootstrap: bool,
    48   tables: tables,
    49   sml_tables: tables,
    50   breakpoints: (bool Unsynchronized.ref * Position.T) Inttab.table};
    51 
    52 fun make_data (bootstrap, tables, sml_tables, breakpoints) : data =
    53   {bootstrap = bootstrap, tables = tables, sml_tables = sml_tables, breakpoints = breakpoints};
    54 
    55 structure Env = Generic_Data
    56 (
    57   type T = data
    58   val empty =
    59     make_data (true,
    60       (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty),
    61       (Symtab.make ML_Name_Space.sml_val,
    62        Symtab.make ML_Name_Space.sml_type,
    63        Symtab.make ML_Name_Space.sml_fixity,
    64        Symtab.make ML_Name_Space.sml_structure,
    65        Symtab.make ML_Name_Space.sml_signature,
    66        Symtab.make ML_Name_Space.sml_functor),
    67       Inttab.empty);
    68   fun extend (data : T) = make_data (false, #tables data, #sml_tables data, #breakpoints data);
    69   fun merge (data : T * T) =
    70     make_data (false,
    71       merge_tables (apply2 #tables data),
    72       merge_tables (apply2 #sml_tables data),
    73       Inttab.merge (K true) (apply2 #breakpoints data));
    74 );
    75 
    76 val inherit = Env.put o Env.get;
    77 
    78 fun forget_structure name =
    79   Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
    80     let
    81       val _ = if bootstrap then ML_Name_Space.forget_structure name else ();
    82       val tables' =
    83         (#1 tables, #2 tables, #3 tables, Symtab.delete_safe name (#4 tables), #5 tables, #6 tables);
    84     in make_data (bootstrap, tables', sml_tables, breakpoints) end);
    85 
    86 fun add_breakpoint breakpoint =
    87   Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
    88     let val breakpoints' = Inttab.update_new breakpoint breakpoints;
    89     in make_data (bootstrap, tables, sml_tables, breakpoints') end);
    90 
    91 val get_breakpoint = Inttab.lookup o #breakpoints o Env.get;
    92 
    93 
    94 (* name space *)
    95 
    96 val init_bootstrap =
    97   Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
    98     let
    99       val sml_tables' =
   100         sml_tables |> (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
   101             let
   102               val val2 =
   103                 fold (fn (x, y) =>
   104                   member (op =) ML_Name_Space.bootstrap_values x ? Symtab.update (x, y))
   105                 (#allVal ML_Name_Space.global ()) val1;
   106               val structure2 =
   107                 fold (fn (x, y) =>
   108                   member (op =) ML_Name_Space.bootstrap_structures x ? Symtab.update (x, y))
   109                 (#allStruct ML_Name_Space.global ()) structure1;
   110             in (val2, type1, fixity1, structure2, signature1, functor1) end);
   111     in make_data (bootstrap, tables, sml_tables', breakpoints) end);
   112 
   113 fun add_name_space {SML} (space: ML_Name_Space.T) =
   114   Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
   115     let
   116       val (tables', sml_tables') =
   117         (tables, sml_tables) |> (if SML then apsnd else apfst)
   118           (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
   119             let
   120               val val2 = fold Symtab.update (#allVal space ()) val1;
   121               val type2 = fold Symtab.update (#allType space ()) type1;
   122               val fixity2 = fold Symtab.update (#allFix space ()) fixity1;
   123               val structure2 = fold Symtab.update (#allStruct space ()) structure1;
   124               val signature2 = fold Symtab.update (#allSig space ()) signature1;
   125               val functor2 = fold Symtab.update (#allFunct space ()) functor1;
   126             in (val2, type2, fixity2, structure2, signature2, functor2) end);
   127     in make_data (bootstrap, tables', sml_tables', breakpoints) end);
   128 
   129 fun make_name_space {SML, exchange} : ML_Name_Space.T =
   130   let
   131     fun lookup sel1 sel2 name =
   132       if SML then
   133         Context.the_generic_context ()
   134         |> (fn context => Symtab.lookup (sel1 (#sml_tables (Env.get context))) name)
   135       else
   136         Context.get_generic_context ()
   137         |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
   138         |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
   139 
   140     fun all sel1 sel2 () =
   141       (if SML then
   142         Context.the_generic_context ()
   143         |> (fn context => Symtab.dest (sel1 (#sml_tables (Env.get context))))
   144       else
   145         Context.get_generic_context ()
   146         |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
   147         |> append (sel2 ML_Name_Space.global ()))
   148       |> sort_distinct (string_ord o apply2 #1);
   149 
   150     fun enter ap1 sel2 entry =
   151       if SML <> exchange then
   152         Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
   153           let val sml_tables' = ap1 (Symtab.update entry) sml_tables
   154           in make_data (bootstrap, tables, sml_tables', breakpoints) end))
   155       else if is_some (Context.get_generic_context ()) then
   156         Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
   157           let
   158             val _ = if bootstrap then sel2 ML_Name_Space.global entry else ();
   159             val tables' = ap1 (Symtab.update entry) tables;
   160           in make_data (bootstrap, tables', sml_tables, breakpoints) end))
   161       else sel2 ML_Name_Space.global entry;
   162   in
   163    {lookupVal    = lookup #1 #lookupVal,
   164     lookupType   = lookup #2 #lookupType,
   165     lookupFix    = lookup #3 #lookupFix,
   166     lookupStruct = lookup #4 #lookupStruct,
   167     lookupSig    = lookup #5 #lookupSig,
   168     lookupFunct  = lookup #6 #lookupFunct,
   169     enterVal     = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)) #enterVal,
   170     enterType    = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)) #enterType,
   171     enterFix     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)) #enterFix,
   172     enterStruct  = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)) #enterStruct,
   173     enterSig     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)) #enterSig,
   174     enterFunct   = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)) #enterFunct,
   175     allVal       = all #1 #allVal,
   176     allType      = all #2 #allType,
   177     allFix       = all #3 #allFix,
   178     allStruct    = all #4 #allStruct,
   179     allSig       = all #5 #allSig,
   180     allFunct     = all #6 #allFunct}
   181   end;
   182 
   183 val context: ML_Compiler0.context =
   184  {name_space = make_name_space {SML = false, exchange = false},
   185   print_depth = NONE,
   186   here = Position.here oo Position.line_file,
   187   print = writeln,
   188   error = error};
   189 
   190 val name_space = #name_space context;
   191 
   192 val is_functor = is_some o #lookupFunct name_space;
   193 
   194 fun check_functor name =
   195   if not (is_functor "Table") (*mask dummy version of name_space*) orelse is_functor name then ()
   196   else error ("Unknown ML functor: " ^ quote name);
   197 
   198 end;