--- a/src/Tools/Code/code_eval.ML Wed Apr 28 14:54:17 2010 +0200
+++ b/src/Tools/Code/code_eval.ML Wed Apr 28 15:17:09 2010 +0200
@@ -9,7 +9,7 @@
val target: string
val eval: string option -> string * (unit -> 'a) option Unsynchronized.ref
-> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
- val evaluation_code: theory -> string list -> string list
+ val evaluation_code: theory -> string -> string list -> string list
-> string * ((string * string) list * (string * string) list)
val setup: theory -> theory
end;
@@ -23,12 +23,14 @@
val eval_struct_name = "Code";
-fun evaluation_code thy tycos consts =
+fun evaluation_code thy struct_name_hint 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 struct_name = if struct_name_hint = "" then eval_struct_name
+ else struct_name_hint;
val (ml_code, target_names) = Code_ML.evaluation_code_of thy target
- eval_struct_name naming program (consts' @ tycos');
+ struct_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
@@ -84,7 +86,8 @@
val (struct_name', ctxt') = if struct_name = ""
then ML_Antiquote.variant eval_struct_name ctxt
else (struct_name, ctxt);
- val acc_code = Lazy.lazy (fn () => evaluation_code (ProofContext.theory_of ctxt) tycos' consts');
+ val acc_code = Lazy.lazy
+ (fn () => evaluation_code (ProofContext.theory_of ctxt) eval_struct_name tycos' consts');
in CodeAntiqData.put ((tycos', consts'), (false, (struct_name', acc_code))) ctxt' end;
fun register_const const = register_code [] [const];
@@ -140,6 +143,71 @@
end; (*local*)
+(** reflection support **)
+
+fun check_datatype thy tyco consts =
+ let
+ val constrs = (map 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_syntax_tyco target tyco (SOME (k, pr))
+ end;
+
+fun add_eval_const (const, const') = Code_Target.add_syntax_const target
+ const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')));
+
+fun process (code_body, (tyco_map, const_map)) module_name NONE thy =
+ let
+ val pr = Code_Printer.str o Long_Name.append module_name;
+ in
+ thy
+ |> Code_Target.add_reserved target module_name
+ |> Context.theory_map (ML_Context.exec (fn () => ML_Context.eval true Position.none code_body))
+ |> fold (add_eval_tyco o apsnd pr) tyco_map
+ |> fold (add_eval_const o apsnd pr) const_map
+ end
+ | process (code_body, _) _ (SOME file_name) thy =
+ let
+ val preamble = "(* Generated from " ^ Path.implode (ThyLoad.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 functions = map (prep_const thy) raw_functions;
+ val _ = map (uncurry (check_datatype thy)) datatypes;
+ in
+ thy
+ |> process (evaluation_code thy module_name (map fst datatypes) (maps snd datatypes @ functions)) 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);
@@ -148,6 +216,35 @@
-- (Args.term ::: Scan.repeat (Scan.lift (Args.$$$ "|") |-- Args.term)))
>> ml_code_datatype_antiq);
+local
+
+structure P = OuterParse
+and K = OuterKeyword
+
+val datatypesK = "datatypes";
+val functionsK = "functions";
+val module_nameK = "module_name";
+val fileK = "file";
+val andK = "and"
+
+val _ = List.app K.keyword [datatypesK, functionsK];
+
+val parse_datatype = (P.name --| P.$$$ "=" -- (P.term ::: (Scan.repeat (P.$$$ "|" |-- P.term))));
+
+in
+
+val _ =
+ OuterSyntax.command "code_reflect" "enrich runtime environment with generated code"
+ K.thy_decl (Scan.optional (P.$$$ datatypesK |-- (parse_datatype
+ ::: Scan.repeat (P.$$$ andK |-- parse_datatype))) []
+ -- Scan.optional (P.$$$ functionsK |-- Scan.repeat1 P.name) []
+ --| P.$$$ module_nameK -- P.name
+ -- Scan.option (P.$$$ fileK |-- P.name)
+ >> (fn (((raw_datatypes, raw_functions), module_name), 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*)