From 16cfdda70f1d59d0e8b9344fa125acfabd3f0482 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Gabrielle=20Guimar=C3=A3es=20de=20Oliveira?=
 <gabrielle1guim@gmail.com>
Date: Wed, 29 May 2024 20:23:48 -0300
Subject: [PATCH] refactor(sol-thir): fix warnings

---
 sol-thir/src/source.rs      |  2 +-
 sol-thir/src/unification.rs |  4 ++--
 sol-thir/src/value.rs       | 17 +++--------------
 3 files changed, 6 insertions(+), 17 deletions(-)

diff --git a/sol-thir/src/source.rs b/sol-thir/src/source.rs
index 0a16a6b..decfc84 100644
--- a/sol-thir/src/source.rs
+++ b/sol-thir/src/source.rs
@@ -20,7 +20,7 @@ pub enum Term {
 
 impl Default for Term {
     fn default() -> Self {
-        Term::U
+        Term::InsertedMeta(shared::MetaVar::new(None))
     }
 }
 
diff --git a/sol-thir/src/unification.rs b/sol-thir/src/unification.rs
index 65b92fe..a28ff53 100644
--- a/sol-thir/src/unification.rs
+++ b/sol-thir/src/unification.rs
@@ -170,10 +170,10 @@ impl Value {
             }
             (Lam(_, _, clos_a)                 , rhs) => {
                 clos_a.apply(db, Value::new_var(ctx.lvl(db), None))?
-                    .unify(db, ctx.increase_level(db), rhs.apply(db, Value::new_var(ctx.lvl(db), None))?)
+                    .unify(db, ctx.increase_level(db), rhs.apply_to_spine(db, Value::new_var(ctx.lvl(db), None))?)
             }
             (lhs                               , Lam(_, _, clos_b)) => {
-                lhs.apply(db, Value::new_var(ctx.lvl(db), None))?
+                lhs.apply_to_spine(db, Value::new_var(ctx.lvl(db), None))?
                     .unify(db, ctx.increase_level(db), clos_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 7cf275e..a2f2b22 100644
--- a/sol-thir/src/value.rs
+++ b/sol-thir/src/value.rs
@@ -1,5 +1,4 @@
-use sol_diagnostic::fail;
-use unification::UnifyError;
+use shared::MetaVar;
 
 use super::*;
 
@@ -19,7 +18,7 @@ pub enum Value {
 
 impl Default for Value {
     fn default() -> Self {
-        Value::U
+        Value::Flexible(MetaVar::new(None), vec![])
     }
 }
 
@@ -42,16 +41,6 @@ impl Value {
         }
     }
 
-    pub fn apply(self, db: &dyn ThirDb, argument: Value) -> sol_diagnostic::Result<Value> {
-        match self {
-            _ => {
-                let this = db.thir_quote(debruijin::Level::new(db, 0), self.clone())?;
-                let argument = db.thir_quote(debruijin::Level::new(db, 0), argument.clone())?;
-                fail(UnifyError::CouldNotApply(this, argument))
-            }
-        }
-    }
-
     pub fn apply_with_spine(
         self,
         db: &dyn ThirDb,
@@ -60,7 +49,7 @@ impl Value {
         spine
             .into_iter()
             .rev()
-            .fold(Ok(self), |acc, next| Ok(acc?.apply_to_spine(db, next)?))
+            .try_fold(self, |acc, next| acc.apply_to_spine(db, next))
     }
 
     pub fn apply_to_spine(self, db: &dyn ThirDb, argument: Value) -> sol_diagnostic::Result<Value> {