diff --git a/dhall/dhall-lang b/dhall/dhall-lang index 25cf020ab..b0bfdef01 160000 --- a/dhall/dhall-lang +++ b/dhall/dhall-lang @@ -1 +1 @@ -Subproject commit 25cf020ab307cb2d66826b0d1ddac8bc89241e27 +Subproject commit b0bfdef01a2bccaec3817dce40689175421fc199 diff --git a/dhall/dhall.cabal b/dhall/dhall.cabal index a3be524b8..593915ac3 100644 --- a/dhall/dhall.cabal +++ b/dhall/dhall.cabal @@ -381,6 +381,7 @@ Library Dhall.Syntax.Instances.Functor Dhall.Syntax.Instances.Lift Dhall.Syntax.Instances.Monad + Dhall.Syntax.Instances.Monoid Dhall.Syntax.Instances.NFData Dhall.Syntax.Instances.Ord Dhall.Syntax.Instances.Pretty diff --git a/dhall/src/Dhall/Eval.hs b/dhall/src/Dhall/Eval.hs index aac4b0c28..4461b6866 100644 --- a/dhall/src/Dhall/Eval.hs +++ b/dhall/src/Dhall/Eval.hs @@ -367,6 +367,9 @@ vField t0 k = go t0 Just (Just _) -> VPrim $ \ ~u -> VInject m k (Just u) Just Nothing -> VInject m k Nothing _ -> error errorMsg + VRecord m + | Just v <- Map.lookup k m -> v + | otherwise -> error errorMsg VRecordLit m | Just v <- Map.lookup k m -> v | otherwise -> error errorMsg @@ -414,6 +417,9 @@ vProjectByFields env t ks = VRecordLit kvs -> let kvs' = Map.restrictKeys kvs (Dhall.Set.toSet ks) in VRecordLit kvs' + VRecord kTs -> + let kTs' = Map.restrictKeys kTs (Dhall.Set.toSet ks) + in VRecord kTs' VProject t' _ -> vProjectByFields env t' ks VPrefer l (VRecordLit kvs) -> diff --git a/dhall/src/Dhall/Normalize.hs b/dhall/src/Dhall/Normalize.hs index e6a51a777..6d5e9614b 100644 --- a/dhall/src/Dhall/Normalize.hs +++ b/dhall/src/Dhall/Normalize.hs @@ -664,6 +664,11 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0) case Dhall.Map.lookup x kvs of Just v -> pure $ recordFieldValue v Nothing -> Field <$> (RecordLit <$> traverse (Syntax.recordFieldExprs loop) kvs) <*> pure k + Record kTs -> + case Dhall.Map.lookup x kTs of + Just _T -> pure $ recordFieldValue _T + Nothing -> Field <$> (Record <$> traverse (Syntax.recordFieldExprs loop) kTs) <*> pure k + Project r_ _ -> loop (Field r_ k) Prefer cs _ (RecordLit kvs) r_ -> case Dhall.Map.lookup x kvs of Just v -> pure (Field (Prefer cs PreferFromSource (singletonRecordLit v) r_) k) @@ -684,6 +689,8 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0) case x' of RecordLit kvs -> pure (RecordLit (Dhall.Map.restrictKeys kvs fieldsSet)) + Record kTs -> + pure (Record (Dhall.Map.restrictKeys kTs fieldsSet)) Project y _ -> loop (Project y (Left fields)) Prefer cs _ l (RecordLit rKvs) -> do @@ -980,6 +987,7 @@ isNormalized e0 = loop (Syntax.denote e0) _ -> True Field r (FieldSelection Nothing k Nothing) -> case r of RecordLit _ -> False + Record _ -> False Project _ _ -> False Prefer _ _ (RecordLit m) _ -> Dhall.Map.keys m == [k] && loop r Prefer _ _ _ (RecordLit _) -> False @@ -991,6 +999,7 @@ isNormalized e0 = loop (Syntax.denote e0) case p of Left s -> case r of RecordLit _ -> False + Record _ -> False Project _ _ -> False Prefer _ _ _ (RecordLit _) -> False _ -> not (null s) && Data.Set.toList (Data.Set.fromList s) == s diff --git a/dhall/src/Dhall/Syntax.hs b/dhall/src/Dhall/Syntax.hs index dcdc06b61..2e346bf24 100644 --- a/dhall/src/Dhall/Syntax.hs +++ b/dhall/src/Dhall/Syntax.hs @@ -19,6 +19,7 @@ import Dhall.Syntax.Instances.Foldable as Export () import Dhall.Syntax.Instances.Functor as Export () import Dhall.Syntax.Instances.Lift as Export () import Dhall.Syntax.Instances.Monad as Export () +import Dhall.Syntax.Instances.Monoid as Export () import Dhall.Syntax.Instances.NFData as Export () import Dhall.Syntax.Instances.Ord as Export () import Dhall.Syntax.Instances.Pretty as Export diff --git a/dhall/src/Dhall/Syntax/Instances/Monoid.hs b/dhall/src/Dhall/Syntax/Instances/Monoid.hs new file mode 100644 index 000000000..d462e4268 --- /dev/null +++ b/dhall/src/Dhall/Syntax/Instances/Monoid.hs @@ -0,0 +1,12 @@ +{-# OPTIONS_GHC -Wno-orphans #-} + +module Dhall.Syntax.Instances.Monoid () where + +import Dhall.Syntax.Const (Const(..)) +import Dhall.Syntax.Instances.Ord () + +instance Semigroup Const where + (<>) = max + +instance Monoid Const where + mempty = Type diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index 1e2c5184a..624e8b16b 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -1158,22 +1158,26 @@ infer typer = loop case Dhall.Map.lookup x xTs' of Just _T' -> return _T' Nothing -> die (MissingField x _E'') - _ -> do - let e' = eval values e - - let e'' = quote names e' - - case e' of - VUnion xTs' -> - case Dhall.Map.lookup x xTs' of - Just (Just _T') -> return (VHPi x _T' (\_ -> e')) - Just Nothing -> return e' - Nothing -> die (MissingConstructor x e) - - _ -> do - let text = Dhall.Pretty.Internal.docToStrictText (Dhall.Pretty.Internal.prettyLabel x) - - die (CantAccess text e'' _E'') + _ | VRecord xTs' <- eval values e -> + case Dhall.Map.lookup x xTs' of + Just _T' -> loop ctx (quote names _T') + Nothing -> die (MissingField x _E'') + | otherwise -> do + let e' = eval values e + + let e'' = quote names e' + + case e' of + VUnion xTs' -> + case Dhall.Map.lookup x xTs' of + Just (Just _T') -> return (VHPi x _T' (\_ -> e')) + Just Nothing -> return e' + Nothing -> die (MissingConstructor x e) + + _ -> do + let text = Dhall.Pretty.Internal.docToStrictText (Dhall.Pretty.Internal.prettyLabel x) + + die (CantAccess text e'' _E'') Project e (Left xs) -> do case duplicateElement xs of Just x -> do @@ -1185,6 +1189,9 @@ infer typer = loop let _E'' = quote names _E' + let text = + Dhall.Pretty.Internal.docToStrictText (Dhall.Pretty.Internal.prettyLabels xs) + case _E' of VRecord xTs' -> do let process x = @@ -1196,11 +1203,25 @@ infer typer = loop fmap adapt (traverse process xs) - _ -> do - let text = - Dhall.Pretty.Internal.docToStrictText (Dhall.Pretty.Internal.prettyLabels xs) + _ | VRecord xTs' <- eval values e -> do + let process x = + case Dhall.Map.lookup x xTs' of + Just _T' -> do + _T'' <- loop ctx (quote names _T') + + case _T'' of + VConst c -> pure c + _ -> die (CantProject text e _E'') + + Nothing -> do + die (MissingField x _E'') + + cs <- traverse process xs + + return (VConst (mconcat cs)) - die (CantProject text e _E'') + | otherwise -> do + die (CantProject text e _E'') Project e (Right s) -> do _E' <- loop ctx e