From 23dc359d91ac4a90b65d3c4927b3cd928b63da3a Mon Sep 17 00:00:00 2001 From: Michael Williamson Date: Sat, 10 Jun 2023 14:37:28 +0100 Subject: Type check type level references --- .../ast/typed/TypedTypeLevelExpressionNode.java | 7 +++ .../ast/typed/TypedTypeLevelReferenceNode.java | 11 +++++ .../shedlang/compiler/typechecker/TypeChecker.java | 53 ++++++++++++++++++---- .../compiler/typechecker/typesets/TypeSet.java | 2 +- .../typesets/TypeSetTypeLevelValue.java | 13 ++++++ .../compiler/typechecker/typesets/TypeSets.java | 1 + .../java/org/shedlang/compiler/types/Type.java | 4 +- .../shedlang/compiler/types/TypeLevelValue.java | 5 ++ .../compiler/types/TypeLevelValueType.java | 8 ++++ .../java/org/shedlang/compiler/types/Types.java | 4 ++ 10 files changed, 96 insertions(+), 12 deletions(-) create mode 100644 src/main/java/org/shedlang/compiler/ast/typed/TypedTypeLevelExpressionNode.java create mode 100644 src/main/java/org/shedlang/compiler/ast/typed/TypedTypeLevelReferenceNode.java create mode 100644 src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSetTypeLevelValue.java create mode 100644 src/main/java/org/shedlang/compiler/types/TypeLevelValue.java create mode 100644 src/main/java/org/shedlang/compiler/types/TypeLevelValueType.java (limited to 'src/main/java') diff --git a/src/main/java/org/shedlang/compiler/ast/typed/TypedTypeLevelExpressionNode.java b/src/main/java/org/shedlang/compiler/ast/typed/TypedTypeLevelExpressionNode.java new file mode 100644 index 00000000..4b10483d --- /dev/null +++ b/src/main/java/org/shedlang/compiler/ast/typed/TypedTypeLevelExpressionNode.java @@ -0,0 +1,7 @@ +package org.shedlang.compiler.ast.typed; + +import org.shedlang.compiler.types.TypeLevelValue; + +public interface TypedTypeLevelExpressionNode extends TypedNode { + TypeLevelValue value(); +} diff --git a/src/main/java/org/shedlang/compiler/ast/typed/TypedTypeLevelReferenceNode.java b/src/main/java/org/shedlang/compiler/ast/typed/TypedTypeLevelReferenceNode.java new file mode 100644 index 00000000..009d0b8b --- /dev/null +++ b/src/main/java/org/shedlang/compiler/ast/typed/TypedTypeLevelReferenceNode.java @@ -0,0 +1,11 @@ +package org.shedlang.compiler.ast.typed; + +import org.shedlang.compiler.sources.Source; +import org.shedlang.compiler.types.TypeLevelValue; + +public record TypedTypeLevelReferenceNode( + String name, + TypeLevelValue value, + Source source +) implements TypedTypeLevelExpressionNode { +} diff --git a/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java b/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java index f707dac0..f2af9769 100644 --- a/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java +++ b/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java @@ -2,10 +2,12 @@ package org.shedlang.compiler.typechecker; import org.shedlang.compiler.ast.typed.*; import org.shedlang.compiler.ast.untyped.*; +import org.shedlang.compiler.sources.Source; import org.shedlang.compiler.typechecker.errors.*; import org.shedlang.compiler.typechecker.typesets.TypeSets; import org.shedlang.compiler.types.FunctionType; import org.shedlang.compiler.types.Type; +import org.shedlang.compiler.types.TypeLevelValueType; import java.util.HashSet; @@ -27,6 +29,16 @@ public class TypeChecker { return subType.equals(superType); } + private static Type lookupVariable(String name, Source source, TypeCheckerContext context) { + var type = context.environment(name); + + if (type.isEmpty()) { + throw new UnknownVariableError(name, source); + } + + return type.get(); + } + private static TypedArgsNode typeCheckArgs( UntypedArgsNode args, TypeCheckerContext context, @@ -171,25 +183,48 @@ public class TypeChecker { UntypedReferenceNode untyped, TypeCheckerContext context ) { - var type = context.environment(untyped.name()); - - if (type.isEmpty()) { - throw new UnknownVariableError(untyped.name(), untyped.source()); - } + var type = lookupVariable(untyped.name(), untyped.source(), context); return new TypedReferenceNode( untyped.name(), - type.get(), + type, untyped.source() ); } private static TypedStringLiteralNode typeCheckStringLiteral( - UntypedStringLiteralNode untype + UntypedStringLiteralNode untyped ) { return new TypedStringLiteralNode( - untype.value(), - untype.source() + untyped.value(), + untyped.source() + ); + } + + static TypedTypeLevelExpressionNode typeCheckTypeLevelExpression( + UntypedTypeLevelExpressionNode untyped, + TypeCheckerContext context + ) { + return switch (untyped) { + case UntypedTypeLevelReferenceNode reference -> + typeCheckTypeLevelReference(reference, context); + }; + } + + private static TypedTypeLevelExpressionNode typeCheckTypeLevelReference( + UntypedTypeLevelReferenceNode untyped, + TypeCheckerContext context + ) { + var type = lookupVariable(untyped.name(), untyped.source(), context); + + if (!(type instanceof TypeLevelValueType typeLevelValueType)) { + throw new UnexpectedTypeError(TypeSets.TYPE_LEVEL_VALUE, type, untyped.source()); + } + + return new TypedTypeLevelReferenceNode( + untyped.name(), + typeLevelValueType.value(), + untyped.source() ); } } diff --git a/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSet.java b/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSet.java index 79cb0433..01899978 100644 --- a/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSet.java +++ b/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSet.java @@ -1,5 +1,5 @@ package org.shedlang.compiler.typechecker.typesets; -public sealed interface TypeSet permits TypeSetFunction, TypeSetType { +public sealed interface TypeSet permits TypeSetFunction, TypeSetType, TypeSetTypeLevelValue { String describe(); } diff --git a/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSetTypeLevelValue.java b/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSetTypeLevelValue.java new file mode 100644 index 00000000..791ec37a --- /dev/null +++ b/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSetTypeLevelValue.java @@ -0,0 +1,13 @@ +package org.shedlang.compiler.typechecker.typesets; + +public final class TypeSetTypeLevelValue implements TypeSet { + private TypeSetTypeLevelValue() { + } + + static final TypeSetTypeLevelValue INSTANCE = new TypeSetTypeLevelValue(); + + @Override + public String describe() { + return "type-level value"; + } +} diff --git a/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSets.java b/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSets.java index b783a5ef..6bb13f7a 100644 --- a/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSets.java +++ b/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSets.java @@ -7,6 +7,7 @@ public class TypeSets { } public static final TypeSet FUNCTION = TypeSetFunction.INSTANCE; + public static final TypeSet TYPE_LEVEL_VALUE = TypeSetTypeLevelValue.INSTANCE; public static TypeSet type(Type type) { return new TypeSetType(type); diff --git a/src/main/java/org/shedlang/compiler/types/Type.java b/src/main/java/org/shedlang/compiler/types/Type.java index 5077776c..fdefb86f 100644 --- a/src/main/java/org/shedlang/compiler/types/Type.java +++ b/src/main/java/org/shedlang/compiler/types/Type.java @@ -1,5 +1,5 @@ package org.shedlang.compiler.types; -public sealed interface Type permits BoolType, FunctionType, IntType, StringType, UnitType { - String describe(); +public sealed interface Type extends TypeLevelValue + permits BoolType, FunctionType, IntType, StringType, TypeLevelValueType, UnitType { } diff --git a/src/main/java/org/shedlang/compiler/types/TypeLevelValue.java b/src/main/java/org/shedlang/compiler/types/TypeLevelValue.java new file mode 100644 index 00000000..3eaddb7f --- /dev/null +++ b/src/main/java/org/shedlang/compiler/types/TypeLevelValue.java @@ -0,0 +1,5 @@ +package org.shedlang.compiler.types; + +public sealed interface TypeLevelValue permits Type { + String describe(); +} diff --git a/src/main/java/org/shedlang/compiler/types/TypeLevelValueType.java b/src/main/java/org/shedlang/compiler/types/TypeLevelValueType.java new file mode 100644 index 00000000..ee47af68 --- /dev/null +++ b/src/main/java/org/shedlang/compiler/types/TypeLevelValueType.java @@ -0,0 +1,8 @@ +package org.shedlang.compiler.types; + +public record TypeLevelValueType(TypeLevelValue value) implements Type { + @Override + public String describe() { + return "TypeLevelValue[" + value.describe() + "]"; + } +} diff --git a/src/main/java/org/shedlang/compiler/types/Types.java b/src/main/java/org/shedlang/compiler/types/Types.java index 9655d2bb..cb734272 100644 --- a/src/main/java/org/shedlang/compiler/types/Types.java +++ b/src/main/java/org/shedlang/compiler/types/Types.java @@ -8,4 +8,8 @@ public class Types { public static final Type INT = IntType.INSTANCE; public static final Type STRING = StringType.INSTANCE; public static final Type UNIT = UnitType.INSTANCE; + + public static Type metaType(Type type) { + return new TypeLevelValueType(type); + } } -- cgit v1.2.3