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