Add support for accessing/projecting record type fields

dhall-lang · Dec 3, 2023 · 00b18b8 · 00b18b8
1 parent 44b9f30
commit 00b18b8
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 0 deletions.
diff --git 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/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs
@@ -1158,6 +1158,11 @@ infer typer = loop
                     case Dhall.Map.lookup x xTs' of
                         Just _T' -> return _T'
                         Nothing  -> die (MissingField x _E'')
+                VConst _
+                    | VRecord xTs' <- eval values e ->
+                        case Dhall.Map.lookup x xTs' of
+                            Just _T' -> return _T'
+                            Nothing  -> die (MissingField x _E'')
                 _ -> do
                     let e' = eval values e
 
@@ -1195,6 +1200,16 @@ infer typer = loop
                     let adapt = VRecord . Dhall.Map.unorderedFromList
 
                     fmap adapt (traverse process xs)
+                VConst c
+                    | VRecord xTs' <- eval values e -> do
+                        let process x =
+                                if Dhall.Map.member x xTs'
+                                    then return ()
+                                    else die (MissingField x _E'')
+
+                        Foldable.traverse_ process xs
+
+                        pure (VConst c)
 
                 _ -> do
                     let text =