Normalization.hs

{-# LANGUAGE OverloadedStrings #-}

module Dhall.Test.Normalization where

import Data.Text       (Text)
import Data.Void       (Void)
import Dhall.Core      (Expr (..), Var (..), throws)
import System.FilePath ((</>))
import Test.Tasty      (TestTree)

import qualified Data.Text        as Text
import qualified Data.Text.IO     as Text.IO
import qualified Dhall.Context    as Context
import qualified Dhall.Core       as Core
import qualified Dhall.Import     as Import
import qualified Dhall.Parser     as Parser
import qualified Dhall.Test.Util  as Test.Util
import qualified Dhall.TypeCheck  as TypeCheck
import qualified System.FilePath  as FilePath
import qualified Test.Tasty       as Tasty
import qualified Test.Tasty.HUnit as Tasty.HUnit
import qualified Turtle

normalizationDirectory :: FilePath
normalizationDirectory = "./dhall-lang/tests/normalization/success"

unitDirectory :: FilePath
unitDirectory = normalizationDirectory </> "unit/"

getTests :: IO TestTree
getTests = do
    let pattern = Turtle.chars <* "A.dhall"

    let normalizationFiles = do
            path <- FilePath.normalise <$> Turtle.lstree normalizationDirectory

            unitDirectory `Test.Util.pathNotPrefixOf` path

            return path

    betaNormalizationTests <- Test.Util.discover pattern betaNormalizationTest normalizationFiles

    alphaNormalizationTests <-
        Test.Util.discover pattern alphaNormalizationTest
            (Turtle.lstree "./dhall-lang/tests/alpha-normalization/success/")

    let unitTestFiles = Turtle.lstree unitDirectory

    unitTests <- Test.Util.discover pattern unitTest unitTestFiles

    let testTree =
            Tasty.testGroup "normalization"
                [ Tasty.testGroup "beta-normalization"
                    [ betaNormalizationTests
                    ]
                , Tasty.testGroup "unit tests"
                    [ unitTests
                    ]
                , Tasty.testGroup "alpha-normalization"
                    [ alphaNormalizationTests
                    ]
                , customization
                ]

    return testTree

customization :: TestTree
customization =
    Tasty.testGroup "customization"
        [ simpleCustomization
        , nestedReduction
        ]

simpleCustomization :: TestTree
simpleCustomization = Tasty.HUnit.testCase "simpleCustomization" $ do
    let tyCtx =
            Context.insert
                "min"
                (Pi mempty "_" Natural (Pi mempty "_" Natural Natural))
                Context.empty

        valCtx e =
            case e of
                App (App (Var (V "min" 0)) (NaturalLit x)) (NaturalLit y) ->
                    pure (Just (NaturalLit (min x y)))
                _ ->
                    pure Nothing

    e <- Test.Util.codeWith tyCtx "min (min 11 12) 8 + 1"

    Test.Util.assertNormalizesToWith valCtx e "9"

nestedReduction :: TestTree
nestedReduction = Tasty.HUnit.testCase "doubleReduction" $ do
    minType        <- Context.insert "min"        <$> Test.Util.code "Natural → Natural → Natural"
    fiveorlessType <- Context.insert "fiveorless" <$> Test.Util.code "Natural → Natural"
    wurbleType     <- Context.insert "wurble"     <$> Test.Util.code "Natural → Natural"

    let tyCtx = minType . fiveorlessType . wurbleType $ Context.empty

        valCtx e =
            case e of
                App (App (Var (V "min" 0)) (NaturalLit x)) (NaturalLit y) ->
                    pure (Just (NaturalLit (min x y)))
                App (Var (V "wurble" 0)) (NaturalLit x) ->
                    pure (Just (App (Var (V "fiveorless" 0)) (NaturalPlus (NaturalLit x) (NaturalLit 2))))
                App (Var (V "fiveorless" 0)) (NaturalLit x) ->
                    pure (Just (App (App (Var (V "min" 0)) (NaturalLit x)) (NaturalPlus (NaturalLit 3) (NaturalLit 2))))
                _ ->
                    pure Nothing

    e <- Test.Util.codeWith tyCtx "wurble 6"

    Test.Util.assertNormalizesToWith valCtx e "5"

alphaNormalizationTest :: Text -> TestTree
alphaNormalizationTest prefix = do
    let prefixString = Text.unpack prefix

    Tasty.HUnit.testCase prefixString $ do
        let actualPath   = prefixString <> "A.dhall"
        let expectedPath = prefixString <> "B.dhall"

        actualCode   <- Text.IO.readFile actualPath
        expectedCode <- Text.IO.readFile expectedPath

        actualExpr <- throws (Parser.exprFromText mempty actualCode)

        actualResolved <- Import.assertNoImports actualExpr

        let actualNormalized = Core.alphaNormalize (Core.denote actualResolved)

        expectedExpr <- throws (Parser.exprFromText mempty expectedCode)

        expectedResolved <- Import.assertNoImports expectedExpr

        let expectedNormalized = Core.denote expectedResolved :: Expr Void Void

        let message =
                "The alpha-normalized expression did not match the expected output"

        Tasty.HUnit.assertEqual message expectedNormalized actualNormalized

{- Unit tests don't type-check, so we only verify that they normalize to the
   expected output
-}
unitTest :: Text -> TestTree
unitTest prefix = do
    let expectedFailures = []

    let prefixString = Text.unpack prefix

    Test.Util.testCase prefix expectedFailures $ do
        let actualPath   = prefixString <> "A.dhall"
        let expectedPath = prefixString <> "B.dhall"

        actualCode   <- Text.IO.readFile actualPath
        expectedCode <- Text.IO.readFile expectedPath

        actualExpr <- throws (Parser.exprFromText mempty actualCode)

        actualResolved <- Import.assertNoImports actualExpr

        let actualNormalized =
                Core.alphaNormalize
                    (Core.normalize actualResolved :: Expr Void Void)

        expectedExpr <- throws (Parser.exprFromText mempty expectedCode)

        expectedResolved <- Import.assertNoImports expectedExpr

        let expectedNormalized =
                Core.alphaNormalize (Core.denote expectedResolved)

        let message =
                "The normalized expression did not match the expected output"

        Tasty.HUnit.assertEqual message expectedNormalized actualNormalized

betaNormalizationTest :: Text -> TestTree
betaNormalizationTest prefix = do
    let prefixString = Text.unpack prefix

    Tasty.HUnit.testCase prefixString $ do
        let actualCode = Test.Util.toDhallPath (prefix <> "A.dhall")

        let expectedPath = prefixString <> "B.dhall"
        expectedCode <- Text.IO.readFile expectedPath

        actualExpr <- throws (Parser.exprFromText mempty actualCode)

        actualResolved <- Import.load actualExpr

        _ <- throws (TypeCheck.typeOf actualResolved)

        let actualNormalized =
                Core.alphaNormalize
                    (Core.normalize actualResolved :: Expr Void Void)

        expectedExpr <- throws (Parser.exprFromText mempty expectedCode)

        expectedResolved <- Import.load expectedExpr

        _ <- throws (TypeCheck.typeOf expectedResolved)

        -- Use `denote` instead of `normalize` to enforce that the expected
        -- expression is already in normal form
        let expectedNormalized =
                Core.alphaNormalize (Core.denote expectedResolved)

        let message =
                "The beta-normalized expression did not match the expected output"

        Tasty.HUnit.assertEqual message expectedNormalized actualNormalized