summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDougal <d.maclaurin@gmail.com>2023-12-13 21:01:30 -0500
committerDougal <d.maclaurin@gmail.com>2023-12-13 21:01:41 -0500
commit1a9bf82f0ebe84fdd7547dac55a1da6a3d5ea3ab (patch)
tree93732df6cf9eaf65b1488ae5db9ebdacced3daee
parentdaf6e824512407fdab7ad49d4a390e8544fc78fa (diff)
Add hover types for binders
-rw-r--r--src/lib/Inference.hs14
-rw-r--r--static/style.css4
2 files changed, 10 insertions, 8 deletions
diff --git a/src/lib/Inference.hs b/src/lib/Inference.hs
index 22038303..996eb16e 100644
--- a/src/lib/Inference.hs
+++ b/src/lib/Inference.hs
@@ -1298,8 +1298,9 @@ inferClassDef className methodNames paramBs methodTys = do
return $ ClassDef className builtinName methodNames paramNames roleExpls' paramBs''' superclassBs methodTys'
withUBinder :: UAnnBinder i i' -> InfererCPSB2 (WithExpl CBinder) i i' o a
-withUBinder (UAnnBinder expl b ann cs) cont = do
- ty <- inferAnn (getSrcId b) ann cs
+withUBinder (UAnnBinder expl (WithSrcB sid b) ann cs) cont = do
+ ty <- inferAnn sid ann cs
+ emitExprType sid ty
withFreshBinderInf (getNameHint b) expl ty \b' ->
extendSubst (b@>binderName b') $ cont (WithAttrB expl b')
@@ -1316,10 +1317,11 @@ inferUBinders
-> (forall o'. DExt o o' => [CAtomName o'] -> InfererM i' o' (e o'))
-> InfererM i o (Abs (Nest (WithExpl CBinder)) e o)
inferUBinders Empty cont = withDistinct $ Abs Empty <$> cont []
-inferUBinders (Nest (UAnnBinder expl b ann cs) bs) cont = do
+inferUBinders (Nest (UAnnBinder expl (WithSrcB sid b) ann cs) bs) cont = do
-- TODO: factor out the common part of each case (requires an annotated
-- `where` clause because of the rank-2 type)
- ty <- inferAnn (getSrcId b) ann cs
+ ty <- inferAnn sid ann cs
+ emitExprType sid ty
withFreshBinderInf (getNameHint b) expl ty \b' -> do
extendSubst (b@>binderName b') do
Abs bs' e <- inferUBinders bs \vs -> cont (sink (binderName b') : vs)
@@ -1393,7 +1395,7 @@ checkULamPartial partialPiTy sid lamExpr = do
Abs piBs' UnitE <- applyRename (piB@>binderName b) (EmptyAbs piBs)
checkLamBinders piExpls piBs' lamBs \bs -> cont (Nest b bs)
Explicit -> case lamBs of
- Nest (UAnnBinder _ lamB lamAnn _) lamBsRest -> do
+ Nest (UAnnBinder _ (WithSrcB bSid lamB) lamAnn _) lamBsRest -> emitExprType bSid piAnn >> do
case lamAnn of
UAnn lamAnn' -> checkUType lamAnn' >>= expectEq (getSrcId lamAnn') piAnn
UNoAnn -> return ()
@@ -1576,7 +1578,7 @@ bindLetPat
=> UPat i i' -> CAtomVar o
-> (forall o'. (Emits o', DExt o o') => InfererM i' o' (e o'))
-> InfererM i o (e o)
-bindLetPat (WithSrcB sid pat) v cont = case pat of
+bindLetPat (WithSrcB sid pat) v cont = emitExprType sid (getType v) >> case pat of
UPatBinder b -> getDistinct >>= \Distinct -> extendSubst (b @> atomVarName v) cont
UPatProd ps -> do
let n = nestLength ps
diff --git a/static/style.css b/static/style.css
index c61141ef..bceabfe6 100644
--- a/static/style.css
+++ b/static/style.css
@@ -21,7 +21,7 @@ body {
position: fixed;
top: 0em;
left: 0em;
- height: 90vh;
+ height: 85vh;
width: 32px;
overflow: hidden;
}
@@ -34,7 +34,7 @@ body {
}
#hover-info {
position: fixed;
- height: 10vh;
+ height: 15vh;
bottom: 0em;
width: 100vw;
overflow: hidden;