Permalink
Browse files

modifications in order to make insynth work on leon examples

  • Loading branch information...
1 parent 0bc0551 commit 5ffae3ada98b76899a6ba68164a62c1cc15f5e08 @kaptoxic committed Nov 7, 2012
@@ -24,5 +24,6 @@ object TestSuite {
Activator.getDefault.getPreferenceStore.setValue(OfferedSnippetsPropertyString, 10)
Activator.getDefault.getPreferenceStore.setValue(MaximumTimePropertyString, 500)
Activator.getDefault.getPreferenceStore.setValue(DoSeparateLoggingPropertyString, true)
+ Activator.getDefault.getPreferenceStore.setValue(CodeStyleParenthesesPropertyString, CodeStyleParenthesesClassic)
}
}
@@ -30,6 +30,7 @@ class LeonProjectSetup {
val SCALACLASSPATH = classpathArray mkString ":"
//"/home/ivcha/git/leon-2.0/unmanaged/z3-64.jar:/home/ivcha/git/leon-2.0/target/scala-2.9.1-1/classes:/home/ivcha/git/leon-2.0/library/target/scala-2.9.1-1/classes:/home/ivcha/.sbt/boot/scala-2.9.1-1/lib/scala-library.jar:/home/ivcha/.sbt/boot/scala-2.9.1-1/lib/scala-compiler.jar"
+ @Ignore
@Test
def runList() {
val validCompletions = List("sizeTail(tail, 1)", "0", "sizeTail(tail, acc+1)")
@@ -6,5 +6,8 @@
<classpathentry kind="con" path="org.scala-ide.sdt.launching.SCALA_CONTAINER"/>
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER"/>
<classpathentry kind="lib" path="target/lib/ch.epfl.insynth.library-1.0.0.jar"/>
+ <classpathentry kind="lib" path="target/lib/leon-1.0.0.jar"/>
+ <classpathentry kind="lib" path="target/lib/leon_library-1.0.0.jar"/>
+ <classpathentry kind="lib" path="/home/kuraj/git/leon-2.0/unmanaged/z3-64.jar"/>
<classpathentry kind="output" path="target/classes"/>
</classpath>
@@ -17,32 +17,25 @@
<artifactId>ch.epfl.insynth.library</artifactId>
<version>1.0.0</version>
</dependency>
+ <dependency>
+ <groupId>ch.epfl.lara</groupId>
+ <artifactId>leon</artifactId>
+ <version>1.0.0</version>
+ </dependency>
+ <dependency>
+ <groupId>ch.epfl.lara</groupId>
+ <artifactId>leon_library</artifactId>
+ <version>1.0.0</version>
+ </dependency>
+ <dependency>
+ <groupId>ch.epfl.lara</groupId>
+ <artifactId>z3</artifactId>
+ <version>1.0.0</version>
+ </dependency>
</dependencies>
<build>
- <plugins>
- <!--<plugin>
- <groupId>org.apache.maven.plugins</groupId>
- <artifactId>maven-install-plugin</artifactId>
- <version>2.3.1</version>
- <executions>
- <execution>
- <id>install-insynth-library</id>
- <phase>process-resources</phase>
- <goals>
- <goal>install-file</goal>
- </goals>
- <configuration>
- <file>${basedir}/lib/ch.epfl.insynth.library.jar
- </file>
- <groupId>ch.epfl</groupId>
- <artifactId>ch.epfl.insynth.library</artifactId>
- <version>0.0.1-SNAPSHOT</version>
- <packaging>jar</packaging>
- </configuration>
- </execution>
- </executions>
- </plugin> -->
+ <plugins>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-dependency-plugin</artifactId>
@@ -61,6 +54,21 @@
<artifactId>ch.epfl.insynth.library</artifactId>
<outputDirectory>${project.build.directory}/lib</outputDirectory>
</artifactItem>
+ <artifactItem>
+ <groupId>ch.epfl.lara</groupId>
+ <artifactId>leon</artifactId>
+ <outputDirectory>${project.build.directory}/lib</outputDirectory>
+ </artifactItem>
+ <artifactItem>
+ <groupId>ch.epfl.lara</groupId>
+ <artifactId>leon_library</artifactId>
+ <outputDirectory>${project.build.directory}/lib</outputDirectory>
+ </artifactItem>
+ <artifactItem>
+ <groupId>ch.epfl.lara</groupId>
+ <artifactId>z3</artifactId>
+ <outputDirectory>${project.build.directory}/lib</outputDirectory>
+ </artifactItem>
</artifactItems>
</configuration>
</execution>
@@ -25,11 +25,15 @@ import ch.epfl.insynth.reconstruction.Output
import ch.epfl.insynth.reconstruction.Reconstructor
import ch.epfl.insynth.core.Activator
import scala.tools.eclipse.logging.HasLogger
-import ch.epfl.insynth.reconstruction.Output
-import ch.epfl.insynth.Config
+import ch.epfl.insynth.reconstruction.Output
+import ch.epfl.insynth.Config
import ch.epfl.insynth.core.preferences.InSynthConstants
import ch.epfl.insynth.reconstruction.codegen.{ CleanCodeGenerator, ClassicStyleCodeGenerator, ApplyTransfromer }
-import ch.epfl.insynth.reconstruction.codegen.SimpleApplicationNamesTransfromer
+import ch.epfl.insynth.reconstruction.codegen.SimpleApplicationNamesTransfromer
+import ch.epfl.insynth.leon.CodeExtractionForInSynth
+import leon.purescala.Definitions.Program
+import leon.Reporter
+import leon.DefaultReporter
/*
TODO:
@@ -51,6 +55,20 @@ object InnerFinder extends ((ScalaCompilationUnit, Int) => Option[List[Output]])
scu.withSourceFile {
(sourceFile, compiler) =>
+// val reporter: Reporter = new DefaultReporter
+// val actionOnProgram : Option[Program=>Unit] = Some(_ => Unit)
+// val leonPlugin = new LeonPlugin(this, actionOnProgram)
+
+ val codeExtraction = new CodeExtractionForInSynth(compiler, null)
+
+// val prog: purescala.Definitions.Program = extractCode(unit)
+// if(pluginInstance.stopAfterExtraction) {
+// println("Extracted program for " + unit + ": ")
+// println(prog)
+// println("Extraction complete. Now terminating the compiler process.")
+// sys.exit(0)
+// }
+
Config.inSynthLogger.info("InSynth working on source file: " + sourceFile.path)
logger.info("InSynth working on source file: " + sourceFile.path)
@@ -125,8 +125,8 @@ class ClassicStyleCodeGenerator extends CodeGenerator {
//group(decl.getObjectName :: "." :: doParen(appIdentifier, paramsDoc))
group(
parenthesesRequired ?
- (decl.getObjectName :: "." :: appIdentifier :: paren(paramsDoc)) |
- decl.getObjectName :: "." :: appIdentifier
+ (/* decl.getObjectName :: "." ::*/ appIdentifier :: paren(paramsDoc)) |
+ /* decl.getObjectName :: "." ::*/ appIdentifier
)
}
}

0 comments on commit 5ffae3a

Please sign in to comment.