split off evaluation mechanisms in separte module Code_Eval
authorhaftmann
Mon Dec 07 16:27:48 2009 +0100 (2009-12-07)
changeset 340281e6206763036
parent 34023 7c2c38a5bca3
child 34029 d3dead6ae0d2
split off evaluation mechanisms in separte module Code_Eval
src/HOL/Code_Evaluation.thy
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/HOL/Library/Eval_Witness.thy
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
src/HOL/Tools/quickcheck_generators.ML
src/Tools/Code/code_eval.ML
src/Tools/Code/code_ml.ML
src/Tools/Code_Generator.thy
     1.1 --- a/src/HOL/Code_Evaluation.thy	Mon Dec 07 14:54:28 2009 +0100
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Mon Dec 07 16:27:48 2009 +0100
     1.3 @@ -279,7 +279,7 @@
     1.4  val eval_ref = Unsynchronized.ref (NONE : (unit -> term) option);
     1.5  
     1.6  fun eval_term thy t =
     1.7 -  Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
     1.8 +  Code_Eval.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
     1.9  
    1.10  end;
    1.11  *}
     2.1 --- a/src/HOL/HOL.thy	Mon Dec 07 14:54:28 2009 +0100
     2.2 +++ b/src/HOL/HOL.thy	Mon Dec 07 16:27:48 2009 +0100
     2.3 @@ -1971,7 +1971,7 @@
     2.4      val t = Thm.term_of ct;
     2.5      val dummy = @{cprop True};
     2.6    in case try HOLogic.dest_Trueprop t
     2.7 -   of SOME t' => if Code_ML.eval NONE
     2.8 +   of SOME t' => if Code_Eval.eval NONE
     2.9           ("Eval_Method.eval_ref", Eval_Method.eval_ref) (K I) thy t' [] 
    2.10         then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
    2.11         else dummy
     3.1 --- a/src/HOL/IsaMakefile	Mon Dec 07 14:54:28 2009 +0100
     3.2 +++ b/src/HOL/IsaMakefile	Mon Dec 07 16:27:48 2009 +0100
     3.3 @@ -103,6 +103,7 @@
     3.4    $(SRC)/Provers/hypsubst.ML \
     3.5    $(SRC)/Provers/quantifier1.ML \
     3.6    $(SRC)/Provers/splitter.ML \
     3.7 +  $(SRC)/Tools/Code/code_eval.ML \
     3.8    $(SRC)/Tools/Code/code_haskell.ML \
     3.9    $(SRC)/Tools/Code/code_ml.ML \
    3.10    $(SRC)/Tools/Code/code_preproc.ML \
     4.1 --- a/src/HOL/Library/Eval_Witness.thy	Mon Dec 07 14:54:28 2009 +0100
     4.2 +++ b/src/HOL/Library/Eval_Witness.thy	Mon Dec 07 16:27:48 2009 +0100
     4.3 @@ -68,7 +68,7 @@
     4.4      | dest_exs _ _ = sys_error "dest_exs";
     4.5    val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
     4.6  in
     4.7 -  if Code_ML.eval NONE ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) (K I) thy t ws
     4.8 +  if Code_Eval.eval NONE ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) (K I) thy t ws
     4.9    then Thm.cterm_of thy goal
    4.10    else @{cprop True} (*dummy*)
    4.11  end
     5.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Dec 07 14:54:28 2009 +0100
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Dec 07 16:27:48 2009 +0100
     5.3 @@ -2586,11 +2586,11 @@
     5.4      val t' = mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t;
     5.5      val eval =
     5.6        if random then
     5.7 -        Code_ML.eval NONE ("Predicate_Compile_Core.random_eval_ref", random_eval_ref)
     5.8 +        Code_Eval.eval NONE ("Predicate_Compile_Core.random_eval_ref", random_eval_ref)
     5.9              (fn proc => fn g => fn s => g s |>> Predicate.map proc) thy t' []
    5.10            |> Random_Engine.run
    5.11        else
    5.12 -        Code_ML.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref) Predicate.map thy t' []
    5.13 +        Code_Eval.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref) Predicate.map thy t' []
    5.14    in (T, eval) end;
    5.15  
    5.16  fun values ctxt param_user_modes options k t_compr =
     6.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Mon Dec 07 14:54:28 2009 +0100
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Mon Dec 07 16:27:48 2009 +0100
     6.3 @@ -106,7 +106,7 @@
     6.4        mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term}
     6.5        (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))))
     6.6      val _ = tracing (Syntax.string_of_term ctxt' qc_term)
     6.7 -    val compile = Code_ML.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref)
     6.8 +    val compile = Code_Eval.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref)
     6.9        (fn proc => fn g => fn s => g s #>> (Predicate.map o map) proc)
    6.10        thy'' qc_term []
    6.11    in
     7.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Mon Dec 07 14:54:28 2009 +0100
     7.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Mon Dec 07 16:27:48 2009 +0100
     7.3 @@ -379,7 +379,7 @@
     7.4    let
     7.5      val Ts = (map snd o fst o strip_abs) t;
     7.6      val t' = mk_generator_expr thy t Ts;
     7.7 -    val compile = Code_ML.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref)
     7.8 +    val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref)
     7.9        (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
    7.10    in compile #> Random_Engine.run end;
    7.11  
    7.12 @@ -388,7 +388,7 @@
    7.13  
    7.14  val setup = Typecopy.interpretation ensure_random_typecopy
    7.15    #> Datatype.interpretation ensure_random_datatype
    7.16 -  #> Code_Target.extend_target (target, (Code_ML.target_Eval, K I))
    7.17 +  #> Code_Target.extend_target (target, (Code_Eval.target, K I))
    7.18    #> Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of);
    7.19  
    7.20  end;
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Tools/Code/code_eval.ML	Mon Dec 07 16:27:48 2009 +0100
     8.3 @@ -0,0 +1,153 @@
     8.4 +(*  Title:      Tools/code/code_eval.ML_
     8.5 +    Author:     Florian Haftmann, TU Muenchen
     8.6 +
     8.7 +Runtime services building on code generation into implementation language SML.
     8.8 +*)
     8.9 +
    8.10 +signature CODE_EVAL =
    8.11 +sig
    8.12 +  val target: string
    8.13 +  val eval: string option -> string * (unit -> 'a) option Unsynchronized.ref
    8.14 +    -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
    8.15 +  val evaluation_code: theory -> string list -> string list
    8.16 +    -> string * ((string * string) list * (string * string) list)
    8.17 +  val setup: theory -> theory
    8.18 +end;
    8.19 +
    8.20 +structure Code_Eval : CODE_EVAL =
    8.21 +struct
    8.22 +
    8.23 +(** generic **)
    8.24 +
    8.25 +val target = "Eval";
    8.26 +
    8.27 +val eval_struct_name = "Code"
    8.28 +
    8.29 +fun evaluation_code thy tycos consts =
    8.30 +  let
    8.31 +    val (consts', (naming, program)) = Code_Thingol.consts_program thy consts;
    8.32 +    val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
    8.33 +    val (ml_code, target_names) = Code_ML.evaluation_code_of thy target
    8.34 +      (SOME eval_struct_name) naming program (consts' @ tycos');
    8.35 +    val (consts'', tycos'') = chop (length consts') target_names;
    8.36 +    val consts_map = map2 (fn const => fn NONE =>
    8.37 +        error ("Constant " ^ (quote o Code.string_of_const thy) const
    8.38 +          ^ "\nhas a user-defined serialization")
    8.39 +      | SOME const'' => (const, const'')) consts consts''
    8.40 +    val tycos_map = map2 (fn tyco => fn NONE =>
    8.41 +        error ("Type " ^ (quote o Sign.extern_type thy) tyco
    8.42 +          ^ "\nhas a user-defined serialization")
    8.43 +      | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
    8.44 +  in (ml_code, (tycos_map, consts_map)) end;
    8.45 +
    8.46 +
    8.47 +(** evaluation **)
    8.48 +
    8.49 +fun eval some_target reff postproc thy t args =
    8.50 +  let
    8.51 +    val ctxt = ProofContext.init thy;
    8.52 +    fun evaluator naming program ((_, (_, ty)), t) deps =
    8.53 +      let
    8.54 +        val _ = if Code_Thingol.contains_dictvar t then
    8.55 +          error "Term to be evaluated contains free dictionaries" else ();
    8.56 +        val value_name = "Value.VALUE.value"
    8.57 +        val program' = program
    8.58 +          |> Graph.new_node (value_name,
    8.59 +              Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))])))
    8.60 +          |> fold (curry Graph.add_edge value_name) deps;
    8.61 +        val (value_code, [SOME value_name']) = Code_ML.evaluation_code_of thy
    8.62 +          (the_default target some_target) NONE naming program' [value_name];
    8.63 +        val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
    8.64 +          ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
    8.65 +      in ML_Context.evaluate ctxt false reff sml_code end;
    8.66 +  in Code_Thingol.eval thy postproc evaluator t end;
    8.67 +
    8.68 +
    8.69 +(** instrumentalization by antiquotation **)
    8.70 +
    8.71 +local
    8.72 +
    8.73 +structure CodeAntiqData = Proof_Data
    8.74 +(
    8.75 +  type T = (string list * string list) * (bool * (string
    8.76 +    * (string * ((string * string) list * (string * string) list)) lazy));
    8.77 +  fun init _ = (([], []), (true, ("", Lazy.value ("", ([], [])))));
    8.78 +);
    8.79 +
    8.80 +val is_first_occ = fst o snd o CodeAntiqData.get;
    8.81 +
    8.82 +fun register_code new_tycos new_consts ctxt =
    8.83 +  let
    8.84 +    val ((tycos, consts), (_, (struct_name, _))) = CodeAntiqData.get ctxt;
    8.85 +    val tycos' = fold (insert (op =)) new_tycos tycos;
    8.86 +    val consts' = fold (insert (op =)) new_consts consts;
    8.87 +    val (struct_name', ctxt') = if struct_name = ""
    8.88 +      then ML_Antiquote.variant eval_struct_name ctxt
    8.89 +      else (struct_name, ctxt);
    8.90 +    val acc_code = Lazy.lazy (fn () => evaluation_code (ProofContext.theory_of ctxt) tycos' consts');
    8.91 +  in CodeAntiqData.put ((tycos', consts'), (false, (struct_name', acc_code))) ctxt' end;
    8.92 +
    8.93 +fun register_const const = register_code [] [const];
    8.94 +
    8.95 +fun register_datatype tyco constrs = register_code [tyco] constrs;
    8.96 +
    8.97 +fun print_const const all_struct_name tycos_map consts_map =
    8.98 +  (Long_Name.append all_struct_name o the o AList.lookup (op =) consts_map) const;
    8.99 +
   8.100 +fun print_datatype tyco constrs all_struct_name tycos_map consts_map =
   8.101 +  let
   8.102 +    val upperize = implode o nth_map 0 Symbol.to_ascii_upper o explode;
   8.103 +    fun check_base name name'' =
   8.104 +      if upperize (Long_Name.base_name name) = upperize name''
   8.105 +      then () else error ("Name as printed " ^ quote name''
   8.106 +        ^ "\ndiffers from logical base name " ^ quote (Long_Name.base_name name) ^ "; sorry.");
   8.107 +    val tyco'' = (the o AList.lookup (op =) tycos_map) tyco;
   8.108 +    val constrs'' = map (the o AList.lookup (op =) consts_map) constrs;
   8.109 +    val _ = check_base tyco tyco'';
   8.110 +    val _ = map2 check_base constrs constrs'';
   8.111 +  in "datatype " ^ tyco'' ^ " = datatype " ^ Long_Name.append all_struct_name tyco'' end;
   8.112 +
   8.113 +fun print_code struct_name is_first print_it ctxt =
   8.114 +  let
   8.115 +    val (_, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
   8.116 +    val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code;
   8.117 +    val ml_code = if is_first then ml_code
   8.118 +      else "";
   8.119 +    val all_struct_name = Long_Name.append struct_name struct_code_name;
   8.120 +  in (ml_code, print_it all_struct_name tycos_map consts_map) end;
   8.121 +
   8.122 +in
   8.123 +
   8.124 +fun ml_code_antiq raw_const {struct_name, background} =
   8.125 +  let
   8.126 +    val const = Code.check_const (ProofContext.theory_of background) raw_const;
   8.127 +    val is_first = is_first_occ background;
   8.128 +    val background' = register_const const background;
   8.129 +  in (print_code struct_name is_first (print_const const), background') end;
   8.130 +
   8.131 +fun ml_code_datatype_antiq (raw_tyco, raw_constrs) {struct_name, background} =
   8.132 +  let
   8.133 +    val thy = ProofContext.theory_of background;
   8.134 +    val tyco = Sign.intern_type thy raw_tyco;
   8.135 +    val constrs = map (Code.check_const thy) raw_constrs;
   8.136 +    val constrs' = (map fst o snd o Code.get_datatype thy) tyco;
   8.137 +    val _ = if eq_set (op =) (constrs, constrs') then ()
   8.138 +      else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors")
   8.139 +    val is_first = is_first_occ background;
   8.140 +    val background' = register_datatype tyco constrs background;
   8.141 +  in (print_code struct_name is_first (print_datatype tyco constrs), background') end;
   8.142 +
   8.143 +end; (*local*)
   8.144 +
   8.145 +
   8.146 +(** Isar setup **)
   8.147 +
   8.148 +val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
   8.149 +val _ = ML_Context.add_antiq "code_datatype" (fn _ =>
   8.150 +  (Args.tyname --| Scan.lift (Args.$$$ "=")
   8.151 +    -- (Args.term ::: Scan.repeat (Scan.lift (Args.$$$ "|") |-- Args.term)))
   8.152 +      >> ml_code_datatype_antiq);
   8.153 +
   8.154 +val setup = Code_Target.extend_target (target, (Code_ML.target_SML, K I));
   8.155 +
   8.156 +end; (*struct*)
     9.1 --- a/src/Tools/Code/code_ml.ML	Mon Dec 07 14:54:28 2009 +0100
     9.2 +++ b/src/Tools/Code/code_ml.ML	Mon Dec 07 16:27:48 2009 +0100
     9.3 @@ -6,9 +6,9 @@
     9.4  
     9.5  signature CODE_ML =
     9.6  sig
     9.7 -  val eval: string option -> string * (unit -> 'a) option Unsynchronized.ref
     9.8 -    -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
     9.9 -  val target_Eval: string
    9.10 +  val target_SML: string
    9.11 +  val evaluation_code_of: theory -> string -> string option
    9.12 +    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
    9.13    val setup: theory -> theory
    9.14  end;
    9.15  
    9.16 @@ -26,7 +26,6 @@
    9.17  
    9.18  val target_SML = "SML";
    9.19  val target_OCaml = "OCaml";
    9.20 -val target_Eval = "Eval";
    9.21  
    9.22  datatype ml_binding =
    9.23      ML_Function of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)
    9.24 @@ -937,142 +936,19 @@
    9.25  end; (*local*)
    9.26  
    9.27  
    9.28 -(** ML (system language) code for evaluation and instrumentalization **)
    9.29 +(** for instrumentalization **)
    9.30  
    9.31 -val eval_struct_name = "Code"
    9.32 -
    9.33 -fun eval_code_of some_target with_struct thy =
    9.34 +fun evaluation_code_of thy target some_struct_name =
    9.35    let
    9.36 -    val target = the_default target_Eval some_target;
    9.37 -    val serialize = if with_struct then fn _ => fn [] =>
    9.38 -        serialize_ml target_SML (SOME (K ())) print_sml_module print_sml_stmt (SOME eval_struct_name) true
    9.39 +    val serialize = if is_some some_struct_name then fn _ => fn [] =>
    9.40 +        serialize_ml target (SOME (K ())) print_sml_module print_sml_stmt some_struct_name true
    9.41        else fn _ => fn [] => 
    9.42 -        serialize_ml target_SML (SOME (K ())) ((K o K) Pretty.chunks2) print_sml_stmt (SOME eval_struct_name) true;
    9.43 +        serialize_ml target (SOME (K ())) ((K o K) Pretty.chunks2) print_sml_stmt some_struct_name true;
    9.44    in Code_Target.serialize_custom thy (target, (serialize, literals_sml)) end;
    9.45  
    9.46  
    9.47 -(* evaluation *)
    9.48 -
    9.49 -fun eval some_target reff postproc thy t args =
    9.50 -  let
    9.51 -    val ctxt = ProofContext.init thy;
    9.52 -    fun evaluator naming program ((_, (_, ty)), t) deps =
    9.53 -      let
    9.54 -        val _ = if Code_Thingol.contains_dictvar t then
    9.55 -          error "Term to be evaluated contains free dictionaries" else ();
    9.56 -        val value_name = "Value.VALUE.value"
    9.57 -        val program' = program
    9.58 -          |> Graph.new_node (value_name,
    9.59 -              Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))])))
    9.60 -          |> fold (curry Graph.add_edge value_name) deps;
    9.61 -        val (value_code, [SOME value_name']) = eval_code_of some_target false thy naming program' [value_name];
    9.62 -        val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
    9.63 -          ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
    9.64 -      in ML_Context.evaluate ctxt false reff sml_code end;
    9.65 -  in Code_Thingol.eval thy postproc evaluator t end;
    9.66 -
    9.67 -
    9.68 -(* instrumentalization by antiquotation *)
    9.69 -
    9.70 -local
    9.71 -
    9.72 -structure CodeAntiqData = Proof_Data
    9.73 -(
    9.74 -  type T = (string list * string list) * (bool * (string
    9.75 -    * (string * ((string * string) list * (string * string) list)) lazy));
    9.76 -  fun init _ = (([], []), (true, ("", Lazy.value ("", ([], [])))));
    9.77 -);
    9.78 -
    9.79 -val is_first_occ = fst o snd o CodeAntiqData.get;
    9.80 -
    9.81 -fun delayed_code thy tycos consts () =
    9.82 -  let
    9.83 -    val (consts', (naming, program)) = Code_Thingol.consts_program thy consts;
    9.84 -    val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
    9.85 -    val (ml_code, target_names) = eval_code_of NONE true thy naming program (consts' @ tycos');
    9.86 -    val (consts'', tycos'') = chop (length consts') target_names;
    9.87 -    val consts_map = map2 (fn const => fn NONE =>
    9.88 -        error ("Constant " ^ (quote o Code.string_of_const thy) const
    9.89 -          ^ "\nhas a user-defined serialization")
    9.90 -      | SOME const'' => (const, const'')) consts consts''
    9.91 -    val tycos_map = map2 (fn tyco => fn NONE =>
    9.92 -        error ("Type " ^ (quote o Sign.extern_type thy) tyco
    9.93 -          ^ "\nhas a user-defined serialization")
    9.94 -      | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
    9.95 -  in (ml_code, (tycos_map, consts_map)) end;
    9.96 -
    9.97 -fun register_code new_tycos new_consts ctxt =
    9.98 -  let
    9.99 -    val ((tycos, consts), (_, (struct_name, _))) = CodeAntiqData.get ctxt;
   9.100 -    val tycos' = fold (insert (op =)) new_tycos tycos;
   9.101 -    val consts' = fold (insert (op =)) new_consts consts;
   9.102 -    val (struct_name', ctxt') = if struct_name = ""
   9.103 -      then ML_Antiquote.variant eval_struct_name ctxt
   9.104 -      else (struct_name, ctxt);
   9.105 -    val acc_code = Lazy.lazy (delayed_code (ProofContext.theory_of ctxt) tycos' consts');
   9.106 -  in CodeAntiqData.put ((tycos', consts'), (false, (struct_name', acc_code))) ctxt' end;
   9.107 -
   9.108 -fun register_const const = register_code [] [const];
   9.109 -
   9.110 -fun register_datatype tyco constrs = register_code [tyco] constrs;
   9.111 -
   9.112 -fun print_const const all_struct_name tycos_map consts_map =
   9.113 -  (Long_Name.append all_struct_name o the o AList.lookup (op =) consts_map) const;
   9.114 -
   9.115 -fun print_datatype tyco constrs all_struct_name tycos_map consts_map =
   9.116 -  let
   9.117 -    val upperize = implode o nth_map 0 Symbol.to_ascii_upper o explode;
   9.118 -    fun check_base name name'' =
   9.119 -      if upperize (Long_Name.base_name name) = upperize name''
   9.120 -      then () else error ("Name as printed " ^ quote name''
   9.121 -        ^ "\ndiffers from logical base name " ^ quote (Long_Name.base_name name) ^ "; sorry.");
   9.122 -    val tyco'' = (the o AList.lookup (op =) tycos_map) tyco;
   9.123 -    val constrs'' = map (the o AList.lookup (op =) consts_map) constrs;
   9.124 -    val _ = check_base tyco tyco'';
   9.125 -    val _ = map2 check_base constrs constrs'';
   9.126 -  in "datatype " ^ tyco'' ^ " = datatype " ^ Long_Name.append all_struct_name tyco'' end;
   9.127 -
   9.128 -fun print_code struct_name is_first print_it ctxt =
   9.129 -  let
   9.130 -    val (_, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
   9.131 -    val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code;
   9.132 -    val ml_code = if is_first then ml_code
   9.133 -      else "";
   9.134 -    val all_struct_name = Long_Name.append struct_name struct_code_name;
   9.135 -  in (ml_code, print_it all_struct_name tycos_map consts_map) end;
   9.136 -
   9.137 -in
   9.138 -
   9.139 -fun ml_code_antiq raw_const {struct_name, background} =
   9.140 -  let
   9.141 -    val const = Code.check_const (ProofContext.theory_of background) raw_const;
   9.142 -    val is_first = is_first_occ background;
   9.143 -    val background' = register_const const background;
   9.144 -  in (print_code struct_name is_first (print_const const), background') end;
   9.145 -
   9.146 -fun ml_code_datatype_antiq (raw_tyco, raw_constrs) {struct_name, background} =
   9.147 -  let
   9.148 -    val thy = ProofContext.theory_of background;
   9.149 -    val tyco = Sign.intern_type thy raw_tyco;
   9.150 -    val constrs = map (Code.check_const thy) raw_constrs;
   9.151 -    val constrs' = (map fst o snd o Code.get_datatype thy) tyco;
   9.152 -    val _ = if eq_set (op =) (constrs, constrs') then ()
   9.153 -      else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors")
   9.154 -    val is_first = is_first_occ background;
   9.155 -    val background' = register_datatype tyco constrs background;
   9.156 -  in (print_code struct_name is_first (print_datatype tyco constrs), background') end;
   9.157 -
   9.158 -end; (*local*)
   9.159 -
   9.160 -
   9.161  (** Isar setup **)
   9.162  
   9.163 -val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
   9.164 -val _ = ML_Context.add_antiq "code_datatype" (fn _ =>
   9.165 -  (Args.tyname --| Scan.lift (Args.$$$ "=")
   9.166 -    -- (Args.term ::: Scan.repeat (Scan.lift (Args.$$$ "|") |-- Args.term)))
   9.167 -      >> ml_code_datatype_antiq);
   9.168 -
   9.169  fun isar_seri_sml module_name =
   9.170    Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
   9.171    >> (fn with_signatures => serialize_ml target_SML
   9.172 @@ -1087,7 +963,6 @@
   9.173  val setup =
   9.174    Code_Target.add_target (target_SML, (isar_seri_sml, literals_sml))
   9.175    #> Code_Target.add_target (target_OCaml, (isar_seri_ocaml, literals_ocaml))
   9.176 -  #> Code_Target.extend_target (target_Eval, (target_SML, K I))
   9.177    #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   9.178        brackify_infix (1, R) fxy [
   9.179          print_typ (INFX (1, X)) ty1,
    10.1 --- a/src/Tools/Code_Generator.thy	Mon Dec 07 14:54:28 2009 +0100
    10.2 +++ b/src/Tools/Code_Generator.thy	Mon Dec 07 16:27:48 2009 +0100
    10.3 @@ -16,6 +16,7 @@
    10.4    "~~/src/Tools/Code/code_printer.ML"
    10.5    "~~/src/Tools/Code/code_target.ML"
    10.6    "~~/src/Tools/Code/code_ml.ML"
    10.7 +  "~~/src/Tools/Code/code_eval.ML"
    10.8    "~~/src/Tools/Code/code_haskell.ML"
    10.9    "~~/src/Tools/nbe.ML"
   10.10  begin
   10.11 @@ -23,6 +24,7 @@
   10.12  setup {*
   10.13    Code_Preproc.setup
   10.14    #> Code_ML.setup
   10.15 +  #> Code_Eval.setup
   10.16    #> Code_Haskell.setup
   10.17    #> Nbe.setup
   10.18  *}