Skip to content

Commit

Permalink
Merge pull request utwente-fmt#1218 from utwente-fmt/perf
Browse files Browse the repository at this point in the history
Performance improvements
  • Loading branch information
pieter-bos authored Jun 26, 2024
2 parents 523623e + 65b0c6e commit 99d9cc5
Show file tree
Hide file tree
Showing 16 changed files with 119 additions and 43 deletions.
12 changes: 3 additions & 9 deletions src/col/vct/col/ast/type/typeclass/TypeImpl.scala
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ import vct.col.rewrite.NonLatchingRewriter
import vct.col.typerules.CoercionUtils
import vct.col.print._
import vct.col.ast.ops.TypeFamilyOps
import vct.col.util.IdentitySuccessorsProvider

trait TypeImpl[G] extends TypeFamilyOps[G] {
this: Type[G] =>
Expand Down Expand Up @@ -53,15 +54,8 @@ trait TypeImpl[G] extends TypeFamilyOps[G] {

def particularize(substitutions: Map[Variable[G], Type[G]]): Type[G] = {
case object Particularize extends NonLatchingRewriter[G, G] {
case object IdentitySuccessorsProvider
extends SuccessorsProviderTrafo[G, G](allScopes.freeze) {
override def preTransform[I <: Declaration[G], O <: Declaration[G]](
pre: I
): Option[O] = Some(pre.asInstanceOf[O])
}

override def succProvider: SuccessorsProvider[G, G] =
IdentitySuccessorsProvider
override val succProvider: SuccessorsProvider[G, G] =
new IdentitySuccessorsProvider

override def dispatch(t: Type[G]): Type[G] =
t match {
Expand Down
13 changes: 13 additions & 0 deletions src/col/vct/col/rewrite/SuccessorProviderChain.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
package vct.col.rewrite

import vct.col.ast.Declaration

class SuccessorProviderChain[A, B, C, AD <: Declaration[A], BD <: Declaration[
B
], CD <: Declaration[C]](
left: SuccessorProvider[A, B, AD, BD],
right: SuccessorProvider[B, C, BD, CD],
) extends SuccessorProvider[A, C, AD, CD] {
override def computeSucc(decl: AD): Option[CD] =
left.computeSucc(decl).flatMap(right.computeSucc)
}
10 changes: 10 additions & 0 deletions src/col/vct/col/rewrite/SuccessorProviderNothing.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
package vct.col.rewrite

import vct.col.ast.Declaration

class SuccessorProviderNothing[Pre, Post, PreDecl <: Declaration[
Pre
], PostDecl <: Declaration[Post]](crash: => Nothing)
extends SuccessorProvider[Pre, Post, PreDecl, PostDecl] {
override def computeSucc(decl: PreDecl): Nothing = crash
}
17 changes: 17 additions & 0 deletions src/col/vct/col/rewrite/SuccessorProviderTrafo.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
package vct.col.rewrite

import vct.col.ast.Declaration

class SuccessorProviderTrafo[Pre, Post, PreDecl <: Declaration[
Pre
], PostDecl <: Declaration[Post]](
inner: SuccessorProvider[Pre, Post, PreDecl, PostDecl]
) extends SuccessorProvider[Pre, Post, PreDecl, PostDecl] {
def preTransform[I <: PreDecl, O <: PostDecl](pre: I): Option[O] = None
def postTransform[T <: PostDecl](pre: PreDecl, post: Option[T]): Option[T] =
post

override def computeSucc(decl: PreDecl): Option[PostDecl] =
preTransform(decl).orElse(postTransform(decl, inner.computeSucc(decl)))

}
6 changes: 4 additions & 2 deletions src/col/vct/col/typerules/CoercingRewriter.scala
Original file line number Diff line number Diff line change
Expand Up @@ -58,14 +58,16 @@ abstract class CoercingRewriter[Pre <: Generation]()
SuccessionMap()

class CoercedSuccessorsProvider
extends SuccessorsProviderTrafo[Pre, Pre](null) {
extends SuccessorsProviderTrafo[Pre, Pre](new SuccessorsProviderNothing(
throw Unreachable("Always preTransformed")
)) {
override def preTransform[I <: Declaration[Pre], O <: Declaration[Pre]](
pre: I
): Option[O] = Some(coercedDeclaration(pre).asInstanceOf[O])
}

override def succProvider: SuccessorsProvider[Pre, Post] =
SuccessorsProviderChain(new CoercedSuccessorsProvider, allScopes.freeze)
SuccessorsProviderChain(new CoercedSuccessorsProvider, allScopes)

/** Apply a particular coercion to an expression. SAFETY: all promoting
* coercions must be injective; otherwise the default mapping coercion of
Expand Down
17 changes: 17 additions & 0 deletions src/col/vct/col/util/IdentitySuccessorsProvider.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
package vct.col.util

import vct.col.ast.{
Declaration,
SuccessorsProviderNothing,
SuccessorsProviderTrafo,
}
import vct.result.VerificationError.Unreachable

class IdentitySuccessorsProvider[G]
extends SuccessorsProviderTrafo[G, G](new SuccessorsProviderNothing(
throw Unreachable("Always preTransformed")
)) {
override def preTransform[I <: Declaration[G], O <: Declaration[G]](
pre: I
): Option[O] = Some(pre.asInstanceOf[O])
}
3 changes: 1 addition & 2 deletions src/col/vct/col/util/Substitute.scala
Original file line number Diff line number Diff line change
Expand Up @@ -14,8 +14,7 @@ case class Substitute[G](
originTrafo: Origin => Origin = identity,
) extends NonLatchingRewriter[G, G] {

case class SuccOrIdentity()
extends SuccessorsProviderTrafo[G, G](allScopes.freeze) {
case class SuccOrIdentity() extends SuccessorsProviderTrafo[G, G](allScopes) {
override def postTransform[T <: Declaration[G]](
pre: Declaration[G],
post: Option[T],
Expand Down
5 changes: 5 additions & 0 deletions src/helpers/vct/col/ast/helpers/defn/Constants.scala
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ import vct.col.ast.structure.Constants.{DeclarationName, RootNodeName}
import scala.meta._

object Constants {
val NothingType: Type = t"_root_.scala.Nothing"
val SeqType: Type = t"_root_.scala.Seq"
val SeqObj: Term = q"_root_.scala.Seq"
val Unit: Type = t"_root_.scala.Unit"
Expand Down Expand Up @@ -47,6 +48,10 @@ object Constants {
q"_root_.vct.col.err.InconsistentSuccessionTypes"
val RefType: Type = t"_root_.vct.col.ref.Ref"
val LazyRef: Type = t"_root_.vct.col.ref.LazyRef"
val SuccessorProvider: Type = t"_root_.vct.col.rewrite.SuccessorProvider"
val SuccessorProviderChain: Type = t"_root_.vct.col.rewrite.SuccessorProviderChain"
val SuccessorProviderNothing: Type = t"_root_.vct.col.rewrite.SuccessorProviderNothing"
val SuccessorProviderTrafo: Type = t"_root_.vct.col.rewrite.SuccessorProviderTrafo"

val AbstractRewriter: Type = t"_root_.vct.col.ast.AbstractRewriter"
val Scopes: Type = t"_root_.vct.col.util.Scopes"
Expand Down
2 changes: 2 additions & 0 deletions src/helpers/vct/col/ast/helpers/defn/Naming.scala
Original file line number Diff line number Diff line change
Expand Up @@ -111,4 +111,6 @@ object Naming {
Type.Name(node.base + "FamilyDeclare")
def declareType(node: structure.Name) =
t"${packageFromRoot(DeclarePackage)}.${declareTrait(node)}"
def succProviderName(name: structure.Name) =
Term.Name(scopes(name.base) + "SuccProvider")
}
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ class AbstractRewriter extends AllFamiliesGenerator {
def porcelainRefSeqSucc[RefDecl <: $Declaration[Post]](refs: $SeqType[$RefType[Pre, _]])(implicit tag: $ClassTag[RefDecl]): $OptionType[$SeqType[$RefType[Post, RefDecl]]] = None

val allScopes: $AllScopes[Pre, Post] = $AllScopesObj()
def succProvider: $SuccessorsProvider[Pre, Post] = this.allScopes.freeze
def succProvider: $SuccessorsProvider[Pre, Post] = this.allScopes

def anySucc[RefDecl <: $Declaration[Post]](`~decl`: $Declaration[Pre])(implicit tag: $ClassTag[RefDecl]): $RefType[Post, RefDecl] =
succProvider.anySucc[RefDecl](`~decl`)(tag)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ class AllFrozenScopes extends AllFamiliesGenerator {
source"""
package vct.col.ast

class AllFrozenScopes[Pre, Post](`~scopes`: $AllScopes[Pre, Post]) extends ${Init(t"$SuccessorsProvider[Pre, Post]", Name.Anonymous(), List.empty)} {
class AllFrozenScopes[Pre, Post](`~scopes`: $AllScopes[Pre, Post]) {
override def equals(`~obj`: $Any): $Boolean = `~obj` match {
case other: $AllFrozenScopes[_, _] =>
${declaredFamilies
Expand All @@ -42,7 +42,7 @@ class AllFrozenScopes extends AllFamiliesGenerator {
""").toList}

..${declaredFamilies.map(name => q"""
override def succ[RefDecl <: $Declaration[Post]](decl: ${typ(name)}[Pre])(implicit tag: $ClassTag[RefDecl]): $RefType[Post, RefDecl] =
def succ[RefDecl <: $Declaration[Post]](decl: ${typ(name)}[Pre])(implicit tag: $ClassTag[RefDecl]): $RefType[Post, RefDecl] =
${scopes(name.base)}.succ(decl)
""").toList}
}
Expand Down
11 changes: 8 additions & 3 deletions src/helpers/vct/col/ast/helpers/generator/AllScopes.scala
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
package vct.col.ast.helpers.generator

import vct.col.ast.helpers.defn.Constants._
import vct.col.ast.helpers.defn.Naming.{scopes, typ}
import vct.col.ast.helpers.defn.Naming.{scopes, succProviderName, typ}
import vct.col.ast.structure
import vct.col.ast.structure.AllFamiliesGenerator

Expand All @@ -21,7 +21,7 @@ class AllScopes extends AllFamiliesGenerator {
source"""
package vct.col.ast

case class AllScopes[Pre, Post]() {
case class AllScopes[Pre, Post]() extends ${Init(t"$SuccessorsProvider[Pre, Post]", Name.Anonymous(), List.empty)} {
def freeze: $AllFrozenScopes[Pre, Post] = new $AllFrozenScopes(this)

def anyDeclare[T <: $Declaration[Post]](`~decl`: T): T =
Expand All @@ -45,7 +45,12 @@ class AllScopes extends AllFamiliesGenerator {
""").toList}

..${declaredFamilies.map(name => q"""
def succ[RefDecl <: $Declaration[Post]](decl: ${typ(name)}[Pre])(implicit tag: $ClassTag[RefDecl]): $RefType[Post, RefDecl] =
def ${succProviderName(name)}: $SuccessorProvider[Pre, Post, ${typ(name)}[Pre], ${typ(name)}[Post]] =
this.${scopes(name.base)}.freeze
""").toList}

..${declaredFamilies.map(name => q"""
override def succ[RefDecl <: $Declaration[Post]](decl: ${typ(name)}[Pre])(implicit tag: $ClassTag[RefDecl]): $RefType[Post, RefDecl] =
this.${scopes(name.base)}.freeze.succ(decl)
""").toList}
}
Expand Down
38 changes: 29 additions & 9 deletions src/helpers/vct/col/ast/helpers/generator/SuccessorsProvider.scala
Original file line number Diff line number Diff line change
@@ -1,9 +1,10 @@
package vct.col.ast.helpers.generator

import vct.col.ast.helpers.defn.Naming.typ
import vct.col.ast.helpers.defn.Naming.{succProviderName, typ}
import vct.col.ast.helpers.defn.Constants._
import vct.col.ast.structure
import vct.col.ast.structure.{AllFamiliesGenerator}
import vct.col.ast.structure.AllFamiliesGenerator
import vct.col.ast.structure.Type.Nothing

import java.nio.file.Path
import scala.meta._
Expand All @@ -22,6 +23,7 @@ class SuccessorsProvider extends AllFamiliesGenerator {
package vct.col.ast

${successorsProvider(declaredFamilies)}
${successorsProviderNothing(declaredFamilies)}
${successorsProviderChain(declaredFamilies)}
${successorsProviderTrafo(declaredFamilies)}
"""
Expand All @@ -33,12 +35,24 @@ class SuccessorsProvider extends AllFamiliesGenerator {
${Term.Match(q"`~decl`", declaredFamilies.map(name => Case(p"(decl: ${typ(name)}[Pre])", None, q"succ(decl)")).toList)}

..${declaredFamilies.map(name => q"""
def computeSucc(decl: ${typ(name)}[Pre]): $OptionType[${typ(name)}[Post]]
def ${succProviderName(name)}: $SuccessorProvider[Pre, Post, ${typ(name)}[Pre], ${typ(name)}[Post]]
""").toList}

..${declaredFamilies.map(name => q"""
def succ[RefDecl <: $Declaration[Post]](decl: ${typ(name)}[Pre])(implicit tag: $ClassTag[RefDecl]): $RefType[Post, RefDecl] =
new ${Init(t"$LazyRef[Post, RefDecl]", Name.Anonymous(), List(List(q"this.computeSucc(decl).get")))}
${succProviderName(name)}.succ(decl)(tag)
""").toList}
}
"""

def successorsProviderNothing(
declaredFamilies: Seq[structure.Name]
): Defn.Class =
q"""
class SuccessorsProviderNothing[Pre, Post](crash: => Nothing) extends ${Init(t"$SuccessorsProvider[Pre, Post]", Name.Anonymous(), List.empty)} {
..${declaredFamilies.map(name => q"""
override def ${succProviderName(name)}: $SuccessorProvider[Pre, Post, ${typ(name)}[Pre], ${typ(name)}[Post]] =
new $SuccessorProviderNothing(crash)
""").toList}
}
"""
Expand All @@ -49,8 +63,8 @@ class SuccessorsProvider extends AllFamiliesGenerator {
q"""
case class SuccessorsProviderChain[A, B, C](left: $SuccessorsProvider[A, B], right: $SuccessorsProvider[B, C]) extends ${Init(t"SuccessorsProvider[A, C]", Name.Anonymous(), List.empty)} {
..${declaredFamilies.map(name => q"""
def computeSucc(decl: ${typ(name)}[A]): $OptionType[${typ(name)}[C]] =
this.left.computeSucc(decl).flatMap(this.right.computeSucc)
override def ${succProviderName(name)}: $SuccessorProvider[A, C, ${typ(name)}[A], ${typ(name)}[C]] =
new $SuccessorProviderChain(left.${succProviderName(name)}, right.${succProviderName(name)})
""").toList}
}
"""
Expand All @@ -59,13 +73,19 @@ class SuccessorsProvider extends AllFamiliesGenerator {
declaredFamilies: Seq[structure.Name]
): Defn.Class =
q"""
abstract class SuccessorsProviderTrafo[Pre, Post](inner: $SuccessorsProvider[Pre, Post]) extends ${Init(t"$SuccessorsProvider[Pre, Post]", Name.Anonymous(), List.empty)} {
abstract class SuccessorsProviderTrafo[Pre, Post](inner: $SuccessorsProvider[Pre, Post]) extends ${Init(t"$SuccessorsProvider[Pre, Post]", Name.Anonymous(), List.empty)} { outer =>
def preTransform[I <: $Declaration[Pre], O <: $Declaration[Post]](pre: I): $OptionType[O] = None
def postTransform[T <: $Declaration[Post]](pre: $Declaration[Pre], post: $OptionType[T]): $OptionType[T] = post

..${declaredFamilies.map((name: structure.Name) => q"""
def computeSucc(decl: ${typ(name)}[Pre]): $OptionType[${typ(name)}[Post]] =
this.preTransform(decl).orElse(this.postTransform(decl, this.inner.computeSucc(decl)))
override def ${succProviderName(name)}: $SuccessorProvider[Pre, Post, ${typ(name)}[Pre], ${typ(name)}[Post]] =
new ${Init(t"$SuccessorProviderTrafo[Pre, Post, ${typ(name)}[Pre], ${typ(name)}[Post]]", Name.Anonymous(), List(List(q"inner.${succProviderName(name)}")))} {
override def preTransform[I <: ${typ(name)}[Pre], O <: ${typ(name)}[Post]](pre: I): $OptionType[O] =
outer.preTransform[I, O](pre)

override def postTransform[T <: ${typ(name)}[Post]](pre: ${typ(name)}[Pre], post: $OptionType[T]): $OptionType[T] =
outer.postTransform[T](pre, post)
}
""").toList}
}
"""
Expand Down
17 changes: 4 additions & 13 deletions src/rewrite/vct/rewrite/ApplyTermRewriter.scala
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ import vct.col.rewrite.util.FreeVariables
import vct.col.origin.{DiagnosticOrigin, Name, Origin, SourceName}
import vct.col.ref.{LazyRef, Ref}
import vct.col.rewrite._
import vct.col.util.IdentitySuccessorsProvider
import vct.result.VerificationError.{Unreachable, UserError}

import scala.annotation.tailrec
Expand Down Expand Up @@ -98,12 +99,7 @@ case class ApplyTermRewriter[Rule, Pre <: Generation](
bindings: Map[Variable[Pre], Ref[Pre, Variable[Pre]]]
) extends NonLatchingRewriter[Pre, Pre] {
override def succProvider: SuccessorsProvider[Pre, Pre] =
new SuccessorsProviderTrafo(allScopes.freeze) {
override def postTransform[T <: Declaration[Pre]](
pre: Declaration[Pre],
post: Option[T],
): Option[T] = Some(pre.asInstanceOf[T])

new IdentitySuccessorsProvider[Pre] {
override def succ[RefDecl <: Declaration[Pre]](
decl: Variable[Pre]
)(implicit tag: ClassTag[RefDecl]): Ref[Pre, RefDecl] =
Expand Down Expand Up @@ -392,13 +388,8 @@ case class ApplyTermRewriter[Rule, Pre <: Generation](
}

case class ApplyRecursively() extends NonLatchingRewriter[Pre, Pre] {
case object IdentitySucc extends SuccessorsProviderTrafo(allScopes.freeze) {
override def preTransform[I <: Declaration[Pre], O <: Declaration[Pre]](
pre: I
): Option[O] = Some(pre.asInstanceOf[O])
}

override def succProvider: SuccessorsProvider[Pre, Pre] = IdentitySucc
override val succProvider: SuccessorsProvider[Pre, Pre] =
new IdentitySuccessorsProvider

@tailrec
override final def dispatch(e: Expr[Pre]): Expr[Pre] = {
Expand Down
2 changes: 1 addition & 1 deletion src/rewrite/vct/rewrite/InlineApplicables.scala
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ case object InlineApplicables extends RewriterBuilder {
case class ReplaceReturn[G](newStatement: Expr[G] => Statement[G])
extends NonLatchingRewriter[G, G] {
case class SuccOrIdentity()
extends SuccessorsProviderTrafo[G, G](allScopes.freeze) {
extends SuccessorsProviderTrafo[G, G](allScopes) {
override def postTransform[T <: Declaration[G]](
pre: Declaration[G],
post: Option[T],
Expand Down
3 changes: 2 additions & 1 deletion src/rewrite/vct/rewrite/adt/ImportADT.scala
Original file line number Diff line number Diff line change
Expand Up @@ -115,7 +115,8 @@ abstract class ImportADT[Pre <: Generation](importer: ImportADTImporter)
protected def parse(name: String): Seq[GlobalDeclaration[Post]] = {
val program = importer.loadAdt[Pre](name)
program.declarations.foreach(dispatch)
program.declarations.map(succProvider.computeSucc).map(_.get)
program.declarations
.map(succProvider.globalDeclarationsSuccProvider.computeSucc).map(_.get)
}

protected def find[T](decls: Seq[Declaration[Post]], name: String)(
Expand Down

0 comments on commit 99d9cc5

Please sign in to comment.