fix(sol-thir): add normalize function

sol-thir/src/lib.rs

@@ -36,6 +36,7 @@ pub mod value;
 pub struct Jar(
     shared::Env,
     shared::Env_push,
+    shared::Env_len,
     shared::Context,
     debruijin::Indices,
     debruijin::Level,
@@ -72,7 +73,7 @@ impl<DB> ThirDb for DB where
 
 /// Represents the lowering functions for Low-Level Intermediate Representation.
 pub trait ThirLowering {
-    fn thir_eval(&self, env: Env, expr: Expr) -> Value;
+    fn thir_eval(&self, env: Env, term: Term) -> Value;
 
     fn thir_quote(&self, lvl: Level, value: Value) -> Term;
 }

sol-thir/src/shared.rs

@@ -73,6 +73,11 @@ impl Env {
         values.push_front(value);
         Env::new(db, values)
     }
+
+    #[salsa::tracked]
+    pub fn len(self, db: &dyn ThirDb) -> usize {
+        self.values(db).len()
+    }
 }
 
 pub type Meta = usize;

sol-thir/src/source.rs

@@ -15,3 +15,9 @@ pub enum Term {
     Location(Location, Expr),
     Sorry(Location, Option<ThirError>),
 }
+
+impl Term {
+    pub fn normalise(self, db: &dyn ThirDb, env: shared::Env) -> Term {
+        db.thir_quote(Level::new(db, env.len(db)), db.thir_eval(env, self))
+    }
+}

sol-thir/src/value.rs

@@ -33,7 +33,7 @@ impl Value {
 #[derive(Debug, Clone, Hash, PartialEq, Eq)]
 pub struct Closure {
     pub env: shared::Env,
-    pub expr: Expr,
+    pub expr: Term,
 }
 
 impl Closure {