From c9a4d001621dfc95597db5afdcd5e3fa95c018d0 Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Sat, 5 Aug 2023 02:22:47 +0800 Subject: [PATCH 01/13] term: HcomU --- .../main/java/org/aya/lamett/syntax/Term.java | 31 +++++++++++++++++++ .../main/java/org/aya/lamett/syntax/Type.java | 7 +++++ .../main/java/org/aya/lamett/tyck/KanPDF.java | 9 ++++++ .../java/org/aya/lamett/tyck/Normalizer.java | 8 +++++ 4 files changed, 55 insertions(+) diff --git a/base/src/main/java/org/aya/lamett/syntax/Term.java b/base/src/main/java/org/aya/lamett/syntax/Term.java index 1b0d433..f02d6e8 100644 --- a/base/src/main/java/org/aya/lamett/syntax/Term.java +++ b/base/src/main/java/org/aya/lamett/syntax/Term.java @@ -210,10 +210,41 @@ record Ext(@NotNull Term type, @NotNull F restr) implements Ter record Path(@NotNull ImmutableSeq binders, @NotNull Ext ext) implements Term { } + /// region Cubical Subtype + record Sub(@NotNull Term type, @NotNull Term partEl) implements Term {} record InS(@NotNull Term phi, @NotNull Term of) implements Term {} record OutS(@NotNull Term phi, @NotNull Term partEl, @NotNull Term of) implements Term {} + /// endregion Cubical Subtype + + /// region HcompU + + // Composition type in Kan.pdf, but there is already a class Hcom! So I use HcomU. + record HcomU( + @NotNull Term r /* : I */, + @NotNull Term s /* : I */, + @NotNull LocalVar i /* : I*/, + // @NotNull Cofib φ, // come from PartEl + @NotNull Restr.Cubical A /* Partial (i = r \/ φ) code(U) // under i */ + ) implements Term { + } + + record Box( + @NotNull Term r, @NotNull Term s, + @NotNull Term ceiling /* : A[ i ↦ s ] // under φ */, + @NotNull Term floor /* : Sub (A[ i ↦ r ]) {| φ ↦ coe^{s ~> r}_{λ i, A i} ceiling |} */ + ) implements Term { + } + + record Cap( + @NotNull Term r, @NotNull Term s, + @NotNull Term hcompU /* : HcomU (r ~> s) i A */ + ) implements Term { + } + + /// endregion HcompU + /** Let A be argument, then A i -> A j */ static @NotNull Pi familyI2J(Term term, Term i, Term j) { return (Pi) mkPi(new App(term, i), new App(term, j)); diff --git a/base/src/main/java/org/aya/lamett/syntax/Type.java b/base/src/main/java/org/aya/lamett/syntax/Type.java index 5820e20..39b3a2e 100644 --- a/base/src/main/java/org/aya/lamett/syntax/Type.java +++ b/base/src/main/java/org/aya/lamett/syntax/Type.java @@ -81,6 +81,13 @@ record Sub( } } + record HcomU( + @NotNull Term r, @NotNull Term s, + @NotNull LocalVar i, + @NotNull ImmutableSeq> restrs // under i + ) /* implements Type */ { + } + default @NotNull Type subst(@NotNull LocalVar x, @NotNull Term t) { return subst(MutableMap.of(x, t)); } diff --git a/base/src/main/java/org/aya/lamett/tyck/KanPDF.java b/base/src/main/java/org/aya/lamett/tyck/KanPDF.java index 1648a3e..d0a5d90 100644 --- a/base/src/main/java/org/aya/lamett/tyck/KanPDF.java +++ b/base/src/main/java/org/aya/lamett/tyck/KanPDF.java @@ -1,6 +1,7 @@ package org.aya.lamett.tyck; import kala.collection.mutable.MutableMap; +import org.aya.lamett.syntax.Restr; import org.aya.lamett.syntax.Term; import org.aya.lamett.util.LocalVar; import org.jetbrains.annotations.NotNull; @@ -75,4 +76,12 @@ static Term coeSigma(Term.Sigma sigma, LocalVar i, Term coeR, Term coeS) { var m1 = Term.com(hcomR, hcomS, comType, phi, i, partEl.map2(t -> t.proj(false))); return new Term.Pair(m0.apply(hcomS), m1); } + + static @NotNull Term hcomU( + @NotNull Term hcomR, + @NotNull Term hcomS, + @NotNull LocalVar i, + @NotNull Term.PartEl el) { + return new Term.HcomU(hcomR, hcomS, i, Restr.Cubical.fromPartial(el)); + } } diff --git a/base/src/main/java/org/aya/lamett/tyck/Normalizer.java b/base/src/main/java/org/aya/lamett/tyck/Normalizer.java index 9b215b0..87ec004 100644 --- a/base/src/main/java/org/aya/lamett/tyck/Normalizer.java +++ b/base/src/main/java/org/aya/lamett/tyck/Normalizer.java @@ -163,6 +163,12 @@ yield switch (A) { } yield new Term.OutS(outPhi, outPartEl, outOf); } + case Term.Box(var r, var s, var N, var M) -> { + throw new UnsupportedOperationException("TODO"); // TODO + } + case Term.Cap cap -> { + throw new UnsupportedOperationException("TODO"); // TODO + } }; } @@ -244,6 +250,8 @@ public Term term(Term term) { case Term.Sub(var A, var partEl) -> new Term.Sub(term(A), term(partEl)); case Term.InS(var phi, var of) -> new Term.InS(term(phi), term(of)); case Term.OutS(var phi, var partEl, var of) -> new Term.OutS(term(phi), term(partEl), term(of)); + case Term.Box(var r, var s, var ceil, var floor) -> new Term.Box(term(r), term(s), term(ceil), term(floor)); + case Term.Cap(var r, var s, var hcom) -> new Term.Cap(term(r), term(s), term(hcom)); }; } From aa2af48a36646b82817baea3da976c2ffff12633 Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Sat, 5 Aug 2023 10:53:17 +0800 Subject: [PATCH 02/13] hcomU: normalizer --- .../main/java/org/aya/lamett/syntax/Term.java | 8 +++- .../main/java/org/aya/lamett/tyck/KanPDF.java | 2 +- .../java/org/aya/lamett/tyck/Normalizer.java | 37 ++++++++++++++++--- 3 files changed, 40 insertions(+), 7 deletions(-) diff --git a/base/src/main/java/org/aya/lamett/syntax/Term.java b/base/src/main/java/org/aya/lamett/syntax/Term.java index f02d6e8..28e3015 100644 --- a/base/src/main/java/org/aya/lamett/syntax/Term.java +++ b/base/src/main/java/org/aya/lamett/syntax/Term.java @@ -129,6 +129,10 @@ record PartEl(@NotNull ImmutableSeq> elems) implements public @NotNull PartEl map2(UnaryOperator f) { return new PartEl(elems.map(t -> Tuple.of(t.component1(), f.apply(t.component2())))); } + + public @NotNull Cofib phi() { + return new Cofib(ImmutableSeq.empty(), elems.map(Tuple2::component1)); + } } @@ -226,12 +230,13 @@ record HcomU( @NotNull Term s /* : I */, @NotNull LocalVar i /* : I*/, // @NotNull Cofib φ, // come from PartEl - @NotNull Restr.Cubical A /* Partial (i = r \/ φ) code(U) // under i */ + @NotNull PartEl A /* Partial (i = r \/ φ) code(U) // under i */ ) implements Term { } record Box( @NotNull Term r, @NotNull Term s, + @NotNull Term phi, @NotNull Term ceiling /* : A[ i ↦ s ] // under φ */, @NotNull Term floor /* : Sub (A[ i ↦ r ]) {| φ ↦ coe^{s ~> r}_{λ i, A i} ceiling |} */ ) implements Term { @@ -239,6 +244,7 @@ record Box( record Cap( @NotNull Term r, @NotNull Term s, + @NotNull Term phi, @NotNull Term hcompU /* : HcomU (r ~> s) i A */ ) implements Term { } diff --git a/base/src/main/java/org/aya/lamett/tyck/KanPDF.java b/base/src/main/java/org/aya/lamett/tyck/KanPDF.java index d0a5d90..d97144b 100644 --- a/base/src/main/java/org/aya/lamett/tyck/KanPDF.java +++ b/base/src/main/java/org/aya/lamett/tyck/KanPDF.java @@ -82,6 +82,6 @@ static Term coeSigma(Term.Sigma sigma, LocalVar i, Term coeR, Term coeS) { @NotNull Term hcomS, @NotNull LocalVar i, @NotNull Term.PartEl el) { - return new Term.HcomU(hcomR, hcomS, i, Restr.Cubical.fromPartial(el)); + return new Term.HcomU(hcomR, hcomS, i, el); } } diff --git a/base/src/main/java/org/aya/lamett/tyck/Normalizer.java b/base/src/main/java/org/aya/lamett/tyck/Normalizer.java index 87ec004..7fe9f9e 100644 --- a/base/src/main/java/org/aya/lamett/tyck/Normalizer.java +++ b/base/src/main/java/org/aya/lamett/tyck/Normalizer.java @@ -163,11 +163,37 @@ yield switch (A) { } yield new Term.OutS(outPhi, outPartEl, outOf); } - case Term.Box(var r, var s, var N, var M) -> { - throw new UnsupportedOperationException("TODO"); // TODO + case Term.Box box -> { + var r = term(box.r()); + var s = term(box.s()); + var phi = term(box.phi()); + var ceil = term(box.ceiling()); + var floor = term(box.floor()); + + if (floor instanceof Term.Cap cap && phi instanceof Term.Cofib coffee) { + // unique rule + var success = unifier.withCofibDisj(coffee.conjs(), () -> + unifier.untyped(ceil, cap.hcompU()), + true); + if (success) { + yield term(cap.hcompU()); + } + } + + yield new Term.Box(r, s, phi, ceil, floor); } case Term.Cap cap -> { - throw new UnsupportedOperationException("TODO"); // TODO + var r = term(cap.r()); + var s = term(cap.s()); + var phi = term(cap.phi()); + var hcomU = term(cap.hcompU()); + + if (hcomU instanceof Term.Box box) { + // computation rule + yield term(box.floor()); + } + + yield new Term.Cap(r, s, phi, hcomU); } }; } @@ -250,8 +276,9 @@ public Term term(Term term) { case Term.Sub(var A, var partEl) -> new Term.Sub(term(A), term(partEl)); case Term.InS(var phi, var of) -> new Term.InS(term(phi), term(of)); case Term.OutS(var phi, var partEl, var of) -> new Term.OutS(term(phi), term(partEl), term(of)); - case Term.Box(var r, var s, var ceil, var floor) -> new Term.Box(term(r), term(s), term(ceil), term(floor)); - case Term.Cap(var r, var s, var hcom) -> new Term.Cap(term(r), term(s), term(hcom)); + case Term.Box(var r, var s, var phi, var ceil, var floor) -> + new Term.Box(term(r), term(s), term(phi), term(ceil), term(floor)); + case Term.Cap(var r, var s, var phi, var hcom) -> new Term.Cap(term(r), term(s), term(phi), term(hcom)); }; } From 96e12d8e0c66c69cd1344396d8e04d1415d1cc3f Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Sat, 5 Aug 2023 14:31:12 +0800 Subject: [PATCH 03/13] hcomU: correct impl --- base/src/main/java/org/aya/lamett/tyck/Normalizer.java | 1 + 1 file changed, 1 insertion(+) diff --git a/base/src/main/java/org/aya/lamett/tyck/Normalizer.java b/base/src/main/java/org/aya/lamett/tyck/Normalizer.java index 7fe9f9e..785d0cb 100644 --- a/base/src/main/java/org/aya/lamett/tyck/Normalizer.java +++ b/base/src/main/java/org/aya/lamett/tyck/Normalizer.java @@ -1,5 +1,6 @@ package org.aya.lamett.tyck; +import kala.collection.SeqView; import kala.collection.immutable.ImmutableSeq; import kala.collection.mutable.MutableMap; import kala.tuple.Tuple; From cb1b425c8f9e471bcc66aacfeec2d87cdf056d3e Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Sat, 5 Aug 2023 17:54:48 +0800 Subject: [PATCH 04/13] hcomU: remove `HcomU` , use `hcom ... U` instead --- .../main/java/org/aya/lamett/syntax/Term.java | 16 ++++++++-------- .../main/java/org/aya/lamett/syntax/Type.java | 6 +++++- .../main/java/org/aya/lamett/tyck/KanPDF.java | 8 -------- .../main/java/org/aya/lamett/tyck/Unifier.java | 1 + .../java/org/aya/lamett/tyck/WeaklyTarski.java | 8 ++++++++ 5 files changed, 22 insertions(+), 17 deletions(-) diff --git a/base/src/main/java/org/aya/lamett/syntax/Term.java b/base/src/main/java/org/aya/lamett/syntax/Term.java index 28e3015..c724c01 100644 --- a/base/src/main/java/org/aya/lamett/syntax/Term.java +++ b/base/src/main/java/org/aya/lamett/syntax/Term.java @@ -225,14 +225,14 @@ record OutS(@NotNull Term phi, @NotNull Term partEl, @NotNull Term of) implement /// region HcompU // Composition type in Kan.pdf, but there is already a class Hcom! So I use HcomU. - record HcomU( - @NotNull Term r /* : I */, - @NotNull Term s /* : I */, - @NotNull LocalVar i /* : I*/, - // @NotNull Cofib φ, // come from PartEl - @NotNull PartEl A /* Partial (i = r \/ φ) code(U) // under i */ - ) implements Term { - } + // record HcomU( + // @NotNull Term r /* : I */, + // @NotNull Term s /* : I */, + // @NotNull LocalVar i /* : I*/, + // // @NotNull Cofib φ, // come from PartEl + // @NotNull PartEl A /* Partial (i = r \/ φ) code(U) // under i */ + // ) implements Term { + // } record Box( @NotNull Term r, @NotNull Term s, diff --git a/base/src/main/java/org/aya/lamett/syntax/Type.java b/base/src/main/java/org/aya/lamett/syntax/Type.java index 39b3a2e..07cc0b3 100644 --- a/base/src/main/java/org/aya/lamett/syntax/Type.java +++ b/base/src/main/java/org/aya/lamett/syntax/Type.java @@ -85,7 +85,11 @@ record HcomU( @NotNull Term r, @NotNull Term s, @NotNull LocalVar i, @NotNull ImmutableSeq> restrs // under i - ) /* implements Type */ { + ) implements Type { + @Override + public @NotNull Doc toDoc() { + return Doc.plain("HcomU"); + } } default @NotNull Type subst(@NotNull LocalVar x, @NotNull Term t) { diff --git a/base/src/main/java/org/aya/lamett/tyck/KanPDF.java b/base/src/main/java/org/aya/lamett/tyck/KanPDF.java index d97144b..35b9334 100644 --- a/base/src/main/java/org/aya/lamett/tyck/KanPDF.java +++ b/base/src/main/java/org/aya/lamett/tyck/KanPDF.java @@ -76,12 +76,4 @@ static Term coeSigma(Term.Sigma sigma, LocalVar i, Term coeR, Term coeS) { var m1 = Term.com(hcomR, hcomS, comType, phi, i, partEl.map2(t -> t.proj(false))); return new Term.Pair(m0.apply(hcomS), m1); } - - static @NotNull Term hcomU( - @NotNull Term hcomR, - @NotNull Term hcomS, - @NotNull LocalVar i, - @NotNull Term.PartEl el) { - return new Term.HcomU(hcomR, hcomS, i, el); - } } diff --git a/base/src/main/java/org/aya/lamett/tyck/Unifier.java b/base/src/main/java/org/aya/lamett/tyck/Unifier.java index e1198bf..a00dd98 100644 --- a/base/src/main/java/org/aya/lamett/tyck/Unifier.java +++ b/base/src/main/java/org/aya/lamett/tyck/Unifier.java @@ -104,6 +104,7 @@ && untypedInner(ldt.param().type(), rdt.param().type()) case Term.INeg(var ll) when r instanceof Term.INeg(var rr) -> untypedInner(ll, rr); case Term.Coe(var r1, var s1, var A1) when r instanceof Term.Coe(var r2, var s2, var A2) -> untypedInner(r1, r2) && untypedInner(s1, s2) && untypedInner(A1, A2); + case Term.Hcom hcom -> throw new UnsupportedOperationException(); default -> false; }; if (!happy && data == null) data = new FailureData(l, r); diff --git a/base/src/main/java/org/aya/lamett/tyck/WeaklyTarski.java b/base/src/main/java/org/aya/lamett/tyck/WeaklyTarski.java index 2565666..22dd3b3 100644 --- a/base/src/main/java/org/aya/lamett/tyck/WeaklyTarski.java +++ b/base/src/main/java/org/aya/lamett/tyck/WeaklyTarski.java @@ -1,6 +1,7 @@ package org.aya.lamett.tyck; import org.aya.lamett.syntax.Cofib; +import kala.tuple.Tuple; import org.aya.lamett.syntax.Keyword; import org.aya.lamett.syntax.Term; import org.aya.lamett.syntax.Type; @@ -25,6 +26,13 @@ public record WeaklyTarski(@NotNull Normalizer n) { case Term.PartTy(var c, var type) when c instanceof Cofib cofib -> new Type.PartTy(el(type), n.term(cofib)); case Term.Sub(var A, var p) when p instanceof Term.PartEl partEl -> new Type.Sub(el(A), partEl.elems()); + // composition type + case Term.Hcom hcom when hcom.A() instanceof Term.Lit tyLit && tyLit.keyword() == Keyword.U -> { + // hcom is wellTyped, then hcom.el has type `Partial U (i = r ∨ φ) {| ... |}` + // constructing `Partial Type (i = r ∨ φ) {| ... |}` from hcom.el + var tyPartEl = hcom.el().elems().map(x -> Tuple.of(x.component1(), el(x.component2()))); + yield new Type.HcomU(hcom.r(), hcom.s(), hcom.i(), tyPartEl); + } case Term misc -> new Type.El(misc); }; } From 5311a2f8768bb087fff92a4fc8848488418258c8 Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Sun, 6 Aug 2023 22:00:08 +0800 Subject: [PATCH 05/13] hcom: correct property again --- base/src/main/java/org/aya/lamett/syntax/Term.java | 4 ++++ base/src/main/java/org/aya/lamett/tyck/Normalizer.java | 1 + 2 files changed, 5 insertions(+) diff --git a/base/src/main/java/org/aya/lamett/syntax/Term.java b/base/src/main/java/org/aya/lamett/syntax/Term.java index c724c01..af54ff7 100644 --- a/base/src/main/java/org/aya/lamett/syntax/Term.java +++ b/base/src/main/java/org/aya/lamett/syntax/Term.java @@ -7,13 +7,16 @@ import kala.tuple.Tuple2; import org.aya.lamett.tyck.Normalizer; import org.aya.lamett.tyck.Unification; +import org.aya.lamett.tyck.Unifier; import org.aya.lamett.util.Distiller; import org.aya.lamett.util.LocalVar; import org.aya.lamett.util.Param; import org.aya.pretty.doc.Doc; import org.aya.pretty.doc.Docile; import org.jetbrains.annotations.NotNull; +import org.jetbrains.annotations.Nullable; +import java.util.function.Predicate; import java.util.function.UnaryOperator; public sealed interface Term extends Docile permits Cofib, Cofib.Eq, Term.App, Term.Coe, Term.ConCall, Term.DT, Term.DataCall, @@ -52,6 +55,7 @@ record Lam(@NotNull LocalVar x, @NotNull Term body) implements Term { static @NotNull Term mkLam(@NotNull SeqView telescope, @NotNull Term body) { return telescope.foldRight(body, Lam::new); } + default @NotNull Term app(@NotNull Term... args) { var f = this; for (var a : args) f = f instanceof Lam lam ? lam.body.subst(lam.x, a) : new App(f, a); diff --git a/base/src/main/java/org/aya/lamett/tyck/Normalizer.java b/base/src/main/java/org/aya/lamett/tyck/Normalizer.java index 785d0cb..16b2632 100644 --- a/base/src/main/java/org/aya/lamett/tyck/Normalizer.java +++ b/base/src/main/java/org/aya/lamett/tyck/Normalizer.java @@ -52,6 +52,7 @@ public Type type(Type type) { case Type.Sigma sig -> new Type.Sigma(new Param<>(sig.param().x(), type(sig.param().type())), type(sig.cod())); case Type.PartTy partTy -> new Type.PartTy(type(partTy.underlying()), term(partTy.restrs())); case Type.Sub sub -> new Type.Sub(type(sub.underlying()), partEl(sub.restrs())); + case Type.HcomU hcomU -> Type.Lit.U; }; } From 2654a70a3314f2ee0dd6bb5b2664e933650ec974 Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Sun, 6 Aug 2023 22:15:31 +0800 Subject: [PATCH 06/13] misc: fix compile --- base/src/main/java/org/aya/lamett/syntax/Term.java | 4 ++-- base/src/main/java/org/aya/lamett/syntax/Type.java | 2 +- base/src/main/java/org/aya/lamett/tyck/Normalizer.java | 2 +- base/src/main/java/org/aya/lamett/util/Distiller.java | 2 ++ 4 files changed, 6 insertions(+), 4 deletions(-) diff --git a/base/src/main/java/org/aya/lamett/syntax/Term.java b/base/src/main/java/org/aya/lamett/syntax/Term.java index af54ff7..dad2f6b 100644 --- a/base/src/main/java/org/aya/lamett/syntax/Term.java +++ b/base/src/main/java/org/aya/lamett/syntax/Term.java @@ -21,7 +21,7 @@ public sealed interface Term extends Docile permits Cofib, Cofib.Eq, Term.App, Term.Coe, Term.ConCall, Term.DT, Term.DataCall, Term.Error, Term.Ext, Term.FnCall, Term.Hcom, Term.INeg, Term.InS, Term.Lam, Term.Lit, Term.OutS, Term.Pair, Term.PartEl, - Term.PartTy, Term.Path, Term.Proj, Term.Ref, Term.Sub { + Term.PartTy, Term.Path, Term.Proj, Term.Ref, Term.Sub, Term.Box, Term.Cap { @Override default @NotNull Doc toDoc() { return Distiller.term(this, Distiller.Prec.Free); } @@ -135,7 +135,7 @@ record PartEl(@NotNull ImmutableSeq> elems) implements } public @NotNull Cofib phi() { - return new Cofib(ImmutableSeq.empty(), elems.map(Tuple2::component1)); + return new Cofib(elems.map(Tuple2::component1)); } } diff --git a/base/src/main/java/org/aya/lamett/syntax/Type.java b/base/src/main/java/org/aya/lamett/syntax/Type.java index 07cc0b3..504b28f 100644 --- a/base/src/main/java/org/aya/lamett/syntax/Type.java +++ b/base/src/main/java/org/aya/lamett/syntax/Type.java @@ -84,7 +84,7 @@ record Sub( record HcomU( @NotNull Term r, @NotNull Term s, @NotNull LocalVar i, - @NotNull ImmutableSeq> restrs // under i + @NotNull ImmutableSeq> restrs // under i ) implements Type { @Override public @NotNull Doc toDoc() { diff --git a/base/src/main/java/org/aya/lamett/tyck/Normalizer.java b/base/src/main/java/org/aya/lamett/tyck/Normalizer.java index 16b2632..4bd1e63 100644 --- a/base/src/main/java/org/aya/lamett/tyck/Normalizer.java +++ b/base/src/main/java/org/aya/lamett/tyck/Normalizer.java @@ -172,7 +172,7 @@ yield switch (A) { var ceil = term(box.ceiling()); var floor = term(box.floor()); - if (floor instanceof Term.Cap cap && phi instanceof Term.Cofib coffee) { + if (floor instanceof Term.Cap cap && phi instanceof Cofib coffee) { // unique rule var success = unifier.withCofibDisj(coffee.conjs(), () -> unifier.untyped(ceil, cap.hcompU()), diff --git a/base/src/main/java/org/aya/lamett/util/Distiller.java b/base/src/main/java/org/aya/lamett/util/Distiller.java index eba21b5..56e7460 100644 --- a/base/src/main/java/org/aya/lamett/util/Distiller.java +++ b/base/src/main/java/org/aya/lamett/util/Distiller.java @@ -160,6 +160,8 @@ enum Prec { case Term.Sub(Term A, Term partEl) -> call(envPrec, "Sub", A, Doc.plain("φ"), partEl); case Term.InS(var phi, var of) -> insideOut(envPrec, phi, of, "inS"); case Term.OutS(var phi, var partEl, var of) -> insideOut(envPrec, phi, of, "outS"); + case Term.Box box -> throw new UnsupportedOperationException("TODO"); + case Term.Cap cap -> throw new UnsupportedOperationException("TODO"); }; } From 82c8a37c8411dd5fbb2329f91db52540210e91c5 Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Mon, 7 Aug 2023 03:03:35 +0800 Subject: [PATCH 07/13] misc: useless document --- .../main/java/org/aya/lamett/syntax/Term.java | 10 +++++- .../org/aya/lamett/tyck/WeaklyTarski.java | 2 +- base/src/test/java/TermTest.java | 34 +++++++++++++++++++ 3 files changed, 44 insertions(+), 2 deletions(-) create mode 100644 base/src/test/java/TermTest.java diff --git a/base/src/main/java/org/aya/lamett/syntax/Term.java b/base/src/main/java/org/aya/lamett/syntax/Term.java index dad2f6b..5fb17c7 100644 --- a/base/src/main/java/org/aya/lamett/syntax/Term.java +++ b/base/src/main/java/org/aya/lamett/syntax/Term.java @@ -16,6 +16,7 @@ import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.Nullable; +import java.util.function.Function; import java.util.function.Predicate; import java.util.function.UnaryOperator; @@ -56,6 +57,11 @@ record Lam(@NotNull LocalVar x, @NotNull Term body) implements Term { return telescope.foldRight(body, Lam::new); } + static @NotNull Term mkLam(@NotNull String name, @NotNull Function closeBody) { + var i = new LocalVar(name); + return new Lam(i, closeBody.apply(i)); + } + default @NotNull Term app(@NotNull Term... args) { var f = this; for (var a : args) f = f instanceof Lam lam ? lam.body.subst(lam.x, a) : new App(f, a); @@ -242,7 +248,9 @@ record Box( @NotNull Term r, @NotNull Term s, @NotNull Term phi, @NotNull Term ceiling /* : A[ i ↦ s ] // under φ */, - @NotNull Term floor /* : Sub (A[ i ↦ r ]) {| φ ↦ coe^{s ~> r}_{λ i, A i} ceiling |} */ + @NotNull Term floor + /* : A[ i ↦ r ] for user + * : Sub (A[ i ↦ r ]) {| φ ↦ coe^{s ~> r}_{λ i, A i} ceiling |} for compiler */ ) implements Term { } diff --git a/base/src/main/java/org/aya/lamett/tyck/WeaklyTarski.java b/base/src/main/java/org/aya/lamett/tyck/WeaklyTarski.java index 22dd3b3..8fa1e47 100644 --- a/base/src/main/java/org/aya/lamett/tyck/WeaklyTarski.java +++ b/base/src/main/java/org/aya/lamett/tyck/WeaklyTarski.java @@ -28,7 +28,7 @@ public record WeaklyTarski(@NotNull Normalizer n) { new Type.Sub(el(A), partEl.elems()); // composition type case Term.Hcom hcom when hcom.A() instanceof Term.Lit tyLit && tyLit.keyword() == Keyword.U -> { - // hcom is wellTyped, then hcom.el has type `Partial U (i = r ∨ φ) {| ... |}` + // hcom is wellTyped, then hcom.el has type `Partial U φ {| ... |}` // constructing `Partial Type (i = r ∨ φ) {| ... |}` from hcom.el var tyPartEl = hcom.el().elems().map(x -> Tuple.of(x.component1(), el(x.component2()))); yield new Type.HcomU(hcom.r(), hcom.s(), hcom.i(), tyPartEl); diff --git a/base/src/test/java/TermTest.java b/base/src/test/java/TermTest.java new file mode 100644 index 0000000..8c9d371 --- /dev/null +++ b/base/src/test/java/TermTest.java @@ -0,0 +1,34 @@ +import kala.collection.immutable.ImmutableSeq; +import org.aya.lamett.syntax.Cofib; +import org.aya.lamett.syntax.Term; +import org.aya.lamett.tyck.Normalizer; +import org.aya.lamett.tyck.Unification; +import org.aya.lamett.util.LocalVar; +import org.junit.jupiter.api.Test; + +public class TermTest { + @Test + public void waitForice1000sGrammar() { + var unification = new Unification(); + var nf = new Normalizer(unification); + + var phi = new LocalVar("φ"); + var A = new LocalVar("A"); // I → Partial (i = r ∨ φ) U + var u0 = new LocalVar("u0"); // A r + var refPhi = new Term.Ref(phi); + var refA = new Term.Ref(A); + var refU0 = new Term.Ref(u0); + + unification.addNFConj(new Cofib.Conj(ImmutableSeq.of(refPhi))); + + // coe (r ~> s) (λ i. A i) u0 + var halfCoe = new Term.Coe(Term.Lit.Zero, Term.Lit.One, Term.mkLam("i", i -> new Term.App(refA, new Term.Ref(i)))); + var ceiling = new Term.App(halfCoe, refU0); + var box = new Term.Box(Term.Lit.Zero, Term.Lit.One, refPhi, ceiling, refU0); + var cap = new Term.Cap(Term.Lit.Zero, Term.Lit.One, refPhi, box); + + var result = nf.term(cap); + var box2 = new Term.Box(Term.Lit.Zero, Term.Lit.One, refPhi, ceiling, cap); + var result2 = nf.term(box2); + } +} From 51d719cbf9d293a79c95850d3e5103b60db1434b Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Tue, 8 Aug 2023 02:32:01 +0800 Subject: [PATCH 08/13] git: rebase --onto main --- .../main/java/org/aya/lamett/tyck/Normalizer.java | 2 +- .../main/java/org/aya/lamett/tyck/WeaklyTarski.java | 13 +++++++++---- 2 files changed, 10 insertions(+), 5 deletions(-) diff --git a/base/src/main/java/org/aya/lamett/tyck/Normalizer.java b/base/src/main/java/org/aya/lamett/tyck/Normalizer.java index 4bd1e63..7d9c8f8 100644 --- a/base/src/main/java/org/aya/lamett/tyck/Normalizer.java +++ b/base/src/main/java/org/aya/lamett/tyck/Normalizer.java @@ -174,7 +174,7 @@ yield switch (A) { if (floor instanceof Term.Cap cap && phi instanceof Cofib coffee) { // unique rule - var success = unifier.withCofibDisj(coffee.conjs(), () -> + var success = unifier.withCofib(coffee, () -> unifier.untyped(ceil, cap.hcompU()), true); if (success) { diff --git a/base/src/main/java/org/aya/lamett/tyck/WeaklyTarski.java b/base/src/main/java/org/aya/lamett/tyck/WeaklyTarski.java index 8fa1e47..6946b87 100644 --- a/base/src/main/java/org/aya/lamett/tyck/WeaklyTarski.java +++ b/base/src/main/java/org/aya/lamett/tyck/WeaklyTarski.java @@ -5,6 +5,7 @@ import org.aya.lamett.syntax.Keyword; import org.aya.lamett.syntax.Term; import org.aya.lamett.syntax.Type; +import org.aya.lamett.util.LocalVar; import org.aya.lamett.util.Param; import org.jetbrains.annotations.NotNull; @@ -28,10 +29,14 @@ public record WeaklyTarski(@NotNull Normalizer n) { new Type.Sub(el(A), partEl.elems()); // composition type case Term.Hcom hcom when hcom.A() instanceof Term.Lit tyLit && tyLit.keyword() == Keyword.U -> { - // hcom is wellTyped, then hcom.el has type `Partial U φ {| ... |}` - // constructing `Partial Type (i = r ∨ φ) {| ... |}` from hcom.el - var tyPartEl = hcom.el().elems().map(x -> Tuple.of(x.component1(), el(x.component2()))); - yield new Type.HcomU(hcom.r(), hcom.s(), hcom.i(), tyPartEl); + // hcom is wellTyped, then hcom.u has type `I -> Partial U (i = r ∨ φ) {| ... |}` + // constructing `Partial Type (i = r ∨ φ) {| ... |}` from hcom.u under our `i` + var i = new LocalVar("i"); + var inner = n.term(hcom.u().app(new Term.Ref(i))); + if (inner instanceof Term.PartEl partEl) { + var tyInner = partEl.elems().map(x -> Tuple.of(x.component1(), el(x.component2()))); + yield new Type.HcomU(hcom.r(), hcom.s(), i, tyInner); + } else yield new Type.El(hcom); } case Term misc -> new Type.El(misc); }; From 7f8c0332acff29cdcd1084f83b82e80bbdfe0417 Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Sat, 12 Aug 2023 09:55:14 +0800 Subject: [PATCH 09/13] hcomU: metalanguage-level term --- .../main/java/org/aya/lamett/syntax/Term.java | 53 +++++++++-- .../java/org/aya/lamett/tyck/Elaborator.java | 2 + .../java/org/aya/lamett/tyck/Normalizer.java | 93 +++++++++++++------ 3 files changed, 116 insertions(+), 32 deletions(-) diff --git a/base/src/main/java/org/aya/lamett/syntax/Term.java b/base/src/main/java/org/aya/lamett/syntax/Term.java index 5fb17c7..bc25e0f 100644 --- a/base/src/main/java/org/aya/lamett/syntax/Term.java +++ b/base/src/main/java/org/aya/lamett/syntax/Term.java @@ -37,7 +37,12 @@ public sealed interface Term extends Docile permits Cofib, Cofib.Eq, Term.App, T } record Error(@NotNull String msg) implements Term {} - record Ref(@NotNull LocalVar var) implements Term {} + record Ref(@NotNull LocalVar var) implements Term { + // For import static + public static @NotNull Term.Ref ref(@NotNull LocalVar var) { + return new Ref(var); + } + } record FnCall(@NotNull DefVar fn, @NotNull ImmutableSeq args) implements Term {} record DataCall(@NotNull DefVar fn, @NotNull ImmutableSeq args) implements Term {} record ConCall(@NotNull DefVar fn, @NotNull ImmutableSeq args, @@ -143,6 +148,15 @@ record PartEl(@NotNull ImmutableSeq> elems) implements public @NotNull Cofib phi() { return new Cofib(elems.map(Tuple2::component1)); } + + /** + * Returns the first clause who makes simplifier happy. + * + * @param simplifier a simplifier, should confluent. + */ + public @Nullable Tuple2 simplifyUnder(@NotNull Predicate simplifier) { + return elems.firstOrNull(pair -> simplifier.test(pair.component1())); + } } @@ -210,6 +224,19 @@ record Hcom(@NotNull Term r, @NotNull Term s, @NotNull Term A, @NotNull Term phi return new Hcom(r, s, A.app(s), phi, mkPi(ImmutableSeq.of(new Param<>(i, Lit.I)), newEl)); } + /** + * 
+   * Γ ⊢ {@param A}   : U
+   * Γ ⊢ {@param phi} : F
+   * Γ ⊢ {@param u}   : {@link PartTy} phi A
+   * -------------------------------------------
+   * Γ, phi ⊢ outPartial A phi u = hcom 0 1 phi (λ i. u) : A
+   *
+ */ + static @NotNull Term outPartial(@NotNull Term A, @NotNull Term phi, @NotNull Term u) { + return new Hcom(Lit.Zero, Lit.One, A, phi, mkLam("i", $ -> u)); + } + /** * Generalized extension type. * @@ -244,20 +271,34 @@ record OutS(@NotNull Term phi, @NotNull Term partEl, @NotNull Term of) implement // ) implements Term { // } + /** + * 
+   * Γ ⊢ {@param r} {@param s} : I
+   * Γ ⊢ {@param phi} : F
+   * Γ ⊢ {@param A} : (i : I) → {@link PartTy} (i = r ∨ φ) U
+   * Γ ⊢ {@param eave} : Partial φ (A s)
+   * Γ ⊢ {@param floor} : A r | φ ↦ coe s r A eave
+   * outPartial (A s)
+   * ------------------------------- outS floor : A r
+   * Γ ⊢ box r s phi A eave floor : hcom r s U phi A
+   *                              | r = s ↦ outS (floor) : outPartial (A r)
+   *
+ */ record Box( @NotNull Term r, @NotNull Term s, @NotNull Term phi, - @NotNull Term ceiling /* : A[ i ↦ s ] // under φ */, - @NotNull Term floor - /* : A[ i ↦ r ] for user - * : Sub (A[ i ↦ r ]) {| φ ↦ coe^{s ~> r}_{λ i, A i} ceiling |} for compiler */ + @NotNull Term A /* : (i : I) → Partial (i = r ∨ φ) U */, + // omit metalanguage-level `outPartial : (Partial ⊤ A) → A` below + @NotNull PartEl eave /* Partial φ (A s) */, + @NotNull Term floor /* : A r | φ ↦ coe s r A eave */ ) implements Term { } record Cap( @NotNull Term r, @NotNull Term s, @NotNull Term phi, - @NotNull Term hcompU /* : HcomU (r ~> s) i A */ + @NotNull Term A /* : (i : I) → Partial (i = r ∨ φ) U */, + @NotNull Term hcomU /* : hcom (r ~> s) U φ A */ ) implements Term { } diff --git a/base/src/main/java/org/aya/lamett/tyck/Elaborator.java b/base/src/main/java/org/aya/lamett/tyck/Elaborator.java index 3671c09..25ee29b 100644 --- a/base/src/main/java/org/aya/lamett/tyck/Elaborator.java +++ b/base/src/main/java/org/aya/lamett/tyck/Elaborator.java @@ -19,7 +19,9 @@ import java.util.function.Function; import java.util.function.Supplier; +import static org.aya.lamett.syntax.Term.*; import static org.aya.lamett.tyck.Normalizer.rename; +import static org.aya.lamett.syntax.Term.Ref.ref; public record Elaborator( @NotNull MutableMap, Def> sigma, diff --git a/base/src/main/java/org/aya/lamett/tyck/Normalizer.java b/base/src/main/java/org/aya/lamett/tyck/Normalizer.java index 7d9c8f8..d86c430 100644 --- a/base/src/main/java/org/aya/lamett/tyck/Normalizer.java +++ b/base/src/main/java/org/aya/lamett/tyck/Normalizer.java @@ -1,6 +1,5 @@ package org.aya.lamett.tyck; -import kala.collection.SeqView; import kala.collection.immutable.ImmutableSeq; import kala.collection.mutable.MutableMap; import kala.tuple.Tuple; @@ -9,9 +8,12 @@ import org.aya.lamett.util.LocalVar; import org.aya.lamett.util.Param; import org.jetbrains.annotations.NotNull; +import org.jetbrains.annotations.Nullable; import java.util.function.UnaryOperator; +import static org.aya.lamett.syntax.Term.Ref.ref; + public class Normalizer { private final @NotNull MutableMap rho; @@ -52,7 +54,7 @@ public Type type(Type type) { case Type.Sigma sig -> new Type.Sigma(new Param<>(sig.param().x(), type(sig.param().type())), type(sig.cod())); case Type.PartTy partTy -> new Type.PartTy(type(partTy.underlying()), term(partTy.restrs())); case Type.Sub sub -> new Type.Sub(type(sub.underlying()), partEl(sub.restrs())); - case Type.HcomU hcomU -> Type.Lit.U; + case Type.HcomU(var r, var s, var i, var restr) -> new Type.HcomU(term(r), term(s), i, partEl(restr, this::type)); }; } @@ -165,37 +167,64 @@ yield switch (A) { } yield new Term.OutS(outPhi, outPartEl, outOf); } - case Term.Box box -> { - var r = term(box.r()); - var s = term(box.s()); - var phi = term(box.phi()); - var ceil = term(box.ceiling()); - var floor = term(box.floor()); + case Term.Box(var r, var s, var phi, var A, var eave, var floor) -> { + r = term(r); + s = term(s); + phi = term(phi); + A = term(A); + eave = (Term.PartEl) term(eave); + floor = term(floor); + // r = s + if (unifier.untyped(r, s)) yield floor; + + // φ true + var branch = eave.simplifyUnder(conj -> unifier.cofibIsTrue(Cofib.of(conj))); + if (branch != null) yield branch.component2(); // FIXME: term(...) if we switch to whnf + + // unique rule if (floor instanceof Term.Cap cap && phi instanceof Cofib coffee) { - // unique rule - var success = unifier.withCofib(coffee, () -> - unifier.untyped(ceil, cap.hcompU()), - true); + var mEave = eave; + var success = unifier.withCofib(coffee, () -> { + var realEave = mEave.simplifyUnder(conj -> unifier.cofibIsTrue(Cofib.of(conj))); + assert realEave != null : "φ ∧ ¬ φ"; + return unifier.untyped(realEave.component2(), cap.hcomU()); + }, true); if (success) { - yield term(cap.hcompU()); + yield term(cap.hcomU()); } } - yield new Term.Box(r, s, phi, ceil, floor); + yield new Term.Box(r, s, phi, A, eave, floor); } - case Term.Cap cap -> { - var r = term(cap.r()); - var s = term(cap.s()); - var phi = term(cap.phi()); - var hcomU = term(cap.hcompU()); + case Term.Cap(var r, var s, var phi, var A, var hcomU) -> { + r = term(r); + s = term(s); + phi = term(phi); + A = term(A); + hcomU = term(hcomU); + + if (unifier.untyped(r, s)) yield hcomU; + + var i = new LocalVar("i"); + if (term(A.app(ref(i))) instanceof Term.PartEl wall + && phi instanceof Cofib coffee + && unifier.cofibIsTrue(coffee)) { + // since `A : (i : I) → Partial (i = r ∨ φ) U` and we are under `φ` + // We have `A i : Partial ⊤ U` for any i, + // and `realAi := outPartial (A i) : U` + var realAi = wall.simplifyUnder(conj -> unifier.cofibIsTrue(Cofib.of(conj))); + assert realAi != null : "φ ∧ ¬ φ"; + // coe { s ~> r } A hcomU + yield term(new Term.Coe(s, r, new Term.Lam(i, realAi.component2())).app(hcomU)); + } if (hcomU instanceof Term.Box box) { // computation rule yield term(box.floor()); } - yield new Term.Cap(r, s, phi, hcomU); + yield new Term.Cap(r, s, phi, A, hcomU); } }; } @@ -228,18 +257,29 @@ yield switch (A) { cofib = cofib.conj(cofib1); continue; } - default -> {} + default -> { + } } cofib = cofib.conj(Cofib.from(atom)); } return cofib; } - private @NotNull ImmutableSeq> partEl(@NotNull ImmutableSeq> elems) { + private @NotNull ImmutableSeq> partEl( + @NotNull ImmutableSeq> elems, + @NotNull UnaryOperator checker + ) { return elems.flatMap(tup -> - term(tup.component1()).conjs().map(conj -> Tuple.of(conj, term(tup.component2())))); + term(tup.component1()).conjs().map(conj -> Tuple.of(conj, checker.apply(tup.component2())))); + } + + private @NotNull ImmutableSeq> partEl( + @NotNull ImmutableSeq> elems + ) { + return partEl(elems, this::term); } + public @NotNull Normalizer derive() { return new Normalizer(MutableMap.from(rho), unification.derive()); } @@ -278,9 +318,10 @@ public Term term(Term term) { case Term.Sub(var A, var partEl) -> new Term.Sub(term(A), term(partEl)); case Term.InS(var phi, var of) -> new Term.InS(term(phi), term(of)); case Term.OutS(var phi, var partEl, var of) -> new Term.OutS(term(phi), term(partEl), term(of)); - case Term.Box(var r, var s, var phi, var ceil, var floor) -> - new Term.Box(term(r), term(s), term(phi), term(ceil), term(floor)); - case Term.Cap(var r, var s, var phi, var hcom) -> new Term.Cap(term(r), term(s), term(phi), term(hcom)); + case Term.Box(var r, var s, var phi, var A, var eave, var floor) -> + new Term.Box(term(r), term(s), term(phi), term(A), (Term.PartEl) term(eave), term(floor)); + case Term.Cap(var r, var s, var phi, var A, var hcom) -> + new Term.Cap(term(r), term(s), term(phi), term(A), term(hcom)); }; } From 93ef5610678a9ceace8150cff6337e4728c1f83e Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Sat, 12 Aug 2023 11:12:14 +0800 Subject: [PATCH 10/13] kan: hcom on hcomU, however, nobody knows if it is correct or not --- .../main/java/org/aya/lamett/syntax/Term.java | 6 +- .../main/java/org/aya/lamett/tyck/KanPDF.java | 81 ++++++++++++++++++- .../java/org/aya/lamett/tyck/Normalizer.java | 7 +- .../java/org/aya/lamett/tyck/Unifier.java | 2 +- 4 files changed, 89 insertions(+), 7 deletions(-) diff --git a/base/src/main/java/org/aya/lamett/syntax/Term.java b/base/src/main/java/org/aya/lamett/syntax/Term.java index bc25e0f..1c4ea81 100644 --- a/base/src/main/java/org/aya/lamett/syntax/Term.java +++ b/base/src/main/java/org/aya/lamett/syntax/Term.java @@ -154,9 +154,13 @@ record PartEl(@NotNull ImmutableSeq> elems) implements * * @param simplifier a simplifier, should confluent. */ - public @Nullable Tuple2 simplifyUnder(@NotNull Predicate simplifier) { + public @Nullable Tuple2 simplify(@NotNull Predicate simplifier) { return elems.firstOrNull(pair -> simplifier.test(pair.component1())); } + + public @Nullable Tuple2 simplify(@NotNull Unifier unifier) { + return simplify(conj -> unifier.cofibIsTrue(Cofib.of(conj))); + } } diff --git a/base/src/main/java/org/aya/lamett/tyck/KanPDF.java b/base/src/main/java/org/aya/lamett/tyck/KanPDF.java index 35b9334..77768c4 100644 --- a/base/src/main/java/org/aya/lamett/tyck/KanPDF.java +++ b/base/src/main/java/org/aya/lamett/tyck/KanPDF.java @@ -1,13 +1,18 @@ package org.aya.lamett.tyck; +import kala.collection.immutable.ImmutableSeq; import kala.collection.mutable.MutableMap; -import org.aya.lamett.syntax.Restr; +import kala.tuple.Tuple; +import org.aya.lamett.syntax.Cofib; import org.aya.lamett.syntax.Term; import org.aya.lamett.util.LocalVar; import org.jetbrains.annotations.NotNull; +import java.util.function.BiFunction; +import java.util.function.Function; import java.util.function.UnaryOperator; +import static org.aya.lamett.syntax.Term.Ref.ref; import static org.aya.lamett.tyck.Normalizer.rename; public interface KanPDF { @@ -76,4 +81,78 @@ static Term coeSigma(Term.Sigma sigma, LocalVar i, Term coeR, Term coeS) { var m1 = Term.com(hcomR, hcomS, comType, phi, i, partEl.map2(t -> t.proj(false))); return new Term.Pair(m0.apply(hcomS), m1); } + + static @NotNull Term hcomHcomU( + // hcom + @NotNull Term hcomR, @NotNull Term hcomS, + @NotNull Term hcomPhi, @NotNull LocalVar hcomI, @NotNull Term.PartEl hcomU, + // hcomU + @NotNull Term hcomUr, @NotNull Term hcomUs, + @NotNull Term hcomUphi, @NotNull LocalVar hcomUi, @NotNull Term.PartEl hcomUA, + @NotNull Unifier unifier + ) { + var conjHcomPhi = Cofib.Conj.of(hcomPhi); + var conjHcomUphi = Cofib.Conj.of(hcomUphi); + var conjReqS = Cofib.Conj.of(new Cofib.Eq(hcomUr, hcomUs)); + + // hcom { r ~> s } (hcom { r' ~> s' } U ψ A) φ u = + // box { r' ~> s' } ?0 ?1 : hcom { r' ~> s' } U ψ A + // where ψ ⊢ ?0 : A s' + // ⊢ ?1 : A r' | ψ ↦ coe { s' ~> r' } A ?0 + + // r' = s' ∨ ψ , i : I ⊢ P := hcom { r ~> i } (A s') φ u : A s' | ψ ↦ u i + Function P = i -> + new Term.Hcom(hcomR, i, hcomUA.subst(hcomUi, hcomUs), hcomPhi, new Term.Lam(hcomI, hcomU)); + + // ⊢ ?1 := hcom { r ~> s } (A r') (φ ∨ ψ ∨ r' = s') + // (λ i. {| i = r ∨ φ ↦ ?2 ; ψ ↦ ?3 ; r' = s' ↦ ?4 |} + // : A r' + // | r = s ∨ φ ↦ ... + // | ψ ↦ coe { s' ~> r' } A (P s') (required by box) + // | r' = s' ↦ ... + + // i : I, i = r ∨ φ ⊢ ?2 := cap { r' <~ s' } ψ (u i) + BiFunction Q = (i, proof) -> { + var result = unifier.withCofibConj(proof, () -> { + var realU = hcomU.simplify(conj -> unifier.cofibIsTrue(Cofib.of(conj))); + assert realU != null : "φ ∧ ¬ φ"; + return new Term.Cap(hcomUr, hcomUs, hcomUphi, hcomUA, realU.component2().subst(hcomI, i)); + }, null); // TODO: I am not sure !! + assert result != null : "i != r"; + return result; + }; + + Function Q0 = i -> Q.apply(i, Cofib.Conj.of(new Cofib.Eq(i, hcomR))); + Function Q1 = i -> Q.apply(i, conjHcomPhi); + + // i : I, ψ ⊢ ?3 := coe { s' ~> r' } A (P i) + Function R = i -> { + var realA = hcomUA.simplify(unifier); + assert realA != null : "φ ∧ ¬ φ"; + return new Term.Coe(hcomUs, hcomUr, realA.component2()).app(P.apply(i)); + }; + + // i : I, r' = s' ⊢ ?4 := P i : A r' + Function S = P; + + Function T = i -> new Term.PartEl(ImmutableSeq.of( + Tuple.of(Cofib.Conj.of(new Cofib.Eq(i, hcomR)), Q0.apply(i)), + Tuple.of(conjHcomPhi, Q1.apply(i)), + Tuple.of(conjHcomUphi, R.apply(i)), + Tuple.of(conjReqS, S.apply(i)) + )); + + // (i : I) -> Partial (i = r ∨ φ ∨ ψ ∨ r' = s') (A r') + var termT = Term.mkLam("i", i -> T.apply(ref(i))); + + var realAr = ((Term.PartEl) hcomUA.subst(hcomUi, hcomUr)) + .simplify(unifier) // since `i : I ⊢ A : Partial (i = r' ∨ ψ) U`, we have a clause with cof `r' = r'` + .component2(); + + return new Term.Box(hcomUr, hcomUs, hcomUphi, new Term.Lam(hcomUi, hcomUA), + new Term.PartEl(ImmutableSeq.of(Tuple.of(conjHcomUphi, P.apply(hcomUs)))), + new Term.Hcom(hcomR, hcomS, realAr, + Cofib.of(conjHcomPhi, conjHcomUphi, conjReqS), + termT)); + } } diff --git a/base/src/main/java/org/aya/lamett/tyck/Normalizer.java b/base/src/main/java/org/aya/lamett/tyck/Normalizer.java index d86c430..0e337b1 100644 --- a/base/src/main/java/org/aya/lamett/tyck/Normalizer.java +++ b/base/src/main/java/org/aya/lamett/tyck/Normalizer.java @@ -8,7 +8,6 @@ import org.aya.lamett.util.LocalVar; import org.aya.lamett.util.Param; import org.jetbrains.annotations.NotNull; -import org.jetbrains.annotations.Nullable; import java.util.function.UnaryOperator; @@ -179,14 +178,14 @@ yield switch (A) { if (unifier.untyped(r, s)) yield floor; // φ true - var branch = eave.simplifyUnder(conj -> unifier.cofibIsTrue(Cofib.of(conj))); + var branch = eave.simplify(conj -> unifier.cofibIsTrue(Cofib.of(conj))); if (branch != null) yield branch.component2(); // FIXME: term(...) if we switch to whnf // unique rule if (floor instanceof Term.Cap cap && phi instanceof Cofib coffee) { var mEave = eave; var success = unifier.withCofib(coffee, () -> { - var realEave = mEave.simplifyUnder(conj -> unifier.cofibIsTrue(Cofib.of(conj))); + var realEave = mEave.simplify(conj -> unifier.cofibIsTrue(Cofib.of(conj))); assert realEave != null : "φ ∧ ¬ φ"; return unifier.untyped(realEave.component2(), cap.hcomU()); }, true); @@ -213,7 +212,7 @@ yield switch (A) { // since `A : (i : I) → Partial (i = r ∨ φ) U` and we are under `φ` // We have `A i : Partial ⊤ U` for any i, // and `realAi := outPartial (A i) : U` - var realAi = wall.simplifyUnder(conj -> unifier.cofibIsTrue(Cofib.of(conj))); + var realAi = wall.simplify(conj -> unifier.cofibIsTrue(Cofib.of(conj))); assert realAi != null : "φ ∧ ¬ φ"; // coe { s ~> r } A hcomU yield term(new Term.Coe(s, r, new Term.Lam(i, realAi.component2())).app(hcomU)); diff --git a/base/src/main/java/org/aya/lamett/tyck/Unifier.java b/base/src/main/java/org/aya/lamett/tyck/Unifier.java index a00dd98..7cb1f6b 100644 --- a/base/src/main/java/org/aya/lamett/tyck/Unifier.java +++ b/base/src/main/java/org/aya/lamett/tyck/Unifier.java @@ -112,7 +112,7 @@ && untypedInner(ldt.param().type(), rdt.param().type()) return happy; } - boolean cofibIsTrue(@NotNull Cofib cofib) { + public boolean cofibIsTrue(@NotNull Cofib cofib) { return cofib.conjs().anyMatch(conj -> conj.atoms().allMatch(atom -> switch (atom) { case Cofib.Eq eq -> untyped(eq.lhs(), eq.rhs()); case Term.Ref(var ref) -> unification.cofibVars.contains(ref); From bc1367b5209666a29a59a73f9cfd18ade53ff7bf Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Sat, 12 Aug 2023 11:14:57 +0800 Subject: [PATCH 11/13] mics: maybe I should use "no one" --- base/src/test/java/TermTest.java | 34 -------------------------------- 1 file changed, 34 deletions(-) delete mode 100644 base/src/test/java/TermTest.java diff --git a/base/src/test/java/TermTest.java b/base/src/test/java/TermTest.java deleted file mode 100644 index 8c9d371..0000000 --- a/base/src/test/java/TermTest.java +++ /dev/null @@ -1,34 +0,0 @@ -import kala.collection.immutable.ImmutableSeq; -import org.aya.lamett.syntax.Cofib; -import org.aya.lamett.syntax.Term; -import org.aya.lamett.tyck.Normalizer; -import org.aya.lamett.tyck.Unification; -import org.aya.lamett.util.LocalVar; -import org.junit.jupiter.api.Test; - -public class TermTest { - @Test - public void waitForice1000sGrammar() { - var unification = new Unification(); - var nf = new Normalizer(unification); - - var phi = new LocalVar("φ"); - var A = new LocalVar("A"); // I → Partial (i = r ∨ φ) U - var u0 = new LocalVar("u0"); // A r - var refPhi = new Term.Ref(phi); - var refA = new Term.Ref(A); - var refU0 = new Term.Ref(u0); - - unification.addNFConj(new Cofib.Conj(ImmutableSeq.of(refPhi))); - - // coe (r ~> s) (λ i. A i) u0 - var halfCoe = new Term.Coe(Term.Lit.Zero, Term.Lit.One, Term.mkLam("i", i -> new Term.App(refA, new Term.Ref(i)))); - var ceiling = new Term.App(halfCoe, refU0); - var box = new Term.Box(Term.Lit.Zero, Term.Lit.One, refPhi, ceiling, refU0); - var cap = new Term.Cap(Term.Lit.Zero, Term.Lit.One, refPhi, box); - - var result = nf.term(cap); - var box2 = new Term.Box(Term.Lit.Zero, Term.Lit.One, refPhi, ceiling, cap); - var result2 = nf.term(box2); - } -} From d474698921fb52aeda53c6c40886f90567f4bbd9 Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Sat, 12 Aug 2023 11:26:22 +0800 Subject: [PATCH 12/13] kan: fix warning --- base/src/main/java/org/aya/lamett/tyck/KanPDF.java | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/base/src/main/java/org/aya/lamett/tyck/KanPDF.java b/base/src/main/java/org/aya/lamett/tyck/KanPDF.java index 77768c4..0f47b84 100644 --- a/base/src/main/java/org/aya/lamett/tyck/KanPDF.java +++ b/base/src/main/java/org/aya/lamett/tyck/KanPDF.java @@ -114,7 +114,7 @@ static Term coeSigma(Term.Sigma sigma, LocalVar i, Term coeR, Term coeS) { // i : I, i = r ∨ φ ⊢ ?2 := cap { r' <~ s' } ψ (u i) BiFunction Q = (i, proof) -> { var result = unifier.withCofibConj(proof, () -> { - var realU = hcomU.simplify(conj -> unifier.cofibIsTrue(Cofib.of(conj))); + var realU = hcomU.simplify(unifier); assert realU != null : "φ ∧ ¬ φ"; return new Term.Cap(hcomUr, hcomUs, hcomUphi, hcomUA, realU.component2().subst(hcomI, i)); }, null); // TODO: I am not sure !! @@ -145,9 +145,11 @@ static Term coeSigma(Term.Sigma sigma, LocalVar i, Term coeR, Term coeS) { // (i : I) -> Partial (i = r ∨ φ ∨ ψ ∨ r' = s') (A r') var termT = Term.mkLam("i", i -> T.apply(ref(i))); - var realAr = ((Term.PartEl) hcomUA.subst(hcomUi, hcomUr)) - .simplify(unifier) // since `i : I ⊢ A : Partial (i = r' ∨ ψ) U`, we have a clause with cof `r' = r'` - .component2(); + var halfRealAr = ((Term.PartEl) hcomUA.subst(hcomUi, hcomUr)) + .simplify(unifier); // since `i : I ⊢ A : Partial (i = r' ∨ ψ) U`, we have a clause with cof `r' = r'` + assert halfRealAr != null : "φ ∧ ¬ φ"; + var realAr = halfRealAr.component2(); + return new Term.Box(hcomUr, hcomUs, hcomUphi, new Term.Lam(hcomUi, hcomUA), new Term.PartEl(ImmutableSeq.of(Tuple.of(conjHcomUphi, P.apply(hcomUs)))), From 6c4e26b6afb0a415d697c18800abcf492946e47a Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Sun, 13 Aug 2023 02:06:09 +0800 Subject: [PATCH 13/13] misc: no more (PartEl) --- .../main/java/org/aya/lamett/tyck/Normalizer.java | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/base/src/main/java/org/aya/lamett/tyck/Normalizer.java b/base/src/main/java/org/aya/lamett/tyck/Normalizer.java index 0e337b1..b6b0275 100644 --- a/base/src/main/java/org/aya/lamett/tyck/Normalizer.java +++ b/base/src/main/java/org/aya/lamett/tyck/Normalizer.java @@ -306,8 +306,7 @@ public Term term(Term term) { case Cofib.Eq eq -> new Cofib.Eq(term(eq.lhs()), term(eq.rhs())); case Term.INeg t -> new Term.INeg(term(t)); case Term.PartTy(var cof, var ty) -> new Term.PartTy(term(cof), term(ty)); - case Term.PartEl(var elems) -> - new Term.PartEl(elems.map(tup -> Tuple.of(term(tup.component1()), term(tup.component2())))); + case Term.PartEl partEl -> partEl(partEl); case Term.Error error -> error; case Term.Coe(var r, var s, var A) -> new Term.Coe(term(r), term(s), term(A)); case Term.Hcom(var r, var s, var A, var f, var partial) -> @@ -318,7 +317,7 @@ public Term term(Term term) { case Term.InS(var phi, var of) -> new Term.InS(term(phi), term(of)); case Term.OutS(var phi, var partEl, var of) -> new Term.OutS(term(phi), term(partEl), term(of)); case Term.Box(var r, var s, var phi, var A, var eave, var floor) -> - new Term.Box(term(r), term(s), term(phi), term(A), (Term.PartEl) term(eave), term(floor)); + new Term.Box(term(r), term(s), term(phi), term(A), partEl(eave), term(floor)); case Term.Cap(var r, var s, var phi, var A, var hcom) -> new Term.Cap(term(r), term(s), term(phi), term(A), term(hcom)); }; @@ -328,6 +327,14 @@ public Term term(Term term) { return new Term.Ext<>(term(ext.type()), (F) ext.restr().map(this::term, this::term)); } + // avoiding explicitly casting + public @NotNull Term.PartEl partEl(@NotNull Term.PartEl partEl) { + return new Term.PartEl( + partEl.elems().map(tup -> + Tuple.of(term(tup.component1()), term(tup.component2()))) + ); + } + public @NotNull Cofib.Conj term(@NotNull Cofib.Conj conj) { return new Cofib.Conj(conj.atoms().map(this::term)); }