formality_core/
binder.rs

1//! Manages binders so that the main rules can be nice and simple.
2
3use std::sync::atomic::{AtomicUsize, Ordering};
4
5use anyhow::bail;
6use lazy_static::lazy_static;
7
8use crate::{
9    cast::{Downcast, DowncastFrom, DowncastTo, To, Upcast, UpcastFrom},
10    fold::CoreFold,
11    fold::SubstitutionFn,
12    language::{CoreKind, CoreParameter, HasKind, Language},
13    substitution::CoreSubstitution,
14    variable::{CoreBoundVar, CoreVariable, DebruijnIndex, VarIndex},
15    visit::CoreVisit,
16    Fallible,
17};
18
19#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
20pub struct CoreBinder<L: Language, T> {
21    kinds: Vec<CoreKind<L>>,
22    term: T,
23}
24
25impl<L: Language, T: CoreFold<L>> CoreBinder<L, T> {
26    /// Accesses the contents of the binder.
27    ///
28    /// The variables inside will be renamed to fresh var indices
29    /// that do not alias any other indices seen during this computation.
30    ///
31    /// The expectation is that you will create a term and use `Binder::new`.
32    pub fn open(&self) -> (Vec<CoreBoundVar<L>>, T) {
33        let (bound_vars, substitution): (Vec<CoreBoundVar<L>>, CoreSubstitution<L>) = self
34            .kinds
35            .iter()
36            .zip(0..)
37            .map(|(kind, index)| {
38                let old_bound_var = CoreBoundVar {
39                    debruijn: Some(DebruijnIndex::INNERMOST),
40                    var_index: VarIndex { index },
41                    kind: *kind,
42                };
43                let new_bound_var = CoreBoundVar::fresh(*kind);
44                (new_bound_var, (old_bound_var, new_bound_var))
45            })
46            .unzip();
47
48        (bound_vars, substitution.apply(&self.term))
49    }
50
51    pub fn dummy(term: T) -> Self {
52        let v: Vec<CoreVariable<L>> = vec![];
53        Self::new(v, term)
54    }
55
56    /// Given a set of variables (X, Y, Z) and a term referecing some subset of them,
57    /// create a binder where exactly those variables are bound (even the ones not used).
58    pub fn new(variables: impl Upcast<Vec<CoreVariable<L>>>, term: T) -> Self {
59        let variables: Vec<CoreVariable<L>> = variables.upcast();
60        let (kinds, substitution): (Vec<CoreKind<L>>, CoreSubstitution<L>) = variables
61            .iter()
62            .zip(0..)
63            .map(|(old_bound_var, index)| {
64                let old_bound_var: CoreVariable<L> = old_bound_var.upcast();
65                assert!(old_bound_var.is_free());
66                let new_bound_var: CoreParameter<L> = CoreBoundVar {
67                    debruijn: Some(DebruijnIndex::INNERMOST),
68                    var_index: VarIndex { index },
69                    kind: old_bound_var.kind(),
70                }
71                .upcast();
72                (old_bound_var.kind(), (old_bound_var, new_bound_var))
73            })
74            .unzip();
75
76        let term = substitution.apply(&term);
77        CoreBinder { kinds, term }
78    }
79
80    /// Given a set of variables (X, Y, Z) and a term referecing some subset of them,
81    /// create a binder for just those variables that are mentioned.
82    pub fn mentioned(variables: impl Upcast<Vec<CoreVariable<L>>>, term: T) -> Self {
83        let mut variables: Vec<CoreVariable<L>> = variables.upcast();
84        let fv = term.free_variables();
85        variables.retain(|v| fv.contains(v));
86        let variables: Vec<CoreVariable<L>> = variables.into_iter().collect();
87        CoreBinder::new(variables, term)
88    }
89
90    pub fn into<U>(self) -> CoreBinder<L, U>
91    where
92        T: Into<U>,
93    {
94        CoreBinder {
95            kinds: self.kinds,
96            term: self.term.into(),
97        }
98    }
99
100    /// Number of variables bound by this binder
101    pub fn len(&self) -> usize {
102        self.kinds.len()
103    }
104
105    pub fn is_empty(&self) -> bool {
106        self.kinds.is_empty()
107    }
108
109    /// Instantiate the binder with the given parameters, returning an err if the parameters
110    /// are the wrong number or ill-kinded.
111    pub fn instantiate_with(&self, parameters: &[impl Upcast<CoreParameter<L>>]) -> Fallible<T> {
112        if parameters.len() != self.kinds.len() {
113            bail!("wrong number of parameters");
114        }
115
116        for ((p, k), i) in parameters.iter().zip(&self.kinds).zip(0..) {
117            let p: CoreParameter<L> = p.upcast();
118            if p.kind() != *k {
119                bail!(
120                    "parameter {i} has kind {:?} but should have kind {:?}",
121                    p.kind(),
122                    k
123                );
124            }
125        }
126
127        Ok(self.instantiate(|_kind, index| parameters[index.index].to()))
128    }
129
130    /// Instantiate the term, replacing each bound variable with `op(i)`.
131    pub fn instantiate(&self, mut op: impl FnMut(CoreKind<L>, VarIndex) -> CoreParameter<L>) -> T {
132        let substitution: Vec<CoreParameter<L>> = self
133            .kinds
134            .iter()
135            .zip(0..)
136            .map(|(&kind, index)| op(kind, VarIndex { index }))
137            .collect();
138
139        self.term.substitute(&mut |var| match var {
140            CoreVariable::BoundVar(CoreBoundVar {
141                debruijn: Some(DebruijnIndex::INNERMOST),
142                var_index,
143                kind: _,
144            }) => Some(substitution[var_index.index].clone()),
145
146            _ => None,
147        })
148    }
149
150    /// Accesses the data inside the binder. Use this for simple tests that extract data
151    /// that is independent of the bound variables. If that's not the case, use `open`.
152    pub fn peek(&self) -> &T {
153        &self.term
154    }
155
156    /// Returns the kinds of each variable bound by this binder
157    pub fn kinds(&self) -> &[CoreKind<L>] {
158        &self.kinds
159    }
160
161    pub fn map<U: CoreFold<L>>(&self, op: impl FnOnce(T) -> U) -> CoreBinder<L, U> {
162        let (vars, t) = self.open();
163        let u = op(t);
164        CoreBinder::new(vars, u)
165    }
166}
167
168impl<L: Language> CoreBoundVar<L> {
169    /// Creates a fresh bound var of the given kind that is not yet part of a binder.
170    /// You can put this into a term and then use `Binder::new`.
171    pub fn fresh(kind: CoreKind<L>) -> Self {
172        lazy_static! {
173            static ref COUNTER: AtomicUsize = AtomicUsize::new(0);
174        }
175
176        let index = COUNTER.fetch_add(1, Ordering::SeqCst);
177        let var_index = VarIndex { index };
178        CoreBoundVar {
179            debruijn: None,
180            var_index,
181            kind,
182        }
183    }
184}
185
186impl<L: Language, T: CoreVisit<L>> CoreVisit<L> for CoreBinder<L, T> {
187    fn free_variables(&self) -> Vec<CoreVariable<L>> {
188        self.term.free_variables()
189    }
190
191    fn size(&self) -> usize {
192        self.term.size()
193    }
194
195    fn assert_valid(&self) {
196        self.term.assert_valid();
197    }
198}
199
200impl<L: Language, T: CoreFold<L>> CoreFold<L> for CoreBinder<L, T> {
201    fn substitute(&self, substitution_fn: SubstitutionFn<'_, L>) -> Self {
202        let term = self.term.substitute(&mut |v| {
203            // Shift this variable out through the binder. If that fails,
204            // it's a variable bound by this binder, so the substitution can't
205            // affect it, and we can just return None.
206            let v1 = v.shift_out()?;
207
208            // Get the result of the subst (if any).
209            let parameter = substitution_fn(v1)?;
210
211            // Shift that result in to account for this binder.
212            Some(parameter.shift_in())
213        });
214
215        CoreBinder {
216            kinds: self.kinds.clone(),
217            term,
218        }
219    }
220
221    fn shift_in(&self) -> Self {
222        let term = self.term.shift_in();
223        CoreBinder {
224            kinds: self.kinds.clone(),
225            term,
226        }
227    }
228}
229
230impl<L: Language, T, U> UpcastFrom<CoreBinder<L, T>> for CoreBinder<L, U>
231where
232    T: Clone,
233    U: Clone,
234    T: Upcast<U>,
235{
236    fn upcast_from(term: CoreBinder<L, T>) -> Self {
237        let CoreBinder { kinds, term } = term;
238        CoreBinder {
239            kinds,
240            term: term.upcast(),
241        }
242    }
243}
244
245impl<L: Language, T, U> DowncastTo<CoreBinder<L, T>> for CoreBinder<L, U>
246where
247    T: DowncastFrom<U>,
248{
249    fn downcast_to(&self) -> Option<CoreBinder<L, T>> {
250        let CoreBinder { kinds, term } = self;
251        let term = term.downcast()?;
252        Some(CoreBinder {
253            kinds: kinds.clone(),
254            term,
255        })
256    }
257}
258
259impl<L: Language, T> std::fmt::Debug for CoreBinder<L, T>
260where
261    T: std::fmt::Debug,
262{
263    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
264        write!(f, "<")?;
265        for (kind, i) in self.kinds.iter().zip(0..) {
266            if i > 0 {
267                write!(f, ", ")?;
268            }
269            write!(f, "{:?}", kind)?;
270        }
271        write!(f, "> ")?;
272        write!(f, "{:?}", &self.term)?;
273        Ok(())
274    }
275}
formality_core/binder.rs

formality_core/
binder.rs
