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

Improve display ordering on names and group constraint synonyms separately.

Browse Source 
See #503
This commit is contained in:
Iavor Diatchki 2018-03-30 15:28:22 -07:00
parent 9d344bb452
commit bfb3290e9b
2 changed files with 43 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

31
src/Cryptol/ModuleSystem/Name.hs
View File

@ -54,11 +54,14 @@ import Cryptol.Utils.Ident
import Cryptol.Utils.Panic
import Cryptol.Utils.PP
import Control.DeepSeq
import Control.Monad.Fix (MonadFix(mfix))
import qualified Data.Map as Map
import qualified Data.Monoid as M
import Data.Ord (comparing)
import qualified Data.Text as Text
import Data.Char(isAlpha,toUpper)
import GHC.Generics (Generic)
import MonadLib
import Prelude ()
@ -127,25 +130,41 @@ cmpNameDisplay disp l r =
(Declared nsl, Declared nsr) ->
let pfxl = fmtModName nsl (getNameFormat nsl (nameIdent l) disp)
pfxr = fmtModName nsr (getNameFormat nsr (nameIdent r) disp)
in case compare pfxl pfxr of
EQ -> compare (nameIdent l) (nameIdent r)
in case cmpText pfxl pfxr of
EQ -> cmpName l r
cmp -> cmp
(Parameter,Parameter) ->
compare (nameIdent l) (nameIdent r)
(Parameter,Parameter) -> cmpName l r
(Declared nsl,Parameter) ->
let pfxl = fmtModName nsl (getNameFormat nsl (nameIdent l) disp)
in case compare pfxl (identText (nameIdent r)) of
in case cmpText pfxl (identText (nameIdent r)) of
EQ -> GT
cmp -> cmp
(Parameter,Declared nsr) ->
let pfxr = fmtModName nsr (getNameFormat nsr (nameIdent r) disp)
in case compare (identText (nameIdent l)) pfxr of
in case cmpText (identText (nameIdent l)) pfxr of
EQ -> LT
cmp -> cmp
where
cmpName xs ys = cmpIdent (nameIdent xs) (nameIdent ys)
cmpIdent xs ys = cmpText (identText xs) (identText ys)
-- Note that this assumes that `xs` is `l` and `ys` is `r`
cmpText xs ys =
case (Text.null xs, Text.null ys) of
(True,True) -> EQ
(True,False) -> LT
(False,True) -> GT
(False,False) -> compare (cmp (fx l) xs) (cmp (fx r) ys)
where
fx a = fLevel <$> nameFixity a
cmp a cs = (ordC (Text.index cs 0), a, cs)
ordC a | isAlpha a = fromEnum (toUpper a)
| a == '_' = 1
| otherwise = 0
-- | Figure out how the name should be displayed, by referencing the display
-- function in the environment. NOTE: this function doesn't take into account

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

@ -813,11 +813,14 @@ browseTSyns :: (M.Name -> Bool) -> M.IfaceDecls -> NameDisp -> REPL ()
browseTSyns isVisible M.IfaceDecls { .. } names = do
let tsyns = sortBy (M.cmpNameDisplay names `on` T.tsName)
[ ts | ts <- Map.elems ifTySyns, isVisible (T.tsName ts) ]
unless (null tsyns) $ do
rPutStrLn "Type Synonyms"
rPutStrLn "============="
rPrint (runDoc names (nest 4 (vcat (map pp tsyns))))
rPutStrLn ""
(cts,tss) = partition isCtrait tsyns
ppBlock names pp "Type Synonyms" tss
ppBlock names pp "Constraint Synonyms" cts
where
isCtrait t = T.kindResult (T.kindOf (T.tsDef t)) == T.KProp
browseNewtypes :: (M.Name -> Bool) -> M.IfaceDecls -> NameDisp -> REPL ()
browseNewtypes isVisible M.IfaceDecls { .. } names = do
@ -838,16 +841,19 @@ browseVars isVisible M.IfaceDecls { .. } names = do
let isProp p = T.PragmaProperty `elem` (M.ifDeclPragmas p)
(props,syms) = partition isProp vars
ppBlock "Properties" props
ppBlock "Symbols" syms
where
ppBlock name xs = unless (null xs) $
let ppVar M.IfaceDecl { .. } = hang (pp ifDeclName <+> char ':')
2 (pp ifDeclSig)
ppBlock names ppVar "Properties" props
ppBlock names ppVar "Symbols" syms
ppBlock :: NameDisp -> (a -> Doc) -> String -> [a] -> REPL ()
ppBlock names ppFun name xs = unless (null xs) $
do rPutStrLn name
rPutStrLn (replicate (length name) '=')
let ppVar M.IfaceDecl { .. } = hang (pp ifDeclName <+> char ':')
2 (pp ifDeclSig)
rPrint (runDoc names (nest 4 (vcat (map ppVar xs))))
rPrint (runDoc names (nest 4 (vcat (map ppFun xs))))
rPutStrLn ""