From b7f6c5778c3c980a452abd3da715996fa24d4449 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 23 Feb 2020 20:56:27 +0000 Subject: Prepare test buffer --- tests_buffer | 51 +++++++++++++++++++++++---------------------------- 1 file changed, 23 insertions(+), 28 deletions(-) (limited to 'tests_buffer') diff --git a/tests_buffer b/tests_buffer index db63cde..c582689 100644 --- a/tests_buffer +++ b/tests_buffer @@ -1,3 +1,26 @@ +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" @@ -5,18 +28,6 @@ text interpolation and escapes projection by expression unit tests fix fakeurlencode test s/QuotedVariable/VariableQuoted/ -success/ - operators/ - PrecedenceAll1 a ? b || c + d ++ e # f && g ∧ h ⫽ i ⩓ j * k == l != m n.o - PrecedenceAll2 a b != c == d * e ⩓ f ⫽ g ∧ h && i # j ++ k + l || m ? n - LetNoAnnot let x = y in e - LetAnnot let x: T = y in e - EmptyRecordLiteral {=} - ToMap toMap x - ToMapAnnot toMap x : T - VariableQuotedWithSpace ` x ` -failure/ - AssertNoAnnotation assert binary decoding: decode old-style optional literals ? @@ -30,37 +41,21 @@ failure/ normalization: variables across import boundaries - Text/show "" - TextLitNested1 "${""}${x}" - TextLitNested2 "${"${x}"}" - TextLitNested3 "${"${""}"}${x}" - regression/ - NaturalFoldExtraArg Natural/fold 0 (Bool -> Bool) (λ(_ : (Bool -> Bool)) → λ(_ : Bool) → True) (λ(_ : Bool) → False) True - let T = Natural let ap = λ(f : T → List T) -> λ(x : T) -> f x in ap (λ(x : T) -> ap (λ(y : T) -> [x, y]) 1) 0 typecheck: something that involves destructuring a recordtype after merge add some of the more complicated Prelude tests back, like List/enumerate success/ regression/ - RecursiveRecordTypeMergeTripleCollision { x : { a : Bool } } ⩓ { x : { b : Bool } } ⩓ { x : { c : Bool } } somehow test that ({ x = { z = 1 } } ∧ { x = { y = 2 } }).x has a type somehow test that the recordtype from List/indexed has a type in both empty and nonempty cases somehow test types added to the Foo/build closures - λ(todo : ∀(a : Type) → a) → todo - let T = 0 in λ(T : Type) → λ(x : T) → 1 - (λ(T : Type) → let x = 0 in λ(x : T) → x) : ∀(T : Type) → ∀(x : T) → T failure/ \(_: Bool) -> assert : (\(_: Bool) -> _) === (\(x: Bool) -> _) - unit/FunctionTypeOutputTypeNotAType Bool -> 1 - unit/NestedAnnotInnerWrong (0 : Bool) : Natural - unit/NestedAnnotOuterWrong (0 : Natural) : Bool merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True) merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y > merge { x = True, y = 1 } < x | y >.x merge {x=...,y=...} .x merge {x=...,y=...} .x - MergeBool merge x True - LetInSort \(x: let x = 0 in Sort) -> 1 equivalence: -- cgit v1.3.1 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 --- .../success/regression/NaturalFoldExtraArgA.dhall | 1 + .../success/regression/NaturalFoldExtraArgB.dhall | 1 + .../success/regression/TrickyBinderIdentityA.dhall | 1 + .../success/regression/TrickyBinderIdentityB.dhall | 1 + .../success/unit/TextLitNested1A.dhall | 1 + .../success/unit/TextLitNested1B.dhall | 1 + .../success/unit/TextLitNested2A.dhall | 1 + .../success/unit/TextLitNested2B.dhall | 1 + .../success/unit/TextLitNested3A.dhall | 1 + .../success/unit/TextLitNested3B.dhall | 1 + .../success/unit/TextShowEmptyA.dhall | 1 + .../success/unit/TextShowEmptyB.dhall | 1 + .../parser/failure/unit/AssertNoAnnotation.dhall | 1 + .../parser/success/unit/EmptyRecordLiteralA.dhall | 1 + .../parser/success/unit/EmptyRecordLiteralB.dhallb | 1 + .../parser/success/unit/EmptyRecordLiteralB.diag | 1 + dhall/tests/parser/success/unit/LetAnnotA.dhall | 1 + dhall/tests/parser/success/unit/LetAnnotB.dhallb | Bin 0 -> 17 bytes dhall/tests/parser/success/unit/LetAnnotB.diag | 1 + dhall/tests/parser/success/unit/LetNoAnnotA.dhall | 1 + dhall/tests/parser/success/unit/LetNoAnnotB.dhallb | Bin 0 -> 14 bytes dhall/tests/parser/success/unit/LetNoAnnotB.diag | 1 + dhall/tests/parser/success/unit/ToMapA.dhall | 1 + dhall/tests/parser/success/unit/ToMapAnnotA.dhall | 1 + dhall/tests/parser/success/unit/ToMapAnnotB.dhallb | Bin 0 -> 11 bytes dhall/tests/parser/success/unit/ToMapAnnotB.diag | 1 + dhall/tests/parser/success/unit/ToMapB.dhallb | Bin 0 -> 7 bytes dhall/tests/parser/success/unit/ToMapB.diag | 1 + .../success/unit/VariableQuotedWithSpaceA.dhall | 1 + .../success/unit/VariableQuotedWithSpaceB.dhallb | Bin 0 -> 6 bytes .../success/unit/VariableQuotedWithSpaceB.diag | 1 + .../unit/FunctionTypeOutputTypeNotAType.dhall | 1 + .../unit/FunctionTypeOutputTypeNotAType.txt | 7 +++++++ .../type-inference/failure/unit/LetInSort.dhall | 1 + .../type-inference/failure/unit/LetInSort.txt | 6 ++++++ .../type-inference/failure/unit/MergeBool.dhall | 1 + .../type-inference/failure/unit/MergeBool.txt | 6 ++++++ .../failure/unit/NestedAnnotInnerWrong.dhall | 1 + .../failure/unit/NestedAnnotInnerWrong.txt | 6 ++++++ .../failure/unit/NestedAnnotOuterWrong.dhall | 1 + .../failure/unit/NestedAnnotOuterWrong.txt | 6 ++++++ .../success/regression/LambdaInLetScoping1A.dhall | 1 + .../success/regression/LambdaInLetScoping1B.dhall | 1 + .../success/regression/LambdaInLetScoping2A.dhall | 1 + .../success/regression/LambdaInLetScoping2B.dhall | 1 + .../RecursiveRecordTypeMergeTripleCollisionA.dhall | 1 + .../RecursiveRecordTypeMergeTripleCollisionB.dhall | 1 + .../type-inference/success/regression/TodoA.dhall | 1 + .../type-inference/success/regression/TodoB.dhall | 1 + tests_buffer | 23 --------------------- 50 files changed, 70 insertions(+), 23 deletions(-) create mode 100644 dhall/tests/normalization/success/regression/NaturalFoldExtraArgA.dhall create mode 100644 dhall/tests/normalization/success/regression/NaturalFoldExtraArgB.dhall create mode 100644 dhall/tests/normalization/success/regression/TrickyBinderIdentityA.dhall create mode 100644 dhall/tests/normalization/success/regression/TrickyBinderIdentityB.dhall create mode 100644 dhall/tests/normalization/success/unit/TextLitNested1A.dhall create mode 100644 dhall/tests/normalization/success/unit/TextLitNested1B.dhall create mode 100644 dhall/tests/normalization/success/unit/TextLitNested2A.dhall create mode 100644 dhall/tests/normalization/success/unit/TextLitNested2B.dhall create mode 100644 dhall/tests/normalization/success/unit/TextLitNested3A.dhall create mode 100644 dhall/tests/normalization/success/unit/TextLitNested3B.dhall create mode 100644 dhall/tests/normalization/success/unit/TextShowEmptyA.dhall create mode 100644 dhall/tests/normalization/success/unit/TextShowEmptyB.dhall create mode 100644 dhall/tests/parser/failure/unit/AssertNoAnnotation.dhall create mode 100644 dhall/tests/parser/success/unit/EmptyRecordLiteralA.dhall create mode 100644 dhall/tests/parser/success/unit/EmptyRecordLiteralB.dhallb create mode 100644 dhall/tests/parser/success/unit/EmptyRecordLiteralB.diag create mode 100644 dhall/tests/parser/success/unit/LetAnnotA.dhall create mode 100644 dhall/tests/parser/success/unit/LetAnnotB.dhallb create mode 100644 dhall/tests/parser/success/unit/LetAnnotB.diag create mode 100644 dhall/tests/parser/success/unit/LetNoAnnotA.dhall create mode 100644 dhall/tests/parser/success/unit/LetNoAnnotB.dhallb create mode 100644 dhall/tests/parser/success/unit/LetNoAnnotB.diag create mode 100644 dhall/tests/parser/success/unit/ToMapA.dhall create mode 100644 dhall/tests/parser/success/unit/ToMapAnnotA.dhall create mode 100644 dhall/tests/parser/success/unit/ToMapAnnotB.dhallb create mode 100644 dhall/tests/parser/success/unit/ToMapAnnotB.diag create mode 100644 dhall/tests/parser/success/unit/ToMapB.dhallb create mode 100644 dhall/tests/parser/success/unit/ToMapB.diag create mode 100644 dhall/tests/parser/success/unit/VariableQuotedWithSpaceA.dhall create mode 100644 dhall/tests/parser/success/unit/VariableQuotedWithSpaceB.dhallb create mode 100644 dhall/tests/parser/success/unit/VariableQuotedWithSpaceB.diag 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 'tests_buffer') 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 new file mode 100644 index 0000000..4e3a7e4 Binary files /dev/null and b/dhall/tests/parser/success/unit/LetAnnotB.dhallb differ 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 new file mode 100644 index 0000000..79a2384 Binary files /dev/null and b/dhall/tests/parser/success/unit/LetNoAnnotB.dhallb differ 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 new file mode 100644 index 0000000..4b53587 Binary files /dev/null and b/dhall/tests/parser/success/unit/ToMapAnnotB.dhallb differ 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 new file mode 100644 index 0000000..25ecd95 Binary files /dev/null and b/dhall/tests/parser/success/unit/ToMapB.dhallb differ 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 new file mode 100644 index 0000000..56d9cd9 Binary files /dev/null and b/dhall/tests/parser/success/unit/VariableQuotedWithSpaceB.dhallb differ 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` + --> :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 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" -- cgit v1.3.1 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/build.rs | 2 ++ dhall/tests/import/success/unit/asLocation/AbsoluteA.dhall | 1 + dhall/tests/import/success/unit/asLocation/AbsoluteB.dhall | 2 ++ dhall/tests/import/success/unit/asLocation/Canonicalize1A.dhall | 1 + dhall/tests/import/success/unit/asLocation/Canonicalize1B.dhall | 2 ++ dhall/tests/import/success/unit/asLocation/Canonicalize2A.dhall | 1 + dhall/tests/import/success/unit/asLocation/Canonicalize2B.dhall | 2 ++ dhall/tests/import/success/unit/asLocation/Canonicalize3A.dhall | 1 + dhall/tests/import/success/unit/asLocation/Canonicalize3B.dhall | 2 ++ dhall/tests/import/success/unit/asLocation/Canonicalize4A.dhall | 1 + dhall/tests/import/success/unit/asLocation/Canonicalize4B.dhall | 2 ++ dhall/tests/import/success/unit/asLocation/Canonicalize5A.dhall | 1 + dhall/tests/import/success/unit/asLocation/Canonicalize5B.dhall | 2 ++ dhall/tests/import/success/unit/asLocation/Chain1A.dhall | 1 + dhall/tests/import/success/unit/asLocation/Chain1B.dhall | 2 ++ dhall/tests/import/success/unit/asLocation/Chain2A.dhall | 1 + dhall/tests/import/success/unit/asLocation/Chain2B.dhall | 2 ++ dhall/tests/import/success/unit/asLocation/Chain3A.dhall | 1 + dhall/tests/import/success/unit/asLocation/Chain3B.dhall | 2 ++ dhall/tests/import/success/unit/asLocation/DontTryResolvingA.dhall | 1 + dhall/tests/import/success/unit/asLocation/DontTryResolvingB.dhall | 1 + dhall/tests/import/success/unit/asLocation/EnvA.dhall | 1 + dhall/tests/import/success/unit/asLocation/EnvB.dhall | 2 ++ dhall/tests/import/success/unit/asLocation/HashA.dhall | 1 + dhall/tests/import/success/unit/asLocation/HashB.dhall | 2 ++ dhall/tests/import/success/unit/asLocation/HomeA.dhall | 1 + dhall/tests/import/success/unit/asLocation/HomeB.dhall | 2 ++ dhall/tests/import/success/unit/asLocation/MissingA.dhall | 1 + dhall/tests/import/success/unit/asLocation/MissingB.dhall | 1 + dhall/tests/import/success/unit/asLocation/RelativeA.dhall | 1 + dhall/tests/import/success/unit/asLocation/RelativeB.dhall | 2 ++ dhall/tests/import/success/unit/asLocation/RemoteA.dhall | 1 + dhall/tests/import/success/unit/asLocation/RemoteB.dhall | 2 ++ dhall/tests/type-inference/success/CacheImportsA.dhall | 1 + dhall/tests/type-inference/success/CacheImportsB.dhall | 1 + tests_buffer | 2 +- 36 files changed, 51 insertions(+), 1 deletion(-) create mode 100644 dhall/tests/import/success/unit/asLocation/AbsoluteA.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/AbsoluteB.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/Canonicalize1A.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/Canonicalize1B.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/Canonicalize2A.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/Canonicalize2B.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/Canonicalize3A.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/Canonicalize3B.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/Canonicalize4A.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/Canonicalize4B.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/Canonicalize5A.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/Canonicalize5B.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/Chain1A.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/Chain1B.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/Chain2A.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/Chain2B.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/Chain3A.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/Chain3B.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/DontTryResolvingA.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/DontTryResolvingB.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/EnvA.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/EnvB.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/HashA.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/HashB.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/HomeA.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/HomeB.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/MissingA.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/MissingB.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/RelativeA.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/RelativeB.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/RemoteA.dhall create mode 100644 dhall/tests/import/success/unit/asLocation/RemoteB.dhall create mode 100644 dhall/tests/type-inference/success/CacheImportsA.dhall create mode 100644 dhall/tests/type-inference/success/CacheImportsB.dhall (limited to 'tests_buffer') diff --git a/dhall/build.rs b/dhall/build.rs index 884a4cd..137ef02 100644 --- a/dhall/build.rs +++ b/dhall/build.rs @@ -321,6 +321,8 @@ fn generate_tests() -> std::io::Result<()> { // Too slow, but also not all features implemented // For now needs support for hashed imports || path == "prelude" + // TODO: imports + || path == "CacheImports" }), input_type: FileType::Text, output_type: Some(FileType::Text), diff --git a/dhall/tests/import/success/unit/asLocation/AbsoluteA.dhall b/dhall/tests/import/success/unit/asLocation/AbsoluteA.dhall new file mode 100644 index 0000000..dcf45d1 --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/AbsoluteA.dhall @@ -0,0 +1 @@ +/absolute/import as Location diff --git a/dhall/tests/import/success/unit/asLocation/AbsoluteB.dhall b/dhall/tests/import/success/unit/asLocation/AbsoluteB.dhall new file mode 100644 index 0000000..1c1add7 --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/AbsoluteB.dhall @@ -0,0 +1,2 @@ +< Environment : Text | Remote : Text | Local : Text | Missing >.Local + "/absolute/import" diff --git a/dhall/tests/import/success/unit/asLocation/Canonicalize1A.dhall b/dhall/tests/import/success/unit/asLocation/Canonicalize1A.dhall new file mode 100644 index 0000000..e636ed1 --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/Canonicalize1A.dhall @@ -0,0 +1 @@ +./foo/./bar/import.dhall as Location diff --git a/dhall/tests/import/success/unit/asLocation/Canonicalize1B.dhall b/dhall/tests/import/success/unit/asLocation/Canonicalize1B.dhall new file mode 100644 index 0000000..3a8a926 --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/Canonicalize1B.dhall @@ -0,0 +1,2 @@ +< Environment : Text | Remote : Text | Local : Text | Missing >.Local + "./dhall/tests/import/success/unit/asLocation/foo/bar/import.dhall" diff --git a/dhall/tests/import/success/unit/asLocation/Canonicalize2A.dhall b/dhall/tests/import/success/unit/asLocation/Canonicalize2A.dhall new file mode 100644 index 0000000..c6ef89f --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/Canonicalize2A.dhall @@ -0,0 +1 @@ +./foo/baz/../bar/import.dhall as Location diff --git a/dhall/tests/import/success/unit/asLocation/Canonicalize2B.dhall b/dhall/tests/import/success/unit/asLocation/Canonicalize2B.dhall new file mode 100644 index 0000000..3a8a926 --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/Canonicalize2B.dhall @@ -0,0 +1,2 @@ +< Environment : Text | Remote : Text | Local : Text | Missing >.Local + "./dhall/tests/import/success/unit/asLocation/foo/bar/import.dhall" diff --git a/dhall/tests/import/success/unit/asLocation/Canonicalize3A.dhall b/dhall/tests/import/success/unit/asLocation/Canonicalize3A.dhall new file mode 100644 index 0000000..e6be780 --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/Canonicalize3A.dhall @@ -0,0 +1 @@ +./../bar/import.dhall as Location diff --git a/dhall/tests/import/success/unit/asLocation/Canonicalize3B.dhall b/dhall/tests/import/success/unit/asLocation/Canonicalize3B.dhall new file mode 100644 index 0000000..b223da6 --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/Canonicalize3B.dhall @@ -0,0 +1,2 @@ +< Environment : Text | Remote : Text | Local : Text | Missing >.Local + "./dhall/tests/import/success/unit/bar/import.dhall" diff --git a/dhall/tests/import/success/unit/asLocation/Canonicalize4A.dhall b/dhall/tests/import/success/unit/asLocation/Canonicalize4A.dhall new file mode 100644 index 0000000..ffccd47 --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/Canonicalize4A.dhall @@ -0,0 +1 @@ +../../bar/import.dhall as Location diff --git a/dhall/tests/import/success/unit/asLocation/Canonicalize4B.dhall b/dhall/tests/import/success/unit/asLocation/Canonicalize4B.dhall new file mode 100644 index 0000000..b6301f8 --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/Canonicalize4B.dhall @@ -0,0 +1,2 @@ +< Environment : Text | Remote : Text | Local : Text | Missing >.Local + "./dhall/tests/import/success/bar/import.dhall" diff --git a/dhall/tests/import/success/unit/asLocation/Canonicalize5A.dhall b/dhall/tests/import/success/unit/asLocation/Canonicalize5A.dhall new file mode 100644 index 0000000..7e58f0b --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/Canonicalize5A.dhall @@ -0,0 +1 @@ +./foo/../../bar/import.dhall as Location diff --git a/dhall/tests/import/success/unit/asLocation/Canonicalize5B.dhall b/dhall/tests/import/success/unit/asLocation/Canonicalize5B.dhall new file mode 100644 index 0000000..b223da6 --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/Canonicalize5B.dhall @@ -0,0 +1,2 @@ +< Environment : Text | Remote : Text | Local : Text | Missing >.Local + "./dhall/tests/import/success/unit/bar/import.dhall" diff --git a/dhall/tests/import/success/unit/asLocation/Chain1A.dhall b/dhall/tests/import/success/unit/asLocation/Chain1A.dhall new file mode 100644 index 0000000..7b20bc3 --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/Chain1A.dhall @@ -0,0 +1 @@ +./RelativeA.dhall diff --git a/dhall/tests/import/success/unit/asLocation/Chain1B.dhall b/dhall/tests/import/success/unit/asLocation/Chain1B.dhall new file mode 100644 index 0000000..6aee0b5 --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/Chain1B.dhall @@ -0,0 +1,2 @@ +< Environment : Text | Local : Text | Missing | Remote : Text >.Local + "./dhall/tests/import/success/unit/asLocation/some/import.dhall" diff --git a/dhall/tests/import/success/unit/asLocation/Chain2A.dhall b/dhall/tests/import/success/unit/asLocation/Chain2A.dhall new file mode 100644 index 0000000..cdbd10d --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/Chain2A.dhall @@ -0,0 +1 @@ +./Canonicalize4A.dhall diff --git a/dhall/tests/import/success/unit/asLocation/Chain2B.dhall b/dhall/tests/import/success/unit/asLocation/Chain2B.dhall new file mode 100644 index 0000000..6aba54e --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/Chain2B.dhall @@ -0,0 +1,2 @@ +< Environment : Text | Local : Text | Missing | Remote : Text >.Local + "./dhall/tests/import/success/bar/import.dhall" diff --git a/dhall/tests/import/success/unit/asLocation/Chain3A.dhall b/dhall/tests/import/success/unit/asLocation/Chain3A.dhall new file mode 100644 index 0000000..b44f0d4 --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/Chain3A.dhall @@ -0,0 +1 @@ +./../asLocation/Canonicalize4A.dhall diff --git a/dhall/tests/import/success/unit/asLocation/Chain3B.dhall b/dhall/tests/import/success/unit/asLocation/Chain3B.dhall new file mode 100644 index 0000000..6aba54e --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/Chain3B.dhall @@ -0,0 +1,2 @@ +< Environment : Text | Local : Text | Missing | Remote : Text >.Local + "./dhall/tests/import/success/bar/import.dhall" diff --git a/dhall/tests/import/success/unit/asLocation/DontTryResolvingA.dhall b/dhall/tests/import/success/unit/asLocation/DontTryResolvingA.dhall new file mode 100644 index 0000000..e70016c --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/DontTryResolvingA.dhall @@ -0,0 +1 @@ +(missing as Location) ? 42 -- `missing` fails as an import, but definitely resolves as Location diff --git a/dhall/tests/import/success/unit/asLocation/DontTryResolvingB.dhall b/dhall/tests/import/success/unit/asLocation/DontTryResolvingB.dhall new file mode 100644 index 0000000..dd5e798 --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/DontTryResolvingB.dhall @@ -0,0 +1 @@ +< Environment : Text | Remote : Text | Local : Text | Missing >.Missing diff --git a/dhall/tests/import/success/unit/asLocation/EnvA.dhall b/dhall/tests/import/success/unit/asLocation/EnvA.dhall new file mode 100644 index 0000000..eb4b4a6 --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/EnvA.dhall @@ -0,0 +1 @@ +env:HOME as Location diff --git a/dhall/tests/import/success/unit/asLocation/EnvB.dhall b/dhall/tests/import/success/unit/asLocation/EnvB.dhall new file mode 100644 index 0000000..4947caa --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/EnvB.dhall @@ -0,0 +1,2 @@ +< Environment : Text | Remote : Text | Local : Text | Missing >.Environment + "HOME" diff --git a/dhall/tests/import/success/unit/asLocation/HashA.dhall b/dhall/tests/import/success/unit/asLocation/HashA.dhall new file mode 100644 index 0000000..79f4fda --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/HashA.dhall @@ -0,0 +1 @@ +./some/import.dhall sha256:f9340badf94a684e652e0a384f64363293d8b632d971f3453f7ee22f10ab6e75 as Location diff --git a/dhall/tests/import/success/unit/asLocation/HashB.dhall b/dhall/tests/import/success/unit/asLocation/HashB.dhall new file mode 100644 index 0000000..6aee0b5 --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/HashB.dhall @@ -0,0 +1,2 @@ +< Environment : Text | Local : Text | Missing | Remote : Text >.Local + "./dhall/tests/import/success/unit/asLocation/some/import.dhall" diff --git a/dhall/tests/import/success/unit/asLocation/HomeA.dhall b/dhall/tests/import/success/unit/asLocation/HomeA.dhall new file mode 100644 index 0000000..18cc2cd --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/HomeA.dhall @@ -0,0 +1 @@ +~/some/import.dhall as Location diff --git a/dhall/tests/import/success/unit/asLocation/HomeB.dhall b/dhall/tests/import/success/unit/asLocation/HomeB.dhall new file mode 100644 index 0000000..8b4f0fd --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/HomeB.dhall @@ -0,0 +1,2 @@ +< Environment : Text | Remote : Text | Local : Text | Missing >.Local + "~/some/import.dhall" diff --git a/dhall/tests/import/success/unit/asLocation/MissingA.dhall b/dhall/tests/import/success/unit/asLocation/MissingA.dhall new file mode 100644 index 0000000..e06a30b --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/MissingA.dhall @@ -0,0 +1 @@ +missing as Location diff --git a/dhall/tests/import/success/unit/asLocation/MissingB.dhall b/dhall/tests/import/success/unit/asLocation/MissingB.dhall new file mode 100644 index 0000000..dd5e798 --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/MissingB.dhall @@ -0,0 +1 @@ +< Environment : Text | Remote : Text | Local : Text | Missing >.Missing diff --git a/dhall/tests/import/success/unit/asLocation/RelativeA.dhall b/dhall/tests/import/success/unit/asLocation/RelativeA.dhall new file mode 100644 index 0000000..b514f79 --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/RelativeA.dhall @@ -0,0 +1 @@ +./some/import.dhall as Location diff --git a/dhall/tests/import/success/unit/asLocation/RelativeB.dhall b/dhall/tests/import/success/unit/asLocation/RelativeB.dhall new file mode 100644 index 0000000..b3bd255 --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/RelativeB.dhall @@ -0,0 +1,2 @@ +< Environment : Text | Remote : Text | Local : Text | Missing >.Local + "./dhall/tests/import/success/unit/asLocation/some/import.dhall" diff --git a/dhall/tests/import/success/unit/asLocation/RemoteA.dhall b/dhall/tests/import/success/unit/asLocation/RemoteA.dhall new file mode 100644 index 0000000..e0be314 --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/RemoteA.dhall @@ -0,0 +1 @@ +https://prelude.dhall-lang.org/package.dhall as Location diff --git a/dhall/tests/import/success/unit/asLocation/RemoteB.dhall b/dhall/tests/import/success/unit/asLocation/RemoteB.dhall new file mode 100644 index 0000000..8ab6366 --- /dev/null +++ b/dhall/tests/import/success/unit/asLocation/RemoteB.dhall @@ -0,0 +1,2 @@ +< Environment : Text | Remote : Text | Local : Text | Missing >.Remote + "https://prelude.dhall-lang.org/package.dhall" 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 diff --git a/tests_buffer b/tests_buffer index 6f6e67e..d7c8e84 100644 --- a/tests_buffer +++ b/tests_buffer @@ -19,7 +19,7 @@ failure/ normalization: variables across import boundaries -typecheck: +type-inference: something that involves destructuring a recordtype after merge add some of the more complicated Prelude tests back, like List/enumerate success/ -- cgit v1.3.1 From 81ce30dde067ca0067fda32b1e0ade1dbdfbdf58 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 29 Feb 2020 23:21:18 +0000 Subject: Implement `as Location` imports --- dhall/build.rs | 1 + dhall/src/semantics/resolve/hir.rs | 3 + dhall/src/semantics/resolve/resolve.rs | 129 ++++++++++++++++----- dhall/src/syntax/ast/text.rs | 29 ----- .../import/success/unit/asLocation/Chain3A.dhall | 2 +- tests_buffer | 1 + 6 files changed, 105 insertions(+), 60 deletions(-) (limited to 'tests_buffer') diff --git a/dhall/build.rs b/dhall/build.rs index 137ef02..2c70b89 100644 --- a/dhall/build.rs +++ b/dhall/build.rs @@ -258,6 +258,7 @@ fn generate_tests() -> std::io::Result<()> { || path == "hashFromCache" || path == "headerForwarding" || path == "noHeaderForwarding" + || path == "unit/asLocation/Remote" }), input_type: FileType::Text, output_type: Some(FileType::Text), diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs index 2f3464a..317708a 100644 --- a/dhall/src/semantics/resolve/hir.rs +++ b/dhall/src/semantics/resolve/hir.rs @@ -72,6 +72,9 @@ impl Hir { ) -> Result, TypeError> { type_with(env, self, None) } + pub fn typecheck_noenv<'hir>(&'hir self) -> Result, TypeError> { + self.typecheck(&TyEnv::new()) + } /// Eval the Hir. It will actually get evaluated only as needed on demand. pub fn eval(&self, env: impl Into) -> Nir { diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs index 82800ec..b27dd2c 100644 --- a/dhall/src/semantics/resolve/resolve.rs +++ b/dhall/src/semantics/resolve/resolve.rs @@ -1,3 +1,4 @@ +use itertools::Itertools; use std::borrow::Cow; use std::path::{Path, PathBuf}; @@ -5,7 +6,11 @@ use crate::error::ErrorBuilder; use crate::error::{Error, ImportError}; use crate::semantics::{mkerr, Hir, HirKind, ImportEnv, NameEnv, Type}; use crate::syntax; -use crate::syntax::{BinOp, Expr, ExprKind, FilePath, ImportLocation, URL}; +use crate::syntax::map::DupTreeMap; +use crate::syntax::{ + BinOp, Builtin, Expr, ExprKind, FilePath, FilePrefix, ImportLocation, + ImportMode, Span, URL, +}; use crate::{Parsed, ParsedExpr, Resolved}; // TODO: evaluate import headers @@ -25,24 +30,95 @@ fn resolve_one_import( import: &Import, root: &ImportRoot, ) -> Result { - use self::ImportRoot::*; - use syntax::FilePrefix::*; - use syntax::ImportLocation::*; let cwd = match root { - LocalDir(cwd) => cwd, + ImportRoot::LocalDir(cwd) => cwd, }; - match &import.location { - Local(prefix, path) => { - let path_buf: PathBuf = path.file_path.iter().collect(); - let path_buf = match prefix { - // TODO: fail gracefully - Parent => cwd.parent().unwrap().join(path_buf), - Here => cwd.join(path_buf), + + match import.mode { + ImportMode::Code => { + match &import.location { + ImportLocation::Local(prefix, path) => { + let path_buf: PathBuf = path.file_path.iter().collect(); + let path_buf = match prefix { + // TODO: fail gracefully + FilePrefix::Parent => { + cwd.parent().unwrap().join(path_buf) + } + FilePrefix::Here => cwd.join(path_buf), + _ => unimplemented!("{:?}", import), + }; + Ok(load_import(env, &path_buf)?) + } + _ => unimplemented!("{:?}", import), + } + } + ImportMode::RawText => unimplemented!("{:?}", import), + ImportMode::Location => { + let mkexpr = |kind| Expr::new(kind, Span::Artificial); + let text_type = mkexpr(ExprKind::Builtin(Builtin::Text)); + let mut location_union = DupTreeMap::default(); + location_union.insert("Local".into(), Some(text_type.clone())); + location_union.insert("Remote".into(), Some(text_type.clone())); + location_union + .insert("Environment".into(), Some(text_type.clone())); + location_union.insert("Missing".into(), None); + let location_union = mkexpr(ExprKind::UnionType(location_union)); + + let expr = match &import.location { + ImportLocation::Local(prefix, path) => { + let mut cwd: Vec = cwd + .components() + .map(|component| { + component.as_os_str().to_string_lossy().into_owned() + }) + .collect(); + let root = match prefix { + FilePrefix::Here => cwd, + FilePrefix::Parent => { + cwd.push("..".to_string()); + cwd + } + FilePrefix::Absolute => vec![], + FilePrefix::Home => vec![], + }; + let path: Vec<_> = root + .into_iter() + .chain(path.file_path.iter().cloned()) + .collect(); + let path = + (FilePath { file_path: path }).canonicalize().file_path; + let prefix = match prefix { + FilePrefix::Here | FilePrefix::Parent => ".", + FilePrefix::Absolute => "", + FilePrefix::Home => "~", + }; + let path = Some(prefix.to_string()) + .into_iter() + .chain(path) + .join("/"); + + mkexpr(ExprKind::App( + mkexpr(ExprKind::Field(location_union, "Local".into())), + mkexpr(ExprKind::TextLit(path.into())), + )) + } + ImportLocation::Env(name) => mkexpr(ExprKind::App( + mkexpr(ExprKind::Field( + location_union, + "Environment".into(), + )), + mkexpr(ExprKind::TextLit(name.clone().into())), + )), + ImportLocation::Missing => { + mkexpr(ExprKind::Field(location_union, "Missing".into())) + } _ => unimplemented!("{:?}", import), }; - Ok(load_import(env, &path_buf)?) + + let hir = skip_resolve(&expr)?; + let ty = hir.typecheck_noenv()?.ty().clone(); + Ok((hir, ty)) } - _ => unimplemented!("{:?}", import), } } @@ -166,21 +242,15 @@ pub trait Canonicalize { impl Canonicalize for FilePath { fn canonicalize(&self) -> FilePath { let mut file_path = Vec::new(); - let mut file_path_components = self.file_path.clone().into_iter(); - - loop { - let component = file_path_components.next(); - match component.as_ref() { - // ─────────────────── - // canonicalize(ε) = ε - None => break, + for c in &self.file_path { + match c.as_ref() { // canonicalize(directory₀) = directory₁ // ─────────────────────────────────────── // canonicalize(directory₀/.) = directory₁ - Some(c) if c == "." => continue, + "." => continue, - Some(c) if c == ".." => match file_path_components.next() { + ".." => match file_path.last() { // canonicalize(directory₀) = ε // ──────────────────────────── // canonicalize(directory₀/..) = /.. @@ -189,21 +259,20 @@ impl Canonicalize for FilePath { // canonicalize(directory₀) = directory₁/.. // ────────────────────────────────────────────── // canonicalize(directory₀/..) = directory₁/../.. - Some(ref c) if c == ".." => { - file_path.push("..".to_string()); - file_path.push("..".to_string()); - } + Some(c) if c == ".." => file_path.push("..".to_string()), // canonicalize(directory₀) = directory₁/component // ─────────────────────────────────────────────── ; If "component" is not // canonicalize(directory₀/..) = directory₁ ; ".." - Some(_) => continue, + Some(_) => { + file_path.pop(); + } }, // canonicalize(directory₀) = directory₁ // ───────────────────────────────────────────────────────── ; If no other // canonicalize(directory₀/component) = directory₁/component ; rule matches - Some(c) => file_path.push(c.clone()), + _ => file_path.push(c.clone()), } } diff --git a/dhall/src/syntax/ast/text.rs b/dhall/src/syntax/ast/text.rs index 83aaf9a..c40f4a1 100644 --- a/dhall/src/syntax/ast/text.rs +++ b/dhall/src/syntax/ast/text.rs @@ -54,16 +54,6 @@ impl InterpolatedTextContents { Text(s) => Text(s.clone()), }) } - pub fn traverse_mut<'a, E, F>(&'a mut self, mut f: F) -> Result<(), E> - where - F: FnMut(&'a mut SubExpr) -> Result<(), E>, - { - use InterpolatedTextContents::Expr; - if let Expr(e) = self { - f(e)?; - } - Ok(()) - } pub fn map_ref<'a, SubExpr2, F>( &'a self, mut f: F, @@ -77,15 +67,6 @@ impl InterpolatedTextContents { Text(s) => Text(s.clone()), } } - pub fn map_mut<'a, F>(&'a mut self, mut f: F) - where - F: FnMut(&'a mut SubExpr), - { - use InterpolatedTextContents::Expr; - if let Expr(e) = self { - f(e); - } - } } impl InterpolatedText { @@ -126,16 +107,6 @@ impl InterpolatedText { }) } - pub fn traverse_mut<'a, E, F>(&'a mut self, mut f: F) -> Result<(), E> - where - F: FnMut(&'a mut SubExpr) -> Result<(), E>, - { - for (e, _) in &mut self.tail { - f(e)? - } - Ok(()) - } - pub fn iter<'a>( &'a self, ) -> impl Iterator> + 'a { diff --git a/dhall/tests/import/success/unit/asLocation/Chain3A.dhall b/dhall/tests/import/success/unit/asLocation/Chain3A.dhall index b44f0d4..57751f6 100644 --- a/dhall/tests/import/success/unit/asLocation/Chain3A.dhall +++ b/dhall/tests/import/success/unit/asLocation/Chain3A.dhall @@ -1 +1 @@ -./../asLocation/Canonicalize4A.dhall +../asLocation/Canonicalize4A.dhall diff --git a/tests_buffer b/tests_buffer index d7c8e84..478edbb 100644 --- a/tests_buffer +++ b/tests_buffer @@ -15,6 +15,7 @@ success/ recover recursive import error failure/ don't recover cycle + don't resolve symlinks in canonicalizing normalization: variables across import boundaries -- cgit v1.3.1