diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,37 @@ +1.14.0 + +* BREAKING CHANGE TO THE LANGUAGE: Switch grammar of `Natural` and `Integer` + * `Natural` number literals are now unsigned and `Integer` literals always + require a sign + * This is a **VERY** disruptive change to most Dhall code in the wild but + was unanimously agreed upon here: + https://github.com/dhall-lang/dhall-lang/issues/138 + * See also: https://github.com/dhall-lang/dhall-haskell/pull/381 +* BREAKING CHANGE TO THE LANGUAGE: Drop support for importing directories + * Importing `dir/` used to resolve to `dir/@`, which is no longer supported + * See: https://github.com/dhall-lang/dhall-haskell/pull/384 +* BREAKING CHANGE TO THE LANGUAGE: Change to the grammar for imports + * File path components can no longer contain `#` or `?` characters + * URL imports must now contain at least one path component + * URL path components must match the grammar for file path components + * See: https://github.com/dhall-lang/dhall-haskell/pull/390 +* BREAKING CHANGE TO THE API: Rename `Path{,Mode,Hashed,Type}` to + `Import{,Mode,Hashed,Type}` + * In practice this change is not breaking for the most common use cases + since this also provides a `Path` type synonym for backwards compatibility + * See: https://github.com/dhall-lang/dhall-haskell/pull/376 +* BUG FIX: Fix α-equivalence bug when type-checking `merge` + * `merge` expressions would sometimes reject valid code due to a + type-checking bug + * See: https://github.com/dhall-lang/dhall-haskell/pull/394 +* Improve import caching + * See: https://github.com/dhall-lang/dhall-haskell/pull/388 + * See: https://github.com/dhall-lang/dhall-haskell/pull/392 +* Increase upper bound on `tasty` + * See: https://github.com/dhall-lang/dhall-haskell/pull/382 +* Fix lower bound on `insert-ordered-containers` + * See: https://github.com/dhall-lang/dhall-haskell/pull/377 + 1.13.1 * Increase upper bound on `ansi-terminal` and `megaparsec` diff --git a/Prelude/Bool/fold b/Prelude/Bool/fold --- a/Prelude/Bool/fold +++ b/Prelude/Bool/fold @@ -4,9 +4,9 @@ Examples: ``` -./fold True Integer 0 1 = 0 +./fold True Natural 0 1 = 0 -./fold False Integer 0 1 = 1 +./fold False Natural 0 1 = 1 ``` -} let fold diff --git a/Prelude/Integer/show b/Prelude/Integer/show --- a/Prelude/Integer/show +++ b/Prelude/Integer/show @@ -1,13 +1,14 @@ {- Render an `Integer` as `Text` using the same representation as Dhall source -code (i.e. a decimal number with a leading `-` sign if negative) +code (i.e. a decimal number with a leading `-` sign if negative and a leading +`+` sign if non-negative) Examples: ``` ./show -3 = "-3" -./show 0 = "0" +./show +0 = "+0" ``` -} let show : Integer → Text = Integer/show in show diff --git a/Prelude/List/all b/Prelude/List/all --- a/Prelude/List/all +++ b/Prelude/List/all @@ -5,7 +5,7 @@ Examples: ``` -./all Natural Natural/even [ +2, +3, +5 ] = False +./all Natural Natural/even [ 2, 3, 5 ] = False ./all Natural Natural/even ([] : List Natural) = True ``` diff --git a/Prelude/List/any b/Prelude/List/any --- a/Prelude/List/any +++ b/Prelude/List/any @@ -5,7 +5,7 @@ Examples: ``` -./any Natural Natural/even [ +2, +3, +5 ] = True +./any Natural Natural/even [ 2, 3, 5 ] = True ./any Natural Natural/even ([] : List Natural) = False ``` diff --git a/Prelude/List/concat b/Prelude/List/concat --- a/Prelude/List/concat +++ b/Prelude/List/concat @@ -4,22 +4,22 @@ Examples: ``` -./concat Integer +./concat Natural [ [0, 1, 2] , [3, 4] , [5, 6, 7, 8] ] = [ 0, 1, 2, 3, 4, 5, 6, 7, 8 ] -./concat Integer -( [ [] : List Integer - , [] : List Integer - , [] : List Integer +./concat Natural +( [ [] : List Natural + , [] : List Natural + , [] : List Natural ] ) -= [] : List Integer += [] : List Natural -./concat Integer ([] : List (List Integer)) = [] : List Integer +./concat Natural ([] : List (List Natural)) = [] : List Natural ``` -} let concat diff --git a/Prelude/List/concatMap b/Prelude/List/concatMap --- a/Prelude/List/concatMap +++ b/Prelude/List/concatMap @@ -5,8 +5,8 @@ Examples: ``` -./concatMap Natural Natural (λ(n : Natural) → [n, n]) [+2, +3, +5] -= [ +2, +2, +3, +3, +5, +5 ] +./concatMap Natural Natural (λ(n : Natural) → [n, n]) [2, 3, 5] += [ 2, 2, 3, 3, 5, 5 ] ./concatMap Natural Natural (λ(n : Natural) → [n, n]) ([] : List Natural) = [] : List Natural diff --git a/Prelude/List/filter b/Prelude/List/filter --- a/Prelude/List/filter +++ b/Prelude/List/filter @@ -4,11 +4,11 @@ Examples: ``` -./filter Natural Natural/even [+2, +3, +5] -= [ +2 ] +./filter Natural Natural/even [ 2, 3, 5 ] += [ 2 ] -./filter Natural Natural/odd [+2, +3, +5] -= [ +3, +5 ] +./filter Natural Natural/odd [ 2, 3, 5 ] += [ 3, 5 ] ``` -} let filter diff --git a/Prelude/List/fold b/Prelude/List/fold --- a/Prelude/List/fold +++ b/Prelude/List/fold @@ -9,29 +9,29 @@ ``` ./fold Natural - [ +2, +3, +5 ] + [ 2, 3, 5 ] Natural (λ(x : Natural) → λ(y : Natural) → x + y) - +0 -= +10 + 0 += 10 λ(nil : Natural) → ./fold Natural - [ +2, +3, +5 ] + [ 2, 3, 5 ] Natural (λ(x : Natural) → λ(y : Natural) → x + y) nil -= λ(nil : Natural) → +2 + +3 + +5 + nil += λ(nil : Natural) → 2 + 3 + 5 + nil λ(list : Type) → λ(cons : Natural → list → list) → λ(nil : list) -→ ./fold Natural [ +2, +3, +5 ] list cons nil +→ ./fold Natural [ 2, 3, 5 ] list cons nil = λ(list : Type) → λ(cons : Natural → list → list) → λ(nil : list) -→ cons +2 (cons +3 (cons +5 nil)) +→ cons 2 (cons 3 (cons 5 nil)) ``` -} let fold diff --git a/Prelude/List/generate b/Prelude/List/generate --- a/Prelude/List/generate +++ b/Prelude/List/generate @@ -1,13 +1,13 @@ {- -Build a list by calling the supplied function on all `Natural` numbers from `+0` +Build a list by calling the supplied function on all `Natural` numbers from `0` up to but not including the supplied `Natural` number Examples: ``` -./generate +5 Bool Natural/even = [ True, False, True, False, True ] +./generate 5 Bool Natural/even = [ True, False, True, False, True ] -./generate +0 Bool Natural/even = [] : List Bool +./generate 0 Bool Natural/even = [] : List Bool ``` -} let generate diff --git a/Prelude/List/head b/Prelude/List/head --- a/Prelude/List/head +++ b/Prelude/List/head @@ -4,9 +4,9 @@ Examples: ``` -./head Integer [ 0, 1, 2 ] = [ 0 ] : Optional Integer +./head Natural [ 0, 1, 2 ] = [ 0 ] : Optional Natural -./head Integer ([] : List Integer) = [] : Optional Integer +./head Natural ([] : List Natural) = [] : Optional Natural ``` -} let head : ∀(a : Type) → List a → Optional a = List/head in head diff --git a/Prelude/List/indexed b/Prelude/List/indexed --- a/Prelude/List/indexed +++ b/Prelude/List/indexed @@ -5,9 +5,9 @@ ``` ./indexed Bool [ True, False, True ] -= [ { index = +0, value = True } - , { index = +1, value = False } - , { index = +2, value = True } += [ { index = 0, value = True } + , { index = 1, value = False } + , { index = 2, value = True } ] : List { index : Natural, value : Bool } ./indexed Bool ([] : List Bool) diff --git a/Prelude/List/iterate b/Prelude/List/iterate --- a/Prelude/List/iterate +++ b/Prelude/List/iterate @@ -5,10 +5,10 @@ Examples: ``` -./iterate +10 Natural (λ(x : Natural) → x * +2) +1 -= [ +1, +2, +4, +8, +16, +32, +64, +128, +256, +512 ] +./iterate 10 Natural (λ(x : Natural) → x * 2) 1 += [ 1, 2, 4, 8, 16, 32, 64, 128, 256, 512 ] -./iterate +0 Natural (λ(x : Natural) → x * +2) +1 +./iterate 0 Natural (λ(x : Natural) → x * 2) 1 = [] : List Natural ``` -} diff --git a/Prelude/List/last b/Prelude/List/last --- a/Prelude/List/last +++ b/Prelude/List/last @@ -4,9 +4,9 @@ Examples: ``` -./last Integer [ 0, 1, 2 ] = [ 2 ] : Optional Integer +./last Natural [ 0, 1, 2 ] = [ 2 ] : Optional Natural -./last Integer ([] : List Integer) = [] : Optional Integer +./last Natural ([] : List Natural) = [] : Optional Natural ``` -} let last : ∀(a : Type) → List a → Optional a = List/last in last diff --git a/Prelude/List/length b/Prelude/List/length --- a/Prelude/List/length +++ b/Prelude/List/length @@ -4,9 +4,9 @@ Examples: ``` -./length Integer [ 0, 1, 2 ] = +3 +./length Natural [ 0, 1, 2 ] = 3 -./length Integer ([] : List Integer) = +0 +./length Natural ([] : List Natural) = 0 ``` -} let length : ∀(a : Type) → List a → Natural = List/length in length diff --git a/Prelude/List/map b/Prelude/List/map --- a/Prelude/List/map +++ b/Prelude/List/map @@ -4,7 +4,7 @@ Examples: ``` -./map Natural Bool Natural/even [ +2, +3, +5 ] +./map Natural Bool Natural/even [ 2, 3, 5 ] = [ True, False, False ] ./map Natural Bool Natural/even ([] : List Natural) diff --git a/Prelude/List/null b/Prelude/List/null --- a/Prelude/List/null +++ b/Prelude/List/null @@ -4,9 +4,9 @@ Examples: ``` -./null Integer [ 0, 1, 2 ] = False +./null Natural [ 0, 1, 2 ] = False -./null Integer ([] : List Integer) = True +./null Natural ([] : List Natural) = True ``` -} let null diff --git a/Prelude/List/replicate b/Prelude/List/replicate --- a/Prelude/List/replicate +++ b/Prelude/List/replicate @@ -4,9 +4,9 @@ Examples: ``` -./replicate +9 Integer 1 = [ 1, 1, 1, 1, 1, 1, 1, 1, 1 ] +./replicate 9 Natural 1 = [ 1, 1, 1, 1, 1, 1, 1, 1, 1 ] -./replicate +0 Integer 1 = [] : List Integer +./replicate 0 Natural 1 = [] : List Natural ``` -} let replicate diff --git a/Prelude/List/reverse b/Prelude/List/reverse --- a/Prelude/List/reverse +++ b/Prelude/List/reverse @@ -4,9 +4,9 @@ Examples: ``` -./reverse Integer [ 0, 1, 2 ] = [ 2, 1, 0 ] : List Integer +./reverse Natural [ 0, 1, 2 ] = [ 2, 1, 0 ] : List Natural -./reverse Integer ([] : List Integer) = [] : List Integer +./reverse Natural ([] : List Natural) = [] : List Natural ``` -} let reverse : ∀(a : Type) → List a → List a = List/reverse in reverse diff --git a/Prelude/List/shifted b/Prelude/List/shifted --- a/Prelude/List/shifted +++ b/Prelude/List/shifted @@ -7,28 +7,28 @@ ``` ./shifted Bool -[ [ { index = +0, value = True } - , { index = +1, value = True } - , { index = +2, value = True } +[ [ { index = 0, value = True } + , { index = 1, value = True } + , { index = 2, value = True } ] -, [ { index = +0, value = False } - , { index = +1, value = False } +, [ { index = 0, value = False } + , { index = 1, value = False } ] -, [ { index = +0, value = True } - , { index = +1, value = True } - , { index = +2, value = True } - , { index = +3, value = True } +, [ { index = 0, value = True } + , { index = 1, value = True } + , { index = 2, value = True } + , { index = 3, value = True } ] ] -= [ { index = +0, value = True } - , { index = +1, value = True } - , { index = +2, value = True } - , { index = +3, value = False } - , { index = +4, value = False } - , { index = +5, value = True } - , { index = +6, value = True } - , { index = +7, value = True } - , { index = +8, value = True } += [ { index = 0, value = True } + , { index = 1, value = True } + , { index = 2, value = True } + , { index = 3, value = False } + , { index = 4, value = False } + , { index = 5, value = True } + , { index = 6, value = True } + , { index = 7, value = True } + , { index = 8, value = True } ] ./shifted Bool ([] : List (List { index : Natural, value : Bool })) @@ -79,9 +79,9 @@ (y.diff (n + length)) } ) - { count = +0, diff = λ(_ : Natural) → nil } + { count = 0, diff = λ(_ : Natural) → nil } - in result.diff +0 + in result.diff 0 ) in shifted diff --git a/Prelude/Natural/build b/Prelude/Natural/build --- a/Prelude/Natural/build +++ b/Prelude/Natural/build @@ -10,7 +10,7 @@ → λ(zero : natural) → succ (succ (succ zero)) ) -= +3 += 3 ./build ( λ(natural : Type) @@ -18,7 +18,7 @@ → λ(zero : natural) → zero ) -= +0 += 0 ``` -} let build diff --git a/Prelude/Natural/enumerate b/Prelude/Natural/enumerate --- a/Prelude/Natural/enumerate +++ b/Prelude/Natural/enumerate @@ -1,13 +1,13 @@ {- -Generate a list of numbers from `+0` up to but not including the specified +Generate a list of numbers from `0` up to but not including the specified number Examples: ``` -./enumerate +10 = [ +0, +1, +2, +3, +4, +5, +6, +7, +8, +9 ] +./enumerate 10 = [ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9 ] -./enumerate +0 = [] : List Natural +./enumerate 0 = [] : List Natural ``` -} let enumerate diff --git a/Prelude/Natural/even b/Prelude/Natural/even --- a/Prelude/Natural/even +++ b/Prelude/Natural/even @@ -4,9 +4,9 @@ Examples: ``` -./even +3 = False +./even 3 = False -./even +0 = True +./even 0 = True ``` -} let even : Natural → Bool = Natural/even in even diff --git a/Prelude/Natural/fold b/Prelude/Natural/fold --- a/Prelude/Natural/fold +++ b/Prelude/Natural/fold @@ -1,21 +1,21 @@ {- `fold` is the primitive function for consuming `Natural` numbers -If you treat the number `+3` as `succ (succ (succ zero))` then a `fold` just +If you treat the number `3` as `succ (succ (succ zero))` then a `fold` just replaces each `succ` and `zero` with something else Examples: ``` -./fold +3 Natural (λ(x : Natural) → +5 * x) +1 = +125 +./fold 3 Natural (λ(x : Natural) → 5 * x) 1 = 125 -λ(zero : Natural) → ./fold +3 Natural (λ(x : Natural) → +5 * x) zero -= λ(zero : Natural) → +5 * +5 * +5 * zero +λ(zero : Natural) → ./fold 3 Natural (λ(x : Natural) → 5 * x) zero += λ(zero : Natural) → 5 * 5 * 5 * zero λ(natural : Type) → λ(succ : natural → natural) → λ(zero : natural) -→ ./fold +3 natural succ zero +→ ./fold 3 natural succ zero = λ(natural : Type) → λ(succ : natural → natural) → λ(zero : natural) diff --git a/Prelude/Natural/isZero b/Prelude/Natural/isZero --- a/Prelude/Natural/isZero +++ b/Prelude/Natural/isZero @@ -1,12 +1,12 @@ {- -Returns `True` if a number is `+0` and returns `False` otherwise +Returns `True` if a number is `0` and returns `False` otherwise Examples: ``` -./isZero +2 = False +./isZero 2 = False -./isZero +0 = True +./isZero 0 = True ``` -} let isZero : Natural → Bool = Natural/isZero in isZero diff --git a/Prelude/Natural/odd b/Prelude/Natural/odd --- a/Prelude/Natural/odd +++ b/Prelude/Natural/odd @@ -4,9 +4,9 @@ Examples: ``` -./odd +3 = True +./odd 3 = True -./odd +0 = False +./odd 0 = False ``` -} let odd : Natural → Bool = Natural/odd in odd diff --git a/Prelude/Natural/product b/Prelude/Natural/product --- a/Prelude/Natural/product +++ b/Prelude/Natural/product @@ -4,9 +4,9 @@ Examples: ``` -./product [ +2, +3, +5 ] = +30 +./product [ 2, 3, 5 ] = 30 -./product ([] : List Natural) = +1 +./product ([] : List Natural) = 1 ``` -} let product @@ -17,6 +17,6 @@ xs Natural (λ(l : Natural) → λ(r : Natural) → l * r) - +1 + 1 in product diff --git a/Prelude/Natural/show b/Prelude/Natural/show --- a/Prelude/Natural/show +++ b/Prelude/Natural/show @@ -1,13 +1,13 @@ {- Render a `Natural` number as `Text` using the same representation as Dhall -source code (i.e. a decimal number with a leading `+` sign) +source code (i.e. a decimal number) Examples: ``` -./show +3 = "+3" +./show 3 = "3" -./show +0 = "+0" +./show 0 = "0" ``` -} let show : Natural → Text = Natural/show in show diff --git a/Prelude/Natural/sum b/Prelude/Natural/sum --- a/Prelude/Natural/sum +++ b/Prelude/Natural/sum @@ -4,9 +4,9 @@ Examples: ``` -./sum [ +2, +3, +5 ] = +10 +./sum [ 2, 3, 5 ] = 10 -./sum ([] : List Natural) = +0 +./sum ([] : List Natural) = 0 ``` -} let sum @@ -17,6 +17,6 @@ xs Natural (λ(l : Natural) → λ(r : Natural) → l + r) - +0 + 0 in sum diff --git a/Prelude/Natural/toInteger b/Prelude/Natural/toInteger --- a/Prelude/Natural/toInteger +++ b/Prelude/Natural/toInteger @@ -4,9 +4,9 @@ Examples: ``` -./toInteger +3 = 3 +./toInteger 3 = +3 -./toInteger +0 = 0 +./toInteger 0 = +0 ``` -} let toInteger : Natural → Integer = Natural/toInteger in toInteger diff --git a/Prelude/Optional/all b/Prelude/Optional/all --- a/Prelude/Optional/all +++ b/Prelude/Optional/all @@ -5,7 +5,7 @@ Examples: ``` -./all Natural Natural/even ([ +3 ] : Optional Natural) = False +./all Natural Natural/even ([ 3 ] : Optional Natural) = False ./all Natural Natural/even ([] : Optional Natural) = True ``` diff --git a/Prelude/Optional/any b/Prelude/Optional/any --- a/Prelude/Optional/any +++ b/Prelude/Optional/any @@ -5,7 +5,7 @@ Examples: ``` -./any Natural Natural/even ([ +2 ] : Optional Natural) = True +./any Natural Natural/even ([ 2 ] : Optional Natural) = True ./any Natural Natural/even ([] : Optional Natural) = False ``` diff --git a/Prelude/Optional/build b/Prelude/Optional/build --- a/Prelude/Optional/build +++ b/Prelude/Optional/build @@ -5,22 +5,22 @@ ``` ./build -Integer +Natural ( λ(optional : Type) -→ λ(just : Integer → optional) +→ λ(just : Natural → optional) → λ(nothing : optional) → just 1 ) -= [ 1 ] : Optional Integer += [ 1 ] : Optional Natural ./build -Integer +Natural ( λ(optional : Type) -→ λ(just : Integer → optional) +→ λ(just : Natural → optional) → λ(nothing : optional) → nothing ) -= [] : Optional Integer += [] : Optional Natural ``` -} let build diff --git a/Prelude/Optional/concat b/Prelude/Optional/concat --- a/Prelude/Optional/concat +++ b/Prelude/Optional/concat @@ -4,14 +4,14 @@ Examples: ``` -./concat Integer ([ [ 1 ] : Optional Integer ] : Optional (Optional Integer)) -= [ 1 ] : Optional Integer +./concat Natural ([ [ 1 ] : Optional Natural ] : Optional (Optional Natural)) += [ 1 ] : Optional Natural -./concat Integer ([ [] : Optional Integer ] : Optional (Optional Integer)) -= [] : Optional Integer +./concat Natural ([ [] : Optional Natural ] : Optional (Optional Natural)) += [] : Optional Natural -./concat Integer ([] : Optional (Optional Integer)) -= [] : Optional Integer +./concat Natural ([] : Optional (Optional Natural)) += [] : Optional Natural ``` -} let concat diff --git a/Prelude/Optional/filter b/Prelude/Optional/filter --- a/Prelude/Optional/filter +++ b/Prelude/Optional/filter @@ -4,10 +4,10 @@ Examples: ``` -./filter Natural Natural/even ([ +2 ] : Optional Natural) -= [ +2 ] : Optional Natural +./filter Natural Natural/even ([ 2 ] : Optional Natural) += [ 2 ] : Optional Natural -./filter Natural Natural/odd ([ +2 ] : Optional Natural) +./filter Natural Natural/odd ([ 2 ] : Optional Natural) = [] : Optional Natural ``` -} diff --git a/Prelude/Optional/fold b/Prelude/Optional/fold --- a/Prelude/Optional/fold +++ b/Prelude/Optional/fold @@ -4,9 +4,9 @@ Examples: ``` -./fold Integer ([ 2 ] : Optional Integer) Integer (λ(x : Integer) → x) 0 = 2 +./fold Natural ([ 2 ] : Optional Natural) Natural (λ(x : Natural) → x) 0 = 2 -./fold Integer ([] : Optional Integer) Integer (λ(x : Integer) → x) 0 = 0 +./fold Natural ([] : Optional Natural) Natural (λ(x : Natural) → x) 0 = 0 ``` -} let fold diff --git a/Prelude/Optional/head b/Prelude/Optional/head --- a/Prelude/Optional/head +++ b/Prelude/Optional/head @@ -5,20 +5,20 @@ ``` ./head -Integer -[ [ ] : Optional Integer -, [ 1 ] : Optional Integer -, [ 2 ] : Optional Integer +Natural +[ [ ] : Optional Natural +, [ 1 ] : Optional Natural +, [ 2 ] : Optional Natural ] -= [ 1 ] : Optional Integer += [ 1 ] : Optional Natural ./head -Integer -[ [] : Optional Integer, [] : Optional Integer ] -= [] : Optional Integer +Natural +[ [] : Optional Natural, [] : Optional Natural ] += [] : Optional Natural -./head Integer ([] : List (Optional Integer)) -= [] : Optional Integer +./head Natural ([] : List (Optional Natural)) += [] : Optional Natural ``` -} let head diff --git a/Prelude/Optional/last b/Prelude/Optional/last --- a/Prelude/Optional/last +++ b/Prelude/Optional/last @@ -5,20 +5,20 @@ ``` ./last -Integer -[ [ ] : Optional Integer -, [ 1 ] : Optional Integer -, [ 2 ] : Optional Integer +Natural +[ [ ] : Optional Natural +, [ 1 ] : Optional Natural +, [ 2 ] : Optional Natural ] -= [ 2 ] : Optional Integer += [ 2 ] : Optional Natural ./last -Integer -[ [] : Optional Integer, [] : Optional Integer ] -= [] : Optional Integer +Natural +[ [] : Optional Natural, [] : Optional Natural ] += [] : Optional Natural -./last Integer ([] : List (Optional Integer)) -= [] : Optional Integer +./last Natural ([] : List (Optional Natural)) += [] : Optional Natural ``` -} let last diff --git a/Prelude/Optional/length b/Prelude/Optional/length --- a/Prelude/Optional/length +++ b/Prelude/Optional/length @@ -1,18 +1,18 @@ {- -Returns `+1` if the `Optional` value is present and `+0` if the value is absent +Returns `1` if the `Optional` value is present and `0` if the value is absent Examples: ``` -./length Integer ([ 2 ] : Optional Integer) = +1 +./length Natural ([ 2 ] : Optional Natural) = 1 -./length Integer ([] : Optional Integer) = +0 +./length Natural ([] : Optional Natural) = 0 ``` -} let length : ∀(a : Type) → Optional a → Natural = λ(a : Type) → λ(xs : Optional a) - → Optional/fold a xs Natural (λ(_ : a) → +1) +0 + → Optional/fold a xs Natural (λ(_ : a) → 1) 0 in length diff --git a/Prelude/Optional/map b/Prelude/Optional/map --- a/Prelude/Optional/map +++ b/Prelude/Optional/map @@ -4,7 +4,7 @@ Examples: ``` -./map Natural Bool Natural/even ([ +3 ] : Optional Natural) +./map Natural Bool Natural/even ([ 3 ] : Optional Natural) = [ False ] : Optional Bool ./map Natural Bool Natural/even ([] : Optional Natural) diff --git a/Prelude/Optional/null b/Prelude/Optional/null --- a/Prelude/Optional/null +++ b/Prelude/Optional/null @@ -4,9 +4,9 @@ Examples: ``` -./null Integer ([ 2 ] : Optional Integer) = False +./null Natural ([ 2 ] : Optional Natural) = False -./null Integer ([] : Optional Integer) = True +./null Natural ([] : Optional Natural) = True ``` -} let null diff --git a/Prelude/Optional/toList b/Prelude/Optional/toList --- a/Prelude/Optional/toList +++ b/Prelude/Optional/toList @@ -4,9 +4,9 @@ Examples: ``` -./toList Integer ([ 1 ] : Optional Integer) = [ 1 ] +./toList Natural ([ 1 ] : Optional Natural) = [ 1 ] -./toList Integer ([] : Optional Integer) = [] : List Integer +./toList Natural ([] : Optional Natural) = [] : List Natural ``` -} let toList diff --git a/Prelude/Text/concatMap b/Prelude/Text/concatMap --- a/Prelude/Text/concatMap +++ b/Prelude/Text/concatMap @@ -4,10 +4,10 @@ Examples: ``` -./concatMap Integer (λ(n : Integer) → "${Integer/show n} ") [ 0, 1, 2 ] +./concatMap Natural (λ(n : Natural) → "${Natural/show n} ") [ 0, 1, 2 ] = "0 1 2 " -./concatMap Integer (λ(n : Integer) → "${Integer/show n} ") ([] : List Integer) +./concatMap Natural (λ(n : Natural) → "${Natural/show n} ") ([] : List Natural) = "" ``` -} diff --git a/Prelude/Text/concatMapSep b/Prelude/Text/concatMapSep --- a/Prelude/Text/concatMapSep +++ b/Prelude/Text/concatMapSep @@ -5,9 +5,9 @@ Examples: ``` -./concatMapSep ", " Integer Integer/show [ 0, 1, 2 ] = "0, 1, 2" +./concatMapSep ", " Natural Natural/show [ 0, 1, 2 ] = "0, 1, 2" -./concatMapSep ", " Integer Integer/show ([] : List Integer) = "" +./concatMapSep ", " Natural Natural/show ([] : List Natural) = "" ``` -} let concatMapSep diff --git a/dhall.cabal b/dhall.cabal --- a/dhall.cabal +++ b/dhall.cabal @@ -1,5 +1,5 @@ Name: dhall -Version: 1.13.1 +Version: 1.14.0 Cabal-Version: >=1.8.0.2 Build-Type: Simple Tested-With: GHC == 8.0.1 @@ -168,7 +168,7 @@ formatting >= 6.3 && < 6.4 , http-client >= 0.4.30 && < 0.6 , http-client-tls >= 0.2.0 && < 0.4 , - insert-ordered-containers >= 0.1.0.1 && < 0.3 , + insert-ordered-containers >= 0.2.1.0 && < 0.3 , lens-family-core >= 1.0.0 && < 1.3 , megaparsec >= 6.1.1 && < 6.6 , memory >= 0.14 && < 0.15, @@ -258,7 +258,7 @@ Other-Modules: Paths_dhall -Test-Suite test +Test-Suite tasty Type: exitcode-stdio-1.0 Hs-Source-Dirs: tests Main-Is: Tests.hs @@ -277,7 +277,16 @@ dhall , insert-ordered-containers , prettyprinter , - tasty >= 0.11.2 && < 1.1 , + tasty >= 0.11.2 && < 1.2 , tasty-hunit >= 0.9.2 && < 0.11, text >= 0.11.1.0 && < 1.3 , vector >= 0.11.0.0 && < 0.13 + +Test-Suite doctest + Type: exitcode-stdio-1.0 + Hs-Source-Dirs: doctest + Main-Is: Main.hs + GHC-Options: -Wall + Build-Depends: + base , + doctest >= 0.7.0 && < 0.16 diff --git a/dhall/Main.hs b/dhall/Main.hs --- a/dhall/Main.hs +++ b/dhall/Main.hs @@ -11,7 +11,7 @@ import Data.Text.Prettyprint.Doc (Pretty) import Data.Typeable (Typeable) import Data.Version (showVersion) -import Dhall.Core (Expr, Path) +import Dhall.Core (Expr, Import) import Dhall.Import (Imported(..), load) import Dhall.Parser (Src) import Dhall.Pretty (annToAnsiStyle, prettyExpr) @@ -94,13 +94,13 @@ throws (Left e) = Control.Exception.throwIO e throws (Right a) = return a -getExpression :: IO (Expr Src Path) +getExpression :: IO (Expr Src Import) getExpression = do inText <- Data.Text.Lazy.IO.getContents throws (Dhall.Parser.exprFromText "(stdin)" inText) -assertNoImports :: Expr Src Path -> IO (Expr Src X) +assertNoImports :: Expr Src Import -> IO (Expr Src X) assertNoImports expression = throws (traverse (\_ -> Left ImportResolutionDisabled) expression) diff --git a/doctest/Main.hs b/doctest/Main.hs new file mode 100644 --- /dev/null +++ b/doctest/Main.hs @@ -0,0 +1,6 @@ +module Main where + +import qualified Test.DocTest + +main :: IO () +main = Test.DocTest.doctest [ "-isrc", "src/Dhall.hs" ] diff --git a/src/Dhall.hs b/src/Dhall.hs --- a/src/Dhall.hs +++ b/src/Dhall.hs @@ -104,6 +104,9 @@ import qualified Dhall.Parser import qualified Dhall.TypeCheck +-- $setup +-- >>> :set -XOverloadedStrings + throws :: Exception e => Either e a -> IO a throws (Left e) = Control.Exception.throwIO e throws (Right r) = return r @@ -133,7 +136,7 @@ The first argument determines the type of value that you decode: ->>> input integer "2" +>>> input integer "+2" 2 >>> input (vector double) "[1.0, 2.0]" [1.0,2.0] @@ -169,7 +172,7 @@ -- ^ The decoded value in Haskell inputWith (Type {..}) ctx n txt = do expr <- throws (Dhall.Parser.exprFromText "(input)" txt) - expr' <- Dhall.Import.loadWithContext ctx expr + expr' <- Dhall.Import.loadWithContext ctx n expr let suffix = ( Data.Text.Lazy.Builder.toLazyText . build @@ -235,13 +238,13 @@ > > > ┌─────────────┐ -> │ 1 : Integer │ ❰1❱ is an expression that has type ❰Integer❱, so the type +> │ 1 : Natural │ ❰1❱ is an expression that has type ❰Natural❱, so the type > └─────────────┘ checker accepts the annotation > > -> ┌────────────────────────┐ -> │ Natural/even +2 : Bool │ ❰Natural/even +2❱ has type ❰Bool❱, so the type -> └────────────────────────┘ checker accepts the annotation +> ┌───────────────────────┐ +> │ Natural/even 2 : Bool │ ❰Natural/even 2❱ has type ❰Bool❱, so the type +> └───────────────────────┘ checker accepts the annotation > > > ┌────────────────────┐ @@ -362,7 +365,7 @@ {-| Decode a `Natural` ->>> input natural "+42" +>>> input natural "42" 42 -} natural :: Type Natural @@ -375,7 +378,7 @@ {-| Decode an `Integer` ->>> input integer "42" +>>> input integer "+42" 42 -} integer :: Type Integer @@ -430,7 +433,7 @@ {-| Decode a `Maybe` ->>> input (maybe integer) "[1] : Optional Integer" +>>> input (maybe natural) "[1] : Optional Natural" Just 1 -} maybe :: Type a -> Type (Maybe a) @@ -443,8 +446,8 @@ {-| Decode a `Seq` - ->>> input (sequence integer) "[1, 2, 3]" -[1,2,3] +>>> input (sequence natural) "[1, 2, 3]" +fromList [1,2,3] -} sequence :: Type a -> Type (Seq a) sequence (Type extractIn expectedIn) = Type extractOut expectedOut @@ -456,7 +459,7 @@ {-| Decode a list ->>> input (list integer) "[1, 2, 3]" +>>> input (list natural) "[1, 2, 3]" [1,2,3] -} list :: Type a -> Type [a] @@ -464,7 +467,7 @@ {-| Decode a `Vector` ->>> input (vector integer) "[1, 2, 3]" +>>> input (vector natural) "[1, 2, 3]" [1,2,3] -} vector :: Type a -> Type (Vector a) @@ -472,8 +475,8 @@ {-| Decode `()` from an empty record. ->>> input unit "{=}" -() +>>> input unit "{=}" -- GHC doesn't print the result if it is @()@ + -} unit :: Type () unit = Type extractOut expectedOut @@ -495,8 +498,8 @@ {-| Given a pair of `Type`s, decode a tuple-record into their pairing. ->>> input (pair natural bool) "{ _1 = +42, _2 = False }" -(42, False) +>>> input (pair natural bool) "{ _1 = 42, _2 = False }" +(42,False) -} pair :: Type a -> Type b -> Type (a, b) pair l r = Type extractOut expectedOut @@ -517,7 +520,7 @@ {-| Any value that implements `Interpret` can be automatically decoded based on the inferred return type of `input` ->>> input auto "[1, 2, 3]" :: IO (Vector Integer) +>>> input auto "[1, 2, 3]" :: IO (Vector Natural) [1,2,3] This class auto-generates a default implementation for records that @@ -1077,7 +1080,7 @@ > , description = > "A configuration language guaranteed to terminate" > , stars = -> +289 +> 289 > } Our parser has type 'Type' @Project@, but we can't build that out of any diff --git a/src/Dhall/Core.hs b/src/Dhall/Core.hs --- a/src/Dhall/Core.hs +++ b/src/Dhall/Core.hs @@ -18,11 +18,14 @@ module Dhall.Core ( -- * Syntax Const(..) - , HasHome(..) - , PathType(..) - , PathHashed(..) - , PathMode(..) - , Path(..) + , Directory(..) + , File(..) + , FilePrefix(..) + , Import(..) + , ImportHashed(..) + , ImportMode(..) + , ImportType(..) + , Path , Var(..) , Chunks(..) , Expr(..) @@ -79,9 +82,8 @@ import qualified Data.Sequence import qualified Data.Set import qualified Data.Text -import qualified Data.Text.Lazy as Text -import qualified Data.Text.Lazy.Builder as Builder -import qualified Data.Text.Prettyprint.Doc as Pretty +import qualified Data.Text.Lazy.Builder as Builder +import qualified Data.Text.Prettyprint.Doc as Pretty {-| Constants for a pure type system @@ -105,64 +107,145 @@ instance Buildable Const where build = buildConst --- | Whether or not a path is relative to the user's home directory -data HasHome = Home | Homeless deriving (Eq, Ord, Show) +{-| Internal representation of a directory that stores the path components in + reverse order --- | The type of path to import (i.e. local vs. remote vs. environment) -data PathType - = File HasHome FilePath + In other words, the directory @/foo/bar/baz@ is encoded as + @Directory { components = [ "baz", "bar", "foo" ] }@ +-} +newtype Directory = Directory { components :: [Text] } + deriving (Eq, Ord, Show) + +instance Semigroup Directory where + Directory components₀ <> Directory components₁ = + Directory (components₁ <> components₀) + +instance Buildable Directory where + build (Directory {..}) = + foldMap buildComponent (reverse components) + where + buildComponent text = "/" <> build text + +{-| A `File` is a `directory` followed by one additional path component + representing the `file` name +-} +data File = File + { directory :: Directory + , file :: Text + } deriving (Eq, Ord, Show) + +instance Buildable File where + build (File {..}) = build directory <> "/" <> build file + +instance Semigroup File where + File directory₀ _ <> File directory₁ file = + File (directory₀ <> directory₁) file + +data FilePrefix + = Absolute + -- ^ Absolute path + | Here + -- ^ Path relative to @.@ + | Parent + -- ^ Path relative to @..@ + | Home + -- ^ Path relative to @~@ + deriving (Eq, Ord, Show) + +instance Buildable FilePrefix where + build Absolute = "" + build Here = "." + build Parent = ".." + build Home = "~" + +-- | The type of import (i.e. local vs. remote vs. environment) +data ImportType + = Local FilePrefix File -- ^ Local path - | URL Text (Maybe PathHashed) - -- ^ URL of remote resource and optional headers stored in a path + | URL Text File Text (Maybe ImportHashed) + -- ^ URL of remote resource and optional headers stored in an import | Env Text -- ^ Environment variable deriving (Eq, Ord, Show) -instance Buildable PathType where - build (File Home file) - = "~/" <> build (Text.pack file) - build (File Homeless file) - | Text.isPrefixOf "./" txt - || Text.isPrefixOf "/" txt - || Text.isPrefixOf "../" txt - = build txt <> " " - | otherwise - = "./" <> build txt <> " " +parent :: File +parent = File { directory = Directory { components = [ ".." ] }, file = "" } + +instance Semigroup ImportType where + Local prefix file₀ <> Local Here file₁ = Local prefix (file₀ <> file₁) + + URL prefix file₀ suffix headers <> Local Here file₁ = + URL prefix (file₀ <> file₁) suffix headers + + Local prefix file₀ <> Local Parent file₁ = + Local prefix (file₀ <> parent <> file₁) + + URL prefix file₀ suffix headers <> Local Parent file₁ = + URL prefix (file₀ <> parent <> file₁) suffix headers + + _ <> import₁ = + import₁ + +instance Buildable ImportType where + build (Local prefix file) = + build prefix <> build file <> " " + + build (URL prefix file suffix headers) = + build prefix + <> build file + <> build suffix + <> foldMap buildHeaders headers + <> " " where - txt = Text.pack file - build (URL str Nothing ) = build str <> " " - build (URL str (Just headers)) = build str <> " using " <> build headers <> " " - build (Env env) = "env:" <> build env + buildHeaders h = " using " <> build h --- | How to interpret the path's contents (i.e. as Dhall code or raw text) -data PathMode = Code | RawText deriving (Eq, Ord, Show) + build (Env env) = + "env:" <> build env <> " " --- | A `PathType` extended with an optional hash for semantic integrity checks -data PathHashed = PathHashed - { hash :: Maybe (Crypto.Hash.Digest SHA256) - , pathType :: PathType +-- | How to interpret the import's contents (i.e. as Dhall code or raw text) +data ImportMode = Code | RawText deriving (Eq, Ord, Show) + +-- | A `ImportType` extended with an optional hash for semantic integrity checks +data ImportHashed = ImportHashed + { hash :: Maybe (Crypto.Hash.Digest SHA256) + , importType :: ImportType } deriving (Eq, Ord, Show) -instance Buildable PathHashed where - build (PathHashed Nothing p) = build p - build (PathHashed (Just h) p) = build p <> "sha256:" <> build (show h) <> " " +instance Semigroup ImportHashed where + ImportHashed _ importType₀ <> ImportHashed hash importType₁ = + ImportHashed hash (importType₀ <> importType₁) --- | Path to an external resource -data Path = Path - { pathHashed :: PathHashed - , pathMode :: PathMode +instance Buildable ImportHashed where + build (ImportHashed Nothing p) = + build p + build (ImportHashed (Just h) p) = + build p <> "sha256:" <> build (show h) <> " " + +-- | Reference to an external resource +data Import = Import + { importHashed :: ImportHashed + , importMode :: ImportMode } deriving (Eq, Ord, Show) -instance Buildable Path where - build (Path {..}) = build pathHashed <> suffix +instance Semigroup Import where + Import importHashed₀ _ <> Import importHashed₁ code = + Import (importHashed₀ <> importHashed₁) code + +instance Buildable Import where + build (Import {..}) = build importHashed <> suffix where - suffix = case pathMode of + suffix = case importMode of RawText -> "as Text" Code -> "" -instance Pretty Path where - pretty path = Pretty.pretty (Builder.toLazyText (build path)) +instance Pretty Import where + pretty import_ = Pretty.pretty (Builder.toLazyText (build import_)) +-- | Type synonym for `Import`, provided for backwards compatibility +type Path = Import + +{-# DEPRECATED Path "Use Dhall.Core.Import instead" #-} + {-| Label for a bound variable The `Text` field is the variable's name (i.e. \"@x@\"). @@ -239,7 +322,7 @@ | BoolIf (Expr s a) (Expr s a) (Expr s a) -- | > Natural ~ Natural | Natural - -- | > NaturalLit n ~ +n + -- | > NaturalLit n ~ n | NaturalLit Natural -- | > NaturalFold ~ Natural/fold | NaturalFold @@ -261,7 +344,7 @@ | NaturalTimes (Expr s a) (Expr s a) -- | > Integer ~ Integer | Integer - -- | > IntegerLit n ~ n + -- | > IntegerLit n ~ ±n | IntegerLit Integer -- | > IntegerShow ~ Integer/show | IntegerShow @@ -332,7 +415,7 @@ | Project (Expr s a) (Set Text) -- | > Note s x ~ e | Note s (Expr s a) - -- | > Embed path ~ path + -- | > Embed import ~ import | Embed a deriving (Functor, Foldable, Traversable, Show, Eq) @@ -1302,9 +1385,10 @@ App NaturalOdd (NaturalLit n) -> BoolLit (odd n) App NaturalToInteger (NaturalLit n) -> IntegerLit (toInteger n) App NaturalShow (NaturalLit n) -> - TextLit (Chunks [] ("+" <> buildNatural n)) - App IntegerShow (IntegerLit n) -> - TextLit (Chunks [] (buildNumber n)) + TextLit (Chunks [] (buildNatural n)) + App IntegerShow (IntegerLit n) + | 0 <= n -> TextLit (Chunks [] ("+" <> buildNumber n)) + | otherwise -> TextLit (Chunks [] (buildNumber n)) App DoubleShow (DoubleLit n) -> TextLit (Chunks [] (buildScientific n)) App (App OptionalBuild _A₀) g -> diff --git a/src/Dhall/Import.hs b/src/Dhall/Import.hs --- a/src/Dhall/Import.hs +++ b/src/Dhall/Import.hs @@ -1,7 +1,9 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -Wall #-} @@ -58,10 +60,6 @@ > http://example.com/id - You can also reuse directory names as expressions. If you provide a path - to a local or remote directory then the compiler will look for a file named - @\@@ within that directory and use that file to represent the directory. - You can also import expressions stored within environment variables using @env:NAME@, where @NAME@ is the name of the environment variable. For example: @@ -74,7 +72,7 @@ > > { bar = "Hi", baz = λ(x : Bool) → x == False, foo = 1 } - If you wish to import the raw contents of a path as @Text@ then add + If you wish to import the raw contents of an impoert as @Text@ then add @as Text@ to the end of the import: > $ dhall <<< "http://example.com as Text" @@ -101,7 +99,7 @@ module Dhall.Import ( -- * Import - exprFromPath + exprFromImport , load , loadWith , loadWithContext @@ -118,17 +116,16 @@ ) where import Control.Applicative (empty) -import Control.Exception - (Exception, IOException, SomeException, onException, throwIO) +import Control.Exception (Exception, SomeException, throwIO) import Control.Monad (join) import Control.Monad.Catch (throwM, MonadCatch(catch)) import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.Trans.State.Strict (StateT) import Crypto.Hash (SHA256) -import Data.ByteString.Lazy (ByteString) import Data.CaseInsensitive (CI) +import Data.List.NonEmpty (NonEmpty(..)) import Data.Map (Map) -import Data.Monoid ((<>)) +import Data.Semigroup (sconcat, (<>)) import Data.Text.Lazy (Text) import Data.Text.Lazy.Builder (Builder) #if MIN_VERSION_base(4,8,0) @@ -141,11 +138,13 @@ import Dhall.Core ( Expr(..) , Chunks(..) - , HasHome(..) - , PathHashed(..) - , PathMode(..) - , PathType(..) - , Path(..) + , Directory(..) + , File(..) + , FilePrefix(..) + , ImportHashed(..) + , ImportType(..) + , ImportMode(..) + , Import(..) ) import Dhall.Parser (Parser(..), ParseError(..), Src(..)) import Dhall.TypeCheck (X(..)) @@ -167,7 +166,6 @@ import qualified Data.HashMap.Strict.InsOrd import qualified Data.Map.Strict as Map import qualified Data.Text.Encoding -import qualified Data.Text.IO import qualified Data.Text.Lazy as Text import qualified Data.Text.Lazy.Builder as Builder import qualified Data.Text.Lazy.Encoding @@ -190,14 +188,15 @@ -- | An import failed because of a cycle in the import graph newtype Cycle = Cycle - { cyclicImport :: Path -- ^ The offending cyclic import + { cyclicImport :: Import -- ^ The offending cyclic import } deriving (Typeable) instance Exception Cycle instance Show Cycle where - show (Cycle path) = "\nCyclic import: " ++ builderToString (build path) + show (Cycle import_) = + "\nCyclic import: " ++ builderToString (build import_) {-| Dhall tries to ensure that all expressions hosted on network endpoints are weakly referentially transparent, meaning roughly that any two clients will @@ -226,33 +225,33 @@ All other imports are defined to be non-local -} newtype ReferentiallyOpaque = ReferentiallyOpaque - { opaqueImport :: Path -- ^ The offending opaque import + { opaqueImport :: Import -- ^ The offending opaque import } deriving (Typeable) instance Exception ReferentiallyOpaque instance Show ReferentiallyOpaque where - show (ReferentiallyOpaque path) = - "\nReferentially opaque import: " ++ builderToString (build path) + show (ReferentiallyOpaque import_) = + "\nReferentially opaque import: " ++ builderToString (build import_) -- | Extend another exception with the current import stack data Imported e = Imported - { importStack :: [Path] -- ^ Imports resolved so far, in reverse order - , nested :: e -- ^ The nested exception + { importStack :: [Import] -- ^ Imports resolved so far, in reverse order + , nested :: e -- ^ The nested exception } deriving (Typeable) instance Exception e => Exception (Imported e) instance Show e => Show (Imported e) where - show (Imported paths e) = - (case paths of [] -> ""; _ -> "\n") - ++ unlines (map indent paths') + show (Imported imports e) = + (case imports of [] -> ""; _ -> "\n") + ++ unlines (map indent imports') ++ show e where - indent (n, path) = - take (2 * n) (repeat ' ') ++ "↳ " ++ builderToString (build path) - -- Canonicalize all paths - paths' = zip [0..] (drop 1 (reverse (canonicalizeAll paths))) + indent (n, import_) = + take (2 * n) (repeat ' ') ++ "↳ " ++ builderToString (build import_) + -- Canonicalize all imports + imports' = zip [0..] (drop 1 (reverse (canonicalizeAll imports))) -- | Newtype used to wrap `HttpException`s with a prettier `Show` instance newtype PrettyHttpException = PrettyHttpException HttpException @@ -328,10 +327,10 @@ -- | State threaded throughout the import process data Status = Status - { _stack :: [Path] - -- ^ Stack of `Path`s that we've imported along the way to get to the + { _stack :: [Import] + -- ^ Stack of `Import`s that we've imported along the way to get to the -- current point - , _cache :: Map Path (Expr Src X) + , _cache :: Map Import (Expr Src X) -- ^ Cache of imported expressions in order to avoid importing the same -- expression twice with different values , _manager :: Maybe Manager @@ -342,13 +341,13 @@ emptyStatus :: Status emptyStatus = Status [] Map.empty Nothing -canonicalizeAll :: [Path] -> [Path] -canonicalizeAll = map canonicalizePath . List.tails +canonicalizeAll :: [Import] -> [Import] +canonicalizeAll = map canonicalizeImport . List.tails -stack :: Functor f => LensLike' f Status [Path] +stack :: Functor f => LensLike' f Status [Import] stack k s = fmap (\x -> s { _stack = x }) (k (_stack s)) -cache :: Functor f => LensLike' f Status (Map Path (Expr Src X)) +cache :: Functor f => LensLike' f Status (Map Import (Expr Src X)) cache k s = fmap (\x -> s { _cache = x }) (k (_cache s)) manager :: Functor f => LensLike' f Status (Maybe Manager) @@ -370,107 +369,62 @@ zoom manager (State.put (Just m)) return m -{-| This function computes the current path by taking the last absolute path - (either an absolute `FilePath` or `URL`) and combining it with all following - relative paths +{-| +> canonicalize (canonicalize x) = canonicalize x +-} +class Canonicalize path where + canonicalize :: path -> path - For example, if the file `./foo/bar` imports `./baz`, that will resolve to - `./foo/baz`. Relative imports are relative to a file's parent directory. - This also works for URLs, too. +instance Canonicalize Directory where + canonicalize (Directory []) = Directory [] - This code is full of all sorts of edge cases so it wouldn't surprise me at - all if you find something broken in here. Most of the ugliness is due to: + canonicalize (Directory ("." : components₀)) = + canonicalize (Directory components₀) - * Handling paths ending with @/\@@ by stripping the @/\@@ suffix if and only - if you navigate to any downstream relative paths - * Removing spurious @.@s and @..@s from the path + canonicalize (Directory (".." : components₀)) = + case canonicalize (Directory components₀) of + Directory [] -> Directory [ ".." ] + Directory (_ : components₁) -> Directory components₁ - Also, there are way too many `reverse`s in the URL-handling code For now I - don't mind, but if were to really do this correctly we'd store the URLs as - `Text` for O(1) access to the end of the string. The only reason we use - `String` at all is for consistency with the @http-client@ library. --} -canonicalize :: [PathType] -> PathType -canonicalize [] = File Homeless "." -canonicalize (File hasHome0 file0:paths0) = - if FilePath.isRelative file0 && hasHome0 == Homeless - then go file0 paths0 - else File hasHome0 (FilePath.normalise file0) - where - go currPath [] = File Homeless (FilePath.normalise currPath) - go currPath (Env _ :_ ) = File Homeless (FilePath.normalise currPath) - go currPath (URL url0 headers:rest ) = combine prefix suffix + canonicalize (Directory (component : components₀)) = + Directory (component : components₁) where - headers' = fmap (onPathType (\h -> canonicalize (h:rest))) headers - - prefix = parentURL (removeAtFromURL url0) + Directory components₁ = canonicalize (Directory components₀) - suffix = FilePath.normalise currPath +instance Canonicalize File where + canonicalize (File { directory, .. }) = + File { directory = canonicalize directory, .. } - -- `clean` will resolve internal @.@/@..@'s in @currPath@, but we still - -- need to manually handle @.@/@..@'s at the beginning of the path - combine url path = case List.stripPrefix "../" path of - Just path' -> combine url' path' - where - url' = parentURL (removeAtFromURL url) - Nothing -> case List.stripPrefix "./" path of - Just path' -> combine url path' - Nothing -> - -- This `last` is safe because the lexer constrains all - -- URLs to be non-empty. I couldn't find a simple and safe - -- equivalent in the `text` API - case Text.last url of - '/' -> URL (url <> path') headers' - _ -> URL (url <> "/" <> path') headers' - where - path' = Text.pack path - go currPath (File hasHome file:paths) = - if FilePath.isRelative file && hasHome == Homeless - then go file' paths - else File hasHome (FilePath.normalise file') - where - file' = FilePath.takeDirectory (removeAtFromFilename file) currPath -canonicalize (URL path headers:rest) = URL path headers' - where - headers' = fmap (onPathType (\h -> canonicalize (h:rest))) headers -canonicalize (Env env :_ ) = Env env +instance Canonicalize ImportType where + canonicalize (Local prefix file) = + Local prefix (canonicalize file) -onPathType :: (PathType -> PathType) -> PathHashed -> PathHashed -onPathType f (PathHashed a b) = PathHashed a (f b) + canonicalize (URL prefix file suffix header) = + URL prefix (canonicalize file) suffix header -canonicalizePath :: [Path] -> Path -canonicalizePath [] = - Path - { pathMode = Code - , pathHashed = PathHashed - { hash = Nothing - , pathType = canonicalize [] - } - } -canonicalizePath (path:paths) = - Path - { pathMode = pathMode path - , pathHashed = (pathHashed path) - { hash = hash (pathHashed path) - , pathType = - canonicalize (map (pathType . pathHashed) (path:paths)) - } - } + canonicalize (Env name) = + Env name -parentURL :: Text -> Text -parentURL = Text.dropWhileEnd (/= '/') +instance Canonicalize ImportHashed where + canonicalize (ImportHashed hash importType) = + ImportHashed hash (canonicalize importType) -removeAtFromURL:: Text -> Text -removeAtFromURL url - | Text.isSuffixOf "/@" url = Text.dropEnd 2 url - | Text.isSuffixOf "/" url = Text.dropEnd 1 url - | otherwise = url +instance Canonicalize Import where + canonicalize (Import importHashed importMode) = + Import (canonicalize importHashed) importMode -removeAtFromFilename :: FilePath -> FilePath -removeAtFromFilename fp = - if FilePath.takeFileName fp == "@" - then FilePath.takeDirectory fp - else fp +canonicalizeImport :: [Import] -> Import +canonicalizeImport imports = + canonicalize (sconcat (defaultImport :| reverse imports)) + where + defaultImport = + Import + { importMode = Code + , importHashed = ImportHashed + { hash = Nothing + , importType = Local Here (File (Directory []) ".") + } + } toHeaders :: Expr s a @@ -549,262 +503,235 @@ <> "\n" <> "↳ " <> show actualHash <> "\n" --- | Parse an expression from a `Path` containing a Dhall program -exprFromPath :: Path -> StateT Status IO (Expr Src Path) -exprFromPath (Path {..}) = case pathType of - File hasHome file -> liftIO (do - path <- case hasHome of - Home -> do - home <- System.Directory.getHomeDirectory - return (home file) - Homeless -> do - return file +-- | Parse an expression from a `Import` containing a Dhall program +exprFromImport :: Import -> StateT Status IO (Expr Src Import) +exprFromImport (Import {..}) = do + let ImportHashed {..} = importHashed - case pathMode of - Code -> do - exists <- System.Directory.doesFileExist path - if exists - then return () - else throwIO (MissingFile path) + (path, text) <- case importType of + Local prefix (File {..}) -> liftIO $ do + let Directory {..} = directory - -- Unfortunately, GHC throws an `InappropriateType` exception - -- when trying to read a directory, but does not export the - -- exception, so I must resort to a more heavy-handed `catch` - let handler :: IOException -> IO Text - handler e = do - -- If the fallback fails, reuse the original exception - -- to avoid user confusion - Data.Text.Lazy.IO.readFile (path "@") - `onException` throwIO e + prefixPath <- case prefix of + Home -> do + System.Directory.getHomeDirectory - text <- Data.Text.Lazy.IO.readFile path `catch` handler - case Text.Megaparsec.parse parser path text of - Left errInfo -> do - throwIO (ParseError errInfo text) - Right expr -> do - return expr - RawText -> do - text <- Data.Text.IO.readFile path - return (TextLit (Chunks [] (build text))) ) - URL url headerPath -> do - m <- needManager - request <- liftIO (HTTP.parseUrlThrow (Text.unpack url)) + Absolute -> do + return "/" - let handler :: HTTP.HttpException -> IO (HTTP.Response ByteString) -#if MIN_VERSION_http_client(0,5,0) - handler err@(HttpExceptionRequest _ (StatusCodeException _ _)) = do -#else - handler err@(StatusCodeException _ _ _) = do -#endif - let request' = request { HTTP.path = HTTP.path request <> "/@" } - -- If the fallback fails, reuse the original exception to avoid - -- user confusion - HTTP.httpLbs request' m `onException` throwIO (PrettyHttpException err) - handler err = throwIO (PrettyHttpException err) + Parent -> do + pwd <- System.Directory.getCurrentDirectory + return (FilePath.takeDirectory pwd) - requestWithHeaders <- case headerPath of - Nothing -> return request - Just path -> do - expr <- loadStaticIO Dhall.Context.empty (Path path Code) - let expected :: Expr Src X - expected = - App List - ( Record - ( Data.HashMap.Strict.InsOrd.fromList - [("header", Text), ("value", Text)] + Here -> do + System.Directory.getCurrentDirectory + + let cs = map Text.unpack (file : components) + + let cons component dir = dir component + + let path = foldr cons prefixPath cs + + exists <- System.Directory.doesFileExist path + + if exists + then return () + else throwIO (MissingFile path) + + text <- Data.Text.Lazy.IO.readFile path + + return (path, text) + + URL prefix file suffix maybeHeaders -> do + m <- needManager + + let fileText = Builder.toLazyText (build file) + let url = Text.unpack (prefix <> fileText <> suffix) + + request <- liftIO (HTTP.parseUrlThrow url) + + requestWithHeaders <- case maybeHeaders of + Nothing -> return request + Just importHashed_ -> do + expr <- loadStaticIO Dhall.Context.empty + (const Nothing) + (Import importHashed_ Code) + let expected :: Expr Src X + expected = + App List + ( Record + ( Data.HashMap.Strict.InsOrd.fromList + [("header", Text), ("value", Text)] + ) ) - ) - let suffix = - ( Builder.toLazyText - . build - ) expected - let annot = case expr of - Note (Src begin end bytes) _ -> - Note (Src begin end bytes') (Annot expr expected) - where - bytes' = bytes <> " : " <> suffix - _ -> - Annot expr expected - case Dhall.TypeCheck.typeOf annot of - Left err -> liftIO (throwIO err) - Right _ -> return () - let expr' = Dhall.Core.normalize expr - headers <- case toHeaders expr' of - Just headers -> do - return headers - Nothing -> do - liftIO (throwIO InternalError) - let requestWithHeaders = request - { HTTP.requestHeaders = headers - } - return requestWithHeaders - response <- liftIO (HTTP.httpLbs requestWithHeaders m `catch` handler) + let suffix_ = + ( Builder.toLazyText + . build + ) expected + let annot = case expr of + Note (Src begin end bytes) _ -> + Note (Src begin end bytes') (Annot expr expected) + where + bytes' = bytes <> " : " <> suffix_ + _ -> + Annot expr expected - let bytes = HTTP.responseBody response + case Dhall.TypeCheck.typeOf annot of + Left err -> liftIO (throwIO err) + Right _ -> return () - text <- case Data.Text.Lazy.Encoding.decodeUtf8' bytes of - Left err -> liftIO (throwIO err) - Right text -> return text + let expr' = Dhall.Core.normalize expr - case pathMode of - Code -> - case Text.Megaparsec.parse parser (Text.unpack url) text of - Left err -> do - -- Also try the fallback in case of a parse error, since - -- the parse error might signify that this URL points to - -- a directory list - let err' = ParseError err text + headers <- case toHeaders expr' of + Just headers -> do + return headers + Nothing -> do + liftIO (throwIO InternalError) - request' <- liftIO (HTTP.parseUrlThrow (Text.unpack url)) + let requestWithHeaders = request + { HTTP.requestHeaders = headers + } - let request'' = - request' - { HTTP.path = HTTP.path request' <> "/@" } - response' <- liftIO (HTTP.httpLbs request'' m `onException` throwIO err' ) + return requestWithHeaders - let bytes' = HTTP.responseBody response' + response <- liftIO (HTTP.httpLbs requestWithHeaders m) - text' <- case Data.Text.Lazy.Encoding.decodeUtf8' bytes' of - Left _ -> liftIO (throwIO err') - Right text' -> return text' + let bytes = HTTP.responseBody response - case Text.Megaparsec.parse parser (Text.unpack url) text' of - Left _ -> liftIO (throwIO err') - Right expr -> return expr - Right expr -> return expr - RawText -> do - return (TextLit (Chunks [] (build text))) - Env env -> liftIO (do - x <- System.Environment.lookupEnv (Text.unpack env) - case x of - Just str -> do - let text = Text.pack str - case pathMode of - Code -> - case Text.Megaparsec.parse parser (Text.unpack env) text of - Left errInfo -> do - throwIO (ParseError errInfo text) - Right expr -> do - return expr - RawText -> return (TextLit (Chunks [] (build str))) - Nothing -> throwIO (MissingEnvironmentVariable env) ) - where - PathHashed {..} = pathHashed + case Data.Text.Lazy.Encoding.decodeUtf8' bytes of + Left err -> liftIO (throwIO err) + Right text -> return (url, text) - parser = unParser (do - Text.Parser.Token.whiteSpace - r <- Dhall.Parser.expr - Text.Parser.Combinators.eof - return r ) + Env env -> liftIO $ do + x <- System.Environment.lookupEnv (Text.unpack env) + case x of + Just string -> return (Text.unpack env, Text.pack string) + Nothing -> throwIO (MissingEnvironmentVariable env) -{-| Load a `Path` as a \"dynamic\" expression (without resolving any imports) + case importMode of + Code -> do + let parser = unParser $ do + Text.Parser.Token.whiteSpace + r <- Dhall.Parser.expr + Text.Parser.Combinators.eof + return r - This also returns the true final path (i.e. explicit "/@" at the end for - directories) + case Text.Megaparsec.parse parser path text of + Left errInfo -> do + liftIO (throwIO (ParseError errInfo text)) + Right expr -> do + return expr + + RawText -> do + return (TextLit (Chunks [] (build text))) + +{-| Load an `Import` as a \"dynamic\" expression (without resolving any imports) -} loadDynamic :: forall m . MonadCatch m - => (Path -> StateT Status m (Expr Src Path)) - -> Path - -> StateT Status m (Expr Src Path) -loadDynamic from_path p = do - paths <- zoom stack State.get + => (Import -> StateT Status m (Expr Src Import)) + -> Import + -> StateT Status m (Expr Src Import) +loadDynamic from_import import_ = do + imports <- zoom stack State.get - let handler :: SomeException -> StateT Status m (Expr Src Path) - handler e = throwM (Imported (p:paths) e) + let handler :: SomeException -> StateT Status m (Expr Src Import) + handler e = throwM (Imported (import_:imports) e) - from_path (canonicalizePath (p:paths)) `catch` handler + from_import (canonicalizeImport (import_:imports)) `catch` handler loadStaticIO :: Dhall.Context.Context (Expr Src X) - -> Path + -> Dhall.Core.Normalizer X + -> Import -> StateT Status IO (Expr Src X) -loadStaticIO = loadStaticWith exprFromPath +loadStaticIO = loadStaticWith exprFromImport --- | Resolve all imports within an expression using a custom typing context and Path --- resolving callback in arbitrary `MonadCatch` monad. +-- | Resolve all imports within an expression using a custom typing context and +-- `Import`-resolving callback in arbitrary `MonadCatch` monad. loadWith :: MonadCatch m - => (Path -> StateT Status m (Expr Src Path)) + => (Import -> StateT Status m (Expr Src Import)) -> Dhall.Context.Context (Expr Src X) - -> Expr Src Path + -> Dhall.Core.Normalizer X + -> Expr Src Import -> m (Expr Src X) -loadWith from_path ctx = evalStatus (loadStaticWith from_path ctx) +loadWith from_import ctx n = evalStatus (loadStaticWith from_import ctx n) -- | Resolve all imports within an expression using a custom typing context. -- -- @load = loadWithContext Dhall.Context.empty@ loadWithContext :: Dhall.Context.Context (Expr Src X) - -> Expr Src Path + -> Dhall.Core.Normalizer X + -> Expr Src Import -> IO (Expr Src X) -loadWithContext ctx = evalStatus (loadStaticIO ctx) +loadWithContext ctx n = evalStatus (loadStaticIO ctx n) loadStaticWith :: MonadCatch m - => (Path -> StateT Status m (Expr Src Path)) + => (Import -> StateT Status m (Expr Src Import)) -> Dhall.Context.Context (Expr Src X) - -> Path + -> Dhall.Core.Normalizer X + -> Import -> StateT Status m (Expr Src X) -loadStaticWith from_path ctx path = do - paths <- zoom stack State.get +loadStaticWith from_import ctx n import_ = do + imports <- zoom stack State.get - let local (Path (PathHashed _ (URL _ _ )) _) = False - local (Path (PathHashed _ (File _ _)) _) = True - local (Path (PathHashed _ (Env _ )) _) = True + let local (Import (ImportHashed _ (URL {})) _) = False + local (Import (ImportHashed _ (Local {})) _) = True + local (Import (ImportHashed _ (Env {})) _) = True - let parent = canonicalizePath paths - let here = canonicalizePath (path:paths) + let parent = canonicalizeImport imports + let here = canonicalizeImport (import_:imports) if local here && not (local parent) - then throwM (Imported paths (ReferentiallyOpaque path)) + then throwM (Imported imports (ReferentiallyOpaque import_)) else return () - (expr, cached) <- if here `elem` canonicalizeAll paths - then throwM (Imported paths (Cycle path)) + expr <- if here `elem` canonicalizeAll imports + then throwM (Imported imports (Cycle import_)) else do m <- zoom cache State.get case Map.lookup here m of - Just expr -> return (expr, True) + Just expr -> return expr Nothing -> do - expr' <- loadDynamic from_path path + expr' <- loadDynamic from_import import_ expr'' <- case traverse (\_ -> Nothing) expr' of -- No imports left - Just expr -> do - zoom cache (State.put $! Map.insert here expr m) - return expr + Just expr -> return expr -- Some imports left, so recurse Nothing -> do - let paths' = path:paths - zoom stack (State.put paths') - expr'' <- fmap join (traverse (loadStaticWith from_path ctx) + let imports' = import_:imports + zoom stack (State.put imports') + expr'' <- fmap join (traverse (loadStaticWith from_import ctx n) expr') - zoom stack (State.put paths) + zoom stack (State.put imports) return expr'' - return (expr'', False) - - -- Type-check expressions here for three separate reasons: - -- - -- * to verify that they are closed - -- * to catch type errors as early in the import process as possible - -- * to avoid normalizing ill-typed expressions that need to be hashed - -- - -- There is no need to check expressions that have been cached, since they - -- have already been checked - if cached - then return () - else case Dhall.TypeCheck.typeWith ctx expr of - Left err -> throwM (Imported (path:paths) err) - Right _ -> return () + -- Type-check expressions here for three separate reasons: + -- + -- * to verify that they are closed + -- * to catch type errors as early in the import process + -- as possible + -- * to avoid normalizing ill-typed expressions that need + -- to be hashed + -- + -- There is no need to check expressions that have been + -- cached, since they have already been checked + expr''' <- case Dhall.TypeCheck.typeWith ctx expr'' of + Left err -> throwM (Imported (import_:imports) err) + Right _ -> return (Dhall.Core.normalizeWith n expr'') + zoom cache (State.put $! Map.insert here expr''' m) + return expr''' - case hash (pathHashed path) of + case hash (importHashed import_) of Nothing -> do return () Just expectedHash -> do let actualHash = hashExpression expr if expectedHash == actualHash then return () - else throwM (HashMismatch {..}) + else throwM (Imported (import_:imports) (HashMismatch {..})) return expr @@ -814,8 +741,8 @@ evalStatus cb expr = State.evalStateT (fmap join (traverse cb expr)) emptyStatus -- | Resolve all imports within an expression -load :: Expr Src Path -> IO (Expr Src X) -load = loadWithContext Dhall.Context.empty +load :: Expr Src Import -> IO (Expr Src X) +load = loadWithContext Dhall.Context.empty (const Nothing) -- | Hash a fully resolved expression hashExpression :: Expr s X -> (Crypto.Hash.Digest SHA256) diff --git a/src/Dhall/Parser.hs b/src/Dhall/Parser.hs --- a/src/Dhall/Parser.hs +++ b/src/Dhall/Parser.hs @@ -50,6 +50,7 @@ import qualified Data.HashMap.Strict.InsOrd import qualified Data.HashSet import qualified Data.List +import qualified Data.List.NonEmpty import qualified Data.Sequence import qualified Data.Set import qualified Data.Text @@ -748,11 +749,15 @@ return (sign a) ) "double literal" integerLiteral :: Parser Integer -integerLiteral = Text.Parser.Token.integer "integer literal" +integerLiteral = (do + let positive = fmap (\_ -> id ) (Text.Parser.Char.char '+') + let negative = fmap (\_ -> negate) (Text.Parser.Char.char '-') + sign <- positive <|> negative + a <- Text.Parser.Token.natural + return (sign a) ) "integer literal" naturalLiteral :: Parser Natural naturalLiteral = (do - _ <- Text.Parser.Char.char '+' a <- Text.Parser.Token.natural return (fromIntegral a) ) "natural literal" @@ -767,75 +772,87 @@ n <- indexed <|> pure 0 return (V x n) -headPathCharacter :: Char -> Bool -headPathCharacter c = - ('\x21' <= c && c <= '\x27') +pathCharacter :: Char -> Bool +pathCharacter c = + ('\x21' <= c && c <= '\x22') + || ('\x24' <= c && c <= '\x27') || ('\x2A' <= c && c <= '\x2B') || ('\x2D' <= c && c <= '\x2E') || ('\x30' <= c && c <= '\x3B') || c == '\x3D' - || ('\x3F' <= c && c <= '\x5A') + || ('\x40' <= c && c <= '\x5A') || ('\x5E' <= c && c <= '\x7A') || c == '\x7C' || c == '\x7E' -pathCharacter :: Char -> Bool -pathCharacter c = - headPathCharacter c - || c == '\\' - || c == '/' +pathComponent :: Parser Text +pathComponent = do + _ <- "/" :: Parser Builder + string <- some (Text.Parser.Char.satisfy pathCharacter) -fileRaw :: Parser PathType -fileRaw = + return (Data.Text.Lazy.pack string) + +file_ :: Parser File +file_ = do + path <- Data.List.NonEmpty.some1 pathComponent + + let directory = Directory (reverse (Data.List.NonEmpty.init path)) + let file = Data.List.NonEmpty.last path + + return (File {..}) + +localRaw :: Parser ImportType +localRaw = choice - [ try absolutePath - , relativePath - , parentPath + [ parentPath + , herePath , homePath + , try absolutePath ] where - absolutePath = do - _ <- Text.Parser.Char.char '/' - a <- Text.Parser.Char.satisfy headPathCharacter - bs <- many (Text.Parser.Char.satisfy pathCharacter) - let filepath = '/':a:bs - return (File Homeless filepath) + parentPath = do + _ <- ".." :: Parser Builder + file <- file_ - relativePath = do - _ <- Text.Parser.Char.text "./" - as <- many (Text.Parser.Char.satisfy pathCharacter) - let filepath = "./" <> as - return (File Homeless filepath) + return (Local Parent file) - parentPath = do - _ <- Text.Parser.Char.text "../" - as <- many (Text.Parser.Char.satisfy pathCharacter) - let filepath = "../" <> as - return (File Homeless filepath) + herePath = do + _ <- "." :: Parser Builder + file <- file_ + return (Local Here file) + homePath = do - _ <- Text.Parser.Char.text "~/" - as <- many (Text.Parser.Char.satisfy pathCharacter) - return (File Home as) + _ <- "~" :: Parser Builder + file <- file_ -file :: Parser PathType -file = do - a <- fileRaw + return (Local Home file) + + absolutePath = do + file <- file_ + + return (Local Absolute file) + +local :: Parser ImportType +local = do + a <- localRaw whitespace return a scheme :: Parser Builder scheme = "http" <> option "s" -httpRaw :: Parser Builder -httpRaw = - scheme - <> "://" - <> authority - <> pathAbempty - <> option ("?" <> query) - <> option ("#" <> fragment) +httpRaw :: Parser (Text, File, Text) +httpRaw = do + prefix <- scheme <> "://" <> authority + file <- file_ + suffix <- option ("?" <> query) <> option ("#" <> fragment) + let prefixText = Data.Text.Lazy.Builder.toLazyText prefix + let suffixText = Data.Text.Lazy.Builder.toLazyText suffix + + return (prefixText, file, suffixText) + authority :: Parser Builder authority = option (try (userinfo <> "@")) <> host <> option (":" <> port) @@ -942,12 +959,6 @@ where predicate c = unreserved c || subDelims c -pathAbempty :: Parser Builder -pathAbempty = star ("/" <> segment) - -segment :: Parser Builder -segment = star pchar - pchar :: Parser Builder pchar = satisfy predicate <|> pctEncoded where @@ -973,16 +984,16 @@ subDelims :: Char -> Bool subDelims c = c `elem` ("!$&'()*+,;=" :: String) -http :: Parser PathType +http :: Parser ImportType http = do - a <- httpRaw + (prefix, path, suffix) <- httpRaw whitespace - b <- optional (do + headers <- optional (do _using - pathHashed_ ) - return (URL (Data.Text.Lazy.Builder.toLazyText a) b) + importHashed_ ) + return (URL prefix path suffix headers) -env :: Parser PathType +env :: Parser ImportType env = do _ <- Text.Parser.Char.text "env:" a <- (alternative0 <|> alternative1) @@ -1546,7 +1557,7 @@ snoc m (k, v) = Data.HashMap.Strict.InsOrd.insertWith combine k v m -- | Parser for a top-level Dhall expression -expr :: Parser (Expr Src Path) +expr :: Parser (Expr Src Import) expr = exprA import_ -- | Parser for a top-level Dhall expression. The expression is parameterized @@ -1554,16 +1565,16 @@ exprA :: Parser a -> Parser (Expr Src a) exprA = completeExpression -pathType_ :: Parser PathType -pathType_ = choice [ file, http, env ] +importType_ :: Parser ImportType +importType_ = choice [ local, http, env ] -pathHashed_ :: Parser PathHashed -pathHashed_ = do - pathType <- pathType_ - hash <- optional pathHash_ - return (PathHashed {..}) +importHashed_ :: Parser ImportHashed +importHashed_ = do + importType <- importType_ + hash <- optional importHash_ + return (ImportHashed {..}) where - pathHash_ = do + importHash_ = do _ <- Text.Parser.Char.text "sha256:" builder <- count 64 (satisfy hexdig "hex digit") whitespace @@ -1577,11 +1588,11 @@ Nothing -> fail "Invalid sha256 hash" Just h -> pure h -import_ :: Parser Path +import_ :: Parser Import import_ = (do - pathHashed <- pathHashed_ - pathMode <- alternative <|> pure Code - return (Path {..}) ) "import" + importHashed <- importHashed_ + importMode <- alternative <|> pure Code + return (Import {..}) ) "import" where alternative = do _as @@ -1601,7 +1612,7 @@ instance Exception ParseError -- | Parse an expression from `Text` containing a Dhall program -exprFromText :: String -> Text -> Either ParseError (Expr Src Path) +exprFromText :: String -> Text -> Either ParseError (Expr Src Import) exprFromText delta text = fmap snd (exprAndHeaderFromText delta text) {-| Like `exprFromText` but also returns the leading comments and whitespace @@ -1619,7 +1630,7 @@ exprAndHeaderFromText :: String -> Text - -> Either ParseError (Text, Expr Src Path) + -> Either ParseError (Text, Expr Src Import) exprAndHeaderFromText delta text = case result of Left errInfo -> Left (ParseError { unwrap = errInfo, input = text }) Right (txt, r) -> Right (Data.Text.Lazy.dropWhileEnd (/= '\n') txt, r) diff --git a/src/Dhall/Pretty/Internal.hs b/src/Dhall/Pretty/Internal.hs --- a/src/Dhall/Pretty/Internal.hs +++ b/src/Dhall/Pretty/Internal.hs @@ -736,10 +736,11 @@ builtin "True" prettyExprF (BoolLit False) = builtin "False" -prettyExprF (IntegerLit a) = - prettyNumber a +prettyExprF (IntegerLit a) + | 0 <= a = literal "+" <> prettyNumber a + | otherwise = prettyNumber a prettyExprF (NaturalLit a) = - literal "+" <> prettyNatural a + prettyNatural a prettyExprF (DoubleLit a) = prettyScientific a prettyExprF (TextLit a) = @@ -1094,10 +1095,11 @@ "True" buildExprF (BoolLit False) = "False" -buildExprF (IntegerLit a) = - buildNumber a +buildExprF (IntegerLit a) + | 0 <= a = "+" <> buildNumber a + | otherwise = buildNumber a buildExprF (NaturalLit a) = - "+" <> buildNatural a + buildNatural a buildExprF (DoubleLit a) = buildScientific a buildExprF (TextLit a) = diff --git a/src/Dhall/Tutorial.hs b/src/Dhall/Tutorial.hs --- a/src/Dhall/Tutorial.hs +++ b/src/Dhall/Tutorial.hs @@ -189,7 +189,7 @@ -- > -- > import Dhall -- > --- > data Example = Example { foo :: Integer, bar :: Vector Double } +-- > data Example = Example { foo :: Natural, bar :: Vector Double } -- > deriving (Generic, Show) -- > -- > instance Interpret Example @@ -275,7 +275,7 @@ -- > -- > import Dhall -- > --- > data Person = Person { age :: Integer, name :: Text } +-- > data Person = Person { age :: Natural, name :: Text } -- > deriving (Generic, Show) -- > -- > instance Interpret Person @@ -304,16 +304,25 @@ -- Suppose that we try to decode a value of the wrong type, like this: -- -- > >>> input auto "1" :: IO Bool --- > *** Exception: +-- > *** Exception: -- > Error: Expression doesn't match annotation -- > +-- > - Bool +-- > + Natural +-- > -- > 1 : Bool -- > -- > (input):1:1 -- -- The interpreter complains because the string @\"1\"@ cannot be decoded into a --- Haskell value of type `Bool`. +-- Haskell value of type `Bool`. This part of the type error: -- +-- > - Bool +-- > + Natural +-- +-- ... means that the expected type was @Bool@ but the inferred type of the +-- expression @1@ was @Natural@. +-- -- The code excerpt from the above error message has two components: -- -- * the expression being type checked (i.e. @1@) @@ -406,7 +415,7 @@ -- -- ... then the interpreter will reject the import: -- --- > >>> input auto "./file1" :: IO Integer +-- > >>> input auto "./file1" :: IO Natural -- > *** Exception: -- > ↳ ./file1 -- > ↳ ./file2 @@ -438,7 +447,7 @@ -- You can also import Dhall expressions from environment variables, too: -- -- > >>> System.Environment.setEnv "FOO" "1" --- > >>> input auto "env:FOO" :: IO Integer +-- > >>> input auto "env:FOO" :: IO Natural -- > 1 -- -- You can import types, too. For example, we can change our @./bar@ file to: @@ -474,12 +483,12 @@ -- -- __Exercise:__ There is a @not@ function hosted online here: -- --- +-- -- -- Visit that link and read the documentation. Then try to guess what this -- code returns: -- --- > >>> input auto "https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool +-- > >>> input auto "https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/Bool/not https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool -- > ??? -- -- Run the code to test your guess @@ -494,31 +503,35 @@ -- required for empty lists but optional for non-empty lists. You will get a -- type error if you provide an empty list without a type annotation: -- --- > >>> input auto "[]" :: IO (Vector Integer) --- > *** Exception: --- > Error: Empty lists need a type annotation --- > --- > [] +-- > >>> input auto "[]" :: IO (Vector Natural) +-- > *** Exception: +-- > Error: Invalid input -- > --- > (input):1:1 --- > >>> input auto "[] : List Integer" :: IO (Vector Integer) --- > [] +-- > (input):1:3: +-- > | +-- > 1 | [] +-- > | ^ +-- > unexpected end of input +-- > expecting ':' or whitespace -- -- Also, list elements must all have the same type. You will get an error if -- you try to store elements of different types in a list: -- --- > >>> input auto "[1, True, 3]" :: IO (Vector Integer) --- > *** Exception: --- > Error: List elements should have the same type +-- > >>> input auto "[1, True, 3]" :: IO (Vector Natural) +-- > *** Exception: +-- > Error: List elements should all have the same type -- > --- > [1, True, 3] +-- > - Natural +-- > + Bool -- > --- > (input):1:1 +-- > True +-- > +-- > (input):1:5 -- -- __Exercise:__ What is the shortest @./config@ file that you can decode using -- this command: -- --- > >>> input auto "./config" :: IO (Vector (Vector Integer)) +-- > >>> input auto "./config" :: IO (Vector (Vector Natural)) -- $optional0 -- @@ -527,19 +540,19 @@ -- -- For example, these are valid @Optional@ values: -- --- > [1] : Optional Integer +-- > [1] : Optional Natural -- > --- > [] : Optional Integer +-- > [] : Optional Natural -- -- ... but this is /not/ valid: -- --- > [1, 2] : Optional Integer -- NOT valid +-- > [1, 2] : Optional Natural -- NOT valid -- -- An @Optional@ corresponds to Haskell's `Maybe` type for decoding purposes: -- --- > >>> input auto "[1] : Optional Integer" :: IO (Maybe Integer) +-- > >>> input auto "[1] : Optional Natural" :: IO (Maybe Natural) -- > Just 1 --- > >>> input auto "[] : Optional Integer" :: IO (Maybe Integer) +-- > >>> input auto "[] : Optional Natural" :: IO (Maybe Natural) -- > Nothing -- -- You cannot omit the type annotation for @Optional@ values. The type @@ -548,7 +561,7 @@ -- __Exercise:__ What is the shortest possible @./config@ file that you can decode -- like this: -- --- > >>> input auto "./config" :: IO (Maybe (Maybe (Maybe Integer))) +-- > >>> input auto "./config" :: IO (Maybe (Maybe (Maybe Natural))) -- > ??? -- -- __Exercise:__ Try to decode an @Optional@ value with more than one element and @@ -569,7 +582,7 @@ -- record literal has the following record type: -- -- > { foo : Bool --- > , bar : Integer +-- > , bar : Natural -- > , baz : Double -- > } -- @@ -612,7 +625,7 @@ -- > $ dhall -- > { x = 1, y = True, z = "ABC" }.{ x, y } -- > --- > { x : Integer, y : Bool } +-- > { x : Natural, y : Bool } -- > -- > { x = 1, y = True } -- @@ -714,7 +727,7 @@ -- > -- > ∀(n : Bool) → List Bool -- > --- > λ(n : Bool) → [n && True, n && False, n || True, n || False] +-- > λ(n : Bool) → [ n, False, True, n ] -- -- The first line says that @makeBools@ is a function of one argument named @n@ -- that has type @Bool@ and the function returns a @List@ of @Bool@s. The @∀@ @@ -737,10 +750,15 @@ -- -- The second line of Dhall's output is our program's normal form: -- --- > λ(n : Bool) → [n && True, n && False, n || True, n || False] +-- > λ(n : Bool) → [ n, False, True, n ] -- --- ... which in this case happens to be identical to our original program. +-- ... and the interpreter was able to simplify our expression by noting that: -- +-- * @n && True = n@ +-- * @n && False = False@ +-- * @n || True = True@ +-- * @n || False = n@ +-- -- To apply a function to an argument you separate the function and argument by -- whitespace (just like Haskell): -- @@ -847,7 +865,7 @@ -- > $ dhall -- > let name = "John Doe" -- > in let age = 21 --- > in "My name is ${name} and my age is ${Integer/show age}" +-- > in "My name is ${name} and my age is ${Natural/show age}" -- > -- > Text -- > @@ -875,13 +893,13 @@ -- > $ dhall -- > { foo = 1, bar = "ABC" } // { baz = True } -- > --- > { bar : Text, baz : Bool, foo : Integer } +-- > { bar : Text, baz : Bool, foo : Natural } -- > -- > { bar = "ABC", baz = True, foo = 1 } -- > $ dhall -- > { foo = 1, bar = "ABC" } ⫽ { bar = True } -- Fancy unicode -- > --- > { bar : Bool, foo : Integer } +-- > { bar : Bool, foo : Natural } -- > -- > { bar = True, foo = 1 } -- @@ -926,9 +944,9 @@ -- operator descends recursively into record types: -- -- > $ dhall --- > { foo : { bar : Text } } ⩓ { foo : { baz : Bool }, qux : Integer } +-- > { foo : { bar : Text } } ⩓ { foo : { baz : Bool }, qux : Natural } -- > --- > { foo : { bar : Text, baz : Bool }, qux : Integer } +-- > { foo : { bar : Text, baz : Bool }, qux : Natural } -- $let -- @@ -983,10 +1001,14 @@ -- > $ dhall -- > let twice (x : Text) = x ++ x in twice "ha" -- > --- > (stdin):1:11: error: expected: ":", --- > "=" --- > let twice (x : Text) = x ++ x in twice "ha" --- > ^ +-- > Error: Invalid input +-- > +-- > (stdin):1:11: +-- > | +-- > 1 | let twice (x : Text) = x ++ x in twice "ha" +-- > | ^ +-- > unexpected '(' +-- > expecting ':', '=', or the rest of label -- -- The error message says that Dhall expected either a @(:)@ (i.e. the beginning -- of a type annotation) or a @(=)@ (the beginning of the assignment) and not a @@ -995,7 +1017,7 @@ -- You can also use @let@ expressions to rename imports, like this: -- -- > $ dhall --- > let not = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not +-- > let not = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/Bool/not -- > in not True -- > -- > Bool @@ -1048,7 +1070,7 @@ -- remaining alternatives. For example, both of the following union literals -- have the same type, which is the above union type: -- --- > < Left = +0 | Right : Bool > +-- > < Left = 0 | Right : Bool > -- -- > < Right = True | Left : Natural > -- @@ -1070,7 +1092,7 @@ -- Now our @./process@ function can handle both alternatives: -- -- > $ dhall --- > ./process < Left = +3 | Right : Bool > +-- > ./process < Left = 3 | Right : Bool > -- > -- > Bool -- > @@ -1100,8 +1122,8 @@ -- -- So, for example: -- --- > merge { Left = Natural/even, Right = λ(b : Bool) → b } < Left = +3 | Right : Bool > : Bool --- > = Natural/even +3 : Bool +-- > merge { Left = Natural/even, Right = λ(b : Bool) → b } < Left = 3 | Right : Bool > : Bool +-- > = Natural/even 3 : Bool -- > = False -- -- ... and similarly: @@ -1135,8 +1157,8 @@ -- > in let Person = -- > λ(p : { name : Text, age : Natural }) → < Person = p | Empty : {} > -- > in [ Empty --- > , Person { name = "John", age = +23 } --- > , Person { name = "Amy" , age = +25 } +-- > , Person { name = "John", age = 23 } +-- > , Person { name = "Amy" , age = 25 } -- > , Empty -- > ] -- @@ -1145,8 +1167,8 @@ -- -- > let MyType = constructors < Empty : {} | Person : { name : Text, age : Natural } > -- > in [ MyType.Empty {=} --- > , MyType.Person { name = "John", age = +23 } --- > , MyType.Person { name = "Amy" , age = +25 } +-- > , MyType.Person { name = "John", age = 23 } +-- > , MyType.Person { name = "Amy" , age = 25 } -- > ] -- -- The @constructors@ keyword takes a union type argument and returns a record @@ -1186,7 +1208,7 @@ -- __Exercise__: Create a list of the following type with at least one element -- per alternative: -- --- > List < Left : Integer | Right : Double > +-- > List < Left : Natural | Right : Double > -- $polymorphic -- @@ -1236,15 +1258,15 @@ -- argument). The result also has type @a@.\" -- -- This means that the type of the second argument changes depending on what --- type we provide for the first argument. When we apply @./id@ to @Integer@, we --- create a function that expects an @Integer@ argument: +-- type we provide for the first argument. When we apply @./id@ to @Natural@, +-- we create a function that expects an @Natural@ argument: -- -- > $ dhall --- > ./id Integer +-- > ./id Natural -- > --- > ∀(x : Integer) → Integer +-- > ∀(x : Natural) → Natural -- > --- > λ(x : Integer) → x +-- > λ(x : Natural) → x -- -- Similarly, when we apply @./id@ to @Bool@, we create a function that expects a -- @Bool@ argument: @@ -1260,9 +1282,9 @@ -- that they both work on their respective types: -- -- > $ dhall --- > ./id Integer 4 +-- > ./id Natural 4 -- > --- > Integer +-- > Natural -- > -- > 4 -- @@ -1317,11 +1339,11 @@ -- > $ dhall -- > λ(_ : Text) → 1 -- > --- > Text → Integer +-- > Text → Natural -- > -- > λ(_ : Text) → 1 -- --- The type @(Text → Integer)@ is the same as @(∀(_ : Text) → Integer)@ +-- The type @(Text → Natural)@ is the same as @(∀(_ : Text) → Natural)@ -- -- __Exercise__ : Translate Haskell's `flip` function to Dhall @@ -1339,11 +1361,11 @@ -- applied. For example, the following program is an anonymous function: -- -- > $ dhall --- > \(n : Bool) -> +10 * +10 +-- > \(n : Bool) -> 10 * 10 -- > -- > ∀(n : Bool) → Natural -- > --- > λ(n : Bool) → +100 +-- > λ(n : Bool) → 100 -- -- ... and even though the function is still missing the first argument named -- @n@ the compiler is smart enough to evaluate the body of the anonymous @@ -1353,12 +1375,12 @@ -- complex example: -- -- > $ dhall --- > let Prelude/List/map = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/map --- > in λ(f : Integer → Integer) → Prelude/List/map Integer Integer f [1, 2, 3] +-- > let Prelude/List/map = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/map +-- > in λ(f : Natural → Natural) → Prelude/List/map Natural Natural f [1, 2, 3] -- > --- > ∀(f : Integer → Integer) → List Integer +-- > ∀(f : Natural → Natural) → List Natural -- > --- > λ(f : Integer → Integer) → [f 1, f 2, f 3] : List Integer +-- > λ(f : Natural → Natural) → [f 1, f 2, f 3] : List Natural -- -- Dhall can apply our function to each element of the list even before we specify -- which function to apply. @@ -1368,21 +1390,21 @@ -- an @Optional@ value: -- -- > $ dhall --- > List/head Integer ([] : List Integer) +-- > List/head Natural ([] : List Natural) -- > --- > Optional Integer +-- > Optional Natural -- > --- > [] : Optional Integer +-- > [] : Optional Natural -- -- __Exercise__: The Dhall Prelude provides a @replicate@ function which you can -- find here: -- --- +-- -- -- Test what the following Dhall expression normalizes to: -- --- > let replicate = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate --- > in replicate +10 +-- > let replicate = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/replicate +-- > in replicate 10 -- -- __Exercise__: If you have a lot of spare time, try to \"break the compiler\" by -- finding an input expression that crashes or loops forever (and file a bug @@ -1461,7 +1483,7 @@ -- imported Dhall value and reject the import if there is a hash mismatch: -- -- > $ dhall <<< './foo' --- > Integer +-- > Natural -- > -- > 1 -- @@ -1477,7 +1499,7 @@ -- changes to whitespace or comments: -- -- > $ dhall <<< './foo' # This still succeeds --- > Integer +-- > Natural -- > -- > 1 -- @@ -1592,7 +1614,7 @@ -- > index : Natural, value : a } kvs list (λ(kvOld : { index : Natural, value : a -- > }) → λ(z : list) → cons { index = kvOld.index + n, value = kvOld.value } -- > z) (y.diff (n + List/length { index : Natural, value : a } kvs)) }) { count = --- > +0, diff = λ(_ : Natural) → nil }).diff +0) +-- > 0, diff = λ(_ : Natural) → nil }).diff 0) -- -- ... and run the expression through the @dhall-format@ executable: -- @@ -1624,25 +1646,25 @@ -- > (y.diff (n + List/length { index : Natural, value : a } kvs)) -- > } -- > ) --- > { count = +0, diff = λ(_ : Natural) → nil } +-- > { count = 0, diff = λ(_ : Natural) → nil } -- > ).diff --- > +0 +-- > 0 -- > ) -- -- The executable formats expressions without resolving, type-checking, or -- normalizing them: -- -- > $ dhall-format --- > let replicate = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate --- > in replicate +5 (List (List Integer)) (replicate +5 (List Integer) (replicate +5 Integer 1)) +-- > let replicate = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/replicate +-- > in replicate 5 (List (List Natural)) (replicate 5 (List Natural) (replicate 5 Natural 1)) -- > -- > let replicate = --- > https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate +-- > https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/replicate -- > -- > in replicate --- > +5 --- > (List (List Integer)) --- > (replicate +5 (List Integer) (replicate +5 Integer 1)) +-- > 5 +-- > (List (List Natural)) +-- > (replicate 5 (List Natural) (replicate 5 Natural 1)) -- -- You can also use the formatter to modify files in place using the -- @--inplace@ flag (i.e. for formatting source code): @@ -1676,9 +1698,9 @@ -- > (y.diff (n + List/length { index : Natural, value : a } kvs)) -- > } -- > ) --- > { count = +0, diff = λ(_ : Natural) → nil } +-- > { count = 0, diff = λ(_ : Natural) → nil } -- > ).diff --- > +0 +-- > 0 -- > ) -- -- Carefully note that the code formatter does not preserve all comments. @@ -1700,48 +1722,48 @@ -- multi-line expressions, too: -- -- > $ dhall --- > let replicate = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate --- > in replicate +5 (List (List Integer)) (replicate +5 (List Integer) (replicate +5 Integer 1)) +-- > let replicate = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/replicate +-- > in replicate 5 (List (List Natural)) (replicate 5 (List Natural) (replicate 5 Natural 1)) -- > --- > List (List (List Integer)) +-- > List (List (List Natural)) -- > --- > [ [ [ 1, 1, 1, 1, 1 ] : List Integer --- > , [ 1, 1, 1, 1, 1 ] : List Integer --- > , [ 1, 1, 1, 1, 1 ] : List Integer --- > , [ 1, 1, 1, 1, 1 ] : List Integer --- > , [ 1, 1, 1, 1, 1 ] : List Integer +-- > [ [ [ 1, 1, 1, 1, 1 ] : List Natural +-- > , [ 1, 1, 1, 1, 1 ] : List Natural +-- > , [ 1, 1, 1, 1, 1 ] : List Natural +-- > , [ 1, 1, 1, 1, 1 ] : List Natural +-- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > ] --- > : List (List Integer) --- > , [ [ 1, 1, 1, 1, 1 ] : List Integer --- > , [ 1, 1, 1, 1, 1 ] : List Integer --- > , [ 1, 1, 1, 1, 1 ] : List Integer --- > , [ 1, 1, 1, 1, 1 ] : List Integer --- > , [ 1, 1, 1, 1, 1 ] : List Integer +-- > : List (List Natural) +-- > , [ [ 1, 1, 1, 1, 1 ] : List Natural +-- > , [ 1, 1, 1, 1, 1 ] : List Natural +-- > , [ 1, 1, 1, 1, 1 ] : List Natural +-- > , [ 1, 1, 1, 1, 1 ] : List Natural +-- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > ] --- > : List (List Integer) --- > , [ [ 1, 1, 1, 1, 1 ] : List Integer --- > , [ 1, 1, 1, 1, 1 ] : List Integer --- > , [ 1, 1, 1, 1, 1 ] : List Integer --- > , [ 1, 1, 1, 1, 1 ] : List Integer --- > , [ 1, 1, 1, 1, 1 ] : List Integer +-- > : List (List Natural) +-- > , [ [ 1, 1, 1, 1, 1 ] : List Natural +-- > , [ 1, 1, 1, 1, 1 ] : List Natural +-- > , [ 1, 1, 1, 1, 1 ] : List Natural +-- > , [ 1, 1, 1, 1, 1 ] : List Natural +-- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > ] --- > : List (List Integer) --- > , [ [ 1, 1, 1, 1, 1 ] : List Integer --- > , [ 1, 1, 1, 1, 1 ] : List Integer --- > , [ 1, 1, 1, 1, 1 ] : List Integer --- > , [ 1, 1, 1, 1, 1 ] : List Integer --- > , [ 1, 1, 1, 1, 1 ] : List Integer +-- > : List (List Natural) +-- > , [ [ 1, 1, 1, 1, 1 ] : List Natural +-- > , [ 1, 1, 1, 1, 1 ] : List Natural +-- > , [ 1, 1, 1, 1, 1 ] : List Natural +-- > , [ 1, 1, 1, 1, 1 ] : List Natural +-- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > ] --- > : List (List Integer) --- > , [ [ 1, 1, 1, 1, 1 ] : List Integer --- > , [ 1, 1, 1, 1, 1 ] : List Integer --- > , [ 1, 1, 1, 1, 1 ] : List Integer --- > , [ 1, 1, 1, 1, 1 ] : List Integer --- > , [ 1, 1, 1, 1, 1 ] : List Integer +-- > : List (List Natural) +-- > , [ [ 1, 1, 1, 1, 1 ] : List Natural +-- > , [ 1, 1, 1, 1, 1 ] : List Natural +-- > , [ 1, 1, 1, 1, 1 ] : List Natural +-- > , [ 1, 1, 1, 1, 1 ] : List Natural +-- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > ] --- > : List (List Integer) +-- > : List (List Natural) -- > ] --- > : List (List (List Integer)) +-- > : List (List (List Natural)) -- $builtins -- @@ -1782,18 +1804,19 @@ -- -- First, Dhall only supports addition and multiplication on @Natural@ numbers -- (i.e. non-negative integers), which are not the same type of number as --- @Integer@s (which can be negative). A @Natural@ number is a number prefixed --- with the @+@ symbol. If you try to add or multiply two @Integer@s (without --- the @+@ prefix) you will get a type error: +-- @Integer@s (which can be negative). An @Integer@ number is a number prefixed +-- with either a @+@ or @-@ symbol whereas a @Natural@ number has no leading +-- sign. If you try to add or multiply two @Integer@s you will get a type +-- error: -- -- > $ dhall --- > 2 + 2 +-- > +2 + +2 -- > -- > Use "dhall --explain" for detailed errors -- > -- > Error: ❰+❱ only works on ❰Natural❱s -- > --- > 2 + 2 +-- > +2 + +2 -- > -- > (stdin):1:1 -- @@ -1983,7 +2006,7 @@ -- > $ dhall -- > if True then 3 else 5 -- > --- > Integer +-- > Natural -- > -- > 3 -- @@ -2005,11 +2028,12 @@ -- $natural -- --- @Natural@ literals are numbers prefixed by a @+@ sign, like this: +-- @Natural@ literals are non-negative numbers without any leading sign, like +-- this: -- --- > +4 : Natural +-- > 4 : Natural -- --- If you omit the @+@ sign then you get an @Integer@ literal, which is a +-- If you add a @+@ or @-@ sign then you get an @Integer@ literal, which is a -- different type of value -- $plus @@ -2017,11 +2041,11 @@ -- Example: -- -- > $ dhall --- > +2 + +3 +-- > 2 + 3 -- > -- > Natural -- > --- > +5 +-- > 5 -- -- Type: -- @@ -2033,20 +2057,20 @@ -- -- > (x + y) + z = x + (y + z) -- > --- > x + +0 = x +-- > x + 0 = x -- > --- > +0 + x = x +-- > 0 + x = x -- $times -- -- Example: -- -- > $ dhall --- > +2 * +3 +-- > 2 * 3 -- > -- > Natural -- > --- > +6 +-- > 6 -- -- Type: -- @@ -2058,24 +2082,24 @@ -- -- > (x * y) * z = x * (y * z) -- > --- > x * +1 = x +-- > x * 1 = x -- > --- > +1 * x = x +-- > 1 * x = x -- > -- > (x + y) * z = (x * z) + (y * z) -- > -- > x * (y + z) = (x * y) + (x * z) -- > --- > x * +0 = +0 +-- > x * 0 = 0 -- > --- > +0 * x = +0 +-- > 0 * x = 0 -- $even -- -- Example: -- -- > $ dhall --- > Natural/even +6 +-- > Natural/even 6 -- > -- > Bool -- > @@ -2090,18 +2114,18 @@ -- -- > Natural/even (x + y) = Natural/even x == Natural/even y -- > --- > Natural/even +0 = True +-- > Natural/even 0 = True -- > -- > Natural/even (x * y) = Natural/even x || Natural/even y -- > --- > Natural/even +1 = False +-- > Natural/even 1 = False -- $odd -- -- Example: -- -- > $ dhall --- > Natural/odd +6 +-- > Natural/odd 6 -- > -- > Bool -- > @@ -2116,18 +2140,18 @@ -- -- > Natural/odd (x + y) = Natural/odd x != Natural/odd y -- > --- > Natural/odd +0 = False +-- > Natural/odd 0 = False -- > -- > Natural/odd (x * y) = Natural/odd x && Natural/odd y -- > --- > Natural/odd +1 = True +-- > Natural/odd 1 = True -- $isZero -- -- Example: -- -- > $ dhall --- > Natural/isZero +6 +-- > Natural/isZero 6 -- > -- > Bool -- > @@ -2142,18 +2166,18 @@ -- -- > Natural/isZero (x + y) = Natural/isZero x && Natural/isZero y -- > --- > Natural/isZero +0 = True +-- > Natural/isZero 0 = True -- > -- > Natural/isZero (x * y) = Natural/isZero x || Natural/isZero y -- > --- > Natural/isZero +1 = False +-- > Natural/isZero 1 = False -- $naturalFold -- -- Example: -- -- > $ dhall --- > Natural/fold +40 Text (λ(t : Text) → t ++ "!") "You're welcome" +-- > Natural/fold 40 Text (λ(t : Text) → t ++ "!") "You're welcome" -- > -- > Text -- > @@ -2168,11 +2192,11 @@ -- -- > Natural/fold (x + y) n s z = Natural/fold x n s (Natural/fold y n s z) -- > --- > Natural/fold +0 n s z = z +-- > Natural/fold 0 n s z = z -- > -- > Natural/fold (x * y) n s = Natural/fold x n (Natural/fold y n s) -- > --- > Natural/fold +1 n s = s +-- > Natural/fold 1 n s = s -- $naturalBuild -- @@ -2183,7 +2207,7 @@ -- > -- > Natural -- > --- > +2 +-- > 2 -- -- Type: -- @@ -2198,14 +2222,13 @@ -- $integer -- --- @Integer@ literals are either prefixed with a @-@ sign (if they are negative) --- or no sign (if they are positive), like this: +-- @Integer@ literals are prefixed with a @+@ (if they are non-negative) or a +-- @-@ sign (if they are negative), like this: -- --- > 3 : Integer +-- > +3 : Integer -- > -2 : Integer -- --- If you prefix them with a @+@ sign then they are @Natural@ literals and not --- @Integer@s +-- If you omit the sign then they are @Natural@ literals and not @Integer@s -- -- There are no built-in operations on @Integer@s. For all practical purposes -- they are opaque values within the Dhall language @@ -2266,7 +2289,7 @@ -- -- Also, every empty @List@ must end with a mandatory type annotation, for example: -- --- > [] : List Integer +-- > [] : List Natural -- -- The built-in operations on @List@s are: @@ -2277,7 +2300,7 @@ -- > $ dhall -- > [1, 2, 3] # [4, 5, 6] -- > --- > List Integer +-- > List Natural -- > -- > [1, 2, 3, 4, 5, 6] -- @@ -2313,7 +2336,7 @@ -- -- Rules: -- --- > let Prelude/List/concat = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concat +-- > let Prelude/List/concat = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/concat -- > -- > List/fold a (Prelude/List/concat a xss) b c -- > = List/fold (List a) xss b (λ(x : List a) → List/fold a x b c) @@ -2327,11 +2350,11 @@ -- Example: -- -- > $ dhall --- > List/build Integer (λ(list : Type) → λ(cons : Integer → list → list) → λ(nil : list) → cons 1 (cons 2 (cons 3 nil))) +-- > List/build Natural (λ(list : Type) → λ(cons : Natural → list → list) → λ(nil : list) → cons 1 (cons 2 (cons 3 nil))) -- > --- > List Integer +-- > List Natural -- > --- > [1, 2, 3] : List Integer +-- > [1, 2, 3] : List Natural -- -- Type: -- @@ -2349,11 +2372,11 @@ -- Example: -- -- > $ dhall --- > List/length Integer [1, 2, 3] +-- > List/length Natural [1, 2, 3] -- > -- > Natural -- > --- > +3 +-- > 3 -- -- Type: -- @@ -2362,18 +2385,18 @@ -- -- Rules: -- --- > List/length t xs = List/fold t xs Natural (λ(_ : t) → λ(n : Natural) → n + +1) +0 +-- > List/length t xs = List/fold t xs Natural (λ(_ : t) → λ(n : Natural) → n + 1) 0 -- $listHead -- -- Example: -- -- > $ dhall --- > List/head Integer [1, 2, 3] +-- > List/head Natural [1, 2, 3] -- > --- > Optional Integer +-- > Optional Natural -- > --- > [1] : Optional Integer +-- > [1] : Optional Natural -- -- Type: -- @@ -2382,10 +2405,10 @@ -- -- Rules: -- --- > let Prelude/Optional/head = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Optional/head --- > let Prelude/List/concat = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concat --- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concatMap --- > let Prelude/List/map = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/map +-- > let Prelude/Optional/head = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/Optional/head +-- > let Prelude/List/concat = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/concat +-- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/concatMap +-- > let Prelude/List/map = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/map -- > -- > List/head a (Prelude/List/concat a xss) = -- > Prelude/Optional/head a (Prelude/List/map (List a) (Optional a) (List/head a) xss) @@ -2400,11 +2423,11 @@ -- Example: -- -- > $ dhall --- > List/last Integer [1, 2, 3] +-- > List/last Natural [1, 2, 3] -- > --- > Optional Integer +-- > Optional Natural -- > --- > [1] : Optional Integer +-- > [1] : Optional Natural -- -- Type: -- @@ -2413,10 +2436,10 @@ -- -- Rules: -- --- > let Prelude/Optional/last = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Optional/last --- > let Prelude/List/concat = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concat --- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concatMap --- > let Prelude/List/map = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/map +-- > let Prelude/Optional/last = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/Optional/last +-- > let Prelude/List/concat = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/concat +-- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/concatMap +-- > let Prelude/List/map = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/map -- > -- > List/last a (Prelude/List/concat a xss) = -- > Prelude/Optional/last a (Prelude/List/map (List a) (Optional a) (List/last a) xss) @@ -2435,7 +2458,7 @@ -- > -- > List { index : Natural, value : Text } -- > --- > [{ index = +0, value = "ABC" }, { index = +1, value = "DEF" }, { index = +2, value = "GHI" }] : List { index : Natural, value : Text } +-- > [{ index = 0, value = "ABC" }, { index = 1, value = "DEF" }, { index = 2, value = "GHI" }] : List { index : Natural, value : Text } -- -- Type: -- @@ -2444,9 +2467,9 @@ -- -- Rules: -- --- > let Prelude/List/shifted = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/shifted --- > let Prelude/List/concat = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concat --- > let Prelude/List/map = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/map +-- > let Prelude/List/shifted = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/shifted +-- > let Prelude/List/concat = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/concat +-- > let Prelude/List/map = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/map -- > -- > List/indexed a (Prelude/List/concat a xss) = -- > Prelude/List/shifted a (Prelude/List/map (List a) (List { index : Natural, value : a }) (List/indexed a) xss) @@ -2456,11 +2479,11 @@ -- Example: -- -- > $ dhall --- > List/reverse Integer [1, 2, 3] +-- > List/reverse Natural [1, 2, 3] -- > --- > List Integer +-- > List Natural -- > --- > [3, 2, 1] : List Integer +-- > [3, 2, 1] : List Natural -- -- Type: -- @@ -2469,9 +2492,9 @@ -- -- Rules: -- --- > let Prelude/List/map = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/map --- > let Prelude/List/concat = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concat --- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concatMap +-- > let Prelude/List/map = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/map +-- > let Prelude/List/concat = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/concat +-- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/concatMap -- > -- > List/reverse a (Prelude/List/concat a xss) -- > = Prelude/List/concat a (List/reverse (List a) (Prelude/List/map (List a) (List a) (List/reverse a) xss)) @@ -2529,7 +2552,7 @@ -- -- ... which currenty redirects to: -- --- +-- -- -- There is nothing \"official\" or \"standard\" about this Prelude other than -- the fact that it is mentioned in this tutorial. The \"Prelude\" is just a @@ -2540,12 +2563,12 @@ -- subdirectories. For example, the @Bool@ subdirectory has a @not@ file -- located here: -- --- +-- -- -- The @not@ function is just a UTF8-encoded text file hosted online with the -- following contents -- --- > $ curl https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not +-- > $ curl https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/Bool/not -- > {- -- > Flip the value of a `Bool` -- > @@ -2578,7 +2601,7 @@ -- You can use this @not@ function either directly: -- -- > $ dhall --- > https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not True +-- > https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/Bool/not True -- > -- > Bool -- > @@ -2587,7 +2610,7 @@ -- ... or assign the URL to a shorter name: -- -- > $ dhall --- > let Bool/not = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not +-- > let Bool/not = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/Bool/not -- > in Bool/not True -- > -- > Bool @@ -2598,16 +2621,16 @@ -- consistency and documentation, such as @Prelude\/Natural\/even@, which -- re-exports the built-in @Natural/even@ function: -- --- > $ curl https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Natural/even +-- > $ curl https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/Natural/even -- > {- -- > Returns `True` if a number if even and returns `False` otherwise -- > -- > Examples: -- > -- > ``` --- > ./even +3 = False +-- > ./even 3 = False -- > --- > ./even +0 = True +-- > ./even 0 = True -- > ``` -- > -} -- > let even : Natural → Bool @@ -2619,7 +2642,7 @@ -- using local relative paths instead of URLs. For example, you can use @wget@, -- like this: -- --- > $ wget -np -nH -r --cut-dirs=2 https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/ +-- > $ wget -np -nH -r --cut-dirs=2 https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/ -- > $ tree Prelude -- > Prelude -- > ├── Bool @@ -2683,12 +2706,12 @@ -- locally like this: -- -- > $ ipfs mount --- > $ cd /ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude +-- > $ cd /ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude -- -- Browse the Prelude online to learn more by seeing what functions are -- available and reading their inline documentation: -- --- +-- -- -- __Exercise__: Try to use a new Prelude function that has not been covered -- previously in this tutorial @@ -2697,14 +2720,14 @@ -- convenience: -- -- > $ dhall --- > let Prelude = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/package.dhall +-- > let Prelude = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/package.dhall -- > -- > in λ(x : Text) --- > → Prelude.`List`.length Text (Prelude.`List`.replicate +10 Text x) +-- > → Prelude.`List`.length Text (Prelude.`List`.replicate 10 Text x) -- > -- > ∀(x : Text) → Natural -- > --- > λ(x : Text) → +10 +-- > λ(x : Text) → 10 -- -- The organization of the package mirrors the layout of the Prelude, meaning -- that every directory is stored as a record whose children are the fields of @@ -2712,7 +2735,7 @@ -- -- __Exercise__: Browse the Prelude by running: -- --- > $ dhall <<< 'https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/package.dhall' +-- > $ dhall <<< 'https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/package.dhall' -- $conclusion -- diff --git a/src/Dhall/TypeCheck.hs b/src/Dhall/TypeCheck.hs --- a/src/Dhall/TypeCheck.hs +++ b/src/Dhall/TypeCheck.hs @@ -629,13 +629,14 @@ Nothing -> Left (TypeError ctx e (MissingHandler diffY)) Just tX -> case tX of - Pi _ tY' t' -> do + Pi y tY' t' -> do if Dhall.Core.judgmentallyEqual tY tY' then return () else Left (TypeError ctx e (HandlerInputTypeMismatch kY tY tY')) - if Dhall.Core.judgmentallyEqual t t' + let t'' = Dhall.Core.shift (-1) (V y 0) t' + if Dhall.Core.judgmentallyEqual t t'' then return () - else Left (TypeError ctx e (InvalidHandlerOutputType kY t t')) + else Left (TypeError ctx e (InvalidHandlerOutputType kY t t'')) _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX)) mapM_ process (Data.HashMap.Strict.InsOrd.toList ktsY) return t @@ -661,20 +662,21 @@ (kX, t) <- case Data.HashMap.Strict.InsOrd.toList ktsX of [] -> Left (TypeError ctx e MissingMergeType) - (kX, Pi _ _ t):_ -> return (kX, t) + (kX, Pi y _ t):_ -> return (kX, Dhall.Core.shift (-1) (V y 0) t) (kX, tX ):_ -> Left (TypeError ctx e (HandlerNotAFunction kX tX)) let process (kY, tY) = do case Data.HashMap.Strict.InsOrd.lookup kY ktsX of Nothing -> Left (TypeError ctx e (MissingHandler diffY)) Just tX -> case tX of - Pi _ tY' t' -> do + Pi y tY' t' -> do if Dhall.Core.judgmentallyEqual tY tY' then return () else Left (TypeError ctx e (HandlerInputTypeMismatch kY tY tY')) - if Dhall.Core.judgmentallyEqual t t' + let t'' = Dhall.Core.shift (-1) (V y 0) t' + if Dhall.Core.judgmentallyEqual t t'' then return () - else Left (TypeError ctx e (HandlerOutputTypeMismatch kX t kY t')) + else Left (TypeError ctx e (HandlerOutputTypeMismatch kX t kY t'')) _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX)) mapM_ process (Data.HashMap.Strict.InsOrd.toList ktsY) return t @@ -915,9 +917,9 @@ \● You tried to define a recursive value, like this: \n\ \ \n\ \ \n\ - \ ┌─────────────────────┐ \n\ - \ │ let x = x + +1 in x │ \n\ - \ └─────────────────────┘ \n\ + \ ┌────────────────────┐ \n\ + \ │ let x = x + 1 in x │ \n\ + \ └────────────────────┘ \n\ \ ⇧ \n\ \ Recursive definitions are not allowed \n\ \ \n\ @@ -961,7 +963,7 @@ \ \n\ \ \n\ \ ┌────────────────┐ \n\ - \ │ Bool → Integer │ This is the type of a function that accepts an anonymous\n\ + \ │ Bool → Natural │ This is the type of a function that accepts an anonymous\n\ \ └────────────────┘ input term that has type ❰Bool❱ \n\ \ ⇧ \n\ \ This is the type of the input term \n\ @@ -1028,8 +1030,8 @@ \ \n\ \ \n\ \ ┌────────────────┐ \n\ - \ │ Bool → Integer │ This is the type of a function that returns an output \n\ - \ └────────────────┘ term that has type ❰Int❱ \n\ + \ │ Bool → Natural │ This is the type of a function that returns an output \n\ + \ └────────────────┘ term that has type ❰Natural❱ \n\ \ ⇧ \n\ \ This is the type of the output term \n\ \ \n\ @@ -1167,13 +1169,13 @@ \ \n\ \ \n\ \ ┌─────────────┐ \n\ - \ │ 1 : Integer │ ❰1❱ is not a function because ❰Integer❱ is not the type of \n\ + \ │ 1 : Natural │ ❰1❱ is not a function because ❰Natural❱ is not the type of \n\ \ └─────────────┘ a function \n\ \ \n\ \ \n\ - \ ┌────────────────────────┐ \n\ - \ │ Natural/even +2 : Bool │ ❰Natural/even +2❱ is not a function because \n\ - \ └────────────────────────┘ ❰Bool❱ is not the type of a function \n\ + \ ┌───────────────────────┐ \n\ + \ │ Natural/even 2 : Bool │ ❰Natural/even 2❱ is not a function because \n\ + \ └───────────────────────┘ ❰Bool❱ is not the type of a function \n\ \ \n\ \ \n\ \ ┌──────────────────┐ \n\ @@ -1183,7 +1185,7 @@ \ \n\ \Some common reasons why you might get this error: \n\ \ \n\ - \● You tried to add two ❰Integer❱s without a space around the ❰+❱, like this: \n\ + \● You tried to add two ❰Natural❱s without a space around the ❰+❱, like this: \n\ \ \n\ \ \n\ \ ┌─────┐ \n\ @@ -1202,21 +1204,17 @@ \ \n\ \ \n\ \ This is because the ❰+❱ symbol has two meanings: you use ❰+❱ to add two \n\ - \ numbers, but you also can prefix ❰Integer❱ literals with a ❰+❱ to turn them \n\ - \ into ❰Natural❱ literals (like ❰+2❱) \n\ + \ numbers, but you also can prefix ❰Natural❱ literals with a ❰+❱ to turn them \n\ + \ into ❰Integer❱ literals (like ❰+2❱) \n\ \ \n\ - \ To fix the code, you need to put spaces around the ❰+❱ and also prefix each \n\ - \ ❰2❱ with a ❰+❱, like this: \n\ + \ To fix the code, you need to put spaces around the ❰+❱, like this: \n\ \ \n\ \ \n\ - \ ┌─────────┐ \n\ - \ │ +2 + +2 │ \n\ - \ └─────────┘ \n\ + \ ┌───────┐ \n\ + \ │ 2 + 2 │ \n\ + \ └───────┘ \n\ \ \n\ \ \n\ - \ You can only add ❰Natural❱ numbers, which is why you must also change each \n\ - \ ❰2❱ to ❰+2❱ \n\ - \ \n\ \────────────────────────────────────────────────────────────────────────────────\n\ \ \n\ \You tried to use the following expression as a function: \n\ @@ -1280,9 +1278,9 @@ \ └────────────────────────┘ of argument that the anonymous function accepts \n\ \ \n\ \ \n\ - \ ┌─────────────────┐ \n\ - \ │ Natural/even +2 │ ❰+2❱ has type ❰Natural❱, which matches the type of \n\ - \ └─────────────────┘ argument that the ❰Natural/even❱ function accepts, \n\ + \ ┌────────────────┐ \n\ + \ │ Natural/even 2 │ ❰2❱ has type ❰Natural❱, which matches the type of \n\ + \ └────────────────┘ argument that the ❰Natural/even❱ function accepts, \n\ \ \n\ \ \n\ \ ┌────────────────────────┐ \n\ @@ -1316,7 +1314,7 @@ \ \n\ \ \n\ \ ┌────────┐ \n\ - \ │ List 1 │ ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an \n\ + \ │ List 1 │ ❰1❱ has type ❰Natural❱, but the ❰List❱ function expects an \n\ \ └────────┘ argument that has kind ❰Type❱ \n\ \ \n\ \ \n\ @@ -1330,17 +1328,17 @@ \ └───────────────────────┘ \n\ \ ⇧ \n\ \ ❰List/head❱ is missing the first argument, \n\ - \ which should be: ❰Integer❱ \n\ + \ which should be: ❰Natural❱ \n\ \ \n\ \ \n\ \● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱ \n\ \ \n\ \ \n\ - \ ┌────────────────┐ \n\ - \ │ Natural/even 2 │ \n\ - \ └────────────────┘ \n\ + \ ┌─────────────────┐ \n\ + \ │ Natural/even +2 │ \n\ + \ └─────────────────┘ \n\ \ ⇧ \n\ - \ This should be ❰+2❱ \n\ + \ This should be ❰2❱ \n\ \ \n\ \ \n\ \────────────────────────────────────────────────────────────────────────────────\n\ @@ -1388,13 +1386,13 @@ \ \n\ \ \n\ \ ┌─────────────┐ \n\ - \ │ 1 : Integer │ ❰1❱ is an expression that has type ❰Integer❱, so the type \n\ + \ │ 1 : Natural │ ❰1❱ is an expression that has type ❰Natural❱, so the type \n\ \ └─────────────┘ checker accepts the annotation \n\ \ \n\ \ \n\ - \ ┌────────────────────────┐ \n\ - \ │ Natural/even +2 : Bool │ ❰Natural/even +2❱ has type ❰Bool❱, so the type \n\ - \ └────────────────────────┘ checker accepts the annotation \n\ + \ ┌───────────────────────┐ \n\ + \ │ Natural/even 2 : Bool │ ❰Natural/even 2❱ has type ❰Bool❱, so the type \n\ + \ └───────────────────────┘ checker accepts the annotation \n\ \ \n\ \ \n\ \ ┌────────────────────┐ \n\ @@ -1587,7 +1585,7 @@ \ \n\ \ \n\ \ ┌────────────────────┐ \n\ - \ │ 1 : Integer : Type │ ❰1❱ is a term with a type (❰Integer❱) of kind ❰Type❱\n\ + \ │ 1 : Natural : Type │ ❰1❱ is a term with a type (❰Natural❱) of kind ❰Type❱\n\ \ └────────────────────┘ \n\ \ ⇧ \n\ \ term \n\ @@ -1674,7 +1672,7 @@ \ \n\ \ \n\ \ ┌──────────────────────────────────┐ \n\ - \ │ λ(b : Bool) → if b then 0 else 1 │ Both branches have type ❰Integer❱ \n\ + \ │ λ(b : Bool) → if b then 0 else 1 │ Both branches have type ❰Natural❱ \n\ \ └──────────────────────────────────┘ \n\ \ \n\ \ \n\ @@ -1688,7 +1686,7 @@ \However, the following expression is " <> _NOT <> " valid: \n\ \ \n\ \ \n\ - \ This branch has type ❰Integer❱ \n\ + \ This branch has type ❰Natural❱ \n\ \ ⇩ \n\ \ ┌────────────────────────┐ \n\ \ │ if True then 0 │ \n\ @@ -1734,14 +1732,15 @@ \ \n\ \ \n\ \ ┌──────────────────────────┐ \n\ - \ │ [1, 2, 3] : List Integer │ A ❰List❱ of three ❰Integer❱s \n\ + \ │ [1, 2, 3] : List Natural │ A ❰List❱ of three ❰Natural❱ numbers \n\ \ └──────────────────────────┘ \n\ \ ⇧ \n\ - \ The type of the ❰List❱'s elements, which are ❰Integer❱s \n\ + \ The type of the ❰List❱'s elements, which are ❰Natural❱ \n\ + \ numbers \n\ \ \n\ \ \n\ \ ┌───────────────────┐ \n\ - \ │ [] : List Integer │ An empty ❰List❱ \n\ + \ │ [] : List Natural │ An empty ❰List❱ \n\ \ └───────────────────┘ \n\ \ ⇧ \n\ \ You must specify the type when the ❰List❱ is empty \n\ @@ -1755,7 +1754,7 @@ \ │ ... : List 1 │ \n\ \ └──────────────┘ \n\ \ ⇧ \n\ - \ This is an ❰Integer❱ and not a ❰Type❱ \n\ + \ This is a ❰Natural❱ number and not a ❰Type❱ \n\ \ \n\ \ \n\ \ ┌─────────────────┐ \n\ @@ -1784,7 +1783,7 @@ \ \n\ \ \n\ \ ┌───────────┐ \n\ - \ │ [1, 2, 3] │ The compiler can infer that this list has type ❰List Integer❱\n\ + \ │ [1, 2, 3] │ The compiler can infer that this list has type ❰List Natural❱\n\ \ └───────────┘ \n\ \ \n\ \ \n\ @@ -1792,7 +1791,7 @@ \ \n\ \ \n\ \ ┌───────────────────┐ \n\ - \ │ [] : List Integer │ This type annotation is mandatory \n\ + \ │ [] : List Natural │ This type annotation is mandatory \n\ \ └───────────────────┘ \n\ \ \n\ \ \n\ @@ -1812,7 +1811,7 @@ \ \n\ \ \n\ \ ┌───────────┐ \n\ - \ │ [1, 2, 3] │ Every element in this ❰List❱ is an ❰Integer❱ \n\ + \ │ [1, 2, 3] │ Every element in this ❰List❱ is a ❰Natural❱ number \n\ \ └───────────┘ \n\ \ \n\ \ \n\ @@ -1851,7 +1850,7 @@ \ \n\ \ \n\ \ ┌──────────────────────────┐ \n\ - \ │ [1, 2, 3] : List Integer │ Every element in this ❰List❱ is an ❰Integer❱ \n\ + \ │ [1, 2, 3] : List Natural │ Every element in this ❰List❱ is an ❰Natural❱ \n\ \ └──────────────────────────┘ \n\ \ \n\ \ \n\ @@ -1859,7 +1858,7 @@ \ \n\ \ \n\ \ ┌──────────────────────────────┐ \n\ - \ │ [1, \"ABC\", 3] : List Integer │ The second element is not an ❰Integer❱ \n\ + \ │ [1, \"ABC\", 3] : List Natural │ The second element is not an ❰Natural❱ \n\ \ └──────────────────────────────┘ \n\ \ \n\ \ \n\ @@ -1885,14 +1884,15 @@ \ \n\ \ \n\ \ ┌────────────────────────┐ \n\ - \ │ [1] : Optional Integer │ An optional element that's present \n\ + \ │ [1] : Optional Natural │ An optional element that's present \n\ \ └────────────────────────┘ \n\ \ ⇧ \n\ - \ The type of the ❰Optional❱ element, which is an ❰Integer❱ \n\ + \ The type of the ❰Optional❱ element, which is an ❰Natural❱ \n\ + \ number \n\ \ \n\ \ \n\ \ ┌────────────────────────┐ \n\ - \ │ [] : Optional Integer │ An optional element that's absent \n\ + \ │ [] : Optional Natural │ An optional element that's absent \n\ \ └────────────────────────┘ \n\ \ ⇧ \n\ \ You still specify the type even when the element is absent \n\ @@ -1906,7 +1906,7 @@ \ │ ... : Optional 1 │ \n\ \ └──────────────────┘ \n\ \ ⇧ \n\ - \ This is an ❰Integer❱ and not a ❰Type❱ \n\ + \ This is a ❰Natural❱ number and not a ❰Type❱ \n\ \ \n\ \ \n\ \ ┌─────────────────────┐ \n\ @@ -1939,15 +1939,15 @@ \ \n\ \ \n\ \ ┌────────────────────────┐ \n\ - \ │ [1] : Optional Integer │ ❰1❱ is an ❰Integer❱, which matches the type \n\ - \ └────────────────────────┘ \n\ + \ │ [1] : Optional Natural │ ❰1❱ is a ❰Natural❱ number, which matches the \n\ + \ └────────────────────────┘ number \n\ \ \n\ \ \n\ \... but this is " <> _NOT <> " a valid ❰Optional❱ value: \n\ \ \n\ \ \n\ \ ┌────────────────────────────┐ \n\ - \ │ [\"ABC\"] : Optional Integer │ ❰\"ABC\"❱ is not an ❰Integer❱ \n\ + \ │ [\"ABC\"] : Optional Natural │ ❰\"ABC\"❱ is not a ❰Natural❱ number \n\ \ └────────────────────────────┘ \n\ \ \n\ \ \n\ @@ -1977,7 +1977,7 @@ \ \n\ \ \n\ \ ┌──────────────────────────────────────────────┐ \n\ - \ │ { foo : Integer, bar : Integer, baz : Text } │ Every field is annotated \n\ + \ │ { foo : Natural, bar : Integer, baz : Text } │ Every field is annotated \n\ \ └──────────────────────────────────────────────┘ with a ❰Type❱ \n\ \ \n\ \ \n\ @@ -1990,10 +1990,11 @@ \ \n\ \ \n\ \ ┌────────────────────────────┐ \n\ - \ │ { foo : Integer, bar : 1 } │ Invalid record type \n\ + \ │ { foo : Natural, bar : 1 } │ Invalid record type \n\ \ └────────────────────────────┘ \n\ \ ⇧ \n\ - \ ❰1❱ is an ❰Integer❱ and not a ❰Type❱ or ❰Kind❱ \n\ + \ ❰1❱ is a ❰Natural❱ number and not a ❰Type❱ or \n\ + \ ❰Kind❱ \n\ \ \n\ \ \n\ \You provided a record type with a field named: \n\ @@ -2019,7 +2020,7 @@ \ \n\ \ \n\ \ ┌──────────────────────────────────────────────┐ \n\ - \ │ { foo : Integer, bar : Integer, baz : Text } │ Every field is annotated \n\ + \ │ { foo : Natural, bar : Integer, baz : Text } │ Every field is annotated \n\ \ └──────────────────────────────────────────────┘ with a ❰Type❱ \n\ \ \n\ \ \n\ @@ -2034,7 +2035,7 @@ \ This is a ❰Type❱ annotation \n\ \ ⇩ \n\ \ ┌───────────────────────────────┐ \n\ - \ │ { foo : Integer, bar : Type } │ Invalid record type \n\ + \ │ { foo : Natural, bar : Type } │ Invalid record type \n\ \ └───────────────────────────────┘ \n\ \ ⇧ \n\ \ ... but this is a ❰Kind❱ annotation \n\ @@ -2086,7 +2087,7 @@ \ \n\ \ \n\ \ ┌───────────────────────────────┐ \n\ - \ │ { foo = Integer, bar = Text } │ Every field is a type \n\ + \ │ { foo = Natural, bar = Text } │ Every field is a type \n\ \ └───────────────────────────────┘ \n\ \ \n\ \ \n\ @@ -2311,7 +2312,7 @@ \For example, the following expression is " <> _NOT <> " valid: \n\ \ \n\ \ \n\ - \ These elements have type ❰Integer❱ \n\ + \ These elements have type ❰Natural❱ \n\ \ ⇩ \n\ \ ┌───────────────────────────┐ \n\ \ │ [1, 2, 3] # [True, False] │ Invalid: the element types don't match \n\ @@ -2594,7 +2595,7 @@ \ \n\ \ \n\ \ ┌─────────────────────────────────────────────────────────────────────┐ \n\ - \ │ let union = < Left = +2 | Right : Bool > │ \n\ + \ │ let union = < Left = 2 | Right : Bool > │ \n\ \ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\ \ │ in merge handlers union : Bool │ \n\ \ └─────────────────────────────────────────────────────────────────────┘ \n\ @@ -2649,7 +2650,7 @@ \ \n\ \ \n\ \ ┌─────────────────────────────────────────────────────────────────────┐ \n\ - \ │ let union = < Left = +2 | Right : Bool > │ \n\ + \ │ let union = < Left = 2 | Right : Bool > │ \n\ \ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\ \ │ in merge handlers union : Bool │ \n\ \ └─────────────────────────────────────────────────────────────────────┘ \n\ @@ -2689,7 +2690,7 @@ \ \n\ \ \n\ \ ┌─────────────────────────────────────────────────────────────────────┐ \n\ - \ │ let union = < Left = +2 | Right : Bool > │ \n\ + \ │ let union = < Left = 2 | Right : Bool > │ \n\ \ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\ \ │ in merge handlers union : Bool │ \n\ \ └─────────────────────────────────────────────────────────────────────┘ \n\ @@ -2702,11 +2703,11 @@ \ \n\ \ \n\ \ ┌───────────────────────────────────────┐ \n\ - \ │ let union = < Left = +2 > │ The ❰Right❱ alternative is missing\n\ - \ │ in let handlers = │ \n\ + \ │ let union = < Left = 2 > │ The ❰Right❱ alternative is \n\ + \ │ in let handlers = │ missing \n\ \ │ { Left = Natural/even │ \n\ - \ │ , Right = λ(x : Bool) → x │ Invalid: ❰Right❱ handler isn't used\n\ - \ │ } │ \n\ + \ │ , Right = λ(x : Bool) → x │ Invalid: ❰Right❱ handler isn't \n\ + \ │ } │ used \n\ \ │ in merge handlers union : Bool │ \n\ \ └───────────────────────────────────────┘ \n\ \ \n\ @@ -2729,7 +2730,7 @@ \ \n\ \ \n\ \ ┌─────────────────────────────────────────────────────────────────────┐ \n\ - \ │ let union = < Left = +2 | Right : Bool > │ \n\ + \ │ let union = < Left = 2 | Right : Bool > │ \n\ \ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\ \ │ in merge handlers union : Bool │ \n\ \ └─────────────────────────────────────────────────────────────────────┘ \n\ @@ -2745,7 +2746,7 @@ \ ⇩ \n\ \ ┌─────────────────────────────────────────────────┐ \n\ \ │ let handlers = { Left = Natural/even } │ \n\ - \ │ in let union = < Left = +2 | Right : Bool > │ \n\ + \ │ in let union = < Left = 2 | Right : Bool > │ \n\ \ │ in merge handlers union : Bool │ \n\ \ └─────────────────────────────────────────────────┘ \n\ \ \n\ @@ -2770,7 +2771,7 @@ \ \n\ \ \n\ \ ┌─────────────────────────────────────────────────────────────────────┐ \n\ - \ │ let union = < Left = +2 | Right : Bool > │ \n\ + \ │ let union = < Left = 2 | Right : Bool > │ \n\ \ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\ \ │ in merge handlers union │ \n\ \ └─────────────────────────────────────────────────────────────────────┘ \n\ @@ -2802,7 +2803,7 @@ \ \n\ \ \n\ \ ┌─────────────────────────────────────────────────────────────────────┐ \n\ - \ │ let union = < Left = +2 | Right : Bool > │ \n\ + \ │ let union = < Left = 2 | Right : Bool > │ \n\ \ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\ \ │ in merge handlers union : Bool │ \n\ \ └─────────────────────────────────────────────────────────────────────┘ \n\ @@ -2830,7 +2831,7 @@ \ ⇩ \n\ \ ┌──────────────────────────────────────────────────────────────────────┐ \n\ \ │ let handlers = { Left = Natural/even | Right = λ(x : Text) → x } │ \n\ - \ │ in let union = < Left = +2 | Right : Bool > │ \n\ + \ │ in let union = < Left = 2 | Right : Bool > │ \n\ \ │ in merge handlers union : Bool │ \n\ \ └──────────────────────────────────────────────────────────────────────┘ \n\ \ \n\ @@ -2864,7 +2865,7 @@ \ \n\ \ \n\ \ ┌─────────────────────────────────────────────────────────────────────┐ \n\ - \ │ let union = < Left = +2 | Right : Bool > │ \n\ + \ │ let union = < Left = 2 | Right : Bool > │ \n\ \ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\ \ │ in merge handlers union : Bool │ \n\ \ └─────────────────────────────────────────────────────────────────────┘ \n\ @@ -2891,7 +2892,7 @@ \ \n\ \ \n\ \ ┌──────────────────────────────────────────────────────────────────────┐ \n\ - \ │ let union = < Left = +2 | Right : Bool > │ \n\ + \ │ let union = < Left = 2 | Right : Bool > │ \n\ \ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\ \ │ in merge handlers union : Text │ \n\ \ └──────────────────────────────────────────────────────────────────────┘ \n\ @@ -2928,7 +2929,7 @@ \ \n\ \ \n\ \ ┌─────────────────────────────────────────────────────────────────────┐ \n\ - \ │ let union = < Left = +2 | Right : Bool > │ \n\ + \ │ let union = < Left = 2 | Right : Bool > │ \n\ \ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\ \ │ in merge handlers union │ \n\ \ └─────────────────────────────────────────────────────────────────────┘ \n\ @@ -2948,7 +2949,7 @@ \ \n\ \ \n\ \ ┌─────────────────────────────────────────────────┐ \n\ - \ │ let union = < Left = +2 | Right : Bool > │ \n\ + \ │ let union = < Left = 2 | Right : Bool > │ \n\ \ │ in let handlers = │ \n\ \ │ { Left = λ(x : Natural) → x │ This outputs ❰Natural❱ \n\ \ │ , Right = λ(x : Bool ) → x │ This outputs ❰Bool❱ \n\ @@ -2982,7 +2983,7 @@ \ \n\ \ \n\ \ ┌─────────────────────────────────────────────────────────────────────┐ \n\ - \ │ let union = < Left = +2 | Right : Bool > │ \n\ + \ │ let union = < Left = 2 | Right : Bool > │ \n\ \ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\ \ │ in merge handlers union : Bool │ \n\ \ └─────────────────────────────────────────────────────────────────────┘ \n\ @@ -3197,9 +3198,9 @@ \ └────────────────────────────┘ \n\ \ \n\ \ \n\ - \ ┌───────────────────────────────────────────────────────────────────┐ \n\ - \ │ λ(age : Natural) → \"Age: ${Integer/show (Natural/toInteger age)}\" │ \n\ - \ └───────────────────────────────────────────────────────────────────┘ \n\ + \ ┌───────────────────────────────────────────────┐ \n\ + \ │ λ(age : Natural) → \"Age: ${Natural/show age}\" │ \n\ + \ └───────────────────────────────────────────────┘ \n\ \ \n\ \ \n\ \Some common reasons why you might get this error: \n\ @@ -3341,9 +3342,9 @@ \Similarly, this is " <> _NOT <> " legal code: \n\ \ \n\ \ \n\ - \ ┌────────────────────────────────────────────────────┐ \n\ - \ │ λ(Vector : Natural → Type → Type) → Vector +0 Text │ \n\ - \ └────────────────────────────────────────────────────┘ \n\ + \ ┌───────────────────────────────────────────────────┐ \n\ + \ │ λ(Vector : Natural → Type → Type) → Vector 0 Text │ \n\ + \ └───────────────────────────────────────────────────┘ \n\ \ ⇧ \n\ \ Invalid dependent type \n\ \ \n\ @@ -3401,9 +3402,9 @@ \For example, this is a valid use of ❰" <> txt2 <> "❱: \n\ \ \n\ \ \n\ - \ ┌─────────┐ \n\ - \ │ +3 " <> txt2 <> " +5 │ \n\ - \ └─────────┘ \n\ + \ ┌───────┐ \n\ + \ │ 3 " <> txt2 <> " 5 │ \n\ + \ └───────┘ \n\ \ \n\ \ \n\ \Some common reasons why you might get this error: \n\ @@ -3422,18 +3423,18 @@ \● You might have mistakenly used an ❰Integer❱ literal, which is " <> _NOT <> " allowed:\n\ \ \n\ \ \n\ - \ ┌───────┐ \n\ - \ │ 2 " <> txt2 <> " 2 │ Not valid \n\ - \ └───────┘ \n\ + \ ┌─────────┐ \n\ + \ │ +2 " <> txt2 <> " +2 │ Not valid \n\ + \ └─────────┘ \n\ \ \n\ \ \n\ - \ You need to prefix each literal with a ❰+❱ to transform them into ❰Natural❱ \n\ - \ literals, like this: \n\ + \ You need to remove the leading ❰+❱ to transform them into ❰Natural❱ literals, \n\ + \ like this: \n\ \ \n\ \ \n\ - \ ┌─────────┐ \n\ - \ │ +2 " <> txt2 <> " +2 │ Valid \n\ - \ └─────────┘ \n\ + \ ┌───────┐ \n\ + \ │ 2 " <> txt2 <> " 2 │ Valid \n\ + \ └───────┘ \n\ \ \n\ \ \n\ \────────────────────────────────────────────────────────────────────────────────\n\ diff --git a/tests/Normalization.hs b/tests/Normalization.hs --- a/tests/Normalization.hs +++ b/tests/Normalization.hs @@ -203,8 +203,8 @@ valCtx e = case e of (App (App (Var (V "min" 0)) (NaturalLit x)) (NaturalLit y)) -> Just (NaturalLit (min x y)) _ -> Nothing - e <- codeWith tyCtx "min (min +11 +12) +8 + +1" - assertNormalizesToWith valCtx e "+9" + e <- codeWith tyCtx "min (min 11 12) 8 + 1" + assertNormalizesToWith valCtx e "9" nestedReduction :: TestTree nestedReduction = testCase "doubleReduction" $ do @@ -219,8 +219,8 @@ (App (Var (V "fiveorless" 0)) (NaturalLit x)) -> Just (App (App (Var (V "min" 0)) (NaturalLit x)) (NaturalPlus (NaturalLit 3) (NaturalLit 2))) _ -> Nothing - e <- codeWith tyCtx "wurble +6" - assertNormalizesToWith valCtx e "+5" + e <- codeWith tyCtx "wurble 6" + assertNormalizesToWith valCtx e "5" should :: Text -> Text -> TestTree should name basename = diff --git a/tests/Tutorial.hs b/tests/Tutorial.hs --- a/tests/Tutorial.hs +++ b/tests/Tutorial.hs @@ -44,7 +44,7 @@ e <- Util.code " let name = \"John Doe\" \n\ \in let age = 21 \n\ - \in \"My name is ${name} and my age is ${Integer/show age}\"\n" + \in \"My name is ${name} and my age is ${Natural/show age}\"\n" Util.assertNormalizesTo e "\"My name is John Doe and my age is 21\"" ) _Interpolation_1 :: TestTree diff --git a/tests/TypeCheck.hs b/tests/TypeCheck.hs --- a/tests/TypeCheck.hs +++ b/tests/TypeCheck.hs @@ -40,6 +40,9 @@ , should "allow anonymous functions in types to be judgmentally equal" "anonymousFunctionsInTypes" + , should + "correctly handle α-equivalent merge alternatives" + "mergeEquivalence" ] should :: Text -> Text -> TestTree diff --git a/tests/normalization/examples/Bool/fold/0A.dhall b/tests/normalization/examples/Bool/fold/0A.dhall --- a/tests/normalization/examples/Bool/fold/0A.dhall +++ b/tests/normalization/examples/Bool/fold/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Bool/fold True Integer 0 1 +../../../../../Prelude/Bool/fold True Natural 0 1 diff --git a/tests/normalization/examples/Bool/fold/1A.dhall b/tests/normalization/examples/Bool/fold/1A.dhall --- a/tests/normalization/examples/Bool/fold/1A.dhall +++ b/tests/normalization/examples/Bool/fold/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Bool/fold False Integer 0 1 +../../../../../Prelude/Bool/fold False Natural 0 1 diff --git a/tests/normalization/examples/Integer/show/1A.dhall b/tests/normalization/examples/Integer/show/1A.dhall --- a/tests/normalization/examples/Integer/show/1A.dhall +++ b/tests/normalization/examples/Integer/show/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Integer/show 0 +../../../../../Prelude/Integer/show +0 diff --git a/tests/normalization/examples/Integer/show/1B.dhall b/tests/normalization/examples/Integer/show/1B.dhall --- a/tests/normalization/examples/Integer/show/1B.dhall +++ b/tests/normalization/examples/Integer/show/1B.dhall @@ -1,1 +1,1 @@ -"0" +"+0" diff --git a/tests/normalization/examples/List/all/0A.dhall b/tests/normalization/examples/List/all/0A.dhall --- a/tests/normalization/examples/List/all/0A.dhall +++ b/tests/normalization/examples/List/all/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/List/all Natural Natural/even [ +2, +3, +5 ] +../../../../../Prelude/List/all Natural Natural/even [ 2, 3, 5 ] diff --git a/tests/normalization/examples/List/any/0A.dhall b/tests/normalization/examples/List/any/0A.dhall --- a/tests/normalization/examples/List/any/0A.dhall +++ b/tests/normalization/examples/List/any/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/List/any Natural Natural/even [ +2, +3, +5 ] +../../../../../Prelude/List/any Natural Natural/even [ 2, 3, 5 ] diff --git a/tests/normalization/examples/List/concat/0A.dhall b/tests/normalization/examples/List/concat/0A.dhall --- a/tests/normalization/examples/List/concat/0A.dhall +++ b/tests/normalization/examples/List/concat/0A.dhall @@ -1,4 +1,4 @@ -../../../../../Prelude/List/concat Integer +../../../../../Prelude/List/concat Natural [ [ 0, 1, 2 ] , [ 3, 4 ] , [ 5, 6, 7, 8 ] diff --git a/tests/normalization/examples/List/concat/1A.dhall b/tests/normalization/examples/List/concat/1A.dhall --- a/tests/normalization/examples/List/concat/1A.dhall +++ b/tests/normalization/examples/List/concat/1A.dhall @@ -1,5 +1,5 @@ -../../../../../Prelude/List/concat Integer -[ [] : List Integer -, [] : List Integer -, [] : List Integer +../../../../../Prelude/List/concat Natural +[ [] : List Natural +, [] : List Natural +, [] : List Natural ] diff --git a/tests/normalization/examples/List/concat/1B.dhall b/tests/normalization/examples/List/concat/1B.dhall --- a/tests/normalization/examples/List/concat/1B.dhall +++ b/tests/normalization/examples/List/concat/1B.dhall @@ -1,1 +1,1 @@ -[] : List Integer +[] : List Natural diff --git a/tests/normalization/examples/List/concatMap/0A.dhall b/tests/normalization/examples/List/concatMap/0A.dhall --- a/tests/normalization/examples/List/concatMap/0A.dhall +++ b/tests/normalization/examples/List/concatMap/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/List/concatMap Natural Natural (λ(n : Natural) → [ n, n ]) [ +2, +3, +5 ] +../../../../../Prelude/List/concatMap Natural Natural (λ(n : Natural) → [ n, n ]) [ 2, 3, 5 ] diff --git a/tests/normalization/examples/List/concatMap/0B.dhall b/tests/normalization/examples/List/concatMap/0B.dhall --- a/tests/normalization/examples/List/concatMap/0B.dhall +++ b/tests/normalization/examples/List/concatMap/0B.dhall @@ -1,1 +1,1 @@ -[ +2, +2, +3, +3, +5, +5 ] +[ 2, 2, 3, 3, 5, 5 ] diff --git a/tests/normalization/examples/List/filter/0A.dhall b/tests/normalization/examples/List/filter/0A.dhall --- a/tests/normalization/examples/List/filter/0A.dhall +++ b/tests/normalization/examples/List/filter/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/List/filter Natural Natural/even [ +2, +3, +5 ] +../../../../../Prelude/List/filter Natural Natural/even [ 2, 3, 5 ] diff --git a/tests/normalization/examples/List/filter/0B.dhall b/tests/normalization/examples/List/filter/0B.dhall --- a/tests/normalization/examples/List/filter/0B.dhall +++ b/tests/normalization/examples/List/filter/0B.dhall @@ -1,1 +1,1 @@ -[ +2 ] +[ 2 ] diff --git a/tests/normalization/examples/List/filter/1A.dhall b/tests/normalization/examples/List/filter/1A.dhall --- a/tests/normalization/examples/List/filter/1A.dhall +++ b/tests/normalization/examples/List/filter/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/List/filter Natural Natural/odd [ +2, +3, +5 ] +../../../../../Prelude/List/filter Natural Natural/odd [ 2, 3, 5 ] diff --git a/tests/normalization/examples/List/filter/1B.dhall b/tests/normalization/examples/List/filter/1B.dhall --- a/tests/normalization/examples/List/filter/1B.dhall +++ b/tests/normalization/examples/List/filter/1B.dhall @@ -1,1 +1,1 @@ -[ +3, +5 ] +[ 3, 5 ] diff --git a/tests/normalization/examples/List/fold/0A.dhall b/tests/normalization/examples/List/fold/0A.dhall --- a/tests/normalization/examples/List/fold/0A.dhall +++ b/tests/normalization/examples/List/fold/0A.dhall @@ -1,6 +1,6 @@ ../../../../../Prelude/List/fold Natural -[ +2, +3, +5 ] +[ 2, 3, 5 ] Natural (λ(x : Natural) → λ(y : Natural) → x + y) -+0 +0 diff --git a/tests/normalization/examples/List/fold/0B.dhall b/tests/normalization/examples/List/fold/0B.dhall --- a/tests/normalization/examples/List/fold/0B.dhall +++ b/tests/normalization/examples/List/fold/0B.dhall @@ -1,1 +1,1 @@ -+10 +10 diff --git a/tests/normalization/examples/List/fold/1A.dhall b/tests/normalization/examples/List/fold/1A.dhall --- a/tests/normalization/examples/List/fold/1A.dhall +++ b/tests/normalization/examples/List/fold/1A.dhall @@ -1,7 +1,7 @@ λ(nil : Natural) → ../../../../../Prelude/List/fold Natural - [ +2, +3, +5 ] + [ 2, 3, 5 ] Natural (λ(x : Natural) → λ(y : Natural) → x + y) nil diff --git a/tests/normalization/examples/List/fold/1B.dhall b/tests/normalization/examples/List/fold/1B.dhall --- a/tests/normalization/examples/List/fold/1B.dhall +++ b/tests/normalization/examples/List/fold/1B.dhall @@ -1,1 +1,1 @@ -λ(nil : Natural) → +2 + +3 + +5 + nil +λ(nil : Natural) → 2 + 3 + 5 + nil diff --git a/tests/normalization/examples/List/fold/2A.dhall b/tests/normalization/examples/List/fold/2A.dhall --- a/tests/normalization/examples/List/fold/2A.dhall +++ b/tests/normalization/examples/List/fold/2A.dhall @@ -1,4 +1,4 @@ λ(list : Type) → λ(cons : Natural → list → list) → λ(nil : list) -→ ../../../../../Prelude/List/fold Natural [ +2, +3, +5 ] list cons nil +→ ../../../../../Prelude/List/fold Natural [ 2, 3, 5 ] list cons nil diff --git a/tests/normalization/examples/List/fold/2B.dhall b/tests/normalization/examples/List/fold/2B.dhall --- a/tests/normalization/examples/List/fold/2B.dhall +++ b/tests/normalization/examples/List/fold/2B.dhall @@ -1,4 +1,4 @@ λ(list : Type) → λ(cons : Natural → list → list) → λ(nil : list) -→ cons +2 (cons +3 (cons +5 nil)) +→ cons 2 (cons 3 (cons 5 nil)) diff --git a/tests/normalization/examples/List/generate/0A.dhall b/tests/normalization/examples/List/generate/0A.dhall --- a/tests/normalization/examples/List/generate/0A.dhall +++ b/tests/normalization/examples/List/generate/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/List/generate +5 Bool Natural/even +../../../../../Prelude/List/generate 5 Bool Natural/even diff --git a/tests/normalization/examples/List/generate/1A.dhall b/tests/normalization/examples/List/generate/1A.dhall --- a/tests/normalization/examples/List/generate/1A.dhall +++ b/tests/normalization/examples/List/generate/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/List/generate +0 Bool Natural/even +../../../../../Prelude/List/generate 0 Bool Natural/even diff --git a/tests/normalization/examples/List/head/0A.dhall b/tests/normalization/examples/List/head/0A.dhall --- a/tests/normalization/examples/List/head/0A.dhall +++ b/tests/normalization/examples/List/head/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/List/head Integer [ 0, 1, 2 ] +../../../../../Prelude/List/head Natural [ 0, 1, 2 ] diff --git a/tests/normalization/examples/List/head/0B.dhall b/tests/normalization/examples/List/head/0B.dhall --- a/tests/normalization/examples/List/head/0B.dhall +++ b/tests/normalization/examples/List/head/0B.dhall @@ -1,1 +1,1 @@ -[ 0 ] : Optional Integer +[ 0 ] : Optional Natural diff --git a/tests/normalization/examples/List/head/1A.dhall b/tests/normalization/examples/List/head/1A.dhall --- a/tests/normalization/examples/List/head/1A.dhall +++ b/tests/normalization/examples/List/head/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/List/head Integer ([] : List Integer) +../../../../../Prelude/List/head Natural ([] : List Natural) diff --git a/tests/normalization/examples/List/head/1B.dhall b/tests/normalization/examples/List/head/1B.dhall --- a/tests/normalization/examples/List/head/1B.dhall +++ b/tests/normalization/examples/List/head/1B.dhall @@ -1,1 +1,1 @@ -[] : Optional Integer +[] : Optional Natural diff --git a/tests/normalization/examples/List/iterate/0A.dhall b/tests/normalization/examples/List/iterate/0A.dhall --- a/tests/normalization/examples/List/iterate/0A.dhall +++ b/tests/normalization/examples/List/iterate/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/List/iterate +10 Natural (λ(x : Natural) → x * +2) +1 +../../../../../Prelude/List/iterate 10 Natural (λ(x : Natural) → x * 2) 1 diff --git a/tests/normalization/examples/List/iterate/0B.dhall b/tests/normalization/examples/List/iterate/0B.dhall --- a/tests/normalization/examples/List/iterate/0B.dhall +++ b/tests/normalization/examples/List/iterate/0B.dhall @@ -1,1 +1,1 @@ -[ +1, +2, +4, +8, +16, +32, +64, +128, +256, +512 ] +[ 1, 2, 4, 8, 16, 32, 64, 128, 256, 512 ] diff --git a/tests/normalization/examples/List/iterate/1A.dhall b/tests/normalization/examples/List/iterate/1A.dhall --- a/tests/normalization/examples/List/iterate/1A.dhall +++ b/tests/normalization/examples/List/iterate/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/List/iterate +0 Natural (λ(x : Natural) → x * +2) +1 +../../../../../Prelude/List/iterate 0 Natural (λ(x : Natural) → x * 2) 1 diff --git a/tests/normalization/examples/List/last/0A.dhall b/tests/normalization/examples/List/last/0A.dhall --- a/tests/normalization/examples/List/last/0A.dhall +++ b/tests/normalization/examples/List/last/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/List/last Integer [ 0, 1, 2 ] +../../../../../Prelude/List/last Natural [ 0, 1, 2 ] diff --git a/tests/normalization/examples/List/last/0B.dhall b/tests/normalization/examples/List/last/0B.dhall --- a/tests/normalization/examples/List/last/0B.dhall +++ b/tests/normalization/examples/List/last/0B.dhall @@ -1,1 +1,1 @@ -[ 2 ] : Optional Integer +[ 2 ] : Optional Natural diff --git a/tests/normalization/examples/List/last/1A.dhall b/tests/normalization/examples/List/last/1A.dhall --- a/tests/normalization/examples/List/last/1A.dhall +++ b/tests/normalization/examples/List/last/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/List/last Integer ([] : List Integer) +../../../../../Prelude/List/last Natural ([] : List Natural) diff --git a/tests/normalization/examples/List/last/1B.dhall b/tests/normalization/examples/List/last/1B.dhall --- a/tests/normalization/examples/List/last/1B.dhall +++ b/tests/normalization/examples/List/last/1B.dhall @@ -1,1 +1,1 @@ -[] : Optional Integer +[] : Optional Natural diff --git a/tests/normalization/examples/List/length/0A.dhall b/tests/normalization/examples/List/length/0A.dhall --- a/tests/normalization/examples/List/length/0A.dhall +++ b/tests/normalization/examples/List/length/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/List/length Integer [ 0, 1, 2 ] +../../../../../Prelude/List/length Natural [ 0, 1, 2 ] diff --git a/tests/normalization/examples/List/length/0B.dhall b/tests/normalization/examples/List/length/0B.dhall --- a/tests/normalization/examples/List/length/0B.dhall +++ b/tests/normalization/examples/List/length/0B.dhall @@ -1,1 +1,1 @@ -+3 +3 diff --git a/tests/normalization/examples/List/length/1A.dhall b/tests/normalization/examples/List/length/1A.dhall --- a/tests/normalization/examples/List/length/1A.dhall +++ b/tests/normalization/examples/List/length/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/List/length Integer ([] : List Integer) +../../../../../Prelude/List/length Natural ([] : List Natural) diff --git a/tests/normalization/examples/List/length/1B.dhall b/tests/normalization/examples/List/length/1B.dhall --- a/tests/normalization/examples/List/length/1B.dhall +++ b/tests/normalization/examples/List/length/1B.dhall @@ -1,1 +1,1 @@ -+0 +0 diff --git a/tests/normalization/examples/List/map/0A.dhall b/tests/normalization/examples/List/map/0A.dhall --- a/tests/normalization/examples/List/map/0A.dhall +++ b/tests/normalization/examples/List/map/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/List/map Natural Bool Natural/even [ +2, +3, +5 ] +../../../../../Prelude/List/map Natural Bool Natural/even [ 2, 3, 5 ] diff --git a/tests/normalization/examples/List/null/0A.dhall b/tests/normalization/examples/List/null/0A.dhall --- a/tests/normalization/examples/List/null/0A.dhall +++ b/tests/normalization/examples/List/null/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/List/null Integer [ 0, 1, 2 ] +../../../../../Prelude/List/null Natural [ 0, 1, 2 ] diff --git a/tests/normalization/examples/List/null/1A.dhall b/tests/normalization/examples/List/null/1A.dhall --- a/tests/normalization/examples/List/null/1A.dhall +++ b/tests/normalization/examples/List/null/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/List/null Integer ([] : List Integer) +../../../../../Prelude/List/null Natural ([] : List Natural) diff --git a/tests/normalization/examples/List/replicate/0A.dhall b/tests/normalization/examples/List/replicate/0A.dhall --- a/tests/normalization/examples/List/replicate/0A.dhall +++ b/tests/normalization/examples/List/replicate/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/List/replicate +9 Integer 1 +../../../../../Prelude/List/replicate 9 Natural 1 diff --git a/tests/normalization/examples/List/replicate/1A.dhall b/tests/normalization/examples/List/replicate/1A.dhall --- a/tests/normalization/examples/List/replicate/1A.dhall +++ b/tests/normalization/examples/List/replicate/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/List/replicate +0 Integer 1 +../../../../../Prelude/List/replicate 0 Natural 1 diff --git a/tests/normalization/examples/List/replicate/1B.dhall b/tests/normalization/examples/List/replicate/1B.dhall --- a/tests/normalization/examples/List/replicate/1B.dhall +++ b/tests/normalization/examples/List/replicate/1B.dhall @@ -1,1 +1,1 @@ -[] : List Integer +[] : List Natural diff --git a/tests/normalization/examples/List/reverse/0A.dhall b/tests/normalization/examples/List/reverse/0A.dhall --- a/tests/normalization/examples/List/reverse/0A.dhall +++ b/tests/normalization/examples/List/reverse/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/List/reverse Integer [ 0, 1, 2 ] +../../../../../Prelude/List/reverse Natural [ 0, 1, 2 ] diff --git a/tests/normalization/examples/List/reverse/1A.dhall b/tests/normalization/examples/List/reverse/1A.dhall --- a/tests/normalization/examples/List/reverse/1A.dhall +++ b/tests/normalization/examples/List/reverse/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/List/reverse Integer ([] : List Integer) +../../../../../Prelude/List/reverse Natural ([] : List Natural) diff --git a/tests/normalization/examples/List/reverse/1B.dhall b/tests/normalization/examples/List/reverse/1B.dhall --- a/tests/normalization/examples/List/reverse/1B.dhall +++ b/tests/normalization/examples/List/reverse/1B.dhall @@ -1,1 +1,1 @@ -[] : List Integer +[] : List Natural diff --git a/tests/normalization/examples/List/shifted/0A.dhall b/tests/normalization/examples/List/shifted/0A.dhall --- a/tests/normalization/examples/List/shifted/0A.dhall +++ b/tests/normalization/examples/List/shifted/0A.dhall @@ -1,15 +1,15 @@ ../../../../../Prelude/List/shifted Bool -[ [ { index = +0, value = True } - , { index = +1, value = True } - , { index = +2, value = False } +[ [ { index = 0, value = True } + , { index = 1, value = True } + , { index = 2, value = False } ] -, [ { index = +0, value = False } - , { index = +1, value = False } +, [ { index = 0, value = False } + , { index = 1, value = False } ] -, [ { index = +0, value = True } - , { index = +1, value = True } - , { index = +2, value = True } - , { index = +3, value = True } +, [ { index = 0, value = True } + , { index = 1, value = True } + , { index = 2, value = True } + , { index = 3, value = True } ] ] diff --git a/tests/normalization/examples/List/shifted/0B.dhall b/tests/normalization/examples/List/shifted/0B.dhall --- a/tests/normalization/examples/List/shifted/0B.dhall +++ b/tests/normalization/examples/List/shifted/0B.dhall @@ -1,10 +1,10 @@ -[ { index = +0, value = True } -, { index = +1, value = True } -, { index = +2, value = False } -, { index = +3, value = False } -, { index = +4, value = False } -, { index = +5, value = True } -, { index = +6, value = True } -, { index = +7, value = True } -, { index = +8, value = True } +[ { index = 0, value = True } +, { index = 1, value = True } +, { index = 2, value = False } +, { index = 3, value = False } +, { index = 4, value = False } +, { index = 5, value = True } +, { index = 6, value = True } +, { index = 7, value = True } +, { index = 8, value = True } ] diff --git a/tests/normalization/examples/Natural/build/0B.dhall b/tests/normalization/examples/Natural/build/0B.dhall --- a/tests/normalization/examples/Natural/build/0B.dhall +++ b/tests/normalization/examples/Natural/build/0B.dhall @@ -1,1 +1,1 @@ -+3 +3 diff --git a/tests/normalization/examples/Natural/build/1B.dhall b/tests/normalization/examples/Natural/build/1B.dhall --- a/tests/normalization/examples/Natural/build/1B.dhall +++ b/tests/normalization/examples/Natural/build/1B.dhall @@ -1,1 +1,1 @@ -+0 +0 diff --git a/tests/normalization/examples/Natural/enumerate/0A.dhall b/tests/normalization/examples/Natural/enumerate/0A.dhall --- a/tests/normalization/examples/Natural/enumerate/0A.dhall +++ b/tests/normalization/examples/Natural/enumerate/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Natural/enumerate +10 +../../../../../Prelude/Natural/enumerate 10 diff --git a/tests/normalization/examples/Natural/enumerate/0B.dhall b/tests/normalization/examples/Natural/enumerate/0B.dhall --- a/tests/normalization/examples/Natural/enumerate/0B.dhall +++ b/tests/normalization/examples/Natural/enumerate/0B.dhall @@ -1,1 +1,1 @@ -[ +0, +1, +2, +3, +4, +5, +6, +7, +8, +9 ] +[ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9 ] diff --git a/tests/normalization/examples/Natural/enumerate/1A.dhall b/tests/normalization/examples/Natural/enumerate/1A.dhall --- a/tests/normalization/examples/Natural/enumerate/1A.dhall +++ b/tests/normalization/examples/Natural/enumerate/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Natural/enumerate +0 +../../../../../Prelude/Natural/enumerate 0 diff --git a/tests/normalization/examples/Natural/even/0A.dhall b/tests/normalization/examples/Natural/even/0A.dhall --- a/tests/normalization/examples/Natural/even/0A.dhall +++ b/tests/normalization/examples/Natural/even/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Natural/even +3 +../../../../../Prelude/Natural/even 3 diff --git a/tests/normalization/examples/Natural/even/1A.dhall b/tests/normalization/examples/Natural/even/1A.dhall --- a/tests/normalization/examples/Natural/even/1A.dhall +++ b/tests/normalization/examples/Natural/even/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Natural/even +0 +../../../../../Prelude/Natural/even 0 diff --git a/tests/normalization/examples/Natural/fold/0A.dhall b/tests/normalization/examples/Natural/fold/0A.dhall --- a/tests/normalization/examples/Natural/fold/0A.dhall +++ b/tests/normalization/examples/Natural/fold/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Natural/fold +3 Natural (λ(x : Natural) → +5 * x) +1 +../../../../../Prelude/Natural/fold 3 Natural (λ(x : Natural) → 5 * x) 1 diff --git a/tests/normalization/examples/Natural/fold/0B.dhall b/tests/normalization/examples/Natural/fold/0B.dhall --- a/tests/normalization/examples/Natural/fold/0B.dhall +++ b/tests/normalization/examples/Natural/fold/0B.dhall @@ -1,1 +1,1 @@ -+125 +125 diff --git a/tests/normalization/examples/Natural/fold/1A.dhall b/tests/normalization/examples/Natural/fold/1A.dhall --- a/tests/normalization/examples/Natural/fold/1A.dhall +++ b/tests/normalization/examples/Natural/fold/1A.dhall @@ -1,1 +1,1 @@ -λ(zero : Natural) → ../../../../../Prelude/Natural/fold +3 Natural (λ(x : Natural) → +5 * x) zero +λ(zero : Natural) → ../../../../../Prelude/Natural/fold 3 Natural (λ(x : Natural) → 5 * x) zero diff --git a/tests/normalization/examples/Natural/fold/1B.dhall b/tests/normalization/examples/Natural/fold/1B.dhall --- a/tests/normalization/examples/Natural/fold/1B.dhall +++ b/tests/normalization/examples/Natural/fold/1B.dhall @@ -1,1 +1,1 @@ -λ(zero : Natural) → +5 * +5 * +5 * zero +λ(zero : Natural) → 5 * 5 * 5 * zero diff --git a/tests/normalization/examples/Natural/fold/2A.dhall b/tests/normalization/examples/Natural/fold/2A.dhall --- a/tests/normalization/examples/Natural/fold/2A.dhall +++ b/tests/normalization/examples/Natural/fold/2A.dhall @@ -1,4 +1,4 @@ λ(natural : Type) → λ(succ : natural → natural) → λ(zero : natural) -→ ../../../../../Prelude/Natural/fold +3 natural succ zero +→ ../../../../../Prelude/Natural/fold 3 natural succ zero diff --git a/tests/normalization/examples/Natural/isZero/0A.dhall b/tests/normalization/examples/Natural/isZero/0A.dhall --- a/tests/normalization/examples/Natural/isZero/0A.dhall +++ b/tests/normalization/examples/Natural/isZero/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Natural/isZero +2 +../../../../../Prelude/Natural/isZero 2 diff --git a/tests/normalization/examples/Natural/isZero/1A.dhall b/tests/normalization/examples/Natural/isZero/1A.dhall --- a/tests/normalization/examples/Natural/isZero/1A.dhall +++ b/tests/normalization/examples/Natural/isZero/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Natural/isZero +0 +../../../../../Prelude/Natural/isZero 0 diff --git a/tests/normalization/examples/Natural/odd/0A.dhall b/tests/normalization/examples/Natural/odd/0A.dhall --- a/tests/normalization/examples/Natural/odd/0A.dhall +++ b/tests/normalization/examples/Natural/odd/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Natural/odd +3 +../../../../../Prelude/Natural/odd 3 diff --git a/tests/normalization/examples/Natural/odd/1A.dhall b/tests/normalization/examples/Natural/odd/1A.dhall --- a/tests/normalization/examples/Natural/odd/1A.dhall +++ b/tests/normalization/examples/Natural/odd/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Natural/odd +0 +../../../../../Prelude/Natural/odd 0 diff --git a/tests/normalization/examples/Natural/product/0A.dhall b/tests/normalization/examples/Natural/product/0A.dhall --- a/tests/normalization/examples/Natural/product/0A.dhall +++ b/tests/normalization/examples/Natural/product/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Natural/product [ +2, +3, +5 ] +../../../../../Prelude/Natural/product [ 2, 3, 5 ] diff --git a/tests/normalization/examples/Natural/product/0B.dhall b/tests/normalization/examples/Natural/product/0B.dhall --- a/tests/normalization/examples/Natural/product/0B.dhall +++ b/tests/normalization/examples/Natural/product/0B.dhall @@ -1,1 +1,1 @@ -+30 +30 diff --git a/tests/normalization/examples/Natural/product/1B.dhall b/tests/normalization/examples/Natural/product/1B.dhall --- a/tests/normalization/examples/Natural/product/1B.dhall +++ b/tests/normalization/examples/Natural/product/1B.dhall @@ -1,1 +1,1 @@ -+1 +1 diff --git a/tests/normalization/examples/Natural/show/0A.dhall b/tests/normalization/examples/Natural/show/0A.dhall --- a/tests/normalization/examples/Natural/show/0A.dhall +++ b/tests/normalization/examples/Natural/show/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Natural/show +3 +../../../../../Prelude/Natural/show 3 diff --git a/tests/normalization/examples/Natural/show/0B.dhall b/tests/normalization/examples/Natural/show/0B.dhall --- a/tests/normalization/examples/Natural/show/0B.dhall +++ b/tests/normalization/examples/Natural/show/0B.dhall @@ -1,1 +1,1 @@ -"+3" +"3" diff --git a/tests/normalization/examples/Natural/show/1A.dhall b/tests/normalization/examples/Natural/show/1A.dhall --- a/tests/normalization/examples/Natural/show/1A.dhall +++ b/tests/normalization/examples/Natural/show/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Natural/show +0 +../../../../../Prelude/Natural/show 0 diff --git a/tests/normalization/examples/Natural/show/1B.dhall b/tests/normalization/examples/Natural/show/1B.dhall --- a/tests/normalization/examples/Natural/show/1B.dhall +++ b/tests/normalization/examples/Natural/show/1B.dhall @@ -1,1 +1,1 @@ -"+0" +"0" diff --git a/tests/normalization/examples/Natural/sum/0A.dhall b/tests/normalization/examples/Natural/sum/0A.dhall --- a/tests/normalization/examples/Natural/sum/0A.dhall +++ b/tests/normalization/examples/Natural/sum/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Natural/sum [ +2, +3, +5 ] +../../../../../Prelude/Natural/sum [ 2, 3, 5 ] diff --git a/tests/normalization/examples/Natural/sum/0B.dhall b/tests/normalization/examples/Natural/sum/0B.dhall --- a/tests/normalization/examples/Natural/sum/0B.dhall +++ b/tests/normalization/examples/Natural/sum/0B.dhall @@ -1,1 +1,1 @@ -+10 +10 diff --git a/tests/normalization/examples/Natural/sum/1B.dhall b/tests/normalization/examples/Natural/sum/1B.dhall --- a/tests/normalization/examples/Natural/sum/1B.dhall +++ b/tests/normalization/examples/Natural/sum/1B.dhall @@ -1,1 +1,1 @@ -+0 +0 diff --git a/tests/normalization/examples/Natural/toInteger/0A.dhall b/tests/normalization/examples/Natural/toInteger/0A.dhall --- a/tests/normalization/examples/Natural/toInteger/0A.dhall +++ b/tests/normalization/examples/Natural/toInteger/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Natural/toInteger +3 +../../../../../Prelude/Natural/toInteger 3 diff --git a/tests/normalization/examples/Natural/toInteger/0B.dhall b/tests/normalization/examples/Natural/toInteger/0B.dhall --- a/tests/normalization/examples/Natural/toInteger/0B.dhall +++ b/tests/normalization/examples/Natural/toInteger/0B.dhall @@ -1,1 +1,1 @@ -3 ++3 diff --git a/tests/normalization/examples/Natural/toInteger/1A.dhall b/tests/normalization/examples/Natural/toInteger/1A.dhall --- a/tests/normalization/examples/Natural/toInteger/1A.dhall +++ b/tests/normalization/examples/Natural/toInteger/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Natural/toInteger +0 +../../../../../Prelude/Natural/toInteger 0 diff --git a/tests/normalization/examples/Natural/toInteger/1B.dhall b/tests/normalization/examples/Natural/toInteger/1B.dhall --- a/tests/normalization/examples/Natural/toInteger/1B.dhall +++ b/tests/normalization/examples/Natural/toInteger/1B.dhall @@ -1,1 +1,1 @@ -0 ++0 diff --git a/tests/normalization/examples/Optional/all/0A.dhall b/tests/normalization/examples/Optional/all/0A.dhall --- a/tests/normalization/examples/Optional/all/0A.dhall +++ b/tests/normalization/examples/Optional/all/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Optional/all Natural Natural/even ([ +3 ] : Optional Natural) +../../../../../Prelude/Optional/all Natural Natural/even ([ 3 ] : Optional Natural) diff --git a/tests/normalization/examples/Optional/any/0A.dhall b/tests/normalization/examples/Optional/any/0A.dhall --- a/tests/normalization/examples/Optional/any/0A.dhall +++ b/tests/normalization/examples/Optional/any/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Optional/any Natural Natural/even ([ +2 ] : Optional Natural) +../../../../../Prelude/Optional/any Natural Natural/even ([ 2 ] : Optional Natural) diff --git a/tests/normalization/examples/Optional/build/0A.dhall b/tests/normalization/examples/Optional/build/0A.dhall --- a/tests/normalization/examples/Optional/build/0A.dhall +++ b/tests/normalization/examples/Optional/build/0A.dhall @@ -1,7 +1,7 @@ ../../../../../Prelude/Optional/build -Integer +Natural ( λ(optional : Type) -→ λ(just : Integer → optional) +→ λ(just : Natural → optional) → λ(nothing : optional) → just 1 ) diff --git a/tests/normalization/examples/Optional/build/0B.dhall b/tests/normalization/examples/Optional/build/0B.dhall --- a/tests/normalization/examples/Optional/build/0B.dhall +++ b/tests/normalization/examples/Optional/build/0B.dhall @@ -1,1 +1,1 @@ -[ 1 ] : Optional Integer +[ 1 ] : Optional Natural diff --git a/tests/normalization/examples/Optional/build/1A.dhall b/tests/normalization/examples/Optional/build/1A.dhall --- a/tests/normalization/examples/Optional/build/1A.dhall +++ b/tests/normalization/examples/Optional/build/1A.dhall @@ -1,7 +1,7 @@ ../../../../../Prelude/Optional/build -Integer +Natural ( λ(optional : Type) -→ λ(just : Integer → optional) +→ λ(just : Natural → optional) → λ(nothing : optional) → nothing ) diff --git a/tests/normalization/examples/Optional/build/1B.dhall b/tests/normalization/examples/Optional/build/1B.dhall --- a/tests/normalization/examples/Optional/build/1B.dhall +++ b/tests/normalization/examples/Optional/build/1B.dhall @@ -1,1 +1,1 @@ -[] : Optional Integer +[] : Optional Natural diff --git a/tests/normalization/examples/Optional/concat/0A.dhall b/tests/normalization/examples/Optional/concat/0A.dhall --- a/tests/normalization/examples/Optional/concat/0A.dhall +++ b/tests/normalization/examples/Optional/concat/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Optional/concat Integer ([ [ 1 ] : Optional Integer ] : Optional (Optional Integer)) +../../../../../Prelude/Optional/concat Natural ([ [ 1 ] : Optional Natural ] : Optional (Optional Natural)) diff --git a/tests/normalization/examples/Optional/concat/0B.dhall b/tests/normalization/examples/Optional/concat/0B.dhall --- a/tests/normalization/examples/Optional/concat/0B.dhall +++ b/tests/normalization/examples/Optional/concat/0B.dhall @@ -1,1 +1,1 @@ -[ 1 ] : Optional Integer +[ 1 ] : Optional Natural diff --git a/tests/normalization/examples/Optional/concat/1A.dhall b/tests/normalization/examples/Optional/concat/1A.dhall --- a/tests/normalization/examples/Optional/concat/1A.dhall +++ b/tests/normalization/examples/Optional/concat/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Optional/concat Integer ([ [] : Optional Integer ] : Optional (Optional Integer)) +../../../../../Prelude/Optional/concat Natural ([ [] : Optional Natural ] : Optional (Optional Natural)) diff --git a/tests/normalization/examples/Optional/concat/1B.dhall b/tests/normalization/examples/Optional/concat/1B.dhall --- a/tests/normalization/examples/Optional/concat/1B.dhall +++ b/tests/normalization/examples/Optional/concat/1B.dhall @@ -1,1 +1,1 @@ -[] : Optional Integer +[] : Optional Natural diff --git a/tests/normalization/examples/Optional/concat/2A.dhall b/tests/normalization/examples/Optional/concat/2A.dhall --- a/tests/normalization/examples/Optional/concat/2A.dhall +++ b/tests/normalization/examples/Optional/concat/2A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Optional/concat Integer ([ [] : Optional Integer ]: Optional (Optional Integer)) +../../../../../Prelude/Optional/concat Natural ([ [] : Optional Natural ]: Optional (Optional Natural)) diff --git a/tests/normalization/examples/Optional/concat/2B.dhall b/tests/normalization/examples/Optional/concat/2B.dhall --- a/tests/normalization/examples/Optional/concat/2B.dhall +++ b/tests/normalization/examples/Optional/concat/2B.dhall @@ -1,1 +1,1 @@ -[] : Optional Integer +[] : Optional Natural diff --git a/tests/normalization/examples/Optional/filter/0A.dhall b/tests/normalization/examples/Optional/filter/0A.dhall --- a/tests/normalization/examples/Optional/filter/0A.dhall +++ b/tests/normalization/examples/Optional/filter/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Optional/filter Natural Natural/even ([ +2 ] : Optional Natural) +../../../../../Prelude/Optional/filter Natural Natural/even ([ 2 ] : Optional Natural) diff --git a/tests/normalization/examples/Optional/filter/0B.dhall b/tests/normalization/examples/Optional/filter/0B.dhall --- a/tests/normalization/examples/Optional/filter/0B.dhall +++ b/tests/normalization/examples/Optional/filter/0B.dhall @@ -1,1 +1,1 @@ -[ +2 ] : Optional Natural +[ 2 ] : Optional Natural diff --git a/tests/normalization/examples/Optional/filter/1A.dhall b/tests/normalization/examples/Optional/filter/1A.dhall --- a/tests/normalization/examples/Optional/filter/1A.dhall +++ b/tests/normalization/examples/Optional/filter/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Optional/filter Natural Natural/odd ([ +2 ] : Optional Natural) +../../../../../Prelude/Optional/filter Natural Natural/odd ([ 2 ] : Optional Natural) diff --git a/tests/normalization/examples/Optional/fold/0A.dhall b/tests/normalization/examples/Optional/fold/0A.dhall --- a/tests/normalization/examples/Optional/fold/0A.dhall +++ b/tests/normalization/examples/Optional/fold/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Optional/fold Integer ([ 2 ] : Optional Integer) Integer (λ(x : Integer) → x) 0 +../../../../../Prelude/Optional/fold Natural ([ 2 ] : Optional Natural) Natural (λ(x : Natural) → x) 0 diff --git a/tests/normalization/examples/Optional/fold/1A.dhall b/tests/normalization/examples/Optional/fold/1A.dhall --- a/tests/normalization/examples/Optional/fold/1A.dhall +++ b/tests/normalization/examples/Optional/fold/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Optional/fold Integer ([] : Optional Integer) Integer (λ(x : Integer) → x) 0 +../../../../../Prelude/Optional/fold Natural ([] : Optional Natural) Natural (λ(x : Natural) → x) 0 diff --git a/tests/normalization/examples/Optional/head/0A.dhall b/tests/normalization/examples/Optional/head/0A.dhall --- a/tests/normalization/examples/Optional/head/0A.dhall +++ b/tests/normalization/examples/Optional/head/0A.dhall @@ -1,6 +1,6 @@ ../../../../../Prelude/Optional/head -Integer -[ [] : Optional Integer -, [ 1 ] : Optional Integer -, [ 2 ] : Optional Integer +Natural +[ [] : Optional Natural +, [ 1 ] : Optional Natural +, [ 2 ] : Optional Natural ] diff --git a/tests/normalization/examples/Optional/head/0B.dhall b/tests/normalization/examples/Optional/head/0B.dhall --- a/tests/normalization/examples/Optional/head/0B.dhall +++ b/tests/normalization/examples/Optional/head/0B.dhall @@ -1,1 +1,1 @@ -[ 1 ] : Optional Integer +[ 1 ] : Optional Natural diff --git a/tests/normalization/examples/Optional/head/1A.dhall b/tests/normalization/examples/Optional/head/1A.dhall --- a/tests/normalization/examples/Optional/head/1A.dhall +++ b/tests/normalization/examples/Optional/head/1A.dhall @@ -1,3 +1,3 @@ ../../../../../Prelude/Optional/head -Integer -[ [] : Optional Integer, [] : Optional Integer ] +Natural +[ [] : Optional Natural, [] : Optional Natural ] diff --git a/tests/normalization/examples/Optional/head/1B.dhall b/tests/normalization/examples/Optional/head/1B.dhall --- a/tests/normalization/examples/Optional/head/1B.dhall +++ b/tests/normalization/examples/Optional/head/1B.dhall @@ -1,1 +1,1 @@ -[] : Optional Integer +[] : Optional Natural diff --git a/tests/normalization/examples/Optional/last/0A.dhall b/tests/normalization/examples/Optional/last/0A.dhall --- a/tests/normalization/examples/Optional/last/0A.dhall +++ b/tests/normalization/examples/Optional/last/0A.dhall @@ -1,7 +1,7 @@ ../../../../../Prelude/Optional/last -Integer -( [ [] : Optional Integer - , [ 1 ] : Optional Integer - , [ 2 ] : Optional Integer +Natural +( [ [] : Optional Natural + , [ 1 ] : Optional Natural + , [ 2 ] : Optional Natural ] ) diff --git a/tests/normalization/examples/Optional/last/0B.dhall b/tests/normalization/examples/Optional/last/0B.dhall --- a/tests/normalization/examples/Optional/last/0B.dhall +++ b/tests/normalization/examples/Optional/last/0B.dhall @@ -1,1 +1,1 @@ -[ 2 ] : Optional Integer +[ 2 ] : Optional Natural diff --git a/tests/normalization/examples/Optional/last/1A.dhall b/tests/normalization/examples/Optional/last/1A.dhall --- a/tests/normalization/examples/Optional/last/1A.dhall +++ b/tests/normalization/examples/Optional/last/1A.dhall @@ -1,3 +1,3 @@ ../../../../../Prelude/Optional/last -Integer -[ [] : Optional Integer, [] : Optional Integer ] +Natural +[ [] : Optional Natural, [] : Optional Natural ] diff --git a/tests/normalization/examples/Optional/last/1B.dhall b/tests/normalization/examples/Optional/last/1B.dhall --- a/tests/normalization/examples/Optional/last/1B.dhall +++ b/tests/normalization/examples/Optional/last/1B.dhall @@ -1,1 +1,1 @@ -[] : Optional Integer +[] : Optional Natural diff --git a/tests/normalization/examples/Optional/last/2A.dhall b/tests/normalization/examples/Optional/last/2A.dhall --- a/tests/normalization/examples/Optional/last/2A.dhall +++ b/tests/normalization/examples/Optional/last/2A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Optional/last Integer ([] : List (Optional Integer)) +../../../../../Prelude/Optional/last Natural ([] : List (Optional Natural)) diff --git a/tests/normalization/examples/Optional/last/2B.dhall b/tests/normalization/examples/Optional/last/2B.dhall --- a/tests/normalization/examples/Optional/last/2B.dhall +++ b/tests/normalization/examples/Optional/last/2B.dhall @@ -1,1 +1,1 @@ -[] : Optional Integer +[] : Optional Natural diff --git a/tests/normalization/examples/Optional/length/0A.dhall b/tests/normalization/examples/Optional/length/0A.dhall --- a/tests/normalization/examples/Optional/length/0A.dhall +++ b/tests/normalization/examples/Optional/length/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Optional/length Integer ([ 2 ] : Optional Integer) +../../../../../Prelude/Optional/length Natural ([ 2 ] : Optional Natural) diff --git a/tests/normalization/examples/Optional/length/0B.dhall b/tests/normalization/examples/Optional/length/0B.dhall --- a/tests/normalization/examples/Optional/length/0B.dhall +++ b/tests/normalization/examples/Optional/length/0B.dhall @@ -1,1 +1,1 @@ -+1 +1 diff --git a/tests/normalization/examples/Optional/length/1A.dhall b/tests/normalization/examples/Optional/length/1A.dhall --- a/tests/normalization/examples/Optional/length/1A.dhall +++ b/tests/normalization/examples/Optional/length/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Optional/length Integer ([] : Optional Integer) +../../../../../Prelude/Optional/length Natural ([] : Optional Natural) diff --git a/tests/normalization/examples/Optional/length/1B.dhall b/tests/normalization/examples/Optional/length/1B.dhall --- a/tests/normalization/examples/Optional/length/1B.dhall +++ b/tests/normalization/examples/Optional/length/1B.dhall @@ -1,1 +1,1 @@ -+0 +0 diff --git a/tests/normalization/examples/Optional/map/0A.dhall b/tests/normalization/examples/Optional/map/0A.dhall --- a/tests/normalization/examples/Optional/map/0A.dhall +++ b/tests/normalization/examples/Optional/map/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Optional/map Natural Bool Natural/even ([ +3 ] : Optional Natural) +../../../../../Prelude/Optional/map Natural Bool Natural/even ([ 3 ] : Optional Natural) diff --git a/tests/normalization/examples/Optional/null/0A.dhall b/tests/normalization/examples/Optional/null/0A.dhall --- a/tests/normalization/examples/Optional/null/0A.dhall +++ b/tests/normalization/examples/Optional/null/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Optional/null Integer ([ 2 ] : Optional Integer) +../../../../../Prelude/Optional/null Natural ([ 2 ] : Optional Natural) diff --git a/tests/normalization/examples/Optional/null/1A.dhall b/tests/normalization/examples/Optional/null/1A.dhall --- a/tests/normalization/examples/Optional/null/1A.dhall +++ b/tests/normalization/examples/Optional/null/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Optional/null Integer ([] : Optional Integer) +../../../../../Prelude/Optional/null Natural ([] : Optional Natural) diff --git a/tests/normalization/examples/Optional/toList/0A.dhall b/tests/normalization/examples/Optional/toList/0A.dhall --- a/tests/normalization/examples/Optional/toList/0A.dhall +++ b/tests/normalization/examples/Optional/toList/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Optional/toList Integer ([ 1 ] : Optional Integer) +../../../../../Prelude/Optional/toList Natural ([ 1 ] : Optional Natural) diff --git a/tests/normalization/examples/Optional/toList/1A.dhall b/tests/normalization/examples/Optional/toList/1A.dhall --- a/tests/normalization/examples/Optional/toList/1A.dhall +++ b/tests/normalization/examples/Optional/toList/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Optional/toList Integer ([] : Optional Integer) +../../../../../Prelude/Optional/toList Natural ([] : Optional Natural) diff --git a/tests/normalization/examples/Optional/toList/1B.dhall b/tests/normalization/examples/Optional/toList/1B.dhall --- a/tests/normalization/examples/Optional/toList/1B.dhall +++ b/tests/normalization/examples/Optional/toList/1B.dhall @@ -1,1 +1,1 @@ -[] : List Integer +[] : List Natural diff --git a/tests/normalization/examples/Text/concatMap/0A.dhall b/tests/normalization/examples/Text/concatMap/0A.dhall --- a/tests/normalization/examples/Text/concatMap/0A.dhall +++ b/tests/normalization/examples/Text/concatMap/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Text/concatMap Integer (λ(n : Integer) → "${Integer/show n} ") [ 0, 1, 2 ] +../../../../../Prelude/Text/concatMap Natural (λ(n : Natural) → "${Natural/show n} ") [ 0, 1, 2 ] diff --git a/tests/normalization/examples/Text/concatMap/1A.dhall b/tests/normalization/examples/Text/concatMap/1A.dhall --- a/tests/normalization/examples/Text/concatMap/1A.dhall +++ b/tests/normalization/examples/Text/concatMap/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Text/concatMap Integer (λ(n : Integer) → "${Integer/show n} ") ([] : List Integer) +../../../../../Prelude/Text/concatMap Natural (λ(n : Natural) → "${Natural/show n} ") ([] : List Natural) diff --git a/tests/normalization/examples/Text/concatMapSep/0A.dhall b/tests/normalization/examples/Text/concatMapSep/0A.dhall --- a/tests/normalization/examples/Text/concatMapSep/0A.dhall +++ b/tests/normalization/examples/Text/concatMapSep/0A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Text/concatMapSep ", " Integer Integer/show [ 0, 1, 2 ] +../../../../../Prelude/Text/concatMapSep ", " Natural Natural/show [ 0, 1, 2 ] diff --git a/tests/normalization/examples/Text/concatMapSep/1A.dhall b/tests/normalization/examples/Text/concatMapSep/1A.dhall --- a/tests/normalization/examples/Text/concatMapSep/1A.dhall +++ b/tests/normalization/examples/Text/concatMapSep/1A.dhall @@ -1,1 +1,1 @@ -../../../../../Prelude/Text/concatMapSep ", " Integer Integer/show ([] : List Integer) +../../../../../Prelude/Text/concatMapSep ", " Natural Natural/show ([] : List Natural) diff --git a/tests/normalization/integerShowA.dhall b/tests/normalization/integerShowA.dhall --- a/tests/normalization/integerShowA.dhall +++ b/tests/normalization/integerShowA.dhall @@ -1,4 +1,4 @@ -{ example0 = Integer/show 1337 +{ example0 = Integer/show +1337 , example1 = Integer/show -42 -, example2 = Integer/show 0 +, example2 = Integer/show +0 } diff --git a/tests/normalization/integerShowB.dhall b/tests/normalization/integerShowB.dhall --- a/tests/normalization/integerShowB.dhall +++ b/tests/normalization/integerShowB.dhall @@ -1,1 +1,1 @@ -{ example0 = "1337", example1 = "-42", example2 = "0" } +{ example0 = "+1337", example1 = "-42", example2 = "+0" } diff --git a/tests/normalization/naturalPlusA.dhall b/tests/normalization/naturalPlusA.dhall --- a/tests/normalization/naturalPlusA.dhall +++ b/tests/normalization/naturalPlusA.dhall @@ -1,1 +1,1 @@ -+1 + +2 +1 + 2 diff --git a/tests/normalization/naturalPlusB.dhall b/tests/normalization/naturalPlusB.dhall --- a/tests/normalization/naturalPlusB.dhall +++ b/tests/normalization/naturalPlusB.dhall @@ -1,1 +1,1 @@ -+3 +3 diff --git a/tests/normalization/naturalShowA.dhall b/tests/normalization/naturalShowA.dhall --- a/tests/normalization/naturalShowA.dhall +++ b/tests/normalization/naturalShowA.dhall @@ -1,1 +1,1 @@ -Natural/show +42 +Natural/show 42 diff --git a/tests/normalization/naturalShowB.dhall b/tests/normalization/naturalShowB.dhall --- a/tests/normalization/naturalShowB.dhall +++ b/tests/normalization/naturalShowB.dhall @@ -1,1 +1,1 @@ -"+42" +"42" diff --git a/tests/normalization/naturalToIntegerA.dhall b/tests/normalization/naturalToIntegerA.dhall --- a/tests/normalization/naturalToIntegerA.dhall +++ b/tests/normalization/naturalToIntegerA.dhall @@ -1,1 +1,1 @@ -Natural/toInteger +1 +Natural/toInteger 1 diff --git a/tests/normalization/naturalToIntegerB.dhall b/tests/normalization/naturalToIntegerB.dhall --- a/tests/normalization/naturalToIntegerB.dhall +++ b/tests/normalization/naturalToIntegerB.dhall @@ -1,1 +1,1 @@ -1 ++1 diff --git a/tests/normalization/optionalBuildA.dhall b/tests/normalization/optionalBuildA.dhall --- a/tests/normalization/optionalBuildA.dhall +++ b/tests/normalization/optionalBuildA.dhall @@ -4,12 +4,12 @@ ( λ(optional : Type) → λ(just : Natural → optional) → λ(nothing : optional) - → just +1 + → just 1 ) , example1 = Optional/build Integer - (λ(optional : Type) → λ(x : Integer → optional) → λ(x : optional) → x@1 1) + (λ(optional : Type) → λ(x : Integer → optional) → λ(x : optional) → x@1 +1) , example2 = λ(id : ∀(a : Type) → a → a) → Optional/build diff --git a/tests/normalization/optionalBuildB.dhall b/tests/normalization/optionalBuildB.dhall --- a/tests/normalization/optionalBuildB.dhall +++ b/tests/normalization/optionalBuildB.dhall @@ -1,7 +1,7 @@ { example0 = - [ +1 ] : Optional Natural + [ 1 ] : Optional Natural , example1 = - [ 1 ] : Optional Integer + [ +1 ] : Optional Integer , example2 = λ(id : ∀(a : Type) → a → a) → id (Optional Bool) ([ True ] : Optional Bool) , example3 = diff --git a/tests/normalization/optionalFoldA.dhall b/tests/normalization/optionalFoldA.dhall --- a/tests/normalization/optionalFoldA.dhall +++ b/tests/normalization/optionalFoldA.dhall @@ -1,6 +1,6 @@ let f = λ(o : Optional Text) - → Optional/fold Text o Natural (λ(j : Text) → +1) +2 + → Optional/fold Text o Natural (λ(j : Text) → 1) 2 in { example0 = f ([ "foo" ] : Optional Text) , example1 = f ([] : Optional Text) diff --git a/tests/normalization/optionalFoldB.dhall b/tests/normalization/optionalFoldB.dhall --- a/tests/normalization/optionalFoldB.dhall +++ b/tests/normalization/optionalFoldB.dhall @@ -1,1 +1,1 @@ -{ example0 = +1, example1 = +2 } +{ example0 = 1, example1 = 2 } diff --git a/tests/parser/urls.dhall b/tests/parser/urls.dhall --- a/tests/parser/urls.dhall +++ b/tests/parser/urls.dhall @@ -1,11 +1,11 @@ -[ http://example.com +[ http://example.com/someFile.dhall , https://john:doe@example.com:8080/foo/bar?qux=0#xyzzy -, http://prelude.dhall-lang.org/ +, http://prelude.dhall-lang.org/package.dhall , https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude -, https://127.0.0.1 -, https://[::] -, https://[2001:0db8:85a3:0000:0000:8a2e:0370:7334] +, https://127.0.0.1/index.dhall +, https://[::]/index.dhall +, https://[2001:0db8:85a3:0000:0000:8a2e:0370:7334]/tutorial.dhall -- Yes, this is legal -, https://-._~%2C!$&'()*+,;=:@-._~%2C!$&'()*+,;=:/-._~%2C!$&'()*+,;=:@?/-._~%2C!$&'()*+,;=:@/?#/-._~%2C!$&'()*+,;=:@/? +, https://-._~%2C!$&'()*+,;=:@-._~%2C!$&'()*+,;=:/foo?/-._~%2C!$&'()*+,;=:@/?#/-._~%2C!$&'()*+,;=:@/? ] diff --git a/tests/regression/issue216b.dhall b/tests/regression/issue216b.dhall --- a/tests/regression/issue216b.dhall +++ b/tests/regression/issue216b.dhall @@ -1,10 +1,2 @@ - let GitHubProject : Type = { owner : Text, repo : Text } - -in let gitHubProject = - λ(github : GitHubProject) - → let gitHubRoot = - "https://github.com/${github.owner}/${github.repo}" - - in { bugReports = "${gitHubRoot}/issues" } - -in gitHubProject + λ(github : { owner : Text, repo : Text }) +→ { bugReports = "https://github.com/${github.owner}/${github.repo}/issues" } diff --git a/tests/tutorial/unions0A.dhall b/tests/tutorial/unions0A.dhall --- a/tests/tutorial/unions0A.dhall +++ b/tests/tutorial/unions0A.dhall @@ -1,1 +1,1 @@ -./process.dhall < Left = +3 | Right : Bool > +./process.dhall < Left = 3 | Right : Bool > diff --git a/tests/tutorial/unions2A.dhall b/tests/tutorial/unions2A.dhall --- a/tests/tutorial/unions2A.dhall +++ b/tests/tutorial/unions2A.dhall @@ -2,7 +2,7 @@ in let Person = λ(p : { name : Text, age : Natural }) → < Person = p | Empty : {} > in [ Empty - , Person { name = "John", age = +23 } - , Person { name = "Amy" , age = +25 } + , Person { name = "John", age = 23 } + , Person { name = "Amy" , age = 25 } , Empty ] diff --git a/tests/tutorial/unions2B.dhall b/tests/tutorial/unions2B.dhall --- a/tests/tutorial/unions2B.dhall +++ b/tests/tutorial/unions2B.dhall @@ -1,5 +1,5 @@ [ < Empty = {=} | Person : { age : Natural, name : Text } > -, < Person = { age = +23, name = "John" } | Empty : {} > -, < Person = { age = +25, name = "Amy" } | Empty : {} > +, < Person = { age = 23, name = "John" } | Empty : {} > +, < Person = { age = 25, name = "Amy" } | Empty : {} > , < Empty = {=} | Person : { age : Natural, name : Text } > ] diff --git a/tests/tutorial/unions3A.dhall b/tests/tutorial/unions3A.dhall --- a/tests/tutorial/unions3A.dhall +++ b/tests/tutorial/unions3A.dhall @@ -1,5 +1,5 @@ let MyType = constructors < Empty : {} | Person : { name : Text, age : Natural } > in [ MyType.Empty {=} - , MyType.Person { name = "John", age = +23 } - , MyType.Person { name = "Amy" , age = +25 } + , MyType.Person { name = "John", age = 23 } + , MyType.Person { name = "Amy" , age = 25 } ] diff --git a/tests/tutorial/unions3B.dhall b/tests/tutorial/unions3B.dhall --- a/tests/tutorial/unions3B.dhall +++ b/tests/tutorial/unions3B.dhall @@ -1,4 +1,4 @@ [ < Empty = {=} | Person : { age : Natural, name : Text } > -, < Person = { age = +23, name = "John" } | Empty : {} > -, < Person = { age = +25, name = "Amy" } | Empty : {} > +, < Person = { age = 23, name = "John" } | Empty : {} > +, < Person = { age = 25, name = "Amy" } | Empty : {} > ] diff --git a/tests/typecheck/mergeEquivalenceA.dhall b/tests/typecheck/mergeEquivalenceA.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/mergeEquivalenceA.dhall @@ -0,0 +1,6 @@ + let Foo = < Bar : {} | Baz : {} > + +in λ(a : Type) + → λ(f : {} → a) + → λ(ts : Foo) + → merge { Bar = λ(a : {}) → f a, Baz = f } ts diff --git a/tests/typecheck/mergeEquivalenceB.dhall b/tests/typecheck/mergeEquivalenceB.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/mergeEquivalenceB.dhall @@ -0,0 +1,1 @@ +∀(a : Type) → ∀(f : {} → a) → ∀(ts : < Bar : {} | Baz : {} >) → a