catlog/tt/
text_elab.rs

1//! Elaboration for doublett
2use crate::{
3    dbl::{
4        category::VDblCategory,
5        theory::{DblTheory, DiscreteDblTheory},
6    },
7    zero::name,
8};
9use fnotation::*;
10use nonempty::nonempty;
11use scopeguard::{ScopeGuard, guard};
12use std::fmt::Write;
13
14use tattle::declare_error;
15
16use crate::{
17    tt::{context::*, eval::*, modelgen::*, prelude::*, stx::*, toplevel::*, val::*},
18    zero::QualifiedName,
19};
20
21/// The result of elaborating a top-level statement.
22pub enum TopElabResult {
23    /// A new declaration
24    Declaration(TopVarName, TopDecl),
25    /// Output that should be logged
26    Output(String),
27}
28
29/// Context for top-level elaboration
30///
31/// Top-level elaboration is elaboration of declarations.
32pub struct TopElaborator {
33    current_theory: Option<Theory>,
34    reporter: Reporter,
35}
36
37impl TopElaborator {
38    /// Constructor
39    pub fn new(reporter: Reporter) -> Self {
40        Self {
41            current_theory: None,
42            reporter,
43        }
44    }
45
46    fn bare_def<'c>(&self, n: &FNtn<'c>) -> Option<(TopVarName, &'c FNtn<'c>)> {
47        match n.ast0() {
48            App2(L(_, Keyword(":=")), L(_, Var(name)), tn) => {
49                Some((NameSegment::Text(ustr(name)), tn))
50            }
51            _ => None,
52        }
53    }
54
55    fn annotated_def<'c>(
56        &self,
57        n: &FNtn<'c>,
58    ) -> Option<(TopVarName, Option<&'c [&'c FNtn<'c>]>, &'c FNtn<'c>, &'c FNtn<'c>)> {
59        match n.ast0() {
60            App2(L(_, Keyword(":=")), L(_, App2(L(_, Keyword(":")), head_n, annotn)), valn) => {
61                match head_n.ast0() {
62                    App1(L(_, Var(name)), L(_, Tuple(args))) => {
63                        Some((name_seg(*name), Some(args.as_slice()), annotn, valn))
64                    }
65                    Var(name) => Some((name_seg(*name), None, annotn, valn)),
66                    _ => None,
67                }
68            }
69            _ => None,
70        }
71    }
72
73    fn expr_with_context<'c>(&self, n: &'c FNtn<'c>) -> (&'c [&'c FNtn<'c>], &'c FNtn<'c>) {
74        match n.ast0() {
75            App1(L(_, Tuple(ctx_elems)), n) => (ctx_elems.as_slice(), n),
76            _ => (&[], n),
77        }
78    }
79
80    fn get_theory(&self, loc: Loc) -> Option<Theory> {
81        let Some(theory) = &self.current_theory else {
82            return self.error(
83                loc,
84                "have not yet set a theory, set a theory via `set_theory <THEORY_NAME>`",
85            );
86        };
87        Some(theory.clone())
88    }
89
90    fn elaborator<'a>(&self, theory: &Theory, toplevel: &'a Toplevel) -> Elaborator<'a> {
91        Elaborator::new(theory.clone(), self.reporter.clone(), toplevel)
92    }
93
94    fn error<T>(&self, loc: Loc, msg: impl Into<String>) -> Option<T> {
95        self.reporter.error(loc, ELAB_ERROR, msg.into());
96        None
97    }
98
99    /// Elaborate a single top-level declaration
100    pub fn elab(&mut self, toplevel: &Toplevel, tn: &FNtnTop) -> Option<TopElabResult> {
101        match tn.name {
102            "set_theory" => match tn.body.ast0() {
103                Var(theory_name) => match toplevel.theory_library.get(&name(*theory_name)) {
104                    Some(theory) => {
105                        self.current_theory = Some(theory.clone());
106                        Some(TopElabResult::Output(format!("set theory to {}", theory_name)))
107                    }
108                    None => self.error(tn.loc, format!("{theory_name} not found")),
109                },
110                _ => self.error(tn.loc, "expected a theory name"),
111            },
112            "type" => {
113                let theory = self.get_theory(tn.loc)?;
114                let (name, ty_n) = self.bare_def(tn.body).or_else(|| {
115                    self.error(
116                        tn.loc,
117                        "unknown syntax for type declaration, expected <name> := <type>",
118                    )
119                })?;
120                let (ty_s, ty_v) = self.elaborator(&theory, toplevel).ty(ty_n)?;
121                Some(TopElabResult::Declaration(
122                    name,
123                    TopDecl::Type(Type::new(theory.clone(), ty_s, ty_v)),
124                ))
125            }
126            "def" => {
127                let theory = self.get_theory(tn.loc)?;
128                let (name, args_n, ty_n, tm_n) = self.annotated_def(tn.body).or_else(|| {
129                    self.error(
130                        tn.loc,
131                        "unknown syntax for term declaration, expected <name> : <type> := <term>",
132                    )
133                })?;
134                match args_n {
135                    Some(args_n) => {
136                        let mut elab = self.elaborator(&theory, toplevel);
137                        let mut args_stx = IndexMap::new();
138                        for arg_n in args_n {
139                            let (name, label, ty_s, ty_v) = elab.binding(arg_n)?;
140                            args_stx.insert(name, (label, ty_s));
141                            elab.intro(name, label, Some(ty_v));
142                        }
143                        let (ret_ty_s, ret_ty_v) = elab.ty(ty_n)?;
144                        let (body_s, _) = elab.chk(&ret_ty_v, tm_n)?;
145                        Some(TopElabResult::Declaration(
146                            name,
147                            TopDecl::Def(Def::new(
148                                theory.clone(),
149                                args_stx.into(),
150                                ret_ty_s,
151                                body_s,
152                            )),
153                        ))
154                    }
155                    None => {
156                        let mut elab = self.elaborator(&theory, toplevel);
157                        let (_, ty_v) = elab.ty(ty_n)?;
158                        let (tm_s, tm_v) = elab.chk(&ty_v, tm_n)?;
159                        Some(TopElabResult::Declaration(
160                            name,
161                            TopDecl::DefConst(DefConst::new(theory.clone(), tm_s, tm_v, ty_v)),
162                        ))
163                    }
164                }
165            }
166            "syn" => {
167                let theory = self.get_theory(tn.loc)?;
168                let (ctx_ns, n) = self.expr_with_context(tn.body);
169                let mut elab = self.elaborator(&theory, toplevel);
170                for ctx_n in ctx_ns {
171                    let (name, label, _, ty_v) = elab.binding(ctx_n)?;
172                    elab.intro(name, label, Some(ty_v));
173                }
174                let (tm_s, _, ty_v) = elab.syn(n)?;
175                Some(TopElabResult::Output(format!(
176                    "{tm_s} : {}",
177                    elab.evaluator().quote_ty(&ty_v)
178                )))
179            }
180            "norm" => {
181                let theory = self.get_theory(tn.loc)?;
182                let (ctx_ns, n) = self.expr_with_context(tn.body);
183                let mut elab = self.elaborator(&theory, toplevel);
184                for ctx_n in ctx_ns {
185                    let (name, label, _, ty_v) = elab.binding(ctx_n)?;
186                    elab.intro(name, label, Some(ty_v));
187                }
188                let (_, tm_v, ty_v) = elab.syn(n)?;
189                let eval = elab.evaluator();
190                Some(TopElabResult::Output(format!("{}", eval.quote_tm(&eval.eta(&tm_v, &ty_v)),)))
191            }
192            "chk" => {
193                let theory = self.get_theory(tn.loc)?;
194                let (ctx_ns, n) = self.expr_with_context(tn.body);
195                let mut elab = self.elaborator(&theory, toplevel);
196                for ctx_n in ctx_ns {
197                    let (name, label, _, ty_v) = elab.binding(ctx_n)?;
198                    elab.intro(name, label, Some(ty_v));
199                }
200                let (tm_n, ty_n) = match n.ast0() {
201                    App2(L(_, Keyword(":")), tm_n, ty_n) => (tm_n, ty_n),
202                    _ => return elab.error("expected <expr> : <type>"),
203                };
204                let (_, ty_v) = elab.ty(ty_n)?;
205                let (tm_s, _) = elab.chk(&ty_v, tm_n)?;
206                Some(TopElabResult::Output(format!("{tm_s}")))
207            }
208            "generate" => {
209                let theory = self.get_theory(tn.loc)?;
210                let mut elab = self.elaborator(&theory, toplevel);
211                let (_, ty_v) = elab.ty(tn.body)?;
212                let (model, name_translation) = generate(toplevel, &theory, &ty_v);
213                let mut out = String::new();
214                writeln!(&mut out).unwrap();
215                model_output("#/ ", &mut out, &model, &name_translation).unwrap();
216                Some(TopElabResult::Output(out))
217            }
218            _ => self.error(tn.loc, "unknown toplevel declaration"),
219        }
220    }
221}
222
223struct Elaborator<'a> {
224    theory: Theory,
225    reporter: Reporter,
226    toplevel: &'a Toplevel,
227    loc: Option<Loc>,
228    ctx: Context,
229}
230
231struct ElaboratorCheckpoint {
232    loc: Option<Loc>,
233    ctx: ContextCheckpoint,
234}
235
236declare_error!(ELAB_ERROR, "elab", "an error during elaboration");
237
238impl<'a> Elaborator<'a> {
239    fn new(theory: Theory, reporter: Reporter, toplevel: &'a Toplevel) -> Self {
240        Self {
241            theory,
242            reporter,
243            toplevel,
244            loc: None,
245            ctx: Context::new(),
246        }
247    }
248
249    fn dbl_theory(&self) -> &DiscreteDblTheory {
250        &self.theory.definition
251    }
252
253    fn checkpoint(&self) -> ElaboratorCheckpoint {
254        ElaboratorCheckpoint {
255            loc: self.loc,
256            ctx: self.ctx.checkpoint(),
257        }
258    }
259
260    fn reset_to(&mut self, c: ElaboratorCheckpoint) {
261        self.loc = c.loc;
262        self.ctx.reset_to(c.ctx);
263    }
264
265    fn enter<'c>(&'c mut self, loc: Loc) -> ScopeGuard<&'c mut Self, impl FnOnce(&'c mut Self)> {
266        let c = self.checkpoint();
267        self.loc = Some(loc);
268        guard(self, |e| {
269            e.reset_to(c);
270        })
271    }
272
273    fn error<T>(&self, msg: impl Into<String>) -> Option<T> {
274        self.reporter.error_option_loc(self.loc, ELAB_ERROR, msg.into());
275        None
276    }
277
278    fn evaluator(&self) -> Evaluator<'a> {
279        Evaluator::new(self.toplevel, self.ctx.env.clone(), self.ctx.scope.len())
280    }
281
282    fn intro(&mut self, name: VarName, label: LabelSegment, ty: Option<TyV>) -> TmV {
283        let v = TmV::Neu(
284            TmN::var(self.ctx.scope.len().into(), name, label),
285            ty.clone().unwrap_or(TyV::unit()),
286        );
287        let v = if let Some(ty) = &ty {
288            self.evaluator().eta(&v, ty)
289        } else {
290            v
291        };
292        self.ctx.env = self.ctx.env.snoc(v.clone());
293        self.ctx.push_scope(name, label, ty);
294        v
295    }
296
297    fn binding(&mut self, n: &FNtn) -> Option<(VarName, LabelSegment, TyS, TyV)> {
298        let mut elab = self.enter(n.loc());
299        match n.ast0() {
300            App2(L(_, Keyword(":")), L(_, Var(name)), ty_n) => {
301                let (ty_s, ty_v) = elab.ty(ty_n)?;
302                Some((name_seg(*name), label_seg(*name), ty_s, ty_v))
303            }
304            _ => elab.error("unexpected notation for binding"),
305        }
306    }
307
308    fn lookup_ty(&self, name: VarName) -> Option<(TyS, TyV)> {
309        let qname = QualifiedName::single(name);
310        if self.dbl_theory().has_ob(&qname) {
311            Some((TyS::object(qname.clone()), TyV::object(qname)))
312        } else if let Some(d) = self.toplevel.declarations.get(&name) {
313            match d {
314                TopDecl::Type(t) => {
315                    if t.theory == self.theory {
316                        Some((TyS::topvar(name), t.val.clone()))
317                    } else {
318                        self.error(format!(
319                            "{name} refers to a type in theory {}, expected a type in theory {}",
320                            t.theory, self.theory
321                        ))
322                    }
323                }
324                TopDecl::Def(_) | TopDecl::DefConst(_) => {
325                    self.error(format!("{name} refers to a term not a type"))
326                }
327            }
328        } else {
329            self.error(format!("no such type {name} defined"))
330        }
331    }
332
333    fn morphism_ty(&mut self, n: &FNtn) -> Option<(MorphismType, ObjectType, ObjectType)> {
334        let elab = self.enter(n.loc());
335        match n.ast0() {
336            App1(L(_, Keyword("Id")), L(_, Var(name))) => {
337                let qname = QualifiedName::single(name_seg(*name));
338                if elab.dbl_theory().has_ob(&qname) {
339                    Some((MorphismType(Path::Id(qname.clone())), qname.clone(), qname))
340                } else {
341                    elab.error(format!("no such object type {name}"))
342                }
343            }
344            Var(name) => {
345                let qname = QualifiedName::single(name_seg(*name));
346                let mt = Path::single(qname);
347                let theory = elab.dbl_theory();
348                if theory.has_proarrow(&mt) {
349                    let dom = theory.src(&mt);
350                    let cod = theory.tgt(&mt);
351                    Some((MorphismType(mt), dom, cod))
352                } else {
353                    elab.error(format!("no such morphism type {name}"))
354                }
355            }
356            _ => elab.error("unexpected notation for morphism type"),
357        }
358    }
359
360    fn path(&mut self, n: &FNtn) -> Option<Vec<(NameSegment, LabelSegment)>> {
361        let mut elab = self.enter(n.loc());
362        match n.ast0() {
363            Field(f) => Some(vec![(name_seg(*f), label_seg(*f))]),
364            App1(p_n, L(_, Field(f))) => {
365                let mut p = elab.path(p_n)?;
366                p.push((name_seg(*f), label_seg(*f)));
367                Some(p)
368            }
369            _ => elab.error("unexpected notation for path"),
370        }
371    }
372
373    #[allow(clippy::type_complexity)]
374    fn specialization(&mut self, n: &FNtn) -> Option<(Vec<(NameSegment, LabelSegment)>, TyS, TyV)> {
375        let mut elab = self.enter(n.loc());
376        match n.ast0() {
377            App2(L(_, Keyword(":")), p_n, ty_n) => {
378                let p = elab.path(p_n)?;
379                let (ty_s, ty_v) = elab.ty(ty_n)?;
380                Some((p, ty_s, ty_v))
381            }
382            App2(L(_, Keyword(":=")), p_n, tm_n) => {
383                let p = elab.path(p_n)?;
384                let (tm_s, tm_v, ty_v) = elab.syn(tm_n)?;
385                Some((p, TyS::sing(elab.evaluator().quote_ty(&ty_v), tm_s), TyV::sing(ty_v, tm_v)))
386            }
387            _ => elab.error("unexpected notation for specialization"),
388        }
389    }
390
391    fn ty(&mut self, n: &FNtn) -> Option<(TyS, TyV)> {
392        let mut elab = self.enter(n.loc());
393        match n.ast0() {
394            Var(name) => elab.lookup_ty(name_seg(*name)),
395            Keyword("Unit") => Some((TyS::unit(), TyV::unit())),
396            App1(L(_, Prim("sing")), tm_n) => {
397                let (tm_s, tm_v, ty_v) = elab.syn(tm_n)?;
398                Some((TyS::sing(elab.evaluator().quote_ty(&ty_v), tm_s), TyV::sing(ty_v, tm_v)))
399            }
400            App1(mt_n, L(_, Tuple(domcod_n))) => {
401                if domcod_n.len() != 2 {
402                    return elab.error("expected two arguments for morphism type");
403                }
404                let (mt, dom_ty, cod_ty) = elab.morphism_ty(mt_n)?;
405                let (dom_s, dom_v) = elab.chk(&TyV::object(dom_ty.clone()), domcod_n[0])?;
406                let (cod_s, cod_v) = elab.chk(&TyV::object(cod_ty.clone()), domcod_n[1])?;
407                Some((
408                    TyS::morphism(mt.clone(), dom_s, cod_s),
409                    TyV::morphism(mt.clone(), dom_v, cod_v),
410                ))
411            }
412            Tuple(field_ns) => {
413                let mut field_ty0s = Vec::<(FieldName, (LabelSegment, Ty0))>::new();
414                let mut field_ty_vs = Vec::<(FieldName, (LabelSegment, TyV))>::new();
415                let mut failed = false;
416                let self_var = elab.intro(name_seg("self"), label_seg("self"), None).as_neu();
417                let c = elab.checkpoint();
418                for field_n in field_ns.iter() {
419                    elab.loc = Some(field_n.loc());
420                    let Some((name, label, ty_n)) = (match field_n.ast0() {
421                        App2(L(_, Keyword(":")), L(_, Var(name)), ty_n) => {
422                            Some((name_seg(*name), label_seg(*name), ty_n))
423                        }
424                        _ => elab.error("expected fields in the form <name> : <type>"),
425                    }) else {
426                        println!("failed");
427                        failed = true;
428                        continue;
429                    };
430                    let Some((_, ty_v)) = elab.ty(ty_n) else {
431                        failed = true;
432                        continue;
433                    };
434                    field_ty0s.push((name, (label, ty_v.ty0())));
435                    field_ty_vs.push((name, (label, ty_v.clone())));
436                    elab.ctx.push_scope(name, label, Some(ty_v.clone()));
437                    elab.ctx.env =
438                        elab.ctx.env.snoc(TmV::Neu(TmN::proj(self_var.clone(), name, label), ty_v));
439                }
440                if failed {
441                    return None;
442                }
443                elab.reset_to(c);
444                let field_tys: Row<_> = field_ty_vs
445                    .iter()
446                    .map(|(name, (label, ty_v))| (*name, (*label, elab.evaluator().quote_ty(ty_v))))
447                    .collect();
448                let field_ty0s: Row<_> = field_ty0s.into_iter().collect();
449                let r_s = RecordS::new(field_ty0s.clone(), field_tys.clone());
450                let r_v = RecordV::new(field_ty0s, elab.ctx.env.clone(), field_tys, Dtry::empty());
451                Some((TyS::record(r_s), TyV::record(r_v)))
452            }
453            App2(L(_, Keyword("&")), ty_n, L(_, Tuple(specialization_ns))) => {
454                let (ty_s, mut ty_v) = elab.ty(ty_n)?;
455                let mut specializations = Vec::new();
456                // Approach:
457                //
458                // 1. Write a try_specialize method which attempts to specialize ty_v
459                // with a given path + type (e.g. `.x.y : @sing a`), returning a new
460                // type or an error message.
461                // 2. Iteratively apply try_specialize to each specialization in turn.
462                for specialization_n in specialization_ns.iter() {
463                    elab.loc = Some(specialization_n.loc());
464                    let (path, sty_s, sty_v) = elab.specialization(specialization_n)?;
465                    match elab.evaluator().try_specialize(&ty_v, &path, sty_v) {
466                        Ok(specialized) => {
467                            ty_v = specialized;
468                            specializations.push((path, sty_s));
469                        }
470                        Err(s) => {
471                            return elab.error(format!("Failed to specialize:\n... because {s}"));
472                        }
473                    }
474                }
475                Some((TyS::specialize(ty_s, specializations), ty_v))
476            }
477            _ => elab.error("unexpected notation for type"),
478        }
479    }
480
481    fn lookup_tm(&mut self, name: Ustr) -> Option<(TmS, TmV, TyV)> {
482        let label = label_seg(name);
483        let name = name_seg(name);
484        if let Some((i, _, ty)) = self.ctx.lookup(name) {
485            Some((
486                TmS::var(i, name, label),
487                self.ctx.env.get(*i).unwrap().clone(),
488                ty.clone().unwrap(),
489            ))
490        } else if let Some(d) = self.toplevel.lookup(name) {
491            match d {
492                TopDecl::Type(_) => self.error(format!("{name} refers type, not term")),
493                TopDecl::DefConst(d) => Some((TmS::topvar(name), d.val.clone(), d.ty.clone())),
494                TopDecl::Def(_) => self.error(format!("{name} must be applied to arguments")),
495            }
496        } else {
497            self.error(format!("no such variable {name}"))
498        }
499    }
500
501    fn syn(&mut self, n: &FNtn) -> Option<(TmS, TmV, TyV)> {
502        let mut elab = self.enter(n.loc());
503        match n.ast0() {
504            Var(name) => elab.lookup_tm(ustr(name)),
505            App1(tm_n, L(_, Field(f))) => {
506                let (tm_s, tm_v, ty_v) = elab.syn(tm_n)?;
507                let TyV_::Record(r) = &*ty_v else {
508                    return elab.error("can only project from record type");
509                };
510                let label = label_seg(*f);
511                let f = name_seg(*f);
512                if !r.fields1.has(f) {
513                    return elab.error(format!("no such field {f}"));
514                }
515                Some((
516                    TmS::proj(tm_s, f, label),
517                    elab.evaluator().proj(&tm_v, f, label),
518                    elab.evaluator().field_ty(&ty_v, &tm_v, f),
519                ))
520            }
521            App1(L(_, Prim("id")), ob_n) => {
522                let (ob_s, ob_v, ob_t) = elab.syn(ob_n)?;
523                let TyV_::Object(ot) = &*ob_t else {
524                    return elab.error("can only apply @id to objects");
525                };
526                Some((
527                    TmS::id(ob_s),
528                    TmV::Tt,
529                    TyV::morphism(MorphismType(Path::Id(ot.clone())), ob_v.clone(), ob_v),
530                ))
531            }
532            App2(L(_, Keyword("*")), f_n, g_n) => {
533                let (f_s, _, f_ty) = elab.syn(f_n)?;
534                let (g_s, _, g_ty) = elab.syn(g_n)?;
535                let TyV_::Morphism(f_mt, f_dom, f_cod) = &*f_ty else {
536                    elab.loc = Some(f_n.loc());
537                    return elab.error("expected a morphism");
538                };
539                let TyV_::Morphism(g_mt, g_dom, g_cod) = &*g_ty else {
540                    elab.loc = Some(g_n.loc());
541                    return elab.error("expected a morphism");
542                };
543                if elab.dbl_theory().tgt(&f_mt.0) != elab.dbl_theory().src(&g_mt.0) {
544                    return elab.error("incompatible morphism types");
545                }
546                if let Err(s) = elab.evaluator().equal_tm(f_cod, g_dom) {
547                    return elab.error(format!(
548                        "codomain {} and domain {} not equal:\n...because {}",
549                        elab.evaluator().quote_tm(f_cod),
550                        elab.evaluator().quote_tm(g_dom),
551                        s.pretty()
552                    ));
553                }
554                Some((
555                    TmS::compose(f_s, g_s),
556                    TmV::Tt,
557                    TyV::morphism(
558                        MorphismType(
559                            elab.dbl_theory()
560                                .compose_types(Path::Seq(nonempty![f_mt.0.clone(), g_mt.0.clone()]))
561                                .unwrap(),
562                        ),
563                        f_dom.clone(),
564                        g_cod.clone(),
565                    ),
566                ))
567            }
568            App1(L(_, Var(tv)), L(_, Tuple(args_n))) => {
569                let tv = name_seg(*tv);
570                let Some(TopDecl::Def(d)) = elab.toplevel.lookup(tv) else {
571                    return elab.error(format!("no such toplevel def {tv}"));
572                };
573                let mut arg_stxs = Vec::new();
574                let mut env = Env::nil();
575                if args_n.len() != d.args.len() {
576                    return elab.error(format!(
577                        "wrong number of args for {tv}, expected {}, got {}",
578                        d.args.len(),
579                        args_n.len()
580                    ));
581                }
582                for (arg_n, (_, (_, arg_ty_s))) in args_n.iter().zip(d.args.iter()) {
583                    let arg_ty_v = elab.evaluator().with_env(env.clone()).eval_ty(arg_ty_s);
584                    let (arg_s, arg_v) = elab.chk(&arg_ty_v, arg_n)?;
585                    arg_stxs.push(arg_s);
586                    env = env.snoc(arg_v);
587                }
588                let eval = elab.evaluator().with_env(env.clone());
589                Some((TmS::topapp(tv, arg_stxs), eval.eval_tm(&d.body), eval.eval_ty(&d.ret_ty)))
590            }
591            Tag("tt") => Some((TmS::tt(), TmV::Tt, TyV::unit())),
592            Tuple(_) => elab.error("must check agains a type in order to construct a record"),
593            _ => elab.error("unexpected notation for term"),
594        }
595    }
596
597    fn chk(&mut self, ty: &TyV, n: &FNtn) -> Option<(TmS, TmV)> {
598        let mut elab = self.enter(n.loc());
599        match n.ast0() {
600            Tuple(field_ns) => {
601                let TyV_::Record(r) = &**ty else {
602                    return elab.error("must check record former against record type");
603                };
604                if r.fields1.len() != field_ns.len() {
605                    return elab.error(format!(
606                        "wrong number of fields provided, expected {}, got {}",
607                        r.fields1.len(),
608                        r.fields0.len(),
609                    ));
610                }
611                let mut field_stxs = IndexMap::new();
612                let mut field_vals = IndexMap::new();
613                for (field_n, (name, (label, field_ty_s))) in field_ns.iter().zip(r.fields1.iter())
614                {
615                    elab.loc = Some(field_n.loc());
616                    let tm_n = match field_n.ast0() {
617                        App2(L(_, Keyword(":=")), L(_, Var(given_name)), field_val_n) => {
618                            if name_seg(*given_name) == *name {
619                                field_val_n
620                            } else {
621                                return elab.error(format!("unexpected field {given_name}"));
622                            }
623                        }
624                        _ => {
625                            return elab.error("unexpected notation for field");
626                        }
627                    };
628                    let v = TmV::Cons(field_vals.clone().into());
629                    let field_ty_v =
630                        elab.evaluator().with_env(r.env.snoc(v.clone())).eval_ty(field_ty_s);
631                    let (tm_s, tm_v) = elab.chk(&field_ty_v, tm_n)?;
632                    field_stxs.insert(*name, (*label, tm_s));
633                    field_vals.insert(*name, (*label, tm_v));
634                }
635                Some((TmS::cons(field_stxs.into()), TmV::Cons(field_vals.into())))
636            }
637            _ => {
638                let (tm_s, tm_v, synthed) = elab.syn(n)?;
639                let eval = elab.evaluator();
640                if let Err(e) = eval.convertable_ty(&synthed, ty) {
641                    return elab.error(format!(
642                        "synthesized type {} does not match expected type {}:\n{}",
643                        eval.quote_ty(&synthed),
644                        eval.quote_ty(ty),
645                        e.pretty()
646                    ));
647                }
648                if let Err(e) = eval.element_of(&tm_v, ty) {
649                    return elab.error(format!(
650                        "evaluated term {} is not an element of specialized type {}:\n{}",
651                        eval.quote_tm(&tm_v),
652                        eval.quote_ty(ty),
653                        e.pretty()
654                    ));
655                }
656                Some((tm_s, tm_v))
657            }
658        }
659    }
660}
catlog/tt/text_elab.rs

catlog/tt/
text_elab.rs
