ehmry/dhall-haskell
ehmry/dhall-haskell
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Fix semantics of {List,Optional,Natural}/build (#300)

Browse Source 
This fixes all of the build built-ins  to match the standard semantics

The easiest way to illustrate the problem is the following example from
the test suite:

```haskell
  λ(id : ∀(a : Type) → a → a)
→ Natural/build
  (   λ(natural : Type)
    → λ(succ : natural → natural)
    → λ(zero : natural)
    → id natural (succ zero)
  )
```

According to the standard semantics that should normalize to:

```haskell
λ(id : ∀(a : Type) → a → a) → id Natural +1
```

... but before this change it was not reducing at all.  After this
change it reduces correctly.

However, there is a further issue, which is that correctly implementing
the semantics leads to poor time complexity for `List/build` since it is
specified in terms of repeatedly prepending a single element, which
leads to quadratic time complexity since lists are implemented in terms
of `Vector` under the hood.

You might think that you could use the efficient approach for
expressions like this:

```haskell
List/build
Bool
( λ(list : Type)
→ λ(cons : Bool → list → list)
→ λ(nil : list)
→ cons True (cons False nil)
)
```

... and then fall back on the slower approach for more interesting cases
such as this:

```haskell
  λ(id : ∀(a : Type) → a → a)
→ List/build
  Bool
  ( λ(list : Type)
  → λ(cons : Bool → list → list)
  → λ(nil : list)
  → id list (cons True (cons False nil))
  )
```

... but that does not work either!  The reason why is that very often
you don't use `List/build` directly and instead use it indirectly via
helper functions such as `Prelude/List/concat`:

```haskell
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
```

... so what happens is that if you try to normalize something like:

```haskell
concat Text [["Example"]]
```

... the `concat` function will be normalized first, which will cause the
`List/build` to be normalized when its argument is still abstract, which will
trigger the slow path for the semantics.

Consequently, this change also modifies Dhall lists to be backed by
`Data.Sequence.Seq` instead of `Data.Vector.Vector`, so that
`List/build` can always use the correct implementation of semantics
in linear time while still implementing other operations on lists
reasonably efficiently.

This in turn triggers another change to the `OptionalLit` constructor
to use `Maybe` to store the payload instead of `Vector`.  The only
reason that `OptionalLit` originally used `Vector` was so that
`List/head` and `List/last` could be implemented as just a slice into
the `ListLit` vector, but now that it's not a vector any longer it's
simpler to just use a more accurate `Maybe` type to represent the
payload.
This commit is contained in:
Gabriel Gonzalez 2018-02-26 10:50:27 -08:00 committed by GitHub
parent 4b3f28374c
commit 6b56aa5a0f
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
44 changed files with 351 additions and 447 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Prelude/Bool/and
View File

@ -5,7 +5,7 @@ The `and` function returns `False` if there are any `False` elements in the
Examples:
```
./and ([ True, False, True ] : List Bool) = False
./and [ True, False, True ] = False
./and ([] : List Bool) = True
```

6
Prelude/Bool/even
View File

@ -5,11 +5,11 @@ returns `False` otherwise
Examples:
```
./even ([ False, True, False ] : List Bool) = True
./even [ False, True, False ] = True
./even ([ False, True ] : List Bool) = False
./even [ False, True ] = False
./even ([ False ] : List Bool) = False
./even [ False ] = False
./even ([] : List Bool) = True
```

6
Prelude/Bool/odd
View File

@ -5,11 +5,11 @@ returns `False` otherwise
Examples:
```
./odd ([ True, False, True ] : List Bool) = False
./odd [ True, False, True ] = False
./odd ([ True, False ] : List Bool) = True
./odd [ True, False ] = True
./odd ([ True ] : List Bool) = True
./odd [ True ] = True
./odd ([] : List Bool) = False
```

2
Prelude/Bool/or
View File

@ -5,7 +5,7 @@ and returns `False` otherwise
Examples:
```
./or ([ True, False, True ] : List Bool) = True
./or [ True, False, True ] = True
./or ([] : List Bool) = False
```

2
Prelude/List/all
View File

@ -5,7 +5,7 @@ Returns `True` if the supplied function returns `True` for all elements in the
Examples:
```
./all Natural Natural/even ([ +2, +3, +5 ] : List Natural) = False
./all Natural Natural/even [ +2, +3, +5 ] = False
./all Natural Natural/even ([] : List Natural) = True
```

2
Prelude/List/any
View File

@ -5,7 +5,7 @@ Returns `True` if the supplied function returns `True` for any element in the
Examples:
```
./any Natural Natural/even ([ +2, +3, +5 ] : List Natural) = True
./any Natural Natural/even [ +2, +3, +5 ] = True
./any Natural Natural/even ([] : List Natural) = False
```

2
Prelude/List/build
View File

@ -11,7 +11,7 @@ Text
→ λ(nil : list)
→ cons "ABC" (cons "DEF" nil)
)
= [ "ABC", "DEF" ] : List Text
= [ "ABC", "DEF" ]
./build
Text

13
Prelude/List/concat
View File

@ -5,18 +5,17 @@ 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
[ [0, 1, 2]
, [3, 4]
, [5, 6, 7, 8]
]
= [ 0, 1, 2, 3, 4, 5, 6, 7, 8 ]
./concat Integer
( [ [] : List Integer
, [] : List Integer
, [] : List Integer
] : List (List Integer)
]
)
= [] : List Integer

2
Prelude/List/concatMap
View File

@ -6,7 +6,7 @@ Examples:
```
./concatMap Natural Natural (λ(n : Natural) → [n, n]) [+2, +3, +5]
= [ +2, +2, +3, +3, +5, +5 ] : List Natural
= [ +2, +2, +3, +3, +5, +5 ]
./concatMap Natural Natural (λ(n : Natural) → [n, n]) ([] : List Natural)
= [] : List Natural

8
Prelude/List/filter
View File

@ -4,11 +4,11 @@ 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/even [+2, +3, +5]
= [ +2 ]
./filter Natural Natural/odd ([+2, +3, +5] : List Natural)
= [ +3, +5 ] : List Natural
./filter Natural Natural/odd [+2, +3, +5]
= [ +3, +5 ]
```
-}
let filter

10
Prelude/List/fold
View File

@ -1,15 +1,15 @@
{-
`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
If you treat the list `[ x, y, z ]` 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)
[ +2, +3, +5 ]
Natural
(λ(x : Natural) → λ(y : Natural) → x + y)
+0
@ -18,7 +18,7 @@ Examples:
λ(nil : Natural)
→ ./fold
Natural
([ +2, +3, +5 ] : List Natural)
[ +2, +3, +5 ]
Natural
(λ(x : Natural) → λ(y : Natural) → x + y)
nil
@ -27,7 +27,7 @@ Examples:
λ(list : Type)
→ λ(cons : Natural → list → list)
→ λ(nil : list)
→ ./fold Natural ([ +2, +3, +5 ] : List Natural) list cons nil
→ ./fold Natural [ +2, +3, +5 ] list cons nil
= λ(list : Type)
→ λ(cons : Natural → list → list)
→ λ(nil : list)

2
Prelude/List/generate
View File

@ -5,7 +5,7 @@ up to but not including the supplied `Natural` number
Examples:
```
./generate +5 Bool Natural/even = [ True, False, True, False, True ] : List Bool
./generate +5 Bool Natural/even = [ True, False, True, False, True ]
./generate +0 Bool Natural/even = [] : List Bool
```

2
Prelude/List/head
View File

@ -4,7 +4,7 @@ Retrieve the first element of the list
Examples:
```
./head Integer ([ 0, 1, 2 ] : List Integer) = [ 0 ] : Optional Integer
./head Integer [ 0, 1, 2 ] = [ 0 ] : Optional Integer
./head Integer ([] : List Integer) = [] : Optional Integer
```

4
Prelude/List/indexed
View File

@ -4,11 +4,11 @@ Tag each element of the list with its index
Examples:
```
./indexed Bool ([ True, False, True ] : List Bool)
./indexed Bool [ True, False, True ]
= [ { index = +0, value = True }
, { index = +1, value = False }
, { index = +2, value = True }
] : List { index : Natural, value : Bool }
] : List { index : Natural, value : Bool }
./indexed Bool ([] : List Bool)
= [] : List { index : Natural, value : Bool }

2
Prelude/List/iterate
View File

@ -6,7 +6,7 @@ Examples:
```
./iterate +10 Natural (λ(x : Natural) → x * +2) +1
= [ +1, +2, +4, +8, +16, +32, +64, +128, +256, +512 ] : List Natural
= [ +1, +2, +4, +8, +16, +32, +64, +128, +256, +512 ]
./iterate +0 Natural (λ(x : Natural) → x * +2) +1
= [] : List Natural

2
Prelude/List/last
View File

@ -4,7 +4,7 @@ Retrieve the last element of the list
Examples:
```
./last Integer ([ 0, 1, 2 ] : List Integer) = [ 2 ] : Optional Integer
./last Integer [ 0, 1, 2 ] = [ 2 ] : Optional Integer
./last Integer ([] : List Integer) = [] : Optional Integer
```

2
Prelude/List/length
View File

@ -4,7 +4,7 @@ Returns the number of elements in a list
Examples:
```
./length Integer ([ 0, 1, 2 ] : List Integer) = +3
./length Integer [ 0, 1, 2 ] = +3
./length Integer ([] : List Integer) = +0
```

4
Prelude/List/map
View File

@ -4,8 +4,8 @@ Transform 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 [ +2, +3, +5 ]
= [ True, False, False ]
./map Natural Bool Natural/even ([] : List Natural)
= [] : List Bool

2
Prelude/List/null
View File

@ -4,7 +4,7 @@ Returns `True` if the `List` is empty and `False` otherwise
Examples:
```
./null Integer ([ 0, 1, 2 ] : List Integer) = False
./null Integer [ 0, 1, 2 ] = False
./null Integer ([] : List Integer) = True
```

2
Prelude/List/replicate
View File

@ -4,7 +4,7 @@ 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 +9 Integer 1 = [ 1, 1, 1, 1, 1, 1, 1, 1, 1 ]
./replicate +0 Integer 1 = [] : List Integer
```

2
Prelude/List/reverse
View File

@ -4,7 +4,7 @@ Reverse a list
Examples:
```
./reverse Integer ([ 0, 1, 2 ] : List Integer) = [ 2, 1, 0 ] : List Integer
./reverse Integer [ 0, 1, 2 ] = [ 2, 1, 0 ] : List Integer
./reverse Integer ([] : List Integer) = [] : List Integer
```

29
Prelude/List/shifted
View File

@ -7,20 +7,19 @@ 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 = +0, value = False }
, { index = +1, value = False }
]
, [ { index = +0, value = True }
, { index = +1, value = True }
, { index = +2, value = True }
, { index = +3, value = True }
]
]
= [ { index = +0, value = True }
, { index = +1, value = True }
, { index = +2, value = True }
@ -30,7 +29,7 @@ Bool
, { 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 }

6
Prelude/List/unzip
View File

@ -10,10 +10,10 @@ 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
= { _1 = [ "ABC", "DEF", "GHI" ]
, _2 = [ True, False, True ]
}
./unzip Text Bool ([] : List { _1 : Text, _2 : Bool })

2
Prelude/Natural/enumerate
View File

@ -5,7 +5,7 @@ number
Examples:
```
./enumerate +10 = [ +0, +1, +2, +3, +4, +5, +6, +7, +8, +9 ] : List Natural
./enumerate +10 = [ +0, +1, +2, +3, +4, +5, +6, +7, +8, +9 ]
./enumerate +0 = [] : List Natural
```

2
Prelude/Natural/product
View File

@ -4,7 +4,7 @@ Multiply all the numbers in a `List`
Examples:
```
./product ([ +2, +3, +5 ] : List Natural) = +30
./product [ +2, +3, +5 ] = +30
./product ([] : List Natural) = +1
```

2
Prelude/Natural/sum
View File

@ -4,7 +4,7 @@ Add all the numbers in a `List`
Examples:
```
./sum ([ +2, +3, +5 ] : List Natural) = +10
./sum [ +2, +3, +5 ] = +10
./sum ([] : List Natural) = +0
```

12
Prelude/Optional/head
View File

@ -6,17 +6,15 @@ Examples:
```
./head
Integer
( [ [ ] : Optional Integer
, [ 1 ] : Optional Integer
, [ 2 ] : Optional Integer
]
: List (Optional Integer)
)
[ [ ] : Optional Integer
, [ 1 ] : Optional Integer
, [ 2 ] : Optional Integer
]
= [ 1 ] : Optional Integer
./head
Integer
([ [] : Optional Integer, [] : Optional Integer ] : List (Optional Integer))
[ [] : Optional Integer, [] : Optional Integer ]
= [] : Optional Integer
./head Integer ([] : List (Optional Integer))

11
Prelude/Optional/last
View File

@ -6,16 +6,15 @@ Examples:
```
./last
Integer
( [ [ ] : Optional Integer
, [ 1 ] : Optional Integer
, [ 2 ] : Optional Integer
] : List (Optional Integer)
)
[ [ ] : Optional Integer
, [ 1 ] : Optional Integer
, [ 2 ] : Optional Integer
]
= [ 2 ] : Optional Integer
./last
Integer
([ [] : Optional Integer, [] : Optional Integer ] : List (Optional Integer))
[ [] : Optional Integer, [] : Optional Integer ]
= [] : Optional Integer
./last Integer ([] : List (Optional Integer))

2
Prelude/Text/concat
View File

@ -4,7 +4,7 @@ Concatenate all the `Text` values in a `List`
Examples:
```
./concat ([ "ABC", "DEF", "GHI" ] : List Text) = "ABCDEFGHI"
./concat [ "ABC", "DEF", "GHI" ] = "ABCDEFGHI"
./concat ([] : List Text) = ""
```

58
src/Dhall.hs
View File

@ -40,8 +40,9 @@ module Dhall
, lazyText
, strictText
, maybe
, vector
, sequence
, list
, vector
, unit
, string
, pair
@ -56,6 +57,7 @@ module Dhall
-- * Re-exports
, Natural
, Seq
, Text
, Vector
, Generic
@ -67,6 +69,7 @@ import Control.Monad.Trans.State.Strict
import Data.Functor.Contravariant (Contravariant(..))
import Data.Monoid ((<>))
import Data.Scientific (Scientific)
import Data.Sequence (Seq)
import Data.Text.Buildable (Buildable(..))
import Data.Text.Lazy (Text)
import Data.Typeable (Typeable)
@ -78,7 +81,7 @@ import Dhall.Parser (Src(..))
import Dhall.TypeCheck (DetailedTypeError(..), TypeError, X)
import GHC.Generics
import Numeric.Natural (Natural)
import Prelude hiding (maybe)
import Prelude hiding (maybe, sequence)
import Text.Trifecta.Delta (Delta(..))
import qualified Control.Exception
@ -434,20 +437,18 @@ Just 1
maybe :: Type a -> Type (Maybe a)
maybe (Type extractIn expectedIn) = Type extractOut expectedOut
where
extractOut (OptionalLit _ es) = traverse extractIn es'
where
es' = if Data.Vector.null es then Nothing else Just (Data.Vector.head es)
extractOut _ = Nothing
extractOut (OptionalLit _ es) = traverse extractIn es
extractOut _ = Nothing
expectedOut = App Optional expectedIn
{-| Decode a `Vector`
>>> input (vector integer) "[1, 2, 3]"
{-| Decode a `Seq`
-
>>> input (sequence integer) "[1, 2, 3]"
[1,2,3]
-}
vector :: Type a -> Type (Vector a)
vector (Type extractIn expectedIn) = Type extractOut expectedOut
sequence :: Type a -> Type (Seq a)
sequence (Type extractIn expectedIn) = Type extractOut expectedOut
where
extractOut (ListLit _ es) = traverse extractIn es
extractOut _ = Nothing
@ -460,7 +461,15 @@ vector (Type extractIn expectedIn) = Type extractOut expectedOut
[1,2,3]
-}
list :: Type a -> Type [a]
list = fmap Data.Vector.toList . vector
list = fmap Data.Foldable.toList . sequence
{-| Decode a `Vector`
>>> input (vector integer) "[1, 2, 3]"
[1,2,3]
-}
vector :: Type a -> Type (Vector a)
vector = fmap Data.Vector.fromList . list
{-| Decode `()` from an empty record.
@ -549,12 +558,15 @@ instance Interpret Data.Text.Text where
instance Interpret a => Interpret (Maybe a) where
autoWith opts = maybe (autoWith opts)
instance Interpret a => Interpret (Vector a) where
autoWith opts = vector (autoWith opts)
instance Interpret a => Interpret (Seq a) where
autoWith opts = sequence (autoWith opts)
instance Interpret a => Interpret [a] where
autoWith = fmap (fmap Data.Vector.toList) autoWith
instance Interpret a => Interpret (Vector a) where
autoWith opts = vector (autoWith opts)
instance (Inject a, Interpret b) => Interpret (a -> b) where
autoWith opts = Type extractOut expectedOut
where
@ -885,15 +897,15 @@ instance Inject a => Inject (Maybe a) where
injectWith options = InputType embedOut declaredOut
where
embedOut (Just x) =
OptionalLit declaredIn (Data.Vector.singleton (embedIn x))
OptionalLit declaredIn (pure (embedIn x))
embedOut Nothing =
OptionalLit declaredIn Data.Vector.empty
OptionalLit declaredIn empty
InputType embedIn declaredIn = injectWith options
declaredOut = App Optional declaredIn
instance Inject a => Inject (Vector a) where
instance Inject a => Inject (Seq a) where
injectWith options = InputType embedOut declaredOut
where
embedOut xs = ListLit (Just declaredIn) (fmap embedIn xs)
@ -903,15 +915,13 @@ instance Inject a => Inject (Vector a) where
InputType embedIn declaredIn = injectWith options
instance Inject a => Inject [a] where
injectWith = fmap (contramap Data.Vector.fromList) injectWith
injectWith = fmap (contramap Data.Sequence.fromList) injectWith
instance Inject a => Inject (Vector a) where
injectWith = fmap (contramap Data.Vector.toList) injectWith
instance Inject a => Inject (Data.Set.Set a) where
injectWith = fmap (contramap go) injectWith where
go se = Data.Vector.fromListN (Data.Set.size se) (Data.Foldable.toList se)
instance Inject a => Inject (Data.Sequence.Seq a) where
injectWith = fmap (contramap go) injectWith where
go se = Data.Vector.fromListN (Data.Sequence.length se) (Data.Foldable.toList se)
injectWith = fmap (contramap Data.Set.toList) injectWith
deriving instance (Inject a, Inject b) => Inject (a, b)

205
src/Dhall/Core.hs
View File

@ -6,6 +6,7 @@
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE UnicodeSyntax #-}
{-# OPTIONS_GHC -Wall #-}
{-| This module contains the core calculus for the Dhall language.
@ -57,12 +58,12 @@ import Data.HashSet (HashSet)
import Data.Monoid ((<>))
import Data.String (IsString(..))
import Data.Scientific (Scientific)
import Data.Sequence (Seq, ViewL(..), ViewR(..))
import Data.Text.Buildable (Buildable(..))
import Data.Text.Lazy (Text)
import Data.Text.Lazy.Builder (Builder)
import Data.Text.Prettyprint.Doc (Pretty)
import Data.Traversable
import Data.Vector (Vector)
import {-# SOURCE #-} Dhall.Pretty.Internal
import Numeric.Natural (Natural)
import Prelude hiding (succ)
@ -73,13 +74,11 @@ import qualified Data.ByteString.Char8
import qualified Data.ByteString.Base16
import qualified Data.HashMap.Strict.InsOrd
import qualified Data.HashSet
import qualified Data.Maybe
import qualified Data.Sequence
import qualified Data.Text
import qualified Data.Text.Lazy as Text
import qualified Data.Text.Lazy.Builder as Builder
import qualified Data.Text.Prettyprint.Doc as Pretty
import qualified Data.Vector
import qualified Data.Vector.Mutable
{-| Constants for a pure type system
@ -283,7 +282,7 @@ data Expr s a
| List
-- | > ListLit (Just t ) [x, y, z] ~ [x, y, z] : List t
-- > ListLit Nothing [x, y, z] ~ [x, y, z]
| ListLit (Maybe (Expr s a)) (Vector (Expr s a))
| ListLit (Maybe (Expr s a)) (Seq (Expr s a))
-- | > ListAppend x y ~ x # y
| ListAppend (Expr s a) (Expr s a)
-- | > ListBuild ~ List/build
@ -302,9 +301,9 @@ data Expr s a
| ListReverse
-- | > Optional ~ Optional
| Optional
-- | > OptionalLit t [e] ~ [e] : Optional t
-- > OptionalLit t [] ~ [] : Optional t
| OptionalLit (Expr s a) (Vector (Expr s a))
-- | > OptionalLit t (Just e) ~ [e] : Optional t
-- > OptionalLit t Nothing ~ [] : Optional t
| OptionalLit (Expr s a) (Maybe (Expr s a))
-- | > OptionalFold ~ Optional/fold
| OptionalFold
-- | > OptionalBuild ~ Optional/build
@ -965,14 +964,6 @@ denote (Embed a ) = Embed a
normalizeWith :: Normalizer a -> Expr s a -> Expr t a
normalizeWith ctx e0 = loop (denote e0)
where
-- This is to avoid a `Show` constraint on the @a@ and @s@ in the type of
-- `loop`. In theory, this might change a failing repro case into
-- a successful one, but the risk of that is low enough to not warrant
-- the `Show` constraint. I care more about proving at the type level
-- that the @a@ and @s@ type parameters are never used
e'' = bimap (\_ -> ()) (\_ -> ()) e0
text = "NormalizeWith.loop (" <> Data.Text.pack (show e'') <> ")"
loop e = case e of
Const k -> Const k
Var v -> Var v
@ -991,16 +982,14 @@ normalizeWith ctx e0 = loop (denote e0)
b' = subst (V x 0) a' b
b'' = shift (-1) (V x 0) b'
f' -> case App f' a' of
-- fold/build fusion for `List`
-- build/fold fusion for `List`
App (App ListBuild _) (App (App ListFold _) e') -> loop e'
App (App ListFold _) (App (App ListBuild _) e') -> loop e'
-- fold/build fusion for `Natural`
App NaturalBuild (App NaturalFold e') -> loop e'
App NaturalFold (App NaturalBuild e') -> loop e'
-- fold/build fusion for `Optional`
-- build/fold fusion for `Natural`
App NaturalBuild (App NaturalFold e') -> loop e'
-- build/fold fusion for `Optional`
App (App OptionalBuild _) (App (App OptionalFold _) e') -> loop e'
App (App OptionalFold _) (App (App OptionalBuild _) e') -> loop e'
App (App (App (App NaturalFold (NaturalLit n0)) t) succ') zero ->
if boundedType (loop t) then strict else lazy
@ -1013,23 +1002,11 @@ normalizeWith ctx e0 = loop (denote e0)
lazyLoop !0 = zero
lazyLoop !n = App succ' (lazyLoop (n - 1))
App NaturalBuild k
| check -> NaturalLit n
| otherwise -> App f' a'
App NaturalBuild g -> loop (App (App (App g Natural) succ) zero)
where
labeled =
loop (App (App (App k Natural) "Succ") "Zero")
succ = Lam "x" Natural (NaturalPlus "x" (NaturalLit 1))
n = go 0 labeled
where
go !m (App (Var "Succ") e') = go (m + 1) e'
go !m (Var "Zero") = m
go !_ _ = internalError text
check = go labeled
where
go (App (Var "Succ") e') = go e'
go (Var "Zero") = True
go _ = False
zero = NaturalLit 0
App NaturalIsZero (NaturalLit n) -> BoolLit (n == 0)
App NaturalEven (NaturalLit n) -> BoolLit (even n)
App NaturalOdd (NaturalLit n) -> BoolLit (odd n)
@ -1040,44 +1017,35 @@ normalizeWith ctx e0 = loop (denote e0)
TextLit (Chunks [] (buildNumber n))
App DoubleShow (DoubleLit n) ->
TextLit (Chunks [] (buildScientific n))
App (App OptionalBuild t) k
| check -> OptionalLit t k'
| otherwise -> App f' a'
App (App OptionalBuild _A₀) g ->
loop (App (App (App g optional) just) nothing)
where
labeled = loop (App (App (App k (App Optional t)) "Just") "Nothing")
_A₁ = shift 1 "a" _A₀
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'
optional = App Optional _A₀
just = Lam "a" _A₀ (OptionalLit _A₁ (pure "a"))
nothing = OptionalLit _A₀ empty
App (App ListBuild _A₀) g -> loop (App (App (App g list) cons) nil)
where
labeled =
loop (App (App (App k (App List t)) "Cons") "Nil")
_A₁ = shift 1 "a" _A₀
k' cons nil = go labeled
where
go (App (App (Var "Cons") x) e') = cons x (go e')
go (Var "Nil") = nil
go _ = internalError text
check = go labeled
where
go (App (App (Var "Cons") _) e') = go e'
go (Var "Nil") = True
go _ = False
list = App List _A₀
cons =
Lam "a" _A₀
(Lam "as"
(App List _A₁)
(ListAppend (ListLit Nothing (pure "a")) "as")
)
nil = ListLit (Just _A₀) empty
App (App (App (App (App ListFold _) (ListLit _ xs)) t) cons) nil ->
if boundedType (loop t) then strict else lazy
where
strict = Data.Vector.foldr strictCons strictNil xs
lazy = loop (Data.Vector.foldr lazyCons lazyNil xs)
strict = foldr strictCons strictNil xs
lazy = loop (foldr lazyCons lazyNil xs)
strictNil = loop nil
lazyNil = nil
@ -1085,35 +1053,40 @@ normalizeWith ctx e0 = loop (denote e0)
strictCons y ys = loop (App (App cons y) ys)
lazyCons y ys = App (App cons y) ys
App (App ListLength _) (ListLit _ ys) ->
NaturalLit (fromIntegral (Data.Vector.length ys))
App (App ListHead t) (ListLit _ ys) ->
loop (OptionalLit t (Data.Vector.take 1 ys))
App (App ListLast t) (ListLit _ ys) ->
loop (OptionalLit t y)
NaturalLit (fromIntegral (Data.Sequence.length ys))
App (App ListHead t) (ListLit _ ys) -> loop (OptionalLit t m)
where
y = if Data.Vector.null ys
then Data.Vector.empty
else Data.Vector.singleton (Data.Vector.last ys)
App (App ListIndexed t) (ListLit _ xs) ->
loop (ListLit (Just t') (fmap adapt (Data.Vector.indexed xs)))
m = case Data.Sequence.viewl ys of
y :< _ -> Just y
_ -> Nothing
App (App ListLast t) (ListLit _ ys) -> loop (OptionalLit t m)
where
t' = Record (Data.HashMap.Strict.InsOrd.fromList kts)
m = case Data.Sequence.viewr ys of
_ :> y -> Just y
_ -> Nothing
App (App ListIndexed _A₀) (ListLit _A₁ as₀) ->
loop (ListLit (Just _A₂) as₁)
where
as₁ = Data.Sequence.mapWithIndex adapt as₀
_A₂ = Record (Data.HashMap.Strict.InsOrd.fromList kts)
where
kts = [ ("index", Natural)
, ("value", t)
, ("value", _A₀)
]
adapt (n, x) = RecordLit (Data.HashMap.Strict.InsOrd.fromList kvs)
adapt n a_ =
RecordLit (Data.HashMap.Strict.InsOrd.fromList kvs)
where
kvs = [ ("index", NaturalLit (fromIntegral n))
, ("value", x)
, ("value", a_)
]
App (App ListReverse t) (ListLit _ xs) ->
loop (ListLit (Just t) (Data.Vector.reverse xs))
loop (ListLit (Just t) (Data.Sequence.reverse xs))
App (App (App (App (App OptionalFold _) (OptionalLit _ xs)) _) just) nothing ->
loop (maybe nothing just' (toMaybe xs))
loop (maybe nothing just' xs)
where
just' y = App just y
toMaybe = Data.Maybe.listToMaybe . Data.Vector.toList
just' = App just
_ -> case ctx (App f' a') of
Nothing -> App f' a'
Just app' -> loop app'
@ -1350,28 +1323,17 @@ isNormalized e = case denote e of
App f a -> isNormalized f && isNormalized a && case App f a of
App (Lam _ _ _) _ -> False
-- fold/build fusion for `List`
-- build/fold fusion for `List`
App (App ListBuild _) (App (App ListFold _) _) -> False
App (App ListFold _) (App (App ListBuild _) _) -> False
-- fold/build fusion for `Natural`
-- build/fold fusion for `Natural`
App NaturalBuild (App NaturalFold _) -> False
App NaturalFold (App NaturalBuild _) -> False
-- fold/build fusion for `Optional`
-- build/fold 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
check0 (Lam _ _ (Lam succ _ (Lam zero _ k))) = check1 succ zero k
check0 _ = False
check1 succ zero (App (Var (V succ' n)) k) =
succ == succ' && n == (if succ == zero then 1 else 0) && check1 succ zero k
check1 _ zero (Var (V zero' 0)) = zero == zero'
check1 _ _ _ = False
App NaturalBuild _ -> False
App NaturalIsZero (NaturalLit _) -> False
App NaturalEven (NaturalLit _) -> False
App NaturalOdd (NaturalLit _) -> False
@ -1379,24 +1341,8 @@ isNormalized e = case denote e of
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
check0 _ = False
check1 cons nil (App (Var (V cons' n)) k) =
cons == cons' && n == (if cons == nil then 1 else 0) && check1 cons nil k
check1 _ nil (Var (V nil' 0)) = nil == nil'
check1 _ _ _ = False
App (App OptionalBuild _) _ -> False
App (App ListBuild _) _ -> False
App (App (App (App (App ListFold _) (ListLit _ _)) _) _) _ ->
False
App (App ListLength _) (ListLit _ _) -> False
@ -1565,25 +1511,6 @@ internalError text = error (unlines
, "``` "
] )
buildVector :: (forall x . (a -> x -> x) -> x -> x) -> Vector a
buildVector f = Data.Vector.reverse (Data.Vector.create (do
let cons a st = do
(len, cap, mv) <- st
if len < cap
then do
Data.Vector.Mutable.write mv len a
return (len + 1, cap, mv)
else do
let cap' = 2 * cap
mv' <- Data.Vector.Mutable.unsafeGrow mv cap'
Data.Vector.Mutable.write mv' len a
return (len + 1, cap', mv')
let nil = do
mv <- Data.Vector.Mutable.unsafeNew 1
return (0, 1, mv)
(len, _, mv) <- f cons nil
return (Data.Vector.Mutable.slice 0 len mv) ))
-- | The set of reserved identifiers for the Dhall language
reservedIdentifiers :: HashSet Text
reservedIdentifiers =

4
src/Dhall/Import.hs
View File

@ -166,6 +166,7 @@ import qualified Data.ByteString.Base16
import qualified Data.ByteString.Char8
import qualified Data.ByteString.Lazy
import qualified Data.CaseInsensitive
import qualified Data.Foldable
import qualified Data.List as List
import qualified Data.HashMap.Strict.InsOrd
import qualified Data.Map.Strict as Map
@ -175,7 +176,6 @@ import qualified Data.Text.Lazy as Text
import qualified Data.Text.Lazy.Builder as Builder
import qualified Data.Text.Lazy.Encoding
import qualified Data.Text.Lazy.IO
import qualified Data.Vector
import qualified Dhall.Core
import qualified Dhall.Parser
import qualified Dhall.Context
@ -481,7 +481,7 @@ toHeaders
-> Maybe [(CI Data.ByteString.ByteString, Data.ByteString.ByteString)]
toHeaders (ListLit _ hs) = do
hs' <- mapM toHeader hs
return (Data.Vector.toList hs')
return (Data.Foldable.toList hs')
toHeaders _ = do
empty

9
src/Dhall/Parser.hs
View File

@ -56,7 +56,6 @@ import qualified Data.Text.Encoding
import qualified Data.Text.Lazy
import qualified Data.Text.Lazy.Builder
import qualified Data.Text.Lazy.Encoding
import qualified Data.Vector
import qualified Text.Parser.Char
import qualified Text.Parser.Combinators
import qualified Text.Parser.Token
@ -1070,15 +1069,15 @@ emptyCollection embedded = do
_colon
a <- alternative0 <|> alternative1
b <- selectorExpression embedded
return (a b empty)
return (a b)
where
alternative0 = do
_List
return (\a b -> ListLit (Just a) b)
return (\a -> ListLit (Just a) empty)
alternative1 = do
_Optional
return OptionalLit
return (\a -> OptionalLit a empty)
nonEmptyOptional :: Parser a -> Parser (Expr Src a)
nonEmptyOptional embedded = do
@ -1459,7 +1458,7 @@ nonEmptyListLiteral embedded = (do
a <- expression embedded
b <- many (do _comma; expression embedded)
_closeBracket
return (ListLit Nothing (Data.Vector.fromList (a:b))) ) <?> "list literal"
return (ListLit Nothing (Data.Sequence.fromList (a:b))) ) <?> "list literal"
completeExpression :: Parser a -> Parser (Expr Src a)
completeExpression embedded = do

17
src/Dhall/Pretty/Internal.hs
View File

@ -46,7 +46,6 @@ import qualified Data.Text.Lazy as Text
import qualified Data.Text.Lazy.Builder as Builder
import qualified Data.Text.Prettyprint.Doc as Pretty
import qualified Data.Text.Prettyprint.Doc.Render.Text as Pretty
import qualified Data.Vector
{-| Annotation type used to tag elements in a pretty-printed document for
syntax highlighting purposes
@ -433,13 +432,13 @@ prettyExprB a0@(Let _ _ _ _) =
docs d =
[ prettyExprB d ]
prettyExprB (ListLit Nothing b) =
list (map prettyExprA (Data.Vector.toList b))
list (map prettyExprA (Data.Foldable.toList b))
prettyExprB (ListLit (Just a) b) =
list (map prettyExprA (Data.Vector.toList b))
list (map prettyExprA (Data.Foldable.toList b))
<> " : "
<> prettyExprD (App List a)
prettyExprB (OptionalLit a b) =
list (map prettyExprA (Data.Vector.toList b))
list (map prettyExprA (Data.Foldable.toList b))
<> " : "
<> prettyExprD (App Optional a)
prettyExprB (Merge a b (Just c)) =
@ -702,7 +701,7 @@ prettyExprF (Union a) =
prettyExprF (UnionLit a b c) =
prettyUnionLit a b c
prettyExprF (ListLit Nothing b) =
list (map prettyExprA (Data.Vector.toList b))
list (map prettyExprA (Data.Foldable.toList b))
prettyExprF (Embed a) =
Pretty.pretty a
prettyExprF (Note _ b) =
@ -886,11 +885,11 @@ buildExprB (Let a (Just b) c d) =
<> " in "
<> buildExprB d
buildExprB (ListLit Nothing b) =
"[" <> buildElems (Data.Vector.toList b) <> "]"
"[" <> buildElems (Data.Foldable.toList b) <> "]"
buildExprB (ListLit (Just a) b) =
"[" <> buildElems (Data.Vector.toList b) <> "] : List " <> buildExprE a
"[" <> buildElems (Data.Foldable.toList b) <> "] : List " <> buildExprE a
buildExprB (OptionalLit a b) =
"[" <> buildElems (Data.Vector.toList b) <> "] : Optional " <> buildExprE a
"[" <> buildElems (Data.Foldable.toList b) <> "] : Optional " <> buildExprE a
buildExprB (Merge a b (Just c)) =
"merge " <> buildExprE a <> " " <> buildExprE b <> " : " <> buildExprD c
buildExprB (Merge a b Nothing) =
@ -1054,7 +1053,7 @@ buildExprF (Union a) =
buildExprF (UnionLit a b c) =
buildUnionLit a b c
buildExprF (ListLit Nothing b) =
"[" <> buildElems (Data.Vector.toList b) <> "]"
"[" <> buildElems (Data.Foldable.toList b) <> "]"
buildExprF (Embed a) =
build a
buildExprF (Note _ b) =

89
src/Dhall/TypeCheck.hs
View File

@ -25,6 +25,7 @@ import Control.Exception (Exception)
import Data.Foldable (forM_, toList)
import Data.HashMap.Strict.InsOrd (InsOrdHashMap)
import Data.Monoid ((<>))
import Data.Sequence (Seq, ViewL(..))
import Data.Set (Set)
import Data.Text.Buildable (Buildable(..))
import Data.Text.Lazy (Text)
@ -36,17 +37,22 @@ import Dhall.Core (Const(..), Chunks(..), Expr(..), Var(..))
import Dhall.Context (Context)
import qualified Control.Monad.Trans.State.Strict as State
import qualified Data.Foldable
import qualified Data.HashMap.Strict
import qualified Data.HashMap.Strict.InsOrd
import qualified Data.List
import qualified Data.Ord
import qualified Data.Sequence
import qualified Data.Set
import qualified Data.Text.Lazy as Text
import qualified Data.Text.Lazy.Builder as Builder
import qualified Data.Vector
import qualified Dhall.Context
import qualified Dhall.Core
traverseWithIndex_ :: Applicative f => (Int -> a -> f b) -> Seq a -> f ()
traverseWithIndex_ k xs =
Data.Foldable.sequenceA_ (Data.Sequence.mapWithIndex k xs)
axiom :: Const -> Either (TypeError s a) Const
axiom Type = return Kind
axiom Kind = Left (TypeError Dhall.Context.empty (Const Kind) Untyped)
@ -388,15 +394,14 @@ typeWithA tpa = loop
loop _ List = do
return (Pi "_" (Const Type) (Const Type))
loop ctx e@(ListLit Nothing xs) = do
if Data.Vector.null xs
then Left (TypeError ctx e MissingListType)
else do
t <- loop ctx (Data.Vector.head xs)
case Data.Sequence.viewl xs of
x0 :< _ -> do
t <- loop ctx x0
s <- fmap Dhall.Core.normalize (loop ctx t)
case s of
Const Type -> return ()
_ -> Left (TypeError ctx e (InvalidListType t))
flip Data.Vector.imapM_ xs (\i x -> do
flip traverseWithIndex_ xs (\i x -> do
t' <- loop ctx x
if propEqual t t'
then return ()
@ -406,12 +411,13 @@ typeWithA tpa = loop
let err = MismatchedListElements i nf_t x nf_t'
Left (TypeError ctx x err) )
return (App List t)
_ -> Left (TypeError ctx e MissingListType)
loop ctx e@(ListLit (Just t ) xs) = do
s <- fmap Dhall.Core.normalize (loop ctx t)
case s of
Const Type -> return ()
_ -> Left (TypeError ctx e (InvalidListType t))
flip Data.Vector.imapM_ xs (\i x -> do
flip traverseWithIndex_ xs (\i x -> do
t' <- loop ctx x
if propEqual t t'
then return ()
@ -470,10 +476,6 @@ typeWithA tpa = loop
case s of
Const Type -> return ()
_ -> Left (TypeError ctx e (InvalidOptionalType t))
let n = Data.Vector.length xs
if 2 <= n
then Left (TypeError ctx e (InvalidOptionalLiteral n))
else return ()
forM_ xs (\x -> do
t' <- loop ctx x
if propEqual t t'
@ -714,7 +716,6 @@ data TypeMessage s a
| InvalidListElement Int (Expr s a) (Expr s a) (Expr s a)
| InvalidListType (Expr s a)
| InvalidOptionalElement (Expr s a) (Expr s a) (Expr s a)
| InvalidOptionalLiteral Int
| InvalidOptionalType (Expr s a)
| InvalidPredicate (Expr s a) (Expr s a)
| IfBranchMismatch (Expr s a) (Expr s a) (Expr s a) (Expr s a)
@ -1895,70 +1896,6 @@ prettyTypeMessage (InvalidOptionalElement expr0 expr1 expr2) = ErrorMessages {..
txt1 = build expr1
txt2 = build expr2
prettyTypeMessage (InvalidOptionalLiteral n) = ErrorMessages {..}
where
short = "Multiple ❰Optional❱ elements not allowed"
long =
"Explanation: The syntax for ❰Optional❱ values resembles the syntax for ❰List❱s: \n\
\ \n\
\ \n\
\ ┌───────────────────────┐ \n\
\ │ [] : Optional Integer │ An ❰Optional❱ value which is absent \n\
\ └───────────────────────┘ \n\
\ \n\
\ \n\
\ ┌───────────────────────┐ \n\
\ │ [] : List Integer │ An empty (0-element) ❰List❱ \n\
\ └───────────────────────┘ \n\
\ \n\
\ \n\
\ ┌────────────────────────┐ \n\
\ │ [1] : Optional Integer │ An ❰Optional❱ value which is present \n\
\ └────────────────────────┘ \n\
\ \n\
\ \n\
\ ┌────────────────────────┐ \n\
\ │ [1] : List Integer │ A singleton (1-element) ❰List❱ \n\
\ └────────────────────────┘ \n\
\ \n\
\ \n\
\However, an ❰Optional❱ value can " <> _NOT <> " have more than one element, whereas a\n\
\❰List❱ can have multiple elements: \n\
\ \n\
\ \n\
\ ┌───────────────────────────┐ \n\
\ │ [1, 2] : Optional Integer │ Invalid: multiple elements " <> _NOT <> " allowed\n\
\ └───────────────────────────┘ \n\
\ \n\
\ \n\
\ ┌───────────────────────────┐ \n\
\ │ [1, 2] : List Integer │ Valid: multiple elements allowed \n\
\ └───────────────────────────┘ \n\
\ \n\
\ \n\
\Some common reasons why you might get this error: \n\
\ \n\
\● You accidentally typed ❰Optional❱ when you meant ❰List❱, like this: \n\
\ \n\
\ \n\
\ ┌────────────────────────────────────────────────────┐ \n\
\ │ List/length Integer ([1, 2, 3] : Optional Integer) │ \n\
\ └────────────────────────────────────────────────────┘ \n\
\ ⇧ \n\
\ This should be ❰List❱ instead \n\
\ \n\
\ \n\
\────────────────────────────────────────────────────────────────────────────────\n\
\ \n\
\Your ❰Optional❱ value had this many elements: \n\
\ \n\
\↳ " <> txt0 <> " \n\
\ \n\
\... when an ❰Optional❱ value can only have at most one element \n"
where
txt0 = build n
prettyTypeMessage (InvalidFieldType k expr0) = ErrorMessages {..}
where
short = "Invalid field type"

167
tests/Examples.hs
View File

@ -275,7 +275,7 @@ exampleTests =
_Bool_and_0 :: TestTree
_Bool_and_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code "./Prelude/Bool/and ([ True, False, True ] : List Bool)"
e <- Util.code "./Prelude/Bool/and [ True, False, True ]"
Util.assertNormalizesTo e "False" )
_Bool_and_1 :: TestTree
@ -297,17 +297,17 @@ _Bool_build_1 = Test.Tasty.HUnit.testCase "Example #1" (do
_Bool_even_0 :: TestTree
_Bool_even_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code "./Prelude/Bool/even ([ False, True, False ] : List Bool)"
e <- Util.code "./Prelude/Bool/even [ False, True, False ]"
Util.assertNormalizesTo e "True" )
_Bool_even_1 :: TestTree
_Bool_even_1 = Test.Tasty.HUnit.testCase "Example #1" (do
e <- Util.code "./Prelude/Bool/even ([ False, True ] : List Bool)"
e <- Util.code "./Prelude/Bool/even [ False, True ]"
Util.assertNormalizesTo e "False" )
_Bool_even_2 :: TestTree
_Bool_even_2 = Test.Tasty.HUnit.testCase "Example #2" (do
e <- Util.code "./Prelude/Bool/even ([ False ] : List Bool)"
e <- Util.code "./Prelude/Bool/even [ False ]"
Util.assertNormalizesTo e "False" )
_Bool_even_3 :: TestTree
@ -337,17 +337,17 @@ _Bool_not_1 = Test.Tasty.HUnit.testCase "Example #1" (do
_Bool_odd_0 :: TestTree
_Bool_odd_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code "./Prelude/Bool/odd ([ True, False, True ] : List Bool)"
e <- Util.code "./Prelude/Bool/odd [ True, False, True ]"
Util.assertNormalizesTo e "False" )
_Bool_odd_1 :: TestTree
_Bool_odd_1 = Test.Tasty.HUnit.testCase "Example #1" (do
e <- Util.code "./Prelude/Bool/odd ([ True, False ] : List Bool)"
e <- Util.code "./Prelude/Bool/odd [ True, False ]"
Util.assertNormalizesTo e "True" )
_Bool_odd_2 :: TestTree
_Bool_odd_2 = Test.Tasty.HUnit.testCase "Example #2" (do
e <- Util.code "./Prelude/Bool/odd ([ True ] : List Bool)"
e <- Util.code "./Prelude/Bool/odd [ True ]"
Util.assertNormalizesTo e "True" )
_Bool_odd_3 :: TestTree
@ -357,7 +357,7 @@ _Bool_odd_3 = Test.Tasty.HUnit.testCase "Example #3" (do
_Bool_or_0 :: TestTree
_Bool_or_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code "./Prelude/Bool/or ([ True, False, True ] : List Bool)"
e <- Util.code "./Prelude/Bool/or [ True, False, True ]"
Util.assertNormalizesTo e "True" )
_Bool_or_1 :: TestTree
@ -397,7 +397,7 @@ _Integer_show_1 = Test.Tasty.HUnit.testCase "Example #1" (do
_List_all_0 :: TestTree
_List_all_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code "./Prelude/List/all Natural Natural/even ([ +2, +3, +5 ] : List Natural)"
e <- Util.code "./Prelude/List/all Natural Natural/even [ +2, +3, +5 ]"
Util.assertNormalizesTo e "False" )
_List_all_1 :: TestTree
@ -407,7 +407,7 @@ _List_all_1 = Test.Tasty.HUnit.testCase "Example #1" (do
_List_any_0 :: TestTree
_List_any_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code "./Prelude/List/any Natural Natural/even ([ +2, +3, +5 ] : List Natural)"
e <- Util.code "./Prelude/List/any Natural Natural/even [ +2, +3, +5 ]"
Util.assertNormalizesTo e "True" )
_List_any_1 :: TestTree
@ -425,7 +425,7 @@ _List_build_0 = Test.Tasty.HUnit.testCase "Example #0" (do
\→ λ(nil : list) \n\
\→ cons \"ABC\" (cons \"DEF\" nil)\n\
\) \n"
Util.assertNormalizesTo e "[ \"ABC\", \"DEF\" ] : List Text" )
Util.assertNormalizesTo e "[ \"ABC\", \"DEF\" ]" )
_List_build_1 :: TestTree
_List_build_1 = Test.Tasty.HUnit.testCase "Example #1" (do
@ -442,30 +442,28 @@ _List_build_1 = Test.Tasty.HUnit.testCase "Example #1" (do
_List_concat_0 :: TestTree
_List_concat_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code
"./Prelude/List/concat Integer \n\
\( [ [0, 1, 2] : List Integer\n\
\ , [3, 4] : List Integer\n\
\ , [5, 6, 7, 8] : List Integer\n\
\ ] : List (List Integer) \n\
\) \n"
Util.assertNormalizesTo e "[ 0, 1, 2, 3, 4, 5, 6, 7, 8 ] : List Integer" )
"./Prelude/List/concat Integer\n\
\[ [0, 1, 2] \n\
\, [3, 4] \n\
\, [5, 6, 7, 8] \n\
\] \n"
Util.assertNormalizesTo e "[ 0, 1, 2, 3, 4, 5, 6, 7, 8 ]" )
_List_concat_1 :: TestTree
_List_concat_1 = Test.Tasty.HUnit.testCase "Example #1" (do
e <- Util.code
"./Prelude/List/concat Integer\n\
\( [ [] : List Integer \n\
\ , [] : List Integer \n\
\ , [] : List Integer \n\
\ ] : List (List Integer)\n\
\) \n"
\[ [] : List Integer \n\
\, [] : List Integer \n\
\, [] : List Integer \n\
\] \n"
Util.assertNormalizesTo e "[] : List Integer" )
_List_concatMap_0 :: TestTree
_List_concatMap_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code
"./Prelude/List/concatMap Natural Natural (λ(n : Natural) → [n, n]) [+2, +3, +5]"
Util.assertNormalizesTo e "[ +2, +2, +3, +3, +5, +5 ] : List Natural" )
Util.assertNormalizesTo e "[ +2, +2, +3, +3, +5, +5 ]" )
_List_concatMap_1 :: TestTree
_List_concatMap_1 = Test.Tasty.HUnit.testCase "Example #1" (do
@ -476,20 +474,20 @@ _List_concatMap_1 = Test.Tasty.HUnit.testCase "Example #1" (do
_List_filter_0 :: TestTree
_List_filter_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code
"./Prelude/List/filter Natural Natural/even ([+2, +3, +5] : List Natural)"
Util.assertNormalizesTo e "[ +2 ] : List Natural" )
"./Prelude/List/filter Natural Natural/even [+2, +3, +5]"
Util.assertNormalizesTo e "[ +2 ]" )
_List_filter_1 :: TestTree
_List_filter_1 = Test.Tasty.HUnit.testCase "Example #1" (do
e <- Util.code "./Prelude/List/filter Natural Natural/odd ([+2, +3, +5] : List Natural)"
Util.assertNormalizesTo e "[ +3, +5 ] : List Natural" )
e <- Util.code "./Prelude/List/filter Natural Natural/odd [+2, +3, +5]"
Util.assertNormalizesTo e "[ +3, +5 ]" )
_List_fold_0 :: TestTree
_List_fold_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code
"./Prelude/List/fold \n\
\Natural \n\
\([ +2, +3, +5 ] : List Natural) \n\
\[ +2, +3, +5 ] \n\
\Natural \n\
\(λ(x : Natural) → λ(y : Natural) → x + y)\n\
\+0 \n"
@ -501,7 +499,7 @@ _List_fold_1 = Test.Tasty.HUnit.testCase "Example #1" (do
" λ(nil : Natural) \n\
\→ ./Prelude/List/fold \n\
\ Natural \n\
\ ([ +2, +3, +5 ] : List Natural) \n\
\ [ +2, +3, +5 ] \n\
\ Natural \n\
\ (λ(x : Natural) → λ(y : Natural) → x + y)\n\
\ nil \n"
@ -513,13 +511,13 @@ _List_fold_2 = Test.Tasty.HUnit.testCase "Example #2" (do
" λ(list : Type) \n\
\→ λ(cons : Natural → list → list) \n\
\→ λ(nil : list) \n\
\→ ./Prelude/List/fold Natural ([ +2, +3, +5 ] : List Natural) list cons nil\n"
\→ ./Prelude/List/fold Natural [ +2, +3, +5 ] list cons nil\n"
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 "./Prelude/List/generate +5 Bool Natural/even"
Util.assertNormalizesTo e "[ True, False, True, False, True ] : List Bool" )
Util.assertNormalizesTo e "[ True, False, True, False, True ]" )
_List_generate_1 :: TestTree
_List_generate_1 = Test.Tasty.HUnit.testCase "Example #1" (do
@ -528,7 +526,7 @@ _List_generate_1 = Test.Tasty.HUnit.testCase "Example #1" (do
_List_head_0 :: TestTree
_List_head_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code "./Prelude/List/head Integer ([ 0, 1, 2 ] : List Integer)"
e <- Util.code "./Prelude/List/head Integer [ 0, 1, 2 ]"
Util.assertNormalizesTo e "[ 0 ] : Optional Integer" )
_List_head_1 :: TestTree
@ -538,7 +536,7 @@ _List_head_1 = Test.Tasty.HUnit.testCase "Example #1" (do
_List_indexed_0 :: TestTree
_List_indexed_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code "./Prelude/List/indexed Bool ([ True, False, True ] : List Bool)"
e <- Util.code "./Prelude/List/indexed Bool [ True, False, True ]"
Util.assertNormalizesTo e "[ { index = +0, value = True }, { index = +1, value = False }, { index = +2, value = True } ] : List { index : Natural, value : Bool }" )
_List_indexed_1 :: TestTree
@ -549,7 +547,7 @@ _List_indexed_1 = Test.Tasty.HUnit.testCase "Example #1" (do
_List_iterate_0 :: TestTree
_List_iterate_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code "./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" )
Util.assertNormalizesTo e "[ +1, +2, +4, +8, +16, +32, +64, +128, +256, +512 ]" )
_List_iterate_1 :: TestTree
_List_iterate_1 = Test.Tasty.HUnit.testCase "Example #1" (do
@ -558,7 +556,7 @@ _List_iterate_1 = Test.Tasty.HUnit.testCase "Example #1" (do
_List_last_0 :: TestTree
_List_last_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code "./Prelude/List/last Integer ([ 0, 1, 2 ] : List Integer)"
e <- Util.code "./Prelude/List/last Integer [ 0, 1, 2 ]"
Util.assertNormalizesTo e "[ 2 ] : Optional Integer" )
_List_last_1 :: TestTree
@ -568,7 +566,7 @@ _List_last_1 = Test.Tasty.HUnit.testCase "Example #1" (do
_List_length_0 :: TestTree
_List_length_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code "./Prelude/List/length Integer ([ 0, 1, 2 ] : List Integer)"
e <- Util.code "./Prelude/List/length Integer [ 0, 1, 2 ]"
Util.assertNormalizesTo e "+3" )
_List_length_1 :: TestTree
@ -579,8 +577,8 @@ _List_length_1 = Test.Tasty.HUnit.testCase "Example #1" (do
_List_map_0 :: TestTree
_List_map_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code
"./Prelude/List/map Natural Bool Natural/even ([ +2, +3, +5 ] : List Natural)"
Util.assertNormalizesTo e "[ True, False, False ] : List Bool" )
"./Prelude/List/map Natural Bool Natural/even [ +2, +3, +5 ]"
Util.assertNormalizesTo e "[ True, False, False ]" )
_List_map_1 :: TestTree
_List_map_1 = Test.Tasty.HUnit.testCase "Example #1" (do
@ -589,7 +587,7 @@ _List_map_1 = Test.Tasty.HUnit.testCase "Example #1" (do
_List_null_0 :: TestTree
_List_null_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code "./Prelude/List/null Integer ([ 0, 1, 2 ] : List Integer)"
e <- Util.code "./Prelude/List/null Integer [ 0, 1, 2 ]"
Util.assertNormalizesTo e "False" )
_List_null_1 :: TestTree
@ -600,7 +598,7 @@ _List_null_1 = Test.Tasty.HUnit.testCase "Example #1" (do
_List_replicate_0 :: TestTree
_List_replicate_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code "./Prelude/List/replicate +9 Integer 1"
Util.assertNormalizesTo e "[ 1, 1, 1, 1, 1, 1, 1, 1, 1 ] : List Integer" )
Util.assertNormalizesTo e "[ 1, 1, 1, 1, 1, 1, 1, 1, 1 ]" )
_List_replicate_1 :: TestTree
_List_replicate_1 = Test.Tasty.HUnit.testCase "Example #1" (do
@ -609,7 +607,7 @@ _List_replicate_1 = Test.Tasty.HUnit.testCase "Example #1" (do
_List_reverse_0 :: TestTree
_List_reverse_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code "./Prelude/List/reverse Integer ([0, 1, 2] : List Integer)"
e <- Util.code "./Prelude/List/reverse Integer [0, 1, 2]"
Util.assertNormalizesTo e "[ 2, 1, 0 ] : List Integer" )
_List_reverse_1 :: TestTree
@ -620,23 +618,22 @@ _List_reverse_1 = Test.Tasty.HUnit.testCase "Example #1" (do
_List_shifted_0 :: TestTree
_List_shifted_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code
"./Prelude/List/shifted \n\
\Bool \n\
\( [ [ { index = +0, value = True } \n\
\ , { index = +1, value = True } \n\
\ , { index = +2, value = True } \n\
\ ] : List { index : Natural, value : Bool } \n\
\ , [ { index = +0, value = False } \n\
\ , { index = +1, value = False } \n\
\ ] : List { index : Natural, value : Bool } \n\
\ , [ { index = +0, value = True } \n\
\ , { index = +1, value = True } \n\
\ , { index = +2, value = True } \n\
\ , { index = +3, value = True } \n\
\ ] : List { index : Natural, value : Bool } \n\
\ ] : List (List { index : Natural, value : Bool })\n\
\) \n"
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 }" )
"./Prelude/List/shifted \n\
\Bool \n\
\[ [ { index = +0, value = True }\n\
\ , { index = +1, value = True }\n\
\ , { index = +2, value = True }\n\
\ ] \n\
\, [ { index = +0, value = False }\n\
\ , { index = +1, value = False }\n\
\ ] \n\
\, [ { index = +0, value = True }\n\
\ , { index = +1, value = True }\n\
\ , { index = +2, value = True }\n\
\ , { index = +3, value = True }\n\
\ ] \n\
\] \n"
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_shifted_1 :: TestTree
_List_shifted_1 = Test.Tasty.HUnit.testCase "Example #1" (do
@ -647,15 +644,14 @@ _List_shifted_1 = Test.Tasty.HUnit.testCase "Example #1" (do
_List_unzip_0 :: TestTree
_List_unzip_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code
"./Prelude/List/unzip \n\
\Text \n\
\Bool \n\
\( [ { _1 = \"ABC\", _2 = True } \n\
\ , { _1 = \"DEF\", _2 = False } \n\
\ , { _1 = \"GHI\", _2 = True } \n\
\ ] : List { _1 : Text, _2 : Bool }\n\
\) \n"
Util.assertNormalizesTo e "{ _1 = [ \"ABC\", \"DEF\", \"GHI\" ] : List Text, _2 = [ True, False, True ] : List Bool }" )
"./Prelude/List/unzip \n\
\Text \n\
\Bool \n\
\[ { _1 = \"ABC\", _2 = True } \n\
\, { _1 = \"DEF\", _2 = False } \n\
\, { _1 = \"GHI\", _2 = True } \n\
\] \n"
Util.assertNormalizesTo e "{ _1 = [ \"ABC\", \"DEF\", \"GHI\" ], _2 = [ True, False, True ] }" )
_List_unzip_1 :: TestTree
_List_unzip_1 = Test.Tasty.HUnit.testCase "Example #1" (do
@ -736,7 +732,7 @@ _Natural_build_1 = Test.Tasty.HUnit.testCase "Example #1" (do
_Natural_enumerate_0 :: TestTree
_Natural_enumerate_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code "./Prelude/Natural/enumerate +10"
Util.assertNormalizesTo e "[ +0, +1, +2, +3, +4, +5, +6, +7, +8, +9 ] : List Natural" )
Util.assertNormalizesTo e "[ +0, +1, +2, +3, +4, +5, +6, +7, +8, +9 ]" )
_Natural_enumerate_1 :: TestTree
_Natural_enumerate_1 = Test.Tasty.HUnit.testCase "Example #1" (do
@ -795,7 +791,7 @@ _Natural_odd_1 = Test.Tasty.HUnit.testCase "Example #1" (do
_Natural_product_0 :: TestTree
_Natural_product_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code "./Prelude/Natural/product ([ +2, +3, +5 ] : List Natural)"
e <- Util.code "./Prelude/Natural/product [ +2, +3, +5 ]"
Util.assertNormalizesTo e "+30" )
_Natural_product_1 :: TestTree
@ -815,7 +811,7 @@ _Natural_show_1 = Test.Tasty.HUnit.testCase "Example #1" (do
_Natural_sum_0 :: TestTree
_Natural_sum_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code "./Prelude/Natural/sum ([ +2, +3, +5 ] : List Natural)"
e <- Util.code "./Prelude/Natural/sum [ +2, +3, +5 ]"
Util.assertNormalizesTo e "+10" )
_Natural_sum_1 :: TestTree
@ -920,21 +916,20 @@ _Optional_fold_1 = Test.Tasty.HUnit.testCase "Example #1" (do
_Optional_head_0 :: TestTree
_Optional_head_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code
"./Prelude/Optional/head \n\
\Integer \n\
\( [ [] : Optional Integer \n\
\ , [ 1 ] : Optional Integer \n\
\ , [ 2 ] : Optional Integer \n\
\ ] : List (Optional Integer)\n\
\) \n"
"./Prelude/Optional/head \n\
\Integer \n\
\[ [] : Optional Integer\n\
\, [ 1 ] : Optional Integer\n\
\, [ 2 ] : Optional Integer\n\
\] \n"
Util.assertNormalizesTo e "[ 1 ] : Optional Integer" )
_Optional_head_1 :: TestTree
_Optional_head_1 = Test.Tasty.HUnit.testCase "Example #1" (do
e <- Util.code
"./Prelude/Optional/head \n\
\Integer \n\
\([ [] : Optional Integer, [] : Optional Integer ] : List (Optional Integer))\n"
"./Prelude/Optional/head \n\
\Integer \n\
\[ [] : Optional Integer, [] : Optional Integer ]\n"
Util.assertNormalizesTo e "[] : Optional Integer" )
_Optional_head_2 :: TestTree
@ -950,16 +945,16 @@ _Optional_last_0 = Test.Tasty.HUnit.testCase "Example #0" (do
\( [ [] : Optional Integer \n\
\ , [1] : Optional Integer \n\
\ , [2] : Optional Integer \n\
\ ] : List (Optional Integer)\n\
\ ] \n\
\) \n"
Util.assertNormalizesTo e "[ 2 ] : Optional Integer" )
_Optional_last_1 :: TestTree
_Optional_last_1 = Test.Tasty.HUnit.testCase "Example #1" (do
e <- Util.code
"./Prelude/Optional/last \n\
\Integer \n\
\([ [] : Optional Integer, [] : Optional Integer ] : List (Optional Integer))\n"
"./Prelude/Optional/last \n\
\Integer \n\
\[ [] : Optional Integer, [] : Optional Integer ]\n"
Util.assertNormalizesTo e "[] : Optional Integer" )
_Optional_last_2 :: TestTree
@ -1028,7 +1023,7 @@ _Optional_unzip_1 = Test.Tasty.HUnit.testCase "Example #1" (do
_Text_concat_0 :: TestTree
_Text_concat_0 = Test.Tasty.HUnit.testCase "Example #0" (do
e <- Util.code "./Prelude/Text/concat ([ \"ABC\", \"DEF\", \"GHI\" ] : List Text)"
e <- Util.code "./Prelude/Text/concat [ \"ABC\", \"DEF\", \"GHI\" ]"
Util.assertNormalizesTo e "\"ABCDEFGHI\"" )
_Text_concat_1 :: TestTree

22
tests/normalization/listBuildA.dhall Normal file
View File

@ -0,0 +1,22 @@
{ example0 =
List/build
Bool
( λ(list : Type)
→ λ(cons : Bool → list → list)
→ λ(nil : list)
→ cons True (cons False nil)
)
, example1 =
List/build
Bool
(λ(x : Type) → λ(x : Bool → x → x) → λ(x : x@1) → x@1 True (x@1 False x))
, example2 =
λ(id : ∀(a : Type) → a → a)
→ List/build
Bool
( λ(list : Type)
→ λ(cons : Bool → list → list)
→ λ(nil : list)
→ id list (cons True (cons False nil))
)
}

7
tests/normalization/listBuildB.dhall Normal file
View File

@ -0,0 +1,7 @@
{ example0 =
[ True, False ] : List Bool
, example1 =
[ True, False ] : List Bool
, example2 =
λ(id : ∀(a : Type) → a → a) → id (List Bool) [ True, False ]
}

18
tests/normalization/naturalBuildA.dhall Normal file
View File

@ -0,0 +1,18 @@
{ example0 =
Natural/build
( λ(natural : Type)
→ λ(succ : natural → natural)
→ λ(zero : natural)
→ succ zero
)
, example1 =
Natural/build (λ(x : Type) → λ(x : x → x) → λ(x : x@1) → x@1 x)
, example2 =
λ(id : ∀(a : Type) → a → a)
→ Natural/build
( λ(natural : Type)
→ λ(succ : natural → natural)
→ λ(zero : natural)
→ id natural (succ zero)
)
}

7
tests/normalization/naturalBuildB.dhall Normal file
View File

@ -0,0 +1,7 @@
{ example0 =
+1
, example1 =
+1
, example2 =
λ(id : ∀(a : Type) → a → a) → id Natural +1
}

10
tests/normalization/optionalBuildA.dhall
View File

@ -19,4 +19,14 @@
→ λ(nothing : optional)
→ id optional (just True)
)
, example3 =
λ(a : Type)
→ λ(x : a)
→ Optional/build
a
( λ(optional : Type)
→ λ(just : a → optional)
→ λ(nothing : optional)
→ just x
)
}

17
tests/normalization/optionalBuildB.dhall
View File

@ -1,12 +1,9 @@
{ example0 = [ +1 ] : Optional Natural
, example1 = [ 1 ] : Optional Integer
{ example0 =
[ +1 ] : Optional Natural
, example1 =
[ 1 ] : Optional Integer
, example2 =
λ(id : ∀(a : Type) → a → a)
→ Optional/build
Bool
( λ(optional : Type)
→ λ(just : Bool → optional)
→ λ(nothing : optional)
→ id optional (just True)
)
λ(id : ∀(a : Type) → a → a) → id (Optional Bool) ([ True ] : Optional Bool)
, example3 =
λ(a : Type) → λ(x : a) → [ x ] : Optional a
}

12
tests/normalization/optionalBuildFoldA.dhall
View File

@ -1,11 +1 @@
{ example0 =
λ ( f
: ∀(optional : Type)
→ ∀(just : Text → optional)
→ ∀(nothing : optional)
→ optional
)
→ Optional/fold Text (Optional/build Text f)
, example1 =
Optional/build Text (Optional/fold Text ([ "foo" ] : Optional Text))
}
Optional/build Text (Optional/fold Text ([ "foo" ] : Optional Text))

11
tests/normalization/optionalBuildFoldB.dhall
View File

@ -1,10 +1 @@
{ example0 =
λ ( f
: ∀(optional : Type)
→ ∀(just : Text → optional)
→ ∀(nothing : optional)
→ optional
)
→ f
, example1 = [ "foo" ] : Optional Text
}
[ "foo" ] : Optional Text