merged

--- a/src/HOL/Lazy_Sequence.thy	Wed Apr 28 19:46:09 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Thu Apr 29 07:02:22 2010 +0200
@@ -123,6 +123,13 @@
 
 subsection {* Code setup *}
 
+code_reflect
+  datatypes lazy_sequence = Lazy_Sequence
+  functions map yield
+  module_name Lazy_Sequence
+
+(* FIXME formulate yieldn in the logic with type code_numeral -- get rid of mapa confusion *)
+
 ML {*
 signature LAZY_SEQUENCE =
 sig
@@ -130,14 +137,15 @@
   val yield : 'a lazy_sequence -> ('a * 'a lazy_sequence) option
   val yieldn : int -> 'a lazy_sequence -> ('a list * 'a lazy_sequence)
   val map : ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
+  val mapa : ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
 end;
 
 structure Lazy_Sequence : LAZY_SEQUENCE =
 struct
 
-@{code_datatype lazy_sequence = Lazy_Sequence}
+open Lazy_Sequence;
 
-val yield = @{code yield}
+fun map f = mapa f;
 
 fun anamorph f k x = (if k = 0 then ([], x)
   else case f x
@@ -148,17 +156,9 @@
 
 fun yieldn S = anamorph yield S;
 
-val map = @{code map}
-
 end;
 *}
 
-code_reserved Eval Lazy_Sequence
-
-code_type lazy_sequence (Eval "_/ Lazy'_Sequence.lazy'_sequence")
-
-code_const Lazy_Sequence (Eval "Lazy'_Sequence.Lazy'_Sequence")
-
 section {* With Hit Bound Value *}
 text {* assuming in negative context *}
 

--- a/src/HOL/Predicate.thy	Wed Apr 28 19:46:09 2010 +0200
+++ b/src/HOL/Predicate.thy	Thu Apr 29 07:02:22 2010 +0200
@@ -880,6 +880,11 @@
 
 code_abort not_unique
 
+code_reflect
+  datatypes pred = Seq and seq = Empty | Insert | Join
+  functions map
+  module_name Predicate
+
 ML {*
 signature PREDICATE =
 sig
@@ -893,15 +898,17 @@
 structure Predicate : PREDICATE =
 struct
 
-@{code_datatype pred = Seq};
-@{code_datatype seq = Empty | Insert | Join};
+datatype pred = datatype Predicate.pred
+datatype seq = datatype Predicate.seq
+
+fun map f = Predicate.map f;
 
-fun yield (@{code Seq} f) = next (f ())
-and next @{code Empty} = NONE
-  | next (@{code Insert} (x, P)) = SOME (x, P)
-  | next (@{code Join} (P, xq)) = (case yield P
+fun yield (Seq f) = next (f ())
+and next Empty = NONE
+  | next (Insert (x, P)) = SOME (x, P)
+  | next (Join (P, xq)) = (case yield P
      of NONE => next xq
-      | SOME (x, Q) => SOME (x, @{code Seq} (fn _ => @{code Join} (Q, xq))));
+      | SOME (x, Q) => SOME (x, Seq (fn _ => Join (Q, xq))));
 
 fun anamorph f k x = (if k = 0 then ([], x)
   else case f x
@@ -912,19 +919,9 @@
 
 fun yieldn P = anamorph yield P;
 
-fun map f = @{code map} f;
-
 end;
 *}
 
-code_reserved Eval Predicate
-
-code_type pred and seq
-  (Eval "_/ Predicate.pred" and "_/ Predicate.seq")
-
-code_const Seq and Empty and Insert and Join
-  (Eval "Predicate.Seq" and "Predicate.Empty" and "Predicate.Insert/ (_,/ _)" and "Predicate.Join/ (_,/ _)")
-
 no_notation
   inf (infixl "\<sqinter>" 70) and
   sup (infixl "\<squnion>" 65) and

--- a/src/Tools/Code/code_eval.ML	Wed Apr 28 19:46:09 2010 +0200
+++ b/src/Tools/Code/code_eval.ML	Thu Apr 29 07:02:22 2010 +0200
@@ -171,10 +171,20 @@
     |> Code_Target.add_syntax_tyco 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_ML.print_tuple pr' Code_Printer.BR (map fst ts)));
+  in
+    thy
+    |> Code_Target.add_syntax_const target const (SOME (Code_Printer.simple_const_syntax (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 =
+fun process (code_body, (tyco_map, (constr_map, const_map))) module_name NONE thy =
       let
         val pr = Code_Printer.str o Long_Name.append module_name;
       in
@@ -182,6 +192,7 @@
         |> 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_constr o apsnd pr) constr_map
         |> fold (add_eval_const o apsnd pr) const_map
       end
   | process (code_body, _) _ (SOME file_name) thy =
@@ -197,11 +208,15 @@
   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 _ = map (uncurry (check_datatype thy)) datatypes;
+    val result = evaluation_code thy module_name tycos (constrs @ functions)
+      |> (apsnd o apsnd) (chop (length constrs));
   in
     thy
-    |> process (evaluation_code thy module_name (map fst datatypes) (maps snd datatypes @ functions)) module_name some_file
+    |> process result module_name some_file
   end;
 
 val code_reflect = gen_code_reflect Code_Target.cert_tyco Code.check_const;

--- a/src/Tools/Code/code_ml.ML	Wed Apr 28 19:46:09 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Thu Apr 29 07:02:22 2010 +0200
@@ -9,6 +9,8 @@
   val target_SML: string
   val evaluation_code_of: theory -> string -> string
     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
+  val print_tuple: (Code_Printer.fixity -> 'a -> Pretty.T)
+    -> Code_Printer.fixity -> 'a list -> Pretty.T option
   val setup: theory -> theory
 end;