1use crate::context::{Context, Store};
2use crate::error::Kind;
3use crate::state::State;
4use crate::stream;
5use crate::KResult;
6use crate::Var;
7use crate::{Sort, Table, Term, Theorem};
8
9use core::ops::Range;
10
11#[derive(Debug, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
12pub enum Opcode {
13 End,
14 Sort,
15 TermDef,
16 Axiom,
17 Thm,
18}
19
20use crate::opcode;
21
22pub trait StatementStream: Iterator
23where
24 <Self as Iterator>::Item: TryInto<Opcode>,
25{
26 type ProofStream: Iterator<Item = opcode::Command<opcode::Proof>>;
27
28 fn take_proof_stream(&mut self) -> Option<Self::ProofStream>;
29
30 fn put_proof_stream(&mut self, proofs: Self::ProofStream);
31}
32
33#[derive(Debug)]
34pub enum TermDef<S, Ty> {
35 Start {
36 idx: u32,
37 stream: S,
38 },
39 RunProof {
40 stepper: stream::proof::Stepper<S>,
41 ret_type: Ty,
42 nr_args: usize,
43 commands: Range<usize>,
44 },
45 ProofDone {
46 stream: S,
47 ret_type: Ty,
48 commands: Range<usize>,
49 nr_args: usize,
50 },
51 RunUnify {
52 stream: S,
53 stepper: stream::unify::Stepper,
54 },
55 Done {
56 stream: S,
57 },
58 Dummy,
59}
60
61use core::convert::TryInto;
62
63#[derive(Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
64pub enum TermDefAction {
65 Done,
66 StartProof,
67 Proof(stream::proof::Action),
68 ProofDone,
69 StartUnify,
70 Unify(stream::unify::Action),
71 UnifyDone,
72}
73
74impl<S, Ty> TermDef<S, Ty>
75where
76 S: Iterator<Item = opcode::Command<opcode::Proof>>,
77 Ty: Var,
78{
79 pub fn new(idx: u32, stream: S) -> TermDef<S, Ty> {
80 TermDef::Start { idx, stream }
81 }
82
83 pub fn take_stream_if_done(self) -> Option<S> {
84 match self {
85 TermDef::Done { stream } => Some(stream),
86 _ => None,
87 }
88 }
89
90 pub fn is_done(&self) -> bool {
91 matches!(self, TermDef::Done { .. })
92 }
93
94 pub fn step<SS: Store<Var = Ty>, T: Table<Var = SS::Var>>(
95 &mut self,
96 context: &mut Context<SS>,
97 state: &State,
98 table: &T,
99 ) -> KResult<TermDefAction> {
100 let old = core::mem::replace(self, Self::Dummy);
101
102 let (next_state, ret_val) = match old {
103 TermDef::Start { idx, stream } => {
104 let term = table.term(idx).ok_or(Kind::InvalidTerm)?;
105
106 let sort_idx = term.sort_idx();
107 let current_sort = state.current_sort();
108
109 if sort_idx >= current_sort {
110 return Err(Kind::SortOutOfRange);
111 }
112
113 let sort = table.sort(sort_idx).ok_or(Kind::InvalidSort)?;
114
115 if sort.is_pure() {
116 return Err(Kind::SortIsPure);
117 }
118
119 let binders = term.binders();
120 let nr_args = binders.len();
121 let binders = table.binders(binders).ok_or(Kind::InvalidBinderIndices)?;
122
123 context.store.clear();
124 context.proof_stack.clear();
125 context.proof_heap.clear();
126 context.unify_stack.clear();
127 context.unify_heap.clear();
128 context.hyp_stack.clear();
129
130 context.allocate_binders(table, current_sort, binders)?;
131
132 let mut next_bv = context.next_bv;
133 let ret_type = term.return_type();
134
135 Context::<SS>::binder_check(table, ret_type, current_sort, &mut next_bv)?;
136
137 context.next_bv = next_bv;
138
139 if term.sort_idx() != ret_type.sort_idx() {
140 return Err(Kind::BadReturnType);
141 }
142
143 if !term.is_definition() {
144 (TermDef::Done { stream }, TermDefAction::Done)
145 } else {
146 let stepper = stream::proof::Stepper::new(true, *state, stream);
147
148 let commands = term.command_stream();
149
150 (
151 TermDef::RunProof {
152 stepper,
153 ret_type: *ret_type,
154 nr_args,
155 commands,
156 },
157 TermDefAction::StartProof,
158 )
159 }
160 }
161 TermDef::RunProof {
162 mut stepper,
163 ret_type,
164 nr_args,
165 commands,
166 } => match stepper.step(context, table)? {
167 Some(x) => {
168 (
170 TermDef::RunProof {
171 stepper,
172 ret_type,
173 nr_args,
174 commands,
175 },
176 TermDefAction::Proof(x),
177 )
178 }
179 None => (
180 TermDef::ProofDone {
181 stream: stepper.take_stream(),
182 ret_type,
183 commands,
184 nr_args,
185 },
186 TermDefAction::ProofDone,
187 ),
188 },
189 TermDef::ProofDone {
190 stream,
191 ret_type,
192 commands,
193 nr_args,
194 } => {
195 if context.proof_stack.len() != 1 {
196 return Err(Kind::StackHasMoreThanOne);
197 }
198
199 let expr = context
200 .proof_stack
201 .pop()
202 .ok_or(Kind::Impossible)?
203 .as_expr()
204 .ok_or(Kind::InvalidStoreExpr)?;
205
206 let ty = context
207 .store
208 .get_type_of_expr(expr)
209 .ok_or(Kind::InvalidStoreType)?;
210
211 if !ty.is_compatible_to(&ret_type) {
212 return Err(Kind::TypeError);
213 }
214
215 if ty.dependencies() != ret_type.dependencies() {
216 return Err(Kind::UnaccountedDependencies);
217 }
218
219 let subslice = context
220 .proof_heap
221 .as_slice()
222 .get(..nr_args)
223 .ok_or(Kind::InvalidHeapIndex)?;
224
225 context.unify_heap.clone_from(subslice);
226
227 let stepper = stream::unify::Stepper::new(stream::unify::Mode::Def, expr, commands);
228
229 (
230 TermDef::RunUnify { stream, stepper },
231 TermDefAction::StartUnify,
232 )
233 }
234 TermDef::RunUnify {
235 stream,
236 mut stepper,
237 } => match stepper.step(context, table)? {
238 Some(x) => (
239 TermDef::RunUnify { stream, stepper },
240 TermDefAction::Unify(x),
241 ),
242 None => (TermDef::Done { stream }, TermDefAction::Done),
243 },
244 TermDef::Done { stream } => (TermDef::Done { stream }, TermDefAction::Done),
245 TermDef::Dummy => (TermDef::Dummy, TermDefAction::Done),
246 };
247
248 *self = next_state;
249
250 Ok(ret_val)
251 }
252}
253
254#[derive(Debug)]
255pub enum AxiomThm<S> {
256 Start {
257 idx: u32,
258 is_axiom: bool,
259 stream: S,
260 },
261 RunProof {
262 stepper: stream::proof::Stepper<S>,
263 is_axiom: bool,
264 commands: Range<usize>,
265 nr_args: usize,
266 },
267 ProofDone {
268 stream: S,
269 is_axiom: bool,
270 commands: Range<usize>,
271 nr_args: usize,
272 },
273 RunUnify {
274 stream: S,
275 stepper: stream::unify::Stepper,
276 },
277 Done {
278 stream: S,
279 },
280 Dummy,
281}
282
283#[derive(Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
284pub enum AxiomThmAction {
285 StartProof,
286 Proof(stream::proof::Action),
287 ProofDone,
288 StartUnify,
289 Unify(stream::unify::Action),
290 Done,
291}
292
293impl<S> AxiomThm<S>
294where
295 S: Iterator<Item = opcode::Command<opcode::Proof>>,
296{
297 pub fn new(idx: u32, stream: S, is_axiom: bool) -> AxiomThm<S> {
298 AxiomThm::Start {
299 idx,
300 stream,
301 is_axiom,
302 }
303 }
304
305 pub fn take_stream_if_done(self) -> Option<S> {
306 match self {
307 AxiomThm::Done { stream } => Some(stream),
308 _ => None,
309 }
310 }
311
312 pub fn is_done(&self) -> bool {
313 matches!(self, AxiomThm::Done { .. })
314 }
315
316 pub fn step<SS: Store, T: Table<Var = SS::Var>>(
317 &mut self,
318 context: &mut Context<SS>,
319 state: &State,
320 table: &T,
321 ) -> KResult<AxiomThmAction> {
322 let old = core::mem::replace(self, Self::Dummy);
323
324 let (next_state, ret_val) = match old {
325 AxiomThm::Start {
326 idx,
327 stream,
328 is_axiom,
329 } => {
330 let thm = table.theorem(idx).ok_or(Kind::InvalidTheorem)?;
331
332 context.store.clear();
333 context.proof_stack.clear();
334 context.proof_heap.clear();
335 context.unify_stack.clear();
336 context.unify_heap.clear();
337 context.hyp_stack.clear();
338
339 let binders = thm.binders();
340 let nr_args = binders.len();
341 let binders = table.binders(binders).ok_or(Kind::InvalidBinderIndices)?;
342
343 context.allocate_binders(table, state.current_sort(), binders)?;
344
345 let stepper = stream::proof::Stepper::new(false, *state, stream);
346
347 let commands = thm.unify_commands();
348
349 (
350 AxiomThm::RunProof {
351 stepper,
352 commands,
353 is_axiom,
354 nr_args,
355 },
356 AxiomThmAction::StartProof,
357 )
358 }
359 AxiomThm::RunProof {
360 mut stepper,
361 commands,
362 is_axiom,
363 nr_args,
364 } => match stepper.step(context, table)? {
365 Some(x) => {
366 (
368 AxiomThm::RunProof {
369 stepper,
370 commands,
371 is_axiom,
372 nr_args,
373 },
374 AxiomThmAction::Proof(x),
375 )
376 }
377 None => (
378 AxiomThm::ProofDone {
379 stream: stepper.take_stream(),
380 commands,
381 is_axiom,
382 nr_args,
383 },
384 AxiomThmAction::ProofDone,
385 ),
386 },
387 AxiomThm::ProofDone {
388 stream,
389 commands,
390 is_axiom,
391 nr_args,
392 } => {
393 if context.proof_stack.len() != 1 {
394 return Err(Kind::StackHasMoreThanOne);
395 }
396
397 let expr = context.proof_stack.pop().ok_or(Kind::Impossible)?;
398
399 let expr = if is_axiom {
400 expr.as_expr()
401 } else {
402 expr.as_proof()
403 };
404
405 let expr = expr.ok_or(Kind::InvalidStackType)?;
406
407 let sort = context
408 .store
409 .get_type_of_expr(expr)
410 .ok_or(Kind::InvalidStoreExpr)?
411 .sort_idx();
412
413 let sort = table.sort(sort).ok_or(Kind::InvalidSort)?;
414
415 if !sort.is_provable() {
416 return Err(Kind::SortNotProvable);
417 }
418
419 let subslice = context
420 .proof_heap
421 .as_slice()
422 .get(..nr_args)
423 .ok_or(Kind::InvalidHeapIndex)?;
424
425 context.unify_heap.clone_from(subslice);
426
427 let stepper =
428 stream::unify::Stepper::new(stream::unify::Mode::ThmEnd, expr, commands);
429
430 (
431 AxiomThm::RunUnify { stream, stepper },
432 AxiomThmAction::StartUnify,
433 )
434 }
435 AxiomThm::RunUnify {
436 stream,
437 mut stepper,
438 } => match stepper.step(context, table)? {
439 Some(x) => (
440 AxiomThm::RunUnify { stream, stepper },
441 AxiomThmAction::Unify(x),
442 ),
443 None => (AxiomThm::Done { stream }, AxiomThmAction::Done),
444 },
445 AxiomThm::Done { stream } => (AxiomThm::Done { stream }, AxiomThmAction::Done),
446 AxiomThm::Dummy => (AxiomThm::Dummy, AxiomThmAction::Done),
447 };
448
449 *self = next_state;
450
451 Ok(ret_val)
452 }
453}
454
455#[derive(Debug)]
456enum StepState<S, Ty> {
457 Normal,
458 TermDef(TermDef<S, Ty>),
459 AxiomThm(AxiomThm<S>),
460}
461
462#[derive(Debug)]
463pub struct Stepper<S, Ty>
464where
465 S: StatementStream + Iterator,
466 <S as Iterator>::Item: TryInto<Opcode>,
467{
468 stream: S,
469 state: StepState<S::ProofStream, Ty>,
470}
471
472#[derive(Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
473pub enum Action {
474 AxiomStart(u32),
475 ThmStart(u32),
476 AxiomThmDone,
477 TermDefStart(u32),
478 TermDef(TermDefAction),
479 TermDefDone,
480 AxiomThm(AxiomThmAction),
481 Sort,
482}
483
484impl<S, Ty> Stepper<S, Ty>
485where
486 S: StatementStream + Iterator,
487 <S as Iterator>::Item: TryInto<Opcode>,
488 Ty: Var,
489{
490 pub fn new(stream: S) -> Stepper<S, Ty> {
491 Stepper {
492 stream,
493 state: StepState::Normal,
494 }
495 }
496
497 pub fn is_state_normal(&self) -> bool {
498 matches!(self.state, StepState::Normal)
499 }
500
501 pub fn get_stream(&self) -> &S {
502 &self.stream
503 }
504
505 pub fn get_stream_mut(&mut self) -> &mut S {
506 &mut self.stream
507 }
508
509 pub fn step<SS: Store<Var = Ty>, T: Table<Var = SS::Var>>(
510 &mut self,
511 context: &mut Context<SS>,
512 state: &mut State,
513 table: &T,
514 ) -> KResult<Option<Action>> {
515 let old = core::mem::replace(&mut self.state, StepState::Normal);
516
517 let (next_state, ret) = match old {
518 StepState::Normal => return self.normal(state),
519 StepState::TermDef(mut td) => {
520 if td.is_done() {
521 if let Some(stream) = td.take_stream_if_done() {
522 self.stream.put_proof_stream(stream);
523 } else {
524 unreachable!("impossible");
525 }
526
527 state.increment_current_term();
528 (StepState::Normal, Ok(Some(Action::TermDefDone)))
529 } else {
530 let ret = td.step(context, state, table)?;
531 (StepState::TermDef(td), Ok(Some(Action::TermDef(ret))))
532 }
533 }
534 StepState::AxiomThm(mut at) => {
535 if at.is_done() {
536 if let Some(stream) = at.take_stream_if_done() {
537 self.stream.put_proof_stream(stream);
538 } else {
539 unreachable!("impossible");
540 }
541
542 state.increment_current_theorem();
543
544 (StepState::Normal, Ok(Some(Action::AxiomThmDone)))
545 } else {
546 let ret = at.step(context, state, table)?;
547 (StepState::AxiomThm(at), Ok(Some(Action::AxiomThm(ret))))
548 }
549 }
550 };
551
552 self.state = next_state;
553
554 ret
555 }
556
557 fn normal(&mut self, state: &mut State) -> KResult<Option<Action>> {
558 if let Some(x) = self.stream.next() {
559 let x = x.try_into().map_err(|_| Kind::UnknownCommand)?;
560
561 match x {
562 Opcode::End => {
563 Ok(None)
564 }
566 Opcode::Sort => {
567 state.increment_current_sort();
568 Ok(Some(Action::Sort))
569 }
570 Opcode::TermDef => {
571 let ps = self
572 .stream
573 .take_proof_stream()
574 .ok_or(Kind::MissingProofStream)?;
575 let idx = state.current_term();
576 let td = TermDef::new(idx, ps);
577
578 self.state = StepState::TermDef(td);
579 Ok(Some(Action::TermDefStart(idx)))
580 }
581 Opcode::Axiom => {
582 let ps = self
583 .stream
584 .take_proof_stream()
585 .ok_or(Kind::MissingProofStream)?;
586 let idx = state.current_theorem();
587 let at = AxiomThm::new(idx, ps, true);
588 self.state = StepState::AxiomThm(at);
589 Ok(Some(Action::AxiomStart(idx)))
590 }
591 Opcode::Thm => {
592 let ps = self
593 .stream
594 .take_proof_stream()
595 .ok_or(Kind::MissingProofStream)?;
596 let idx = state.current_theorem();
597 let at = AxiomThm::new(idx, ps, false);
598 self.state = StepState::AxiomThm(at);
599 Ok(Some(Action::ThmStart(idx)))
600 }
601 }
602 } else {
603 Ok(None)
604 }
605 }
606}