Skip to content
Snippets Groups Projects
Commit 4da32aa4 authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

Move State examples out of library

parent 6596b511
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
library/monads/state/State.scala
+ 0
− 207
View file @ 4da32aa4
......@@ -217,210 +217,3 @@ object MonadStateLaws {
}
@library
object ExampleCounter {
import State._
def counter(init: BigInt) = {
@inline
@library
def tick = modify[BigInt](_ + 1)
init >:: (for {
_ <- tick
_ <- tick
_ <- tick
r <- get
} yield r)
} ensuring( _ == init + 3 )
}
@library
object ExampleTicTacToe {
import State._
abstract class Square
case object UL extends Square
case object U extends Square
case object UR extends Square
case object L extends Square
case object C extends Square
case object R extends Square
case object DL extends Square
case object D extends Square
case object DR extends Square
@inline
val winningSets: List[Set[Square]] = List(
Set(UL, U, UR),
Set( L, C, R),
Set(DL, D, DR),
Set(UL, L, DL),
Set( U, C, D),
Set(UR, R, DR),
Set(UR, C, DL),
Set(UL, C, DR)
)
@inline
def wins(sqs: Set[Square]) = winningSets exists { _ subsetOf sqs}
case class Board(xs: Set[Square], os: Set[Square])
case class TState(b: Board, xHasMove: Boolean) // true = X, false = O
@inline
val init = TState(Board(Set.empty[Square], Set.empty[Square]), true)
@inline
def legalMove(b: Board, sq: Square) = !(b.xs ++ b.os).contains(sq)
@inline
def move(sq: Square): State[TState, Unit] = {
modify[TState] { case TState(board, xHasMove) =>
TState(
if (xHasMove)
Board(board.xs ++ Set(sq), board.os)
else
Board(board.xs, board.os ++ Set(sq)),
if (legalMove(board, sq))
!xHasMove
else
xHasMove
)
}
}
@inline
def play(moves: List[Square]): Option[Boolean] = {
val b = foldLeftM_ (move, moves).exec(init).b
if (wins(b.xs)) Some(true)
else if (wins(b.os)) Some(false)
else None[Boolean]()
}
//def ex = {
// play(List(UL, UR, C, D, DR)) == Some(true)
//}.holds
//def gameEnds(moves: List[Square], oneMore: Square) = {
// val res1 = play(moves)
// val res2 = play(moves :+ oneMore)
// res1.isDefined ==> (res1 == res2)
//}.holds
}
@library
object ExampleFreshen {
import State._
import leon.lang.string._
case class Id(name: String, id: BigInt)
abstract class Expr
case class EVar(id: Id) extends Expr
case class EAbs(v: Id, body: Expr) extends Expr
case class EApp(f: Expr, arg: Expr) extends Expr
case class EState(counters: Map[String, BigInt])
def addVar(name: String): State[EState, Id] = for {
s <- get[EState]
newId = if (s.counters.contains(name)) s.counters(name) + 1 else BigInt(0)
_ <- put( EState(s.counters + (name -> newId) ) )
} yield Id(name, newId)
def freshen(e: Expr): State[EState, Expr] = e match {
case EVar(Id(name, id)) =>
for {
s <- get
} yield {
val newId = if (s.counters.contains(name)) s.counters(name) else id
EVar(Id(name, newId))
}
case EAbs(v, body) =>
for {
v2 <- addVar(v.name)
body2 <- freshen(body)
} yield EAbs(v2, body2)
case EApp(f, arg) =>
for {
// We need to freshen both f and arg with the initial state,
// so we save it here
init <- get
f2 <- freshen(f)
_ <- put(init)
arg2 <- freshen(arg)
} yield EApp(f2, arg2)
}
val empty = EState(Map[String, BigInt]())
def freshenNames(e: Expr): Expr = empty >:: freshen(e)
}
@library
object ExampleStackEval {
import State._
abstract class Expr
case class Plus(e1: Expr, e2: Expr) extends Expr
case class Minus(e1: Expr, e2: Expr) extends Expr
case class UMinus(e: Expr) extends Expr
case class Lit(i: BigInt) extends Expr
def push(i: BigInt) = State[List[BigInt], Unit]( s => ( (), i :: s) )
def pop: State[List[BigInt], BigInt] = for {
l <- get
_ <- put(l.tailOption.getOrElse(Nil[BigInt]()))
} yield l.headOption.getOrElse(0)
def evalM(e: Expr): State[List[BigInt], Unit] = e match {
case Plus(e1, e2) =>
for {
_ <- evalM(e1)
_ <- evalM(e2)
i2 <- pop
i1 <- pop
_ <- push(i1 + i2)
} yield(())
case Minus(e1, e2) =>
for {
_ <- evalM(e1)
_ <- evalM(e2)
i2 <- pop
i1 <- pop
_ <- push(i1 - i2)
} yield(())
case UMinus(e) =>
evalM(e) >> pop >>= (i => push(-i))
case Lit(i) =>
push(i)
}
def eval(e: Expr): BigInt = e match {
case Plus(e1, e2) =>
eval(e1) + eval(e2)
case Minus(e1, e2) =>
eval(e1) - eval(e2)
case UMinus(e) =>
-eval(e)
case Lit(i) =>
i
}
def empty = List[BigInt]()
//def evalVsEval(e: Expr) = {
// evalM(e).exec(empty).head == eval(e)
//}.holds
}
testcases/verification/monads/Counter.scala 0 → 100644
+ 22
− 0
View file @ 4da32aa4
/* Copyright 2009-2015 EPFL, Lausanne */
import leon.monads.state._
object Counter {
import State._
def counter(init: BigInt) = {
@inline
def tick = modify[BigInt](_ + 1)
init >:: (for {
_ <- tick
_ <- tick
_ <- tick
r <- get
} yield r)
} ensuring( _ == init + 3 )
}
\ No newline at end of file
testcases/verification/monads/Freshen.scala 0 → 100644
+ 53
− 0
View file @ 4da32aa4
/* Copyright 2009-2015 EPFL, Lausanne */
import leon.monads.state._
object Freshen {
import State._
import leon.lang.string._
case class Id(name: String, id: BigInt)
abstract class Expr
case class EVar(id: Id) extends Expr
case class EAbs(v: Id, body: Expr) extends Expr
case class EApp(f: Expr, arg: Expr) extends Expr
case class EState(counters: Map[String, BigInt])
def addVar(name: String): State[EState, Id] = for {
s <- get[EState]
newId = if (s.counters.contains(name)) s.counters(name) + 1 else BigInt(0)
_ <- put( EState(s.counters + (name -> newId) ) )
} yield Id(name, newId)
def freshen(e: Expr): State[EState, Expr] = e match {
case EVar(Id(name, id)) =>
for {
s <- get
} yield {
val newId = if (s.counters.contains(name)) s.counters(name) else id
EVar(Id(name, newId))
}
case EAbs(v, body) =>
for {
v2 <- addVar(v.name)
body2 <- freshen(body)
} yield EAbs(v2, body2)
case EApp(f, arg) =>
for {
// We need to freshen both f and arg with the initial state,
// so we save it here
init <- get
f2 <- freshen(f)
_ <- put(init)
arg2 <- freshen(arg)
} yield EApp(f2, arg2)
}
val empty = EState(Map[String, BigInt]())
def freshenNames(e: Expr): Expr = empty >:: freshen(e)
}
\ No newline at end of file
testcases/verification/monads/StackEvaluator.scala 0 → 100644
+ 62
− 0
View file @ 4da32aa4
/* Copyright 2009-2015 EPFL, Lausanne */
import leon.monads.state._
object StackEvaluator {
import State._
abstract class Expr
case class Plus(e1: Expr, e2: Expr) extends Expr
case class Minus(e1: Expr, e2: Expr) extends Expr
case class UMinus(e: Expr) extends Expr
case class Lit(i: BigInt) extends Expr
def push(i: BigInt) = State[List[BigInt], Unit]( s => ( (), i :: s) )
def pop: State[List[BigInt], BigInt] = for {
l <- get
_ <- put(l.tailOption.getOrElse(Nil[BigInt]()))
} yield l.headOption.getOrElse(0)
def evalM(e: Expr): State[List[BigInt], Unit] = e match {
case Plus(e1, e2) =>
for {
_ <- evalM(e1)
_ <- evalM(e2)
i2 <- pop
i1 <- pop
_ <- push(i1 + i2)
} yield(())
case Minus(e1, e2) =>
for {
_ <- evalM(e1)
_ <- evalM(e2)
i2 <- pop
i1 <- pop
_ <- push(i1 - i2)
} yield(())
case UMinus(e) =>
evalM(e) >> pop >>= (i => push(-i))
case Lit(i) =>
push(i)
}
def eval(e: Expr): BigInt = e match {
case Plus(e1, e2) =>
eval(e1) + eval(e2)
case Minus(e1, e2) =>
eval(e1) - eval(e2)
case UMinus(e) =>
-eval(e)
case Lit(i) =>
i
}
def empty = List[BigInt]()
//def evalVsEval(e: Expr) = {
// evalM(e).exec(empty).head == eval(e)
//}.holds
}
testcases/verification/monads/TicTacToe.scala 0 → 100644
+ 77
− 0
View file @ 4da32aa4
/* Copyright 2009-2015 EPFL, Lausanne */
import leon.monads.state._
object TicTacToe {
import State._
abstract class Square
case object UL extends Square
case object U extends Square
case object UR extends Square
case object L extends Square
case object C extends Square
case object R extends Square
case object DL extends Square
case object D extends Square
case object DR extends Square
@inline
val winningSets: List[Set[Square]] = List(
Set(UL, U, UR),
Set( L, C, R),
Set(DL, D, DR),
Set(UL, L, DL),
Set( U, C, D),
Set(UR, R, DR),
Set(UR, C, DL),
Set(UL, C, DR)
)
@inline
def wins(sqs: Set[Square]) = winningSets exists { _ subsetOf sqs}
case class Board(xs: Set[Square], os: Set[Square])
case class TState(b: Board, xHasMove: Boolean) // true = X, false = O
@inline
val init = TState(Board(Set.empty[Square], Set.empty[Square]), true)
@inline
def legalMove(b: Board, sq: Square) = !(b.xs ++ b.os).contains(sq)
@inline
def move(sq: Square): State[TState, Unit] = {
modify[TState] { case TState(board, xHasMove) =>
TState(
if (xHasMove)
Board(board.xs ++ Set(sq), board.os)
else
Board(board.xs, board.os ++ Set(sq)),
if (legalMove(board, sq))
!xHasMove
else
xHasMove
)
}
}
@inline
def play(moves: List[Square]): Option[Boolean] = {
val b = foldLeftM_ (move, moves).exec(init).b
if (wins(b.xs)) Some(true)
else if (wins(b.os)) Some(false)
else None[Boolean]()
}
//def ex = {
// play(List(UL, UR, C, D, DR)) == Some(true)
//}.holds
//def gameEnds(moves: List[Square], oneMore: Square) = {
// val res1 = play(moves)
// val res2 = play(moves :+ oneMore)
// res1.isDefined ==> (res1 == res2)
//}.holds
}
\ No newline at end of file
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment