From f928b2bae39a65f50c29b27f75f54a7115814ccc Mon Sep 17 00:00:00 2001 From: Moritz Dieing <63721811+moritzdieing@users.noreply.github.com> Date: Fri, 2 Jul 2021 14:47:25 +0200 Subject: [PATCH 1/4] Optimise type assumption syntax --- frontend/src/type-input-listener.ts | 4 ++-- src/main/resources/language/general.properties | 3 ++- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/frontend/src/type-input-listener.ts b/frontend/src/type-input-listener.ts index 13001ec..b83b083 100644 --- a/frontend/src/type-input-listener.ts +++ b/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 - area.value = value.replace(/(^|\s+|\(|\)|>|∀|:|\.)t[0-9]+(?=\s+|\)|\(|-|:|\.|;|$)/ig, replacer); + // 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.selectionStart = start; area.selectionEnd = end; } diff --git a/src/main/resources/language/general.properties b/src/main/resources/language/general.properties index 35cfc6b..c829e3c 100644 --- a/src/main/resources/language/general.properties +++ b/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
\ -\u2329QuantifiedType\u232A ::= ∀\u2329VarType\u232A.\u2329NormalType\u232A
\ +\u2329QuantifiedType\u232A ::= ∀\u2329EnumVarType\u232A.\u2329NormalType\u232A
\ \u2329NormalType\u232A ::= (\u2329NormalType\u232A) | \u2329NamedType\u232A | \u2329VarType\u232A | \ \u2329FunctionType\u232A
\ \u2329NamedType\u232A ::= [a-zA-Z][a-zA-Z0-9]*  \\t[0-9]+
\ +\u2329EnumVarType\u232A ::= \u2329VarType\u232A , \u2329EnumVarType\u232A | \u2329VarType\u232A
\ \u2329VarType\u232A ::= t[0-9]+
\ \u2329FunctionType\u232A ::= \u2329NormalType\u232A -> \u2329NormalType\u232A From 99e1eef0bc38222ed7d343bd573c5c4c815afca8 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Fri, 2 Jul 2021 14:48:51 +0200 Subject: [PATCH 2/4] 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()); + } +} From 480275e3a7cff6a19dfef2d5fa014641da89a734 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Fri, 2 Jul 2021 14:57:25 +0200 Subject: [PATCH 3/4] Semantic highlighting of variables --- src/main/java/edu/kit/typicalc/model/ModelImpl.java | 7 +++++-- .../latexcreator/LatexCreatorTerm.java | 2 ++ 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/src/main/java/edu/kit/typicalc/model/ModelImpl.java b/src/main/java/edu/kit/typicalc/model/ModelImpl.java index a1fbd28..d2472a7 100644 --- a/src/main/java/edu/kit/typicalc/model/ModelImpl.java +++ b/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 - TypeInferer typeInferer = new TypeInferer(result.unwrap(), assumptionMap.unwrap()); + // scope variables + LambdaTerm term = result.unwrap(); + term.accept(new ScopingVisitor()); + TypeInferer typeInferer = new TypeInferer(term, assumptionMap.unwrap()); return new Result<>(typeInferer, null); } } diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTerm.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTerm.java index b943d54..4d2f684 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTerm.java +++ b/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); From 116aea51c387caaa0eb989da5179c6f512ac0f32 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Fri, 2 Jul 2021 15:13:10 +0200 Subject: [PATCH 4/4] Replace variables in MGU properly --- src/main/java/edu/kit/typicalc/model/Tree.java | 1 + 1 file changed, 1 insertion(+) diff --git a/src/main/java/edu/kit/typicalc/model/Tree.java b/src/main/java/edu/kit/typicalc/model/Tree.java index 894dd5d..939357e 100644 --- a/src/main/java/edu/kit/typicalc/model/Tree.java +++ b/src/main/java/edu/kit/typicalc/model/Tree.java @@ -133,6 +133,7 @@ public class Tree implements TermVisitorTree { Map 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();