ftml_solver/rules/
unknowns.rs

1use std::borrow::Cow;
2
3use ftml_ontology::terms::{ApplicationTerm, Argument, BoundArgument, MaybeSequence, Term};
4use ftml_solver_trace::SizedSolverRule;
5
6use crate::{
7    impls::solving::TermExtSolvable,
8    rules::{InferenceRule, SimplificationRule},
9    split::SplitStrategy,
10};
11
12#[derive(Debug, Copy, Clone, PartialEq, Eq)]
13pub struct UnknownsRule;
14impl SizedSolverRule for UnknownsRule {
15    fn display(&self) -> Vec<crate::trace::Displayable> {
16        ftml_solver_trace::trace!("bound unknowns")
17    }
18    fn priority(&self) -> isize {
19        100_000
20    }
21}
22
23fn unsolved<'t, Split: SplitStrategy>(
24    mut checker: crate::CheckRef<'t, '_, Split>,
25    app: &'t ApplicationTerm,
26) -> Option<Term> {
27    let [Argument::Sequence(MaybeSequence::Seq(args))] = &*app.arguments else {
28        checker.failure("argument is not simple");
29        return None;
30    };
31    let tp = checker.infer_type(&app.head)?;
32    let Term::Bound(b) = tp else {
33        checker.failure("not a binder");
34        return None;
35    };
36    if !b.head.is(&*ftml_uris::metatheory::BIND_UNKNOWNS) {
37        checker.failure("Not an unknown binder");
38        return None;
39    }
40    let [
41        BoundArgument::BoundSeq(MaybeSequence::Seq(vs)),
42        BoundArgument::Simple(body),
43    ] = &*b.arguments
44    else {
45        checker.failure("arguments don't match");
46        return None;
47    };
48    if vs.len() != args.len() {
49        checker.failure("lengths don't match");
50        return None;
51    }
52    let mut substs = smallvec::SmallVec::<_, 2>::new();
53    for (v, arg) in vs.iter().zip(args.iter()) {
54        if let Some(tp) = v.tp.as_ref() {
55            let tp = tp / &*substs;
56            if !checker.scoped(|slf| slf.check_type(arg, &tp))? {
57                return None;
58            }
59            substs.push((v.var.name(), arg));
60        }
61    }
62    Some(body.clone() / &*substs)
63}
64impl<Split: SplitStrategy> SimplificationRule<Split> for UnknownsRule {
65    fn applicable(&self, term: &ftml_ontology::terms::Term) -> bool {
66        if let Term::Application(app) = term
67            && let Term::Bound(b) = &app.head
68            && b.head.is(&*ftml_uris::metatheory::BIND_UNKNOWNS)
69            && let [
70                BoundArgument::BoundSeq(MaybeSequence::Seq(vs)),
71                BoundArgument::Simple(_),
72            ] = &*b.arguments
73            && let [Argument::Sequence(MaybeSequence::Seq(args))] = &*app.arguments
74        {
75            vs.len() == args.len()
76        } else {
77            false
78        }
79    }
80    fn apply<'t>(
81        &self,
82        // TODO should check types
83        checker: crate::CheckRef<'t, '_, Split>,
84        term: &'t Term,
85    ) -> Result<Term, Option<ftml_ontology::terms::termpaths::TermPath>> {
86        match beta_unknowns_cow(term) {
87            Cow::Owned(term) => Ok(term),
88            _ => Err(None),
89        }
90    }
91}
92
93impl<Split: SplitStrategy> InferenceRule<Split> for UnknownsRule {
94    fn applicable(&self, term: &ftml_ontology::terms::Term) -> bool {
95        let Term::Application(app) = term else {
96            return false;
97        };
98        if app.head.is_solvable().is_some() {
99            return true;
100        }
101        if let Term::Bound(b) = &app.head
102            && b.head.is(&*ftml_uris::metatheory::BIND_UNKNOWNS)
103            && let [
104                BoundArgument::BoundSeq(MaybeSequence::Seq(vs)),
105                BoundArgument::Simple(_),
106            ] = &*b.arguments
107            && let [Argument::Sequence(MaybeSequence::Seq(args))] = &*app.arguments
108        {
109            vs.len() == args.len()
110        } else {
111            false
112        }
113    }
114    fn infer<'t>(
115        &self,
116        mut checker: crate::CheckRef<'t, '_, Split>,
117        term: &'t Term,
118    ) -> Option<Term> {
119        let Term::Application(app) = term else {
120            return None;
121        };
122        if app.head.is_solvable().is_some() {
123            unsolved(checker, app)
124        } else if let Cow::Owned(t) = beta_unknowns_cow(term) {
125            // TODO should check types ?
126            checker.scoped(|slf| slf.infer_type(&t))
127        } else {
128            None
129        }
130    }
131}
132
133pub(crate) fn beta_unknowns(t: Term) -> Term {
134    if let Cow::Owned(t) = beta_unknowns_cow(&t) {
135        t
136    } else {
137        t
138    }
139}
140
141pub(crate) fn beta_unknowns_cow(t: &Term) -> Cow<'_, Term> {
142    //tracing::warn!("Applying beta to {:?}", t.debug_short());
143    let r = t.modify(|t| {
144        if let Term::Application(app) = t
145            && let Term::Bound(b) = &app.head
146            && b.head.is(&*ftml_uris::metatheory::BIND_UNKNOWNS)
147            && let [
148                BoundArgument::BoundSeq(MaybeSequence::Seq(vs)),
149                BoundArgument::Simple(body),
150            ] = &*b.arguments
151            && let [Argument::Sequence(MaybeSequence::Seq(args))] = &*app.arguments
152            && vs.len() == args.len()
153        {
154            let substs = vs
155                .iter()
156                .map(|i| i.var.name())
157                .zip(args.iter())
158                .collect::<smallvec::SmallVec<_, 2>>();
159            let r = body.clone() / &*substs;
160            /*tracing::warn!(
161                "Substituting: {:?}\n        {:?}",
162                t.debug_short(),
163                r.debug_short()
164            );*/
165            Some(r)
166        } else {
167            None
168        }
169    });
170    /*match &r {
171        Cow::Owned(t) => tracing::warn!("Changed: {:?}", t.debug_short()),
172        _ => tracing::warn!("unchanged"),
173    }*/
174    r
175}
ftml_solver/rules/unknowns.rs

ftml_solver/rules/
unknowns.rs
