Skip to content

Commit

Permalink
user-defined types
Browse files Browse the repository at this point in the history
  • Loading branch information
byorgey committed Jun 1, 2024
1 parent cb4e74b commit 6d002f5
Show file tree
Hide file tree
Showing 26 changed files with 370 additions and 129 deletions.
2 changes: 1 addition & 1 deletion editors/emacs/swarm-mode.el
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@
(let* (
;; Generate the current keywords with:
;; cabal run swarm:swarm-docs -- editors --emacs
(x-keywords '("def" "end" "let" "in" "require"))
(x-keywords '("def" "tydef" "end" "let" "in" "require"))
(x-builtins '(
"self"
"parent"
Expand Down
2 changes: 1 addition & 1 deletion editors/vim/swarm.vim
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
syn keyword Keyword def end let in require
syn keyword Keyword def tydef 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 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 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 as robotnamed robotnumbered knows
syn keyword Direction east north west south down forward left back right
Expand Down
9 changes: 9 additions & 0 deletions example/maybe.sw
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
tydef Maybe a = Unit + a end

def just : a -> Maybe a = inr end

def nothing : Maybe a = inl () end

def positive : Int -> Maybe Int = \x.
if (x > 0) {just x} {nothing}
end
14 changes: 6 additions & 8 deletions src/swarm-engine/Swarm/Game/CESK.hs
Original file line number Diff line number Diff line change
Expand Up @@ -95,7 +95,6 @@ import Swarm.Language.Context
import Swarm.Language.Module
import Swarm.Language.Pipeline
import Swarm.Language.Pretty
import Swarm.Language.Requirement (ReqCtx)
import Swarm.Language.Syntax
import Swarm.Language.Types
import Swarm.Language.Value as V
Expand Down Expand Up @@ -143,7 +142,7 @@ data Frame
-- we should take the resulting 'Env' and add it to the robot's
-- 'Swarm.Game.Robot.robotEnv', along with adding this accompanying 'Ctx' and
-- 'ReqCtx' to the robot's 'Swarm.Game.Robot.robotCtx'.
FLoadEnv TCtx ReqCtx
FLoadEnv Contexts
| -- | We were executing a definition; next we should take the resulting value
-- and return a context binding the variable to the value.
FDef Var
Expand Down Expand Up @@ -290,18 +289,17 @@ initMachine t e s = initMachine' t e s []

-- | Like 'initMachine', but also take an explicit starting continuation.
initMachine' :: ProcessedTerm -> Env -> Store -> Cont -> CESK
initMachine' (ProcessedTerm (Module t' ctx _tydefs) _ reqCtx) e s k =
initMachine' (ProcessedTerm (Module t' ctx tydefs) _ reqCtx) e s k =
case t' ^. sType of
-- If the starting term has a command type...
Forall _ (TyCmd _) ->
case ctx of
case (ctx, tydefs) of
-- ...but doesn't contain any definitions, just create a machine
-- that will evaluate it and then execute it.
Empty -> In t e s (FExec : k)
-- XXX do we also need to load tydefs?
(Empty, Empty) -> In t e s (FExec : k)
-- Or, if it does contain definitions, then load the resulting
-- context after executing it.
_ -> In t e s (FExec : FLoadEnv ctx reqCtx : k)
_ -> In t e s (FExec : FLoadEnv (Contexts ctx reqCtx tydefs) : k)
-- Otherwise, for a term with a non-command type, just
-- create a machine to evaluate it.
_ -> In t e s k
Expand Down Expand Up @@ -368,7 +366,7 @@ prettyFrame (FApp v) (p, inner) = (10, prettyPrec 10 (valueToTerm v) <+> pparens
prettyFrame (FLet x t _) (_, inner) = (11, hsep ["let", pretty x, "=", inner, "in", ppr t])
prettyFrame (FTry v) (p, inner) = (10, "try" <+> pparens (p < 11) inner <+> prettyPrec 11 (valueToTerm v))
prettyFrame (FUnionEnv _) inner = prettyPrefix "∪·" inner
prettyFrame (FLoadEnv _ _) inner = prettyPrefix "" inner
prettyFrame (FLoadEnv {}) inner = prettyPrefix "" inner
prettyFrame (FDef x) (_, inner) = (11, "def" <+> pretty x <+> "=" <+> inner <+> "end")
prettyFrame FExec inner = prettyPrefix "" inner
prettyFrame (FBind Nothing t _) (p, inner) = (0, pparens (p < 1) inner <+> ";" <+> ppr t)
Expand Down
6 changes: 4 additions & 2 deletions src/swarm-engine/Swarm/Game/Robot/Context.hs
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ import Swarm.Game.CESK qualified as C
import Swarm.Language.Context qualified as Ctx
import Swarm.Language.Requirement (ReqCtx)
import Swarm.Language.Typed (Typed (..))
import Swarm.Language.Types (TCtx)
import Swarm.Language.Types (TCtx, TDCtx)
import Swarm.Language.Value as V

-- | A record that stores the information
Expand All @@ -37,13 +37,15 @@ data RobotContext = RobotContext
, _defStore :: C.Store
-- ^ A store containing memory cells allocated to hold
-- definitions.
, _tydefVals :: TDCtx
-- ^ Type synonym definitions.
}
deriving (Eq, Show, Generic, Ae.FromJSON, Ae.ToJSON)

makeLenses ''RobotContext

emptyRobotContext :: RobotContext
emptyRobotContext = RobotContext Ctx.empty Ctx.empty Ctx.empty C.emptyStore
emptyRobotContext = RobotContext Ctx.empty Ctx.empty Ctx.empty C.emptyStore Ctx.empty

type instance Index RobotContext = Ctx.Var
type instance IxValue RobotContext = Typed Value
Expand Down
11 changes: 3 additions & 8 deletions src/swarm-engine/Swarm/Game/Scenario/Scoring/GenericMetrics.hs
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ import Data.Aeson
import Data.Ord (Down (Down))
import GHC.Generics (Generic)
import Swarm.Util (maxOn)
import Swarm.Util.JSON (optionsUntagged)

-- | This is a subset of the "ScenarioStatus" type
-- that excludes the "NotStarted" case.
Expand All @@ -17,17 +18,11 @@ data Progress
| Completed
deriving (Eq, Ord, Show, Read, Generic)

untaggedJsonOptions :: Options
untaggedJsonOptions =
defaultOptions
{ sumEncoding = UntaggedValue
}

instance FromJSON Progress where
parseJSON = genericParseJSON untaggedJsonOptions
parseJSON = genericParseJSON optionsUntagged

instance ToJSON Progress where
toJSON = genericToJSON untaggedJsonOptions
toJSON = genericToJSON optionsUntagged

data Metric a = Metric Progress a
deriving (Eq, Ord, Show, Read, Generic, FromJSON, ToJSON)
Expand Down
9 changes: 7 additions & 2 deletions src/swarm-engine/Swarm/Game/Step.hs
Original file line number Diff line number Diff line change
Expand Up @@ -791,12 +791,17 @@ stepCESK cesk = case cesk of
-- environment, store, and type and capability contexts into the robot's
-- top-level environment and contexts, so they will be available to
-- future programs.
Out (VResult v e) s (FLoadEnv ctx rctx : k) -> do
Out (VResult v e) s (FLoadEnv (Contexts ctx rctx tdctx) : k) -> do
robotContext . defVals %= (`union` e)
robotContext . defTypes %= (`union` ctx)
robotContext . defReqs %= (`union` rctx)
robotContext . tydefVals %= (`union` tdctx)
return $ Out v s k
Out v s (FLoadEnv (Contexts ctx rctx tdctx) : k) -> do
robotContext . defTypes %= (`union` ctx)
robotContext . defReqs %= (`union` rctx)
robotContext . tydefVals %= (`union` tdctx)
return $ Out v s k
Out v s (FLoadEnv {} : k) -> return $ Out v s k
-- Any other type of value wiwth an FExec frame is an error (should
-- never happen).
Out _ s (FExec : _) -> badMachineState s "FExec frame with non-executable value"
Expand Down
15 changes: 5 additions & 10 deletions src/swarm-engine/Swarm/Game/Step/Path/Type.hs
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@
module Swarm.Game.Step.Path.Type where

import Control.Lens
import Data.Aeson (Options (..), SumEncoding (ObjectWithSingleField), ToJSON (..), defaultOptions, genericToJSON)
import Data.Aeson (ToJSON (..), genericToJSON)
import Data.IntMap.Strict (IntMap)
import Data.List.NonEmpty (NonEmpty)
import Data.Map (Map)
Expand All @@ -28,6 +28,7 @@ import Swarm.Game.Location
import Swarm.Game.Robot (RID)
import Swarm.Game.Robot.Walk (WalkabilityContext)
import Swarm.Game.Universe (SubworldName)
import Swarm.Util.JSON (optionsObjectSingleField)
import Swarm.Util.Lens (makeLensesNoSigs)
import Swarm.Util.RingBuffer

Expand Down Expand Up @@ -67,19 +68,13 @@ data CacheLogEntry = CacheLogEntry
}
deriving (Show, Eq, Generic, ToJSON)

objectSingleFieldEncoding :: Options
objectSingleFieldEncoding =
defaultOptions
{ sumEncoding = ObjectWithSingleField
}

data CacheRetrievalAttempt
= Success
| RecomputationRequired CacheRetreivalInapplicability
deriving (Show, Eq, Generic)

instance ToJSON CacheRetrievalAttempt where
toJSON = genericToJSON objectSingleFieldEncoding
toJSON = genericToJSON optionsObjectSingleField

-- | Certain events can obligate the cache to be
-- completely invalidated, or partially or fully preserved.
Expand All @@ -90,7 +85,7 @@ data CacheEvent
deriving (Show, Eq, Generic)

instance ToJSON CacheEvent where
toJSON = genericToJSON objectSingleFieldEncoding
toJSON = genericToJSON optionsObjectSingleField

data DistanceLimitChange
= LimitIncreased
Expand All @@ -113,7 +108,7 @@ data CacheRetreivalInapplicability
deriving (Show, Eq, Generic)

instance ToJSON CacheRetreivalInapplicability where
toJSON = genericToJSON objectSingleFieldEncoding
toJSON = genericToJSON optionsObjectSingleField

-- | Reasons for cache being invalidated
data InvalidationReason
Expand Down
2 changes: 2 additions & 0 deletions src/swarm-lang/Swarm/Effect/Unify.hs
Original file line number Diff line number Diff line change
Expand Up @@ -50,4 +50,6 @@ data UnificationError where
Infinite :: IntVar -> UType -> UnificationError
-- | Mismatch error between the given terms.
UnifyErr :: TypeF UType -> TypeF UType -> UnificationError
-- | Encountered an undefined/unknown type constructor.
UndefinedUserType :: UType -> UnificationError
deriving (Show)
27 changes: 19 additions & 8 deletions src/swarm-lang/Swarm/Effect/Unify/Fast.hs
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ import Control.Applicative (Alternative)
import Control.Carrier.State.Strict (StateC, evalState)
import Control.Carrier.Throw.Either (ThrowC, runThrow)
import Control.Category ((>>>))
import Control.Effect.Reader (Reader)
import Control.Effect.State (State, get, gets, modify)
import Control.Effect.Throw (Throw, throwError)
import Control.Monad (zipWithM)
Expand Down Expand Up @@ -86,11 +87,6 @@ instance Substitutes IntVar UType UType where
------------------------------------------------------------
-- Carrier type

-- Note: this carrier type and the runUnification function are
-- identical between this module and Swarm.Effect.Unify.Naive, but it
-- seemed best to duplicate it, so we can modify the carriers
-- independently in the future if we want.

-- | Carrier type for unification: we maintain a current substitution,
-- a counter for generating fresh unification variables, and can
-- throw unification errors.
Expand All @@ -104,8 +100,13 @@ newtype UnificationC m a = UnificationC
newtype FreshVarCounter = FreshVarCounter {getFreshVarCounter :: Int}
deriving (Eq, Ord, Enum)

-- | Run a 'Unification' effect via the 'UnificationC' carrier.
runUnification :: Algebra sig m => UnificationC m a -> m (Either UnificationError a)
-- | Run a 'Unification' effect via the 'UnificationC' carrier. Note
-- that we also require an ambient @Reader 'TDCtx'@ effect, so unification
-- will be sure to pick up whatever type aliases happen to be in scope.
runUnification ::
(Algebra sig m, Has (Reader TDCtx) sig m) =>
UnificationC m a ->
m (Either UnificationError a)
runUnification =
unUnificationC >>> evalState idS >>> evalState (FreshVarCounter 0) >>> runThrow

Expand All @@ -132,7 +133,10 @@ runUnification =

-- | Implementation of the 'Unification' effect in terms of the
-- 'UnificationC' carrier.
instance Algebra sig m => Algebra (Unification :+: sig) (UnificationC m) where
instance
(Algebra sig m, Has (Reader TDCtx) sig m) =>
Algebra (Unification :+: sig) (UnificationC m)
where
alg hdl sig ctx = UnificationC $ case sig of
L (Unify t1 t2) -> (<$ ctx) <$> runThrow (unify t1 t2)
L (ApplyBindings t) -> do
Expand All @@ -152,6 +156,7 @@ instance Algebra sig m => Algebra (Unification :+: sig) (UnificationC m) where
-- instead lazily during substitution.
unify ::
( Has (Throw UnificationError) sig m
, Has (Reader TDCtx) sig m
, Has (State (Subst IntVar UType)) sig m
) =>
UType ->
Expand All @@ -165,13 +170,18 @@ unify ty1 ty2 = case (ty1, ty2) of
Nothing -> unifyVar x y
Just xv -> unify xv y
(x, Pure y) -> unify (Pure y) x
(UTyUser x1 tys, _) -> do
ty1' <- expandTydef x1 tys
unify ty1' ty2
(_, UTyUser {}) -> unify ty2 ty1
(Free t1, Free t2) -> Free <$> unifyF t1 t2

-- | Unify a unification variable which /is not/ bound by the current
-- substitution with another term. If the other term is also a
-- variable, we must look it up as well to see if it is bound.
unifyVar ::
( Has (Throw UnificationError) sig m
, Has (Reader TDCtx) sig m
, Has (State (Subst IntVar UType)) sig m
) =>
IntVar ->
Expand Down Expand Up @@ -199,6 +209,7 @@ unifyVar x t = modify (insert x t) >> pure t
-- contents.
unifyF ::
( Has (Throw UnificationError) sig m
, Has (Reader TDCtx) sig m
, Has (State (Subst IntVar UType)) sig m
) =>
TypeF UType ->
Expand Down
5 changes: 4 additions & 1 deletion src/swarm-lang/Swarm/Effect/Unify/Naive.hs
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,10 @@
-- substitutions, and returns a substitution from unification which
-- must then be composed with the substitution being tracked.
--
-- Not used in Swarm, but useful for testing/comparison.
-- Not used in Swarm, and also unmaintained
-- (e.g. "Swarm.Effect.Unify.Fast" now supports expanding type
-- aliases; this module does not). It's still here just for
-- testing/comparison.
module Swarm.Effect.Unify.Naive where

import Control.Algebra
Expand Down
6 changes: 5 additions & 1 deletion src/swarm-lang/Swarm/Language/Context.hs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
module Swarm.Language.Context where

import Control.Algebra (Has)
import Control.Effect.Reader (Reader, local)
import Control.Effect.Reader (Reader, ask, local)
import Control.Lens.Empty (AsEmpty (..))
import Control.Lens.Prism (prism)
import Data.Aeson (FromJSON, ToJSON)
Expand Down Expand Up @@ -53,6 +53,10 @@ singleton x t = Ctx (M.singleton x t)
lookup :: Var -> Ctx t -> Maybe t
lookup x (Ctx c) = M.lookup x c

-- | Look up a variable in a context in an ambient Reader effect.
lookupR :: Has (Reader (Ctx t)) sig m => Var -> m (Maybe t)
lookupR x = lookup x <$> ask

-- | Delete a variable from a context.
delete :: Var -> Ctx t -> Ctx t
delete x (Ctx c) = Ctx (M.delete x c)
Expand Down
22 changes: 14 additions & 8 deletions src/swarm-lang/Swarm/Language/Kindcheck.hs
Original file line number Diff line number Diff line change
Expand Up @@ -9,19 +9,21 @@ module Swarm.Language.Kindcheck (
) where

import Control.Algebra (Has)
import Control.Effect.Reader (Reader, ask)
import Control.Effect.Throw (Throw, throwError)
import Data.Fix (Fix (..))
import Swarm.Language.Types (Poly (..), Polytype, TyCon, Type, TypeF (..), getArity, tcArity)
import Swarm.Language.Types

-- | Kind checking errors that can occur. For now, the only possible
-- error is an arity mismatch error.
data KindError
= ArityMismatch TyCon [Type]
= ArityMismatch TyCon Int [Type]
| UndefinedTyCon TyCon Type
deriving (Eq, Show)

-- | Check that a polytype is well-kinded.
checkPolytypeKind :: Has (Throw KindError) sig m => Polytype -> m ()
checkPolytypeKind (Forall _ t) = checkKind t
checkPolytypeKind :: (Has (Reader TDCtx) sig m, Has (Throw KindError) sig m) => Polytype -> m TydefInfo
checkPolytypeKind pty@(Forall xs t) = TydefInfo pty (Arity $ length xs) <$ checkKind t

-- | Check that a type is well-kinded. For now, we don't allow
-- higher-kinded types, *i.e.* all kinds will be of the form @Type
Expand All @@ -32,9 +34,13 @@ checkPolytypeKind (Forall _ t) = checkKind t
-- well want to generalize to arbitrary higher kinds (e.g. @(Type ->
-- Type) -> Type@ etc.) which would require generalizing this
-- checking code a bit.
checkKind :: Has (Throw KindError) sig m => Type -> m ()
checkKind (Fix (TyConF c tys)) = case compare (length tys) (getArity (tcArity c)) of
EQ -> mapM_ checkKind tys
_ -> throwError $ ArityMismatch c tys
checkKind :: (Has (Reader TDCtx) sig m, Has (Throw KindError) sig m) => Type -> m ()
checkKind ty@(Fix (TyConF c tys)) = do
tdCtx <- ask
case getArity <$> tcArity tdCtx c of
Nothing -> throwError $ UndefinedTyCon c ty
Just a -> case compare (length tys) a of
EQ -> mapM_ checkKind tys
_ -> throwError $ ArityMismatch c a tys
checkKind (Fix (TyVarF _)) = return ()
checkKind (Fix (TyRcdF m)) = mapM_ checkKind m
2 changes: 1 addition & 1 deletion src/swarm-lang/Swarm/Language/LSP.hs
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,7 @@ validateSwarmCode doc version content = do
VU.Usage _ problems = VU.getUsage mempty term
unusedWarnings = mapMaybe (VU.toErrPos content) problems

parsingErrors = case processParsedTerm' mempty mempty term of
parsingErrors = case processParsedTerm' mempty term of
Right _ -> []
Left e -> pure $ showTypeErrorPos content e
Left e -> (pure $ showErrorPos e, [])
Expand Down
4 changes: 2 additions & 2 deletions src/swarm-lang/Swarm/Language/Module.hs
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ import Data.Yaml (FromJSON, ToJSON)
import GHC.Generics (Generic)
import Swarm.Language.Context (Ctx, empty)
import Swarm.Language.Syntax (Syntax')
import Swarm.Language.Types (Polytype, UPolytype, UType)
import Swarm.Language.Types (Polytype, TDCtx, UPolytype, UType)

------------------------------------------------------------
-- Modules
Expand All @@ -37,7 +37,7 @@ import Swarm.Language.Types (Polytype, UPolytype, UType)
data Module s t = Module
{ _moduleSyntax :: Syntax' s
, _moduleCtx :: Ctx t
, _moduleTydefs :: Ctx Polytype
, _moduleTydefs :: TDCtx
}
deriving (Show, Eq, Functor, Data, Generic, FromJSON, ToJSON)

Expand Down
Loading

0 comments on commit 6d002f5

Please sign in to comment.