Skip to content

Commit

Permalink
Several ADT improvements (#687)
Browse files Browse the repository at this point in the history
* fixed reordering issue, type of constructors, implicit conversion of argument, some incorrect handling of imported adts, conversion issues with ghost data types, name space conflicts with adt types. I changed the representation of adt types, which I still need to double check.

* fixed some issues

* adapted parser to parse adts without field names

* fixed some bugs, also fixed error message with duplicate fields and clauses for adts

* fixed intendation, added comment, removed todo
  • Loading branch information
Felalolf authored Oct 3, 2023
1 parent 2e8205a commit 61d0bd9
Show file tree
Hide file tree
Showing 45 changed files with 3,622 additions and 3,197 deletions.
2 changes: 1 addition & 1 deletion build.sbt
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ lazy val gobra = (project in file("."))
libraryDependencies += "org.apache.commons" % "commons-lang3" % "3.9", // for SystemUtils
libraryDependencies += "org.apache.commons" % "commons-text" % "1.9", // for escaping strings in parser preprocessor
libraryDependencies += "commons-codec" % "commons-codec" % "1.15", // for obtaining the hex encoding of a string
libraryDependencies += "org.antlr" % "antlr4-runtime" % "4.12.0",
libraryDependencies += "org.antlr" % "antlr4-runtime" % "4.13.0",
libraryDependencies += "org.scalaz" %% "scalaz-core" % "7.3.7", // used for EitherT

scalacOptions ++= Seq(
Expand Down
4 changes: 3 additions & 1 deletion src/main/antlr4/GobraParser.g4
Original file line number Diff line number Diff line change
Expand Up @@ -150,7 +150,9 @@ domainClause: FUNC IDENTIFIER signature | AXIOM L_CURLY expression eos R_CURLY;

adtType: ADT L_CURLY (adtClause eos)* R_CURLY;

adtClause: IDENTIFIER L_CURLY (fieldDecl eos)* R_CURLY;
adtClause: IDENTIFIER L_CURLY (adtFieldDecl eos)* R_CURLY;

adtFieldDecl: identifierList? type_;

ghostSliceType: GHOST L_BRACKET R_BRACKET elementType;

Expand Down
634 changes: 319 additions & 315 deletions src/main/java/viper/gobra/frontend/GobraLexer.java

Large diffs are not rendered by default.

Loading

0 comments on commit 61d0bd9

Please sign in to comment.