dhall 1.6.0 → 1.7.0
raw patch · 109 files changed
+3865/−1575 lines, 109 filesdep +prettyprinterdep ~basenew-component:exe:dhall-formatPVP ok
version bump matches the API change (PVP)
Dependencies added: prettyprinter
Dependency ranges changed: base
API changes (from Hackage documentation)
+ Dhall: instance Dhall.Inject ()
+ Dhall.Core: instance Data.Text.Prettyprint.Doc.Internal.Pretty Dhall.Core.Path
+ Dhall.Core: instance Data.Text.Prettyprint.Doc.Internal.Pretty a => Data.Text.Prettyprint.Doc.Internal.Pretty (Dhall.Core.Expr s a)
+ Dhall.Parser: exprAndHeaderFromText :: Delta -> Text -> Either ParseError (Text, Expr Src Path)
+ Dhall.Parser: instance Data.String.IsString a => Data.String.IsString (Dhall.Parser.Parser a)
+ Dhall.Parser: instance GHC.Base.Monoid a => GHC.Base.Monoid (Dhall.Parser.Parser a)
+ Dhall.TypeCheck: instance Data.Text.Prettyprint.Doc.Internal.Pretty Dhall.TypeCheck.X
- Dhall.Core: reservedIdentifiers :: HashSet String
+ Dhall.Core: reservedIdentifiers :: HashSet Text
- Dhall.Parser: exprA :: Show a => Parser a -> Parser (Expr Src a)
+ Dhall.Parser: exprA :: Parser a -> Parser (Expr Src a)
Files
- CHANGELOG.md +24/−0
- Prelude/Bool/and +4/−3
- Prelude/Bool/build +4/−3
- Prelude/Bool/even +4/−3
- Prelude/Bool/fold +7/−6
- Prelude/Bool/not +1/−4
- Prelude/Bool/odd +4/−3
- Prelude/Bool/or +4/−3
- Prelude/Bool/show +1/−4
- Prelude/Double/show +1/−4
- Prelude/Integer/show +1/−4
- Prelude/List/all +6/−5
- Prelude/List/any +6/−5
- Prelude/List/build +5/−5
- Prelude/List/concat +14/−21
- Prelude/List/concatMap +12/−11
- Prelude/List/filter +14/−13
- Prelude/List/fold +8/−8
- Prelude/List/generate +19/−18
- Prelude/List/head +1/−4
- Prelude/List/indexed +3/−2
- Prelude/List/iterate +22/−21
- Prelude/List/last +1/−4
- Prelude/List/length +1/−4
- Prelude/List/map +12/−11
- Prelude/List/null +3/−2
- Prelude/List/replicate +11/−10
- Prelude/List/reverse +1/−4
- Prelude/List/shifted +48/−40
- Prelude/List/unzip +31/−31
- Prelude/Monoid +1/−4
- Prelude/Natural/build +8/−8
- Prelude/Natural/enumerate +17/−19
- Prelude/Natural/even +1/−4
- Prelude/Natural/fold +7/−7
- Prelude/Natural/isZero +1/−4
- Prelude/Natural/odd +1/−4
- Prelude/Natural/product +9/−3
- Prelude/Natural/show +1/−4
- Prelude/Natural/sum +9/−3
- Prelude/Natural/toInteger +1/−4
- Prelude/Optional/all +6/−5
- Prelude/Optional/any +6/−5
- Prelude/Optional/build +9/−9
- Prelude/Optional/concat +10/−9
- Prelude/Optional/filter +16/−15
- Prelude/Optional/fold +8/−8
- Prelude/Optional/head +13/−12
- Prelude/Optional/last +13/−12
- Prelude/Optional/length +5/−4
- Prelude/Optional/map +12/−11
- Prelude/Optional/null +5/−4
- Prelude/Optional/toList +11/−5
- Prelude/Optional/unzip +23/−23
- Prelude/Text/concat +4/−3
- Prelude/Text/concatMap +6/−5
- Prelude/Text/concatMapSep +31/−33
- Prelude/Text/concatSep +29/−30
- dhall-format/Main.hs +100/−0
- dhall.cabal +21/−2
- dhall/Main.hs +85/−0
- exec/Main.hs +0/−87
- src/Dhall.hs +7/−0
- src/Dhall/Core.hs +634/−17
- src/Dhall/Parser.hs +1543/−944
- src/Dhall/Tutorial.hs +270/−5
- src/Dhall/TypeCheck.hs +15/−5
- tests/Examples.hs +1/−1
- tests/Parser.hs +141/−0
- tests/Regression.hs +118/−0
- tests/Tests.hs +3/−1
- tests/parser/annotations.dhall +4/−0
- tests/parser/blockComment.dhall +3/−0
- tests/parser/builtins.dhall +31/−0
- tests/parser/double.dhall +1/−0
- tests/parser/doubleQuotedString.dhall +1/−0
- tests/parser/environmentVariables.dhall +5/−0
- tests/parser/escapedDoubleQuotedString.dhall +1/−0
- tests/parser/escapedSingleQuotedString.dhall +4/−0
- tests/parser/fields.dhall +1/−0
- tests/parser/forall.dhall +1/−0
- tests/parser/functionType.dhall +1/−0
- tests/parser/identifier.dhall +1/−0
- tests/parser/ifThenElse.dhall +1/−0
- tests/parser/interpolatedDoubleQuotedString.dhall +1/−0
- tests/parser/interpolatedSingleQuotedString.dhall +4/−0
- tests/parser/label.dhall +2/−0
- tests/parser/lambda.dhall +1/−0
- tests/parser/largeExpression.dhall +254/−0
- tests/parser/let.dhall +3/−0
- tests/parser/lineComment.dhall +3/−0
- tests/parser/list.dhall +4/−0
- tests/parser/merge.dhall +7/−0
- tests/parser/natural.dhall +1/−0
- tests/parser/nestedBlockComment.dhall +3/−0
- tests/parser/operators.dhall +2/−0
- tests/parser/pathTermination.dhall +3/−0
- tests/parser/paths.dhall +5/−0
- tests/parser/quotedLabel.dhall +2/−0
- tests/parser/record.dhall +4/−0
- tests/parser/singleQuotedString.dhall +4/−0
- tests/parser/unicodeComment.dhall +3/−0
- tests/parser/unicodeDoubleQuotedString.dhall +1/−0
- tests/parser/union.dhall +4/−0
- tests/parser/urls.dhall +11/−0
- tests/parser/whitespace.dhall +3/−0
- tests/parser/whitespaceBuffet.dhall +9/−0
- tests/regression/issue151a.dhall +1/−0
- tests/regression/issue151b.dhall +1/−0
CHANGELOG.md view
@@ -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.*
Prelude/Bool/and view
@@ -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
Prelude/Bool/build view
@@ -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
Prelude/Bool/even view
@@ -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
Prelude/Bool/fold view
@@ -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
Prelude/Bool/not view
@@ -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
Prelude/Bool/odd view
@@ -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
Prelude/Bool/or view
@@ -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
Prelude/Bool/show view
@@ -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
Prelude/Double/show view
@@ -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
Prelude/Integer/show view
@@ -10,7 +10,4 @@ ./show 0 = "0" ``` -}-let show : Integer → Text- = Integer/show--in show+let show : Integer → Text = Integer/show in show
Prelude/List/all view
@@ -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
Prelude/List/any view
@@ -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
Prelude/List/build view
@@ -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
Prelude/List/concat view
@@ -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
Prelude/List/concatMap view
@@ -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
Prelude/List/filter view
@@ -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
Prelude/List/fold view
@@ -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
Prelude/List/generate view
@@ -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
Prelude/List/head view
@@ -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
Prelude/List/indexed view
@@ -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
Prelude/List/iterate view
@@ -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
Prelude/List/last view
@@ -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
Prelude/List/length view
@@ -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
Prelude/List/map view
@@ -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
Prelude/List/null view
@@ -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
Prelude/List/replicate view
@@ -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
Prelude/List/reverse view
@@ -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
Prelude/List/shifted view
@@ -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
Prelude/List/unzip view
@@ -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
Prelude/Monoid view
@@ -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
Prelude/Natural/build view
@@ -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
Prelude/Natural/enumerate view
@@ -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
Prelude/Natural/even view
@@ -9,7 +9,4 @@ ./even +0 = True ``` -}-let even : Natural → Bool- = Natural/even--in even+let even : Natural → Bool = Natural/even in even
Prelude/Natural/fold view
@@ -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
Prelude/Natural/isZero view
@@ -9,7 +9,4 @@ ./isZero +0 = True ``` -}-let isZero : Natural → Bool- = Natural/isZero--in isZero+let isZero : Natural → Bool = Natural/isZero in isZero
Prelude/Natural/odd view
@@ -9,7 +9,4 @@ ./odd +0 = False ``` -}-let odd : Natural → Bool- = Natural/odd--in odd+let odd : Natural → Bool = Natural/odd in odd
Prelude/Natural/product view
@@ -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
Prelude/Natural/show view
@@ -10,7 +10,4 @@ ./show +0 = "+0" ``` -}-let show : Natural → Text- = Natural/show--in show+let show : Natural → Text = Natural/show in show
Prelude/Natural/sum view
@@ -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
Prelude/Natural/toInteger view
@@ -9,7 +9,4 @@ ./toInteger +0 = 0 ``` -}-let toInteger : Natural → Integer- = Natural/toInteger--in toInteger+let toInteger : Natural → Integer = Natural/toInteger in toInteger
Prelude/Optional/all view
@@ -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
Prelude/Optional/any view
@@ -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
Prelude/Optional/build view
@@ -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
Prelude/Optional/concat view
@@ -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
Prelude/Optional/filter view
@@ -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
Prelude/Optional/fold view
@@ -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
Prelude/Optional/head view
@@ -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
Prelude/Optional/last view
@@ -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
Prelude/Optional/length view
@@ -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
Prelude/Optional/map view
@@ -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
Prelude/Optional/null view
@@ -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
Prelude/Optional/toList view
@@ -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
Prelude/Optional/unzip view
@@ -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
Prelude/Text/concat view
@@ -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
Prelude/Text/concatMap view
@@ -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
Prelude/Text/concatMapSep view
@@ -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
Prelude/Text/concatSep view
@@ -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
+ dhall-format/Main.hs view
@@ -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 "" )
dhall.cabal view
@@ -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
+ dhall/Main.hs view
@@ -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')) )
− exec/Main.hs
@@ -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')) )
src/Dhall.hs view
@@ -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
src/Dhall/Core.hs view
@@ -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
src/Dhall/Parser.hs view
@@ -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
src/Dhall/Tutorial.hs view
@@ -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))+-- > <Ctrl-D>+-- > 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))+-- > <Ctrl-D>+-- > 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+-- > <Ctrl-D>+-- > {- 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] -- > <Ctrl-D> -- > List Integer -- >@@ -2125,6 +2386,10 @@ -- $prelude -- -- There is also a Prelude available at:+--+-- <http://prelude.dhall-lang.org>+--+-- ... which currenty redirects to: -- -- <https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude> --
src/Dhall/TypeCheck.hs view
@@ -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\
tests/Examples.hs view
@@ -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
+ tests/Parser.hs view
@@ -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 () )
tests/Regression.hs view
@@ -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
tests/Tests.hs view
@@ -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 ()
+ tests/parser/annotations.dhall view
@@ -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 }
+ tests/parser/blockComment.dhall view
@@ -0,0 +1,3 @@+{- foo -}++1
+ tests/parser/builtins.dhall view
@@ -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+ }
+ tests/parser/double.dhall view
@@ -0,0 +1,1 @@+[ 1.1, -1.1, 1e1, 1.1e1, -1.1 ]
+ tests/parser/doubleQuotedString.dhall view
@@ -0,0 +1,1 @@+"ABC"
+ tests/parser/environmentVariables.dhall view
@@ -0,0 +1,5 @@+[ env:FOO++ -- Yes, this is legal+, env:"\"\\\a\b\f\n\r\t\v"+]
+ tests/parser/escapedDoubleQuotedString.dhall view
@@ -0,0 +1,1 @@+"\\\"\$\\\/\b\f\n\r\t \u2200(a : Type) \u2192 a"
+ tests/parser/escapedSingleQuotedString.dhall view
@@ -0,0 +1,4 @@+''+''${+'''+''
+ tests/parser/fields.dhall view
@@ -0,0 +1,1 @@+({ foo = { bar = { baz = 1 } } }).foo. bar .baz
+ tests/parser/forall.dhall view
@@ -0,0 +1,1 @@+∀(a : Type) → forall (b : Type) -> a
+ tests/parser/functionType.dhall view
@@ -0,0 +1,1 @@+Bool → Bool -> Bool
+ tests/parser/identifier.dhall view
@@ -0,0 +1,1 @@+λ(a : Type) → λ(a : Type) → a@1
+ tests/parser/ifThenElse.dhall view
@@ -0,0 +1,1 @@+if True then 1 else 2
+ tests/parser/interpolatedDoubleQuotedString.dhall view
@@ -0,0 +1,1 @@+"ABC${Integer/show 123}"
+ tests/parser/interpolatedSingleQuotedString.dhall view
@@ -0,0 +1,4 @@+''+ABC+${Integer/show 123}+''
+ tests/parser/label.dhall view
@@ -0,0 +1,2 @@+let _ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789-/ = 1+in _ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789-/
+ tests/parser/lambda.dhall view
@@ -0,0 +1,1 @@+λ(a : Type) → \(b : Type) -> a
+ tests/parser/largeExpression.dhall view
@@ -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+ )+ ""
+ tests/parser/let.dhall view
@@ -0,0 +1,3 @@+ let x = 1+in let y : Integer = 2+in x
+ tests/parser/lineComment.dhall view
@@ -0,0 +1,3 @@+-- foo++1
+ tests/parser/list.dhall view
@@ -0,0 +1,4 @@+[ [1, 2, 3]+, [1, 2, 3] : List Integer+, [] : List Integer+]
+ tests/parser/merge.dhall view
@@ -0,0 +1,7 @@+ λ(x : <>)+→ { bar = merge {=} x : Integer+ , foo =+ merge+ { Left = λ(b : Bool) → b, Right = Natural/even }+ < Left = True | Right : Natural >+ }
+ tests/parser/natural.dhall view
@@ -0,0 +1,1 @@+[ +0, +1, +01, +10 ]
+ tests/parser/nestedBlockComment.dhall view
@@ -0,0 +1,3 @@+{- foo {- bar -} baz -}++1
+ tests/parser/operators.dhall view
@@ -0,0 +1,2 @@+ { foo = (False && Natural/even (+1 + +2 * +3)) || True == False != True }+∧ { bar = [ "ABC" ++ "DEF" ] # [ "GHI" ] } ⫽ { baz = True }
+ tests/parser/pathTermination.dhall view
@@ -0,0 +1,3 @@+-- Verify that certain punctuation marks terminate paths correctly+ λ(x : ./example)+→ ./example[./example, ./example{bar = ./example<baz = ./example>, qux = ./example}, ./example]
+ tests/parser/paths.dhall view
@@ -0,0 +1,5 @@+[ /absolute/path+, ./relative/path+, ~/home/anchored/path+, /ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude+]
+ tests/parser/quotedLabel.dhall view
@@ -0,0 +1,2 @@+let `let` = 1+in `let`
+ tests/parser/record.dhall view
@@ -0,0 +1,4 @@+{ foo = 1+, bar = +2+, baz = True+} : { foo : Integer, bar : Natural, baz : Bool }
+ tests/parser/singleQuotedString.dhall view
@@ -0,0 +1,4 @@+''+ABC+DEF+''
+ tests/parser/unicodeComment.dhall view
@@ -0,0 +1,3 @@+{- ∀(a : Type) → a -}++1
+ tests/parser/unicodeDoubleQuotedString.dhall view
@@ -0,0 +1,1 @@+"∀(a : Type) → a"
+ tests/parser/union.dhall view
@@ -0,0 +1,4 @@+< A : { }+| B = { = }+| C : {}+> : < A : {} | B : {} | C : {} >
+ tests/parser/urls.dhall view
@@ -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!$&'()*+,;=:@/?+]
+ tests/parser/whitespace.dhall view
@@ -0,0 +1,3 @@++1+
+ tests/parser/whitespaceBuffet.dhall view
@@ -0,0 +1,9 @@+ -- This+ + Natural/even {-+ +{- file+-} + has+ + -} +2 -- mixed {- line endings -}
+ tests/regression/issue151a.dhall view
@@ -0,0 +1,1 @@+let foo : (\(x : A) -> x x) (\(x : A) -> x x) = 1 in foo
+ tests/regression/issue151b.dhall view
@@ -0,0 +1,1 @@+\(omega : ((\(x : A) -> x x) (\(x : A) -> x x))) -> omega 1