diff --git a/playground/samples/DSL.newt b/playground/samples/DSL.newt index e2f03bd..234d48d 100644 --- a/playground/samples/DSL.newt +++ b/playground/samples/DSL.newt @@ -95,7 +95,7 @@ enumMul (x :: xs) ys = map (_,_ x) ys ++ enumMul xs ys enumerate : (t : E) → Vec (typ t) (card t) enumerate Zero = Nil -enumerate One = unit :: Nil +enumerate One = MkUnit :: Nil enumerate (Add x y) = enumAdd (enumerate x) (enumerate y) enumerate (Mul x y) = enumMul (enumerate x) (enumerate y) diff --git a/src/Commands.newt b/src/Commands.newt index 0540e51..cc3dd78 100644 --- a/src/Commands.newt +++ b/src/Commands.newt @@ -28,12 +28,8 @@ decomposeName fn = switchModule : FileSource → String → M ModContext switchModule repo modns = do - addPrimitives - modifyTop [ metaCtx := MC emptyMap Nil 0 CheckAll ] mod <- processModule emptyFC repo Nil modns - -- FIXME keep these in ModContext, drop from TopContext - modifyTop [ defs := mod.modDefs; metaCtx := mod.modMetaCtx; ops := mod.ctxOps; imported := mod.modDeps; infos := mod.modInfos; ns := modns; errors := mod.modErrors ] - top <- getTop + modifyTop [ currentMod := mod; ops := mod.modOps ] pure mod -- The cheap version of type at point, find the token, lookup in global context @@ -112,7 +108,7 @@ makeEdits : FC → List QName → Bool → M (List FileEdit) makeEdits fc@(MkFC uri (MkBounds sr sc er ec)) names inPlace = do cons <- map applyDCon <$> traverse lookupDCon names top <- getTop - let (Just mod) = lookupMap' top.ns top.modules | _ => pure Nil + let (Just mod) = lookupMap' top.currentMod.modName top.modules | _ => pure Nil let lines = split mod.modSource "\n" let (Just line) = getAt' sr lines | _ => pure Nil let cs = unpack line @@ -171,7 +167,7 @@ getActions : FileSource → String → Int → Int → M (List CodeAction) getActions repo modns row col = do mod <- switchModule repo modns top <- getTop - let xx = filter (posInFC row col ∘ getFC) top.infos + let xx = filter (posInFC row col ∘ getFC) top.currentMod.modInfos putStrLn "Filter got \{show $ length' xx}" go Nil $ xx where diff --git a/src/LSP.newt b/src/LSP.newt index 341cebe..dc0d0c7 100644 --- a/src/LSP.newt +++ b/src/LSP.newt @@ -1,7 +1,6 @@ module LSP import Prelude --- TODO pull this into its own file import Lib.Common import Lib.Eval import Lib.Types @@ -165,7 +164,7 @@ errorToDiag (Postpone fc qn msg) = errorToDiag $ E fc "Postpone \{show qn} \{msg getInfos : M (List Json) getInfos = do top <- getTop - go Nil $ listValues $ top.metaCtx.metas + go Nil $ listValues $ top.currentMod.modMetaCtx.metas where go : List Json → List MetaEntry → M (List Json) go acc Nil = pure acc @@ -194,13 +193,12 @@ checkFile fn = unsafePerformIO $ do then resetState base else pure MkUnit (Right (top, json)) <- (do - modifyTop [ errors := Nil ] putStrLn "processModule" _ <- switchModule lspFileSource modName -- pull out errors and infos top <- getTop - let errors = map (errorToDiag) top.errors + let errors = map (errorToDiag) top.currentMod.modErrors infos <- getInfos pure $ infos ++ errors ).runM st.topContext diff --git a/src/Lib/Compile.newt b/src/Lib/Compile.newt index 4ea3a1c..656e564 100644 --- a/src/Lib/Compile.newt +++ b/src/Lib/Compile.newt @@ -516,8 +516,8 @@ process names = do compile : M (List Doc) compile = do top <- getTop - let exports = getExports Nil $ listValues top.defs - let mainName = (QN top.ns "main") + let exports = getExports Nil $ listValues top.currentMod.modDefs + let mainName = (QN top.currentMod.modName "main") let main = lookup mainName top let todo = case main of Nothing => exports diff --git a/src/Lib/CompileExp.newt b/src/Lib/CompileExp.newt index 8ae5e4e..0e287d8 100644 --- a/src/Lib/CompileExp.newt +++ b/src/Lib/CompileExp.newt @@ -267,7 +267,7 @@ compileDCon ix (QN _ nm) info arity = -- probably want to drop the Ref2 when we can defToCExp : {{Ref2 Defs St}} → (QName × Def) -> M (QName × CExp) -defToCExp (qn, Axiom) = pure (qn, CErased) +defToCExp (qn, Axiom) = error emptyFC "\{show qn} is Axiom" -- pure (qn, CErased) defToCExp (qn, (PrimOp _)) = (_,_ qn) <$> compilePop qn defToCExp (qn, DCon ix info arity _) = pure (qn, compileDCon ix qn info arity) -- We're not using these are runtime at the moment, no typecase diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index 1ece5c8..5a9b844 100644 --- a/src/Lib/Elab.newt +++ b/src/Lib/Elab.newt @@ -119,7 +119,10 @@ isCandidate _ _ = False setMetaMode : MetaMode → M Unit -- ideally we would support dotted paths like metaCtx.mcmode := CheckFirst -setMetaMode mcmode = modifyTop [ metaCtx $= [mcmode := mcmode] ] +setMetaMode mcmode = modifyTop [ currentMod $= [modMetaCtx $= [mcmode := mcmode] ] ] + +setMetaContext : MetaContext → M Unit +setMetaContext mc = modifyTop [ currentMod $= [ modMetaCtx := mc ]] findMatches : Context -> Val -> List (QName × Tm) -> M (List QName) findMatches ctx ty Nil = pure Nil @@ -129,7 +132,7 @@ findMatches ctx ty ((name, type) :: xs) = do top <- getTop -- save context - let mc = top.metaCtx + let mc = top.currentMod.modMetaCtx catchError (do -- TODO sort out the FC here let fc = getFC ty @@ -140,11 +143,11 @@ findMatches ctx ty ((name, type) :: xs) = do setMetaMode CheckFirst tm <- check ctx (RVar fc nm) ty debug $ \ _ => "Found \{rpprint Nil tm} for \{show ty}" - modifyTop [ metaCtx := mc ] + setMetaContext mc (_::_ name) <$> findMatches ctx ty xs) (\ err => do debug $ \ _ => "No match \{show ty} \{rpprint Nil type} \{showError "" err}" - modifyTop [ metaCtx := mc ] + setMetaContext mc findMatches ctx ty xs) contextMatches : Context -> Val -> M (List (Tm × Val)) @@ -156,17 +159,17 @@ contextMatches ctx ty = go (zip ctx.env ctx.types) type <- quote ctx.lvl vty let (True) = isCandidate ty type | False => go xs top <- getTop - let mc = top.metaCtx + let mc = top.currentMod.modMetaCtx catchError(do debug $ \ _ => "TRY context \{nm} : \{rpprint (names ctx) type} for \{show ty}" unifyCatch (getFC ty) ctx ty vty - let mc' = top.metaCtx - modifyTop [ metaCtx := mc] + let mc' = top.currentMod.modMetaCtx + setMetaContext mc tm <- quote ctx.lvl tm (_::_ (tm, vty)) <$> go xs) (\ err => do debug $ \ _ => "No match \{show ty} \{rpprint (names ctx) type} \{showError "" err}" - modifyTop [ metaCtx := mc] + setMetaContext mc go xs) getArity : Tm -> List Quant @@ -229,7 +232,7 @@ trySolveAuto _ = pure False solveAutos : M Unit solveAutos = do top <- getTop - let mc = top.metaCtx + let mc = top.currentMod.modMetaCtx let autos = filter isAuto $ mapMaybe (flip lookupMap' mc.metas) mc.autos res <- run autos -- If anything is solved, we try again from the top @@ -248,13 +251,13 @@ solveAutos = do updateMeta : QName -> (MetaEntry -> M MetaEntry) -> M Unit updateMeta ix f = do top <- getTop - let mc = top.metaCtx + let mc = top.currentMod.modMetaCtx let (Just me) = lookupMap' ix mc.metas | Nothing => pure MkUnit me <- f me let autos = case me of Solved _ _ _ => filter (_/=_ ix) mc.autos _ => mc.autos - modifyTop [ metaCtx := MC (updateMap ix me mc.metas) autos mc.next mc.mcmode ] + setMetaContext $ [metas $= updateMap ix me; autos := autos] mc -- Try to solve autos that reference the meta ix checkAutos : QName -> List QName -> M Unit @@ -278,7 +281,7 @@ checkAutos ix (_ :: rest) = checkAutos ix rest addConstraint : Env -> QName -> SnocList Val -> Val -> M Unit addConstraint env ix sp tm = do top <- getTop - let mc = top.metaCtx + let mc = top.currentMod.modMetaCtx let (CheckAll) = mc.mcmode | _ => pure MkUnit updateMeta ix $ \case (Unsolved pos k a b c cons) => do @@ -373,7 +376,7 @@ ctx.boundNames = map snd $ filter (\x => fst x == Bound) $ zip ctx.bds (map fst maybeCheck : M Unit -> M Unit maybeCheck action = do top <- getTop - let mc = top.metaCtx + let mc = top.currentMod.modMetaCtx case mc.mcmode of CheckAll => action CheckFirst => do @@ -426,7 +429,7 @@ solve env m sp t = do unify env UNormal val rhs -- check any autos top <- getTop - let mc = top.metaCtx + let mc = top.currentMod.modMetaCtx let (CheckAll) = mc.mcmode | _ => pure MkUnit debug $ \ _ => "check autos depending on \{show ix} \{debugStr mc.mcmode}" checkAutos ix mc.autos @@ -617,16 +620,17 @@ unifyCatch fc ctx ty' ty = do freshMeta : Context -> FC -> Val -> MetaKind -> M Tm freshMeta ctx fc ty kind = do top <- getTop - let mc = top.metaCtx + let mc = top.currentMod.modMetaCtx debug $ \ _ => "fresh meta \{show mc.next} : \{show ty} (\{show kind})" -- need the ns here -- we were fudging this for v1 - let qn = QN top.ns "$m\{show mc.next}" + let qn = QN top.currentMod.modName "$m\{show mc.next}" let newmeta = Unsolved fc qn ctx ty kind Nil let autos = case kind of AutoSolve => qn :: mc.autos _ => mc.autos - modifyTop [metaCtx := MC (updateMap qn newmeta mc.metas) autos (1 + mc.next) mc.mcmode ] + setMetaContext $ [ metas $= updateMap qn newmeta; autos := autos; next $= 1 +] mc + -- I tried checking Auto immediately if CheckAll, but there isn't enough information yet. pure $ applyBDs 0 (Meta fc qn) ctx.bds where diff --git a/src/Lib/ProcessDecl.newt b/src/Lib/ProcessDecl.newt index 98818ad..6bb8605 100644 --- a/src/Lib/ProcessDecl.newt +++ b/src/Lib/ProcessDecl.newt @@ -51,7 +51,6 @@ logMetas (Unsolved fc k ctx ty User cons :: rest) = do logMetas (Unsolved fc k ctx ty kind cons :: rest) = do ty' <- forceMeta ty tm <- quote ctx.lvl ty' - -- FIXME in Combinatory.newt, the val doesn't match environment? let msg = "Unsolved meta \{show k} \{show kind} type \{render 90 $ pprint (names ctx) tm} \{show $ length' cons} constraints" msgs <- for cons $ \case (MkMc fc env sp val) => do @@ -69,7 +68,7 @@ logMetas (Unsolved fc k ctx ty kind cons :: rest) = do pure (" \{show $ length' matches} Solutions: \{show matches}" :: Nil) _ => pure Nil - -- info fc $ unlines ((msg :: Nil) ++ msgs ++ sols) + addError $ E fc $ unlines ((msg :: Nil) ++ msgs ++ sols) logMetas rest @@ -95,7 +94,7 @@ impTele tele = map foo tele checkAlreadyDef : FC → Name → M Unit checkAlreadyDef fc nm = do top <- getTop - case lookup (QN top.ns nm) top of + case lookup (QN top.currentMod.modName nm) top of Nothing => pure MkUnit Just entry => error fc "\{show nm} is already defined at \{show entry.fc}" @@ -158,7 +157,7 @@ processDef ns fc nm clauses = do log 1 $ \ _ => "-----" log 1 $ \ _ => "Def \{show nm}" top <- getTop - let mc = top.metaCtx + let mc = top.currentMod.modMetaCtx let (Just entry) = lookup (QN ns nm) top | Nothing => throwError $ E fc "No declaration for \{nm}" let (MkEntry fc name ty Axiom _) = entry @@ -436,7 +435,7 @@ processData ns fc (nameFC, nm) ty cons = do log 1 $ \ _ => "-----" log 1 $ \ _ => "Data \{nm}" top <- getTop - let mc = top.metaCtx + let mc = top.currentMod.modMetaCtx tyty <- check (mkCtx fc) ty (VU fc) case lookup (QN ns nm) top of Just (MkEntry _ name type Axiom _) => do diff --git a/src/Lib/ProcessModule.newt b/src/Lib/ProcessModule.newt index 39d1c65..2eff71a 100644 --- a/src/Lib/ProcessModule.newt +++ b/src/Lib/ProcessModule.newt @@ -16,21 +16,14 @@ import Lib.Elab -- declare internal primitives addPrimitives : M ModContext addPrimitives = do + modifyTop [ currentMod := emptyModCtx "Prim" ""; hints := emptyMap; ops := emptyMap ] 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 - let mod = MkModCtx "" top.defs (MC emptyMap Nil 0 CheckAll) top.ops Nil top.errors Nil - let modules = updateMap primNS mod top.modules - -- TODO - do we clear this? Try just modules := modules, but wait until this refactor is done. - modifyTop [ modules := modules - ; imported := primNS :: Nil - ; hints := emptyMap - ; ns := "" - ; defs := emptyMap - ] - pure mod + modifyTop [ modules $= updateMap primNS top.currentMod ] + pure top.currentMod record FileSource where getFile : FC → String → M (String × String) @@ -60,9 +53,11 @@ importHints (entry :: entries) = do when (elem Hint entry.eflags) $ \ _ => addHint entry.name importHints entries --- HACK this is returning src to help render errors.. --- Maybe return module, put src and errors in module, add error for import with error, callers can sort out what they want to do? --- The issue here is command line newt wants to report all errors (we can print that though?) LSP wants something more subtle +mergeOps : Operators → Operators → Operators +mergeOps mod top = foldMap (flip const) top $ toList mod + +-- processModule might reset the currentModule in the topContext +-- do not rely on topContext state afterwards - it may or may not contain the module processModule : FC → FileSource → List String → String → M ModContext processModule importFC repo stk modns = do top <- getTop @@ -70,8 +65,8 @@ processModule importFC repo stk modns = do let (Nothing) = lookupMap' modns top.modules | Just mod => pure mod - let (False) = modns == primNS - | _ => addPrimitives + let (False) = modns == primNS | _ => addPrimitives + let parts = split modns "." let fn = joinBy "/" parts ++ ".newt" -- TODO now we can pass in the module name... @@ -92,47 +87,60 @@ processModule importFC repo stk modns = do imported <- for imports $ \case MkImport fc (nameFC, name') => do when (elem name' stk) $ \ _ => error nameFC "import loop \{modns} → \{name'}" - processModule nameFC repo (modns :: stk) name' + mod <- processModule nameFC repo (modns :: stk) name' pure $ name' + processModule nameFC repo (modns :: stk) primNS let imported = snoc imported primNS putStrLn "module \{modName}" + top <- getTop + let freshMC = MC emptyMap Nil 0 CheckAll + let mod = MkModCtx modns src emptyMap freshMC emptyMap imported Nil Nil + modifyTop [ currentMod := mod + ; hints := emptyMap + ; ops := ops + ] - log 1 $ \ _ => "MODNS " ++ show modns + -- top hints / ops include all directly imported modules + for_ imports $ \case + (MkImport fc (nameFC, ns)) => do + let (Just mod) = lookupMap' ns top.modules | _ => error emptyFC "namespace \{show ns} missing" + importHints (listValues mod.modDefs) + modifyTop [ ops $= mergeOps mod.modOps ] + + -- add error if an import contains an error + -- maybe move this to after reporting + case mod.modErrors of + Nil => pure MkUnit + _ => addError $ E nameFC "Error in import \{ns}" + + log 1 $ \ _ => "parse Decls" top <- getTop (decls, ops) <- parseDecls fn top.ops toks Lin - top <- getTop - let freshMC = MC emptyMap Nil 0 CheckAll - -- NOW Print and drop errors here - -- clear per module fields before processing this module - modifyTop [ imported := imported - ; hints := emptyMap - ; ns := modns - ; defs := emptyMap - ; infos := Nil - ; 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) + -- TODO only include this module's ops + -- aside from reworking parsing, we could filter + -- other options are removing updates from parsing (so we must use incremental parsing) + -- or removing pratt from parsing (so it happens in elaboration) + modifyTop [ currentMod $= [ modOps := ops ] ] log 1 $ \ _ => "process Decls" traverse (tryProcessDecl src modns) (collectDecl decls) + top <- getTop -- This has addErrors as a side-effect - logMetas $ reverse $ listValues top.metaCtx.metas + logMetas $ reverse $ listValues top.currentMod.modMetaCtx.metas + + -- print errors (for batch processing case) + for_ top.currentMod.modErrors $ \ err => putStrLn $ showError src err -- update modules with result, leave the rest of context in case this is top file top <- getTop - let mod = MkModCtx src top.defs top.metaCtx top.ops imported top.errors top.infos - let modules = updateMap modns mod top.modules + let modules = updateMap modns top.currentMod top.modules modifyTop [modules := modules] - -- FIXME module context should hold errors, to report in replay - pure mod + pure top.currentMod where tryProcessDecl : String → String → Decl → M Unit tryProcessDecl src ns decl = do diff --git a/src/Lib/TopContext.newt b/src/Lib/TopContext.newt index c91dd01..cb201f9 100644 --- a/src/Lib/TopContext.newt +++ b/src/Lib/TopContext.newt @@ -7,32 +7,31 @@ import Prelude import Lib.Common import Lib.Types --- I want unique ids, to be able to lookup, update, and a Ref so --- I don't need good Context discipline. (I seem to have made mistakes already.) - +-- TODO move the def in here (along with M) or merge this into types +-- The Monad can be its own file if we pull all of the monad update functions there. lookup : QName -> TopContext -> Maybe TopEntry lookup qn@(QN ns nm) top = - if ns == top.ns - then lookupMap' qn top.defs + if ns == top.currentMod.modName + then lookupMap' qn top.currentMod.modDefs else case lookupMap' ns top.modules of Just mod => lookupMap' qn mod.modDefs Nothing => Nothing lookupImported : String → TopContext -> List TopEntry lookupImported raw top = - mapMaybe (flip lookup top) $ (QN top.ns raw) :: map (flip QN raw) top.imported + mapMaybe (flip lookup top) $ (QN top.currentMod.modName raw) :: map (flip QN raw) top.currentMod.modDeps -- For repl / out of scope errors lookupAll : String → TopContext -> List TopEntry lookupAll raw top = - mapMaybe (flip lookup top) $ (QN top.ns raw) :: map (flip QN raw) (map fst $ toList top.modules) + mapMaybe (flip lookup top) $ (QN top.currentMod.modName raw) :: map (flip QN raw) (map fst $ toList top.modules) lookupRaw : String -> TopContext -> Maybe TopEntry lookupRaw raw top = - case lookupMap' (QN top.ns raw) top.defs of + case lookupMap' (QN top.currentMod.modName raw) top.currentMod.modDefs of Just entry => Just entry - Nothing => go top.imported + Nothing => go top.currentMod.modDeps where go : List String → Maybe TopEntry go Nil = Nothing @@ -42,35 +41,33 @@ lookupRaw raw top = Just entry => Just entry Nothing => go nss - instance Show TopContext where - show top = "\nContext:\n [\{ joinBy "\n" $ map (show ∘ snd) $ toList top.defs}]" + show top = "\nContext:\n [\{ joinBy "\n" $ map (show ∘ snd) $ toList top.currentMod.modDefs}]" emptyTop : TopContext -emptyTop = MkTop emptyMap Nil emptyMap Nil "" emptyMap (MC emptyMap Nil 0 CheckAll) 0 Nil emptyMap - +emptyTop = MkTop emptyMap emptyMap (emptyModCtx "" "") 0 emptyMap setFlag : QName → FC → EFlag → M Unit setFlag name fc flag = do top <- getTop - let (Just (MkEntry fc nm ty def flags)) = lookupMap' name top.defs + let (Just (MkEntry fc nm ty def flags)) = lookupMap' name top.currentMod.modDefs | Nothing => error fc "\{show name} not declared" - modifyTop [ defs $= (updateMap name (MkEntry fc name ty def (flag :: flags))) ] + modifyTop [ currentMod $= [ modDefs $= (updateMap name (MkEntry fc name ty def (flag :: flags)))] ] setDef : QName -> FC -> Tm -> Def → List EFlag -> M Unit setDef name fc ty def flags = do top <- getTop - let (Nothing) = lookupMap' name top.defs + let (Nothing) = lookupMap' name top.currentMod.modDefs | Just (MkEntry fc' nm' ty' def' _) => error fc "\{show name} is already defined at \{show fc'}" - modifyTop $ \top => - [ defs := (updateMap name (MkEntry fc name ty def flags) top.defs)] top + + modifyTop [currentMod $= [ modDefs $= (updateMap name (MkEntry fc name ty def flags))] ] updateDef : QName -> FC -> Tm -> Def -> M Unit updateDef name fc ty def = do top <- getTop - let (Just (MkEntry fc' nm' ty' def' flags)) = lookupMap' name top.defs + let (Just (MkEntry fc' nm' ty' def' flags)) = lookupMap' name top.currentMod.modDefs | Nothing => error fc "\{show name} not declared" - putTop $ [ defs := updateMap name (MkEntry fc' name ty def flags) top.defs ] top + modifyTop [ currentMod $= [ modDefs := updateMap name (MkEntry fc' name ty def flags) top.currentMod.modDefs ] ] typeName : Tm → Maybe QName typeName (Pi fc nm Explicit rig t u) = Nothing @@ -88,15 +85,11 @@ addHint qn = do | Nothing => error entry.fc "can't find tcon name for \{show qn}" let xs = fromMaybe Nil $ lookupMap' tyname top.hints let hints = updateMap tyname ((qn, entry.type) :: xs) top.hints - putTop $ [ hints := hints ] top + modifyTop [ hints := hints ] Nothing => pure MkUnit addError : Error -> M Unit -addError err = do - top <- getTop - modifyTop [ errors $= (err ::) ] +addError err = modifyTop [ currentMod $= [ modErrors $= (err ::) ] ] addInfo : EditorInfo → M Unit -addInfo info = do - top <- getTop - modifyTop [ infos $= (info ::)] +addInfo info = modifyTop [ currentMod $= [modInfos $= (info ::) ] ] diff --git a/src/Lib/Types.newt b/src/Lib/Types.newt index 8016ca0..edb4eeb 100644 --- a/src/Lib/Types.newt +++ b/src/Lib/Types.newt @@ -398,12 +398,13 @@ data EditorInfo record ModContext where constructor MkModCtx + modName : String modSource : String modDefs : SortedMap QName TopEntry -- Do we need this if everything solved is zonked? modMetaCtx : MetaContext -- longer term maybe drop this, put the operator decls in ctxDefs and collect them on import - ctxOps : Operators + modOps : Operators modDeps : List String modErrors : List Error modInfos : List EditorInfo @@ -416,8 +417,8 @@ record ModContext where -- expand these during normalization? -- A placeholder while walking through dependencies of a module -emptyModCtx : String → ModContext -emptyModCtx source = MkModCtx source emptyMap (MC emptyMap Nil 0 NoCheck) emptyMap Nil Nil Nil +emptyModCtx : String → String → ModContext +emptyModCtx modName source = MkModCtx modName source emptyMap (MC emptyMap Nil 0 NoCheck) emptyMap Nil Nil Nil HintTable : U HintTable = SortedMap QName (List (QName × Tm)) @@ -428,23 +429,17 @@ instance HasFC EditorInfo where getFC (CaseSplit fc _ _ _) = fc getFC (MissingCases fc _ _) = fc - +-- modules are "modules" +-- currentMod represents the current module +-- when we switch modules, load imports into ops and hints +-- as we process the decls, update ops and currentMod.ops record TopContext where constructor MkTop modules : SortedMap String ModContext - imported : List String - -- TCon name → function name × type hints : HintTable - infos : List EditorInfo - -- current module - ns : String - defs : SortedMap QName TopEntry - metaCtx : MetaContext - - -- Global values - verbose : Int -- command line flag - errors : List Error + currentMod : ModContext + verbose : Int -- command line flag increments this ops : Operators -- we'll use this for typechecking, but need to keep a TopContext around too. @@ -592,7 +587,7 @@ error' msg = throwError $ E emptyFC msg lookupMeta : QName -> M MetaEntry lookupMeta ix@(QN ns nm) = do top <- getTop - case lookupMap' ix top.metaCtx.metas of + case lookupMap' ix top.currentMod.modMetaCtx.metas of Just meta => pure meta Nothing => case lookupMap' ns top.modules of Nothing => diff --git a/src/Main.newt b/src/Main.newt index 5d5bf2a..cd2fe25 100644 --- a/src/Main.newt +++ b/src/Main.newt @@ -65,11 +65,8 @@ baseDir Lin _ = Left "module path doesn't match directory" showErrors : String -> String -> M Unit showErrors fn src = do top <- getTop - -- TODO {M} needed to sort out scrutinee - let (Nil) = top.errors - | errors => do - traverse (putStrLn ∘ showError src) errors - throwError $ E (MkFC fn $ MkBounds 0 0 0 0) "Compile failed" + let (Nil) = top.currentMod.modErrors + | _ => throwError $ E (MkFC fn $ MkBounds 0 0 0 0) "Compile failed" pure MkUnit