validate that imports only contain definitions + imports

Author: byorgey

src/swarm-lang/Swarm/Language/Load.hs

@@ -32,15 +32,18 @@ import Network.HTTP.Simple (getResponseBody, httpBS, parseRequest)
 import Swarm.Failure (Asset (..), AssetData (..), Entry (..), LoadingFailure (..), SystemFailure (..))
 import Swarm.Language.Parser (readTerm')
 import Swarm.Language.Parser.Core (defaultParserConfig, importLoc)
-import Swarm.Language.Syntax (ImportPhaseFor, Phase (..), SwarmType, Syntax)
+import Swarm.Language.Syntax
 import Swarm.Language.Syntax.Import hiding (ImportPhase (..))
 import Swarm.Language.Syntax.Import qualified as Import
-import Swarm.Language.Syntax.Util (Erasable(..), traverseSyntax)
+import Swarm.Language.Syntax.Util (Erasable(..))
 import Swarm.Language.Types (TCtx, UCtx)
+import Swarm.Pretty (prettyText)
 import Swarm.Util (readFileMayT, showT)
 import Swarm.Util.Graph (findCycle)
 import Witch (into)
 
+type ResLoc = ImportLoc Import.Resolved
+
 -- | The context for a module, containing names and types of things
 --   defined in the module (once typechecking has run).
 type family ModuleCtx (phase :: Phase) where
@@ -120,8 +123,6 @@ resolve' = traverseSyntax pure (throwError . DisallowedImport)
 eraseSourceMap :: SourceMap Elaborated -> SourceMap Resolved
 eraseSourceMap = M.map erase
 
-type ResLoc = ImportLoc Import.Resolved
-
 -- | Convert a 'SourceMap' into a suitable form for 'findCycle'.
 toImportGraph :: SourceMap Resolved -> [(ResLoc, ResLoc, [ResLoc])]
 toImportGraph = map processNode . M.assocs
@@ -172,8 +173,8 @@ resolveImport parent loc = do
   add $ S.singleton canonicalLoc
 
   srcMap <- get @(SourceMap Resolved)
-  case M.lookup canonicalLoc srcMap of
-    Just _ -> pure () -- Already loaded - do nothing
+  resMod <- case M.lookup canonicalLoc srcMap of
+    Just m -> pure m    -- Already loaded - do nothing
     Nothing -> do
       -- Record this import loc in the source map using a temporary, empty module,
       -- to prevent it from attempting to load itself recursively
@@ -188,14 +189,35 @@ resolveImport parent loc = do
       let (imps, mt') = sequence mres
 
       -- Finally, record the loaded module in the SourceMap.
-      modify @(SourceMap Resolved) (M.insert canonicalLoc $ Module mt' () imps)
+      let m = Module mt' () imps
+      modify @(SourceMap Resolved) (M.insert canonicalLoc m)
+
+      pure m
 
-  -- XXX make sure imports contain ONLY defs + more imports?
-  -- Otherwise we can't cache their values---we would have to
-  -- re-execute them every time they are imported.
+  -- Make sure imports are pure, i.e. contain ONLY defs + imports.
+  validateImport canonicalLoc resMod
 
   pure canonicalLoc
 
+-- | Validate the source code of the import to ensure that it contains
+--   *only* imports and definitions.  This is so we do not have to worry
+--   about side-effects happening every time a module is imported.  In
+--   other words, imports must be pure so we can get away with only
+--   evaluating them once.
+validateImport :: forall sig m. (Has (Throw SystemFailure) sig m) => ResLoc -> Module Resolved -> m ()
+validateImport loc = maybe (pure ()) validate . moduleTerm
+  where
+    validate :: Syntax Resolved -> m ()
+    validate = validateTerm . _sTerm
+
+    validateTerm :: Term Resolved -> m ()
+    validateTerm = \case
+      SLet LSDef _ _ _ _ _ _ t -> validate t
+      SImportIn _ t -> validate t
+      STydef _ _ _ t -> validate t
+      TConst Noop -> pure ()
+      t -> throwError $ ImpureImport loc (prettyText t)
+
 -- | Try to read and parse a term from a specific import location,
 --   either over the network or on disk.
 readLoc ::

src/swarm-lang/Swarm/Language/Typecheck.hs

@@ -1127,7 +1127,7 @@ infer s@(CSyntax l t cs) = addLocToTypeErr l $ case t of
     check s sTy
 
 -- | Collect up the names and types of any top-level definitions into
---   a context.
+--   a context. XXX this must collect tydefs as well!
 collectDefs ::
   (Has Unification sig m, Has (Reader UCtx) sig m) =>
   Syntax Inferred ->
@@ -1136,6 +1136,7 @@ collectDefs (Syntax _ (SLet LSDef _ x _ _ _ body t) _ _) = do
   ty' <- generalize (body ^. sType)
   (Ctx.singleton (lvVar x) ty' <>) <$> collectDefs t
 collectDefs (Syntax _ (SImportIn _ t) _ _) = collectDefs t
+collectDefs (Syntax _ (STydef _ _ _ t) _ _) = collectDefs t
 collectDefs _ = pure Ctx.empty
 
 -- | Infer the type of a module, i.e. import, by (1) typechecking and

src/swarm-util/Swarm/Failure.hs

@@ -28,7 +28,7 @@ import Data.Text.Encoding.Error qualified as T
 import Data.Void
 import Data.Yaml (ParseException, prettyPrintParseException)
 import Prettyprinter (Pretty (pretty), nest, squotes, vcat, (<+>))
-import Swarm.Language.Syntax.Import (ImportLoc, ImportPhase (Raw))
+import Swarm.Language.Syntax.Import (ImportLoc, ImportPhase (..))
 import Swarm.Language.Syntax.Loc (SrcLoc)
 import Swarm.Pretty (BulletList (..), PrettyPrec (..), ppr, prettyShowLow, prettyString)
 import Swarm.Util (showLowT)
@@ -89,6 +89,7 @@ data SystemFailure
   | ImportCycle [FilePath]
   | EmptyTerm
   | DisallowedImport (ImportLoc Raw)
+  | ImpureImport (ImportLoc Resolved) Text -- See Note [Pretty-printing typechecking errors]
   | CustomFailure Text
   deriving (Show)
 
@@ -162,4 +163,10 @@ instance PrettyPrec SystemFailure where
       ppr $ BulletList "Imports form a cycle:" (map (into @Text) imps)
     EmptyTerm -> "Term was only whitespace"
     DisallowedImport _imp -> "Import is not allowed here"
+    ImpureImport imp t ->
+      nest 2 . vcat $
+      [ "While processing import" <+> ppr imp <> ":"
+      , "Imported modules must only contain imports + definitions, but found:"
+      , squotes (pretty t)
+      ]
     CustomFailure m -> pretty m