diff --git a/src/Commands.newt b/src/Commands.newt index 796afe8..903d2e4 100644 --- a/src/Commands.newt +++ b/src/Commands.newt @@ -12,19 +12,19 @@ import Lib.Token import Lib.Elab -- For now we cheat and assume capitalized directories are a module component -decomposeName : String → String × List String +decomposeName : String → String × String decomposeName fn = go Nil $ Lin <>< split (fst $ splitFileName fn) "/" where - go : List String → SnocList String → String × List String - go acc Lin = (".", acc) + go : List String → SnocList String → String × String + go acc Lin = (".", joinBy "." acc) go acc (xs :< x) = if isUpper $ strIndex x 0 then go (x :: acc) xs - else (joinBy "/" (xs :< x <>> Nil), acc) + else (joinBy "/" (xs :< x <>> Nil), joinBy "." acc) -- The cheap version of type at point, find the token, lookup in global context -- Later we will either get good FC for entries or scan them all and build a cache. -getHoverInfo : FileSource → List String → Int → Int → M (Maybe (String × FC)) +getHoverInfo : FileSource → String → Int → Int → M (Maybe (String × FC)) getHoverInfo repo modns row col = do mod <- processModule emptyFC repo Nil modns -- not necessarily loaded into top... (Maybe push this down into that branch of processModule) diff --git a/src/LSP.newt b/src/LSP.newt index 681c72e..276ed7a 100644 --- a/src/LSP.newt +++ b/src/LSP.newt @@ -73,7 +73,7 @@ updateFile fn src = unsafePerformIO $ do let (Right ((nameFC, modName), _, _)) = partialParse fn parseModHeader emptyMap toks | Left (err,toks) => writeIORef state st - Right (ctx,_) <- (invalidateModule $ split modName ".").runM st.topContext + Right (ctx,_) <- (invalidateModule modName).runM st.topContext | _ => writeIORef state st -- TODO It doesn't have record type, but eta expanding resolves this. See if there is a quick fix. -- modifyIORef state [ topContext := ctx ] @@ -90,7 +90,7 @@ fcToRange (MkFC uri (MkBounds sr sc er ec)) = hoverInfo : String → Int → Int → JSObject hoverInfo uri line col = unsafePerformIO $ do let (base,modns) = decomposeName uri - putStrLn "Hover \{uri} base \{base} mod \{joinBy "." modns}" + putStrLn "Hover \{uri} base \{base} mod \{modns}" st <- readIORef state if (st.baseDir /= base) then resetState base @@ -119,8 +119,9 @@ errorToDiag (Postpone fc qn msg) = errorToDiag $ E fc "Postpone \{show qn} \{msg checkFile : String → JSObject checkFile fn = unsafePerformIO $ do - let (base,modns) = decomposeName fn - putStrLn "Checking \{fn} base \{base} mod \{joinBy "." modns}" + let (base,modName) = decomposeName fn + + putStrLn "Checking \{fn} base \{base} mod \{modName}" st <- readIORef state if (st.baseDir /= base) then resetState base @@ -128,7 +129,7 @@ checkFile fn = unsafePerformIO $ do (Right (top, json)) <- (do modifyTop [ errors := Nil ] putStrLn "processModule" - _ <- processModule emptyFC lspFileSource Nil modns + _ <- processModule emptyFC lspFileSource Nil modName pure MkUnit -- pull out errors and infos top <- getTop diff --git a/src/Lib/Common.newt b/src/Lib/Common.newt index 03806e5..9084951 100644 --- a/src/Lib/Common.newt +++ b/src/Lib/Common.newt @@ -132,8 +132,8 @@ fcCol fc = fc.bnds.startCol class HasFC a where getFC : a -> FC -primNS : List String -primNS = ("Prim" :: Nil) +primNS : String +primNS = "Prim" emptyFC : FC emptyFC = MkFC "" (MkBounds 0 0 0 0) @@ -141,10 +141,9 @@ emptyFC = MkFC "" (MkBounds 0 0 0 0) emptyFC' : String → FC emptyFC' fn = MkFC fn (MkBounds 0 0 0 0) --- Error of a parse - +-- Using a String instead of List String for the module shaved about 16% of compile time... data QName : U where - QN : List String -> String -> QName + QN : String -> String -> QName .baseName : QName → String (QN _ name).baseName = name @@ -154,8 +153,8 @@ instance Eq QName where QN ns n == QN ns' n' = if n == n' then ns == ns' else False instance Show QName where - show (QN Nil n) = n - show (QN ns n) = joinBy "." ns ++ "." ++ n + show (QN "" n) = n + show (QN ns n) = ns ++ "." ++ n instance Ord QName where compare (QN ns nm) (QN ns' nm') = if ns == ns' then compare nm nm' else compare ns ns' diff --git a/src/Lib/CompileExp.newt b/src/Lib/CompileExp.newt index b4cab63..d9e045a 100644 --- a/src/Lib/CompileExp.newt +++ b/src/Lib/CompileExp.newt @@ -157,7 +157,7 @@ compileTerm tm@(App _ _ _) = case funArgs tm of applySucc Nil = pure $ CLam "x" $ CPrimOp "+" (CLit $ LInt 1) (CBnd 0) applySucc (t :: Nil) = pure $ CPrimOp "+" (CLit $ LInt 1) t applySucc _ = error emptyFC "overapplied Succ \{show tm}" -compileTerm (UU _) = pure $ CRef (QN Nil "U") +compileTerm (UU _) = pure $ CRef (QN "" "U") compileTerm (Pi _ nm icit rig t u) = do t' <- compileTerm t u' <- compileTerm u diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index fe4ca6e..dd38ec6 100644 --- a/src/Lib/Elab.newt +++ b/src/Lib/Elab.newt @@ -1549,7 +1549,7 @@ infer ctx tm@(RUpdateRec fc _ _) = do infer ctx (RVar fc nm) = go 0 ctx.types where entryNS : TopEntry → String - entryNS (MkEntry fc (QN ns _) _ _ _) = joinBy "." ns + entryNS (MkEntry fc (QN ns _) _ _ _) = ns go : Int -> List (String × Val) -> M (Tm × Val) go i Nil = do diff --git a/src/Lib/ProcessDecl.newt b/src/Lib/ProcessDecl.newt index a9f91ec..d17e169 100644 --- a/src/Lib/ProcessDecl.newt +++ b/src/Lib/ProcessDecl.newt @@ -100,9 +100,9 @@ checkAlreadyDef fc nm = do Just entry => error fc "\{show nm} is already defined at \{show entry.fc}" -processDecl : List String -> Decl -> M Unit +processDecl : String -> Decl -> M Unit -processTypeSig : List String → FC → List Name → Raw → M Unit +processTypeSig : String → FC → List Name → Raw → M Unit processTypeSig ns fc names tm = do log 1 $ \ _ => "-----" top <- getTop @@ -112,7 +112,7 @@ processTypeSig ns fc names tm = do ignore $ for names $ \nm => setDef (QN ns nm) fc ty Axiom Nil -processPrimType : List Name → FC → Name → Maybe Raw → M Unit +processPrimType : String → FC → Name → Maybe Raw → M Unit processPrimType ns fc nm ty = do top <- getTop ty' <- check (mkCtx fc) (maybe (RU fc) id ty) (VU fc) @@ -120,7 +120,7 @@ processPrimType ns fc nm ty = do setDef (QN ns nm) fc ty' (PrimTCon arity) Nil -processPrimFn : List String → FC → String → List String → Raw → String → M Unit +processPrimFn : String → FC → String → List String → Raw → String → M Unit processPrimFn ns fc nm used ty src = do top <- getTop ty <- check (mkCtx fc) ty (VU fc) @@ -153,7 +153,7 @@ complexity (Lit _ _) = 0 complexity (Case _ sc (CaseCons _ _ t :: Nil)) = 1 + complexity sc + complexity t complexity _ = 100 -processDef : List String → FC → String → List (Raw × Maybe Raw) → M Unit +processDef : String → FC → String → List (Raw × Maybe Raw) → M Unit processDef ns fc nm clauses = do log 1 $ \ _ => "-----" log 1 $ \ _ => "Def \{show nm}" @@ -194,7 +194,7 @@ processDef ns fc nm clauses = do then setFlag (QN ns nm) fc Inline else pure MkUnit -processCheck : List String → FC → Raw → Raw → M Unit +processCheck : String → FC → Raw → Raw → M Unit processCheck ns fc tm ty = do log 1 $ \ _ => "----- DCheck" top <- getTop @@ -209,7 +209,7 @@ processCheck ns fc tm ty = do putStrLn " NF \{render 90 $ pprint Nil norm}" -processClass : List String → FC → (FC × String) → Telescope → List Decl → M Unit +processClass : String → FC → (FC × String) → Telescope → List Decl → M Unit processClass ns classFC (nameFC, nm) tele decls = do -- REVIEW maybe we can leverage Record for this -- a couple of catches, we don't want the dotted accessors and @@ -257,7 +257,7 @@ processClass ns classFC (nameFC, nm) tele decls = do mkApp : Raw → BindInfo × Raw → Raw mkApp acc (BI fc nm icit _, _) = RApp fc acc (RVar fc nm) icit -processInstance : List String → FC → Raw → Maybe (List Decl) → M Unit +processInstance : String → FC → Raw → Maybe (List Decl) → M Unit processInstance ns instfc ty decls = do log 1 $ \ _ => "-----" log 1 $ \ _ => "Instance \{render 90 $ pretty ty}" @@ -372,7 +372,7 @@ processInstance ns instfc ty decls = do apply x (y :: xs) = error instfc "expected pi type \{show x}" -- desugars to Data and processes it -processShortData : List String → FC → Raw → List Raw → M Unit +processShortData : String → FC → Raw → List Raw → M Unit processShortData ns fc lhs sigs = do (nameFC, nm,args) <- getArgs lhs Nil let ty = foldr mkPi (RU fc) args @@ -431,7 +431,7 @@ populateConInfo entries = isSucc (MkEntry fc nm dty@(Pi _ _ _ _ (Ref _ a) (Ref _ b)) (DCon _ _ (Many :: Nil) hn) _) = a == b isSucc _ = False -processData : List String → FC → FC × String → Raw → List Decl → M Unit +processData : String → FC → FC × String → Raw → List Decl → M Unit processData ns fc (nameFC, nm) ty cons = do log 1 $ \ _ => "-----" log 1 $ \ _ => "Data \{nm}" @@ -487,7 +487,7 @@ processData ns fc (nameFC, nm) ty cons = do checkDeclType _ = error fc "data type doesn't return U" -processRecord : List String → FC → FC × String → Telescope → Maybe (FC × Name) → List Decl → M Unit +processRecord : String → FC → FC × String → Telescope → Maybe (FC × Name) → List Decl → M Unit processRecord ns recordFC (nameFC, nm) tele cname decls = do log 1 $ \ _ => "-----" log 1 $ \ _ => "Record" diff --git a/src/Lib/ProcessModule.newt b/src/Lib/ProcessModule.newt index 4d59240..57965b9 100644 --- a/src/Lib/ProcessModule.newt +++ b/src/Lib/ProcessModule.newt @@ -23,10 +23,11 @@ addPrimitives = do top <- getTop let mod = MkModCtx "" top.defs (MC emptyMap Nil 0 CheckAll) top.ops Nil top.errors 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 := Nil + ; ns := "" ; defs := emptyMap ] pure mod @@ -62,17 +63,17 @@ importHints (entry :: entries) = do -- 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 -processModule : FC → FileSource → List String → (stack : List String) → M ModContext +processModule : FC → FileSource → List String → String → M ModContext processModule importFC repo stk modns = do top <- getTop - let name = joinBy "." modns + let (Nothing) = lookupMap' modns top.modules | Just mod => pure mod let (False) = modns == primNS | _ => addPrimitives - - let fn = joinBy "/" modns ++ ".newt" + let parts = split modns "." + let fn = joinBy "/" parts ++ ".newt" -- TODO now we can pass in the module name... (fn,src) <- repo.getFile importFC fn let (Right toks) = tokenise fn src @@ -82,21 +83,18 @@ processModule importFC repo stk modns = do | Left (err, toks) => throwError err log 1 $ \ _ => "scan imports for module \{modName}" - let (True) = modns == split modName "." + let (True) = modns == 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 - processModule nameFC repo (name :: stk) primNS + when (elem name' stk) $ \ _ => error nameFC "import loop \{modns} → \{name'}" + processModule nameFC repo (modns :: stk) name' + pure $ name' + processModule nameFC repo (modns :: stk) primNS let imported = snoc imported primNS putStrLn "module \{modName}" @@ -107,6 +105,7 @@ processModule importFC repo stk modns = do top <- getTop let freshMC = MC emptyMap Nil 0 CheckAll + -- NOW Print and drop errors here -- set imported, mod, freshMC, ops before processing modifyTop [ imported := imported ; hints := emptyMap @@ -125,7 +124,7 @@ processModule importFC repo stk modns = do -- 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 importNames top.errors + let mod = MkModCtx src top.defs top.metaCtx top.ops imported top.errors let modules = updateMap modns mod top.modules modifyTop [modules := modules] @@ -134,11 +133,11 @@ processModule importFC repo stk modns = do -- FIXME module context should hold errors, to report in replay pure mod where - tryProcessDecl : String → List String → Decl → M Unit + tryProcessDecl : String → String → Decl → M Unit tryProcessDecl src ns decl = do (Left err) <- tryError $ processDecl ns decl | _ => pure MkUnit addError err --- TODO clear dependents too. -invalidateModule : List String -> M Unit +-- NOW TODO clear dependents too. +invalidateModule : String -> M Unit invalidateModule modname = modifyTop [modules $= deleteMap modname] diff --git a/src/Lib/ReplParser.newt b/src/Lib/ReplParser.newt index a07f63b..6d132d3 100644 --- a/src/Lib/ReplParser.newt +++ b/src/Lib/ReplParser.newt @@ -36,7 +36,8 @@ replQN = do ident <- uident rest <- many $ token Projection let name = joinBy "" (ident :: rest) - pure $ uncurry QN $ unsnoc $ split1 name "." + let (ns,nm) = unsnoc $ split1 name "." + pure $ QN (joinBy "." ns) nm data ArgType = ArgNone | ArgString | ArgIdent | ArgOptInt | ArgQName diff --git a/src/Lib/TCO.newt b/src/Lib/TCO.newt index a72135f..ea32ff8 100644 --- a/src/Lib/TCO.newt +++ b/src/Lib/TCO.newt @@ -65,7 +65,7 @@ rewriteTailCalls nms tm = case tm of -- the name of our trampoline bouncer : QName -bouncer = QN Nil "bouncer" +bouncer = QN "" "bouncer" doOptimize : List (QName × CExp) → M (List (QName × CExp)) doOptimize fns = do diff --git a/src/Lib/TopContext.newt b/src/Lib/TopContext.newt index 14bdd60..58b5df4 100644 --- a/src/Lib/TopContext.newt +++ b/src/Lib/TopContext.newt @@ -34,7 +34,7 @@ lookupRaw raw top = Just entry => Just entry Nothing => go top.imported where - go : List (List String) → Maybe TopEntry + go : List String → Maybe TopEntry go Nil = Nothing go (ns :: nss) = case lookupMap' ns top.modules of Nothing => go nss @@ -47,7 +47,7 @@ instance Show TopContext where show top = "\nContext:\n [\{ joinBy "\n" $ map (show ∘ snd) $ toList top.defs}]" emptyTop : TopContext -emptyTop = MkTop emptyMap Nil emptyMap Nil emptyMap (MC emptyMap Nil 0 CheckAll) 0 Nil emptyMap +emptyTop = MkTop emptyMap Nil emptyMap "" emptyMap (MC emptyMap Nil 0 CheckAll) 0 Nil emptyMap setFlag : QName → FC → EFlag → M Unit diff --git a/src/Lib/Types.newt b/src/Lib/Types.newt index c2d96f8..26fa98b 100644 --- a/src/Lib/Types.newt +++ b/src/Lib/Types.newt @@ -402,7 +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 (List String) + modDeps : List String modErrors : List Error -- Top level context. @@ -421,15 +421,13 @@ HintTable = SortedMap QName (List (QName × Tm)) record TopContext where constructor MkTop - -- maybe we use a String instead of List String for the left of QN - -- I'm putting a dummy entry in - modules : SortedMap (List String) ModContext - imported : List (List String) + modules : SortedMap String ModContext + imported : List String -- TCon name → function name × type hints : HintTable -- current module - ns : List String + ns : String defs : SortedMap QName TopEntry metaCtx : MetaContext diff --git a/src/Main.newt b/src/Main.newt index 1673ac9..424bd4e 100644 --- a/src/Main.newt +++ b/src/Main.newt @@ -95,9 +95,9 @@ processFile fn = do let modns = split modName "." base <- getBaseDir fn nameFC modns - invalidateModule modns + invalidateModule modName let repo = dirFileSource base - mod <- processModule emptyFC repo Nil modns + mod <- processModule emptyFC repo Nil modName top <- getTop showErrors fn mod.modSource @@ -122,7 +122,7 @@ cmdLine (fn :: args) = do browseTop : QName → M Unit browseTop qn@(QN ns x) = do top <- getTop - let ns = snoc ns x + let ns = ns ++ "." ++ x let (Just mod) = lookupMap' ns top.modules | _ => putStrLn "module \{show qn} not loaded" go $ listValues mod.modDefs