Skip to content

Commit

Permalink
interfaces: precondition, scala ast, decoder/encoder (#11452)
Browse files Browse the repository at this point in the history
* interfaces: precondition, scala ast, decoder/encoder

This adds the interface precondition to the scala Daml LF AST, plus
decoder/encoder and the typechecker.

CHANGELOG_BEGIN
CHANGELOG_END

* Update daml-lf/archive/src/main/scala/com/digitalasset/daml/lf/archive/DecodeV1.scala

Co-authored-by: Remy <remy.haemmerle@daml.com>

* format

Co-authored-by: Remy <remy.haemmerle@daml.com>
  • Loading branch information
Robin Krom and remyhaemmerle-da authored Oct 29, 2021
1 parent fd973e6 commit b98a3ad
Show file tree
Hide file tree
Showing 9 changed files with 21 additions and 10 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -444,7 +444,7 @@ convertInterfaces env tyThings = interfaceClasses
intVirtualChoices <- NM.fromList <$> mapM convertVirtualChoice
(MS.findWithDefault [] intName (envInterfaceChoiceData env))
intFixedChoices <- convertChoices env intName emptyTemplateBinds
let intPrecondition = EUnit -- TODO (drsk) #11397 Implement interface preconditions
let intPrecondition = ETrue -- TODO (drsk) #11397 Implement interface preconditions
pure DefInterface {..}

convertVirtualChoice :: ChoiceData -> ConvertM InterfaceChoice
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -677,6 +677,7 @@ private[archive] class DecodeV1(minor: LV.Minor) {
methods = lfInterface.getMethodsList.asScala.view
.map(decodeInterfaceMethod)
.map(method => method.name -> method),
precond = decodeExpr(lfInterface.getPrecond, s"$id:ensure"),
)

private[this] def decodeInterfaceChoice(
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -728,6 +728,7 @@ private[daml] class EncodeV1(minor: LV.Minor) {
builder.accumulateLeft(interface.virtualChoices.sortByKey)(_ addChoices _)
builder.accumulateLeft(interface.fixedChoices.sortByKey)(_ addFixedChoices _)
builder.accumulateLeft(interface.methods.sortByKey)(_ addMethods _)
builder.setPrecond(interface.precond)
builder.build()
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -642,6 +642,7 @@ object Ast {
virtualChoices: Map[ChoiceName, InterfaceChoice],
fixedChoices: Map[ChoiceName, GenTemplateChoice[E]],
methods: Map[MethodName, InterfaceMethod],
precond: E, // Interface creation precondition.
) {
virtualChoices.keys.foreach(name =>
if (fixedChoices.isDefinedAt(name))
Expand All @@ -655,6 +656,7 @@ object Ast {
virtualChoices: Iterable[(ChoiceName, InterfaceChoice)],
fixedChoices: Iterable[(ChoiceName, GenTemplateChoice[E])],
methods: Iterable[(MethodName, InterfaceMethod)],
precond: E,
): GenDefInterface[E] = {
val virtualChoiceMap = toMapWithoutDuplicate(
virtualChoices,
Expand All @@ -668,17 +670,18 @@ object Ast {
methods,
(name: MethodName) => throw PackageError(s"collision on interface method name $name"),
)
GenDefInterface(param, virtualChoiceMap, fixedChoiceMap, methodMap)
GenDefInterface(param, virtualChoiceMap, fixedChoiceMap, methodMap, precond)
}
def unapply(arg: GenDefInterface[E]): Some[
(
ExprVarName,
Map[ChoiceName, InterfaceChoice],
Map[ChoiceName, GenTemplateChoice[E]],
Map[MethodName, InterfaceMethod],
E,
)
] =
Some((arg.param, arg.virtualChoices, arg.fixedChoices, arg.methods))
Some((arg.param, arg.virtualChoices, arg.fixedChoices, arg.methods, arg.precond))
}

type DefInterface = GenDefInterface[Expr]
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -243,12 +243,13 @@ object Util {

private def toSignature(interface: DefInterface): DefInterfaceSignature =
interface match {
case DefInterface(param, virtualChoices, fixedChoices, methods) =>
case DefInterface(param, virtualChoices, fixedChoices, methods, _) =>
DefInterfaceSignature(
param,
virtualChoices,
fixedChoices.transform((_, choice) => toSignature(choice)),
methods,
(),
)
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -323,12 +323,13 @@ private[daml] class AstRewriter(

def apply(x: DefInterface): DefInterface =
x match {
case DefInterface(param, virtualChoices, fixedChoices, methods) =>
case DefInterface(param, virtualChoices, fixedChoices, methods, precond) =>
DefInterface(
param,
virtualChoices.transform((_, v) => apply(v)),
fixedChoices.transform((_, v) => apply(v)),
methods.transform((_, v) => apply(v)),
apply(precond),
)
}
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -455,12 +455,14 @@ private[validation] object Typing {

def checkDefIface(ifaceName: TypeConName, iface: DefInterface): Unit =
iface match {
case DefInterface(param, virtualChoices, fixedChoices, methods) =>
case DefInterface(param, virtualChoices, fixedChoices, methods, precond) =>
fixedChoices.values.foreach(
introExprVar(param, TTyCon(ifaceName)).checkChoice(ifaceName, _)
)
virtualChoices.values.foreach(checkIfaceChoice)
methods.values.foreach(checkIfaceMethod)
val env = introExprVar(param, TTyCon(ifaceName))
env.checkExpr(precond, TBool)
}

def checkIfaceChoice(choice: InterfaceChoice): Unit = {
Expand All @@ -477,7 +479,7 @@ private[validation] object Typing {
AlphaEquiv.alphaEquiv(expandTypeSynonyms(t1), expandTypeSynonyms(t2))

def checkIfaceImplementation(tplTcon: TypeConName, impl: TemplateImplements): Unit = {
val DefInterfaceSignature(_, virtualChoices, _, methods) =
val DefInterfaceSignature(_, virtualChoices, _, methods, _) =
handleLookup(ctx, interface.lookupInterface(impl.interface))
virtualChoices.values.foreach { case InterfaceChoice(name, consuming, argType, returnType) =>
val tplChoice = handleLookup(ctx, interface.lookupChoice(tplTcon, name))
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -206,8 +206,9 @@ private[validation] object ExprIterable {
virtualChoices @ _,
fixedChoices,
methods @ _,
precond,
) =>
fixedChoices.values.iterator.flatMap(iterator(_))
Iterator(precond) ++ fixedChoices.values.iterator.flatMap(iterator(_))
}

def apply(expr: Expr): Iterable[Expr] =
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -238,8 +238,9 @@ private[validation] object TypeIterable {

private[validation] def iterator(interface: DefInterface): Iterator[Type] =
interface match {
case DefInterface(_, virtualChoices, fixedChoice, methods) =>
virtualChoices.values.iterator.flatMap(iterator) ++
case DefInterface(_, virtualChoices, fixedChoice, methods, precond) =>
iterator(precond) ++
virtualChoices.values.iterator.flatMap(iterator) ++
fixedChoice.values.iterator.flatMap(iterator) ++
methods.values.iterator.flatMap(iterator)
}
Expand Down

0 comments on commit b98a3ad

Please sign in to comment.