Skip to content

Commit

Permalink
misc: I want to eat lamb
Browse files Browse the repository at this point in the history
Co-authored-by: Hoshino Tented <hoshinotented@qq.com>
  • Loading branch information
ice1000 and HoshinoTented committed Dec 13, 2023
1 parent 6fb5542 commit 9a364e9
Show file tree
Hide file tree
Showing 5 changed files with 10 additions and 11 deletions.
4 changes: 2 additions & 2 deletions base/src/main/java/org/aya/core/serde/SerTerm.java
Original file line number Diff line number Diff line change
Expand Up @@ -368,8 +368,8 @@ record SerIntegerOps(
@Override
public @NotNull Shaped.Applicable<Term, ?, ?> deShape(@NotNull DeState state) {
return data.fold(
left -> new IntegerOps.ConRule(state.resolve(this.ref), left.result.de(state), left.data.de(state)),
right -> new IntegerOps.FnRule(state.resolve(this.ref), right)
left -> new IntegerOps.ConRule(state.resolve(ref), left.result.de(state), left.data.de(state)),
right -> new IntegerOps.FnRule(state.resolve(ref), right)

Check warning on line 372 in base/src/main/java/org/aya/core/serde/SerTerm.java

View check run for this annotation

Codecov / codecov/patch

base/src/main/java/org/aya/core/serde/SerTerm.java#L372

Added line #L372 was not covered by tests
);
}
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -16,11 +16,7 @@ Error: The 3rd clause matches on a constructor with condition(s). When checking
posneg 1
Normalized:
pos 0
suc 0
In particular, we failed to unify
zero
with
suc 0
1

1 error(s), 0 warning(s).
What are you doing?
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ In file $FILE:18:4 ->
Error: The 4th clause matches on a constructor with condition(s). When checking
the 1st condition, we failed to unify
zero
(Normalized: 0)
for the arguments:
posneg n 1
Normalized:
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,10 @@ In file $FILE:3:12 ->

Error: The 2nd and the 1st clauses are not confluent because we failed to unify
suc zero
(Normalized: 1)
and
zero
(Normalized: 0)

In file $FILE:5:3 ->

Expand Down
8 changes: 4 additions & 4 deletions ide-lsp/src/test/java/org/aya/lsp/LspTest.java
Original file line number Diff line number Diff line change
Expand Up @@ -51,19 +51,19 @@ public class LspTest {
@Test public void test541() {
launch(TEST_LIB).execute(compile((a, e) -> {
var testOpt = a.lastCompiled()
.filter(x -> x.moduleName().last().equals("Vec"))
.filter(x -> x.moduleName().getLast().equals("Vec"))
.flatMap(x -> x.program().get())
.filterIsInstance(TeleDecl.FnDecl.class)
.filter(x -> x.ref.name().equals("test"))
.firstOption();
.getFirstOption();
assertFalse(testOpt.isEmpty(), "Do not delete the function called test in Vec");
var testClause = ((TeleDecl.BlockBody) testOpt.get().body).clauses().getFirst();
// vnil, ys => 0
var testPat = (Pattern.Bind) testClause.patterns.last().term();
var testPat = (Pattern.Bind) testClause.patterns.getLast().term();
var testTy = assertInstanceOf(DataCall.class, testPat.type().get());
assertNotNull(testTy);
// ys : Vec A m
var lastArg = testTy.args().last().term();
var lastArg = testTy.args().getLast().term();
assertFalse(lastArg instanceof MetaPatTerm);
}));
}
Expand Down

0 comments on commit 9a364e9

Please sign in to comment.