[WIP] HcomU

base/src/main/java/org/aya/lamett/syntax/Term.java

@@ -7,18 +7,22 @@
 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.Function;
+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,
   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);
   }
@@ -33,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<Def.Fn> fn, @NotNull ImmutableSeq<Term> args) implements Term {}
   record DataCall(@NotNull DefVar<Def.Data> fn, @NotNull ImmutableSeq<Term> args) implements Term {}
   record ConCall(@NotNull DefVar<Def.Cons> fn, @NotNull ImmutableSeq<Term> args,
@@ -52,6 +61,12 @@ record Lam(@NotNull LocalVar x, @NotNull Term body) implements Term {
   static @NotNull Term mkLam(@NotNull SeqView<LocalVar> telescope, @NotNull Term body) {
     return telescope.foldRight(body, Lam::new);
   }
+
+  static @NotNull Term mkLam(@NotNull String name, @NotNull Function<LocalVar, Term> 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);
@@ -129,6 +144,23 @@ record PartEl(@NotNull ImmutableSeq<Tuple2<Cofib.Conj, Term>> elems) implements
     public @NotNull PartEl map2(UnaryOperator<Term> f) {
       return new PartEl(elems.map(t -> Tuple.of(t.component1(), f.apply(t.component2()))));
     }
+
+    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<Cofib.Conj, Term> simplify(@NotNull Predicate<Cofib.Conj> simplifier) {
+      return elems.firstOrNull(pair -> simplifier.test(pair.component1()));
+    }
+
+    public @Nullable Tuple2<Cofib.Conj, Term> simplify(@NotNull Unifier unifier) {
+      return simplify(conj -> unifier.cofibIsTrue(Cofib.of(conj)));
+    }
   }
 
 
@@ -196,6 +228,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));
   }
 
+  /**
+   * <pre>
+   * Γ ⊢ {@param A}   : U
+   * Γ ⊢ {@param phi} : F
+   * Γ ⊢ {@param u}   : {@link PartTy} phi A
+   * -------------------------------------------
+   * Γ, phi ⊢ outPartial A phi u = hcom 0 1 phi (λ i. u) : A
+   * </pre>
+   */
+  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.
    *
@@ -210,10 +255,59 @@ record Ext<F extends Restr>(@NotNull Term type, @NotNull F restr) implements Ter
   record Path(@NotNull ImmutableSeq<LocalVar> binders, @NotNull Ext<Restr.Cubical> 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 PartEl A /* Partial (i = r \/ φ) code(U) // under i */
+  // ) implements Term {
+  // }
+
+  /**
+   * <pre>
+   * Γ ⊢ {@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)
+   * </pre>
+   */
+  record Box(
+    @NotNull Term r, @NotNull Term s,
+    @NotNull Term phi,
+    @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 A /* : (i : I) → Partial (i = r ∨ φ) U */,
+    @NotNull Term hcomU /* : hcom (r ~> s) U φ A */
+  ) implements Term {
+  }
+
+  /// endregion HcompU
+
   /** Let A be argument, then <code>A i -> A j</code> */
   static @NotNull Pi familyI2J(Term term, Term i, Term j) {
     return (Pi) mkPi(new App(term, i), new App(term, j));

base/src/main/java/org/aya/lamett/syntax/Type.java

@@ -81,6 +81,17 @@ record Sub(
     }
   }
 
+  record HcomU(
+    @NotNull Term r, @NotNull Term s,
+    @NotNull LocalVar i,
+    @NotNull ImmutableSeq<Tuple2<Cofib.Conj, Type>> restrs // under i
+  ) implements Type {
+    @Override
+    public @NotNull Doc toDoc() {
+      return Doc.plain("HcomU");
+    }
+  }
+
   default @NotNull Type subst(@NotNull LocalVar x, @NotNull Term t) {
     return subst(MutableMap.of(x, t));
   }

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<DefVar<?>, Def> sigma,

base/src/main/java/org/aya/lamett/tyck/KanPDF.java

@@ -1,12 +1,18 @@
 package org.aya.lamett.tyck;
 
+import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableMap;
+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 {
@@ -75,4 +81,80 @@ 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<Term, Term> 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<Term, Cofib.Conj, Term> Q = (i, proof) -> {
+      var result = unifier.withCofibConj(proof, () -> {
+        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 !!
+      assert result != null : "i != r";
+      return result;
+    };
+
+    Function<Term, Term> Q0 = i -> Q.apply(i, Cofib.Conj.of(new Cofib.Eq(i, hcomR)));
+    Function<Term, Term> Q1 = i -> Q.apply(i, conjHcomPhi);
+
+    // i : I, ψ ⊢ ?3 := coe { s' ~> r' } A (P i)
+    Function<Term, Term> 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<Term, Term> S = P;
+
+    Function<Term, Term.PartEl> 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 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)))),
+      new Term.Hcom(hcomR, hcomS, realAr,
+        Cofib.of(conjHcomPhi, conjHcomUphi, conjReqS),
+        termT));
+  }
 }