From a4c8057a28e043caed531e7d035efc2a41dc30a1 Mon Sep 17 00:00:00 2001 From: Brent Yorgey Date: Sat, 25 Mar 2023 06:58:34 -0500 Subject: [PATCH] Records (#1148) Add record types to the language: record values are written like `[x = 3, y = "hi"]` and have types like `[x : int, y : text]`. Empty and singleton records are allowed. You can project a field out of a record using standard dot notation, like `r.x`. If things named e.g. `x` and `y` are in scope, you can also write e.g. `[x, y]` as a shorthand for `[x=x, y=y]`. Closes #1093 . #153 would make this even nicer to use. One reason this is significant is that record projection is our first language construct whose type cannot be inferred, because if we see something like `r.x` all we know about the type of `r` is that it is a record type with at least one field `x`, but we don't know how many other fields it might have. Without some complex stuff like row polymorphism we can't deal with that, so we just punt and throw an error saying that we can't infer the type of a projection. To make this usable we have to do a better job checking types, a la #99 . For example `def f : [x:int] -> int = \r. r.x end` would not have type checked before, since when checking the lambda we immediately switched into inference mode, and then encountered the record projection and threw up our hands. Now we work harder to push the given function type down into the lambda so that we are still in checking mode when we get to `r.x` which makes it work. But it is probably easy to write examples of other things where this doesn't work. Eventually we will want to fully implement #99 ; in the meantime one can always add a type annotation (#1164) on the record to get around this problem. Note, I was planning to add a `open e1 in e2` syntax, which would take a record expression `e1` and "open" it locally in `e2`, so all the fields would be in scope within `e2`. For example, if we had `r = [x = 3, y = 7]` then instead of writing `r.x + r.y` you could write `open r in x + y`. This would be especially useful for imports, as in `open import foo.sw in ...`. However, it turns out to be problematic: the only way to figure out the free variables in `open e1 in e2` is if you know the *type* of `e1`, so you know which names it binds in `e2`. (In all other cases, bound names can be determined statically from the *syntax*.) However, in our current codebase there is one place where we get the free variables of an untyped term: we decide at parse time whether definitions are recursive (and fill in a boolean to that effect) by checking whether the name of the thing being defined occurs free in its body. One idea might be to either fill in this boolean later, after typechecking, or simply compute it on the fly when it is needed; currently this is slightly problematic because we need the info about whether a definition is recursive when doing capability checking, which is currently independent of typechecking. I was also planning to add `export` keyword which creates a record with all names currently in scope --- this could be useful for creating modules. However, I realized that very often you don't really want *all* in-scope names, so it's not that useful to have `export`. Instead I added record punning so if you have several variables `x`, `y`, `z` in scope that you want to package into a record, you can just write `[x, y, z]` instead of `[x=x, y=y, z=z]`. Though it could still be rather annoying if you wanted to make a module with tons of useful functions and had to list them all in a record at the end... Originally I started adding records because I thought it would be a helpful way to organize modules and imports. However, that would require having records that contain fields with polymorphic types. I am not yet sure how that would play out. It would essentially allow encoding arbitrary higher-rank types, so it sounds kind of scary. In any case, I'm still glad I implemented records and I learned a lot, even if they can't be used for my original motivation. I can't think of a way to make a scenario that requires the use of records. Eventually once we have proper #94 we could make a scenario where you have to communicate with another robot and send it a value of some required type. That would be a cool way to test the use of other language features like lambdas, too. --- data/entities.yaml | 30 +++++++++++ data/recipes.yaml | 21 ++++++++ feedback.yaml | 1 + src/Swarm/Game/CESK.hs | 16 +++++- src/Swarm/Game/Entity.hs | 6 +-- src/Swarm/Game/Scenario.hs | 7 ++- .../Game/Scenario/Objective/Validation.hs | 19 +++---- src/Swarm/Game/Scenario/RobotLookup.hs | 5 +- src/Swarm/Game/Step.hs | 25 ++++++++- src/Swarm/Game/Terrain.hs | 3 +- src/Swarm/Language/Capability.hs | 7 ++- src/Swarm/Language/LSP/Hover.hs | 8 ++- src/Swarm/Language/Parse.hs | 36 ++++++++++--- src/Swarm/Language/Pipeline/QQ.hs | 4 +- src/Swarm/Language/Pretty.hs | 17 +++++- src/Swarm/Language/Requirement.hs | 5 ++ src/Swarm/Language/Syntax.hs | 24 ++++++++- src/Swarm/Language/Typecheck.hs | 52 +++++++++++++++++-- src/Swarm/Language/Types.hs | 26 ++++++++++ src/Swarm/Language/Value.hs | 4 ++ src/Swarm/Util.hs | 22 ++++++++ src/Swarm/Util/Yaml.hs | 4 +- test/unit/TestEval.hs | 41 +++++++++++++++ 23 files changed, 342 insertions(+), 41 deletions(-) diff --git a/data/entities.yaml b/data/entities.yaml index e5484deb..e7b3e433 100644 --- a/data/entities.yaml +++ b/data/entities.yaml @@ -1193,3 +1193,33 @@ inner workings. properties: [portable] capabilities: [debug] + +- name: victrola + display: + attr: device + char: 'Q' + description: + - | + A device for reading and writing data on circular platters made of + a soft plastic material. The stylus must be made of a + hard and durable material, with a special tip that relies on + quantum effects to extract high-density information. + - | + Also allows manipulating composite values consisting of a + collection of named fields. For example, `[x = 2, y = "hi"]` + is a value of type `[x : int, y : text]`. Individual fields + can be projected using dot notation. For example, + `let r = [y="hi", x=2] in r.x` has the value 2. The order + of the fields does not matter. + properties: [portable] + capabilities: [record] + +- name: quantum dot + display: + attr: gold + char: '.' + description: + - | + A nanoscale semiconductor particle with a wide range of + applications. + properties: [portable] diff --git a/data/recipes.yaml b/data/recipes.yaml index 77e935d4..181c4bc9 100644 --- a/data/recipes.yaml +++ b/data/recipes.yaml @@ -808,3 +808,24 @@ - [256, string] out: - [1, net] + +######################################### +## MISC ## +######################################### + +- in: + - [1, water] + - [1, silicon] + required: + - [50, solar panel] + out: + - [1, quantum dot] + +- in: + - [1, small motor] + - [1, copper pipe] + - [1, mithril] + - [1, quantum dot] + - [1, iron plate] + out: + - [1, victrola] diff --git a/feedback.yaml b/feedback.yaml index 5c80a9b9..36d8eea3 100644 --- a/feedback.yaml +++ b/feedback.yaml @@ -1,2 +1,3 @@ loops: test: stack test --fast + unit: stack test swarm:swarm-unit --fast diff --git a/src/Swarm/Game/CESK.hs b/src/Swarm/Game/CESK.hs index 1b608547..e230532f 100644 --- a/src/Swarm/Game/CESK.hs +++ b/src/Swarm/Game/CESK.hs @@ -86,7 +86,7 @@ import Data.Aeson (FromJSON, ToJSON) import Data.IntMap.Strict (IntMap) import Data.IntMap.Strict qualified as IM import GHC.Generics (Generic) -import Prettyprinter (Doc, Pretty (..), hsep, (<+>)) +import Prettyprinter (Doc, Pretty (..), encloseSep, hsep, (<+>)) import Swarm.Game.Entity (Count, Entity) import Swarm.Game.Exception import Swarm.Game.World (WorldUpdate (..)) @@ -169,6 +169,12 @@ data Frame -- nearby robots. We have the function to run, and the list of -- robot IDs to run it on. FMeetAll Value [Int] + | -- | We are in the middle of evaluating a record: some fields have + -- already been evaluated; we are focusing on evaluating one + -- field; and some fields have yet to be evaluated. + FRcd Env [(Var, Value)] Var [(Var, Maybe Term)] + | -- | We are in the middle of evaluating a record field projection.(:*:) + FProj Var deriving (Eq, Show, Generic, FromJSON, ToJSON) -- | A continuation is just a stack of frames. @@ -368,6 +374,14 @@ prettyFrame (FImmediate c _worldUpds _robotUpds) inner = prettyPrefix ("I[" <> p prettyFrame (FUpdate addr) inner = prettyPrefix ("S@" <> pretty addr) inner prettyFrame FFinishAtomic inner = prettyPrefix "A·" inner prettyFrame (FMeetAll _ _) inner = prettyPrefix "M·" inner +prettyFrame (FRcd _ done foc rest) (_, inner) = (11, encloseSep "[" "]" ", " (pDone ++ [pFoc] ++ pRest)) + where + pDone = map (\(x, v) -> pretty x <+> "=" <+> ppr (valueToTerm v)) (reverse done) + pFoc = pretty foc <+> "=" <+> inner + pRest = map pprEq rest + pprEq (x, Nothing) = pretty x + pprEq (x, Just t) = pretty x <+> "=" <+> ppr t +prettyFrame (FProj x) (p, inner) = (11, pparens (p < 11) inner <> "." <> pretty x) -- | Pretty-print a special "prefix application" frame, i.e. a frame -- formatted like @X· inner@. Unlike typical applications, these diff --git a/src/Swarm/Game/Entity.hs b/src/Swarm/Game/Entity.hs index b1e141bb..b741ffed 100644 --- a/src/Swarm/Game/Entity.hs +++ b/src/Swarm/Game/Entity.hs @@ -107,7 +107,7 @@ import Swarm.Game.Failure.Render (prettyFailure) import Swarm.Game.Location import Swarm.Game.ResourceLoading (getDataFileNameSafe) import Swarm.Language.Capability -import Swarm.Util (binTuples, plural, reflow, (?)) +import Swarm.Util (binTuples, failT, plural, reflow, (?)) import Swarm.Util.Yaml import Text.Read (readMaybe) import Witch @@ -143,7 +143,7 @@ instance FromJSON EntityProperty where tryRead :: Text -> Parser EntityProperty tryRead t = case readMaybe . from . T.toTitle $ t of Just c -> return c - Nothing -> fail $ "Unknown entity property " ++ from t + Nothing -> failT ["Unknown entity property", t] -- | How long an entity takes to regrow. This represents the minimum -- and maximum amount of time taken by one growth stage (there are @@ -343,7 +343,7 @@ instance FromJSON Entity where instance FromJSONE EntityMap Entity where parseJSONE = withTextE "entity name" $ \name -> E $ \em -> case lookupEntityName name em of - Nothing -> fail $ "Unknown entity: " ++ from @Text name + Nothing -> failT ["Unknown entity:", name] Just e -> return e instance ToJSON Entity where diff --git a/src/Swarm/Game/Scenario.hs b/src/Swarm/Game/Scenario.hs index fa8c15ac..ce30f618 100644 --- a/src/Swarm/Game/Scenario.hs +++ b/src/Swarm/Game/Scenario.hs @@ -67,10 +67,11 @@ import Swarm.Game.Scenario.RobotLookup import Swarm.Game.Scenario.Style import Swarm.Game.Scenario.WorldDescription import Swarm.Language.Pipeline (ProcessedTerm) +import Swarm.Util (failT) import Swarm.Util.Yaml import System.Directory (doesFileExist) import System.FilePath ((<.>), ()) -import Witch (from, into) +import Witch (from) ------------------------------------------------------------ -- Scenario @@ -111,9 +112,7 @@ instance FromJSONE EntityMap Scenario where em' <- getE case filter (isNothing . (`lookupEntityName` em')) known of [] -> return () - unk -> - fail . into @String $ - "Unknown entities in 'known' list: " <> T.intercalate ", " unk + unk -> failT ["Unknown entities in 'known' list:", T.intercalate ", " unk] -- parse robots and build RobotMap rs <- v ..: "robots" diff --git a/src/Swarm/Game/Scenario/Objective/Validation.hs b/src/Swarm/Game/Scenario/Objective/Validation.hs index 2a2883be..2cc48332 100644 --- a/src/Swarm/Game/Scenario/Objective/Validation.hs +++ b/src/Swarm/Game/Scenario/Objective/Validation.hs @@ -14,8 +14,7 @@ import Data.Set qualified as Set import Data.Text qualified as T import Swarm.Game.Scenario.Objective import Swarm.Game.Scenario.Objective.Graph -import Swarm.Util (quote) -import Witch (into) +import Swarm.Util (failT, quote) -- | Performs monadic validation before returning -- the "pure" construction of a wrapper record. @@ -31,21 +30,19 @@ validateObjectives objectives = do for_ objectives $ \x -> case _objectivePrerequisite x of Just p -> unless (null remaining) $ - fail . into @String $ - T.unwords - [ "Reference to undefined objective(s)" - , T.intercalate ", " (map quote $ Set.toList remaining) <> "." - , "Defined are:" - , T.intercalate ", " (map quote $ Set.toList allIds) - ] + failT + [ "Reference to undefined objective(s)" + , T.intercalate ", " (map quote $ Set.toList remaining) <> "." + , "Defined are:" + , T.intercalate ", " (map quote $ Set.toList allIds) + ] where refs = Set.fromList $ toList $ logic p remaining = Set.difference refs allIds Nothing -> return () unless (isAcyclicGraph connectedComponents) $ - fail . into @String $ - T.unwords ["There are dependency cycles in the prerequisites."] + failT ["There are dependency cycles in the prerequisites."] return objectives where diff --git a/src/Swarm/Game/Scenario/RobotLookup.hs b/src/Swarm/Game/Scenario/RobotLookup.hs index 1e4ef18e..1ff371a1 100644 --- a/src/Swarm/Game/Scenario/RobotLookup.hs +++ b/src/Swarm/Game/Scenario/RobotLookup.hs @@ -11,6 +11,7 @@ import Data.Map qualified as M import Data.Text (Text) import Swarm.Game.Entity import Swarm.Game.Robot (TRobot, trobotName) +import Swarm.Util (failT, quote) import Swarm.Util.Yaml ------------------------------------------------------------ @@ -35,11 +36,11 @@ buildRobotMap rs = M.fromList $ zipWith (\x y -> (view trobotName y, (x, y))) [0 -- | Look up a thing by name, throwing a parse error if it is not -- found. -getThing :: String -> (Text -> m -> Maybe a) -> Text -> ParserE m a +getThing :: Text -> (Text -> m -> Maybe a) -> Text -> ParserE m a getThing thing lkup name = do m <- getE case lkup name m of - Nothing -> fail $ "Unknown " <> thing <> " name: " ++ show name + Nothing -> failT ["Unknown", thing, "name:", quote name] Just a -> return a -- | Look up an entity by name in an 'EntityMap', throwing a parse diff --git a/src/Swarm/Game/Step.hs b/src/Swarm/Game/Step.hs index 32a866ae..0ac544b5 100644 --- a/src/Swarm/Game/Step.hs +++ b/src/Swarm/Game/Step.hs @@ -30,7 +30,7 @@ import Control.Effect.Error import Control.Effect.Lens import Control.Effect.Lift import Control.Lens as Lens hiding (Const, distrib, from, parts, use, uses, view, (%=), (+=), (.=), (<+=), (<>=)) -import Control.Monad (foldM, forM, forM_, guard, msum, unless, when) +import Control.Monad (foldM, forM, forM_, guard, msum, unless, when, zipWithM) import Control.Monad.Except (runExceptT) import Data.Array (bounds, (!)) import Data.Bifunctor (second) @@ -687,6 +687,26 @@ stepCESK cesk = case cesk of evalConst c (reverse (v2 : args)) s k | otherwise -> return $ Out (VCApp c (v2 : args)) s k Out _ s (FApp _ : _) -> badMachineState s "FApp of non-function" + -- Start evaluating a record. If it's empty, we're done. Otherwise, focus + -- on the first field and record the rest in a FRcd frame. + In (TRcd m) e s k -> return $ case M.assocs m of + [] -> Out (VRcd M.empty) s k + ((x, t) : fs) -> In (fromMaybe (TVar x) t) e s (FRcd e [] x fs : k) + -- When we finish evaluating the last field, return a record value. + Out v s (FRcd _ done x [] : k) -> return $ Out (VRcd (M.fromList ((x, v) : done))) s k + -- Otherwise, save the value of the field just evaluated and move on + -- to focus on evaluating the next one. + Out v s (FRcd e done x ((y, t) : rest) : k) -> + return $ In (fromMaybe (TVar y) t) e s (FRcd e ((x, v) : done) y rest : k) + -- Evaluate a record projection: evaluate the record and remember we + -- need to do the projection later. + In (TProj t x) e s k -> return $ In t e s (FProj x : k) + -- Do a record projection + Out v s (FProj x : k) -> case v of + VRcd m -> case M.lookup x m of + Nothing -> badMachineState s $ T.unwords ["Record projection for variable", x, "that does not exist"] + Just xv -> return $ Out xv s k + _ -> badMachineState s "FProj frame with non-record value" -- To evaluate non-recursive let expressions, we start by focusing on the -- let-bound expression. In (TLet False x _ t1 t2) e s k -> return $ In t1 e s (FLet x t2 e : k) @@ -2297,6 +2317,9 @@ compareValues v1 = case v1 of VPair v21 v22 -> (<>) <$> compareValues v11 v21 <*> compareValues v12 v22 v2 -> incompatCmp v1 v2 + VRcd m1 -> \case + VRcd m2 -> mconcat <$> (zipWithM compareValues `on` M.elems) m1 m2 + v2 -> incompatCmp v1 v2 VClo {} -> incomparable v1 VCApp {} -> incomparable v1 VDef {} -> incomparable v1 diff --git a/src/Swarm/Game/Terrain.hs b/src/Swarm/Game/Terrain.hs index 818e7a7a..8f41bca4 100644 --- a/src/Swarm/Game/Terrain.hs +++ b/src/Swarm/Game/Terrain.hs @@ -15,6 +15,7 @@ import Data.Map (Map) import Data.Map qualified as M import Data.Text qualified as T import Swarm.Game.Display +import Swarm.Util (failT) import Text.Read (readMaybe) import Witch (into) @@ -32,7 +33,7 @@ instance FromJSON TerrainType where parseJSON = withText "text" $ \t -> case readMaybe (into @String (T.toTitle t) ++ "T") of Just ter -> return ter - Nothing -> fail $ "Unknown terrain type: " ++ into @String t + Nothing -> failT ["Unknown terrain type:", t] -- | A map containing a 'Display' record for each different 'TerrainType'. terrainMap :: Map TerrainType Display diff --git a/src/Swarm/Language/Capability.hs b/src/Swarm/Language/Capability.hs index 3141052e..b7848b1b 100644 --- a/src/Swarm/Language/Capability.hs +++ b/src/Swarm/Language/Capability.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE OverloadedStrings #-} + -- | -- SPDX-License-Identifier: BSD-3-Clause -- @@ -21,6 +23,7 @@ import Data.Text qualified as T import Data.Yaml import GHC.Generics (Generic) import Swarm.Language.Syntax +import Swarm.Util (failT) import Text.Read (readMaybe) import Witch (from) import Prelude hiding (lookup) @@ -126,6 +129,8 @@ data Capability CSum | -- | Capability for working with product types. CProd + | -- | Capability for working with record types. + CRecord | -- | Debug capability. CDebug | -- | God-like capabilities. For e.g. commands intended only for @@ -146,7 +151,7 @@ instance FromJSON Capability where tryRead :: Text -> Parser Capability tryRead t = case readMaybe . from . T.cons 'C' . T.toTitle $ t of Just c -> return c - Nothing -> fail $ "Unknown capability " ++ from t + Nothing -> failT ["Unknown capability", t] -- | Capabilities needed to evaluate or execute a constant. constCaps :: Const -> Maybe Capability diff --git a/src/Swarm/Language/LSP/Hover.hs b/src/Swarm/Language/LSP/Hover.hs index cddae101..a235e9ba 100644 --- a/src/Swarm/Language/LSP/Hover.hs +++ b/src/Swarm/Language/LSP/Hover.hs @@ -17,9 +17,11 @@ module Swarm.Language.LSP.Hover ( import Control.Applicative ((<|>)) import Control.Lens ((^.)) import Control.Monad (guard, void) +import Data.Foldable (asum) import Data.Graph import Data.List.NonEmpty (NonEmpty (..)) -import Data.Maybe (fromMaybe) +import Data.Map qualified as M +import Data.Maybe (catMaybes, fromMaybe) import Data.Text (Text) import Data.Text qualified as T import Data.Text.Utf16.Rope qualified as R @@ -112,6 +114,8 @@ narrowToPosition s0@(Syntax' _ t ty) pos = fromMaybe s0 $ case t of SBind mlv s1@(Syntax' _ _ lty) s2 -> (mlv >>= d . flip locVarToSyntax' (getInnerType lty)) <|> d s1 <|> d s2 SPair s1 s2 -> d s1 <|> d s2 SDelay _ s -> d s + SRcd m -> asum . map d . catMaybes . M.elems $ m + SProj s1 _ -> d s1 SAnnotate s _ -> d s -- atoms - return their position and end recursion TUnit -> Nothing @@ -179,6 +183,8 @@ explain trm = case trm ^. sTerm of TText {} -> literal "A text literal." TBool {} -> literal "A boolean literal." TVar v -> pure $ typeSignature v ty "" + SRcd {} -> literal "A record literal." + SProj {} -> literal "A record projection." -- type ascription SAnnotate lhs typeAnn -> Node diff --git a/src/Swarm/Language/Parse.hs b/src/Swarm/Language/Parse.hs index f9236884..f557cb37 100644 --- a/src/Swarm/Language/Parse.hs +++ b/src/Swarm/Language/Parse.hs @@ -1,5 +1,6 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE ViewPatterns #-} -- | -- SPDX-License-Identifier: BSD-3-Clause @@ -37,8 +38,9 @@ import Control.Monad.Combinators.Expr import Control.Monad.Reader import Data.Bifunctor import Data.Foldable (asum) -import Data.List (nub) +import Data.List (foldl', nub) import Data.List.NonEmpty qualified (head) +import Data.Map.Strict (Map) import Data.Map.Strict qualified as Map import Data.Maybe (fromMaybe, mapMaybe) import Data.Set qualified as S @@ -48,6 +50,7 @@ import Data.Text qualified as T import Data.Void import Swarm.Language.Syntax import Swarm.Language.Types +import Swarm.Util (failT, findDup, squote) import Text.Megaparsec hiding (runParser) import Text.Megaparsec.Char import Text.Megaparsec.Char.Lexer qualified as L @@ -134,12 +137,10 @@ locIdentifier :: Parser LocVar locIdentifier = uncurry LV <$> parseLocG ((lexeme . try) (p >>= check) "variable name") where p = (:) <$> (letterChar <|> char '_') <*> many (alphaNumChar <|> char '_' <|> char '\'') - check s + check (into @Text -> t) | toLower t `elem` reservedWords = - fail $ "reserved word '" ++ s ++ "' cannot be used as variable name" + failT ["reserved word", squote t, "cannot be used as variable name"] | otherwise = return t - where - t = into @Text s -- | Parse a text literal (including escape sequences) in double quotes. textLiteral :: Parser Text @@ -166,6 +167,9 @@ braces = between (symbol "{") (symbol "}") parens :: Parser a -> Parser a parens = between (symbol "(") (symbol ")") +brackets :: Parser a -> Parser a +brackets = between (symbol "[") (symbol "]") + -------------------------------------------------- -- Parser @@ -217,8 +221,18 @@ parseTypeAtom = <|> TyActor <$ reserved "actor" <|> TyCmd <$> (reserved "cmd" *> parseTypeAtom) <|> TyDelay <$> braces parseType + <|> TyRcd <$> brackets (parseRecord (symbol ":" *> parseType)) <|> parens parseType +-- XXX reserved words should be OK to use as record fields? +parseRecord :: Parser a -> Parser (Map Var a) +parseRecord p = (parseBinding `sepBy` symbol ",") >>= fromListUnique + where + parseBinding = (,) <$> identifier <*> p + fromListUnique kvs = case findDup (map fst kvs) of + Nothing -> return $ Map.fromList kvs + Just x -> failT ["duplicate field name", squote x, "in record literal"] + parseDirection :: Parser Direction parseDirection = asum (map alternative allDirs) "direction constant" where @@ -243,8 +257,17 @@ parseLocG pa = do parseLoc :: Parser Term -> Parser Syntax parseLoc pterm = uncurry Syntax <$> parseLocG pterm +-- | Parse an atomic term, optionally trailed by record projections like @t.x.y.z@. +-- Record projection binds more tightly than function application. parseTermAtom :: Parser Syntax -parseTermAtom = +parseTermAtom = do + s1 <- parseTermAtom2 + ps <- many (symbol "." *> parseLocG identifier) + return $ foldl' (\(Syntax l1 t) (l2, x) -> Syntax (l1 <> l2) (TProj t x)) s1 ps + +-- | Parse an atomic term. +parseTermAtom2 :: Parser Syntax +parseTermAtom2 = parseLoc ( TUnit <$ symbol "()" <|> TConst <$> parseConst @@ -275,6 +298,7 @@ parseTermAtom = <$> (reserved "def" *> locIdentifier) <*> optional (symbol ":" *> parsePolytype) <*> (symbol "=" *> parseTerm <* reserved "end") + <|> SRcd <$> brackets (parseRecord (optional (symbol "=" *> parseTerm))) <|> parens (view sTerm . mkTuple <$> (parseTerm `sepBy` symbol ",")) ) -- Potential syntax for explicitly requesting memoized delay. diff --git a/src/Swarm/Language/Pipeline/QQ.hs b/src/Swarm/Language/Pipeline/QQ.hs index 3c5cc451..6d35c803 100644 --- a/src/Swarm/Language/Pipeline/QQ.hs +++ b/src/Swarm/Language/Pipeline/QQ.hs @@ -12,7 +12,7 @@ import Swarm.Language.Pipeline import Swarm.Language.Pretty (prettyText) import Swarm.Language.Syntax import Swarm.Language.Types (Polytype) -import Swarm.Util (liftText) +import Swarm.Util (failT, liftText) import Witch (from) -- | A quasiquoter for Swarm language terms, so we can conveniently @@ -42,7 +42,7 @@ quoteTermExp s = do ) parsed <- runParserTH pos parseTerm s case processParsedTerm parsed of - Left errMsg -> fail $ from $ prettyText errMsg + Left errMsg -> failT [prettyText errMsg] Right ptm -> dataToExpQ ((fmap liftText . cast) `extQ` antiTermExp) ptm antiTermExp :: Term' Polytype -> Maybe TH.ExpQ diff --git a/src/Swarm/Language/Pretty.hs b/src/Swarm/Language/Pretty.hs index 994d6415..9ec1dc77 100644 --- a/src/Swarm/Language/Pretty.hs +++ b/src/Swarm/Language/Pretty.hs @@ -14,6 +14,7 @@ import Control.Unification import Control.Unification.IntVar import Data.Bool (bool) import Data.Functor.Fixedpoint (Fix, unFix) +import Data.Map.Strict qualified as M import Data.String (fromString) import Data.Text (Text) import Data.Text qualified as T @@ -83,6 +84,7 @@ instance PrettyPrec t => PrettyPrec (TypeF t) where prettyPrec p (TyFunF ty1 ty2) = pparens (p > 0) $ prettyPrec 1 ty1 <+> "->" <+> prettyPrec 0 ty2 + prettyPrec _ (TyRcdF m) = brackets $ hsep (punctuate "," (map prettyBinding (M.assocs m))) instance PrettyPrec Polytype where prettyPrec _ (Forall [] t) = ppr t @@ -95,8 +97,9 @@ instance PrettyPrec UPolytype where instance PrettyPrec t => PrettyPrec (Ctx t) where prettyPrec _ Empty = emptyDoc prettyPrec _ (assocs -> bs) = brackets (hsep (punctuate "," (map prettyBinding bs))) - where - prettyBinding (x, ty) = pretty x <> ":" <+> ppr ty + +prettyBinding :: (Pretty a, PrettyPrec b) => (a, b) -> Doc ann +prettyBinding (x, ty) = pretty x <> ":" <+> ppr ty instance PrettyPrec Direction where prettyPrec _ = pretty . directionSyntax @@ -166,10 +169,16 @@ instance PrettyPrec Term where prettyPrec p (TBind (Just x) t1 t2) = pparens (p > 0) $ pretty x <+> "<-" <+> prettyPrec 1 t1 <> ";" <+> prettyPrec 0 t2 + prettyPrec _ (TRcd m) = brackets $ hsep (punctuate "," (map prettyEquality (M.assocs m))) + prettyPrec _ (TProj t x) = prettyPrec 11 t <> "." <> pretty x prettyPrec p (TAnnotate t pt) = pparens (p > 0) $ prettyPrec 1 t <+> ":" <+> ppr pt +prettyEquality :: (Pretty a, PrettyPrec b) => (a, Maybe b) -> Doc ann +prettyEquality (x, Nothing) = pretty x +prettyEquality (x, Just t) = pretty x <+> "=" <+> ppr t + prettyTuple :: Term -> Doc a prettyTuple = pparens True . hsep . punctuate "," . map ppr . unnestTuple where @@ -200,6 +209,10 @@ instance PrettyPrec TypeErr where "Definitions may only be at the top level:" <+> ppr t prettyPrec _ (CantInfer _ t) = "Couldn't infer the type of term (this shouldn't happen; please report this as a bug!):" <+> ppr t + prettyPrec _ (CantInferProj _ t) = + "Can't infer the type of a record projection:" <+> ppr t + prettyPrec _ (UnknownProj _ x t) = + "Record does not have a field with name" <+> pretty x <> ":" <+> ppr t prettyPrec _ (InvalidAtomic _ reason t) = "Invalid atomic block:" <+> ppr reason <> ":" <+> ppr t diff --git a/src/Swarm/Language/Requirement.hs b/src/Swarm/Language/Requirement.hs index 537107e2..8983eba1 100644 --- a/src/Swarm/Language/Requirement.hs +++ b/src/Swarm/Language/Requirement.hs @@ -238,5 +238,10 @@ requirements' = go -- typechecked; Def commands are only allowed at the top level, -- so simply returning mempty is safe. TDef {} -> mempty + TRcd m -> insert (ReqCap CRecord) $ foldMap (go ctx . expandEq) (M.assocs m) + where + expandEq (x, Nothing) = TVar x + expandEq (_, Just t) = t + TProj t _ -> insert (ReqCap CRecord) $ go ctx t -- A type ascription doesn't change requirements TAnnotate t _ -> go ctx t diff --git a/src/Swarm/Language/Syntax.hs b/src/Swarm/Language/Syntax.hs index 830799fb..dd2dce48 100644 --- a/src/Swarm/Language/Syntax.hs +++ b/src/Swarm/Language/Syntax.hs @@ -56,6 +56,8 @@ module Swarm.Language.Syntax ( pattern TDef, pattern TBind, pattern TDelay, + pattern TRcd, + pattern TProj, pattern TAnnotate, -- * Terms @@ -88,6 +90,7 @@ import Data.Hashable (Hashable) import Data.List qualified as L (tail) import Data.List.NonEmpty (NonEmpty) import Data.List.NonEmpty qualified as NonEmpty +import Data.Map.Strict (Map) import Data.Set qualified as S import Data.String (IsString (fromString)) import Data.Text hiding (filter, map) @@ -796,6 +799,12 @@ data Term' ty -- be a special syntactic form so its argument can get special -- treatment during evaluation. SDelay DelayType (Syntax' ty) + | -- | Record literals @[x1 = e1, x2 = e2, x3, ...]@ Names @x@ + -- without an accompanying definition are sugar for writing + -- @x=x@. + SRcd (Map Var (Maybe (Syntax' ty))) + | -- | Record projection @e.x@ + SProj (Syntax' ty) Var | -- | Annotate a term with a type SAnnotate (Syntax' ty) Polytype deriving (Eq, Show, Functor, Foldable, Traversable, Data, Generic, FromJSON, ToJSON) @@ -908,12 +917,21 @@ pattern TBind mv t1 t2 <- SBind (fmap lvVar -> mv) (STerm t1) (STerm t2) pattern TDelay :: DelayType -> Term -> Term pattern TDelay m t = SDelay m (STerm t) +-- | Match a TRcd without syntax +pattern TRcd :: Map Var (Maybe Term) -> Term +pattern TRcd m <- SRcd ((fmap . fmap) _sTerm -> m) + where + TRcd m = SRcd ((fmap . fmap) STerm m) + +pattern TProj :: Term -> Var -> Term +pattern TProj t x = SProj (STerm t) x + -- | Match a TAnnotate without syntax pattern TAnnotate :: Term -> Polytype -> Term pattern TAnnotate t pt = SAnnotate (STerm t) pt -- | COMPLETE pragma tells GHC using this set of pattern is complete for Term -{-# COMPLETE TUnit, TConst, TDir, TInt, TAntiInt, TText, TAntiText, TBool, TRequireDevice, TRequire, TVar, TPair, TLam, TApp, TLet, TDef, TBind, TDelay, TAnnotate #-} +{-# COMPLETE TUnit, TConst, TDir, TInt, TAntiInt, TText, TAntiText, TBool, TRequireDevice, TRequire, TVar, TPair, TLam, TApp, TLet, TDef, TBind, TDelay, TRcd, TProj, TAnnotate #-} -- | Make infix operation (e.g. @2 + 3@) a curried function -- application (@((+) 2) 3@). @@ -974,6 +992,8 @@ erase (SApp s1 s2) = TApp (eraseS s1) (eraseS s2) erase (SLet r x mty s1 s2) = TLet r (lvVar x) mty (eraseS s1) (eraseS s2) erase (SDef r x mty s) = TDef r (lvVar x) mty (eraseS s) erase (SBind mx s1 s2) = TBind (lvVar <$> mx) (eraseS s1) (eraseS s2) +erase (SRcd m) = TRcd ((fmap . fmap) eraseS m) +erase (SProj s x) = TProj (eraseS s) x erase (SAnnotate s pty) = TAnnotate (eraseS s) pty ------------------------------------------------------------ @@ -1016,6 +1036,8 @@ freeVarsS f = go S.empty SDef r x xty s1 -> rewrap $ SDef r x xty <$> go (S.insert (lvVar x) bound) s1 SBind mx s1 s2 -> rewrap $ SBind mx <$> go bound s1 <*> go (maybe id (S.insert . lvVar) mx bound) s2 SDelay m s1 -> rewrap $ SDelay m <$> go bound s1 + SRcd m -> rewrap $ SRcd <$> (traverse . traverse) (go bound) m + SProj s1 x -> rewrap $ SProj <$> go bound s1 <*> pure x SAnnotate s1 pty -> rewrap $ SAnnotate <$> go bound s1 <*> pure pty where rewrap s' = Syntax' l <$> s' <*> pure ty diff --git a/src/Swarm/Language/Typecheck.hs b/src/Swarm/Language/Typecheck.hs index 269af713..2cecd092 100644 --- a/src/Swarm/Language/Typecheck.hs +++ b/src/Swarm/Language/Typecheck.hs @@ -45,6 +45,7 @@ module Swarm.Language.Typecheck ( import Control.Category ((>>>)) import Control.Lens ((^.)) +import Control.Lens.Indexed (itraverse) import Control.Monad.Except import Control.Monad.Reader import Control.Unification hiding (applyBindings, (=:=)) @@ -237,6 +238,11 @@ data TypeErr | -- | A term was encountered which we cannot infer the type of. -- This should never happen. CantInfer SrcLoc Term + | -- | We can't infer the type of a record projection @r.x@ if we + -- don't concretely know the type of the record @r@. + CantInferProj SrcLoc Term + | -- | An attempt to project out a nonexistent field + UnknownProj SrcLoc Var Term | -- | An invalid argument was provided to @atomic@. InvalidAtomic SrcLoc InvalidAtomicReason Term deriving (Show) @@ -267,6 +273,8 @@ getTypeErrSrcLoc te = case te of Mismatch l _ _ -> Just l DefNotTopLevel l _ -> Just l CantInfer l _ -> Just l + CantInferProj l _ -> Just l + UnknownProj l _ _ -> Just l InvalidAtomic l _ _ -> Just l ------------------------------------------------------------ @@ -452,6 +460,16 @@ infer s@(Syntax l t) = (`catchError` addLocToTypeErr s) $ case t of c2' <- maybe id ((`withBinding` Forall [] a) . lvVar) mx $ infer c2 _ <- decomposeCmdTy (c2' ^. sType) return $ Syntax' l (SBind mx c1' c2') (c2' ^. sType) + SRcd m -> do + m' <- itraverse (\x -> infer . fromMaybe (STerm (TVar x))) m + return $ Syntax' l (SRcd (Just <$> m')) (UTyRcd (fmap (^. sType) m')) + SProj t1 x -> do + t1' <- infer t1 + case t1' ^. sType of + UTyRcd m -> case M.lookup x m of + Just xTy -> return $ Syntax' l (SProj t1' x) xTy + Nothing -> throwError $ UnknownProj l x (SProj t1 x) + _ -> throwError $ CantInferProj l (SProj t1 x) SAnnotate c pty -> do let upty = toU pty -- Typecheck against skolemized polytype. @@ -502,6 +520,15 @@ decomposeFunTy ty = do _ <- ty =:= UTyFun ty1 ty2 return (ty1, ty2) +-- | Decompose a type that is supposed to be a product type. +decomposeProdTy :: UType -> Infer (UType, UType) +decomposeProdTy (UTyProd ty1 ty2) = return (ty1, ty2) +decomposeProdTy ty = do + ty1 <- fresh + ty2 <- fresh + _ <- ty =:= UTyProd ty1 ty2 + return (ty1, ty2) + -- | Infer the type of a constant. inferConst :: Const -> Polytype inferConst c = case c of @@ -595,10 +622,21 @@ inferConst c = case c of -- | @check t ty@ checks that @t@ has type @ty@, returning a -- type-annotated AST if so. check :: Syntax -> UType -> Infer (Syntax' UType) -check t ty = do - Syntax' l t' ty' <- infer t - theTy <- ty =:= ty' - return $ Syntax' l t' theTy +check s@(Syntax l t) ty = (`catchError` addLocToTypeErr s) $ case t of + SPair s1 s2 -> do + (ty1, ty2) <- decomposeProdTy ty + s1' <- check s1 ty1 + s2' <- check s2 ty2 + return $ Syntax' l (SPair s1' s2') (UTyProd ty1 ty2) + SLam x xTy body -> do + (argTy, resTy) <- decomposeFunTy ty + _ <- maybe (return argTy) (=:= argTy) (toU xTy) + body' <- withBinding (lvVar x) (Forall [] argTy) $ check body resTy + return $ Syntax' l (SLam x xTy body') (UTyFun argTy resTy) + _ -> do + Syntax' l' t' ty' <- infer s + theTy <- ty =:= ty' + return $ Syntax' l' t' theTy -- | Ensure a term is a valid argument to @atomic@. Valid arguments -- may not contain @def@, @let@, or lambda. Any variables which are @@ -669,6 +707,12 @@ analyzeAtomic locals (Syntax l t) = case t of -- Bind is similarly simple except that we have to keep track of a local variable -- bound in the RHS. SBind mx s1 s2 -> (+) <$> analyzeAtomic locals s1 <*> analyzeAtomic (maybe id (S.insert . lvVar) mx locals) s2 + SRcd m -> sum <$> mapM analyzeField (M.assocs m) + where + analyzeField :: (Var, Maybe Syntax) -> Infer Int + analyzeField (x, Nothing) = analyzeAtomic locals (STerm (TVar x)) + analyzeField (_, Just s) = analyzeAtomic locals s + SProj {} -> return 0 -- Variables are allowed if bound locally, or if they have a simple type. TVar x | x `S.member` locals -> return 0 diff --git a/src/Swarm/Language/Types.hs b/src/Swarm/Language/Types.hs index f2bbb5bd..04831e9f 100644 --- a/src/Swarm/Language/Types.hs +++ b/src/Swarm/Language/Types.hs @@ -29,6 +29,7 @@ module Swarm.Language.Types ( pattern (:+:), pattern (:*:), pattern (:->:), + pattern TyRcd, pattern TyCmd, pattern TyDelay, @@ -46,6 +47,7 @@ module Swarm.Language.Types ( pattern UTySum, pattern UTyProd, pattern UTyFun, + pattern UTyRcd, pattern UTyCmd, pattern UTyDelay, @@ -67,12 +69,17 @@ module Swarm.Language.Types ( WithU (..), ) where +import Control.Monad (guard) import Control.Unification import Control.Unification.IntVar import Data.Aeson (FromJSON, ToJSON) import Data.Data (Data) import Data.Foldable (fold) +import Data.Function (on) import Data.Functor.Fixedpoint +import Data.Map.Merge.Strict qualified as M +import Data.Map.Strict (Map) +import Data.Map.Strict qualified as M import Data.Maybe (fromJust) import Data.Set (Set) import Data.Set qualified as S @@ -129,8 +136,21 @@ data TypeF t TyProdF t t | -- | Function type. TyFunF t t + | -- | Record type. + TyRcdF (Map Var t) deriving (Show, Eq, Functor, Foldable, Traversable, Generic, Generic1, Unifiable, Data, FromJSON, ToJSON) +-- | Unify two Maps by insisting they must have exactly the same keys, +-- and if so, simply matching up corresponding values to be +-- recursively unified. There could be other reasonable +-- implementations, but in our case we will use this for unifying +-- record types, and we do not have any subtyping, so record types +-- will only unify if they have exactly the same keys. +instance Ord k => Unifiable (Map k) where + zipMatch m1 m2 = do + guard $ ((==) `on` M.keysSet) m1 m2 + pure $ M.merge M.dropMissing M.dropMissing (M.zipWithMatched (\_ a1 a2 -> Right (a1, a2))) m1 m2 + -- | @Type@ is now defined as the fixed point of 'TypeF'. It would be -- annoying to manually apply and match against 'Fix' constructors -- everywhere, so we provide pattern synonyms that allow us to work @@ -295,6 +315,9 @@ infixr 1 :->: pattern (:->:) :: Type -> Type -> Type pattern ty1 :->: ty2 = Fix (TyFunF ty1 ty2) +pattern TyRcd :: Map Var Type -> Type +pattern TyRcd m = Fix (TyRcdF m) + pattern TyCmd :: Type -> Type pattern TyCmd ty1 = Fix (TyCmdF ty1) @@ -337,6 +360,9 @@ pattern UTyProd ty1 ty2 = UTerm (TyProdF ty1 ty2) pattern UTyFun :: UType -> UType -> UType pattern UTyFun ty1 ty2 = UTerm (TyFunF ty1 ty2) +pattern UTyRcd :: Map Var UType -> UType +pattern UTyRcd m = UTerm (TyRcdF m) + pattern UTyCmd :: UType -> UType pattern UTyCmd ty1 = UTerm (TyCmdF ty1) diff --git a/src/Swarm/Language/Value.hs b/src/Swarm/Language/Value.hs index fe08d4b7..8235d7e6 100644 --- a/src/Swarm/Language/Value.hs +++ b/src/Swarm/Language/Value.hs @@ -19,6 +19,7 @@ module Swarm.Language.Value ( import Data.Aeson (FromJSON, ToJSON) import Data.Bool (bool) import Data.List (foldl') +import Data.Map (Map) import Data.Map qualified as M import Data.Set qualified as S import Data.Set.Lens (setOf) @@ -81,6 +82,8 @@ data Value where VDelay :: Term -> Env -> Value -- | A reference to a memory cell in the store. VRef :: Int -> Value + -- | A record value. + VRcd :: Map Var Value -> Value deriving (Eq, Show, Generic, FromJSON, ToJSON) -- | Ensure that a value is not wrapped in 'VResult'. @@ -113,6 +116,7 @@ valueToTerm (VResult v _) = valueToTerm v valueToTerm (VBind mx c1 c2 _) = TBind mx c1 c2 valueToTerm (VDelay t _) = TDelay SimpleDelay t valueToTerm (VRef n) = TRef n +valueToTerm (VRcd m) = TRcd (Just . valueToTerm <$> m) -- | An environment is a mapping from variable names to values. type Env = Ctx Value diff --git a/src/Swarm/Util.hs b/src/Swarm/Util.hs index 440e0b41..b283718d 100644 --- a/src/Swarm/Util.hs +++ b/src/Swarm/Util.hs @@ -16,6 +16,7 @@ module Swarm.Util ( listEnums, uniq, binTuples, + findDup, -- * Directory utilities readFileMay, @@ -24,6 +25,8 @@ module Swarm.Util ( -- * Text utilities isIdentChar, replaceLast, + failT, + showT, -- * English language utilities reflow, @@ -86,6 +89,7 @@ import NLP.Minimorph.English qualified as MM import NLP.Minimorph.Util ((<+>)) import System.Clock (TimeSpec) import System.IO.Error (catchIOError) +import Witch (from) infixr 1 ? infix 4 %%=, <+=, <%=, <<.=, <>= @@ -145,6 +149,15 @@ binTuples = foldr f mempty where f = uncurry (M.insertWith (<>)) . fmap pure +-- | Find a duplicate element within the list, if any exists. +findDup :: Ord a => [a] -> Maybe a +findDup = go S.empty + where + go _ [] = Nothing + go seen (a : as) + | a `S.member` seen = Just a + | otherwise = go (S.insert a seen) as + ------------------------------------------------------------ -- Directory stuff @@ -185,6 +198,15 @@ isIdentChar c = isAlphaNum c || c == '_' || c == '\'' replaceLast :: Text -> Text -> Text replaceLast r t = T.append (T.dropWhileEnd isIdentChar t) r +-- | Fail with a Text-based message, made out of phrases to be joined +-- by spaces. +failT :: MonadFail m => [Text] -> m a +failT = fail . from @Text . T.unlines + +-- | Show a value, but as Text. +showT :: Show a => a -> Text +showT = from @String . show + ------------------------------------------------------------ -- Some language-y stuff diff --git a/src/Swarm/Util/Yaml.hs b/src/Swarm/Util/Yaml.hs index 33ab3dfa..16de73c3 100644 --- a/src/Swarm/Util/Yaml.hs +++ b/src/Swarm/Util/Yaml.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE DerivingVia #-} +{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE UndecidableInstances #-} -- | @@ -31,6 +32,7 @@ import Data.Maybe (fromMaybe) import Data.Text (Text) import Data.Vector qualified as V import Data.Yaml as Y +import Swarm.Util (failT, showT) ------------------------------------------------------------ -- WithEntities wrapper @@ -96,7 +98,7 @@ instance (FromJSONE e a, FromJSONE e b) => FromJSONE e (a, b) where (,) <$> parseJSONE (V.unsafeIndex t 0) <*> parseJSONE (V.unsafeIndex t 1) - else fail $ "cannot unpack array of length " ++ show n ++ " into a tuple of length 2" + else failT ["cannot unpack array of length", showT n, "into a tuple of length 2"] ------------------------------------------------------------ -- Decoding diff --git a/test/unit/TestEval.hs b/test/unit/TestEval.hs index cc8fd416..8067a898 100644 --- a/test/unit/TestEval.hs +++ b/test/unit/TestEval.hs @@ -9,6 +9,7 @@ module TestEval where import Control.Lens ((^.), _3) import Data.Char (ord) +import Data.Map qualified as M import Data.Text (Text) import Data.Text qualified as T import Swarm.Game.State @@ -264,6 +265,46 @@ testEval g = `evaluatesToP` VInt i ) ] + , testGroup + "records - #1093" + [ testCase + "empty record" + ("[]" `evaluatesTo` VRcd M.empty) + , testCase + "singleton record" + ("[y = 3 + 4]" `evaluatesTo` VRcd (M.singleton "y" (VInt 7))) + , testCase + "record equality up to reordering" + ("[x = 2, y = 3] == [y = 3, x = 2]" `evaluatesTo` VBool True) + , testCase + "record projection" + ("[x = 2, y = 3].x" `evaluatesTo` VInt 2) + , testCase + "nested record projection" + ("let r = [x=2, y=3] in let z = [q = r, n=\"hi\"] in z.q.y" `evaluatesTo` VInt 3) + , testCase + "record punning" + ( "let x = 2 in let y = 3 in [x,y,z=\"hi\"]" + `evaluatesTo` VRcd (M.fromList [("x", VInt 2), ("y", VInt 3), ("z", VText "hi")]) + ) + , testCase + "record comparison" + ("[y=1, x=2] < [x=3,y=0]" `evaluatesTo` VBool True) + , testCase + "record comparison" + ("[y=1, x=3] < [x=3,y=0]" `evaluatesTo` VBool False) + , testCase + "record function" + ("let f : [x:int, y:text] -> int = \\r.r.x + 1 in f [x=3,y=\"hi\"]" `evaluatesTo` VInt 4) + , testCase + "format record" + ("format [y = 2, x = 1+2]" `evaluatesTo` VText "[x = 3, y = 2]") + , testCase + "record fields don't scope over other fields" + ( "let x = 1 in [x = x + 1, y = x]" + `evaluatesTo` VRcd (M.fromList [("x", VInt 2), ("y", VInt 1)]) + ) + ] ] where tquote :: String -> Text