Add a field order option for the pretty-printer

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
+  }

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 "<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
 

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

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"]
 

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
                        }