# HG changeset patch # User wenzelm # Date 1284561349 -7200 # Node ID 4a6243de74b98e82806cd59485c0298e9ff036f4 # Parent a8c337299bc18f36f3f1ddfb55a61addb765cfd6# Parent e8b94d51fa85a187fa7d7c838789209a09b0bff8 merged diff -r e8b94d51fa85 -r 4a6243de74b9 src/HOL/Code_Evaluation.thy --- 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 diff -r e8b94d51fa85 -r 4a6243de74b9 src/HOL/HOL.thy --- 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 \ \ prop \ prop \ prop"} ct) dummy else dummy diff -r e8b94d51fa85 -r 4a6243de74b9 src/HOL/IsaMakefile --- 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 \ diff -r e8b94d51fa85 -r 4a6243de74b9 src/HOL/Library/Eval_Witness.thy --- 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 diff -r e8b94d51fa85 -r 4a6243de74b9 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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; diff -r e8b94d51fa85 -r 4a6243de74b9 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- 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) diff -r e8b94d51fa85 -r 4a6243de74b9 src/HOL/Tools/quickcheck_generators.ML --- 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)); diff -r e8b94d51fa85 -r 4a6243de74b9 src/Tools/Code/code_eval.ML --- 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*) diff -r e8b94d51fa85 -r 4a6243de74b9 src/Tools/Code/code_runtime.ML --- /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*) diff -r e8b94d51fa85 -r 4a6243de74b9 src/Tools/Code_Generator.thy --- 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 *}