From 3cee85d75ec5d8dcebde4a5f6884c8f43ed21b0b Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Fri, 11 Apr 2014 20:21:15 +0200
Subject: [PATCH] Actually add the files
---
library/lang/synthesis/Oracle.scala | 30 ++++++++++++++++++++++++++++
library/lang/synthesis/package.scala | 30 ++++++++++++++++++++++++++++
2 files changed, 60 insertions(+)
create mode 100644 library/lang/synthesis/Oracle.scala
create mode 100644 library/lang/synthesis/package.scala
diff --git a/library/lang/synthesis/Oracle.scala b/library/lang/synthesis/Oracle.scala
new file mode 100644
index 000000000..cc0af6415
--- /dev/null
+++ b/library/lang/synthesis/Oracle.scala
@@ -0,0 +1,30 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon.lang.synthesis
+
+import leon.annotation._
+import leon.lang._
+
+import scala.annotation._
+
+@implicitNotFound("No Oracle available for this source of non-determinism, please provide an implicit arg <: Oracle[T]")
+@verified
+abstract class Oracle[T] {
+ def head: T = this match {
+ case Node(_, h, _) => h
+ case Leaf(h) => h
+ }
+
+ def left: Oracle[T] = this match {
+ case Node(l, _, _) => l
+ case Leaf(_) => this
+ }
+
+ def right: Oracle[T] = this match {
+ case Node(_, _, r) => r
+ case Leaf(_) => this
+ }
+}
+
+case class Node[T](l: Oracle[T], v: T, r: Oracle[T]) extends Oracle[T];
+case class Leaf[T](v: T) extends Oracle[T];
diff --git a/library/lang/synthesis/package.scala b/library/lang/synthesis/package.scala
new file mode 100644
index 000000000..abf314dc8
--- /dev/null
+++ b/library/lang/synthesis/package.scala
@@ -0,0 +1,30 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon.lang
+
+import leon.annotation._
+
+package object synthesis {
+ @ignore
+ private def noChoose = throw new RuntimeException("Implementation not supported")
+
+ @ignore
+ def choose[A](predicate: A => Boolean): A = noChoose
+ @ignore
+ def choose[A, B](predicate: (A, B) => Boolean): (A, B) = noChoose
+ @ignore
+ def choose[A, B, C](predicate: (A, B, C) => Boolean): (A, B, C) = noChoose
+ @ignore
+ def choose[A, B, C, D](predicate: (A, B, C, D) => Boolean): (A, B, C, D) = noChoose
+ @ignore
+ def choose[A, B, C, D, E](predicate: (A, B, C, D, E) => Boolean): (A, B, C, D, E) = noChoose
+
+ @library
+ def ???[T](implicit o: Oracle[T]): T = o.head
+
+ @library
+ def ?[T](e1: T)(implicit o: Oracle[Boolean], o2: Oracle[T]): T = if(???[Boolean]) e1 else ???[T]
+
+ @ignore
+ def ?[T](e1: T, es: T*)(implicit o: Oracle[Boolean]): T = noChoose
+}
--
GitLab