modifications in order to make insynth work on leon examples

ikuraj · Nov 7, 2012 · 5ffae3a · 5ffae3a
1 parent 0bc0551
commit 5ffae3a
Show file tree

Hide file tree

Showing 7 changed files with 59 additions and 28 deletions.
diff --git a/ch.epfl.insynth.build/ch.epfl.insynth.library/ch.epfl.insynth.library.jar b/ch.epfl.insynth.build/ch.epfl.insynth.library/ch.epfl.insynth.library.jar
diff --git a/ch.epfl.insynth.build/ch.epfl.insynth.tests/src/ch/epfl/insynth/test/TestSuite.scala b/ch.epfl.insynth.build/ch.epfl.insynth.tests/src/ch/epfl/insynth/test/TestSuite.scala
@@ -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)
   }
 }
diff --git a/....insynth.build/ch.epfl.insynth.tests/src/ch/epfl/insynth/test/leon/LeonProjectSetup.scala b/....insynth.build/ch.epfl.insynth.tests/src/ch/epfl/insynth/test/leon/LeonProjectSetup.scala
@@ -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)")

diff --git a/ch.epfl.insynth.build/ch.epfl.insynth/.classpath b/ch.epfl.insynth.build/ch.epfl.insynth/.classpath
@@ -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>
diff --git a/ch.epfl.insynth.build/ch.epfl.insynth/pom.xml b/ch.epfl.insynth.build/ch.epfl.insynth/pom.xml
@@ -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>

diff --git a/....epfl.insynth/src/ch/epfl/insynth/core/completion/InsynthCompletionProposalComputer.scala b/....epfl.insynth/src/ch/epfl/insynth/core/completion/InsynthCompletionProposalComputer.scala
@@ -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)
 

diff --git a/...h.epfl.insynth/src/ch/epfl/insynth/reconstruction/codegen/ClassicStyleCodeGenerator.scala b/...h.epfl.insynth/src/ch/epfl/insynth/reconstruction/codegen/ClassicStyleCodeGenerator.scala
@@ -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        				    
       				    )
           	}	
           }