From 93eb874315122fdae4dcc8dc99fa643cfeb38145 Mon Sep 17 00:00:00 2001
From: Xie Yuheng <xyheme@gmail.com>
Date: Thu, 4 Apr 2024 17:13:17 +0800
Subject: [PATCH] [lang0] `doAp` should not apply a `FnRecursive` when the
 `arg` is `NotYet`

- we need `Neutral` (`Neutral.ApRecursive`) to not apply a value.
---
 TODO.md                                   |  4 ++--
 src/lang0/actions/doAp.ts                 | 10 +++++++++-
 src/lang0/equivalent/equivalentNeutral.ts |  4 ++++
 src/lang0/neutral/Neutral.ts              | 20 ++++++++++++++++++--
 src/lang0/readback/readbackNeutral.ts     |  7 +++++++
 5 files changed, 40 insertions(+), 5 deletions(-)

diff --git a/TODO.md b/TODO.md
index 32d62bf..d656b59 100644
--- a/TODO.md
+++ b/TODO.md
@@ -2,9 +2,9 @@
 
 > 支持直接递归函数与相互递归函数，不能判断等价的地方就不判断。
 
+[lang0] `define` -- check occor to create `FnRecursive` instead of `Fn`
 [lang0] `equivalent` -- `FnRecursive`
-[lang0] `doAp` should not apply a `FnRecursive` when the `arg` is `NotYet`
-[lang0] `defineMod` -- check occor to create `FnRecursive` instead of `Fn`
+[lang0] `equivalentNeutral` -- `ApRecursive`
 
 [lang0] 用中文重新整理 lambda encoding 相关的知识，形成一本书。
 [lang0] 用中文重新整理 lambda encoding 和 self type 相关的知识。
diff --git a/src/lang0/actions/doAp.ts b/src/lang0/actions/doAp.ts
index a15d28b..19398ff 100644
--- a/src/lang0/actions/doAp.ts
+++ b/src/lang0/actions/doAp.ts
@@ -15,7 +15,15 @@ export function doAp(target: Value, arg: Value): Value {
     }
 
     case "FnRecursive": {
-      throw new Error()
+      if (arg['@kind'] === 'NotYet') {
+        return Values.NotYet(Neutrals.ApRecursive(target, arg.neutral))
+      }
+
+      return evaluate(
+        target.mod,
+        envExtend(target.env, target.name, arg),
+        target.ret,
+      )
     }
 
     case "Lazy": {
diff --git a/src/lang0/equivalent/equivalentNeutral.ts b/src/lang0/equivalent/equivalentNeutral.ts
index d92d3bb..ee0fd42 100644
--- a/src/lang0/equivalent/equivalentNeutral.ts
+++ b/src/lang0/equivalent/equivalentNeutral.ts
@@ -18,5 +18,9 @@ export function equivalentNeutral(
         equivalent(ctx, left.arg, right.arg)
       )
     }
+
+    case "ApRecursive": {
+      throw new Error()
+    }
   }
 }
diff --git a/src/lang0/neutral/Neutral.ts b/src/lang0/neutral/Neutral.ts
index 476831d..53a6135 100644
--- a/src/lang0/neutral/Neutral.ts
+++ b/src/lang0/neutral/Neutral.ts
@@ -1,6 +1,6 @@
-import { type Value } from "../value/index.js"
+import { type FnRecursive, type Value } from "../value/index.js"
 
-export type Neutral = Var | Ap
+export type Neutral = Var | Ap | ApRecursive
 
 export type Var = {
   "@type": "Neutral"
@@ -31,3 +31,19 @@ export function Ap(target: Neutral, arg: Value): Ap {
     arg,
   }
 }
+
+export type ApRecursive = {
+  "@type": "Neutral"
+  "@kind": "ApRecursive"
+  fn: FnRecursive
+  arg: Neutral
+}
+
+export function ApRecursive(fn: FnRecursive, arg: Neutral): ApRecursive {
+  return {
+    "@type": "Neutral",
+    "@kind": "ApRecursive",
+    fn,
+    arg,
+  }
+}
diff --git a/src/lang0/readback/readbackNeutral.ts b/src/lang0/readback/readbackNeutral.ts
index 9d3637e..6447b70 100644
--- a/src/lang0/readback/readbackNeutral.ts
+++ b/src/lang0/readback/readbackNeutral.ts
@@ -15,5 +15,12 @@ export function readbackNeutral(ctx: ReadbackCtx, neutral: Neutral): Exp {
         readback(ctx, neutral.arg),
       )
     }
+
+    case "ApRecursive": {
+      return Exps.Ap(
+        readback(ctx, neutral.fn),
+        readbackNeutral(ctx, neutral.arg),
+      )
+    }
   }
 }