26 val static_value_exn: 'a cookie -> { ctxt: Proof.context, target: string option, |
26 val static_value_exn: 'a cookie -> { ctxt: Proof.context, target: string option, |
27 lift_postproc: (term -> term) -> 'a -> 'a, consts: string list } |
27 lift_postproc: (term -> term) -> 'a -> 'a, consts: string list } |
28 -> Proof.context -> term -> 'a Exn.result |
28 -> Proof.context -> term -> 'a Exn.result |
29 val dynamic_holds_conv: Proof.context -> conv |
29 val dynamic_holds_conv: Proof.context -> conv |
30 val static_holds_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv |
30 val static_holds_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv |
31 val experimental_computation: (Proof.context -> term -> 'a) cookie |
31 val experimental_computation: (term -> 'a) cookie |
32 -> { ctxt: Proof.context, lift_postproc: (term -> term) -> 'a -> 'a, |
32 -> { ctxt: Proof.context, lift_postproc: (term -> term) -> 'a -> 'a, |
33 terms: term list, T: typ } |
33 terms: term list, T: typ } |
34 -> Proof.context -> term -> 'a (*EXPERIMENTAL!*) |
34 -> Proof.context -> term -> 'a (*EXPERIMENTAL!*) |
35 val code_reflect: (string * string list option) list -> string list -> string |
35 val code_reflect: (string * string list option) list -> string list -> string |
36 -> string option -> theory -> theory |
36 -> string option -> theory -> theory |
194 end; (*local*) |
194 end; (*local*) |
195 |
195 |
196 |
196 |
197 (** computations -- experimental! **) |
197 (** computations -- experimental! **) |
198 |
198 |
|
199 fun monomorphic T = fold_atyps ((K o K) false) T true; |
|
200 |
199 fun typ_signatures_for T = |
201 fun typ_signatures_for T = |
200 let |
202 let |
201 val (Ts, T') = strip_type T; |
203 val (Ts, T') = strip_type T; |
202 in map_range (fn n => (drop n Ts ---> T', take n Ts)) (length Ts + 1) end; |
204 in map_range (fn n => (drop n Ts ---> T', take n Ts)) (length Ts + 1) end; |
203 |
205 |
215 fun print_of_term_funs { typ_sign_for, eval_for_const, of_term_for_typ } Ts = |
217 fun print_of_term_funs { typ_sign_for, eval_for_const, of_term_for_typ } Ts = |
216 let |
218 let |
217 val var_names = map_range (fn n => "t" ^ string_of_int (n + 1)); |
219 val var_names = map_range (fn n => "t" ^ string_of_int (n + 1)); |
218 fun print_lhs c xs = "Const (" ^ quote c ^ ", _)" |
220 fun print_lhs c xs = "Const (" ^ quote c ^ ", _)" |
219 |> fold (fn x => fn s => s ^ " $ " ^ x) xs |
221 |> fold (fn x => fn s => s ^ " $ " ^ x) xs |
220 |> enclose "(" ")" |
222 |> enclose "(" ")"; |
221 |> prefix "ctxt "; |
|
222 fun print_rhs c Ts T xs = eval_for_const (c, Ts ---> T) |
223 fun print_rhs c Ts T xs = eval_for_const (c, Ts ---> T) |
223 |> fold2 (fn T' => fn x => fn s => |
224 |> fold2 (fn T' => fn x => fn s => |
224 s ^ (" (" ^ of_term_for_typ T' ^ " ctxt " ^ x ^ ")")) Ts xs |
225 s ^ (" (" ^ of_term_for_typ T' ^ " " ^ x ^ ")")) Ts xs |
225 fun print_eq T (c, Ts) = |
226 fun print_eq T (c, Ts) = |
226 let |
227 let |
227 val xs = var_names (length Ts); |
228 val xs = var_names (length Ts); |
228 in print_lhs c xs ^ " = " ^ print_rhs c Ts T xs end; |
229 in print_lhs c xs ^ " = " ^ print_rhs c Ts T xs end; |
229 val err_eq = |
|
230 "ctxt t = error (" ^ quote "Bad term: " ^ " ^ Syntax.string_of_term ctxt t)"; |
|
231 fun print_eqs T = |
230 fun print_eqs T = |
232 let |
231 let |
233 val typ_signs = typ_sign_for T; |
232 val typ_signs = typ_sign_for T; |
234 val name = of_term_for_typ T; |
233 val name = of_term_for_typ T; |
235 in |
234 in |
236 (map (print_eq T) typ_signs @ [err_eq]) |
235 map (print_eq T) typ_signs |
237 |> map (prefix (name ^ " ")) |
236 |> map (prefix (name ^ " ")) |
238 |> space_implode "\n | " |
237 |> space_implode "\n | " |
239 end; |
238 end; |
240 in |
239 in |
241 map print_eqs Ts |
240 map print_eqs Ts |
304 "", |
303 "", |
305 "end" |
304 "end" |
306 ], map (prefix (generated_computationN ^ ".")) of_terms) |
305 ], map (prefix (generated_computationN ^ ".")) of_terms) |
307 end; |
306 end; |
308 |
307 |
|
308 fun check_typ ctxt T t = |
|
309 Syntax.check_term ctxt (Type.constraint T t); |
|
310 |
|
311 fun check_computation_input ctxt cTs t = |
|
312 let |
|
313 fun check t = check_comb (strip_comb t) |
|
314 and check_comb (t as Abs _, _) = |
|
315 error ("Bad term, contains abstraction: " ^ Syntax.string_of_term ctxt t) |
|
316 | check_comb (t as Const (cT as (c, T)), ts) = |
|
317 let |
|
318 val _ = if not (member (op =) cTs cT) |
|
319 then error ("Bad term, computation cannot proceed on constant " ^ Syntax.string_of_term ctxt t) |
|
320 else (); |
|
321 val _ = if not (monomorphic T) |
|
322 then error ("Bad term, contains polymorphic constant " ^ Syntax.string_of_term ctxt t) |
|
323 else (); |
|
324 val _ = map check ts; |
|
325 in () end; |
|
326 val _ = check t; |
|
327 in t end; |
|
328 |
309 fun compile_computation cookie ctxt T program evals vs_ty_evals deps = |
329 fun compile_computation cookie ctxt T program evals vs_ty_evals deps = |
310 let |
330 let |
311 val raw_cTs = case evals of |
331 val raw_cTs = case evals of |
312 Abs (_, _, t) => (snd o strip_comb) t |
332 Abs (_, _, t) => (snd o strip_comb) t |
313 | _ => error ("Bad term after preprocessing: " ^ Syntax.string_of_term ctxt evals); |
333 | _ => error ("Bad term after preprocessing: " ^ Syntax.string_of_term ctxt evals); |
323 enclose "(" ")" ("fn () => " ^ List.last of_terms)) |
343 enclose "(" ")" ("fn () => " ^ List.last of_terms)) |
324 end; |
344 end; |
325 val compiled_computation = |
345 val compiled_computation = |
326 Exn.release (run_computation_text cookie ctxt comp' vs_ty_evals []); |
346 Exn.release (run_computation_text cookie ctxt comp' vs_ty_evals []); |
327 in fn ctxt' => |
347 in fn ctxt' => |
328 compiled_computation ctxt' o reject_vars ctxt' o Syntax.check_term ctxt' o Type.constraint T |
348 check_typ ctxt' T |
|
349 #> reject_vars ctxt' |
|
350 #> check_computation_input ctxt cTs |
|
351 #> compiled_computation |
329 end; |
352 end; |
330 |
353 |
331 fun experimental_computation cookie { ctxt, lift_postproc, terms = ts, T } = |
354 fun experimental_computation cookie { ctxt, lift_postproc, terms = ts, T } = |
332 let |
355 let |
333 val cTs = (fold o fold_aterms) (fn Const cT => insert (op =) cT | _ => I) ts []; |
356 val cTs = (fold o fold_aterms) |
|
357 (fn (t as Const (cT as (_, T))) => |
|
358 if not (monomorphic T) then error ("Polymorphic constant:" ^ Syntax.string_of_term ctxt t) |
|
359 else insert (op =) cT | _ => I) ts []; |
334 val vT = TFree (singleton (Name.variant_list |
360 val vT = TFree (singleton (Name.variant_list |
335 (fold (fn (_, T) => fold_atyps (fn TFree (v, _) => insert (op =) v | _ => I) |
361 (fold (fn (_, T) => fold_atyps (fn TFree (v, _) => insert (op =) v | _ => I) |
336 T) cTs [])) Name.aT, []); |
362 T) cTs [])) Name.aT, []); |
337 val evals = Abs ("eval", map snd cTs ---> vT, list_comb (Bound 0, map Const cTs)); |
363 val evals = Abs ("eval", map snd cTs ---> vT, list_comb (Bound 0, map Const cTs)); |
338 val computation = Code_Thingol.dynamic_value ctxt |
364 val computation = Code_Thingol.dynamic_value ctxt |