From bdd561c3e56f5c4db7cf7817bc89c6d15ce8b4c1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Gabrielle=20Guimar=C3=A3es=20de=20Oliveira?=
 <gabrielle1guim@gmail.com>
Date: Sun, 12 May 2024 12:35:50 -0300
Subject: [PATCH] feat(sol-driver): reference functions

---
 sol-driver/src/lib.rs        | 28 +++++++++++++++++++++++++++-
 sol-thir-lowering/src/lib.rs |  8 ++++----
 2 files changed, 31 insertions(+), 5 deletions(-)

diff --git a/sol-driver/src/lib.rs b/sol-driver/src/lib.rs
index a0a2aa5..dd7bdb9 100644
--- a/sol-driver/src/lib.rs
+++ b/sol-driver/src/lib.rs
@@ -9,7 +9,9 @@ use sol_hir::{
     lowering::HirLowering,
     package::{HasManifest, Package},
     primitives::{PrimitiveBag, PrimitiveProvider},
+    source::expr::Expr,
 };
+use sol_thir::{source::Term, value::Type, ThirLowering, ThirTyping};
 
 /// Defines watcher strategies for [`RootDb`].
 pub mod watcher;
@@ -35,7 +37,9 @@ extern crate salsa_2022 as salsa;
     sol_syntax::Jar,
     sol_diagnostic::Jar,
     sol_typer::Jar,
-    sol_hir_lowering::Jar
+    sol_hir_lowering::Jar,
+    sol_thir::Jar,
+    sol_thir_lowering::Jar
 )]
 #[derive(Default)]
 pub struct RootDb {
@@ -59,6 +63,28 @@ impl HirLowering for RootDb {
     }
 }
 
+/// Bridges the [`RootDb`] with the [`sol_thir::ThirLowering`] trait.
+impl ThirLowering for RootDb {
+    fn thir_eval(&self, env: sol_thir::shared::Env, term: Term) -> sol_thir::value::Value {
+        sol_thir_lowering::thir_eval(self, env, term)
+    }
+
+    fn thir_quote(&self, lvl: sol_thir::debruijin::Level, value: sol_thir::value::Value) -> Term {
+        sol_thir_lowering::thir_quote(self, lvl, value)
+    }
+}
+
+/// Bridges the [`RootDb`] with the [`sol_thir::ThirTyping`] trait.
+impl ThirTyping for RootDb {
+    fn thir_infer(&self, ctx: sol_thir::shared::Context, expr: Expr) -> (Term, Type) {
+        sol_thir_lowering::thir_infer(self, ctx, expr)
+    }
+
+    fn thir_check(&self, ctx: sol_thir::shared::Context, expr: Expr, type_repr: Type) -> Term {
+        sol_thir_lowering::thir_check(self, ctx, expr, type_repr)
+    }
+}
+
 impl RootDb {
     /// Registers a package in the database.
     pub fn register_package(&self, package: Package) -> Package {
diff --git a/sol-thir-lowering/src/lib.rs b/sol-thir-lowering/src/lib.rs
index 2ee9f25..974eb79 100644
--- a/sol-thir-lowering/src/lib.rs
+++ b/sol-thir-lowering/src/lib.rs
@@ -49,7 +49,7 @@ fn eval_app(callee: Value, argument: Value) -> Value {
 }
 
 #[salsa::tracked]
-fn thir_eval(db: &dyn ThirLoweringDb, env: Env, term: Term) -> Value {
+pub fn thir_eval(db: &dyn ThirLoweringDb, env: Env, term: Term) -> Value {
     match term {
         Term::U => Value::U,
         Term::Var(idx, _) => env.get(db, idx),
@@ -68,7 +68,7 @@ fn thir_eval(db: &dyn ThirLoweringDb, env: Env, term: Term) -> Value {
 
 /// The quoting function to convert the value back to the term.
 #[salsa::tracked]
-fn thir_quote(db: &dyn ThirLoweringDb, lvl: Level, value: Value) -> Term {
+pub fn thir_quote(db: &dyn ThirLoweringDb, lvl: Level, value: Value) -> Term {
     let (location, value) = value.force(db);
 
     location
@@ -128,7 +128,7 @@ fn thir_quote_impl(
 
 /// The infer function to infer the type of the term.
 #[salsa::tracked]
-fn thir_infer(db: &dyn ThirLoweringDb, ctx: Context, expr: Expr) -> (Term, Type) {
+pub fn thir_infer(db: &dyn ThirLoweringDb, ctx: Context, expr: Expr) -> (Term, Type) {
     ctx.location(db).update(expr.location(db));
 
     todo!()
@@ -136,7 +136,7 @@ fn thir_infer(db: &dyn ThirLoweringDb, ctx: Context, expr: Expr) -> (Term, Type)
 
 /// The check function to check the type of the term.
 #[salsa::tracked]
-fn thir_check(db: &dyn ThirLoweringDb, ctx: Context, expr: Expr, type_repr: Type) -> Term {
+pub fn thir_check(db: &dyn ThirLoweringDb, ctx: Context, expr: Expr, type_repr: Type) -> Term {
     todo!()
 }