From 2b8f19b0c9e85cb9d8b9efb8bff713834b537590 Mon Sep 17 00:00:00 2001 From: Stephen Paul Weber Date: Tue, 19 Mar 2019 21:26:08 -0500 Subject: [PATCH] Working typechecker --- lib/dhall/ast.rb | 112 ++- lib/dhall/binary.rb | 6 +- lib/dhall/builtins.rb | 4 +- lib/dhall/normalize.rb | 27 +- lib/dhall/typecheck.rb | 662 +++++++++++++++++- test/test_typechecker.rb | 5 +- ...FunctionApplicationArgumentNotMatch.dhallb | Bin 0 -> 14 bytes .../FunctionApplicationIsNotFunction.dhallb | Bin 0 -> 4 bytes .../FunctionArgumentTypeNotAType.dhallb | Bin 0 -> 6 bytes .../failure/FunctionDependentType.dhallb | 1 + .../failure/FunctionDependentType2.dhallb | 1 + .../FunctionTypeArgumentTypeNotAType.dhallb | Bin 0 -> 6 bytes .../failure/FunctionTypeKindSort.dhallb | 1 + .../failure/FunctionTypeTypeKind.dhallb | 1 + .../failure/FunctionTypeTypeSort.dhallb | 1 + .../failure/LetWithWrongAnnotation.dhallb | 1 + .../MergeAlternativeHasNoHandler.dhallb | 1 + .../failure/MergeAnnotationNotType.dhallb | 1 + .../MergeEmptyWithoutAnnotation.dhallb | 1 + .../failure/MergeHandlerNotFunction.dhallb | 1 + .../failure/MergeHandlerNotInUnion.dhallb | Bin 0 -> 23 bytes ...MergeHandlerNotMatchAlternativeType.dhallb | Bin 0 -> 23 bytes .../MergeHandlersWithDifferentType.dhallb | Bin 0 -> 34 bytes .../failure/MergeLhsNotRecord.dhallb | 1 + .../failure/MergeRhsNotUnion.dhallb | 1 + .../failure/MergeWithWrongAnnotation.dhallb | Bin 0 -> 29 bytes .../failure/RecordMixedKinds.dhallb | 1 + .../failure/RecordMixedKinds2.dhallb | 1 + .../failure/RecordMixedKinds3.dhallb | 1 + .../failure/RecordProjectionEmpty.dhallb | 2 + .../failure/RecordProjectionNotPresent.dhallb | 2 + .../failure/RecordProjectionNotRecord.dhallb | 2 + .../failure/RecordSelectionEmpty.dhallb | 1 + .../failure/RecordSelectionNotPresent.dhallb | 1 + .../failure/RecordSelectionNotRecord.dhallb | 1 + .../failure/RecordTypeMixedKinds.dhallb | 1 + .../failure/RecordTypeMixedKinds2.dhallb | 1 + .../failure/RecordTypeMixedKinds3.dhallb | 1 + .../failure/RecordTypeValueMember.dhallb | 1 + .../RecursiveRecordMergeLhsNotRecord.dhallb | 1 + .../RecursiveRecordMergeMixedKinds.dhallb | 1 + .../RecursiveRecordMergeOverlapping.dhallb | 1 + .../RecursiveRecordMergeRhsNotRecord.dhallb | 1 + ...siveRecordTypeMergeLhsNotRecordType.dhallb | 2 + ...RecursiveRecordTypeMergeOverlapping.dhallb | 2 + ...siveRecordTypeMergeRhsNotRecordType.dhallb | 2 + .../RightBiasedRecordMergeLhsNotRecord.dhallb | 1 + .../RightBiasedRecordMergeMixedKinds.dhallb | 1 + .../RightBiasedRecordMergeMixedKinds2.dhallb | 1 + .../RightBiasedRecordMergeMixedKinds3.dhallb | 1 + .../RightBiasedRecordMergeRhsNotRecord.dhallb | 1 + test/typechecker/failure/SomeNotType.dhallb | 1 + .../failure/TypeAnnotationWrong.dhallb | 1 + .../UnionConstructorFieldNotPresent.dhallb | 1 + .../failure/UnionTypeMixedKinds.dhallb | 1 + .../failure/UnionTypeMixedKinds2.dhallb | 1 + .../failure/UnionTypeMixedKinds3.dhallb | 1 + .../failure/UnionTypeNotType.dhallb | 1 + test/typechecker/gen | 10 + test/typechecker/success/DoubleA.dhallb | 1 + test/typechecker/success/DoubleB.dhallb | 1 + .../typechecker/success/DoubleLiteralA.dhallb | Bin 0 -> 5 bytes .../typechecker/success/DoubleLiteralB.dhallb | 1 + test/typechecker/success/DoubleShowA.dhallb | 1 + test/typechecker/success/DoubleShowB.dhallb | 1 + test/typechecker/success/FunctionA.dhallb | Bin 0 -> 8 bytes .../success/FunctionApplicationA.dhallb | Bin 0 -> 11 bytes .../success/FunctionApplicationB.dhallb | 1 + test/typechecker/success/FunctionB.dhallb | 1 + .../success/FunctionNamedArgA.dhallb | 1 + .../success/FunctionNamedArgB.dhallb | 1 + .../success/FunctionTypeKindKindA.dhallb | 1 + .../success/FunctionTypeKindKindB.dhallb | 1 + .../success/FunctionTypeKindTermA.dhallb | 1 + .../success/FunctionTypeKindTermB.dhallb | 1 + .../success/FunctionTypeKindTypeA.dhallb | 1 + .../success/FunctionTypeKindTypeB.dhallb | 1 + .../success/FunctionTypeTermTermA.dhallb | 1 + .../success/FunctionTypeTermTermB.dhallb | 1 + .../success/FunctionTypeTypeTermA.dhallb | 1 + .../success/FunctionTypeTypeTermB.dhallb | 1 + .../success/FunctionTypeTypeTypeA.dhallb | 1 + .../success/FunctionTypeTypeTypeB.dhallb | 1 + .../success/FunctionTypeUsingArgumentA.dhallb | Bin 0 -> 8 bytes .../success/FunctionTypeUsingArgumentB.dhallb | 1 + test/typechecker/success/IntegerA.dhallb | 1 + test/typechecker/success/IntegerB.dhallb | 1 + .../success/IntegerLiteralA.dhallb | 1 + .../success/IntegerLiteralB.dhallb | 1 + test/typechecker/success/IntegerShowA.dhallb | 1 + test/typechecker/success/IntegerShowB.dhallb | 1 + .../success/IntegerToDoubleA.dhallb | 1 + .../success/IntegerToDoubleB.dhallb | 1 + test/typechecker/success/LetA.dhallb | 1 + test/typechecker/success/LetB.dhallb | 1 + .../success/LetNestedTypeSynonymA.dhallb | 1 + .../success/LetNestedTypeSynonymB.dhallb | 1 + .../success/LetTypeSynonymA.dhallb | 1 + .../success/LetTypeSynonymB.dhallb | 1 + .../success/LetWithAnnotationA.dhallb | 1 + .../success/LetWithAnnotationB.dhallb | 1 + .../success/MergeEmptyUnionA.dhallb | 1 + .../success/MergeEmptyUnionB.dhallb | 1 + test/typechecker/success/MergeOneA.dhallb | Bin 0 -> 21 bytes test/typechecker/success/MergeOneB.dhallb | 1 + .../success/MergeOneWithAnnotationA.dhallb | Bin 0 -> 26 bytes .../success/MergeOneWithAnnotationB.dhallb | 1 + test/typechecker/success/NoneA.dhallb | 1 + test/typechecker/success/NoneB.dhallb | Bin 0 -> 22 bytes .../success/OldOptionalNoneA.dhallb | 1 + .../success/OldOptionalNoneB.dhallb | Bin 0 -> 16 bytes .../success/OldOptionalTrueA.dhallb | 1 + .../success/OldOptionalTrueB.dhallb | Bin 0 -> 16 bytes test/typechecker/success/OptionalA.dhallb | 1 + test/typechecker/success/OptionalB.dhallb | 1 + .../typechecker/success/OptionalBuildA.dhallb | 1 + .../typechecker/success/OptionalBuildB.dhallb | Bin 0 -> 88 bytes test/typechecker/success/OptionalFoldA.dhallb | 1 + test/typechecker/success/OptionalFoldB.dhallb | Bin 0 -> 88 bytes test/typechecker/success/RecordEmptyA.dhallb | 1 + test/typechecker/success/RecordEmptyB.dhallb | 1 + .../typechecker/success/RecordOneKindA.dhallb | 1 + .../typechecker/success/RecordOneKindB.dhallb | 1 + .../typechecker/success/RecordOneTypeA.dhallb | 1 + .../typechecker/success/RecordOneTypeB.dhallb | 1 + .../success/RecordOneValueA.dhallb | 1 + .../success/RecordOneValueB.dhallb | 1 + .../success/RecordProjectionEmptyA.dhallb | 2 + .../success/RecordProjectionEmptyB.dhallb | 1 + .../success/RecordProjectionKindA.dhallb | 2 + .../success/RecordProjectionKindB.dhallb | 1 + .../success/RecordProjectionTypeA.dhallb | 2 + .../success/RecordProjectionTypeB.dhallb | 1 + .../success/RecordProjectionValueA.dhallb | 2 + .../success/RecordProjectionValueB.dhallb | 1 + .../success/RecordSelectionKindA.dhallb | 1 + .../success/RecordSelectionKindB.dhallb | 1 + .../success/RecordSelectionTypeA.dhallb | 1 + .../success/RecordSelectionTypeB.dhallb | 1 + .../success/RecordSelectionValueA.dhallb | 1 + .../success/RecordSelectionValueB.dhallb | 1 + test/typechecker/success/RecordTypeA.dhallb | 1 + test/typechecker/success/RecordTypeB.dhallb | 1 + .../success/RecordTypeEmptyA.dhallb | 1 + .../success/RecordTypeEmptyB.dhallb | 1 + .../success/RecordTypeKindA.dhallb | 1 + .../success/RecordTypeKindB.dhallb | 1 + .../success/RecordTypeTypeA.dhallb | 1 + .../success/RecordTypeTypeB.dhallb | 1 + .../RecursiveRecordMergeLhsEmptyA.dhallb | 1 + .../RecursiveRecordMergeLhsEmptyB.dhallb | 1 + .../RecursiveRecordMergeRecursivelyA.dhallb | 1 + .../RecursiveRecordMergeRecursivelyB.dhallb | 1 + ...cursiveRecordMergeRecursivelyKindsA.dhallb | 1 + ...cursiveRecordMergeRecursivelyKindsB.dhallb | 1 + ...cursiveRecordMergeRecursivelyTypesA.dhallb | 1 + ...cursiveRecordMergeRecursivelyTypesB.dhallb | 1 + .../RecursiveRecordMergeRhsEmptyA.dhallb | 1 + .../RecursiveRecordMergeRhsEmptyB.dhallb | 1 + .../success/RecursiveRecordMergeTwoA.dhallb | 1 + .../success/RecursiveRecordMergeTwoB.dhallb | 1 + .../RecursiveRecordMergeTwoKindsA.dhallb | 1 + .../RecursiveRecordMergeTwoKindsB.dhallb | 1 + .../RecursiveRecordMergeTwoTypesA.dhallb | 1 + .../RecursiveRecordMergeTwoTypesB.dhallb | 1 + ...ecursiveRecordTypeMergeRecursivelyA.dhallb | 2 + ...ecursiveRecordTypeMergeRecursivelyB.dhallb | 1 + ...iveRecordTypeMergeRecursivelyKindsA.dhallb | 2 + ...iveRecordTypeMergeRecursivelyKindsB.dhallb | 1 + ...iveRecordTypeMergeRecursivelyTypesA.dhallb | 2 + ...iveRecordTypeMergeRecursivelyTypesB.dhallb | 1 + .../RecursiveRecordTypeMergeRhsEmptyA.dhallb | 2 + .../RecursiveRecordTypeMergeRhsEmptyB.dhallb | 1 + .../RecursiveRecordTypeMergeTwoA.dhallb | 2 + .../RecursiveRecordTypeMergeTwoB.dhallb | 1 + .../RecursiveRecordTypeMergeTwoKindsA.dhallb | 2 + .../RecursiveRecordTypeMergeTwoKindsB.dhallb | 1 + .../RecursiveRecordTypeMergeTwoTypesA.dhallb | 2 + .../RecursiveRecordTypeMergeTwoTypesB.dhallb | 1 + .../RightBiasedRecordMergeRhsEmptyA.dhallb | 1 + .../RightBiasedRecordMergeRhsEmptyB.dhallb | 1 + .../success/RightBiasedRecordMergeTwoA.dhallb | 1 + .../success/RightBiasedRecordMergeTwoB.dhallb | 1 + ...RightBiasedRecordMergeTwoDifferentA.dhallb | 1 + ...RightBiasedRecordMergeTwoDifferentB.dhallb | 1 + .../RightBiasedRecordMergeTwoKindsA.dhallb | 1 + .../RightBiasedRecordMergeTwoKindsB.dhallb | 1 + .../RightBiasedRecordMergeTwoTypesA.dhallb | 1 + .../RightBiasedRecordMergeTwoTypesB.dhallb | 1 + test/typechecker/success/SomeTrueA.dhallb | 1 + test/typechecker/success/SomeTrueB.dhallb | Bin 0 -> 16 bytes .../success/TypeAnnotationA.dhallb | 1 + .../success/TypeAnnotationB.dhallb | 1 + .../success/UnionConstructorFieldA.dhallb | 1 + .../success/UnionConstructorFieldB.dhallb | 1 + test/typechecker/success/UnionOneA.dhallb | 1 + test/typechecker/success/UnionOneB.dhallb | 1 + .../success/UnionTypeEmptyA.dhallb | 1 + .../success/UnionTypeEmptyB.dhallb | 1 + .../typechecker/success/UnionTypeKindA.dhallb | 1 + .../typechecker/success/UnionTypeKindB.dhallb | 1 + test/typechecker/success/UnionTypeOneA.dhallb | 1 + test/typechecker/success/UnionTypeOneB.dhallb | 1 + .../typechecker/success/UnionTypeTypeA.dhallb | 1 + .../typechecker/success/UnionTypeTypeB.dhallb | 1 + 205 files changed, 976 insertions(+), 45 deletions(-) create mode 100644 test/typechecker/failure/FunctionApplicationArgumentNotMatch.dhallb create mode 100644 test/typechecker/failure/FunctionApplicationIsNotFunction.dhallb create mode 100644 test/typechecker/failure/FunctionArgumentTypeNotAType.dhallb create mode 100644 test/typechecker/failure/FunctionDependentType.dhallb create mode 100644 test/typechecker/failure/FunctionDependentType2.dhallb create mode 100644 test/typechecker/failure/FunctionTypeArgumentTypeNotAType.dhallb create mode 100644 test/typechecker/failure/FunctionTypeKindSort.dhallb create mode 100644 test/typechecker/failure/FunctionTypeTypeKind.dhallb create mode 100644 test/typechecker/failure/FunctionTypeTypeSort.dhallb create mode 100644 test/typechecker/failure/LetWithWrongAnnotation.dhallb create mode 100644 test/typechecker/failure/MergeAlternativeHasNoHandler.dhallb create mode 100644 test/typechecker/failure/MergeAnnotationNotType.dhallb create mode 100644 test/typechecker/failure/MergeEmptyWithoutAnnotation.dhallb create mode 100644 test/typechecker/failure/MergeHandlerNotFunction.dhallb create mode 100644 test/typechecker/failure/MergeHandlerNotInUnion.dhallb create mode 100644 test/typechecker/failure/MergeHandlerNotMatchAlternativeType.dhallb create mode 100644 test/typechecker/failure/MergeHandlersWithDifferentType.dhallb create mode 100644 test/typechecker/failure/MergeLhsNotRecord.dhallb create mode 100644 test/typechecker/failure/MergeRhsNotUnion.dhallb create mode 100644 test/typechecker/failure/MergeWithWrongAnnotation.dhallb create mode 100644 test/typechecker/failure/RecordMixedKinds.dhallb create mode 100644 test/typechecker/failure/RecordMixedKinds2.dhallb create mode 100644 test/typechecker/failure/RecordMixedKinds3.dhallb create mode 100644 test/typechecker/failure/RecordProjectionEmpty.dhallb create mode 100644 test/typechecker/failure/RecordProjectionNotPresent.dhallb create mode 100644 test/typechecker/failure/RecordProjectionNotRecord.dhallb create mode 100644 test/typechecker/failure/RecordSelectionEmpty.dhallb create mode 100644 test/typechecker/failure/RecordSelectionNotPresent.dhallb create mode 100644 test/typechecker/failure/RecordSelectionNotRecord.dhallb create mode 100644 test/typechecker/failure/RecordTypeMixedKinds.dhallb create mode 100644 test/typechecker/failure/RecordTypeMixedKinds2.dhallb create mode 100644 test/typechecker/failure/RecordTypeMixedKinds3.dhallb create mode 100644 test/typechecker/failure/RecordTypeValueMember.dhallb create mode 100644 test/typechecker/failure/RecursiveRecordMergeLhsNotRecord.dhallb create mode 100644 test/typechecker/failure/RecursiveRecordMergeMixedKinds.dhallb create mode 100644 test/typechecker/failure/RecursiveRecordMergeOverlapping.dhallb create mode 100644 test/typechecker/failure/RecursiveRecordMergeRhsNotRecord.dhallb create mode 100644 test/typechecker/failure/RecursiveRecordTypeMergeLhsNotRecordType.dhallb create mode 100644 test/typechecker/failure/RecursiveRecordTypeMergeOverlapping.dhallb create mode 100644 test/typechecker/failure/RecursiveRecordTypeMergeRhsNotRecordType.dhallb create mode 100644 test/typechecker/failure/RightBiasedRecordMergeLhsNotRecord.dhallb create mode 100644 test/typechecker/failure/RightBiasedRecordMergeMixedKinds.dhallb create mode 100644 test/typechecker/failure/RightBiasedRecordMergeMixedKinds2.dhallb create mode 100644 test/typechecker/failure/RightBiasedRecordMergeMixedKinds3.dhallb create mode 100644 test/typechecker/failure/RightBiasedRecordMergeRhsNotRecord.dhallb create mode 100644 test/typechecker/failure/SomeNotType.dhallb create mode 100644 test/typechecker/failure/TypeAnnotationWrong.dhallb create mode 100644 test/typechecker/failure/UnionConstructorFieldNotPresent.dhallb create mode 100644 test/typechecker/failure/UnionTypeMixedKinds.dhallb create mode 100644 test/typechecker/failure/UnionTypeMixedKinds2.dhallb create mode 100644 test/typechecker/failure/UnionTypeMixedKinds3.dhallb create mode 100644 test/typechecker/failure/UnionTypeNotType.dhallb create mode 100755 test/typechecker/gen create mode 100644 test/typechecker/success/DoubleA.dhallb create mode 100644 test/typechecker/success/DoubleB.dhallb create mode 100644 test/typechecker/success/DoubleLiteralA.dhallb create mode 100644 test/typechecker/success/DoubleLiteralB.dhallb create mode 100644 test/typechecker/success/DoubleShowA.dhallb create mode 100644 test/typechecker/success/DoubleShowB.dhallb create mode 100644 test/typechecker/success/FunctionA.dhallb create mode 100644 test/typechecker/success/FunctionApplicationA.dhallb create mode 100644 test/typechecker/success/FunctionApplicationB.dhallb create mode 100644 test/typechecker/success/FunctionB.dhallb create mode 100644 test/typechecker/success/FunctionNamedArgA.dhallb create mode 100644 test/typechecker/success/FunctionNamedArgB.dhallb create mode 100644 test/typechecker/success/FunctionTypeKindKindA.dhallb create mode 100644 test/typechecker/success/FunctionTypeKindKindB.dhallb create mode 100644 test/typechecker/success/FunctionTypeKindTermA.dhallb create mode 100644 test/typechecker/success/FunctionTypeKindTermB.dhallb create mode 100644 test/typechecker/success/FunctionTypeKindTypeA.dhallb create mode 100644 test/typechecker/success/FunctionTypeKindTypeB.dhallb create mode 100644 test/typechecker/success/FunctionTypeTermTermA.dhallb create mode 100644 test/typechecker/success/FunctionTypeTermTermB.dhallb create mode 100644 test/typechecker/success/FunctionTypeTypeTermA.dhallb create mode 100644 test/typechecker/success/FunctionTypeTypeTermB.dhallb create mode 100644 test/typechecker/success/FunctionTypeTypeTypeA.dhallb create mode 100644 test/typechecker/success/FunctionTypeTypeTypeB.dhallb create mode 100644 test/typechecker/success/FunctionTypeUsingArgumentA.dhallb create mode 100644 test/typechecker/success/FunctionTypeUsingArgumentB.dhallb create mode 100644 test/typechecker/success/IntegerA.dhallb create mode 100644 test/typechecker/success/IntegerB.dhallb create mode 100644 test/typechecker/success/IntegerLiteralA.dhallb create mode 100644 test/typechecker/success/IntegerLiteralB.dhallb create mode 100644 test/typechecker/success/IntegerShowA.dhallb create mode 100644 test/typechecker/success/IntegerShowB.dhallb create mode 100644 test/typechecker/success/IntegerToDoubleA.dhallb create mode 100644 test/typechecker/success/IntegerToDoubleB.dhallb create mode 100644 test/typechecker/success/LetA.dhallb create mode 100644 test/typechecker/success/LetB.dhallb create mode 100644 test/typechecker/success/LetNestedTypeSynonymA.dhallb create mode 100644 test/typechecker/success/LetNestedTypeSynonymB.dhallb create mode 100644 test/typechecker/success/LetTypeSynonymA.dhallb create mode 100644 test/typechecker/success/LetTypeSynonymB.dhallb create mode 100644 test/typechecker/success/LetWithAnnotationA.dhallb create mode 100644 test/typechecker/success/LetWithAnnotationB.dhallb create mode 100644 test/typechecker/success/MergeEmptyUnionA.dhallb create mode 100644 test/typechecker/success/MergeEmptyUnionB.dhallb create mode 100644 test/typechecker/success/MergeOneA.dhallb create mode 100644 test/typechecker/success/MergeOneB.dhallb create mode 100644 test/typechecker/success/MergeOneWithAnnotationA.dhallb create mode 100644 test/typechecker/success/MergeOneWithAnnotationB.dhallb create mode 100644 test/typechecker/success/NoneA.dhallb create mode 100644 test/typechecker/success/NoneB.dhallb create mode 100644 test/typechecker/success/OldOptionalNoneA.dhallb create mode 100644 test/typechecker/success/OldOptionalNoneB.dhallb create mode 100644 test/typechecker/success/OldOptionalTrueA.dhallb create mode 100644 test/typechecker/success/OldOptionalTrueB.dhallb create mode 100644 test/typechecker/success/OptionalA.dhallb create mode 100644 test/typechecker/success/OptionalB.dhallb create mode 100644 test/typechecker/success/OptionalBuildA.dhallb create mode 100644 test/typechecker/success/OptionalBuildB.dhallb create mode 100644 test/typechecker/success/OptionalFoldA.dhallb create mode 100644 test/typechecker/success/OptionalFoldB.dhallb create mode 100644 test/typechecker/success/RecordEmptyA.dhallb create mode 100644 test/typechecker/success/RecordEmptyB.dhallb create mode 100644 test/typechecker/success/RecordOneKindA.dhallb create mode 100644 test/typechecker/success/RecordOneKindB.dhallb create mode 100644 test/typechecker/success/RecordOneTypeA.dhallb create mode 100644 test/typechecker/success/RecordOneTypeB.dhallb create mode 100644 test/typechecker/success/RecordOneValueA.dhallb create mode 100644 test/typechecker/success/RecordOneValueB.dhallb create mode 100644 test/typechecker/success/RecordProjectionEmptyA.dhallb create mode 100644 test/typechecker/success/RecordProjectionEmptyB.dhallb create mode 100644 test/typechecker/success/RecordProjectionKindA.dhallb create mode 100644 test/typechecker/success/RecordProjectionKindB.dhallb create mode 100644 test/typechecker/success/RecordProjectionTypeA.dhallb create mode 100644 test/typechecker/success/RecordProjectionTypeB.dhallb create mode 100644 test/typechecker/success/RecordProjectionValueA.dhallb create mode 100644 test/typechecker/success/RecordProjectionValueB.dhallb create mode 100644 test/typechecker/success/RecordSelectionKindA.dhallb create mode 100644 test/typechecker/success/RecordSelectionKindB.dhallb create mode 100644 test/typechecker/success/RecordSelectionTypeA.dhallb create mode 100644 test/typechecker/success/RecordSelectionTypeB.dhallb create mode 100644 test/typechecker/success/RecordSelectionValueA.dhallb create mode 100644 test/typechecker/success/RecordSelectionValueB.dhallb create mode 100644 test/typechecker/success/RecordTypeA.dhallb create mode 100644 test/typechecker/success/RecordTypeB.dhallb create mode 100644 test/typechecker/success/RecordTypeEmptyA.dhallb create mode 100644 test/typechecker/success/RecordTypeEmptyB.dhallb create mode 100644 test/typechecker/success/RecordTypeKindA.dhallb create mode 100644 test/typechecker/success/RecordTypeKindB.dhallb create mode 100644 test/typechecker/success/RecordTypeTypeA.dhallb create mode 100644 test/typechecker/success/RecordTypeTypeB.dhallb create mode 100644 test/typechecker/success/RecursiveRecordMergeLhsEmptyA.dhallb create mode 100644 test/typechecker/success/RecursiveRecordMergeLhsEmptyB.dhallb create mode 100644 test/typechecker/success/RecursiveRecordMergeRecursivelyA.dhallb create mode 100644 test/typechecker/success/RecursiveRecordMergeRecursivelyB.dhallb create mode 100644 test/typechecker/success/RecursiveRecordMergeRecursivelyKindsA.dhallb create mode 100644 test/typechecker/success/RecursiveRecordMergeRecursivelyKindsB.dhallb create mode 100644 test/typechecker/success/RecursiveRecordMergeRecursivelyTypesA.dhallb create mode 100644 test/typechecker/success/RecursiveRecordMergeRecursivelyTypesB.dhallb create mode 100644 test/typechecker/success/RecursiveRecordMergeRhsEmptyA.dhallb create mode 100644 test/typechecker/success/RecursiveRecordMergeRhsEmptyB.dhallb create mode 100644 test/typechecker/success/RecursiveRecordMergeTwoA.dhallb create mode 100644 test/typechecker/success/RecursiveRecordMergeTwoB.dhallb create mode 100644 test/typechecker/success/RecursiveRecordMergeTwoKindsA.dhallb create mode 100644 test/typechecker/success/RecursiveRecordMergeTwoKindsB.dhallb create mode 100644 test/typechecker/success/RecursiveRecordMergeTwoTypesA.dhallb create mode 100644 test/typechecker/success/RecursiveRecordMergeTwoTypesB.dhallb create mode 100644 test/typechecker/success/RecursiveRecordTypeMergeRecursivelyA.dhallb create mode 100644 test/typechecker/success/RecursiveRecordTypeMergeRecursivelyB.dhallb create mode 100644 test/typechecker/success/RecursiveRecordTypeMergeRecursivelyKindsA.dhallb create mode 100644 test/typechecker/success/RecursiveRecordTypeMergeRecursivelyKindsB.dhallb create mode 100644 test/typechecker/success/RecursiveRecordTypeMergeRecursivelyTypesA.dhallb create mode 100644 test/typechecker/success/RecursiveRecordTypeMergeRecursivelyTypesB.dhallb create mode 100644 test/typechecker/success/RecursiveRecordTypeMergeRhsEmptyA.dhallb create mode 100644 test/typechecker/success/RecursiveRecordTypeMergeRhsEmptyB.dhallb create mode 100644 test/typechecker/success/RecursiveRecordTypeMergeTwoA.dhallb create mode 100644 test/typechecker/success/RecursiveRecordTypeMergeTwoB.dhallb create mode 100644 test/typechecker/success/RecursiveRecordTypeMergeTwoKindsA.dhallb create mode 100644 test/typechecker/success/RecursiveRecordTypeMergeTwoKindsB.dhallb create mode 100644 test/typechecker/success/RecursiveRecordTypeMergeTwoTypesA.dhallb create mode 100644 test/typechecker/success/RecursiveRecordTypeMergeTwoTypesB.dhallb create mode 100644 test/typechecker/success/RightBiasedRecordMergeRhsEmptyA.dhallb create mode 100644 test/typechecker/success/RightBiasedRecordMergeRhsEmptyB.dhallb create mode 100644 test/typechecker/success/RightBiasedRecordMergeTwoA.dhallb create mode 100644 test/typechecker/success/RightBiasedRecordMergeTwoB.dhallb create mode 100644 test/typechecker/success/RightBiasedRecordMergeTwoDifferentA.dhallb create mode 100644 test/typechecker/success/RightBiasedRecordMergeTwoDifferentB.dhallb create mode 100644 test/typechecker/success/RightBiasedRecordMergeTwoKindsA.dhallb create mode 100644 test/typechecker/success/RightBiasedRecordMergeTwoKindsB.dhallb create mode 100644 test/typechecker/success/RightBiasedRecordMergeTwoTypesA.dhallb create mode 100644 test/typechecker/success/RightBiasedRecordMergeTwoTypesB.dhallb create mode 100644 test/typechecker/success/SomeTrueA.dhallb create mode 100644 test/typechecker/success/SomeTrueB.dhallb create mode 100644 test/typechecker/success/TypeAnnotationA.dhallb create mode 100644 test/typechecker/success/TypeAnnotationB.dhallb create mode 100644 test/typechecker/success/UnionConstructorFieldA.dhallb create mode 100644 test/typechecker/success/UnionConstructorFieldB.dhallb create mode 100644 test/typechecker/success/UnionOneA.dhallb create mode 100644 test/typechecker/success/UnionOneB.dhallb create mode 100644 test/typechecker/success/UnionTypeEmptyA.dhallb create mode 100644 test/typechecker/success/UnionTypeEmptyB.dhallb create mode 100644 test/typechecker/success/UnionTypeKindA.dhallb create mode 100644 test/typechecker/success/UnionTypeKindB.dhallb create mode 100644 test/typechecker/success/UnionTypeOneA.dhallb create mode 100644 test/typechecker/success/UnionTypeOneB.dhallb create mode 100644 test/typechecker/success/UnionTypeTypeA.dhallb create mode 100644 test/typechecker/success/UnionTypeTypeB.dhallb diff --git a/lib/dhall/ast.rb b/lib/dhall/ast.rb index a678712..3dcf33d 100644 --- a/lib/dhall/ast.rb +++ b/lib/dhall/ast.rb @@ -179,7 +179,11 @@ module Dhall end def dhall_eq(other) - reduce(other, super) + if other.is_a?(Bool) + reduce(other, with(value: self == other)) + else + reduce(other, super) + end end def as_json @@ -197,6 +201,10 @@ module Dhall new(name: name, index: index) end + def to_s + "#{name}@#{index}" + end + def as_json if name == "_" index @@ -241,8 +249,11 @@ module Dhall end class List < Expression + include Enumerable + include(ValueSemantics.for_attributes do - elements ArrayOf(Expression) + elements Util::ArrayOf.new(Expression, min: 1) + type Either(nil, Expression), default: nil end) def self.of(*args) @@ -253,12 +264,8 @@ module Dhall [4, nil, *elements.map(&:as_json)] end - def type - # TODO: inferred element type - end - def map(type: nil, &block) - with(elements: elements.each_with_index.map(&block)) + with(elements: elements.each_with_index.map(&block), type: type) end def each(&block) @@ -275,11 +282,11 @@ module Dhall end def first - Optional.new(value: elements.first, type: type) + Optional.for(elements.first, type: type) end def last - Optional.new(value: elements.last, type: type) + Optional.for(elements.last, type: type) end def reverse @@ -297,7 +304,7 @@ module Dhall class EmptyList < List include(ValueSemantics.for_attributes do - type Expression + type Either(nil, Expression) end) def as_json @@ -343,6 +350,18 @@ module Dhall type Either(nil, Expression), default: nil end) + def self.for(value, type: nil) + if value.nil? + OptionalNone.new(type: type) + else + Optional.new(value: value, type: type) + end + end + + def map(type: nil, &block) + with(value: block[value], type: type) + end + def reduce(_, &block) block[value] end @@ -357,6 +376,10 @@ module Dhall type Expression end) + def map(type: nil) + type.nil? ? self : with(type: type) + end + def reduce(z) z end @@ -384,8 +407,22 @@ module Dhall record Util::HashOf.new(::String, Expression, min: 1) end) + def self.for(types) + if types.empty? + EmptyRecordType.new + else + RecordType.new(record: types) + end + end + + def merge_type(other) + return self if other.is_a?(EmptyRecordType) + + with(record: record.merge(other.record)) + end + def deep_merge_type(other) - return super unless other.is_a?(RecordType) + return super unless other.class == RecordType with(record: Hash[record.merge(other.record) { |_, v1, v2| v1.deep_merge_type(v2) @@ -405,9 +442,17 @@ module Dhall end end - class EmptyRecordType < Expression + class EmptyRecordType < RecordType include(ValueSemantics.for_attributes {}) + def record + {} + end + + def merge_type(other) + other + end + def deep_merge_type(other) other end @@ -448,6 +493,10 @@ module Dhall with(record: Hash[record.merge(other.record).sort]) end + def map(&block) + with(record: Hash[record.map(&block)]) + end + def ==(other) other.respond_to?(:record) && record.to_a == other.record.to_a end @@ -480,6 +529,10 @@ module Dhall other end + def map + self + end + def as_json [8, {}] end @@ -512,6 +565,10 @@ module Dhall record Expression end) + def selectors + [] + end + def as_json [10, record.as_json] end @@ -522,6 +579,10 @@ module Dhall alternatives Util::HashOf.new(::String, Expression) end) + def record + alternatives + end + def ==(other) other.is_a?(UnionType) && alternatives.to_a == other.alternatives.to_a end @@ -530,7 +591,11 @@ module Dhall self == other end - def fetch(k) + def fetch(k, default=nil) + if (default || block_given?) && !alternatives.key?(k) + return (default || yield) + end + remains = with(alternatives: alternatives.dup.tap { |r| r.delete(k) }) Function.new( var: k, @@ -540,7 +605,7 @@ module Dhall value: Variable.new(name: k), alternatives: remains ) - ) + ).normalize end def as_json @@ -944,6 +1009,25 @@ module Dhall body Expression end) + def unflatten + lets.reverse.reduce(body) do |inside, let| + LetBlock.new(lets: [let], body: inside) + end + end + + def desugar + lets.reverse.reduce(body) do |inside, let| + Application.new( + function: Function.new( + var: let.var, + type: let.type, + body: inside + ), + arguments: [let.assign] + ) + end + end + def as_json [25, *lets.flat_map(&:as_json), body.as_json] end diff --git a/lib/dhall/binary.rb b/lib/dhall/binary.rb index 0c09099..017790c 100644 --- a/lib/dhall/binary.rb +++ b/lib/dhall/binary.rb @@ -70,10 +70,10 @@ module Dhall class List def self.decode(type, *els) - if type.nil? - List.new(elements: els.map(&Dhall.method(:decode))) + if els.empty? + EmptyList.new(type: type.nil? ? nil : Dhall.decode(type)) else - EmptyList.new(type: Dhall.decode(type)) + List.new(elements: els.map(&Dhall.method(:decode))) end end end diff --git a/lib/dhall/builtins.rb b/lib/dhall/builtins.rb index 18ed7d7..ea2a104 100644 --- a/lib/dhall/builtins.rb +++ b/lib/dhall/builtins.rb @@ -257,14 +257,14 @@ module Dhall protected def _call(arg) - arg.map(type: indexed_type(type)) do |x, idx| + arg.map(type: indexed_type(type)) { |x, idx| Record.new( record: { "index" => Natural.new(value: idx), "value" => x } ) - end + }.normalize end def indexed_type(value_type) diff --git a/lib/dhall/normalize.rb b/lib/dhall/normalize.rb index 6e9452f..4d2bb6a 100644 --- a/lib/dhall/normalize.rb +++ b/lib/dhall/normalize.rb @@ -236,9 +236,15 @@ module Dhall end class List + def normalize + super.with(type: nil) + end end class EmptyList + def normalize + super.with(type: type.normalize) + end end class Optional @@ -353,21 +359,14 @@ module Dhall desugar.normalize end - def desugar - lets.reverse.reduce(body) do |inside, let| - Application.new( - function: Function.new( - var: let.var, - type: let.type, - body: inside - ), - arguments: [let.assign] - ) - end - end - def shift(amount, name, min_index) - desugar.shift(amount, name, min_index) + return unflatten.shift(amount, name, min_index) if lets.length > 1 + return super unless lets.first.var == name + + with( + lets: [let.first.shift(amount, name, min_index)], + body: body.shift(amount, name, min_index + 1) + ) end end diff --git a/lib/dhall/typecheck.rb b/lib/dhall/typecheck.rb index 6b69146..56cfeaf 100644 --- a/lib/dhall/typecheck.rb +++ b/lib/dhall/typecheck.rb @@ -1,6 +1,7 @@ # frozen_string_literal: true require "dhall/ast" +require "dhall/normalize" module Dhall module TypeChecker @@ -8,7 +9,8 @@ module Dhall case expr when Dhall::Variable Variable.new(expr) - when Dhall::Bool, Dhall::Natural, Dhall::Text + when Dhall::Bool, Dhall::Natural, Dhall::Text, Dhall::Integer, + Dhall::Double Literal.new(expr) when Dhall::TextLiteral TextLiteral.new(expr) @@ -16,11 +18,14 @@ module Dhall EmptyList.new(expr) when Dhall::List List.new(expr) + when Dhall::OptionalNone + OptionalNone.new(expr) + when Dhall::Optional + Optional.new(expr) when Dhall::If If.new(expr) when Dhall::Application - # TODO - Variable.new(Dhall::Variable["Bool"]) + Application.new(expr) when Dhall::Operator::And, Dhall::Operator::Or, Dhall::Operator::Equal, Dhall::Operator::NotEqual Operator.new(expr, Dhall::Variable["Bool"]) @@ -30,6 +35,36 @@ module Dhall Operator.new(expr, Dhall::Variable["Text"]) when Dhall::Operator::ListConcatenate OperatorListConcatenate.new(expr) + when Dhall::Operator::RecursiveRecordMerge + OperatorRecursiveRecordMerge.new(expr) + when Dhall::Operator::RightBiasedRecordMerge + OperatorRightBiasedRecordMerge.new(expr) + when Dhall::Operator::RecursiveRecordTypeMerge + OperatorRecursiveRecordTypeMerge.new(expr) + when Dhall::EmptyRecordType + EmptyAnonymousType.new(expr) + when Dhall::RecordType, Dhall::UnionType + AnonymousType.new(expr) + when Dhall::EmptyRecord + EmptyRecord.new(expr) + when Dhall::Record + Record.new(expr) + when Dhall::RecordSelection + RecordSelection.new(expr) + when Dhall::RecordProjection, Dhall::EmptyRecordProjection + RecordProjection.new(expr) + when Dhall::Union + Union.new(expr) + when Dhall::Merge + Merge.new(expr) + when Dhall::Forall + Forall.new(expr) + when Dhall::Function + Function.new(expr) + when Dhall::LetBlock + LetBlock.new(expr) + when Dhall::TypeAnnotation + TypeAnnotation.new(expr) when Dhall::Builtin Builtin.new(expr) else @@ -53,22 +88,50 @@ module Dhall name => [type] + @bindings[name] )) end + + def shift(amount, name, min_index) + self.class.new(@bindings.merge( + Hash[@bindings.map { |var, bindings| + [var, bindings.map { |b| b.shift(amount, name, min_index) }] + }] + )) + end end + KINDS = [ + Dhall::Variable["Type"], + Dhall::Variable["Kind"], + Dhall::Variable["Sort"] + ].freeze + class Variable def initialize(var) @var = var end BUILTIN = { - "Type" => Dhall::Variable["Kind"], - "Kind" => Dhall::Variable["Sort"], - "Bool" => Dhall::Variable["Type"], - "Natural" => Dhall::Variable["Type"], - "Text" => Dhall::Variable["Type"], - "List" => Dhall::Forall.of_arguments( + "Type" => Dhall::Variable["Kind"], + "Kind" => Dhall::Variable["Sort"], + "Bool" => Dhall::Variable["Type"], + "Natural" => Dhall::Variable["Type"], + "Integer" => Dhall::Variable["Type"], + "Double" => Dhall::Variable["Type"], + "Text" => Dhall::Variable["Type"], + "List" => Dhall::Forall.of_arguments( Dhall::Variable["Type"], body: Dhall::Variable["Type"] + ), + "Optional" => Dhall::Forall.of_arguments( + Dhall::Variable["Type"], + body: Dhall::Variable["Type"] + ), + "None" => Dhall::Forall.new( + var: "A", + type: Dhall::Variable["Type"], + body: Dhall::Application.new( + function: Dhall::Variable["Optional"], + arguments: [Dhall::Variable["A"]] + ) ) }.freeze @@ -216,6 +279,104 @@ module Dhall end end + class OperatorRecursiveRecordMerge + def initialize(expr) + @expr = expr + @lhs = TypeChecker.for(expr.lhs) + @rhs = TypeChecker.for(expr.rhs) + end + + def annotate(context) + annotated_lhs = @lhs.annotate(context) + annotated_rhs = @rhs.annotate(context) + + type = annotated_lhs.type.deep_merge_type(annotated_rhs.type) + + unless type.is_a?(Dhall::RecordType) + raise TypeError, "RecursiveRecordMerge got #{type}" + end + + # Annotate to sanity check + TypeChecker.for(type).annotate(context) + + Dhall::TypeAnnotation.new( + value: @expr.with(lhs: annotated_lhs, rhs: annotated_rhs), + type: type + ) + end + end + + class OperatorRightBiasedRecordMerge + def initialize(expr) + @expr = expr + @lhs = TypeChecker.for(expr.lhs) + @rhs = TypeChecker.for(expr.rhs) + end + + def annotate(context) + annotated_lhs = @lhs.annotate(context) + annotated_rhs = @rhs.annotate(context) + + unless annotated_lhs.type.is_a?(Dhall::RecordType) + raise TypeError, "RecursiveRecordMerge got #{annotated_lhs.type}" + end + + unless annotated_rhs.type.is_a?(Dhall::RecordType) + raise TypeError, "RecursiveRecordMerge got #{annotated_rhs.type}" + end + + lkind = TypeChecker.for(annotated_lhs.type).annotate(context).type + rkind = TypeChecker.for(annotated_rhs.type).annotate(context).type + + if lkind != rkind + raise TypeError, "RecursiveRecordMerge got mixed kinds: " \ + "#{lkind}, #{rkind}" + end + + type = annotated_lhs.type.merge_type(annotated_rhs.type) + + # Annotate to sanity check + TypeChecker.for(type).annotate(context) + + Dhall::TypeAnnotation.new( + value: @expr.with(lhs: annotated_lhs, rhs: annotated_rhs), + type: type + ) + end + end + + class OperatorRecursiveRecordTypeMerge + def initialize(expr) + @expr = expr + @lhs = TypeChecker.for(expr.lhs) + @rhs = TypeChecker.for(expr.rhs) + end + + def annotate(context) + annotated_lhs = @lhs.annotate(context) + annotated_rhs = @rhs.annotate(context) + + if annotated_lhs.type != annotated_rhs.type + raise TypeError, "RecursiveRecordTypeMerge mixed kinds: " \ + "#{annotated_lhs.type}, #{annotated_rhs.type}" + end + + type = @expr.lhs.deep_merge_type(@expr.rhs) + + unless type.is_a?(Dhall::RecordType) + raise TypeError, "RecursiveRecordMerge got #{type}" + end + + # Annotate to sanity check + TypeChecker.for(type).annotate(context) + + Dhall::TypeAnnotation.new( + value: @expr, + type: annotated_lhs.type + ) + end + end + class EmptyList def initialize(expr) @expr = expr @@ -267,6 +428,423 @@ module Dhall end end + class OptionalNone + def initialize(expr) + @expr = expr + end + + def annotate(context) + type_type = TypeChecker.for(@expr.type).annotate(context).type + if type_type != Dhall::Variable["Type"] + raise TypeError, "OptionalNone element type not of type Type" + end + + Dhall::TypeAnnotation.new( + value: @expr, + type: Dhall::Application.new( + function: Dhall::Variable["Optional"], + arguments: [@expr.type] + ) + ) + end + end + + class Optional + def initialize(some) + @some = some + end + + def annotate(context) + asome = @some.map(type: @some.type) do |el| + TypeChecker.for(el).annotate(context) + end + some = asome.with(type: asome.value.type) + + type_type = TypeChecker.for(some.type).annotate(context).type + if type_type != Dhall::Variable["Type"] + raise TypeError, "Some type no of type Type, was: #{type_type}" + end + + Dhall::TypeAnnotation.new( + value: some, + type: Dhall::Application.new( + function: Dhall::Variable["Optional"], + arguments: [some.type] + ) + ) + end + end + + class EmptyAnonymousType + def initialize(expr) + @expr = expr + end + + def annotate(context) + Dhall::TypeAnnotation.new( + value: @expr, + type: Dhall::Variable["Type"] + ) + end + end + + class AnonymousType + def initialize(type) + @type = type + end + + def annotate(context) + kinds = @type.record.values.map do |mtype| + TypeChecker.for(mtype).annotate(context).type + end + + if (bad = kinds.find { |t| !KINDS.include?(t) }) + raise TypeError, "AnonymousType field kind #{bad} "\ + "not one of #{KINDS}" + end + + if (bad = kinds.find { |t| t != kinds.first }) + raise TypeError, "AnonymousType field kind #{bad} "\ + "does not match #{kinds.first}" + end + + Dhall::TypeAnnotation.new( + value: @type, + type: kinds.first || KINDS.first + ) + end + end + + class EmptyRecord + def initialize(expr) + @expr = expr + end + + def annotate(context) + Dhall::TypeAnnotation.new( + value: @expr, + type: Dhall::EmptyRecordType.new + ) + end + end + + class Record + def initialize(record) + @record = record + end + + def annotate(context) + arecord = @record.map do |k, v| + [k, TypeChecker.for(v).annotate(context)] + end + + type = Dhall::RecordType.for(Hash[ + arecord.record.map { |k, v| [k, v.type] } + ]) + + # Annonate to sanity check + TypeChecker.for(type).annotate(context) + + Dhall::TypeAnnotation.new( + value: arecord, + type: type + ) + end + end + + class RecordSelection + def initialize(selection) + @selection = selection + @record = selection.record + @selector = selection.selector + end + + def annotate(context) + arecord = TypeChecker.for(@record).annotate(context) + + if arecord.type == Dhall::Variable["Type"] + Dhall::TypeAnnotation.new( + value: @selection, + type: TypeChecker.for(@record.normalize.fetch(@selector) { + raise TypeError, "#{@record} has no field #{@selector}" + }).annotate(context).type.with(var: @selector) + ) + else + fetch_from = if arecord.type.class == Dhall::RecordType + arecord.type.record + elsif arecord.value.is_a?(Dhall::Record) + arecord.value.record + else + raise TypeError, "RecordSelection on #{arecord.type}" + end + + Dhall::TypeAnnotation.new( + value: @selection.with(record: arecord), + type: fetch_from.fetch(@selector) do + raise TypeError, "#{fetch_from} has no field #{@selector}" + end + ) + end + end + end + + class RecordProjection + def initialize(projection) + @projection = projection + @record = projection.record + @selectors = projection.selectors + end + + def annotate(context) + arecord = TypeChecker.for(@record).annotate(context) + + unless arecord.type.class == Dhall::RecordType + raise TypeError, "RecordProjection on #{arecord.type}" + end + + slice = arecord.type.record.select { |k, _| @selectors.include?(k) } + if slice.size != @selectors.length + raise TypeError, "#{arecord.type} missing one of: #{@selectors}" + end + + Dhall::TypeAnnotation.new( + value: @projection.with(record: arecord), + type: Dhall::RecordType.for(slice) + ) + end + end + + class Union + def initialize(union) + @union = union + @value = TypeChecker.for(union.value) + end + + def annotate(context) + annotated_value = @value.annotate(context) + + type = Dhall::UnionType.new( + alternatives: Hash[@union.alternatives.alternatives.merge( + @union.tag => annotated_value.type + ).sort] + ) + + # Annotate to sanity check + TypeChecker.for(type).annotate(context) + + Dhall::TypeAnnotation.new( + value: @union.with(value: annotated_value), + type: type + ) + end + end + + class Merge + def initialize(merge) + @merge = merge + @record = TypeChecker.for(merge.record) + @union = TypeChecker.for(merge.input) + end + + def annotate(context) + arecord = @record.annotate(context) + aunion = @union.annotate(context) + + unless arecord.type.is_a?(Dhall::RecordType) + raise TypeError, "Merge expected Record got: #{arecord.type}" + end + + unless aunion.type.is_a?(Dhall::UnionType) + raise TypeError, "Merge expected Union got: #{aunion.type}" + end + + type = arecord.type.record.reduce(@merge.type) do |type, (k, htype)| + unless aunion.type.alternatives.key?(k) + raise TypeError, "Merge handler for unknown alternative: #{k}" + end + + unless htype.is_a?(Dhall::Forall) + raise TypeError, "Merge handlers must all be functions" + end + + if type && htype.body != type + raise TypeError, "Handler output types must all match" + end + + htype.body.shift(-1, htype.var, 0) + end + + aunion.type.alternatives.each do |k, atype| + unless arecord.type.record.key?(k) + raise TypeError, "No merge handler for alternative: #{k}" + end + + unless arecord.type.record[k].type == atype + raise TypeError, "Handler argument does not match " \ + "alternative type: #{atype}" + end + end + + kind = TypeChecker.for(type).annotate(context).type + unless kind == Dhall::Variable["Type"] + raise TypeError, "Merge must have kind Type" + end + + Dhall::TypeAnnotation.new( + value: @merge.with(record: arecord, input: aunion), + type: type + ) + end + end + + class Forall + def initialize(expr) + @expr = expr + @input = TypeChecker.for(expr.type) + @output = TypeChecker.for(expr.body) + end + + def annotate(context) + inkind = @input.annotate(context).type + outkind = @output.annotate( + context.add(@expr.var, @expr.type).shift(1, @expr.var, 0) + ).type + + if !KINDS.include?(inkind) || !KINDS.include?(outkind) + raise TypeError, "FunctionType part of this is a term" + end + + if KINDS.index(outkind) > KINDS.index(inkind) + raise TypeError, "Dependent types are not allowed" + end + + type = if outkind == KINDS.first + KINDS.first + else + KINDS[[KINDS.index(outkind), KINDS.index(inkind)].max] + end + + Dhall::TypeAnnotation.new( + value: @expr, + type: type + ) + end + end + + class Function + def initialize(func) + @func = func + @output = TypeChecker.for(func.body) + end + + def annotate(context) + abody = @output.annotate( + context.add(@func.var, @func.type).shift(1, @func.var, 0) + ) + + type = Dhall::Forall.new( + var: @func.var, + type: @func.type, + body: abody.type + ) + + # Annotate to sanity check + TypeChecker.for(type).annotate(context) + + Dhall::TypeAnnotation.new( + value: @func.with(body: abody), + type: type + ) + end + end + + class Application + def initialize(app) + @app = app + @func = TypeChecker.for(app.function) + @arg = TypeChecker.for(app.arguments.first) + end + + def annotate(context) + afunc = @func.annotate(context) + aarg = @arg.annotate(context) + + unless afunc.type.is_a?(Dhall::Forall) + raise TypeError, "Application LHS is not a function" + end + + unless afunc.type.type.normalize == aarg.type.normalize + raise TypeError, "Application expected #{afunc.type.type} "\ + "got #{aarg.type}" + end + + type = afunc.type.body.substitute( + Dhall::Variable[afunc.type.var], + aarg.value.shift(1, afunc.type.var, 0) + ).shift(-1, afunc.type.var, 0) + + Dhall::TypeAnnotation.new( + value: @app.with(function: afunc, arguments: [aarg]), + type: type + ) + end + end + + class LetBlock + def initialize(letblock) + @letblock = letblock.unflatten + @let = @letblock.lets.first + end + + def annotate(context) + aassign = TypeChecker.for(@let.assign).annotate(context) + + if @let.type && @let.type != aassign.type + raise TypeError, "Let assignment does not match annotation: " \ + "#{@let.type}, #{aassign.type}" + end + + Dhall::Function.disable_alpha_normalization! + nassign = @let.assign.normalize.shift(1, @let.var, 0) + Dhall::Function.enable_alpha_normalization! + + abody = TypeChecker.for(@letblock.body.substitute( + Dhall::Variable[@let.var], + nassign + ).shift(-1, @let.var, 0)).annotate(context) + + ablock = @letblock.with( + lets: [@let.with(type: aassign.type)], + body: Dhall::TypeAnnotation.new( + value: @letblock.body, + type: abody.type + ) + ) + + Dhall::TypeAnnotation.new( + value: ablock, + type: abody.type + ) + end + end + + class TypeAnnotation + def initialize(expr) + @expr = expr + end + + def annotate(context) + redo_annotation = TypeChecker.for(@expr.value).annotate(context) + + if redo_annotation.type == @expr.type + redo_annotation + else + raise TypeError, "TypeAnnotation does not match: " \ + "#{@expr.type}, #{redo_annotation.type}" + end + end + end + class Builtin def initialize(builtin) @expr = builtin @@ -459,7 +1037,71 @@ module Dhall arguments: [Dhall::Variable["a"]] ) ) - ) + ), + "Optional/fold" => Dhall::Forall.new( + var: "a", + type: Dhall::Variable["Type"], + body: Dhall::Forall.of_arguments( + Dhall::Application.new( + function: Dhall::Variable["Optional"], + arguments: [Dhall::Variable["a"]] + ), + body: Dhall::Forall.new( + var: "optional", + type: Dhall::Variable["Type"], + body: Dhall::Forall.new( + var: "just", + type: Dhall::Forall.of_arguments( + Dhall::Variable["a"], + body: Dhall::Variable["optional"] + ), + body: Dhall::Forall.new( + var: "nothing", + type: Dhall::Variable["optional"], + body: Dhall::Variable["optional"] + ) + ) + ) + ) + ), + "Optional/build" => Dhall::Forall.new( + var: "a", + type: Dhall::Variable["Type"], + body: Dhall::Forall.of_arguments( + Dhall::Forall.new( + var: "optional", + type: Dhall::Variable["Type"], + body: Dhall::Forall.new( + var: "just", + type: Dhall::Forall.of_arguments( + Dhall::Variable["a"], + body: Dhall::Variable["optional"] + ), + body: Dhall::Forall.new( + var: "nothing", + type: Dhall::Variable["optional"], + body: Dhall::Variable["optional"] + ) + ) + ), + body: Dhall::Application.new( + function: Dhall::Variable["Optional"], + arguments: [Dhall::Variable["a"]] + ) + ) + ), + "Integer/show" => Dhall::Forall.of_arguments( + Dhall::Variable["Integer"], + body: Dhall::Variable["Text"] + ), + "Integer/toDouble" => Dhall::Forall.of_arguments( + Dhall::Variable["Integer"], + body: Dhall::Variable["Double"] + ), + "Double/show" => Dhall::Forall.of_arguments( + Dhall::Variable["Double"], + body: Dhall::Variable["Text"] + ), }.freeze def annotate(*) diff --git a/test/test_typechecker.rb b/test/test_typechecker.rb index 999d038..39ff1fb 100644 --- a/test/test_typechecker.rb +++ b/test/test_typechecker.rb @@ -6,12 +6,13 @@ require "pathname" require "dhall/typecheck" require "dhall/binary" -class TestNormalization < Minitest::Test +class TestTypechecker < Minitest::Test DIRPATH = Pathname.new(File.dirname(__FILE__)) TESTS = DIRPATH + "typechecker/" Pathname.glob(TESTS + "success/**/*A.dhallb").each do |path| test = path.relative_path_from(TESTS).to_s.sub(/A\.dhallb$/, "") + next if test =~ /prelude/ define_method("test_#{test}") do assert_equal( @@ -31,7 +32,7 @@ class TestNormalization < Minitest::Test expr = Dhall.from_binary(path.binread) Dhall::TypeChecker.for( expr - ).annotate(Dhall::TypeChecker::Context.new).type + ).annotate(Dhall::TypeChecker::Context.new) end end end diff --git a/test/typechecker/failure/FunctionApplicationArgumentNotMatch.dhallb b/test/typechecker/failure/FunctionApplicationArgumentNotMatch.dhallb new file mode 100644 index 0000000000000000000000000000000000000000..ed4dc82d454b4296b0c33251edcbc2da02dff89a GIT binary patch literal 14 VcmZo>Xl6|JODriZO3Y#S3IHP%1v>x$ literal 0 HcmV?d00001 diff --git a/test/typechecker/failure/FunctionApplicationIsNotFunction.dhallb b/test/typechecker/failure/FunctionApplicationIsNotFunction.dhallb new file mode 100644 index 0000000000000000000000000000000000000000..76981709a4e0b623fb8e1b85aaa3340f5b8f4280 GIT binary patch literal 4 LcmZo>`1%z91n&ZF literal 0 HcmV?d00001 diff --git a/test/typechecker/failure/FunctionArgumentTypeNotAType.dhallb b/test/typechecker/failure/FunctionArgumentTypeNotAType.dhallb new file mode 100644 index 0000000000000000000000000000000000000000..fca496703a906dd97613b821ba61b295770eced6 GIT binary patch literal 6 NcmZo>Y~p8R000G40T%!O literal 0 HcmV?d00001 diff --git a/test/typechecker/failure/FunctionDependentType.dhallb b/test/typechecker/failure/FunctionDependentType.dhallb new file mode 100644 index 0000000..70f240a --- /dev/null +++ b/test/typechecker/failure/FunctionDependentType.dhallb @@ -0,0 +1 @@ +„axdBooldBool \ No newline at end of file diff --git a/test/typechecker/failure/FunctionDependentType2.dhallb b/test/typechecker/failure/FunctionDependentType2.dhallb new file mode 100644 index 0000000..4d6d713 --- /dev/null +++ b/test/typechecker/failure/FunctionDependentType2.dhallb @@ -0,0 +1 @@ +„axdBooldType \ No newline at end of file diff --git a/test/typechecker/failure/FunctionTypeArgumentTypeNotAType.dhallb b/test/typechecker/failure/FunctionTypeArgumentTypeNotAType.dhallb new file mode 100644 index 0000000000000000000000000000000000000000..0654cf40765735b6883bb9b02c9c6b6e687685f9 GIT binary patch literal 6 NcmZo>YT{>N000GB0T}=Q literal 0 HcmV?d00001 diff --git a/test/typechecker/failure/FunctionTypeKindSort.dhallb b/test/typechecker/failure/FunctionTypeKindSort.dhallb new file mode 100644 index 0000000..766fd9a --- /dev/null +++ b/test/typechecker/failure/FunctionTypeKindSort.dhallb @@ -0,0 +1 @@ +ƒdKinddSort \ No newline at end of file diff --git a/test/typechecker/failure/FunctionTypeTypeKind.dhallb b/test/typechecker/failure/FunctionTypeTypeKind.dhallb new file mode 100644 index 0000000..362c98f --- /dev/null +++ b/test/typechecker/failure/FunctionTypeTypeKind.dhallb @@ -0,0 +1 @@ +ƒdTypedKind \ No newline at end of file diff --git a/test/typechecker/failure/FunctionTypeTypeSort.dhallb b/test/typechecker/failure/FunctionTypeTypeSort.dhallb new file mode 100644 index 0000000..908733a --- /dev/null +++ b/test/typechecker/failure/FunctionTypeTypeSort.dhallb @@ -0,0 +1 @@ +ƒdTypedSort \ No newline at end of file diff --git a/test/typechecker/failure/LetWithWrongAnnotation.dhallb b/test/typechecker/failure/LetWithWrongAnnotation.dhallb new file mode 100644 index 0000000..adf0620 --- /dev/null +++ b/test/typechecker/failure/LetWithWrongAnnotation.dhallb @@ -0,0 +1 @@ +…axgNaturalõõ \ No newline at end of file diff --git a/test/typechecker/failure/MergeAlternativeHasNoHandler.dhallb b/test/typechecker/failure/MergeAlternativeHasNoHandler.dhallb new file mode 100644 index 0000000..1e7418c --- /dev/null +++ b/test/typechecker/failure/MergeAlternativeHasNoHandler.dhallb @@ -0,0 +1 @@ +ƒ‚ „ axõ  \ No newline at end of file diff --git a/test/typechecker/failure/MergeAnnotationNotType.dhallb b/test/typechecker/failure/MergeAnnotationNotType.dhallb new file mode 100644 index 0000000..8de8486 --- /dev/null +++ b/test/typechecker/failure/MergeAnnotationNotType.dhallb @@ -0,0 +1 @@ +„‚ ‚  dType \ No newline at end of file diff --git a/test/typechecker/failure/MergeEmptyWithoutAnnotation.dhallb b/test/typechecker/failure/MergeEmptyWithoutAnnotation.dhallb new file mode 100644 index 0000000..250175d --- /dev/null +++ b/test/typechecker/failure/MergeEmptyWithoutAnnotation.dhallb @@ -0,0 +1 @@ +ƒ‚ ‚   \ No newline at end of file diff --git a/test/typechecker/failure/MergeHandlerNotFunction.dhallb b/test/typechecker/failure/MergeHandlerNotFunction.dhallb new file mode 100644 index 0000000..31c3f0c --- /dev/null +++ b/test/typechecker/failure/MergeHandlerNotFunction.dhallb @@ -0,0 +1 @@ +ƒ‚¡axõ„ axõ  \ No newline at end of file diff --git a/test/typechecker/failure/MergeHandlerNotInUnion.dhallb b/test/typechecker/failure/MergeHandlerNotInUnion.dhallb new file mode 100644 index 0000000000000000000000000000000000000000..6104bbf47c2b54635c6c3a6a2eac0e5ae39d3f30 GIT binary patch literal 23 bcmZo+YvNd#SkcUw;*_7C!_dUN0L%aYUvLN@ literal 0 HcmV?d00001 diff --git a/test/typechecker/failure/MergeHandlerNotMatchAlternativeType.dhallb b/test/typechecker/failure/MergeHandlerNotMatchAlternativeType.dhallb new file mode 100644 index 0000000000000000000000000000000000000000..0fd3f8dc92b40a6aa915c33af088273677c9dc5f GIT binary patch literal 23 ecmZo>YvNd#SkcUw;*_7C!_dN$Skc7KxBviMk_Vjt literal 0 HcmV?d00001 diff --git a/test/typechecker/failure/MergeHandlersWithDifferentType.dhallb b/test/typechecker/failure/MergeHandlersWithDifferentType.dhallb new file mode 100644 index 0000000000000000000000000000000000000000..433440a2acde759805202c4e5e69c195d1f26225 GIT binary patch literal 34 pcmZo>YvNdxSkcUw;*_7C!;o0n%$V+%SW;S)n8VP*lUVU}0RYbp44nV~ literal 0 HcmV?d00001 diff --git a/test/typechecker/failure/MergeLhsNotRecord.dhallb b/test/typechecker/failure/MergeLhsNotRecord.dhallb new file mode 100644 index 0000000..fd40d46 --- /dev/null +++ b/test/typechecker/failure/MergeLhsNotRecord.dhallb @@ -0,0 +1 @@ +ƒõ„ axõ  \ No newline at end of file diff --git a/test/typechecker/failure/MergeRhsNotUnion.dhallb b/test/typechecker/failure/MergeRhsNotUnion.dhallb new file mode 100644 index 0000000..ecca354 --- /dev/null +++ b/test/typechecker/failure/MergeRhsNotUnion.dhallb @@ -0,0 +1 @@ +ƒ‚ õ \ No newline at end of file diff --git a/test/typechecker/failure/MergeWithWrongAnnotation.dhallb b/test/typechecker/failure/MergeWithWrongAnnotation.dhallb new file mode 100644 index 0000000000000000000000000000000000000000..bbe9f8cb8a67adcb0a34ab8b0d796986cf65ad1f GIT binary patch literal 29 kcmZo+YvNd#SkcUw;*_7C!_dN$Sn+j1x?f^RX;ESh0G`MTKL7v# literal 0 HcmV?d00001 diff --git a/test/typechecker/failure/RecordMixedKinds.dhallb b/test/typechecker/failure/RecordMixedKinds.dhallb new file mode 100644 index 0000000..98dc39c --- /dev/null +++ b/test/typechecker/failure/RecordMixedKinds.dhallb @@ -0,0 +1 @@ +‚¢ax‚ aydBool \ No newline at end of file diff --git a/test/typechecker/failure/RecordMixedKinds2.dhallb b/test/typechecker/failure/RecordMixedKinds2.dhallb new file mode 100644 index 0000000..12c1665 --- /dev/null +++ b/test/typechecker/failure/RecordMixedKinds2.dhallb @@ -0,0 +1 @@ +‚¢axdTypeay‚  \ No newline at end of file diff --git a/test/typechecker/failure/RecordMixedKinds3.dhallb b/test/typechecker/failure/RecordMixedKinds3.dhallb new file mode 100644 index 0000000..af55b92 --- /dev/null +++ b/test/typechecker/failure/RecordMixedKinds3.dhallb @@ -0,0 +1 @@ +‚¢axdTypeaydKind \ No newline at end of file diff --git a/test/typechecker/failure/RecordProjectionEmpty.dhallb b/test/typechecker/failure/RecordProjectionEmpty.dhallb new file mode 100644 index 0000000..d03755b --- /dev/null +++ b/test/typechecker/failure/RecordProjectionEmpty.dhallb @@ -0,0 +1,2 @@ +ƒ +‚ ax \ No newline at end of file diff --git a/test/typechecker/failure/RecordProjectionNotPresent.dhallb b/test/typechecker/failure/RecordProjectionNotPresent.dhallb new file mode 100644 index 0000000..6803819 --- /dev/null +++ b/test/typechecker/failure/RecordProjectionNotPresent.dhallb @@ -0,0 +1,2 @@ +ƒ +‚¡ay‚ ax \ No newline at end of file diff --git a/test/typechecker/failure/RecordProjectionNotRecord.dhallb b/test/typechecker/failure/RecordProjectionNotRecord.dhallb new file mode 100644 index 0000000..d76137c --- /dev/null +++ b/test/typechecker/failure/RecordProjectionNotRecord.dhallb @@ -0,0 +1,2 @@ +ƒ +õax \ No newline at end of file diff --git a/test/typechecker/failure/RecordSelectionEmpty.dhallb b/test/typechecker/failure/RecordSelectionEmpty.dhallb new file mode 100644 index 0000000..7aa4e6a --- /dev/null +++ b/test/typechecker/failure/RecordSelectionEmpty.dhallb @@ -0,0 +1 @@ +ƒ ‚ ax \ No newline at end of file diff --git a/test/typechecker/failure/RecordSelectionNotPresent.dhallb b/test/typechecker/failure/RecordSelectionNotPresent.dhallb new file mode 100644 index 0000000..97a3c73 --- /dev/null +++ b/test/typechecker/failure/RecordSelectionNotPresent.dhallb @@ -0,0 +1 @@ +ƒ ‚¡ay‚ ax \ No newline at end of file diff --git a/test/typechecker/failure/RecordSelectionNotRecord.dhallb b/test/typechecker/failure/RecordSelectionNotRecord.dhallb new file mode 100644 index 0000000..2e8d4f9 --- /dev/null +++ b/test/typechecker/failure/RecordSelectionNotRecord.dhallb @@ -0,0 +1 @@ +ƒ õax \ No newline at end of file diff --git a/test/typechecker/failure/RecordTypeMixedKinds.dhallb b/test/typechecker/failure/RecordTypeMixedKinds.dhallb new file mode 100644 index 0000000..5254dc6 --- /dev/null +++ b/test/typechecker/failure/RecordTypeMixedKinds.dhallb @@ -0,0 +1 @@ +‚¢axdBoolaydType \ No newline at end of file diff --git a/test/typechecker/failure/RecordTypeMixedKinds2.dhallb b/test/typechecker/failure/RecordTypeMixedKinds2.dhallb new file mode 100644 index 0000000..0af3480 --- /dev/null +++ b/test/typechecker/failure/RecordTypeMixedKinds2.dhallb @@ -0,0 +1 @@ +‚¢axdKindaydType \ No newline at end of file diff --git a/test/typechecker/failure/RecordTypeMixedKinds3.dhallb b/test/typechecker/failure/RecordTypeMixedKinds3.dhallb new file mode 100644 index 0000000..ba991d0 --- /dev/null +++ b/test/typechecker/failure/RecordTypeMixedKinds3.dhallb @@ -0,0 +1 @@ +‚¢axdKindaydBool \ No newline at end of file diff --git a/test/typechecker/failure/RecordTypeValueMember.dhallb b/test/typechecker/failure/RecordTypeValueMember.dhallb new file mode 100644 index 0000000..70249d1 --- /dev/null +++ b/test/typechecker/failure/RecordTypeValueMember.dhallb @@ -0,0 +1 @@ +‚¡axõ \ No newline at end of file diff --git a/test/typechecker/failure/RecursiveRecordMergeLhsNotRecord.dhallb b/test/typechecker/failure/RecursiveRecordMergeLhsNotRecord.dhallb new file mode 100644 index 0000000..65d4b73 --- /dev/null +++ b/test/typechecker/failure/RecursiveRecordMergeLhsNotRecord.dhallb @@ -0,0 +1 @@ +„õ‚  \ No newline at end of file diff --git a/test/typechecker/failure/RecursiveRecordMergeMixedKinds.dhallb b/test/typechecker/failure/RecursiveRecordMergeMixedKinds.dhallb new file mode 100644 index 0000000..69f9ca6 --- /dev/null +++ b/test/typechecker/failure/RecursiveRecordMergeMixedKinds.dhallb @@ -0,0 +1 @@ +„‚¡axõ‚¡aydBool \ No newline at end of file diff --git a/test/typechecker/failure/RecursiveRecordMergeOverlapping.dhallb b/test/typechecker/failure/RecursiveRecordMergeOverlapping.dhallb new file mode 100644 index 0000000..29d093e --- /dev/null +++ b/test/typechecker/failure/RecursiveRecordMergeOverlapping.dhallb @@ -0,0 +1 @@ +„‚¡axõ‚¡axô \ No newline at end of file diff --git a/test/typechecker/failure/RecursiveRecordMergeRhsNotRecord.dhallb b/test/typechecker/failure/RecursiveRecordMergeRhsNotRecord.dhallb new file mode 100644 index 0000000..a73b23b --- /dev/null +++ b/test/typechecker/failure/RecursiveRecordMergeRhsNotRecord.dhallb @@ -0,0 +1 @@ +„‚ õ \ No newline at end of file diff --git a/test/typechecker/failure/RecursiveRecordTypeMergeLhsNotRecordType.dhallb b/test/typechecker/failure/RecursiveRecordTypeMergeLhsNotRecordType.dhallb new file mode 100644 index 0000000..08663c3 --- /dev/null +++ b/test/typechecker/failure/RecursiveRecordTypeMergeLhsNotRecordType.dhallb @@ -0,0 +1,2 @@ +„ +dBool‚  \ No newline at end of file diff --git a/test/typechecker/failure/RecursiveRecordTypeMergeOverlapping.dhallb b/test/typechecker/failure/RecursiveRecordTypeMergeOverlapping.dhallb new file mode 100644 index 0000000..6210523 --- /dev/null +++ b/test/typechecker/failure/RecursiveRecordTypeMergeOverlapping.dhallb @@ -0,0 +1,2 @@ +„ +‚¡axdBool‚¡axgNatural \ No newline at end of file diff --git a/test/typechecker/failure/RecursiveRecordTypeMergeRhsNotRecordType.dhallb b/test/typechecker/failure/RecursiveRecordTypeMergeRhsNotRecordType.dhallb new file mode 100644 index 0000000..66c3a19 --- /dev/null +++ b/test/typechecker/failure/RecursiveRecordTypeMergeRhsNotRecordType.dhallb @@ -0,0 +1,2 @@ +„ +‚ dBool \ No newline at end of file diff --git a/test/typechecker/failure/RightBiasedRecordMergeLhsNotRecord.dhallb b/test/typechecker/failure/RightBiasedRecordMergeLhsNotRecord.dhallb new file mode 100644 index 0000000..9440dbe --- /dev/null +++ b/test/typechecker/failure/RightBiasedRecordMergeLhsNotRecord.dhallb @@ -0,0 +1 @@ +„ õ‚  \ No newline at end of file diff --git a/test/typechecker/failure/RightBiasedRecordMergeMixedKinds.dhallb b/test/typechecker/failure/RightBiasedRecordMergeMixedKinds.dhallb new file mode 100644 index 0000000..3ff3410 --- /dev/null +++ b/test/typechecker/failure/RightBiasedRecordMergeMixedKinds.dhallb @@ -0,0 +1 @@ +„ ‚¡ax‚ ‚¡axdBool \ No newline at end of file diff --git a/test/typechecker/failure/RightBiasedRecordMergeMixedKinds2.dhallb b/test/typechecker/failure/RightBiasedRecordMergeMixedKinds2.dhallb new file mode 100644 index 0000000..6ac2393 --- /dev/null +++ b/test/typechecker/failure/RightBiasedRecordMergeMixedKinds2.dhallb @@ -0,0 +1 @@ +„ ‚¡axdBool‚¡axdKind \ No newline at end of file diff --git a/test/typechecker/failure/RightBiasedRecordMergeMixedKinds3.dhallb b/test/typechecker/failure/RightBiasedRecordMergeMixedKinds3.dhallb new file mode 100644 index 0000000..76f061a --- /dev/null +++ b/test/typechecker/failure/RightBiasedRecordMergeMixedKinds3.dhallb @@ -0,0 +1 @@ +„ ‚¡ax‚ ‚¡axdKind \ No newline at end of file diff --git a/test/typechecker/failure/RightBiasedRecordMergeRhsNotRecord.dhallb b/test/typechecker/failure/RightBiasedRecordMergeRhsNotRecord.dhallb new file mode 100644 index 0000000..b4a1af1 --- /dev/null +++ b/test/typechecker/failure/RightBiasedRecordMergeRhsNotRecord.dhallb @@ -0,0 +1 @@ +„ ‚ õ \ No newline at end of file diff --git a/test/typechecker/failure/SomeNotType.dhallb b/test/typechecker/failure/SomeNotType.dhallb new file mode 100644 index 0000000..d1238b2 --- /dev/null +++ b/test/typechecker/failure/SomeNotType.dhallb @@ -0,0 +1 @@ +ƒödBool \ No newline at end of file diff --git a/test/typechecker/failure/TypeAnnotationWrong.dhallb b/test/typechecker/failure/TypeAnnotationWrong.dhallb new file mode 100644 index 0000000..c8cd318 --- /dev/null +++ b/test/typechecker/failure/TypeAnnotationWrong.dhallb @@ -0,0 +1 @@ +ƒ‚dBool \ No newline at end of file diff --git a/test/typechecker/failure/UnionConstructorFieldNotPresent.dhallb b/test/typechecker/failure/UnionConstructorFieldNotPresent.dhallb new file mode 100644 index 0000000..83070a3 --- /dev/null +++ b/test/typechecker/failure/UnionConstructorFieldNotPresent.dhallb @@ -0,0 +1 @@ +ƒ ‚ ¡axdBoolay \ No newline at end of file diff --git a/test/typechecker/failure/UnionTypeMixedKinds.dhallb b/test/typechecker/failure/UnionTypeMixedKinds.dhallb new file mode 100644 index 0000000..35e62d1 --- /dev/null +++ b/test/typechecker/failure/UnionTypeMixedKinds.dhallb @@ -0,0 +1 @@ +‚ ¢axdBoolaydType \ No newline at end of file diff --git a/test/typechecker/failure/UnionTypeMixedKinds2.dhallb b/test/typechecker/failure/UnionTypeMixedKinds2.dhallb new file mode 100644 index 0000000..56f72bc --- /dev/null +++ b/test/typechecker/failure/UnionTypeMixedKinds2.dhallb @@ -0,0 +1 @@ +‚ ¢axdKindaydType \ No newline at end of file diff --git a/test/typechecker/failure/UnionTypeMixedKinds3.dhallb b/test/typechecker/failure/UnionTypeMixedKinds3.dhallb new file mode 100644 index 0000000..2262325 --- /dev/null +++ b/test/typechecker/failure/UnionTypeMixedKinds3.dhallb @@ -0,0 +1 @@ +‚ ¢axdKindaydBool \ No newline at end of file diff --git a/test/typechecker/failure/UnionTypeNotType.dhallb b/test/typechecker/failure/UnionTypeNotType.dhallb new file mode 100644 index 0000000..cec9f6e --- /dev/null +++ b/test/typechecker/failure/UnionTypeNotType.dhallb @@ -0,0 +1 @@ +‚ ¡axõ \ No newline at end of file diff --git a/test/typechecker/gen b/test/typechecker/gen new file mode 100755 index 0000000..ce6ddaf --- /dev/null +++ b/test/typechecker/gen @@ -0,0 +1,10 @@ +#!/bin/sh + +cp -r "$(git root)"/dhall-lang/tests/typecheck/success "$(git root)"/test/typechecker/success/standard +cp -r "$(git root)"/dhall-lang/tests/typecheck/failure "$(git root)"/test/typechecker/failure/standard + +cd "$(git root)"/test/typechecker/success/standard +find . -name '*.dhall' -exec "$(git root)"/test/normalization/dhall-encode '{}' \; + +cd "$(git root)"/test/typechecker/failure/standard +find . -name '*.dhall' -exec "$(git root)"/test/normalization/dhall-encode '{}' \; diff --git a/test/typechecker/success/DoubleA.dhallb b/test/typechecker/success/DoubleA.dhallb new file mode 100644 index 0000000..800d4fd --- /dev/null +++ b/test/typechecker/success/DoubleA.dhallb @@ -0,0 +1 @@ +fDouble \ No newline at end of file diff --git a/test/typechecker/success/DoubleB.dhallb b/test/typechecker/success/DoubleB.dhallb new file mode 100644 index 0000000..0533f44 --- /dev/null +++ b/test/typechecker/success/DoubleB.dhallb @@ -0,0 +1 @@ +dType \ No newline at end of file diff --git a/test/typechecker/success/DoubleLiteralA.dhallb b/test/typechecker/success/DoubleLiteralA.dhallb new file mode 100644 index 0000000000000000000000000000000000000000..64b893274f3a9621f447d111e1bc61dec67f5253 GIT binary patch literal 5 Mcmexm-@w2C00(0Mx&QzG literal 0 HcmV?d00001 diff --git a/test/typechecker/success/DoubleLiteralB.dhallb b/test/typechecker/success/DoubleLiteralB.dhallb new file mode 100644 index 0000000..800d4fd --- /dev/null +++ b/test/typechecker/success/DoubleLiteralB.dhallb @@ -0,0 +1 @@ +fDouble \ No newline at end of file diff --git a/test/typechecker/success/DoubleShowA.dhallb b/test/typechecker/success/DoubleShowA.dhallb new file mode 100644 index 0000000..c7a21ec --- /dev/null +++ b/test/typechecker/success/DoubleShowA.dhallb @@ -0,0 +1 @@ +kDouble/show \ No newline at end of file diff --git a/test/typechecker/success/DoubleShowB.dhallb b/test/typechecker/success/DoubleShowB.dhallb new file mode 100644 index 0000000..f39579c --- /dev/null +++ b/test/typechecker/success/DoubleShowB.dhallb @@ -0,0 +1 @@ +ƒfDoubledText \ No newline at end of file diff --git a/test/typechecker/success/FunctionA.dhallb b/test/typechecker/success/FunctionA.dhallb new file mode 100644 index 0000000000000000000000000000000000000000..bb2a4a669336041074bdae4e718c69bc7727b4cb GIT binary patch literal 8 PcmZo>OmWK3&tU)n3#tNj literal 0 HcmV?d00001 diff --git a/test/typechecker/success/FunctionApplicationA.dhallb b/test/typechecker/success/FunctionApplicationA.dhallb new file mode 100644 index 0000000000000000000000000000000000000000..73b4d7fcf64cb098f91a1107ce81d0ad3263e71a GIT binary patch literal 11 ScmZo>Xl6`t%FoYX_zD0Nw*&0} literal 0 HcmV?d00001 diff --git a/test/typechecker/success/FunctionApplicationB.dhallb b/test/typechecker/success/FunctionApplicationB.dhallb new file mode 100644 index 0000000..c418df5 --- /dev/null +++ b/test/typechecker/success/FunctionApplicationB.dhallb @@ -0,0 +1 @@ +dBool \ No newline at end of file diff --git a/test/typechecker/success/FunctionB.dhallb b/test/typechecker/success/FunctionB.dhallb new file mode 100644 index 0000000..7d37b4c --- /dev/null +++ b/test/typechecker/success/FunctionB.dhallb @@ -0,0 +1 @@ +ƒdBooldBool \ No newline at end of file diff --git a/test/typechecker/success/FunctionNamedArgA.dhallb b/test/typechecker/success/FunctionNamedArgA.dhallb new file mode 100644 index 0000000..c4edf3c --- /dev/null +++ b/test/typechecker/success/FunctionNamedArgA.dhallb @@ -0,0 +1 @@ +„axdBoolax \ No newline at end of file diff --git a/test/typechecker/success/FunctionNamedArgB.dhallb b/test/typechecker/success/FunctionNamedArgB.dhallb new file mode 100644 index 0000000..ff75af6 --- /dev/null +++ b/test/typechecker/success/FunctionNamedArgB.dhallb @@ -0,0 +1 @@ +„axdBooldBool \ No newline at end of file diff --git a/test/typechecker/success/FunctionTypeKindKindA.dhallb b/test/typechecker/success/FunctionTypeKindKindA.dhallb new file mode 100644 index 0000000..9513da7 --- /dev/null +++ b/test/typechecker/success/FunctionTypeKindKindA.dhallb @@ -0,0 +1 @@ +ƒdKinddKind \ No newline at end of file diff --git a/test/typechecker/success/FunctionTypeKindKindB.dhallb b/test/typechecker/success/FunctionTypeKindKindB.dhallb new file mode 100644 index 0000000..5ca4cc6 --- /dev/null +++ b/test/typechecker/success/FunctionTypeKindKindB.dhallb @@ -0,0 +1 @@ +dSort \ No newline at end of file diff --git a/test/typechecker/success/FunctionTypeKindTermA.dhallb b/test/typechecker/success/FunctionTypeKindTermA.dhallb new file mode 100644 index 0000000..6b122a6 --- /dev/null +++ b/test/typechecker/success/FunctionTypeKindTermA.dhallb @@ -0,0 +1 @@ +ƒdKinddBool \ No newline at end of file diff --git a/test/typechecker/success/FunctionTypeKindTermB.dhallb b/test/typechecker/success/FunctionTypeKindTermB.dhallb new file mode 100644 index 0000000..0533f44 --- /dev/null +++ b/test/typechecker/success/FunctionTypeKindTermB.dhallb @@ -0,0 +1 @@ +dType \ No newline at end of file diff --git a/test/typechecker/success/FunctionTypeKindTypeA.dhallb b/test/typechecker/success/FunctionTypeKindTypeA.dhallb new file mode 100644 index 0000000..43dabe8 --- /dev/null +++ b/test/typechecker/success/FunctionTypeKindTypeA.dhallb @@ -0,0 +1 @@ +ƒdKinddType \ No newline at end of file diff --git a/test/typechecker/success/FunctionTypeKindTypeB.dhallb b/test/typechecker/success/FunctionTypeKindTypeB.dhallb new file mode 100644 index 0000000..5ca4cc6 --- /dev/null +++ b/test/typechecker/success/FunctionTypeKindTypeB.dhallb @@ -0,0 +1 @@ +dSort \ No newline at end of file diff --git a/test/typechecker/success/FunctionTypeTermTermA.dhallb b/test/typechecker/success/FunctionTypeTermTermA.dhallb new file mode 100644 index 0000000..7d37b4c --- /dev/null +++ b/test/typechecker/success/FunctionTypeTermTermA.dhallb @@ -0,0 +1 @@ +ƒdBooldBool \ No newline at end of file diff --git a/test/typechecker/success/FunctionTypeTermTermB.dhallb b/test/typechecker/success/FunctionTypeTermTermB.dhallb new file mode 100644 index 0000000..0533f44 --- /dev/null +++ b/test/typechecker/success/FunctionTypeTermTermB.dhallb @@ -0,0 +1 @@ +dType \ No newline at end of file diff --git a/test/typechecker/success/FunctionTypeTypeTermA.dhallb b/test/typechecker/success/FunctionTypeTypeTermA.dhallb new file mode 100644 index 0000000..28ddf55 --- /dev/null +++ b/test/typechecker/success/FunctionTypeTypeTermA.dhallb @@ -0,0 +1 @@ +ƒdTypedBool \ No newline at end of file diff --git a/test/typechecker/success/FunctionTypeTypeTermB.dhallb b/test/typechecker/success/FunctionTypeTypeTermB.dhallb new file mode 100644 index 0000000..0533f44 --- /dev/null +++ b/test/typechecker/success/FunctionTypeTypeTermB.dhallb @@ -0,0 +1 @@ +dType \ No newline at end of file diff --git a/test/typechecker/success/FunctionTypeTypeTypeA.dhallb b/test/typechecker/success/FunctionTypeTypeTypeA.dhallb new file mode 100644 index 0000000..d98e47d --- /dev/null +++ b/test/typechecker/success/FunctionTypeTypeTypeA.dhallb @@ -0,0 +1 @@ +ƒdTypedType \ No newline at end of file diff --git a/test/typechecker/success/FunctionTypeTypeTypeB.dhallb b/test/typechecker/success/FunctionTypeTypeTypeB.dhallb new file mode 100644 index 0000000..9d1177c --- /dev/null +++ b/test/typechecker/success/FunctionTypeTypeTypeB.dhallb @@ -0,0 +1 @@ +dKind \ No newline at end of file diff --git a/test/typechecker/success/FunctionTypeUsingArgumentA.dhallb b/test/typechecker/success/FunctionTypeUsingArgumentA.dhallb new file mode 100644 index 0000000000000000000000000000000000000000..3907892fc104fed3fa822680a0017115b8548e0f GIT binary patch literal 8 PcmZo>N(refNM!&33@8GO literal 0 HcmV?d00001 diff --git a/test/typechecker/success/FunctionTypeUsingArgumentB.dhallb b/test/typechecker/success/FunctionTypeUsingArgumentB.dhallb new file mode 100644 index 0000000..0533f44 --- /dev/null +++ b/test/typechecker/success/FunctionTypeUsingArgumentB.dhallb @@ -0,0 +1 @@ +dType \ No newline at end of file diff --git a/test/typechecker/success/IntegerA.dhallb b/test/typechecker/success/IntegerA.dhallb new file mode 100644 index 0000000..9e85af5 --- /dev/null +++ b/test/typechecker/success/IntegerA.dhallb @@ -0,0 +1 @@ +gInteger \ No newline at end of file diff --git a/test/typechecker/success/IntegerB.dhallb b/test/typechecker/success/IntegerB.dhallb new file mode 100644 index 0000000..0533f44 --- /dev/null +++ b/test/typechecker/success/IntegerB.dhallb @@ -0,0 +1 @@ +dType \ No newline at end of file diff --git a/test/typechecker/success/IntegerLiteralA.dhallb b/test/typechecker/success/IntegerLiteralA.dhallb new file mode 100644 index 0000000..dc4c19f --- /dev/null +++ b/test/typechecker/success/IntegerLiteralA.dhallb @@ -0,0 +1 @@ +‚ \ No newline at end of file diff --git a/test/typechecker/success/IntegerLiteralB.dhallb b/test/typechecker/success/IntegerLiteralB.dhallb new file mode 100644 index 0000000..9e85af5 --- /dev/null +++ b/test/typechecker/success/IntegerLiteralB.dhallb @@ -0,0 +1 @@ +gInteger \ No newline at end of file diff --git a/test/typechecker/success/IntegerShowA.dhallb b/test/typechecker/success/IntegerShowA.dhallb new file mode 100644 index 0000000..ffbc424 --- /dev/null +++ b/test/typechecker/success/IntegerShowA.dhallb @@ -0,0 +1 @@ +lInteger/show \ No newline at end of file diff --git a/test/typechecker/success/IntegerShowB.dhallb b/test/typechecker/success/IntegerShowB.dhallb new file mode 100644 index 0000000..60808ed --- /dev/null +++ b/test/typechecker/success/IntegerShowB.dhallb @@ -0,0 +1 @@ +ƒgIntegerdText \ No newline at end of file diff --git a/test/typechecker/success/IntegerToDoubleA.dhallb b/test/typechecker/success/IntegerToDoubleA.dhallb new file mode 100644 index 0000000..89b4696 --- /dev/null +++ b/test/typechecker/success/IntegerToDoubleA.dhallb @@ -0,0 +1 @@ +pInteger/toDouble \ No newline at end of file diff --git a/test/typechecker/success/IntegerToDoubleB.dhallb b/test/typechecker/success/IntegerToDoubleB.dhallb new file mode 100644 index 0000000..cc9f9b1 --- /dev/null +++ b/test/typechecker/success/IntegerToDoubleB.dhallb @@ -0,0 +1 @@ +ƒgIntegerfDouble \ No newline at end of file diff --git a/test/typechecker/success/LetA.dhallb b/test/typechecker/success/LetA.dhallb new file mode 100644 index 0000000..777994c --- /dev/null +++ b/test/typechecker/success/LetA.dhallb @@ -0,0 +1 @@ +…axöõax \ No newline at end of file diff --git a/test/typechecker/success/LetB.dhallb b/test/typechecker/success/LetB.dhallb new file mode 100644 index 0000000..c418df5 --- /dev/null +++ b/test/typechecker/success/LetB.dhallb @@ -0,0 +1 @@ +dBool \ No newline at end of file diff --git a/test/typechecker/success/LetNestedTypeSynonymA.dhallb b/test/typechecker/success/LetNestedTypeSynonymA.dhallb new file mode 100644 index 0000000..0805ab7 --- /dev/null +++ b/test/typechecker/success/LetNestedTypeSynonymA.dhallb @@ -0,0 +1 @@ +ˆaxödBoolayaxõay \ No newline at end of file diff --git a/test/typechecker/success/LetNestedTypeSynonymB.dhallb b/test/typechecker/success/LetNestedTypeSynonymB.dhallb new file mode 100644 index 0000000..c418df5 --- /dev/null +++ b/test/typechecker/success/LetNestedTypeSynonymB.dhallb @@ -0,0 +1 @@ +dBool \ No newline at end of file diff --git a/test/typechecker/success/LetTypeSynonymA.dhallb b/test/typechecker/success/LetTypeSynonymA.dhallb new file mode 100644 index 0000000..2bfef43 --- /dev/null +++ b/test/typechecker/success/LetTypeSynonymA.dhallb @@ -0,0 +1 @@ +…axödBoolƒõax \ No newline at end of file diff --git a/test/typechecker/success/LetTypeSynonymB.dhallb b/test/typechecker/success/LetTypeSynonymB.dhallb new file mode 100644 index 0000000..c418df5 --- /dev/null +++ b/test/typechecker/success/LetTypeSynonymB.dhallb @@ -0,0 +1 @@ +dBool \ No newline at end of file diff --git a/test/typechecker/success/LetWithAnnotationA.dhallb b/test/typechecker/success/LetWithAnnotationA.dhallb new file mode 100644 index 0000000..b56e78e --- /dev/null +++ b/test/typechecker/success/LetWithAnnotationA.dhallb @@ -0,0 +1 @@ +…axdBoolõax \ No newline at end of file diff --git a/test/typechecker/success/LetWithAnnotationB.dhallb b/test/typechecker/success/LetWithAnnotationB.dhallb new file mode 100644 index 0000000..c418df5 --- /dev/null +++ b/test/typechecker/success/LetWithAnnotationB.dhallb @@ -0,0 +1 @@ +dBool \ No newline at end of file diff --git a/test/typechecker/success/MergeEmptyUnionA.dhallb b/test/typechecker/success/MergeEmptyUnionA.dhallb new file mode 100644 index 0000000..11d6251 --- /dev/null +++ b/test/typechecker/success/MergeEmptyUnionA.dhallb @@ -0,0 +1 @@ +„ax‚  „‚ axdBool \ No newline at end of file diff --git a/test/typechecker/success/MergeEmptyUnionB.dhallb b/test/typechecker/success/MergeEmptyUnionB.dhallb new file mode 100644 index 0000000..7760698 --- /dev/null +++ b/test/typechecker/success/MergeEmptyUnionB.dhallb @@ -0,0 +1 @@ +„ax‚  dBool \ No newline at end of file diff --git a/test/typechecker/success/MergeOneA.dhallb b/test/typechecker/success/MergeOneA.dhallb new file mode 100644 index 0000000000000000000000000000000000000000..409a798c0e85f4c75b572a845f6e404651297103 GIT binary patch literal 21 ccmZo>YvNd#SkcUw;*_7C!_dN$Sn+iM08noT00000 literal 0 HcmV?d00001 diff --git a/test/typechecker/success/MergeOneB.dhallb b/test/typechecker/success/MergeOneB.dhallb new file mode 100644 index 0000000..c418df5 --- /dev/null +++ b/test/typechecker/success/MergeOneB.dhallb @@ -0,0 +1 @@ +dBool \ No newline at end of file diff --git a/test/typechecker/success/MergeOneWithAnnotationA.dhallb b/test/typechecker/success/MergeOneWithAnnotationA.dhallb new file mode 100644 index 0000000000000000000000000000000000000000..47870518004444563bd0d41d7377ab212ebf788d GIT binary patch literal 26 ecmZo+YvNd#SkcUw;*_7C!_dN$Sn+iMm<<4a90~CN literal 0 HcmV?d00001 diff --git a/test/typechecker/success/MergeOneWithAnnotationB.dhallb b/test/typechecker/success/MergeOneWithAnnotationB.dhallb new file mode 100644 index 0000000..c418df5 --- /dev/null +++ b/test/typechecker/success/MergeOneWithAnnotationB.dhallb @@ -0,0 +1 @@ +dBool \ No newline at end of file diff --git a/test/typechecker/success/NoneA.dhallb b/test/typechecker/success/NoneA.dhallb new file mode 100644 index 0000000..8b46e48 --- /dev/null +++ b/test/typechecker/success/NoneA.dhallb @@ -0,0 +1 @@ +dNone \ No newline at end of file diff --git a/test/typechecker/success/NoneB.dhallb b/test/typechecker/success/NoneB.dhallb new file mode 100644 index 0000000000000000000000000000000000000000..85438b7f681ea8db313fd0de148d4b8bde21f4e3 GIT binary patch literal 22 dcmZo+N_0#KsVqosX2|d_D9OyvOUy}h1OQoZ2m$~A literal 0 HcmV?d00001 diff --git a/test/typechecker/success/OldOptionalNoneA.dhallb b/test/typechecker/success/OldOptionalNoneA.dhallb new file mode 100644 index 0000000..92ce508 --- /dev/null +++ b/test/typechecker/success/OldOptionalNoneA.dhallb @@ -0,0 +1 @@ +‚dBool \ No newline at end of file diff --git a/test/typechecker/success/OldOptionalNoneB.dhallb b/test/typechecker/success/OldOptionalNoneB.dhallb new file mode 100644 index 0000000000000000000000000000000000000000..b9ded578d26af23894fb0e59ec8f30f873de5fd6 GIT binary patch literal 16 XcmZo>$nY;H$;{77%t>*|&(8q>GGYcI literal 0 HcmV?d00001 diff --git a/test/typechecker/success/OldOptionalTrueA.dhallb b/test/typechecker/success/OldOptionalTrueA.dhallb new file mode 100644 index 0000000..ac562af --- /dev/null +++ b/test/typechecker/success/OldOptionalTrueA.dhallb @@ -0,0 +1 @@ +ƒdBoolõ \ No newline at end of file diff --git a/test/typechecker/success/OldOptionalTrueB.dhallb b/test/typechecker/success/OldOptionalTrueB.dhallb new file mode 100644 index 0000000000000000000000000000000000000000..b9ded578d26af23894fb0e59ec8f30f873de5fd6 GIT binary patch literal 16 XcmZo>$nY;H$;{77%t>*|&(8q>GGYcI literal 0 HcmV?d00001 diff --git a/test/typechecker/success/OptionalA.dhallb b/test/typechecker/success/OptionalA.dhallb new file mode 100644 index 0000000..ba21fbe --- /dev/null +++ b/test/typechecker/success/OptionalA.dhallb @@ -0,0 +1 @@ +hOptional \ No newline at end of file diff --git a/test/typechecker/success/OptionalB.dhallb b/test/typechecker/success/OptionalB.dhallb new file mode 100644 index 0000000..d98e47d --- /dev/null +++ b/test/typechecker/success/OptionalB.dhallb @@ -0,0 +1 @@ +ƒdTypedType \ No newline at end of file diff --git a/test/typechecker/success/OptionalBuildA.dhallb b/test/typechecker/success/OptionalBuildA.dhallb new file mode 100644 index 0000000..9c1bfee --- /dev/null +++ b/test/typechecker/success/OptionalBuildA.dhallb @@ -0,0 +1 @@ +nOptional/build \ No newline at end of file diff --git a/test/typechecker/success/OptionalBuildB.dhallb b/test/typechecker/success/OptionalBuildB.dhallb new file mode 100644 index 0000000000000000000000000000000000000000..a52107c2fbff24b653c8b6c456122959c2e59748 GIT binary patch literal 88 zcmZo+N=!@%sVqosW@=%|$S)|#%+E{A0gJRSrDT;Bmox)az$IFk()035GBWeh;X-gm MGed?yRDWV30Nr#VW&i*H literal 0 HcmV?d00001 diff --git a/test/typechecker/success/OptionalFoldA.dhallb b/test/typechecker/success/OptionalFoldA.dhallb new file mode 100644 index 0000000..df18fa4 --- /dev/null +++ b/test/typechecker/success/OptionalFoldA.dhallb @@ -0,0 +1 @@ +mOptional/fold \ No newline at end of file diff --git a/test/typechecker/success/OptionalFoldB.dhallb b/test/typechecker/success/OptionalFoldB.dhallb new file mode 100644 index 0000000000000000000000000000000000000000..dde78130af3ca31799acd988829e97882a0f91b6 GIT binary patch literal 88 zcmZo+N=!@%sVqosW@={0@GmII%+E{ANla{E%E*Uuz|t*DDOsh(CCxzPaETVC^t}9% MjLf`rxDcEH0L>vHW&i*H literal 0 HcmV?d00001 diff --git a/test/typechecker/success/RecordEmptyA.dhallb b/test/typechecker/success/RecordEmptyA.dhallb new file mode 100644 index 0000000..58e2e39 --- /dev/null +++ b/test/typechecker/success/RecordEmptyA.dhallb @@ -0,0 +1 @@ +‚  \ No newline at end of file diff --git a/test/typechecker/success/RecordEmptyB.dhallb b/test/typechecker/success/RecordEmptyB.dhallb new file mode 100644 index 0000000..f6964c2 --- /dev/null +++ b/test/typechecker/success/RecordEmptyB.dhallb @@ -0,0 +1 @@ +‚  \ No newline at end of file diff --git a/test/typechecker/success/RecordOneKindA.dhallb b/test/typechecker/success/RecordOneKindA.dhallb new file mode 100644 index 0000000..285036e --- /dev/null +++ b/test/typechecker/success/RecordOneKindA.dhallb @@ -0,0 +1 @@ +‚¡axdType \ No newline at end of file diff --git a/test/typechecker/success/RecordOneKindB.dhallb b/test/typechecker/success/RecordOneKindB.dhallb new file mode 100644 index 0000000..83359ae --- /dev/null +++ b/test/typechecker/success/RecordOneKindB.dhallb @@ -0,0 +1 @@ +‚¡axdKind \ No newline at end of file diff --git a/test/typechecker/success/RecordOneTypeA.dhallb b/test/typechecker/success/RecordOneTypeA.dhallb new file mode 100644 index 0000000..44a214b --- /dev/null +++ b/test/typechecker/success/RecordOneTypeA.dhallb @@ -0,0 +1 @@ +‚¡ax‚  \ No newline at end of file diff --git a/test/typechecker/success/RecordOneTypeB.dhallb b/test/typechecker/success/RecordOneTypeB.dhallb new file mode 100644 index 0000000..32ae7cb --- /dev/null +++ b/test/typechecker/success/RecordOneTypeB.dhallb @@ -0,0 +1 @@ +‚¡axdType \ No newline at end of file diff --git a/test/typechecker/success/RecordOneValueA.dhallb b/test/typechecker/success/RecordOneValueA.dhallb new file mode 100644 index 0000000..539a424 --- /dev/null +++ b/test/typechecker/success/RecordOneValueA.dhallb @@ -0,0 +1 @@ +‚¡ax‚  \ No newline at end of file diff --git a/test/typechecker/success/RecordOneValueB.dhallb b/test/typechecker/success/RecordOneValueB.dhallb new file mode 100644 index 0000000..e3965ac --- /dev/null +++ b/test/typechecker/success/RecordOneValueB.dhallb @@ -0,0 +1 @@ +‚¡ax‚  \ No newline at end of file diff --git a/test/typechecker/success/RecordProjectionEmptyA.dhallb b/test/typechecker/success/RecordProjectionEmptyA.dhallb new file mode 100644 index 0000000..fbc5c62 --- /dev/null +++ b/test/typechecker/success/RecordProjectionEmptyA.dhallb @@ -0,0 +1,2 @@ +‚ +‚¡ax‚  \ No newline at end of file diff --git a/test/typechecker/success/RecordProjectionEmptyB.dhallb b/test/typechecker/success/RecordProjectionEmptyB.dhallb new file mode 100644 index 0000000..f6964c2 --- /dev/null +++ b/test/typechecker/success/RecordProjectionEmptyB.dhallb @@ -0,0 +1 @@ +‚  \ No newline at end of file diff --git a/test/typechecker/success/RecordProjectionKindA.dhallb b/test/typechecker/success/RecordProjectionKindA.dhallb new file mode 100644 index 0000000..ac508a6 --- /dev/null +++ b/test/typechecker/success/RecordProjectionKindA.dhallb @@ -0,0 +1,2 @@ +ƒ +‚¢axdTypeaydTypeax \ No newline at end of file diff --git a/test/typechecker/success/RecordProjectionKindB.dhallb b/test/typechecker/success/RecordProjectionKindB.dhallb new file mode 100644 index 0000000..83359ae --- /dev/null +++ b/test/typechecker/success/RecordProjectionKindB.dhallb @@ -0,0 +1 @@ +‚¡axdKind \ No newline at end of file diff --git a/test/typechecker/success/RecordProjectionTypeA.dhallb b/test/typechecker/success/RecordProjectionTypeA.dhallb new file mode 100644 index 0000000..e14b89c --- /dev/null +++ b/test/typechecker/success/RecordProjectionTypeA.dhallb @@ -0,0 +1,2 @@ +ƒ +‚¢axdBoolaygNaturalax \ No newline at end of file diff --git a/test/typechecker/success/RecordProjectionTypeB.dhallb b/test/typechecker/success/RecordProjectionTypeB.dhallb new file mode 100644 index 0000000..32ae7cb --- /dev/null +++ b/test/typechecker/success/RecordProjectionTypeB.dhallb @@ -0,0 +1 @@ +‚¡axdType \ No newline at end of file diff --git a/test/typechecker/success/RecordProjectionValueA.dhallb b/test/typechecker/success/RecordProjectionValueA.dhallb new file mode 100644 index 0000000..912e929 --- /dev/null +++ b/test/typechecker/success/RecordProjectionValueA.dhallb @@ -0,0 +1,2 @@ +ƒ +‚¢ax‚ ay‚ ax \ No newline at end of file diff --git a/test/typechecker/success/RecordProjectionValueB.dhallb b/test/typechecker/success/RecordProjectionValueB.dhallb new file mode 100644 index 0000000..e3965ac --- /dev/null +++ b/test/typechecker/success/RecordProjectionValueB.dhallb @@ -0,0 +1 @@ +‚¡ax‚  \ No newline at end of file diff --git a/test/typechecker/success/RecordSelectionKindA.dhallb b/test/typechecker/success/RecordSelectionKindA.dhallb new file mode 100644 index 0000000..db365eb --- /dev/null +++ b/test/typechecker/success/RecordSelectionKindA.dhallb @@ -0,0 +1 @@ +ƒ ‚¡axdTypeax \ No newline at end of file diff --git a/test/typechecker/success/RecordSelectionKindB.dhallb b/test/typechecker/success/RecordSelectionKindB.dhallb new file mode 100644 index 0000000..9d1177c --- /dev/null +++ b/test/typechecker/success/RecordSelectionKindB.dhallb @@ -0,0 +1 @@ +dKind \ No newline at end of file diff --git a/test/typechecker/success/RecordSelectionTypeA.dhallb b/test/typechecker/success/RecordSelectionTypeA.dhallb new file mode 100644 index 0000000..65f6732 --- /dev/null +++ b/test/typechecker/success/RecordSelectionTypeA.dhallb @@ -0,0 +1 @@ +ƒ ‚¡ax‚ ax \ No newline at end of file diff --git a/test/typechecker/success/RecordSelectionTypeB.dhallb b/test/typechecker/success/RecordSelectionTypeB.dhallb new file mode 100644 index 0000000..0533f44 --- /dev/null +++ b/test/typechecker/success/RecordSelectionTypeB.dhallb @@ -0,0 +1 @@ +dType \ No newline at end of file diff --git a/test/typechecker/success/RecordSelectionValueA.dhallb b/test/typechecker/success/RecordSelectionValueA.dhallb new file mode 100644 index 0000000..de5858e --- /dev/null +++ b/test/typechecker/success/RecordSelectionValueA.dhallb @@ -0,0 +1 @@ +ƒ ‚¡ax‚ ax \ No newline at end of file diff --git a/test/typechecker/success/RecordSelectionValueB.dhallb b/test/typechecker/success/RecordSelectionValueB.dhallb new file mode 100644 index 0000000..f6964c2 --- /dev/null +++ b/test/typechecker/success/RecordSelectionValueB.dhallb @@ -0,0 +1 @@ +‚  \ No newline at end of file diff --git a/test/typechecker/success/RecordTypeA.dhallb b/test/typechecker/success/RecordTypeA.dhallb new file mode 100644 index 0000000..cebf88e --- /dev/null +++ b/test/typechecker/success/RecordTypeA.dhallb @@ -0,0 +1 @@ +‚¡axdBool \ No newline at end of file diff --git a/test/typechecker/success/RecordTypeB.dhallb b/test/typechecker/success/RecordTypeB.dhallb new file mode 100644 index 0000000..0533f44 --- /dev/null +++ b/test/typechecker/success/RecordTypeB.dhallb @@ -0,0 +1 @@ +dType \ No newline at end of file diff --git a/test/typechecker/success/RecordTypeEmptyA.dhallb b/test/typechecker/success/RecordTypeEmptyA.dhallb new file mode 100644 index 0000000..f6964c2 --- /dev/null +++ b/test/typechecker/success/RecordTypeEmptyA.dhallb @@ -0,0 +1 @@ +‚  \ No newline at end of file diff --git a/test/typechecker/success/RecordTypeEmptyB.dhallb b/test/typechecker/success/RecordTypeEmptyB.dhallb new file mode 100644 index 0000000..0533f44 --- /dev/null +++ b/test/typechecker/success/RecordTypeEmptyB.dhallb @@ -0,0 +1 @@ +dType \ No newline at end of file diff --git a/test/typechecker/success/RecordTypeKindA.dhallb b/test/typechecker/success/RecordTypeKindA.dhallb new file mode 100644 index 0000000..83359ae --- /dev/null +++ b/test/typechecker/success/RecordTypeKindA.dhallb @@ -0,0 +1 @@ +‚¡axdKind \ No newline at end of file diff --git a/test/typechecker/success/RecordTypeKindB.dhallb b/test/typechecker/success/RecordTypeKindB.dhallb new file mode 100644 index 0000000..5ca4cc6 --- /dev/null +++ b/test/typechecker/success/RecordTypeKindB.dhallb @@ -0,0 +1 @@ +dSort \ No newline at end of file diff --git a/test/typechecker/success/RecordTypeTypeA.dhallb b/test/typechecker/success/RecordTypeTypeA.dhallb new file mode 100644 index 0000000..32ae7cb --- /dev/null +++ b/test/typechecker/success/RecordTypeTypeA.dhallb @@ -0,0 +1 @@ +‚¡axdType \ No newline at end of file diff --git a/test/typechecker/success/RecordTypeTypeB.dhallb b/test/typechecker/success/RecordTypeTypeB.dhallb new file mode 100644 index 0000000..9d1177c --- /dev/null +++ b/test/typechecker/success/RecordTypeTypeB.dhallb @@ -0,0 +1 @@ +dKind \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordMergeLhsEmptyA.dhallb b/test/typechecker/success/RecursiveRecordMergeLhsEmptyA.dhallb new file mode 100644 index 0000000..5624142 --- /dev/null +++ b/test/typechecker/success/RecursiveRecordMergeLhsEmptyA.dhallb @@ -0,0 +1 @@ +„‚ ‚¡axõ \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordMergeLhsEmptyB.dhallb b/test/typechecker/success/RecursiveRecordMergeLhsEmptyB.dhallb new file mode 100644 index 0000000..cebf88e --- /dev/null +++ b/test/typechecker/success/RecursiveRecordMergeLhsEmptyB.dhallb @@ -0,0 +1 @@ +‚¡axdBool \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordMergeRecursivelyA.dhallb b/test/typechecker/success/RecursiveRecordMergeRecursivelyA.dhallb new file mode 100644 index 0000000..48c9845 --- /dev/null +++ b/test/typechecker/success/RecursiveRecordMergeRecursivelyA.dhallb @@ -0,0 +1 @@ +„‚¡ax‚¡aaõ‚¡ax‚¡abõ \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordMergeRecursivelyB.dhallb b/test/typechecker/success/RecursiveRecordMergeRecursivelyB.dhallb new file mode 100644 index 0000000..c43de37 --- /dev/null +++ b/test/typechecker/success/RecursiveRecordMergeRecursivelyB.dhallb @@ -0,0 +1 @@ +‚¡ax‚¢aadBoolabdBool \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordMergeRecursivelyKindsA.dhallb b/test/typechecker/success/RecursiveRecordMergeRecursivelyKindsA.dhallb new file mode 100644 index 0000000..e0669fb --- /dev/null +++ b/test/typechecker/success/RecursiveRecordMergeRecursivelyKindsA.dhallb @@ -0,0 +1 @@ +„‚¡ax‚¡aadType‚¡ax‚¡abdType \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordMergeRecursivelyKindsB.dhallb b/test/typechecker/success/RecursiveRecordMergeRecursivelyKindsB.dhallb new file mode 100644 index 0000000..d637f62 --- /dev/null +++ b/test/typechecker/success/RecursiveRecordMergeRecursivelyKindsB.dhallb @@ -0,0 +1 @@ +‚¡ax‚¢aadKindabdKind \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordMergeRecursivelyTypesA.dhallb b/test/typechecker/success/RecursiveRecordMergeRecursivelyTypesA.dhallb new file mode 100644 index 0000000..584eb8f --- /dev/null +++ b/test/typechecker/success/RecursiveRecordMergeRecursivelyTypesA.dhallb @@ -0,0 +1 @@ +„‚¡ax‚¡aadBool‚¡ax‚¡abgNatural \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordMergeRecursivelyTypesB.dhallb b/test/typechecker/success/RecursiveRecordMergeRecursivelyTypesB.dhallb new file mode 100644 index 0000000..f8894ea --- /dev/null +++ b/test/typechecker/success/RecursiveRecordMergeRecursivelyTypesB.dhallb @@ -0,0 +1 @@ +‚¡ax‚¢aadTypeabdType \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordMergeRhsEmptyA.dhallb b/test/typechecker/success/RecursiveRecordMergeRhsEmptyA.dhallb new file mode 100644 index 0000000..bf403c8 --- /dev/null +++ b/test/typechecker/success/RecursiveRecordMergeRhsEmptyA.dhallb @@ -0,0 +1 @@ +„‚¡axõ‚  \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordMergeRhsEmptyB.dhallb b/test/typechecker/success/RecursiveRecordMergeRhsEmptyB.dhallb new file mode 100644 index 0000000..cebf88e --- /dev/null +++ b/test/typechecker/success/RecursiveRecordMergeRhsEmptyB.dhallb @@ -0,0 +1 @@ +‚¡axdBool \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordMergeTwoA.dhallb b/test/typechecker/success/RecursiveRecordMergeTwoA.dhallb new file mode 100644 index 0000000..70d372c --- /dev/null +++ b/test/typechecker/success/RecursiveRecordMergeTwoA.dhallb @@ -0,0 +1 @@ +„‚¡axõ‚¡ayõ \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordMergeTwoB.dhallb b/test/typechecker/success/RecursiveRecordMergeTwoB.dhallb new file mode 100644 index 0000000..1a4796a --- /dev/null +++ b/test/typechecker/success/RecursiveRecordMergeTwoB.dhallb @@ -0,0 +1 @@ +‚¢axdBoolaydBool \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordMergeTwoKindsA.dhallb b/test/typechecker/success/RecursiveRecordMergeTwoKindsA.dhallb new file mode 100644 index 0000000..a7a00d9 --- /dev/null +++ b/test/typechecker/success/RecursiveRecordMergeTwoKindsA.dhallb @@ -0,0 +1 @@ +„‚¡axdType‚¡aydType \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordMergeTwoKindsB.dhallb b/test/typechecker/success/RecursiveRecordMergeTwoKindsB.dhallb new file mode 100644 index 0000000..3ab6e92 --- /dev/null +++ b/test/typechecker/success/RecursiveRecordMergeTwoKindsB.dhallb @@ -0,0 +1 @@ +‚¢axdKindaydKind \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordMergeTwoTypesA.dhallb b/test/typechecker/success/RecursiveRecordMergeTwoTypesA.dhallb new file mode 100644 index 0000000..3d46bd2 --- /dev/null +++ b/test/typechecker/success/RecursiveRecordMergeTwoTypesA.dhallb @@ -0,0 +1 @@ +„‚¡axdBool‚¡aygNatural \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordMergeTwoTypesB.dhallb b/test/typechecker/success/RecursiveRecordMergeTwoTypesB.dhallb new file mode 100644 index 0000000..0eb7ba6 --- /dev/null +++ b/test/typechecker/success/RecursiveRecordMergeTwoTypesB.dhallb @@ -0,0 +1 @@ +‚¢axdTypeaydType \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordTypeMergeRecursivelyA.dhallb b/test/typechecker/success/RecursiveRecordTypeMergeRecursivelyA.dhallb new file mode 100644 index 0000000..76a40a6 --- /dev/null +++ b/test/typechecker/success/RecursiveRecordTypeMergeRecursivelyA.dhallb @@ -0,0 +1,2 @@ +„ +‚¡ax‚¡aadBool‚¡ay‚¡abdBool \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordTypeMergeRecursivelyB.dhallb b/test/typechecker/success/RecursiveRecordTypeMergeRecursivelyB.dhallb new file mode 100644 index 0000000..0533f44 --- /dev/null +++ b/test/typechecker/success/RecursiveRecordTypeMergeRecursivelyB.dhallb @@ -0,0 +1 @@ +dType \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordTypeMergeRecursivelyKindsA.dhallb b/test/typechecker/success/RecursiveRecordTypeMergeRecursivelyKindsA.dhallb new file mode 100644 index 0000000..07b6f57 --- /dev/null +++ b/test/typechecker/success/RecursiveRecordTypeMergeRecursivelyKindsA.dhallb @@ -0,0 +1,2 @@ +„ +‚¡ax‚¡aadKind‚¡ay‚¡abdKind \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordTypeMergeRecursivelyKindsB.dhallb b/test/typechecker/success/RecursiveRecordTypeMergeRecursivelyKindsB.dhallb new file mode 100644 index 0000000..5ca4cc6 --- /dev/null +++ b/test/typechecker/success/RecursiveRecordTypeMergeRecursivelyKindsB.dhallb @@ -0,0 +1 @@ +dSort \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordTypeMergeRecursivelyTypesA.dhallb b/test/typechecker/success/RecursiveRecordTypeMergeRecursivelyTypesA.dhallb new file mode 100644 index 0000000..02d05b4 --- /dev/null +++ b/test/typechecker/success/RecursiveRecordTypeMergeRecursivelyTypesA.dhallb @@ -0,0 +1,2 @@ +„ +‚¡ax‚¡aadType‚¡ay‚¡abdType \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordTypeMergeRecursivelyTypesB.dhallb b/test/typechecker/success/RecursiveRecordTypeMergeRecursivelyTypesB.dhallb new file mode 100644 index 0000000..9d1177c --- /dev/null +++ b/test/typechecker/success/RecursiveRecordTypeMergeRecursivelyTypesB.dhallb @@ -0,0 +1 @@ +dKind \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordTypeMergeRhsEmptyA.dhallb b/test/typechecker/success/RecursiveRecordTypeMergeRhsEmptyA.dhallb new file mode 100644 index 0000000..68a7fef --- /dev/null +++ b/test/typechecker/success/RecursiveRecordTypeMergeRhsEmptyA.dhallb @@ -0,0 +1,2 @@ +„ +‚¡axdBool‚  \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordTypeMergeRhsEmptyB.dhallb b/test/typechecker/success/RecursiveRecordTypeMergeRhsEmptyB.dhallb new file mode 100644 index 0000000..0533f44 --- /dev/null +++ b/test/typechecker/success/RecursiveRecordTypeMergeRhsEmptyB.dhallb @@ -0,0 +1 @@ +dType \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordTypeMergeTwoA.dhallb b/test/typechecker/success/RecursiveRecordTypeMergeTwoA.dhallb new file mode 100644 index 0000000..f5b7ea6 --- /dev/null +++ b/test/typechecker/success/RecursiveRecordTypeMergeTwoA.dhallb @@ -0,0 +1,2 @@ +„ +‚¡axdBool‚¡aydBool \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordTypeMergeTwoB.dhallb b/test/typechecker/success/RecursiveRecordTypeMergeTwoB.dhallb new file mode 100644 index 0000000..0533f44 --- /dev/null +++ b/test/typechecker/success/RecursiveRecordTypeMergeTwoB.dhallb @@ -0,0 +1 @@ +dType \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordTypeMergeTwoKindsA.dhallb b/test/typechecker/success/RecursiveRecordTypeMergeTwoKindsA.dhallb new file mode 100644 index 0000000..fe1158d --- /dev/null +++ b/test/typechecker/success/RecursiveRecordTypeMergeTwoKindsA.dhallb @@ -0,0 +1,2 @@ +„ +‚¡axdKind‚¡aydKind \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordTypeMergeTwoKindsB.dhallb b/test/typechecker/success/RecursiveRecordTypeMergeTwoKindsB.dhallb new file mode 100644 index 0000000..5ca4cc6 --- /dev/null +++ b/test/typechecker/success/RecursiveRecordTypeMergeTwoKindsB.dhallb @@ -0,0 +1 @@ +dSort \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordTypeMergeTwoTypesA.dhallb b/test/typechecker/success/RecursiveRecordTypeMergeTwoTypesA.dhallb new file mode 100644 index 0000000..0ea04a0 --- /dev/null +++ b/test/typechecker/success/RecursiveRecordTypeMergeTwoTypesA.dhallb @@ -0,0 +1,2 @@ +„ +‚¡axdType‚¡aydType \ No newline at end of file diff --git a/test/typechecker/success/RecursiveRecordTypeMergeTwoTypesB.dhallb b/test/typechecker/success/RecursiveRecordTypeMergeTwoTypesB.dhallb new file mode 100644 index 0000000..9d1177c --- /dev/null +++ b/test/typechecker/success/RecursiveRecordTypeMergeTwoTypesB.dhallb @@ -0,0 +1 @@ +dKind \ No newline at end of file diff --git a/test/typechecker/success/RightBiasedRecordMergeRhsEmptyA.dhallb b/test/typechecker/success/RightBiasedRecordMergeRhsEmptyA.dhallb new file mode 100644 index 0000000..57fccb3 --- /dev/null +++ b/test/typechecker/success/RightBiasedRecordMergeRhsEmptyA.dhallb @@ -0,0 +1 @@ +„ ‚¡ax‚ ‚  \ No newline at end of file diff --git a/test/typechecker/success/RightBiasedRecordMergeRhsEmptyB.dhallb b/test/typechecker/success/RightBiasedRecordMergeRhsEmptyB.dhallb new file mode 100644 index 0000000..e3965ac --- /dev/null +++ b/test/typechecker/success/RightBiasedRecordMergeRhsEmptyB.dhallb @@ -0,0 +1 @@ +‚¡ax‚  \ No newline at end of file diff --git a/test/typechecker/success/RightBiasedRecordMergeTwoA.dhallb b/test/typechecker/success/RightBiasedRecordMergeTwoA.dhallb new file mode 100644 index 0000000..d6c4c4a --- /dev/null +++ b/test/typechecker/success/RightBiasedRecordMergeTwoA.dhallb @@ -0,0 +1 @@ +„ ‚¡ax‚ ‚¡ax‚  \ No newline at end of file diff --git a/test/typechecker/success/RightBiasedRecordMergeTwoB.dhallb b/test/typechecker/success/RightBiasedRecordMergeTwoB.dhallb new file mode 100644 index 0000000..e3965ac --- /dev/null +++ b/test/typechecker/success/RightBiasedRecordMergeTwoB.dhallb @@ -0,0 +1 @@ +‚¡ax‚  \ No newline at end of file diff --git a/test/typechecker/success/RightBiasedRecordMergeTwoDifferentA.dhallb b/test/typechecker/success/RightBiasedRecordMergeTwoDifferentA.dhallb new file mode 100644 index 0000000..9545111 --- /dev/null +++ b/test/typechecker/success/RightBiasedRecordMergeTwoDifferentA.dhallb @@ -0,0 +1 @@ +„ ‚¡ax‚ ‚¡axõ \ No newline at end of file diff --git a/test/typechecker/success/RightBiasedRecordMergeTwoDifferentB.dhallb b/test/typechecker/success/RightBiasedRecordMergeTwoDifferentB.dhallb new file mode 100644 index 0000000..cebf88e --- /dev/null +++ b/test/typechecker/success/RightBiasedRecordMergeTwoDifferentB.dhallb @@ -0,0 +1 @@ +‚¡axdBool \ No newline at end of file diff --git a/test/typechecker/success/RightBiasedRecordMergeTwoKindsA.dhallb b/test/typechecker/success/RightBiasedRecordMergeTwoKindsA.dhallb new file mode 100644 index 0000000..eb49109 --- /dev/null +++ b/test/typechecker/success/RightBiasedRecordMergeTwoKindsA.dhallb @@ -0,0 +1 @@ +„ ‚¡axdType‚¡axdType \ No newline at end of file diff --git a/test/typechecker/success/RightBiasedRecordMergeTwoKindsB.dhallb b/test/typechecker/success/RightBiasedRecordMergeTwoKindsB.dhallb new file mode 100644 index 0000000..83359ae --- /dev/null +++ b/test/typechecker/success/RightBiasedRecordMergeTwoKindsB.dhallb @@ -0,0 +1 @@ +‚¡axdKind \ No newline at end of file diff --git a/test/typechecker/success/RightBiasedRecordMergeTwoTypesA.dhallb b/test/typechecker/success/RightBiasedRecordMergeTwoTypesA.dhallb new file mode 100644 index 0000000..d730d3a --- /dev/null +++ b/test/typechecker/success/RightBiasedRecordMergeTwoTypesA.dhallb @@ -0,0 +1 @@ +„ ‚¡axdBool‚¡axgNatural \ No newline at end of file diff --git a/test/typechecker/success/RightBiasedRecordMergeTwoTypesB.dhallb b/test/typechecker/success/RightBiasedRecordMergeTwoTypesB.dhallb new file mode 100644 index 0000000..32ae7cb --- /dev/null +++ b/test/typechecker/success/RightBiasedRecordMergeTwoTypesB.dhallb @@ -0,0 +1 @@ +‚¡axdType \ No newline at end of file diff --git a/test/typechecker/success/SomeTrueA.dhallb b/test/typechecker/success/SomeTrueA.dhallb new file mode 100644 index 0000000..f40f60e --- /dev/null +++ b/test/typechecker/success/SomeTrueA.dhallb @@ -0,0 +1 @@ +ƒöõ \ No newline at end of file diff --git a/test/typechecker/success/SomeTrueB.dhallb b/test/typechecker/success/SomeTrueB.dhallb new file mode 100644 index 0000000000000000000000000000000000000000..b9ded578d26af23894fb0e59ec8f30f873de5fd6 GIT binary patch literal 16 XcmZo>$nY;H$;{77%t>*|&(8q>GGYcI literal 0 HcmV?d00001 diff --git a/test/typechecker/success/TypeAnnotationA.dhallb b/test/typechecker/success/TypeAnnotationA.dhallb new file mode 100644 index 0000000..1ed6c46 --- /dev/null +++ b/test/typechecker/success/TypeAnnotationA.dhallb @@ -0,0 +1 @@ +ƒõdBool \ No newline at end of file diff --git a/test/typechecker/success/TypeAnnotationB.dhallb b/test/typechecker/success/TypeAnnotationB.dhallb new file mode 100644 index 0000000..c418df5 --- /dev/null +++ b/test/typechecker/success/TypeAnnotationB.dhallb @@ -0,0 +1 @@ +dBool \ No newline at end of file diff --git a/test/typechecker/success/UnionConstructorFieldA.dhallb b/test/typechecker/success/UnionConstructorFieldA.dhallb new file mode 100644 index 0000000..847e34c --- /dev/null +++ b/test/typechecker/success/UnionConstructorFieldA.dhallb @@ -0,0 +1 @@ +ƒ ‚ ¡axdBoolax \ No newline at end of file diff --git a/test/typechecker/success/UnionConstructorFieldB.dhallb b/test/typechecker/success/UnionConstructorFieldB.dhallb new file mode 100644 index 0000000..6fca6d1 --- /dev/null +++ b/test/typechecker/success/UnionConstructorFieldB.dhallb @@ -0,0 +1 @@ +„axdBool‚ ¡axdBool \ No newline at end of file diff --git a/test/typechecker/success/UnionOneA.dhallb b/test/typechecker/success/UnionOneA.dhallb new file mode 100644 index 0000000..3a17da1 --- /dev/null +++ b/test/typechecker/success/UnionOneA.dhallb @@ -0,0 +1 @@ +„ axõ  \ No newline at end of file diff --git a/test/typechecker/success/UnionOneB.dhallb b/test/typechecker/success/UnionOneB.dhallb new file mode 100644 index 0000000..31afa54 --- /dev/null +++ b/test/typechecker/success/UnionOneB.dhallb @@ -0,0 +1 @@ +‚ ¡axdBool \ No newline at end of file diff --git a/test/typechecker/success/UnionTypeEmptyA.dhallb b/test/typechecker/success/UnionTypeEmptyA.dhallb new file mode 100644 index 0000000..d1a5b3e --- /dev/null +++ b/test/typechecker/success/UnionTypeEmptyA.dhallb @@ -0,0 +1 @@ +‚   \ No newline at end of file diff --git a/test/typechecker/success/UnionTypeEmptyB.dhallb b/test/typechecker/success/UnionTypeEmptyB.dhallb new file mode 100644 index 0000000..0533f44 --- /dev/null +++ b/test/typechecker/success/UnionTypeEmptyB.dhallb @@ -0,0 +1 @@ +dType \ No newline at end of file diff --git a/test/typechecker/success/UnionTypeKindA.dhallb b/test/typechecker/success/UnionTypeKindA.dhallb new file mode 100644 index 0000000..c8d94d4 --- /dev/null +++ b/test/typechecker/success/UnionTypeKindA.dhallb @@ -0,0 +1 @@ +‚ ¡axdKind \ No newline at end of file diff --git a/test/typechecker/success/UnionTypeKindB.dhallb b/test/typechecker/success/UnionTypeKindB.dhallb new file mode 100644 index 0000000..5ca4cc6 --- /dev/null +++ b/test/typechecker/success/UnionTypeKindB.dhallb @@ -0,0 +1 @@ +dSort \ No newline at end of file diff --git a/test/typechecker/success/UnionTypeOneA.dhallb b/test/typechecker/success/UnionTypeOneA.dhallb new file mode 100644 index 0000000..31afa54 --- /dev/null +++ b/test/typechecker/success/UnionTypeOneA.dhallb @@ -0,0 +1 @@ +‚ ¡axdBool \ No newline at end of file diff --git a/test/typechecker/success/UnionTypeOneB.dhallb b/test/typechecker/success/UnionTypeOneB.dhallb new file mode 100644 index 0000000..0533f44 --- /dev/null +++ b/test/typechecker/success/UnionTypeOneB.dhallb @@ -0,0 +1 @@ +dType \ No newline at end of file diff --git a/test/typechecker/success/UnionTypeTypeA.dhallb b/test/typechecker/success/UnionTypeTypeA.dhallb new file mode 100644 index 0000000..5998c8d --- /dev/null +++ b/test/typechecker/success/UnionTypeTypeA.dhallb @@ -0,0 +1 @@ +‚ ¡axdType \ No newline at end of file diff --git a/test/typechecker/success/UnionTypeTypeB.dhallb b/test/typechecker/success/UnionTypeTypeB.dhallb new file mode 100644 index 0000000..9d1177c --- /dev/null +++ b/test/typechecker/success/UnionTypeTypeB.dhallb @@ -0,0 +1 @@ +dKind \ No newline at end of file -- 2.34.5