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