Implement missing rules for field selection normalization (#1179)

…as standardized in https://github.com/dhall-lang/dhall-lang/pull/682.
This commit is contained in:
Simon Jakobi 2019-08-08 16:36:01 +02:00 committed by mergify[bot]
parent 6609270fe4
commit c2cc641408
3 changed files with 22 additions and 10 deletions

@ -1 +1 @@
Subproject commit b08bfa062e2373d1cafaadfb75661e30f4caa91e
Subproject commit c465bb9b50b66bbd413837814f000df95752ff80

View File

@ -1752,6 +1752,8 @@ normalizeWithM ctx e0 = loop (denote e0)
_ -> do
return (ToMap x' t')
Field r x -> do
let singletonRecordLit v = RecordLit (Dhall.Map.singleton x v)
r' <- loop r
case r' of
RecordLit kvs ->
@ -1759,14 +1761,18 @@ normalizeWithM ctx e0 = loop (denote e0)
Just v -> pure v
Nothing -> Field <$> (RecordLit <$> traverse loop kvs) <*> pure x
Project r_ _ -> loop (Field r_ x)
Prefer (RecordLit kvs) r_ -> case Dhall.Map.lookup x kvs of
Just v -> pure (Field (Prefer (singletonRecordLit v) r_) x)
Nothing -> loop (Field r_ x)
Prefer l (RecordLit kvs) -> case Dhall.Map.lookup x kvs of
Just v -> pure v
Nothing -> loop (Field l x)
Prefer (RecordLit kvs) r_ | not (Dhall.Map.member x kvs) -> loop (Field r_ x)
Combine (RecordLit kvs) r_ -> case Dhall.Map.lookup x kvs of
Just v -> pure (Field (Combine (singletonRecordLit v) r_) x)
Nothing -> loop (Field r_ x)
Combine l (RecordLit kvs) -> case Dhall.Map.lookup x kvs of
Just v -> pure (Field (Combine l (RecordLit (Dhall.Map.singleton x v))) x)
Just v -> pure (Field (Combine l (singletonRecordLit v)) x)
Nothing -> loop (Field l x)
Combine (RecordLit kvs) r_ | not (Dhall.Map.member x kvs) -> loop (Field r_ x)
_ -> pure (Field r' x)
Project r (Left xs)-> do
r' <- loop r
@ -2017,10 +2023,10 @@ isNormalized e0 = loop (denote e0)
Field r k -> case r of
RecordLit _ -> False
Project _ _ -> False
Combine (RecordLit m) _ -> Dhall.Map.member k m && loop r
Combine _ (RecordLit m) -> Dhall.Map.keys m == [k] && loop r
Prefer (RecordLit m) _ -> Dhall.Map.member k m && loop r
Prefer (RecordLit m) _ -> Dhall.Map.keys m == [k] && loop r
Prefer _ (RecordLit _) -> False
Combine (RecordLit m) _ -> Dhall.Map.keys m == [k] && loop r
Combine _ (RecordLit m) -> Dhall.Map.keys m == [k] && loop r
_ -> loop r
Project r p -> loop r &&
case p of

View File

@ -311,15 +311,21 @@ vField t0 k = go t0 where
| Just v <- Dhall.Map.lookup k m -> v
| otherwise -> error errorMsg
VProject t _ -> go t
VPrefer (VRecordLit m) r -> case Dhall.Map.lookup k m of
Just v -> VField (VPrefer (singletonVRecordLit v) r) k
Nothing -> go r
VPrefer l (VRecordLit m) -> case Dhall.Map.lookup k m of
Just v -> v
Nothing -> go l
VPrefer (VRecordLit m) r | not (Dhall.Map.member k m) -> go r
VCombine (VRecordLit m) r -> case Dhall.Map.lookup k m of
Just v -> VField (VCombine (singletonVRecordLit v) r) k
Nothing -> go r
VCombine l (VRecordLit m) -> case Dhall.Map.lookup k m of
Just v -> VField (VCombine l (VRecordLit (Dhall.Map.singleton k v))) k
Just v -> VField (VCombine l (singletonVRecordLit v)) k
Nothing -> go l
VCombine (VRecordLit m) r | not (Dhall.Map.member k m) -> go r
t -> VField t k
singletonVRecordLit v = VRecordLit (Dhall.Map.singleton k v)
{-# inline vField #-}
eval :: forall a. Eq a => Env a -> Expr Void a -> Val a