From 99e1eef0bc38222ed7d343bd573c5c4c815afca8 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Fri, 2 Jul 2021 14:48:51 +0200 Subject: [PATCH] Calculate scope of VarTerms --- .../typicalc/model/term/ScopingVisitor.java | 63 ++++++++++++++++++ .../edu/kit/typicalc/model/term/VarTerm.java | 13 ++++ .../model/term/ScopingVisitorTest.java | 64 +++++++++++++++++++ 3 files changed, 140 insertions(+) create mode 100644 src/main/java/edu/kit/typicalc/model/term/ScopingVisitor.java create mode 100644 src/test/java/edu/kit/typicalc/model/term/ScopingVisitorTest.java diff --git a/src/main/java/edu/kit/typicalc/model/term/ScopingVisitor.java b/src/main/java/edu/kit/typicalc/model/term/ScopingVisitor.java new file mode 100644 index 0000000..a593d6d --- /dev/null +++ b/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 index = new HashMap<>(); + + public ScopingVisitor() { + + } + + private ScopingVisitor(int counter, Map 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) { + } +} diff --git a/src/main/java/edu/kit/typicalc/model/term/VarTerm.java b/src/main/java/edu/kit/typicalc/model/term/VarTerm.java index 8d1da7a..ef4e570 100644 --- a/src/main/java/edu/kit/typicalc/model/term/VarTerm.java +++ b/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; diff --git a/src/test/java/edu/kit/typicalc/model/term/ScopingVisitorTest.java b/src/test/java/edu/kit/typicalc/model/term/ScopingVisitorTest.java new file mode 100644 index 0000000..f91d49d --- /dev/null +++ b/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()); + } +}