From 4da32aa444de9d97a9538b900840984137d96b1f Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 25 Sep 2015 12:14:36 +0200
Subject: [PATCH] Move State examples out of library
---
library/monads/state/State.scala | 207 ------------------
testcases/verification/monads/Counter.scala | 22 ++
testcases/verification/monads/Freshen.scala | 53 +++++
.../verification/monads/StackEvaluator.scala | 62 ++++++
testcases/verification/monads/TicTacToe.scala | 77 +++++++
5 files changed, 214 insertions(+), 207 deletions(-)
create mode 100644 testcases/verification/monads/Counter.scala
create mode 100644 testcases/verification/monads/Freshen.scala
create mode 100644 testcases/verification/monads/StackEvaluator.scala
create mode 100644 testcases/verification/monads/TicTacToe.scala
diff --git a/library/monads/state/State.scala b/library/monads/state/State.scala
index 8e268c79e..d16048688 100644
--- a/library/monads/state/State.scala
+++ b/library/monads/state/State.scala
@@ -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
-
-}
diff --git a/testcases/verification/monads/Counter.scala b/testcases/verification/monads/Counter.scala
new file mode 100644
index 000000000..26991d2be
--- /dev/null
+++ b/testcases/verification/monads/Counter.scala
@@ -0,0 +1,22 @@
+/* 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
diff --git a/testcases/verification/monads/Freshen.scala b/testcases/verification/monads/Freshen.scala
new file mode 100644
index 000000000..06c7c4bd2
--- /dev/null
+++ b/testcases/verification/monads/Freshen.scala
@@ -0,0 +1,53 @@
+/* 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
diff --git a/testcases/verification/monads/StackEvaluator.scala b/testcases/verification/monads/StackEvaluator.scala
new file mode 100644
index 000000000..cbe565429
--- /dev/null
+++ b/testcases/verification/monads/StackEvaluator.scala
@@ -0,0 +1,62 @@
+/* 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
+
+}
diff --git a/testcases/verification/monads/TicTacToe.scala b/testcases/verification/monads/TicTacToe.scala
new file mode 100644
index 000000000..8c52fe89f
--- /dev/null
+++ b/testcases/verification/monads/TicTacToe.scala
@@ -0,0 +1,77 @@
+/* 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
--
GitLab