-
Notifications
You must be signed in to change notification settings - Fork 126
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Initial implementation of check docstrings from python (#1712)
* Initial implementation of "check docstrings" from python * Improve and synchronize the unlit and docstring code fence parser to better match GitHub markdown syntax * Associate identifiers with docstring comes from * Add :set proverTimeout support for goal-level timeouts * Adds and evaluates docstrings on top-level module declarations
- Loading branch information
Showing
35 changed files
with
634 additions
and
107 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
143 changes: 143 additions & 0 deletions
143
cryptol-remote-api/src/CryptolServer/CheckDocstrings.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,143 @@ | ||
| {-# LANGUAGE MultiParamTypeClasses #-} | ||
| {-# LANGUAGE ScopedTypeVariables #-} | ||
| {-# LANGUAGE OverloadedStrings #-} | ||
| {-# OPTIONS_GHC -Wno-orphans #-} | ||
| {-# LANGUAGE InstanceSigs #-} | ||
| module CryptolServer.CheckDocstrings | ||
| ( checkDocstrings | ||
| , checkDocstringsDescr | ||
| , CheckDocstringsParams(..) | ||
| , CheckDocstringsResult(..) | ||
| ) | ||
| where | ||
|
|
||
| import qualified Argo.Doc as Doc | ||
| import Control.Monad.IO.Class (MonadIO(liftIO)) | ||
| import Data.Aeson ((.=),FromJSON, ToJSON) | ||
| import qualified Data.Aeson as Aeson | ||
| import qualified Data.Aeson as JSON | ||
| import Data.IORef (newIORef) | ||
| import qualified Cryptol.ModuleSystem.Env as M | ||
| import Cryptol.REPL.Command | ||
| import CryptolServer | ||
| import CryptolServer.Exceptions (noModule, moduleNotLoaded) | ||
| import qualified Cryptol.REPL.Monad as REPL | ||
| import Cryptol.Utils.Logger (quietLogger) | ||
| import Cryptol.Parser.AST (ImpName(..)) | ||
| import qualified System.Random.TF as TF | ||
| import qualified Cryptol.Symbolic.SBV as SBV | ||
| import Cryptol.REPL.Monad (mkUserEnv, userOptions) | ||
| import Cryptol.Utils.PP (pp) | ||
| import Data.Proxy (Proxy(Proxy)) | ||
| import Data.Typeable (typeRep) | ||
|
|
||
| checkDocstringsDescr :: Doc.Block | ||
| checkDocstringsDescr = | ||
| Doc.Paragraph | ||
| [ Doc.Text "Check docstrings" ] | ||
|
|
||
| checkDocstrings :: CheckDocstringsParams -> CryptolCommand CheckDocstringsResult | ||
| checkDocstrings CheckDocstringsParams = do | ||
| env <- getModuleEnv | ||
| ln <- case M.meFocusedModule env of | ||
| Just (ImpTop n) -> pure n | ||
| _ -> raise noModule | ||
| m <- case M.lookupModule ln env of | ||
| Nothing -> raise (moduleNotLoaded ln) | ||
| Just m -> pure m | ||
| solver <- getTCSolver | ||
| cfg <- getTCSolverConfig | ||
| liftIO $ | ||
| do rng <- TF.newTFGen | ||
| rwRef <- newIORef REPL.RW | ||
| { REPL.eLoadedMod = Nothing | ||
| , REPL.eEditFile = Nothing | ||
| , REPL.eContinue = True | ||
| , REPL.eIsBatch = False | ||
| , REPL.eModuleEnv = env | ||
| , REPL.eUserEnv = mkUserEnv userOptions | ||
| , REPL.eLogger = quietLogger | ||
| , REPL.eCallStacks = False | ||
| , REPL.eUpdateTitle = return () | ||
| , REPL.eProverConfig = Left SBV.defaultProver | ||
| , REPL.eTCConfig = cfg | ||
| , REPL.eTCSolver = Just solver | ||
| , REPL.eTCSolverRestarts = 0 | ||
| , REPL.eRandomGen = rng | ||
| } | ||
| REPL.unREPL (CheckDocstringsResult <$> checkDocStrings m) rwRef | ||
|
|
||
| newtype CheckDocstringsResult = CheckDocstringsResult [DocstringResult] | ||
|
|
||
| instance ToJSON CheckDocstringsResult where | ||
| toJSON (CheckDocstringsResult r) = JSON.object ["results" .= r] | ||
|
|
||
| instance ToJSON DocstringResult where | ||
| toJSON dr = JSON.object ["name" .= show (pp (drName dr)), "fences" .= drFences dr] | ||
|
|
||
| instance ToJSON SubcommandResult where | ||
| toJSON r = JSON.object | ||
| [ "input" .= srInput r | ||
| , "log" .= srLog r | ||
| , "result" .= srResult r | ||
| ] | ||
|
|
||
| instance ToJSON CommandResult where | ||
| toJSON r = JSON.object | ||
| [ "type" .= crType r | ||
| , "value" .= crValue r | ||
| , "success" .= crSuccess r | ||
| ] | ||
|
|
||
| data CheckDocstringsParams = CheckDocstringsParams | ||
|
|
||
| instance FromJSON CheckDocstringsParams where | ||
| parseJSON = | ||
| JSON.withObject "check docstrings parameters" $ | ||
| \_ -> pure CheckDocstringsParams | ||
|
|
||
|
|
||
| instance Doc.DescribedMethod CheckDocstringsParams CheckDocstringsResult where | ||
| parameterFieldDescription = [] | ||
|
|
||
| resultFieldDescription = | ||
| [("results", | ||
| Doc.Paragraph | ||
| [ Doc.Text "A list of " | ||
| , Doc.Link (Doc.TypeDesc (typeRep (Proxy :: Proxy DocstringResult))) "docstring results" | ||
| , Doc.Text " correspoding to each definition in the current module." | ||
| ] | ||
|
|
||
| )] | ||
|
|
||
| instance Doc.Described DocstringResult where | ||
| typeName = "DocstringResult" | ||
| description = | ||
| [ Doc.Paragraph [Doc.Text "The result of evaluating the code fences in a docstring"] | ||
| , Doc.DescriptionList | ||
| [ ( pure (Doc.Literal "name") | ||
| , Doc.Paragraph[Doc.Text "The definition assocated with the docstring"] | ||
| ) | ||
| , ( pure (Doc.Literal "fences") | ||
| , Doc.Paragraph[Doc.Text "An array code fences each containing an array of individual " | ||
| , Doc.Link (Doc.TypeDesc (typeRep (Proxy :: Proxy CommandResult))) "command results"] | ||
| ) | ||
| ] | ||
| ] | ||
|
|
||
| instance Doc.Described CommandResult where | ||
| typeName = "CommandResult" | ||
| description = | ||
| [ Doc.Paragraph [Doc.Text "The result of executing a single REPL command."] | ||
| , Doc.DescriptionList | ||
| [ ( pure (Doc.Literal "success") | ||
| , Doc.Paragraph [Doc.Text "Boolean indicating successful execution of the command"] | ||
| ) | ||
| , ( pure (Doc.Literal "type") | ||
| , Doc.Paragraph[Doc.Text "The string representation of the type returned or null"] | ||
| ) | ||
| , ( pure (Doc.Literal "value") | ||
| , Doc.Paragraph[Doc.Text "The string representation of the value returned or null"] | ||
| ) | ||
| ] | ||
| ] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.