diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,41 @@ +1.11.0 + +* BREAKING CHANGE TO THE API: Fix `{Natural,Optional,List}/build` semantics to + match standard + * This is a breaking change because the `OptionalLit` and `ListLit` + constructors changed their representations to efficiently support the + standard semantics + * `ListLit` now stores a `Data.Sequence.Seq` instead of a + `Data.Vector.Vector` + * `OptionalLit` now stores a `Maybe` instead of a `Data.Vector.Vector` + * See: https://github.com/dhall-lang/dhall-haskell/pull/300 +* BREAKING CHANGE TO THE COMMAND LINE: `dhall` executable always formats output + * Previously you had to opt into formatting using `--pretty` + * Now formatting is obligatory and the `--pretty` flag is gone + * See: https://github.com/dhall-lang/dhall-haskell/pull/303 +* Feature: New `:save` command for `dhall-repl` + * Now you can save an expression to a file: `./yourFile = someExpression` + * See: https://github.com/dhall-lang/dhall-haskell/pull/309 +* Improvement: Add new simplifications to match standard + * See: https://github.com/dhall-lang/dhall-haskell/pull/312 + * See: https://github.com/dhall-lang/dhall-haskell/pull/316 +* Improvement: Fix equivalence check to match standard + * Practically this means that more corner cases of the language correctly + type-check than before +* Improvement: New `--plain` flag to disable syntax highlighting + * See: https://github.com/dhall-lang/dhall-haskell/pull/310 +* Improvement: Prelude now provides an umbrella `package.dhall` import + * This is primarily for convenience + * See: https://github.com/dhall-lang/dhall-haskell/pull/298 +* Improvement: Context is now normalized + * See: https://github.com/dhall-lang/dhall-haskell/pull/302 +* Replace `cryptohash` dependency with `cryptonite` + * See: https://github.com/dhall-lang/dhall-haskell/commit/5d2012927a062ec8bdf2bbaba77150344f38db77 +* Increase upper bound on exceptions + * See: https://github.com/dhall-lang/dhall-haskell/pull/306 +* Fix type error in tutorial + * See: https://github.com/dhall-lang/dhall-haskell/commit/5a9126b2f684d3236fc1e8e20e206cfaf47d97db + 1.10.0 * Feature: Records/unions can now have fields/alternatives that are types 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 ] = 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 ] = True -./even ([ False, True ] : List Bool) = False +./even [ False, True ] = False -./even ([ False ] : List Bool) = False +./even [ False ] = 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 ] = False -./odd ([ True, False ] : List Bool) = True +./odd [ True, False ] = True -./odd ([ True ] : List Bool) = True +./odd [ True ] = 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 ] = 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 ] = 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 ] = 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" ] ./build Text diff --git a/Prelude/List/concat b/Prelude/List/concat --- a/Prelude/List/concat +++ b/Prelude/List/concat @@ -5,18 +5,17 @@ ``` ./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 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 ] ./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 @@ -4,11 +4,11 @@ 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 diff --git a/Prelude/List/fold b/Prelude/List/fold --- a/Prelude/List/fold +++ b/Prelude/List/fold @@ -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 @@ λ(nil : Natural) → ./fold Natural - ([ +2, +3, +5 ] : List Natural) + [ +2, +3, +5 ] 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 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 ] ./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 ] = [ 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,11 +4,11 @@ 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 } 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 ] ./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 ] = [ 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 ] = +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 ] += [ True, False, False ] ./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 ] = 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 ] ./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 ] = [ 2, 1, 0 ] : List Integer ./reverse Integer ([] : List Integer) = [] : List Integer ``` diff --git a/Prelude/List/shifted b/Prelude/List/shifted --- a/Prelude/List/shifted +++ b/Prelude/List/shifted @@ -7,20 +7,19 @@ ``` ./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 @@ , { 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 } diff --git a/Prelude/List/unzip b/Prelude/List/unzip --- a/Prelude/List/unzip +++ b/Prelude/List/unzip @@ -10,10 +10,10 @@ ( [ { _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 }) 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 ] ./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 ] = +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 ] = +10 ./sum ([] : List Natural) = +0 ``` diff --git a/Prelude/Optional/head b/Prelude/Optional/head --- a/Prelude/Optional/head +++ b/Prelude/Optional/head @@ -6,17 +6,15 @@ ``` ./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)) diff --git a/Prelude/Optional/last b/Prelude/Optional/last --- a/Prelude/Optional/last +++ b/Prelude/Optional/last @@ -6,16 +6,15 @@ ``` ./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)) 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" ] = "ABCDEFGHI" ./concat ([] : List Text) = "" ``` diff --git a/dhall-repl/Main.hs b/dhall-repl/Main.hs --- a/dhall-repl/Main.hs +++ b/dhall-repl/Main.hs @@ -20,6 +20,7 @@ import qualified Dhall.Import as Dhall import qualified Dhall.Parser as Dhall import qualified Dhall.TypeCheck as Dhall +import qualified System.Console.ANSI import qualified System.Console.Haskeline.MonadException as Haskeline import qualified System.Console.Repline as Repline import qualified System.IO @@ -97,7 +98,7 @@ modify ( \e -> e { envIt = Just ( Binding expr exprType ) } ) - output expr + output System.IO.stdout expr @@ -116,7 +117,7 @@ exprType' <- normalize exprType - output ( Expr.Annot loaded exprType' ) + output System.IO.stdout ( Expr.Annot loaded exprType' ) @@ -181,18 +182,33 @@ ) output + System.IO.stdout ( Expr.Annot ( Expr.Var ( Dhall.V varName 0 ) ) t ) addBinding _ = liftIO ( fail ":let should be of the form `:let x = y`" ) +saveBinding :: ( MonadIO m, MonadState Env m ) => [String] -> m () +saveBinding (file : "=" : tokens) = do + loadedExpression <- parseAndLoad (unwords tokens) + _ <- typeCheck loadedExpression + + normalizedExpression <- normalize loadedExpression + + let handler handle = output handle normalizedExpression + + liftIO (System.IO.withFile file System.IO.WriteMode handler) +saveBinding _ = fail ":save should be of the form `:save x = y`" + + options :: ( Haskeline.MonadException m, MonadIO m, MonadState Env m ) => Repline.Options m options = [ ( "type", dontCrash . typeOf ) , ( "let", dontCrash . addBinding ) + , ( "save", dontCrash . saveBinding ) ] @@ -213,20 +229,21 @@ ( \ e@SomeException{} -> liftIO ( putStrLn ( displayException e ) ) ) -output :: ( Pretty.Pretty a, MonadIO m ) => Dhall.Expr s a -> m () -output expr = do - let - opts = - Pretty.defaultLayoutOptions - { Pretty.layoutPageWidth = Pretty.AvailablePerLine 80 1.0 } +output + :: (Pretty.Pretty a, MonadIO m) + => System.IO.Handle -> Dhall.Expr s a -> m () +output handle expr = do + let opts = + Pretty.defaultLayoutOptions + { Pretty.layoutPageWidth = Pretty.AvailablePerLine 80 1.0 } - liftIO - ( Pretty.renderIO - System.IO.stdout - ( fmap - Dhall.Pretty.annToAnsiStyle - ( Pretty.layoutSmart opts ( Dhall.Pretty.prettyExpr expr ) ) - ) - ) + let stream = Pretty.layoutSmart opts (Dhall.Pretty.prettyExpr expr) + supportsANSI <- liftIO (System.Console.ANSI.hSupportsANSI handle) + let ansiStream = + if supportsANSI + then fmap Dhall.Pretty.annToAnsiStyle stream + else Pretty.unAnnotateS stream - liftIO ( putStrLn "" ) -- Pretty printing doesn't end with a new line + liftIO (Pretty.renderIO handle ansiStream) + + liftIO (putStrLn "") -- Pretty printing doesn't end with a new line diff --git a/dhall.cabal b/dhall.cabal --- a/dhall.cabal +++ b/dhall.cabal @@ -1,5 +1,5 @@ Name: dhall -Version: 1.10.0 +Version: 1.11.0 Cabal-Version: >=1.8.0.2 Build-Type: Simple Tested-With: GHC == 8.0.1 @@ -83,10 +83,68 @@ Prelude/Text/concatSep tests/format/*.dhall tests/normalization/*.dhall + tests/normalization/examples/Bool/and/*.dhall + tests/normalization/examples/Bool/build/*.dhall + tests/normalization/examples/Bool/even/*.dhall + tests/normalization/examples/Bool/fold/*.dhall + tests/normalization/examples/Bool/not/*.dhall + tests/normalization/examples/Bool/odd/*.dhall + tests/normalization/examples/Bool/or/*.dhall + tests/normalization/examples/Bool/show/*.dhall + tests/normalization/examples/Double/show/*.dhall + tests/normalization/examples/Integer/show/*.dhall + tests/normalization/examples/List/all/*.dhall + tests/normalization/examples/List/any/*.dhall + tests/normalization/examples/List/build/*.dhall + tests/normalization/examples/List/concat/*.dhall + tests/normalization/examples/List/concatMap/*.dhall + tests/normalization/examples/List/filter/*.dhall + tests/normalization/examples/List/fold/*.dhall + tests/normalization/examples/List/generate/*.dhall + tests/normalization/examples/List/head/*.dhall + tests/normalization/examples/List/indexed/*.dhall + tests/normalization/examples/List/iterate/*.dhall + tests/normalization/examples/List/last/*.dhall + tests/normalization/examples/List/length/*.dhall + tests/normalization/examples/List/map/*.dhall + tests/normalization/examples/List/null/*.dhall + tests/normalization/examples/List/replicate/*.dhall + tests/normalization/examples/List/reverse/*.dhall + tests/normalization/examples/List/shifted/*.dhall + tests/normalization/examples/List/unzip/*.dhall + tests/normalization/examples/Natural/build/*.dhall + tests/normalization/examples/Natural/enumerate/*.dhall + tests/normalization/examples/Natural/even/*.dhall + tests/normalization/examples/Natural/fold/*.dhall + tests/normalization/examples/Natural/isZero/*.dhall + tests/normalization/examples/Natural/odd/*.dhall + tests/normalization/examples/Natural/product/*.dhall + tests/normalization/examples/Natural/show/*.dhall + tests/normalization/examples/Natural/sum/*.dhall + tests/normalization/examples/Natural/toInteger/*.dhall + tests/normalization/examples/Optional/all/*.dhall + tests/normalization/examples/Optional/any/*.dhall + tests/normalization/examples/Optional/build/*.dhall + tests/normalization/examples/Optional/concat/*.dhall + tests/normalization/examples/Optional/filter/*.dhall + tests/normalization/examples/Optional/fold/*.dhall + tests/normalization/examples/Optional/head/*.dhall + tests/normalization/examples/Optional/last/*.dhall + tests/normalization/examples/Optional/length/*.dhall + tests/normalization/examples/Optional/map/*.dhall + tests/normalization/examples/Optional/null/*.dhall + tests/normalization/examples/Optional/toList/*.dhall + tests/normalization/examples/Optional/unzip/*.dhall + tests/normalization/examples/Text/concat/*.dhall + tests/normalization/examples/Text/concatMap/*.dhall + tests/normalization/examples/Text/concatMapSep/*.dhall + tests/normalization/examples/Text/concatSep/*.dhall + tests/normalization/simplifications/*.dhall tests/parser/*.dhall tests/regression/*.dhall tests/tutorial/*.dhall tests/typecheck/*.dhall + tests/typecheck/examples/Monoid/*.dhall Source-Repository head Type: git @@ -102,14 +160,15 @@ case-insensitive < 1.3 , containers >= 0.5.0.0 && < 0.6 , contravariant < 1.5 , - cryptohash < 0.12, - exceptions >= 0.8.3 && < 0.9 , + cryptonite >= 0.23 && < 1.0 , + exceptions >= 0.8.3 && < 0.10, directory >= 1.3 && < 1.4 , filepath >= 1.4 && < 1.5 , http-client >= 0.4.30 && < 0.6 , http-client-tls >= 0.2.0 && < 0.4 , insert-ordered-containers >= 0.1.0.1 && < 0.3 , lens-family-core >= 1.0.0 && < 1.3 , + memory >= 0.14 && < 0.15, parsers >= 0.12.4 && < 0.13, prettyprinter >= 1.2.0.1 && < 1.3 , prettyprinter-ansi-terminal >= 1.1.1 && < 1.2 , @@ -154,6 +213,7 @@ Main-Is: Main.hs Build-Depends: base >= 4 && < 5 , + ansi-terminal , dhall , haskeline >= 0.7.3.0 && < 0.8 , mtl >= 2.2.1 && < 2.3 , @@ -198,7 +258,6 @@ Main-Is: Tests.hs GHC-Options: -Wall Other-Modules: - Examples Format Normalization Parser diff --git a/dhall/Main.hs b/dhall/Main.hs --- a/dhall/Main.hs +++ b/dhall/Main.hs @@ -36,7 +36,7 @@ data Options w = Options { explain :: w ::: Bool "Explain error messages in more detail" , version :: w ::: Bool "Display version and exit" - , pretty :: w ::: Bool "Format output" + , plain :: w ::: Bool "Disable syntax highlighting" } deriving (Generic) instance ParseRecord (Options Wrapped) @@ -46,9 +46,6 @@ Pretty.defaultLayoutOptions { Pretty.layoutPageWidth = Pretty.AvailablePerLine 80 1.0 } -unbounded :: Pretty.LayoutOptions -unbounded = Pretty.LayoutOptions { Pretty.layoutPageWidth = Pretty.Unbounded } - main :: IO () main = do Options {..} <- Options.Generic.unwrapRecord "Compiler for the Dhall language" @@ -96,12 +93,12 @@ let render h e = do let doc = prettyExpr e - let layoutOptions = if pretty then opts else unbounded + let layoutOptions = opts let stream = Pretty.layoutSmart layoutOptions doc supportsANSI <- System.Console.ANSI.hSupportsANSI h let ansiStream = - if supportsANSI + if supportsANSI && not plain then fmap annToAnsiStyle stream else Pretty.unAnnotateS stream diff --git a/src/Dhall.hs b/src/Dhall.hs --- a/src/Dhall.hs +++ b/src/Dhall.hs @@ -40,8 +40,9 @@ , lazyText , strictText , maybe - , vector + , sequence , list + , vector , unit , string , pair @@ -56,6 +57,7 @@ -- * Re-exports , Natural + , Seq , Text , Vector , Generic @@ -67,6 +69,7 @@ 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.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 @@ 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,8 +461,16 @@ [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. >>> input unit "{=}" @@ -549,12 +558,15 @@ 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 @@ 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 @@ 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 (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 (Vector a) where + injectWith = fmap (contramap Data.Vector.toList) injectWith -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) +instance Inject a => Inject (Data.Set.Set a) where + injectWith = fmap (contramap Data.Set.toList) injectWith deriving instance (Inject a, Inject b) => Inject (a, b) diff --git a/src/Dhall/Core.hs b/src/Dhall/Core.hs --- a/src/Dhall/Core.hs +++ b/src/Dhall/Core.hs @@ -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. @@ -27,9 +28,11 @@ , Expr(..) -- * Normalization + , alphaNormalize , normalize , normalizeWith , Normalizer + , judgmentallyEqual , subst , shift , isNormalized @@ -50,6 +53,7 @@ import Control.Applicative (Applicative(..), (<$>)) #endif import Control.Applicative (empty) +import Crypto.Hash (SHA256) import Data.Bifunctor (Bifunctor(..)) import Data.Foldable import Data.HashMap.Strict.InsOrd (InsOrdHashMap) @@ -57,29 +61,25 @@ 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) import qualified Control.Monad -import qualified Data.ByteString -import qualified Data.ByteString.Char8 -import qualified Data.ByteString.Base16 +import qualified Crypto.Hash 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 @@ -137,17 +137,13 @@ -- | A `PathType` extended with an optional hash for semantic integrity checks data PathHashed = PathHashed - { hash :: Maybe Data.ByteString.ByteString + { hash :: Maybe (Crypto.Hash.Digest SHA256) , 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 + build (PathHashed (Just h) p) = build p <> "sha256:" <> build (show h) <> " " -- | Path to an external resource data Path = Path @@ -283,7 +279,7 @@ | 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 +298,9 @@ | 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 @@ -851,6 +847,258 @@ -- and `subst` does nothing to a closed expression subst _ _ (Embed p) = Embed p +{-| α-normalize an expression by renaming all variables to @\"_\"@ and using + De Bruijn indices to distinguish them +-} +alphaNormalize :: Expr s a -> Expr s a +alphaNormalize (Const c) = + Const c +alphaNormalize (Var v) = + Var v +alphaNormalize (Lam x _A₀ b₀) = + Lam "_" _A₁ b₃ + where + _A₁ = alphaNormalize _A₀ + + v₀ = Var (V "_" 0) + v₁ = shift 1 (V x 0) v₀ + b₁ = subst (V x 0) v₁ b₀ + b₂ = shift (-1) (V x 0) b₁ + b₃ = alphaNormalize b₂ +alphaNormalize (Pi x _A₀ _B₀) = + Pi "_" _A₁ _B₃ + where + _A₁ = alphaNormalize _A₀ + + v₀ = Var (V "_" 0) + v₁ = shift 1 (V x 0) v₀ + _B₁ = subst (V x 0) v₁ _B₀ + _B₂ = shift (-1) (V x 0) _B₁ + _B₃ = alphaNormalize _B₂ +alphaNormalize (App f₀ a₀) = + App f₁ a₁ + where + f₁ = alphaNormalize f₀ + + a₁ = alphaNormalize a₀ +alphaNormalize (Let x (Just _A₀) a₀ b₀) = + Let x (Just _A₁) a₁ b₃ + where + _A₁ = alphaNormalize _A₀ + + a₁ = alphaNormalize a₀ + + v₀ = Var (V "_" 0) + v₁ = shift 1 (V x 0) v₀ + b₁ = subst (V x 0) v₁ b₀ + b₂ = shift (-1) (V x 0) b₁ + b₃ = alphaNormalize b₂ +alphaNormalize (Let x Nothing a₀ b₀) = + Let x Nothing a₁ b₃ + where + a₁ = alphaNormalize a₀ + + v₀ = Var (V "_" 0) + v₁ = shift 1 (V x 0) v₀ + b₁ = subst (V x 0) v₁ b₀ + b₂ = shift (-1) (V x 0) b₁ + b₃ = alphaNormalize b₂ +alphaNormalize (Annot t₀ _T₀) = + Annot t₁ _T₁ + where + t₁ = alphaNormalize t₀ + + _T₁ = alphaNormalize _T₀ +alphaNormalize Bool = + Bool +alphaNormalize (BoolLit b) = + BoolLit b +alphaNormalize (BoolAnd l₀ r₀) = + BoolAnd l₁ r₁ + where + l₁ = alphaNormalize l₀ + + r₁ = alphaNormalize r₀ +alphaNormalize (BoolOr l₀ r₀) = + BoolOr l₁ r₁ + where + l₁ = alphaNormalize l₀ + + r₁ = alphaNormalize r₀ +alphaNormalize (BoolEQ l₀ r₀) = + BoolEQ l₁ r₁ + where + l₁ = alphaNormalize l₀ + + r₁ = alphaNormalize r₀ +alphaNormalize (BoolNE l₀ r₀) = + BoolNE l₁ r₁ + where + l₁ = alphaNormalize l₀ + + r₁ = alphaNormalize r₀ +alphaNormalize (BoolIf t₀ l₀ r₀) = + BoolIf t₁ l₁ r₁ + where + t₁ = alphaNormalize t₀ + + l₁ = alphaNormalize l₀ + + r₁ = alphaNormalize r₀ +alphaNormalize Natural = + Natural +alphaNormalize (NaturalLit n) = + NaturalLit n +alphaNormalize NaturalFold = + NaturalFold +alphaNormalize NaturalBuild = + NaturalBuild +alphaNormalize NaturalIsZero = + NaturalIsZero +alphaNormalize NaturalEven = + NaturalEven +alphaNormalize NaturalOdd = + NaturalOdd +alphaNormalize NaturalToInteger = + NaturalToInteger +alphaNormalize NaturalShow = + NaturalShow +alphaNormalize (NaturalPlus l₀ r₀) = + NaturalPlus l₁ r₁ + where + l₁ = alphaNormalize l₀ + + r₁ = alphaNormalize r₀ +alphaNormalize (NaturalTimes l₀ r₀) = + NaturalTimes l₁ r₁ + where + l₁ = alphaNormalize l₀ + + r₁ = alphaNormalize r₀ +alphaNormalize Integer = + Integer +alphaNormalize (IntegerLit n) = + IntegerLit n +alphaNormalize IntegerShow = + IntegerShow +alphaNormalize Double = + Double +alphaNormalize (DoubleLit n) = + DoubleLit n +alphaNormalize DoubleShow = + DoubleShow +alphaNormalize Text = + Text +alphaNormalize (TextLit (Chunks xys₀ z)) = + TextLit (Chunks xys₁ z) + where + xys₁ = do + (x, y₀) <- xys₀ + let y₁ = alphaNormalize y₀ + return (x, y₁) +alphaNormalize (TextAppend l₀ r₀) = + TextAppend l₁ r₁ + where + l₁ = alphaNormalize l₀ + + r₁ = alphaNormalize r₀ +alphaNormalize List = + List +alphaNormalize (ListLit (Just _T₀) ts₀) = + ListLit (Just _T₁) ts₁ + where + _T₁ = alphaNormalize _T₀ + + ts₁ = fmap alphaNormalize ts₀ +alphaNormalize (ListLit Nothing ts₀) = + ListLit Nothing ts₁ + where + ts₁ = fmap alphaNormalize ts₀ +alphaNormalize (ListAppend l₀ r₀) = + ListAppend l₁ r₁ + where + l₁ = alphaNormalize l₀ + + r₁ = alphaNormalize r₀ +alphaNormalize ListBuild = + ListBuild +alphaNormalize ListFold = + ListFold +alphaNormalize ListLength = + ListLength +alphaNormalize ListHead = + ListHead +alphaNormalize ListLast = + ListLast +alphaNormalize ListIndexed = + ListIndexed +alphaNormalize ListReverse = + ListReverse +alphaNormalize Optional = + Optional +alphaNormalize (OptionalLit _T₀ ts₀) = + OptionalLit _T₁ ts₁ + where + _T₁ = alphaNormalize _T₀ + + ts₁ = fmap alphaNormalize ts₀ +alphaNormalize OptionalFold = + OptionalFold +alphaNormalize OptionalBuild = + OptionalBuild +alphaNormalize (Record kts₀) = + Record kts₁ + where + kts₁ = fmap alphaNormalize kts₀ +alphaNormalize (RecordLit kvs₀) = + RecordLit kvs₁ + where + kvs₁ = fmap alphaNormalize kvs₀ +alphaNormalize (Union kts₀) = + Union kts₁ + where + kts₁ = fmap alphaNormalize kts₀ +alphaNormalize (UnionLit k v₀ kts₀) = + UnionLit k v₁ kts₁ + where + v₁ = alphaNormalize v₀ + + kts₁ = fmap alphaNormalize kts₀ +alphaNormalize (Combine l₀ r₀) = + Combine l₁ r₁ + where + l₁ = alphaNormalize l₀ + + r₁ = alphaNormalize r₀ +alphaNormalize (Prefer l₀ r₀) = + Prefer l₁ r₁ + where + l₁ = alphaNormalize l₀ + + r₁ = alphaNormalize r₀ +alphaNormalize (Merge t₀ u₀ _T₀) = + Merge t₁ u₁ _T₁ + where + t₁ = alphaNormalize t₀ + + u₁ = alphaNormalize u₀ + + _T₁ = fmap alphaNormalize _T₀ +alphaNormalize (Constructors u₀) = + Constructors u₁ + where + u₁ = alphaNormalize u₀ +alphaNormalize (Field e₀ a) = + Field e₁ a + where + e₁ = alphaNormalize e₀ +alphaNormalize (Note s e₀) = + Note s e₁ + where + e₁ = alphaNormalize e₀ +alphaNormalize (Embed a) = + Embed a + {-| Reduce an expression to its normal form, performing beta reduction `normalize` does not type-check the expression. You may want to type-check @@ -860,7 +1108,7 @@ However, `normalize` will not fail if the expression is ill-typed and will leave ill-typed sub-expressions unevaluated. -} -normalize :: Expr s a -> Expr t a +normalize :: Eq a => Expr s a -> Expr t a normalize = normalizeWith (const Nothing) {-| This function is used to determine whether folds like @Natural/fold@ or @@ -949,30 +1197,22 @@ {-| Reduce an expression to its normal form, performing beta reduction and applying any custom definitions. - + `normalizeWith` is designed to be used with function `typeWith`. The `typeWith` - function allows typing of Dhall functions in a custom typing context whereas - `normalizeWith` allows evaluating Dhall expressions in a custom context. + function allows typing of Dhall functions in a custom typing context whereas + `normalizeWith` allows evaluating Dhall expressions in a custom context. To be more precise `normalizeWith` applies the given normalizer when it finds an application term that it cannot reduce by other means. Note that the context used in normalization will determine the properties of normalization. That is, if the functions in custom context are not total then the Dhall language, evaluated - with those functions is not total either. - + with those functions is not total either. + -} -normalizeWith :: Normalizer a -> Expr s a -> Expr t a +normalizeWith :: Eq a => 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 +1231,14 @@ 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` + + -- build/fold 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 `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 +1251,11 @@ 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 +1266,35 @@ 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 +1302,42 @@ 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 m (Data.Sequence.reverse xs)) + where + m = if Data.Sequence.null xs then Just t else Nothing 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' @@ -1127,53 +1351,46 @@ Annot x _ -> loop x Bool -> Bool BoolLit b -> BoolLit b - BoolAnd x y -> - case x' of - BoolLit xn -> - case y' of - BoolLit yn -> BoolLit (xn && yn) - _ -> BoolAnd x' y' - _ -> BoolAnd x' y' + BoolAnd x y -> decide (loop x) (loop y) where - x' = loop x - y' = loop y - BoolOr x y -> - case x' of - BoolLit xn -> - case y' of - BoolLit yn -> BoolLit (xn || yn) - _ -> BoolOr x' y' - _ -> BoolOr x' y' + decide (BoolLit True ) r = r + decide (BoolLit False) _ = BoolLit False + decide l (BoolLit True ) = l + decide _ (BoolLit False) = BoolLit False + decide l r + | judgmentallyEqual l r = l + | otherwise = BoolAnd l r + BoolOr x y -> decide (loop x) (loop y) where - x' = loop x - y' = loop y - BoolEQ x y -> - case x' of - BoolLit xn -> - case y' of - BoolLit yn -> BoolLit (xn == yn) - _ -> BoolEQ x' y' - _ -> BoolEQ x' y' + decide (BoolLit False) r = r + decide (BoolLit True ) _ = BoolLit True + decide l (BoolLit False) = l + decide _ (BoolLit True ) = BoolLit True + decide l r + | judgmentallyEqual l r = l + | otherwise = BoolOr l r + BoolEQ x y -> decide (loop x) (loop y) where - x' = loop x - y' = loop y - BoolNE x y -> - case x' of - BoolLit xn -> - case y' of - BoolLit yn -> BoolLit (xn /= yn) - _ -> BoolNE x' y' - _ -> BoolNE x' y' + decide (BoolLit True ) r = r + decide l (BoolLit True ) = l + decide l r + | judgmentallyEqual l r = BoolLit True + | otherwise = BoolEQ l r + BoolNE x y -> decide (loop x) (loop y) where - x' = loop x - y' = loop y - BoolIf b true false -> case loop b of - BoolLit True -> true' - BoolLit False -> false' - b' -> BoolIf b' true' false' + decide (BoolLit False) r = r + decide l (BoolLit False) = l + decide l r + | judgmentallyEqual l r = BoolLit False + | otherwise = BoolNE l r + BoolIf bool true false -> decide (loop bool) (loop true) (loop false) where - true' = loop true - false' = loop false + decide (BoolLit True ) l _ = l + decide (BoolLit False) _ r = r + decide b (BoolLit True) (BoolLit False) = b + decide b l r + | judgmentallyEqual l r = l + | otherwise = BoolIf b l r Natural -> Natural NaturalLit n -> NaturalLit n NaturalFold -> NaturalFold @@ -1183,26 +1400,20 @@ NaturalOdd -> NaturalOdd NaturalToInteger -> NaturalToInteger NaturalShow -> NaturalShow - NaturalPlus x y -> - case x' of - NaturalLit xn -> - case y' of - NaturalLit yn -> NaturalLit (xn + yn) - _ -> NaturalPlus x' y' - _ -> NaturalPlus x' y' + NaturalPlus x y -> decide (loop x) (loop y) where - x' = loop x - y' = loop y - NaturalTimes x y -> - case x' of - NaturalLit xn -> - case y' of - NaturalLit yn -> NaturalLit (xn * yn) - _ -> NaturalTimes x' y' - _ -> NaturalTimes x' y' + decide (NaturalLit 0) r = r + decide l (NaturalLit 0) = l + decide (NaturalLit m) (NaturalLit n) = NaturalLit (m + n) + decide l r = NaturalPlus l r + NaturalTimes x y -> decide (loop x) (loop y) where - x' = loop x - y' = loop y + decide (NaturalLit 1) r = r + decide l (NaturalLit 1) = l + decide (NaturalLit 0) _ = NaturalLit 0 + decide _ (NaturalLit 0) = NaturalLit 0 + decide (NaturalLit m) (NaturalLit n) = NaturalLit (m * n) + decide l r = NaturalTimes l r Integer -> Integer IntegerLit n -> IntegerLit n IntegerShow -> IntegerShow @@ -1220,31 +1431,26 @@ process (x, y) = case loop y of TextLit c -> [Chunks [] x, c] y' -> [Chunks [(x, y')] mempty] - TextAppend x y -> - case x' of - TextLit xt -> - case y' of - TextLit yt -> TextLit (xt <> yt) - _ -> TextAppend x' y' - _ -> TextAppend x' y' + TextAppend x y -> decide (loop x) (loop y) where - x' = loop x - y' = loop y + isEmpty (Chunks [] "") = True + isEmpty _ = False + + decide (TextLit m) r | isEmpty m = r + decide l (TextLit n) | isEmpty n = l + decide (TextLit m) (TextLit n) = TextLit (m <> n) + decide l r = TextAppend l r List -> List ListLit t es -> ListLit t' es' where t' = fmap loop t es' = fmap loop es - ListAppend x y -> - case x' of - ListLit t xs -> - case y' of - ListLit _ ys -> ListLit t (xs <> ys) - _ -> ListAppend x' y' - _ -> ListAppend x' y' + ListAppend x y -> decide (loop x) (loop y) where - x' = loop x - y' = loop y + decide (ListLit _ m) r | Data.Sequence.null m = r + decide l (ListLit _ n) | Data.Sequence.null n = l + decide (ListLit t m) (ListLit _ n) = ListLit t (m <> n) + decide l r = ListAppend l r ListBuild -> ListBuild ListFold -> ListFold ListLength -> ListLength @@ -1272,26 +1478,26 @@ where v' = loop v kvs' = fmap loop kvs - Combine x0 y0 -> - let combine x y = case x of - RecordLit kvsX -> case y of - RecordLit kvsY -> - let kvs = Data.HashMap.Strict.InsOrd.unionWith combine kvsX kvsY - in RecordLit (fmap loop kvs) - _ -> Combine x y - _ -> Combine x y - in combine (loop x0) (loop y0) - Prefer x y -> - case x' of - RecordLit kvsX -> - case y' of - RecordLit kvsY -> - RecordLit (fmap loop (Data.HashMap.Strict.InsOrd.union kvsY kvsX)) - _ -> Prefer x' y' - _ -> Prefer x' y' + Combine x y -> decide (loop x) (loop y) where - x' = loop x - y' = loop y + decide (RecordLit m) r | Data.HashMap.Strict.InsOrd.null m = + r + decide l (RecordLit n) | Data.HashMap.Strict.InsOrd.null n = + l + decide (RecordLit m) (RecordLit n) = + RecordLit (Data.HashMap.Strict.InsOrd.unionWith decide m n) + decide l r = + Combine l r + Prefer x y -> decide (loop x) (loop y) + where + decide (RecordLit m) r | Data.HashMap.Strict.InsOrd.null m = + r + decide l (RecordLit n) | Data.HashMap.Strict.InsOrd.null n = + l + decide (RecordLit m) (RecordLit n) = + RecordLit (Data.HashMap.Strict.InsOrd.union n m) + decide l r = + Prefer l r Merge x y t -> case x' of RecordLit kvsX -> @@ -1328,13 +1534,22 @@ Note _ e' -> loop e' Embed a -> Embed a +{-| Returns `True` if two expressions are α-equivalent and β-equivalent and + `False` otherwise +-} +judgmentallyEqual :: Eq a => Expr s a -> Expr t a -> Bool +judgmentallyEqual eL0 eR0 = alphaBetaNormalize eL0 == alphaBetaNormalize eR0 + where + alphaBetaNormalize :: Eq a => Expr s a -> Expr () a + alphaBetaNormalize = alphaNormalize . normalize + -- | Use this to wrap you embedded functions (see `normalizeWith`) to make them -- polymorphic enough to be used. type Normalizer a = forall s. Expr s a -> Maybe (Expr s a) -- | Check if an expression is in a normal form given a context of evaluation. --- Unlike `isNormalized`, this will fully normalize and traverse through the expression. --- +-- Unlike `isNormalized`, this will fully normalize and traverse through the expression. +-- -- It is much more efficient to use `isNormalized`. isNormalizedWith :: (Eq s, Eq a) => Normalizer a -> Expr s a -> Bool isNormalizedWith ctx e = e == (normalizeWith ctx e) @@ -1350,28 +1565,17 @@ 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 +1583,8 @@ 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 @@ -1564,25 +1752,6 @@ , Data.Text.unpack text <> " " , "``` " ] ) - -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 diff --git a/src/Dhall/Import.hs b/src/Dhall/Import.hs --- a/src/Dhall/Import.hs +++ b/src/Dhall/Import.hs @@ -71,7 +71,7 @@ > $ export BAZ='λ(x : Bool) → x == False' > $ dhall <<< "{ foo = env:FOO , bar = env:BAR , baz = env:BAZ }" > { bar : Text, baz : ∀(x : Bool) → Bool, foo : Integer } - > + > > { bar = "Hi", baz = λ(x : Bool) → x == False, foo = 1 } If you wish to import the raw contents of a path as @Text@ then add @@ -79,19 +79,19 @@ > $ dhall <<< "http://example.com as Text" > Text - > + > > "\n\n\n Example Domain\n\n charset=\"utf-8\" />\n ; charset=utf-8\" />\n ; charset=utf-8\" />\n initial-scale=1\" />\n \n\n\n\n
\n

Example Domain h1>\n

This domain is established to be used for illustrative examples in d > ocuments. You may use this\n domain in examples without prior coordination or @@ -124,6 +124,7 @@ import Control.Monad.Catch (throwM, MonadCatch(catch)) import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.Trans.State.Strict (StateT) +import Crypto.Hash (SHA256) import Data.ByteString.Lazy (ByteString) import Data.CaseInsensitive (CI) import Data.Map (Map) @@ -160,12 +161,13 @@ import Text.Trifecta.Delta (Delta(..)) import qualified Control.Monad.Trans.State.Strict as State -import qualified Crypto.Hash.SHA256 +import qualified Crypto.Hash +import qualified Data.ByteArray 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.Foldable import qualified Data.List as List import qualified Data.HashMap.Strict.InsOrd import qualified Data.Map.Strict as Map @@ -175,7 +177,6 @@ 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 +482,7 @@ -> 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 @@ -534,8 +535,8 @@ -- | Exception thrown when an integrity check fails data HashMismatch = HashMismatch - { expectedHash :: Data.ByteString.ByteString - , actualHash :: Data.ByteString.ByteString + { expectedHash :: Crypto.Hash.Digest SHA256 + , actualHash :: Crypto.Hash.Digest SHA256 } deriving (Typeable) instance Exception HashMismatch @@ -547,14 +548,11 @@ <> "\n" <> "Expected hash:\n" <> "\n" - <> "↳ " <> toString expectedHash <> "\n" + <> "↳ " <> show expectedHash <> "\n" <> "\n" <> "Actual hash:\n" <> "\n" - <> "↳ " <> toString actualHash <> "\n" - where - toString = - Data.ByteString.Char8.unpack . Data.ByteString.Base16.encode + <> "↳ " <> show actualHash <> "\n" parseFromFileEx :: Text.Trifecta.Parser a @@ -849,8 +847,8 @@ load = loadWithContext Dhall.Context.empty -- | Hash a fully resolved expression -hashExpression :: Expr s X -> Data.ByteString.ByteString -hashExpression expr = Crypto.Hash.SHA256.hashlazy actualBytes +hashExpression :: Expr s X -> (Crypto.Hash.Digest SHA256) +hashExpression expr = Crypto.Hash.hashlazy actualBytes where text = Dhall.Core.pretty (Dhall.Core.normalize expr) actualBytes = Data.Text.Lazy.Encoding.encodeUtf8 text @@ -866,7 +864,7 @@ where bytes = hashExpression expr - bytes16 = Data.ByteString.Base16.encode bytes + bytes16 = Data.ByteArray.convert bytes -- Notes that `decodeUtf8` is partial, but the base16-encoded bytestring -- should always successfully decode diff --git a/src/Dhall/Parser.hs b/src/Dhall/Parser.hs --- a/src/Dhall/Parser.hs +++ b/src/Dhall/Parser.hs @@ -44,7 +44,7 @@ import Text.Trifecta.Delta (Delta) import qualified Control.Monad -import qualified Data.ByteString.Base16.Lazy +import qualified Crypto.Hash import qualified Data.ByteString.Lazy import qualified Data.Char import qualified Data.HashMap.Strict.InsOrd @@ -56,7 +56,6 @@ 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 @@ _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 @@ 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 @@ -1510,10 +1509,9 @@ 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" + case Crypto.Hash.digestFromByteString (Data.ByteString.Lazy.toStrict lazyBytes) of + Nothing -> fail "Invalid sha256 hash" + Just h -> pure h import_ :: Parser Path import_ = (do diff --git a/src/Dhall/Pretty/Internal.hs b/src/Dhall/Pretty/Internal.hs --- a/src/Dhall/Pretty/Internal.hs +++ b/src/Dhall/Pretty/Internal.hs @@ -46,7 +46,6 @@ 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 @@ 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 (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 @@ <> " 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 (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) = diff --git a/src/Dhall/Tutorial.hs b/src/Dhall/Tutorial.hs --- a/src/Dhall/Tutorial.hs +++ b/src/Dhall/Tutorial.hs @@ -474,12 +474,12 @@ -- -- __Exercise:__ There is a @not@ function hosted online here: -- --- +-- -- -- Visit that link and read the documentation. Then try to guess what this -- code returns: -- --- > >>> input auto "https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Bool/not https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool +-- > >>> input auto "https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool -- > ??? -- -- Run the code to test your guess @@ -966,7 +966,7 @@ -- You can also use @let@ expressions to rename imports, like this: -- -- > $ dhall --- > let not = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Bool/not +-- > let not = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not -- > in not True -- > -- > Bool @@ -1115,7 +1115,7 @@ -- common pattern: -- -- > let MyType = constructors < Empty : {} | Person : { name : Text, age : Natural } > --- > in [ MyType.Empty {} +-- > in [ MyType.Empty {=} -- > , MyType.Person { name = "John", age = +23 } -- > , MyType.Person { name = "Amy" , age = +25 } -- > ] @@ -1324,7 +1324,7 @@ -- complex example: -- -- > $ dhall --- > let Prelude/List/map = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/map +-- > let Prelude/List/map = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/map -- > in λ(f : Integer → Integer) → Prelude/List/map Integer Integer f [1, 2, 3] -- > -- > ∀(f : Integer → Integer) → List Integer @@ -1348,11 +1348,11 @@ -- __Exercise__: The Dhall Prelude provides a @replicate@ function which you can -- find here: -- --- +-- -- -- Test what the following Dhall expression normalizes to: -- --- > let replicate = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate +-- > let replicate = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate -- > in replicate +10 -- -- __Exercise__: If you have a lot of spare time, try to \"break the compiler\" by @@ -1604,22 +1604,22 @@ -- normalizing them: -- -- > $ dhall-format --- > let replicate = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate +-- > let replicate = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate -- > in replicate +5 (List (List Integer)) (replicate +5 (List Integer) (replicate +5 Integer 1)) -- > -- > let replicate = --- > https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate +-- > https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate -- > -- > in replicate -- > +5 -- > (List (List Integer)) -- > (replicate +5 (List Integer) (replicate +5 Integer 1)) -- --- If you want to evaluate and format an expression then you can combine the --- @dhall@ and @dhall-format@ executables: +-- If you want to evaluate and format an expression then you can use the +-- @--pretty@ flag of the @dhall@ executable: -- --- > $ dhall | dhall-format --- > let replicate = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate +-- > $ dhall --pretty +-- > let replicate = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate -- > in replicate +5 (List (List Integer)) (replicate +5 (List Integer) (replicate +5 Integer 1)) -- > -- > List (List (List Integer)) @@ -2283,7 +2283,7 @@ -- -- Rules: -- --- > let Prelude/List/concat = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concat +-- > let Prelude/List/concat = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concat -- > -- > List/fold a (Prelude/List/concat a xss) b c -- > = List/fold (List a) xss b (λ(x : List a) → List/fold a x b c) @@ -2352,10 +2352,10 @@ -- -- Rules: -- --- > let Prelude/Optional/head = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Optional/head --- > let Prelude/List/concat = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concat --- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concatMap --- > let Prelude/List/map = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/map +-- > let Prelude/Optional/head = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Optional/head +-- > let Prelude/List/concat = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concat +-- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concatMap +-- > let Prelude/List/map = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/map -- > -- > List/head a (Prelude/List/concat a xss) = -- > Prelude/Optional/head a (Prelude/List/map (List a) (Optional a) (List/head a) xss) @@ -2383,10 +2383,10 @@ -- -- Rules: -- --- > let Prelude/Optional/last = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Optional/last --- > let Prelude/List/concat = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concat --- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concatMap --- > let Prelude/List/map = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/map +-- > let Prelude/Optional/last = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Optional/last +-- > let Prelude/List/concat = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concat +-- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concatMap +-- > let Prelude/List/map = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/map -- > -- > List/last a (Prelude/List/concat a xss) = -- > Prelude/Optional/last a (Prelude/List/map (List a) (Optional a) (List/last a) xss) @@ -2414,9 +2414,9 @@ -- -- Rules: -- --- > let Prelude/List/shifted = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/shifted --- > let Prelude/List/concat = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concat --- > let Prelude/List/map = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/map +-- > let Prelude/List/shifted = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/shifted +-- > let Prelude/List/concat = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concat +-- > let Prelude/List/map = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/map -- > -- > List/indexed a (Prelude/List/concat a xss) = -- > Prelude/List/shifted a (Prelude/List/map (List a) (List { index : Natural, value : a }) (List/indexed a) xss) @@ -2439,9 +2439,9 @@ -- -- Rules: -- --- > let Prelude/List/map = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/map --- > let Prelude/List/concat = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concat --- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concatMap +-- > let Prelude/List/map = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/map +-- > let Prelude/List/concat = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concat +-- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concatMap -- > -- > List/reverse a (Prelude/List/concat a xss) -- > = Prelude/List/concat a (List/reverse (List a) (Prelude/List/map (List a) (List a) (List/reverse a) xss)) @@ -2499,7 +2499,7 @@ -- -- ... which currenty redirects to: -- --- +-- -- -- There is nothing \"official\" or \"standard\" about this Prelude other than -- the fact that it is mentioned in this tutorial. The \"Prelude\" is just a @@ -2510,12 +2510,12 @@ -- subdirectories. For example, the @Bool@ subdirectory has a @not@ file -- located here: -- --- +-- -- -- The @not@ function is just a UTF8-encoded text file hosted online with the -- following contents -- --- > $ curl https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Bool/not +-- > $ curl https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not -- > {- -- > Flip the value of a `Bool` -- > @@ -2548,7 +2548,7 @@ -- You can use this @not@ function either directly: -- -- > $ dhall --- > https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Bool/not True +-- > https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not True -- > -- > Bool -- > @@ -2557,7 +2557,7 @@ -- ... or assign the URL to a shorter name: -- -- > $ dhall --- > let Bool/not = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Bool/not +-- > let Bool/not = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not -- > in Bool/not True -- > -- > Bool @@ -2568,7 +2568,7 @@ -- consistency and documentation, such as @Prelude\/Natural\/even@, which -- re-exports the built-in @Natural/even@ function: -- --- > $ curl https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Natural/even +-- > $ curl https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Natural/even -- > {- -- > Returns `True` if a number if even and returns `False` otherwise -- > @@ -2589,7 +2589,7 @@ -- using local relative paths instead of URLs. For example, you can use @wget@, -- like this: -- --- > $ wget -np -nH -r --cut-dirs=2 https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/ +-- > $ wget -np -nH -r --cut-dirs=2 https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/ -- > $ tree Prelude -- > Prelude -- > ├── Bool @@ -2653,15 +2653,36 @@ -- locally like this: -- -- > $ ipfs mount --- > $ cd /ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude +-- > $ cd /ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude -- -- Browse the Prelude online to learn more by seeing what functions are -- available and reading their inline documentation: -- --- +-- -- -- __Exercise__: Try to use a new Prelude function that has not been covered -- previously in this tutorial +-- +-- You can also import the entire Prelude as a single large record for +-- convenience: +-- +-- > $ dhall +-- > let Prelude = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/package.dhall +-- > +-- > in λ(x : Text) +-- > → Prelude.`List`.length Text (Prelude.`List`.replicate +10 Text x) +-- > +-- > ∀(x : Text) → Natural +-- > +-- > λ(x : Text) → +10 +-- +-- The organization of the package mirrors the layout of the Prelude, meaning +-- that every directory is stored as a record whose children are the fields of +-- that record. +-- +-- __Exercise__: Browse the Prelude by running: +-- +-- > $ dhall --pretty <<< 'https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/package.dhall' -- $conclusion -- diff --git a/src/Dhall/TypeCheck.hs b/src/Dhall/TypeCheck.hs --- a/src/Dhall/TypeCheck.hs +++ b/src/Dhall/TypeCheck.hs @@ -23,8 +23,8 @@ 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) @@ -35,16 +35,19 @@ import Dhall.Core (Const(..), Chunks(..), Expr(..), Var(..)) import Dhall.Context (Context) -import qualified Control.Monad.Trans.State.Strict as State -import qualified Data.HashMap.Strict +import qualified Data.Foldable import qualified Data.HashMap.Strict.InsOrd +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) @@ -55,75 +58,6 @@ rule Kind Kind = return Kind rule Kind Type = return Type -match :: Var -> Var -> [(Text, Text)] -> Bool -match (V xL nL) (V xR nR) [] = - xL == xR && nL == nR -match (V xL 0 ) (V xR 0 ) ((xL', xR'):_ ) - | xL == xL' && xR == xR' = True -match (V xL nL) (V xR nR) ((xL', xR'):xs) = - match (V xL nL') (V xR nR') xs - where - nL' = if xL == xL' then nL - 1 else nL - nR' = if xR == xR' then nR - 1 else nR - -toSortedList :: InsOrdHashMap k v -> [(k, v)] -toSortedList = - Data.HashMap.Strict.toList . Data.HashMap.Strict.InsOrd.toHashMap - -propEqual :: Eq a => Expr s a -> Expr t a -> Bool -propEqual eL0 eR0 = - State.evalState - (go (Dhall.Core.normalize eL0) (Dhall.Core.normalize eR0)) - [] - where - go (Const Type) (Const Type) = return True - go (Const Kind) (Const Kind) = return True - go (Var vL) (Var vR) = do - ctx <- State.get - return (match vL vR ctx) - go (Pi xL tL bL) (Pi xR tR bR) = do - ctx <- State.get - eq1 <- go tL tR - if eq1 - then do - State.put ((xL, xR):ctx) - eq2 <- go bL bR - State.put ctx - return eq2 - else return False - go (App fL aL) (App fR aR) = do - b1 <- go fL fR - if b1 then go aL aR else return False - go Bool Bool = return True - go Natural Natural = return True - go Integer Integer = return True - go Double Double = return True - go Text Text = return True - go List List = return True - go Optional Optional = return True - go (Record ktsL0) (Record ktsR0) = do - let loop ((kL, tL):ktsL) ((kR, tR):ktsR) - | kL == kR = do - b <- go tL tR - if b - then loop ktsL ktsR - else return False - loop [] [] = return True - loop _ _ = return False - loop (toSortedList ktsL0) (toSortedList ktsR0) - go (Union ktsL0) (Union ktsR0) = do - let loop ((kL, tL):ktsL) ((kR, tR):ktsR) - | kL == kR = do - b <- go tL tR - if b - then loop ktsL ktsR - else return False - loop [] [] = return True - loop _ _ = return False - loop (toSortedList ktsL0) (toSortedList ktsR0) - go (Embed eL) (Embed eR) = return (eL == eR) - go _ _ = return False - {-| Type-check an expression and return the expression's type if type-checking succeeds or an error if type-checking fails @@ -162,7 +96,7 @@ return a loop ctx (Lam x _A b ) = do _ <- loop ctx _A - let ctx' = fmap (Dhall.Core.shift 1 (V x 0)) (Dhall.Context.insert x _A ctx) + let ctx' = fmap (Dhall.Core.shift 1 (V x 0)) (Dhall.Context.insert x (Dhall.Core.normalize _A) ctx) _B <- loop ctx' b let p = Pi x _A _B _t <- loop ctx p @@ -174,7 +108,7 @@ _ -> Left (TypeError ctx e (InvalidInputType _A)) _ <- loop ctx _A - let ctx' = fmap (Dhall.Core.shift 1 (V x 0)) (Dhall.Context.insert x _A ctx) + let ctx' = fmap (Dhall.Core.shift 1 (V x 0)) (Dhall.Context.insert x (Dhall.Core.normalize _A) ctx) tB <- fmap Dhall.Core.normalize (loop ctx' _B) kB <- case tB of Const k -> return k @@ -189,7 +123,7 @@ Pi x _A _B -> return (x, _A, _B) _ -> Left (TypeError ctx e (NotAFunction f tf)) _A' <- loop ctx a - if propEqual _A _A' + if Dhall.Core.judgmentallyEqual _A _A' then do let a' = Dhall.Core.shift 1 (V x 0) a let _B' = Dhall.Core.subst (V x 0) a' _B @@ -206,7 +140,7 @@ _ <- loop ctx _A0 let nf_A0 = Dhall.Core.normalize _A0 let nf_A1 = Dhall.Core.normalize _A1 - if propEqual _A0 _A1 + if Dhall.Core.judgmentallyEqual _A0 _A1 then return () else Left (TypeError ctx e (AnnotMismatch a0 nf_A0 nf_A1)) Nothing -> return () @@ -219,7 +153,7 @@ _ <- loop ctx t t' <- loop ctx x - if propEqual t t' + if Dhall.Core.judgmentallyEqual t t' then do return t else do @@ -295,7 +229,7 @@ Const Type -> return () _ -> Left (TypeError ctx e (IfBranchMustBeTerm False z tz ttz)) - if propEqual ty tz + if Dhall.Core.judgmentallyEqual ty tz then return () else Left (TypeError ctx e (IfBranchMismatch y z ty tz)) return ty @@ -384,17 +318,16 @@ 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' + if Dhall.Core.judgmentallyEqual t t' then return () else do let nf_t = Dhall.Core.normalize t @@ -402,14 +335,15 @@ 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' + if Dhall.Core.judgmentallyEqual t t' then return () else do let nf_t = Dhall.Core.normalize t @@ -427,7 +361,7 @@ App List er -> return er _ -> Left (TypeError ctx e (CantListAppend r tr)) - if propEqual el er + if Dhall.Core.judgmentallyEqual el er then return (App List el) else Left (TypeError ctx e (ListAppendMismatch el er)) loop _ ListBuild = do @@ -466,13 +400,9 @@ 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' + if Dhall.Core.judgmentallyEqual t t' then return () else do let nf_t = Dhall.Core.normalize t @@ -527,7 +457,7 @@ Just _ -> Left (TypeError ctx e (DuplicateAlternative k)) Nothing -> return () t <- loop ctx v - let union = Union (Data.HashMap.Strict.InsOrd.insert k t kts) + let union = Union (Data.HashMap.Strict.InsOrd.insert k (Dhall.Core.normalize t) kts) _ <- loop ctx union return union loop ctx e@(Combine kvsX kvsY) = do @@ -600,10 +530,10 @@ Just tX -> case tX of Pi _ tY' t' -> do - if propEqual tY tY' + if Dhall.Core.judgmentallyEqual tY tY' then return () else Left (TypeError ctx e (HandlerInputTypeMismatch kY tY tY')) - if propEqual t t' + if Dhall.Core.judgmentallyEqual t t' then return () else Left (TypeError ctx e (InvalidHandlerOutputType kY t t')) _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX)) @@ -639,10 +569,10 @@ Just tX -> case tX of Pi _ tY' t' -> do - if propEqual tY tY' + if Dhall.Core.judgmentallyEqual tY tY' then return () else Left (TypeError ctx e (HandlerInputTypeMismatch kY tY tY')) - if propEqual t t' + if Dhall.Core.judgmentallyEqual t t' then return () else Left (TypeError ctx e (HandlerOutputTypeMismatch kX t kY t')) _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX)) @@ -710,7 +640,6 @@ | 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) @@ -1890,70 +1819,6 @@ txt0 = build expr0 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 diff --git a/tests/Examples.hs b/tests/Examples.hs deleted file mode 100644 --- a/tests/Examples.hs +++ /dev/null @@ -1,1070 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} - -module Examples where - -import qualified Test.Tasty -import qualified Test.Tasty.HUnit -import qualified Util - -import Test.Tasty (TestTree) - -exampleTests :: TestTree -exampleTests = - Test.Tasty.testGroup "examples" - [ Test.Tasty.testGroup "Bool" - [ Test.Tasty.testGroup "and" - [ _Bool_and_0 - , _Bool_and_1 - ] - , Test.Tasty.testGroup "build" - [ _Bool_build_0 - , _Bool_build_1 - ] - , Test.Tasty.testGroup "even" - [ _Bool_even_0 - , _Bool_even_1 - , _Bool_even_2 - , _Bool_even_3 - ] - , Test.Tasty.testGroup "fold" - [ _Bool_fold_0 - , _Bool_fold_1 - ] - , Test.Tasty.testGroup "not" - [ _Bool_not_0 - , _Bool_not_1 - ] - , Test.Tasty.testGroup "odd" - [ _Bool_odd_0 - , _Bool_odd_1 - , _Bool_odd_2 - , _Bool_odd_3 - ] - , Test.Tasty.testGroup "or" - [ _Bool_or_0 - , _Bool_or_1 - ] - , Test.Tasty.testGroup "show" - [ _Bool_show_0 - , _Bool_show_1 - ] - ] - , Test.Tasty.testGroup "Double" - [ Test.Tasty.testGroup "show" - [ _Double_show_0 - , _Double_show_1 - ] - ] - , Test.Tasty.testGroup "Integer" - [ Test.Tasty.testGroup "show" - [ _Integer_show_0 - , _Integer_show_1 - ] - ] - , Test.Tasty.testGroup "List" - [ Test.Tasty.testGroup "all" - [ _List_all_0 - , _List_all_1 - ] - , Test.Tasty.testGroup "any" - [ _List_any_0 - , _List_any_1 - ] - , Test.Tasty.testGroup "build" - [ _List_build_0 - , _List_build_1 - ] - , Test.Tasty.testGroup "concat" - [ _List_concat_0 - , _List_concat_1 - ] - , Test.Tasty.testGroup "concatMap" - [ _List_concatMap_0 - , _List_concatMap_1 - ] - , Test.Tasty.testGroup "filter" - [ _List_filter_0 - , _List_filter_1 - ] - , Test.Tasty.testGroup "fold" - [ _List_fold_0 - , _List_fold_1 - , _List_fold_2 - ] - , Test.Tasty.testGroup "generate" - [ _List_generate_0 - , _List_generate_1 - ] - , Test.Tasty.testGroup "head" - [ _List_head_0 - , _List_head_1 - ] - , Test.Tasty.testGroup "indexed" - [ _List_indexed_0 - , _List_indexed_1 - ] - , Test.Tasty.testGroup "iterate" - [ _List_iterate_0 - , _List_iterate_1 - ] - , Test.Tasty.testGroup "last" - [ _List_last_0 - , _List_last_1 - ] - , Test.Tasty.testGroup "length" - [ _List_length_0 - , _List_length_1 - ] - , Test.Tasty.testGroup "map" - [ _List_map_0 - , _List_map_1 - ] - , Test.Tasty.testGroup "null" - [ _List_null_0 - , _List_null_1 - ] - , Test.Tasty.testGroup "replicate" - [ _List_replicate_0 - , _List_replicate_1 - ] - , Test.Tasty.testGroup "reverse" - [ _List_reverse_0 - , _List_reverse_1 - ] - , Test.Tasty.testGroup "shifted" - [ _List_shifted_0 - , _List_shifted_1 - ] - , Test.Tasty.testGroup "unzip" - [ _List_unzip_0 - , _List_unzip_1 - ] - ] - , Test.Tasty.testGroup "Monoid" - [ _Monoid_00 - , _Monoid_01 - , _Monoid_02 - , _Monoid_03 - , _Monoid_04 - , _Monoid_05 - , _Monoid_06 - , _Monoid_07 - , _Monoid_08 - , _Monoid_09 - , _Monoid_10 - ] - , Test.Tasty.testGroup "Natural" - [ Test.Tasty.testGroup "build" - [ _Natural_build_0 - , _Natural_build_1 - ] - , Test.Tasty.testGroup "enumerate" - [ _Natural_enumerate_0 - , _Natural_enumerate_1 - ] - , Test.Tasty.testGroup "even" - [ _Natural_even_0 - , _Natural_even_1 - ] - , Test.Tasty.testGroup "fold" - [ _Natural_fold_0 - , _Natural_fold_1 - , _Natural_fold_2 - ] - , Test.Tasty.testGroup "isZero" - [ _Natural_isZero_0 - , _Natural_isZero_1 - ] - , Test.Tasty.testGroup "odd" - [ _Natural_odd_0 - , _Natural_odd_1 - ] - , Test.Tasty.testGroup "product" - [ _Natural_product_0 - , _Natural_product_1 - ] - , Test.Tasty.testGroup "show" - [ _Natural_show_0 - , _Natural_show_1 - ] - , Test.Tasty.testGroup "sum" - [ _Natural_sum_0 - , _Natural_sum_1 - ] - , Test.Tasty.testGroup "toInteger" - [ _Natural_toInteger_0 - , _Natural_toInteger_1 - ] - ] - , Test.Tasty.testGroup "Optional" - [ Test.Tasty.testGroup "all" - [ _Optional_all_0 - , _Optional_all_1 - ] - , Test.Tasty.testGroup "any" - [ _Optional_any_0 - , _Optional_any_1 - ] - , Test.Tasty.testGroup "build" - [ _Optional_build_0 - , _Optional_build_1 - ] - , Test.Tasty.testGroup "concat" - [ _Optional_concat_0 - , _Optional_concat_1 - , _Optional_concat_2 - ] - , Test.Tasty.testGroup "filter" - [ _Optional_filter_0 - , _Optional_filter_1 - ] - , Test.Tasty.testGroup "fold" - [ _Optional_fold_0 - , _Optional_fold_1 - ] - , Test.Tasty.testGroup "head" - [ _Optional_head_0 - , _Optional_head_1 - , _Optional_head_2 - ] - , Test.Tasty.testGroup "last" - [ _Optional_last_0 - , _Optional_last_1 - , _Optional_last_2 - ] - , Test.Tasty.testGroup "length" - [ _Optional_length_0 - , _Optional_length_1 - ] - , Test.Tasty.testGroup "null" - [ _Optional_null_0 - , _Optional_null_1 - ] - , Test.Tasty.testGroup "map" - [ _Optional_map_0 - , _Optional_map_1 - ] - , Test.Tasty.testGroup "toList" - [ _Optional_toList_0 - , _Optional_toList_1 - ] - , Test.Tasty.testGroup "unzip" - [ _Optional_unzip_0 - , _Optional_unzip_1 - ] - ] - , Test.Tasty.testGroup "Text" - [ Test.Tasty.testGroup "concat" - [ _Text_concat_0 - , _Text_concat_1 - ] - , Test.Tasty.testGroup "concatMap" - [ _Text_concatMap_0 - , _Text_concatMap_1 - ] - , Test.Tasty.testGroup "concatMapSep" - [ _Text_concatMapSep_0 - , _Text_concatMapSep_1 - ] - , Test.Tasty.testGroup "concatSep" - [ _Text_concatSep_0 - , _Text_concatSep_1 - ] - ] - ] - -_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)" - Util.assertNormalizesTo e "False" ) - -_Bool_and_1 :: TestTree -_Bool_and_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/Bool/and ([] : List Bool)" - Util.assertNormalizesTo e "True" ) - -_Bool_build_0 :: TestTree -_Bool_build_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code - "./Prelude/Bool/build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → true)" - Util.assertNormalizesTo e "True" ) - -_Bool_build_1 :: TestTree -_Bool_build_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code - "./Prelude/Bool/build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → false)" - Util.assertNormalizesTo e "False" ) - -_Bool_even_0 :: TestTree -_Bool_even_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./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)" - 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)" - Util.assertNormalizesTo e "False" ) - -_Bool_even_3 :: TestTree -_Bool_even_3 = Test.Tasty.HUnit.testCase "Example #3" (do - e <- Util.code "./Prelude/Bool/even ([] : List Bool)" - Util.assertNormalizesTo e "True" ) - -_Bool_fold_0 :: TestTree -_Bool_fold_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Bool/fold True Integer 0 1" - Util.assertNormalizesTo e "0" ) - -_Bool_fold_1 :: TestTree -_Bool_fold_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/Bool/fold False Integer 0 1" - Util.assertNormalizesTo e "1" ) - -_Bool_not_0 :: TestTree -_Bool_not_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Bool/not True" - Util.assertNormalizesTo e "False" ) - -_Bool_not_1 :: TestTree -_Bool_not_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/Bool/not False" - Util.assertNormalizesTo e "True" ) - -_Bool_odd_0 :: TestTree -_Bool_odd_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./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)" - 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)" - Util.assertNormalizesTo e "True" ) - -_Bool_odd_3 :: TestTree -_Bool_odd_3 = Test.Tasty.HUnit.testCase "Example #3" (do - e <- Util.code "./Prelude/Bool/odd ([] : List Bool)" - Util.assertNormalizesTo e "False" ) - -_Bool_or_0 :: TestTree -_Bool_or_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Bool/or ([ True, False, True ] : List Bool)" - Util.assertNormalizesTo e "True" ) - -_Bool_or_1 :: TestTree -_Bool_or_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/Bool/or ([] : List Bool)" - Util.assertNormalizesTo e "False" ) - -_Bool_show_0 :: TestTree -_Bool_show_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Bool/show True" - Util.assertNormalizesTo e "\"True\"" ) - -_Bool_show_1 :: TestTree -_Bool_show_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/Bool/show False" - Util.assertNormalizesTo e "\"False\"" ) - -_Double_show_0 :: TestTree -_Double_show_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Double/show -3.1" - Util.assertNormalizesTo e "\"-3.1\"" ) - -_Double_show_1 :: TestTree -_Double_show_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/Double/show 0.4" - Util.assertNormalizesTo e "\"0.4\"" ) - -_Integer_show_0 :: TestTree -_Integer_show_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Integer/show -3" - Util.assertNormalizesTo e "\"-3\"" ) - -_Integer_show_1 :: TestTree -_Integer_show_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/Integer/show 0" - Util.assertNormalizesTo e "\"0\"" ) - -_List_all_0 :: TestTree -_List_all_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/List/all Natural Natural/even ([ +2, +3, +5 ] : List Natural)" - Util.assertNormalizesTo e "False" ) - -_List_all_1 :: TestTree -_List_all_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/List/all Natural Natural/even ([] : List Natural)" - Util.assertNormalizesTo e "True" ) - -_List_any_0 :: TestTree -_List_any_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/List/any Natural Natural/even ([ +2, +3, +5 ] : List Natural)" - Util.assertNormalizesTo e "True" ) - -_List_any_1 :: TestTree -_List_any_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/List/any Natural Natural/even ([] : List Natural)" - Util.assertNormalizesTo e "False" ) - -_List_build_0 :: TestTree -_List_build_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code - "./Prelude/List/build \n\ - \Text \n\ - \( λ(list : Type) \n\ - \→ λ(cons : Text → list → list) \n\ - \→ λ(nil : list) \n\ - \→ cons \"ABC\" (cons \"DEF\" nil)\n\ - \) \n" - Util.assertNormalizesTo e "[ \"ABC\", \"DEF\" ] : List Text" ) - -_List_build_1 :: TestTree -_List_build_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code - "./Prelude/List/build \n\ - \Text \n\ - \( λ(list : Type) \n\ - \→ λ(cons : Text → list → list)\n\ - \→ λ(nil : list) \n\ - \→ nil \n\ - \) \n" - Util.assertNormalizesTo e "[] : List Text" ) - -_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" ) - -_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" - 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" ) - -_List_concatMap_1 :: TestTree -_List_concatMap_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code - "./Prelude/List/concatMap Natural Natural (λ(n : Natural) → [n, n]) ([] : List Natural)" - Util.assertNormalizesTo e "[] : List Natural" ) - -_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" ) - -_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" ) - -_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\ - \Natural \n\ - \(λ(x : Natural) → λ(y : Natural) → x + y)\n\ - \+0 \n" - Util.assertNormalizesTo e "+10" ) - -_List_fold_1 :: TestTree -_List_fold_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code - " λ(nil : Natural) \n\ - \→ ./Prelude/List/fold \n\ - \ Natural \n\ - \ ([ +2, +3, +5 ] : List Natural) \n\ - \ Natural \n\ - \ (λ(x : Natural) → λ(y : Natural) → x + y)\n\ - \ nil \n" - Util.assertNormalizesTo e "λ(nil : Natural) → +2 + +3 + +5 + nil" ) - -_List_fold_2 :: TestTree -_List_fold_2 = Test.Tasty.HUnit.testCase "Example #2" (do - e <- Util.code - " λ(list : Type) \n\ - \→ λ(cons : Natural → list → list) \n\ - \→ λ(nil : list) \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" ) - -_List_generate_1 :: TestTree -_List_generate_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/List/generate +0 Bool Natural/even" - Util.assertNormalizesTo e "[] : List Bool" ) - -_List_head_0 :: TestTree -_List_head_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/List/head Integer ([ 0, 1, 2 ] : List Integer)" - Util.assertNormalizesTo e "[ 0 ] : Optional Integer" ) - -_List_head_1 :: TestTree -_List_head_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/List/head Integer ([] : List Integer)" - Util.assertNormalizesTo e "[] : Optional Integer" ) - -_List_indexed_0 :: TestTree -_List_indexed_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/List/indexed Bool ([ True, False, True ] : List Bool)" - Util.assertNormalizesTo e "[ { index = +0, value = True }, { index = +1, value = False }, { index = +2, value = True } ] : List { index : Natural, value : Bool }" ) - -_List_indexed_1 :: TestTree -_List_indexed_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/List/indexed Bool ([] : List Bool)" - Util.assertNormalizesTo e "[] : List { index : Natural, value : Bool }" ) - -_List_iterate_0 :: TestTree -_List_iterate_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/List/iterate +10 Natural (λ(x : Natural) → x * +2) +1" - Util.assertNormalizesTo e "[ +1, +2, +4, +8, +16, +32, +64, +128, +256, +512 ] : List Natural" ) - -_List_iterate_1 :: TestTree -_List_iterate_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/List/iterate +0 Natural (λ(x : Natural) → x * +2) +1" - Util.assertNormalizesTo e "[] : List Natural" ) - -_List_last_0 :: TestTree -_List_last_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/List/last Integer ([ 0, 1, 2 ] : List Integer)" - Util.assertNormalizesTo e "[ 2 ] : Optional Integer" ) - -_List_last_1 :: TestTree -_List_last_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/List/last Integer ([] : List Integer)" - Util.assertNormalizesTo e "[] : Optional Integer" ) - -_List_length_0 :: TestTree -_List_length_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/List/length Integer ([ 0, 1, 2 ] : List Integer)" - Util.assertNormalizesTo e "+3" ) - -_List_length_1 :: TestTree -_List_length_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/List/length Integer ([] : List Integer)" - Util.assertNormalizesTo e "+0" ) - -_List_map_0 :: TestTree -_List_map_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code - "./Prelude/List/map Natural Bool Natural/even ([ +2, +3, +5 ] : List Natural)" - Util.assertNormalizesTo e "[ True, False, False ] : List Bool" ) - -_List_map_1 :: TestTree -_List_map_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/List/map Natural Bool Natural/even ([] : List Natural)" - Util.assertNormalizesTo e "[] : List Bool" ) - -_List_null_0 :: TestTree -_List_null_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/List/null Integer ([ 0, 1, 2 ] : List Integer)" - Util.assertNormalizesTo e "False" ) - -_List_null_1 :: TestTree -_List_null_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/List/null Integer ([] : List Integer)" - Util.assertNormalizesTo e "True" ) - -_List_replicate_0 :: TestTree -_List_replicate_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/List/replicate +9 Integer 1" - Util.assertNormalizesTo e "[ 1, 1, 1, 1, 1, 1, 1, 1, 1 ] : List Integer" ) - -_List_replicate_1 :: TestTree -_List_replicate_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/List/replicate +0 Integer 1" - Util.assertNormalizesTo e "[] : List Integer" ) - -_List_reverse_0 :: TestTree -_List_reverse_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/List/reverse Integer ([0, 1, 2] : List Integer)" - Util.assertNormalizesTo e "[ 2, 1, 0 ] : List Integer" ) - -_List_reverse_1 :: TestTree -_List_reverse_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/List/reverse Integer ([] : List Integer)" - Util.assertNormalizesTo e "[] : List Integer" ) - -_List_shifted_0 :: TestTree -_List_shifted_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code - "./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 }" ) - -_List_shifted_1 :: TestTree -_List_shifted_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code - "./Prelude/List/shifted Bool ([] : List (List { index : Natural, value : Bool }))" - Util.assertNormalizesTo e "[] : List { index : Natural, value : Bool }" ) - -_List_unzip_0 :: TestTree -_List_unzip_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code - "./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 }" ) - -_List_unzip_1 :: TestTree -_List_unzip_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/List/unzip Text Bool ([] : List { _1 : Text, _2 : Bool })" - Util.assertNormalizesTo e "{ _1 = [] : List Text, _2 = [] : List Bool }" ) - -_Monoid_00 :: TestTree -_Monoid_00 = Test.Tasty.HUnit.testCase "Example #0" - (Util.assertTypeChecks "./Prelude/Bool/and : ./Prelude/Monoid Bool") - -_Monoid_01 :: TestTree -_Monoid_01 = Test.Tasty.HUnit.testCase "Example #1" - (Util.assertTypeChecks "./Prelude/Bool/or : ./Prelude/Monoid Bool") - -_Monoid_02 :: TestTree -_Monoid_02 = Test.Tasty.HUnit.testCase "Example #2" - (Util.assertTypeChecks "./Prelude/Bool/even : ./Prelude/Monoid Bool") - -_Monoid_03 :: TestTree -_Monoid_03 = Test.Tasty.HUnit.testCase "Example #3" - (Util.assertTypeChecks "./Prelude/Bool/odd : ./Prelude/Monoid Bool") - -_Monoid_04 :: TestTree -_Monoid_04 = Test.Tasty.HUnit.testCase "Example #4" - (Util.assertTypeChecks - "./Prelude/List/concat : ∀(a : Type) → ./Prelude/Monoid (List a)" ) - -_Monoid_05 :: TestTree -_Monoid_05 = Test.Tasty.HUnit.testCase "Example #5" - (Util.assertTypeChecks - "./Prelude/List/shifted \n\ - \ : ∀(a : Type) → ./Prelude/Monoid (List { index : Natural, value : a })\n" ) - -_Monoid_06 :: TestTree -_Monoid_06 = Test.Tasty.HUnit.testCase "Example #6" - (Util.assertTypeChecks "./Prelude/Natural/sum : ./Prelude/Monoid Natural") - -_Monoid_07 :: TestTree -_Monoid_07 = Test.Tasty.HUnit.testCase "Example #7" - (Util.assertTypeChecks "./Prelude/Natural/product : ./Prelude/Monoid Natural") - -_Monoid_08 :: TestTree -_Monoid_08 = Test.Tasty.HUnit.testCase "Example #8" - (Util.assertTypeChecks - "./Prelude/Optional/head : ∀(a : Type) → ./Prelude/Monoid (Optional a)" ) - -_Monoid_09 :: TestTree -_Monoid_09 = Test.Tasty.HUnit.testCase "Example #9" - (Util.assertTypeChecks - "./Prelude/Optional/last : ∀(a : Type) → ./Prelude/Monoid (Optional a)" ) - -_Monoid_10 :: TestTree -_Monoid_10 = Test.Tasty.HUnit.testCase "Example #10" - (Util.assertTypeChecks "./Prelude/Text/concat : ./Prelude/Monoid Text") - -_Natural_build_0 :: TestTree -_Natural_build_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code - "./Prelude/Natural/build \n\ - \( λ(natural : Type) \n\ - \→ λ(succ : natural → natural)\n\ - \→ λ(zero : natural) \n\ - \→ succ (succ (succ zero)) \n\ - \) \n" - Util.assertNormalizesTo e "+3" ) - -_Natural_build_1 :: TestTree -_Natural_build_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code - "./Prelude/Natural/build \n\ - \( λ(natural : Type) \n\ - \→ λ(succ : natural → natural)\n\ - \→ λ(zero : natural) \n\ - \→ zero \n\ - \) \n" - Util.assertNormalizesTo e "+0" ) - -_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" ) - -_Natural_enumerate_1 :: TestTree -_Natural_enumerate_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/Natural/enumerate +0" - Util.assertNormalizesTo e "[] : List Natural" ) - -_Natural_even_0 :: TestTree -_Natural_even_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Natural/even +3" - Util.assertNormalizesTo e "False" ) - -_Natural_even_1 :: TestTree -_Natural_even_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/Natural/even +0" - Util.assertNormalizesTo e "True" ) - -_Natural_fold_0 :: TestTree -_Natural_fold_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Natural/fold +3 Natural (λ(x : Natural) → +5 * x) +1" - Util.assertNormalizesTo e "+125" ) - -_Natural_fold_1 :: TestTree -_Natural_fold_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code - "λ(zero : Natural) → ./Prelude/Natural/fold +3 Natural (λ(x : Natural) → +5 * x) zero" - Util.assertNormalizesTo e "λ(zero : Natural) → +5 * +5 * +5 * zero" ) - -_Natural_fold_2 :: TestTree -_Natural_fold_2 = Test.Tasty.HUnit.testCase "Example #2" (do - e <- Util.code - " λ(natural : Type) \n\ - \→ λ(succ : natural → natural) \n\ - \→ λ(zero : natural) \n\ - \→ ./Prelude/Natural/fold +3 natural succ zero\n" - Util.assertNormalizesTo e "λ(natural : Type) → λ(succ : natural → natural) → λ(zero : natural) → succ (succ (succ zero))" ) - -_Natural_isZero_0 :: TestTree -_Natural_isZero_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Natural/isZero +2" - Util.assertNormalizesTo e "False" ) - -_Natural_isZero_1 :: TestTree -_Natural_isZero_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/Natural/isZero +0" - Util.assertNormalizesTo e "True" ) - -_Natural_odd_0 :: TestTree -_Natural_odd_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Natural/odd +3" - Util.assertNormalizesTo e "True" ) - -_Natural_odd_1 :: TestTree -_Natural_odd_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/Natural/odd +0" - Util.assertNormalizesTo e "False" ) - -_Natural_product_0 :: TestTree -_Natural_product_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Natural/product ([ +2, +3, +5 ] : List Natural)" - Util.assertNormalizesTo e "+30" ) - -_Natural_product_1 :: TestTree -_Natural_product_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/Natural/product ([] : List Natural)" - Util.assertNormalizesTo e "+1" ) - -_Natural_show_0 :: TestTree -_Natural_show_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Natural/show +3" - Util.assertNormalizesTo e "\"+3\"" ) - -_Natural_show_1 :: TestTree -_Natural_show_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/Natural/show +0" - Util.assertNormalizesTo e "\"+0\"" ) - -_Natural_sum_0 :: TestTree -_Natural_sum_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Natural/sum ([ +2, +3, +5 ] : List Natural)" - Util.assertNormalizesTo e "+10" ) - -_Natural_sum_1 :: TestTree -_Natural_sum_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/Natural/sum ([] : List Natural)" - Util.assertNormalizesTo e "+0" ) - -_Natural_toInteger_0 :: TestTree -_Natural_toInteger_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Natural/toInteger +3" - Util.assertNormalizesTo e "3" ) - -_Natural_toInteger_1 :: TestTree -_Natural_toInteger_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/Natural/toInteger +0" - Util.assertNormalizesTo e "0" ) - -_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)" - Util.assertNormalizesTo e "False" ) - -_Optional_all_1 :: TestTree -_Optional_all_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/Optional/all Natural Natural/even ([] : Optional Natural)" - Util.assertNormalizesTo e "True" ) - -_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)" - Util.assertNormalizesTo e "True" ) - -_Optional_any_1 :: TestTree -_Optional_any_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/Optional/any Natural Natural/even ([] : Optional Natural)" - Util.assertNormalizesTo e "False" ) - -_Optional_build_0 :: TestTree -_Optional_build_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code - "./Prelude/Optional/build \n\ - \Integer \n\ - \( λ(optional : Type) \n\ - \→ λ(just : Integer → optional)\n\ - \→ λ(nothing : optional) \n\ - \→ just 1 \n\ - \) \n" - Util.assertNormalizesTo e "[ 1 ] : Optional Integer" ) - -_Optional_build_1 :: TestTree -_Optional_build_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code - "./Prelude/Optional/build \n\ - \Integer \n\ - \( λ(optional : Type) \n\ - \→ λ(just : Integer → optional)\n\ - \→ λ(nothing : optional) \n\ - \→ nothing \n\ - \) \n" - Util.assertNormalizesTo e "[] : Optional Integer" ) - -_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" ) - -_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))" - Util.assertNormalizesTo e "[] : Optional Integer" ) - -_Optional_concat_2 :: TestTree -_Optional_concat_2 = Test.Tasty.HUnit.testCase "Example #2" (do - e <- Util.code "./Prelude/Optional/concat Integer ([] : Optional (Optional Integer))" - Util.assertNormalizesTo e "[] : Optional Integer" ) - -_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" ) - -_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)" - 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" - Util.assertNormalizesTo e "2" ) - -_Optional_fold_1 :: TestTree -_Optional_fold_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code - "./Prelude/Optional/fold Integer ([] : Optional Integer) Integer (λ(x : Integer) → x) 0" - Util.assertNormalizesTo e "0" ) - -_Optional_head_0 :: TestTree -_Optional_head_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code - "./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" - Util.assertNormalizesTo e "[] : Optional Integer" ) - -_Optional_head_2 :: TestTree -_Optional_head_2 = Test.Tasty.HUnit.testCase "Example #2" (do - e <- Util.code "./Prelude/Optional/head Integer ([] : List (Optional Integer))" - Util.assertNormalizesTo e "[] : Optional Integer" ) - -_Optional_last_0 :: TestTree -_Optional_last_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code - "./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" - Util.assertNormalizesTo e "[] : Optional Integer" ) - -_Optional_last_2 :: TestTree -_Optional_last_2 = Test.Tasty.HUnit.testCase "Example #2" (do - e <- Util.code "./Prelude/Optional/last Integer ([] : List (Optional Integer))" - Util.assertNormalizesTo e "[] : Optional Integer" ) - -_Optional_map_0 :: TestTree -_Optional_map_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code - "./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)" - Util.assertNormalizesTo e "+1" ) - -_Optional_length_1 :: TestTree -_Optional_length_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/Optional/length Integer ([] : Optional Integer)" - Util.assertNormalizesTo e "+0" ) - -_Optional_null_0 :: TestTree -_Optional_null_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Optional/null Integer ([ 2] : Optional Integer)" - Util.assertNormalizesTo e "False" ) - -_Optional_null_1 :: TestTree -_Optional_null_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/Optional/null Integer ([] : Optional Integer)" - Util.assertNormalizesTo e "True" ) - -_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 ]" ) - -_Optional_toList_1 :: TestTree -_Optional_toList_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/Optional/toList Integer ([] : Optional Integer)" - Util.assertNormalizesTo e "[] : List Integer" ) - -_Optional_unzip_0 :: TestTree -_Optional_unzip_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code - "./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 - e <- Util.code - "./Prelude/Optional/unzip Text Bool ([] : Optional { _1 : Text, _2 : Bool })" - Util.assertNormalizesTo e "{ _1 = [] : Optional Text, _2 = [] : Optional Bool }" ) - -_Text_concat_0 :: TestTree -_Text_concat_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Text/concat ([ \"ABC\", \"DEF\", \"GHI\" ] : List Text)" - Util.assertNormalizesTo e "\"ABCDEFGHI\"" ) - -_Text_concat_1 :: TestTree -_Text_concat_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/Text/concat ([] : List Text)" - Util.assertNormalizesTo e "\"\"" ) - -_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 ]" - Util.assertNormalizesTo e "\"0 1 2 \"" ) - -_Text_concatMap_1 :: TestTree -_Text_concatMap_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code - "./Prelude/Text/concatMap Integer (λ(n : Integer) → \"${Integer/show n} \") ([] : List Integer)" - Util.assertNormalizesTo e "\"\"" ) - -_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 ]" - Util.assertNormalizesTo e "\"0, 1, 2\"" ) - -_Text_concatMapSep_1 :: TestTree -_Text_concatMapSep_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code - "./Prelude/Text/concatMapSep \", \" Integer Integer/show ([] : List Integer)" - Util.assertNormalizesTo e "\"\"" ) - -_Text_concatSep_0 :: TestTree -_Text_concatSep_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code "./Prelude/Text/concatSep \", \" [ \"ABC\", \"DEF\", \"GHI\" ]" - Util.assertNormalizesTo e "\"ABC, DEF, GHI\"" ) - -_Text_concatSep_1 :: TestTree -_Text_concatSep_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code "./Prelude/Text/concatSep \", \" ([] : List Text)" - Util.assertNormalizesTo e "\"\"" ) diff --git a/tests/Normalization.hs b/tests/Normalization.hs --- a/tests/Normalization.hs +++ b/tests/Normalization.hs @@ -24,11 +24,145 @@ normalizationTests :: TestTree normalizationTests = testGroup "normalization" - [ constantFolding + [ examples + , simplifications + , constantFolding , conversions , shouldNormalize "Optional build/fold fusion" "optionalBuildFold" , customization , shouldNormalize "a remote-systems.conf builder" "remoteSystems" + ] + +examples :: TestTree +examples = + testGroup "Prelude examples" + [ shouldNormalize "Bool/and" "./examples/Bool/and/0" + , shouldNormalize "Bool/and" "./examples/Bool/and/1" + , shouldNormalize "Bool/build" "./examples/Bool/build/0" + , shouldNormalize "Bool/build" "./examples/Bool/build/1" + , shouldNormalize "Bool/even" "./examples/Bool/even/0" + , shouldNormalize "Bool/even" "./examples/Bool/even/1" + , shouldNormalize "Bool/even" "./examples/Bool/even/2" + , shouldNormalize "Bool/even" "./examples/Bool/even/3" + , shouldNormalize "Bool/fold" "./examples/Bool/fold/0" + , shouldNormalize "Bool/fold" "./examples/Bool/fold/1" + , shouldNormalize "Bool/not" "./examples/Bool/not/0" + , shouldNormalize "Bool/not" "./examples/Bool/not/1" + , shouldNormalize "Bool/odd" "./examples/Bool/odd/0" + , shouldNormalize "Bool/odd" "./examples/Bool/odd/1" + , shouldNormalize "Bool/odd" "./examples/Bool/odd/2" + , shouldNormalize "Bool/odd" "./examples/Bool/odd/3" + , shouldNormalize "Bool/or" "./examples/Bool/or/0" + , shouldNormalize "Bool/or" "./examples/Bool/or/1" + , shouldNormalize "Bool/show" "./examples/Bool/show/0" + , shouldNormalize "Bool/show" "./examples/Bool/show/1" + , shouldNormalize "Double/show" "./examples/Double/show/0" + , shouldNormalize "Double/show" "./examples/Double/show/1" + , shouldNormalize "Integer/show" "./examples/Integer/show/0" + , shouldNormalize "Integer/show" "./examples/Integer/show/1" + , shouldNormalize "List/all" "./examples/List/all/0" + , shouldNormalize "List/all" "./examples/List/all/1" + , shouldNormalize "List/any" "./examples/List/any/0" + , shouldNormalize "List/any" "./examples/List/any/1" + , shouldNormalize "List/build" "./examples/List/build/0" + , shouldNormalize "List/build" "./examples/List/build/1" + , shouldNormalize "List/concat" "./examples/List/concat/0" + , shouldNormalize "List/concat" "./examples/List/concat/1" + , shouldNormalize "List/concatMap" "./examples/List/concatMap/0" + , shouldNormalize "List/concatMap" "./examples/List/concatMap/1" + , shouldNormalize "List/filter" "./examples/List/filter/0" + , shouldNormalize "List/filter" "./examples/List/filter/1" + , shouldNormalize "List/fold" "./examples/List/fold/0" + , shouldNormalize "List/fold" "./examples/List/fold/1" + , shouldNormalize "List/fold" "./examples/List/fold/2" + , shouldNormalize "List/generate" "./examples/List/generate/0" + , shouldNormalize "List/generate" "./examples/List/generate/1" + , shouldNormalize "List/head" "./examples/List/head/0" + , shouldNormalize "List/head" "./examples/List/head/1" + , shouldNormalize "List/iterate" "./examples/List/iterate/0" + , shouldNormalize "List/iterate" "./examples/List/iterate/1" + , shouldNormalize "List/last" "./examples/List/last/0" + , shouldNormalize "List/last" "./examples/List/last/1" + , shouldNormalize "List/length" "./examples/List/length/0" + , shouldNormalize "List/length" "./examples/List/length/1" + , shouldNormalize "List/map" "./examples/List/map/0" + , shouldNormalize "List/map" "./examples/List/map/1" + , shouldNormalize "List/null" "./examples/List/null/0" + , shouldNormalize "List/null" "./examples/List/null/1" + , shouldNormalize "List/replicate" "./examples/List/replicate/0" + , shouldNormalize "List/replicate" "./examples/List/replicate/1" + , shouldNormalize "List/reverse" "./examples/List/reverse/0" + , shouldNormalize "List/reverse" "./examples/List/reverse/1" + , shouldNormalize "List/shifted" "./examples/List/shifted/0" + , shouldNormalize "List/shifted" "./examples/List/shifted/1" + , shouldNormalize "List/unzip" "./examples/List/unzip/0" + , shouldNormalize "List/unzip" "./examples/List/unzip/1" + , shouldNormalize "Natural/build" "./examples/Natural/build/0" + , shouldNormalize "Natural/build" "./examples/Natural/build/1" + , shouldNormalize "Natural/enumerate" "./examples/Natural/enumerate/0" + , shouldNormalize "Natural/enumerate" "./examples/Natural/enumerate/1" + , shouldNormalize "Natural/even" "./examples/Natural/even/0" + , shouldNormalize "Natural/even" "./examples/Natural/even/1" + , shouldNormalize "Natural/fold" "./examples/Natural/fold/0" + , shouldNormalize "Natural/fold" "./examples/Natural/fold/1" + , shouldNormalize "Natural/fold" "./examples/Natural/fold/2" + , shouldNormalize "Natural/isZero" "./examples/Natural/isZero/0" + , shouldNormalize "Natural/isZero" "./examples/Natural/isZero/1" + , shouldNormalize "Natural/odd" "./examples/Natural/odd/0" + , shouldNormalize "Natural/odd" "./examples/Natural/odd/1" + , shouldNormalize "Natural/product" "./examples/Natural/product/0" + , shouldNormalize "Natural/product" "./examples/Natural/product/1" + , shouldNormalize "Natural/show" "./examples/Natural/show/0" + , shouldNormalize "Natural/show" "./examples/Natural/show/1" + , shouldNormalize "Natural/sum" "./examples/Natural/sum/0" + , shouldNormalize "Natural/sum" "./examples/Natural/sum/1" + , shouldNormalize "Natural/toInteger" "./examples/Natural/toInteger/0" + , shouldNormalize "Natural/toInteger" "./examples/Natural/toInteger/1" + , shouldNormalize "Optional/all" "./examples/Optional/all/0" + , shouldNormalize "Optional/all" "./examples/Optional/all/1" + , shouldNormalize "Optional/any" "./examples/Optional/any/0" + , shouldNormalize "Optional/any" "./examples/Optional/any/1" + , shouldNormalize "Optional/build" "./examples/Optional/build/0" + , shouldNormalize "Optional/build" "./examples/Optional/build/1" + , shouldNormalize "Optional/concat" "./examples/Optional/concat/0" + , shouldNormalize "Optional/concat" "./examples/Optional/concat/1" + , shouldNormalize "Optional/concat" "./examples/Optional/concat/2" + , shouldNormalize "Optional/filter" "./examples/Optional/filter/0" + , shouldNormalize "Optional/filter" "./examples/Optional/filter/1" + , shouldNormalize "Optional/fold" "./examples/Optional/fold/0" + , shouldNormalize "Optional/fold" "./examples/Optional/fold/1" + , shouldNormalize "Optional/head" "./examples/Optional/head/0" + , shouldNormalize "Optional/head" "./examples/Optional/head/1" + , shouldNormalize "Optional/last" "./examples/Optional/last/0" + , shouldNormalize "Optional/last" "./examples/Optional/last/1" + , shouldNormalize "Optional/length" "./examples/Optional/length/0" + , shouldNormalize "Optional/length" "./examples/Optional/length/1" + , shouldNormalize "Optional/map" "./examples/Optional/map/0" + , shouldNormalize "Optional/map" "./examples/Optional/map/1" + , shouldNormalize "Optional/null" "./examples/Optional/null/0" + , shouldNormalize "Optional/null" "./examples/Optional/null/1" + , shouldNormalize "Optional/toList" "./examples/Optional/toList/0" + , shouldNormalize "Optional/toList" "./examples/Optional/toList/1" + , shouldNormalize "Optional/unzip" "./examples/Optional/unzip/0" + , shouldNormalize "Optional/unzip" "./examples/Optional/unzip/1" + , shouldNormalize "Text/concat" "./examples/Text/concat/0" + , shouldNormalize "Text/concat" "./examples/Text/concat/1" + , shouldNormalize "Text/concatMap" "./examples/Text/concatMap/0" + , shouldNormalize "Text/concatMap" "./examples/Text/concatMap/1" + , shouldNormalize "Text/concatMapSep" "./examples/Text/concatMapSep/0" + , shouldNormalize "Text/concatMapSep" "./examples/Text/concatMapSep/1" + , shouldNormalize "Text/concatSep" "./examples/Text/concatSep/0" + , shouldNormalize "Text/concatSep" "./examples/Text/concatSep/1" + ] + +simplifications :: TestTree +simplifications = + testGroup "Simplifications" + [ shouldNormalize "if/then/else" "./simplifications/ifThenElse" + , shouldNormalize "||" "./simplifications/or" + , shouldNormalize "&&" "./simplifications/and" + , shouldNormalize "==" "./simplifications/eq" + , shouldNormalize "!=" "./simplifications/ne" ] constantFolding :: TestTree diff --git a/tests/Tests.hs b/tests/Tests.hs --- a/tests/Tests.hs +++ b/tests/Tests.hs @@ -1,7 +1,6 @@ module Main where import Normalization (normalizationTests) -import Examples (exampleTests) import Parser (parserTests) import Regression (regressionTests) import Tutorial (tutorialTests) @@ -13,7 +12,6 @@ allTests = testGroup "Dhall Tests" [ normalizationTests - , exampleTests , parserTests , regressionTests , tutorialTests diff --git a/tests/TypeCheck.hs b/tests/TypeCheck.hs --- a/tests/TypeCheck.hs +++ b/tests/TypeCheck.hs @@ -4,8 +4,6 @@ import Data.Monoid (mempty, (<>)) import Data.Text.Lazy (Text) -import Dhall.Core (Expr) -import Dhall.TypeCheck (X) import Test.Tasty (TestTree) import qualified Control.Exception @@ -20,12 +18,28 @@ typecheckTests :: TestTree typecheckTests = Test.Tasty.testGroup "typecheck tests" - [ should + [ Test.Tasty.testGroup "Prelude examples" + [ should "Monoid" "./examples/Monoid/00" + , should "Monoid" "./examples/Monoid/01" + , should "Monoid" "./examples/Monoid/02" + , should "Monoid" "./examples/Monoid/03" + , should "Monoid" "./examples/Monoid/04" + , should "Monoid" "./examples/Monoid/05" + , should "Monoid" "./examples/Monoid/06" + , should "Monoid" "./examples/Monoid/07" + , should "Monoid" "./examples/Monoid/08" + , should "Monoid" "./examples/Monoid/09" + , should "Monoid" "./examples/Monoid/10" + ] + , should "allow type-valued fields in a record" "fieldsAreTypes" , should "allow type-valued alternatives in a union" "alternativesAreTypes" + , should + "allow anonymous functions in types to be judgmentally equal" + "anonymousFunctionsInTypes" ] should :: Text -> Text -> TestTree @@ -37,17 +51,13 @@ actualExpr <- case Dhall.Parser.exprFromText mempty actualCode of Left err -> Control.Exception.throwIO err Right expr -> return expr - actualResolved <- Dhall.Import.load actualExpr - actualType <- case Dhall.TypeCheck.typeOf actualResolved of - Left err -> Control.Exception.throwIO err - Right expr -> return expr - let actualNormalized = Dhall.Core.normalize actualType :: Expr X X - expectedExpr <- case Dhall.Parser.exprFromText mempty expectedCode of Left err -> Control.Exception.throwIO err Right expr -> return expr - expectedResolved <- Dhall.Import.load expectedExpr - let expectedNormalized = Dhall.Core.normalize expectedResolved - let message = "The expression's type did not match the expected type" - Test.Tasty.HUnit.assertEqual message expectedNormalized actualNormalized + let annotatedExpr = Dhall.Core.Annot actualExpr expectedExpr + + resolvedExpr <- Dhall.Import.load annotatedExpr + case Dhall.TypeCheck.typeOf resolvedExpr of + Left err -> Control.Exception.throwIO err + Right _ -> return () diff --git a/tests/normalization/examples/Bool/and/0A.dhall b/tests/normalization/examples/Bool/and/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/and/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Bool/and [ True, False, True ] diff --git a/tests/normalization/examples/Bool/and/0B.dhall b/tests/normalization/examples/Bool/and/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/and/0B.dhall @@ -0,0 +1,1 @@ +False diff --git a/tests/normalization/examples/Bool/and/1A.dhall b/tests/normalization/examples/Bool/and/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/and/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Bool/and ([] : List Bool) diff --git a/tests/normalization/examples/Bool/and/1B.dhall b/tests/normalization/examples/Bool/and/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/and/1B.dhall @@ -0,0 +1,1 @@ +True diff --git a/tests/normalization/examples/Bool/build/0A.dhall b/tests/normalization/examples/Bool/build/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/build/0A.dhall @@ -0,0 +1,2 @@ +../../../../../Prelude/Bool/build +(λ(bool : Type) → λ(true : bool) → λ(false : bool) → true) diff --git a/tests/normalization/examples/Bool/build/0B.dhall b/tests/normalization/examples/Bool/build/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/build/0B.dhall @@ -0,0 +1,1 @@ +True diff --git a/tests/normalization/examples/Bool/build/1A.dhall b/tests/normalization/examples/Bool/build/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/build/1A.dhall @@ -0,0 +1,2 @@ +../../../../../Prelude/Bool/build +(λ(bool : Type) → λ(true : bool) → λ(false : bool) → false) diff --git a/tests/normalization/examples/Bool/build/1B.dhall b/tests/normalization/examples/Bool/build/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/build/1B.dhall @@ -0,0 +1,1 @@ +False diff --git a/tests/normalization/examples/Bool/even/0A.dhall b/tests/normalization/examples/Bool/even/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/even/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Bool/even [ False, True, False ] diff --git a/tests/normalization/examples/Bool/even/0B.dhall b/tests/normalization/examples/Bool/even/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/even/0B.dhall @@ -0,0 +1,1 @@ +True diff --git a/tests/normalization/examples/Bool/even/1A.dhall b/tests/normalization/examples/Bool/even/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/even/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Bool/even [ False, True ] diff --git a/tests/normalization/examples/Bool/even/1B.dhall b/tests/normalization/examples/Bool/even/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/even/1B.dhall @@ -0,0 +1,1 @@ +False diff --git a/tests/normalization/examples/Bool/even/2A.dhall b/tests/normalization/examples/Bool/even/2A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/even/2A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Bool/even [ False ] diff --git a/tests/normalization/examples/Bool/even/2B.dhall b/tests/normalization/examples/Bool/even/2B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/even/2B.dhall @@ -0,0 +1,1 @@ +False diff --git a/tests/normalization/examples/Bool/even/3A.dhall b/tests/normalization/examples/Bool/even/3A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/even/3A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Bool/even ([] : List Bool) diff --git a/tests/normalization/examples/Bool/even/3B.dhall b/tests/normalization/examples/Bool/even/3B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/even/3B.dhall @@ -0,0 +1,1 @@ +True diff --git a/tests/normalization/examples/Bool/fold/0A.dhall b/tests/normalization/examples/Bool/fold/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/fold/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Bool/fold True Integer 0 1 diff --git a/tests/normalization/examples/Bool/fold/0B.dhall b/tests/normalization/examples/Bool/fold/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/fold/0B.dhall @@ -0,0 +1,1 @@ +0 diff --git a/tests/normalization/examples/Bool/fold/1A.dhall b/tests/normalization/examples/Bool/fold/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/fold/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Bool/fold False Integer 0 1 diff --git a/tests/normalization/examples/Bool/fold/1B.dhall b/tests/normalization/examples/Bool/fold/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/fold/1B.dhall @@ -0,0 +1,1 @@ +1 diff --git a/tests/normalization/examples/Bool/not/0A.dhall b/tests/normalization/examples/Bool/not/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/not/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Bool/not True diff --git a/tests/normalization/examples/Bool/not/0B.dhall b/tests/normalization/examples/Bool/not/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/not/0B.dhall @@ -0,0 +1,1 @@ +False diff --git a/tests/normalization/examples/Bool/not/1A.dhall b/tests/normalization/examples/Bool/not/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/not/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Bool/not False diff --git a/tests/normalization/examples/Bool/not/1B.dhall b/tests/normalization/examples/Bool/not/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/not/1B.dhall @@ -0,0 +1,1 @@ +True diff --git a/tests/normalization/examples/Bool/odd/0A.dhall b/tests/normalization/examples/Bool/odd/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/odd/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Bool/odd [ True, False, True ] diff --git a/tests/normalization/examples/Bool/odd/0B.dhall b/tests/normalization/examples/Bool/odd/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/odd/0B.dhall @@ -0,0 +1,1 @@ +False diff --git a/tests/normalization/examples/Bool/odd/1A.dhall b/tests/normalization/examples/Bool/odd/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/odd/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Bool/odd [ True, False ] diff --git a/tests/normalization/examples/Bool/odd/1B.dhall b/tests/normalization/examples/Bool/odd/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/odd/1B.dhall @@ -0,0 +1,1 @@ +True diff --git a/tests/normalization/examples/Bool/odd/2A.dhall b/tests/normalization/examples/Bool/odd/2A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/odd/2A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Bool/odd [ True ] diff --git a/tests/normalization/examples/Bool/odd/2B.dhall b/tests/normalization/examples/Bool/odd/2B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/odd/2B.dhall @@ -0,0 +1,1 @@ +True diff --git a/tests/normalization/examples/Bool/odd/3A.dhall b/tests/normalization/examples/Bool/odd/3A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/odd/3A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Bool/odd ([] : List Bool) diff --git a/tests/normalization/examples/Bool/odd/3B.dhall b/tests/normalization/examples/Bool/odd/3B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/odd/3B.dhall @@ -0,0 +1,1 @@ +False diff --git a/tests/normalization/examples/Bool/or/0A.dhall b/tests/normalization/examples/Bool/or/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/or/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Bool/or [ True, False, True ] diff --git a/tests/normalization/examples/Bool/or/0B.dhall b/tests/normalization/examples/Bool/or/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/or/0B.dhall @@ -0,0 +1,1 @@ +True diff --git a/tests/normalization/examples/Bool/or/1A.dhall b/tests/normalization/examples/Bool/or/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/or/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Bool/or ([] : List Bool) diff --git a/tests/normalization/examples/Bool/or/1B.dhall b/tests/normalization/examples/Bool/or/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/or/1B.dhall @@ -0,0 +1,1 @@ +False diff --git a/tests/normalization/examples/Bool/show/0A.dhall b/tests/normalization/examples/Bool/show/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/show/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Bool/show True diff --git a/tests/normalization/examples/Bool/show/0B.dhall b/tests/normalization/examples/Bool/show/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/show/0B.dhall @@ -0,0 +1,1 @@ +"True" diff --git a/tests/normalization/examples/Bool/show/1A.dhall b/tests/normalization/examples/Bool/show/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/show/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Bool/show False diff --git a/tests/normalization/examples/Bool/show/1B.dhall b/tests/normalization/examples/Bool/show/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Bool/show/1B.dhall @@ -0,0 +1,1 @@ +"False" diff --git a/tests/normalization/examples/Double/show/0A.dhall b/tests/normalization/examples/Double/show/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Double/show/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Double/show -3.1 diff --git a/tests/normalization/examples/Double/show/0B.dhall b/tests/normalization/examples/Double/show/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Double/show/0B.dhall @@ -0,0 +1,1 @@ +"-3.1" diff --git a/tests/normalization/examples/Double/show/1A.dhall b/tests/normalization/examples/Double/show/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Double/show/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Double/show 0.4 diff --git a/tests/normalization/examples/Double/show/1B.dhall b/tests/normalization/examples/Double/show/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Double/show/1B.dhall @@ -0,0 +1,1 @@ +"0.4" diff --git a/tests/normalization/examples/Integer/show/0A.dhall b/tests/normalization/examples/Integer/show/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Integer/show/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Integer/show -3 diff --git a/tests/normalization/examples/Integer/show/0B.dhall b/tests/normalization/examples/Integer/show/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Integer/show/0B.dhall @@ -0,0 +1,1 @@ +"-3" diff --git a/tests/normalization/examples/Integer/show/1A.dhall b/tests/normalization/examples/Integer/show/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Integer/show/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Integer/show 0 diff --git a/tests/normalization/examples/Integer/show/1B.dhall b/tests/normalization/examples/Integer/show/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Integer/show/1B.dhall @@ -0,0 +1,1 @@ +"0" diff --git a/tests/normalization/examples/List/all/0A.dhall b/tests/normalization/examples/List/all/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/all/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/all Natural Natural/even [ +2, +3, +5 ] diff --git a/tests/normalization/examples/List/all/0B.dhall b/tests/normalization/examples/List/all/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/all/0B.dhall @@ -0,0 +1,1 @@ +False diff --git a/tests/normalization/examples/List/all/1A.dhall b/tests/normalization/examples/List/all/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/all/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/all Natural Natural/even ([] : List Natural) diff --git a/tests/normalization/examples/List/all/1B.dhall b/tests/normalization/examples/List/all/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/all/1B.dhall @@ -0,0 +1,1 @@ +True diff --git a/tests/normalization/examples/List/any/0A.dhall b/tests/normalization/examples/List/any/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/any/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/any Natural Natural/even [ +2, +3, +5 ] diff --git a/tests/normalization/examples/List/any/0B.dhall b/tests/normalization/examples/List/any/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/any/0B.dhall @@ -0,0 +1,1 @@ +True diff --git a/tests/normalization/examples/List/any/1A.dhall b/tests/normalization/examples/List/any/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/any/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/any Natural Natural/even ([] : List Natural) diff --git a/tests/normalization/examples/List/any/1B.dhall b/tests/normalization/examples/List/any/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/any/1B.dhall @@ -0,0 +1,1 @@ +False diff --git a/tests/normalization/examples/List/build/0A.dhall b/tests/normalization/examples/List/build/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/build/0A.dhall @@ -0,0 +1,7 @@ +../../../../../Prelude/List/build +Text +( λ(list : Type) +→ λ(cons : Text → list → list) +→ λ(nil : list) +→ cons "ABC" (cons "DEF" nil) +) diff --git a/tests/normalization/examples/List/build/0B.dhall b/tests/normalization/examples/List/build/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/build/0B.dhall @@ -0,0 +1,1 @@ +[ "ABC", "DEF" ] diff --git a/tests/normalization/examples/List/build/1A.dhall b/tests/normalization/examples/List/build/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/build/1A.dhall @@ -0,0 +1,7 @@ +../../../../../Prelude/List/build +Text +( λ(list : Type) +→ λ(cons : Text → list → list) +→ λ(nil : list) +→ nil +) diff --git a/tests/normalization/examples/List/build/1B.dhall b/tests/normalization/examples/List/build/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/build/1B.dhall @@ -0,0 +1,1 @@ +[] : List Text diff --git a/tests/normalization/examples/List/concat/0A.dhall b/tests/normalization/examples/List/concat/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/concat/0A.dhall @@ -0,0 +1,5 @@ +../../../../../Prelude/List/concat Integer +[ [ 0, 1, 2 ] +, [ 3, 4 ] +, [ 5, 6, 7, 8 ] +] diff --git a/tests/normalization/examples/List/concat/0B.dhall b/tests/normalization/examples/List/concat/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/concat/0B.dhall @@ -0,0 +1,1 @@ +[ 0, 1, 2, 3, 4, 5, 6, 7, 8 ] diff --git a/tests/normalization/examples/List/concat/1A.dhall b/tests/normalization/examples/List/concat/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/concat/1A.dhall @@ -0,0 +1,5 @@ +../../../../../Prelude/List/concat Integer +[ [] : List Integer +, [] : List Integer +, [] : List Integer +] diff --git a/tests/normalization/examples/List/concat/1B.dhall b/tests/normalization/examples/List/concat/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/concat/1B.dhall @@ -0,0 +1,1 @@ +[] : List Integer diff --git a/tests/normalization/examples/List/concatMap/0A.dhall b/tests/normalization/examples/List/concatMap/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/concatMap/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/concatMap Natural Natural (λ(n : Natural) → [ n, n ]) [ +2, +3, +5 ] diff --git a/tests/normalization/examples/List/concatMap/0B.dhall b/tests/normalization/examples/List/concatMap/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/concatMap/0B.dhall @@ -0,0 +1,1 @@ +[ +2, +2, +3, +3, +5, +5 ] diff --git a/tests/normalization/examples/List/concatMap/1A.dhall b/tests/normalization/examples/List/concatMap/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/concatMap/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/concatMap Natural Natural (λ(n : Natural) → [ n, n ]) ([] : List Natural) diff --git a/tests/normalization/examples/List/concatMap/1B.dhall b/tests/normalization/examples/List/concatMap/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/concatMap/1B.dhall @@ -0,0 +1,1 @@ +[] : List Natural diff --git a/tests/normalization/examples/List/filter/0A.dhall b/tests/normalization/examples/List/filter/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/filter/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/filter Natural Natural/even [ +2, +3, +5 ] diff --git a/tests/normalization/examples/List/filter/0B.dhall b/tests/normalization/examples/List/filter/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/filter/0B.dhall @@ -0,0 +1,1 @@ +[ +2 ] diff --git a/tests/normalization/examples/List/filter/1A.dhall b/tests/normalization/examples/List/filter/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/filter/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/filter Natural Natural/odd [ +2, +3, +5 ] diff --git a/tests/normalization/examples/List/filter/1B.dhall b/tests/normalization/examples/List/filter/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/filter/1B.dhall @@ -0,0 +1,1 @@ +[ +3, +5 ] diff --git a/tests/normalization/examples/List/fold/0A.dhall b/tests/normalization/examples/List/fold/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/fold/0A.dhall @@ -0,0 +1,6 @@ +../../../../../Prelude/List/fold +Natural +[ +2, +3, +5 ] +Natural +(λ(x : Natural) → λ(y : Natural) → x + y) ++0 diff --git a/tests/normalization/examples/List/fold/0B.dhall b/tests/normalization/examples/List/fold/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/fold/0B.dhall @@ -0,0 +1,1 @@ ++10 diff --git a/tests/normalization/examples/List/fold/1A.dhall b/tests/normalization/examples/List/fold/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/fold/1A.dhall @@ -0,0 +1,7 @@ + λ(nil : Natural) +→ ../../../../../Prelude/List/fold + Natural + [ +2, +3, +5 ] + Natural + (λ(x : Natural) → λ(y : Natural) → x + y) + nil diff --git a/tests/normalization/examples/List/fold/1B.dhall b/tests/normalization/examples/List/fold/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/fold/1B.dhall @@ -0,0 +1,1 @@ +λ(nil : Natural) → +2 + +3 + +5 + nil diff --git a/tests/normalization/examples/List/fold/2A.dhall b/tests/normalization/examples/List/fold/2A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/fold/2A.dhall @@ -0,0 +1,4 @@ + λ(list : Type) +→ λ(cons : Natural → list → list) +→ λ(nil : list) +→ ../../../../../Prelude/List/fold Natural [ +2, +3, +5 ] list cons nil diff --git a/tests/normalization/examples/List/fold/2B.dhall b/tests/normalization/examples/List/fold/2B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/fold/2B.dhall @@ -0,0 +1,4 @@ + λ(list : Type) +→ λ(cons : Natural → list → list) +→ λ(nil : list) +→ cons +2 (cons +3 (cons +5 nil)) diff --git a/tests/normalization/examples/List/generate/0A.dhall b/tests/normalization/examples/List/generate/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/generate/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/generate +5 Bool Natural/even diff --git a/tests/normalization/examples/List/generate/0B.dhall b/tests/normalization/examples/List/generate/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/generate/0B.dhall @@ -0,0 +1,1 @@ +[ True, False, True, False, True ] diff --git a/tests/normalization/examples/List/generate/1A.dhall b/tests/normalization/examples/List/generate/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/generate/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/generate +0 Bool Natural/even diff --git a/tests/normalization/examples/List/generate/1B.dhall b/tests/normalization/examples/List/generate/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/generate/1B.dhall @@ -0,0 +1,1 @@ +[] : List Bool diff --git a/tests/normalization/examples/List/head/0A.dhall b/tests/normalization/examples/List/head/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/head/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/head Integer [ 0, 1, 2 ] diff --git a/tests/normalization/examples/List/head/0B.dhall b/tests/normalization/examples/List/head/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/head/0B.dhall @@ -0,0 +1,1 @@ +[ 0 ] : Optional Integer diff --git a/tests/normalization/examples/List/head/1A.dhall b/tests/normalization/examples/List/head/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/head/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/head Integer ([] : List Integer) diff --git a/tests/normalization/examples/List/head/1B.dhall b/tests/normalization/examples/List/head/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/head/1B.dhall @@ -0,0 +1,1 @@ +[] : Optional Integer diff --git a/tests/normalization/examples/List/indexed/0A.dhall b/tests/normalization/examples/List/indexed/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/indexed/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/indexed Bool ([] : List Bool) diff --git a/tests/normalization/examples/List/indexed/0B.dhall b/tests/normalization/examples/List/indexed/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/indexed/0B.dhall @@ -0,0 +1,4 @@ +[ { index = +0, value = True } +, { index = +1, value = False } +, { index = +2, valu;e = True } +] diff --git a/tests/normalization/examples/List/indexed/1A.dhall b/tests/normalization/examples/List/indexed/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/indexed/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/indexed Bool ([] : List Bool) diff --git a/tests/normalization/examples/List/indexed/1B.dhall b/tests/normalization/examples/List/indexed/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/indexed/1B.dhall @@ -0,0 +1,1 @@ +[] : List { index : Natural, value : Bool } diff --git a/tests/normalization/examples/List/iterate/0A.dhall b/tests/normalization/examples/List/iterate/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/iterate/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/iterate +10 Natural (λ(x : Natural) → x * +2) +1 diff --git a/tests/normalization/examples/List/iterate/0B.dhall b/tests/normalization/examples/List/iterate/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/iterate/0B.dhall @@ -0,0 +1,1 @@ +[ +1, +2, +4, +8, +16, +32, +64, +128, +256, +512 ] diff --git a/tests/normalization/examples/List/iterate/1A.dhall b/tests/normalization/examples/List/iterate/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/iterate/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/iterate +0 Natural (λ(x : Natural) → x * +2) +1 diff --git a/tests/normalization/examples/List/iterate/1B.dhall b/tests/normalization/examples/List/iterate/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/iterate/1B.dhall @@ -0,0 +1,1 @@ +[] : List Natural diff --git a/tests/normalization/examples/List/last/0A.dhall b/tests/normalization/examples/List/last/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/last/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/last Integer [ 0, 1, 2 ] diff --git a/tests/normalization/examples/List/last/0B.dhall b/tests/normalization/examples/List/last/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/last/0B.dhall @@ -0,0 +1,1 @@ +[ 2 ] : Optional Integer diff --git a/tests/normalization/examples/List/last/1A.dhall b/tests/normalization/examples/List/last/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/last/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/last Integer ([] : List Integer) diff --git a/tests/normalization/examples/List/last/1B.dhall b/tests/normalization/examples/List/last/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/last/1B.dhall @@ -0,0 +1,1 @@ +[] : Optional Integer diff --git a/tests/normalization/examples/List/length/0A.dhall b/tests/normalization/examples/List/length/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/length/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/length Integer [ 0, 1, 2 ] diff --git a/tests/normalization/examples/List/length/0B.dhall b/tests/normalization/examples/List/length/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/length/0B.dhall @@ -0,0 +1,1 @@ ++3 diff --git a/tests/normalization/examples/List/length/1A.dhall b/tests/normalization/examples/List/length/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/length/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/length Integer ([] : List Integer) diff --git a/tests/normalization/examples/List/length/1B.dhall b/tests/normalization/examples/List/length/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/length/1B.dhall @@ -0,0 +1,1 @@ ++0 diff --git a/tests/normalization/examples/List/map/0A.dhall b/tests/normalization/examples/List/map/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/map/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/map Natural Bool Natural/even [ +2, +3, +5 ] diff --git a/tests/normalization/examples/List/map/0B.dhall b/tests/normalization/examples/List/map/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/map/0B.dhall @@ -0,0 +1,1 @@ +[ True, False, False ] diff --git a/tests/normalization/examples/List/map/1A.dhall b/tests/normalization/examples/List/map/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/map/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/map Natural Bool Natural/even ([] : List Natural) diff --git a/tests/normalization/examples/List/map/1B.dhall b/tests/normalization/examples/List/map/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/map/1B.dhall @@ -0,0 +1,1 @@ +[] : List Bool diff --git a/tests/normalization/examples/List/null/0A.dhall b/tests/normalization/examples/List/null/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/null/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/null Integer [ 0, 1, 2 ] diff --git a/tests/normalization/examples/List/null/0B.dhall b/tests/normalization/examples/List/null/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/null/0B.dhall @@ -0,0 +1,1 @@ +False diff --git a/tests/normalization/examples/List/null/1A.dhall b/tests/normalization/examples/List/null/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/null/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/null Integer ([] : List Integer) diff --git a/tests/normalization/examples/List/null/1B.dhall b/tests/normalization/examples/List/null/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/null/1B.dhall @@ -0,0 +1,1 @@ +True diff --git a/tests/normalization/examples/List/replicate/0A.dhall b/tests/normalization/examples/List/replicate/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/replicate/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/replicate +9 Integer 1 diff --git a/tests/normalization/examples/List/replicate/0B.dhall b/tests/normalization/examples/List/replicate/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/replicate/0B.dhall @@ -0,0 +1,1 @@ +[ 1, 1, 1, 1, 1, 1, 1, 1, 1 ] diff --git a/tests/normalization/examples/List/replicate/1A.dhall b/tests/normalization/examples/List/replicate/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/replicate/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/replicate +0 Integer 1 diff --git a/tests/normalization/examples/List/replicate/1B.dhall b/tests/normalization/examples/List/replicate/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/replicate/1B.dhall @@ -0,0 +1,1 @@ +[] : List Integer diff --git a/tests/normalization/examples/List/reverse/0A.dhall b/tests/normalization/examples/List/reverse/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/reverse/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/reverse Integer [ 0, 1, 2 ] diff --git a/tests/normalization/examples/List/reverse/0B.dhall b/tests/normalization/examples/List/reverse/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/reverse/0B.dhall @@ -0,0 +1,1 @@ +[ 2, 1, 0 ] diff --git a/tests/normalization/examples/List/reverse/1A.dhall b/tests/normalization/examples/List/reverse/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/reverse/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/reverse Integer ([] : List Integer) diff --git a/tests/normalization/examples/List/reverse/1B.dhall b/tests/normalization/examples/List/reverse/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/reverse/1B.dhall @@ -0,0 +1,1 @@ +[] : List Integer diff --git a/tests/normalization/examples/List/shifted/0A.dhall b/tests/normalization/examples/List/shifted/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/shifted/0A.dhall @@ -0,0 +1,15 @@ +../../../../../Prelude/List/shifted +Bool +[ [ { index = +0, value = True } + , { index = +1, value = True } + , { index = +2, value = False } + ] +, [ { index = +0, value = False } + , { index = +1, value = False } + ] +, [ { index = +0, value = True } + , { index = +1, value = True } + , { index = +2, value = True } + , { index = +3, value = True } + ] +] diff --git a/tests/normalization/examples/List/shifted/0B.dhall b/tests/normalization/examples/List/shifted/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/shifted/0B.dhall @@ -0,0 +1,10 @@ +[ { index = +0, value = True } +, { index = +1, value = True } +, { index = +2, value = False } +, { index = +3, value = False } +, { index = +4, value = False } +, { index = +5, value = True } +, { index = +6, value = True } +, { index = +7, value = True } +, { index = +8, value = True } +] diff --git a/tests/normalization/examples/List/shifted/1A.dhall b/tests/normalization/examples/List/shifted/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/shifted/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/shifted Bool ([] : List (List { index : Natural, value : Bool })) diff --git a/tests/normalization/examples/List/shifted/1B.dhall b/tests/normalization/examples/List/shifted/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/shifted/1B.dhall @@ -0,0 +1,1 @@ +[] : List { index : Natural, value : Bool } diff --git a/tests/normalization/examples/List/unzip/0A.dhall b/tests/normalization/examples/List/unzip/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/unzip/0A.dhall @@ -0,0 +1,7 @@ +../../../../../Prelude/List/unzip +Text +Bool +[ { _1 = "ABC", _2 = True } +, { _1 = "DEF", _2 = False } +, { _1 = "GHI", _2 = True } +] diff --git a/tests/normalization/examples/List/unzip/0B.dhall b/tests/normalization/examples/List/unzip/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/unzip/0B.dhall @@ -0,0 +1,1 @@ +{ _1 = [ "ABC", "DEF", "GHI" ], _2 = [ True, False, True ] } diff --git a/tests/normalization/examples/List/unzip/1A.dhall b/tests/normalization/examples/List/unzip/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/unzip/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/List/unzip Text Bool ([] : List { _1 : Text, _2 : Bool }) diff --git a/tests/normalization/examples/List/unzip/1B.dhall b/tests/normalization/examples/List/unzip/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/List/unzip/1B.dhall @@ -0,0 +1,1 @@ +{ _1 = [] : List Text, _2 = [] : List Bool } diff --git a/tests/normalization/examples/Natural/build/0A.dhall b/tests/normalization/examples/Natural/build/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/build/0A.dhall @@ -0,0 +1,6 @@ +../../../../../Prelude/Natural/build +( λ(natural : Type) +→ λ(succ : natural → natural) +→ λ(zero : natural) +→ succ (succ (succ zero)) +) diff --git a/tests/normalization/examples/Natural/build/0B.dhall b/tests/normalization/examples/Natural/build/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/build/0B.dhall @@ -0,0 +1,1 @@ ++3 diff --git a/tests/normalization/examples/Natural/build/1A.dhall b/tests/normalization/examples/Natural/build/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/build/1A.dhall @@ -0,0 +1,6 @@ +../../../../../Prelude/Natural/build +( λ(natural : Type) +→ λ(succ : natural → natural) +→ λ(zero : natural) +→ zero +) diff --git a/tests/normalization/examples/Natural/build/1B.dhall b/tests/normalization/examples/Natural/build/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/build/1B.dhall @@ -0,0 +1,1 @@ ++0 diff --git a/tests/normalization/examples/Natural/enumerate/0A.dhall b/tests/normalization/examples/Natural/enumerate/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/enumerate/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Natural/enumerate +10 diff --git a/tests/normalization/examples/Natural/enumerate/0B.dhall b/tests/normalization/examples/Natural/enumerate/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/enumerate/0B.dhall @@ -0,0 +1,1 @@ +[ +0, +1, +2, +3, +4, +5, +6, +7, +8, +9 ] diff --git a/tests/normalization/examples/Natural/enumerate/1A.dhall b/tests/normalization/examples/Natural/enumerate/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/enumerate/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Natural/enumerate +0 diff --git a/tests/normalization/examples/Natural/enumerate/1B.dhall b/tests/normalization/examples/Natural/enumerate/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/enumerate/1B.dhall @@ -0,0 +1,1 @@ +[] : List Natural diff --git a/tests/normalization/examples/Natural/even/0A.dhall b/tests/normalization/examples/Natural/even/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/even/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Natural/even +3 diff --git a/tests/normalization/examples/Natural/even/0B.dhall b/tests/normalization/examples/Natural/even/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/even/0B.dhall @@ -0,0 +1,1 @@ +False diff --git a/tests/normalization/examples/Natural/even/1A.dhall b/tests/normalization/examples/Natural/even/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/even/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Natural/even +0 diff --git a/tests/normalization/examples/Natural/even/1B.dhall b/tests/normalization/examples/Natural/even/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/even/1B.dhall @@ -0,0 +1,1 @@ +True diff --git a/tests/normalization/examples/Natural/fold/0A.dhall b/tests/normalization/examples/Natural/fold/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/fold/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Natural/fold +3 Natural (λ(x : Natural) → +5 * x) +1 diff --git a/tests/normalization/examples/Natural/fold/0B.dhall b/tests/normalization/examples/Natural/fold/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/fold/0B.dhall @@ -0,0 +1,1 @@ ++125 diff --git a/tests/normalization/examples/Natural/fold/1A.dhall b/tests/normalization/examples/Natural/fold/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/fold/1A.dhall @@ -0,0 +1,1 @@ +λ(zero : Natural) → ../../../../../Prelude/Natural/fold +3 Natural (λ(x : Natural) → +5 * x) zero diff --git a/tests/normalization/examples/Natural/fold/1B.dhall b/tests/normalization/examples/Natural/fold/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/fold/1B.dhall @@ -0,0 +1,1 @@ +λ(zero : Natural) → +5 * +5 * +5 * zero diff --git a/tests/normalization/examples/Natural/fold/2A.dhall b/tests/normalization/examples/Natural/fold/2A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/fold/2A.dhall @@ -0,0 +1,4 @@ + λ(natural : Type) +→ λ(succ : natural → natural) +→ λ(zero : natural) +→ ../../../../../Prelude/Natural/fold +3 natural succ zero diff --git a/tests/normalization/examples/Natural/fold/2B.dhall b/tests/normalization/examples/Natural/fold/2B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/fold/2B.dhall @@ -0,0 +1,1 @@ +λ(natural : Type) → λ(succ : natural → natural) → λ(zero : natural) → succ (succ (succ zero)) diff --git a/tests/normalization/examples/Natural/isZero/0A.dhall b/tests/normalization/examples/Natural/isZero/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/isZero/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Natural/isZero +2 diff --git a/tests/normalization/examples/Natural/isZero/0B.dhall b/tests/normalization/examples/Natural/isZero/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/isZero/0B.dhall @@ -0,0 +1,1 @@ +False diff --git a/tests/normalization/examples/Natural/isZero/1A.dhall b/tests/normalization/examples/Natural/isZero/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/isZero/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Natural/isZero +0 diff --git a/tests/normalization/examples/Natural/isZero/1B.dhall b/tests/normalization/examples/Natural/isZero/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/isZero/1B.dhall @@ -0,0 +1,1 @@ +True diff --git a/tests/normalization/examples/Natural/odd/0A.dhall b/tests/normalization/examples/Natural/odd/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/odd/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Natural/odd +3 diff --git a/tests/normalization/examples/Natural/odd/0B.dhall b/tests/normalization/examples/Natural/odd/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/odd/0B.dhall @@ -0,0 +1,1 @@ +True diff --git a/tests/normalization/examples/Natural/odd/1A.dhall b/tests/normalization/examples/Natural/odd/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/odd/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Natural/odd +0 diff --git a/tests/normalization/examples/Natural/odd/1B.dhall b/tests/normalization/examples/Natural/odd/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/odd/1B.dhall @@ -0,0 +1,1 @@ +False diff --git a/tests/normalization/examples/Natural/product/0A.dhall b/tests/normalization/examples/Natural/product/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/product/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Natural/product [ +2, +3, +5 ] diff --git a/tests/normalization/examples/Natural/product/0B.dhall b/tests/normalization/examples/Natural/product/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/product/0B.dhall @@ -0,0 +1,1 @@ ++30 diff --git a/tests/normalization/examples/Natural/product/1A.dhall b/tests/normalization/examples/Natural/product/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/product/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Natural/product ([] : List Natural) diff --git a/tests/normalization/examples/Natural/product/1B.dhall b/tests/normalization/examples/Natural/product/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/product/1B.dhall @@ -0,0 +1,1 @@ ++1 diff --git a/tests/normalization/examples/Natural/show/0A.dhall b/tests/normalization/examples/Natural/show/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/show/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Natural/show +3 diff --git a/tests/normalization/examples/Natural/show/0B.dhall b/tests/normalization/examples/Natural/show/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/show/0B.dhall @@ -0,0 +1,1 @@ +"+3" diff --git a/tests/normalization/examples/Natural/show/1A.dhall b/tests/normalization/examples/Natural/show/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/show/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Natural/show +0 diff --git a/tests/normalization/examples/Natural/show/1B.dhall b/tests/normalization/examples/Natural/show/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/show/1B.dhall @@ -0,0 +1,1 @@ +"+0" diff --git a/tests/normalization/examples/Natural/sum/0A.dhall b/tests/normalization/examples/Natural/sum/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/sum/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Natural/sum [ +2, +3, +5 ] diff --git a/tests/normalization/examples/Natural/sum/0B.dhall b/tests/normalization/examples/Natural/sum/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/sum/0B.dhall @@ -0,0 +1,1 @@ ++10 diff --git a/tests/normalization/examples/Natural/sum/1A.dhall b/tests/normalization/examples/Natural/sum/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/sum/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Natural/sum ([] : List Natural) diff --git a/tests/normalization/examples/Natural/sum/1B.dhall b/tests/normalization/examples/Natural/sum/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/sum/1B.dhall @@ -0,0 +1,1 @@ ++0 diff --git a/tests/normalization/examples/Natural/toInteger/0A.dhall b/tests/normalization/examples/Natural/toInteger/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/toInteger/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Natural/toInteger +3 diff --git a/tests/normalization/examples/Natural/toInteger/0B.dhall b/tests/normalization/examples/Natural/toInteger/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/toInteger/0B.dhall @@ -0,0 +1,1 @@ +3 diff --git a/tests/normalization/examples/Natural/toInteger/1A.dhall b/tests/normalization/examples/Natural/toInteger/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/toInteger/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Natural/toInteger +0 diff --git a/tests/normalization/examples/Natural/toInteger/1B.dhall b/tests/normalization/examples/Natural/toInteger/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Natural/toInteger/1B.dhall @@ -0,0 +1,1 @@ +0 diff --git a/tests/normalization/examples/Optional/all/0A.dhall b/tests/normalization/examples/Optional/all/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/all/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Optional/all Natural Natural/even ([ +3 ] : Optional Natural) diff --git a/tests/normalization/examples/Optional/all/0B.dhall b/tests/normalization/examples/Optional/all/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/all/0B.dhall @@ -0,0 +1,1 @@ +False diff --git a/tests/normalization/examples/Optional/all/1A.dhall b/tests/normalization/examples/Optional/all/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/all/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Optional/all Natural Natural/even ([] : Optional Natural) diff --git a/tests/normalization/examples/Optional/all/1B.dhall b/tests/normalization/examples/Optional/all/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/all/1B.dhall @@ -0,0 +1,1 @@ +True diff --git a/tests/normalization/examples/Optional/any/0A.dhall b/tests/normalization/examples/Optional/any/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/any/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Optional/any Natural Natural/even ([ +2 ] : Optional Natural) diff --git a/tests/normalization/examples/Optional/any/0B.dhall b/tests/normalization/examples/Optional/any/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/any/0B.dhall @@ -0,0 +1,1 @@ +True diff --git a/tests/normalization/examples/Optional/any/1A.dhall b/tests/normalization/examples/Optional/any/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/any/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Optional/any Natural Natural/even ([] : Optional Natural) diff --git a/tests/normalization/examples/Optional/any/1B.dhall b/tests/normalization/examples/Optional/any/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/any/1B.dhall @@ -0,0 +1,1 @@ +False diff --git a/tests/normalization/examples/Optional/build/0A.dhall b/tests/normalization/examples/Optional/build/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/build/0A.dhall @@ -0,0 +1,7 @@ +../../../../../Prelude/Optional/build +Integer +( λ(optional : Type) +→ λ(just : Integer → optional) +→ λ(nothing : optional) +→ just 1 +) diff --git a/tests/normalization/examples/Optional/build/0B.dhall b/tests/normalization/examples/Optional/build/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/build/0B.dhall @@ -0,0 +1,1 @@ +[ 1 ] : Optional Integer diff --git a/tests/normalization/examples/Optional/build/1A.dhall b/tests/normalization/examples/Optional/build/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/build/1A.dhall @@ -0,0 +1,7 @@ +../../../../../Prelude/Optional/build +Integer +( λ(optional : Type) +→ λ(just : Integer → optional) +→ λ(nothing : optional) +→ nothing +) diff --git a/tests/normalization/examples/Optional/build/1B.dhall b/tests/normalization/examples/Optional/build/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/build/1B.dhall @@ -0,0 +1,1 @@ +[] : Optional Integer diff --git a/tests/normalization/examples/Optional/concat/0A.dhall b/tests/normalization/examples/Optional/concat/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/concat/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Optional/concat Integer ([ [ 1 ] : Optional Integer ] : Optional (Optional Integer)) diff --git a/tests/normalization/examples/Optional/concat/0B.dhall b/tests/normalization/examples/Optional/concat/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/concat/0B.dhall @@ -0,0 +1,1 @@ +[ 1 ] : Optional Integer diff --git a/tests/normalization/examples/Optional/concat/1A.dhall b/tests/normalization/examples/Optional/concat/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/concat/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Optional/concat Integer ([ [] : Optional Integer ] : Optional (Optional Integer)) diff --git a/tests/normalization/examples/Optional/concat/1B.dhall b/tests/normalization/examples/Optional/concat/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/concat/1B.dhall @@ -0,0 +1,1 @@ +[] : Optional Integer diff --git a/tests/normalization/examples/Optional/concat/2A.dhall b/tests/normalization/examples/Optional/concat/2A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/concat/2A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Optional/concat Integer ([ [] : Optional Integer ]: Optional (Optional Integer)) diff --git a/tests/normalization/examples/Optional/concat/2B.dhall b/tests/normalization/examples/Optional/concat/2B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/concat/2B.dhall @@ -0,0 +1,1 @@ +[] : Optional Integer diff --git a/tests/normalization/examples/Optional/filter/0A.dhall b/tests/normalization/examples/Optional/filter/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/filter/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Optional/filter Natural Natural/even ([ +2 ] : Optional Natural) diff --git a/tests/normalization/examples/Optional/filter/0B.dhall b/tests/normalization/examples/Optional/filter/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/filter/0B.dhall @@ -0,0 +1,1 @@ +[ +2 ] : Optional Natural diff --git a/tests/normalization/examples/Optional/filter/1A.dhall b/tests/normalization/examples/Optional/filter/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/filter/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Optional/filter Natural Natural/odd ([ +2 ] : Optional Natural) diff --git a/tests/normalization/examples/Optional/filter/1B.dhall b/tests/normalization/examples/Optional/filter/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/filter/1B.dhall @@ -0,0 +1,1 @@ +[] : Optional Natural diff --git a/tests/normalization/examples/Optional/fold/0A.dhall b/tests/normalization/examples/Optional/fold/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/fold/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Optional/fold Integer ([ 2 ] : Optional Integer) Integer (λ(x : Integer) → x) 0 diff --git a/tests/normalization/examples/Optional/fold/0B.dhall b/tests/normalization/examples/Optional/fold/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/fold/0B.dhall @@ -0,0 +1,1 @@ +2 diff --git a/tests/normalization/examples/Optional/fold/1A.dhall b/tests/normalization/examples/Optional/fold/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/fold/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Optional/fold Integer ([] : Optional Integer) Integer (λ(x : Integer) → x) 0 diff --git a/tests/normalization/examples/Optional/fold/1B.dhall b/tests/normalization/examples/Optional/fold/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/fold/1B.dhall @@ -0,0 +1,1 @@ +0 diff --git a/tests/normalization/examples/Optional/head/0A.dhall b/tests/normalization/examples/Optional/head/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/head/0A.dhall @@ -0,0 +1,6 @@ +../../../../../Prelude/Optional/head +Integer +[ [] : Optional Integer +, [ 1 ] : Optional Integer +, [ 2 ] : Optional Integer +] diff --git a/tests/normalization/examples/Optional/head/0B.dhall b/tests/normalization/examples/Optional/head/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/head/0B.dhall @@ -0,0 +1,1 @@ +[ 1 ] : Optional Integer diff --git a/tests/normalization/examples/Optional/head/1A.dhall b/tests/normalization/examples/Optional/head/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/head/1A.dhall @@ -0,0 +1,3 @@ +../../../../../Prelude/Optional/head +Integer +[ [] : Optional Integer, [] : Optional Integer ] diff --git a/tests/normalization/examples/Optional/head/1B.dhall b/tests/normalization/examples/Optional/head/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/head/1B.dhall @@ -0,0 +1,1 @@ +[] : Optional Integer diff --git a/tests/normalization/examples/Optional/last/0A.dhall b/tests/normalization/examples/Optional/last/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/last/0A.dhall @@ -0,0 +1,7 @@ +../../../../../Prelude/Optional/last +Integer +( [ [] : Optional Integer + , [ 1 ] : Optional Integer + , [ 2 ] : Optional Integer + ] +) diff --git a/tests/normalization/examples/Optional/last/0B.dhall b/tests/normalization/examples/Optional/last/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/last/0B.dhall @@ -0,0 +1,1 @@ +[ 2 ] : Optional Integer diff --git a/tests/normalization/examples/Optional/last/1A.dhall b/tests/normalization/examples/Optional/last/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/last/1A.dhall @@ -0,0 +1,3 @@ +../../../../../Prelude/Optional/last +Integer +[ [] : Optional Integer, [] : Optional Integer ] diff --git a/tests/normalization/examples/Optional/last/1B.dhall b/tests/normalization/examples/Optional/last/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/last/1B.dhall @@ -0,0 +1,1 @@ +[] : Optional Integer diff --git a/tests/normalization/examples/Optional/last/2A.dhall b/tests/normalization/examples/Optional/last/2A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/last/2A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Optional/last Integer ([] : List (Optional Integer)) diff --git a/tests/normalization/examples/Optional/last/2B.dhall b/tests/normalization/examples/Optional/last/2B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/last/2B.dhall @@ -0,0 +1,1 @@ +[] : Optional Integer diff --git a/tests/normalization/examples/Optional/length/0A.dhall b/tests/normalization/examples/Optional/length/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/length/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Optional/length Integer ([ 2 ] : Optional Integer) diff --git a/tests/normalization/examples/Optional/length/0B.dhall b/tests/normalization/examples/Optional/length/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/length/0B.dhall @@ -0,0 +1,1 @@ ++1 diff --git a/tests/normalization/examples/Optional/length/1A.dhall b/tests/normalization/examples/Optional/length/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/length/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Optional/length Integer ([] : Optional Integer) diff --git a/tests/normalization/examples/Optional/length/1B.dhall b/tests/normalization/examples/Optional/length/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/length/1B.dhall @@ -0,0 +1,1 @@ ++0 diff --git a/tests/normalization/examples/Optional/map/0A.dhall b/tests/normalization/examples/Optional/map/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/map/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Optional/map Natural Bool Natural/even ([ +3 ] : Optional Natural) diff --git a/tests/normalization/examples/Optional/map/0B.dhall b/tests/normalization/examples/Optional/map/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/map/0B.dhall @@ -0,0 +1,1 @@ +[ False ] : Optional Bool diff --git a/tests/normalization/examples/Optional/map/1A.dhall b/tests/normalization/examples/Optional/map/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/map/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Optional/map Natural Bool Natural/even ([] : Optional Natural) diff --git a/tests/normalization/examples/Optional/map/1B.dhall b/tests/normalization/examples/Optional/map/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/map/1B.dhall @@ -0,0 +1,1 @@ +[] : Optional Bool diff --git a/tests/normalization/examples/Optional/null/0A.dhall b/tests/normalization/examples/Optional/null/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/null/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Optional/null Integer ([ 2 ] : Optional Integer) diff --git a/tests/normalization/examples/Optional/null/0B.dhall b/tests/normalization/examples/Optional/null/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/null/0B.dhall @@ -0,0 +1,1 @@ +False diff --git a/tests/normalization/examples/Optional/null/1A.dhall b/tests/normalization/examples/Optional/null/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/null/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Optional/null Integer ([] : Optional Integer) diff --git a/tests/normalization/examples/Optional/null/1B.dhall b/tests/normalization/examples/Optional/null/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/null/1B.dhall @@ -0,0 +1,1 @@ +True diff --git a/tests/normalization/examples/Optional/toList/0A.dhall b/tests/normalization/examples/Optional/toList/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/toList/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Optional/toList Integer ([ 1 ] : Optional Integer) diff --git a/tests/normalization/examples/Optional/toList/0B.dhall b/tests/normalization/examples/Optional/toList/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/toList/0B.dhall @@ -0,0 +1,1 @@ +[ 1 ] diff --git a/tests/normalization/examples/Optional/toList/1A.dhall b/tests/normalization/examples/Optional/toList/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/toList/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Optional/toList Integer ([] : Optional Integer) diff --git a/tests/normalization/examples/Optional/toList/1B.dhall b/tests/normalization/examples/Optional/toList/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/toList/1B.dhall @@ -0,0 +1,1 @@ +[] : List Integer diff --git a/tests/normalization/examples/Optional/unzip/0A.dhall b/tests/normalization/examples/Optional/unzip/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/unzip/0A.dhall @@ -0,0 +1,4 @@ +../../../../../Prelude/Optional/unzip +Text +Bool +([ { _1 = "ABC", _2 = True } ] : Optional { _1 : Text, _2 : Bool }) diff --git a/tests/normalization/examples/Optional/unzip/0B.dhall b/tests/normalization/examples/Optional/unzip/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/unzip/0B.dhall @@ -0,0 +1,1 @@ +{ _1 = [ "ABC" ] : Optional Text, _2 = [ True ] : Optional Bool } diff --git a/tests/normalization/examples/Optional/unzip/1A.dhall b/tests/normalization/examples/Optional/unzip/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/unzip/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Optional/unzip Text Bool ([] : Optional { _1 : Text, _2 : Bool }) diff --git a/tests/normalization/examples/Optional/unzip/1B.dhall b/tests/normalization/examples/Optional/unzip/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Optional/unzip/1B.dhall @@ -0,0 +1,1 @@ +{ _1 = [] : Optional Text, _2 = [] : Optional Bool } diff --git a/tests/normalization/examples/Text/concat/0A.dhall b/tests/normalization/examples/Text/concat/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Text/concat/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Text/concat [ "ABC", "DEF", "GHI" ] diff --git a/tests/normalization/examples/Text/concat/0B.dhall b/tests/normalization/examples/Text/concat/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Text/concat/0B.dhall @@ -0,0 +1,1 @@ +"ABCDEFGHI" diff --git a/tests/normalization/examples/Text/concat/1A.dhall b/tests/normalization/examples/Text/concat/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Text/concat/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Text/concat ([] : List Text) diff --git a/tests/normalization/examples/Text/concat/1B.dhall b/tests/normalization/examples/Text/concat/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Text/concat/1B.dhall @@ -0,0 +1,1 @@ +"" diff --git a/tests/normalization/examples/Text/concatMap/0A.dhall b/tests/normalization/examples/Text/concatMap/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Text/concatMap/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Text/concatMap Integer (λ(n : Integer) → "${Integer/show n} ") [ 0, 1, 2 ] diff --git a/tests/normalization/examples/Text/concatMap/0B.dhall b/tests/normalization/examples/Text/concatMap/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Text/concatMap/0B.dhall @@ -0,0 +1,1 @@ +"0 1 2 " diff --git a/tests/normalization/examples/Text/concatMap/1A.dhall b/tests/normalization/examples/Text/concatMap/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Text/concatMap/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Text/concatMap Integer (λ(n : Integer) → "${Integer/show n} ") ([] : List Integer) diff --git a/tests/normalization/examples/Text/concatMap/1B.dhall b/tests/normalization/examples/Text/concatMap/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Text/concatMap/1B.dhall @@ -0,0 +1,1 @@ +"" diff --git a/tests/normalization/examples/Text/concatMapSep/0A.dhall b/tests/normalization/examples/Text/concatMapSep/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Text/concatMapSep/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Text/concatMapSep ", " Integer Integer/show [ 0, 1, 2 ] diff --git a/tests/normalization/examples/Text/concatMapSep/0B.dhall b/tests/normalization/examples/Text/concatMapSep/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Text/concatMapSep/0B.dhall @@ -0,0 +1,1 @@ +"0, 1, 2" diff --git a/tests/normalization/examples/Text/concatMapSep/1A.dhall b/tests/normalization/examples/Text/concatMapSep/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Text/concatMapSep/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Text/concatMapSep ", " Integer Integer/show ([] : List Integer) diff --git a/tests/normalization/examples/Text/concatMapSep/1B.dhall b/tests/normalization/examples/Text/concatMapSep/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Text/concatMapSep/1B.dhall @@ -0,0 +1,1 @@ +"" diff --git a/tests/normalization/examples/Text/concatSep/0A.dhall b/tests/normalization/examples/Text/concatSep/0A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Text/concatSep/0A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Text/concatSep ", " [ "ABC", "DEF", "GHI" ] diff --git a/tests/normalization/examples/Text/concatSep/0B.dhall b/tests/normalization/examples/Text/concatSep/0B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Text/concatSep/0B.dhall @@ -0,0 +1,1 @@ +"ABC, DEF, GHI" diff --git a/tests/normalization/examples/Text/concatSep/1A.dhall b/tests/normalization/examples/Text/concatSep/1A.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Text/concatSep/1A.dhall @@ -0,0 +1,1 @@ +../../../../../Prelude/Text/concatSep ", " ([] : List Text) diff --git a/tests/normalization/examples/Text/concatSep/1B.dhall b/tests/normalization/examples/Text/concatSep/1B.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/examples/Text/concatSep/1B.dhall @@ -0,0 +1,1 @@ +"" diff --git a/tests/normalization/listBuildA.dhall b/tests/normalization/listBuildA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/listBuildA.dhall @@ -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)) + ) +} diff --git a/tests/normalization/listBuildB.dhall b/tests/normalization/listBuildB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/listBuildB.dhall @@ -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 ] +} diff --git a/tests/normalization/naturalBuildA.dhall b/tests/normalization/naturalBuildA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/naturalBuildA.dhall @@ -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) + ) +} diff --git a/tests/normalization/naturalBuildB.dhall b/tests/normalization/naturalBuildB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/naturalBuildB.dhall @@ -0,0 +1,7 @@ +{ example0 = + +1 +, example1 = + +1 +, example2 = + λ(id : ∀(a : Type) → a → a) → id Natural +1 +} diff --git a/tests/normalization/optionalBuildA.dhall b/tests/normalization/optionalBuildA.dhall --- a/tests/normalization/optionalBuildA.dhall +++ b/tests/normalization/optionalBuildA.dhall @@ -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 + ) } diff --git a/tests/normalization/optionalBuildB.dhall b/tests/normalization/optionalBuildB.dhall --- a/tests/normalization/optionalBuildB.dhall +++ b/tests/normalization/optionalBuildB.dhall @@ -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 } diff --git a/tests/normalization/optionalBuildFoldA.dhall b/tests/normalization/optionalBuildFoldA.dhall --- a/tests/normalization/optionalBuildFoldA.dhall +++ b/tests/normalization/optionalBuildFoldA.dhall @@ -1,11 +1,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)) diff --git a/tests/normalization/optionalBuildFoldB.dhall b/tests/normalization/optionalBuildFoldB.dhall --- a/tests/normalization/optionalBuildFoldB.dhall +++ b/tests/normalization/optionalBuildFoldB.dhall @@ -1,10 +1,1 @@ -{ example0 = - λ ( f - : ∀(optional : Type) - → ∀(just : Text → optional) - → ∀(nothing : optional) - → optional - ) - → f -, example1 = [ "foo" ] : Optional Text -} +[ "foo" ] : Optional Text diff --git a/tests/normalization/remoteSystemsA.dhall b/tests/normalization/remoteSystemsA.dhall --- a/tests/normalization/remoteSystemsA.dhall +++ b/tests/normalization/remoteSystemsA.dhall @@ -1,8 +1,8 @@ let Text/concatMap = - https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Text/concatMap + ../../Prelude/Text/concatMap in let Text/concatSep = - https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Text/concatSep + ../../Prelude/Text/concatSep in let Row = { cores : diff --git a/tests/normalization/simplifications/andA.dhall b/tests/normalization/simplifications/andA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/simplifications/andA.dhall @@ -0,0 +1,6 @@ +{ example0 = λ(x : Bool) → x && True +, example1 = λ(x : Bool) → True && x +, example2 = λ(x : Bool) → x && False +, example3 = λ(x : Bool) → False && x +, example4 = λ(x : Bool) → x && x +} diff --git a/tests/normalization/simplifications/andB.dhall b/tests/normalization/simplifications/andB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/simplifications/andB.dhall @@ -0,0 +1,6 @@ +{ example0 = λ(x : Bool) → x +, example1 = λ(x : Bool) → x +, example2 = λ(x : Bool) → False +, example3 = λ(x : Bool) → False +, example4 = λ(x : Bool) → x +} diff --git a/tests/normalization/simplifications/eqA.dhall b/tests/normalization/simplifications/eqA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/simplifications/eqA.dhall @@ -0,0 +1,4 @@ +{ example0 = λ(x : Bool) → x == True +, example1 = λ(x : Bool) → True == x +, example2 = λ(x : Bool) → x == x +} diff --git a/tests/normalization/simplifications/eqB.dhall b/tests/normalization/simplifications/eqB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/simplifications/eqB.dhall @@ -0,0 +1,4 @@ +{ example0 = λ(x : Bool) → x +, example1 = λ(x : Bool) → x +, example2 = λ(x : Bool) → True +} diff --git a/tests/normalization/simplifications/ifThenElseA.dhall b/tests/normalization/simplifications/ifThenElseA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/simplifications/ifThenElseA.dhall @@ -0,0 +1,3 @@ +{ example0 = λ(x : Bool) → if x then True else False +, example1 = λ(x : Bool) → λ(y : Text) → if x then y else y +} diff --git a/tests/normalization/simplifications/ifThenElseB.dhall b/tests/normalization/simplifications/ifThenElseB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/simplifications/ifThenElseB.dhall @@ -0,0 +1,3 @@ +{ example0 = λ(x : Bool) → x +, example1 = λ(x : Bool) → λ(y : Text) → y +} diff --git a/tests/normalization/simplifications/neA.dhall b/tests/normalization/simplifications/neA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/simplifications/neA.dhall @@ -0,0 +1,4 @@ +{ example0 = λ(x : Bool) → x != False +, example1 = λ(x : Bool) → False != x +, example2 = λ(x : Bool) → x != x +} diff --git a/tests/normalization/simplifications/neB.dhall b/tests/normalization/simplifications/neB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/simplifications/neB.dhall @@ -0,0 +1,4 @@ +{ example0 = λ(x : Bool) → x +, example1 = λ(x : Bool) → x +, example2 = λ(x : Bool) → False +} diff --git a/tests/normalization/simplifications/orA.dhall b/tests/normalization/simplifications/orA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/simplifications/orA.dhall @@ -0,0 +1,6 @@ +{ example0 = λ(x : Bool) → x || True +, example1 = λ(x : Bool) → True || x +, example2 = λ(x : Bool) → x || False +, example3 = λ(x : Bool) → False || x +, example4 = λ(x : Bool) → x || x +} diff --git a/tests/normalization/simplifications/orB.dhall b/tests/normalization/simplifications/orB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/simplifications/orB.dhall @@ -0,0 +1,6 @@ +{ example0 = λ(x : Bool) → True +, example1 = λ(x : Bool) → True +, example2 = λ(x : Bool) → x +, example3 = λ(x : Bool) → x +, example4 = λ(x : Bool) → x +} diff --git a/tests/typecheck/anonymousFunctionsInTypesA.dhall b/tests/typecheck/anonymousFunctionsInTypesA.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/anonymousFunctionsInTypesA.dhall @@ -0,0 +1,5 @@ + let anonymousFunction = λ(a : Type) → List a + +in λ(HigherOrderType : (Type → Type) → Type) + → λ(x : HigherOrderType anonymousFunction) + → (x : HigherOrderType anonymousFunction) diff --git a/tests/typecheck/anonymousFunctionsInTypesB.dhall b/tests/typecheck/anonymousFunctionsInTypesB.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/anonymousFunctionsInTypesB.dhall @@ -0,0 +1,4 @@ + ∀(HigherOrderType : (Type → Type) → Type) +→ ∀(x : HigherOrderType (λ(a : Type) → List a)) +→ HigherOrderType (λ(a : Type) → List a) + diff --git a/tests/typecheck/examples/Monoid/00A.dhall b/tests/typecheck/examples/Monoid/00A.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/examples/Monoid/00A.dhall @@ -0,0 +1,1 @@ +../../../../Prelude/Bool/and diff --git a/tests/typecheck/examples/Monoid/00B.dhall b/tests/typecheck/examples/Monoid/00B.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/examples/Monoid/00B.dhall @@ -0,0 +1,1 @@ +../../../../Prelude/Monoid Bool diff --git a/tests/typecheck/examples/Monoid/01A.dhall b/tests/typecheck/examples/Monoid/01A.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/examples/Monoid/01A.dhall @@ -0,0 +1,1 @@ +../../../../Prelude/Bool/or diff --git a/tests/typecheck/examples/Monoid/01B.dhall b/tests/typecheck/examples/Monoid/01B.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/examples/Monoid/01B.dhall @@ -0,0 +1,1 @@ +../../../../Prelude/Monoid Bool diff --git a/tests/typecheck/examples/Monoid/02A.dhall b/tests/typecheck/examples/Monoid/02A.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/examples/Monoid/02A.dhall @@ -0,0 +1,1 @@ +../../../../Prelude/Bool/even diff --git a/tests/typecheck/examples/Monoid/02B.dhall b/tests/typecheck/examples/Monoid/02B.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/examples/Monoid/02B.dhall @@ -0,0 +1,1 @@ +../../../../Prelude/Monoid Bool diff --git a/tests/typecheck/examples/Monoid/03A.dhall b/tests/typecheck/examples/Monoid/03A.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/examples/Monoid/03A.dhall @@ -0,0 +1,1 @@ +../../../../Prelude/Bool/odd diff --git a/tests/typecheck/examples/Monoid/03B.dhall b/tests/typecheck/examples/Monoid/03B.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/examples/Monoid/03B.dhall @@ -0,0 +1,1 @@ +../../../../Prelude/Monoid Bool diff --git a/tests/typecheck/examples/Monoid/04A.dhall b/tests/typecheck/examples/Monoid/04A.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/examples/Monoid/04A.dhall @@ -0,0 +1,1 @@ +../../../../Prelude/List/concat diff --git a/tests/typecheck/examples/Monoid/04B.dhall b/tests/typecheck/examples/Monoid/04B.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/examples/Monoid/04B.dhall @@ -0,0 +1,1 @@ +∀(a : Type) → ../../../../Prelude/Monoid (List a) diff --git a/tests/typecheck/examples/Monoid/05A.dhall b/tests/typecheck/examples/Monoid/05A.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/examples/Monoid/05A.dhall @@ -0,0 +1,1 @@ +../../../../Prelude/List/shifted diff --git a/tests/typecheck/examples/Monoid/05B.dhall b/tests/typecheck/examples/Monoid/05B.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/examples/Monoid/05B.dhall @@ -0,0 +1,1 @@ +∀(a : Type) → ../../../../Prelude/Monoid (List { index : Natural, value : a }) diff --git a/tests/typecheck/examples/Monoid/06A.dhall b/tests/typecheck/examples/Monoid/06A.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/examples/Monoid/06A.dhall @@ -0,0 +1,1 @@ +../../../../Prelude/Natural/sum diff --git a/tests/typecheck/examples/Monoid/06B.dhall b/tests/typecheck/examples/Monoid/06B.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/examples/Monoid/06B.dhall @@ -0,0 +1,1 @@ +../../../../Prelude/Monoid Natural diff --git a/tests/typecheck/examples/Monoid/07A.dhall b/tests/typecheck/examples/Monoid/07A.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/examples/Monoid/07A.dhall @@ -0,0 +1,1 @@ +../../../../Prelude/Natural/product diff --git a/tests/typecheck/examples/Monoid/07B.dhall b/tests/typecheck/examples/Monoid/07B.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/examples/Monoid/07B.dhall @@ -0,0 +1,1 @@ +../../../../Prelude/Monoid Natural diff --git a/tests/typecheck/examples/Monoid/08A.dhall b/tests/typecheck/examples/Monoid/08A.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/examples/Monoid/08A.dhall @@ -0,0 +1,1 @@ +../../../../Prelude/Optional/head diff --git a/tests/typecheck/examples/Monoid/08B.dhall b/tests/typecheck/examples/Monoid/08B.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/examples/Monoid/08B.dhall @@ -0,0 +1,1 @@ +∀(a : Type) → ../../../../Prelude/Monoid (Optional a) diff --git a/tests/typecheck/examples/Monoid/09A.dhall b/tests/typecheck/examples/Monoid/09A.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/examples/Monoid/09A.dhall @@ -0,0 +1,1 @@ +../../../../Prelude/Optional/last diff --git a/tests/typecheck/examples/Monoid/09B.dhall b/tests/typecheck/examples/Monoid/09B.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/examples/Monoid/09B.dhall @@ -0,0 +1,1 @@ +∀(a : Type) → ../../../../Prelude/Monoid (Optional a) diff --git a/tests/typecheck/examples/Monoid/10A.dhall b/tests/typecheck/examples/Monoid/10A.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/examples/Monoid/10A.dhall @@ -0,0 +1,1 @@ +../../../../Prelude/Text/concat diff --git a/tests/typecheck/examples/Monoid/10B.dhall b/tests/typecheck/examples/Monoid/10B.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/examples/Monoid/10B.dhall @@ -0,0 +1,1 @@ +../../../../Prelude/Monoid Text