equal
deleted
inserted
replaced
9 |
9 |
10 structure Predicate_Compile : PREDICATE_COMPILE = |
10 structure Predicate_Compile : PREDICATE_COMPILE = |
11 struct |
11 struct |
12 |
12 |
13 (* options *) |
13 (* options *) |
14 val fail_safe_mode = false |
14 val fail_safe_mode = true |
15 |
15 |
16 open Predicate_Compile_Aux; |
16 open Predicate_Compile_Aux; |
17 |
17 |
18 val priority = tracing; |
18 val priority = tracing; |
19 |
19 |
109 expected_modes = Option.map (pair const) modes, |
109 expected_modes = Option.map (pair const) modes, |
110 show_steps = chk "show_steps", |
110 show_steps = chk "show_steps", |
111 show_intermediate_results = chk "show_intermediate_results", |
111 show_intermediate_results = chk "show_intermediate_results", |
112 show_proof_trace = chk "show_proof_trace", |
112 show_proof_trace = chk "show_proof_trace", |
113 show_mode_inference = chk "show_mode_inference", |
113 show_mode_inference = chk "show_mode_inference", |
|
114 show_compilation = chk "show_compilation", |
|
115 skip_proof = chk "skip_proof", |
114 inductify = chk "inductify", |
116 inductify = chk "inductify", |
115 rpred = chk "rpred", |
117 rpred = chk "rpred", |
116 depth_limited = chk "depth_limited" |
118 depth_limited = chk "depth_limited" |
117 } |
119 } |
118 end |
120 end |
139 end |
141 end |
140 |
142 |
141 val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup |
143 val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup |
142 |
144 |
143 val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", |
145 val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", |
144 "show_mode_inference", "inductify", "rpred", "depth_limited"] |
146 "show_mode_inference", "show_compilation", "skip_proof", "inductify", "rpred", "depth_limited"] |
145 |
147 |
146 val _ = List.app OuterKeyword.keyword ("mode" :: bool_options) |
148 val _ = List.app OuterKeyword.keyword ("mode" :: bool_options) |
147 |
149 |
148 local structure P = OuterParse |
150 local structure P = OuterParse |
149 in |
151 in |