diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,17 @@ +1.8.0 + +* BREAKING CHANGE TO LANGUAGE: Add support for import integrity checks + * In practice, the likelihood of this breaking code in the wild is + astronomically low + * This would only break code of the form `sha256:aaa...aaa` (i.e. a + variabled named `sha256` with a type annotation for a type with a name + 64 characters long drawn from the first 6 characters of the alphabet) +* BUG FIX: Fix parsing of single quotes in single-quoted strings +* BUG FIX: Fix superfluous parentheses introduced by `dhall-format` +* New `dhall-hash` executable + * This goes hand-in-hand with the added support for integrity checks since + the executable lets you compute the current hash of an import + 1.7.0 * BREAKING CHANGE TO LANGUAGE: Update parser to match standardized grammar diff --git a/Prelude/Bool/and b/Prelude/Bool/and --- a/Prelude/Bool/and +++ b/Prelude/Bool/and @@ -5,7 +5,7 @@ Examples: ``` -./and ([True, False, True] : List Bool) = False +./and ([ True, False, True ] : List Bool) = False ./and ([] : List Bool) = True ``` diff --git a/Prelude/Bool/even b/Prelude/Bool/even --- a/Prelude/Bool/even +++ b/Prelude/Bool/even @@ -5,11 +5,11 @@ Examples: ``` -./even ([False, True, False] : List Bool) = True +./even ([ False, True, False ] : List Bool) = True -./even ([False, True] : List Bool) = False +./even ([ False, True ] : List Bool) = False -./even ([False] : List Bool) = False +./even ([ False ] : List Bool) = False ./even ([] : List Bool) = True ``` diff --git a/Prelude/Bool/odd b/Prelude/Bool/odd --- a/Prelude/Bool/odd +++ b/Prelude/Bool/odd @@ -5,11 +5,11 @@ Examples: ``` -./odd ([True, False, True] : List Bool) = False +./odd ([ True, False, True ] : List Bool) = False -./odd ([True, False] : List Bool) = True +./odd ([ True, False ] : List Bool) = True -./odd ([True] : List Bool) = True +./odd ([ True ] : List Bool) = True ./odd ([] : List Bool) = False ``` diff --git a/Prelude/Bool/or b/Prelude/Bool/or --- a/Prelude/Bool/or +++ b/Prelude/Bool/or @@ -5,7 +5,7 @@ Examples: ``` -./or ([True, False, True] : List Bool) = True +./or ([ True, False, True ] : List Bool) = True ./or ([] : List Bool) = False ``` diff --git a/Prelude/List/all b/Prelude/List/all --- a/Prelude/List/all +++ b/Prelude/List/all @@ -5,7 +5,7 @@ Examples: ``` -./all Natural Natural/even ([+2, +3, +5] : List Natural) = False +./all Natural Natural/even ([ +2, +3, +5 ] : List Natural) = False ./all Natural Natural/even ([] : List Natural) = True ``` diff --git a/Prelude/List/any b/Prelude/List/any --- a/Prelude/List/any +++ b/Prelude/List/any @@ -5,7 +5,7 @@ Examples: ``` -./any Natural Natural/even ([+2, +3, +5] : List Natural) = True +./any Natural Natural/even ([ +2, +3, +5 ] : List Natural) = True ./any Natural Natural/even ([] : List Natural) = False ``` diff --git a/Prelude/List/build b/Prelude/List/build --- a/Prelude/List/build +++ b/Prelude/List/build @@ -11,7 +11,7 @@ → λ(nil : list) → cons "ABC" (cons "DEF" nil) ) -= ["ABC", "DEF"] : List Text += [ "ABC", "DEF" ] : List Text ./build Text diff --git a/Prelude/List/concat b/Prelude/List/concat --- a/Prelude/List/concat +++ b/Prelude/List/concat @@ -10,7 +10,7 @@ , [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 ] : List Integer ./concat Integer ( [ [] : List Integer diff --git a/Prelude/List/concatMap b/Prelude/List/concatMap --- a/Prelude/List/concatMap +++ b/Prelude/List/concatMap @@ -6,7 +6,7 @@ ``` ./concatMap Natural Natural (λ(n : Natural) → [n, n]) [+2, +3, +5] -= [+2, +2, +3, +3, +5, +5] : List Natural += [ +2, +2, +3, +3, +5, +5 ] : List Natural ./concatMap Natural Natural (λ(n : Natural) → [n, n]) ([] : List Natural) = [] : List Natural diff --git a/Prelude/List/filter b/Prelude/List/filter --- a/Prelude/List/filter +++ b/Prelude/List/filter @@ -5,10 +5,10 @@ ``` ./filter Natural Natural/even ([+2, +3, +5] : List Natural) -= [+2] : List Natural += [ +2 ] : List Natural ./filter Natural Natural/odd ([+2, +3, +5] : List Natural) -= [+3, +5] : List Natural += [ +3, +5 ] : List Natural ``` -} let filter diff --git a/Prelude/List/fold b/Prelude/List/fold --- a/Prelude/List/fold +++ b/Prelude/List/fold @@ -1,7 +1,7 @@ {- `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))`, +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: @@ -9,7 +9,7 @@ ``` ./fold Natural - ([+2, +3, +5] : List Natural) + ([ +2, +3, +5 ] : List Natural) Natural (λ(x : Natural) → λ(y : Natural) → x + y) +0 @@ -18,7 +18,7 @@ λ(nil : Natural) → ./fold Natural - ([+2, +3, +5] : List Natural) + ([ +2, +3, +5 ] : List Natural) Natural (λ(x : Natural) → λ(y : Natural) → x + y) nil @@ -27,7 +27,7 @@ λ(list : Type) → λ(cons : Natural → list → list) → λ(nil : list) -→ ./fold Natural ([+2, +3, +5] : List Natural) list cons nil +→ ./fold Natural ([ +2, +3, +5 ] : List Natural) list cons nil = λ(list : Type) → λ(cons : Natural → list → list) → λ(nil : list) diff --git a/Prelude/List/generate b/Prelude/List/generate --- a/Prelude/List/generate +++ b/Prelude/List/generate @@ -5,7 +5,7 @@ Examples: ``` -./generate +5 Bool Natural/even = [True, False, True, False, True] : List Bool +./generate +5 Bool Natural/even = [ True, False, True, False, True ] : List Bool ./generate +0 Bool Natural/even = [] : List Bool ``` diff --git a/Prelude/List/head b/Prelude/List/head --- a/Prelude/List/head +++ b/Prelude/List/head @@ -4,7 +4,7 @@ Examples: ``` -./head Integer ([0, 1, 2] : List Integer) = [0] : Optional Integer +./head Integer ([ 0, 1, 2 ] : List Integer) = [ 0 ] : Optional Integer ./head Integer ([] : List Integer) = [] : Optional Integer ``` diff --git a/Prelude/List/indexed b/Prelude/List/indexed --- a/Prelude/List/indexed +++ b/Prelude/List/indexed @@ -4,7 +4,7 @@ Examples: ``` -./indexed Bool ([True, False, True] : List Bool) +./indexed Bool ([ True, False, True ] : List Bool) = [ { index = +0, value = True } , { index = +1, value = False } , { index = +2, value = True } diff --git a/Prelude/List/iterate b/Prelude/List/iterate --- a/Prelude/List/iterate +++ b/Prelude/List/iterate @@ -6,7 +6,7 @@ ``` ./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 ] : List Natural ./iterate +0 Natural (λ(x : Natural) → x * +2) +1 = [] : List Natural diff --git a/Prelude/List/last b/Prelude/List/last --- a/Prelude/List/last +++ b/Prelude/List/last @@ -4,7 +4,7 @@ Examples: ``` -./last Integer ([0, 1, 2] : List Integer) = [2] : Optional Integer +./last Integer ([ 0, 1, 2 ] : List Integer) = [ 2 ] : Optional Integer ./last Integer ([] : List Integer) = [] : Optional Integer ``` diff --git a/Prelude/List/length b/Prelude/List/length --- a/Prelude/List/length +++ b/Prelude/List/length @@ -4,7 +4,7 @@ Examples: ``` -./length Integer ([0, 1, 2] : List Integer) = +3 +./length Integer ([ 0, 1, 2 ] : List Integer) = +3 ./length Integer ([] : List Integer) = +0 ``` diff --git a/Prelude/List/map b/Prelude/List/map --- a/Prelude/List/map +++ b/Prelude/List/map @@ -4,8 +4,8 @@ Examples: ``` -./map Natural Bool Natural/even ([+2, +3, +5] : List Natural) -= [True, False, False] : List Bool +./map Natural Bool Natural/even ([ +2, +3, +5 ] : List Natural) += [ True, False, False ] : List Bool ./map Natural Bool Natural/even ([] : List Natural) = [] : List Bool diff --git a/Prelude/List/null b/Prelude/List/null --- a/Prelude/List/null +++ b/Prelude/List/null @@ -4,7 +4,7 @@ Examples: ``` -./null Integer ([0, 1, 2] : List Integer) = False +./null Integer ([ 0, 1, 2 ] : List Integer) = False ./null Integer ([] : List Integer) = True ``` diff --git a/Prelude/List/replicate b/Prelude/List/replicate --- a/Prelude/List/replicate +++ b/Prelude/List/replicate @@ -4,7 +4,7 @@ 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 ] : List Integer ./replicate +0 Integer 1 = [] : List Integer ``` diff --git a/Prelude/List/reverse b/Prelude/List/reverse --- a/Prelude/List/reverse +++ b/Prelude/List/reverse @@ -4,7 +4,7 @@ Examples: ``` -./reverse Integer ([0, 1, 2] : List Integer) = [2, 1, 0] : List Integer +./reverse Integer ([ 0, 1, 2 ] : List Integer) = [ 2, 1, 0 ] : List Integer ./reverse Integer ([] : List Integer) = [] : List Integer ``` diff --git a/Prelude/List/unzip b/Prelude/List/unzip --- a/Prelude/List/unzip +++ b/Prelude/List/unzip @@ -12,8 +12,8 @@ , { _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" ] : List Text + , _2 = [ True, False, True ] : List Bool } ./unzip Text Bool ([] : List { _1 : Text, _2 : Bool }) diff --git a/Prelude/Natural/enumerate b/Prelude/Natural/enumerate --- a/Prelude/Natural/enumerate +++ b/Prelude/Natural/enumerate @@ -5,7 +5,7 @@ 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 ] : List Natural ./enumerate +0 = [] : List Natural ``` diff --git a/Prelude/Natural/product b/Prelude/Natural/product --- a/Prelude/Natural/product +++ b/Prelude/Natural/product @@ -4,7 +4,7 @@ Examples: ``` -./product ([+2, +3, +5] : List Natural) = +30 +./product ([ +2, +3, +5 ] : List Natural) = +30 ./product ([] : List Natural) = +1 ``` diff --git a/Prelude/Natural/sum b/Prelude/Natural/sum --- a/Prelude/Natural/sum +++ b/Prelude/Natural/sum @@ -4,7 +4,7 @@ Examples: ``` -./sum ([+2, +3, +5] : List Natural) = +10 +./sum ([ +2, +3, +5 ] : List Natural) = +10 ./sum ([] : List Natural) = +0 ``` diff --git a/Prelude/Optional/all b/Prelude/Optional/all --- a/Prelude/Optional/all +++ b/Prelude/Optional/all @@ -5,7 +5,7 @@ Examples: ``` -./all Natural Natural/even ([+3] : Optional Natural) = False +./all Natural Natural/even ([ +3 ] : Optional Natural) = False ./all Natural Natural/even ([] : Optional Natural) = True ``` diff --git a/Prelude/Optional/any b/Prelude/Optional/any --- a/Prelude/Optional/any +++ b/Prelude/Optional/any @@ -5,7 +5,7 @@ Examples: ``` -./any Natural Natural/even ([+2] : Optional Natural) = True +./any Natural Natural/even ([ +2 ] : Optional Natural) = True ./any Natural Natural/even ([] : Optional Natural) = False ``` diff --git a/Prelude/Optional/build b/Prelude/Optional/build --- a/Prelude/Optional/build +++ b/Prelude/Optional/build @@ -11,7 +11,7 @@ → λ(nothing : optional) → just 1 ) -= [1] : Optional Integer += [ 1 ] : Optional Integer ./build Integer diff --git a/Prelude/Optional/concat b/Prelude/Optional/concat --- a/Prelude/Optional/concat +++ b/Prelude/Optional/concat @@ -4,10 +4,10 @@ Examples: ``` -./concat Integer ([[1] : Optional Integer] : Optional (Optional Integer)) -= [1] : Optional Integer +./concat Integer ([ [ 1 ] : Optional Integer ] : Optional (Optional Integer)) += [ 1 ] : Optional Integer -./concat Integer ([[] : Optional Integer] : Optional (Optional Integer)) +./concat Integer ([ [] : Optional Integer ] : Optional (Optional Integer)) = [] : Optional Integer ./concat Integer ([] : Optional (Optional Integer)) diff --git a/Prelude/Optional/filter b/Prelude/Optional/filter --- a/Prelude/Optional/filter +++ b/Prelude/Optional/filter @@ -4,10 +4,10 @@ Examples: ``` -./filter Natural Natural/even ([+2] : Optional Natural) -= [+2] : Optional Natural +./filter Natural Natural/even ([ +2 ] : Optional Natural) += [ +2 ] : Optional Natural -./filter Natural Natural/odd ([+2] : Optional Natural) +./filter Natural Natural/odd ([ +2 ] : Optional Natural) = [] : Optional Natural ``` -} diff --git a/Prelude/Optional/fold b/Prelude/Optional/fold --- a/Prelude/Optional/fold +++ b/Prelude/Optional/fold @@ -4,9 +4,9 @@ Examples: ``` -./fold Integer ([2] : Optional Integer) Integer (λ(x : Integer) → x) 0 = 2 +./fold Integer ([ 2 ] : Optional Integer) Integer (λ(x : Integer) → x) 0 = 2 -./fold Integer ([] : Optional Integer) Integer (λ(x : Integer) → x) 0 = 0 +./fold Integer ([] : Optional Integer) Integer (λ(x : Integer) → x) 0 = 0 ``` -} let fold diff --git a/Prelude/Optional/head b/Prelude/Optional/head --- a/Prelude/Optional/head +++ b/Prelude/Optional/head @@ -6,14 +6,17 @@ ``` ./head Integer -( [[] : Optional Integer, [1] : Optional Integer, [2] : Optional Integer] +( [ [ ] : Optional Integer + , [ 1 ] : Optional Integer + , [ 2 ] : Optional Integer + ] : List (Optional Integer) ) -= [1] : Optional Integer += [ 1 ] : Optional Integer ./head Integer -([[] : Optional Integer, [] : Optional Integer] : List (Optional Integer)) +([ [] : Optional Integer, [] : Optional Integer ] : List (Optional Integer)) = [] : Optional Integer ./head Integer ([] : List (Optional Integer)) diff --git a/Prelude/Optional/last b/Prelude/Optional/last --- a/Prelude/Optional/last +++ b/Prelude/Optional/last @@ -6,14 +6,16 @@ ``` ./last Integer -( [[] : Optional Integer, [1] : Optional Integer, [2] : Optional Integer] - : List (Optional Integer) +( [ [ ] : Optional Integer + , [ 1 ] : Optional Integer + , [ 2 ] : Optional Integer + ] : List (Optional Integer) ) -= [2] : Optional Integer += [ 2 ] : Optional Integer ./last Integer -([[] : Optional Integer, [] : Optional Integer] : List (Optional Integer)) +([ [] : Optional Integer, [] : Optional Integer ] : List (Optional Integer)) = [] : Optional Integer ./last Integer ([] : List (Optional Integer)) diff --git a/Prelude/Optional/length b/Prelude/Optional/length --- a/Prelude/Optional/length +++ b/Prelude/Optional/length @@ -4,7 +4,7 @@ Examples: ``` -./length Integer ([2] : Optional Integer) = +1 +./length Integer ([ 2 ] : Optional Integer) = +1 ./length Integer ([] : Optional Integer) = +0 ``` diff --git a/Prelude/Optional/map b/Prelude/Optional/map --- a/Prelude/Optional/map +++ b/Prelude/Optional/map @@ -4,8 +4,8 @@ Examples: ``` -./map Natural Bool Natural/even ([+3] : Optional Natural) -= [False] : Optional Bool +./map Natural Bool Natural/even ([ +3 ] : Optional Natural) += [ False ] : Optional Bool ./map Natural Bool Natural/even ([] : Optional Natural) = [] : Optional Bool diff --git a/Prelude/Optional/null b/Prelude/Optional/null --- a/Prelude/Optional/null +++ b/Prelude/Optional/null @@ -4,7 +4,7 @@ Examples: ``` -./null Integer ([2] : Optional Integer) = False +./null Integer ([ 2 ] : Optional Integer) = False ./null Integer ([] : Optional Integer) = True ``` diff --git a/Prelude/Optional/toList b/Prelude/Optional/toList --- a/Prelude/Optional/toList +++ b/Prelude/Optional/toList @@ -4,7 +4,7 @@ Examples: ``` -./toList Integer ([1] : Optional Integer) = [1] +./toList Integer ([ 1 ] : Optional Integer) = [ 1 ] ./toList Integer ([] : Optional Integer) = [] : List Integer ``` diff --git a/Prelude/Optional/unzip b/Prelude/Optional/unzip --- a/Prelude/Optional/unzip +++ b/Prelude/Optional/unzip @@ -7,8 +7,8 @@ ./unzip Text Bool -([{ _1 = "ABC", _2 = True }] : Optional { _1 : Text, _2 : Bool }) -= { _1 = ["ABC"] : Optional Text, _2 = [True] : Optional 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 } diff --git a/Prelude/Text/concat b/Prelude/Text/concat --- a/Prelude/Text/concat +++ b/Prelude/Text/concat @@ -4,7 +4,7 @@ Examples: ``` -./concat (["ABC", "DEF", "GHI"] : List Text) = "ABCDEFGHI" +./concat ([ "ABC", "DEF", "GHI" ] : List Text) = "ABCDEFGHI" ./concat ([] : List Text) = "" ``` diff --git a/Prelude/Text/concatMap b/Prelude/Text/concatMap --- a/Prelude/Text/concatMap +++ b/Prelude/Text/concatMap @@ -4,7 +4,7 @@ Examples: ``` -./concatMap Integer (λ(n : Integer) → "${Integer/show n} ") [0, 1, 2] +./concatMap Integer (λ(n : Integer) → "${Integer/show n} ") [ 0, 1, 2 ] = "0 1 2 " ./concatMap Integer (λ(n : Integer) → "${Integer/show n} ") ([] : List Integer) diff --git a/Prelude/Text/concatMapSep b/Prelude/Text/concatMapSep --- a/Prelude/Text/concatMapSep +++ b/Prelude/Text/concatMapSep @@ -5,7 +5,7 @@ Examples: ``` -./concatMapSep ", " Integer Integer/show [0, 1, 2] = "0, 1, 2" +./concatMapSep ", " Integer Integer/show [ 0, 1, 2 ] = "0, 1, 2" ./concatMapSep ", " Integer Integer/show ([] : List Integer) = "" ``` diff --git a/Prelude/Text/concatSep b/Prelude/Text/concatSep --- a/Prelude/Text/concatSep +++ b/Prelude/Text/concatSep @@ -4,7 +4,7 @@ Examples: ``` -./concatSep ", " ["ABC", "DEF", "GHI"] = "ABC, DEF, GHI" +./concatSep ", " [ "ABC", "DEF", "GHI" ] = "ABC, DEF, GHI" ./concatSep ", " ([] : List Text) = "" ``` diff --git a/dhall-hash/Main.hs b/dhall-hash/Main.hs new file mode 100644 --- /dev/null +++ b/dhall-hash/Main.hs @@ -0,0 +1,84 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeOperators #-} + +module Main where + +import Control.Exception (SomeException) +import Control.Monad (when) +import Data.Monoid (mempty) +import Data.Version (showVersion) +import Dhall.Core (pretty, normalize) +import Dhall.Import (Imported(..), hashExpressionToCode, load) +import Dhall.Parser (Src, exprFromText) +import Dhall.TypeCheck (DetailedTypeError(..), TypeError) +import Options.Generic (Generic, ParseRecord, type ()(..)) +import System.IO (stderr) +import System.Exit (exitFailure, exitSuccess) +import Text.Trifecta.Delta (Delta(..)) + +import qualified Paths_dhall as Meta + +import qualified Control.Exception +import qualified Data.Text.Lazy.IO +import qualified Dhall.TypeCheck +import qualified Options.Generic +import qualified System.IO + +data Options = Options + { explain :: Bool "Explain error messages in more detail" + , version :: Bool "Display version and exit" + } deriving (Generic) + +instance ParseRecord Options + +main :: IO () +main = do + options <- Options.Generic.getRecord "Compiler for the Dhall language" + when (unHelpful (version options)) $ do + putStrLn (showVersion Meta.version) + exitSuccess + let handle = + Control.Exception.handle handler2 + . Control.Exception.handle handler1 + . Control.Exception.handle handler0 + where + handler0 e = do + let _ = e :: TypeError Src + System.IO.hPutStrLn stderr "" + if unHelpful (explain options) + then Control.Exception.throwIO (DetailedTypeError e) + else do + Data.Text.Lazy.IO.hPutStrLn stderr "\ESC[2mUse \"dhall --explain\" for detailed errors\ESC[0m" + Control.Exception.throwIO e + + handler1 (Imported ps e) = do + let _ = e :: TypeError Src + System.IO.hPutStrLn stderr "" + if unHelpful (explain options) + then Control.Exception.throwIO (Imported ps (DetailedTypeError e)) + else do + Data.Text.Lazy.IO.hPutStrLn stderr "\ESC[2mUse \"dhall --explain\" for detailed errors\ESC[0m" + Control.Exception.throwIO (Imported ps e) + + handler2 e = do + let _ = e :: SomeException + System.IO.hPrint stderr e + System.Exit.exitFailure + + handle (do + inText <- Data.Text.Lazy.IO.getContents + + expr <- case exprFromText (Directed "(stdin)" 0 0 0 0) inText of + Left err -> Control.Exception.throwIO err + Right expr -> return expr + + expr' <- load expr + + _ <- case Dhall.TypeCheck.typeOf expr' of + Left err -> Control.Exception.throwIO err + Right _ -> return () + + Data.Text.Lazy.IO.putStrLn (hashExpressionToCode (normalize expr')) ) diff --git a/dhall.cabal b/dhall.cabal --- a/dhall.cabal +++ b/dhall.cabal @@ -1,5 +1,5 @@ Name: dhall -Version: 1.7.0 +Version: 1.8.0 Cabal-Version: >=1.8.0.2 Build-Type: Simple Tested-With: GHC == 8.0.1 @@ -93,11 +93,13 @@ Build-Depends: base >= 4.9.0.0 && < 5 , ansi-wl-pprint < 0.7 , + base16-bytestring < 0.2 , bytestring < 0.11, case-insensitive < 1.3 , charset < 0.4 , containers >= 0.5.0.0 && < 0.6 , contravariant < 1.5 , + cryptohash < 0.12, exceptions >= 0.8.3 && < 0.9 , http-client >= 0.4.30 && < 0.6 , http-client-tls >= 0.2.0 && < 0.4 , @@ -150,6 +152,16 @@ Other-Modules: Paths_dhall +Executable dhall-hash + Hs-Source-Dirs: dhall-hash + Main-Is: Main.hs + Build-Depends: + base >= 4 && < 5 , + dhall , + optparse-generic >= 1.1.1 && < 1.3, + trifecta >= 1.6 && < 1.8, + text >= 0.11.1.0 && < 1.3 + Test-Suite test Type: exitcode-stdio-1.0 Hs-Source-Dirs: tests @@ -166,7 +178,7 @@ base >= 4 && < 5 , containers >= 0.5.0.0 && < 0.6 , dhall , - tasty >= 0.11.2 && < 0.12, + tasty >= 0.11.2 && < 0.13, tasty-hunit >= 0.9.2 && < 0.10, text >= 0.11.1.0 && < 1.3 , vector >= 0.11.0.0 && < 0.13 diff --git a/src/Dhall/Core.hs b/src/Dhall/Core.hs --- a/src/Dhall/Core.hs +++ b/src/Dhall/Core.hs @@ -19,6 +19,7 @@ Const(..) , HasHome(..) , PathType(..) + , PathHashed(..) , PathMode(..) , Path(..) , Var(..) @@ -63,6 +64,9 @@ import Prelude hiding (FilePath, succ) import qualified Control.Monad +import qualified Data.ByteString +import qualified Data.ByteString.Char8 +import qualified Data.ByteString.Base16 import qualified Data.Char import qualified Data.HashSet import qualified Data.List @@ -71,7 +75,8 @@ import qualified Data.Text import qualified Data.Text.Lazy as Text import qualified Data.Text.Lazy.Builder as Builder -import qualified Data.Text.Prettyprint.Doc as Pretty +import qualified Data.Text.Prettyprint.Doc as Pretty +import qualified Data.Text.Prettyprint.Doc.Render.Text as Pretty import qualified Data.Vector import qualified Data.Vector.Mutable import qualified Filesystem.Path.CurrentOS as Filesystem @@ -105,7 +110,7 @@ data PathType = File HasHome FilePath -- ^ Local path - | URL Text (Maybe PathType) + | URL Text (Maybe PathHashed) -- ^ URL of emote resource and optional headers stored in a path | Env Text -- ^ Environment variable @@ -132,14 +137,27 @@ -- | How to interpret the path's contents (i.e. as Dhall code or raw text) data PathMode = Code | RawText deriving (Eq, Ord, Show) +data PathHashed = PathHashed + { hash :: Maybe Data.ByteString.ByteString + , pathType :: PathType + } deriving (Eq, Ord, Show) + +instance Buildable PathHashed where + build (PathHashed Nothing p) = build p + build (PathHashed (Just h) p) = build p <> "sha256:" <> build string <> " " + where + bytes = Data.ByteString.Base16.encode h + + string = Data.ByteString.Char8.unpack bytes + -- | Path to an external resource data Path = Path - { pathType :: PathType - , pathMode :: PathMode + { pathHashed :: PathHashed + , pathMode :: PathMode } deriving (Eq, Ord, Show) instance Buildable Path where - build (Path {..}) = build pathType <> suffix + build (Path {..}) = build pathHashed <> suffix where suffix = case pathMode of RawText -> "as Text" @@ -586,7 +604,10 @@ docs (Annot a b) = prettyExprB a : docs b docs (Note _ b) = docs b docs b = [ prettyExprB b ] -prettyExprA a0 = prettyExprB a0 +prettyExprA (Note _ a) = + prettyExprA a +prettyExprA a0 = + prettyExprB a0 prettyExprB :: Pretty a => Expr s a -> Doc ann prettyExprB a0@(Lam _ _ _) = arrows (fmap duplicate (docs a0)) @@ -762,6 +783,8 @@ docs (BoolOr a b) = prettyExprC1 a : docs b docs (Note _ b) = docs b docs b = [ prettyExprC1 b ] +prettyExprC0 (Note _ a) = + prettyExprC0 a prettyExprC0 a0 = prettyExprC1 a0 @@ -772,6 +795,8 @@ docs (TextAppend a b) = prettyExprC2 a : docs b docs (Note _ b) = docs b docs b = [ prettyExprC2 b ] +prettyExprC1 (Note _ a) = + prettyExprC1 a prettyExprC1 a0 = prettyExprC2 a0 @@ -782,6 +807,8 @@ docs (NaturalPlus a b) = prettyExprC3 a : docs b docs (Note _ b) = docs b docs b = [ prettyExprC3 b ] +prettyExprC2 (Note _ a) = + prettyExprC2 a prettyExprC2 a0 = prettyExprC3 a0 @@ -792,6 +819,8 @@ docs (ListAppend a b) = prettyExprC4 a : docs b docs (Note _ b) = docs b docs b = [ prettyExprC4 b ] +prettyExprC3 (Note _ a) = + prettyExprC3 a prettyExprC3 a0 = prettyExprC4 a0 @@ -802,6 +831,8 @@ docs (BoolAnd a b) = prettyExprC5 a : docs b docs (Note _ b) = docs b docs b = [ prettyExprC5 b ] +prettyExprC4 (Note _ a) = + prettyExprC4 a prettyExprC4 a0 = prettyExprC5 a0 @@ -812,6 +843,8 @@ docs (Combine a b) = prettyExprC6 a : docs b docs (Note _ b) = docs b docs b = [ prettyExprC6 b ] +prettyExprC5 (Note _ a) = + prettyExprC5 a prettyExprC5 a0 = prettyExprC6 a0 @@ -822,6 +855,8 @@ docs (Prefer a b) = prettyExprC7 a : docs b docs (Note _ b) = docs b docs b = [ prettyExprC7 b ] +prettyExprC6 (Note _ a) = + prettyExprC6 a prettyExprC6 a0 = prettyExprC7 a0 @@ -832,6 +867,8 @@ docs (NaturalTimes a b) = prettyExprC8 a : docs b docs (Note _ b) = docs b docs b = [ prettyExprC8 b ] +prettyExprC7 (Note _ a) = + prettyExprC7 a prettyExprC7 a0 = prettyExprC8 a0 @@ -842,6 +879,8 @@ docs (BoolEQ a b) = prettyExprC9 a : docs b docs (Note _ b) = docs b docs b = [ prettyExprC9 b ] +prettyExprC8 (Note _ a) = + prettyExprC8 a prettyExprC8 a0 = prettyExprC9 a0 @@ -852,6 +891,8 @@ docs (BoolNE a b) = prettyExprD a : docs b docs (Note _ b) = docs b docs b = [ prettyExprD b ] +prettyExprC9 (Note _ a) = + prettyExprC9 a prettyExprC9 a0 = prettyExprD a0 @@ -1010,8 +1051,10 @@ adapt = prettyKeyValue ":" keyLength -- | Pretty-print a value -pretty :: Buildable a => a -> Text -pretty = Builder.toLazyText . build +pretty :: Pretty a => a -> Text +pretty = Pretty.renderLazy . Pretty.layoutPretty options . Pretty.pretty + where + options = Pretty.LayoutOptions { Pretty.layoutPageWidth = Pretty.Unbounded } -- | Builder corresponding to the @label@ token in "Dhall.Parser" buildLabel :: Text -> Builder diff --git a/src/Dhall/Import.hs b/src/Dhall/Import.hs --- a/src/Dhall/Import.hs +++ b/src/Dhall/Import.hs @@ -104,6 +104,8 @@ exprFromPath , load , loadWith + , hashExpression + , hashExpressionToCode , Cycle(..) , ReferentiallyOpaque(..) , Imported(..) @@ -134,7 +136,13 @@ import Data.Typeable (Typeable) import Filesystem.Path ((), FilePath) import Dhall.Core - (Expr(..), HasHome(..), PathMode(..), PathType(..), Path(..)) + ( Expr(..) + , HasHome(..) + , PathHashed(..) + , PathMode(..) + , PathType(..) + , Path(..) + ) import Dhall.Parser (Parser(..), ParseError(..), Src(..)) import Dhall.TypeCheck (X(..)) #if MIN_VERSION_http_client(0,5,0) @@ -148,7 +156,10 @@ import Text.Trifecta.Delta (Delta(..)) import qualified Control.Monad.Trans.State.Strict as State +import qualified Crypto.Hash.SHA256 import qualified Data.ByteString +import qualified Data.ByteString.Base16 +import qualified Data.ByteString.Char8 import qualified Data.ByteString.Lazy import qualified Data.CaseInsensitive import qualified Data.List as List @@ -157,6 +168,7 @@ 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 @@ -376,7 +388,7 @@ go currPath (Env _ :_ ) = File Homeless (clean currPath) go currPath (URL url0 headers:rest ) = combine prefix suffix where - headers' = fmap (\h -> canonicalize (h:rest)) headers + headers' = fmap (onPathType (\h -> canonicalize (h:rest))) headers prefix = parentURL (removeAtFromURL url0) @@ -409,19 +421,29 @@ file' = Filesystem.parent (removeAtFromFile file) currPath canonicalize (URL path headers:rest) = URL path headers' where - headers' = fmap (\h -> canonicalize (h:rest)) headers + headers' = fmap (onPathType (\h -> canonicalize (h:rest))) headers canonicalize (Env env :_ ) = Env env +onPathType :: (PathType -> PathType) -> PathHashed -> PathHashed +onPathType f (PathHashed a b) = PathHashed a (f b) + canonicalizePath :: [Path] -> Path canonicalizePath [] = Path - { pathMode = Code - , pathType = canonicalize [] + { pathMode = Code + , pathHashed = PathHashed + { hash = Nothing + , pathType = canonicalize [] + } } canonicalizePath (path:paths) = Path - { pathMode = pathMode path - , pathType = canonicalize (map pathType (path:paths)) + { pathMode = pathMode path + , pathHashed = (pathHashed path) + { hash = hash (pathHashed path) + , pathType = + canonicalize (map (pathType . pathHashed) (path:paths)) + } } parentURL :: Text -> Text @@ -503,6 +525,53 @@ instance Exception InternalError +-- | Exception thrown when an integrity check fails +data HashMismatch = HashMismatch + { expectedHash :: Data.ByteString.ByteString + , actualHash :: Data.ByteString.ByteString + } deriving (Typeable) + +instance Exception HashMismatch + +instance Show HashMismatch where + show (HashMismatch {..}) = + "\n" + <> "\ESC[1;31mError\ESC[0m: Import integrity check failed\n" + <> "\n" + <> "Expected hash:\n" + <> "\n" + <> "↳ " <> toString expectedHash <> "\n" + <> "\n" + <> "Actual hash:\n" + <> "\n" + <> "↳ " <> toString actualHash <> "\n" + where + toString = + Data.ByteString.Char8.unpack . Data.ByteString.Base16.encode + +parseFromFileEx + :: Text.Trifecta.Parser a + -> FilePath + -> IO (Text.Trifecta.Result a) +parseFromFileEx parser path = do + text <- Data.Text.Lazy.IO.readFile stringPath + + let lazyBytes = Data.Text.Lazy.Encoding.encodeUtf8 text + + let strictBytes = Data.ByteString.Lazy.toStrict lazyBytes + + let delta = Directed bytesPath 0 0 0 0 + + return (Text.Trifecta.parseByteString parser delta strictBytes) + where + stringPath = Filesystem.Path.CurrentOS.encodeString path + + textPath = case Filesystem.Path.CurrentOS.toText path of + Left text -> text + Right text -> text + + bytesPath = Data.Text.Encoding.encodeUtf8 textPath + -- | Parse an expression from a `Path` containing a Dhall program exprFromPath :: Manager -> Path -> IO (Expr Src Path) exprFromPath m (Path {..}) = case pathType of @@ -521,23 +590,17 @@ then return () else Control.Exception.throwIO MissingFile - let string = Filesystem.Path.CurrentOS.encodeString path - -- Unfortunately, GHC throws an `InappropriateType` exception -- when trying to read a directory, but does not export the -- exception, so I must resort to a more heavy-handed `catch` let handler :: IOException -> IO (Result (Expr Src Path)) handler e = do - let string' = - Filesystem.Path.CurrentOS.encodeString - (path "@") - -- If the fallback fails, reuse the original exception -- to avoid user confusion - Text.Trifecta.parseFromFileEx parser string' + parseFromFileEx parser (path "@") `onException` throwIO e - x <- Text.Trifecta.parseFromFileEx parser string `catch` handler + x <- parseFromFileEx parser path `catch` handler case x of Failure errInfo -> do throwIO (ParseError (Text.Trifecta._errDoc errInfo)) @@ -654,6 +717,8 @@ RawText -> return (TextLit (build str)) Nothing -> throwIO (MissingEnvironmentVariable env) where + PathHashed {..} = pathHashed + parser = unParser (do Text.Parser.Token.whiteSpace r <- Dhall.Parser.expr @@ -691,15 +756,15 @@ loadStaticWith from_path ctx path = do paths <- zoom stack State.get - let local (Path (URL url _) _) = + let local (Path (PathHashed _ (URL url _)) _) = case HTTP.parseUrlThrow (Text.unpack url) of Nothing -> False Just request -> case HTTP.host request of "127.0.0.1" -> True "localhost" -> True _ -> False - local (Path (File _ _ ) _) = True - local (Path (Env _ ) _) = True + local (Path (PathHashed _ (File _ _ )) _) = True + local (Path (PathHashed _ (Env _ )) _) = True let parent = canonicalizePath paths let here = canonicalizePath (path:paths) @@ -731,10 +796,11 @@ return expr'' return (expr'', False) - -- Type-check expressions here for two separate reasons: + -- Type-check expressions here for three separate reasons: -- -- * to verify that they are closed -- * to catch type errors as early in the import process as possible + -- * to avoid normalizing ill-typed expressions that need to be hashed -- -- There is no need to check expressions that have been cached, since they -- have already been checked @@ -744,6 +810,15 @@ Left err -> throwM (Imported (path:paths) err) Right _ -> return () + case hash (pathHashed path) of + Nothing -> do + return () + Just expectedHash -> do + let actualHash = hashExpression expr + if expectedHash == actualHash + then return () + else throwM (HashMismatch {..}) + return expr evalStatus :: (Traversable f, Monad m, Monad f) => @@ -755,3 +830,29 @@ -- | Resolve all imports within an expression load :: Expr Src Path -> IO (Expr Src X) load = evalStatus (loadStaticIO Dhall.Context.empty) + +-- | Hash a fully resolved expression +hashExpression :: Expr s X -> Data.ByteString.ByteString +hashExpression expr = Crypto.Hash.SHA256.hashlazy actualBytes + where + text = Dhall.Core.pretty (Dhall.Core.normalize expr) + actualBytes = Data.Text.Lazy.Encoding.encodeUtf8 text + +{-| Convenience utility to hash a fully resolved expression and return the + base-16 encoded hash with the @sha256:@ prefix + + In other words, the output of this function can be pasted into Dhall + source code to add an integrity check to an import +-} +hashExpressionToCode :: Expr s X -> Text +hashExpressionToCode expr = "sha256:" <> lazyText + where + bytes = hashExpression expr + + bytes16 = Data.ByteString.Base16.encode bytes + + -- Notes that `decodeUtf8` is partial, but the base16-encoded bytestring + -- should always successfully decode + text = Data.Text.Encoding.decodeUtf8 bytes16 + + lazyText = Text.fromStrict text diff --git a/src/Dhall/Parser.hs b/src/Dhall/Parser.hs --- a/src/Dhall/Parser.hs +++ b/src/Dhall/Parser.hs @@ -43,6 +43,7 @@ import Text.Trifecta.Delta (Delta) import qualified Control.Monad +import qualified Data.ByteString.Base16.Lazy import qualified Data.Char import qualified Data.HashSet import qualified Data.Map @@ -448,9 +449,7 @@ b <- singleQuoteContinue embedded return (textAppend a b) where - predicate c = - ('\x20' <= c && c <= '\x26' ) - || ('\x28' <= c && c <= '\x10FFFF') + predicate c = '\x20' <= c && c <= '\x10FFFF' endOfLine = do a <- fmap TextLit "\n" <|> fmap TextLit "\r\n" @@ -933,7 +932,7 @@ whitespace b <- optional (do _using - pathType_ ) + pathHashed_ ) return (URL (Data.Text.Lazy.Builder.toLazyText a) b) env :: Parser PathType @@ -1495,10 +1494,27 @@ pathType_ :: Parser PathType pathType_ = choice [ file, http, env ] +pathHashed_ :: Parser PathHashed +pathHashed_ = do + pathType <- pathType_ + hash <- optional pathHash_ + return (PathHashed {..}) + where + pathHash_ = do + _ <- Text.Parser.Char.text "sha256:" + builder <- count 64 (satisfy hexdig "hex digit") + whitespace + let lazyText = Data.Text.Lazy.Builder.toLazyText builder + let lazyBytes = Data.Text.Lazy.Encoding.encodeUtf8 lazyText + let (hash, suffix) = Data.ByteString.Base16.Lazy.decode lazyBytes + if Data.ByteString.Lazy.null suffix + then return (Data.ByteString.Lazy.toStrict hash) + else fail "Invalid sha256 hash" + import_ :: Parser Path import_ = (do - pathType <- pathType_ - pathMode <- alternative <|> pure Code + pathHashed <- pathHashed_ + pathMode <- alternative <|> pure Code return (Path {..}) ) "import" where alternative = do diff --git a/src/Dhall/Tutorial.hs b/src/Dhall/Tutorial.hs --- a/src/Dhall/Tutorial.hs +++ b/src/Dhall/Tutorial.hs @@ -50,6 +50,9 @@ -- * Headers -- $headers + -- * Import integrity + -- $integrity + -- * Raw text -- $rawText @@ -1387,6 +1390,104 @@ -- ... and @http:\/\/example.com@ contains a relative import of @./foo@ then -- Dhall will import @http:\/\/example.com/foo@ using the same @./headers@ file. +-- $integrity +-- +-- Sometimes you want to use share code while still ensuring that the imported +-- value never changes and can't be corrupted by a malicious attacker. Dhall +-- provides built-in support for hashing imported values to verify that their +-- value never changes +-- +-- For example, suppose you save the following two files: +-- +-- > $ cat ./foo +-- > ./bar sha256:6b86b273ff34fce19d6b804eff5a3f5747ada4eaa22f1d49c01e52ddb7875b4b +-- +-- > $ cat ./bar +-- > ./baz +-- +-- > $ cat ./baz +-- > 1 +-- +-- The first file named @./foo@ contains an example of an integrity check. You +-- can add @sha256:XXX@ after any import (such as after @./bar@), where @XXX@ is +-- an expected 64-character @sha256@ hash of the Dhall value. To be precise, +-- the hash represents a @sha256@ hash of the UTF-8 encoding of a canonical text +-- representation of the fully resolved and normalized abstract syntax tree of +-- the imported expression. +-- +-- Dhall will verify that the expected hash matches the actual hash of the +-- imported Dhall value and reject the import if there is a hash mismatch: +-- +-- > $ dhall <<< './foo' +-- > Integer +-- > +-- > 1 +-- +-- This implies that the hash only changes if the Dhall value changes. For +-- example, if you add a comment to the @./bar@ file: +-- +-- > $ cat ./bar +-- > -- This comment does not change the hash +-- > ./baz +-- +-- ... then @./foo@ will still successfully import @./bar@ because the hash +-- only depends on the normalized value and does not depend on meaningless +-- changes to whitespace or comments: +-- +-- > $ dhall <<< './foo' # This still succeeds +-- > Integer +-- > +-- > 1 +-- +-- You can compute the Hash for any import by using the @dhall-hash@ utility +-- installed by this package. For example: +-- +-- > dhall-hash <<< './bar' +-- > sha256:6b86b273ff34fce19d6b804eff5a3f5747ada4eaa22f1d49c01e52ddb7875b4b +-- +-- Then you can paste that output into your code after the import +-- +-- Now suppose that you you change the value of the @./baz@ file: +-- +-- > $ cat ./baz +-- > 2 +-- +-- ... then the @./foo@ file will fail to import @./bar@, even though the +-- text of the @./bar@ file technically never changed: +-- +-- > dhall <<< './foo' +-- > +-- > Error: Import integrity check failed +-- > +-- > Expected hash: +-- > +-- > ↳ 6b86b273ff34fce19d6b804eff5a3f5747ada4eaa22f1d49c01e52ddb7875b4b +-- > +-- > Actual hash: +-- > +-- > ↳ d4735e3a265e16eee03f59718b9b5d03019c07d8b6c51f90da3a666eec13ab35 +-- +-- This is because the @./bar@ file now represents a new value (@2@ instead of +-- @1@), even though the text of the @./bar@ is still the same. Since the value +-- changed the hash must change as well. However, we could change @./baz@ to: +-- +-- > $ cat baz +-- > if True then 1 else 2 +-- +-- ... and the import would succeed again because the final result is still @1@. +-- +-- The integrity hash ensures that your import's final meaning can never change, +-- so an attacker can never compromise an imported value protected by a hash +-- unless they can break SHA-256 encryption. The hash not only protects the +-- file that you immediately import, but also protects every transitive import +-- as well. +-- +-- You can also safely refactor your imported dependencies knowing that the +-- refactor will not change your hash so long as your refactor is +-- behavior-preserving. This provides an easy way to detect refactoring errors +-- that you might accidentally introduce. The hash not only protects you +-- from attackers, but also protects against human error, too! + -- $rawText -- -- Sometimes you want to import the contents of a raw text file as a Dhall @@ -2583,3 +2684,25 @@ -- the above polymorphic function then you'd get the unexpected behavior where -- a list literal is a function if the list has 0 elements but not a function -- otherwise. +-- +-- * Does Dhall support type synonyms like Haskell? +-- +-- No. For example, the following expression will not type-check: +-- +-- > let MyType = Integer in 1 : MyType +-- +-- Haskell can support type synonyms because Haskell does not allow type-level +-- functions like Dhall does. Dhall's support for type-level computation means +-- that type synonyms cannot be safely substituted until after the type-checking +-- phase, otherwise type-checking might infinitely loop +-- +-- You can work around this limitation using Dhall's import system by saving the +-- type synonym to a path and importing that path, like this: +-- +-- > cat ./MyType +-- > Integer +-- +-- > 1 : ./MyType -- This will type-check +-- +-- This is because import resolution precedes type-checking and does not run the +-- risk of causing the type-checker to diverge diff --git a/src/Dhall/TypeCheck.hs b/src/Dhall/TypeCheck.hs --- a/src/Dhall/TypeCheck.hs +++ b/src/Dhall/TypeCheck.hs @@ -3152,7 +3152,7 @@ } deriving (Typeable) instance Buildable s => Show (TypeError s) where - show = Text.unpack . Dhall.Core.pretty + show = Text.unpack . Builder.toLazyText . build instance (Buildable s, Typeable s) => Exception (TypeError s) @@ -3186,7 +3186,7 @@ deriving (Typeable) instance Buildable s => Show (DetailedTypeError s) where - show = Text.unpack . Dhall.Core.pretty + show = Text.unpack . Builder.toLazyText . build instance (Buildable s, Typeable s) => Exception (DetailedTypeError s) diff --git a/tests/Examples.hs b/tests/Examples.hs --- a/tests/Examples.hs +++ b/tests/Examples.hs @@ -275,7 +275,7 @@ _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 ] : List Bool)" Util.assertNormalizesTo e "False" ) _Bool_and_1 :: TestTree @@ -297,17 +297,17 @@ _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 ] : List Bool)" 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 ] : List Bool)" 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 ] : List Bool)" Util.assertNormalizesTo e "False" ) _Bool_even_3 :: TestTree @@ -337,17 +337,17 @@ _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 ] : List Bool)" 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 ] : List Bool)" 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 ] : List Bool)" Util.assertNormalizesTo e "True" ) _Bool_odd_3 :: TestTree @@ -357,7 +357,7 @@ _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 ] : List Bool)" Util.assertNormalizesTo e "True" ) _Bool_or_1 :: TestTree @@ -397,7 +397,7 @@ _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 ] : List Natural)" Util.assertNormalizesTo e "False" ) _List_all_1 :: TestTree @@ -407,7 +407,7 @@ _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 ] : List Natural)" Util.assertNormalizesTo e "True" ) _List_any_1 :: TestTree @@ -425,7 +425,7 @@ \→ λ(nil : list) \n\ \→ cons \"ABC\" (cons \"DEF\" nil)\n\ \) \n" - Util.assertNormalizesTo e "[\"ABC\", \"DEF\"] : List Text" ) + Util.assertNormalizesTo e "[ \"ABC\", \"DEF\" ] : List Text" ) _List_build_1 :: TestTree _List_build_1 = Test.Tasty.HUnit.testCase "Example #1" (do @@ -448,7 +448,7 @@ \ , [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" ) + 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 @@ -465,7 +465,7 @@ _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 Natural" ) _List_concatMap_1 :: TestTree _List_concatMap_1 = Test.Tasty.HUnit.testCase "Example #1" (do @@ -477,19 +477,19 @@ _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" ) + Util.assertNormalizesTo e "[ +2 ] : List Natural" ) _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" ) + Util.assertNormalizesTo e "[ +3, +5 ] : List Natural" ) _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 ] : List Natural) \n\ \Natural \n\ \(λ(x : Natural) → λ(y : Natural) → x + y)\n\ \+0 \n" @@ -501,7 +501,7 @@ " λ(nil : Natural) \n\ \→ ./Prelude/List/fold \n\ \ Natural \n\ - \ ([+2, +3, +5] : List Natural) \n\ + \ ([ +2, +3, +5 ] : List Natural) \n\ \ Natural \n\ \ (λ(x : Natural) → λ(y : Natural) → x + y)\n\ \ nil \n" @@ -513,13 +513,13 @@ " λ(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 Natural) 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 Bool" ) _List_generate_1 :: TestTree _List_generate_1 = Test.Tasty.HUnit.testCase "Example #1" (do @@ -528,8 +528,8 @@ _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)" - Util.assertNormalizesTo e "[0] : Optional Integer" ) + e <- Util.code "./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 @@ -538,8 +538,8 @@ _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)" - Util.assertNormalizesTo e "[{ index = +0, value = True }, { index = +1, value = False }, { index = +2, value = True }] : List { index : Natural, value : Bool }" ) + e <- Util.code "./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 @@ -549,7 +549,7 @@ _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 Natural" ) _List_iterate_1 :: TestTree _List_iterate_1 = Test.Tasty.HUnit.testCase "Example #1" (do @@ -558,8 +558,8 @@ _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)" - Util.assertNormalizesTo e "[2] : Optional Integer" ) + e <- Util.code "./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 @@ -568,7 +568,7 @@ _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 ] : List Integer)" Util.assertNormalizesTo e "+3" ) _List_length_1 :: TestTree @@ -579,8 +579,8 @@ _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 ] : List Natural)" + Util.assertNormalizesTo e "[ True, False, False ] : List Bool" ) _List_map_1 :: TestTree _List_map_1 = Test.Tasty.HUnit.testCase "Example #1" (do @@ -589,7 +589,7 @@ _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 ] : List Integer)" Util.assertNormalizesTo e "False" ) _List_null_1 :: TestTree @@ -600,7 +600,7 @@ _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 Integer" ) _List_replicate_1 :: TestTree _List_replicate_1 = Test.Tasty.HUnit.testCase "Example #1" (do @@ -610,7 +610,7 @@ _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)" - Util.assertNormalizesTo e "[2, 1, 0] : List Integer" ) + Util.assertNormalizesTo e "[ 2, 1, 0 ] : List Integer" ) _List_reverse_1 :: TestTree _List_reverse_1 = Test.Tasty.HUnit.testCase "Example #1" (do @@ -636,7 +636,7 @@ \ ] : 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 }" ) + 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 @@ -655,7 +655,7 @@ \ , { _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 }" ) + 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 @@ -736,7 +736,7 @@ _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 ] : List Natural" ) _Natural_enumerate_1 :: TestTree _Natural_enumerate_1 = Test.Tasty.HUnit.testCase "Example #1" (do @@ -795,7 +795,7 @@ _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 ] : List Natural)" Util.assertNormalizesTo e "+30" ) _Natural_product_1 :: TestTree @@ -815,7 +815,7 @@ _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 ] : List Natural)" Util.assertNormalizesTo e "+10" ) _Natural_sum_1 :: TestTree @@ -835,7 +835,7 @@ _Optional_all_0 :: TestTree _Optional_all_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Optional/all Natural Natural/even ([+3] : Optional Natural)" + e <- Util.code "./Prelude/Optional/all Natural Natural/even ([ +3 ] : Optional Natural)" Util.assertNormalizesTo e "False" ) _Optional_all_1 :: TestTree @@ -845,7 +845,7 @@ _Optional_any_0 :: TestTree _Optional_any_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Optional/any Natural Natural/even ([+2] : Optional Natural)" + e <- Util.code "./Prelude/Optional/any Natural Natural/even ([ +2 ] : Optional Natural)" Util.assertNormalizesTo e "True" ) _Optional_any_1 :: TestTree @@ -863,7 +863,7 @@ \→ λ(nothing : optional) \n\ \→ just 1 \n\ \) \n" - Util.assertNormalizesTo e "[1] : Optional Integer" ) + Util.assertNormalizesTo e "[ 1 ] : Optional Integer" ) _Optional_build_1 :: TestTree _Optional_build_1 = Test.Tasty.HUnit.testCase "Example #1" (do @@ -880,13 +880,13 @@ _Optional_concat_0 :: TestTree _Optional_concat_0 = Test.Tasty.HUnit.testCase "Example #0" (do e <- Util.code - "./Prelude/Optional/concat Integer ([[1] : Optional Integer] : Optional (Optional Integer))" - Util.assertNormalizesTo e "[1] : Optional Integer" ) + "./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 - "./Prelude/Optional/concat Integer ([[] : Optional Integer] : Optional (Optional Integer))" + "./Prelude/Optional/concat Integer ([ [] : Optional Integer ] : Optional (Optional Integer))" Util.assertNormalizesTo e "[] : Optional Integer" ) _Optional_concat_2 :: TestTree @@ -897,18 +897,18 @@ _Optional_filter_0 :: TestTree _Optional_filter_0 = Test.Tasty.HUnit.testCase "Example #0" (do e <- Util.code - "./Prelude/Optional/filter Natural Natural/even ([+2] : Optional Natural)" - Util.assertNormalizesTo e "[+2] : Optional Natural" ) + "./Prelude/Optional/filter Natural Natural/even ([ +2 ] : Optional Natural)" + Util.assertNormalizesTo e "[ +2 ] : Optional Natural" ) _Optional_filter_1 :: TestTree _Optional_filter_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/Optional/filter Natural Natural/odd ([+2] : Optional Natural)" + e <- Util.code "./Prelude/Optional/filter Natural Natural/odd ([ +2 ] : Optional Natural)" Util.assertNormalizesTo e "[] : Optional Natural" ) _Optional_fold_0 :: TestTree _Optional_fold_0 = Test.Tasty.HUnit.testCase "Example #0" (do e <- Util.code - "./Prelude/Optional/fold Integer ([2] : Optional Integer) Integer (λ(x : Integer) → x) 0" + "./Prelude/Optional/fold Integer ([ 2 ] : Optional Integer) Integer (λ(x : Integer) → x) 0" Util.assertNormalizesTo e "2" ) _Optional_fold_1 :: TestTree @@ -920,19 +920,21 @@ _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, [1] : Optional Integer, [2] : Optional Integer]\n\ - \ : List (Optional Integer) \n\ - \) \n" - Util.assertNormalizesTo e "[1] : Optional Integer" ) + "./Prelude/Optional/head \n\ + \Integer \n\ + \( [ [] : Optional Integer \n\ + \ , [ 1 ] : Optional Integer \n\ + \ , [ 2 ] : Optional Integer \n\ + \ ] : List (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 ] : List (Optional Integer))\n" Util.assertNormalizesTo e "[] : Optional Integer" ) _Optional_head_2 :: TestTree @@ -943,19 +945,21 @@ _Optional_last_0 :: TestTree _Optional_last_0 = Test.Tasty.HUnit.testCase "Example #0" (do e <- Util.code - "./Prelude/Optional/last \n\ - \Integer \n\ - \( [[] : Optional Integer, [1] : Optional Integer, [2] : Optional Integer]\n\ - \ : List (Optional Integer) \n\ - \) \n" - Util.assertNormalizesTo e "[2] : Optional Integer" ) + "./Prelude/Optional/last \n\ + \Integer \n\ + \( [ [] : Optional Integer \n\ + \ , [1] : Optional Integer \n\ + \ , [2] : Optional Integer \n\ + \ ] : List (Optional Integer)\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 ] : List (Optional Integer))\n" Util.assertNormalizesTo e "[] : Optional Integer" ) _Optional_last_2 :: TestTree @@ -966,12 +970,19 @@ _Optional_map_0 :: TestTree _Optional_map_0 = Test.Tasty.HUnit.testCase "Example #0" (do e <- Util.code - "./Prelude/Optional/map Natural Bool Natural/even ([+3] : Optional Natural)" - Util.assertNormalizesTo e "[False] : Optional Bool" ) + "./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 + "./Prelude/Optional/map Natural Bool Natural/even ([] : Optional Natural)" + Util.assertNormalizesTo e "[] : Optional Bool" ) + _Optional_length_0 :: TestTree _Optional_length_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Optional/length Integer ([2] : Optional Integer)" + e <- Util.code + "./Prelude/Optional/length Integer ([ 2 ] : Optional Integer)" Util.assertNormalizesTo e "+1" ) _Optional_length_1 :: TestTree @@ -979,15 +990,9 @@ e <- Util.code "./Prelude/Optional/length Integer ([] : Optional Integer)" Util.assertNormalizesTo e "+0" ) -_Optional_map_1 :: TestTree -_Optional_map_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code - "./Prelude/Optional/map Natural Bool Natural/even ([] : Optional Natural)" - Util.assertNormalizesTo e "[] : Optional Bool" ) - _Optional_null_0 :: TestTree _Optional_null_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Optional/null Integer ([2] : Optional Integer)" + e <- Util.code "./Prelude/Optional/null Integer ([ 2] : Optional Integer)" Util.assertNormalizesTo e "False" ) _Optional_null_1 :: TestTree @@ -997,8 +1002,9 @@ _Optional_toList_0 :: TestTree _Optional_toList_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Optional/toList Integer ([1] : Optional Integer)" - Util.assertNormalizesTo e "[1]" ) + e <- Util.code + "./Prelude/Optional/toList Integer ([ 1 ] : Optional Integer)" + Util.assertNormalizesTo e "[ 1 ]" ) _Optional_toList_1 :: TestTree _Optional_toList_1 = Test.Tasty.HUnit.testCase "Example #1" (do @@ -1008,11 +1014,11 @@ _Optional_unzip_0 :: TestTree _Optional_unzip_0 = Test.Tasty.HUnit.testCase "Example #0" (do e <- Util.code - "./Prelude/Optional/unzip \n\ - \Text \n\ - \Bool \n\ - \([{ _1 = \"ABC\", _2 = True }] : Optional { _1 : Text, _2 : Bool })\n" - Util.assertNormalizesTo e "{ _1 = [\"ABC\"] : Optional Text, _2 = [True] : Optional Bool }" ) + "./Prelude/Optional/unzip \n\ + \Text \n\ + \Bool \n\ + \([ { _1 = \"ABC\", _2 = True } ] : Optional { _1 : Text, _2 : Bool })\n" + 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 @@ -1022,7 +1028,7 @@ _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\" ] : List Text)" Util.assertNormalizesTo e "\"ABCDEFGHI\"" ) _Text_concat_1 :: TestTree @@ -1033,7 +1039,7 @@ _Text_concatMap_0 :: TestTree _Text_concatMap_0 = Test.Tasty.HUnit.testCase "Example #0" (do e <- Util.code - "./Prelude/Text/concatMap Integer (λ(n : Integer) → \"${Integer/show n} \") [0, 1, 2]" + "./Prelude/Text/concatMap Integer (λ(n : Integer) → \"${Integer/show n} \") [ 0, 1, 2 ]" Util.assertNormalizesTo e "\"0 1 2 \"" ) _Text_concatMap_1 :: TestTree @@ -1044,7 +1050,7 @@ _Text_concatMapSep_0 :: TestTree _Text_concatMapSep_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Text/concatMapSep \", \" Integer Integer/show [0, 1, 2]" + e <- Util.code "./Prelude/Text/concatMapSep \", \" Integer Integer/show [ 0, 1, 2 ]" Util.assertNormalizesTo e "\"0, 1, 2\"" ) _Text_concatMapSep_1 :: TestTree @@ -1055,7 +1061,7 @@ _Text_concatSep_0 :: TestTree _Text_concatSep_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Text/concatSep \", \" [\"ABC\", \"DEF\", \"GHI\"]" + e <- Util.code "./Prelude/Text/concatSep \", \" [ \"ABC\", \"DEF\", \"GHI\" ]" Util.assertNormalizesTo e "\"ABC, DEF, GHI\"" ) _Text_concatSep_1 :: TestTree diff --git a/tests/Normalization.hs b/tests/Normalization.hs --- a/tests/Normalization.hs +++ b/tests/Normalization.hs @@ -79,12 +79,12 @@ integerShow :: TestTree integerShow = testCase "Integer/show" $ do e <- code "[Integer/show 1337, Integer/show -42, Integer/show 0]" - e `assertNormalizesTo` "[\"1337\", \"-42\", \"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\"]" + e `assertNormalizesTo` "[ \"-0.42\", \"13.37\" ]" optionalFold :: TestTree optionalFold = testGroup "Optional/fold" [ just, nothing ] @@ -110,7 +110,7 @@ \→ λ(nothing : optional) \n\ \→ just +1 \n\ \) \n" - e `assertNormalizesTo` "[+1] : Optional Natural" + e `assertNormalizesTo` "[ +1 ] : Optional Natural" optionalBuildShadowing :: TestTree optionalBuildShadowing = testCase "handles shadowing" $ do @@ -122,7 +122,7 @@ \→ λ(x : optional) \n\ \→ x@1 1 \n\ \) \n" - e `assertNormalizesTo` "[1] : Optional Integer" + e `assertNormalizesTo` "[ 1 ] : Optional Integer" optionalBuildIrreducible :: TestTree optionalBuildIrreducible = testCase "irreducible" $ do @@ -176,4 +176,4 @@ \ Text \n\ \ ([\"foo\"] : Optional Text)\n\ \) \n" - test `assertNormalizesTo` "[\"foo\"] : Optional Text" + test `assertNormalizesTo` "[ \"foo\" ] : Optional Text" diff --git a/tests/Regression.hs b/tests/Regression.hs --- a/tests/Regression.hs +++ b/tests/Regression.hs @@ -26,6 +26,7 @@ [ issue96 , issue126 , issue151 + , issue164 , parsing0 , typeChecking0 , typeChecking1 @@ -106,6 +107,13 @@ -- immediately with a type-checking failure. shouldNotTypeCheck "./tests/regression/issue151a.dhall" shouldNotTypeCheck "./tests/regression/issue151b.dhall" ) + +issue164 :: TestTree +issue164 = Test.Tasty.HUnit.testCase "Issue #164" (do + -- Verify that parsing should not fail on a single-quote within a + -- single-quoted string + _ <- Util.code "./tests/regression/issue164.dhall" + return () ) parsing0 :: TestTree parsing0 = Test.Tasty.HUnit.testCase "Parsing regression #0" (do diff --git a/tests/regression/issue164.dhall b/tests/regression/issue164.dhall new file mode 100644 --- /dev/null +++ b/tests/regression/issue164.dhall @@ -0,0 +1,1 @@ +''Single quotes like ' should be allowed in a single-quoted string''