catlog/tt/
eval.rs

1//! Evaluation, quoting, and conversion/equality checking
2//!
3//! At a high level, this module implements three operations:
4//!
5//! - `eval : syntax -> value` ([Evaluator::eval_tm], [Evaluator::eval_ty])
6//! - `quote : value -> syntax` ([Evaluator::quote_tm], [Evaluator::quote_neu], [Evaluator::quote_ty])
7//! - `convertable? : value -> value -> bool` ([Evaluator::equal_tm], [Evaluator::element_of], [Evaluator::subtype])
8use crate::{
9    tt::{prelude::*, stx::*, toplevel::*, val::*},
10    zero::LabelSegment,
11};
12
13/// The context used in evaluation, quoting, and conversion checking
14///
15/// We bundle this all together because conversion checking and quoting
16/// sometimes need to evaluate terms. For instance, quoting a lambda
17/// involves evaluating the body of the lambda in the context of a freshly
18/// introduced variable; even though we don't have lambdas, a similar
19/// thing applies to dependent records.
20#[derive(Clone)]
21pub struct Evaluator<'a> {
22    toplevel: &'a Toplevel,
23    env: Env,
24    // The next neutral
25    scope_length: usize,
26}
27
28impl<'a> Evaluator<'a> {
29    /// Constructor for [Evaluator]
30    pub fn new(toplevel: &'a Toplevel, env: Env, scope_length: usize) -> Self {
31        Self {
32            toplevel,
33            env,
34            scope_length,
35        }
36    }
37
38    fn eval_record(&self, r: &RecordS) -> RecordV {
39        RecordV::new(r.fields0.clone(), self.env.clone(), r.fields1.clone(), Dtry::empty())
40    }
41
42    /// Return a new [Evaluator] with environment `env`
43    pub fn with_env(&self, env: Env) -> Self {
44        Self {
45            env,
46            ..self.clone()
47        }
48    }
49
50    /// Evaluate type syntax to produce a type value
51    ///
52    /// Assumes that the type syntax is well-formed and well-scoped with respect
53    /// to self.env
54    pub fn eval_ty(&self, ty: &TyS) -> TyV {
55        match &**ty {
56            TyS_::TopVar(tv) => self.toplevel.declarations.get(tv).unwrap().as_ty().val,
57            TyS_::Object(ot) => TyV::object(ot.clone()),
58            TyS_::Morphism(pt, dom, cod) => {
59                TyV::morphism(pt.clone(), self.eval_tm(dom), self.eval_tm(cod))
60            }
61            TyS_::Record(r) => TyV::record(self.eval_record(r)),
62            TyS_::Sing(ty_s, tm_s) => TyV::sing(self.eval_ty(ty_s), self.eval_tm(tm_s)),
63            TyS_::Specialize(ty_s, specializations) => {
64                specializations.iter().fold(self.eval_ty(ty_s), |ty_v, (path, s)| {
65                    ty_v.add_specialization(path, self.eval_ty(s))
66                })
67            }
68            TyS_::Unit => TyV::unit(),
69        }
70    }
71
72    /// Evaluate term syntax to produce a term value
73    ///
74    /// Assumes that the term syntax is well-formed and well-scoped with respect
75    /// to self.env
76    pub fn eval_tm(&self, tm: &TmS) -> TmV {
77        match &**tm {
78            TmS_::TopVar(tv) => self.toplevel.declarations.get(tv).unwrap().as_const().val,
79            TmS_::TopApp(tv, args_s) => {
80                let env = Env::nil().extend_by(args_s.iter().map(|arg_s| self.eval_tm(arg_s)));
81                let def = self.toplevel.declarations.get(tv).unwrap().as_def();
82                self.with_env(env).eval_tm(&def.body)
83            }
84            TmS_::Var(i, _, _) => self.env.get(**i).cloned().unwrap(),
85            TmS_::Cons(fields) => TmV::Cons(fields.map(|tm| self.eval_tm(tm))),
86            TmS_::Proj(tm, field, label) => self.proj(&self.eval_tm(tm), *field, *label),
87            TmS_::Tt => TmV::Tt,
88            TmS_::Id(_) => TmV::Opaque,
89            TmS_::Compose(_, _) => TmV::Opaque,
90            TmS_::Opaque => TmV::Opaque,
91        }
92    }
93
94    /// Compute the projection of a field from a term value
95    pub fn proj(&self, tm: &TmV, field_name: FieldName, field_label: LabelSegment) -> TmV {
96        match tm {
97            TmV::Neu(n, ty) => TmV::Neu(
98                TmN::proj(n.clone(), field_name, field_label),
99                self.field_ty(ty, tm, field_name),
100            ),
101            TmV::Cons(fields) => fields.get(field_name).cloned().unwrap(),
102            _ => panic!(),
103        }
104    }
105
106    /// Evaluate the type of the field `field_name` of `val : ty`.
107    pub fn field_ty(&self, ty: &TyV, val: &TmV, field_name: FieldName) -> TyV {
108        match &**ty {
109            TyV_::Record(r) => {
110                let field_ty_s = r.fields1.get(field_name).unwrap();
111                let orig_field_ty = self.with_env(r.env.snoc(val.clone())).eval_ty(field_ty_s);
112                match r.specializations.entry(&field_name) {
113                    Some(DtryEntry::File(ty)) => ty.clone(),
114                    Some(DtryEntry::SubDir(d)) => orig_field_ty.specialize(d),
115                    Option::None => orig_field_ty,
116                }
117            }
118            _ => panic!("tried to get the type of field for non-record type"),
119        }
120    }
121
122    /// Bind a new neutral of type `ty`
123    pub fn bind_neu(&self, name: VarName, label: LabelSegment, ty: TyV) -> (TmN, Self) {
124        let n = TmN::var(self.scope_length.into(), name, label);
125        let v = TmV::Neu(n.clone(), ty);
126        (
127            n,
128            Self {
129                env: self.env.snoc(v),
130                scope_length: self.scope_length + 1,
131                ..self.clone()
132            },
133        )
134    }
135
136    /// Bind a variable called "self" to `ty`
137    pub fn bind_self(&self, ty: TyV) -> (TmN, Self) {
138        self.bind_neu(name_seg("self"), label_seg("self"), ty)
139    }
140
141    /// Produce type syntax from a type value.
142    ///
143    /// This is a *section* of eval, in that `self.eval_ty(self.quote_ty(ty_v)) == ty_v`
144    /// but it is not necessarily true that `self.quote_ty(self.eval_ty(ty_s)) == ty_v`.
145    ///
146    /// This is used for displaying [TyV] to the user in type errors, and for
147    /// creating syntax that can be re-evaluated in other contexts. In theory this
148    /// could be used for conversion checking, but it's more efficient to implement
149    /// that directly, and it's better to *not* do eta-expansion for user-facing
150    /// messages or for syntax that is meant to be re-evaluated.
151    pub fn quote_ty(&self, ty: &TyV) -> TyS {
152        match &**ty {
153            TyV_::Object(object_type) => TyS::object(object_type.clone()),
154            TyV_::Morphism(morphism_type, dom, cod) => {
155                TyS::morphism(morphism_type.clone(), self.quote_tm(dom), self.quote_tm(cod))
156            }
157            TyV_::Record(r) => {
158                let r_eval = self.with_env(r.env.clone()).bind_self(ty.clone()).1;
159                let fields1 = r
160                    .fields1
161                    .map(|ty_s| self.bind_self(ty.clone()).1.quote_ty(&r_eval.eval_ty(ty_s)));
162                let record_ty_s = TyS::record(RecordS::new(r.fields0.clone(), fields1));
163                if r.specializations.is_empty() {
164                    record_ty_s
165                } else {
166                    TyS::specialize(
167                        record_ty_s,
168                        r.specializations
169                            .flatten()
170                            .into_iter()
171                            .map(|(name, label, ty_v)| {
172                                (
173                                    name.segments()
174                                        .copied()
175                                        .zip(label.segments().copied())
176                                        .collect::<Vec<_>>(),
177                                    self.quote_ty(&ty_v),
178                                )
179                            })
180                            .collect(),
181                    )
182                }
183            }
184            TyV_::Sing(ty, tm) => TyS::sing(self.quote_ty(ty), self.quote_tm(tm)),
185            TyV_::Unit => TyS::unit(),
186        }
187    }
188
189    /// Produce term syntax from a term neutral.
190    ///
191    /// The documentation for [Evaluator::quote_ty] is also applicable here.
192    pub fn quote_neu(&self, n: &TmN) -> TmS {
193        match &**n {
194            TmN_::Var(i, name, label) => TmS::var(i.as_bwd(self.scope_length), *name, *label),
195            TmN_::Proj(tm, field, label) => TmS::proj(self.quote_neu(tm), *field, *label),
196        }
197    }
198
199    /// Produce term syntax from a term value.
200    ///
201    /// The documentation for [Evaluator::quote_ty] is also applicable here.
202    pub fn quote_tm(&self, tm: &TmV) -> TmS {
203        match tm {
204            TmV::Neu(n, _) => self.quote_neu(n),
205            TmV::Cons(fields) => TmS::cons(fields.map(|tm| self.quote_tm(tm))),
206            TmV::Tt => TmS::tt(),
207            TmV::Opaque => TmS::opaque(),
208        }
209    }
210
211    /// Check if `ty1` is a subtype of `ty2`.
212    ///
213    /// This is true iff `ty1` is convertable with `ty2`, and an eta-expanded
214    /// neutral of type `ty1` is an element of `ty2`.
215    pub fn subtype<'b>(&self, ty1: &TyV, ty2: &TyV) -> Result<(), D<'b>> {
216        self.convertable_ty(ty1, ty2)?;
217        let (n, _) = self.bind_self(ty1.clone());
218        let v = self.eta_neu(&n, ty1);
219        self.element_of(&v, ty2)
220    }
221
222    /// Check if `tm` is an element of `ty`, accounting for specializations
223    /// of `ty`.
224    ///
225    /// Precondition: the type of `tm` must be convertable with `ty`, and `tm`
226    /// is eta-expanded.
227    ///
228    /// Example: if `a : Entity` and `b : Entity` are neutrals, then `a` is not an
229    /// element of `@sing b`, but `a` is an element of `@sing a`.
230    pub fn element_of<'b>(&self, tm: &TmV, ty: &TyV) -> Result<(), D<'b>> {
231        match &**ty {
232            TyV_::Object(_) => Ok(()),
233            TyV_::Morphism(_, _, _) => Ok(()),
234            TyV_::Record(r) => {
235                for (name, (label, _)) in r.fields1.iter() {
236                    self.element_of(&self.proj(tm, *name, *label), &self.field_ty(ty, tm, *name))?
237                }
238                Ok(())
239            }
240            TyV_::Sing(_, x) => self.equal_tm(tm, x),
241            TyV_::Unit => Ok(()),
242        }
243    }
244
245    /// Check if two types are convertable.
246    ///
247    /// Ignores specializations: specializations are handled in [Evaluator::subtype]
248    ///
249    /// On failure, returns a doc which describes the obstruction to convertability.
250    pub fn convertable_ty<'b>(&self, ty1: &TyV, ty2: &TyV) -> Result<(), D<'b>> {
251        match (&**ty1, &**ty2) {
252            (TyV_::Object(ot1), TyV_::Object(ot2)) => {
253                if ot1 == ot2 {
254                    Ok(())
255                } else {
256                    Err(t(format!("object types {ot1} and {ot2} are not equal")))
257                }
258            }
259            (TyV_::Morphism(mt1, dom1, cod1), TyV_::Morphism(mt2, dom2, cod2)) => {
260                if mt1 != mt2 {
261                    return Err(t(format!("morphism types {mt1} and {mt2} are not equal")));
262                }
263                self.equal_tm(dom1, dom2).map_err(|d| t("could not convert domains: ") + d)?;
264                self.equal_tm(cod1, cod2).map_err(|d| t("could not convert codomains: ") + d)?;
265                Ok(())
266            }
267            (TyV_::Record(r1), TyV_::Record(r2)) => {
268                if r1.fields0 != r2.fields0 {
269                    return Err(t("record types have unequal base types"));
270                }
271                let mut fields = IndexMap::new();
272                let mut self1 = self.clone();
273                for ((name, (label, field_ty1_s)), (_, (_, field_ty2_s))) in
274                    r1.fields1.iter().zip(r2.fields1.iter())
275                {
276                    let v = TmV::Cons(fields.clone().into());
277                    let field_ty1_v = self1.with_env(r1.env.snoc(v.clone())).eval_ty(field_ty1_s);
278                    let field_ty2_v = self1.with_env(r2.env.snoc(v.clone())).eval_ty(field_ty2_s);
279                    self1.convertable_ty(&field_ty1_v, &field_ty2_v)?;
280                    let (field_val, self_next) = self.bind_neu(*name, *label, field_ty1_v.clone());
281                    self1 = self_next;
282                    fields.insert(*name, (*label, TmV::Neu(field_val, field_ty1_v)));
283                }
284                Ok(())
285            }
286            (TyV_::Sing(ty1, _), _) => self.convertable_ty(ty1, ty2),
287            (_, TyV_::Sing(ty2, _)) => self.convertable_ty(ty1, ty2),
288            (TyV_::Unit, TyV_::Unit) => Ok(()),
289            _ => Err(t(
290                "tried to convert between types of different type constructors (for instance, object type and record type)",
291            )),
292        }
293    }
294
295    /// Performs eta-expansion of the neutral `n` at type `ty`.
296    pub fn eta_neu(&self, n: &TmN, ty: &TyV) -> TmV {
297        match &**ty {
298            TyV_::Object(_) => TmV::Neu(n.clone(), ty.clone()),
299            TyV_::Morphism(_, _, _) => TmV::Opaque,
300            TyV_::Record(r) => {
301                let mut fields = Row::empty();
302                for (name, (label, _)) in r.fields1.iter() {
303                    let ty_v = self.field_ty(ty, &TmV::Cons(fields.clone()), *name);
304                    let v = self.eta_neu(&TmN::proj(n.clone(), *name, *label), &ty_v);
305                    fields = fields.insert(*name, *label, v);
306                }
307                TmV::Cons(fields)
308            }
309            TyV_::Sing(_, x) => x.clone(),
310            TyV_::Unit => TmV::Tt,
311        }
312    }
313
314    /// Performs eta-expansion of the term `n` at type `ty`
315    pub fn eta(&self, v: &TmV, ty: &TyV) -> TmV {
316        match v {
317            TmV::Neu(tm_n, ty_v) => self.eta_neu(tm_n, ty_v),
318            TmV::Cons(row) => TmV::Cons(
319                row.iter()
320                    .map(|(name, (label, field_v))| {
321                        (*name, (*label, self.eta(field_v, &self.field_ty(ty, v, *name))))
322                    })
323                    .collect(),
324            ),
325            TmV::Tt => TmV::Tt,
326            TmV::Opaque => TmV::Opaque,
327        }
328    }
329
330    /// Check if two terms are definitionally equal.
331    ///
332    /// On failure, returns a doc which describes the obstruction to convertability.
333    ///
334    /// Assumes that the base type of tm1 is convertable with the base type of tm2.
335    /// First attempts to do conversion checking without eta-expansion (strict
336    /// mode), and if that fails, does conversion checking with eta-expansion.
337    pub fn equal_tm<'b>(&self, tm1: &TmV, tm2: &TmV) -> Result<(), D<'b>> {
338        if self.equal_tm_helper(tm1, tm2, true, true).is_err() {
339            self.equal_tm_helper(tm1, tm2, false, false)
340        } else {
341            Ok(())
342        }
343    }
344
345    fn equal_tm_helper<'b>(
346        &self,
347        tm1: &TmV,
348        tm2: &TmV,
349        strict1: bool,
350        strict2: bool,
351    ) -> Result<(), D<'b>> {
352        match (tm1, tm2) {
353            (TmV::Neu(n1, ty1), _) if !strict1 => {
354                self.equal_tm_helper(&self.eta_neu(n1, ty1), tm2, true, strict2)
355            }
356            (_, TmV::Neu(n2, ty2)) if !strict2 => {
357                self.equal_tm_helper(tm1, &self.eta_neu(n2, ty2), strict1, true)
358            }
359            (TmV::Neu(n1, _), TmV::Neu(n2, _)) => {
360                if n1 == n2 {
361                    Ok(())
362                } else {
363                    Err(t(format!(
364                        "Neutrals {} and {} are not equal.",
365                        self.quote_neu(n1),
366                        self.quote_neu(n2)
367                    )))
368                }
369            }
370            (TmV::Cons(fields1), TmV::Cons(fields2)) => {
371                for ((_, (_, tm1)), (_, (_, tm2))) in fields1.iter().zip(fields2.iter()) {
372                    self.equal_tm_helper(tm1, tm2, strict1, strict2)?
373                }
374                Ok(())
375            }
376            (TmV::Tt, TmV::Tt) => Ok(()),
377            (TmV::Opaque, TmV::Opaque) => Ok(()),
378            _ => Err(t(format!(
379                "failed to match terms {} and {}",
380                self.quote_tm(tm1),
381                self.quote_tm(tm2)
382            ))),
383        }
384    }
385
386    fn can_specialize(
387        &self,
388        ty: &TyV,
389        val: &TmV,
390        path: &[(FieldName, LabelSegment)],
391        field_ty: TyV,
392    ) -> Result<(), String> {
393        assert!(!path.is_empty());
394
395        let TyV_::Record(r) = &**ty else {
396            return Err("cannot specialize a non-record type".into());
397        };
398
399        let (field, path) = (path[0], &path[1..]);
400        if !r.fields1.has(field.0) {
401            return Err(format!("no such field .{}", field.1));
402        }
403        let orig_field_ty = self.field_ty(ty, val, field.0);
404        if path.is_empty() {
405            self.subtype(&field_ty, &orig_field_ty).map_err(|msg| {
406                format!(
407                    "{} is not a subtype of {}:\n... because {}",
408                    self.quote_ty(&field_ty),
409                    self.quote_ty(&orig_field_ty),
410                    msg.pretty()
411                )
412            })
413        } else {
414            self.can_specialize(&orig_field_ty, &self.proj(val, field.0, field.1), path, field_ty)
415        }
416    }
417
418    /// Try to specialize the record `r` with the subtype `ty` at `path`
419    ///
420    /// Precondition: `path` is non-empty.
421    pub fn try_specialize(
422        &self,
423        ty: &TyV,
424        path: &[(FieldName, LabelSegment)],
425        field_ty: TyV,
426    ) -> Result<TyV, String> {
427        let (self_var, _) = self.bind_self(ty.clone());
428        let self_val = self.eta_neu(&self_var, ty);
429        self.can_specialize(ty, &self_val, path, field_ty.clone())?;
430        let TyV_::Record(r) = &**ty else { panic!() };
431        Ok(TyV::record(r.add_specialization(path, field_ty)))
432    }
433}
catlog/tt/eval.rs

catlog/tt/
eval.rs
