diff --git a/src-tool/Pact/Analyze/Feature.hs b/src-tool/Pact/Analyze/Feature.hs index 4127a5456..58d3ae34c 100644 --- a/src-tool/Pact/Analyze/Feature.hs +++ b/src-tool/Pact/Analyze/Feature.hs @@ -9,7 +9,105 @@ -- the invariant and property languages. Note that currently this omits -- features found in the Pact term language that do not appear in either -- properties or invariants -- e.g. @write@ for modifying a database table. -module Pact.Analyze.Feature where +module Pact.Analyze.Feature +( Availability(..) +, Bindings(..) +, ConcreteType(..) +, Constraint(..) +, FormType(..) +, Type(..) +, TypeVar(..) +, Usage(..) +, Var(..) +, availability +, availableFeatures +, classFeatures +, classTitle +, mkOpNamePrism +, pattern Feature +, symbolFeatures +, toDoc +, toOp +, writeTypeP + +, pattern SAddition +, pattern SSubtraction +, pattern SMultiplication +, pattern SDivision +, pattern SExponentiation +, pattern SLogarithm +, pattern SNumericNegation +, pattern SSquareRoot +, pattern SNaturalLogarithm +, pattern SExponential +, pattern SAbsoluteValue +, pattern SBankersRound +, pattern SCeilingRound +, pattern SFloorRound +, pattern SModulus +, pattern SBitwiseAnd +, pattern SBitwiseOr +, pattern SXor +, pattern SShift +, pattern SComplement +, pattern SGreaterThan +, pattern SLessThan +, pattern SGreaterThanOrEqual +, pattern SLessThanOrEqual +, pattern SEquality +, pattern SInequality +, pattern SLogicalConjunction +, pattern SLogicalDisjunction +, pattern SLogicalNegation +, pattern SLogicalImplication +, pattern SAndQ +, pattern SOrQ +, pattern SObjectProjection +, pattern SListLength +, pattern SContains +, pattern SReverse +, pattern SSort +, pattern SListDrop +, pattern SListTake +, pattern SMakeList +, pattern SMap +, pattern SFilter +, pattern SFold +, pattern SObjectMerge +, pattern SObjectDrop +, pattern SObjectTake +, pattern SObjectLength +, pattern SStringLength +, pattern SConcatenation +, pattern SStringToInteger +, pattern STemporalAddition +, pattern SUniversalQuantification +, pattern SExistentialQuantification +, pattern SColumnOf +, pattern STransactionAborts +, pattern STransactionSucceeds +, pattern SGovernancePasses +, pattern SFunctionResult +, pattern STableWritten +, pattern STableRead +, pattern SCellDelta +, pattern SColumnDelta +, pattern SColumnWritten +, pattern SColumnRead +, pattern SRowRead +, pattern SRowWritten +, pattern SRowReadCount +, pattern SRowWriteCount +, pattern SRowExists +, pattern SPropRead +, pattern SAuthorizedBy +, pattern SRowEnforced +, pattern SIdentity +, pattern SConstantly +, pattern SCompose +, pattern SWhere +, pattern STypeof +) where import Control.Lens (Prism', preview, prism', review) import Data.Foldable (foldl') diff --git a/src-tool/Pact/Analyze/Parse/Prop.hs b/src-tool/Pact/Analyze/Parse/Prop.hs index 39358faef..3088f5818 100644 --- a/src-tool/Pact/Analyze/Parse/Prop.hs +++ b/src-tool/Pact/Analyze/Parse/Prop.hs @@ -67,8 +67,7 @@ import Pact.Types.Lang hiding (KeySet, KeySetName, TableName, TyObject, Type, TyList) import Pact.Types.Pretty -import Pact.Analyze.Feature hiding (Doc, Type, Var, ks, obj, - str) +import Pact.Analyze.Feature hiding (Type, Var) import Pact.Analyze.Parse.Types import Pact.Analyze.PrenexNormalize import Pact.Analyze.Types diff --git a/src-tool/Pact/Analyze/Parse/Types.hs b/src-tool/Pact/Analyze/Parse/Types.hs index 6faa82d1c..d78c8a5da 100644 --- a/src-tool/Pact/Analyze/Parse/Types.hs +++ b/src-tool/Pact/Analyze/Parse/Types.hs @@ -33,8 +33,7 @@ import qualified Pact.Types.Lang as Pact import Pact.Types.Typecheck (UserType) import Pact.Types.Pretty -import Pact.Analyze.Feature hiding (Doc, Type, Var, ks, obj, - str) +import Pact.Analyze.Feature hiding (Type, Var) import Pact.Analyze.Types -- @PreProp@ stands between @Exp@ and @Prop@. diff --git a/src-tool/Pact/Analyze/Translate.hs b/src-tool/Pact/Analyze/Translate.hs index 0a9c6b934..d3deda0b1 100644 --- a/src-tool/Pact/Analyze/Translate.hs +++ b/src-tool/Pact/Analyze/Translate.hs @@ -61,8 +61,7 @@ import Pact.Types.Typecheck (AST, Named (..), Node, aId, import qualified Pact.Types.Typecheck as Pact import Pact.Types.Util (tShow) -import Pact.Analyze.Feature hiding (TyFun, TyVar, Var, col, - list, obj, str, time) +import Pact.Analyze.Feature hiding (TyFun, TyVar, Var) import Pact.Analyze.Patterns import Pact.Analyze.Types import Pact.Analyze.Util diff --git a/src-tool/Pact/Analyze/Types/Eval.hs b/src-tool/Pact/Analyze/Types/Eval.hs index 77ec66450..6fce87c73 100644 --- a/src-tool/Pact/Analyze/Types/Eval.hs +++ b/src-tool/Pact/Analyze/Types/Eval.hs @@ -27,6 +27,7 @@ import Control.Lens (Lens', at, ifoldl, iso, ix, lens, import Control.Lens.Wrapped import Control.Monad.Except (MonadError) import Control.Monad.Reader (MonadReader) +import Data.Kind (Type) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.Maybe (mapMaybe) @@ -44,7 +45,6 @@ import GHC.Generics hiding (S) import GHC.Stack (HasCallStack) import Pact.Types.Lang (Info) -import Pact.Types.Runtime (Type (TyPrim)) import qualified Pact.Types.Runtime as Pact import qualified Pact.Types.Typecheck as Pact @@ -69,7 +69,7 @@ instance Wrapped SymbolicSuccess where _Wrapped' = iso successBool SymbolicSuccess class (MonadError AnalyzeFailure m, S :*<: TermOf m) => Analyzer m where - type TermOf m :: Ty -> * + type TermOf m :: Ty -> Type eval :: SingI a => TermOf m a -> m (S (Concrete a)) throwErrorNoLoc :: AnalyzeFailureNoLoc -> m a getVar :: VarId -> m (Maybe AVal) @@ -430,10 +430,10 @@ mkInitialAnalyzeState trivialGuard tables caps = AnalyzeState tableNames :: [TableName] tableNames = map (TableName . T.unpack . view Types.tableName) tables - intCellDeltas = mkTableColumnMap tables (== TyPrim Pact.TyInteger) (mkPactSFunArray (const 0)) - decCellDeltas = mkTableColumnMap tables (== TyPrim Pact.TyDecimal) (mkPactSFunArray (const (fromInteger 0))) - intColumnDeltas = mkTableColumnMap tables (== TyPrim Pact.TyInteger) 0 - decColumnDeltas = mkTableColumnMap tables (== TyPrim Pact.TyDecimal) (fromInteger 0) + intCellDeltas = mkTableColumnMap tables (== Pact.TyPrim Pact.TyInteger) (mkPactSFunArray (const 0)) + decCellDeltas = mkTableColumnMap tables (== Pact.TyPrim Pact.TyDecimal) (mkPactSFunArray (const (fromInteger 0))) + intColumnDeltas = mkTableColumnMap tables (== Pact.TyPrim Pact.TyInteger) 0 + decColumnDeltas = mkTableColumnMap tables (== Pact.TyPrim Pact.TyDecimal) (fromInteger 0) cellsEnforced = mkTableColumnMap tables isGuardTy (mkPactSFunArray (const sFalse)) cellsWritten = mkTableColumnMap tables (const True) (mkPactSFunArray (const sFalse)) diff --git a/src-tool/Pact/Analyze/Types/Languages.hs b/src-tool/Pact/Analyze/Types/Languages.hs index 0a7d7ad11..5388e076d 100644 --- a/src-tool/Pact/Analyze/Types/Languages.hs +++ b/src-tool/Pact/Analyze/Types/Languages.hs @@ -76,6 +76,7 @@ module Pact.Analyze.Types.Languages , propToInvariant ) where +import qualified Data.Kind as K (Type) import Control.Lens (Prism', review, preview, prism') import Control.Monad ((>=>)) import Data.Maybe (fromMaybe) @@ -96,8 +97,7 @@ import Pact.Types.Pretty (commaBraces, commaBrackets, RenderColor(RPlain)) import Pact.Types.Persistence (WriteType) -import Pact.Analyze.Feature hiding (Doc, Sym, Var, col, str, - obj, dec, ks) +import Pact.Analyze.Feature hiding (Sym, Var) import Pact.Analyze.Types.Capability import Pact.Analyze.Types.Model import Pact.Analyze.Types.Numerical @@ -110,7 +110,7 @@ import Pact.Analyze.Util -- -- This can be read as "subtype", where we can always 'inject' the subtype into -- its supertype and sometimes 'project' the supertype down. -class (sub :: Ty -> *) :<: (sup :: Ty -> *) where +class (sub :: Ty -> K.Type) :<: (sup :: Ty -> K.Type) where subP :: Prism' (sup a) (sub a) -- | Inject a subtype into a supertype via 'subP' @@ -134,7 +134,7 @@ pattern Inj a <- (project -> Just a) where -- the type on the left is indexed by a *concrete* type. For example, @S -- Integer@ is injectable into @Term TyInteger@ because @Integer ~ Concrete -- TyInteger@. -class (sub :: * -> *) :*<: (sup :: Ty -> *) where +class (sub :: K.Type -> K.Type) :*<: (sup :: Ty -> K.Type) where subP' :: Prism' (sup a) (sub (Concrete a)) -- | Inject a subtype into a supertype via 'subP'' @@ -146,7 +146,7 @@ project' :: sub :*<: sup => sup a -> Maybe (sub (Concrete a)) project' = preview subP' -- | An open term (@: b@) with a free variable (@: a@). -data Open (a :: Ty) (tm :: Ty -> *) (b :: Ty) = Open !VarId !Text !(tm b) +data Open (a :: Ty) (tm :: Ty -> K.Type) (b :: Ty) = Open !VarId !Text !(tm b) deriving (Eq, Show) -- | Core terms. @@ -168,7 +168,7 @@ data Open (a :: Ty) (tm :: Ty -> *) (b :: Ty) = Open !VarId !Text !(tm b) -- * @add-time@ -- * @at@ -- * lit operations -data Core (t :: Ty -> *) (a :: Ty) where +data Core (t :: Ty -> K.Type) (a :: Ty) where Lit :: Concrete a -> Core t a -- | Injects a symbolic value into the language Sym :: S (Concrete a) -> Core t a diff --git a/src-tool/Pact/Analyze/Types/Numerical.hs b/src-tool/Pact/Analyze/Types/Numerical.hs index 4e98d7c88..a68753d10 100644 --- a/src-tool/Pact/Analyze/Types/Numerical.hs +++ b/src-tool/Pact/Analyze/Types/Numerical.hs @@ -34,7 +34,7 @@ import qualified Data.SBV.Internals as SBVI import Data.Text (Text) import GHC.Real ((%)) -import Pact.Analyze.Feature hiding (Constraint, dec) +import Pact.Analyze.Feature hiding (Constraint) import Pact.Analyze.Types.Types import Pact.Types.Pretty (Pretty(..), parensSep, viaShow) diff --git a/src-tool/Pact/Analyze/Types/ObjUtil.hs b/src-tool/Pact/Analyze/Types/ObjUtil.hs index 98b073f6b..6b22ac0fa 100644 --- a/src-tool/Pact/Analyze/Types/ObjUtil.hs +++ b/src-tool/Pact/Analyze/Types/ObjUtil.hs @@ -36,6 +36,7 @@ module Pact.Analyze.Types.ObjUtil , sansProof ) where +import Data.Kind (Type) import Data.Type.Bool (If) import Data.Type.Equality (type (==)) import Data.Typeable (Typeable) @@ -105,7 +106,7 @@ filterV (flag :: Flag) (p :: Symbol) (xs :: [ (Symbol, Ty) ]) - (f :: Ty -> *). + (f :: Ty -> Type). Sing flag -> Sing p -> HList f xs diff --git a/src-tool/Pact/Analyze/Types/Shared.hs b/src-tool/Pact/Analyze/Types/Shared.hs index 92c1a2155..56dcda4c1 100644 --- a/src-tool/Pact/Analyze/Types/Shared.hs +++ b/src-tool/Pact/Analyze/Types/Shared.hs @@ -73,8 +73,7 @@ import qualified Pact.Types.Lang as Pact import Pact.Types.Util (AsString) import Pact.Analyze.PactSFunArray (PactSFunArray) -import Pact.Analyze.Feature hiding (Constraint, Doc, Type, - dec, ks, obj, str, time) +import Pact.Analyze.Feature hiding (Constraint, Type) import Pact.Analyze.Types.Numerical import Pact.Analyze.Types.ObjUtil import Pact.Analyze.Types.Types diff --git a/src/Pact/Types/Scheme.hs b/src/Pact/Types/Scheme.hs index a1434eac4..8ccfeebde 100644 --- a/src/Pact/Types/Scheme.hs +++ b/src/Pact/Types/Scheme.hs @@ -14,6 +14,7 @@ module Pact.Types.Scheme import GHC.Generics import Control.DeepSeq +import Data.Kind import Data.Serialize import Data.Aeson @@ -48,7 +49,7 @@ defPPKScheme = ED25519 -- Run-time witness to PPKScheme kind. -data SPPKScheme :: PPKScheme -> * where +data SPPKScheme :: PPKScheme -> Type where SED25519 :: SPPKScheme 'ED25519 SETH :: SPPKScheme 'ETH instance Show (SPPKScheme a) where