diff --git a/sol-thir-lowering/src/check.rs b/sol-thir-lowering/src/check.rs index 953c077..1a754be 100644 --- a/sol-thir-lowering/src/check.rs +++ b/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 { - 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())) diff --git a/sol-thir-lowering/src/infer.rs b/sol-thir-lowering/src/infer.rs index 45720cb..5258b77 100644 --- a/sol-thir-lowering/src/infer.rs +++ b/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 { + 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()); diff --git a/sol-thir-lowering/src/lib.rs b/sol-thir-lowering/src/lib.rs index c3a832f..1e3bba6 100644 --- a/sol-thir-lowering/src/lib.rs +++ b/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()) diff --git a/sol-thir/src/lib.rs b/sol-thir/src/lib.rs index d63e760..9c6b714 100644 --- a/sol-thir/src/lib.rs +++ b/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))] diff --git a/sol-thir/src/unification.rs b/sol-thir/src/unification.rs index a28ff53..20fbf00 100644 --- a/sol-thir/src/unification.rs +++ b/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))?)?; diff --git a/sol-thir/src/value.rs b/sol-thir/src/value.rs index a2f2b22..7e3b757 100644 --- a/sol-thir/src/value.rs +++ b/sol-thir/src/value.rs @@ -98,6 +98,6 @@ impl Closure { pub struct Pi { pub name: Option, pub implicitness: shared::Implicitness, - pub type_repr: Box, - pub closure: Closure, + pub domain: Box, + pub codomain: Closure, }