Naive implementation of subst (#233)

JetBrains · Aug 9, 2020 · 9f2a6ee · 9f2a6ee
1 parent 842b978
commit 9f2a6ee
Show file tree

Hide file tree

Showing 2 changed files with 49 additions and 2 deletions.
diff --git a/base/src/main/java/org/arend/term/concrete/ConcreteSubstitution.java b/base/src/main/java/org/arend/term/concrete/ConcreteSubstitution.java
@@ -0,0 +1,38 @@
+package org.arend.term.concrete;
+
+import org.arend.naming.reference.Referable;
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+
+import java.util.HashMap;
+import java.util.Map;
+
+public class ConcreteSubstitution extends BaseConcreteExpressionVisitor<Void> {
+  private final Map<Referable, Concrete.Expression> mySubstitution;
+
+  public ConcreteSubstitution(@NotNull Map<Referable, Concrete.Expression> substitution) {
+    mySubstitution = substitution;
+  }
+
+  public ConcreteSubstitution() {
+    this(new HashMap<>());
+  }
+
+  public void bind(@NotNull Referable referable, @Nullable Concrete.Expression expression) {
+    mySubstitution.put(referable, expression);
+  }
+
+  public void unbind(@NotNull Referable referable) {
+    mySubstitution.remove(referable);
+  }
+
+  public int size() {
+    return mySubstitution.size();
+  }
+
+  @Override
+  public Concrete.Expression visitReference(Concrete.ReferenceExpression expr, Void params) {
+    var subst = mySubstitution.get(expr.getReferent());
+    return subst != null ? subst : super.visitReference(expr, params);
+  }
+}
diff --git a/base/src/main/java/org/arend/term/concrete/DefinableMetaDefinition.java b/base/src/main/java/org/arend/term/concrete/DefinableMetaDefinition.java
@@ -15,6 +15,7 @@
 import org.jetbrains.annotations.Nullable;
 
 import java.util.List;
+import java.util.Objects;
 
 /**
  * User-defined meta in Arend, not Java extension meta.
@@ -71,8 +72,16 @@ public boolean checkContextData(@NotNull ContextData contextData, @NotNull Error
 
   @Override
   public @Nullable TypedExpression invokeMeta(@NotNull ExpressionTypechecker typechecker, @NotNull ContextData contextData) {
-    // TODO[meta]: implement this
-    return null;
+    var arguments = contextData.getArguments();
+    assert myParameters.size() == arguments.size();
+    var subst = new ConcreteSubstitution();
+    for (int i = 0; i < myParameters.size(); i++) {
+      subst.bind(Objects.requireNonNull(myParameters.get(i).getReferable()),
+        (Concrete.Expression) arguments.get(i).getExpression());
+    }
+    // TODO[meta]: clone the expression
+    var substExpr = body.accept(subst, null);
+    return typechecker.typecheck(substExpr, contextData.getExpectedType());
   }
 
   @Override