Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

New read command to act as partial inverse to format #2224

Merged
merged 22 commits into from
Dec 26, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
6caadbd
[wip] basic runtime type-passing and start on `read` primitive
byorgey Dec 17, 2024
327fa03
[wip] start on Value parser for `read`
byorgey Dec 17, 2024
e683b15
more work on Value parser
byorgey Dec 18, 2024
3b440a9
Parsing for record Values
byorgey Dec 18, 2024
def8d23
Parsing for Key values
byorgey Dec 18, 2024
1a43a75
Value parser for recursive types
byorgey Dec 19, 2024
f1d9478
`expandTydefs`
byorgey Dec 19, 2024
26356b8
link TODO to issue number
byorgey Dec 19, 2024
c360930
add `parsley` entity that enables `read` command
byorgey Dec 19, 2024
4643cbb
Restyled by fourmolu (#2225)
github-actions[bot] Dec 19, 2024
d9d764a
remove unused LANGUAGE pragma
byorgey Dec 19, 2024
f1938a9
update editor configs with new `read` command
byorgey Dec 19, 2024
94e0b7c
normalize YAML
byorgey Dec 19, 2024
391ae69
give `read` type `Text -> a` rather than `Text -> Unit + a`
byorgey Dec 19, 2024
e0c87a6
Restyled by fourmolu (#2226)
github-actions[bot] Dec 19, 2024
08a22cb
apply hlint suggestions
byorgey Dec 19, 2024
92dd2f1
allow `Swarm.Language.Types.expandTydefs` to be unused for now
byorgey Dec 19, 2024
eddf4f0
fix parsley description
byorgey Dec 26, 2024
8678e03
note that `read` cannot deal with function, delay, or command types
byorgey Dec 26, 2024
b26a844
use swarm-lang parser followed by value check to implement `read`
byorgey Dec 26, 2024
bbd81e8
fix warnings, style, + add TODO re: `read` for other types
byorgey Dec 26, 2024
f3922cc
Merge branch 'main' into feature/read
mergify[bot] Dec 26, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 16 additions & 0 deletions data/entities.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -330,6 +330,22 @@
ignition: 0.1
duration: [20, 40]
product: ash
- name: parsley
display:
attr: plant
char: 'p'
description:
- A fast-growing plant with a pungent aroma, often found growing near rocks.
- |
When equipped as a device, parsley enables the `read` command, which can be used to turn text into values:
```
read : Text -> a
```
If the given `Text`{=type} represents a value of the expected type, the value will be returned; otherwise, an exception is thrown. For example, `(read "3" : Int) == 3`, but `read "hello" : Int` crashes.
- Note that `read`, unlike `format`, is unable to deal with function, delay, or command types.
properties: [pickable, growable]
capabilities: [read]
growth: [10, 100]
- name: linotype
display:
attr: silver
Expand Down
1 change: 1 addition & 0 deletions data/worlds/classic.world
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,7 @@ overlay
[ {stone}
, mask (hash % 10 == 0) {stone, rock}
, mask (hash % 100 == 0) {stone, lodestone}
, mask (hash % 300 == 0) {grass, parsley}
byorgey marked this conversation as resolved.
Show resolved Hide resolved
]
)
, mask (big && soft && natural)
Expand Down
1 change: 1 addition & 0 deletions editors/emacs/swarm-mode.el
Original file line number Diff line number Diff line change
Expand Up @@ -161,6 +161,7 @@
"fail"
"not"
"format"
"read"
"chars"
"split"
"charat"
Expand Down
2 changes: 1 addition & 1 deletion editors/vim/swarm.vim
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
syn keyword Keyword def tydef rec end let in require
syn keyword Builtins self parent base if inl inr case fst snd force undefined fail not format chars split charat tochar key
syn keyword Builtins self parent base if inl inr case fst snd force undefined fail not format read chars split charat tochar key
syn keyword Command noop wait selfdestruct move backup volume path push stride turn grab harvest sow ignite place ping give equip unequip make has equipped count drill use build salvage reprogram say listen log view appear create halt time scout whereami locateme waypoint structure floorplan hastag tagmembers detect resonate density sniff chirp watch surveil heading blocked scan upload ishere isempty meet meetall whoami setname random run return try swap atomic instant installkeyhandler teleport warp as robotnamed robotnumbered knows
syn keyword Direction east north west south down forward left back right
syn match Type "\<[A-Z][a-zA-Z_]*\>"
Expand Down
2 changes: 1 addition & 1 deletion editors/vscode/syntaxes/swarm.tmLanguage.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ repository:
keyword:
name: keyword.other
match: >-
\b(self|parent|base|if|inl|inr|case|fst|snd|force|undefined|fail|not|format|chars|split|charat|tochar|key|noop|wait|selfdestruct|move|backup|volume|path|push|stride|turn|grab|harvest|sow|ignite|place|ping|give|equip|unequip|make|has|equipped|count|drill|use|build|salvage|reprogram|say|listen|log|view|appear|create|halt|time|scout|whereami|locateme|waypoint|structure|floorplan|hastag|tagmembers|detect|resonate|density|sniff|chirp|watch|surveil|heading|blocked|scan|upload|ishere|isempty|meet|meetall|whoami|setname|random|run|return|try|swap|atomic|instant|installkeyhandler|teleport|warp|as|robotnamed|robotnumbered|knows)\b
\b(self|parent|base|if|inl|inr|case|fst|snd|force|undefined|fail|not|format|read|chars|split|charat|tochar|key|noop|wait|selfdestruct|move|backup|volume|path|push|stride|turn|grab|harvest|sow|ignite|place|ping|give|equip|unequip|make|has|equipped|count|drill|use|build|salvage|reprogram|say|listen|log|view|appear|create|halt|time|scout|whereami|locateme|waypoint|structure|floorplan|hastag|tagmembers|detect|resonate|density|sniff|chirp|watch|surveil|heading|blocked|scan|upload|ishere|isempty|meet|meetall|whoami|setname|random|run|return|try|swap|atomic|instant|installkeyhandler|teleport|warp|as|robotnamed|robotnumbered|knows)\b
require:
name: keyword.control.require
match: \b(require)\b
Expand Down
1 change: 1 addition & 0 deletions src/swarm-engine/Swarm/Game/Step.hs
Original file line number Diff line number Diff line change
Expand Up @@ -561,6 +561,7 @@ stepCESK cesk = case cesk of
In (TInt n) _ s k -> return $ Out (VInt n) s k
In (TText str) _ s k -> return $ Out (VText str) s k
In (TBool b) _ s k -> return $ Out (VBool b) s k
In (TType ty) _ s k -> return $ Out (VType ty) s k
-- There should not be any antiquoted variables left at this point.
In (TAntiText v) _ s k ->
return $ Up (Fatal (T.append "Antiquoted variable found at runtime: $str:" v)) s k
Expand Down
1 change: 1 addition & 0 deletions src/swarm-engine/Swarm/Game/Step/Arithmetic.hs
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,7 @@ compareValues v1 = case v1 of
VSuspend {} -> incomparable v1
VExc {} -> incomparable v1
VBlackhole {} -> incomparable v1
VType {} -> incomparable v1

-- | Values with different types were compared; this should not be
-- possible since the type system should catch it.
Expand Down
6 changes: 6 additions & 0 deletions src/swarm-engine/Swarm/Game/Step/Const.hs
Original file line number Diff line number Diff line change
Expand Up @@ -87,6 +87,7 @@ import Swarm.Game.Universe
import Swarm.Game.Value
import Swarm.Language.Capability
import Swarm.Language.Key (parseKeyComboFull)
import Swarm.Language.Parser.Value (readValue)
import Swarm.Language.Pipeline
import Swarm.Language.Requirements qualified as R
import Swarm.Language.Syntax
Expand Down Expand Up @@ -1208,6 +1209,11 @@ execConst runChildProg c vs s k = do
Format -> case vs of
[v] -> return $ mkReturn $ prettyValue v
_ -> badConst
Read -> case vs of
[VType ty, VText txt] -> case readValue ty txt of
Nothing -> raise Read ["Could not read", showT txt, "at type", prettyText ty]
Just v -> return (mkReturn v)
_ -> badConst
Chars -> case vs of
[VText t] -> return $ mkReturn $ T.length t
_ -> badConst
Expand Down
3 changes: 3 additions & 0 deletions src/swarm-engine/Swarm/Game/Value.hs
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,9 @@ pattern VRect x1 y1 x2 y2 = VPair (VPair (VInt x1) (VInt y1)) (VPair (VInt x2) (
class Valuable a where
asValue :: a -> Value

instance Valuable Value where
asValue = id

instance Valuable Int32 where
asValue = VInt . fromIntegral

Expand Down
7 changes: 6 additions & 1 deletion src/swarm-lang/Swarm/Language/Elaborate.hs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ViewPatterns #-}

-- |
-- SPDX-License-Identifier: BSD-3-Clause
Expand All @@ -8,6 +9,7 @@ module Swarm.Language.Elaborate where

import Control.Lens (transform, (^.))
import Swarm.Language.Syntax
import Swarm.Language.Types

-- | Perform some elaboration / rewriting on a fully type-annotated
-- term. This currently performs such operations as rewriting @if@
Expand All @@ -23,7 +25,10 @@ elaborate :: TSyntax -> TSyntax
elaborate = transform rewrite
where
rewrite :: TSyntax -> TSyntax
rewrite (Syntax' l t cs ty) = Syntax' l (rewriteTerm t) cs ty
rewrite = \case
syn@(Syntax' l (TConst Read) cs pty@(ptBody -> TyText :->: outTy)) ->
Syntax' l (SApp syn (Syntax' NoLoc (TType outTy) mempty (mkTrivPoly TyUnit))) cs pty
Syntax' l t cs ty -> Syntax' l (rewriteTerm t) cs ty

rewriteTerm :: TTerm -> TTerm
rewriteTerm = \case
Expand Down
2 changes: 2 additions & 0 deletions src/swarm-lang/Swarm/Language/LSP/Hover.hs
Original file line number Diff line number Diff line change
Expand Up @@ -130,6 +130,7 @@ narrowToPosition s0@(Syntax' _ t _ ty) pos = fromMaybe s0 $ case t of
TVar {} -> Nothing
TRequire {} -> Nothing
TRequireDevice {} -> Nothing
TType {} -> Nothing
-- these should not show up in surface language
TRef {} -> Nothing
TRobot {} -> Nothing
Expand Down Expand Up @@ -203,6 +204,7 @@ explain trm = case trm ^. sTerm of
SRcd {} -> literal "A record literal."
SProj {} -> literal "A record projection."
STydef {} -> literal "A type synonym definition."
TType {} -> literal "A type literal."
-- type ascription
SAnnotate lhs typeAnn ->
Node
Expand Down
4 changes: 2 additions & 2 deletions src/swarm-lang/Swarm/Language/Parser/Record.hs
Original file line number Diff line number Diff line change
Expand Up @@ -16,8 +16,8 @@ import Swarm.Language.Parser.Lex (symbol, tmVar)
import Swarm.Util (failT, findDup, squote)
import Text.Megaparsec (sepBy)

-- | Parse something using record syntax of the form @{x1 v1, x2 v2,
-- ...}@. The same parser is used both in parsing record types and
-- | Parse something using record syntax of the form @x1 v1, x2 v2,
-- ...@. The same parser is used both in parsing record types and
-- record values, so it is factored out into its own module.
--
-- The @Parser a@ argument is the parser to use for the RHS of each
Expand Down
71 changes: 71 additions & 0 deletions src/swarm-lang/Swarm/Language/Parser/Value.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,71 @@
-- |
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Parse values of the Swarm language, indexed by type, by running the
-- full swarm-lang parser and then checking that the result is a value
-- of the proper type.
module Swarm.Language.Parser.Value (readValue) where

import Control.Lens ((^.))
import Data.Either.Extra (eitherToMaybe)
import Data.Text (Text)
import Swarm.Language.Context qualified as Ctx
import Swarm.Language.Key (parseKeyComboFull)
import Swarm.Language.Parser (readNonemptyTerm)
import Swarm.Language.Syntax
import Swarm.Language.Typecheck (checkTop)
import Swarm.Language.Types (Type)
import Swarm.Language.Value
import Text.Megaparsec qualified as MP

readValue :: Type -> Text -> Maybe Value
readValue ty txt = do
s <- eitherToMaybe $ readNonemptyTerm txt
_ <- eitherToMaybe $ checkTop Ctx.empty Ctx.empty Ctx.empty s ty
toValue $ s ^. sTerm

toValue :: Term -> Maybe Value
toValue = \case
TUnit -> Just VUnit
TDir d -> Just $ VDir d
TInt n -> Just $ VInt n
TText t -> Just $ VText t
TBool b -> Just $ VBool b
TApp (TConst c) t2 -> case c of
Neg -> toValue t2 >>= negateInt
Inl -> VInj False <$> toValue t2
Inr -> VInj True <$> toValue t2
Key -> do
VText k <- toValue t2
VKey <$> eitherToMaybe (MP.runParser parseKeyComboFull "" k)
_ -> Nothing
TPair t1 t2 -> VPair <$> toValue t1 <*> toValue t2
TRcd m -> VRcd <$> traverse (>>= toValue) m
-- List the other cases explicitly, instead of a catch-all, so that
-- we will get a warning if we ever add new constructors in the
-- future
TConst {} -> Nothing
TAntiInt {} -> Nothing
TAntiText {} -> Nothing
TRequireDevice {} -> Nothing
TRequire {} -> Nothing
TRequirements {} -> Nothing
TVar {} -> Nothing
TLam {} -> Nothing
TApp {} -> Nothing
TLet {} -> Nothing
TTydef {} -> Nothing
TBind {} -> Nothing
TDelay {} -> Nothing
TProj {} -> Nothing
TAnnotate {} -> Nothing
TSuspend {} -> Nothing

-- TODO(#2232): in order to get `read` to work for delay, function,
-- and/or command types, we will need to handle a few more of the
-- above cases, e.g. TConst, TLam, TApp, TLet, TBind, TDelay.

negateInt :: Value -> Maybe Value
negateInt = \case
VInt n -> Just (VInt (-n))
_ -> Nothing
2 changes: 2 additions & 0 deletions src/swarm-lang/Swarm/Language/Syntax/AST.hs
Original file line number Diff line number Diff line change
Expand Up @@ -142,6 +142,8 @@ data Term' ty
| -- | Run the given command, then suspend and wait for a new REPL
-- input.
SSuspend (Syntax' ty)
| -- | A type literal.
TType Type
deriving
( Eq
, Show
Expand Down
3 changes: 3 additions & 0 deletions src/swarm-lang/Swarm/Language/Syntax/Constants.hs
Original file line number Diff line number Diff line change
Expand Up @@ -271,6 +271,8 @@ data Const

-- | Turn an arbitrary value into a string
Format
| -- | Try to turn a string into a value
Read
| -- | Concatenate string values
Concat
| -- | Count number of characters.
Expand Down Expand Up @@ -813,6 +815,7 @@ constInfo c = case c of
Leq -> binaryOp "<=" 4 N $ shortDoc Set.empty "Check that the left value is lesser or equal to the right one."
Geq -> binaryOp ">=" 4 N $ shortDoc Set.empty "Check that the left value is greater or equal to the right one."
Format -> function 1 $ shortDoc Set.empty "Turn an arbitrary value into a string."
Read -> function 2 $ shortDoc Set.empty "Try to read a string into a value of the expected type."
Concat -> binaryOp "++" 6 R $ shortDoc Set.empty "Concatenate the given strings."
Chars -> function 1 $ shortDoc Set.empty "Counts the number of characters in the text."
Split ->
Expand Down
1 change: 1 addition & 0 deletions src/swarm-lang/Swarm/Language/Syntax/Pretty.hs
Original file line number Diff line number Diff line change
Expand Up @@ -136,6 +136,7 @@ instance PrettyPrec (Term' ty) where
SSuspend t ->
pparens (p > 10) $
"suspend" <+> prettyPrec 11 t
TType ty -> prettyPrec p ty

prettyDefinition :: Doc ann -> Var -> Maybe (Poly q Type) -> Syntax' ty -> Doc ann
prettyDefinition defName x mty t1 =
Expand Down
1 change: 1 addition & 0 deletions src/swarm-lang/Swarm/Language/Syntax/Util.hs
Original file line number Diff line number Diff line change
Expand Up @@ -145,6 +145,7 @@ freeVarsS f = go S.empty
SProj s1 x -> rewrap $ SProj <$> go bound s1 <*> pure x
SAnnotate s1 pty -> rewrap $ SAnnotate <$> go bound s1 <*> pure pty
SSuspend s1 -> rewrap $ SSuspend <$> go bound s1
TType {} -> pure s
where
rewrap s' = Syntax' l <$> s' <*> pure ty <*> pure cmts

Expand Down
7 changes: 7 additions & 0 deletions src/swarm-lang/Swarm/Language/Typecheck.hs
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ module Swarm.Language.Typecheck (

-- * Type inference
inferTop,
checkTop,
infer,
inferConst,
check,
Expand Down Expand Up @@ -811,6 +812,10 @@ decomposeProdTy = decomposeTyConApp2 TCProd
inferTop :: TCtx -> ReqCtx -> TDCtx -> Syntax -> Either ContextualTypeErr TSyntax
inferTop ctx reqCtx tdCtx = runTC ctx reqCtx tdCtx Ctx.empty . infer

-- | Top level type checking function.
checkTop :: TCtx -> ReqCtx -> TDCtx -> Syntax -> Type -> Either ContextualTypeErr TSyntax
checkTop ctx reqCtx tdCtx t ty = runTC ctx reqCtx tdCtx Ctx.empty $ check t (toU ty)

-- | Infer the type of a term, returning a type-annotated term.
--
-- The only cases explicitly handled in 'infer' are those where
Expand Down Expand Up @@ -1094,6 +1099,7 @@ inferConst c = run . runReader @TVCtx Ctx.empty . quantify $ case c of
Div -> arithBinT
Exp -> arithBinT
Format -> [tyQ| a -> Text |]
Read -> [tyQ| Text -> a |]
Concat -> [tyQ| Text -> Text -> Text |]
Chars -> [tyQ| Text -> Int |]
Split -> [tyQ| Int -> Text -> (Text * Text) |]
Expand Down Expand Up @@ -1387,6 +1393,7 @@ analyzeAtomic locals (Syntax l t) = case t of
TRequire {} -> return 0
SRequirements {} -> return 0
STydef {} -> return 0
TType {} -> return 0
-- Constants.
TConst c
-- Nested 'atomic' is not allowed.
Expand Down
17 changes: 16 additions & 1 deletion src/swarm-lang/Swarm/Language/Types.hs
Original file line number Diff line number Diff line change
Expand Up @@ -112,6 +112,7 @@ module Swarm.Language.Types (
tydefArity,
substTydef,
expandTydef,
expandTydefs,
elimTydef,
TDCtx,

Expand All @@ -125,10 +126,11 @@ module Swarm.Language.Types (
import Control.Algebra (Has, run)
import Control.Carrier.Reader (runReader)
import Control.Effect.Reader (Reader, ask)
import Control.Lens (makeLenses, view)
import Control.Lens (Plated (..), makeLenses, rewriteM, view)
import Control.Monad.Free
import Data.Aeson (FromJSON (..), FromJSON1 (..), ToJSON (..), ToJSON1 (..), genericLiftParseJSON, genericLiftToJSON, genericParseJSON, genericToJSON)
import Data.Data (Data)
import Data.Data.Lens (uniplate)
import Data.Eq.Deriving (deriveEq1)
import Data.Fix
import Data.Foldable (fold)
Expand Down Expand Up @@ -299,6 +301,9 @@ instance FromJSON1 TypeF where
-- with 'Type' as if it were defined in a directly recursive way.
type Type = Fix TypeF

instance Plated Type where
plate = uniplate

newtype IntVar = IntVar Int
deriving (Show, Data, Eq, Ord, Generic, Hashable)

Expand Down Expand Up @@ -818,6 +823,16 @@ expandTydef userTyCon tys = do
tydefInfo = fromMaybe (error errMsg) mtydefInfo
return $ substTydef tydefInfo tys

-- | Expand *all* applications of user-defined type constructors
-- everywhere in a type.
expandTydefs :: forall sig m. (Has (Reader TDCtx) sig m) => Type -> m Type
expandTydefs = rewriteM expand
where
expand :: Type -> m (Maybe Type)
expand = \case
TyUser u tys -> Just <$> expandTydef u tys
_ -> pure Nothing

-- | Given the definition of a type alias, substitute the given
-- arguments into its body and return the resulting type.
substTydef :: forall t. Typical t => TydefInfo -> [t] -> t
Expand Down
6 changes: 5 additions & 1 deletion src/swarm-lang/Swarm/Language/Value.hs
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ import Swarm.Language.Requirements.Type (ReqCtx, Requirements)
import Swarm.Language.Syntax
import Swarm.Language.Syntax.Direction
import Swarm.Language.Typed
import Swarm.Language.Types (Polytype, TCtx, TDCtx, TydefInfo)
import Swarm.Language.Types (Polytype, TCtx, TDCtx, TydefInfo, Type)
import Swarm.Pretty (prettyText)

-- | A /value/ is a term that cannot (or does not) take any more
Expand Down Expand Up @@ -119,6 +119,9 @@ data Value where
-- <http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html cannot detect
-- /all/ infinite loops this way>.)
VBlackhole :: Value
-- | A special value used to represent runtime type information
-- passed to ad-hoc polymorphic functions.
VType :: Type -> Value
deriving (Eq, Show, Generic, Hashable)

-- | A value context is a mapping from variable names to their runtime
Expand Down Expand Up @@ -241,3 +244,4 @@ valueToTerm = \case
VSuspend t _ -> TSuspend t
VExc -> TConst Undefined
VBlackhole -> TConst Undefined
VType _ -> TConst Undefined
1 change: 1 addition & 0 deletions swarm.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -460,6 +460,7 @@ library swarm-lang
Swarm.Language.Parser.Term
Swarm.Language.Parser.Type
Swarm.Language.Parser.Util
Swarm.Language.Parser.Value
Swarm.Language.Pipeline
Swarm.Language.Pipeline.QQ
Swarm.Language.Requirements
Expand Down
Loading
Loading