Skip to content

Commit

Permalink
feat(sol-thir): elaborate path
Browse files Browse the repository at this point in the history
  • Loading branch information
aripiprazole committed May 30, 2024
1 parent a56f1cc commit 295d95a
Show file tree
Hide file tree
Showing 3 changed files with 59 additions and 46 deletions.
17 changes: 12 additions & 5 deletions sol-thir-lowering/src/infer.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
use sol_diagnostic::bail;
use sol_thir::{
infer_constructor,
find_reference_type, infer_constructor,
shared::{Constructor, ConstructorKind},
ElaboratedTerm, ThirConstructor,
};
Expand Down Expand Up @@ -42,16 +42,23 @@ pub fn thir_infer(

Ok(ElaboratedTerm::from(match expr {
Empty | Error(_) | Match(_) => todo!(),
Path(_) => todo!(),
Path(path) => {
let constructor = Constructor {
kind: ConstructorKind::Reference(path),
location: path.location(db),
};
let (_, inferred_type) = find_reference_type(db, ctx, path)?;

(Term::Constructor(constructor), inferred_type)
}
Literal(literal) => {
let constructor = Constructor {
location: literal.location(db),
kind: literal.value.into(),
};
let inferred_type =
infer_constructor(db, ctx, ThirConstructor::new(db, constructor.clone()))?;
let inferred_type = infer_constructor(db, ctx, constructor.clone())?;

(Term::Constructor(constructor.clone()), inferred_type)
(Term::Constructor(constructor), inferred_type)
}
Type(definition, location) => match create_from_type(definition, location) {
Term::U => (Term::U, Value::U),
Expand Down
63 changes: 34 additions & 29 deletions sol-thir/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ pub struct Jar(
shared::Context_insert_new_binder,
shared::Context_increase_level,
ThirConstructor,
infer_constructor,
find_reference_type,
debruijin::Indices,
debruijin::Level,
debruijin::Level_as_idx,
Expand Down Expand Up @@ -175,13 +175,11 @@ pub struct CouldNotFindTypeOfDefinitionError {
pub location: Location,
}

#[salsa::tracked]
pub fn infer_constructor(
db: &dyn ThirDb,
ctx: Context,
constructor: ThirConstructor,
constructor: Constructor,
) -> sol_diagnostic::Result<Type> {
let constructor = constructor.constructor(db);
Ok(match constructor.kind {
ConstructorKind::UnitType
| ConstructorKind::BooleanType
Expand All @@ -204,30 +202,37 @@ pub fn infer_constructor(
kind: ConstructorKind::IntType(true, 32),
location: constructor.location,
}),
ConstructorKind::Reference(reference) => {
let definition = reference.definition(db);
let Some(src) = definition.location(db).source() else {
return fail(CouldNotFindLocationSourceError {
location: reference.location(db),
});
};

let type_table =
if definition.location(db).text_source() == reference.location(db).text_source() {
ctx.env(db).definitions(db)
} else {
let hir_src = db.hir_lower(ctx.pkg(db), src);
db.infer_type_table(hir_src)?
};

let Some((_, inferred_type)) = type_table.get(&definition).cloned() else {
return fail(CouldNotFindTypeOfDefinitionError {
name: definition.name(db).to_string(db).unwrap(),
location: reference.location(db),
});
};

inferred_type
}
ConstructorKind::Reference(reference) => find_reference_type(db, ctx, reference)?.1,
})
}

#[salsa::tracked]
pub fn find_reference_type(
db: &dyn ThirDb,
ctx: Context,
reference: Reference,
) -> sol_diagnostic::Result<(Term, Value)> {
let definition = reference.definition(db);
let Some(src) = definition.location(db).source() else {
return fail(CouldNotFindLocationSourceError {
location: reference.location(db),
});
};

let type_table =
if definition.location(db).text_source() == reference.location(db).text_source() {
ctx.env(db).definitions(db)
} else {
let hir_src = db.hir_lower(ctx.pkg(db), src);
db.infer_type_table(hir_src)?
};

let Some(elaborated_type) = type_table.get(&definition).cloned() else {
return fail(CouldNotFindTypeOfDefinitionError {
name: definition.name(db).to_string(db).unwrap(),
location: reference.location(db),
});
};

Ok(elaborated_type)
}
25 changes: 13 additions & 12 deletions sol-thir/src/shared.rs
Original file line number Diff line number Diff line change
Expand Up @@ -121,18 +121,19 @@ pub enum ConstructorKind {
impl From<Literal> for ConstructorKind {
fn from(literal: Literal) -> Self {
match literal {
Literal::Empty => todo!(),
Literal::Int8(_) => todo!(),
Literal::UInt8(_) => todo!(),
Literal::Int16(_) => todo!(),
Literal::UInt16(_) => todo!(),
Literal::Int32(_) => todo!(),
Literal::UInt32(_) => todo!(),
Literal::Int64(_) => todo!(),
Literal::UInt64(_) => todo!(),
Literal::String(_) => todo!(),
Literal::Boolean(_) => todo!(),
Literal::Char(_) => todo!(),
Literal::Empty => ConstructorKind::Unit,
Literal::Int8(value) => ConstructorKind::Int(value as _),
Literal::UInt8(value) => ConstructorKind::Int(value as _),
Literal::Int16(value) => ConstructorKind::Int(value as _),
Literal::UInt16(value) => ConstructorKind::Int(value as _),
Literal::Int32(value) => ConstructorKind::Int(value as _),
Literal::UInt32(value) => ConstructorKind::Int(value as _),
Literal::Int64(value) => ConstructorKind::Int(value as _),
Literal::UInt64(value) => ConstructorKind::Int(value as _),
Literal::String(string) => ConstructorKind::String(string),
Literal::Boolean(true) => ConstructorKind::True,
Literal::Boolean(false) => ConstructorKind::False,
Literal::Char(char) => ConstructorKind::Int(char as _),
}
}
}
Expand Down

0 comments on commit 295d95a

Please sign in to comment.