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//! - `convertible? : value -> value -> bool` ([Evaluator::equal_tm], [Evaluator::element_of], [Evaluator::subtype])
8
9use derive_more::Constructor;
10
11use crate::{
12    tt::{prelude::*, stx::*, toplevel::*, val::*},
13    zero::LabelSegment,
14};
15
16/// The context used in evaluation, quoting, and conversion checking.
17///
18/// We bundle this all together because conversion checking and quoting
19/// sometimes need to evaluate terms. For instance, quoting a lambda
20/// involves evaluating the body of the lambda in the context of a freshly
21/// introduced variable; even though we don't have lambdas, a similar
22/// point applies to dependent records.
23#[derive(Constructor, Clone)]
24pub struct Evaluator<'a> {
25    toplevel: &'a Toplevel,
26    env: Env,
27    // The next neutral
28    scope_length: usize,
29}
30
31impl<'a> Evaluator<'a> {
32    /// Constructs a new [Evaluator] with empty environment.
33    pub fn empty(toplevel: &'a Toplevel) -> Self {
34        Self::new(toplevel, Env::Nil, 0)
35    }
36
37    /// Return a new [Evaluator] with environment `env`.
38    pub fn with_env(&self, env: Env) -> Self {
39        Self { env, ..self.clone() }
40    }
41
42    fn eval_record(&self, fields: &Row<BaseTyS>) -> RecordV {
43        RecordV::new(self.env.clone(), fields.clone(), Dtry::empty())
44    }
45
46    /// Evaluate type syntax to produce a type value.
47    ///
48    /// Assumes that the type syntax is well-formed and well-scoped with respect
49    /// to self.env.
50    pub fn eval_ty(&self, ty: &BaseTyS) -> BaseTyV {
51        match &**ty {
52            BaseTyS_::TopVar(tv) => match self.toplevel.declarations.get(tv).unwrap() {
53                TopDecl::Type(t) => t.val.clone(),
54                _ => panic!("top-level {tv} should be a type declaration"),
55            },
56            BaseTyS_::Object(ot) => BaseTyV::object(ot.clone()),
57            BaseTyS_::Morphism(pt, dom, cod) => {
58                BaseTyV::morphism(pt.clone(), self.eval_tm(dom), self.eval_tm(cod))
59            }
60            BaseTyS_::Record(r) => BaseTyV::record(self.eval_record(r)),
61            BaseTyS_::Sing(ty_s, tm_s) => BaseTyV::sing(self.eval_ty(ty_s), self.eval_tm(tm_s)),
62            BaseTyS_::Id(ty_s, tm_s1, tm_s2) => {
63                BaseTyV::id(self.eval_ty(ty_s), self.eval_tm(tm_s1), self.eval_tm(tm_s2))
64            }
65            BaseTyS_::Specialize(ty_s, specializations) => {
66                specializations.iter().fold(self.eval_ty(ty_s), |ty_v, (path, s)| {
67                    ty_v.add_specialization(path, self.eval_ty(s))
68                })
69            }
70            BaseTyS_::Meta(mv) => BaseTyV::meta(*mv),
71        }
72    }
73
74    /// Evaluate term syntax to produce a term value.
75    ///
76    /// Assumes that the term syntax is well-formed and well-scoped with respect
77    /// to self.env.
78    pub fn eval_tm(&self, tm: &BaseTmS) -> BaseTmV {
79        match &**tm {
80            BaseTmS_::TopApp(tv, args_s) => {
81                let env = Env::nil().extend_by(args_s.iter().map(|arg_s| self.eval_tm(arg_s)));
82                let def = self.toplevel.declarations.get(tv).unwrap().clone().unwrap_def();
83                self.with_env(env).eval_tm(&def.body)
84            }
85            BaseTmS_::Var(i, _, _) => self.env.get(**i).cloned().unwrap(),
86            BaseTmS_::Cons(fields) => BaseTmV::cons(fields.map(|tm| self.eval_tm(tm))),
87            BaseTmS_::Proj(tm, field, label) => self.proj(&self.eval_tm(tm), *field, *label),
88            BaseTmS_::Id(x) => BaseTmV::id(self.eval_tm(x)),
89            BaseTmS_::Tab(mor) => BaseTmV::tab(self.eval_tm(mor)),
90            BaseTmS_::Compose(f, g) => BaseTmV::compose(self.eval_tm(f), self.eval_tm(g)),
91            BaseTmS_::ObApp(name, x) => BaseTmV::app(*name, self.eval_tm(x)),
92            BaseTmS_::List(elems) => {
93                BaseTmV::list(elems.iter().map(|tm| self.eval_tm(tm)).collect())
94            }
95            BaseTmS_::Meta(mv) => BaseTmV::meta(*mv),
96        }
97    }
98
99    /// Compute the projection of a field from a term value.
100    pub fn proj(&self, tm: &BaseTmV, field_name: FieldName, field_label: LabelSegment) -> BaseTmV {
101        match &**tm {
102            BaseTmV_::Neu(n, ty) => BaseTmV::neu(
103                TmN::proj(n.clone(), field_name, field_label),
104                self.field_ty(ty, tm, field_name),
105            ),
106            BaseTmV_::Cons(fields) => fields.get(field_name).cloned().unwrap(),
107            _ => unreachable!("projected field {field_name} from a non-record term value"),
108        }
109    }
110
111    /// Evaluate the type of the field `field_name` of `val : ty`.
112    pub fn field_ty(&self, ty: &BaseTyV, val: &BaseTmV, field_name: FieldName) -> BaseTyV {
113        match &**ty {
114            BaseTyV_::Record(r) => {
115                let field_ty_s = r.fields.get(field_name).unwrap();
116                let orig_field_ty = self.with_env(r.env.snoc(val.clone())).eval_ty(field_ty_s);
117                match r.specializations.entry(&field_name) {
118                    Some(DtryEntry::File(ty)) => ty.clone(),
119                    Some(DtryEntry::SubDir(d)) => orig_field_ty.specialize(d),
120                    Option::None => orig_field_ty,
121                }
122            }
123            _ => panic!("tried to get the type of field for non-record type"),
124        }
125    }
126
127    /// Bind a new neutral of type `ty`.
128    pub fn bind_neu(&self, name: VarName, label: LabelSegment, ty: BaseTyV) -> (TmN, Self) {
129        let n = TmN::var(self.scope_length.into(), name, label);
130        let v = BaseTmV::neu(n.clone(), ty);
131        (
132            n,
133            Self {
134                env: self.env.snoc(v),
135                scope_length: self.scope_length + 1,
136                ..self.clone()
137            },
138        )
139    }
140
141    /// Bind a variable called "self" to `ty`.
142    pub fn bind_self(&self, ty: BaseTyV) -> (TmN, Self) {
143        self.bind_neu("self".into(), "self".into(), ty)
144    }
145
146    /// Produce type syntax from a type value.
147    ///
148    /// This is a *section* of eval, in that `self.eval_ty(self.quote_ty(ty_v)) == ty_v`
149    /// but it is not necessarily true that `self.quote_ty(self.eval_ty(ty_s)) == ty_v`.
150    ///
151    /// This is used for displaying [BaseTyV] to the user in type errors, and for
152    /// creating syntax that can be re-evaluated in other contexts. In theory this
153    /// could be used for conversion checking, but it's more efficient to implement
154    /// that directly, and it's better to *not* do eta-expansion for user-facing
155    /// messages or for syntax that is meant to be re-evaluated.
156    pub fn quote_ty(&self, ty: &BaseTyV) -> BaseTyS {
157        match &**ty {
158            BaseTyV_::Object(object_type) => BaseTyS::object(object_type.clone()),
159            BaseTyV_::Morphism(morphism_type, dom, cod) => {
160                BaseTyS::morphism(morphism_type.clone(), self.quote_tm(dom), self.quote_tm(cod))
161            }
162            BaseTyV_::Record(r) => {
163                let r_eval = self.with_env(r.env.clone()).bind_self(ty.clone()).1;
164                let fields = r
165                    .fields
166                    .map(|ty_s| self.bind_self(ty.clone()).1.quote_ty(&r_eval.eval_ty(ty_s)));
167                let record_ty_s = BaseTyS::record(fields);
168                if r.specializations.is_empty() {
169                    record_ty_s
170                } else {
171                    BaseTyS::specialize(
172                        record_ty_s,
173                        r.specializations
174                            .flatten()
175                            .into_iter()
176                            .map(|(name, label, ty_v)| {
177                                (
178                                    name.segments()
179                                        .copied()
180                                        .zip(label.segments().copied())
181                                        .collect::<Vec<_>>(),
182                                    self.quote_ty(&ty_v),
183                                )
184                            })
185                            .collect(),
186                    )
187                }
188            }
189            BaseTyV_::Sing(ty, tm) => BaseTyS::sing(self.quote_ty(ty), self.quote_tm(tm)),
190            BaseTyV_::Id(ty, tm1, tm2) => {
191                BaseTyS::id(self.quote_ty(ty), self.quote_tm(tm1), self.quote_tm(tm2))
192            }
193            BaseTyV_::Meta(mv) => BaseTyS::meta(*mv),
194        }
195    }
196
197    /// Produce term syntax from a neutral term.
198    ///
199    /// The documentation for [Evaluator::quote_ty] is also applicable here.
200    pub fn quote_neu(&self, n: &TmN) -> BaseTmS {
201        match &**n {
202            TmN_::Var(i, name, label) => BaseTmS::var(i.as_bwd(self.scope_length), *name, *label),
203            TmN_::Proj(tm, field, label) => BaseTmS::proj(self.quote_neu(tm), *field, *label),
204        }
205    }
206
207    /// Produce term syntax from a term value.
208    ///
209    /// The documentation for [Evaluator::quote_ty] is also applicable here.
210    pub fn quote_tm(&self, tm: &BaseTmV) -> BaseTmS {
211        match &**tm {
212            BaseTmV_::Neu(n, _) => self.quote_neu(n),
213            BaseTmV_::App(name, x) => BaseTmS::ob_app(*name, self.quote_tm(x)),
214            BaseTmV_::List(elems) => {
215                BaseTmS::list(elems.iter().map(|tm| self.quote_tm(tm)).collect())
216            }
217            BaseTmV_::Cons(fields) => BaseTmS::cons(fields.map(|tm| self.quote_tm(tm))),
218            BaseTmV_::Id(x) => BaseTmS::id(self.quote_tm(x)),
219            BaseTmV_::Tab(mor) => BaseTmS::tab(self.quote_tm(mor)),
220            BaseTmV_::Compose(f, g) => BaseTmS::compose(self.quote_tm(f), self.quote_tm(g)),
221            BaseTmV_::Meta(mv) => BaseTmS::meta(*mv),
222        }
223    }
224
225    /// Check if `ty1` is a subtype of `ty2`.
226    ///
227    /// This is true iff `ty1` is convertible with `ty2`, and an eta-expanded
228    /// neutral of type `ty1` is an element of `ty2`.
229    pub fn subtype<'b>(&self, ty1: &BaseTyV, ty2: &BaseTyV) -> Result<(), D<'b>> {
230        self.convertible_ty(ty1, ty2)?;
231        let (n, _) = self.bind_self(ty1.clone());
232        let v = self.eta_neu(&n, ty1);
233        self.element_of(&v, ty2)
234    }
235
236    /// Check if `tm` is an element of `ty`, accounting for specializations
237    /// of `ty`.
238    ///
239    /// Precondition: the type of `tm` must be convertible with `ty`, and `tm`
240    /// is eta-expanded.
241    ///
242    /// Example: if `a : Entity` and `b : Entity` are neutrals, then `a` is not an
243    /// element of `@sing b`, but `a` is an element of `@sing a`.
244    pub fn element_of<'b>(&self, tm: &BaseTmV, ty: &BaseTyV) -> Result<(), D<'b>> {
245        match &**ty {
246            BaseTyV_::Object(_) => Ok(()),
247            BaseTyV_::Morphism(_, _, _) => Ok(()),
248            BaseTyV_::Record(r) => {
249                for (name, (label, _)) in r.fields.iter() {
250                    self.element_of(&self.proj(tm, *name, *label), &self.field_ty(ty, tm, *name))?
251                }
252                Ok(())
253            }
254            BaseTyV_::Sing(_, x) => self.equal_tm(tm, x),
255            BaseTyV_::Id(_, _, _) => Ok(()),
256            BaseTyV_::Meta(_) => Ok(()),
257        }
258    }
259
260    /// Check if two types are convertible.
261    ///
262    /// Ignores specializations: specializations are handled in [`Evaluator::subtype`].
263    ///
264    /// On failure, returns a doc which describes the obstruction to convertibility.
265    pub fn convertible_ty<'b>(&self, ty1: &BaseTyV, ty2: &BaseTyV) -> Result<(), D<'b>> {
266        match (&**ty1, &**ty2) {
267            (BaseTyV_::Object(ot1), BaseTyV_::Object(ot2)) => {
268                if ot1 == ot2 {
269                    Ok(())
270                } else {
271                    Err(t(format!("object types {ot1} and {ot2} are not equal")))
272                }
273            }
274            (BaseTyV_::Morphism(mt1, dom1, cod1), BaseTyV_::Morphism(mt2, dom2, cod2)) => {
275                if mt1 != mt2 {
276                    return Err(t(format!("morphism types {mt1} and {mt2} are not equal")));
277                }
278                self.equal_tm(dom1, dom2).map_err(|d| t("could not convert domains: ") + d)?;
279                self.equal_tm(cod1, cod2).map_err(|d| t("could not convert codomains: ") + d)?;
280                Ok(())
281            }
282            (BaseTyV_::Record(r1), BaseTyV_::Record(r2)) => {
283                let mut fields = IndexMap::new();
284                let mut self1 = self.clone();
285                for ((name, (label, field_ty1_s)), (_, (_, field_ty2_s))) in
286                    r1.fields.iter().zip(r2.fields.iter())
287                {
288                    let v = BaseTmV::cons(fields.clone().into());
289                    let field_ty1_v = self1.with_env(r1.env.snoc(v.clone())).eval_ty(field_ty1_s);
290                    let field_ty2_v = self1.with_env(r2.env.snoc(v.clone())).eval_ty(field_ty2_s);
291                    self1.convertible_ty(&field_ty1_v, &field_ty2_v)?;
292                    let (field_val, self_next) = self.bind_neu(*name, *label, field_ty1_v.clone());
293                    self1 = self_next;
294                    fields.insert(*name, (*label, BaseTmV::neu(field_val, field_ty1_v)));
295                }
296                Ok(())
297            }
298            (BaseTyV_::Sing(ty1, _), _) => self.convertible_ty(ty1, ty2),
299            (_, BaseTyV_::Sing(ty2, _)) => self.convertible_ty(ty1, ty2),
300            _ => Err(t("tried to convert between types of different type constructors")),
301        }
302    }
303
304    /// Performs eta-expansion of the neutral `n` at type `ty`.
305    pub fn eta_neu(&self, n: &TmN, ty: &BaseTyV) -> BaseTmV {
306        match &**ty {
307            BaseTyV_::Object(_) => BaseTmV::neu(n.clone(), ty.clone()),
308            BaseTyV_::Morphism(_, _, _) => BaseTmV::neu(n.clone(), ty.clone()),
309            BaseTyV_::Record(r) => {
310                let mut fields = Row::empty();
311                for (name, (label, _)) in r.fields.iter() {
312                    let ty_v = self.field_ty(ty, &BaseTmV::cons(fields.clone()), *name);
313                    let v = self.eta_neu(&TmN::proj(n.clone(), *name, *label), &ty_v);
314                    fields.insert(*name, *label, v);
315                }
316                BaseTmV::cons(fields)
317            }
318            BaseTyV_::Sing(_, x) => x.clone(),
319            BaseTyV_::Id(_, _, _) => BaseTmV::empty_cons(), /* Extensional equality at a 100% discount! */
320            BaseTyV_::Meta(_) => BaseTmV::neu(n.clone(), ty.clone()),
321        }
322    }
323
324    /// Performs eta-expansion of the term `v` at type `ty`.
325    pub fn eta(&self, v: &BaseTmV, ty: Option<&BaseTyV>) -> BaseTmV {
326        match &**v {
327            BaseTmV_::Neu(tm_n, ty_v) => self.eta_neu(tm_n, ty_v),
328            BaseTmV_::App(name, x) => BaseTmV::app(*name, self.eta(x, None)),
329            BaseTmV_::List(elems) => {
330                BaseTmV::list(elems.iter().map(|elem| self.eta(elem, None)).collect())
331            }
332            BaseTmV_::Cons(row) => {
333                if let Some(ty) = ty {
334                    let row = row
335                        .iter()
336                        .map(|(name, (label, field_v))| {
337                            (*name, (*label, self.eta(field_v, Some(&self.field_ty(ty, v, *name)))))
338                        })
339                        .collect();
340                    BaseTmV::cons(row)
341                }
342                // Is this right? Couldn't a cons be nested below top-level and so not get expanded right?
343                else {
344                    v.clone()
345                }
346            }
347            BaseTmV_::Id(x) => BaseTmV::id(self.eta(x, None)),
348            BaseTmV_::Tab(mor) => BaseTmV::tab(self.eta(mor, None)),
349            BaseTmV_::Compose(f, g) => BaseTmV::compose(self.eta(f, None), self.eta(g, None)),
350            BaseTmV_::Meta(_) => v.clone(),
351        }
352    }
353
354    /// Check if two terms are definitionally equal.
355    ///
356    /// On failure, returns a doc which describes the obstruction to convertibility.
357    ///
358    /// Assumes that the type of tm1 is convertible with the type of tm2. First
359    /// attempts to do conversion checking without eta-expansion (strict mode),
360    /// and if that fails, does conversion checking with eta-expansion.
361    pub fn equal_tm<'b>(&self, tm1: &BaseTmV, tm2: &BaseTmV) -> Result<(), D<'b>> {
362        if self.equal_tm_helper(tm1, tm2, true, true).is_err() {
363            self.equal_tm_helper(tm1, tm2, false, false)
364        } else {
365            Ok(())
366        }
367    }
368
369    fn equal_tm_helper<'b>(
370        &self,
371        tm1: &BaseTmV,
372        tm2: &BaseTmV,
373        strict1: bool,
374        strict2: bool,
375    ) -> Result<(), D<'b>> {
376        match (&**tm1, &**tm2) {
377            (BaseTmV_::Neu(n1, ty1), _) if !strict1 => {
378                self.equal_tm_helper(&self.eta_neu(n1, ty1), tm2, true, strict2)
379            }
380            (_, BaseTmV_::Neu(n2, ty2)) if !strict2 => {
381                self.equal_tm_helper(tm1, &self.eta_neu(n2, ty2), strict1, true)
382            }
383            (BaseTmV_::Neu(n1, _), BaseTmV_::Neu(n2, _)) => {
384                if n1 == n2 {
385                    Ok(())
386                } else {
387                    Err(t(format!(
388                        "Neutrals {} and {} are not equal.",
389                        self.quote_neu(n1),
390                        self.quote_neu(n2)
391                    )))
392                }
393            }
394            (BaseTmV_::Cons(fields1), BaseTmV_::Cons(fields2)) => {
395                for ((_, (_, tm1)), (_, (_, tm2))) in fields1.iter().zip(fields2.iter()) {
396                    self.equal_tm_helper(tm1, tm2, strict1, strict2)?
397                }
398                Ok(())
399            }
400            (BaseTmV_::Meta(mv1), BaseTmV_::Meta(mv2)) => {
401                if mv1 == mv2 {
402                    Ok(())
403                } else {
404                    Err(t(format!("Holes {} and {} are not equal.", mv1, mv2)))
405                }
406            }
407            (BaseTmV_::Id(x1), BaseTmV_::Id(x2)) => self.equal_tm_helper(x1, x2, strict1, strict2),
408            (BaseTmV_::Compose(f1, g1), BaseTmV_::Compose(f2, g2)) => {
409                self.equal_tm_helper(f1, f2, strict1, strict2)?;
410                self.equal_tm_helper(g1, g2, strict1, strict2)
411            }
412            (BaseTmV_::Tab(mor1), BaseTmV_::Tab(mor2)) => {
413                self.equal_tm_helper(mor1, mor2, strict1, strict2)
414            }
415            (BaseTmV_::List(es1), BaseTmV_::List(es2)) => {
416                if es1.len() != es2.len() {
417                    return Err(t("lists have different lengths"));
418                }
419                for (e1, e2) in es1.iter().zip(es2.iter()) {
420                    self.equal_tm_helper(e1, e2, strict1, strict2)?;
421                }
422                Ok(())
423            }
424            (BaseTmV_::App(n1, a1), BaseTmV_::App(n2, a2)) => {
425                if n1 != n2 {
426                    return Err(t(format!("object operations {n1} and {n2} are not equal")));
427                }
428                self.equal_tm_helper(a1, a2, strict1, strict2)
429            }
430            // Constructor mismatch. Enumerating the left term's variants
431            // (rather than `_`) keeps this exhaustive, so a new `BaseTmV_`
432            // variant fails to compile here until its equality is defined.
433            (
434                BaseTmV_::Neu(_, _)
435                | BaseTmV_::App(_, _)
436                | BaseTmV_::List(_)
437                | BaseTmV_::Cons(_)
438                | BaseTmV_::Id(_)
439                | BaseTmV_::Tab(_)
440                | BaseTmV_::Compose(_, _)
441                | BaseTmV_::Meta(_),
442                _,
443            ) => Err(t(format!(
444                "failed to match terms {} and {}",
445                self.quote_tm(tm1),
446                self.quote_tm(tm2)
447            ))),
448        }
449    }
450
451    fn can_specialize(
452        &self,
453        ty: &BaseTyV,
454        val: &BaseTmV,
455        path: &[(FieldName, LabelSegment)],
456        field_ty: BaseTyV,
457    ) -> Result<(), String> {
458        assert!(!path.is_empty());
459        let orig_field_ty = self.path_ty(ty, val, path)?;
460        self.subtype(&field_ty, &orig_field_ty).map_err(|msg| {
461            format!(
462                "{} is not a subtype of {}:\n... because {}",
463                self.quote_ty(&field_ty),
464                self.quote_ty(&orig_field_ty),
465                msg.pretty()
466            )
467        })
468    }
469
470    /// Walk `path` from the value `val` of record type `ty`, returning
471    /// the type of the field at the end of the path.
472    ///
473    /// An empty path returns `ty` unchanged. Each segment requires the
474    /// current type to be a record containing the named field.
475    pub fn path_ty(
476        &self,
477        ty: &BaseTyV,
478        val: &BaseTmV,
479        path: &[(FieldName, LabelSegment)],
480    ) -> Result<BaseTyV, String> {
481        let mut ty = ty.clone();
482        let mut val = val.clone();
483        for &(name, label) in path {
484            let BaseTyV_::Record(r) = &*ty.clone() else {
485                return Err(format!("expected a record type at .{label}"));
486            };
487            if !r.fields.has(name) {
488                return Err(format!("no such field .{label}"));
489            }
490            let next_ty = self.field_ty(&ty, &val, name);
491            let next_val = self.proj(&val, name, label);
492            ty = next_ty;
493            val = next_val;
494        }
495        Ok(ty)
496    }
497
498    /// Try to specialize the record `r` with the subtype `ty` at `path`.
499    ///
500    /// Precondition: `path` is non-empty.
501    pub fn try_specialize(
502        &self,
503        ty: &BaseTyV,
504        path: &[(FieldName, LabelSegment)],
505        field_ty: BaseTyV,
506    ) -> Result<BaseTyV, String> {
507        let (self_var, _) = self.bind_self(ty.clone());
508        let self_val = self.eta_neu(&self_var, ty);
509        self.can_specialize(ty, &self_val, path, field_ty.clone())?;
510        let BaseTyV_::Record(r) = &**ty else {
511            panic!("Input to `try_specialize` should be a record type")
512        };
513        Ok(BaseTyV::record(r.add_specialization(path, field_ty)))
514    }
515
516    // --- Fiber-world NbE and conversion ---------------------------------
517    //
518    // Fiber types/terms carry no closures or computation rules (every
519    // fiber term is neutral), so there is no fiber eval/quote: the
520    // elaborator builds [`FiberTyS`]/[`FiberTyV`] (and the term sorts) in
521    // parallel. What remains is conversion checking and field projection.
522
523    /// The fiber type of field `field` of a fiber record type, if present.
524    ///
525    /// Only [`Over`](FiberTyV_::Over) generator fields are ever projected
526    /// (as `we.e`); their types are closed, so this is a plain lookup with
527    /// no environment.
528    pub fn fiber_field_ty(&self, ty: &FiberTyV, field: FieldName) -> Option<FiberTyV> {
529        match &**ty {
530            FiberTyV_::Record(r) => r.get(field).cloned(),
531            _ => None,
532        }
533    }
534
535    /// Check that two fiber types are convertible.
536    pub fn convertible_fiber_ty<'b>(&self, ty1: &FiberTyV, ty2: &FiberTyV) -> Result<(), D<'b>> {
537        match (&**ty1, &**ty2) {
538            (FiberTyV_::Over(o1), FiberTyV_::Over(o2)) => self
539                .equal_tm(o1, o2)
540                .map_err(|d| t("over-types lie over different codomain objects: ") + d),
541            (FiberTyV_::Record(r1), FiberTyV_::Record(r2)) => {
542                if r1.iter().count() != r2.iter().count() {
543                    return Err(t("instance records have differing shapes"));
544                }
545                for ((n1, (_, f1)), (n2, (_, f2))) in r1.iter().zip(r2.iter()) {
546                    if n1 != n2 {
547                        return Err(t(format!("instance field {n1} differs from {n2}")));
548                    }
549                    self.convertible_fiber_ty(f1, f2)?;
550                }
551                Ok(())
552            }
553            (FiberTyV_::Id(ty1, l1, r1), FiberTyV_::Id(ty2, l2, r2)) => {
554                self.convertible_fiber_ty(ty1, ty2)?;
555                self.equal_fiber_tm(l1, l2)?;
556                self.equal_fiber_tm(r1, r2)
557            }
558            _ => Err(t("tried to convert between fiber types of different constructors")),
559        }
560    }
561
562    /// Check that two fiber terms are equal. Fiber terms are all neutral,
563    /// so this is structural.
564    pub fn equal_fiber_tm<'b>(&self, tm1: &FiberTmV, tm2: &FiberTmV) -> Result<(), D<'b>> {
565        match (&**tm1, &**tm2) {
566            (FiberTmV_::Var(i1, _, _), FiberTmV_::Var(i2, _, _)) => {
567                if i1 == i2 {
568                    Ok(())
569                } else {
570                    Err(t("fiber variables are not equal"))
571                }
572            }
573            (FiberTmV_::Proj(t1, f1, _), FiberTmV_::Proj(t2, f2, _)) => {
574                if f1 != f2 {
575                    return Err(t(format!("fiber projections {f1} and {f2} are not equal")));
576                }
577                self.equal_fiber_tm(t1, t2)
578            }
579            (FiberTmV_::List(es1), FiberTmV_::List(es2)) => {
580                if es1.len() != es2.len() {
581                    return Err(t("fiber lists have different lengths"));
582                }
583                for (e1, e2) in es1.iter().zip(es2.iter()) {
584                    self.equal_fiber_tm(e1, e2)?;
585                }
586                Ok(())
587            }
588            (FiberTmV_::ObApp(n1, a1), FiberTmV_::ObApp(n2, a2)) => {
589                if n1 != n2 {
590                    return Err(t(format!("object operations {n1} and {n2} are not equal")));
591                }
592                self.equal_fiber_tm(a1, a2)
593            }
594            (FiberTmV_::OverApp(p1, _, i1), FiberTmV_::OverApp(p2, _, i2)) => {
595                // Compare the morphism paths by name.
596                let names1 = p1.iter().map(|(n, _)| n).collect::<Vec<_>>();
597                let names2 = p2.iter().map(|(n, _)| n).collect::<Vec<_>>();
598                if names1 != names2 {
599                    return Err(t("applied codomain morphisms are not equal"));
600                }
601                self.equal_fiber_tm(i1, i2)
602            }
603            (FiberTmV_::Meta(a), FiberTmV_::Meta(b)) => {
604                if a == b {
605                    Ok(())
606                } else {
607                    Err(t(format!("Holes {a} and {b} are not equal.")))
608                }
609            }
610            _ => Err(t("fiber terms are not equal")),
611        }
612    }
613}
catlog/tt/eval.rs

catlog/tt/
eval.rs
