Skip to content

Commit

Permalink
Fixed a bug with \cons
Browse files Browse the repository at this point in the history
  • Loading branch information
@valis
valis committed Jul 28, 2020
1 parent 367a5cd commit 4db21e3
Show file tree
Hide file tree
Showing 7 changed files with 128 additions and 10 deletions.
10 changes: 10 additions & 0 deletions base/src/main/java/org/arend/core/pattern/BindingPattern.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,16 @@ public List<? extends ExpressionPattern> getSubPatterns() {
return Collections.emptyList();
}

@Override
public Concrete.Pattern toConcrete(Object data, boolean isExplicit, Map<DependentLink, Concrete.Pattern> subPatterns) {
Concrete.Pattern subPattern = subPatterns.get(myBinding);
if (subPattern != null && subPattern.isExplicit() != isExplicit) {
subPattern = subPattern.copy();
subPattern.setExplicit(isExplicit);
}
return subPattern == null ? new Concrete.NamePattern(data, isExplicit, null, null) : subPattern;
}

@Override
public DependentLink replaceBindings(DependentLink link, List<Pattern> result) {
result.add(new BindingPattern(link));
Expand Down
20 changes: 20 additions & 0 deletions base/src/main/java/org/arend/core/pattern/ConstructorExpressionPattern.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,26 @@ public List<? extends ExpressionPattern> getSubPatterns() {
return (List<? extends ExpressionPattern>) super.getSubPatterns();
}

@Override
public Concrete.Pattern toConcrete(Object data, boolean isExplicit, Map<DependentLink, Concrete.Pattern> subPatterns) {
Definition definition = getDefinition();
DependentLink param = definition != null ? definition.getParameters() : EmptyDependentLink.getInstance();

List<Concrete.Pattern> patterns = new ArrayList<>();
for (ExpressionPattern subPattern : getSubPatterns()) {
patterns.add(subPattern.toConcrete(data, !param.hasNext() || param.isExplicit(), subPatterns));
if (param.hasNext()) {
param = param.getNext();
}
}

if (definition != null && !(definition instanceof ClassDefinition)) {
return new Concrete.ConstructorPattern(data, isExplicit, definition.getRef(), patterns, Collections.emptyList());
} else {
return new Concrete.TuplePattern(data, isExplicit, patterns, Collections.emptyList());
}
}

@Override
public DependentLink replaceBindings(DependentLink link, List<Pattern> result) {
List<ExpressionPattern> subPatterns = new ArrayList<>();
Expand Down
5 changes: 5 additions & 0 deletions base/src/main/java/org/arend/core/pattern/EmptyPattern.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,11 @@ public List<ExpressionPattern> getSubPatterns() {
return Collections.emptyList();
}

@Override
public Concrete.Pattern toConcrete(Object data, boolean isExplicit, Map<DependentLink, Concrete.Pattern> subPatterns) {
return new Concrete.TuplePattern(data, isExplicit, Collections.emptyList(), Collections.emptyList());
}

@Override
public boolean isAbsurd() {
return true;
Expand Down
1 change: 1 addition & 0 deletions base/src/main/java/org/arend/core/pattern/ExpressionPattern.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ public interface ExpressionPattern extends Pattern {
ExpressionPattern subst(ExprSubstitution exprSubst, LevelSubstitution levelSubst, Map<DependentLink, ExpressionPattern> patternSubst);
Pattern removeExpressions();
@Override @NotNull List<? extends ExpressionPattern> getSubPatterns();
Concrete.Pattern toConcrete(Object data, boolean isExplicit, Map<DependentLink, Concrete.Pattern> subPatterns);

default Expression toPatternExpression() {
return toExpression();
Expand Down
24 changes: 24 additions & 0 deletions base/src/main/java/org/arend/term/concrete/Concrete.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2072,6 +2072,8 @@ public void setExplicit(boolean isExplicit) {
myExplicit = isExplicit;
}

public abstract Pattern copy();

@NotNull
@Override
public ConcretePattern implicit() {
Expand Down Expand Up @@ -2107,6 +2109,13 @@ public NumberPattern(Object data, int number, List<TypedReferable> asReferables)
public int getNumber() {
return myNumber;
}

@Override
public Pattern copy() {
NumberPattern result = new NumberPattern(getData(), myNumber, getAsReferables());
result.setExplicit(isExplicit());
return result;
}
}

public static class NamePattern extends Pattern {
Expand All @@ -2125,6 +2134,11 @@ public Referable getReferable() {
return myReferable;
}

@Override
public Pattern copy() {
return new NamePattern(getData(), isExplicit(), myReferable, type);
}

@NotNull
@Override
public ConcretePattern as(@NotNull ArendRef ref, @Nullable ConcreteExpression type) {
Expand Down Expand Up @@ -2184,6 +2198,11 @@ public List<Pattern> getPatterns() {
public ConstructorPattern getSourceNode() {
return this;
}

@Override
public Pattern copy() {
return new ConstructorPattern(getData(), isExplicit(), myConstructor, myArguments, getAsReferables());
}
}

public static class TuplePattern extends Pattern {
Expand All @@ -2203,5 +2222,10 @@ public TuplePattern(Object data, boolean isExplicit, List<Pattern> patterns, Lis
public List<Pattern> getPatterns() {
return myPatterns;
}

@Override
public Pattern copy() {
return new TuplePattern(getData(), isExplicit(), myPatterns, getAsReferables());
}
}
}
69 changes: 59 additions & 10 deletions base/src/main/java/org/arend/typechecking/patternmatching/PatternTypechecking.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -194,7 +194,7 @@ private ExtElimClause typecheckClause(Concrete.FunctionClause clause, List<? ext
}
}

public Result typecheckPatterns(List<? extends Concrete.Pattern> patterns, List<? extends Concrete.Parameter> abstractParameters, DependentLink parameters, ExprSubstitution substitution, ExprSubstitution totalSubst, List<DependentLink> elimParams, Concrete.SourceNode sourceNode) {
public Result typecheckPatterns(List<Concrete.Pattern> patterns, List<? extends Concrete.Parameter> abstractParameters, DependentLink parameters, ExprSubstitution substitution, ExprSubstitution totalSubst, List<DependentLink> elimParams, Concrete.SourceNode sourceNode) {
assert myVisitor != null;
myContext = myVisitor.getContext();
if (myMode.isContextFree()) {
Expand Down Expand Up @@ -230,7 +230,7 @@ public Result typecheckPatterns(List<? extends Concrete.Pattern> patterns, List<
}

@TestOnly
Pair<List<ExpressionPattern>, Map<Referable, Binding>> typecheckPatterns(List<? extends Concrete.Pattern> patterns, DependentLink parameters, Concrete.SourceNode sourceNode, @SuppressWarnings("SameParameterValue") boolean withElim) {
Pair<List<ExpressionPattern>, Map<Referable, Binding>> typecheckPatterns(List<Concrete.Pattern> patterns, DependentLink parameters, Concrete.SourceNode sourceNode, @SuppressWarnings("SameParameterValue") boolean withElim) {
myContext = myVisitor == null ? new HashMap<>() : myVisitor.getContext();
Result result = doTypechecking(patterns, parameters, new LinkList(), new ExprSubstitution(), null, sourceNode, withElim);
if (result == null) {
Expand Down Expand Up @@ -274,7 +274,7 @@ private void typecheckAsPatterns(List<Concrete.TypedReferable> asPatterns, Expre
}
}

private Result doTypechecking(List<? extends Concrete.Pattern> patterns, DependentLink parameters, ExprSubstitution paramSubst, ExprSubstitution totalSubst, List<DependentLink> elimParams, Concrete.SourceNode sourceNode) {
private Result doTypechecking(List<Concrete.Pattern> patterns, DependentLink parameters, ExprSubstitution paramSubst, ExprSubstitution totalSubst, List<DependentLink> elimParams, Concrete.SourceNode sourceNode) {
// Put patterns in the correct order
// If some parameters are not eliminated (i.e. absent in elimParams), then we put null in corresponding patterns
if (!elimParams.isEmpty()) {
Expand Down Expand Up @@ -329,12 +329,13 @@ private static void listSubst(List<ExpressionPattern> patterns, List<Expression>
}
}

private Result doTypechecking(List<? extends Concrete.Pattern> patterns, DependentLink parameters, LinkList linkList, ExprSubstitution paramsSubst, ExprSubstitution totalSubst, Concrete.SourceNode sourceNode, boolean withElim) {
private Result doTypechecking(List<Concrete.Pattern> patterns, DependentLink parameters, LinkList linkList, ExprSubstitution paramsSubst, ExprSubstitution totalSubst, Concrete.SourceNode sourceNode, boolean withElim) {
List<ExpressionPattern> result = new ArrayList<>();
List<Expression> exprs = new ArrayList<>();
ExprSubstitution varSubst = new ExprSubstitution();

for (Concrete.Pattern pattern : patterns) {
for (int k = 0; k < patterns.size(); k++) {
Concrete.Pattern pattern = patterns.get(k);
if (!parameters.hasNext()) {
myErrorReporter.report(new CertainTypecheckingError(CertainTypecheckingError.Kind.TOO_MANY_PATTERNS, pattern));
return null;
Expand Down Expand Up @@ -555,21 +556,61 @@ private Result doTypechecking(List<? extends Concrete.Pattern> patterns, Depende
sortArg = Sort.generateInferVars(myVisitor.getEquations(), def.getUniverseKind(), conPattern);
LevelSubstitution levelSubst = sortArg.toLevelSubstitution();

if (constructor.getNumberOfParameters() > 0) {
FreeVariablesCollector collector = new FreeVariablesCollector();
constructor.getResultType().accept(collector, null);
if (constructor.getNumberOfParameters() > 0 || !collector.getResult().isEmpty()) {
Set<Binding> bindings = myVisitor.getAllBindings();
for (int i = 0; i < constructor.getNumberOfParameters(); i++) {
int i = 0;
for (; i < constructor.getNumberOfParameters(); i++) {
Expression arg = new InferenceReferenceExpression(new FunctionInferenceVariable(constructor, link, i + 1, link.getTypeExpr().subst(substitution, levelSubst), conPattern, bindings), myVisitor.getEquations());
args.add(arg);
substitution.add(link, arg);
collector.getResult().remove(link);
link = link.getNext();
}
if (!collector.getResult().isEmpty()) {
for (DependentLink link1 = link; link1.hasNext(); link1 = link1.getNext(), i++) {
substitution.add(link1, new InferenceReferenceExpression(new FunctionInferenceVariable(constructor, link1, i + 1, link1.getTypeExpr().subst(substitution, levelSubst), conPattern, bindings), myVisitor.getEquations()));
}
}
}

Expression actualType = constructor.getResultType().subst(substitution, levelSubst).normalize(NormalizationMode.WHNF);
if (!CompareVisitor.compare(myVisitor.getEquations(), CMP.EQ, actualType, expr, Type.OMEGA, conPattern)) {
myErrorReporter.report(new TypeMismatchError(expr, actualType, conPattern));
return null;
}
myVisitor.getEquations().solveEquations();

Map<DependentLink, Concrete.Pattern> concretePatterns = new HashMap<>();
DependentLink param = constructor.getParameters();
for (int j = 0; j < constructor.getNumberOfParameters() && param.hasNext(); j++) {
param = param.getNext();
}

for (Concrete.Pattern subPattern : conPattern.getPatterns()) {
while (param.hasNext() && subPattern.isExplicit() && !param.isExplicit()) {
param = param.getNext();
}
if (!param.hasNext()) {
break;
}

if (param.isExplicit() != subPattern.isExplicit()) {
myErrorReporter.report(new CertainTypecheckingError(CertainTypecheckingError.Kind.EXPECTED_EXPLICIT_PATTERN, subPattern));
continue;
}

concretePatterns.put(param, subPattern);
param = param.getNext();
}

if (param.hasNext()) {
myErrorReporter.report(new NotEnoughPatternsError(DependentLink.Helper.size(param), conPattern));
}

patterns.set(k--, constructor.getPattern().toConcrete(conPattern.getData(), conPattern.isExplicit(), concretePatterns));
continue;
}
myVisitor.getEquations().solveEquations();
LevelSubstitution levelSolution = myFinal ? myVisitor.getEquations().solveLevels(conPattern) : LevelSubstitution.EMPTY;
Expand All @@ -588,9 +629,17 @@ private Result doTypechecking(List<? extends Concrete.Pattern> patterns, Depende
}

Map<DependentLink, ExpressionPattern> patternSubst = new HashMap<>();
DependentLink link1 = link;
for (ExpressionPattern patternArg : conResult.patterns) {
patternSubst.put(link, patternArg);
link = link.getNext();
patternSubst.put(link1, patternArg);
link1 = link1.getNext();
}
if (conResult.exprs != null) {
link1 = link;
for (Expression expression : conResult.exprs) {
substitution.add(link1, expression);
link1 = link1.getNext();
}
}

substitution.subst(conResult.varSubst);
Expand Down Expand Up @@ -655,7 +704,7 @@ private Result doTypechecking(List<? extends Concrete.Pattern> patterns, Depende

Constructor constructor = conPattern.getConstructor() instanceof GlobalReferable ? dataCall.getDefinition().getConstructor((GlobalReferable) conPattern.getConstructor()) : null;
List<ConCallExpression> conCalls = new ArrayList<>(1);
if (constructor == null || !dataCall.getMatchedConCall(constructor, conCalls) || conCalls.isEmpty() ) {
if (constructor == null || !dataCall.getMatchedConCall(constructor, conCalls) || conCalls.isEmpty()) {
Referable conRef = conPattern.getConstructor();
if (constructor != null || conRef instanceof TCReferable && ((TCReferable) conRef).getKind() == GlobalReferable.Kind.CONSTRUCTOR) {
myErrorReporter.report(new ExpectedConstructorError((GlobalReferable) conRef, dataCall, conPattern));
Expand Down
9 changes: 9 additions & 0 deletions src/test/java/org/arend/typechecking/definition/ConstructorTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -244,4 +244,13 @@ public void goalTest() {
typeCheckDef("\\cons test => suc {?}", 1);
assertThatErrorsAre(goalError());
}

@Test
public void dependentTypeTest() {
typeCheckModule(
"\\data D (n : Nat) | con {m : Nat} (m = n)\n" +
"\\cons con2 (x : Nat) : D x => con idp\n" +
"\\func f (d : D 0) : Nat | con2 y => y\n" +
"\\func test : f (con idp) = 0 => idp");
}
}

0 comments on commit 4db21e3

Please sign in to comment.