Skip to content

Commit 73c2e7a

Browse files
ice1000ice1000
authored
merge: Partial (#1451)
Solved #1448, but variables still cannot appear in LHS of a partial element clause yet.
2 parents 2f109a5 + 17346af commit 73c2e7a

File tree

16 files changed

+107
-64
lines changed

16 files changed

+107
-64
lines changed

‎base/src/main/java/org/aya/normalize/Normalizer.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -76,7 +76,7 @@ public final class Normalizer implements UnaryOperator<Term> {
7676
}
7777

7878
// compute a and b
79-
private @NotNull DisjCofNF expandAnd(@NotNull DisjCofNF a, @NotNull DisjCofNF b) {
79+
public @NotNull DisjCofNF expandAnd(@NotNull DisjCofNF a, @NotNull DisjCofNF b) {
8080
MutableSeq<ConjCofNF> ret = MutableSeq.create(a.elements().size() * b.elements().size());
8181
var i = 0;
8282
for (var ae : a.elements())

‎base/src/main/java/org/aya/tyck/ExprTycker.java‎

Lines changed: 19 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -176,25 +176,35 @@ && whnf(type) instanceof DataCall dataCall
176176
var A = arg.get(1);
177177
// check each clause
178178
MutableList<PartialTerm.Clause> cls = MutableList.create();
179-
MutableList<ConjCofNF> allCof = MutableList.create();
179+
MutableList<Term> allCof = MutableList.create();
180180
for (var rcls : clause) {
181-
var clsCof = elabCof(rcls.cof());
182-
var clsRhs = inherit(rcls.tm(), A).wellTyped();
183-
cls.append(new PartialTerm.Clause(clsCof, clsRhs));
184-
allCof.append(clsCof);
181+
var clsCof = inherit(rcls.cof(), state().primFactory.getCall(PrimDef.ID.COF));
182+
var clsCofNF = expand(clsCof.wellTyped());
183+
if (clsCofNF == null) {
184+
yield fail(expr.data(), type, new IllegalPartialElement.BadPartialLHS(clsCof.wellTyped(), rcls.cof().sourcePos(), state()));
185+
}
186+
var clsRhs = withConnection(clsCofNF, () -> inherit(rcls.tm(), A).wellTyped(), () -> inherit(rcls.tm(), A).wellTyped());
187+
cls.append(new PartialTerm.Clause(clsCofNF, clsRhs));
188+
allCof.append(clsCof.wellTyped());
185189
}
186190
// coverage. cof <=> allCof
187191
var disj = expand(cof);
188-
var cnf = new DisjCofNF(allCof.toSeq());
192+
var cnf = new DisjCofNF(ImmutableSeq.empty());
193+
if (!allCof.isEmpty()) {
194+
cnf = expand(allCof.drop(1).foldRight(allCof.get(0), (l, r) ->
195+
state().primFactory.getCall(PrimDef.ID.COF_OR, ImmutableSeq.of(l,r)) ));
196+
}
197+
if (disj == null || cnf == null) {
198+
yield fail(expr.data(), type, BadTypeError.partialElement(state, expr, type));
199+
}
189200
if (!(unifier(expr.sourcePos(), Ordering.Eq).cofibrationEquiv(disj, cnf)))
190201
yield fail(expr.data(), type, new IllegalPartialElement.CofMismatch(disj, cnf, expr.sourcePos(), state()));
191202
// boundary
192203
for (@Closed var c1 : cls)
193204
for (@Closed var c2 : cls) {
194205
if (c1 == c2) continue;
195-
if (!(withConnection(c1.cof().add(c2.cof().descent(whnfVisitor())),
196-
() -> unifier(expr.sourcePos(), Ordering.Eq).compare(c1.tm(), c2.tm(), A) == Decision.YES,
197-
() -> true)))
206+
if (!(withConnection(expandAnd(c1.cof(), (c2.cof().descent(whnfVisitor()))),
207+
() -> unifier(expr.sourcePos(), Ordering.Eq).compare(c1.tm(), c2.tm(), A) == Decision.YES)))
198208
yield fail(expr.data(), type, new IllegalPartialElement.ValueMismatch(c1, c2, expr.sourcePos(), state()));
199209
}
200210
yield new Jdg.Default(new PartialTerm(cls.toSeq()), type);

‎base/src/main/java/org/aya/tyck/error/IllegalPartialElement.java‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44

55
import org.aya.pretty.doc.Doc;
66
import org.aya.states.TyckState;
7+
import org.aya.syntax.core.term.Term;
78
import org.aya.syntax.core.term.xtt.DisjCofNF;
89
import org.aya.syntax.core.term.xtt.PartialTerm;
910
import org.aya.tyck.tycker.Stateful;
@@ -37,4 +38,14 @@ record ValueMismatch(@NotNull PartialTerm.Clause cls1,
3738
return Doc.english("Two partial clauses are different in their intersection"); // TODO: elaborate the info.
3839
}
3940
}
41+
42+
record BadPartialLHS(@NotNull Term lhs,
43+
@NotNull SourcePos sourcePos,
44+
@NotNull TyckState state)
45+
implements IllegalPartialElement {
46+
@Override
47+
public @NotNull Doc describe(@NotNull PrettierOptions options) {
48+
return Doc.english("LHS of this clause is not a cofibration.");
49+
}
50+
}
4051
}

‎base/src/main/java/org/aya/tyck/tycker/Stateful.java‎

Lines changed: 23 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77
import org.aya.normalize.Normalizer;
88
import org.aya.states.TyckState;
99
import org.aya.syntax.core.annotation.Closed;
10-
import org.aya.syntax.core.term.NewTerm;
10+
import org.aya.syntax.core.term.ErrorTerm;
1111
import org.aya.syntax.core.term.Term;
1212
import org.aya.syntax.core.term.xtt.ConjCofNF;
1313
import org.aya.syntax.core.term.xtt.DimTerm;
@@ -33,6 +33,7 @@ public interface Stateful {
3333
@NotNull TyckState state();
3434
default @Closed @NotNull Term whnf(@Closed @NotNull Term term) { return new Normalizer(state()).apply(term); }
3535
default @Nullable DisjCofNF expand(@Closed @NotNull Term term) {return new Normalizer(state()).expand(term); }
36+
default @NotNull DisjCofNF expandAnd(@Closed @NotNull DisjCofNF a, @Closed @NotNull DisjCofNF b) {return new Normalizer(state()).expandAnd(a, b); }
3637
default @NotNull TermVisitor whnfVisitor() {
3738
return TermVisitor.expectTerm(this::whnf);
3839
}
@@ -63,4 +64,25 @@ default <R> R withConnection(@NotNull ConjCofNF cof, @NotNull Supplier<R> action
6364
disconnectConj(cof);
6465
return ret;
6566
}
67+
68+
default Term withConnection(@NotNull DisjCofNF cof, @NotNull Supplier<Term> action, @NotNull Supplier<Term> ifBottom) {
69+
Term ret = null;
70+
for (var conj : cof.elements()) {
71+
ret = withConnection(conj, action, ifBottom);
72+
if (ret instanceof ErrorTerm) {
73+
return ret;
74+
}
75+
}
76+
return ret == null? ifBottom.get() : ret;
77+
}
78+
79+
default boolean withConnection(@NotNull DisjCofNF cof, @NotNull Supplier<Boolean> action) {
80+
for (var conj : cof.elements()) {
81+
if (!withConnection(conj, action, () -> true)) {
82+
return false;
83+
}
84+
}
85+
return true;
86+
}
87+
6688
}

‎base/src/main/java/org/aya/unify/DoubleChecker.java‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -100,10 +100,10 @@ case PartialTerm(var cls) -> {
100100
ImmutableSeq<ConjCofNF> cls_cof = ImmutableSeq.empty();
101101
for (@Closed var c : cls) {
102102
if (!withConnection(c.cof(),
103-
() -> inherit(c.tm(), A),
104-
() -> true)
103+
() -> inherit(c.tm(), A))
105104
) yield failF(new DoubleCheckError.RuleError(preterm, unifier.pos, expected));
106-
cls_cof = cls_cof.appended(c.cof());
105+
// cls_cof = cls_cof || c.cof()
106+
cls_cof = cls_cof.appendedAll(c.cof().elements());
107107
}
108108
// check cofibration
109109
var disj = expand(cof);

‎base/src/main/java/org/aya/unify/TermComparator.java‎

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@
1010
import org.aya.generic.term.SortKind;
1111
import org.aya.prettier.AyaPrettierOptions;
1212
import org.aya.states.TyckState;
13-
import org.aya.states.primitive.PrimFactory;
1413
import org.aya.syntax.core.annotation.Closed;
1514
import org.aya.syntax.core.def.PrimDef;
1615
import org.aya.syntax.core.term.*;
@@ -338,10 +337,8 @@ case PrimCall(var ref, _, var arg) when ref.id() == PrimDef.ID.PARTIAL && arg.si
338337
// if
339338
// forall i j, phi_i ∩ psi_j |- u_i = v_j
340339
for(var cl1 : clauses1) for(var cl2 : clauses2) {
341-
if (withConnection(cl1.cof().add(cl2.cof().descent(whnfVisitor())),
342-
() -> doCompareTyped(whnf(cl1.tm()), whnf(cl2.tm()), A),
343-
() -> Decision.YES)
344-
== Decision.NO)
340+
if (!withConnection(expandAnd(cl1.cof(), cl2.cof().descent(whnfVisitor())),
341+
() -> doCompareTyped(whnf(cl1.tm()), whnf(cl2.tm()), A) == Decision.YES))
345342
yield Decision.NO;
346343
}
347344
yield Decision.YES;

‎cli-impl/src/test/java/org/aya/test/fixtures/ExprTyckError.java‎

Lines changed: 10 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -72,16 +72,19 @@ def what (A : Type) (w : Wrap) : w = w => refl
7272
@Language("Aya") String testBadPartial = """
7373
open import arith::nat::base
7474
open import relation::binary::equality
75-
def test (i : I) : Nat => partial [ i = 1 => 3 ]
75+
open import relation::binary::equality::cubical hiding (I)
76+
77+
def test (i : I) : Nat => partial [ i =f 1 => 3 ]
7678
""";
7779

7880
@Language("Aya") String testPartialMissingClause = """
7981
open import arith::nat::base
8082
open import relation::binary::equality
81-
def test (i j : I) : Partial [ i = 0, j = 1, j = 0 ] Nat =>
83+
open import relation::binary::equality::cubical hiding (I)
84+
def test (i j : I) : Partial ((i =f 0) ∨f (j =f 1) ∨f (j =f 0)) Nat =>
8285
partial
83-
[ i = 0 => 3
84-
, j = 0 => 3
86+
[ i =f 0 => 3
87+
, j =f 0 => 3
8588
]
8689
""";
8790

@@ -90,9 +93,9 @@ def test (i j : I) : Partial [ i = 0, j = 1, j = 0 ] Nat =>
9093
open import relation::binary::equality::cubical
9194
def test (i j : I) : Partial (((i =f 0) ∨f (j =f 1)) ∨f (j =f 0)) Nat =>
9295
partial
93-
[ i = 0 => 3
94-
, j = 0 => 3
95-
, j = 1 => 1
96+
[ i =f 0 => 3
97+
, j =f 0 => 3
98+
, j =f 1 => 1
9699
]
97100
""";
98101
}

‎cli-impl/src/test/resources/negative/ExprTyckError.txt‎

Lines changed: 21 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -262,30 +262,36 @@ Error: Unsolved meta A
262262
Let's learn from that.
263263

264264
BadPartial:
265-
In file $FILE:3:26 ->
265+
In file $FILE:5:26 ->
266266

267-
1 │ open import arith::nat::base
268-
2 │ open import relation::binary::equality
269-
3 │ def test (i : I) : Nat => partial [ i = 1 => 3 ]
270-
│ ╰────────────────────╯
267+
3 │ open import relation::binary::equality::cubical hiding (I)
268+
4 │
269+
5 │ def test (i : I) : Nat => partial [ i =f 1 => 3 ]
270+
│ ╰─────────────────────╯
271271

272272
Error: The following partial element is not good:
273-
partial [i = 1 ⇒ 3]
273+
partial [cofEq i 1 ⇒ 3]
274274
because the type being expected is not a Partial type, but instead:
275275
Nat
276276

277277
1 error(s), 0 warning(s).
278278
Let's learn from that.
279279

280280
PartialMissingClause:
281-
In file $FILE:3:21 ->
281+
In file $FILE:5:2 ->
282282

283-
1 │ open import arith::nat::base
284-
2 │ open import relation::binary::equality
285-
3 │ def test (i j : I) : Partial [ i = 0, j = 1, j = 0 ] Nat =>
286-
│ ╰─────╯
283+
3 │ open import relation::binary::equality::cubical hiding (I)
284+
4 │ def test (i j : I) : Partial ((i =f 0) ∨f (j =f 1) ∨f (j =f 0)) Nat =>
285+
5 │ partial
286+
│ ╭───╯
287+
6 │ │ [ i =f 0 => 3
288+
│ │
289+
7 │ │ , j =f 0 => 3
290+
│ │
291+
8 │ │ ]
292+
│ ╰───╯
287293

288-
Error: The name `Partial` is not defined in the current scope
294+
Error: Two cofibrations are not equivalent to each other.
289295

290296
1 error(s), 0 warning(s).
291297
Let's learn from that.
@@ -297,11 +303,11 @@ In file $FILE:4:2 ->
297303
3 │ def test (i j : I) : Partial (((i =f 0) ∨f (j =f 1)) ∨f (j =f 0)) Nat =>
298304
4 │ partial
299305
│ ╭───╯
300-
5 │ │ [ i = 0 => 3
306+
5 │ │ [ i =f 0 => 3
301307
│ │
302-
6 │ │ , j = 0 => 3
308+
6 │ │ , j =f 0 => 3
303309
│ │
304-
7 │ │ , j = 1 => 1
310+
7 │ │ , j =f 1 => 1
305311
│ │
306312
8 │ │ ]
307313
│ ╰───╯

‎cli-impl/src/test/resources/success/src/Test.aya‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -153,16 +153,16 @@ module Issue1293 {
153153
open import relation::binary::equality::cubical hiding (I)
154154
def test1 (i : I) : Partial ((i =f 0) ∨f (i =f 1)) Nat =>
155155
partial
156-
[ i = 0 => 114
157-
, i = 1 => 514
156+
[ i =f 0 => 114
157+
, i =f 1 => 514
158158
]
159159

160160
def test2 (i j : I) : Partial ((i =f 0) ∨f (j =f 1) ∨f (j =f 0)) Nat =>
161161
partial
162-
[ i = 0 => 114
163-
, j = 1 => 114
164-
, j = 0 => 114
162+
[ i =f 0 => 114
163+
, j =f 1 => 114
164+
, j =f 0 => 114
165165
]
166166

167-
// def test3 (i j : I) : Partial (((i =f 0) ∨f (j =f 1)) ∧f (i =f 1)) Nat
167+
// def test3 (i j : I) : Partial (((i =f 0) ∨f (j =f 1)) ∧f (i =f 1)) Nat
168168
}

‎parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java‎

Lines changed: 0 additions & 3 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

0 commit comments

Comments
 (0)