Merge remote-tracking branch 'origin/master'

frontend/src/type-input-listener.ts

@@ -19,8 +19,8 @@ function modifyValue(area: HTMLInputElement) {
 	const value = parseBack(area.value);
 	const start = area.selectionStart;
 	const end = area.selectionEnd;
-	// ignore brackets, allow '>', spaces, ':', '.' or '∀' in front and '-', spaces, '.', ':' or ';' at the end of string
+	// ignore brackets, allow '>', spaces, ':', '.', ',' or '∀' in front and '-', spaces, '.', ':', ',' or ';' at the end of string
-	area.value = value.replace(/(^|\s+|\(|\)|>|∀|:|\.)t[0-9]+(?=\s+|\)|\(|-|:|\.|;|$)/ig, replacer);
+	area.value = value.replace(/(^|\s+|\(|\)|>|∀|:|,|\.)t[0-9]+(?=\s+|\)|\(|-|:|\.|;|,|$)/ig, replacer);
 	area.selectionStart = start;
 	area.selectionEnd = end;
 }

src/main/java/edu/kit/typicalc/model/ModelImpl.java

@@ -4,6 +4,7 @@ import edu.kit.typicalc.model.parser.LambdaParser;
 import edu.kit.typicalc.model.parser.ParseError;
 import edu.kit.typicalc.model.parser.TypeAssumptionParser;
 import edu.kit.typicalc.model.term.LambdaTerm;
+import edu.kit.typicalc.model.term.ScopingVisitor;
 import edu.kit.typicalc.model.term.VarTerm;
 import edu.kit.typicalc.model.type.TypeAbstraction;
 import edu.kit.typicalc.util.Result;
@@ -39,8 +40,10 @@ public class ModelImpl implements Model {
         if (assumptionMap.isError()) {
             return new Result<>(null, assumptionMap.unwrapError());
         }
-        //Create and return TypeInferer
+        // scope variables
-        TypeInferer typeInferer = new TypeInferer(result.unwrap(), assumptionMap.unwrap());
+        LambdaTerm term = result.unwrap();
+        term.accept(new ScopingVisitor());
+        TypeInferer typeInferer = new TypeInferer(term, assumptionMap.unwrap());
         return new Result<>(typeInferer, null);
     }
 }

src/main/java/edu/kit/typicalc/model/Tree.java

@@ -133,6 +133,7 @@ public class Tree implements TermVisitorTree {
         Map<VarTerm, TypeAbstraction> extendedTypeAssumptions = new LinkedHashMap<>(typeAssumptions);
         Type assType = typeVarFactory.nextTypeVariable();
         TypeAbstraction assAbs = new TypeAbstraction(assType);
+        extendedTypeAssumptions.remove(absTerm.getVariable());
         extendedTypeAssumptions.put(absTerm.getVariable(), assAbs);
 
         Type premiseType = typeVarFactory.nextTypeVariable();

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/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTerm.java

@@ -82,6 +82,8 @@ public class LatexCreatorTerm implements TermVisitor {
         if (mode == LatexCreatorMode.MATHJAX) {
             latex.append("\\class{typicalc-type typicalc-type-v-");
             latex.append(varTerm.hashCode());
+            latex.append("-");
+            latex.append(varTerm.uniqueIndex());
             latex.append("}{");
         }
         latex.append(MONO_TEXT);

src/main/resources/language/general.properties

@@ -23,10 +23,11 @@ root.termGrammar=\u2329Term\u232A ::= (\u2329Term\u232A) | \u2329App\u232A | \u2
 \u2329Const\u232A ::= [0-9]+ | true | false
 
 root.typeGrammar=\u2329Type\u232A ::= \u2329QuantifiedType\u232A | \u2329NormalType\u232A <br> \
-\u2329QuantifiedType\u232A ::= <b>∀</b>\u2329VarType\u232A<b>.</b>\u2329NormalType\u232A <br> \
+\u2329QuantifiedType\u232A ::= <b>∀</b>\u2329EnumVarType\u232A<b>.</b>\u2329NormalType\u232A <br> \
 \u2329NormalType\u232A ::= (\u2329NormalType\u232A) | \u2329NamedType\u232A | \u2329VarType\u232A | \
 \u2329FunctionType\u232A <br> \
 \u2329NamedType\u232A ::= [a-zA-Z][a-zA-Z0-9]*&nbsp;&nbsp\\t[0-9]+ <br> \
+\u2329EnumVarType\u232A ::= \u2329VarType\u232A <b>,</b> \u2329EnumVarType\u232A | \u2329VarType\u232A <br>\
 \u2329VarType\u232A ::= t[0-9]+ <br> \
 \u2329FunctionType\u232A ::= \u2329NormalType\u232A -> \u2329NormalType\u232A
 

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());
+    }
+}