ftml_solver/rules/operators/
bindin.rs

1use std::{borrow::Cow, hint::unreachable_unchecked};
2
3use ftml_ontology::terms::{
4    ApplicationTerm, Argument, BindingTerm, BoundArgument, ComponentVar, MaybeSequence, Term,
5    helpers::IntoTerm,
6};
7use ftml_solver_trace::{SizedSolverRule, traceref};
8use ftml_uris::SymbolUri;
9
10use crate::{
11    CheckRef,
12    rules::{InferenceRule, InhabitableRule, SimplificationRule},
13    split::SplitStrategy,
14};
15
16#[derive(Debug, Clone, PartialEq, Eq)]
17pub struct BindInInhabitableRule {
18    pub bindin: SymbolUri,
19    pub bind: SymbolUri,
20}
21impl SizedSolverRule for BindInInhabitableRule {
22    fn display(&self) -> Vec<crate::trace::Displayable> {
23        ftml_solver_trace::trace!(
24            "{ INH T, INH B, f: (",
25            &self.bind,
26            " x:T. B), INH t } ⊢ INH ",
27            &self.bindin,
28            " f: (",
29            &self.bind,
30            " x:T. B). t"
31        )
32    }
33}
34impl<Split: SplitStrategy> InhabitableRule<Split> for BindInInhabitableRule {
35    fn applicable(&self, term: &Term) -> bool {
36        if let Term::Bound(b) = term
37            && let Term::Symbol { uri, .. } = &b.head
38            && *uri == self.bindin
39            && let [BoundArgument::BoundSeq(_), BoundArgument::Simple(_)] = &*b.arguments
40        {
41            true
42        } else {
43            false
44        }
45    }
46    fn apply<'t>(
47        &self,
48        mut checker: crate::CheckRef<'t, '_, Split>,
49        term: &'t Term,
50    ) -> Option<bool> {
51        let Term::Bound(b) = term else { return None };
52        let [BoundArgument::BoundSeq(f), BoundArgument::Simple(ret)] = &*b.arguments else {
53            return None;
54        };
55        match f {
56            MaybeSequence::Seq(seq) if seq.len() == 1 => {
57                let [
58                    ComponentVar {
59                        var,
60                        tp: Some(tp),
61                        df: None,
62                    },
63                ] = &**seq
64                else {
65                    // technically unreachable
66                    return None;
67                };
68                let Some(bind) = checker.simplify_until(tp, |_, t| {
69                    if let Term::Bound(b) = t
70                        && let Term::Symbol { uri, .. } = &b.head
71                        && *uri == self.bind
72                    {
73                        true
74                    } else {
75                        false
76                    }
77                }) else {
78                    checker.failure("Type of bound variable is not a binder");
79                    return None;
80                };
81                // subsumes INH T, INH B
82                if !checker.scoped(|checker| checker.check_inhabitable(&bind))? {
83                    return None;
84                }
85                checker.extend_context(ComponentVar {
86                    var: var.clone(),
87                    tp: Some(bind.into_owned()),
88                    df: None,
89                });
90                checker.check_inhabitable(ret)
91            }
92            MaybeSequence::Seq(_) => {
93                checker.comment("TODO: sequence variable in BindIn");
94                None
95            }
96            MaybeSequence::One(_) => {
97                checker.failure("Untyped bound variable");
98                None
99            }
100        }
101    }
102}
103
104#[derive(Debug, Clone, PartialEq, Eq)]
105pub struct BindInInferenceRule {
106    pub bindin: SymbolUri,
107    pub bind: SymbolUri,
108}
109impl SizedSolverRule for BindInInferenceRule {
110    fn display(&self) -> Vec<crate::trace::Displayable> {
111        ftml_solver_trace::trace!(
112            "{ INH A, INH B, f: (",
113            &self.bind,
114            " x:A. B), t: T } ⊢ (",
115            &self.bindin,
116            " f: (",
117            &self.bind,
118            " x:A. B). t) :=> ",
119            &self.bindin,
120            " f: (",
121            &self.bind,
122            " x:A. B). T"
123        )
124    }
125}
126impl<Split: SplitStrategy> InferenceRule<Split> for BindInInferenceRule {
127    fn applicable(&self, term: &Term) -> bool {
128        if let Term::Bound(b) = term
129            && let Term::Symbol { uri, .. } = &b.head
130            && *uri == self.bindin
131            && let [BoundArgument::BoundSeq(_), BoundArgument::Simple(_)] = &*b.arguments
132        {
133            true
134        } else {
135            false
136        }
137    }
138
139    fn infer<'t>(
140        &self,
141        mut checker: crate::CheckRef<'t, '_, Split>,
142        term: &'t Term,
143    ) -> Option<Term> {
144        let Term::Bound(b) = term else { return None };
145        let [BoundArgument::BoundSeq(f), BoundArgument::Simple(ret)] = &*b.arguments else {
146            return None;
147        };
148        match f {
149            MaybeSequence::Seq(seq) if seq.len() == 1 => {
150                let [
151                    cv @ ComponentVar {
152                        var,
153                        tp: Some(tp),
154                        df: None,
155                    },
156                ] = &**seq
157                else {
158                    // technically unreachable
159                    return None;
160                };
161                checker.extend_context(cv);
162
163                // first infer type of body, *then* check type of variable
164                // to potentially solve variables
165                let body = checker.infer_type(ret)?;
166
167                let Some(bind) = checker.simplify_until(tp, |_, t| {
168                    if let Term::Bound(b) = t
169                        && let Term::Symbol { uri, .. } = &b.head
170                        && *uri == self.bind
171                    {
172                        true
173                    } else {
174                        false
175                    }
176                }) else {
177                    checker.failure("Type of bound variable is not a binder");
178                    return None;
179                };
180                // subsumes INH T, INH B
181                if !checker.scoped(|checker| checker.check_inhabitable(&bind))? {
182                    return None;
183                }
184
185                Some(Term::Bound(BindingTerm::new(
186                    b.head.clone(),
187                    Box::new([
188                        BoundArgument::BoundSeq(MaybeSequence::Seq(Box::new([ComponentVar {
189                            var: var.clone(),
190                            tp: Some(bind.into_owned()),
191                            df: None,
192                        }]))),
193                        BoundArgument::Simple(body),
194                    ]),
195                    None,
196                )))
197            }
198            MaybeSequence::Seq(_) => {
199                checker.comment("TODO: sequence variable in BindIn");
200                None
201            }
202            MaybeSequence::One(_) => {
203                checker.failure("Untyped bound variable");
204                None
205            }
206        }
207    }
208    /*
209    fn apply<'t>(
210        &self,
211        mut checker: crate::CheckRef<'t, '_, Split>,
212        term: &'t Term,
213    ) -> Option<bool> {
214
215    }
216     */
217}
218
219#[derive(Debug, Clone, PartialEq, Eq)]
220pub struct BindInApplyRule {
221    pub bindin: SymbolUri,
222    pub bind: SymbolUri,
223}
224impl SizedSolverRule for BindInApplyRule {
225    fn display(&self) -> Vec<crate::trace::Displayable> {
226        ftml_solver_trace::trace!(
227            "{ F: (",
228            &self.bindin,
229            " f: (",
230            &self.bind,
231            " x:A. B). T(f)) } ⊢ F y:A. t :=> T(",
232            &self.bind,
233            " y:A. t)"
234        )
235    }
236}
237impl<Split: SplitStrategy> InferenceRule<Split> for BindInApplyRule {
238    fn applicable(&self, term: &Term) -> bool {
239        matches!(term, Term::Bound(_))
240    }
241    fn infer<'t>(
242        &self,
243        mut checker: crate::CheckRef<'t, '_, Split>,
244        term: &'t Term,
245    ) -> Option<Term> {
246        let Term::Bound(app) = term else { return None };
247        let mut ret = checker.infer_type(&app.head)?;
248        let args = &*app.arguments;
249        let mut i = 0;
250        loop {
251            if args.get(i).is_none() {
252                return Some(ret);
253            }
254            let (b, is_bindin) = self.deconstruct_tp(&mut checker, ret)?;
255
256            let [first, BoundArgument::Simple(body)] = &*b.arguments else {
257                // SAFETY: invariant of deconstruct_tp
258                unsafe { unreachable_unchecked() }
259            };
260            // SAFETY: !args.get(i).is_none() above
261            let arg = unsafe { args.get(i).unwrap_unchecked() };
262            if is_bindin {
263                let Some(BoundArgument::Simple(next_arg)) = args.get(i + 1) else {
264                    checker.failure("Need normal argument after bound variable");
265                    return None;
266                };
267                checker.counter("Binding argument", i + 1);
268                i += 2;
269                let BoundArgument::BoundSeq(MaybeSequence::Seq(seq)) = first else {
270                    checker.failure("not a bound variable sequence");
271                    return None;
272                };
273                let [
274                    ComponentVar {
275                        var: tpvar,
276                        tp: Some(expected),
277                        df: None,
278                    },
279                ] = &**seq
280                else {
281                    checker.failure("TODO: multiple bound variables / type inference 1");
282                    return None;
283                };
284
285                if let BoundArgument::Bound(cv @ ComponentVar { df: None, .. })
286                | BoundArgument::BoundSeq(MaybeSequence::One(
287                    cv @ ComponentVar { df: None, .. },
288                )) = arg
289                {
290                    let f = Term::Bound(BindingTerm::new(
291                        Term::Symbol {
292                            uri: self.bind.clone(),
293                            presentation: None,
294                        },
295                        Box::new([
296                            if matches!(arg, BoundArgument::BoundSeq(_)) {
297                                BoundArgument::BoundSeq(MaybeSequence::One(cv.clone()))
298                            } else {
299                                BoundArgument::Bound(cv.clone())
300                            },
301                            BoundArgument::Simple(next_arg.clone()),
302                        ]),
303                        None,
304                    ));
305                    if !checker.scoped(|checker| checker.check_type(&f, expected))? {
306                        return None;
307                    }
308                    ret = (body / (tpvar.name(), &f)).into_owned();
309                } else {
310                    checker.failure("TODO: multiple bound variables / type inference 2");
311                    return None;
312                }
313            } else {
314                ret = self.do_app(&mut checker, first, arg, body, &b, &mut i)?;
315            }
316        }
317    }
318}
319
320impl BindInApplyRule {
321    // INVARIANT: return has 2 arguments, the second one being simple
322    fn deconstruct_tp<Split: SplitStrategy>(
323        &self,
324        checker: &mut CheckRef<'_, '_, Split>,
325        tp: Term,
326    ) -> Option<(BindingTerm, bool)> {
327        let Some(nret) = checker.scoped(|checker| {
328            match checker.simplify_until(&tp, |_, t| matches!(t, Term::Bound(_)))? {
329                Cow::Borrowed(_) => Some(None),
330                Cow::Owned(tp) => Some(Some(tp)),
331            }
332        }) else {
333            checker.add_msg(traceref!(FAIL "type is not a binder: ",tp).into());
334            return None;
335        };
336        let Term::Bound(b) = nret.unwrap_or(tp) else {
337            // SAFETY: simplify_until above would have returned None otherwise
338            unsafe { unreachable_unchecked() }
339        };
340        if b.arguments.len() != 2 || !matches!(b.arguments.get(1), Some(BoundArgument::Simple(_))) {
341            checker.failure("Type is not a Π anymore");
342            return None;
343        }
344        match &b.head {
345            Term::Symbol { uri, .. } if *uri == self.bind => Some((b, false)),
346            Term::Symbol { uri, .. } if *uri == self.bindin => Some((b, true)),
347            _ => None,
348        }
349    }
350
351    fn do_app<'t, Split: SplitStrategy>(
352        &self,
353        checker: &mut crate::CheckRef<'t, '_, Split>,
354        first: &BoundArgument,
355        arg: &'t BoundArgument,
356        body: &Term,
357        b: &BindingTerm,
358        i: &mut usize,
359    ) -> Option<Term> {
360        match (first, arg) {
361            (
362                BoundArgument::Bound(ComponentVar {
363                    var,
364                    tp: Some(tp),
365                    df: None,
366                }),
367                BoundArgument::Sequence(seq),
368            ) if !body.has_free_such_that(|v| v.name() == var.name())
369                && tp.as_sequence().is_some_and(|s| s.is_concrete()) =>
370            {
371                Some(super::pi::PiInferenceRule::flatten_sequence(
372                    checker,
373                    tp,
374                    b,
375                    body.clone(),
376                ))
377            }
378            (
379                BoundArgument::Bound(ComponentVar {
380                    var,
381                    tp: Some(tp),
382                    df: None,
383                }),
384                BoundArgument::Sequence(MaybeSequence::Seq(seq)),
385            ) if !seq.is_empty() => {
386                *i += 1;
387                checker.counter("Checking Argument", *i);
388                super::pi::PiInferenceRule::recurse_seq_args(&self.bind, checker, b, seq, body)
389            }
390            (_, BoundArgument::Simple(arg)) => {
391                *i += 1;
392                checker.counter("Checking Argument", *i);
393                super::pi::PiInferenceRule::simple_apply(checker, b, arg, body)
394            }
395            (_, BoundArgument::Sequence(arg)) => {
396                *i += 1;
397                checker.counter("Checking Argument", *i);
398                checker
399                    .scoped(|checker| super::pi::PiInferenceRule::seq_apply(checker, b, arg, body))
400            }
401            _ => {
402                checker.failure("argument modes don't match");
403                None
404            }
405        }
406    }
407}
408
409#[derive(Debug, Clone, PartialEq, Eq)]
410pub struct BindInComputationRule {
411    pub bindin: SymbolUri,
412    pub bind: SymbolUri,
413}
414impl SizedSolverRule for BindInComputationRule {
415    fn display(&self) -> Vec<crate::trace::Displayable> {
416        ftml_solver_trace::trace!(
417            "⊢ ( ",
418            &self.bindin,
419            " f: (",
420            &self.bind,
421            " x:A. B). t(f)) ) y:A. z ==> t(",
422            &self.bind,
423            " y:A. z)"
424        )
425    }
426}
427impl<Split: SplitStrategy> SimplificationRule<Split> for BindInComputationRule {
428    fn applicable(&self, term: &Term) -> bool {
429        if let Term::Bound(b) = term
430            && let Term::Bound(b) = &b.head
431            && let Term::Symbol { uri, .. } = &b.head
432        {
433            *uri == self.bindin
434                && matches!(
435                    &*b.arguments,
436                    [
437                        BoundArgument::Bound(_) | BoundArgument::BoundSeq(_),
438                        BoundArgument::Simple(_)
439                    ]
440                )
441        } else {
442            false
443        }
444    }
445    fn apply<'t>(
446        &self,
447        mut checker: CheckRef<'t, '_, Split>,
448        term: &'t Term,
449    ) -> Result<Term, Option<ftml_ontology::terms::termpaths::TermPath>> {
450        let Term::Bound(top) = term else {
451            return Err(None);
452        };
453        let Term::Bound(bindin_term) = &top.head else {
454            return Err(None);
455        };
456        let [bv, BoundArgument::Simple(body)] = &*bindin_term.arguments else {
457            return Err(None);
458        };
459        let bv = match bv {
460            BoundArgument::Bound(v) => v,
461            BoundArgument::BoundSeq(MaybeSequence::Seq(vs)) if let [v] = &**vs => v,
462            _ => return Err(None),
463        };
464        let f = &bv.var;
465        let Some(Term::Bound(bind)) = &bv.tp else {
466            return Err(None);
467        };
468        match &bind.head {
469            Term::Symbol { uri, .. } if *uri == self.bind => (),
470            _ => return Err(None),
471        }
472
473        let [f_bv, BoundArgument::Simple(f_ret_tp)] = &*bind.arguments else {
474            return Err(None);
475        };
476        let f_bv = match f_bv {
477            BoundArgument::Bound(v) => v,
478            BoundArgument::BoundSeq(MaybeSequence::Seq(vs)) if let [v] = &**vs => v,
479            _ => return Err(None),
480        };
481        let Some(f_arg_tp) = &f_bv.tp else {
482            return Err(None);
483        };
484
485        let top_args = &*top.arguments;
486        let top_bv = match top_args.first() {
487            Some(BoundArgument::Bound(bv)) => bv,
488            Some(BoundArgument::BoundSeq(MaybeSequence::Seq(vs))) if let [bv] = &**vs => bv,
489            _ => return Err(None),
490        };
491        let Some(BoundArgument::Simple(f_body)) = top_args.get(1) else {
492            return Err(None);
493        };
494        let tp = match &top_bv.tp {
495            Some(tp) => {
496                if checker.check_equality(tp, f_arg_tp) != Some(true) {
497                    return Err(None);
498                }
499                tp
500            }
501            _ => f_arg_tp,
502        };
503        let ret_tp = f_ret_tp / (f_bv.var.name(), &top_bv.var.clone().into());
504        if checker.scoped(|checker| {
505            checker.extend_context(ComponentVar {
506                var: top_bv.var.clone(),
507                tp: Some(tp.clone()),
508                df: None,
509            });
510            checker.check_type(f_body, &ret_tp)
511        }) != Some(true)
512        {
513            return Err(None);
514        }
515
516        let resolved = body
517            / (
518                f.name(),
519                &self.bind.clone().simple_bind(
520                    top_bv.var.clone(),
521                    Some(tp.clone()),
522                    None,
523                    f_body.clone(),
524                ),
525            );
526        let resolved = resolved.into_owned();
527        let rest_args = &top_args[2..];
528        Ok(if rest_args.is_empty() {
529            resolved
530        } else if rest_args
531            .iter()
532            .all(|a| matches!(a, BoundArgument::Sequence(_) | BoundArgument::Simple(_)))
533        {
534            Term::Application(ApplicationTerm::new(
535                resolved,
536                rest_args
537                    .iter()
538                    .map(|a| match a {
539                        BoundArgument::Sequence(s) => Argument::Sequence(s.clone()),
540                        BoundArgument::Simple(t) => Argument::Simple(t.clone()),
541                        // SAFETY: iter().all() check above
542                        _ => unsafe { unreachable_unchecked() },
543                    })
544                    .collect(),
545                None,
546            ))
547        } else {
548            Term::Bound(BindingTerm::new(
549                resolved,
550                rest_args.to_vec().into_boxed_slice(),
551                None,
552            ))
553        })
554    }
555}
ftml_solver/rules/operators/bindin.rs

ftml_solver/rules/operators/
bindin.rs
