author  bulwahn 
Mon, 22 Mar 2010 08:30:13 +0100  
changeset 35879  99818df5b8f5 
parent 35875  b0d24a74b06b 
child 35880  2623b23e41fc 
permissions  rwrr 
33265  1 
(* Title: HOL/Tools/Predicate_Compile/predicate_compile_aux.ML 
2 
Author: Lukas Bulwahn, TU Muenchen 

33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

3 

33265  4 
Auxilary functions for predicate compiler. 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

5 
*) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

6 

35404  7 
(* FIXME proper signature! *) 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

8 

33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

9 
structure Predicate_Compile_Aux = 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

10 
struct 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

11 

34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

12 
(* general functions *) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

13 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

14 
fun apfst3 f (x, y, z) = (f x, y, z) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

15 
fun apsnd3 f (x, y, z) = (x, f y, z) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

16 
fun aptrd3 f (x, y, z) = (x, y, f z) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

17 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

18 
fun comb_option f (SOME x1, SOME x2) = SOME (f (x1, x2)) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

19 
 comb_option f (NONE, SOME x2) = SOME x2 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

20 
 comb_option f (SOME x1, NONE) = SOME x1 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

21 
 comb_option f (NONE, NONE) = NONE 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

22 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

23 
fun map2_optional f (x :: xs) (y :: ys) = (f x (SOME y)) :: (map2_optional f xs ys) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

24 
 map2_optional f (x :: xs) [] = (f x NONE) :: (map2_optional f xs []) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

25 
 map2_optional f [] [] = [] 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

26 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

27 
fun find_indices f xs = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

28 
map_filter (fn (i, true) => SOME i  (i, false) => NONE) (map_index (apsnd f) xs) 
33328
1d93dd8a02c9
moved datatype mode and string functions to the auxillary structure
bulwahn
parents:
33327
diff
changeset

29 

35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

30 
fun assert check = if check then () else error "Assertion failed!" 
33328
1d93dd8a02c9
moved datatype mode and string functions to the auxillary structure
bulwahn
parents:
33327
diff
changeset

31 
(* mode *) 
1d93dd8a02c9
moved datatype mode and string functions to the auxillary structure
bulwahn
parents:
33327
diff
changeset

32 

34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

33 
datatype mode = Bool  Input  Output  Pair of mode * mode  Fun of mode * mode 
33619
d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33473
diff
changeset

34 

33623
4ec42d38224f
changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned
bulwahn
parents:
33620
diff
changeset

35 
(* equality of instantiatedness with respect to equivalences: 
4ec42d38224f
changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned
bulwahn
parents:
33620
diff
changeset

36 
Pair Input Input == Input and Pair Output Output == Output *) 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

37 
fun eq_mode (Fun (m1, m2), Fun (m3, m4)) = eq_mode (m1, m3) andalso eq_mode (m2, m4) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

38 
 eq_mode (Pair (m1, m2), Pair (m3, m4)) = eq_mode (m1, m3) andalso eq_mode (m2, m4) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

39 
 eq_mode (Pair (m1, m2), Input) = eq_mode (m1, Input) andalso eq_mode (m2, Input) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

40 
 eq_mode (Pair (m1, m2), Output) = eq_mode (m1, Output) andalso eq_mode (m2, Output) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

41 
 eq_mode (Input, Pair (m1, m2)) = eq_mode (Input, m1) andalso eq_mode (Input, m2) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

42 
 eq_mode (Output, Pair (m1, m2)) = eq_mode (Output, m1) andalso eq_mode (Output, m2) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

43 
 eq_mode (Input, Input) = true 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

44 
 eq_mode (Output, Output) = true 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

45 
 eq_mode (Bool, Bool) = true 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

46 
 eq_mode _ = false 
33623
4ec42d38224f
changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned
bulwahn
parents:
33620
diff
changeset

47 

33619
d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33473
diff
changeset

48 
(* name: binder_modes? *) 
d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33473
diff
changeset

49 
fun strip_fun_mode (Fun (mode, mode')) = mode :: strip_fun_mode mode' 
d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33473
diff
changeset

50 
 strip_fun_mode Bool = [] 
d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33473
diff
changeset

51 
 strip_fun_mode _ = error "Bad mode for strip_fun_mode" 
d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33473
diff
changeset

52 

d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33473
diff
changeset

53 
fun dest_fun_mode (Fun (mode, mode')) = mode :: dest_fun_mode mode' 
d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33473
diff
changeset

54 
 dest_fun_mode mode = [mode] 
d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33473
diff
changeset

55 

d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33473
diff
changeset

56 
fun dest_tuple_mode (Pair (mode, mode')) = mode :: dest_tuple_mode mode' 
d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33473
diff
changeset

57 
 dest_tuple_mode _ = [] 
d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33473
diff
changeset

58 

35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

59 

c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

60 
fun all_modes_of_typ' (T as Type ("fun", _)) = 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

61 
let 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

62 
val (S, U) = strip_type T 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

63 
in 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

64 
if U = HOLogic.boolT then 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

65 
fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2) 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

66 
(map all_modes_of_typ' S) [Bool] 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

67 
else 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

68 
[Input, Output] 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

69 
end 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

70 
 all_modes_of_typ' (Type ("*", [T1, T2])) = 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

71 
map_product (curry Pair) (all_modes_of_typ' T1) (all_modes_of_typ' T2) 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

72 
 all_modes_of_typ' _ = [Input, Output] 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

73 

c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

74 
fun all_modes_of_typ (T as Type ("fun", _)) = 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

75 
let 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

76 
val (S, U) = strip_type T 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

77 
in 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

78 
if U = HOLogic.boolT then 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

79 
fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2) 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

80 
(map all_modes_of_typ' S) [Bool] 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

81 
else 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

82 
[Input, Output] 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

83 
end 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

84 
 all_modes_of_typ (Type ("bool", [])) = [Bool] 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

85 
 all_modes_of_typ T = all_modes_of_typ' T 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

86 

35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

87 
fun all_smodes_of_typ (T as Type ("fun", _)) = 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

88 
let 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

89 
val (S, U) = strip_type T 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

90 
fun all_smodes (Type ("*", [T1, T2])) = 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

91 
map_product (curry Pair) (all_smodes T1) (all_smodes T2) 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

92 
 all_smodes _ = [Input, Output] 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

93 
in 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

94 
if U = HOLogic.boolT then 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

95 
fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2) (map all_smodes S) [Bool] 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

96 
else 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

97 
error "all_smodes_of_typ: invalid type for predicate" 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

98 
end 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

99 
(* 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

100 
fun extract_params arg = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

101 
case fastype_of arg of 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

102 
(T as Type ("fun", _)) => 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

103 
(if (body_type T = HOLogic.boolT) then 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

104 
(case arg of 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

105 
Free _ => [arg]  _ => error "extract_params: Unexpected term") 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

106 
else []) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

107 
 (Type ("*", [T1, T2])) => 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

108 
let 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

109 
val (t1, t2) = HOLogic.dest_prod arg 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

110 
in 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

111 
extract_params t1 @ extract_params t2 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

112 
end 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

113 
 _ => [] 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

114 
*) 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

115 
fun ho_arg_modes_of mode = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

116 
let 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

117 
fun ho_arg_mode (m as Fun _) = [m] 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

118 
 ho_arg_mode (Pair (m1, m2)) = ho_arg_mode m1 @ ho_arg_mode m2 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

119 
 ho_arg_mode _ = [] 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

120 
in 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

121 
maps ho_arg_mode (strip_fun_mode mode) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

122 
end 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

123 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

124 
fun ho_args_of mode ts = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

125 
let 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

126 
fun ho_arg (Fun _) (SOME t) = [t] 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

127 
 ho_arg (Fun _) NONE = error "ho_arg_of" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

128 
 ho_arg (Pair (m1, m2)) (SOME (Const ("Pair", _) $ t1 $ t2)) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

129 
ho_arg m1 (SOME t1) @ ho_arg m2 (SOME t2) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

130 
 ho_arg (Pair (m1, m2)) NONE = ho_arg m1 NONE @ ho_arg m2 NONE 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

131 
 ho_arg _ _ = [] 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

132 
in 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

133 
flat (map2_optional ho_arg (strip_fun_mode mode) ts) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

134 
end 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

135 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

136 
(* temporary function should be replaced by unsplit_input or so? *) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

137 
fun replace_ho_args mode hoargs ts = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

138 
let 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

139 
fun replace (Fun _, _) (arg' :: hoargs') = (arg', hoargs') 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

140 
 replace (Pair (m1, m2), Const ("Pair", T) $ t1 $ t2) hoargs = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

141 
let 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

142 
val (t1', hoargs') = replace (m1, t1) hoargs 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

143 
val (t2', hoargs'') = replace (m2, t2) hoargs' 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

144 
in 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

145 
(Const ("Pair", T) $ t1' $ t2', hoargs'') 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

146 
end 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

147 
 replace (_, t) hoargs = (t, hoargs) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

148 
in 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

149 
fst (fold_map replace ((strip_fun_mode mode) ~~ ts) hoargs) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

150 
end 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

151 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

152 
fun ho_argsT_of mode Ts = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

153 
let 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

154 
fun ho_arg (Fun _) T = [T] 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

155 
 ho_arg (Pair (m1, m2)) (Type ("*", [T1, T2])) = ho_arg m1 T1 @ ho_arg m2 T2 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

156 
 ho_arg _ _ = [] 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

157 
in 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

158 
flat (map2 ho_arg (strip_fun_mode mode) Ts) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

159 
end 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

160 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

161 
(* splits mode and maps function to higherorder argument types *) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

162 
fun split_map_mode f mode ts = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

163 
let 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

164 
fun split_arg_mode' (m as Fun _) t = f m t 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

165 
 split_arg_mode' (Pair (m1, m2)) (Const ("Pair", _) $ t1 $ t2) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

166 
let 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

167 
val (i1, o1) = split_arg_mode' m1 t1 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

168 
val (i2, o2) = split_arg_mode' m2 t2 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

169 
in 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

170 
(comb_option HOLogic.mk_prod (i1, i2), comb_option HOLogic.mk_prod (o1, o2)) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

171 
end 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

172 
 split_arg_mode' m t = 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

173 
if eq_mode (m, Input) then (SOME t, NONE) 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

174 
else if eq_mode (m, Output) then (NONE, SOME t) 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

175 
else error "split_map_mode: mode and term do not match" 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

176 
in 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

177 
(pairself (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) ts) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

178 
end 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

179 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

180 
(* splits mode and maps function to higherorder argument types *) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

181 
fun split_map_modeT f mode Ts = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

182 
let 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

183 
fun split_arg_mode' (m as Fun _) T = f m T 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

184 
 split_arg_mode' (Pair (m1, m2)) (Type ("*", [T1, T2])) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

185 
let 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

186 
val (i1, o1) = split_arg_mode' m1 T1 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

187 
val (i2, o2) = split_arg_mode' m2 T2 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

188 
in 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

189 
(comb_option HOLogic.mk_prodT (i1, i2), comb_option HOLogic.mk_prodT (o1, o2)) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

190 
end 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

191 
 split_arg_mode' Input T = (SOME T, NONE) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

192 
 split_arg_mode' Output T = (NONE, SOME T) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

193 
 split_arg_mode' _ _ = error "split_modeT': mode and type do not match" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

194 
in 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

195 
(pairself (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) Ts) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

196 
end 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

197 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

198 
fun split_mode mode ts = split_map_mode (fn _ => fn _ => (NONE, NONE)) mode ts 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

199 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

200 
fun fold_map_aterms_prodT comb f (Type ("*", [T1, T2])) s = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

201 
let 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

202 
val (x1, s') = fold_map_aterms_prodT comb f T1 s 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

203 
val (x2, s'') = fold_map_aterms_prodT comb f T2 s' 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

204 
in 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

205 
(comb x1 x2, s'') 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

206 
end 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

207 
 fold_map_aterms_prodT comb f T s = f T s 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

208 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

209 
fun map_filter_prod f (Const ("Pair", _) $ t1 $ t2) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

210 
comb_option HOLogic.mk_prod (map_filter_prod f t1, map_filter_prod f t2) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

211 
 map_filter_prod f t = f t 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

212 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

213 
(* obviously, split_mode' and split_modeT' do not match? where does that cause problems? *) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

214 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

215 
fun split_modeT' mode Ts = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

216 
let 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

217 
fun split_arg_mode' (Fun _) T = ([], []) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

218 
 split_arg_mode' (Pair (m1, m2)) (Type ("*", [T1, T2])) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

219 
let 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

220 
val (i1, o1) = split_arg_mode' m1 T1 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

221 
val (i2, o2) = split_arg_mode' m2 T2 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

222 
in 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

223 
(i1 @ i2, o1 @ o2) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

224 
end 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

225 
 split_arg_mode' Input T = ([T], []) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

226 
 split_arg_mode' Output T = ([], [T]) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

227 
 split_arg_mode' _ _ = error "split_modeT': mode and type do not match" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

228 
in 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

229 
(pairself flat o split_list) (map2 split_arg_mode' (strip_fun_mode mode) Ts) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

230 
end 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

231 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

232 
fun string_of_mode mode = 
33619
d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33473
diff
changeset

233 
let 
d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33473
diff
changeset

234 
fun string_of_mode1 Input = "i" 
d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33473
diff
changeset

235 
 string_of_mode1 Output = "o" 
d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33473
diff
changeset

236 
 string_of_mode1 Bool = "bool" 
d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33473
diff
changeset

237 
 string_of_mode1 mode = "(" ^ (string_of_mode3 mode) ^ ")" 
33626
42f69386943a
new names for predicate functions in the predicate compiler
bulwahn
parents:
33623
diff
changeset

238 
and string_of_mode2 (Pair (m1, m2)) = string_of_mode3 m1 ^ " * " ^ string_of_mode2 m2 
33619
d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33473
diff
changeset

239 
 string_of_mode2 mode = string_of_mode1 mode 
d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33473
diff
changeset

240 
and string_of_mode3 (Fun (m1, m2)) = string_of_mode2 m1 ^ " => " ^ string_of_mode3 m2 
d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33473
diff
changeset

241 
 string_of_mode3 mode = string_of_mode2 mode 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

242 
in string_of_mode3 mode end 
33619
d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33473
diff
changeset

243 

34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

244 
fun ascii_string_of_mode mode' = 
33626
42f69386943a
new names for predicate functions in the predicate compiler
bulwahn
parents:
33623
diff
changeset

245 
let 
42f69386943a
new names for predicate functions in the predicate compiler
bulwahn
parents:
33623
diff
changeset

246 
fun ascii_string_of_mode' Input = "i" 
42f69386943a
new names for predicate functions in the predicate compiler
bulwahn
parents:
33623
diff
changeset

247 
 ascii_string_of_mode' Output = "o" 
42f69386943a
new names for predicate functions in the predicate compiler
bulwahn
parents:
33623
diff
changeset

248 
 ascii_string_of_mode' Bool = "b" 
42f69386943a
new names for predicate functions in the predicate compiler
bulwahn
parents:
33623
diff
changeset

249 
 ascii_string_of_mode' (Pair (m1, m2)) = 
42f69386943a
new names for predicate functions in the predicate compiler
bulwahn
parents:
33623
diff
changeset

250 
"P" ^ ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Pair m2 
42f69386943a
new names for predicate functions in the predicate compiler
bulwahn
parents:
33623
diff
changeset

251 
 ascii_string_of_mode' (Fun (m1, m2)) = 
42f69386943a
new names for predicate functions in the predicate compiler
bulwahn
parents:
33623
diff
changeset

252 
"F" ^ ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Fun m2 ^ "B" 
42f69386943a
new names for predicate functions in the predicate compiler
bulwahn
parents:
33623
diff
changeset

253 
and ascii_string_of_mode'_Fun (Fun (m1, m2)) = 
42f69386943a
new names for predicate functions in the predicate compiler
bulwahn
parents:
33623
diff
changeset

254 
ascii_string_of_mode' m1 ^ (if m2 = Bool then "" else "_" ^ ascii_string_of_mode'_Fun m2) 
42f69386943a
new names for predicate functions in the predicate compiler
bulwahn
parents:
33623
diff
changeset

255 
 ascii_string_of_mode'_Fun Bool = "B" 
42f69386943a
new names for predicate functions in the predicate compiler
bulwahn
parents:
33623
diff
changeset

256 
 ascii_string_of_mode'_Fun m = ascii_string_of_mode' m 
42f69386943a
new names for predicate functions in the predicate compiler
bulwahn
parents:
33623
diff
changeset

257 
and ascii_string_of_mode'_Pair (Pair (m1, m2)) = 
42f69386943a
new names for predicate functions in the predicate compiler
bulwahn
parents:
33623
diff
changeset

258 
ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Pair m2 
42f69386943a
new names for predicate functions in the predicate compiler
bulwahn
parents:
33623
diff
changeset

259 
 ascii_string_of_mode'_Pair m = ascii_string_of_mode' m 
42f69386943a
new names for predicate functions in the predicate compiler
bulwahn
parents:
33623
diff
changeset

260 
in ascii_string_of_mode'_Fun mode' end 
42f69386943a
new names for predicate functions in the predicate compiler
bulwahn
parents:
33623
diff
changeset

261 

34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

262 
(* premises *) 
33619
d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33473
diff
changeset

263 

34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

264 
datatype indprem = Prem of term  Negprem of term  Sidecond of term 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

265 
 Generator of (string * typ); 
33619
d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33473
diff
changeset

266 

33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

267 
(* general syntactic functions *) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

268 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

269 
(*Like dest_conj, but flattens conjunctions however nested*) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

270 
fun conjuncts_aux (Const ("op &", _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

271 
 conjuncts_aux t conjs = t::conjs; 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

272 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

273 
fun conjuncts t = conjuncts_aux t []; 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

274 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

275 
fun is_equationlike_term (Const ("==", _) $ _ $ _) = true 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

276 
 is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

277 
 is_equationlike_term _ = false 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

278 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

279 
val is_equationlike = is_equationlike_term o prop_of 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

280 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

281 
fun is_pred_equation_term (Const ("==", _) $ u $ v) = 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

282 
(fastype_of u = @{typ bool}) andalso (fastype_of v = @{typ bool}) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

283 
 is_pred_equation_term _ = false 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

284 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

285 
val is_pred_equation = is_pred_equation_term o prop_of 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

286 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

287 
fun is_intro_term constname t = 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

288 
the_default false (try (fn t => case fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl t))) of 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

289 
Const (c, _) => c = constname 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

290 
 _ => false) t) 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

291 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

292 
fun is_intro constname t = is_intro_term constname (prop_of t) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

293 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

294 
fun is_pred thy constname = 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

295 
let 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

296 
val T = (Sign.the_const_type thy constname) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

297 
in body_type T = @{typ "bool"} end; 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

298 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

299 
fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = HOLogic.boolT) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

300 
 is_predT _ = false 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

301 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

302 
(*** check if a term contains only constructor functions ***) 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

303 
(* TODO: another copy in the core! *) 
33623
4ec42d38224f
changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned
bulwahn
parents:
33620
diff
changeset

304 
(* FIXME: constructor terms are supposed to be seen in the way the code generator 
4ec42d38224f
changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned
bulwahn
parents:
33620
diff
changeset

305 
sees constructors.*) 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

306 
fun is_constrt thy = 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

307 
let 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

308 
val cnstrs = flat (maps 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

309 
(map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

310 
(Symtab.dest (Datatype.get_all thy))); 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

311 
fun check t = (case strip_comb t of 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

312 
(Free _, []) => true 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

313 
 (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

314 
(SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

315 
 _ => false) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

316 
 _ => false) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

317 
in check end; 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

318 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

319 
fun is_funtype (Type ("fun", [_, _])) = true 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

320 
 is_funtype _ = false; 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

321 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

322 
fun is_Type (Type _) = true 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

323 
 is_Type _ = false 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

324 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

325 
(* returns true if t is an application of an datatype constructor *) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

326 
(* which then consequently would be splitted *) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

327 
(* else false *) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

328 
(* 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

329 
fun is_constructor thy t = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

330 
if (is_Type (fastype_of t)) then 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

331 
(case DatatypePackage.get_datatype thy ((fst o dest_Type o fastype_of) t) of 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

332 
NONE => false 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

333 
 SOME info => (let 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

334 
val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

335 
val (c, _) = strip_comb t 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

336 
in (case c of 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

337 
Const (name, _) => name mem_string constr_consts 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

338 
 _ => false) end)) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

339 
else false 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

340 
*) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

341 

35224  342 
val is_constr = Code.is_constr; 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

343 

33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

344 
fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) = 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

345 
let 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

346 
val (xTs, t') = strip_ex t 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

347 
in 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

348 
((x, T) :: xTs, t') 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

349 
end 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

350 
 strip_ex t = ([], t) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

351 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

352 
fun focus_ex t nctxt = 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

353 
let 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

354 
val ((xs, Ts), t') = apfst split_list (strip_ex t) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

355 
val (xs', nctxt') = Name.variants xs nctxt; 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

356 
val ps' = xs' ~~ Ts; 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

357 
val vs = map Free ps'; 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

358 
val t'' = Term.subst_bounds (rev vs, t'); 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

359 
in ((ps', t''), nctxt') end; 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

360 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

361 
(* introduction rule combinators *) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

362 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

363 
(* combinators to apply a function to all literals of an introduction rules *) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

364 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

365 
fun map_atoms f intro = 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

366 
let 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

367 
val (literals, head) = Logic.strip_horn intro 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

368 
fun appl t = (case t of 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

369 
(@{term "Not"} $ t') => HOLogic.mk_not (f t') 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

370 
 _ => f t) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

371 
in 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

372 
Logic.list_implies 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

373 
(map (HOLogic.mk_Trueprop o appl o HOLogic.dest_Trueprop) literals, head) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

374 
end 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

375 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

376 
fun fold_atoms f intro s = 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

377 
let 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

378 
val (literals, head) = Logic.strip_horn intro 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

379 
fun appl t s = (case t of 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

380 
(@{term "Not"} $ t') => f t' s 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

381 
 _ => f t s) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

382 
in fold appl (map HOLogic.dest_Trueprop literals) s end 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

383 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

384 
fun fold_map_atoms f intro s = 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

385 
let 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

386 
val (literals, head) = Logic.strip_horn intro 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

387 
fun appl t s = (case t of 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

388 
(@{term "Not"} $ t') => apfst HOLogic.mk_not (f t' s) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

389 
 _ => f t s) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

390 
val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

391 
in 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

392 
(Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s') 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

393 
end; 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

394 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

395 
fun maps_premises f intro = 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

396 
let 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

397 
val (premises, head) = Logic.strip_horn intro 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

398 
in 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

399 
Logic.list_implies (maps f premises, head) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

400 
end 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

401 

35875  402 
fun map_concl f intro = 
403 
let 

404 
val (premises, head) = Logic.strip_horn intro 

405 
in 

406 
Logic.list_implies (premises, f head) 

407 
end 

408 

409 
(* combinators to apply a function to all basic parts of nested products *) 

410 

411 
fun map_products f (Const ("Pair", T) $ t1 $ t2) = 

412 
Const ("Pair", T) $ map_products f t1 $ map_products f t2 

413 
 map_products f t = f t 

35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

414 

c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

415 
(* split theorems of case expressions *) 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

416 

c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

417 
(* 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

418 
fun has_split_rule_cname @{const_name "nat_case"} = true 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

419 
 has_split_rule_cname @{const_name "list_case"} = true 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

420 
 has_split_rule_cname _ = false 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

421 

35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

422 
fun has_split_rule_term thy (Const (@{const_name "nat_case"}, _)) = true 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

423 
 has_split_rule_term thy (Const (@{const_name "list_case"}, _)) = true 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

424 
 has_split_rule_term thy _ = false 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

425 

c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

426 
fun has_split_rule_term' thy (Const (@{const_name "If"}, _)) = true 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

427 
 has_split_rule_term' thy (Const (@{const_name "Let"}, _)) = true 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

428 
 has_split_rule_term' thy c = has_split_rule_term thy c 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

429 

c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

430 
*) 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

431 
fun prepare_split_thm ctxt split_thm = 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

432 
(split_thm RS @{thm iffD2}) 
35624  433 
> Local_Defs.unfold ctxt [@{thm atomize_conjL[symmetric]}, 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

434 
@{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}] 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

435 

c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

436 
fun find_split_thm thy (Const (name, typ)) = 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

437 
let 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

438 
fun split_name str = 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

439 
case first_field "." str 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

440 
of (SOME (field, rest)) => field :: split_name rest 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

441 
 NONE => [str] 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

442 
val splitted_name = split_name name 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

443 
in 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

444 
if length splitted_name > 0 andalso 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

445 
String.isSuffix "_case" (List.last splitted_name) 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

446 
then 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

447 
(List.take (splitted_name, length splitted_name  1)) @ ["split"] 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

448 
> space_implode "." 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

449 
> PureThy.get_thm thy 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

450 
> SOME 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

451 
handle ERROR msg => NONE 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

452 
else NONE 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

453 
end 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

454 
 find_split_thm _ _ = NONE 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

455 

c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

456 

c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

457 
(* TODO: split rules for let and if are different *) 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

458 
fun find_split_thm' thy (Const (@{const_name "If"}, _)) = SOME @{thm split_if} 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

459 
 find_split_thm' thy (Const (@{const_name "Let"}, _)) = SOME @{thm refl} (* TODO *) 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

460 
 find_split_thm' thy c = find_split_thm thy c 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

461 

c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

462 
fun has_split_thm thy t = is_some (find_split_thm thy t) 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

463 

c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

464 
fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t) 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

465 

c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

466 

33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

467 
(* lifting term operations to theorems *) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

468 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

469 
fun map_term thy f th = 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

470 
Skip_Proof.make_thm thy (f (prop_of th)) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

471 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

472 
(* 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

473 
fun equals_conv lhs_cv rhs_cv ct = 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

474 
case Thm.term_of ct of 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

475 
Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

476 
 _ => error "equals_conv" 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

477 
*) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

478 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

479 
(* Different options for compiler *) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

480 

35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

481 
datatype compilation = Pred  Random  Depth_Limited  DSeq  Annotated 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

482 
 Pos_Random_DSeq  Neg_Random_DSeq 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

483 

c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

484 

c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

485 
fun negative_compilation_of Pos_Random_DSeq = Neg_Random_DSeq 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

486 
 negative_compilation_of Neg_Random_DSeq = Pos_Random_DSeq 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

487 
 negative_compilation_of c = c 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

488 

c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

489 
fun compilation_for_polarity false Pos_Random_DSeq = Neg_Random_DSeq 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

490 
 compilation_for_polarity _ c = c 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

491 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

492 
fun string_of_compilation c = case c of 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

493 
Pred => "" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

494 
 Random => "random" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

495 
 Depth_Limited => "depth limited" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

496 
 DSeq => "dseq" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

497 
 Annotated => "annotated" 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

498 
 Pos_Random_DSeq => "pos_random dseq" 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

499 
 Neg_Random_DSeq => "neg_random_dseq" 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

500 

34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

501 
(*datatype compilation_options = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

502 
Pred  Random of int  Depth_Limited of int  DSeq of int  Annotated*) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

503 

33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

504 
datatype options = Options of { 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

505 
expected_modes : (string * mode list) option, 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

506 
proposed_modes : (string * mode list) option, 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

507 
proposed_names : ((string * mode) * string) list, 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

508 
show_steps : bool, 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

509 
show_proof_trace : bool, 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

510 
show_intermediate_results : bool, 
33251  511 
show_mode_inference : bool, 
512 
show_modes : bool, 

33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

513 
show_compilation : bool, 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

514 
show_caught_failures : bool, 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

515 
skip_proof : bool, 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

516 
no_topmost_reordering : bool, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

517 
function_flattening : bool, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

518 
fail_safe_function_flattening : bool, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

519 
no_higher_order_predicate : string list, 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

520 
inductify : bool, 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

521 
compilation : compilation 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

522 
}; 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

523 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

524 
fun expected_modes (Options opt) = #expected_modes opt 
33752
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33626
diff
changeset

525 
fun proposed_modes (Options opt) = #proposed_modes opt 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

526 
fun proposed_names (Options opt) name mode = AList.lookup (eq_pair (op =) eq_mode) 
33623
4ec42d38224f
changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned
bulwahn
parents:
33620
diff
changeset

527 
(#proposed_names opt) (name, mode) 
33620
b6bf2dc5aed7
added interface of user proposals for names of generated constants
bulwahn
parents:
33619
diff
changeset

528 

33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

529 
fun show_steps (Options opt) = #show_steps opt 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

530 
fun show_intermediate_results (Options opt) = #show_intermediate_results opt 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

531 
fun show_proof_trace (Options opt) = #show_proof_trace opt 
33251  532 
fun show_modes (Options opt) = #show_modes opt 
533 
fun show_mode_inference (Options opt) = #show_mode_inference opt 

33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

534 
fun show_compilation (Options opt) = #show_compilation opt 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

535 
fun show_caught_failures (Options opt) = #show_caught_failures opt 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

536 

33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

537 
fun skip_proof (Options opt) = #skip_proof opt 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

538 

35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

539 
fun function_flattening (Options opt) = #function_flattening opt 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

540 
fun fail_safe_function_flattening (Options opt) = #fail_safe_function_flattening opt 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

541 
fun no_topmost_reordering (Options opt) = #no_topmost_reordering opt 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

542 
fun no_higher_order_predicate (Options opt) = #no_higher_order_predicate opt 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

543 

33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

544 
fun is_inductify (Options opt) = #inductify opt 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

545 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

546 
fun compilation (Options opt) = #compilation opt 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

547 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

548 
val default_options = Options { 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

549 
expected_modes = NONE, 
33752
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33626
diff
changeset

550 
proposed_modes = NONE, 
33623
4ec42d38224f
changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned
bulwahn
parents:
33620
diff
changeset

551 
proposed_names = [], 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

552 
show_steps = false, 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

553 
show_intermediate_results = false, 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

554 
show_proof_trace = false, 
33251  555 
show_modes = false, 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

556 
show_mode_inference = false, 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

557 
show_compilation = false, 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

558 
show_caught_failures = false, 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

559 
skip_proof = true, 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

560 
no_topmost_reordering = false, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

561 
function_flattening = false, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

562 
fail_safe_function_flattening = false, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

563 
no_higher_order_predicate = [], 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

564 
inductify = false, 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

565 
compilation = Pred 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

566 
} 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

567 

34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

568 
val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes", 
35381
5038f36b5ea1
adding no_topmost_reordering as new option to the code_pred command
bulwahn
parents:
35324
diff
changeset

569 
"show_mode_inference", "show_compilation", "skip_proof", "inductify", "no_function_flattening", 
5038f36b5ea1
adding no_topmost_reordering as new option to the code_pred command
bulwahn
parents:
35324
diff
changeset

570 
"no_topmost_reordering"] 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

571 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset

572 
val compilation_names = [("pred", Pred), 
35879
99818df5b8f5
reviving the classical depthlimited computation in the predicate compiler
bulwahn
parents:
35875
diff
changeset

573 
(*("random", Random),*) 
99818df5b8f5
reviving the classical depthlimited computation in the predicate compiler
bulwahn
parents:
35875
diff
changeset

574 
("depth_limited", Depth_Limited), (*("annotated", Annotated),*) 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35224
diff
changeset

575 
("dseq", DSeq), ("random_dseq", Pos_Random_DSeq)] 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

576 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

577 
fun print_step options s = 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

578 
if show_steps options then tracing s else () 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

579 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

580 
(* tuple processing *) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

581 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

582 
fun expand_tuples thy intro = 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

583 
let 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

584 
fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

585 
 rewrite_args (arg::args) (pats, intro_t, ctxt) = 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

586 
(case HOLogic.strip_tupleT (fastype_of arg) of 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

587 
(Ts as _ :: _ :: _) => 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

588 
let 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

589 
fun rewrite_arg' (Const ("Pair", _) $ _ $ t2, Type ("*", [_, T2])) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

590 
(args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt)) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

591 
 rewrite_arg' (t, Type ("*", [T1, T2])) (args, (pats, intro_t, ctxt)) = 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

592 
let 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

593 
val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

594 
val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2))) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

595 
val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

596 
val args' = map (Pattern.rewrite_term thy [pat] []) args 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

597 
in 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

598 
rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt')) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

599 
end 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

600 
 rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt)) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

601 
val (args', (pats, intro_t', ctxt')) = rewrite_arg' (arg, fastype_of arg) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

602 
(args, (pats, intro_t, ctxt)) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

603 
in 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

604 
rewrite_args args' (pats, intro_t', ctxt') 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

605 
end 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

606 
 _ => rewrite_args args (pats, intro_t, ctxt)) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

607 
fun rewrite_prem atom = 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

608 
let 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

609 
val (_, args) = strip_comb atom 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

610 
in rewrite_args args end 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

611 
val ctxt = ProofContext.init thy 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

612 
val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

613 
val intro_t = prop_of intro' 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

614 
val concl = Logic.strip_imp_concl intro_t 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

615 
val (p, args) = strip_comb (HOLogic.dest_Trueprop concl) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

616 
val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

617 
val (pats', intro_t', ctxt3) = 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

618 
fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

619 
fun rewrite_pat (ct1, ct2) = 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

620 
(ct1, cterm_of thy (Pattern.rewrite_term thy pats' [] (term_of ct2))) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

621 
val t_insts' = map rewrite_pat t_insts 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

622 
val intro'' = Thm.instantiate (T_insts, t_insts') intro 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

623 
val [intro'''] = Variable.export ctxt3 ctxt [intro''] 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

624 
val intro'''' = Simplifier.full_simplify 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

625 
(HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

626 
intro''' 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

627 
(* splitting conjunctions introduced by Pair_eq*) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

628 
fun split_conj prem = 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

629 
map HOLogic.mk_Trueprop (conjuncts (HOLogic.dest_Trueprop prem)) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

630 
val intro''''' = map_term thy (maps_premises split_conj) intro'''' 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

631 
in 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

632 
intro''''' 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

633 
end 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

634 

35875  635 
(* eta contract higherorder arguments *) 
636 

637 

638 
fun eta_contract_ho_arguments thy intro = 

639 
let 

640 
fun f atom = list_comb (apsnd ((map o map_products) Envir.eta_contract) (strip_comb atom)) 

641 
in 

642 
map_term thy (map_concl f o map_atoms f) intro 

643 
end 

644 

645 

33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

646 
end; 