diff --git a/cryptol-remote-api/src/CryptolServer/Options.hs b/cryptol-remote-api/src/CryptolServer/Options.hs index f09b3963d..e9ee3fb99 100644 --- a/cryptol-remote-api/src/CryptolServer/Options.hs +++ b/cryptol-remote-api/src/CryptolServer/Options.hs @@ -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 + } diff --git a/src/Cryptol/Eval/Value.hs b/src/Cryptol/Eval/Value.hs index 75808e048..3666e75f5 100644 --- a/src/Cryptol/Eval/Value.hs +++ b/src/Cryptol/Eval/Value.hs @@ -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 "" VNumPoly{} -> return $ text "" + 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 diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs index 4004f82bc..7e9062e4a 100644 --- a/src/Cryptol/REPL/Monad.hs +++ b/src/Cryptol/REPL/Monad.hs @@ -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 diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs index 3e129f405..af6127a32 100644 --- a/src/Cryptol/TypeCheck/Monad.hs +++ b/src/Cryptol/TypeCheck/Monad.hs @@ -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"] diff --git a/src/Cryptol/Utils/PP.hs b/src/Cryptol/Utils/PP.hs index ba197c5a3..e91b3bcce 100644 --- a/src/Cryptol/Utils/PP.hs +++ b/src/Cryptol/Utils/PP.hs @@ -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 }