Skip to content

Commit

Permalink
Comments
Browse files Browse the repository at this point in the history
  • Loading branch information
michaelpj committed Sep 22, 2023
1 parent 00d1718 commit dded1b8
Show file tree
Hide file tree
Showing 6 changed files with 45 additions and 29 deletions.
20 changes: 10 additions & 10 deletions plutus-core/plutus-core/src/PlutusCore/Core/Type.hs
Original file line number Diff line number Diff line change
Expand Up @@ -22,9 +22,9 @@ module PlutusCore.Core.Type
, fromPatFuncKind
, argsFunKind
, Type (..)
, funTySections
, splitFunTyParts
, funTyArgs
, funResultType
, funTyResultType
, Term (..)
, Program (..)
, HasTermLevel
Expand Down Expand Up @@ -110,24 +110,24 @@ data Type tyname uni ann
deriving anyclass (NFData)

-- | Get recursively all the domains and codomains of a type.
-- @funTySections (A->B->C) = [A, B, C]@
-- @funTySections (X) = [X]@
funTySections :: Type tyname uni a -> NE.NonEmpty (Type tyname uni a)
funTySections = \case
TyFun _ t1 t2 -> t1 NE.<| funTySections t2
-- @splitFunTyParts (A->B->C) = [A, B, C]@
-- @splitFunTyParts (X) = [X]@
splitFunTyParts :: Type tyname uni a -> NE.NonEmpty (Type tyname uni a)
splitFunTyParts = \case
TyFun _ t1 t2 -> t1 NE.<| splitFunTyParts t2
t -> pure t

-- | Get the argument types of a function type.
-- @funTyArgs (A->B->C) = [A, B]@
funTyArgs :: Type tyname uni a -> [Type tyname uni a]
funTyArgs = NE.init . funTySections
funTyArgs = NE.init . splitFunTyParts

-- | Get the result type of a function.
-- If not a function, then is the same as `id`
-- @funResultType (A->B->C) = C@
-- @funResultType (X) = X@
funResultType :: Type tyname uni a -> Type tyname uni a
funResultType = NE.last . funTySections
funTyResultType :: Type tyname uni a -> Type tyname uni a
funTyResultType = NE.last . splitFunTyParts

data Term tyname name uni fun ann
= Var ann name -- ^ a named variable
Expand Down
1 change: 1 addition & 0 deletions plutus-core/plutus-ir/src/PlutusIR/Analysis/Builtins.hs
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ import PlutusCore.Builtin
import PlutusCore.Builtin qualified as PLC
import PlutusPrelude (Default (..))

-- | All non-static information about builtins that the compiler might want.
data BuiltinsInfo (uni :: Type -> Type) fun = BuiltinsInfo
{ _biSemanticsVariant :: PLC.BuiltinSemanticsVariant fun
}
Expand Down
35 changes: 24 additions & 11 deletions plutus-core/plutus-ir/src/PlutusIR/Analysis/VarInfo.hs
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ import PlutusCore.Name qualified as PLC
import PlutusIR.Core
import Prettyprinter

-- | Information about variables and type variables in the program.
data VarsInfo tyname name = VarsInfo
{ termVarInfoMap :: PLC.UniqueMap PLC.TermUnique (VarInfo tyname name)
, typeVarInfoMap :: PLC.UniqueMap PLC.TypeUnique (TyVarInfo tyname name)
Expand All @@ -20,28 +21,40 @@ instance Semigroup (VarsInfo tyname name) where
instance Monoid (VarsInfo tyname name) where
mempty = VarsInfo mempty mempty

-- | Lookup the 'VarInfo' for a 'name'.
lookupVarInfo ::
(PLC.HasUnique name PLC.TermUnique)
=> name
-> VarsInfo tyname name
-> Maybe (VarInfo tyname name)
lookupVarInfo name (VarsInfo vim _) = PLC.lookupName name vim

-- | Lookup the 'TyVarInfo' for a 'tyname'.
lookupTyVarInfo ::
(PLC.HasUnique tyname PLC.TypeUnique)
=> tyname
-> VarsInfo tyname name
-> Maybe (TyVarInfo tyname name)
lookupTyVarInfo name (VarsInfo _ vim) = PLC.lookupName name vim

-- | Information about a type variable in the program.
data TyVarInfo tyname name =
NormalTyVar {}
| DatatypeTyVar { dtNumTyVars :: Int, dtConstructors :: [name] }
-- | A normal type variable, which could be anything.
NormalTyVar
-- | A type variable corresponding to a datatype.
-- Tells us the number of type variables and the constructors.
| DatatypeTyVar Int [name]

data VarInfo tyname name =
NormalVar { varStrictness :: Strictness, varArity :: Maybe Arity }
| DatatypeConstructor { dcArity :: Arity , dcParentTyname :: tyname }
| DatatypeMatcher { dmArity :: Arity , dmParentTyname :: tyname }
-- | A normal term variable, which could be anything.
-- Tells us if it is strictly evaluated, and possibly its arity.
NormalVar Strictness (Maybe Arity)
-- | A term variable corresponding to a datatype constructor.
-- Tells us the arity and the name of the datatype that owns it.
| DatatypeConstructor Arity tyname
-- | A term variable corresponding to a datatype matcher.
-- Tells us the arity and the name of the datatype that owns it.
| DatatypeMatcher Arity tyname

-- | Is the next argument a term or a type?
data Param =
Expand All @@ -67,15 +80,15 @@ type Arity = [Param]

varInfoStrictness :: VarInfo tyname name -> Strictness
varInfoStrictness = \case
NormalVar { varStrictness } -> varStrictness
DatatypeConstructor{} -> Strict
DatatypeMatcher{} -> Strict
NormalVar s _ -> s
DatatypeConstructor{} -> Strict
DatatypeMatcher{} -> Strict

varInfoArity :: VarInfo tyname name -> Maybe Arity
varInfoArity = \case
NormalVar { varArity } -> varArity
DatatypeConstructor { dcArity } -> Just dcArity
DatatypeMatcher { dmArity} -> Just dmArity
NormalVar _ a -> a
DatatypeConstructor a _ -> Just a
DatatypeMatcher a _ -> Just a

termVarInfo ::
(PLC.HasUnique name PLC.TermUnique
Expand Down
4 changes: 3 additions & 1 deletion plutus-core/plutus-ir/src/PlutusIR/Purity.hs
Original file line number Diff line number Diff line change
Expand Up @@ -152,11 +152,13 @@ termEvaluationOrder binfo vinfo = goTerm
-- reduce; if fully-applied they are pure; if over-applied it's going to be
-- a type error since they never return a function. So we can ignore the arity
-- in this case!
(splitApplication -> (h@(Var _ n), args))
t@(splitApplication -> (h@(Var _ n), args))
| Just (DatatypeConstructor{}) <- lookupVarInfo n vinfo ->
evalThis (EvalTerm Pure MaybeWork h)
<>
goAppCtx args
<>
evalThis (EvalTerm Pure MaybeWork t)
-- No Unknown: we go to a known pure place, but we can't show it,
-- so we just skip it here. This has the effect of making constructor
-- applications pure
Expand Down
12 changes: 6 additions & 6 deletions plutus-core/plutus-ir/src/PlutusIR/Transform/KnownCon.hs
Original file line number Diff line number Diff line change
Expand Up @@ -58,26 +58,26 @@ processTerm ::
Term tyname name uni fun a
processTerm vinfo t
| (Var _ n, args) <- splitApplication t
, Just (DatatypeMatcher { dmParentTyname }) <- lookupVarInfo n vinfo
, Just (DatatypeTyVar { dtNumTyVars, dtConstructors }) <- lookupTyVarInfo dmParentTyname vinfo
, Just (DatatypeMatcher _ parentName) <- lookupVarInfo n vinfo
, Just (DatatypeTyVar numTyVars constructors ) <- lookupTyVarInfo parentName vinfo
, (TermAppContext scrut _ (TypeAppContext _resTy _ branchArgs)) <-
-- The datatype may have some type arguments, we
-- aren't interested in them, so we drop them.
dropAppContext dtNumTyVars args
dropAppContext numTyVars args
, -- The scrutinee is itself an application
(Var _ con, conArgs) <- splitApplication scrut
, -- ... of one of the constructors from the same datatype as the destructor
Just i <- List.findIndex (== con) dtConstructors
Just i <- List.findIndex (== con) constructors
, -- ... and there is a branch for that constructor in the destructor application
(TermAppContext branch _ _) <- dropAppContext i branchArgs
, -- This condition ensures the destructor is fully-applied
-- (which should always be the case in programs that come from Plutus Tx,
-- but not necessarily in arbitrary PIR programs).
lengthContext branchArgs == length dtConstructors =
lengthContext branchArgs == length constructors =
fillAppContext
branch
-- The arguments to the selected branch consists of the arguments
-- to the constructor, without the leading type arguments - e.g.,
-- if the scrutinee is `Just {integer} 1`, we only need the `1`).
(dropAppContext dtNumTyVars conArgs)
(dropAppContext numTyVars conArgs)
| otherwise = t
2 changes: 1 addition & 1 deletion plutus-core/plutus-ir/src/PlutusIR/TypeCheck/Internal.hs
Original file line number Diff line number Diff line change
Expand Up @@ -405,7 +405,7 @@ checkTypeFromBinding recurs = \case
checkConRes ty =
-- We earlier checked that datacons' type is *-kinded (using checkKindBinding), but this is not enough:
-- we must also check that its result type is EXACTLY `[[TypeCon tyarg1] ... tyargn]` (ignoring annotations)
when (void (PLC.funResultType ty) /= void appliedTyCon) .
when (void (PLC.funTyResultType ty) /= void appliedTyCon) .
throwing _TypeErrorExt $ MalformedDataConstrResType ann appliedTyCon

-- if nonrec binding, make sure that type-constructor is not part of the data-constructor's argument types.
Expand Down

0 comments on commit dded1b8

Please sign in to comment.