Show types of local vars and subexpressions on hover

src/lib/Inference.hs

@@ -155,7 +155,7 @@ data InfState (n::S) = InfState
   , infEffects     :: EffectRow CoreIR n }
 
 newtype InfererM (i::S) (o::S) (a:: *) = InfererM
-  { runInfererM' :: SubstReaderT Name (ReaderT1 InfState (BuilderT CoreIR (ExceptT (State TypeInfo)))) i o a }
+  { runInfererM' :: SubstReaderT Name (ReaderT1 InfState (BuilderT CoreIR (ExceptT (State TypingInfo)))) i o a }
   deriving (Functor, Applicative, Monad, MonadFail, Alternative, Builder CoreIR,
             EnvExtender, ScopableBuilder CoreIR,
             ScopeReader, EnvReader, Fallible, Catchable, SubstReader Name)
@@ -166,11 +166,11 @@ type InfererCPSB2 b i i' o a = (forall o'. DExt o o' => b o o' -> InfererM i' o'
 liftInfererM :: (EnvReader m, TopLogger1 m, Fallible1 m) => InfererM n n a -> m n a
 liftInfererM cont = do
   (ansExcept, typeInfo) <- liftInfererMPure cont
-  emitLog $ Outputs [SourceInfo $ SITypeInfo typeInfo]
+  emitLog $ Outputs [SourceInfo $ SITypingInfo typeInfo]
   liftExcept ansExcept
 {-# INLINE liftInfererM #-}
 
-liftInfererMPure :: EnvReader m => InfererM n n a -> m n (Except a, TypeInfo)
+liftInfererMPure :: EnvReader m => InfererM n n a -> m n (Except a, TypingInfo)
 liftInfererMPure cont = do
   ansM <- liftBuilderT $ runReaderT1 emptyInfState $ runSubstReaderT idSubst $ runInfererM' cont
   return $ runState (runExceptT ansM) mempty
@@ -347,8 +347,18 @@ withAllowedEffects :: EffectRow CoreIR o -> InfererM i o a -> InfererM i o a
 withAllowedEffects effs cont = withInfState (\(InfState g _) -> InfState g effs) cont
 {-# INLINE withAllowedEffects #-}
 
-emitTypeInfo :: SrcId -> String -> InfererM i o ()
-emitTypeInfo _ _ = return ()
+getTypeAndEmit :: HasType CoreIR e => SrcId -> e o -> InfererM i o (e o)
+getTypeAndEmit sid e = do
+  emitExprType sid (getType e)
+  return e
+
+emitExprType :: SrcId -> CType any -> InfererM i o ()
+emitExprType sid ty = emitTypeInfo sid $ ExprType $ pprint ty
+
+emitTypeInfo :: SrcId -> TypeInfo -> InfererM i o ()
+emitTypeInfo sid tyInfo =
+  InfererM $ liftSubstReaderT $ lift11 $ lift1 $ lift $
+    modify (<> TypingInfo (M.singleton sid tyInfo))
 
 withReducibleEmissions
   :: (HasNamesE e, SubstE AtomSubstVal e, ToErr err)
@@ -417,7 +427,7 @@ etaExpandPartialPi (PartialPiType appExpl expls bs effs reqTy) cont = do
 
 -- Doesn't introduce implicit pi binders or dependent pairs
 topDownExplicit :: forall i o. Emits o => CType o -> UExpr i -> InfererM i o (CAtom o)
-topDownExplicit reqTy exprWithSrc@(WithSrcE sid expr) = case expr of
+topDownExplicit reqTy exprWithSrc@(WithSrcE sid expr) = emitExprType sid reqTy >> case expr of
   ULam lamExpr -> case reqTy of
     TyCon (Pi piTy) -> toAtom <$> Lam <$> checkULam sid lamExpr piTy
     _       -> throw sid $ UnexpectedTerm "lambda" (pprint reqTy)
@@ -477,11 +487,10 @@ bottomUp expr = bottomUpExplicit expr >>= instantiateSigma (getSrcId expr) Infer
 
 -- Doesn't instantiate implicit args
 bottomUpExplicit :: Emits o => UExpr i -> InfererM i o (SigmaAtom o)
-bottomUpExplicit (WithSrcE sid expr) = case expr of
+bottomUpExplicit (WithSrcE sid expr) = getTypeAndEmit sid =<< case expr of
   UVar ~(InternalName _ sn v) ->  do
     v' <- renameM v
     ty <- getUVarType v'
-    emitTypeInfo sid $ pprint sn ++ " : " ++ pprint ty
     return $ SigmaUVar sn ty v'
   ULit l -> return $ SigmaAtom Nothing $ Con $ Lit l
   UFieldAccess x (WithSrc _ field) -> do

src/lib/RenderHtml.hs

@@ -92,8 +92,8 @@ data TreeNodeState  = TreeNodeState
   deriving (Show, Eq, Generic)
 
 data TreeNodeUpdate = TreeNodeUpdate
-  { tnuHighlights :: Overwrite [RenderedHighlight]
-  , tnuText       :: Overwrite String }
+  { tnuHighlights :: [RenderedHighlight]
+  , tnuText       :: [String] }
     deriving (Show, Eq, Generic)
 
 renderOutputs :: Outputs -> RenderedOutputs
@@ -106,7 +106,7 @@ renderOutput = \case
   SourceInfo s   -> case s of
     SIGroupingInfo  info -> renderGroupingInfo  info
     SINamingInfo    info -> renderNamingInfo    info
-    SITypeInfo      info -> renderTypeInfo      info
+    SITypingInfo    info -> renderTypingInfo      info
   PassResult n s -> pure $ RenderedPassResult n s
   MiscLog s      -> pure $ RenderedMiscLog s
   Error e        -> pure $ RenderedError (getErrSrcId e) (pprint e)
@@ -161,13 +161,20 @@ renderNamingInfo (NamingInfo m) = [RenderedTreeNodeUpdate treeNodeUpdate]
 
 renderNameInfo :: NameInfo -> TreeNodeUpdate
 renderNameInfo = \case
-  LocalOcc _ -> TreeNodeUpdate NoChange (OverwriteWith "Local name")
+  LocalOcc _ -> TreeNodeUpdate [] ["Local name"]
   LocalBinder _ -> TreeNodeUpdate mempty mempty
-  TopOcc s -> TreeNodeUpdate NoChange (OverwriteWith s)
+  TopOcc s -> TreeNodeUpdate [] [s]
 
-renderTypeInfo :: TypeInfo -> RenderedOutputs
-renderTypeInfo _ = mempty
+renderTypingInfo :: TypingInfo -> RenderedOutputs
+renderTypingInfo (TypingInfo m) = [RenderedTreeNodeUpdate treeNodeUpdate]
+  where
+    treeNodeUpdate = M.toList m <&> \(sid, node) ->
+      (sid, Update $ renderTypeInfo node)
 
+renderTypeInfo :: TypeInfo -> TreeNodeUpdate
+renderTypeInfo = \case
+  ExprType s -> TreeNodeUpdate mempty ["Type:   " <> s]
+  _ -> TreeNodeUpdate mempty mempty
 
 instance ToJSON RenderedSourceBlock
 instance ToJSON RenderedOutput

src/lib/Types/Source.hs

@@ -100,7 +100,7 @@ instance Monoid LexemeInfo where
 data SourceInfo =
    SIGroupingInfo  GroupingInfo
  | SINamingInfo    NamingInfo
- | SITypeInfo      TypeInfo
+ | SITypingInfo    TypingInfo
    deriving (Show, Eq, Generic)
 
 newtype GroupingInfo = GroupingInfo (M.Map SrcId GroupTreeNode)
@@ -120,11 +120,11 @@ data NameInfo =
  | TopOcc String
  deriving (Show, Eq, Generic)
 
-newtype TypeInfo = TypeInfo (M.Map SrcId TypeInfo)
+newtype TypingInfo = TypingInfo (M.Map SrcId TypeInfo)
         deriving (Show, Eq, Semigroup, Monoid, Generic)
 type TypeStr = String
 type ExprStr = String
-data NodeTypeInfo =
+data TypeInfo =
    ExprType TypeStr      -- type of arbitrary expression
  | BinderType TypeStr
  | AppType

static/index.ts

@@ -64,8 +64,8 @@ type HsTreeNodeState = {
     tnHighlights  : Highlight[]
     tnText        : HTMLString}
 type HsTreeNodeUpdate = {
-    tnuHighlights : HsOverwrite<Highlight[]>;
-    tnuText       : HsOverwrite<HTMLString>}
+    tnuHighlights : Highlight[];
+    tnuText       : HTMLString[]}
 type HsTreeNodeMapUpdate =
     {tag: "Create" ; contents: HsTreeNodeState}  |
     {tag: "Replace"; contents: HsTreeNodeState}  |
@@ -283,14 +283,9 @@ function applyTreeNodeUpdate(cell:Cell, srcId:SrcId, update:HsTreeNodeMapUpdate)
             break
         case "Update":
             const nodeUpdate : HsTreeNodeUpdate = update.contents
-            const curTreeNode : TreeNode = cell.treeMap.get(srcId) ?? oops()
-            const text = nodeUpdate.tnuText
-            if (text.tag == "OverwriteWith") {
-                curTreeNode.text = text.contents}
-            const hl = nodeUpdate.tnuHighlights
-            if (hl.tag == "OverwriteWith") {
-                curTreeNode.highlights = hl.contents}
-            break}
+            const node : TreeNode = cell.treeMap.get(srcId) ?? oops()
+            nodeUpdate.tnuText.forEach(      (t) => {node.text       = node.text.concat(t, "\n")})
+            nodeUpdate.tnuHighlights.forEach((h) => {node.highlights = node.highlights.concat(h)})}
 }
 function computeRange(cell:Cell, l:SrcId, r:SrcId) : [Div, Div] | null {
     const lDiv = selectSpan(cell, l)