Skip to content
Snippets Groups Projects
Commit 182106ab authored by Emmanouil (Manos) Koukoutos's avatar Emmanouil (Manos) Koukoutos Committed by Etienne Kneuss
Browse files

Two more benchmarks

parent 914e24f9
Branches
Tags
No related merge requests found
import leon.lang.synthesis._
object Naturals {
abstract class Nat {
def intValue : Int = { this match {
case Zero => 0
case Succ(n) => n.intValue + 1
}} ensuring { _ >= 0 }
def +(that : Nat) : Nat = { this match {
case Zero => that
case Succ(n) => n + Succ(that)
}} ensuring { _.intValue == this.intValue + that.intValue }
def <=(that : Nat) : Boolean = { (this, that) match {
case (Zero, _) => true
case (_, Zero) => false
case (Succ(n1), Succ(n2)) => n1 <= n2
}} ensuring { _ == this.intValue <= that.intValue }
def >(that : Nat) = !(this <= that)
def -(that : Nat) : Nat = {
require(that <= this)
(this, that) match {
case (_, Zero) => this
case (Succ(n1), Succ(n2)) => n1 - n2
}
} ensuring { _.intValue == this.intValue - that.intValue }
def * (that: Nat) : Nat = { this match {
case Zero => Zero
case Succ(n) => that + n * that
}} ensuring { _.intValue == this.intValue * that.intValue }
/*
def /(that : Nat) : Nat = {
require(that > Zero)
if (that <= this) (this - that)/ that + one
else Zero
} ensuring { _.intValue == this.intValue / that.intValue }
def %(that : Nat) : Nat = {
require(that > Zero)
this - (this / that) * that
} ensuring { _.intValue == this.intValue % that.intValue }
// Convension : least s. digit first
def isDecimalRepr(l : List[Nat]) : Boolean = l match {
case Nil() => false
case Cons(h, t) => h <= ten && isDecimalRepr(t)
}
def decimalToNat(l : List[Nat]) : Nat = {
require(isDecimalRepr(l))
l match {
case Cons(h, Nil()) => h
case Cons(h, t) => 10 * decimalToNat(t) + h
}
}
*/
}
case object Zero extends Nat
case class Succ(n : Nat) extends Nat
def ten = {
val two = Succ(Succ(Zero))
val five = Succ(two + two)
two * five
}
def fortyTwo = {
val one = Succ(Zero)
val two = one + one
val three = two + one
val seven = (two * three) + one
two * three * seven
} ensuring { _.intValue == 42 }
}
import leon._
import leon.lang.string._
import leon.collection._
object Parser {
abstract class Token
case object LParen extends Token
case object RParen extends Token
case class Id(id : Int) extends Token
abstract class Tree
case class App(args : List[Tree]) extends Tree
case class Leaf(id : Int) extends Tree
def parse(in : List[Token]) : (Option[Tree], List[Token]) = { in match {
case Cons(Id(s), tl) =>
(Some[Tree](Leaf(s)),tl)
case Cons(LParen, tl) => parseMany(tl) match {
case (Some(trees:Cons[Tree]), Cons(RParen,rest)) =>
(Some[Tree](App(trees)), rest)
case (_, rest) => (None[Tree](), rest)
}
case _ => (None[Tree](), in)
}} ensuring { _ match {
case ( Some(tree), rest@Cons(h,_)) =>
print(tree, rest) == in
// case ( None(), Cons(h,_)) => !h.isInstanceOf[Id]
// case ( None(), Nil) =>
case _ => true
}}
def parseMany(in : List[Token]) : (Option[List[Tree]], List[Token]) = { parse(in) match {
case (None(), rest) if rest == in => (Some[List[Tree]](Nil()), in)
case (None(), rest) => (None[List[Tree]](), rest)
case (Some(tree), rest) => parseMany(rest) match {
case ( None(), rest2) => (None[List[Tree]](), rest2)
case ( Some(trees), rest2) =>
( Some[List[Tree]](tree::trees), rest2 )
}
}} ensuring { _ match {
case ( Some(t), rest@Cons(h, _) ) =>
h == RParen && printL(t, rest) == in
case ( None(), Cons(h, _)) =>
h == RParen
case _ => true
}}
def printL(args : List[Tree], rest : List[Token]) : List[Token] = args match {
case Nil() => rest
case Cons(h,t) => print(h, printL(t, rest))
}
def print(t : Tree, rest : List[Token]) : List[Token] = t match {
case Leaf(s) => Id(s) :: rest
case App(args) => LParen :: printL(args, RParen :: rest)
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment