Skip to content

Make isNormalized consistent with normalize #1115

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Jul 17, 2019
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions dhall/dhall.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -538,6 +538,7 @@ Library
containers >= 0.5.0.0 && < 0.7 ,
contravariant < 1.6 ,
cryptonite >= 0.23 && < 1.0 ,
deepseq < 1.5 ,
Diff >= 0.2 && < 0.4 ,
directory >= 1.2.2.0 && < 1.4 ,
dotgen >= 0.4.2 && < 0.5 ,
Expand Down Expand Up @@ -686,6 +687,7 @@ Test-Suite tasty
QuickCheck >= 2.10 && < 2.14,
quickcheck-instances >= 0.3.12 && < 0.4 ,
serialise ,
spoon < 0.4 ,
tasty >= 0.11.2 && < 1.3 ,
tasty-hunit >= 0.9.2 && < 0.11,
tasty-quickcheck >= 0.9.2 && < 0.11,
Expand Down
76 changes: 38 additions & 38 deletions dhall/src/Dhall/Core.hs
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveTraversable #-}
Expand Down Expand Up @@ -68,6 +69,7 @@ module Dhall.Core (
import Control.Applicative (Applicative(..), (<$>))
#endif
import Control.Applicative (empty)
import Control.DeepSeq (NFData)
import Control.Exception (Exception)
import Control.Monad.IO.Class (MonadIO(..))
import Crypto.Hash (SHA256)
Expand Down Expand Up @@ -126,7 +128,7 @@ import qualified Text.Printf
Dhall is not a dependently typed language
-}
data Const = Type | Kind | Sort
deriving (Show, Eq, Ord, Data, Bounded, Enum, Generic)
deriving (Show, Eq, Ord, Data, Bounded, Enum, Generic, NFData)

instance Pretty Const where
pretty = Pretty.unAnnotate . prettyConst
Expand All @@ -138,7 +140,7 @@ instance Pretty Const where
@Directory { components = [ "baz", "bar", "foo" ] }@
-}
newtype Directory = Directory { components :: [Text] }
deriving (Eq, Generic, Ord, Show)
deriving (Eq, Generic, Ord, Show, NFData)

instance Semigroup Directory where
Directory components₀ <> Directory components₁ =
Expand All @@ -153,7 +155,7 @@ instance Pretty Directory where
data File = File
{ directory :: Directory
, file :: Text
} deriving (Eq, Generic, Ord, Show)
} deriving (Eq, Generic, Ord, Show, NFData)

instance Pretty File where
pretty (File {..}) =
Expand All @@ -174,23 +176,23 @@ data FilePrefix
-- ^ Path relative to @..@
| Home
-- ^ Path relative to @~@
deriving (Eq, Generic, Ord, Show)
deriving (Eq, Generic, Ord, Show, NFData)

instance Pretty FilePrefix where
pretty Absolute = ""
pretty Here = "."
pretty Parent = ".."
pretty Home = "~"

data Scheme = HTTP | HTTPS deriving (Eq, Generic, Ord, Show)
data Scheme = HTTP | HTTPS deriving (Eq, Generic, Ord, Show, NFData)

data URL = URL
{ scheme :: Scheme
, authority :: Text
, path :: File
, query :: Maybe Text
, headers :: Maybe (Expr Src Import)
} deriving (Eq, Generic, Ord, Show)
} deriving (Eq, Generic, Ord, Show, NFData)

instance Pretty URL where
pretty (URL {..}) =
Expand Down Expand Up @@ -228,7 +230,7 @@ data ImportType
| Env Text
-- ^ Environment variable
| Missing
deriving (Eq, Generic, Ord, Show)
deriving (Eq, Generic, Ord, Show, NFData)

parent :: File
parent = File { directory = Directory { components = [ ".." ] }, file = "" }
Expand Down Expand Up @@ -267,13 +269,13 @@ instance Pretty ImportType where

-- | How to interpret the import's contents (i.e. as Dhall code or raw text)
data ImportMode = Code | RawText | Location
deriving (Eq, Generic, Ord, Show)
deriving (Eq, Generic, Ord, Show, NFData)

-- | A `ImportType` extended with an optional hash for semantic integrity checks
data ImportHashed = ImportHashed
{ hash :: Maybe (Crypto.Hash.Digest SHA256)
, importType :: ImportType
} deriving (Eq, Generic, Ord, Show)
} deriving (Eq, Generic, Ord, Show, NFData)

instance Semigroup ImportHashed where
ImportHashed _ importType₀ <> ImportHashed hash importType₁ =
Expand All @@ -289,7 +291,7 @@ instance Pretty ImportHashed where
data Import = Import
{ importHashed :: ImportHashed
, importMode :: ImportMode
} deriving (Eq, Generic, Ord, Show)
} deriving (Eq, Generic, Ord, Show, NFData)

instance Semigroup Import where
Import importHashed₀ _ <> Import importHashed₁ code =
Expand Down Expand Up @@ -337,7 +339,7 @@ instance Pretty Import where
appear as a numeric suffix.
-}
data Var = V Text !Int
deriving (Data, Generic, Eq, Ord, Show)
deriving (Data, Generic, Eq, Ord, Show, NFData)

instance IsString Var where
fromString str = V (fromString str) 0
Expand Down Expand Up @@ -484,7 +486,9 @@ data Expr s a
| ImportAlt (Expr s a) (Expr s a)
-- | > Embed import ~ import
| Embed a
deriving (Eq, Ord, Foldable, Generic, Traversable, Show, Data)
deriving (Eq, Ord, Foldable, Generic, Traversable, Show, Data, NFData)
-- NB: If you add a constructor to Expr, please also update the Arbitrary
-- instance in Dhall.Test.QuickCheck.

-- This instance is hand-written due to the fact that deriving
-- it does not give us an INLINABLE pragma. We annotate this fmap
Expand Down Expand Up @@ -710,7 +714,7 @@ data Binding s a = Binding
{ variable :: Text
, annotation :: Maybe (Expr s a)
, value :: Expr s a
} deriving (Functor, Foldable, Generic, Traversable, Show, Eq, Ord, Data)
} deriving (Functor, Foldable, Generic, Traversable, Show, Eq, Ord, Data, NFData)

instance Bifunctor Binding where
first k (Binding a b c) = Binding a (fmap (first k) b) (first k c)
Expand All @@ -719,7 +723,7 @@ instance Bifunctor Binding where

-- | The body of an interpolated @Text@ literal
data Chunks s a = Chunks [(Text, Expr s a)] Text
deriving (Functor, Foldable, Generic, Traversable, Show, Eq, Ord, Data)
deriving (Functor, Foldable, Generic, Traversable, Show, Eq, Ord, Data, NFData)

instance Data.Semigroup.Semigroup (Chunks s a) where
Chunks xysL zL <> Chunks [] zR =
Expand Down Expand Up @@ -1754,6 +1758,11 @@ isNormalizedWith :: (Eq s, Eq a) => Normalizer a -> Expr s a -> Bool
isNormalizedWith ctx e = e == normalizeWith (Just (ReifiedNormalizer ctx)) e

-- | Quickly check if an expression is in normal form
--
-- Given a well-typed expression @e@, @'isNormalized' e@ is equivalent to
-- @e == 'normalize' e@.
--
-- Given an ill-typed expression, 'isNormalized' may return 'True' or 'False'.
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@Gabriel439 What do you think about this "contract"?

Otherwise I'd propose returning a Maybe Bool that is Nothing when normalization should fail.

Or maybe a custom type like data Normalized = NormalForm | NonNormalForm | IllTyped or so?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've played around with a Maybe Bool-version of isNormalized a bit. It seems rather tricky to nail down the consistency with normalize though. I think this should wait until normalize itself is more principled, possibly after the NbE changes.

isNormalized :: Eq a => Expr s a -> Bool
isNormalized e0 = loop (denote e0)
where
Expand All @@ -1775,6 +1784,7 @@ isNormalized e0 = loop (denote e0)
App (App OptionalBuild _) (App (App OptionalFold _) _) -> False

App (App (App (App NaturalFold (NaturalLit _)) _) _) _ -> False
App NaturalFold (NaturalLit _) -> False
App NaturalBuild _ -> False
App NaturalIsZero (NaturalLit _) -> False
App NaturalEven (NaturalLit _) -> False
Expand Down Expand Up @@ -1921,30 +1931,20 @@ isNormalized e0 = loop (denote e0)
Nothing -> True
_ -> True
_ -> True
ToMap x t -> loop x && all loop t
Field r x -> loop r &&
case r of
RecordLit kvs ->
case Dhall.Map.lookup x kvs of
Just _ -> False
Nothing -> True
Union kvs ->
case Dhall.Map.lookup x kvs of
Just _ -> False
Nothing -> True
_ -> True
Project r xs -> loop r &&
case r of
RecordLit kvs ->
case xs of
Left s -> not (all (flip Dhall.Map.member kvs) s) && Dhall.Set.isSorted s
Right e' ->
case e' of
Record kts ->
loop (Project r (Left (Dhall.Set.fromSet (Dhall.Map.keysSet kts))))
_ ->
False
_ -> not (null xs)
ToMap x t -> case x of
RecordLit _ -> False
_ -> loop x && all loop t
Field r _ -> case r of
RecordLit _ -> False
_ -> loop r
Project r p -> loop r &&
case p of
Left s -> case r of
RecordLit _ -> False
_ -> not (Dhall.Set.null s) && Dhall.Set.isSorted s
Right e' -> case e' of
Record _ -> False
_ -> loop e'
Note _ e' -> loop e'
ImportAlt l _r -> loop l
Embed _ -> True
Expand Down
8 changes: 6 additions & 2 deletions dhall/src/Dhall/Map.hs
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeFamilies #-}
Expand Down Expand Up @@ -63,8 +65,10 @@ module Dhall.Map
) where

import Control.Applicative ((<|>))
import Control.DeepSeq (NFData)
import Data.Data (Data)
import Data.Semigroup
import GHC.Generics (Generic)
import Prelude hiding (filter, lookup)

import qualified Data.List
Expand All @@ -81,12 +85,12 @@ import qualified Prelude
and also to improve performance
-}
data Map k v = Map (Data.Map.Map k v) (Keys k)
deriving (Data)
deriving (Data, Generic, NFData)

data Keys a
= Sorted
| Original [a]
deriving (Data)
deriving (Data, Generic, NFData)

instance (Ord k, Eq v) => Eq (Map k v) where
m1 == m2 =
Expand Down
16 changes: 14 additions & 2 deletions dhall/src/Dhall/Set.hs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}

-- | This module only exports ways of constructing a Set,
Expand All @@ -18,9 +19,11 @@ module Dhall.Set (
, difference
, sort
, isSorted
, null
) where

import Prelude
import Prelude hiding (null)
import Control.DeepSeq (NFData)
import Data.List (foldl')
import Data.Sequence (Seq, (|>))
import Data.Data (Data)
Expand All @@ -31,7 +34,7 @@ import qualified Data.Sequence
import qualified Data.Foldable

data Set a = Set (Data.Set.Set a) (Seq a)
deriving (Eq, Generic, Ord, Show, Data)
deriving (Eq, Generic, Ord, Show, Data, NFData)

instance Foldable Set where
foldMap f = foldMap f . toSeq
Expand Down Expand Up @@ -85,3 +88,12 @@ True
-}
isSorted :: Ord a => Set a -> Bool
isSorted s = toList s == Data.Set.toList (toSet s)

{-|
>>> null (fromList [1])
False
>>> null (fromList [])
True
-}
null :: Set a -> Bool
null (Set s _) = Data.Set.null s
4 changes: 3 additions & 1 deletion dhall/src/Dhall/Src.hs
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}
Expand All @@ -9,6 +10,7 @@ module Dhall.Src
Src(..)
) where

import Control.DeepSeq (NFData)
import Data.Data (Data)
import Data.Monoid ((<>))
import Data.Text (Text)
Expand All @@ -25,7 +27,7 @@ import qualified Text.Printf as Printf
-- | Source code extract
data Src = Src !SourcePos !SourcePos Text
-- Text field is intentionally lazy
deriving (Data, Eq, Generic, Ord, Show)
deriving (Data, Eq, Generic, Ord, Show, NFData)

instance Pretty Src where
pretty (Src begin _ text) =
Expand Down
Loading