diff --git a/build.sbt b/build.sbt
index 121a1311a55c452093541116e74a593be8094999..fc3aa2584872a570b4301e62c145ae93ba9b7983 100644
--- a/build.sbt
+++ b/build.sbt
@@ -38,6 +38,7 @@ libraryDependencies ++= Seq(
"info.hupel" %% "libisabelle" % "0.1.1",
"info.hupel" %% "libisabelle-setup" % "0.1.1",
"info.hupel" %% "pide-2015" % "0.1.1",
+ "org.ow2.asm" % "asm-all" % "5.0.4",
"com.fasterxml.jackson.module" %% "jackson-module-scala" % "2.6.0-rc2"
)
diff --git a/src/main/scala/leon/LeonContext.scala b/src/main/scala/leon/LeonContext.scala
index 8677364ee1cd5948a80001a72424e45a0538afcf..dd4e25ba35ef621c92b5cc880163be77c424295f 100644
--- a/src/main/scala/leon/LeonContext.scala
+++ b/src/main/scala/leon/LeonContext.scala
@@ -16,6 +16,7 @@ case class LeonContext(
interruptManager: InterruptManager,
options: Seq[LeonOption[Any]] = Seq(),
files: Seq[File] = Seq(),
+ classDir: Option[File] = None,
timers: TimerStorage = new TimerStorage
) {
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index b29f017c66eb80fb6e8fd6bb601c773cb1927a0c..3a8cb39df090fcb5ca3d3d902bedf6a52557026b 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -9,6 +9,7 @@ object Main {
lazy val allPhases: List[LeonPhase[_, _]] = {
List(
frontends.scalac.ExtractionPhase,
+ frontends.scalac.ClassgenPhase,
utils.TypingPhase,
FileOutputPhase,
purescala.RestoreMethods,
@@ -142,7 +143,7 @@ object Main {
import purescala.Definitions.Program
import purescala.{FunctionClosure, RestoreMethods}
import utils.FileOutputPhase
- import frontends.scalac.ExtractionPhase
+ import frontends.scalac.{ExtractionPhase, ClassgenPhase}
import synthesis.SynthesisPhase
import termination.TerminationPhase
import xlang.FixReportLabels
@@ -172,6 +173,7 @@ object Main {
displayHelp(ctx.reporter, error = false)
} else {
val pipeBegin: Pipeline[List[String], Program] =
+ ClassgenPhase andThen
ExtractionPhase andThen
new PreprocessingPhase(xlangF)
diff --git a/src/main/scala/leon/codegen/runtime/RuntimeResources.scala b/src/main/scala/leon/codegen/runtime/RuntimeResources.scala
new file mode 100644
index 0000000000000000000000000000000000000000..86c84d78396b0a59a6371906a90d4325b6bca0fd
--- /dev/null
+++ b/src/main/scala/leon/codegen/runtime/RuntimeResources.scala
@@ -0,0 +1,43 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.codegen.runtime
+
+import leon.utils.UniqueCounter
+
+import java.util.WeakHashMap
+import java.lang.ref.WeakReference
+import scala.collection.mutable.{HashMap => MutableMap}
+
+/**
+ * This class allows an evaluator to statically register a resource, identified
+ * by an integer. This identifier can be stored in bytecode, allowing .class to
+ * access the resource at runtime.
+ *
+ * The user/evaluator should keep hold of the returned Token, otherwise the
+ * resource may be garbage-collected.
+ *
+ * This is not statically-typed, but
+ *
+ * get[A]( register[A]( ... ) )
+ *
+ * should always be safe.
+ */
+object RuntimeResources {
+ case class Token(id: Int)
+
+ private val intCounter = new UniqueCounter[Unit]
+
+ private[this] val store = new WeakHashMap[Token, WeakReference[AnyRef]]()
+
+ def register[T <: AnyRef](data: T): Token = synchronized {
+ val t = Token(intCounter.nextGlobal)
+
+ store.put(t, new WeakReference(data))
+
+ t
+ }
+
+ def get[T <: AnyRef](id: Int): T = {
+ store.get(Token(id)).get.asInstanceOf[T]
+ }
+}
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index f17f9caefb644bfb08c1c5d9b7a429c2f408a872..68709c64e1bcd21df8de780c4a6c317af6384581 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -21,7 +21,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
val name = "evaluator"
val description = "Recursive interpreter for PureScala expressions"
- private implicit val ctx0 = ctx
+ private implicit val _ = ctx
type RC <: RecContext
type GC <: GlobalContext
@@ -29,6 +29,8 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case class EvalError(msg : String) extends Exception
case class RuntimeError(msg : String) extends Exception
+ val scalaEv = new ScalacEvaluator(this, ctx, prog)
+
trait RecContext {
def mappings: Map[Identifier, Expr]
@@ -169,12 +171,16 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
}
}
- if(!tfd.hasBody && !rctx.mappings.isDefinedAt(tfd.id)) {
- throw EvalError("Evaluation of function with unknown implementation.")
- }
+ val callResult = if (tfd.fd.annotations("extern") && ctx.classDir.isDefined) {
+ scalaEv.call(tfd, evArgs)
+ } else {
+ if(!tfd.hasBody && !rctx.mappings.isDefinedAt(tfd.id)) {
+ throw EvalError("Evaluation of function with unknown implementation.")
+ }
- val body = tfd.body.getOrElse(rctx.mappings(tfd.id))
- val callResult = e(body)(frame, gctx)
+ val body = tfd.body.getOrElse(rctx.mappings(tfd.id))
+ e(body)(frame, gctx)
+ }
tfd.postcondition match {
case Some(post) =>
diff --git a/src/main/scala/leon/evaluators/ScalacEvaluator.scala b/src/main/scala/leon/evaluators/ScalacEvaluator.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2b13d2655b43bd5e9a41fd236a8acb963d106356
--- /dev/null
+++ b/src/main/scala/leon/evaluators/ScalacEvaluator.scala
@@ -0,0 +1,469 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package evaluators
+
+import leon.codegen.runtime.RuntimeResources
+
+import purescala.Definitions._
+import purescala.DefOps._
+import purescala.Expressions._
+import purescala.Types._
+
+import java.io.File
+import java.nio.file.Files
+import java.net.{URL, URLClassLoader}
+import java.lang.reflect.{Constructor, Method}
+
+import frontends.scalac.FullScalaCompiler
+
+import scala.tools.nsc.{Settings=>NSCSettings,CompilerCommand}
+
+/**
+ * Call scalac-compiled functions from within Leon
+ *
+ * Known limitations:
+ * - Multiple argument lists
+ */
+class ScalacEvaluator(ev: Evaluator, ctx: LeonContext, pgm: Program) extends LeonComponent {
+ implicit val _: Program = pgm
+
+ val name = "Evaluator of external functions"
+ val description = "Evaluator for non-purescala functions"
+
+ implicit val debugSection = utils.DebugSectionEvaluation
+
+ val classPaths: List[File] = ctx.classDir.toList
+
+ lazy val runtimeTok = {
+ RuntimeResources.register(this)
+ }
+
+ private def unsupported(err: String): Nothing = {
+ throw new RuntimeException(err)
+ }
+
+ private def encodeName(name: String): String = {
+ scala.reflect.NameTransformer.encode(name)
+ }
+
+ private def jvmName(d: Definition): String = {
+ compiledName(d).replace(".", "/")
+ }
+
+ private def jvmClassName(tpe: TypeTree): String = tpe match {
+ case IntegerType =>
+ "scala/math/BigInt"
+
+ case TupleType(subs) =>
+ f"scala/Tuple${subs.size}%d"
+
+ case UnitType =>
+ "scala/runtime/BoxedUnit"
+
+ case ct: ClassType =>
+ jvmName(ct.classDef)
+
+ case _ =>
+ ctx.reporter.internalError(s"$tpe is not a jvm class type ?!?")
+ }
+
+ private def compiledName(d: Definition): String = {
+ // Scala encodes fullname of modules using ".". After the module, it
+ // becomes an inner class, with '$'
+ val path = pathFromRoot(d)
+
+ val pathToModule = path.takeWhile{!_.isInstanceOf[ModuleDef]}
+ val rest = path.drop(pathToModule.size)
+
+ val upToModule = pathToNames(pathToModule, false).map(encodeName).mkString(".")
+
+ if(rest.isEmpty) {
+ upToModule
+ } else {
+ d match {
+ case md: ModuleDef =>
+ upToModule+"."+encodeName(md.id.name)+"$"
+ case _ =>
+ val afterModule = pathToNames(rest, false).map(encodeName).mkString("$")
+ upToModule+"."+afterModule
+ }
+ }
+ }
+
+ def call(tfd: TypedFunDef, args: Seq[Expr]): Expr = {
+ val fd = tfd.fd
+
+ val methodName = encodeName(fd.id.name)
+
+ val jvmArgs = args.map(leonToScalac)
+
+ val (clazz, jvmRec, jvmCallArgs) = fd.methodOwner match {
+ case Some(cd) =>
+ (cd, jvmArgs.head, jvmArgs.tail)
+
+ case None =>
+ val md = moduleOf(fd).get
+
+ val jvmModule = loadClass(compiledName(md))
+ val rec = jvmModule.getField("MODULE$").get(null)
+
+ (md, rec, jvmArgs)
+ }
+
+ val jvmClassName = compiledName(clazz)
+ val jvmClass = loadClass(jvmClassName)
+
+ ctx.reporter.debug(s"Calling $jvmClassName.${tfd.signature}(${args.mkString(", ")})")
+
+ // Lookup method in jvmClass
+
+ jvmClass.getMethods().filter(_.getName() == methodName).toList match {
+ case List(meth) =>
+
+ val res = if (jvmCallArgs.isEmpty) {
+ meth.invoke(jvmRec)
+ } else {
+ meth.invoke(jvmRec, jvmCallArgs: _*)
+ }
+
+ scalacToLeon(res, tfd.returnType)
+
+ case Nil =>
+ unsupported(s"Unable to lookup method")
+
+ case ms =>
+ unsupported(s"Ambiguous reference to method: ${ms.size} methods found with a matching name")
+
+ }
+ }
+
+ val localClassLoader = {
+ classOf[ScalacEvaluator].getClassLoader()
+ }
+
+ val toInstrument = {
+ val fds = (for (fd <- pgm.definedFunctions if !fd.annotations("extern")) yield {
+ encodeName(fd.id.name) -> fd
+ }).toMap
+
+ fds.groupBy { case (n, fd) =>
+ compiledName(fd.methodOwner.getOrElse(moduleOf(fd).get))
+ }
+ }
+
+ val compiledClassLoader = {
+ val classUrls = ctx.classDir.map(_.toURI.toURL)
+ val cl = new URLClassLoader(classUrls.toArray, localClassLoader)
+ new InterceptingClassLoader(cl)
+ }
+
+ def loadClass(classname: String): Class[_] = {
+ compiledClassLoader.loadClass(classname)
+ }
+
+ def leonToScalac(e: Expr): AnyRef = e match {
+ case eo: ExternalObject =>
+ eo
+
+ case CharLiteral(v) =>
+ new java.lang.Character(v)
+
+ case IntLiteral(v) =>
+ new java.lang.Integer(v)
+
+ case InfiniteIntegerLiteral(v) =>
+ v
+
+ case BooleanLiteral(v) =>
+ new java.lang.Boolean(v)
+
+ case Tuple(exprs) =>
+ val name = f"scala.Tuple${exprs.size}%d"
+
+ val cl = localClassLoader.loadClass(name)
+ val constr = cl.getConstructors().head.asInstanceOf[Constructor[AnyRef]]
+
+ constr.newInstance(exprs.map(leonToScalac) : _*)
+
+ case UnitLiteral() =>
+ Unit.box(())
+
+ case FiniteSet(exprs, tpe) =>
+
+ val cl = compiledClassLoader.loadClass("leon.lang.Set")
+ val constr = cl.getConstructors().head.asInstanceOf[Constructor[AnyRef]]
+
+ constr.newInstance(Set(exprs.toSeq.map(leonToScalac) : _*))
+
+ case FiniteMap(pairs, ktpe, vtpe) =>
+
+ val cl = compiledClassLoader.loadClass("leon.lang.Map")
+ val constr = cl.getConstructors().head.asInstanceOf[Constructor[AnyRef]]
+
+ constr.newInstance(Map(
+ pairs.map { case (k, v) =>
+ leonToScalac(k) -> leonToScalac(v)
+ }.toSeq : _*
+ ))
+
+ case CaseClass(cct, fields) =>
+
+ val name = compiledName(cct.classDef)
+
+ val cl = loadClass(name)
+ val constr = cl.getConstructors().head.asInstanceOf[Constructor[AnyRef]]
+ constr.newInstance(fields.map(leonToScalac) : _*)
+
+
+ case Lambda(_, _) =>
+ unsupported("It is not yet possible to pass a closure to an @extern function")
+
+ case t: Terminal =>
+ unsupported("Unhandled conversion to scala runtime: "+t)
+
+ case _ =>
+ unsupported("Trying to convert non-terminal: "+e)
+ }
+
+ def productToElems(p: Product, tps: Seq[TypeTree]): Seq[Expr] = {
+ for ((t,i) <- tps.zipWithIndex) yield {
+ scalacToLeon(p.productElement(i), t)
+ }
+ }
+
+ def scalacToLeon(o: Any, t: TypeTree): Expr = t match {
+ case BooleanType =>
+ BooleanLiteral(o.asInstanceOf[Boolean].booleanValue)
+ case Int32Type =>
+ IntLiteral(o.asInstanceOf[Integer].intValue)
+ case CharType =>
+ CharLiteral(o.asInstanceOf[Character].charValue)
+ case IntegerType =>
+ InfiniteIntegerLiteral(o.asInstanceOf[BigInt])
+ case UnitType =>
+ UnitLiteral()
+ case TupleType(tps) =>
+ Tuple(productToElems(o.asInstanceOf[Product], tps))
+ case cct: CaseClassType =>
+ CaseClass(cct, productToElems(o.asInstanceOf[Product], cct.fieldsTypes))
+
+ case act: AbstractClassType =>
+ val className = o.getClass.getName
+
+ act.knownCCDescendants.find(cct => compiledName(cct.classDef) == className) match {
+ case Some(cct) =>
+ scalacToLeon(o, cct)
+
+ case None =>
+ unsupported("Expected "+act+", got: "+className)
+ }
+
+ case SetType(b) =>
+ val cl = compiledClassLoader.loadClass("leon.lang.Set")
+
+ val s = cl.getMethod("theSet").invoke(o).asInstanceOf[Set[_]]
+
+ FiniteSet(s.iterator.map(scalacToLeon(_, b)).toSet, b)
+
+ case MapType(ktpe, vtpe) =>
+
+ val cl = compiledClassLoader.loadClass("leon.lang.Map")
+
+ val s = cl.getMethod("theMap").invoke(o).asInstanceOf[Map[_, _]]
+
+ FiniteMap(s.iterator.map {
+ case (k, v) => scalacToLeon(k, ktpe) -> scalacToLeon(v, vtpe)
+ }.toSeq, ktpe, vtpe)
+
+ case FunctionType(_, _) =>
+ unsupported("It is not possible to pass a closure from @extern back to leon")
+
+ case _ =>
+ unsupported("Unhandled conversion from scala runtime: "+t)
+ }
+
+ def jvmCallBack(cName: String, fName: String, args: Array[AnyRef]): AnyRef = {
+ toInstrument.get(cName).flatMap(_.get(fName)) match {
+ case Some(fd) =>
+ val leonArgs = fd.params.map(_.getType).zip(args).map {
+ case (tpe, arg) => scalacToLeon(arg, tpe)
+ }
+
+ val fi = FunctionInvocation(fd.typed, leonArgs)
+ leonToScalac(ev.eval(fi).result.getOrElse {
+ unsupported("Evaluation in Leon failed!")
+ })
+
+ case None =>
+ unsupported("Unable to locate callback function "+cName+"."+fName)
+ }
+ }
+
+ /**
+ * Black magic here we come!
+ */
+ import org.objectweb.asm.ClassReader;
+ import org.objectweb.asm.ClassWriter;
+ import org.objectweb.asm.ClassVisitor;
+ import org.objectweb.asm.MethodVisitor;
+ import org.objectweb.asm.Opcodes;
+
+ class InterceptingClassLoader(p: ClassLoader) extends ClassLoader(p) {
+ import java.io._
+
+ var loaded = Set[String]()
+
+ override def loadClass(name: String, resolve: Boolean): Class[_] = {
+ if (loaded(name)) {
+ super.loadClass(name, resolve)
+ } else {
+ loaded += name
+
+ if (!(toInstrument contains name)) {
+ super.loadClass(name, resolve)
+ } else {
+ val bs = new ByteArrayOutputStream();
+ val is = getResourceAsStream(name.replace('.', '/') + ".class");
+ val buf = new Array[Byte](512);
+ var len = is.read(buf);
+ while (len > 0) {
+ bs.write(buf, 0, len);
+ len = is.read(buf)
+ }
+
+ // Transform bytecode
+ val cr = new ClassReader(bs.toByteArray());
+ val cw = new ClassWriter(cr, ClassWriter.COMPUTE_FRAMES);
+ val cv = new LeonCallsClassVisitor(cw, name, toInstrument(name));
+ cr.accept(cv, 0);
+
+ val res = cw.toByteArray();
+
+ defineClass(name, res, 0, res.length);
+ }
+ }
+ }
+ }
+
+ class LeonCallsClassVisitor(cv: ClassVisitor, cName: String, fdMap: Map[String, FunDef]) extends ClassVisitor(Opcodes.ASM5, cv) {
+ override def visitMethod(access: Int, fName: String, desc: String, sig: String, exceptions: Array[String]) = {
+ val mv = super.visitMethod(access, fName, desc, sig, exceptions)
+ if ((fdMap contains fName)) {
+ new LeonCallsMethodVisitor(mv, cName, fName, fdMap(fName))
+ } else {
+ mv
+ }
+ }
+ }
+
+ class LeonCallsMethodVisitor(mv: MethodVisitor, cName: String, fName: String, fd: FunDef) extends MethodVisitor(Opcodes.ASM5, mv) {
+
+ def box(tpe: TypeTree) = tpe match {
+ case Int32Type =>
+ mv.visitTypeInsn(Opcodes.NEW, "java/lang/Integer")
+ mv.visitInsn(Opcodes.DUP_X1)
+ mv.visitInsn(Opcodes.SWAP)
+ mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Integer", "<init>", "(I)V", false)
+
+ case CharType =>
+ mv.visitTypeInsn(Opcodes.NEW, "java/lang/Character")
+ mv.visitInsn(Opcodes.DUP_X1)
+ mv.visitInsn(Opcodes.SWAP)
+ mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Character", "<init>", "(C)V", false)
+
+ case BooleanType =>
+ mv.visitTypeInsn(Opcodes.NEW, "java/lang/Boolean")
+ mv.visitInsn(Opcodes.DUP_X1)
+ mv.visitInsn(Opcodes.SWAP)
+ mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Boolean", "<init>", "(Z)V", false)
+
+ case _ =>
+ }
+
+ def unbox(tpe: TypeTree) = tpe match {
+ case Int32Type =>
+ mv.visitTypeInsn(Opcodes.CHECKCAST, "java/lang/Integer")
+ mv.visitMethodInsn(Opcodes.INVOKEVIRTUAL, "java/lang/Integer", "intValue", "()I", false)
+
+ case CharType =>
+ mv.visitTypeInsn(Opcodes.CHECKCAST, "java/lang/Character")
+ mv.visitMethodInsn(Opcodes.INVOKEVIRTUAL, "java/lang/Character", "charValue", "()C", false)
+
+ case BooleanType =>
+ mv.visitTypeInsn(Opcodes.CHECKCAST, "java/lang/Boolean")
+ mv.visitMethodInsn(Opcodes.INVOKEVIRTUAL, "java/lang/Boolean", "booleanValue", "()Z", false)
+
+ case tpe =>
+ mv.visitTypeInsn(Opcodes.CHECKCAST, jvmClassName(tpe))
+ }
+
+ def loadOpCode(tpe: TypeTree) = tpe match {
+ case CharType => Opcodes.ILOAD
+ case Int32Type => Opcodes.ILOAD
+ case BooleanType => Opcodes.ILOAD
+ case _ => Opcodes.ALOAD
+ }
+
+ def returnOpCode(tpe: TypeTree) = tpe match {
+ case CharType => Opcodes.IRETURN
+ case Int32Type => Opcodes.IRETURN
+ case BooleanType => Opcodes.IRETURN
+ case UnitType => Opcodes.RETURN
+ case _ => Opcodes.ARETURN
+ }
+
+
+ override def visitCode() {
+ mv.visitLdcInsn(runtimeTok.id)
+ mv.visitLdcInsn(cName)
+ mv.visitLdcInsn(fName)
+
+ // If we are visiting a method, we need to add the receiver in the arguments array
+ val readOffset = fd.methodOwner match {
+ case Some(cd) =>
+ // $this is the receiver
+ 0
+ case _ =>
+ // We skip the module object
+ 1
+ }
+
+ // Array of arguments called
+ mv.visitLdcInsn(fd.params.size)
+ mv.visitTypeInsn(Opcodes.ANEWARRAY, "java/lang/Object")
+
+ // Note: fd.params includes the receiver!
+ // Add actual arguments, box necessary values
+ for ((tpe, i) <- fd.params.map(_.getType).zipWithIndex) {
+ // Array ref
+ mv.visitInsn(Opcodes.DUP)
+ mv.visitLdcInsn(i)
+ // Arg Value
+ mv.visitVarInsn(loadOpCode(tpe), i+readOffset)
+ box(tpe)
+ mv.visitInsn(Opcodes.AASTORE)
+ }
+
+
+ mv.visitMethodInsn(Opcodes.INVOKESTATIC,
+ "leon/evaluators/LeonJVMCallBacks",
+ "callBack",
+ "(ILjava/lang/String;Ljava/lang/String;[Ljava/lang/Object;)Ljava/lang/Object;",
+ false)
+
+ unbox(fd.returnType)
+ mv.visitInsn(returnOpCode(fd.returnType))
+ mv.visitEnd();
+ }
+ }
+}
+
+case class ExternalObject(o: Any, getType: TypeTree) extends Expr with Terminal
+
+object LeonJVMCallBacks {
+ def callBack(token: Int, className: String, methodName: String, args: Array[AnyRef]): AnyRef = {
+ val ev = RuntimeResources.get[ScalacEvaluator](token)
+ ev.jvmCallBack(className, methodName, args)
+ }
+}
diff --git a/src/main/scala/leon/frontends/scalac/ClassgenPhase.scala b/src/main/scala/leon/frontends/scalac/ClassgenPhase.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b2650740483613b02d3cd208b913febdb15bca5f
--- /dev/null
+++ b/src/main/scala/leon/frontends/scalac/ClassgenPhase.scala
@@ -0,0 +1,82 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package frontends.scalac
+
+import purescala.Definitions.Program
+import utils._
+
+import scala.tools.nsc.{Settings,CompilerCommand}
+import java.io.File
+import java.nio.file.Files
+
+object ClassgenPhase extends LeonPhase[List[String], List[String]] {
+
+ val optExtern = LeonFlagOptionDef("extern", "Run @extern function on the JVM", false)
+
+ override val definedOptions: Set[LeonOptionDef[Any]] = Set(optExtern)
+
+ val name = "Scalac .class generation"
+ val description = "Generation of .class for evaluation of @extern functions"
+
+ implicit val debug = DebugSectionTrees
+
+ def run(ctx: LeonContext, args: List[String]): (LeonContext, List[String]) = {
+ if (ctx.findOptionOrDefault(optExtern)) {
+ val timer = ctx.timers.frontend.extern.start()
+
+ val settings = new Settings
+
+ val scalaLib = Option(scala.Predef.getClass.getProtectionDomain.getCodeSource).map{
+ _.getLocation.getPath
+ }.orElse( for {
+ // We are in Eclipse. Look in Eclipse plugins to find scala lib
+ eclipseHome <- Option(System.getenv("ECLIPSE_HOME"))
+ pluginsHome = eclipseHome + "/plugins"
+ plugins <- scala.util.Try(new File(pluginsHome).listFiles().map{ _.getAbsolutePath }).toOption
+ path <- plugins.find{ _ contains "scala-library"}
+ } yield path).getOrElse( ctx.reporter.fatalError(
+ "No Scala library found. If you are working in Eclipse, " +
+ "make sure to set the ECLIPSE_HOME environment variable to your Eclipse installation home directory"
+ ))
+
+ val tempOut = Files.createTempDirectory(new File("tmp/").toPath, "classes").toFile
+
+ settings.classpath.value = scalaLib
+ settings.usejavacp.value = false
+ settings.deprecation.value = true
+ settings.outdir.value = tempOut.getPath
+
+ val compilerOpts = Build.libFiles ::: args.filterNot(_.startsWith("--"))
+
+ val command = new CompilerCommand(compilerOpts, settings) {
+ override val cmdName = "leon"
+ }
+
+ if(command.ok) {
+ // Debugging code for classpath crap
+ // new scala.tools.util.PathResolver(settings).Calculated.basis.foreach { cp =>
+ // cp.foreach( p =>
+ // println(" => "+p.toString)
+ // )
+ // }
+
+
+ val compiler = new FullScalaCompiler(settings, ctx)
+ val run = new compiler.Run
+ run.compile(command.files)
+
+ timer.stop()
+
+ val ctx2 = ctx.copy(classDir = Some(tempOut))
+
+ (ctx2, args)
+ } else {
+ ctx.reporter.fatalError("No input program.")
+ }
+ } else {
+ (ctx, args)
+ }
+ }
+}
+
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 9fa7606da23741a13f4d705374f867c23957fc53..299e8995a072084bba0adf0a98603e64b1611aac 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -947,7 +947,11 @@ trait CodeExtraction extends ASTExtractors {
private def extractTreeOrNoTree(tr: Tree)(implicit dctx: DefContext): LeonExpr = {
try {
- extractTree(tr)
+ val res = extractTree(tr)
+ if (dctx.isExtern) {
+ reporter.warning(res.getPos, "External function could be extracted as Leon tree")
+ }
+ res
} catch {
case e: ImpureCodeEncounteredException =>
if (dctx.isExtern) {
diff --git a/src/main/scala/leon/frontends/scalac/FullScalaCompiler.scala b/src/main/scala/leon/frontends/scalac/FullScalaCompiler.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2ae74e2020ccc391f5b478d60fda42d5f2809ab5
--- /dev/null
+++ b/src/main/scala/leon/frontends/scalac/FullScalaCompiler.scala
@@ -0,0 +1,16 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package frontends.scalac
+
+import scala.tools.nsc.{Global,Settings=>NSCSettings}
+import scala.reflect.internal.Positions
+
+class FullScalaCompiler(settings: NSCSettings, ctx: LeonContext) extends Global(settings, new SimpleReporter(settings, ctx.reporter)) with Positions {
+
+ class Run extends super.Run {
+ override def progress(current: Int, total: Int) {
+ ctx.reporter.onCompilerProgress(current, total)
+ }
+ }
+}
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 89c0fce8145f9ad43b1924e8cbb81f57de3d0a56..1e5e120112330ca85fccfdded79f425c0035214b 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -22,7 +22,13 @@ object DefOps {
case other => pgm.units.find(_.containsDef(df))
}
- private def pathFromRoot(df: Definition)(implicit pgm: Program): List[Definition] = {
+ def moduleOf(df: Definition)(implicit pgm: Program): Option[ModuleDef] = df match {
+ case p : Program => None
+ case u : UnitDef => None
+ case other => pgm.units.flatMap(_.modules).find { _.containsDef(df) }
+ }
+
+ def pathFromRoot(df: Definition)(implicit pgm: Program): List[Definition] = {
def rec(from: Definition): List[Definition] = {
from :: (if (from == df) {
Nil
diff --git a/testcases/extern/Editor.scala b/testcases/extern/Editor.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d843697f1c362e0ef33ef4a980a785dc4418d789
--- /dev/null
+++ b/testcases/extern/Editor.scala
@@ -0,0 +1,229 @@
+import leon.lang._
+import leon.annotation._
+import leon.lang.synthesis._
+import leon.collection._
+import scala.reflect.runtime.universe._
+import scala.reflect.api.{TypeCreator, Universe, Mirror}
+
+
+import scala.collection.immutable.{List => ScalaList, Nil => ScalaNil}
+
+object Editor {
+ abstract class Mode
+ case object Edit extends Mode
+ case object Quitted extends Mode
+
+ case class State(line: List[Int], cursor: Int, buffer: List[Int], actions: List[Action], mode: Mode) {
+ def setLine(l: List[Int]) = State(l, cursor, buffer, actions, mode)
+ def setCursor(c: Int) = State(line, c, buffer, actions, mode)
+ def setBuffer(b: List[Int]) = State(line, cursor, b, actions, mode)
+ def addAction(a: Action) = State(line, cursor, buffer, Cons(a, actions), mode)
+ def setMode(m: Mode) = State(line, cursor, buffer, actions, m)
+ }
+
+ sealed abstract class Action
+ case object Unknown extends Action
+ case object Write extends Action
+ case object Quit extends Action
+ case object Replace extends Action
+ case object Erase extends Action
+ case class Content(l: List[Int]) extends Action
+
+ @extern
+ def getCommand(): List[Int] = {
+ print("> ")
+ readLine().toList.map(_.toInt)
+ }
+
+ @extern
+ def getOracle(): Oracle[Action] = {
+ new KeyboardOracle()
+ }
+
+ def replStep(state: State): State = {
+ if (state.mode == Quitted) {
+ state
+ } else {
+ implicit val o = getOracle()
+ val a = {
+ //val a = withOracle { implicit o: Oracle[Action] =>
+ val i = getCommand()
+
+ getAction(i, state)
+ }
+
+ val newState = doAction(state, a)
+ replStep(newState)
+ }
+ }
+
+ @extern
+ def unknown() = {
+ println("?")
+ }
+
+ @extern
+ def display(a: Action, s: State) = {
+ println(" | Action : "+a)
+ println(" | Line : "+s.line)
+ println(" | Curs : "+s.cursor)
+ println(" | Buff : "+s.buffer)
+ println(" | A* : "+s.actions.map(_.toString).mkString(", "))
+ }
+
+ def getAction(input: List[Int], state: State)(implicit o: Oracle[Action]): Action = {
+ ???
+ }
+
+ def doAction(state: State, action: Action): State = {
+ val c = state.cursor
+ val l = state.line
+
+ val tmp = display(action, state)
+
+ val ns = (action, state.actions) match {
+ case (Content(cnt), Cons(Write, _)) =>
+ val nl = l.take(c) ++ cnt ++ l.drop(c)
+ state.setLine(nl).setCursor(c + cnt.size)
+ case (Content(cnt), Cons(Replace, _)) =>
+ val nl = l.take(c) ++ cnt ++ l.drop(c+cnt.size)
+ state.setLine(nl).setCursor(c + cnt.size)
+ case (Erase, _) =>
+ state.setLine(Nil()).setCursor(0)
+ case (Quit, _) =>
+ state.setMode(Quitted)
+ case _ =>
+ unknown()
+ state
+ }
+
+ ns.addAction(action)
+ }
+
+ @ignore
+ @extern
+ class KeyboardOracle[T: TypeTag](lvl: Int = 0) extends Oracle[T] {
+ var result: T = _
+
+ val ind = " "*lvl
+
+ lazy val h: T = {
+ val m = runtimeMirror(getClass.getClassLoader)
+ val oracleClass = typeOf[KeyboardOracle[T]].typeSymbol.asClass
+ val refOracle = m.reflectClass(oracleClass)
+
+ val ls = Erase
+
+ val tpeClass = typeOf[T].typeSymbol.asClass
+ println(s"~${ind} Requesting value for (_ <: ${typeOf[T]}):")
+
+ var askAgain = true
+ while (askAgain) {
+ if (tpeClass.isSealed) {
+ val TypeRef(pre, sym, tpts) = typeOf[T]
+ val subClasses = tpeClass.knownDirectSubclasses.toSeq.sortBy(_.name.toString)
+
+ for ((sub, i) <- subClasses.zipWithIndex) {
+ println(f"~${ind} $i%2d: $sub%s")
+ }
+
+ print(s"~${ind} > ")
+ val i = readLine().toInt
+ if (i >= 0 && i < subClasses.size) {
+ val subClass = subClasses(i).asClass
+ val subType = TypeRef(pre, subClass, tpts)
+
+ val refClass = m.reflectClass(subClass)
+ val ctor = subType.declaration(nme.CONSTRUCTOR).asMethod
+ val refCtor = refClass.reflectConstructor(ctor)
+ val ctorTpe = ctor.typeSignatureIn(subType).asInstanceOf[MethodType]
+
+ val rargs = for (arg <- ctorTpe.params) yield {
+ val argTpe = arg.typeSignature
+ val oracleTpe = typeRef(NoPrefix, oracleClass, List(argTpe))
+ val oracleCtor = oracleTpe.declaration(nme.CONSTRUCTOR).asMethod
+ val refOracleCtor = refOracle.reflectConstructor(oracleCtor)
+
+ val typeTag = TypeTag(m, new TypeCreator {
+ def apply[U <: Universe with Singleton](m: Mirror[U]): U#Type = {
+ if (m == runtimeMirror(getClass.getClassLoader)) {
+ argTpe.asInstanceOf[U#Type]
+ } else {
+ sys.error("Unsupported")
+ }
+ }
+ })
+
+ // Build an instance of this oracle:
+ val oracle = refOracleCtor(lvl+1, typeTag)
+
+ // We call its `head` method
+ val head = oracleTpe.declaration(("head": TermName)).asMethod
+
+ m.reflect(oracle).reflectMethod(head)()
+ }
+
+ result = refCtor(rargs: _*).asInstanceOf[T]
+ askAgain = false;
+ }
+ } else if (tpeClass.name.toString == "Int") {
+ print(s"~${ind} > ")
+ try {
+ result = readLine().toInt.asInstanceOf[T]
+ askAgain = false
+ } catch {
+ case _: Throwable =>
+ }
+ } else if (tpeClass.name.toString == "Boolean") {
+ print(s"~${ind} > ")
+ readLine() match {
+ case "true" =>
+ result = true.asInstanceOf[T]
+ askAgain = false
+ case "false" =>
+ result = false.asInstanceOf[T]
+ askAgain = false
+ case _ =>
+ }
+ } else {
+ sys.error("Don't know how to generate for non-sealed class")
+ }
+ }
+
+ result
+ }
+
+
+ lazy val l = new KeyboardOracle[T]()
+ lazy val r = new KeyboardOracle[T]()
+ override def head = h
+ override def left = l
+ override def right = r
+ }
+
+ def repl() = {
+ val state = State(Nil(), 0, Nil(), Nil(), Edit)
+ replStep(state)
+ }
+
+ @ignore
+ @extern
+ implicit def scalaToList[T](l: ScalaList[T]): List[T] = {
+ l.foldLeft[List[T]](Nil())( (l, e) => Cons(e, l) )
+ }
+
+ @ignore
+ @extern
+ implicit def listToScala[T](l: List[T]): ScalaList[T] = l match {
+ case Nil() => ScalaNil
+ case Cons(h, t) => h :: listToScala(t)
+ }
+
+ @ignore
+ @extern
+ implicit def listToString(l: List[Int]): String = {
+ l.map(_.toChar).mkString("")
+ }
+
+
+}
diff --git a/testcases/extern/EditorSimple.scala b/testcases/extern/EditorSimple.scala
new file mode 100644
index 0000000000000000000000000000000000000000..888f09debaa25c7223759470105d333b30148746
--- /dev/null
+++ b/testcases/extern/EditorSimple.scala
@@ -0,0 +1,170 @@
+import leon.lang._
+import leon.annotation._
+import leon.lang.synthesis._
+import leon.collection._
+import scala.reflect.runtime.universe._
+import scala.reflect.api.{TypeCreator, Universe, Mirror}
+
+
+import scala.collection.immutable.{List => ScalaList, Nil => ScalaNil}
+
+object Editor {
+ abstract class Mode
+ case object Edit extends Mode
+ case object Quitted extends Mode
+
+ case class State(line: List[Int], cursor: Int, buffer: List[Int], actions: List[Action], mode: Mode) {
+ def setLine(l: List[Int]) = State(l, cursor, buffer, actions, mode)
+ def setCursor(c: Int) = State(line, c, buffer, actions, mode)
+ def setBuffer(b: List[Int]) = State(line, cursor, b, actions, mode)
+ def addAction(a: Action) = State(line, cursor, buffer, Cons(a, actions), mode)
+ def setMode(m: Mode) = State(line, cursor, buffer, actions, m)
+ }
+
+ sealed abstract class Action
+ case object Unknown extends Action
+ case object Write extends Action
+ case object Quit extends Action
+ case class MoveCursor(to: Int) extends Action
+ case object Replace extends Action
+ case object Erase extends Action
+ case class Content(l: List[Int]) extends Action
+
+ //@extern
+ //def getCommand(): List[Int] = {
+ // print("> ")
+ // readLine().toList.map(_.toInt)
+ //}
+
+ def getCommand()(implicit o: Oracle[List[Int]]): List[Int] = {
+ ???
+ }
+
+ @extern
+ def unknown() = {
+ println("?")
+ }
+
+ @extern
+ def displayState(s: State) = {
+ println(" | Line : "+listToString(s.line))
+ println(" | Cursor : "+(" "*s.cursor)+"^")
+ println(" | Buffer : "+listToString(s.buffer))
+ println(" | A* : "+s.actions.collect {
+ case Content(l) => "Content("+listToString(l)+")"
+ case a => a.toString
+ }.mkString(", "))
+ }
+
+ @extern
+ def display(input: List[Int], a: Action, s: State) = {
+ println(" | Input : "+listToString(input))
+ println(" | Action : "+a)
+ println(" ~~~~~~~~~~~~~~~~~~~")
+ displayState(s)
+ }
+
+ def replStep(state: State)(implicit o: Oracle[List[Int]]): State = {
+ if (state.mode == Quitted) {
+ state
+ } else {
+ val i = getCommand()
+ val a = getAction(i, state)
+
+ doAction(state, a)
+ }
+ }
+
+ def getAction(input: List[Int], state: State): Action = {
+ if (input == Cons(113, Nil())) {
+ Quit
+ } else if (input == Cons(100, Nil())) {
+ Erase
+ } else if (input == Cons(94, Nil())) {
+ MoveCursor(0)
+ } else if (input == Cons(36, Nil())) {
+ MoveCursor(-1)
+ } else if (input == Cons(114, Nil())) {
+ Replace
+ } else if (input == Cons(119, Nil())) {
+ Write
+ } else if (input.size > 1) {
+ Content(input)
+ } else {
+ Unknown
+ }
+ }
+
+ def doAction(state: State, action: Action): State = {
+ val c = state.cursor
+ val l = state.line
+
+
+ val ns = (action, state.actions) match {
+ case (Content(cnt), Cons(Write, _)) =>
+ val nl = l.take(c) ++ cnt ++ l.drop(c)
+ state.setLine(nl).setCursor(c + cnt.size)
+ case (Content(cnt), Cons(Replace, _)) =>
+ val nl = l.take(c) ++ cnt ++ l.drop(c+cnt.size)
+ state.setLine(nl).setCursor(c + cnt.size)
+ case (MoveCursor(i), _) =>
+ if (i < 0) {
+ state.setCursor(state.line.size+1+i)
+ } else {
+ state.setCursor(i)
+ }
+ case (Erase, _) =>
+ state.setLine(Nil()).setCursor(0)
+ case (Quit, _) =>
+ state.setMode(Quitted)
+ case (Unknown, _) =>
+ //unknown()
+ state
+ case _ =>
+ state
+ }
+
+ ns.addAction(action)
+ }
+
+ def repl() = {
+ val finalState = {
+ withOracle { implicit o: Oracle[List[Int]] =>
+ {
+ val state = State(Nil(), 0, Nil(), Nil(), Edit)
+ val res = replStep(replStep(replStep(state)(o.left))(o.right.left))(o.right.right.left)
+ val tmp = displayState(res)
+ res
+ } ensuring {
+ s => s.line == Cons(97, Cons(97, Cons(97, Nil()))) && s.mode == Quitted
+ }
+ }
+ }
+ finalState
+ }
+
+ @ignore
+ @extern
+ implicit def scalaToList[T](l: ScalaList[T]): List[T] = {
+ l.foldRight[List[T]](Nil())( (e, l) => Cons(e, l) )
+ }
+
+ @ignore
+ @extern
+ implicit def listToScala[T](l: List[T]): ScalaList[T] = l match {
+ case Nil() => ScalaNil
+ case Cons(h, t) => h :: listToScala(t)
+ }
+
+ @ignore
+ @extern
+ implicit def listToString(l: List[Int]): String = {
+ l.map(_.toChar).mkString("")
+ }
+
+ @ignore
+ @extern
+ def asList(l: String): List[Int] = {
+ l.toList.map(_.toInt)
+ }
+}
diff --git a/testcases/extern/Game.scala b/testcases/extern/Game.scala
new file mode 100644
index 0000000000000000000000000000000000000000..fc365d8109711e37a11ba9c5861548ec5f08ca9c
--- /dev/null
+++ b/testcases/extern/Game.scala
@@ -0,0 +1,311 @@
+import leon.lang._
+import leon.annotation._
+import leon.lang.synthesis._
+import leon.collection._
+
+object Test {
+ case class Pos(x: Int, y: Int) {
+ def up = Pos(x, y-1)
+ def down = Pos(x, y+1)
+ def left = Pos(x-1, y)
+ def right = Pos(x+1, y)
+
+ // Simple over aproximation of the distance
+ def distance(o: Pos) = {
+ val dx = o.x-x
+ val dy = o.y-y
+
+ (dx*dx + dy*dy)
+ }
+
+ def update(a: Action) = a match {
+ case MoveUp =>
+ up
+ case MoveDown =>
+ down
+ case MoveLeft =>
+ left
+ case MoveRight =>
+ right
+ case Noop =>
+ this
+ }
+ }
+
+ case class Map(walls: Set[Pos], size: Pos) {
+ // Returns whether a certain position is a valid position to be in given
+ // the map
+ def isValidPos(p: Pos): Boolean = {
+ p.x >= 0 && p.y >= 0 &&
+ p.x < size.x && p.y < size.y &&
+ !(walls contains p)
+ }
+
+ def allValidPos(lp: List[Pos]): Boolean = lp match {
+ case Cons(h, t) => isValidPos(h) && allValidPos(t)
+ case Nil() => true
+ }
+ }
+
+ abstract class Action;
+ case object MoveUp extends Action
+ case object MoveDown extends Action
+ case object MoveLeft extends Action
+ case object MoveRight extends Action
+ case object Noop extends Action
+
+ case class Game(player: Pos,
+ monsters: List[Pos],
+ map: Map) {
+
+ def isValidAction(pos: Pos, action: Action) = {
+ val np = pos.update(action)
+ map.isValidPos(np)
+ }
+
+ def isDead = {
+ isAtPositions(player, monsters)
+ }
+
+ def isAtPositions(p: Pos, lp: List[Pos]): Boolean = lp match {
+ case Cons(h,t) => (h == p) || isAtPositions(p, t)
+ case _ => false
+ }
+
+ def isValid = {
+ map.isValidPos(player) &&
+ map.allValidPos(monsters)
+ }
+
+ def isRunning = !isDead
+ }
+
+ def step(g: Game)(implicit o: Oracle[Action]): Game = {
+ if (g.isDead) {
+ g
+ } else {
+ val g1 = stepPlayer(g)
+ Game(g1.player, stepMonsters(g1, g1.monsters), g1.map)
+ }
+ }
+
+ def steps(g: Game, b: Int)(implicit o: Oracle[Action]): Game = {
+ if (b <= 0 || g.isDead) {
+ g
+ } else {
+ steps(step(g)(o.left), b-1)(o.right)
+ }
+ }
+
+ def gameStep(g: Game)(implicit o: Oracle[Action]): Game = {
+ val u = display(g)
+ //withOracle { implicit o: Oracle[Action] => {
+ steps(g, 1)
+ //step(step(g))
+ // step(step(g)(o.left))(o.right)
+ //} ensuring { g => !g.isDead }}
+ }
+
+ def play(g: Game)(implicit o: Oracle[Action]): Game = {
+ val r = gameStep(g)(o.left)
+ if (r.isDead) {
+ r
+ } else {
+ play(r)(o.left)
+ }
+ }
+
+ def stepMonster(g: Game, oldPos: Pos): Pos = {
+ val a = choose { a: Action =>
+ bestTowards(g, oldPos, a, g.player)
+ }
+
+ oldPos.update(a)
+ }
+
+ def bestTowards(g: Game, old: Pos, action: Action, target: Pos): Boolean = {
+ def metric(a: Action): Int = {
+ old.update(a).distance(target)
+ }
+
+ def betterThan(a: Action, other: Action): Boolean = {
+ !g.isValidAction(old, other) || (metric(a) <= metric(other))
+ }
+
+ g.isValidAction(old, action) &&
+ betterThan(action, MoveUp) &&
+ betterThan(action, MoveDown) &&
+ betterThan(action, MoveLeft) &&
+ betterThan(action, MoveRight) &&
+ betterThan(action, Noop)
+ }
+
+ def stepMonsters(g: Game, lp: List[Pos]): List[Pos] = lp match {
+ case Cons(h,t) => Cons(stepMonster(g, h), stepMonsters(g, t))
+ case Nil() => Nil()
+ }
+
+ def stepPlayer(g: Game)(implicit o: Oracle[Action]) = {
+ val action: Action = ???
+
+ val np = g.player.update(action)
+
+ Game(if (g.map.isValidPos(np)) np else g.player, g.monsters, g.map)
+ }
+
+ def stepPlayerTmp(g: Game) = {
+ val np = withOracle{ implicit o: Oracle[Action] => {
+ val action: Action = ???
+
+ g.player.update(action)
+ } ensuring { g.map.isValidPos(_) }}
+
+ Game(if (g.map.isValidPos(np)) np else g.player, g.monsters, g.map)
+ }
+
+ @extern
+ def display(g: Game): Int = {
+ print("\033[2J\033[1;1H")
+ print(" ")
+ for (x <- 0 until g.map.size.x) {
+ print(x)
+ }
+ println
+ print(" â•”")
+ for (x <- 0 until g.map.size.x) {
+ print('â•')
+ }
+ println('â•—')
+ for (y <- 0 until g.map.size.y) {
+ print(y+" â•‘")
+ for (x <- 0 until g.map.size.x) {
+ val c = Pos(x,y)
+ if (g.map.walls contains c) {
+ print('â–’')
+ } else if (g.player == c) {
+ if (g.isDead) {
+ print(Console.RED+Console.BOLD+"☠"+Console.RESET)
+ } else {
+ print(Console.GREEN+"☺"+Console.RESET)
+ }
+ } else if (g.isAtPositions(c, g.monsters)) {
+ print(Console.RED+"X"+Console.RESET)
+ } else {
+ print(" ")
+ }
+ }
+ println('â•‘')
+ }
+ print(" â•š")
+ for (x <- 0 until g.map.size.x) {
+ print('â•')
+ }
+ println('â•')
+
+ 42
+ }
+
+ @ignore
+ def foreach[A](l: List[A], f: A => Unit): Unit = l match {
+ case Cons(h, t) => f(h); foreach(t, f)
+ case Nil() =>
+ }
+
+ @extern
+ abstract class OracleSource[T] extends Oracle[T] {
+ def branch: OracleSource[T]
+ def value: T
+
+ lazy val v: T = value
+ lazy val l: OracleSource[T] = branch
+ lazy val r: OracleSource[T] = branch
+
+ override def head: T = v
+ override def left: Oracle[T] = l
+ override def right: Oracle[T] = r
+ }
+
+ @extern
+ class Keyboard extends OracleSource[Action] {
+ def branch = new Keyboard
+ def value = {
+ import scala.tools.jline._
+
+ var askAgain = false
+ var action: Action = Noop
+
+ val t = new UnixTerminal()
+
+ try {
+ t.init()
+
+ do {
+ if (askAgain) println("?")
+ askAgain = false
+
+ t.readVirtualKey(System.in) match {
+ case 16 =>
+ action = MoveUp
+ case 14 =>
+ action = MoveDown
+ case 6 =>
+ action = MoveRight
+ case 2 =>
+ action = MoveLeft
+ case a =>
+ println("Got "+a)
+ askAgain = true
+ }
+
+ } while(askAgain)
+
+ } finally {
+ t.restore()
+ }
+
+ action
+ }
+ }
+
+ @extern
+ class Random extends OracleSource[Action] {
+ def value = {
+ scala.util.Random.nextInt(4) match {
+ case 0 =>
+ MoveUp
+ case 1 =>
+ MoveDown
+ case 2 =>
+ MoveLeft
+ case 3 =>
+ MoveRight
+ case _ =>
+ MoveUp
+ }
+ }
+
+ def branch = new Random
+ }
+
+ @extern
+ def getOracle(): Oracle[Action] = {
+ new Keyboard
+ }
+
+ @extern
+ def pause(): Unit = {
+ readLine
+ }
+
+ def start() = {
+ val map = Map(Set(Pos(2,2), Pos(2,3), Pos(4,4), Pos(5,5)), Pos(10,10))
+ val monsters = Cons(Pos(8,5), Cons(Pos(6,2), Nil()))
+ val init = Game(Pos(0,0), monsters, map)
+
+ val res = play(init)(getOracle())
+
+ val tmp = display(res)
+
+ res
+ }
+}
diff --git a/testcases/extern/GameDemo.scala b/testcases/extern/GameDemo.scala
new file mode 100644
index 0000000000000000000000000000000000000000..fef85891a44d37b1a29474d505709a7af53ab0c8
--- /dev/null
+++ b/testcases/extern/GameDemo.scala
@@ -0,0 +1,294 @@
+import leon.lang._
+import leon.annotation._
+import leon.lang.synthesis._
+import leon.collection._
+
+object Test {
+ case class Pos(x: Int, y: Int) {
+ def up = Pos(x, y-1)
+ def down = Pos(x, y+1)
+ def left = Pos(x-1, y)
+ def right = Pos(x+1, y)
+
+ // Simple over aproximation of the distance
+ def distance(o: Pos) = {
+ val dx = o.x-x
+ val dy = o.y-y
+
+ (dx*dx + dy*dy)
+ }
+
+ def update(a: Action) = a match {
+ case MoveUp =>
+ up
+ case MoveDown =>
+ down
+ case MoveLeft =>
+ left
+ case MoveRight =>
+ right
+ case Noop =>
+ this
+ }
+ }
+
+ case class Map(walls: Set[Pos], size: Pos) {
+ // Returns whether a certain position is a valid position to be in given
+ // the map
+ def isValidPos(p: Pos): Boolean = {
+ p.x >= 0 && p.y >= 0 &&
+ p.x < size.x && p.y < size.y &&
+ !(walls contains p)
+ }
+
+ def allValidPos(lp: List[Pos]): Boolean = lp match {
+ case Cons(h, t) => isValidPos(h) && allValidPos(t)
+ case Nil() => true
+ }
+ }
+
+ abstract class Action;
+ case object MoveUp extends Action
+ case object MoveDown extends Action
+ case object MoveLeft extends Action
+ case object MoveRight extends Action
+ case object Noop extends Action
+
+ case class Game(player: Pos,
+ monsters: List[Pos],
+ map: Map) {
+
+ def isValidAction(pos: Pos, action: Action) = {
+ val np = pos.update(action)
+ map.isValidPos(np)
+ }
+
+ def isDead = {
+ isAtPositions(player, monsters)
+ }
+
+ def isAtPositions(p: Pos, lp: List[Pos]): Boolean = lp match {
+ case Cons(h,t) => (h == p) || isAtPositions(p, t)
+ case _ => false
+ }
+
+ def isValid = {
+ map.isValidPos(player) &&
+ map.allValidPos(monsters)
+ }
+
+ def isRunning = !isDead
+ }
+
+ def step(g: Game)(implicit o: Oracle[Action]): Game = {
+ if (g.isDead) {
+ g
+ } else {
+ val g1 = stepPlayer(g)
+ Game(g1.player, stepMonsters(g1, g1.monsters), g1.map)
+ }
+ }
+
+ def gameStep(g: Game)(implicit o: Oracle[Action]): Game = {
+ val u = display(g)
+ //withOracle { implicit o: Oracle[Action] => {
+ step(g)
+ //} ensuring { g => !g.isDead }}
+ }
+
+ def play(g: Game)(implicit o: Oracle[Action]): Game = {
+ val r = gameStep(g)(o.left)
+ if (r.isDead) {
+ r
+ } else {
+ play(r)(o.left)
+ }
+ }
+
+
+ def stepMonster(g: Game, oldPos: Pos): Pos = {
+ val a = choose { a: Action =>
+ bestTowards(g, oldPos, a, g.player)
+ }
+
+ oldPos.update(a)
+ }
+
+ def stepPlayer(g: Game)(implicit o: Oracle[Action]) = {
+ //withOracle { implicit o: Oracle[Action] => {
+ val action: Action = ???
+
+ val np = g.player.update(action)
+
+ Game(if (g.map.isValidPos(np)) np else g.player, g.monsters, g.map)
+ //} ensuring { g => !g.isDead }}
+ }
+
+ def bestTowards(g: Game, old: Pos, action: Action, target: Pos): Boolean = {
+ def metric(a: Action): Int = {
+ old.update(a).distance(target)
+ }
+
+ def betterThan(a: Action, other: Action): Boolean = {
+ !g.isValidAction(old, other) || (metric(a) <= metric(other))
+ }
+
+ g.isValidAction(old, action) &&
+ betterThan(action, MoveUp) &&
+ betterThan(action, MoveDown) &&
+ betterThan(action, MoveLeft) &&
+ betterThan(action, MoveRight) &&
+ betterThan(action, Noop)
+ }
+
+ def stepMonsters(g: Game, lp: List[Pos]): List[Pos] = lp match {
+ case Cons(h,t) => Cons(stepMonster(g, h), stepMonsters(g, t))
+ case Nil() => Nil()
+ }
+
+ @extern
+ def display(g: Game): Int = {
+ print("\033[2J\033[1;1H")
+ print(" ")
+ for (x <- 0 until g.map.size.x) {
+ print(x)
+ }
+ println
+ print(" â•”")
+ for (x <- 0 until g.map.size.x) {
+ print('â•')
+ }
+ println('â•—')
+ for (y <- 0 until g.map.size.y) {
+ print(y+" â•‘")
+ for (x <- 0 until g.map.size.x) {
+ val c = Pos(x,y)
+ if (g.map.walls contains c) {
+ print('â–’')
+ } else if (g.player == c) {
+ if (g.isDead) {
+ print(Console.RED+Console.BOLD+"☠"+Console.RESET)
+ } else {
+ print(Console.GREEN+"☺"+Console.RESET)
+ }
+ } else if (g.isAtPositions(c, g.monsters)) {
+ print(Console.RED+"X"+Console.RESET)
+ } else {
+ print(" ")
+ }
+ }
+ println('â•‘')
+ }
+ print(" â•š")
+ for (x <- 0 until g.map.size.x) {
+ print('â•')
+ }
+ println('â•')
+
+ 42
+ }
+
+ @ignore
+ def foreach[A](l: List[A], f: A => Unit): Unit = l match {
+ case Cons(h, t) => f(h); foreach(t, f)
+ case Nil() =>
+ }
+
+ @extern
+ abstract class OracleSource[T] extends Oracle[T] {
+ def branch: OracleSource[T]
+ def value: T
+
+ lazy val v: T = value
+ lazy val l: OracleSource[T] = branch
+ lazy val r: OracleSource[T] = branch
+
+ override def head: T = v
+ override def left: Oracle[T] = l
+ override def right: Oracle[T] = r
+ }
+
+ @extern
+ class Keyboard extends OracleSource[Action] {
+ def branch = new Keyboard
+ def value = {
+ import scala.tools.jline._
+
+ var askAgain = false
+ var action: Action = Noop
+
+ val t = new UnixTerminal()
+
+ try {
+ t.init()
+
+ do {
+ if (askAgain) println("?")
+ askAgain = false
+
+ t.readVirtualKey(System.in) match {
+ case 16 =>
+ action = MoveUp
+ case 14 =>
+ action = MoveDown
+ case 6 =>
+ action = MoveRight
+ case 2 =>
+ action = MoveLeft
+ case a =>
+ println("Got "+a)
+ askAgain = true
+ }
+
+ } while(askAgain)
+
+ } finally {
+ t.restore()
+ }
+
+ action
+ }
+ }
+
+ @extern
+ class Random extends OracleSource[Action] {
+ def value = {
+ scala.util.Random.nextInt(4) match {
+ case 0 =>
+ MoveUp
+ case 1 =>
+ MoveDown
+ case 2 =>
+ MoveLeft
+ case 3 =>
+ MoveRight
+ case _ =>
+ MoveUp
+ }
+ }
+
+ def branch = new Random
+ }
+
+ @extern
+ def getOracle(): Oracle[Action] = {
+ new Keyboard
+ }
+
+ @extern
+ def pause(): Unit = {
+ readLine
+ }
+
+ def start() = {
+ val map = Map(Set(Pos(2,2), Pos(2,3), Pos(4,4), Pos(5,5)), Pos(10,10))
+ val monsters = Cons(Pos(8,5), Cons(Pos(6,2), Nil()))
+ val init = Game(Pos(0,0), monsters, map)
+
+ val res = play(init)(getOracle())
+
+ val tmp = display(res)
+
+ res
+ }
+}
diff --git a/testcases/extern/GameNoSet.scala b/testcases/extern/GameNoSet.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b167933bfee929eb1f8e39d9135796f436320eef
--- /dev/null
+++ b/testcases/extern/GameNoSet.scala
@@ -0,0 +1,312 @@
+import leon.lang._
+import leon.annotation._
+import leon.lang.synthesis._
+import leon.collection._
+
+object Test {
+ case class Pos(x: Int, y: Int) {
+ def up = Pos(x, y-1)
+ def down = Pos(x, y+1)
+ def left = Pos(x-1, y)
+ def right = Pos(x+1, y)
+
+ // Simple over aproximation of the distance
+ def distance(o: Pos) = {
+ val dx = o.x-x
+ val dy = o.y-y
+
+ (dx*dx + dy*dy)
+ }
+
+ def update(a: Action) = a match {
+ case MoveUp =>
+ up
+ case MoveDown =>
+ down
+ case MoveLeft =>
+ left
+ case MoveRight =>
+ right
+ case Noop =>
+ this
+ }
+
+ def isAtAny(lp: List[Pos]): Boolean = lp match {
+ case Cons(h,t) => (h == this) || isAtAny(t)
+ case _ => false
+ }
+ }
+
+ case class Map(walls: List[Pos], size: Pos) {
+ // Returns whether a certain position is a valid position to be in given
+ // the map
+ def isValidPos(p: Pos): Boolean = {
+ p.x >= 0 && p.y >= 0 &&
+ p.x < size.x && p.y < size.y &&
+ !p.isAtAny(walls)
+ }
+
+ def allValidPos(lp: List[Pos]): Boolean = lp match {
+ case Cons(h, t) => isValidPos(h) && allValidPos(t)
+ case Nil() => true
+ }
+ }
+
+ abstract class Action;
+ case object MoveUp extends Action
+ case object MoveDown extends Action
+ case object MoveLeft extends Action
+ case object MoveRight extends Action
+ case object Noop extends Action
+
+ case class Game(player: Pos,
+ monsters: List[Pos],
+ map: Map) {
+
+ def isValidAction(pos: Pos, action: Action) = {
+ val np = pos.update(action)
+ map.isValidPos(np)
+ }
+
+ def isDead = {
+ player.isAtAny(monsters)
+ }
+
+
+ def isValid = {
+ map.isValidPos(player) &&
+ map.allValidPos(monsters)
+ }
+
+ def isRunning = !isDead
+ }
+
+ def step(g: Game)(implicit o: Oracle[Action]): Game = {
+ if (g.isDead) {
+ g
+ } else {
+ val g1 = stepPlayer(g)
+ Game(g1.player, stepMonsters(g1, g1.monsters), g1.map)
+ }
+ }
+
+ def steps(g: Game, b: Int)(implicit o: Oracle[Action]): Game = {
+ if (b <= 0 || g.isDead) {
+ g
+ } else {
+ steps(step(g)(o.left), b-1)(o.right)
+ }
+ }
+
+ def gameStep(g: Game)(implicit o: Oracle[Action]): Game = {
+ val u = display(g)
+ //withOracle { implicit o: Oracle[Action] => {
+ steps(g, 1)
+ //step(step(g))
+ // step(step(g)(o.left))(o.right)
+ //} ensuring { g => !g.isDead }}
+ }
+
+ def play(g: Game)(implicit o: Oracle[Action]): Game = {
+ val r = gameStep(g)(o.left)
+ if (r.isDead) {
+ r
+ } else {
+ play(r)(o.left)
+ }
+ }
+
+ def stepMonster(g: Game, oldPos: Pos): Pos = {
+ val a = choose { a: Action =>
+ bestTowards(g, oldPos, a, g.player)
+ }
+
+ oldPos.update(a)
+ }
+
+ def bestTowards(g: Game, old: Pos, action: Action, target: Pos): Boolean = {
+ def metric(a: Action): Int = {
+ old.update(a).distance(target)
+ }
+
+ def betterThan(a: Action, other: Action): Boolean = {
+ !g.isValidAction(old, other) || (metric(a) <= metric(other))
+ }
+
+ g.isValidAction(old, action) &&
+ betterThan(action, MoveUp) &&
+ betterThan(action, MoveDown) &&
+ betterThan(action, MoveLeft) &&
+ betterThan(action, MoveRight) &&
+ betterThan(action, Noop)
+ }
+
+ def stepMonsters(g: Game, lp: List[Pos]): List[Pos] = lp match {
+ case Cons(h,t) => Cons(stepMonster(g, h), stepMonsters(g, t))
+ case Nil() => Nil()
+ }
+
+ def stepPlayer(g: Game)(implicit o: Oracle[Action]) = {
+ val action: Action = ???
+
+ val np = g.player.update(action)
+
+ Game(if (g.map.isValidPos(np)) np else g.player, g.monsters, g.map)
+ }
+
+ def stepPlayerTmp(g: Game) = {
+ val np = withOracle{ implicit o: Oracle[Action] => {
+ val action: Action = ???
+
+ g.player.update(action)
+ } ensuring { g.map.isValidPos(_) }}
+
+ Game(if (g.map.isValidPos(np)) np else g.player, g.monsters, g.map)
+ }
+
+ @extern
+ def display(g: Game): Int = {
+ print("\033[2J\033[1;1H")
+ print(" ")
+ for (x <- 0 until g.map.size.x) {
+ print(x)
+ }
+ println
+ print(" â•”")
+ for (x <- 0 until g.map.size.x) {
+ print('â•')
+ }
+ println('â•—')
+ for (y <- 0 until g.map.size.y) {
+ print(y+" â•‘")
+ for (x <- 0 until g.map.size.x) {
+ val c = Pos(x,y)
+ if (c.isAtAny(g.map.walls)) {
+ print('â–’')
+ } else if (g.player == c) {
+ if (g.isDead) {
+ print(Console.RED+Console.BOLD+"☠"+Console.RESET)
+ } else {
+ print(Console.GREEN+"☺"+Console.RESET)
+ }
+ } else if (c.isAtAny(g.monsters)) {
+ print(Console.RED+"X"+Console.RESET)
+ } else {
+ print(" ")
+ }
+ }
+ println('â•‘')
+ }
+ print(" â•š")
+ for (x <- 0 until g.map.size.x) {
+ print('â•')
+ }
+ println('â•')
+
+ 42
+ }
+
+ @ignore
+ def foreach[A](l: List[A], f: A => Unit): Unit = l match {
+ case Cons(h, t) => f(h); foreach(t, f)
+ case Nil() =>
+ }
+
+ @extern
+ abstract class OracleSource[T] extends Oracle[T] {
+ def branch: OracleSource[T]
+ def value: T
+
+ lazy val v: T = value
+ lazy val l: OracleSource[T] = branch
+ lazy val r: OracleSource[T] = branch
+
+ override def head: T = v
+ override def left: Oracle[T] = l
+ override def right: Oracle[T] = r
+ }
+
+ @extern
+ class Keyboard extends OracleSource[Action] {
+ def branch = new Keyboard
+ def value = {
+ import scala.tools.jline._
+
+ var askAgain = false
+ var action: Action = Noop
+
+ val t = new UnixTerminal()
+
+ try {
+ t.init()
+
+ do {
+ if (askAgain) println("?")
+ askAgain = false
+
+ t.readVirtualKey(System.in) match {
+ case 16 =>
+ action = MoveUp
+ case 14 =>
+ action = MoveDown
+ case 6 =>
+ action = MoveRight
+ case 2 =>
+ action = MoveLeft
+ case a =>
+ println("Got "+a)
+ askAgain = true
+ }
+
+ } while(askAgain)
+
+ } finally {
+ t.restore()
+ }
+
+ action
+ }
+ }
+
+ @extern
+ class Random extends OracleSource[Action] {
+ def value = {
+ scala.util.Random.nextInt(4) match {
+ case 0 =>
+ MoveUp
+ case 1 =>
+ MoveDown
+ case 2 =>
+ MoveLeft
+ case 3 =>
+ MoveRight
+ case _ =>
+ MoveUp
+ }
+ }
+
+ def branch = new Random
+ }
+
+ @extern
+ def getOracle(): Oracle[Action] = {
+ new Keyboard
+ }
+
+ @extern
+ def pause(): Unit = {
+ readLine
+ }
+
+ def start() = {
+ val map = Map(Cons(Pos(2,2), Cons(Pos(2,3), Nil())), Pos(10,10))
+ val monsters = Cons(Pos(8,5), Cons(Pos(6,2), Nil()))
+ val init = Game(Pos(0,0), monsters, map)
+
+ val res = play(init)(getOracle())
+
+ val tmp = display(res)
+
+ res
+ }
+}
diff --git a/testcases/extern/GameSimpler.scala b/testcases/extern/GameSimpler.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6249ad535ddf00bf061b7ce3b215d1f73dc3de17
--- /dev/null
+++ b/testcases/extern/GameSimpler.scala
@@ -0,0 +1,293 @@
+import leon.lang._
+import leon.annotation._
+import leon.lang.synthesis._
+import leon.collection._
+
+object Test {
+ case class Pos(x: Int, y: Int) {
+ def up = Pos(x, y-1)
+ def down = Pos(x, y+1)
+ def left = Pos(x-1, y)
+ def right = Pos(x+1, y)
+
+ // Simple over aproximation of the distance
+ def distance(o: Pos) = {
+ val dx = o.x-x
+ val dy = o.y-y
+
+ (dx*dx + dy*dy)
+ }
+
+ def update(a: Action) = a match {
+ case MoveUp =>
+ up
+ case MoveDown =>
+ down
+ case MoveLeft =>
+ left
+ case MoveRight =>
+ right
+ case Noop =>
+ this
+ }
+ }
+
+ case class Map(size: Pos) {
+ // Returns whether a certain position is a valid position to be in given
+ // the map
+ def isValidPos(p: Pos): Boolean = {
+ p.x >= 0 && p.y >= 0 &&
+ p.x < size.x && p.y < size.y
+ }
+ }
+
+ abstract class Action;
+ case object MoveUp extends Action
+ case object MoveDown extends Action
+ case object MoveLeft extends Action
+ case object MoveRight extends Action
+ case object Noop extends Action
+
+ case class Game(player: Pos,
+ monster: Pos,
+ map: Map) {
+
+ def isValidAction(pos: Pos, action: Action) = {
+ val np = pos.update(action)
+ map.isValidPos(np)
+ }
+
+ def isDead = {
+ player == monster
+ }
+
+ def isValid = {
+ map.isValidPos(player) &&
+ map.isValidPos(monster)
+ }
+
+ def isRunning = !isDead
+ }
+
+ def step(g: Game)(implicit o: Oracle[Action]): Game = {
+ if (g.isDead) {
+ g
+ } else {
+ val g1 = stepPlayer(g)
+ Game(g1.player, stepMonster(g1, g1.monster), g1.map)
+ }
+ }
+
+ def steps(g: Game, b: Int)(implicit o: Oracle[Action]): Game = {
+ if (b <= 0 || g.isDead) {
+ g
+ } else {
+ steps(step(g)(o.left), b-1)(o.right)
+ }
+ }
+
+ def gameStep(g: Game)(implicit o: Oracle[Action]): Game = {
+ val u = display(g)
+ withOracle { implicit o: Oracle[Action] => {
+ steps(g, 2)
+ //step(step(g))
+ // step(step(g)(o.left))(o.right)
+ } ensuring { g => !g.isDead }}
+ }
+
+ def play(g: Game)(implicit o: Oracle[Action]): Game = {
+ val r = gameStep(g)(o.left)
+ if (r.isDead) {
+ r
+ } else {
+ play(r)(o.left)
+ }
+ }
+
+ def stepMonster(g: Game, oldPos: Pos): Pos = {
+ val a = choose { a: Action =>
+ bestTowards(g, oldPos, a, g.player)
+ }
+
+ oldPos.update(a)
+ }
+
+ def bestTowards(g: Game, old: Pos, action: Action, target: Pos): Boolean = {
+ def metric(a: Action): Int = {
+ old.update(a).distance(target)
+ }
+
+ def betterThan(a: Action, other: Action): Boolean = {
+ !g.isValidAction(old, other) || (metric(a) <= metric(other))
+ }
+
+ g.isValidAction(old, action) &&
+ betterThan(action, MoveUp) &&
+ betterThan(action, MoveDown) &&
+ betterThan(action, MoveLeft) &&
+ betterThan(action, MoveRight) &&
+ betterThan(action, Noop)
+ }
+
+
+ def stepPlayer(g: Game)(implicit o: Oracle[Action]) = {
+ val action: Action = ???
+
+ val np = g.player.update(action)
+
+ Game(if (g.map.isValidPos(np)) np else g.player, g.monster, g.map)
+ }
+
+ def stepPlayerTmp(g: Game) = {
+ val np = withOracle{ implicit o: Oracle[Action] => {
+ val action: Action = ???
+
+ g.player.update(action)
+ } ensuring { g.map.isValidPos(_) }}
+
+ Game(if (g.map.isValidPos(np)) np else g.player, g.monster, g.map)
+ }
+
+ @extern
+ def display(g: Game): Int = {
+ print("\033[2J\033[1;1H")
+ print(" ")
+ for (x <- 0 until g.map.size.x) {
+ print(x)
+ }
+ println
+ print(" â•”")
+ for (x <- 0 until g.map.size.x) {
+ print('â•')
+ }
+ println('â•—')
+ for (y <- 0 until g.map.size.y) {
+ print(y+" â•‘")
+ for (x <- 0 until g.map.size.x) {
+ val c = Pos(x,y)
+ if (g.player == c) {
+ if (g.isDead) {
+ print(Console.RED+Console.BOLD+"☠"+Console.RESET)
+ } else {
+ print(Console.GREEN+"☺"+Console.RESET)
+ }
+ } else if (c == g.monster) {
+ print(Console.RED+"X"+Console.RESET)
+ } else {
+ print(" ")
+ }
+ }
+ println('â•‘')
+ }
+ print(" â•š")
+ for (x <- 0 until g.map.size.x) {
+ print('â•')
+ }
+ println('â•')
+
+ 42
+ }
+
+ @ignore
+ def foreach[A](l: List[A], f: A => Unit): Unit = l match {
+ case Cons(h, t) => f(h); foreach(t, f)
+ case Nil() =>
+ }
+
+ @extern
+ abstract class OracleSource[T] extends Oracle[T] {
+ def branch: OracleSource[T]
+ def value: T
+
+ lazy val v: T = value
+ lazy val l: OracleSource[T] = branch
+ lazy val r: OracleSource[T] = branch
+
+ override def head: T = v
+ override def left: Oracle[T] = l
+ override def right: Oracle[T] = r
+ }
+
+ @extern
+ class Keyboard extends OracleSource[Action] {
+ def branch = new Keyboard
+ def value = {
+ import scala.tools.jline._
+
+ var askAgain = false
+ var action: Action = Noop
+
+ val t = new UnixTerminal()
+
+ try {
+ t.init()
+
+ do {
+ if (askAgain) println("?")
+ askAgain = false
+
+ t.readVirtualKey(System.in) match {
+ case 16 =>
+ action = MoveUp
+ case 14 =>
+ action = MoveDown
+ case 6 =>
+ action = MoveRight
+ case 2 =>
+ action = MoveLeft
+ case a =>
+ println("Got "+a)
+ askAgain = true
+ }
+
+ } while(askAgain)
+
+ } finally {
+ t.restore()
+ }
+
+ action
+ }
+ }
+
+ @extern
+ class Random extends OracleSource[Action] {
+ def value = {
+ scala.util.Random.nextInt(4) match {
+ case 0 =>
+ MoveUp
+ case 1 =>
+ MoveDown
+ case 2 =>
+ MoveLeft
+ case 3 =>
+ MoveRight
+ case _ =>
+ MoveUp
+ }
+ }
+
+ def branch = new Random
+ }
+
+ @extern
+ def getOracle(): Oracle[Action] = {
+ new Keyboard
+ }
+
+ @extern
+ def pause(): Unit = {
+ readLine
+ }
+
+ def start() = {
+ val map = Map(Pos(10,10))
+ val init = Game(Pos(0,0), Pos(3, 3), map)
+
+ val res = play(init)(getOracle())
+
+ val tmp = display(res)
+
+ res
+ }
+}
diff --git a/testcases/extern/features.scala b/testcases/extern/features.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6b3db19119aed089997bcec2592e8147e8222a19
--- /dev/null
+++ b/testcases/extern/features.scala
@@ -0,0 +1,102 @@
+package testextern
+
+import leon.lang._
+import leon.annotation._
+import leon.lang.synthesis._
+import leon.collection._
+
+object ExternTest {
+ // All types 1
+ def test1() = {
+ allTypes1(false, (1,2), ExternFoo(12), Bar(false))
+ }
+
+ // All types 2
+ def test2() = {
+ allTypes2(Set(1,2,3), Map(1->2))
+ }
+
+ // External function calling back
+ def test3() = {
+ testCallBack(51);
+ }
+
+ // External method
+ def test4() = {
+ Test(12).bar(21)
+ }
+
+ // Generics
+ def test5() = {
+ id(List[BigInt](1,2,3)).tail.head == 2
+ }
+
+ // Name encoding
+ def test6() = {
+ +*/!(1,2)
+ }
+
+ // Unit1
+ def test7() = {
+ testUnit(1, (), ((), 3))
+ }
+
+
+ def leonFun(a: BigInt): BigInt = {
+ choose((x: BigInt) => x > a && x <= a+1)
+ }
+
+
+
+ // External functions
+
+ @extern
+ def testCallBack(a: BigInt): BigInt = {
+ val f = new scala.collection.mutable.ArrayBuffer[BigInt]()
+ leonFun(a+1)
+ }
+
+ @extern
+ def +*/!(a: Int, b: BigInt): BigInt = {
+ println("asd")
+ b+b
+ }
+
+ @extern
+ def allTypes1(a: Boolean, b: (BigInt, BigInt), c: ExternFoo, d: Bar): (Boolean, (BigInt, BigInt), ExternFoo, Bar) = {
+ println("asd")
+ (a,b,c,d)
+ }
+
+ @extern
+ def allTypes2(s: Set[Int], m: Map[Int, Int]): (Set[Int], Map[Int, Int]) = {
+ println("asd")
+ (s,m)
+ }
+
+ @extern
+ def id[T](a: T): T = {
+ println("asd")
+ a
+ }
+
+ @extern
+ def testUnit(a: Int, b: Unit, c: (Unit, Int)): Unit = {
+ println("asd")
+ b
+ }
+
+ case class Test(a: Int) {
+ @extern
+ def bar(b: BigInt): BigInt = {
+ println("asd")
+ b*4+a
+ }
+ }
+
+ case class Bar(b: Boolean);
+}
+
+case class ExternFoo(a: BigInt) {
+ def leonMethod(z: Int): Int = z
+}