Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

replace star by type #896

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
100 changes: 99 additions & 1 deletion src-tool/Pact/Analyze/Feature.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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')
Expand Down
3 changes: 1 addition & 2 deletions src-tool/Pact/Analyze/Parse/Prop.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 1 addition & 2 deletions src-tool/Pact/Analyze/Parse/Types.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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@.
Expand Down
3 changes: 1 addition & 2 deletions src-tool/Pact/Analyze/Translate.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
12 changes: 6 additions & 6 deletions src-tool/Pact/Analyze/Types/Eval.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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

Expand All @@ -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)
Expand Down Expand Up @@ -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))

Expand Down
12 changes: 6 additions & 6 deletions src-tool/Pact/Analyze/Types/Languages.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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
Expand All @@ -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'
Expand All @@ -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''
Expand All @@ -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.
Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src-tool/Pact/Analyze/Types/Numerical.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
3 changes: 2 additions & 1 deletion src-tool/Pact/Analyze/Types/ObjUtil.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -105,7 +106,7 @@ filterV
(flag :: Flag)
(p :: Symbol)
(xs :: [ (Symbol, Ty) ])
(f :: Ty -> *).
(f :: Ty -> Type).
Sing flag
-> Sing p
-> HList f xs
Expand Down
3 changes: 1 addition & 2 deletions src-tool/Pact/Analyze/Types/Shared.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 2 additions & 1 deletion src/Pact/Types/Scheme.hs
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ module Pact.Types.Scheme

import GHC.Generics
import Control.DeepSeq
import Data.Kind
import Data.Serialize
import Data.Aeson

Expand Down Expand Up @@ -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
Expand Down