--- a/src/HOL/Code_Evaluation.thy Wed Sep 15 16:22:12 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy Wed Sep 15 16:35:49 2010 +0200
@@ -315,7 +315,7 @@
fun tracing s x = (Output.tracing s; x);
-fun eval_term thy t = Code_Eval.eval NONE (Evaluation.get, put_term, "Code_Evaluation.put_term")
+fun eval_term thy t = Code_Runtime.value NONE (Evaluation.get, put_term, "Code_Evaluation.put_term")
I thy (HOLogic.mk_term_of (fastype_of t) t) [];
end
--- a/src/HOL/HOL.thy Wed Sep 15 16:22:12 2010 +0200
+++ b/src/HOL/HOL.thy Wed Sep 15 16:35:49 2010 +0200
@@ -1978,7 +1978,7 @@
val t = Thm.term_of ct;
val dummy = @{cprop True};
in case try HOLogic.dest_Trueprop t
- of SOME t' => if Code_Eval.eval NONE
+ of SOME t' => if Code_Runtime.value NONE
(Eval_Method.get, Eval_Method.put, "Eval_Method.put") (K I) thy t' []
then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
else dummy
--- a/src/HOL/IsaMakefile Wed Sep 15 16:22:12 2010 +0200
+++ b/src/HOL/IsaMakefile Wed Sep 15 16:35:49 2010 +0200
@@ -106,12 +106,12 @@
$(SRC)/Provers/quantifier1.ML \
$(SRC)/Provers/splitter.ML \
$(SRC)/Tools/cache_io.ML \
- $(SRC)/Tools/Code/code_eval.ML \
$(SRC)/Tools/Code/code_haskell.ML \
$(SRC)/Tools/Code/code_ml.ML \
$(SRC)/Tools/Code/code_namespace.ML \
$(SRC)/Tools/Code/code_preproc.ML \
$(SRC)/Tools/Code/code_printer.ML \
+ $(SRC)/Tools/Code/code_runtime.ML \
$(SRC)/Tools/Code/code_scala.ML \
$(SRC)/Tools/Code/code_simp.ML \
$(SRC)/Tools/Code/code_target.ML \
--- a/src/HOL/Library/Eval_Witness.thy Wed Sep 15 16:22:12 2010 +0200
+++ b/src/HOL/Library/Eval_Witness.thy Wed Sep 15 16:35:49 2010 +0200
@@ -59,7 +59,7 @@
| dest_exs _ _ = sys_error "dest_exs";
val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
in
- if Code_Eval.eval NONE (Eval_Method.get, Eval_Method.put, "Eval_Method.put") (K I) thy t ws
+ if Code_Runtime.value NONE (Eval_Method.get, Eval_Method.put, "Eval_Method.put") (K I) thy t ws
then Thm.cterm_of thy goal
else @{cprop True} (*dummy*)
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 15 16:22:12 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 15 16:35:49 2010 +0200
@@ -3277,7 +3277,7 @@
val [nrandom, size, depth] = arguments
in
rpair NONE (fst (DSequence.yieldn k
- (Code_Eval.eval NONE (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
+ (Code_Runtime.value NONE (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
(fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc)
thy t' [] nrandom size
|> Random_Engine.run)
@@ -3285,7 +3285,7 @@
end
| DSeq =>
rpair NONE (fst (DSequence.yieldn k
- (Code_Eval.eval NONE (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
+ (Code_Runtime.value NONE (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
DSequence.map thy t' []) (the_single arguments) true))
| New_Pos_Random_DSeq =>
let
@@ -3295,14 +3295,14 @@
if stats then
apsnd (SOME o accumulate) (split_list
(fst (Lazy_Sequence.yieldn k
- (Code_Eval.eval NONE
+ (Code_Runtime.value NONE
(Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result")
(fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
|> Lazy_Sequence.mapa (apfst proc))
thy t' [] nrandom size seed depth))))
else rpair NONE
(fst (Lazy_Sequence.yieldn k
- (Code_Eval.eval NONE
+ (Code_Runtime.value NONE
(Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
(fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
|> Lazy_Sequence.mapa proc)
@@ -3310,7 +3310,7 @@
end
| _ =>
rpair NONE (fst (Predicate.yieldn k
- (Code_Eval.eval NONE (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
+ (Code_Runtime.value NONE (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
Predicate.map thy t' [])))
in ((T, ts), statistics) end;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Sep 15 16:22:12 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Sep 15 16:35:49 2010 +0200
@@ -272,7 +272,7 @@
Pos_Random_DSeq =>
let
val compiled_term =
- Code_Eval.eval (SOME target) (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
+ Code_Runtime.value (SOME target) (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
(fn proc => fn g => fn n => fn size => fn s => g n size s |>> (DSequence.map o map) proc)
thy4 qc_term []
in
@@ -283,7 +283,7 @@
| New_Pos_Random_DSeq =>
let
val compiled_term =
- Code_Eval.eval (SOME target)
+ Code_Runtime.value (SOME target)
(Lseq_Result.get, put_lseq_result, "Predicate_Compile_Quickcheck.put_lseq_result")
(fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
g nrandom size s depth |> (Lazy_Sequence.mapa o map) proc)
@@ -297,7 +297,7 @@
end
| Depth_Limited_Random =>
let
- val compiled_term = Code_Eval.eval (SOME target)
+ val compiled_term = Code_Runtime.value (SOME target)
(Pred_Result.get, put_pred_result, "Predicate_Compile_Quickcheck.put_pred_result")
(fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
g depth nrandom size seed |> (Predicate.map o map) proc)
--- a/src/HOL/Tools/quickcheck_generators.ML Wed Sep 15 16:22:12 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Wed Sep 15 16:35:49 2010 +0200
@@ -392,14 +392,14 @@
in if Quickcheck.report ctxt then
let
val t' = mk_reporting_generator_expr thy t Ts;
- val compile = Code_Eval.eval (SOME target)
+ val compile = Code_Runtime.value (SOME target)
(Counterexample_Report.get, put_counterexample_report, "Quickcheck_Generators.put_counterexample_report")
(fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) thy t' [];
in compile #> Random_Engine.run end
else
let
val t' = mk_generator_expr thy t Ts;
- val compile = Code_Eval.eval (SOME target)
+ val compile = Code_Runtime.value (SOME target)
(Counterexample.get, put_counterexample, "Quickcheck_Generators.put_counterexample")
(fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
val dummy_report = ([], false)
@@ -411,7 +411,7 @@
val setup =
Datatype.interpretation ensure_random_datatype
- #> Code_Target.extend_target (target, (Code_Eval.target, K I))
+ #> Code_Target.extend_target (target, (Code_Runtime.target, K I))
#> Context.theory_map
(Quickcheck.add_generator ("code", compile_generator_expr));
--- a/src/Tools/Code/code_eval.ML Wed Sep 15 16:22:12 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,222 +0,0 @@
-(* Title: Tools/Code/code_eval.ML
- Author: Florian Haftmann, TU Muenchen
-
-Runtime services building on code generation into implementation language SML.
-*)
-
-signature CODE_EVAL =
-sig
- val target: string
- val eval: string option
- -> (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string
- -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
- val setup: theory -> theory
-end;
-
-structure Code_Eval : CODE_EVAL =
-struct
-
-(** generic **)
-
-val target = "Eval";
-
-fun evaluation_code thy module_name tycos consts =
- let
- val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
- val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
- val (ml_code, target_names) = Code_Target.produce_code_for thy
- target NONE module_name [] naming program (consts' @ tycos');
- val (consts'', tycos'') = chop (length consts') target_names;
- val consts_map = map2 (fn const => fn NONE =>
- error ("Constant " ^ (quote o Code.string_of_const thy) const
- ^ "\nhas a user-defined serialization")
- | SOME const'' => (const, const'')) consts consts''
- val tycos_map = map2 (fn tyco => fn NONE =>
- error ("Type " ^ (quote o Sign.extern_type thy) tyco
- ^ "\nhas a user-defined serialization")
- | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
- in (ml_code, (tycos_map, consts_map)) end;
-
-
-(** evaluation **)
-
-fun eval some_target cookie postproc thy t args =
- let
- val ctxt = ProofContext.init_global thy;
- fun evaluator naming program ((_, (_, ty)), t) deps =
- let
- val _ = if Code_Thingol.contains_dictvar t then
- error "Term to be evaluated contains free dictionaries" else ();
- val value_name = "Value.VALUE.value"
- val program' = program
- |> Graph.new_node (value_name,
- Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE)))
- |> fold (curry Graph.add_edge value_name) deps;
- val (program_code, [SOME value_name']) = Code_Target.produce_code_for thy
- (the_default target some_target) NONE "Code" [] naming program' [value_name];
- val value_code = space_implode " "
- (value_name' :: map (enclose "(" ")") args);
- in ML_Context.value ctxt cookie (program_code, value_code) end;
- in Code_Thingol.dynamic_eval_value thy postproc evaluator t end;
-
-
-(** instrumentalization by antiquotation **)
-
-local
-
-structure Code_Antiq_Data = Proof_Data
-(
- type T = (string list * string list) * (bool
- * (string * ((string * string) list * (string * string) list)) lazy);
- fun init _ = (([], []), (true, (Lazy.value ("", ([], [])))));
-);
-
-val is_first_occ = fst o snd o Code_Antiq_Data.get;
-
-fun register_code new_tycos new_consts ctxt =
- let
- val ((tycos, consts), _) = Code_Antiq_Data.get ctxt;
- val tycos' = fold (insert (op =)) new_tycos tycos;
- val consts' = fold (insert (op =)) new_consts consts;
- val acc_code = Lazy.lazy (fn () =>
- evaluation_code (ProofContext.theory_of ctxt) "Code" tycos' consts');
- in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end;
-
-fun register_const const = register_code [] [const];
-
-fun register_datatype tyco constrs = register_code [tyco] constrs;
-
-fun print_const const all_struct_name tycos_map consts_map =
- (Long_Name.append all_struct_name o the o AList.lookup (op =) consts_map) const;
-
-fun print_code is_first print_it ctxt =
- let
- val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt;
- val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code;
- val ml_code = if is_first then ml_code
- else "";
- val all_struct_name = "Isabelle";
- in (ml_code, print_it all_struct_name tycos_map consts_map) end;
-
-in
-
-fun ml_code_antiq raw_const background =
- let
- val const = Code.check_const (ProofContext.theory_of background) raw_const;
- val is_first = is_first_occ background;
- val background' = register_const const background;
- in (print_code is_first (print_const const), background') end;
-
-end; (*local*)
-
-
-(** reflection support **)
-
-fun check_datatype thy tyco consts =
- let
- val constrs = (map (fst o fst) o snd o Code.get_type thy) tyco;
- val missing_constrs = subtract (op =) consts constrs;
- val _ = if null missing_constrs then []
- else error ("Missing constructor(s) " ^ commas (map quote missing_constrs)
- ^ " for datatype " ^ quote tyco);
- val false_constrs = subtract (op =) constrs consts;
- val _ = if null false_constrs then []
- else error ("Non-constructor(s) " ^ commas (map quote false_constrs)
- ^ " for datatype " ^ quote tyco);
- in () end;
-
-fun add_eval_tyco (tyco, tyco') thy =
- let
- val k = Sign.arity_number thy tyco;
- fun pr pr' fxy [] = tyco'
- | pr pr' fxy [ty] =
- Code_Printer.concat [pr' Code_Printer.BR ty, tyco']
- | pr pr' fxy tys =
- Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
- in
- thy
- |> Code_Target.add_tyco_syntax target tyco (SOME (k, pr))
- end;
-
-fun add_eval_constr (const, const') thy =
- let
- val k = Code.args_number thy const;
- fun pr pr' fxy ts = Code_Printer.brackify fxy
- (const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts)));
- in
- thy
- |> Code_Target.add_const_syntax target const (SOME (Code_Printer.simple_const_syntax (k, pr)))
- end;
-
-fun add_eval_const (const, const') = Code_Target.add_const_syntax target
- const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')));
-
-fun process (code_body, (tyco_map, (constr_map, const_map))) module_name NONE thy =
- thy
- |> Code_Target.add_reserved target module_name
- |> Context.theory_map
- (ML_Context.exec (fn () => ML_Context.eval_text true Position.none code_body))
- |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map
- |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map
- |> fold (add_eval_const o apsnd Code_Printer.str) const_map
- | process (code_body, _) _ (SOME file_name) thy =
- let
- val preamble =
- "(* Generated from " ^ Path.implode (Thy_Header.thy_path (Context.theory_name thy))
- ^ "; DO NOT EDIT! *)";
- val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code_body);
- in
- thy
- end;
-
-fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy =
- let
- val datatypes = map (fn (raw_tyco, raw_cos) =>
- (prep_type thy raw_tyco, map (prep_const thy) raw_cos)) raw_datatypes;
- val _ = map (uncurry (check_datatype thy)) datatypes;
- val tycos = map fst datatypes;
- val constrs = maps snd datatypes;
- val functions = map (prep_const thy) raw_functions;
- val result = evaluation_code thy module_name tycos (constrs @ functions)
- |> (apsnd o apsnd) (chop (length constrs));
- in
- thy
- |> process result module_name some_file
- end;
-
-val code_reflect = gen_code_reflect Code_Target.cert_tyco Code.check_const;
-val code_reflect_cmd = gen_code_reflect Code_Target.read_tyco Code.read_const;
-
-
-(** Isar setup **)
-
-val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
-
-local
-
-val datatypesK = "datatypes";
-val functionsK = "functions";
-val fileK = "file";
-val andK = "and"
-
-val _ = List.app Keyword.keyword [datatypesK, functionsK];
-
-val parse_datatype =
- Parse.name --| Parse.$$$ "=" -- (Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term)));
-
-in
-
-val _ =
- Outer_Syntax.command "code_reflect" "enrich runtime environment with generated code"
- Keyword.thy_decl (Parse.name -- Scan.optional (Parse.$$$ datatypesK |-- (parse_datatype
- ::: Scan.repeat (Parse.$$$ andK |-- parse_datatype))) []
- -- Scan.optional (Parse.$$$ functionsK |-- Scan.repeat1 Parse.name) []
- -- Scan.option (Parse.$$$ fileK |-- Parse.name)
- >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
- (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
-
-end; (*local*)
-
-val setup = Code_Target.extend_target (target, (Code_ML.target_SML, K I));
-
-end; (*struct*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Code/code_runtime.ML Wed Sep 15 16:35:49 2010 +0200
@@ -0,0 +1,222 @@
+(* Title: Tools/Code/code_runtime.ML
+ Author: Florian Haftmann, TU Muenchen
+
+Runtime services building on code generation into implementation language SML.
+*)
+
+signature CODE_RUNTIME =
+sig
+ val target: string
+ val value: string option
+ -> (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string
+ -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
+ val setup: theory -> theory
+end;
+
+structure Code_Runtime : CODE_RUNTIME =
+struct
+
+(** evaluation **)
+
+val target = "Eval";
+
+fun value some_target cookie postproc thy t args =
+ let
+ val ctxt = ProofContext.init_global thy;
+ fun evaluator naming program ((_, (_, ty)), t) deps =
+ let
+ val _ = if Code_Thingol.contains_dictvar t then
+ error "Term to be evaluated contains free dictionaries" else ();
+ val value_name = "Value.VALUE.value"
+ val program' = program
+ |> Graph.new_node (value_name,
+ Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE)))
+ |> fold (curry Graph.add_edge value_name) deps;
+ val (program_code, [SOME value_name']) = Code_Target.produce_code_for thy
+ (the_default target some_target) NONE "Code" [] naming program' [value_name];
+ val value_code = space_implode " "
+ (value_name' :: map (enclose "(" ")") args);
+ in ML_Context.value ctxt cookie (program_code, value_code) end;
+ in Code_Thingol.dynamic_eval_value thy postproc evaluator t end;
+
+
+(** instrumentalization **)
+
+fun evaluation_code thy module_name tycos consts =
+ let
+ val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
+ val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
+ val (ml_code, target_names) = Code_Target.produce_code_for thy
+ target NONE module_name [] naming program (consts' @ tycos');
+ val (consts'', tycos'') = chop (length consts') target_names;
+ val consts_map = map2 (fn const => fn NONE =>
+ error ("Constant " ^ (quote o Code.string_of_const thy) const
+ ^ "\nhas a user-defined serialization")
+ | SOME const'' => (const, const'')) consts consts''
+ val tycos_map = map2 (fn tyco => fn NONE =>
+ error ("Type " ^ (quote o Sign.extern_type thy) tyco
+ ^ "\nhas a user-defined serialization")
+ | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
+ in (ml_code, (tycos_map, consts_map)) end;
+
+
+(* by antiquotation *)
+
+local
+
+structure Code_Antiq_Data = Proof_Data
+(
+ type T = (string list * string list) * (bool
+ * (string * ((string * string) list * (string * string) list)) lazy);
+ fun init _ = (([], []), (true, (Lazy.value ("", ([], [])))));
+);
+
+val is_first_occ = fst o snd o Code_Antiq_Data.get;
+
+fun register_code new_tycos new_consts ctxt =
+ let
+ val ((tycos, consts), _) = Code_Antiq_Data.get ctxt;
+ val tycos' = fold (insert (op =)) new_tycos tycos;
+ val consts' = fold (insert (op =)) new_consts consts;
+ val acc_code = Lazy.lazy (fn () =>
+ evaluation_code (ProofContext.theory_of ctxt) "Code" tycos' consts');
+ in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end;
+
+fun register_const const = register_code [] [const];
+
+fun register_datatype tyco constrs = register_code [tyco] constrs;
+
+fun print_const const all_struct_name tycos_map consts_map =
+ (Long_Name.append all_struct_name o the o AList.lookup (op =) consts_map) const;
+
+fun print_code is_first print_it ctxt =
+ let
+ val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt;
+ val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code;
+ val ml_code = if is_first then ml_code
+ else "";
+ val all_struct_name = "Isabelle";
+ in (ml_code, print_it all_struct_name tycos_map consts_map) end;
+
+in
+
+fun ml_code_antiq raw_const background =
+ let
+ val const = Code.check_const (ProofContext.theory_of background) raw_const;
+ val is_first = is_first_occ background;
+ val background' = register_const const background;
+ in (print_code is_first (print_const const), background') end;
+
+end; (*local*)
+
+
+(* reflection support *)
+
+fun check_datatype thy tyco consts =
+ let
+ val constrs = (map (fst o fst) o snd o Code.get_type thy) tyco;
+ val missing_constrs = subtract (op =) consts constrs;
+ val _ = if null missing_constrs then []
+ else error ("Missing constructor(s) " ^ commas (map quote missing_constrs)
+ ^ " for datatype " ^ quote tyco);
+ val false_constrs = subtract (op =) constrs consts;
+ val _ = if null false_constrs then []
+ else error ("Non-constructor(s) " ^ commas (map quote false_constrs)
+ ^ " for datatype " ^ quote tyco);
+ in () end;
+
+fun add_eval_tyco (tyco, tyco') thy =
+ let
+ val k = Sign.arity_number thy tyco;
+ fun pr pr' fxy [] = tyco'
+ | pr pr' fxy [ty] =
+ Code_Printer.concat [pr' Code_Printer.BR ty, tyco']
+ | pr pr' fxy tys =
+ Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
+ in
+ thy
+ |> Code_Target.add_tyco_syntax target tyco (SOME (k, pr))
+ end;
+
+fun add_eval_constr (const, const') thy =
+ let
+ val k = Code.args_number thy const;
+ fun pr pr' fxy ts = Code_Printer.brackify fxy
+ (const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts)));
+ in
+ thy
+ |> Code_Target.add_const_syntax target const (SOME (Code_Printer.simple_const_syntax (k, pr)))
+ end;
+
+fun add_eval_const (const, const') = Code_Target.add_const_syntax target
+ const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')));
+
+fun process (code_body, (tyco_map, (constr_map, const_map))) module_name NONE thy =
+ thy
+ |> Code_Target.add_reserved target module_name
+ |> Context.theory_map
+ (ML_Context.exec (fn () => ML_Context.eval_text true Position.none code_body))
+ |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map
+ |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map
+ |> fold (add_eval_const o apsnd Code_Printer.str) const_map
+ | process (code_body, _) _ (SOME file_name) thy =
+ let
+ val preamble =
+ "(* Generated from " ^ Path.implode (Thy_Header.thy_path (Context.theory_name thy))
+ ^ "; DO NOT EDIT! *)";
+ val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code_body);
+ in
+ thy
+ end;
+
+fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy =
+ let
+ val datatypes = map (fn (raw_tyco, raw_cos) =>
+ (prep_type thy raw_tyco, map (prep_const thy) raw_cos)) raw_datatypes;
+ val _ = map (uncurry (check_datatype thy)) datatypes;
+ val tycos = map fst datatypes;
+ val constrs = maps snd datatypes;
+ val functions = map (prep_const thy) raw_functions;
+ val result = evaluation_code thy module_name tycos (constrs @ functions)
+ |> (apsnd o apsnd) (chop (length constrs));
+ in
+ thy
+ |> process result module_name some_file
+ end;
+
+val code_reflect = gen_code_reflect Code_Target.cert_tyco Code.check_const;
+val code_reflect_cmd = gen_code_reflect Code_Target.read_tyco Code.read_const;
+
+
+(** Isar setup **)
+
+val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
+
+local
+
+val datatypesK = "datatypes";
+val functionsK = "functions";
+val fileK = "file";
+val andK = "and"
+
+val _ = List.app Keyword.keyword [datatypesK, functionsK];
+
+val parse_datatype =
+ Parse.name --| Parse.$$$ "=" -- (Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term)));
+
+in
+
+val _ =
+ Outer_Syntax.command "code_reflect" "enrich runtime environment with generated code"
+ Keyword.thy_decl (Parse.name -- Scan.optional (Parse.$$$ datatypesK |-- (parse_datatype
+ ::: Scan.repeat (Parse.$$$ andK |-- parse_datatype))) []
+ -- Scan.optional (Parse.$$$ functionsK |-- Scan.repeat1 Parse.name) []
+ -- Scan.option (Parse.$$$ fileK |-- Parse.name)
+ >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
+ (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
+
+end; (*local*)
+
+val setup = Code_Target.extend_target (target, (Code_ML.target_SML, K I));
+
+end; (*struct*)
--- a/src/Tools/Code_Generator.thy Wed Sep 15 16:22:12 2010 +0200
+++ b/src/Tools/Code_Generator.thy Wed Sep 15 16:35:49 2010 +0200
@@ -21,7 +21,7 @@
"~~/src/Tools/Code/code_ml.ML"
"~~/src/Tools/Code/code_haskell.ML"
"~~/src/Tools/Code/code_scala.ML"
- "~~/src/Tools/Code/code_eval.ML"
+ "~~/src/Tools/Code/code_runtime.ML"
"~~/src/Tools/nbe.ML"
begin
@@ -32,7 +32,7 @@
#> Code_ML.setup
#> Code_Haskell.setup
#> Code_Scala.setup
- #> Code_Eval.setup
+ #> Code_Runtime.setup
#> Nbe.setup
#> Quickcheck.setup
*}