cleanup

viperproject · Jan 23, 2025 · 91dd34f · 91dd34f
1 parent 5ef3294
commit 91dd34f
Show file tree

Hide file tree

Showing 9 changed files with 2,227 additions and 2,252 deletions.
diff --git a/src/main/antlr4/GobraLexer.g4 b/src/main/antlr4/GobraLexer.g4
@@ -89,8 +89,6 @@ DUPLICABLE  : 'dup';
 PKG_INV     : 'pkgInvariant';
 OPEN_DUP_SINV : 'openDupPkgInv' -> mode(NLSEMI);
 INIT_POST   : 'initEnsures';
-INIT_PRE    : 'initRequires';
-// The following is deprecated and meant to be replaced by INIT_PRE
 IMPORT_PRE  : 'importRequires';
 PROOF       : 'proof';
 GHOST_EQUALS     : '===';

diff --git a/src/main/antlr4/GobraParser.g4 b/src/main/antlr4/GobraParser.g4
@@ -45,7 +45,7 @@ preamble: (pkgInvariant eos)* (initPost eos)* packageClause eos (friendPkgDecl e
 
 initPost: INIT_POST expression;
 
-importPre: (IMPORT_PRE | INIT_PRE) expression;
+importPre: IMPORT_PRE expression;
 
 pkgInvariant: DUPLICABLE? PKG_INV assertion;
 

diff --git a/src/main/java/viper/gobra/frontend/GobraLexer.java b/src/main/java/viper/gobra/frontend/GobraLexer.java
diff --git a/src/main/java/viper/gobra/frontend/GobraParser.java b/src/main/java/viper/gobra/frontend/GobraParser.java
diff --git a/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala b/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala
@@ -313,6 +313,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
       case PFold(exp) => "fold" <+> showExpr(exp)
       case PPackageWand(wand, blockOpt) => "package" <+> showExpr(wand) <+> opt(blockOpt)(showStmt)
       case PApplyWand(wand) => "apply" <+> showExpr(wand)
+      case POpenDupPkgInv() => "openDupPkgInv"
       case PMatchStatement(exp, clauses, _) => "match" <+>
         showExpr(exp) <+> block(ssep(clauses map showMatchClauseStatement, line))
     }

diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ImportTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ImportTyping.scala
@@ -7,9 +7,7 @@
 package viper.gobra.frontend.info.implementation.typing
 
 import org.bitbucket.inkytonik.kiama.util.Messaging.{message, noMessages}
-import viper.gobra.GoVerifier
-import viper.gobra.ast.frontend.{PExplicitQualifiedImport, PImplicitQualifiedImport, PImport, PNode, PUnqualifiedImport}
-import viper.gobra.frontend.Config
+import viper.gobra.ast.frontend._
 import viper.gobra.frontend.PackageResolver.RegularImport
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 

diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala
@@ -6,17 +6,16 @@
 
 package viper.gobra.frontend.info.implementation.typing
 
-import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, check, checkUse, error, message, noMessages}
-
-import scala.collection.immutable.ListMap
-import viper.gobra.ast.frontend._
-import viper.gobra.ast.frontend.{AstPattern => ap}
+import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, noMessages}
+import viper.gobra.ast.frontend.{AstPattern => ap, _}
 import viper.gobra.frontend.info.base.SymbolTable
 import viper.gobra.frontend.info.base.SymbolTable.{Embbed, Field}
-import viper.gobra.frontend.info.base.Type.{StructT, _}
+import viper.gobra.frontend.info.base.Type._
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.frontend.info.implementation.property.UnderlyingType
 
+import scala.collection.immutable.ListMap
+
 trait TypeTyping extends BaseTyping { this: TypeInfoImpl =>
 
   import viper.gobra.util.Violation._

diff --git a/src/main/scala/viper/gobra/translator/transformers/TerminationDomainTransformer.scala b/src/main/scala/viper/gobra/translator/transformers/TerminationDomainTransformer.scala
@@ -5,18 +5,17 @@
 // Copyright (c) 2011-2021 ETH Zurich.
 
 package viper.gobra.translator.transformers
-import java.nio.file.Path
 import viper.gobra.backend.BackendVerifier
 import viper.silicon.Silicon
 import viper.silver.ast.utility.FileLoader
-import viper.silver.{ast => vpr}
 import viper.silver.frontend.{DefaultStates, ViperAstProvider}
-import viper.silver.plugin.SilverPlugin
 import viper.silver.plugin.standard.predicateinstance.PredicateInstance.PredicateInstanceDomainName
-import viper.silver.plugin.standard.termination.{DecreasesTuple, TerminationPlugin}
+import viper.silver.plugin.standard.termination.DecreasesTuple
 import viper.silver.reporter.{NoopReporter, Reporter}
-import viper.silver.plugin.standard.predicateinstance.PredicateInstancePlugin
 import viper.silver.verifier.AbstractError
+import viper.silver.{ast => vpr}
+
+import java.nio.file.Path
 
 // This class should be removed in the future because Viper already implements inference of
 // imports for termination domains. However, at the moment, Viper performs the inference in

diff --git a/src/test/resources/same_package/pkg_init/scion/scion.go b/src/test/resources/same_package/pkg_init/scion/scion.go
@@ -16,10 +16,10 @@ package scion
 // side effects that would not happen otherwise.
 import (
 	// @ "monotonicset"
-	// @ initRequires path.PkgInv()
-	// @ initRequires path.RegisteredTypes().DoesNotContain(1) &&
+	// @ importRequires path.PkgInv()
+	// @ importRequires path.RegisteredTypes().DoesNotContain(1) &&
 	// @ 	path.RegisteredTypes().DoesNotContain(2)
-	// @ initRequires false
+	//  importRequires false // TODO: check and then drop
 	// @ "scion/path"
 	"scion/path/onehop"
 	"scion/path/scion"