From e1535017f01792701d6bce4f7375b41bfb30b068 Mon Sep 17 00:00:00 2001 From: Yann Bolliger Date: Mon, 22 Feb 2021 15:36:22 +0100 Subject: [PATCH 1/3] Use rebased stainless & inox dependencies. --- .stainless-version | 2 +- stainless_backend/src/lib.rs | 10 ++++------ 2 files changed, 5 insertions(+), 7 deletions(-) diff --git a/.stainless-version b/.stainless-version index bc5a6fed..2828eb51 100644 --- a/.stainless-version +++ b/.stainless-version @@ -1 +1 @@ -noxt-0.7.1-21-g381fb00 +noxt-0.7.6-67-g533f5d5 \ No newline at end of file diff --git a/stainless_backend/src/lib.rs b/stainless_backend/src/lib.rs index b20a8b16..d25d7c45 100644 --- a/stainless_backend/src/lib.rs +++ b/stainless_backend/src/lib.rs @@ -56,20 +56,18 @@ impl Backend { .arg("--interactive") .arg("--batched") .arg("--vc-cache=false") + .arg("--type-checker=false") .arg(format!("--timeout={}", config.timeout)) .arg(format!("--print-ids={}", config.print_ids)) .arg(format!("--print-types={}", config.print_types)) - .arg(format!("--strict-arithmetic={}", config.strict_arithmetic)) - // FIXME: Turn the measure inference back on as soon as - // https://github.com/epfl-lara/rust-stainless/issues/68 - // is solved. - .arg("--infer-measures=no") - .arg("--check-measures=false"); + .arg(format!("--strict-arithmetic={}", config.strict_arithmetic)); + if config.debug_trees { cmd .arg("--debug=trees") .arg(format!("--debug-phases={}", config.debug_phases.join(","))); } + if let Ok(extra_flags) = env::var("STAINLESS_FLAGS") { cmd.args(extra_flags.split(' ')); } From 1e98dfd59ab47e4e903138f4775fc0baa81043c3 Mon Sep 17 00:00:00 2001 From: Yann Bolliger Date: Mon, 22 Feb 2021 15:36:32 +0100 Subject: [PATCH 2/3] Adapt tests. --- demo/examples/adts.rs | 18 ++-- demo/examples/type_class.rs | 95 ++++++++------------- stainless_frontend/tests/pass/type_class.rs | 4 +- 3 files changed, 46 insertions(+), 71 deletions(-) diff --git a/demo/examples/adts.rs b/demo/examples/adts.rs index aaa75fe9..5a8e3853 100644 --- a/demo/examples/adts.rs +++ b/demo/examples/adts.rs @@ -1,3 +1,5 @@ +extern crate stainless; + // In rustc's HIR all of the following make_* functions contain somewhat // distinct trees. Here's a succinct overview of the cases I think we'd like to // consider in the short term: @@ -14,13 +16,13 @@ pub struct Foo2(i32, bool); pub struct Foo3 { a: i32, - b: bool + b: bool, } pub enum Bar { Bar1, Bar2(i32, bool), - Bar3 { c: i32, d: bool } + Bar3 { c: i32, d: bool }, } fn make_foo1() -> Foo1 { @@ -51,7 +53,7 @@ fn get_i32_from_bar(bar: Bar) -> i32 { match bar { Bar::Bar1 => 0, Bar::Bar2(c, _) => c, - Bar::Bar3 { c, .. } => c + Bar::Bar3 { c, .. } => c, } } @@ -59,27 +61,27 @@ fn get_bool_from_bar(bar: Bar) -> bool { match bar { Bar::Bar1 => false, Bar::Bar2(_, d) => d, - Bar::Bar3 { d, .. } => d + Bar::Bar3 { d, .. } => d, } } -fn main() -> () { +pub fn main() -> () { match make_foo1() { - Foo1 => () + Foo1 => (), }; let foo2 = make_foo2(); foo2.0; foo2.1; match foo2 { - Foo2(a, b) => (a, b) + Foo2(a, b) => (a, b), }; let foo3 = make_foo3(); foo3.a; foo3.b; match foo3 { - Foo3 { a, b } => (a, b) + Foo3 { a, b } => (a, b), }; get_i32_from_bar(make_bar1()); diff --git a/demo/examples/type_class.rs b/demo/examples/type_class.rs index cfda76b9..7d0d6724 100644 --- a/demo/examples/type_class.rs +++ b/demo/examples/type_class.rs @@ -10,7 +10,6 @@ trait Equals { // - trait => abstract class // - take trait with all type params, add one new at the end // => abstract class Equals[T] - fn equals(&self, x: &Self) -> bool; // type_class_insts: Map( ("Equals", "Self", []) -> "this" ) @@ -36,16 +35,16 @@ trait Equals { } } -impl Equals for List { - /* - - 'impl<..> Z for X' and has type params => case class - - impl => ListEquals[tps] - - trait bounds => trait bounds implemented by evidence params - - the trait with as last type param the 'for X' => extends trait[..., X] - (the last two use the same translation) - => case class ListEquals[T](ev: Equals[T]) extends Equals[List[T]] - */ +/* +- 'impl<..> Z for X' and has type params => case class +- impl => ListEquals[tps] +- trait bounds => trait bounds implemented by evidence params +- the trait with as last type param the 'for X' => extends trait[..., X] +(the last two use the same translation) +=> case class ListEquals[T](ev: Equals[T]) extends Equals[List[T]] +*/ +impl Equals for List { // #[measure(self)] fn equals(&self, other: &List) -> bool { match (self, other) { @@ -54,6 +53,31 @@ impl Equals for List { _ => false, } } + + fn law_reflexive(x: &Self) -> bool { + match x { + List::Cons(x, xs) => T::law_reflexive(x) && Self::law_reflexive(xs), + List::Nil => true, + } + } + + fn law_symmetric(x: &Self, y: &Self) -> bool { + match (x, y) { + (List::Cons(x, xs), List::Cons(y, ys)) => { + T::law_symmetric(x, y) && Self::law_symmetric(xs, ys) + } + _ => true, + } + } + + fn law_transitive(x: &Self, y: &Self, z: &Self) -> bool { + match (x, y, z) { + (List::Cons(x, xs), List::Cons(y, ys), List::Cons(z, zs)) => { + T::law_transitive(x, y, z) && Self::law_transitive(xs, ys, zs) + } + _ => true, + } + } } // case object IntEquals extends Equals[i32] @@ -65,31 +89,12 @@ impl Equals for i32 { } } -trait Ord: Equals { - fn less_than_eq(&self, other: &Self) -> bool; - - fn less_than(&self, other: &Self) -> bool { - self.less_than_eq(other) && self.not_equals(other) - } -} - -impl Ord for i32 { - fn less_than_eq(&self, other: &Self) -> bool { - self <= other - } - - fn less_than(&self, other: &Self) -> bool { - self < other - } -} - pub fn main() { let a = 2; let b = 4; // => IntEquals.equals(a, b) assert!(a.not_equals(&b)); - assert!(a.less_than(&b)); // => ListEquals.equals(list, list)(IntEquals) let list = List::Cons(123, Box::new(List::Cons(456, Box::new(List::Nil)))); @@ -130,36 +135,4 @@ case class ListEquals[A](ev: Equals[A]) extends Equals[List[A]] { case object IntEquals extends Equals[Int] { def equals(x: Int, y: Int): Boolean = x == y } - -// stainless extracts this as follows - - Symbols before PartialFunctions - --------------Functions------------- -@abstract -@method(Equals) -def equals(x: T, y: T): Boolean = [Boolean] - -@law -@method(Equals) -def law_transitive(x: T, y: T, z: T): Boolean = ¬(this.equals(x, y) && this.equals(y, z)) || this.equals(x, z) - -@law -@method(Equals) -def law_symmetric(x: T, y: T): Boolean = this.equals(x, y) == this.equals(y, x) - -@method(IntEquals) -def equals(x: Int, y: Int): Boolean = x == y - -@law -@method(Equals) -def law_reflexive(x: T): Boolean = this.equals(x, x) - --------------Classes------------- -@caseObject -case class IntEquals extends Equals[Int] - -@abstract -abstract class Equals[T] - */ diff --git a/stainless_frontend/tests/pass/type_class.rs b/stainless_frontend/tests/pass/type_class.rs index bc68964b..7d0d6724 100644 --- a/stainless_frontend/tests/pass/type_class.rs +++ b/stainless_frontend/tests/pass/type_class.rs @@ -97,8 +97,8 @@ pub fn main() { assert!(a.not_equals(&b)); // => ListEquals.equals(list, list)(IntEquals) - // let list = List::Cons(123, Box::new(List::Cons(456, Box::new(List::Nil)))); - // assert!(list.equals(&list)); + let list = List::Cons(123, Box::new(List::Cons(456, Box::new(List::Nil)))); + assert!(list.equals(&list)); } /* From b006d6a07dfeb67aa339a3acc2cbac210f8aed6c Mon Sep 17 00:00:00 2001 From: Yann Bolliger Date: Mon, 22 Feb 2021 16:10:49 +0100 Subject: [PATCH 3/3] Forget about the measure in list equals test. --- .stainless-version | 2 +- demo/examples/type_class.rs | 4 ++-- stainless_frontend/tests/pass/type_class.rs | 4 ++-- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/.stainless-version b/.stainless-version index 2828eb51..8b771430 100644 --- a/.stainless-version +++ b/.stainless-version @@ -1 +1 @@ -noxt-0.7.6-67-g533f5d5 \ No newline at end of file +noxt-0.7.6-67-g533f5d5 diff --git a/demo/examples/type_class.rs b/demo/examples/type_class.rs index 7d0d6724..915b35b2 100644 --- a/demo/examples/type_class.rs +++ b/demo/examples/type_class.rs @@ -45,7 +45,6 @@ trait Equals { */ impl Equals for List { - // #[measure(self)] fn equals(&self, other: &List) -> bool { match (self, other) { (List::Nil, List::Nil) => true, @@ -123,13 +122,14 @@ abstract class Equals[T] { case class ListEquals[A](ev: Equals[A]) extends Equals[List[A]] { def equals(xs: List[A], ys: List[A]): Boolean = { - decreases(xs.size) (xs, ys) match { case (Cons(x, xs), Cons(y, ys)) => ev.equals(x, y) && equals(xs, ys) case (Nil(), Nil()) => true case _ => false } } + + // will also require manual proofs of the laws } case object IntEquals extends Equals[Int] { diff --git a/stainless_frontend/tests/pass/type_class.rs b/stainless_frontend/tests/pass/type_class.rs index 7d0d6724..915b35b2 100644 --- a/stainless_frontend/tests/pass/type_class.rs +++ b/stainless_frontend/tests/pass/type_class.rs @@ -45,7 +45,6 @@ trait Equals { */ impl Equals for List { - // #[measure(self)] fn equals(&self, other: &List) -> bool { match (self, other) { (List::Nil, List::Nil) => true, @@ -123,13 +122,14 @@ abstract class Equals[T] { case class ListEquals[A](ev: Equals[A]) extends Equals[List[A]] { def equals(xs: List[A], ys: List[A]): Boolean = { - decreases(xs.size) (xs, ys) match { case (Cons(x, xs), Cons(y, ys)) => ev.equals(x, y) && equals(xs, ys) case (Nil(), Nil()) => true case _ => false } } + + // will also require manual proofs of the laws } case object IntEquals extends Equals[Int] {