src/Pure/ML/ml_name_space.ML
changeset 62934 6e3fb0aa857a
parent 62930 51ac6bc389e8
child 68815 6296915dee6e
equal deleted inserted replaced
62933:f14569a9ab93 62934:6e3fb0aa857a
     2     Author:     Makarius
     2     Author:     Makarius
     3 
     3 
     4 ML name space, with initial entries for strict Standard ML.
     4 ML name space, with initial entries for strict Standard ML.
     5 *)
     5 *)
     6 
     6 
     7 structure ML_Name_Space =
     7 signature ML_NAME_SPACE =
       
     8 sig
       
     9   type T
       
    10   val global: T
       
    11   val global_values: (string * string) list -> T
       
    12   val forget_val: string -> unit
       
    13   val forget_type: string -> unit
       
    14   val forget_structure: string -> unit
       
    15   val bootstrap_values: string list
       
    16   val hidden_structures: string list
       
    17   val bootstrap_structures: string list
       
    18   val bootstrap_signatures: string list
       
    19   val sml_val: (string * PolyML.NameSpace.Values.value) list
       
    20   val sml_type: (string * PolyML.NameSpace.TypeConstrs.typeConstr) list
       
    21   val sml_fixity: (string * PolyML.NameSpace.Infixes.fixity) list
       
    22   val sml_structure: (string * PolyML.NameSpace.Structures.structureVal) list
       
    23   val sml_signature: (string * PolyML.NameSpace.Signatures.signatureVal) list
       
    24   val sml_functor: (string * PolyML.NameSpace.Functors.functorVal) list
       
    25 end;
       
    26 
       
    27 structure ML_Name_Space: ML_NAME_SPACE =
     8 struct
    28 struct
     9   open PolyML.NameSpace;
       
    10 
    29 
    11   type T = PolyML.NameSpace.nameSpace;
    30 type T = PolyML.NameSpace.nameSpace;
    12 
       
    13   val global = PolyML.globalNameSpace;
       
    14   fun global_values values : T =
       
    15    {lookupVal = #lookupVal global,
       
    16     lookupType = #lookupType global,
       
    17     lookupStruct = #lookupStruct global,
       
    18     lookupFix = #lookupFix global,
       
    19     lookupSig = #lookupSig global,
       
    20     lookupFunct = #lookupFunct global,
       
    21     enterVal =
       
    22       fn (x, value) =>
       
    23         (case List.find (fn (y, _) => x = y) values of
       
    24           SOME (_, x') => #enterVal global (x', value)
       
    25         | NONE => ()),
       
    26     enterType = fn _ => (),
       
    27     enterFix = fn _ => (),
       
    28     enterStruct = fn _ => (),
       
    29     enterSig = fn _ => (),
       
    30     enterFunct = fn _ => (),
       
    31     allVal = #allVal global,
       
    32     allType = #allType global,
       
    33     allFix = #allFix global,
       
    34     allStruct = #allStruct global,
       
    35     allSig = #allSig global,
       
    36     allFunct = #allFunct global};
       
    37 
       
    38   type valueVal = Values.value;
       
    39   fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
       
    40   fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
       
    41   val forget_val = PolyML.Compiler.forgetValue;
       
    42 
       
    43   type typeVal = TypeConstrs.typeConstr;
       
    44   fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
       
    45   val forget_type = PolyML.Compiler.forgetType;
       
    46 
       
    47   type fixityVal = Infixes.fixity;
       
    48   fun displayFix (_: string, x) = Infixes.print x;
       
    49 
       
    50   type structureVal = Structures.structureVal;
       
    51   fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
       
    52   val forget_structure = PolyML.Compiler.forgetStructure;
       
    53 
       
    54   type signatureVal = Signatures.signatureVal;
       
    55   fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
       
    56 
       
    57   type functorVal = Functors.functorVal;
       
    58   fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
       
    59 
    31 
    60 
    32 
    61   (* bootstrap environment *)
    33 (* global *)
    62 
    34 
    63   val bootstrap_values =
    35 val global = PolyML.globalNameSpace;
    64     ["use", "exit", "ML_file", "ML_system_pretty", "ML_system_pp", "ML_system_overload",
    36 fun global_values values : T =
    65       "chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph"];
    37  {lookupVal = #lookupVal global,
    66   val hidden_structures = ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
    38   lookupType = #lookupType global,
    67   val bootstrap_structures =
    39   lookupStruct = #lookupStruct global,
    68     ["Exn", "Output_Primitives", "Basic_Exn", "Thread_Data", "Thread_Position", "ML_Recursive",
    40   lookupFix = #lookupFix global,
    69       "Private_Output", "PolyML"] @ hidden_structures;
    41   lookupSig = #lookupSig global,
    70   val bootstrap_signatures =
    42   lookupFunct = #lookupFunct global,
    71     ["EXN", "OUTPUT_PRIMITIVES", "BASIC_EXN", "THREAD_DATA", "THREAD_POSITION", "ML_RECURSIVE",
    43   enterVal =
    72       "PRIVATE_OUTPUT"];
    44     fn (x, value) =>
       
    45       (case List.find (fn (y, _) => x = y) values of
       
    46         SOME (_, x') => #enterVal global (x', value)
       
    47       | NONE => ()),
       
    48   enterType = fn _ => (),
       
    49   enterFix = fn _ => (),
       
    50   enterStruct = fn _ => (),
       
    51   enterSig = fn _ => (),
       
    52   enterFunct = fn _ => (),
       
    53   allVal = #allVal global,
       
    54   allType = #allType global,
       
    55   allFix = #allFix global,
       
    56   allStruct = #allStruct global,
       
    57   allSig = #allSig global,
       
    58   allFunct = #allFunct global};
    73 
    59 
    74 
    60 
    75   (* Standard ML environment *)
    61 (* forget entries *)
    76 
    62 
    77   val sml_val =
    63 val forget_val = PolyML.Compiler.forgetValue;
    78     List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_values) (#allVal global ());
    64 val forget_type = PolyML.Compiler.forgetType;
    79   val sml_type = #allType global ();
    65 val forget_structure = PolyML.Compiler.forgetStructure;
    80   val sml_fixity = #allFix global ();
    66 
    81   val sml_structure =
    67 
    82     List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_structures) (#allStruct global ());
    68 (* bootstrap environment *)
    83   val sml_signature =
    69 
    84     List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_signatures) (#allSig global ());
    70 val bootstrap_values =
    85   val sml_functor = #allFunct global ();
    71   ["use", "exit", "ML_file", "ML_system_pretty", "ML_system_pp", "ML_system_overload",
       
    72     "chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph"];
       
    73 val hidden_structures = ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
       
    74 val bootstrap_structures =
       
    75   ["Exn", "Output_Primitives", "Basic_Exn", "Thread_Data", "Thread_Position", "ML_Recursive",
       
    76     "Private_Output", "PolyML"] @ hidden_structures;
       
    77 val bootstrap_signatures =
       
    78   ["EXN", "OUTPUT_PRIMITIVES", "BASIC_EXN", "THREAD_DATA", "THREAD_POSITION", "ML_RECURSIVE",
       
    79     "PRIVATE_OUTPUT", "ML_NAME_SPACE"];
       
    80 
       
    81 
       
    82 (* Standard ML environment *)
       
    83 
       
    84 val sml_val =
       
    85   List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_values) (#allVal global ());
       
    86 val sml_type = #allType global ();
       
    87 val sml_fixity = #allFix global ();
       
    88 val sml_structure =
       
    89   List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_structures) (#allStruct global ());
       
    90 val sml_signature =
       
    91   List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_signatures) (#allSig global ());
       
    92 val sml_functor = #allFunct global ();
       
    93 
    86 end;
    94 end;