From 30fa4424f09fd8b02c4462fe009109422b019a89 Mon Sep 17 00:00:00 2001
From: belazy <aarthuur01@gmail.com>
Date: Tue, 27 Dec 2022 12:50:59 +0100
Subject: [PATCH] =?UTF-8?q?Resolve=20"`whnf`=20doesn't=20unfold=20applicat?=
 =?UTF-8?q?ions=20where=20the=20head=20is=20a=20declaration"=20=E2=9C=A8?=
 =?UTF-8?q?=EF=B8=8F=20Closes=20#75=20=F0=9F=90=94=EF=B8=8F=F0=9F=91=8D?=
 =?UTF-8?q?=EF=B8=8F?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

🦀️🍰🦀️🍰🦀️🍰

* chore(clippy): clippy

* fix(kernel): unfold applications where the header is a `Decl`
---
 kernel/src/calculus/term.rs | 33 +++++++++++++++++++++++++++++++--
 1 file changed, 31 insertions(+), 2 deletions(-)

diff --git a/kernel/src/calculus/term.rs b/kernel/src/calculus/term.rs
index 51443c0c..ae32fd5d 100644
--- a/kernel/src/calculus/term.rs
+++ b/kernel/src/calculus/term.rs
@@ -10,13 +10,20 @@ use crate::memory::term::Payload::{Abs, App, Decl, Prod, Sort, Var};
 use crate::memory::term::Term;
 
 impl<'arena> Term<'arena> {
+    fn unfold(self, arena: &mut Arena<'arena>) -> Self {
+        match *self {
+            Decl(decl) => decl.get_term(arena),
+            _ => self,
+        }
+    }
+
     /// Apply one step of β-reduction, using the leftmost-outermost evaluation strategy.
     #[inline]
     #[must_use]
     pub fn beta_reduction(self, arena: &mut Arena<'arena>) -> Self {
         match *self {
             App(t1, t2) => {
-                if let Abs(_, t1) = *t1 {
+                if let Abs(_, t1) = *t1.unfold(arena) {
                     t1.substitute(t2, 1, arena)
                 } else {
                     let t1_new = t1.beta_reduction(arena);
@@ -157,7 +164,7 @@ impl<'arena> Term<'arena> {
     #[must_use]
     pub fn whnf(self, arena: &mut Arena<'arena>) -> Self {
         self.get_whnf_or_init(|| match *self {
-            App(t1, t2) => match *t1.whnf(arena) {
+            App(t1, t2) => match *t1.unfold(arena).whnf(arena) {
                 Abs(_, t1) => {
                     let subst = t1.substitute(t2, 1, arena);
                     subst.whnf(arena)
@@ -334,6 +341,28 @@ mod tests {
         });
     }
 
+    #[test]
+    fn decl_app_whnf() {
+        use crate::memory::term::builder::Builder::*;
+        use_arena(|arena| {
+            let false_ = arena.build_term_raw(prod(prop(), var(0.into(), prop())));
+
+            let decl_ = crate::memory::declaration::InstantiatedDeclaration::instantiate(
+                crate::memory::declaration::builder::Builder::Decl(Abs("x", Prop.into(), Prop.into()).into(), Vec::new())
+                    .realise(arena)
+                    .unwrap(),
+                &Vec::new(),
+                arena,
+            );
+            let decl = crate::memory::term::Term::decl(decl_, arena);
+            let app = crate::memory::term::Term::app(decl, false_, arena);
+            let reduced = arena.build_term_raw(prop());
+
+            assert_eq!(app.beta_reduction(arena), reduced);
+            assert_eq!(app.whnf(arena), reduced);
+        });
+    }
+
     #[test]
     fn shift_prod() {
         use_arena(|arena| {
-- 
GitLab