Tiny scripts for compiling and running with ordinary scalac and scala

Annotated incomplete matches in List and Option Leon library.
Removed out-of-place files.

Game.scala

-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)
-
-    def isValid(s: State) = {
-      x >= 0 && y >= 0 &&
-      x < s.map.size.x && y < s.map.size.y &&
-      !(s.map.walls contains this)
-    }
-
-    def distance(o: Pos) = {
-      (if (o.x < x) (x-o.x) else (o.x-x)) +
-      (if (o.y < y) (y-o.y) else (o.y-y))
-    }
-  }
-
-  case class Map(walls: Set[Pos], size: Pos)
-
-  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 Quit extends Action
-
-  case class State(pos: Pos,
-                   monster: Pos,
-                   stop: Boolean,
-                   map: Map) {
-
-    def isValid = {
-      pos.isValid(this) && monster.isValid(this)
-    }
-
-   }
-
-  def step(s: State)(implicit o: Oracle[Action]): State = {
-    require(s.isValid)
-
-    val u = display(s)
-
-    stepMonster(stepPlayer(s)(o.left))
-  }
-
-  def stepMonster(s: State) = {
-    require(s.isValid)
-    if (s.pos == s.monster) {
-      State(s.pos, s.monster, true, s.map)
-    } else {
-      val mp = choose {
-        (res: Pos) =>
-          res.distance(s.monster) <= 1 &&
-          res.distance(s.pos) <= s.monster.distance(s.pos) &&
-          res.isValid(s)
-      }
-      State(s.pos, mp, mp != s.pos, s.map)
-    }
-  } ensuring { _.isValid }
-
-  def stepPlayer(s: State)(implicit o: Oracle[Action]) = {
-    val action: Action = ???
-
-    val ns = action match {
-      case Quit =>
-        State(s.pos, s.monster, true, s.map)
-      case _ if s.stop =>
-        s
-      case MoveUp if s.pos.y > 0 =>
-        State(s.pos.up, s.monster, s.stop, s.map)
-      case MoveDown =>
-        State(s.pos.down, s.monster, s.stop, s.map)
-      case MoveLeft if s.pos.x > 0 =>
-        State(s.pos.left, s.monster, s.stop, s.map)
-      case MoveRight =>
-        State(s.pos.right, s.monster, s.stop, s.map)
-      case _ =>
-        s
-    }
-
-    if (ns.isValid) ns else s
-  }
-
-  def steps(s: State, b: Int)(implicit o: Oracle[Action]): State = {
-    if (b == 0 || s.stop) {
-      s
-    } else {
-      steps(step(s)(o), b-1)(o.right)
-    }
-  }
-
-  def play(s: State)(implicit o: Oracle[Action]): State = {
-    steps(s, -1)
-  }
-
-  @extern
-  def display(s: State): Int = {
-    print('╔')
-    for (x <- 0 until s.map.size.x) {
-      print('═')
-    }
-    println('╗')
-    for (y <- 0 until s.map.size.y) {
-      print('║')
-      for (x <- 0 until s.map.size.x) {
-        val c = Pos(x,y)
-        if (s.map.walls contains c) {
-          print('X')
-        } else if (s.pos == c) {
-          print('o')
-        } else if (s.monster == c) {
-          print('m')
-        } else {
-          print(" ")
-        }
-      }
-      println('║')
-    }
-    print('╚')
-    for (x <- 0 until s.map.size.x) {
-      print('═')
-    }
-    println('╝')
-
-    42
-  }
-
-  @extern
-  def main(args: Array[String]) {
-
-    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 = v
-      override def left = l
-      override def right = r
-    }
-
-    class Keyboard extends OracleSource[Action] {
-      def branch = new Keyboard
-      def value = {
-        var askAgain = false
-        var action: Action = Quit
-        do {
-          if (askAgain) println("?")
-          askAgain = false
-          print("> ")
-          readLine().trim match {
-            case "up" =>
-              action = MoveUp
-            case "down" =>
-              action = MoveDown
-            case "left" =>
-              action = MoveLeft
-            case "right" =>
-              action = MoveRight
-            case "quit" =>
-              action = Quit
-            case _ =>
-              askAgain = true
-          }
-        } while(askAgain)
-
-        action
-      }
-    }
-
-    class Random extends OracleSource[Action] {
-      def value = {
-        readLine()
-        scala.util.Random.nextInt(4) match {
-          case 0 =>
-            MoveUp
-          case 1 =>
-            MoveDown
-          case 2 =>
-            MoveLeft
-          case 3 =>
-            MoveRight
-          case _ =>
-            MoveUp
-        }
-      }
-
-      def branch = new Random
-    }
-
-    val map  = Map(Set(Pos(2,2), Pos(2,3), Pos(4,4), Pos(5,5)), Pos(10,10))
-    val init = State(Pos(0,0), Pos(4,5), false, map)
-
-    play(init)(new Random)
-  }
-
-  def test1() = {
-    withOracle{ o: Oracle[Action] =>
-      {
-        val map  = Map(Set(Pos(2,2), Pos(2,3), Pos(4,4), Pos(5,5)), Pos(10,10))
-        val init = State(Pos(0,0), Pos(4,4), false, map)
-
-        steps(init, 5)(o)
-      } ensuring {
-        _.pos == Pos(0,3)
-      }
-    }
-  }
-
-  def validStep(s: State) = {
-    require(s.map.size.x > 3 &&  s.map.size.y > 3 && s.pos != s.monster && s.isValid && !s.stop)
-
-    val ns = withOracle { o: Oracle[Action] =>
-      {
-        stepPlayer(s)(o)
-      } ensuring {
-        res => res.isValid && !res.stop
-      }
-    }
-    stepMonster(ns)
-  } ensuring {
-    res => res.isValid && !res.stop
-  }
-}

PERMISSIONS

-#!/bin/bash
-
-# Just editing this file won't affect the permissions. After editing it, you
-# also need to execute it.
-#
-# The creator of this repository is psuter.
-
-thisrepo="projects/leon-2.0"
-
-tail -2 "$0" | ssh git@laragit.epfl.ch setperms ${thisrepo}
-
-exit $_
-
-# **Do not** add new lines after the following two!
-WRITERS kuncak psuter rblanc edarulov hojjat ekneuss kandhada kuraj gvero
-READERS @lara mazimmer hardy amin

library/collection/List.scala

@@ -231,7 +231,7 @@ sealed abstract class List[T] {
 
   def init: List[T] = {
     require(!isEmpty)
-    (this match {
+    ((this : @unchecked) match {
       case Cons(h, Nil()) =>
         Nil[T]()
       case Cons(h, t) =>
@@ -244,7 +244,7 @@ sealed abstract class List[T] {
 
   def last: T = {
     require(!isEmpty)
-    this match {
+    (this : @unchecked) match {
       case Cons(h, Nil()) => h
       case Cons(_, t) => t.last
     }

library/lang/Option.scala

@@ -9,7 +9,7 @@ sealed abstract class Option[T] {
 
   def get : T = {
     require(this.isDefined)
-    this match {
+    (this : @unchecked) match {
       case Some(x) => x
     }
   }

scalacleon

+#!/bin/bash --posix
+# Assumes:
+#  - Leon home is stored in PATH_TO_LEON
+#  - we have xargs installed
+#  - ${SCALA_COMPILER} is on the path
+PATH_TO_LEON="./"  # assume we run from Leon home directory
+PATH_TO_LEON_LIB="${PATH_TO_LEON}/library/"
+OUT_CLASSES_DIR="./out-classes"
+SCALA_COMPILER="fsc"
+mkdir -p ${OUT_CLASSES_DIR}
+echo ========= Now invoking: ====================================
+echo ${SCALA_COMPILER} $(find ${PATH_TO_LEON_LIB} -name "*.scala" | xargs) $* -d ${OUT_CLASSES_DIR}
+echo ============================================================
+fsc -deprecation $(find ${PATH_TO_LEON_LIB} -name "*.scala" | xargs) $* -d ${OUT_CLASSES_DIR}
+echo ========= Done. ============================================
+echo Class files generated in directory: ${OUT_CLASSES_DIR}

scalaleon

+#!/bin/bash --posix
+# Assumes:
+#  - ${SCALA} is on the path
+OUT_CLASSES_DIR="./out-classes"
+SCALA="scala"
+if [[ -d ${OUT_CLASSES_DIR} ]] 
+then
+    scala -cp ${OUT_CLASSES_DIR} $*
+else
+    echo Script is designed to run after scalacleon
+fi