From 2bc60a8737e326a6763afe786027bd3ab2389f44 Mon Sep 17 00:00:00 2001 From: Michael Williamson Date: Sat, 2 Mar 2024 15:22:07 +0000 Subject: Include effect params in constraint solving --- .../typechecker/TypeCheckerIsSubTypeTests.java | 166 +++++++++++++++++++-- 1 file changed, 157 insertions(+), 9 deletions(-) (limited to 'src/test/java') diff --git a/src/test/java/org/shedlang/compiler/typechecker/TypeCheckerIsSubTypeTests.java b/src/test/java/org/shedlang/compiler/typechecker/TypeCheckerIsSubTypeTests.java index 7821c68e..a1928bf8 100644 --- a/src/test/java/org/shedlang/compiler/typechecker/TypeCheckerIsSubTypeTests.java +++ b/src/test/java/org/shedlang/compiler/typechecker/TypeCheckerIsSubTypeTests.java @@ -2,6 +2,7 @@ package org.shedlang.compiler.typechecker; import org.junit.jupiter.api.Test; import org.shedlang.compiler.sources.Sources; +import org.shedlang.compiler.typechecker.errors.UnexpectedEffectError; import org.shedlang.compiler.typechecker.errors.UnexpectedTypeError; import org.shedlang.compiler.typechecker.typesets.TypeSets; import org.shedlang.compiler.types.*; @@ -11,12 +12,123 @@ import java.util.List; import java.util.Map; import static org.junit.jupiter.api.Assertions.assertThrows; +import static org.shedlang.compiler.typechecker.TypeCheckerSubTyping.isSubEffect; import static org.shedlang.compiler.typechecker.TypeCheckerSubTyping.isSubType; import static org.zwobble.precisely.AssertThat.assertThat; import static org.zwobble.precisely.Matchers.*; public class TypeCheckerIsSubTypeTests { - // == General == + // == General effects == + + @Test + public void effectsAreSubeffectsOfThemselves() { + var namespaceName = NamespaceName.of("Example", "Project"); + var typeInfos = TypeInfos.EMPTY; + + assertThat(isSubEffect(Effects.IO, Effects.IO, typeInfos), equalTo(true)); + assertThat( + isSubEffect( + new UserDefinedEffect(namespaceName, "E"), + new UserDefinedEffect(namespaceName, "E"), + typeInfos + ), + equalTo(true) + ); + } + + @Test + public void unrelatedEffectsAreNotSubeffects() { + var namespaceName = NamespaceName.of("Example", "Project"); + var typeInfos = TypeInfos.EMPTY; + + assertThat( + isSubEffect( + new UserDefinedEffect(namespaceName, "E1"), + new UserDefinedEffect(namespaceName, "E2"), + typeInfos + ), + equalTo(false) + ); + } + + // == None effect == + + @Test + public void noneEffectIsSubEffectOfAllEffects() { + var namespaceName = NamespaceName.of("Example", "Project"); + var typeInfos = TypeInfos.EMPTY; + + assertThat(isSubEffect(Effects.NONE, Effects.IO, typeInfos), equalTo(true)); + assertThat( + isSubEffect( + Effects.NONE, + new UserDefinedEffect(namespaceName, "E"), + typeInfos + ), + equalTo(true) + ); + } + + @Test + public void noneEffectIsSupereffectOfNoOtherEffects() { + var namespaceName = NamespaceName.of("Example", "Project"); + var typeInfos = TypeInfos.EMPTY; + + assertThat(isSubEffect(Effects.IO, Effects.NONE, typeInfos), equalTo(false)); + assertThat( + isSubEffect( + new UserDefinedEffect(namespaceName, "E"), + Effects.NONE, + typeInfos + ), + equalTo(false) + ); + } + + // == Effect params == + + @Test + public void whenSupereffectIsEffectArgThenEffectArgIsConstrained() { + var effectParam = EffectParam.forStructType( + Types.struct(NamespaceName.of("Example"), "Struct"), + "E" + ); + var effectArg = new EffectArg(effectParam); + + var constraints = TypeCheckerSubTyping.addSubeffectConstraint( + Effects.IO, + effectArg, + Sources.NULL, + TypeCheckerSubTyping.constraints(List.of(effectArg), TypeInfos.EMPTY) + ); + + assertThat(constraints.effectBounds().get(effectArg), isSequence( + equalTo(Effects.IO) + )); + } + + @Test + public void whenSupereffectIsFreeEffectParamThenOtherEffectsAreNotSubtype() { + var effectParam = EffectParam.forStructType( + Types.struct(NamespaceName.of("Example"), "Struct"), + "E" + ); + + var error = assertThrows( + UnexpectedEffectError.class, + () -> TypeCheckerSubTyping.addSubeffectConstraint( + Effects.IO, + effectParam, + Sources.NULL, + TypeCheckerSubTyping.constraints(List.of(), TypeInfos.EMPTY) + ) + ); + + assertThat(error.allowed(), equalTo(effectParam)); + assertThat(error.actual(), equalTo(Effects.IO)); + } + + // == General types == @Test public void typesAreSubTypesOfThemselves() { @@ -585,6 +697,42 @@ public class TypeCheckerIsSubTypeTests { // == Constraint solving == + @Test + public void whenEffectParamHasNoBoundThenEffectParamIsResolvedToNoneEffect() { + var effectParam = EffectParam.forStructType( + Types.struct(NamespaceName.of("Example"), "Struct"), + "E" + ); + var effectArg = new EffectArg(effectParam); + + var constraints = TypeCheckerSubTyping.constraints(List.of(effectArg), TypeInfos.EMPTY); + var result = constraints.solve(Sources.NULL); + + assertThat(result, equalTo(TypeSubstitutionMap.of( + Map.entry(effectParam, Effects.NONE) + ))); + } + + @Test + public void whenEffectParamHasLowerBoundsThenEffectParamIsResolvedToUnionOfBounds() { + var effect1 = new UserDefinedEffect(NamespaceName.of("Example"), "E1"); + var effect2 = new UserDefinedEffect(NamespaceName.of("Example"), "E2"); + var effectParam = EffectParam.forStructType( + Types.struct(NamespaceName.of("Example"), "Struct"), + "E" + ); + var effectArg = new EffectArg(effectParam); + + var constraints = TypeCheckerSubTyping.constraints(List.of(effectArg), TypeInfos.EMPTY) + .addLowerEffectBound(effectArg, effect1) + .addLowerEffectBound(effectArg, effect2); + var result = constraints.solve(Sources.NULL); + + assertThat(result, equalTo(TypeSubstitutionMap.of( + Map.entry(effectParam, Effects.union(effect1, effect2)) + ))); + } + @Test public void whenTypeParamHasUpperBoundThenTypeParamIsResolvedToUpperBound() { var typeParam = TypeParam.forStructType( @@ -594,7 +742,7 @@ public class TypeCheckerIsSubTypeTests { var typeArg = new TypeArg(typeParam); var constraints = TypeCheckerSubTyping.constraints(List.of(typeArg), TypeInfos.EMPTY) - .addUpperBound(typeArg, Types.INT); + .addUpperTypeBound(typeArg, Types.INT); var result = constraints.solve(Sources.NULL); assertThat(result, equalTo(TypeSubstitutionMap.of( @@ -611,7 +759,7 @@ public class TypeCheckerIsSubTypeTests { var typeArg = new TypeArg(typeParam); var constraints = TypeCheckerSubTyping.constraints(List.of(typeArg), TypeInfos.EMPTY) - .addLowerBound(typeArg, Types.INT); + .addLowerTypeBound(typeArg, Types.INT); var result = constraints.solve(Sources.NULL); assertThat(result, equalTo(TypeSubstitutionMap.of( @@ -628,8 +776,8 @@ public class TypeCheckerIsSubTypeTests { var typeArg = new TypeArg(typeParam); var constraints = TypeCheckerSubTyping.constraints(List.of(typeArg), TypeInfos.EMPTY) - .addLowerBound(typeArg, Types.INT) - .addLowerBound(typeArg, Types.STRING); + .addLowerTypeBound(typeArg, Types.INT) + .addLowerTypeBound(typeArg, Types.STRING); var result = constraints.solve(Sources.NULL); assertThat(result, equalTo(TypeSubstitutionMap.of( @@ -655,8 +803,8 @@ public class TypeCheckerIsSubTypeTests { ))); var constraints = TypeCheckerSubTyping.constraints(List.of(typeArg), typeInfos) - .addLowerBound(typeArg, variantType1) - .addUpperBound(typeArg, sumType); + .addLowerTypeBound(typeArg, variantType1) + .addUpperTypeBound(typeArg, sumType); var result = constraints.solve(Sources.NULL); assertThat(result, equalTo(TypeSubstitutionMap.of( @@ -682,8 +830,8 @@ public class TypeCheckerIsSubTypeTests { ))); var constraints = TypeCheckerSubTyping.constraints(List.of(typeArg), typeInfos) - .addLowerBound(typeArg, sumType) - .addUpperBound(typeArg, variantType1); + .addLowerTypeBound(typeArg, sumType) + .addUpperTypeBound(typeArg, variantType1); var error = assertThrows( // TODO: more specific error IllegalStateException.class, -- cgit v1.2.3