Skip to content

Commit

Permalink
merge: Coercive subtyping fixes + cherry pick from classes (#1131)
Browse files Browse the repository at this point in the history 
Fixes #1130
CP from #1129
  • Loading branch information
@ice1000
ice1000 authored Jul 8, 2024
2 parents f6a0b42 + f3a198a commit e8cf3f8
Show file tree
Hide file tree
Showing 13 changed files with 106 additions and 134 deletions.
5 changes: 5 additions & 0 deletions base/build.gradle.kts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,3 +32,8 @@ val cleanGenerated = tasks.register("cleanGenerated") {
}

tasks.named("clean") { dependsOn(cleanGenerated) }

// Thank you Long
tasks.withType<JavaExec>().configureEach {
jvmArgs( "-Xss32m")
}
3 changes: 0 additions & 3 deletions base/src/main/java/org/aya/normalize/Normalizer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -94,9 +94,6 @@ case CoeTerm(var type, var r, var s) -> {
}
yield defaultValue;
}
// TODO: handle other cases
// ice: what are the other cases?
// h: i don't know
default -> defaultValue;
};
}
Expand Down
39 changes: 28 additions & 11 deletions base/src/main/java/org/aya/tyck/ExprTycker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,7 @@
import org.aya.util.reporter.Reporter;
import org.jetbrains.annotations.Contract;
import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;

import java.util.Comparator;
import java.util.function.Function;
Expand Down Expand Up @@ -136,28 +137,44 @@ case PiTerm(var dom, var cod) -> {
private @NotNull Jdg inheritFallbackUnify(@NotNull Term type, @NotNull Jdg result, @NotNull WithPos<Expr> expr) {
type = whnf(type);
var resultType = result.type();
// Try coercive subtyping for (Path A ...) into (I -> A)
if (type instanceof PiTerm(var dom, var cod) && dom == DimTyTerm.INSTANCE) {
if (whnf(resultType) instanceof EqTerm eq) {
var closure = makeClosurePiPath(expr, eq, cod, result.wellTyped());
if (closure == null) return makeErrorResult(type, result);
return new Jdg.Default(new LamTerm(closure), eq);
}
}
// Try coercive subtyping for (I -> A) into (Path A ...)
if (type instanceof EqTerm eq) {
resultType = whnf(resultType);
if (resultType instanceof PiTerm(var dom, var cod) && dom == DimTyTerm.INSTANCE) {
var ref = new FreeTerm(new LocalVar("i"));
var wellTyped = subscoped(ref.name(), DimTyTerm.INSTANCE, () ->
unifyTyReported(eq.appA(ref), cod.apply(ref), expr));
if (!wellTyped) return result;
var closure = result.wellTyped() instanceof LamTerm(var clo) ? clo
// This is kinda unsafe but it should be fine
: new Closure.Jit(i -> new AppTerm(result.wellTyped(), i));
if (whnf(resultType) instanceof PiTerm(var dom, var cod) && dom == DimTyTerm.INSTANCE) {
var closure = makeClosurePiPath(expr, eq, cod, result.wellTyped());
if (closure == null) return makeErrorResult(type, result);
checkBoundaries(eq, closure, expr.sourcePos(), msg ->
new CubicalError.BoundaryDisagree(expr, msg, new UnifyInfo(state)));
if (expr.data() instanceof Expr.WithTerm with)
addWithTerm(with, expr.sourcePos(), eq);
return new Jdg.Default(new LamTerm(closure), eq);
}
}
if (unifyTyReported(type, resultType, expr)) return result;
return makeErrorResult(type, result);
}

private static @NotNull Jdg makeErrorResult(@NotNull Term type, @NotNull Jdg result) {
return new Jdg.Default(new ErrorTerm(result.wellTyped()), type);
}

private @Nullable Closure makeClosurePiPath(@NotNull WithPos<Expr> expr, EqTerm eq, Closure cod, @NotNull Term core) {
var ref = new FreeTerm(new LocalVar("i"));
var wellTyped = subscoped(ref.name(), DimTyTerm.INSTANCE, () ->
unifyTyReported(eq.appA(ref), cod.apply(ref), expr));
if (!wellTyped) return null;
if (expr.data() instanceof Expr.WithTerm with)
addWithTerm(with, expr.sourcePos(), eq);
return core instanceof LamTerm(var clo) ? clo
// This is kinda unsafe but it should be fine
: new Closure.Jit(i -> new AppTerm(core, i));
}

public @NotNull Term ty(@NotNull WithPos<Expr> expr) {
return switch (expr.data()) {
case Expr.Hole hole -> {
Expand Down
1 change: 1 addition & 0 deletions base/src/test/java/org/aya/syntax/concrete/SyntaxTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ public class SyntaxTest {
prim I
def foo (f : Type -> Type 0) (a : Type 0) =>
[ f a ]
def foo2 => ↑↑ foo
def bar (A : Type 0) : A -> A => fn x => {? x ?}
open inductive Nat | O | S Nat
open inductive Fin Nat
Expand Down
3 changes: 2 additions & 1 deletion cli-impl/src/test/java/org/aya/test/fixtures/GoalAndMeta.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -95,7 +95,8 @@ open inductive List2 (A : Type) | nil2 | cons2 A (List2 A)
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
: Path (fn i ⇒ Vec (+-assoc i) A)
(xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
| [] ⇒ refl
| x :> _ => pmap (x :>) (++-assoc' _ _ _)
""";
Expand Down
126 changes: 40 additions & 86 deletions cli-impl/src/test/resources/negative/GoalAndMeta.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -225,73 +225,25 @@ Info: Solving equation(s) with not very general solution(s)
That looks right!

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

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
8 │ : Path (fn i ⇒ Vec (+-assoc i) A)
9 │ (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 ->
In file $FILE:11:18 ->

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

Error: The solution
Expand All @@ -301,11 +253,11 @@ Error: The solution
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`

In file $FILE:10:25 ->
In file $FILE:11:25 ->

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

Error: Cannot check the expression
Expand All @@ -326,11 +278,11 @@ Error: Cannot check the expression
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 ->
In file $FILE:11:18 ->

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

Error: The solution
Expand All @@ -339,17 +291,19 @@ Error: The solution
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`

In file $FILE:10:12 ->
In file $FILE:11:12 ->

8 │ : Path (fn i ⇒ Vec (+-assoc i) A) (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
9 │ | [] ⇒ refl
10 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | 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)
(=) {?B A x n m o _ ys zs} (x :> ?a A x n m o _ ys zs) (x :> ?b A x n m
o _ ys zs)
(Normalized: (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
Expand All @@ -361,11 +315,11 @@ Error: Cannot check the expression
Vec (+-assoc {suc n} {m} {o} i) A
(Normalized: Vec (suc (+-assoc {n} {m} {o} i)) A)

In file $FILE:10:18 ->
In file $FILE:11:18 ->

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

Error: The solution
Expand All @@ -374,11 +328,11 @@ Error: The solution
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`

In file $FILE:10:18 ->
In file $FILE:11:18 ->

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

Error: The solution
Expand All @@ -387,11 +341,11 @@ Error: The solution
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`

In file $FILE:10:18 ->
In file $FILE:11:18 ->

8 │ : Path (fn i ⇒ Vec (+-assoc i) A) (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
9 │ | [] ⇒ refl
10 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | 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 _)
Expand Down
5 changes: 5 additions & 0 deletions cli-impl/src/test/resources/success/src/Test.aya
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,3 +14,8 @@ module Issue942 {
def what? (m : Nat) : Wrapper (suc m = 0) =>
wrap (\ x => z≠s (pinv x))
}

module Issue1130 {
def f (p : I -> Nat) => 0
def test => f (refl {a := 1})
}
8 changes: 0 additions & 8 deletions parser/src/main/gen/org/aya/parser/AyaPsiParser.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2261,18 +2261,10 @@ public static boolean newExpr(PsiBuilder b, int l) {
r = consumeTokenSmart(b, KW_NEW);
p = r;
r = p && expr(b, l, 0);
r = p && report_error_(b, newExpr_1(b, l + 1)) && r;
exit_section_(b, l, m, NEW_EXPR, r, p, null);
return r || p;
}

// newBody?
private static boolean newExpr_1(PsiBuilder b, int l) {
if (!recursion_guard_(b, l, "newExpr_1")) return false;
newBody(b, l + 1);
return true;
}

public static boolean piExpr(PsiBuilder b, int l) {
if (!recursion_guard_(b, l, "piExpr")) return false;
if (!nextTokenIsSmart(b, KW_PI)) return false;
Expand Down
2 changes: 1 addition & 1 deletion parser/src/main/grammar/AyaPsiParser.bnf
View file
Original file line number Diff line number Diff line change
Expand Up @@ -279,7 +279,7 @@ arrayCompBlock ::= expr BAR <<commaSep doBinding>>
arrayElementsBlock ::= exprList
idiomBlock ::= barred* expr

newExpr ::= KW_NEW expr newBody?
newExpr ::= KW_NEW expr // newBody?
appExpr ::= expr argument+
arrowExpr ::= expr TO expr { rightAssociative = true }
projExpr ::= expr projFix
Expand Down
19 changes: 4 additions & 15 deletions producer/src/main/java/org/aya/producer/AyaProducer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -563,21 +563,10 @@ private record DeclNameOrInfix(@NotNull WithPos<String> name, @Nullable OpDecl.O
var param = new Expr.Param(paramPos, Constants.randomlyNamed(paramPos), expr(expr0), true);
return new WithPos<>(pos, new Expr.Pi(param, to));
}
// if (node.is(NEW_EXPR)) {
// var struct = expr(node.child(EXPR));
// var newBody = node.peekChild(NEW_BODY);
// return new WithPos<>(pos, new Expr.New(pos, struct,
// newBody == null
// ? ImmutableSeq.empty()
// : newBody.childrenOfType(NEW_ARG).map(arg -> {
// var id = newArgField(arg.child(NEW_ARG_FIELD));
// var bindings = arg.childrenOfType(TELE_PARAM_NAME).map(this::teleParamName)
// .map(b -> b.map(_ -> LocalVar.from(b)))
// .toImmutableSeq();
// var body = expr(arg.child(EXPR));
// return new WithPos<>(pos, new Expr.Field<>(sourcePosOf(arg), id, bindings, body, MutableValue.create()));
// }).toImmutableSeq()));
// }
if (node.is(NEW_EXPR)) {
var classCall = expr(node.child(EXPR));
return new WithPos<>(pos, new Expr.New(classCall));
}
if (node.is(PI_EXPR)) return Expr.buildPi(pos,
telescope(node.childrenOfType(TELE)).view(),
expr(node.child(EXPR)));
Expand Down
11 changes: 2 additions & 9 deletions syntax/src/main/java/org/aya/prettier/ConcretePrettier.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -114,7 +114,7 @@ yield visitConcreteCalls(assoc,
var docTele = telescope.map(this::lambdaParam);

prelude.appendAll(docTele);
if (!(body instanceof Expr.Hole)) {
if (!(body instanceof Expr.Hole hole && !hole.explicit())) {
prelude.append(FN_DEFINED_AS);
prelude.append(term(Outer.Free, body));
}
Expand Down Expand Up @@ -142,14 +142,6 @@ yield visitConcreteCalls(assoc,
}
case Expr.LitInt expr -> Doc.plain(String.valueOf(expr.integer()));
case Expr.RawSort e -> Doc.styled(KEYWORD, e.kind().name());
// case Expr.New expr -> Doc.cblock(
// Doc.sep(Doc.styled(KEYWORD, "new"), term(Outer.Free, expr.struct())),
// 2, Doc.vcat(expr.fields().view().map(t ->
// Doc.sep(Doc.symbol("|"), Doc.styled(MEMBER, t.name().data()),
// Doc.emptyIf(t.bindings().isEmpty(), () ->
// Doc.sep(t.bindings().map(v -> varDoc(v.data())))),
// Doc.plain("=>"), term(Outer.Free, t.body()))
// )));
case Expr.Sigma expr -> checkParen(outer, Doc.sep(
KW_SIGMA,
visitTele(expr.params().dropLast(1)),
Expand Down Expand Up @@ -235,6 +227,7 @@ yield visitCalls(null, fn, (_, l) -> l.toDoc(options), outer,
Doc.sep(Doc.styled(KEYWORD, "let"), stmt(letOpen.openCmd()), Doc.styled(KEYWORD, "in")),
Doc.indent(2, term(Outer.Free, letOpen.body()))
);
case Expr.New neu -> Doc.sep(KW_NEW, term(Outer.Free, neu.classCall()));
};
}

Expand Down
1 change: 1 addition & 0 deletions syntax/src/main/java/org/aya/prettier/Tokens.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ private Tokens() {
public static final Doc KW_DEF = Doc.styled(KEYWORD, "def");
public static final Doc KW_DATA = Doc.styled(KEYWORD, "inductive");
public static final Doc KW_CLASS = Doc.styled(KEYWORD, "class");
public static final Doc KW_NEW = Doc.styled(KEYWORD, "new");
public static final Doc PAT_ABSURD = Doc.styled(KEYWORD, "()");
public static final Doc KW_TIGHTER = Doc.styled(KEYWORD, "tighter");
public static final Doc KW_LOOSER = Doc.styled(KEYWORD, "looser");
Expand Down
Loading

0 comments on commit e8cf3f8

Please sign in to comment.