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);