From 73af29fb11517f85043d8a866697b150dc7c2191 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 23 Feb 2020 20:56:03 +0000 Subject: Add a bunch of tests --- .../failure/unit/FunctionTypeOutputTypeNotAType.dhall | 1 + .../type-inference/failure/unit/FunctionTypeOutputTypeNotAType.txt | 7 +++++++ dhall/tests/type-inference/failure/unit/LetInSort.dhall | 1 + dhall/tests/type-inference/failure/unit/LetInSort.txt | 6 ++++++ dhall/tests/type-inference/failure/unit/MergeBool.dhall | 1 + dhall/tests/type-inference/failure/unit/MergeBool.txt | 6 ++++++ .../tests/type-inference/failure/unit/NestedAnnotInnerWrong.dhall | 1 + dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.txt | 6 ++++++ .../tests/type-inference/failure/unit/NestedAnnotOuterWrong.dhall | 1 + dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.txt | 6 ++++++ .../type-inference/success/regression/LambdaInLetScoping1A.dhall | 1 + .../type-inference/success/regression/LambdaInLetScoping1B.dhall | 1 + .../type-inference/success/regression/LambdaInLetScoping2A.dhall | 1 + .../type-inference/success/regression/LambdaInLetScoping2B.dhall | 1 + .../regression/RecursiveRecordTypeMergeTripleCollisionA.dhall | 1 + .../regression/RecursiveRecordTypeMergeTripleCollisionB.dhall | 1 + dhall/tests/type-inference/success/regression/TodoA.dhall | 1 + dhall/tests/type-inference/success/regression/TodoB.dhall | 1 + 18 files changed, 44 insertions(+) create mode 100644 dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.dhall create mode 100644 dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.txt create mode 100644 dhall/tests/type-inference/failure/unit/LetInSort.dhall create mode 100644 dhall/tests/type-inference/failure/unit/LetInSort.txt create mode 100644 dhall/tests/type-inference/failure/unit/MergeBool.dhall create mode 100644 dhall/tests/type-inference/failure/unit/MergeBool.txt create mode 100644 dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.dhall create mode 100644 dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.txt create mode 100644 dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.dhall create mode 100644 dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.txt create mode 100644 dhall/tests/type-inference/success/regression/LambdaInLetScoping1A.dhall create mode 100644 dhall/tests/type-inference/success/regression/LambdaInLetScoping1B.dhall create mode 100644 dhall/tests/type-inference/success/regression/LambdaInLetScoping2A.dhall create mode 100644 dhall/tests/type-inference/success/regression/LambdaInLetScoping2B.dhall create mode 100644 dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionA.dhall create mode 100644 dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionB.dhall create mode 100644 dhall/tests/type-inference/success/regression/TodoA.dhall create mode 100644 dhall/tests/type-inference/success/regression/TodoB.dhall (limited to 'dhall/tests/type-inference') 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` + --> :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 + --> :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 + --> :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 + --> :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 + --> :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 -- cgit v1.2.3 From 60d202471ed5013d1ab607a4c34b82448d708261 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 29 Feb 2020 22:03:46 +0000 Subject: Add a bunch of `as Location` unit tests --- dhall/tests/type-inference/success/CacheImportsA.dhall | 1 + dhall/tests/type-inference/success/CacheImportsB.dhall | 1 + 2 files changed, 2 insertions(+) create mode 100644 dhall/tests/type-inference/success/CacheImportsA.dhall create mode 100644 dhall/tests/type-inference/success/CacheImportsB.dhall (limited to 'dhall/tests/type-inference') diff --git a/dhall/tests/type-inference/success/CacheImportsA.dhall b/dhall/tests/type-inference/success/CacheImportsA.dhall new file mode 100644 index 0000000..3bd2bc1 --- /dev/null +++ b/dhall/tests/type-inference/success/CacheImportsA.dhall @@ -0,0 +1 @@ +let _ = assert : https://csrng.net/csrng/csrng.php?min=0&max=1000 as Text === https://csrng.net/csrng/csrng.php?min=0&max=1000 as Text in 0 diff --git a/dhall/tests/type-inference/success/CacheImportsB.dhall b/dhall/tests/type-inference/success/CacheImportsB.dhall new file mode 100644 index 0000000..2f184a4 --- /dev/null +++ b/dhall/tests/type-inference/success/CacheImportsB.dhall @@ -0,0 +1 @@ +Natural -- cgit v1.2.3 From 24ff14dc98b83ddc12239a0eae4852c9cd87d41f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 1 Mar 2020 16:37:10 +0000 Subject: Add a lot of import tests --- dhall/tests/type-inference/success/CacheImportsA.dhall | 5 +++++ dhall/tests/type-inference/success/CacheImportsCanonicalizeA.dhall | 5 +++++ dhall/tests/type-inference/success/CacheImportsCanonicalizeB.dhall | 1 + 3 files changed, 11 insertions(+) create mode 100644 dhall/tests/type-inference/success/CacheImportsCanonicalizeA.dhall create mode 100644 dhall/tests/type-inference/success/CacheImportsCanonicalizeB.dhall (limited to 'dhall/tests/type-inference') diff --git a/dhall/tests/type-inference/success/CacheImportsA.dhall b/dhall/tests/type-inference/success/CacheImportsA.dhall index 3bd2bc1..7180b19 100644 --- a/dhall/tests/type-inference/success/CacheImportsA.dhall +++ b/dhall/tests/type-inference/success/CacheImportsA.dhall @@ -1 +1,6 @@ +{- + This URL returns (probably) a different result for each request. This test + ensures that import results for a given URL are correctly cached within an + execution of dhall. +-} let _ = assert : https://csrng.net/csrng/csrng.php?min=0&max=1000 as Text === https://csrng.net/csrng/csrng.php?min=0&max=1000 as Text in 0 diff --git a/dhall/tests/type-inference/success/CacheImportsCanonicalizeA.dhall b/dhall/tests/type-inference/success/CacheImportsCanonicalizeA.dhall new file mode 100644 index 0000000..e7f4dcd --- /dev/null +++ b/dhall/tests/type-inference/success/CacheImportsCanonicalizeA.dhall @@ -0,0 +1,5 @@ +{- + This URL returns (probably) a different result for each request. This test + ensures that import locations are canonicalized before being cached. +-} +let _ = assert : https://csrng.net/csrng/csrng.php?min=0&max=1000 as Text === https://csrng.net/csrng/../csrng/csrng.php?min=0&max=1000 as Text in 0 diff --git a/dhall/tests/type-inference/success/CacheImportsCanonicalizeB.dhall b/dhall/tests/type-inference/success/CacheImportsCanonicalizeB.dhall new file mode 100644 index 0000000..2f184a4 --- /dev/null +++ b/dhall/tests/type-inference/success/CacheImportsCanonicalizeB.dhall @@ -0,0 +1 @@ +Natural -- cgit v1.2.3