{-# LANGUAGE OverloadedStrings #-}

-- |
-- SPDX-License-Identifier: BSD-3-Clause
module Swarm.Language.LSP.Hover (
  showHoverInfo,

  -- * Documentation rendering
  renderDoc,
  treeToMarkdown,

  -- * Finding source location
  narrowToPosition,

  -- * Explaining source position
  explain,
) where

import Control.Applicative ((<|>))
import Control.Lens ((^.))
import Control.Monad (guard, void)
import Data.Foldable (asum)
import Data.Graph
import Data.List.NonEmpty (NonEmpty (..))
import Data.Map qualified as M
import Data.Maybe (catMaybes, fromMaybe)
import Data.Text (Text)
import Data.Text qualified as T
import Data.Text.Utf16.Rope qualified as R
import Language.LSP.Types qualified as J
import Language.LSP.VFS
import Swarm.Language.Context as Ctx
import Swarm.Language.Module (Module (..))
import Swarm.Language.Parse (readTerm', unTuple)
import Swarm.Language.Pipeline (ProcessedTerm (..), processParsedTerm)
import Swarm.Language.Pretty (prettyText)
import Swarm.Language.Syntax
import Swarm.Language.Typecheck (inferConst)
import Swarm.Language.Types
import Swarm.Util qualified as U

withinBound :: Int -> SrcLoc -> Bool
withinBound :: Int -> SrcLoc -> Bool
withinBound Int
pos (SrcLoc Int
s Int
e) = Int
pos forall a. Ord a => a -> a -> Bool
>= Int
s Bool -> Bool -> Bool
&& Int
pos forall a. Ord a => a -> a -> Bool
< Int
e
withinBound Int
_ SrcLoc
NoLoc = Bool
False

ropeToLspPosition :: R.Position -> J.Position
ropeToLspPosition :: Position -> Position
ropeToLspPosition (R.Position Word
l Word
c) =
  UInt -> UInt -> Position
J.Position (forall a b. (Integral a, Num b) => a -> b
fromIntegral Word
l) (forall a b. (Integral a, Num b) => a -> b
fromIntegral Word
c)

lspToRopePosition :: J.Position -> R.Position
lspToRopePosition :: Position -> Position
lspToRopePosition (J.Position UInt
myLine UInt
myCol) =
  Word -> Word -> Position
R.Position (forall a b. (Integral a, Num b) => a -> b
fromIntegral UInt
myLine) (forall a b. (Integral a, Num b) => a -> b
fromIntegral UInt
myCol)

showHoverInfo ::
  J.NormalizedUri ->
  J.TextDocumentVersion ->
  J.Position ->
  VirtualFile ->
  Maybe (Text, Maybe J.Range)
showHoverInfo :: NormalizedUri
-> TextDocumentVersion
-> Position
-> VirtualFile
-> Maybe (Text, Maybe Range)
showHoverInfo NormalizedUri
_ TextDocumentVersion
_ Position
p vf :: VirtualFile
vf@(VirtualFile Int32
_ Int
_ Rope
myRope) =
  case Text -> Either ParserError (Maybe Syntax)
readTerm' Text
content of
    Left ParserError
_ -> forall a. Maybe a
Nothing
    Right Maybe Syntax
Nothing -> forall a. Maybe a
Nothing
    Right (Just Syntax
stx) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ case Syntax -> Either ContextualTypeErr ProcessedTerm
processParsedTerm Syntax
stx of
      Left ContextualTypeErr
_e ->
        let found :: Syntax
found@(Syntax SrcLoc
foundSloc Term
_) = forall ty. ExplainableType ty => Syntax' ty -> Int -> Syntax' ty
narrowToPosition Syntax
stx forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral Word
absolutePos
            finalPos :: Maybe Range
finalPos = Rope -> SrcLoc -> Maybe Range
posToRange Rope
myRope SrcLoc
foundSloc
         in (,Maybe Range
finalPos) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Tree Text -> Text
treeToMarkdown Int
0 forall a b. (a -> b) -> a -> b
$ forall ty. ExplainableType ty => Syntax' ty -> Tree Text
explain Syntax
found
      Right (ProcessedTerm TModule
modul Requirements
_req ReqCtx
_reqCtx) ->
        let found :: Syntax' Polytype
found@(Syntax' SrcLoc
foundSloc Term' Polytype
_ Polytype
_) = forall ty. ExplainableType ty => Syntax' ty -> Int -> Syntax' ty
narrowToPosition (forall s t. Module s t -> Syntax' s
moduleAST TModule
modul) forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral Word
absolutePos
            finalPos :: Maybe Range
finalPos = Rope -> SrcLoc -> Maybe Range
posToRange Rope
myRope SrcLoc
foundSloc
         in (,Maybe Range
finalPos) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Tree Text -> Text
treeToMarkdown Int
0 forall a b. (a -> b) -> a -> b
$ forall ty. ExplainableType ty => Syntax' ty -> Tree Text
explain Syntax' Polytype
found
 where
  content :: Text
content = VirtualFile -> Text
virtualFileText VirtualFile
vf
  absolutePos :: Word
absolutePos =
    forall b a. b -> (a -> b) -> Maybe a -> b
maybe Word
0 (Rope -> Word
R.length forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$
      Position -> Rope -> Maybe (Rope, Rope)
R.splitAtPosition (Position -> Position
lspToRopePosition Position
p) Rope
myRope

posToRange :: R.Rope -> SrcLoc -> Maybe J.Range
posToRange :: Rope -> SrcLoc -> Maybe Range
posToRange Rope
myRope SrcLoc
foundSloc = do
  (Int
s, Int
e) <- case SrcLoc
foundSloc of
    SrcLoc Int
s Int
e -> forall a. a -> Maybe a
Just (Int
s, Int
e)
    SrcLoc
_ -> forall a. Maybe a
Nothing
  (Rope
startRope, Rope
_) <- Word -> Rope -> Maybe (Rope, Rope)
R.splitAt (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
s) Rope
myRope
  (Rope
endRope, Rope
_) <- Word -> Rope -> Maybe (Rope, Rope)
R.splitAt (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
e) Rope
myRope
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    Position -> Position -> Range
J.Range
      (Position -> Position
ropeToLspPosition forall a b. (a -> b) -> a -> b
$ Rope -> Position
R.lengthAsPosition Rope
startRope)
      (Position -> Position
ropeToLspPosition forall a b. (a -> b) -> a -> b
$ Rope -> Position
R.lengthAsPosition Rope
endRope)

descend ::
  ExplainableType ty =>
  -- | position
  Int ->
  -- | next element to inspect
  Syntax' ty ->
  Maybe (Syntax' ty)
descend :: forall ty.
ExplainableType ty =>
Int -> Syntax' ty -> Maybe (Syntax' ty)
descend Int
pos s1 :: Syntax' ty
s1@(Syntax' SrcLoc
l1 Term' ty
_ ty
_) = do
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Int -> SrcLoc -> Bool
withinBound Int
pos SrcLoc
l1
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. ExplainableType ty => Syntax' ty -> Int -> Syntax' ty
narrowToPosition Syntax' ty
s1 Int
pos

-- | Find the most specific term for a given
-- position within the code.
narrowToPosition ::
  ExplainableType ty =>
  -- | parent term
  Syntax' ty ->
  -- | absolute offset within the file
  Int ->
  Syntax' ty
narrowToPosition :: forall ty. ExplainableType ty => Syntax' ty -> Int -> Syntax' ty
narrowToPosition s0 :: Syntax' ty
s0@(Syntax' SrcLoc
_ Term' ty
t ty
ty) Int
pos = forall a. a -> Maybe a -> a
fromMaybe Syntax' ty
s0 forall a b. (a -> b) -> a -> b
$ case Term' ty
t of
  SLam LocVar
lv Maybe Type
_ Syntax' ty
s -> Syntax' ty -> Maybe (Syntax' ty)
d (forall ty. LocVar -> ty -> Syntax' ty
locVarToSyntax' LocVar
lv forall a b. (a -> b) -> a -> b
$ forall t. ExplainableType t => t -> t
getInnerType ty
ty) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Syntax' ty -> Maybe (Syntax' ty)
d Syntax' ty
s
  SApp Syntax' ty
s1 Syntax' ty
s2 -> Syntax' ty -> Maybe (Syntax' ty)
d Syntax' ty
s1 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Syntax' ty -> Maybe (Syntax' ty)
d Syntax' ty
s2
  SLet Bool
_ LocVar
lv Maybe Polytype
_ s1 :: Syntax' ty
s1@(Syntax' SrcLoc
_ Term' ty
_ ty
lty) Syntax' ty
s2 -> Syntax' ty -> Maybe (Syntax' ty)
d (forall ty. LocVar -> ty -> Syntax' ty
locVarToSyntax' LocVar
lv ty
lty) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Syntax' ty -> Maybe (Syntax' ty)
d Syntax' ty
s1 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Syntax' ty -> Maybe (Syntax' ty)
d Syntax' ty
s2
  SDef Bool
_ LocVar
lv Maybe Polytype
_ s :: Syntax' ty
s@(Syntax' SrcLoc
_ Term' ty
_ ty
lty) -> Syntax' ty -> Maybe (Syntax' ty)
d (forall ty. LocVar -> ty -> Syntax' ty
locVarToSyntax' LocVar
lv ty
lty) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Syntax' ty -> Maybe (Syntax' ty)
d Syntax' ty
s
  SBind Maybe LocVar
mlv s1 :: Syntax' ty
s1@(Syntax' SrcLoc
_ Term' ty
_ ty
lty) Syntax' ty
s2 -> (Maybe LocVar
mlv forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Syntax' ty -> Maybe (Syntax' ty)
d forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall ty. LocVar -> ty -> Syntax' ty
locVarToSyntax' (forall t. ExplainableType t => t -> t
getInnerType ty
lty)) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Syntax' ty -> Maybe (Syntax' ty)
d Syntax' ty
s1 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Syntax' ty -> Maybe (Syntax' ty)
d Syntax' ty
s2
  SPair Syntax' ty
s1 Syntax' ty
s2 -> Syntax' ty -> Maybe (Syntax' ty)
d Syntax' ty
s1 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Syntax' ty -> Maybe (Syntax' ty)
d Syntax' ty
s2
  SDelay DelayType
_ Syntax' ty
s -> Syntax' ty -> Maybe (Syntax' ty)
d Syntax' ty
s
  SRcd Map Text (Maybe (Syntax' ty))
m -> forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Syntax' ty -> Maybe (Syntax' ty)
d forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Maybe a] -> [a]
catMaybes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [a]
M.elems forall a b. (a -> b) -> a -> b
$ Map Text (Maybe (Syntax' ty))
m
  SProj Syntax' ty
s1 Text
_ -> Syntax' ty -> Maybe (Syntax' ty)
d Syntax' ty
s1
  SAnnotate Syntax' ty
s Polytype
_ -> Syntax' ty -> Maybe (Syntax' ty)
d Syntax' ty
s
  SRequirements Text
_ Syntax' ty
s -> Syntax' ty -> Maybe (Syntax' ty)
d Syntax' ty
s
  -- atoms - return their position and end recursion
  Term' ty
TUnit -> forall a. Maybe a
Nothing
  TConst {} -> forall a. Maybe a
Nothing
  TDir {} -> forall a. Maybe a
Nothing
  TInt {} -> forall a. Maybe a
Nothing
  TText {} -> forall a. Maybe a
Nothing
  TBool {} -> forall a. Maybe a
Nothing
  TVar {} -> forall a. Maybe a
Nothing
  TRequire {} -> forall a. Maybe a
Nothing
  TRequireDevice {} -> forall a. Maybe a
Nothing
  -- these should not show up in surface language
  TRef {} -> forall a. Maybe a
Nothing
  TRobot {} -> forall a. Maybe a
Nothing
  TAntiInt {} -> forall a. Maybe a
Nothing
  TAntiText {} -> forall a. Maybe a
Nothing
 where
  d :: Syntax' ty -> Maybe (Syntax' ty)
d = forall ty.
ExplainableType ty =>
Int -> Syntax' ty -> Maybe (Syntax' ty)
descend Int
pos

renderDoc :: Int -> Text -> Text
renderDoc :: Int -> Text -> Text
renderDoc Int
d Text
t
  | Int
d forall a. Eq a => a -> a -> Bool
== Int
0 = Text
t
  | Bool
otherwise = Int -> Text -> Text
T.drop Int
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Text -> Text
indent (forall a. Ord a => a -> a -> a
max Int
0 (Int
4 forall a. Num a => a -> a -> a
* (Int
d forall a. Num a => a -> a -> a
- Int
1)) forall a. Num a => a -> a -> a
+ Int
2) forall a b. (a -> b) -> a -> b
$ Text
"* " forall a. Semigroup a => a -> a -> a
<> Text
t
 where
  indent :: Int -> Text -> Text
indent Int
x = [Text] -> Text
T.unlines forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (Int -> Text -> Text
T.replicate Int
x Text
" " forall a. Semigroup a => a -> a -> a
<>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [Text]
T.lines

treeToMarkdown :: Int -> Tree Text -> Text
treeToMarkdown :: Int -> Tree Text -> Text
treeToMarkdown Int
d (Node Text
t [Tree Text]
children) =
  [Text] -> Text
T.unlines forall a b. (a -> b) -> a -> b
$ Int -> Text -> Text
renderDoc Int
d Text
t forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (Int -> Tree Text -> Text
treeToMarkdown forall a b. (a -> b) -> a -> b
$ Int
d forall a. Num a => a -> a -> a
+ Int
1) [Tree Text]
children

class Show t => ExplainableType t where
  -- | Pretty print the type.
  prettyType :: t -> Text

  -- | Strip the type of its outermost layer.
  --
  -- This allows us to strip lambda or command type
  -- and get the type of the bound variable.
  getInnerType :: t -> t

  -- | Check if this type is same as the given 'Polytype'.
  --
  -- We use it to not print same type twice (e.g. inferred and generic).
  eq :: t -> Polytype -> Bool

instance ExplainableType () where
  prettyType :: () -> Text
prettyType = forall a b. a -> b -> a
const Text
"?"
  getInnerType :: () -> ()
getInnerType = forall a. a -> a
id
  eq :: () -> Polytype -> Bool
eq ()
_ Polytype
_ = Bool
False

instance ExplainableType Polytype where
  prettyType :: Polytype -> Text
prettyType = forall a. PrettyPrec a => a -> Text
prettyText
  getInnerType :: Polytype -> Polytype
getInnerType = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ \case
    (Type
l :->: Type
_r) -> Type
l
    (TyCmd Type
t) -> Type
t
    Type
t -> Type
t
  eq :: Polytype -> Polytype -> Bool
eq = forall a. Eq a => a -> a -> Bool
(==)

explain :: ExplainableType ty => Syntax' ty -> Tree Text
explain :: forall ty. ExplainableType ty => Syntax' ty -> Tree Text
explain Syntax' ty
trm = case Syntax' ty
trm forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) (Term' ty)
sTerm of
  Term' ty
TUnit -> Text -> Tree Text
literal Text
"The unit value."
  TConst Const
c -> Text -> Tree Text
literal forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const -> Text -> Text
constGenSig Const
c forall a b. (a -> b) -> a -> b
$ ConstDoc -> Text
briefDoc (ConstInfo -> ConstDoc
constDoc forall a b. (a -> b) -> a -> b
$ Const -> ConstInfo
constInfo Const
c)
  TDir {} -> Text -> Tree Text
literal Text
"A direction literal."
  TInt {} -> Text -> Tree Text
literal Text
"An integer literal."
  TText {} -> Text -> Tree Text
literal Text
"A text literal."
  TBool {} -> Text -> Tree Text
literal Text
"A boolean literal."
  TVar Text
v -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall ty. ExplainableType ty => Text -> ty -> Text -> Text
typeSignature Text
v ty
ty Text
""
  SRcd {} -> Text -> Tree Text
literal Text
"A record literal."
  SProj {} -> Text -> Tree Text
literal Text
"A record projection."
  -- type ascription
  SAnnotate Syntax' ty
lhs Polytype
typeAnn ->
    forall a. a -> [Tree a] -> Tree a
Node
      (forall ty. ExplainableType ty => Text -> ty -> Text -> Text
typeSignature Text
"_" Polytype
typeAnn Text
"A type ascription for")
      [forall ty. ExplainableType ty => Syntax' ty -> Tree Text
explain Syntax' ty
lhs]
  -- special forms (function application will show for `$`, but really should be rare)
  SApp {} -> forall ty. ExplainableType ty => Syntax' ty -> Tree Text
explainFunction Syntax' ty
trm
  TRequireDevice {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Text
"Require a specific device to be equipped."
  TRequire {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Text
"Require a certain number of an entity."
  SRequirements {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Text
"Query the requirements of a term."
  -- definition or bindings
  SLet Bool
isRecursive LocVar
var Maybe Polytype
mTypeAnn Syntax' ty
rhs Syntax' ty
_b -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall ty.
ExplainableType ty =>
Bool -> Bool -> LocVar -> ty -> Maybe Polytype -> Text
explainDefinition Bool
False Bool
isRecursive LocVar
var (Syntax' ty
rhs forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType) Maybe Polytype
mTypeAnn
  SDef Bool
isRecursive LocVar
var Maybe Polytype
mTypeAnn Syntax' ty
rhs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall ty.
ExplainableType ty =>
Bool -> Bool -> LocVar -> ty -> Maybe Polytype -> Text
explainDefinition Bool
True Bool
isRecursive LocVar
var (Syntax' ty
rhs forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType) Maybe Polytype
mTypeAnn
  SLam (LV SrcLoc
_s Text
v) Maybe Type
_mType Syntax' ty
_syn ->
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
      forall ty. ExplainableType ty => Text -> ty -> Text -> Text
typeSignature Text
v ty
ty forall a b. (a -> b) -> a -> b
$
        Text
"A lambda expression binding the variable " forall a. Semigroup a => a -> a -> a
<> Text -> Text
U.bquote Text
v forall a. Semigroup a => a -> a -> a
<> Text
"."
  SBind Maybe LocVar
mv Syntax' ty
rhs Syntax' ty
_cmds ->
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
      forall ty. ExplainableType ty => Text -> ty -> Text -> Text
typeSignature (forall b a. b -> (a -> b) -> Maybe a -> b
maybe Text
"__rhs" LocVar -> Text
lvVar Maybe LocVar
mv) (forall t. ExplainableType t => t -> t
getInnerType forall a b. (a -> b) -> a -> b
$ Syntax' ty
rhs forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType) forall a b. (a -> b) -> a -> b
$
        Text
"A monadic bind for commands" forall a. Semigroup a => a -> a -> a
<> forall b a. b -> (a -> b) -> Maybe a -> b
maybe Text
"." (\(LV SrcLoc
_s Text
v) -> Text
", that binds variable " forall a. Semigroup a => a -> a -> a
<> Text -> Text
U.bquote Text
v forall a. Semigroup a => a -> a -> a
<> Text
".") Maybe LocVar
mv
  -- composite types
  SPair {} ->
    forall a. a -> [Tree a] -> Tree a
Node
      (forall ty. ExplainableType ty => Text -> ty -> Text -> Text
typeSignature Text
"_" ty
ty Text
"A tuple consisting of:")
      (forall ty. ExplainableType ty => Syntax' ty -> Tree Text
explain forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ty. Syntax' ty -> [Syntax' ty]
unTuple Syntax' ty
trm)
  SDelay {} ->
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Text] -> Text
T.unlines forall a b. (a -> b) -> a -> b
$
      [ Text
"Delay evaluation of a term, written `{...}`."
      , Text
""
      , Text
"Swarm is an eager language, but in some cases (e.g. for `if` statements and recursive bindings) we need to delay evaluation."
      , Text
""
      , Text
"The counterpart to `{...}` is `force`:"
      , Text
"```"
      , Text
"force {t} = t"
      , Text
"```"
      ]
  -- internal syntax that should not actually show in hover
  TRef {} -> Text -> Tree Text
internal Text
"A memory reference."
  TAntiInt {} -> Text -> Tree Text
internal Text
"An antiquoted Haskell variable name of type Integer."
  TAntiText {} -> Text -> Tree Text
internal Text
"An antiquoted Haskell variable name of type Text."
  TRobot {} -> Text -> Tree Text
internal Text
"A robot reference."
 where
  ty :: ty
ty = Syntax' ty
trm forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType
  literal :: Text -> Tree Text
literal = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty. ExplainableType ty => Text -> ty -> Text -> Text
typeSignature (forall a. PrettyPrec a => a -> Text
prettyText forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ Syntax' ty
trm forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) (Term' ty)
sTerm) ty
ty
  internal :: Text -> Tree Text
internal Text
description = Text -> Tree Text
literal forall a b. (a -> b) -> a -> b
$ Text
description forall a. Semigroup a => a -> a -> a
<> Text
"\n**These should never show up in surface syntax.**"
  constGenSig :: Const -> Text -> Text
constGenSig Const
c =
    let ity :: Polytype
ity = Const -> Polytype
inferConst Const
c
     in if ty
ty forall t. ExplainableType t => t -> Polytype -> Bool
`eq` Polytype
ity then forall a. a -> a
id else forall ty. ExplainableType ty => Text -> ty -> Text -> Text
typeSignature (forall a. PrettyPrec a => a -> Text
prettyText Const
c) Polytype
ity

-- | Helper function to explain function application.
--
-- Note that 'Force' is often inserted internally, so
-- if it shows up here we drop it.
explainFunction :: ExplainableType ty => Syntax' ty -> Tree Text
explainFunction :: forall ty. ExplainableType ty => Syntax' ty -> Tree Text
explainFunction Syntax' ty
s =
  case forall ty. Syntax' ty -> NonEmpty (Syntax' ty)
unfoldApps Syntax' ty
s of
    (Syntax' SrcLoc
_ (TConst Const
Force) ty
_ :| [Syntax' ty
innerT]) -> forall ty. ExplainableType ty => Syntax' ty -> Tree Text
explain Syntax' ty
innerT
    (Syntax' SrcLoc
_ (TConst Const
Force) ty
_ :| Syntax' ty
f : [Syntax' ty]
params) -> forall {ty} {ty}.
(ExplainableType ty, ExplainableType ty) =>
Syntax' ty -> [Syntax' ty] -> Tree Text
explainF Syntax' ty
f [Syntax' ty]
params
    (Syntax' ty
f :| [Syntax' ty]
params) -> forall {ty} {ty}.
(ExplainableType ty, ExplainableType ty) =>
Syntax' ty -> [Syntax' ty] -> Tree Text
explainF Syntax' ty
f [Syntax' ty]
params
 where
  explainF :: Syntax' ty -> [Syntax' ty] -> Tree Text
explainF Syntax' ty
f [Syntax' ty]
params =
    forall a. a -> [Tree a] -> Tree a
Node
      Text
"Function application of:"
      [ forall ty. ExplainableType ty => Syntax' ty -> Tree Text
explain Syntax' ty
f
      , forall a. a -> [Tree a] -> Tree a
Node
          Text
"with parameters:"
          (forall a b. (a -> b) -> [a] -> [b]
map forall ty. ExplainableType ty => Syntax' ty -> Tree Text
explain [Syntax' ty]
params)
      ]

explainDefinition :: ExplainableType ty => Bool -> Bool -> LocVar -> ty -> Maybe Polytype -> Text
explainDefinition :: forall ty.
ExplainableType ty =>
Bool -> Bool -> LocVar -> ty -> Maybe Polytype -> Text
explainDefinition Bool
isDef Bool
isRecursive (LV SrcLoc
_s Text
var) ty
ty Maybe Polytype
maybeTypeAnnotation =
  forall ty. ExplainableType ty => Text -> ty -> Text -> Text
typeSignature Text
var ty
ty forall a b. (a -> b) -> a -> b
$
    [Text] -> Text
T.unwords
      [ Text
"A"
      , (if Bool
isRecursive then Text
"" else Text
"non-") forall a. Semigroup a => a -> a -> a
<> Text
"recursive"
      , if Bool
isDef then Text
"definition" else Text
"let"
      , Text
"expression"
      , if forall (t :: * -> *) a. Foldable t => t a -> Bool
null Maybe Polytype
maybeTypeAnnotation then Text
"without" else Text
"with"
      , Text
"a type annotation on the variable."
      ]

typeSignature :: ExplainableType ty => Var -> ty -> Text -> Text
typeSignature :: forall ty. ExplainableType ty => Text -> ty -> Text -> Text
typeSignature Text
v ty
typ Text
body = [Text] -> Text
T.unlines [Text
"```", Text
short, Text
"```", Text
body]
 where
  short :: Text
short = Text
v forall a. Semigroup a => a -> a -> a
<> Text
": " forall a. Semigroup a => a -> a -> a
<> forall t. ExplainableType t => t -> Text
prettyType ty
typ