GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-03 18:22:58 +03:00
Code Issues Projects Releases Wiki Activity

Have :help use the doc string, instead of built-in docs

Browse Source
This commit is contained in:
Trevor Elliott 2015-06-05 14:37:25 -07:00
parent a736f740f9
commit 7eb7c93985
7 changed files with 91 additions and 37 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Cryptol/ModuleSystem/Interface.hs
View File

@ -83,6 +83,7 @@ data IfaceDecl = IfaceDecl
, ifDeclPragmas :: [Pragma]
, ifDeclInfix :: Bool
, ifDeclFixity :: Maybe Fixity
, ifDeclDoc :: Maybe String
} deriving (Show)
mkIfaceDecl :: Decl -> IfaceDecl
@ -92,6 +93,7 @@ mkIfaceDecl d = IfaceDecl
, ifDeclPragmas = dPragmas d
, ifDeclInfix = dInfix d
, ifDeclFixity = dFixity d
, ifDeclDoc = dDoc d
}
-- | Like mapIfaceDecls, but gives you back a NameEnv that describes the

24
src/Cryptol/Parser.y
View File

@ -9,7 +9,7 @@ module Cryptol.Parser
, parseLetDecl, parseLetDeclWith
, parseRepl, parseReplWith
, parseSchema, parseSchemaWith
, parseModName
, parseModName, parseHelpName
, ParseError(..), ppError
, Layout(..)
, Config(..), defaultConfig
@ -132,6 +132,7 @@ import Paths_cryptol
%name repl repl
%name schema schema
%name modName modName
%name helpName help_name
%tokentype { Located Token }
%monad { ParseM }
%lexer { lexerP } { Located _ (Token EOF _) }
@ -253,10 +254,10 @@ prim_bind :: { [TopDecl] }
| mbDoc 'primitive' '(' op ')' ':' schema { mkPrim $1 True $4 $7 }
doc :: { Text }
: DOC { tokenText (thing $1) }
doc :: { Located String }
: DOC { mkDoc (fmap tokenText $1) }
mbDoc :: { Maybe Text }
mbDoc :: { Maybe (Located String) }
: doc { Just $1 }
| {- empty -} { Nothing }
@ -653,6 +654,15 @@ modName :: { Located ModName }
qname :: { Located QName }
: qname_parts { mkQName $1 }
help_name :: { Located QName }
: help_name_parts { mkQName $1 }
help_name_parts :: { [LName] }
: name { [$1] }
| op { [fmap unqual $1] }
| qname_parts '::' name { $3:$1 }
| qname_parts '::' op { fmap unqual $3:$1 }
{- The types that can come after a back-tick: either a type demotion,
or an explicit type application. Explicit type applications are converted
to records, which cannot be demoted. -}
@ -684,6 +694,12 @@ parseModName txt =
Right a -> Just (thing a)
Left _ -> Nothing
parseHelpName :: String -> Maybe QName
parseHelpName txt =
case parseString defaultConfig { cfgModuleScope = False } helpName txt of
Right a -> Just (thing a)
Left _ -> Nothing
addImplicitIncludes :: Config -> Program -> Program
addImplicitIncludes cfg (Program ds) =
Program $ map path (cfgAutoInclude cfg) ++ ds

13
src/Cryptol/Parser/AST.hs
View File

@ -73,7 +73,6 @@ import qualified Data.Set as Set
import Data.List(intersperse)
import Data.Bits(shiftR)
import Data.Maybe (catMaybes)
import Data.Text.Lazy (Text)
import Numeric(showIntAtBase)
#if __GLASGOW_HASKELL__ < 710
@ -92,12 +91,12 @@ type LString = Located String
newtype Program = Program [TopDecl]
deriving (Eq,Show)
deriving (Show)
data Module = Module { mName :: Located ModName
, mImports :: [Located Import]
, mDecls :: [TopDecl]
} deriving (Eq,Show)
} deriving (Show)
modRange :: Module -> Range
modRange m = rCombs $ catMaybes
@ -111,7 +110,7 @@ modRange m = rCombs $ catMaybes
data TopDecl = Decl (TopLevel Decl)
| TDNewtype (TopLevel Newtype)
| Include (Located FilePath)
deriving (Eq,Show)
deriving (Show)
data Decl = DSignature [LQName] Schema
| DFixity !Fixity [LQName]
@ -160,7 +159,7 @@ data Bind = Bind { bName :: LQName -- ^ Defined thing
, bFixity :: Maybe Fixity -- ^ Optional fixity info
, bPragmas :: [Pragma] -- ^ Optional pragmas
, bMono :: Bool -- ^ Is this a monomorphic binding
, bDoc :: Maybe Text -- ^ Optional doc string
, bDoc :: Maybe String -- ^ Optional doc string
} deriving (Eq,Show)
type LBindDef = Located BindDef
@ -197,9 +196,9 @@ data ExportType = Public
deriving (Eq,Show,Ord)
data TopLevel a = TopLevel { tlExport :: ExportType
, tlDoc :: Maybe Text
, tlDoc :: Maybe (Located String)
, tlValue :: a
} deriving (Show,Eq,Ord)
} deriving (Show)
instance Functor TopLevel where
fmap f tl = tl { tlValue = f (tlValue tl) }

25
src/Cryptol/Parser/NoPat.hs
View File

@ -25,15 +25,12 @@ import MonadLib
import Data.Maybe(maybeToList)
import Data.Either(partitionEithers)
import qualified Data.Map as Map
import Data.Text.Lazy (Text)
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative(Applicative(..),(<$>)(<$))
import Data.Traversable(traverse)
#endif
import Debug.Trace
class RemovePatterns t where
-- | Eliminate all patterns in a program.
removePatterns :: t -> (t, [Error])
@ -311,7 +308,7 @@ noPatModule m =
type AnnotMap = ( Map.Map QName [Located Pragma]
, Map.Map QName [Located Schema]
, Map.Map QName [Located Fixity]
, Map.Map QName [Text]
, Map.Map QName [Located String]
)
-- | Add annotations to exported declaration groups.
@ -372,7 +369,7 @@ annotB Bind { .. } =
f <- lift $ checkFixs name (jn thisFixes)
d <- lift $ checkDocs name (jn thisDocs)
set (pragmas1,sigs1,fixes1,docs1)
traceShow d $ return Bind { bSignature = s
return Bind { bSignature = s
, bPragmas = map thing (jn thisPs) ++ bPragmas
, bFixity = f
, bDoc = d
@ -394,11 +391,11 @@ checkFixs f fs@(x:_) = do recordError $ MultipleFixities f $ map srcRange fs
return (Just (thing x))
checkDocs :: QName -> [Text] -> NoPatM (Maybe Text)
checkDocs _ [] = return Nothing
checkDocs _ [d] = return (Just d)
checkDocs f (d:_) = do recordError $ MultipleDocs f
return (Just d)
checkDocs :: QName -> [Located String] -> NoPatM (Maybe String)
checkDocs _ [] = return Nothing
checkDocs _ [d] = return (Just (thing d))
checkDocs f ds@(d:_) = do recordError $ MultipleDocs f (map srcRange ds)
return (Just (thing d))
-- | Does this declaration provide some signatures?
@ -419,7 +416,7 @@ toFixity (DFixity f ns) = [ (thing n, [Located (srcRange n) f]) | n <- ns ]
toFixity _ = []
-- | Does this top-level declaration provide a documentation string?
toDocs :: TopLevel Decl -> [(QName, [Text])]
toDocs :: TopLevel Decl -> [(QName, [Located String])]
toDocs TopLevel { .. }
| Just txt <- tlDoc = go txt tlValue
| otherwise = []
@ -450,7 +447,7 @@ data Error = MultipleSignatures QName [Located Schema]
| PragmaNoBind (Located QName) Pragma
| MultipleFixities QName [Range]
| FixityNoBind (Located QName)
| MultipleDocs QName
| MultipleDocs QName [Range]
deriving (Show)
instance Functor NoPatM where fmap = liftM
@ -514,7 +511,7 @@ instance PP Error where
text "Fixity declaration without a matching binding for:" <+>
pp (thing n)
-- XXX it would be nice to have the locations of the documentation strings
MultipleDocs n ->
MultipleDocs n locs ->
text "Multiple documentation blocks given for:" <+> pp n
$$ nest 2 (vcat (map pp locs))

34
src/Cryptol/Parser/ParserUtils.hs
View File

@ -266,7 +266,7 @@ anonRecord ~(Just r) ts = TRecord (map toField ts)
where noName = Located { srcRange = r, thing = Name "" }
toField t = Named { name = noName, value = t }
exportDecl :: Maybe Text -> ExportType -> Decl -> TopDecl
exportDecl :: Maybe (Located String) -> ExportType -> Decl -> TopDecl
exportDecl mbDoc e d = Decl TopLevel { tlExport = e
, tlDoc = mbDoc
, tlValue = d }
@ -344,7 +344,7 @@ mkIf ifThens theElse = foldr addIfThen theElse ifThens
-- pass. This is also the reason we add the doc to the TopLevel constructor,
-- instead of just place it on the binding directly. A better solution might be
-- to just have a different constructor for primitives.
mkPrim :: Maybe Text -> Bool -> LQName -> Schema -> [TopDecl]
mkPrim :: Maybe (Located String) -> Bool -> LQName -> Schema -> [TopDecl]
mkPrim mbDoc isInfix n sig =
[ exportDecl mbDoc Public
$ DBind Bind { bName = n
@ -360,3 +360,33 @@ mkPrim mbDoc isInfix n sig =
, exportDecl Nothing Public
$ DSignature [n] sig
]
mkDoc :: Located Text -> Located String
mkDoc ltxt = ltxt { thing = docStr }
where
docStr = unlines
$ map T.unpack
$ dropPrefix
$ trimFront
$ T.lines
$ T.dropWhileEnd (`elem` "/* \r\n\t")
$ thing ltxt
trimFront [] = []
trimFront (l:ls)
| T.all (`elem` "/* \r\n\t") l = ls
| otherwise = T.dropWhile (`elem` "/* ") l : ls
dropPrefix [] = []
dropPrefix [t] = [T.dropWhile (`elem` "/* ") t]
dropPrefix ts@(l:ls) =
case T.uncons l of
Just (c,_) | all (commonPrefix c) ls -> dropPrefix (map (T.drop 1) ts)
_ -> ts
where
commonPrefix c t =
case T.uncons t of
Just (c',_) -> c == c'
Nothing -> False

27
src/Cryptol/REPL/Command.hs
View File

@ -6,7 +6,7 @@
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE CPP, PatternGuards, FlexibleContexts #-}
{-# LANGUAGE CPP, PatternGuards, FlexibleContexts, RecordWildCards #-}
module Cryptol.REPL.Command (
-- * Commands
Command(..), CommandDescr(..), CommandBody(..)
@ -42,7 +42,8 @@ import qualified Cryptol.Testing.Eval as Test
import qualified Cryptol.Testing.Random as TestR
import qualified Cryptol.Testing.Exhaust as TestX
import Cryptol.Parser
(parseExprWith,parseReplWith,ParseError(),Config(..),defaultConfig,parseModName)
(parseExprWith,parseReplWith,ParseError(),Config(..),defaultConfig
,parseModName,parseHelpName)
import Cryptol.Parser.Position (emptyRange)
import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.TypeCheck.Subst as T
@ -138,7 +139,7 @@ nbCommandList =
, CommandDescr [ ":b", ":browse" ] (ExprTypeArg browseCmd)
"display the current environment"
, CommandDescr [ ":?", ":help" ] (ExprArg helpCmd)
"display a brief description about a built-in operator"
"display a brief description about a function"
, CommandDescr [ ":s", ":set" ] (OptionArg setOptionCmd)
"set an environmental option (:set on its own displays current values)"
, CommandDescr [ ":check" ] (ExprArg (qcCmd QCRandom))
@ -627,11 +628,20 @@ setOptionCmd str
helpCmd :: String -> REPL ()
helpCmd cmd
| null cmd = mapM_ rPutStrLn (genHelp commandList)
| Just (ec,_) <- lookup cmd builtIns =
rPrint $ helpDoc ec
| otherwise = do rPutStrLn $ "// No documentation is available."
typeOfCmd cmd
| null cmd = mapM_ rPutStrLn (genHelp commandList)
| otherwise =
case parseHelpName cmd of
Just qname ->
do (env,_) <- getFocusedEnv
case Map.lookup qname (M.ifDecls env) of
Just [M.IfaceDecl { .. }]
| Just str <- ifDeclDoc -> do rPutStrLn ""
rPutStrLn str
_ -> rPutStrLn "// No documentation is available."
Nothing ->
rPutStrLn ("Unable to parse name: " ++ cmd)
runShellCmd :: String -> REPL ()
@ -785,6 +795,7 @@ bindItVariable ty expr = do
, T.dPragmas = []
, T.dInfix = False
, T.dFixity = Nothing
, T.dDoc = Nothing
}
liftModuleCmd (M.evalDecls [dg])
denv <- getDynEnv

3
src/Cryptol/TypeCheck/AST.hs
View File

@ -37,7 +37,6 @@ import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.IntMap as IntMap
import Data.Set (Set)
import Data.Text.Lazy (Text)
{- | A Cryptol module.
-}
@ -263,7 +262,7 @@ data Decl = Decl { dName :: QName
, dPragmas :: [Pragma]
, dInfix :: !Bool
, dFixity :: Maybe Fixity
, dDoc :: Maybe Text
, dDoc :: Maybe String
} deriving (Show)
data DeclDef = DPrim