feat(sol-thir-lowering): start infer elaboration

sol-thir-lowering/src/check.rs

@@ -1,3 +1,5 @@
+use sol_thir::InferResult;
+
 use super::*;
 
 enum Curried {
@@ -49,8 +51,8 @@ fn type_hole() -> Term {
 }
 
 fn term_equality(db: &dyn ThirLoweringDb, ctx: Context, expr: Expr, expected: Type) -> Term {
-    let (term, type_repr) = db.thir_infer(ctx, expr);
-    let (term, inferred_type) = elaboration::insert(ctx, term, type_repr);
+    let InferResult(term, type_repr) = db.thir_infer(ctx, expr);
+    let InferResult(term, inferred_type) = elaboration::insert(ctx, term, type_repr);
     elaboration::unify_catch(db, ctx, expected, inferred_type);
     term
 }

sol-thir-lowering/src/elaboration.rs

@@ -1,3 +1,5 @@
+use sol_thir::InferResult;
+
 use super::*;
 
 #[salsa::tracked]
@@ -7,6 +9,6 @@ pub fn unify_catch(db: &dyn ThirLoweringDb, ctx: Context, lhs: Value, rhs: Value
 
 /// Insert fresh implicit applications to a term which is not
 /// an implicit lambda (i.e. neutral).
-pub fn insert(ctx: Context, term: Term, type_repr: Value) -> (Term, Type) {
+pub fn insert(ctx: Context, term: Term, type_repr: Value) -> InferResult {
     todo!()
 }

sol-thir-lowering/src/infer.rs

@@ -0,0 +1,35 @@
+use sol_thir::{shared::Constructor, InferResult};
+
+use super::*;
+
+/// The infer function to infer the type of the term.
+#[salsa::tracked]
+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!(),
+        Literal(literal) => {
+            let constructor = Constructor {
+                location: literal.location(db),
+                kind: literal.value.into(),
+            };
+
+            (Term::Constructor(constructor.clone()), constructor.infer())
+        }
+        Call(_) => todo!(),
+        Ann(_) => todo!(),
+        Abs(_) => todo!(),
+        Upgrade(box TypeRep::App(_)) => todo!(),
+        Upgrade(box TypeRep::Hole) => todo!(),
+        Upgrade(box TypeRep::Unit) => todo!(),
+        Upgrade(box TypeRep::Type) => todo!(),
+        Upgrade(box TypeRep::Pi(_)) => todo!(),
+        Upgrade(box TypeRep::Path(_, _)) => todo!(),
+        Upgrade(box TypeRep::Error(_) | box TypeRep::SelfType) => todo!("unsuporrted type rep"),
+        Upgrade(box TypeRep::Downgrade(box expr)) => return db.thir_infer(ctx, expr),
+    })
+}

sol-thir-lowering/src/lib.rs

@@ -29,11 +29,12 @@ extern crate salsa_2022 as salsa;
 
 pub mod check;
 pub mod elaboration;
+pub mod infer;
 
 #[salsa::jar(db = ThirLoweringDb)]
 pub struct Jar(
     thir_eval,
-    thir_infer,
+    infer::thir_infer,
     check::thir_check,
     thir_quote,
     elaboration::unify_catch,
@@ -136,34 +137,6 @@ pub fn thir_quote(db: &dyn ThirLoweringDb, lvl: Level, value: Value) -> Term {
         .unwrap_or_else(|| thir_quote_impl(db, None, lvl, value))
 }
 
-/// The infer function to infer the type of the term.
-#[salsa::tracked]
-pub fn thir_infer(db: &dyn ThirLoweringDb, ctx: Context, expr: Expr) -> (Term, Type) {
-    use Expr::*;
-
-    ctx.location(db).update(expr.location(db));
-
-    match expr {
-        Empty => todo!(),
-        Error(_) => todo!(),
-        Path(_) => todo!(),
-        Literal(_) => todo!(),
-        Call(_) => todo!(),
-        Ann(_) => todo!(),
-        Abs(_) => todo!(),
-        Match(_) => todo!(),
-        Upgrade(box TypeRep::App(_)) => todo!(),
-        Upgrade(box TypeRep::Hole) => todo!(),
-        Upgrade(box TypeRep::SelfType) => todo!(),
-        Upgrade(box TypeRep::Unit) => todo!(),
-        Upgrade(box TypeRep::Type) => todo!(),
-        Upgrade(box TypeRep::Pi(_)) => todo!(),
-        Upgrade(box TypeRep::Path(_, _)) => todo!(),
-        Upgrade(box TypeRep::Error(_)) => todo!(),
-        Upgrade(box TypeRep::Downgrade(box expr)) => db.thir_infer(ctx, expr),
-    }
-}
-
 pub fn extract_parameter_definition(db: &dyn ThirLoweringDb, pattern: Pattern) -> Definition {
     let location = pattern.location(db);
     let hole = HirPath::create(db, "_");

sol-thir/src/lib.rs

@@ -84,12 +84,27 @@ pub trait ThirLowering {
 /// Represents the typing functions for Typed High-Level Intermediate Representation.
 pub trait ThirTyping {
     /// The infer function to infer the type of the term.
-    fn thir_infer(&self, ctx: Context, expr: Expr) -> (Term, Type);
+    fn thir_infer(&self, ctx: Context, expr: Expr) -> InferResult;
 
     /// The check function to check the type of the term.
     fn thir_check(&self, ctx: Context, expr: Expr, type_repr: Type) -> Term;
 }
 
+#[derive(Debug, Clone, Hash, PartialEq, Eq)]
+pub struct InferResult(pub Term, pub Type);
+
+impl From<(Term, Type)> for InferResult {
+    fn from((term, ty): (Term, Type)) -> Self {
+        Self(term, ty)
+    }
+}
+
+impl Default for InferResult {
+    fn default() -> Self {
+        todo!()
+    }
+}
+
 /// Represents the diagnostic for High-Level Intermediate Representation. It's intended to be used
 /// to report errors to the diagnostic database, by this crate, only.
 #[derive(Debug, thiserror::Error, serde::Serialize, miette::Diagnostic)]

sol-thir/src/shared.rs

@@ -14,6 +14,12 @@ pub struct Constructor {
     pub location: Location,
 }
 
+impl Constructor {
+    pub fn infer(self) -> Type {
+        todo!()
+    }
+}
+
 #[salsa::tracked]
 pub struct Context {
     pub lvl: Level,