src/Pure/ML/ml_env.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 64556 851ae0e7b09c
child 68276 cbee43ff4ceb
permissions -rw-r--r--
more robust sorted_entries;
     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 get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option
    13   val add_breakpoints: (serial * (bool Unsynchronized.ref * Thread_Position.T)) list -> unit
    14   val init_bootstrap: Context.generic -> Context.generic
    15   val SML_environment: bool Config.T
    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   PolyML.NameSpace.Values.value Symtab.table *
    30   PolyML.NameSpace.TypeConstrs.typeConstr Symtab.table *
    31   PolyML.NameSpace.Infixes.fixity Symtab.table *
    32   PolyML.NameSpace.Structures.structureVal Symtab.table *
    33   PolyML.NameSpace.Signatures.signatureVal Symtab.table *
    34   PolyML.NameSpace.Functors.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 val get_breakpoint = Inttab.lookup o #breakpoints o Env.get;
    87 
    88 fun add_breakpoints more_breakpoints =
    89   if is_some (Context.get_generic_context ()) then
    90     Context.>>
    91       (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
    92         let val breakpoints' =
    93           fold (Inttab.update_new o (apsnd o apsnd) Position.make) more_breakpoints breakpoints;
    94         in make_data (bootstrap, tables, sml_tables, breakpoints') end))
    95   else ();
    96 
    97 
    98 (* SML environment for Isabelle/ML *)
    99 
   100 val SML_environment =
   101   Config.bool (Config.declare ("SML_environment", \<^here>) (fn _ => Config.Bool false));
   102 
   103 fun sml_env SML =
   104   SML orelse
   105     (case Context.get_generic_context () of
   106       NONE => false
   107     | SOME context => Config.get_generic context SML_environment);
   108 
   109 
   110 (* name space *)
   111 
   112 val init_bootstrap =
   113   Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
   114     let
   115       val sml_tables' =
   116         sml_tables |> (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
   117             let
   118               val val2 =
   119                 fold (fn (x, y) =>
   120                   member (op =) ML_Name_Space.bootstrap_values x ? Symtab.update (x, y))
   121                 (#allVal ML_Name_Space.global ()) val1;
   122               val structure2 =
   123                 fold (fn (x, y) =>
   124                   member (op =) ML_Name_Space.bootstrap_structures x ? Symtab.update (x, y))
   125                 (#allStruct ML_Name_Space.global ()) structure1;
   126               val signature2 =
   127                 fold (fn (x, y) =>
   128                   member (op =) ML_Name_Space.bootstrap_signatures x ? Symtab.update (x, y))
   129                 (#allSig ML_Name_Space.global ()) signature1;
   130             in (val2, type1, fixity1, structure2, signature2, functor1) end);
   131     in make_data (bootstrap, tables, sml_tables', breakpoints) end);
   132 
   133 fun add_name_space {SML} (space: ML_Name_Space.T) =
   134   Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
   135     let
   136       val (tables', sml_tables') =
   137         (tables, sml_tables) |> (if sml_env SML then apsnd else apfst)
   138           (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
   139             let
   140               val val2 = fold Symtab.update (#allVal space ()) val1;
   141               val type2 = fold Symtab.update (#allType space ()) type1;
   142               val fixity2 = fold Symtab.update (#allFix space ()) fixity1;
   143               val structure2 = fold Symtab.update (#allStruct space ()) structure1;
   144               val signature2 = fold Symtab.update (#allSig space ()) signature1;
   145               val functor2 = fold Symtab.update (#allFunct space ()) functor1;
   146             in (val2, type2, fixity2, structure2, signature2, functor2) end);
   147     in make_data (bootstrap, tables', sml_tables', breakpoints) end);
   148 
   149 fun make_name_space {SML, exchange} : ML_Name_Space.T =
   150   let
   151     fun lookup sel1 sel2 name =
   152       if sml_env SML then
   153         Context.the_generic_context ()
   154         |> (fn context => Symtab.lookup (sel1 (#sml_tables (Env.get context))) name)
   155       else
   156         Context.get_generic_context ()
   157         |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
   158         |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
   159 
   160     fun all sel1 sel2 () =
   161       (if sml_env SML then
   162         Context.the_generic_context ()
   163         |> (fn context => Symtab.dest (sel1 (#sml_tables (Env.get context))))
   164       else
   165         Context.get_generic_context ()
   166         |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
   167         |> append (sel2 ML_Name_Space.global ()))
   168       |> sort_distinct (string_ord o apply2 #1);
   169 
   170     fun enter ap1 sel2 entry =
   171       if sml_env SML <> exchange then
   172         Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
   173           let val sml_tables' = ap1 (Symtab.update entry) sml_tables
   174           in make_data (bootstrap, tables, sml_tables', breakpoints) end))
   175       else if is_some (Context.get_generic_context ()) then
   176         Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
   177           let
   178             val _ = if bootstrap then sel2 ML_Name_Space.global entry else ();
   179             val tables' = ap1 (Symtab.update entry) tables;
   180           in make_data (bootstrap, tables', sml_tables, breakpoints) end))
   181       else sel2 ML_Name_Space.global entry;
   182   in
   183    {lookupVal    = lookup #1 #lookupVal,
   184     lookupType   = lookup #2 #lookupType,
   185     lookupFix    = lookup #3 #lookupFix,
   186     lookupStruct = lookup #4 #lookupStruct,
   187     lookupSig    = lookup #5 #lookupSig,
   188     lookupFunct  = lookup #6 #lookupFunct,
   189     enterVal     = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)) #enterVal,
   190     enterType    = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)) #enterType,
   191     enterFix     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)) #enterFix,
   192     enterStruct  = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)) #enterStruct,
   193     enterSig     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)) #enterSig,
   194     enterFunct   = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)) #enterFunct,
   195     allVal       = all #1 #allVal,
   196     allType      = all #2 #allType,
   197     allFix       = all #3 #allFix,
   198     allStruct    = all #4 #allStruct,
   199     allSig       = all #5 #allSig,
   200     allFunct     = all #6 #allFunct}
   201   end;
   202 
   203 val context: ML_Compiler0.context =
   204  {name_space = make_name_space {SML = false, exchange = false},
   205   print_depth = NONE,
   206   here = Position.here oo Position.line_file,
   207   print = writeln,
   208   error = error};
   209 
   210 val name_space = #name_space context;
   211 
   212 val is_functor = is_some o #lookupFunct name_space;
   213 
   214 fun check_functor name =
   215   if not (is_functor "Table") (*mask dummy version of name_space*) orelse is_functor name then ()
   216   else error ("Unknown ML functor: " ^ quote name);
   217 
   218 end;