diff --git a/src/Lib/Types.newt b/src/Lib/Types.newt index faa1061..6558bac 100644 --- a/src/Lib/Types.newt +++ b/src/Lib/Types.newt @@ -402,6 +402,7 @@ record ModContext where modMetaCtx : MetaContext -- longer term maybe drop this, put the operator decls in ctxDefs and collect them on import ctxOps : Operators + modDeps : List QName -- Top level context. -- Most of the reason this is separate is to have a different type @@ -412,7 +413,7 @@ record ModContext where -- A placeholder while walking through dependencies of a module emptyModCtx : String → ModContext -emptyModCtx csum = MkModCtx csum emptyMap (MC emptyMap Nil 0 NoCheck) emptyMap +emptyModCtx csum = MkModCtx csum emptyMap (MC emptyMap Nil 0 NoCheck) emptyMap Nil HintTable : U HintTable = SortedMap QName (List (QName × Tm)) diff --git a/src/Main.newt b/src/Main.newt index a48f0c3..eed682e 100644 --- a/src/Main.newt +++ b/src/Main.newt @@ -91,6 +91,9 @@ importHints (entry :: entries) = do when (elem Hint entry.eflags) $ \ _ => addHint entry.name importHints entries +importToQN : Import → QName +importToQN (MkImport fc name') = uncurry QN $ unsnoc $ split1 name' "." + -- New style loader, one def at a time processModule : FC -> String -> List String -> QName -> M String processModule importFC base stk qn@(QN ns nm) = do @@ -120,6 +123,8 @@ processModule importFC base stk qn@(QN ns nm) = do let (Right (imports, ops, toks)) = partialParse fn parseImports ops toks | Left (err, toks) => exitFailure (showError src err) + let importNames = map importToQN imports + imported <- for imports $ \case MkImport fc name' => do let (a,b) = unsnoc $ split1 name' "." @@ -164,7 +169,7 @@ processModule importFC base stk qn@(QN ns nm) = do -- update modules with result, leave the rest of context in case this is top file top <- getTop - let mod = MkModCtx csum top.defs top.metaCtx top.ops + let mod = MkModCtx csum top.defs top.metaCtx top.ops importNames if stk /= Nil && length' top.errors == 0 then dumpModule qn src mod else pure MkUnit @@ -229,7 +234,7 @@ processFile fn = do setDef (QN primNS "PiType") emptyFC (Erased emptyFC) (PrimFn "(h0, h1) => ({ tag: \"PiType\", h0, h1 });" (S (S Z)) Nil) Nil top <- getTop - let modules = updateMap primNS (MkModCtx "" top.defs (MC emptyMap Nil 0 CheckAll) top.ops) top.modules + let modules = updateMap primNS (MkModCtx "" top.defs (MC emptyMap Nil 0 CheckAll) top.ops Nil) top.modules modifyTop (\ top => MkTop modules (primNS :: Nil) emptyMap Nil emptyMap top.metaCtx top.verbose top.errors top.ops) src <- processModule emptyFC base Nil qn diff --git a/src/Serialize.newt b/src/Serialize.newt index 65c95e2..49a214e 100644 --- a/src/Serialize.newt +++ b/src/Serialize.newt @@ -7,7 +7,7 @@ import Lib.Types import Data.SortedMap ModFile : U -ModFile = (String × List TopEntry × List (String × OpDef) × List (QName × MetaEntry)) +ModFile = (String × List TopEntry × List (String × OpDef) × List (QName × MetaEntry) × List QName) pfunc checksum uses (MkIORes) : String → IO String := `(a) => (w) => { const arr = new TextEncoder().encode(a); @@ -39,7 +39,8 @@ dumpModule qn src mod = do let defs = listValues mod.modDefs let ops = toList mod.ctxOps let mctx = toList mod.modMetaCtx.metas - liftIO $ dumpModFile fn (csum,defs,ops,mctx) + let deps = mod.modDeps + liftIO $ dumpModFile fn (csum,defs,ops,mctx, deps) pfunc readModFile uses (MkIORes Just Nothing): String → IO (Maybe ModFile) := `(fn) => (w) => { let fs = require('fs') @@ -56,7 +57,7 @@ pfunc readModFile uses (MkIORes Just Nothing): String → IO (Maybe ModFile) := loadModule : QName → String → M (Maybe ModContext) loadModule qn src = do let fn = "build/\{show qn}.newtmod" - (Just (csum, defs, ops, mctx)) <- liftIO {M} $ readModFile fn + (Just (csum, defs, ops, mctx, deps)) <- liftIO {M} $ readModFile fn | _ => pure Nothing let ops = mapFromList ops @@ -64,5 +65,5 @@ loadModule qn src = do -- REVIEW can we ignore those last two inside a module let mctx = MC (mapFromList mctx) Nil 0 NoCheck if csum == src - then pure $ Just $ MkModCtx csum defs mctx ops + then pure $ Just $ MkModCtx csum defs mctx ops deps else pure Nothing