Skip to content

Commit

Permalink
[lang0] occurCheck -- a pass to create FnRecursive from Fn
Browse files Browse the repository at this point in the history
- only in the same module for now
  • Loading branch information
xieyuheng committed Apr 5, 2024
1 parent 20d0d92 commit 4c94062
Show file tree
Hide file tree
Showing 7 changed files with 67 additions and 22 deletions.
5 changes: 1 addition & 4 deletions TODO.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,10 +2,7 @@

> 支持直接递归函数与相互递归函数,不能判断等价的地方就不判断。
[lang0] `occurCheck` -- a pass to create `FnRecursive` from `Fn`

- only in the same module for now

[lang0] `assertEqual` & `assertNotEqual` improve error message
[lang0] `equivalent` -- `FnRecursive`
[lang0] `equivalentNeutral` -- `ApRecursive`

Expand Down
18 changes: 18 additions & 0 deletions docs/lang0/examples/factorial.scm
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
(import "./nat-church.scm" zero? add mul sub1)
(import "./nat-church.scm" zero one two three four)
(import "./boolean.scm" if true false)

;; (claim factorial (-> Nat Nat))

(define (factorial n)
(if (zero? n)
one
(mul n (factorial (sub1 n)))))

factorial

(assert-equal (factorial zero) one)
(assert-equal (factorial one) one)
(assert-equal (factorial two) two)
(assert-equal (factorial three) (mul three two))
(assert-equal (factorial four) (mul four (mul three two)))
20 changes: 6 additions & 14 deletions docs/lang0/examples/nat-even-odd.scm
Original file line number Diff line number Diff line change
Expand Up @@ -3,21 +3,13 @@
(import "./nat-church.scm" one two three four)
(import "./fix.scm" Y)

(define even?
(let ([wrap (lambda (even?)
(lambda (n)
(if (zero? n) true
(if (zero? (sub1 n)) false
(even? (sub1 (sub1 n)))))))])
(Y wrap)))
(define (even? n)
(if (zero? n) true
(odd? (sub1 n))))

(define odd?
(let ([wrap (lambda (odd?)
(lambda (n)
(if (zero? n) false
(if (zero? (sub1 n)) true
(odd? (sub1 (sub1 n)))))))])
(Y wrap)))
(define (odd? n)
(if (zero? n) false
(even? (sub1 n))))

(assert-equal
(even? zero)
Expand Down
16 changes: 15 additions & 1 deletion package-lock.json

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

3 changes: 2 additions & 1 deletion package.json
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,8 @@
"@cicada-lang/framework": "^0.2.0",
"@cicada-lang/sexp": "^0.1.2",
"@xieyuheng/command-line": "^0.1.2",
"@xieyuheng/ty": "^0.2.1"
"@xieyuheng/ty": "^0.2.1",
"dedent": "^1.5.1"
},
"devDependencies": {
"@types/node": "^20.12.4",
Expand Down
25 changes: 24 additions & 1 deletion src/lang0/run/occurCheck.ts
Original file line number Diff line number Diff line change
@@ -1,6 +1,29 @@
import dedent from "dedent"
import type { Definition } from "../definition/Definition.js"
import { expIndirectFreeNames } from "../exp/expIndirectFreeNames.js"
import * as Exps from "../exp/index.js"
import { formatExp } from "../format/formatExp.js"
import type { Mod } from "../mod/index.js"

export function occurCheck(mod: Mod, definition: Definition): void {
// TODO
const indirectFreeNames = expIndirectFreeNames(mod, definition.exp)

if (!indirectFreeNames.has(definition.name)) return

if (definition.exp["@kind"] !== "Fn") {
throw new Error(
dedent`
[occurCheck] Only function can be recursive
non-function exp: ${formatExp(definition.exp)}
recursive name: ${definition.name}
`,
)
}

definition.exp = Exps.FnRecursive(
definition.name,
definition.exp.name,
definition.exp.ret,
)
}
2 changes: 1 addition & 1 deletion src/lang0/run/runMod.ts
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
import { modOwnDefinitions, type Mod } from "../mod/index.js"
import { assertAllNamesDefined } from "./assertAllNamesDefined.js"
import { occurCheck } from "./occurCheck.js"
import { define } from "./define.js"
import { execute } from "./execute.js"
import { occurCheck } from "./occurCheck.js"

export function runMod(mod: Mod): void {
if (mod.isFinished) return
Expand Down

0 comments on commit 4c94062

Please sign in to comment.