ftml_solver/
paragraphs.rs

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

ftml_solver/
paragraphs.rs
