Merge remote-tracking branch 'origin/dev' into fix-utwente-fmt#1215

src/col/vct/col/ast/type/typeclass/TypeImpl.scala

@@ -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] =>
@@ -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 {

src/col/vct/col/rewrite/SuccessorProviderChain.scala

@@ -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)
+}

src/col/vct/col/rewrite/SuccessorProviderNothing.scala

@@ -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
+}

src/col/vct/col/rewrite/SuccessorProviderTrafo.scala

@@ -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)))
+
+}

src/col/vct/col/typerules/CoercingRewriter.scala

@@ -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

src/col/vct/col/util/IdentitySuccessorsProvider.scala

@@ -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])
+}

src/col/vct/col/util/Substitute.scala

@@ -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],

src/helpers/vct/col/ast/helpers/defn/Constants.scala

@@ -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"
@@ -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"

src/helpers/vct/col/ast/helpers/defn/Naming.scala

@@ -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")
 }

src/helpers/vct/col/ast/helpers/generator/AbstractRewriter.scala

@@ -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)

src/helpers/vct/col/ast/helpers/generator/AllFrozenScopes.scala

@@ -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
@@ -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}
       }

src/helpers/vct/col/ast/helpers/generator/AllScopes.scala

@@ -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
 
@@ -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 =
@@ -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}
       }

src/helpers/vct/col/ast/helpers/generator/SuccessorsProvider.scala

@@ -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._
@@ -22,6 +23,7 @@ class SuccessorsProvider extends AllFamiliesGenerator {
       package vct.col.ast
 
       ${successorsProvider(declaredFamilies)}
+      ${successorsProviderNothing(declaredFamilies)}
       ${successorsProviderChain(declaredFamilies)}
       ${successorsProviderTrafo(declaredFamilies)}
     """
@@ -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}
       }
     """
@@ -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}
       }
     """
@@ -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}
       }
     """

src/rewrite/vct/rewrite/ApplyTermRewriter.scala

@@ -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
@@ -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] =
@@ -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] = {

src/rewrite/vct/rewrite/InlineApplicables.scala

@@ -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],

src/rewrite/vct/rewrite/adt/ImportADT.scala

@@ -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)(