Use List String for module name, add abstraction for loading files (prep for LSP)
This commit is contained in:
154
src/Lib/ProcessModule.newt
Normal file
154
src/Lib/ProcessModule.newt
Normal file
@@ -0,0 +1,154 @@
|
|||||||
|
module Lib.ProcessModule
|
||||||
|
|
||||||
|
import Prelude
|
||||||
|
import Serialize
|
||||||
|
import Lib.Types
|
||||||
|
import Lib.Common
|
||||||
|
import Lib.Syntax
|
||||||
|
import Lib.ProcessDecl
|
||||||
|
import Lib.TopContext
|
||||||
|
import Lib.Tokenizer
|
||||||
|
import Data.SortedMap
|
||||||
|
import Lib.Parser.Impl
|
||||||
|
import Lib.Parser
|
||||||
|
import Data.List1
|
||||||
|
import Lib.Elab
|
||||||
|
|
||||||
|
-- declare internal primitives
|
||||||
|
addPrimitives : M Unit
|
||||||
|
addPrimitives = do
|
||||||
|
processDecl primNS (PType emptyFC "Int" Nothing)
|
||||||
|
processDecl primNS (PType emptyFC "String" Nothing)
|
||||||
|
processDecl primNS (PType emptyFC "Char" Nothing)
|
||||||
|
setDef (QN primNS "PiType") emptyFC (Erased emptyFC) (PrimFn "(h0, h1) => ({ tag: \"PiType\", h0, h1 });" (S (S Z)) Nil) Nil
|
||||||
|
|
||||||
|
|
||||||
|
record FileSource where
|
||||||
|
getFile : FC → String → M (String × String)
|
||||||
|
|
||||||
|
parseDecls : String → Operators → TokenList → SnocList Decl → M (List Decl × Operators)
|
||||||
|
parseDecls fn ops Nil acc = pure (acc <>> Nil, ops)
|
||||||
|
parseDecls fn ops toks@(first :: _) acc =
|
||||||
|
case partialParse fn (sameLevel parseDecl) ops toks of
|
||||||
|
Left (err, toks) => do
|
||||||
|
putStrLn $ showError "" err
|
||||||
|
addError err
|
||||||
|
parseDecls fn ops (recover toks) acc
|
||||||
|
Right (decl,ops,toks) => parseDecls fn ops toks (acc :< decl)
|
||||||
|
where
|
||||||
|
recover : TokenList → TokenList
|
||||||
|
recover Nil = Nil
|
||||||
|
-- skip to top token, but make sure there is progress
|
||||||
|
recover (tok :: toks) = if tok.bounds.startCol == 0 && tok.bounds /= first.bounds
|
||||||
|
then (tok :: toks)
|
||||||
|
else recover toks
|
||||||
|
|
||||||
|
moduleHash : String → List (List String) → M String
|
||||||
|
moduleHash src imports = do
|
||||||
|
srcHash <- liftIO $ checksum src
|
||||||
|
top <- getTop
|
||||||
|
let mods = mapMaybe (\x => lookupMap' x top.modules) imports
|
||||||
|
let modHashes = map (\x => x.csum) mods
|
||||||
|
liftIO $ checksum $ fastConcat $ srcHash :: modHashes
|
||||||
|
|
||||||
|
importToName : Import → List String
|
||||||
|
importToName (MkImport fc (_,name)) = split name "."
|
||||||
|
|
||||||
|
importHints : List TopEntry → M Unit
|
||||||
|
importHints Nil = pure MkUnit
|
||||||
|
importHints (entry :: entries) = do
|
||||||
|
when (elem Hint entry.eflags) $ \ _ => addHint entry.name
|
||||||
|
importHints entries
|
||||||
|
|
||||||
|
processModule : FC → FileSource → List String → List String → M String
|
||||||
|
processModule importFC repo stk modns = do
|
||||||
|
top <- getTop
|
||||||
|
-- let modns = (snoc ns nm)
|
||||||
|
let name = joinBy "." modns
|
||||||
|
let (Nothing) = lookupMap modns top.modules | _ => pure ""
|
||||||
|
-- dummy entry for processing
|
||||||
|
modifyTop [modules := updateMap modns (emptyModCtx "") top.modules]
|
||||||
|
|
||||||
|
let fn = joinBy "/" modns ++ ".newt"
|
||||||
|
-- TODO now we can pass in the module name...
|
||||||
|
(fn,src) <- repo.getFile importFC fn
|
||||||
|
let (Right toks) = tokenise fn src
|
||||||
|
| Left err => throwError err
|
||||||
|
|
||||||
|
let (Right ((nameFC, modName), ops, toks)) = partialParse fn parseModHeader top.ops toks
|
||||||
|
| Left (err, toks) => throwError err
|
||||||
|
|
||||||
|
log 1 $ \ _ => "scan imports for module \{modName}"
|
||||||
|
let (True) = modns == split modName "."
|
||||||
|
| _ => throwError $ E nameFC "module name \{show modName} doesn't match file name \{show fn}"
|
||||||
|
|
||||||
|
let (Right (imports, ops, toks)) = partialParse fn parseImports ops toks
|
||||||
|
| Left (err, toks) => throwError err
|
||||||
|
|
||||||
|
let importNames = map importToName imports
|
||||||
|
|
||||||
|
imported <- for imports $ \case
|
||||||
|
MkImport fc (nameFC,name') => do
|
||||||
|
let imp = split name' "."
|
||||||
|
when (elem name' stk) $ \ _ => error nameFC "import loop \{show name} → \{show name'}"
|
||||||
|
processModule nameFC repo (name :: stk) imp
|
||||||
|
pure $ imp
|
||||||
|
let imported = snoc imported primNS
|
||||||
|
srcSum <- liftIO $ checksum src
|
||||||
|
csum <- moduleHash srcSum imported
|
||||||
|
|
||||||
|
putStrLn "module \{modName}"
|
||||||
|
top <- getTop
|
||||||
|
-- TODO we need a flag on this so `make newt3.js` properly tests self-compile
|
||||||
|
(Nothing) <- loadModule modns csum
|
||||||
|
| Just mod => do
|
||||||
|
let modules = updateMap modns mod top.modules
|
||||||
|
|
||||||
|
-- FIXME - we don't want stray operators in a module.
|
||||||
|
-- inject module ops into top
|
||||||
|
let ops = foldMap const top.ops $ toList mod.ctxOps
|
||||||
|
modifyTop [modules := modules; ops := ops ]
|
||||||
|
pure src -- why am I returning this?
|
||||||
|
|
||||||
|
log 1 $ \ _ => "MODNS " ++ show modns
|
||||||
|
top <- getTop
|
||||||
|
(decls, ops) <- parseDecls fn top.ops toks Lin
|
||||||
|
|
||||||
|
top <- getTop
|
||||||
|
let freshMC = MC emptyMap Nil 0 CheckAll
|
||||||
|
-- set imported, mod, freshMC, ops before processing
|
||||||
|
modifyTop [ imported := imported
|
||||||
|
; hints := emptyMap
|
||||||
|
; ns := modns
|
||||||
|
; defs := emptyMap
|
||||||
|
; metaCtx := freshMC
|
||||||
|
; ops := ops
|
||||||
|
]
|
||||||
|
for imported $ \ ns => do
|
||||||
|
let (Just mod) = lookupMap' ns top.modules | _ => error emptyFC "namespace \{show ns} missing"
|
||||||
|
importHints (listValues mod.modDefs)
|
||||||
|
|
||||||
|
log 1 $ \ _ => "process Decls"
|
||||||
|
traverse (tryProcessDecl src modns) (collectDecl decls)
|
||||||
|
|
||||||
|
-- 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 importNames
|
||||||
|
if stk /= Nil && length' top.errors == 0
|
||||||
|
then dumpModule modns src mod
|
||||||
|
else pure MkUnit
|
||||||
|
|
||||||
|
let modules = updateMap modns mod top.modules
|
||||||
|
modifyTop [modules := modules]
|
||||||
|
|
||||||
|
logMetas $ reverse $ listValues top.metaCtx.metas
|
||||||
|
let (Nil) = top.errors
|
||||||
|
| errors => throwError $ E importFC "Failed to compile module \{joinBy "." modns}"
|
||||||
|
pure src
|
||||||
|
where
|
||||||
|
tryProcessDecl : String → List String → Decl → M Unit
|
||||||
|
tryProcessDecl src ns decl = do
|
||||||
|
(Left err) <- tryError $ processDecl ns decl | _ => pure MkUnit
|
||||||
|
putStrLn $ showError src err
|
||||||
|
addError err
|
||||||
@@ -402,7 +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
|
modDeps : List (List String)
|
||||||
|
|
||||||
-- 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
|
||||||
|
|||||||
@@ -32,27 +32,20 @@ splitTele = go Nil
|
|||||||
go ts (Pi fc nm icit quant t u) = go (MkBinder fc nm icit quant t :: ts) u
|
go ts (Pi fc nm icit quant t u) = go (MkBinder fc nm icit quant t :: ts) u
|
||||||
go ts tm = (tm, reverse ts)
|
go ts tm = (tm, reverse ts)
|
||||||
|
|
||||||
|
-- given a filename and split module name, return the base path or an error
|
||||||
|
getBaseDir : String → FC → List String → M String
|
||||||
getBaseDir : String → FC → String → M (String × QName)
|
|
||||||
getBaseDir fn fc modName = do
|
getBaseDir fn fc modName = do
|
||||||
let (path, modName') = unsnoc $ split1 modName "."
|
let path = fst $ splitFileName fn
|
||||||
let parts = split1 fn "/"
|
let dirs = split path "/"
|
||||||
let (dirs,file) = unsnoc parts
|
let (Right base) = baseDir (Lin <>< dirs) (Lin <>< modName)
|
||||||
let (name, ext) = splitFileName file
|
|
||||||
|
|
||||||
let parts = split1 fn "/"
|
|
||||||
let (dirs,file) = unsnoc parts
|
|
||||||
let (path, modName') = unsnoc $ split1 modName "."
|
|
||||||
unless (modName' == name) $ \ _ => error fc "module name \{modName'} doesn't match \{name}"
|
|
||||||
let (Right base) = baseDir (Lin <>< dirs) (Lin <>< path)
|
|
||||||
| Left err => error fc err
|
| Left err => error fc err
|
||||||
let base = if base == "" then "." else base
|
let base = if base == "" then "." else base
|
||||||
pure (base, QN path modName')
|
pure base
|
||||||
where
|
where
|
||||||
baseDir : SnocList String -> SnocList String -> Either String String
|
baseDir : SnocList String -> SnocList String -> Either String String
|
||||||
baseDir dirs Lin = Right $ joinBy "/" (dirs <>> Nil)
|
baseDir dirs Lin = Right $ joinBy "/" (dirs <>> Nil)
|
||||||
baseDir (dirs :< d) (ns :< n) = if d == n
|
baseDir (dirs :< d) (ns :< n) = if d == n
|
||||||
then baseDir dirs ns
|
then baseDir dirs ns
|
||||||
else Left "module path doesn't match directory"
|
else Left "module name \{joinBy "." modName} doesn't match path \{fn}"
|
||||||
baseDir Lin _ = Left "module path doesn't match directory"
|
baseDir Lin _ = Left "module name \{joinBy "." modName} doesn't match path \{fn}"
|
||||||
|
|
||||||
|
|||||||
172
src/Main.newt
172
src/Main.newt
@@ -11,6 +11,7 @@ import Lib.Util
|
|||||||
import Lib.Parser.Impl
|
import Lib.Parser.Impl
|
||||||
import Lib.Prettier
|
import Lib.Prettier
|
||||||
import Lib.ProcessDecl
|
import Lib.ProcessDecl
|
||||||
|
import Lib.ProcessModule
|
||||||
import Lib.Tokenizer
|
import Lib.Tokenizer
|
||||||
import Lib.TopContext
|
import Lib.TopContext
|
||||||
import Lib.Types
|
import Lib.Types
|
||||||
@@ -20,6 +21,13 @@ import Node
|
|||||||
import Serialize
|
import Serialize
|
||||||
import Revision
|
import Revision
|
||||||
|
|
||||||
|
dirFileSource : String → FileSource
|
||||||
|
dirFileSource base = MkFileSource $ \fc fn => do
|
||||||
|
let fn = base ++ "/" ++ fn
|
||||||
|
(Right src) <- liftIO {M} $ readFile fn
|
||||||
|
| Left err => throwError $ E fc "error reading \{fn}: \{show err}"
|
||||||
|
pure (fn,src)
|
||||||
|
|
||||||
-- For editors, dump some information about the context (fc, name, type)
|
-- For editors, dump some information about the context (fc, name, type)
|
||||||
jsonTopContext : M Json
|
jsonTopContext : M Json
|
||||||
jsonTopContext = do
|
jsonTopContext = do
|
||||||
@@ -35,16 +43,6 @@ jsonTopContext = do
|
|||||||
:: ("type", toJson (render 80 $ pprint Nil type) )
|
:: ("type", toJson (render 80 $ pprint Nil type) )
|
||||||
:: Nil)
|
:: Nil)
|
||||||
|
|
||||||
dumpContext : TopContext -> M Unit
|
|
||||||
dumpContext top = do
|
|
||||||
putStrLn "Context:"
|
|
||||||
go $ listValues top.defs
|
|
||||||
putStrLn "---"
|
|
||||||
where
|
|
||||||
go : List TopEntry -> M Unit
|
|
||||||
go Nil = pure MkUnit
|
|
||||||
go (x :: xs) = putStrLn " \{show x}" >> go xs
|
|
||||||
|
|
||||||
writeSource : String -> M Unit
|
writeSource : String -> M Unit
|
||||||
writeSource fn = do
|
writeSource fn = do
|
||||||
docs <- compile
|
docs <- compile
|
||||||
@@ -57,139 +55,6 @@ writeSource fn = do
|
|||||||
| Left err => throwError $ E (MkFC fn $ MkBounds 0 0 0 0) err
|
| Left err => throwError $ E (MkFC fn $ MkBounds 0 0 0 0) err
|
||||||
pure MkUnit
|
pure MkUnit
|
||||||
|
|
||||||
|
|
||||||
parseDecls : String -> Operators -> TokenList -> SnocList Decl -> M (List Decl × Operators)
|
|
||||||
parseDecls fn ops Nil acc = pure (acc <>> Nil, ops)
|
|
||||||
parseDecls fn ops toks@(first :: _) acc =
|
|
||||||
case partialParse fn (sameLevel parseDecl) ops toks of
|
|
||||||
Left (err, toks) => do
|
|
||||||
putStrLn $ showError "" err
|
|
||||||
addError err
|
|
||||||
parseDecls fn ops (recover toks) acc
|
|
||||||
Right (decl,ops,toks) => parseDecls fn ops toks (acc :< decl)
|
|
||||||
where
|
|
||||||
recover : TokenList -> TokenList
|
|
||||||
recover Nil = Nil
|
|
||||||
-- skip to top token, but make sure there is progress
|
|
||||||
recover (tok :: toks) = if tok.bounds.startCol == 0 && tok.bounds /= first.bounds
|
|
||||||
then (tok :: toks)
|
|
||||||
else recover toks
|
|
||||||
|
|
||||||
moduleHash : String → List (List String) → M String
|
|
||||||
moduleHash src imports = do
|
|
||||||
srcHash <- liftIO $ checksum src
|
|
||||||
top <- getTop
|
|
||||||
let mods = mapMaybe (\x => lookupMap' x top.modules) imports
|
|
||||||
let modHashes = map (\x => x.csum) mods
|
|
||||||
liftIO $ checksum $ fastConcat $ srcHash :: modHashes
|
|
||||||
|
|
||||||
importHints : List TopEntry → M Unit
|
|
||||||
importHints Nil = pure MkUnit
|
|
||||||
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
|
|
||||||
top <- getTop
|
|
||||||
-- TODO make top.loaded a List QName
|
|
||||||
let modns = (snoc ns nm)
|
|
||||||
let name = joinBy "." modns
|
|
||||||
let (Nothing) = lookupMap modns top.modules | _ => pure ""
|
|
||||||
-- dummy entry for processing
|
|
||||||
modifyTop [modules := updateMap modns (emptyModCtx "") top.modules]
|
|
||||||
let fn = (joinBy "/" (base :: ns)) ++ "/" ++ nm ++ ".newt"
|
|
||||||
(Right src) <- liftIO {M} $ readFile fn
|
|
||||||
| Left err => throwError $ E importFC "error reading \{fn}: \{show err}"
|
|
||||||
let (Right toks) = tokenise fn src
|
|
||||||
| Left err => throwError err
|
|
||||||
|
|
||||||
let (Right ((nameFC, modName), ops, toks)) = partialParse fn parseModHeader top.ops toks
|
|
||||||
| Left (err, toks) => throwError err
|
|
||||||
|
|
||||||
log 1 $ \ _ => "scan imports for module \{modName}"
|
|
||||||
let ns = split modName "."
|
|
||||||
let (path, modName') = unsnoc $ split1 modName "."
|
|
||||||
-- let bparts = split base "/"
|
|
||||||
let (True) = qn == QN path modName'
|
|
||||||
| _ => throwError $ E nameFC "module name \{show modName} doesn't match file name \{show fn}"
|
|
||||||
|
|
||||||
let (Right (imports, ops, toks)) = partialParse fn parseImports ops toks
|
|
||||||
| Left (err, toks) => throwError err
|
|
||||||
|
|
||||||
let importNames = map importToQN imports
|
|
||||||
|
|
||||||
imported <- for imports $ \case
|
|
||||||
MkImport fc (nameFC,name') => do
|
|
||||||
let (a,b) = unsnoc $ split1 name' "."
|
|
||||||
let qname = QN a b
|
|
||||||
when (elem name' stk) $ \ _ => error nameFC "import loop \{show name} -> \{show name'}"
|
|
||||||
processModule nameFC base (name :: stk) qname
|
|
||||||
pure $ split name' "."
|
|
||||||
let imported = snoc imported primNS
|
|
||||||
srcSum <- liftIO $ checksum src
|
|
||||||
csum <- moduleHash srcSum imported
|
|
||||||
|
|
||||||
putStrLn "module \{modName}"
|
|
||||||
top <- getTop
|
|
||||||
-- TODO we need a flag on this so `make newt3.js` properly tests self-compile
|
|
||||||
(Nothing) <- loadModule qn csum
|
|
||||||
| Just mod => do
|
|
||||||
let modules = updateMap modns mod top.modules
|
|
||||||
|
|
||||||
-- FIXME - we don't want stray operators in a module.
|
|
||||||
-- inject module ops into top
|
|
||||||
let ops = foldMap const top.ops $ toList mod.ctxOps
|
|
||||||
modifyTop [modules := modules; ops := ops ]
|
|
||||||
pure src -- why am I returning this?
|
|
||||||
|
|
||||||
log 1 $ \ _ => "MODNS " ++ show modns
|
|
||||||
top <- getTop
|
|
||||||
(decls, ops) <- parseDecls fn top.ops toks Lin
|
|
||||||
|
|
||||||
top <- getTop
|
|
||||||
let freshMC = MC emptyMap Nil 0 CheckAll
|
|
||||||
-- set imported, mod, freshMC, ops before processing
|
|
||||||
modifyTop [ imported := imported
|
|
||||||
; hints := emptyMap
|
|
||||||
; ns := modns
|
|
||||||
; defs := emptyMap
|
|
||||||
; metaCtx := freshMC
|
|
||||||
; ops := ops
|
|
||||||
]
|
|
||||||
for imported $ \ ns => do
|
|
||||||
let (Just mod) = lookupMap' ns top.modules | _ => error emptyFC "namespace \{show ns} missing"
|
|
||||||
importHints (listValues mod.modDefs)
|
|
||||||
|
|
||||||
log 1 $ \ _ => "process Decls"
|
|
||||||
traverse (tryProcessDecl src ns) (collectDecl decls)
|
|
||||||
|
|
||||||
-- 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 importNames
|
|
||||||
if stk /= Nil && length' top.errors == 0
|
|
||||||
then dumpModule qn src mod
|
|
||||||
else pure MkUnit
|
|
||||||
|
|
||||||
let modules = updateMap modns mod top.modules
|
|
||||||
modifyTop [modules := modules]
|
|
||||||
|
|
||||||
logMetas $ reverse $ listValues top.metaCtx.metas
|
|
||||||
let (Nil) = top.errors
|
|
||||||
| errors => throwError $ E importFC "Failed to compile module \{show qn}"
|
|
||||||
pure src
|
|
||||||
where
|
|
||||||
tryProcessDecl : String -> List String → Decl -> M Unit
|
|
||||||
tryProcessDecl src ns decl = do
|
|
||||||
(Left err) <- tryError $ processDecl ns decl | _ => pure MkUnit
|
|
||||||
putStrLn $ showError src err
|
|
||||||
addError err
|
|
||||||
|
|
||||||
-- unwind the module part of the path name
|
-- unwind the module part of the path name
|
||||||
baseDir : SnocList String -> SnocList String -> Either String String
|
baseDir : SnocList String -> SnocList String -> Either String String
|
||||||
baseDir dirs Lin = Right $ joinBy "/" (dirs <>> Nil)
|
baseDir dirs Lin = Right $ joinBy "/" (dirs <>> Nil)
|
||||||
@@ -208,8 +73,8 @@ showErrors fn src = do
|
|||||||
throwError $ E (MkFC fn $ MkBounds 0 0 0 0) "Compile failed"
|
throwError $ E (MkFC fn $ MkBounds 0 0 0 0) "Compile failed"
|
||||||
pure MkUnit
|
pure MkUnit
|
||||||
|
|
||||||
invalidateModule : QName -> M Unit
|
invalidateModule : List String -> M Unit
|
||||||
invalidateModule (QN ns nm) = modifyTop [modules $= deleteMap (snoc ns nm)]
|
invalidateModule modname = modifyTop [modules $= deleteMap modname]
|
||||||
|
|
||||||
-- processFile called on the top level file
|
-- processFile called on the top level file
|
||||||
-- it sets up everything and then recurses into processModule
|
-- it sets up everything and then recurses into processModule
|
||||||
@@ -229,14 +94,9 @@ processFile fn = do
|
|||||||
let (Right ((nameFC, modName), _, _)) = partialParse fn parseModHeader emptyMap toks
|
let (Right ((nameFC, modName), _, _)) = partialParse fn parseModHeader emptyMap toks
|
||||||
| Left (err,toks) => throwError err
|
| Left (err,toks) => throwError err
|
||||||
|
|
||||||
(base,qn) <- getBaseDir fn nameFC modName
|
let modns = split modName "."
|
||||||
|
base <- getBaseDir fn nameFC modns
|
||||||
-- declare internal primitives
|
addPrimitives
|
||||||
|
|
||||||
processDecl primNS (PType emptyFC "Int" Nothing)
|
|
||||||
processDecl primNS (PType emptyFC "String" Nothing)
|
|
||||||
processDecl primNS (PType emptyFC "Char" Nothing)
|
|
||||||
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 Nil) top.modules
|
let modules = updateMap primNS (MkModCtx "" top.defs (MC emptyMap Nil 0 CheckAll) top.ops Nil) top.modules
|
||||||
@@ -247,9 +107,9 @@ processFile fn = do
|
|||||||
; defs := emptyMap
|
; defs := emptyMap
|
||||||
]
|
]
|
||||||
|
|
||||||
invalidateModule qn
|
invalidateModule modns
|
||||||
|
let repo = dirFileSource base
|
||||||
src <- processModule emptyFC base Nil qn
|
src <- processModule emptyFC repo Nil modns
|
||||||
top <- getTop
|
top <- getTop
|
||||||
|
|
||||||
showErrors fn src
|
showErrors fn src
|
||||||
|
|||||||
@@ -953,3 +953,5 @@ pfunc fatalError : ∀ a. String → a := `(_, msg) => { throw new Error(msg) }`
|
|||||||
|
|
||||||
foldlM : ∀ m a e. {{Monad m}} → (a → e → m a) → a → List e → m a
|
foldlM : ∀ m a e. {{Monad m}} → (a → e → m a) → a → List e → m a
|
||||||
foldlM f a xs = foldl (\ ma b => ma >>= flip f b) (pure a) xs
|
foldlM f a xs = foldl (\ ma b => ma >>= flip f b) (pure a) xs
|
||||||
|
|
||||||
|
pfunc unsafePerformIO : ∀ a. IO a → a := `(a, f) => f().h1`
|
||||||
|
|||||||
@@ -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) × List QName)
|
ModFile = (String × List TopEntry × List (String × OpDef) × List (QName × MetaEntry) × List (List String))
|
||||||
|
|
||||||
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);
|
||||||
@@ -32,9 +32,9 @@ pfunc dumpModFile uses (MkIORes MkUnit): String → ModFile → IO Unit := `(fn,
|
|||||||
|
|
||||||
|
|
||||||
-- for now, include src and use that to see if something changed
|
-- for now, include src and use that to see if something changed
|
||||||
dumpModule : QName → String → ModContext → M Unit
|
dumpModule : List String → String → ModContext → M Unit
|
||||||
dumpModule qn src mod = do
|
dumpModule qn src mod = do
|
||||||
let fn = "build/\{show qn}.newtmod"
|
let fn = "build/\{joinBy "." qn}.newtmod"
|
||||||
let csum = mod.csum
|
let csum = mod.csum
|
||||||
let defs = listValues mod.modDefs
|
let defs = listValues mod.modDefs
|
||||||
let ops = toList mod.ctxOps
|
let ops = toList mod.ctxOps
|
||||||
@@ -54,9 +54,9 @@ pfunc readModFile uses (MkIORes Just Nothing): String → IO (Maybe ModFile) :=
|
|||||||
}
|
}
|
||||||
}`
|
}`
|
||||||
|
|
||||||
loadModule : QName → String → M (Maybe ModContext)
|
loadModule : List String → String → M (Maybe ModContext)
|
||||||
loadModule qn src = do
|
loadModule qn src = do
|
||||||
let fn = "build/\{show qn}.newtmod"
|
let fn = "build/\{joinBy "." qn}.newtmod"
|
||||||
(Just (csum, defs, ops, mctx, deps)) <- liftIO {M} $ readModFile fn
|
(Just (csum, defs, ops, mctx, deps)) <- liftIO {M} $ readModFile fn
|
||||||
| _ => pure Nothing
|
| _ => pure Nothing
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user