Replace !<...!> predicate-constructor delimiters with {...}

src/main/antlr4/GobraParser.g4

@@ -424,7 +424,7 @@ functionLit: specification closureDecl[$specification.trusted, $specification.pu
 
 closureDecl[boolean trusted, boolean pure]:  FUNC IDENTIFIER? (signature blockWithBodyParameterInfo?);
 
-predConstructArgs: L_PRED expressionList? COMMA? R_PRED;
+predConstructArgs: L_CURLY expressionList? COMMA? R_CURLY;
 
 // Added predicate spec and method specifications
 interfaceType:

src/main/resources/stubs/sync/waitgroup.gobra

@@ -58,14 +58,14 @@ func (g *WaitGroup) SetWaitMode(ghost p perm, ghost q perm)
 // latest proposal for WaitGroups (as of 21/01/2021)
 ghost
 requires P() && g.UnitDebt(P)
-ensures g.UnitDebt(PredTrue!<!>)
+ensures g.UnitDebt(PredTrue{})
 decreases _
 func (g *WaitGroup) PayDebt(ghost P pred())
 
-// Simplified version of the debt redistribution rule, instantiated with P == { PredTrue!<!> } and Q == { R }.
+// Simplified version of the debt redistribution rule, instantiated with P == { PredTrue{} } and Q == { R }.
 // This is the only rule that generates a Token.
 ghost
-requires g.UnitDebt(PredTrue!<!>)
+requires g.UnitDebt(PredTrue{})
 ensures g.UnitDebt(R) && g.Token(R)
 decreases _
 func (g *WaitGroup) GenerateTokenAndDebt(ghost R pred())
@@ -80,16 +80,16 @@ func (g *WaitGroup) GenerateToken(ghost R pred())
 requires p >= 0
 requires n > 0 && p > 0 ==> acc(g.WaitGroupP(), p) && !g.WaitMode()
 requires (n > 0 && p == 0) ==> g.UnitDebt(P)
-requires n < 0 ==> acc(g.UnitDebt(PredTrue!<!>), -n/1)
+requires n < 0 ==> acc(g.UnitDebt(PredTrue{}), -n/1)
 ensures (n > 0 && p > 0) ==> acc(g.WaitGroupP(), p)
 ensures (n > 0 && p == 0) ==> g.UnitDebt(P)
-ensures n > 0 ==> acc(g.UnitDebt(PredTrue!<!>), n/1)
+ensures n > 0 ==> acc(g.UnitDebt(PredTrue{}), n/1)
 // this is actually necessary, otherwise Gobra cannot prove that Add does not modify the wait mode
 ensures (n > 0 && p > 0) ==> g.WaitMode() == old(g.WaitMode())
 decreases _
 func (g *WaitGroup) Add(n int, ghost p perm, ghost P pred())
 
-requires g.UnitDebt(PredTrue!<!>)
+requires g.UnitDebt(PredTrue{})
 decreases _
 func (g *WaitGroup) Done()
 
@@ -120,9 +120,9 @@ pred CollectFractions(ghost P seq[pred()], ghost perms seq[perm]) {
 ghost
 requires len(P) == len(permsP)
 requires len(Q) == len(permsQ)
-requires g.UnitDebt(CollectFractions!<P ++ Q, permsP ++ permsQ!>)
-requires g.UnitDebt(PredTrue!<!>)
-ensures g.UnitDebt(CollectFractions!<P, permsP!>) && g.UnitDebt(CollectFractions!<Q, permsQ!>)
+requires g.UnitDebt(CollectFractions{P ++ Q, permsP ++ permsQ})
+requires g.UnitDebt(PredTrue{})
+ensures g.UnitDebt(CollectFractions{P, permsP}) && g.UnitDebt(CollectFractions{Q, permsQ})
 decreases _
 func (g *WaitGroup) SplitSequence(ghost P seq[pred()], ghost Q seq[pred()], ghost permsP seq[perm], ghost permsQ seq[perm])
 
@@ -133,10 +133,10 @@ requires len(P) == len(permsQ)
 requires len(P) == len(permsR)
 requires forall i int :: 0 <= i && i < len(P) ==> permsP[i] >= 0
 requires forall i int :: 0 <= i && i < len(P) ==> permsQ[i] >= 0
-requires g.UnitDebt(CollectFractions!<P, permsR!>)
-requires g.UnitDebt(PredTrue!<!>)
+requires g.UnitDebt(CollectFractions{P, permsR})
+requires g.UnitDebt(PredTrue{})
 requires forall i int :: 0 <= i && i < len(P) ==> permsP[i] + permsQ[i] == permsR[i]
-ensures g.UnitDebt(CollectFractions!<P, permsP!>)
-ensures g.UnitDebt(CollectFractions!<P, permsQ!>)
+ensures g.UnitDebt(CollectFractions{P, permsP})
+ensures g.UnitDebt(CollectFractions{P, permsQ})
 decreases _
 func (g *WaitGroup) SplitFractions(ghost P seq[pred()], ghost permsP seq[perm], ghost permsQ seq[perm], ghost permsR seq[perm])

src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala

@@ -1364,7 +1364,7 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
 
   /**
     * Visits the rule
-    * predConstructArgs: L_PRED expressionList? COMMA? R_PRED
+    * predConstructArgs: L_CURLY expressionList? COMMA? R_CURLY
     * @param ctx the parse tree
     *     */
   override def visitPredConstructArgs(ctx: PredConstructArgsContext): PredArgs = {

src/main/scala/viper/gobra/frontend/Parser.scala

@@ -239,6 +239,7 @@ object Parser extends LazyLogging {
       postprocessors = Seq(
         new ImportPostprocessor(parseAst.positions.positions),
         new TerminationMeasurePostprocessor(parseAst.positions.positions, specOnly = specOnly),
+        new PredicateConstructorPostprocessor(parseAst.positions.positions),
       )
       postprocessedAst <- postprocessors.foldLeft[Either[Vector[ParserError], PPackage]](Right(parseAst)) {
         case (Right(ast), postprocessor) => postprocessor.postprocess(ast)(config)
@@ -515,6 +516,108 @@ object Parser extends LazyLogging {
     }
   }
 
+  private class PredicateConstructorPostprocessor(override val positions: Positions) extends Postprocessor {
+    /**
+      * Predicate constructors share their `name { args }` surface syntax with composite literals,
+      * so the parser conservatively builds a `PCompositeLit` for `IDENT { ... }` and
+      * `IDENT.IDENT { ... }` shapes. This postprocessor rewrites such literals into
+      * `PPredConstructor` when they are unambiguously predicate constructors:
+      *   1. They contain at least one positional `_` element (illegal in composite literals), or
+      *   2. The named/dotted base resolves syntactically to a top-level predicate declared in
+      *      the current package or to a built-in predicate.
+      *
+      * Cross-package cases (e.g. `pkg.P{1}()`) are deferred to a second pass driven by the
+      * type checker -- see [[PredicateConstructorRewriter.rewriteCrossPackage]].
+      */
+    def postprocess(pkg: PPackage)(config: Config): Either[Vector[ParserError], PPackage] = {
+      // collect names of all top-level (function and method) predicate declarations
+      val localPredicateNames: Set[String] = pkg.programs.flatMap(_.declarations.collect {
+        case d: PFPredicateDecl => d.id.name
+        case d: PMPredicateDecl => d.id.name
+      }).toSet
+      Right(PredicateConstructorRewriter.rewrite(pkg, localPredicateNames, _ => Set.empty)(positions))
+    }
+  }
+
+  /**
+    * Shared rewrite logic that turns `PCompositeLit` nodes whose name resolves (syntactically) to
+    * a predicate into the equivalent `PPredConstructor`. Used both by the parse-time
+    * [[PredicateConstructorPostprocessor]] (which only knows the current package's predicates)
+    * and by [[viper.gobra.frontend.info.Info]] (which additionally has access to imported
+    * packages' predicate names via `dependentTypeInfo`).
+    */
+  object PredicateConstructorRewriter {
+    private lazy val builtInPredicateNames: Set[String] =
+      viper.gobra.frontend.info.base.BuiltInMemberTag.builtInMembers().collect {
+        case t: viper.gobra.frontend.info.base.BuiltInMemberTag.BuiltInPredicateTag => t.identifier
+      }.toSet
+
+    private class Impl(override val positions: Positions) extends PositionedRewriter {
+      def at[N <: AnyRef](node: N, source: PNode): N = { positions.dupPos(source, node); node }
+
+      def run(
+        pkg: PPackage,
+        localPredicateNames: Set[String],
+        importedPredicateNames: String => Set[String],
+      ): PPackage = {
+        def hasKey(lit: PLiteralValue): Boolean = lit.elems.exists(_.key.isDefined)
+        def hasBlank(lit: PLiteralValue): Boolean = lit.elems.exists {
+          case PKeyedElement(None, PExpCompositeVal(_: PBlankIdentifier)) => true
+          case _ => false
+        }
+        def isLocalOrBuiltInPredName(name: String): Boolean =
+          localPredicateNames.contains(name) || builtInPredicateNames.contains(name)
+
+        def shouldRewrite(typ: PLiteralType, lit: PLiteralValue): Boolean = {
+          if (hasKey(lit)) false
+          else typ match {
+            case PNamedOperand(id) => hasBlank(lit) || isLocalOrBuiltInPredName(id.name)
+            case PDot(qual: PNamedOperand, id) =>
+              hasBlank(lit) || isLocalOrBuiltInPredName(id.name) || importedPredicateNames(qual.id.name).contains(id.name)
+            case PDot(_, id) => hasBlank(lit) || isLocalOrBuiltInPredName(id.name)
+            case _ => false
+          }
+        }
+
+        def convertArgs(lit: PLiteralValue): Vector[Option[PExpression]] = lit.elems.map {
+          case PKeyedElement(None, PExpCompositeVal(_: PBlankIdentifier)) => None
+          case PKeyedElement(None, PExpCompositeVal(e)) => Some(e)
+          case e => Violation.violation(s"unexpected element form in predicate constructor candidate: $e")
+        }
+
+        def buildBase(typ: PLiteralType): PPredConstructorBase = typ match {
+          case op@PNamedOperand(id) => at(PFPredBase(id), op)
+          case d: PDot => at(PDottedBase(d), d)
+          case t => Violation.violation(s"unexpected base for predicate constructor: $t")
+        }
+
+        val rewritePredConstructors: Strategy =
+          strategyWithName[Any]("rewritePredConstructors", {
+            case n@PCompositeLit(typ, lit) if shouldRewrite(typ, lit) =>
+              Some(at(PPredConstructor(buildBase(typ), convertArgs(lit)), n))
+            case n => Some(n)
+          })
+
+        val updatedProgs = pkg.programs.map { prog =>
+          val updatedDecls = rewrite(topdown(attempt(rewritePredConstructors)))(prog.declarations)
+          at(PProgram(prog.packageClause, prog.pkgInvariants, prog.imports, prog.friends, updatedDecls), prog)
+        }
+        at(PPackage(pkg.packageClause, updatedProgs, pkg.positions, pkg.info), pkg)
+      }
+    }
+
+    /** Runs the rewrite over `pkg`. `localPredicateNames` is the set of top-level predicate
+      * names (function and method) declared in `pkg`. `importedPredicateNames(qual)` returns the
+      * set of predicate names exposed by the package imported under qualifier `qual`, or an
+      * empty set if `qual` is not an import qualifier or its imports aren't yet known. */
+    def rewrite(
+      pkg: PPackage,
+      localPredicateNames: Set[String],
+      importedPredicateNames: String => Set[String],
+    )(positions: Positions): PPackage =
+      new Impl(positions).run(pkg, localPredicateNames, importedPredicateNames)
+  }
+
   private class SyntaxAnalyzer[Rule <: ParserRuleContext, Node <: AnyRef](tokens: CommonTokenStream, source: Source, errors: ListBuffer[ParserError], pom: PositionManager, specOnly: Boolean = false) extends GobraParser(tokens){
 
 

src/main/scala/viper/gobra/frontend/info/Info.scala

@@ -221,6 +221,60 @@ object Info extends LazyLogging {
     } yield typeInfo
   }
 
+  /**
+    * Performs a second-pass rewrite of cross-package predicate constructors.
+    *
+    * The parse-time postprocessor only knows the current package's predicate names and so
+    * leaves expressions like `pkg.P{1}()` -- where `P` is a predicate declared in the imported
+    * package `pkg` -- as `PCompositeLit`. Once `dependentTypeInfo` is available, we know each
+    * import's qualifier name and can ask its `ExternalTypeInfo` whether a given identifier
+    * resolves to a predicate.
+    */
+  private def rewriteCrossPackagePredConstructors(
+    pkg: PPackage,
+    deps: Map[AbstractImport, ExternalTypeInfo],
+  ): PPackage = {
+    import viper.gobra.ast.frontend.PExplicitQualifiedImport
+
+    // Local predicate names (function and method): used to skip work for cases the parse-time
+    // postprocessor already handled.
+    val localPredicateNames: Set[String] = pkg.programs.flatMap(_.declarations.collect {
+      case d: viper.gobra.ast.frontend.PFPredicateDecl => d.id.name
+      case d: viper.gobra.ast.frontend.PMPredicateDecl => d.id.name
+    }).toSet
+
+    // Build a per-program function: qualifier-name -> set of predicate names exposed by the
+    // package imported under that qualifier.
+    val importedByQualifier: Map[String, Set[String]] = pkg.programs.flatMap { prog =>
+      prog.imports.collect {
+        case pi: PExplicitQualifiedImport =>
+          val abstractImport = RegularImport(pi.importPath)
+          deps.get(abstractImport).map { extInfo =>
+            // walk the imported package's declarations and collect top-level predicate names
+            val importedPkg = extInfo.getTypeInfo match {
+              case ti: TypeInfoImpl => Some(ti.tree.root)
+              case _ => None
+            }
+            val names: Set[String] = importedPkg.toVector.flatMap(_.programs.flatMap(_.declarations.collect {
+              case d: viper.gobra.ast.frontend.PFPredicateDecl => d.id.name
+              case d: viper.gobra.ast.frontend.PMPredicateDecl => d.id.name
+            })).toSet
+            pi.qualifier.name -> names
+          }
+      }.flatten
+    }.toMap
+
+    if (importedByQualifier.isEmpty) pkg
+    else {
+      val positions = pkg.positions.positions
+      viper.gobra.frontend.Parser.PredicateConstructorRewriter.rewrite(
+        pkg,
+        localPredicateNames,
+        q => importedByQualifier.getOrElse(q, Set.empty),
+      )(positions)
+    }
+  }
+
   type TypeInfoCacheKey = String
   private val typeInfoCache: ConcurrentMap[TypeInfoCacheKey, TypeInfoImpl] = new ConcurrentHashMap()
 
@@ -255,7 +309,11 @@ object Info extends LazyLogging {
     var cacheHit: Boolean = true
     def getTypeInfo(pkg: PPackage, dependentTypeInfo: Map[AbstractImport, ExternalTypeInfo], isMainContext: Boolean, config: Config): TypeInfoImpl = {
       cacheHit = false
-      val tree = new GoTree(pkg)
+      // Rewrite any remaining `pkg.P{...}` composite literals into predicate constructors when
+      // `P` is a top-level predicate of the imported package. This finishes the disambiguation
+      // started at parse time (see Parser.PredicateConstructorPostprocessor).
+      val rewrittenPkg = rewriteCrossPackagePredConstructors(pkg, dependentTypeInfo)
+      val tree = new GoTree(rewrittenPkg)
       new TypeInfoImpl(tree, dependentTypeInfo, isMainContext)(config: Config)
     }
 

src/test/resources/regressions/examples/evaluation/impl_errors/parallel_search_replace.gobra

@@ -27,20 +27,20 @@ pred replacedPerm(ghost s0 seq[int], ghost s [] int, ghost x, y int) {
 
 pred messagePerm(ghost wg *sync.WaitGroup, s []int, ghost x, y int) {
   (forall i int :: 0 <= i && i < len(s) ==> acc(&s[i])) &&
-  wg.UnitDebt(replacedPerm!<toSeq(s),s,x,y!>)
+  wg.UnitDebt(replacedPerm{toSeq(s),s,x,y})
 }
 
 requires acc(c.RecvChannel(),_)
-requires c.RecvGivenPerm() == PredTrue!<!>
-requires c.RecvGotPerm() == messagePerm!<wg,_,x,y!>
+requires c.RecvGivenPerm() == PredTrue{}
+requires c.RecvGotPerm() == messagePerm{wg,_,x,y}
 func worker(c <- chan[]int, wg *sync.WaitGroup, x, y int) {
-  fold acc(PredTrue!<!>(),2/1);
-  invariant PredTrue!<!>() && acc(c.RecvChannel(),_)
-  invariant c.RecvGivenPerm() == PredTrue!<!>
-  invariant c.RecvGotPerm() == messagePerm!<wg,_,x,y,!>
-  invariant ok ==> messagePerm!<wg,_,x,y!>(s)
+  fold acc(PredTrue{}(),2/1);
+  invariant PredTrue{}() && acc(c.RecvChannel(),_)
+  invariant c.RecvGivenPerm() == PredTrue{}
+  invariant c.RecvGotPerm() == messagePerm{wg,_,x,y,}
+  invariant ok ==> messagePerm{wg,_,x,y}(s)
   for s, ok := <- c; ok; s, ok = <-c {
-    unfold messagePerm!<wg,_,x,y!>(s)
+    unfold messagePerm{wg,_,x,y}(s)
     ghost s0 := toSeq(s)
     invariant 0 <= i && i <= len(s)
     invariant forall j int :: 0 <= j && j < len(s) ==> acc(&s[j])
@@ -51,10 +51,10 @@ func worker(c <- chan[]int, wg *sync.WaitGroup, x, y int) {
       // we forget to perform the worker's task (seeded bug):
       // if(s[i] == x) { s[i] = y }
     }
-    fold replacedPerm!<s0,s,x,y!>()
-    wg.PayDebt(replacedPerm!<s0,s,x,y!>)
+    fold replacedPerm{s0,s,x,y}()
+    wg.PayDebt(replacedPerm{s0,s,x,y})
     wg.Done()
-    fold PredTrue!<!>()
+    fold PredTrue{}()
   }
 }
 
@@ -73,13 +73,13 @@ func SearchReplace(s []int, x, y int) {
   ghost s0 := toSeq(s)
   c := make(chan []int,4)
   var wg@ sync.WaitGroup
-  ghost pr := messagePerm!<&wg,_,x,y!>
-  c.Init(pr,PredTrue!<!>)
+  ghost pr := messagePerm{&wg,_,x,y}
+  c.Init(pr,PredTrue{})
   wg.Init()
   ghost seqs := seq[seq[int]] {}
   ghost pseqs := seq[pred()] {}
   invariant acc(c.RecvChannel(),_)
-  invariant c.RecvGivenPerm() == PredTrue!<!> && c.RecvGotPerm() == pr
+  invariant c.RecvGivenPerm() == PredTrue{} && c.RecvGotPerm() == pr
   for i := 0; i != workers; i++ {
     go worker(c,&wg,x,y)
   }
@@ -98,7 +98,7 @@ func SearchReplace(s []int, x, y int) {
     0 <= j && j < len(seqs[i]) ==> seqs[i][j] == s0[i * workRange + j]
   invariant len(pseqs) == len(seqs)
   invariant forall i int :: {pseqs[i]} 0 <= i && i < len(pseqs) ==>
-    pseqs[i] == replacedPerm!<seqs[i],s[i * workRange:i * workRange + len(seqs[i])],x,y!>
+    pseqs[i] == replacedPerm{seqs[i],s[i * workRange:i * workRange + len(seqs[i])],x,y}
   invariant forall i int :: 0 <= i && i < len(pseqs) ==> wg.TokenById(pseqs[i],i)
   for offset := 0; offset != len(s); {
     nextOffset := offset + workRange;
@@ -109,16 +109,16 @@ func SearchReplace(s []int, x, y int) {
     assert forall i int :: {&section[i]} 0 <= i && i < len(s) ==>
       &section[i] == &s[i + offset]
     ghost s1 := toSeq(section)
-    ghost wpr := replacedPerm!<s1,section,x,y!>
-    wg.Add(1,1/2,PredTrue!<!>)
+    ghost wpr := replacedPerm{s1,section,x,y}
+    wg.Add(1,1/2,PredTrue{})
     ghost if(offset == 0) {
-      wg.Start(1/2,PredTrue!<!>)
+      wg.Start(1/2,PredTrue{})
     }
     wg.GenerateTokenAndDebt(wpr)
     fold wg.TokenById(wpr,len(pseqs))
     seqs = seqs ++ seq[seq[int]]{ s1 }
     pseqs = pseqs ++ seq[pred()] { wpr }
-    fold messagePerm!<&wg,_,x,y!>(section)
+    fold messagePerm{&wg,_,x,y}(section)
     c <- section
     offset = nextOffset
   }
@@ -137,7 +137,7 @@ func SearchReplace(s []int, x, y int) {
       down := i * workRange
       up := down + len(seqs[i])
       s1 := s[down:up]
-      unfold replacedPerm!<seqs[i],s1,x,y!>()
+      unfold replacedPerm{seqs[i],s1,x,y}()
       assert forall j int :: {&s[j]} down <= j && j < up ==> &s[j] == &s1[j-down]
     }
   }