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

32667  3 

33265  4 
A compiler from predicates specified by intro/elim rules to equations. 
32667  5 
*) 
6 

7 
signature PREDICATE_COMPILE_CORE = 

8 
sig 

33478
b70fe083694d
moved values command from core to predicate compile
bulwahn
parents:
33476
diff
changeset

9 
val setup : theory > theory 
b70fe083694d
moved values command from core to predicate compile
bulwahn
parents:
33476
diff
changeset

10 
val code_pred : Predicate_Compile_Aux.options > string > Proof.context > Proof.state 
b70fe083694d
moved values command from core to predicate compile
bulwahn
parents:
33476
diff
changeset

11 
val code_pred_cmd : Predicate_Compile_Aux.options > string > Proof.context > Proof.state 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

12 
val values_cmd : string list > Predicate_Compile_Aux.mode option list option 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

13 
> (string option * (Predicate_Compile_Aux.compilation * int list)) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

14 
> int > string > Toplevel.state > unit 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

15 
val register_predicate : (string * thm list * thm) > theory > theory 
33146
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33145
diff
changeset

16 
val register_intros : string * thm list > theory > theory 
32667  17 
val is_registered : theory > string > bool 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

18 
val function_name_of : Predicate_Compile_Aux.compilation > theory 
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:
35267
diff
changeset

19 
> string > bool * Predicate_Compile_Aux.mode > string 
33328
1d93dd8a02c9
moved datatype mode and string functions to the auxillary structure
bulwahn
parents:
33327
diff
changeset

20 
val predfun_intro_of: theory > string > Predicate_Compile_Aux.mode > thm 
1d93dd8a02c9
moved datatype mode and string functions to the auxillary structure
bulwahn
parents:
33327
diff
changeset

21 
val predfun_elim_of: theory > string > Predicate_Compile_Aux.mode > thm 
32667  22 
val all_preds_of : theory > string list 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

23 
val modes_of: Predicate_Compile_Aux.compilation 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

24 
> theory > string > Predicate_Compile_Aux.mode list 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

25 
val all_modes_of : Predicate_Compile_Aux.compilation 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

26 
> theory > (string * Predicate_Compile_Aux.mode list) list 
33484
e96a0c52d74b
renamed generator to random_function in the predicate compiler
bulwahn
parents:
33483
diff
changeset

27 
val all_random_modes_of : theory > (string * Predicate_Compile_Aux.mode list) list 
33478
b70fe083694d
moved values command from core to predicate compile
bulwahn
parents:
33476
diff
changeset

28 
val intros_of : theory > string > thm list 
b70fe083694d
moved values command from core to predicate compile
bulwahn
parents:
33476
diff
changeset

29 
val add_intro : thm > theory > theory 
b70fe083694d
moved values command from core to predicate compile
bulwahn
parents:
33476
diff
changeset

30 
val set_elim : thm > theory > theory 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

31 
val preprocess_intro : theory > thm > thm 
33478
b70fe083694d
moved values command from core to predicate compile
bulwahn
parents:
33476
diff
changeset

32 
val print_stored_rules : theory > unit 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

33 
val print_all_modes : Predicate_Compile_Aux.compilation > theory > unit 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

34 
val mk_casesrule : Proof.context > term > thm list > term 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

35 

33137
0d16c07f8d24
added option to generate random values to values command in the predicate compiler
bulwahn
parents:
33135
diff
changeset

36 
val eval_ref : (unit > term Predicate.pred) option Unsynchronized.ref 
33482
5029ec373036
strictly respecting the line margin in the predicate compiler core
bulwahn
parents:
33479
diff
changeset

37 
val random_eval_ref : (unit > int * int > term Predicate.pred * (int * int)) 
5029ec373036
strictly respecting the line margin in the predicate compiler core
bulwahn
parents:
33479
diff
changeset

38 
option Unsynchronized.ref 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

39 
val dseq_eval_ref : (unit > term DSequence.dseq) option Unsynchronized.ref 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

40 
val random_dseq_eval_ref : (unit > int > int > int * int > term DSequence.dseq * (int * int)) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

41 
option Unsynchronized.ref 
33628  42 
val code_pred_intro_attrib : attribute 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

43 

32667  44 
(* used by Quickcheck_Generator *) 
45 
(* temporary for testing of the compilation *) 

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

46 

32667  47 
datatype compilation_funs = CompilationFuns of { 
48 
mk_predT : typ > typ, 

49 
dest_predT : typ > typ, 

50 
mk_bot : typ > term, 

51 
mk_single : term > term, 

52 
mk_bind : term * term > term, 

53 
mk_sup : term * term > term, 

54 
mk_if : term > term, 

55 
mk_not : term > term, 

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

56 
mk_map : typ > typ > term > term > term 
33140
83951822bfd0
cleaning the signature of the predicate compiler core; renaming signature and structures to uniform long names
bulwahn
parents:
33139
diff
changeset

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

58 

32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32671
diff
changeset

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

60 
val randompred_compfuns : compilation_funs 
33256
b350516cb1f9
adding a prototype of a counterexample generator based on the predicate compiler to HOL/ex
bulwahn
parents:
33251
diff
changeset

61 
val add_equations : Predicate_Compile_Aux.options > string list > theory > theory 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

62 
val add_random_dseq_equations : Predicate_Compile_Aux.options > string list > theory > theory 
33473
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
33377
diff
changeset

63 
val mk_tracing : string > term > term 
32667  64 
end; 
65 

66 
structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE = 

67 
struct 

68 

32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32667
diff
changeset

69 
open Predicate_Compile_Aux; 
33144
1831516747d4
removed obsolete GeneratorPrem; cleanup after modularization; tuned
bulwahn
parents:
33143
diff
changeset

70 

32667  71 
(** auxiliary **) 
72 

73 
(* debug stuff *) 

74 

33108
9d9afd478016
added test for higherorder function inductification; added debug messages
bulwahn
parents:
33106
diff
changeset

75 
fun print_tac s = Seq.single; 
33139
9c01ee6f8ee9
added skip_proof option; playing with compilation of depthlimited predicates
bulwahn
parents:
33138
diff
changeset

76 

33127  77 
fun print_tac' options s = 
78 
if show_proof_trace options then Tactical.print_tac s else Seq.single; 

79 

32667  80 
fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *) 
81 

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

82 
fun assert b = if not b then error "Assertion failed" else warning "Assertion holds" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

83 

33108
9d9afd478016
added test for higherorder function inductification; added debug messages
bulwahn
parents:
33106
diff
changeset

84 
datatype assertion = Max_number_of_subgoals of int 
9d9afd478016
added test for higherorder function inductification; added debug messages
bulwahn
parents:
33106
diff
changeset

85 
fun assert_tac (Max_number_of_subgoals i) st = 
9d9afd478016
added test for higherorder function inductification; added debug messages
bulwahn
parents:
33106
diff
changeset

86 
if (nprems_of st <= i) then Seq.single st 
9d9afd478016
added test for higherorder function inductification; added debug messages
bulwahn
parents:
33106
diff
changeset

87 
else error ("assert_tac: Numbers of subgoals mismatch at goal state :" 
9d9afd478016
added test for higherorder function inductification; added debug messages
bulwahn
parents:
33106
diff
changeset

88 
^ "\n" ^ Pretty.string_of (Pretty.chunks 
9d9afd478016
added test for higherorder function inductification; added debug messages
bulwahn
parents:
33106
diff
changeset

89 
(Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st))); 
9d9afd478016
added test for higherorder function inductification; added debug messages
bulwahn
parents:
33106
diff
changeset

90 

32667  91 
(** fundamentals **) 
92 

93 
(* syntactic operations *) 

94 

95 
fun mk_eq (x, xs) = 

96 
let fun mk_eqs _ [] = [] 

97 
 mk_eqs a (b::cs) = 

98 
HOLogic.mk_eq (Free (a, fastype_of b), b) :: mk_eqs a cs 

99 
in mk_eqs x xs end; 

100 

101 
fun mk_scomp (t, u) = 

102 
let 

103 
val T = fastype_of t 

104 
val U = fastype_of u 

105 
val [A] = binder_types T 

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

106 
val D = body_type U 
32667  107 
in 
108 
Const (@{const_name "scomp"}, T > U > A > D) $ t $ u 

109 
end; 

110 

111 
fun dest_funT (Type ("fun",[S, T])) = (S, T) 

112 
 dest_funT T = raise TYPE ("dest_funT", [T], []) 

113 

114 
fun mk_fun_comp (t, u) = 

115 
let 

116 
val (_, B) = dest_funT (fastype_of t) 

117 
val (C, A) = dest_funT (fastype_of u) 

118 
in 

119 
Const(@{const_name "Fun.comp"}, (A > B) > (C > A) > C > B) $ t $ u 

120 
end; 

121 

122 
fun dest_randomT (Type ("fun", [@{typ Random.seed}, 

32674
b629fbcc5313
merged; adopted to changes from Code_Evaluation in the predicate compiler
bulwahn
parents:
32673
diff
changeset

123 
Type ("*", [Type ("*", [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T 
32667  124 
 dest_randomT T = raise TYPE ("dest_randomT", [T], []) 
125 

33473
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
33377
diff
changeset

126 
fun mk_tracing s t = 
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
33377
diff
changeset

127 
Const(@{const_name Code_Evaluation.tracing}, 
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
33377
diff
changeset

128 
@{typ String.literal} > (fastype_of t) > (fastype_of t)) $ (HOLogic.mk_literal s) $ t 
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
33377
diff
changeset

129 

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

130 
val strip_intro_concl = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

131 

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

132 
(* derivation trees for modes of premises *) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

133 

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

134 
datatype mode_derivation = Mode_App of mode_derivation * mode_derivation  Context of mode 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

135 
 Mode_Pair of mode_derivation * mode_derivation  Term of mode 
32667  136 

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

137 
fun string_of_derivation (Mode_App (m1, m2)) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

138 
"App (" ^ string_of_derivation m1 ^ ", " ^ string_of_derivation m2 ^ ")" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

139 
 string_of_derivation (Mode_Pair (m1, m2)) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

140 
"Pair (" ^ string_of_derivation m1 ^ ", " ^ string_of_derivation m2 ^ ")" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

141 
 string_of_derivation (Term m) = "Term (" ^ string_of_mode m ^ ")" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

142 
 string_of_derivation (Context m) = "Context (" ^ string_of_mode m ^ ")" 
32667  143 

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

144 
fun strip_mode_derivation deriv = 
32667  145 
let 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

146 
fun strip (Mode_App (deriv1, deriv2)) ds = strip deriv1 (deriv2 :: ds) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

147 
 strip deriv ds = (deriv, ds) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

149 
strip deriv [] 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

151 

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

152 
fun mode_of (Context m) = m 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

153 
 mode_of (Term m) = m 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

154 
 mode_of (Mode_App (d1, d2)) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

155 
(case mode_of d1 of Fun (m, m') => 
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:
35267
diff
changeset

156 
(if eq_mode (m, mode_of d2) then m' else error "mode_of") 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

157 
 _ => error "mode_of2") 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

158 
 mode_of (Mode_Pair (d1, d2)) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

159 
Pair (mode_of d1, mode_of d2) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

160 

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

161 
fun head_mode_of deriv = mode_of (fst (strip_mode_derivation deriv)) 
32667  162 

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

163 
fun param_derivations_of deriv = 
32667  164 
let 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

165 
val (_, argument_derivs) = strip_mode_derivation deriv 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

166 
fun param_derivation (Mode_Pair (m1, m2)) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

167 
param_derivation m1 @ param_derivation m2 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

168 
 param_derivation (Term _) = [] 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

169 
 param_derivation m = [m] 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

171 
maps param_derivation argument_derivs 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

172 
end 
32667  173 

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

174 
fun collect_context_modes (Mode_App (m1, m2)) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

175 
collect_context_modes m1 @ collect_context_modes m2 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

176 
 collect_context_modes (Mode_Pair (m1, m2)) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

177 
collect_context_modes m1 @ collect_context_modes m2 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

178 
 collect_context_modes (Context m) = [m] 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

179 
 collect_context_modes (Term _) = [] 
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32667
diff
changeset

180 

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

181 
(* representation of inferred clauses with modes *) 
32667  182 

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

183 
type moded_clause = term list * (indprem * mode_derivation) list 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

184 

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:
35267
diff
changeset

185 
type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list 
32667  186 

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

187 
(* bookkeeping *) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

188 

32667  189 
datatype predfun_data = PredfunData of { 
190 
definition : thm, 

191 
intro : thm, 

192 
elim : thm 

193 
}; 

194 

195 
fun rep_predfun_data (PredfunData data) = data; 

196 

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

197 
fun mk_predfun_data (definition, intro, elim) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

198 
PredfunData {definition = definition, intro = intro, elim = elim} 
32667  199 

200 
datatype pred_data = PredData of { 

201 
intros : thm list, 

202 
elim : thm option, 

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

203 
function_names : (compilation * (mode * string) list) list, 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

204 
predfun_data : (mode * predfun_data) list, 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

205 
needs_random : mode list 
32667  206 
}; 
207 

208 
fun rep_pred_data (PredData data) = data; 

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

209 

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

210 
fun mk_pred_data ((intros, elim), (function_names, predfun_data, needs_random)) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

211 
PredData {intros = intros, elim = elim, 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

212 
function_names = function_names, predfun_data = predfun_data, needs_random = needs_random} 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

213 

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

214 
fun map_pred_data f (PredData {intros, elim, function_names, predfun_data, needs_random}) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

215 
mk_pred_data (f ((intros, elim), (function_names, predfun_data, needs_random))) 
33144
1831516747d4
removed obsolete GeneratorPrem; cleanup after modularization; tuned
bulwahn
parents:
33143
diff
changeset

216 

32667  217 
fun eq_option eq (NONE, NONE) = true 
218 
 eq_option eq (SOME x, SOME y) = eq (x, y) 

219 
 eq_option eq _ = false 

33144
1831516747d4
removed obsolete GeneratorPrem; cleanup after modularization; tuned
bulwahn
parents:
33143
diff
changeset

220 

32667  221 
fun eq_pred_data (PredData d1, PredData d2) = 
222 
eq_list (Thm.eq_thm) (#intros d1, #intros d2) andalso 

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

223 
eq_option (Thm.eq_thm) (#elim d1, #elim d2) 
33144
1831516747d4
removed obsolete GeneratorPrem; cleanup after modularization; tuned
bulwahn
parents:
33143
diff
changeset

224 

33522  225 
structure PredData = Theory_Data 
32667  226 
( 
227 
type T = pred_data Graph.T; 

228 
val empty = Graph.empty; 

229 
val extend = I; 

33522  230 
val merge = Graph.merge eq_pred_data; 
32667  231 
); 
232 

233 
(* queries *) 

234 

235 
fun lookup_pred_data thy name = 

236 
Option.map rep_pred_data (try (Graph.get_node (PredData.get thy)) name) 

237 

238 
fun the_pred_data thy name = case lookup_pred_data thy name 

239 
of NONE => error ("No such predicate " ^ quote name) 

240 
 SOME data => data; 

241 

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

242 
val is_registered = is_some oo lookup_pred_data 
32667  243 

244 
val all_preds_of = Graph.keys o PredData.get 

245 

246 
fun intros_of thy = map (Thm.transfer thy) o #intros o the_pred_data thy 

247 

248 
fun the_elim_of thy name = case #elim (the_pred_data thy name) 

249 
of NONE => error ("No elimination rule for predicate " ^ quote name) 

250 
 SOME thm => Thm.transfer thy thm 

251 

252 
val has_elim = is_some o #elim oo the_pred_data; 

253 

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

254 
fun function_names_of compilation thy name = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

255 
case AList.lookup (op =) (#function_names (the_pred_data thy name)) compilation of 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

256 
NONE => error ("No " ^ string_of_compilation compilation 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

257 
^ "functions defined for predicate " ^ quote name) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

258 
 SOME fun_names => fun_names 
32667  259 

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:
35267
diff
changeset

260 
fun function_name_of compilation thy name (pol, mode) = 
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:
35267
diff
changeset

261 
case AList.lookup eq_mode 
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:
35267
diff
changeset

262 
(function_names_of (compilation_for_polarity pol compilation) thy name) mode of 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

263 
NONE => error ("No " ^ string_of_compilation compilation 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

264 
^ "function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

265 
 SOME function_name => function_name 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

266 

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

267 
fun modes_of compilation thy name = map fst (function_names_of compilation thy name) 
32667  268 

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

269 
fun all_modes_of compilation thy = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

270 
map_filter (fn name => Option.map (pair name) (try (modes_of compilation thy) name)) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

271 
(all_preds_of thy) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

272 

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

273 
val all_random_modes_of = all_modes_of Random 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

274 

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

275 
fun defined_functions compilation thy name = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

276 
AList.defined (op =) (#function_names (the_pred_data thy name)) compilation 
32667  277 

278 
fun lookup_predfun_data thy name mode = 

33483
a15a2f7f7560
improved handling of already defined functions in the predicate compiler; could cause trouble before when no modes for a predicate were infered
bulwahn
parents:
33482
diff
changeset

279 
Option.map rep_predfun_data 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

280 
(AList.lookup (op =) (#predfun_data (the_pred_data thy name)) mode) 
32667  281 

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

282 
fun the_predfun_data thy name mode = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

283 
case lookup_predfun_data thy name mode of 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

284 
NONE => error ("No function defined for mode " ^ string_of_mode mode ^ 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

285 
" of predicate " ^ name) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

286 
 SOME data => data; 
32667  287 

288 
val predfun_definition_of = #definition ooo the_predfun_data 

289 

290 
val predfun_intro_of = #intro ooo the_predfun_data 

291 

292 
val predfun_elim_of = #elim ooo the_predfun_data 

293 

294 
(* diagnostic display functions *) 

295 

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

296 
fun print_modes options thy modes = 
33251  297 
if show_modes options then 
33326
7d0288d90535
improved handling of alternative rules; added test cases for alternative rules; normalized tracing in the predicate compiler
bulwahn
parents:
33268
diff
changeset

298 
tracing ("Inferred modes:\n" ^ 
33251  299 
cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map 
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:
35267
diff
changeset

300 
(fn (p, m) => string_of_mode m ^ (if p then "pos" else "neg")) ms)) modes)) 
33251  301 
else () 
32667  302 

303 
fun print_pred_mode_table string_of_entry thy pred_mode_table = 

304 
let 

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:
35267
diff
changeset

305 
fun print_mode pred ((pol, mode), entry) = "mode : " ^ 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:
33526
diff
changeset

306 
^ string_of_entry pred mode entry 
32667  307 
fun print_pred (pred, modes) = 
308 
"predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes) 

33326
7d0288d90535
improved handling of alternative rules; added test cases for alternative rules; normalized tracing in the predicate compiler
bulwahn
parents:
33268
diff
changeset

309 
val _ = tracing (cat_lines (map print_pred pred_mode_table)) 
32667  310 
in () end; 
311 

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

312 
fun string_of_prem thy (Prem t) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

313 
(Syntax.string_of_term_global thy t) ^ "(premise)" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

314 
 string_of_prem thy (Negprem t) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

315 
(Syntax.string_of_term_global thy (HOLogic.mk_not t)) ^ "(negative premise)" 
33130
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33129
diff
changeset

316 
 string_of_prem thy (Sidecond t) = 
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33129
diff
changeset

317 
(Syntax.string_of_term_global thy t) ^ "(sidecondition)" 
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33129
diff
changeset

318 
 string_of_prem thy _ = error "string_of_prem: unexpected input" 
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33129
diff
changeset

319 

7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33129
diff
changeset

320 
fun string_of_clause thy pred (ts, prems) = 
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33129
diff
changeset

321 
(space_implode " > " 
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33129
diff
changeset

322 
(map (string_of_prem thy) prems)) ^ " > " ^ pred ^ " " 
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33129
diff
changeset

323 
^ (space_implode " " (map (Syntax.string_of_term_global thy) ts)) 
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33129
diff
changeset

324 

33139
9c01ee6f8ee9
added skip_proof option; playing with compilation of depthlimited predicates
bulwahn
parents:
33138
diff
changeset

325 
fun print_compiled_terms options thy = 
9c01ee6f8ee9
added skip_proof option; playing with compilation of depthlimited predicates
bulwahn
parents:
33138
diff
changeset

326 
if show_compilation options then 
9c01ee6f8ee9
added skip_proof option; playing with compilation of depthlimited predicates
bulwahn
parents:
33138
diff
changeset

327 
print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term_global thy) thy 
9c01ee6f8ee9
added skip_proof option; playing with compilation of depthlimited predicates
bulwahn
parents:
33138
diff
changeset

328 
else K () 
9c01ee6f8ee9
added skip_proof option; playing with compilation of depthlimited predicates
bulwahn
parents:
33138
diff
changeset

329 

32667  330 
fun print_stored_rules thy = 
331 
let 

332 
val preds = (Graph.keys o PredData.get) thy 

333 
fun print pred () = let 

334 
val _ = writeln ("predicate: " ^ pred) 

335 
val _ = writeln ("introrules: ") 

336 
val _ = fold (fn thm => fn u => writeln (Display.string_of_thm_global thy thm)) 

337 
(rev (intros_of thy pred)) () 

338 
in 

339 
if (has_elim thy pred) then 

340 
writeln ("elimrule: " ^ Display.string_of_thm_global thy (the_elim_of thy pred)) 

341 
else 

342 
writeln ("no elimrule defined") 

343 
end 

344 
in 

345 
fold print preds () 

346 
end; 

347 

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

348 
fun print_all_modes compilation thy = 
32667  349 
let 
350 
val _ = writeln ("Inferred modes:") 

351 
fun print (pred, modes) u = 

352 
let 

353 
val _ = writeln ("predicate: " ^ pred) 

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

354 
val _ = writeln ("modes: " ^ (commas (map string_of_mode modes))) 
33619
d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33526
diff
changeset

355 
in u end 
32667  356 
in 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

357 
fold print (all_modes_of compilation thy) () 
32667  358 
end 
33129
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

359 

33132
07efd452a698
moved argument expected_modes into options; improved mode check to only check mode of the named predicate
bulwahn
parents:
33131
diff
changeset

360 
(* validity checks *) 
33752
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

361 
(* EXPECTED MODE and PROPOSED_MODE are largely the same; define a clear semantics for those! *) 
33132
07efd452a698
moved argument expected_modes into options; improved mode check to only check mode of the named predicate
bulwahn
parents:
33131
diff
changeset

362 

33752
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

363 
fun check_expected_modes preds options modes = 
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

364 
case expected_modes options of 
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

365 
SOME (s, ms) => (case AList.lookup (op =) modes s of 
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

366 
SOME modes => 
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

367 
let 
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:
35267
diff
changeset

368 
val modes' = map snd modes 
33752
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

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

370 
if not (eq_set eq_mode (ms, modes')) then 
33752
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

371 
error ("expected modes were not inferred:\n" 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

372 
^ " inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes') ^ "\n" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

373 
^ " expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms)) 
33752
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

374 
else () 
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

375 
end 
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

376 
 NONE => ()) 
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

377 
 NONE => () 
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

378 

9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

379 
fun check_proposed_modes preds options modes extra_modes errors = 
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

380 
case proposed_modes options of 
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

381 
SOME (s, ms) => (case AList.lookup (op =) modes s of 
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

382 
SOME inferred_ms => 
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

383 
let 
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

384 
val preds_without_modes = map fst (filter (null o snd) (modes @ extra_modes)) 
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:
35267
diff
changeset

385 
val modes' = map snd inferred_ms 
33752
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

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

387 
if not (eq_set eq_mode (ms, modes')) then 
33752
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

388 
error ("expected modes were not inferred:\n" 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

389 
^ " inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes') ^ "\n" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

390 
^ " expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms) ^ "\n" 
33752
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

391 
^ "For the following clauses, the following modes could not be inferred: " ^ "\n" 
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

392 
^ cat_lines errors ^ 
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

393 
(if not (null preds_without_modes) then 
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

394 
"\n" ^ "No mode inferred for the predicates " ^ commas preds_without_modes 
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

395 
else "")) 
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

396 
else () 
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

397 
end 
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

398 
 NONE => ()) 
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

399 
 NONE => () 
33132
07efd452a698
moved argument expected_modes into options; improved mode check to only check mode of the named predicate
bulwahn
parents:
33131
diff
changeset

400 

33144
1831516747d4
removed obsolete GeneratorPrem; cleanup after modularization; tuned
bulwahn
parents:
33143
diff
changeset

401 
(* importing introduction rules *) 
33129
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

402 

3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

403 
fun unify_consts thy cs intr_ts = 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

404 
(let 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

405 
val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c  _ => I); 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

406 
fun varify (t, (i, ts)) = 
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35411
diff
changeset

407 
let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify_global [] t)) 
33129
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

408 
in (maxidx_of_term t', t'::ts) end; 
33150
75eddea4abef
further changes due to the previous merge in the predicate compiler
bulwahn
parents:
33149
diff
changeset

409 
val (i, cs') = List.foldr varify (~1, []) cs; 
75eddea4abef
further changes due to the previous merge in the predicate compiler
bulwahn
parents:
33149
diff
changeset

410 
val (i', intr_ts') = List.foldr varify (i, []) intr_ts; 
33129
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

411 
val rec_consts = fold add_term_consts_2 cs' []; 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

412 
val intr_consts = fold add_term_consts_2 intr_ts' []; 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

413 
fun unify (cname, cT) = 
33317  414 
let val consts = map snd (filter (fn c => fst c = cname) intr_consts) 
33129
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

415 
in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end; 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

416 
val (env, _) = fold unify rec_consts (Vartab.empty, i'); 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

417 
val subst = map_types (Envir.norm_type env) 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

418 
in (map subst cs', map subst intr_ts') 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

419 
end) handle Type.TUNIFY => 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

420 
(warning "Occurrences of recursive constant have nonunifiable types"; (cs, intr_ts)); 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

421 

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

422 
fun import_intros inp_pred [] ctxt = 
33146
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33145
diff
changeset

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

424 
val ([outp_pred], ctxt') = Variable.import_terms true [inp_pred] ctxt 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

425 
val T = fastype_of outp_pred 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

426 
(* TODO: put in a function for this next line! *) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

427 
val paramTs = ho_argsT_of (hd (all_modes_of_typ T)) (binder_types T) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

428 
val (param_names, ctxt'') = Variable.variant_fixes 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

429 
(map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt' 
33629
5f35cf91c6a4
improving code quality thanks to Florian's code review
bulwahn
parents:
33628
diff
changeset

430 
val params = map2 (curry Free) param_names paramTs 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

432 
(((outp_pred, params), []), ctxt') 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

434 
 import_intros inp_pred (th :: ths) ctxt = 
33129
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

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

436 
val ((_, [th']), ctxt') = Variable.import true [th] ctxt 
33129
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

437 
val thy = ProofContext.theory_of ctxt' 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

438 
val (pred, args) = strip_intro_concl th' 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

439 
val T = fastype_of pred 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

440 
val ho_args = ho_args_of (hd (all_modes_of_typ T)) args 
33146
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33145
diff
changeset

441 
fun subst_of (pred', pred) = 
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33145
diff
changeset

442 
let 
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33145
diff
changeset

443 
val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty 
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33145
diff
changeset

444 
in map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) end 
33129
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

445 
fun instantiate_typ th = 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

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

447 
val (pred', _) = strip_intro_concl th 
33129
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

448 
val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

449 
error "Trying to instantiate another predicate" else () 
33146
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33145
diff
changeset

450 
in Thm.certify_instantiate (subst_of (pred', pred), []) th end; 
33129
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

451 
fun instantiate_ho_args th = 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

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

453 
val (_, args') = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of) th 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

454 
val ho_args' = map dest_Var (ho_args_of (hd (all_modes_of_typ T)) args') 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

455 
in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end 
33146
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33145
diff
changeset

456 
val outp_pred = 
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33145
diff
changeset

457 
Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred 
33129
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

458 
val ((_, ths'), ctxt1) = 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

459 
Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt' 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

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

461 
(((outp_pred, ho_args), th' :: ths'), ctxt1) 
33129
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

462 
end 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

463 

3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

464 
(* generation of case rules from usergiven introduction rules *) 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

465 

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

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

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

468 
val (t1, st') = mk_args2 T1 st 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

469 
val (t2, st'') = mk_args2 T2 st' 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

471 
(HOLogic.mk_prod (t1, t2), st'') 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

473 
 mk_args2 (T as Type ("fun", _)) (params, ctxt) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

475 
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:
34028
diff
changeset

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

477 
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:
34028
diff
changeset

478 
(hd params, (tl params, ctxt)) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

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

481 
val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

483 
(Free (x, T), (params, ctxt')) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

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

486 
 mk_args2 T (params, ctxt) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

488 
val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

490 
(Free (x, T), (params, ctxt')) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

492 

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

493 
fun mk_casesrule ctxt pred introrules = 
33129
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

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

495 
val (((pred, params), intros_th), ctxt1) = import_intros pred introrules ctxt 
33129
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

496 
val intros = map prop_of intros_th 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

497 
val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

498 
val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT)) 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

499 
val argsT = binder_types (fastype_of pred) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

500 
val (argvs, _) = fold_map mk_args2 argsT (params, ctxt2) 
33129
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

501 
fun mk_case intro = 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

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

503 
val (_, args) = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl) intro 
33129
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

504 
val prems = Logic.strip_imp_prems intro 
33629
5f35cf91c6a4
improving code quality thanks to Florian's code review
bulwahn
parents:
33628
diff
changeset

505 
val eqprems = map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) argvs args 
33129
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

506 
val frees = (fold o fold_aterms) 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

507 
(fn t as Free _ => 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

508 
if member (op aconv) params t then I else insert (op aconv) t 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

509 
 _ => I) (args @ prems) [] 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

510 
in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

511 
val assm = HOLogic.mk_Trueprop (list_comb (pred, argvs)) 
33129
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

512 
val cases = map mk_case intros 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

513 
in Logic.list_implies (assm :: cases, prop) end; 
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higherorder function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33128
diff
changeset

514 

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

515 
(** preprocessing rules **) 
32667  516 

517 
fun imp_prems_conv cv ct = 

518 
case Thm.term_of ct of 

519 
Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct 

520 
 _ => Conv.all_conv ct 

521 

522 
fun Trueprop_conv cv ct = 

523 
case Thm.term_of ct of 

524 
Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct 

525 
 _ => error "Trueprop_conv" 

526 

527 
fun preprocess_intro thy rule = 

528 
Conv.fconv_rule 

529 
(imp_prems_conv 

530 
(Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq}))))) 

531 
(Thm.transfer thy rule) 

532 

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

533 
fun preprocess_elim thy elimrule = 
32667  534 
let 
535 
fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) = 

536 
HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs) 

537 
 replace_eqs t = t 

33128  538 
val ctxt = ProofContext.init thy 
539 
val ((_, [elimrule]), ctxt') = Variable.import false [elimrule] ctxt 

540 
val prems = Thm.prems_of elimrule 

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

541 
val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems)))) 
32667  542 
fun preprocess_case t = 
33128  543 
let 
32667  544 
val params = Logic.strip_params t 
545 
val (assums1, assums2) = chop nargs (Logic.strip_assums_hyp t) 

546 
val assums_hyp' = assums1 @ (map replace_eqs assums2) 

33128  547 
in 
32667  548 
list_all (params, Logic.list_implies (assums_hyp', Logic.strip_assums_concl t)) 
33128  549 
end 
32667  550 
val cases' = map preprocess_case (tl prems) 
551 
val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule) 

552 
val bigeq = (Thm.symmetric (Conv.implies_concl_conv 

553 
(MetaSimplifier.rewrite true [@{thm Predicate.eq_is_eq}]) 

554 
(cterm_of thy elimrule'))) 

33150
75eddea4abef
further changes due to the previous merge in the predicate compiler
bulwahn
parents:
33149
diff
changeset

555 
val tac = (fn _ => Skip_Proof.cheat_tac thy) 
33109
7025bc7a5054
changed elimination preprocessing due to an error with a JinjaThread predicate
bulwahn
parents:
33108
diff
changeset

556 
val eq = Goal.prove ctxt' [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) tac 
32667  557 
in 
33109
7025bc7a5054
changed elimination preprocessing due to an error with a JinjaThread predicate
bulwahn
parents:
33108
diff
changeset

558 
Thm.equal_elim eq elimrule > singleton (Variable.export ctxt' ctxt) 
32667  559 
end; 
560 

33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset

561 
fun expand_tuples_elim th = th 
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset

562 

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

563 
val no_compilation = ([], [], []) 
33483
a15a2f7f7560
improved handling of already defined functions in the predicate compiler; could cause trouble before when no modes for a predicate were infered
bulwahn
parents:
33482
diff
changeset

564 

32667  565 
fun fetch_pred_data thy name = 
566 
case try (Inductive.the_inductive (ProofContext.init thy)) name of 

567 
SOME (info as (_, result)) => 

568 
let 

569 
fun is_intro_of intro = 

570 
let 

571 
val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro)) 

572 
in (fst (dest_Const const) = name) end; 

33752
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

573 
val intros = 
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset

574 
(map (expand_tuples thy #> preprocess_intro thy) (filter is_intro_of (#intrs result))) 
33146
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33145
diff
changeset

575 
val index = find_index (fn s => s = name) (#names (fst info)) 
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33145
diff
changeset

576 
val pre_elim = nth (#elims result) index 
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33145
diff
changeset

577 
val pred = nth (#preds result) index 
33752
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

578 
(*val elim = singleton (Inductive_Set.codegen_preproc thy) (preprocess_elim thy nparams 
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset

579 
(expand_tuples_elim pre_elim))*) 
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset

580 
val elim = 
35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
34974
diff
changeset

581 
(Drule.export_without_context o Skip_Proof.make_thm thy) 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

582 
(mk_casesrule (ProofContext.init thy) pred intros) 
32667  583 
in 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

584 
mk_pred_data ((intros, SOME elim), no_compilation) 
33483
a15a2f7f7560
improved handling of already defined functions in the predicate compiler; could cause trouble before when no modes for a predicate were infered
bulwahn
parents:
33482
diff
changeset

585 
end 
32667  586 
 NONE => error ("No such predicate: " ^ quote name) 
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset

587 

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

588 
fun add_predfun_data name mode data = 
32667  589 
let 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

590 
val add = (apsnd o apsnd3) (cons (mode, mk_predfun_data data)) 
32667  591 
in PredData.map (Graph.map_node name (map_pred_data add)) end 
592 

593 
fun is_inductive_predicate thy name = 

594 
is_some (try (Inductive.the_inductive (ProofContext.init thy)) name) 

595 

596 
fun depending_preds_of thy (key, value) = 

597 
let 

598 
val intros = (#intros o rep_pred_data) value 

599 
in 

600 
fold Term.add_const_names (map Thm.prop_of intros) [] 

33482
5029ec373036
strictly respecting the line margin in the predicate compiler core
bulwahn
parents:
33479
diff
changeset

601 
> filter (fn c => (not (c = key)) andalso 
5029ec373036
strictly respecting the line margin in the predicate compiler core
bulwahn
parents:
33479
diff
changeset

602 
(is_inductive_predicate thy c orelse is_registered thy c)) 
32667  603 
end; 
604 

33629
5f35cf91c6a4
improving code quality thanks to Florian's code review
bulwahn
parents:
33628
diff
changeset

605 
fun add_intro thm thy = 
5f35cf91c6a4
improving code quality thanks to Florian's code review
bulwahn
parents:
33628
diff
changeset

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

607 
val (name, T) = dest_Const (fst (strip_intro_concl thm)) 
33629
5f35cf91c6a4
improving code quality thanks to Florian's code review
bulwahn
parents:
33628
diff
changeset

608 
fun cons_intro gr = 
32667  609 
case try (Graph.get_node gr) name of 
610 
SOME pred_data => Graph.map_node name (map_pred_data 

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

611 
(apfst (fn (intros, elim) => (intros @ [thm], elim)))) gr 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

612 
 NONE => Graph.new_node (name, mk_pred_data (([thm], NONE), no_compilation)) gr 
32667  613 
in PredData.map cons_intro thy end 
614 

33629
5f35cf91c6a4
improving code quality thanks to Florian's code review
bulwahn
parents:
33628
diff
changeset

615 
fun set_elim thm = 
5f35cf91c6a4
improving code quality thanks to Florian's code review
bulwahn
parents:
33628
diff
changeset

616 
let 
32667  617 
val (name, _) = dest_Const (fst 
618 
(strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm))))) 

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

619 
fun set (intros, _) = (intros, SOME thm) 
32667  620 
in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end 
621 

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

622 
fun register_predicate (constname, pre_intros, pre_elim) thy = 
33629
5f35cf91c6a4
improving code quality thanks to Florian's code review
bulwahn
parents:
33628
diff
changeset

623 
let 
33752
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

624 
val intros = map (preprocess_intro thy) pre_intros 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

625 
val elim = preprocess_elim thy pre_elim 
32667  626 
in 
33146
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33145
diff
changeset

627 
if not (member (op =) (Graph.keys (PredData.get thy)) constname) then 
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32667
diff
changeset

628 
PredData.map 
33482
5029ec373036
strictly respecting the line margin in the predicate compiler core
bulwahn
parents:
33479
diff
changeset

629 
(Graph.new_node (constname, 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

630 
mk_pred_data ((intros, SOME elim), no_compilation))) thy 
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32667
diff
changeset

631 
else thy 
32667  632 
end 
633 

33146
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33145
diff
changeset

634 
fun register_intros (constname, pre_intros) thy = 
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32667
diff
changeset

635 
let 
33146
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33145
diff
changeset

636 
val T = Sign.the_const_type thy constname 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

637 
fun constname_of_intro intr = fst (dest_Const (fst (strip_intro_concl intr))) 
33146
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33145
diff
changeset

638 
val _ = if not (forall (fn intr => constname_of_intro intr = constname) pre_intros) then 
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33145
diff
changeset

639 
error ("register_intros: Introduction rules of different constants are used\n" ^ 
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33145
diff
changeset

640 
"expected rules for " ^ constname ^ ", but received rules for " ^ 
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33145
diff
changeset

641 
commas (map constname_of_intro pre_intros)) 
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33145
diff
changeset

642 
else () 
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33145
diff
changeset

643 
val pred = Const (constname, T) 
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32671
diff
changeset

644 
val pre_elim = 
35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
34974
diff
changeset

645 
(Drule.export_without_context o Skip_Proof.make_thm thy) 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

646 
(mk_casesrule (ProofContext.init thy) pred pre_intros) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

647 
in register_predicate (constname, pre_intros, pre_elim) thy end 
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32667
diff
changeset

648 

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

649 
fun defined_function_of compilation pred = 
32667  650 
let 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

651 
val set = (apsnd o apfst3) (cons (compilation, [])) 
32667  652 
in 
653 
PredData.map (Graph.map_node pred (map_pred_data set)) 

654 
end 

655 

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

656 
fun set_function_name compilation pred mode name = 
32667  657 
let 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

658 
val set = (apsnd o apfst3) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

659 
(AList.map_default (op =) (compilation, [(mode, name)]) (cons (mode, name))) 
33473
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
33377
diff
changeset

660 
in 
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
33377
diff
changeset

661 
PredData.map (Graph.map_node pred (map_pred_data set)) 
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
33377
diff
changeset

662 
end 
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
33377
diff
changeset

663 

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

664 
fun set_needs_random name modes = 
33473
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
33377
diff
changeset

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

666 
val set = (apsnd o aptrd3) (K modes) 
32667  667 
in 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

668 
PredData.map (Graph.map_node name (map_pred_data set)) 
32667  669 
end 
670 

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

671 
(* datastructures and setup for generic compilation *) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

672 

32667  673 
datatype compilation_funs = CompilationFuns of { 
674 
mk_predT : typ > typ, 

675 
dest_predT : typ > typ, 

676 
mk_bot : typ > term, 

677 
mk_single : term > term, 

678 
mk_bind : term * term > term, 

679 
mk_sup : term * term > term, 

680 
mk_if : term > term, 

681 
mk_not : term > term, 

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

682 
mk_map : typ > typ > term > term > term 
32667  683 
}; 
684 

685 
fun mk_predT (CompilationFuns funs) = #mk_predT funs 

686 
fun dest_predT (CompilationFuns funs) = #dest_predT funs 

687 
fun mk_bot (CompilationFuns funs) = #mk_bot funs 

688 
fun mk_single (CompilationFuns funs) = #mk_single funs 

689 
fun mk_bind (CompilationFuns funs) = #mk_bind funs 

690 
fun mk_sup (CompilationFuns funs) = #mk_sup funs 

691 
fun mk_if (CompilationFuns funs) = #mk_if funs 

692 
fun mk_not (CompilationFuns funs) = #mk_not funs 

693 
fun mk_map (CompilationFuns funs) = #mk_map funs 

694 

695 
structure PredicateCompFuns = 

696 
struct 

697 

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

698 
fun mk_predT T = Type (@{type_name Predicate.pred}, [T]) 
32667  699 

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

700 
fun dest_predT (Type (@{type_name Predicate.pred}, [T])) = T 
32667  701 
 dest_predT T = raise TYPE ("dest_predT", [T], []); 
702 

703 
fun mk_bot T = Const (@{const_name Orderings.bot}, mk_predT T); 

704 

705 
fun mk_single t = 

706 
let val T = fastype_of t 

707 
in Const(@{const_name Predicate.single}, T > mk_predT T) $ t end; 

708 

709 
fun mk_bind (x, f) = 

710 
let val T as Type ("fun", [_, U]) = fastype_of f 

711 
in 

712 
Const (@{const_name Predicate.bind}, fastype_of x > T > U) $ x $ f 

713 
end; 

714 

715 
val mk_sup = HOLogic.mk_binop @{const_name sup}; 

716 

717 
fun mk_if cond = Const (@{const_name Predicate.if_pred}, 

718 
HOLogic.boolT > mk_predT HOLogic.unitT) $ cond; 

719 

720 
fun mk_not t = let val T = mk_predT HOLogic.unitT 

721 
in Const (@{const_name Predicate.not_pred}, T > T) $ t end 

722 

723 
fun mk_Enum f = 

724 
let val T as Type ("fun", [T', _]) = fastype_of f 

725 
in 

726 
Const (@{const_name Predicate.Pred}, T > mk_predT T') $ f 

727 
end; 

728 

729 
fun mk_Eval (f, x) = 

730 
let 

731 
val T = fastype_of x 

732 
in 

733 
Const (@{const_name Predicate.eval}, mk_predT T > T > HOLogic.boolT) $ f $ x 

734 
end; 

735 

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

736 
fun dest_Eval (Const (@{const_name Predicate.eval}, _) $ f $ x) = (f, x) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

737 

32667  738 
fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map}, 
739 
(T1 > T2) > mk_predT T1 > mk_predT T2) $ tf $ tp; 

740 

741 
val compfuns = CompilationFuns {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot, 

742 
mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not, 

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

743 
mk_map = mk_map}; 
32667  744 

745 
end; 

746 

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

747 
structure RandomPredCompFuns = 
32667  748 
struct 
749 

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

750 
fun mk_randompredT T = 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33150
diff
changeset

751 
@{typ Random.seed} > HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ Random.seed}) 
32667  752 

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

753 
fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name "*"}, 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33150
diff
changeset

754 
[Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33150
diff
changeset

755 
 dest_randompredT T = raise TYPE ("dest_randompredT", [T], []); 
32667  756 

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

757 
fun mk_bot T = Const(@{const_name Quickcheck.empty}, mk_randompredT T) 
32667  758 

759 
fun mk_single t = 

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

760 
let 
32667  761 
val T = fastype_of t 
762 
in 

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

763 
Const (@{const_name Quickcheck.single}, T > mk_randompredT T) $ t 
32667  764 
end; 
765 

766 
fun mk_bind (x, f) = 

767 
let 

768 
val T as (Type ("fun", [_, U])) = fastype_of f 

769 
in 

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

770 
Const (@{const_name Quickcheck.bind}, fastype_of x > T > U) $ x $ f 
32667  771 
end 
772 

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

773 
val mk_sup = HOLogic.mk_binop @{const_name Quickcheck.union} 
32667  774 

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

775 
fun mk_if cond = Const (@{const_name Quickcheck.if_randompred}, 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33150
diff
changeset

776 
HOLogic.boolT > mk_randompredT HOLogic.unitT) $ cond; 
32667  777 

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

778 
fun mk_not t = let val T = mk_randompredT HOLogic.unitT 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33150
diff
changeset

779 
in Const (@{const_name Quickcheck.not_randompred}, T > T) $ t end 
32667  780 

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

781 
fun mk_map T1 T2 tf tp = Const (@{const_name Quickcheck.map}, 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33150
diff
changeset

782 
(T1 > T2) > mk_randompredT T1 > mk_randompredT T2) $ tf $ tp 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33150
diff
changeset

783 

33482
5029ec373036
strictly respecting the line margin in the predicate compiler core
bulwahn
parents:
33479
diff
changeset

784 
val compfuns = CompilationFuns {mk_predT = mk_randompredT, dest_predT = dest_randompredT, 
5029ec373036
strictly respecting the line margin in the predicate compiler core
bulwahn
parents:
33479
diff
changeset

785 
mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, 
5029ec373036
strictly respecting the line margin in the predicate compiler core
bulwahn
parents:
33479
diff
changeset

786 
mk_not = mk_not, mk_map = mk_map}; 
32667  787 

788 
end; 

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

789 

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

790 
structure DSequence_CompFuns = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

792 

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

793 
fun mk_dseqT T = Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool}, 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

794 
Type (@{type_name Option.option}, [Type ("Lazy_Sequence.lazy_sequence", [T])])])]) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

795 

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

796 
fun dest_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool}, 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

797 
Type (@{type_name Option.option}, [Type ("Lazy_Sequence.lazy_sequence", [T])])])])) = T 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

798 
 dest_dseqT T = raise TYPE ("dest_dseqT", [T], []); 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

799 

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

800 
fun mk_bot T = Const ("DSequence.empty", mk_dseqT T); 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

801 

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

802 
fun mk_single t = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

803 
let val T = fastype_of t 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

804 
in Const("DSequence.single", T > mk_dseqT T) $ t end; 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

805 

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

806 
fun mk_bind (x, f) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

807 
let val T as Type ("fun", [_, U]) = fastype_of f 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

809 
Const ("DSequence.bind", fastype_of x > T > U) $ x $ f 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

811 

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

812 
val mk_sup = HOLogic.mk_binop "DSequence.union"; 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

813 

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

814 
fun mk_if cond = Const ("DSequence.if_seq", 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

815 
HOLogic.boolT > mk_dseqT HOLogic.unitT) $ cond; 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

816 

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

817 
fun mk_not t = let val T = mk_dseqT HOLogic.unitT 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

818 
in Const ("DSequence.not_seq", T > T) $ t end 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

819 

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

820 
fun mk_map T1 T2 tf tp = Const ("DSequence.map", 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

821 
(T1 > T2) > mk_dseqT T1 > mk_dseqT T2) $ tf $ tp 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

822 

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

823 
val compfuns = CompilationFuns {mk_predT = mk_dseqT, dest_predT = dest_dseqT, 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

824 
mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

825 
mk_not = mk_not, mk_map = mk_map} 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

826 

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

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

828 

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

829 
structure Random_Sequence_CompFuns = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

831 

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

832 
fun mk_random_dseqT T = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

833 
@{typ code_numeral} > @{typ code_numeral} > @{typ Random.seed} > 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

834 
HOLogic.mk_prodT (DSequence_CompFuns.mk_dseqT T, @{typ Random.seed}) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

835 

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

836 
fun dest_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral}, 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

837 
Type ("fun", [@{typ Random.seed}, 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

838 
Type (@{type_name "*"}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

839 
 dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []); 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

840 

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

841 
fun mk_bot T = Const ("Random_Sequence.empty", mk_random_dseqT T); 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

842 

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

843 
fun mk_single t = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

844 
let val T = fastype_of t 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

845 
in Const("Random_Sequence.single", T > mk_random_dseqT T) $ t end; 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

846 

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

847 
fun mk_bind (x, f) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

849 
val T as Type ("fun", [_, U]) = fastype_of f 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

851 
Const ("Random_Sequence.bind", fastype_of x > T > U) $ x $ f 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

853 

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

854 
val mk_sup = HOLogic.mk_binop "Random_Sequence.union"; 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

855 

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

856 
fun mk_if cond = Const ("Random_Sequence.if_random_dseq", 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

857 
HOLogic.boolT > mk_random_dseqT HOLogic.unitT) $ cond; 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

858 

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

859 
fun mk_not t = let val T = mk_random_dseqT HOLogic.unitT 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

860 
in Const ("Random_Sequence.not_random_dseq", T > T) $ t end 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

861 

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

862 
fun mk_map T1 T2 tf tp = Const ("Random_Sequence.map", 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

863 
(T1 > T2) > mk_random_dseqT T1 > mk_random_dseqT T2) $ tf $ tp 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

864 

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

865 
val compfuns = CompilationFuns {mk_predT = mk_random_dseqT, dest_predT = dest_random_dseqT, 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

866 
mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

867 
mk_not = mk_not, mk_map = mk_map} 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

868 

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

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

870 

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

871 

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

872 

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

873 
fun mk_random T = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

875 
val random = Const ("Quickcheck.random_class.random", 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

876 
@{typ code_numeral} > @{typ Random.seed} > 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

877 
HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

879 
Const ("Random_Sequence.Random", (@{typ code_numeral} > @{typ Random.seed} > 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

880 
HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) > 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

881 
Random_Sequence_CompFuns.mk_random_dseqT T) $ random 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

883 

32667  884 
(* for external use with interactive mode *) 
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32671
diff
changeset

885 
val pred_compfuns = PredicateCompFuns.compfuns 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

886 
val randompred_compfuns = Random_Sequence_CompFuns.compfuns; 
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32671
diff
changeset

887 

33473
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
33377
diff
changeset

888 
(* function types and names of different compilations *) 
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
33377
diff
changeset

889 

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

890 
fun funT_of compfuns mode T = 
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32671
diff
changeset

891 
let 
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32671
diff
changeset

892 
val Ts = binder_types T 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

893 
val (inTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode Ts 
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32671
diff
changeset

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

895 
inTs > (mk_predT compfuns (HOLogic.mk_tupleT outTs)) 
33473
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
33377
diff
changeset

896 
end; 
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32671
diff
changeset

897 

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

898 
(** mode analysis **) 
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32671
diff
changeset

899 

35411  900 
type mode_analysis_options = {use_random : bool, reorder_premises : bool, infer_pos_and_neg_modes : 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:
35267
diff
changeset

901 

32667  902 
fun is_constrt thy = 
903 
let 

904 
val cnstrs = flat (maps 

905 
(map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd) 

906 
(Symtab.dest (Datatype.get_all thy))); 

907 
fun check t = (case strip_comb t of 

908 
(Free _, []) => true 

909 
 (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of 

33482
5029ec373036
strictly respecting the line margin in the predicate compiler core
bulwahn
parents:
33479
diff
changeset

910 
(SOME (i, Tname), Type (Tname', _)) => 
5029ec373036
strictly respecting the line margin in the predicate compiler core
bulwahn
parents:
33479
diff
changeset

911 
length ts = i andalso Tname = Tname' andalso forall check ts 
32667  912 
 _ => false) 
913 
 _ => false) 

914 
in check end; 

915 

916 
(*** check if a type is an equality type (i.e. doesn't contain fun) 

917 
FIXME this is only an approximation ***) 

918 
fun is_eqT (Type (s, Ts)) = s <> "fun" andalso forall is_eqT Ts 

919 
 is_eqT _ = true; 

920 

921 
fun term_vs tm = fold_aterms (fn Free (x, T) => cons x  _ => I) tm []; 

922 
val terms_vs = distinct (op =) o maps term_vs; 

923 

924 
(** collect all Frees in a term (with duplicates!) **) 

925 
fun term_vTs tm = 

926 
fold_aterms (fn Free xT => cons xT  _ => I) tm []; 

927 

33138
e2e23987c59a
reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents:
33137
diff
changeset

928 
fun subsets i j = 
e2e23987c59a
reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents:
33137
diff
changeset

929 
if i <= j then 
e2e23987c59a
reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents:
33137
diff
changeset

930 
let 
e2e23987c59a
reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents:
33137
diff
changeset

931 
fun merge xs [] = xs 
e2e23987c59a
reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents:
33137
diff
changeset

932 
 merge [] ys = ys 
e2e23987c59a
reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents:
33137
diff
changeset

933 
 merge (x::xs) (y::ys) = if length x >= length y then x::merge xs (y::ys) 
e2e23987c59a
reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents:
33137
diff
changeset

934 
else y::merge (x::xs) ys; 
e2e23987c59a
reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents:
33137
diff
changeset

935 
val is = subsets (i+1) j 
e2e23987c59a
reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents:
33137
diff
changeset

936 
in merge (map (fn ks => i::ks) is) is end 
e2e23987c59a
reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents:
33137
diff
changeset

937 
else [[]]; 
32667  938 

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:
35267
diff
changeset

939 
fun print_failed_mode options thy modes p (pol, m) rs is = 
33130
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33129
diff
changeset

940 
if show_mode_inference options then 
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33129
diff
changeset

941 
let 
33752
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

942 
val _ = tracing ("Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^ 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

943 
p ^ " violates mode " ^ string_of_mode m) 
33130
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33129
diff
changeset

944 
in () end 
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33129
diff
changeset

945 
else () 
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33129
diff
changeset

946 

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:
35267
diff
changeset

947 
fun error_of p (pol, m) is = 
33752
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

948 
(" Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^ 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

949 
p ^ " violates mode " ^ string_of_mode m) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

950 

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

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

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

953 
fun is_all_input' (Fun _) = true 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

954 
 is_all_input' (Pair (m1, m2)) = is_all_input' m1 andalso is_all_input' m2 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

955 
 is_all_input' Input = true 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

956 
 is_all_input' Output = false 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

958 
forall is_all_input' (strip_fun_mode mode) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

960 

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

961 
fun all_input_of T = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

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

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

965 
 input_of _ = Input 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

967 
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:
34028
diff
changeset

968 
fold_rev (curry Fun) (map input_of Ts) Bool 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

970 
error "all_input_of: not a predicate" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

972 

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

973 
fun partial_hd [] = NONE 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

974 
 partial_hd (x :: xs) = SOME x 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

975 

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

976 
fun term_vs tm = fold_aterms (fn Free (x, T) => cons x  _ => I) tm []; 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

977 
val terms_vs = distinct (op =) o maps term_vs; 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

978 

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

979 
fun input_mode T = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

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

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

983 
fold_rev (curry Fun) (map (K Input) Ts) Input 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

985 

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

986 
fun output_mode T = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

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

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

990 
fold_rev (curry Fun) (map (K Output) Ts) Output 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

992 

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

993 
fun is_invertible_function thy (Const (f, _)) = is_constr thy f 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

994 
 is_invertible_function thy _ = false 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

995 

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:
35267
diff
changeset

996 
fun non_invertible_subterms thy (t as Free _) = [] 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

997 
 non_invertible_subterms thy t = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

998 
case (strip_comb t) of (f, args) => 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

999 
if is_invertible_function thy f then 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1000 
maps (non_invertible_subterms thy) args 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

1002 
[t] 
33752
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

1003 

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

1004 
fun collect_non_invertible_subterms thy (f as Free _) (names, eqs) = (f, (names, eqs)) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1005 
 collect_non_invertible_subterms thy t (names, eqs) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1006 
case (strip_comb t) of (f, args) => 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1007 
if is_invertible_function thy f then 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

1009 
val (args', (names', eqs')) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1010 
fold_map (collect_non_invertible_subterms thy) args (names, eqs) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

1012 
(list_comb (f, args'), (names', eqs')) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

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

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

1016 
val s = Name.variant names "x" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1017 
val v = Free (s, fastype_of t) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

1019 
(v, (s :: names, HOLogic.mk_eq (v, t) :: eqs)) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

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

1022 
if is_constrt thy t then (t, (names, eqs)) else 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

1024 
val s = Name.variant names "x" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1025 
val v = Free (s, fastype_of t) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1026 
in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end; 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

1028 

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

1029 
fun is_possible_output thy vs t = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

1031 
(fn t => is_eqT (fastype_of t) andalso forall (member (op =) vs) (term_vs t)) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1032 
(non_invertible_subterms thy 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:
35267
diff
changeset

1033 
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:
35267
diff
changeset

1034 
(forall (is_eqT o snd) 
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:
35267
diff
changeset

1035 
(inter (fn ((f', _), f) => f = f') vs (Term.add_frees t []))) 
33752
9aa8e961f850
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents:
33671
diff
changeset

1036 

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

1037 
fun vars_of_destructable_term thy (Free (x, _)) = [x] 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1038 
 vars_of_destructable_term thy t = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1039 
case (strip_comb t) of (f, args) => 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1040 
if is_invertible_function thy f then 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1041 
maps (vars_of_destructable_term thy) args 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

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

1044 

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

1045 
fun is_constructable thy vs t = forall (member (op =) vs) (term_vs t) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1046 

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

1047 
fun missing_vars vs t = subtract (op =) vs (term_vs t) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1048 

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:
35267
diff
changeset

1049 
fun output_terms (Const ("Pair", _) $ t1 $ t2, Mode_Pair (d1, d2)) = 
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:
35267
diff
changeset

1050 
output_terms (t1, d1) @ output_terms (t2, d2) 
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:
35267
diff
changeset

1051 
 output_terms (t1 $ t2, Mode_App (d1, d2)) = 
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:
35267
diff
changeset

1052 
output_terms (t1, d1) @ output_terms (t2, d2) 
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:
35267
diff
changeset

1053 
 output_terms (t, Term Output) = [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:
35267
diff
changeset

1054 
 output_terms _ = [] 
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:
35267
diff
changeset

1055 

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:
35267
diff
changeset

1056 
fun lookup_mode modes (Const (s, 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:
35267
diff
changeset

1057 
(case (AList.lookup (op =) modes s) of 
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:
35267
diff
changeset

1058 
SOME ms => SOME (map (fn m => (Context m, [])) ms) 
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:
35267
diff
changeset

1059 
 NONE => 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:
35267
diff
changeset

1060 
 lookup_mode modes (Free (x, _)) = 
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:
35267
diff
changeset

1061 
(case (AList.lookup (op =) modes x) of 
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:
35267
diff
changeset

1062 
SOME ms => SOME (map (fn m => (Context m , [])) ms) 
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:
35267
diff
changeset

1063 
 NONE => 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:
35267
diff
changeset

1064 

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:
35267
diff
changeset

1065 
fun derivations_of thy modes vs (Const ("Pair", _) $ t1 $ t2) (Pair (m1, m2)) = 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

1067 
(fn (m1, mvars1) => fn (m2, mvars2) => (Mode_Pair (m1, m2), union (op =) mvars1 mvars2)) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1068 
(derivations_of thy modes vs t1 m1) (derivations_of thy modes vs t2 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:
35267
diff
changeset

1069 
 derivations_of thy modes vs t (m as 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:
35267
diff
changeset

1070 
(*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:
35267
diff
changeset

1071 
val (p, args) = strip_comb 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:
35267
diff
changeset

1072 
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:
35267
diff
changeset

1073 
(case lookup_mode modes p of 
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:
35267
diff
changeset

1074 
SOME ms => map_filter (fn (Context m, []) => 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:
35267
diff
changeset

1075 
val ms = strip_fun_mode m 
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:
35267
diff
changeset

1076 
val (argms, restms) = chop (length args) ms 
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:
35267
diff
changeset

1077 
val m' = fold_rev (curry Fun) restms 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:
35267
diff
changeset

1078 
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:
35267
diff
changeset

1079 
if forall (fn m => eq_mode (Input, m)) argms andalso eq_mode (m', mode) 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:
35267
diff
changeset

1080 
SOME (fold (curry Mode_App) (map Term argms) (Context m), missing_vars vs 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:
35267
diff
changeset

1081 
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:
35267
diff
changeset

1082 
end) ms 
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:
35267
diff
changeset

1083 
 NONE => (if is_all_input mode then [(Context mode, [])] 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:
35267
diff
changeset

1084 
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:
35267
diff
changeset

1085 
(case try (all_derivations_of thy modes vs) t of 
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:
35267
diff
changeset

1086 
SOME derivs => 
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:
35267
diff
changeset

1087 
filter (fn (d, mvars) => eq_mode (mode_of d, m) andalso null (output_terms (t, d))) derivs 
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:
35267
diff
changeset

1088 
 NONE => (if is_all_input m then [(Context m, [])] else [])) 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1089 
 derivations_of thy modes vs t m = 
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:
35267
diff
changeset

1090 
if eq_mode (m, Input) 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:
35267
diff
changeset

1091 
[(Term Input, missing_vars vs 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:
35267
diff
changeset

1092 
else if eq_mode (m, Output) 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:
35267
diff
changeset

1093 
(if is_possible_output thy vs t then [(Term Output, [])] 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:
35267
diff
changeset

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

1095 
and all_derivations_of thy modes vs (Const ("Pair", _) $ t1 $ t2) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

1097 
val derivs1 = all_derivations_of thy modes vs t1 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1098 
val derivs2 = all_derivations_of thy modes vs t2 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

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

1101 
(fn (m1, mvars1) => fn (m2, mvars2) => (Mode_Pair (m1, m2), union (op =) mvars1 mvars2)) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

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

1104 
 all_derivations_of thy modes vs (t1 $ t2) = 
33146
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33145
diff
changeset

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

1106 
val derivs1 = all_derivations_of thy modes vs t1 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

1108 
maps (fn (d1, mvars1) => 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1109 
case mode_of d1 of 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1110 
Fun (m', _) => map (fn (d2, mvars2) => 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1111 
(Mode_App (d1, d2), union (op =) mvars1 mvars2)) (derivations_of thy modes vs t2 m') 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1112 
 _ => error "Something went wrong") derivs1 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1113 
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:
35267
diff
changeset

1114 
 all_derivations_of thy modes vs (Const (s, T)) = the (lookup_mode modes (Const (s, 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:
35267
diff
changeset

1115 
 all_derivations_of thy modes vs (Free (x, T)) = the (lookup_mode modes (Free (x, T))) 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1116 
 all_derivations_of _ modes vs _ = error "all_derivations_of" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1117 

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

1118 
fun rev_option_ord ord (NONE, NONE) = EQUAL 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1119 
 rev_option_ord ord (NONE, SOME _) = GREATER 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1120 
 rev_option_ord ord (SOME _, NONE) = LESS 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1121 
 rev_option_ord ord (SOME x, SOME y) = ord (x, y) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1122 

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