Skip to content

Commit

Permalink
feat(sol-thir): add query that finds constructor type
Browse files Browse the repository at this point in the history
  • Loading branch information
aripiprazole committed May 30, 2024
1 parent 8144c4b commit a56f1cc
Show file tree
Hide file tree
Showing 8 changed files with 131 additions and 30 deletions.
4 changes: 2 additions & 2 deletions sol-cli/src/build.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ use sol_hir::{
source::HirSource,
};
use sol_hir_lowering::hir_lower;
use sol_syntax::{parse, Source};
use sol_syntax::Source;
use sol_vfs::SourceFile;

#[derive(Serialize, Deserialize, Debug, Clone)]
Expand All @@ -29,7 +29,7 @@ pub struct Manifest<'db> {
pub root_folder: PathBuf,
pub soruce_folder: PathBuf,
pub config: Config,
pub diagnostics: im::Vector<sol_diagnostic::Diagnostic, FxBuildHasher>,
pub diagnostics: im::Vector<sol_diagnostic::Diagnostic>,
}

impl<'db> Manifest<'db> {
Expand Down
2 changes: 1 addition & 1 deletion sol-driver/src/suite.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ use salsa_2022::DebugWithDb;
use similar::{ChangeTag, TextDiff};
use sol_diagnostic::Diagnostic;
use sol_hir::{fmt::HirFormatter, source::HirElement};
use sol_typer::TypeTable;
use sol_thir::TypeTable;

use crate::RootDb;

Expand Down
7 changes: 7 additions & 0 deletions sol-hir/src/source.rs
Original file line number Diff line number Diff line change
Expand Up @@ -187,6 +187,13 @@ impl Location {
}
}

pub fn source(&self) -> Option<Source> {
match self {
Location::TextRange(range) => Some(range.abstract_source),
Location::CallSite => None,
}
}

pub fn as_source_span(self) -> SourceSpan {
match self {
Location::TextRange(range) => SourceSpan::new(range.start, range.end),
Expand Down
8 changes: 6 additions & 2 deletions sol-thir-lowering/src/infer.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
use sol_diagnostic::bail;
use sol_thir::{
infer_constructor,
shared::{Constructor, ConstructorKind},
ElaboratedTerm,
ElaboratedTerm, ThirConstructor,
};

use super::*;
Expand Down Expand Up @@ -47,7 +48,10 @@ pub fn thir_infer(
location: literal.location(db),
kind: literal.value.into(),
};
(Term::Constructor(constructor.clone()), constructor.infer())
let inferred_type =
infer_constructor(db, ctx, ThirConstructor::new(db, constructor.clone()))?;

(Term::Constructor(constructor.clone()), inferred_type)
}
Type(definition, location) => match create_from_type(definition, location) {
Term::U => (Term::U, Value::U),
Expand Down
1 change: 0 additions & 1 deletion sol-thir-lowering/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@
#![feature(stmt_expr_attributes)]

use salsa::DbWithJar;
use sol_diagnostic::IntoSolDiagnostic;
use sol_hir::{
solver::{Definition, DefinitionId, DefinitionKind::Variable, Reference},
source::{
Expand Down
100 changes: 96 additions & 4 deletions sol-thir/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,21 +6,21 @@
#![feature(trait_upcasting)]
#![feature(box_patterns)]

use debruijin::Level;
use salsa::DbWithJar;
use shared::{Context, Env};
use sol_diagnostic::DiagnosticDb;
use sol_diagnostic::{fail, DiagnosticDb};
use sol_hir::{
lowering::HirLowering,
package::HasManifest,
primitives::PrimitiveProvider,
solver::{Definition, Reference},
source::{expr::Expr, literal::Literal, Location},
source::{expr::Expr, literal::Literal, HirSource, Location},
HirDb,
};
use sol_syntax::ParseDb;

use crate::{
debruijin::Level,
shared::{Constructor, ConstructorKind, Context, Env},
source::Term,
value::{Type, Value},
};
Expand All @@ -45,6 +45,8 @@ pub struct Jar(
shared::Context_create_new_value,
shared::Context_insert_new_binder,
shared::Context_increase_level,
ThirConstructor,
infer_constructor,
debruijin::Indices,
debruijin::Level,
debruijin::Level_as_idx,
Expand All @@ -53,6 +55,7 @@ pub struct Jar(

pub trait ThirDb:
PrimitiveProvider
+ Typer
+ HirDb
+ ThirLowering
+ ThirTyping
Expand All @@ -66,6 +69,7 @@ pub trait ThirDb:

impl<DB> ThirDb for DB where
DB: ?Sized
+ Typer
+ ParseDb
+ DiagnosticDb
+ HasManifest
Expand All @@ -78,6 +82,12 @@ impl<DB> ThirDb for DB where
{
}

pub type TypeTable = im::HashMap<Definition, (Term, Type)>;

pub trait Typer {
fn infer_type_table(&self, source: HirSource) -> sol_diagnostic::Result<TypeTable>;
}

/// Represents the lowering functions for Low-Level Intermediate Representation.
pub trait ThirLowering {
fn thir_eval(&self, env: Env, term: Term) -> sol_diagnostic::Result<Value>;
Expand Down Expand Up @@ -139,3 +149,85 @@ pub enum ThirErrorKind {
#[diagnostic(code(solc::thir::incorrect_kind), url(docsrs))]
IncorrectKind(String),
}

#[salsa::input]
pub struct ThirConstructor {
pub constructor: Constructor,
}

#[derive(Debug, thiserror::Error, miette::Diagnostic)]
#[error("could not find the source code location")]
#[diagnostic(code(sol::thir::could_not_find_location_source))]
pub struct CouldNotFindLocationSourceError {
#[source_code]
#[label = "here"]
pub location: Location,
}

#[derive(Debug, thiserror::Error, miette::Diagnostic)]
#[error("could not find the type of the definition: {name}")]
#[diagnostic(code(sol::thir::could_not_find_type_of_definition))]
pub struct CouldNotFindTypeOfDefinitionError {
pub name: String,

#[source_code]
#[label = "here"]
pub location: Location,
}

#[salsa::tracked]
pub fn infer_constructor(
db: &dyn ThirDb,
ctx: Context,
constructor: ThirConstructor,
) -> sol_diagnostic::Result<Type> {
let constructor = constructor.constructor(db);
Ok(match constructor.kind {
ConstructorKind::UnitType
| ConstructorKind::BooleanType
| ConstructorKind::StringType
| ConstructorKind::NatType
| ConstructorKind::IntType(_, _) => Type::U,
ConstructorKind::Unit => Type::Constructor(Constructor {
kind: ConstructorKind::UnitType,
location: constructor.location,
}),
ConstructorKind::True | ConstructorKind::False => Type::Constructor(Constructor {
kind: ConstructorKind::BooleanType,
location: constructor.location,
}),
ConstructorKind::String(_) => Type::Constructor(Constructor {
kind: ConstructorKind::StringType,
location: constructor.location,
}),
ConstructorKind::Int(_) => Type::Constructor(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
}
})
}
31 changes: 17 additions & 14 deletions sol-thir/src/shared.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,8 @@ use std::{
sync::{Arc, Mutex},
};

use sol_hir::package::Package;

use self::debruijin::Index;
use super::*;

Expand All @@ -14,12 +16,6 @@ pub struct Constructor {
pub location: Location,
}

impl Constructor {
pub fn infer(self) -> Type {
todo!()
}
}

#[salsa::input]
pub struct GlobalEnv {
pub definitions: im::HashMap<Definition, (Term, Type)>,
Expand All @@ -30,11 +26,18 @@ pub struct Context {
pub lvl: Level,
pub locals: Env,
pub env: GlobalEnv,
pub pkg: Package,
}

impl Context {
pub fn default_with_env(db: &dyn ThirDb, env: GlobalEnv) -> Self {
Self::new(db, Level::new(db, 0), Env::new(db, VecDeque::new()), env)
pub fn default_with_env(db: &dyn ThirDb, env: GlobalEnv, pkg: Package) -> Self {
Self::new(
db,
Level::new(db, 0),
Env::new(db, VecDeque::new()),
env,
pkg,
)
}
}

Expand All @@ -43,7 +46,7 @@ impl Context {
#[salsa::tracked]
pub fn increase_level(self, db: &dyn ThirDb) -> Context {
let lvl = self.lvl(db).increase(db);
Context::new(db, lvl, self.locals(db), self.env(db))
Context::new(db, lvl, self.locals(db), self.env(db), self.pkg(db))
}

#[salsa::tracked]
Expand Down Expand Up @@ -108,7 +111,7 @@ pub enum ConstructorKind {
False,
BooleanType,
NatType,
Definition(Definition),
Reference(Reference),
IntType(bool, isize),
Int(isize),
StringType,
Expand Down Expand Up @@ -139,16 +142,16 @@ macro_rules! mutable_reference {
pub struct $name(Arc<Mutex<$type>>);

impl $name {
pub fn new(location: $type) -> Self {
Self(Arc::new(Mutex::new(location)))
pub fn new(value: $type) -> Self {
Self(Arc::new(Mutex::new(value)))
}

pub fn get(&self) -> $type {
self.0.lock().unwrap().clone()
}

pub fn update(&self, location: $type) {
*self.0.lock().unwrap() = location;
pub fn update(&self, value: $type) {
*self.0.lock().unwrap() = value;
}
}

Expand Down
8 changes: 2 additions & 6 deletions sol-typer/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,21 +13,17 @@ use std::{
use salsa::DbWithJar;
use sol_diagnostic::{report_error, TextSource, UnwrapOrReport};
use sol_hir::{
solver::Definition,
source::{declaration::Declaration, top_level::TopLevel, HirSource},
HirDb,
};
use sol_thir::{
shared::{Context, Env, GlobalEnv, MetaVar},
source::Term,
value::Type,
ThirDb,
ThirDb, TypeTable,
};

extern crate salsa_2022 as salsa;

pub type TypeTable = im::HashMap<Definition, (Term, Type)>;

#[salsa::jar(db = TyperDb)]
pub struct Jar(infer_type_table);

Expand Down Expand Up @@ -93,7 +89,7 @@ pub struct TyperPanicError {
#[salsa::tracked]
pub fn infer_type_table(db: &dyn TyperDb, global_env: GlobalEnv, source: HirSource) -> TypeTable {
let mut table = TypeTable::new();
let ctx = Context::default_with_env(db, global_env);
let ctx = Context::default_with_env(db, global_env, source.package(db));
let text_source = TextSource::new(
source.source(db).file_path(db).to_string_lossy(),
Arc::new(source.source(db).source_text(db).to_string()),
Expand Down

0 comments on commit a56f1cc

Please sign in to comment.