diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,6 +6,21 @@ ## UNRELEASED -## 1.0.0 -- 08-05-2025 +## 1.1.0 -- 2025-07-11 +### Added + +* Representation of datatype declarations and datatype types +* Generators for various flavors of data declaration and value type +* A "kind checker" which serves as a basic sanity check on datatype declarations ingested by the pipeline +* Base functor transformation machinery +* Tests for the base functor transformation +* Misc internal helpers to support the above functionality +* Ledger type definitions for use in the ASG +* Support for primops over data types +* Support for arity-six primops in the ASG + Initial version + +## 1.0.0 -- 2025-05-07 + diff --git a/covenant.cabal b/covenant.cabal --- a/covenant.cabal +++ b/covenant.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: covenant -version: 1.0.0 +version: 1.1.0 synopsis: Standalone IR for Cardano scripts. description: A library describing a call-by-push-value, Turner-total IR. Includes the ability to build up the IR programmatically. @@ -11,9 +11,9 @@ author: Koz Ross, Sean Hunter maintainer: koz@mlabs.city, sean@mlabs.city bug-reports: https://github.com/mlabs-haskell/covenant/issues -copyright: (C) MLabs 2024 +copyright: (C) MLabs 2024-2025 category: Covenant -tested-with: ghc ==9.8.4 || ==9.10.1 || ==9.12.1 +tested-with: ghc ==9.8.4 || ==9.10.2 || ==9.12.2 build-type: Simple extra-source-files: CHANGELOG.md @@ -76,11 +76,19 @@ -with-rtsopts=-N build-depends: + -- temporary, maybe, for debugging tests QuickCheck ==2.15.0.1, + containers >=0.6.8 && <0.8, covenant, + mtl >=2.3.1 && <3, + nonempty-vector ==0.2.4, + optics-core ==0.4.1.1, + prettyprinter ==1.7.1, tasty ==1.5.3, + tasty-expected-failure ==0.12.3, tasty-hunit ==0.10.2, tasty-quickcheck ==0.11.1, + vector ==0.13.2.0, common bench-lang import: lang @@ -94,6 +102,7 @@ Control.Monad.HashCons Covenant.ASG Covenant.Constant + Covenant.Data Covenant.DeBruijn Covenant.Index Covenant.Prim @@ -102,7 +111,11 @@ Covenant.Util other-modules: + Covenant.Internal.KindCheck + Covenant.Internal.Ledger + Covenant.Internal.PrettyPrint Covenant.Internal.Rename + Covenant.Internal.Strategy Covenant.Internal.Term Covenant.Internal.Type Covenant.Internal.Unification @@ -122,6 +135,7 @@ prettyprinter ==1.7.1, quickcheck-instances ==0.3.32, quickcheck-transformer ==0.3.1.2, + tasty-hunit ==0.10.2, text >=2.1.1 && <2.2, transformers >=0.6.1.0 && <0.7.0.0, vector ==0.13.2.0, @@ -135,6 +149,12 @@ main-is: Main.hs hs-source-dirs: test/renaming +test-suite base-functor + import: test-lang + type: exitcode-stdio-1.0 + main-is: Main.hs + hs-source-dirs: test/base-functor + test-suite type-applications import: test-lang type: exitcode-stdio-1.0 @@ -158,5 +178,17 @@ vector, hs-source-dirs: test/asg + +test-suite bb + import: test-lang + type: exitcode-stdio-1.0 + main-is: Main.hs + hs-source-dirs: test/bb + +test-suite kindcheck + import: test-lang + type: exitcode-stdio-1.0 + main-is: Main.hs + hs-source-dirs: test/kindcheck -- Benchmarks diff --git a/src/Covenant/ASG.hs b/src/Covenant/ASG.hs --- a/src/Covenant/ASG.hs +++ b/src/Covenant/ASG.hs @@ -35,6 +35,7 @@ ( Builtin1, Builtin2, Builtin3, + Builtin6, Lam, Force, Return @@ -51,38 +52,16 @@ CovenantError (..), ScopeInfo, ASGBuilder, - CovenantTypeError - ( BrokenIdReference, - ForceCompType, - ForceNonThunk, - ForceError, - ThunkValType, - ThunkError, - ApplyToValType, - ApplyToError, - ApplyCompType, - RenameFunctionFailed, - RenameArgumentFailed, - NoSuchArgument, - ReturnCompType, - LambdaResultsInValType, - LambdaResultsInNonReturn, - ReturnWrapsError, - ReturnWrapsCompType, - WrongReturnType, - UnificationError - ), - RenameError - ( InvalidAbstractionReference, - IrrelevantAbstraction, - UndeterminedAbstraction - ), + TypeAppError (..), + RenameError (..), + CovenantTypeError (..), -- ** Introducers arg, builtin1, builtin2, builtin3, + builtin6, force, ret, lam, @@ -92,6 +71,11 @@ app, -- ** Elimination + + -- *** Environment + defaultDatatypes, + + -- *** Function runASGBuilder, ) where @@ -113,13 +97,14 @@ runReaderT, ) import Covenant.Constant (AConstant, typeConstant) +import Covenant.Data (DatatypeInfo, mkDatatypeInfo) import Covenant.DeBruijn (DeBruijn, asInt) import Covenant.Index (Index, count0, intIndex) +import Covenant.Internal.KindCheck (checkEncodingArgs) +import Covenant.Internal.Ledger (ledgerTypes) import Covenant.Internal.Rename ( RenameError - ( InvalidAbstractionReference, - IrrelevantAbstraction, - UndeterminedAbstraction + ( InvalidAbstractionReference ), renameCompT, renameValT, @@ -134,6 +119,7 @@ ( Builtin1Internal, Builtin2Internal, Builtin3Internal, + Builtin6Internal, ForceInternal, LamInternal, ReturnInternal @@ -143,6 +129,7 @@ ApplyToError, ApplyToValType, BrokenIdReference, + EncodingError, ForceCompType, ForceError, ForceNonThunk, @@ -170,15 +157,32 @@ ( AbstractTy, CompT (CompT), CompTBody (CompTBody), + DataDeclaration, Renamed, + TyName, ValT (ThunkT), ) -import Covenant.Internal.Unification (checkApp) +import Covenant.Internal.Unification + ( TypeAppError + ( DatatypeInfoRenameFailed, + DoesNotUnify, + ExcessArgs, + ImpossibleHappened, + InsufficientArgs, + LeakingUnifiable, + LeakingWildcard, + NoBBForm, + NoDatatypeInfo + ), + checkApp, + ) import Covenant.Prim ( OneArgFunc, + SixArgFunc, ThreeArgFunc, TwoArgFunc, typeOneArgFunc, + typeSixArgFunc, typeThreeArgFunc, typeTwoArgFunc, ) @@ -201,6 +205,7 @@ over, preview, review, + view, (%), ) @@ -244,6 +249,28 @@ nodeAt :: Id -> ASG -> ASGNode nodeAt i (ASG (_, mappings)) = fromJust . Map.lookup i $ mappings +data ASGEnv = ASGEnv ScopeInfo (Map TyName (DatatypeInfo AbstractTy)) + +instance + (k ~ A_Lens, a ~ ScopeInfo, b ~ ScopeInfo) => + LabelOptic "scopeInfo" k ASGEnv ASGEnv a b + where + {-# INLINEABLE labelOptic #-} + labelOptic = + lens + (\(ASGEnv si _) -> si) + (\(ASGEnv _ dti) si -> ASGEnv si dti) + +instance + (k ~ A_Lens, a ~ Map TyName (DatatypeInfo AbstractTy), b ~ Map TyName (DatatypeInfo AbstractTy)) => + LabelOptic "datatypeInfo" k ASGEnv ASGEnv a b + where + {-# INLINEABLE labelOptic #-} + labelOptic = + lens + (\(ASGEnv _ dti) -> dti) + (\(ASGEnv si _) dti -> ASGEnv si dti) + -- | A tracker for scope-related information while building an ASG -- programmatically. Currently only tracks available arguments. -- @@ -295,6 +322,12 @@ pattern Builtin3 :: ThreeArgFunc -> CompNodeInfo pattern Builtin3 f <- Builtin3Internal f +-- | A Plutus primop with six arguments. +-- +-- @since 1.1.0 +pattern Builtin6 :: SixArgFunc -> CompNodeInfo +pattern Builtin6 f <- Builtin6Internal f + -- | Force a thunk back into the computation it wraps. -- -- @since 1.0.0 @@ -313,7 +346,7 @@ pattern Lam :: Id -> CompNodeInfo pattern Lam i <- LamInternal i -{-# COMPLETE Builtin1, Builtin2, Builtin3, Force, Return, Lam #-} +{-# COMPLETE Builtin1, Builtin2, Builtin3, Builtin6, Force, Return, Lam #-} -- | A compile-time literal of a flat builtin type. -- @@ -369,7 +402,7 @@ -- -- @since 1.0.0 newtype ASGBuilder (a :: Type) - = ASGBuilder (ReaderT ScopeInfo (ExceptT CovenantTypeError (HashConsT Id ASGNode Identity)) a) + = ASGBuilder (ReaderT ASGEnv (ExceptT CovenantTypeError (HashConsT Id ASGNode Identity)) a) deriving ( -- | @since 1.0.0 Functor, @@ -377,24 +410,38 @@ Applicative, -- | @since 1.0.0 Monad, - -- | @since 1.0.0 - MonadReader ScopeInfo, + -- | @since 1.1.0 + MonadReader ASGEnv, -- | @since 1.0.0 MonadError CovenantTypeError, -- | @since 1.0.0 MonadHashCons Id ASGNode ) - via ReaderT ScopeInfo (ExceptT CovenantTypeError (HashConsT Id ASGNode Identity)) + via ReaderT ASGEnv (ExceptT CovenantTypeError (HashConsT Id ASGNode Identity)) +-- | A standard collection of types required for almost any realistic script. +-- This includes non-\'flat\' builtin types (such as lists and pairs), as well +-- as all types required by the ledger (including types like @Maybe@). +-- +-- @since 1.1.0 +defaultDatatypes :: Map TyName (DatatypeInfo AbstractTy) +defaultDatatypes = foldMap go ledgerTypes + where + go :: DataDeclaration AbstractTy -> Map TyName (DatatypeInfo AbstractTy) + go decl = case mkDatatypeInfo decl of + Left err' -> error $ "Unexpected failure in default datatypes: " <> show err' + Right info -> Map.singleton (view #datatypeName decl) info + -- | Executes an 'ASGBuilder' to make a \'finished\' ASG. -- -- @since 1.0.0 runASGBuilder :: forall (a :: Type). + Map TyName (DatatypeInfo AbstractTy) -> ASGBuilder a -> Either CovenantError ASG -runASGBuilder (ASGBuilder comp) = - case runIdentity . runHashConsT . runExceptT . runReaderT comp . ScopeInfo $ Vector.empty of +runASGBuilder tyDict (ASGBuilder comp) = + case runIdentity . runHashConsT . runExceptT . runReaderT comp $ ASGEnv (ScopeInfo Vector.empty) tyDict of (result, bm) -> case result of Left err' -> Left . TypeError bm $ err' Right _ -> case Bimap.size bm of @@ -413,14 +460,14 @@ -- @since 1.0.0 arg :: forall (m :: Type -> Type). - (MonadError CovenantTypeError m, MonadReader ScopeInfo m) => + (MonadError CovenantTypeError m, MonadReader ASGEnv m) => DeBruijn -> Index "arg" -> m Arg arg scope index = do - let scopeAsInt = asInt scope + let scopeAsInt = review asInt scope let indexAsInt = review intIndex index - lookedUp <- asks (preview (#argumentInfo % ix scopeAsInt % ix indexAsInt)) + lookedUp <- asks (preview (#scopeInfo % #argumentInfo % ix scopeAsInt % ix indexAsInt)) case lookedUp of Nothing -> throwError . NoSuchArgument scope $ index Just t -> pure . Arg scope index $ t @@ -461,6 +508,18 @@ let node = ACompNode (typeThreeArgFunc bi) . Builtin3Internal $ bi refTo node +-- | As 'builtin1', but for six-argument primops. +-- +-- @since 1.1.0 +builtin6 :: + forall (m :: Type -> Type). + (MonadHashCons Id ASGNode m) => + SixArgFunc -> + m Id +builtin6 bi = do + let node = ACompNode (typeSixArgFunc bi) . Builtin6Internal $ bi + refTo node + -- | Given a reference to a thunk, turn it back into a computation. Will fail if -- the reference isn't a thunk. -- @@ -513,13 +572,13 @@ -- @since 1.0.0 lam :: forall (m :: Type -> Type). - (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ScopeInfo m) => + (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) => CompT AbstractTy -> m Id -> m Id lam expectedT@(CompT _ (CompTBody xs)) bodyComp = do let (args, resultT) = NonEmpty.unsnoc xs - bodyId <- local (over #argumentInfo (Vector.cons args)) bodyComp + bodyId <- local (over (#scopeInfo % #argumentInfo) (Vector.cons args)) bodyComp bodyNode <- lookupRef bodyId case bodyNode of Nothing -> throwError . BrokenIdReference $ bodyId @@ -561,7 +620,7 @@ -- @since 1.0.0 app :: forall (m :: Type -> Type). - (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) => + (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) => Id -> Vector Ref -> m Id @@ -572,11 +631,11 @@ Left err' -> throwError . RenameFunctionFailed fT $ err' Right renamedFT -> do renamedArgs <- traverse renameArg argRefs - case checkApp renamedFT . Vector.toList $ renamedArgs of - Left err' -> throwError . UnificationError $ err' - Right result -> do - let restored = undoRename result - refTo . AValNode restored . AppInternal fId $ argRefs + tyDict <- asks (view #datatypeInfo) + result <- either (throwError . UnificationError) pure $ checkApp tyDict renamedFT (Vector.toList renamedArgs) + let restored = undoRename result + checkEncodingWithInfo tyDict restored + refTo . AValNode restored . AppInternal fId $ argRefs ValNodeType t -> throwError . ApplyToValType $ t ErrorNodeType -> throwError ApplyToError @@ -611,7 +670,8 @@ renameArg :: forall (m :: Type -> Type). (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) => - Ref -> m (Maybe (ValT Renamed)) + Ref -> + m (Maybe (ValT Renamed)) renameArg r = typeRef r >>= \case CompNodeType t -> throwError . ApplyCompType $ t @@ -619,3 +679,13 @@ Left err' -> throwError . RenameArgumentFailed t $ err' Right renamed -> pure . Just $ renamed ErrorNodeType -> pure Nothing + +checkEncodingWithInfo :: + forall (a :: Type) (m :: Type -> Type). + (MonadError CovenantTypeError m) => + Map TyName (DatatypeInfo a) -> + ValT AbstractTy -> + m () +checkEncodingWithInfo tyDict valT = case checkEncodingArgs (view (#originalDecl % #datatypeEncoding)) tyDict valT of + Left encErr -> throwError $ EncodingError encErr + Right {} -> pure () diff --git a/src/Covenant/Constant.hs b/src/Covenant/Constant.hs --- a/src/Covenant/Constant.hs +++ b/src/Covenant/Constant.hs @@ -49,7 +49,6 @@ Show ) --- | @since 1.0.0 instance Arbitrary AConstant where {-# INLINEABLE arbitrary #-} arbitrary = @@ -73,7 +72,8 @@ -- @since 1.0.0 typeConstant :: forall (a :: Type). - AConstant -> ValT a + AConstant -> + ValT a typeConstant = BuiltinFlat . \case AUnit -> UnitT diff --git a/src/Covenant/Data.hs b/src/Covenant/Data.hs new file mode 100644 --- /dev/null +++ b/src/Covenant/Data.hs @@ -0,0 +1,417 @@ +{-# LANGUAGE ViewPatterns #-} + +-- | +-- Module: Covenant.Data +-- Copyright: (C) MLabs 2025 +-- License: Apache 2.0 +-- Maintainer: koz@mlabs.city, sean@mlabs.city +-- +-- Information about datatype definitions, and various ways to interact with +-- them. Most of the useful functionality is in 'DatatypeInfo' and its optics. +-- +-- = Note +-- +-- Some of the low-level functions in the module make use of @ScopeBoundary@. +-- This is mostly an artifact of needing this for tests; if you ever need their +-- functionality, assume that the only sensible value is @0@, which will work +-- via its overloaded number syntax. +-- +-- @since 1.1.0 +module Covenant.Data + ( -- * Types + BBFError (..), + DatatypeInfo (..), + + -- * Functions + + -- ** Datatype-related + mkDatatypeInfo, + allComponentTypes, + mkBBF, + noPhantomTyVars, + + -- ** Lower-level + mkBaseFunctor, + isRecursiveChildOf, + hasRecursive, + everythingOf, + ) +where + +import Control.Monad.Except (MonadError (throwError)) +import Control.Monad.Reader (MonadReader (ask, local), MonadTrans (lift), Reader, runReader) +import Control.Monad.Trans.Except (ExceptT, runExceptT) +import Covenant.DeBruijn (DeBruijn (S, Z), asInt) +import Covenant.Index (Count, Index, count0, intCount, intIndex) +import Covenant.Internal.PrettyPrint (ScopeBoundary (ScopeBoundary)) +import Covenant.Internal.Type + ( AbstractTy (BoundAt), + CompT (CompT), + CompTBody (CompTBody), + Constructor (Constructor), + ConstructorName (ConstructorName), + DataDeclaration (DataDeclaration, OpaqueData), + TyName (TyName), + ValT (Abstraction, BuiltinFlat, Datatype, ThunkT), + ) +import Data.Bitraversable (bisequence) +import Data.Kind (Type) +import Data.Maybe (fromJust) +import Data.Set (Set) +import Data.Set qualified as Set +import Data.Vector qualified as V +import Data.Vector.NonEmpty qualified as NEV +import Optics.Core (A_Lens, LabelOptic (labelOptic), folded, lens, preview, review, toListOf, view, (%), _2) +import Optics.Indexed.Core (A_Fold) + +-- | All possible errors that could arise when constructing a Boehm-Berrarducci +-- form. +-- +-- @since 1.1.0 +data BBFError + = -- | The type is recursive in a prohibited way. Typically, this means + -- contravariant recursion. This gives the type name and the invalid + -- recursive constructor argument. + -- + -- @since 1.1.0 + InvalidRecursion TyName (ValT AbstractTy) + deriving stock + ( -- | @since 1.1.0 + Show, + -- | @since 1.1.0 + Eq + ) + +-- | Contains essential information about datatype definitions. Most of the +-- time, you want to use this type via its optics, rather than directly. +-- +-- In pretty much any case imaginable, the @var@ type variable will be one of +-- 'AbstractTy' or 'Renamed'. +-- +-- @since 1.1.0 +data DatatypeInfo (var :: Type) + = DatatypeInfo + { _originalDecl :: DataDeclaration var, + _baseFunctorStuff :: Maybe (DataDeclaration var, ValT var), + -- NOTE: The ONLY type that won't have a BB form is `Void` (or something isomorphic to it) + _bbForm :: Maybe (ValT var) + } + deriving stock + ( -- | @since 1.1.0 + Eq, + -- | @since 1.1.0 + Show + ) + +-- | The original declaration of the data type. +-- +-- @since 1.1.0 +instance + (k ~ A_Lens, a ~ DataDeclaration var, b ~ DataDeclaration var) => + LabelOptic "originalDecl" k (DatatypeInfo var) (DatatypeInfo var) a b + where + {-# INLINEABLE labelOptic #-} + labelOptic = + lens + (\(DatatypeInfo ogDecl _ _) -> ogDecl) + (\(DatatypeInfo _ b c) ogDecl -> DatatypeInfo ogDecl b c) + +-- | The base functor for this data type, if it exists. Types which are not +-- self-recursive lack base functors. +-- +-- @since 1.1.0 +instance + (k ~ A_Lens, a ~ Maybe (DataDeclaration var, ValT var), b ~ Maybe (DataDeclaration var, ValT var)) => + LabelOptic "baseFunctor" k (DatatypeInfo var) (DatatypeInfo var) a b + where + {-# INLINEABLE labelOptic #-} + labelOptic = + lens + (\(DatatypeInfo _ baseF _) -> baseF) + (\(DatatypeInfo a _ c) baseF -> DatatypeInfo a baseF c) + +-- | The Boehm-Berrarducci form of this type, if it exists. Types with no +-- constructors (that is, types without inhabitants) lack Boehm-Berrarducci +-- forms. +-- +-- @since 1.1.0 +instance + (k ~ A_Lens, a ~ Maybe (ValT var), b ~ Maybe (ValT var)) => + LabelOptic "bbForm" k (DatatypeInfo var) (DatatypeInfo var) a b + where + {-# INLINEABLE labelOptic #-} + labelOptic = + lens + (\(DatatypeInfo _ _ bb) -> bb) + (\(DatatypeInfo a b _) bb -> DatatypeInfo a b bb) + +-- | The base functor Boehm-Berrarducci form of this type, if it exists. A type +-- must have both a base functor and a Boehm-Berrarducci form to have a base +-- functor Boehm-Berrarducci form. In other words, they must have at least one +-- constructor and be self-recursive. +-- +-- @since 1.1.0 +instance + (k ~ A_Fold, a ~ ValT var, b ~ ValT var) => + LabelOptic "bbBaseF" k (DatatypeInfo var) (DatatypeInfo var) a b + where + {-# INLINEABLE labelOptic #-} + labelOptic = #baseFunctor % folded % _2 + +-- | Given a declaration of a datatype, either produce its datatype info, or +-- fail. +-- +-- @since 1.1.0 +mkDatatypeInfo :: DataDeclaration AbstractTy -> Either BBFError (DatatypeInfo AbstractTy) +mkDatatypeInfo decl = DatatypeInfo decl <$> baseFStuff <*> mkBBF decl + where + baseFStuff :: Either BBFError (Maybe (DataDeclaration AbstractTy, ValT AbstractTy)) + baseFStuff = + let baseFDecl = runReader (mkBaseFunctor decl) 0 + baseBBF = case baseFDecl of + Nothing -> Right Nothing + Just d -> mkBBF d + in (bisequence . (baseFDecl,) <$> baseBBF) + +-- | Returns all datatype constructors used as any argument to the datatype +-- defined by the first argument. +-- +-- @since 1.1.0 +allComponentTypes :: DataDeclaration AbstractTy -> [ValT AbstractTy] +allComponentTypes = toListOf (#datatypeConstructors % folded % #constructorArgs % folded) + +-- | Constructs a base functor from a suitable data declaration, returning +-- 'Nothing' if the input is not a recursive type. +-- +-- @since 1.1.0 +mkBaseFunctor :: DataDeclaration AbstractTy -> Reader ScopeBoundary (Maybe (DataDeclaration AbstractTy)) +mkBaseFunctor OpaqueData {} = pure Nothing +mkBaseFunctor (DataDeclaration tn numVars ctors strat) = do + anyRecComponents <- or <$> traverse (hasRecursive tn) allCtorArgs + if null ctors || not anyRecComponents + then pure Nothing + else do + baseCtors <- traverse mkBaseCtor ctors + pure . Just $ DataDeclaration baseFName baseFNumVars baseCtors strat + where + baseFName :: TyName + baseFName = case tn of + TyName tyNameInner -> TyName (tyNameInner <> "_F") + baseFNumVars :: Count "tyvar" + baseFNumVars = fromJust . preview intCount $ review intCount numVars + 1 + -- The argument position of the new type variable parameter (typically `r`). + -- A count represents the number of variables, but indices for those variables start at 0, + -- so an additional tyvar will always have an index == the old count + rIndex :: Index "tyvar" + rIndex = fromJust . preview intIndex $ review intCount numVars + -- Replace recursive children with a DeBruijn index & position index that points at the top-level binding context + -- (technically the top level binding context is the ONLY admissable binding context if we forbid higher-rank types, + -- but we still have to regard a computation type that binds 0 variables as having a scope boundary) + replaceWithR :: ValT AbstractTy -> Reader ScopeBoundary (ValT AbstractTy) + replaceWithR vt = + isRecursive vt >>= \case + True -> do + ScopeBoundary here <- ask -- this should be the distance from the initial binding context (which is what we want) + let db = fromJust $ preview asInt here + pure $ Abstraction (BoundAt db rIndex) + False -> pure vt + -- TODO: This should be refactored with `mapMValT`, which I will do after I write it :P + replaceAllRecursive :: ValT AbstractTy -> Reader ScopeBoundary (ValT AbstractTy) + replaceAllRecursive = \case + abst@Abstraction {} -> pure abst + bif@BuiltinFlat {} -> pure bif + ThunkT (CompT cnt (CompTBody compTargs)) -> + local (+ 1) $ ThunkT . CompT cnt . CompTBody <$> traverse replaceAllRecursive compTargs + Datatype tx args -> (replaceWithR . Datatype tx =<< traverse replaceAllRecursive args) + mkBaseCtor :: Constructor AbstractTy -> Reader ScopeBoundary (Constructor AbstractTy) + mkBaseCtor (Constructor ctorNm ctorArgs) = Constructor (baseFCtorName ctorNm) <$> traverse replaceAllRecursive ctorArgs + where + baseFCtorName :: ConstructorName -> ConstructorName + baseFCtorName (ConstructorName nm) = ConstructorName (nm <> "_F") + allCtorArgs :: [ValT AbstractTy] + allCtorArgs = concatMap (V.toList . view #constructorArgs) ctors + -- This tells us whether the ValT *is* a recursive child of the parent type + isRecursive :: ValT AbstractTy -> Reader ScopeBoundary Bool + isRecursive = isRecursiveChildOf tn + +-- | Returns 'True' if the second argument is a recursive child of the datatype +-- named by the first argument. +-- +-- @since 1.1.0 +isRecursiveChildOf :: TyName -> ValT AbstractTy -> Reader ScopeBoundary Bool +isRecursiveChildOf tn = \case + Datatype tn' args + | tn' == tn -> V.ifoldM checkArgsIsRec' True args + | otherwise -> pure False + _ -> pure False + where + checkArgsIsRec' :: Bool -> Int -> ValT AbstractTy -> Reader ScopeBoundary Bool + checkArgsIsRec' acc n = \case + Abstraction (BoundAt db varIx) -> do + ScopeBoundary here <- ask + let dbInt = review asInt db + -- Explanation: A component ValT is only a recursive instance of the parent type if + -- the DeBruijn index of its type variables points to Z (and the other conditions obtain) + if dbInt - here == 0 && review intIndex varIx == n + then pure acc + else pure False + _ -> pure False + +-- | Determines whether the type represented by the second argument and named by +-- the first requires a base functor. +-- +-- @since 1.1.0 +hasRecursive :: TyName -> ValT AbstractTy -> Reader ScopeBoundary Bool +hasRecursive tn = \case + Abstraction {} -> pure False + BuiltinFlat {} -> pure False + -- NOTE: This assumes that we've forbidden higher rank arguments to constructors (i.e. we can ignore the scope here) + ThunkT (CompT _ (CompTBody (NEV.toList -> compTArgs))) -> local (+ 1) $ do + or <$> traverse (hasRecursive tn) compTArgs + dt@(Datatype _ args) -> do + thisTypeIsRecursive <- isRecursiveChildOf tn dt + aComponentIsRecursive <- or <$> traverse (hasRecursive tn) args + pure $ thisTypeIsRecursive || aComponentIsRecursive + +-- | Constructs a base functor Boehm-Berrarducci form for the given datatype. +-- Returns 'Nothing' if the type is not self-recursive. +-- +-- @since 1.1.0 +mkBBF :: DataDeclaration AbstractTy -> Either BBFError (Maybe (ValT AbstractTy)) +mkBBF decl = sequence . runExceptT $ mkBBF' decl + +-- | Verifies that all type variables declared by the given datatype have a +-- corresponding value in some \'arm\'. +-- +-- @since 1.1.0 +noPhantomTyVars :: DataDeclaration AbstractTy -> Bool +noPhantomTyVars OpaqueData {} = True +noPhantomTyVars decl@(DataDeclaration _ numVars _ _) = + let allChildren = allComponentTypes decl + allResolved = Set.unions $ runReader (traverse allResolvedTyVars' allChildren) 0 + indices :: [Index "tyvar"] + indices = fromJust . preview intIndex <$> [0 .. (review intCount numVars - 1)] + declaredTyVars = BoundAt Z <$> indices + in all (`Set.member` allResolved) declaredTyVars + +-- | Collect all (other) value types a given value type refers to. +-- +-- @since 1.1.0 +everythingOf :: forall (a :: Type). (Ord a) => ValT a -> Set (ValT a) +everythingOf = foldValT (flip Set.insert) Set.empty + +-- Helpers + +{- NOTE: For the purposes of base functor transformation, we follow the pattern established by Edward Kmett's + 'recursion-schemes' library. That is, we regard a datatype as "recursive" if and only if at least one + argument to a constructor contains "the exact same thing as we find to the left of the =". Dunno how to + describe it more precisely, but the general idea is that things like these ARE recursive for us: + + data Foo = End Int | More Foo Int -- contains 'Foo' as a ctor arg + + data Bar a = Beep | Boom a (Bar a) -- contains 'Bar a' + + but things like this are NOT recursive by our reckoning (even though in some sense they might be considered as such): + + data FunL a b = Done b | Go (FunL b a) a -- `FunL b a` isn't `FunL a b` so it's not literally recursive + + Obviously we're working with DeBruijn indices so the letters are more-or-less fictitious, but hopefully + these examples nonetheless get the point across. +-} + +-- TODO: Rewrite this as `mapMValT`. The change to a `Reader` below makes this unusable, but we can +-- write the non-monadic version as a special case of the monadic version and it is *highly* likely +-- we will need both going forward. +mapValT :: forall (a :: Type). (ValT a -> ValT a) -> ValT a -> ValT a +mapValT f = \case + -- for terminal nodes we just apply the function + absr@(Abstraction {}) -> f absr + bif@BuiltinFlat {} -> f bif + -- For CompT and Datatype we apply the function to the components and then to the top level + ThunkT (CompT cnt (CompTBody compTargs)) -> f (ThunkT $ CompT cnt (CompTBody (mapValT f <$> compTargs))) + Datatype tn args -> f $ Datatype tn (mapValT f <$> args) + +-- Did in fact need it +foldValT :: forall (a :: Type) (b :: Type). (b -> ValT a -> b) -> b -> ValT a -> b +foldValT f e = \case + absr@(Abstraction {}) -> f e absr + bif@(BuiltinFlat {}) -> f e bif + thk@(ThunkT (CompT _ (CompTBody compTArgs))) -> + let e' = NEV.foldl' f e compTArgs + in f e' thk + dt@(Datatype _ args) -> + let e' = V.foldl' f e args + in f e' dt + +allResolvedTyVars' :: ValT AbstractTy -> Reader Int (Set AbstractTy) +allResolvedTyVars' = \case + Abstraction (BoundAt db argpos) -> do + here <- ask + let db' = fromJust . preview asInt $ review asInt db - here + pure . Set.singleton $ BoundAt db' argpos + ThunkT (CompT _ (CompTBody nev)) -> local (+ 1) $ do + Set.unions <$> traverse allResolvedTyVars' nev + BuiltinFlat {} -> pure Set.empty + Datatype _ args -> Set.unions <$> traverse allResolvedTyVars' args + +incAbstractionDB :: ValT AbstractTy -> ValT AbstractTy +incAbstractionDB = mapValT $ \case + Abstraction (BoundAt db indx) -> + let db' = fromJust . preview asInt $ review asInt db + 1 + in Abstraction (BoundAt db' indx) + other -> other + +-- Only returns `Nothing` if there are no Constructors or the type is Opaque +mkBBF' :: DataDeclaration AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy) +mkBBF' OpaqueData {} = lift Nothing +mkBBF' (DataDeclaration tn numVars ctors _) + | V.null ctors = lift Nothing + | otherwise = do + ctors' <- traverse mkBBCtor ctors + lift $ ThunkT . CompT bbfCount . CompTBody . flip NEV.snoc topLevelOut <$> NEV.fromVector ctors' + where + topLevelOut = Abstraction $ BoundAt Z outIx + + outIx :: Index "tyvar" + outIx = fromJust . preview intIndex $ review intCount numVars + + bbfCount = fromJust . preview intCount $ review intCount numVars + 1 + + mkBBCtor :: Constructor AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy) + mkBBCtor (Constructor _ args) + | V.null args = pure topLevelOut + | otherwise = do + elimArgs <- fmap incAbstractionDB <$> traverse fixArg args + elimArgs' <- lift . NEV.fromVector $ elimArgs + let out = Abstraction $ BoundAt (S Z) outIx + pure . ThunkT . CompT count0 . CompTBody . flip NEV.snoc out $ elimArgs' + + fixArg :: ValT AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy) + fixArg arg = do + let isDirectRecursiveTy = runReader (isRecursiveChildOf tn arg) 0 + if isDirectRecursiveTy + then pure $ Abstraction (BoundAt Z outIx) + else case arg of + Datatype tn' dtArgs + | tn == tn' -> throwError $ InvalidRecursion tn arg + | otherwise -> do + dtArgs' <- traverse fixArg dtArgs + pure . Datatype tn' $ dtArgs' + _ -> pure arg + +{- Note (Sean, 14/05/25): Re DeBruijn indices: + + - None of the existing variable DeBruijn or position indices change at all b/c the binding context of the + `forall` we're introducing replaces the binding context of the datatype declaration and only extends it. + + - The only special thing we have to keep track of is the (DeBruijn) index of the `out` variable, but this doesn't require + any fancy scope tracking: It will always be Z for the top-level result and `S Z` wherever it occurs in a + transformed constructor. It won't ever occur any "deeper" than that (because we don't nest these, and a constructor gets exactly one + `out`) + + - Actually this is slightly false, we need to "bump" all of the indices inside constructor arms by one (because + they now occur within a Thunk), but after that bump everything is stable as indicated above. +-} + +{- Here for lack of a better place to put it (has to be available to Unification and ASG) +-} diff --git a/src/Covenant/DeBruijn.hs b/src/Covenant/DeBruijn.hs --- a/src/Covenant/DeBruijn.hs +++ b/src/Covenant/DeBruijn.hs @@ -19,6 +19,7 @@ import Data.List.NonEmpty (NonEmpty) import Data.Semigroup (Semigroup (sconcat, stimes), Sum (Sum)) import Data.Word (Word32) +import Optics.Core (Prism', prism) import Test.QuickCheck (Arbitrary) -- | A DeBruijn index. @@ -75,13 +76,12 @@ {-# COMPLETE Z, S #-} --- | Convert a DeBruijn index into a (non-negative) 'Int'. +-- | Construct a DeBruijn from an Int, or deconstruct a Debruijn into an Int -- --- @since 1.0.0 -asInt :: DeBruijn -> Int -asInt (DeBruijn i) = fromIntegral i +-- @since 1.1.0 +asInt :: Prism' Int DeBruijn +asInt = prism (\(DeBruijn x) -> fromIntegral x) (\x -> if x >= 0 then Right . DeBruijn $ fromIntegral x else Left x) -- Helpers - reduce :: DeBruijn -> Maybe DeBruijn reduce (DeBruijn x) = DeBruijn (x - 1) <$ guard (x > 0) diff --git a/src/Covenant/Internal/KindCheck.hs b/src/Covenant/Internal/KindCheck.hs new file mode 100644 --- /dev/null +++ b/src/Covenant/Internal/KindCheck.hs @@ -0,0 +1,263 @@ +-- | This module define a "kind-checking" pass. This requires some explanation, since we don't have +-- an *explicit* notion of kinds in Covenant: +-- +-- With the addition of type constructors for datatypes into ValT comes a new set of things that can +-- "go wrong". In particular: +-- - Someone may try to use a type constructor which is not defined anywhere +-- - A type may be applied to an incorrect number of arguments +-- - The "count" - the number of bound tyvars in the `ValT.Datatype` representation - may be incorrect (i.e. inconsistent with the count in the declaration) +-- +-- The checks to detect these errors are entirely independent from the checks performed during typechecking or renaming, so we do them in a separate pass. +module Covenant.Internal.KindCheck + ( checkDataDecls, + checkValT, + KindCheckError (..), + EncodingArgErr (..), + cycleCheck, + checkEncodingArgs, + ) +where + +import Control.Monad (unless) +import Control.Monad.Except (ExceptT, MonadError (throwError), runExceptT) +import Control.Monad.Reader + ( MonadReader (local), + ReaderT (ReaderT), + asks, + runReaderT, + ) +import Covenant.Data (everythingOf) +import Covenant.Index (Count, intCount) +import Covenant.Internal.Strategy + ( DataEncoding (SOP), + ) +import Covenant.Internal.Type + ( AbstractTy, + CompT (CompT), + CompTBody (CompTBody), + Constructor (Constructor), + DataDeclaration (DataDeclaration, OpaqueData), + TyName, + ValT (Abstraction, BuiltinFlat, Datatype, ThunkT), + checkStrategy, + datatype, + ) +import Data.Foldable (traverse_) +import Data.Functor.Identity (Identity, runIdentity) +import Data.Kind (Type) +import Data.Map.Strict (Map) +import Data.Map.Strict qualified as M +import Data.Maybe (mapMaybe) +import Data.Set (Set) +import Data.Set qualified as Set +import Data.Vector (Vector) +import Data.Vector qualified as V +import Optics.Core (A_Lens, LabelOptic (labelOptic), folded, lens, preview, review, to, toListOf, view, (%)) + +{- TODO: Explicitly separate the kind checker into two check functions: + - One which kind checks `ValT`s to ensure: + 1. All TyCons in the ValT exist + 2. All TyCons in the ValT have the correct arity + + - One which checks *datatype declarations* to ensure: + 1. Everything satisfies the above ValT checks + 2. No thunk arguments to ctors! + 3. No mutual recursion (cycles) +-} + +data KindCheckError + = UnknownType TyName + | IncorrectNumArgs TyName (Count "tyvar") (Vector (ValT AbstractTy)) -- first is expected (from the decl), second is actual + | ThunkConstructorArg (CompT AbstractTy) -- no polymorphic function args to ctors + | MutualRecursionDetected (Set TyName) + | InvalidStrategy TyName + | EncodingMismatch (EncodingArgErr AbstractTy) + deriving stock (Show, Eq) + +newtype KindCheckContext a = KindCheckContext (Map TyName (DataDeclaration a)) + +instance + (k ~ A_Lens, a ~ Map TyName (DataDeclaration c), b ~ Map TyName (DataDeclaration c)) => + LabelOptic "kindCheckContext" k (KindCheckContext c) (KindCheckContext c) a b + where + {-# INLINEABLE labelOptic #-} + labelOptic = + lens + (\(KindCheckContext x) -> x) + (\(KindCheckContext _) x' -> KindCheckContext x') + +newtype KindCheckM t a = KindCheckM (ReaderT (KindCheckContext t) (ExceptT KindCheckError Identity) a) + deriving + (Functor, Applicative, Monad, MonadReader (KindCheckContext t), MonadError KindCheckError) + via (ReaderT (KindCheckContext t) (ExceptT KindCheckError Identity)) + +runKindCheckM :: forall (t :: Type) (a :: Type). Map TyName (DataDeclaration t) -> KindCheckM t a -> Either KindCheckError a +runKindCheckM dtypes (KindCheckM act) = runIdentity . runExceptT $ runReaderT act (KindCheckContext dtypes) + +lookupDeclaration :: forall (t :: Type). TyName -> KindCheckM t (DataDeclaration t) +lookupDeclaration tn = do + types <- asks (view #kindCheckContext) + case M.lookup tn types of + Nothing -> throwError $ UnknownType tn + Just decl -> pure decl + +{- This sanity checks datatype declarations using the criteria enumerated above. +-} + +-- | Checks that all the data declarations in the argument \'make sense\'. +-- Specifically: +-- +-- * The strategy declared for the datatype is valid for it +-- * There are no mutually recursive datatype declarations +-- * Constructor arguments are not thunks +-- * The number of type variables in any constructor isn't greater than we +-- expect +-- +-- @since 1.1.0 +checkDataDecls :: Map TyName (DataDeclaration AbstractTy) -> Either KindCheckError () +checkDataDecls decls = runKindCheckM decls $ traverse_ checkDataDecl (M.elems decls) + +checkDataDecl :: DataDeclaration AbstractTy -> KindCheckM AbstractTy () +checkDataDecl OpaqueData {} = pure () +checkDataDecl decl@(DataDeclaration tn _ ctors _) = do + unless (checkStrategy decl) $ throwError (InvalidStrategy tn) + cycleCheck' mempty decl + let allCtorArgs = view #constructorArgs =<< ctors + traverse_ (checkKinds CheckDataDecl) allCtorArgs + checkEncodingArgsInDataDecl decl + +data KindCheckMode = CheckDataDecl | CheckValT + deriving stock (Show, Eq, Ord) + +-- This isn't really a "kind checker" in the normal sense and just checks that none of the three failure conditions above obtain +checkKinds :: KindCheckMode -> ValT AbstractTy -> KindCheckM AbstractTy () +checkKinds mode = \case + Abstraction _ -> pure () + ThunkT compT@(CompT _ (CompTBody nev)) + | mode == CheckDataDecl -> throwError $ ThunkConstructorArg compT + | otherwise -> traverse_ (checkKinds mode) nev + BuiltinFlat {} -> pure () + Datatype tn args -> + lookupDeclaration tn >>= \case + OpaqueData {} -> pure () + DataDeclaration _ numVars _ _ -> do + let numArgsActual = V.length args + numArgsExpected = review intCount numVars + unless (numArgsActual == numArgsExpected) $ throwError (IncorrectNumArgs tn numVars args) + traverse_ (checkKinds mode) args + +-- | This is for checking type annotations in the ASG, *not* datatypes +checkValT :: Map TyName (DataDeclaration AbstractTy) -> ValT AbstractTy -> Maybe KindCheckError +checkValT dtypes = either Just (const Nothing) . runKindCheckM dtypes . checkKinds CheckValT + +-- | Verifies that no types in the argument are mutually recursive. +-- +-- @since 1.1.0 +cycleCheck :: forall (a :: Type). (Ord a) => Map TyName (DataDeclaration a) -> Maybe KindCheckError +cycleCheck decls = either Just (const Nothing) $ runKindCheckM decls go + where + go = + local (\_ -> KindCheckContext decls) $ + traverse_ (cycleCheck' mempty) =<< asks (view (#kindCheckContext % to M.elems)) + +{- This is a bit odd b/c we don't want to fail for auto-recursive types, so we need to be careful + *not* to mark the current decl being examined as "visited" until we've "descended" into the dependencies + (I think?) +-} +cycleCheck' :: forall (a :: Type). (Ord a) => Set TyName -> DataDeclaration a -> KindCheckM a () +cycleCheck' _ OpaqueData {} = pure () +cycleCheck' visited (DataDeclaration tn _ ctors _) = traverse_ (checkCtor visited tn) ctors + where + checkCtor :: Set TyName -> TyName -> Constructor a -> KindCheckM a () + checkCtor vs tn' (Constructor _ args) = do + let allComponents = Set.toList . Set.unions $ everythingOf <$> V.toList args + -- every type constructor in any part of a constructor arg, *except* the tycon of the decl + -- we're examining, since autorecursion is fine/necessary + allTyCons = Set.filter (/= tn') . Set.fromList . mapMaybe (fmap fst . preview datatype) $ allComponents + alreadyVisitedArgTys = Set.intersection allTyCons vs + unless (null alreadyVisitedArgTys) $ throwError (MutualRecursionDetected alreadyVisitedArgTys) + let newVisited = Set.insert tn' vs + nextRound <- traverse lookupDeclaration (Set.toList allTyCons) + traverse_ (cycleCheck' newVisited) nextRound + +{- Arguably the closest thing to a real kind checker in the module. + + Checks whether the arguments to type constructors (ValT 'Datatype's) conform with their encoding. + +-} + +-- First arg is the name of the type constructor w/ a bad argument, second arg is the bad argument. +data EncodingArgErr a = EncodingArgMismatch TyName (ValT a) + deriving stock (Show, Eq) + +-- | Verifies that a datatype (third argument) is valid according to its stated +-- encoding, as provided by the first two arguments (projection and metadata). +-- +-- = Note +-- +-- If the datatype being validated refers to other datatypes, we assume that +-- they exist in the metadata 'Map'. Thus, we must ensure this holds or the +-- check will fail. +-- +-- @since 1.1.0 +checkEncodingArgs :: + forall (a :: Type) (info :: Type). + (info -> DataEncoding) -> -- this lets us not care about whether we're doing this w/ a DataDeclaration or DatatypeInfo + Map TyName info -> + ValT a -> + Either (EncodingArgErr a) () +checkEncodingArgs getEncoding tyDict = \case + Abstraction {} -> pure () + BuiltinFlat {} -> pure () + ThunkT (CompT _ (CompTBody args)) -> traverse_ go args + Datatype tn args -> do + let encoding = getEncoding $ tyDict M.! tn + case encoding of + -- Might as well check all the way down + SOP -> do + {- NOTE Sean 7/2/25: We are *temporarily* disallowing thunk arguments to SOPs to speed up development and + create consistency. We disallow Thunk arguments to constructors in datatype declarations, + and while we could very well allow them outside of those declarations, it creates a strange situation + where the same function might be safe/unsafe depending on whether it is used on a ValT inside of a data + declaration vs (e.g.) a type annotation in the ASG. + + To remove this restriction, delete the `traverse_ isValidSOPArg args` line below + -} + traverse_ go args + traverse_ (isValidSOPArg tn) args + + -- Both explicit data encodings and builtins should be "morally data encoded" + _ -> do + traverse_ go args + traverse_ (isValidDataArg tn) args + where + go :: ValT a -> Either (EncodingArgErr a) () + go = checkEncodingArgs getEncoding tyDict + + isValidDataArg :: TyName -> ValT a -> Either (EncodingArgErr a) () + isValidDataArg tn = \case + Abstraction {} -> pure () + BuiltinFlat {} -> pure () + thunk@ThunkT {} -> throwError $ EncodingArgMismatch tn thunk + dt@(Datatype tn' args') -> do + let encoding = getEncoding $ tyDict M.! tn' + case encoding of + SOP -> throwError $ EncodingArgMismatch tn dt + _ -> traverse_ go args' + + isValidSOPArg :: TyName -> ValT a -> Either (EncodingArgErr a) () + isValidSOPArg tn = \case + Abstraction {} -> pure () + BuiltinFlat {} -> pure () + thunk@ThunkT {} -> throwError $ EncodingArgMismatch tn thunk + Datatype tn' args' -> traverse_ (isValidSOPArg tn') args' + +checkEncodingArgsInDataDecl :: DataDeclaration AbstractTy -> KindCheckM AbstractTy () +checkEncodingArgsInDataDecl decl = + asks (view #kindCheckContext) >>= \tyDict -> + case traverse (checkEncodingArgs (view #datatypeEncoding) tyDict) allConstructorArgs of + Left encErr -> throwError $ EncodingMismatch encErr + Right _ -> pure () + where + allConstructorArgs :: Vector (ValT AbstractTy) + allConstructorArgs = V.concat $ toListOf (#datatypeConstructors % folded % #constructorArgs) decl diff --git a/src/Covenant/Internal/Ledger.hs b/src/Covenant/Internal/Ledger.hs new file mode 100644 --- /dev/null +++ b/src/Covenant/Internal/Ledger.hs @@ -0,0 +1,706 @@ +module Covenant.Internal.Ledger + ( ledgerTypes, + -- For testing + DeclBuilder (Decl), + CtorBuilder (Ctor), + mkDecl, + maybeT, + pair, + list, + tree, + weirderList, + ) +where + +import Covenant.DeBruijn (DeBruijn (Z)) +import Covenant.Index (Count, count0, count1, count2, ix0, ix1) +import Covenant.Internal.Strategy + ( DataEncoding (BuiltinStrategy, PlutusData), + InternalStrategy (InternalAssocMapStrat, InternalDataStrat, InternalListStrat, InternalPairStrat), + PlutusDataStrategy (ConstrData, NewtypeData), + ) +import Covenant.Internal.Type + ( AbstractTy (BoundAt), + BuiltinFlatT (BoolT, ByteStringT, IntegerT), + Constructor (Constructor), + ConstructorName (ConstructorName), + DataDeclaration (DataDeclaration), + TyName (TyName), + ValT (Abstraction, BuiltinFlat, Datatype), + ) +import Data.Coerce (coerce) +import Data.Vector qualified as Vector + +-- All the ledger types. Just putting them in a list for now but they'll probably end up in some other kind of container eventually +ledgerTypes :: [DataDeclaration AbstractTy] +ledgerTypes = + [ list, + pair, + plutusData, + datum, + redeemer, + scriptHash, + datumHash, + redeemerHash, + credential, + stakingCredential, + pubKeyHash, + address, + maybeT, + posixTime, + interval, + upperBound, + lowerBound, + extended, + ledgerBytes, + assocMap, + currencySymbol, + tokenName, + value, + lovelace, + rational, + mintValue, + txId, + txOutRef, + txOut, + outputDatum, + txInInfo, + dRepCredential, + dRep, + delegatee, + coldCommitteeCredential, + hotCommitteeCredential, + txCert, + voter, + vote, + governanceActionId, + committee, + constitution, + changedParameters, + protocolVersion, + governanceAction, + proposalProcedure, + scriptPurpose, + scriptInfo, + txInfo, + scriptContext + ] + +-- Builtins. These aren't "real" ADTs and their unique encoding strategies indicate special handling + +-- Note (Koz, 11/07/25): This has a Haddock, and is versioned, because +-- Covenant.Test exposes it. If we ever stop doing this, we can remove this +-- Haddock. + +-- | The onchain list type. +-- +-- @since 1.1.0 +list :: DataDeclaration AbstractTy +list = + mkDecl $ + Decl + "List" + count1 + [ Ctor "Nil" [], + Ctor "Cons" [Abstraction (BoundAt Z ix0), tycon "List" [Abstraction (BoundAt Z ix0)]] + ] + (BuiltinStrategy InternalListStrat) + +pair :: DataDeclaration AbstractTy +pair = mkDecl $ Decl "Pair" count2 [Ctor "Pair" [a, b]] (BuiltinStrategy InternalPairStrat) + +-- Make sure this matches up with chooseData +plutusData :: DataDeclaration AbstractTy +plutusData = + mkDecl $ + Decl + "Data" + count0 + [ Ctor "Constr" [BuiltinFlat IntegerT, tycon "List" [tycon "Data" []]], + Ctor "Map" [tycon "List" [tycon "Pair" [tycon "Data" [], tycon "Data" []]]], + Ctor "List" [tycon "List" [tycon "Data" []]], + Ctor "I" [BuiltinFlat IntegerT], + Ctor "B" [BuiltinFlat ByteStringT] + ] + (BuiltinStrategy InternalDataStrat) + +-- Newtypes and Hash Types (from V1) + +datum :: DataDeclaration AbstractTy +datum = mkDecl $ Decl "Datum" count0 [Ctor "Datum" [tycon "Data" []]] (PlutusData NewtypeData) + +redeemer :: DataDeclaration AbstractTy +redeemer = mkDecl $ Decl "Redeemer" count0 [Ctor "Redeemer" [tycon "Data" []]] (PlutusData NewtypeData) + +scriptHash :: DataDeclaration AbstractTy +scriptHash = mkDecl $ Decl "ScriptHash" count0 [Ctor "ScriptHash" [BuiltinFlat ByteStringT]] (PlutusData NewtypeData) + +datumHash :: DataDeclaration AbstractTy +datumHash = mkDecl $ Decl "DatumHash" count0 [Ctor "DatumHash" [BuiltinFlat ByteStringT]] (PlutusData NewtypeData) + +redeemerHash :: DataDeclaration AbstractTy +redeemerHash = mkDecl $ Decl "RedeemerHash" count0 [Ctor "RedeemerHash" [BuiltinFlat ByteStringT]] (PlutusData NewtypeData) + +-- Credential + Staking Credential (from V1) +credential :: DataDeclaration AbstractTy +credential = + mkDecl $ + Decl + "Credential" + count0 + [ Ctor "PubKeyCredential" [tycon "PubKeyHash" []], + Ctor "ScriptCredential" [tycon "ScriptHash" []] + ] + (PlutusData ConstrData) + +stakingCredential :: DataDeclaration AbstractTy +stakingCredential = + mkDecl $ + Decl + "StakingCredential" + count0 + [ Ctor "StakingHash" [tycon "Credential" []], + Ctor "StakingPtr" [BuiltinFlat IntegerT, BuiltinFlat IntegerT, BuiltinFlat IntegerT] + ] + (PlutusData ConstrData) + +-- PubKeyHash (from V1) +pubKeyHash :: DataDeclaration AbstractTy +pubKeyHash = mkDecl $ Decl "PubKeyHash" count0 [Ctor "PubKeyHash" [BuiltinFlat ByteStringT]] (PlutusData NewtypeData) + +-- Address (from V1) +address :: DataDeclaration AbstractTy +address = + mkDecl $ + Decl + "Address" + count0 + [ Ctor "Address" [tycon "Credential" [], tycon "Maybe" [tycon "StakingCredential" []]] + ] + (PlutusData ConstrData) + +-- PlutusTX types, from https://github.com/IntersectMBO/plutus/blob/master/plutus-tx/src/PlutusTx/IsData/Instances.hs +maybeT :: DataDeclaration AbstractTy +maybeT = + mkDecl $ + Decl + "Maybe" + count1 + [ Ctor "Just" [Abstraction (BoundAt Z ix0)], + Ctor "Nothing" [] + ] + (PlutusData ConstrData) + +-- Time & Intervals (V1) + +posixTime :: DataDeclaration AbstractTy +posixTime = mkSimpleNewtype "POSIXTime" (BuiltinFlat IntegerT) + +interval :: DataDeclaration AbstractTy +interval = + mkDecl $ + Decl + "Interval" + count1 + [ Ctor + "Interval" + [ tycon "LowerBound" [a], + tycon "UpperBound" [a] + ] + ] + (PlutusData ConstrData) + +upperBound :: DataDeclaration AbstractTy +upperBound = + mkDecl $ + Decl + "UpperBound" + count1 + [ Ctor "UpperBound" [tycon "Extended" [a], BuiltinFlat BoolT] + ] + (PlutusData ConstrData) + +lowerBound :: DataDeclaration AbstractTy +lowerBound = + mkDecl $ + Decl + "LowerBound" + count1 + [ Ctor "LowerBound" [tycon "Extended" [a], BuiltinFlat BoolT] + ] + (PlutusData ConstrData) + +extended :: DataDeclaration AbstractTy +extended = + mkDecl $ + Decl + "Extended" + count1 + [ Ctor "NegInf" [], + Ctor "Finite" [a], + Ctor "PosInf" [] + ] + (PlutusData ConstrData) + +-- LedgerBytes (V1) + +ledgerBytes :: DataDeclaration AbstractTy +ledgerBytes = mkSimpleNewtype "LedgerBytes" (BuiltinFlat ByteStringT) + +-- Value & Friends (should be V1). Also AssocMap (v1) + +-- NOTE Sean 5/28: This is "magical" like List/Pair/Data due to the fact that we cannot use an opaque +-- (because opaques do not take type parameters) +assocMap :: DataDeclaration AbstractTy +assocMap = + mkDecl $ + Decl + "Map" + count2 + [Ctor "Map" [tycon "List" [tycon "Pair" [a, b]]]] + (BuiltinStrategy InternalAssocMapStrat) + +currencySymbol :: DataDeclaration AbstractTy +currencySymbol = mkSimpleNewtype "CurrencySymbol" (BuiltinFlat ByteStringT) + +tokenName :: DataDeclaration AbstractTy +tokenName = mkSimpleNewtype "TokenName" (BuiltinFlat ByteStringT) + +value :: DataDeclaration AbstractTy +value = + mkSimpleNewtype + "Value" + ( tycon + "Map" + [ tycon "CurrencySymbol" [], + tycon "Map" [tycon "TokenName" [], BuiltinFlat IntegerT] + ] + ) + +lovelace :: DataDeclaration AbstractTy +lovelace = mkSimpleNewtype "Lovelace" (BuiltinFlat IntegerT) + +rational :: DataDeclaration AbstractTy +rational = + mkDecl $ + Decl + "Rational" + count0 + [ Ctor "Rational" [tycon "Pair" [BuiltinFlat IntegerT, BuiltinFlat IntegerT]] + ] + (PlutusData NewtypeData) + +-- MintValue (V3) + +mintValue :: DataDeclaration AbstractTy +mintValue = + mkDecl $ + Decl + "MintValue" + count0 + [ Ctor + "UnsafeMintValue" + [ tycon + "Map" + [ tycon "CurrencySymbol" [], + tycon "Map" [tycon "TokenName" [], BuiltinFlat IntegerT] + ] + ] + ] + (PlutusData NewtypeData) + +-- TxId (v3) +txId :: DataDeclaration AbstractTy +txId = mkSimpleNewtype "TxId" (BuiltinFlat ByteStringT) + +-- TxOutRef (v3) +txOutRef :: DataDeclaration AbstractTy +txOutRef = + mkDecl $ + Decl + "TxOutRef" + count0 + [ Ctor "TxOutRef" [tycon "TxId" [], BuiltinFlat IntegerT] + ] + (PlutusData ConstrData) + +-- TxOut (v2) +txOut :: DataDeclaration AbstractTy +txOut = + mkDecl $ + Decl + "TxOut" + count0 + [ Ctor + "TxOut" + [ tycon "Address" [], + tycon "Value" [], + tycon "OutputDatum" [], + tycon "Maybe" [tycon "ScriptHash" []] + ] + ] + (PlutusData ConstrData) + +-- OutputDatum (v2) +outputDatum :: DataDeclaration AbstractTy +outputDatum = + mkDecl $ + Decl + "OutputDatum" + count0 + [ Ctor "NoOutputDatum" [], + Ctor "OutputDatumHash" [tycon "DatumHash" []], + Ctor "OutputDatum" [tycon "OutputDatum" []] + ] + (PlutusData ConstrData) + +-- txInInfo (V3) +txInInfo :: DataDeclaration AbstractTy +txInInfo = + mkDecl $ + Decl + "TxInInfo" + count0 + [ Ctor + "TxInInfo" + [ tycon "TxOutRef" [], + tycon "TxOut" [] + ] + ] + (PlutusData ConstrData) + +-- DRepCredential (v3) +dRepCredential :: DataDeclaration AbstractTy +dRepCredential = mkSimpleNewtype "DRepCredential" (tycon "Credential" []) + +-- DRep (v3) +dRep :: DataDeclaration AbstractTy +dRep = + mkDecl $ + Decl + "DRep" + count0 + [ Ctor "DRep" [tycon "DRepCredential" []], + Ctor "DRepAlwaysAbstain" [], + Ctor "DRepAlwaysNoConfidence" [] + ] + (PlutusData ConstrData) + +-- delegatee (v3) +delegatee :: DataDeclaration AbstractTy +delegatee = + mkDecl $ + Decl + "Delegatee" + count0 + [ Ctor "DelegStake" [tycon "PubKeyHash" []], + Ctor "DelegVote" [tycon "DRep" []], + Ctor "DelegStakeVoke" [tycon "PubKeyHash" [], tycon "DRep" []] + ] + (PlutusData ConstrData) + +coldCommitteeCredential :: DataDeclaration AbstractTy +coldCommitteeCredential = mkSimpleNewtype "ColdCommitteeCredential" (tycon "Credential" []) + +hotCommitteeCredential :: DataDeclaration AbstractTy +hotCommitteeCredential = mkSimpleNewtype "HotCommitteeCredential" (tycon "Credential" []) + +-- txCert (v3) +txCert :: DataDeclaration AbstractTy +txCert = + mkDecl $ + Decl + "TxCert" + count0 + [ Ctor "TxCertRegStaking" [tycon "Credential" [], tycon "Maybe" [tycon "Lovelace" []]], + Ctor "TxCertUnRegStaking" [tycon "Credential" [], tycon "Maybe" [tycon "Lovelace" []]], + Ctor "TxCertDelegStaking" [tycon "Credential" [], tycon "Delegatee" []], + Ctor "TxCertRegDeleg" [tycon "Credential" [], tycon "Delegatee" [], tycon "Lovelace" []], + Ctor "TxCertRegDRep" [tycon "DRepCredential" [], tycon "Lovelace" []], + Ctor "TxCertUpdateDRep" [tycon "DRepCredential" []], + Ctor "TxCertUnRegDRep" [tycon "DRepCredential" [], tycon "Lovelace" []], + Ctor "TxCertPoolRegister" [tycon "PubKeyHash" [], tycon "PubKeyHash" []], + Ctor "TxCertPoolRetire" [tycon "PubKeyHash" [], BuiltinFlat IntegerT], + Ctor "TxCertAuthHotCommittee" [tycon "ColdCommitteeCredential" [], tycon "HotCommitteeCredential" []], + Ctor "TxCertResignColdCommittee" [tycon "ColdCommitteeCredential" []] + ] + (PlutusData ConstrData) + +-- voter (v3) +voter :: DataDeclaration AbstractTy +voter = + mkDecl $ + Decl + "Voter" + count0 + [ Ctor "CommitteeVoter" [tycon "HotCommitteeCredential" []], + Ctor "DRepVoter" [tycon "DRepCredential" []], + Ctor "StakePoolVoter" [tycon "PubKeyHash" []] + ] + (PlutusData ConstrData) + +-- vote (v3) +vote :: DataDeclaration AbstractTy +vote = + mkDecl $ + Decl + "Vote" + count0 + [ Ctor "VoteNo" [], + Ctor "VoteYes" [], + Ctor "Abstain" [] + ] + (PlutusData ConstrData) + +-- GovernanceActionID (v3) +governanceActionId :: DataDeclaration AbstractTy +governanceActionId = + mkDecl $ + Decl + "GovernanceActionId" + count0 + [ Ctor + "GovernanceActionId" + [ tycon "TxId" [], + BuiltinFlat IntegerT + ] + ] + (PlutusData ConstrData) + +-- Committee (v3) +committee :: DataDeclaration AbstractTy +committee = + mkDecl $ + Decl + "Committee" + count0 + [ Ctor + "Committee" + [ tycon "Map" [tycon "ColdCommitteeCredential" [], BuiltinFlat IntegerT], + tycon "Rational" [] + ] + ] + (PlutusData ConstrData) + +-- constitution (V3) +constitution :: DataDeclaration AbstractTy +constitution = mkSimpleNewtype "Constitution" (tycon "Maybe" [tycon "ScriptHash" []]) + +-- changedParameters (V3) +changedParameters :: DataDeclaration AbstractTy +changedParameters = mkSimpleNewtype "ChangedParameters" (tycon "Data" []) + +-- ProtocolVersion (V3) +protocolVersion :: DataDeclaration AbstractTy +protocolVersion = + mkDecl $ + Decl + "ProtocolVersion" + count0 + [ Ctor "ProtocolVersion" [BuiltinFlat IntegerT, BuiltinFlat IntegerT] + ] + (PlutusData ConstrData) + +-- GovernanceAction (v3) +governanceAction :: DataDeclaration AbstractTy +governanceAction = + mkDecl $ + Decl + "GovernanceAction" + count0 + [ Ctor + "ParameterChange" + [ tycon "Maybe" [tycon "GovernanceActionId" []], + tycon "ChangedParameters" [], + tycon "Maybe" [tycon "ScriptHash" []] + ], + Ctor + "HardForkInitiation" + [ tycon "Maybe" [tycon "GovernanceActionId" []], + tycon "ProtocolVersion" [] + ], + Ctor + "TreasuryWithdrawals" + [ tycon "Map" [tycon "Credential" [], tycon "Lovelace" []], + tycon "Maybe" [tycon "ScriptHash" []] + ], + Ctor "NoConfidence" [tycon "Maybe" [tycon "GovernanceActionId" []]], + Ctor + "UpdateCommittee" + [ tycon "Maybe" [tycon "GovernanceActionId" []], + tycon "List" [tycon "ColdCommitteeCredential" []], + tycon "Map" [tycon "ColdCommitteeCredential" [], BuiltinFlat IntegerT], + tycon "Rational" [] + ], + Ctor "NewConstitution" [tycon "Maybe" [tycon "GovernanceActionId" []], tycon "Constitution" []], + Ctor "InfoAction" [] + ] + (PlutusData ConstrData) + +-- ProposalProcedure (v3) +proposalProcedure :: DataDeclaration AbstractTy +proposalProcedure = + mkDecl $ + Decl + "ProposalProcedure" + count0 + [ Ctor + "ProposalProcedure" + [ tycon "Lovelace" [], + tycon "Credential" [], + tycon "GovernanceAction" [] + ] + ] + (PlutusData ConstrData) + +-- scriptPurpose (v3) +scriptPurpose :: DataDeclaration AbstractTy +scriptPurpose = + mkDecl $ + Decl + "ScriptPurpose" + count0 + [ Ctor "Minting" [tycon "CurrencySymbol" []], + Ctor "Spending" [tycon "TxOutRef" []], + Ctor "Rewarding" [tycon "Credential" []], + Ctor "Certifying" [BuiltinFlat IntegerT, tycon "TxCert" []], + Ctor "Voting" [tycon "Voter" []], + Ctor "Proposing" [BuiltinFlat IntegerT, tycon "ProposalProcedure" []] + ] + (PlutusData ConstrData) + +-- ScriptInfo (V3) +scriptInfo :: DataDeclaration AbstractTy +scriptInfo = + mkDecl $ + Decl + "ScriptInfo" + count0 + [ Ctor "MintingScript" [tycon "CurrencySymbol" []], + Ctor "SpendingScript" [tycon "TxOutRef" [], tycon "Maybe" [tycon "Datum" []]], + Ctor "RewardingScript" [tycon "Credential" []], + Ctor "CertifyingScript" [BuiltinFlat IntegerT, tycon "TxCert" []], + Ctor "VotingScript" [tycon "Voter" []], + Ctor "ProposingScript" [BuiltinFlat IntegerT, tycon "ProposalProcedure" []] + ] + (PlutusData ConstrData) + +-- This is a TypeSyn, so not a declaration, but it's *annoying* to type the ValT version out +posixTimeRange :: ValT AbstractTy +posixTimeRange = tycon "Interval" [tycon "POSIXTime" []] + +-- txInfo (v3) +txInfo :: DataDeclaration AbstractTy +txInfo = + mkDecl $ + Decl + "TxInfo" + count0 + [ Ctor + "TxInfo" + [ tycon "List" [tycon "TxInInfo" []], + tycon "List" [tycon "TxInInfo" []], + tycon "List" [tycon "TxOut" []], + tycon "Lovelace" [], + tycon "MintValue" [], + tycon "List" [tycon "TxCert" []], + tycon "Map" [tycon "Credential" [], tycon "Lovelace" []], + posixTimeRange, + tycon "List" [tycon "PubKeyHash" []], + tycon "Map" [tycon "ScriptPurpose" [], tycon "Redeemer" []], + tycon "Map" [tycon "DatumHash" [], tycon "Datum" []], + tycon "TxId" [], + tycon "Map" [tycon "Voter" [], tycon "Map" [tycon "GovernanceActionId" [], tycon "Vote" []]], + tycon "List" [tycon "ProposalProcedure" []], + tycon "Maybe" [tycon "Lovelace" []], + tycon "Maybe" [tycon "Lovelace" []] + ] + ] + (PlutusData ConstrData) + +-- scriptContext (v3) +scriptContext :: DataDeclaration AbstractTy +scriptContext = + mkDecl $ + Decl + "ScriptContext" + count0 + [ Ctor + "ScriptContext" + [ tycon "TxInfo" [], + tycon "Redeemer" [], + tycon "ScriptInfo" [] + ] + ] + (PlutusData ConstrData) + +-- Helpers + +-- Variants of DataDeclaration and Constructor that use Lists to avoid a slew of Vector.fromList cluttering up the module + +data DeclBuilder = Decl TyName (Count "tyvar") [CtorBuilder] DataEncoding + +data CtorBuilder = Ctor ConstructorName [ValT AbstractTy] + +mkDecl :: DeclBuilder -> DataDeclaration AbstractTy +mkDecl (Decl tn cnt ctors enc) = DataDeclaration tn cnt (Vector.fromList . fmap mkCtor $ ctors) enc + where + mkCtor :: CtorBuilder -> Constructor AbstractTy + mkCtor (Ctor cnm fields) = Constructor cnm (Vector.fromList fields) + +tycon :: TyName -> [ValT AbstractTy] -> ValT AbstractTy +tycon tn vals = Datatype tn (Vector.fromList vals) + +{- This is shorthand for a non-polymorphic newtype (i.e. a single ctor / arg type with a newtype strategy) where + the name of the constructor is the same as the name of the type. + + This is a *very* common case and this seems useful to save extra typing. + +-} +mkSimpleNewtype :: TyName -> ValT AbstractTy -> DataDeclaration AbstractTy +mkSimpleNewtype tn val = mkDecl $ Decl tn count0 [Ctor (coerce tn) [val]] (PlutusData NewtypeData) + +-- obviously should not export these, solely exist to improve readability of declarations. +-- Since everything here is data-encodeable the DB index *should* always be Z & I don't think anything uses more than +-- 2 tyvars + +a :: ValT AbstractTy +a = Abstraction (BoundAt Z ix0) + +b :: ValT AbstractTy +b = Abstraction (BoundAt Z ix1) + +-- For tests, much easier to define this here w/ the helpers + +-- Note (Koz, 11/07/25): Same as for `list`. + +-- | A datatype equivalent to +-- +-- @data Tree a = Bin (Tree a) (Tree a) | Tip a@ +-- +-- @since 1.1.0 +tree :: DataDeclaration AbstractTy +tree = + mkDecl $ + Decl + "Tree" + count1 + [ Ctor "Bin" [tycon "Tree" [a], tycon "Tree" [a]], + Ctor "Tip" [a] + ] + (PlutusData ConstrData) + +-- | A datatype equivalent to +-- +-- @data WeirderList a = Uncons (Maybe (a, WeirderList a))@ +-- +-- @since 1.1.0 +weirderList :: DataDeclaration AbstractTy +weirderList = + mkDecl $ + Decl + "WeirderList" + count1 + [ Ctor "Uncons" [tycon "Maybe" [tycon "Pair" [a, tycon "WeirderList" [a]]]] + ] + (PlutusData ConstrData) diff --git a/src/Covenant/Internal/PrettyPrint.hs b/src/Covenant/Internal/PrettyPrint.hs new file mode 100644 --- /dev/null +++ b/src/Covenant/Internal/PrettyPrint.hs @@ -0,0 +1,169 @@ +module Covenant.Internal.PrettyPrint + ( ScopeBoundary (..), + PrettyContext (..), + PrettyM, + runPrettyM, + bindVars, + mkForall, + lookupAbstraction, + ) +where + +import Control.Monad.Reader + ( MonadReader (local), + Reader, + asks, + runReader, + ) +import Covenant.Index + ( Count, + Index, + intCount, + intIndex, + ) +import Data.Kind (Type) +import Data.Map.Strict (Map) +import Data.Map.Strict qualified as Map +import Data.Vector (Vector) +import Data.Vector qualified as Vector +import GHC.Exts (fromListN) +import Optics.At () +import Optics.Core + ( A_Lens, + LabelOptic (labelOptic), + ix, + lens, + over, + preview, + review, + set, + view, + (%), + ) +import Prettyprinter + ( Doc, + Pretty (pretty), + hsep, + (<+>), + ) + +newtype ScopeBoundary = ScopeBoundary Int + deriving (Show, Eq, Ord, Num, Real, Enum, Integral) via Int + +-- Keeping the field names for clarity even if we don't use them +data PrettyContext (ann :: Type) + = PrettyContext + { _boundIdents :: Map ScopeBoundary (Vector (Doc ann)), + _currentScope :: ScopeBoundary, + _varStream :: [Doc ann] + } + +instance + (k ~ A_Lens, a ~ Map ScopeBoundary (Vector (Doc ann)), b ~ Map ScopeBoundary (Vector (Doc ann))) => + LabelOptic "boundIdents" k (PrettyContext ann) (PrettyContext ann) a b + where + {-# INLINEABLE labelOptic #-} + labelOptic = + lens + (\(PrettyContext x _ _) -> x) + (\(PrettyContext _ y z) x -> PrettyContext x y z) + +instance + (k ~ A_Lens, a ~ ScopeBoundary, b ~ ScopeBoundary) => + LabelOptic "currentScope" k (PrettyContext ann) (PrettyContext ann) a b + where + {-# INLINEABLE labelOptic #-} + labelOptic = + lens + (\(PrettyContext _ x _) -> x) + (\(PrettyContext x _ z) y -> PrettyContext x y z) + +instance + (k ~ A_Lens, a ~ [Doc ann], b ~ [Doc ann]) => + LabelOptic "varStream" k (PrettyContext ann) (PrettyContext ann) a b + where + {-# INLINEABLE labelOptic #-} + labelOptic = + lens + (\(PrettyContext _ _ x) -> x) + (\(PrettyContext x y _) z -> PrettyContext x y z) + +-- Maybe make a newtype with error reporting since this can fail, but do later since *should't* fail +newtype PrettyM (ann :: Type) (a :: Type) = PrettyM (Reader (PrettyContext ann) a) + deriving + ( Functor, + Applicative, + Monad, + MonadReader (PrettyContext ann) + ) + via (Reader (PrettyContext ann)) + +runPrettyM :: forall (ann :: Type) (a :: Type). PrettyM ann a -> a +runPrettyM (PrettyM ma) = runReader ma (PrettyContext mempty 0 infiniteVars) + where + -- Lazily generated infinite list of variables. Will start with a, b, c... + -- and cycle around to a1, b2, c3 etc. + -- We could do something more sophisticated but this should work. + infiniteVars :: [Doc ann] + infiniteVars = + let aToZ = ['a' .. 'z'] + intStrings = ("" <$ aToZ) <> map (show @Integer) [0 ..] + in zipWith (\x xs -> pretty (x : xs)) aToZ intStrings + +bindVars :: + forall (ann :: Type) (a :: Type). + Count "tyvar" -> + (Vector (Doc ann) -> PrettyM ann a) -> + PrettyM ann a +bindVars count' act + | count == 0 = crossBoundary (act Vector.empty) + | otherwise = crossBoundary $ do + here <- asks (view #currentScope) + withFreshVarNames count $ \newBoundVars -> + local (over #boundIdents (Map.insert here newBoundVars)) (act newBoundVars) + where + -- Increment the current scope + crossBoundary :: PrettyM ann a -> PrettyM ann a + crossBoundary = local (over #currentScope (+ 1)) + count :: Int + count = review intCount count' + +mkForall :: + forall (ann :: Type). + Vector (Doc ann) -> + Doc ann -> + Doc ann +mkForall tvars funTyBody = + if Vector.null tvars + then funTyBody + else "forall" <+> hsep (Vector.toList tvars) <> "." <+> funTyBody + +lookupAbstraction :: forall (ann :: Type). Int -> Index "tyvar" -> PrettyM ann (Doc ann) +lookupAbstraction offset argIndex = do + let scopeOffset = ScopeBoundary offset + let argIndex' = review intIndex argIndex + here <- asks (view #currentScope) + asks (preview (#boundIdents % ix (here + scopeOffset) % ix argIndex')) >>= \case + Nothing -> + -- TODO: actual error reporting + error $ + "Internal error: The encountered a variable at arg index " + <> show argIndex' + <> " with true level " + <> show scopeOffset + <> " but could not locate the corresponding pretty form at scope level " + <> show here + Just res' -> pure res' + +-- Helpers + +-- Generate N fresh var names and use the supplied monadic function to do something with them. +withFreshVarNames :: + forall (ann :: Type) (a :: Type). + Int -> + (Vector (Doc ann) -> PrettyM ann a) -> + PrettyM ann a +withFreshVarNames n act = do + stream <- asks (view #varStream) + let (used, rest) = splitAt n stream + local (set #varStream rest) . act . fromListN n $ used diff --git a/src/Covenant/Internal/Rename.hs b/src/Covenant/Internal/Rename.hs --- a/src/Covenant/Internal/Rename.hs +++ b/src/Covenant/Internal/Rename.hs @@ -3,8 +3,10 @@ RenameError (..), runRenameM, renameValT, + renameDataDecl, renameCompT, undoRename, + renameDatatypeInfo, ) where @@ -26,15 +28,19 @@ gets, modify, ) +import Covenant.Data (DatatypeInfo (DatatypeInfo)) import Covenant.DeBruijn (DeBruijn (S, Z), asInt) import Covenant.Index (Count, Index, intCount, intIndex) import Covenant.Internal.Type ( AbstractTy (BoundAt), CompT (CompT), CompTBody (CompTBody), + Constructor (Constructor), + DataDeclaration (DataDeclaration, OpaqueData), Renamed (Rigid, Unifiable, Wildcard), - ValT (Abstraction, BuiltinFlat, ThunkT), + ValT (Abstraction, BuiltinFlat, Datatype, ThunkT), ) +import Data.Bitraversable (Bitraversable (bitraverse)) import Data.Coerce (coerce) import Data.Kind (Type) import Data.Tuple.Optics (_1) @@ -107,7 +113,7 @@ -- | Ways in which the renamer can fail. -- --- @since 1.0.0 +-- @since 1.1.0 data RenameError = -- | An attempt to reference an abstraction in a scope where this -- abstraction doesn't exist. First field is the true level, second is @@ -115,18 +121,6 @@ -- -- @since 1.0.0 InvalidAbstractionReference Int (Index "tyvar") - | -- | A value type specifies an abstraction that never gets used - -- anywhere. For example, the type @forall a b . [a]@ has @b@ - -- irrelevant. - -- - -- @since 1.0.0 - IrrelevantAbstraction - | -- | A computation type specifies an abstraction which is not used - -- by any argument. For example, the type @forall a b . a -> !(b -> !a)@ - -- has @b@ undetermined. - -- - -- @since 1.0.0 - UndeterminedAbstraction deriving stock (Eq, Show) -- | A \'renaming monad\' which allows us to convert type representations from @@ -183,9 +177,6 @@ Vector.generateM (NonEmpty.length xs - 1) (\i -> coerce . renameValT $ xs NonEmpty.! i) - -- Check that we don't overdetermine anything - ourAbstractions <- gets (view (#tracker % to Vector.head % _1)) - unless (Vector.and ourAbstractions) (throwError UndeterminedAbstraction) -- Check result type renamedResult <- coerce . renameValT . NonEmpty.last $ xs -- Roll back state @@ -201,7 +192,32 @@ Abstraction t -> Abstraction <$> renameAbstraction t ThunkT t -> ThunkT <$> renameCompT t BuiltinFlat t -> pure . BuiltinFlat $ t + -- Assumes kind-checking has occurred + Datatype tn xs -> RenameM $ do + -- We don't step or un-step the scope here b/c a TyCon which appears as a ValT _cannot_ bind variables. + -- This Vector here doesn't represent a function, but a product, so we there is no "return" type to treat specially (I think!) + renamedXS <- Vector.mapM (coerce . renameValT) xs + pure $ Datatype tn renamedXS +-- @since 1.1.0 +renameDataDecl :: DataDeclaration AbstractTy -> RenameM (DataDeclaration Renamed) +renameDataDecl (OpaqueData tn manual) = pure $ OpaqueData tn manual +renameDataDecl (DataDeclaration tn cnt ctors strat) = RenameM $ do + modify (stepUpScope cnt) + renamedCtors <- Vector.mapM (coerce . renameCtor) ctors + modify dropDownScope + pure $ DataDeclaration tn cnt renamedCtors strat + where + renameCtor :: Constructor AbstractTy -> RenameM (Constructor Renamed) + renameCtor (Constructor cn args) = Constructor cn <$> traverse renameValT args + +renameDatatypeInfo :: DatatypeInfo AbstractTy -> Either RenameError (DatatypeInfo Renamed) +renameDatatypeInfo (DatatypeInfo ogDecl baseFStuff bb) = runRenameM $ do + ogDecl' <- renameDataDecl ogDecl + baseFStuff' <- traverse (bitraverse renameDataDecl renameValT) baseFStuff + bb' <- traverse renameValT bb + pure $ DatatypeInfo ogDecl' baseFStuff' bb' + -- A way of 'undoing' the renaming process. This is meant to be used only after -- applications, and assumes that what is being un-renamed is the result of a -- computation. @@ -218,6 +234,7 @@ ThunkT (CompT abses (CompTBody xs)) -> ThunkT . CompT abses . CompTBody <$> local (+ 1) (traverse go xs) BuiltinFlat t' -> pure . BuiltinFlat $ t' + Datatype tn args -> Datatype tn <$> traverse go args -- Helpers @@ -231,8 +248,8 @@ renameAbstraction :: AbstractTy -> RenameM Renamed renameAbstraction (BoundAt scope index) = RenameM $ do - trueLevel <- gets (\x -> view (#tracker % to Vector.length) x - asInt scope) - scopeInfo <- gets (\x -> view #tracker x Vector.!? asInt scope) + trueLevel <- gets (\x -> view (#tracker % to Vector.length) x - review asInt scope) + scopeInfo <- gets (\x -> view #tracker x Vector.!? review asInt scope) let asIntIx = review intIndex index case scopeInfo of -- This variable is bound in a scope that encloses the renaming scope. Thus, @@ -274,4 +291,4 @@ -- we've seen this variable. noteUsed :: DeBruijn -> Index "tyvar" -> RenameState -> RenameState noteUsed scope index = - set (#tracker % ix (asInt scope) % _1 % ix (review intIndex index)) True + set (#tracker % ix (review asInt scope) % _1 % ix (review intIndex index)) True diff --git a/src/Covenant/Internal/Strategy.hs b/src/Covenant/Internal/Strategy.hs new file mode 100644 --- /dev/null +++ b/src/Covenant/Internal/Strategy.hs @@ -0,0 +1,100 @@ +module Covenant.Internal.Strategy + ( DataEncoding (..), + PlutusDataStrategy (..), + InternalStrategy (..), + PlutusDataConstructor (..), + ) +where + +-- | Describes how a datatype is represented onchain. +-- +-- @since 1.1.0 +data DataEncoding + = -- | The datatype is represented using the SOP primitives. + -- + -- @since 1.1.0 + SOP + | -- | The datatype is represented as @Data@, using the + -- specified strategy to determine specifics. + -- + -- @since 1.1.0 + PlutusData PlutusDataStrategy + | -- | The type uses one of the builtin \'special\' strategies. This + -- is used only for specific types and isn't generally available + -- for use. + -- + -- @since 1.1.0 + BuiltinStrategy InternalStrategy + deriving stock + ( -- | @since 1.1.0 + Show, + -- | @since 1.1.0 + Eq, + -- | @since 1.1.0 + Ord + ) + +-- NOTE: Wrapped data-primitive (Integer + ByteString) require a special case for their encoders, which was originally +-- part of a "WrapperData" strategy here which we generalized to the NewtypeData strategy. + +-- | Specifics of how a @Data@-encoded datatype is represented. +-- +-- @since 1.1.0 +data PlutusDataStrategy + = -- | The type is encoded as an @Integer@, corresponding to which \'arm\' + -- of the datatype we want. + -- + -- @since 1.1.0 + EnumData + | -- | The type is encoded as a list of its fields. + -- + -- @since 1.1.0 + ProductListData + | -- | The type is encoded using @Constr@. + -- + -- @since 1.1.0 + ConstrData + | -- | The type \'borrows\' the encoding of whatever it wraps. + -- + -- @since 1.1.0 + NewtypeData + deriving stock + ( -- | @since 1.1.0 + Show, + -- | @since 1.1.0 + Eq, + -- | @since 1.1.0 + Ord + ) + +-- | The constructors of the onchain @Data@ type. Needed for other definitions +-- here. +-- +-- @since 1.1.0 +data PlutusDataConstructor + = PlutusI + | PlutusB + | PlutusConstr + | PlutusList + | PlutusMap + deriving stock + ( -- | @since 1.1.0 + Show, + -- | @since 1.1.0 + Eq, + -- | @since 1.1.0 + Ord + ) + +data InternalStrategy + = InternalListStrat + | InternalPairStrat + | InternalDataStrat + | InternalAssocMapStrat + | -- This exists solely so I can get a 'DataEncoding' out of an opaque, it's not really used + InternalOpaqueStrat + deriving stock + ( Show, + Eq, + Ord + ) diff --git a/src/Covenant/Internal/Term.hs b/src/Covenant/Internal/Term.hs --- a/src/Covenant/Internal/Term.hs +++ b/src/Covenant/Internal/Term.hs @@ -19,10 +19,11 @@ import Covenant.Constant (AConstant) import Covenant.DeBruijn (DeBruijn) import Covenant.Index (Index) +import Covenant.Internal.KindCheck (EncodingArgErr) import Covenant.Internal.Rename (RenameError) import Covenant.Internal.Type (AbstractTy, CompT, ValT) import Covenant.Internal.Unification (TypeAppError) -import Covenant.Prim (OneArgFunc, ThreeArgFunc, TwoArgFunc) +import Covenant.Prim (OneArgFunc, SixArgFunc, ThreeArgFunc, TwoArgFunc) import Data.Kind (Type) import Data.Vector (Vector) import Data.Word (Word64) @@ -117,6 +118,10 @@ -- -- @since 1.0.0 WrongReturnType (ValT AbstractTy) (ValT AbstractTy) + | -- @since 1.1.0 + + -- | Wraps an encoding argument mismatch error from KindCheck + EncodingError (EncodingArgErr AbstractTy) deriving stock ( -- | @since 1.0.0 Eq, @@ -150,7 +155,8 @@ typeId :: forall (m :: Type -> Type). (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) => - Id -> m ASGNodeType + Id -> + m ASGNodeType typeId i = do lookedUp <- lookupRef i case lookedUp of @@ -199,7 +205,8 @@ typeRef :: forall (m :: Type -> Type). (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) => - Ref -> m ASGNodeType + Ref -> + m ASGNodeType typeRef = \case AnArg arg -> pure . ValNodeType . typeArg $ arg AnId i -> typeId i @@ -211,6 +218,7 @@ = Builtin1Internal OneArgFunc | Builtin2Internal TwoArgFunc | Builtin3Internal ThreeArgFunc + | Builtin6Internal SixArgFunc | LamInternal Id | ForceInternal Ref | ReturnInternal Ref diff --git a/src/Covenant/Internal/Type.hs b/src/Covenant/Internal/Type.hs --- a/src/Covenant/Internal/Type.hs +++ b/src/Covenant/Internal/Type.hs @@ -1,57 +1,99 @@ +{-# LANGUAGE OverloadedLists #-} +{-# LANGUAGE PatternSynonyms #-} + module Covenant.Internal.Type ( AbstractTy (..), Renamed (..), CompT (..), CompTBody (..), + DataDeclaration (..), + Constructor (..), + ConstructorName (..), ValT (..), BuiltinFlatT (..), + TyName (..), + runConstructorName, + abstraction, + thunkT, + builtinFlat, + datatype, + checkStrategy, + naturalBaseFunctor, + negativeBaseFunctor, + byteStringBaseFunctor, ) where -import Control.Monad.Reader - ( MonadReader (local), - Reader, - asks, - runReader, - ) -import Covenant.DeBruijn (DeBruijn) +import Covenant.DeBruijn (DeBruijn (Z)) import Covenant.Index ( Count, Index, + count1, intCount, intIndex, + ix0, ) +import Covenant.Internal.PrettyPrint + ( PrettyM, + bindVars, + lookupAbstraction, + mkForall, + runPrettyM, + ) +import Covenant.Internal.Strategy + ( DataEncoding + ( BuiltinStrategy, + PlutusData, + SOP + ), + InternalStrategy + ( InternalAssocMapStrat, + InternalDataStrat, + InternalListStrat, + InternalOpaqueStrat, + InternalPairStrat + ), + PlutusDataConstructor, + PlutusDataStrategy + ( ConstrData, + EnumData, + NewtypeData, + ProductListData + ), + ) +import Covenant.Util (pattern ConsV, pattern NilV) import Data.Functor.Classes (Eq1 (liftEq)) import Data.Kind (Type) -import Data.Map.Strict (Map) -import Data.Map.Strict qualified as Map +import Data.Set (Set) +import Data.String (IsString) +import Data.Text (Text) import Data.Vector (Vector) import Data.Vector qualified as Vector import Data.Vector.NonEmpty (NonEmptyVector) import Data.Vector.NonEmpty qualified as NonEmpty import Data.Word (Word64) -import GHC.Exts (fromListN) -import Optics.At () import Optics.Core - ( A_Lens, + ( A_Fold, + A_Lens, LabelOptic (labelOptic), - ix, + Prism', + folding, lens, - over, preview, + prism, review, - set, - view, - (%), ) import Prettyprinter ( Doc, Pretty (pretty), hsep, + indent, parens, + vcat, viaShow, (<+>), ) +import Test.QuickCheck.Instances.Text () -- | A type abstraction, using a combination of a DeBruijn index (to indicate -- which scope it refers to) and a positional index (to indicate which bound @@ -150,6 +192,23 @@ instance Pretty (CompT Renamed) where pretty = runPrettyM . prettyCompTWithContext +-- | The name of a data type. This refers specifically to non-\'flat\' types +-- either provided by the ledger, or defined by the user. +-- +-- @since 1.1.0 +newtype TyName = TyName Text + deriving + ( -- | @since 1.1.0 + Show, + -- | @since 1.1.0 + Eq, + -- | @since 1.1.0 + Ord, + -- | @since 1.1.0 + IsString + ) + via Text + -- | A value type, with abstractions indicated by the type argument. In pretty -- much any case imaginable, this would be either 'AbstractTy' (in the ASG) or -- 'Renamed' (after renaming). @@ -162,6 +221,9 @@ ThunkT (CompT a) | -- | A builtin type without any nesting. BuiltinFlat BuiltinFlatT + | -- | An applied type constructor for a non-\'flat\' data type. + -- | @since 1.1.0 + Datatype TyName (Vector (ValT a)) deriving stock ( -- | @since 1.0.0 Eq, @@ -184,9 +246,36 @@ BuiltinFlat t1 -> \case BuiltinFlat t2 -> t1 == t2 _ -> False + Datatype tn1 args1 -> \case + Datatype tn2 args2 -> tn1 == tn2 && liftEq (liftEq f) args1 args2 + _ -> False +-- | /Do not/ use this instance to write other 'Pretty' instances. It exists to +-- ensure readable tests without having to expose a lot of internals. +-- +-- @since 1.0.0 +instance Pretty (ValT Renamed) where + pretty = runPrettyM . prettyValTWithContext + +abstraction :: forall (a :: Type). Prism' (ValT a) a +abstraction = prism Abstraction (\case (Abstraction a) -> Right a; other -> Left other) + +thunkT :: forall (a :: Type). Prism' (ValT a) (CompT a) +thunkT = prism ThunkT (\case (ThunkT compT) -> Right compT; other -> Left other) + +builtinFlat :: forall (a :: Type). Prism' (ValT a) BuiltinFlatT +builtinFlat = prism BuiltinFlat (\case (BuiltinFlat bi) -> Right bi; other -> Left other) + +datatype :: forall (a :: Type). Prism' (ValT a) (TyName, Vector (ValT a)) +datatype = + prism + (uncurry Datatype) + (\case (Datatype tn args) -> Right (tn, args); other -> Left other) + -- | All builtin types that are \'flat\': that is, do not have other types -- \'nested inside them\'. +-- +-- @since 1.0.0 data BuiltinFlatT = UnitT | BoolT @@ -205,151 +294,217 @@ Show ) --- Helpers +-- | The name of a data type constructor. +-- +-- @since 1.1.0 +newtype ConstructorName = ConstructorName Text + deriving + ( -- | @since 1.1.0 + Show, + -- | @since 1.1.0 + Eq, + -- | @since 1.1.0 + Ord, + -- | @since 1.1.0 + IsString + ) + via Text -newtype ScopeBoundary = ScopeBoundary Int - deriving (Show, Eq, Ord, Num) via Int +-- | @since 1.1.0 +runConstructorName :: ConstructorName -> Text +runConstructorName (ConstructorName nm) = nm --- Keeping the field names for clarity even if we don't use them -data PrettyContext (ann :: Type) - = PrettyContext - { _boundIdents :: Map ScopeBoundary (Vector (Doc ann)), - _currentScope :: ScopeBoundary, - _varStream :: [Doc ann] - } +-- | A single constructor of a data type, with its fields. +-- +-- @since 1.1.0 +data Constructor (a :: Type) + = Constructor ConstructorName (Vector (ValT a)) + deriving stock + ( -- | @since 1.1.0 + Show, + -- | @since 1.1.0 + Eq + ) +-- | @since 1.1.0 +instance Eq1 Constructor where + liftEq f (Constructor nm args) (Constructor nm' args') = + nm == nm' && liftEq (liftEq f) args args' + +-- | @since 1.1.0 instance - (k ~ A_Lens, a ~ Map ScopeBoundary (Vector (Doc ann)), b ~ Map ScopeBoundary (Vector (Doc ann))) => - LabelOptic "boundIdents" k (PrettyContext ann) (PrettyContext ann) a b + (k ~ A_Lens, a ~ ConstructorName, b ~ ConstructorName) => + LabelOptic "constructorName" k (Constructor c) (Constructor c) a b where {-# INLINEABLE labelOptic #-} + labelOptic = lens (\(Constructor n _) -> n) (\(Constructor _ args) n -> Constructor n args) + +-- | @since 1.1.0 +instance + (k ~ A_Lens, a ~ Vector (ValT c), b ~ Vector (ValT c)) => + LabelOptic "constructorArgs" k (Constructor c) (Constructor c) a b + where + {-# INLINEABLE labelOptic #-} + labelOptic = lens (\(Constructor _ args) -> args) (\(Constructor n _) args -> Constructor n args) + +-- | Description of a non-\'flat\' type, together with how it is encoded. +-- +-- @since 1.1.0 +data DataDeclaration a + = -- | A \'standard\' datatype, with its constructors and encoding. + -- + -- @since 1.1.0 + DataDeclaration TyName (Count "tyvar") (Vector (Constructor a)) DataEncoding + | -- | An \'opaque\' datatype, with the permitted constructors of + -- @Data@ we can use to build and tear it down. + -- + -- @since 1.1.0 + OpaqueData TyName (Set PlutusDataConstructor) + deriving stock + ( -- | @since 1.1.0 + Show, + -- | @since 1.1.0 + Eq + ) + +-- | @since 1.1.0 +instance Pretty (DataDeclaration Renamed) where + pretty = runPrettyM . prettyDataDeclWithContext + +-- | @since 1.1.0 +instance + (k ~ A_Lens, a ~ TyName, b ~ TyName) => + LabelOptic "datatypeName" k (DataDeclaration c) (DataDeclaration c) a b + where + {-# INLINEABLE labelOptic #-} labelOptic = lens - (\(PrettyContext x _ _) -> x) - (\(PrettyContext _ y z) x -> PrettyContext x y z) + (\case OpaqueData tn _ -> tn; DataDeclaration tn _ _ _ -> tn) + (\decl tn -> case decl of OpaqueData _ x -> OpaqueData tn x; DataDeclaration _ x y z -> DataDeclaration tn x y z) +-- | @since 1.1.0 instance - (k ~ A_Lens, a ~ ScopeBoundary, b ~ ScopeBoundary) => - LabelOptic "currentScope" k (PrettyContext ann) (PrettyContext ann) a b + (k ~ A_Fold, a ~ Count "tyvar", b ~ Count "tyvar") => + LabelOptic "datatypeBinders" k (DataDeclaration c) (DataDeclaration c) a b where {-# INLINEABLE labelOptic #-} labelOptic = - lens - (\(PrettyContext _ x _) -> x) - (\(PrettyContext x _ z) y -> PrettyContext x y z) + folding $ \case + DataDeclaration _ cnt _ _ -> Just cnt + _ -> Nothing +-- | @since 1.1.0 instance - (k ~ A_Lens, a ~ [Doc ann], b ~ [Doc ann]) => - LabelOptic "varStream" k (PrettyContext ann) (PrettyContext ann) a b + (k ~ A_Fold, a ~ Vector (Constructor c), b ~ Vector (Constructor c)) => + LabelOptic "datatypeConstructors" k (DataDeclaration c) (DataDeclaration c) a b where {-# INLINEABLE labelOptic #-} labelOptic = + folding $ \case + DataDeclaration _ _ ctors _ -> Just ctors + _ -> Nothing + +-- | @since 1.1.0 +instance + (k ~ A_Lens, a ~ DataEncoding, b ~ DataEncoding) => + LabelOptic "datatypeEncoding" k (DataDeclaration c) (DataDeclaration c) a b + where + {-# INLINEABLE labelOptic #-} + labelOptic = lens - (\(PrettyContext _ _ x) -> x) - (\(PrettyContext x y _) z -> PrettyContext x y z) + (\case OpaqueData {} -> BuiltinStrategy InternalOpaqueStrat; DataDeclaration _ _ _ enc -> enc) + (\decl enc -> case decl of OpaqueData tn x -> OpaqueData tn x; DataDeclaration tn x y _ -> DataDeclaration tn x y enc) --- Maybe make a newtype with error reporting since this can fail, but do later since *should't* fail -newtype PrettyM (ann :: Type) (a :: Type) = PrettyM (Reader (PrettyContext ann) a) - deriving - ( Functor, - Applicative, - Monad, - MonadReader (PrettyContext ann) - ) - via (Reader (PrettyContext ann)) +checkStrategy :: forall (a :: Type). DataDeclaration a -> Bool +checkStrategy = \case + OpaqueData _ _ -> True + DataDeclaration tn _ ctors strat -> case strat of + SOP -> True + BuiltinStrategy internalStrat -> case internalStrat of + InternalListStrat -> tn == "List" + InternalPairStrat -> tn == "Pair" + InternalDataStrat -> tn == "Data" + InternalAssocMapStrat -> tn == "Map" + InternalOpaqueStrat -> False + PlutusData plutusStrat -> case plutusStrat of + ConstrData -> True + EnumData -> all (\(Constructor _ args) -> null args) ctors + ProductListData -> length ctors == 1 + NewtypeData -> case ctors of + ConsV x NilV -> case preview #constructorArgs x of + Just (ConsV _ NilV) -> True + _ -> False + _ -> False -runPrettyM :: forall (ann :: Type) (a :: Type). PrettyM ann a -> a -runPrettyM (PrettyM ma) = runReader ma (PrettyContext mempty 0 infiniteVars) +naturalBaseFunctor :: DataDeclaration AbstractTy +naturalBaseFunctor = DataDeclaration "Natural_F" count1 constrs SOP where - -- Lazily generated infinite list of variables. Will start with a, b, c... - -- and cycle around to a1, b2, c3 etc. - -- We could do something more sophisticated but this should work. - infiniteVars :: [Doc ann] - infiniteVars = - let aToZ = ['a' .. 'z'] - intStrings = ("" <$ aToZ) <> map (show @Integer) [0 ..] - in zipWith (\x xs -> pretty (x : xs)) aToZ intStrings + constrs :: Vector (Constructor AbstractTy) + constrs = + [ Constructor "ZeroNat_F" [], + Constructor "SuccNat_F" [Abstraction . BoundAt Z $ ix0] + ] +negativeBaseFunctor :: DataDeclaration AbstractTy +negativeBaseFunctor = DataDeclaration "Negative_F" count1 constrs SOP + where + constrs :: Vector (Constructor AbstractTy) + constrs = + [ Constructor "ZeroNeg_F" [], + Constructor "PredNeg_F" [Abstraction . BoundAt Z $ ix0] + ] + +byteStringBaseFunctor :: DataDeclaration AbstractTy +byteStringBaseFunctor = DataDeclaration "ByteString_F" count1 constrs SOP + where + constrs :: Vector (Constructor AbstractTy) + constrs = + [ Constructor "EmptyByteString_F" [], + Constructor "ConsByteString_F" [BuiltinFlat IntegerT, Abstraction . BoundAt Z $ ix0] + ] + +-- Helpers + prettyCompTWithContext :: forall (ann :: Type). CompT Renamed -> PrettyM ann (Doc ann) prettyCompTWithContext (CompT count (CompTBody funArgs)) - | review intCount count == 0 = prettyFunTy funArgs + | review intCount count == 0 = prettyFunTy' funArgs | otherwise = bindVars count $ \newVars -> do - funTy <- prettyFunTy funArgs + funTy <- prettyFunTy' funArgs pure $ mkForall newVars funTy -prettyFunTy :: +prettyFunTy' :: forall (ann :: Type). NonEmptyVector (ValT Renamed) -> PrettyM ann (Doc ann) -prettyFunTy args = case NonEmpty.uncons args of - (arg, rest) -> Vector.foldl' go (("!" <>) <$> prettyArg arg) rest - where - go :: - PrettyM ann (Doc ann) -> - ValT Renamed -> - PrettyM ann (Doc ann) - go acc t = (\x y -> x <+> "->" <+> y) <$> prettyArg t <*> acc - prettyArg :: ValT Renamed -> PrettyM ann (Doc ann) - prettyArg vt = - let prettyVT = prettyValTWithContext vt - in if isSimpleValT vt - then prettyVT - else parens <$> prettyVT - -bindVars :: - forall (ann :: Type) (a :: Type). - Count "tyvar" -> - (Vector (Doc ann) -> PrettyM ann a) -> - PrettyM ann a -bindVars count' act - | count == 0 = crossBoundary (act Vector.empty) - | otherwise = crossBoundary $ do - here <- asks (view #currentScope) - withFreshVarNames count $ \newBoundVars -> - local (over #boundIdents (Map.insert here newBoundVars)) (act newBoundVars) - where - -- Increment the current scope - crossBoundary :: PrettyM ann a -> PrettyM ann a - crossBoundary = local (over #currentScope (+ 1)) - count :: Int - count = review intCount count' - -mkForall :: - forall (ann :: Type). - Vector (Doc ann) -> - Doc ann -> - Doc ann -mkForall tvars funTyBody = - if Vector.null tvars - then funTyBody - else "forall" <+> hsep (Vector.toList tvars) <> "." <+> funTyBody - --- I.e. can we omit parens and get something unambiguous? This might be overly aggressive w/ parens but that's OK -isSimpleValT :: forall (a :: Type). ValT a -> Bool -isSimpleValT = \case - ThunkT thunk -> isSimpleCompT thunk - _ -> True - where - isSimpleCompT :: CompT a -> Bool - isSimpleCompT (CompT count (CompTBody args)) = - review intCount count == 0 && NonEmpty.length args == 1 +prettyFunTy' args = case NonEmpty.unsnoc args of + (rest, resTy) -> do + resTy' <- ("!" <>) <$> prettyValTWithContext resTy + case Vector.uncons rest of + Nothing -> pure resTy' + Just (firstArg, otherArgs) -> do + prettyArg1 <- prettyValTWithContext firstArg + argsWithoutResult <- Vector.foldM (\acc x -> (\z -> acc <+> "->" <+> z) <$> prettyValTWithContext x) prettyArg1 otherArgs + pure . parens $ argsWithoutResult <+> "->" <+> resTy' prettyValTWithContext :: forall (ann :: Type). ValT Renamed -> PrettyM ann (Doc ann) prettyValTWithContext = \case Abstraction abstr -> prettyRenamedWithContext abstr ThunkT compT -> prettyCompTWithContext compT BuiltinFlat biFlat -> pure $ viaShow biFlat + Datatype (TyName tn) args -> do + args' <- traverse prettyValTWithContext args + let tn' = pretty tn + case Vector.toList args' of + [] -> pure tn' + argsList -> pure . parens $ tn' <+> hsep argsList --- Generate N fresh var names and use the supplied monadic function to do something with them. -withFreshVarNames :: - forall (ann :: Type) (a :: Type). - Int -> - (Vector (Doc ann) -> PrettyM ann a) -> - PrettyM ann a -withFreshVarNames n act = do - stream <- asks (view #varStream) - let (used, rest) = splitAt n stream - local (set #varStream rest) . act . fromListN n $ used +prettyCtorWithContext :: forall (ann :: Type). Constructor Renamed -> PrettyM ann (Doc ann) +prettyCtorWithContext (Constructor ctorNm ctorArgs) + | Vector.null ctorArgs = pure $ pretty (runConstructorName ctorNm) + | otherwise = do + let ctorNm' = pretty (runConstructorName ctorNm) + args' <- Vector.toList <$> traverse prettyValTWithContext ctorArgs + pure $ ctorNm' <+> hsep args' prettyRenamedWithContext :: forall (ann :: Type). Renamed -> PrettyM ann (Doc ann) prettyRenamedWithContext = \case @@ -357,19 +512,21 @@ Unifiable i -> lookupAbstraction 0 i Wildcard w64 offset i -> pure $ pretty offset <> "_" <> viaShow w64 <> "#" <> pretty (review intIndex i) -lookupAbstraction :: forall (ann :: Type). Int -> Index "tyvar" -> PrettyM ann (Doc ann) -lookupAbstraction offset argIndex = do - let scopeOffset = ScopeBoundary offset - let argIndex' = review intIndex argIndex - here <- asks (view #currentScope) - asks (preview (#boundIdents % ix (here + scopeOffset) % ix argIndex')) >>= \case - Nothing -> - -- TODO: actual error reporting - error $ - "Internal error: The encountered a variable at arg index " - <> show argIndex' - <> " with true level " - <> show scopeOffset - <> " but could not locate the corresponding pretty form at scope level " - <> show here - Just res' -> pure res' +prettyDataDeclWithContext :: forall (ann :: Type). DataDeclaration Renamed -> PrettyM ann (Doc ann) +prettyDataDeclWithContext (OpaqueData (TyName tn) _) = pure . pretty $ tn +prettyDataDeclWithContext (DataDeclaration (TyName tn) numVars ctors _) = bindVars numVars $ \boundVars -> do + let tn' = pretty tn + ctors' <- traverse prettyCtorWithContext ctors + let prettyCtors = indent 2 . vcat . prefix "| " . Vector.toList $ ctors' + if Vector.null ctors + then pure $ "data" <+> tn' <+> hsep (Vector.toList boundVars) + else pure $ "data" <+> tn' <+> hsep (Vector.toList boundVars) <+> "=" <+> prettyCtors + where + -- I don't think there's a library fn that does this? This is for the `|` in a sum type. + prefix :: Doc ann -> [Doc ann] -> [Doc ann] + prefix _ [] = [] + prefix _ [x] = [x] + prefix sep (x : xs) = x : goPrefix xs + where + goPrefix [] = [] + goPrefix (y : ys) = (sep <> y) : goPrefix ys diff --git a/src/Covenant/Internal/Unification.hs b/src/Covenant/Internal/Unification.hs --- a/src/Covenant/Internal/Unification.hs +++ b/src/Covenant/Internal/Unification.hs @@ -3,22 +3,29 @@ module Covenant.Internal.Unification ( TypeAppError (..), checkApp, + runUnifyM, + UnifyM, ) where -import Control.Monad (foldM, unless) +import Control.Monad (foldM, unless, when) import Data.Ord (comparing) #if __GLASGOW_HASKELL__==908 import Data.Foldable (foldl') #endif -import Control.Monad.Except (catchError, throwError) +import Control.Monad.Except (MonadError, catchError, throwError) +import Control.Monad.Reader (MonadReader, ReaderT (runReaderT), ask) +import Covenant.Data (DatatypeInfo) import Covenant.Index (Index, intCount, intIndex) +import Covenant.Internal.Rename (RenameError, renameDatatypeInfo) import Covenant.Internal.Type - ( BuiltinFlatT, + ( AbstractTy, + BuiltinFlatT, CompT (CompT), CompTBody (CompTBody), Renamed (Rigid, Unifiable, Wildcard), - ValT (Abstraction, BuiltinFlat, ThunkT), + TyName, + ValT (Abstraction, BuiltinFlat, Datatype, ThunkT), ) import Data.Kind (Type) import Data.Map (Map) @@ -27,13 +34,17 @@ import Data.Maybe (fromJust, mapMaybe) import Data.Set (Set) import Data.Set qualified as Set +import Data.Text (Text) import Data.Vector (Vector) import Data.Vector qualified as Vector +import Data.Vector.NonEmpty (NonEmptyVector) import Data.Vector.NonEmpty qualified as NonEmpty import Data.Word (Word64) -import Optics.Core (preview) +import Optics.Core (ix, preview, view) --- | @since 1.0.0 +-- | Possible errors resulting from applications of arguments to functions. +-- +-- @since 1.0.0 data TypeAppError = -- | The final type after all arguments are applied is @forall a . a@. LeakingUnifiable (Index "tyvar") @@ -42,10 +53,29 @@ | -- | We were given too many arguments. ExcessArgs (CompT Renamed) (Vector (Maybe (ValT Renamed))) | -- | We weren't given enough arguments. - InsufficientArgs (CompT Renamed) + -- + -- @since 1.1.0 + InsufficientArgs Int (CompT Renamed) [Maybe (ValT Renamed)] | -- | The expected type (first field) and actual type (second field) do not -- unify. DoesNotUnify (ValT Renamed) (ValT Renamed) + | -- | No datatype info associated with requested TyName + -- + -- @since 1.1.0 + NoDatatypeInfo TyName + | -- | No BB form. The only datatypes which should lack one are those isomorphic to `Void`. + -- + -- @since 1.1.0 + NoBBForm TyName + | -- | Datatype renaming failed. + -- + -- @since 1.1.0 + DatatypeInfoRenameFailed TyName RenameError + | -- | Something happened that definitely should not have. For right now, this means: The BB form of a datatype isn't a thunk + -- (but it might be useful to keep this around as a catchall for things that really shouldn't happen). + -- + -- @since 1.1.0 + ImpossibleHappened Text deriving stock ( -- | @since 1.0.0 Eq, @@ -53,17 +83,68 @@ Show ) --- | @since 1.0.0 -checkApp :: CompT Renamed -> [Maybe (ValT Renamed)] -> Either TypeAppError (ValT Renamed) -checkApp f@(CompT _ (CompTBody xs)) = +{- This will probably only get used directly in testing and we'll use capabilities w/ the class everywhere else? -} +newtype UnifyM a = UnifyM (ReaderT (Map TyName (DatatypeInfo AbstractTy)) (Either TypeAppError) a) + deriving + ( -- | @since 1.1.0 + Functor, + Applicative, + Monad, + MonadReader (Map TyName (DatatypeInfo AbstractTy)), + MonadError TypeAppError + ) + via (ReaderT (Map TyName (DatatypeInfo AbstractTy)) (Either TypeAppError)) + +runUnifyM :: Map TyName (DatatypeInfo AbstractTy) -> UnifyM a -> Either TypeAppError a +runUnifyM tyDict (UnifyM act) = runReaderT act tyDict + +lookupDatatypeInfo :: + TyName -> + UnifyM (DatatypeInfo Renamed) +lookupDatatypeInfo tn = + ask >>= \tyDict -> case preview (ix tn) tyDict of + Nothing -> throwError $ NoDatatypeInfo tn + Just dti -> either (throwError . DatatypeInfoRenameFailed tn) pure $ renameDatatypeInfo dti + +lookupBBForm :: TyName -> UnifyM (ValT Renamed) +lookupBBForm tn = + lookupDatatypeInfo tn >>= \dti -> case view #bbForm dti of + Nothing -> throwError $ NoBBForm tn + Just bbForm -> pure bbForm + +-- | Given information about in-scope datatypes, a computation type, and a list +-- of arguments (some of which may be errors), try to construct the type of the +-- result of the application of those arguments to the computation. +-- +-- @since 1.0.0 +checkApp :: + Map TyName (DatatypeInfo AbstractTy) -> + CompT Renamed -> + [Maybe (ValT Renamed)] -> + Either TypeAppError (ValT Renamed) +checkApp tyDict f args = runUnifyM tyDict $ checkApp' f args + +checkApp' :: + CompT Renamed -> + [Maybe (ValT Renamed)] -> + UnifyM (ValT Renamed) +checkApp' f@(CompT _ (CompTBody xs)) ys = do let (curr, rest) = NonEmpty.uncons xs - in go curr (Vector.toList rest) + numArgsExpected = NonEmpty.length xs - 1 + numArgsActual = length ys + when (numArgsActual < numArgsExpected) $ + throwError $ + InsufficientArgs numArgsActual f ys + when (numArgsExpected > numArgsActual) $ + throwError $ + ExcessArgs f (Vector.fromList ys) + go curr (Vector.toList rest) ys where go :: ValT Renamed -> [ValT Renamed] -> [Maybe (ValT Renamed)] -> - Either TypeAppError (ValT Renamed) + UnifyM (ValT Renamed) go currParam restParams args = case restParams of [] -> case args of -- If we got here, currParam is the resulting type after all @@ -71,7 +152,7 @@ [] -> fixUp currParam _ -> throwError . ExcessArgs f . Vector.fromList $ args _ -> case args of - [] -> throwError . InsufficientArgs $ f + [] -> throwError $ InsufficientArgs (length args) f args (currArg : restArgs) -> do newRestParams <- case currArg of -- An error argument unifies with anything, as it's effectively @@ -82,7 +163,7 @@ subs <- catchError (unify currParam currArg') (promoteUnificationError currParam currArg') pure . Map.foldlWithKey' applySub restParams $ subs case newRestParams of - [] -> throwError . InsufficientArgs $ f + [] -> throwError $ InsufficientArgs (length args) f args (currParam' : restParams') -> go currParam' restParams' restArgs -- Helpers @@ -109,6 +190,7 @@ ThunkT (CompT abstractions (CompTBody xs)) -> ThunkT . CompT abstractions . CompTBody . fmap (substitute index toSub) $ xs BuiltinFlat t -> BuiltinFlat t + Datatype tn args -> Datatype tn $ substitute index toSub <$> args -- Because unification is inherently recursive, if we find an error deep within -- a type, the message will signify only the _part_ that fails to unify, not the @@ -117,17 +199,16 @@ -- function, which effectively allows us to rename the types reported in -- unification errors to whatever types 'wrap' them. promoteUnificationError :: - forall (a :: Type). ValT Renamed -> ValT Renamed -> TypeAppError -> - Either TypeAppError a + UnifyM a promoteUnificationError topLevelExpected topLevelActual = - Left . \case + throwError . \case DoesNotUnify _ _ -> DoesNotUnify topLevelExpected topLevelActual err -> err -fixUp :: ValT Renamed -> Either TypeAppError (ValT Renamed) +fixUp :: ValT Renamed -> UnifyM (ValT Renamed) fixUp = \case -- We have a result that's effectively `forall a . a` but not an error Abstraction (Unifiable index) -> throwError . LeakingUnifiable $ index @@ -162,11 +243,12 @@ _ -> Set.empty BuiltinFlat _ -> Set.empty ThunkT (CompT _ (CompTBody xs)) -> NonEmpty.foldl' (\acc t -> acc <> collectUnifiables t) Set.empty xs + Datatype _ args -> Vector.foldl' (\acc t -> acc <> collectUnifiables t) Set.empty args unify :: ValT Renamed -> ValT Renamed -> - Either TypeAppError (Map (Index "tyvar") (ValT Renamed)) + UnifyM (Map (Index "tyvar") (ValT Renamed)) unify expected actual = catchError ( case expected of @@ -177,15 +259,16 @@ Wildcard scopeId1 _ index1 -> expectWildcard scopeId1 index1 ThunkT t1 -> expectThunk t1 BuiltinFlat t1 -> expectFlatBuiltin t1 + Datatype tn xs -> expectDatatype tn xs ) (promoteUnificationError expected actual) where - unificationError :: forall (a :: Type). Either TypeAppError a - unificationError = Left . DoesNotUnify expected $ actual - noSubUnify :: forall (k :: Type) (a :: Type). Either TypeAppError (Map k a) + unificationError :: forall (a :: Type). UnifyM a + unificationError = throwError . DoesNotUnify expected $ actual + noSubUnify :: forall (k :: Type) (a :: Type). UnifyM (Map k a) noSubUnify = pure Map.empty expectRigid :: - Int -> Index "tyvar" -> Either TypeAppError (Map (Index "tyvar") (ValT Renamed)) + Int -> Index "tyvar" -> UnifyM (Map (Index "tyvar") (ValT Renamed)) -- Rigids behave identically to concrete types: they can unify with -- themselves, or any other abstraction, but nothing else. No substitutional -- rewrites are needed. @@ -197,7 +280,7 @@ Abstraction _ -> noSubUnify _ -> unificationError expectWildcard :: - Word64 -> Index "tyvar" -> Either TypeAppError (Map (Index "tyvar") (ValT Renamed)) + Word64 -> Index "tyvar" -> UnifyM (Map (Index "tyvar") (ValT Renamed)) -- Wildcards can unify with unifiables, as well as themselves, but nothing -- else. No substitutional rewrites are needed. expectWildcard scopeId1 index1 = case actual of @@ -207,7 +290,7 @@ then noSubUnify else unificationError _ -> unificationError - expectThunk :: CompT Renamed -> Either TypeAppError (Map (Index "tyvar") (ValT Renamed)) + expectThunk :: CompT Renamed -> UnifyM (Map (Index "tyvar") (ValT Renamed)) -- Thunks unify unconditionally with wildcards or unifiables. They unify -- conditionally with other thunks, provided that we can unify each argument -- with its counterpart in the same position, as well as their result types, @@ -221,7 +304,7 @@ (foldM (\acc (l, r) -> unify l r >>= reconcile acc) Map.empty . NonEmpty.zip t1 $ t2) (promoteUnificationError expected actual) _ -> unificationError - expectFlatBuiltin :: BuiltinFlatT -> Either TypeAppError (Map (Index "tyvar") (ValT Renamed)) + expectFlatBuiltin :: BuiltinFlatT -> UnifyM (Map (Index "tyvar") (ValT Renamed)) -- 'Flat' builtins are always concrete. They can unify with themselves, -- unifiables or wildcards, but nothing else. No substitutional rewrites are -- needed. @@ -233,10 +316,38 @@ then noSubUnify else unificationError _ -> unificationError + expectDatatype :: TyName -> Vector (ValT Renamed) -> UnifyM (Map (Index "tyvar") (ValT Renamed)) + -- Datatypes unify with wildcards or unifiables, or other "suitable" instances of the same datatype. + -- Suitability with other datatypes is determined by converting to BB form, then concretifying + -- the BB form using the arguments to the actual datatype. + -- For example, the BB form of `Maybe` is: forall a r. r -> (a -> r) -> r + -- which, if we concretify while attempting to unify with `Maybe Int`, becomes: `forall r. r -> (Int -> r) -> r` + expectDatatype tn args = do + bbForm <- lookupBBForm tn + bbFormConcreteE <- concretify bbForm args + case actual of + Abstraction (Rigid _ _) -> unificationError + Abstraction _ -> noSubUnify + Datatype tn' args' + | tn' /= tn -> unificationError + | otherwise -> do + bbFormConcreteA <- concretify bbForm args' + unify bbFormConcreteE bbFormConcreteA + _ -> unificationError + concretify :: ValT Renamed -> Vector (ValT Renamed) -> UnifyM (ValT Renamed) + concretify (ThunkT (CompT count (CompTBody fn))) args = fixUp $ ThunkT (CompT count (CompTBody newFn)) + where + indexedArgs :: [(Index "tyvar", ValT Renamed)] + indexedArgs = Vector.toList $ Vector.imap (\i x -> (fromJust . preview intIndex $ i, x)) args + newFn :: NonEmptyVector (ValT Renamed) + newFn = go indexedArgs <$> fn + go :: [(Index "tyvar", ValT Renamed)] -> ValT Renamed -> ValT Renamed + go subs arg = foldl' (\val (i, concrete) -> substitute i concrete val) arg subs + concretify _ _ = throwError $ ImpossibleHappened "bbForm is not a thunk" reconcile :: Map (Index "tyvar") (ValT Renamed) -> Map (Index "tyvar") (ValT Renamed) -> - Either TypeAppError (Map (Index "tyvar") (ValT Renamed)) + UnifyM (Map (Index "tyvar") (ValT Renamed)) -- Note (Koz, 14/04/2025): This utter soup means the following: -- -- - If the old map and the new map don't have any overlapping assignments, @@ -248,4 +359,13 @@ Merge.mergeA Merge.preserveMissing Merge.preserveMissing - (Merge.zipWithAMatched $ \_ l r -> l <$ unless (l == r) unificationError) + (Merge.zipWithAMatched combineBindings) + combineBindings :: Index "tyvar" -> ValT Renamed -> ValT Renamed -> UnifyM (ValT Renamed) + combineBindings _ old new = + if old == new + then pure old + else case old of + Abstraction (Unifiable _) -> pure new + _ -> case new of + Abstraction (Unifiable _) -> pure old + _ -> unificationError diff --git a/src/Covenant/Prim.hs b/src/Covenant/Prim.hs --- a/src/Covenant/Prim.hs +++ b/src/Covenant/Prim.hs @@ -7,12 +7,6 @@ -- Contains definitions relating to Plutus primitive functions in Covenant -- programs. -- --- = Note --- --- In the 1.0.0 release, we didn't include non-flat builtin types, specifically --- pairs, lists and @Data@. Thus, the primops that operate on, or produce, these --- are not currently included. --- -- @since 1.0.0 module Covenant.Prim ( OneArgFunc (..), @@ -21,20 +15,23 @@ typeTwoArgFunc, ThreeArgFunc (..), typeThreeArgFunc, - -- SixArgFunc (..), - -- typeSixArgFunc, + SixArgFunc (..), + typeSixArgFunc, ) where -import Covenant.DeBruijn (DeBruijn (Z)) -import Covenant.Index (ix0) +import Covenant.DeBruijn (DeBruijn (S, Z)) +import Covenant.Index (ix0, ix1) import Covenant.Type ( AbstractTy, - CompT (Comp0, Comp1), + CompT (Comp0, Comp1, Comp2), CompTBody (ReturnT, (:--:>)), - ValT, + ValT (ThunkT), boolT, byteStringT, + dataType1T, + dataType2T, + dataTypeT, g1T, g2T, integerT, @@ -55,10 +52,7 @@ -- to directly \'lift\' empty list constants into itself. Secondly, while these -- primitives /could/ still be used instead of direct lifts, there is never a -- reason to prefer them, as they are less efficient than embedding a constant --- directly. Thirdly, their naive typings would end up with overdetermined type --- variables - consider the typing of @MkNilData@: --- --- @forall a . () -> ![a]@ +-- directly. -- -- For all of these reasons, we do not represent these primitives in the ASG. -- @@ -70,22 +64,37 @@ | Blake2b_256 | EncodeUtf8 | DecodeUtf8 - | -- | FstPair - -- | SndPair - -- | HeadList - -- | TailList - -- | NullList - -- | MapData - -- | ListData - -- | IData - -- | BData - -- | UnConstrData - -- | UnMapData - -- | UnListData - -- | UnIData - -- | UnBData - -- | SerialiseData - BLS12_381_G1_neg + | -- | @since 1.1.0 + FstPair + | -- | @since 1.1.0 + SndPair + | -- | @since 1.1.0 + HeadList + | -- | @since 1.1.0 + TailList + | -- | @since 1.1.0 + NullList + | -- | @since 1.1.0 + MapData + | -- | @since 1.1.0 + ListData + | -- | @since 1.1.0 + IData + | -- | @since 1.1.0 + BData + | -- | @since 1.1.0 + UnConstrData + | -- | @since 1.1.0 + UnMapData + | -- | @since 1.1.0 + UnListData + | -- | @since 1.1.0 + UnIData + | -- | @since 1.1.0 + UnBData + | -- | @since 1.1.0 + SerialiseData + | BLS12_381_G1_neg | BLS12_381_G1_compress | BLS12_381_G1_uncompress | BLS12_381_G2_neg @@ -119,21 +128,21 @@ Blake2b_256, EncodeUtf8, DecodeUtf8, - -- FstPair, - -- SndPair, - -- HeadList, - -- TailList, - -- NullList, - -- MapData, - -- ListData, - -- IData, - -- BData, - -- UnConstrData, - -- UnMapData, - -- UnListData, - -- UnIData, - -- UnBData, - -- SerialiseData, + FstPair, + SndPair, + HeadList, + TailList, + NullList, + MapData, + ListData, + IData, + BData, + UnConstrData, + UnMapData, + UnListData, + UnIData, + UnBData, + SerialiseData, BLS12_381_G1_neg, BLS12_381_G1_compress, BLS12_381_G1_uncompress, @@ -159,6 +168,21 @@ Blake2b_256 -> hashingT EncodeUtf8 -> Comp0 $ stringT :--:> ReturnT byteStringT DecodeUtf8 -> Comp0 $ byteStringT :--:> ReturnT stringT + FstPair -> Comp2 $ pairT aT bT :--:> ReturnT aT + SndPair -> Comp2 $ pairT aT bT :--:> ReturnT bT + HeadList -> Comp1 $ listT aT :--:> ReturnT aT + TailList -> Comp1 $ listT aT :--:> ReturnT (listT aT) + NullList -> Comp1 $ listT aT :--:> ReturnT boolT + MapData -> Comp0 $ listT (pairT dataT dataT) :--:> ReturnT dataT + ListData -> Comp0 $ listT dataT :--:> ReturnT dataT + IData -> Comp0 $ integerT :--:> ReturnT dataT + BData -> Comp0 $ byteStringT :--:> ReturnT dataT + UnConstrData -> Comp0 $ dataT :--:> ReturnT (pairT integerT (listT dataT)) + UnMapData -> Comp0 $ dataT :--:> ReturnT (listT (pairT dataT dataT)) + UnListData -> Comp0 $ dataT :--:> ReturnT (listT dataT) + UnIData -> Comp0 $ dataT :--:> ReturnT integerT + UnBData -> Comp0 $ dataT :--:> ReturnT byteStringT + SerialiseData -> Comp0 $ dataT :--:> ReturnT byteStringT BLS12_381_G1_neg -> Comp0 $ g1T :--:> ReturnT g1T BLS12_381_G1_compress -> Comp0 $ g1T :--:> ReturnT byteStringT BLS12_381_G1_uncompress -> Comp0 $ byteStringT :--:> ReturnT g1T @@ -199,11 +223,15 @@ | EqualsString | ChooseUnit | Trace - | -- | MkCons - -- | ConstrData - -- | EqualsData - -- | MkPairData - BLS12_381_G1_add + | -- | @since 1.1.0 + MkCons + | -- | @since 1.1.0 + ConstrData + | -- | @since 1.1.0 + EqualsData + | -- | @since 1.1.0 + MkPairData + | BLS12_381_G1_add | BLS12_381_G1_scalarMul | BLS12_381_G1_equal | BLS12_381_G1_hashToGroup @@ -255,10 +283,10 @@ EqualsString, ChooseUnit, Trace, - -- MkCons, - -- ConstrData, - -- EqualsData, - -- MkPairData, + MkCons, + ConstrData, + EqualsData, + MkPairData, BLS12_381_G1_add, BLS12_381_G1_scalarMul, BLS12_381_G1_equal, @@ -300,8 +328,12 @@ LessThanEqualsByteString -> compareT byteStringT AppendString -> combineT stringT EqualsString -> compareT stringT - ChooseUnit -> Comp1 $ unitT :--:> tyvar Z ix0 :--:> ReturnT (tyvar Z ix0) - Trace -> Comp1 $ stringT :--:> tyvar Z ix0 :--:> ReturnT (tyvar Z ix0) + ChooseUnit -> Comp1 $ unitT :--:> aT :--:> ReturnT aT + Trace -> Comp1 $ stringT :--:> aT :--:> ReturnT aT + MkCons -> Comp1 $ aT :--:> listT aT :--:> ReturnT (listT aT) + ConstrData -> Comp0 $ integerT :--:> listT dataT :--:> ReturnT dataT + EqualsData -> compareT dataT + MkPairData -> Comp0 $ dataT :--:> dataT :--:> ReturnT (pairT dataT dataT) BLS12_381_G1_add -> combineT g1T BLS12_381_G1_scalarMul -> Comp0 $ integerT :--:> g1T :--:> ReturnT g1T BLS12_381_G1_equal -> compareT g1T @@ -332,14 +364,16 @@ | VerifyEcdsaSecp256k1Signature | VerifySchnorrSecp256k1Signature | IfThenElse - | -- | ChooseList - -- | CaseList - IntegerToByteString + | -- | @since 1.1.0 + ChooseList + | -- | @since 1.1.0 + CaseList + | IntegerToByteString | AndByteString | OrByteString | XorByteString - | -- | WriteBits - ExpModInteger + | WriteBits + | ExpModInteger deriving stock ( -- | @since 1.0.0 Eq, @@ -360,13 +394,13 @@ VerifyEcdsaSecp256k1Signature, VerifySchnorrSecp256k1Signature, IfThenElse, - -- ChooseList, - -- CaseList, + ChooseList, + CaseList, IntegerToByteString, AndByteString, OrByteString, XorByteString, - -- WriteBits, + WriteBits, ExpModInteger ] @@ -378,18 +412,23 @@ VerifyEd25519Signature -> signatureT VerifyEcdsaSecp256k1Signature -> signatureT VerifySchnorrSecp256k1Signature -> signatureT - IfThenElse -> - Comp1 $ - boolT - :--:> tyvar Z ix0 - :--:> tyvar Z ix0 - :--:> ReturnT (tyvar Z ix0) + IfThenElse -> Comp1 $ boolT :--:> aT :--:> aT :--:> ReturnT aT + ChooseList -> Comp2 $ listT aT :--:> bT :--:> bT :--:> ReturnT bT + CaseList -> + Comp2 $ + bT + :--:> ThunkT (Comp0 $ aTOuter :--:> listT aTOuter :--:> ReturnT bTOuter) + :--:> listT aT + :--:> ReturnT bT IntegerToByteString -> Comp0 $ boolT :--:> integerT :--:> integerT :--:> ReturnT byteStringT AndByteString -> bitwiseT OrByteString -> bitwiseT XorByteString -> bitwiseT + WriteBits -> + Comp0 $ + byteStringT :--:> listT integerT :--:> boolT :--:> ReturnT byteStringT ExpModInteger -> Comp0 $ integerT @@ -412,10 +451,9 @@ :--:> byteStringT :--:> ReturnT byteStringT -{- -- | All six-argument primitives provided by Plutus. -- --- @since 1.0.0 +-- @since 1.1.0 data SixArgFunc = ChooseData | CaseData @@ -430,8 +468,54 @@ -- | Does not shrink. -- --- @since 1.0.0 +-- @since 1.1.0 instance Arbitrary SixArgFunc where {-# INLINEABLE arbitrary #-} arbitrary = elements [ChooseData, CaseData] --} + +-- | Produce the type of a six-argument primop. +-- +-- @since 1.1.0 +typeSixArgFunc :: SixArgFunc -> CompT AbstractTy +typeSixArgFunc = \case + ChooseData -> + Comp1 $ + dataT + :--:> aT + :--:> aT + :--:> aT + :--:> aT + :--:> aT + :--:> ReturnT aT + CaseData -> + Comp1 $ + ThunkT (Comp0 $ integerT :--:> listT dataT :--:> ReturnT aTOuter) + :--:> ThunkT (Comp0 $ listT (pairT dataT dataT) :--:> ReturnT aTOuter) + :--:> ThunkT (Comp0 $ listT dataT :--:> ReturnT aTOuter) + :--:> ThunkT (Comp0 $ integerT :--:> ReturnT aTOuter) + :--:> ThunkT (Comp0 $ byteStringT :--:> ReturnT aTOuter) + :--:> dataT + :--:> ReturnT aT + +-- Helpers + +dataT :: ValT AbstractTy +dataT = dataTypeT "Data" + +listT :: ValT AbstractTy -> ValT AbstractTy +listT = dataType1T "List" + +pairT :: ValT AbstractTy -> ValT AbstractTy -> ValT AbstractTy +pairT = dataType2T "Pair" + +aT :: ValT AbstractTy +aT = tyvar Z ix0 + +aTOuter :: ValT AbstractTy +aTOuter = tyvar (S Z) ix0 + +bT :: ValT AbstractTy +bT = tyvar Z ix1 + +bTOuter :: ValT AbstractTy +bTOuter = tyvar (S Z) ix1 diff --git a/src/Covenant/Test.hs b/src/Covenant/Test.hs --- a/src/Covenant/Test.hs +++ b/src/Covenant/Test.hs @@ -1,21 +1,124 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE PolyKinds #-} + -- | -- Module: Covenant.Test -- Copyright: (C) MLabs 2025 -- License: Apache 2.0 -- Maintainer: koz@mlabs.city, sean@mlabs.city -- --- Utilities designed to help test Covenant itself. +-- Various utilities designed to help test Covenant. -- +-- = Note +-- +-- This is probably not that useful to end users of Covenant, but needs to be +-- exposed so the tests can use this functionality. +-- -- @since 1.0.0 module Covenant.Test - ( Concrete (Concrete), + ( -- * QuickCheck data wrappers + Concrete (Concrete), + DataDeclFlavor (ConcreteDecl, ConcreteNestedDecl, SimpleRecursive, Poly1, Poly1PolyThunks), + DataDeclSet (DataDeclSet), + + -- * Functions + + -- ** Lifted QuickCheck functions + chooseInt, + scale, + + -- ** 'DataDeclSet' functionality + prettyDeclSet, + + -- ** Test helpers + checkApp, + failLeft, + tyAppTestDatatypes, + list, + tree, + weirderList, + unsafeTyCon, + + -- ** Datatype checks + cycleCheck, + checkDataDecls, + checkEncodingArgs, + + -- ** Renaming + + -- *** Types + RenameError (..), + RenameM, + + -- *** Introduction + renameValT, + renameCompT, + renameDataDecl, + + -- *** Elimination + runRenameM, ) where +#if __GLASGOW_HASKELL__==908 +import Data.Foldable (foldl') +#endif import Control.Applicative ((<|>)) -import Covenant.Index (count0) -import Covenant.Type - ( AbstractTy, +import Control.Monad (void) +import Control.Monad.State.Strict + ( MonadState (get, put), + State, + evalState, + gets, + modify, + ) +import Control.Monad.Trans (MonadTrans (lift)) +import Covenant.Data + ( DatatypeInfo, + mkDatatypeInfo, + noPhantomTyVars, + ) +import Covenant.DeBruijn (DeBruijn (Z), asInt) +import Covenant.Index + ( Count, + count0, + count1, + count2, + intCount, + intIndex, + ix0, + ix1, + ) +import Covenant.Internal.KindCheck + ( checkDataDecls, + checkEncodingArgs, + cycleCheck, + ) +import Covenant.Internal.Ledger + ( CtorBuilder (Ctor), + DeclBuilder (Decl), + list, + maybeT, + mkDecl, + pair, + tree, + weirderList, + ) +import Covenant.Internal.PrettyPrint (ScopeBoundary) +import Covenant.Internal.Rename + ( RenameError (InvalidAbstractionReference), + RenameM, + renameCompT, + renameDataDecl, + renameValT, + runRenameM, + ) +import Covenant.Internal.Strategy + ( DataEncoding (PlutusData, SOP), + PlutusDataStrategy (ConstrData), + ) +import Covenant.Internal.Type + ( AbstractTy (BoundAt), BuiltinFlatT ( BLS12_381_G1_ElementT, BLS12_381_G2_ElementT, @@ -26,21 +129,61 @@ StringT, UnitT ), - CompT (Comp0, CompN), + Constructor (Constructor), + ConstructorName (ConstructorName), + DataDeclaration (DataDeclaration, OpaqueData), + TyName (TyName), + ValT (Abstraction, BuiltinFlat, Datatype, ThunkT), + runConstructorName, + ) +import Covenant.Internal.Unification (checkApp) +import Covenant.Type + ( CompT (Comp0, CompN), CompTBody (ArgsAndResult), - ValT (Abstraction, BuiltinFlat, ThunkT), ) +import Covenant.Util (prettyStr) import Data.Coerce (coerce) +import Data.Kind (Type) +import Data.Map.Strict (Map) +import Data.Map.Strict qualified as M +import Data.Maybe (fromJust, mapMaybe) +import Data.Set (Set) +import Data.Set qualified as Set +import Data.Text (Text) +import Data.Text qualified as T +import Data.Vector (Vector) import Data.Vector qualified as Vector +import GHC.Exts (fromListN) +import GHC.Word (Word32) +import Optics.Core + ( A_Lens, + LabelOptic (labelOptic), + folded, + lens, + over, + preview, + review, + set, + toListOf, + view, + (%), + ) import Test.QuickCheck ( Arbitrary (arbitrary, shrink), + Arbitrary1 (liftArbitrary, liftShrink), Gen, elements, - liftArbitrary, - oneof, + frequency, sized, + suchThat, + vectorOf, ) +import Test.QuickCheck qualified as QC (chooseInt) +import Test.QuickCheck.GenT (GenT, MonadGen) +import Test.QuickCheck.GenT qualified as GT +import Test.QuickCheck.Instances.Containers () import Test.QuickCheck.Instances.Vector () +import Test.Tasty.HUnit (assertFailure) -- | Wrapper for 'ValT' to provide an 'Arbitrary' instance to generate only -- value types without any type variables. @@ -77,16 +220,16 @@ BLS12_381_MlResultT ] | otherwise = - oneof - [ pure . BuiltinFlat $ UnitT, - pure . BuiltinFlat $ BoolT, - pure . BuiltinFlat $ IntegerT, - pure . BuiltinFlat $ StringT, - pure . BuiltinFlat $ ByteStringT, - pure . BuiltinFlat $ BLS12_381_G1_ElementT, - pure . BuiltinFlat $ BLS12_381_G2_ElementT, - pure . BuiltinFlat $ BLS12_381_MlResultT, - ThunkT . Comp0 <$> (ArgsAndResult <$> liftArbitrary (go (size `quot` 4)) <*> go (size `quot` 4)) + frequency + [ (10, pure . BuiltinFlat $ UnitT), + (10, pure . BuiltinFlat $ BoolT), + (10, pure . BuiltinFlat $ IntegerT), + (10, pure . BuiltinFlat $ StringT), + (10, pure . BuiltinFlat $ ByteStringT), + (10, pure . BuiltinFlat $ BLS12_381_G1_ElementT), + (10, pure . BuiltinFlat $ BLS12_381_G2_ElementT), + (10, pure . BuiltinFlat $ BLS12_381_MlResultT), + (2, ThunkT . Comp0 <$> (ArgsAndResult <$> liftArbitrary (go (size `quot` 4)) <*> go (size `quot` 4))) ] {-# INLINEABLE shrink #-} shrink (Concrete v) = @@ -102,3 +245,614 @@ pure (ArgsAndResult args' result) <|> pure (ArgsAndResult args result') -- Can't shrink this BuiltinFlat _ -> [] + Datatype tn args -> + Datatype tn <$> do + let argsList = Vector.toList args + (fmap (Vector.fromList . coerce) . shrink . fmap Concrete) argsList + +-- | A \'description type\' designed for use with 'DataDeclSet' to describe what +-- kind of types it contains. +-- +-- @since 1.1.0 +data DataDeclFlavor + = -- | All constructor arguments are concrete and the declaration is monomorphic. + -- + -- @since 1.1.0 + ConcreteDecl + | -- | As 'ConcreteDecl', but can re-use already generated concrete declarations + -- in the context to make nested types. + -- + -- @since 1.1.0 + ConcreteNestedDecl + | -- | Recursive, monomorphic type (such as @data IntList = End | More Int IntList@). + -- + -- @since 1.1.0 + SimpleRecursive + | -- | Polymorphic types in one variable, which may or may not be recursive. + -- + -- @since 1.1.0 + Poly1 + | -- | As 'Poly1', but may have further polymorphism via thunks. + -- + -- @since 1.1.0 + Poly1PolyThunks + +-- | Helper type to generate datatype definitions. Specifically, this stores +-- already-generated datatype declarations for our (re)use when generating. +-- +-- @since 1.1.0 +newtype DataDeclSet (flavor :: DataDeclFlavor) = DataDeclSet [DataDeclaration AbstractTy] + +-- @since 1.1.0 +instance Arbitrary (DataDeclSet 'ConcreteDecl) where + arbitrary = coerce $ genDataList genConcreteDataDecl + shrink = coerce . shrinkDataDecls . coerce + +-- @since 1.1.0 +instance Arbitrary (DataDeclSet 'ConcreteNestedDecl) where + arbitrary = coerce $ genDataList genNestedConcrete + shrink = coerce . shrinkDataDecls . coerce + +-- @since 1.1.0 +instance Arbitrary (DataDeclSet 'SimpleRecursive) where + arbitrary = coerce $ genDataList genArbitraryRecursive + shrink = coerce . shrinkDataDecls . coerce + +-- @since 1.1.0 +instance Arbitrary (DataDeclSet 'Poly1) where + arbitrary = coerce $ genDataList genPolymorphic1Decl + shrink = coerce . shrinkDataDecls . coerce + +instance Arbitrary (DataDeclSet 'Poly1PolyThunks) where + arbitrary = coerce . runDataGenM $ do + -- If we don't have this we can't generate ctor args of the sort we want here. + -- I *think* we're very unlikely to get 10 unsuitable decls out of this + void $ GT.vectorOf 10 genPolymorphic1Decl + void $ GT.listOf genNonConcreteDecl + decls <- M.elems <$> gets (view #decls) -- simpler to just pluck them from the monadic context + pure $ filter noPhantomTyVars decls -- TODO/FIXME: We shouldn't have to filter here, better to catch things earlier + shrink = coerce . shrinkDataDecls . coerce + +-- | Prettyprinter for 'DataDeclSet'. +-- +-- @since 1.1.0 +prettyDeclSet :: forall (a :: DataDeclFlavor). DataDeclSet a -> String +prettyDeclSet (DataDeclSet decls) = + concatMap (\x -> (prettyStr . unsafeRename . renameDataDecl $ x) <> "\n\n") decls + +-- | The same as 'QC.chooseInt', but lifted to work in any 'MonadGen'. +-- +-- @since 1.1.0 +chooseInt :: + forall (m :: Type -> Type). + (MonadGen m) => (Int, Int) -> m Int +chooseInt bounds = GT.liftGen $ QC.chooseInt bounds + +-- | The same as 'QC.scale', but lifted to work in any 'MonadGen'. +-- +-- @since 1.1.0 +scale :: + forall (m :: Type -> Type) (a :: Type). + (MonadGen m) => (Int -> Int) -> m a -> m a +scale f g = GT.sized (\n -> GT.resize (f n) g) + +-- | If the argument is a 'Right', pass the assertion; otherwise, fail the +-- assertion. +-- +-- @since 1.1.0 +failLeft :: + forall (a :: Type) (b :: Type). + (Show a) => + Either a b -> + IO b +failLeft = either (assertFailure . show) pure + +-- | Small collection of datatypes needed to test type application logic. +-- +-- @since 1.1.0 +tyAppTestDatatypes :: M.Map TyName (DatatypeInfo AbstractTy) +tyAppTestDatatypes = + foldl' (\acc decl -> M.insert (view #datatypeName decl) (unsafeMkDatatypeInfo decl) acc) M.empty testDatatypes + where + unsafeMkDatatypeInfo d = case mkDatatypeInfo d of + Left err -> error (show err) + Right res -> res + +-- | Helper for tests to quickly construct 'Datatype's. This is unsafe, as it +-- allows construction of nonsensical renamings. +-- +-- @since 1.1.0 +unsafeTyCon :: TyName -> [ValT a] -> ValT a +unsafeTyCon tn args = Datatype tn (Vector.fromList args) + +-- Helpers + +{- The state used by our datatype generators. +-} +data DataGen = DataGen + { -- Keeps track of decls we've already generated. Used for "nested" generators and also essential for ValT generation (when we get around to implementing it) + _dgDecls :: Map TyName (DataDeclaration AbstractTy), + -- All used constructor names. Have to track separately, even though the information eventually ends up in the previous field, to avoid duplicate constructors in the same type. + _dgCtors :: Set ConstructorName, + -- Current scope. Needed for generating polymorphic `ValT`s for arguments to constructors . (That's not implemented yet but we 100% will need this ) + _dgCurrentScope :: ScopeBoundary, + -- NOTE: Needs to maintain the invariant that the Word32 is always >0, since we will use this to select in scope variables for polymorphic args to ctors. (Again, not implemented yet) + _dgBoundVars :: Map ScopeBoundary Word32, + -- We need this for recursive types. We can't lookup the arity in dgDecls if we want to recurse b/c it won't be there until we've finished generating the whole decl + _dgArities :: Map TyName (Count "tyvar") + } + +instance + (k ~ A_Lens, a ~ Map TyName (DataDeclaration AbstractTy), b ~ Map TyName (DataDeclaration AbstractTy)) => + LabelOptic "decls" k DataGen DataGen a b + where + {-# INLINEABLE labelOptic #-} + labelOptic = lens (\(DataGen a _ _ _ _) -> a) (\(DataGen _ b c d e) a -> DataGen a b c d e) + +instance + (k ~ A_Lens, a ~ Set ConstructorName, b ~ Set ConstructorName) => + LabelOptic "constructors" k DataGen DataGen a b + where + {-# INLINEABLE labelOptic #-} + labelOptic = lens (\(DataGen _ b _ _ _) -> b) (\(DataGen a _ c d e) b -> DataGen a b c d e) + +instance + (k ~ A_Lens, a ~ ScopeBoundary, b ~ ScopeBoundary) => + LabelOptic "currentScope" k DataGen DataGen a b + where + {-# INLINEABLE labelOptic #-} + labelOptic = lens (\(DataGen _ _ c _ _) -> c) (\(DataGen a b _ d e) c -> DataGen a b c d e) + +instance + (k ~ A_Lens, a ~ Map ScopeBoundary Word32, b ~ Map ScopeBoundary Word32) => + LabelOptic "boundVars" k DataGen DataGen a b + where + {-# INLINEABLE labelOptic #-} + labelOptic = lens (\(DataGen _ _ _ d _) -> d) (\(DataGen a b c _ e) d -> DataGen a b c d e) + +instance + (k ~ A_Lens, a ~ Map TyName (Count "tyvar"), b ~ Map TyName (Count "tyvar")) => + LabelOptic "arities" k DataGen DataGen a b + where + {-# INLINEABLE labelOptic #-} + labelOptic = lens (\(DataGen _ _ _ _ e) -> e) (\(DataGen a b c d _) e -> DataGen a b c d e) + +{- Monadic stack for generating monomorphic datatype declarations. Not every generator uses every part of the state, but + it ought to suffice for generating *any* datatype declaration we choose. + + In theory this could be a reader but it becomes super awkward to work, StateT is easier + + While we don't have any generators for polymorphic `ValT`s yet, the scope stuff will be necessary there. +-} +newtype DataGenM a = DataGenM (GenT (State DataGen) a) + deriving newtype (Functor, Applicative, Monad) + deriving (MonadGen) via GenT (State DataGen) + +instance MonadState DataGen DataGenM where + get = DataGenM $ lift get + put = DataGenM . lift . put + +{- N.B. We don't need this *yet* but we will need it to generate constructors which take polymorphic functions as arguments. +-} +bindVars :: Count "tyvar" -> DataGenM () +bindVars count' + | count == 0 = crossBoundary + | otherwise = do + crossBoundary + here <- gets (view #currentScope) + modify $ over #boundVars (M.insert here $ fromIntegral count) + where + count :: Int + count = review intCount count' + + crossBoundary :: DataGenM () + crossBoundary = modify $ over #currentScope (+ 1) + +-- performs action in the deeper scope then resets. +withBoundVars :: forall (a :: Type). Count "tyvar" -> DataGenM a -> DataGenM a +withBoundVars count act = do + oldScope <- gets (view #currentScope) + bindVars count + res <- act + modify $ set #currentScope oldScope + pure res + +runDataGenM :: forall (a :: Type). DataGenM a -> Gen a +runDataGenM (DataGenM ma) = (\x -> evalState x (DataGen M.empty Set.empty 0 M.empty M.empty)) <$> GT.runGenT ma + +-- Stupid helper, saves us from forgetting to update part of the state +returnDecl :: DataDeclaration AbstractTy -> DataGenM (DataDeclaration AbstractTy) +returnDecl od@(OpaqueData tn _) = modify (over #decls (M.insert tn od)) >> pure od +returnDecl decl@(DataDeclaration tyNm arity _ _) = do + modify $ over #decls (M.insert tyNm decl) + logArity tyNm arity + pure decl + +{- We need this outside of `returnDecl` to construct recursive polymorphic types, i.e. types where an argument to + a constructor is the parent type applied to the type variables bound at the start of the declaration. +-} +logArity :: TyName -> Count "tyvar" -> DataGenM () +logArity tn cnt = modify $ over #arities (M.insert tn cnt) + +newtype ConcreteDataDecl = ConcreteDataDecl (DataDeclaration AbstractTy) + deriving (Eq) via (DataDeclaration AbstractTy) + deriving stock (Show) + +{- These should never be used in a DataGenM context, we should always use the fresh generators below-} +anyCtorName :: Gen ConstructorName +anyCtorName = ConstructorName <$> genValidCtorName + where + genValidCtorName :: Gen Text + genValidCtorName = do + let caps = ['A' .. 'Z'] + lower = ['a' .. 'z'] + nmLen <- chooseInt (1, 6) -- should be more than enough to ensure `suchThat` doesn't run into clashes all the time + x <- elements caps + xs <- vectorOf nmLen $ elements (caps <> lower) + pure . T.pack $ (x : xs) + +anyTyName :: Gen TyName +anyTyName = TyName . runConstructorName <$> anyCtorName + +{- These ensure that we don't ever duplicate type names or constructor names. We need the DataGenM state + to ensure that, so these should *always* be used when writing generators, and the arbitrary instances should be avoided. +-} +freshConstructorName :: DataGenM ConstructorName +freshConstructorName = do + datatypes <- gets (M.elems . view #decls) + let allCtorNames = Set.fromList $ toListOf (folded % #datatypeConstructors % folded % #constructorName) datatypes + thisName <- GT.liftGen $ anyCtorName `suchThat` (`Set.notMember` allCtorNames) + modify $ over #constructors (Set.insert thisName) + pure thisName + +freshTyName :: DataGenM TyName +freshTyName = do + datatypes <- gets (M.elems . view #decls) + let allDataTypeNames = Set.fromList $ toListOf (folded % #datatypeName) datatypes + GT.liftGen $ anyTyName `suchThat` (`Set.notMember` allDataTypeNames) + +newtype ConcreteConstructor = ConcreteConstructor (Constructor AbstractTy) + deriving (Eq) via (Constructor AbstractTy) + deriving stock (Show) + +notAThunk :: Concrete -> Bool +notAThunk (Concrete valT) = case valT of + ThunkT _ -> False + _ -> True + +genConcreteConstructor :: DataGenM ConcreteConstructor +genConcreteConstructor = ConcreteConstructor <$> go + where + go :: DataGenM (Constructor AbstractTy) + go = do + ctorNm <- freshConstructorName + numArgs <- chooseInt (0, 5) + args <- GT.liftGen $ Vector.replicateM numArgs (arbitrary @Concrete `suchThat` notAThunk) + pure $ Constructor ctorNm (coerce <$> args) + +genConcreteDataDecl :: DataGenM ConcreteDataDecl +genConcreteDataDecl = + ConcreteDataDecl <$> do + tyNm <- freshTyName + numArgs <- chooseInt (0, 5) + ctors <- coerce <$> Vector.replicateM numArgs genConcreteConstructor + let decl = DataDeclaration tyNm count0 ctors SOP + returnDecl decl + +{- Concrete datatypes which may contain other concrete datatypes as constructor args. (Still no TyVars) + + For example, if you have (in the DataGen context) an already generated: + + data Foo = Foo Integer + + this can generate a datatype like: + + data Bar = Bar Foo | Baz String + + I.e. it generates datatype declarations that use previously generated datatype declarations. + + This isn't useful unless you generate a *set* (or some other collection of them) in the DataGen monad, + since generating them one at a time will always give you the same thing as a ConcreteDataDecl. +-} +newtype NestedConcreteDataDecl = NestedConcreteDataDecl (DataDeclaration AbstractTy) + deriving (Eq) via (DataDeclaration AbstractTy) + deriving stock (Show) + +newtype NestedConcreteCtor = NestedConcreteCtor (Constructor AbstractTy) + +genNestedConcrete :: DataGenM NestedConcreteDataDecl +genNestedConcrete = + NestedConcreteDataDecl <$> do + tyNm <- freshTyName + res <- GT.oneof [nullary tyNm, nonNestedConcrete tyNm, nested tyNm] + returnDecl res + where + nullary :: TyName -> DataGenM (DataDeclaration AbstractTy) + nullary tyNm = do + ctorNm <- freshConstructorName + pure $ DataDeclaration tyNm count0 (Vector.singleton (Constructor ctorNm Vector.empty)) SOP + + nonNestedConcrete :: TyName -> DataGenM (DataDeclaration AbstractTy) + nonNestedConcrete tyNm = do + numCtors <- chooseInt (0, 5) + ctors <- fmap coerce <$> Vector.replicateM numCtors genConcreteConstructor + pure $ DataDeclaration tyNm count0 ctors SOP + + nested :: TyName -> DataGenM (DataDeclaration AbstractTy) + nested tyNm = do + numCtors <- chooseInt (0, 5) + ctors <- Vector.replicateM numCtors nestedCtor + pure $ DataDeclaration tyNm count0 (coerce <$> ctors) SOP + +{- It's useful to have access to these outside of the above function because sometimes we want to mix and match + "simpler" constructors like this with the more complex sorts we generate below. +-} +nestedCtor :: DataGenM NestedConcreteCtor +nestedCtor = do + -- We want this: Not very much hinges on the # of args to each constructor and having finite bounds like this makes the output easier to read + numArgs <- chooseInt (0, 5) + args <- Vector.replicateM numArgs nestedCtorArg + ctorNm <- freshConstructorName + pure . coerce $ Constructor ctorNm args + +nestedCtorArg :: DataGenM (ValT AbstractTy) +nestedCtorArg = do + userTyNames <- gets (M.keys . view #decls) + if null userTyNames + then coerce <$> GT.liftGen (arbitrary @Concrete) + else do + let userTypes = (`Datatype` Vector.empty) <$> userTyNames + GT.liftGen $ frequency [(8, elements userTypes), (2, coerce <$> arbitrary @Concrete)] + +newtype RecursiveConcreteDataDecl = RecursiveConcreteDataDecl (DataDeclaration AbstractTy) + deriving (Eq) via (DataDeclaration AbstractTy) + deriving stock (Show) + +{- Non-polymorphic recursive types, i.e. things like: + + data IntList = Empty | ConsInt Int IntList + + The general idea is that we construct a base case constructor (Nil or Empty) and then + construct a recursive constructor. We can expand this later (e.g. to have multiple recursive constructors, or a polymorphic variant) + but this will be enough to handle initial testing w/ the base functor / BBF stuff (and we have to ensure we have things like this to test that) +-} +genArbitraryRecursive :: DataGenM RecursiveConcreteDataDecl +genArbitraryRecursive = + RecursiveConcreteDataDecl <$> do + tyNm <- freshTyName + baseCtor <- coerce <$> genConcreteConstructor -- any concrete ctor - or any ctor that doesn't contain the parent type - will suffice as a base case + numRecCtors <- chooseInt (1, 5) + recCtor <- GT.vectorOf numRecCtors $ genRecCtor tyNm + returnDecl $ DataDeclaration tyNm count0 (Vector.fromList (baseCtor : recCtor)) SOP + where + genRecCtor :: TyName -> DataGenM (Constructor AbstractTy) + genRecCtor tyNm = do + ctorNm <- freshConstructorName + let thisType = Datatype tyNm Vector.empty + numNonRecArgs <- chooseInt (1, 5) -- need at least one to avoid "bad" types + args <- coerce $ GT.vectorOf numNonRecArgs nestedCtorArg + pure $ Constructor ctorNm (Vector.fromList (thisType : args)) + +{- Single variable polymorphic datatypes. That is, things like: + + data Foo a = Nope | Yup a + + data Snowk a = Start | More (Snowk a) a +-} +newtype Polymorphic1 = Polymorphic1 (DataDeclaration AbstractTy) + deriving (Eq) via (DataDeclaration AbstractTy) + deriving stock (Show) + +{- Generator for single variable polymorphic datatypes, no polymorphic *functions* as arguments to the datatypes yet (that requires something different). + + When run multiple times in the monadic context, will reuse single variable declarations that are "in scope" (i.e. have already been generated and are + known in the DataGenM state). + + TODO: Rework this to generate declarations with an arbitrary number of tyvar arguments. Doing so would be fairly simple (but isn't needed ATM) +-} +genPolymorphic1Decl :: DataGenM Polymorphic1 +genPolymorphic1Decl = + Polymorphic1 + <$> GT.suchThat + ( do + -- this is a hack to save avoid reworking generator logic. It should be fine cuz we're not super likely to get phantoms anyway + tyNm <- freshTyName + logArity tyNm count1 + numCtors <- chooseInt (1, 5) + polyCtors <- concat <$> GT.vectorOf numCtors (genPolyCtor tyNm) + let result = DataDeclaration tyNm count1 (Vector.fromList polyCtors) SOP + returnDecl result + ) + noPhantomTyVars + where + -- We return a single constructor UNLESS we're generating a recursive type, in which case we have to return 2 to ensure a base case + genPolyCtor :: TyName -> DataGenM [Constructor AbstractTy] + genPolyCtor thisTy = do + ctorNm <- freshConstructorName + numArgs <- chooseInt (1, 5) + argsRaw <- GT.vectorOf numArgs polyArg + let recCase = Datatype thisTy (Vector.singleton (Abstraction (BoundAt Z ix0))) + if recCase `elem` argsRaw + then do + baseCtorNm <- freshConstructorName + let baseCtor = Constructor baseCtorNm mempty + recCtor = Constructor ctorNm (fromListN numArgs argsRaw) + pure [baseCtor, recCtor] + else pure [Constructor ctorNm (fromListN numArgs argsRaw)] + where + arityOne :: Count "tyvar" -> Bool + arityOne c = c == count1 + + polyArg :: DataGenM (ValT AbstractTy) + polyArg = do + -- first we choose a type with an arity >=1. We have to have at least one of those because we've added the parent type to the arity map + availableArity1 <- gets (M.keys . M.filter arityOne . view #arities) + someTyCon1 <- GT.elements availableArity1 + GT.oneof + [ pure $ Abstraction (BoundAt Z ix0), + pure $ Datatype someTyCon1 (Vector.singleton (Abstraction (BoundAt Z ix0))), + GT.liftGen (coerce <$> arbitrary @Concrete) + ] + +{- Non-concrete ValTs. This needs to be scope- and context-sensitive in order to generate ThunkTs that *use* (but never *bind*) variables. + +This will give us things like: + + data Foo a b = Foo Int Bool a (a -> (Int -> b) -> b -> b) +-} + +newtype NonConcrete = NonConcrete (ValT AbstractTy) + deriving + ( -- | @since 1.0.0 + Eq + ) + via (ValT AbstractTy) + deriving stock + ( -- | @since 1.0.0 + Show + ) + +genNonConcrete :: DataGenM NonConcrete +genNonConcrete = NonConcrete <$> GT.sized go + where + -- smaller to make output more readable + genConcrete :: DataGenM Concrete + genConcrete = GT.liftGen $ scale (`quot` 8) (arbitrary @Concrete) + + go :: Int -> DataGenM (ValT AbstractTy) + go = helper + + -- A polymorphic tycon applied to *either* an in-scope type variable *or* a concrete type. + -- TODO: Conceivably this could recursively call `helper` to generate "fancier" tycon arguments + -- but that shouldn't matter much for now & runs the risk of generating unusably large output w/o + -- careful implementation. + appliedTyCon :: Int -> DataGenM (ValT AbstractTy) + appliedTyCon size = do + currentScope <- gets (view #currentScope) + tyConsWithArity <- M.toList <$> gets (view #arities) + boundVars <- M.toList <$> gets (view #boundVars) + -- We *have* to have some variables bound for this to work. We can't meaningfully return a `Maybe` here + -- Also we have to have some Arity >= 1 TyCon around + -- I.e. we cannot run this generator in a "fresh" DataGenM stack and have to both pre-generate + -- some fresh polymorphic types *and* ensure that we only use this in a context where we have bound variables. + (thisTyCon, thisArity) <- GT.elements tyConsWithArity + let arityInt = review intCount thisArity + let resolvedArgs = concatMap (resolveArgs currentScope) boundVars + let choices + | size <= 0 = [coerce <$> genConcrete] + | otherwise = [coerce <$> genConcrete, GT.elements resolvedArgs] + tyConArgs <- GT.vectorOf arityInt $ GT.oneof choices + pure $ Datatype thisTyCon (Vector.fromList tyConArgs) + + resolveArgs :: ScopeBoundary -> (ScopeBoundary, Word32) -> [ValT AbstractTy] + resolveArgs currentScope (varScope, numIndices) = + let resolvedScope :: DeBruijn + resolvedScope = fromJust . preview asInt . fromIntegral $ currentScope - varScope + in mapMaybe (fmap (Abstraction . BoundAt resolvedScope) . preview intIndex) [0 .. (fromIntegral numIndices - 1)] + + helper :: Int -> DataGenM (ValT AbstractTy) + helper size = do + GT.oneof [coerce <$> genConcrete, appliedTyCon size] + +-- NOTE: We have to call this with a "driver" which pre-generates suitable (i.e. polymorphic) data declarations, see notes in `genNonConcrete` +genNonConcreteDecl :: DataGenM (DataDeclaration AbstractTy) +genNonConcreteDecl = flip GT.suchThat noPhantomTyVars . withBoundVars count1 $ do + -- we need to bind the vars before we're done constructing the type + tyNm <- freshTyName + numArgs <- chooseInt (1, 5) + ctors <- Vector.replicateM numArgs genNonConcreteCtor + let decl = DataDeclaration tyNm count1 ctors SOP + returnDecl decl + where + genNonConcreteCtor :: DataGenM (Constructor AbstractTy) + genNonConcreteCtor = do + ctorNm <- freshConstructorName + numArgs <- chooseInt (0, 5) + args <- GT.vectorOf numArgs genNonConcrete + pure $ Constructor ctorNm (coerce . Vector.fromList $ args) + +{- + Misc Helpers and the Arbitrary instances +-} + +{- NOTE: This is supposed to be a "generic" shrinker for datatypes. It *should* return two paths: + - One that shrinks the number of constructors + - One that shrinks the constructors + + This is why I had to add handling for `datatype` into `Concrete`. To use `shrink` recursively + on the structural components, we need some kind of instance to pivot off of. Since we want to avoid + writing a generic Arbitrary instance for Constructor or DataDeclaration, this seems like the + simplest solution. +-} +shrinkDataDecl :: DataDeclaration AbstractTy -> [DataDeclaration AbstractTy] +shrinkDataDecl OpaqueData {} = [] +shrinkDataDecl (DataDeclaration nm cnt ctors strat) + | Vector.null ctors = [] + | otherwise = filter noPhantomTyVars $ smallerNumCtors <|> smallerCtorArgs + where + smallerNumCtors :: [DataDeclaration AbstractTy] + smallerNumCtors = Vector.toList $ (\cs -> DataDeclaration nm cnt cs strat) <$> Vector.init (subVectors ctors) + smallerCtorArgs = (\cs -> DataDeclaration nm cnt cs strat) <$> shrinkCtorsNumArgs ctors + + -- need a fn which takes a single ctor and just shrinks the args + -- this is difficult to keep track of: THIS ONE GIVES US IDENTICALLY NAMED CTORS WITH DIFFERENT ARG LISTS + shrinkNumArgs :: Constructor AbstractTy -> [Constructor AbstractTy] + shrinkNumArgs (Constructor ctorNm args) = + let smallerArgs :: [Vector (ValT AbstractTy)] + smallerArgs = coerce $ shrink (fmap Concrete args) + in fmap (Constructor ctorNm) smallerArgs + + shrinkCtorsNumArgs :: Vector (Constructor AbstractTy) -> [Vector (Constructor AbstractTy)] + shrinkCtorsNumArgs cs = + let -- the inner lists exhaust the arg-deletion possibilities for each constructor + cs' = Vector.toList $ shrinkNumArgs <$> cs + go [] = [] + go (x : xs) = (:) <$> x <*> xs + in Vector.fromList <$> go cs' + +-- Helper, should probably exist in Data.Vector but doesn't +subVectors :: forall (a :: Type). Vector a -> Vector (Vector a) +subVectors xs = Vector.cons Vector.empty (nonEmptySubVectors xs) + +nonEmptySubVectors :: forall (a :: Type). Vector a -> Vector (Vector a) +nonEmptySubVectors v = case Vector.uncons v of + Nothing -> Vector.empty + Just (x, xs) -> + let f :: Vector a -> Vector (Vector a) -> Vector (Vector a) + f ys r = ys `Vector.cons` ((x `Vector.cons` ys) `Vector.cons` r) + in Vector.singleton x `Vector.cons` foldr f Vector.empty (nonEmptySubVectors xs) + +shrinkDataDecls :: [DataDeclaration AbstractTy] -> [[DataDeclaration AbstractTy]] +shrinkDataDecls decls = liftShrink shrinkDataDecl decls <|> (shrinkDataDecl <$> decls) + +genDataList :: forall (a :: Type). DataGenM a -> Gen [a] +genDataList = runDataGenM . GT.listOf + +-- For convenience. Don't remove this, necessary for efficient development on future work +unsafeRename :: forall (a :: Type). RenameM a -> a +unsafeRename act = case runRenameM act of + Left err -> error $ show err + Right res -> res + +eitherT :: DataDeclaration AbstractTy +eitherT = + mkDecl $ + Decl + "Either" + count2 + [ Ctor "Left" [Abstraction (BoundAt Z ix0)], + Ctor "Right" [Abstraction (BoundAt Z ix1)] + ] + (PlutusData ConstrData) + +unitT :: DataDeclaration AbstractTy +unitT = + mkDecl $ + Decl + "Unit" + count0 + [Ctor "Unit" []] + (PlutusData ConstrData) + +testDatatypes :: [DataDeclaration AbstractTy] +testDatatypes = [maybeT, eitherT, unitT, pair] diff --git a/src/Covenant/Type.hs b/src/Covenant/Type.hs --- a/src/Covenant/Type.hs +++ b/src/Covenant/Type.hs @@ -22,6 +22,9 @@ -- * Value types ValT (..), + dataTypeT, + dataType1T, + dataType2T, BuiltinFlatT (..), byteStringT, integerT, @@ -33,22 +36,25 @@ mlResultT, unitT, - -- * Renaming - - -- ** Types - RenameError (..), - RenameM, - - -- ** Introduction - renameValT, - renameCompT, - - -- ** Elimination - runRenameM, - - -- * Type application - TypeAppError (..), - checkApp, + -- * Data declarations + TyName (TyName), + ConstructorName (ConstructorName), + Constructor (Constructor), + PlutusDataStrategy + ( EnumData, + ProductListData, + ConstrData, + NewtypeData + ), + DataEncoding (SOP, PlutusData, BuiltinStrategy), + PlutusDataConstructor + ( PlutusI, + PlutusB, + PlutusConstr, + PlutusList, + PlutusMap + ), + DataDeclaration (DataDeclaration, OpaqueData), ) where @@ -63,16 +69,21 @@ count3, intCount, ) -import Covenant.Internal.Rename - ( RenameError - ( InvalidAbstractionReference, - IrrelevantAbstraction, - UndeterminedAbstraction +import Covenant.Internal.Strategy + ( DataEncoding (BuiltinStrategy, PlutusData, SOP), + PlutusDataConstructor + ( PlutusB, + PlutusConstr, + PlutusI, + PlutusList, + PlutusMap ), - RenameM, - renameCompT, - renameValT, - runRenameM, + PlutusDataStrategy + ( ConstrData, + EnumData, + NewtypeData, + ProductListData + ), ) import Covenant.Internal.Type ( AbstractTy (BoundAt), @@ -88,18 +99,12 @@ ), CompT (CompT), CompTBody (CompTBody), + Constructor (Constructor), + ConstructorName (ConstructorName), + DataDeclaration (DataDeclaration, OpaqueData), Renamed (Rigid, Unifiable, Wildcard), - ValT (Abstraction, BuiltinFlat, ThunkT), - ) -import Covenant.Internal.Unification - ( TypeAppError - ( DoesNotUnify, - ExcessArgs, - InsufficientArgs, - LeakingUnifiable, - LeakingWildcard - ), - checkApp, + TyName (TyName), + ValT (Abstraction, BuiltinFlat, Datatype, ThunkT), ) import Data.Coerce (coerce) import Data.Kind (Type) @@ -107,6 +112,7 @@ import Data.Vector qualified as Vector import Data.Vector.NonEmpty (NonEmptyVector) import Data.Vector.NonEmpty qualified as NonEmpty +import GHC.Exts (fromListN) import Optics.Core (preview) -- | The body of a computation type that doesn't take any arguments and produces @@ -249,6 +255,24 @@ -- @since 1.0.0 tyvar :: DeBruijn -> Index "tyvar" -> ValT AbstractTy tyvar db = Abstraction . BoundAt db + +-- | Helper for referring to compound data types with no type variables. +-- +-- @since 1.1.0 +dataTypeT :: forall (a :: Type). TyName -> ValT a +dataTypeT tn = Datatype tn Vector.empty + +-- | Helper for referring to compound data types with one type variable. +-- +-- @since 1.1.0 +dataType1T :: TyName -> ValT AbstractTy -> ValT AbstractTy +dataType1T tn = Datatype tn . Vector.singleton + +-- | Helper for referring to compound data types with two type variables. +-- +-- @since 1.1.0 +dataType2T :: TyName -> ValT AbstractTy -> ValT AbstractTy -> ValT AbstractTy +dataType2T tn v1 v2 = Datatype tn . fromListN 2 $ [v1, v2] -- | Helper for defining the value type of builtin bytestrings. -- diff --git a/src/Covenant/Util.hs b/src/Covenant/Util.hs --- a/src/Covenant/Util.hs +++ b/src/Covenant/Util.hs @@ -9,12 +9,16 @@ module Covenant.Util ( pattern NilV, pattern ConsV, + prettyStr, ) where import Data.Kind (Type) +import Data.Text qualified as Text import Data.Vector.Generic (Vector) import Data.Vector.Generic qualified as Vector +import Prettyprinter (Pretty (pretty), defaultLayoutOptions, layoutPretty) +import Prettyprinter.Render.Text (renderStrict) -- | A pattern matching helper for vectors (of all types), corresponding to @[]@ -- for lists. This pattern is bidirectional, which means it can be used just @@ -43,3 +47,14 @@ pattern ConsV x xs <- (Vector.uncons -> Just (x, xs)) {-# COMPLETE NilV, ConsV #-} + +-- | Shorthand to transform any 'Pretty' into a 'String' using the default +-- layout. +-- +-- @since 1.1.0 +prettyStr :: forall (a :: Type). (Pretty a) => a -> String +prettyStr = + Text.unpack + . renderStrict + . layoutPretty defaultLayoutOptions + . pretty diff --git a/test/asg/Main.hs b/test/asg/Main.hs --- a/test/asg/Main.hs +++ b/test/asg/Main.hs @@ -65,6 +65,7 @@ import Covenant.Util (pattern ConsV, pattern NilV) import Data.Coerce (coerce) import Data.Kind (Type) +import Data.Map qualified as M import Data.Maybe (fromJust) import Data.Vector qualified as Vector import Optics.Core (preview, review) @@ -120,20 +121,20 @@ unitEmptyASG = do let builtUp = pure () let expected = Left EmptyASG - let actual = runASGBuilder builtUp + let actual = runASGBuilder M.empty builtUp assertEqual "" expected actual unitSingleError :: IO () unitSingleError = do let builtUp = err let expected = Left TopLevelError - let actual = runASGBuilder builtUp + let actual = runASGBuilder M.empty builtUp assertEqual "" expected actual unitForceError :: IO () unitForceError = do let builtUp = err >>= \i -> force (AnId i) - let result = runASGBuilder builtUp + let result = runASGBuilder M.empty builtUp case result of Left (TypeError _ ForceError) -> pure () _ -> assertFailure $ "Unexpected result: " <> show result @@ -141,7 +142,7 @@ unitThunkError :: IO () unitThunkError = do let builtUp = err >>= thunk - let result = runASGBuilder builtUp + let result = runASGBuilder M.empty builtUp case result of Left (TypeError _ ThunkError) -> pure () _ -> assertFailure $ "Unexpected result: " <> show result @@ -235,7 +236,9 @@ where mkComps :: forall (a :: Type). - (a -> ASGBuilder Id) -> a -> (ASGBuilder Id, ASGBuilder Id) + (a -> ASGBuilder Id) -> + a -> + (ASGBuilder Id, ASGBuilder Id) mkComps f x = let comp = f x forceThunkComp = do @@ -431,12 +434,12 @@ failWrongError err' = failWithCounterExample ("Unexpected error: " <> show err') withCompilationFailure :: ASGBuilder Id -> (CovenantError -> Property) -> Property -withCompilationFailure comp cb = case runASGBuilder comp of +withCompilationFailure comp cb = case runASGBuilder M.empty comp of Left err' -> cb err' Right asg -> failWithCounterExample ("Unexpected success: " <> show asg) withCompilationSuccess :: ASGBuilder Id -> (ASG -> Property) -> Property -withCompilationSuccess comp cb = case runASGBuilder comp of +withCompilationSuccess comp cb = case runASGBuilder M.empty comp of Left err' -> failWithCounterExample ("Unexpected failure: " <> show err') Right asg -> cb asg diff --git a/test/base-functor/Main.hs b/test/base-functor/Main.hs new file mode 100644 --- /dev/null +++ b/test/base-functor/Main.hs @@ -0,0 +1,46 @@ +module Main (main) where + +import Control.Monad.Reader (runReader) +import Covenant.Data + ( allComponentTypes, + hasRecursive, + mkBaseFunctor, + ) +import Covenant.Test + ( DataDeclFlavor (Poly1PolyThunks), + DataDeclSet (DataDeclSet), + prettyDeclSet, + ) +import Covenant.Type () +import Data.Map.Strict qualified as M +import Optics.Core (view) +import Test.QuickCheck + ( Arbitrary (arbitrary, shrink), + Property, + ) +import Test.Tasty (defaultMain, testGroup) +import Test.Tasty.QuickCheck (forAllShrinkShow, testProperty) + +main :: IO () +main = + defaultMain . testGroup "BaseFunctors" $ + [testProperty "All recursion is replaced in base functor transform" baseFunctorsContainNoRecursion] + +baseFunctorsContainNoRecursion :: Property +baseFunctorsContainNoRecursion = forAllShrinkShow (arbitrary @(DataDeclSet 'Poly1PolyThunks)) shrink prettyDeclSet $ \(DataDeclSet decls) -> + let declMap = M.fromList $ (\x -> (view #datatypeName x, x)) <$> decls + baseFunctorResults = flip runReader 0 . mkBaseFunctor <$> declMap + in M.foldlWithKey' + ( \acc tyNm origDecl -> + let isTyRecursive = any (\x -> runReader (hasRecursive tyNm x) 0) (allComponentTypes origDecl) + mBaseFDecl = baseFunctorResults M.! tyNm + in case mBaseFDecl of + -- if we didn't make a base functor then the original type must NOT be recursive + Nothing -> not isTyRecursive && acc + Just baseFDecl -> + -- If we did make a base functor, it should contain no recursion + let recursionInBaseF = any (\x -> runReader (hasRecursive (view #datatypeName baseFDecl) x) 0) (allComponentTypes baseFDecl) + in not recursionInBaseF && acc + ) + True + declMap diff --git a/test/bb/Main.hs b/test/bb/Main.hs new file mode 100644 --- /dev/null +++ b/test/bb/Main.hs @@ -0,0 +1,156 @@ +{-# LANGUAGE ViewPatterns #-} + +module Main (main) where + +-- import Data.Either (isRight) + +import Control.Exception (throwIO) +import Control.Monad ((<=<)) +import Covenant.Data + ( mkBBF, + ) +import Covenant.DeBruijn (DeBruijn (S, Z)) +import Covenant.Index (ix0, ix1) +import Covenant.Test + ( DataDeclFlavor (Poly1PolyThunks), + DataDeclSet (DataDeclSet), + failLeft, + list, + prettyDeclSet, + renameCompT, + renameValT, + runRenameM, + tree, + tyAppTestDatatypes, + unsafeTyCon, + weirderList, + ) +import Covenant.Type + ( AbstractTy (BoundAt), + CompT (Comp0, Comp1, Comp2), + CompTBody (ReturnT, (:--:>)), + ValT (Abstraction, ThunkT), + tyvar, + ) +import Data.Map qualified as M +import Data.Maybe (catMaybes, fromJust) +import Optics.Core (view) +import Test.QuickCheck + ( Arbitrary (arbitrary, shrink), + Property, + ) +import Test.Tasty (TestTree, adjustOption, defaultMain, testGroup) +import Test.Tasty.HUnit (assertEqual, assertFailure, testCase) +import Test.Tasty.QuickCheck (QuickCheckTests, forAllShrinkShow, testProperty) + +main :: IO () +main = + defaultMain . adjustOption moreTests . testGroup "BB" $ + [ testProperty "All BBF transformations rename properly" bbFormRenames, + testMonotypeBB, + bbfList, + bbfTree, + bbfWeirderList + ] + where + -- These tests are suuuuppeeerr inefficient, it'd be ideal to run more but it'll take too long + moreTests :: QuickCheckTests -> QuickCheckTests + moreTests = max 500 + +{- This is the only reasonable property I can think of, and is ultimately more of a test of the + "ensure there aren't any phantom type variables" than it is of the bb transform. + + Fortunately the transform itself is fairly straightforward and isn't likely to contain major errors. +-} +bbFormRenames :: Property +bbFormRenames = forAllShrinkShow (arbitrary @(DataDeclSet 'Poly1PolyThunks)) shrink prettyDeclSet $ \(DataDeclSet decls) -> + case traverse mkBBF decls of + Left _ -> False + Right (catMaybes -> bbfDecls) -> + let results = + mapM + ( \valT -> case runRenameM . renameValT $ valT of + Left err -> Left (err, valT) + Right res -> Right res + ) + bbfDecls + in case results of -- all (isRight . runRenameM . renameValT) bbfDecls + Right {} -> True + Left err -> error (show err) + +bbfList :: TestTree +bbfList = testCase "bbfList" $ do + let bbf = mkBBF list + bbf' <- either (assertFailure . show) (maybe (assertFailure "no bbf for list") pure) bbf + assertEqual "bbfList" expectedListBBF bbf' + where + expectedListBBF = + ThunkT + ( Comp2 + ( tyvar Z ix1 + :--:> ThunkT + ( Comp0 + ( tyvar (S Z) ix0 + :--:> tyvar (S Z) ix1 + :--:> ReturnT (tyvar (S Z) ix1) + ) + ) + :--:> ReturnT (tyvar Z ix1) + ) + ) + +bbfTree :: TestTree +bbfTree = testCase "bbfTree" $ do + let bbf = mkBBF tree + bbf' <- either (assertFailure . show) (maybe (assertFailure "no bbf for tree") pure) bbf + assertEqual "bbfList" expectedTreeBBF bbf' + where + expectedTreeBBF = + ThunkT + ( Comp2 + ( ThunkT + ( Comp0 + ( tyvar (S Z) ix1 + :--:> tyvar (S Z) ix1 + :--:> ReturnT (tyvar (S Z) ix1) + ) + ) + :--:> ThunkT + ( Comp0 + ( tyvar (S Z) ix0 + :--:> ReturnT (tyvar (S Z) ix1) + ) + ) + :--:> ReturnT (tyvar Z ix1) + ) + ) + +bbfWeirderList :: TestTree +bbfWeirderList = testCase "bbfWeirderList" $ do + let bbf = mkBBF weirderList + bbf' <- either (assertFailure . show) (maybe (assertFailure "no bbf for tree") pure) bbf + assertEqual "bbfWeirderTree" expectedWeirdBBF bbf' + where + -- forall a r. (Maybe (a,r) -> r) -> r + expectedWeirdBBF = + ThunkT + ( Comp2 + ( ThunkT + ( Comp0 + ( unsafeTyCon "Maybe" [unsafeTyCon "Pair" [tyvar (S Z) ix0, tyvar (S Z) ix1]] + :--:> ReturnT (tyvar (S Z) ix1) + ) + ) + :--:> ReturnT (tyvar Z ix1) + ) + ) + +-- Simple datatype unification unit test. Checks whether `data Unit = Unit` has the expected BB form +testMonotypeBB :: TestTree +testMonotypeBB = testCase "unitBbf" $ do + let expected = Comp1 $ Abstraction (BoundAt Z ix0) :--:> ReturnT (Abstraction $ BoundAt Z ix0) + expected' <- failLeft . runRenameM . renameCompT $ expected + actual <- case fromJust . (view #bbForm <=< M.lookup "Unit") $ tyAppTestDatatypes of + ThunkT inner -> either (throwIO . userError . show) pure . runRenameM $ renameCompT inner + _ -> assertFailure "BB form not a thunk!" + assertEqual "unit bbf" expected' actual diff --git a/test/kindcheck/Main.hs b/test/kindcheck/Main.hs new file mode 100644 --- /dev/null +++ b/test/kindcheck/Main.hs @@ -0,0 +1,159 @@ +module Main (main) where + +import Covenant.ASG (defaultDatatypes) +import Covenant.Data () +import Covenant.DeBruijn (DeBruijn (Z)) +import Covenant.Index (count0, count1, ix0) +import Covenant.Test + ( checkDataDecls, + checkEncodingArgs, + cycleCheck, + unsafeTyCon, + ) +import Covenant.Type + ( AbstractTy (BoundAt), + BuiltinFlatT (IntegerT), + CompT (Comp1), + CompTBody (ReturnT, (:--:>)), + Constructor (Constructor), + DataDeclaration (DataDeclaration, OpaqueData), + DataEncoding (PlutusData, SOP), + PlutusDataStrategy (ConstrData), + TyName, + ValT (Abstraction, BuiltinFlat, Datatype, ThunkT), + tyvar, + ) +import Data.Map.Strict qualified as M +import Data.Vector qualified as V +import Optics.Core (view) +import Test.Tasty (TestTree, defaultMain, testGroup) +import Test.Tasty.ExpectedFailure (expectFail) +import Test.Tasty.HUnit (assertFailure, testCase) + +main :: IO () +main = + defaultMain . testGroup "DatatypeCycleCheck" $ + [ testCase "singleNonRec" $ runCycleCheck [maybee], + testCase "singleSelfRec" $ runCycleCheck [intList], + expectFail $ testCase "mutRecShouldFail" (runCycleCheck [mutRec1, mutRec2]), + checkLedgerTypes, + simpleEncodingMismatch, + nestedThunkArg, + noThunkArgsToSOPTyCons, + goodSOPArg + ] + +checkLedgerTypes :: TestTree +checkLedgerTypes = + testCase "kindCheckLedgerTypes" + . either (assertFailure . show) pure + . checkDataDecls + . fmap (view #originalDecl) + $ defaultDatatypes + +encodingCheck :: String -> [DataDeclaration AbstractTy] -> ValT AbstractTy -> TestTree +encodingCheck testNm tyDict valT = + testCase testNm $ + either (assertFailure . show) pure $ + checkEncodingArgs (view #datatypeEncoding) (mkTyDict tyDict) valT + +shouldFailEncodingCheck :: String -> [DataDeclaration AbstractTy] -> ValT AbstractTy -> TestTree +shouldFailEncodingCheck tnm tyDict valT = expectFail $ encodingCheck tnm tyDict valT + +simpleEncodingMismatch :: TestTree +simpleEncodingMismatch = shouldFailEncodingCheck "simpleEncodingMismatch" [maybee, intList] encodingMismatch + +noThunkArgsToSOPTyCons :: TestTree +noThunkArgsToSOPTyCons = + shouldFailEncodingCheck "no thunk args to SOP tycons (for now)" [maybeSOP] badSOPThunk + +nestedThunkArg :: TestTree +nestedThunkArg = shouldFailEncodingCheck "nestedThunkArg" [maybee] badThunkArg + +goodSOPArg :: TestTree +goodSOPArg = encodingCheck "goodSOP" [maybeSOP] goodSOP + +mkTyDict :: forall a. [DataDeclaration a] -> M.Map TyName (DataDeclaration a) +mkTyDict = foldr (\decl acc -> M.insert (view #datatypeName decl) decl acc) M.empty + +runCycleCheck :: [DataDeclaration AbstractTy] -> IO () +runCycleCheck decls = case cycleCheck declMap of + Nothing -> pure () + Just err -> assertFailure $ show err + where + declMap = + foldr + ( \dd acc -> case dd of + OpaqueData {} -> acc + DataDeclaration tn _ _ _ -> M.insert tn dd acc + ) + M.empty + decls + +maybee :: DataDeclaration AbstractTy +maybee = DataDeclaration "Maybe" count1 (V.fromList ctors) (PlutusData ConstrData) + where + ctors = + [ Constructor "Nothing" V.empty, + Constructor "Just" (V.singleton (Abstraction $ BoundAt Z ix0)) + ] + +maybeSOP :: DataDeclaration AbstractTy +maybeSOP = DataDeclaration "MaybeSOP" count1 (V.fromList ctors) SOP + where + ctors = + [ Constructor "Nothing" V.empty, + Constructor "Just" (V.singleton (Abstraction $ BoundAt Z ix0)) + ] + +intList :: DataDeclaration AbstractTy +intList = DataDeclaration "IntList" count0 (V.fromList ctors) SOP + where + ctors = + [ Constructor "Empty" V.empty, + Constructor "More" (V.fromList intListMore) + ] + + intListMore :: [ValT AbstractTy] + intListMore = [BuiltinFlat IntegerT, Datatype "IntList" V.empty] + +-- DATA ENCODED MAYBE, SOP ENCODED INTLIST +-- Maybe IntList +encodingMismatch :: ValT AbstractTy +encodingMismatch = Datatype "Maybe" (V.fromList [Datatype "IntList" V.empty]) + +-- forall a. (a -> a) +identitee :: ValT AbstractTy +identitee = ThunkT $ Comp1 (tyvar Z ix0 :--:> ReturnT (tyvar Z ix0)) + +-- DATA ENCODED MAYBE +-- Maybe (Maybe (forall a. a -> a)) +badThunkArg :: ValT AbstractTy +badThunkArg = unsafeTyCon "Maybe" [unsafeTyCon "Maybe" [identitee]] + +-- SOP ENCODED MAYBE +-- Maybe (Maybe (Maybe Integer)) +goodSOP :: ValT AbstractTy +goodSOP = + unsafeTyCon + "MaybeSOP" + [ unsafeTyCon "MaybeSOP" [unsafeTyCon "MaybeSOP" [BuiltinFlat IntegerT]] + ] + +-- NOTE Sean 7/2/2025: We are *temporarily* forbidding thunk arguments even to SOP encoded type constructors. +-- This is not strictly necessary, and we can go back and change that if we have time, but it +-- does greatly simplify getting a proof-of-concept off the ground. +-- SOP ENCODED MAYBE +-- Maybe (forall a. a -> a) +badSOPThunk :: ValT AbstractTy +badSOPThunk = unsafeTyCon "MaybeSOP" [identitee] + +mutRec1 :: DataDeclaration AbstractTy +mutRec1 = DataDeclaration "MutRec1" count0 (V.fromList ctors) SOP + where + ctors = [Constructor "MutRec1" (V.singleton (Datatype "MutRec2" V.empty))] + +mutRec2 :: DataDeclaration AbstractTy +mutRec2 = DataDeclaration "MutRec2" count0 (V.fromList ctors) SOP + where + ctors = [Constructor "MutRec2" (V.fromList [Datatype "MutRec1" V.empty])] diff --git a/test/primops/Main.hs b/test/primops/Main.hs --- a/test/primops/Main.hs +++ b/test/primops/Main.hs @@ -1,20 +1,56 @@ +{-# LANGUAGE PatternSynonyms #-} + module Main (main) where +import Covenant.ASG (defaultDatatypes) import Covenant.Prim - ( typeOneArgFunc, + ( OneArgFunc + ( BData, + FstPair, + HeadList, + IData, + ListData, + MapData, + NullList, + SerialiseData, + SndPair, + TailList, + UnBData, + UnConstrData, + UnIData, + UnListData, + UnMapData + ), + SixArgFunc (CaseData, ChooseData), + ThreeArgFunc (CaseList, ChooseList), + TwoArgFunc (ConstrData, EqualsData, MkCons, MkPairData), + typeOneArgFunc, + typeSixArgFunc, typeThreeArgFunc, typeTwoArgFunc, ) +import Covenant.Test + ( checkApp, + renameCompT, + renameValT, + runRenameM, + ) import Covenant.Type ( AbstractTy (BoundAt), - CompT, + CompT (Comp0), Renamed (Unifiable), + ValT (Datatype, ThunkT), arity, - renameCompT, - runRenameM, + boolT, + byteStringT, + integerT, + pattern ReturnT, + pattern (:--:>), ) import Data.Functor.Classes (liftEq) +import Data.Functor.Identity (Identity (Identity)) import Data.Kind (Type) +import Data.Vector qualified as Vector import Test.QuickCheck ( Arbitrary (arbitrary), Property, @@ -24,6 +60,7 @@ (===), ) import Test.Tasty (defaultMain, testGroup) +import Test.Tasty.HUnit (assertEqual, assertFailure, testCase) import Test.Tasty.QuickCheck (testProperty) main :: IO () @@ -35,15 +72,53 @@ "Arity" [ testProperty "One-argument primops take one argument" prop1Arg, testProperty "Two-argument primops take two arguments" prop2Args, - testProperty "Three-argument primops take three arguments" prop3Args - -- testProperty "Six-argument primops take six arguments" prop6Args + testProperty "Three-argument primops take three arguments" prop3Args, + testProperty "Six-argument primops take six arguments" prop6Args ], testGroup "Renaming" [ testProperty "One-argument primops rename correctly" prop1Rename, testProperty "Two-argument primops rename correctly" prop2Rename, - testProperty "Three-argument primops rename correctly" prop3Rename - -- testProperty "Six-argument primops rename correctly" prop6Rename + testProperty "Three-argument primops rename correctly" prop3Rename, + testProperty "Six-argument primops rename correctly" prop6Rename + ], + testGroup + "Application with data types" + [ testGroup + "One argument" + [ testCase "FstPair" unitFstPair, + testCase "SndPair" unitSndPair, + testCase "HeadList" unitHeadList, + testCase "TailList" unitTailList, + testCase "NullList" unitNullList, + testCase "MapData" unitMapData, + testCase "ListData" unitListData, + testCase "IData" unitIData, + testCase "BData" unitBData, + testCase "UnConstrData" unitUnConstrData, + testCase "UnMapData" unitUnMapData, + testCase "UnListData" unitUnListData, + testCase "UnIData" unitUnIData, + testCase "UnBData" unitUnBData, + testCase "SerialiseData" unitSerialiseData + ], + testGroup + "Two arguments" + [ testCase "MkCons" unitMkCons, + testCase "ConstrData" unitConstrData, + testCase "EqualsData" unitEqualsData, + testCase "MkPairData" unitMkPairData + ], + testGroup + "Three arguments" + [ testCase "ChooseList" unitChooseList, + testCase "CaseList" unitCaseList + ], + testGroup + "Six arguments" + [ testCase "ChooseData" unitChooseData, + testCase "CaseData" unitCaseData + ] ] ] @@ -67,14 +142,137 @@ prop3Rename :: Property prop3Rename = mkRenameProp typeThreeArgFunc -{- prop6Args :: Property prop6Args = mkArgProp typeSixArgFunc 6 prop6Rename :: Property prop6Rename = mkRenameProp typeSixArgFunc --} +unitFstPair :: IO () +unitFstPair = withRenamedComp (typeOneArgFunc FstPair) $ \renamedFunT -> + withRenamedVals [Datatype "Pair" . Vector.fromList $ [integerT, byteStringT]] $ + tryAndApply integerT renamedFunT + +unitSndPair :: IO () +unitSndPair = withRenamedComp (typeOneArgFunc SndPair) $ \renamedFunT -> + withRenamedVals [Datatype "Pair" . Vector.fromList $ [integerT, byteStringT]] $ + tryAndApply byteStringT renamedFunT + +unitHeadList :: IO () +unitHeadList = withRenamedComp (typeOneArgFunc HeadList) $ \renamedFunT -> + withRenamedVals [Datatype "List" . Vector.singleton $ integerT] $ + tryAndApply integerT renamedFunT + +unitTailList :: IO () +unitTailList = withRenamedComp (typeOneArgFunc TailList) $ \renamedFunT -> + withRenamedVals (Identity . Datatype "List" . Vector.singleton $ integerT) $ \(Identity renamedArgT) -> + tryAndApply renamedArgT renamedFunT [renamedArgT] + +unitNullList :: IO () +unitNullList = withRenamedComp (typeOneArgFunc NullList) $ \renamedFunT -> + withRenamedVals [Datatype "List" . Vector.singleton $ integerT] $ + tryAndApply boolT renamedFunT + +unitMapData :: IO () +unitMapData = withRenamedComp (typeOneArgFunc MapData) $ \renamedFunT -> + let pairDataT = Datatype "Pair" . Vector.fromList $ [dataT, dataT] + in withRenamedVals [Datatype "List" . Vector.singleton $ pairDataT] $ + tryAndApply dataT renamedFunT + +unitListData :: IO () +unitListData = withRenamedComp (typeOneArgFunc ListData) $ \renamedFunT -> + withRenamedVals [Datatype "List" . Vector.singleton $ dataT] $ + tryAndApply dataT renamedFunT + +unitIData :: IO () +unitIData = withRenamedComp (typeOneArgFunc IData) $ \renamedFunT -> + withRenamedVals [integerT] $ tryAndApply dataT renamedFunT + +unitBData :: IO () +unitBData = withRenamedComp (typeOneArgFunc BData) $ \renamedFunT -> + withRenamedVals [byteStringT] $ tryAndApply dataT renamedFunT + +unitUnConstrData :: IO () +unitUnConstrData = withRenamedComp (typeOneArgFunc UnConstrData) $ \renamedFunT -> + withRenamedVals (Identity dataT) $ \(Identity renamedArgT) -> + let listDataT = Datatype "List" . Vector.singleton $ dataT + returnT = Datatype "Pair" . Vector.fromList $ [integerT, listDataT] + in tryAndApply returnT renamedFunT [renamedArgT] + +unitUnMapData :: IO () +unitUnMapData = withRenamedComp (typeOneArgFunc UnMapData) $ \renamedFunT -> + withRenamedVals (Identity dataT) $ \(Identity renamedArgT) -> + let pairDataT = Datatype "Pair" . Vector.fromList $ [dataT, dataT] + listPairDataT = Datatype "List" . Vector.singleton $ pairDataT + in tryAndApply listPairDataT renamedFunT [renamedArgT] + +unitUnListData :: IO () +unitUnListData = withRenamedComp (typeOneArgFunc UnListData) $ \renamedFunT -> + withRenamedVals [dataT] $ + tryAndApply (Datatype "List" . Vector.singleton $ dataT) renamedFunT + +unitUnIData :: IO () +unitUnIData = withRenamedComp (typeOneArgFunc UnIData) $ \renamedFunT -> + withRenamedVals [dataT] $ tryAndApply integerT renamedFunT + +unitUnBData :: IO () +unitUnBData = withRenamedComp (typeOneArgFunc UnBData) $ \renamedFunT -> + withRenamedVals [dataT] $ tryAndApply byteStringT renamedFunT + +unitSerialiseData :: IO () +unitSerialiseData = withRenamedComp (typeOneArgFunc SerialiseData) $ \renamedFunT -> + withRenamedVals [dataT] $ tryAndApply byteStringT renamedFunT + +unitMkCons :: IO () +unitMkCons = withRenamedComp (typeTwoArgFunc MkCons) $ \renamedFunT -> + let listT = Datatype "List" . Vector.singleton $ integerT + in withRenamedVals [integerT, listT] $ tryAndApply listT renamedFunT + +unitConstrData :: IO () +unitConstrData = withRenamedComp (typeTwoArgFunc ConstrData) $ \renamedFunT -> + let listT = Datatype "List" . Vector.singleton $ dataT + in withRenamedVals [integerT, listT] $ tryAndApply dataT renamedFunT + +unitEqualsData :: IO () +unitEqualsData = withRenamedComp (typeTwoArgFunc EqualsData) $ \renamedFunT -> + withRenamedVals [dataT, dataT] $ tryAndApply boolT renamedFunT + +unitMkPairData :: IO () +unitMkPairData = withRenamedComp (typeTwoArgFunc MkPairData) $ \renamedFunT -> + let pairDataT = Datatype "Pair" . Vector.fromList $ [dataT, dataT] + in withRenamedVals [dataT, dataT] $ tryAndApply pairDataT renamedFunT + +unitChooseList :: IO () +unitChooseList = withRenamedComp (typeThreeArgFunc ChooseList) $ \renamedFunT -> + let listT = Datatype "List" . Vector.singleton $ integerT + in withRenamedVals [listT, byteStringT, byteStringT] $ + tryAndApply byteStringT renamedFunT + +unitCaseList :: IO () +unitCaseList = withRenamedComp (typeThreeArgFunc CaseList) $ \renamedFunT -> + let listT = Datatype "List" . Vector.singleton $ integerT + thunkT = ThunkT $ Comp0 $ integerT :--:> listT :--:> ReturnT byteStringT + in withRenamedVals [byteStringT, thunkT, listT] $ + tryAndApply byteStringT renamedFunT + +unitChooseData :: IO () +unitChooseData = withRenamedComp (typeSixArgFunc ChooseData) $ \renamedFunT -> + withRenamedVals [dataT, integerT, integerT, integerT, integerT, integerT] $ + tryAndApply integerT renamedFunT + +unitCaseData :: IO () +unitCaseData = withRenamedComp (typeSixArgFunc CaseData) $ \renamedFunT -> + let listDataT = Datatype "List" . Vector.singleton $ dataT + pairDataT = Datatype "Pair" . Vector.fromList $ [dataT, dataT] + listPairDataT = Datatype "List" . Vector.singleton $ pairDataT + constrThunkT = ThunkT $ Comp0 $ integerT :--:> listDataT :--:> ReturnT integerT + mapThunkT = ThunkT $ Comp0 $ listPairDataT :--:> ReturnT integerT + listThunkT = ThunkT $ Comp0 $ listDataT :--:> ReturnT integerT + integerThunkT = ThunkT $ Comp0 $ integerT :--:> ReturnT integerT + byteStringThunkT = ThunkT $ Comp0 $ byteStringT :--:> ReturnT integerT + in withRenamedVals [constrThunkT, mapThunkT, listThunkT, integerThunkT, byteStringThunkT, dataT] $ + tryAndApply integerT renamedFunT + -- Helpers mkArgProp :: @@ -106,3 +304,33 @@ eqRenamedVar (BoundAt _ ix) = \case Unifiable ix' -> ix == ix' _ -> False + +withRenamedComp :: + CompT AbstractTy -> + (CompT Renamed -> IO ()) -> + IO () +withRenamedComp t f = case runRenameM . renameCompT $ t of + Left err -> assertFailure $ "Could not rename: " <> show err + Right t' -> f t' + +withRenamedVals :: + forall (t :: Type -> Type). + (Traversable t) => + t (ValT AbstractTy) -> + (t (ValT Renamed) -> IO ()) -> + IO () +withRenamedVals vals f = case runRenameM . traverse renameValT $ vals of + Left err -> assertFailure $ "Could not rename: " <> show err + Right vals' -> f vals' + +tryAndApply :: + ValT Renamed -> + CompT Renamed -> + [ValT Renamed] -> + IO () +tryAndApply expected f xs = case checkApp defaultDatatypes f . fmap Just $ xs of + Left err -> assertFailure $ "Could not apply: " <> show err + Right res -> assertEqual "" expected res + +dataT :: forall (a :: Type). ValT a +dataT = Datatype "Data" Vector.empty diff --git a/test/renaming/Main.hs b/test/renaming/Main.hs --- a/test/renaming/Main.hs +++ b/test/renaming/Main.hs @@ -8,7 +8,13 @@ ( ix0, ix1, ) -import Covenant.Test (Concrete (Concrete)) +import Covenant.Test + ( Concrete (Concrete), + RenameError (InvalidAbstractionReference), + renameCompT, + renameValT, + runRenameM, + ) import Covenant.Type ( BuiltinFlatT ( BLS12_381_G1_ElementT, @@ -20,16 +26,9 @@ StringT, UnitT ), - CompT (Comp0, Comp1, Comp2), - RenameError - ( InvalidAbstractionReference, - UndeterminedAbstraction - ), + CompT (Comp1, Comp2), Renamed (Unifiable, Wildcard), ValT (Abstraction, BuiltinFlat, ThunkT), - renameCompT, - renameValT, - runRenameM, tyvar, pattern ReturnT, pattern (:--:>), @@ -64,11 +63,6 @@ testCase "forall a b . a -> b -> !a" testConstT, testCase "forall a . a -> !(forall b . b -> !a)" testConstT2, testGroup - "Overdeterminance" - [ testCase "forall a b . a -> !(b -> !a)" testDodgyConstT, - testCase "forall a b . a -> !a" testDodgyIdT - ], - testGroup "Non-existent abstractions" [ testCase "forall a . b -> !a" testIndexingIdT ] @@ -138,29 +132,6 @@ let result = runRenameM . renameCompT $ constT assertRight (assertEqual "" expected) result --- Checks that `forall a b . a -> !a` triggers the undetermined variable checker. -testDodgyIdT :: IO () -testDodgyIdT = do - let idT = Comp2 $ tyvar Z ix0 :--:> ReturnT (tyvar Z ix0) - let result = runRenameM . renameCompT $ idT - case result of - Left UndeterminedAbstraction -> assertBool "" True - Left _ -> assertBool "wrong renaming error" False - _ -> assertBool "renaming succeeded when it should have failed" False - --- Checks that `forall a b. a -> !(b -> !a)` triggers the undetermined variable checker. -testDodgyConstT :: IO () -testDodgyConstT = do - let constT = - Comp2 $ - tyvar Z ix0 - :--:> ReturnT (ThunkT . Comp0 $ tyvar (S Z) ix1 :--:> ReturnT (tyvar (S Z) ix0)) - let result = runRenameM . renameCompT $ constT - case result of - Left UndeterminedAbstraction -> assertBool "" True - Left _ -> assertBool "wrong renaming error" False - _ -> assertBool "renaming succeeded when it should have failed" False - -- Checks that `forall a . b -> !a` triggers the variable indexing checker. testIndexingIdT :: IO () testIndexingIdT = do @@ -170,7 +141,6 @@ Left (InvalidAbstractionReference trueLevel ix) -> do assertEqual "" trueLevel 1 assertEqual "" ix ix1 - Left _ -> assertBool "wrong renaming error" False _ -> assertBool "renaming succeeded when it should have failed" False -- Helpers diff --git a/test/type-applications/Main.hs b/test/type-applications/Main.hs --- a/test/type-applications/Main.hs +++ b/test/type-applications/Main.hs @@ -4,39 +4,47 @@ import Control.Applicative ((<|>)) import Control.Monad (guard) +import Covenant.ASG + ( TypeAppError + ( DoesNotUnify, + ExcessArgs, + InsufficientArgs + ), + ) import Covenant.DeBruijn (DeBruijn (S, Z), asInt) import Covenant.Index ( Index, ix0, ix1, + ix2, ) -import Covenant.Test (Concrete (Concrete)) -import Covenant.Type - ( AbstractTy, - CompT (Comp0, Comp1, Comp2), - Renamed (Rigid, Wildcard), - TypeAppError - ( DoesNotUnify, - ExcessArgs, - InsufficientArgs - ), - ValT - ( Abstraction, - ThunkT - ), +import Covenant.Test + ( Concrete (Concrete), checkApp, - integerT, + failLeft, renameCompT, renameValT, runRenameM, + tyAppTestDatatypes, + ) +import Covenant.Type + ( AbstractTy, + BuiltinFlatT (BoolT, IntegerT, UnitT), + CompT (Comp0, Comp1, Comp2, Comp3), + Renamed (Rigid, Unifiable, Wildcard), + ValT (Abstraction, BuiltinFlat, Datatype, ThunkT), + integerT, tyvar, pattern ReturnT, pattern (:--:>), ) +import Covenant.Util (prettyStr) import Data.Coerce (coerce) import Data.Functor.Identity (Identity (Identity)) import Data.Kind (Type) +import Data.Map qualified as M import Data.Vector qualified as Vector +import Optics.Core (review) import Test.QuickCheck ( Gen, Property, @@ -53,7 +61,7 @@ vectorOf, (===), ) -import Test.Tasty (adjustOption, defaultMain, testGroup) +import Test.Tasty (TestTree, adjustOption, defaultMain, testGroup) import Test.Tasty.HUnit (assertEqual, assertFailure, testCase) import Test.Tasty.QuickCheck (QuickCheckTests, testProperty) @@ -77,7 +85,21 @@ testProperty "concrete expected, rigid actual" propUnifyConcreteRigid, testProperty "unifiable expected, rigid actual" propUnifyUnifiableRigid, testProperty "rigid expected, rigid actual" propUnifyRigid, - testProperty "wildcard expected, rigid actual" propUnifyWildcardRigid + testProperty "wildcard expected, rigid actual" propUnifyWildcardRigid, + testProperty "thunk with unifiable result" propThunkWithUnifiableResult + ], + testGroup + "Datatypes" + [ testEitherConcrete, + polymorphicApplicationM, + polymorphicApplicationE, + polymorphicApplicationP, + unifyMaybe, + testCase "nested datatypes" unitNestedDatatypes, + testProperty "thunk with datatype argument" propThunkWithDatatype, + testProperty "concrete thunk with datatype argument" propConcreteThunkWithDatatype, + testProperty "thunk with unifiable and datatype argument" propThunkUnifiableWithDatatype, + testProperty "thunk with unifiable datatype" propThunkUnifiableDatatype ] ] where @@ -100,7 +122,7 @@ [] -> discard -- should be impossible _ : extraArgs -> let expected = Left . ExcessArgs renamedIdT . Vector.fromList . fmap Just $ extraArgs - actual = checkApp renamedIdT (fmap Just renamedExcessArgs) + actual = checkApp M.empty renamedIdT (fmap Just renamedExcessArgs) in expected === actual where -- Note (Koz, 14/04/2025): The default size of 100 makes it rather painful @@ -126,8 +148,8 @@ unitInsufficientArgs :: IO () unitInsufficientArgs = do renamedIdT <- failLeft . runRenameM . renameCompT $ idT - let expected = Left . InsufficientArgs $ renamedIdT - let actual = checkApp renamedIdT [] + let expected = Left $ InsufficientArgs 0 renamedIdT [] + let actual = checkApp M.empty renamedIdT [] assertEqual "" expected actual -- Try to apply `forall a . a -> !a` to a random concrete type. Result should be @@ -137,7 +159,7 @@ withRenamedComp idT $ \renamedIdT -> withRenamedVals (Identity t) $ \(Identity t') -> let expected = Right t' - actual = checkApp renamedIdT [Just t'] + actual = checkApp M.empty renamedIdT [Just t'] in expected === actual -- Try to apply `forall a b . a -> b -> !a` to two identical concrete types. @@ -147,7 +169,7 @@ withRenamedComp const2T $ \renamedConst2T -> withRenamedVals (Identity t) $ \(Identity t') -> let expected = Right t' - actual = checkApp renamedConst2T [Just t', Just t'] + actual = checkApp M.empty renamedConst2T [Just t', Just t'] in expected === actual -- Try to apply `forall a b . a -> b -> !a` to two random _different_ concrete @@ -160,7 +182,7 @@ withRenamedVals (Identity t1) $ \(Identity t1') -> withRenamedVals (Identity t2) $ \(Identity t2') -> let expected = Right t1' - actual = checkApp renamedConst2T [Just t1', Just t2'] + actual = checkApp M.empty renamedConst2T [Just t1', Just t2'] in expected === actual -- Randomly pick a concrete type `A`, then pick a type `b` which is either `A` @@ -174,14 +196,14 @@ case mtB of Nothing -> let expected = Right integerT - actual = checkApp f [Just tA'] + actual = checkApp M.empty f [Just tA'] in expected === actual Just tB -> if tA == tB then discard else withRenamedVals (Identity tB) $ \(Identity arg) -> let expected = Left . DoesNotUnify tA' $ arg - actual = checkApp f [Just arg] + actual = checkApp M.empty f [Just arg] in expected === actual where -- This ensures that our cases occur with equal frequency. @@ -210,9 +232,9 @@ -- be based on `S scope`, since that's what's in the computation type. -- However, we actually have to reduce it by 1, as we have a 'scope -- stepdown' for `f` even though we bind no variables. - let trueLevel = negate . asInt $ scope + let trueLevel = negate . review asInt $ scope expected = Left . DoesNotUnify (Abstraction . Rigid trueLevel $ ix) $ t' - actual = checkApp f [Just t'] + actual = checkApp M.empty f [Just t'] in expected === actual -- Randomly pick a concrete type A, then try to apply `(forall a . a -> @@ -225,7 +247,7 @@ in withRenamedVals (Identity argT) $ \(Identity argT') -> let lhs = ThunkT . Comp1 $ Abstraction (Wildcard 1 2 ix0) :--:> ReturnT integerT expected = Left . DoesNotUnify lhs $ argT' - actual = checkApp f [Just argT'] + actual = checkApp M.empty f [Just argT'] in expected === actual -- Randomly generate a concrete type A, then try to apply @@ -237,7 +259,7 @@ withRenamedVals (Identity t) $ \(Identity t') -> withRenamedVals (Identity . ThunkT . Comp1 $ tyvar Z ix0 :--:> ReturnT t) $ \(Identity arg) -> let expected = Right t' - actual = checkApp f [Just arg] + actual = checkApp M.empty f [Just arg] in expected === actual -- Randomly generate a concrete type A, and a rigid type B, then try to apply `A @@ -247,9 +269,9 @@ withRenamedComp (Comp0 $ aT :--:> ReturnT integerT) $ \f -> withRenamedVals (Identity $ tyvar scope index) $ \(Identity arg) -> withRenamedVals (Identity aT) $ \(Identity aT') -> - let level = negate . asInt $ scope + let level = negate . review asInt $ scope expected = Left . DoesNotUnify aT' . Abstraction . Rigid level $ index - actual = checkApp f [Just arg] + actual = checkApp M.empty f [Just arg] in expected === actual -- Randomly generate a rigid type A, then try to apply `forall a . a -> !a` to @@ -259,7 +281,7 @@ withRenamedComp idT $ \f -> withRenamedVals (Identity $ tyvar scope index) $ \(Identity arg) -> let expected = Right arg - actual = checkApp f [Just arg] + actual = checkApp M.empty f [Just arg] in expected === actual -- Randomly generate a scope S and an index I, then another scope S' and another @@ -271,7 +293,7 @@ propUnifyRigid :: Property propUnifyRigid = forAllShrink gen shr $ \testData -> withTestData testData $ \(f, arg, expected) -> - let actual = checkApp f [Just arg] + let actual = checkApp M.empty f [Just arg] in expected === actual where gen :: Gen (DeBruijn, Index "tyvar", Maybe (Either DeBruijn (Index "tyvar"))) @@ -312,7 +334,7 @@ Nothing -> withRenamedVals (Identity . tyvar db $ index) $ \(Identity arg) -> f (fun, arg, Right integerT) Just rest -> - let level = negate . asInt $ db + let level = negate . review asInt $ db lhs = Abstraction . Rigid level $ index in case rest of Left db2 -> withRenamedVals (Identity . tyvar db2 $ index) $ \(Identity arg) -> @@ -330,9 +352,204 @@ in withRenamedVals (Identity argT) $ \(Identity argT') -> let lhs = ThunkT . Comp1 $ Abstraction (Wildcard 1 2 ix0) :--:> ReturnT integerT expected = Left . DoesNotUnify lhs $ argT' - actual = checkApp f [Just argT'] + actual = checkApp M.empty f [Just argT'] in expected === actual +-- Randomly pick concrete types A and B, then try to apply to `forall a . ((A -> B -> +-- !a) -> !a)` the argument `(A -> B -> !A)`. Result should unify and produce +-- `A`. +propThunkWithUnifiableResult :: Property +propThunkWithUnifiableResult = forAllShrink arbitrary shrink $ \(Concrete aT, Concrete bT) -> + let funThunkArgT = ThunkT $ Comp0 $ aT :--:> bT :--:> ReturnT (tyvar (S Z) ix0) + funT = Comp1 $ funThunkArgT :--:> ReturnT (tyvar Z ix0) + thunkT = ThunkT $ Comp0 $ aT :--:> bT :--:> ReturnT aT + in withRenamedComp funT $ \f -> + withRenamedVals (Identity thunkT) $ \(Identity argT) -> + withRenamedVals (Identity aT) $ \(Identity aT') -> + let expected = Right aT' + actual = checkApp M.empty f [Just argT] + in expected === actual + +-- Tries to apply some concrete types to `defaultLeft`, checks that the return type is +-- correct after unification (via checkApp) +testEitherConcrete :: TestTree +testEitherConcrete = testCase "testEitherConcrete" $ do + -- a == unit + -- b == bool + -- c == integer + let arg1 = BuiltinFlat IntegerT + arg2 = ThunkT (Comp0 $ BuiltinFlat BoolT :--:> ReturnT (BuiltinFlat IntegerT)) + arg3 = Datatype "Either" . Vector.fromList $ [BuiltinFlat UnitT, BuiltinFlat BoolT] + + expected = BuiltinFlat IntegerT + defaultLeftRenamed <- failLeft . runRenameM . renameCompT $ defaultLeft + actual <- + either (assertFailure . show) pure $ + checkApp + tyAppTestDatatypes + defaultLeftRenamed + (pure <$> [arg1, arg2, arg3]) + assertEqual "testEitherConcrete" expected actual + +-- Tries to apply arguments containing a mixture of concrete and abstract types to the BB form for maybe, +-- then checks whether the application types as the (concrete) return type. +-- note: The order of args is wrong for a Plutus "Maybe" (but that doesn't matter). BB form is: +-- forall a r. r -> (a -> r) -> r +-- (Plutus defines 'Maybe' incorrectly, i.e., with the 'Just' ctor first) +polymorphicApplicationM :: TestTree +polymorphicApplicationM = testCase "polyAppMaybe" $ do + let testFn = + Comp1 $ + ( ThunkT . Comp1 $ + tyvar Z ix0 + :--:> ThunkT (Comp0 (tyvar (S (S Z)) ix0 :--:> ReturnT (tyvar (S Z) ix0))) + :--:> ReturnT (tyvar Z ix0) + ) + :--:> ReturnT (BuiltinFlat IntegerT) + testArg = + ThunkT . Comp1 $ + tyvar Z ix0 + :--:> ThunkT (Comp0 (BuiltinFlat BoolT :--:> ReturnT (tyvar (S Z) ix0))) + :--:> ReturnT (tyvar Z ix0) + fnRenamed <- failLeft . runRenameM . renameCompT $ testFn + argRenamed <- failLeft . runRenameM . renameValT $ testArg + result <- + either (assertFailure . show) pure $ + checkApp tyAppTestDatatypes fnRenamed [Just argRenamed] + assertEqual "polyAppMaybe" result (BuiltinFlat IntegerT) + +-- Applies a mixture of polymorphic and concrete arguments to `defaultLeft` and checks that the return +-- type is what we expected after unification +polymorphicApplicationE :: TestTree +polymorphicApplicationE = testCase "polyAppEither" $ do + -- a = a' (arbitrary unifiable) + -- b = Bool + -- c = Integer + let arg1 = Abstraction $ Unifiable ix0 + arg2 = ThunkT (Comp0 $ BuiltinFlat BoolT :--:> ReturnT (BuiltinFlat IntegerT)) + arg3 = Datatype "Either" . Vector.fromList $ [arg1, BuiltinFlat BoolT] + fnRenamed <- failLeft . runRenameM . renameCompT $ defaultLeft + actual <- + either (assertFailure . show) pure $ + checkApp tyAppTestDatatypes fnRenamed (pure <$> [arg1, arg2, arg3]) + assertEqual "polyAppEither" actual (BuiltinFlat IntegerT) + +-- Applies a mixture of polymorphic and concrete arguments to `defaultPair` and checks that the return type +-- is what we expected after unification +polymorphicApplicationP :: TestTree +polymorphicApplicationP = testCase "polyAppPair" $ do + -- a = a' (arbitrary unifiable) + -- b = Bool + -- c = Integer + let arg1 = Abstraction $ Unifiable ix0 + arg2 = BuiltinFlat BoolT + arg3 = ThunkT $ Comp0 $ Abstraction (Rigid 1 ix0) :--:> BuiltinFlat BoolT :--:> ReturnT (BuiltinFlat IntegerT) + arg4 = Datatype "Pair" (Vector.fromList [arg1, BuiltinFlat BoolT]) + fnRenamed <- failLeft . runRenameM . renameCompT $ defaultPair + actual <- + either (assertFailure . show) pure $ + checkApp tyAppTestDatatypes fnRenamed (pure <$> [arg1, arg2, arg3, arg4]) + assertEqual "polyAppPair" actual (BuiltinFlat IntegerT) + +-- Checks whether `forall a. Maybe a -> Integer` unifies properly with `Maybe Bool -> Integer` +unifyMaybe :: TestTree +unifyMaybe = testCase "unifyMaybe" $ do + let testFn = + Comp1 $ + Datatype "Maybe" (Vector.fromList [tyvar Z ix0]) + :--:> ReturnT (BuiltinFlat IntegerT) + testArg = Datatype "Maybe" (Vector.fromList [BuiltinFlat BoolT]) + fnRenamed <- failLeft . runRenameM . renameCompT $ testFn + result <- + either (assertFailure . catchInsufficientArgs) pure $ + checkApp tyAppTestDatatypes fnRenamed [Just testArg] + assertEqual "unifyMaybe" result (BuiltinFlat IntegerT) + where + catchInsufficientArgs :: TypeAppError -> String + catchInsufficientArgs = \case + InsufficientArgs _ fn _ -> prettyStr fn + other -> show other + +-- Checks that `forall a . Maybe a -> Maybe (Maybe a)`, when applied to `Maybe +-- Integer`, produces `Maybe (Maybe Integer)` +unitNestedDatatypes :: IO () +unitNestedDatatypes = do + let fn = + Comp1 $ + Datatype "Maybe" (Vector.singleton $ tyvar Z ix0) + :--:> ReturnT (Datatype "Maybe" (Vector.singleton . Datatype "Maybe" . Vector.singleton $ tyvar Z ix0)) + fnRenamed <- failLeft . runRenameM . renameCompT $ fn + let arg = Datatype "Maybe" . Vector.singleton $ integerT + let expected = Datatype "Maybe" . Vector.singleton . Datatype "Maybe" . Vector.singleton $ integerT + case checkApp tyAppTestDatatypes fnRenamed [Just arg] of + Left err -> assertFailure . show $ err + Right res -> assertEqual "type mismatch" expected res + +-- Randomly pick concrete types A and B, then try to apply to `forall a. ((A -> +-- Maybe B -> !a) -> !a)` the argument `(A -> Maybe B -> !A)`. Result should +-- unify and produce `A`. +propThunkWithDatatype :: Property +propThunkWithDatatype = forAllShrink arbitrary shrink $ \(Concrete aT, Concrete bT) -> + let maybeT = Datatype "Maybe" (Vector.singleton bT) + funThunkArg = ThunkT $ Comp0 $ aT :--:> maybeT :--:> ReturnT (tyvar (S Z) ix0) + funT = Comp1 $ funThunkArg :--:> ReturnT (tyvar Z ix0) + thunkT = ThunkT $ Comp0 $ aT :--:> maybeT :--:> ReturnT aT + in withRenamedComp funT $ \f -> + withRenamedVals (Identity thunkT) $ \(Identity argT) -> + withRenamedVals (Identity aT) $ \(Identity aT') -> + let expected = Right aT' + actual = checkApp tyAppTestDatatypes f [Just argT] + in expected === actual + +-- Randomly pick concrete types A and B, then try to apply to `((A -> Maybe B -> +-- !A) -> !A)` the argument `(A -> Maybe B -> !A)`. Result should unify and +-- produce `A`. +propConcreteThunkWithDatatype :: Property +propConcreteThunkWithDatatype = forAllShrink arbitrary shrink $ \(Concrete aT, Concrete bT) -> + let maybeT = Datatype "Maybe" (Vector.singleton bT) + funThunkArg = ThunkT $ Comp0 $ aT :--:> maybeT :--:> ReturnT aT + funT = Comp0 $ funThunkArg :--:> ReturnT aT + thunkT = ThunkT $ Comp0 $ aT :--:> maybeT :--:> ReturnT aT + in withRenamedComp funT $ \f -> + withRenamedVals (Identity thunkT) $ \(Identity argT) -> + withRenamedVals (Identity aT) $ \(Identity aT') -> + let expected = Right aT' + actual = checkApp tyAppTestDatatypes f [Just argT] + in expected === actual + +-- Randomly pick concrete types A and B, then try to apply to `forall a. ((a -> Maybe B +-- -> !A) -> !A)` the argument `(A -> Maybe B -> !A)`. Result should unify and +-- produce `A`. +propThunkUnifiableWithDatatype :: Property +propThunkUnifiableWithDatatype = forAllShrink arbitrary shrink $ \(Concrete aT, Concrete bT) -> + let maybeT = Datatype "Maybe" (Vector.singleton bT) + funThunkArg = ThunkT $ Comp1 $ tyvar (S Z) ix0 :--:> maybeT :--:> ReturnT aT + funT = Comp1 $ funThunkArg :--:> ReturnT aT + thunkT = ThunkT $ Comp0 $ aT :--:> maybeT :--:> ReturnT aT + in withRenamedComp funT $ \f -> + withRenamedVals (Identity thunkT) $ \(Identity argT) -> + withRenamedVals (Identity aT) $ \(Identity aT') -> + let expected = Right aT' + actual = checkApp tyAppTestDatatypes f [Just argT] + in expected === actual + +-- Randomly pick concrete type A, then try to apply to `forall a . ((Maybe A -> +-- !a) -> !a)` the argument `(Maybe A -> !A)`. Result should unify and produce +-- `A`. +propThunkUnifiableDatatype :: Property +propThunkUnifiableDatatype = forAllShrink arbitrary shrink $ \(Concrete aT) -> + let -- maybeTUnifiable = Datatype "Maybe" . Vector.singleton $ tyvar (S Z) ix0 + maybeTConcrete = Datatype "Maybe" . Vector.singleton $ aT + funThunkArg = ThunkT $ Comp0 $ maybeTConcrete :--:> ReturnT (tyvar (S Z) ix0) + funT = Comp1 $ funThunkArg :--:> ReturnT (tyvar Z ix0) + thunkT = ThunkT $ Comp0 $ maybeTConcrete :--:> ReturnT aT + in withRenamedComp funT $ \f -> + withRenamedVals (Identity thunkT) $ \(Identity argT) -> + withRenamedVals (Identity aT) $ \(Identity aT') -> + let expected = Right aT' + actual = checkApp tyAppTestDatatypes f [Just argT] + in expected === actual + -- Helpers -- `forall a. a -> !a` @@ -343,12 +560,25 @@ const2T :: CompT AbstractTy const2T = Comp2 $ tyvar Z ix0 :--:> tyvar Z ix1 :--:> ReturnT (tyvar Z ix0) -failLeft :: - forall (a :: Type) (b :: Type). - (Show a) => - Either a b -> - IO b -failLeft = either (assertFailure . show) pure +-- forall a b c. c -> (b -> !c) -> Either a b -> !c +-- ...I hope +defaultLeft :: CompT AbstractTy +defaultLeft = + Comp3 $ + tyvar Z ix2 + :--:> ThunkT (Comp0 $ tyvar (S Z) ix1 :--:> ReturnT (tyvar (S Z) ix2)) + :--:> Datatype "Either" (Vector.fromList [tyvar Z ix0, tyvar Z ix1]) + :--:> ReturnT (tyvar Z ix2) + +-- forall a b c. a -> b -> (a -> b -> !c) -> Pair a b -> c +defaultPair :: CompT AbstractTy +defaultPair = + Comp3 $ + tyvar Z ix0 + :--:> tyvar Z ix1 + :--:> ThunkT (Comp0 $ tyvar (S Z) ix0 :--:> tyvar (S Z) ix1 :--:> ReturnT (tyvar (S Z) ix2)) + :--:> Datatype "Pair" (Vector.fromList [tyvar Z ix0, tyvar Z ix1]) + :--:> ReturnT (tyvar Z ix2) withRenamedComp :: CompT AbstractTy ->