Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: ml_env.ML Sprache: SML

Original von: Isabelle^©

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

Toplevel environment for Standard ML and Isabelle/ML within the
implicit context.
*)

signature ML_ENV =
sig
  val Isabelle: string
  val SML: string
  val ML_environment: string Config.T
  val ML_read_global: bool Config.T
  val ML_write_global: bool Config.T
  val inherit: Context.generic list -> Context.generic -> Context.generic
  type operations =
   {read_source: Input.source -> ML_Lex.token Antiquote.antiquote list,
    explode_token: ML_Lex.token -> char list,
    ML_system: bool}
  type environment = {read: string, write: string}
  val parse_environment: Context.generic option -> string -> environment
  val print_environment: environment -> string
  val SML_export: string
  val SML_import: string
  val setup: string -> operations -> theory -> theory
  val Isabelle_operations: operations
  val SML_operations: operations
  val operations: Context.generic option -> string -> operations
  val forget_structure: string -> Context.generic -> Context.generic
  val bootstrap_name_space: Context.generic -> Context.generic
  val add_name_space: string -> ML_Name_Space.T -> Context.generic -> Context.generic
  val make_name_space: string -> ML_Name_Space.T
  val context: ML_Compiler0.context
  val name_space: ML_Name_Space.T
  val check_functor: string -> unit
  val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option
  val add_breakpoints: (serial * (bool Unsynchronized.ref * Thread_Position.T)) list -> unit
end

structure ML_Env: ML_ENV =
struct

(* named environments *)

val Isabelle = "Isabelle";
val SML = "SML";

val ML_environment = Config.declare_string ("ML_environment", \<^here>) (K Isabelle);

(* global read/write *)

val ML_read_global = Config.declare_bool ("ML_read_global", \<^here>) (K true);
val ML_write_global = Config.declare_bool ("ML_write_global", \<^here>) (K true);

val read_global = Config.apply_generic ML_read_global;
val write_global = Config.apply_generic ML_write_global;

(* name space tables *)

type tables =
  PolyML.NameSpace.Values.value Symtab.table *
  PolyML.NameSpace.TypeConstrs.typeConstr Symtab.table *
  PolyML.NameSpace.Infixes.fixity Symtab.table *
  PolyML.NameSpace.Structures.structureVal Symtab.table *
  PolyML.NameSpace.Signatures.signatureVal Symtab.table *
  PolyML.NameSpace.Functors.functorVal Symtab.table;

val empty_tables: tables =
  (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty);

fun merge_tables
  ((val1, type1, fixity1, structure1, signature1, functor1),
   (val2, type2, fixity2, structure2, signature2, functor2)) : tables =
  (Symtab.merge (K true) (val1, val2),
   Symtab.merge (K true) (type1, type2),
   Symtab.merge (K true) (fixity1, fixity2),
   Symtab.merge (K true) (structure1, structure2),
   Symtab.merge (K true) (signature1, signature2),
   Symtab.merge (K true) (functor1, functor2));

fun update_tables_values vals (val1, type1, fixity1, structure1, signature1, functor1) : tables =
  (fold Symtab.update vals val1, type1, fixity1, structure1, signature1, functor1);

val sml_tables: tables =
  (Symtab.make ML_Name_Space.sml_val,
   Symtab.make ML_Name_Space.sml_type,
   Symtab.make ML_Name_Space.sml_fixity,
   Symtab.make ML_Name_Space.sml_structure,
   Symtab.make ML_Name_Space.sml_signature,
   Symtab.make ML_Name_Space.sml_functor);

(* context data *)

type operations =
{read_source: Input.source -> ML_Lex.token Antiquote.antiquote list,
  explode_token: ML_Lex.token -> char list,
  ML_system: bool};

local

type env = tables * operations;
type data = env Name_Space.table * (bool Unsynchronized.ref * Position.T) Inttab.table;

val empty_data: data = (Name_Space.empty_table "ML_environment", Inttab.empty);

fun merge_data ((envs1, breakpoints1), (envs2, breakpoints2)) : data =
  ((envs1, envs2) |> Name_Space.join_tables
    (K (fn ((tables1, ops), (tables2, _)) => (merge_tables (tables1, tables2), ops))),
   Inttab.merge (K true) (breakpoints1, breakpoints2));

in

structure Data = Generic_Data
(
  type T = data;
  val empty = empty_data;
  val extend = I;
  val merge = merge_data;
);

fun inherit contexts = Data.put (Library.foldl1 merge_data (map Data.get contexts));

end;

val get_env = Name_Space.get o #1 o Data.get;
val get_tables = #1 oo get_env;

fun update_tables env_name f context = context |> (Data.map o apfst) (fn envs =>
  let val _ = Name_Space.get envs env_name;
  in Name_Space.map_table_entry env_name (apfst f) envs end);

fun forget_structure name context =
  (if write_global context then ML_Name_Space.forget_structure name else ();
    context |> update_tables Isabelle (fn tables =>
      (#1 tables, #2 tables, #3 tables, Symtab.delete_safe name (#4 tables), #5 tables, #6 tables)));

(* environment name *)

type environment = {read: string, write: string};

val separator = ">";

fun parse_environment opt_context environment =
  let
    fun check name =
      (case opt_context of
        NONE =>
          if name = Isabelle then name
          else error ("Bad ML environment name " ^ quote name ^ " -- no context")
      | SOME context => if name = Isabelle then name else (get_env context name; name));

    val spec =
      if environment = "" then
        (case opt_context of
          NONE => Isabelle
        | SOME context => Config.get_generic context ML_environment)
      else environment;
    val (read, write) =
      (case space_explode separator spec of
        [a] => (a, a)
      | [a, b] => (a, b)
      | _ => error ("Malformed ML environment specification: " ^ quote spec));
  in {read = check read, write = check write} end;

fun print_environment {read, write} = read ^ separator ^ write;

val SML_export = print_environment {read = SML, write = Isabelle};
val SML_import = print_environment {read = Isabelle, write = SML};

(* setup operations *)

val ML_system_values =
  #allVal (ML_Name_Space.global) ()
  |> filter (member (op =) ["ML_system_pretty", "ML_system_pp", "ML_system_overload"] o #1);

fun setup env_name ops thy =
  thy |> (Context.theory_map o Data.map o apfst) (fn envs =>
    let
      val thy' = Sign.map_naming (K Name_Space.global_naming) thy;
      val tables =
        (if env_name = Isabelle then empty_tables else sml_tables)
        |> #ML_system ops ? update_tables_values ML_system_values;
      val (_, envs') =
        Name_Space.define (Context.Theory thy') true (Binding.name env_name, (tables, ops)) envs;
    in envs' end);

val Isabelle_operations: operations =
{read_source = ML_Lex.read_source,
  explode_token = ML_Lex.check_content_of #> Symbol.explode #> maps (Symbol.esc #> String.explode),
  ML_system = false};

val SML_operations: operations =
{read_source = ML_Lex.read_source_sml,
  explode_token = ML_Lex.check_content_of #> String.explode,
  ML_system = false};

val _ = Theory.setup (setup Isabelle Isabelle_operations #> setup SML SML_operations);

fun operations opt_context environment =
  let val env = #read (parse_environment opt_context environment) in
    (case opt_context of
      NONE => Isabelle_operations
    | SOME context => #2 (get_env context env))
  end;

(* name space *)

val bootstrap_name_space =
  update_tables Isabelle (fn (tables: tables) =>
    let
      fun update entries (x, y) = member (op =) entries x ? Symtab.update (x, y);
      val bootstrap_val = update ML_Name_Space.bootstrap_values;
      val bootstrap_structure = update ML_Name_Space.bootstrap_structures;
      val bootstrap_signature = update ML_Name_Space.bootstrap_signatures;

      val (val1, type1, fixity1, structure1, signature1, functor1) = sml_tables;
      val val2 = val1
        |> fold bootstrap_val (#allVal ML_Name_Space.global ())
        |> Symtab.fold bootstrap_val (#1 tables);
      val structure2 = structure1
        |> fold bootstrap_structure (#allStruct ML_Name_Space.global ())
        |> Symtab.fold bootstrap_structure (#4 tables);
      val signature2 = signature1
        |> fold bootstrap_signature (#allSig ML_Name_Space.global ())
        |> Symtab.fold bootstrap_signature (#5 tables);
    in (val2, type1, fixity1, structure2, signature2, functor1) end);

fun add_name_space env (space: ML_Name_Space.T) =
  update_tables env (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
    let
      val val2 = fold Symtab.update (#allVal space ()) val1;
      val type2 = fold Symtab.update (#allType space ()) type1;
      val fixity2 = fold Symtab.update (#allFix space ()) fixity1;
      val structure2 = fold Symtab.update (#allStruct space ()) structure1;
      val signature2 = fold Symtab.update (#allSig space ()) signature1;
      val functor2 = fold Symtab.update (#allFunct space ()) functor1;
    in (val2, type2, fixity2, structure2, signature2, functor2) end);

fun make_name_space environment : ML_Name_Space.T =
  let
    val {read, write} = parse_environment (Context.get_generic_context ()) environment;

    fun lookup_env sel1 context name = Symtab.lookup (sel1 (get_tables context read)) name;
    fun dest_env sel1 context = Symtab.dest (sel1 (get_tables context read));
    fun enter_env ap1 entry = update_tables write (ap1 (Symtab.update entry));

    fun lookup sel1 sel2 name =
      if read = Isabelle then
        (case Context.get_generic_context () of
          NONE => sel2 ML_Name_Space.global name
        | SOME context =>
            (case lookup_env sel1 context name of
              NONE => if read_global context then sel2 ML_Name_Space.global name else NONE
            | some => some))
      else lookup_env sel1 (Context.the_generic_context ()) name;

    fun all sel1 sel2 () =
      sort_distinct (string_ord o apply2 #1)
        (if read = Isabelle then
          (case Context.get_generic_context () of
            NONE => sel2 ML_Name_Space.global ()
          | SOME context =>
              dest_env sel1 context @
              (if read_global context then sel2 ML_Name_Space.global () else []))
         else dest_env sel1 (Context.the_generic_context ()));

    fun enter ap1 sel2 entry =
      if write = Isabelle then
        (case Context.get_generic_context () of
          NONE => sel2 ML_Name_Space.global entry
        | SOME context =>
            (if write_global context then sel2 ML_Name_Space.global entry else ();
             Context.>> (enter_env ap1 entry)))
      else Context.>> (enter_env ap1 entry);
  in
   {lookupVal    = lookup #1 #lookupVal,
    lookupType   = lookup #2 #lookupType,
    lookupFix    = lookup #3 #lookupFix,
    lookupStruct = lookup #4 #lookupStruct,
    lookupSig    = lookup #5 #lookupSig,
    lookupFunct  = lookup #6 #lookupFunct,
    enterVal     = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)) #enterVal,
    enterType    = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)) #enterType,
    enterFix     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)) #enterFix,
    enterStruct  = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)) #enterStruct,
    enterSig     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)) #enterSig,
    enterFunct   = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)) #enterFunct,
    allVal       = all #1 #allVal,
    allType      = all #2 #allType,
    allFix       = all #3 #allFix,
    allStruct    = all #4 #allStruct,
    allSig       = all #5 #allSig,
    allFunct     = all #6 #allFunct}
  end;

val context: ML_Compiler0.context =
{name_space = make_name_space "",
  print_depth = NONE,
  here = Position.here oo Position.line_file,
  print = writeln,
  error = error};

val name_space = #name_space context;

val is_functor = is_some o #lookupFunct name_space;

fun check_functor name =
  if not (is_functor "Table") (*mask dummy version of name_space*) orelse is_functor name then ()
  else error ("Unknown ML functor: " ^ quote name);

(* breakpoints *)

val get_breakpoint = Inttab.lookup o #2 o Data.get;

fun add_breakpoints more_breakpoints =
  if is_some (Context.get_generic_context ()) then
    Context.>>
      ((Data.map o apsnd)
        (fold (Inttab.update_new o (apsnd o apsnd) Position.make) more_breakpoints))
  else ();

end;

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.