--- 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) = _)")
--- 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*)
--- 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