feat(sol-thir-lowering): finish check checks

sol-thir-lowering/src/check.rs

@@ -1,7 +1,20 @@
 use sol_thir::InferResult;
+use Implicitness::*;
 
 use super::*;
 
+/// CASE: lam-pi / lam-pi-implicit
+fn lam_pi(db: &dyn ThirLoweringDb, ctx: Context, lam: Curried, pi: Pi, icit: Implicitness) -> Term {
+    let Curried::Lam(definition, value) = lam else {
+        panic!("handle: no parameters")
+    };
+    let inner_ctx = ctx.create_new_value(db, definition, *pi.type_repr);
+    let term_type = pi.closure.apply(db, Value::new_var(ctx.lvl(db), None));
+    let elab_term = lam_thir_check(db, inner_ctx, *value, term_type, icit);
+
+    Term::Lam(definition, pi.implicitness, elab_term.into())
+}
+
 enum Curried {
     Lam(Definition, Box<Curried>),
     Expr(Expr),
@@ -19,20 +32,11 @@ fn new_curried_function(db: &dyn ThirLoweringDb, abs: AbsExpr) -> Curried {
     acc
 }
 
-fn lam_pi(db: &dyn ThirLoweringDb, ctx: Context, lam: Curried, pi: Pi) -> Term {
-    let Curried::Lam(definition, value) = lam else {
-        panic!("handle: no parameters")
-    };
-    let inner_ctx = ctx.create_new_value(db, definition, *pi.type_repr);
-    let term_type = pi.closure.apply(db, Value::new_var(ctx.lvl(db), None));
-    let elab_term = lam_thir_check(db, inner_ctx, *value, term_type);
-
-    Term::Lam(definition, pi.implicitness, elab_term.into())
-}
-
-fn lam_thir_check(db: &dyn ThirLoweringDb, ctx: Context, expr: Curried, type_repr: Type) -> Term {
+#[rustfmt::skip]
+fn lam_thir_check(db: &dyn ThirLoweringDb, ctx: Context, expr: Curried, type_repr: Type, icit: Implicitness) -> Term {
     match (&expr, &type_repr) {
-        (Curried::Lam(_, _), Value::Pi(pi)) => lam_pi(db, ctx, expr, pi.clone()),
+        (Curried::Lam(_, _), Value::Pi(pi)) => lam_pi(db, ctx, expr, pi.clone(), icit),
+        (Curried::Expr(expr), Value::Pi(pi @ Pi { implicitness: Implicit, .. })) => implicit_fun_eta(db, ctx, expr.clone(), pi.clone()),
         (Curried::Lam(_, _), _) => expected_lam_pi(db, ctx, expr, type_repr),
         (Curried::Expr(expr), _) => db.thir_check(ctx, expr.clone(), type_repr),
     }
@@ -42,14 +46,22 @@ fn expected_lam_pi(db: &dyn ThirLoweringDb, ctx: Context, expr: Curried, type_re
     todo!("handle: error")
 }
 
-fn implicit_fun_eta(db: &dyn ThirLoweringDb, value: Expr, pi: Pi) -> Term {
-    todo!()
+/// CASE: implicit-fun-n
+///
+/// If the pi is implicit, we transform it into an implicit lambda
+fn implicit_fun_eta(db: &dyn ThirLoweringDb, ctx: Context, value: Expr, pi: Pi) -> Term {
+    let inner_ctx = ctx.insert_new_binder(db, pi.name.unwrap(), *pi.type_repr);
+    let term_type = pi.closure.apply(db, Value::new_var(ctx.lvl(db), None));
+    let elab_term = thir_check(db, inner_ctx, value, term_type);
+
+    Term::Lam(pi.name.unwrap(), Implicit, elab_term.into())
 }
 
 fn type_hole() -> Term {
     Term::InsertedMeta(MetaVar::new(None))
 }
 
+/// CASE: term_equality
 fn term_equality(db: &dyn ThirLoweringDb, ctx: Context, expr: Expr, expected: Type) -> Term {
     let InferResult(term, type_repr) = db.thir_infer(ctx, expr);
     let InferResult(term, inferred_type) = elaboration::insert(ctx, term, type_repr);
@@ -59,15 +71,11 @@ fn term_equality(db: &dyn ThirLoweringDb, ctx: Context, expr: Expr, expected: Ty
 
 /// The check function to check the type of the term.
 #[salsa::tracked]
+#[rustfmt::skip]
 pub fn thir_check(db: &dyn ThirLoweringDb, ctx: Context, expr: Expr, type_repr: Type) -> Term {
-    use Implicitness::*;
-
-    ctx.location(db).update(expr.location(db));
-
-    #[rustfmt::skip]
     match (expr, type_repr) {
-        (value, Type::Pi(pi @ Pi { implicitness: Implicit, .. })) => implicit_fun_eta(db, value, pi),
-        (Expr::Abs(abs), Type::Pi(pi)) => lam_pi(db, ctx, new_curried_function(db, abs), pi),
+        (Expr::Abs(abs), Type::Pi(pi)) => lam_pi(db, ctx, new_curried_function(db, abs), pi.clone(), pi.implicitness),
+        (value, Type::Pi(pi @ Pi { implicitness: Implicit, .. })) => implicit_fun_eta(db, ctx, value, pi),
         (Expr::Upgrade(box TypeRep::Hole), _) => type_hole(),
         (value, expected) => term_equality(db, ctx, value, expected)
     }

sol-thir-lowering/src/infer.rs

@@ -7,8 +7,6 @@ use super::*;
 pub fn thir_infer(db: &dyn ThirLoweringDb, ctx: Context, expr: Expr) -> InferResult {
     use Expr::*;
 
-    ctx.location(db).update(expr.location(db));
-
     InferResult::from(match expr {
         Empty | Error(_) | Match(_) => todo!(),
         Path(_) => todo!(),

sol-thir/src/lib.rs

@@ -41,6 +41,7 @@ pub struct Jar(
     shared::Env_len,
     shared::Context,
     shared::Context_create_new_value,
+    shared::Context_insert_new_binder,
     debruijin::Indices,
     debruijin::Level,
     debruijin::Level_as_idx,

sol-thir/src/shared.rs

@@ -23,7 +23,6 @@ impl Constructor {
 #[salsa::tracked]
 pub struct Context {
     pub lvl: Level,
-    pub location: CurrentLocation,
 }
 
 #[salsa::tracked]
@@ -32,6 +31,11 @@ impl Context {
     pub fn create_new_value(self, db: &dyn ThirDb, name: Definition, value: Value) -> Context {
         todo!()
     }
+
+    #[salsa::tracked]
+    pub fn insert_new_binder(self, db: &dyn ThirDb, name: Definition, value: Value) -> Context {
+        todo!()
+    }
 }
 
 #[salsa::tracked]
@@ -152,10 +156,6 @@ macro_rules! mutable_reference {
     };
 }
 
-mutable_reference! {
-  struct CurrentLocation = Location
-}
-
 mutable_reference! {
   struct MetaVar = Option<Value>
 }