[lang0] doAp should not apply a FnRecursive when the arg is `No…

…tYet`

- we need `Neutral` (`Neutral.ApRecursive`) to not apply a value.

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 相关的知识。

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": {

src/lang0/equivalent/equivalentNeutral.ts

@@ -18,5 +18,9 @@ export function equivalentNeutral(
         equivalent(ctx, left.arg, right.arg)
       )
     }
+
+    case "ApRecursive": {
+      throw new Error()
+    }
   }
 }

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,
+  }
+}

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),
+      )
+    }
   }
 }