src/Pure/ML/ml_name_space.ML
author wenzelm
Mon, 04 Apr 2016 20:28:17 +0200
changeset 62853 8e54fd480809
parent 62851 07eea2843b82
child 62860 045dc4ad6d98
permissions -rw-r--r--
tuned;

(*  Title:      Pure/ML/ml_name_space.ML
    Author:     Makarius

ML name space, with initial entries for strict Standard ML.
*)

structure ML_Name_Space =
struct
  open PolyML.NameSpace;

  type T = PolyML.NameSpace.nameSpace;

  val global = PolyML.globalNameSpace;
  fun global_values values : T =
   {lookupVal = #lookupVal global,
    lookupType = #lookupType global,
    lookupStruct = #lookupStruct global,
    lookupFix = #lookupFix global,
    lookupSig = #lookupSig global,
    lookupFunct = #lookupFunct global,
    enterVal =
      fn (x, value) =>
        (case List.find (fn (y, _) => x = y) values of
          SOME (_, x') => #enterVal global (x', value)
        | NONE => ()),
    enterType = fn _ => (),
    enterFix = fn _ => (),
    enterStruct = fn _ => (),
    enterSig = fn _ => (),
    enterFunct = fn _ => (),
    allVal = #allVal global,
    allType = #allType global,
    allFix = #allFix global,
    allStruct = #allStruct global,
    allSig = #allSig global,
    allFunct = #allFunct global};

  type valueVal = Values.value;
  fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
  fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
  val forget_val = PolyML.Compiler.forgetValue;

  type typeVal = TypeConstrs.typeConstr;
  fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
  val forget_type = PolyML.Compiler.forgetType;

  type fixityVal = Infixes.fixity;
  fun displayFix (_: string, x) = Infixes.print x;

  type structureVal = Structures.structureVal;
  fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
  val forget_structure = PolyML.Compiler.forgetStructure;

  type signatureVal = Signatures.signatureVal;
  fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);

  type functorVal = Functors.functorVal;
  fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);


  (* Standard ML name space *)

  val sml_val = List.filter (fn (a, _) => a <> "use" andalso a <> "exit") (#allVal global ());
  val sml_type = #allType global ();
  val sml_fixity = #allFix global ();
  val sml_structure =
    List.filter (fn (a, _) =>
      List.all (fn b => a <> b)
        ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"])
      (#allStruct global ());
  val sml_signature = #allSig global ();
  val sml_functor = #allFunct global ();
end;