diff --git a/base/src/main/java/org/aya/normalize/Finalizer.java b/base/src/main/java/org/aya/normalize/Finalizer.java index d5102999e0..dd3d88694e 100644 --- a/base/src/main/java/org/aya/normalize/Finalizer.java +++ b/base/src/main/java/org/aya/normalize/Finalizer.java @@ -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())); diff --git a/base/src/main/java/org/aya/resolve/salt/ExprBinParser.java b/base/src/main/java/org/aya/resolve/salt/ExprBinParser.java index c261e9852f..390fa770da 100644 --- a/base/src/main/java/org/aya/resolve/salt/ExprBinParser.java +++ b/base/src/main/java/org/aya/resolve/salt/ExprBinParser.java @@ -75,8 +75,10 @@ public ExprBinParser(@NotNull ResolveInfo resolveInfo, @NotNull SeqView> 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)); diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java index addb327ae6..5ca96f7888 100644 --- a/base/src/main/java/org/aya/tyck/ExprTycker.java +++ b/base/src/main/java/org/aya/tyck/ExprTycker.java @@ -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())); @@ -160,7 +161,7 @@ case PiTerm(var dom, var cod) -> { public @NotNull Term ty(@NotNull WithPos 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; } @@ -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(); @@ -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); } @@ -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())); diff --git a/base/src/main/java/org/aya/tyck/tycker/Contextful.java b/base/src/main/java/org/aya/tyck/tycker/Contextful.java index b160540eb1..5841c249b9 100644 --- a/base/src/main/java/org/aya/tyck/tycker/Contextful.java +++ b/base/src/main/java/org/aya/tyck/tycker/Contextful.java @@ -62,7 +62,7 @@ default 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); } /** @@ -70,10 +70,10 @@ default R subscoped(@NotNull LocalVar var, @NotNull Term type, @NotNull Supp * * @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.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) { @@ -83,8 +83,8 @@ default 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)); } } diff --git a/cli-impl/src/test/java/org/aya/test/fixtures/GoalAndMeta.java b/cli-impl/src/test/java/org/aya/test/fixtures/GoalAndMeta.java index 07ef883dac..893588215b 100644 --- a/cli-impl/src/test/java/org/aya/test/fixtures/GoalAndMeta.java +++ b/cli-impl/src/test/java/org/aya/test/fixtures/GoalAndMeta.java @@ -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' _ _ _) + """; } diff --git a/cli-impl/src/test/resources/negative/GoalAndMeta.txt b/cli-impl/src/test/resources/negative/GoalAndMeta.txt index a2c8326d28..c85fe1af51 100644 --- a/cli-impl/src/test/resources/negative/GoalAndMeta.txt +++ b/cli-impl/src/test/resources/negative/GoalAndMeta.txt @@ -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 -> @@ -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. + diff --git a/syntax/src/main/java/org/aya/syntax/ref/MetaVar.java b/syntax/src/main/java/org/aya/syntax/ref/MetaVar.java index 262fa9a870..1cdf534490 100644 --- a/syntax/src/main/java/org/aya/syntax/ref/MetaVar.java +++ b/syntax/src/main/java/org/aya/syntax/ref/MetaVar.java @@ -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 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); } diff --git a/tools/src/main/java/org/aya/util/error/SourcePos.java b/tools/src/main/java/org/aya/util/error/SourcePos.java index de64906fd3..1ce0da2bb8 100644 --- a/tools/src/main/java/org/aya/util/error/SourcePos.java +++ b/tools/src/main/java/org/aya/util/error/SourcePos.java @@ -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; @@ -27,7 +27,7 @@ public record SourcePos( int endColumn ) implements Comparable { public SourcePos { - assert tokenEndIndex >= tokenStartIndex; + assert tokenEndIndex >= tokenStartIndex - 1; } /** Single instance SourcePos for mocking tests and other usages. */ @@ -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 params) { return sourcePosForSubExpr(file, params); @@ -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); } }