author  bulwahn 
Thu, 22 Sep 2011 07:26:53 +0200  
changeset 45039  632a033616e9 
parent 45002  df36896aae0f 
child 45159  3f1d1ce024cb 
permissions  rwrr 
41930
1e008cc4883a
renaming lazysmallcheck ML file to Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset

1 
(* Title: HOL/Tools/Quickcheck/narrowing_generators.ML 
41905  2 
Author: Lukas Bulwahn, TU Muenchen 
3 

41938  4 
Narrowingbased counterexample generation. 
41905  5 
*) 
6 

41930
1e008cc4883a
renaming lazysmallcheck ML file to Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset

7 
signature NARROWING_GENERATORS = 
41905  8 
sig 
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

9 
val allow_existentials : bool Config.T 
42023
1bd4b6d1c482
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents:
42020
diff
changeset

10 
val finite_functions : bool Config.T 
43079
4022892a2f28
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
bulwahn
parents:
43047
diff
changeset

11 
val overlord : bool Config.T 
43891
4690f76f327a
making active configuration public in narrowingbased quickcheck
bulwahn
parents:
43878
diff
changeset

12 
val active : bool Config.T 
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

13 
val test_term: Proof.context > bool * bool > term * term list > Quickcheck.result 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

14 
datatype counterexample = Universal_Counterexample of (term * counterexample) 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

15 
 Existential_Counterexample of (term * counterexample) list 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

16 
 Empty_Assignment 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

17 
val put_counterexample: (unit > term list option) > Proof.context > Proof.context 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

18 
val put_existential_counterexample : (unit > counterexample option) > Proof.context > Proof.context 
41905  19 
val setup: theory > theory 
20 
end; 

21 

41930
1e008cc4883a
renaming lazysmallcheck ML file to Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset

22 
structure Narrowing_Generators : NARROWING_GENERATORS = 
41905  23 
struct 
24 

42023
1bd4b6d1c482
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents:
42020
diff
changeset

25 
(* configurations *) 
1bd4b6d1c482
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents:
42020
diff
changeset

26 

43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

27 
val allow_existentials = Attrib.setup_config_bool @{binding quickcheck_allow_existentials} (K true) 
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42361
diff
changeset

28 
val finite_functions = Attrib.setup_config_bool @{binding quickcheck_finite_functions} (K true) 
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

29 
val overlord = Attrib.setup_config_bool @{binding quickcheck_narrowing_overlord} (K false) 
42023
1bd4b6d1c482
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents:
42020
diff
changeset

30 

43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

31 
(* partial_term_of instances *) 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

32 

26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

33 
fun mk_partial_term_of (x, T) = 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

34 
Const (@{const_name Quickcheck_Narrowing.partial_term_of_class.partial_term_of}, 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

35 
Term.itselfT T > @{typ narrowing_term} > @{typ Code_Evaluation.term}) 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

36 
$ Const ("TYPE", Term.itselfT T) $ x 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

37 

26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

38 
(** formal definition **) 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

39 

26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

40 
fun add_partial_term_of tyco raw_vs thy = 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

41 
let 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

42 
val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs; 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

43 
val ty = Type (tyco, map TFree vs); 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

44 
val lhs = Const (@{const_name partial_term_of}, 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

45 
Term.itselfT ty > @{typ narrowing_term} > @{typ Code_Evaluation.term}) 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

46 
$ Free ("x", Term.itselfT ty) $ Free ("t", @{typ narrowing_term}); 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

47 
val rhs = @{term "undefined :: Code_Evaluation.term"}; 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

48 
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

49 
fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

50 
o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv"; 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

51 
in 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

52 
thy 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

53 
> Class.instantiation ([tyco], vs, @{sort partial_term_of}) 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

54 
> `(fn lthy => Syntax.check_term lthy eq) 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

55 
> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq))) 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

56 
> snd 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

57 
> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

58 
end; 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

59 

26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

60 
fun ensure_partial_term_of (tyco, (raw_vs, _)) thy = 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

61 
let 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

62 
val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort partial_term_of}) 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

63 
andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep}; 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

64 
in if need_inst then add_partial_term_of tyco raw_vs thy else thy end; 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

65 

26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

66 

26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

67 
(** code equations for datatypes **) 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

68 

26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

69 
fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) = 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

70 
let 
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43317
diff
changeset

71 
val frees = map Free (Name.invent_names Name.context "a" (map (K @{typ narrowing_term}) tys)) 
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

72 
val narrowing_term = @{term "Quickcheck_Narrowing.Ctr"} $ HOLogic.mk_number @{typ code_int} i 
43079
4022892a2f28
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
bulwahn
parents:
43047
diff
changeset

73 
$ (HOLogic.mk_list @{typ narrowing_term} (rev frees)) 
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

74 
val rhs = fold (fn u => fn t => @{term "Code_Evaluation.App"} $ t $ u) 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

75 
(map mk_partial_term_of (frees ~~ tys)) 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

76 
(@{term "Code_Evaluation.Const"} $ HOLogic.mk_literal c $ HOLogic.mk_typerep (tys > ty)) 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

77 
val insts = 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

78 
map (SOME o Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global) 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

79 
[Free ("ty", Term.itselfT ty), narrowing_term, rhs] 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

80 
val cty = Thm.ctyp_of thy ty; 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

81 
in 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

82 
@{thm partial_term_of_anything} 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

83 
> Drule.instantiate' [SOME cty] insts 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

84 
> Thm.varifyT_global 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

85 
end 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

86 

26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

87 
fun add_partial_term_of_code tyco raw_vs raw_cs thy = 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

88 
let 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

89 
val algebra = Sign.classes_of thy; 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

90 
val vs = map (fn (v, sort) => 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

91 
(v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs; 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

92 
val ty = Type (tyco, map TFree vs); 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

93 
val cs = (map o apsnd o apsnd o map o map_atyps) 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

94 
(fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs; 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

95 
val const = AxClass.param_of_inst thy (@{const_name partial_term_of}, tyco); 
43079
4022892a2f28
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
bulwahn
parents:
43047
diff
changeset

96 
val var_insts = map (SOME o Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global) 
4022892a2f28
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
bulwahn
parents:
43047
diff
changeset

97 
[Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Var p tt"}, 
4022892a2f28
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
bulwahn
parents:
43047
diff
changeset

98 
@{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty] 
4022892a2f28
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
bulwahn
parents:
43047
diff
changeset

99 
val var_eq = 
4022892a2f28
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
bulwahn
parents:
43047
diff
changeset

100 
@{thm partial_term_of_anything} 
4022892a2f28
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
bulwahn
parents:
43047
diff
changeset

101 
> Drule.instantiate' [SOME (Thm.ctyp_of thy ty)] var_insts 
4022892a2f28
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
bulwahn
parents:
43047
diff
changeset

102 
> Thm.varifyT_global 
4022892a2f28
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
bulwahn
parents:
43047
diff
changeset

103 
val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs; 
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

104 
in 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

105 
thy 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

106 
> Code.del_eqns const 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

107 
> fold Code.add_eqn eqs 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

108 
end; 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

109 

26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

110 
fun ensure_partial_term_of_code (tyco, (raw_vs, cs)) thy = 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

111 
let 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

112 
val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort partial_term_of}; 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

113 
in if has_inst then add_partial_term_of_code tyco raw_vs cs thy else thy end; 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

114 

26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

115 

26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

116 
(* narrowing generators *) 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

117 

26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

118 
(** narrowing specific names and types **) 
41963
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

119 

d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

120 
exception FUNCTION_TYPE; 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

121 

d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

122 
val narrowingN = "narrowing"; 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

123 

d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

124 
fun narrowingT T = 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

125 
@{typ Quickcheck_Narrowing.code_int} > Type (@{type_name Quickcheck_Narrowing.cons}, [T]) 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

126 

d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

127 
fun mk_empty T = Const (@{const_name Quickcheck_Narrowing.empty}, narrowingT T) 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

128 

d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

129 
fun mk_cons c T = Const (@{const_name Quickcheck_Narrowing.cons}, T > narrowingT T) $ Const (c, T) 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

130 

d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

131 
fun mk_apply (T, t) (U, u) = 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

132 
let 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

133 
val (_, U') = dest_funT U 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

134 
in 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

135 
(U', Const (@{const_name Quickcheck_Narrowing.apply}, 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

136 
narrowingT U > narrowingT T > narrowingT U') $ u $ t) 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

137 
end 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

138 

d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

139 
fun mk_sum (t, u) = 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

140 
let 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

141 
val T = fastype_of t 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

142 
in 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

143 
Const (@{const_name Quickcheck_Narrowing.sum}, T > T > T) $ t $ u 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

144 
end 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

145 

43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

146 
(** deriving narrowing instances **) 
41963
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

147 

d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

148 
fun mk_equations descr vs tycos narrowings (Ts, Us) = 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

149 
let 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

150 
fun mk_call T = 
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42184
diff
changeset

151 
(T, Const (@{const_name "Quickcheck_Narrowing.narrowing_class.narrowing"}, narrowingT T)) 
41963
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

152 
fun mk_aux_call fTs (k, _) (tyco, Ts) = 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

153 
let 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

154 
val T = Type (tyco, Ts) 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

155 
val _ = if not (null fTs) then raise FUNCTION_TYPE else () 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

156 
in 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

157 
(T, nth narrowings k) 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

158 
end 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

159 
fun mk_consexpr simpleT (c, xs) = 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

160 
let 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

161 
val Ts = map fst xs 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

162 
in snd (fold mk_apply xs (Ts > simpleT, mk_cons c (Ts > simpleT))) end 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

163 
fun mk_rhs exprs = foldr1 mk_sum exprs 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

164 
val rhss = 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

165 
Datatype_Aux.interpret_construction descr vs 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

166 
{ atyp = mk_call, dtyp = mk_aux_call } 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

167 
> (map o apfst) Type 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

168 
> map (fn (T, cs) => map (mk_consexpr T) cs) 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

169 
> map mk_rhs 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

170 
val lhss = narrowings 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

171 
val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss) 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

172 
in 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

173 
eqs 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

174 
end 
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

175 

8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

176 
fun contains_recursive_type_under_function_types xs = 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

177 
exists (fn (_, (_, _, cs)) => cs > exists (snd #> exists (fn dT => 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

178 
(case Datatype_Aux.strip_dtyp dT of (_ :: _, Datatype.DtRec _) => true  _ => false)))) xs 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

179 

41963
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

180 
fun instantiate_narrowing_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy = 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

181 
let 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

182 
val _ = Datatype_Aux.message config "Creating narrowing generators ..."; 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

183 
val narrowingsN = map (prefix (narrowingN ^ "_")) (names @ auxnames); 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

184 
in 
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

185 
if not (contains_recursive_type_under_function_types descr) then 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

186 
thy 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

187 
> Class.instantiation (tycos, vs, @{sort narrowing}) 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

188 
> Quickcheck_Common.define_functions 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

189 
(fn narrowings => mk_equations descr vs tycos narrowings (Ts, Us), NONE) 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

190 
prfx [] narrowingsN (map narrowingT (Ts @ Us)) 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

191 
> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

192 
else 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

193 
thy 
41963
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

194 
end; 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

195 

d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

196 
(* testing framework *) 
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset

197 

43308
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43240
diff
changeset

198 
val target = "Haskell_Quickcheck" 
41930
1e008cc4883a
renaming lazysmallcheck ML file to Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset

199 

43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

200 
(** invocation of Haskell interpreter **) 
41905  201 

43702
24fb44c1086a
more abstract Thy_Load.load_file/use_file for external theory resources;
wenzelm
parents:
43619
diff
changeset

202 
val narrowing_engine = 
24fb44c1086a
more abstract Thy_Load.load_file/use_file for external theory resources;
wenzelm
parents:
43619
diff
changeset

203 
Context.>>> (Context.map_theory_result 
24fb44c1086a
more abstract Thy_Load.load_file/use_file for external theory resources;
wenzelm
parents:
43619
diff
changeset

204 
(Thy_Load.use_file (Path.explode "Tools/Quickcheck/Narrowing_Engine.hs"))) 
24fb44c1086a
more abstract Thy_Load.load_file/use_file for external theory resources;
wenzelm
parents:
43619
diff
changeset

205 

24fb44c1086a
more abstract Thy_Load.load_file/use_file for external theory resources;
wenzelm
parents:
43619
diff
changeset

206 
val pnf_narrowing_engine = 
24fb44c1086a
more abstract Thy_Load.load_file/use_file for external theory resources;
wenzelm
parents:
43619
diff
changeset

207 
Context.>>> (Context.map_theory_result 
24fb44c1086a
more abstract Thy_Load.load_file/use_file for external theory resources;
wenzelm
parents:
43619
diff
changeset

208 
(Thy_Load.use_file (Path.explode "Tools/Quickcheck/PNF_Narrowing_Engine.hs"))) 
41905  209 

210 
fun exec verbose code = 

211 
ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code) 

212 

43079
4022892a2f28
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
bulwahn
parents:
43047
diff
changeset

213 
fun with_overlord_dir name f = 
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

214 
let 
43602  215 
val path = 
216 
Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ())) 

43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

217 
val _ = Isabelle_System.mkdirs path; 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

218 
in Exn.release (Exn.capture f path) end; 
43379
8c4b383e5143
quickcheck_narrowing returns some timing information
bulwahn
parents:
43329
diff
changeset

219 

8c4b383e5143
quickcheck_narrowing returns some timing information
bulwahn
parents:
43329
diff
changeset

220 
fun elapsed_time description e = 
8c4b383e5143
quickcheck_narrowing returns some timing information
bulwahn
parents:
43329
diff
changeset

221 
let val ({elapsed, ...}, result) = Timing.timing e () 
8c4b383e5143
quickcheck_narrowing returns some timing information
bulwahn
parents:
43329
diff
changeset

222 
in (result, (description, Time.toMilliseconds elapsed)) end 
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

223 

43585  224 
fun value (contains_existentials, opts) ctxt cookie (code, value_name) = 
41905  225 
let 
43585  226 
val (limit_time, is_interactive, timeout, quiet, size) = opts 
227 
val (get, put, put_ml) = cookie 

43308
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43240
diff
changeset

228 
fun message s = if quiet then () else Output.urgent_message s 
43585  229 
val current_size = Unsynchronized.ref 0 
230 
val current_result = Unsynchronized.ref Quickcheck.empty_result 

231 
fun excipit () = 

232 
"Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size) 

41930
1e008cc4883a
renaming lazysmallcheck ML file to Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset

233 
val tmp_prefix = "Quickcheck_Narrowing" 
43079
4022892a2f28
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
bulwahn
parents:
43047
diff
changeset

234 
val with_tmp_dir = 
4022892a2f28
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
bulwahn
parents:
43047
diff
changeset

235 
if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir 
41905  236 
fun run in_path = 
237 
let 

44751
f523923d8182
avoid "Code" as structure name (cf. 3bc39cfe27fe)
bulwahn
parents:
44321
diff
changeset

238 
val code_file = Path.append in_path (Path.basic "Generated_Code.hs") 
41930
1e008cc4883a
renaming lazysmallcheck ML file to Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset

239 
val narrowing_engine_file = Path.append in_path (Path.basic "Narrowing_Engine.hs") 
41905  240 
val main_file = Path.append in_path (Path.basic "Main.hs") 
241 
val main = "module Main where {\n\n" ^ 

43114
b9fca691addd
Quickcheck Narrowing only requires one compilation with GHC now
bulwahn
parents:
43079
diff
changeset

242 
"import System;\n" ^ 
41933
10f254a4e5b9
adapting Main file generation for Quickcheck_Narrowing
bulwahn
parents:
41932
diff
changeset

243 
"import Narrowing_Engine;\n" ^ 
44751
f523923d8182
avoid "Code" as structure name (cf. 3bc39cfe27fe)
bulwahn
parents:
44321
diff
changeset

244 
"import Generated_Code;\n\n" ^ 
f523923d8182
avoid "Code" as structure name (cf. 3bc39cfe27fe)
bulwahn
parents:
44321
diff
changeset

245 
"main = getArgs >>= \\[size] > Narrowing_Engine.depthCheck (read size) (Generated_Code.value ())\n\n" ^ 
41905  246 
"}\n" 
44751
f523923d8182
avoid "Code" as structure name (cf. 3bc39cfe27fe)
bulwahn
parents:
44321
diff
changeset

247 
val code' = prefix "module Generated_Code where {\n\ndata Typerep = Typerep String [Typerep];\n" 
f523923d8182
avoid "Code" as structure name (cf. 3bc39cfe27fe)
bulwahn
parents:
44321
diff
changeset

248 
(unprefix "module Generated_Code where {" code) 
41909
383bbdad1650
replacing strings in generated Code resolves the changing names of Typerep in lazysmallcheck prototype
bulwahn
parents:
41908
diff
changeset

249 
val _ = File.write code_file code' 
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

250 
val _ = File.write narrowing_engine_file 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

251 
(if contains_existentials then pnf_narrowing_engine else narrowing_engine) 
41905  252 
val _ = File.write main_file main 
43114
b9fca691addd
Quickcheck Narrowing only requires one compilation with GHC now
bulwahn
parents:
43079
diff
changeset

253 
val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing")) 
44926
de3ed037c9a5
create central list for language extensions used by the haskell code generator
noschinl
parents:
44852
diff
changeset

254 
val cmd = "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ 
41946  255 
(space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^ 
43114
b9fca691addd
Quickcheck Narrowing only requires one compilation with GHC now
bulwahn
parents:
43079
diff
changeset

256 
" o " ^ executable ^ ";" 
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43702
diff
changeset

257 
val (result, compilation_time) = 
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43702
diff
changeset

258 
elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd) 
43585  259 
val _ = Quickcheck.add_timing compilation_time current_result 
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43702
diff
changeset

260 
val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else () 
43585  261 
fun with_size k = 
43308
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43240
diff
changeset

262 
if k > size then 
43585  263 
(NONE, !current_result) 
43114
b9fca691addd
Quickcheck Narrowing only requires one compilation with GHC now
bulwahn
parents:
43079
diff
changeset

264 
else 
b9fca691addd
Quickcheck Narrowing only requires one compilation with GHC now
bulwahn
parents:
43079
diff
changeset

265 
let 
43910  266 
val _ = message ("[QuickcheckNarrowing] Test data size: " ^ string_of_int k) 
43585  267 
val _ = current_size := k 
268 
val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k) 

43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43702
diff
changeset

269 
(fn () => Isabelle_System.bash_output (executable ^ " " ^ string_of_int k)) 
43585  270 
val _ = Quickcheck.add_timing timing current_result 
43114
b9fca691addd
Quickcheck Narrowing only requires one compilation with GHC now
bulwahn
parents:
43079
diff
changeset

271 
in 
43585  272 
if response = "NONE\n" then 
273 
with_size (k + 1) 

274 
else 

275 
let 

276 
val output_value = the_default "NONE" 

277 
(try (snd o split_last o filter_out (fn s => s = "") o split_lines) response) 

278 
> translate_string (fn s => if s = "\\" then "\\\\" else s) 

279 
val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml 

280 
^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))"; 

281 
val ctxt' = ctxt 

282 
> put (fn () => error ("Bad evaluation for " ^ quote put_ml)) 

283 
> Context.proof_map (exec false ml_code); 

284 
in (get ctxt' (), !current_result) end 

285 
end 

286 
in with_size 0 end 

287 
in 

43915  288 
(*Quickcheck.limit timeout (limit_time, is_interactive) 
289 
(fn () =>*) with_tmp_dir tmp_prefix run 

290 
(*(fn () => (message (excipit ()); (NONE, !current_result))) ()*) 

43585  291 
end; 
41905  292 

43308
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43240
diff
changeset

293 
fun dynamic_value_strict opts cookie thy postproc t = 
41905  294 
let 
43114
b9fca691addd
Quickcheck Narrowing only requires one compilation with GHC now
bulwahn
parents:
43079
diff
changeset

295 
val ctxt = Proof_Context.init_global thy 
43308
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43240
diff
changeset

296 
fun evaluator naming program ((_, vs_ty), t) deps = Exn.interruptible_capture (value opts ctxt cookie) 
43114
b9fca691addd
Quickcheck Narrowing only requires one compilation with GHC now
bulwahn
parents:
43079
diff
changeset

297 
(Code_Target.evaluator thy target naming program deps (vs_ty, t)); 
41905  298 
in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end; 
299 

43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

300 
(** counterexample generator **) 
41905  301 

41932
e8f113ce8a94
adapting Quickcheck_Narrowing and example file to new names
bulwahn
parents:
41930
diff
changeset

302 
structure Counterexample = Proof_Data 
41905  303 
( 
304 
type T = unit > term list option 

41936
9792a882da9c
renaming tester from lazy_exhaustive to narrowing
bulwahn
parents:
41933
diff
changeset

305 
fun init _ () = error "Counterexample" 
41905  306 
) 
307 

43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

308 
datatype counterexample = Universal_Counterexample of (term * counterexample) 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

309 
 Existential_Counterexample of (term * counterexample) list 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

310 
 Empty_Assignment 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

311 

8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

312 
fun map_counterexample f Empty_Assignment = Empty_Assignment 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

313 
 map_counterexample f (Universal_Counterexample (t, c)) = 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

314 
Universal_Counterexample (f t, map_counterexample f c) 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

315 
 map_counterexample f (Existential_Counterexample cs) = 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

316 
Existential_Counterexample (map (fn (t, c) => (f t, map_counterexample f c)) cs) 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

317 

8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

318 
structure Existential_Counterexample = Proof_Data 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

319 
( 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

320 
type T = unit > counterexample option 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

321 
fun init _ () = error "Counterexample" 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

322 
) 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

323 

8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

324 
val put_existential_counterexample = Existential_Counterexample.put 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

325 

42024
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

326 
val put_counterexample = Counterexample.put 
42023
1bd4b6d1c482
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents:
42020
diff
changeset

327 

43240
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset

328 
fun finitize_functions (xTs, t) = 
42024
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

329 
let 
43240
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset

330 
val (names, boundTs) = split_list xTs 
42024
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

331 
fun mk_eval_ffun dT rT = 
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

332 
Const (@{const_name "Quickcheck_Narrowing.eval_ffun"}, 
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

333 
Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT]) > dT > rT) 
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

334 
fun mk_eval_cfun dT rT = 
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

335 
Const (@{const_name "Quickcheck_Narrowing.eval_cfun"}, 
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

336 
Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT]) > dT > rT) 
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

337 
fun eval_function (T as Type (@{type_name fun}, [dT, rT])) = 
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

338 
let 
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

339 
val (rt', rT') = eval_function rT 
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

340 
in 
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

341 
case dT of 
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

342 
Type (@{type_name fun}, _) => 
44241  343 
(fn t => absdummy dT (rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)), 
344 
Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT'])) 

345 
 _ => 

346 
(fn t => absdummy dT (rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)), 

347 
Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT'])) 

42024
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

348 
end 
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

349 
 eval_function T = (I, T) 
43240
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset

350 
val (tt, boundTs') = split_list (map eval_function boundTs) 
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset

351 
val t' = subst_bounds (map2 (fn f => fn x => f x) (rev tt) (map_index (Bound o fst) boundTs), t) 
42024
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

352 
in 
43240
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset

353 
(names ~~ boundTs', t') 
42024
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

354 
end 
42023
1bd4b6d1c482
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents:
42020
diff
changeset

355 

45039
632a033616e9
adding postprocessing of terms to narrowingbased Quickcheck
bulwahn
parents:
45002
diff
changeset

356 
fun dest_ffun (Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT])) = (dT, rT) 
632a033616e9
adding postprocessing of terms to narrowingbased Quickcheck
bulwahn
parents:
45002
diff
changeset

357 

632a033616e9
adding postprocessing of terms to narrowingbased Quickcheck
bulwahn
parents:
45002
diff
changeset

358 
fun eval_finite_functions (Const (@{const_name "Quickcheck_Narrowing.ffun.Constant"}, T) $ value) = 
632a033616e9
adding postprocessing of terms to narrowingbased Quickcheck
bulwahn
parents:
45002
diff
changeset

359 
absdummy (fst (dest_ffun (body_type T))) (eval_finite_functions value) 
632a033616e9
adding postprocessing of terms to narrowingbased Quickcheck
bulwahn
parents:
45002
diff
changeset

360 
 eval_finite_functions (Const (@{const_name "Quickcheck_Narrowing.ffun.Update"}, T) $ a $ b $ f) = 
632a033616e9
adding postprocessing of terms to narrowingbased Quickcheck
bulwahn
parents:
45002
diff
changeset

361 
let 
632a033616e9
adding postprocessing of terms to narrowingbased Quickcheck
bulwahn
parents:
45002
diff
changeset

362 
val (T1, T2) = dest_ffun (body_type T) 
632a033616e9
adding postprocessing of terms to narrowingbased Quickcheck
bulwahn
parents:
45002
diff
changeset

363 
in 
632a033616e9
adding postprocessing of terms to narrowingbased Quickcheck
bulwahn
parents:
45002
diff
changeset

364 
Quickcheck_Common.mk_fun_upd T1 T2 
632a033616e9
adding postprocessing of terms to narrowingbased Quickcheck
bulwahn
parents:
45002
diff
changeset

365 
(eval_finite_functions a, eval_finite_functions b) (eval_finite_functions f) 
632a033616e9
adding postprocessing of terms to narrowingbased Quickcheck
bulwahn
parents:
45002
diff
changeset

366 
end 
632a033616e9
adding postprocessing of terms to narrowingbased Quickcheck
bulwahn
parents:
45002
diff
changeset

367 
 eval_finite_functions t = t 
632a033616e9
adding postprocessing of terms to narrowingbased Quickcheck
bulwahn
parents:
45002
diff
changeset

368 

43114
b9fca691addd
Quickcheck Narrowing only requires one compilation with GHC now
bulwahn
parents:
43079
diff
changeset

369 
(** tester **) 
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

370 

8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

371 
val rewrs = 
43240
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset

372 
map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) 
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset

373 
(@{thms all_simps} @ @{thms ex_simps}) 
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset

374 
@ map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) 
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset

375 
[@{thm iff_conv_conj_imp}, @{thm not_ex}, @{thm not_all}] 
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

376 

8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

377 
fun make_pnf_term thy t = Pattern.rewrite_term thy rewrs [] t 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

378 

8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

379 
fun strip_quantifiers (Const (@{const_name Ex}, _) $ Abs (x, T, t)) = 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

380 
apfst (cons (@{const_name Ex}, (x, T))) (strip_quantifiers t) 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

381 
 strip_quantifiers (Const (@{const_name All}, _) $ Abs (x, T, t)) = 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

382 
apfst (cons (@{const_name All}, (x, T))) (strip_quantifiers t) 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

383 
 strip_quantifiers t = ([], t) 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

384 

8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

385 
fun contains_existentials t = exists (fn (Q, _) => Q = @{const_name Ex}) (fst (strip_quantifiers t)) 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

386 

8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

387 
fun mk_property qs t = 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

388 
let 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

389 
fun enclose (@{const_name Ex}, (x, T)) t = 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

390 
Const (@{const_name Quickcheck_Narrowing.exists}, (T > @{typ property}) > @{typ property}) 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

391 
$ Abs (x, T, t) 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

392 
 enclose (@{const_name All}, (x, T)) t = 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

393 
Const (@{const_name Quickcheck_Narrowing.all}, (T > @{typ property}) > @{typ property}) 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

394 
$ Abs (x, T, t) 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

395 
in 
45002
df36896aae0f
removing superfluous definition in the quickcheck narrowing invocation as the code generator now generates valid Haskell code with necessary type annotations without a separate definition
bulwahn
parents:
44926
diff
changeset

396 
fold_rev enclose qs (@{term Quickcheck_Narrowing.Property} $ t) 
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

397 
end 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

398 

8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

399 
fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) = 
43317  400 
Datatype.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) => 
401 
(t, mk_case_term ctxt (p  1) qs' c)) cs) 

43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

402 
 mk_case_term ctxt p ((@{const_name All}, (x, T)) :: qs') (Universal_Counterexample (t, c)) = 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

403 
if p = 0 then t else mk_case_term ctxt (p  1) qs' c 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

404 

45039
632a033616e9
adding postprocessing of terms to narrowingbased Quickcheck
bulwahn
parents:
45002
diff
changeset

405 
val post_process = (perhaps (try Quickcheck_Common.post_process_term)) o eval_finite_functions 
632a033616e9
adding postprocessing of terms to narrowingbased Quickcheck
bulwahn
parents:
45002
diff
changeset

406 

43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

407 
fun mk_terms ctxt qs result = 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

408 
let 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

409 
val 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

410 
ps = filter (fn (_, (@{const_name All}, _)) => true  _ => false) (map_index I qs) 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

411 
in 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

412 
map (fn (p, (_, (x, T))) => (x, mk_case_term ctxt p qs result)) ps 
45039
632a033616e9
adding postprocessing of terms to narrowingbased Quickcheck
bulwahn
parents:
45002
diff
changeset

413 
> map (apsnd post_process) 
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

414 
end 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

415 

8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

416 
fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) = 
41905  417 
let 
43585  418 
fun dest_result (Quickcheck.Result r) = r 
419 
val opts = 

420 
(limit_time, is_interactive, seconds (Config.get ctxt Quickcheck.timeout), 

421 
Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.size) 

42361  422 
val thy = Proof_Context.theory_of ctxt 
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

423 
val t' = fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) (Term.add_frees t []) t 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

424 
val pnf_t = make_pnf_term thy t' 
41905  425 
in 
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

426 
if Config.get ctxt allow_existentials andalso contains_existentials pnf_t then 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

427 
let 
43240
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset

428 
fun wrap f (qs, t) = 
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset

429 
let val (qs1, qs2) = split_list qs in 
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset

430 
apfst (map2 pair qs1) (f (qs2, t)) end 
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset

431 
val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I 
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset

432 
val (qs, prop_t) = finitize (strip_quantifiers pnf_t) 
43585  433 
val (counterexample, result) = dynamic_value_strict (true, opts) 
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

434 
(Existential_Counterexample.get, Existential_Counterexample.put, 
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

435 
"Narrowing_Generators.put_existential_counterexample") 
45002
df36896aae0f
removing superfluous definition in the quickcheck narrowing invocation as the code generator now generates valid Haskell code with necessary type annotations without a separate definition
bulwahn
parents:
44926
diff
changeset

436 
thy (apfst o Option.map o map_counterexample) (mk_property qs prop_t) 
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

437 
in 
43585  438 
Quickcheck.Result 
45002
df36896aae0f
removing superfluous definition in the quickcheck narrowing invocation as the code generator now generates valid Haskell code with necessary type annotations without a separate definition
bulwahn
parents:
44926
diff
changeset

439 
{counterexample = Option.map (mk_terms ctxt qs) counterexample, 
43585  440 
evaluation_terms = Option.map (K []) counterexample, 
441 
timings = #timings (dest_result result), reports = #reports (dest_result result)} 

43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset

442 
end 
43240
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset

443 
else 
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset

444 
let 
44241  445 
val t' = fold_rev absfree (Term.add_frees t []) t 
43240
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset

446 
fun wrap f t = list_abs (f (strip_abs t)) 
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset

447 
val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I 
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset

448 
fun ensure_testable t = 
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset

449 
Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t > fastype_of t) $ t 
43585  450 
val (counterexample, result) = dynamic_value_strict (false, opts) 
43240
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset

451 
(Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample") 
43379
8c4b383e5143
quickcheck_narrowing returns some timing information
bulwahn
parents:
43329
diff
changeset

452 
thy (apfst o Option.map o map) (ensure_testable (finitize t')) 
43240
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset

453 
in 
43585  454 
Quickcheck.Result 
45039
632a033616e9
adding postprocessing of terms to narrowingbased Quickcheck
bulwahn
parents:
45002
diff
changeset

455 
{counterexample = 
632a033616e9
adding postprocessing of terms to narrowingbased Quickcheck
bulwahn
parents:
45002
diff
changeset

456 
Option.map (((curry (op ~~)) (Term.add_free_names t [])) o map post_process) counterexample, 
43585  457 
evaluation_terms = Option.map (K []) counterexample, 
458 
timings = #timings (dest_result result), reports = #reports (dest_result result)} 

43240
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset

459 
end 
41905  460 
end; 
461 

43114
b9fca691addd
Quickcheck Narrowing only requires one compilation with GHC now
bulwahn
parents:
43079
diff
changeset

462 
fun test_goals ctxt (limit_time, is_interactive) insts goals = 
43314
a9090cabca14
adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
bulwahn
parents:
43308
diff
changeset

463 
if (not (getenv "ISABELLE_GHC" = "")) then 
a9090cabca14
adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
bulwahn
parents:
43308
diff
changeset

464 
let 
a9090cabca14
adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
bulwahn
parents:
43308
diff
changeset

465 
val correct_inst_goals = Quickcheck.instantiate_goals ctxt insts goals 
a9090cabca14
adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
bulwahn
parents:
43308
diff
changeset

466 
in 
43114
b9fca691addd
Quickcheck Narrowing only requires one compilation with GHC now
bulwahn
parents:
43079
diff
changeset

467 
Quickcheck.collect_results (test_term ctxt (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) [] 
43314
a9090cabca14
adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
bulwahn
parents:
43308
diff
changeset

468 
end 
a9090cabca14
adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
bulwahn
parents:
43308
diff
changeset

469 
else 
a9090cabca14
adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
bulwahn
parents:
43308
diff
changeset

470 
(if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message 
a9090cabca14
adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
bulwahn
parents:
43308
diff
changeset

471 
("Environment variable ISABELLE_GHC is not set. To use narrowingbased quickcheck, please set " 
43911
a1da544e2652
more information for the user how to deactivate quickcheck_narrowing if he does not want to use it
bulwahn
parents:
43910
diff
changeset

472 
^ "this variable to your GHC Haskell compiler in your settings file. " 
a1da544e2652
more information for the user how to deactivate quickcheck_narrowing if he does not want to use it
bulwahn
parents:
43910
diff
changeset

473 
^ "To deactivate narrowingbased quickcheck, set quickcheck_narrowing_active to false."); 
a1da544e2652
more information for the user how to deactivate quickcheck_narrowing if he does not want to use it
bulwahn
parents:
43910
diff
changeset

474 
[Quickcheck.empty_result]) 
43114
b9fca691addd
Quickcheck Narrowing only requires one compilation with GHC now
bulwahn
parents:
43079
diff
changeset

475 

43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

476 
(* setup *) 
41905  477 

44272  478 
val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K true); 
43878
eeb10fdd9535
changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
bulwahn
parents:
43850
diff
changeset

479 

41905  480 
val setup = 
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

481 
Code.datatype_interpretation ensure_partial_term_of 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

482 
#> Code.datatype_interpretation ensure_partial_term_of_code 
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset

483 
#> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype 
42258
79cb339d8989
changing ensure_sort_datatype call in narrowing quickcheck (missed in 1491b7209e76)
bulwahn
parents:
42214
diff
changeset

484 
(((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype)) 
43878
eeb10fdd9535
changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
bulwahn
parents:
43850
diff
changeset

485 
#> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals))) 
41905  486 

44272  487 
end; 