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