--- a/NEWS Thu Apr 17 14:52:23 2014 +0200
+++ b/NEWS Sat Apr 19 17:23:05 2014 +0200
@@ -37,11 +37,14 @@
exception. Potential INCOMPATIBILITY for non-conformant tactical
proof tools.
-* Command 'SML_file' reads and evaluates the given Standard ML file.
+* Support for official Standard ML within the Isabelle context.
+Command 'SML_file' reads and evaluates the given Standard ML file.
Toplevel bindings are stored within the theory context; the initial
environment is restricted to the Standard ML implementation of
-Poly/ML, without the add-ons of Isabelle/ML. See also
-~~/src/Tools/SML/Examples.thy for some basic examples.
+Poly/ML, without the add-ons of Isabelle/ML. Commands 'SML_import'
+and 'SML_export' allow to exchange toplevel bindings between the two
+separate environments. See also ~~/src/Tools/SML/Examples.thy for
+some examples.
*** Prover IDE -- Isabelle/Scala/jEdit ***
--- a/etc/isar-keywords-ZF.el Thu Apr 17 14:52:23 2014 +0200
+++ b/etc/isar-keywords-ZF.el Sat Apr 19 17:23:05 2014 +0200
@@ -20,7 +20,9 @@
"ProofGeneral\\.process_pgip"
"ProofGeneral\\.restart"
"ProofGeneral\\.undo"
+ "SML_export"
"SML_file"
+ "SML_import"
"abbreviation"
"also"
"apply"
@@ -345,7 +347,9 @@
(defconst isar-keywords-theory-decl
'("ML"
"ML_file"
+ "SML_export"
"SML_file"
+ "SML_import"
"abbreviation"
"attribute_setup"
"axiomatization"
--- a/etc/isar-keywords.el Thu Apr 17 14:52:23 2014 +0200
+++ b/etc/isar-keywords.el Sat Apr 19 17:23:05 2014 +0200
@@ -20,7 +20,9 @@
"ProofGeneral\\.process_pgip"
"ProofGeneral\\.restart"
"ProofGeneral\\.undo"
+ "SML_export"
"SML_file"
+ "SML_import"
"abbreviation"
"adhoc_overloading"
"also"
@@ -483,7 +485,9 @@
(defconst isar-keywords-theory-decl
'("ML"
"ML_file"
+ "SML_export"
"SML_file"
+ "SML_import"
"abbreviation"
"adhoc_overloading"
"atom_decl"
--- a/src/Pure/Isar/isar_syn.ML Thu Apr 17 14:52:23 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML Sat Apr 19 17:23:05 2014 +0200
@@ -273,13 +273,30 @@
let
val ([{lines, pos, ...}], thy') = files thy;
val source = {delimited = true, text = cat_lines lines, pos = pos};
- val flags = {SML = true, redirect = true, verbose = true};
+ val flags = {SML = true, exchange = false, redirect = true, verbose = true};
in
thy' |> Context.theory_map
(ML_Context.exec (fn () => ML_Context.eval_source flags source))
end)));
val _ =
+ Outer_Syntax.command @{command_spec "SML_export"} "evaluate SML within Isabelle/ML environment"
+ (Parse.ML_source >> (fn source =>
+ let val flags = {SML = true, exchange = true, redirect = false, verbose = true} in
+ Toplevel.theory
+ (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
+ end));
+
+val _ =
+ Outer_Syntax.command @{command_spec "SML_import"} "evaluate Isabelle/ML within SML environment"
+ (Parse.ML_source >> (fn source =>
+ let val flags = {SML = false, exchange = true, redirect = false, verbose = true} in
+ Toplevel.generic_theory
+ (ML_Context.exec (fn () => ML_Context.eval_source flags source) #>
+ Local_Theory.propagate_ml_env)
+ end));
+
+val _ =
Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory"
(Parse.ML_source >> (fn source =>
Toplevel.generic_theory
--- a/src/Pure/ML/ml_compiler.ML Thu Apr 17 14:52:23 2014 +0200
+++ b/src/Pure/ML/ml_compiler.ML Sat Apr 19 17:23:05 2014 +0200
@@ -6,7 +6,7 @@
signature ML_COMPILER =
sig
- type flags = {SML: bool, redirect: bool, verbose: bool}
+ type flags = {SML: bool, exchange: bool, redirect: bool, verbose: bool}
val flags: flags
val verbose: bool -> flags -> flags
val eval: flags -> Position.T -> ML_Lex.token list -> unit
@@ -15,9 +15,11 @@
structure ML_Compiler: ML_COMPILER =
struct
-type flags = {SML: bool, redirect: bool, verbose: bool};
-val flags = {SML = false, redirect = false, verbose = false};
-fun verbose v (flags: flags) = {SML = #SML flags, redirect = #redirect flags, verbose = v};
+type flags = {SML: bool, exchange: bool, redirect: bool, verbose: bool};
+val flags = {SML = false, exchange = false, redirect = false, verbose = false};
+
+fun verbose b (flags: flags) =
+ {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags, verbose = b};
fun eval (flags: flags) pos toks =
let
--- a/src/Pure/ML/ml_compiler_polyml.ML Thu Apr 17 14:52:23 2014 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML Sat Apr 19 17:23:05 2014 +0200
@@ -70,7 +70,7 @@
fun eval (flags: flags) pos toks =
let
val _ = Secure.secure_mltext ();
- val space = if #SML flags then ML_Env.SML_name_space else ML_Env.name_space;
+ val space = ML_Env.name_space {SML = #SML flags, exchange = #exchange flags}
val opt_context = Context.thread_data ();
--- a/src/Pure/ML/ml_env.ML Thu Apr 17 14:52:23 2014 +0200
+++ b/src/Pure/ML/ml_env.ML Sat Apr 19 17:23:05 2014 +0200
@@ -8,9 +8,9 @@
signature ML_ENV =
sig
val inherit: Context.generic -> Context.generic -> Context.generic
- val SML_name_space: ML_Name_Space.T
- val name_space: ML_Name_Space.T
+ val name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
val local_context: use_context
+ val local_name_space: ML_Name_Space.T
val check_functor: string -> unit
end
@@ -64,62 +64,35 @@
val inherit = Env.put o Env.get;
-(* SML name space *)
-
-val SML_name_space: ML_Name_Space.T =
- let
- fun lookup which name =
- Context.the_thread_data ()
- |> (fn context => Symtab.lookup (which (#sml_tables (Env.get context))) name);
-
- fun all which () =
- Context.the_thread_data ()
- |> (fn context => Symtab.dest (which (#sml_tables (Env.get context))))
- |> sort_distinct (string_ord o pairself #1);
+(* name space *)
- fun enter which entry =
- Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
- let val sml_tables' = which (Symtab.update entry) sml_tables
- in make_data (bootstrap, tables, sml_tables') end));
- in
- {lookupVal = lookup #1,
- lookupType = lookup #2,
- lookupFix = lookup #3,
- lookupStruct = lookup #4,
- lookupSig = lookup #5,
- lookupFunct = lookup #6,
- enterVal = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)),
- enterType = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)),
- enterFix = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)),
- enterStruct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)),
- enterSig = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)),
- enterFunct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)),
- allVal = all #1,
- allType = all #2,
- allFix = all #3,
- allStruct = all #4,
- allSig = all #5,
- allFunct = all #6}
- end;
-
-
-(* Isabelle/ML name space *)
-
-val name_space: ML_Name_Space.T =
+fun name_space {SML, exchange} : ML_Name_Space.T =
let
fun lookup sel1 sel2 name =
- Context.thread_data ()
- |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
- |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
+ if SML then
+ Context.the_thread_data ()
+ |> (fn context => Symtab.lookup (sel1 (#sml_tables (Env.get context))) name)
+ else
+ Context.thread_data ()
+ |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
+ |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
fun all sel1 sel2 () =
- Context.thread_data ()
- |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
- |> append (sel2 ML_Name_Space.global ())
+ (if SML then
+ Context.the_thread_data ()
+ |> (fn context => Symtab.dest (sel1 (#sml_tables (Env.get context))))
+ else
+ Context.thread_data ()
+ |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
+ |> append (sel2 ML_Name_Space.global ()))
|> sort_distinct (string_ord o pairself #1);
fun enter ap1 sel2 entry =
- if is_some (Context.thread_data ()) then
+ if SML <> exchange then
+ Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
+ let val sml_tables' = ap1 (Symtab.update entry) sml_tables
+ in make_data (bootstrap, tables, sml_tables') end))
+ else if is_some (Context.thread_data ()) then
Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
let
val _ = if bootstrap then sel2 ML_Name_Space.global entry else ();
@@ -149,12 +122,14 @@
val local_context: use_context =
{tune_source = ML_Parse.fix_ints,
- name_space = name_space,
+ name_space = name_space {SML = false, exchange = false},
str_of_pos = Position.here oo Position.line_file,
print = writeln,
error = error};
-val is_functor = is_some o #lookupFunct name_space;
+val local_name_space = #name_space local_context;
+
+val is_functor = is_some o #lookupFunct local_name_space;
fun check_functor name =
if not (is_functor "Table") (*mask dummy version of name_space*) orelse is_functor name then ()
--- a/src/Pure/Pure.thy Thu Apr 17 14:52:23 2014 +0200
+++ b/src/Pure/Pure.thy Sat Apr 19 17:23:05 2014 +0200
@@ -14,7 +14,6 @@
"infixr" "is" "keywords" "notes" "obtains" "open" "output"
"overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
and "theory" :: thy_begin % "theory"
- and "SML_file" "ML_file" :: thy_load % "ML"
and "header" :: diag
and "chapter" :: thy_heading1
and "section" :: thy_heading2
@@ -30,6 +29,8 @@
"definition" "abbreviation" "type_notation" "no_type_notation" "notation"
"no_notation" "axiomatization" "theorems" "lemmas" "declare"
"hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
+ and "SML_file" "ML_file" :: thy_load % "ML"
+ and "SML_import" "SML_export" :: thy_decl % "ML"
and "ML" :: thy_decl % "ML"
and "ML_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *)
and "ML_val" "ML_command" :: diag % "ML"
--- a/src/Pure/pure_syn.ML Thu Apr 17 14:52:23 2014 +0200
+++ b/src/Pure/pure_syn.ML Sat Apr 19 17:23:05 2014 +0200
@@ -23,7 +23,7 @@
val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
val provide = Resources.provide (src_path, digest);
val source = {delimited = true, text = cat_lines lines, pos = pos};
- val flags = {SML = false, redirect = true, verbose = true};
+ val flags = {SML = false, exchange = false, redirect = true, verbose = true};
in
gthy
|> ML_Context.exec (fn () => ML_Context.eval_source flags source)
--- a/src/Tools/Code/code_runtime.ML Thu Apr 17 14:52:23 2014 +0200
+++ b/src/Tools/Code/code_runtime.ML Sat Apr 19 17:23:05 2014 +0200
@@ -392,7 +392,7 @@
fun notify_val (string, value) =
let
- val _ = #enterVal ML_Env.name_space (string, value);
+ val _ = #enterVal ML_Env.local_name_space (string, value);
val _ = Theory.setup (Loaded_Values.map (insert (op =) string));
in () end;
@@ -401,24 +401,24 @@
val notifying_context : use_context =
{tune_source = #tune_source ML_Env.local_context,
name_space =
- {lookupVal = #lookupVal ML_Env.name_space,
- lookupType = #lookupType ML_Env.name_space,
- lookupFix = #lookupFix ML_Env.name_space,
- lookupStruct = #lookupStruct ML_Env.name_space,
- lookupSig = #lookupSig ML_Env.name_space,
- lookupFunct = #lookupFunct ML_Env.name_space,
+ {lookupVal = #lookupVal ML_Env.local_name_space,
+ lookupType = #lookupType ML_Env.local_name_space,
+ lookupFix = #lookupFix ML_Env.local_name_space,
+ lookupStruct = #lookupStruct ML_Env.local_name_space,
+ lookupSig = #lookupSig ML_Env.local_name_space,
+ lookupFunct = #lookupFunct ML_Env.local_name_space,
enterVal = notify_val,
enterType = abort,
enterFix = abort,
enterStruct = abort,
enterSig = abort,
enterFunct = abort,
- allVal = #allVal ML_Env.name_space,
- allType = #allType ML_Env.name_space,
- allFix = #allFix ML_Env.name_space,
- allStruct = #allStruct ML_Env.name_space,
- allSig = #allSig ML_Env.name_space,
- allFunct = #allFunct ML_Env.name_space},
+ allVal = #allVal ML_Env.local_name_space,
+ allType = #allType ML_Env.local_name_space,
+ allFix = #allFix ML_Env.local_name_space,
+ allStruct = #allStruct ML_Env.local_name_space,
+ allSig = #allSig ML_Env.local_name_space,
+ allFunct = #allFunct ML_Env.local_name_space},
str_of_pos = #str_of_pos ML_Env.local_context,
print = #print ML_Env.local_context,
error = #error ML_Env.local_context};
--- a/src/Tools/SML/Examples.thy Thu Apr 17 14:52:23 2014 +0200
+++ b/src/Tools/SML/Examples.thy Sat Apr 19 17:23:05 2014 +0200
@@ -23,7 +23,6 @@
SML_file "factorial.sml"
-
text {*
The subsequent example illustrates the use of multiple 'SML_file'
commands to build larger Standard ML projects. The toplevel SML
@@ -34,4 +33,20 @@
SML_file "Example.sig"
SML_file "Example.sml"
+
+text {*
+ Isabelle/ML and SML share a common run-time system, but the static
+ environments are separate. It is possible to exchange toplevel bindings
+ via separate commands like this.
+*}
+
+SML_export {* val f = factorial *} -- {* re-use factorial from SML environment *}
+ML {* f 42 *}
+
+SML_import {* val println = Output.writeln *}
+ -- {* re-use Isabelle/ML channel for SML *}
+
+SML_import {* val par_map = Par_List.map *}
+ -- {* re-use Isabelle/ML parallel list combinator for SML *}
+
end