# HG changeset patch
# User wenzelm
# Date 1285944253 -7200
# Node ID 6ddbd932fc00e58c234e09964149b532818247ff
# Parent  ff9e9d5ac17173edbe51a8d3b4554f9ebfbecb0a# Parent  37bdc2220cf88bb3e8b80594cb656373af6cc660
merged

diff -r 37bdc2220cf8 -r 6ddbd932fc00 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Oct 01 15:11:15 2010 +0200
+++ b/src/HOL/Code_Numeral.thy	Fri Oct 01 16:44:13 2010 +0200
@@ -340,7 +340,7 @@
   (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
   (Haskell "divMod")
   (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
-  (Eval "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
+  (Eval "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (Integer.div'_mod n m))")
 
 code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   (SML "!((_ : Int.int) = _)")
diff -r 37bdc2220cf8 -r 6ddbd932fc00 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Fri Oct 01 15:11:15 2010 +0200
+++ b/src/Tools/Code/code_runtime.ML	Fri Oct 01 16:44:13 2010 +0200
@@ -26,6 +26,7 @@
     -> theory -> theory
   datatype truth = Holds
   val put_truth: (unit -> truth) -> Proof.context -> Proof.context
+  val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory
 end;
 
 structure Code_Runtime : CODE_RUNTIME =
@@ -341,4 +342,93 @@
 
 end; (*local*)
 
+
+(** using external SML files as substitute for proper definitions -- only for polyml!  **)
+
+local
+
+structure Loaded_Values = Theory_Data(
+  type T = string list
+  val empty = []
+  val merge = merge (op =)
+  val extend = I
+);
+
+fun notify_val (string, value) = 
+  let
+    val _ = #enterVal ML_Env.name_space (string, value);
+    val _ = Context.>> ((Context.map_theory o Loaded_Values.map) (insert (op =) string));
+  in () end;
+
+fun abort _ = error "Only value bindings allowed.";
+
+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,
+    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},
+  str_of_pos = #str_of_pos ML_Env.local_context,
+  print = #print ML_Env.local_context,
+  error = #error ML_Env.local_context};
+
+in
+
+fun use_file filepath thy =
+  let
+    val thy' = Loaded_Values.put [] thy;
+    val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
+    val _ = Secure.use_text notifying_context
+      (0, Path.implode filepath) false (File.read filepath);
+    val thy'' = (Context.the_theory o the) (Context.thread_data ())
+    val names = Loaded_Values.get thy''
+  in (names, thy'') end;
+
+end;
+
+fun add_definiendum (ml_name, (b, T)) thy =
+  thy
+  |> Code_Target.add_reserved target ml_name
+  |> Specification.axiomatization [(b, SOME T, NoSyn)] []
+  |-> (fn ([Const (const, _)], _) =>
+     Code_Target.add_const_syntax target const
+       (SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name))));
+
+fun process_file filepath (definienda, thy) =
+  let
+    val (ml_names, thy') = use_file filepath thy;
+    val superfluous = subtract (fn ((name1, _), name2) => name1 = name2) definienda ml_names;
+    val _ = if null superfluous then ()
+      else error ("Value binding(s) " ^ commas_quote superfluous
+        ^ " found in external file " ^ quote (Path.implode filepath)
+        ^ " not present among the given contants binding(s).");
+    val these_definienda = AList.make (the o AList.lookup (op =) definienda) ml_names;
+    val thy'' = fold add_definiendum these_definienda thy';
+    val definienda' = fold (AList.delete (op =)) ml_names definienda;
+  in (definienda', thy'') end;
+
+fun polyml_as_definition bTs filepaths thy =
+  let
+    val definienda = map (fn bT => ((Binding.name_of o fst) bT, bT)) bTs;
+    val (remaining, thy') = fold process_file filepaths (definienda, thy);
+    val _ = if null remaining then ()
+      else error ("Constant binding(s) " ^ commas_quote (map fst remaining)
+        ^ " not present in external file(s).");
+  in thy' end;
+
 end; (*struct*)
diff -r 37bdc2220cf8 -r 6ddbd932fc00 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Fri Oct 01 15:11:15 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Fri Oct 01 16:44:13 2010 +0200
@@ -244,12 +244,10 @@
 
 fun the_literals thy = #literals o the_fundamental thy;
 
-local
-
-fun activate_target thy target =
+fun collapse_hierarchy thy =
   let
-    val ((targets, abortable), default_width) = Targets.get thy;
-    fun collapse_hierarchy target =
+    val ((targets, _), _) = Targets.get thy;
+    fun collapse target = 
       let
         val data = case Symtab.lookup targets target
          of SOME data => data
@@ -257,10 +255,17 @@
       in case the_description data
        of Fundamental _ => (K I, data)
         | Extension (super, modify) => let
-            val (modify', data') = collapse_hierarchy super
+            val (modify', data') = collapse super
           in (fn naming => modify' naming #> modify naming, merge_target false target (data', data)) end
       end;
-    val (modify, data) = collapse_hierarchy target;
+  in collapse end;
+
+local
+
+fun activate_target thy target =
+  let
+    val ((targets, abortable), default_width) = Targets.get thy;
+    val (modify, data) = collapse_hierarchy thy target;
   in (default_width, abortable, data, modify) end;
 
 fun activate_syntax lookup_name src_tab = Symtab.empty
@@ -537,12 +542,16 @@
       then error ("Too many arguments in syntax for constant " ^ quote c)
       else syn);
 
-fun add_reserved target =
+fun add_reserved target sym thy =
   let
-    fun add sym syms = if member (op =) syms sym
+    val (_, data) = collapse_hierarchy thy target;
+    val _ = if member (op =) (the_reserved data) sym
       then error ("Reserved symbol " ^ quote sym ^ " already declared")
-      else insert (op =) sym syms
-  in map_reserved target o add end;
+      else ();
+  in
+    thy
+    |> map_reserved target (insert (op =) sym)
+  end;
 
 fun gen_add_include read_const target args thy =
   let