Fix missing clauses error in presence of external variables

JetBrains · Nov 20, 2024 · b499994 · b499994
1 parent fc01f9e
commit b499994
Show file tree

Hide file tree

Showing 6 changed files with 25 additions and 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
@@ -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
@@ -54,19 +54,21 @@ public class ElimTypechecking {
   private final Concrete.SourceNode mySourceNode;
   private boolean myAllowInterval = true;
   private List<ExtElimClause> myCoreClauses;
+  private final int myNumberOfExternalParameters;
 
   private static Integer getMinPlus1(Integer level1, Level l2, int sub) {
     Integer level2 = !l2.isInfinity() && l2.isClosed() ? l2.getConstant() : null;
     Integer result = level1 != null && level2 != null ? Integer.valueOf(Math.min(level1, level2 - sub)) : level2 != null ? Integer.valueOf(level2 - sub) : level1;
     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<? extends Concrete.FunctionClause> 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<? extends Concrete.FunctionClause> 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<DependentLink, List<Pair<ExpressionPattern, Map<DependentLink, Const
 
   private DependentLink reportNoClauses(DependentLink parameters, List<DependentLink> 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
@@ -193,7 +193,7 @@ private boolean typecheckClause(Concrete.FunctionClause clause, List<? extends C
         List<Binding> 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
@@ -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
@@ -1612,7 +1612,7 @@ private List<ExtElimClause> 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
@@ -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
+      }
+      """);
+  }
 }