diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,29 @@ +1.3.0 + +* BREAKING CHANGE TO THE API: Add support for new primitives, specifically: + * `(//)` - Right-biased and shallow record merge + * `Optional/build` (now a built-in in order to support build/fold fusion) + * `Natural/show` + * `Integer/show` + * `Double/show` + * `Natural/toInteger` + * These all add new constructors to the `Expr` type, which would break + exhaustive pattern matches +* BREAKING CHANGE TO THE LANGUAGE: Imported paths and URLs no longer support + the characters: "()[]{}<>:" + * This reduces the number of cases where you have to add a space after + imports + * Note that this does not exclude the `:` in the URL scheme (i.e. `http://`) +* Increase connection timeout for imports +* Variable names now allow the `-` character for all but the first character +* You can now escape identifiers with backticks + * This lets you name identifiers so that they don't conflict with reserved + key words + * This is most useful when converting Dhall to other file formats (like + JSON) where you might need to emit a field that conflicts with one of + Dhall's reserved keywords +* New `--version` flag for the `dhall` executable + 1.2.0 * BREAKING CHANGE: Add support for customizing derived `Interpret` instances diff --git a/Prelude/Bool/and b/Prelude/Bool/and new file mode 100644 --- /dev/null +++ b/Prelude/Bool/and @@ -0,0 +1,17 @@ +{- +The `and` function returns `False` if there are any `False` elements in the +`List` and returns `True` otherwise + +Examples: + +``` +./and ([True, False, True] : List Bool) = False + +./and ([] : List Bool) = True +``` +-} +let and : List Bool → Bool + = λ(xs : List Bool) + → List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l && r) True + +in and diff --git a/Prelude/Bool/build b/Prelude/Bool/build new file mode 100644 --- /dev/null +++ b/Prelude/Bool/build @@ -0,0 +1,16 @@ +{- +`build` is the inverse of `fold` + +Examples: + +``` +./build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → true) = True + +./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 + +in build diff --git a/Prelude/Bool/even b/Prelude/Bool/even new file mode 100644 --- /dev/null +++ b/Prelude/Bool/even @@ -0,0 +1,21 @@ +{- +Returns `True` if there are an even number of `False` elements in the list and +returns `False` otherwise + +Examples: + +``` +./even ([False, True, False] : List Bool) = True + +./even ([False, True] : List Bool) = False + +./even ([False] : List Bool) = False + +./even ([] : List Bool) = True +``` +-} +let even : List Bool → Bool + = λ(xs : List Bool) + → List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x == y) True + +in even diff --git a/Prelude/Bool/fold b/Prelude/Bool/fold new file mode 100644 --- /dev/null +++ b/Prelude/Bool/fold @@ -0,0 +1,19 @@ +{- +`fold` is essentially the same as `if`/`then`/else` except as a function + +Examples: + +``` +./fold True Integer 0 1 = 0 + +./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 + +in fold diff --git a/Prelude/Bool/not b/Prelude/Bool/not new file mode 100644 --- /dev/null +++ b/Prelude/Bool/not @@ -0,0 +1,15 @@ +{- +Flip the value of a `Bool` + +Examples: + +``` +./not True = False + +./not False = True +``` +-} +let not : Bool → Bool + = λ(b : Bool) → b == False + +in not diff --git a/Prelude/Bool/odd b/Prelude/Bool/odd new file mode 100644 --- /dev/null +++ b/Prelude/Bool/odd @@ -0,0 +1,21 @@ +{- +Returns `True` if there are an odd number of `True` elements in the list and +returns `False` otherwise + +Examples: + +``` +./odd ([True, False, True] : List Bool) = False + +./odd ([True, False] : List Bool) = True + +./odd ([True] : List Bool) = True + +./odd ([] : List Bool) = False +``` +-} +let odd : List Bool → Bool + = λ(xs : List Bool) + → List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x != y) False + +in odd diff --git a/Prelude/Bool/or b/Prelude/Bool/or new file mode 100644 --- /dev/null +++ b/Prelude/Bool/or @@ -0,0 +1,17 @@ +{- +The `or` function returns `True` if there are any `True` elements in the `List` +and returns `False` otherwise + +Examples: + +``` +./or ([True, False, True] : List Bool) = True + +./or ([] : List Bool) = False +``` +-} +let or : List Bool → Bool + = λ(xs : List Bool) + → List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l || r) False + +in or diff --git a/Prelude/Bool/show b/Prelude/Bool/show new file mode 100644 --- /dev/null +++ b/Prelude/Bool/show @@ -0,0 +1,16 @@ +{- +Render a `Bool` as `Text` using the same representation as Dhall source code +(i.e. beginning with a capital letter) + +Examples: + +``` +./show True = "True" + +./show False = "False" +``` +-} +let show : Bool → Text + = λ(b : Bool) → if b then "True" else "False" + +in show diff --git a/Prelude/Double/show b/Prelude/Double/show new file mode 100644 --- /dev/null +++ b/Prelude/Double/show @@ -0,0 +1,16 @@ +{- +Render a `Double` as `Text` using the same representation as Dhall source +code (i.e. a decimal floating point number with a leading `-` sign if negative) + +Examples: + +``` +./show -3.1 = "-3.1" + +./show 0.4 = "0.4" +``` +-} +let show : Double → Text + = Double/show + +in show diff --git a/Prelude/Integer/show b/Prelude/Integer/show new file mode 100644 --- /dev/null +++ b/Prelude/Integer/show @@ -0,0 +1,16 @@ +{- +Render an `Integer` as `Text` using the same representation as Dhall source +code (i.e. a decimal number with a leading `-` sign if negative) + +Examples: + +``` +./show -3 = "-3" + +./show 0 = "0" +``` +-} +let show : Integer → Text + = Integer/show + +in show diff --git a/Prelude/List/all b/Prelude/List/all new file mode 100644 --- /dev/null +++ b/Prelude/List/all @@ -0,0 +1,19 @@ +{- +Returns `True` if the supplied function returns `True` for all elements in the +`List` + +Examples: + +``` +./all Natural Natural/even ([+2, +3, +5] : List Natural) = False + +./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 + +in all diff --git a/Prelude/List/any b/Prelude/List/any new file mode 100644 --- /dev/null +++ b/Prelude/List/any @@ -0,0 +1,19 @@ +{- +Returns `True` if the supplied function returns `True` for any element in the +`List` + +Examples: + +``` +./any Natural Natural/even ([+2, +3, +5] : List Natural) = True + +./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 + +in any diff --git a/Prelude/List/build b/Prelude/List/build new file mode 100644 --- /dev/null +++ b/Prelude/List/build @@ -0,0 +1,32 @@ +{- +`build` is the inverse of `fold` + +Examples: + +``` +./build +Text +( λ(list : Type) +→ λ(cons : Text → list → list) +→ λ(nil : list) +→ cons "ABC" (cons "DEF" nil) +) += ["ABC", "DEF"] : List Text + +./build +Text +( λ(list : Type) +→ λ(cons : Text → list → list) +→ λ(nil : list) +→ nil +) += [] : List Text +``` +-} +let build + : ∀(a : Type) + → (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list) + → List a + = List/build + +in build diff --git a/Prelude/List/concat b/Prelude/List/concat new file mode 100644 --- /dev/null +++ b/Prelude/List/concat @@ -0,0 +1,50 @@ +{- +Concatenate a `List` of `List`s into a single `List` + +Examples: + +``` +./concat Integer +( [ [0, 1, 2] : List Integer + , [3, 4] : List Integer + , [5, 6, 7, 8] : List Integer + ] : List (List Integer) +) += [0, 1, 2, 3, 4, 5, 6, 7, 8] : List Integer + +./concat Integer +( [ [] : List Integer + , [] : List Integer + , [] : List Integer + ] : List (List Integer) +) += [] : List Integer + +./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 + list + cons + ys + ) + nil + ) + +in concat diff --git a/Prelude/List/filter b/Prelude/List/filter new file mode 100644 --- /dev/null +++ b/Prelude/List/filter @@ -0,0 +1,29 @@ +{- +Only keep elements of the list where the supplied function returns `True` + +Examples: + +``` +./filter Natural Natural/even ([+2, +3, +5] : List Natural) += [+2] : List Natural + +./filter Natural Natural/odd ([+2, +3, +5] : List Natural) += [+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 + a + xs + list + (λ(x : a) → λ(xs : list) → if f x then cons x xs else xs) + ) + +in filter diff --git a/Prelude/List/fold b/Prelude/List/fold new file mode 100644 --- /dev/null +++ b/Prelude/List/fold @@ -0,0 +1,46 @@ +{- +`fold` is the primitive function for consuming `List`s + +If you treat the list `[x, y, z] : List t` as `cons x (cons y (cons z nil))`, +then a `fold` just replaces each `cons` and `nil` with something else + +Examples: + +``` + ./fold + Natural + ([+2, +3, +5] : List Natural) + Natural + (λ(x : Natural) → λ(y : Natural) → x + y) + +0 += +10 + + λ(nil : Natural) +→ ./fold + Natural + ([+2, +3, +5] : List Natural) + Natural + (λ(x : Natural) → λ(y : Natural) → x + y) + nil += λ(nil : Natural) → +2 + +3 + +5 + nil + + λ(list : Type) +→ λ(cons : Natural → list → list) +→ λ(nil : list) +→ ./fold Natural ([+2, +3, +5] : List Natural) list cons nil += λ(list : Type) +→ λ(cons : Natural → list → list) +→ λ(nil : list) +→ cons +2 (cons +3 (cons +5 nil)) +``` +-} +let fold + : ∀(a : Type) + → List a + → ∀(list : Type) + → ∀(cons : a → list → list) + → ∀(nil : list) + → list + = List/fold + +in fold diff --git a/Prelude/List/generate b/Prelude/List/generate new file mode 100644 --- /dev/null +++ b/Prelude/List/generate @@ -0,0 +1,37 @@ +{- +Build a list by calling the supplied function on all `Natural` numbers from `+0` +up to but not including the supplied `Natural` number + +Examples: + +``` +./generate +5 Bool Natural/even = [True, False, True, False, True] : List Bool + +./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 + {} + ( λ(list : Type) + → λ(cons : {} → list → list) + → Natural/fold n list (cons {=}) + ) + ) + ) + list + (λ(x : { index : Natural, value : {} }) → cons (f x.index)) + ) + +in generate diff --git a/Prelude/List/head b/Prelude/List/head new file mode 100644 --- /dev/null +++ b/Prelude/List/head @@ -0,0 +1,15 @@ +{- +Retrieve the first element of the list + +Examples: + +``` +./head Integer ([0, 1, 2] : List Integer) = [0] : Optional Integer + +./head Integer ([] : List Integer) = [] : Optional Integer +``` +-} +let head : ∀(a : Type) → List a → Optional a + = List/head + +in head diff --git a/Prelude/List/indexed b/Prelude/List/indexed new file mode 100644 --- /dev/null +++ b/Prelude/List/indexed @@ -0,0 +1,20 @@ +{- +Tag each element of the list with its index + +Examples: + +``` +./indexed Bool ([True, False, True] : List Bool) += [ { index = +0, value = True } + , { index = +1, value = False } + , { index = +2, value = True } + ] : List { index : Natural, value : Bool } + +./indexed Bool ([] : List Bool) += [] : List { index : Natural, value : Bool } +``` +-} +let indexed : ∀(a : Type) → List a → List { index : Natural, value : a } + = List/indexed + +in indexed diff --git a/Prelude/List/iterate b/Prelude/List/iterate new file mode 100644 --- /dev/null +++ b/Prelude/List/iterate @@ -0,0 +1,42 @@ +{- +Generate a list of the specified length given a seed value and transition +function + +Examples: + +``` +./iterate +10 Natural (λ(x : Natural) → x * +2) +1 += [+1, +2, +4, +8, +16, +32, +64, +128, +256, +512] : List Natural + +./iterate +0 Natural (λ(x : Natural) → x * +2) +1 += [] : 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 + {} + ( λ(list : Type) + → λ(cons : {} → list → list) + → Natural/fold n list (cons {=}) + ) + ) + ) + list + ( λ(y : { index : Natural, value : {} }) + → cons (Natural/fold y.index a f x) + ) + ) + +in iterate diff --git a/Prelude/List/last b/Prelude/List/last new file mode 100644 --- /dev/null +++ b/Prelude/List/last @@ -0,0 +1,15 @@ +{- +Retrieve the last element of the list + +Examples: + +``` +./last Integer ([0, 1, 2] : List Integer) = [2] : Optional Integer + +./last Integer ([] : List Integer) = [] : Optional Integer +``` +-} +let last : ∀(a : Type) → List a → Optional a + = List/last + +in last diff --git a/Prelude/List/length b/Prelude/List/length new file mode 100644 --- /dev/null +++ b/Prelude/List/length @@ -0,0 +1,15 @@ +{- +Returns the number of elements in a list + +Examples: + +``` +./length Integer ([0, 1, 2] : List Integer) = +3 + +./length Integer ([] : List Integer) = +0 +``` +-} +let length : ∀(a : Type) → List a → Natural + = List/length + +in length diff --git a/Prelude/List/map b/Prelude/List/map new file mode 100644 --- /dev/null +++ b/Prelude/List/map @@ -0,0 +1,26 @@ +{- +Tranform a list by applying a function to each element + +Examples: + +``` +./map Natural Bool Natural/even ([+2, +3, +5] : List Natural) += [True, False, False] : List Bool + +./map Natural Bool Natural/even ([] : List Natural) += [] : 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)) + ) + +in map diff --git a/Prelude/List/null b/Prelude/List/null new file mode 100644 --- /dev/null +++ b/Prelude/List/null @@ -0,0 +1,15 @@ +{- +Returns `True` if the `List` is empty and `False` otherwise + +Examples: + +``` +./null Integer ([0, 1, 2] : List Integer) = False + +./null Integer ([] : List Integer) = True +``` +-} +let null : ∀(a : Type) → List a → Bool + = λ(a : Type) → λ(xs : List a) → Natural/isZero (List/length a xs) + +in null diff --git a/Prelude/List/replicate b/Prelude/List/replicate new file mode 100644 --- /dev/null +++ b/Prelude/List/replicate @@ -0,0 +1,23 @@ +{- +Build a list by copying the given element the specified number of times + +Examples: + +``` +./replicate +9 Integer 1 = [1, 1, 1, 1, 1, 1, 1, 1, 1] : List Integer + +./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) + ) + +in replicate diff --git a/Prelude/List/reverse b/Prelude/List/reverse new file mode 100644 --- /dev/null +++ b/Prelude/List/reverse @@ -0,0 +1,15 @@ +{- +Reverse a list + +Examples: + +``` +./reverse Integer ([0, 1, 2] : List Integer) = [2, 1, 0] : List Integer + +./reverse Integer ([] : List Integer) = [] : List Integer +``` +-} +let reverse : ∀(a : Type) → List a → List a + = List/reverse + +in reverse diff --git a/Prelude/List/shifted b/Prelude/List/shifted new file mode 100644 --- /dev/null +++ b/Prelude/List/shifted @@ -0,0 +1,80 @@ +{- +Combine a `List` of `List`s, offsetting the `index` of each element by the +number of elements in preceding lists + +Examples: + +``` +./shifted +Bool +( [ [ { index = +0, value = True } + , { index = +1, value = True } + , { index = +2, value = True } + ] : List { index : Natural, value : Bool } + , [ { index = +0, value = False } + , { index = +1, value = False } + ] : List { index : Natural, value : Bool } + , [ { index = +0, value = True } + , { index = +1, value = True } + , { index = +2, value = True } + , { index = +3, value = True } + ] : List { index : Natural, value : Bool } + ] : List (List { index : Natural, value : Bool }) +) += [ { index = +0, value = True } + , { index = +1, value = True } + , { index = +2, value = True } + , { index = +3, value = False } + , { index = +4, value = False } + , { index = +5, value = True } + , { index = +6, value = True } + , { index = +7, value = True } + , { index = +8, value = True } + ] : List { index : Natural, value : Bool } + +./shifted Bool ([] : List (List { index : Natural, value : Bool })) += [] : 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 + ) + +in shifted diff --git a/Prelude/List/unzip b/Prelude/List/unzip new file mode 100644 --- /dev/null +++ b/Prelude/List/unzip @@ -0,0 +1,55 @@ +{- +Unzip a `List` into two separate `List`s + +Examples: + +``` +./unzip +Text +Bool +( [ { _1 = "ABC", _2 = True } + , { _1 = "DEF", _2 = False } + , { _1 = "GHI", _2 = True } + ] : List { _1 : Text, _2 : Bool } +) += { _1 = ["ABC", "DEF", "GHI"] : List Text + , _2 = [True, False, True] : List Bool + } + +./unzip Text Bool ([] : List { _1 : Text, _2 : Bool }) += { _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) + ) + } + +in unzip diff --git a/Prelude/Monoid b/Prelude/Monoid new file mode 100644 --- /dev/null +++ b/Prelude/Monoid @@ -0,0 +1,42 @@ +{- +Any function `f` that is a `Monoid` must satisfy the following law: + +``` +t : Type +f : ./Monoid t +xs : List (List t) + +f (./List/concat t xs) = f (./map (List t) t f xs) +``` + +Examples: + +``` +./Bool/and + : ./Monoid Bool +./Bool/or + : ./Monoid Bool +./Bool/even + : ./Monoid Bool +./Bool/odd + : ./Monoid Bool +./List/concat + : ∀(a : Type) → ./Monoid (List a) +./List/shifted + : ∀(a : Type) → ./Monoid (List { index : Natural, value : a }) +./Natural/sum + : ./Monoid Natural +./Natural/product + : ./Monoid Natural +./Optional/head + : ∀(a : Type) → ./Monoid (Optional a) +./Optional/last + : ∀(a : Type) → ./Monoid (Optional a) +./Text/concat + : ./Monoid Text +``` +-} +let Monoid : ∀(m : Type) → Type + = λ(m : Type) → List m → m + +in Monoid diff --git a/Prelude/Natural/build b/Prelude/Natural/build new file mode 100644 --- /dev/null +++ b/Prelude/Natural/build @@ -0,0 +1,33 @@ +{- +`build` is the inverse of `fold` + +Examples: + +``` +./build +( λ(natural : Type) +→ λ(succ : natural → natural) +→ λ(zero : natural) +→ succ (succ (succ zero)) +) += +3 + +./build +( λ(natural : Type) +→ λ(succ : natural → natural) +→ λ(zero : natural) +→ zero +) += +0 +``` +-} +let build + : ( ∀(natural : Type) + → ∀(succ : natural → natural) + → ∀(zero : natural) + → natural + ) + → Natural + = Natural/build + +in build diff --git a/Prelude/Natural/enumerate b/Prelude/Natural/enumerate new file mode 100644 --- /dev/null +++ b/Prelude/Natural/enumerate @@ -0,0 +1,38 @@ +{- +Generate a list of numbers from `+0` up to but not including the specified +number + +Examples: + +``` +./enumerate +10 = [+0, +1, +2, +3, +4, +5, +6, +7, +8, +9] : List Natural + +./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 + {} + ( λ(list : Type) + → λ(cons : {} → list → list) + → Natural/fold + n + list + (cons {=}) + ) + ) + ) + list + (λ(x : { index : Natural, value : {} }) → cons x.index) + ) + +in enumerate diff --git a/Prelude/Natural/even b/Prelude/Natural/even new file mode 100644 --- /dev/null +++ b/Prelude/Natural/even @@ -0,0 +1,15 @@ +{- +Returns `True` if a number if even and returns `False` otherwise + +Examples: + +``` +./even +3 = False + +./even +0 = True +``` +-} +let even : Natural → Bool + = Natural/even + +in even diff --git a/Prelude/Natural/fold b/Prelude/Natural/fold new file mode 100644 --- /dev/null +++ b/Prelude/Natural/fold @@ -0,0 +1,33 @@ +{- +`fold` is the primitive function for consuming `Natural` numbers + +If you treat the number `+3` as `succ (succ (succ zero))` then a `fold` just +replaces each `succ` and `zero` with something else + +Examples: + +``` +./fold +3 Natural (λ(x : Natural) → +5 * x) +1 = +125 + +λ(zero : Natural) → ./fold +3 Natural (λ(x : Natural) → +5 * x) zero += λ(zero : Natural) → +5 * +5 * +5 * zero + + λ(natural : Type) +→ λ(succ : natural → natural) +→ λ(zero : natural) +→ ./fold +3 natural succ zero += λ(natural : Type) +→ λ(succ : natural → natural) +→ λ(zero : natural) +→ succ (succ (succ zero)) +``` +-} +let fold + : Natural + → ∀(natural : Type) + → ∀(succ : natural → natural) + → ∀(zero : natural) + → natural + = Natural/fold + +in fold diff --git a/Prelude/Natural/isZero b/Prelude/Natural/isZero new file mode 100644 --- /dev/null +++ b/Prelude/Natural/isZero @@ -0,0 +1,15 @@ +{- +Returns `True` if a number is `+0` and returns `False` otherwise + +Examples: + +``` +./isZero +2 = False + +./isZero +0 = True +``` +-} +let isZero : Natural → Bool + = Natural/isZero + +in isZero diff --git a/Prelude/Natural/odd b/Prelude/Natural/odd new file mode 100644 --- /dev/null +++ b/Prelude/Natural/odd @@ -0,0 +1,15 @@ +{- +Returns `True` if a number is odd and returns `False` otherwise + +Examples: + +``` +./odd +3 = True + +./odd +0 = False +``` +-} +let odd : Natural → Bool + = Natural/odd + +in odd diff --git a/Prelude/Natural/product b/Prelude/Natural/product new file mode 100644 --- /dev/null +++ b/Prelude/Natural/product @@ -0,0 +1,16 @@ +{- +Multiply all the numbers in a `List` + +Examples: + +``` +./product ([+2, +3, +5] : List Natural) = +30 + +./product ([] : List Natural) = +1 +``` +-} +let product : List Natural → Natural + = λ(xs : List Natural) + → List/fold Natural xs Natural (λ(l : Natural) → λ(r : Natural) → l * r) +1 + +in product diff --git a/Prelude/Natural/show b/Prelude/Natural/show new file mode 100644 --- /dev/null +++ b/Prelude/Natural/show @@ -0,0 +1,16 @@ +{- +Render a `Natural` number as `Text` using the same representation as Dhall +source code (i.e. a decimal number with a leading `+` sign) + +Examples: + +``` +./show +3 = "+3" + +./show +0 = "+0" +``` +-} +let show : Natural → Text + = Natural/show + +in show diff --git a/Prelude/Natural/sum b/Prelude/Natural/sum new file mode 100644 --- /dev/null +++ b/Prelude/Natural/sum @@ -0,0 +1,16 @@ +{- +Add all the numbers in a `List` + +Examples: + +``` +./sum ([+2, +3, +5] : List Natural) = +10 + +./sum ([] : List Natural) = +0 +``` +-} +let sum : List Natural → Natural + = λ(xs : List Natural) + → List/fold Natural xs Natural (λ(l : Natural) → λ(r : Natural) → l + r) +0 + +in sum diff --git a/Prelude/Natural/toInteger b/Prelude/Natural/toInteger new file mode 100644 --- /dev/null +++ b/Prelude/Natural/toInteger @@ -0,0 +1,15 @@ +{- +Convert a `Natural` number to the corresponding `Integer` + +Examples: + +``` +./toInteger +3 = 3 + +./toInteger +0 = 0 +``` +-} +let toInteger : Natural → Integer + = Natural/toInteger + +in toInteger diff --git a/Prelude/Optional/build b/Prelude/Optional/build new file mode 100644 --- /dev/null +++ b/Prelude/Optional/build @@ -0,0 +1,36 @@ +{- +`build` is the inverse of `fold` + +Examples: + +``` +./build +Integer +( λ(optional : Type) +→ λ(just : Integer → optional) +→ λ(nothing : optional) +→ just 1 +) += [1] : Optional Integer + +./build +Integer +( λ(optional : Type) +→ λ(just : Integer → optional) +→ λ(nothing : optional) +→ nothing +) += [] : Optional Integer +``` +-} +let build + : ∀(a : Type) + → ( ∀(optional : Type) + → ∀(just : a → optional) + → ∀(nothing : optional) + → optional + ) + → Optional a + = Optional/build + +in build diff --git a/Prelude/Optional/concat b/Prelude/Optional/concat new file mode 100644 --- /dev/null +++ b/Prelude/Optional/concat @@ -0,0 +1,27 @@ +{- +Flatten two `Optional` layers into a single `Optional` layer + +Examples: + +``` +./concat Integer ([[1] : Optional Integer] : Optional (Optional Integer)) += [1] : Optional Integer + +./concat Integer ([[] : Optional Integer] : Optional (Optional Integer)) += [] : Optional Integer + +./concat Integer ([] : Optional (Optional Integer)) += [] : 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) + +in concat diff --git a/Prelude/Optional/fold b/Prelude/Optional/fold new file mode 100644 --- /dev/null +++ b/Prelude/Optional/fold @@ -0,0 +1,21 @@ +{- +`fold` is the primitive function for consuming `Optional` values + +Examples: + +``` +./fold Integer ([2] : Optional Integer) Integer (λ(x : Integer) → x) 0 = 2 + +./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 + +in fold diff --git a/Prelude/Optional/head b/Prelude/Optional/head new file mode 100644 --- /dev/null +++ b/Prelude/Optional/head @@ -0,0 +1,36 @@ +{- +Returns the first non-empty `Optional` value in a `List` + +Examples: + +``` +./head +Integer +( [[] : Optional Integer, [1] : Optional Integer, [2] : Optional Integer] + : List (Optional Integer) +) += [1] : Optional Integer + +./head +Integer +([[] : Optional Integer, [] : Optional Integer] : List (Optional Integer)) += [] : Optional Integer + +./head Integer ([] : List (Optional Integer)) += [] : 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) + +in head diff --git a/Prelude/Optional/last b/Prelude/Optional/last new file mode 100644 --- /dev/null +++ b/Prelude/Optional/last @@ -0,0 +1,36 @@ +{- +Returns the last non-empty `Optional` value in a `List` + +Examples: + +``` +./last +Integer +( [[] : Optional Integer, [1] : Optional Integer, [2] : Optional Integer] + : List (Optional Integer) +) += [2] : Optional Integer + +./last +Integer +([[] : Optional Integer, [] : Optional Integer] : List (Optional Integer)) += [] : Optional Integer + +./last Integer ([] : List (Optional Integer)) += [] : 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) + +in last diff --git a/Prelude/Optional/map b/Prelude/Optional/map new file mode 100644 --- /dev/null +++ b/Prelude/Optional/map @@ -0,0 +1,26 @@ +{- +Transform an `Optional` value with a function + +Examples: + +``` +./map Natural Bool Natural/even ([+3] : Optional Natural) += [False] : Optional Bool + +./map Natural Bool Natural/even ([] : Optional Natural) += [] : 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) + +in map diff --git a/Prelude/Optional/toList b/Prelude/Optional/toList new file mode 100644 --- /dev/null +++ b/Prelude/Optional/toList @@ -0,0 +1,17 @@ +{- +Convert an `Optional` value into the equivalent `List` + +Examples: + +``` +./toList Integer ([1] : Optional Integer) = [1] : List Integer + +./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) + +in toList diff --git a/Prelude/Optional/unzip b/Prelude/Optional/unzip new file mode 100644 --- /dev/null +++ b/Prelude/Optional/unzip @@ -0,0 +1,41 @@ +{- +Unzip an `Optional` value into two separate `Optional` values + +Examples: + +``` +./unzip +Text +Bool +([{ _1 = "ABC", _2 = True }] : Optional { _1 : Text, _2 : Bool }) += { _1 = ["ABC"] : Optional Text, _2 = [True] : Optional Bool } + +./unzip Text Bool ([] : Optional { _1 : Text, _2 : Bool }) += { _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) + } + +in unzip diff --git a/Prelude/Text/concat b/Prelude/Text/concat new file mode 100644 --- /dev/null +++ b/Prelude/Text/concat @@ -0,0 +1,16 @@ +{- +Concatenate all the `Text` values in a `List` + +Examples: + +``` +./concat (["ABC", "DEF", "GHI"] : List Text) = "ABCDEFGHI" + +./concat ([] : List Text) = "" +``` +-} +let concat : List Text → Text + = λ(xs : List Text) + → List/fold Text xs Text (λ(x : Text) → λ(y : Text) → x ++ y) "" + +in concat diff --git a/dhall.cabal b/dhall.cabal --- a/dhall.cabal +++ b/dhall.cabal @@ -1,5 +1,5 @@ Name: dhall -Version: 1.2.0 +Version: 1.3.0 Cabal-Version: >=1.8.0.2 Build-Type: Simple Tested-With: GHC == 7.10.2, GHC == 8.0.1 @@ -22,7 +22,57 @@ . Read "Dhall.Tutorial" to learn how to use this library Category: Compiler -Extra-Source-Files: CHANGELOG.md +Extra-Source-Files: + CHANGELOG.md + Prelude/Bool/and + Prelude/Bool/build + Prelude/Bool/even + Prelude/Bool/fold + Prelude/Bool/not + Prelude/Bool/odd + Prelude/Bool/or + Prelude/Bool/show + Prelude/Double/show + Prelude/Integer/show + Prelude/List/all + Prelude/List/any + Prelude/List/build + Prelude/List/concat + Prelude/List/filter + Prelude/List/fold + Prelude/List/generate + Prelude/List/head + Prelude/List/indexed + Prelude/List/iterate + Prelude/List/last + Prelude/List/length + Prelude/List/map + Prelude/List/null + Prelude/List/replicate + Prelude/List/reverse + Prelude/List/shifted + Prelude/List/unzip + Prelude/Monoid + Prelude/Natural/build + Prelude/Natural/enumerate + Prelude/Natural/even + Prelude/Natural/fold + Prelude/Natural/isZero + Prelude/Natural/odd + Prelude/Natural/product + Prelude/Natural/show + Prelude/Natural/sum + Prelude/Natural/toInteger + Prelude/Optional/build + Prelude/Optional/concat + Prelude/Optional/fold + Prelude/Optional/head + Prelude/Optional/last + Prelude/Optional/map + Prelude/Optional/toList + Prelude/Optional/unzip + Prelude/Text/concat + Source-Repository head Type: git Location: https://github.com/Gabriel439/Haskell-Dhall-Library @@ -33,6 +83,7 @@ base >= 4.8.0.0 && < 5 , ansi-wl-pprint < 0.7 , bytestring < 0.11, + charset < 0.4 , containers >= 0.5.0.0 && < 0.6 , http-client >= 0.4.30 && < 0.6 , http-client-tls >= 0.2.0 && < 0.4 , @@ -46,7 +97,7 @@ transformers >= 0.2.0.0 && < 0.6 , trifecta >= 1.6 && < 1.7 , unordered-containers >= 0.1.3.0 && < 0.3 , - vector >= 0.11.0.0 && < 0.12 + vector >= 0.11.0.0 && < 0.13 Exposed-Modules: Dhall, Dhall.Context, @@ -67,3 +118,23 @@ trifecta >= 1.6 && < 1.7, 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 + Main-Is: Tests.hs + GHC-Options: -Wall + Other-Modules: + Examples + Normalization + Util + Build-Depends: + base >= 4 && < 5 , + dhall , + neat-interpolation >= 0.3.2.1 && < 0.4 , + tasty >= 0.11.2 && < 0.12, + tasty-hunit >= 0.9.2 && < 0.10, + text >= 0.11.1.0 && < 1.3 , + vector >= 0.11.0.0 && < 0.12 diff --git a/exec/Main.hs b/exec/Main.hs --- a/exec/Main.hs +++ b/exec/Main.hs @@ -7,16 +7,20 @@ 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) +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 @@ -27,6 +31,7 @@ data Options = Options { explain :: Bool "Explain error messages in more detail" + , version :: Bool "Display version and exit" } deriving (Generic) instance ParseRecord Options @@ -34,7 +39,9 @@ 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 diff --git a/src/Dhall/Core.hs b/src/Dhall/Core.hs --- a/src/Dhall/Core.hs +++ b/src/Dhall/Core.hs @@ -36,14 +36,17 @@ -- * Miscellaneous , internalError + , reservedIdentifiers ) where #if MIN_VERSION_base(4,8,0) #else import Control.Applicative (Applicative(..), (<$>)) #endif +import Control.Applicative (empty) import Data.Bifunctor (Bifunctor(..)) import Data.Foldable +import Data.HashSet (HashSet) import Data.Map (Map) import Data.Monoid ((<>)) import Data.String (IsString(..)) @@ -57,6 +60,7 @@ import Prelude hiding (FilePath, succ) import qualified Control.Monad +import qualified Data.HashSet import qualified Data.Map import qualified Data.Maybe import qualified Data.Text @@ -84,7 +88,7 @@ Note that Dhall does not support functions from terms to types and therefore Dhall is not a dependently typed language -} -data Const = Type | Kind deriving (Show, Bounded, Enum) +data Const = Type | Kind deriving (Show, Eq, Bounded, Enum) instance Buildable Const where build = buildConst @@ -182,7 +186,7 @@ = Const Const -- | > Var (V x 0) ~ x -- > Var (V x n) ~ x@n - | Var Var + | Var Var -- | > Lam x A b ~ λ(x : A) -> b | Lam Text (Expr s a) (Expr s a) -- | > Pi "_" A B ~ A -> B @@ -223,6 +227,10 @@ | NaturalEven -- | > NaturalOdd ~ Natural/odd | NaturalOdd + -- | > NaturalToInteger ~ Natural/toInteger + | NaturalToInteger + -- | > NaturalShow ~ Natural/show + | NaturalShow -- | > NaturalPlus x y ~ x + y | NaturalPlus (Expr s a) (Expr s a) -- | > NaturalTimes x y ~ x * y @@ -231,10 +239,14 @@ | Integer -- | > IntegerLit n ~ n | IntegerLit Integer + -- | > IntegerShow ~ Integer/show + | IntegerShow -- | > Double ~ Double | Double -- | > DoubleLit n ~ n | DoubleLit Double + -- | > DoubleShow ~ Double/show + | DoubleShow -- | > Text ~ Text | Text -- | > TextLit t ~ t @@ -253,7 +265,7 @@ -- | > ListLength ~ List/length | ListLength -- | > ListHead ~ List/head - | ListHead + | ListHead -- | > ListLast ~ List/last | ListLast -- | > ListIndexed ~ List/indexed @@ -267,16 +279,20 @@ | OptionalLit (Expr s a) (Vector (Expr s a)) -- | > OptionalFold ~ Optional/fold | OptionalFold + -- | > OptionalBuild ~ Optional/build + | OptionalBuild -- | > Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 } | Record (Map Text (Expr s a)) -- | > RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 } | RecordLit (Map Text (Expr s a)) -- | > Union [(k1, t1), (k2, t2)] ~ < k1 : t1 | k2 : t2 > | Union (Map Text (Expr s a)) - -- | > UnionLit (k1, v1) [(k2, t2), (k3, t3)] ~ < k1 = t1 | k2 : t2 | k3 : t3 > + -- | > UnionLit (k1, v1) [(k2, t2), (k3, t3)] ~ < k1 = t1 | k2 : t2 | k3 : t3 > | UnionLit Text (Expr s a) (Map Text (Expr s a)) -- | > Combine x y ~ x ∧ y | Combine (Expr s a) (Expr s a) + -- | > CombineRight x y ~ x ⫽ y + | Prefer (Expr s a) (Expr s a) -- | > Merge x y t ~ merge x y : t | Merge (Expr s a) (Expr s a) (Expr s a) -- | > Field e x ~ e.x @@ -285,7 +301,7 @@ | Note s (Expr s a) -- | > Embed path ~ path | Embed a - deriving (Functor, Foldable, Traversable, Show) + deriving (Functor, Foldable, Traversable, Show, Eq) instance Applicative (Expr s) where pure = Embed @@ -316,12 +332,16 @@ NaturalIsZero >>= _ = NaturalIsZero NaturalEven >>= _ = NaturalEven NaturalOdd >>= _ = NaturalOdd + NaturalToInteger >>= _ = NaturalToInteger + NaturalShow >>= _ = NaturalShow NaturalPlus a b >>= k = NaturalPlus (a >>= k) (b >>= k) NaturalTimes a b >>= k = NaturalTimes (a >>= k) (b >>= k) Integer >>= _ = Integer IntegerLit a >>= _ = IntegerLit a + IntegerShow >>= _ = IntegerShow Double >>= _ = Double DoubleLit a >>= _ = DoubleLit a + DoubleShow >>= _ = DoubleShow Text >>= _ = Text TextLit a >>= _ = TextLit a TextAppend a b >>= k = TextAppend (a >>= k) (b >>= k) @@ -337,11 +357,13 @@ Optional >>= _ = Optional OptionalLit a b >>= k = OptionalLit (a >>= k) (fmap (>>= k) b) OptionalFold >>= _ = OptionalFold + OptionalBuild >>= _ = OptionalBuild Record a >>= k = Record (fmap (>>= k) a) RecordLit a >>= k = RecordLit (fmap (>>= k) a) Union a >>= k = Union (fmap (>>= k) a) UnionLit a b c >>= k = UnionLit a (b >>= k) (fmap (>>= k) c) Combine a b >>= k = Combine (a >>= k) (b >>= k) + Prefer a b >>= k = Prefer (a >>= k) (b >>= k) Merge a b c >>= k = Merge (a >>= k) (b >>= k) (c >>= k) Field a b >>= k = Field (a >>= k) b Note a b >>= k = Note a (b >>= k) @@ -369,12 +391,16 @@ first _ NaturalIsZero = NaturalIsZero first _ NaturalEven = NaturalEven first _ NaturalOdd = NaturalOdd + first _ NaturalToInteger = NaturalToInteger + first _ NaturalShow = NaturalShow first k (NaturalPlus a b ) = NaturalPlus (first k a) (first k b) first k (NaturalTimes a b) = NaturalTimes (first k a) (first k b) first _ Integer = Integer first _ (IntegerLit a ) = IntegerLit a + first _ IntegerShow = IntegerShow first _ Double = Double first _ (DoubleLit a ) = DoubleLit a + first _ DoubleShow = DoubleShow first _ Text = Text first _ (TextLit a ) = TextLit a first k (TextAppend a b ) = TextAppend (first k a) (first k b) @@ -390,11 +416,13 @@ first _ Optional = Optional first k (OptionalLit a b ) = OptionalLit (first k a) (fmap (first k) b) first _ OptionalFold = OptionalFold + first _ OptionalBuild = OptionalBuild first k (Record a ) = Record (fmap (first k) a) first k (RecordLit a ) = RecordLit (fmap (first k) a) first k (Union a ) = Union (fmap (first k) a) first k (UnionLit a b c ) = UnionLit a (first k b) (fmap (first k) c) first k (Combine a b ) = Combine (first k a) (first k b) + first k (Prefer a b ) = Prefer (first k a) (first k b) first k (Merge a b c ) = Merge (first k a) (first k b) (first k c) first k (Field a b ) = Field (first k a) b first k (Note a b ) = Note (k a) (first k b) @@ -422,7 +450,10 @@ -- | Builder corresponding to the @label@ token in "Dhall.Parser" buildLabel :: Text -> Builder -buildLabel = build +buildLabel label = + if Data.HashSet.member label reservedIdentifiersText + then "`" <> build label <> "`" + else build label -- | Builder corresponding to the @number@ token in "Dhall.Parser" buildNumber :: Integer -> Builder @@ -536,28 +567,34 @@ -- | Builder corresponding to the @exprC4@ parser in "Dhall.Parser" buildExprC4 :: Buildable a => Expr s a -> Builder -buildExprC4 (Combine a b) = buildExprC5 a <> " ∧ " <> buildExprC4 b -buildExprC4 (Note _ b) = buildExprC4 b -buildExprC4 a = buildExprC5 a +buildExprC4 (Combine a b) = buildExprC5 a <> " ∧ " <> buildExprC4 b +buildExprC4 (Note _ b) = buildExprC4 b +buildExprC4 a = buildExprC5 a -- | Builder corresponding to the @exprC5@ parser in "Dhall.Parser" buildExprC5 :: Buildable a => Expr s a -> Builder -buildExprC5 (NaturalTimes a b) = buildExprC6 a <> " * " <> buildExprC5 b -buildExprC5 (Note _ b) = buildExprC5 b -buildExprC5 a = buildExprC6 a +buildExprC5 (Prefer a b) = buildExprC6 a <> " ⫽ " <> buildExprC5 b +buildExprC5 (Note _ b) = buildExprC5 b +buildExprC5 a = buildExprC6 a -- | Builder corresponding to the @exprC6@ parser in "Dhall.Parser" buildExprC6 :: Buildable a => Expr s a -> Builder -buildExprC6 (BoolEQ a b) = buildExprC7 a <> " == " <> buildExprC6 b -buildExprC6 (Note _ b) = buildExprC6 b -buildExprC6 a = buildExprC7 a +buildExprC6 (NaturalTimes a b) = buildExprC7 a <> " * " <> buildExprC6 b +buildExprC6 (Note _ b) = buildExprC6 b +buildExprC6 a = buildExprC7 a -- | Builder corresponding to the @exprC7@ parser in "Dhall.Parser" buildExprC7 :: Buildable a => Expr s a -> Builder -buildExprC7 (BoolNE a b) = buildExprD a <> " != " <> buildExprC7 b +buildExprC7 (BoolEQ a b) = buildExprC8 a <> " == " <> buildExprC7 b buildExprC7 (Note _ b) = buildExprC7 b -buildExprC7 a = buildExprD a +buildExprC7 a = buildExprC8 a +-- | Builder corresponding to the @exprC8@ parser in "Dhall.Parser" +buildExprC8 :: Buildable a => Expr s a -> Builder +buildExprC8 (BoolNE a b) = buildExprD a <> " != " <> buildExprC8 b +buildExprC8 (Note _ b) = buildExprC8 b +buildExprC8 a = buildExprD a + -- | Builder corresponding to the @exprD@ parser in "Dhall.Parser" buildExprD :: Buildable a => Expr s a -> Builder buildExprD (App a b) = buildExprD a <> " " <> buildExprE b @@ -590,10 +627,18 @@ "Natural/even" buildExprF NaturalOdd = "Natural/odd" +buildExprF NaturalToInteger = + "Natural/toInteger" +buildExprF NaturalShow = + "Natural/show" buildExprF Integer = "Integer" +buildExprF IntegerShow = + "Integer/show" buildExprF Double = "Double" +buildExprF DoubleShow = + "Double/show" buildExprF Text = "Text" buildExprF List = @@ -616,6 +661,8 @@ "Optional" buildExprF OptionalFold = "Optional/fold" +buildExprF OptionalBuild = + "Optional/build" buildExprF (BoolLit True) = "True" buildExprF (BoolLit False) = @@ -861,6 +908,8 @@ shift _ _ NaturalIsZero = NaturalIsZero shift _ _ NaturalEven = NaturalEven shift _ _ NaturalOdd = NaturalOdd +shift _ _ NaturalToInteger = NaturalToInteger +shift _ _ NaturalShow = NaturalShow shift d v (NaturalPlus a b) = NaturalPlus a' b' where a' = shift d v a @@ -871,8 +920,10 @@ b' = shift d v b shift _ _ Integer = Integer shift _ _ (IntegerLit a) = IntegerLit a +shift _ _ IntegerShow = IntegerShow shift _ _ Double = Double shift _ _ (DoubleLit a) = DoubleLit a +shift _ _ DoubleShow = DoubleShow shift _ _ Text = Text shift _ _ (TextLit a) = TextLit a shift d v (TextAppend a b) = TextAppend a' b' @@ -897,6 +948,7 @@ a' = shift d v a b' = fmap (shift d v) b shift _ _ OptionalFold = OptionalFold +shift _ _ OptionalBuild = OptionalBuild shift d v (Record a) = Record a' where a' = fmap (shift d v) a @@ -914,6 +966,10 @@ where a' = shift d v a b' = shift d v b +shift d v (Prefer a b) = Prefer a' b' + where + a' = shift d v a + b' = shift d v b shift d v (Merge a b c) = Merge a' b' c' where a' = shift d v a @@ -992,6 +1048,8 @@ subst _ _ NaturalIsZero = NaturalIsZero subst _ _ NaturalEven = NaturalEven subst _ _ NaturalOdd = NaturalOdd +subst _ _ NaturalToInteger = NaturalToInteger +subst _ _ NaturalShow = NaturalShow subst x e (NaturalPlus a b) = NaturalPlus a' b' where a' = subst x e a @@ -1002,8 +1060,10 @@ b' = subst x e b subst _ _ Integer = Integer subst _ _ (IntegerLit a) = IntegerLit a +subst _ _ IntegerShow = IntegerShow subst _ _ Double = Double subst _ _ (DoubleLit a) = DoubleLit a +subst _ _ DoubleShow = DoubleShow subst _ _ Text = Text subst _ _ (TextLit a) = TextLit a subst x e (TextAppend a b) = TextAppend a' b' @@ -1028,6 +1088,7 @@ a' = subst x e a b' = fmap (subst x e) b subst _ _ OptionalFold = OptionalFold +subst _ _ OptionalBuild = OptionalBuild subst x e (Record kts) = Record (fmap (subst x e) kts) subst x e (RecordLit kvs) = RecordLit (fmap (subst x e) kvs) subst x e (Union kts) = Union (fmap (subst x e) kts) @@ -1036,6 +1097,10 @@ where a' = subst x e a b' = subst x e b +subst x e (Prefer a b) = Prefer a' b' + where + a' = subst x e a + b' = subst x e b subst x e (Merge a b c) = Merge a' b' c' where a' = subst x e a @@ -1082,11 +1147,14 @@ -- fold/build fusion for `List` App (App ListBuild _) (App (App ListFold _) e') -> normalize e' App (App ListFold _) (App (App ListBuild _) e') -> normalize e' - -- fold/build fusion for `Natural` App NaturalBuild (App NaturalFold e') -> normalize e' App NaturalFold (App NaturalBuild e') -> normalize e' + -- fold/build fusion for `Optional` + App (App OptionalBuild _) (App (App OptionalFold _) e') -> normalize e' + App (App OptionalFold _) (App (App OptionalBuild _) e') -> normalize e' + App (App (App (App NaturalFold (NaturalLit n0)) _) succ') zero -> normalize (go n0) where @@ -1112,6 +1180,26 @@ App NaturalIsZero (NaturalLit n) -> BoolLit (n == 0) App NaturalEven (NaturalLit n) -> BoolLit (even n) App NaturalOdd (NaturalLit n) -> BoolLit (odd n) + App NaturalToInteger (NaturalLit n) -> IntegerLit (toInteger n) + App NaturalShow (NaturalLit n) -> TextLit ("+" <> buildNatural n) + App IntegerShow (IntegerLit n) -> TextLit (buildNumber n) + App DoubleShow (DoubleLit n) -> TextLit (buildDouble n) + App (App OptionalBuild t) k + | check -> OptionalLit t k' + | otherwise -> App f' a' + where + labeled = normalize (App (App (App k (App Optional t)) "Just") "Nothing") + + k' = go labeled + where + go (App (Var "Just") e') = pure e' + go (Var "Nothing") = empty + go _ = internalError text + check = go labeled + where + go (App (Var "Just") _) = True + go (Var "Nothing") = True + go _ = False App (App ListBuild t) k | check -> ListLit (Just t) (buildVector k') | otherwise -> App f' a' @@ -1228,6 +1316,8 @@ NaturalIsZero -> NaturalIsZero NaturalEven -> NaturalEven NaturalOdd -> NaturalOdd + NaturalToInteger -> NaturalToInteger + NaturalShow -> NaturalShow NaturalPlus x y -> case x' of NaturalLit xn -> @@ -1250,8 +1340,10 @@ y' = normalize y Integer -> Integer IntegerLit n -> IntegerLit n + IntegerShow -> IntegerShow Double -> Double DoubleLit n -> DoubleLit n + DoubleShow -> DoubleShow Text -> Text TextLit t -> TextLit t TextAppend x y -> @@ -1282,6 +1374,7 @@ t' = normalize t es' = fmap normalize es OptionalFold -> OptionalFold + OptionalBuild -> OptionalBuild Record kts -> Record kts' where kts' = fmap normalize kts @@ -1304,6 +1397,17 @@ _ -> Combine x y _ -> Combine x y in combine (normalize x0) (normalize y0) + Prefer x y -> + case x' of + RecordLit kvsX -> + case y' of + RecordLit kvsY -> + RecordLit (fmap normalize (Data.Map.union kvsY kvsX)) + _ -> Prefer x' y' + _ -> Prefer x' y' + where + x' = normalize x + y' = normalize y Merge x y t -> case x' of RecordLit kvsX -> @@ -1347,6 +1451,7 @@ App f a -> isNormalized f && isNormalized a && case App f a of App (Lam _ _ _) _ -> False + -- fold/build fusion for `List` App (App ListBuild _) (App (App ListFold _) _) -> False App (App ListFold _) (App (App ListBuild _) _) -> False @@ -1354,6 +1459,10 @@ App NaturalBuild (App NaturalFold _) -> False App NaturalFold (App NaturalBuild _) -> False + -- fold/build fusion for `Optional` + App (App OptionalBuild _) (App (App OptionalFold _) _) -> False + App (App OptionalFold _) (App (App OptionalBuild _) _) -> False + App (App (App (App NaturalFold (NaturalLit _)) _) _) _ -> False App NaturalBuild k0 -> isNormalized k0 && not (check0 k0) where @@ -1367,6 +1476,19 @@ App NaturalIsZero (NaturalLit _) -> False App NaturalEven (NaturalLit _) -> False App NaturalOdd (NaturalLit _) -> False + App NaturalShow (NaturalLit _) -> False + App NaturalToInteger (NaturalLit _) -> False + App IntegerShow (IntegerLit _) -> False + App DoubleShow (DoubleLit _) -> False + App (App OptionalBuild t) k0 -> isNormalized t && isNormalized k0 && not (check0 k0) + where + check0 (Lam _ _ (Lam just _ (Lam nothing _ k))) = check1 just nothing k + check0 _ = False + + check1 just nothing (App (Var (V just' n)) _) = + just == just' && n == (if just == nothing then 1 else 0) + check1 _ nothing (Var (V nothing' 0)) = nothing == nothing' + check1 _ _ _ = False App (App ListBuild t) k0 -> isNormalized t && isNormalized k0 && not (check0 k0) where check0 (Lam _ _ (Lam cons _ (Lam nil _ k))) = check1 cons nil k @@ -1428,6 +1550,8 @@ NaturalIsZero -> True NaturalEven -> True NaturalOdd -> True + NaturalShow -> True + NaturalToInteger -> True NaturalPlus x y -> isNormalized x && isNormalized y && case x of NaturalLit _ -> @@ -1444,8 +1568,10 @@ _ -> True Integer -> True IntegerLit _ -> True + IntegerShow -> True Double -> True DoubleLit _ -> True + DoubleShow -> True Text -> True TextLit _ -> True TextAppend x y -> isNormalized x && isNormalized y && @@ -1467,17 +1593,25 @@ Optional -> True OptionalLit t es -> isNormalized t && all isNormalized es OptionalFold -> True + OptionalBuild -> True Record kts -> all isNormalized kts RecordLit kvs -> all isNormalized kvs Union kts -> all isNormalized kts UnionLit _ v kvs -> isNormalized v && all isNormalized kvs - Combine x0 y0 -> isNormalized x0 && isNormalized y0 && combine x0 y0 + Combine x y -> isNormalized x && isNormalized y && combine where - combine x y = case x of + combine = case x of RecordLit _ -> case y of RecordLit _ -> False _ -> True _ -> True + Prefer x y -> isNormalized x && isNormalized y && combine + where + combine = case x of + RecordLit _ -> case y of + RecordLit _ -> False + _ -> True + _ -> True Merge x y t -> isNormalized x && isNormalized y && isNormalized t && case x of RecordLit kvsX -> @@ -1488,7 +1622,7 @@ Nothing -> True _ -> True _ -> True - Field r x -> isNormalized r && + Field r x -> isNormalized r && case r of RecordLit kvs -> case Data.Map.lookup x kvs of @@ -1539,3 +1673,47 @@ return (0, 1, mv) (len, _, mv) <- f cons nil return (Data.Vector.Mutable.slice 0 len mv) )) + +reservedIdentifiers :: HashSet String +reservedIdentifiers = + Data.HashSet.fromList + [ "let" + , "in" + , "Type" + , "Kind" + , "forall" + , "Bool" + , "True" + , "False" + , "merge" + , "if" + , "then" + , "else" + , "as" + , "Natural" + , "Natural/fold" + , "Natural/build" + , "Natural/isZero" + , "Natural/even" + , "Natural/odd" + , "Natural/toInteger" + , "Natural/show" + , "Integer" + , "Integer/show" + , "Double" + , "Double/show" + , "Text" + , "List" + , "List/build" + , "List/fold" + , "List/length" + , "List/head" + , "List/last" + , "List/indexed" + , "List/reverse" + , "Optional" + , "Optional/fold" + ] + +reservedIdentifiersText :: HashSet Text +reservedIdentifiersText = Data.HashSet.map Text.pack reservedIdentifiers diff --git a/src/Dhall/Import.hs b/src/Dhall/Import.hs --- a/src/Dhall/Import.hs +++ b/src/Dhall/Import.hs @@ -325,9 +325,9 @@ Nothing -> do let settings = HTTP.tlsManagerSettings #if MIN_VERSION_http_client(0,5,0) - { HTTP.managerResponseTimeout = HTTP.responseTimeoutMicro 1000000 } -- 1 second + { HTTP.managerResponseTimeout = HTTP.responseTimeoutMicro (30 * 1000 * 1000) } -- 30 seconds #else - { HTTP.managerResponseTimeout = Just 1000000 } -- 1 second + { HTTP.managerResponseTimeout = Just (30 * 1000 * 1000) } -- 30 seconds #endif m <- liftIO (HTTP.newManager settings) zoom manager (State.put (Just m)) diff --git a/src/Dhall/Parser.hs b/src/Dhall/Parser.hs --- a/src/Dhall/Parser.hs +++ b/src/Dhall/Parser.hs @@ -22,6 +22,7 @@ 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(..)) @@ -41,7 +42,7 @@ import Text.Trifecta.Delta (Delta) import qualified Data.Char -import qualified Data.HashSet +import qualified Data.CharSet import qualified Data.Map import qualified Data.ByteString.Lazy import qualified Data.List @@ -92,7 +93,7 @@ instance TokenParsing Parser where someSpace = - Text.Parser.Token.Style.buildSomeSpaceParser + Text.Parser.Token.Style.buildSomeSpaceParser (Parser someSpace) Text.Parser.Token.Style.haskellCommentStyle @@ -113,41 +114,8 @@ , _styleStart = Text.Parser.Char.oneOf (['A'..'Z'] ++ ['a'..'z'] ++ "_") , _styleLetter = - Text.Parser.Char.oneOf (['A'..'Z'] ++ ['a'..'z'] ++ ['0'..'9'] ++ "_/") - , _styleReserved = Data.HashSet.fromList - [ "let" - , "in" - , "Type" - , "Kind" - , "forall" - , "Bool" - , "True" - , "False" - , "merge" - , "if" - , "then" - , "else" - , "as" - , "Natural" - , "Natural/fold" - , "Natural/build" - , "Natural/isZero" - , "Natural/even" - , "Natural/odd" - , "Integer" - , "Double" - , "Text" - , "List" - , "List/build" - , "List/fold" - , "List/length" - , "List/head" - , "List/last" - , "List/indexed" - , "List/reverse" - , "Optional" - , "Optional/fold" - ] + Text.Parser.Char.oneOf (['A'..'Z'] ++ ['a'..'z'] ++ ['0'..'9'] ++ "_-/") + , _styleReserved = reservedIdentifiers , _styleHighlight = Identifier , _styleReservedHighlight = ReservedIdentifier } @@ -262,9 +230,21 @@ combine :: Parser () combine = symbol "/\\" <|> symbol "∧" +prefer :: Parser () +prefer = symbol "//" <|> symbol "⫽" + label :: Parser Text -label = Text.Parser.Token.ident identifierStyle "label" +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_ @@ -389,14 +369,15 @@ a <- pA try (do _ <- pOp "operator"; b <- pB; return (op a b)) <|> pure a ) - exprC0 = chain exprC1 (symbol "||") BoolOr exprC0 - exprC2 = chain exprC3 (symbol "++") TextAppend exprC2 - exprC1 = chain exprC2 (symbol "+" ) NaturalPlus exprC1 - exprC3 = chain exprC4 (symbol "&&") BoolAnd exprC3 - exprC4 = chain exprC5 combine Combine exprC4 - exprC5 = chain exprC6 (symbol "*" ) NaturalTimes exprC5 - exprC6 = chain exprC7 (symbol "==") BoolEQ exprC6 - exprC7 = chain (exprD embedded) (symbol "!=") BoolNE exprC7 + exprC0 = chain exprC1 (symbol "||") BoolOr exprC0 + exprC1 = chain exprC2 (symbol "+" ) NaturalPlus exprC1 + exprC2 = chain exprC3 (symbol "++") TextAppend exprC2 + exprC3 = chain exprC4 (symbol "&&") BoolAnd exprC3 + exprC4 = chain exprC5 combine Combine exprC4 + exprC5 = chain exprC6 prefer Prefer exprC5 + exprC6 = chain exprC7 (symbol "*" ) NaturalTimes exprC6 + exprC7 = chain exprC8 (symbol "==") BoolEQ exprC7 + exprC8 = chain (exprD embedded) (symbol "!=") BoolNE exprC8 -- 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 @@ -426,177 +407,202 @@ exprF :: Show a => Parser a -> Parser (Expr Src a) exprF embedded = choice - [ noted (try exprF26) - , noted (try exprF25) - , noted exprF24 - , noted exprF27 - , noted (try exprF28) - , noted exprF29 - , noted (try exprF30) - , noted exprF31 - , noted exprF32 - , noted exprF33 + [ 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 exprF03 - , noted exprF04 - , noted exprF05 - , noted exprF06 - , noted exprF07 - , noted exprF12 - , noted exprF13 - , noted exprF14 - , noted exprF15 - , noted exprF16 - , noted exprF17 - , noted exprF18 - , noted exprF20 - , noted exprF21 - , noted exprF19 - , noted exprF02 - , noted exprF08 - , noted exprF09 - , noted exprF10 - , noted exprF11 - , noted exprF22 - , noted exprF23 - , noted exprF01 + [ 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 exprF00 - , exprF34 + , noted exprVar + , exprParens ] where - exprF00 = do + exprVar = do a <- var return (Var a) - exprF01 = do + exprConst = do a <- const return (Const a) - exprF02 = do + exprNatural = do reserve "Natural" return Natural - exprF03 = do + exprNaturalFold = do reserve "Natural/fold" return NaturalFold - exprF04 = do + exprNaturalBuild = do reserve "Natural/build" return NaturalBuild - exprF05 = do + exprNaturalIsZero = do reserve "Natural/isZero" return NaturalIsZero - exprF06 = do + exprNaturalEven = do reserve "Natural/even" return NaturalEven - exprF07 = do + exprNaturalOdd = do reserve "Natural/odd" return NaturalOdd - exprF08 = do + exprNaturalToInteger = do + reserve "Natural/toInteger" + return NaturalToInteger + + exprNaturalShow = do + reserve "Natural/show" + return NaturalShow + + exprInteger = do reserve "Integer" return Integer - exprF09 = do + exprIntegerShow = do + reserve "Integer/show" + return IntegerShow + + exprDouble = do reserve "Double" return Double - exprF10 = do + exprDoubleShow = do + reserve "Double/show" + return DoubleShow + + exprText = do reserve "Text" return Text - exprF11 = do + exprList = do reserve "List" return List - exprF12 = do + exprListBuild = do reserve "List/build" return ListBuild - exprF13 = do + exprListFold = do reserve "List/fold" return ListFold - exprF14 = do + exprListLength = do reserve "List/length" return ListLength - exprF15 = do + exprListHead = do reserve "List/head" return ListHead - exprF16 = do + exprListLast = do reserve "List/last" return ListLast - exprF17 = do + exprListIndexed = do reserve "List/indexed" return ListIndexed - exprF18 = do + exprListReverse = do reserve "List/reverse" return ListReverse - exprF19 = do + exprOptional = do reserve "Optional" return Optional - exprF20 = do + exprOptionalFold = do reserve "Optional/fold" return OptionalFold - exprF21 = do + exprOptionalBuild = do + reserve "Optional/build" + return OptionalBuild + + exprBool = do reserve "Bool" return Bool - exprF22 = do + exprBoolLitTrue = do reserve "True" return (BoolLit True) - exprF23 = do + exprBoolLitFalse = do reserve "False" return (BoolLit False) - exprF24 = do + exprIntegerLit = do a <- Text.Parser.Token.integer return (IntegerLit a) - exprF25 = (do + exprNaturalLit = (do _ <- Text.Parser.Char.char '+' a <- Text.Parser.Token.natural return (NaturalLit (fromIntegral a)) ) "natural" - exprF26 = do + 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)) - exprF27 = do + exprStringLiteral = do a <- stringLiteral return (TextLit a) - exprF28 = record embedded "record type" + exprRecordType = record embedded "record type" - exprF29 = recordLit embedded "record literal" + exprRecordLiteral = recordLit embedded "record literal" - exprF30 = union embedded "union type" + exprUnionType = union embedded "union type" - exprF31 = unionLit embedded "union literal" + exprUnionLiteral = unionLit embedded "union literal" - exprF32 = listLit embedded "list literal" + exprListLiteral = listLit embedded "list literal" - exprF33 = do + exprImport = do a <- embedded "import" return (Embed a) - exprF34 = do + exprParens = do symbol "(" a <- exprA embedded symbol ")" @@ -734,6 +740,16 @@ pathMode <- rawText <|> pure Code return (Path {..}) +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 @@ -742,26 +758,27 @@ where file0 = do a <- Text.Parser.Char.string "/" - b <- many (Text.Parser.Char.satisfy (not . Data.Char.isSpace)) + 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 () return (File Homeless (Filesystem.Path.CurrentOS.decodeString (a <> b))) file1 = do a <- Text.Parser.Char.string "./" - b <- many (Text.Parser.Char.satisfy (not . Data.Char.isSpace)) + b <- many (Text.Parser.Char.satisfy pathChar) return (File Homeless (Filesystem.Path.CurrentOS.decodeString (a <> b))) file2 = do a <- Text.Parser.Char.string "../" - b <- many (Text.Parser.Char.satisfy (not . Data.Char.isSpace)) + b <- many (Text.Parser.Char.satisfy pathChar) 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 (not . Data.Char.isSpace)) + b <- many (Text.Parser.Char.satisfy pathChar) return (File Home (Filesystem.Path.CurrentOS.decodeString b)) url :: Parser PathType @@ -770,18 +787,18 @@ where url0 = do a <- Text.Parser.Char.string "https://" - b <- many (Text.Parser.Char.satisfy (not . Data.Char.isSpace)) + b <- many (Text.Parser.Char.satisfy pathChar) return (URL (Data.Text.Lazy.pack (a <> b))) url1 = do a <- Text.Parser.Char.string "http://" - b <- many (Text.Parser.Char.satisfy (not . Data.Char.isSpace)) + b <- many (Text.Parser.Char.satisfy pathChar) return (URL (Data.Text.Lazy.pack (a <> b))) env :: Parser PathType env = do _ <- Text.Parser.Char.string "env:" - a <- many (Text.Parser.Char.satisfy (not . Data.Char.isSpace)) + a <- many (Text.Parser.Char.satisfy pathChar) return (Env (Data.Text.Lazy.pack a)) -- | A parsing error diff --git a/src/Dhall/Tutorial.hs b/src/Dhall/Tutorial.hs --- a/src/Dhall/Tutorial.hs +++ b/src/Dhall/Tutorial.hs @@ -456,12 +456,12 @@ -- -- __Exercise:__ There is a @not@ function hosted online here: -- --- +-- -- -- Visit that link and read the documentation. Then try to guess what this -- code returns: -- --- > >>> input auto "https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool +-- > >>> input auto "https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool -- > ??? -- -- Run the code to test your guess @@ -766,37 +766,40 @@ -- $combine -- --- You can combine two records, using the @(/\\)@ operator or the --- corresponding Unicode @(∧)@ (U+2227) operator: +-- You can combine two records, using either the @(//)@ operator or the +-- @(/\\)@ operator. -- +-- The @(//)@ operator (or @(⫽)@ U+2AFD) combines the fields of both records, +-- preferring fields from the right record if they share fields in common: +-- -- > $ dhall --- > { foo = 1, bar = "ABC" } /\ { baz = True } +-- > { foo = 1, bar = "ABC" } // { baz = True } -- > -- > { bar : Text, baz : Bool, foo : Integer } -- > -- > { bar = "ABC", baz = True, foo = 1 } --- -- > $ dhall --- > { foo = 1, bar = "ABC" } ∧ { baz = True } -- Fancy unicode +-- > { foo = 1, bar = "ABC" } ⫽ { bar = True } -- Fancy unicode -- > --- > { bar : Text, baz : Bool, foo : Integer } +-- > { bar : Bool, foo : Integer } -- > --- > { bar = "ABC", baz = True, foo = 1 } +-- > { bar = True, foo = 1 } -- -- Note that the order of record fields does not matter. The compiler --- automatically sorts the fields when normalizing expressions. +-- automatically sorts the fields. -- --- The @(∧)@ operator also merges records recursively. For example: +-- The @(/\\)@ operator (or @(∧)@ U+2227) also lets you combine records, but +-- behaves differently if the records share fields in common. The operator +-- combines shared fields recursively if they are both records: -- -- > $ dhall --- > { foo = { bar = True }, baz = "ABC" } ∧ { foo = { qux = 1.0 } } +-- > { foo = { bar = True }, baz = "ABC" } /\ { foo = { qux = 1.0 } } -- > -- > { baz : Text, foo : { bar : Bool, qux : Double } } -- > -- > { baz = "ABC", foo = { bar = True, qux = 1.0 } } -- --- However, you cannot combine two records if they share a field that is not a --- record: +-- ... but fails with a type error if either shared field is not a record: -- -- > $ dhall -- > { foo = 1, bar = "ABC" } ∧ { foo = True } @@ -809,8 +812,8 @@ -- > -- > (stdin):1:1 -- --- __Exercise__: Combine any record with the empty record. What do you expect to --- happen? +-- __Exercise__: Combine any record with the empty record. What do you expect +-- to happen? -- $let -- @@ -901,7 +904,7 @@ -- You can also use @let@ expressions to rename imports, like this: -- -- > $ dhall --- > let not = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not +-- > let not = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not -- > in not True -- > -- > Bool @@ -1182,7 +1185,7 @@ -- complex example: -- -- > $ dhall --- > let List/map = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map +-- > let List/map = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/map -- > in λ(f : Integer → Integer) → List/map Integer Integer f [1, 2, 3] -- > -- > ∀(f : Integer → Integer) → List Integer @@ -1206,11 +1209,11 @@ -- __Exercise__: The Dhall Prelude provides a @replicate@ function which you can -- find here: -- --- +-- -- -- Test what the following Dhall expression normalizes to: -- --- > let replicate = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/replicate +-- > let replicate = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/replicate -- > in replicate +10 -- -- __Exercise__: If you have a lot of spare time, try to \"break the compiler\" by @@ -1760,7 +1763,7 @@ -- -- Rules: -- --- > let List/concat = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat +-- > let List/concat = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concat -- > -- > List/fold a (List/concat a xss) b c -- > = List/fold (List a) xss b (λ(x : List a) → List/fold a x b c) @@ -1829,10 +1832,10 @@ -- -- Rules: -- --- > let Optional/head = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Optional/head --- > let List/concat = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat --- > let List/concatMap = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concatMap --- > let List/map = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map +-- > let Optional/head = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Optional/head +-- > let List/concat = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concat +-- > let List/concatMap = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concatMap +-- > let List/map = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/map -- > -- > List/head a (List/concat a xss) = -- > Optional/head a (List/map (List a) (Optional a) (List/head a) xss) @@ -1860,10 +1863,10 @@ -- -- Rules: -- --- > let Optional/last = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Optional/last --- > let List/concat = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat --- > let List/concatMap = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concatMap --- > let List/map = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map +-- > let Optional/last = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Optional/last +-- > let List/concat = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concat +-- > let List/concatMap = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concatMap +-- > let List/map = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/map -- > -- > List/last a (List/concat a xss) = -- > Optional/last a (List/map (List a) (Optional a) (List/last a) xss) @@ -1891,9 +1894,9 @@ -- -- Rules: -- --- > let List/shifted = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/shifted --- > let List/concat = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat --- > let List/map = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map +-- > let List/shifted = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/shifted +-- > let List/concat = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concat +-- > let List/map = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/map -- > -- > List/indexed a (List/concat a xss) = -- > List/shifted a (List/map (List a) (List { index : Natural, value : a }) (List/indexed a) xss) @@ -1916,9 +1919,9 @@ -- -- Rules: -- --- > let List/map = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map --- > let List/concat = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat --- > let List/concatMap = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concatMap +-- > let List/map = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/map +-- > let List/concat = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concat +-- > let List/concatMap = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concatMap -- > -- > List/reverse a (List/concat a xss) -- > = List/concat a (List/reverse (List a) (List/map (List a) (List a) (List/reverse a) xss)) @@ -1972,7 +1975,7 @@ -- -- There is also a Prelude available at: -- --- +-- -- -- There is nothing \"official\" or \"standard\" about this Prelude other than -- the fact that it is mentioned in this tutorial. The \"Prelude\" is just a @@ -1983,12 +1986,12 @@ -- subdirectories. For example, the @Bool@ subdirectory has a @not@ file -- located here: -- --- +-- -- -- The @not@ function is just a UTF8-encoded text file hosted online with the -- following contents -- --- > $ curl https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not +-- > $ curl https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not -- > {- -- > Flip the value of a `Bool` -- > @@ -2021,7 +2024,7 @@ -- You can use this @not@ function either directly: -- -- > $ dhall --- > https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not True +-- > https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not True -- > -- > Bool -- > @@ -2030,7 +2033,7 @@ -- ... or assign the URL to a shorter name: -- -- > $ dhall --- > let Bool/not = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not +-- > let Bool/not = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not -- > in Bool/not True -- > -- > Bool @@ -2041,7 +2044,7 @@ -- consistency and documentation, such as @Prelude\/Natural\/even@, which -- re-exports the built-in @Natural/even@ function: -- --- > $ curl https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Natural/even +-- > $ curl https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Natural/even -- > {- -- > Returns `True` if a number if even and returns `False` otherwise -- > @@ -2062,7 +2065,7 @@ -- using local relative paths instead of URLs. For example, you can use @wget@, -- like this: -- --- > $ wget -np -nH -r --cut-dirs=2 https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/ +-- > $ wget -np -nH -r --cut-dirs=2 https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/ -- > $ tree Prelude -- > Prelude -- > ├── Bool @@ -2072,7 +2075,12 @@ -- > │   ├── fold -- > │   ├── not -- > │   ├── odd --- > │   └── or +-- > │   ├── or +-- > │   └── show +-- > ├── Double +-- > │   └── show +-- > ├── Integer +-- > │   └── show -- > ├── List -- > │   ├── all -- > │   ├── any @@ -2101,7 +2109,9 @@ -- > │   ├── isZero -- > │   ├── odd -- > │   ├── product --- > │   └── sum +-- > │   ├── show +-- > │   ├── sum +-- > │   └── toInteger -- > ├── Optional -- > │   ├── build -- > │   ├── concat @@ -2111,19 +2121,20 @@ -- > │   ├── map -- > │   ├── toList -- > │   └── unzip --- > └── Text --- > └── concat +-- > ├── Text +-- > │   └── concat +-- > └── index.html -- -- ... or if you have an @ipfs@ daemon running, you can mount the Prelude -- locally like this: -- -- > $ ipfs mount --- > $ cd /ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude +-- > $ cd /ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude -- -- Browse the Prelude online to learn more by seeing what functions are -- available and reading their inline documentation: -- --- +-- -- -- __Exercise__: Try to use a new Prelude function that has not been covered -- previously in this tutorial diff --git a/src/Dhall/TypeCheck.hs b/src/Dhall/TypeCheck.hs --- a/src/Dhall/TypeCheck.hs +++ b/src/Dhall/TypeCheck.hs @@ -308,6 +308,10 @@ return (Pi "_" Natural Bool) typeWith _ NaturalOdd = do return (Pi "_" Natural Bool) +typeWith _ NaturalToInteger = do + return (Pi "_" Natural Integer) +typeWith _ NaturalShow = do + return (Pi "_" Natural Text) typeWith ctx e@(NaturalPlus l r) = do tl <- fmap Dhall.Core.normalize (typeWith ctx l) case tl of @@ -334,10 +338,14 @@ return (Const Type) typeWith _ (IntegerLit _ ) = do return Integer +typeWith _ IntegerShow = do + return (Pi "_" Integer Text) typeWith _ Double = do return (Const Type) typeWith _ (DoubleLit _ ) = do return Double +typeWith _ DoubleShow = do + return (Pi "_" Double Text) typeWith _ Text = do return (Const Type) typeWith _ (TextLit _ ) = do @@ -444,6 +452,13 @@ (Pi "optional" (Const Type) (Pi "just" (Pi "_" "a" "optional") (Pi "nothing" "optional" "optional") ) ) ) ) +typeWith _ OptionalBuild = do + return + (Pi "a" (Const Type) + (Pi "_" f (App Optional "a") ) ) + where f = Pi "optional" (Const Type) + (Pi "just" (Pi "_" "a" "optional") + (Pi "nothing" "optional" "optional") ) typeWith ctx e@(Record kts ) = do let process (k, t) = do s <- fmap Dhall.Core.normalize (typeWith ctx t) @@ -482,12 +497,12 @@ tKvsX <- fmap Dhall.Core.normalize (typeWith ctx kvsX) ktsX <- case tKvsX of Record kts -> return kts - _ -> Left (TypeError ctx e (MustCombineARecord kvsX tKvsX)) + _ -> Left (TypeError ctx e (MustCombineARecord '∧' kvsX tKvsX)) tKvsY <- fmap Dhall.Core.normalize (typeWith ctx kvsY) ktsY <- case tKvsY of Record kts -> return kts - _ -> Left (TypeError ctx e (MustCombineARecord kvsY tKvsY)) + _ -> Left (TypeError ctx e (MustCombineARecord '∧' kvsY tKvsY)) let combineTypes ktsL ktsR = do let ks = @@ -506,6 +521,17 @@ return (Record (Data.Map.fromList kts)) combineTypes ktsX ktsY +typeWith ctx e@(Prefer kvsX kvsY) = do + tKvsX <- fmap Dhall.Core.normalize (typeWith ctx kvsX) + ktsX <- case tKvsX of + Record kts -> return kts + _ -> Left (TypeError ctx e (MustCombineARecord '⫽' kvsX tKvsX)) + + tKvsY <- fmap Dhall.Core.normalize (typeWith ctx kvsY) + ktsY <- case tKvsY of + Record kts -> return kts + _ -> Left (TypeError ctx e (MustCombineARecord '⫽' kvsY tKvsY)) + return (Record (Data.Map.union ktsY ktsX)) typeWith ctx e@(Merge kvsX kvsY t) = do tKvsX <- fmap Dhall.Core.normalize (typeWith ctx kvsX) ktsX <- case tKvsX of @@ -569,6 +595,9 @@ instance Show X where show = absurd +instance Eq X where + _ == _ = True + instance Buildable X where build = absurd @@ -596,7 +625,7 @@ | InvalidAlternative Text (Expr s X) | InvalidAlternativeType Text (Expr s X) | DuplicateAlternative Text - | MustCombineARecord (Expr s X) (Expr s X) + | MustCombineARecord Char (Expr s X) (Expr s X) | FieldCollision Text | MustMergeARecord (Expr s X) (Expr s X) | MustMergeUnion (Expr s X) (Expr s X) @@ -2086,22 +2115,22 @@ where txt0 = Text.toStrict (Dhall.Core.pretty k) -prettyTypeMessage (MustCombineARecord expr0 expr1) = ErrorMessages {..} +prettyTypeMessage (MustCombineARecord c expr0 expr1) = ErrorMessages {..} where short = "You can only combine records" long = Builder.fromText [NeatInterpolation.text| -Explanation: You can combine records using the ❰∧❱ operator, like this: +Explanation: You can combine records using the ❰$op❱ operator, like this: ┌───────────────────────────────────────────┐ - │ { foo = 1, bar = "ABC" } ∧ { baz = True } │ + │ { foo = 1, bar = "ABC" } $op { baz = True } │ └───────────────────────────────────────────┘ ┌─────────────────────────────────────────────┐ - │ λ(r : { foo : Bool }) → r ∧ { bar = "ABC" } │ + │ λ(r : { foo : Bool }) → r $op { bar = "ABC" } │ └─────────────────────────────────────────────┘ @@ -2111,21 +2140,21 @@ ┌──────────────────────────────┐ - │ { foo = 1, bar = "ABC" } ∧ 1 │ + │ { foo = 1, bar = "ABC" } $op 1 │ └──────────────────────────────┘ ⇧ Invalid: Not a record ┌───────────────────────────────────────────┐ - │ { foo = 1, bar = "ABC" } ∧ { baz : Bool } │ + │ { foo = 1, bar = "ABC" } $op { baz : Bool } │ └───────────────────────────────────────────┘ ⇧ Invalid: This is a record type and not a record ┌───────────────────────────────────────────┐ - │ { foo = 1, bar = "ABC" } ∧ < baz = True > │ + │ { foo = 1, bar = "ABC" } $op < baz = True > │ └───────────────────────────────────────────┘ ⇧ Invalid: This is a union and not a record @@ -2140,6 +2169,7 @@ ↳ $txt1 |] where + op = Data.Text.singleton c txt0 = Text.toStrict (Dhall.Core.pretty expr0) txt1 = Text.toStrict (Dhall.Core.pretty expr1) diff --git a/tests/Examples.hs b/tests/Examples.hs new file mode 100644 --- /dev/null +++ b/tests/Examples.hs @@ -0,0 +1,1136 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE QuasiQuotes #-} + +module Examples where + +import qualified NeatInterpolation +import qualified Test.Tasty +import qualified Test.Tasty.HUnit +import qualified Util + +import Test.Tasty (TestTree) + +exampleTests :: TestTree +exampleTests = + Test.Tasty.testGroup "examples" + [ Test.Tasty.testGroup "Bool" + [ Test.Tasty.testGroup "and" + [ _Bool_and_0 + , _Bool_and_1 + ] + , Test.Tasty.testGroup "build" + [ _Bool_build_0 + , _Bool_build_1 + ] + , Test.Tasty.testGroup "even" + [ _Bool_even_0 + , _Bool_even_1 + , _Bool_even_2 + , _Bool_even_3 + ] + , Test.Tasty.testGroup "fold" + [ _Bool_fold_0 + , _Bool_fold_1 + ] + , Test.Tasty.testGroup "not" + [ _Bool_not_0 + , _Bool_not_1 + ] + , Test.Tasty.testGroup "odd" + [ _Bool_odd_0 + , _Bool_odd_1 + , _Bool_odd_2 + , _Bool_odd_3 + ] + , Test.Tasty.testGroup "or" + [ _Bool_or_0 + , _Bool_or_1 + ] + , Test.Tasty.testGroup "show" + [ _Bool_show_0 + , _Bool_show_1 + ] + ] + , Test.Tasty.testGroup "Double" + [ Test.Tasty.testGroup "show" + [ _Double_show_0 + , _Double_show_1 + ] + ] + , Test.Tasty.testGroup "Integer" + [ Test.Tasty.testGroup "show" + [ _Integer_show_0 + , _Integer_show_1 + ] + ] + , Test.Tasty.testGroup "List" + [ Test.Tasty.testGroup "all" + [ _List_all_0 + , _List_all_1 + ] + , Test.Tasty.testGroup "any" + [ _List_any_0 + , _List_any_1 + ] + , Test.Tasty.testGroup "build" + [ _List_build_0 + , _List_build_1 + ] + , Test.Tasty.testGroup "concat" + [ _List_concat_0 + , _List_concat_1 + ] + , Test.Tasty.testGroup "filter" + [ _List_filter_0 + , _List_filter_1 + ] + , Test.Tasty.testGroup "fold" + [ _List_fold_0 + , _List_fold_1 + , _List_fold_2 + ] + , Test.Tasty.testGroup "generate" + [ _List_generate_0 + , _List_generate_1 + ] + , Test.Tasty.testGroup "head" + [ _List_head_0 + , _List_head_1 + ] + , Test.Tasty.testGroup "indexed" + [ _List_indexed_0 + , _List_indexed_1 + ] + , Test.Tasty.testGroup "iterate" + [ _List_iterate_0 + , _List_iterate_1 + ] + , Test.Tasty.testGroup "last" + [ _List_last_0 + , _List_last_1 + ] + , Test.Tasty.testGroup "length" + [ _List_length_0 + , _List_length_1 + ] + , Test.Tasty.testGroup "map" + [ _List_map_0 + , _List_map_1 + ] + , Test.Tasty.testGroup "null" + [ _List_null_0 + , _List_null_1 + ] + , Test.Tasty.testGroup "replicate" + [ _List_replicate_0 + , _List_replicate_1 + ] + , Test.Tasty.testGroup "reverse" + [ _List_reverse_0 + , _List_reverse_1 + ] + , Test.Tasty.testGroup "shifted" + [ _List_shifted_0 + , _List_shifted_1 + ] + , Test.Tasty.testGroup "unzip" + [ _List_unzip_0 + , _List_unzip_1 + ] + ] + , Test.Tasty.testGroup "Monoid" + [ _Monoid_00 + , _Monoid_01 + , _Monoid_02 + , _Monoid_03 + , _Monoid_04 + , _Monoid_05 + , _Monoid_06 + , _Monoid_07 + , _Monoid_08 + , _Monoid_09 + , _Monoid_10 + ] + , Test.Tasty.testGroup "Natural" + [ Test.Tasty.testGroup "build" + [ _Natural_build_0 + , _Natural_build_1 + ] + , Test.Tasty.testGroup "enumerate" + [ _Natural_enumerate_0 + , _Natural_enumerate_1 + ] + , Test.Tasty.testGroup "even" + [ _Natural_even_0 + , _Natural_even_1 + ] + , Test.Tasty.testGroup "fold" + [ _Natural_fold_0 + , _Natural_fold_1 + , _Natural_fold_2 + ] + , Test.Tasty.testGroup "isZero" + [ _Natural_isZero_0 + , _Natural_isZero_1 + ] + , Test.Tasty.testGroup "odd" + [ _Natural_odd_0 + , _Natural_odd_1 + ] + , Test.Tasty.testGroup "product" + [ _Natural_product_0 + , _Natural_product_1 + ] + , Test.Tasty.testGroup "show" + [ _Natural_show_0 + , _Natural_show_1 + ] + , Test.Tasty.testGroup "sum" + [ _Natural_sum_0 + , _Natural_sum_1 + ] + , Test.Tasty.testGroup "toInteger" + [ _Natural_toInteger_0 + , _Natural_toInteger_1 + ] + ] + , Test.Tasty.testGroup "Optional" + [ Test.Tasty.testGroup "build" + [ _Optional_build_0 + , _Optional_build_1 + ] + , Test.Tasty.testGroup "concat" + [ _Optional_concat_0 + , _Optional_concat_1 + , _Optional_concat_2 + ] + , Test.Tasty.testGroup "fold" + [ _Optional_fold_0 + , _Optional_fold_1 + ] + , Test.Tasty.testGroup "head" + [ _Optional_head_0 + , _Optional_head_1 + , _Optional_head_2 + ] + , Test.Tasty.testGroup "last" + [ _Optional_last_0 + , _Optional_last_1 + , _Optional_last_2 + ] + , Test.Tasty.testGroup "map" + [ _Optional_map_0 + , _Optional_map_1 + ] + , Test.Tasty.testGroup "toList" + [ _Optional_toList_0 + , _Optional_toList_1 + ] + , Test.Tasty.testGroup "unzip" + [ _Optional_unzip_0 + , _Optional_unzip_1 + ] + ] + , Test.Tasty.testGroup "Text" + [ Test.Tasty.testGroup "concat" + [ _Text_concat_0 + , _Text_concat_1 + ] + ] + ] + +_Bool_and_0 :: TestTree +_Bool_and_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Bool/and ([True, False, True] : List Bool) +|] + Util.assertNormalizesTo e "False" ) + +_Bool_and_1 :: TestTree +_Bool_and_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Bool/and ([] : List Bool) +|] + Util.assertNormalizesTo e "True" ) + +_Bool_build_0 :: TestTree +_Bool_build_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Bool/build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → true) +|] + Util.assertNormalizesTo e "True" ) + +_Bool_build_1 :: TestTree +_Bool_build_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Bool/build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → false) +|] + Util.assertNormalizesTo e "False" ) + +_Bool_even_0 :: TestTree +_Bool_even_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Bool/even ([False, True, False] : List Bool) +|] + Util.assertNormalizesTo e "True" ) + +_Bool_even_1 :: TestTree +_Bool_even_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Bool/even ([False, True] : List Bool) +|] + Util.assertNormalizesTo e "False" ) + +_Bool_even_2 :: TestTree +_Bool_even_2 = Test.Tasty.HUnit.testCase "Example #2" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Bool/even ([False] : List Bool) +|] + Util.assertNormalizesTo e "False" ) + +_Bool_even_3 :: TestTree +_Bool_even_3 = Test.Tasty.HUnit.testCase "Example #3" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Bool/even ([] : List Bool) +|] + Util.assertNormalizesTo e "True" ) + +_Bool_fold_0 :: TestTree +_Bool_fold_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Bool/fold True Integer 0 1 +|] + Util.assertNormalizesTo e "0" ) + +_Bool_fold_1 :: TestTree +_Bool_fold_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Bool/fold False Integer 0 1 +|] + Util.assertNormalizesTo e "1" ) + +_Bool_not_0 :: TestTree +_Bool_not_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Bool/not True +|] + Util.assertNormalizesTo e "False" ) + +_Bool_not_1 :: TestTree +_Bool_not_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Bool/not False +|] + Util.assertNormalizesTo e "True" ) + +_Bool_odd_0 :: TestTree +_Bool_odd_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Bool/odd ([True, False, True] : List Bool) +|] + Util.assertNormalizesTo e "False" ) + +_Bool_odd_1 :: TestTree +_Bool_odd_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Bool/odd ([True, False] : List Bool) +|] + Util.assertNormalizesTo e "True" ) + +_Bool_odd_2 :: TestTree +_Bool_odd_2 = Test.Tasty.HUnit.testCase "Example #2" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Bool/odd ([True] : List Bool) +|] + Util.assertNormalizesTo e "True" ) + +_Bool_odd_3 :: TestTree +_Bool_odd_3 = Test.Tasty.HUnit.testCase "Example #3" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Bool/odd ([] : List Bool) +|] + Util.assertNormalizesTo e "False" ) + +_Bool_or_0 :: TestTree +_Bool_or_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Bool/or ([True, False, True] : List Bool) +|] + Util.assertNormalizesTo e "True" ) + +_Bool_or_1 :: TestTree +_Bool_or_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Bool/or ([] : List Bool) +|] + Util.assertNormalizesTo e "False" ) + +_Bool_show_0 :: TestTree +_Bool_show_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Bool/show True +|] + Util.assertNormalizesTo e "\"True\"" ) + +_Bool_show_1 :: TestTree +_Bool_show_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Bool/show False +|] + Util.assertNormalizesTo e "\"False\"" ) + +_Double_show_0 :: TestTree +_Double_show_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Double/show -3.1 +|] + Util.assertNormalizesTo e "\"-3.1\"" ) + +_Double_show_1 :: TestTree +_Double_show_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Double/show 0.4 +|] + Util.assertNormalizesTo e "\"0.4\"" ) + +_Integer_show_0 :: TestTree +_Integer_show_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Integer/show -3 +|] + Util.assertNormalizesTo e "\"-3\"" ) + +_Integer_show_1 :: TestTree +_Integer_show_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Integer/show 0 +|] + Util.assertNormalizesTo e "\"0\"" ) + +_List_all_0 :: TestTree +_List_all_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/all Natural Natural/even ([+2, +3, +5] : List Natural) +|] + Util.assertNormalizesTo e "False" ) + +_List_all_1 :: TestTree +_List_all_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/all Natural Natural/even ([] : List Natural) +|] + Util.assertNormalizesTo e "True" ) + +_List_any_0 :: TestTree +_List_any_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/any Natural Natural/even ([+2, +3, +5] : List Natural) +|] + Util.assertNormalizesTo e "True" ) + +_List_any_1 :: TestTree +_List_any_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/any Natural Natural/even ([] : List Natural) +|] + Util.assertNormalizesTo e "False" ) + +_List_build_0 :: TestTree +_List_build_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/build +Text +( λ(list : Type) +→ λ(cons : Text → list → list) +→ λ(nil : list) +→ cons "ABC" (cons "DEF" nil) +) +|] + Util.assertNormalizesTo e "[\"ABC\", \"DEF\"] : List Text" ) + +_List_build_1 :: TestTree +_List_build_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/build +Text +( λ(list : Type) +→ λ(cons : Text → list → list) +→ λ(nil : list) +→ nil +) +|] + Util.assertNormalizesTo e "[] : List Text" ) + +_List_concat_0 :: TestTree +_List_concat_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/concat Integer +( [ [0, 1, 2] : List Integer + , [3, 4] : List Integer + , [5, 6, 7, 8] : List Integer + ] : List (List Integer) +) +|] + Util.assertNormalizesTo e "[0, 1, 2, 3, 4, 5, 6, 7, 8] : List Integer" ) + +_List_concat_1 :: TestTree +_List_concat_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/concat Integer +( [ [] : List Integer + , [] : List Integer + , [] : List Integer + ] : List (List Integer) +) +|] + Util.assertNormalizesTo e "[] : List Integer" ) + +_List_filter_0 :: TestTree +_List_filter_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/filter Natural Natural/even ([+2, +3, +5] : List Natural) +|] + Util.assertNormalizesTo e "[+2] : List Natural" ) + +_List_filter_1 :: TestTree +_List_filter_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/filter Natural Natural/odd ([+2, +3, +5] : List Natural) +|] + Util.assertNormalizesTo e "[+3, +5] : List Natural" ) + +_List_fold_0 :: TestTree +_List_fold_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| + ./Prelude/List/fold + Natural + ([+2, +3, +5] : List Natural) + Natural + (λ(x : Natural) → λ(y : Natural) → x + y) + +0 +|] + Util.assertNormalizesTo e "+10" ) + +_List_fold_1 :: TestTree +_List_fold_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| + λ(nil : Natural) +→ ./Prelude/List/fold + Natural + ([+2, +3, +5] : List Natural) + Natural + (λ(x : Natural) → λ(y : Natural) → x + y) + nil +|] + Util.assertNormalizesTo e "λ(nil : Natural) → +2 + +3 + +5 + nil" ) + +_List_fold_2 :: TestTree +_List_fold_2 = Test.Tasty.HUnit.testCase "Example #2" (do + e <- Util.code [NeatInterpolation.text| + λ(list : Type) +→ λ(cons : Natural → list → list) +→ λ(nil : list) +→ ./Prelude/List/fold Natural ([+2, +3, +5] : List Natural) list cons nil +|] + Util.assertNormalizesTo e "λ(list : Type) → λ(cons : Natural → list → list) → λ(nil : list) → cons +2 (cons +3 (cons +5 nil))" ) + +_List_generate_0 :: TestTree +_List_generate_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/generate +5 Bool Natural/even +|] + Util.assertNormalizesTo e "[True, False, True, False, True] : List Bool" ) + +_List_generate_1 :: TestTree +_List_generate_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/generate +0 Bool Natural/even +|] + Util.assertNormalizesTo e "[] : List Bool" ) + +_List_head_0 :: TestTree +_List_head_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/head Integer ([0, 1, 2] : List Integer) +|] + Util.assertNormalizesTo e "[0] : Optional Integer" ) + +_List_head_1 :: TestTree +_List_head_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/head Integer ([] : List Integer) +|] + Util.assertNormalizesTo e "[] : Optional Integer" ) + +_List_indexed_0 :: TestTree +_List_indexed_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/indexed Bool ([True, False, True] : List Bool) +|] + Util.assertNormalizesTo e "[{ index = +0, value = True }, { index = +1, value = False }, { index = +2, value = True }] : List { index : Natural, value : Bool }" ) + +_List_indexed_1 :: TestTree +_List_indexed_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/indexed Bool ([] : List Bool) +|] + Util.assertNormalizesTo e "[] : List { index : Natural, value : Bool }" ) + +_List_iterate_0 :: TestTree +_List_iterate_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/iterate +10 Natural (λ(x : Natural) → x * +2) +1 +|] + Util.assertNormalizesTo e "[+1, +2, +4, +8, +16, +32, +64, +128, +256, +512] : List Natural" ) + +_List_iterate_1 :: TestTree +_List_iterate_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/iterate +0 Natural (λ(x : Natural) → x * +2) +1 +|] + Util.assertNormalizesTo e "[] : List Natural" ) + +_List_last_0 :: TestTree +_List_last_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/last Integer ([0, 1, 2] : List Integer) +|] + Util.assertNormalizesTo e "[2] : Optional Integer" ) + +_List_last_1 :: TestTree +_List_last_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/last Integer ([] : List Integer) +|] + Util.assertNormalizesTo e "[] : Optional Integer" ) + +_List_length_0 :: TestTree +_List_length_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/length Integer ([0, 1, 2] : List Integer) +|] + Util.assertNormalizesTo e "+3" ) + +_List_length_1 :: TestTree +_List_length_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/length Integer ([] : List Integer) +|] + Util.assertNormalizesTo e "+0" ) + +_List_map_0 :: TestTree +_List_map_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/map Natural Bool Natural/even ([+2, +3, +5] : List Natural) +|] + Util.assertNormalizesTo e "[True, False, False] : List Bool" ) + +_List_map_1 :: TestTree +_List_map_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/map Natural Bool Natural/even ([] : List Natural) +|] + Util.assertNormalizesTo e "[] : List Bool" ) + +_List_null_0 :: TestTree +_List_null_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/null Integer ([0, 1, 2] : List Integer) +|] + Util.assertNormalizesTo e "False" ) + +_List_null_1 :: TestTree +_List_null_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/null Integer ([] : List Integer) +|] + Util.assertNormalizesTo e "True" ) + +_List_replicate_0 :: TestTree +_List_replicate_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/replicate +9 Integer 1 +|] + Util.assertNormalizesTo e "[1, 1, 1, 1, 1, 1, 1, 1, 1] : List Integer" ) + +_List_replicate_1 :: TestTree +_List_replicate_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/replicate +0 Integer 1 +|] + Util.assertNormalizesTo e "[] : List Integer" ) + +_List_reverse_0 :: TestTree +_List_reverse_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/reverse Integer ([0, 1, 2] : List Integer) +|] + Util.assertNormalizesTo e "[2, 1, 0] : List Integer" ) + +_List_reverse_1 :: TestTree +_List_reverse_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/reverse Integer ([] : List Integer) +|] + Util.assertNormalizesTo e "[] : List Integer" ) + +_List_shifted_0 :: TestTree +_List_shifted_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/shifted +Bool +( [ [ { index = +0, value = True } + , { index = +1, value = True } + , { index = +2, value = True } + ] : List { index : Natural, value : Bool } + , [ { index = +0, value = False } + , { index = +1, value = False } + ] : List { index : Natural, value : Bool } + , [ { index = +0, value = True } + , { index = +1, value = True } + , { index = +2, value = True } + , { index = +3, value = True } + ] : List { index : Natural, value : Bool } + ] : List (List { index : Natural, value : Bool }) +) +|] + Util.assertNormalizesTo e "[{ index = +0, value = True }, { index = +1, value = True }, { index = +2, value = True }, { index = +3, value = False }, { index = +4, value = False }, { index = +5, value = True }, { index = +6, value = True }, { index = +7, value = True }, { index = +8, value = True }] : List { index : Natural, value : Bool }" ) + +_List_shifted_1 :: TestTree +_List_shifted_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/shifted Bool ([] : List (List { index : Natural, value : Bool })) +|] + Util.assertNormalizesTo e "[] : List { index : Natural, value : Bool }" ) + +_List_unzip_0 :: TestTree +_List_unzip_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/unzip +Text +Bool +( [ { _1 = "ABC", _2 = True } + , { _1 = "DEF", _2 = False } + , { _1 = "GHI", _2 = True } + ] : List { _1 : Text, _2 : Bool } +) +|] + Util.assertNormalizesTo e "{ _1 = [\"ABC\", \"DEF\", \"GHI\"] : List Text, _2 = [True, False, True] : List Bool }" ) + +_List_unzip_1 :: TestTree +_List_unzip_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/List/unzip Text Bool ([] : List { _1 : Text, _2 : Bool }) +|] + Util.assertNormalizesTo e "{ _1 = [] : List Text, _2 = [] : List Bool }" ) + +_Monoid_00 :: TestTree +_Monoid_00 = Test.Tasty.HUnit.testCase "Example #0" + (Util.assertTypeChecks [NeatInterpolation.text| +./Prelude/Bool/and + : ./Prelude/Monoid Bool +|] ) + +_Monoid_01 :: TestTree +_Monoid_01 = Test.Tasty.HUnit.testCase "Example #1" + (Util.assertTypeChecks [NeatInterpolation.text| +./Prelude/Bool/or + : ./Prelude/Monoid Bool +|] ) + +_Monoid_02 :: TestTree +_Monoid_02 = Test.Tasty.HUnit.testCase "Example #2" + (Util.assertTypeChecks [NeatInterpolation.text| +./Prelude/Bool/even + : ./Prelude/Monoid Bool +|] ) + +_Monoid_03 :: TestTree +_Monoid_03 = Test.Tasty.HUnit.testCase "Example #3" + (Util.assertTypeChecks[NeatInterpolation.text| +./Prelude/Bool/odd + : ./Prelude/Monoid Bool +|] ) + +_Monoid_04 :: TestTree +_Monoid_04 = Test.Tasty.HUnit.testCase "Example #4" + (Util.assertTypeChecks [NeatInterpolation.text| +./Prelude/List/concat + : ∀(a : Type) → ./Prelude/Monoid (List a) +|] ) + +_Monoid_05 :: TestTree +_Monoid_05 = Test.Tasty.HUnit.testCase "Example #5" + (Util.assertTypeChecks [NeatInterpolation.text| +./Prelude/List/shifted + : ∀(a : Type) → ./Prelude/Monoid (List { index : Natural, value : a }) +|] ) + +_Monoid_06 :: TestTree +_Monoid_06 = Test.Tasty.HUnit.testCase "Example #6" + (Util.assertTypeChecks [NeatInterpolation.text| +./Prelude/Natural/sum + : ./Prelude/Monoid Natural +|] ) + +_Monoid_07 :: TestTree +_Monoid_07 = Test.Tasty.HUnit.testCase "Example #7" + (Util.assertTypeChecks [NeatInterpolation.text| +./Prelude/Natural/product + : ./Prelude/Monoid Natural +|] ) + +_Monoid_08 :: TestTree +_Monoid_08 = Test.Tasty.HUnit.testCase "Example #8" + (Util.assertTypeChecks [NeatInterpolation.text| +./Prelude/Optional/head + : ∀(a : Type) → ./Prelude/Monoid (Optional a) +|] ) + +_Monoid_09 :: TestTree +_Monoid_09 = Test.Tasty.HUnit.testCase "Example #9" + (Util.assertTypeChecks [NeatInterpolation.text| +./Prelude/Optional/last + : ∀(a : Type) → ./Prelude/Monoid (Optional a) +|] ) + +_Monoid_10 :: TestTree +_Monoid_10 = Test.Tasty.HUnit.testCase "Example #10" + (Util.assertTypeChecks [NeatInterpolation.text| +./Prelude/Text/concat + : ./Prelude/Monoid Text +|] ) + +_Natural_build_0 :: TestTree +_Natural_build_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Natural/build +( λ(natural : Type) +→ λ(succ : natural → natural) +→ λ(zero : natural) +→ succ (succ (succ zero)) +) +|] + Util.assertNormalizesTo e "+3" ) + +_Natural_build_1 :: TestTree +_Natural_build_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Natural/build +( λ(natural : Type) +→ λ(succ : natural → natural) +→ λ(zero : natural) +→ zero +) +|] + Util.assertNormalizesTo e "+0" ) + +_Natural_enumerate_0 :: TestTree +_Natural_enumerate_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Natural/enumerate +10 +|] + Util.assertNormalizesTo e "[+0, +1, +2, +3, +4, +5, +6, +7, +8, +9] : List Natural" ) + +_Natural_enumerate_1 :: TestTree +_Natural_enumerate_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Natural/enumerate +0 +|] + Util.assertNormalizesTo e "[] : List Natural" ) + +_Natural_even_0 :: TestTree +_Natural_even_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Natural/even +3 +|] + Util.assertNormalizesTo e "False" ) + +_Natural_even_1 :: TestTree +_Natural_even_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Natural/even +0 +|] + Util.assertNormalizesTo e "True" ) + +_Natural_fold_0 :: TestTree +_Natural_fold_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Natural/fold +3 Natural (λ(x : Natural) → +5 * x) +1 +|] + Util.assertNormalizesTo e "+125" ) + +_Natural_fold_1 :: TestTree +_Natural_fold_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +λ(zero : Natural) → ./Prelude/Natural/fold +3 Natural (λ(x : Natural) → +5 * x) zero +|] + Util.assertNormalizesTo e "λ(zero : Natural) → +5 * +5 * +5 * zero" ) + +_Natural_fold_2 :: TestTree +_Natural_fold_2 = Test.Tasty.HUnit.testCase "Example #2" (do + e <- Util.code [NeatInterpolation.text| + λ(natural : Type) +→ λ(succ : natural → natural) +→ λ(zero : natural) +→ ./Prelude/Natural/fold +3 natural succ zero +|] + Util.assertNormalizesTo e "λ(natural : Type) → λ(succ : natural → natural) → λ(zero : natural) → succ (succ (succ zero))" ) + +_Natural_isZero_0 :: TestTree +_Natural_isZero_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Natural/isZero +2 +|] + Util.assertNormalizesTo e "False" ) + +_Natural_isZero_1 :: TestTree +_Natural_isZero_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Natural/isZero +0 +|] + Util.assertNormalizesTo e "True" ) + +_Natural_odd_0 :: TestTree +_Natural_odd_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Natural/odd +3 +|] + Util.assertNormalizesTo e "True" ) + +_Natural_odd_1 :: TestTree +_Natural_odd_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Natural/odd +0 +|] + Util.assertNormalizesTo e "False" ) + +_Natural_product_0 :: TestTree +_Natural_product_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Natural/product ([+2, +3, +5] : List Natural) +|] + Util.assertNormalizesTo e "+30" ) + +_Natural_product_1 :: TestTree +_Natural_product_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Natural/product ([] : List Natural) +|] + Util.assertNormalizesTo e "+1" ) + +_Natural_show_0 :: TestTree +_Natural_show_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Natural/show +3 +|] + Util.assertNormalizesTo e "\"+3\"" ) + +_Natural_show_1 :: TestTree +_Natural_show_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Natural/show +0 +|] + Util.assertNormalizesTo e "\"+0\"" ) + +_Natural_sum_0 :: TestTree +_Natural_sum_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Natural/sum ([+2, +3, +5] : List Natural) +|] + Util.assertNormalizesTo e "+10" ) + +_Natural_sum_1 :: TestTree +_Natural_sum_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Natural/sum ([] : List Natural) +|] + Util.assertNormalizesTo e "+0" ) + +_Natural_toInteger_0 :: TestTree +_Natural_toInteger_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Natural/toInteger +3 +|] + Util.assertNormalizesTo e "3" ) + +_Natural_toInteger_1 :: TestTree +_Natural_toInteger_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Natural/toInteger +0 +|] + Util.assertNormalizesTo e "0" ) + +_Optional_build_0 :: TestTree +_Optional_build_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/build +Integer +( λ(optional : Type) +→ λ(just : Integer → optional) +→ λ(nothing : optional) +→ just 1 +) +|] + Util.assertNormalizesTo e "[1] : Optional Integer" ) + +_Optional_build_1 :: TestTree +_Optional_build_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/build +Integer +( λ(optional : Type) +→ λ(just : Integer → optional) +→ λ(nothing : optional) +→ nothing +) +|] + Util.assertNormalizesTo e "[] : Optional Integer" ) + +_Optional_concat_0 :: TestTree +_Optional_concat_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/concat Integer ([[1] : Optional Integer] : Optional (Optional Integer)) +|] + Util.assertNormalizesTo e "[1] : Optional Integer" ) + +_Optional_concat_1 :: TestTree +_Optional_concat_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/concat Integer ([[] : Optional Integer] : Optional (Optional Integer)) +|] + Util.assertNormalizesTo e "[] : Optional Integer" ) + +_Optional_concat_2 :: TestTree +_Optional_concat_2 = Test.Tasty.HUnit.testCase "Example #2" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/concat Integer ([] : Optional (Optional Integer)) +|] + Util.assertNormalizesTo e "[] : Optional Integer" ) + +_Optional_fold_0 :: TestTree +_Optional_fold_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/fold Integer ([2] : Optional Integer) Integer (λ(x : Integer) → x) 0 +|] + Util.assertNormalizesTo e "2" ) + +_Optional_fold_1 :: TestTree +_Optional_fold_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/fold Integer ([] : Optional Integer) Integer (λ(x : Integer) → x) 0 +|] + Util.assertNormalizesTo e "0" ) + +_Optional_head_0 :: TestTree +_Optional_head_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/head +Integer +( [[] : Optional Integer, [1] : Optional Integer, [2] : Optional Integer] + : List (Optional Integer) +) +|] + Util.assertNormalizesTo e "[1] : Optional Integer" ) + +_Optional_head_1 :: TestTree +_Optional_head_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/head +Integer +([[] : Optional Integer, [] : Optional Integer] : List (Optional Integer)) +|] + Util.assertNormalizesTo e "[] : Optional Integer" ) + +_Optional_head_2 :: TestTree +_Optional_head_2 = Test.Tasty.HUnit.testCase "Example #2" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/head Integer ([] : List (Optional Integer)) +|] + Util.assertNormalizesTo e "[] : Optional Integer" ) + +_Optional_last_0 :: TestTree +_Optional_last_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/last +Integer +( [[] : Optional Integer, [1] : Optional Integer, [2] : Optional Integer] + : List (Optional Integer) +) +|] + Util.assertNormalizesTo e "[2] : Optional Integer" ) + +_Optional_last_1 :: TestTree +_Optional_last_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/last +Integer +([[] : Optional Integer, [] : Optional Integer] : List (Optional Integer)) +|] + Util.assertNormalizesTo e "[] : Optional Integer" ) + +_Optional_last_2 :: TestTree +_Optional_last_2 = Test.Tasty.HUnit.testCase "Example #2" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/last Integer ([] : List (Optional Integer)) +|] + Util.assertNormalizesTo e "[] : Optional Integer" ) + +_Optional_map_0 :: TestTree +_Optional_map_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/map Natural Bool Natural/even ([+3] : Optional Natural) +|] + Util.assertNormalizesTo e "[False] : Optional Bool" ) + +_Optional_map_1 :: TestTree +_Optional_map_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/map Natural Bool Natural/even ([] : Optional Natural) +|] + Util.assertNormalizesTo e "[] : Optional Bool" ) + +_Optional_toList_0 :: TestTree +_Optional_toList_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/toList Integer ([1] : Optional Integer) +|] + Util.assertNormalizesTo e "[1] : List Integer" ) + +_Optional_toList_1 :: TestTree +_Optional_toList_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/toList Integer ([] : Optional Integer) +|] + Util.assertNormalizesTo e "[] : List Integer" ) + +_Optional_unzip_0 :: TestTree +_Optional_unzip_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/unzip +Text +Bool +([{ _1 = "ABC", _2 = True }] : Optional { _1 : Text, _2 : Bool }) +|] + Util.assertNormalizesTo e "{ _1 = [\"ABC\"] : Optional Text, _2 = [True] : Optional Bool }" ) + +_Optional_unzip_1 :: TestTree +_Optional_unzip_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/unzip Text Bool ([] : Optional { _1 : Text, _2 : Bool }) +|] + Util.assertNormalizesTo e "{ _1 = [] : Optional Text, _2 = [] : Optional Bool }" ) + +_Text_concat_0 :: TestTree +_Text_concat_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Text/concat (["ABC", "DEF", "GHI"] : List Text) +|] + Util.assertNormalizesTo e "\"ABCDEFGHI\"" ) + +_Text_concat_1 :: TestTree +_Text_concat_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Text/concat ([] : List Text) +|] + Util.assertNormalizesTo e "\"\"" ) diff --git a/tests/Normalization.hs b/tests/Normalization.hs new file mode 100644 --- /dev/null +++ b/tests/Normalization.hs @@ -0,0 +1,156 @@ +{-# LANGUAGE OverloadedLists #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE QuasiQuotes #-} + +module Normalization (normalizationTests) where + +import Dhall.Core +import qualified NeatInterpolation +import Test.Tasty +import Test.Tasty.HUnit +import Util (code, normalize', assertNormalizesTo, assertNormalized) + +normalizationTests :: TestTree +normalizationTests = testGroup "normalization" [ constantFolding + , conversions + , fusion + ] + +constantFolding :: TestTree +constantFolding = testGroup "folding of constants" [ naturalPlus + , optionalFold + , optionalBuild + ] + +conversions :: TestTree +conversions = testGroup "conversions" [ naturalShow + , integerShow + , doubleShow + , naturalToInteger + ] + +naturalPlus :: TestTree +naturalPlus = testCase "natural plus" $ do + e <- code "+1 + +2" + e `assertNormalizesTo` "+3" + +naturalToInteger :: TestTree +naturalToInteger = testCase "Natural/toInteger" $ do + e <- code "Natural/toInteger +1" + isNormalized e @?= False + normalize' e @?= "1" + +naturalShow :: TestTree +naturalShow = testCase "Natural/show" $ do + e <- code "Natural/show +42" + e `assertNormalizesTo` "\"+42\"" + +integerShow :: TestTree +integerShow = testCase "Integer/show" $ do + e <- code "[Integer/show 1337, Integer/show -42, Integer/show 0]" + e `assertNormalizesTo` "[\"1337\", \"-42\", \"0\"]" + +doubleShow :: TestTree +doubleShow = testCase "Double/show" $ do + e <- code "[Double/show -0.42, Double/show 13.37]" + e `assertNormalizesTo` "[\"-0.42\", \"13.37\"]" + +optionalFold :: TestTree +optionalFold = testGroup "Optional/fold" [ just, nothing ] + where test label inp out = testCase label $ do + e <- code [NeatInterpolation.text| + Optional/fold Text ([$inp] : Optional Text) Natural (λ(j : Text) → +1) +2 + |] + e `assertNormalizesTo` out + just = test "just" "\"foo\"" "+1" + nothing = test "nothing" "" "+2" + +optionalBuild :: TestTree +optionalBuild = testGroup "Optional/build" [ optionalBuild1 + , optionalBuildShadowing + , optionalBuildIrreducible + ] + +optionalBuild1 :: TestTree +optionalBuild1 = testCase "reducible" $ do + e <- code [NeatInterpolation.text| +Optional/build +Natural +( λ(optional : Type) +→ λ(just : Natural → optional) +→ λ(nothing : optional) +→ just +1 +) +|] + e `assertNormalizesTo` "[+1] : Optional Natural" + +optionalBuildShadowing :: TestTree +optionalBuildShadowing = testCase "handles shadowing" $ do + e <- code [NeatInterpolation.text| +Optional/build +Integer +( λ(optional : Type) +→ λ(x : Integer → optional) +→ λ(x : optional) +→ x@1 1 +) +|] + e `assertNormalizesTo` "[1] : Optional Integer" + +optionalBuildIrreducible :: TestTree +optionalBuildIrreducible = testCase "irreducible" $ do + e <- code [NeatInterpolation.text| + λ(id : ∀(a : Type) → a → a) +→ Optional/build + Bool + ( λ(optional : Type) + → λ(just : Bool → optional) + → λ(nothing : optional) + → id optional (just True) + ) +|] + assertNormalized e + +fusion :: TestTree +fusion = testGroup "Optional build/fold fusion" [ fuseOptionalBF + , fuseOptionalFB + ] + +fuseOptionalBF :: TestTree +fuseOptionalBF = testCase "fold . build" $ do + e0 <- code [NeatInterpolation.text| + λ( f + : ∀(optional : Type) + → ∀(just : Text → optional) + → ∀(nothing : optional) + → optional + ) +→ Optional/fold + Text + ( Optional/build + Text + f + ) +|] + e1 <- code [NeatInterpolation.text| + λ( f + : ∀(optional : Type) + → ∀(just : Text → optional) + → ∀(nothing : optional) + → optional + ) +→ f +|] + e0 `assertNormalizesTo` (Dhall.Core.pretty e1) + +fuseOptionalFB :: TestTree +fuseOptionalFB = testCase "build . fold" $ do + test <- code [NeatInterpolation.text| +Optional/build +Text +( Optional/fold + Text + (["foo"] : Optional Text) +) +|] + test `assertNormalizesTo` "[\"foo\"] : Optional Text" diff --git a/tests/Tests.hs b/tests/Tests.hs new file mode 100644 --- /dev/null +++ b/tests/Tests.hs @@ -0,0 +1,15 @@ +module Main where + +import Normalization (normalizationTests) +import Examples (exampleTests) +import Test.Tasty + +allTests :: TestTree +allTests = + testGroup "Dhall Tests" + [ normalizationTests + , exampleTests + ] + +main :: IO () +main = defaultMain allTests diff --git a/tests/Util.hs b/tests/Util.hs new file mode 100644 --- /dev/null +++ b/tests/Util.hs @@ -0,0 +1,53 @@ +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE OverloadedStrings #-} +module Util + ( code + , normalize' + , assertNormalizesTo + , assertNormalized + , assertTypeChecks + ) where + +import qualified Control.Exception +import qualified Data.Functor +import Data.Text (Text) +import qualified Data.Text.Lazy +import qualified Dhall.Core +import Dhall.Core (Expr) +import qualified Dhall.Import +import qualified Dhall.Parser +import Dhall.Parser (Src) +import qualified Dhall.TypeCheck +import Dhall.TypeCheck (X) +import Test.Tasty.HUnit + +normalize' :: Expr Src X -> Data.Text.Lazy.Text +normalize' = Dhall.Core.pretty . Dhall.Core.normalize + +code :: Data.Text.Text -> IO (Expr Src X) +code strictText = do + let lazyText = Data.Text.Lazy.fromStrict strictText + expr0 <- case Dhall.Parser.exprFromText mempty lazyText of + Left parseError -> Control.Exception.throwIO parseError + Right expr0 -> return expr0 + expr1 <- Dhall.Import.load expr0 + case Dhall.TypeCheck.typeOf expr1 of + Left typeError -> Control.Exception.throwIO typeError + Right _ -> return () + return expr1 + +assertNormalizesTo :: Expr Src X -> Data.Text.Lazy.Text -> IO () +assertNormalizesTo e expected = do + assertBool msg (not $ Dhall.Core.isNormalized e) + normalize' e @?= expected + where msg = "Given expression is already in normal form" + +assertNormalized :: Expr Src X -> IO () +assertNormalized e = do + assertBool msg1 (Dhall.Core.isNormalized e) + assertEqual msg2 (normalize' e) (Dhall.Core.pretty e) + where msg1 = "Expression was not in normal form" + msg2 = "Normalization is not supposed to change the expression" + +assertTypeChecks :: Text -> IO () +assertTypeChecks text = Data.Functor.void (code text)