Implement the Leon library. Support classes and methods.
- Implement the Leon Library in Leon-land rather than Scala-land. import leon.Utils._ becomes import leon.lang._ import leon.Annotations._ becomes import leon.annontation._ For now, the library defines generic Options and Lists. The library is automatically imported from the ./leon script, unless the --library=no option is passed. - Support parsing of multiple files and modules. - Introduce new annontations: @ignore: remove definition from Leon @verified: do not consider for verification unless explicitly specified
Showing
- Library.scala 2 additions, 63 deletionsLibrary.scala
- lib-bin/32/libz3.so 0 additions, 0 deletionslib-bin/32/libz3.so
- library/Option.scala 32 additions, 0 deletionslibrary/Option.scala
- library/annotation/package.scala 14 additions, 0 deletionslibrary/annotation/package.scala
- library/build.sbt 0 additions, 15 deletionslibrary/build.sbt
- library/collection/List.scala 169 additions, 0 deletionslibrary/collection/List.scala
- library/lang/package.scala 5 additions, 5 deletionslibrary/lang/package.scala
- library/src/main/scala/leon/Annotations.scala 0 additions, 13 deletionslibrary/src/main/scala/leon/Annotations.scala
- project/Build.scala 5 additions, 10 deletionsproject/Build.scala
- src/main/scala/leon/Main.scala 13 additions, 3 deletionssrc/main/scala/leon/Main.scala
- src/main/scala/leon/Settings.scala 7 additions, 8 deletionssrc/main/scala/leon/Settings.scala
- src/main/scala/leon/codegen/CodeGeneration.scala 1 addition, 1 deletionsrc/main/scala/leon/codegen/CodeGeneration.scala
- src/main/scala/leon/frontends/scalac/ASTExtractors.scala 14 additions, 44 deletionssrc/main/scala/leon/frontends/scalac/ASTExtractors.scala
- src/main/scala/leon/frontends/scalac/CodeExtraction.scala 139 additions, 100 deletionssrc/main/scala/leon/frontends/scalac/CodeExtraction.scala
- src/main/scala/leon/frontends/scalac/ExtractionPhase.scala 9 additions, 1 deletionsrc/main/scala/leon/frontends/scalac/ExtractionPhase.scala
- src/main/scala/leon/purescala/ScalaPrinter.scala 1 addition, 2 deletionssrc/main/scala/leon/purescala/ScalaPrinter.scala
- src/main/scala/leon/utils/TemporaryInputPhase.scala 2 additions, 1 deletionsrc/main/scala/leon/utils/TemporaryInputPhase.scala
- src/main/scala/leon/xlang/Trees.scala 0 additions, 6 deletionssrc/main/scala/leon/xlang/Trees.scala
- src/test/resources/regression/synthesis/Church/Add.scala 1 addition, 1 deletionsrc/test/resources/regression/synthesis/Church/Add.scala
- src/test/resources/regression/synthesis/Church/Distinct.scala 1 addition, 1 deletion...test/resources/regression/synthesis/Church/Distinct.scala
Loading
Please register or sign in to comment