1use crate::context::{store, Context, Ptr, Store};
2use crate::error::Kind;
3use crate::stream;
4use crate::KResult;
5use crate::Var;
6use crate::{Sort, State, Table, Term, Theorem};
7
8use crate::opcode;
9
10#[derive(Debug, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
11pub enum FinalizeState {
12 Theorem(bool),
13 Unfold,
14}
15
16pub trait Proof<T>
17where
18 T: Table,
19{
20 fn end(&mut self) -> KResult;
21
22 fn reference(&mut self, idx: u32) -> KResult;
23
24 fn dummy(&mut self, table: &T, sort: u32, current_sort: u32) -> KResult;
25
26 fn term(&mut self, table: &T, idx: u32, current_term: u32, save: bool, def: bool) -> KResult;
27
28 fn theorem(&mut self, table: &T, idx: u32, save: bool) -> KResult;
29
30 fn theorem_start(
31 &mut self,
32 table: &T,
33 idx: u32,
34 current_theorem: u32,
35 save: bool,
36 ) -> KResult<(stream::unify::Stepper, Ptr, bool)>;
37
38 fn theorem_end(&mut self, target: Ptr, save: bool) -> KResult;
39
40 fn hyp(&mut self, table: &T) -> KResult;
41
42 fn conv(&mut self) -> KResult;
43
44 fn refl(&mut self) -> KResult;
45
46 fn symm(&mut self) -> KResult;
47
48 fn cong(&mut self) -> KResult;
49
50 fn unfold_start(&mut self, table: &T) -> KResult<(stream::unify::Stepper, Ptr, Ptr)>;
51
52 fn unfold_end(&mut self, t_ptr: Ptr, e: Ptr) -> KResult;
53
54 fn unfold(&mut self, table: &T) -> KResult;
55
56 fn conv_cut(&mut self) -> KResult;
57
58 fn conv_ref(&mut self, idx: u32) -> KResult;
59
60 fn conv_save(&mut self) -> KResult;
61
62 fn save(&mut self) -> KResult;
63
64 fn execute(
65 &mut self,
66 table: &T,
67 state: &State,
68 command: opcode::Command<opcode::Proof>,
69 is_definition: bool,
70 ) -> KResult<bool> {
71 use crate::opcode::Proof::*;
72 match (command.opcode, is_definition) {
73 (End, _) => {
74 self.end()?;
75 return Ok(true);
76 }
77 (Ref, _) => self.reference(command.operand),
78 (Dummy, _) => self.dummy(table, command.operand, state.current_sort().into()),
79 (Term, _) => self.term(
80 table,
81 command.operand,
82 state.current_term(),
83 false,
84 is_definition,
85 ),
86 (TermSave, _) => self.term(
87 table,
88 command.operand,
89 state.current_term(),
90 true,
91 is_definition,
92 ),
93 (Thm, false) => self.theorem(table, command.operand, false),
94 (ThmSave, false) => self.theorem(table, command.operand, true),
95 (Thm, true) => Err(Kind::InvalidOpcodeInDef),
96 (ThmSave, true) => Err(Kind::InvalidOpcodeInDef),
97 (Hyp, false) => self.hyp(table),
98 (Hyp, true) => Err(Kind::InvalidOpcodeInDef),
99 (Conv, _) => self.conv(),
100 (Refl, _) => self.refl(),
101 (Symm, _) => self.symm(),
102 (Cong, _) => self.cong(),
103 (Unfold, _) => self.unfold(table),
104 (ConvCut, _) => self.conv_cut(),
105 (ConvRef, _) => self.conv_ref(command.operand),
106 (ConvSave, _) => self.conv_save(),
107 (Save, _) => self.save(),
108 }?;
109
110 Ok(false)
111 }
112
113 fn step(
114 &mut self,
115 table: &T,
116 state: &State,
117 command: opcode::Command<opcode::Proof>,
118 is_definition: bool,
119 ) -> KResult<Option<FinalizeState>> {
120 use crate::opcode::Proof::*;
121 match (command.opcode, is_definition) {
122 (End, _) => {
123 self.end()?;
124 return Ok(None);
125 }
126 (Ref, _) => self.reference(command.operand),
127 (Dummy, _) => self.dummy(table, command.operand, state.current_sort().into()),
128 (Term, _) => self.term(
129 table,
130 command.operand,
131 state.current_term(),
132 false,
133 is_definition,
134 ),
135 (TermSave, _) => self.term(
136 table,
137 command.operand,
138 state.current_term(),
139 true,
140 is_definition,
141 ),
142 (Thm, false) => {
143 return Ok(Some(FinalizeState::Theorem(false)));
144 }
145 (ThmSave, false) => {
146 return Ok(Some(FinalizeState::Theorem(true)));
147 }
148 (Thm, true) => Err(Kind::InvalidOpcodeInDef),
149 (ThmSave, true) => Err(Kind::InvalidOpcodeInDef),
150 (Hyp, false) => self.hyp(table),
151 (Hyp, true) => Err(Kind::InvalidOpcodeInDef),
152 (Conv, _) => self.conv(),
153 (Refl, _) => self.refl(),
154 (Symm, _) => self.symm(),
155 (Cong, _) => self.cong(),
156 (Unfold, _) => {
157 return Ok(Some(FinalizeState::Unfold));
158 }
159 (ConvCut, _) => self.conv_cut(),
160 (ConvRef, _) => self.conv_ref(command.operand),
161 (ConvSave, _) => self.conv_save(),
162 (Save, _) => self.save(),
163 }?;
164
165 Ok(None)
167 }
168}
169
170impl<T, S: Store> Proof<T> for Context<S>
171where
172 T: Table<Var = S::Var>,
173{
174 fn end(&mut self) -> KResult {
175 Ok(())
177 }
178
179 fn reference(&mut self, idx: u32) -> KResult {
180 let i = self.proof_heap.get(idx).ok_or(Kind::InvalidHeapIndex)?;
181
182 self.proof_stack.push(i);
183
184 Ok(())
185 }
186
187 fn dummy(&mut self, table: &T, sort: u32, current_sort: u32) -> KResult {
188 if sort >= current_sort {
189 return Err(Kind::SortOutOfRange);
190 }
191
192 let s = table.sort(sort as u8).ok_or(Kind::InvalidSort)?;
193
194 if s.is_strict() {
195 return Err(Kind::SortIsStrict);
196 }
197
198 if (self.next_bv >> 56) != 0 {
199 return Err(Kind::TooManyBoundVariables);
200 }
201
202 let ty = Var::new(sort as u8, self.next_bv, true);
203
204 self.next_bv *= 2;
205
206 let ptr = self.store.alloc_var(ty, self.proof_heap.len() as u16);
207
208 self.proof_stack.push(ptr);
209 self.proof_heap.push(ptr);
210
211 Ok(())
212 }
213
214 fn term(&mut self, table: &T, idx: u32, current_term: u32, save: bool, def: bool) -> KResult {
215 if idx >= current_term {
216 return Err(Kind::TermOutOfRange);
217 }
218
219 let term = table.term(idx).ok_or(Kind::InvalidTerm)?;
220
221 let binders = term.binders();
222 let nr_args = binders.len();
223 let last = self.proof_stack.get_last(nr_args)?;
224
225 let binders = table.binders(binders).ok_or(Kind::InvalidBinderIndices)?;
226
227 let ptr = self.store.create_term(
228 idx,
229 last.iter().cloned(),
230 binders,
231 term.return_type(),
232 term.sort_idx(),
233 def,
234 )?;
235
236 self.proof_stack.truncate_last(nr_args);
237
238 self.proof_stack.push(ptr);
239
240 if save {
241 self.proof_heap.push(ptr);
242 }
243
244 Ok(())
245 }
246
247 fn theorem(&mut self, table: &T, idx: u32, save: bool) -> KResult {
248 let thm = table.theorem(idx).ok_or(Kind::InvalidTheorem)?;
249 let target = self
250 .proof_stack
251 .pop()
252 .ok_or(Kind::ProofStackUnderflow)?
253 .as_expr()
254 .ok_or(Kind::InvalidStoreExpr)?;
255
256 let types = thm.binders();
257 let nr_args = types.len();
258 let last = self.proof_stack.get_last(nr_args)?;
259
260 let types = table.binders(types).ok_or(Kind::InvalidBinderIndices)?;
261
262 self.unify_heap.clear();
263
264 let mut g_deps = [0; 256];
265 let mut bound: u8 = 0;
266
267 for (i, (&arg, &target_type)) in last.iter().zip(types.iter()).enumerate() {
268 let arg = arg.as_expr().ok_or(Kind::InvalidStoreExpr)?;
269
270 let ty = self
271 .store
272 .get_type_of_expr(arg)
273 .ok_or(Kind::InvalidStoreExpr)?;
274
275 let deps = ty.dependencies();
276
277 if target_type.is_bound() {
278 *g_deps
279 .get_mut(bound as usize)
280 .ok_or(Kind::DependencyOverflow)? = deps;
281
282 bound += 1;
283
284 for &i in last.get(..i).ok_or(Kind::DependencyOverflow)? {
285 let i = i.as_expr().ok_or(Kind::InvalidStoreExpr)?;
286
287 let d = self
288 .store
289 .get_type_of_expr(i)
290 .ok_or(Kind::InvalidStoreExpr)?;
291
292 if d.depends_on_full(deps) {
293 return Err(Kind::DisjointVariableViolation);
294 }
295 }
296 } else {
297 for (i, &j) in g_deps
298 .get(..(bound as usize))
299 .ok_or(Kind::DependencyOverflow)?
300 .iter()
301 .enumerate()
302 {
303 if !(target_type.depends_on(i as u8) || ((j & deps) == 0)) {
304 return Err(Kind::DisjointVariableViolation);
305 }
306 }
307 }
308 }
309
310 self.unify_heap.extend(last);
311 self.proof_stack.truncate_last(nr_args);
312
313 let commands = thm.unify_commands();
314
315 stream::unify::Run::run(self, commands, table, stream::unify::Mode::Thm, target)?;
316
317 let proof = target.to_proof();
318
319 self.proof_stack.push(proof);
320
321 if save {
322 self.proof_heap.push(proof);
323 }
324
325 Ok(())
326 }
327
328 fn theorem_start(
329 &mut self,
330 table: &T,
331 idx: u32,
332 current_theorem: u32,
333 save: bool,
334 ) -> KResult<(stream::unify::Stepper, Ptr, bool)> {
335 if idx >= current_theorem {
336 return Err(Kind::TheoremOutOfRange);
337 }
338
339 let thm = table.theorem(idx).ok_or(Kind::InvalidTheorem)?;
340 let target = self
341 .proof_stack
342 .pop()
343 .ok_or(Kind::ProofStackUnderflow)?
344 .as_expr()
345 .ok_or(Kind::InvalidStoreExpr)?;
346
347 let types = thm.binders();
348 let nr_args = types.len();
349 let last = self.proof_stack.get_last(nr_args)?;
350
351 let types = table.binders(types).ok_or(Kind::InvalidBinderIndices)?;
352
353 self.unify_heap.clear();
354
355 let mut g_deps = [0; 256];
356 let mut bound: u8 = 0;
357
358 for (i, (&arg, &target_type)) in last.iter().zip(types.iter()).enumerate() {
359 let arg = arg.as_expr().ok_or(Kind::InvalidStoreExpr)?;
360
361 let ty = self
362 .store
363 .get_type_of_expr(arg)
364 .ok_or(Kind::InvalidStoreExpr)?;
365
366 let deps = ty.dependencies();
367
368 if target_type.is_bound() {
369 *g_deps
370 .get_mut(bound as usize)
371 .ok_or(Kind::DependencyOverflow)? = deps;
372
373 bound += 1;
374
375 for &i in last.get(..i).ok_or(Kind::DependencyOverflow)? {
376 let i = i.as_expr().ok_or(Kind::InvalidStoreExpr)?;
377
378 let d = self
379 .store
380 .get_type_of_expr(i)
381 .ok_or(Kind::InvalidStoreExpr)?;
382
383 if d.depends_on_full(deps) {
384 return Err(Kind::DisjointVariableViolation);
385 }
386 }
387 } else {
388 for (i, &j) in g_deps
389 .get(..(bound as usize))
390 .ok_or(Kind::DependencyOverflow)?
391 .iter()
392 .enumerate()
393 {
394 if !(target_type.depends_on(i as u8) || ((j & deps) == 0)) {
395 return Err(Kind::DisjointVariableViolation);
396 }
397 }
398 }
399 }
400
401 self.unify_heap.extend(last);
402 self.proof_stack.truncate_last(nr_args);
403
404 let commands = thm.unify_commands();
405
406 let stepper = stream::unify::Stepper::new(stream::unify::Mode::Thm, target, commands);
407
408 Ok((stepper, target, save))
409 }
410
411 fn theorem_end(&mut self, target: Ptr, save: bool) -> KResult {
412 let proof = target.to_proof();
413
414 self.proof_stack.push(proof);
415
416 if save {
417 self.proof_heap.push(proof);
418 }
419
420 Ok(())
421 }
422
423 fn hyp(&mut self, table: &T) -> KResult {
424 let e = self
425 .proof_stack
426 .pop()
427 .ok_or(Kind::ProofStackUnderflow)?
428 .as_expr()
429 .ok_or(Kind::InvalidStoreExpr)?;
430 let ty = self
431 .store
432 .get_type_of_expr(e)
433 .ok_or(Kind::InvalidStoreExpr)?;
434
435 let sort = table.sort(ty.sort_idx()).ok_or(Kind::InvalidSort)?;
436
437 if !sort.is_provable() {
438 return Err(Kind::SortNotProvable);
439 }
440
441 self.hyp_stack.push(e.to_expr());
442 self.proof_heap.push(e.to_proof());
443
444 Ok(())
445 }
446
447 fn conv(&mut self) -> KResult {
448 let e2 = self
449 .proof_stack
450 .pop()
451 .ok_or(Kind::ProofStackUnderflow)?
452 .as_proof()
453 .ok_or(Kind::InvalidStoreExpr)?;
454 let e1 = self
455 .proof_stack
456 .pop()
457 .ok_or(Kind::ProofStackUnderflow)?
458 .as_expr()
459 .ok_or(Kind::InvalidStoreExpr)?;
460
461 self.proof_stack.push(e1.to_proof());
462 self.proof_stack.push(e2.to_expr());
463 self.proof_stack.push(e1.to_co_conv());
464
465 Ok(())
466 }
467
468 fn refl(&mut self) -> KResult {
469 let e1 = self
470 .proof_stack
471 .pop()
472 .ok_or(Kind::ProofStackUnderflow)?
473 .as_co_conv()
474 .ok_or(Kind::InvalidStoreExpr)?;
475 let e2 = self
476 .proof_stack
477 .pop()
478 .ok_or(Kind::ProofStackUnderflow)?
479 .as_expr()
480 .ok_or(Kind::InvalidStoreExpr)?;
481
482 if e1 != e2 {
483 return Err(Kind::UnifyRefFailure);
484 }
485
486 Ok(())
487 }
488
489 fn symm(&mut self) -> KResult {
490 let e1 = self
491 .proof_stack
492 .pop()
493 .ok_or(Kind::ProofStackUnderflow)?
494 .as_co_conv()
495 .ok_or(Kind::InvalidStoreExpr)?;
496 let e2 = self
497 .proof_stack
498 .pop()
499 .ok_or(Kind::ProofStackUnderflow)?
500 .as_expr()
501 .ok_or(Kind::InvalidStoreExpr)?;
502
503 self.proof_stack.push(e1.to_expr());
504 self.proof_stack.push(e2.to_co_conv());
505
506 Ok(())
507 }
508
509 fn cong(&mut self) -> KResult {
510 let e1 = self
511 .proof_stack
512 .pop()
513 .ok_or(Kind::ProofStackUnderflow)?
514 .as_co_conv()
515 .ok_or(Kind::InvalidStoreExpr)?;
516
517 let e2 = self
518 .proof_stack
519 .pop()
520 .ok_or(Kind::ProofStackUnderflow)?
521 .as_expr()
522 .ok_or(Kind::InvalidStoreExpr)?;
523
524 let e1: store::Term<_> = self.store.get(e1)?;
525 let e2: store::Term<_> = self.store.get(e2)?;
526
527 if e1.id != e2.id {
528 return Err(Kind::CongUnifyError);
529 }
530
531 for (i, j) in e1.args.iter().zip(e2.args.iter()).rev() {
532 self.proof_stack.push(Into::<Ptr>::into(j).to_expr());
533 self.proof_stack.push(Into::<Ptr>::into(i).to_co_conv());
534 }
535
536 Ok(())
537 }
538
539 fn unfold_start(&mut self, table: &T) -> KResult<(stream::unify::Stepper, Ptr, Ptr)> {
540 let e = self
541 .proof_stack
542 .pop()
543 .ok_or(Kind::ProofStackUnderflow)?
544 .as_expr()
545 .ok_or(Kind::InvalidStoreType)?;
546
547 let t_ptr = self
548 .proof_stack
549 .pop()
550 .ok_or(Kind::ProofStackUnderflow)?
551 .as_expr()
552 .ok_or(Kind::InvalidStoreType)?;
553
554 let t: store::Term<_> = self.store.get(t_ptr)?;
555
556 let term = table.term(*t.id).ok_or(Kind::InvalidTerm)?;
557
558 if !term.is_definition() {
559 return Err(Kind::InvalidSort);
560 }
561
562 self.unify_heap.clear();
563 self.unify_heap.extend(t.args);
564
565 let commands = term.command_stream();
566
567 let stepper = stream::unify::Stepper::new(stream::unify::Mode::Def, e, commands);
568
569 Ok((stepper, t_ptr, e))
570 }
571
572 fn unfold_end(&mut self, t_ptr: Ptr, e: Ptr) -> KResult {
573 let t_prime = self
574 .proof_stack
575 .pop()
576 .ok_or(Kind::ProofStackUnderflow)?
577 .as_co_conv()
578 .ok_or(Kind::InvalidStoreType)?;
579
580 if t_ptr != t_prime {
581 return Err(Kind::UnifyTermFailure);
582 }
583
584 let e2 = self
585 .proof_stack
586 .pop()
587 .ok_or(Kind::ProofStackUnderflow)?
588 .as_expr()
589 .ok_or(Kind::InvalidStoreType)?;
590
591 self.proof_stack.push(e2.to_expr());
592 self.proof_stack.push(e.to_co_conv());
593
594 Ok(())
595 }
596
597 fn unfold(&mut self, table: &T) -> KResult {
598 let e = self
599 .proof_stack
600 .pop()
601 .ok_or(Kind::ProofStackUnderflow)?
602 .as_expr()
603 .ok_or(Kind::InvalidStoreType)?;
604
605 let t_ptr = self
606 .proof_stack
607 .pop()
608 .ok_or(Kind::ProofStackUnderflow)?
609 .as_expr()
610 .ok_or(Kind::InvalidStoreType)?;
611
612 let t: store::Term<_> = self.store.get(t_ptr)?;
613
614 let term = table.term(*t.id).ok_or(Kind::InvalidTerm)?;
615
616 if !term.is_definition() {
617 return Err(Kind::InvalidSort);
618 }
619
620 self.unify_heap.clear();
621 self.unify_heap.extend(t.args);
622
623 let commands = term.command_stream();
624
625 stream::unify::Run::run(self, commands, table, stream::unify::Mode::Def, e)?;
626
627 let t_prime = self
628 .proof_stack
629 .pop()
630 .ok_or(Kind::ProofStackUnderflow)?
631 .as_co_conv()
632 .ok_or(Kind::InvalidStoreType)?;
633
634 if t_ptr != t_prime {
635 return Err(Kind::UnifyTermFailure);
636 }
637
638 let e2 = self
639 .proof_stack
640 .pop()
641 .ok_or(Kind::ProofStackUnderflow)?
642 .as_expr()
643 .ok_or(Kind::InvalidStoreType)?;
644
645 self.proof_stack.push(e2.to_expr());
646 self.proof_stack.push(e.to_co_conv());
647
648 Ok(())
649 }
650
651 fn conv_cut(&mut self) -> KResult {
652 let e1 = self
653 .proof_stack
654 .pop()
655 .ok_or(Kind::ProofStackUnderflow)?
656 .as_co_conv()
657 .ok_or(Kind::InvalidStoreExpr)?;
658
659 let e2 = self
660 .proof_stack
661 .pop()
662 .ok_or(Kind::ProofStackUnderflow)?
663 .as_expr()
664 .ok_or(Kind::InvalidStoreExpr)?;
665
666 self.proof_stack.push(e2.to_expr());
667 self.proof_stack.push(e1.to_conv());
668
669 self.proof_stack.push(e2.to_expr());
670 self.proof_stack.push(e1.to_co_conv());
671
672 Ok(())
673 }
674
675 fn conv_ref(&mut self, idx: u32) -> KResult {
676 let x: store::Conv = self.store.get(Ptr(idx))?;
677
678 let e1 = self
679 .proof_stack
680 .pop()
681 .ok_or(Kind::ProofStackUnderflow)?
682 .as_co_conv()
683 .ok_or(Kind::InvalidStoreExpr)?;
684
685 let e2 = self
686 .proof_stack
687 .pop()
688 .ok_or(Kind::ProofStackUnderflow)?
689 .as_expr()
690 .ok_or(Kind::InvalidStoreExpr)?;
691
692 if Into::<Ptr>::into(x.e1) != e1 || Into::<Ptr>::into(x.e2) != e2 {
693 return Err(Kind::UnifyRefFailure);
694 }
695
696 Ok(())
697 }
698
699 fn conv_save(&mut self) -> KResult {
700 let e1 = self
701 .proof_stack
702 .pop()
703 .ok_or(Kind::ProofStackUnderflow)?
704 .as_conv()
705 .ok_or(Kind::InvalidStoreExpr)?;
706
707 let e2 = self
708 .proof_stack
709 .pop()
710 .ok_or(Kind::ProofStackUnderflow)?
711 .as_expr()
712 .ok_or(Kind::InvalidStoreExpr)?;
713
714 let ptr = self.store.alloc_conv(e1.to_expr(), e2.to_expr());
715 self.proof_heap.push(ptr);
716
717 Ok(())
718 }
719
720 fn save(&mut self) -> KResult {
721 let element = self.proof_stack.peek().ok_or(Kind::ProofStackUnderflow)?;
722
723 if element.as_co_conv().is_some() {
724 return Err(Kind::CantSaveConvertabilityObligation);
725 }
726
727 if element.as_conv().is_some() {
728 let e = self.proof_stack.get_last(2)?;
729
730 let l = Into::<Ptr>::into(e[0]).to_expr();
731 let r = Into::<Ptr>::into(e[1]).to_expr();
732
733 let ptr = self.store.alloc_conv(l, r);
734 self.proof_heap.push(ptr);
735
736 Ok(())
737 } else {
738 self.proof_heap.push(*element);
739 Ok(())
740 }
741 }
742}
743
744use core::convert::TryInto;
745
746pub trait Run<SS: Store> {
747 fn run<T: Table, S>(
748 &mut self,
749 state: &State,
750 table: &T,
751 is_definition: bool,
752 stream: S,
753 ) -> KResult
754 where
755 T: Table<Var = SS::Var>,
756 S: IntoIterator,
757 S::Item: TryInto<opcode::Command<opcode::Proof>>;
758}
759
760impl<SS: Store> Run<SS> for Context<SS> {
761 fn run<T: Table, S>(
762 &mut self,
763 state: &State,
764 table: &T,
765 is_definition: bool,
766 stream: S,
767 ) -> KResult
768 where
769 T: Table<Var = SS::Var>,
770 S: IntoIterator,
771 S::Item: TryInto<opcode::Command<opcode::Proof>>,
772 {
773 for i in stream {
774 let command = i.try_into().map_err(|_| Kind::UnknownCommand)?;
775
776 if self.execute(table, state, command, is_definition)? {
777 return Ok(());
778 }
779 }
780
781 Err(Kind::StreamExhausted)
782 }
783}
784
785#[derive(Debug)]
786enum Continue {
787 Normal,
788 BeforeTheorem {
789 idx: u32,
790 save: bool,
791 },
792 Theorem {
793 idx: u32,
794 save: bool,
795 },
796 UnifyTheorem {
797 stepper: stream::unify::Stepper,
798 target: Ptr,
799 save: bool,
800 },
801 UnifyTheoremDone {
802 target: Ptr,
803 save: bool,
804 },
805 BeforeUnfold,
806 Unfold,
807 UnifyUnfold {
808 stepper: stream::unify::Stepper,
809 t_ptr: Ptr,
810 e: Ptr,
811 },
812 UnfoldDone {
813 t_ptr: Ptr,
814 e: Ptr,
815 },
816}
817
818#[derive(Debug)]
819pub struct Stepper<S> {
820 is_definition: bool,
821 state: State,
822 stream: S,
823 idx: usize,
824 con: Continue,
825}
826
827#[derive(Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
828pub enum Action {
829 Unify(stream::unify::Action),
830 UnifyDone,
831 UnfoldDone,
832 BeforeUnfold,
833 UnfoldApplied,
834 TheoremDone,
835 BeforeTheorem(u32),
836 TheoremApplied,
837 Cmd(usize, opcode::Command<opcode::Proof>),
838}
839
840impl<S> Stepper<S>
841where
842 S: Iterator<Item = opcode::Command<opcode::Proof>>,
843{
844 pub fn new(is_definition: bool, state: State, stream: S) -> Stepper<S> {
845 Stepper {
846 is_definition,
847 state,
848 stream,
849 idx: 0,
850 con: Continue::Normal,
851 }
852 }
853
854 pub fn take_stream(self) -> S {
855 self.stream
856 }
857
858 pub fn run<SS: Store, T: Table<Var = SS::Var>>(
859 &mut self,
860 context: &mut Context<SS>,
861 table: &T,
862 ) -> KResult<()> {
863 while self.step(context, table)?.is_some() {}
864
865 Ok(())
866 }
867
868 pub fn step<SS: Store, T: Table<Var = SS::Var>>(
869 &mut self,
870 context: &mut Context<SS>,
871 table: &T,
872 ) -> KResult<Option<Action>> {
873 let (next_state, ret) = match &mut self.con {
874 Continue::Normal => {
875 if let Some(command) = self.stream.next() {
876 let idx = self.idx;
877 self.idx += 1;
878
879 let next_state =
880 match context.step(table, &self.state, command, self.is_definition)? {
881 Some(FinalizeState::Theorem(save)) => Continue::BeforeTheorem {
882 idx: command.operand,
883 save,
884 },
885 Some(FinalizeState::Unfold) => Continue::BeforeUnfold,
886 None => Continue::Normal,
887 };
888
889 (Some(next_state), Ok(Some(Action::Cmd(idx, command))))
890 } else {
891 (None, Ok(None))
892 }
893 }
894 Continue::BeforeTheorem { ref idx, ref save } => (
895 Some(Continue::Theorem {
896 idx: *idx,
897 save: *save,
898 }),
899 Ok(Some(Action::BeforeTheorem(*idx))),
900 ),
901 Continue::Theorem { idx, save } => {
902 let (x, a, b) =
903 context.theorem_start(table, *idx, self.state.current_theorem(), *save)?;
904 (
905 Some(Continue::UnifyTheorem {
906 stepper: x,
907 target: a,
908 save: b,
909 }),
910 Ok(Some(Action::TheoremApplied)),
911 )
912 }
913
914 Continue::BeforeUnfold => (Some(Continue::Unfold), Ok(Some(Action::BeforeUnfold))),
915 Continue::Unfold => {
916 let (x, a, b) = context.unfold_start(table)?;
917 (
918 Some(Continue::UnifyUnfold {
919 stepper: x,
920 t_ptr: a,
921 e: b,
922 }),
923 Ok(Some(Action::UnfoldApplied)),
924 )
925 }
926 Continue::UnifyUnfold {
927 ref mut stepper,
928 ref t_ptr,
929 ref e,
930 } => match stepper.step(context, table)? {
931 Some(x) => (None, Ok(Some(Action::Unify(x)))),
932 None => (
933 Some(Continue::UnfoldDone {
934 t_ptr: *t_ptr,
935 e: *e,
936 }),
937 Ok(Some(Action::UnifyDone)),
938 ),
939 },
940 Continue::UnfoldDone { t_ptr, e } => {
941 Proof::<T>::unfold_end(context, *t_ptr, *e)?;
942 (Some(Continue::Normal), Ok(Some(Action::UnfoldDone)))
943 }
944 Continue::UnifyTheorem {
945 ref mut stepper,
946 ref target,
947 ref save,
948 } => match stepper.step(context, table)? {
949 Some(x) => (None, Ok(Some(Action::Unify(x)))),
950 None => (
951 Some(Continue::UnifyTheoremDone {
952 target: *target,
953 save: *save,
954 }),
955 Ok(Some(Action::UnifyDone)),
956 ),
957 },
958 Continue::UnifyTheoremDone { target, save } => {
959 Proof::<T>::theorem_end(context, *target, *save)?;
960 (Some(Continue::Normal), Ok(Some(Action::TheoremDone)))
961 }
962 };
963
964 if let Some(x) = next_state {
965 self.con = x;
966 }
967
968 ret
969 }
970}