mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
Merge pull request #1199 from GaloisInc/feature/master-field-order
Add a field order option for the pretty-printer
This commit is contained in:
commit
bd8588adca
@ -7,12 +7,15 @@ module CryptolServer.Options (Options(..), WithOptions(..)) where
|
||||
|
||||
import qualified Argo.Doc as Doc
|
||||
import Data.Aeson hiding (Options)
|
||||
import Data.Aeson.Types (Parser, typeMismatch)
|
||||
import Data.Coerce
|
||||
import qualified Data.HashMap.Strict as HM
|
||||
import qualified Data.Text as T
|
||||
|
||||
import Cryptol.Eval(EvalOpts(..))
|
||||
import Cryptol.REPL.Monad (parsePPFloatFormat)
|
||||
import Cryptol.REPL.Monad (parseFieldOrder, parsePPFloatFormat)
|
||||
import Cryptol.Utils.Logger (quietLogger)
|
||||
import Cryptol.Utils.PP (PPOpts(..), PPFloatFormat(..), PPFloatExp(..))
|
||||
import Cryptol.Utils.PP (PPOpts(..), PPFloatFormat(..), PPFloatExp(..), FieldOrder(..), defaultPPOpts)
|
||||
|
||||
data Options = Options { optCallStacks :: Bool, optEvalOpts :: EvalOpts }
|
||||
|
||||
@ -27,9 +30,17 @@ instance FromJSON JSONEvalOpts where
|
||||
o .:! "base" .!= 10 <*>
|
||||
o .:! "prefix of infinite lengths" .!= 5 <*>
|
||||
o .:! "floating point base" .!= 10 <*>
|
||||
(getFloatFormat <$>
|
||||
o .:! "floating point format" .!=
|
||||
JSONFloatFormat (FloatFree AutoExponent))
|
||||
newtypeField getFloatFormat o "floating point format" (FloatFree AutoExponent) <*>
|
||||
newtypeField getFieldOrder o "field order" DisplayOrder
|
||||
|
||||
newtypeField :: forall wrapped bare proxy.
|
||||
(Coercible wrapped bare, FromJSON wrapped) =>
|
||||
proxy wrapped bare ->
|
||||
Object -> T.Text -> bare -> Parser bare
|
||||
newtypeField _proxy o field def = unwrap (o .:! field) .!= def where
|
||||
unwrap :: Parser (Maybe wrapped) -> Parser (Maybe bare)
|
||||
unwrap = coerce
|
||||
|
||||
|
||||
newtype JSONFloatFormat = JSONFloatFormat { getFloatFormat :: PPFloatFormat }
|
||||
|
||||
@ -46,6 +57,14 @@ instance FromJSON JSONFloatFormat where
|
||||
fail $ "Expected a valid floating point spec as in the Cryptol REPL, but got " ++ str
|
||||
|
||||
|
||||
newtype JSONFieldOrder = JSONFieldOrder { getFieldOrder :: FieldOrder }
|
||||
|
||||
instance FromJSON JSONFieldOrder where
|
||||
parseJSON (String t)
|
||||
| Just order <- parseFieldOrder (T.unpack t) = pure $ JSONFieldOrder order
|
||||
parseJSON v = typeMismatch "field order (\"display\" or \"canonical\")" v
|
||||
|
||||
|
||||
instance FromJSON Options where
|
||||
parseJSON =
|
||||
withObject "options" $
|
||||
@ -68,4 +87,7 @@ defaultOpts :: Options
|
||||
defaultOpts = Options False theEvalOpts
|
||||
|
||||
theEvalOpts :: EvalOpts
|
||||
theEvalOpts = EvalOpts quietLogger (PPOpts False 10 25 10 (FloatFree AutoExponent))
|
||||
theEvalOpts = EvalOpts quietLogger defaultPPOpts
|
||||
{ useInfLength = 25
|
||||
, useFPBase = 10
|
||||
}
|
||||
|
@ -165,7 +165,7 @@ ppValue x opts = loop
|
||||
loop :: GenValue sym -> SEval sym Doc
|
||||
loop val = case val of
|
||||
VRecord fs -> do fs' <- traverse (>>= loop) fs
|
||||
return $ braces (sep (punctuate comma (map ppField (displayFields fs'))))
|
||||
return $ braces (sep (punctuate comma (map ppField (fields fs'))))
|
||||
where
|
||||
ppField (f,r) = pp f <+> char '=' <+> r
|
||||
VTuple vals -> do vals' <- traverse (>>=loop) vals
|
||||
@ -185,6 +185,11 @@ ppValue x opts = loop
|
||||
VPoly{} -> return $ text "<polymorphic value>"
|
||||
VNumPoly{} -> return $ text "<polymorphic value>"
|
||||
|
||||
fields :: RecordMap Ident Doc -> [(Ident, Doc)]
|
||||
fields = case useFieldOrder opts of
|
||||
DisplayOrder -> displayFields
|
||||
CanonicalOrder -> canonicalFields
|
||||
|
||||
ppWordVal :: WordValue sym -> SEval sym Doc
|
||||
ppWordVal w = ppSWord x opts =<< asWordVal x w
|
||||
|
||||
|
@ -67,6 +67,7 @@ module Cryptol.REPL.Monad (
|
||||
, getUserShowProverStats
|
||||
, getUserProverValidate
|
||||
, parsePPFloatFormat
|
||||
, parseFieldOrder
|
||||
, getProverConfig
|
||||
|
||||
-- ** Configurable Output
|
||||
@ -432,22 +433,24 @@ resetTCSolver =
|
||||
-- Get the setting we should use for displaying values.
|
||||
getPPValOpts :: REPL PPOpts
|
||||
getPPValOpts =
|
||||
do base <- getKnownUser "base"
|
||||
ascii <- getKnownUser "ascii"
|
||||
infLength <- getKnownUser "infLength"
|
||||
do base <- getKnownUser "base"
|
||||
ascii <- getKnownUser "ascii"
|
||||
infLength <- getKnownUser "infLength"
|
||||
|
||||
fpBase <- getKnownUser "fpBase"
|
||||
fpFmtTxt <- getKnownUser "fpFormat"
|
||||
fpBase <- getKnownUser "fpBase"
|
||||
fpFmtTxt <- getKnownUser "fpFormat"
|
||||
fieldOrder <- getKnownUser "fieldOrder"
|
||||
let fpFmt = case parsePPFloatFormat fpFmtTxt of
|
||||
Just f -> f
|
||||
Nothing -> panic "getPPOpts"
|
||||
[ "Failed to parse fp-format" ]
|
||||
|
||||
return PPOpts { useBase = base
|
||||
, useAscii = ascii
|
||||
, useInfLength = infLength
|
||||
, useFPBase = fpBase
|
||||
, useFPFormat = fpFmt
|
||||
return PPOpts { useBase = base
|
||||
, useAscii = ascii
|
||||
, useInfLength = infLength
|
||||
, useFPBase = fpBase
|
||||
, useFPFormat = fpFmt
|
||||
, useFieldOrder = fieldOrder
|
||||
}
|
||||
|
||||
getEvalOptsAction :: REPL (IO EvalOpts)
|
||||
@ -774,6 +777,12 @@ instance IsEnvVal String where
|
||||
EnvString b -> b
|
||||
_ -> badIsEnv "String"
|
||||
|
||||
instance IsEnvVal FieldOrder where
|
||||
fromEnvVal x = case x of
|
||||
EnvString s | Just o <- parseFieldOrder s
|
||||
-> o
|
||||
_ -> badIsEnv "display` or `canonical"
|
||||
|
||||
badIsEnv :: String -> a
|
||||
badIsEnv x = panic "fromEnvVal" [ "[REPL] Expected a `" ++ x ++ "` value." ]
|
||||
|
||||
@ -908,6 +917,13 @@ userOptions = mkOptionMap
|
||||
|
||||
, simpleOpt "ignoreSafety" ["ignore-safety"] (EnvBool False) noCheck
|
||||
"Ignore safety predicates when performing :sat or :prove checks"
|
||||
|
||||
, simpleOpt "fieldOrder" ["field-order"] (EnvString "display") checkFieldOrder
|
||||
$ unlines
|
||||
[ "The order that record fields are displayed in."
|
||||
, " * display try to match the order they were written in the source code"
|
||||
, " * canonical use a predictable, canonical order"
|
||||
]
|
||||
]
|
||||
|
||||
|
||||
@ -932,7 +948,16 @@ checkPPFloatFormat val =
|
||||
EnvString s | Just _ <- parsePPFloatFormat s -> noWarns Nothing
|
||||
_ -> noWarns $ Just "Failed to parse `fp-format`"
|
||||
|
||||
parseFieldOrder :: String -> Maybe FieldOrder
|
||||
parseFieldOrder "canonical" = Just CanonicalOrder
|
||||
parseFieldOrder "display" = Just DisplayOrder
|
||||
parseFieldOrder _ = Nothing
|
||||
|
||||
checkFieldOrder :: Checker
|
||||
checkFieldOrder val =
|
||||
case val of
|
||||
EnvString s | Just _ <- parseFieldOrder s -> noWarns Nothing
|
||||
_ -> noWarns $ Just "Failed to parse field-order (expected one of \"canonical\" or \"display\")"
|
||||
|
||||
-- | Check the value to the `base` option.
|
||||
checkBase :: Checker
|
||||
|
@ -223,9 +223,6 @@ data RO = RO
|
||||
-- modules we are currently constructing.
|
||||
-- XXX: this sould probably be an interface
|
||||
|
||||
-- ^ Information about top-level declarations in modules under
|
||||
-- construction, most nested first.
|
||||
|
||||
, iSolvedHasLazy :: Map Int HasGoalSln
|
||||
-- ^ NOTE: This field is lazy in an important way! It is the
|
||||
-- final version of 'iSolvedHas' in 'RW', and the two are tied
|
||||
@ -813,7 +810,7 @@ endLocalScope =
|
||||
case iScope rw of
|
||||
x : xs | LocalScope <- mName x ->
|
||||
(reverse (mDecls x), rw { iScope = xs })
|
||||
-- ^ This ignores local type synonyms... Where should we put them?
|
||||
-- This ignores local type synonyms... Where should we put them?
|
||||
|
||||
_ -> panic "endLocalScope" ["Missing local scope"]
|
||||
|
||||
|
@ -30,11 +30,12 @@ import Prelude.Compat
|
||||
|
||||
-- | How to pretty print things when evaluating
|
||||
data PPOpts = PPOpts
|
||||
{ useAscii :: Bool
|
||||
, useBase :: Int
|
||||
, useInfLength :: Int
|
||||
, useFPBase :: Int
|
||||
, useFPFormat :: PPFloatFormat
|
||||
{ useAscii :: Bool
|
||||
, useBase :: Int
|
||||
, useInfLength :: Int
|
||||
, useFPBase :: Int
|
||||
, useFPFormat :: PPFloatFormat
|
||||
, useFieldOrder :: FieldOrder
|
||||
}
|
||||
deriving Show
|
||||
|
||||
@ -51,11 +52,14 @@ data PPFloatExp = ForceExponent -- ^ Always show an exponent
|
||||
| AutoExponent -- ^ Only show exponent when needed
|
||||
deriving Show
|
||||
|
||||
data FieldOrder = DisplayOrder | CanonicalOrder deriving (Bounded, Enum, Eq, Ord, Read, Show)
|
||||
|
||||
|
||||
defaultPPOpts :: PPOpts
|
||||
defaultPPOpts = PPOpts { useAscii = False, useBase = 10, useInfLength = 5
|
||||
, useFPBase = 16
|
||||
, useFPFormat = FloatFree AutoExponent
|
||||
, useFieldOrder = DisplayOrder
|
||||
}
|
||||
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user