Fix some problems with number pattern checker

JetBrains · Oct 24, 2020 · 5d83b35 · 5d83b35
1 parent 8ecb1a5
commit 5d83b35
Show file tree

Hide file tree

Showing 4 changed files with 35 additions and 15 deletions.
diff --git a/base/src/main/java/org/arend/extImpl/ConcreteFactoryImpl.java b/base/src/main/java/org/arend/extImpl/ConcreteFactoryImpl.java
@@ -588,20 +588,20 @@ public ConcretePattern refPattern(@Nullable ArendRef ref, @Nullable ConcreteExpr
   @NotNull
   @Override
   public ConcretePattern tuplePattern(@NotNull ConcretePattern... subpatterns) {
-    return new Concrete.TuplePattern(myData, true, patterns(Arrays.asList(subpatterns)), new ArrayList<>(1));
+    return new Concrete.TuplePattern(myData, true, patterns(Arrays.asList(subpatterns)), Collections.emptyList());
   }
 
   @Override
   public @NotNull ConcretePattern tuplePattern(@NotNull Collection<? extends ConcretePattern> subpatterns) {
-    return new Concrete.TuplePattern(myData, true, patterns(subpatterns), new ArrayList<>(1));
+    return new Concrete.TuplePattern(myData, true, patterns(subpatterns), Collections.emptyList());
   }
 
   @NotNull
   @Override
   public ConcretePattern numberPattern(int number) {
     if (number > Concrete.NumberPattern.MAX_VALUE) number = Concrete.NumberPattern.MAX_VALUE;
     if (number < -Concrete.NumberPattern.MAX_VALUE) number = -Concrete.NumberPattern.MAX_VALUE;
-    return new Concrete.NumberPattern(myData, number, new ArrayList<>(1));
+    return new Concrete.NumberPattern(myData, number, Collections.emptyList());
   }
 
   @NotNull
@@ -610,15 +610,15 @@ public ConcretePattern conPattern(@NotNull ArendRef constructor, @NotNull Concre
     if (!(constructor instanceof Referable)) {
       throw new IllegalArgumentException();
     }
-    return new Concrete.ConstructorPattern(myData, true, (Referable) constructor, patterns(Arrays.asList(subpatterns)), new ArrayList<>(1));
+    return new Concrete.ConstructorPattern(myData, true, (Referable) constructor, patterns(Arrays.asList(subpatterns)), Collections.emptyList());
   }
 
   @Override
   public @NotNull ConcretePattern conPattern(@NotNull ArendRef constructor, @NotNull Collection<? extends ConcretePattern> subpatterns) {
     if (!(constructor instanceof Referable)) {
       throw new IllegalArgumentException();
     }
-    return new Concrete.ConstructorPattern(myData, true, (Referable) constructor, patterns(subpatterns), new ArrayList<>(1));
+    return new Concrete.ConstructorPattern(myData, true, (Referable) constructor, patterns(subpatterns), Collections.emptyList());
   }
 
   @NotNull

diff --git a/base/src/main/java/org/arend/term/concrete/Concrete.java b/base/src/main/java/org/arend/term/concrete/Concrete.java
@@ -2324,7 +2324,7 @@ public interface PatternHolder {
   public static abstract class Pattern extends SourceNodeImpl implements ConcretePattern {
     public static final byte PREC = 11;
     private boolean myExplicit;
-    private final List<TypedReferable> myAsReferables;
+    private List<TypedReferable> myAsReferables;
 
     public Pattern(Object data, List<TypedReferable> asReferables) {
       super(data);
@@ -2355,6 +2355,9 @@ public ConcretePattern as(@NotNull ArendRef ref, @Nullable ConcreteExpression ty
       if (!(ref instanceof Referable && type instanceof Expression)) {
         throw new IllegalArgumentException();
       }
+      if (myAsReferables.isEmpty()) {
+        myAsReferables = new ArrayList<>();
+      }
       myAsReferables.add(new TypedReferable(null, (Referable) ref, (Expression) type));
       return this;
     }
@@ -2363,6 +2366,10 @@ public ConcretePattern as(@NotNull ArendRef ref, @Nullable ConcreteExpression ty
     public List<TypedReferable> getAsReferables() {
       return myAsReferables;
     }
+
+    public void setAsReferables(List<TypedReferable> asReferables) {
+      myAsReferables = asReferables;
+    }
   }
 
   public static class NumberPattern extends Pattern implements ConcreteNumberPattern {

diff --git a/base/src/main/java/org/arend/typechecking/patternmatching/PatternTypechecking.java b/base/src/main/java/org/arend/typechecking/patternmatching/PatternTypechecking.java
@@ -25,6 +25,7 @@
 import org.arend.core.subst.ExprSubstitution;
 import org.arend.core.subst.LevelSubstitution;
 import org.arend.core.subst.SubstVisitor;
+import org.arend.ext.concrete.ConcretePattern;
 import org.arend.ext.concrete.ConcreteSourceNode;
 import org.arend.ext.core.ops.CMP;
 import org.arend.ext.core.ops.NormalizationMode;
@@ -33,7 +34,6 @@
 import org.arend.ext.error.TypecheckingError;
 import org.arend.ext.prettyprinting.doc.DocFactory;
 import org.arend.extImpl.definitionRenamer.PatternContextDataImpl;
-import org.arend.naming.reference.FakeLocalReferable;
 import org.arend.naming.reference.GlobalReferable;
 import org.arend.naming.reference.Referable;
 import org.arend.naming.reference.TCDefReferable;
@@ -388,13 +388,11 @@ private Result doTypechecking(List<Concrete.Pattern> patterns, DependentLink par
       if (pattern instanceof Concrete.NumberPattern) {
         var newPattern = translateNumberPatterns((Concrete.NumberPattern) pattern, expr);
         if (newPattern == null) {
-          myErrorReporter.report(new CertainTypecheckingError(CertainTypecheckingError.Kind.PATTERN_IGNORED, pattern));
-          var newParam = parameters.subst(new SubstVisitor(paramsSubst, LevelSubstitution.EMPTY), 1, false);
-          linkList.append(newParam);
-          result.add(new BindingPattern(newParam));
-          exprs.add(new ReferenceExpression(newParam));
-          addBinding(null, newParam);
-          parameters = parameters.getNext();
+          return null;
+        }
+        newPattern.setExplicit(pattern.isExplicit());
+        if (newPattern instanceof Concrete.NamePattern) {
+          patterns.set(k--, newPattern);
           continue;
         } else {
           pattern = newPattern;
@@ -795,7 +793,19 @@ private Result doTypechecking(List<Concrete.Pattern> patterns, DependentLink par
     if (checker == null) {
       return DesugarVisitor.desugarNumberPattern(pattern, myErrorReporter);
     }
-    return (Concrete.Pattern) checker.desugarNumberPattern(pattern, myVisitor, new PatternContextDataImpl(typeExpr, pattern));
+
+    int numberOfErrors = myVisitor.getNumberOfErrors();
+    ConcretePattern result = checker.desugarNumberPattern(pattern, myVisitor, new PatternContextDataImpl(typeExpr, pattern));
+    if (result == null && myVisitor.getNumberOfErrors() == numberOfErrors) {
+      myErrorReporter.report(new TypecheckingError("Cannot typecheck pattern", pattern));
+    }
+    if (result != null && !(result instanceof Concrete.Pattern)) {
+      throw new IllegalStateException("ConcretePattern must be created with ConcreteFactory");
+    }
+    if (result instanceof Concrete.NumberPattern) {
+      throw new IllegalStateException("desugarNumberPattern should not return ConcreteNumberPattern");
+    }
+    return (Concrete.Pattern) result;
   }
 
   // Chains the bindings in the leaves of patterns

diff --git a/base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java b/base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java
@@ -389,6 +389,9 @@ public TypecheckingResult check(@NotNull UncheckedExpression expression, @NotNul
 
   @Override
   public @NotNull Concrete.Pattern desugarNumberPattern(@NotNull ConcreteNumberPattern pattern) {
+    if (!(pattern instanceof Concrete.NumberPattern)) {
+      throw new IllegalArgumentException();
+    }
     return DesugarVisitor.desugarNumberPattern((Concrete.NumberPattern) pattern, errorReporter);
   }