feat(sol-thir-lowering): elaborate on pi

sol-thir-lowering/src/check.rs

@@ -14,8 +14,8 @@ fn lam_pi(
     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 inner_ctx = ctx.create_new_value(db, definition, *pi.domain);
+    let term_type = pi.codomain.apply(db, Value::new_var(ctx.lvl(db), None))?;
     let elab_term = lam_thir_check(db, inner_ctx, *value, term_type, icit)?;
 
     Ok(Term::Lam(definition, pi.implicitness, elab_term.into()))
@@ -66,8 +66,8 @@ fn implicit_fun_eta(
     value: Expr,
     pi: Pi,
 ) -> sol_diagnostic::Result<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 inner_ctx = ctx.insert_new_binder(db, pi.name.unwrap(), *pi.domain);
+    let term_type = pi.codomain.apply(db, Value::new_var(ctx.lvl(db), None))?;
     let elab_term = db.thir_check(inner_ctx, value, term_type)?;
 
     Ok(Term::Lam(pi.name.unwrap(), Implicit, elab_term.into()))

sol-thir-lowering/src/infer.rs

@@ -1,8 +1,11 @@
+use std::str::pattern::Pattern;
+
 use sol_diagnostic::{bail, fail};
+use sol_hir::source::pattern::Pattern;
 use sol_thir::{
     find_reference_type, infer_constructor,
     shared::{Constructor, ConstructorKind},
-    ElaboratedTerm, ThirConstructor,
+    ElaboratedTerm,
 };
 
 use super::*;
@@ -47,10 +50,13 @@ pub fn thir_infer(
     ctx: Context,
     expr: Expr,
 ) -> sol_diagnostic::Result<ElaboratedTerm> {
+    use sol_hir::source::expr::Pi as EPi;
+    use sol_hir::source::pattern::Pattern;
+    use sol_thir::value::Pi as VPi;
     use Expr::*;
 
     Ok(ElaboratedTerm::from(match expr {
-        Empty | Error(_) | Match(_) => {
+        Empty | Error(_) | Match(_) | Sigma(_) => {
             return fail(UnsupportedTerm {
                 location: expr.location(db),
             })
@@ -83,12 +89,31 @@ pub fn thir_infer(
             let term = db.thir_check(ctx, *ann.value, actual_type.clone())?;
             (term, actual_type)
         }
-        Call(call) => {
-            todo!()
-        }
+        Call(_) => todo!(),
         Lam(_) => todo!(),
-        Pi(_) => todo!(),
-        Sigma(_) => bail!("sigma types are not supported yet"),
+        Pi(EPi {
+            parameters,
+            value,
+            location,
+        }) => {
+            let mut codomain = db.thir_check(ctx, *value.expr, Value::U)?;
+            for parameter in parameters {
+                let parameter_type = parameter.parameter_type(db);
+                let name = match parameter.binding(db) {
+                    Pattern::Binding(binding) => Some(binding.name),
+                    _ => None,
+                };
+                let domain = db.thir_check(ctx, *parameter_type.expr, Value::U)?;
+                let implicitness = if parameter.is_implicit(db) {
+                    Implicitness::Implicit
+                } else {
+                    Implicitness::Explicit
+                };
+                codomain = Term::Pi(name, implicitness, domain.into(), codomain.into());
+            }
+
+            (codomain, Value::U)
+        }
         Hole(_) => {
             let meta = MetaVar::new(None);
             let term = Term::InsertedMeta(meta.clone());

sol-thir-lowering/src/lib.rs

@@ -59,8 +59,8 @@ pub fn thir_eval(db: &dyn ThirLoweringDb, env: Env, term: Term) -> sol_diagnosti
         Term::Pi(name, implicitness, domain, codomain) => Value::Pi(Pi {
             name,
             implicitness,
-            type_repr: Box::new(db.thir_eval(env, *domain)?),
-            closure: Closure {
+            domain: Box::new(db.thir_eval(env, *domain)?),
+            codomain: Closure {
                 env,
                 expr: *codomain,
             },
@@ -110,7 +110,7 @@ pub fn thir_quote(
             Pi(pi) => {
                 // Pi (quote lvl pi.type_rep) (quote (lvl + 1) (pi.closure $$ (Var lvl pi.name)))
                 let name = create_reference_of(db, pi.name, location.clone());
-                let domain = db.thir_quote(lvl, *pi.type_repr.clone())?;
+                let domain = db.thir_quote(lvl, *pi.domain.clone())?;
                 let codomain = db.thir_quote(lvl.increase(db), Value::new_var(lvl, name))?;
 
                 Term::Pi(pi.name, pi.implicitness, domain.into(), codomain.into())

sol-thir/src/lib.rs

@@ -45,7 +45,6 @@ pub struct Jar(
     shared::Context_create_new_value,
     shared::Context_insert_new_binder,
     shared::Context_increase_level,
-    ThirConstructor,
     find_reference_type,
     debruijin::Indices,
     debruijin::Level,
@@ -150,11 +149,6 @@ pub enum ThirErrorKind {
     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))]

sol-thir/src/unification.rs

@@ -186,7 +186,7 @@ impl Value {
                 let rhs = db.thir_quote(ctx.lvl(db), rhs.clone())?;
                 fail(UnifyError::IcitMismatch(icit_a, icit_b, lhs, rhs))
             }
-            (Pi(VPi { type_repr: box dom_a, closure: cod_a, .. }), Pi(VPi { type_repr: box dom_b, closure: cod_b, .. })) => {
+            (Pi(VPi { domain: box dom_a, codomain: cod_a, .. }), Pi(VPi { domain: box dom_b, codomain: cod_b, .. })) => {
                 dom_a.unify(db, ctx, dom_b)?;
                 cod_a.apply(db, Value::new_var(ctx.lvl(db), None))?
                     .unify(db, ctx.increase_level(db), cod_b.apply(db, Value::new_var(ctx.lvl(db), None))?)?;

sol-thir/src/value.rs

@@ -98,6 +98,6 @@ impl Closure {
 pub struct Pi {
     pub name: Option<Definition>,
     pub implicitness: shared::Implicitness,
-    pub type_repr: Box<Type>,
-    pub closure: Closure,
+    pub domain: Box<Type>,
+    pub codomain: Closure,
 }