web: fancier popups (#449)

Show a preview of definitions when hovering over them

src/Borceux.lagda.md

@@ -1116,3 +1116,5 @@ _ = const-nato
 * Exercise 8.4.6:
   * (⇒) `dependent-product→lcc`{.Agda}
   * (⇐) `lcc→dependent-product`{.Agda}
+
+[[marked graph homomorphism]]

support/shake/app/Definitions.hs

@@ -113,7 +113,7 @@ newtype LinkTargetQ     = LinkTargetQ Text
 
 type instance RuleResult GlossaryQ       = Glossary
 type instance RuleResult ModuleGlossaryQ = Glossary
-type instance RuleResult LinkTargetQ     = Text
+type instance RuleResult LinkTargetQ     = (Text, Text)
 
 addDefinition :: Mangled -> Definition -> Glossary -> Glossary
 addDefinition _ Definition{definitionCopy = True} ge = ge
@@ -154,7 +154,7 @@ glossaryRules = do
   _ <- addOracle \(LinkTargetQ target) -> do
     glo <- getEntries <$> askOracle GlossaryQ
     case Map.lookup (mangleLink target) glo of
-      Just def -> pure $ definitionTarget def
+      Just def -> pure (definitionAnchor def, definitionTarget def)
       Nothing  -> error $
         "Unknown wiki-link target: " ++ Text.unpack target
 
@@ -203,10 +203,10 @@ isWikiLink (Link attr contents (url, title))
   | "wikilink" == title = pure $ WikiLink url contents attr
 isWikiLink _ = Nothing
 
-getWikiLinkUrl :: Text -> Action Text
+getWikiLinkUrl :: Text -> Action (Text, Text)
 getWikiLinkUrl = askOracle . LinkTargetQ
 
 getWikiLink :: WikiLink -> Action Inline
-getWikiLink (WikiLink dest contents attr) = do
-  url <- getWikiLinkUrl dest
-  pure $ Link attr contents (url, "")
+getWikiLink (WikiLink dest contents (id, cls, kv)) = do
+  (anchor, url) <- getWikiLinkUrl dest
+  pure $ Link (id, cls, ("data-target", anchor):kv) contents (url, "")

support/shake/app/HTML/Backend.hs

@@ -1,7 +1,9 @@
 -- Copyright (c) 2005-2021 remains with the Agda authors. See /support/shake/LICENSE.agda
 
 -- | Backend for generating highlighted, hyperlinked HTML from Agda sources.
-{-# LANGUAGE FlexibleContexts, BlockArguments, LambdaCase, DerivingStrategies, OverloadedStrings #-}
+{-# LANGUAGE FlexibleContexts, BlockArguments, LambdaCase, DerivingStrategies, OverloadedStrings, NondecreasingIndentation #-}
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE TypeFamilies #-}
 module HTML.Backend
   ( htmlBackend
   , compileOneModule
@@ -14,56 +16,77 @@ import HTML.Base
 import Prelude hiding ((!!), concatMap)
 import Control.Monad.Identity
 import Control.Monad.Except
+import Control.Monad.Reader
 
 import qualified Data.HashMap.Strict as Hm
 import qualified Data.Map.Strict as Map
 import qualified Data.HashSet as HashSet
 import qualified Data.Text as Text
+import qualified Data.Set as Set
+
 import Data.HashMap.Strict (HashMap)
 import Data.List.NonEmpty (NonEmpty((:|)))
 import Data.Map.Strict (Map)
 import Data.Foldable
 import Data.HashSet (HashSet)
 import Data.Aeson
+import Data.Maybe
 import Data.IORef
 import Data.Text (Text)
 import Data.List
+import Data.Set (Set)
 
-import Agda.Compiler.Backend
+import Agda.Compiler.Backend hiding (topLevelModuleName)
 import Agda.Compiler.Common
 
+import Control.DeepSeq
+
 import qualified Agda.Syntax.Concrete.Generic as Con
 import qualified Agda.Syntax.Internal.Generic as I
 import qualified Agda.Syntax.Abstract.Views as A
+import qualified Agda.Syntax.Common.Aspect as Asp
+import qualified Agda.Syntax.Scope.Base as Scope
+import qualified Agda.Syntax.Concrete as Con
 import qualified Agda.Syntax.Internal as I
 import qualified Agda.Syntax.Abstract as A
-import qualified Agda.Syntax.Concrete as Con
-import qualified Agda.Syntax.Scope.Base as Scope
+import qualified Agda.Syntax.Concrete as C
 
 import Agda.Syntax.Translation.InternalToAbstract ( Reify(reify) )
-import Agda.Syntax.Translation.AbstractToConcrete (abstractToConcrete_)
+import Agda.Syntax.Translation.AbstractToConcrete (abstractToConcrete_, abstractToConcreteCtx)
 import Agda.Syntax.TopLevelModuleName
+import Agda.Syntax.Abstract.Pretty (prettyA, prettyATop)
 import Agda.Syntax.Abstract.Views
 import Agda.Syntax.Common.Pretty
+import Agda.Syntax.Scope.Monad (modifyCurrentScope, getCurrentModule, freshConcreteName)
 import Agda.Syntax.Abstract hiding (Type)
 import Agda.Syntax.Position
 import Agda.Syntax.Internal (Type, domName)
+import Agda.Syntax.Fixity (Precedence(TopCtx))
 import Agda.Syntax.Common
 import Agda.Syntax.Info
 
+import qualified Agda.TypeChecking.Monad.Base as I
+import qualified Agda.TypeChecking.Pretty as P
+import Agda.TypeChecking.Substitute
+import Agda.TypeChecking.Telescope
+import Agda.TypeChecking.Records (isRecord)
 import Agda.TypeChecking.Reduce (instantiateFull, reduceDefCopyTCM, normalise)
+import Agda.TypeChecking.Level (reallyUnLevelView)
 
+import qualified Agda.Utils.Maybe.Strict as S
 import Agda.Utils.FileName
+import Agda.Utils.Lens
+import Agda.Utils.Size
 
 import System.FilePath hiding (normalise)
-import Debug.Trace
-import qualified Agda.Utils.Maybe.Strict as S
-import Agda.Syntax.Scope.Monad (modifyCurrentScope)
-import Agda.Syntax.Abstract.Pretty (prettyA)
-import Agda.TypeChecking.Records (isRecord)
-import Data.Set (Set)
-import qualified Data.Set as Set
-import Agda.TypeChecking.Level (reallyUnLevelView)
+
+import Text.Show.Pretty (ppShow)
+
+import HTML.Render
+import Debug.Trace (traceShow)
+import Agda.Syntax.Internal.Names (namesIn')
+import Agda.Interaction.Response (Response_boot(Resp_RunningInfo))
+import Agda.Interaction.Options.Lenses (LensVerbosity(setVerbosity))
 
 data HtmlCompileEnv = HtmlCompileEnv
   { htmlCompileEnvOpts     :: HtmlOptions
@@ -163,12 +186,13 @@ compileDefHtml env _ _ _
 compileDefHtml env _menv _isMain def = withCurrentModule (qnameModule (defName def)) $
   case definitionAnchor env def of
     Just mn -> do
-      ty <- typeToText def
+      (tooltip, ty) <- typeToText def
       let
         ident = Identifier
-          { idAnchor = mn
-          , idIdent  = Text.pack (render (pretty (qnameName (defName def))))
-          , idType   = ty
+          { idAnchor  = mn
+          , idIdent   = Text.pack (render (pretty (qnameName (defName def))))
+          , idType    = ty
+          , idTooltip = tooltip
           }
       pure (Just (mn, ident))
     Nothing -> do
@@ -196,6 +220,7 @@ postModuleHtml env menv _isMain _modName _defs = do
       . htmlCompileEnvOpts
       . htmlModEnvCompileEnv
       $ menv
+
   htmlSrc <- srcFileOfInterface (htmlModEnvName menv) <$> curIF
   runLogHtmlWithMonadDebug $ generatePage htmlSrc
   pure $ HtmlModule $ foldr ins mempty _defs
@@ -233,23 +258,6 @@ compileOneModule _pn opts types iface = do
     compDef env menv def = setCurrentRange (defName def) $
       compileDefHtml env menv NotMain def
 
-killQual :: Con.Expr -> Con.Expr
-killQual = Con.mapExpr (wrap . forget) where
-  work :: Con.QName -> Con.QName
-  work (Con.Qual _ x) = work x
-  work x = x
-
-  forget :: Con.Expr -> Con.Expr
-  forget (Con.KnownOpApp r w qual names args) = Con.OpApp w qual names args
-  forget (Con.KnownIdent r nm) = Con.Ident nm
-  forget x = x
-
-  wrap :: Con.Expr -> Con.Expr
-  wrap (Con.Ident v)                 = Con.Ident (work v)
-  wrap (Con.KnownIdent v w)          = Con.KnownIdent v (work w)
-  wrap (Con.OpApp v qual names args) = Con.OpApp v (work qual) names args
-  wrap x = x
-
 getClass :: QName -> TCM (Set QName)
 getClass q = isRecord q >>= \case
   Just RecordData{ _recFields = f } -> pure $! Set.fromList (map I.unDom f)
@@ -264,43 +272,96 @@ usedInstances = I.foldTerm \case
       Nothing -> pure mempty
   _ -> pure mempty
 
-typeToText :: Definition -> TCM Text
+typeToText :: Definition -> TCM (Text, Text)
 typeToText d = do
   ui <- usedInstances (I.unEl (defType d))
+  fv <- getDefFreeVars (defName d)
+
   ty <- locallyReduceDefs (OnlyReduceDefs ui) $ normalise (defType d)
-  expr <- runNoCopy (reify ty)
-  fmap (Text.pack . render . pretty . killQual) .
-    abstractToConcrete_ . removeImpls $ expr
+
+  topm <- topLevelModuleName (qnameModule (defName d))
+
+  let
+    n k = Asp.Name (Just k) False
+    asp = \case
+      I.Axiom{}          -> n Asp.Postulate
+      DataOrRecSig{}     -> n Asp.Datatype
+      GeneralizableVar{} -> n Asp.Generalizable
+      AbstractDefn d     -> asp d
+      d@Function{}
+        | isProperProjection d -> n Asp.Field
+        | otherwise -> n Asp.Function
+      Datatype{}         -> n Asp.Datatype
+      Record{}           -> n Asp.Record{}
+      Constructor{conSrcCon = c} ->
+        n $ Asp.Constructor (I.conInductive c)
+      I.Primitive{} -> n Asp.Primitive
+      PrimitiveSort{} -> Asp.PrimitiveType
+
+    aspect = asp (theDef d)
+
+    a = Asp.Aspects
+      { Asp.aspect         = Just aspect
+      , Asp.otherAspects   = mempty
+      , Asp.note           = ""
+      , Asp.definitionSite = toDefinitionSite topm (nameBindingSite (qnameName (defName d)))
+      , Asp.tokenBased     = Asp.TokenBased
+      }
+
+  expr <- removeImpls <$> reify ty
+
+  here <- currentTopLevelModule
+  tooltip <- fmap renderToHtml $ P.vcat
+    [ annotate a <$> P.pretty (qnameName (defName d))
+    , P.nest 2 (P.colon P.<+> prettyATop expr)
+    ]
+  plain <- Text.pack . render <$> prettyATop expr
+  pure (tooltip, plain)
+
+toDefinitionSite :: TopLevelModuleName -> Range -> Maybe Asp.DefinitionSite
+toDefinitionSite topm r = do
+  p <- fmap (fromIntegral . posPos) . rStart $ r
+  pure $ Asp.DefinitionSite
+    { Asp.defSiteModule = topm
+    , Asp.defSitePos    = fromIntegral p
+    , Asp.defSiteHere   = True
+    , Asp.defSiteAnchor = Nothing
+    }
+
+killQual :: Con.Expr -> Con.Expr
+killQual = Con.mapExpr wrap where
+  work :: Con.QName -> Con.QName
+  work (Con.Qual _ x) = work x
+  work x = x
+
+  wrap :: Con.Expr -> Con.Expr
+  wrap (Con.Ident v)                 = Con.Ident (work v)
+  wrap (Con.KnownIdent v w)          = Con.KnownIdent v (work w)
+  wrap (Con.KnownOpApp v a b c d)    = Con.KnownOpApp v a (work b) c d
+  wrap (Con.OpApp v qual names args) = Con.OpApp v (work qual) names args
+  wrap x = x
 
 removeImpls :: A.Expr -> A.Expr
 removeImpls (A.Pi _ (x :| xs) e) =
-  makePi (map (A.mapExpr removeImpls) $ filter ((/= Hidden) . getHiding) (x:xs)) (removeImpls e)
+  let
+    fixup :: TypedBinding -> TypedBinding
+    fixup q@(TBind rng inf as _)
+      | Hidden <- getHiding q = TBind rng inf as underscore
+      | otherwise = q
+  in makePi (map (A.mapExpr removeImpls) $ map fixup (x:xs)) (removeImpls e)
 removeImpls (A.Fun span arg ret) =
   A.Fun span (removeImpls <$> arg) (removeImpls ret)
 removeImpls e = e
 
 makePi :: [A.TypedBinding] -> A.Expr -> A.Expr
-makePi [] = id
-makePi (b:bs) = A.Pi exprNoRange (b :| bs)
-
-newtype NoCopy a = NoCopy { runNoCopy :: TCM a }
-  deriving newtype (Functor, Applicative, Monad, MonadFail)
-  deriving newtype
-    ( HasBuiltins, MonadDebug, MonadReduce, HasOptions, MonadTCEnv
-    , ReadTCState, MonadAddContext, MonadInteractionPoints
-    , MonadFresh NameId
-    )
-
-noCopyOp :: Definition -> Definition
-noCopyOp def | defCopy def, Con.numHoles (defName def) >= 1 = traceShow (pretty (defName def)) $ def{defCopy = False}
-noCopyOp def = def
-
-instance HasConstInfo NoCopy where
-  getConstInfo = NoCopy . fmap noCopyOp . getConstInfo
-  getConstInfo' = NoCopy . fmap (fmap noCopyOp) . getConstInfo'
-  getRewriteRulesFor = NoCopy . getRewriteRulesFor
-
-instance PureTCM NoCopy
+makePi [] e = e
+makePi (b:bs) (A.Pi _ bs' e') = makePi (b:bs ++ toList bs') e'
+makePi (b:bs) e = A.Pi exprNoRange (b `mergeTBinds` bs) e
+
+mergeTBinds :: A.TypedBinding -> [A.TypedBinding] -> NonEmpty A.TypedBinding
+mergeTBinds (A.TBind r i as Underscore{}) (A.TBind _ _ as' Underscore{}:bs) =
+  mergeTBinds (A.TBind r i (as <> as') underscore) bs
+mergeTBinds x xs = x :| xs
 
 definitionAnchor :: HtmlCompileEnv -> Definition -> Maybe Text
 definitionAnchor _ def | defCopy def = Nothing