Dependency injection to split up more of the big balls of hair in

constrained-generators

Author: MaximilianAlgehed

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Ledger.hs

@@ -45,7 +45,6 @@ import Test.Cardano.Ledger.Conway.Arbitrary ()
 
 import Cardano.Ledger.Conway (ConwayEra)
 import Constrained.API (
-  Specification (..),
   assert,
   constrained,
   constrained',
@@ -119,7 +118,7 @@ instance ExecSpecRule "LEDGER" ConwayEra where
 
   genExecContext = do
     ctx <- arbitrary
-    env <- genFromSpec TrueSpec
+    env <- genFromSpec mempty
     ConwayLedgerExecContext
       <$> arbitrary
       <*> genFromSpec (enactStateSpec ctx env)

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Ledgers.hs

@@ -10,7 +10,7 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Ledgers () where
 
 import Cardano.Ledger.Conway (ConwayEra)
 import Cardano.Ledger.Conway.Governance (EnactState)
-import Constrained.API (Specification (..))
+import Constrained.API ()
 import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
 import Test.Cardano.Ledger.Conformance (
   ExecSpecRule (..),
@@ -21,7 +21,7 @@ import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway ()
 instance ExecSpecRule "LEDGERS" ConwayEra where
   type ExecContext "LEDGERS" ConwayEra = EnactState ConwayEra
 
-  environmentSpec _ = TrueSpec
-  stateSpec _ _ = TrueSpec
-  signalSpec _ _ _ = TrueSpec
+  environmentSpec _ = mempty
+  stateSpec _ _ = mempty
+  signalSpec _ _ _ = mempty
   runAgdaRule env st sig = unComputationResult $ Agda.ledgersStep env st sig

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Epoch.hs

@@ -64,7 +64,7 @@ epochStateSpec epochNo = constrained $ \es ->
                       reify proposals (toInteger . proposalsSize) $ \ [var|sz|] ->
                         [ ifElse
                             (sz <=. 0)
-                            (expired ==. (Lit mempty))
+                            (expired ==. mempty)
                             (sizeOf_ expired <. sz)
                         ]
                     , forAll expired $ \ [var| gasId |] ->

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Ledger.hs

@@ -874,6 +874,7 @@ instance Typeable a => HasSimpleRep (THKD tag Identity a) where
   type SimpleRep (THKD tag Identity a) = a
   fromSimpleRep = THKD
   toSimpleRep (THKD a) = a
+
 instance
   ( IsNormalType a
   , Typeable tag

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/WitnessUniverse.hs

@@ -429,7 +429,7 @@ witShelleyTxCert univ =
       (caseOn txcert)
         ( branchW 5 $ \delegcert ->
             (caseOn delegcert)
-              (branch $ \_register -> TruePred)
+              (branch $ \_register -> TruePred :: Pred)
               (branch $ \unregisterAuthor -> satisfies unregisterAuthor (witCredSpec univ))
               (branch $ \delegateAuthor _ -> satisfies delegateAuthor (witCredSpec univ))
         )
@@ -440,7 +440,7 @@ witShelleyTxCert univ =
         )
         ( branchW 1 $ \genesiscert -> match genesiscert $ \authorkey _ _ -> satisfies authorkey (witKeyHashSpec univ)
         )
-        (branchW 1 $ \_mircert -> FalsePred (pure "NO MIR"))
+        (branchW 1 $ \_mircert -> FalsePred (pure "NO MIR") :: Pred)
 
 -- | Constrains all the Certificate Authors. Sometimes thay are keyHashes, and sometimes Credentials
 witConwayTxCert ::
@@ -455,7 +455,7 @@ witConwayTxCert univ =
             (caseOn delegcert)
               ( branch $ \registerAuthor deposit ->
                   (caseOn deposit)
-                    (branch $ \_ -> TruePred)
+                    (branch $ \_ -> TruePred :: Pred)
                     (branch $ \_ -> satisfies registerAuthor (witCredSpec univ))
               )
               (branch $ \unregisterAuthor _ -> satisfies unregisterAuthor (witCredSpec univ))

libs/constrained-generators/constrained-generators.cabal

@@ -19,9 +19,11 @@ source-repository head
 library
   exposed-modules:
     Constrained.API
+    Constrained.AbstractSyntax
     Constrained.Base
     Constrained.Conformance
     Constrained.Core
+    Constrained.DependencyInjection
     Constrained.Env
     Constrained.Examples
     Constrained.Examples.Basic
@@ -32,11 +34,13 @@ library
     Constrained.Examples.Map
     Constrained.Examples.Set
     Constrained.Examples.Tree
+    Constrained.FunctionSymbol
     Constrained.GenT
     Constrained.Generic
     Constrained.Graph
     Constrained.List
     Constrained.NumSpec
+    Constrained.PrettyUtils
     Constrained.Properties
     Constrained.Spec.Map
     Constrained.Spec.Set

libs/constrained-generators/src/Constrained/API.hs

@@ -5,6 +5,9 @@
 {-# LANGUAGE ViewPatterns #-}
 
 module Constrained.API (
+  PredD (..),
+  TermD (..),
+  SpecificationD (..),
   GenericallyInstantiated,
   Logic (..),
   Semantics (..),
@@ -13,12 +16,13 @@ module Constrained.API (
   NumSpec (..),
   MaybeBounded (..),
   NonEmpty ((:|)),
-  Specification (..),
-  Term (..),
+  Specification,
+  pattern TypeSpec,
+  Term,
   Fun (..),
   name,
   named,
-  Pred (..),
+  Pred,
   HasSpec (..),
   HasSimpleRep (..),
   OrdLike (..),
@@ -143,16 +147,15 @@ module Constrained.API (
 )
 where
 
+import Constrained.AbstractSyntax
 import Constrained.Base (
   Fun (..),
   GenericallyInstantiated,
   HasSpec (..),
   Logic (..),
-  Pred (..),
-  Semantics (..),
-  Specification (..),
-  Syntax (..),
-  Term (..),
+  Pred,
+  Specification,
+  Term,
   constrained,
   equalSpec,
   fromGeneric_,
@@ -164,6 +167,7 @@ import Constrained.Base (
   toGeneric_,
   pattern FromGeneric,
   pattern ToGeneric,
+  pattern TypeSpec,
   pattern Unary,
   pattern (:<:),
   pattern (:>:),
@@ -174,6 +178,7 @@ import Constrained.Conformance (
   satisfies,
  )
 import Constrained.Core (NonEmpty ((:|)))
+import Constrained.FunctionSymbol
 import Constrained.Generic (HasSimpleRep (..), Prod (..))
 import Constrained.NumSpec (
   MaybeBounded (..),