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.
This commit is contained in:
Brent Yorgey 2023-03-25 06:58:34 -05:00 committed by GitHub
parent d52c36d05c
commit a4c8057a28
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
23 changed files with 342 additions and 41 deletions

View File

@ -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]

View File

@ -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]

View File

@ -1,2 +1,3 @@
loops:
test: stack test --fast
unit: stack test swarm:swarm-unit --fast

View File

@ -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 "" inner
prettyFrame (FMeetAll _ _) inner = prettyPrefix "" 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

View File

@ -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

View File

@ -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"

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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.

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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)

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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