mirror of
https://github.com/digital-asset/daml.git
synced 2024-09-20 01:07:18 +03:00
DAML-LF add Type Representation value (#3326)
* daml-lf: update spec with type-rep * daml-lf: update proto with type-rep * daml-lf: update scala side with TypeRep * daml-lf: update compiler side with TypeRep * Get triggers to compile * Add featureTypeRep to allFeatures * Apply suggestions from code review Co-Authored-By: Moritz Kiefer <moritz.kiefer@purelyfunctional.org> * daml-lf: add builtin for TypeRep equality * Address Andrea's comments * formatting * Fix triggers * Fix template typerep tests
This commit is contained in:
parent
edb2d15cec
commit
7c427119e1
@ -155,6 +155,7 @@ data BuiltinType
|
||||
| BTMap
|
||||
| BTArrow
|
||||
| BTAny
|
||||
| BTTypeRep
|
||||
deriving (Eq, Data, Generic, NFData, Ord, Show)
|
||||
|
||||
-- | Type as used in typed binders.
|
||||
@ -448,7 +449,7 @@ data Expr
|
||||
{ fromAnyType :: !Type
|
||||
, fromAnyBody :: !Expr
|
||||
}
|
||||
| EToTextTypeConName !(Qualified TypeConName)
|
||||
| ETypeRep !Type
|
||||
-- | Update expression.
|
||||
| EUpdate !Update
|
||||
-- | Scenario expression.
|
||||
|
@ -135,6 +135,7 @@ instance Pretty BuiltinType where
|
||||
BTMap -> "Map"
|
||||
BTArrow -> "(->)"
|
||||
BTAny -> "Any"
|
||||
BTTypeRep -> "TypeRep"
|
||||
|
||||
prettyRecord :: (Pretty a) =>
|
||||
PrettyLevel -> Doc ann -> [(FieldName, a)] -> Doc ann
|
||||
@ -449,7 +450,7 @@ instance Pretty Expr where
|
||||
ENone typ -> prettyAppKeyword lvl prec "none" [TyArg typ]
|
||||
EToAny ty body -> prettyAppKeyword lvl prec "to_any" [TyArg ty, TmArg body]
|
||||
EFromAny ty body -> prettyAppKeyword lvl prec "from_any" [TyArg ty, TmArg body]
|
||||
EToTextTypeConName tycon -> prettyAppKeyword lvl prec "to_text_type_con_name" [tplArg tycon]
|
||||
ETypeRep ty -> prettyAppKeyword lvl prec "type_rep" [TyArg ty]
|
||||
|
||||
instance Pretty DefDataType where
|
||||
pPrintPrec lvl _prec (DefDataType mbLoc tcon (IsSerializable serializable) params dataCons) =
|
||||
|
@ -45,7 +45,7 @@ data ExprF expr
|
||||
| ESomeF !Type !expr
|
||||
| EToAnyF !Type !expr
|
||||
| EFromAnyF !Type !expr
|
||||
| EToTextTypeConNameF !(Qualified TypeConName)
|
||||
| ETypeRepF !Type
|
||||
deriving (Foldable, Functor, Traversable)
|
||||
|
||||
data BindingF expr = BindingF !(ExprVarName, Type) !expr
|
||||
@ -177,7 +177,7 @@ instance Recursive Expr where
|
||||
ESome a b -> ESomeF a b
|
||||
EToAny a b -> EToAnyF a b
|
||||
EFromAny a b -> EFromAnyF a b
|
||||
EToTextTypeConName a -> EToTextTypeConNameF a
|
||||
ETypeRep a -> ETypeRepF a
|
||||
|
||||
instance Corecursive Expr where
|
||||
embed = \case
|
||||
@ -207,4 +207,4 @@ instance Corecursive Expr where
|
||||
ESomeF a b -> ESome a b
|
||||
EToAnyF a b -> EToAny a b
|
||||
EFromAnyF a b -> EFromAny a b
|
||||
EToTextTypeConNameF a -> EToTextTypeConName a
|
||||
ETypeRepF a -> ETypeRep a
|
||||
|
@ -154,7 +154,7 @@ infixr 1 :->
|
||||
pattern (:->) :: Type -> Type -> Type
|
||||
pattern a :-> b = TArrow `TApp` a `TApp` b
|
||||
|
||||
pattern TUnit, TBool, TInt64, TDecimal, TText, TTimestamp, TParty, TDate, TArrow, TNumeric10, TAny, TNat10 :: Type
|
||||
pattern TUnit, TBool, TInt64, TDecimal, TText, TTimestamp, TParty, TDate, TArrow, TNumeric10, TAny, TNat10, TTypeRep :: Type
|
||||
pattern TUnit = TBuiltin BTUnit
|
||||
pattern TBool = TBuiltin BTBool
|
||||
pattern TInt64 = TBuiltin BTInt64
|
||||
@ -167,6 +167,7 @@ pattern TParty = TBuiltin BTParty
|
||||
pattern TDate = TBuiltin BTDate
|
||||
pattern TArrow = TBuiltin BTArrow
|
||||
pattern TAny = TBuiltin BTAny
|
||||
pattern TTypeRep = TBuiltin BTTypeRep
|
||||
|
||||
pattern TList, TOptional, TMap, TUpdate, TScenario, TContractId, TNumeric :: Type -> Type
|
||||
pattern TList typ = TApp (TBuiltin BTList) typ
|
||||
|
@ -67,11 +67,11 @@ featureAnyType = Feature
|
||||
, featureCppFlag = "DAML_ANY_TYPE"
|
||||
}
|
||||
|
||||
featureTemplateTypeRep :: Feature
|
||||
featureTemplateTypeRep = Feature
|
||||
{ featureName = "templateTypeRep builtin"
|
||||
featureTypeRep :: Feature
|
||||
featureTypeRep = Feature
|
||||
{ featureName = "TypeRep type"
|
||||
, featureMinVersion = versionDev
|
||||
, featureCppFlag = "DAML_TEMPLATE_TYPE_REP"
|
||||
, featureCppFlag = "DAML_TYPE_REP"
|
||||
}
|
||||
|
||||
featureStringInterning :: Feature
|
||||
@ -85,6 +85,7 @@ allFeatures :: [Feature]
|
||||
allFeatures =
|
||||
[ featureNumeric
|
||||
, featureAnyType
|
||||
, featureTypeRep
|
||||
, featureStringInterning
|
||||
]
|
||||
|
||||
|
@ -298,6 +298,7 @@ decodeBuiltinFunction = pure . \case
|
||||
LF1.BuiltinFunctionEQUAL_DATE -> BEEqual BTDate
|
||||
LF1.BuiltinFunctionEQUAL_PARTY -> BEEqual BTParty
|
||||
LF1.BuiltinFunctionEQUAL_BOOL -> BEEqual BTBool
|
||||
LF1.BuiltinFunctionEQUAL_TYPE_REP -> BEEqual BTTypeRep
|
||||
|
||||
LF1.BuiltinFunctionLEQ_INT64 -> BELessEq BTInt64
|
||||
LF1.BuiltinFunctionLEQ_DECIMAL -> BELessEq BTDecimal
|
||||
@ -506,9 +507,8 @@ decodeExprSum exprSum = mayDecode "exprSum" exprSum $ \case
|
||||
type' <- mayDecode "expr_FromAnyType" mbType decodeType
|
||||
expr <- mayDecode "expr_FromAnyExpr" mbExpr decodeExpr
|
||||
return (EFromAny type' expr)
|
||||
LF1.ExprSumToTextTypeConName tycon -> do
|
||||
con <- decodeTypeConName tycon
|
||||
return (EToTextTypeConName con)
|
||||
LF1.ExprSumTypeRep typ ->
|
||||
ETypeRep <$> decodeType typ
|
||||
|
||||
decodeUpdate :: LF1.Update -> Decode Expr
|
||||
decodeUpdate LF1.Update{..} = mayDecode "updateSum" updateSum $ \case
|
||||
@ -678,6 +678,7 @@ decodePrim = pure . \case
|
||||
LF1.PrimTypeMAP -> BTMap
|
||||
LF1.PrimTypeARROW -> BTArrow
|
||||
LF1.PrimTypeANY -> BTAny
|
||||
LF1.PrimTypeTYPE_REP -> BTTypeRep
|
||||
|
||||
decodeTypeLevelNat :: Integer -> Decode TypeLevelNat
|
||||
decodeTypeLevelNat m =
|
||||
|
@ -276,6 +276,7 @@ encodeBuiltinType = P.Enumerated . Right . \case
|
||||
BTArrow -> P.PrimTypeARROW
|
||||
BTNumeric -> P.PrimTypeNUMERIC
|
||||
BTAny -> P.PrimTypeANY
|
||||
BTTypeRep -> P.PrimTypeTYPE_REP
|
||||
|
||||
encodeType' :: Type -> Encode P.Type
|
||||
encodeType' typ = fmap (P.Type . Just) $ case typ ^. _TApps of
|
||||
@ -354,6 +355,7 @@ encodeBuiltinExpr = \case
|
||||
BTDate -> builtin P.BuiltinFunctionEQUAL_DATE
|
||||
BTParty -> builtin P.BuiltinFunctionEQUAL_PARTY
|
||||
BTBool -> builtin P.BuiltinFunctionEQUAL_BOOL
|
||||
BTTypeRep -> builtin P.BuiltinFunctionEQUAL_TYPE_REP
|
||||
other -> error $ "BEEqual unexpected type " <> show other
|
||||
|
||||
BELessEq typ -> case typ of
|
||||
@ -579,8 +581,8 @@ encodeExpr' = \case
|
||||
expr_FromAnyType <- encodeType ty
|
||||
expr_FromAnyExpr <- encodeExpr body
|
||||
pureExpr $ P.ExprSumFromAny P.Expr_FromAny{..}
|
||||
EToTextTypeConName tycon -> do
|
||||
expr . P.ExprSumToTextTypeConName <$> encodeQualTypeConName' tycon
|
||||
ETypeRep ty -> do
|
||||
expr . P.ExprSumTypeRep <$> encodeType' ty
|
||||
where
|
||||
expr = P.Expr Nothing . Just
|
||||
pureExpr = pure . expr
|
||||
|
@ -59,7 +59,7 @@ freeVarsStep = \case
|
||||
ESomeF _ s -> s
|
||||
EToAnyF _ s -> s
|
||||
EFromAnyF _ s -> s
|
||||
EToTextTypeConNameF _ -> mempty
|
||||
ETypeRepF _ -> mempty
|
||||
EUpdateF u ->
|
||||
case u of
|
||||
UPureF _ s -> s
|
||||
@ -217,7 +217,7 @@ safetyStep = \case
|
||||
EFromAnyF _ s
|
||||
| Safe _ <- s -> Safe 0
|
||||
| otherwise -> Unsafe
|
||||
EToTextTypeConNameF _ -> Safe 0
|
||||
ETypeRepF _ -> Safe 0
|
||||
|
||||
|
||||
infoStep :: ExprF Info -> Info
|
||||
|
@ -121,6 +121,7 @@ kindOfBuiltin = \case
|
||||
BTMap -> KStar `KArrow` KStar
|
||||
BTArrow -> KStar `KArrow` KStar `KArrow` KStar
|
||||
BTAny -> KStar
|
||||
BTTypeRep -> KStar
|
||||
|
||||
kindOf :: MonadGamma m => Type -> m Kind
|
||||
kindOf = \case
|
||||
@ -502,29 +503,33 @@ typeOf = \case
|
||||
ESome bodyType bodyExpr -> checkSome bodyType bodyExpr $> TOptional bodyType
|
||||
ENone bodyType -> checkType bodyType KStar $> TOptional bodyType
|
||||
EToAny ty bodyExpr -> do
|
||||
checkAnyType ty
|
||||
checkGroundType ty
|
||||
checkExpr bodyExpr ty
|
||||
pure $ TBuiltin BTAny
|
||||
EFromAny ty bodyExpr -> do
|
||||
checkAnyType ty
|
||||
checkGroundType ty
|
||||
checkExpr bodyExpr (TBuiltin BTAny)
|
||||
pure $ TOptional ty
|
||||
EToTextTypeConName tycon -> do
|
||||
-- Ensure that the type is known.
|
||||
_ <- inWorld (lookupDataType tycon)
|
||||
pure $ TBuiltin BTText
|
||||
ETypeRep ty -> do
|
||||
checkGroundType ty
|
||||
pure $ TBuiltin BTTypeRep
|
||||
EUpdate upd -> typeOfUpdate upd
|
||||
EScenario scen -> typeOfScenario scen
|
||||
ELocation _ expr -> typeOf expr
|
||||
|
||||
-- Check that the type contains no type variables or quantifiers
|
||||
checkAnyType :: MonadGamma m => Type -> m ()
|
||||
checkAnyType ty =
|
||||
checkGroundType' :: MonadGamma m => Type -> m ()
|
||||
checkGroundType' ty =
|
||||
when (para (\t children -> or (isForbidden t : children)) ty) $ throwWithContext $ EExpectedAnyType ty
|
||||
where isForbidden (TVar _) = True
|
||||
isForbidden (TForall _ _) = True
|
||||
isForbidden _ = False
|
||||
|
||||
checkGroundType :: MonadGamma m => Type -> m ()
|
||||
checkGroundType ty = do
|
||||
_ <- checkType ty KStar
|
||||
checkGroundType' ty
|
||||
|
||||
checkExpr' :: MonadGamma m => Expr -> Type -> m Type
|
||||
checkExpr' expr typ = do
|
||||
exprType <- typeOf expr
|
||||
|
@ -62,6 +62,7 @@ data UnserializabilityReason
|
||||
| URNumericOutOfRange !Natural
|
||||
| URTypeLevelNat
|
||||
| URAny -- ^ It contains a value of type Any.
|
||||
| URTypeRep -- ^ It contains a value of type TypeRep.
|
||||
|
||||
data Error
|
||||
= EUnknownTypeVar !TypeVarName
|
||||
@ -168,6 +169,7 @@ instance Pretty UnserializabilityReason where
|
||||
URNumericOutOfRange n -> "Numeric scale " <> integer (fromIntegral n) <> " is out of range (needs to be between 0 and 38)"
|
||||
URTypeLevelNat -> "type-level nat"
|
||||
URAny -> "Any"
|
||||
URTypeRep -> "TypeRep"
|
||||
|
||||
instance Pretty Error where
|
||||
pPrint = \case
|
||||
|
@ -98,6 +98,7 @@ serializabilityConditionsType world0 _version mbModNameTpls vars = go
|
||||
BTArrow -> Left URFunction
|
||||
BTNumeric -> Left URNumeric -- 'Numeric' is used as a higher-kinded type constructor.
|
||||
BTAny -> Left URAny
|
||||
BTTypeRep -> Left URTypeRep
|
||||
TForall{} -> Left URForall
|
||||
TTuple{} -> Left URTuple
|
||||
|
||||
|
@ -538,6 +538,8 @@ generateSrcFromLf (Qualify qualify) thisPkgId pkgMap m = noLoc mod
|
||||
LF.BTNumeric -> mkGhcType "Numeric"
|
||||
-- TODO see https://github.com/digital-asset/daml/issues/2876
|
||||
LF.BTAny -> error "Any type not yet supported in upgrades"
|
||||
LF.BTTypeRep -> error "TypeRep type not yet supported in upgrades"
|
||||
|
||||
mkGhcType =
|
||||
HsTyVar noExt NotPromoted .
|
||||
noLoc . mkOrig gHC_TYPES . mkOccName varName
|
||||
@ -646,6 +648,7 @@ generateSrcFromLf (Qualify qualify) thisPkgId pkgMap m = noLoc mod
|
||||
LF.BTNumeric -> (primUnitId, LF.ModuleName ["GHC", "Types"])
|
||||
-- TODO: see https://github.com/digital-asset/daml/issues/2876
|
||||
LF.BTAny -> error "Any type not yet supported in upgrades"
|
||||
LF.BTTypeRep -> error "TypeRep type not yet supported in upgrades"
|
||||
|
||||
translateModName ::
|
||||
forall a. NamedThing a
|
||||
|
@ -460,8 +460,8 @@ convertGenericTemplate env x
|
||||
resField = mkField "getTemplateTypeRep"
|
||||
in
|
||||
ETyLam (proxyName, KStar `KArrow` KStar) $!
|
||||
if envLfVersion env `supports` featureTemplateTypeRep
|
||||
then ETmLam (arg, argType) $ ERecCon resType [(resField, EToTextTypeConName monoTyCon)]
|
||||
if envLfVersion env `supports` featureTypeRep
|
||||
then ETmLam (arg, argType) $ ERecCon resType [(resField, ETypeRep (TCon monoTyCon))]
|
||||
else EBuiltin BEError `ETyApp` (argType :-> typeConAppToType resType) `ETmApp` EBuiltin (BEText "templateTypeRep is not supported in this DAML-LF version")
|
||||
tyArgs <- mapM (convertType env) tyArgs
|
||||
-- NOTE(MH): The additional lambda is DICTIONARY SANITIZATION step (3).
|
||||
@ -689,7 +689,7 @@ convertBind env (name, x)
|
||||
-- during conversion to DAML-LF together with their constructors since we
|
||||
-- deliberately remove 'GHC.Types.Opaque' as well.
|
||||
internalTypes :: UniqSet FastString
|
||||
internalTypes = mkUniqSet ["Scenario","Update","ContractId","Time","Date","Party","Pair", "TextMap", "Any"]
|
||||
internalTypes = mkUniqSet ["Scenario","Update","ContractId","Time","Date","Party","Pair", "TextMap", "Any", "TypeRep"]
|
||||
|
||||
internalFunctions :: UniqFM (UniqSet FastString)
|
||||
internalFunctions = listToUFM $ map (bimap mkModuleNameFS mkUniqSet)
|
||||
@ -1375,6 +1375,13 @@ convertTyCon env t
|
||||
pure $ if envLfVersion env `supports` featureAnyType
|
||||
then TAny
|
||||
else TUnit
|
||||
"TypeRep" ->
|
||||
-- We just translate this to TUnit when it is not supported.
|
||||
-- We can’t get rid of it completely since the template desugaring uses
|
||||
-- this and we do not want to make that dependent on the DAML-LF version.
|
||||
pure $ if envLfVersion env `supports` featureTypeRep
|
||||
then TTypeRep
|
||||
else TUnit
|
||||
_ -> defaultTyCon
|
||||
| isBuiltinName "Optional" t = pure (TBuiltin BTOptional)
|
||||
| otherwise = defaultTyCon
|
||||
|
@ -1,6 +1,7 @@
|
||||
-- Copyright (c) 2019 The DAML Authors. All rights reserved.
|
||||
-- SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
{-# LANGUAGE CPP #-}
|
||||
{-# LANGUAGE NoImplicitPrelude #-}
|
||||
{-# OPTIONS -Wno-unused-binds #-} -- the opaque constructors are not exported
|
||||
|
||||
@ -41,8 +42,6 @@ module DA.Internal.LF
|
||||
, AnyChoice
|
||||
|
||||
, TemplateTypeRep
|
||||
, templateTypeRepToText
|
||||
, templateTypeRepFromText
|
||||
) where
|
||||
|
||||
import GHC.Types (Opaque, Symbol)
|
||||
@ -221,12 +220,17 @@ newtype AnyTemplate = AnyTemplate { getAnyTemplate : Any }
|
||||
-- | Existential choice type that can wrap an arbitrary chice.
|
||||
newtype AnyChoice = AnyChoice { getAnyChoice : Any }
|
||||
|
||||
-- | Value-level representation of a type.
|
||||
-- We do not expose this directly and instead only expose TemplateTypeRep.
|
||||
data TypeRep = TypeRep Opaque
|
||||
|
||||
-- | Unique textual representation of a template Id.
|
||||
newtype TemplateTypeRep = TemplateTypeRep { getTemplateTypeRep : Text }
|
||||
deriving (Eq, Ord, Show)
|
||||
newtype TemplateTypeRep = TemplateTypeRep { getTemplateTypeRep : TypeRep }
|
||||
deriving Eq
|
||||
|
||||
templateTypeRepToText : TemplateTypeRep -> Text
|
||||
templateTypeRepToText = getTemplateTypeRep
|
||||
|
||||
templateTypeRepFromText : Text -> Optional TemplateTypeRep
|
||||
templateTypeRepFromText = Some . TemplateTypeRep
|
||||
instance Eq TypeRep where
|
||||
#ifdef DAML_TYPE_REP
|
||||
(==) = primitive @"BEEqual"
|
||||
#else
|
||||
(==) = error "TYPE_REP not supported in this version of DAML-LF"
|
||||
#endif
|
||||
|
@ -60,10 +60,6 @@ instance MapKey Party where
|
||||
keyToText = partyToText
|
||||
keyFromText = fromSome . partyFromText
|
||||
|
||||
instance MapKey TemplateTypeRep where
|
||||
keyToText = templateTypeRepToText
|
||||
keyFromText = fromSome . templateTypeRepFromText
|
||||
|
||||
instance MapKey Int where
|
||||
keyToText = show
|
||||
keyFromText = fromSome . parseInt
|
||||
|
@ -4,7 +4,7 @@
|
||||
-- @SINCE-LF 1.dev
|
||||
daml 1.2 module TemplateTypeRep where
|
||||
|
||||
import DA.Assert
|
||||
import DA.Action
|
||||
import qualified TemplateTypeRep2
|
||||
|
||||
template T1
|
||||
@ -31,12 +31,21 @@ template Template t => GenericT t
|
||||
template instance GT1 = GenericT T1
|
||||
template instance GT2 = GenericT T2
|
||||
|
||||
main = scenario do
|
||||
templateTypeRep @T1 === templateTypeRep @T1
|
||||
templateTypeRep @T2 === templateTypeRep @T2
|
||||
templateTypeRep @GT1 === templateTypeRep @GT1
|
||||
templateTypeRep @GT2 === templateTypeRep @GT2
|
||||
assertTypeRepEq : CanAbort m => TemplateTypeRep -> TemplateTypeRep -> m ()
|
||||
assertTypeRepEq a b =
|
||||
unless (a == b) $ abort "TypeReps are not equal"
|
||||
|
||||
templateTypeRep @T1 =/= templateTypeRep @T2
|
||||
templateTypeRep @GT1 =/= templateTypeRep @GT2
|
||||
templateTypeRep @T1 =/= templateTypeRep @TemplateTypeRep2.T1
|
||||
assertTypeRepNeq : CanAbort m => TemplateTypeRep -> TemplateTypeRep -> m ()
|
||||
assertTypeRepNeq a b =
|
||||
unless (a /= b) $ abort "TypeReps are equal"
|
||||
|
||||
|
||||
main = scenario do
|
||||
assertTypeRepEq (templateTypeRep @T1) (templateTypeRep @T1)
|
||||
assertTypeRepEq (templateTypeRep @T2) (templateTypeRep @T2)
|
||||
assertTypeRepEq (templateTypeRep @GT1) (templateTypeRep @GT1)
|
||||
assertTypeRepEq (templateTypeRep @GT2) (templateTypeRep @GT2)
|
||||
|
||||
assertTypeRepNeq (templateTypeRep @T1) (templateTypeRep @T2)
|
||||
assertTypeRepNeq (templateTypeRep @GT1) (templateTypeRep @GT2)
|
||||
assertTypeRepNeq (templateTypeRep @T1) (templateTypeRep @TemplateTypeRep2.T1)
|
||||
|
@ -274,6 +274,10 @@ enum PrimType {
|
||||
// Builtin type 'Any'
|
||||
// *Available in versions >= 1.dev*
|
||||
ANY = 18;
|
||||
|
||||
// Builtin type 'TypeRep'
|
||||
// *Available in versions >= 1.dev*
|
||||
TYPE_REP = 19;
|
||||
}
|
||||
|
||||
// Types
|
||||
@ -483,6 +487,8 @@ enum BuiltinFunction {
|
||||
EQUAL_BOOL = 85;
|
||||
EQUAL_CONTRACT_ID = 86;
|
||||
EQUAL_LIST = 87;
|
||||
EQUAL_TYPE_REP = 123;
|
||||
|
||||
|
||||
TRACE = 88;
|
||||
|
||||
@ -490,7 +496,7 @@ enum BuiltinFunction {
|
||||
|
||||
TEXT_FROM_CODE_POINTS = 105; // *Available in versions >= 1.6*
|
||||
TEXT_TO_CODE_POINTS = 106; // *Available in versions >= 1.6*
|
||||
// Next id is 123. 122 is SHIFT_NUMERIC.
|
||||
// Next id is 124. 123 is EQUAL_TYPE_REP.
|
||||
}
|
||||
|
||||
// Builtin literals
|
||||
@ -878,9 +884,9 @@ message Expr {
|
||||
// *Available in versions >= 1.dev*
|
||||
FromAny from_any = 31;
|
||||
|
||||
// Obtain a unique textual representation of a type constructor
|
||||
// A type representation
|
||||
// *Available in versions >= 1.dev*
|
||||
TypeConName to_text_type_con_name = 32;
|
||||
Type type_rep = 32;
|
||||
}
|
||||
|
||||
reserved 19; // This was equals. Removed in favour of BuiltinFunction.EQUAL_*
|
||||
|
@ -842,9 +842,9 @@ private[archive] class DecodeV1(minor: LV.Minor) extends Decode.OfPackage[PLF.Pa
|
||||
decodeType(lfExpr.getFromAny.getType),
|
||||
decodeExpr(lfExpr.getFromAny.getExpr, definition))
|
||||
|
||||
case PLF.Expr.SumCase.TO_TEXT_TYPE_CON_NAME =>
|
||||
assertSince(LV.Features.toTextTypeConName, "Expr.ToTextTypeConName")
|
||||
EToTextTypeConName(decodeTypeConName(lfExpr.getToTextTypeConName))
|
||||
case PLF.Expr.SumCase.TYPE_REP =>
|
||||
assertSince(LV.Features.typeRep, "Expr.type_rep")
|
||||
ETypeRep(decodeType(lfExpr.getTypeRep))
|
||||
|
||||
case PLF.Expr.SumCase.SUM_NOT_SET =>
|
||||
throw ParseError("Expr.SUM_NOT_SET")
|
||||
@ -1223,7 +1223,8 @@ private[lf] object DecodeV1 {
|
||||
BuiltinTypeInfo(MAP, BTMap, minVersion = optional),
|
||||
BuiltinTypeInfo(ARROW, BTArrow, minVersion = arrowType),
|
||||
BuiltinTypeInfo(NUMERIC, BTNumeric, minVersion = numeric),
|
||||
BuiltinTypeInfo(ANY, BTAny, minVersion = anyType)
|
||||
BuiltinTypeInfo(ANY, BTAny, minVersion = anyType),
|
||||
BuiltinTypeInfo(TYPE_REP, BTTypeRep, minVersion = typeRep)
|
||||
)
|
||||
}
|
||||
|
||||
@ -1404,6 +1405,7 @@ private[lf] object DecodeV1 {
|
||||
BuiltinFunctionInfo(EQUAL_BOOL, BEqualBool),
|
||||
BuiltinFunctionInfo(EQUAL_LIST, BEqualList),
|
||||
BuiltinFunctionInfo(EQUAL_CONTRACT_ID, BEqualContractId),
|
||||
BuiltinFunctionInfo(EQUAL_TYPE_REP, BEqualTypeRep),
|
||||
BuiltinFunctionInfo(TRACE, BTrace),
|
||||
BuiltinFunctionInfo(COERCE_CONTRACT_ID, BCoerceContractId, minVersion = coerceContractId)
|
||||
)
|
||||
|
@ -141,23 +141,7 @@ object Ref {
|
||||
|
||||
/* A fully-qualified identifier pointing to a definition in the
|
||||
* specified package. */
|
||||
case class Identifier(packageId: PackageId, qualifiedName: QualifiedName) {
|
||||
override def toString: String = packageId.toString + ":" + qualifiedName.toString
|
||||
}
|
||||
object Identifier {
|
||||
type T = Identifier
|
||||
|
||||
def fromString(s: String): Either[String, Identifier] = {
|
||||
val segments = split(s, ':')
|
||||
if (segments.length != 3)
|
||||
Left(s"Expecting three segments in $s, but got ${segments.length}")
|
||||
else
|
||||
for {
|
||||
packageId <- PackageId.fromString(segments(0))
|
||||
qualifiedName <- QualifiedName.fromString(segments(1) + ":" + segments(2))
|
||||
} yield Identifier(packageId, qualifiedName)
|
||||
}
|
||||
}
|
||||
case class Identifier(packageId: PackageId, qualifiedName: QualifiedName)
|
||||
|
||||
/* Choice name in a template. */
|
||||
val ChoiceName: Name.type = Name
|
||||
|
@ -240,7 +240,7 @@ object InterfaceReader {
|
||||
unserializableDataType(
|
||||
ctx,
|
||||
s"Unserializable primitive type: $a must be applied to one and only one TNat")
|
||||
case Ast.BTUpdate | Ast.BTScenario | Ast.BTArrow | Ast.BTAny =>
|
||||
case Ast.BTUpdate | Ast.BTScenario | Ast.BTArrow | Ast.BTAny | Ast.BTTypeRep =>
|
||||
unserializableDataType(ctx, s"Unserializable primitive type: $a")
|
||||
}
|
||||
(arity, primType) = ab
|
||||
|
@ -71,6 +71,7 @@ class TypeSpec extends WordSpec with Matchers {
|
||||
case Pkg.BTOptional => TypePrim(PrimTypeOptional, ImmArraySeq(assertOneArg(args)))
|
||||
case Pkg.BTArrow => sys.error("cannot use arrow in interface type")
|
||||
case Pkg.BTAny => sys.error("cannot use any in interface type")
|
||||
case Pkg.BTTypeRep => sys.error("cannot use type representation in interface type")
|
||||
}
|
||||
case Pkg.TTyCon(tycon) => TypeCon(TypeConName(tycon), args.toImmArray.toSeq)
|
||||
case Pkg.TNat(_) => sys.error("cannot use nat type in interface type")
|
||||
|
@ -296,6 +296,7 @@ final case class Compiler(packages: PackageId PartialFunction Package) {
|
||||
case BEqualParty => SBEqual
|
||||
case BEqualBool => SBEqual
|
||||
case BEqualContractId => SBEqual
|
||||
case BEqualTypeRep => SBEqual
|
||||
|
||||
// Map
|
||||
|
||||
@ -598,8 +599,8 @@ final case class Compiler(packages: PackageId PartialFunction Package) {
|
||||
case EFromAny(ty, e) =>
|
||||
SEApp(SEBuiltin(SBFromAny(ty)), Array(translate(e)))
|
||||
|
||||
case EToTextTypeConName(tyCon) =>
|
||||
SEValue(SText(tyCon.toString))
|
||||
case ETypeRep(typ) =>
|
||||
SEValue(STypeRep(typ))
|
||||
}
|
||||
|
||||
@tailrec
|
||||
@ -1038,7 +1039,7 @@ final case class Compiler(packages: PackageId PartialFunction Package) {
|
||||
|
||||
def goV(v: SValue): Unit = {
|
||||
v match {
|
||||
case _: SPrimLit | STNat(_) =>
|
||||
case _: SPrimLit | STNat(_) | STypeRep(_) =>
|
||||
case SList(a) => a.iterator.foreach(goV)
|
||||
case SOptional(x) => x.foreach(goV)
|
||||
case SMap(map) => map.values.foreach(goV)
|
||||
|
@ -295,7 +295,7 @@ object SBuiltin {
|
||||
case SParty(p) => p
|
||||
case SUnit => s"<unit>"
|
||||
case SDate(date) => date.toString
|
||||
case SContractId(_) | SNumeric(_) => crash("litToText: literal not supported")
|
||||
case SContractId(_) | SNumeric(_) | STypeRep(_) => crash("litToText: literal not supported")
|
||||
})
|
||||
}
|
||||
}
|
||||
|
@ -68,6 +68,8 @@ sealed trait SValue {
|
||||
V.ValueContractId(coid)
|
||||
case SAny(_, _) =>
|
||||
throw SErrorCrash("SValue.toValue: unexpected SAny")
|
||||
case STypeRep(_) =>
|
||||
throw SErrorCrash("SValue.toValue: unexpected STypeRep")
|
||||
case STNat(_) =>
|
||||
throw SErrorCrash("SValue.toValue: unexpected STNat")
|
||||
case _: SPAP =>
|
||||
@ -78,6 +80,8 @@ sealed trait SValue {
|
||||
|
||||
def mapContractId(f: V.ContractId => V.ContractId): SValue =
|
||||
this match {
|
||||
case SContractId(coid) => SContractId(f(coid))
|
||||
case SEnum(_, _) | _: SPrimLit | SToken | STNat(_) | STypeRep(_) => this
|
||||
case SPAP(prim, args, arity) =>
|
||||
val prim2 = prim match {
|
||||
case PClosure(expr, vars) =>
|
||||
@ -98,9 +102,6 @@ sealed trait SValue {
|
||||
SOptional(mbV.map(_.mapContractId(f)))
|
||||
case SMap(value) =>
|
||||
SMap(value.transform((_, v) => v.mapContractId(f)))
|
||||
case SContractId(coid) =>
|
||||
SContractId(f(coid))
|
||||
case SEnum(_, _) | _: SPrimLit | SToken | STNat(_) => this
|
||||
case SAny(ty, value) =>
|
||||
SAny(ty, value.mapContractId(f))
|
||||
}
|
||||
@ -194,6 +195,7 @@ object SValue {
|
||||
final case object SUnit extends SPrimLit
|
||||
final case class SDate(value: Time.Date) extends SPrimLit
|
||||
final case class SContractId(value: V.ContractId) extends SPrimLit
|
||||
final case class STypeRep(ty: Type) extends SPrimLit
|
||||
// The "effect" token for update or scenario builtin functions.
|
||||
final case object SToken extends SValue
|
||||
|
||||
|
@ -508,8 +508,8 @@ object Speedy {
|
||||
}
|
||||
}
|
||||
case SContractId(_) | SDate(_) | SNumeric(_) | SInt64(_) | SParty(_) | SText(_) |
|
||||
STimestamp(_) | STuple(_, _) | SMap(_) | SRecord(_, _, _) | SAny(_, _) | STNat(_) |
|
||||
_: SPAP | SToken =>
|
||||
STimestamp(_) | STuple(_, _) | SMap(_) | SRecord(_, _, _) | SAny(_, _) | STypeRep(_) |
|
||||
STNat(_) | _: SPAP | SToken =>
|
||||
crash("Match on non-matchable value")
|
||||
}
|
||||
|
||||
|
@ -1121,6 +1121,30 @@ class SBuiltinTest extends FreeSpec with Matchers with TableDrivenPropertyChecks
|
||||
|
||||
}
|
||||
|
||||
"EQUAL_CONTRACT_ID" - {
|
||||
|
||||
val values = Table(
|
||||
"values",
|
||||
"(type_rep @Mod:T)",
|
||||
"(type_rep @Mod:R)",
|
||||
"(type_rep @Int64)",
|
||||
"(type_rep @(Mod:Tree (List Text)))",
|
||||
"(type_rep @((ContractId Mod:T) -> Mod:Color))",
|
||||
)
|
||||
|
||||
"is reflexive" in {
|
||||
forEvery(values)(v => {
|
||||
val e = e"EQUAL_TYPE_REP $v $v"
|
||||
eval(e) shouldBe Right(SBool(true))
|
||||
})
|
||||
}
|
||||
|
||||
"works as expected" in {
|
||||
forEvery(values)(v1 =>
|
||||
forEvery(values)(v2 => eval(e"EQUAL_TYPE_REP $v1 $v2") shouldBe Right(SBool(v1 == v2))))
|
||||
}
|
||||
}
|
||||
|
||||
"Debugging builtins" - {
|
||||
|
||||
"TRACE" - {
|
||||
|
@ -202,11 +202,15 @@ class SpeedyTest extends WordSpec with Matchers {
|
||||
}
|
||||
}
|
||||
|
||||
"to_text_type_con_name" should {
|
||||
"type_rep" should {
|
||||
|
||||
"produces expected output" in {
|
||||
eval(e"""to_text_type_con_name @Test:T1""", anyPkgs) shouldBe Right(SText("-pkgId-:Test:T1"))
|
||||
eval(e"""to_text_type_con_name @Test:T2""", anyPkgs) shouldBe Right(SText("-pkgId-:Test:T2"))
|
||||
eval(e"""type_rep @Test:T1""", anyPkgs) shouldBe Right(STypeRep(t"Test:T1"))
|
||||
eval(e"""type_rep @Test2:T2""", anyPkgs) shouldBe Right(STypeRep(t"Test2:T2"))
|
||||
eval(e"""type_rep @(Mod:Tree (List Text))""", anyPkgs) shouldBe Right(
|
||||
STypeRep(t"Mod:Tree (List Text)"))
|
||||
eval(e"""type_rep @((ContractId Mod:T) -> Mod:Color)""", anyPkgs) shouldBe Right(
|
||||
STypeRep(t"(ContractId Mod:T) -> Mod:Color"))
|
||||
}
|
||||
|
||||
}
|
||||
|
@ -152,7 +152,7 @@ object Ast {
|
||||
final case class EFromAny(ty: Type, body: Expr) extends Expr
|
||||
|
||||
/** Unique textual representation of template Id **/
|
||||
final case class EToTextTypeConName(tyCon: TypeConName) extends Expr
|
||||
final case class ETypeRep(typ: Type) extends Expr
|
||||
|
||||
//
|
||||
// Kinds
|
||||
@ -289,6 +289,7 @@ object Ast {
|
||||
case object BTContractId extends BuiltinType
|
||||
case object BTArrow extends BuiltinType
|
||||
case object BTAny extends BuiltinType
|
||||
case object BTTypeRep extends BuiltinType
|
||||
|
||||
//
|
||||
// Primitive literals
|
||||
@ -422,6 +423,7 @@ object Ast {
|
||||
final case object BEqualBool extends BuiltinFunction(2) // : Bool -> Bool -> Bool
|
||||
final case object BEqualList extends BuiltinFunction(3) // : ∀a. (a -> a -> Bool) -> List a -> List a -> Bool
|
||||
final case object BEqualContractId extends BuiltinFunction(2) // : ∀a. ContractId a -> ContractId a -> Bool
|
||||
final case object BEqualTypeRep extends BuiltinFunction(2) // : TypeRep -> TypeRep -> Bool
|
||||
final case object BCoerceContractId extends BuiltinFunction(1) // : ∀a b. ContractId a -> ContractId b
|
||||
|
||||
//
|
||||
|
@ -59,7 +59,7 @@ object LanguageVersion {
|
||||
val internedDottedNames = v1_dev
|
||||
val numeric = v1_dev
|
||||
val anyType = v1_dev
|
||||
val toTextTypeConName = v1_dev
|
||||
val typeRep = v1_dev
|
||||
|
||||
/** See <https://github.com/digital-asset/daml/issues/1866>. To not break backwards
|
||||
* compatibility, we introduce a new DAML-LF version where this restriction is in
|
||||
|
@ -49,6 +49,7 @@ object Util {
|
||||
val TDate = TBuiltin(BTDate)
|
||||
val TParty = TBuiltin(BTParty)
|
||||
val TAny = TBuiltin(BTAny)
|
||||
val TTypeRep = TBuiltin(BTTypeRep)
|
||||
|
||||
val TNumeric = new ParametricType1(BTNumeric)
|
||||
val TList = new ParametricType1(BTList)
|
||||
|
@ -71,8 +71,7 @@ private[digitalasset] class AstRewriter(
|
||||
exprRule(x)
|
||||
else
|
||||
x match {
|
||||
case EVar(_) | EBuiltin(_) | EPrimCon(_) | EPrimLit(_) | EContractId(_, _) |
|
||||
EToTextTypeConName(_) =>
|
||||
case EVar(_) | EBuiltin(_) | EPrimCon(_) | EPrimLit(_) | EContractId(_, _) | ETypeRep(_) =>
|
||||
x
|
||||
case EVal(ref) =>
|
||||
EVal(apply(ref))
|
||||
|
@ -188,7 +188,7 @@ private[parser] class ExprParser[P](parserParameters: ParserParameters[P]) {
|
||||
}
|
||||
|
||||
private lazy val eToTextTypeConName: Parser[Expr] =
|
||||
`to_text_type_con_name` ~! `@` ~> fullIdentifier ^^ EToTextTypeConName
|
||||
`type_rep` ~>! argTyp ^^ ETypeRep
|
||||
|
||||
private lazy val pattern: Parser[CasePat] =
|
||||
primCon ^^ CPPrimCon |
|
||||
@ -289,6 +289,7 @@ private[parser] class ExprParser[P](parserParameters: ParserParameters[P]) {
|
||||
"EQUAL_BOOL" -> BEqualBool,
|
||||
"EQUAL_LIST" -> BEqualList,
|
||||
"EQUAL_CONTRACT_ID" -> BEqualContractId,
|
||||
"EQUAL_TYPE_REP" -> BEqualTypeRep,
|
||||
"COERCE_CONTRACT_ID" -> BCoerceContractId,
|
||||
)
|
||||
|
||||
|
@ -42,7 +42,7 @@ private[parser] object Lexer extends RegexParsers {
|
||||
"to" -> `to`,
|
||||
"to_any" -> `to_any`,
|
||||
"from_any" -> `from_any`,
|
||||
"to_text_type_con_name" -> `to_text_type_con_name`
|
||||
"type_rep" -> `type_rep`
|
||||
)
|
||||
|
||||
val token: Parser[Token] =
|
||||
|
@ -53,7 +53,7 @@ private[parser] object Token {
|
||||
case object `to` extends Token
|
||||
case object `to_any` extends Token
|
||||
case object `from_any` extends Token
|
||||
case object `to_text_type_con_name` extends Token
|
||||
case object `type_rep` extends Token
|
||||
|
||||
final case class Id(s: String) extends Token
|
||||
final case class ContractId(s: String) extends Token
|
||||
|
@ -29,6 +29,7 @@ private[parser] class TypeParser[P](parameters: ParserParameters[P]) {
|
||||
"Arrow" -> BTArrow,
|
||||
"Map" -> BTMap,
|
||||
"Any" -> BTAny,
|
||||
"TypeRep" -> BTTypeRep,
|
||||
)
|
||||
|
||||
private[parser] def fullIdentifier: Parser[Ref.Identifier] =
|
||||
|
@ -233,6 +233,7 @@ class ParsersSpec extends WordSpec with TableDrivenPropertyChecks with Matchers
|
||||
"EQUAL_BOOL" -> BEqualBool,
|
||||
"EQUAL_LIST" -> BEqualList,
|
||||
"EQUAL_CONTRACT_ID" -> BEqualContractId,
|
||||
"EQUAL_TYPE_REP" -> BEqualTypeRep,
|
||||
"COERCE_CONTRACT_ID" -> BCoerceContractId,
|
||||
)
|
||||
|
||||
|
@ -245,8 +245,7 @@ Version: 1.dev
|
||||
``from_any`` and ``to_any`` functions to convert from/to
|
||||
an arbitrary ground type (i.e. a type with no free type variables) to ``Any``.
|
||||
|
||||
* **Add** ``to_text_type_con_name`` to generate a unique textual representation
|
||||
of a type constructor.
|
||||
* **Add** ``type_rep``, a value presenting a type.
|
||||
|
||||
Abstract syntax
|
||||
^^^^^^^^^^^^^^^
|
||||
@ -544,6 +543,7 @@ Then we can define our kinds, types, and expressions::
|
||||
| 'Update' -- BTyUpdate
|
||||
| 'ContractId' -- BTyContractId
|
||||
| 'Any' -- BTyAny
|
||||
| 'TypeRep' -- BTTypeRep
|
||||
|
||||
Types (mnemonic: tau for type)
|
||||
τ, σ
|
||||
@ -590,7 +590,7 @@ Then we can define our kinds, types, and expressions::
|
||||
| u -- ExpUpdate: Update expression
|
||||
| 'to_any' @τ t -- ExpToAny: Wrap a value of the given type in Any
|
||||
| 'from_any' @τ t -- ExpToAny: Extract a value of the given from Any or return None
|
||||
| 'to_text_type_con_name' @Mod:T -- ExpToTextTypeConName: Generate a unique textual representation of the given TypeConName
|
||||
| 'type_rep' @τ -- ExpToTypeRep: A type representation
|
||||
|
||||
Patterns
|
||||
p
|
||||
@ -807,6 +807,9 @@ First, we formally defined *well-formed types*. ::
|
||||
————————————————————————————————————————————— TyAny
|
||||
Γ ⊢ 'Any' : ⋆
|
||||
|
||||
————————————————————————————————————————————— TyTypeRep
|
||||
Γ ⊢ 'TypeRep' : ⋆
|
||||
|
||||
'record' T (α₁:k₁) … (αₙ:kₙ) ↦ … ∈ 〚Ξ〛Mod
|
||||
————————————————————————————————————————————— TyRecordCon
|
||||
Γ ⊢ Mod:T : k₁ → … → kₙ → ⋆
|
||||
@ -893,17 +896,9 @@ Then we define *well-formed expressions*. ::
|
||||
——————————————————————————————————————————————————————————————— ExpFromAny
|
||||
Γ ⊢ 'from_any' @τ e : 'Optional' τ
|
||||
|
||||
'record' (x : T) ↦ … ∈ 〚Ξ〛Mod
|
||||
——————————————————————————————————————————————————————————————— ExpToTextTypeConNameRecord
|
||||
Γ ⊢ 'to_text_type_con_name' @Mod:T : 'Text'
|
||||
|
||||
'variant' (x : T) ↦ … ∈ 〚Ξ〛Mod
|
||||
——————————————————————————————————————————————————————————————— ExpToTextTypeConNameVariant
|
||||
Γ ⊢ 'to_text_type_con_name' @Mod:T : 'Text'
|
||||
|
||||
'enum' (x : T) ↦ … ∈ 〚Ξ〛Mod
|
||||
——————————————————————————————————————————————————————————————— ExpToTextTypeConNameEnum
|
||||
Γ ⊢ 'to_text_type_con_name' @Mod:T : 'Text'
|
||||
ε ⊢ τ : * τ contains no quantifiers
|
||||
——————————————————————————————————————————————————————————————— ExpTypeRep
|
||||
Γ ⊢ 'type_rep' @τ : 'TypeRep'
|
||||
|
||||
——————————————————————————————————————————————————————————————— ExpBuiltin
|
||||
Γ ⊢ F : 𝕋(F)
|
||||
@ -1508,11 +1503,13 @@ need to be evaluated further. ::
|
||||
——————————————————————————————————————————————————— ValExpTupleCon
|
||||
⊢ᵥ ⟨ f₁ = e₁, …, fₘ = eₘ ⟩
|
||||
|
||||
|
||||
⊢ᵥ e
|
||||
——————————————————————————————————————————————————— ValExpToAny
|
||||
⊢ᵥ 'to_any' @τ e
|
||||
|
||||
——————————————————————————————————————————————————— ValExpTypeRep
|
||||
⊢ᵥ 'type_rep' @τ
|
||||
|
||||
⊢ᵥ e
|
||||
——————————————————————————————————————————————————— ValExpUpdPure
|
||||
⊢ᵥ 'pure' e
|
||||
@ -1683,10 +1680,6 @@ exact output.
|
||||
—————————————————————————————————————————————————————————————————————— EvExpFromAnyFail
|
||||
'from_any' @τ₂ e ‖ E₀ ⇓ 'None' ‖ E₁
|
||||
|
||||
|
||||
—————————————————————————————————————————————————————————————————————— EvExpToTextTypeConName
|
||||
'to_text_type_con_name' @Mod:T ‖ E₀ ⇓ "Mod:T" ‖ E₀
|
||||
|
||||
e₁ ‖ E₀ ⇓ Ok v₁ ‖ E₁
|
||||
v 'matches' p₁ ⇝ Succ (x₁ ↦ v₁ · … · xₘ ↦ vₘ · ε)
|
||||
e₁[x₁ ↦ v₁, …, xₘ ↦ vₘ] ‖ E₁ ⇓ r ‖ E₂
|
||||
@ -2570,6 +2563,16 @@ Map functions
|
||||
|
||||
[*Available in versions >= 1.3*]
|
||||
|
||||
Type Representation function
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
* ``EQUAL_TYPE_REP`` : 'TypeRep' → 'TypeRep' → 'Bool'``
|
||||
|
||||
Returns ``'True'`` if the first type representation is syntactically equal to
|
||||
the second one, ``'False'`` otherwise.
|
||||
|
||||
[*Available in versions >= 1.dev*]
|
||||
|
||||
Conversions functions
|
||||
~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
|
@ -97,6 +97,8 @@ private[validation] object Serializability {
|
||||
unserializable(URFunction)
|
||||
case BTAny =>
|
||||
unserializable(URAny)
|
||||
case BTTypeRep =>
|
||||
unserializable(URTypeRep)
|
||||
}
|
||||
case TForall(_, _) =>
|
||||
unserializable(URForall)
|
||||
|
@ -113,7 +113,9 @@ private[validation] case class TypeSubst(map: Map[TypeVarName, Type], private va
|
||||
|
||||
def apply(expr0: Expr): Expr = expr0 match {
|
||||
case EVar(_) | EVal(_) | EBuiltin(_) | EPrimCon(_) | EPrimLit(_) | EContractId(_, _) |
|
||||
EEnumCon(_, _) | EToTextTypeConName(_) =>
|
||||
EEnumCon(_, _)
|
||||
// Type checking ensures there is no type variables in the arg of ETypeRep
|
||||
| ETypeRep(_) =>
|
||||
expr0
|
||||
case ERecCon(tycon, fields) =>
|
||||
ERecCon(apply(tycon), fields.transform { (_, x) =>
|
||||
|
@ -24,7 +24,7 @@ private[validation] object Typing {
|
||||
}
|
||||
|
||||
private def kindOfBuiltin(bType: BuiltinType): Kind = bType match {
|
||||
case BTInt64 | BTText | BTTimestamp | BTParty | BTBool | BTDate | BTUnit | BTAny =>
|
||||
case BTInt64 | BTText | BTTimestamp | BTParty | BTBool | BTDate | BTUnit | BTAny | BTTypeRep =>
|
||||
KStar
|
||||
case BTNumeric => KArrow(KNat, KStar)
|
||||
case BTList | BTUpdate | BTScenario | BTContractId | BTOptional | BTMap => KArrow(KStar, KStar)
|
||||
@ -181,6 +181,7 @@ private[validation] object Typing {
|
||||
(alpha ->: alpha ->: TBool) ->: TList(alpha) ->: TList(alpha) ->: TBool),
|
||||
BEqualContractId ->
|
||||
TForall(alpha.name -> KStar, TContractId(alpha) ->: TContractId(alpha) ->: TBool),
|
||||
BEqualTypeRep -> (TTypeRep ->: TTypeRep ->: TBool),
|
||||
BCoerceContractId ->
|
||||
TForall(
|
||||
alpha.name -> KStar,
|
||||
@ -727,34 +728,19 @@ private[validation] object Typing {
|
||||
checkExpr(exp, TScenario(typ))
|
||||
}
|
||||
|
||||
private def checkAnyType(typ: Type): Unit = {
|
||||
// we check that typ contains neither variables nor quantifiers
|
||||
TypeTraversable(typ)
|
||||
// we check that typ contains neither variables nor quantifiers
|
||||
private def checkGroundType_(typ: Type): Unit = {
|
||||
typ match {
|
||||
case TVar(_) | TForall(_, _) =>
|
||||
throw EExpectedAnyType(ctx, typ)
|
||||
case _ =>
|
||||
TypeTraversable(typ).foreach(checkAnyType)
|
||||
TypeTraversable(typ).foreach(checkGroundType_)
|
||||
}
|
||||
}
|
||||
|
||||
private def typeOfToAny(ty: Type, body: Expr): Type = {
|
||||
checkAnyType(ty)
|
||||
checkType(ty, KStar)
|
||||
checkExpr(body, ty)
|
||||
TAny
|
||||
}
|
||||
|
||||
private def typeOfFromAny(ty: Type, body: Expr): Type = {
|
||||
checkAnyType(ty)
|
||||
checkType(ty, KStar)
|
||||
checkExpr(body, TAny)
|
||||
TOptional(ty)
|
||||
}
|
||||
|
||||
private def typeOfToTextTypeConName(tpl: TypeConName): Type = {
|
||||
lookupDataType(ctx, tpl)
|
||||
TText
|
||||
private def checkGroundType(typ: Type): Unit = {
|
||||
checkGroundType_(typ)
|
||||
checkType(typ, KStar)
|
||||
}
|
||||
|
||||
def typeOf(expr0: Expr): Type = expr0 match {
|
||||
@ -820,12 +806,17 @@ private[validation] object Typing {
|
||||
checkType(typ, KStar)
|
||||
val _ = checkExpr(body, typ)
|
||||
TOptional(typ)
|
||||
case EToAny(ty, body) =>
|
||||
typeOfToAny(ty, body)
|
||||
case EFromAny(ty, body) =>
|
||||
typeOfFromAny(ty, body)
|
||||
case EToTextTypeConName(tyCon) =>
|
||||
typeOfToTextTypeConName(tyCon)
|
||||
case EToAny(typ, body) =>
|
||||
checkGroundType(typ)
|
||||
checkExpr(body, typ)
|
||||
TAny
|
||||
case EFromAny(typ, body) =>
|
||||
checkGroundType(typ)
|
||||
checkExpr(body, TAny)
|
||||
TOptional(typ)
|
||||
case ETypeRep(typ) =>
|
||||
checkGroundType(typ)
|
||||
TTypeRep
|
||||
}
|
||||
|
||||
def checkExpr(expr: Expr, typ: Type): Type = {
|
||||
|
@ -141,6 +141,9 @@ case object URUninhabitatedType extends UnserializabilityReason {
|
||||
case object URAny extends UnserializabilityReason {
|
||||
def pretty: String = "Any"
|
||||
}
|
||||
case object URTypeRep extends UnserializabilityReason {
|
||||
def pretty: String = "TypeRep"
|
||||
}
|
||||
|
||||
abstract class ValidationError extends java.lang.RuntimeException with Product with Serializable {
|
||||
def context: Context
|
||||
|
@ -13,7 +13,7 @@ private[validation] object ExprTraversable {
|
||||
private[traversable] def foreach[U](x: Expr, f: Expr => U): Unit = {
|
||||
x match {
|
||||
case EVar(_) | EBuiltin(_) | EPrimCon(_) | EPrimLit(_) | EVal(_) | EContractId(_, _) |
|
||||
EEnumCon(_, _) | EToTextTypeConName(_) =>
|
||||
EEnumCon(_, _) | ETypeRep(_) =>
|
||||
case ELocation(_, expr) =>
|
||||
f(expr)
|
||||
case ERecCon(tycon @ _, fields) =>
|
||||
|
@ -61,8 +61,8 @@ private[validation] object TypeTraversable {
|
||||
case EFromAny(typ, expr) =>
|
||||
f(typ)
|
||||
foreach(expr, f)
|
||||
case EToTextTypeConName(tyCon) =>
|
||||
f(TTyCon(tyCon))
|
||||
case ETypeRep(tyCon) =>
|
||||
f(tyCon)
|
||||
case ENil(typ) =>
|
||||
f(typ)
|
||||
case ECons(typ, front, tail) =>
|
||||
|
@ -166,32 +166,32 @@ class TypingSpec extends WordSpec with TableDrivenPropertyChecks with Matchers {
|
||||
E"Λ (τ : ⋆) (σ : ⋆). λ (e₁ : τ) (e₂: σ) → (( case e₁ of _ → e₂ ))" ->
|
||||
T"∀ (τ : ⋆) (σ : ⋆). τ → σ → (( σ ))",
|
||||
// ExpToAny
|
||||
E"""λ (t : Mod:T) -> (( to_any @Mod:T t ))""" ->
|
||||
T"Mod:T -> Any",
|
||||
E"""λ (t : Mod:R Text) -> (( to_any @(Mod:R Text) t ))""" ->
|
||||
T"Mod:R Text -> Any",
|
||||
E"""λ (t : Text) -> (( to_any @Text t ))""" ->
|
||||
T"Text -> Any",
|
||||
E"""λ (t : Int64) -> (( to_any @Int64 t ))""" ->
|
||||
E"""λ (t : Mod:T) → (( to_any @Mod:T t ))""" ->
|
||||
T"Mod:T → Any",
|
||||
E"""λ (t : Mod:R Text) → (( to_any @(Mod:R Text) t ))""" ->
|
||||
T"Mod:R Text → Any",
|
||||
E"""λ (t : Text) → (( to_any @Text t ))""" ->
|
||||
T"Text → Any",
|
||||
E"""λ (t : Int64) → (( to_any @Int64 t ))""" ->
|
||||
T"Int64 -> Any",
|
||||
// ExpFromAny
|
||||
E"""λ (t: Any) -> (( from_any @Mod:T t ))""" ->
|
||||
E"""λ (t: Any) → (( from_any @Mod:T t ))""" ->
|
||||
T"Any → Option Mod:T",
|
||||
E"""λ (t: Any) -> (( from_any @(Mod:R Text) t ))""" ->
|
||||
E"""λ (t: Any) → (( from_any @(Mod:R Text) t ))""" ->
|
||||
T"Any → Option (Mod:R Text)",
|
||||
E"""λ (t: Any) -> (( from_any @Text t ))""" ->
|
||||
E"""λ (t: Any) → (( from_any @Text t ))""" ->
|
||||
T"Any → Option Text",
|
||||
E"""λ (t: Any) -> (( from_any @Int64 t ))""" ->
|
||||
E"""λ (t: Any) → (( from_any @Int64 t ))""" ->
|
||||
T"Any → Option Int64",
|
||||
// ExpToTextTypeConName
|
||||
E"""(( to_text_type_con_name @Mod:T ))""" ->
|
||||
T"Text",
|
||||
E"""(( to_text_type_con_name @Mod:R ))""" ->
|
||||
T"Text",
|
||||
E"""(( to_text_type_con_name @Mod:Tree ))""" ->
|
||||
T"Text",
|
||||
E"""(( to_text_type_con_name @Mod:Color ))""" ->
|
||||
T"Text",
|
||||
// ExpTypeRep
|
||||
E"""(( type_rep @Mod:T ))""" ->
|
||||
T"TypeRep",
|
||||
E"""(( type_rep @Int64 ))""" ->
|
||||
T"TypeRep",
|
||||
E"""(( type_rep @(Mod:Tree (List Text)) ))""" ->
|
||||
T"TypeRep",
|
||||
E"""(( type_rep @((ContractId Mod:T) → Mod:Color) ))""" ->
|
||||
T"TypeRep",
|
||||
)
|
||||
|
||||
forEvery(testCases) { (exp: Expr, expectedType: Type) =>
|
||||
@ -377,8 +377,10 @@ class TypingSpec extends WordSpec with TableDrivenPropertyChecks with Matchers {
|
||||
E"λ (t: Mod:T) → (( from_any @Mod:T t ))",
|
||||
E"Λ (τ : *). λ (t: Any) → (( to_any @(∀ (α : ⋆). Int64) t ))",
|
||||
E"Λ (τ : *). λ (t: Any) → (( to_any @(List (Optional (∀ (α : ⋆). Int64))) t ))",
|
||||
// ExpToTextTypeConName
|
||||
E"to_text_type_con_name @Mod:NoSuchType",
|
||||
// ExpTypeRep
|
||||
E"(( type_rep @Mod:NoSuchType ))",
|
||||
E"Λ (τ : *). (( type_rep @τ ))",
|
||||
E"(( type_rep @(∀(τ : *) . Int64) ))",
|
||||
// ScnPure
|
||||
E"Λ (τ : ⋆ → ⋆). λ (e: τ) → (( spure @τ e ))",
|
||||
E"Λ (τ : ⋆) (σ : ⋆). λ (e: τ) → (( spure @σ e ))",
|
||||
|
@ -38,13 +38,15 @@ import qualified Daml.Trigger.LowLevel as LowLevel
|
||||
|
||||
-- | Active contract set, you can use `getTemplates` to access the templates of
|
||||
-- a given type.
|
||||
newtype ACS = ACS (Map TemplateTypeRep [(AnyContractId, AnyTemplate)])
|
||||
|
||||
-- This will change to a Map once we have proper maps in DAML-LF
|
||||
newtype ACS = ACS [(AnyContractId, AnyTemplate)]
|
||||
|
||||
-- | Extract the templates of a given type from the ACS.
|
||||
getTemplates : forall a. Template a => ACS -> [(AbsoluteContractId a, a)]
|
||||
getTemplates (ACS tpls) = map fromAny $ fromOptional [] $ Map.lookup (templateTypeRep @a) tpls
|
||||
getTemplates (ACS tpls) = mapOptional fromAny tpls
|
||||
where
|
||||
fromAny (cid, tpl) = (fromSome (fromAnyContractId cid), fromSome (fromAnyTemplate tpl))
|
||||
fromAny (cid, tpl) = (,) <$> fromAnyContractId cid <*> fromAnyTemplate tpl
|
||||
|
||||
-- | This is the type of your trigger. `s` is the user-defined state type which
|
||||
-- you can often leave at `()`.
|
||||
@ -116,7 +118,7 @@ runTrigger userTrigger = LowLevel.Trigger
|
||||
}
|
||||
where
|
||||
initialState party (ActiveContracts createdEvents) =
|
||||
let acs = foldl (\acs created -> applyEvent (CreatedEvent created) acs) (ACS Map.empty) createdEvents
|
||||
let acs = foldl (\acs created -> applyEvent (CreatedEvent created) acs) (ACS []) createdEvents
|
||||
userState = userTrigger.initialize acs
|
||||
state = TriggerState acs party userState Map.empty 0
|
||||
in runRule userTrigger.rule state
|
||||
@ -149,21 +151,14 @@ addCommands : Map CommandId [Command] -> Commands -> Map CommandId [Command]
|
||||
addCommands m (Commands cid cmds) = Map.insert cid cmds m
|
||||
|
||||
insertTpl : AnyContractId -> AnyTemplate -> ACS -> ACS
|
||||
insertTpl cid tpl (ACS acs) =
|
||||
case Map.lookup cid.templateId acs of
|
||||
None -> ACS (Map.insert cid.templateId [(cid, tpl)] acs)
|
||||
Some items -> ACS (Map.insert cid.templateId ((cid, tpl) :: items) acs)
|
||||
insertTpl cid tpl (ACS acs) = ACS ((cid, tpl) :: acs)
|
||||
|
||||
deleteTpl : AnyContractId -> ACS -> ACS
|
||||
deleteTpl cid (ACS acs) =
|
||||
case Map.lookup cid.templateId acs of
|
||||
None -> ACS acs
|
||||
Some items -> ACS (Map.insert cid.templateId (filter (\(cid', _) -> cid /= cid') items) acs)
|
||||
deleteTpl cid (ACS acs) = ACS (filter (\(cid', _) -> cid /= cid') acs)
|
||||
|
||||
lookupTpl : Template a => AnyContractId -> ACS -> Optional a
|
||||
lookupTpl cid (ACS acs) = do
|
||||
items <- Map.lookup cid.templateId acs
|
||||
(_, tpl) <- find ((cid ==) . fst) items
|
||||
(_, tpl) <- find ((cid ==) . fst) acs
|
||||
fromAnyTemplate tpl
|
||||
|
||||
applyEvent : Event -> ACS -> ACS
|
||||
|
@ -37,7 +37,15 @@ import DA.Next.Map (MapKey(..))
|
||||
data AnyContractId = AnyContractId
|
||||
{ templateId : TemplateTypeRep
|
||||
, contractId : Text
|
||||
} deriving (Show, Eq, Ord)
|
||||
} deriving Eq
|
||||
|
||||
-- We can’t derive the Show instance since TemplateTypeRep does not have a Show instance
|
||||
-- but it is useful for debugging so we add one that omits the type.
|
||||
instance Show AnyContractId where
|
||||
showsPrec d (AnyContractId _ cid) = showParen (d > app_prec) $
|
||||
showString "AnyContractId " . showsPrec (app_prec +1) cid
|
||||
where app_prec = 10
|
||||
|
||||
|
||||
-- | An absolute contract id on the ledger.
|
||||
-- Contrary to the `ContractId` type which is used
|
||||
|
@ -110,12 +110,13 @@ object Converter {
|
||||
}
|
||||
|
||||
private def fromIdentifier(id: value.Identifier): SValue = {
|
||||
SText(
|
||||
Identifier(
|
||||
PackageId.assertFromString(id.packageId),
|
||||
QualifiedName(
|
||||
DottedName.assertFromString(id.moduleName),
|
||||
DottedName.assertFromString(id.entityName))).toString())
|
||||
STypeRep(
|
||||
TTyCon(
|
||||
TypeConName(
|
||||
PackageId.assertFromString(id.packageId),
|
||||
QualifiedName(
|
||||
DottedName.assertFromString(id.moduleName),
|
||||
DottedName.assertFromString(id.entityName)))))
|
||||
}
|
||||
|
||||
private def fromTransactionId(triggerIds: TriggerIds, transactionId: String): SValue = {
|
||||
@ -283,8 +284,8 @@ object Converter {
|
||||
|
||||
private def toIdentifier(v: SValue): Either[String, Identifier] = {
|
||||
v match {
|
||||
case SText(s) => Identifier.fromString(s)
|
||||
case _ => Left(s"Expected Identifier but got $v")
|
||||
case STypeRep(TTyCon(id)) => Right(id)
|
||||
case _ => Left(s"Expected STypeRep but got $v")
|
||||
}
|
||||
}
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user