From e1e3e6b2d63b7ed7e32bf62d806a39d5741309b0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 3 Aug 2013 11:27:03 -0700 Subject: [PATCH] Add instantiate tests Signed-off-by: Leonardo de Moura --- src/tests/kernel/replace.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/tests/kernel/replace.cpp b/src/tests/kernel/replace.cpp index 2e76deb38..7e9d70074 100644 --- a/src/tests/kernel/replace.cpp +++ b/src/tests/kernel/replace.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include "expr.h" #include "abstract.h" +#include "instantiate.h" #include "deep_copy.h" #include "name.h" #include "test.h" @@ -27,9 +28,20 @@ static void tst1() { } } +static void tst2() { + expr r = lambda("x", type(level()), app(var(0), var(1), var(2))); + std::cout << instantiate(constant("a"), r) << std::endl; + lean_assert(instantiate(constant("a"), r) == lambda("x", type(level()), app(var(0), constant("a"), var(1)))); + lean_assert(instantiate(constant("b"), instantiate(constant("a"), r)) == + lambda("x", type(level()), app(var(0), constant("a"), constant("b")))); + std::cout << instantiate(constant("a"), abst_body(r)) << std::endl; + lean_assert(instantiate(constant("a"), abst_body(r)) == app(constant("a"), var(0), var(1))); +} + int main() { continue_on_violation(true); tst1(); + tst2(); std::cout << "done" << "\n"; return has_violations() ? 1 : 0; }