Massaging Upper Bounds

.travis.yml

@@ -97,15 +97,15 @@ matrix:
     addons:
       artifacts:
         paths:
-          - .stack-work/dist/x86_64-osx/Cabal-2.2.0.1/build/pact/pact
+          - .stack-work/dist/x86_64-osx/Cabal-2.4.0.1/build/pact/pact
 
   # Linux build
   - env: BUILD=stack ARGS="-j1" Z3VERSION="4.8.3"
     addons:
       apt: {packages: [libgmp-dev]}
       artifacts:
         paths:
-          - .stack-work/dist/x86_64-linux/Cabal-2.2.0.1/build/pact/pact
+          - .stack-work/dist/x86_64-linux/Cabal-2.4.0.1/build/pact/pact
 
   # OSX Build Yosemite
   # - env: BUILD=stack ARGS=""

pact.cabal

@@ -138,27 +138,27 @@ library
 
   build-depends:       Decimal >= 0.4.2 && < 0.6
                      , aeson >= 0.11.3.0 && < 1.5
-                     , algebraic-graphs >= 0.2 && < 0.3
+                     , algebraic-graphs >= 0.2 && < 0.4
                      , prettyprinter >= 1.2 && < 1.3
                      , prettyprinter-ansi-terminal >= 1.1 && < 1.2
                      , prettyprinter-convert-ansi-wl-pprint
                      , attoparsec >= 0.13.0.2 && < 0.14
-                     , base >=4.9.0.0 && < 4.12
+                     , base >=4.9.0.0 && < 4.13
                      , base16-bytestring >=0.1.1.6 && < 0.2
                      , base64-bytestring >= 1.0.0.1
                      , bound >= 2 && < 2.1
                      , bytestring >=0.10.8.1 && < 0.11
                      , cereal >=0.5.4.0 && < 0.6
-                     , containers >= 0.5.7 && < 0.6
+                     , containers >= 0.5.7 && < 0.7
                      , data-default >= 0.7.1.1 && < 0.8
                      , deepseq >= 1.4.2.0 && < 1.5
                      , deriving-compat >= 0.5.1
                      , directory >= 1.2.6.2 && < 1.4
                      , exceptions >= 0.8.3 && < 0.11
                      , filepath >= 1.4.1.0 && < 1.5
                      , hashable >= 1.2.4.0 && < 1.3
-                     , hspec >= 2.2.4 && < 2.6
-                     , lens >= 4.14 && < 4.17
+                     , hspec >= 2.2.4 && < 2.8
+                     , lens >= 4.14 && < 4.18
                      , lens-aeson >= 1.0.0.5 && < 1.1
                      , megaparsec >= 6
                      , mtl >= 2.2.1 && < 2.3
@@ -169,7 +169,7 @@ library
                      , safe >= 0.3.11 && < 0.4
                      , scientific >= 0.3.4.9 && < 0.4
                      , semigroups >= 0.18.2 && < 0.19
-                     , stm >= 2.4.4.1 && < 2.5
+                     , stm >= 2.4.4.1 && < 2.6
                      , text >= 1.2.2.1 && < 1.3
                      -- kadena ghcjs compat fork
                      , thyme == 0.3.6.0
@@ -179,7 +179,7 @@ library
                      , utf8-string >= 1.0.1.1 && < 1.1
                      , vector >= 0.11.0.0 && < 0.13
                      , vector-algorithms >= 0.7
-                     , vector-space >= 0.10.4 && < 0.14
+                     , vector-space >= 0.10.4 && < 0.16
                      , mmorph >= 1.1 && < 1.2
                      , constraints
                      , servant
@@ -194,7 +194,7 @@ library
   if !impl(ghcjs)
     build-depends:
         async
-      , criterion >= 1.1.4 && < 1.5
+      , criterion >= 1.1.4 && < 1.6
       , cryptonite
       , direct-sqlite
       , fast-logger
@@ -203,7 +203,7 @@ library
       , safe-exceptions >= 0.1.5.0 && < 0.2
       , sbv >= 7.11
       , servant-server
-      , statistics >= 0.13.3 && < 0.15
+      , statistics >= 0.13.3 && < 0.16
       , wai-cors
       , warp
       , yaml
@@ -258,32 +258,33 @@ test-suite hspec
   ghc-options:      -Wall -threaded -rtsopts -O2 -Wincomplete-record-updates -Wincomplete-uni-patterns -Wredundant-constraints
   build-depends:
                 base
-              , bound
               , Decimal
-              , deepseq
-              , exceptions
-              , hspec
               , HUnit
-              , pact
               , aeson
+              , base16-bytestring >=0.1.1.6 && < 0.2
+              , bound
+              , bytestring
               , containers
+              , data-default
+              , deepseq
               , directory
+              , errors >= 2.3
+              , exceptions
               , filepath
-              , mmorph
-              , data-default
+              , hedgehog == 0.6.*
+              , hspec
+              , hw-hspec-hedgehog == 0.1.*
+              , intervals
               , lens
-              , unordered-containers
+              , mmorph
+              , mtl
+              , pact
               , prettyprinter
               , prettyprinter-ansi-terminal
               , prettyprinter-convert-ansi-wl-pprint
-              , bytestring
-              , base16-bytestring >=0.1.1.6 && < 0.2
-              , mtl
               , text
               , transformers
-              , hedgehog == 0.6.*
-              , hw-hspec-hedgehog == 0.1.*
-              , intervals
+              , unordered-containers
               , vector
   other-modules:
                 Blake2Spec

stack.yaml

@@ -1,18 +1,29 @@
 # stack yaml for ghc builds
 
-resolver: lts-12.9
+resolver: lts-13.22
 
 packages:
   - '.'
 
+# GHC 8.6 has a more aggressive Pattern Match exhaustion checker. A number of
+# Pact's `Analysis` modules cause seeming infinite loops in the compiler during
+# this analysis, so here we limit the depth to 5000, then override `-Werror`
+# with `-Wwarn` to avoid failing the build.
+ghc-options:
+  pact: -fmax-pmcheck-iterations=5000 -Wwarn
+
 extra-deps:
-  - aeson-1.4.2.0
-  - algebraic-graphs-0.2
-  - crackNum-2.3
-  - FloatingHex-0.4
-  - compactable-0.1.2.2
-  - ed25519-donna-0.1.1
-  - hw-hspec-hedgehog-0.1.0.5
+  # --- Missing from Stackage --- #
+  - ed25519-donna-0.1.1@sha256:344c0bb83603ed896012f441e54b380314dc4910320577cd18a9071e34f24fe9,2358
+  - prettyprinter-convert-ansi-wl-pprint-1.1@sha256:ae908ee44422c38a696858f04928d4b2448df656c09e6b5f5b1be05d99669fb0,3022
+
+  # --- Forced Downgrades --- #
+  - megaparsec-6.5.0
+  - neat-interpolation-0.3.2.2  # Due to megaparsec 7
+
+  # --- Forced Upgrades --- #
+  - sbv-8.2
+
+  # --- Custom Pins --- #
   - git: https://github.com/kadena-io/thyme.git
     commit: 6ee9fcb026ebdb49b810802a981d166680d867c9
-  - sbv-8.1

tests/Analyze/Gen.hs

@@ -254,26 +254,29 @@ genCore BoundedBool = Gen.recursive Gen.choice [
        Gen.subtermM2 (genCore BoundedBool) (genCore BoundedBool) $ \x y ->
          mkBool $ Logical op [extract x, extract y]
   , do op <- Gen.element [Eq', Neq']
-       EType ty <- Gen.element
+       eTy <- Gen.element
          -- TODO?: keyset
          [EType SInteger, EType SDecimal, EType SBool, EType SStr, EType STime]
-       let aSize = case ty of
-             SInteger -> intSize
-             SDecimal -> decSize
-             SStr     -> strSize
-             SBool    -> BoundedBool
-             STime    -> BoundedTime
-             _        -> error "impossible"
-       Gen.subtermM2
-         (genCore (BoundedList aSize)) (genCore (BoundedList aSize)) $
-           \elst1 elst2 -> case (elst1, elst2) of
-             (Some (SList lty1) l1, Some (SList lty2) l2) ->
-               case singEq lty1 ty of
-                 Nothing   -> error "impossible"
-                 Just Refl -> case singEq lty2 ty of
-                   Nothing   -> error "impossible"
-                   Just Refl -> mkBool $ ListEqNeq ty op l1 l2
-             _ -> error (show (elst1, elst2))
+       case eTy of
+         EType ty -> do
+           let aSize = case ty of
+                 SInteger -> intSize
+                 SDecimal -> decSize
+                 SStr     -> strSize
+                 SBool    -> BoundedBool
+                 STime    -> BoundedTime
+                 _        -> error "impossible"
+           Gen.subtermM2
+             (genCore (BoundedList aSize)) (genCore (BoundedList aSize)) $
+               \elst1 elst2 -> case (elst1, elst2) of
+                 (Some (SList lty1) l1, Some (SList lty2) l2) ->
+                   case singEq lty1 ty of
+                     Nothing   -> error "impossible"
+                     Just Refl -> case singEq lty2 ty of
+                       Nothing   -> error "impossible"
+                       Just Refl -> mkBool $ ListEqNeq ty op l1 l2
+                 _ -> error (show (elst1, elst2))
+         _ -> error "impossible (we only generated `EType`s)"
   , Gen.subtermM (genCore BoundedBool) $ \x ->
       mkBool $ Logical NotOp [extract x]
   ]
@@ -449,9 +452,12 @@ genTermSpecific size@(BoundedString _len) = scale 2 $ Gen.choice
   , scale 4 $ do
        -- just generate literal format strings here so this tests something
        -- interesting
-       format        <- genFormat
-       Some STime t2 <- genTerm BoundedTime
-       pure $ Some SStr $ FormatTime (StrLit (showTimeFormat format)) t2
+       format   <- genFormat
+       someTime <- genTerm BoundedTime
+       case someTime of
+         Some STime t2 -> pure $
+           Some SStr $ FormatTime (StrLit (showTimeFormat format)) t2
+         _ -> error "impossible (we only generated `STime`s)"
   , let genHashableTerm = Gen.choice
           [ genTerm intSize
           , genTerm strSize
@@ -549,12 +555,15 @@ genTermSpecific' boundedTy = scale 8 $ Gen.choice
   --      Some ty tm <- genTerm boundedTy
   --      pure $ Some ty $ Sequence eTm tm
   [ do
-       Some SBool b <- genTerm BoundedBool
-       Some tyt1 t1 <- genTerm boundedTy
-       Some tyt2 t2 <- genTerm boundedTy
-       case singEq tyt1 tyt2 of
-         Just Refl -> pure $ Some tyt1 $ IfThenElse tyt1 b (Path 0, t1) (Path 0, t2)
-         Nothing   -> error "t1 and t2 must have the same type"
+       someBool <- genTerm BoundedBool
+       case someBool of
+         Some SBool b -> do
+           Some tyt1 t1 <- genTerm boundedTy
+           Some tyt2 t2 <- genTerm boundedTy
+           case singEq tyt1 tyt2 of
+             Just Refl -> pure $ Some tyt1 $ IfThenElse tyt1 b (Path 0, t1) (Path 0, t2)
+             Nothing   -> error "t1 and t2 must have the same type"
+         _ -> error "impossible (we only generated `SBool`s)"
   ]
 
 genType :: MonadGen m => m EType
@@ -589,11 +598,14 @@ safeGenAnyTerm = (do
 genFormatTime :: Gen (ETerm, GenState)
 genFormatTime = do
   format <- genFormat
-  (Some STime t2, gState) <- runReaderT
+  (someTm, gState) <- runReaderT
     (runStateT (genTerm BoundedTime) emptyGenState)
     genEnv
-  let etm = Some SStr $ FormatTime (StrLit (showTimeFormat format)) t2
-  pure (etm, gState)
+  case someTm of
+    Some STime tm -> do
+      let etm = Some SStr $ FormatTime (StrLit (showTimeFormat format)) tm
+      pure (etm, gState)
+    _ -> error "impossible (we only generated `STime`s)"
 
 genParseTime :: Gen (ETerm, GenState)
 genParseTime = do

tests/AnalyzePropertiesSpec.hs

@@ -57,28 +57,33 @@ testDualEvaluation' etm ty gState = do
       failure
 
     (Right pactVal, Right analyzeVal) -> do
-      Just etm' <- lift $ fromPactVal (EType ty) pactVal
-      case etm' of
-        Some ty' (CoreTerm (Lit pactSval)) -> do
-          Some ty'' (CoreTerm (Lit sval')) <- pure analyzeVal
-
-          -- compare results
-          case singEq ty' ty'' of
-            Just Refl
-              -- we only test bounded lists up to length 10. discard if the
-              -- pact list is too long.
-              -- TODO: this should only be considered a temporary fix. Done
-              -- properly we need to check all intermediate values.
-              | SList{} <- ty'
-              , length pactSval > 10
-              -> discard
-              | otherwise -> withEq ty' $ withShow ty' $ sval' === pactSval
-            Nothing   ->
-              if singEqB ty' (SList SAny) || singEqB ty'' (SList SAny)
-              then discard -- TODO: check this case
-              else EType ty' === EType ty'' -- this'll fail
-
-        Some _ (CoreTerm (LiteralObject _ _obj)) -> do
+      mEtm <- lift $ fromPactVal (EType ty) pactVal
+      case mEtm of
+        Just (Some ty' (CoreTerm (Lit pactSval))) -> do
+          someVal <- pure analyzeVal
+
+          case someVal of
+            Some ty'' (CoreTerm (Lit sval')) ->
+
+              -- compare results
+              case singEq ty' ty'' of
+                Just Refl
+                  -- we only test bounded lists up to length 10. discard if the
+                  -- pact list is too long.
+                  -- TODO: this should only be considered a temporary fix. Done
+                  -- properly we need to check all intermediate values.
+                  | SList{} <- ty'
+                  , length pactSval > 10
+                  -> discard
+                  | otherwise -> withEq ty' $ withShow ty' $ sval' === pactSval
+                Nothing   ->
+                  if singEqB ty' (SList SAny) || singEqB ty'' (SList SAny)
+                  then discard -- TODO: check this case
+                  else EType ty' === EType ty'' -- this'll fail
+
+            _ -> error $ "unexpected value (not literal): " ++ show someVal
+
+        Just (Some _ (CoreTerm (LiteralObject _ _obj))) -> do
           footnote "can't property test evaluation of objects"
           failure
 
@@ -96,8 +101,9 @@ prop_evaluation_time = property $ do
 
 prop_round_trip_type :: Property
 prop_round_trip_type = property $ do
-  ety@(EType ty) <- forAll genType
-  maybeTranslateType (reverseTranslateType ty) === Just ety
+  ety <- forAll genType
+  case ety of
+    EType ty -> maybeTranslateType (reverseTranslateType ty) === Just ety
 
 prop_round_trip_term :: Property
 prop_round_trip_term = property $ do