Skip to content

Instantly share code, notes, and snippets.

@ice1000

ice1000/cubical-patch.diff

Last active August 21, 2022 14:16
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save ice1000/a20bf0ffec2a91ac36c443d0ae000ff8 to your computer and use it in GitHub Desktop.
Save ice1000/a20bf0ffec2a91ac36c443d0ae000ff8 to your computer and use it in GitHub Desktop.
Download ZIP
Cubical code in guest0x0
Raw
cubical-patch.diff
diff --git a/base/src/main/java/org/aya/guest0x0/syntax/BdryData.java b/base/src/main/java/org/aya/guest0x0/syntax/BdryData.java
new file mode 100644
index 0000000..8ef920c
--- /dev/null
+++ b/base/src/main/java/org/aya/guest0x0/syntax/BdryData.java
@@ -0,0 +1,32 @@
+package org.aya.guest0x0.syntax;
+
+import kala.collection.immutable.ImmutableSeq;
+import kala.collection.mutable.MutableList;
+import org.aya.guest0x0.cubical.Restr;
+import org.aya.guest0x0.util.LocalVar;
+import org.aya.pretty.doc.Doc;
+import org.aya.pretty.doc.Docile;
+import org.jetbrains.annotations.NotNull;
+
+import java.util.function.Function;
+
+public record BdryData<E extends Docile & Restr.TermLike<E>>(
+ @NotNull ImmutableSeq<LocalVar> dims,
+ @NotNull E type,
+ @NotNull ImmutableSeq<Restr.Side<E>> boundaries
+) implements Docile {
+ public @NotNull BdryData<E> fmap(@NotNull Function<E, E> f, @NotNull ImmutableSeq<LocalVar> newDims) {
+ return new BdryData<>(newDims, f.apply(type), boundaries.map(b -> b.rename(f)));
+ }
+
+ public @NotNull BdryData<E> fmap(@NotNull Function<E, E> f) {
+ return fmap(f, dims);
+ }
+
+ @Override public @NotNull Doc toDoc() {
+ var head = MutableList.of(Doc.symbol("[|"));
+ dims.forEach(d -> head.append(Doc.plain(d.name())));
+ head.appendAll(new Doc[]{Doc.symbol("|]"), type.toDoc()});
+ return Doc.cblock(Doc.sep(head), 2, Doc.vcat(boundaries.map(Restr.Side::toDoc)));
+ }
+}
diff --git a/base/src/main/java/org/aya/guest0x0/syntax/Expr.java b/base/src/main/java/org/aya/guest0x0/syntax/Expr.java
index 44a6cb1..68f9e43 100644
--- a/base/src/main/java/org/aya/guest0x0/syntax/Expr.java
+++ b/base/src/main/java/org/aya/guest0x0/syntax/Expr.java
@@ -2,6 +2,7 @@ package org.aya.guest0x0.syntax;
import kala.collection.immutable.ImmutableSeq;
import kala.collection.mutable.MutableList;
+import org.aya.guest0x0.cubical.Formula;
import org.aya.guest0x0.cubical.Restr;
import org.aya.guest0x0.util.Distiller;
import org.aya.guest0x0.util.LocalVar;
@@ -36,4 +37,18 @@ public sealed interface Expr extends Docile, Restr.TermLike<Expr> {
record Hole(@Override @NotNull SourcePos pos, ImmutableSeq<LocalVar> accessible) implements Expr {}
/** @param isPi it's a sigma if false */
record DT(boolean isPi, @Override @NotNull SourcePos pos, Param<Expr> param, Expr cod) implements Expr {}
+ record Path(@Override @NotNull SourcePos pos, @NotNull BdryData<Expr> data) implements Expr {}
+ record Mula(@Override @NotNull SourcePos pos, @Override @NotNull Formula<Expr> asFormula) implements Expr {}
+ record Transp(@Override @NotNull SourcePos pos, @NotNull Expr cover, @NotNull Expr restr) implements Expr {}
+ record Cof(@Override @NotNull SourcePos pos, @NotNull Restr<Expr> data) implements Expr {}
+ record PartEl(@Override @NotNull SourcePos pos, @NotNull ImmutableSeq<Restr.Side<Expr>> clauses) implements Expr {}
+ record PartTy(@Override @NotNull SourcePos pos, @NotNull Expr ty, @NotNull Expr restr) implements Expr {}
+ /** "Proper" cubical subtypes */
+ record Sub(@Override @NotNull SourcePos pos, @NotNull Expr ty, @NotNull PartEl par) implements Expr {}
+ /**
+ * inS/outS, the introduction/elimination rules for the subtype relation
+ *
+ * @param isIntro true if inS
+ */
+ record SubEl(@Override @NotNull SourcePos pos, @NotNull Expr e, boolean isIntro) implements Expr {}
}
diff --git a/base/src/main/java/org/aya/guest0x0/syntax/Keyword.java b/base/src/main/java/org/aya/guest0x0/syntax/Keyword.java
index 17f99f0..5e431eb 100644
--- a/base/src/main/java/org/aya/guest0x0/syntax/Keyword.java
+++ b/base/src/main/java/org/aya/guest0x0/syntax/Keyword.java
@@ -1,5 +1,5 @@
package org.aya.guest0x0.syntax;
public enum Keyword {
- U
+ U, I, F
}
diff --git a/base/src/main/java/org/aya/guest0x0/syntax/Term.java b/base/src/main/java/org/aya/guest0x0/syntax/Term.java
index fad3f41..71eb5df 100644
--- a/base/src/main/java/org/aya/guest0x0/syntax/Term.java
+++ b/base/src/main/java/org/aya/guest0x0/syntax/Term.java
@@ -4,6 +4,7 @@ import kala.collection.SeqView;
import kala.collection.immutable.ImmutableSeq;
import kala.collection.mutable.MutableList;
import kala.collection.mutable.MutableMap;
+import org.aya.guest0x0.cubical.Formula;
import org.aya.guest0x0.cubical.Restr;
import org.aya.guest0x0.tyck.Normalizer;
import org.aya.guest0x0.util.Distiller;
@@ -76,6 +77,24 @@ public sealed interface Term extends Docile, Restr.TermLike<Term> {
static @NotNull Term mkPi(@NotNull Term dom, @NotNull Term cod) {
return new Term.DT(true, new Param<>(new LocalVar("_"), dom), cod);
}
- @NotNull Term U = new UI(Keyword.U);
+ @NotNull Term U = new UI(Keyword.U), I = new UI(Keyword.I), F = new UI(Keyword.F);
record UI(@NotNull Keyword keyword) implements Term {}
+ record Path(@NotNull BdryData<Term> data) implements Term {}
+ record PLam(@NotNull ImmutableSeq<LocalVar> dims, @NotNull Term fill) implements Term {}
+ record PCall(@NotNull Term p, @NotNull ImmutableSeq<Term> i, @NotNull PartEl b) implements Term {}
+ record Mula(@Override @NotNull Formula<Term> asFormula) implements Term {}
+ static @NotNull Term end(boolean isLeft) {return new Mula(new Formula.Lit<>(isLeft));}
+ static @NotNull Term neg(@NotNull Term term) {return new Mula(new Formula.Inv<>(term));}
+ static @NotNull Term conn(boolean isAnd, @NotNull Term l, @NotNull Term r) {return new Mula(new Formula.Conn<>(isAnd, l, r));}
+ static @NotNull Term and(@NotNull Term l, @NotNull Term r) {return conn(true, l, r);}
+ static @NotNull Term or(@NotNull Term l, @NotNull Term r) {return conn(false, l, r);}
+ record Transp(@NotNull Term cover, @NotNull Cof restr) implements Term {}
+ record Cof(@NotNull Restr<Term> restr) implements Term {
+ public @NotNull Cof fmap(@NotNull Function<Term, Term> f) {
+ return new Cof(restr.fmap(f));
+ }
+ }
+ record PartTy(@NotNull Term ty, @NotNull Term restr) implements Term {}
+ record PartEl(@NotNull ImmutableSeq<Restr.Side<Term>> clauses) implements Term {}
+ record Sub(@NotNull Term ty, @NotNull PartEl par) implements Term {}
}
diff --git a/base/src/main/java/org/aya/guest0x0/tyck/Elaborator.java b/base/src/main/java/org/aya/guest0x0/tyck/Elaborator.java
index b187aae..5b4e12b 100644
--- a/base/src/main/java/org/aya/guest0x0/tyck/Elaborator.java
+++ b/base/src/main/java/org/aya/guest0x0/tyck/Elaborator.java
@@ -5,10 +5,16 @@ import kala.collection.immutable.ImmutableSeq;
import kala.collection.mutable.MutableArrayList;
import kala.collection.mutable.MutableList;
import kala.collection.mutable.MutableMap;
+import kala.control.Option;
import kala.tuple.Tuple;
+import org.aya.guest0x0.cubical.CofThy;
+import org.aya.guest0x0.cubical.Formula;
+import org.aya.guest0x0.cubical.Restr;
+import org.aya.guest0x0.syntax.BdryData;
import org.aya.guest0x0.syntax.Def;
import org.aya.guest0x0.syntax.Expr;
import org.aya.guest0x0.syntax.Term;
+import org.aya.guest0x0.util.AltF7;
import org.aya.guest0x0.util.LocalVar;
import org.aya.guest0x0.util.Param;
import org.aya.guest0x0.util.SPE;
@@ -36,12 +42,32 @@ public record Elaborator(
public Term inherit(Expr expr, Term type) {
return switch (expr) {
- case Expr.Lam lam -> {
- if (normalize(type) instanceof Term.DT dt && dt.isPi())
- yield new Term.Lam(lam.x(), hof(lam.x(), dt.param().type(), () ->
- inherit(lam.a(), dt.codomain(new Term.Ref(lam.x())))));
- else throw new SPE(lam.pos(),
+ case Expr.Lam lam -> switch (normalize(type)) {
+ case Term.DT dt && dt.isPi() -> new Term.Lam(lam.x(),
+ hof(lam.x(), dt.param().type(), () -> inherit(lam.a(), dt.codomain(new Term.Ref(lam.x())))));
+ // Overloaded lambda
+ case Term.Path path -> {
+ var tyDims = path.data().dims();
+ var lamDims = MutableArrayList.<LocalVar>create(tyDims.size());
+ var unlam = Expr.unlam(lamDims, tyDims.size(), lam);
+ if (unlam == null) throw new SPE(lam.pos(), Doc.english("Expected path lambda"));
+ yield boundaries(lamDims, () -> inherit(unlam,
+ normalizer(lamDims, tyDims).term(path.data().type())
+ ), unlam.pos(), path.data(), normalizer(tyDims, lamDims));
+ }
+ default -> throw new SPE(lam.pos(),
Doc.english("Expects a right adjoint for"), expr, Doc.plain("got"), type);
+ };
+ case Expr.PartEl el -> {
+ if (!(normalize(type) instanceof Term.PartTy par)) throw new SPE(el.pos(),
+ Doc.english("Expects partial type for partial elements"), expr, Doc.plain("got"), type);
+ var cof = cof(par.restr(), el.pos());
+ var clauses = elaborateClauses(el, el.clauses(), par.ty());
+ var face = new Restr.Vary<>(clauses.map(Restr.Side::cof));
+ if (!CofThy.conv(cof.restr(), Normalizer.create(), norm -> CofThy.satisfied(norm.restr(face))))
+ throw new SPE(el.pos(), Doc.english("The faces in the partial element"), face,
+ Doc.english("must cover the face(s) specified in type:"), cof);
+ yield new Term.PartEl(clauses);
}
case Expr.Two two && !two.isApp() -> {
if (!(normalize(type) instanceof Term.DT dt) || dt.isPi()) throw new SPE(two.pos(),
@@ -49,6 +75,17 @@ public record Elaborator(
var lhs = inherit(two.f(), dt.param().type());
yield new Term.Two(false, lhs, inherit(two.a(), dt.codomain(lhs)));
}
+ case Expr.SubEl inS && inS.isIntro() -> {
+ if (!(normalize(type) instanceof Term.Sub sub)) throw new SPE(inS.pos(),
+ Doc.english("Expects cubical subtype, got"), type);
+ var arg = inherit(inS.e(), sub.ty());
+ boundaries(inS.pos(), normalizer(), arg, sub.par().clauses());
+ // yield new Term.SubEl(arg, true);
+ throw new UnsupportedOperationException("TODO");
+ }
+ case Expr.SubEl outS /*&& !outS.isIntro()*/ -> {
+ throw new UnsupportedOperationException("TODO");
+ }
case Expr.Hole hole -> {
var docs = MutableList.<Doc>create();
gamma.forEach((k, v) -> {
@@ -69,8 +106,22 @@ public record Elaborator(
}
default -> {
var synth = synth(expr);
- unify(normalize(type), synth.wellTyped, synth.type, expr.pos());
- yield synth.wellTyped;
+ yield switch (normalize(type)) {
+ case Term.Path path -> {
+ var exTyDims = path.data().dims();
+ var lamDims = MutableArrayList.<LocalVar>create(exTyDims.size());
+ var unlam = Term.unlam(lamDims, synth.wellTyped, exTyDims.size());
+ var acTyDims = MutableArrayList.<LocalVar>create(exTyDims.size());
+ var unpi = Term.unpi(acTyDims, synth.type, exTyDims.size());
+ if (unlam == null || unpi == null) throw new SPE(expr.pos(), Doc.english("Expected (path) lambda"));
+ unify(unpi, unlam, normalizer(exTyDims, acTyDims).term(path.data().type()), expr.pos());
+ yield boundaries(lamDims, () -> unlam, expr.pos(), path.data(), normalizer(exTyDims, lamDims));
+ }
+ case Term ty -> {
+ unify(ty, synth.wellTyped, synth.type, expr.pos());
+ yield synth.wellTyped;
+ }
+ };
}
};
}
@@ -81,6 +132,27 @@ public record Elaborator(
));
}
+ private ImmutableSeq<Restr.Side<Term>> elaborateClauses(
+ Expr on, @NotNull ImmutableSeq<Restr.Side<Expr>> clauses, @NotNull Term ty
+ ) {
+ var sides = clauses.flatMap(cl -> clause(on.pos(), cl, ty));
+ confluence(on, sides, on.pos());
+ return sides;
+ }
+
+ private void confluence(Docile on, ImmutableSeq<Restr.Side<Term>> clauses, @NotNull SourcePos pos) {
+ for (int i = 1; i < clauses.size(); i++) {
+ var lhs = clauses.get(i);
+ for (int j = 0; j < i; j++) {
+ var rhs = clauses.get(j);
+ CofThy.conv(lhs.cof().and(rhs.cof()), normalizer(), norm -> {
+ unify(norm.term(lhs.u()), on, norm.term(rhs.u()), pos, Doc.english("Boundaries disagree."));
+ return true;
+ });
+ }
+ }
+ }
+
private void unify(Term ty, Docile on, @NotNull Term actual, SourcePos pos, Doc prefix) {
unify(ty, actual, pos, u -> Doc.vcat(prefix, unifyDoc(ty, on, actual, u)));
}
@@ -105,6 +177,35 @@ public record Elaborator(
return line1;
}
+ /**
+ * @param subst Must be purely variable-to-variable
+ * @param coreSupplier Already substituted with the variables in the type
+ * @param lamDims Bindings in the type
+ */
+ private @NotNull Term boundaries(
+ @NotNull MutableList<LocalVar> lamDims,
+ @NotNull Supplier<Term> coreSupplier,
+ SourcePos pos, BdryData<Term> data,
+ Normalizer subst
+ ) {
+ lamDims.forEach(t -> gamma.put(t, Term.I));
+ var core = coreSupplier.get();
+ boundaries(pos, subst, core, data.boundaries());
+ lamDims.forEach(gamma::remove);
+ return new Term.PLam(lamDims.toImmutableArray(), core);
+ }
+
+ private void boundaries(SourcePos pos, Normalizer subst, Term core, ImmutableSeq<Restr.Side<Term>> boundaries) {
+ for (var boundary : boundaries) {
+ // Based on the very assumption as in the function's javadoc
+ CofThy.conv(boundary.cof().fmap(subst::term), subst, norm -> {
+ unify(norm.term(boundary.u()), boundary, norm.term(core), pos,
+ Doc.english("Boundary mismatch, oh no."));
+ return true;
+ });
+ }
+ }
+
public Synth synth(Expr expr) {
var synth = switch (expr) {
case Expr.PrimTy u -> new Synth(new Term.UI(u.keyword()), Term.U);
@@ -146,10 +247,82 @@ public record Elaborator(
var cod = hof(x, param.wellTyped, () -> synth(dt.cod()));
yield new Synth(new Term.DT(dt.isPi(), new Param<>(x, param.wellTyped), cod.wellTyped), cod.type);
}
+ case Expr.Sub sub -> {
+ var ty = inherit(sub.ty(), Term.U);
+ var clauses = elaborateClauses(sub, sub.par().clauses(), ty);
+ yield new Synth(new Term.Sub(ty, new Term.PartEl(clauses)), ty);
+ }
+ case Expr.Path path -> {
+ var dims = path.data().dims();
+ for (var dim : dims) gamma.put(dim, Term.I);
+ var ty = inherit(path.data().type(), Term.U);
+ var boundaries = elaborateClauses(expr, path.data().boundaries(), ty);
+ var data = new BdryData<>(dims, ty, boundaries);
+ for (var dim : dims) gamma.remove(dim);
+ yield new Synth(new Term.Path(data), Term.U);
+ }
+ case Expr.Mula f -> switch (f.asFormula()) {
+ case Formula.Inv<Expr> inv -> new Synth(Term.neg(inherit(inv.i(), Term.I)), Term.I);
+ case Formula.Conn<Expr> conn -> new Synth(new Term.Mula(
+ new Formula.Conn<>(conn.isAnd(), inherit(conn.l(), Term.I), inherit(conn.r(), Term.I))), Term.I);
+ case Formula.Lit<Expr> lit -> new Synth(Term.end(lit.isLeft()), Term.I);
+ };
+ case Expr.Cof cof -> new Synth(new Term.Cof(cof.data().mapCond(this::condition)), Term.F);
+ case Expr.PartTy par -> new Synth(new Term.PartTy(inherit(par.ty(), Term.U), cof(par.restr())), Term.U);
+ case Expr.Transp transp -> {
+ var cover = inherit(transp.cover(), Term.mkPi(Term.I, Term.U));
+ var detective = new AltF7(new LocalVar("?"));
+ var sample = cover.app(new Term.Ref(detective.var()));
+ var ty = Term.mkPi(cover.app(Term.end(true)), cover.app(Term.end(false)));
+ var cof = cof(transp.restr());
+ // I believe find-usages is slightly more efficient than what Huber wrote in hcomp.pdf
+ var capture = new Object() {
+ Term under = sample;
+ };
+ // I want it to have no references, so !detective.press(), and if it returns true, it means no problem
+ // So if it returns false then we're in trouble
+ if (!CofThy.conv(cof.restr(), normalizer(), n -> !detective.press(capture.under = n.term(sample))))
+ throw new SPE(transp.pos(), Doc.english("The cover"), cover,
+ Doc.english("has to be constant under the cofibration"), cof,
+ Doc.english("but applying a variable `?` to it results in"), capture.under,
+ Doc.english("which contains a reference to `?`, oh no"));
+ yield new Synth(new Term.Transp(cover, cof), ty);
+ }
default -> throw new SPE(expr.pos(), Doc.english("Synthesis failed for"), expr);
};
var type = normalize(synth.type);
- return new Synth(synth.wellTyped, type);
+ if (type instanceof Term.Path path) {
+ var dims = path.data().dims();
+ return new Synth(Normalizer.rename(Term.mkLam(dims.view(),
+ new Term.PCall(synth.wellTyped, dims.map(Term.Ref::new), new Term.PartEl(path.data().boundaries())))),
+ Term.mkPi(dims.map(x -> new Param<>(x, Term.I)), path.data().type()));
+ } else return new Synth(synth.wellTyped, type);
+ }
+
+ private @NotNull Restr.Cond<Term> condition(Restr.Cond<Expr> c) {
+ return new Restr.Cond<>(inherit(c.inst(), Term.I), c.isLeft());
+ }
+
+ private @NotNull Term.Cof cof(@NotNull Expr restr) {
+ return cof(inherit(restr, Term.F), restr.pos());
+ }
+
+ private static @NotNull Term.Cof cof(Term restr, @NotNull SourcePos pos) {
+ if (!(restr instanceof Term.Cof cof))
+ throw new SPE(pos, Doc.english("Expects a cofibration literal, got"), restr);
+ return cof;
+ }
+
+ private @NotNull Option<Restr.Side<Term>> clause(
+ @NotNull SourcePos pos,
+ @NotNull Restr.Side<Expr> clause, @NotNull Term ty
+ ) {
+ var cofib = new Restr.Cofib<>(clause.cof().ands().map(this::condition));
+ var u = CofThy.vdash(cofib, normalizer(), norm -> inherit(clause.u(), norm.term(ty)));
+ if (u.isDefined() && u.get() == null)
+ throw new SPE(pos, Doc.english("The cofibration in"), cofib,
+ Doc.english("is not well-defined"));
+ return u.map(uu -> new Restr.Side<>(cofib, uu));
}
private <T> T hof(@NotNull LocalVar x, @NotNull Term type, @NotNull Supplier<T> t) {
diff --git a/base/src/main/java/org/aya/guest0x0/tyck/HCompPDF.java b/base/src/main/java/org/aya/guest0x0/tyck/HCompPDF.java
new file mode 100644
index 0000000..fff2236
--- /dev/null
+++ b/base/src/main/java/org/aya/guest0x0/tyck/HCompPDF.java
@@ -0,0 +1,38 @@
+package org.aya.guest0x0.tyck;
+
+import org.aya.guest0x0.cubical.Restr;
+import org.aya.guest0x0.syntax.Term;
+import org.aya.guest0x0.util.LocalVar;
+import org.jetbrains.annotations.NotNull;
+
+import static org.aya.guest0x0.syntax.Term.*;
+
+/**
+ * References:
+ * <ul>
+ * <li><a href="https://github.com/molikto/mlang/blob/5110e18d20484a3f4ee57ee68e2793e5cf0e28e6/src-main/src/main/scala/mlang/compiler/semantic/10_value_fibrant.scala">10_value_fibrant.scala</a></li>
+ * <li><a href="https://www.cse.chalmers.se/~simonhu/misc/hcomp.pdf">hcomp.pdf</a></li>
+ * </ul>
+ */
+public interface HCompPDF {
+ record Transps(@NotNull Term cover, @NotNull Term.Cof restr) {
+ public @NotNull Term inv() {
+ return new Transp(mkLam("i", i -> cover.app(neg(i))), restr);
+ }
+
+ /** Marisa Kirisame!! */
+ public @NotNull Term mk() {return new Transp(cover, restr);}
+
+ public @NotNull Term fill(@NotNull LocalVar i) {
+ var ri = new Ref(i);
+ return new Transp(mkLam("j", j -> cover.app(and(ri, j))),
+ new Cof(restr.restr().or(new Restr.Cond<>(ri, true))));
+ }
+
+ public @NotNull Term invFill(@NotNull LocalVar i) {
+ var ri = new Ref(i);
+ return new Transp(mkLam("j", j -> cover.app(neg(and(neg(ri), j)))),
+ new Cof(restr.restr().or(new Restr.Cond<>(ri, false))));
+ }
+ }
+}
diff --git a/base/src/main/java/org/aya/guest0x0/tyck/Normalizer.java b/base/src/main/java/org/aya/guest0x0/tyck/Normalizer.java
index d2a9371..557001e 100644
--- a/base/src/main/java/org/aya/guest0x0/tyck/Normalizer.java
+++ b/base/src/main/java/org/aya/guest0x0/tyck/Normalizer.java
@@ -1,16 +1,32 @@
package org.aya.guest0x0.tyck;
+import kala.collection.immutable.ImmutableSeq;
+import kala.collection.mutable.MutableArrayList;
import kala.collection.mutable.MutableMap;
+import kala.value.Var;
+import org.aya.guest0x0.cubical.CofThy;
+import org.aya.guest0x0.cubical.Formula;
+import org.aya.guest0x0.cubical.Restr;
+import org.aya.guest0x0.syntax.BdryData;
import org.aya.guest0x0.syntax.Def;
+import org.aya.guest0x0.syntax.Keyword;
import org.aya.guest0x0.syntax.Term;
+import org.aya.guest0x0.tyck.HCompPDF.Transps;
import org.aya.guest0x0.util.LocalVar;
import org.aya.guest0x0.util.Param;
import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+
+import java.util.function.Consumer;
public record Normalizer(
@NotNull MutableMap<LocalVar, Def<Term>> sigma,
@NotNull MutableMap<LocalVar, Term> rho
-) {
+) implements CofThy.SubstObj<Term, LocalVar, Normalizer> {
+ public static @NotNull Normalizer create() {
+ return new Normalizer(MutableMap.create(), MutableMap.create());
+ }
+
public static @NotNull Term rename(@NotNull Term term) {
return new Renamer(MutableMap.create()).term(term);
}
@@ -19,6 +35,24 @@ public record Normalizer(
return new Param<>(param.x(), term(param.type()));
}
+ @Override public void put(LocalVar i, boolean isLeft) {
+ rho.put(i, Term.end(isLeft));
+ }
+
+ @Override public boolean contradicts(LocalVar i, boolean newIsLeft) {
+ if (!rho.containsKey(i)) return false;
+ if (!(rho.get(i).asFormula() instanceof Formula.Lit<Term> lit)) return false;
+ return lit.isLeft() != newIsLeft;
+ }
+
+ @Override public @Nullable LocalVar asRef(@NotNull Term term) {
+ return term instanceof Term.Ref ref ? ref.var() : null;
+ }
+
+ @Override public @NotNull Normalizer derive() {
+ return new Normalizer(sigma, MutableMap.from(rho));
+ }
+
public Term term(Term term) {
return switch (term) {
case Term.Ref ref -> rho.getOption(ref.var())
@@ -49,6 +83,110 @@ public record Normalizer(
fn.telescope().zip(call.args()).forEach(zip -> rho.put(zip._1.x(), term(zip._2)));
yield term(fn.body());
}
+ case Term.Path path -> new Term.Path(path.data().fmap(this::term));
+ case Term.PLam pLam -> new Term.PLam(pLam.dims(), term(pLam.fill()));
+ case Term.PCall pApp -> {
+ var i = pApp.i().map(this::term);
+ var p = term(pApp.p());
+ if (p instanceof Term.PLam pLam) {
+ pLam.dims().zipView(i).forEach(rho::put);
+ var fill = term(pLam.fill());
+ pLam.dims().forEach(rho::remove);
+ yield fill;
+ }
+ var b = pApp.b();
+ var ur = new Var<Term>();
+ // b.dims().zipView(i).forEach(zip -> rho.put(zip._1, zip._2));
+ var clauses = clauses(b.clauses(), ur::set);
+ if (ur.value != null) yield ur.value;
+ // b.dims().forEach(rho::remove);
+ yield new Term.PCall(p, i, new Term.PartEl(clauses));
+ }
+ case Term.Mula f -> formulae(f.asFormula().fmap(this::term));
+ case Term.Cof cof -> new Term.Cof(restr(cof.restr()));
+ case Term.Transp transp -> {
+ var parkerLiu = restr(transp.restr().restr());
+ // Because of his talk about lax 2-functors!
+ if (CofThy.satisfied(parkerLiu)) yield Term.id("x");
+ yield transp(new LocalVar("i"), term(transp.cover()), new Term.Cof(parkerLiu));
+ }
+ case Term.PartTy par -> new Term.PartTy(term(par.ty()), term(par.restr()));
+ case Term.PartEl par -> partial(par);
+ case Term.Sub sub -> new Term.Sub(term(sub.ty()), partial(sub.par()));
+ };
+ }
+
+ private @NotNull Term.PartEl partial(Term.PartEl par) {
+ // TODO: do nothing for now, need a new term for 'to reduce' partials
+ return new Term.PartEl(clauses(par.clauses(), u -> {}));
+ }
+
+ private ImmutableSeq<Restr.Side<Term>> clauses(
+ @NotNull ImmutableSeq<Restr.Side<Term>> sides,
+ @NotNull Consumer<Term> truthHandler
+ ) {
+ var clauses = MutableArrayList.<Restr.Side<Term>>create();
+ for (var clause : sides) {
+ var u = term(clause.u());
+ if (CofThy.normalizeCof(clause.cof().fmap(this::term), clauses, cofib -> new Restr.Side<>(cofib, u))) {
+ truthHandler.accept(u);
+ }
+ }
+ return clauses.toImmutableArray();
+ }
+
+ public Restr<Term> restr(@NotNull Restr<Term> restr) {
+ return switch (restr.fmap(this::term)) {
+ case Restr.Vary<Term> vary -> CofThy.normalizeRestr(vary);
+ case Restr.Const<Term> c -> c;
+ };
+ }
+
+ private Term transp(LocalVar i, Term cover, Term.Cof cof) {
+ return switch (cover.app(new Term.Ref(i))) {
+ case Term.DT dt && dt.isPi() -> Term.mkLam("f", u0 -> Term.mkLam("x", v -> {
+ var laptop = new Transps(rename(new Term.Lam(i, dt.param().type())), cof);
+ var w = laptop.invFill(i).app(v);
+ // w0 = w.subst(i, 0), according to Minghao Liu
+ var w0 = laptop.inv().app(v);
+ var cod = rename(new Term.Lam(i, dt.codomain(w)));
+ return new Term.Transp(cod, cof).app(u0.app(w0));
+ }));
+ case Term.UI u && u.keyword() == Keyword.U -> Term.id("u");
+ case Term.DT dt /*&& !dt.isPi()*/ -> Term.mkLam("t", u0 -> {
+ var laptop = new Transps(rename(new Term.Lam(i, dt.param().type())), cof);
+ // Simon Huber wrote u0.1 both with and without parentheses, extremely confusing!!
+ var v = laptop.fill(i).app(u0.proj(true));
+ return new Term.Two(false, laptop.mk().app(u0.proj(true)),
+ new Term.Transp(rename(new Term.Lam(i, dt.codomain(v))), cof).app(u0.proj(false)));
+ });
+ default -> new Term.Transp(cover, cof);
+ };
+ }
+
+ // https://github.com/mortberg/cubicaltt/blob/a5c6f94bfc0da84e214641e0b87aa9649ea114ea/Connections.hs#L178-L197
+ private Term formulae(Formula<Term> formula) {
+ return switch (formula) { // de Morgan laws
+ // ~ 1 = 0, ~ 0 = 1
+ case Formula.Inv<Term> inv && inv.i().asFormula() instanceof Formula.Lit<Term> lit -> Term.end(!lit.isLeft());
+ // ~ (~ a) = a
+ case Formula.Inv<Term> inv && inv.i().asFormula() instanceof Formula.Inv<Term> ii -> ii.i(); // DNE!! :fear:
+ // ~ (a /\ b) = (~ a \/ ~ b), ~ (a \/ b) = (~ a /\ ~ b)
+ case Formula.Inv<Term> inv && inv.i().asFormula() instanceof Formula.Conn<Term> conn ->
+ new Term.Mula(new Formula.Conn<>(!conn.isAnd(),
+ formulae(new Formula.Inv<>(conn.l())),
+ formulae(new Formula.Inv<>(conn.r()))));
+ // 0 /\ a = 0, 1 /\ a = a, 0 \/ a = a, 1 \/ a = 1
+ case Formula.Conn<Term> conn && conn.l() instanceof Term.Mula lf
+ && lf.asFormula() instanceof Formula.Lit<Term> l -> l.isLeft()
+ ? (conn.isAnd() ? lf : conn.r())
+ : (conn.isAnd() ? conn.r() : lf);
+ // a /\ 0 = 0, a /\ 1 = a, a \/ 0 = a, a \/ 1 = 1
+ case Formula.Conn<Term> conn && conn.r() instanceof Term.Mula rf
+ && rf.asFormula() instanceof Formula.Lit<Term> r -> r.isLeft()
+ ? (conn.isAnd() ? rf : conn.l())
+ : (conn.isAnd() ? conn.l() : rf);
+ default -> new Term.Mula(formula);
};
}
@@ -69,9 +207,29 @@ public record Normalizer(
case Term.Two two -> new Term.Two(two.isApp(), term(two.f()), term(two.a()));
case Term.Proj proj -> new Term.Proj(term(proj.t()), proj.isOne());
case Term.Call call -> new Term.Call(call.fn(), call.args().map(this::term));
+ case Term.Path path -> new Term.Path(boundaries(path.data()));
+ case Term.PLam pLam -> {
+ var params = pLam.dims().map(this::param);
+ yield new Term.PLam(params, term(pLam.fill()));
+ }
+ case Term.PCall pApp -> new Term.PCall(term(pApp.p()), pApp.i().map(this::term), partEl(pApp.b()));
+ case Term.Mula f -> new Term.Mula(f.asFormula().fmap(this::term));
+ case Term.Transp tr -> new Term.Transp(term(tr.cover()), tr.restr().fmap(this::term));
+ case Term.Cof cof -> cof.fmap(this::term);
+ case Term.PartTy par -> new Term.PartTy(term(par.ty()), term(par.restr()));
+ case Term.PartEl par -> partEl(par);
+ case Term.Sub sub -> new Term.Sub(term(sub.ty()), partEl(sub.par()));
};
}
+ private @NotNull Term.PartEl partEl(Term.PartEl par) {
+ return new Term.PartEl(par.clauses().map(clause -> clause.rename(this::term)));
+ }
+
+ private @NotNull BdryData<Term> boundaries(@NotNull BdryData<Term> data) {
+ return data.fmap(this::term, data.dims().map(this::param));
+ }
+
private @NotNull LocalVar vv(@NotNull LocalVar var) {
return map.getOrDefault(var, var);
}
diff --git a/base/src/main/java/org/aya/guest0x0/tyck/Resolver.java b/base/src/main/java/org/aya/guest0x0/tyck/Resolver.java
index 1075ed8..cbe1868 100644
--- a/base/src/main/java/org/aya/guest0x0/tyck/Resolver.java
+++ b/base/src/main/java/org/aya/guest0x0/tyck/Resolver.java
@@ -76,9 +76,28 @@ public record Resolver(@NotNull MutableMap<String, LocalVar> env) {
.getOrThrow(() -> new SPE(unresolved.pos(), Doc.english("Unresolved: " + unresolved.name())));
case Expr.Resolved resolved -> resolved;
case Expr.Proj proj -> new Expr.Proj(proj.pos(), expr(proj.t()), proj.isOne());
+ case Expr.Path path -> {
+ var dims = path.data().dims();
+ var state = mkCache(dims.size());
+ dims.forEach(state::add);
+ var data = path.data().fmap(this::expr);
+ state.purge();
+ yield new Expr.Path(path.pos(), data);
+ }
+ case Expr.Mula f -> new Expr.Mula(f.pos(), f.asFormula().fmap(this::expr));
+ case Expr.Transp transp -> new Expr.Transp(transp.pos(), expr(transp.cover()), expr(transp.restr()));
+ case Expr.Cof cof -> new Expr.Cof(cof.pos(), cof.data().fmap(this::expr));
+ case Expr.PartEl par -> par(par);
+ case Expr.PartTy par -> new Expr.PartTy(par.pos(), expr(par.ty()), expr(par.restr()));
+ case Expr.Sub sub -> new Expr.Sub(sub.pos(), expr(sub.ty()), par(sub.par()));
+ case Expr.SubEl subEl -> new Expr.SubEl(subEl.pos(), expr(subEl.e()), subEl.isIntro());
};
}
+ private @NotNull Expr.PartEl par(Expr.PartEl par) {
+ return new Expr.PartEl(par.pos(), par.clauses().map(clause -> clause.rename(this::expr)));
+ }
+
private @NotNull Expr bodied(LocalVar x, Expr expr) {
var old = put(x);
var e = expr(expr);
diff --git a/base/src/main/java/org/aya/guest0x0/tyck/Unifier.java b/base/src/main/java/org/aya/guest0x0/tyck/Unifier.java
index 5d3f20e..b9a81f9 100644
--- a/base/src/main/java/org/aya/guest0x0/tyck/Unifier.java
+++ b/base/src/main/java/org/aya/guest0x0/tyck/Unifier.java
@@ -1,6 +1,11 @@
package org.aya.guest0x0.tyck;
import kala.collection.immutable.ImmutableSeq;
+import kala.collection.mutable.MutableMap;
+import kala.tuple.Tuple;
+import org.aya.guest0x0.cubical.CofThy;
+import org.aya.guest0x0.cubical.Formula;
+import org.aya.guest0x0.cubical.Restr;
import org.aya.guest0x0.syntax.Term;
import org.aya.guest0x0.util.LocalVar;
import org.jetbrains.annotations.NotNull;
@@ -26,6 +31,28 @@ public class Unifier {
case Term.UI lu && r instanceof Term.UI ru -> lu.keyword() == ru.keyword();
case Term.Call lcall && r instanceof Term.Call rcall -> lcall.fn() == rcall.fn()
&& lcall.args().sameElements(rcall.args(), true);
+ case Term.PLam plam && r instanceof Term.PLam pram && plam.dims().sizeEquals(pram.dims()) ->
+ untyped(plam.fill(), pram.fill().subst(MutableMap.from(
+ pram.dims().zip(plam.dims()).map(p -> Tuple.of(p._1, new Term.Ref(p._2))))));
+ case Term.PCall lpcall && r instanceof Term.PCall rpcall ->
+ untyped(lpcall.p(), rpcall.p()) && unifySeq(lpcall.i(), rpcall.i());
+ case Term.Mula lf && r instanceof Term.Mula rf -> formulae(lf.asFormula(), rf.asFormula());
+ case Term.Transp ltp && r instanceof Term.Transp rtp ->
+ untyped(ltp.cover(), rtp.cover()) && untyped(ltp.restr(), rtp.restr());
+ case Term.Cof lcof && r instanceof Term.Cof rcof -> {
+ var initial = Normalizer.create();
+ var ll = lcof.restr();
+ var rr = rcof.restr();
+ yield CofThy.conv(ll, initial, normalizer -> CofThy.satisfied(normalizer.restr(rr)))
+ && CofThy.conv(rr, initial, normalizer -> CofThy.satisfied(normalizer.restr(ll)));
+ }
+ case Term.PartTy lpart && r instanceof Term.PartTy rpart ->
+ untyped(lpart.ty(), rpart.ty()) && untyped(lpart.restr(), rpart.restr());
+ case Term.PartEl par -> par.clauses().allMatch(clause -> clause(clause, r));
+ case Term ll && r instanceof Term.PartEl par -> par.clauses().allMatch(clause -> clause(clause, ll));
+ case Term.Sub ll && r instanceof Term.Sub rr -> untyped(ll.ty(), rr.ty())
+ && untyped(ll.par(), rr.par());
+ // Cubical subtyping?? Are we ever gonna unify cubes?
default -> false;
};
if (!happy && data == null)
@@ -33,10 +60,27 @@ public class Unifier {
return happy;
}
+ /** Daniel Gratzer used <code>N</code> when explaining these to me */
+ private boolean clause(@NotNull Restr.Side<Term> clause, @NotNull Term n) {
+ return CofThy.conv(new Restr.Vary<>(ImmutableSeq.of(clause.cof())),
+ Normalizer.create(), subst -> untyped(clause.u(), subst.term(n)));
+ }
+
private boolean unifySeq(@NotNull ImmutableSeq<Term> l, @NotNull ImmutableSeq<Term> r) {
return l.zipView(r).allMatch(p -> untyped(p._1, p._2));
}
+ // Hopefully.... I don't know. :shrug:
+ private boolean formulae(Formula<Term> lf, Formula<Term> rf) {
+ return switch (lf) {
+ case Formula.Lit<Term> l && rf instanceof Formula.Lit<Term> r -> l.isLeft() == r.isLeft();
+ case Formula.Inv<Term> l && rf instanceof Formula.Inv<Term> r -> untyped(l.i(), r.i());
+ case Formula.Conn<Term> l && rf instanceof Formula.Conn<Term> r && l.isAnd() == r.isAnd() ->
+ untyped(l.l(), r.l()) && untyped(l.r(), r.r());
+ default -> false;
+ };
+ }
+
private boolean eta(@NotNull Term r, Term.Lam lam) {
return untyped(lam.body(), r.app(new Term.Ref(lam.x())));
}
diff --git a/base/src/main/java/org/aya/guest0x0/util/AltF7.java b/base/src/main/java/org/aya/guest0x0/util/AltF7.java
new file mode 100644
index 0000000..1036c58
--- /dev/null
+++ b/base/src/main/java/org/aya/guest0x0/util/AltF7.java
@@ -0,0 +1,46 @@
+package org.aya.guest0x0.util;
+
+import org.aya.guest0x0.cubical.Formula;
+import org.aya.guest0x0.cubical.Restr;
+import org.aya.guest0x0.syntax.BdryData;
+import org.aya.guest0x0.syntax.Term;
+import org.jetbrains.annotations.NotNull;
+
+public record AltF7(@NotNull LocalVar var) {
+ public boolean press(@NotNull Term term) {
+ return switch (term) {
+ case Term.Ref r -> r.var() == var;
+ case Term.Lam lam -> press(lam.body());
+ case Term.Transp transp -> press(transp.cover()) || press(transp.restr());
+ case Term.PCall pCall -> press(pCall.p()) || pCall.i().anyMatch(this::press) || press(pCall.b());
+ case Term.PLam pLam -> press(pLam.fill());
+ case Term.Call call -> call.fn() == var || call.args().anyMatch(this::press);
+ case Term.Two two -> press(two.f()) || press(two.a());
+ case Term.Proj proj -> press(proj.t());
+ case Term.UI ignored -> false;
+ case Term.DT dt -> press(dt.param().type()) || press(dt.cod());
+ case Term.Path path -> boundaries(path.data());
+ case Term.Mula mula -> formula(mula.asFormula());
+ case Term.Cof cof -> cof.restr().instView().anyMatch(this::press);
+ case Term.PartTy par -> press(par.ty()) || press(par.restr());
+ case Term.PartEl par -> par.clauses().anyMatch(this::clause);
+ case Term.Sub sub -> press(sub.ty()) || press(sub.par());
+ };
+ }
+
+ private boolean boundaries(BdryData<Term> data) {
+ return press(data.type()) || data.boundaries().anyMatch(this::clause);
+ }
+
+ private boolean formula(Formula<Term> formula) {
+ return switch (formula) {
+ case Formula.Lit<?> ignored -> false;
+ case Formula.Inv<Term> inv -> press(inv.i());
+ case Formula.Conn<Term> conn -> press(conn.l()) || press(conn.r());
+ };
+ }
+
+ private boolean clause(Restr.Side<Term> clause) {
+ return press(clause.u()) || clause.cof().view().anyMatch(this::press);
+ }
+}
diff --git a/base/src/main/java/org/aya/guest0x0/util/Distiller.java b/base/src/main/java/org/aya/guest0x0/util/Distiller.java
index d134e72..68c51a6 100644
--- a/base/src/main/java/org/aya/guest0x0/util/Distiller.java
+++ b/base/src/main/java/org/aya/guest0x0/util/Distiller.java
@@ -1,6 +1,10 @@
package org.aya.guest0x0.util;
import kala.collection.Seq;
+import kala.collection.SeqView;
+import kala.collection.mutable.MutableList;
+import org.aya.guest0x0.cubical.Formula;
+import org.aya.guest0x0.cubical.Restr;
import org.aya.guest0x0.syntax.Expr;
import org.aya.guest0x0.syntax.Term;
import org.aya.pretty.doc.Doc;
@@ -32,6 +36,7 @@ public interface Distiller {
yield envPrec.ordinal() > Free.ordinal() ? Doc.parened(doc) : doc;
}
case Expr.Resolved resolved -> Doc.plain(resolved.ref().name());
+ case Expr.Path path -> path.data().toDoc();
case Expr.Unresolved unresolved -> Doc.plain(unresolved.name());
case Expr.Proj proj -> Doc.cat(expr(proj.t(), ProjHead), Doc.plain("." + (proj.isOne() ? 1 : 2)));
case Expr.DT dt -> {
@@ -39,12 +44,44 @@ public interface Distiller {
yield envPrec.ordinal() > Cod.ordinal() ? Doc.parened(doc) : doc;
}
case Expr.Hole ignored -> Doc.symbol("_");
+ case Expr.Mula e -> formulae(Distiller::expr, e.asFormula(), envPrec);
+ case Expr.Transp transp -> fibred("tr", transp.cover(), transp.restr());
+ case Expr.Cof cof -> {
+ var doc = cof.data().toDoc();
+ // Well, hopefully I guessed the precedence right.
+ yield envPrec.ordinal() > AppSpine.ordinal() ? Doc.parened(doc) : doc;
+ }
+ case Expr.PartEl par -> Doc.sep(Doc.symbol("\\"), partial(par));
+ case Expr.PartTy par -> fibred("Partial", par.ty(), par.restr());
+ case Expr.Sub sub -> Doc.sep(Doc.plain("Sub"),
+ expr(sub.ty(), Free), partial(sub.par()));
+ case Expr.SubEl subEl -> Doc.sep(Doc.plain(subEl.isIntro() ? "inS" : "outS"), expr(subEl.e(), Free));
};
}
+ @NotNull private static Doc partial(Expr.PartEl par) {
+ return Doc.wrap("[|", "|]",
+ Doc.join(Doc.symbol("|"), clauses(par.clauses())));
+ }
+ private static @NotNull Doc fibred(String kw, Docile cover, Docile restr) {
+ return Doc.sep(Doc.plain(kw), cover.toDoc(),
+ Doc.symbol("#{"), restr.toDoc(), Doc.symbol("}"));
+ }
private static @NotNull Doc dependentType(boolean isPi, Param<?> param, Docile cod) {
return Doc.sep(Doc.plain(isPi ? "Pi" : "Sig"),
param.toDoc(), Doc.symbol(isPi ? "->" : "**"), cod.toDoc());
}
+ private static @NotNull <E> Doc formulae(PP<E> f, Formula<E> formula, Prec envPrec) {
+ var doc = switch (formula) {
+ case Formula.Conn<E> conn -> Doc.sep(f.apply(conn.l(), IOp),
+ Doc.symbol(conn.isAnd() ? "/\\" : "\\/"), f.apply(conn.r(), IOp));
+ case Formula.Inv<E> inv -> Doc.sep(Doc.plain("~"), f.apply(inv.i(), IOp));
+ case Formula.Lit<E> lit -> {
+ envPrec = Free; // A hack to force no paren
+ yield Doc.symbol(lit.isLeft() ? "0" : "1");
+ }
+ };
+ return envPrec.ordinal() >= IOp.ordinal() ? Doc.parened(doc) : doc;
+ }
static @NotNull Doc term(@NotNull Term term, Prec envPrec) {
return switch (term) {
@@ -54,6 +91,7 @@ public interface Distiller {
}
case Term.UI ui -> Doc.plain(ui.keyword().name());
case Term.Ref ref -> Doc.plain(ref.var().name());
+ case Term.Path path -> path.data().toDoc();
case Term.Lam lam -> {
var doc = Doc.sep(Doc.cat(Doc.plain("\\"),
Doc.symbol(lam.x().name()), Doc.plain(".")), term(lam.body(), Free));
@@ -71,6 +109,38 @@ public interface Distiller {
.map(t -> term(t, AppSpine)).prepended(Doc.plain(call.fn().name())));
yield envPrec.ordinal() > AppHead.ordinal() ? Doc.parened(doc) : doc;
}
+ case Term.PCall call -> {
+ var doc = Doc.sep(call.i().view()
+ .map(t -> term(t, AppSpine)).prepended(term(call.p(), AppHead)));
+ yield envPrec.ordinal() > AppHead.ordinal() ? Doc.parened(doc) : doc;
+ }
+ case Term.PLam pLam -> {
+ var docs = MutableList.of(Doc.plain("\\"));
+ pLam.dims().forEach(d -> docs.append(Doc.symbol(d.name())));
+ docs.append(Doc.plain("."));
+ docs.append(term(pLam.fill(), Free));
+ var doc = Doc.sep(docs);
+ yield envPrec.ordinal() > Free.ordinal() ? Doc.parened(doc) : doc;
+ }
+ case Term.Mula f -> formulae(Distiller::term, f.asFormula(), envPrec);
+ case Term.Transp transp -> fibred("tr", transp.cover(), transp.restr());
+ case Term.Cof cof -> {
+ var doc = cof.restr().toDoc();
+ yield envPrec.ordinal() > AppSpine.ordinal() ? Doc.parened(doc) : doc;
+ }
+ case Term.PartTy par -> fibred("Partial", par.ty(), par.restr());
+ case Term.PartEl par -> partial(par);
+ case Term.Sub sub -> Doc.sep(Doc.plain("Sub"),
+ term(sub.ty(), Free), partial(sub.par()));
};
}
+ private static @NotNull Doc partial(Term.PartEl par) {
+ return Doc.wrap("[|", "|]",
+ Doc.join(Doc.symbol("|"), clauses(par.clauses())));
+ }
+ static <T extends Restr.TermLike<T>> SeqView<Doc> clauses(@NotNull Seq<Restr.Side<T>> clauses) {
+ return clauses.view()
+ .map(Restr.Side::toDoc)
+ .map(Doc::spaced);
+ }
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment