author  bulwahn 
Fri, 11 Nov 2011 10:40:36 +0100  
changeset 45452  414732ebf891 
parent 45450  dc2236b19a3d 
child 45461  130c90bb80b4 
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 

36048  9 
type mode = Predicate_Compile_Aux.mode 
10 
type options = Predicate_Compile_Aux.options 

11 
type compilation = Predicate_Compile_Aux.compilation 

12 
type compilation_funs = Predicate_Compile_Aux.compilation_funs 

13 

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

14 
val setup : theory > theory 
36048  15 
val code_pred : options > string > Proof.context > Proof.state 
16 
val code_pred_cmd : options > string > Proof.context > Proof.state 

17 
val values_cmd : string list > mode option list option 

18 
> ((string option * bool) * (compilation * int list)) > int > string > Toplevel.state > unit 

40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset

19 

42141
2c255ba8f299
changing values_timeout from a static option to a dynamic option as required for testing with SML/NJ
bulwahn
parents:
42094
diff
changeset

20 
val values_timeout : real Config.T 
2c255ba8f299
changing values_timeout from a static option to a dynamic option as required for testing with SML/NJ
bulwahn
parents:
42094
diff
changeset

21 

37007
116670499530
changing operations for accessing data to work with contexts
bulwahn
parents:
37006
diff
changeset

22 
val print_stored_rules : Proof.context > unit 
37003
a393a588b82e
moving towards working with proof contexts in the predicate compiler
bulwahn
parents:
37002
diff
changeset

23 
val print_all_modes : compilation > Proof.context > unit 
39388
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39310
diff
changeset

24 

fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39310
diff
changeset

25 
val put_pred_result : (unit > term Predicate.pred) > Proof.context > Proof.context 
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39310
diff
changeset

26 
val put_pred_random_result : (unit > int * int > term Predicate.pred * (int * int)) > 
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39310
diff
changeset

27 
Proof.context > Proof.context 
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39310
diff
changeset

28 
val put_dseq_result : (unit > term DSequence.dseq) > Proof.context > Proof.context 
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39310
diff
changeset

29 
val put_dseq_random_result : (unit > int > int > int * int > term DSequence.dseq * (int * int)) > 
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39310
diff
changeset

30 
Proof.context > Proof.context 
40102
a9e4e94b3022
restructuring values command and adding generator compilation
bulwahn
parents:
40053
diff
changeset

31 
val put_new_dseq_result : (unit > int > term Lazy_Sequence.lazy_sequence) > 
a9e4e94b3022
restructuring values command and adding generator compilation
bulwahn
parents:
40053
diff
changeset

32 
Proof.context > Proof.context 
39388
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39310
diff
changeset

33 
val put_lseq_random_result : 
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39310
diff
changeset

34 
(unit > int > int > int * int > int > term Lazy_Sequence.lazy_sequence) > 
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39310
diff
changeset

35 
Proof.context > Proof.context 
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39310
diff
changeset

36 
val put_lseq_random_stats_result : 
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39310
diff
changeset

37 
(unit > int > int > int * int > int > (term * int) Lazy_Sequence.lazy_sequence) > 
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39310
diff
changeset

38 
Proof.context > Proof.context 
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39310
diff
changeset

39 

33628  40 
val code_pred_intro_attrib : attribute 
32667  41 
(* used by Quickcheck_Generator *) 
42 
(* temporary for testing of the compilation *) 

36048  43 
val add_equations : options > string list > theory > theory 
44 
val add_depth_limited_random_equations : options > string list > theory > theory 

45 
val add_random_dseq_equations : options > string list > theory > theory 

46 
val add_new_random_dseq_equations : options > string list > theory > theory 

40103  47 
val add_generator_dseq_equations : options > string list > theory > theory 
45450  48 
val add_generator_cps_equations : options > string list > theory > theory 
33473
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
33377
diff
changeset

49 
val mk_tracing : string > term > term 
39310
17ef4415b17c
removing obsolete argument in prepare_intrs; passing context instead of theory in prepare_intrs
bulwahn
parents:
39299
diff
changeset

50 
val prepare_intrs : options > Proof.context > string list > thm list > 
38957
2eb265efa1b0
exporting mode analysis for use in prolog generation
bulwahn
parents:
38864
diff
changeset

51 
((string * typ) list * string list * string list * (string * mode list) list * 
2eb265efa1b0
exporting mode analysis for use in prolog generation
bulwahn
parents:
38864
diff
changeset

52 
(string * (Term.term list * Predicate_Compile_Aux.indprem list) list) list) 
39761
c2a76ec6e2d9
renaming use_random to use_generators in the predicate compiler
bulwahn
parents:
39760
diff
changeset

53 
type mode_analysis_options = 
c2a76ec6e2d9
renaming use_random to use_generators in the predicate compiler
bulwahn
parents:
39760
diff
changeset

54 
{use_generators : bool, 
c2a76ec6e2d9
renaming use_random to use_generators in the predicate compiler
bulwahn
parents:
39760
diff
changeset

55 
reorder_premises : bool, 
c2a76ec6e2d9
renaming use_random to use_generators in the predicate compiler
bulwahn
parents:
39760
diff
changeset

56 
infer_pos_and_neg_modes : bool} 
38957
2eb265efa1b0
exporting mode analysis for use in prolog generation
bulwahn
parents:
38864
diff
changeset

57 
datatype mode_derivation = Mode_App of mode_derivation * mode_derivation  Context of mode 
39310
17ef4415b17c
removing obsolete argument in prepare_intrs; passing context instead of theory in prepare_intrs
bulwahn
parents:
39299
diff
changeset

58 
 Mode_Pair of mode_derivation * mode_derivation  Term of mode 
39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39403
diff
changeset

59 
val head_mode_of : mode_derivation > mode 
38957
2eb265efa1b0
exporting mode analysis for use in prolog generation
bulwahn
parents:
38864
diff
changeset

60 
type moded_clause = term list * (Predicate_Compile_Aux.indprem * mode_derivation) list 
2eb265efa1b0
exporting mode analysis for use in prolog generation
bulwahn
parents:
38864
diff
changeset

61 
type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list 
2eb265efa1b0
exporting mode analysis for use in prolog generation
bulwahn
parents:
38864
diff
changeset

62 

32667  63 
end; 
64 

65 
structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE = 

66 
struct 

67 

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

68 
open Predicate_Compile_Aux; 
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
40051
diff
changeset

69 
open Core_Data; 
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
40051
diff
changeset

70 
open Mode_Inference; 
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
40051
diff
changeset

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

72 

32667  73 
(** fundamentals **) 
74 

75 
(* syntactic operations *) 

76 

77 
fun mk_eq (x, xs) = 

78 
let fun mk_eqs _ [] = [] 

79 
 mk_eqs a (b::cs) = 

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

81 
in mk_eqs x xs end; 

82 

83 
fun mk_scomp (t, u) = 

84 
let 

85 
val T = fastype_of t 

86 
val U = fastype_of u 

87 
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

88 
val D = body_type U 
32667  89 
in 
90 
Const (@{const_name "scomp"}, T > U > A > D) $ t $ u 

91 
end; 

92 

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

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37591
diff
changeset

94 
Type (@{type_name Product_Type.prod}, [Type (@{type_name Product_Type.prod}, [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T 
32667  95 
 dest_randomT T = raise TYPE ("dest_randomT", [T], []) 
96 

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

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

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

99 
@{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

100 

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

101 
(* representation of inferred clauses with modes *) 
32667  102 

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

103 
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

104 

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

105 
type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list 
32667  106 

107 
(* diagnostic display functions *) 

108 

37004  109 
fun print_modes options modes = 
33251  110 
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

111 
tracing ("Inferred modes:\n" ^ 
33251  112 
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

113 
(fn (p, m) => string_of_mode m ^ (if p then "pos" else "neg")) ms)) modes)) 
33251  114 
else () 
32667  115 

37004  116 
fun print_pred_mode_table string_of_entry pred_mode_table = 
32667  117 
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

118 
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

119 
^ string_of_entry pred mode entry 
32667  120 
fun print_pred (pred, modes) = 
121 
"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

122 
val _ = tracing (cat_lines (map print_pred pred_mode_table)) 
32667  123 
in () end; 
124 

37005
842a73dc6d0e
changing compilation to work only with contexts; adapting quickcheck
bulwahn
parents:
37004
diff
changeset

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

126 
if show_compilation options then 
37005
842a73dc6d0e
changing compilation to work only with contexts; adapting quickcheck
bulwahn
parents:
37004
diff
changeset

127 
print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term ctxt) 
33139
9c01ee6f8ee9
added skip_proof option; playing with compilation of depthlimited predicates
bulwahn
parents:
33138
diff
changeset

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

129 

37007
116670499530
changing operations for accessing data to work with contexts
bulwahn
parents:
37006
diff
changeset

130 
fun print_stored_rules ctxt = 
32667  131 
let 
42361  132 
val preds = Graph.keys (PredData.get (Proof_Context.theory_of ctxt)) 
32667  133 
fun print pred () = let 
134 
val _ = writeln ("predicate: " ^ pred) 

135 
val _ = writeln ("introrules: ") 

37007
116670499530
changing operations for accessing data to work with contexts
bulwahn
parents:
37006
diff
changeset

136 
val _ = fold (fn thm => fn u => writeln (Display.string_of_thm ctxt thm)) 
116670499530
changing operations for accessing data to work with contexts
bulwahn
parents:
37006
diff
changeset

137 
(rev (intros_of ctxt pred)) () 
32667  138 
in 
37007
116670499530
changing operations for accessing data to work with contexts
bulwahn
parents:
37006
diff
changeset

139 
if (has_elim ctxt pred) then 
116670499530
changing operations for accessing data to work with contexts
bulwahn
parents:
37006
diff
changeset

140 
writeln ("elimrule: " ^ Display.string_of_thm ctxt (the_elim_of ctxt pred)) 
32667  141 
else 
142 
writeln ("no elimrule defined") 

143 
end 

144 
in 

145 
fold print preds () 

146 
end; 

147 

37003
a393a588b82e
moving towards working with proof contexts in the predicate compiler
bulwahn
parents:
37002
diff
changeset

148 
fun print_all_modes compilation ctxt = 
32667  149 
let 
150 
val _ = writeln ("Inferred modes:") 

151 
fun print (pred, modes) u = 

152 
let 

153 
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

154 
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

155 
in u end 
32667  156 
in 
37003
a393a588b82e
moving towards working with proof contexts in the predicate compiler
bulwahn
parents:
37002
diff
changeset

157 
fold print (all_modes_of compilation ctxt) () 
32667  158 
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

159 

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

160 
(* validity checks *) 
07efd452a698
moved argument expected_modes into options; improved mode check to only check mode of the named predicate
bulwahn
parents:
33131
diff
changeset

161 

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

163 
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

164 
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

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

166 
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

167 
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

168 
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

169 
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

170 
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

171 
^ " 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

172 
^ " 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

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

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

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

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

177 

40138  178 
fun check_proposed_modes options preds modes errors = 
39382
c797f3ab2ae1
proposed modes for code_pred now supports modes for mutual predicates
bulwahn
parents:
39310
diff
changeset

179 
map (fn (s, _) => case proposed_modes options s of 
c797f3ab2ae1
proposed modes for code_pred now supports modes for mutual predicates
bulwahn
parents:
39310
diff
changeset

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

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

182 
let 
39201
234e6ef4ff67
using the proposed modes for starting the fixpoint iteration in the mode analysis
bulwahn
parents:
39194
diff
changeset

183 
val preds_without_modes = map fst (filter (null o snd) 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

184 
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

185 
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

186 
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

187 
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

188 
^ " 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

189 
^ " expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms) ^ "\n" 
39383
ddfafa97da2f
adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents:
39382
diff
changeset

190 
^ (if show_invalid_clauses options then 
ddfafa97da2f
adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents:
39382
diff
changeset

191 
("For the following clauses, the following modes could not be inferred: " ^ "\n" 
ddfafa97da2f
adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents:
39382
diff
changeset

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

193 
(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

194 
"\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

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

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

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

198 
 NONE => ()) 
39382
c797f3ab2ae1
proposed modes for code_pred now supports modes for mutual predicates
bulwahn
parents:
39310
diff
changeset

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

200 

39651
2e06dad03dd3
adding check if usergiven modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents:
39649
diff
changeset

201 
fun check_matches_type ctxt predname T ms = 
2e06dad03dd3
adding check if usergiven modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents:
39649
diff
changeset

202 
let 
2e06dad03dd3
adding check if usergiven modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents:
39649
diff
changeset

203 
fun check (m as Fun (m1, m2)) (Type("fun", [T1,T2])) = check m1 T1 andalso check m2 T2 
39763
03f95582ef63
weakening check for higherorder relations, but adding check for consistent modes
bulwahn
parents:
39762
diff
changeset

204 
 check m (T as Type("fun", _)) = (m = Input orelse m = Output) 
39651
2e06dad03dd3
adding check if usergiven modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents:
39649
diff
changeset

205 
 check (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) = 
2e06dad03dd3
adding check if usergiven modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents:
39649
diff
changeset

206 
check m1 T1 andalso check m2 T2 
2e06dad03dd3
adding check if usergiven modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents:
39649
diff
changeset

207 
 check Input T = true 
2e06dad03dd3
adding check if usergiven modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents:
39649
diff
changeset

208 
 check Output T = true 
2e06dad03dd3
adding check if usergiven modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents:
39649
diff
changeset

209 
 check Bool @{typ bool} = true 
2e06dad03dd3
adding check if usergiven modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents:
39649
diff
changeset

210 
 check _ _ = false 
39763
03f95582ef63
weakening check for higherorder relations, but adding check for consistent modes
bulwahn
parents:
39762
diff
changeset

211 
fun check_consistent_modes ms = 
03f95582ef63
weakening check for higherorder relations, but adding check for consistent modes
bulwahn
parents:
39762
diff
changeset

212 
if forall (fn Fun (m1', m2') => true  _ => false) ms then 
03f95582ef63
weakening check for higherorder relations, but adding check for consistent modes
bulwahn
parents:
39762
diff
changeset

213 
pairself check_consistent_modes (split_list (map (fn Fun (m1, m2) => (m1, m2)) ms)) 
03f95582ef63
weakening check for higherorder relations, but adding check for consistent modes
bulwahn
parents:
39762
diff
changeset

214 
> (fn (res1, res2) => res1 andalso res2) 
03f95582ef63
weakening check for higherorder relations, but adding check for consistent modes
bulwahn
parents:
39762
diff
changeset

215 
else if forall (fn Input => true  Output => true  Pair _ => true  _ => false) ms then 
03f95582ef63
weakening check for higherorder relations, but adding check for consistent modes
bulwahn
parents:
39762
diff
changeset

216 
true 
03f95582ef63
weakening check for higherorder relations, but adding check for consistent modes
bulwahn
parents:
39762
diff
changeset

217 
else if forall (fn Bool => true  _ => false) ms then 
03f95582ef63
weakening check for higherorder relations, but adding check for consistent modes
bulwahn
parents:
39762
diff
changeset

218 
true 
03f95582ef63
weakening check for higherorder relations, but adding check for consistent modes
bulwahn
parents:
39762
diff
changeset

219 
else 
03f95582ef63
weakening check for higherorder relations, but adding check for consistent modes
bulwahn
parents:
39762
diff
changeset

220 
false 
39651
2e06dad03dd3
adding check if usergiven modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents:
39649
diff
changeset

221 
val _ = map 
2e06dad03dd3
adding check if usergiven modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents:
39649
diff
changeset

222 
(fn mode => 
39763
03f95582ef63
weakening check for higherorder relations, but adding check for consistent modes
bulwahn
parents:
39762
diff
changeset

223 
if length (strip_fun_mode mode) = length (binder_types T) 
03f95582ef63
weakening check for higherorder relations, but adding check for consistent modes
bulwahn
parents:
39762
diff
changeset

224 
andalso (forall (uncurry check) (strip_fun_mode mode ~~ binder_types T)) then () 
39651
2e06dad03dd3
adding check if usergiven modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents:
39649
diff
changeset

225 
else error (string_of_mode mode ^ " is not a valid mode for " ^ Syntax.string_of_typ ctxt T 
2e06dad03dd3
adding check if usergiven modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents:
39649
diff
changeset

226 
^ " at predicate " ^ predname)) ms 
39763
03f95582ef63
weakening check for higherorder relations, but adding check for consistent modes
bulwahn
parents:
39762
diff
changeset

227 
val _ = 
03f95582ef63
weakening check for higherorder relations, but adding check for consistent modes
bulwahn
parents:
39762
diff
changeset

228 
if check_consistent_modes ms then () 
03f95582ef63
weakening check for higherorder relations, but adding check for consistent modes
bulwahn
parents:
39762
diff
changeset

229 
else error (commas (map string_of_mode ms) ^ 
03f95582ef63
weakening check for higherorder relations, but adding check for consistent modes
bulwahn
parents:
39762
diff
changeset

230 
" are inconsistent modes for predicate " ^ predname) 
39651
2e06dad03dd3
adding check if usergiven modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents:
39649
diff
changeset

231 
in 
2e06dad03dd3
adding check if usergiven modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents:
39649
diff
changeset

232 
ms 
2e06dad03dd3
adding check if usergiven modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents:
39649
diff
changeset

233 
end 
2e06dad03dd3
adding check if usergiven modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents:
39649
diff
changeset

234 

36019
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

235 
(* compilation modifiers *) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

236 

64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

237 
structure Comp_Mod = 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

238 
struct 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

239 

64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

240 
datatype comp_modifiers = Comp_Modifiers of 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

241 
{ 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

242 
compilation : compilation, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

243 
function_name_prefix : string, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

244 
compfuns : compilation_funs, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

245 
mk_random : typ > term list > term, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

246 
modify_funT : typ > typ, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

247 
additional_arguments : string list > term list, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

248 
wrap_compilation : compilation_funs > string > typ > mode > term list > term > term, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

249 
transform_additional_arguments : indprem > term list > term list 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

250 
} 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

251 

64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

252 
fun dest_comp_modifiers (Comp_Modifiers c) = c 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

253 

64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

254 
val compilation = #compilation o dest_comp_modifiers 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

255 
val function_name_prefix = #function_name_prefix o dest_comp_modifiers 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

256 
val compfuns = #compfuns o dest_comp_modifiers 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

257 

64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

258 
val mk_random = #mk_random o dest_comp_modifiers 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

259 
val funT_of' = funT_of o compfuns 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

260 
val modify_funT = #modify_funT o dest_comp_modifiers 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

261 
fun funT_of comp mode = modify_funT comp o funT_of' comp mode 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

262 

64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

263 
val additional_arguments = #additional_arguments o dest_comp_modifiers 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

264 
val wrap_compilation = #wrap_compilation o dest_comp_modifiers 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

265 
val transform_additional_arguments = #transform_additional_arguments o dest_comp_modifiers 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

266 

40049
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

267 
fun set_compfuns compfuns' (Comp_Modifiers {compilation, function_name_prefix, compfuns, mk_random, 
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

268 
modify_funT, additional_arguments, wrap_compilation, transform_additional_arguments}) = 
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

269 
(Comp_Modifiers {compilation = compilation, function_name_prefix = function_name_prefix, 
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

270 
compfuns = compfuns', mk_random = mk_random, modify_funT = modify_funT, 
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

271 
additional_arguments = additional_arguments, wrap_compilation = wrap_compilation, 
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

272 
transform_additional_arguments = transform_additional_arguments}) 
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

273 

36019
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

274 
end; 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

275 

40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

276 
fun unlimited_compfuns_of true New_Pos_Random_DSeq = 
40049
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

277 
New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns 
40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

278 
 unlimited_compfuns_of false New_Pos_Random_DSeq = 
40049
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

279 
New_Neg_Random_Sequence_CompFuns.depth_unlimited_compfuns 
40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

280 
 unlimited_compfuns_of true Pos_Generator_DSeq = 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

281 
New_Pos_DSequence_CompFuns.depth_unlimited_compfuns 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

282 
 unlimited_compfuns_of false Pos_Generator_DSeq = 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

283 
New_Neg_DSequence_CompFuns.depth_unlimited_compfuns 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

284 
 unlimited_compfuns_of _ c = 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

285 
raise Fail ("No unlimited compfuns for compilation " ^ string_of_compilation c) 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

286 

40049
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

287 
fun limited_compfuns_of true Predicate_Compile_Aux.New_Pos_Random_DSeq = 
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

288 
New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns 
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

289 
 limited_compfuns_of false Predicate_Compile_Aux.New_Pos_Random_DSeq = 
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

290 
New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns 
40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

291 
 limited_compfuns_of true Pos_Generator_DSeq = 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

292 
New_Pos_DSequence_CompFuns.depth_limited_compfuns 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

293 
 limited_compfuns_of false Pos_Generator_DSeq = 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

294 
New_Neg_DSequence_CompFuns.depth_limited_compfuns 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

295 
 limited_compfuns_of _ c = 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

296 
raise Fail ("No limited compfuns for compilation " ^ string_of_compilation c) 
40049
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

297 

36019
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

298 
val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

299 
{ 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

300 
compilation = Depth_Limited, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

301 
function_name_prefix = "depth_limited_", 
45450  302 
compfuns = Predicate_Comp_Funs.compfuns, 
36019
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

303 
mk_random = (fn _ => error "no random generation"), 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

304 
additional_arguments = fn names => 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

305 
let 
43324
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
43253
diff
changeset

306 
val depth_name = singleton (Name.variant_list names) "depth" 
36019
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

307 
in [Free (depth_name, @{typ code_numeral})] end, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

308 
modify_funT = (fn T => let val (Ts, U) = strip_type T 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

309 
val Ts' = [@{typ code_numeral}] in (Ts @ Ts') > U end), 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

310 
wrap_compilation = 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

311 
fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation => 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

312 
let 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

313 
val [depth] = additional_arguments 
40139  314 
val (_, Ts) = split_modeT mode (binder_types T) 
36019
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

315 
val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

316 
val if_const = Const (@{const_name "If"}, @{typ bool} > T' > T' > T') 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

317 
in 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

318 
if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"}) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

319 
$ mk_bot compfuns (dest_predT compfuns T') 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

320 
$ compilation 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

321 
end, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

322 
transform_additional_arguments = 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

323 
fn prem => fn additional_arguments => 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

324 
let 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

325 
val [depth] = additional_arguments 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

326 
val depth' = 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

327 
Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"}) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

328 
$ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"}) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

329 
in [depth'] end 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

330 
} 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

331 

64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

332 
val random_comp_modifiers = Comp_Mod.Comp_Modifiers 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

333 
{ 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

334 
compilation = Random, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

335 
function_name_prefix = "random_", 
45450  336 
compfuns = Predicate_Comp_Funs.compfuns, 
36019
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

337 
mk_random = (fn T => fn additional_arguments => 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

338 
list_comb (Const(@{const_name Quickcheck.iter}, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

339 
[@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] > 
45450  340 
Predicate_Comp_Funs.mk_predT T), additional_arguments)), 
36019
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

341 
modify_funT = (fn T => 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

342 
let 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

343 
val (Ts, U) = strip_type T 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

344 
val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ "code_numeral * code_numeral"}] 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

345 
in (Ts @ Ts') > U end), 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

346 
additional_arguments = (fn names => 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

347 
let 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

348 
val [nrandom, size, seed] = Name.variant_list names ["nrandom", "size", "seed"] 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

349 
in 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

350 
[Free (nrandom, @{typ code_numeral}), Free (size, @{typ code_numeral}), 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

351 
Free (seed, @{typ "code_numeral * code_numeral"})] 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

352 
end), 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

353 
wrap_compilation = K (K (K (K (K I)))) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

354 
: (compilation_funs > string > typ > mode > term list > term > term), 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

355 
transform_additional_arguments = K I : (indprem > term list > term list) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

356 
} 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

357 

64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

358 
val depth_limited_random_comp_modifiers = Comp_Mod.Comp_Modifiers 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

359 
{ 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

360 
compilation = Depth_Limited_Random, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

361 
function_name_prefix = "depth_limited_random_", 
45450  362 
compfuns = Predicate_Comp_Funs.compfuns, 
36019
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

363 
mk_random = (fn T => fn additional_arguments => 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

364 
list_comb (Const(@{const_name Quickcheck.iter}, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

365 
[@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] > 
45450  366 
Predicate_Comp_Funs.mk_predT T), tl additional_arguments)), 
36019
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

367 
modify_funT = (fn T => 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

368 
let 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

369 
val (Ts, U) = strip_type T 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

370 
val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral}, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

371 
@{typ "code_numeral * code_numeral"}] 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

372 
in (Ts @ Ts') > U end), 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

373 
additional_arguments = (fn names => 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

374 
let 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

375 
val [depth, nrandom, size, seed] = Name.variant_list names ["depth", "nrandom", "size", "seed"] 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

376 
in 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

377 
[Free (depth, @{typ code_numeral}), Free (nrandom, @{typ code_numeral}), 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

378 
Free (size, @{typ code_numeral}), Free (seed, @{typ "code_numeral * code_numeral"})] 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

379 
end), 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

380 
wrap_compilation = 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

381 
fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation => 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

382 
let 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

383 
val depth = hd (additional_arguments) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

384 
val (_, Ts) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

385 
mode (binder_types T) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

386 
val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

387 
val if_const = Const (@{const_name "If"}, @{typ bool} > T' > T' > T') 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

388 
in 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

389 
if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"}) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

390 
$ mk_bot compfuns (dest_predT compfuns T') 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

391 
$ compilation 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

392 
end, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

393 
transform_additional_arguments = 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

394 
fn prem => fn additional_arguments => 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

395 
let 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

396 
val [depth, nrandom, size, seed] = additional_arguments 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

397 
val depth' = 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

398 
Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"}) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

399 
$ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"}) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

400 
in [depth', nrandom, size, seed] end 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

401 
} 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

402 

64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

403 
val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

404 
{ 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

405 
compilation = Pred, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

406 
function_name_prefix = "", 
45450  407 
compfuns = Predicate_Comp_Funs.compfuns, 
36019
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

408 
mk_random = (fn _ => error "no random generation"), 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

409 
modify_funT = I, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

410 
additional_arguments = K [], 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

411 
wrap_compilation = K (K (K (K (K I)))) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

412 
: (compilation_funs > string > typ > mode > term list > term > term), 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

413 
transform_additional_arguments = K I : (indprem > term list > term list) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

414 
} 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

415 

64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

416 
val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

417 
{ 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

418 
compilation = Annotated, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

419 
function_name_prefix = "annotated_", 
45450  420 
compfuns = Predicate_Comp_Funs.compfuns, 
36019
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

421 
mk_random = (fn _ => error "no random generation"), 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

422 
modify_funT = I, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

423 
additional_arguments = K [], 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

424 
wrap_compilation = 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

425 
fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation => 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

426 
mk_tracing ("calling predicate " ^ s ^ 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

427 
" with mode " ^ string_of_mode mode) compilation, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

428 
transform_additional_arguments = K I : (indprem > term list > term list) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

429 
} 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

430 

64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

431 
val dseq_comp_modifiers = Comp_Mod.Comp_Modifiers 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

432 
{ 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

433 
compilation = DSeq, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

434 
function_name_prefix = "dseq_", 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

435 
compfuns = DSequence_CompFuns.compfuns, 
40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

436 
mk_random = (fn _ => error "no random generation in dseq"), 
36019
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

437 
modify_funT = I, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

438 
additional_arguments = K [], 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

439 
wrap_compilation = K (K (K (K (K I)))) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

440 
: (compilation_funs > string > typ > mode > term list > term > term), 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

441 
transform_additional_arguments = K I : (indprem > term list > term list) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

442 
} 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

443 

64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

444 
val pos_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

445 
{ 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

446 
compilation = Pos_Random_DSeq, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

447 
function_name_prefix = "random_dseq_", 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

448 
compfuns = Random_Sequence_CompFuns.compfuns, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

449 
mk_random = (fn T => fn additional_arguments => 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

450 
let 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

451 
val random = Const ("Quickcheck.random_class.random", 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

452 
@{typ code_numeral} > @{typ Random.seed} > 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

453 
HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

454 
in 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

455 
Const ("Random_Sequence.Random", (@{typ code_numeral} > @{typ Random.seed} > 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

456 
HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) > 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

457 
Random_Sequence_CompFuns.mk_random_dseqT T) $ random 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

458 
end), 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

459 

64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

460 
modify_funT = I, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

461 
additional_arguments = K [], 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

462 
wrap_compilation = K (K (K (K (K I)))) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

463 
: (compilation_funs > string > typ > mode > term list > term > term), 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

464 
transform_additional_arguments = K I : (indprem > term list > term list) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

465 
} 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

466 

64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

467 
val neg_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

468 
{ 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

469 
compilation = Neg_Random_DSeq, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

470 
function_name_prefix = "random_dseq_neg_", 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

471 
compfuns = Random_Sequence_CompFuns.compfuns, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

472 
mk_random = (fn _ => error "no random generation"), 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

473 
modify_funT = I, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

474 
additional_arguments = K [], 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

475 
wrap_compilation = K (K (K (K (K I)))) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

476 
: (compilation_funs > string > typ > mode > term list > term > term), 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

477 
transform_additional_arguments = K I : (indprem > term list > term list) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

478 
} 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

479 

64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

480 

64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

481 
val new_pos_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

482 
{ 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

483 
compilation = New_Pos_Random_DSeq, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

484 
function_name_prefix = "new_random_dseq_", 
40049
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

485 
compfuns = New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns, 
36019
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

486 
mk_random = (fn T => fn additional_arguments => 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

487 
let 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

488 
val random = Const ("Quickcheck.random_class.random", 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

489 
@{typ code_numeral} > @{typ Random.seed} > 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

490 
HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

491 
in 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

492 
Const ("New_Random_Sequence.Random", (@{typ code_numeral} > @{typ Random.seed} > 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

493 
HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) > 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

494 
New_Pos_Random_Sequence_CompFuns.mk_pos_random_dseqT T) $ random 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

495 
end), 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

496 
modify_funT = I, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

497 
additional_arguments = K [], 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

498 
wrap_compilation = K (K (K (K (K I)))) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

499 
: (compilation_funs > string > typ > mode > term list > term > term), 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

500 
transform_additional_arguments = K I : (indprem > term list > term list) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

501 
} 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

502 

64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

503 
val new_neg_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

504 
{ 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

505 
compilation = New_Neg_Random_DSeq, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

506 
function_name_prefix = "new_random_dseq_neg_", 
40049
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

507 
compfuns = New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns, 
36019
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

508 
mk_random = (fn _ => error "no random generation"), 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

509 
modify_funT = I, 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

510 
additional_arguments = K [], 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

511 
wrap_compilation = K (K (K (K (K I)))) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

512 
: (compilation_funs > string > typ > mode > term list > term > term), 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

513 
transform_additional_arguments = K I : (indprem > term list > term list) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

514 
} 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

515 

40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

516 
val pos_generator_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

517 
{ 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

518 
compilation = Pos_Generator_DSeq, 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

519 
function_name_prefix = "generator_dseq_", 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

520 
compfuns = New_Pos_DSequence_CompFuns.depth_limited_compfuns, 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

521 
mk_random = 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

522 
(fn T => fn additional_arguments => 
45214  523 
Const (@{const_name "Lazy_Sequence.small_lazy_class.small_lazy"}, 
524 
@{typ "Code_Numeral.code_numeral"} > Type (@{type_name "Lazy_Sequence.lazy_sequence"}, [T]))), 

40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

525 
modify_funT = I, 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

526 
additional_arguments = K [], 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

527 
wrap_compilation = K (K (K (K (K I)))) 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

528 
: (compilation_funs > string > typ > mode > term list > term > term), 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

529 
transform_additional_arguments = K I : (indprem > term list > term list) 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

530 
} 
45450  531 

40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

532 
val neg_generator_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

533 
{ 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

534 
compilation = Neg_Generator_DSeq, 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

535 
function_name_prefix = "generator_dseq_neg_", 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

536 
compfuns = New_Neg_DSequence_CompFuns.depth_limited_compfuns, 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

537 
mk_random = (fn _ => error "no random generation"), 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

538 
modify_funT = I, 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

539 
additional_arguments = K [], 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

540 
wrap_compilation = K (K (K (K (K I)))) 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

541 
: (compilation_funs > string > typ > mode > term list > term > term), 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

542 
transform_additional_arguments = K I : (indprem > term list > term list) 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

543 
} 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

544 

45450  545 
val pos_generator_cps_comp_modifiers = Comp_Mod.Comp_Modifiers 
546 
{ 

547 
compilation = Pos_Generator_CPS, 

548 
function_name_prefix = "generator_cps_pos_", 

549 
compfuns = Pos_Bounded_CPS_Comp_Funs.compfuns, 

550 
mk_random = 

551 
(fn T => fn additional_arguments => 

552 
Const (@{const_name "Quickcheck_Exhaustive.exhaustive"}, 

553 
(T > @{typ "term list option"}) > @{typ "code_numeral => term list option"})), 

554 
modify_funT = I, 

555 
additional_arguments = K [], 

556 
wrap_compilation = K (K (K (K (K I)))) 

557 
: (compilation_funs > string > typ > mode > term list > term > term), 

558 
transform_additional_arguments = K I : (indprem > term list > term list) 

559 
} 

560 

561 
val neg_generator_cps_comp_modifiers = Comp_Mod.Comp_Modifiers 

562 
{ 

563 
compilation = Neg_Generator_CPS, 

564 
function_name_prefix = "generator_cps_neg_", 

565 
compfuns = Neg_Bounded_CPS_Comp_Funs.compfuns, 

566 
mk_random = (fn _ => error "No enumerators"), 

567 
modify_funT = I, 

568 
additional_arguments = K [], 

569 
wrap_compilation = K (K (K (K (K I)))) 

570 
: (compilation_funs > string > typ > mode > term list > term > term), 

571 
transform_additional_arguments = K I : (indprem > term list > term list) 

572 
} 

573 

36019
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

574 
fun negative_comp_modifiers_of comp_modifiers = 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

575 
(case Comp_Mod.compilation comp_modifiers of 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

576 
Pos_Random_DSeq => neg_random_dseq_comp_modifiers 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

577 
 Neg_Random_DSeq => pos_random_dseq_comp_modifiers 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

578 
 New_Pos_Random_DSeq => new_neg_random_dseq_comp_modifiers 
40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

579 
 New_Neg_Random_DSeq => new_pos_random_dseq_comp_modifiers 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

580 
 Pos_Generator_DSeq => neg_generator_dseq_comp_modifiers 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
40050
diff
changeset

581 
 Neg_Generator_DSeq => pos_generator_dseq_comp_modifiers 
45450  582 
 Pos_Generator_CPS => neg_generator_cps_comp_modifiers 
583 
 Neg_Generator_CPS => pos_generator_cps_comp_modifiers 

36019
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

584 
 c => comp_modifiers) 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

585 

32667  586 
(* term construction *) 
587 

588 
fun mk_v (names, vs) s T = (case AList.lookup (op =) vs s of 

589 
NONE => (Free (s, T), (names, (s, [])::vs)) 

590 
 SOME xs => 

591 
let 

43324
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
43253
diff
changeset

592 
val s' = singleton (Name.variant_list names) s; 
32667  593 
val v = Free (s', T) 
594 
in 

595 
(v, (s'::names, AList.update (op =) (s, v::xs) vs)) 

596 
end); 

597 

598 
fun distinct_v (Free (s, T)) nvs = mk_v nvs s T 

599 
 distinct_v (t $ u) nvs = 

600 
let 

601 
val (t', nvs') = distinct_v t nvs; 

602 
val (u', nvs'') = distinct_v u nvs'; 

603 
in (t' $ u', nvs'') end 

604 
 distinct_v x nvs = (x, nvs); 

605 

33147
180dc60bd88c
improving the compilation with higherorder arguments in the predicate compiler
bulwahn
parents:
33146
diff
changeset

606 

39648
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

607 
(** specific rpred functions  move them to the correct place in this file *) 
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

608 
fun mk_Eval_of (P as (Free (f, _)), T) mode = 
44241  609 
let 
610 
fun mk_bounds (Type (@{type_name Product_Type.prod}, [T1, T2])) i = 

611 
let 

612 
val (bs2, i') = mk_bounds T2 i 

613 
val (bs1, i'') = mk_bounds T1 i' 

614 
in 

615 
(HOLogic.pair_const T1 T2 $ bs1 $ bs2, i'' + 1) 

616 
end 

617 
 mk_bounds T i = (Bound i, i + 1) 

618 
fun mk_prod ((t1, T1), (t2, T2)) = (HOLogic.pair_const T1 T2 $ t1 $ t2, HOLogic.mk_prodT (T1, T2)) 

619 
fun mk_tuple [] = (HOLogic.unit, HOLogic.unitT) 

620 
 mk_tuple tTs = foldr1 mk_prod tTs 

621 
fun mk_split_abs (T as Type (@{type_name Product_Type.prod}, [T1, T2])) t = 

622 
absdummy T 

623 
(HOLogic.split_const (T1, T2, @{typ bool}) $ (mk_split_abs T1 (mk_split_abs T2 t))) 

624 
 mk_split_abs T t = absdummy T t 

625 
val args = rev (fst (fold_map mk_bounds (rev (binder_types T)) 0)) 

626 
val (inargs, outargs) = split_mode mode args 

627 
val (inTs, outTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) mode (binder_types T) 

45450  628 
val inner_term = Predicate_Comp_Funs.mk_Eval (list_comb (P, inargs), fst (mk_tuple (outargs ~~ outTs))) 
44241  629 
in 
630 
fold_rev mk_split_abs (binder_types T) inner_term 

631 
end 

33147
180dc60bd88c
improving the compilation with higherorder arguments in the predicate compiler
bulwahn
parents:
33146
diff
changeset

632 

39648
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

633 
fun compile_arg compilation_modifiers additional_arguments ctxt param_modes arg = 
33147
180dc60bd88c
improving the compilation with higherorder arguments in the predicate compiler
bulwahn
parents:
33146
diff
changeset

634 
let 
180dc60bd88c
improving the compilation with higherorder arguments in the predicate compiler
bulwahn
parents:
33146
diff
changeset

635 
fun map_params (t as Free (f, T)) = 
39648
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

636 
(case (AList.lookup (op =) param_modes f) of 
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

637 
SOME mode => 
33147
180dc60bd88c
improving the compilation with higherorder arguments in the predicate compiler
bulwahn
parents:
33146
diff
changeset

638 
let 
39648
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

639 
val T' = Comp_Mod.funT_of compilation_modifiers mode T 
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

640 
in 
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

641 
mk_Eval_of (Free (f, T'), T) mode 
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

642 
end 
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

643 
 NONE => t) 
33147
180dc60bd88c
improving the compilation with higherorder arguments in the predicate compiler
bulwahn
parents:
33146
diff
changeset

644 
 map_params t = t 
39648
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

645 
in 
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

646 
map_aterms map_params arg 
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

647 
end 
33147
180dc60bd88c
improving the compilation with higherorder arguments in the predicate compiler
bulwahn
parents:
33146
diff
changeset

648 

39648
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

649 
fun compile_match compilation_modifiers additional_arguments ctxt param_modes 
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

650 
eqs eqs' out_ts success_t = 
32667  651 
let 
36019
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

652 
val compfuns = Comp_Mod.compfuns compilation_modifiers 
32667  653 
val eqs'' = maps mk_eq eqs @ eqs' 
33147
180dc60bd88c
improving the compilation with higherorder arguments in the predicate compiler
bulwahn
parents:
33146
diff
changeset

654 
val eqs'' = 
39648
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

655 
map (compile_arg compilation_modifiers additional_arguments ctxt param_modes) eqs'' 
32667  656 
val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) []; 
43324
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
43253
diff
changeset

657 
val name = singleton (Name.variant_list names) "x"; 
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
43253
diff
changeset

658 
val name' = singleton (Name.variant_list (name :: names)) "y"; 
33148
0808f7d0d0d7
removed tuple functions from the predicate compiler
bulwahn
parents:
33147
diff
changeset

659 
val T = HOLogic.mk_tupleT (map fastype_of out_ts); 
32667  660 
val U = fastype_of success_t; 
36254  661 
val U' = dest_predT compfuns U; 
32667  662 
val v = Free (name, T); 
663 
val v' = Free (name', T); 

664 
in 

43253
fa3c61dc9f2c
removed generation of instantiated pattern set, which is never actually used
krauss
parents:
43123
diff
changeset

665 
lambda v (Datatype.make_case ctxt Datatype_Case.Quiet [] v 
33148
0808f7d0d0d7
removed tuple functions from the predicate compiler
bulwahn
parents:
33147
diff
changeset

666 
[(HOLogic.mk_tuple out_ts, 
32667  667 
if null eqs'' then success_t 
668 
else Const (@{const_name HOL.If}, HOLogic.boolT > U > U > U) $ 

669 
foldr1 HOLogic.mk_conj eqs'' $ success_t $ 

670 
mk_bot compfuns U'), 

43253
fa3c61dc9f2c
removed generation of instantiated pattern set, which is never actually used
krauss
parents:
43123
diff
changeset

671 
(v', mk_bot compfuns U')]) 
32667  672 
end; 
673 

35891
3122bdd95275
contextifying the compilation of the predicate compiler
bulwahn
parents:
35889
diff
changeset

674 
fun string_of_tderiv ctxt (t, deriv) = 
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

675 
(case (t, deriv) 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

676 
(t1 $ t2, Mode_App (deriv1, deriv2)) => 
35891
3122bdd95275
contextifying the compilation of the predicate compiler
bulwahn
parents:
35889
diff
changeset

677 
string_of_tderiv ctxt (t1, deriv1) ^ " $ " ^ string_of_tderiv ctxt (t2, deriv2) 
37391  678 
 (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (deriv1, deriv2)) => 
35891
3122bdd95275
contextifying the compilation of the predicate compiler
bulwahn
parents:
35889
diff
changeset

679 
"(" ^ string_of_tderiv ctxt (t1, deriv1) ^ ", " ^ string_of_tderiv ctxt (t2, deriv2) ^ ")" 
3122bdd95275
contextifying the compilation of the predicate compiler
bulwahn
parents:
35889
diff
changeset

680 
 (t, Term Input) => Syntax.string_of_term ctxt t ^ "[Input]" 
3122bdd95275
contextifying the compilation of the predicate compiler
bulwahn
parents:
35889
diff
changeset

681 
 (t, Term Output) => Syntax.string_of_term ctxt t ^ "[Output]" 
3122bdd95275
contextifying the compilation of the predicate compiler
bulwahn
parents:
35889
diff
changeset

682 
 (t, Context m) => Syntax.string_of_term ctxt t ^ "[" ^ string_of_mode 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

683 

39648
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

684 
fun compile_expr compilation_modifiers ctxt (t, deriv) param_modes additional_arguments = 
32667  685 
let 
36019
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

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

687 
fun expr_of (t, deriv) = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

688 
(case (t, deriv) of 
39648
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

689 
(t, Term Input) => SOME (compile_arg compilation_modifiers additional_arguments ctxt param_modes 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

690 
 (t, Term Output) => NONE 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

691 
 (Const (name, T), Context mode) => 
37003
a393a588b82e
moving towards working with proof contexts in the predicate compiler
bulwahn
parents:
37002
diff
changeset

692 
(case alternative_compilation_of ctxt name mode of 
36038
385f706eff24
generalized alternative functions to alternative compilation to handle arithmetic functions better
bulwahn
parents:
36037
diff
changeset

693 
SOME alt_comp => SOME (alt_comp compfuns T) 
36034
ee84eac07290
added bookkeeping, registration and compilation with alternative functions for predicates in the predicate compiler
bulwahn
parents:
36031
diff
changeset

694 
 NONE => 
ee84eac07290
added bookkeeping, registration and compilation with alternative functions for predicates in the predicate compiler
bulwahn
parents:
36031
diff
changeset

695 
SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers) 
37003
a393a588b82e
moving towards working with proof contexts in the predicate compiler
bulwahn
parents:
37002
diff
changeset

696 
ctxt name mode, 
36034
ee84eac07290
added bookkeeping, registration and compilation with alternative functions for predicates in the predicate compiler
bulwahn
parents:
36031
diff
changeset

697 
Comp_Mod.funT_of compilation_modifiers mode 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

698 
 (Free (s, T), Context m) => 
39785
05c4e9ecf5f6
improving the compilation to handle predicate arguments in higherorder argument positions
bulwahn
parents:
39783
diff
changeset

699 
(case (AList.lookup (op =) param_modes s) of 
05c4e9ecf5f6
improving the compilation to handle predicate arguments in higherorder argument positions
bulwahn
parents:
39783
diff
changeset

700 
SOME mode => SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T)) 
05c4e9ecf5f6
improving the compilation to handle predicate arguments in higherorder argument positions
bulwahn
parents:
39783
diff
changeset

701 
 NONE => 
05c4e9ecf5f6
improving the compilation to handle predicate arguments in higherorder argument positions
bulwahn
parents:
39783
diff
changeset

702 
let 
05c4e9ecf5f6
improving the compilation to handle predicate arguments in higherorder argument positions
bulwahn
parents:
39783
diff
changeset

703 
val bs = map (pair "x") (binder_types (fastype_of t)) 
05c4e9ecf5f6
improving the compilation to handle predicate arguments in higherorder argument positions
bulwahn
parents:
39783
diff
changeset

704 
val bounds = map Bound (rev (0 upto (length bs)  1)) 
05c4e9ecf5f6
improving the compilation to handle predicate arguments in higherorder argument positions
bulwahn
parents:
39783
diff
changeset

705 
in SOME (list_abs (bs, mk_if compfuns (list_comb (t, bounds)))) 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

706 
 (t, Context m) => 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

708 
val bs = map (pair "x") (binder_types (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

709 
val bounds = map Bound (rev (0 upto (length bs)  1)) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

710 
in SOME (list_abs (bs, mk_if compfuns (list_comb (t, bounds)))) end 
37391  711 
 (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (d1, d2)) => 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

712 
(case (expr_of (t1, d1), expr_of (t2, d2)) of 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

713 
(NONE, NONE) => NONE 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

714 
 (NONE, SOME t) => SOME t 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

715 
 (SOME t, NONE) => SOME t 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

716 
 (SOME t1, SOME t2) => SOME (HOLogic.mk_prod (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

717 
 (t1 $ t2, Mode_App (deriv1, deriv2)) => 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

718 
(case (expr_of (t1, deriv1), expr_of (t2, deriv2)) of 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

719 
(SOME t, NONE) => SOME t 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

720 
 (SOME t, SOME u) => SOME (t $ u) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

721 
 _ => error "something went wrong here!")) 
32667  722 
in 
35879
99818df5b8f5
reviving the classical depthlimited computation in the predicate compiler
bulwahn
parents:
35845
diff
changeset

723 
list_comb (the (expr_of (t, deriv)), additional_arguments) 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

724 
end 
33145  725 

39648
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

726 
fun compile_clause compilation_modifiers ctxt all_vs param_modes additional_arguments 
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

727 
inp (in_ts, out_ts) moded_ps = 
32667  728 
let 
36019
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

729 
val compfuns = Comp_Mod.compfuns compilation_modifiers 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

730 
val compile_match = compile_match compilation_modifiers 
39648
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

731 
additional_arguments ctxt param_modes 
32667  732 
val (in_ts', (all_vs', eqs)) = 
35891
3122bdd95275
contextifying the compilation of the predicate compiler
bulwahn
parents:
35889
diff
changeset

733 
fold_map (collect_non_invertible_subterms ctxt) in_ts (all_vs, []); 
32667  734 
fun compile_prems out_ts' vs names [] = 
735 
let 

736 
val (out_ts'', (names', eqs')) = 

35891
3122bdd95275
contextifying the compilation of the predicate compiler
bulwahn
parents:
35889
diff
changeset

737 
fold_map (collect_non_invertible_subterms ctxt) out_ts' (names, []); 
32667  738 
val (out_ts''', (names'', constr_vs)) = fold_map distinct_v 
739 
out_ts'' (names', map (rpair []) vs); 

39762
02fb709ab3cb
handling higherorder relations in output terms; improving proof procedure; added test case
bulwahn
parents:
39761
diff
changeset

740 
val processed_out_ts = map (compile_arg compilation_modifiers additional_arguments 
02fb709ab3cb
handling higherorder relations in output terms; improving proof procedure; added test case
bulwahn
parents:
39761
diff
changeset

741 
ctxt param_modes) out_ts 
32667  742 
in 
33147
180dc60bd88c
improving the compilation with higherorder arguments in the predicate compiler
bulwahn
parents:
33146
diff
changeset

743 
compile_match constr_vs (eqs @ eqs') out_ts''' 
39762
02fb709ab3cb
handling higherorder relations in output terms; improving proof procedure; added test case
bulwahn
parents:
39761
diff
changeset

744 
(mk_single compfuns (HOLogic.mk_tuple processed_out_ts)) 
32667  745 
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

746 
 compile_prems out_ts vs names ((p, deriv) :: ps) = 
32667  747 
let 
748 
val vs' = distinct (op =) (flat (vs :: map term_vs out_ts)); 

749 
val (out_ts', (names', eqs)) = 

35891
3122bdd95275
contextifying the compilation of the predicate compiler
bulwahn
parents:
35889
diff
changeset

750 
fold_map (collect_non_invertible_subterms ctxt) out_ts (names, []) 
32667  751 
val (out_ts'', (names'', constr_vs')) = fold_map distinct_v 
752 
out_ts' ((names', map (rpair []) vs)) 

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

753 
val mode = head_mode_of deriv 
33143
730a2e8a6ec6
modularized the compilation in the predicate compiler
bulwahn
parents:
33141
diff
changeset

754 
val additional_arguments' = 
33330
d6eb7f19bfc6
encapsulating records with datatype constructors and adding type annotations to make SML/NJ happy
bulwahn
parents:
33328
diff
changeset

755 
Comp_Mod.transform_additional_arguments compilation_modifiers p additional_arguments 
32667  756 
val (compiled_clause, rest) = case p 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

757 
Prem t => 
32667  758 
let 
33138
e2e23987c59a
reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents:
33137
diff
changeset

759 
val u = 
39648
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

760 
compile_expr compilation_modifiers ctxt (t, deriv) param_modes additional_arguments' 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

761 
val (_, out_ts''') = split_mode mode (snd (strip_comb t)) 
32667  762 
val rest = compile_prems out_ts''' vs' names'' ps 
763 
in 

764 
(u, rest) 

765 
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

766 
 Negprem t => 
32667  767 
let 
36019
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

768 
val neg_compilation_modifiers = 
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

769 
negative_comp_modifiers_of compilation_modifiers 
33143
730a2e8a6ec6
modularized the compilation in the predicate compiler
bulwahn
parents:
33141
diff
changeset

770 
val u = mk_not compfuns 
39648
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

771 
(compile_expr neg_compilation_modifiers ctxt (t, deriv) param_modes additional_arguments') 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

772 
val (_, out_ts''') = split_mode mode (snd (strip_comb t)) 
32667  773 
val rest = compile_prems out_ts''' vs' names'' ps 
774 
in 

775 
(u, rest) 

776 
end 

777 
 Sidecond t => 

778 
let 

36019
64bbbd858c39
generalizing the compilation process of the predicate compiler
bulwahn
parents:
36018
diff
changeset

779 
val t = compile_arg compilation_modifiers additional_arguments 
39648
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

780 
ctxt param_modes t 
32667  781 
val rest = compile_prems [] vs' names'' ps; 
782 
in 

783 
(mk_if compfuns t, rest) 

784 
end 

785 
 Generator (v, T) => 

786 
let 

35880
2623b23e41fc
a new simpler random compilation for the predicate compiler
bulwahn
parents:
35879
diff
changeset

787 
val u = Comp_Mod.mk_random compilation_modifiers T additional_arguments 
32667  788 
val rest = compile_prems [Free (v, T)] vs' names'' ps; 
789 
in 

790 
(u, rest) 

791 
end 

792 
in 

33147
180dc60bd88c
improving the compilation with higherorder arguments in the predicate compiler
bulwahn
parents:
33146
diff
changeset

793 
compile_match constr_vs' eqs out_ts'' 
32667  794 
(mk_bind compfuns (compiled_clause, rest)) 
795 
end 

39648
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

796 
val prem_t = compile_prems in_ts' (map fst param_modes) all_vs' moded_ps; 
32667  797 
in 
798 
mk_bind compfuns (mk_single compfuns inp, prem_t) 

799 
end 

800 

36254  801 
(* switch detection *) 
802 

803 
(** argument position of an inductive predicates and the executable functions **) 

804 

805 
type position = int * int list 

806 

807 
fun input_positions_pair Input = [[]] 

808 
 input_positions_pair Output = [] 

809 
 input_positions_pair (Fun _) = [] 

810 
 input_positions_pair (Pair (m1, m2)) = 

811 
map (cons 1) (input_positions_pair m1) @ map (cons 2) (input_positions_pair m2) 

812 

813 
fun input_positions_of_mode mode = flat (map_index 

814 
(fn (i, Input) => [(i, [])] 

815 
 (_, Output) => [] 

816 
 (_, Fun _) => [] 

817 
 (i, m as Pair (m1, m2)) => map (pair i) (input_positions_pair m)) 

818 
(Predicate_Compile_Aux.strip_fun_mode mode)) 

819 

820 
fun argument_position_pair mode [] = [] 

821 
 argument_position_pair (Pair (Fun _, m2)) (2 :: is) = argument_position_pair m2 is 

822 
 argument_position_pair (Pair (m1, m2)) (i :: is) = 

823 
(if eq_mode (m1, Output) andalso i = 2 then 

824 
argument_position_pair m2 is 

825 
else if eq_mode (m2, Output) andalso i = 1 then 

826 
argument_position_pair m1 is 

827 
else (i :: argument_position_pair (if i = 1 then m1 else m2) is)) 

828 

829 
fun argument_position_of mode (i, is) = 

830 
(i  (length (filter (fn Output => true  Fun _ => true  _ => false) 

831 
(List.take (strip_fun_mode mode, i)))), 

832 
argument_position_pair (nth (strip_fun_mode mode) i) is) 

833 

834 
fun nth_pair [] t = t 

835 
 nth_pair (1 :: is) (Const (@{const_name Pair}, _) $ t1 $ _) = nth_pair is t1 

836 
 nth_pair (2 :: is) (Const (@{const_name Pair}, _) $ _ $ t2) = nth_pair is t2 

837 
 nth_pair _ _ = raise Fail "unexpected input for nth_tuple" 

838 

839 
(** switch detection analysis **) 

840 

37005
842a73dc6d0e
changing compilation to work only with contexts; adapting quickcheck
bulwahn
parents:
37004
diff
changeset

841 
fun find_switch_test ctxt (i, is) (ts, prems) = 
36254  842 
let 
843 
val t = nth_pair is (nth ts i) 

844 
val T = fastype_of t 

845 
in 

846 
case T of 

847 
TFree _ => NONE 

848 
 Type (Tcon, _) => 

42361  849 
(case Datatype_Data.get_constrs (Proof_Context.theory_of ctxt) Tcon of 
36254  850 
NONE => NONE 
851 
 SOME cs => 

852 
(case strip_comb t of 

853 
(Var _, []) => NONE 

854 
 (Free _, []) => NONE 

855 
 (Const (c, T), _) => if AList.defined (op =) cs c then SOME (c, T) else NONE)) 

856 
end 

857 

37005
842a73dc6d0e
changing compilation to work only with contexts; adapting quickcheck
bulwahn
parents:
37004
diff
changeset

858 
fun partition_clause ctxt pos moded_clauses = 
36254  859 
let 
860 
fun insert_list eq (key, value) = AList.map_default eq (key, []) (cons value) 

861 
fun find_switch_test' moded_clause (cases, left) = 

37005
842a73dc6d0e
changing compilation to work only with contexts; adapting quickcheck
bulwahn
parents:
37004
diff
changeset

862 
case find_switch_test ctxt pos moded_clause of 
36254  863 
SOME (c, T) => (insert_list (op =) ((c, T), moded_clause) cases, left) 
864 
 NONE => (cases, moded_clause :: left) 

865 
in 

866 
fold find_switch_test' moded_clauses ([], []) 

867 
end 

868 

869 
datatype switch_tree = 

870 
Atom of moded_clause list  Node of (position * ((string * typ) * switch_tree) list) * switch_tree 

871 

37005
842a73dc6d0e
changing compilation to work only with contexts; adapting quickcheck
bulwahn
parents:
37004
diff
changeset

872 
fun mk_switch_tree ctxt mode moded_clauses = 
36254  873 
let 
874 
fun select_best_switch moded_clauses input_position best_switch = 

875 
let 

876 
val ord = option_ord (rev_order o int_ord o (pairself (length o snd o snd))) 

37005
842a73dc6d0e
changing compilation to work only with contexts; adapting quickcheck
bulwahn
parents:
37004
diff
changeset

877 
val partition = partition_clause ctxt input_position moded_clauses 
36254  878 
val switch = if (length (fst partition) > 1) then SOME (input_position, partition) else NONE 
879 
in 

880 
case ord (switch, best_switch) of LESS => best_switch 

881 
 EQUAL => best_switch  GREATER => switch 

882 
end 

883 
fun detect_switches moded_clauses = 

884 
case fold (select_best_switch moded_clauses) (input_positions_of_mode mode) NONE of 

885 
SOME (best_pos, (switched_on, left_clauses)) => 

886 
Node ((best_pos, map (apsnd detect_switches) switched_on), 

887 
detect_switches left_clauses) 

888 
 NONE => Atom moded_clauses 

889 
in 

890 
detect_switches moded_clauses 

891 
end 

892 

893 
(** compilation of detected switches **) 

894 

895 
fun destruct_constructor_pattern (pat, obj) = 

896 
(case strip_comb pat of 

897 
(f as Free _, []) => cons (pat, obj) 

898 
 (Const (c, T), pat_args) => 

899 
(case strip_comb obj of 

900 
(Const (c', T'), obj_args) => 

901 
(if c = c' andalso T = T' then 

902 
fold destruct_constructor_pattern (pat_args ~~ obj_args) 

903 
else raise Fail "pattern and object mismatch") 

904 
 _ => raise Fail "unexpected object") 

905 
 _ => raise Fail "unexpected pattern") 

906 

907 

39648
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

908 
fun compile_switch compilation_modifiers ctxt all_vs param_modes additional_arguments mode 
36254  909 
in_ts' outTs switch_tree = 
910 
let 

911 
val compfuns = Comp_Mod.compfuns compilation_modifiers 

42361  912 
val thy = Proof_Context.theory_of ctxt 
36254  913 
fun compile_switch_tree _ _ (Atom []) = NONE 
914 
 compile_switch_tree all_vs ctxt_eqs (Atom moded_clauses) = 

915 
let 

916 
val in_ts' = map (Pattern.rewrite_term thy ctxt_eqs []) in_ts' 

917 
fun compile_clause' (ts, moded_ps) = 

918 
let 

919 
val (ts, out_ts) = split_mode mode ts 

920 
val subst = fold destruct_constructor_pattern (in_ts' ~~ ts) [] 

921 
val (fsubst, pat') = List.partition (fn (_, Free _) => true  _ => false) subst 

922 
val moded_ps' = (map o apfst o map_indprem) 

923 
(Pattern.rewrite_term thy (map swap fsubst) []) moded_ps 

924 
val inp = HOLogic.mk_tuple (map fst pat') 

925 
val in_ts' = map (Pattern.rewrite_term thy (map swap fsubst) []) (map snd pat') 

926 
val out_ts' = map (Pattern.rewrite_term thy (map swap fsubst) []) out_ts 

927 
in 

39648
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

928 
compile_clause compilation_modifiers ctxt all_vs param_modes additional_arguments 
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

929 
inp (in_ts', out_ts') moded_ps' 
36254  930 
end 
931 
in SOME (foldr1 (mk_sup compfuns) (map compile_clause' moded_clauses)) end 

932 
 compile_switch_tree all_vs ctxt_eqs (Node ((position, switched_clauses), left_clauses)) = 

933 
let 

934 
val (i, is) = argument_position_of mode position 

935 
val inp_var = nth_pair is (nth in_ts' i) 

43324
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
43253
diff
changeset

936 
val x = singleton (Name.variant_list all_vs) "x" 
36254  937 
val xt = Free (x, fastype_of inp_var) 
938 
fun compile_single_case ((c, T), switched) = 

939 
let 

940 
val Ts = binder_types T 

941 
val argnames = Name.variant_list (x :: all_vs) 

942 
(map (fn i => "c" ^ string_of_int i) (1 upto length Ts)) 

943 
val args = map2 (curry Free) argnames Ts 

944 
val pattern = list_comb (Const (c, T), args) 

945 
val ctxt_eqs' = (inp_var, pattern) :: ctxt_eqs 

946 
val compilation = the_default (mk_bot compfuns (HOLogic.mk_tupleT outTs)) 

947 
(compile_switch_tree (argnames @ x :: all_vs) ctxt_eqs' switched) 

948 
in 

949 
(pattern, compilation) 

950 
end 

43253
fa3c61dc9f2c
removed generation of instantiated pattern set, which is never actually used
krauss
parents:
43123
diff
changeset

951 
val switch = Datatype.make_case ctxt Datatype_Case.Quiet [] inp_var 
36254  952 
((map compile_single_case switched_clauses) @ 
43253
fa3c61dc9f2c
removed generation of instantiated pattern set, which is never actually used
krauss
parents:
43123
diff
changeset

953 
[(xt, mk_bot compfuns (HOLogic.mk_tupleT outTs))]) 
36254  954 
in 
955 
case compile_switch_tree all_vs ctxt_eqs left_clauses of 

956 
NONE => SOME switch 

957 
 SOME left_comp => SOME (mk_sup compfuns (switch, left_comp)) 

958 
end 

959 
in 

960 
compile_switch_tree all_vs [] switch_tree 

961 
end 

962 

963 
(* compilation of predicates *) 

964 

37005
842a73dc6d0e
changing compilation to work only with contexts; adapting quickcheck
bulwahn
parents:
37004
diff
changeset

965 
fun compile_pred options compilation_modifiers ctxt all_vs param_vs s T (pol, mode) moded_cls = 
32667  966 
let 
40050
638ce4dabe53
for now safely but unpractically assume no predicate is terminating
bulwahn
parents:
40049
diff
changeset

967 
val is_terminating = false (* FIXME: requires an termination analysis *) 
40049
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

968 
val compilation_modifiers = 
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

969 
(if pol then compilation_modifiers else 
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

970 
negative_comp_modifiers_of compilation_modifiers) 
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

971 
> (if is_depth_limited_compilation (Comp_Mod.compilation compilation_modifiers) then 
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

972 
(if is_terminating then 
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

973 
(Comp_Mod.set_compfuns (unlimited_compfuns_of pol (Comp_Mod.compilation compilation_modifiers))) 
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

974 
else 
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

975 
(Comp_Mod.set_compfuns (limited_compfuns_of pol (Comp_Mod.compilation compilation_modifiers)))) 
75d9f57123d6
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
bulwahn
parents:
39785
diff
changeset

976 
else I) 
35879
99818df5b8f5
reviving the classical depthlimited computation in the predicate compiler
bulwahn
parents:
35845
diff
changeset

977 
val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers 
33482
5029ec373036
strictly respecting the line margin in the predicate compiler core
bulwahn
parents:
33479
diff
changeset

978 
(all_vs @ param_vs) 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

979 
val compfuns = Comp_Mod.compfuns compilation_modifiers 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

981 
is_some (try (dest_predT compfuns) T) orelse is_param_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 
 is_param_type T = is_some (try (dest_predT compfuns) T) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

983 
val (inpTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

984 
(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

985 
val predT = mk_predT compfuns (HOLogic.mk_tupleT outTs) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

986 
val funT = Comp_Mod.funT_of compilation_modifiers 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 
val (in_ts, _) = fold_map (fold_map_aterms_prodT (curry HOLogic.mk_prod) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

988 
(fn T => fn (param_vs, names) => 
36018  989 
if is_param_type T then 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

990 
(Free (hd param_vs, T), (tl param_vs, names)) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

992 
let 
43324
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
43253
diff
changeset

993 
val new = singleton (Name.variant_list names) "x" 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

994 
in (Free (new, T), (param_vs, new :: names)) end)) inpTs 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

995 
(param_vs, (all_vs @ param_vs)) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

996 
val in_ts' = map_filter (map_filter_prod 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

997 
(fn t as Free (x, _) => if member (op =) param_vs x then NONE else SOME t  t => SOME t)) in_ts 
39648
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

998 
val param_modes = param_vs ~~ ho_arg_modes_of mode 
36254  999 
val compilation = 
1000 
if detect_switches options then 

1001 
the_default (mk_bot compfuns (HOLogic.mk_tupleT outTs)) 

39648
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

1002 
(compile_switch compilation_modifiers ctxt all_vs param_modes additional_arguments mode 
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

1003 
in_ts' outTs (mk_switch_tree ctxt mode moded_cls)) 
36254  1004 
else 
1005 
let 

1006 
val cl_ts = 

1007 
map (fn (ts, moded_prems) => 

39648
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

1008 
compile_clause compilation_modifiers ctxt all_vs param_modes additional_arguments 
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
39557
diff
changeset

1009 
(HOLogic.mk_tuple in_ts') (split_mode mode ts) moded_prems) moded_cls; 
36254  1010 
in 
1011 
Comp_Mod.wrap_compilation compilation_modifiers compfuns s T mode additional_arguments 

1012 
(if null cl_ts then 

1013 
mk_bot compfuns (HOLogic.mk_tupleT outTs) 

1014 
else 

1015 
foldr1 (mk_sup compfuns) cl_ts) 

1016 
end 

33143
730a2e8a6ec6
modularized the compilation in the predicate compiler
bulwahn
parents:
33141
diff
changeset

1017 
val fun_const = 
35891
3122bdd95275
contextifying the compilation of the predicate compiler
bulwahn
parents:
35889
diff
changeset

1018 
Const (function_name_of (Comp_Mod.compilation compilation_modifiers) 
37003
a393a588b82e
moving towards working with proof contexts in the predicate compiler
bulwahn
parents:
37002
diff
changeset

1019 
ctxt s mode, funT) 
32667  1020 
in 
33143
730a2e8a6ec6
modularized the compilation in the predicate compiler
bulwahn
parents:
33141
diff
changeset

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

1022 
(HOLogic.mk_eq (list_comb (fun_const, in_ts @ additional_arguments), compilation)) 
32667  1023 
end; 
33143
730a2e8a6ec6
modularized the compilation in the predicate compiler
bulwahn
parents:
33141
diff
changeset

1024 

32667  1025 
(* Definition of executable functions and their intro and elim rules *) 
1026 

1027 
fun print_arities arities = tracing ("Arities:\n" ^ 

1028 
cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^ 

1029 
space_implode " > " (map 

1030 
(fn NONE => "X"  SOME k' => string_of_int k') 

1031 
(ks @ [SOME k]))) arities)); 

1032 

37591  1033 
fun strip_split_abs (Const (@{const_name prod_case}, _) $ t) = strip_split_abs 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

1034 
 strip_split_abs (Abs (_, _, t)) = strip_split_abs t 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1035 
 strip_split_abs 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

1036 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37591
diff
changeset

1037 
fun mk_args is_eval (m as Pair (m1, m2), T as Type (@{type_name Product_Type.prod}, [T1, T2])) names = 
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

1038 
if eq_mode (m, Input) orelse 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

1039 
let 
43324
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
43253
diff
changeset

1040 
val x = singleton (Name.variant_list names) "x" 
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

1041 
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

1042 
(Free (x, T), x :: names) 
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

1043 
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

1044 
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

1045 
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

1046 
val (t1, names') = mk_args is_eval (m1, T1) names 
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

1047 
val (t2, names'') = mk_args is_eval (m2, T2) names' 
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

1048 
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

1049 
(HOLogic.mk_prod (t1, t2), names'') 
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 
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

1051 
 mk_args is_eval ((m as Fun _), T) names = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1052 
let 
45450  1053 
val funT = funT_of Predicate_Comp_Funs.compfuns m T 
43324
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
43253
diff
changeset

1054 
val x = singleton (Name.variant_list names) "x" 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1055 
val (args, _) = fold_map (mk_args is_eval) (strip_fun_mode m ~~ binder_types T) (x :: names) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1056 
val (inargs, outargs) = split_map_mode (fn _ => fn t => (SOME t, NONE)) m args 
45450  1057 
val t = fold_rev HOLogic.tupled_lambda args (Predicate_Comp_Funs.mk_Eval 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1058 
(list_comb (Free (x, funT), inargs), HOLogic.mk_tuple outargs)) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

1060 
(if is_eval then t else Free (x, funT), x :: names) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

1062 
 mk_args is_eval (_, T) names = 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1063 
let 
43324
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
43253
diff
changeset

1064 
val x = singleton (Name.variant_list names) "x" 
33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33265
diff
changeset

1065 
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

1066 
(Free (x, T), x :: names) 
33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33265
diff
changeset

1067 
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

1068 

37003
a393a588b82e
moving towards working with proof contexts in the predicate compiler
bulwahn
parents:
37002
diff
changeset

1069 
fun create_intro_elim_rule ctxt mode defthm mode_id funT 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

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

1071 
val funtrm = Const (mode_id, funT) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1072 
val Ts = 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

1073 
val (args, argnames) = fold_map (mk_args true) (strip_fun_mode mode ~~ Ts) [] 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

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

1076 
val t' = strip_split_abs t 
45450  1077 
val (r, _) = Predicate_Comp_Funs.dest_Eval 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

1078 
in (SOME (fst (strip_comb r)), NONE) end 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1079 
val (inargs, outargs) = split_map_mode strip_eval mode args 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1080 
val eval_hoargs = ho_args_of mode args 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1081 
val hoargTs = ho_argsT_of mode Ts 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

1083 
Name.variant_list argnames ((map (fn i => "x" ^ string_of_int i)) (1 upto (length hoargTs))) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1084 
val hoargs' = map2 (curry Free) hoarg_names' hoargTs 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1085 
val args' = replace_ho_args mode hoargs' args 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1086 
val predpropI = HOLogic.mk_Trueprop (list_comb (pred, args')) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1087 
val predpropE = HOLogic.mk_Trueprop (list_comb (pred, args)) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1088 
val param_eqs = map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) eval_hoargs hoargs' 
45450  1089 
val funpropE = HOLogic.mk_Trueprop (Predicate_Comp_Funs.mk_Eval (list_comb (funtrm, inargs), 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1090 
if null outargs then Free("y", HOLogic.unitT) else HOLogic.mk_tuple outargs)) 
45450  1091 
val funpropI = HOLogic.mk_Trueprop (Predicate_Comp_Funs.mk_Eval (list_comb (funtrm, inargs), 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1092 
HOLogic.mk_tuple outargs)) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1093 
val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1094 
val simprules = [defthm, @{thm eval_pred}, 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1095 
@{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}] 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

1096 
val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1 
37003
a393a588b82e
moving towards working with proof contexts in the predicate compiler
bulwahn
parents:
37002
diff
changeset

1097 
val introthm = Goal.prove 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

1098 
(argnames @ hoarg_names' @ ["y"]) [] introtrm (fn _ => unfolddef_tac) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

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

1100 
val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P) 
37003
a393a588b82e
moving towards working with proof contexts in the predicate compiler
bulwahn
parents:
37002
diff
changeset

1101 
val elimthm = Goal.prove 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

1102 
(argnames @ ["y", "P"]) [] elimtrm (fn _ => unfolddef_tac) 
35884
362bfc2ca0ee
adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents:
35881
diff
changeset

1103 
val opt_neg_introthm = 
362bfc2ca0ee
adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents:
35881
diff
changeset

1104 
if is_all_input mode then 
362bfc2ca0ee
adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents:
35881
diff
changeset

1105 
let 
362bfc2ca0ee
adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents:
35881
diff
changeset

1106 
val neg_predpropI = HOLogic.mk_Trueprop (HOLogic.mk_not (list_comb (pred, args'))) 
362bfc2ca0ee
adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents:
35881
diff
changeset

1107 
val neg_funpropI = 
45450  1108 
HOLogic.mk_Trueprop (Predicate_Comp_Funs.mk_Eval 
1109 
(Predicate_Comp_Funs.mk_not (list_comb (funtrm, inargs)), HOLogic.unit)) 

35884
362bfc2ca0ee
adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents:
35881
diff
changeset

1110 
val neg_introtrm = Logic.list_implies (neg_predpropI :: param_eqs, neg_funpropI) 
362bfc2ca0ee
adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents:
35881
diff
changeset

1111 
val tac = 
362bfc2ca0ee
adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents:
35881
diff
changeset

1112 
Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps 
362bfc2ca0ee
adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents:
35881
diff
changeset

1113 
(@{thm if_False} :: @{thm Predicate.not_pred_eq} :: simprules)) 1 
362bfc2ca0ee
adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents:
35881
diff
changeset

1114 
THEN rtac @{thm Predicate.singleI} 1 
37003
a393a588b82e
moving towards working with proof contexts in the predicate compiler
bulwahn
parents:
37002
diff
changeset

1115 
in SOME (Goal.prove ctxt (argnames @ hoarg_names') [] 
35884
362bfc2ca0ee
adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents:
35881
diff
changeset

1116 
neg_introtrm (fn _ => tac)) 
362bfc2ca0ee
adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents:
35881
diff
changeset

1117 
end 
362bfc2ca0ee
adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents:
35881
diff
changeset

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