Skip to content

Commit

Permalink
misc: no more (PartEl)
Browse files Browse the repository at this point in the history
  • Loading branch information
HoshinoTented committed Aug 14, 2023
1 parent d474698 commit 6c4e26b
Showing 1 changed file with 10 additions and 3 deletions.
13 changes: 10 additions & 3 deletions base/src/main/java/org/aya/lamett/tyck/Normalizer.java
Original file line number Diff line number Diff line change
Expand Up @@ -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) ->
Expand All @@ -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));
};
Expand All @@ -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));
}
Expand Down

0 comments on commit 6c4e26b

Please sign in to comment.