added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
authorwenzelm
Sat Apr 19 17:23:05 2014 +0200 (2014-04-19)
changeset 56618874bdedb2313
parent 56617 c00646996701
child 56619 e9726f630a83
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
NEWS
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Pure/Isar/isar_syn.ML
src/Pure/ML/ml_compiler.ML
src/Pure/ML/ml_compiler_polyml.ML
src/Pure/ML/ml_env.ML
src/Pure/Pure.thy
src/Pure/pure_syn.ML
src/Tools/Code/code_runtime.ML
src/Tools/SML/Examples.thy
     1.1 --- a/NEWS	Thu Apr 17 14:52:23 2014 +0200
     1.2 +++ b/NEWS	Sat Apr 19 17:23:05 2014 +0200
     1.3 @@ -37,11 +37,14 @@
     1.4  exception.  Potential INCOMPATIBILITY for non-conformant tactical
     1.5  proof tools.
     1.6  
     1.7 -* Command 'SML_file' reads and evaluates the given Standard ML file.
     1.8 +* Support for official Standard ML within the Isabelle context.
     1.9 +Command 'SML_file' reads and evaluates the given Standard ML file.
    1.10  Toplevel bindings are stored within the theory context; the initial
    1.11  environment is restricted to the Standard ML implementation of
    1.12 -Poly/ML, without the add-ons of Isabelle/ML.  See also
    1.13 -~~/src/Tools/SML/Examples.thy for some basic examples.
    1.14 +Poly/ML, without the add-ons of Isabelle/ML.  Commands 'SML_import'
    1.15 +and 'SML_export' allow to exchange toplevel bindings between the two
    1.16 +separate environments.  See also ~~/src/Tools/SML/Examples.thy for
    1.17 +some examples.
    1.18  
    1.19  
    1.20  *** Prover IDE -- Isabelle/Scala/jEdit ***
     2.1 --- a/etc/isar-keywords-ZF.el	Thu Apr 17 14:52:23 2014 +0200
     2.2 +++ b/etc/isar-keywords-ZF.el	Sat Apr 19 17:23:05 2014 +0200
     2.3 @@ -20,7 +20,9 @@
     2.4      "ProofGeneral\\.process_pgip"
     2.5      "ProofGeneral\\.restart"
     2.6      "ProofGeneral\\.undo"
     2.7 +    "SML_export"
     2.8      "SML_file"
     2.9 +    "SML_import"
    2.10      "abbreviation"
    2.11      "also"
    2.12      "apply"
    2.13 @@ -345,7 +347,9 @@
    2.14  (defconst isar-keywords-theory-decl
    2.15    '("ML"
    2.16      "ML_file"
    2.17 +    "SML_export"
    2.18      "SML_file"
    2.19 +    "SML_import"
    2.20      "abbreviation"
    2.21      "attribute_setup"
    2.22      "axiomatization"
     3.1 --- a/etc/isar-keywords.el	Thu Apr 17 14:52:23 2014 +0200
     3.2 +++ b/etc/isar-keywords.el	Sat Apr 19 17:23:05 2014 +0200
     3.3 @@ -20,7 +20,9 @@
     3.4      "ProofGeneral\\.process_pgip"
     3.5      "ProofGeneral\\.restart"
     3.6      "ProofGeneral\\.undo"
     3.7 +    "SML_export"
     3.8      "SML_file"
     3.9 +    "SML_import"
    3.10      "abbreviation"
    3.11      "adhoc_overloading"
    3.12      "also"
    3.13 @@ -483,7 +485,9 @@
    3.14  (defconst isar-keywords-theory-decl
    3.15    '("ML"
    3.16      "ML_file"
    3.17 +    "SML_export"
    3.18      "SML_file"
    3.19 +    "SML_import"
    3.20      "abbreviation"
    3.21      "adhoc_overloading"
    3.22      "atom_decl"
     4.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Apr 17 14:52:23 2014 +0200
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Apr 19 17:23:05 2014 +0200
     4.3 @@ -273,13 +273,30 @@
     4.4          let
     4.5            val ([{lines, pos, ...}], thy') = files thy;
     4.6            val source = {delimited = true, text = cat_lines lines, pos = pos};
     4.7 -          val flags = {SML = true, redirect = true, verbose = true};
     4.8 +          val flags = {SML = true, exchange = false, redirect = true, verbose = true};
     4.9          in
    4.10            thy' |> Context.theory_map
    4.11              (ML_Context.exec (fn () => ML_Context.eval_source flags source))
    4.12          end)));
    4.13  
    4.14  val _ =
    4.15 +  Outer_Syntax.command @{command_spec "SML_export"} "evaluate SML within Isabelle/ML environment"
    4.16 +    (Parse.ML_source >> (fn source =>
    4.17 +      let val flags = {SML = true, exchange = true, redirect = false, verbose = true} in
    4.18 +        Toplevel.theory
    4.19 +          (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
    4.20 +      end));
    4.21 +
    4.22 +val _ =
    4.23 +  Outer_Syntax.command @{command_spec "SML_import"} "evaluate Isabelle/ML within SML environment"
    4.24 +    (Parse.ML_source >> (fn source =>
    4.25 +      let val flags = {SML = false, exchange = true, redirect = false, verbose = true} in
    4.26 +        Toplevel.generic_theory
    4.27 +          (ML_Context.exec (fn () => ML_Context.eval_source flags source) #>
    4.28 +            Local_Theory.propagate_ml_env)
    4.29 +      end));
    4.30 +
    4.31 +val _ =
    4.32    Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory"
    4.33      (Parse.ML_source >> (fn source =>
    4.34        Toplevel.generic_theory
     5.1 --- a/src/Pure/ML/ml_compiler.ML	Thu Apr 17 14:52:23 2014 +0200
     5.2 +++ b/src/Pure/ML/ml_compiler.ML	Sat Apr 19 17:23:05 2014 +0200
     5.3 @@ -6,7 +6,7 @@
     5.4  
     5.5  signature ML_COMPILER =
     5.6  sig
     5.7 -  type flags = {SML: bool, redirect: bool, verbose: bool}
     5.8 +  type flags = {SML: bool, exchange: bool, redirect: bool, verbose: bool}
     5.9    val flags: flags
    5.10    val verbose: bool -> flags -> flags
    5.11    val eval: flags -> Position.T -> ML_Lex.token list -> unit
    5.12 @@ -15,9 +15,11 @@
    5.13  structure ML_Compiler: ML_COMPILER =
    5.14  struct
    5.15  
    5.16 -type flags = {SML: bool, redirect: bool, verbose: bool};
    5.17 -val flags = {SML = false, redirect = false, verbose = false};
    5.18 -fun verbose v (flags: flags) = {SML = #SML flags, redirect = #redirect flags, verbose = v};
    5.19 +type flags = {SML: bool, exchange: bool, redirect: bool, verbose: bool};
    5.20 +val flags = {SML = false, exchange = false, redirect = false, verbose = false};
    5.21 +
    5.22 +fun verbose b (flags: flags) =
    5.23 +  {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags, verbose = b};
    5.24  
    5.25  fun eval (flags: flags) pos toks =
    5.26    let
     6.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Thu Apr 17 14:52:23 2014 +0200
     6.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Sat Apr 19 17:23:05 2014 +0200
     6.3 @@ -70,7 +70,7 @@
     6.4  fun eval (flags: flags) pos toks =
     6.5    let
     6.6      val _ = Secure.secure_mltext ();
     6.7 -    val space = if #SML flags then ML_Env.SML_name_space else ML_Env.name_space;
     6.8 +    val space = ML_Env.name_space {SML = #SML flags, exchange = #exchange flags}
     6.9      val opt_context = Context.thread_data ();
    6.10  
    6.11  
     7.1 --- a/src/Pure/ML/ml_env.ML	Thu Apr 17 14:52:23 2014 +0200
     7.2 +++ b/src/Pure/ML/ml_env.ML	Sat Apr 19 17:23:05 2014 +0200
     7.3 @@ -8,9 +8,9 @@
     7.4  signature ML_ENV =
     7.5  sig
     7.6    val inherit: Context.generic -> Context.generic -> Context.generic
     7.7 -  val SML_name_space: ML_Name_Space.T
     7.8 -  val name_space: ML_Name_Space.T
     7.9 +  val name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
    7.10    val local_context: use_context
    7.11 +  val local_name_space: ML_Name_Space.T
    7.12    val check_functor: string -> unit
    7.13  end
    7.14  
    7.15 @@ -64,62 +64,35 @@
    7.16  val inherit = Env.put o Env.get;
    7.17  
    7.18  
    7.19 -(* SML name space *)
    7.20 -
    7.21 -val SML_name_space: ML_Name_Space.T =
    7.22 -  let
    7.23 -    fun lookup which name =
    7.24 -      Context.the_thread_data ()
    7.25 -      |> (fn context => Symtab.lookup (which (#sml_tables (Env.get context))) name);
    7.26 -
    7.27 -    fun all which () =
    7.28 -      Context.the_thread_data ()
    7.29 -      |> (fn context => Symtab.dest (which (#sml_tables (Env.get context))))
    7.30 -      |> sort_distinct (string_ord o pairself #1);
    7.31 +(* name space *)
    7.32  
    7.33 -    fun enter which entry =
    7.34 -      Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
    7.35 -        let val sml_tables' = which (Symtab.update entry) sml_tables
    7.36 -        in make_data (bootstrap, tables, sml_tables') end));
    7.37 -  in
    7.38 -   {lookupVal    = lookup #1,
    7.39 -    lookupType   = lookup #2,
    7.40 -    lookupFix    = lookup #3,
    7.41 -    lookupStruct = lookup #4,
    7.42 -    lookupSig    = lookup #5,
    7.43 -    lookupFunct  = lookup #6,
    7.44 -    enterVal     = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)),
    7.45 -    enterType    = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)),
    7.46 -    enterFix     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)),
    7.47 -    enterStruct  = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)),
    7.48 -    enterSig     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)),
    7.49 -    enterFunct   = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)),
    7.50 -    allVal       = all #1,
    7.51 -    allType      = all #2,
    7.52 -    allFix       = all #3,
    7.53 -    allStruct    = all #4,
    7.54 -    allSig       = all #5,
    7.55 -    allFunct     = all #6}
    7.56 -  end;
    7.57 -
    7.58 -
    7.59 -(* Isabelle/ML name space *)
    7.60 -
    7.61 -val name_space: ML_Name_Space.T =
    7.62 +fun name_space {SML, exchange} : ML_Name_Space.T =
    7.63    let
    7.64      fun lookup sel1 sel2 name =
    7.65 -      Context.thread_data ()
    7.66 -      |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
    7.67 -      |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
    7.68 +      if SML then
    7.69 +        Context.the_thread_data ()
    7.70 +        |> (fn context => Symtab.lookup (sel1 (#sml_tables (Env.get context))) name)
    7.71 +      else
    7.72 +        Context.thread_data ()
    7.73 +        |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
    7.74 +        |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
    7.75  
    7.76      fun all sel1 sel2 () =
    7.77 -      Context.thread_data ()
    7.78 -      |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
    7.79 -      |> append (sel2 ML_Name_Space.global ())
    7.80 +      (if SML then
    7.81 +        Context.the_thread_data ()
    7.82 +        |> (fn context => Symtab.dest (sel1 (#sml_tables (Env.get context))))
    7.83 +      else
    7.84 +        Context.thread_data ()
    7.85 +        |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
    7.86 +        |> append (sel2 ML_Name_Space.global ()))
    7.87        |> sort_distinct (string_ord o pairself #1);
    7.88  
    7.89      fun enter ap1 sel2 entry =
    7.90 -      if is_some (Context.thread_data ()) then
    7.91 +      if SML <> exchange then
    7.92 +        Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
    7.93 +          let val sml_tables' = ap1 (Symtab.update entry) sml_tables
    7.94 +          in make_data (bootstrap, tables, sml_tables') end))
    7.95 +      else if is_some (Context.thread_data ()) then
    7.96          Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
    7.97            let
    7.98              val _ = if bootstrap then sel2 ML_Name_Space.global entry else ();
    7.99 @@ -149,12 +122,14 @@
   7.100  
   7.101  val local_context: use_context =
   7.102   {tune_source = ML_Parse.fix_ints,
   7.103 -  name_space = name_space,
   7.104 +  name_space = name_space {SML = false, exchange = false},
   7.105    str_of_pos = Position.here oo Position.line_file,
   7.106    print = writeln,
   7.107    error = error};
   7.108  
   7.109 -val is_functor = is_some o #lookupFunct name_space;
   7.110 +val local_name_space = #name_space local_context;
   7.111 +
   7.112 +val is_functor = is_some o #lookupFunct local_name_space;
   7.113  
   7.114  fun check_functor name =
   7.115    if not (is_functor "Table") (*mask dummy version of name_space*) orelse is_functor name then ()
     8.1 --- a/src/Pure/Pure.thy	Thu Apr 17 14:52:23 2014 +0200
     8.2 +++ b/src/Pure/Pure.thy	Sat Apr 19 17:23:05 2014 +0200
     8.3 @@ -14,7 +14,6 @@
     8.4      "infixr" "is" "keywords" "notes" "obtains" "open" "output"
     8.5      "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
     8.6    and "theory" :: thy_begin % "theory"
     8.7 -  and "SML_file" "ML_file" :: thy_load % "ML"
     8.8    and "header" :: diag
     8.9    and "chapter" :: thy_heading1
    8.10    and "section" :: thy_heading2
    8.11 @@ -30,6 +29,8 @@
    8.12      "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
    8.13      "no_notation" "axiomatization" "theorems" "lemmas" "declare"
    8.14      "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
    8.15 +  and "SML_file" "ML_file" :: thy_load % "ML"
    8.16 +  and "SML_import" "SML_export" :: thy_decl % "ML"
    8.17    and "ML" :: thy_decl % "ML"
    8.18    and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
    8.19    and "ML_val" "ML_command" :: diag % "ML"
     9.1 --- a/src/Pure/pure_syn.ML	Thu Apr 17 14:52:23 2014 +0200
     9.2 +++ b/src/Pure/pure_syn.ML	Sat Apr 19 17:23:05 2014 +0200
     9.3 @@ -23,7 +23,7 @@
     9.4            val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
     9.5            val provide = Resources.provide (src_path, digest);
     9.6            val source = {delimited = true, text = cat_lines lines, pos = pos};
     9.7 -          val flags = {SML = false, redirect = true, verbose = true};
     9.8 +          val flags = {SML = false, exchange = false, redirect = true, verbose = true};
     9.9          in
    9.10            gthy
    9.11            |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
    10.1 --- a/src/Tools/Code/code_runtime.ML	Thu Apr 17 14:52:23 2014 +0200
    10.2 +++ b/src/Tools/Code/code_runtime.ML	Sat Apr 19 17:23:05 2014 +0200
    10.3 @@ -392,7 +392,7 @@
    10.4  
    10.5  fun notify_val (string, value) = 
    10.6    let
    10.7 -    val _ = #enterVal ML_Env.name_space (string, value);
    10.8 +    val _ = #enterVal ML_Env.local_name_space (string, value);
    10.9      val _ = Theory.setup (Loaded_Values.map (insert (op =) string));
   10.10    in () end;
   10.11  
   10.12 @@ -401,24 +401,24 @@
   10.13  val notifying_context : use_context =
   10.14   {tune_source = #tune_source ML_Env.local_context,
   10.15    name_space =
   10.16 -   {lookupVal    = #lookupVal ML_Env.name_space,
   10.17 -    lookupType   = #lookupType ML_Env.name_space,
   10.18 -    lookupFix    = #lookupFix ML_Env.name_space,
   10.19 -    lookupStruct = #lookupStruct ML_Env.name_space,
   10.20 -    lookupSig    = #lookupSig ML_Env.name_space,
   10.21 -    lookupFunct  = #lookupFunct ML_Env.name_space,
   10.22 +   {lookupVal    = #lookupVal ML_Env.local_name_space,
   10.23 +    lookupType   = #lookupType ML_Env.local_name_space,
   10.24 +    lookupFix    = #lookupFix ML_Env.local_name_space,
   10.25 +    lookupStruct = #lookupStruct ML_Env.local_name_space,
   10.26 +    lookupSig    = #lookupSig ML_Env.local_name_space,
   10.27 +    lookupFunct  = #lookupFunct ML_Env.local_name_space,
   10.28      enterVal     = notify_val,
   10.29      enterType    = abort,
   10.30      enterFix     = abort,
   10.31      enterStruct  = abort,
   10.32      enterSig     = abort,
   10.33      enterFunct   = abort,
   10.34 -    allVal       = #allVal ML_Env.name_space,
   10.35 -    allType      = #allType ML_Env.name_space,
   10.36 -    allFix       = #allFix ML_Env.name_space,
   10.37 -    allStruct    = #allStruct ML_Env.name_space,
   10.38 -    allSig       = #allSig ML_Env.name_space,
   10.39 -    allFunct     = #allFunct ML_Env.name_space},
   10.40 +    allVal       = #allVal ML_Env.local_name_space,
   10.41 +    allType      = #allType ML_Env.local_name_space,
   10.42 +    allFix       = #allFix ML_Env.local_name_space,
   10.43 +    allStruct    = #allStruct ML_Env.local_name_space,
   10.44 +    allSig       = #allSig ML_Env.local_name_space,
   10.45 +    allFunct     = #allFunct ML_Env.local_name_space},
   10.46    str_of_pos = #str_of_pos ML_Env.local_context,
   10.47    print = #print ML_Env.local_context,
   10.48    error = #error ML_Env.local_context};
    11.1 --- a/src/Tools/SML/Examples.thy	Thu Apr 17 14:52:23 2014 +0200
    11.2 +++ b/src/Tools/SML/Examples.thy	Sat Apr 19 17:23:05 2014 +0200
    11.3 @@ -23,7 +23,6 @@
    11.4  
    11.5  SML_file "factorial.sml"
    11.6  
    11.7 -
    11.8  text {*
    11.9    The subsequent example illustrates the use of multiple 'SML_file'
   11.10    commands to build larger Standard ML projects.  The toplevel SML
   11.11 @@ -34,4 +33,20 @@
   11.12  SML_file "Example.sig"
   11.13  SML_file "Example.sml"
   11.14  
   11.15 +
   11.16 +text {*
   11.17 +  Isabelle/ML and SML share a common run-time system, but the static
   11.18 +  environments are separate.  It is possible to exchange toplevel bindings
   11.19 +  via separate commands like this.
   11.20 +*}
   11.21 +
   11.22 +SML_export {* val f = factorial *}  -- {* re-use factorial from SML environment *}
   11.23 +ML {* f 42 *}
   11.24 +
   11.25 +SML_import {* val println = Output.writeln *}
   11.26 +  -- {* re-use Isabelle/ML channel for SML *}
   11.27 +
   11.28 +SML_import {* val par_map = Par_List.map *}
   11.29 +  -- {* re-use Isabelle/ML parallel list combinator for SML *}
   11.30 +
   11.31  end