From b4999945997408ba5e674f52972ff6ccfb8a9a68 Mon Sep 17 00:00:00 2001 From: valis Date: Wed, 20 Nov 2024 20:08:28 +0300 Subject: [PATCH] Fix missing clauses error in presence of external variables --- .../doubleChecker/CoreExpressionChecker.java | 2 +- .../patternmatching/ElimTypechecking.java | 11 ++++++++++- .../patternmatching/PatternTypechecking.java | 2 +- .../arend/typechecking/visitor/CheckTypeVisitor.java | 2 +- .../typechecking/visitor/DefinitionTypechecker.java | 2 +- src/test/java/org/arend/typechecking/VarsTest.java | 11 +++++++++++ 6 files changed, 25 insertions(+), 5 deletions(-) diff --git a/base/src/main/java/org/arend/typechecking/doubleChecker/CoreExpressionChecker.java b/base/src/main/java/org/arend/typechecking/doubleChecker/CoreExpressionChecker.java index 22d9a9152..2c5195b3c 100644 --- a/base/src/main/java/org/arend/typechecking/doubleChecker/CoreExpressionChecker.java +++ b/base/src/main/java/org/arend/typechecking/doubleChecker/CoreExpressionChecker.java @@ -841,7 +841,7 @@ void checkElimBody(FunctionDefinition definition, ElimBody elimBody, DependentLi Sort sort = type.getSortOfType(); ErrorReporter errorReporter = new MyErrorReporter(errorExpr); - ElimBody newBody = new ElimTypechecking(errorReporter, myEquations, type, mode, level, sort != null ? sort.getHLevel() : Level.INFINITY, isSFunc, null, mySourceNode).typecheckElim(exprClauses, parameters); + ElimBody newBody = new ElimTypechecking(errorReporter, myEquations, type, mode, level, sort != null ? sort.getHLevel() : Level.INFINITY, isSFunc, null, 0, mySourceNode).typecheckElim(exprClauses, parameters); if (newBody == null) { throw new CoreException(CoreErrorWrapper.make(new TypecheckingError("Cannot check the body", mySourceNode), errorExpr)); } diff --git a/base/src/main/java/org/arend/typechecking/patternmatching/ElimTypechecking.java b/base/src/main/java/org/arend/typechecking/patternmatching/ElimTypechecking.java index ef467b4c6..d00f92cae 100644 --- a/base/src/main/java/org/arend/typechecking/patternmatching/ElimTypechecking.java +++ b/base/src/main/java/org/arend/typechecking/patternmatching/ElimTypechecking.java @@ -54,6 +54,7 @@ public class ElimTypechecking { private final Concrete.SourceNode mySourceNode; private boolean myAllowInterval = true; private List myCoreClauses; + private final int myNumberOfExternalParameters; private static Integer getMinPlus1(Integer level1, Level l2, int sub) { Integer level2 = !l2.isInfinity() && l2.isClosed() ? l2.getConstant() : null; @@ -61,12 +62,13 @@ private static Integer getMinPlus1(Integer level1, Level l2, int sub) { return result == null ? null : result + 1; } - public ElimTypechecking(@Nullable ErrorReporter errorReporter, Equations equations, Expression expectedType, PatternTypechecking.Mode mode, @Nullable Integer level, @NotNull Level actualLevel, boolean isSFunc, List clauses, Concrete.SourceNode sourceNode) { + public ElimTypechecking(@Nullable ErrorReporter errorReporter, Equations equations, Expression expectedType, PatternTypechecking.Mode mode, @Nullable Integer level, @NotNull Level actualLevel, boolean isSFunc, List clauses, int numberOfExternalParameters, Concrete.SourceNode sourceNode) { myErrorReporter = errorReporter; myEquations = equations; myExpectedType = expectedType; myMode = mode; myClauses = clauses; + myNumberOfExternalParameters = numberOfExternalParameters; mySourceNode = sourceNode; int actualLevelSub = 0; @@ -112,6 +114,7 @@ public ElimTypechecking(@Nullable ErrorReporter errorReporter, Equations equatio myActualLevel = Level.INFINITY; myActualLevelSub = 0; myClauses = clauses; + myNumberOfExternalParameters = 0; mySourceNode = sourceNode; } @@ -527,6 +530,12 @@ private Map elimParams) { if (myErrorReporter == null) return null; + if (elimParams.isEmpty()) { + for (int i = 0; i < myNumberOfExternalParameters && parameters.hasNext(); i++) { + parameters = parameters.getNext(); + } + } + if (parameters.hasNext() && !parameters.getNext().hasNext()) { DataCallExpression dataCall = parameters.getTypeExpr().cast(DataCallExpression.class); if (dataCall != null && dataCall.getDefinition() == Prelude.INTERVAL) { diff --git a/base/src/main/java/org/arend/typechecking/patternmatching/PatternTypechecking.java b/base/src/main/java/org/arend/typechecking/patternmatching/PatternTypechecking.java index 75b1439f9..70976c559 100644 --- a/base/src/main/java/org/arend/typechecking/patternmatching/PatternTypechecking.java +++ b/base/src/main/java/org/arend/typechecking/patternmatching/PatternTypechecking.java @@ -193,7 +193,7 @@ private boolean typecheckClause(Concrete.FunctionClause clause, List intervalBindings; Expression exprType = expectedType; if (!myPathPatterns.isEmpty()) { - Body body = new ElimTypechecking(null, null, null, myMode, null, Level.INFINITY, false, null, null).typecheckElim(resultClauses, parameters, myElimParams); + Body body = new ElimTypechecking(null, null, null, myMode, null, Level.INFINITY, false, null, 0, null).typecheckElim(resultClauses, parameters, myElimParams); if (body == null) { myErrorReporter.report(new TypecheckingError("Cannot compute body", clause)); return false; diff --git a/base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java b/base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java index a7040bc9a..1b328f99f 100644 --- a/base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java +++ b/base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java @@ -4108,7 +4108,7 @@ public TypecheckingResult visitCase(Concrete.CaseExpression expr, Expression exp if (clauses == null) { return null; } - ElimBody elimBody = new ElimTypechecking(errorReporter, myEquations, resultExpr, PatternTypechecking.Mode.CASE, level, actualLevel, expr.isSCase(), expr.getClauses(), expr).typecheckElim(clauses, list.getFirst()); + ElimBody elimBody = new ElimTypechecking(errorReporter, myEquations, resultExpr, PatternTypechecking.Mode.CASE, level, actualLevel, expr.isSCase(), expr.getClauses(), 0, expr).typecheckElim(clauses, list.getFirst()); if (elimBody == null) { return null; } diff --git a/base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java b/base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java index 3869d278f..67b997dd4 100644 --- a/base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java +++ b/base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java @@ -1612,7 +1612,7 @@ private List typecheckFunctionBody(FunctionDefinition typedDef, C clauses = typechecker.withErrorReporter(countingErrorReporter, tc -> new PatternTypechecking(PatternTypechecking.Mode.FUNCTION, typechecker, true, null, elimParams).typecheckClauses(elimBody.getClauses(), def.getParameters(), typedDef.getParameters(), expectedType, myNewDef ? typedDef : null)); } Sort sort = expectedType.getSortOfType(); - Body typedBody = clauses == null || def.getKind() == FunctionKind.AXIOM ? null : new ElimTypechecking(errorReporter, typechecker.getEquations(), expectedType, PatternTypechecking.Mode.FUNCTION, typeLevel, sort != null ? sort.getHLevel() : Level.INFINITY, kind.isSFunc() && kind != FunctionKind.TYPE, elimBody.getClauses(), def).typecheckElim(clauses, typedDef.getParameters(), elimParams); + Body typedBody = clauses == null || def.getKind() == FunctionKind.AXIOM ? null : new ElimTypechecking(errorReporter, typechecker.getEquations(), expectedType, PatternTypechecking.Mode.FUNCTION, typeLevel, sort != null ? sort.getHLevel() : Level.INFINITY, kind.isSFunc() && kind != FunctionKind.TYPE, elimBody.getClauses(), typedDef.getParametersOriginalDefinitions().size(), def).typecheckElim(clauses, typedDef.getParameters(), elimParams); if (typedBody != null) { if (myNewDef) { typedDef.setBody(typedBody); diff --git a/src/test/java/org/arend/typechecking/VarsTest.java b/src/test/java/org/arend/typechecking/VarsTest.java index a33eeca3c..c8522658d 100644 --- a/src/test/java/org/arend/typechecking/VarsTest.java +++ b/src/test/java/org/arend/typechecking/VarsTest.java @@ -908,4 +908,15 @@ public void coclauseElimScopeTest2() { } """); } + + @Test + public void patternMatchingTest2() { + typeCheckModule(""" + \\func f {m : Nat} => m \\where { + \\func g (n : Nat) : Nat \\with + | 0 => m + | suc n => n + } + """); + } }