dada_ir_sym/check/
places.rs

1use dada_ir_ast::diagnostic::Err;
2use dada_util::boxed_async_fn;
3
4use crate::{
5    check::env::Env,
6    ir::{
7        classes::SymField,
8        types::{SymGenericTerm, SymPerm, SymPlace, SymPlaceKind, SymTy},
9    },
10    prelude::CheckedFieldTy,
11};
12
13use super::{inference::Direction, red::RedTy, to_red::ToRedTy};
14
15pub trait PlaceTy<'db> {
16    async fn place_ty(&self, env: &mut Env<'db>) -> SymTy<'db>;
17}
18
19impl<'db> PlaceTy<'db> for SymPlace<'db> {
20    #[boxed_async_fn]
21    async fn place_ty(&self, env: &mut Env<'db>) -> SymTy<'db> {
22        match *self.kind(env.db()) {
23            SymPlaceKind::Var(sym_variable) => env.variable_ty(sym_variable).await,
24            SymPlaceKind::Field(owner_place, sym_field) => {
25                let owner_ty = owner_place.place_ty(env).await;
26                let (owner_red_ty, owner_perm) = owner_ty.to_red_ty(env);
27                field_ty(env, owner_place, owner_perm, owner_red_ty, sym_field)
28            }
29            SymPlaceKind::Index(_sym_place) => {
30                todo!()
31            }
32            SymPlaceKind::Error(reported) => SymTy::err(env.db(), reported),
33            SymPlaceKind::Erased => panic!("cannot compute type of an erased place"),
34        }
35    }
36}
37
38fn field_ty<'db>(
39    env: &mut Env<'db>,
40    owner_place: SymPlace<'db>,
41    owner_perm: SymPerm<'db>,
42    owner_red_ty: RedTy<'db>,
43    sym_field: SymField<'db>,
44) -> SymTy<'db> {
45    let db = env.db();
46    match owner_red_ty {
47        RedTy::Error(reported) => SymTy::err(db, reported),
48
49        RedTy::Named(_name, generics) => {
50            // FIXME: eventually we probably want to upcast here
51            let field_ty = sym_field.checked_field_ty(db);
52            let field_ty = field_ty
53                .substitute(env.db(), &generics)
54                .substitute(env.db(), &[SymGenericTerm::Place(owner_place)]);
55
56            owner_perm.apply_to(db, field_ty)
57        }
58
59        RedTy::Infer(infer) => {
60            // To have constructed this place there must have been a valid inference bound already
61            let (infer_red_ty, _) = env
62                .red_bound(infer, Direction::FromBelow)
63                .peek_ty()
64                .unwrap();
65            field_ty(env, owner_place, owner_perm, infer_red_ty, sym_field)
66        }
67
68        RedTy::Perm | RedTy::Var(_) | RedTy::Never => {
69            unreachable!("no fields on a {owner_red_ty:?}")
70        }
71    }
72}
dada_ir_sym/check/places.rs

dada_ir_sym/check/
places.rs
