diff options
| author | Nadrieril | 2020-02-23 20:56:03 +0000 |
|---|---|---|
| committer | Nadrieril | 2020-03-05 15:58:31 +0000 |
| commit | 73af29fb11517f85043d8a866697b150dc7c2191 (patch) | |
| tree | af401099a71c67a647ad5942ae06ff172f4a63c9 | |
| parent | b7f6c5778c3c980a452abd3da715996fa24d4449 (diff) | |
Add a bunch of tests
50 files changed, 70 insertions, 23 deletions
diff --git a/dhall/tests/normalization/success/regression/NaturalFoldExtraArgA.dhall b/dhall/tests/normalization/success/regression/NaturalFoldExtraArgA.dhall new file mode 100644 index 0000000..3a69d1e --- /dev/null +++ b/dhall/tests/normalization/success/regression/NaturalFoldExtraArgA.dhall @@ -0,0 +1 @@ +Natural/fold 0 (Bool -> Bool) (λ(_ : (Bool -> Bool)) → λ(_ : Bool) → True) (λ(_ : Bool) → False) True diff --git a/dhall/tests/normalization/success/regression/NaturalFoldExtraArgB.dhall b/dhall/tests/normalization/success/regression/NaturalFoldExtraArgB.dhall new file mode 100644 index 0000000..bc59c12 --- /dev/null +++ b/dhall/tests/normalization/success/regression/NaturalFoldExtraArgB.dhall @@ -0,0 +1 @@ +False diff --git a/dhall/tests/normalization/success/regression/TrickyBinderIdentityA.dhall b/dhall/tests/normalization/success/regression/TrickyBinderIdentityA.dhall new file mode 100644 index 0000000..5d72bbe --- /dev/null +++ b/dhall/tests/normalization/success/regression/TrickyBinderIdentityA.dhall @@ -0,0 +1 @@ +let T = Natural let ap = λ(f : T → List T) -> λ(x : T) -> f x in ap (λ(x : T) -> ap (λ(y : T) -> [x, y]) 1) 0 diff --git a/dhall/tests/normalization/success/regression/TrickyBinderIdentityB.dhall b/dhall/tests/normalization/success/regression/TrickyBinderIdentityB.dhall new file mode 100644 index 0000000..28233fb --- /dev/null +++ b/dhall/tests/normalization/success/regression/TrickyBinderIdentityB.dhall @@ -0,0 +1 @@ +[ 0, 1 ] diff --git a/dhall/tests/normalization/success/unit/TextLitNested1A.dhall b/dhall/tests/normalization/success/unit/TextLitNested1A.dhall new file mode 100644 index 0000000..104dc41 --- /dev/null +++ b/dhall/tests/normalization/success/unit/TextLitNested1A.dhall @@ -0,0 +1 @@ +λ(x: Text) → "${""}${x}" diff --git a/dhall/tests/normalization/success/unit/TextLitNested1B.dhall b/dhall/tests/normalization/success/unit/TextLitNested1B.dhall new file mode 100644 index 0000000..631a6cf --- /dev/null +++ b/dhall/tests/normalization/success/unit/TextLitNested1B.dhall @@ -0,0 +1 @@ +λ(x : Text) → x diff --git a/dhall/tests/normalization/success/unit/TextLitNested2A.dhall b/dhall/tests/normalization/success/unit/TextLitNested2A.dhall new file mode 100644 index 0000000..5b4ae6e --- /dev/null +++ b/dhall/tests/normalization/success/unit/TextLitNested2A.dhall @@ -0,0 +1 @@ +λ(x: Text) → "${"${x}"}" diff --git a/dhall/tests/normalization/success/unit/TextLitNested2B.dhall b/dhall/tests/normalization/success/unit/TextLitNested2B.dhall new file mode 100644 index 0000000..631a6cf --- /dev/null +++ b/dhall/tests/normalization/success/unit/TextLitNested2B.dhall @@ -0,0 +1 @@ +λ(x : Text) → x diff --git a/dhall/tests/normalization/success/unit/TextLitNested3A.dhall b/dhall/tests/normalization/success/unit/TextLitNested3A.dhall new file mode 100644 index 0000000..d57ac64 --- /dev/null +++ b/dhall/tests/normalization/success/unit/TextLitNested3A.dhall @@ -0,0 +1 @@ +λ(x: Text) → "${"${""}"}${x}" diff --git a/dhall/tests/normalization/success/unit/TextLitNested3B.dhall b/dhall/tests/normalization/success/unit/TextLitNested3B.dhall new file mode 100644 index 0000000..631a6cf --- /dev/null +++ b/dhall/tests/normalization/success/unit/TextLitNested3B.dhall @@ -0,0 +1 @@ +λ(x : Text) → x diff --git a/dhall/tests/normalization/success/unit/TextShowEmptyA.dhall b/dhall/tests/normalization/success/unit/TextShowEmptyA.dhall new file mode 100644 index 0000000..589f65d --- /dev/null +++ b/dhall/tests/normalization/success/unit/TextShowEmptyA.dhall @@ -0,0 +1 @@ +Text/show "" diff --git a/dhall/tests/normalization/success/unit/TextShowEmptyB.dhall b/dhall/tests/normalization/success/unit/TextShowEmptyB.dhall new file mode 100644 index 0000000..8fbbe76 --- /dev/null +++ b/dhall/tests/normalization/success/unit/TextShowEmptyB.dhall @@ -0,0 +1 @@ +"\"\"" diff --git a/dhall/tests/parser/failure/unit/AssertNoAnnotation.dhall b/dhall/tests/parser/failure/unit/AssertNoAnnotation.dhall new file mode 100644 index 0000000..6019020 --- /dev/null +++ b/dhall/tests/parser/failure/unit/AssertNoAnnotation.dhall @@ -0,0 +1 @@ +assert diff --git a/dhall/tests/parser/success/unit/EmptyRecordLiteralA.dhall b/dhall/tests/parser/success/unit/EmptyRecordLiteralA.dhall new file mode 100644 index 0000000..339130f --- /dev/null +++ b/dhall/tests/parser/success/unit/EmptyRecordLiteralA.dhall @@ -0,0 +1 @@ +{=} diff --git a/dhall/tests/parser/success/unit/EmptyRecordLiteralB.dhallb b/dhall/tests/parser/success/unit/EmptyRecordLiteralB.dhallb new file mode 100644 index 0000000..58e2e39 --- /dev/null +++ b/dhall/tests/parser/success/unit/EmptyRecordLiteralB.dhallb @@ -0,0 +1 @@ +‚
\ No newline at end of file diff --git a/dhall/tests/parser/success/unit/EmptyRecordLiteralB.diag b/dhall/tests/parser/success/unit/EmptyRecordLiteralB.diag new file mode 100644 index 0000000..8ead206 --- /dev/null +++ b/dhall/tests/parser/success/unit/EmptyRecordLiteralB.diag @@ -0,0 +1 @@ +[8, {}] diff --git a/dhall/tests/parser/success/unit/LetAnnotA.dhall b/dhall/tests/parser/success/unit/LetAnnotA.dhall new file mode 100644 index 0000000..c7d29f8 --- /dev/null +++ b/dhall/tests/parser/success/unit/LetAnnotA.dhall @@ -0,0 +1 @@ +let x: T = y in e diff --git a/dhall/tests/parser/success/unit/LetAnnotB.dhallb b/dhall/tests/parser/success/unit/LetAnnotB.dhallb Binary files differnew file mode 100644 index 0000000..4e3a7e4 --- /dev/null +++ b/dhall/tests/parser/success/unit/LetAnnotB.dhallb diff --git a/dhall/tests/parser/success/unit/LetAnnotB.diag b/dhall/tests/parser/success/unit/LetAnnotB.diag new file mode 100644 index 0000000..36791e0 --- /dev/null +++ b/dhall/tests/parser/success/unit/LetAnnotB.diag @@ -0,0 +1 @@ +[25, "x", ["T", 0], ["y", 0], ["e", 0]] diff --git a/dhall/tests/parser/success/unit/LetNoAnnotA.dhall b/dhall/tests/parser/success/unit/LetNoAnnotA.dhall new file mode 100644 index 0000000..64d30e6 --- /dev/null +++ b/dhall/tests/parser/success/unit/LetNoAnnotA.dhall @@ -0,0 +1 @@ +let x = y in e diff --git a/dhall/tests/parser/success/unit/LetNoAnnotB.dhallb b/dhall/tests/parser/success/unit/LetNoAnnotB.dhallb Binary files differnew file mode 100644 index 0000000..79a2384 --- /dev/null +++ b/dhall/tests/parser/success/unit/LetNoAnnotB.dhallb diff --git a/dhall/tests/parser/success/unit/LetNoAnnotB.diag b/dhall/tests/parser/success/unit/LetNoAnnotB.diag new file mode 100644 index 0000000..a23f605 --- /dev/null +++ b/dhall/tests/parser/success/unit/LetNoAnnotB.diag @@ -0,0 +1 @@ +[25, "x", null, ["y", 0], ["e", 0]] diff --git a/dhall/tests/parser/success/unit/ToMapA.dhall b/dhall/tests/parser/success/unit/ToMapA.dhall new file mode 100644 index 0000000..ea04391 --- /dev/null +++ b/dhall/tests/parser/success/unit/ToMapA.dhall @@ -0,0 +1 @@ +toMap x diff --git a/dhall/tests/parser/success/unit/ToMapAnnotA.dhall b/dhall/tests/parser/success/unit/ToMapAnnotA.dhall new file mode 100644 index 0000000..ad65b07 --- /dev/null +++ b/dhall/tests/parser/success/unit/ToMapAnnotA.dhall @@ -0,0 +1 @@ +toMap x : T diff --git a/dhall/tests/parser/success/unit/ToMapAnnotB.dhallb b/dhall/tests/parser/success/unit/ToMapAnnotB.dhallb Binary files differnew file mode 100644 index 0000000..4b53587 --- /dev/null +++ b/dhall/tests/parser/success/unit/ToMapAnnotB.dhallb diff --git a/dhall/tests/parser/success/unit/ToMapAnnotB.diag b/dhall/tests/parser/success/unit/ToMapAnnotB.diag new file mode 100644 index 0000000..8e511fb --- /dev/null +++ b/dhall/tests/parser/success/unit/ToMapAnnotB.diag @@ -0,0 +1 @@ +[27, ["x", 0], ["T", 0]] diff --git a/dhall/tests/parser/success/unit/ToMapB.dhallb b/dhall/tests/parser/success/unit/ToMapB.dhallb Binary files differnew file mode 100644 index 0000000..25ecd95 --- /dev/null +++ b/dhall/tests/parser/success/unit/ToMapB.dhallb diff --git a/dhall/tests/parser/success/unit/ToMapB.diag b/dhall/tests/parser/success/unit/ToMapB.diag new file mode 100644 index 0000000..5d25b39 --- /dev/null +++ b/dhall/tests/parser/success/unit/ToMapB.diag @@ -0,0 +1 @@ +[27, ["x", 0]] diff --git a/dhall/tests/parser/success/unit/VariableQuotedWithSpaceA.dhall b/dhall/tests/parser/success/unit/VariableQuotedWithSpaceA.dhall new file mode 100644 index 0000000..a1f4d02 --- /dev/null +++ b/dhall/tests/parser/success/unit/VariableQuotedWithSpaceA.dhall @@ -0,0 +1 @@ +` x ` diff --git a/dhall/tests/parser/success/unit/VariableQuotedWithSpaceB.dhallb b/dhall/tests/parser/success/unit/VariableQuotedWithSpaceB.dhallb Binary files differnew file mode 100644 index 0000000..56d9cd9 --- /dev/null +++ b/dhall/tests/parser/success/unit/VariableQuotedWithSpaceB.dhallb diff --git a/dhall/tests/parser/success/unit/VariableQuotedWithSpaceB.diag b/dhall/tests/parser/success/unit/VariableQuotedWithSpaceB.diag new file mode 100644 index 0000000..035d650 --- /dev/null +++ b/dhall/tests/parser/success/unit/VariableQuotedWithSpaceB.diag @@ -0,0 +1 @@ +[" x ", 0] diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.dhall b/dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.dhall new file mode 100644 index 0000000..94b32f9 --- /dev/null +++ b/dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.dhall @@ -0,0 +1 @@ +Bool -> 1 diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.txt b/dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.txt new file mode 100644 index 0000000..bcc44a5 --- /dev/null +++ b/dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.txt @@ -0,0 +1,7 @@ +Type error: error: Expected a type, found: `1` + --> <current file>:1:8 + | +1 | Bool -> 1 + | ^ this has type: `Natural` + | + = help: An expression in type position must have type `Type`, `Kind` or `Sort` diff --git a/dhall/tests/type-inference/failure/unit/LetInSort.dhall b/dhall/tests/type-inference/failure/unit/LetInSort.dhall new file mode 100644 index 0000000..125ab28 --- /dev/null +++ b/dhall/tests/type-inference/failure/unit/LetInSort.dhall @@ -0,0 +1 @@ +\(x: let x = 0 in Sort) -> 1 diff --git a/dhall/tests/type-inference/failure/unit/LetInSort.txt b/dhall/tests/type-inference/failure/unit/LetInSort.txt new file mode 100644 index 0000000..07be298 --- /dev/null +++ b/dhall/tests/type-inference/failure/unit/LetInSort.txt @@ -0,0 +1,6 @@ +Type error: error: Sort does not have a type + --> <current file>:1:18 + | +1 | \(x: let x = 0 in Sort) -> 1 + | ^^^^ Sort does not have a type + | diff --git a/dhall/tests/type-inference/failure/unit/MergeBool.dhall b/dhall/tests/type-inference/failure/unit/MergeBool.dhall new file mode 100644 index 0000000..01e7e3f --- /dev/null +++ b/dhall/tests/type-inference/failure/unit/MergeBool.dhall @@ -0,0 +1 @@ +\(x: { True: Natural, False: Natural }) -> merge x True diff --git a/dhall/tests/type-inference/failure/unit/MergeBool.txt b/dhall/tests/type-inference/failure/unit/MergeBool.txt new file mode 100644 index 0000000..209def1 --- /dev/null +++ b/dhall/tests/type-inference/failure/unit/MergeBool.txt @@ -0,0 +1,6 @@ +Type error: error: Merge2ArgMustBeUnionOrOptional + --> <current file>:1:43 + | +1 | \(x: { True: Natural, False: Natural }) -> merge x True + | ^^^^^^^^^^^^ Merge2ArgMustBeUnionOrOptional + | diff --git a/dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.dhall b/dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.dhall new file mode 100644 index 0000000..7e5c8ec --- /dev/null +++ b/dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.dhall @@ -0,0 +1 @@ +(0 : Bool) : Natural diff --git a/dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.txt b/dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.txt new file mode 100644 index 0000000..b56db54 --- /dev/null +++ b/dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.txt @@ -0,0 +1,6 @@ +Type error: error: annot mismatch: Natural != Bool + --> <current file>:1:1 + | +1 | (0 : Bool) : Natural + | ^ annot mismatch: Natural != Bool + | diff --git a/dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.dhall b/dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.dhall new file mode 100644 index 0000000..67a1526 --- /dev/null +++ b/dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.dhall @@ -0,0 +1 @@ +(0 : Natural) : Bool diff --git a/dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.txt b/dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.txt new file mode 100644 index 0000000..2f07b8d --- /dev/null +++ b/dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.txt @@ -0,0 +1,6 @@ +Type error: error: annot mismatch: Natural != Bool + --> <current file>:1:1 + | +1 | (0 : Natural) : Bool + | ^^^^^^^^^^^ annot mismatch: Natural != Bool + | diff --git a/dhall/tests/type-inference/success/regression/LambdaInLetScoping1A.dhall b/dhall/tests/type-inference/success/regression/LambdaInLetScoping1A.dhall new file mode 100644 index 0000000..72f866f --- /dev/null +++ b/dhall/tests/type-inference/success/regression/LambdaInLetScoping1A.dhall @@ -0,0 +1 @@ +let T = 0 in λ(T : Type) → λ(x : T) → 1 diff --git a/dhall/tests/type-inference/success/regression/LambdaInLetScoping1B.dhall b/dhall/tests/type-inference/success/regression/LambdaInLetScoping1B.dhall new file mode 100644 index 0000000..42bfeec --- /dev/null +++ b/dhall/tests/type-inference/success/regression/LambdaInLetScoping1B.dhall @@ -0,0 +1 @@ +∀(T : Type) → ∀(x : T) → Natural diff --git a/dhall/tests/type-inference/success/regression/LambdaInLetScoping2A.dhall b/dhall/tests/type-inference/success/regression/LambdaInLetScoping2A.dhall new file mode 100644 index 0000000..30fd03c --- /dev/null +++ b/dhall/tests/type-inference/success/regression/LambdaInLetScoping2A.dhall @@ -0,0 +1 @@ +(λ(T : Type) → let x = 0 in λ(x : T) → x) : ∀(T : Type) → ∀(x : T) → T diff --git a/dhall/tests/type-inference/success/regression/LambdaInLetScoping2B.dhall b/dhall/tests/type-inference/success/regression/LambdaInLetScoping2B.dhall new file mode 100644 index 0000000..20aa0d3 --- /dev/null +++ b/dhall/tests/type-inference/success/regression/LambdaInLetScoping2B.dhall @@ -0,0 +1 @@ +∀(T : Type) → ∀(x : T) → T diff --git a/dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionA.dhall b/dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionA.dhall new file mode 100644 index 0000000..c7b7fb4 --- /dev/null +++ b/dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionA.dhall @@ -0,0 +1 @@ +{ x : { a : Bool } } ⩓ { x : { b : Bool } } ⩓ { x : { c : Bool } } diff --git a/dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionB.dhall b/dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionB.dhall new file mode 100644 index 0000000..245bc9d --- /dev/null +++ b/dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionB.dhall @@ -0,0 +1 @@ +Type diff --git a/dhall/tests/type-inference/success/regression/TodoA.dhall b/dhall/tests/type-inference/success/regression/TodoA.dhall new file mode 100644 index 0000000..9d5ef34 --- /dev/null +++ b/dhall/tests/type-inference/success/regression/TodoA.dhall @@ -0,0 +1 @@ +λ(todo : ∀(a : Type) → a) → todo diff --git a/dhall/tests/type-inference/success/regression/TodoB.dhall b/dhall/tests/type-inference/success/regression/TodoB.dhall new file mode 100644 index 0000000..e0091f2 --- /dev/null +++ b/dhall/tests/type-inference/success/regression/TodoB.dhall @@ -0,0 +1 @@ +∀(todo : ∀(a : Type) → a) → ∀(a : Type) → a diff --git a/tests_buffer b/tests_buffer index c582689..6f6e67e 100644 --- a/tests_buffer +++ b/tests_buffer @@ -1,26 +1,3 @@ -normalization/success/unit/TextShowEmpty Text/show "" -normalization/success/unit/TextLitNested1 λ(x: Text) → "${""}${x}" -normalization/success/unit/TextLitNested2 λ(x: Text) → "${"${x}"}" -normalization/success/unit/TextLitNested3 λ(x: Text) → "${"${""}"}${x}" -normalization/success/regression/NaturalFoldExtraArg Natural/fold 0 (Bool -> Bool) (λ(_ : (Bool -> Bool)) → λ(_ : Bool) → True) (λ(_ : Bool) → False) True -normalization/success/regression/TrickyBinderIdentity let T = Natural let ap = λ(f : T → List T) -> λ(x : T) -> f x in ap (λ(x : T) -> ap (λ(y : T) -> [x, y]) 1) 0 -parser/success/unit/LetNoAnnot let x = y in e -parser/success/unit/LetAnnot let x: T = y in e -parser/success/unit/EmptyRecordLiteral {=} -parser/success/unit/ToMap toMap x -parser/success/unit/ToMapAnnot toMap x : T -parser/success/unit/VariableQuotedWithSpace ` x ` -parser/failure/unit/AssertNoAnnotation assert -type-inference/failure/unit/FunctionTypeOutputTypeNotAType Bool -> 1 -type-inference/failure/unit/NestedAnnotInnerWrong (0 : Bool) : Natural -type-inference/failure/unit/NestedAnnotOuterWrong (0 : Natural) : Bool -type-inference/failure/unit/MergeBool merge x True -type-inference/failure/unit/LetInSort \(x: let x = 0 in Sort) -> 1 -type-inference/success/regression/RecursiveRecordTypeMergeTripleCollision { x : { a : Bool } } ⩓ { x : { b : Bool } } ⩓ { x : { c : Bool } } -type-inference/success/regression/Todo λ(todo : ∀(a : Type) → a) → todo -type-inference/success/regression/LambdaInLetScoping1 let T = 0 in λ(T : Type) → λ(x : T) → 1 -type-inference/success/regression/LambdaInLetScoping2 (λ(T : Type) → let x = 0 in λ(x : T) → x) : ∀(T : Type) → ∀(x : T) → T - parser: ./a%20b ./"a%20b" |