139 show_proof_trace : bool, |
139 show_proof_trace : bool, |
140 show_intermediate_results : bool, |
140 show_intermediate_results : bool, |
141 |
141 |
142 inductify : bool, |
142 inductify : bool, |
143 rpred : bool, |
143 rpred : bool, |
144 sizelim : bool |
144 depth_limited : bool |
145 }; |
145 }; |
146 |
146 |
147 fun expected_modes (Options opt) = #expected_modes opt |
147 fun expected_modes (Options opt) = #expected_modes opt |
148 fun show_steps (Options opt) = #show_steps opt |
148 fun show_steps (Options opt) = #show_steps opt |
149 fun show_mode_inference (Options opt) = #show_mode_inference opt |
149 fun show_mode_inference (Options opt) = #show_mode_inference opt |
150 fun show_intermediate_results (Options opt) = #show_intermediate_results opt |
150 fun show_intermediate_results (Options opt) = #show_intermediate_results opt |
151 fun show_proof_trace (Options opt) = #show_proof_trace opt |
151 fun show_proof_trace (Options opt) = #show_proof_trace opt |
152 |
152 |
153 fun is_inductify (Options opt) = #inductify opt |
153 fun is_inductify (Options opt) = #inductify opt |
154 fun is_rpred (Options opt) = #rpred opt |
154 fun is_rpred (Options opt) = #rpred opt |
155 fun is_sizelim (Options opt) = #sizelim opt |
155 fun is_depth_limited (Options opt) = #depth_limited opt |
156 |
156 |
157 val default_options = Options { |
157 val default_options = Options { |
158 expected_modes = NONE, |
158 expected_modes = NONE, |
159 show_steps = false, |
159 show_steps = false, |
160 show_intermediate_results = false, |
160 show_intermediate_results = false, |
161 show_proof_trace = false, |
161 show_proof_trace = false, |
162 show_mode_inference = false, |
162 show_mode_inference = false, |
163 inductify = false, |
163 inductify = false, |
164 rpred = false, |
164 rpred = false, |
165 sizelim = false |
165 depth_limited = false |
166 } |
166 } |
167 |
167 |
168 |
168 |
169 fun print_step options s = |
169 fun print_step options s = |
170 if show_steps options then tracing s else () |
170 if show_steps options then tracing s else () |