From c92fee274825307c90d676c65f806f99eaae547d Mon Sep 17 00:00:00 2001 From: Sidonie Bouthors <92856411+SidonieBouthors@users.noreply.github.com> Date: Fri, 10 Jan 2025 14:48:49 +0100 Subject: [PATCH] Add support for pattern alternatives (#1627) Addresses issues #1128 and #617 by adding support for pattern alternatives in Stainless. This was done in the context of our project in the Formal Verification CS-550 course. This version adds a new Alternative pattern and handles it throughout the pipeline and therefore allows disjunctions of patterns to be used. Note: This does not yet add support for pattern alternatives in the Coq encoder or GenC, but does include support for pattern alternatives when using the optional simplifiers OL and OCBSL. --------- Co-authored-by: Mai-LinhC --- .../scala/stainless/ast/Deconstructors.scala | 4 +++ .../main/scala/stainless/ast/ExprOps.scala | 8 +++++ .../scala/stainless/ast/Expressions.scala | 7 ++++ .../main/scala/stainless/ast/Printers.scala | 4 +++ .../main/scala/stainless/ast/SymbolOps.scala | 6 ++++ .../main/scala/stainless/ast/TypeOps.scala | 4 +++ .../evaluators/RecursiveEvaluator.scala | 6 ++++ .../extraction/oo/TransformerWithType.scala | 4 +++ .../extraction/oo/TypeEncoding.scala | 10 ++++++ .../stainless/extraction/oo/TypeOps.scala | 1 + .../stainless/genc/phases/Scala2IRPhase.scala | 3 ++ .../transformers/lattices/Core.scala | 19 +++++++++++ .../transformers/lattices/Definitions.scala | 2 ++ .../scala/stainless/utils/Serialization.scala | 5 +-- .../stainless/verification/CoqEncoder.scala | 2 ++ .../valid/PatternAlternative1 copy.scala | 20 +++++++++++ .../valid/PatternAlternative2.scala | 33 +++++++++++++++++++ .../valid/PatternAlternative.scala | 33 +++++++++++++++++++ .../frontends/dotc/CodeExtraction.scala | 5 +++ 19 files changed, 174 insertions(+), 2 deletions(-) create mode 100644 frontends/benchmarks/extraction/valid/PatternAlternative1 copy.scala create mode 100644 frontends/benchmarks/extraction/valid/PatternAlternative2.scala create mode 100644 frontends/benchmarks/verification/valid/PatternAlternative.scala diff --git a/core/src/main/scala/stainless/ast/Deconstructors.scala b/core/src/main/scala/stainless/ast/Deconstructors.scala index 7d745656a2..b236358197 100644 --- a/core/src/main/scala/stainless/ast/Deconstructors.scala +++ b/core/src/main/scala/stainless/ast/Deconstructors.scala @@ -34,6 +34,10 @@ trait TreeDeconstructor extends inox.ast.TreeDeconstructor { (Seq(id), binder.map(_.toVariable).toSeq, recs, tps, subs, (ids, vs, es, tps, pats) => { t.UnapplyPattern(vs.headOption.map(_.toVal), es, ids.head, tps, pats) }) + case s.AlternativePattern(binder, subs) => + (Seq(), binder.map(_.toVariable).toSeq, Seq(), Seq(), subs, (_, vs, _, _, pats) => { + t.AlternativePattern(vs.headOption.map(_.toVal), pats) + }) } /** Rebuild a match case from the given set of identifiers, variables, expressions and types */ diff --git a/core/src/main/scala/stainless/ast/ExprOps.scala b/core/src/main/scala/stainless/ast/ExprOps.scala index c24fd7a14f..815d64d7ba 100644 --- a/core/src/main/scala/stainless/ast/ExprOps.scala +++ b/core/src/main/scala/stainless/ast/ExprOps.scala @@ -458,6 +458,14 @@ class ExprOps(override val trees: Trees) extends inox.ast.ExprOps(trees) { self (_ ++ _) ) + case AlternativePattern(vdOpt, subPatterns) => + val freshVdOpt = vdOpt.map(vd => transform(vd.freshen, env)) + // We don't need to freshen the subPatterns here, as they are not bound + ( + AlternativePattern(freshVdOpt, subPatterns), + env ++ freshVdOpt.map(freshVd => vdOpt.get.id -> freshVd.id) + ) + case LiteralPattern(vdOpt, lit) => val freshVdOpt = vdOpt.map(vd => transform(vd.freshen, env)) val newEnv = env ++ freshVdOpt.map(freshVd => vdOpt.get.id -> freshVd.id) diff --git a/core/src/main/scala/stainless/ast/Expressions.scala b/core/src/main/scala/stainless/ast/Expressions.scala index 4a181610a7..8de472ffd8 100644 --- a/core/src/main/scala/stainless/ast/Expressions.scala +++ b/core/src/main/scala/stainless/ast/Expressions.scala @@ -157,6 +157,13 @@ trait Expressions extends inox.ast.Expressions with Types { self: Trees => val subPatterns = Seq() } + /** + * Pattern encoding like `case binder @ (subPattern1 | subPattern2 | ...) => ...` + * + * If [[binder]] is empty, consider a wildcard `_` in its place. + */ + sealed case class AlternativePattern(binder: Option[ValDef], subPatterns: Seq[Pattern]) extends Pattern + protected def unapplyScrut(scrut: Expr, up: UnapplyPattern)(using s: Symbols): Expr = { FunctionInvocation(up.id, up.tps, up.recs :+ scrut) } diff --git a/core/src/main/scala/stainless/ast/Printers.scala b/core/src/main/scala/stainless/ast/Printers.scala index 6760c887a1..ec4d7a1102 100644 --- a/core/src/main/scala/stainless/ast/Printers.scala +++ b/core/src/main/scala/stainless/ast/Printers.scala @@ -110,6 +110,10 @@ trait Printer extends inox.ast.Printer { printNameWithPath(id) p"(${nary(subs)})" + case AlternativePattern(ovd, subs) => + ovd foreach (vd => p"${vd.toVariable} : ") + p"(${nary(subs, " | ")})" + case Passes(in, out, cases) => optP { p"""|($in, $out) passes { diff --git a/core/src/main/scala/stainless/ast/SymbolOps.scala b/core/src/main/scala/stainless/ast/SymbolOps.scala index a675492a78..d3b0e35d19 100644 --- a/core/src/main/scala/stainless/ast/SymbolOps.scala +++ b/core/src/main/scala/stainless/ast/SymbolOps.scala @@ -88,6 +88,12 @@ trait SymbolOps extends inox.ast.SymbolOps with TypeOps { self => val subTests = subps.zipWithIndex.map { case (p, i) => apply(tupleSelect(in, i+1, subps.size), p) } bind(ob, in) `merge` subTests + case AlternativePattern(ob, subps) => + // one of the alternatives must hold (disjunction) + // we use A \/ B = ~ (~A /\ ~B) + val disjunction = subps.map(p => apply(in, p).negate).reduce(_ `merge` _).negate + bind(ob, in) `merge` disjunction + case up @ UnapplyPattern(ob, _, _, _, subps) => val subs = unwrapTuple(up.get(in), subps.size).zip(subps) map (apply).tupled bind(ob, in) `withCond` Not(up.isEmpty(in)) `merge` subs diff --git a/core/src/main/scala/stainless/ast/TypeOps.scala b/core/src/main/scala/stainless/ast/TypeOps.scala index bdc8b57ee3..bcdabb0bfb 100644 --- a/core/src/main/scala/stainless/ast/TypeOps.scala +++ b/core/src/main/scala/stainless/ast/TypeOps.scala @@ -47,6 +47,10 @@ trait TypeOps extends inox.ast.TypeOps { case _ => false } + case AlternativePattern(ob, subs) => + ob.forall(vd => isSubtypeOf(vd.getType, in)) && + (subs exists (patternIsTyped(in, _))) + case up @ UnapplyPattern(ob, recs, id, tps, subs) => ob.forall(vd => isSubtypeOf(vd.getType, in)) && lookupFunction(id).exists(_.tparams.size == tps.size) && { diff --git a/core/src/main/scala/stainless/evaluators/RecursiveEvaluator.scala b/core/src/main/scala/stainless/evaluators/RecursiveEvaluator.scala index 0ea03ac214..8241bef767 100644 --- a/core/src/main/scala/stainless/evaluators/RecursiveEvaluator.scala +++ b/core/src/main/scala/stainless/evaluators/RecursiveEvaluator.scala @@ -137,6 +137,12 @@ abstract class RecursiveEvaluator(override val program: Program, None } + case (AlternativePattern(ob, subs), scrut) => + subs.map(matchesPattern(_, scrut)).find(_.isDefined) match { + case Some(_) => Some(obind(ob, expr)) // There should be no mapping nested in the alternative + case _ => None + } + case (up @ UnapplyPattern(ob, rec, id, tps, subs), scrut) => val eRec = rec map e val unapp = e(FunctionInvocation(id, tps, eRec :+ scrut)) diff --git a/core/src/main/scala/stainless/extraction/oo/TransformerWithType.scala b/core/src/main/scala/stainless/extraction/oo/TransformerWithType.scala index a7ad42a472..9eed5b147e 100644 --- a/core/src/main/scala/stainless/extraction/oo/TransformerWithType.scala +++ b/core/src/main/scala/stainless/extraction/oo/TransformerWithType.scala @@ -45,6 +45,10 @@ trait TransformerWithType extends TreeTransformer { val rsubs = (subs zip tps).map(p => transform(p._1, p._2)) t.TuplePattern(ob map transform, rsubs).copiedFrom(pat) + case s.AlternativePattern(ob, subs) => + val rsubs = subs map (transform(_, tpe)) + t.AlternativePattern(ob map transform, rsubs).copiedFrom(pat) + case up @ s.UnapplyPattern(ob, recs, id, tps, subs) => val rsubs = (subs zip up.subTypes(tpe)).map(p => transform(p._1, p._2)) val rrecs = (recs zip getFunction(id, tps).params.init).map(p => transform(p._1, p._2.getType)) diff --git a/core/src/main/scala/stainless/extraction/oo/TypeEncoding.scala b/core/src/main/scala/stainless/extraction/oo/TypeEncoding.scala index fc260e68ab..9450a425bf 100644 --- a/core/src/main/scala/stainless/extraction/oo/TypeEncoding.scala +++ b/core/src/main/scala/stainless/extraction/oo/TypeEncoding.scala @@ -920,6 +920,12 @@ class TypeEncoding(override val s: Trees, override val t: Trees) case s.TuplePattern(Some(vd), _) => instanceOfPattern(super.transform(pat, vd.tpe), tpe, vd.tpe) + case s.AlternativePattern(None, subs) => + t.AlternativePattern(None, subs.map(transform)).copiedFrom(pat) + + case s.AlternativePattern(Some(vd), subs) => + instanceOfPattern(t.AlternativePattern(Some(transform(vd)), subs.map(transform)).copiedFrom(pat), tpe, vd.tpe) + case up @ s.UnapplyPattern(ob, recs, id, tps, subs) => val funScope = this `in` id val FunInfo(fun, tparams) = functions(id) @@ -1028,6 +1034,10 @@ class TypeEncoding(override val s: Trees, override val t: Trees) super.transform(pat, in) } + case s.AlternativePattern(ob, subs) => + simple --= s.typeOps.typeParamsOf(in.getType) + super.transform(pat, in) + case up @ s.UnapplyPattern(ob, recs, id, tps, subs) => val tparams = infos(id).tparams simple --= tps.zipWithIndex.flatMap { case (tp, i) => diff --git a/core/src/main/scala/stainless/extraction/oo/TypeOps.scala b/core/src/main/scala/stainless/extraction/oo/TypeOps.scala index e1795c8d5e..f271cb9426 100644 --- a/core/src/main/scala/stainless/extraction/oo/TypeOps.scala +++ b/core/src/main/scala/stainless/extraction/oo/TypeOps.scala @@ -244,6 +244,7 @@ trait TypeOps extends innerfuns.TypeOps { self => .map(cons => ADTType(cons.sort, tps)) .getOrElse(Untyped) case TuplePattern(_, subs) => TupleType(subs map patternInType) + case AlternativePattern(_, subs) => leastUpperBound(subs map patternInType) case ClassPattern(_, ct, subs) => ct case UnapplyPattern(_, recs, id, tps, _) => lookupFunction(id) diff --git a/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala b/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala index 6256b8fb09..e9b644ca1d 100644 --- a/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala +++ b/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala @@ -465,6 +465,9 @@ private class S2IRImpl(override val s: tt.type, update(b, scrutinee) buildBinOp(scrutinee, O.Equals, lit)(pat.getPos) + case AlternativePattern(_, _) => + reporter.fatalError(pat.getPos, s"Alternative Pattern, a.k.a pattern disjunction, is not yet supported by GenC") + case UnapplyPattern(_, _, _, _, _) => reporter.fatalError(pat.getPos, s"Unapply Pattern, a.k.a. Extractor Objects, is not supported by GenC") } diff --git a/core/src/main/scala/stainless/transformers/lattices/Core.scala b/core/src/main/scala/stainless/transformers/lattices/Core.scala index 6c7453cbfc..803f3d7d29 100644 --- a/core/src/main/scala/stainless/transformers/lattices/Core.scala +++ b/core/src/main/scala/stainless/transformers/lattices/Core.scala @@ -938,6 +938,13 @@ trait Core extends Definitions { ocbsl => val subScruts = tupleSubscrutinees(scrut, tt) val (rsubs, subst2) = recHelper(subScruts, subps) (LabelledPattern.TuplePattern(rsubs), subst2) + case AlternativePattern(_, subps) => + val (rsubs, subst2) = subps.foldLeft((Seq.empty[LabelledPattern], subst1)) { + case ((acc, subst), subp) => + val (rsub, subst2) = convertPattern(scrut, subp, subst) + (acc :+ rsub, subst2) + } + (LabelledPattern.Alternative(rsubs), subst2) case UnapplyPattern(_, recs, id, tps, subps) => if (recs.nonEmpty) throw UnsupportedOperationException("recs is not empty") val unapp = unapplySubScrutinees(scrut, id, tps) @@ -2644,6 +2651,7 @@ trait Core extends Definitions { ocbsl => assert(bases.size == subps.size) val rsubs = recHelper(tupleSubscrutinees(scrut, tt), subps) TuplePattern(bdg, rsubs) + case LabelledPattern.Alternative(subs) => AlternativePattern(bdg, subs.map(sub => convertPattern(scrut, sub, vds))) case LabelledPattern.Lit(lit) => LiteralPattern(bdg, lit) case LabelledPattern.Unapply(recs, id, tps, subps) => assert(recs.isEmpty) @@ -3286,6 +3294,17 @@ trait Core extends Definitions { ocbsl => assert(ctxs.isPrefixOf(newCtxs)) PatBdgsAndConds(newCtxs, subscruts ++ recBdgs, recPatConds) + case LabelledPattern.Alternative(sub) => + val PatBdgsAndConds(newCtxs, _, subPatConds) = + sub.foldLeft(PatBdgsAndConds(ctxs, Seq.empty, Seq.empty)) { + case (PatBdgsAndConds(ctxs, _, condsAcc), subpat) => + val PatBdgsAndConds(ctxs2, _, conds2) = addPatternBindingsAndConds(ctxs, scrut, subpat) + PatBdgsAndConds(ctxs2, Seq.empty, condsAcc ++ conds2) + } + val cond = codeOfSig(mkOr(subPatConds), BoolTy) + assert(ctxs.isPrefixOf(newCtxs)) + PatBdgsAndConds(newCtxs.withCond(cond), Seq.empty, Seq(cond)) + case LabelledPattern.Unapply(recs, id, tps, subps) => assert(recs.isEmpty) val unapp = unapplySubScrutinees(scrut, id, tps) diff --git a/core/src/main/scala/stainless/transformers/lattices/Definitions.scala b/core/src/main/scala/stainless/transformers/lattices/Definitions.scala index e15d190ef6..666ad00947 100644 --- a/core/src/main/scala/stainless/transformers/lattices/Definitions.scala +++ b/core/src/main/scala/stainless/transformers/lattices/Definitions.scala @@ -223,6 +223,7 @@ trait Definitions { case Wildcard extends LabelledPattern case ADT(id: Identifier, tps: Seq[Type], sub: Seq[LabelledPattern]) extends LabelledPattern case TuplePattern(sub: Seq[LabelledPattern]) extends LabelledPattern + case Alternative(sub: Seq[LabelledPattern]) extends LabelledPattern case Lit[T](lit: Literal[T]) extends LabelledPattern case Unapply(recs: Seq[Code], id: Identifier, tps: Seq[Type], sub: Seq[LabelledPattern]) extends LabelledPattern @@ -231,6 +232,7 @@ trait Definitions { case Wildcard => Seq.empty case ADT(_, _, sub) => sub.flatMap(_.allPatterns) case TuplePattern(sub) => sub.flatMap(_.allPatterns) + case Alternative(sub) => sub.flatMap(_.allPatterns) case Lit(_) => Seq.empty case Unapply(_, _, _, sub) => sub.flatMap(_.allPatterns) }) diff --git a/core/src/main/scala/stainless/utils/Serialization.scala b/core/src/main/scala/stainless/utils/Serialization.scala index 24bd8fa0e1..cfbf57df96 100644 --- a/core/src/main/scala/stainless/utils/Serialization.scala +++ b/core/src/main/scala/stainless/utils/Serialization.scala @@ -21,9 +21,9 @@ class StainlessSerializer(override val trees: ast.Trees, serializeProducts: Bool /** An extension to the set of registered classes in the `InoxSerializer`. * occur within Stainless programs. * - * The new identifiers in the mapping range from 120 to 172. + * The new identifiers in the mapping range from 120 to 173. * - * NEXT ID: 173 + * NEXT ID: 174 */ override protected def classSerializers: Map[Class[?], Serializer[?]] = super.classSerializers ++ Map( @@ -40,6 +40,7 @@ class StainlessSerializer(override val trees: ast.Trees, serializeProducts: Bool stainlessClassSerializer[TuplePattern] (130), stainlessClassSerializer[LiteralPattern[Any]](131), stainlessClassSerializer[UnapplyPattern] (132), + stainlessClassSerializer[AlternativePattern] (173), stainlessClassSerializer[FiniteArray] (133), stainlessClassSerializer[LargeArray] (134), stainlessClassSerializer[ArraySelect] (135), diff --git a/core/src/main/scala/stainless/verification/CoqEncoder.scala b/core/src/main/scala/stainless/verification/CoqEncoder.scala index 972391b4ee..04997599be 100644 --- a/core/src/main/scala/stainless/verification/CoqEncoder.scala +++ b/core/src/main/scala/stainless/verification/CoqEncoder.scala @@ -225,6 +225,8 @@ trait CoqEncoder { ctx.reporter.warning(s"Ignoring type $tpe in the wildcard pattern $p.") //TODO not tested CoqTuplePatternVd(ps.map(transformPattern), VariablePattern(Some(makeFresh(id)))) + case AlternativePattern(_, _) => + ctx.reporter.fatalError(s"The translation to Coq does not support disjunctive patterns such as `$p` (${p.getClass}) yet.") case _ => ctx.reporter.fatalError(s"Coq does not support patterns such as `$p` (${p.getClass}) yet.") } diff --git a/frontends/benchmarks/extraction/valid/PatternAlternative1 copy.scala b/frontends/benchmarks/extraction/valid/PatternAlternative1 copy.scala new file mode 100644 index 0000000000..2a13c9fb0d --- /dev/null +++ b/frontends/benchmarks/extraction/valid/PatternAlternative1 copy.scala @@ -0,0 +1,20 @@ +object PatternAlternative1 { + sealed trait SignSet + case object None extends SignSet + case object Any extends SignSet + case object Neg extends SignSet + case object Zer extends SignSet + case object Pos extends SignSet + case object NegZer extends SignSet + case object NotZer extends SignSet + case object PosZer extends SignSet + + def subsetOf(a: SignSet, b: SignSet): Boolean = (a, b) match { + case (None, _) => true + case (_, Any) => true + case (Neg, NegZer | NotZer) => true + case (Zer, NegZer | PosZer) => true + case (Pos, NotZer | PosZer) => true + case _ => false + } +} \ No newline at end of file diff --git a/frontends/benchmarks/extraction/valid/PatternAlternative2.scala b/frontends/benchmarks/extraction/valid/PatternAlternative2.scala new file mode 100644 index 0000000000..acdf27809c --- /dev/null +++ b/frontends/benchmarks/extraction/valid/PatternAlternative2.scala @@ -0,0 +1,33 @@ +object PatternAlternative2 { + sealed trait Tree + case class Node(left: Tree, right: Tree) extends Tree + case class IntLeaf(value: Int) extends Tree + case class StringLeaf(value: String) extends Tree + case class NoneLeaf() extends Tree + + def containsNoneLeaf(tree: Tree): Boolean = { + tree match { + case Node(left, right) => containsNoneLeaf(left) || containsNoneLeaf(right) + case NoneLeaf() => true + case _ => false + } + } + + def containsOnlyBinaryLeaves(tree: Tree): Boolean = { + tree match { + case Node(left, right) => containsOnlyBinaryLeaves(left) && containsOnlyBinaryLeaves(right) + case IntLeaf(v) => v == 0 || v == 1 + case StringLeaf(v) => v == "0" || v == "1" + case _ => true + } + } + + def hasBinaryLeaves(tree: Tree): Boolean = { + require(!containsNoneLeaf(tree) && containsOnlyBinaryLeaves(tree)) + tree match { + case a @ Node(left: (IntLeaf | StringLeaf), right: (IntLeaf | StringLeaf)) => hasBinaryLeaves(left) && hasBinaryLeaves(right) + case b @ (IntLeaf(0 | 1) | StringLeaf("0" | "1")) => true + case _ => false + } + } ensuring { res => res } +} \ No newline at end of file diff --git a/frontends/benchmarks/verification/valid/PatternAlternative.scala b/frontends/benchmarks/verification/valid/PatternAlternative.scala new file mode 100644 index 0000000000..7be5703557 --- /dev/null +++ b/frontends/benchmarks/verification/valid/PatternAlternative.scala @@ -0,0 +1,33 @@ +object PatternAlternative { + sealed trait Tree + case class Node(left: Tree, right: Tree) extends Tree + case class IntLeaf(value: Int) extends Tree + case class StringLeaf(value: String) extends Tree + case class NoneLeaf() extends Tree + + def containsNoneLeaf(tree: Tree): Boolean = { + tree match { + case Node(left, right) => containsNoneLeaf(left) || containsNoneLeaf(right) + case NoneLeaf() => true + case _ => false + } + } + + def containsOnlyBinaryLeaves(tree: Tree): Boolean = { + tree match { + case Node(left, right) => containsOnlyBinaryLeaves(left) && containsOnlyBinaryLeaves(right) + case IntLeaf(v) => v == 0 || v == 1 + case StringLeaf(v) => v == "0" || v == "1" + case _ => true + } + } + + def hasBinaryLeaves(tree: Tree): Boolean = { + require(!containsNoneLeaf(tree) && containsOnlyBinaryLeaves(tree)) + tree match { + case a @ Node(left: (IntLeaf | StringLeaf), right: (IntLeaf | StringLeaf)) => hasBinaryLeaves(left) && hasBinaryLeaves(right) + case b @ (IntLeaf(0 | 1) | StringLeaf("0" | "1")) => true + case _ => false + } + } ensuring { res => res } +} \ No newline at end of file diff --git a/frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala b/frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala index 0553d3d7a0..a2922e422e 100644 --- a/frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala +++ b/frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala @@ -917,6 +917,11 @@ class CodeExtraction(inoxCtx: inox.Context, // Note that this pattern will be correctly rejected as "Unsupported pattern" (in fact, it cannot be even tested at runtime): // val (aa: B, bb: B) = (a, b) private def extractPattern(p: tpd.Tree, expectedTpe: Option[xt.Type], binder: Option[xt.ValDef] = None)(using dctx: DefContext): (xt.Pattern, DefContext) = p match { + + case a @ Alternative(subpatterns) => + val (patterns, nctx) = subpatterns.map(extractPattern(_, expectedTpe)).unzip + (xt.AlternativePattern(binder, patterns), dctx) + case b @ Bind(name, t @ Typed(pat, tpt)) => val vd = xt.ValDef(FreshIdentifier(name.toString), extractType(tpt), annotationsOf(b.symbol, ignoreOwner = true)).setPos(b.sourcePos) val pctx = dctx.withNewVar(b.symbol -> (() => vd.toVariable))