Add ViewInterface to LF - stub interpretation in speedy

Should move this to another PR...
digital-asset · Jul 20, 2022 · fe85d96 · fe85d96
1 parent 3338bb4
commit fe85d96
Show file tree

Hide file tree

Showing 21 changed files with 104 additions and 16 deletions.
diff --git a/compiler/daml-lf-ast/src/DA/Daml/LF/Ast/Alpha.hs b/compiler/daml-lf-ast/src/DA/Daml/LF/Ast/Alpha.hs
@@ -284,8 +284,12 @@ alphaExpr' env = \case
     ELocation _ e1 -> \case
         ELocation _ e2 -> alphaExpr' env e1 e2
         _ -> False
-    EViewInterface t1 -> \case
-        EViewInterface t2 -> alphaTypeCon t1 t2
+    EViewInterface iface1 template1 view1 expr1 -> \case
+        EViewInterface iface2 template2 view2 expr2
+            -> alphaTypeCon iface1 iface2
+            && alphaTypeCon template1 template2
+            && alphaType' env view1 view2
+            && alphaExpr' env expr1 expr2
         _ -> False
     EExperimental n1 t1 -> \case
         EExperimental n2 t2 -> n1 == n2 && alphaType t1 t2

diff --git a/compiler/daml-lf-ast/src/DA/Daml/LF/Ast/Base.hs b/compiler/daml-lf-ast/src/DA/Daml/LF/Ast/Base.hs
@@ -606,6 +606,9 @@ data Expr
   -- | Obtain an interface view
   | EViewInterface
     { viewInterfaceInterface :: !(Qualified TypeConName)
+    , viewInterfaceTemplate :: !(Qualified TypeConName)
+    , viewInterfaceViewtype :: !Type
+    , viewInterfaceExpr :: !Expr
     }
   -- | Experimental Expression Hook
   | EExperimental !T.Text !Type

diff --git a/compiler/daml-lf-ast/src/DA/Daml/LF/Ast/FreeVars.hs b/compiler/daml-lf-ast/src/DA/Daml/LF/Ast/FreeVars.hs
@@ -114,7 +114,7 @@ freeVarsStep = \case
     EInterfaceTemplateTypeRepF _ e -> e
     ESignatoryInterfaceF _ e -> e
     EObserverInterfaceF _ e -> e
-    EViewInterfaceF _ -> mempty
+    EViewInterfaceF _ _ t e -> freeVarsInType t <> e
     EExperimentalF _ t -> freeVarsInType t
 
   where

diff --git a/compiler/daml-lf-ast/src/DA/Daml/LF/Ast/Pretty.hs b/compiler/daml-lf-ast/src/DA/Daml/LF/Ast/Pretty.hs
@@ -552,7 +552,8 @@ instance Pretty Expr where
         [interfaceArg ty, TmArg expr]
     EObserverInterface ty expr -> pPrintAppKeyword lvl prec "observer_interface"
         [interfaceArg ty, TmArg expr]
-    EViewInterface ty -> pPrintAppKeyword lvl prec "view" [interfaceArg ty]
+    EViewInterface iface template view expr -> pPrintAppKeyword lvl prec "view"
+        [interfaceArg iface, interfaceArg template, TyArg view, TmArg expr]
     EExperimental name _ ->  pPrint $ "$" <> name
 
 instance Pretty DefTypeSyn where

diff --git a/compiler/daml-lf-ast/src/DA/Daml/LF/Ast/Recursive.hs b/compiler/daml-lf-ast/src/DA/Daml/LF/Ast/Recursive.hs
@@ -60,7 +60,7 @@ data ExprF expr
   | EInterfaceTemplateTypeRepF !(Qualified TypeConName) !expr
   | ESignatoryInterfaceF !(Qualified TypeConName) !expr
   | EObserverInterfaceF !(Qualified TypeConName) !expr
-  | EViewInterfaceF !(Qualified TypeConName)
+  | EViewInterfaceF !(Qualified TypeConName) !(Qualified TypeConName) !Type !expr
   | EExperimentalF !T.Text !Type
   deriving (Foldable, Functor, Traversable)
 
@@ -222,7 +222,7 @@ instance Recursive Expr where
     EInterfaceTemplateTypeRep a b -> EInterfaceTemplateTypeRepF a b
     ESignatoryInterface a b -> ESignatoryInterfaceF a b
     EObserverInterface a b -> EObserverInterfaceF a b
-    EViewInterface a -> EViewInterfaceF a
+    EViewInterface a b c d -> EViewInterfaceF a b c d
     EExperimental a b -> EExperimentalF a b
 
 instance Corecursive Expr where
@@ -267,5 +267,5 @@ instance Corecursive Expr where
     EInterfaceTemplateTypeRepF a b -> EInterfaceTemplateTypeRep a b
     ESignatoryInterfaceF a b -> ESignatoryInterface a b
     EObserverInterfaceF a b -> EObserverInterface a b
-    EViewInterfaceF a -> EViewInterface a
+    EViewInterfaceF a b c d -> EViewInterface a b c d
     EExperimentalF a b -> EExperimental a b
diff --git a/compiler/daml-lf-ast/src/DA/Daml/LF/Ast/Subst.hs b/compiler/daml-lf-ast/src/DA/Daml/LF/Ast/Subst.hs
@@ -221,7 +221,11 @@ applySubstInExpr subst@Subst{..} = \case
     ELocation l e -> ELocation
         l
         (applySubstInExpr subst e)
-    EViewInterface t -> EViewInterface t
+    EViewInterface iface template view expr -> EViewInterface
+        iface
+        template
+        (applySubstInType subst view)
+        (applySubstInExpr subst expr)
     EExperimental name ty ->
         EExperimental name (applySubstInType subst ty)
 

diff --git a/compiler/daml-lf-proto/src/DA/Daml/LF/Proto3/DecodeV1.hs b/compiler/daml-lf-proto/src/DA/Daml/LF/Proto3/DecodeV1.hs
@@ -709,6 +709,11 @@ decodeExprSum exprSum = mayDecode "exprSum" exprSum $ \case
   LF1.ExprSumObserverInterface LF1.Expr_ObserverInterface {..} -> EObserverInterface
     <$> mayDecode "expr_ObserverInterfaceInterface" expr_ObserverInterfaceInterface decodeTypeConName
     <*> mayDecode "expr_ObserverInterfaceExpr" expr_ObserverInterfaceExpr decodeExpr
+  LF1.ExprSumViewInterface LF1.Expr_ViewInterface {..} -> EViewInterface
+    <$> mayDecode "expr_ViewInterfaceInterface" expr_ViewInterfaceInterface decodeTypeConName
+    <*> mayDecode "expr_ViewInterfaceTemplate" expr_ViewInterfaceTemplate decodeTypeConName
+    <*> mayDecode "expr_ViewInterfaceViewtype" expr_ViewInterfaceViewtype decodeType
+    <*> mayDecode "expr_ViewInterfaceExpr" expr_ViewInterfaceExpr decodeExpr
   LF1.ExprSumExperimental (LF1.Expr_Experimental name mbType) -> do
     ty <- mayDecode "expr_Experimental" mbType decodeType
     pure $ EExperimental (decodeString name) ty

diff --git a/compiler/daml-lf-proto/src/DA/Daml/LF/Proto3/EncodeV1.hs b/compiler/daml-lf-proto/src/DA/Daml/LF/Proto3/EncodeV1.hs
@@ -736,8 +736,11 @@ encodeExpr' = \case
         expr_ObserverInterfaceInterface <- encodeQualTypeConName ty
         expr_ObserverInterfaceExpr <- encodeExpr val
         pureExpr $ P.ExprSumObserverInterface P.Expr_ObserverInterface{..}
-    EViewInterface iface -> do
+    EViewInterface iface template view expr -> do
         expr_ViewInterfaceInterface <- encodeQualTypeConName iface
+        expr_ViewInterfaceTemplate <- encodeQualTypeConName template
+        expr_ViewInterfaceViewtype <- encodeType view
+        expr_ViewInterfaceExpr <- encodeExpr expr
         pureExpr $ P.ExprSumViewInterface P.Expr_ViewInterface{..}
     EExperimental name ty -> do
         let expr_ExperimentalName = encodeString name

diff --git a/compiler/daml-lf-tools/src/DA/Daml/LF/Simplifier.hs b/compiler/daml-lf-tools/src/DA/Daml/LF/Simplifier.hs
@@ -217,6 +217,7 @@ safetyStep = \case
   EInterfaceTemplateTypeRepF _ s -> s <> Safe 0
   ESignatoryInterfaceF _ s -> s <> Safe 0
   EObserverInterfaceF _ s -> s <> Safe 0
+  EViewInterfaceF _ _ _ _ -> Unsafe
   EExperimentalF _ _ -> Unsafe
 
 isTypeClassDictionary :: DefValue -> Bool

diff --git a/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Check.hs b/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Check.hs
@@ -793,6 +793,13 @@ typeOf' = \case
   EUpdate upd -> typeOfUpdate upd
   EScenario scen -> typeOfScenario scen
   ELocation _ expr -> typeOf' expr
+  EViewInterface iface template viewtype expr -> do
+    checkImplements template iface
+    iface <- inWorld (lookupInterface iface)
+    unless (alphaType (intView iface) viewtype) $
+      throwWithContext ETypeMismatch{foundType = viewtype, expectedType = intView iface, expr = Nothing}
+    checkExpr expr (TCon template)
+    pure viewtype
   EExperimental name ty -> do
     checkFeature featureExperimental
     checkExperimentalType name ty

diff --git a/compiler/damlc/daml-lf-conversion/src/DA/Daml/LFConversion.hs b/compiler/damlc/daml-lf-conversion/src/DA/Daml/LFConversion.hs
@@ -1240,6 +1240,7 @@ internalFunctions = listToUFM $ map (bimap mkModuleNameFS mkUniqSet)
     , ("DA.Internal.Desugar",
         [ "mkMethod"
         , "mkInterfaceView"
+        , "view"
         ])
     ]
 
@@ -1284,16 +1285,21 @@ convertExpr env0 e = do
     -- erase mkInterfaceView calls and leave only the body.
     go env (VarIn DA_Internal_Desugar "mkInterfaceView") (LType _tpl : LType _iface : LType _viewTy : LExpr _implDict : LExpr _hasInterfaceViewDic : LExpr body : args)
         = go env body args
-    go env (VarIn DA_Internal_Interface "view") (LType t : LType _template : LType _view : LType _ args)
+    go env (VarIn DA_Internal_Desugar "view") (LType iface : LType template : LType view : LExpr _implementsDic : LExpr _hasInterfaceViewDic : args)
         = do
-        ty <- convertType env t
-        case ty of
-            TCon iface ->
+        ifaceLF <- convertType env iface
+        templateLF <- convertType env template
+        viewLF <- convertType env view
+        case (ifaceLF, templateLF) of
+            (TCon ifaceName, TCon templateName) ->
                 pure
-                  ( EView iface
+                  ( ETmLam (mkVar "t", TCon templateName) $
+                    EViewInterface ifaceName templateName viewLF (EVar $ mkVar "t")
                   , args
                   )
-            _ -> unsupported "view not type-applied to interface." t
+            (_, TCon _) -> unsupported "view not type-applied to an interface." iface
+            (TCon _, _) -> unsupported "view not type-applied to an template." template
+            (_, _) -> unsupported "view not type-applied to an interface nor a template." (iface, template)
     go env (VarIn GHC_Types "primitiveInterface") (LType (isStrLitTy -> Just y) : LType t : args)
         = do
         ty <- convertType env t

diff --git a/compiler/damlc/daml-stdlib-src/DA/Internal/Desugar.daml b/compiler/damlc/daml-stdlib-src/DA/Internal/Desugar.daml
@@ -4,6 +4,7 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
 
 -- | HIDE Automatically imported qualified in every module.
 module DA.Internal.Desugar (
@@ -138,4 +139,4 @@ mkInterfaceView = magic @"mkInterfaceView"
 
 -- | Function for views
 view : forall i t v. (Implements t i, HasInterfaceView i v) => t -> v
-view = view -- deleted by the compiler
+view = magic @"view" -- deleted by the compiler
diff --git a/daml-lf/archive/src/main/protobuf/com/daml/daml_lf_dev/daml_lf_1.proto b/daml-lf/archive/src/main/protobuf/com/daml/daml_lf_dev/daml_lf_1.proto
@@ -975,6 +975,9 @@ message Expr {
   // *Available in versions >= 1.dev*
   message ViewInterface {
     TypeConName interface = 1;
+    TypeConName template = 2;
+    Type viewtype = 3;
+    Expr expr = 4;
   }
 
   // Obtain the type representation of a contract through an interface

diff --git a/daml-lf/archive/src/main/scala/com/digitalasset/daml/lf/archive/DecodeV1.scala b/daml-lf/archive/src/main/scala/com/digitalasset/daml/lf/archive/DecodeV1.scala
@@ -1227,6 +1227,16 @@ private[archive] class DecodeV1(minor: LV.Minor) {
         case PLF.Expr.SumCase.SUM_NOT_SET =>
           throw Error.Parsing("Expr.SUM_NOT_SET")
 
+        case PLF.Expr.SumCase.VIEW_INTERFACE =>
+          assertSince(LV.Features.interfaces, "Expr.view_interface")
+          val viewInterface = lfExpr.getViewInterface
+          EViewInterface(
+            ifaceId = decodeTypeConName(viewInterface.getInterface),
+            templateId = decodeTypeConName(viewInterface.getTemplate),
+            viewtype = decodeType(viewInterface.getViewtype),
+            expr = decodeExpr(viewInterface.getExpr, definition),
+          )
+
         case PLF.Expr.SumCase.EXPERIMENTAL =>
           assertSince(LV.v1_dev, "Expr.experimental")
           val experimental = lfExpr.getExperimental

diff --git a/daml-lf/interpreter/src/main/scala/com/digitalasset/daml/lf/speedy/PhaseOne.scala b/daml-lf/interpreter/src/main/scala/com/digitalasset/daml/lf/speedy/PhaseOne.scala
@@ -367,6 +367,10 @@ private[lf] final class PhaseOne(
         compileExp(env, exp) { exp =>
           Return(SBObserverInterface(ifaceId)(exp))
         }
+      case EViewInterface(ifaceId, templateId, view, exp) =>
+        compileExp(env, exp) { exp =>
+          Return(SBViewInterface(ifaceId, templateId, view)(exp))
+        }
       case EExperimental(name, _) =>
         Return(SBExperimental(name))
     }

diff --git a/daml-lf/interpreter/src/main/scala/com/digitalasset/daml/lf/speedy/SBuiltin.scala b/daml-lf/interpreter/src/main/scala/com/digitalasset/daml/lf/speedy/SBuiltin.scala
@@ -1338,6 +1338,18 @@ private[lf] object SBuiltin {
     }
   }
 
+  final case class SBViewInterface(
+      ifaceId: TypeConName,
+      templateId: TypeConName,
+      viewtype: Ast.Type,
+  ) extends SBuiltin(1) {
+    override private[speedy] def execute(args: util.ArrayList[SValue], machine: Machine): Unit = {
+      crash(
+        s"Tried to run unsupported view with interface ${ifaceId}, template ${templateId}, viewtype ${viewtype}."
+      )
+    }
+  }
+
   /** $insertFetch[tid]
     *    :: ContractId a
     *    -> List Party    (signatories)

diff --git a/daml-lf/language/src/main/scala/com/digitalasset/daml/lf/language/Ast.scala b/daml-lf/language/src/main/scala/com/digitalasset/daml/lf/language/Ast.scala
@@ -217,6 +217,14 @@ object Ast {
       body: Expr,
   ) extends Expr
 
+  /** Obtain the view of an interface. */
+  final case class EViewInterface(
+      ifaceId: TypeConName,
+      templateId: TypeConName,
+      viewtype: Type,
+      expr: Expr,
+  ) extends Expr
+
   //
   // Kinds
   //

diff --git a/daml-lf/parser/src/main/scala/com/digitalasset/daml/lf/testing/parser/AstRewriter.scala b/daml-lf/parser/src/main/scala/com/digitalasset/daml/lf/testing/parser/AstRewriter.scala
@@ -148,6 +148,8 @@ private[daml] class AstRewriter(
           EInterfaceTemplateTypeRep(apply(ifaceId), apply(body))
         case ESignatoryInterface(ifaceId, body) =>
           ESignatoryInterface(apply(ifaceId), apply(body))
+        case EViewInterface(ifaceId, templateId, viewtype, expr) =>
+          EViewInterface(apply(ifaceId), apply(templateId), apply(viewtype), apply(expr))
         case EObserverInterface(ifaceId, body) =>
           EObserverInterface(apply(ifaceId), apply(body))
       }

diff --git a/daml-lf/validation/src/main/scala/com/digitalasset/daml/lf/validation/Typing.scala b/daml-lf/validation/src/main/scala/com/digitalasset/daml/lf/validation/Typing.scala
@@ -1261,6 +1261,13 @@ private[validation] object Typing {
         discard(handleLookup(ctx, pkgInterface.lookupInterface(ifaceId)))
         checkExpr(body, TTyCon(ifaceId))
         TList(TParty)
+      case EViewInterface(ifaceId @ _, templateId, view, expr) =>
+        checkImplements(templateId, ifaceId)
+        val iface = handleLookup(ctx, pkgInterface.lookupInterface(ifaceId))
+        if (!alphaEquiv(iface.view, view))
+          throw ETypeMismatch(ctx, foundType = view, expectedType = iface.view, expr = None)
+        checkExpr(expr, TTyCon(templateId))
+        view
       case EExperimental(_, typ) =>
         typ
     }

diff --git a/...validation/src/main/scala/com/digitalasset/daml/lf/validation/iterable/ExprIterable.scala b/...validation/src/main/scala/com/digitalasset/daml/lf/validation/iterable/ExprIterable.scala
@@ -82,6 +82,8 @@ private[validation] object ExprIterable {
         iterator(body)
       case ESignatoryInterface(iface @ _, body) =>
         iterator(body)
+      case EViewInterface(ifaceId @ _, templateId @ _, view @ _, expr) =>
+        iterator(expr)
       case EObserverInterface(iface @ _, body) =>
         iterator(body)
     }

diff --git a/...validation/src/main/scala/com/digitalasset/daml/lf/validation/iterable/TypeIterable.scala b/...validation/src/main/scala/com/digitalasset/daml/lf/validation/iterable/TypeIterable.scala
@@ -99,6 +99,11 @@ private[validation] object TypeIterable {
         Iterator(TTyCon(ifaceId)) ++ iterator(body)
       case EObserverInterface(ifaceId, body) =>
         Iterator(TTyCon(ifaceId)) ++ iterator(body)
+      case EViewInterface(ifaceId, templateId, view, expr) =>
+        Iterator(TTyCon(ifaceId)) ++
+          Iterator(TTyCon(templateId)) ++
+          iterator(view) ++
+          iterator(expr)
       case EVar(_) | EVal(_) | EBuiltin(_) | EPrimCon(_) | EPrimLit(_) | EApp(_, _) | ECase(_, _) |
           ELocation(_, _) | EStructCon(_) | EStructProj(_, _) | EStructUpd(_, _, _) | ETyAbs(_, _) |
           EExperimental(_, _) =>