merging language-plutus-core-prop-test into language-plutus-core-test

IntersectMBO · Jul 10, 2020 · 85b095c · 85b095c
1 parent a0fd503
commit 85b095c
Show file tree

Hide file tree

Showing 3 changed files with 50 additions and 98 deletions.
diff --git a/language-plutus-core/language-plutus-core.cabal b/language-plutus-core/language-plutus-core.cabal
@@ -249,7 +249,7 @@ test-suite language-plutus-core-test
     import: lang
     type: exitcode-stdio-1.0
     main-is: Spec.hs
-    hs-source-dirs: test
+    hs-source-dirs: test, prop-test
     ghc-options: -threaded -rtsopts -with-rtsopts=-N
     other-modules:
         Evaluation.ApplyBuiltinName
@@ -266,6 +266,9 @@ test-suite language-plutus-core-test
         Pretty.Readable
         Check.Spec
         TypeSynthesis.Spec
+        Language.PlutusCore.Gen.Common
+        Language.PlutusCore.Gen.Type
+        Language.PlutusCore.PropTest
     default-language: Haskell2010
     build-depends:
         base -any,
@@ -274,11 +277,13 @@ test-suite language-plutus-core-test
         filepath -any,
         hedgehog -any,
         language-plutus-core -any,
+        lazy-search -any,        
         lens -any,
         mmorph -any,
         mtl -any,
         prettyprinter -any,
         serialise -any,
+        size-based -any,
         tasty -any,
         tasty-golden -any,
         tasty-hedgehog -any,
@@ -355,40 +360,6 @@ executable plc
         prettyprinter -any,
         optparse-applicative -any
 
-test-suite language-plutus-core-prop-test
-    type: exitcode-stdio-1.0
-    main-is: Spec.hs
-    hs-source-dirs: prop-test
-    other-modules: Language.PlutusCore.Gen.Common
-                 , Language.PlutusCore.Gen.Type
-                 , Language.PlutusCore.PropTest
-    default-language: Haskell2010
-    other-extensions: DeriveDataTypeable EmptyDataDeriving FlexibleContexts
-                      FlexibleInstances OverloadedStrings RecordWildCards
-                      ScopedTypeVariables TemplateHaskell
-    ghc-options: -threaded -O2 -Wall
-                 -Wincomplete-uni-patterns -Wincomplete-record-updates
-                 -Wredundant-constraints -Widentities
-    build-depends:
-        base -any,
-        language-plutus-core -any,
-        lazy-search -any,
-        mtl -any,
-        size-based -any,
-        tasty -any,
-        tasty-hunit -any,
-        testing-feat -any,
-        text -any
--- this stuff is from Wen's fork, commeting out for now - James
---    if flag(eventlog)
---        ghc-options: -eventlog
-
---    if (flag(development) && impl(ghc <8.4))
---        ghc-options: -Werror
-
-    if impl(ghc >=8.4)
-        ghc-options: -Wmissing-export-lists
-
 benchmark language-plutus-core-budgeting-bench
     import: lang
     type: exitcode-stdio-1.0

diff --git a/language-plutus-core/prop-test/Spec.hs b/language-plutus-core/prop-test/Spec.hs
diff --git a/language-plutus-core/test/Spec.hs b/language-plutus-core/test/Spec.hs
@@ -23,6 +23,8 @@ import           Language.PlutusCore.Generators
 import           Language.PlutusCore.Generators.AST                         as AST
 import           Language.PlutusCore.Generators.Interesting
 import           Language.PlutusCore.Pretty
+import           Language.PlutusCore.Normalize
+import           Language.PlutusCore.PropTest
 
 import           Codec.Serialise
 import           Control.Monad.Except
@@ -35,6 +37,7 @@ import           Test.Tasty
 import           Test.Tasty.Golden
 import           Test.Tasty.Hedgehog
 import           Test.Tasty.HUnit
+import           Data.Coolean
 
 main :: IO ()
 main = do
@@ -156,6 +159,13 @@ allTests plcFiles rwFiles typeFiles typeErrorFiles evalFiles = testGroup "all te
     , test_evaluation
     , test_normalizationCheck
     , Check.tests
+    -- NEAT tests
+    , testCase "kind checker for generated types is sound" $
+        testTyProp depth kind prop_checkKindSound
+    , testCase "normalization preserves kinds" $
+        testTyProp depth kind prop_normalizePreservesKind
+    , testCase "normalization for generated types is sound" $
+        testTyProp depth kind prop_normalizeTypeSound
     ]
 
 type TestFunction a = BSL.ByteString -> Either (Error DefaultUni a) T.Text
@@ -294,3 +304,37 @@ tests = testCase "example programs" $ fold
         fmt :: BSL.ByteString -> Either (ParseError AlexPosn) T.Text
         fmt = format cfg
         cfg = defPrettyConfigPlcClassic defPrettyConfigPlcOptions
+
+-- NEAT stuff
+
+
+depth :: Int
+depth = 10
+
+kind :: Kind ()
+kind = Type ()
+
+
+-- |Property: Kind checker for generated types is sound.
+prop_checkKindSound :: TyProp
+prop_checkKindSound k _ tyQ = isSafe $ do
+  ty <- liftQuote tyQ
+  checkKind defConfig () ty k
+
+-- |Property: Normalisation preserves kind.
+prop_normalizePreservesKind :: TyProp
+prop_normalizePreservesKind k _ tyQ = isSafe $ do
+  ty <- liftQuote tyQ
+  ty' <- unNormalized <$> normalizeType ty
+  checkKind defConfig () ty' k
+
+-- |Property: Normalisation for generated types is sound.
+prop_normalizeTypeSound :: TyProp
+prop_normalizeTypeSound k tyG tyQ = isSafe $ do
+  ty1 <- unNormalized <$> (normalizeType =<< liftQuote tyQ)
+  ty2 <- toClosedType k (normalizeTypeG tyG)
+  return (ty1 == ty2)
+
+-- |Check if the type/kind checker threw any errors.
+isSafe :: ExceptT (Error DefaultUni a) Quote a -> Cool
+isSafe = toCool . isRight . runQuote . runExceptT