merge

--- a/etc/isar-keywords.el	Wed Apr 28 16:14:56 2010 +0200
+++ b/etc/isar-keywords.el	Wed Apr 28 16:15:45 2010 +0200
@@ -61,6 +61,7 @@
     "code_modulename"
     "code_monad"
     "code_pred"
+    "code_reflect"
     "code_reserved"
     "code_thms"
     "code_type"
@@ -288,10 +289,12 @@
     "congs"
     "constrains"
     "contains"
+    "datatypes"
     "defines"
     "file"
     "fixes"
     "for"
+    "functions"
     "hide_action"
     "hints"
     "identifier"
@@ -466,6 +469,7 @@
     "code_module"
     "code_modulename"
     "code_monad"
+    "code_reflect"
     "code_reserved"
     "code_type"
     "coinductive"

--- a/src/Tools/Code/code_eval.ML	Wed Apr 28 16:14:56 2010 +0200
+++ b/src/Tools/Code/code_eval.ML	Wed Apr 28 16:15:45 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*)

--- a/src/Tools/Code/code_target.ML	Wed Apr 28 16:14:56 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Wed Apr 28 16:15:45 2010 +0200
@@ -6,6 +6,9 @@
 
 signature CODE_TARGET =
 sig
+  val cert_tyco: theory -> string -> string
+  val read_tyco: theory -> string -> string
+
   type serializer
   type literals = Code_Printer.literals
   val add_target: string * (serializer * literals) -> theory -> theory