ehmry/dhall-haskell
ehmry/dhall-haskell
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Union Access (#657)

Browse Source 
Addressing phase 1 of https://github.com/dhall-lang/dhall-lang/issues/244 and https://github.com/dhall-lang/dhall-haskell/issues/635 

@Gabriel439: I haven't implemented any tests for this and I should but is there documentation of how the tests are laid out? I'm slightly confused but possibly it'd be fine if I spent some more time looking through them :)
This commit is contained in:
Fintan Halpenny 2018-10-26 11:07:11 +01:00 committed by GitHub
parent 01d6cad27f
commit 8cad992639
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
13 changed files with 131 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
dhall.cabal
View File

@ -29,6 +29,7 @@ Extra-Source-Files:
tests/format/*.dhall
tests/normalization/tutorial/combineTypes/*.dhall
tests/normalization/tutorial/projection/*.dhall
tests/normalization/tutorial/access/*.dhall
tests/normalization/*.dhall
tests/normalization/examples/Bool/and/*.dhall
tests/normalization/examples/Bool/build/*.dhall
@ -96,6 +97,7 @@ Extra-Source-Files:
tests/typecheck/*.dhall
tests/typecheck/failure/*.dhall
tests/typecheck/examples/Monoid/*.dhall
tests/typecheck/access/*.dhall
tests/import/*.dhall
tests/import/data/foo/bar/a.dhall
benchmark/examples/*.dhall

11
src/Dhall/Core.hs
View File

@ -1829,6 +1829,13 @@ normalizeWith ctx e0 = loop (denote e0)
case Dhall.Map.lookup x kvs of
Just v -> loop v
Nothing -> Field (RecordLit (fmap loop kvs)) x
Union kvs ->
case Dhall.Map.lookup x kvs of
Just t_ -> Lam x t' (UnionLit x (Var (V x 0)) rest)
where
t' = loop t_
rest = Dhall.Map.delete x kvs
Nothing -> Field (Union (fmap loop kvs)) x
r' -> Field r' x
Project r xs ->
case loop r of
@ -2060,6 +2067,10 @@ isNormalized e0 = loop (denote e0)
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

98
src/Dhall/TypeCheck.hs
View File

@ -770,6 +770,9 @@ typeWithA tpa = loop
return (Record (Dhall.Map.mapWithKey adapt kts))
loop ctx e@(Field r x ) = do
t <- fmap Dhall.Core.normalize (loop ctx r)
let text = Dhall.Pretty.Internal.docToStrictText (Dhall.Pretty.Internal.prettyLabel x)
case t of
Record kts -> do
_ <- loop ctx t
@ -777,9 +780,15 @@ typeWithA tpa = loop
case Dhall.Map.lookup x kts of
Just t' -> return t'
Nothing -> Left (TypeError ctx e (MissingField x t))
Const Type -> do
case r of
(Note _ (Union kts)) ->
case Dhall.Map.lookup x kts of
Just t' -> return (Pi x t' (Union kts))
Nothing -> Left (TypeError ctx e (MissingField x t))
_ -> Left (TypeError ctx e (CantAccess text r t))
_ -> do
let text = Dhall.Pretty.Internal.docToStrictText (Dhall.Pretty.Internal.prettyLabel x)
Left (TypeError ctx e (NotARecord text r t))
Left (TypeError ctx e (CantAccess text r t))
loop ctx e@(Project r xs ) = do
t <- fmap Dhall.Core.normalize (loop ctx r)
case t of
@ -794,7 +803,7 @@ typeWithA tpa = loop
fmap adapt (traverse process (Data.Set.toList xs))
_ -> do
let text = Dhall.Pretty.Internal.docToStrictText (Dhall.Pretty.Internal.prettyLabels xs)
Left (TypeError ctx e (NotARecord text r t))
Left (TypeError ctx e (CantProject text r t))
loop ctx (Note s e' ) = case loop ctx e' of
Left (TypeError ctx' (Note s' e'') m) -> Left (TypeError ctx' (Note s' e'') m)
Left (TypeError ctx' e'' m) -> Left (TypeError ctx' (Note s e'') m)
@ -869,7 +878,8 @@ data TypeMessage s a
| MissingMergeType
| HandlerNotAFunction Text (Expr s a)
| ConstructorsRequiresAUnionType (Expr s a) (Expr s a)
| NotARecord Text (Expr s a) (Expr s a)
| CantAccess Text (Expr s a) (Expr s a)
| CantProject Text (Expr s a) (Expr s a)
| MissingField Text (Expr s a)
| CantAnd (Expr s a) (Expr s a)
| CantOr (Expr s a) (Expr s a)
@ -3242,18 +3252,18 @@ prettyTypeMessage (ConstructorsRequiresAUnionType expr0 expr1) = ErrorMessages {
where
txt0 = insert expr0
txt1 = insert expr1
prettyTypeMessage (NotARecord lazyText0 expr0 expr1) = ErrorMessages {..}
prettyTypeMessage (CantAccess lazyText0 expr0 expr1) = ErrorMessages {..}
where
short = "Not a record"
short = "Not a record or a union"
long =
"Explanation: You can only access fields on records, like this: \n\
"Explanation: You can only access fields on records or unions, like this: \n\
\ \n\
\ \n\
\ ┌─────────────────────────────────┐ \n\
\ ┌───────────────────────────────────┐ \n\
\ │ { foo = True, bar = \"ABC\" }.foo │ This is valid ... \n\
\ └─────────────────────────────────┘ \n\
\ └───────────────────────────────────┘ \n\
\ \n\
\ \n\
\ ┌───────────────────────────────────────────┐ \n\
@ -3261,6 +3271,16 @@ prettyTypeMessage (NotARecord lazyText0 expr0 expr1) = ErrorMessages {..}
\ └───────────────────────────────────────────┘ \n\
\ \n\
\ \n\
\ ┌─────────────────────────────────┐ \n\
\ │ < foo : Bool | bar : Text >.foo │ ... and so is this \n\
\ └─────────────────────────────────┘ \n\
\ \n\
\ \n\
\ ┌────────────────────────────────────────────┐ \n\
\ │ λ(r : < foo : Bool | bar : Text >) → r.foo │ ... and so is this \n\
\ └────────────────────────────────────────────┘ \n\
\ \n\
\ \n\
\... but you cannot access fields on non-record expressions \n\
\ \n\
\For example, the following expression is " <> _NOT <> " valid: \n\
@ -3273,22 +3293,70 @@ prettyTypeMessage (NotARecord lazyText0 expr0 expr1) = ErrorMessages {..}
\ Invalid: Not a record \n\
\ \n\
\ \n\
\────────────────────────────────────────────────────────────────────────────────\n\
\ \n\
\You tried to access the field: \n\
\ \n\
\" <> txt0 <> "\n\
\ \n\
\... on the following expression which is not a record nor a union: \n\
\ \n\
\" <> txt1 <> "\n\
\ \n\
\... but is actually an expression of type: \n\
\ \n\
\" <> txt2 <> "\n"
where
txt0 = insert lazyText0
txt1 = insert expr0
txt2 = insert expr1
prettyTypeMessage (CantProject lazyText0 expr0 expr1) = ErrorMessages {..}
where
short = "Not a record"
long =
"Explanation: You can only project fields on records, like this: \n\
\ \n\
\ \n\
\ ┌─────────────────────────────────────────────────────┐ \n\
\ │ { foo = True, bar = \"ABC\", baz = 1 }.{ foo, bar } │ This is valid ... \n\
\ └─────────────────────────────────────────────────────┘ \n\
\ \n\
\ \n\
\ ┌────────────────────────────────────────────────────────────────────┐ \n\
\ │ λ(r : { foo : Bool, bar : Text , baz : Natural }) → r.{ foo, bar } │ ... and so is this \n\
\ └────────────────────────────────────────────────────────────────────┘ \n\
\ \n\
\ \n\
\... but you cannot project fields on non-record expressions \n\
\ \n\
\For example, the following expression is " <> _NOT <> " valid: \n\
\ \n\
\ \n\
\ ┌────────────────┐ \n\
\ │ 1.{ foo, bar } │ \n\
\ └────────────────┘ \n\
\ ⇧ \n\
\ Invalid: Not a record \n\
\ \n\
\ \n\
\Some common reasons why you might get this error: \n\
\ \n\
\● You accidentally try to access a field of a union instead of a record, like \n\
\● You accidentally try to project fields of a union instead of a record, like \n\
\ this: \n\
\ \n\
\ \n\
\ ┌─────────────────┐ \n\
\ │ < foo : a >.foo │ \n\
\ └─────────────────┘ \n\
\ ┌────────────────────────────────────┐ \n\
\ │ < foo : a | bar : b >.{ foo, bar } │ \n\
\ └────────────────────────────────────┘ \n\
\ ⇧ \n\
\ This is a union, not a record \n\
\ \n\
\ \n\
\────────────────────────────────────────────────────────────────────────────────\n\
\ \n\
\You tried to access the field(s): \n\
\You tried to access the fields: \n\
\ \n\
\" <> txt0 <> "\n\
\ \n\

2
tests/Normalization.hs
View File

@ -41,6 +41,8 @@ tutorialExamples =
testGroup "Tutorial examples"
[ shouldNormalize "⩓" "./tutorial/combineTypes/0"
, shouldNormalize "projection" "./tutorial/projection/0"
, shouldNormalize "access record" "./tutorial/access/0"
, shouldNormalize "access union" "./tutorial/access/1"
]
preludeExamples :: TestTree

38
tests/TypeCheck.hs
View File

@ -21,19 +21,8 @@ import qualified Test.Tasty.HUnit
typecheckTests :: TestTree
typecheckTests =
Test.Tasty.testGroup "typecheck tests"
[ 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"
]
[ preludeExamples
, accessTypeChecks
, should
"allow type-valued fields in a record"
"fieldsAreTypes"
@ -57,6 +46,29 @@ typecheckTests =
"failure/preferMixedRecords"
]
preludeExamples :: TestTree
preludeExamples =
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"
]
accessTypeChecks :: TestTree
accessTypeChecks =
Test.Tasty.testGroup "typecheck access"
[ should "record" "./access/0"
, should "record" "./access/1"
]
should :: Text -> Text -> TestTree
should name basename =
Test.Tasty.HUnit.testCase (Data.Text.unpack name) $ do

1
tests/normalization/tutorial/access/0A.dhall Normal file
View File

@ -0,0 +1 @@
{ x = "foo" }.x

1
tests/normalization/tutorial/access/0B.dhall Normal file
View File

@ -0,0 +1 @@
"foo"

1
tests/normalization/tutorial/access/1A.dhall Normal file
View File

@ -0,0 +1 @@
< Foo : Text | Bar : Natural >.Foo

1
tests/normalization/tutorial/access/1B.dhall Normal file
View File

@ -0,0 +1 @@
λ(Foo : Text) → < Foo = Foo | Bar : Natural >

1
tests/typecheck/access/0A.dhall Normal file
View File

@ -0,0 +1 @@
{ x = Text }.x

1
tests/typecheck/access/0B.dhall Normal file
View File

@ -0,0 +1 @@
Type

1
tests/typecheck/access/1A.dhall Normal file
View File

@ -0,0 +1 @@
< Foo : Text | Bar : Natural >.Foo

1
tests/typecheck/access/1B.dhall Normal file
View File

@ -0,0 +1 @@
∀(Foo : Text) → < Bar : Natural | Foo : Text >