arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-11-08 18:30:42 +00:00
Code Issues Packages Projects Releases Wiki Activity

Increase ID of let inferred type variables

Browse Source 
fixes #17
This commit is contained in:
Arne Keller 2021-07-26 10:06:19 +02:00
parent c6d80d9324
commit 19ec6cbc1a
2 changed files with 24 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/main/java/edu/kit/typicalc/model/Tree.java
View File

@ -181,8 +181,14 @@ public class Tree implements TermVisitorTree {
return new TypeAbstraction(newType, value.getQuantifiedVariables()); return new TypeAbstraction(newType, value.getQuantifiedVariables());
}); });
TypeAbstraction newTypeAbstraction = new TypeAbstraction( Type letType = typeInfererLet.getType().orElseThrow(IllegalStateException::new);
typeInfererLet.getType().orElseThrow(IllegalStateException::new), extendedTypeAssumptions); // increase ID of type variables to highlight them separately
for (TypeVariable t : letType.getFreeTypeVariables()) {
TypeVariable t2 = new TypeVariable(t.getKind(), t.getIndex());
t2.setUniqueIndex(t.getUniqueIndex() + 1);
letType = letType.substitute(t, t2);
}
TypeAbstraction newTypeAbstraction = new TypeAbstraction(letType, extendedTypeAssumptions);
extendedTypeAssumptions.remove(letTerm.getVariable()); extendedTypeAssumptions.remove(letTerm.getVariable());
extendedTypeAssumptions.put(letTerm.getVariable(), newTypeAbstraction); extendedTypeAssumptions.put(letTerm.getVariable(), newTypeAbstraction);

18
src/test/java/edu/kit/typicalc/model/TreeTest.java
View File

@ -1,5 +1,6 @@
package edu.kit.typicalc.model; package edu.kit.typicalc.model;
import edu.kit.typicalc.model.parser.LambdaParser;
import edu.kit.typicalc.model.step.*; import edu.kit.typicalc.model.step.*;
import edu.kit.typicalc.model.term.*; import edu.kit.typicalc.model.term.*;
import edu.kit.typicalc.model.type.*; import edu.kit.typicalc.model.type.*;
@ -10,8 +11,7 @@ import org.junit.jupiter.api.Test;
import java.util.*; import java.util.*;
import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.*;
import static org.junit.jupiter.api.Assertions.assertThrows;
class TreeTest { class TreeTest {
@ -171,6 +171,20 @@ class TreeTest {
assertEquals(constraints, tree.getConstraints()); assertEquals(constraints, tree.getConstraints());
} }
@Test
void derivedLetTypeHasNewUniqueIndex() {
var term = "let id = λx.x in id 5";
var tree = new Tree(new HashMap<>(), new LambdaParser(term).parse().unwrap());
var ls = (LetStep) tree.getFirstInferenceStep();
var as = (AbsStepWithLet) ls.getTypeInferer().getFirstInferenceStep();
var vs = (VarStep) as.getPremise();
var tv = (TypeVariable) vs.getInstantiatedTypeAbs();
var as2 = (AppStep) ls.getPremise();
var types = as2.getConclusion().getTypeAssumptions().get(new VarTerm("id")).getQuantifiedVariables().toArray(new TypeVariable[0]);
assertEquals(1, types.length);
assertNotEquals(tv.getUniqueIndex(), types[0].getUniqueIndex());
}
@Test @Test
void equalsTest() { void equalsTest() {
EqualsVerifier.forClass(Tree.class).usingGetClass() EqualsVerifier.forClass(Tree.class).usingGetClass()