author haftmann Fri Jan 27 22:27:03 2017 +0100 (2017-01-27) changeset 64959 9ca021bd718d parent 64958 85b87da722ab child 64960 8be78855ee7a
ML antiquotation for generated computations
 src/HOL/ROOT file | annotate | diff | revisions src/HOL/ex/Computations.thy file | annotate | diff | revisions src/Tools/Code/code_runtime.ML file | annotate | diff | revisions src/Tools/Code/code_target.ML file | annotate | diff | revisions
```     1.1 --- a/src/HOL/ROOT	Thu Jan 26 16:25:32 2017 +0100
1.2 +++ b/src/HOL/ROOT	Fri Jan 27 22:27:03 2017 +0100
1.3 @@ -536,6 +536,7 @@
1.4      "~~/src/HOL/Library/Refute"
1.5      "~~/src/HOL/Library/Transitive_Closure_Table"
1.6      Cartouche_Examples
1.7 +    Computations
1.8    theories
1.9      Commands
```
```     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/ex/Computations.thy	Fri Jan 27 22:27:03 2017 +0100
2.3 @@ -0,0 +1,63 @@
2.4 +(*  Title:      HOL/ex/Computations.thy
2.5 +    Author:     Florian Haftmann, TU Muenchen
2.6 +*)
2.7 +
2.8 +section \<open>Simple example for computations generated by the code generator\<close>
2.9 +
2.10 +theory Computations
2.11 +  imports Nat Fun_Def Num Code_Numeral
2.12 +begin
2.13 +
2.14 +fun even :: "nat \<Rightarrow> bool"
2.15 +  where "even 0 \<longleftrightarrow> True"
2.16 +      | "even (Suc 0) \<longleftrightarrow> False"
2.17 +      | "even (Suc (Suc n)) \<longleftrightarrow> even n"
2.18 +
2.19 +fun fib :: "nat \<Rightarrow> nat"
2.20 +  where "fib 0 = 0"
2.21 +      | "fib (Suc 0) = Suc 0"
2.22 +      | "fib (Suc (Suc n)) = fib (Suc n) + fib n"
2.23 +
2.24 +declare [[ML_source_trace]]
2.25 +
2.26 +ML \<open>
2.27 +local
2.28 +
2.29 +fun int_of_nat @{code "0 :: nat"} = 0
2.30 +  | int_of_nat (@{code Suc} n) = int_of_nat n + 1;
2.31 +
2.32 +in
2.33 +
2.34 +val comp_nat = @{computation "0 :: nat" Suc
2.35 +  "plus :: nat \<Rightarrow>_" "times :: nat \<Rightarrow> _" fib :: nat}
2.36 +  (fn post => post o HOLogic.mk_nat o int_of_nat);
2.37 +
2.38 +val comp_numeral = @{computation "0 :: nat" "1 :: nat" "2 :: nat" "3 :: nat" :: nat}
2.39 +  (fn post => post o HOLogic.mk_nat o int_of_nat);
2.40 +
2.41 +val comp_bool = @{computation True False HOL.conj HOL.disj HOL.implies
2.42 +  HOL.iff even "less_eq :: nat \<Rightarrow> _" "less :: nat \<Rightarrow> _" "HOL.eq :: nat \<Rightarrow> _" :: bool }
2.43 +  (K I)
2.44 +
2.45 +end
2.46 +\<close>
2.47 +
2.48 +declare [[ML_source_trace = false]]
2.49 +
2.50 +ML_val \<open>
2.51 +  comp_nat @{context} @{term "fib (Suc (Suc (Suc 0)) * Suc (Suc (Suc 0))) + Suc 0"}
2.52 +  |> Syntax.string_of_term @{context}
2.53 +  |> writeln
2.54 +\<close>
2.55 +
2.56 +ML_val \<open>
2.57 +  comp_bool @{context} @{term "fib (Suc (Suc (Suc 0)) * Suc (Suc (Suc 0))) + Suc 0 < fib (Suc (Suc 0))"}
2.58 +\<close>
2.59 +
2.60 +ML_val \<open>
2.61 +  comp_numeral @{context} @{term "Suc 42 + 7"}
2.62 +  |> Syntax.string_of_term @{context}
2.63 +  |> writeln
2.64 +\<close>
2.65 +
2.66 +end
```
```     3.1 --- a/src/Tools/Code/code_runtime.ML	Thu Jan 26 16:25:32 2017 +0100
3.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Jan 27 22:27:03 2017 +0100
3.3 @@ -28,10 +28,8 @@
3.4      -> Proof.context -> term -> 'a Exn.result
3.5    val dynamic_holds_conv: Proof.context -> conv
3.6    val static_holds_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv
3.7 -  val experimental_computation: (term -> 'a) cookie
3.8 -    -> { ctxt: Proof.context, lift_postproc: (term -> term) -> 'a -> 'a,
3.9 -           terms: term list, T: typ }
3.10 -    -> Proof.context -> term -> 'a (*EXPERIMENTAL!*)
3.11 +  val mount_computation: Proof.context -> (string * typ) list -> typ
3.12 +    -> (term -> 'b) -> ((term -> term) -> 'b -> 'a) -> Proof.context -> term -> 'a
3.13    val code_reflect: (string * string list option) list -> string list -> string
3.14      -> string option -> theory -> theory
3.15    datatype truth = Holds
3.16 @@ -49,9 +47,9 @@
3.17
3.18  (* technical prerequisites *)
3.19
3.20 -val this = "Code_Runtime";
3.21 -val s_truth = Long_Name.append this "truth";
3.22 -val s_Holds = Long_Name.append this "Holds";
3.23 +val thisN = "Code_Runtime";
3.24 +val truthN = Long_Name.append thisN "truth";
3.25 +val HoldsN = Long_Name.append thisN "Holds";
3.26
3.27  val target = "Eval";
3.28
3.29 @@ -60,10 +58,10 @@
3.30  val _ = Theory.setup
3.32    #> Code_Target.set_printings (Type_Constructor (@{type_name prop},
3.33 -    [(target, SOME (0, (K o K o K) (Code_Printer.str s_truth)))]))
3.34 +    [(target, SOME (0, (K o K o K) (Code_Printer.str truthN)))]))
3.35    #> Code_Target.set_printings (Constant (@{const_name Code_Generator.holds},
3.36 -    [(target, SOME (Code_Printer.plain_const_syntax s_Holds))]))
3.37 -  #> Code_Target.add_reserved target this
3.38 +    [(target, SOME (Code_Printer.plain_const_syntax HoldsN))]))
3.39 +  #> Code_Target.add_reserved target thisN
3.40    #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]);
3.41         (*avoid further pervasive infix names*)
3.42
3.43 @@ -153,7 +151,7 @@
3.44    fun init _ = empty;
3.45  );
3.46  val put_truth = Truth_Result.put;
3.47 -val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth");
3.48 +val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append thisN "put_truth");
3.49
3.50  local
3.51
3.52 @@ -231,6 +229,8 @@
3.53
3.54  in
3.55
3.56 +val covered_constsN = "covered_consts";
3.57 +
3.58  fun of_term_for_typ Ts =
3.59    let
3.60      val names = Ts
3.61 @@ -277,6 +277,8 @@
3.62
3.63  (* code generation for of the universal morphism *)
3.64
3.65 +val print_const = ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_typ;
3.66 +
3.67  fun print_of_term_funs { typ_sign_for, eval_for_const, of_term_for_typ } Ts =
3.68    let
3.69      val var_names = map_range (fn n => "t" ^ string_of_int (n + 1));
3.70 @@ -305,42 +307,47 @@
3.71      |> prefix "fun "
3.72    end;
3.73
3.74 -fun print_computation_code ctxt compiled_value requested_Ts cTs =
3.75 -  let
3.76 -    val proper_cTs = map_filter I cTs;
3.77 -    val typ_sign_for = typ_signatures proper_cTs;
3.78 -    fun add_typ T Ts =
3.79 -      if member (op =) Ts T
3.80 -      then Ts
3.81 -      else Ts
3.82 -        |> cons T
3.83 -        |> fold (fold add_typ o snd) (typ_sign_for T);
3.84 -    val required_Ts = fold add_typ requested_Ts [];
3.85 -    val of_term_for_typ' = of_term_for_typ required_Ts;
3.86 -    val eval_for_const' = eval_for_const ctxt proper_cTs;
3.87 -    val eval_for_const'' = the_default "_" o Option.map eval_for_const';
3.88 -    val eval_tuple = enclose "(" ")" (commas (map eval_for_const' proper_cTs));
3.89 -    fun mk_abs s = "fn " ^ s ^ " => ";
3.90 -    val eval_abs = space_implode ""
3.91 -      (map (mk_abs o eval_for_const'') cTs);
3.92 -    val of_term_code = print_of_term_funs {
3.93 -      typ_sign_for = typ_sign_for,
3.94 -      eval_for_const = eval_for_const',
3.95 -      of_term_for_typ = of_term_for_typ' } required_Ts;
3.96 -  in
3.97 -    (cat_lines [
3.98 -      "structure " ^ generated_computationN ^ " =",
3.99 -      "struct",
3.100 -      "",
3.101 -      "val " ^ eval_tuple ^ " = " ^ compiled_value ^ " ()",
3.102 -      "  (" ^ eval_abs,
3.103 -      "    " ^ eval_tuple ^ ");",
3.104 -      "",
3.105 -      of_term_code,
3.106 -      "",
3.107 -      "end"
3.108 -    ], map (prefix (generated_computationN ^ ".") o of_term_for_typ') requested_Ts)
3.109 -  end;
3.110 +fun print_computation_code ctxt compiled_value [] requested_Ts = ("", [])
3.111 +  | print_computation_code ctxt compiled_value cTs requested_Ts =
3.112 +      let
3.113 +        val proper_cTs = map_filter I cTs;
3.114 +        val typ_sign_for = typ_signatures proper_cTs;
3.115 +        fun add_typ T Ts =
3.116 +          if member (op =) Ts T
3.117 +          then Ts
3.118 +          else Ts
3.119 +            |> cons T
3.120 +            |> fold (fold add_typ o snd) (typ_sign_for T);
3.121 +        val required_Ts = fold add_typ requested_Ts [];
3.122 +        val of_term_for_typ' = of_term_for_typ required_Ts;
3.123 +        val eval_for_const' = eval_for_const ctxt proper_cTs;
3.124 +        val eval_for_const'' = the_default "_" o Option.map eval_for_const';
3.125 +        val eval_tuple = enclose "(" ")" (commas (map eval_for_const' proper_cTs));
3.126 +        fun mk_abs s = "fn " ^ s ^ " => ";
3.127 +        val eval_abs = space_implode ""
3.128 +          (map (mk_abs o eval_for_const'') cTs);
3.129 +        val of_term_code = print_of_term_funs {
3.130 +          typ_sign_for = typ_sign_for,
3.131 +          eval_for_const = eval_for_const',
3.132 +          of_term_for_typ = of_term_for_typ' } required_Ts;
3.133 +        val of_term_names = map (Long_Name.append generated_computationN
3.134 +          o of_term_for_typ') requested_Ts;
3.135 +      in
3.136 +        cat_lines [
3.137 +          "structure " ^ generated_computationN ^ " =",
3.138 +          "struct",
3.139 +          "",
3.140 +          "val " ^ covered_constsN ^ " = " ^ ML_Syntax.print_list print_const proper_cTs ^ ";",
3.141 +          "",
3.142 +          "val " ^ eval_tuple ^ " = " ^ compiled_value ^ " ()",
3.143 +          "  (" ^ eval_abs,
3.144 +          "    " ^ eval_tuple ^ ");",
3.145 +          "",
3.146 +          of_term_code,
3.147 +          "",
3.148 +          "end"
3.149 +        ] |> rpair of_term_names
3.150 +      end;
3.151
3.152  fun mount_computation ctxt cTs T raw_computation lift_postproc =
3.153    Code_Preproc.static_value { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] }
3.154 @@ -350,48 +357,12 @@
3.155        #> check_computation_input ctxt' cTs
3.156        #> raw_computation);
3.157
3.158 -fun compile_computation cookie ctxt T program evals vs_ty_evals deps =
3.159 -  let
3.160 -    fun the_const (Const cT) = cT
3.161 -      | the_const t = error ("No constant after preprocessing: " ^ Syntax.string_of_term ctxt t)
3.162 -    val raw_cTs = case evals of
3.163 -        Abs (_, _, t) => (map the_const o snd o strip_comb) t
3.164 -      | _ => error ("Bad term after preprocessing: " ^ Syntax.string_of_term ctxt evals);
3.165 -    val cTs = fold_rev (fn cT => fn cTs =>
3.166 -      (if member (op =) cTs (SOME cT) then NONE else SOME cT) :: cTs) raw_cTs [];
3.167 -    fun comp' vs_ty_evals =
3.168 -      let
3.169 -        val (generated_code, compiled_value) =
3.170 -          build_compilation_text ctxt NONE program deps vs_ty_evals;
3.171 -        val (of_term_code, [of_term]) = print_computation_code ctxt compiled_value [T] cTs;
3.172 -      in
3.173 -        (generated_code ^ "\n" ^ of_term_code,
3.174 -          enclose "(" ")" ("fn () => " ^ of_term))
3.175 -      end;
3.176 -    val compiled_computation =
3.177 -      Exn.release (run_compilation_text cookie ctxt comp' vs_ty_evals []);
3.178 -  in (map_filter I cTs, compiled_computation) end;
3.179 +
3.180 +(** variants of universal runtime code generation **)
3.181
3.182 -fun experimental_computation cookie { ctxt, lift_postproc, terms = ts, T } =
3.183 -  let
3.184 -    val _ = if not (monomorphic T)
3.185 -      then error ("Polymorphic type: " ^ Syntax.string_of_typ ctxt T)
3.186 -      else ();
3.187 -    val cTs = (fold o fold_aterms)
3.188 -      (fn (t as Const (cT as (_, T))) =>
3.189 -        if not (monomorphic T) then error ("Polymorphic constant:" ^ Syntax.string_of_term ctxt t)
3.190 -        else insert (op =) cT | _ => I) ts [];
3.191 -    val evals = Abs ("eval", map snd cTs ---> TFree (Name.aT, []), list_comb (Bound 0, map Const cTs));
3.192 -    val (cTs, raw_computation) = Code_Thingol.dynamic_value ctxt
3.193 -      (K I) (compile_computation cookie ctxt T) evals;
3.194 -  in
3.195 -    mount_computation ctxt cTs T raw_computation lift_postproc
3.196 -  end;
3.197 +(*FIXME consolidate variants*)
3.198
3.199 -
3.200 -(** code antiquotation **)
3.201 -
3.202 -fun runtime_code ctxt module_name program tycos consts =
3.203 +fun runtime_code'' ctxt module_name program tycos consts =
3.204    let
3.205      val thy = Proof_Context.theory_of ctxt;
3.206      val (ml_modules, target_names) =
3.207 @@ -411,63 +382,159 @@
3.208          | SOME tyco' => (tyco, tyco')) tycos tycos';
3.209    in (ml_code, (tycos_map, consts_map)) end;
3.210
3.211 +fun runtime_code' ctxt some_module_name named_tycos named_consts computation_Ts program evals vs_ty_evals deps =
3.212 +  let
3.213 +    val thy = Proof_Context.theory_of ctxt;
3.214 +    fun the_const (Const cT) = cT
3.215 +      | the_const t = error ("No constant after preprocessing: " ^ Syntax.string_of_term ctxt t)
3.216 +    val raw_computation_cTs = case evals of
3.217 +        Abs (_, _, t) => (map the_const o snd o strip_comb) t
3.218 +      | _ => error ("Bad term after preprocessing: " ^ Syntax.string_of_term ctxt evals);
3.219 +    val computation_cTs = fold_rev (fn cT => fn cTs =>
3.220 +      (if member (op =) cTs (SOME cT) then NONE else SOME cT) :: cTs) raw_computation_cTs [];
3.221 +    val consts' = fold (fn NONE => I | SOME (c, _) => insert (op =) c)
3.222 +      computation_cTs named_consts;
3.223 +    val program' = Code_Thingol.consts_program ctxt consts';
3.224 +      (*FIXME insufficient interfaces require double invocation of code generator*)
3.225 +    val ((ml_modules, compiled_value), deresolve) =
3.226 +      Code_Target.compilation_text' ctxt target some_module_name program'
3.227 +        (map Code_Symbol.Type_Constructor named_tycos @ map Code_Symbol.Constant consts' @ deps) true vs_ty_evals;
3.228 +        (*FIXME constrain signature*)
3.229 +    fun deresolve_const c = case (deresolve o Code_Symbol.Constant) c of
3.230 +          NONE => error ("Constant " ^ (quote o Code.string_of_const thy) c ^
3.231 +            "\nhas a user-defined serialization")
3.232 +        | SOME c' => c';
3.233 +    fun deresolve_tyco tyco = case (deresolve o Code_Symbol.Type_Constructor) tyco of
3.234 +          NONE => error ("Type " ^ quote (Proof_Context.markup_type ctxt tyco) ^
3.235 +            "\nhas a user-defined serialization")
3.236 +        | SOME c' => c';
3.237 +    val tyco_names =  map deresolve_const named_tycos;
3.238 +    val const_names = map deresolve_const named_consts;
3.239 +    val generated_code = space_implode "\n\n" (map snd ml_modules);
3.240 +    val (of_term_code, of_term_names) =
3.241 +      print_computation_code ctxt compiled_value computation_cTs computation_Ts;
3.242 +    val compiled_computation = generated_code ^ "\n" ^ of_term_code;
3.243 +  in
3.244 +    compiled_computation
3.245 +    |> rpair { tyco_map = named_tycos ~~ tyco_names,
3.246 +      const_map = named_consts ~~ const_names,
3.247 +      of_term_map = computation_Ts ~~ of_term_names }
3.248 +  end;
3.249 +
3.250 +fun funs_of_maps { tyco_map, const_map, of_term_map } =
3.251 +  { name_for_tyco = the o AList.lookup (op =) tyco_map,
3.252 +    name_for_const = the o AList.lookup (op =) const_map,
3.253 +    of_term_for_typ = the o AList.lookup (op =) of_term_map };
3.254 +
3.255 +fun runtime_code ctxt some_module_name named_tycos named_consts computation_Ts program evals vs_ty_evals deps =
3.256 +  runtime_code' ctxt some_module_name named_tycos named_consts computation_Ts program evals vs_ty_evals deps
3.257 +  ||> funs_of_maps;
3.258 +
3.259 +
3.260 +(** code and computation antiquotations **)
3.261 +
3.262 +val mount_computationN = Long_Name.append thisN "mount_computation";
3.263 +
3.264  local
3.265
3.266  structure Code_Antiq_Data = Proof_Data
3.267  (
3.268    type T = { named_consts: string list,
3.269 -    first_occurrence: bool,
3.270 -    generated_code: {
3.271 -      code: string,
3.272 -      name_for_const: string -> string
3.273 -    } lazy
3.274 +    computation_Ts: typ list, computation_cTs: (string * typ) list,
3.275 +    position_index: int,
3.276 +    generated_code: (string * {
3.277 +      name_for_tyco: string -> string,
3.278 +      name_for_const: string -> string,
3.279 +      of_term_for_typ: typ -> string
3.280 +    }) lazy
3.281    };
3.282    val empty: T = { named_consts = [],
3.283 -    first_occurrence = true,
3.284 -    generated_code = Lazy.value {
3.285 -      code = "",
3.286 -      name_for_const = I
3.287 -    }
3.288 +    computation_Ts = [], computation_cTs = [],
3.289 +    position_index = 0,
3.290 +    generated_code = Lazy.lazy (fn () => raise Fail "empty")
3.291    };
3.292    fun init _ = empty;
3.293  );
3.294
3.295 -val is_first_occurrence = #first_occurrence o Code_Antiq_Data.get;
3.296 +val current_position_index = #position_index o Code_Antiq_Data.get;
3.297
3.298 -fun lazy_code ctxt consts = Lazy.lazy (fn () =>
3.299 +fun register { named_consts, computation_Ts, computation_cTs } ctxt =
3.300    let
3.301 -    val program = Code_Thingol.consts_program ctxt consts;
3.302 -    val (code, (_, consts_map)) =
3.303 -      runtime_code ctxt Code_Target.generatedN program [] consts
3.304 -  in { code = code, name_for_const = the o AList.lookup (op =) consts_map } end);
3.305 -
3.306 -fun register_const const ctxt =
3.307 -  let
3.308 -    val consts = insert (op =) const ((#named_consts o Code_Antiq_Data.get) ctxt);
3.309 +    val data = Code_Antiq_Data.get ctxt;
3.310 +    val named_consts' = union (op =) named_consts (#named_consts data);
3.311 +    val computation_Ts' = union (op =) computation_Ts (#computation_Ts data);
3.312 +    val computation_cTs' = union (op =) computation_cTs (#computation_cTs data);
3.313 +    val position_index' = #position_index data + 1;
3.314 +    fun generated_code' () =
3.315 +      let
3.316 +        val evals = Abs ("eval", map snd computation_cTs' --->
3.317 +          TFree (Name.aT, []), list_comb (Bound 0, map Const computation_cTs'));
3.318 +      in Code_Thingol.dynamic_value ctxt
3.319 +        (K I) (runtime_code ctxt NONE [] named_consts' computation_Ts') evals
3.320 +      end;
3.321    in
3.322      ctxt
3.323      |> Code_Antiq_Data.put {
3.324 -        named_consts = consts,
3.325 -        first_occurrence = false,
3.326 -        generated_code = lazy_code ctxt consts
3.327 +        named_consts = named_consts',
3.328 +        computation_Ts = computation_Ts',
3.329 +        computation_cTs = computation_cTs',
3.330 +        position_index = position_index',
3.331 +        generated_code = Lazy.lazy generated_code'
3.332        }
3.333    end;
3.334
3.335 -fun print_code is_first_occ const ctxt =
3.336 +fun register_const const =
3.337 +  register { named_consts = [const],
3.338 +    computation_Ts = [],
3.339 +    computation_cTs = [] };
3.340 +
3.341 +fun register_computation cTs T =
3.342 +  register { named_consts = [],
3.343 +    computation_Ts = [T],
3.344 +    computation_cTs = cTs };
3.345 +
3.346 +fun print body_code_for ctxt ctxt' =
3.347    let
3.348 -    val { code, name_for_const } = (Lazy.force o #generated_code o Code_Antiq_Data.get) ctxt;
3.349 -    val context_code = if is_first_occ then code else "";
3.350 -    val body_code = ML_Context.struct_name ctxt ^ "." ^ name_for_const const;
3.351 +    val position_index = current_position_index ctxt;
3.352 +    val (code, name_ofs) = (Lazy.force o #generated_code o Code_Antiq_Data.get) ctxt';
3.353 +    val context_code = if position_index = 0 then code else "";
3.354 +    val body_code = body_code_for name_ofs (ML_Context.struct_name ctxt') position_index;
3.355    in (context_code, body_code) end;
3.356
3.357 +fun print_code ctxt const =
3.358 +  print (fn { name_for_const, ... } => fn prfx => fn _ =>
3.359 +    Long_Name.append prfx (name_for_const const)) ctxt;
3.360 +
3.361 +fun print_computation ctxt T =
3.362 +  print (fn { of_term_for_typ, ... } => fn prfx => fn _ =>
3.363 +    space_implode " " [
3.364 +      mount_computationN,
3.365 +      "(Context.proof_of (Context.the_generic_context ()))",
3.366 +      Long_Name.implode [prfx, generated_computationN, covered_constsN],
3.367 +      (ML_Syntax.atomic o ML_Syntax.print_typ) T,
3.368 +      Long_Name.append prfx (of_term_for_typ T)
3.369 +    ]) ctxt;
3.370 +
3.371  in
3.372
3.373  fun ml_code_antiq raw_const ctxt =
3.374    let
3.375      val thy = Proof_Context.theory_of ctxt;
3.376      val const = Code.check_const thy raw_const;
3.377 -    val is_first = is_first_occurrence ctxt;
3.378 -  in (print_code is_first const, register_const const ctxt) end;
3.379 +  in (print_code ctxt const, register_const const ctxt) end;
3.380 +
3.381 +fun ml_computation_antiq (raw_ts, raw_T) ctxt =
3.382 +  let
3.383 +    val ts = map (Syntax.check_term ctxt) raw_ts;
3.384 +    val T = Syntax.check_typ ctxt raw_T;
3.385 +    val _ = if not (monomorphic T)
3.386 +      then error ("Polymorphic type: " ^ Syntax.string_of_typ ctxt T)
3.387 +      else ();
3.388 +    val cTs = (fold o fold_aterms)
3.389 +      (fn (t as Const (cT as (_, T))) =>
3.390 +        if not (monomorphic T) then error ("Polymorphic constant: " ^ Syntax.string_of_term ctxt t)
3.391 +        else insert (op =) cT | _ => I) ts [];
3.392 +  in (print_computation ctxt T, register_computation cTs T ctxt) end;
3.393
3.394  end; (*local*)
3.395
3.396 @@ -548,7 +615,7 @@
3.397      val functions = map (prep_const thy) raw_functions;
3.398      val consts = constrs @ functions;
3.399      val program = Code_Thingol.consts_program ctxt consts;
3.400 -    val result = runtime_code ctxt module_name program tycos consts
3.401 +    val result = runtime_code'' ctxt module_name program tycos consts
3.402        |> (apsnd o apsnd) (chop (length constrs));
3.403    in
3.404      thy
3.405 @@ -562,7 +629,12 @@
3.406  (** Isar setup **)
3.407
3.408  val _ =
3.409 -  Theory.setup (ML_Antiquotation.declaration @{binding code} Args.term (fn _ => ml_code_antiq));
3.410 +  Theory.setup (ML_Antiquotation.declaration @{binding code}
3.411 +    Args.term (fn _ => ml_code_antiq));
3.412 +
3.413 +val _ =
3.414 +  Theory.setup (ML_Antiquotation.declaration @{binding computation}
3.415 +    (Scan.repeat Args.term --| Scan.lift (Args.\$\$\$ "::") -- Args.typ) (fn _ => ml_computation_antiq));
3.416
3.417  local
3.418
```
```     4.1 --- a/src/Tools/Code/code_target.ML	Thu Jan 26 16:25:32 2017 +0100
4.2 +++ b/src/Tools/Code/code_target.ML	Fri Jan 27 22:27:03 2017 +0100
4.3 @@ -31,6 +31,9 @@
4.4    val compilation_text: Proof.context -> string -> Code_Thingol.program
4.5      -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
4.6      -> (string * string) list * string
4.7 +  val compilation_text': Proof.context -> string -> string option -> Code_Thingol.program
4.8 +    -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
4.9 +    -> ((string * string) list * string) * (Code_Symbol.T -> string option)
4.10
4.11    type serializer
4.12    type literals = Code_Printer.literals
4.13 @@ -414,17 +417,20 @@
4.14      val (program_code, deresolve) =
4.15        produce (mounted_serializer program (if all_public then [] else [Code_Symbol.value]));
4.16      val value_name = the (deresolve Code_Symbol.value);
4.17 -  in (program_code, value_name) end;
4.18 +  in ((program_code, value_name), deresolve) end;
4.19
4.20 -fun compilation_text ctxt target_name program syms =
4.21 +fun compilation_text' ctxt target_name some_module_name program syms =
4.22    let
4.23      val (mounted_serializer, (_, prepared_program)) =
4.24 -      mount_serializer ctxt target_name NONE generatedN [] program syms;
4.25 +      mount_serializer ctxt target_name NONE (the_default generatedN some_module_name) [] program syms;
4.26    in
4.27      Code_Preproc.timed_exec "serializing"
4.28      (fn () => dynamic_compilation_text mounted_serializer prepared_program syms) ctxt
4.29    end;
4.30
4.31 +fun compilation_text ctxt target_name program syms =
4.32 +  fst oo compilation_text' ctxt target_name NONE program syms
4.33 +
4.34  end; (* local *)
4.35
4.36
```