Skip to content

Commit

Permalink
Improve language flexibility (#727)
Browse files Browse the repository at this point in the history
Update to be compatible with new parser output
  • Loading branch information
JonasAlaif authored Jul 12, 2023
1 parent 259efc1 commit 0dde907
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 20 deletions.
2 changes: 1 addition & 1 deletion silver
Submodule silver updated 24 files
+1 −1 src/main/scala/viper/silver/ast/Statement.scala
+2 −2 src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala
+3 −8 src/main/scala/viper/silver/cfg/CfgTest.scala
+8 −19 src/main/scala/viper/silver/frontend/SilFrontend.scala
+3 −3 src/main/scala/viper/silver/parser/FastMessage.scala
+101 −505 src/main/scala/viper/silver/parser/FastParser.scala
+424 −0 src/main/scala/viper/silver/parser/MacroExpander.scala
+143 −98 src/main/scala/viper/silver/parser/ParseAst.scala
+72 −125 src/main/scala/viper/silver/parser/Resolver.scala
+9 −8 src/main/scala/viper/silver/parser/Transformer.scala
+116 −64 src/main/scala/viper/silver/parser/Translator.scala
+16 −4 src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala
+20 −24 src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
+2 −1 src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePASTExtension.scala
+0 −2 src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
+1 −1 src/main/scala/viper/silver/verifier/VerificationError.scala
+7 −1 src/main/scala/viper/silver/verifier/VerificationResult.scala
+53 −0 src/test/resources/all/basic/multi_initialization.vpr
+20 −0 src/test/resources/all/basic/multi_initialization_err.vpr
+13 −0 src/test/resources/all/basic/multi_initialization_translate_err.vpr
+2 −2 src/test/resources/all/issues/silver/0090.vpr
+6 −1 src/test/resources/all/issues/silver/0128.vpr
+1 −1 src/test/resources/all/issues/silver/0138.vpr
+1 −1 src/test/scala/ASTTransformationTests.scala
28 changes: 9 additions & 19 deletions src/main/scala/supporters/BuiltinDomainsContributor.scala
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,6 @@ import viper.silicon.interfaces.PreambleContributor
import viper.silicon.interfaces.decider.ProverLike
import viper.silicon.state.DefaultSymbolConverter
import viper.silicon.state.terms._
import viper.silver.ast.LineCol

abstract class BuiltinDomainsContributor extends PreambleContributor[Sort, DomainFun, Term] {
type BuiltinDomainType <: ast.GenericType
Expand Down Expand Up @@ -194,23 +193,14 @@ private object utils {
}

val fp = new viper.silver.parser.FastParser()
val lc = new LineCol(fp)
fp.parse(content, fromPath) match {
case fastparse.Parsed.Success(parsedProgram: viper.silver.parser.PProgram, _) =>
assert(parsedProgram.errors.isEmpty, s"Unexpected parsing errors: ${parsedProgram.errors}")

val resolver = viper.silver.parser.Resolver(parsedProgram)
val resolved = resolver.run.get
val translator = viper.silver.parser.Translator(resolved)
val program = translator.translate.get

program

case fastparse.Parsed.Failure(msg, index, _) =>
val (line, col) = lc.getPos(index)
sys.error(s"Failure: $msg, at ${viper.silver.ast.FilePosition(fromPath, line, col)}")
//? val pos = extra.input.prettyIndex(index).split(":").map(_.toInt)
//? sys.error(s"Failure: $msg, at ${viper.silver.ast.FilePosition(fromPath, pos(0), pos(1))}")
}
val parsedProgram = fp.parse(content, fromPath)
assert(parsedProgram.errors.isEmpty, s"Unexpected parsing errors: ${parsedProgram.errors}")

val resolver = viper.silver.parser.Resolver(parsedProgram)
val resolved = resolver.run.get
val translator = viper.silver.parser.Translator(resolved)
val program = translator.translate.get

program
}
}

0 comments on commit 0dde907

Please sign in to comment.