ftml_solver/
paragraphs.rs

1use crate::{
2    Checker,
3    facts::GlobalOrLocal,
4    hoas::HOASSymbols,
5    impls::solving::{Solutions, TermExtSolvable},
6    rules::ProofBarrier,
7    split::SplitStrategy,
8};
9use ftml_ontology::{
10    narrative::elements::{LogicalParagraph, paragraphs::ParagraphStep},
11    terms::{BindingTerm, BoundArgument, ComponentVar, MaybeSequence, Term, Variable},
12    utils::SourceRange,
13};
14use ftml_solver_trace::{
15    CheckLog, CheckingTask, PreCheckLog,
16    results::{
17        CheckResult, ContentCheckResult, ProofStepCheckResult, ProofStepResult, SymbolCheckResult,
18        TypeCheckResult,
19    },
20};
21use ftml_uris::{DocumentElementUri, Id, SymbolUri};
22
23impl<Split: SplitStrategy> Checker<Split> {
24    pub fn check_assertion(&mut self, p: &LogicalParagraph) -> Option<Vec<CheckResult>> {
25        let hoas = self.hoas()?;
26        let mut ret = Vec::new();
27        for (target, term) in &p.fors {
28            let Ok(target) = self.get_symbol(target, |t| t) else {
29                continue;
30            };
31            let Some(term) = term else { continue };
32            let Some(term) = term.get_parsed() else {
33                continue;
34            };
35            let params = p
36                .binds_variables
37                .iter()
38                .filter_map(|uri| {
39                    self.get_variable(uri).ok().map(|v| ComponentVar {
40                        var: Variable::Ref {
41                            declaration: uri.clone(),
42                            is_sequence: Some(v.data.is_seq),
43                        },
44                        tp: v.data.tp.checked_or_parsed().map(|(t, _)| t),
45                        df: v.data.df.checked_or_parsed().map(|(t, _)| t),
46                    })
47                })
48                .collect::<Vec<_>>();
49
50            let wrapped = hoas.wrap_types(&p.premises, term);
51            let wrapped = if params.is_empty() {
52                wrapped.into_owned()
53            } else {
54                Term::Bound(BindingTerm::new(
55                    hoas.pi.clone().into(),
56                    Box::new([
57                        BoundArgument::BoundSeq(MaybeSequence::Seq(params.into_boxed_slice())),
58                        BoundArgument::Simple(wrapped.into_owned()),
59                    ]),
60                    None,
61                ))
62            };
63            let (unks, tp) = self.prepare(None, wrapped);
64
65            tracing::trace!("Checking assertion for {}", target.uri);
66            let (b, unks, mut l) = self.check_inhabitable(Some(unks), &tp);
67            let mut tp = self.wrap_none(Some(unks), |slf| slf.subst(tp)).1;
68
69            if tp.has_solvable() {
70                l.push(PreCheckLog::Msg(
71                    vec!["Unsolved unkowns remain".into()],
72                    ftml_solver_trace::MessageLevel::Failure,
73                ));
74                ret.push(CheckResult::Content(ContentCheckResult::Symbol(
75                    target.uri.clone(),
76                    SymbolCheckResult::TypeOnly {
77                        result: TypeCheckResult {
78                            success: false,
79                            log: CheckLog::from_pre(l, &mut |t| self.revert_prepare(t)),
80                        },
81                    },
82                )));
83                continue;
84            }
85            if let Some(t) = self.bind_implicits(&tp) {
86                tp = t;
87            }
88
89            target
90                .data
91                .tp
92                .set_presentation(self.revert_prepare(tp.clone()));
93            target.data.tp.set_checked(tp);
94            ret.push(CheckResult::Content(ContentCheckResult::Symbol(
95                target.uri.clone(),
96                SymbolCheckResult::TypeOnly {
97                    result: TypeCheckResult {
98                        success: b.unwrap_or(false),
99                        log: CheckLog::from_pre(l, &mut |t| self.revert_prepare(t)),
100                    },
101                },
102            )));
103        }
104        Some(ret)
105    }
106
107    pub fn check_definition(&mut self, p: &LogicalParagraph) -> Vec<CheckResult> {
108        let Some(hoas) = self.hoas() else {
109            return Vec::new();
110        };
111        let mut ret = Vec::new();
112        for (target, term) in &p.fors {
113            let Ok(target) = self.get_symbol(target, |t| t) else {
114                continue;
115            };
116            let Some(term) = term else { continue };
117            let Some(term) = term.get_parsed() else {
118                continue;
119            };
120            let params = p
121                .binds_variables
122                .iter()
123                .filter_map(|uri| {
124                    self.get_variable(uri).ok().map(|v| ComponentVar {
125                        var: Variable::Ref {
126                            declaration: uri.clone(),
127                            is_sequence: Some(v.data.is_seq),
128                        },
129                        tp: v.data.tp.checked_or_parsed().map(|(t, _)| t),
130                        df: v.data.df.checked_or_parsed().map(|(t, _)| t),
131                    })
132                })
133                .collect::<Vec<_>>();
134
135            let df = if params.is_empty() {
136                term.clone()
137            } else {
138                Term::Bound(BindingTerm::new(
139                    hoas.lambda.clone().into(),
140                    Box::new([
141                        BoundArgument::BoundSeq(MaybeSequence::Seq(params.into_boxed_slice())),
142                        BoundArgument::Simple(term.clone()),
143                    ]),
144                    None,
145                ))
146            };
147
148            tracing::trace!("Checking definiens for {}", target.uri);
149            if let Some(tp) = target.data.tp.get_parsed() {
150                ret.push(CheckResult::Content(ContentCheckResult::Symbol(
151                    target.uri.clone(),
152                    self.df_and_tp(&df, &target.data.df, tp, &target.data.tp, true, true),
153                )));
154            } else {
155                ret.push(CheckResult::Content(ContentCheckResult::Symbol(
156                    target.uri.clone(),
157                    self.df_only(&df, &target.data.df, &target.data.tp, true, true),
158                )));
159            }
160        }
161        ret
162    }
163
164    pub fn check_proof(&mut self, p: &LogicalParagraph) -> Option<CheckResult> {
165        //println!("Here: {:?}", &p.children);
166        let mut ret = Vec::new();
167        let mut ctx = Vec::new();
168        let _ = self.hoas()?;
169        let mut state = ProofCheckState {
170            context: &mut ctx,
171            counter: 0,
172            conclusion_df: None,
173            conclusion_type: None,
174        };
175        let for_symbol = p
176            .fors
177            .first()
178            .and_then(|sym| self.get_symbol(&sym.0, |t| self.prepare(None, t).1).ok());
179        let block = for_symbol.as_ref().map(|sym| &sym.uri);
180        for s in &p.steps {
181            if let Some(res) = self.proof_step(s, &mut state, block) {
182                let success = res.success();
183                ret.push(res);
184                if !success {
185                    return Some(CheckResult::Proof(p.uri.clone(), ret));
186                }
187            }
188        }
189        if matches!(p.steps.last(), Some(ParagraphStep::ProofConclusion { .. })) {
190            state.context.pop();
191        }
192        let (tp, df) = state.make_conclusion(self.hoas()?, 0);
193        if (tp.is_some() || df.is_some())
194            && let Some(sym) = for_symbol.as_ref()
195        {
196            let orig_tp = &sym.data.tp;
197            let orig_df = &sym.data.df;
198            if let Some(tp) = tp {
199                if let Some((orig, _)) = orig_tp.checked_or_parsed() {
200                    let tp = self.bind_implicits(&tp).unwrap_or(tp.clone());
201                    let (b, _, l) = self.check_subtype(None, &tp, &orig);
202                    ret.push(ProofStepResult::Conclusion {
203                        var: None,
204                        result: ProofStepCheckResult::GoalOnly {
205                            result: TypeCheckResult {
206                                success: b.unwrap_or_default(),
207                                log: CheckLog::from_pre(l, &mut |t| self.revert_prepare(t)),
208                            },
209                        },
210                    });
211                } else {
212                    orig_tp.set_checked(tp.clone());
213                    orig_tp.set_presentation(self.revert_prepare(tp.clone()));
214                }
215                if let Some(df) = df
216                    && orig_df.is_none()
217                {
218                    let df = ProofBarrier::apply(df, tp);
219                    let df = self.bind_implicits(&df).unwrap_or(df);
220                    orig_df.set_checked(df.clone());
221                    orig_df.set_presentation(self.revert_prepare(df));
222                }
223            }
224        } else if for_symbol.is_some() {
225            return Some(CheckResult::Proof(
226                p.uri.clone(),
227                vec![ProofStepResult::Conclusion {
228                    var: None,
229                    result: ProofStepCheckResult::ProofOnly {
230                        inferred: None,
231                        log: CheckLog::Fail(vec![
232                            "does not establish the theorem.".to_string().into(),
233                        ]),
234                    },
235                }],
236            ));
237        }
238        Some(CheckResult::Proof(p.uri.clone(), ret))
239    }
240
241    fn proof_step(
242        &mut self,
243        s: &ParagraphStep,
244        context: &mut ProofCheckState,
245        block: Option<&SymbolUri>,
246    ) -> Option<ProofStepResult> {
247        match s {
248            ParagraphStep::EquationStep => None,
249            ParagraphStep::ProofAssumption {
250                var_name,
251                method,
252                justification,
253                arguments,
254                yields,
255            } => self
256                .step_data(
257                    context,
258                    var_name.as_ref(),
259                    method.as_ref().map(|(t, _)| t),
260                    justification.as_ref().map(|(t, _)| t),
261                    arguments,
262                    yields.as_ref().map(|(t, _)| t),
263                    true,
264                    block,
265                )
266                .map(|r| ProofStepResult::Assumption {
267                    var: var_name.clone(),
268                    result: r,
269                }),
270            ParagraphStep::ProofConclusion {
271                var_name,
272                method,
273                justification,
274                arguments,
275                yields,
276            } => self
277                .conclusion_step(
278                    context,
279                    var_name.as_ref(),
280                    method.as_ref().map(|(t, _)| t),
281                    justification.as_ref().map(|(t, _)| t),
282                    arguments,
283                    yields.as_ref().map(|(t, _)| t),
284                    block,
285                )
286                .map(|r| ProofStepResult::Conclusion {
287                    var: var_name.clone(),
288                    result: r,
289                }),
290            ParagraphStep::ProofStep {
291                var_name,
292                method,
293                justification,
294                arguments,
295                yields,
296            } => self
297                .step_data(
298                    context,
299                    var_name.as_ref(),
300                    method.as_ref().map(|(t, _)| t),
301                    justification.as_ref().map(|(t, _)| t),
302                    arguments,
303                    yields.as_ref().map(|(t, _)| t),
304                    false,
305                    block,
306                )
307                .map(|r| ProofStepResult::Step {
308                    var: var_name.clone(),
309                    result: r,
310                }),
311            ParagraphStep::Subproof {
312                uri,
313                var_name,
314                steps,
315                .. /*
316                method,
317                justification,
318                arguments,
319                yields,
320                */
321            } => {
322                let curr = context.context.len();
323                let mut results = Vec::with_capacity(steps.len());
324                for s in steps {
325                    if let Some(r) = self.proof_step(s, context, block) {
326                        let success = r.success();
327                        results.push(r);
328                        if !success {
329                            return Some(ProofStepResult::Subproof {
330                                uri: uri.clone(),
331                                var: var_name.clone(),
332                                results,
333                            })
334                        }
335                    }
336                }
337
338                if matches!(steps.last(), Some(ParagraphStep::ProofConclusion { .. })) {
339                    context.context.pop();
340                }
341                let (tp, df) = context.make_conclusion(self.hoas().expect("checked earlier"),curr);
342                let var = var_name.as_ref().map_or_else(
343                    || Variable::Name {
344                        name: context.dummy(),
345                        notated: None,
346                    },
347                    |uri| Variable::Ref {
348                        declaration: uri.clone(),
349                        is_sequence: None,
350                    },
351                );
352                if let Some(v) = var_name.as_ref().and_then(|vn| self.get_variable(vn).ok()) {
353                    if let Some(tp) = &tp {
354                        v.data.tp.set_checked(tp.clone());
355                        let pres = self.revert_prepare(tp.clone());
356                        v.data.tp.set_presentation(pres);
357                    }
358                    if let Some(df) = &df {
359                        v.data.df.set_checked(df.clone());
360                        let pres = self.revert_prepare(df.clone());
361                        v.data.df.set_presentation(pres);
362                    }
363                }
364                context.context.push((ComponentVar { var, tp, df }, false));
365                // TODO something reasonable
366                //r
367                Some(ProofStepResult::Subproof {
368                    uri: uri.clone(),
369                    var: var_name.clone(),
370                    results,
371                })
372            }
373        }
374    }
375
376    fn step_data_i(
377        &self,
378        context: &mut ProofCheckState,
379        hoas: &HOASSymbols,
380        var_name: Option<&DocumentElementUri>,
381        method: Option<&Term>,
382        justification: Option<&Term>,
383        arguments: &[Option<(Term, SourceRange)>],
384        yields: Option<&Term>,
385        needs_def: bool,
386        block: Option<&SymbolUri>,
387    ) -> (Option<ProofStepCheckResult>, Option<Term>, Option<Term>) {
388        let mut tp = None;
389        let mut df = None;
390        let mut proof_log = None;
391        let var = var_name.and_then(|vn| self.get_variable(vn).ok());
392        if let Some(tm) = yields {
393            let (unks, tm) = self.prepare(None, tm.clone());
394            let (b, nunks, l) = context.check_inhabitable(self, unks.clone(), &tm, block);
395            if Some(true) == b {
396                proof_log = Some(ProofStepCheckResult::GoalOnly {
397                    result: TypeCheckResult {
398                        success: b.unwrap_or_default(),
399                        log: CheckLog::from_pre(l, &mut |t| self.revert_prepare(t)),
400                    },
401                });
402                tp = Some(self.wrap_none(Some(nunks), |slf| slf.subst(tm)).1);
403            } else {
404                let tm = hoas.wrap_judg(&tm);
405                let (b, unks, l2) = context.check_inhabitable(self, unks, &tm, block);
406                proof_log = Some(ProofStepCheckResult::GoalOnly {
407                    result: TypeCheckResult {
408                        success: b.unwrap_or_default(),
409                        log: if Some(true) == b {
410                            CheckLog::from_pre(l2, &mut |t| self.revert_prepare(t))
411                        } else {
412                            CheckLog::Strategy {
413                                name: "Checking provability".to_string(),
414                                steps: vec![
415                                    CheckLog::from_pre(l, &mut |t| self.revert_prepare(t)),
416                                    CheckLog::from_pre(l2, &mut |t| self.revert_prepare(t)),
417                                ],
418                                success: false,
419                            }
420                        },
421                    },
422                });
423                tp = Some(
424                    self.wrap_none(Some(unks), |slf| slf.subst(tm.into_owned()))
425                        .1,
426                );
427            }
428        }
429        if let Some(tm) = justification {
430            let (unks, tm) = self.prepare(None, tm.clone());
431            if let Some(tp) = tp.as_ref() {
432                let Some(ProofStepCheckResult::GoalOnly { result }) = proof_log.take() else {
433                    panic!("bug");
434                };
435                let (b, unks, l) = context.check_type(self, unks, &tm, tp, block);
436                df = Some(self.wrap_none(Some(unks), |slf| slf.subst(tm)).1);
437                proof_log = Some(ProofStepCheckResult::Both {
438                    inhabitable: result,
439                    matches: Some(TypeCheckResult {
440                        success: b.unwrap_or_default(),
441                        log: CheckLog::from_pre(l, &mut |t| self.revert_prepare(t)),
442                    }),
443                });
444            } else {
445                let (r, mut unks, l) = context.infer(self, unks, &tm, block);
446                let infed = r.clone().map(|t| self.revert_prepare(t));
447                proof_log = Some(ProofStepCheckResult::ProofOnly {
448                    inferred: infed,
449                    log: CheckLog::from_pre(l, &mut |t| self.revert_prepare(t)),
450                });
451                tp = r.map(|t| {
452                    let (unks2, t) =
453                        self.wrap_none(Some(std::mem::take(&mut unks)), |slf| slf.subst(t));
454                    unks = unks2;
455                    t
456                });
457                let d = self.wrap_none(Some(unks), |slf| slf.subst(tm)).1;
458                if let Some(tp) = tp.as_ref() {
459                    df = Some(ProofBarrier::apply(d, tp.clone()));
460                } else {
461                    df = Some(d);
462                }
463            }
464        }
465        if df.is_none() {
466            if let Some(tm) = method {
467                let (tm, unks) = hoas.apply(
468                    self,
469                    tm,
470                    arguments.iter().map(|o| o.as_ref().map(|(t, _)| t.clone())),
471                );
472                let (unks, tm) = self.prepare(Some(unks), tm.into_owned());
473                if let Some(tp) = &tp {
474                    let Some(ProofStepCheckResult::GoalOnly { result }) = proof_log.take() else {
475                        panic!("bug");
476                    };
477                    let (b, unks, l) = context.check_type(self, unks, &tm, tp, block);
478                    let d = self.wrap_none(Some(unks), |slf| slf.subst(tm)).1;
479                    df = Some(ProofBarrier::apply(d, tp.clone()));
480
481                    proof_log = Some(ProofStepCheckResult::Both {
482                        inhabitable: result,
483                        matches: Some(TypeCheckResult {
484                            success: b.unwrap_or_default(),
485                            log: CheckLog::from_pre(l, &mut |t| self.revert_prepare(t)),
486                        }),
487                    });
488                } else {
489                    let (r, mut unks, l) = context.infer(self, unks, &tm, block);
490                    let infed = r.clone().map(|t| self.revert_prepare(t));
491                    proof_log = Some(ProofStepCheckResult::ProofOnly {
492                        inferred: infed,
493                        log: CheckLog::from_pre(l, &mut |t| self.revert_prepare(t)),
494                    });
495                    tp = r.map(|t| {
496                        let (unks2, t) =
497                            self.wrap_none(Some(std::mem::take(&mut unks)), |slf| slf.subst(t));
498                        unks = unks2;
499                        t
500                    });
501
502                    let d = self.wrap_none(Some(unks), |slf| slf.subst(tm)).1;
503                    if let Some(tp) = tp.as_ref() {
504                        df = Some(ProofBarrier::apply(d, tp.clone()));
505                    } else {
506                        df = Some(d);
507                    }
508                }
509            } else if needs_def && let Some(tp) = tp.as_ref() {
510                let Some(ProofStepCheckResult::GoalOnly { result }) = proof_log.take() else {
511                    panic!("bug");
512                };
513                let (r, unks, l) = context.prove(self, Solutions::default(), tp, block);
514                df = r.map(|t| {
515                    ProofBarrier::apply(
516                        self.wrap_none(Some(unks), |slf| slf.subst(t)).1,
517                        tp.clone(),
518                    )
519                });
520                proof_log = Some(ProofStepCheckResult::Both {
521                    inhabitable: result,
522                    matches: Some(TypeCheckResult {
523                        success: df.is_some(),
524                        log: CheckLog::from_pre(l, &mut |t| self.revert_prepare(t)),
525                    }),
526                });
527            }
528        }
529
530        if let Some(v) = var {
531            if let Some(tp) = &tp {
532                v.data.tp.set_checked(tp.clone());
533                let pres = self.revert_prepare(tp.clone());
534                v.data.tp.set_presentation(pres);
535            }
536            if let Some(df) = &df {
537                v.data.df.set_checked(df.clone());
538                let pres = self.revert_prepare(df.clone());
539                v.data.df.set_presentation(pres);
540            }
541        }
542        if needs_def
543            && df.is_none()
544            && let Some(ProofStepCheckResult::GoalOnly { result }) = proof_log.as_mut()
545        {
546            result.success = false;
547            result.log.add_failure("Unproven goal");
548        }
549        (proof_log, tp, df)
550    }
551
552    fn step_data(
553        &mut self,
554        context: &mut ProofCheckState,
555        var_name: Option<&DocumentElementUri>,
556        method: Option<&Term>,
557        justification: Option<&Term>,
558        arguments: &[Option<(Term, SourceRange)>],
559        yields: Option<&Term>,
560        is_assumption: bool,
561        block: Option<&SymbolUri>,
562    ) -> Option<ProofStepCheckResult> {
563        /*
564        if let Some(vn) = var_name
565            && vn.name().as_ref().ends_with("proof/5.")
566        {
567            println!("HERE: {vn}");
568            crate::DEBUG.store(true, std::sync::atomic::Ordering::Relaxed);
569            print!("{esc}[2J{esc}[1;1H", esc = 27 as char);
570            println!("Debug mode on.");
571            crate::pause();
572        } */
573
574        let (r, tp, df) = self.step_data_i(
575            context,
576            self.hoas()?,
577            var_name,
578            method,
579            justification,
580            arguments,
581            yields,
582            !is_assumption,
583            block,
584        );
585        let var = var_name.map_or_else(
586            || Variable::Name {
587                name: context.dummy(),
588                notated: None,
589            },
590            |uri| Variable::Ref {
591                declaration: uri.clone(),
592                is_sequence: None,
593            },
594        );
595        let cv = ComponentVar { var, tp, df };
596        context.context.push((cv, is_assumption));
597        r
598    }
599
600    fn conclusion_step(
601        &self,
602        context: &mut ProofCheckState,
603        var_name: Option<&DocumentElementUri>,
604        method: Option<&Term>,
605        justification: Option<&Term>,
606        arguments: &[Option<(Term, SourceRange)>],
607        yields: Option<&Term>,
608        block: Option<&SymbolUri>,
609    ) -> Option<ProofStepCheckResult> {
610        let (r, tp, df) = self.step_data_i(
611            context,
612            self.hoas()?,
613            var_name,
614            method,
615            justification,
616            arguments,
617            yields,
618            true,
619            block,
620        );
621        let var = var_name.map_or_else(
622            || Variable::Name {
623                name: context.dummy(),
624                notated: None,
625            },
626            |uri| Variable::Ref {
627                declaration: uri.clone(),
628                is_sequence: None,
629            },
630        );
631        context.conclusion_type.clone_from(&tp);
632        context.conclusion_df.clone_from(&df);
633        let cv = ComponentVar { var, tp, df };
634        context.context.push((cv, false));
635        r
636    }
637}
638
639#[derive(Debug)]
640struct ProofCheckState<'c> {
641    context: &'c mut Vec<(ComponentVar, bool)>,
642    counter: usize,
643    conclusion_type: Option<Term>,
644    conclusion_df: Option<Term>,
645}
646
647impl ProofCheckState<'_> {
648    fn dummy(&mut self) -> Id {
649        // SAFETY: valid ID
650        let r = unsafe {
651            format!("DUMMY_{}", self.counter + 1)
652                .parse()
653                .unwrap_unchecked()
654        };
655        self.counter += 1;
656        r
657    }
658    fn make_conclusion(&mut self, hoas: &HOASSymbols, off: usize) -> (Option<Term>, Option<Term>) {
659        self.context.drain(off..).rev().fold(
660            (self.conclusion_type.take(), self.conclusion_df.take()),
661            |(tp, df), (v, is_ass)| match (tp, df) {
662                (Some(tp), None) if is_ass => (Some(hoas.pi(v, tp)), None),
663                (None, Some(df)) if is_ass => (None, Some(hoas.lambda(v, df))),
664                (Some(tp), Some(df)) if is_ass => {
665                    (Some(hoas.pi(v.clone(), tp)), Some(hoas.lambda(v, df)))
666                }
667                (Some(tp), None) => (
668                    (Some(if tp.has_free_such_that(|v2| v2.name() == v.var.name()) {
669                        if let Some(df) = v.df {
670                            tp / (v.var.name(), &df)
671                        } else {
672                            HOASSymbols::let_in(v, tp)
673                        }
674                    } else {
675                        tp
676                    })),
677                    None,
678                ),
679                (None, Some(df)) => (
680                    None,
681                    Some(if let Some(d) = v.df {
682                        df / (v.var.name(), &d)
683                    } else {
684                        HOASSymbols::let_in(v, df)
685                    }),
686                ),
687                (Some(tp), Some(df)) => (
688                    (Some(if tp.has_free_such_that(|v2| v2.name() == v.var.name()) {
689                        if let Some(df) = &v.df {
690                            tp / (v.var.name(), df)
691                        } else {
692                            HOASSymbols::let_in(v.clone(), tp)
693                        }
694                    } else {
695                        tp
696                    })),
697                    Some(if let Some(d) = v.df {
698                        df / (v.var.name(), &d)
699                    } else {
700                        HOASSymbols::let_in(v, df)
701                    }),
702                ),
703                (None, None) => (None, None),
704            },
705        )
706    }
707
708    fn forget(&mut self, off: usize) {
709        self.context.truncate(off);
710    }
711
712    fn check_inhabitable<Split: SplitStrategy>(
713        &self,
714        checker: &Checker<Split>,
715        unks: Solutions,
716        t: &Term,
717        block: Option<&SymbolUri>,
718    ) -> (Option<bool>, Solutions, PreCheckLog) {
719        checker.wrap_task(CheckingTask::Inhabitable(t), Some(unks), |mut slf| {
720            for (c, _) in &*self.context {
721                slf.extend_context(c);
722            }
723            if let Some(blocked) = block {
724                slf.context
725                    .block_fact(GlobalOrLocal::Global(blocked.clone()));
726            }
727            slf.check_inhabitable_i(t)
728        })
729    }
730    fn check_type<Split: SplitStrategy>(
731        &self,
732        checker: &Checker<Split>,
733        unks: Solutions,
734        tm: &Term,
735        tp: &Term,
736        block: Option<&SymbolUri>,
737    ) -> (Option<bool>, Solutions, PreCheckLog) {
738        checker.wrap_task(CheckingTask::HasType(tm, tp), Some(unks), |mut slf| {
739            for (c, _) in &*self.context {
740                slf.extend_context(c);
741            }
742            if let Some(blocked) = block {
743                slf.context
744                    .block_fact(GlobalOrLocal::Global(blocked.clone()));
745            }
746            slf.check_type_i(tm, tp)
747        })
748    }
749    fn check_equal<Split: SplitStrategy>(
750        &self,
751        checker: &Checker<Split>,
752        unks: Solutions,
753        lhs: &Term,
754        rhs: &Term,
755        block: Option<&SymbolUri>,
756    ) -> (Option<bool>, Solutions, PreCheckLog) {
757        checker.wrap_task(CheckingTask::Equality(lhs, rhs), Some(unks), |mut slf| {
758            for (c, _) in &*self.context {
759                slf.extend_context(c);
760            }
761            if let Some(blocked) = block {
762                slf.context
763                    .block_fact(GlobalOrLocal::Global(blocked.clone()));
764            }
765            slf.check_equality_i(lhs, rhs)
766        })
767    }
768    fn infer<Split: SplitStrategy>(
769        &self,
770        checker: &Checker<Split>,
771        unks: Solutions,
772        t: &Term,
773        block: Option<&SymbolUri>,
774    ) -> (Option<Term>, Solutions, PreCheckLog) {
775        checker.wrap_task(CheckingTask::Inference(t), Some(unks), |mut slf| {
776            for (c, _) in &*self.context {
777                slf.extend_context(c);
778            }
779            if let Some(blocked) = block {
780                slf.context
781                    .block_fact(GlobalOrLocal::Global(blocked.clone()));
782            }
783            slf.infer_type_i(t)
784        })
785    }
786    fn prove<Split: SplitStrategy>(
787        &self,
788        checker: &Checker<Split>,
789        unks: Solutions,
790        t: &Term,
791        block: Option<&SymbolUri>,
792    ) -> (Option<Term>, Solutions, PreCheckLog) {
793        checker.wrap_task(CheckingTask::Proving(t), Some(unks), |mut slf| {
794            for (c, _) in &*self.context {
795                slf.extend_context(c);
796            }
797            if let Some(blocked) = block {
798                slf.context
799                    .block_fact(GlobalOrLocal::Global(blocked.clone()));
800            }
801            slf.prove_i(t)
802        })
803    }
804}
ftml_solver/paragraphs.rs

ftml_solver/
paragraphs.rs
