From 448206436f880c8710cc4c23bc7ecf0752afdbc1 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Wed, 19 Jun 2024 18:25:10 -0400 Subject: [PATCH 1/5] class: hook insert implicit to generate `self` --- base/src/main/java/org/aya/tyck/ExprTycker.java | 14 +++++++++++--- base/src/main/java/org/aya/tyck/StmtTycker.java | 8 ++++++-- .../main/java/org/aya/tyck/tycker/AppTycker.java | 14 ++++---------- .../main/java/org/aya/tyck/tycker/Contextful.java | 2 +- .../org/aya/syntax/telescope/AbstractTele.java | 6 +++--- 5 files changed, 25 insertions(+), 19 deletions(-) diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java index 8b880a5bf..addb327ae 100644 --- a/base/src/main/java/org/aya/tyck/ExprTycker.java +++ b/base/src/main/java/org/aya/tyck/ExprTycker.java @@ -16,6 +16,7 @@ import org.aya.syntax.core.def.PrimDef; import org.aya.syntax.core.repr.AyaShape; import org.aya.syntax.core.term.*; +import org.aya.syntax.core.term.call.ClassCall; import org.aya.syntax.core.term.call.DataCall; import org.aya.syntax.core.term.call.MetaCall; import org.aya.syntax.core.term.repr.IntegerTerm; @@ -331,6 +332,13 @@ case CompiledVar(var content) -> new AppTycker<>(state, sourcePos, args.size(), }; } + private @NotNull Term insertImplicit(@NotNull Param param, @NotNull SourcePos pos) { + if (param.type() instanceof ClassCall clazz) { + // TODO: type checking + return new FreeTerm(state.classThis.peek()); + } else return mockTerm(param, pos); + } + private Jdg computeArgs( @NotNull SourcePos pos, @NotNull ImmutableSeq args, @NotNull AbstractTele params, @NotNull Function k @@ -347,12 +355,12 @@ private Jdg computeArgs( break; } else if (arg.name() == null) { // here, arg.explicit() == true and param.explicit() == false - result[paramIx++] = mockTerm(param, arg.sourcePos()); + result[paramIx++] = insertImplicit(param, arg.sourcePos()); continue; } } if (arg.name() != null && !param.nameEq(arg.name())) { - result[paramIx++] = mockTerm(param, arg.sourcePos()); + result[paramIx++] = insertImplicit(param, arg.sourcePos()); continue; } result[paramIx++] = inherit(arg.arg(), param.type()).wellTyped(); @@ -362,7 +370,7 @@ private Jdg computeArgs( while (paramIx < params.telescopeSize()) { if (params.telescopeLicit(paramIx)) break; var param = params.telescopeRich(paramIx, result); - result[paramIx++] = mockTerm(param, pos); + result[paramIx++] = insertImplicit(param, pos); } var extraParams = MutableStack.>create(); if (argIx < args.size()) { diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java index 6428bcdfd..a8a267602 100644 --- a/base/src/main/java/org/aya/tyck/StmtTycker.java +++ b/base/src/main/java/org/aya/tyck/StmtTycker.java @@ -17,9 +17,11 @@ import org.aya.syntax.core.pat.Pat; import org.aya.syntax.core.pat.PatToTerm; import org.aya.syntax.core.term.*; +import org.aya.syntax.core.term.call.ClassCall; import org.aya.syntax.core.term.call.DataCall; import org.aya.syntax.core.term.xtt.DimTyTerm; import org.aya.syntax.core.term.xtt.EqTerm; +import org.aya.syntax.ref.LocalVar; import org.aya.syntax.ref.MapLocalCtx; import org.aya.syntax.telescope.Signature; import org.aya.tyck.ctx.LocalLet; @@ -164,8 +166,10 @@ private void checkMember(@NotNull ClassMember member, @NotNull ExprTycker tycker signature = signature.pusheen(tycker::whnf) .descent(tycker::zonk) .bindTele(SeqView.of(tycker.state.classThis.pop())); - // TODO: prepend {this: Class} to the telescope - new MemberDef(classRef, member.ref, signature.rawParams(), signature.result()); + // TODO: reconsider these `self` references, they should be locally nameless! + var self = new Param("this", new ClassCall(new LocalVar("self"), + new ClassDef.Delegate(classRef), 0, ImmutableSeq.empty()), false); + new MemberDef(classRef, member.ref, signature.rawParams().prepended(self), signature.result()); member.ref.signature = signature; } diff --git a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java index 77f780378..6225c514a 100644 --- a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java +++ b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java @@ -5,7 +5,6 @@ import kala.collection.Seq; import kala.collection.SeqView; import kala.collection.immutable.ImmutableArray; -import kala.collection.immutable.ImmutableSeq; import kala.function.CheckedBiFunction; import org.aya.generic.stmt.Shaped; import org.aya.syntax.compile.JitCon; @@ -151,17 +150,12 @@ public interface Factory extends } private @NotNull Jdg checkProjCall(@NotNull MemberDefLike member) throws Ex { - var self = new FreeTerm(state.classThis.peek()); - var signature = member.signature().inst(ImmutableSeq.of(self)).lift(lift); + var signature = member.signature().lift(lift); return makeArgs.applyChecked(signature, args -> { - // assert args.length >= 1; - // var fieldArgs = ImmutableArray.fill(args.length - 1, i -> args[i + 1]); - // return new Jdg.Default( - // new FieldCall(args[0], member, 0, fieldArgs), - // signature.result(args) - // ); + assert args.length >= 1; + var fieldArgs = ImmutableArray.fill(args.length - 1, i -> args[i + 1]); return new Jdg.Default( - new MemberCall(self, member, 0, ImmutableArray.from(args)), + new MemberCall(args[0], member, 0, fieldArgs), signature.result(args) ); }); 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 f99204653..b160540eb 100644 --- a/base/src/main/java/org/aya/tyck/tycker/Contextful.java +++ b/base/src/main/java/org/aya/tyck/tycker/Contextful.java @@ -61,7 +61,7 @@ default R subscoped(@NotNull LocalVar var, @NotNull Term type, @NotNull Supp /** * Generate a fresh {@link MetaCall} with type {@link Param#type()} */ - default @NotNull Term mockTerm(@NotNull Param param, @NotNull SourcePos pos) { + default @NotNull MetaCall mockTerm(@NotNull Param param, @NotNull SourcePos pos) { return freshMeta(param.name(), pos, new MetaVar.OfType(param.type())); } diff --git a/syntax/src/main/java/org/aya/syntax/telescope/AbstractTele.java b/syntax/src/main/java/org/aya/syntax/telescope/AbstractTele.java index b10aebede..0f9b8f0c0 100644 --- a/syntax/src/main/java/org/aya/syntax/telescope/AbstractTele.java +++ b/syntax/src/main/java/org/aya/syntax/telescope/AbstractTele.java @@ -141,14 +141,14 @@ record Inst( @NotNull ImmutableSeq args ) implements AbstractTele { @Override public @NotNull Term telescope(int i, Seq teleArgs) { - return signature.telescope(i, args.appendedAll(teleArgs)); + return signature.telescope(i + args.size(), args.appendedAll(teleArgs)); } @Override public @NotNull Term result(Seq teleArgs) { return signature.result(args.appendedAll(teleArgs)); } @Override public int telescopeSize() { return signature.telescopeSize(); } - @Override public boolean telescopeLicit(int i) { return signature.telescopeLicit(i); } - @Override public @NotNull String telescopeName(int i) { return signature.telescopeName(i); } + @Override public boolean telescopeLicit(int i) { return signature.telescopeLicit(i + args.size()); } + @Override public @NotNull String telescopeName(int i) { return signature.telescopeName(i + args.size()); } } } From 66d646ec0c6538036f8b38416a8781db732ba777 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Wed, 19 Jun 2024 18:31:42 -0400 Subject: [PATCH 2/5] class: this now passes tycking --- base/src/main/java/org/aya/tyck/StmtTycker.java | 11 +++++++---- .../java/org/aya/syntax/telescope/AbstractTele.java | 2 +- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java index a8a267602..2c945bfae 100644 --- a/base/src/main/java/org/aya/tyck/StmtTycker.java +++ b/base/src/main/java/org/aya/tyck/StmtTycker.java @@ -157,7 +157,11 @@ else fail(BadTypeError.doNotLike(tycker.state, result, signature.result(), private void checkMember(@NotNull ClassMember member, @NotNull ExprTycker tycker) { if (member.ref.core != null) return; var classRef = member.classRef; - tycker.state.classThis.push(classRef.concrete.self); + var self = classRef.concrete.self; + tycker.state.classThis.push(self); + var classCall = new ClassCall(new LocalVar("self"), + new ClassDef.Delegate(classRef), 0, ImmutableSeq.empty()); + tycker.localCtx().put(self, classCall); var teleTycker = new TeleTycker.Default(tycker); var result = member.result; assert result != null; // See AyaProducer @@ -167,9 +171,8 @@ private void checkMember(@NotNull ClassMember member, @NotNull ExprTycker tycker .descent(tycker::zonk) .bindTele(SeqView.of(tycker.state.classThis.pop())); // TODO: reconsider these `self` references, they should be locally nameless! - var self = new Param("this", new ClassCall(new LocalVar("self"), - new ClassDef.Delegate(classRef), 0, ImmutableSeq.empty()), false); - new MemberDef(classRef, member.ref, signature.rawParams().prepended(self), signature.result()); + var selfParam = new Param("this", classCall, false); + new MemberDef(classRef, member.ref, signature.rawParams().prepended(selfParam), signature.result()); member.ref.signature = signature; } diff --git a/syntax/src/main/java/org/aya/syntax/telescope/AbstractTele.java b/syntax/src/main/java/org/aya/syntax/telescope/AbstractTele.java index 0f9b8f0c0..a1efa8be6 100644 --- a/syntax/src/main/java/org/aya/syntax/telescope/AbstractTele.java +++ b/syntax/src/main/java/org/aya/syntax/telescope/AbstractTele.java @@ -147,7 +147,7 @@ record Inst( @Override public @NotNull Term result(Seq teleArgs) { return signature.result(args.appendedAll(teleArgs)); } - @Override public int telescopeSize() { return signature.telescopeSize(); } + @Override public int telescopeSize() { return signature.telescopeSize() - args.size(); } @Override public boolean telescopeLicit(int i) { return signature.telescopeLicit(i + args.size()); } @Override public @NotNull String telescopeName(int i) { return signature.telescopeName(i + args.size()); } } From 2a5faea00a783a8e2a8bd7a80752f7e0c1793ebd Mon Sep 17 00:00:00 2001 From: ice1000 Date: Wed, 19 Jun 2024 18:32:20 -0400 Subject: [PATCH 3/5] class: add test --- base/src/test/java/org/aya/tyck/TyckTest.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/base/src/test/java/org/aya/tyck/TyckTest.java b/base/src/test/java/org/aya/tyck/TyckTest.java index 0f338a872..bf754a552 100644 --- a/base/src/test/java/org/aya/tyck/TyckTest.java +++ b/base/src/test/java/org/aya/tyck/TyckTest.java @@ -150,9 +150,10 @@ open inductive Phantom Nat Nat (A : Type) | mk A // 🦀 assertTrue(tyck(""" class Monoid - | classifying carrier : Type + | carrier : Type | unit : carrier | op : carrier -> carrier -> carrier + | idl (x : carrier) : op unit x = x """).defs.isNotEmpty()); } From 2ac2168f7e1f739965d84e35f36577aff0b40707 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Wed, 19 Jun 2024 18:35:50 -0400 Subject: [PATCH 4/5] class: bind `ClassCall` `self` --- base/src/main/java/org/aya/tyck/StmtTycker.java | 4 +--- base/src/main/java/org/aya/tyck/tycker/AppTycker.java | 5 ++--- .../main/java/org/aya/syntax/core/term/call/ClassCall.java | 6 ++---- 3 files changed, 5 insertions(+), 10 deletions(-) diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java index 2c945bfae..52d87dd96 100644 --- a/base/src/main/java/org/aya/tyck/StmtTycker.java +++ b/base/src/main/java/org/aya/tyck/StmtTycker.java @@ -21,7 +21,6 @@ import org.aya.syntax.core.term.call.DataCall; import org.aya.syntax.core.term.xtt.DimTyTerm; import org.aya.syntax.core.term.xtt.EqTerm; -import org.aya.syntax.ref.LocalVar; import org.aya.syntax.ref.MapLocalCtx; import org.aya.syntax.telescope.Signature; import org.aya.tyck.ctx.LocalLet; @@ -159,8 +158,7 @@ private void checkMember(@NotNull ClassMember member, @NotNull ExprTycker tycker var classRef = member.classRef; var self = classRef.concrete.self; tycker.state.classThis.push(self); - var classCall = new ClassCall(new LocalVar("self"), - new ClassDef.Delegate(classRef), 0, ImmutableSeq.empty()); + var classCall = new ClassCall(new ClassDef.Delegate(classRef), 0, ImmutableSeq.empty()); tycker.localCtx().put(self, classCall); var teleTycker = new TeleTycker.Default(tycker); var result = member.result; diff --git a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java index 6225c514a..1b8d95b76 100644 --- a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java +++ b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java @@ -138,13 +138,12 @@ public interface Factory extends private @NotNull Jdg checkClassCall(@NotNull ClassDefLike clazz) throws Ex { var appliedParams = ofClassMembers(clazz, argsCount).lift(lift); - // TODO: We may just accept a LocalVar and do subscopedClass in ExprTycker as long as appliedParams won't be affected. var self = LocalVar.generate("self"); state.classThis.push(self); var result = makeArgs.applyChecked(appliedParams, args -> new Jdg.Default( - new ClassCall(self, clazz, 0, ImmutableArray.from(args)), + new ClassCall(clazz, 0, ImmutableArray.from(args)), appliedParams.result(args) - )); + ).bindTele(SeqView.of(self))); state.classThis.pop(); return result; } diff --git a/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java b/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java index 6d1843084..5ead26c2e 100644 --- a/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java +++ b/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java @@ -8,7 +8,6 @@ import org.aya.syntax.core.term.Term; import org.aya.syntax.core.term.marker.Formation; import org.aya.syntax.core.term.marker.StableWHNF; -import org.aya.syntax.ref.LocalVar; import org.jetbrains.annotations.NotNull; /** @@ -22,14 +21,13 @@ * @author kiva, ice1000 */ public record ClassCall( - @NotNull LocalVar self, @NotNull ClassDefLike ref, @Override int ulift, @NotNull ImmutableSeq args ) implements StableWHNF, Formation { public @NotNull ClassCall update(@NotNull ImmutableSeq args) { return this.args.sameElements(args, true) - ? this : new ClassCall(self, ref, ulift, args); + ? this : new ClassCall(ref, ulift, args); } @Override public @NotNull Term descent(@NotNull IndexedFunction f) { @@ -37,6 +35,6 @@ public record ClassCall( } @Override public @NotNull Term doElevate(int level) { - return new ClassCall(self, ref, ulift + level, args); + return new ClassCall(ref, ulift + level, args); } } From 539f018631f4806358bcf81bc4f241ac630abbcd Mon Sep 17 00:00:00 2001 From: ice1000 Date: Wed, 19 Jun 2024 18:39:23 -0400 Subject: [PATCH 5/5] test: fix fixture --- base/src/test/java/org/aya/tyck/TyckTest.java | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/base/src/test/java/org/aya/tyck/TyckTest.java b/base/src/test/java/org/aya/tyck/TyckTest.java index bf754a552..bc92b2188 100644 --- a/base/src/test/java/org/aya/tyck/TyckTest.java +++ b/base/src/test/java/org/aya/tyck/TyckTest.java @@ -37,7 +37,7 @@ public class TyckTest { var result = tyck(""" inductive Nat | O | S Nat inductive FreeMonoid (A : Type) | e | cons A (FreeMonoid A) - + def id {A : Type} (a : A) => a def lam (A : Type) : Fn (a : A) -> Type => fn a => A def tup (A : Type) (B : A -> Type) (a : A) (b : Fn (a : A) -> B a) @@ -66,7 +66,7 @@ def letExample (A : Type) (B : A -> Type) (f : Fn (a : A) -> B a) (a : A) : B a prim I : ISet prim Path (A : I -> Type) (a : A 0) (b : A 1) : Type prim coe (r s : I) (A : I -> Type) : A r -> A s - + def transp (A : I -> Type) (a : A 0) : A 1 => coe 0 1 A a def transpInv (A : I -> Type) (a : A 1) : A 0 => coe 1 0 A a def coeFill0 (A : I -> Type) (u : A 0) : Path A u (transp A u) => \\i => coe 0 i A u @@ -149,6 +149,10 @@ open inductive Phantom Nat Nat (A : Type) | mk A @Test public void classTyck() { // 🦀 assertTrue(tyck(""" + prim I prim Path prim coe + variable A : Type + def infix = (a b : A) => Path (\\i => A) a b + class Monoid | carrier : Type | unit : carrier