From a56f1cc31ee8d017af7e93c1ded83c9a33892500 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gabrielle=20Guimar=C3=A3es=20de=20Oliveira?= Date: Wed, 29 May 2024 21:28:51 -0300 Subject: [PATCH] feat(sol-thir): add query that finds constructor type --- sol-cli/src/build.rs | 4 +- sol-driver/src/suite.rs | 2 +- sol-hir/src/source.rs | 7 +++ sol-thir-lowering/src/infer.rs | 8 ++- sol-thir-lowering/src/lib.rs | 1 - sol-thir/src/lib.rs | 100 +++++++++++++++++++++++++++++++-- sol-thir/src/shared.rs | 31 +++++----- sol-typer/src/lib.rs | 8 +-- 8 files changed, 131 insertions(+), 30 deletions(-) diff --git a/sol-cli/src/build.rs b/sol-cli/src/build.rs index 818d0d7..bac9d39 100644 --- a/sol-cli/src/build.rs +++ b/sol-cli/src/build.rs @@ -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)] @@ -29,7 +29,7 @@ pub struct Manifest<'db> { pub root_folder: PathBuf, pub soruce_folder: PathBuf, pub config: Config, - pub diagnostics: im::Vector, + pub diagnostics: im::Vector, } impl<'db> Manifest<'db> { diff --git a/sol-driver/src/suite.rs b/sol-driver/src/suite.rs index 52e6773..85006ed 100644 --- a/sol-driver/src/suite.rs +++ b/sol-driver/src/suite.rs @@ -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; diff --git a/sol-hir/src/source.rs b/sol-hir/src/source.rs index ab0c0b3..e6894e1 100644 --- a/sol-hir/src/source.rs +++ b/sol-hir/src/source.rs @@ -187,6 +187,13 @@ impl Location { } } + pub fn source(&self) -> Option { + 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), diff --git a/sol-thir-lowering/src/infer.rs b/sol-thir-lowering/src/infer.rs index dc22b55..809c0e4 100644 --- a/sol-thir-lowering/src/infer.rs +++ b/sol-thir-lowering/src/infer.rs @@ -1,7 +1,8 @@ use sol_diagnostic::bail; use sol_thir::{ + infer_constructor, shared::{Constructor, ConstructorKind}, - ElaboratedTerm, + ElaboratedTerm, ThirConstructor, }; use super::*; @@ -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), diff --git a/sol-thir-lowering/src/lib.rs b/sol-thir-lowering/src/lib.rs index 3fb223a..c3a832f 100644 --- a/sol-thir-lowering/src/lib.rs +++ b/sol-thir-lowering/src/lib.rs @@ -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::{ diff --git a/sol-thir/src/lib.rs b/sol-thir/src/lib.rs index 6615825..145ac28 100644 --- a/sol-thir/src/lib.rs +++ b/sol-thir/src/lib.rs @@ -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}, }; @@ -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, @@ -53,6 +55,7 @@ pub struct Jar( pub trait ThirDb: PrimitiveProvider + + Typer + HirDb + ThirLowering + ThirTyping @@ -66,6 +69,7 @@ pub trait ThirDb: impl ThirDb for DB where DB: ?Sized + + Typer + ParseDb + DiagnosticDb + HasManifest @@ -78,6 +82,12 @@ impl ThirDb for DB where { } +pub type TypeTable = im::HashMap; + +pub trait Typer { + fn infer_type_table(&self, source: HirSource) -> sol_diagnostic::Result; +} + /// Represents the lowering functions for Low-Level Intermediate Representation. pub trait ThirLowering { fn thir_eval(&self, env: Env, term: Term) -> sol_diagnostic::Result; @@ -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 { + 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 + } + }) +} diff --git a/sol-thir/src/shared.rs b/sol-thir/src/shared.rs index 2a7ed0d..023c243 100644 --- a/sol-thir/src/shared.rs +++ b/sol-thir/src/shared.rs @@ -4,6 +4,8 @@ use std::{ sync::{Arc, Mutex}, }; +use sol_hir::package::Package; + use self::debruijin::Index; use super::*; @@ -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, @@ -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, + ) } } @@ -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] @@ -108,7 +111,7 @@ pub enum ConstructorKind { False, BooleanType, NatType, - Definition(Definition), + Reference(Reference), IntType(bool, isize), Int(isize), StringType, @@ -139,16 +142,16 @@ macro_rules! mutable_reference { pub struct $name(Arc>); 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; } } diff --git a/sol-typer/src/lib.rs b/sol-typer/src/lib.rs index 8c23039..0a06f94 100644 --- a/sol-typer/src/lib.rs +++ b/sol-typer/src/lib.rs @@ -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; - #[salsa::jar(db = TyperDb)] pub struct Jar(infer_type_table); @@ -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()),