Add new Dhall.Map module
#612
+752
−208
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -24,8 +24,8 @@ module Dhall.TypeCheck ( | ||
| import Control.Exception (Exception) | ||
| import Data.Data (Data(..)) | ||
| import Data.Foldable (forM_, toList) | ||
| import Data.Sequence (Seq, ViewL(..)) | ||
| import Data.Semigroup (Semigroup(..)) | ||
|
There was a problem hiding this comment. There is an ambiguous occurrence between the There was a problem hiding this comment. Also happens in |
||
| import Data.Set (Set) | ||
| import Data.Text (Text) | ||
| import Data.Text.Prettyprint.Doc (Doc, Pretty(..)) | ||
| @@ -36,8 +36,6 @@ import Dhall.Context (Context) | ||
| import Dhall.Pretty (Ann, layoutOpts) | ||
|
|
||
| import qualified Data.Foldable | ||
| import qualified Data.Sequence | ||
| import qualified Data.Set | ||
| import qualified Data.Text as Text | ||
| @@ -46,6 +44,7 @@ import qualified Data.Text.Prettyprint.Doc.Render.String as Pretty | ||
| import qualified Dhall.Context | ||
| import qualified Dhall.Core | ||
| import qualified Dhall.Diff | ||
| import qualified Dhall.Map | ||
| import qualified Dhall.Pretty.Internal | ||
| import qualified Dhall.Util | ||
|
|
||
| @@ -425,7 +424,7 @@ typeWithA tpa = loop | ||
| return | ||
| (Pi "a" (Const Type) | ||
| (Pi "_" (App List "a") | ||
| (App List (Record (Dhall.Map.fromList kts))) ) ) | ||
| loop _ ListReverse = do | ||
| return (Pi "a" (Const Type) (Pi "_" (App List "a") (App List "a"))) | ||
| loop _ Optional = do | ||
| @@ -468,9 +467,9 @@ typeWithA tpa = loop | ||
| (Pi "just" (Pi "_" "a" "optional") | ||
| (Pi "nothing" "optional" "optional") ) | ||
| loop ctx e@(Record kts ) = do | ||
| case Dhall.Map.uncons kts of | ||
| Nothing -> return (Const Type) | ||
| Just (k0, t0, rest) -> do | ||
| s0 <- fmap Dhall.Core.normalize (loop ctx t0) | ||
| c <- case s0 of | ||
| Const Type -> | ||
| @@ -479,7 +478,7 @@ typeWithA tpa = loop | ||
| | Dhall.Core.judgmentallyEqual t0 (Const Type) -> | ||
| return Kind | ||
| _ -> Left (TypeError ctx e (InvalidFieldType k0 t0)) | ||
| let process k t = do | ||
| s <- fmap Dhall.Core.normalize (loop ctx t) | ||
| case s of | ||
| Const Type -> | ||
| @@ -495,11 +494,11 @@ typeWithA tpa = loop | ||
| else Left (TypeError ctx e (FieldAnnotationMismatch k t k0 t0 Kind)) | ||
| _ -> | ||
| Left (TypeError ctx e (InvalidFieldType k t)) | ||
| Dhall.Map.traverseWithKey_ process rest | ||
| return (Const c) | ||
| loop ctx e@(RecordLit kvs ) = do | ||
| case Dhall.Map.toList kvs of | ||
| [] -> return (Record mempty) | ||
| (k0, v0):_ -> do | ||
| t0 <- loop ctx v0 | ||
| s0 <- fmap Dhall.Core.normalize (loop ctx t0) | ||
| @@ -529,7 +528,7 @@ typeWithA tpa = loop | ||
| Left (TypeError ctx e (InvalidField k t)) | ||
|
|
||
| return t | ||
| kts <- Dhall.Map.traverseWithKey process kvs | ||
| return (Record kts) | ||
| loop ctx e@(Union kts ) = do | ||
| let process k t = do | ||
| @@ -538,20 +537,14 @@ typeWithA tpa = loop | ||
| Const Type -> return () | ||
| Const Kind -> return () | ||
| _ -> Left (TypeError ctx e (InvalidAlternativeType k t)) | ||
| Dhall.Map.traverseWithKey_ process kts | ||
| return (Const Type) | ||
| loop ctx e@(UnionLit k v kts) = do | ||
| case Dhall.Map.lookup k kts of | ||
| Just _ -> Left (TypeError ctx e (DuplicateAlternative k)) | ||
| Nothing -> return () | ||
| t <- loop ctx v | ||
| let union = Union (Dhall.Map.insert k (Dhall.Core.normalize t) kts) | ||
| _ <- loop ctx union | ||
| return union | ||
| loop ctx e@(Combine kvsX kvsY) = do | ||
| @@ -581,12 +574,12 @@ typeWithA tpa = loop | ||
|
|
||
| let combineTypes ktsL ktsR = do | ||
| let ksL = | ||
| Data.Set.fromList (Dhall.Map.keys ktsL) | ||
| let ksR = | ||
| Data.Set.fromList (Dhall.Map.keys ktsR) | ||
| let ks = Data.Set.union ksL ksR | ||
| kts <- forM (toList ks) (\k -> do | ||
| case (Dhall.Map.lookup k ktsL, Dhall.Map.lookup k ktsR) of | ||
| (Just (Record ktsL'), Just (Record ktsR')) -> do | ||
| t <- combineTypes ktsL' ktsR' | ||
| return (k, t) | ||
| @@ -596,7 +589,7 @@ typeWithA tpa = loop | ||
| return (k, t) | ||
| _ -> do | ||
| Left (TypeError ctx e (FieldCollision k)) ) | ||
| return (Record (Dhall.Map.fromList kts)) | ||
|
|
||
| combineTypes ktsX ktsY | ||
| loop ctx e@(CombineTypes l r) = do | ||
| @@ -627,12 +620,12 @@ typeWithA tpa = loop | ||
|
|
||
| let combineTypes ktsL ktsR = do | ||
| let ksL = | ||
| Data.Set.fromList (Dhall.Map.keys ktsL) | ||
| let ksR = | ||
| Data.Set.fromList (Dhall.Map.keys ktsR) | ||
| let ks = Data.Set.union ksL ksR | ||
| forM_ (toList ks) (\k -> do | ||
| case (Dhall.Map.lookup k ktsL, Dhall.Map.lookup k ktsR) of | ||
| (Just (Record ktsL'), Just (Record ktsR')) -> do | ||
| combineTypes ktsL' ktsR' | ||
| (Nothing, Just _) -> do | ||
| @@ -670,21 +663,21 @@ typeWithA tpa = loop | ||
| then return () | ||
| else Left (TypeError ctx e (RecordMismatch '⫽' kvsX kvsY constX constY)) | ||
|
|
||
| return (Record (Dhall.Map.union ktsY ktsX)) | ||
| loop ctx e@(Merge kvsX kvsY (Just t)) = do | ||
| _ <- loop ctx t | ||
|
|
||
| tKvsX <- fmap Dhall.Core.normalize (loop ctx kvsX) | ||
| ktsX <- case tKvsX of | ||
| Record kts -> return kts | ||
| _ -> Left (TypeError ctx e (MustMergeARecord kvsX tKvsX)) | ||
| let ksX = Data.Set.fromList (Dhall.Map.keys ktsX) | ||
|
|
||
| tKvsY <- fmap Dhall.Core.normalize (loop ctx kvsY) | ||
| ktsY <- case tKvsY of | ||
| Union kts -> return kts | ||
| _ -> Left (TypeError ctx e (MustMergeUnion kvsY tKvsY)) | ||
| let ksY = Data.Set.fromList (Dhall.Map.keys ktsY) | ||
|
|
||
| let diffX = Data.Set.difference ksX ksY | ||
| let diffY = Data.Set.difference ksY ksX | ||
| @@ -694,7 +687,7 @@ typeWithA tpa = loop | ||
| else Left (TypeError ctx e (UnusedHandler diffX)) | ||
|
|
||
| let process (kY, tY) = do | ||
| case Dhall.Map.lookup kY ktsX of | ||
| Nothing -> Left (TypeError ctx e (MissingHandler diffY)) | ||
| Just tX -> | ||
| case tX of | ||
| @@ -707,20 +700,20 @@ typeWithA tpa = loop | ||
| then return () | ||
| else Left (TypeError ctx e (InvalidHandlerOutputType kY t t'')) | ||
| _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX)) | ||
| mapM_ process (Dhall.Map.toList ktsY) | ||
| return t | ||
| loop ctx e@(Merge kvsX kvsY Nothing) = do | ||
| tKvsX <- fmap Dhall.Core.normalize (loop ctx kvsX) | ||
| ktsX <- case tKvsX of | ||
| Record kts -> return kts | ||
| _ -> Left (TypeError ctx e (MustMergeARecord kvsX tKvsX)) | ||
| let ksX = Data.Set.fromList (Dhall.Map.keys ktsX) | ||
|
|
||
| tKvsY <- fmap Dhall.Core.normalize (loop ctx kvsY) | ||
| ktsY <- case tKvsY of | ||
| Union kts -> return kts | ||
| _ -> Left (TypeError ctx e (MustMergeUnion kvsY tKvsY)) | ||
| let ksY = Data.Set.fromList (Dhall.Map.keys ktsY) | ||
|
|
||
| let diffX = Data.Set.difference ksX ksY | ||
| let diffY = Data.Set.difference ksY ksX | ||
| @@ -729,12 +722,12 @@ typeWithA tpa = loop | ||
| then return () | ||
| else Left (TypeError ctx e (UnusedHandler diffX)) | ||
|
|
||
| (kX, t) <- case Dhall.Map.toList ktsX of | ||
| [] -> Left (TypeError ctx e MissingMergeType) | ||
| (kX, Pi y _ t):_ -> return (kX, Dhall.Core.shift (-1) (V y 0) t) | ||
| (kX, tX ):_ -> Left (TypeError ctx e (HandlerNotAFunction kX tX)) | ||
| let process (kY, tY) = do | ||
| case Dhall.Map.lookup kY ktsX of | ||
| Nothing -> Left (TypeError ctx e (MissingHandler diffY)) | ||
| Just tX -> | ||
| case tX of | ||
| @@ -747,7 +740,7 @@ typeWithA tpa = loop | ||
| then return () | ||
| else Left (TypeError ctx e (HandlerOutputTypeMismatch kX t kY t'')) | ||
| _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX)) | ||
| mapM_ process (Dhall.Map.toList ktsY) | ||
| return t | ||
| loop ctx e@(Constructors t ) = do | ||
| _ <- loop ctx t | ||
| @@ -758,14 +751,14 @@ typeWithA tpa = loop | ||
|
|
||
| let adapt k t_ = Pi k t_ (Union kts) | ||
|
|
||
| return (Record (Dhall.Map.mapWithKey adapt kts)) | ||
| loop ctx e@(Field r x ) = do | ||
| t <- fmap Dhall.Core.normalize (loop ctx r) | ||
| case t of | ||
| Record kts -> do | ||
| _ <- loop ctx t | ||
|
|
||
| case Dhall.Map.lookup x kts of | ||
| Just t' -> return t' | ||
| Nothing -> Left (TypeError ctx e (MissingField x t)) | ||
| _ -> do | ||
| @@ -778,10 +771,10 @@ typeWithA tpa = loop | ||
| _ <- loop ctx t | ||
|
|
||
| let process k = | ||
| case Dhall.Map.lookup k kts of | ||
| Just t' -> return (k, t') | ||
| Nothing -> Left (TypeError ctx e (MissingField k t)) | ||
| let adapt = Record . Dhall.Map.fromList | ||
| fmap adapt (traverse process (Data.Set.toList xs)) | ||
| _ -> do | ||
| let text = Dhall.Pretty.Internal.docToStrictText (Dhall.Pretty.Internal.prettyLabels xs) | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think it's worth adding a comment noting that this annotation is the whole reason why this instance isn't derived.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
#620