Allow to compute minimal types in API

JetBrains · Jul 8, 2022 · 81b4f2d · 81b4f2d
1 parent cf0963c
commit 81b4f2d
Show file tree

Hide file tree

Showing 2 changed files with 28 additions and 3 deletions.
diff --git a/api/src/main/java/org/arend/ext/core/expr/CoreExpression.java b/api/src/main/java/org/arend/ext/core/expr/CoreExpression.java
@@ -30,11 +30,25 @@ public interface CoreExpression extends CoreBody, UncheckedExpression, Abstracte
    */
   @Override @NotNull CoreExpression getUnderlyingExpression();
 
+  /**
+   * Computes the type of this expression.
+   *
+   * @param minimal if true, the levels of the expression will be minimized.
+   */
+  @NotNull CoreExpression computeType(boolean minimal);
+
   /**
    * Computes the type of this expression.
    */
   @NotNull CoreExpression computeType();
 
+  /**
+   * Computes the type of this expression and returns the expression with the type.
+   *
+   * @param minimal if true, the levels of the expression will be minimized before computing the type.
+   */
+  @NotNull TypedExpression computeTyped(boolean minimal);
+
   /**
    * Computes the type of this expression and returns the expression with the type.
    */

diff --git a/base/src/main/java/org/arend/core/expr/Expression.java b/base/src/main/java/org/arend/core/expr/Expression.java
@@ -11,6 +11,7 @@
 import org.arend.ext.concrete.ConcreteSourceNode;
 import org.arend.ext.core.expr.*;
 import org.arend.ext.error.ErrorReporter;
+import org.arend.ext.typechecking.TypedExpression;
 import org.arend.ext.variable.Variable;
 import org.arend.core.context.binding.inference.InferenceVariable;
 import org.arend.core.context.param.DependentLink;
@@ -135,14 +136,24 @@ public Expression getType() {
   }
 
   @Override
-  public @NotNull Expression computeType() {
-    Expression type = getType(true);
+  public @NotNull Expression computeType(boolean minimal) {
+    Expression type = getType(minimal);
     return type != null ? type : new ErrorExpression(new TypeComputationError(null, this, null));
   }
 
+  @Override
+  public @NotNull Expression computeType() {
+    return computeType(false);
+  }
+
+  @Override
+  public @NotNull TypecheckingResult computeTyped(boolean minimal) {
+    return new TypecheckingResult(this, computeType(minimal));
+  }
+
   @Override
   public @NotNull TypecheckingResult computeTyped() {
-    return new TypecheckingResult(this, computeType());
+    return computeTyped(false);
   }
 
   public boolean findBinding(Variable binding) {