200 |
200 |
201 fun check_matches_type ctxt predname T ms = |
201 fun check_matches_type ctxt predname T ms = |
202 let |
202 let |
203 fun check (Fun (m1, m2)) (Type("fun", [T1,T2])) = check m1 T1 andalso check m2 T2 |
203 fun check (Fun (m1, m2)) (Type("fun", [T1,T2])) = check m1 T1 andalso check m2 T2 |
204 | check m (Type("fun", _)) = (m = Input orelse m = Output) |
204 | check m (Type("fun", _)) = (m = Input orelse m = Output) |
205 | check (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) = |
205 | check (Pair (m1, m2)) (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) = |
206 check m1 T1 andalso check m2 T2 |
206 check m1 T1 andalso check m2 T2 |
207 | check Input _ = true |
207 | check Input _ = true |
208 | check Output _ = true |
208 | check Output _ = true |
209 | check Bool @{typ bool} = true |
209 | check Bool \<^typ>\<open>bool\<close> = true |
210 | check _ _ = false |
210 | check _ _ = false |
211 fun check_consistent_modes ms = |
211 fun check_consistent_modes ms = |
212 if forall (fn Fun _ => true | _ => false) ms then |
212 if forall (fn Fun _ => true | _ => false) ms then |
213 apply2 check_consistent_modes (split_list (map (fn Fun (m1, m2) => (m1, m2)) ms)) |
213 apply2 check_consistent_modes (split_list (map (fn Fun (m1, m2) => (m1, m2)) ms)) |
214 |> (fn (res1, res2) => res1 andalso res2) |
214 |> (fn (res1, res2) => res1 andalso res2) |
304 compfuns = Predicate_Comp_Funs.compfuns, |
304 compfuns = Predicate_Comp_Funs.compfuns, |
305 mk_random = (fn _ => error "no random generation"), |
305 mk_random = (fn _ => error "no random generation"), |
306 additional_arguments = fn names => |
306 additional_arguments = fn names => |
307 let |
307 let |
308 val depth_name = singleton (Name.variant_list names) "depth" |
308 val depth_name = singleton (Name.variant_list names) "depth" |
309 in [Free (depth_name, @{typ natural})] end, |
309 in [Free (depth_name, \<^typ>\<open>natural\<close>)] end, |
310 modify_funT = (fn T => let val (Ts, U) = strip_type T |
310 modify_funT = (fn T => let val (Ts, U) = strip_type T |
311 val Ts' = [@{typ natural}] in (Ts @ Ts') ---> U end), |
311 val Ts' = [\<^typ>\<open>natural\<close>] in (Ts @ Ts') ---> U end), |
312 wrap_compilation = |
312 wrap_compilation = |
313 fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation => |
313 fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation => |
314 let |
314 let |
315 val [depth] = additional_arguments |
315 val [depth] = additional_arguments |
316 val (_, Ts) = split_modeT mode (binder_types T) |
316 val (_, Ts) = split_modeT mode (binder_types T) |
317 val T' = mk_monadT compfuns (HOLogic.mk_tupleT Ts) |
317 val T' = mk_monadT compfuns (HOLogic.mk_tupleT Ts) |
318 val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T') |
318 val if_const = Const (\<^const_name>\<open>If\<close>, \<^typ>\<open>bool\<close> --> T' --> T' --> T') |
319 in |
319 in |
320 if_const $ HOLogic.mk_eq (depth, @{term "0 :: natural"}) |
320 if_const $ HOLogic.mk_eq (depth, \<^term>\<open>0 :: natural\<close>) |
321 $ mk_empty compfuns (dest_monadT compfuns T') |
321 $ mk_empty compfuns (dest_monadT compfuns T') |
322 $ compilation |
322 $ compilation |
323 end, |
323 end, |
324 transform_additional_arguments = |
324 transform_additional_arguments = |
325 fn _ => fn additional_arguments => |
325 fn _ => fn additional_arguments => |
326 let |
326 let |
327 val [depth] = additional_arguments |
327 val [depth] = additional_arguments |
328 val depth' = |
328 val depth' = |
329 Const (@{const_name Groups.minus}, @{typ "natural => natural => natural"}) |
329 Const (\<^const_name>\<open>Groups.minus\<close>, \<^typ>\<open>natural => natural => natural\<close>) |
330 $ depth $ Const (@{const_name Groups.one}, @{typ "natural"}) |
330 $ depth $ Const (\<^const_name>\<open>Groups.one\<close>, \<^typ>\<open>natural\<close>) |
331 in [depth'] end |
331 in [depth'] end |
332 } |
332 } |
333 |
333 |
334 val random_comp_modifiers = Comp_Mod.Comp_Modifiers |
334 val random_comp_modifiers = Comp_Mod.Comp_Modifiers |
335 { |
335 { |
336 compilation = Random, |
336 compilation = Random, |
337 function_name_prefix = "random_", |
337 function_name_prefix = "random_", |
338 compfuns = Predicate_Comp_Funs.compfuns, |
338 compfuns = Predicate_Comp_Funs.compfuns, |
339 mk_random = (fn T => fn additional_arguments => |
339 mk_random = (fn T => fn additional_arguments => |
340 list_comb (Const(@{const_name Random_Pred.iter}, |
340 list_comb (Const(\<^const_name>\<open>Random_Pred.iter\<close>, |
341 [@{typ natural}, @{typ natural}, @{typ Random.seed}] ---> |
341 [\<^typ>\<open>natural\<close>, \<^typ>\<open>natural\<close>, \<^typ>\<open>Random.seed\<close>] ---> |
342 Predicate_Comp_Funs.mk_monadT T), additional_arguments)), |
342 Predicate_Comp_Funs.mk_monadT T), additional_arguments)), |
343 modify_funT = (fn T => |
343 modify_funT = (fn T => |
344 let |
344 let |
345 val (Ts, U) = strip_type T |
345 val (Ts, U) = strip_type T |
346 val Ts' = [@{typ natural}, @{typ natural}, @{typ Random.seed}] |
346 val Ts' = [\<^typ>\<open>natural\<close>, \<^typ>\<open>natural\<close>, \<^typ>\<open>Random.seed\<close>] |
347 in (Ts @ Ts') ---> U end), |
347 in (Ts @ Ts') ---> U end), |
348 additional_arguments = (fn names => |
348 additional_arguments = (fn names => |
349 let |
349 let |
350 val [nrandom, size, seed] = Name.variant_list names ["nrandom", "size", "seed"] |
350 val [nrandom, size, seed] = Name.variant_list names ["nrandom", "size", "seed"] |
351 in |
351 in |
352 [Free (nrandom, @{typ natural}), Free (size, @{typ natural}), |
352 [Free (nrandom, \<^typ>\<open>natural\<close>), Free (size, \<^typ>\<open>natural\<close>), |
353 Free (seed, @{typ Random.seed})] |
353 Free (seed, \<^typ>\<open>Random.seed\<close>)] |
354 end), |
354 end), |
355 wrap_compilation = K (K (K (K (K I)))) |
355 wrap_compilation = K (K (K (K (K I)))) |
356 : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), |
356 : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), |
357 transform_additional_arguments = K I : (indprem -> term list -> term list) |
357 transform_additional_arguments = K I : (indprem -> term list -> term list) |
358 } |
358 } |
361 { |
361 { |
362 compilation = Depth_Limited_Random, |
362 compilation = Depth_Limited_Random, |
363 function_name_prefix = "depth_limited_random_", |
363 function_name_prefix = "depth_limited_random_", |
364 compfuns = Predicate_Comp_Funs.compfuns, |
364 compfuns = Predicate_Comp_Funs.compfuns, |
365 mk_random = (fn T => fn additional_arguments => |
365 mk_random = (fn T => fn additional_arguments => |
366 list_comb (Const(@{const_name Random_Pred.iter}, |
366 list_comb (Const(\<^const_name>\<open>Random_Pred.iter\<close>, |
367 [@{typ natural}, @{typ natural}, @{typ Random.seed}] ---> |
367 [\<^typ>\<open>natural\<close>, \<^typ>\<open>natural\<close>, \<^typ>\<open>Random.seed\<close>] ---> |
368 Predicate_Comp_Funs.mk_monadT T), tl additional_arguments)), |
368 Predicate_Comp_Funs.mk_monadT T), tl additional_arguments)), |
369 modify_funT = (fn T => |
369 modify_funT = (fn T => |
370 let |
370 let |
371 val (Ts, U) = strip_type T |
371 val (Ts, U) = strip_type T |
372 val Ts' = [@{typ natural}, @{typ natural}, @{typ natural}, |
372 val Ts' = [\<^typ>\<open>natural\<close>, \<^typ>\<open>natural\<close>, \<^typ>\<open>natural\<close>, |
373 @{typ Random.seed}] |
373 \<^typ>\<open>Random.seed\<close>] |
374 in (Ts @ Ts') ---> U end), |
374 in (Ts @ Ts') ---> U end), |
375 additional_arguments = (fn names => |
375 additional_arguments = (fn names => |
376 let |
376 let |
377 val [depth, nrandom, size, seed] = Name.variant_list names ["depth", "nrandom", "size", "seed"] |
377 val [depth, nrandom, size, seed] = Name.variant_list names ["depth", "nrandom", "size", "seed"] |
378 in |
378 in |
379 [Free (depth, @{typ natural}), Free (nrandom, @{typ natural}), |
379 [Free (depth, \<^typ>\<open>natural\<close>), Free (nrandom, \<^typ>\<open>natural\<close>), |
380 Free (size, @{typ natural}), Free (seed, @{typ Random.seed})] |
380 Free (size, \<^typ>\<open>natural\<close>), Free (seed, \<^typ>\<open>Random.seed\<close>)] |
381 end), |
381 end), |
382 wrap_compilation = |
382 wrap_compilation = |
383 fn compfuns => fn _ => fn T => fn mode => fn additional_arguments => fn compilation => |
383 fn compfuns => fn _ => fn T => fn mode => fn additional_arguments => fn compilation => |
384 let |
384 let |
385 val depth = hd (additional_arguments) |
385 val depth = hd (additional_arguments) |
386 val (_, Ts) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) |
386 val (_, Ts) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) |
387 mode (binder_types T) |
387 mode (binder_types T) |
388 val T' = mk_monadT compfuns (HOLogic.mk_tupleT Ts) |
388 val T' = mk_monadT compfuns (HOLogic.mk_tupleT Ts) |
389 val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T') |
389 val if_const = Const (\<^const_name>\<open>If\<close>, \<^typ>\<open>bool\<close> --> T' --> T' --> T') |
390 in |
390 in |
391 if_const $ HOLogic.mk_eq (depth, @{term "0 :: natural"}) |
391 if_const $ HOLogic.mk_eq (depth, \<^term>\<open>0 :: natural\<close>) |
392 $ mk_empty compfuns (dest_monadT compfuns T') |
392 $ mk_empty compfuns (dest_monadT compfuns T') |
393 $ compilation |
393 $ compilation |
394 end, |
394 end, |
395 transform_additional_arguments = |
395 transform_additional_arguments = |
396 fn _ => fn additional_arguments => |
396 fn _ => fn additional_arguments => |
397 let |
397 let |
398 val [depth, nrandom, size, seed] = additional_arguments |
398 val [depth, nrandom, size, seed] = additional_arguments |
399 val depth' = |
399 val depth' = |
400 Const (@{const_name Groups.minus}, @{typ "natural => natural => natural"}) |
400 Const (\<^const_name>\<open>Groups.minus\<close>, \<^typ>\<open>natural => natural => natural\<close>) |
401 $ depth $ Const (@{const_name Groups.one}, @{typ "natural"}) |
401 $ depth $ Const (\<^const_name>\<open>Groups.one\<close>, \<^typ>\<open>natural\<close>) |
402 in [depth', nrandom, size, seed] end |
402 in [depth', nrandom, size, seed] end |
403 } |
403 } |
404 |
404 |
405 val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers |
405 val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers |
406 { |
406 { |
433 compilation = Pos_Random_DSeq, |
433 compilation = Pos_Random_DSeq, |
434 function_name_prefix = "random_dseq_", |
434 function_name_prefix = "random_dseq_", |
435 compfuns = Random_Sequence_CompFuns.compfuns, |
435 compfuns = Random_Sequence_CompFuns.compfuns, |
436 mk_random = (fn T => fn _ => |
436 mk_random = (fn T => fn _ => |
437 let |
437 let |
438 val random = Const (@{const_name Quickcheck_Random.random}, |
438 val random = Const (\<^const_name>\<open>Quickcheck_Random.random\<close>, |
439 @{typ natural} --> @{typ Random.seed} --> |
439 \<^typ>\<open>natural\<close> --> \<^typ>\<open>Random.seed\<close> --> |
440 HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) |
440 HOLogic.mk_prodT (HOLogic.mk_prodT (T, \<^typ>\<open>unit => term\<close>), \<^typ>\<open>Random.seed\<close>)) |
441 in |
441 in |
442 Const (@{const_name Random_Sequence.Random}, (@{typ natural} --> @{typ Random.seed} --> |
442 Const (\<^const_name>\<open>Random_Sequence.Random\<close>, (\<^typ>\<open>natural\<close> --> \<^typ>\<open>Random.seed\<close> --> |
443 HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) --> |
443 HOLogic.mk_prodT (HOLogic.mk_prodT (T, \<^typ>\<open>unit => term\<close>), \<^typ>\<open>Random.seed\<close>)) --> |
444 Random_Sequence_CompFuns.mk_random_dseqT T) $ random |
444 Random_Sequence_CompFuns.mk_random_dseqT T) $ random |
445 end), |
445 end), |
446 |
446 |
447 modify_funT = I, |
447 modify_funT = I, |
448 additional_arguments = K [], |
448 additional_arguments = K [], |
470 compilation = New_Pos_Random_DSeq, |
470 compilation = New_Pos_Random_DSeq, |
471 function_name_prefix = "new_random_dseq_", |
471 function_name_prefix = "new_random_dseq_", |
472 compfuns = New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns, |
472 compfuns = New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns, |
473 mk_random = (fn T => fn _ => |
473 mk_random = (fn T => fn _ => |
474 let |
474 let |
475 val random = Const (@{const_name Quickcheck_Random.random}, |
475 val random = Const (\<^const_name>\<open>Quickcheck_Random.random\<close>, |
476 @{typ natural} --> @{typ Random.seed} --> |
476 \<^typ>\<open>natural\<close> --> \<^typ>\<open>Random.seed\<close> --> |
477 HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) |
477 HOLogic.mk_prodT (HOLogic.mk_prodT (T, \<^typ>\<open>unit => term\<close>), \<^typ>\<open>Random.seed\<close>)) |
478 in |
478 in |
479 Const (@{const_name Random_Sequence.pos_Random}, (@{typ natural} --> @{typ Random.seed} --> |
479 Const (\<^const_name>\<open>Random_Sequence.pos_Random\<close>, (\<^typ>\<open>natural\<close> --> \<^typ>\<open>Random.seed\<close> --> |
480 HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) --> |
480 HOLogic.mk_prodT (HOLogic.mk_prodT (T, \<^typ>\<open>unit => term\<close>), \<^typ>\<open>Random.seed\<close>)) --> |
481 New_Pos_Random_Sequence_CompFuns.mk_pos_random_dseqT T) $ random |
481 New_Pos_Random_Sequence_CompFuns.mk_pos_random_dseqT T) $ random |
482 end), |
482 end), |
483 modify_funT = I, |
483 modify_funT = I, |
484 additional_arguments = K [], |
484 additional_arguments = K [], |
485 wrap_compilation = K (K (K (K (K I)))) |
485 wrap_compilation = K (K (K (K (K I)))) |
505 compilation = Pos_Generator_DSeq, |
505 compilation = Pos_Generator_DSeq, |
506 function_name_prefix = "generator_dseq_", |
506 function_name_prefix = "generator_dseq_", |
507 compfuns = New_Pos_DSequence_CompFuns.depth_limited_compfuns, |
507 compfuns = New_Pos_DSequence_CompFuns.depth_limited_compfuns, |
508 mk_random = |
508 mk_random = |
509 (fn T => fn _ => |
509 (fn T => fn _ => |
510 Const (@{const_name "Lazy_Sequence.small_lazy_class.small_lazy"}, |
510 Const (\<^const_name>\<open>Lazy_Sequence.small_lazy_class.small_lazy\<close>, |
511 @{typ "natural"} --> Type (@{type_name "Lazy_Sequence.lazy_sequence"}, [T]))), |
511 \<^typ>\<open>natural\<close> --> Type (\<^type_name>\<open>Lazy_Sequence.lazy_sequence\<close>, [T]))), |
512 modify_funT = I, |
512 modify_funT = I, |
513 additional_arguments = K [], |
513 additional_arguments = K [], |
514 wrap_compilation = K (K (K (K (K I)))) |
514 wrap_compilation = K (K (K (K (K I)))) |
515 : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), |
515 : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), |
516 transform_additional_arguments = K I : (indprem -> term list -> term list) |
516 transform_additional_arguments = K I : (indprem -> term list -> term list) |
534 compilation = Pos_Generator_CPS, |
534 compilation = Pos_Generator_CPS, |
535 function_name_prefix = "generator_cps_pos_", |
535 function_name_prefix = "generator_cps_pos_", |
536 compfuns = Pos_Bounded_CPS_Comp_Funs.compfuns, |
536 compfuns = Pos_Bounded_CPS_Comp_Funs.compfuns, |
537 mk_random = |
537 mk_random = |
538 (fn T => fn _ => |
538 (fn T => fn _ => |
539 Const (@{const_name "Quickcheck_Exhaustive.exhaustive"}, |
539 Const (\<^const_name>\<open>Quickcheck_Exhaustive.exhaustive\<close>, |
540 (T --> @{typ "(bool * term list) option"}) --> |
540 (T --> \<^typ>\<open>(bool * term list) option\<close>) --> |
541 @{typ "natural => (bool * term list) option"})), |
541 \<^typ>\<open>natural => (bool * term list) option\<close>)), |
542 modify_funT = I, |
542 modify_funT = I, |
543 additional_arguments = K [], |
543 additional_arguments = K [], |
544 wrap_compilation = K (K (K (K (K I)))) |
544 wrap_compilation = K (K (K (K (K I)))) |
545 : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), |
545 : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), |
546 transform_additional_arguments = K I : (indprem -> term list -> term list) |
546 transform_additional_arguments = K I : (indprem -> term list -> term list) |
595 |
595 |
596 |
596 |
597 (** specific rpred functions -- move them to the correct place in this file *) |
597 (** specific rpred functions -- move them to the correct place in this file *) |
598 fun mk_Eval_of (P as (Free _), T) mode = |
598 fun mk_Eval_of (P as (Free _), T) mode = |
599 let |
599 let |
600 fun mk_bounds (Type (@{type_name Product_Type.prod}, [T1, T2])) i = |
600 fun mk_bounds (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) i = |
601 let |
601 let |
602 val (bs2, i') = mk_bounds T2 i |
602 val (bs2, i') = mk_bounds T2 i |
603 val (bs1, i'') = mk_bounds T1 i' |
603 val (bs1, i'') = mk_bounds T1 i' |
604 in |
604 in |
605 (HOLogic.pair_const T1 T2 $ bs1 $ bs2, i'' + 1) |
605 (HOLogic.pair_const T1 T2 $ bs1 $ bs2, i'' + 1) |
606 end |
606 end |
607 | mk_bounds _ i = (Bound i, i + 1) |
607 | mk_bounds _ i = (Bound i, i + 1) |
608 fun mk_prod ((t1, T1), (t2, T2)) = (HOLogic.pair_const T1 T2 $ t1 $ t2, HOLogic.mk_prodT (T1, T2)) |
608 fun mk_prod ((t1, T1), (t2, T2)) = (HOLogic.pair_const T1 T2 $ t1 $ t2, HOLogic.mk_prodT (T1, T2)) |
609 fun mk_tuple [] = (HOLogic.unit, HOLogic.unitT) |
609 fun mk_tuple [] = (HOLogic.unit, HOLogic.unitT) |
610 | mk_tuple tTs = foldr1 mk_prod tTs |
610 | mk_tuple tTs = foldr1 mk_prod tTs |
611 fun mk_split_abs (T as Type (@{type_name Product_Type.prod}, [T1, T2])) t = |
611 fun mk_split_abs (T as Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) t = |
612 absdummy T |
612 absdummy T |
613 (HOLogic.case_prod_const (T1, T2, @{typ bool}) $ (mk_split_abs T1 (mk_split_abs T2 t))) |
613 (HOLogic.case_prod_const (T1, T2, \<^typ>\<open>bool\<close>) $ (mk_split_abs T1 (mk_split_abs T2 t))) |
614 | mk_split_abs T t = absdummy T t |
614 | mk_split_abs T t = absdummy T t |
615 val args = rev (fst (fold_map mk_bounds (rev (binder_types T)) 0)) |
615 val args = rev (fst (fold_map mk_bounds (rev (binder_types T)) 0)) |
616 val (inargs, outargs) = split_mode mode args |
616 val (inargs, outargs) = split_mode mode args |
617 val (_, outTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) mode (binder_types T) |
617 val (_, outTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) mode (binder_types T) |
618 val inner_term = Predicate_Comp_Funs.mk_Eval (list_comb (P, inargs), fst (mk_tuple (outargs ~~ outTs))) |
618 val inner_term = Predicate_Comp_Funs.mk_Eval (list_comb (P, inargs), fst (mk_tuple (outargs ~~ outTs))) |
687 | (t, Context _) => |
687 | (t, Context _) => |
688 let |
688 let |
689 val bs = map (pair "x") (binder_types (fastype_of t)) |
689 val bs = map (pair "x") (binder_types (fastype_of t)) |
690 val bounds = map Bound (rev (0 upto (length bs) - 1)) |
690 val bounds = map Bound (rev (0 upto (length bs) - 1)) |
691 in SOME (fold_rev Term.abs bs (mk_if compfuns (list_comb (t, bounds)))) end |
691 in SOME (fold_rev Term.abs bs (mk_if compfuns (list_comb (t, bounds)))) end |
692 | (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (d1, d2)) => |
692 | (Const (\<^const_name>\<open>Pair\<close>, _) $ t1 $ t2, Mode_Pair (d1, d2)) => |
693 (case (expr_of (t1, d1), expr_of (t2, d2)) of |
693 (case (expr_of (t1, d1), expr_of (t2, d2)) of |
694 (NONE, NONE) => NONE |
694 (NONE, NONE) => NONE |
695 | (NONE, SOME t) => SOME t |
695 | (NONE, SOME t) => SOME t |
696 | (SOME t, NONE) => SOME t |
696 | (SOME t, NONE) => SOME t |
697 | (SOME t1, SOME t2) => SOME (HOLogic.mk_prod (t1, t2))) |
697 | (SOME t1, SOME t2) => SOME (HOLogic.mk_prod (t1, t2))) |
1021 end |
1021 end |
1022 |
1022 |
1023 |
1023 |
1024 (* Definition of executable functions and their intro and elim rules *) |
1024 (* Definition of executable functions and their intro and elim rules *) |
1025 |
1025 |
1026 fun strip_split_abs (Const (@{const_name case_prod}, _) $ t) = strip_split_abs t |
1026 fun strip_split_abs (Const (\<^const_name>\<open>case_prod\<close>, _) $ t) = strip_split_abs t |
1027 | strip_split_abs (Abs (_, _, t)) = strip_split_abs t |
1027 | strip_split_abs (Abs (_, _, t)) = strip_split_abs t |
1028 | strip_split_abs t = t |
1028 | strip_split_abs t = t |
1029 |
1029 |
1030 fun mk_args is_eval (m as Pair (m1, m2), T as Type (@{type_name Product_Type.prod}, [T1, T2])) names = |
1030 fun mk_args is_eval (m as Pair (m1, m2), T as Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) names = |
1031 if eq_mode (m, Input) orelse eq_mode (m, Output) then |
1031 if eq_mode (m, Input) orelse eq_mode (m, Output) then |
1032 let |
1032 let |
1033 val x = singleton (Name.variant_list names) "x" |
1033 val x = singleton (Name.variant_list names) "x" |
1034 in |
1034 in |
1035 (Free (x, T), x :: names) |
1035 (Free (x, T), x :: names) |
1339 val Ts = binder_types T |
1339 val Ts = binder_types T |
1340 val arg_names = Name.variant_list [] |
1340 val arg_names = Name.variant_list [] |
1341 (map (fn i => "x" ^ string_of_int i) (1 upto length Ts)) |
1341 (map (fn i => "x" ^ string_of_int i) (1 upto length Ts)) |
1342 val args = map2 (curry Free) arg_names Ts |
1342 val args = map2 (curry Free) arg_names Ts |
1343 val predfun = Const (Core_Data.function_name_of Pred ctxt predname full_mode, |
1343 val predfun = Const (Core_Data.function_name_of Pred ctxt predname full_mode, |
1344 Ts ---> Predicate_Comp_Funs.mk_monadT @{typ unit}) |
1344 Ts ---> Predicate_Comp_Funs.mk_monadT \<^typ>\<open>unit\<close>) |
1345 val rhs = @{term Predicate.holds} $ (list_comb (predfun, args)) |
1345 val rhs = \<^term>\<open>Predicate.holds\<close> $ (list_comb (predfun, args)) |
1346 val eq_term = HOLogic.mk_Trueprop |
1346 val eq_term = HOLogic.mk_Trueprop |
1347 (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs)) |
1347 (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs)) |
1348 val def = Core_Data.predfun_definition_of ctxt predname full_mode |
1348 val def = Core_Data.predfun_definition_of ctxt predname full_mode |
1349 val tac = fn _ => Simplifier.simp_tac |
1349 val tac = fn _ => Simplifier.simp_tac |
1350 (put_simpset HOL_basic_ss ctxt addsimps [def, @{thm holds_eq}, @{thm pred.sel}]) 1 |
1350 (put_simpset HOL_basic_ss ctxt addsimps [def, @{thm holds_eq}, @{thm pred.sel}]) 1 |
1772 (Const (name, T), all_args) => (Const (name, T), all_args) |
1772 (Const (name, T), all_args) => (Const (name, T), all_args) |
1773 | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head)) |
1773 | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head)) |
1774 in |
1774 in |
1775 if Core_Data.defined_functions compilation ctxt name then |
1775 if Core_Data.defined_functions compilation ctxt name then |
1776 let |
1776 let |
1777 fun extract_mode (Const (@{const_name Pair}, _) $ t1 $ t2) = |
1777 fun extract_mode (Const (\<^const_name>\<open>Pair\<close>, _) $ t1 $ t2) = |
1778 Pair (extract_mode t1, extract_mode t2) |
1778 Pair (extract_mode t1, extract_mode t2) |
1779 | extract_mode (Free (x, _)) = |
1779 | extract_mode (Free (x, _)) = |
1780 if member (op =) output_names x then Output else Input |
1780 if member (op =) output_names x then Output else Input |
1781 | extract_mode _ = Input |
1781 | extract_mode _ = Input |
1782 val user_mode = fold_rev (curry Fun) (map extract_mode all_args) Bool |
1782 val user_mode = fold_rev (curry Fun) (map extract_mode all_args) Bool |
1855 val compfuns = Comp_Mod.compfuns comp_modifiers |
1855 val compfuns = Comp_Mod.compfuns comp_modifiers |
1856 val additional_arguments = |
1856 val additional_arguments = |
1857 (case compilation of |
1857 (case compilation of |
1858 Pred => [] |
1858 Pred => [] |
1859 | Random => |
1859 | Random => |
1860 map (HOLogic.mk_number @{typ "natural"}) arguments @ |
1860 map (HOLogic.mk_number \<^typ>\<open>natural\<close>) arguments @ |
1861 [@{term "(1, 1) :: natural * natural"}] |
1861 [\<^term>\<open>(1, 1) :: natural * natural\<close>] |
1862 | Annotated => [] |
1862 | Annotated => [] |
1863 | Depth_Limited => [HOLogic.mk_number @{typ "natural"} (hd arguments)] |
1863 | Depth_Limited => [HOLogic.mk_number \<^typ>\<open>natural\<close> (hd arguments)] |
1864 | Depth_Limited_Random => |
1864 | Depth_Limited_Random => |
1865 map (HOLogic.mk_number @{typ "natural"}) arguments @ |
1865 map (HOLogic.mk_number \<^typ>\<open>natural\<close>) arguments @ |
1866 [@{term "(1, 1) :: natural * natural"}] |
1866 [\<^term>\<open>(1, 1) :: natural * natural\<close>] |
1867 | DSeq => [] |
1867 | DSeq => [] |
1868 | Pos_Random_DSeq => [] |
1868 | Pos_Random_DSeq => [] |
1869 | New_Pos_Random_DSeq => [] |
1869 | New_Pos_Random_DSeq => [] |
1870 | Pos_Generator_DSeq => []) |
1870 | Pos_Generator_DSeq => []) |
1871 val t = |
1871 val t = |
1872 analyze_compr ctxt (comp_modifiers, additional_arguments) param_user_modes options t_compr |
1872 analyze_compr ctxt (comp_modifiers, additional_arguments) param_user_modes options t_compr |
1873 val T = dest_monadT compfuns (fastype_of t) |
1873 val T = dest_monadT compfuns (fastype_of t) |
1874 val t' = |
1874 val t' = |
1875 if stats andalso compilation = New_Pos_Random_DSeq then |
1875 if stats andalso compilation = New_Pos_Random_DSeq then |
1876 mk_map compfuns T (HOLogic.mk_prodT (HOLogic.termT, @{typ natural})) |
1876 mk_map compfuns T (HOLogic.mk_prodT (HOLogic.termT, \<^typ>\<open>natural\<close>)) |
1877 (absdummy T (HOLogic.mk_prod (HOLogic.term_of_const T $ Bound 0, |
1877 (absdummy T (HOLogic.mk_prod (HOLogic.term_of_const T $ Bound 0, |
1878 @{term natural_of_nat} $ (HOLogic.size_const T $ Bound 0)))) t |
1878 \<^term>\<open>natural_of_nat\<close> $ (HOLogic.size_const T $ Bound 0)))) t |
1879 else |
1879 else |
1880 mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t |
1880 mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t |
1881 val time_limit = seconds (Config.get ctxt values_timeout) |
1881 val time_limit = seconds (Config.get ctxt values_timeout) |
1882 val (ts, statistics) = |
1882 val (ts, statistics) = |
1883 (case compilation of |
1883 (case compilation of |