ML antiquotation for generated computations
authorhaftmann
Fri Jan 27 22:27:03 2017 +0100 (2017-01-27)
changeset 649599ca021bd718d
parent 64958 85b87da722ab
child 64960 8be78855ee7a
ML antiquotation for generated computations
src/HOL/ROOT
src/HOL/ex/Computations.thy
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_target.ML
     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
    1.10      Adhoc_Overloading_Examples
     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.31    (Code_Target.add_derived_target (target, [(Code_ML.target_SML, I)])
    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