Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Some error report issues reported by Utensil Song #1120

Merged
merged 5 commits into from
Jun 21, 2024
Merged

Some error report issues reported by Utensil Song #1120

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
616d8cb
binop: generate in a more clever position
ice1000 Jun 21, 2024
dbcc1af
test: add fixture
ice1000 Jun 21, 2024
3a8316e
error: do not report on user holes
ice1000 Jun 21, 2024
bb1f151
binop: fix operator location
ice1000 Jun 21, 2024
4328b18
binop: fix coalesce
ice1000 Jun 21, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion base/src/main/java/org/aya/normalize/Finalizer.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ public Zonk(@NotNull T delegate) {
var result = doZonk(term);
// result shall not be MetaPatTerm
switch (result) {
case MetaCall meta -> fail(new UnsolvedMeta(stack.view()
case MetaCall meta when !meta.ref().isUser() -> fail(new UnsolvedMeta(stack.view()
.drop(1)
.map(this::freezeHoles)
.toImmutableSeq(), meta.ref().pos(), meta.ref().name()));
Expand Down
6 changes: 4 additions & 2 deletions base/src/main/java/org/aya/resolve/salt/ExprBinParser.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,8 +75,10 @@ public ExprBinParser(@NotNull ResolveInfo resolveInfo, @NotNull SeqView<Expr.@No
@Override public @NotNull Expr.NamedArg makeSectionApp(
@NotNull SourcePos pos, Expr.@NotNull NamedArg op, @NotNull Function<Expr.NamedArg, WithPos<Expr>> lamBody
) {
var missing = Constants.randomlyNamed(op.term().sourcePos());
var missingElem = new Expr.NamedArg(true, new WithPos<>(SourcePos.NONE, new Expr.Ref(missing)));
var defPos = op.term().sourcePos();
var missing = Constants.randomlyNamed(defPos);
var missingElem = new Expr.NamedArg(true, new WithPos<>(
defPos.coalesceLeft(), new Expr.Ref(missing)));
var missingParam = new Expr.Param(missing.definition(), missing, true);
var term = new Expr.Lambda(missingParam, lamBody.apply(missingElem));
return new Expr.NamedArg(op.explicit(), new WithPos<>(pos, term));
Expand Down
11 changes: 6 additions & 5 deletions base/src/main/java/org/aya/tyck/ExprTycker.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,8 @@ case PiTerm(var dom, var cod) -> {
default -> fail(expr.data(), type, BadTypeError.absOnNonPi(state, expr, type));
};
case Expr.Hole hole -> {
var freshHole = freshMeta(Constants.randomName(hole), expr.sourcePos(), new MetaVar.OfType(type));
var freshHole = freshMeta(Constants.randomName(hole), expr.sourcePos(),
new MetaVar.OfType(type), hole.explicit());
hole.solution().set(freshHole);
userHoles.append(new WithPos<>(expr.sourcePos(), hole));
if (hole.explicit()) fail(new Goal(state, freshHole, localCtx().clone(), hole.accessibleLocal()));
Expand Down Expand Up @@ -160,7 +161,7 @@ case PiTerm(var dom, var cod) -> {
public @NotNull Term ty(@NotNull WithPos<Expr> expr) {
return switch (expr.data()) {
case Expr.Hole hole -> {
var meta = freshMeta(Constants.randomName(hole), expr.sourcePos(), MetaVar.Misc.IsType);
var meta = freshMeta(Constants.randomName(hole), expr.sourcePos(), MetaVar.Misc.IsType, hole.explicit());
if (hole.explicit()) fail(new Goal(state, meta, localCtx().clone(), hole.accessibleLocal()));
yield meta;
}
Expand Down Expand Up @@ -243,7 +244,7 @@ yield subscoped(param.ref(), wellParam, () ->
var defs = state.shapeFactory.findImpl(AyaShape.NAT_SHAPE);
if (defs.isEmpty()) yield fail(expr.data(), new NoRuleError(expr, null));
if (defs.sizeGreaterThan(1)) {
var type = freshMeta(STR."_ty\{integer}'", expr.sourcePos(), MetaVar.Misc.IsType);
var type = freshMeta(STR."_ty\{integer}'", expr.sourcePos(), MetaVar.Misc.IsType, false);
yield new Jdg.Default(new MetaLitTerm(expr.sourcePos(), integer, defs, type), type);
}
var match = defs.getFirst();
Expand Down Expand Up @@ -280,7 +281,7 @@ yield subscoped(param.ref(), wellParam, () ->
var defs = state.shapeFactory.findImpl(AyaShape.LIST_SHAPE);
if (defs.isEmpty()) yield fail(arr, new NoRuleError(expr, null));
if (defs.sizeGreaterThan(1)) {
var tyMeta = freshMeta("arr_ty", expr.sourcePos(), MetaVar.Misc.IsType);
var tyMeta = freshMeta("arr_ty", expr.sourcePos(), MetaVar.Misc.IsType, false);
var results = elements.map(element -> inherit(element, tyMeta).wellTyped());
yield new Jdg.Default(new MetaLitTerm(expr.sourcePos(), results, defs, tyMeta), tyMeta);
}
Expand All @@ -290,7 +291,7 @@ yield subscoped(param.ref(), wellParam, () ->
// List (A : Type)
var sort = def.signature().telescopeRich(0);
// the sort of type below.
var elementTy = freshMeta(sort.name(), expr.sourcePos(), new MetaVar.OfType(sort.type()));
var elementTy = freshMeta(sort.name(), expr.sourcePos(), new MetaVar.OfType(sort.type()), false);

// do type check
var results = ImmutableTreeSeq.from(elements.map(element -> inherit(element, elementTy).wellTyped()));
Expand Down
10 changes: 5 additions & 5 deletions base/src/main/java/org/aya/tyck/tycker/Contextful.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,18 +62,18 @@ default <R> R subscoped(@NotNull LocalVar var, @NotNull Term type, @NotNull Supp
* Generate a fresh {@link MetaCall} with type {@link Param#type()}
*/
default @NotNull MetaCall mockTerm(@NotNull Param param, @NotNull SourcePos pos) {
return freshMeta(param.name(), pos, new MetaVar.OfType(param.type()));
return freshMeta(param.name(), pos, new MetaVar.OfType(param.type()), false);
}

/**
* Construct a fresh {@link MetaCall}
*
* @see LocalCtx#extract()
*/
default @NotNull MetaCall freshMeta(String name, @NotNull SourcePos pos, MetaVar.Requirement req) {
default @NotNull MetaCall freshMeta(String name, @NotNull SourcePos pos, MetaVar.Requirement req, boolean isUser) {
var vars = localCtx().extract().toImmutableSeq();
var args = vars.<Term>map(FreeTerm::new);
return new MetaCall(new MetaVar(name, pos, args.size(), req.bind(vars.view())), args);
return new MetaCall(new MetaVar(name, pos, args.size(), req.bind(vars.view()), isUser), args);
}

default @NotNull Term generatePi(Expr.@NotNull Lambda expr, SourcePos sourcePos) {
Expand All @@ -83,8 +83,8 @@ default <R> R subscoped(@NotNull LocalVar var, @NotNull Term type, @NotNull Supp

private @NotNull Term generatePi(@NotNull SourcePos pos, @NotNull String name) {
var genName = name + Constants.GENERATED_POSTFIX;
var domain = freshMeta(STR."\{genName}ty", pos, MetaVar.Misc.IsType);
var codomain = freshMeta(STR."\{genName}ret", pos, MetaVar.Misc.IsType);
var domain = freshMeta(STR."\{genName}ty", pos, MetaVar.Misc.IsType, false);
var codomain = freshMeta(STR."\{genName}ret", pos, MetaVar.Misc.IsType, false);
return new PiTerm(domain, Closure.mkConst(codomain));
}
}
13 changes: 13 additions & 0 deletions cli-impl/src/test/java/org/aya/test/fixtures/GoalAndMeta.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -86,4 +86,17 @@ open inductive List2 (A : Type) | nil2 | cons2 A (List2 A)
(xs ++ (ys ++ zs))
((xs ++ ys) ++ zs)
""";

@Language("Aya") String testUtensilFullFile = """
open import data::vec::base
open import arith::nat::base
open import relation::binary::path
variable n m o : Nat
variable A : Type

def ++-assoc' (xs : Vec n A) (ys : Vec m A) (zs : Vec o A)
: Path (fn i ⇒ Vec (+-assoc i) A) (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
| [] ⇒ refl
| x :> _ => pmap (x :>) (++-assoc' _ _ _)
""";
}
190 changes: 180 additions & 10 deletions cli-impl/src/test/resources/negative/GoalAndMeta.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,16 +23,7 @@ Goal: Goal of type
Context:
a : Nat

In file $FILE:2:28 ->

1 │ open import arith::nat::base
2 │ def test (a : Nat) : Nat => {? a ?}
│ ╰─────╯

Error: Unsolved meta _

1 error(s), 0 warning(s).
Let's learn from that.
That looks right!

UnsolvedMetaLit:
In file $FILE:5:17 ->
Expand Down Expand Up @@ -233,3 +224,182 @@ Info: Solving equation(s) with not very general solution(s)

That looks right!

UtensilFullFile:
In file $FILE:8:54 ->

6 │
7 │ def ++-assoc' (xs : Vec n A) (ys : Vec m A) (zs : Vec o A)
8 │ : Path (fn i ⇒ Vec (+-assoc i) A) (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
│ ╰──────────────╯ ╰──────────────╯ ?a
n
A
m
o
xs
ys
zs
0 >= n,
?b
n
A
m
o
xs
ys
zs
0 >= m,
?c
n
A
m
o
xs
ys
zs
0 >= o
│ ╰──────────────╯ ?a
n
A
m
o
xs
ys
zs
1 >= n,
?b
n
A
m
o
xs
ys
zs
1 >= m,
?c
n
A
m
o
xs
ys
zs
1 >= o

Info: Solving equation(s) with not very general solution(s)

In file $FILE:10:18 ->

8 │ : Path (fn i ⇒ Vec (+-assoc i) A) (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
9 │ | [] ⇒ refl
10 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯

Error: The solution
Vec (+-assoc {?n A x n m o _ ys zs} {?m A x n m o _ ys zs} {?o A x n m o _
ys zs} i) (?A A x n m o _ ys zs)
is not well-scoped
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`

In file $FILE:10:25 ->

8 │ : Path (fn i ⇒ Vec (+-assoc i) A) (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
9 │ | [] ⇒ refl
10 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰─────────────╯

Error: Cannot check the expression
++-assoc' _ _ _
of type
(++) {?n A x n m o _ ys zs} {?A A x n m o _ ys zs} {?m A x n m o _ ys zs +
?o A x n m o _ ys zs} (?_ A x n m o _ ys zs) ((++) {?m A x n m o _ ys zs} {?A
A x n m o _ ys zs} {?o A x n m o _ ys zs} (?_ A x n m o _ ys zs) (?_ A x
n m o _ ys zs)) = (++) {?n A x n m o _ ys zs + ?m A x n m o _ ys zs} {?A
A x n m o _ ys zs} {?o A x n m o _ ys zs} ((++) {?n A x n m o _ ys zs} {?A
A x n m o _ ys zs} {?m A x n m o _ ys zs} (?_ A x n m o _ ys zs) (?_ A x
n m o _ ys zs)) (?_ A x n m o _ ys zs)
against the type
?a A x n m o _ ys zs = ?b A x n m o _ ys zs
In particular, we failed to unify
?A A x n m o _ ys zs
with
Vec (+-assoc {?n A x n m o _ ys zs} {?m A x n m o _ ys zs} {?o A x n m o _
ys zs} i) (?A A x n m o _ ys zs)

In file $FILE:10:18 ->

8 │ : Path (fn i ⇒ Vec (+-assoc i) A) (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
9 │ | [] ⇒ refl
10 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯

Error: The solution
Vec (suc (+-assoc {n} {m} {o} i)) A
is not well-scoped
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`

In file $FILE:10:12 ->

8 │ : Path (fn i ⇒ Vec (+-assoc i) A) (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
9 │ | [] ⇒ refl
10 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰───────────────────────────╯

Error: Cannot check the expression
pmap (\ _ ⇒ x :> _) (++-assoc' _ _ _)
of type
(x :> ?a A x n m o _ ys zs) = (x :> ?b A x n m o _ ys zs)
against the type
(++) {suc n} {A} {m + o} (x :> _) ((++) {m} {A} {o} ys zs) = (++) {suc n +
m} {A} {o} ((++) {suc n} {A} {m} (x :> _) ys) zs
(Normalized: (x :> (++) {n} {A} {m + o} _ ((++) {m} {A} {o} ys zs)) = (x :>
(++) {n + m} {A} {o} ((++) {n} {A} {m} _ ys) zs))
In particular, we failed to unify
?B A x n m o _ ys zs
with
Vec (+-assoc {suc n} {m} {o} i) A
(Normalized: Vec (suc (+-assoc {n} {m} {o} i)) A)

In file $FILE:10:18 ->

8 │ : Path (fn i ⇒ Vec (+-assoc i) A) (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
9 │ | [] ⇒ refl
10 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯

Error: The solution
Vec (?n A x n m o _ ys zs _) (?A A x n m o _ ys zs _)
is not well-scoped
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`

In file $FILE:10:18 ->

8 │ : Path (fn i ⇒ Vec (+-assoc i) A) (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
9 │ | [] ⇒ refl
10 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯

Error: The solution
Vec (suc (?n A x n m o _ ys zs _)) (?A A x n m o _ ys zs _)
is not well-scoped
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`

In file $FILE:10:18 ->

8 │ : Path (fn i ⇒ Vec (+-assoc i) A) (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
9 │ | [] ⇒ refl
10 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯
│ ╰──╯ ?B A x n m o _ ys zs >= Vec (suc (?n A x n m
o _ ys zs _)) (?A A x n m o _ ys zs _)
│ ╰╯ ?A A x n m o _ ys zs <= Vec (?n A x n m o _ ys
zs _) (?A A x n m o _ ys zs _)

Error: Equations do not have solutions!

7 error(s), 0 warning(s).
Let's learn from that.

5 changes: 3 additions & 2 deletions syntax/src/main/java/org/aya/syntax/ref/MetaVar.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,14 +26,15 @@
public record MetaVar(
@Override @NotNull String name,
@NotNull SourcePos pos,
int ctxSize, @NotNull Requirement req
int ctxSize, @NotNull Requirement req,
boolean isUser
) implements AnyVar {
@Override public boolean equals(@Nullable Object o) { return this == o; }
@Override public int hashCode() { return System.identityHashCode(this); }

public @NotNull MetaCall asPiDom(@NotNull SortTerm sort, @NotNull ImmutableSeq<Term> args) {
assert req == Misc.IsType;
var typed = new MetaVar(name, pos, ctxSize, new PiDom(sort));
var typed = new MetaVar(name, pos, ctxSize, new PiDom(sort), isUser);
return new MetaCall(typed, args);
}

Expand Down
29 changes: 10 additions & 19 deletions tools/src/main/java/org/aya/util/error/SourcePos.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
package org.aya.util.error;

Expand Down Expand Up @@ -27,7 +27,7 @@ public record SourcePos(
int endColumn
) implements Comparable<SourcePos> {
public SourcePos {
assert tokenEndIndex >= tokenStartIndex;
assert tokenEndIndex >= tokenStartIndex - 1;
}

/** Single instance SourcePos for mocking tests and other usages. */
Expand Down Expand Up @@ -105,13 +105,8 @@ public boolean containsIndex(@NotNull SourcePos x) {
return tokenStartIndex <= x.tokenStartIndex && tokenEndIndex >= x.tokenEndIndex;
}

public boolean belongsToSomeFile() {
return this != SourcePos.NONE && file.isSomeFile();
}

public int linesOfCode() {
return endLine - startLine + 1;
}
public boolean belongsToSomeFile() { return this != SourcePos.NONE && file.isSomeFile(); }
public int linesOfCode() { return endLine - startLine + 1; }

public @NotNull SourcePos sourcePosForSubExpr(@NotNull SeqView<SourcePos> params) {
return sourcePosForSubExpr(file, params);
Expand Down Expand Up @@ -146,15 +141,11 @@ public int hashCode() {
return Objects.hash(tokenStartIndex, tokenEndIndex, startLine, startColumn, endLine, endColumn);
}

@Override public int compareTo(@NotNull SourcePos o) {
return Integer.compare(tokenStartIndex, o.tokenStartIndex);
}

public boolean isEmpty() {
return size() <= 0;
}

private int size() {
return tokenEndIndex - tokenStartIndex + 1;
@Override public int compareTo(@NotNull SourcePos o) { return Integer.compare(tokenStartIndex, o.tokenStartIndex); }
public boolean isEmpty() { return length() <= 0; }
private int length() { return tokenEndIndex - tokenStartIndex + 1; }
public @NotNull SourcePos coalesceLeft() {
return new SourcePos(file, tokenStartIndex, tokenStartIndex - 1,
startLine, startColumn, startLine, startColumn);
}
}
Loading