-- |
-- Module      :  Cryptol.TypeCheck.Docstrings
-- Copyright   :  (c) 2013-2025 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# LANGUAGE Safe #-}

{-# LANGUAGE OverloadedStrings #-}
module Cryptol.TypeCheck.Docstrings where

import Cryptol.ModuleSystem.Interface
import Cryptol.ModuleSystem.Name
import Cryptol.Parser.AST (ImpName (..))
import Cryptol.TypeCheck.AST (Decl(..), Module, ModuleG(..), Pragma(..),
                              Submodule(..),  groupDecls)
import Cryptol.TypeCheck.PP
import Cryptol.TypeCheck.Type
import Cryptol.Utils.Ident (identText)
import Cryptol.Utils.Panic (panic)

import           Data.Map  (Map)
import qualified Data.Map  as Map
import           Data.Maybe (fromMaybe, maybeToList)
import           Data.Text (Text)
import qualified Data.Text as T

data DocItem = DocItem
  { DocItem -> ImpName Name
docModContext :: ImpName Name -- ^ The module scope to run repl commands in
  , DocItem -> DocFor
docFor        :: DocFor -- ^ The name the documentation is attached to
  , DocItem -> [Text]
docText       :: [Text] -- ^ The text of the attached docstring, if any
  }

data DocFor
  = DocForMod (ImpName Name)
  | DocForDef Name -- definitions that aren't modules

instance PP DocFor where
  ppPrec :: Int -> DocFor -> Doc
ppPrec Int
p DocFor
x =
    case DocFor
x of
      DocForMod ImpName Name
m -> Int -> ImpName Name -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec Int
p ImpName Name
m
      DocForDef Name
n -> Int -> Name -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec Int
p Name
n 


gatherModuleDocstrings ::
  Map Name (ImpName Name) ->
  Module ->
  [DocItem]
gatherModuleDocstrings :: Map Name (ImpName Name) -> Module -> [DocItem]
gatherModuleDocstrings Map Name (ImpName Name)
nameToModule Module
m =
  [DocItem
    { docModContext :: ImpName Name
docModContext = ModName -> ImpName Name
forall name. ModName -> ImpName name
ImpTop (Module -> ModName
forall mname. ModuleG mname -> mname
mName Module
m)
    , docFor :: DocFor
docFor = ImpName Name -> DocFor
DocForMod (ModName -> ImpName Name
forall name. ModName -> ImpName name
ImpTop (Module -> ModName
forall mname. ModuleG mname -> mname
mName Module
m))
    , docText :: [Text]
docText = Module -> [Text]
forall mname. ModuleG mname -> [Text]
mDoc Module
m
    }
  ] [DocItem] -> [DocItem] -> [DocItem]
forall a. [a] -> [a] -> [a]
++
  -- mParams m
  -- mParamTypes m
  -- mParamFuns m
  [DocItem
    { docModContext :: ImpName Name
docModContext = Name -> ImpName Name
lookupModuleName Name
n
    , docFor :: DocFor
docFor = Name -> DocFor
DocForDef Name
n
    , docText :: [Text]
docText = Maybe Text -> [Text]
forall a. Maybe a -> [a]
maybeToList (TySyn -> Maybe Text
tsDoc TySyn
t)
    } | (Name
n, TySyn
t) <- Map Name TySyn -> [(Name, TySyn)]
forall k a. Map k a -> [(k, a)]
Map.assocs (Module -> Map Name TySyn
forall mname. ModuleG mname -> Map Name TySyn
mTySyns Module
m)] [DocItem] -> [DocItem] -> [DocItem]
forall a. [a] -> [a] -> [a]
++
  [DocItem
    { docModContext :: ImpName Name
docModContext = Name -> ImpName Name
lookupModuleName Name
n
    , docFor :: DocFor
docFor = Name -> DocFor
DocForDef Name
n
    , docText :: [Text]
docText = Maybe Text -> [Text]
forall a. Maybe a -> [a]
maybeToList (NominalType -> Maybe Text
ntDoc NominalType
t)
    } | (Name
n, NominalType
t) <- Map Name NominalType -> [(Name, NominalType)]
forall k a. Map k a -> [(k, a)]
Map.assocs (Module -> Map Name NominalType
forall mname. ModuleG mname -> Map Name NominalType
mNominalTypes Module
m)] [DocItem] -> [DocItem] -> [DocItem]
forall a. [a] -> [a] -> [a]
++
  [DocItem
    { docModContext :: ImpName Name
docModContext = Name -> ImpName Name
lookupModuleName (Decl -> Name
dName Decl
d)
    , docFor :: DocFor
docFor = Name -> DocFor
DocForDef (Decl -> Name
dName Decl
d)
    , docText :: [Text]
docText = Maybe Text -> [Text]
forall a. Maybe a -> [a]
maybeToList (Decl -> Maybe Text
dDoc Decl
d Maybe Text -> Maybe Text -> Maybe Text
forall a. Semigroup a => a -> a -> a
<> Decl -> Maybe Text
exhaustBoolProp Decl
d)
    } | DeclGroup
g <- Module -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
mDecls Module
m, Decl
d <- DeclGroup -> [Decl]
groupDecls DeclGroup
g] [DocItem] -> [DocItem] -> [DocItem]
forall a. [a] -> [a] -> [a]
++
  [DocItem
    { docModContext :: ImpName Name
docModContext = Name -> ImpName Name
forall name. name -> ImpName name
ImpNested Name
n
    , docFor :: DocFor
docFor = ImpName Name -> DocFor
DocForMod (Name -> ImpName Name
forall name. name -> ImpName name
ImpNested Name
n)
    , docText :: [Text]
docText = IfaceNames Name -> [Text]
forall name. IfaceNames name -> [Text]
ifsDoc (Submodule -> IfaceNames Name
smIface Submodule
s)
    } | (Name
n, Submodule
s) <- Map Name Submodule -> [(Name, Submodule)]
forall k a. Map k a -> [(k, a)]
Map.assocs (Module -> Map Name Submodule
forall mname. ModuleG mname -> Map Name Submodule
mSubmodules Module
m)] [DocItem] -> [DocItem] -> [DocItem]
forall a. [a] -> [a] -> [a]
++
  [DocItem
    { docModContext :: ImpName Name
docModContext = ModName -> ImpName Name
forall name. ModName -> ImpName name
ImpTop (Module -> ModName
forall mname. ModuleG mname -> mname
mName Module
m)
    , docFor :: DocFor
docFor = ImpName Name -> DocFor
DocForMod (Name -> ImpName Name
forall name. name -> ImpName name
ImpNested Name
n)
    , docText :: [Text]
docText = Maybe Text -> [Text]
forall a. Maybe a -> [a]
maybeToList (ModParamNames -> Maybe Text
mpnDoc ModParamNames
s)
    } | (Name
n, ModParamNames
s) <- Map Name ModParamNames -> [(Name, ModParamNames)]
forall k a. Map k a -> [(k, a)]
Map.assocs (Module -> Map Name ModParamNames
forall mname. ModuleG mname -> Map Name ModParamNames
mSignatures Module
m)]
  where
    lookupModuleName :: Name -> ImpName Name
lookupModuleName Name
n =
      case Name -> Map Name (ImpName Name) -> Maybe (ImpName Name)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
n Map Name (ImpName Name)
nameToModule of
        Just ImpName Name
x -> ImpName Name
x
        Maybe (ImpName Name)
Nothing -> String -> [String] -> ImpName Name
forall a. HasCallStack => String -> [String] -> a
panic String
"gatherModuleDocstrings" [String
"No owning module for name:", Doc -> String
forall a. Show a => a -> String
show (Name -> Doc
forall a. PP a => a -> Doc
pp Name
n)]

    exhaustBoolProp :: Decl -> Maybe Text
exhaustBoolProp Decl
d =
      if ([[Text]] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([[Text]] -> Bool) -> (Decl -> [[Text]]) -> Decl -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [[Text]]
extractCodeBlocks (Text -> [[Text]]) -> (Decl -> Text) -> Decl -> [[Text]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Maybe Text -> Text
forall a. a -> Maybe a -> a
fromMaybe Text
"" (Maybe Text -> Text) -> (Decl -> Maybe Text) -> Decl -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Decl -> Maybe Text
dDoc) Decl
d Bool -> Bool -> Bool
&&
         (Type -> Bool
tIsBit (Type -> Bool) -> (Decl -> Type) -> Decl -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Schema -> Type
sType (Schema -> Type) -> (Decl -> Schema) -> Decl -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Decl -> Schema
dSignature) Decl
d Bool -> Bool -> Bool
&&
         Pragma
PragmaProperty Pragma -> [Pragma] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Decl -> [Pragma]
dPragmas Decl
d
      then Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ Text
"```\n" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
":exhaust " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (Ident -> Text
identText (Ident -> Text) -> (Name -> Ident) -> Name -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Ident
nameIdent) (Decl -> Name
dName Decl
d) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" // implicit" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n```"
      else Maybe Text
forall a. Maybe a
Nothing

-- | Extract the code blocks from the body of a docstring.
--
-- A single code block starts with at least 3 backticks followed by an
-- optional language specifier of \"cryptol\". This allows other kinds
-- of code blocks to be included (and ignored) in docstrings. Longer
-- backtick sequences can be used when a code block needs to be able to
-- contain backtick sequences.
--
-- @
-- /**
--  * A docstring example
--  *
--  * ```cryptol
--  * :check example
--  * ```
--  */
-- @
extractCodeBlocks :: Text -> [[Text]]
extractCodeBlocks :: Text -> [[Text]]
extractCodeBlocks Text
raw = [[Text]] -> [Text] -> [[Text]]
go [] (Text -> [Text]
T.lines Text
raw)
  where
    go :: [[Text]] -> [Text] -> [[Text]]
go [[Text]]
finished [] = [[Text]] -> [[Text]]
forall a. [a] -> [a]
reverse [[Text]]
finished
    go [[Text]]
finished (Text
x:[Text]
xs)
      | (Text
spaces, Text
x1) <- (Char -> Bool) -> Text -> (Text, Text)
T.span (Char
' ' Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==) Text
x
      , (Text
ticks, Text
x2) <- (Char -> Bool) -> Text -> (Text, Text)
T.span (Char
'`' Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==) Text
x1
      , Int
3 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Text -> Int
T.length Text
ticks
      , Bool -> Bool
not (Char -> Text -> Bool
T.elem Char
'`' Text
x2)
      , let info :: Text
info = Text -> Text
T.strip Text
x2
      = if Text
info Text -> [Text] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text
"", Text
"repl"] -- supported languages "unlabeled" and repl
        then [[Text]] -> Int -> Int -> [Text] -> [Text] -> [[Text]]
keep [[Text]]
finished (Text -> Int
T.length Text
spaces) (Text -> Int
T.length Text
ticks) [] [Text]
xs
        else [[Text]] -> Text -> [Text] -> [[Text]]
skip [[Text]]
finished Text
ticks [Text]
xs
      | Bool
otherwise = [[Text]] -> [Text] -> [[Text]]
go [[Text]]
finished [Text]
xs

    -- process a code block that we're keeping
    keep :: [[Text]] -> Int -> Int -> [Text] -> [Text] -> [[Text]]
keep [[Text]]
finished Int
_ Int
_ [Text]
acc [] = [[Text]] -> [Text] -> [[Text]]
go ([Text] -> [Text]
forall a. [a] -> [a]
reverse [Text]
acc [Text] -> [[Text]] -> [[Text]]
forall a. a -> [a] -> [a]
: [[Text]]
finished) [] -- unterminated code fences are defined to be terminated by github
    keep [[Text]]
finished Int
indentLen Int
ticksLen [Text]
acc (Text
x:[Text]
xs)
      | Text
x1 <- (Char -> Bool) -> Text -> Text
T.dropWhile (Char
' ' Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==) Text
x
      , (Text
ticks, Text
x2) <- (Char -> Bool) -> Text -> (Text, Text)
T.span (Char
'`' Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==) Text
x1
      , Int
ticksLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Text -> Int
T.length Text
ticks
      , (Char -> Bool) -> Text -> Bool
T.all (Char
' ' Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==) Text
x2
      = [[Text]] -> [Text] -> [[Text]]
go ([Text] -> [Text]
forall a. [a] -> [a]
reverse [Text]
acc [Text] -> [[Text]] -> [[Text]]
forall a. a -> [a] -> [a]
: [[Text]]
finished) [Text]
xs

      | Bool
otherwise =
        let x' :: Text
x' =
              case (Char -> Bool) -> Text -> (Text, Text)
T.span (Char
' ' Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==) Text
x of
                (Text
spaces, Text
x1)
                  | Text -> Int
T.length Text
spaces Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
indentLen -> Text
x1
                  | Bool
otherwise -> Int -> Text -> Text
T.drop Int
indentLen Text
x
        in [[Text]] -> Int -> Int -> [Text] -> [Text] -> [[Text]]
keep [[Text]]
finished Int
indentLen Int
ticksLen (Text
x' Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
acc) [Text]
xs

    -- process a code block that we're skipping
    skip :: [[Text]] -> Text -> [Text] -> [[Text]]
skip [[Text]]
finished Text
_ [] = [[Text]] -> [Text] -> [[Text]]
go [[Text]]
finished []
    skip [[Text]]
finished Text
close (Text
x:[Text]
xs)
      | Text
close Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
x = [[Text]] -> [Text] -> [[Text]]
go [[Text]]
finished [Text]
xs
      | Bool
otherwise = [[Text]] -> Text -> [Text] -> [[Text]]
skip [[Text]]
finished Text
close [Text]
xs