From 78d9da12bf49e72b97974c372f8826f7af950750 Mon Sep 17 00:00:00 2001 From: Viktor Kuncak <viktor.kuncak@epfl.ch> Date: Thu, 18 Jun 2015 17:52:57 +0200 Subject: [PATCH] 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 | 233 ---------------------------------- PERMISSIONS | 16 --- library/collection/List.scala | 4 +- library/lang/Option.scala | 2 +- scalacleon | 16 +++ scalaleon | 11 ++ 6 files changed, 30 insertions(+), 252 deletions(-) delete mode 100644 Game.scala delete mode 100755 PERMISSIONS create mode 100755 scalacleon create mode 100755 scalaleon diff --git a/Game.scala b/Game.scala deleted file mode 100644 index 391594f76..000000000 --- a/Game.scala +++ /dev/null @@ -1,233 +0,0 @@ -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 - } -} diff --git a/PERMISSIONS b/PERMISSIONS deleted file mode 100755 index b7955144e..000000000 --- a/PERMISSIONS +++ /dev/null @@ -1,16 +0,0 @@ -#!/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 diff --git a/library/collection/List.scala b/library/collection/List.scala index fcd9af4cc..baf9622fe 100644 --- a/library/collection/List.scala +++ b/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 } diff --git a/library/lang/Option.scala b/library/lang/Option.scala index 0d77ef74e..75e018a39 100644 --- a/library/lang/Option.scala +++ b/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 } } diff --git a/scalacleon b/scalacleon new file mode 100755 index 000000000..98fbc7882 --- /dev/null +++ b/scalacleon @@ -0,0 +1,16 @@ +#!/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} diff --git a/scalaleon b/scalaleon new file mode 100755 index 000000000..fbcf6f800 --- /dev/null +++ b/scalaleon @@ -0,0 +1,11 @@ +#!/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 -- GitLab