diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,27 @@ +1.7.0 + +* BREAKING CHANGE TO LANGUAGE: Update parser to match standardized grammar + * Trailing commas and bars no longer supported for union and record literals + * Paths no longer permit commas + * URL grammar is now RFC-compliant + * Environment variables can now be quoted to support full range of + POSIX-compliant names + * Text literals support full set of JSON escape sequences (such as `\u2192`) +* BREAKING CHANGE TO LANGUAGE: Single quoted strings strip leading newlines +* BUG FIX: Fixed type-checking infinite loops due to non-type-checked variables + in context +* BUG FIX: Fixed type-checking bug due to missing context when type-checking + certain expressions +* BUG FIX: Fixed type-checking bug due to off-by-one errors in name shadowing + logic +* New `dhall-format` executable to automatically format code +* Performance optimizations to `Natural/fold` and `List/fold` +* Improved parsing performance (over 3x faster) +* Union literals can now specify the set value anywhere in the literal + * i.e. `< A : Integer | B = False | C : Text >` +* New `Inject` instance for `()` +* Several tutorial fixes and improvements + 1.6.0 * BREAKING CHANGE TO THE API: Drop support for GHC 7.* diff --git a/Prelude/Bool/and b/Prelude/Bool/and --- a/Prelude/Bool/and +++ b/Prelude/Bool/and @@ -10,8 +10,9 @@ ./and ([] : List Bool) = True ``` -} -let and : List Bool → Bool - = λ(xs : List Bool) - → List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l && r) True + let and + : List Bool → Bool + = λ(xs : List Bool) + → List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l && r) True in and diff --git a/Prelude/Bool/build b/Prelude/Bool/build --- a/Prelude/Bool/build +++ b/Prelude/Bool/build @@ -9,8 +9,9 @@ ./build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → false) = False ``` -} -let build : (∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) → Bool - = λ(f : ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) - → f Bool True False + let build + : (∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) → Bool + = λ(f : ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) + → f Bool True False in build diff --git a/Prelude/Bool/even b/Prelude/Bool/even --- a/Prelude/Bool/even +++ b/Prelude/Bool/even @@ -14,8 +14,9 @@ ./even ([] : List Bool) = True ``` -} -let even : List Bool → Bool - = λ(xs : List Bool) - → List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x == y) True + let even + : List Bool → Bool + = λ(xs : List Bool) + → List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x == y) True in even diff --git a/Prelude/Bool/fold b/Prelude/Bool/fold --- a/Prelude/Bool/fold +++ b/Prelude/Bool/fold @@ -9,11 +9,12 @@ ./fold False Integer 0 1 = 1 ``` -} -let fold : ∀(b : Bool) → ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool - = λ(b : Bool) - → λ(bool : Type) - → λ(true : bool) - → λ(false : bool) - → if b then true else false + let fold + : ∀(b : Bool) → ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool + = λ(b : Bool) + → λ(bool : Type) + → λ(true : bool) + → λ(false : bool) + → if b then true else false in fold diff --git a/Prelude/Bool/not b/Prelude/Bool/not --- a/Prelude/Bool/not +++ b/Prelude/Bool/not @@ -9,7 +9,4 @@ ./not False = True ``` -} -let not : Bool → Bool - = λ(b : Bool) → b == False - -in not +let not : Bool → Bool = λ(b : Bool) → b == False in not diff --git a/Prelude/Bool/odd b/Prelude/Bool/odd --- a/Prelude/Bool/odd +++ b/Prelude/Bool/odd @@ -14,8 +14,9 @@ ./odd ([] : List Bool) = False ``` -} -let odd : List Bool → Bool - = λ(xs : List Bool) - → List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x != y) False + let odd + : List Bool → Bool + = λ(xs : List Bool) + → List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x != y) False in odd diff --git a/Prelude/Bool/or b/Prelude/Bool/or --- a/Prelude/Bool/or +++ b/Prelude/Bool/or @@ -10,8 +10,9 @@ ./or ([] : List Bool) = False ``` -} -let or : List Bool → Bool - = λ(xs : List Bool) - → List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l || r) False + let or + : List Bool → Bool + = λ(xs : List Bool) + → List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l || r) False in or diff --git a/Prelude/Bool/show b/Prelude/Bool/show --- a/Prelude/Bool/show +++ b/Prelude/Bool/show @@ -10,7 +10,4 @@ ./show False = "False" ``` -} -let show : Bool → Text - = λ(b : Bool) → if b then "True" else "False" - -in show +let show : Bool → Text = λ(b : Bool) → if b then "True" else "False" in show diff --git a/Prelude/Double/show b/Prelude/Double/show --- a/Prelude/Double/show +++ b/Prelude/Double/show @@ -10,7 +10,4 @@ ./show 0.4 = "0.4" ``` -} -let show : Double → Text - = Double/show - -in show +let show : Double → Text = Double/show in show diff --git a/Prelude/Integer/show b/Prelude/Integer/show --- a/Prelude/Integer/show +++ b/Prelude/Integer/show @@ -10,7 +10,4 @@ ./show 0 = "0" ``` -} -let show : Integer → Text - = Integer/show - -in show +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 @@ -10,10 +10,11 @@ ./all Natural Natural/even ([] : List Natural) = True ``` -} -let all : ∀(a : Type) → (a → Bool) → List a → Bool - = λ(a : Type) - → λ(f : a → Bool) - → λ(xs : List a) - → List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x && r) True + let all + : ∀(a : Type) → (a → Bool) → List a → Bool + = λ(a : Type) + → λ(f : a → Bool) + → λ(xs : List a) + → List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x && r) True in all diff --git a/Prelude/List/any b/Prelude/List/any --- a/Prelude/List/any +++ b/Prelude/List/any @@ -10,10 +10,11 @@ ./any Natural Natural/even ([] : List Natural) = False ``` -} -let any : ∀(a : Type) → (a → Bool) → List a → Bool - = λ(a : Type) - → λ(f : a → Bool) - → λ(xs : List a) - → List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x || r) False + let any + : ∀(a : Type) → (a → Bool) → List a → Bool + = λ(a : Type) + → λ(f : a → Bool) + → λ(xs : List a) + → List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x || r) False in any diff --git a/Prelude/List/build b/Prelude/List/build --- a/Prelude/List/build +++ b/Prelude/List/build @@ -23,10 +23,10 @@ = [] : List Text ``` -} -let build - : ∀(a : Type) - → (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list) - → List a - = List/build + let build + : ∀(a : Type) + → (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list) + → List a + = List/build in build diff --git a/Prelude/List/concat b/Prelude/List/concat --- a/Prelude/List/concat +++ b/Prelude/List/concat @@ -23,28 +23,21 @@ ./concat Integer ([] : List (List Integer)) = [] : List Integer ``` -} -let concat : ∀(a : Type) → List (List a) → List a - = λ(a : Type) - → λ(xss : List (List a)) - → List/build - a - ( λ(list : Type) - → λ(cons : a → list → list) - → λ(nil : list) - → List/fold - (List a) - xss - list - ( λ(xs : List a) - → λ(ys : list) - → List/fold - a - xs + let concat + : ∀(a : Type) → List (List a) → List a + = λ(a : Type) + → λ(xss : List (List a)) + → List/build + a + ( λ(list : Type) + → λ(cons : a → list → list) + → λ(nil : list) + → List/fold + (List a) + xss list - cons - ys + (λ(xs : List a) → λ(ys : list) → List/fold a xs list cons ys) + nil ) - nil - ) in concat diff --git a/Prelude/List/concatMap b/Prelude/List/concatMap --- a/Prelude/List/concatMap +++ b/Prelude/List/concatMap @@ -12,16 +12,17 @@ = [] : List Natural ``` -} -let concatMap : ∀(a : Type) → ∀(b : Type) → (a → List b) → List a → List b - = λ(a : Type) - → λ(b : Type) - → λ(f : a → List b) - → λ(xs : List a) - → List/build - b - ( λ(list : Type) - → λ(cons : b → list → list) - → List/fold a xs list (λ(x : a) → List/fold b (f x) list cons) - ) + let concatMap + : ∀(a : Type) → ∀(b : Type) → (a → List b) → List a → List b + = λ(a : Type) + → λ(b : Type) + → λ(f : a → List b) + → λ(xs : List a) + → List/build + b + ( λ(list : Type) + → λ(cons : b → list → list) + → List/fold a xs list (λ(x : a) → List/fold b (f x) list cons) + ) in concatMap diff --git a/Prelude/List/filter b/Prelude/List/filter --- a/Prelude/List/filter +++ b/Prelude/List/filter @@ -11,19 +11,20 @@ = [+3, +5] : List Natural ``` -} -let filter : ∀(a : Type) → (a → Bool) → List a → List a - = λ(a : Type) - → λ(f : a → Bool) - → λ(xs : List a) - → List/build - a - ( λ(list : Type) - → λ(cons : a → list → list) - → List/fold + let filter + : ∀(a : Type) → (a → Bool) → List a → List a + = λ(a : Type) + → λ(f : a → Bool) + → λ(xs : List a) + → List/build a - xs - list - (λ(x : a) → λ(xs : list) → if f x then cons x xs else xs) - ) + ( λ(list : Type) + → λ(cons : a → list → list) + → List/fold + a + xs + list + (λ(x : a) → λ(xs : list) → if f x then cons x xs else xs) + ) in filter diff --git a/Prelude/List/fold b/Prelude/List/fold --- a/Prelude/List/fold +++ b/Prelude/List/fold @@ -34,13 +34,13 @@ → cons +2 (cons +3 (cons +5 nil)) ``` -} -let fold - : ∀(a : Type) - → List a - → ∀(list : Type) - → ∀(cons : a → list → list) - → ∀(nil : list) - → list - = List/fold + let fold + : ∀(a : Type) + → List a + → ∀(list : Type) + → ∀(cons : a → list → list) + → ∀(nil : list) + → list + = List/fold in fold diff --git a/Prelude/List/generate b/Prelude/List/generate --- a/Prelude/List/generate +++ b/Prelude/List/generate @@ -10,28 +10,29 @@ ./generate +0 Bool Natural/even = [] : List Bool ``` -} -let generate : Natural → ∀(a : Type) → (Natural → a) → List a - = λ(n : Natural) - → λ(a : Type) - → λ(f : Natural → a) - → List/build - a - ( λ(list : Type) - → λ(cons : a → list → list) - → List/fold - { index : Natural, value : {} } - ( List/indexed - {} - ( List/build + let generate + : Natural → ∀(a : Type) → (Natural → a) → List a + = λ(n : Natural) + → λ(a : Type) + → λ(f : Natural → a) + → List/build + a + ( λ(list : Type) + → λ(cons : a → list → list) + → List/fold + { index : Natural, value : {} } + ( List/indexed + {} + ( List/build {} ( λ(list : Type) - → λ(cons : {} → list → list) - → Natural/fold n list (cons {=}) + → λ(cons : {} → list → list) + → Natural/fold n list (cons {=}) ) + ) ) + list + (λ(x : { index : Natural, value : {} }) → cons (f x.index)) ) - list - (λ(x : { index : Natural, value : {} }) → cons (f x.index)) - ) in generate diff --git a/Prelude/List/head b/Prelude/List/head --- a/Prelude/List/head +++ b/Prelude/List/head @@ -9,7 +9,4 @@ ./head Integer ([] : List Integer) = [] : Optional Integer ``` -} -let head : ∀(a : Type) → List a → Optional a - = List/head - -in head +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 @@ -14,7 +14,8 @@ = [] : List { index : Natural, value : Bool } ``` -} -let indexed : ∀(a : Type) → List a → List { index : Natural, value : a } - = List/indexed + let indexed + : ∀(a : Type) → List a → List { index : Natural, value : a } + = List/indexed in indexed diff --git a/Prelude/List/iterate b/Prelude/List/iterate --- a/Prelude/List/iterate +++ b/Prelude/List/iterate @@ -12,31 +12,32 @@ = [] : List Natural ``` -} -let iterate : Natural → ∀(a : Type) → (a → a) → a → List a - = λ(n : Natural) - → λ(a : Type) - → λ(f : a → a) - → λ(x : a) - → List/build - a - ( λ(list : Type) - → λ(cons : a → list → list) - → List/fold - { index : Natural, value : {} } - ( List/indexed - {} - ( List/build + let iterate + : Natural → ∀(a : Type) → (a → a) → a → List a + = λ(n : Natural) + → λ(a : Type) + → λ(f : a → a) + → λ(x : a) + → List/build + a + ( λ(list : Type) + → λ(cons : a → list → list) + → List/fold + { index : Natural, value : {} } + ( List/indexed + {} + ( List/build {} ( λ(list : Type) - → λ(cons : {} → list → list) - → Natural/fold n list (cons {=}) + → λ(cons : {} → list → list) + → Natural/fold n list (cons {=}) ) + ) ) - ) - list - ( λ(y : { index : Natural, value : {} }) - → cons (Natural/fold y.index a f x) + list + ( λ(y : { index : Natural, value : {} }) + → cons (Natural/fold y.index a f x) + ) ) - ) in iterate diff --git a/Prelude/List/last b/Prelude/List/last --- a/Prelude/List/last +++ b/Prelude/List/last @@ -9,7 +9,4 @@ ./last Integer ([] : List Integer) = [] : Optional Integer ``` -} -let last : ∀(a : Type) → List a → Optional a - = List/last - -in last +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 @@ -9,7 +9,4 @@ ./length Integer ([] : List Integer) = +0 ``` -} -let length : ∀(a : Type) → List a → Natural - = List/length - -in length +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 @@ -11,16 +11,17 @@ = [] : List Bool ``` -} -let map : ∀(a : Type) → ∀(b : Type) → (a → b) → List a → List b - = λ(a : Type) - → λ(b : Type) - → λ(f : a → b) - → λ(xs : List a) - → List/build - b - ( λ(list : Type) - → λ(cons : b → list → list) - → List/fold a xs list (λ(x : a) → cons (f x)) - ) + let map + : ∀(a : Type) → ∀(b : Type) → (a → b) → List a → List b + = λ(a : Type) + → λ(b : Type) + → λ(f : a → b) + → λ(xs : List a) + → List/build + b + ( λ(list : Type) + → λ(cons : b → list → list) + → List/fold a xs list (λ(x : a) → cons (f x)) + ) in map diff --git a/Prelude/List/null b/Prelude/List/null --- a/Prelude/List/null +++ b/Prelude/List/null @@ -9,7 +9,8 @@ ./null Integer ([] : List Integer) = True ``` -} -let null : ∀(a : Type) → List a → Bool - = λ(a : Type) → λ(xs : List a) → Natural/isZero (List/length a xs) + let null + : ∀(a : Type) → List a → Bool + = λ(a : Type) → λ(xs : List a) → Natural/isZero (List/length a xs) in null diff --git a/Prelude/List/replicate b/Prelude/List/replicate --- a/Prelude/List/replicate +++ b/Prelude/List/replicate @@ -9,15 +9,16 @@ ./replicate +0 Integer 1 = [] : List Integer ``` -} -let replicate : Natural → ∀(a : Type) → a → List a - = λ(n : Natural) - → λ(a : Type) - → λ(x : a) - → List/build - a - ( λ(list : Type) - → λ(cons : a → list → list) - → Natural/fold n list (cons x) - ) + let replicate + : Natural → ∀(a : Type) → a → List a + = λ(n : Natural) + → λ(a : Type) + → λ(x : a) + → List/build + a + ( λ(list : Type) + → λ(cons : a → list → list) + → Natural/fold n list (cons x) + ) in replicate diff --git a/Prelude/List/reverse b/Prelude/List/reverse --- a/Prelude/List/reverse +++ b/Prelude/List/reverse @@ -9,7 +9,4 @@ ./reverse Integer ([] : List Integer) = [] : List Integer ``` -} -let reverse : ∀(a : Type) → List a → List a - = List/reverse - -in reverse +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 @@ -36,45 +36,53 @@ = [] : List { index : Natural, value : Bool } ``` -} -let shifted - : ∀(a : Type) - → List (List { index : Natural, value : a}) - → List { index : Natural, value : a } - = λ(a : Type) - → λ(kvss : List (List { index : Natural, value : a })) - → List/build - { index : Natural, value : a } - ( λ(list : Type) - → λ(cons : { index : Natural, value : a } → list → list) - → λ(nil : list) - → let result = - List/fold - (List { index : Natural, value : a }) - kvss - { count : Natural, diff : Natural → list } - ( λ(kvs : List { index : Natural, value : a }) - → λ(y : { count : Natural, diff : Natural → list }) - → let length = List/length { index : Natural, value : a } kvs - in { count = y.count + length - , diff = - λ(n : Natural) - → List/fold - { index : Natural, value : a } - kvs - list - ( λ(kvOld : { index : Natural, value : a }) - → λ(z : list) - → let kvNew = - { index = kvOld.index + n - , value = kvOld.value - } - in cons kvNew z - ) - (y.diff (n + length)) - } - ) - { count = +0, diff = λ(_ : Natural) → nil } - in result.diff +0 - ) + let shifted + : ∀(a : Type) + → List (List { index : Natural, value : a }) + → List { index : Natural, value : a } + = λ(a : Type) + → λ(kvss : List (List { index : Natural, value : a })) + → List/build + { index : Natural, value : a } + ( λ(list : Type) + → λ(cons : { index : Natural, value : a } → list → list) + → λ(nil : list) + → let result = + List/fold + (List { index : Natural, value : a }) + kvss + { count : Natural, diff : Natural → list } + ( λ(kvs : List { index : Natural, value : a }) + → λ(y : { count : Natural, diff : Natural → list }) + → let length = + List/length + { index : Natural, value : a } + kvs + + in { count = y.count + length + , diff = + λ(n : Natural) + → List/fold + { index : Natural, value : a } + kvs + list + ( λ ( kvOld + : { index : Natural, value : a } + ) + → λ(z : list) + → let kvNew = + { index = kvOld.index + n + , value = kvOld.value + } + + in cons kvNew z + ) + (y.diff (n + length)) + } + ) + { count = +0, diff = λ(_ : Natural) → nil } + + in result.diff +0 + ) in shifted diff --git a/Prelude/List/unzip b/Prelude/List/unzip --- a/Prelude/List/unzip +++ b/Prelude/List/unzip @@ -20,36 +20,36 @@ = { _1 = [] : List Text, _2 = [] : List Bool } ``` -} -let unzip - : ∀(a : Type) - → ∀(b : Type) - → List { _1 : a, _2 : b } - → { _1 : List a, _2 : List b } - = λ(a : Type) - → λ(b : Type) - → λ(xs : List { _1 : a, _2 : b }) - → { _1 = - List/build - a - ( λ(list : Type) - → λ(cons : a → list → list) - → List/fold - { _1 : a, _2 : b } - xs - list - (λ(x : { _1 : a, _2 : b }) → cons x._1) - ) - , _2 = - List/build - b - ( λ(list : Type) - → λ(cons : b → list → list) - → List/fold - { _1 : a, _2 : b } - xs - list - (λ(x : { _1 : a, _2 : b }) → cons x._2) - ) - } + let unzip + : ∀(a : Type) + → ∀(b : Type) + → List { _1 : a, _2 : b } + → { _1 : List a, _2 : List b } + = λ(a : Type) + → λ(b : Type) + → λ(xs : List { _1 : a, _2 : b }) + → { _1 = + List/build + a + ( λ(list : Type) + → λ(cons : a → list → list) + → List/fold + { _1 : a, _2 : b } + xs + list + (λ(x : { _1 : a, _2 : b }) → cons x._1) + ) + , _2 = + List/build + b + ( λ(list : Type) + → λ(cons : b → list → list) + → List/fold + { _1 : a, _2 : b } + xs + list + (λ(x : { _1 : a, _2 : b }) → cons x._2) + ) + } in unzip diff --git a/Prelude/Monoid b/Prelude/Monoid --- a/Prelude/Monoid +++ b/Prelude/Monoid @@ -36,7 +36,4 @@ : ./Monoid Text ``` -} -let Monoid : ∀(m : Type) → Type - = λ(m : Type) → List m → m - -in Monoid +let Monoid : ∀(m : Type) → Type = λ(m : Type) → List m → m in Monoid diff --git a/Prelude/Natural/build b/Prelude/Natural/build --- a/Prelude/Natural/build +++ b/Prelude/Natural/build @@ -21,13 +21,13 @@ = +0 ``` -} -let build - : ( ∀(natural : Type) - → ∀(succ : natural → natural) - → ∀(zero : natural) - → natural - ) - → Natural - = Natural/build + let build + : ( ∀(natural : Type) + → ∀(succ : natural → natural) + → ∀(zero : natural) + → natural + ) + → Natural + = Natural/build in build diff --git a/Prelude/Natural/enumerate b/Prelude/Natural/enumerate --- a/Prelude/Natural/enumerate +++ b/Prelude/Natural/enumerate @@ -10,29 +10,27 @@ ./enumerate +0 = [] : List Natural ``` -} -let enumerate : Natural → List Natural - = λ(n : Natural) - → List/build - Natural - ( λ(list : Type) - → λ(cons : Natural → list → list) - → List/fold - { index : Natural, value : {} } - ( List/indexed - {} - ( List/build + let enumerate + : Natural → List Natural + = λ(n : Natural) + → List/build + Natural + ( λ(list : Type) + → λ(cons : Natural → list → list) + → List/fold + { index : Natural, value : {} } + ( List/indexed + {} + ( List/build {} ( λ(list : Type) - → λ(cons : {} → list → list) - → Natural/fold - n - list - (cons {=}) + → λ(cons : {} → list → list) + → Natural/fold n list (cons {=}) ) + ) ) + list + (λ(x : { index : Natural, value : {} }) → cons x.index) ) - list - (λ(x : { index : Natural, value : {} }) → cons x.index) - ) in enumerate diff --git a/Prelude/Natural/even b/Prelude/Natural/even --- a/Prelude/Natural/even +++ b/Prelude/Natural/even @@ -9,7 +9,4 @@ ./even +0 = True ``` -} -let even : Natural → Bool - = Natural/even - -in even +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 @@ -22,12 +22,12 @@ → succ (succ (succ zero)) ``` -} -let fold - : Natural - → ∀(natural : Type) - → ∀(succ : natural → natural) - → ∀(zero : natural) - → natural - = Natural/fold + let fold + : Natural + → ∀(natural : Type) + → ∀(succ : natural → natural) + → ∀(zero : natural) + → natural + = Natural/fold in fold diff --git a/Prelude/Natural/isZero b/Prelude/Natural/isZero --- a/Prelude/Natural/isZero +++ b/Prelude/Natural/isZero @@ -9,7 +9,4 @@ ./isZero +0 = True ``` -} -let isZero : Natural → Bool - = Natural/isZero - -in isZero +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 @@ -9,7 +9,4 @@ ./odd +0 = False ``` -} -let odd : Natural → Bool - = Natural/odd - -in odd +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 @@ -9,8 +9,14 @@ ./product ([] : List Natural) = +1 ``` -} -let product : List Natural → Natural - = λ(xs : List Natural) - → List/fold Natural xs Natural (λ(l : Natural) → λ(r : Natural) → l * r) +1 + let product + : List Natural → Natural + = λ(xs : List Natural) + → List/fold + Natural + xs + Natural + (λ(l : Natural) → λ(r : Natural) → l * r) + +1 in product diff --git a/Prelude/Natural/show b/Prelude/Natural/show --- a/Prelude/Natural/show +++ b/Prelude/Natural/show @@ -10,7 +10,4 @@ ./show +0 = "+0" ``` -} -let show : Natural → Text - = Natural/show - -in show +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 @@ -9,8 +9,14 @@ ./sum ([] : List Natural) = +0 ``` -} -let sum : List Natural → Natural - = λ(xs : List Natural) - → List/fold Natural xs Natural (λ(l : Natural) → λ(r : Natural) → l + r) +0 + let sum + : List Natural → Natural + = λ(xs : List Natural) + → List/fold + Natural + xs + Natural + (λ(l : Natural) → λ(r : Natural) → l + r) + +0 in sum diff --git a/Prelude/Natural/toInteger b/Prelude/Natural/toInteger --- a/Prelude/Natural/toInteger +++ b/Prelude/Natural/toInteger @@ -9,7 +9,4 @@ ./toInteger +0 = 0 ``` -} -let toInteger : Natural → Integer - = Natural/toInteger - -in toInteger +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 @@ -10,10 +10,11 @@ ./all Natural Natural/even ([] : Optional Natural) = True ``` -} -let all : ∀(a : Type) → (a → Bool) → Optional a → Bool - = λ(a : Type) - → λ(f : a → Bool) - → λ(xs : Optional a) - → Optional/fold a xs Bool f True + let all + : ∀(a : Type) → (a → Bool) → Optional a → Bool + = λ(a : Type) + → λ(f : a → Bool) + → λ(xs : Optional a) + → Optional/fold a xs Bool f True in all diff --git a/Prelude/Optional/any b/Prelude/Optional/any --- a/Prelude/Optional/any +++ b/Prelude/Optional/any @@ -10,10 +10,11 @@ ./any Natural Natural/even ([] : Optional Natural) = False ``` -} -let any : ∀(a : Type) → (a → Bool) → Optional a → Bool - = λ(a : Type) - → λ(f : a → Bool) - → λ(xs : Optional a) - → Optional/fold a xs Bool f False + let any + : ∀(a : Type) → (a → Bool) → Optional a → Bool + = λ(a : Type) + → λ(f : a → Bool) + → λ(xs : Optional a) + → Optional/fold a xs Bool f False in any diff --git a/Prelude/Optional/build b/Prelude/Optional/build --- a/Prelude/Optional/build +++ b/Prelude/Optional/build @@ -23,14 +23,14 @@ = [] : Optional Integer ``` -} -let build - : ∀(a : Type) - → ( ∀(optional : Type) - → ∀(just : a → optional) - → ∀(nothing : optional) - → optional - ) - → Optional a - = Optional/build + let build + : ∀(a : Type) + → ( ∀(optional : Type) + → ∀(just : a → optional) + → ∀(nothing : optional) + → optional + ) + → Optional a + = Optional/build in build diff --git a/Prelude/Optional/concat b/Prelude/Optional/concat --- a/Prelude/Optional/concat +++ b/Prelude/Optional/concat @@ -14,14 +14,15 @@ = [] : Optional Integer ``` -} -let concat : ∀(a : Type) → Optional (Optional a) → Optional a - = λ(a : Type) - → λ(x : Optional (Optional a)) - → Optional/fold - (Optional a) - x - (Optional a) - (λ(y : Optional a) → y) - ([] : Optional a) + let concat + : ∀(a : Type) → Optional (Optional a) → Optional a + = λ(a : Type) + → λ(x : Optional (Optional a)) + → Optional/fold + (Optional a) + x + (Optional a) + (λ(y : Optional a) → y) + ([] : Optional a) in concat diff --git a/Prelude/Optional/filter b/Prelude/Optional/filter --- a/Prelude/Optional/filter +++ b/Prelude/Optional/filter @@ -11,21 +11,22 @@ = [] : Optional Natural ``` -} -let filter : ∀(a : Type) → (a → Bool) → Optional a -> Optional a - = λ(a : Type) - → λ(f : a → Bool) - → λ(xs : Optional a) - → Optional/build - a - ( λ(optional : Type) - → λ(just : a → optional) - → λ(nil : optional) - → Optional/fold + let filter + : ∀(a : Type) → (a → Bool) → Optional a → Optional a + = λ(a : Type) + → λ(f : a → Bool) + → λ(xs : Optional a) + → Optional/build a - xs - optional - (λ(x : a) → if f x then just x else nil) - nil - ) + ( λ(optional : Type) + → λ(just : a → optional) + → λ(nil : optional) + → Optional/fold + a + xs + optional + (λ(x : a) → if f x then just x else nil) + nil + ) in filter diff --git a/Prelude/Optional/fold b/Prelude/Optional/fold --- a/Prelude/Optional/fold +++ b/Prelude/Optional/fold @@ -9,13 +9,13 @@ ./fold Integer ([] : Optional Integer) Integer (λ(x : Integer) → x) 0 = 0 ``` -} -let fold - : ∀(a : Type) - → Optional a - → ∀(optional : Type) - → ∀(just : a → optional) - → ∀(nothing : optional) - → optional - = Optional/fold + let fold + : ∀(a : Type) + → Optional a + → ∀(optional : Type) + → ∀(just : a → optional) + → ∀(nothing : optional) + → optional + = Optional/fold in fold diff --git a/Prelude/Optional/head b/Prelude/Optional/head --- a/Prelude/Optional/head +++ b/Prelude/Optional/head @@ -20,17 +20,18 @@ = [] : Optional Integer ``` -} -let head : ∀(a : Type) → List (Optional a) → Optional a - = λ(a : Type) - → λ(xs : List (Optional a)) - → List/fold - (Optional a) - xs - (Optional a) - ( λ(l : Optional a) - → λ(r : Optional a) - → Optional/fold a l (Optional a) (λ(x : a) → [x] : Optional a) r - ) - ([] : Optional a) + let head + : ∀(a : Type) → List (Optional a) → Optional a + = λ(a : Type) + → λ(xs : List (Optional a)) + → List/fold + (Optional a) + xs + (Optional a) + ( λ(l : Optional a) + → λ(r : Optional a) + → Optional/fold a l (Optional a) (λ(x : a) → [ x ] : Optional a) r + ) + ([] : Optional a) in head diff --git a/Prelude/Optional/last b/Prelude/Optional/last --- a/Prelude/Optional/last +++ b/Prelude/Optional/last @@ -20,17 +20,18 @@ = [] : Optional Integer ``` -} -let last : ∀(a : Type) → List (Optional a) → Optional a - = λ(a : Type) - → λ(xs : List (Optional a)) - → List/fold - (Optional a) - xs - (Optional a) - ( λ(l : Optional a) - → λ(r : Optional a) - → Optional/fold a r (Optional a) (λ(x : a) → [x] : Optional a) l - ) - ([] : Optional a) + let last + : ∀(a : Type) → List (Optional a) → Optional a + = λ(a : Type) + → λ(xs : List (Optional a)) + → List/fold + (Optional a) + xs + (Optional a) + ( λ(l : Optional a) + → λ(r : Optional a) + → Optional/fold a r (Optional a) (λ(x : a) → [ x ] : Optional a) l + ) + ([] : Optional a) in last diff --git a/Prelude/Optional/length b/Prelude/Optional/length --- a/Prelude/Optional/length +++ b/Prelude/Optional/length @@ -9,9 +9,10 @@ ./length Integer ([] : Optional Integer) = +0 ``` -} -let length : ∀(a : Type) → Optional a → Natural - = λ(a : Type) - → λ(xs : Optional a) - → Optional/fold a xs Natural (λ(_ : a) → +1) +0 + let length + : ∀(a : Type) → Optional a → Natural + = λ(a : Type) + → λ(xs : Optional a) + → 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 @@ -11,16 +11,17 @@ = [] : Optional Bool ``` -} -let map : ∀(a : Type) → ∀(b : Type) → (a → b) → Optional a → Optional b - = λ(a : Type) - → λ(b : Type) - → λ(f : a → b) - → λ(o : Optional a) - → Optional/fold - a - o - (Optional b) - (λ(x : a) → [f x] : Optional b) - ([] : Optional b) + let map + : ∀(a : Type) → ∀(b : Type) → (a → b) → Optional a → Optional b + = λ(a : Type) + → λ(b : Type) + → λ(f : a → b) + → λ(o : Optional a) + → Optional/fold + a + o + (Optional b) + (λ(x : a) → [ f x ] : Optional b) + ([] : Optional b) in map diff --git a/Prelude/Optional/null b/Prelude/Optional/null --- a/Prelude/Optional/null +++ b/Prelude/Optional/null @@ -9,9 +9,10 @@ ./null Integer ([] : Optional Integer) = True ``` -} -let null : ∀(a : Type) → Optional a → Bool - = λ(a : Type) - → λ(xs : Optional a) - → Optional/fold a xs Bool (λ(_ : a) → False) True + let null + : ∀(a : Type) → Optional a → Bool + = λ(a : Type) + → λ(xs : Optional a) + → Optional/fold a xs Bool (λ(_ : a) → False) True in null diff --git a/Prelude/Optional/toList b/Prelude/Optional/toList --- a/Prelude/Optional/toList +++ b/Prelude/Optional/toList @@ -4,14 +4,20 @@ Examples: ``` -./toList Integer ([1] : Optional Integer) = [1] : List Integer +./toList Integer ([1] : Optional Integer) = [1] ./toList Integer ([] : Optional Integer) = [] : List Integer ``` -} -let toList : ∀(a : Type) → Optional a → List a - = λ(a : Type) - → λ(o : Optional a) - → Optional/fold a o (List a) (λ(x : a) → [x] : List a) ([] : List a) + let toList + : ∀(a : Type) → Optional a → List a + = λ(a : Type) + → λ(o : Optional a) + → Optional/fold + a + o + (List a) + (λ(x : a) → ([ x ] : List a)) + ([] : List a) in toList diff --git a/Prelude/Optional/unzip b/Prelude/Optional/unzip --- a/Prelude/Optional/unzip +++ b/Prelude/Optional/unzip @@ -14,28 +14,28 @@ = { _1 = [] : Optional Text, _2 = [] : Optional Bool } ``` -} -let unzip - : ∀(a : Type) - → ∀(b : Type) - → Optional { _1 : a, _2 : b } - → { _1 : Optional a, _2 : Optional b } - = λ(a : Type) - → λ(b : Type) - → λ(xs : Optional { _1 : a, _2 : b }) - → { _1 = - Optional/fold - { _1 : a, _2 : b } - xs - (Optional a) - (λ(x : { _1 : a, _2 : b }) → [x._1] : Optional a) - ([] : Optional a) - , _2 = - Optional/fold - { _1 : a, _2 : b } - xs - (Optional b) - (λ(x : { _1 : a, _2 : b }) → [x._2] : Optional b) - ([] : Optional b) - } + let unzip + : ∀(a : Type) + → ∀(b : Type) + → Optional { _1 : a, _2 : b } + → { _1 : Optional a, _2 : Optional b } + = λ(a : Type) + → λ(b : Type) + → λ(xs : Optional { _1 : a, _2 : b }) + → { _1 = + Optional/fold + { _1 : a, _2 : b } + xs + (Optional a) + (λ(x : { _1 : a, _2 : b }) → [ x._1 ] : Optional a) + ([] : Optional a) + , _2 = + Optional/fold + { _1 : a, _2 : b } + xs + (Optional b) + (λ(x : { _1 : a, _2 : b }) → [ x._2 ] : Optional b) + ([] : Optional b) + } in unzip diff --git a/Prelude/Text/concat b/Prelude/Text/concat --- a/Prelude/Text/concat +++ b/Prelude/Text/concat @@ -9,8 +9,9 @@ ./concat ([] : List Text) = "" ``` -} -let concat : List Text → Text - = λ(xs : List Text) - → List/fold Text xs Text (λ(x : Text) → λ(y : Text) → x ++ y) "" + let concat + : List Text → Text + = λ(xs : List Text) + → List/fold Text xs Text (λ(x : Text) → λ(y : Text) → x ++ y) "" in concat diff --git a/Prelude/Text/concatMap b/Prelude/Text/concatMap --- a/Prelude/Text/concatMap +++ b/Prelude/Text/concatMap @@ -11,10 +11,11 @@ = "" ``` -} -let concatMap : ∀(a : Type) → (a → Text) → List a → Text - = λ(a : Type) - → λ(f : a → Text) - → λ(xs : List a) - → List/fold a xs Text (λ(x : a) → λ(y : Text) → f x ++ y) "" + let concatMap + : ∀(a : Type) → (a → Text) → List a → Text + = λ(a : Type) + → λ(f : a → Text) + → λ(xs : List a) + → List/fold a xs Text (λ(x : a) → λ(y : Text) → f x ++ y) "" in concatMap diff --git a/Prelude/Text/concatMapSep b/Prelude/Text/concatMapSep --- a/Prelude/Text/concatMapSep +++ b/Prelude/Text/concatMapSep @@ -10,38 +10,36 @@ ./concatMapSep ", " Integer Integer/show ([] : List Integer) = "" ``` -} -let concatMapSep - : ∀(separator : Text) → ∀(a : Type) → (a → Text) → List a → Text - = λ(separator : Text) - → λ(a : Type) - → λ(f : a → Text) - → λ(elements : List a) - → let status - = List/fold - a - elements - < Empty : {} | NonEmpty : Text > - ( λ(element : a) - → λ(status : < Empty : {} | NonEmpty : Text >) - → merge - { Empty - = λ(_ : {}) - → < NonEmpty = f element - | Empty : {} - > - , NonEmpty - = λ(result : Text) - → < NonEmpty = f element ++ separator ++ result - | Empty : {} - > - } - status : < Empty : {} | NonEmpty : Text > - ) - < Empty = {=} | NonEmpty : Text > - in merge - { Empty = λ(_ : {}) → "" - , NonEmpty = λ(result : Text) → result - } - status : Text + let concatMapSep + : ∀(separator : Text) → ∀(a : Type) → (a → Text) → List a → Text + = λ(separator : Text) + → λ(a : Type) + → λ(f : a → Text) + → λ(elements : List a) + → let status = + List/fold + a + elements + < Empty : {} | NonEmpty : Text > + ( λ(element : a) + → λ(status : < Empty : {} | NonEmpty : Text >) + → merge + { Empty = + λ(_ : {}) → < NonEmpty = f element | Empty : {} > + , NonEmpty = + λ(result : Text) + → < NonEmpty = f element ++ separator ++ result + | Empty : {} + > + } + status + : < Empty : {} | NonEmpty : Text > + ) + < Empty = {=} | NonEmpty : Text > + + in merge + { Empty = λ(_ : {}) → "", NonEmpty = λ(result : Text) → result } + status + : Text in concatMapSep diff --git a/Prelude/Text/concatSep b/Prelude/Text/concatSep --- a/Prelude/Text/concatSep +++ b/Prelude/Text/concatSep @@ -9,35 +9,34 @@ ./concatSep ", " ([] : List Text) = "" ``` -} -let concatSep : ∀(separator : Text) → ∀(elements : List Text) → Text - = λ(separator : Text) - → λ(elements : List Text) - → let status - = List/fold - Text - elements - < Empty : {} | NonEmpty : Text > - ( λ(element : Text) - → λ(status : < Empty : {} | NonEmpty : Text >) - → merge - { Empty - = λ(_ : {}) - → < NonEmpty = element - | Empty : {} - > - , NonEmpty - = λ(result : Text) - → < NonEmpty = element ++ separator ++ result - | Empty : {} - > - } - status : < Empty : {} | NonEmpty : Text > - ) - < Empty = {=} | NonEmpty : Text > - in merge - { Empty = λ(_ : {}) → "" - , NonEmpty = λ(result : Text) → result - } - status : Text + let concatSep + : ∀(separator : Text) → ∀(elements : List Text) → Text + = λ(separator : Text) + → λ(elements : List Text) + → let status = + List/fold + Text + elements + < Empty : {} | NonEmpty : Text > + ( λ(element : Text) + → λ(status : < Empty : {} | NonEmpty : Text >) + → merge + { Empty = + λ(_ : {}) → < NonEmpty = element | Empty : {} > + , NonEmpty = + λ(result : Text) + → < NonEmpty = element ++ separator ++ result + | Empty : {} + > + } + status + : < Empty : {} | NonEmpty : Text > + ) + < Empty = {=} | NonEmpty : Text > + + in merge + { Empty = λ(_ : {}) → "", NonEmpty = λ(result : Text) → result } + status + : Text in concatSep diff --git a/dhall-format/Main.hs b/dhall-format/Main.hs new file mode 100644 --- /dev/null +++ b/dhall-format/Main.hs @@ -0,0 +1,100 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeOperators #-} + +{-| Utility executable for pretty-printing Dhall code + + You typically want to use this to either: + + * improve the readability of Dhall code (either written or generated) + * automatically format your Dhall code to avoid stylistic debates + + Note that this does not yet support: + + * Preserving all comments + * Currently, this only preserves all leading comments and whitespace + up until the last newline preceding the code + * This lets you preserve a comment header but if you want to document + subexpressions then you will need to split them into a separate + file for now + * Preserving multi-line strings (this reduces them to ordinary strings) + * Preserving string interpolation (this expands interpolation to @++@) + + See the @Dhall.Tutorial@ module for example usage +-} +module Main where + +import Control.Exception (SomeException) +import Control.Monad (when) +import Data.Monoid ((<>)) +import Data.Version (showVersion) +import Dhall.Parser (exprAndHeaderFromText) +import Filesystem.Path.CurrentOS (FilePath) +import Options.Generic (Generic, ParseRecord, type ()(..)) +import Prelude hiding (FilePath) +import System.IO (stderr) +import System.Exit (exitFailure, exitSuccess) +import Text.Trifecta.Delta (Delta(..)) + +import qualified Paths_dhall as Meta + +import qualified Control.Exception +import qualified Data.Text.IO +import qualified Data.Text.Lazy +import qualified Data.Text.Lazy.IO +import qualified Data.Text.Prettyprint.Doc as Pretty +import qualified Data.Text.Prettyprint.Doc.Render.Text as Pretty +import qualified Filesystem.Path.CurrentOS +import qualified Options.Generic +import qualified System.IO + +data Options = Options + { version :: Bool "Display version and exit" + , inplace :: Maybe FilePath "Modify the specified file in-place" + } deriving (Generic) + +instance ParseRecord Options + +opts :: Pretty.LayoutOptions +opts = + Pretty.defaultLayoutOptions + { Pretty.layoutPageWidth = Pretty.AvailablePerLine 80 1.0 } + +main :: IO () +main = do + options <- Options.Generic.getRecord "Formatter for the Dhall language" + when (unHelpful (version options)) $ do + putStrLn (showVersion Meta.version) + exitSuccess + + let handler e = do + let _ = e :: SomeException + System.IO.hPrint stderr e + System.Exit.exitFailure + + Control.Exception.handle handler (do + case unHelpful (inplace options) of + Just file -> do + let fileString = Filesystem.Path.CurrentOS.encodeString file + strictText <- Data.Text.IO.readFile fileString + let lazyText = Data.Text.Lazy.fromStrict strictText + (header, expr) <- case exprAndHeaderFromText (Directed "(stdin)" 0 0 0 0) lazyText of + Left err -> Control.Exception.throwIO err + Right x -> return x + + let doc = Pretty.pretty header <> Pretty.pretty expr + System.IO.withFile fileString System.IO.WriteMode (\handle -> do + Pretty.renderIO handle (Pretty.layoutSmart opts doc) + Data.Text.IO.hPutStrLn handle "" ) + Nothing -> do + inText <- Data.Text.Lazy.IO.getContents + + (header, expr) <- case exprAndHeaderFromText (Directed "(stdin)" 0 0 0 0) inText of + Left err -> Control.Exception.throwIO err + Right x -> return x + + let doc = Pretty.pretty header <> Pretty.pretty expr + Pretty.renderIO System.IO.stdout (Pretty.layoutSmart opts doc) + Data.Text.IO.putStrLn "" ) diff --git a/dhall.cabal b/dhall.cabal --- a/dhall.cabal +++ b/dhall.cabal @@ -1,5 +1,5 @@ Name: dhall -Version: 1.6.0 +Version: 1.7.0 Cabal-Version: >=1.8.0.2 Build-Type: Simple Tested-With: GHC == 8.0.1 @@ -81,6 +81,8 @@ Prelude/Text/concatMap Prelude/Text/concatMapSep Prelude/Text/concatSep + tests/parser/*.dhall + tests/regression/*.dhall Source-Repository head Type: git @@ -101,6 +103,7 @@ http-client-tls >= 0.2.0 && < 0.4 , lens >= 2.4 && < 4.16, parsers >= 0.12.4 && < 0.13, + prettyprinter >= 1.1.1 && < 1.2 , system-filepath >= 0.3.1 && < 0.5 , system-fileio >= 0.2.1 && < 0.4 , text >= 0.11.1.0 && < 1.3 , @@ -120,7 +123,7 @@ GHC-Options: -Wall Executable dhall - Hs-Source-Dirs: exec + Hs-Source-Dirs: dhall Main-Is: Main.hs Build-Depends: base >= 4 && < 5 , @@ -132,6 +135,21 @@ Other-Modules: Paths_dhall +Executable dhall-format + Hs-Source-Dirs: dhall-format + Main-Is: Main.hs + Build-Depends: + base >= 4 && < 5 , + dhall , + optparse-generic >= 1.1.1 && < 1.3, + prettyprinter >= 1.1.1 && < 1.2, + system-filepath >= 0.3.1 && < 0.5, + trifecta >= 1.6 && < 1.8, + text >= 0.11.1.0 && < 1.3 + GHC-Options: -Wall + Other-Modules: + Paths_dhall + Test-Suite test Type: exitcode-stdio-1.0 Hs-Source-Dirs: tests @@ -140,6 +158,7 @@ Other-Modules: Examples Normalization + Parser Regression Tutorial Util diff --git a/dhall/Main.hs b/dhall/Main.hs new file mode 100644 --- /dev/null +++ b/dhall/Main.hs @@ -0,0 +1,85 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeOperators #-} + +module Main where + +import Control.Exception (SomeException) +import Control.Monad (when) +import Data.Monoid (mempty) +import Data.Version (showVersion) +import Dhall.Core (pretty, normalize) +import Dhall.Import (Imported(..), load) +import Dhall.Parser (Src, exprFromText) +import Dhall.TypeCheck (DetailedTypeError(..), TypeError) +import Options.Generic (Generic, ParseRecord, type ()(..)) +import System.IO (stderr) +import System.Exit (exitFailure, exitSuccess) +import Text.Trifecta.Delta (Delta(..)) + +import qualified Paths_dhall as Meta + +import qualified Control.Exception +import qualified Data.Text.Lazy.IO +import qualified Dhall.TypeCheck +import qualified Options.Generic +import qualified System.IO + +data Options = Options + { explain :: Bool "Explain error messages in more detail" + , version :: Bool "Display version and exit" + } deriving (Generic) + +instance ParseRecord Options + +main :: IO () +main = do + options <- Options.Generic.getRecord "Compiler for the Dhall language" + when (unHelpful (version options)) $ do + putStrLn (showVersion Meta.version) + exitSuccess + let handle = + Control.Exception.handle handler2 + . Control.Exception.handle handler1 + . Control.Exception.handle handler0 + where + handler0 e = do + let _ = e :: TypeError Src + System.IO.hPutStrLn stderr "" + if unHelpful (explain options) + then Control.Exception.throwIO (DetailedTypeError e) + else do + Data.Text.Lazy.IO.hPutStrLn stderr "\ESC[2mUse \"dhall --explain\" for detailed errors\ESC[0m" + Control.Exception.throwIO e + + handler1 (Imported ps e) = do + let _ = e :: TypeError Src + System.IO.hPutStrLn stderr "" + if unHelpful (explain options) + then Control.Exception.throwIO (Imported ps (DetailedTypeError e)) + else do + Data.Text.Lazy.IO.hPutStrLn stderr "\ESC[2mUse \"dhall --explain\" for detailed errors\ESC[0m" + Control.Exception.throwIO (Imported ps e) + + handler2 e = do + let _ = e :: SomeException + System.IO.hPrint stderr e + System.Exit.exitFailure + + handle (do + inText <- Data.Text.Lazy.IO.getContents + + expr <- case exprFromText (Directed "(stdin)" 0 0 0 0) inText of + Left err -> Control.Exception.throwIO err + Right expr -> return expr + + expr' <- load expr + + typeExpr <- case Dhall.TypeCheck.typeOf expr' of + Left err -> Control.Exception.throwIO err + Right typeExpr -> return typeExpr + Data.Text.Lazy.IO.hPutStrLn stderr (pretty (normalize typeExpr)) + Data.Text.Lazy.IO.hPutStrLn stderr mempty + Data.Text.Lazy.IO.putStrLn (pretty (normalize expr')) ) diff --git a/exec/Main.hs b/exec/Main.hs deleted file mode 100644 --- a/exec/Main.hs +++ /dev/null @@ -1,87 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE ExplicitNamespaces #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE TypeOperators #-} - -module Main where - -import Control.Exception (SomeException) -import Control.Monad (when) -import Data.Monoid (mempty) -import Data.Version (showVersion) -import Dhall.Core (pretty, normalize) -import Dhall.Import (Imported(..), load) -import Dhall.Parser (Src, exprFromText) -import Dhall.TypeCheck (DetailedTypeError(..), TypeError) -import Options.Generic (Generic, ParseRecord, type ()(..)) -import System.IO (stderr) -import System.Exit (exitFailure, exitSuccess) -import Text.Trifecta.Delta (Delta(..)) - -import qualified Paths_dhall as Meta - -import qualified Control.Exception -import qualified Data.Text.Lazy.IO -import qualified Dhall.TypeCheck -import qualified Options.Generic -import qualified System.IO - -data Mode = Default | Resolve | TypeCheck | Normalize - -data Options = Options - { explain :: Bool "Explain error messages in more detail" - , version :: Bool "Display version and exit" - } deriving (Generic) - -instance ParseRecord Options - -main :: IO () -main = do - options <- Options.Generic.getRecord "Compiler for the Dhall language" - when (unHelpful (version options)) $ do - putStrLn (showVersion Meta.version) - exitSuccess - let handle = - Control.Exception.handle handler2 - . Control.Exception.handle handler1 - . Control.Exception.handle handler0 - where - handler0 e = do - let _ = e :: TypeError Src - System.IO.hPutStrLn stderr "" - if unHelpful (explain options) - then Control.Exception.throwIO (DetailedTypeError e) - else do - Data.Text.Lazy.IO.hPutStrLn stderr "\ESC[2mUse \"dhall --explain\" for detailed errors\ESC[0m" - Control.Exception.throwIO e - - handler1 (Imported ps e) = do - let _ = e :: TypeError Src - System.IO.hPutStrLn stderr "" - if unHelpful (explain options) - then Control.Exception.throwIO (Imported ps (DetailedTypeError e)) - else do - Data.Text.Lazy.IO.hPutStrLn stderr "\ESC[2mUse \"dhall --explain\" for detailed errors\ESC[0m" - Control.Exception.throwIO (Imported ps e) - - handler2 e = do - let _ = e :: SomeException - System.IO.hPrint stderr e - System.Exit.exitFailure - - handle (do - inText <- Data.Text.Lazy.IO.getContents - - expr <- case exprFromText (Directed "(stdin)" 0 0 0 0) inText of - Left err -> Control.Exception.throwIO err - Right expr -> return expr - - expr' <- load expr - - typeExpr <- case Dhall.TypeCheck.typeOf expr' of - Left err -> Control.Exception.throwIO err - Right typeExpr -> return typeExpr - Data.Text.Lazy.IO.hPutStrLn stderr (pretty (normalize typeExpr)) - Data.Text.Lazy.IO.hPutStrLn stderr mempty - Data.Text.Lazy.IO.putStrLn (pretty (normalize expr')) ) diff --git a/src/Dhall.hs b/src/Dhall.hs --- a/src/Dhall.hs +++ b/src/Dhall.hs @@ -760,6 +760,13 @@ declared = Double +instance Inject () where + injectWith _ = InputType {..} + where + embed = const (RecordLit Data.Map.empty) + + declared = Record Data.Map.empty + instance Inject a => Inject (Maybe a) where injectWith options = InputType embedOut declaredOut where diff --git a/src/Dhall/Core.hs b/src/Dhall/Core.hs --- a/src/Dhall/Core.hs +++ b/src/Dhall/Core.hs @@ -55,6 +55,7 @@ import Data.Text.Buildable (Buildable(..)) import Data.Text.Lazy (Text) import Data.Text.Lazy.Builder (Builder) +import Data.Text.Prettyprint.Doc (Doc, Pretty) import Data.Traversable import Data.Vector (Vector) import Filesystem.Path.CurrentOS (FilePath) @@ -62,12 +63,15 @@ import Prelude hiding (FilePath, succ) import qualified Control.Monad +import qualified Data.Char import qualified Data.HashSet +import qualified Data.List import qualified Data.Map import qualified Data.Maybe 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.Vector import qualified Data.Vector.Mutable import qualified Filesystem.Path.CurrentOS as Filesystem @@ -141,6 +145,9 @@ RawText -> "as Text" Code -> "" +instance Pretty Path where + pretty path = Pretty.pretty (Builder.toLazyText (build path)) + {-| Label for a bound variable The `Text` field is the variable's name (i.e. \"@x@\"). @@ -451,6 +458,557 @@ case the corresponding builder. -} +{-| Internal utility for pretty-printing, used when generating element lists + to supply to `enclose` or `enclose'`. This utility indicates that the + compact represent is the same as the multi-line representation for each + element +-} +duplicate :: a -> (a, a) +duplicate x = (x, x) + +-- | Pretty-print a list +list :: [Doc ann] -> Doc ann +list [] = "[]" +list docs = enclose "[ " "[ " ", " ", " " ]" "]" (fmap duplicate docs) + +-- | Pretty-print union types and literals +angles :: [(Doc ann, Doc ann)] -> Doc ann +angles [] = "<>" +angles docs = enclose "< " "< " " | " "| " " >" ">" docs + +-- | Pretty-print record types and literals +braces :: [(Doc ann, Doc ann)] -> Doc ann +braces [] = "{}" +braces docs = enclose "{ " "{ " ", " ", " " }" "}" docs + +-- | Pretty-print anonymous functions and function types +arrows :: [(Doc ann, Doc ann)] -> Doc ann +arrows = enclose' "" " " " → " "→ " + +{-| Format an expression that holds a variable number of elements, such as a + list, record, or union +-} +enclose + :: Doc ann + -- ^ Beginning document for compact representation + -> Doc ann + -- ^ Beginning document for multi-line representation + -> Doc ann + -- ^ Separator for compact representation + -> Doc ann + -- ^ Separator for multi-line representation + -> Doc ann + -- ^ Ending document for compact representation + -> Doc ann + -- ^ Ending document for multi-line representation + -> [(Doc ann, Doc ann)] + -- ^ Elements to format, each of which is a pair: @(compact, multi-line)@ + -> Doc ann +enclose beginShort _ _ _ endShort _ [] = + beginShort <> endShort + where +enclose beginShort beginLong sepShort sepLong endShort endLong docs = + Pretty.group + (Pretty.flatAlt + (Pretty.align + (mconcat (zipWith combineLong (beginLong : repeat sepLong) docsLong) <> endLong) + ) + (mconcat (zipWith combineShort (beginShort : repeat sepShort) docsShort) <> endShort) + ) + where + docsShort = fmap fst docs + + docsLong = fmap snd docs + + combineLong x y = x <> y <> Pretty.hardline + + combineShort x y = x <> y + +{-| Format an expression that holds a variable number of elements without a + trailing document such as nested `let`, nested lambdas, or nested `forall`s +-} +enclose' + :: Doc ann + -- ^ Beginning document for compact representation + -> Doc ann + -- ^ Beginning document for multi-line representation + -> Doc ann + -- ^ Separator for compact representation + -> Doc ann + -- ^ Separator for multi-line representation + -> [(Doc ann, Doc ann)] + -- ^ Elements to format, each of which is a pair: @(compact, multi-line)@ + -> Doc ann +enclose' beginShort beginLong sepShort sepLong docs = + Pretty.group (Pretty.flatAlt long short) + where + longLines = zipWith (<>) (beginLong : repeat sepLong) docsLong + + long = + Pretty.align (mconcat (Data.List.intersperse Pretty.hardline longLines)) + + short = mconcat (zipWith (<>) (beginShort : repeat sepShort) docsShort) + + docsShort = fmap fst docs + + docsLong = fmap snd docs + +prettyLabel :: Text -> Doc ann +prettyLabel a = + if Data.HashSet.member a reservedIdentifiers + then "`" <> Pretty.pretty a <> "`" + else Pretty.pretty a + +prettyNumber :: Integer -> Doc ann +prettyNumber = Pretty.pretty + +prettyNatural :: Natural -> Doc ann +prettyNatural = Pretty.pretty + +prettyDouble :: Double -> Doc ann +prettyDouble = Pretty.pretty + +prettyText :: Builder -> Doc ann +prettyText a = Pretty.pretty (Builder.toLazyText (buildText a)) + +prettyConst :: Const -> Doc ann +prettyConst Type = "Type" +prettyConst Kind = "Kind" + +prettyVar :: Var -> Doc ann +prettyVar (V x 0) = prettyLabel x +prettyVar (V x n) = prettyLabel x <> "@" <> prettyNumber n + +prettyExprA :: Pretty a => Expr s a -> Doc ann +prettyExprA a0@(Annot _ _) = + enclose' "" " " " : " ": " (fmap duplicate (docs a0)) + where + docs (Annot a b) = prettyExprB a : docs b + docs (Note _ b) = docs b + docs b = [ prettyExprB b ] +prettyExprA a0 = prettyExprB a0 + +prettyExprB :: Pretty a => Expr s a -> Doc ann +prettyExprB a0@(Lam _ _ _) = arrows (fmap duplicate (docs a0)) + where + docs (Lam a b c) = Pretty.group (Pretty.flatAlt long short) : docs c + where + long = "λ " + <> Pretty.align + ( "( " + <> prettyLabel a + <> Pretty.hardline + <> ": " + <> prettyExprA b + <> Pretty.hardline + <> ")" + ) + + short = "λ(" + <> prettyLabel a + <> " : " + <> prettyExprA b + <> ")" + docs (Note _ c) = docs c + docs c = [ prettyExprB c ] +prettyExprB a0@(BoolIf _ _ _) = + enclose' "" " " " else " (Pretty.hardline <> "else ") (fmap duplicate (docs a0)) + where + docs (BoolIf a b c) = + Pretty.group (Pretty.flatAlt long short) : docs c + where + long = + Pretty.align + ( "if " + <> prettyExprA a + <> Pretty.hardline + <> "then " + <> prettyExprA b + ) + + short = "if " + <> prettyExprA a + <> " then " + <> prettyExprA b + docs (Note _ c) = docs c + docs c = [ prettyExprB c ] +prettyExprB a0@(Pi _ _ _) = + arrows (fmap duplicate (docs a0)) + where + docs (Pi "_" b c) = prettyExprC b : docs c + docs (Pi a b c) = Pretty.group (Pretty.flatAlt long short) : docs c + where + long = "∀ " + <> Pretty.align + ( "( " + <> prettyLabel a + <> Pretty.hardline + <> ": " + <> prettyExprA b + <> Pretty.hardline + <> ")" + ) + + short = "∀(" + <> prettyLabel a + <> " : " + <> prettyExprA b + <> ")" + docs (Note _ c) = docs c + docs c = [ prettyExprB c ] +prettyExprB a0@(Let _ _ _ _) = + enclose' "" " " " in " (Pretty.hardline <> "in ") + (fmap duplicate (docs a0)) + where + docs (Let a Nothing c d) = + Pretty.group (Pretty.flatAlt long short) : docs d + where + long = "let " + <> Pretty.align + ( prettyLabel a + <> " =" + <> Pretty.hardline + <> " " + <> prettyExprA c + ) + + short = "let " + <> prettyLabel a + <> " = " + <> prettyExprA c + docs (Let a (Just b) c d) = + Pretty.group (Pretty.flatAlt long short) : docs d + where + long = "let " + <> Pretty.align + ( prettyLabel a + <> Pretty.hardline + <> ": " + <> prettyExprA b + <> Pretty.hardline + <> "= " + <> prettyExprA c + ) + + short = "let " + <> prettyLabel a + <> " : " + <> prettyExprA b + <> " = " + <> prettyExprA c + docs (Note _ d) = + docs d + docs d = + [ prettyExprB d ] +prettyExprB (ListLit Nothing b) = + list (map prettyExprA (Data.Vector.toList b)) +prettyExprB (ListLit (Just a) b) = + list (map prettyExprA (Data.Vector.toList b)) + <> " : " + <> prettyExprD (App List a) +prettyExprB (OptionalLit a b) = + list (map prettyExprA (Data.Vector.toList b)) + <> " : " + <> prettyExprD (App Optional a) +prettyExprB (Merge a b (Just c)) = + Pretty.group (Pretty.flatAlt long short) + where + long = + Pretty.align + ( "merge" + <> Pretty.hardline + <> prettyExprE a + <> Pretty.hardline + <> prettyExprE b + <> Pretty.hardline + <> ": " + <> prettyExprD c + ) + + short = "merge " + <> prettyExprE a + <> " " + <> prettyExprE b + <> " : " + <> prettyExprD c +prettyExprB (Merge a b Nothing) = + Pretty.group (Pretty.flatAlt long short) + where + long = + Pretty.align + ( "merge" + <> Pretty.hardline + <> prettyExprE a + <> Pretty.hardline + <> prettyExprE b + ) + + short = "merge " + <> prettyExprE a + <> " " + <> prettyExprE b +prettyExprB (Note _ b) = + prettyExprB b +prettyExprB a = + prettyExprC a + +prettyExprC :: Pretty a => Expr s a -> Doc ann +prettyExprC = prettyExprC0 + +prettyExprC0 :: Pretty a => Expr s a -> Doc ann +prettyExprC0 a0@(BoolOr _ _) = + enclose' "" " " " || " "|| " (fmap duplicate (docs a0)) + where + docs (BoolOr a b) = prettyExprC1 a : docs b + docs (Note _ b) = docs b + docs b = [ prettyExprC1 b ] +prettyExprC0 a0 = + prettyExprC1 a0 + +prettyExprC1 :: Pretty a => Expr s a -> Doc ann +prettyExprC1 a0@(TextAppend _ _) = + enclose' "" " " " ++ " "++ " (fmap duplicate (docs a0)) + where + docs (TextAppend a b) = prettyExprC2 a : docs b + docs (Note _ b) = docs b + docs b = [ prettyExprC2 b ] +prettyExprC1 a0 = + prettyExprC2 a0 + +prettyExprC2 :: Pretty a => Expr s a -> Doc ann +prettyExprC2 a0@(NaturalPlus _ _) = + enclose' "" " " " + " "+ " (fmap duplicate (docs a0)) + where + docs (NaturalPlus a b) = prettyExprC3 a : docs b + docs (Note _ b) = docs b + docs b = [ prettyExprC3 b ] +prettyExprC2 a0 = + prettyExprC3 a0 + +prettyExprC3 :: Pretty a => Expr s a -> Doc ann +prettyExprC3 a0@(ListAppend _ _) = + enclose' "" " " " # " "# " (fmap duplicate (docs a0)) + where + docs (ListAppend a b) = prettyExprC4 a : docs b + docs (Note _ b) = docs b + docs b = [ prettyExprC4 b ] +prettyExprC3 a0 = + prettyExprC4 a0 + +prettyExprC4 :: Pretty a => Expr s a -> Doc ann +prettyExprC4 a0@(BoolAnd _ _) = + enclose' "" " " " && " "&& " (fmap duplicate (docs a0)) + where + docs (BoolAnd a b) = prettyExprC5 a : docs b + docs (Note _ b) = docs b + docs b = [ prettyExprC5 b ] +prettyExprC4 a0 = + prettyExprC5 a0 + +prettyExprC5 :: Pretty a => Expr s a -> Doc ann +prettyExprC5 a0@(Combine _ _) = + enclose' "" " " " ∧ " "∧ " (fmap duplicate (docs a0)) + where + docs (Combine a b) = prettyExprC6 a : docs b + docs (Note _ b) = docs b + docs b = [ prettyExprC6 b ] +prettyExprC5 a0 = + prettyExprC6 a0 + +prettyExprC6 :: Pretty a => Expr s a -> Doc ann +prettyExprC6 a0@(Prefer _ _) = + enclose' "" " " " ⫽ " "⫽ " (fmap duplicate (docs a0)) + where + docs (Prefer a b) = prettyExprC7 a : docs b + docs (Note _ b) = docs b + docs b = [ prettyExprC7 b ] +prettyExprC6 a0 = + prettyExprC7 a0 + +prettyExprC7 :: Pretty a => Expr s a -> Doc ann +prettyExprC7 a0@(NaturalTimes _ _) = + enclose' "" " " " * " "* " (fmap duplicate (docs a0)) + where + docs (NaturalTimes a b) = prettyExprC8 a : docs b + docs (Note _ b) = docs b + docs b = [ prettyExprC8 b ] +prettyExprC7 a0 = + prettyExprC8 a0 + +prettyExprC8 :: Pretty a => Expr s a -> Doc ann +prettyExprC8 a0@(BoolEQ _ _) = + enclose' "" " " " == " "== " (fmap duplicate (docs a0)) + where + docs (BoolEQ a b) = prettyExprC9 a : docs b + docs (Note _ b) = docs b + docs b = [ prettyExprC9 b ] +prettyExprC8 a0 = + prettyExprC9 a0 + +prettyExprC9 :: Pretty a => Expr s a -> Doc ann +prettyExprC9 a0@(BoolNE _ _) = + enclose' "" " " " != " "!= " (fmap duplicate (docs a0)) + where + docs (BoolNE a b) = prettyExprD a : docs b + docs (Note _ b) = docs b + docs b = [ prettyExprD b ] +prettyExprC9 a0 = + prettyExprD a0 + +prettyExprD :: Pretty a => Expr s a -> Doc ann +prettyExprD a0@(App _ _) = + enclose' "" "" " " "" (fmap duplicate (reverse (docs a0))) + where + docs (App a b) = prettyExprE b : docs a + docs (Note _ b) = docs b + docs b = [ prettyExprE b ] +prettyExprD (Note _ b) = prettyExprD b +prettyExprD a0 = + prettyExprE a0 + +prettyExprE :: Pretty a => Expr s a -> Doc ann +prettyExprE (Field a b) = prettyExprE a <> "." <> prettyLabel b +prettyExprE (Note _ b) = prettyExprE b +prettyExprE a = prettyExprF a + +prettyExprF :: Pretty a => Expr s a -> Doc ann +prettyExprF (Var a) = + prettyVar a +prettyExprF (Const k) = + prettyConst k +prettyExprF Bool = + "Bool" +prettyExprF Natural = + "Natural" +prettyExprF NaturalFold = + "Natural/fold" +prettyExprF NaturalBuild = + "Natural/build" +prettyExprF NaturalIsZero = + "Natural/isZero" +prettyExprF NaturalEven = + "Natural/even" +prettyExprF NaturalOdd = + "Natural/odd" +prettyExprF NaturalToInteger = + "Natural/toInteger" +prettyExprF NaturalShow = + "Natural/show" +prettyExprF Integer = + "Integer" +prettyExprF IntegerShow = + "Integer/show" +prettyExprF Double = + "Double" +prettyExprF DoubleShow = + "Double/show" +prettyExprF Text = + "Text" +prettyExprF List = + "List" +prettyExprF ListBuild = + "List/build" +prettyExprF ListFold = + "List/fold" +prettyExprF ListLength = + "List/length" +prettyExprF ListHead = + "List/head" +prettyExprF ListLast = + "List/last" +prettyExprF ListIndexed = + "List/indexed" +prettyExprF ListReverse = + "List/reverse" +prettyExprF Optional = + "Optional" +prettyExprF OptionalFold = + "Optional/fold" +prettyExprF OptionalBuild = + "Optional/build" +prettyExprF (BoolLit True) = + "True" +prettyExprF (BoolLit False) = + "False" +prettyExprF (IntegerLit a) = + prettyNumber a +prettyExprF (NaturalLit a) = + "+" <> prettyNatural a +prettyExprF (DoubleLit a) = + prettyDouble a +prettyExprF (TextLit a) = + prettyText a +prettyExprF (Record a) = + prettyRecord a +prettyExprF (RecordLit a) = + prettyRecordLit a +prettyExprF (Union a) = + prettyUnion a +prettyExprF (UnionLit a b c) = + prettyUnionLit a b c +prettyExprF (ListLit Nothing b) = + list (map prettyExprA (Data.Vector.toList b)) +prettyExprF (Embed a) = + Pretty.pretty a +prettyExprF (Note _ b) = + prettyExprF b +prettyExprF a = + Pretty.group (Pretty.flatAlt long short) + where + long = Pretty.align ("( " <> prettyExprA a <> Pretty.hardline <> ")") + + short = "(" <> prettyExprA a <> ")" + +prettyKeyValue + :: Pretty a + => Doc ann + -> Int + -> (Text, Expr s a) + -> (Doc ann, Doc ann) +prettyKeyValue separator keyLength (key, value) = + ( prettyLabel key <> " " <> separator <> " " <> prettyExprA value + , Pretty.fill keyLength (prettyLabel key) + <> " " + <> separator + <> Pretty.group (Pretty.flatAlt long short) + ) + where + long = Pretty.hardline <> " " <> prettyExprA value + + short = " " <> prettyExprA value + +prettyRecord :: Pretty a => Map Text (Expr s a) -> Doc ann +prettyRecord a = braces (map adapt (Data.Map.toList a)) + where + keyLength = fromIntegral (maximum (map Text.length (Data.Map.keys a))) + + adapt = prettyKeyValue ":" keyLength + +prettyRecordLit :: Pretty a => Map Text (Expr s a) -> Doc ann +prettyRecordLit a + | Data.Map.null a = "{=}" + | otherwise = braces (map adapt (Data.Map.toList a)) + where + keyLength = fromIntegral (maximum (map Text.length (Data.Map.keys a))) + + adapt = prettyKeyValue "=" keyLength + +prettyUnion :: Pretty a => Map Text (Expr s a) -> Doc ann +prettyUnion a = angles (map adapt (Data.Map.toList a)) + where + keyLength = fromIntegral (maximum (map Text.length (Data.Map.keys a))) + + adapt = prettyKeyValue ":" keyLength + +prettyUnionLit :: Pretty a => Text -> Expr s a -> Map Text (Expr s a) -> Doc ann +prettyUnionLit a b c = angles (front : map adapt (Data.Map.toList c)) + where + keyLength = fromIntegral (maximum (map Text.length (a : Data.Map.keys c))) + + front = prettyKeyValue "=" keyLength (a, b) + + adapt = prettyKeyValue ":" keyLength + -- | Pretty-print a value pretty :: Buildable a => a -> Text pretty = Builder.toLazyText . build @@ -458,7 +1016,7 @@ -- | Builder corresponding to the @label@ token in "Dhall.Parser" buildLabel :: Text -> Builder buildLabel label = - if Data.HashSet.member label reservedIdentifiersText + if Data.HashSet.member label reservedIdentifiers then "`" <> build label <> "`" else build label @@ -476,8 +1034,34 @@ -- | Builder corresponding to the @text@ token in "Dhall.Parser" buildText :: Builder -> Builder -buildText a = build (show a) +buildText a = "\"" <> Builder.fromLazyText (Text.concatMap adapt text) <> "\"" + where + adapt c + | '\x20' <= c && c <= '\x21' = Text.singleton c + | '\x23' <= c && c <= '\x5B' = Text.singleton c + | '\x5D' <= c && c <= '\x7F' = Text.singleton c + | c == '"' = "\\\"" + | c == '$' = "\\$" + | c == '\\' = "\\\\" + | c == '\b' = "\\b" + | c == '\f' = "\\f" + | c == '\n' = "\\n" + | c == '\r' = "\\r" + | c == '\t' = "\\t" + | otherwise = "\\u" <> showDigits (Data.Char.ord c) + showDigits r0 = Text.pack (map showDigit [q1, q2, q3, r3]) + where + (q1, r1) = r0 `quotRem` 4096 + (q2, r2) = r1 `quotRem` 256 + (q3, r3) = r2 `quotRem` 16 + + showDigit n + | n < 10 = Data.Char.chr (Data.Char.ord '0' + n) + | otherwise = Data.Char.chr (Data.Char.ord 'A' + n - 10) + + text = Builder.toLazyText a + -- | Builder corresponding to the @expr@ parser in "Dhall.Parser" buildExpr :: Buildable a => Expr s a -> Builder buildExpr = buildExprA @@ -501,9 +1085,9 @@ "if " <> buildExprA a <> " then " - <> buildExprB b + <> buildExprA b <> " else " - <> buildExprC c + <> buildExprA c buildExprB (Pi "_" b c) = buildExprC b <> " → " @@ -797,10 +1381,12 @@ <> " >" -- | Generates a syntactically valid Dhall program -instance Buildable a => Buildable (Expr s a) - where +instance Buildable a => Buildable (Expr s a) where build = buildExpr +instance Pretty a => Pretty (Expr s a) where + pretty = prettyExprA + {-| `shift` is used by both normalization and type-checking to avoid variable capture by shifting variable indices @@ -1153,7 +1739,28 @@ normalize :: Expr s a -> Expr t a normalize = normalizeWith (const Nothing) +{-| This function is used to determine whether folds like @Natural/fold@ or + @List/fold@ should be lazy or strict in their accumulator based on the type + of the accumulator + If this function returns `True`, then they will be strict in their + accumulator since we can guarantee an upper bound on the amount of work to + normalize the accumulator on each step of the loop. If this function + returns `False` then they will be lazy in their accumulator and only + normalize the final result at the end of the fold +-} +boundedType :: Expr s a -> Bool +boundedType Bool = True +boundedType Natural = True +boundedType Integer = True +boundedType Double = True +boundedType Text = True +boundedType (App List _) = False +boundedType (App Optional t) = boundedType t +boundedType (Record kvs) = all boundedType kvs +boundedType (Union kvs) = all boundedType kvs +boundedType _ = False + {-| Reduce an expression to its normal form, performing beta reduction and applying any custom definitions. @@ -1209,11 +1816,17 @@ App (App OptionalBuild _) (App (App OptionalFold _) e') -> loop e' App (App OptionalFold _) (App (App OptionalBuild _) e') -> loop e' - App (App (App (App NaturalFold (NaturalLit n0)) _) succ') zero -> - loop (go n0) + App (App (App (App NaturalFold (NaturalLit n0)) t) succ') zero -> + if boundedType (loop t) then strict else lazy where - go !0 = zero - go !n = App succ' (go (n - 1)) + strict = strictLoop n0 + lazy = loop ( lazyLoop n0) + + strictLoop !0 = loop zero + strictLoop !n = loop (App succ' (strictLoop (n - 1))) + + lazyLoop !0 = zero + lazyLoop !n = App succ' (lazyLoop (n - 1)) App NaturalBuild k | check -> NaturalLit n | otherwise -> App f' a' @@ -1271,10 +1884,17 @@ go (App (App (Var "Cons") _) e') = go e' go (Var "Nil") = True go _ = False - App (App (App (App (App ListFold _) (ListLit _ xs)) _) cons) nil -> - loop (Data.Vector.foldr cons' nil xs) + App (App (App (App (App ListFold _) (ListLit _ xs)) t) cons) nil -> + if boundedType (loop t) then strict else lazy where - cons' y ys = App (App cons y) ys + strict = Data.Vector.foldr strictCons strictNil xs + lazy = loop (Data.Vector.foldr lazyCons lazyNil xs) + + strictNil = loop nil + lazyNil = nil + + strictCons y ys = loop (App (App cons y) ys) + lazyCons y ys = App (App cons y) ys App (App ListLength _) (ListLit _ ys) -> NaturalLit (fromIntegral (Data.Vector.length ys)) App (App ListHead t) (ListLit _ ys) -> @@ -1751,7 +2371,7 @@ return (Data.Vector.Mutable.slice 0 len mv) )) -- | The set of reserved identifiers for the Dhall language -reservedIdentifiers :: HashSet String +reservedIdentifiers :: HashSet Text reservedIdentifiers = Data.HashSet.fromList [ "let" @@ -1792,6 +2412,3 @@ , "Optional" , "Optional/fold" ] - -reservedIdentifiersText :: HashSet Text -reservedIdentifiersText = Data.HashSet.map Text.pack reservedIdentifiers diff --git a/src/Dhall/Parser.hs b/src/Dhall/Parser.hs --- a/src/Dhall/Parser.hs +++ b/src/Dhall/Parser.hs @@ -8,949 +8,1548 @@ module Dhall.Parser ( -- * Utilities exprFromText - - -- * Parsers - , expr, exprA - - -- * Types - , Src(..) - , ParseError(..) - , Parser(..) - ) where - -import Control.Applicative (Alternative(..), optional) -import Control.Exception (Exception) -import Control.Monad (MonadPlus) -import Data.ByteString (ByteString) -import Data.CharSet (CharSet) -import Data.Map (Map) -import Data.Monoid ((<>)) -import Data.Sequence (ViewL(..)) -import Data.Text.Buildable (Buildable(..)) -import Data.Text.Lazy (Text) -import Data.Typeable (Typeable) -import Data.Vector (Vector) -import Dhall.Core -import Prelude hiding (const, pi) -import Text.PrettyPrint.ANSI.Leijen (Doc) -import Text.Parser.Combinators (choice, try, ()) -import Text.Parser.Token (IdentifierStyle(..), TokenParsing(..)) -import Text.Parser.Token.Highlight (Highlight(..)) -import Text.Trifecta - (CharParsing, DeltaParsing, MarkParsing, Parsing, Result(..)) -import Text.Trifecta.Delta (Delta) - -import qualified Data.Char -import qualified Data.CharSet -import qualified Data.Map -import qualified Data.ByteString.Lazy -import qualified Data.List -import qualified Data.Sequence -import qualified Data.Text.Lazy -import qualified Data.Text.Lazy.Builder -import qualified Data.Text.Lazy.Encoding -import qualified Data.Vector -import qualified Filesystem.Path.CurrentOS -import qualified Text.Parser.Char -import qualified Text.Parser.Combinators -import qualified Text.Parser.Token -import qualified Text.Parser.Token.Style -import qualified Text.PrettyPrint.ANSI.Leijen -import qualified Text.Trifecta - --- | Source code extract -data Src = Src Delta Delta ByteString deriving (Eq, Show) - -instance Buildable Src where - build (Src begin _ bytes) = - build text <> "\n" - <> "\n" - <> build (show (Text.PrettyPrint.ANSI.Leijen.pretty begin)) - <> "\n" - where - bytes' = Data.ByteString.Lazy.fromStrict bytes - - text = Data.Text.Lazy.strip (Data.Text.Lazy.Encoding.decodeUtf8 bytes') - -{-| A `Parser` that is almost identical to - @"Text.Trifecta".`Text.Trifecta.Parser`@ except treating Haskell-style - comments as whitespace --} -newtype Parser a = Parser { unParser :: Text.Trifecta.Parser a } - deriving - ( Functor - , Applicative - , Monad - , Alternative - , MonadPlus - , Parsing - , CharParsing - , DeltaParsing - , MarkParsing Delta - ) - -instance TokenParsing Parser where - someSpace = - Text.Parser.Token.Style.buildSomeSpaceParser - (Parser someSpace) - Text.Parser.Token.Style.haskellCommentStyle - - nesting (Parser m) = Parser (nesting m) - - semi = Parser semi - - highlight h (Parser m) = Parser (highlight h m) - -identifierStyle :: IdentifierStyle Parser -identifierStyle = IdentifierStyle - { _styleName = "dhall" - , _styleStart = - Text.Parser.Char.oneOf (['A'..'Z'] ++ ['a'..'z'] ++ "_") - , _styleLetter = - Text.Parser.Char.oneOf (['A'..'Z'] ++ ['a'..'z'] ++ ['0'..'9'] ++ "_-/") - , _styleReserved = reservedIdentifiers - , _styleHighlight = Identifier - , _styleReservedHighlight = ReservedIdentifier - } - -noted :: Parser (Expr Src a) -> Parser (Expr Src a) -noted parser = do - before <- Text.Trifecta.position - (e, bytes) <- Text.Trifecta.slicedWith (,) parser - after <- Text.Trifecta.position - return (Note (Src before after bytes) e) - -toMap :: [(Text, a)] -> Parser (Map Text a) -toMap kvs = do - let adapt (k, v) = (k, pure v) - let m = Data.Map.fromListWith (<|>) (fmap adapt kvs) - let action k vs = case Data.Sequence.viewl vs of - EmptyL -> empty - v :< vs' -> - if null vs' - then pure v - else - Text.Parser.Combinators.unexpected - ("duplicate field: " ++ Data.Text.Lazy.unpack k) - Data.Map.traverseWithKey action m - -reserve :: String -> Parser () -reserve string = do - _ <- Text.Parser.Token.reserve identifierStyle string - return () - -symbol :: String -> Parser () -symbol string = do - _ <- Text.Parser.Token.symbol string - return () - -sepBy :: Parser a -> Parser b -> Parser [a] -sepBy p sep = sepBy1 p sep <|> pure [] - -sepBy1 :: Parser a -> Parser b -> Parser [a] -sepBy1 p sep = do - a <- p - b <- optional sep - case b of - Nothing -> return [a] - Just _ -> do - as <- sepBy p sep - return (a:as) - -stringLiteral :: Show a => Parser a -> Parser (Expr Src a) -stringLiteral embedded = - Text.Parser.Token.token - ( doubleQuoteLiteral embedded - <|> doubleSingleQuoteString embedded - ) - -doubleQuoteLiteral :: Show a => Parser a -> Parser (Expr Src a) -doubleQuoteLiteral embedded = do - _ <- Text.Parser.Char.char '"' - go - where - go = go0 <|> go1 <|> go2 <|> go3 - - go0 = do - _ <- Text.Parser.Char.char '"' - return (TextLit mempty) - - go1 = do - _ <- Text.Parser.Char.text "${" - Text.Parser.Token.whiteSpace - a <- exprA embedded - _ <- Text.Parser.Char.char '}' - b <- go - return (TextAppend a b) - - go2 = do - _ <- Text.Parser.Char.text "''${" - b <- go - let e = case b of - TextLit cs -> - TextLit ("${" <> cs) - TextAppend (TextLit cs) d -> - TextAppend (TextLit ("${" <> cs)) d - _ -> - TextAppend (TextLit "${") b - return e - - go3 = do - a <- stringChar - b <- go - let e = case b of - TextLit cs -> - TextLit (build a <> cs) - TextAppend (TextLit cs) d -> - TextAppend (TextLit (build a <> cs)) d - _ -> - TextAppend (TextLit (build a)) b - return e - -doubleSingleQuoteString :: Show a => Parser a -> Parser (Expr Src a) -doubleSingleQuoteString embedded = do - expr0 <- p0 - - let builder0 = concatFragments expr0 - let text0 = Data.Text.Lazy.Builder.toLazyText builder0 - let lines0 = Data.Text.Lazy.lines text0 - let isEmpty = Data.Text.Lazy.all Data.Char.isSpace - let nonEmptyLines = filter (not . isEmpty) lines0 - - let indentLength line = - Data.Text.Lazy.length - (Data.Text.Lazy.takeWhile Data.Char.isSpace line) - - let shortestIndent = case nonEmptyLines of - [] -> 0 - _ -> minimum (map indentLength nonEmptyLines) - - -- The purpose of this complicated `trim0`/`trim1` is to ensure that we - -- strip leading whitespace without stripping whitespace after variable - -- interpolation - let trim0 = - build - . Data.Text.Lazy.intercalate "\n" - . map (Data.Text.Lazy.drop shortestIndent) - . Data.Text.Lazy.splitOn "\n" - . Data.Text.Lazy.Builder.toLazyText - - let trim1 builder = build (Data.Text.Lazy.intercalate "\n" lines_) - where - text = Data.Text.Lazy.Builder.toLazyText builder - - lines_ = case Data.Text.Lazy.splitOn "\n" text of - [] -> [] - l:ls -> l:map (Data.Text.Lazy.drop shortestIndent) ls - - let process trim (TextAppend (TextLit t) e) = - TextAppend (TextLit (trim t)) (process trim1 e) - process _ (TextAppend e0 e1) = - TextAppend e0 (process trim1 e1) - process trim (TextLit t) = - TextLit (trim t) - process _ e = - e - - return (process trim0 expr0) - where - -- This treats variable interpolation as breaking leading whitespace for the - -- purposes of computing the shortest leading whitespace. The "${VAR}" - -- could really be any text that breaks whitespace - concatFragments (TextAppend (TextLit t) e) = t <> concatFragments e - concatFragments (TextAppend _ e) = "${VAR}" <> concatFragments e - concatFragments (TextLit t) = t - concatFragments _ = mempty - - p0 = do - _ <- Text.Parser.Char.string "''" - p1 - - p1 = p2 - <|> p3 - <|> p4 - <|> p5 (Text.Parser.Char.char '\'') - <|> p6 - <|> p5 Text.Parser.Char.anyChar - - p2 = do - _ <- Text.Parser.Char.text "'''" - s1 <- p1 - let s4 = case s1 of - TextLit s2 -> - TextLit ("''" <> s2) - TextAppend (TextLit s2) s3 -> - TextAppend (TextLit ("''" <> s2)) s3 - _ -> - TextAppend (TextLit "''") s1 - return s4 - - p3 = do - _ <- Text.Parser.Char.text "''${" - s1 <- p1 - let s4 = case s1 of - TextLit s2 -> - TextLit ("${" <> s2) - TextAppend (TextLit s2) s3 -> - TextAppend (TextLit ("${" <> s2)) s3 - _ -> - TextAppend (TextLit "${") s1 - return s4 - - p4 = do - _ <- Text.Parser.Char.text "''" - return (TextLit mempty) - - p5 parser = do - s0 <- parser - s1 <- p1 - let s4 = case s1 of - TextLit s2 -> - TextLit (build s0 <> s2) - TextAppend (TextLit s2) s3 -> - TextAppend (TextLit (build s0 <> s2)) s3 - _ -> TextAppend (TextLit (build s0)) s1 - return s4 - - p6 = do - _ <- Text.Parser.Char.text "${" - Text.Parser.Token.whiteSpace - s1 <- exprA embedded - _ <- Text.Parser.Char.char '}' - s3 <- p1 - return (TextAppend s1 s3) - -stringChar :: Parser Char -stringChar = - Text.Parser.Char.satisfy predicate - <|> (do _ <- Text.Parser.Char.text "\\\\"; return '\\') - <|> (do _ <- Text.Parser.Char.text "\\\""; return '"' ) - <|> (do _ <- Text.Parser.Char.text "\\n" ; return '\n') - <|> (do _ <- Text.Parser.Char.text "\\r" ; return '\r') - <|> (do _ <- Text.Parser.Char.text "\\t" ; return '\t') - where - predicate c = c /= '"' && c /= '\\' && c > '\026' - -lambda :: Parser () -lambda = symbol "\\" <|> symbol "λ" - -pi :: Parser () -pi = reserve "forall" <|> reserve "∀" - -arrow :: Parser () -arrow = symbol "->" <|> symbol "→" - -combine :: Parser () -combine = symbol "/\\" <|> symbol "∧" - -prefer :: Parser () -prefer = symbol "//" <|> symbol "⫽" - -label :: Parser Text -label = (normalIdentifier <|> escapedIdentifier) "label" - where - normalIdentifier = Text.Parser.Token.ident identifierStyle - - escapedIdentifier = Text.Parser.Token.token (do - _ <- Text.Parser.Char.char '`' - c <- Text.Parser.Token._styleStart identifierStyle - cs <- many (Text.Parser.Token._styleLetter identifierStyle) - _ <- Text.Parser.Char.char '`' - return (Data.Text.Lazy.pack (c:cs)) ) - --- | Parser for a top-level Dhall expression -expr :: Parser (Expr Src Path) -expr = exprA import_ - --- | Parser for a top-level Dhall expression. The expression is parameterized --- over any parseable type, allowing the language to be extended as needed. -exprA :: Show a => Parser a -> Parser (Expr Src a) -exprA embedded = choice - [ noted exprA0 - , noted exprA1 - , noted exprA2 - , noted exprA3 - , noted (try exprA4) - , exprA5 - ] - where - exprA0 = do - lambda - symbol "(" - a <- label - symbol ":" - b <- exprA embedded - symbol ")" - arrow - c <- exprA embedded - return (Lam a b c) - - exprA1 = do - reserve "if" - a <- exprA embedded - reserve "then" - b <- exprA embedded - reserve "else" - c <- exprA embedded - return (BoolIf a b c) - - exprA2 = do - pi - symbol "(" - a <- label - symbol ":" - b <- exprA embedded - symbol ")" - arrow - c <- exprA embedded - return (Pi a b c) - - exprA3 = do - reserve "let" - a <- label - b <- optional (do - symbol ":" - exprA embedded ) - symbol "=" - c <- exprA embedded - reserve "in" - d <- exprA embedded - return (Let a b c d) - - exprA4 = do - a <- exprC embedded - arrow - b <- exprA embedded - return (Pi "_" a b) - - exprA5 = exprB embedded - -exprB :: Show a => Parser a -> Parser (Expr Src a) -exprB embedded = choice - [ noted exprB0 - , noted (try exprB1) - , noted exprB2 - ] - where - exprB0 = do - reserve "merge" - a <- exprE embedded - b <- exprE embedded - c <- optional (do - symbol ":" - exprD embedded ) - return (Merge a b c) - - exprB1 = do - symbol "[" - a <- elems embedded - symbol "]" - symbol ":" - b <- listLike - c <- exprE embedded - return (b c a) - - exprB2 = do - a <- exprC embedded - - let exprB2A= do - symbol ":" - b <- exprA embedded - return (Annot a b) - - let exprB2B = pure a - - exprB2A <|> exprB2B - -listLike :: Parser (Expr Src a -> Vector (Expr Src a) -> Expr Src a) -listLike = - ( listLike0 - <|> listLike1 - ) - where - listLike0 = do - reserve "List" - return (\a b -> ListLit (Just a) b) - - listLike1 = do - reserve "Optional" - return OptionalLit - -exprC :: Show a => Parser a -> Parser (Expr Src a) -exprC embedded = exprC0 - where - chain pA pOp op pB = noted (do - a <- pA - try (do _ <- pOp "operator"; b <- pB; return (op a b)) <|> pure a ) - - exprC0 = chain exprC1 (symbol "||") BoolOr exprC0 - exprC1 = chain exprC2 (symbol "+" ) NaturalPlus exprC1 - exprC2 = chain exprC3 (symbol "++") TextAppend exprC2 - exprC3 = chain exprC4 (symbol "#" ) ListAppend exprC3 - exprC4 = chain exprC5 (symbol "&&") BoolAnd exprC4 - exprC5 = chain exprC6 combine Combine exprC5 - exprC6 = chain exprC7 prefer Prefer exprC6 - exprC7 = chain exprC8 (symbol "*" ) NaturalTimes exprC7 - exprC8 = chain exprC9 (symbol "==") BoolEQ exprC8 - exprC9 = chain (exprD embedded) (symbol "!=") BoolNE exprC9 - --- We can't use left-recursion to define `exprD` otherwise the parser will --- loop infinitely. However, I'd still like to use left-recursion in the --- definition because left recursion greatly simplifies the use of `noted`. The --- work-around is to parse in two phases: --- --- * First, parse to count how many arguments the function is applied to --- * Second, restart the parse using left recursion bounded by the number of --- arguments -exprD :: Show a => Parser a -> Parser (Expr Src a) -exprD embedded = do - e <- noted (exprE embedded) - es <- many (noted (try (exprE embedded))) - let app nL@(Note (Src before _ bytesL) _) nR@(Note (Src _ after bytesR) _) = - Note (Src before after (bytesL <> bytesR)) (App nL nR) - app nL nR = App nL nR - return (Data.List.foldl1 app (e:es)) - -exprE :: Show a => Parser a -> Parser (Expr Src a) -exprE embedded = noted (do - a <- exprF embedded - b <- many (try (do - symbol "." - label )) - return (Data.List.foldl Field a b) ) - -exprF :: Show a => Parser a -> Parser (Expr Src a) -exprF embedded = choice - [ noted (try exprParseDouble) - , noted (try exprNaturalLit) - , noted exprIntegerLit - , noted exprStringLiteral - , noted (try exprRecordType) - , noted exprRecordLiteral - , noted (try exprUnionType) - , noted exprUnionLiteral - , noted exprListLiteral - , noted exprImport - , (choice - [ noted exprNaturalFold - , noted exprNaturalBuild - , noted exprNaturalIsZero - , noted exprNaturalEven - , noted exprNaturalOdd - , noted exprNaturalToInteger - , noted exprNaturalShow - , noted exprIntegerShow - , noted exprDoubleShow - , noted exprListBuild - , noted exprListFold - , noted exprListLength - , noted exprListHead - , noted exprListLast - , noted exprListIndexed - , noted exprListReverse - , noted exprOptionalFold - , noted exprOptionalBuild - , noted exprBool - , noted exprOptional - , noted exprNatural - , noted exprInteger - , noted exprDouble - , noted exprText - , noted exprList - , noted exprBoolLitTrue - , noted exprBoolLitFalse - , noted exprConst - ] - ) "built-in value" - , noted exprVar - , exprParens - ] - where - exprVar = do - a <- var - return (Var a) - - exprConst = do - a <- const - return (Const a) - - exprNatural = do - reserve "Natural" - return Natural - - exprNaturalFold = do - reserve "Natural/fold" - return NaturalFold - - exprNaturalBuild = do - reserve "Natural/build" - return NaturalBuild - - exprNaturalIsZero = do - reserve "Natural/isZero" - return NaturalIsZero - - exprNaturalEven = do - reserve "Natural/even" - return NaturalEven - - exprNaturalOdd = do - reserve "Natural/odd" - return NaturalOdd - - exprNaturalToInteger = do - reserve "Natural/toInteger" - return NaturalToInteger - - exprNaturalShow = do - reserve "Natural/show" - return NaturalShow - - exprInteger = do - reserve "Integer" - return Integer - - exprIntegerShow = do - reserve "Integer/show" - return IntegerShow - - exprDouble = do - reserve "Double" - return Double - - exprDoubleShow = do - reserve "Double/show" - return DoubleShow - - exprText = do - reserve "Text" - return Text - - exprList = do - reserve "List" - return List - - exprListBuild = do - reserve "List/build" - return ListBuild - - exprListFold = do - reserve "List/fold" - return ListFold - - exprListLength = do - reserve "List/length" - return ListLength - - exprListHead = do - reserve "List/head" - return ListHead - - exprListLast = do - reserve "List/last" - return ListLast - - exprListIndexed = do - reserve "List/indexed" - return ListIndexed - - exprListReverse = do - reserve "List/reverse" - return ListReverse - - exprOptional = do - reserve "Optional" - return Optional - - exprOptionalFold = do - reserve "Optional/fold" - return OptionalFold - - exprOptionalBuild = do - reserve "Optional/build" - return OptionalBuild - - exprBool = do - reserve "Bool" - return Bool - - exprBoolLitTrue = do - reserve "True" - return (BoolLit True) - - exprBoolLitFalse = do - reserve "False" - return (BoolLit False) - - exprIntegerLit = do - a <- Text.Parser.Token.integer - return (IntegerLit a) - - exprNaturalLit = (do - _ <- Text.Parser.Char.char '+' - a <- Text.Parser.Token.natural - return (NaturalLit (fromIntegral a)) ) "natural" - - exprParseDouble = do - sign <- fmap (\_ -> negate) (Text.Parser.Char.char '-') - <|> fmap (\_ -> id ) (Text.Parser.Char.char '+') - <|> pure id - a <- Text.Parser.Token.double - return (DoubleLit (sign a)) - - exprStringLiteral = stringLiteral embedded - - exprRecordType = record embedded "record type" - - exprRecordLiteral = recordLit embedded "record literal" - - exprUnionType = union embedded "union type" - - exprUnionLiteral = unionLit embedded "union literal" - - exprListLiteral = listLit embedded "list literal" - - exprImport = do - a <- embedded "import" - return (Embed a) - - exprParens = do - symbol "(" - a <- exprA embedded - symbol ")" - return a - -const :: Parser Const -const = const0 - <|> const1 - where - const0 = do - reserve "Type" - return Type - - const1 = do - reserve "Kind" - return Kind - -var :: Parser Var -var = do - a <- label - m <- optional (do - symbol "@" - Text.Parser.Token.natural ) - let b = case m of - Just r -> r - Nothing -> 0 - return (V a b) - -elems :: Show a => Parser a -> Parser (Vector (Expr Src a)) -elems embedded = do - a <- sepBy (exprA embedded) (symbol ",") - return (Data.Vector.fromList a) - -recordLit :: Show a => Parser a -> Parser (Expr Src a) -recordLit embedded = - recordLit0 - <|> recordLit1 - where - recordLit0 = do - symbol "{=}" - return (RecordLit (Data.Map.fromList [])) - - recordLit1 = do - symbol "{" - a <- fieldValues embedded - b <- toMap a - symbol "}" - return (RecordLit b) - -fieldValues :: Show a => Parser a -> Parser [(Text, Expr Src a)] -fieldValues embedded = sepBy1 (fieldValue embedded) (symbol ",") - -fieldValue :: Show a => Parser a -> Parser (Text, Expr Src a) -fieldValue embedded = do - a <- label - symbol "=" - b <- exprA embedded - return (a, b) - -record :: Show a => Parser a -> Parser (Expr Src a) -record embedded = do - symbol "{" - a <- fieldTypes embedded - b <- toMap a - symbol "}" - return (Record b) - -fieldTypes :: Show a => Parser a -> Parser [(Text, Expr Src a)] -fieldTypes embedded = sepBy (fieldType embedded) (symbol ",") - -fieldType :: Show a => Parser a -> Parser (Text, Expr Src a) -fieldType embedded = do - a <- label - symbol ":" - b <- exprA embedded - return (a, b) - -union :: Show a => Parser a -> Parser (Expr Src a) -union embedded = do - symbol "<" - a <- alternativeTypes embedded - b <- toMap a - symbol ">" - return (Union b) - -alternativeTypes :: Show a => Parser a -> Parser [(Text, Expr Src a)] -alternativeTypes embedded = sepBy (alternativeType embedded) (symbol "|") - -alternativeType :: Show a => Parser a -> Parser (Text, Expr Src a) -alternativeType embedded = do - a <- label - symbol ":" - b <- exprA embedded - return (a, b) - -unionLit :: Show a => Parser a -> Parser (Expr Src a) -unionLit embedded = - try unionLit0 - <|> unionLit1 - where - unionLit0 = do - symbol "<" - a <- label - symbol "=" - b <- exprA embedded - symbol ">" - return (UnionLit a b Data.Map.empty) - - unionLit1 = do - symbol "<" - a <- label - symbol "=" - b <- exprA embedded - symbol "|" - c <- alternativeTypes embedded - d <- toMap c - symbol ">" - return (UnionLit a b d) - -listLit :: Show a => Parser a -> Parser (Expr Src a) -listLit embedded = do - symbol "[" - a <- elems embedded - symbol "]" - return (ListLit Nothing a) - -import_ :: Parser Path -import_ = do - pathType <- pathType_ - let rawText = do - _ <- reserve "as" - _ <- reserve "Text" - return RawText - pathMode <- rawText <|> pure Code - return (Path {..}) - -pathType_ :: Parser PathType -pathType_ = file <|> url <|> env - -pathChar :: Char -> Bool -pathChar c = - not - ( Data.Char.isSpace c - || Data.CharSet.member c disallowedPathChars - ) - -disallowedPathChars :: CharSet -disallowedPathChars = Data.CharSet.fromList "()[]{}<>" - -file :: Parser PathType -file = try (token file0) - <|> token file1 - <|> token file2 - <|> token file3 - where - file0 = do - a <- Text.Parser.Char.string "/" - b <- many (Text.Parser.Char.satisfy pathChar) - case b of - '\\':_ -> empty -- So that "/\" parses as the operator and not a path - '/' :_ -> empty -- So that "//" parses as the operator and not a path - _ -> return () - Text.Parser.Token.whiteSpace - return (File Homeless (Filesystem.Path.CurrentOS.decodeString (a <> b))) - - file1 = do - a <- Text.Parser.Char.string "./" - b <- many (Text.Parser.Char.satisfy pathChar) - Text.Parser.Token.whiteSpace - return (File Homeless (Filesystem.Path.CurrentOS.decodeString (a <> b))) - - file2 = do - a <- Text.Parser.Char.string "../" - b <- many (Text.Parser.Char.satisfy pathChar) - Text.Parser.Token.whiteSpace - return (File Homeless (Filesystem.Path.CurrentOS.decodeString (a <> b))) - - file3 = do - _ <- Text.Parser.Char.string "~" - _ <- some (Text.Parser.Char.string "/") - b <- many (Text.Parser.Char.satisfy pathChar) - Text.Parser.Token.whiteSpace - return (File Home (Filesystem.Path.CurrentOS.decodeString b)) - -url :: Parser PathType -url = try url0 - <|> url1 - where - url0 = do - a <- Text.Parser.Char.string "https://" - b <- many (Text.Parser.Char.satisfy pathChar) - Text.Parser.Token.whiteSpace - c <- optional (do - _ <- Text.Parser.Char.string "using" - Text.Parser.Token.whiteSpace - pathType_ ) - return (URL (Data.Text.Lazy.pack (a <> b)) c) - - url1 = do - a <- Text.Parser.Char.string "http://" - b <- many (Text.Parser.Char.satisfy pathChar) - Text.Parser.Token.whiteSpace - c <- optional (do - _ <- Text.Parser.Char.string "using" - Text.Parser.Token.whiteSpace - pathType_ ) - return (URL (Data.Text.Lazy.pack (a <> b)) c) - -env :: Parser PathType -env = do - _ <- Text.Parser.Char.string "env:" - a <- many (Text.Parser.Char.satisfy pathChar) - Text.Parser.Token.whiteSpace - return (Env (Data.Text.Lazy.pack a)) - --- | A parsing error -newtype ParseError = ParseError Doc deriving (Typeable) - -instance Show ParseError where - show (ParseError doc) = - "\n\ESC[1;31mError\ESC[0m: Invalid input\n\n" <> show doc - -instance Exception ParseError - --- | Parse an expression from `Text` containing a Dhall program -exprFromText :: Delta -> Text -> Either ParseError (Expr Src Path) -exprFromText delta text = case result of - Success r -> Right r - Failure errInfo -> Left (ParseError (Text.Trifecta._errDoc errInfo)) - where - string = Data.Text.Lazy.unpack text - - parser = unParser (do - Text.Parser.Token.whiteSpace - r <- expr - Text.Parser.Combinators.eof - return r ) + , exprAndHeaderFromText + + -- * Parsers + , expr, exprA + + -- * Types + , Src(..) + , ParseError(..) + , Parser(..) + ) where + +import Control.Applicative (Alternative(..), liftA2, optional) +import Control.Exception (Exception) +import Control.Monad (MonadPlus) +import Data.ByteString (ByteString) +import Data.Functor (void) +import Data.Map (Map) +import Data.Monoid ((<>)) +import Data.Sequence (ViewL(..)) +import Data.String (IsString(..)) +import Data.Text.Buildable (Buildable(..)) +import Data.Text.Lazy (Text) +import Data.Text.Lazy.Builder (Builder) +import Data.Typeable (Typeable) +import Dhall.Core +import Numeric.Natural (Natural) +import Prelude hiding (const, pi) +import Text.PrettyPrint.ANSI.Leijen (Doc) +import Text.Parser.Combinators (choice, try, ()) +import Text.Parser.Token (TokenParsing(..)) +import Text.Trifecta + (CharParsing, DeltaParsing, MarkParsing, Parsing, Result(..)) +import Text.Trifecta.Delta (Delta) + +import qualified Control.Monad +import qualified Data.Char +import qualified Data.HashSet +import qualified Data.Map +import qualified Data.ByteString.Lazy +import qualified Data.Sequence +import qualified Data.Text +import qualified Data.Text.Encoding +import qualified Data.Text.Lazy +import qualified Data.Text.Lazy.Builder +import qualified Data.Text.Lazy.Encoding +import qualified Data.Vector +import qualified Filesystem.Path.CurrentOS +import qualified Text.Parser.Char +import qualified Text.Parser.Combinators +import qualified Text.Parser.Token +import qualified Text.Parser.Token.Style +import qualified Text.PrettyPrint.ANSI.Leijen +import qualified Text.Trifecta + +-- | Source code extract +data Src = Src Delta Delta ByteString deriving (Eq, Show) + +instance Buildable Src where + build (Src begin _ bytes) = + build text <> "\n" + <> "\n" + <> build (show (Text.PrettyPrint.ANSI.Leijen.pretty begin)) + <> "\n" + where + bytes' = Data.ByteString.Lazy.fromStrict bytes + + text = Data.Text.Lazy.strip (Data.Text.Lazy.Encoding.decodeUtf8 bytes') + +{-| A `Parser` that is almost identical to + @"Text.Trifecta".`Text.Trifecta.Parser`@ except treating Haskell-style + comments as whitespace +-} +newtype Parser a = Parser { unParser :: Text.Trifecta.Parser a } + deriving + ( Functor + , Applicative + , Monad + , Alternative + , MonadPlus + , Parsing + , CharParsing + , DeltaParsing + , MarkParsing Delta + ) + +instance Monoid a => Monoid (Parser a) where + mempty = pure mempty + + mappend = liftA2 mappend + +instance IsString a => IsString (Parser a) where + fromString x = fmap fromString (Text.Parser.Char.string x) + +instance TokenParsing Parser where + someSpace = + Text.Parser.Token.Style.buildSomeSpaceParser + (Parser someSpace) + Text.Parser.Token.Style.haskellCommentStyle + + nesting (Parser m) = Parser (nesting m) + + semi = Parser semi + + highlight h (Parser m) = Parser (highlight h m) + +noted :: Parser (Expr Src a) -> Parser (Expr Src a) +noted parser = do + before <- Text.Trifecta.position + (e, bytes) <- Text.Trifecta.slicedWith (,) parser + after <- Text.Trifecta.position + return (Note (Src before after bytes) e) + +count :: Monoid a => Int -> Parser a -> Parser a +count n parser = mconcat (replicate n parser) + +range :: Monoid a => Int -> Int -> Parser a -> Parser a +range minimumBound maximumMatches parser = + count minimumBound parser <> loop maximumMatches + where + loop 0 = mempty + loop n = (parser <> loop (n - 1)) <|> mempty + +option :: (Alternative f, Monoid a) => f a -> f a +option p = p <|> pure mempty + +star :: (Alternative f, Monoid a) => f a -> f a +star p = plus p <|> pure mempty + +plus :: (Alternative f, Monoid a) => f a -> f a +plus p = mappend <$> p <*> star p + +satisfy :: (Char -> Bool) -> Parser Builder +satisfy predicate = + fmap Data.Text.Lazy.Builder.singleton (Text.Parser.Char.satisfy predicate) + +blockComment :: Parser () +blockComment = do + _ <- Text.Parser.Char.text "{-" + blockCommentContinue + +blockCommentChunk :: Parser () +blockCommentChunk = + choice + [ blockComment -- Nested block comment + , character + , endOfLine + ] + where + character = void (Text.Parser.Char.satisfy predicate) + where + predicate c = '\x20' <= c && c <= '\x10FFFF' || c == '\n' || c == '\t' + + endOfLine = void (Text.Parser.Char.text "\r\n") + +blockCommentContinue :: Parser () +blockCommentContinue = endOfComment <|> continue + where + endOfComment = void (Text.Parser.Char.text "-}") + + continue = do + blockCommentChunk + blockCommentContinue + +lineComment :: Parser () +lineComment = do + _ <- Text.Parser.Char.text "--" + Text.Parser.Combinators.skipMany notEndOfLine + endOfLine + return () + where + endOfLine = + void (Text.Parser.Char.char '\n' ) + <|> void (Text.Parser.Char.text "\r\n") + + notEndOfLine = void (Text.Parser.Char.satisfy predicate) + where + predicate c = ('\x20' <= c && c <= '\x10FFFF') || c == '\t' + + +whitespaceChunk :: Parser () +whitespaceChunk = + choice + [ void (Text.Parser.Char.satisfy predicate) + , void (Text.Parser.Char.text "\r\n") + , lineComment + , blockComment + ] "whitespace" + where + predicate c = c == ' ' || c == '\t' || c == '\n' + +whitespace :: Parser () +whitespace = Text.Parser.Combinators.skipMany whitespaceChunk + +alpha :: Char -> Bool +alpha c = ('\x41' <= c && c <= '\x5A') || ('\x61' <= c && c <= '\x7A') + +digit :: Char -> Bool +digit c = '\x30' <= c && c <= '\x39' + +hexdig :: Char -> Bool +hexdig c = + ('0' <= c && c <= '9') + || ('A' <= c && c <= 'F') + || ('a' <= c && c <= 'f') + +hexNumber :: Parser Int +hexNumber = choice [ hexDigit, hexUpper, hexLower ] + where + hexDigit = do + c <- Text.Parser.Char.satisfy predicate + return (Data.Char.ord c - Data.Char.ord '0') + where + predicate c = '0' <= c && c <= '9' + + hexUpper = do + c <- Text.Parser.Char.satisfy predicate + return (10 + Data.Char.ord c - Data.Char.ord 'A') + where + predicate c = 'A' <= c && c <= 'F' + + hexLower = do + c <- Text.Parser.Char.satisfy predicate + return (10 + Data.Char.ord c - Data.Char.ord 'a') + where + predicate c = 'a' <= c && c <= 'f' + +simpleLabel :: Parser Text +simpleLabel = try (do + text <- quotedLabel + Control.Monad.guard (not (Data.HashSet.member text reservedIdentifiers)) + return text ) + +quotedLabel :: Parser Text +quotedLabel = try (do + c <- Text.Parser.Char.satisfy headCharacter + cs <- many (Text.Parser.Char.satisfy tailCharacter) + let string = c:cs + return (Data.Text.Lazy.pack string) ) + where + headCharacter c = alpha c || c == '_' + + tailCharacter c = alpha c || digit c || c == '_' || c == '-' || c == '/' + +backtickLabel :: Parser Text +backtickLabel = do + _ <- Text.Parser.Char.char '`' + t <- quotedLabel + _ <- Text.Parser.Char.char '`' + return t + +label :: Parser Text +label = (do + t <- backtickLabel <|> simpleLabel + whitespace + return t ) "label" + +-- | Combine consecutive chunks to eliminate gratuitous appends +textAppend :: Expr Src a -> Expr Src a -> Expr Src a +textAppend (TextLit a) (TextLit b) = + TextLit (a <> b) +textAppend (TextLit a) (TextAppend (TextLit b) c) = + TextAppend (TextLit (a <> b)) c +textAppend a b = + TextAppend a b + +doubleQuotedChunk :: Parser a -> Parser (Expr Src a) +doubleQuotedChunk embedded = + choice + [ interpolation + , unescapedCharacter + , escapedCharacter + ] + where + interpolation = do + _ <- Text.Parser.Char.text "${" + e <- expression embedded + _ <- Text.Parser.Char.char '}' + return e + + unescapedCharacter = do + c <- Text.Parser.Char.satisfy predicate + return (TextLit (Data.Text.Lazy.Builder.singleton c)) + where + predicate c = + ('\x20' <= c && c <= '\x21' ) + || ('\x23' <= c && c <= '\x5B' ) + || ('\x5D' <= c && c <= '\x10FFFF') + + escapedCharacter = do + _ <- Text.Parser.Char.char '\\' + c <- choice + [ quotationMark + , dollarSign + , backSlash + , forwardSlash + , backSpace + , formFeed + , lineFeed + , carriageReturn + , tab + , unicode + ] + return (TextLit (Data.Text.Lazy.Builder.singleton c)) + where + quotationMark = Text.Parser.Char.char '"' + + dollarSign = Text.Parser.Char.char '$' + + backSlash = Text.Parser.Char.char '\\' + + forwardSlash = Text.Parser.Char.char '/' + + backSpace = do _ <- Text.Parser.Char.char 'b'; return '\b' + + formFeed = do _ <- Text.Parser.Char.char 'f'; return '\f' + + lineFeed = do _ <- Text.Parser.Char.char 'n'; return '\n' + + carriageReturn = do _ <- Text.Parser.Char.char 'r'; return '\r' + + tab = do _ <- Text.Parser.Char.char 't'; return '\t' + + unicode = do + _ <- Text.Parser.Char.char 'u'; + n0 <- hexNumber + n1 <- hexNumber + n2 <- hexNumber + n3 <- hexNumber + let n = ((n0 * 16 + n1) * 16 + n2) * 16 + n3 + return (Data.Char.chr n) + +doubleQuotedLiteral :: Parser a -> Parser (Expr Src a) +doubleQuotedLiteral embedded = do + _ <- Text.Parser.Char.char '"' + chunks <- many (doubleQuotedChunk embedded) + _ <- Text.Parser.Char.char '"' + return (foldr textAppend (TextLit "") chunks) + +dedent :: Expr Src a -> Expr Src a +dedent expr0 = process trimBegin expr0 + where + -- This treats variable interpolation as breaking leading whitespace for the + -- purposes of computing the shortest leading whitespace. The "${x}" + -- could really be any text that breaks whitespace + concatFragments (TextAppend (TextLit t) e) = t <> concatFragments e + concatFragments (TextAppend _ e) = "${x}" <> concatFragments e + concatFragments (TextLit t) = t + concatFragments _ = mempty + + builder0 = concatFragments expr0 + + text0 = Data.Text.Lazy.Builder.toLazyText builder0 + + lines0 = Data.Text.Lazy.lines text0 + + isEmpty = Data.Text.Lazy.all Data.Char.isSpace + + nonEmptyLines = filter (not . isEmpty) lines0 + + indentLength line = + Data.Text.Lazy.length (Data.Text.Lazy.takeWhile Data.Char.isSpace line) + + shortestIndent = case nonEmptyLines of + [] -> 0 + _ -> minimum (map indentLength nonEmptyLines) + + -- The purpose of this complicated `trim0`/`trim1` is to ensure that we + -- strip leading whitespace without stripping whitespace after variable + -- interpolation + + -- This is the trim function we use up until the first variable + -- interpolation, dedenting all lines + trimBegin = + build + . Data.Text.Lazy.intercalate "\n" + . map (Data.Text.Lazy.drop shortestIndent) + . Data.Text.Lazy.splitOn "\n" + . Data.Text.Lazy.Builder.toLazyText + + -- This is the trim function we use after each variable interpolation + -- where we indent each line except the first line (since it's not a true + -- beginning of a line) + trimContinue builder = build (Data.Text.Lazy.intercalate "\n" lines_) + where + text = Data.Text.Lazy.Builder.toLazyText builder + + lines_ = case Data.Text.Lazy.splitOn "\n" text of + [] -> [] + l:ls -> l:map (Data.Text.Lazy.drop shortestIndent) ls + + -- This is the loop that drives whether or not to use `trimBegin` or + -- `trimContinue`. We call this function with `trimBegin`, but after the + -- first interpolation we switch permanently to `trimContinue` + process trim (TextAppend (TextLit t) e) = + TextAppend (TextLit (trim t)) (process trimContinue e) + process _ (TextAppend e0 e1) = + TextAppend e0 (process trimContinue e1) + process trim (TextLit t) = + TextLit (trim t) + process _ e = + e + +singleQuoteContinue :: Parser a -> Parser (Expr Src a) +singleQuoteContinue embedded = + choice + [ escapeSingleQuotes + , interpolation + , escapeInterpolation + , endLiteral + , unescapedCharacter + , tab + , endOfLine + ] + where + escapeSingleQuotes = do + a <- fmap TextLit "'''" + b <- singleQuoteContinue embedded + return (textAppend a b) + + interpolation = do + _ <- Text.Parser.Char.text "${" + a <- expression embedded + _ <- Text.Parser.Char.char '}' + b <- singleQuoteContinue embedded + return (textAppend a b) + + escapeInterpolation = do + _ <- Text.Parser.Char.text "''${" + b <- singleQuoteContinue embedded + return (textAppend (TextLit "${") b) + + endLiteral = do + _ <- Text.Parser.Char.text "''" + return (TextLit "") + + unescapedCharacter = do + a <- fmap TextLit (satisfy predicate) + b <- singleQuoteContinue embedded + return (textAppend a b) + where + predicate c = + ('\x20' <= c && c <= '\x26' ) + || ('\x28' <= c && c <= '\x10FFFF') + + endOfLine = do + a <- fmap TextLit "\n" <|> fmap TextLit "\r\n" + b <- singleQuoteContinue embedded + return (textAppend a b) + + tab = do + _ <- Text.Parser.Char.char '\t' + b <- singleQuoteContinue embedded + return (textAppend (TextLit "\t") b) + +singleQuoteLiteral :: Parser a -> Parser (Expr Src a) +singleQuoteLiteral embedded = do + _ <- Text.Parser.Char.text "''" + + -- This is technically not in the grammar, but it's still equivalent to the + -- original grammar and an easy way to discard the first character if it's + -- a newline + _ <- optional endOfLine + + a <- singleQuoteContinue embedded + + return (dedent a) + where + endOfLine = + void (Text.Parser.Char.char '\n' ) + <|> void (Text.Parser.Char.text "\r\n") + +textLiteral :: Parser a -> Parser (Expr Src a) +textLiteral embedded = (do + literal <- doubleQuotedLiteral embedded <|> singleQuoteLiteral embedded + whitespace + return literal ) "text literal" + +reserved :: Data.Text.Text -> Parser () +reserved x = do _ <- Text.Parser.Char.text x; whitespace + +_if :: Parser () +_if = reserved "if" + +_then :: Parser () +_then = reserved "then" + +_else :: Parser () +_else = reserved "else" + +_let :: Parser () +_let = reserved "let" + +_in :: Parser () +_in = reserved "in" + +_as :: Parser () +_as = reserved "as" + +_using :: Parser () +_using = reserved "using" + +_merge :: Parser () +_merge = reserved "merge" + +_NaturalFold :: Parser () +_NaturalFold = reserved "Natural/fold" + +_NaturalBuild :: Parser () +_NaturalBuild = reserved "Natural/build" + +_NaturalIsZero :: Parser () +_NaturalIsZero = reserved "Natural/isZero" + +_NaturalEven :: Parser () +_NaturalEven = reserved "Natural/even" + +_NaturalOdd :: Parser () +_NaturalOdd = reserved "Natural/odd" + +_NaturalToInteger :: Parser () +_NaturalToInteger = reserved "Natural/toInteger" + +_NaturalShow :: Parser () +_NaturalShow = reserved "Natural/show" + +_IntegerShow :: Parser () +_IntegerShow = reserved "Integer/show" + +_DoubleShow :: Parser () +_DoubleShow = reserved "Double/show" + +_ListBuild :: Parser () +_ListBuild = reserved "List/build" + +_ListFold :: Parser () +_ListFold = reserved "List/fold" + +_ListLength :: Parser () +_ListLength = reserved "List/length" + +_ListHead :: Parser () +_ListHead = reserved "List/head" + +_ListLast :: Parser () +_ListLast = reserved "List/last" + +_ListIndexed :: Parser () +_ListIndexed = reserved "List/indexed" + +_ListReverse :: Parser () +_ListReverse = reserved "List/reverse" + +_OptionalFold :: Parser () +_OptionalFold = reserved "Optional/fold" + +_OptionalBuild :: Parser () +_OptionalBuild = reserved "Optional/build" + +_Bool :: Parser () +_Bool = reserved "Bool" + +_Optional :: Parser () +_Optional = reserved "Optional" + +_Natural :: Parser () +_Natural = reserved "Natural" + +_Integer :: Parser () +_Integer = reserved "Integer" + +_Double :: Parser () +_Double = reserved "Double" + +_Text :: Parser () +_Text = reserved "Text" + +_List :: Parser () +_List = reserved "List" + +_True :: Parser () +_True = reserved "True" + +_False :: Parser () +_False = reserved "False" + +_Type :: Parser () +_Type = reserved "Type" + +_Kind :: Parser () +_Kind = reserved "Kind" + +_equal :: Parser () +_equal = reserved "=" + +_or :: Parser () +_or = reserved "||" + +_plus :: Parser () +_plus = reserved "+" + +_textAppend :: Parser () +_textAppend = reserved "++" + +_listAppend :: Parser () +_listAppend = reserved "#" + +_and :: Parser () +_and = reserved "&&" + +_times :: Parser () +_times = reserved "*" + +_doubleEqual :: Parser () +_doubleEqual = reserved "==" + +_notEqual :: Parser () +_notEqual = reserved "!=" + +_dot :: Parser () +_dot = reserved "." + +_openBrace :: Parser () +_openBrace = reserved "{" + +_closeBrace :: Parser () +_closeBrace = reserved "}" + +_openBracket :: Parser () +_openBracket = reserved "[" + +_closeBracket :: Parser () +_closeBracket = reserved "]" + +_openAngle :: Parser () +_openAngle = reserved "<" + +_closeAngle :: Parser () +_closeAngle = reserved ">" + +_bar :: Parser () +_bar = reserved "|" + +_comma :: Parser () +_comma = reserved "," + +_openParens :: Parser () +_openParens = reserved "(" + +_closeParens :: Parser () +_closeParens = reserved ")" + +_colon :: Parser () +_colon = reserved ":" + +_at :: Parser () +_at = reserved "@" + +_combine :: Parser () +_combine = do + void (Text.Parser.Char.char '∧' "\"∧\"") <|> void (Text.Parser.Char.text "/\\") + whitespace + +_prefer :: Parser () +_prefer = do + void (Text.Parser.Char.char '⫽' "\"⫽\"") <|> void (Text.Parser.Char.text "//") + whitespace + +_lambda :: Parser () +_lambda = do + _ <- Text.Parser.Char.satisfy predicate + whitespace + where + predicate 'λ' = True + predicate '\\' = True + predicate _ = False + +_forall :: Parser () +_forall = do + void (Text.Parser.Char.char '∀' "\"∀\"") <|> void (Text.Parser.Char.text "forall") + whitespace + +_arrow :: Parser () +_arrow = do + void (Text.Parser.Char.char '→' "\"→\"") <|> void (Text.Parser.Char.text "->") + whitespace + +doubleLiteral :: Parser Double +doubleLiteral = (do + sign <- fmap (\_ -> negate) (Text.Parser.Char.char '-') + <|> pure id + a <- Text.Parser.Token.double + return (sign a) ) "double literal" + +integerLiteral :: Parser Integer +integerLiteral = Text.Parser.Token.integer "integer literal" + +naturalLiteral :: Parser Natural +naturalLiteral = (do + _ <- Text.Parser.Char.char '+' + a <- Text.Parser.Token.natural + return (fromIntegral a) ) "natural literal" + +identifier :: Parser Var +identifier = do + x <- label + + let indexed = do + _ <- Text.Parser.Char.char '@' + Text.Parser.Token.natural + + n <- indexed <|> pure 0 + return (V x n) + +headPathCharacter :: Char -> Bool +headPathCharacter c = + ('\x21' <= c && c <= '\x27') + || ('\x2A' <= c && c <= '\x2B') + || ('\x2D' <= c && c <= '\x2E') + || ('\x30' <= c && c <= '\x3B') + || c == '\x3D' + || ('\x3F' <= c && c <= '\x5A') + || ('\x5E' <= c && c <= '\x7A') + || c == '\x7C' + || c == '\x7E' + +pathCharacter :: Char -> Bool +pathCharacter c = + headPathCharacter c + || c == '\\' + || c == '/' + +fileRaw :: Parser PathType +fileRaw = + choice + [ try absolutePath + , relativePath + , parentPath + , homePath + ] + where + absolutePath = do + _ <- Text.Parser.Char.char '/' + a <- Text.Parser.Char.satisfy headPathCharacter + bs <- many (Text.Parser.Char.satisfy pathCharacter) + let string = '/':a:bs + return (File Homeless (Filesystem.Path.CurrentOS.decodeString string)) + + relativePath = do + _ <- Text.Parser.Char.text "./" + as <- many (Text.Parser.Char.satisfy pathCharacter) + let string = "./" <> as + return (File Homeless (Filesystem.Path.CurrentOS.decodeString string)) + + parentPath = do + _ <- Text.Parser.Char.text "../" + as <- many (Text.Parser.Char.satisfy pathCharacter) + let string = "../" <> as + return (File Homeless (Filesystem.Path.CurrentOS.decodeString string)) + + homePath = do + _ <- Text.Parser.Char.text "~/" + as <- many (Text.Parser.Char.satisfy pathCharacter) + return (File Home (Filesystem.Path.CurrentOS.decodeString as)) + +file :: Parser PathType +file = do + a <- fileRaw + whitespace + return a + +scheme :: Parser Builder +scheme = "http" <> option "s" + +httpRaw :: Parser Builder +httpRaw = + scheme + <> "://" + <> authority + <> pathAbempty + <> option ("?" <> query) + <> option ("#" <> fragment) + +authority :: Parser Builder +authority = option (try (userinfo <> "@")) <> host <> option (":" <> port) + +userinfo :: Parser Builder +userinfo = star (satisfy predicate <|> pctEncoded) + where + predicate c = unreserved c || subDelims c || c == ':' + +host :: Parser Builder +host = choice [ ipLiteral, ipV4Address, regName ] + +port :: Parser Builder +port = star (satisfy digit) + +ipLiteral :: Parser Builder +ipLiteral = "[" <> (ipV6Address <|> ipVFuture) <> "]" + +ipVFuture :: Parser Builder +ipVFuture = "v" <> plus (satisfy hexdig) <> "." <> plus (satisfy predicate) + where + predicate c = unreserved c || subDelims c || c == ':' + +ipV6Address :: Parser Builder +ipV6Address = + choice + [ try alternative0 + , try alternative1 + , try alternative2 + , try alternative3 + , try alternative4 + , try alternative5 + , try alternative6 + , try alternative7 + , alternative8 + ] + where + alternative0 = count 6 (h16 <> ":") <> ls32 + + alternative1 = "::" <> count 5 (h16 <> ":") <> ls32 + + alternative2 = option h16 <> "::" <> count 4 (h16 <> ":") <> ls32 + + alternative3 = + option (range 0 1 (h16 <> ":") <> h16) + <> "::" + <> count 3 (h16 <> ":") + <> ls32 + + alternative4 = + option (range 0 2 (h16 <> ":") <> h16) + <> "::" + <> count 2 (h16 <> ":") + <> ls32 + + alternative5 = + option (range 0 3 (h16 <> ":") <> h16) <> "::" <> h16 <> ":" <> ls32 + + alternative6 = + option (range 0 4 (h16 <> ":") <> h16) <> "::" <> ls32 + + alternative7 = + option (range 0 5 (h16 <> ":") <> h16) <> "::" <> h16 + + alternative8 = + option (range 0 6 (h16 <> ":") <> h16) <> "::" + +h16 :: Parser Builder +h16 = range 1 3 (satisfy hexdig) + +ls32 :: Parser Builder +ls32 = (h16 <> ":" <> h16) <|> ipV4Address + +ipV4Address :: Parser Builder +ipV4Address = decOctet <> "." <> decOctet <> "." <> decOctet <> "." <> decOctet + +decOctet :: Parser Builder +decOctet = + choice + [ try alternative4 + , try alternative3 + , try alternative2 + , try alternative1 + , alternative0 + ] + where + alternative0 = satisfy digit + + alternative1 = satisfy predicate <> satisfy digit + where + predicate c = '\x31' <= c && c <= '\x39' + + alternative2 = "1" <> count 2 (satisfy digit) + + alternative3 = "2" <> satisfy predicate <> satisfy digit + where + predicate c = '\x30' <= c && c <= '\x34' + + alternative4 = "25" <> satisfy predicate + where + predicate c = '\x30' <= c && c <= '\x35' + +regName :: Parser Builder +regName = star (satisfy predicate <|> pctEncoded) + 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 + predicate c = unreserved c || subDelims c || c == ':' || c == '@' + +query :: Parser Builder +query = star (pchar <|> satisfy predicate) + where + predicate c = c == '/' || c == '?' + +fragment :: Parser Builder +fragment = star (pchar <|> satisfy predicate) + where + predicate c = c == '/' || c == '?' + +pctEncoded :: Parser Builder +pctEncoded = "%" <> count 2 (satisfy hexdig) + +unreserved :: Char -> Bool +unreserved c = + alpha c || digit c || c == '-' || c == '.' || c == '_' || c == '~' + +subDelims :: Char -> Bool +subDelims c = c `elem` ("!$&'()*+,;=" :: String) + +http :: Parser PathType +http = do + a <- httpRaw + whitespace + b <- optional (do + _using + pathType_ ) + return (URL (Data.Text.Lazy.Builder.toLazyText a) b) + +env :: Parser PathType +env = do + _ <- Text.Parser.Char.text "env:" + a <- (alternative0 <|> alternative1) + whitespace + return (Env a) + where + alternative0 = do + a <- bashEnvironmentVariable + return (Data.Text.Lazy.Builder.toLazyText a) + + alternative1 = do + _ <- Text.Parser.Char.char '"' + a <- posixEnvironmentVariable + _ <- Text.Parser.Char.char '"' + return (Data.Text.Lazy.Builder.toLazyText a) + +bashEnvironmentVariable :: Parser Builder +bashEnvironmentVariable = satisfy predicate0 <> star (satisfy predicate1) + where + predicate0 c = alpha c || c == '_' + + predicate1 c = alpha c || digit c || c == '_' + +posixEnvironmentVariable :: Parser Builder +posixEnvironmentVariable = plus posixEnvironmentVariableCharacter + +posixEnvironmentVariableCharacter :: Parser Builder +posixEnvironmentVariableCharacter = + ("\\" <> satisfy predicate0) <|> satisfy predicate1 + where + predicate0 c = c `elem` ("\"\\abfnrtv" :: String) + + predicate1 c = + ('\x20' <= c && c <= '\x21') + || ('\x23' <= c && c <= '\x3C') + || ('\x3E' <= c && c <= '\x5B') + || ('\x5D' <= c && c <= '\x7E') + +expression :: Parser a -> Parser (Expr Src a) +expression embedded = + ( noted + ( choice + [ alternative0 + , alternative1 + , alternative2 + , alternative3 + , alternative4 + ] + ) + <|> alternative5 + ) "expression" + where + alternative0 = do + _lambda + _openParens + a <- label + _colon + b <- expression embedded + _closeParens + _arrow + c <- expression embedded + return (Lam a b c) + + alternative1 = do + _if + a <- expression embedded + _then + b <- expression embedded + _else + c <- expression embedded + return (BoolIf a b c) + + alternative2 = do + _let + a <- label + b <- optional (do + _colon + expression embedded ) + _equal + c <- expression embedded + _in + d <- expression embedded + return (Let a b c d) + + alternative3 = do + _forall + _openParens + a <- label + _colon + b <- expression embedded + _closeParens + _arrow + c <- expression embedded + return (Pi a b c) + + alternative4 = do + a <- try (do a <- operatorExpression embedded; _arrow; return a) + b <- expression embedded + return (Pi "_" a b) + + alternative5 = annotatedExpression embedded + +annotatedExpression :: Parser a -> Parser (Expr Src a) +annotatedExpression embedded = + noted + ( choice + [ alternative0 + , try alternative1 + , alternative2 + ] + ) + where + alternative0 = do + _merge + a <- selectorExpression embedded + b <- selectorExpression embedded + c <- optional (do + _colon + applicationExpression embedded ) + return (Merge a b c) + + alternative1 = (do + _openBracket + (emptyCollection embedded <|> nonEmptyOptional embedded) ) + "list literal" + + alternative2 = do + a <- operatorExpression embedded + b <- optional (do _colon; expression embedded) + case b of + Nothing -> return a + Just c -> return (Annot a c) + +emptyCollection :: Parser a -> Parser (Expr Src a) +emptyCollection embedded = do + _closeBracket + _colon + a <- alternative0 <|> alternative1 + b <- selectorExpression embedded + return (a b empty) + where + alternative0 = do + _List + return (\a b -> ListLit (Just a) b) + + alternative1 = do + _Optional + return OptionalLit + +nonEmptyOptional :: Parser a -> Parser (Expr Src a) +nonEmptyOptional embedded = do + a <- expression embedded + _closeBracket + _colon + _Optional + b <- selectorExpression embedded + return (OptionalLit b (pure a)) + +operatorExpression :: Parser a -> Parser (Expr Src a) +operatorExpression = orExpression + +makeOperatorExpression + :: (Parser a -> Parser (Expr Src a)) + -> Parser () + -> (Expr Src a -> Expr Src a -> Expr Src a) + -> Parser a + -> Parser (Expr Src a) +makeOperatorExpression subExpression operatorParser operator embedded = + noted (do + a <- subExpression embedded + b <- many (do operatorParser; subExpression embedded) + return (foldr1 operator (a:b)) ) + +orExpression :: Parser a -> Parser (Expr Src a) +orExpression = + makeOperatorExpression plusExpression _or BoolOr + +plusExpression :: Parser a -> Parser (Expr Src a) +plusExpression = + makeOperatorExpression textAppendExpression _plus NaturalPlus + +textAppendExpression :: Parser a -> Parser (Expr Src a) +textAppendExpression = + makeOperatorExpression listAppendExpression _textAppend TextAppend + +listAppendExpression :: Parser a -> Parser (Expr Src a) +listAppendExpression = + makeOperatorExpression andExpression _listAppend ListAppend + +andExpression :: Parser a -> Parser (Expr Src a) +andExpression = + makeOperatorExpression combineExpression _and BoolAnd + +combineExpression :: Parser a -> Parser (Expr Src a) +combineExpression = + makeOperatorExpression preferExpression _combine Combine + +preferExpression :: Parser a -> Parser (Expr Src a) +preferExpression = + makeOperatorExpression timesExpression _prefer Prefer + +timesExpression :: Parser a -> Parser (Expr Src a) +timesExpression = + makeOperatorExpression equalExpression _times NaturalTimes + +equalExpression :: Parser a -> Parser (Expr Src a) +equalExpression = + makeOperatorExpression notEqualExpression _doubleEqual BoolEQ + +notEqualExpression :: Parser a -> Parser (Expr Src a) +notEqualExpression = + makeOperatorExpression applicationExpression _notEqual BoolNE + +applicationExpression :: Parser a -> Parser (Expr Src a) +applicationExpression embedded = do + a <- some (noted (selectorExpression embedded)) + return (foldl1 app a) + where + app nL@(Note (Src before _ bytesL) _) nR@(Note (Src _ after bytesR) _) = + Note (Src before after (bytesL <> bytesR)) (App nL nR) + app nL nR = + App nL nR + +selectorExpression :: Parser a -> Parser (Expr Src a) +selectorExpression embedded = noted (do + a <- primitiveExpression embedded + b <- many (try (do _dot; label)) + return (foldl Field a b) ) + +primitiveExpression :: Parser a -> Parser (Expr Src a) +primitiveExpression embedded = + noted + ( choice + [ alternative00 + , alternative01 + , alternative02 + , alternative03 + , alternative04 + , alternative05 + , alternative06 + , alternative07 + + , choice + [ alternative08 + , alternative09 + , alternative10 + , alternative11 + , alternative12 + , alternative13 + , alternative14 + , alternative15 + , alternative16 + , alternative17 + , alternative18 + , alternative19 + , alternative20 + , alternative21 + , alternative22 + , alternative23 + , alternative24 + , alternative25 + , alternative26 + , alternative27 + , alternative28 + , alternative29 + , alternative30 + , alternative31 + , alternative32 + , alternative33 + , alternative34 + , alternative35 + , alternative36 + ] "built-in expression" + , alternative37 + ] + ) + <|> alternative38 + where + alternative00 = do + a <- try doubleLiteral + return (DoubleLit a) + + alternative01 = do + a <- try naturalLiteral + return (NaturalLit a) + + alternative02 = do + a <- try integerLiteral + return (IntegerLit a) + + alternative03 = textLiteral embedded + + alternative04 = (do + _openBrace + a <- recordTypeOrLiteral embedded + _closeBrace + return a ) "record type or literal" + + alternative05 = (do + _openAngle + a <- unionTypeOrLiteral embedded + _closeAngle + return a ) "union type or literal" + + alternative06 = nonEmptyListLiteral embedded + + alternative07 = do + a <- embedded + return (Embed a) + + alternative08 = do + _NaturalFold + return NaturalFold + + alternative09 = do + _NaturalBuild + return NaturalBuild + + alternative10 = do + _NaturalIsZero + return NaturalIsZero + + alternative11 = do + _NaturalEven + return NaturalEven + + alternative12 = do + _NaturalOdd + return NaturalOdd + + alternative13 = do + _NaturalToInteger + return NaturalToInteger + + alternative14 = do + _NaturalShow + return NaturalShow + + alternative15 = do + _IntegerShow + return IntegerShow + + alternative16 = do + _DoubleShow + return DoubleShow + + alternative17 = do + _ListBuild + return ListBuild + + alternative18 = do + _ListFold + return ListFold + + alternative19 = do + _ListLength + return ListLength + + alternative20 = do + _ListHead + return ListHead + + alternative21 = do + _ListLast + return ListLast + + alternative22 = do + _ListIndexed + return ListIndexed + + alternative23 = do + _ListReverse + return ListReverse + + alternative24 = do + _OptionalFold + return OptionalFold + + alternative25 = do + _OptionalBuild + return OptionalBuild + + alternative26 = do + _Bool + return Bool + + alternative27 = do + _Optional + return Optional + + alternative28 = do + _Natural + return Natural + + alternative29 = do + _Integer + return Integer + + alternative30 = do + _Double + return Double + + alternative31 = do + _Text + return Text + + alternative32 = do + _List + return List + + alternative33 = do + _True + return (BoolLit True) + + alternative34 = do + _False + return (BoolLit False) + + alternative35 = do + _Type + return (Const Type) + + alternative36 = do + _Kind + return (Const Kind) + + alternative37 = do + a <- identifier + return (Var a) + + alternative38 = do + _openParens + a <- expression embedded + _closeParens + return a + +recordTypeOrLiteral :: Parser a -> Parser (Expr Src a) +recordTypeOrLiteral embedded = + choice + [ alternative0 + , alternative1 + , alternative2 + ] + where + alternative0 = do + _equal + return (RecordLit Data.Map.empty) + + alternative1 = nonEmptyRecordTypeOrLiteral embedded + + alternative2 = return (Record Data.Map.empty) + +nonEmptyRecordTypeOrLiteral :: Parser a -> Parser (Expr Src a) +nonEmptyRecordTypeOrLiteral embedded = do + a <- label + + let nonEmptyRecordType = do + _colon + b <- expression embedded + e <- many (do + _comma + c <- label + _colon + d <- expression embedded + return (c, d) ) + return (Record (Data.Map.fromList ((a, b):e))) + + let nonEmptyRecordLiteral = do + _equal + b <- expression embedded + e <- many (do + _comma + c <- label + _equal + d <- expression embedded + return (c, d) ) + return (RecordLit (Data.Map.fromList ((a, b):e))) + + nonEmptyRecordType <|> nonEmptyRecordLiteral + +unionTypeOrLiteral :: Parser a -> Parser (Expr Src a) +unionTypeOrLiteral embedded = + nonEmptyUnionTypeOrLiteral embedded <|> return (Union Data.Map.empty) + +nonEmptyUnionTypeOrLiteral :: Parser a -> Parser (Expr Src a) +nonEmptyUnionTypeOrLiteral embedded = do + (f, kvs) <- loop + m <- toMap kvs + return (f m) + where + loop = do + a <- label + + let alternative0 = do + _equal + b <- expression embedded + kvs <- many (do + _bar + c <- label + _colon + d <- expression embedded + return (c, d) ) + return (UnionLit a b, kvs) + + let alternative1 = do + _colon + b <- expression embedded + + let alternative2 = do + _bar + (f, kvs) <- loop + return (f, (a, b):kvs) + + let alternative3 = return (Union, [(a, b)]) + + alternative2 <|> alternative3 + + alternative0 <|> alternative1 + +nonEmptyListLiteral :: Parser a -> Parser (Expr Src a) +nonEmptyListLiteral embedded = (do + _openBracket + a <- expression embedded + b <- many (do _comma; expression embedded) + _closeBracket + return (ListLit Nothing (Data.Vector.fromList (a:b))) ) "list literal" + +completeExpression :: Parser a -> Parser (Expr Src a) +completeExpression embedded = do + whitespace + expression embedded + +toMap :: [(Text, a)] -> Parser (Map Text a) +toMap kvs = do + let adapt (k, v) = (k, pure v) + let m = Data.Map.fromListWith (<|>) (fmap adapt kvs) + let action k vs = case Data.Sequence.viewl vs of + EmptyL -> empty + v :< vs' -> + if null vs' + then pure v + else + Text.Parser.Combinators.unexpected + ("duplicate field: " ++ Data.Text.Lazy.unpack k) + Data.Map.traverseWithKey action m + +-- | Parser for a top-level Dhall expression +expr :: Parser (Expr Src Path) +expr = exprA import_ + +-- | Parser for a top-level Dhall expression. The expression is parameterized +-- over any parseable type, allowing the language to be extended as needed. +exprA :: Parser a -> Parser (Expr Src a) +exprA = completeExpression + +pathType_ :: Parser PathType +pathType_ = choice [ file, http, env ] + +import_ :: Parser Path +import_ = (do + pathType <- pathType_ + pathMode <- alternative <|> pure Code + return (Path {..}) ) "import" + where + alternative = do + _as + _Text + return RawText + +-- | A parsing error +newtype ParseError = ParseError Doc deriving (Typeable) + +instance Show ParseError where + show (ParseError doc) = + "\n\ESC[1;31mError\ESC[0m: Invalid input\n\n" <> show doc + +instance Exception ParseError + +-- | Parse an expression from `Text` containing a Dhall program +exprFromText :: Delta -> Text -> Either ParseError (Expr Src Path) +exprFromText delta text = fmap snd (exprAndHeaderFromText delta text) + +{-| Like `exprFromText` but also returns the leading comments and whitespace + (i.e. header) up to the last newline before the code begins + + In other words, if you have a Dhall file of the form: + +> -- Comment 1 +> {- Comment -} 2 + + Then this will preserve @Comment 1@, but not @Comment 2@ + + This is used by @dhall-format@ to preserve leading comments and whitespace +-} +exprAndHeaderFromText + :: Delta + -> Text + -> Either ParseError (Text, Expr Src Path) +exprAndHeaderFromText delta text = case result of + Failure errInfo -> Left (ParseError (Text.Trifecta._errDoc errInfo)) + Success (bytes, r) -> case Data.Text.Encoding.decodeUtf8' bytes of + Left errInfo -> Left (ParseError (fromString (show errInfo))) + Right txt -> do + let stripped = Data.Text.dropWhileEnd (/= '\n') txt + let lazyText = Data.Text.Lazy.fromStrict stripped + Right (lazyText, r) + where + string = Data.Text.Lazy.unpack text + + parser = unParser (do + bytes <- Text.Trifecta.slicedWith (\_ x -> x) whitespace + r <- expr + Text.Parser.Combinators.eof + return (bytes, r) ) result = Text.Trifecta.parseString parser delta string diff --git a/src/Dhall/Tutorial.hs b/src/Dhall/Tutorial.hs --- a/src/Dhall/Tutorial.hs +++ b/src/Dhall/Tutorial.hs @@ -50,6 +50,12 @@ -- * Headers -- $headers + -- * Raw text + -- $rawText + + -- * Formatting code + -- $format + -- * Built-in functions -- $builtins @@ -1097,6 +1103,41 @@ -- -- > merge { Left = Natural/even, Right = λ(b : Bool) → b } < Right = True | Left : Natural > -- +-- You can also store more than one value or less than one value within +-- alternatives using Dhall's support for anonymous records. You can nest an +-- anonymous record within a union such as in this type: +-- +-- > < Empty : {} | Person : { name : Text, age : Natural } > +-- +-- This union of records resembles following equivalent Haskell data type: +-- +-- > data Example = Empty | Person { name :: Text, age :: Text } +-- +-- You can resemble Haskell further by defining convenient constructors for each +-- alternative, like this: +-- +-- > let Empty = < Empty = {=} | Person : { name : Text, age : Natural } > +-- > in let Person = +-- > λ(p : { name : Text, age : Natural }) → < Person = p | Empty : {} > +-- > in [ Empty +-- > , Person { name = "John", age = +23 } +-- > , Person { name = "Amy" , age = +25 } +-- > , Empty +-- > ] +-- +-- You can also extract fields during pattern matching such as in the following +-- function which renders each value to `Text`: +-- +-- > λ(x : < Empty : {} | Person : { name : Text, age : Natural } >) +-- > → merge +-- > { Empty = λ(_ : {}) → "Unknown" +-- > +-- > , Person = +-- > λ(person : { name : Text, age : Natural }) +-- > → "Name: ${person.name}, Age: ${Natural/show person.age}" +-- > } +-- > x +-- -- __Exercise__: Create a list of the following type with at least one element -- per alternative: -- @@ -1327,7 +1368,7 @@ -- ... or if you needed to provide an authorization token to access a private -- GitHub repository, then your headers could look like this: -- --- > [ { header = "Authorization", value = "token ${env:GITHUB_TOKEN}" } ] +-- > [ { header = "Authorization", value = "token ${env:GITHUB_TOKEN as Text}" } ] -- -- This would read your GitHub API token from the @GITHUB_TOKEN@ environment -- variable and supply that token in the authorization header. @@ -1346,6 +1387,224 @@ -- ... and @http:\/\/example.com@ contains a relative import of @./foo@ then -- Dhall will import @http:\/\/example.com/foo@ using the same @./headers@ file. +-- $rawText +-- +-- Sometimes you want to import the contents of a raw text file as a Dhall +-- value of type `Text`. For example, one of the fields of a record might be +-- the contents of a software license: +-- +-- > { package = "dhall" +-- > , author = "Gabriel Gonzalez" +-- > , license = ./LICENSE +-- > } +-- +-- Normally if you wanted to import a text file you would need to wrap the +-- contents of the file in double single-quotes, like this: +-- +-- > $ cat LICENSE +-- > '' +-- > Copyright (c) 2017 Gabriel Gonzalez +-- > All rights reserved. +-- > +-- > ... +-- > (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +-- > SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +-- > '' +-- +-- ... which does not work well if you need to reuse the same text file for +-- other programs +-- +-- However, Dhall supports importing a raw text file by adding @as Text@ to the +-- end of the import, like this: +-- +-- > { package = "dhall" +-- > , author = "Gabriel Gonzalez" +-- > , license = ./LICENSE as Text +-- > } +-- +-- ... and then you can use the original text file unmodified: +-- +-- > $ cat LICENSE +-- > Copyright (c) 2017 Gabriel Gonzalez +-- > All rights reserved. +-- > +-- > ... +-- > (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +-- > SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +-- $format +-- +-- This package also provides a @dhall-format@ executable that you can use to +-- automatically format Dhall expressions. For example, we can take the +-- following unformatted Dhall expression: +-- +-- > $ cat ./unformatted +-- > λ(a : Type) → λ(kvss : List (List { index : Natural, value : a })) → +-- > List/build { index : Natural, value : a } (λ(list : Type) → λ(cons : { +-- > index : Natural, value : a } → list → list) → λ(nil : list) → +-- > (List/fold (List { index : Natural, value : a }) kvss { count : Natural, diff : +-- > Natural → list } (λ(kvs : List { index : Natural, value : a }) → λ(y : { +-- > count : Natural, diff : Natural → list }) → { count = y.count + List/length +-- > { index : Natural, value : a } kvs, diff = λ(n : Natural) → List/fold { +-- > 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) +-- +-- ... and run the expression through the @dhall-format@ executable: +-- +-- > $ dhall-format < ./unformatted +-- > λ(a : Type) +-- > → λ(kvss : List (List { index : Natural, value : a })) +-- > → List/build +-- > { index : Natural, value : a } +-- > ( λ(list : Type) +-- > → λ(cons : { index : Natural, value : a } → list → list) +-- > → λ(nil : list) +-- > → ( List/fold +-- > (List { index : Natural, value : a }) +-- > kvss +-- > { count : Natural, diff : Natural → list } +-- > ( λ(kvs : List { index : Natural, value : a }) +-- > → λ(y : { count : Natural, diff : Natural → list }) +-- > → { count = y.count + List/length { index : Natural, value : a } kvs +-- > , diff = +-- > λ(n : Natural) +-- > → List/fold +-- > { 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 +-- > ) +-- +-- The executable formats expressions without resolving, type-checking, or +-- normalizing them: +-- +-- > $ dhall-format +-- > let replicate = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate +-- > in replicate +5 (List (List Integer)) (replicate +5 (List Integer) (replicate +5 Integer 1)) +-- > +-- > let replicate = +-- > https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate +-- > +-- > in replicate +-- > +5 +-- > (List (List Integer)) +-- > (replicate +5 (List Integer) (replicate +5 Integer 1)) +-- +-- If you want to evaluate and format an expression then you can combine the +-- @dhall@ and @dhall-format@ executables: +-- +-- > $ dhall | dhall-format +-- > let replicate = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate +-- > in replicate +5 (List (List Integer)) (replicate +5 (List Integer) (replicate +5 Integer 1)) +-- > +-- > List (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 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 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 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 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 Integer) +-- > ) +-- > ] +-- > : List (List (List Integer)) +-- > ) +-- +-- You can also use the formatter to modify files in place using the +-- @--inplace@ flag: +-- +-- > $ dhall-format --inplace ./unformatted +-- > $ cat ./unformatted +-- > λ(a : Type) +-- > → λ(kvss : List (List { index : Natural, value : a })) +-- > → List/build +-- > { index : Natural, value : a } +-- > ( λ(list : Type) +-- > → λ(cons : { index : Natural, value : a } → list → list) +-- > → λ(nil : list) +-- > → ( List/fold +-- > (List { index : Natural, value : a }) +-- > kvss +-- > { count : Natural, diff : Natural → list } +-- > ( λ(kvs : List { index : Natural, value : a }) +-- > → λ(y : { count : Natural, diff : Natural → list }) +-- > → { count = y.count + List/length { index : Natural, value : a } kvs +-- > , diff = +-- > λ(n : Natural) +-- > → List/fold +-- > { 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 +-- > ) +-- +-- Carefully note that the code formatter does not preserve all comments. +-- Currently, the formatter only preserves leading comments and whitespace +-- up until the last newline preceding the code. In other words: +-- +-- > $ dhall-format +-- > {- This comment will be preserved by the formatter -} +-- > -- ... and this comment will be preserved, too +-- > {- This comment will *NOT* be preserved -} 1 +-- > -- ... and this comment will also *NOT* be preserved +-- > +-- > {- This comment will be preserved by the formatter -} +-- > -- ... and this comment will be preserved, too +-- > 1 + -- $builtins -- -- Dhall is a restricted programming language that only supports simple built-in @@ -1596,7 +1855,7 @@ -- > ───────────────────── -- > Γ ⊢ b : Bool Γ ⊢ l : t Γ ⊢ r : t -- > ──────────────────────────────────── --- > Γ ⊢ if b then l else r +-- > Γ ⊢ if b then l else r : t -- -- Rules: -- @@ -1775,7 +2034,7 @@ -- > -- > 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 -- @@ -1867,8 +2126,10 @@ -- > ────────────────────────────────────────── -- > Γ ⊢ [x, y, ... ] : List t -- --- Also, every @List@ must end with a mandatory type annotation +-- Also, every empty @List@ must end with a mandatory type annotation, for example: -- +-- > [] : List Integer +-- -- The built-in operations on @List@s are: -- $listAppend @@ -1876,7 +2137,7 @@ -- Example: -- -- > $ dhall --- > [1, 2, 3] # [5, 6, 7] +-- > [1, 2, 3] # [4, 5, 6] -- > -- > List Integer -- > @@ -2125,6 +2386,10 @@ -- $prelude -- -- There is also a Prelude available at: +-- +-- +-- +-- ... which currenty redirects to: -- -- -- diff --git a/src/Dhall/TypeCheck.hs b/src/Dhall/TypeCheck.hs --- a/src/Dhall/TypeCheck.hs +++ b/src/Dhall/TypeCheck.hs @@ -25,6 +25,7 @@ import Data.Text.Buildable (Buildable(..)) import Data.Text.Lazy (Text) import Data.Text.Lazy.Builder (Builder) +import Data.Text.Prettyprint.Doc (Pretty(..)) import Data.Traversable (forM) import Data.Typeable (Typeable) import Dhall.Core (Const(..), Expr(..), Var(..)) @@ -128,6 +129,7 @@ Nothing -> Left (TypeError ctx e (UnboundVariable x)) Just a -> return a typeWith ctx (Lam x _A b ) = do + _ <- typeWith ctx _A let ctx' = fmap (Dhall.Core.shift 1 (V x 0)) (Dhall.Context.insert x _A ctx) _B <- typeWith ctx' b let p = Pi x _A _B @@ -139,6 +141,7 @@ Const k -> return k _ -> Left (TypeError ctx e (InvalidInputType _A)) + _ <- typeWith ctx _A let ctx' = fmap (Dhall.Core.shift 1 (V x 0)) (Dhall.Context.insert x _A ctx) tB <- fmap Dhall.Core.normalize (typeWith ctx' _B) kB <- case tB of @@ -173,9 +176,9 @@ -- message because this should never happen anyway _ -> Left (TypeError ctx e (InvalidInputType tR)) - let ctx' = Dhall.Context.insert f tR ctx + let ctx' = fmap (Dhall.Core.shift 1 (V f 0)) (Dhall.Context.insert f tR ctx) tB <- typeWith ctx' b - ttB <- fmap Dhall.Core.normalize (typeWith ctx tB) + ttB <- fmap Dhall.Core.normalize (typeWith ctx' tB) kB <- case ttB of Const k -> return k -- Don't bother to provide a `let`-specific version of this error @@ -190,13 +193,17 @@ Nothing -> do return () Just t -> do + _ <- typeWith ctx t let nf_t = Dhall.Core.normalize t let nf_tR = Dhall.Core.normalize tR if propEqual nf_tR nf_t then return () else Left (TypeError ctx e (AnnotMismatch r nf_t nf_tR)) - return tB + let r' = Dhall.Core.shift 1 (V f 0) r + let tB' = Dhall.Core.subst (V f 0) r' (Dhall.Core.normalize tB) + let tB'' = Dhall.Core.shift (-1) (V f 0) tB' + return tB'' typeWith ctx e@(Annot x t ) = do -- This is mainly just to check that `t` is not `Kind` _ <- typeWith ctx t @@ -651,6 +658,9 @@ instance Buildable X where build = absurd +instance Pretty X where + pretty = absurd + -- | The specific type error data TypeMessage s = UnboundVariable Text @@ -1354,14 +1364,14 @@ short = "❰Kind❱ has no type or kind" long = - "Explanation: There are four levels of expressions that form a heirarchy: \n\ + "Explanation: There are four levels of expressions that form a hierarchy: \n\ \ \n\ \● terms \n\ \● types \n\ \● kinds \n\ \● sorts \n\ \ \n\ - \The following example illustrates this heirarchy: \n\ + \The following example illustrates this hierarchy: \n\ \ \n\ \ ┌────────────────────────────┐ \n\ \ │ \"ABC\" : Text : Type : Kind │ \n\ diff --git a/tests/Examples.hs b/tests/Examples.hs --- a/tests/Examples.hs +++ b/tests/Examples.hs @@ -998,7 +998,7 @@ _Optional_toList_0 :: TestTree _Optional_toList_0 = Test.Tasty.HUnit.testCase "Example #0" (do e <- Util.code "./Prelude/Optional/toList Integer ([1] : Optional Integer)" - Util.assertNormalizesTo e "[1] : List Integer" ) + Util.assertNormalizesTo e "[1]" ) _Optional_toList_1 :: TestTree _Optional_toList_1 = Test.Tasty.HUnit.testCase "Example #1" (do diff --git a/tests/Parser.hs b/tests/Parser.hs new file mode 100644 --- /dev/null +++ b/tests/Parser.hs @@ -0,0 +1,141 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Parser where + +import Data.Text (Text) +import Test.Tasty (TestTree) + +import qualified Control.Exception +import qualified Data.Text +import qualified Data.Text.Lazy.IO +import qualified Dhall.Parser +import qualified Test.Tasty +import qualified Test.Tasty.HUnit +import qualified Util + +parserTests :: TestTree +parserTests = + Test.Tasty.testGroup "parser tests" + [ Test.Tasty.testGroup "whitespace" + [ shouldPass + "prefix/suffix" + "./tests/parser/whitespace.dhall" + , shouldPass + "block comment" + "./tests/parser/blockComment.dhall" + , shouldPass + "nested block comment" + "./tests/parser/nestedBlockComment.dhall" + , shouldPass + "line comment" + "./tests/parser/lineComment.dhall" + , shouldPass + "Unicode comment" + "./tests/parser/unicodeComment.dhall" + , shouldPass + "whitespace buffet" + "./tests/parser/whitespaceBuffet.dhall" + , shouldPass + "label" + "./tests/parser/label.dhall" + , shouldPass + "quoted label" + "./tests/parser/quotedLabel.dhall" + , shouldPass + "double quoted string" + "./tests/parser/doubleQuotedString.dhall" + , shouldPass + "Unicode double quoted string" + "./tests/parser/unicodeDoubleQuotedString.dhall" + , shouldPass + "escaped double quoted string" + "./tests/parser/escapedDoubleQuotedString.dhall" + , shouldPass + "interpolated double quoted string" + "./tests/parser/interpolatedDoubleQuotedString.dhall" + , shouldPass + "single quoted string" + "./tests/parser/singleQuotedString.dhall" + , shouldPass + "escaped single quoted string" + "./tests/parser/escapedSingleQuotedString.dhall" + , shouldPass + "interpolated single quoted string" + "./tests/parser/interpolatedSingleQuotedString.dhall" + , shouldPass + "double" + "./tests/parser/double.dhall" + , shouldPass + "natural" + "./tests/parser/natural.dhall" + , shouldPass + "identifier" + "./tests/parser/identifier.dhall" + , shouldParse + "paths" + "./tests/parser/paths.dhall" + , shouldParse + "path termination" + "./tests/parser/pathTermination.dhall" + , shouldParse + "urls" + "./tests/parser/urls.dhall" + , shouldParse + "environmentVariables" + "./tests/parser/environmentVariables.dhall" + , shouldPass + "lambda" + "./tests/parser/lambda.dhall" + , shouldPass + "if then else" + "./tests/parser/ifThenElse.dhall" + , shouldPass + "let" + "./tests/parser/let.dhall" + , shouldPass + "forall" + "./tests/parser/forall.dhall" + , shouldPass + "function type" + "./tests/parser/functionType.dhall" + , shouldPass + "operators" + "./tests/parser/operators.dhall" + , shouldPass + "annotations" + "./tests/parser/annotations.dhall" + , shouldPass + "merge" + "./tests/parser/merge.dhall" + , shouldPass + "fields" + "./tests/parser/fields.dhall" + , shouldPass + "record" + "./tests/parser/record.dhall" + , shouldPass + "union" + "./tests/parser/union.dhall" + , shouldPass + "list" + "./tests/parser/list.dhall" + , shouldPass + "builtins" + "./tests/parser/builtins.dhall" + , shouldPass + "large expression" + "./tests/parser/largeExpression.dhall" + ] + ] + +shouldPass :: Text -> Text -> TestTree +shouldPass name code = Test.Tasty.HUnit.testCase (Data.Text.unpack name) (do + _ <- Util.code code + return () ) + +shouldParse :: Text -> FilePath -> TestTree +shouldParse name path = Test.Tasty.HUnit.testCase (Data.Text.unpack name) (do + text <- Data.Text.Lazy.IO.readFile path + case Dhall.Parser.exprFromText mempty text of + Left err -> Control.Exception.throwIO err + Right _ -> return () ) diff --git a/tests/Regression.hs b/tests/Regression.hs --- a/tests/Regression.hs +++ b/tests/Regression.hs @@ -5,19 +5,31 @@ module Regression where +import qualified Control.Exception import qualified Data.Map import qualified Dhall import qualified Dhall.Core +import qualified Dhall.Parser import qualified Test.Tasty import qualified Test.Tasty.HUnit import qualified Util +import Dhall.Import (Imported) +import Dhall.Parser (Src) +import Dhall.TypeCheck (TypeError) import Test.Tasty (TestTree) +import Test.Tasty.HUnit ((@?=)) regressionTests :: TestTree regressionTests = Test.Tasty.testGroup "regression tests" [ issue96 + , issue126 + , issue151 + , parsing0 + , typeChecking0 + , typeChecking1 + , typeChecking2 , unnamedFields , trailingSpaceAfterStringLiterals ] @@ -53,6 +65,112 @@ issue96 = Test.Tasty.HUnit.testCase "Issue #96" (do -- Verify that parsing should not fail _ <- Util.code "\"bar'baz\"" + return () ) + +issue126 :: TestTree +issue126 = Test.Tasty.HUnit.testCase "Issue #126" (do + e <- Util.code + "''\n\ + \ foo\n\ + \ bar\n\ + \''" + Util.normalize' e @?= "\"foo\\nbar\\n\"" ) + +issue151 :: TestTree +issue151 = Test.Tasty.HUnit.testCase "Issue #151" (do + let shouldNotTypeCheck text = do + let handler :: Imported (TypeError Src) -> IO Bool + handler _ = return True + + let typeCheck = do + _ <- Util.code text + return False + b <- Control.Exception.handle handler typeCheck + Test.Tasty.HUnit.assertBool "The expression should not type-check" b + + -- These two examples contain the following expression that loops infinitely + -- if you normalize the expression before type-checking the expression: + -- + -- (λ(x : A) → x x) (λ(x : A) → x x) + -- + -- There was a bug in the Dhall type-checker were expressions were not + -- being type-checked before being added to the context (which is a + -- violation of the standard type-checking rules for a pure type system). + -- The reason this is problematic is that several places in the + -- type-checking logic assume that the context is safe to normalize. + -- + -- Both of these examples exercise area of the type-checker logic that + -- assume that the context is normalized. If you fail to type-check terms + -- before adding them to the context then this test will "fail" with an + -- infinite loop. This test "succeeds" if the examples terminate + -- immediately with a type-checking failure. + shouldNotTypeCheck "./tests/regression/issue151a.dhall" + shouldNotTypeCheck "./tests/regression/issue151b.dhall" ) + +parsing0 :: TestTree +parsing0 = Test.Tasty.HUnit.testCase "Parsing regression #0" (do + -- Verify that parsing should not fail + -- + -- In 267093f8cddf1c2f909f2d997c31fd0a7cb2440a I broke the parser when left + -- factoring the grammer by failing to handle the source tested by this + -- regression test. The root of the problem was that the parser was trying + -- to parse `List ./Node` as `Field List "/Node"` instead of + -- `App List (Embed (Path (File Homeless "./Node") Code))`. The latter is + -- the correct parse because `/Node` is not a valid field label, but the + -- mistaken parser was committed to the incorrect parse and never attempted + -- the correct parse. + case Dhall.Parser.exprFromText mempty "List ./Node" of + Left e -> Control.Exception.throwIO e + Right _ -> return () ) + +typeChecking0 :: TestTree +typeChecking0 = Test.Tasty.HUnit.testCase "Type-checking regression #0" (do + -- There used to be a bug in the type-checking logic where `T` would be + -- added to the context when inferring the type of `λ(x : T) → x`, but was + -- missing from the context when inferring the kind of the inferred type + -- (i.e. the kind of `∀(x : T) → T`). This led to an unbound variable + -- error when inferring the kind + -- + -- This bug was originally reported in issue #10 + _ <- Util.code "let Day : Type = Natural in λ(x : Day) → x" + return () ) + +typeChecking1 :: TestTree +typeChecking1 = Test.Tasty.HUnit.testCase "Type-checking regression #1" (do + -- There used to be a bug in the type-checking logic when inferring the + -- type of `let`. Specifically, given an expression of the form: + -- + -- let x : t = e1 in e2 + -- + -- ... the type-checker would not substitute `x` for `e1` in the inferred + -- of the `let` expression. This meant that if the inferred type contained + -- any references to `x` then these references would escape their scope and + -- result in unbound variable exceptions + -- + -- This regression test exercises that code path by creating a `let` + -- expression where the inferred type before substitution (`∀(x : b) → b` in + -- this example), contains a reference to the `let`-bound variable (`b`) + -- that needs to be substituted with `a` in order to produce the final + -- correct inferred type (`∀(x : a) → a`). If this test passes then + -- substitution worked correctly. If substitution doesn't occur then you + -- expect an `Unbound variable` error from `b` escaping its scope due to + -- being returned as part of the inferred type + _ <- Util.code "λ(a : Type) → let b : Type = a in λ(x : b) → x" + return () ) + +typeChecking2 :: TestTree +typeChecking2 = Test.Tasty.HUnit.testCase "Type-checking regression #2" (do + -- There used to be a bug in the type-checking logic where `let` bound + -- variables would not correctly shadow variables of the same name when + -- inferring the type of of the `let` expression + -- + -- This example exercises this code path with a `let` expression where the + -- `let`-bound variable (`a`) has the same name as its own type (`a`). If + -- shadowing works correctly then the final `a` in the expression should + -- refer to the `let`-bound variable and not its type. An invalid reference + -- to the shadowed type `a` would result in an invalid dependently typed + -- function + _ <- Util.code "λ(a : Type) → λ(x : a) → let a : a = x in a" return () ) trailingSpaceAfterStringLiterals :: TestTree diff --git a/tests/Tests.hs b/tests/Tests.hs --- a/tests/Tests.hs +++ b/tests/Tests.hs @@ -2,6 +2,7 @@ import Normalization (normalizationTests) import Examples (exampleTests) +import Parser (parserTests) import Regression (regressionTests) import Tutorial (tutorialTests) import Test.Tasty @@ -11,8 +12,9 @@ testGroup "Dhall Tests" [ normalizationTests , exampleTests - , tutorialTests + , parserTests , regressionTests + , tutorialTests ] main :: IO () diff --git a/tests/parser/annotations.dhall b/tests/parser/annotations.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/annotations.dhall @@ -0,0 +1,4 @@ +{ foo = ([] : List Integer) # [1, 2, 3] # ([1, 2, 3] : List Integer) +, bar = [] : Optional Integer +, baz = [1] : Optional Integer +} : { foo : List Integer, bar : Optional Integer, baz : Optional Integer } diff --git a/tests/parser/blockComment.dhall b/tests/parser/blockComment.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/blockComment.dhall @@ -0,0 +1,3 @@ +{- foo -} + +1 diff --git a/tests/parser/builtins.dhall b/tests/parser/builtins.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/builtins.dhall @@ -0,0 +1,31 @@ + λ ( x + : { field0 : Bool + , field1 : Optional (Optional Bool) + , field2 : Natural + , field3 : Integer + , field4 : Double + , field5 : Text + , field6 : List (List Bool) + } + ) +→ { field00 = Natural/fold + , field01 = Natural/build + , field02 = Natural/isZero + , field03 = Natural/even + , field04 = Natural/odd + , field05 = Natural/toInteger + , field06 = Natural/show + , field07 = Integer/show + , field08 = Double/show + , field09 = List/build + , field10 = List/fold + , field11 = List/length + , field12 = List/head + , field13 = List/last + , field14 = List/indexed + , field15 = List/reverse + , field16 = Optional/fold + , field17 = Optional/build + , field18 = True + , field19 = False + } diff --git a/tests/parser/double.dhall b/tests/parser/double.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/double.dhall @@ -0,0 +1,1 @@ +[ 1.1, -1.1, 1e1, 1.1e1, -1.1 ] diff --git a/tests/parser/doubleQuotedString.dhall b/tests/parser/doubleQuotedString.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/doubleQuotedString.dhall @@ -0,0 +1,1 @@ +"ABC" diff --git a/tests/parser/environmentVariables.dhall b/tests/parser/environmentVariables.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/environmentVariables.dhall @@ -0,0 +1,5 @@ +[ env:FOO + + -- Yes, this is legal +, env:"\"\\\a\b\f\n\r\t\v" +] diff --git a/tests/parser/escapedDoubleQuotedString.dhall b/tests/parser/escapedDoubleQuotedString.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/escapedDoubleQuotedString.dhall @@ -0,0 +1,1 @@ +"\\\"\$\\\/\b\f\n\r\t \u2200(a : Type) \u2192 a" diff --git a/tests/parser/escapedSingleQuotedString.dhall b/tests/parser/escapedSingleQuotedString.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/escapedSingleQuotedString.dhall @@ -0,0 +1,4 @@ +'' +''${ +''' +'' diff --git a/tests/parser/fields.dhall b/tests/parser/fields.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/fields.dhall @@ -0,0 +1,1 @@ +({ foo = { bar = { baz = 1 } } }).foo. bar .baz diff --git a/tests/parser/forall.dhall b/tests/parser/forall.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/forall.dhall @@ -0,0 +1,1 @@ +∀(a : Type) → forall (b : Type) -> a diff --git a/tests/parser/functionType.dhall b/tests/parser/functionType.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/functionType.dhall @@ -0,0 +1,1 @@ +Bool → Bool -> Bool diff --git a/tests/parser/identifier.dhall b/tests/parser/identifier.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/identifier.dhall @@ -0,0 +1,1 @@ +λ(a : Type) → λ(a : Type) → a@1 diff --git a/tests/parser/ifThenElse.dhall b/tests/parser/ifThenElse.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/ifThenElse.dhall @@ -0,0 +1,1 @@ +if True then 1 else 2 diff --git a/tests/parser/interpolatedDoubleQuotedString.dhall b/tests/parser/interpolatedDoubleQuotedString.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/interpolatedDoubleQuotedString.dhall @@ -0,0 +1,1 @@ +"ABC${Integer/show 123}" diff --git a/tests/parser/interpolatedSingleQuotedString.dhall b/tests/parser/interpolatedSingleQuotedString.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/interpolatedSingleQuotedString.dhall @@ -0,0 +1,4 @@ +'' +ABC +${Integer/show 123} +'' diff --git a/tests/parser/label.dhall b/tests/parser/label.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/label.dhall @@ -0,0 +1,2 @@ +let _ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789-/ = 1 +in _ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789-/ diff --git a/tests/parser/lambda.dhall b/tests/parser/lambda.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/lambda.dhall @@ -0,0 +1,1 @@ +λ(a : Type) → \(b : Type) -> a diff --git a/tests/parser/largeExpression.dhall b/tests/parser/largeExpression.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/largeExpression.dhall @@ -0,0 +1,254 @@ + λ ( xs + : List + { cores : Natural + , host : Text + , key : Text + , mandatoryFeatures : List Text + , platforms : + List + < AArch64_Linux : {} + | ARMv5tel_Linux : {} + | ARMv7l_Linux : {} + | I686_Cygwin : {} + | I686_Linux : {} + | MIPS64el_Linux : {} + | PowerPC_Linux : {} + | X86_64_Cygwin : {} + | X86_64_Darwin : {} + | X86_64_FreeBSD : {} + | X86_64_Linux : {} + | X86_64_Solaris : {} + > + , speedFactor : Natural + , supportedFeatures : List Text + , user : Optional Text + } + ) +→ List/fold + { cores : Natural + , host : Text + , key : Text + , mandatoryFeatures : List Text + , platforms : + List + < AArch64_Linux : {} + | ARMv5tel_Linux : {} + | ARMv7l_Linux : {} + | I686_Cygwin : {} + | I686_Linux : {} + | MIPS64el_Linux : {} + | PowerPC_Linux : {} + | X86_64_Cygwin : {} + | X86_64_Darwin : {} + | X86_64_FreeBSD : {} + | X86_64_Linux : {} + | X86_64_Solaris : {} + > + , speedFactor : Natural + , supportedFeatures : List Text + , user : Optional Text + } + xs + Text + ( λ ( x + : { cores : Natural + , host : Text + , key : Text + , mandatoryFeatures : List Text + , platforms : + List + < AArch64_Linux : {} + | ARMv5tel_Linux : {} + | ARMv7l_Linux : {} + | I686_Cygwin : {} + | I686_Linux : {} + | MIPS64el_Linux : {} + | PowerPC_Linux : {} + | X86_64_Cygwin : {} + | X86_64_Darwin : {} + | X86_64_FreeBSD : {} + | X86_64_Linux : {} + | X86_64_Solaris : {} + > + , speedFactor : Natural + , supportedFeatures : List Text + , user : Optional Text + } + ) + → λ(y : Text) + → ( Optional/fold + Text + x.user + Text + (λ(user : Text) → user ++ "@" ++ x.host ++ "") + x.host + ++ " " + ++ ( merge + { Empty = λ(_ : {}) → "" + , NonEmpty = λ(result : Text) → result + } + ( List/fold + < AArch64_Linux : {} + | ARMv5tel_Linux : {} + | ARMv7l_Linux : {} + | I686_Cygwin : {} + | I686_Linux : {} + | MIPS64el_Linux : {} + | PowerPC_Linux : {} + | X86_64_Cygwin : {} + | X86_64_Darwin : {} + | X86_64_FreeBSD : {} + | X86_64_Linux : {} + | X86_64_Solaris : {} + > + x.platforms + < Empty : {} | NonEmpty : Text > + ( λ ( element + : < AArch64_Linux : {} + | ARMv5tel_Linux : {} + | ARMv7l_Linux : {} + | I686_Cygwin : {} + | I686_Linux : {} + | MIPS64el_Linux : {} + | PowerPC_Linux : {} + | X86_64_Cygwin : {} + | X86_64_Darwin : {} + | X86_64_FreeBSD : {} + | X86_64_Linux : {} + | X86_64_Solaris : {} + > + ) + → λ(status : < Empty : {} | NonEmpty : Text >) + → merge + { Empty = + λ(_ : {}) + → < NonEmpty = + merge + { AArch64_Linux = λ(_ : {}) → "aarch64-linux" + , ARMv5tel_Linux = + λ(_ : {}) → "armv5tel-linux" + , ARMv7l_Linux = λ(_ : {}) → "armv7l-linux" + , I686_Cygwin = λ(_ : {}) → "i686-cygwin" + , I686_Linux = λ(_ : {}) → "i686-linux" + , MIPS64el_Linux = + λ(_ : {}) → "mips64el-linux" + , PowerPC_Linux = λ(_ : {}) → "powerpc-linux" + , X86_64_Cygwin = λ(_ : {}) → "x86_64-cygwin" + , X86_64_Darwin = λ(_ : {}) → "x86_64-darwin" + , X86_64_FreeBSD = + λ(_ : {}) → "x86_64-freebsd" + , X86_64_Linux = λ(_ : {}) → "x86_64-linux" + , X86_64_Solaris = + λ(_ : {}) → "x86_64-solaris" + } + element + | Empty : {} + > + , NonEmpty = + λ(result : Text) + → < NonEmpty = + ( merge + { AArch64_Linux = + λ(_ : {}) → "aarch64-linux" + , ARMv5tel_Linux = + λ(_ : {}) → "armv5tel-linux" + , ARMv7l_Linux = + λ(_ : {}) → "armv7l-linux" + , I686_Cygwin = + λ(_ : {}) → "i686-cygwin" + , I686_Linux = + λ(_ : {}) → "i686-linux" + , MIPS64el_Linux = + λ(_ : {}) → "mips64el-linux" + , PowerPC_Linux = + λ(_ : {}) → "powerpc-linux" + , X86_64_Cygwin = + λ(_ : {}) → "x86_64-cygwin" + , X86_64_Darwin = + λ(_ : {}) → "x86_64-darwin" + , X86_64_FreeBSD = + λ(_ : {}) → "x86_64-freebsd" + , X86_64_Linux = + λ(_ : {}) → "x86_64-linux" + , X86_64_Solaris = + λ(_ : {}) → "x86_64-solaris" + } + element + ) + ++ "," + ++ result + | Empty : {} + > + } + status + : < Empty : {} | NonEmpty : Text > + ) + < Empty = {=} | NonEmpty : Text > + ) + : Text + ) + ++ " " + ++ x.key + ++ " " + ++ Integer/show (Natural/toInteger x.cores) + ++ " " + ++ Integer/show (Natural/toInteger x.speedFactor) + ++ " " + ++ ( merge + { Empty = λ(_ : {}) → "" + , NonEmpty = λ(result : Text) → result + } + ( List/fold + Text + x.supportedFeatures + < Empty : {} | NonEmpty : Text > + ( λ(element : Text) + → λ(status : < Empty : {} | NonEmpty : Text >) + → merge + { Empty = + λ(_ : {}) → < NonEmpty = element | Empty : {} > + , NonEmpty = + λ(result : Text) + → < NonEmpty = element ++ "," ++ result + | Empty : {} + > + } + status + : < Empty : {} | NonEmpty : Text > + ) + < Empty = {=} | NonEmpty : Text > + ) + : Text + ) + ++ " " + ++ ( merge + { Empty = λ(_ : {}) → "" + , NonEmpty = λ(result : Text) → result + } + ( List/fold + Text + x.mandatoryFeatures + < Empty : {} | NonEmpty : Text > + ( λ(element : Text) + → λ(status : < Empty : {} | NonEmpty : Text >) + → merge + { Empty = + λ(_ : {}) → < NonEmpty = element | Empty : {} > + , NonEmpty = + λ(result : Text) + → < NonEmpty = element ++ "," ++ result + | Empty : {} + > + } + status + : < Empty : {} | NonEmpty : Text > + ) + < Empty = {=} | NonEmpty : Text > + ) + : Text + ) + ++ "\n" + ) + ++ y + ) + "" diff --git a/tests/parser/let.dhall b/tests/parser/let.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/let.dhall @@ -0,0 +1,3 @@ + let x = 1 +in let y : Integer = 2 +in x diff --git a/tests/parser/lineComment.dhall b/tests/parser/lineComment.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/lineComment.dhall @@ -0,0 +1,3 @@ +-- foo + +1 diff --git a/tests/parser/list.dhall b/tests/parser/list.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/list.dhall @@ -0,0 +1,4 @@ +[ [1, 2, 3] +, [1, 2, 3] : List Integer +, [] : List Integer +] diff --git a/tests/parser/merge.dhall b/tests/parser/merge.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/merge.dhall @@ -0,0 +1,7 @@ + λ(x : <>) +→ { bar = merge {=} x : Integer + , foo = + merge + { Left = λ(b : Bool) → b, Right = Natural/even } + < Left = True | Right : Natural > + } diff --git a/tests/parser/natural.dhall b/tests/parser/natural.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/natural.dhall @@ -0,0 +1,1 @@ +[ +0, +1, +01, +10 ] diff --git a/tests/parser/nestedBlockComment.dhall b/tests/parser/nestedBlockComment.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/nestedBlockComment.dhall @@ -0,0 +1,3 @@ +{- foo {- bar -} baz -} + +1 diff --git a/tests/parser/operators.dhall b/tests/parser/operators.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/operators.dhall @@ -0,0 +1,2 @@ + { foo = (False && Natural/even (+1 + +2 * +3)) || True == False != True } +∧ { bar = [ "ABC" ++ "DEF" ] # [ "GHI" ] } ⫽ { baz = True } diff --git a/tests/parser/pathTermination.dhall b/tests/parser/pathTermination.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/pathTermination.dhall @@ -0,0 +1,3 @@ +-- Verify that certain punctuation marks terminate paths correctly + λ(x : ./example) +→ ./example[./example, ./example{bar = ./example, qux = ./example}, ./example] diff --git a/tests/parser/paths.dhall b/tests/parser/paths.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/paths.dhall @@ -0,0 +1,5 @@ +[ /absolute/path +, ./relative/path +, ~/home/anchored/path +, /ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude +] diff --git a/tests/parser/quotedLabel.dhall b/tests/parser/quotedLabel.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/quotedLabel.dhall @@ -0,0 +1,2 @@ +let `let` = 1 +in `let` diff --git a/tests/parser/record.dhall b/tests/parser/record.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/record.dhall @@ -0,0 +1,4 @@ +{ foo = 1 +, bar = +2 +, baz = True +} : { foo : Integer, bar : Natural, baz : Bool } diff --git a/tests/parser/singleQuotedString.dhall b/tests/parser/singleQuotedString.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/singleQuotedString.dhall @@ -0,0 +1,4 @@ +'' +ABC +DEF +'' diff --git a/tests/parser/unicodeComment.dhall b/tests/parser/unicodeComment.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/unicodeComment.dhall @@ -0,0 +1,3 @@ +{- ∀(a : Type) → a -} + +1 diff --git a/tests/parser/unicodeDoubleQuotedString.dhall b/tests/parser/unicodeDoubleQuotedString.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/unicodeDoubleQuotedString.dhall @@ -0,0 +1,1 @@ +"∀(a : Type) → a" diff --git a/tests/parser/union.dhall b/tests/parser/union.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/union.dhall @@ -0,0 +1,4 @@ +< A : { } +| B = { = } +| C : {} +> : < A : {} | B : {} | C : {} > diff --git a/tests/parser/urls.dhall b/tests/parser/urls.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/urls.dhall @@ -0,0 +1,11 @@ +[ http://example.com +, https://john:doe@example.com:8080/foo/bar?qux=0#xyzzy +, http://prelude.dhall-lang.org/ +, https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude +, https://127.0.0.1 +, https://[::] +, https://[2001:0db8:85a3:0000:0000:8a2e:0370:7334] + + -- Yes, this is legal +, https://-._~%2C!$&'()*+,;=:@-._~%2C!$&'()*+,;=:/-._~%2C!$&'()*+,;=:@?/-._~%2C!$&'()*+,;=:@/?#/-._~%2C!$&'()*+,;=:@/? +] diff --git a/tests/parser/whitespace.dhall b/tests/parser/whitespace.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/whitespace.dhall @@ -0,0 +1,3 @@ + +1 + diff --git a/tests/parser/whitespaceBuffet.dhall b/tests/parser/whitespaceBuffet.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/whitespaceBuffet.dhall @@ -0,0 +1,9 @@ + -- This + + Natural/even {- + +{- file +-} + has + + -} +2 -- mixed {- line endings -} diff --git a/tests/regression/issue151a.dhall b/tests/regression/issue151a.dhall new file mode 100644 --- /dev/null +++ b/tests/regression/issue151a.dhall @@ -0,0 +1,1 @@ +let foo : (\(x : A) -> x x) (\(x : A) -> x x) = 1 in foo diff --git a/tests/regression/issue151b.dhall b/tests/regression/issue151b.dhall new file mode 100644 --- /dev/null +++ b/tests/regression/issue151b.dhall @@ -0,0 +1,1 @@ +\(omega : ((\(x : A) -> x x) (\(x : A) -> x x))) -> omega 1