Calculate scope of VarTerms

src/main/java/edu/kit/typicalc/model/term/ScopingVisitor.java

@@ -0,0 +1,63 @@
+package edu.kit.typicalc.model.term;
+
+import java.util.HashMap;
+import java.util.Map;
+
+/**
+ * Visitor to add unique indices to variables of the same name.
+ *
+ * @see VarTerm#uniqueIndex()
+ */
+public class ScopingVisitor implements TermVisitor {
+    private int counter = 0;
+    private Map<String, Integer> index = new HashMap<>();
+
+    public ScopingVisitor() {
+
+    }
+
+    private ScopingVisitor(int counter, Map<String, Integer> index) {
+        this.counter = counter;
+        this.index = index;
+    }
+
+    @Override
+    public void visit(AppTerm appTerm) {
+        ScopingVisitor a = new ScopingVisitor(counter, new HashMap<>(index));
+        appTerm.getFunction().accept(a);
+        this.counter = a.counter;
+        appTerm.getParameter().accept(this);
+    }
+
+    @Override
+    public void visit(AbsTerm absTerm) {
+        VarTerm v = absTerm.getVariable();
+        v.setUniqueIndex(counter++);
+        index.put(v.getName(), v.uniqueIndex());
+        absTerm.getInner().accept(this);
+    }
+
+    @Override
+    public void visit(LetTerm letTerm) {
+        VarTerm v = letTerm.getVariable();
+        v.setUniqueIndex(counter++);
+        letTerm.getVariableDefinition().accept(this);
+        index.put(v.getName(), v.uniqueIndex());
+        letTerm.getInner().accept(this);
+    }
+
+    @Override
+    public void visit(VarTerm varTerm) {
+        if (index.containsKey(varTerm.getName())) {
+            varTerm.setUniqueIndex(index.get(varTerm.getName()));
+        } // else: unscoped variables share a single type variable
+    }
+
+    @Override
+    public void visit(IntegerTerm intTerm) {
+    }
+
+    @Override
+    public void visit(BooleanTerm boolTerm) {
+    }
+}

src/main/java/edu/kit/typicalc/model/term/VarTerm.java

@@ -11,6 +11,7 @@ import java.util.*;
  */
 public class VarTerm extends LambdaTerm {
     private final String name;
+    private int uniqueIndex = -1;
 
     /**
      * Initializes a new variable term with its name.
@@ -51,6 +52,18 @@ public class VarTerm extends LambdaTerm {
         return visitor.visit(this, assumptions, type);
     }
 
+    /**
+     * @see ScopingVisitor
+     * @return unique identifier of this VarTerm among VarTerms with the same name
+     */
+    public int uniqueIndex() {
+        return this.uniqueIndex;
+    }
+
+    public void setUniqueIndex(int index) {
+        this.uniqueIndex = index;
+    }
+
     @Override
     public String toString() {
         return name;

src/test/java/edu/kit/typicalc/model/term/ScopingVisitorTest.java

@@ -0,0 +1,64 @@
+package edu.kit.typicalc.model.term;
+
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+
+
+class ScopingVisitorTest {
+    @Test
+    void simple() {
+        AppTerm x = new AppTerm(
+                new AbsTerm(new VarTerm("x"), new VarTerm("x")),
+                new VarTerm("x")
+        ); // (λx.x)x
+
+        ScopingVisitor visitor = new ScopingVisitor();
+        x.accept(visitor);
+        assertEquals(0, ((AbsTerm) x.getFunction()).getVariable().uniqueIndex());
+        assertEquals(0, ((VarTerm) ((AbsTerm) x.getFunction()).getInner()).uniqueIndex());
+        assertEquals(-1, ((VarTerm) x.getParameter()).uniqueIndex());
+    }
+
+    @Test
+    void simpleNesting() {
+        AppTerm x = new AppTerm(
+                new AbsTerm(new VarTerm("x"),
+                        new AppTerm(new AbsTerm(new VarTerm("x"), new VarTerm("x")),
+                                new VarTerm("x"))),
+                new VarTerm("x")
+        ); // (λx.(λx.x)x)x
+
+        ScopingVisitor visitor = new ScopingVisitor();
+        x.accept(visitor);
+        assertEquals(0,
+                ((AbsTerm) x.getFunction()).getVariable().uniqueIndex());
+        assertEquals(1,
+                ((AbsTerm) ((AppTerm) ((AbsTerm) x.getFunction()).getInner()).getFunction()).getVariable().uniqueIndex());
+        assertEquals(1,
+                ((VarTerm) ((AbsTerm) ((AppTerm) ((AbsTerm) x.getFunction()).getInner()).getFunction()).getInner()).uniqueIndex());
+        assertEquals(0,
+                ((VarTerm) ((AppTerm) ((AbsTerm) x.getFunction()).getInner()).getParameter()).uniqueIndex());
+        assertEquals(-1, ((VarTerm) x.getParameter()).uniqueIndex());
+    }
+
+    @Test
+    void letTerm() {
+        // let x = λx.x in x 5
+        LetTerm x = new LetTerm(
+                new VarTerm("x"),
+                new AbsTerm(new VarTerm("x"), new VarTerm("x")),
+                new AppTerm(new VarTerm("x"), new IntegerTerm(5)));
+
+        ScopingVisitor visitor = new ScopingVisitor();
+        x.accept(visitor);
+        assertEquals(0,
+                x.getVariable().uniqueIndex());
+        assertEquals(1,
+                ((AbsTerm) x.getVariableDefinition()).getVariable().uniqueIndex());
+        assertEquals(1,
+                ((VarTerm) ((AbsTerm) x.getVariableDefinition()).getInner()).uniqueIndex());
+        assertEquals(0,
+                ((VarTerm) ((AppTerm) x.getInner()).getFunction()).uniqueIndex());
+    }
+}