author | wenzelm |
Mon, 03 Nov 2014 14:50:27 +0100 | |
changeset 58893 | 9e0ecb66d6a7 |
parent 58823 | 513268cb2178 |
child 59205 | 663794ab87e6 |
permissions | -rw-r--r-- |
33265 | 1 |
(* Title: HOL/Tools/Predicate_Compile/predicate_compile.ML |
2 |
Author: Lukas Bulwahn, TU Muenchen |
|
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
3 |
|
41941 | 4 |
Entry point for the predicate compiler; definition of Toplevel |
5 |
commands code_pred and values. |
|
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
6 |
*) |
33265 | 7 |
|
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
8 |
signature PREDICATE_COMPILE = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
9 |
sig |
36050
88203782cf12
activating the signature of Predicate_Compile again which was deactivated in changeset d93a3cb55068 for debugging purposes
bulwahn
parents:
36032
diff
changeset
|
10 |
val preprocess : Predicate_Compile_Aux.options -> term -> theory -> theory |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
11 |
val present_graph : bool Unsynchronized.ref |
36023
d606ca1674a7
adding a hook for experiments in the predicate compilation process
bulwahn
parents:
36022
diff
changeset
|
12 |
val intro_hook : (theory -> thm -> unit) option Unsynchronized.ref |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
13 |
end; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
14 |
|
36050
88203782cf12
activating the signature of Predicate_Compile again which was deactivated in changeset d93a3cb55068 for debugging purposes
bulwahn
parents:
36032
diff
changeset
|
15 |
structure Predicate_Compile : PREDICATE_COMPILE = |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
16 |
struct |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
17 |
|
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:
34948
diff
changeset
|
18 |
val present_graph = Unsynchronized.ref false |
33108
9d9afd478016
added test for higher-order function inductification; added debug messages
bulwahn
parents:
33107
diff
changeset
|
19 |
|
36023
d606ca1674a7
adding a hook for experiments in the predicate compilation process
bulwahn
parents:
36022
diff
changeset
|
20 |
val intro_hook = Unsynchronized.ref NONE : (theory -> thm -> unit) option Unsynchronized.ref |
d606ca1674a7
adding a hook for experiments in the predicate compilation process
bulwahn
parents:
36022
diff
changeset
|
21 |
|
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
22 |
open Predicate_Compile_Aux; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
23 |
|
33125 | 24 |
fun print_intross options thy msg intross = |
25 |
if show_intermediate_results options then |
|
55437 | 26 |
tracing (msg ^ |
55628 | 27 |
(cat_lines (map |
33376
5cb663aa48ee
predicate compiler creates code equations for predicates with full mode
bulwahn
parents:
33375
diff
changeset
|
28 |
(fn (c, intros) => "Introduction rule(s) of " ^ c ^ ":\n" ^ |
5cb663aa48ee
predicate compiler creates code equations for predicates with full mode
bulwahn
parents:
33375
diff
changeset
|
29 |
commas (map (Display.string_of_thm_global thy) intros)) intross))) |
33125 | 30 |
else () |
55437 | 31 |
|
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:
34948
diff
changeset
|
32 |
fun print_specs options thy specs = |
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:
34948
diff
changeset
|
33 |
if show_intermediate_results options then |
55437 | 34 |
map (fn (c, thms) => |
35 |
"Constant " ^ c ^ " has specification:\n" ^ |
|
55628 | 36 |
(cat_lines (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs |
37 |
|> cat_lines |> tracing |
|
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:
34948
diff
changeset
|
38 |
else () |
55437 | 39 |
|
51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
50056
diff
changeset
|
40 |
fun overload_const thy s = the_default s (Option.map fst (Axclass.inst_of_param thy s)) |
33404 | 41 |
|
33146
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33142
diff
changeset
|
42 |
fun map_specs f specs = |
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33142
diff
changeset
|
43 |
map (fn (s, ths) => (s, f ths)) specs |
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33142
diff
changeset
|
44 |
|
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
45 |
fun process_specification options specs thy' = |
33121
9b10dc5da0e0
added to process higher-order arguments by adding new constants
bulwahn
parents:
33120
diff
changeset
|
46 |
let |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
47 |
val _ = print_step options "Compiling predicates to flat introrules..." |
55437 | 48 |
val specs = |
49 |
map |
|
50 |
(apsnd (map |
|
51 |
(fn th => |
|
52 |
if is_equationlike th then Predicate_Compile_Data.normalize_equation thy' th else th))) |
|
53 |
specs |
|
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:
34948
diff
changeset
|
54 |
val (intross1, thy'') = |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
55 |
apfst flat (fold_map (Predicate_Compile_Pred.preprocess options) specs thy') |
33125 | 56 |
val _ = print_intross options thy'' "Flattened introduction rules: " intross1 |
33129
3085da75ed54
changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents:
33127
diff
changeset
|
57 |
val _ = print_step options "Replacing functions in introrules..." |
33121
9b10dc5da0e0
added to process higher-order arguments by adding new constants
bulwahn
parents:
33120
diff
changeset
|
58 |
val intross2 = |
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:
34948
diff
changeset
|
59 |
if function_flattening options 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:
34948
diff
changeset
|
60 |
if fail_safe_function_flattening options then |
55437 | 61 |
(case try (map_specs (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross1 of |
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:
34948
diff
changeset
|
62 |
SOME intross => intross |
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:
34948
diff
changeset
|
63 |
| NONE => |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
64 |
(if show_caught_failures options then tracing "Function replacement failed!" else (); |
55437 | 65 |
intross1)) |
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:
34948
diff
changeset
|
66 |
else map_specs (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross1 |
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:
34948
diff
changeset
|
67 |
else |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
68 |
intross1 |
33125 | 69 |
val _ = print_intross options thy'' "Introduction rules with replaced functions: " intross2 |
55437 | 70 |
val _ = print_step options |
71 |
"Introducing new constants for abstractions at higher-order argument positions..." |
|
72 |
val (intross3, (new_defs, thy''')) = |
|
73 |
Predicate_Compile_Pred.flat_higher_order_arguments (intross2, thy'') |
|
74 |
val (new_intross, thy'''') = |
|
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
75 |
if not (null new_defs) then |
33404 | 76 |
let |
55437 | 77 |
val _ = |
78 |
print_step options "Recursively obtaining introduction rules for new definitions..." |
|
33404 | 79 |
in process_specification options new_defs thy''' end |
80 |
else ([], thy''') |
|
33121
9b10dc5da0e0
added to process higher-order arguments by adding new constants
bulwahn
parents:
33120
diff
changeset
|
81 |
in |
9b10dc5da0e0
added to process higher-order arguments by adding new constants
bulwahn
parents:
33120
diff
changeset
|
82 |
(intross3 @ new_intross, thy'''') |
9b10dc5da0e0
added to process higher-order arguments by adding new constants
bulwahn
parents:
33120
diff
changeset
|
83 |
end |
9b10dc5da0e0
added to process higher-order arguments by adding new constants
bulwahn
parents:
33120
diff
changeset
|
84 |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset
|
85 |
fun preprocess_strong_conn_constnames options gr ts thy = |
55437 | 86 |
if forall (fn (Const (c, _)) => Core_Data.is_registered (Proof_Context.init_global thy) c) ts |
87 |
then thy |
|
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:
34948
diff
changeset
|
88 |
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:
34948
diff
changeset
|
89 |
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:
34948
diff
changeset
|
90 |
fun get_specs ts = map_filter (fn t => |
35404 | 91 |
Term_Graph.get_node gr t |> |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
92 |
(fn ths => if null ths then NONE else SOME (fst (dest_Const t), ths))) |
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:
34948
diff
changeset
|
93 |
ts |
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:
34948
diff
changeset
|
94 |
val _ = print_step options ("Preprocessing scc 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:
34948
diff
changeset
|
95 |
commas (map (Syntax.string_of_term_global thy) ts)) |
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:
34948
diff
changeset
|
96 |
val (prednames, funnames) = List.partition (fn t => body_type (fastype_of t) = @{typ bool}) ts |
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:
34948
diff
changeset
|
97 |
(* untangle recursion by defining predicates for all functions *) |
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:
34948
diff
changeset
|
98 |
val _ = print_step options |
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:
34948
diff
changeset
|
99 |
("Compiling functions (" ^ commas (map (Syntax.string_of_term_global thy) funnames) ^ |
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:
34948
diff
changeset
|
100 |
") to predicates...") |
36032
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
36027
diff
changeset
|
101 |
val (fun_pred_specs, thy1) = |
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:
34948
diff
changeset
|
102 |
(if function_flattening options andalso (not (null funnames)) 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:
34948
diff
changeset
|
103 |
if fail_safe_function_flattening options then |
55437 | 104 |
(case try (Predicate_Compile_Fun.define_predicates (get_specs funnames)) thy of |
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:
34948
diff
changeset
|
105 |
SOME (intross, thy) => (intross, thy) |
55437 | 106 |
| NONE => ([], thy)) |
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:
34948
diff
changeset
|
107 |
else Predicate_Compile_Fun.define_predicates (get_specs funnames) thy |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
108 |
else ([], thy)) |
36032
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
36027
diff
changeset
|
109 |
val _ = print_specs options thy1 fun_pred_specs |
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:
34948
diff
changeset
|
110 |
val specs = (get_specs prednames) @ fun_pred_specs |
36032
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
36027
diff
changeset
|
111 |
val (intross3, thy2) = process_specification options specs thy1 |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
36027
diff
changeset
|
112 |
val _ = print_intross options thy2 "Introduction rules with new constants: " intross3 |
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:
34948
diff
changeset
|
113 |
val intross4 = map_specs (maps remove_pointless_clauses) intross3 |
36032
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
36027
diff
changeset
|
114 |
val _ = print_intross options thy2 "After removing pointless clauses: " intross4 |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
36027
diff
changeset
|
115 |
val intross5 = map_specs (map (remove_equalities thy2)) intross4 |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
36027
diff
changeset
|
116 |
val _ = print_intross options thy2 "After removing equality premises:" intross5 |
36022
c0fa8499e366
removing simple equalities in introduction rules in the predicate compiler
bulwahn
parents:
36004
diff
changeset
|
117 |
val intross6 = |
51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
50056
diff
changeset
|
118 |
map (fn (s, ths) => (overload_const thy2 s, map (Axclass.overload thy2) ths)) intross5 |
36032
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
36027
diff
changeset
|
119 |
val intross7 = map_specs (map (expand_tuples thy2)) intross6 |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
36027
diff
changeset
|
120 |
val intross8 = map_specs (map (eta_contract_ho_arguments thy2)) intross7 |
55437 | 121 |
val _ = (case !intro_hook of NONE => () | SOME f => (map_specs (map (f thy2)) intross8; ())) |
122 |
val _ = |
|
123 |
print_step options ("Looking for specialisations in " ^ commas (map fst intross8) ^ "...") |
|
36248
9ed1a37de465
added option for specialisation to the predicate compiler
bulwahn
parents:
36246
diff
changeset
|
124 |
val (intross9, thy3) = |
9ed1a37de465
added option for specialisation to the predicate compiler
bulwahn
parents:
36246
diff
changeset
|
125 |
if specialise options then |
9ed1a37de465
added option for specialisation to the predicate compiler
bulwahn
parents:
36246
diff
changeset
|
126 |
Predicate_Compile_Specialisation.find_specialisations [] intross8 thy2 |
9ed1a37de465
added option for specialisation to the predicate compiler
bulwahn
parents:
36246
diff
changeset
|
127 |
else (intross8, thy2) |
36246
43fecedff8cf
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents:
36050
diff
changeset
|
128 |
val _ = print_intross options thy3 "introduction rules after specialisations: " intross9 |
43fecedff8cf
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents:
36050
diff
changeset
|
129 |
val intross10 = map_specs (map_filter (peephole_optimisation thy3)) intross9 |
43fecedff8cf
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents:
36050
diff
changeset
|
130 |
val _ = print_intross options thy3 "introduction rules before registering: " intross10 |
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:
34948
diff
changeset
|
131 |
val _ = print_step options "Registering introduction rules..." |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40048
diff
changeset
|
132 |
val thy4 = fold Core_Data.register_intros intross10 thy3 |
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:
34948
diff
changeset
|
133 |
in |
36032
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
36027
diff
changeset
|
134 |
thy4 |
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:
34948
diff
changeset
|
135 |
end; |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
136 |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset
|
137 |
fun preprocess options t thy = |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
138 |
let |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
139 |
val _ = print_step options "Fetching definitions from theory..." |
55437 | 140 |
val gr = |
141 |
cond_timeit (Config.get_global thy Quickcheck.timing) "preprocess-obtain graph" |
|
142 |
(fn () => |
|
143 |
Predicate_Compile_Data.obtain_specification_graph options thy t |
|
46614
165886a4fe64
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
wenzelm
parents:
42361
diff
changeset
|
144 |
|> (fn gr => Term_Graph.restrict (member (op =) (Term_Graph.all_succs gr [t])) gr)) |
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:
34948
diff
changeset
|
145 |
val _ = if !present_graph then Predicate_Compile_Data.present_graph gr else () |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset
|
146 |
in |
42088
8d00484551fe
making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents:
42011
diff
changeset
|
147 |
cond_timeit (Config.get_global thy Quickcheck.timing) "preprocess-process" |
55437 | 148 |
(fn () => |
149 |
fold_rev (preprocess_strong_conn_constnames options gr) |
|
150 |
(Term_Graph.strong_conn gr) thy) |
|
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
151 |
end |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
152 |
|
39382
c797f3ab2ae1
proposed modes for code_pred now supports modes for mutual predicates
bulwahn
parents:
38757
diff
changeset
|
153 |
datatype proposed_modes = Multiple_Preds of (string * (mode * string option) list) list |
c797f3ab2ae1
proposed modes for code_pred now supports modes for mutual predicates
bulwahn
parents:
38757
diff
changeset
|
154 |
| Single_Pred of (mode * string option) list |
c797f3ab2ae1
proposed modes for code_pred now supports modes for mutual predicates
bulwahn
parents:
38757
diff
changeset
|
155 |
|
c797f3ab2ae1
proposed modes for code_pred now supports modes for mutual predicates
bulwahn
parents:
38757
diff
changeset
|
156 |
fun extract_options lthy (((expected_modes, proposed_modes), (compilation, raw_options)), const) = |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
157 |
let |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
158 |
fun chk s = member (op =) raw_options s |
55437 | 159 |
val proposed_modes = |
160 |
(case proposed_modes of |
|
161 |
Single_Pred proposed_modes => [(const, proposed_modes)] |
|
162 |
| Multiple_Preds proposed_modes => |
|
163 |
map (apfst (Code.read_const (Proof_Context.theory_of lthy))) proposed_modes) |
|
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
164 |
in |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
165 |
Options { |
33623
4ec42d38224f
changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned
bulwahn
parents:
33620
diff
changeset
|
166 |
expected_modes = Option.map (pair const) expected_modes, |
55437 | 167 |
proposed_modes = |
39382
c797f3ab2ae1
proposed modes for code_pred now supports modes for mutual predicates
bulwahn
parents:
38757
diff
changeset
|
168 |
map (apsnd (map fst)) proposed_modes, |
33623
4ec42d38224f
changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned
bulwahn
parents:
33620
diff
changeset
|
169 |
proposed_names = |
39382
c797f3ab2ae1
proposed modes for code_pred now supports modes for mutual predicates
bulwahn
parents:
38757
diff
changeset
|
170 |
maps (fn (predname, ms) => (map_filter |
50056 | 171 |
(fn (_, NONE) => NONE | (m, SOME name) => SOME ((predname, m), name))) ms) proposed_modes, |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
172 |
show_steps = chk "show_steps", |
33125 | 173 |
show_intermediate_results = chk "show_intermediate_results", |
33127 | 174 |
show_proof_trace = chk "show_proof_trace", |
33251 | 175 |
show_modes = chk "show_modes", |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
176 |
show_mode_inference = chk "show_mode_inference", |
33139
9c01ee6f8ee9
added skip_proof option; playing with compilation of depth-limited predicates
bulwahn
parents:
33134
diff
changeset
|
177 |
show_compilation = chk "show_compilation", |
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:
34948
diff
changeset
|
178 |
show_caught_failures = false, |
39383
ddfafa97da2f
adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents:
39382
diff
changeset
|
179 |
show_invalid_clauses = chk "show_invalid_clauses", |
33139
9c01ee6f8ee9
added skip_proof option; playing with compilation of depth-limited predicates
bulwahn
parents:
33134
diff
changeset
|
180 |
skip_proof = chk "skip_proof", |
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:
34948
diff
changeset
|
181 |
function_flattening = not (chk "no_function_flattening"), |
36248
9ed1a37de465
added option for specialisation to the predicate compiler
bulwahn
parents:
36246
diff
changeset
|
182 |
specialise = chk "specialise", |
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:
34948
diff
changeset
|
183 |
fail_safe_function_flattening = false, |
35381
5038f36b5ea1
adding no_topmost_reordering as new option to the code_pred command
bulwahn
parents:
35324
diff
changeset
|
184 |
no_topmost_reordering = (chk "no_topmost_reordering"), |
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:
34948
diff
changeset
|
185 |
no_higher_order_predicate = [], |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
186 |
inductify = chk "inductify", |
36254 | 187 |
detect_switches = chk "detect_switches", |
40048
f3a46d524101
adding option smart_depth_limiting to predicate compiler
bulwahn
parents:
39383
diff
changeset
|
188 |
smart_depth_limiting = chk "smart_depth_limiting", |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset
|
189 |
compilation = compilation |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
190 |
} |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
191 |
end |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
192 |
|
33623
4ec42d38224f
changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned
bulwahn
parents:
33620
diff
changeset
|
193 |
fun code_pred_cmd (((expected_modes, proposed_modes), raw_options), raw_const) lthy = |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
194 |
let |
42361 | 195 |
val thy = Proof_Context.theory_of lthy |
33132
07efd452a698
moved argument expected_modes into options; improved mode check to only check mode of the named predicate
bulwahn
parents:
33131
diff
changeset
|
196 |
val const = Code.read_const thy raw_const |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset
|
197 |
val T = Sign.the_const_type thy const |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset
|
198 |
val t = Const (const, T) |
39382
c797f3ab2ae1
proposed modes for code_pred now supports modes for mutual predicates
bulwahn
parents:
38757
diff
changeset
|
199 |
val options = extract_options lthy (((expected_modes, proposed_modes), raw_options), const) |
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 |
in |
38757
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38664
diff
changeset
|
201 |
if is_inductify options then |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
202 |
let |
38757
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38664
diff
changeset
|
203 |
val lthy' = Local_Theory.background_theory (preprocess options t) lthy |
33623
4ec42d38224f
changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned
bulwahn
parents:
33620
diff
changeset
|
204 |
val const = |
55437 | 205 |
(case Predicate_Compile_Fun.pred_of_function (Proof_Context.theory_of lthy') const of |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
206 |
SOME c => c |
55437 | 207 |
| NONE => const) |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
208 |
val _ = print_step options "Starting Predicate Compile Core..." |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
209 |
in |
33132
07efd452a698
moved argument expected_modes into options; improved mode check to only check mode of the named predicate
bulwahn
parents:
33131
diff
changeset
|
210 |
Predicate_Compile_Core.code_pred options const lthy' |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
211 |
end |
55437 | 212 |
else Predicate_Compile_Core.code_pred_cmd options raw_const lthy |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
213 |
end |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
214 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
215 |
|
33478
b70fe083694d
moved values command from core to predicate compile
bulwahn
parents:
33475
diff
changeset
|
216 |
(* Parser for mode annotations *) |
33327 | 217 |
|
33625
eefee41ede3a
removed deprecated mode annotation parser; renamed accepted mode annotation parser to nicer naming
bulwahn
parents:
33623
diff
changeset
|
218 |
fun parse_mode_basic_expr xs = |
eefee41ede3a
removed deprecated mode annotation parser; renamed accepted mode annotation parser to nicer naming
bulwahn
parents:
33623
diff
changeset
|
219 |
(Args.$$$ "i" >> K Input || Args.$$$ "o" >> K Output || |
eefee41ede3a
removed deprecated mode annotation parser; renamed accepted mode annotation parser to nicer naming
bulwahn
parents:
33623
diff
changeset
|
220 |
Args.$$$ "bool" >> K Bool || Args.$$$ "(" |-- parse_mode_expr --| Args.$$$ ")") xs |
eefee41ede3a
removed deprecated mode annotation parser; renamed accepted mode annotation parser to nicer naming
bulwahn
parents:
33623
diff
changeset
|
221 |
and parse_mode_tuple_expr xs = |
55437 | 222 |
(parse_mode_basic_expr --| (Args.$$$ "*" || Args.$$$ "\<times>") -- parse_mode_tuple_expr >> Pair || |
223 |
parse_mode_basic_expr) xs |
|
33625
eefee41ede3a
removed deprecated mode annotation parser; renamed accepted mode annotation parser to nicer naming
bulwahn
parents:
33623
diff
changeset
|
224 |
and parse_mode_expr xs = |
55437 | 225 |
(parse_mode_tuple_expr --| (Args.$$$ "=>" || Args.$$$ "\<Rightarrow>") -- parse_mode_expr >> Fun || |
226 |
parse_mode_tuple_expr) xs |
|
33619
d93a3cb55068
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents:
33481
diff
changeset
|
227 |
|
33625
eefee41ede3a
removed deprecated mode annotation parser; renamed accepted mode annotation parser to nicer naming
bulwahn
parents:
33623
diff
changeset
|
228 |
val mode_and_opt_proposal = parse_mode_expr -- |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36254
diff
changeset
|
229 |
Scan.optional (Args.$$$ "as" |-- Parse.xname >> SOME) NONE |
33620
b6bf2dc5aed7
added interface of user proposals for names of generated constants
bulwahn
parents:
33619
diff
changeset
|
230 |
|
39382
c797f3ab2ae1
proposed modes for code_pred now supports modes for mutual predicates
bulwahn
parents:
38757
diff
changeset
|
231 |
|
33114
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
232 |
val opt_modes = |
46949 | 233 |
Scan.optional (@{keyword "("} |-- Args.$$$ "modes" |-- @{keyword ":"} |-- |
234 |
(((Parse.enum1 "and" (Parse.xname --| @{keyword ":"} -- |
|
39382
c797f3ab2ae1
proposed modes for code_pred now supports modes for mutual predicates
bulwahn
parents:
38757
diff
changeset
|
235 |
(Parse.enum "," mode_and_opt_proposal))) >> Multiple_Preds) |
c797f3ab2ae1
proposed modes for code_pred now supports modes for mutual predicates
bulwahn
parents:
38757
diff
changeset
|
236 |
|| ((Parse.enum "," mode_and_opt_proposal) >> Single_Pred)) |
46949 | 237 |
--| @{keyword ")"}) (Multiple_Preds []) |
33623
4ec42d38224f
changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned
bulwahn
parents:
33620
diff
changeset
|
238 |
|
4ec42d38224f
changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned
bulwahn
parents:
33620
diff
changeset
|
239 |
val opt_expected_modes = |
46949 | 240 |
Scan.optional (@{keyword "("} |-- Args.$$$ "expected_modes" |-- @{keyword ":"} |-- |
241 |
Parse.enum "," parse_mode_expr --| @{keyword ")"} >> SOME) NONE |
|
33114
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
242 |
|
55437 | 243 |
|
33478
b70fe083694d
moved values command from core to predicate compile
bulwahn
parents:
33475
diff
changeset
|
244 |
(* Parser for options *) |
b70fe083694d
moved values command from core to predicate compile
bulwahn
parents:
33475
diff
changeset
|
245 |
|
b70fe083694d
moved values command from core to predicate compile
bulwahn
parents:
33475
diff
changeset
|
246 |
val scan_options = |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
247 |
let |
33478
b70fe083694d
moved values command from core to predicate compile
bulwahn
parents:
33475
diff
changeset
|
248 |
val scan_bool_option = foldl1 (op ||) (map Args.$$$ bool_options) |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset
|
249 |
val scan_compilation = foldl1 (op ||) (map (fn (s, c) => Args.$$$ s >> K c) compilation_names) |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
250 |
in |
46949 | 251 |
Scan.optional (@{keyword "["} |-- Scan.optional scan_compilation Pred |
252 |
-- Parse.enum "," scan_bool_option --| @{keyword "]"}) |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset
|
253 |
(Pred, []) |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
254 |
end |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
255 |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36254
diff
changeset
|
256 |
val opt_print_modes = |
55437 | 257 |
Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [] |
33478
b70fe083694d
moved values command from core to predicate compile
bulwahn
parents:
33475
diff
changeset
|
258 |
|
46949 | 259 |
val opt_mode = (Args.$$$ "_" >> K NONE) || (parse_mode_expr >> SOME) |
33479
428ddcc16e7b
added optional mode annotations for parameters in the values command
bulwahn
parents:
33478
diff
changeset
|
260 |
|
46949 | 261 |
val opt_param_modes = Scan.optional (@{keyword "["} |-- Args.$$$ "mode" |-- @{keyword ":"} |-- |
262 |
Parse.enum ", " opt_mode --| @{keyword "]"} >> SOME) NONE |
|
33479
428ddcc16e7b
added optional mode annotations for parameters in the values command
bulwahn
parents:
33478
diff
changeset
|
263 |
|
36027
29a15da9c63d
added statistics to values command for random generation
bulwahn
parents:
36023
diff
changeset
|
264 |
val stats = Scan.optional (Args.$$$ "stats" >> K true) false |
29a15da9c63d
added statistics to values command for random generation
bulwahn
parents:
36023
diff
changeset
|
265 |
|
33478
b70fe083694d
moved values command from core to predicate compile
bulwahn
parents:
33475
diff
changeset
|
266 |
val value_options = |
b70fe083694d
moved values command from core to predicate compile
bulwahn
parents:
33475
diff
changeset
|
267 |
let |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36254
diff
changeset
|
268 |
val expected_values = Scan.optional (Args.$$$ "expected" |-- Parse.term >> SOME) NONE |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset
|
269 |
val scan_compilation = |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset
|
270 |
Scan.optional |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset
|
271 |
(foldl1 (op ||) |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36254
diff
changeset
|
272 |
(map (fn (s, c) => Args.$$$ s -- Parse.enum "," Parse.int >> (fn (_, ps) => (c, ps))) |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset
|
273 |
compilation_names)) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset
|
274 |
(Pred, []) |
33478
b70fe083694d
moved values command from core to predicate compile
bulwahn
parents:
33475
diff
changeset
|
275 |
in |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36254
diff
changeset
|
276 |
Scan.optional |
46949 | 277 |
(@{keyword "["} |-- (expected_values -- stats) -- scan_compilation --| @{keyword "]"}) |
36027
29a15da9c63d
added statistics to values command for random generation
bulwahn
parents:
36023
diff
changeset
|
278 |
((NONE, false), (Pred, [])) |
33478
b70fe083694d
moved values command from core to predicate compile
bulwahn
parents:
33475
diff
changeset
|
279 |
end |
b70fe083694d
moved values command from core to predicate compile
bulwahn
parents:
33475
diff
changeset
|
280 |
|
55437 | 281 |
|
33478
b70fe083694d
moved values command from core to predicate compile
bulwahn
parents:
33475
diff
changeset
|
282 |
(* code_pred command and values command *) |
b70fe083694d
moved values command from core to predicate compile
bulwahn
parents:
33475
diff
changeset
|
283 |
|
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
284 |
val _ = |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
285 |
Outer_Syntax.local_theory_to_proof @{command_spec "code_pred"} |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
286 |
"prove equations for predicate specified by intro/elim rules" |
52801 | 287 |
(opt_expected_modes -- opt_modes -- scan_options -- Parse.term >> code_pred_cmd) |
33478
b70fe083694d
moved values command from core to predicate compile
bulwahn
parents:
33475
diff
changeset
|
288 |
|
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
289 |
val _ = |
58893
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58823
diff
changeset
|
290 |
Outer_Syntax.command @{command_spec "values"} |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
291 |
"enumerate and print comprehensions" |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
292 |
(opt_print_modes -- opt_param_modes -- value_options -- Scan.optional Parse.nat ~1 -- Parse.term |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
293 |
>> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.keep |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
294 |
(Predicate_Compile_Core.values_cmd print_modes param_modes options k t))) |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
295 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
296 |
end |