author | bulwahn |
Fri, 06 Nov 2009 08:11:58 +0100 | |
changeset 33473 | 3b275a0bf18c |
parent 33404 | 66746e4b4531 |
child 33475 | 42fed8eac357 |
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 |
|
33265 | 4 |
FIXME. |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
5 |
*) |
33265 | 6 |
|
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
7 |
signature PREDICATE_COMPILE = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
8 |
sig |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
9 |
val setup : theory -> theory |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
10 |
val preprocess : Predicate_Compile_Aux.options -> string -> theory -> theory |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
11 |
end; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
12 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
13 |
structure Predicate_Compile : PREDICATE_COMPILE = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
14 |
struct |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
15 |
|
33108
9d9afd478016
added test for higher-order function inductification; added debug messages
bulwahn
parents:
33107
diff
changeset
|
16 |
(* options *) |
33139
9c01ee6f8ee9
added skip_proof option; playing with compilation of depth-limited predicates
bulwahn
parents:
33134
diff
changeset
|
17 |
val fail_safe_mode = true |
33108
9d9afd478016
added test for higher-order function inductification; added debug messages
bulwahn
parents:
33107
diff
changeset
|
18 |
|
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
19 |
open Predicate_Compile_Aux; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
20 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
21 |
(* Some last processing *) |
33113 | 22 |
|
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
23 |
fun remove_pointless_clauses intro = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
24 |
if Logic.strip_imp_prems (prop_of intro) = [@{prop "False"}] then |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
25 |
[] |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
26 |
else [intro] |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
27 |
|
33125 | 28 |
fun print_intross options thy msg intross = |
29 |
if show_intermediate_results options then |
|
33376
5cb663aa48ee
predicate compiler creates code equations for predicates with full mode
bulwahn
parents:
33375
diff
changeset
|
30 |
tracing (msg ^ |
5cb663aa48ee
predicate compiler creates code equations for predicates with full mode
bulwahn
parents:
33375
diff
changeset
|
31 |
(space_implode "\n" (map |
5cb663aa48ee
predicate compiler creates code equations for predicates with full mode
bulwahn
parents:
33375
diff
changeset
|
32 |
(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
|
33 |
commas (map (Display.string_of_thm_global thy) intros)) intross))) |
33125 | 34 |
else () |
35 |
||
33122
7d01480cc8e3
added first support for higher-order function translation
bulwahn
parents:
33121
diff
changeset
|
36 |
fun print_specs thy specs = |
7d01480cc8e3
added first support for higher-order function translation
bulwahn
parents:
33121
diff
changeset
|
37 |
map (fn (c, thms) => "Constant " ^ c ^ " has specification:\n" |
7d01480cc8e3
added first support for higher-order function translation
bulwahn
parents:
33121
diff
changeset
|
38 |
^ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs |
7d01480cc8e3
added first support for higher-order function translation
bulwahn
parents:
33121
diff
changeset
|
39 |
|
33404 | 40 |
(* TODO: *) |
41 |
fun overload_const thy s = s |
|
42 |
||
33146
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33142
diff
changeset
|
43 |
fun map_specs f specs = |
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33142
diff
changeset
|
44 |
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
|
45 |
|
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
46 |
fun process_specification options specs thy' = |
33121
9b10dc5da0e0
added to process higher-order arguments by adding new constants
bulwahn
parents:
33120
diff
changeset
|
47 |
let |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
48 |
val _ = print_step options "Compiling predicates to flat introrules..." |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
49 |
val specs = map (apsnd (map |
33140
83951822bfd0
cleaning the signature of the predicate compiler core; renaming signature and structures to uniform long names
bulwahn
parents:
33139
diff
changeset
|
50 |
(fn th => if is_equationlike th then Predicate_Compile_Data.normalize_equation thy' th else th))) specs |
33121
9b10dc5da0e0
added to process higher-order arguments by adding new constants
bulwahn
parents:
33120
diff
changeset
|
51 |
val (intross1, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess specs thy') |
33125 | 52 |
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
|
53 |
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
|
54 |
val intross2 = |
9b10dc5da0e0
added to process higher-order arguments by adding new constants
bulwahn
parents:
33120
diff
changeset
|
55 |
if fail_safe_mode then |
33146
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33142
diff
changeset
|
56 |
case try (map_specs (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross1 of |
33121
9b10dc5da0e0
added to process higher-order arguments by adding new constants
bulwahn
parents:
33120
diff
changeset
|
57 |
SOME intross => intross |
9b10dc5da0e0
added to process higher-order arguments by adding new constants
bulwahn
parents:
33120
diff
changeset
|
58 |
| NONE => let val _ = warning "Function replacement failed!" in intross1 end |
33146
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33142
diff
changeset
|
59 |
else map_specs (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross1 |
33125 | 60 |
val _ = print_intross options thy'' "Introduction rules with replaced functions: " intross2 |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
61 |
val _ = print_step options "Introducing new constants for abstractions at higher-order argument positions..." |
33121
9b10dc5da0e0
added to process higher-order arguments by adding new constants
bulwahn
parents:
33120
diff
changeset
|
62 |
val (intross3, (new_defs, thy''')) = Predicate_Compile_Pred.flat_higher_order_arguments (intross2, thy'') |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
63 |
val (new_intross, thy'''') = |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
64 |
if not (null new_defs) then |
33404 | 65 |
let |
66 |
val _ = print_step options "Recursively obtaining introduction rules for new definitions..." |
|
67 |
in process_specification options new_defs thy''' end |
|
68 |
else ([], thy''') |
|
33121
9b10dc5da0e0
added to process higher-order arguments by adding new constants
bulwahn
parents:
33120
diff
changeset
|
69 |
in |
9b10dc5da0e0
added to process higher-order arguments by adding new constants
bulwahn
parents:
33120
diff
changeset
|
70 |
(intross3 @ new_intross, thy'''') |
9b10dc5da0e0
added to process higher-order arguments by adding new constants
bulwahn
parents:
33120
diff
changeset
|
71 |
end |
9b10dc5da0e0
added to process higher-order arguments by adding new constants
bulwahn
parents:
33120
diff
changeset
|
72 |
|
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
73 |
fun preprocess_strong_conn_constnames options gr constnames thy = |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
74 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
75 |
val get_specs = map (fn k => (k, Graph.get_node gr k)) |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
76 |
val _ = print_step options ("Preprocessing scc of " ^ commas constnames) |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
77 |
val (prednames, funnames) = List.partition (is_pred thy) constnames |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
78 |
(* untangle recursion by defining predicates for all functions *) |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
79 |
val _ = print_step options |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
80 |
("Compiling functions (" ^ commas funnames ^ ") to predicates...") |
33122
7d01480cc8e3
added first support for higher-order function translation
bulwahn
parents:
33121
diff
changeset
|
81 |
val (fun_pred_specs, thy') = |
7d01480cc8e3
added first support for higher-order function translation
bulwahn
parents:
33121
diff
changeset
|
82 |
if not (null funnames) then Predicate_Compile_Fun.define_predicates |
7d01480cc8e3
added first support for higher-order function translation
bulwahn
parents:
33121
diff
changeset
|
83 |
(get_specs funnames) thy else ([], thy) |
7d01480cc8e3
added first support for higher-order function translation
bulwahn
parents:
33121
diff
changeset
|
84 |
val _ = print_specs thy' fun_pred_specs |
7d01480cc8e3
added first support for higher-order function translation
bulwahn
parents:
33121
diff
changeset
|
85 |
val specs = (get_specs prednames) @ fun_pred_specs |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
86 |
val (intross3, thy''') = process_specification options specs thy' |
33125 | 87 |
val _ = print_intross options thy''' "Introduction rules with new constants: " intross3 |
33146
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33142
diff
changeset
|
88 |
val intross4 = map_specs (maps remove_pointless_clauses) intross3 |
33125 | 89 |
val _ = print_intross options thy''' "After removing pointless clauses: " intross4 |
33404 | 90 |
val intross5 = (*map (fn (s, ths) => (overload_const s, map (AxClass.overload thy''') ths))*) intross4 |
33146
bf852ef586f2
now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents:
33142
diff
changeset
|
91 |
val intross6 = map_specs (map (expand_tuples thy''')) intross4 |
33125 | 92 |
val _ = print_intross options thy''' "introduction rules before registering: " intross6 |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
93 |
val _ = print_step options "Registering introduction rules..." |
33121
9b10dc5da0e0
added to process higher-order arguments by adding new constants
bulwahn
parents:
33120
diff
changeset
|
94 |
val thy'''' = fold Predicate_Compile_Core.register_intros intross6 thy''' |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
95 |
in |
33121
9b10dc5da0e0
added to process higher-order arguments by adding new constants
bulwahn
parents:
33120
diff
changeset
|
96 |
thy'''' |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
97 |
end; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
98 |
|
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
99 |
fun preprocess options const thy = |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
100 |
let |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
101 |
val _ = print_step options "Fetching definitions from theory..." |
33404 | 102 |
val table = Predicate_Compile_Data.make_const_spec_table options thy |
33252
8bd2eb003b8f
print retrieved specification when printing intermediate results
bulwahn
parents:
33251
diff
changeset
|
103 |
val gr = Predicate_Compile_Data.obtain_specification_graph options thy table const |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
104 |
val gr = Graph.subgraph (member (op =) (Graph.all_succs gr [const])) gr |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
105 |
in fold_rev (preprocess_strong_conn_constnames options gr) |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
106 |
(Graph.strong_conn gr) thy |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
107 |
end |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
108 |
|
33132
07efd452a698
moved argument expected_modes into options; improved mode check to only check mode of the named predicate
bulwahn
parents:
33131
diff
changeset
|
109 |
fun extract_options ((modes, raw_options), const) = |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
110 |
let |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
111 |
fun chk s = member (op =) raw_options s |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
112 |
in |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
113 |
Options { |
33132
07efd452a698
moved argument expected_modes into options; improved mode check to only check mode of the named predicate
bulwahn
parents:
33131
diff
changeset
|
114 |
expected_modes = Option.map (pair const) modes, |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
115 |
show_steps = chk "show_steps", |
33125 | 116 |
show_intermediate_results = chk "show_intermediate_results", |
33127 | 117 |
show_proof_trace = chk "show_proof_trace", |
33251 | 118 |
show_modes = chk "show_modes", |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
119 |
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
|
120 |
show_compilation = chk "show_compilation", |
9c01ee6f8ee9
added skip_proof option; playing with compilation of depth-limited predicates
bulwahn
parents:
33134
diff
changeset
|
121 |
skip_proof = chk "skip_proof", |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
122 |
inductify = chk "inductify", |
33375 | 123 |
random = chk "random", |
33473
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
33404
diff
changeset
|
124 |
depth_limited = chk "depth_limited", |
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
33404
diff
changeset
|
125 |
annotated = chk "annotated" |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
126 |
} |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
127 |
end |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
128 |
|
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
129 |
fun code_pred_cmd ((modes, raw_options), raw_const) lthy = |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
130 |
let |
33132
07efd452a698
moved argument expected_modes into options; improved mode check to only check mode of the named predicate
bulwahn
parents:
33131
diff
changeset
|
131 |
val thy = ProofContext.theory_of lthy |
07efd452a698
moved argument expected_modes into options; improved mode check to only check mode of the named predicate
bulwahn
parents:
33131
diff
changeset
|
132 |
val const = Code.read_const thy raw_const |
07efd452a698
moved argument expected_modes into options; improved mode check to only check mode of the named predicate
bulwahn
parents:
33131
diff
changeset
|
133 |
val options = extract_options ((modes, raw_options), const) |
07efd452a698
moved argument expected_modes into options; improved mode check to only check mode of the named predicate
bulwahn
parents:
33131
diff
changeset
|
134 |
in |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
135 |
if (is_inductify options) then |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
136 |
let |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
137 |
val lthy' = LocalTheory.theory (preprocess options const) lthy |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
138 |
|> LocalTheory.checkpoint |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
139 |
val const = case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
140 |
SOME c => c |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
141 |
| NONE => const |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
142 |
val _ = print_step options "Starting Predicate Compile Core..." |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
143 |
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
|
144 |
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
|
145 |
end |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
146 |
else |
33132
07efd452a698
moved argument expected_modes into options; improved mode check to only check mode of the named predicate
bulwahn
parents:
33131
diff
changeset
|
147 |
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
|
148 |
end |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
149 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
150 |
val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
151 |
|
33251 | 152 |
val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes", |
33473
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
33404
diff
changeset
|
153 |
"show_mode_inference", "show_compilation", "skip_proof", "inductify", "random", "depth_limited", |
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
33404
diff
changeset
|
154 |
"annotated"] |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
155 |
|
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
156 |
local structure P = OuterParse |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
157 |
in |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
158 |
|
33327 | 159 |
(*val parse_argmode' = P.nat >> rpair NONE || P.$$$ "(" |-- P.enum1 "," --| P.$$$ ")"*) |
160 |
datatype raw_argmode = Argmode of string | Argmode_Tuple of string list |
|
161 |
||
162 |
val parse_argmode' = |
|
163 |
((Args.$$$ "i" || Args.$$$ "o") >> Argmode) || |
|
164 |
(Args.$$$ "(" |-- P.enum1 "," (Args.$$$ "i" || Args.$$$ "o") --| Args.$$$ ")" >> Argmode_Tuple) |
|
165 |
||
166 |
fun mk_numeral_mode ss = flat (map_index (fn (i, s) => if s = "i" then [i + 1] else []) ss) |
|
167 |
||
168 |
val parse_smode' = P.$$$ "[" |-- P.enum1 "," parse_argmode' --| P.$$$ "]" |
|
169 |
>> (fn m => flat (map_index |
|
170 |
(fn (i, Argmode s) => if s = "i" then [(i + 1, NONE)] else [] |
|
171 |
| (i, Argmode_Tuple ss) => [(i + 1, SOME (mk_numeral_mode ss))]) m)) |
|
172 |
||
33330
d6eb7f19bfc6
encapsulating records with datatype constructors and adding type annotations to make SML/NJ happy
bulwahn
parents:
33329
diff
changeset
|
173 |
val parse_smode = (P.$$$ "[" |-- P.enum "," P.nat --| P.$$$ "]") |
d6eb7f19bfc6
encapsulating records with datatype constructors and adding type annotations to make SML/NJ happy
bulwahn
parents:
33329
diff
changeset
|
174 |
>> map (rpair (NONE : int list option)) |
33327 | 175 |
|
176 |
fun gen_parse_mode smode_parser = |
|
177 |
(Scan.optional |
|
33329
b129e4c476d6
improved mode parser; added mode annotations to examples
bulwahn
parents:
33327
diff
changeset
|
178 |
((P.enum "=>" ((Args.$$$ "X" >> K NONE) || (smode_parser >> SOME))) --| Args.$$$ "==>") []) |
b129e4c476d6
improved mode parser; added mode annotations to examples
bulwahn
parents:
33327
diff
changeset
|
179 |
-- smode_parser |
33327 | 180 |
|
181 |
val parse_mode = gen_parse_mode parse_smode |
|
182 |
||
183 |
val parse_mode' = gen_parse_mode parse_smode' |
|
184 |
||
33114
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
185 |
val opt_modes = |
33142
edab304696ec
adapted parser for options in the predicate compiler
bulwahn
parents:
33140
diff
changeset
|
186 |
Scan.optional (P.$$$ "(" |-- Args.$$$ "mode" |-- P.$$$ ":" |-- |
33327 | 187 |
P.enum1 "," (parse_mode || parse_mode') --| P.$$$ ")" >> 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
|
188 |
|
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
189 |
val scan_params = |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
190 |
let |
33142
edab304696ec
adapted parser for options in the predicate compiler
bulwahn
parents:
33140
diff
changeset
|
191 |
val scan_bool_param = foldl1 (op ||) (map Args.$$$ bool_options) |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
192 |
in |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
193 |
Scan.optional (P.$$$ "[" |-- P.enum1 "," scan_bool_param --| P.$$$ "]") [] |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
194 |
end |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33122
diff
changeset
|
195 |
|
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
196 |
val _ = OuterSyntax.local_theory_to_proof "code_pred" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
197 |
"prove equations for predicate specified by intro/elim rules" |
33329
b129e4c476d6
improved mode parser; added mode annotations to examples
bulwahn
parents:
33327
diff
changeset
|
198 |
OuterKeyword.thy_goal (opt_modes -- scan_params -- P.term_group >> code_pred_cmd) |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
199 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
200 |
end |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
201 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
202 |
end |