From bf517781556290db3af4c6133d799160d0e2a962 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 4 Jan 2024 01:14:19 -0500 Subject: [PATCH] qpz --- base/.gitignore | 4 ++++ base/src/main/java/org/aya/base/core/AppTerm.java | 5 ++++- base/src/main/java/org/aya/base/core/LamTerm.java | 4 +++- 3 files changed, 11 insertions(+), 2 deletions(-) create mode 100644 base/.gitignore diff --git a/base/.gitignore b/base/.gitignore new file mode 100644 index 00000000..00597b17 --- /dev/null +++ b/base/.gitignore @@ -0,0 +1,4 @@ +build +.gradle +src/main/gen +src/main/resources/META-INF/native-image diff --git a/base/src/main/java/org/aya/base/core/AppTerm.java b/base/src/main/java/org/aya/base/core/AppTerm.java index b78c8bf6..f2061b85 100644 --- a/base/src/main/java/org/aya/base/core/AppTerm.java +++ b/base/src/main/java/org/aya/base/core/AppTerm.java @@ -5,6 +5,9 @@ public record AppTerm(@NotNull Term fun, @NotNull Term arg) implements Term { @Override public @NotNull Term bindAt(@NotNull LocalVar var, int depth) { - return new AppTerm(fun.bindAt(var, depth), arg.bindAt(var, depth)); + var newFun = fun.bindAt(var, depth); + var newArg = arg.bindAt(var, depth); + if (newFun == fun && newArg == arg) return this; + return new AppTerm(newFun, newArg); } } diff --git a/base/src/main/java/org/aya/base/core/LamTerm.java b/base/src/main/java/org/aya/base/core/LamTerm.java index bc8d4e87..ed305758 100644 --- a/base/src/main/java/org/aya/base/core/LamTerm.java +++ b/base/src/main/java/org/aya/base/core/LamTerm.java @@ -5,6 +5,8 @@ public record LamTerm(Term body) implements Term { @Override public @NotNull Term bindAt(@NotNull LocalVar var, int depth) { - return new LamTerm(body.bindAt(var, depth + 1)); + var newBody = body.bindAt(var, depth + 1); + if (newBody == body) return this; + return new LamTerm(newBody); } }