cleanup

src/Commands.newt

@@ -46,7 +46,8 @@ getHoverInfo repo modns row col = do
 
     -- Lookup the name
     let (Just e) = lookupRaw name top   | _ => pure Nothing
-    pure $ Just ("\{show e.name} : \{rpprint Nil e.type}", e.fc)
+    ty <- nf Nil e.type
+    pure $ Just ("\{show e.name} : \{rpprint Nil ty}", e.fc)
 
     where
         getTok : List BTok → Maybe String

src/LSP.newt

@@ -70,12 +70,7 @@ updateFile fn src = unsafePerformIO $ do
     st <- readIORef state
     modifyIORef state [ files $= updateMap fn src ]
     let st = the LSPState $ [ files $= updateMap fn src ] st
-    -- module relative to base
-
-    let (Right toks) = tokenise fn src | Left err => writeIORef state st
-    let (Right ((nameFC, modName), _, _)) = partialParse fn parseModHeader emptyMap toks
-        | Left (err,toks) => writeIORef state st
-
+    let (base,modName) = decomposeName fn
     Right (ctx,_) <- (invalidateModule modName).runM st.topContext
         | _ => writeIORef state st
     modifyIORef state [ topContext := ctx ]
@@ -209,6 +204,7 @@ checkFile fn = unsafePerformIO $ do
         pure $ infos ++ errors
         ).runM st.topContext
         | Left err => do
+            putStrLn "**** Error without updating top:"
             putStrLn $ showError "" err
             pure $ jsonToJObject $ JsonArray $ errorToDiag err :: Nil
     -- Cache loaded modules

src/Lib/CompileExp.newt

@@ -120,6 +120,7 @@ compileTerm t@(Ref fc nm@(QN _ tag)) = do
   defs <- getRef Defs
   case arity of
     Nil =>
+      -- Translate special constructors (Enum, Bool-like, Nat-like)
       case lookupMap' nm defs : Maybe Def of
         Just (DCon ix EnumCon _ _) => pure $ CLit $ LInt $ cast ix
         Just (DCon ix FalseCon _ _) => pure $ CLit $ LBool False
@@ -156,7 +157,8 @@ compileTerm tm@(App _ _ _) = case funArgs tm of
     applySucc : List CExp → M CExp
     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}"
+    applySucc _ = error (getFC tm) "overapplied Succ \{show tm}"
+
 compileTerm (UU _) = pure $ CRef (QN "" "U")
 compileTerm (Pi _ nm icit rig t u) = do
   t' <- compileTerm t
@@ -269,7 +271,7 @@ defToCExp (qn, 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
--- we need to sort out tag number if we do that
+-- we need to sort out tag number if we do typecase
 defToCExp (qn, TCon arity conNames) = pure (qn, compileDCon Z qn NormalCon (replicate' (cast arity) Many))
 defToCExp (qn, PrimTCon arity) = pure (qn, compileDCon Z qn NormalCon (replicate' (cast arity) Many))
 defToCExp (qn, PrimFn src _ deps) = pure (qn, CRaw src deps)

src/Lib/Elab.newt

@@ -659,13 +659,6 @@ insert ctx tm ty = do
       insert ctx (App (getFC tm) tm m) bapp
     va => pure (tm, va)
 
-primType : FC -> QName -> M Val
-primType fc nm = do
-  top <- getTop
-  case lookup nm top of
-      Just (MkEntry _ name ty (PrimTCon _) _) => pure $ VRef fc name Lin
-      _ => error fc "Primitive type \{show nm} not in scope"
-
 data Bind = MkBind String Icit Val
 
 instance Show Bind where
@@ -1625,14 +1618,8 @@ infer ctx (RImplicit fc) = do
   tm <- freshMeta ctx fc vty Normal
   pure (tm, vty)
 
-infer ctx (RLit fc (LString str)) = do
-  ty <- primType fc stringType
-  pure (Lit fc (LString str), ty)
-infer ctx (RLit fc (LInt i)) = do
-  ty <- primType fc intType
-  pure (Lit fc (LInt i), ty)
-infer ctx (RLit fc (LChar c)) = do
-  ty <- primType fc charType
-  pure (Lit fc (LChar c), ty)
+infer ctx (RLit fc (LString str)) = pure (Lit fc (LString str), VRef fc stringType Lin)
+infer ctx (RLit fc (LInt i)) = pure (Lit fc (LInt i), VRef fc intType Lin)
+infer ctx (RLit fc (LChar c)) = pure (Lit fc (LChar c), VRef fc charType Lin)
 infer ctx (RAs fc _ _) = error fc "@ can only be used in patterns"
 infer ctx tm = error (getFC tm) "Implement infer \{show tm}"

src/Lib/Erasure.newt

@@ -18,6 +18,7 @@ getType : Tm -> M (Maybe Tm)
 getType (Ref fc nm) = do
   top <- getTop
   case lookup nm top of
+    -- Should not nappen.
     Nothing => error fc "\{show nm} not in scope"
     (Just (MkEntry _ name type def _)) => pure $ Just type
 getType tm = pure Nothing

src/Lib/ProcessModule.newt

@@ -122,15 +122,15 @@ processModule importFC repo stk modns = do
   log 1 $ \ _ => "process Decls"
   traverse (tryProcessDecl src modns) (collectDecl decls)
 
+  -- This has addErrors as a side-effect
+  logMetas $ reverse $ listValues top.metaCtx.metas
+
   -- 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
   modifyTop [modules := modules]
 
-  logMetas $ reverse $ listValues top.metaCtx.metas
   -- FIXME module context should hold errors, to report in replay
   pure mod
   where