Skip to content

Add with support for Optional values #2386

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.

Sign up for GitHub

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
Gabriella439 merged 7 commits into from
Feb 19, 2022
Merged

Add with support for Optional values #2386

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
055731c
First pass on `Optional` support for `with`
darichey Dec 23, 2021
1b7490c
Merge branch 'master' into optional-with
Gabriella439 Feb 16, 2022
5f4fd2b
Add error messages
Gabriella439 Feb 17, 2022
141c303
Create strongly-typed `WithComponent` type
Gabriella439 Feb 17, 2022
dbbcd9c
Remove `dhall-to-nix` dependence on `desugarWith`
Gabriella439 Feb 19, 2022
bbbdad7
Fix missing haddocks
Gabriella439 Feb 19, 2022
9017122
Fix typo
Gabriella439 Feb 19, 2022
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
3 changes: 3 additions & 0 deletions dhall/src/Dhall/Eval.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -427,6 +427,9 @@ vWith (VRecordLit kvs) (k₀ :| k₁ : ks) v = VRecordLit (Map.insert k₀ e₂
Just e₁' -> e₁'

e₂ = vWith e₁ (k₁ :| ks) v
vWith (VNone _T) ("?" :| _ ) _ = VNone _T
vWith (VSome _) ("?" :| [] ) v = VSome v
vWith (VSome t) ("?" :| k₁ : ks) v = VSome (vWith t (k₁ :| ks) v)
vWith e₀ ks v₀ = VWith e₀ ks v₀

eval :: forall a. Eq a => Environment a -> Expr Void a -> Val a
Expand Down
2 changes: 1 addition & 1 deletion dhall/src/Dhall/Parser/Expression.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -388,7 +388,7 @@ parsers embedded = Parsers{..}
bs <- some (do
try (nonemptyWhitespace *> _with *> nonemptyWhitespace)

keys <- Combinators.NonEmpty.sepBy1 anyLabelOrSome (try (whitespace *> _dot) *> whitespace)
keys <- Combinators.NonEmpty.sepBy1 (anyLabelOrSome <|> text "?") (try (whitespace *> _dot) *> whitespace)

whitespace

Expand Down
116 changes: 102 additions & 14 deletions dhall/src/Dhall/TypeCheck.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1283,25 +1283,43 @@ infer typer = loop

-- The purpose of this inner loop is to ensure that we only need to
-- typecheck the record once
let with tE' ks v = do
kTs' <- case tE' of
VRecord kTs' -> return kTs'
_ -> die (NotWithARecord e₀ (quote names tE'))

let with tE' ks v = case tE' of

VRecord kTs' ->

case ks of
k :| [] -> do
tV' <- loop ctx v
k :| [] -> do
tV' <- loop ctx v

return (VRecord (Dhall.Map.insert k tV' kTs'))
k₀ :| k₁ : ks' -> do
let _T =
case Dhall.Map.lookup k₀ kTs' of
Just _T' -> _T'
Nothing -> VRecord mempty
return (VRecord (Dhall.Map.insert k tV' kTs'))
k₀ :| k₁ : ks' -> do
let _T =
case Dhall.Map.lookup k₀ kTs' of
Just _T' -> _T'
Nothing -> VRecord mempty

tV' <- with _T (k₁ :| ks') v
tV' <- with _T (k₁ :| ks') v

return (VRecord (Dhall.Map.insert k₀ tV' kTs'))
return (VRecord (Dhall.Map.insert k₀ tV' kTs'))

VOptional _O' -> do

case ks of

"?" :| [] -> do
tV' <- loop ctx v
if Eval.conv values _O' tV'
then return (VOptional _O')
else die OptionalWithTypeMismatch

"?" :| k₁ : ks' -> do
tV' <- with _O' (k₁ :| ks') v
return (VOptional tV')

_ -> die NotAQuestionPath

_ -> die (NotWithARecord e₀ (quote names tE')) -- TODO: NotWithARecordOrOptional

with tE₀' ks₀ v₀

Expand Down Expand Up @@ -1404,6 +1422,8 @@ data TypeMessage s a
| CantListAppend (Expr s a) (Expr s a)
| CantAdd (Expr s a) (Expr s a)
| CantMultiply (Expr s a) (Expr s a)
| OptionalWithTypeMismatch
| NotAQuestionPath
| ShowConstructorNotOnUnion
deriving (Show)

Expand Down Expand Up @@ -4559,6 +4579,70 @@ prettyTypeMessage (CantAdd expr0 expr1) =
prettyTypeMessage (CantMultiply expr0 expr1) =
buildNaturalOperator "*" expr0 expr1

prettyTypeMessage OptionalWithTypeMismatch = ErrorMessages {..}
where
short = "❰with❱ cannot change the type of an ❰Optional❱ value"
hints = []
long =
"Explanation: The ❰with❱ keyword cannot change the type of a value stored inside \n\
\of a ❰Some❱ constructor \n\
\ \n\
\For example, this is a valid use of ❰with❱: \n\
\ \n\
\ \n\
\ The old value has type ❰Natural❱ \n\
\ ⇩ \n\
\ ┌───────────────────┐ \n\
\ │ Some 1 with ? = 2 │ \n\
\ └───────────────────┘ \n\
\ ⇧ \n\
\ ... which matches the type of the new value, which is also\n\
\ ❰Natural❱ \n\
\ \n\
\ \n\
\... but the following example is not valid: \n\
\ \n\
\ \n\
\ The old value has type ❰Natural❱ \n\
\ ⇩ \n\
\ ┌──────────────────────┐ \n\
\ │ Some 1 with ? = True │ \n\
\ └──────────────────────┘ \n\
\ ⇧ \n\
\ ... but the new value has type ❰Bool❱, which does not \n\
\ match \n"

prettyTypeMessage NotAQuestionPath = ErrorMessages {..}
where
short = "Use ❰?❱ to update an ❰Optional❱ value"
hints = []
long =
"Explanation: The ❰with❱ keyword supports updating ❰Optional❱ values using a path\n\
\component of ❰?❱, but you provided a path component other than ❰?❱. \n\
\ \n\
\For example, these are valid uses of ❰with❱ to update an ❰Optional❱ value: \n\
\ \n\
\ \n\
\ ┌───────────────────┐ \n\
\ │ Some 1 with ? = 2 │ \n\
\ └───────────────────┘ \n\
\ \n\
\ \n\
\ ┌─────────────────────────────┐ \n\
\ │ { x = Some 1 } with x.? = 2 │ \n\
\ └─────────────────────────────┘ \n\
\ \n\
\ \n\
\... but the following example is not valid: \n\
\ \n\
\ \n\
\ ┌──────────────────────┐ \n\
\ │ Some 1 with x = True │ \n\
\ └──────────────────────┘ \n\
\ ⇧ \n\
\ This path component should have been ❰?❱ \n"


prettyTypeMessage ShowConstructorNotOnUnion = ErrorMessages {..}
where
short = "ShowConstructorNotOnUnion"
Expand Down Expand Up @@ -4846,6 +4930,10 @@ messageExpressions f m = case m of
CantAdd <$> f a <*> f b
CantMultiply a b ->
CantMultiply <$> f a <*> f b
OptionalWithTypeMismatch ->
pure OptionalWithTypeMismatch
NotAQuestionPath ->
pure NotAQuestionPath
ShowConstructorNotOnUnion ->
pure ShowConstructorNotOnUnion

Expand Down