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