From 4401b390fef4003941a6225b9bae45093431efad Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 30 Dec 2013 11:25:43 -0800
Subject: [PATCH] refactor(library/arith): do not load specialfn by default

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/builtin/cast.olean                   | Bin 941 -> 924 bytes
 src/library/arith/CMakeLists.txt         |   2 +-
 src/library/arith/arith.cpp              |   1 -
 src/library/arith/arith.h                |   1 -
 src/library/arith/special_fn.cpp         |  36 -------------
 src/library/arith/special_fn.h           |  63 -----------------------
 tests/lean/arith4.lean                   |   1 +
 tests/lean/arith4.lean.expected.out      |   1 +
 tests/lean/arith5.lean                   |   1 +
 tests/lean/arith5.lean.expected.out      |   1 +
 tests/lean/compact_def.lean              |   1 +
 tests/lean/compact_def.lean.expected.out |   1 +
 tests/lean/elab4.lean.expected.out       |   1 -
 tests/lean/elab5.lean.expected.out       |   1 -
 14 files changed, 7 insertions(+), 104 deletions(-)
 delete mode 100644 src/library/arith/special_fn.cpp
 delete mode 100644 src/library/arith/special_fn.h

diff --git a/src/builtin/cast.olean b/src/builtin/cast.olean
index 031ab9ddf921f30e7eff4a461b68ac010d5ebf69..59c5f21fcda532bfd1c5e813bfdfd7a42b0b3bce 100644
GIT binary patch
delta 10
RcmZ3>K8JmR<Hn$9W&jm51Bw6u

delta 27
icmbQkzLtH0qkv~_L4HvQLvcZBa%N&qTHZ#77-j&6U<tVZ

diff --git a/src/library/arith/CMakeLists.txt b/src/library/arith/CMakeLists.txt
index 8dc8ca686..5bb7ae295 100644
--- a/src/library/arith/CMakeLists.txt
+++ b/src/library/arith/CMakeLists.txt
@@ -1,2 +1,2 @@
-add_library(arithlib nat.cpp int.cpp real.cpp special_fn.cpp arith.cpp)
+add_library(arithlib nat.cpp int.cpp real.cpp arith.cpp)
 target_link_libraries(arithlib ${LEAN_LIBS})
diff --git a/src/library/arith/arith.cpp b/src/library/arith/arith.cpp
index 67afab7a9..cb4019f57 100644
--- a/src/library/arith/arith.cpp
+++ b/src/library/arith/arith.cpp
@@ -11,6 +11,5 @@ void import_arith(environment const & env) {
     import_nat(env);
     import_int(env);
     import_real(env);
-    import_special_fn(env);
 }
 }
diff --git a/src/library/arith/arith.h b/src/library/arith/arith.h
index 2ea15f8a4..819f29126 100644
--- a/src/library/arith/arith.h
+++ b/src/library/arith/arith.h
@@ -8,7 +8,6 @@ Author: Leonardo de Moura
 #include "library/arith/nat.h"
 #include "library/arith/int.h"
 #include "library/arith/real.h"
-#include "library/arith/special_fn.h"
 
 namespace lean {
 class environment;
diff --git a/src/library/arith/special_fn.cpp b/src/library/arith/special_fn.cpp
deleted file mode 100644
index 758cff59b..000000000
--- a/src/library/arith/special_fn.cpp
+++ /dev/null
@@ -1,36 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "kernel/environment.h"
-#include "kernel/abstract.h"
-#include "kernel/io_state.h"
-#include "library/arith/special_fn.h"
-#include "library/arith/real.h"
-
-namespace lean {
-MK_CONSTANT(exp_fn, name("exp"));
-MK_CONSTANT(log_fn, name("log"));
-
-MK_CONSTANT(real_pi, name("\u03C0")); // lower case pi
-MK_CONSTANT(sin_fn, name("sin"));
-MK_CONSTANT(cos_fn, name("cos"));
-MK_CONSTANT(tan_fn, name("tan"));
-MK_CONSTANT(cot_fn, name("cot"));
-MK_CONSTANT(sec_fn, name("sec"));
-MK_CONSTANT(csc_fn, name("csc"));
-
-MK_CONSTANT(sinh_fn, name("sinh"));
-MK_CONSTANT(cosh_fn, name("cosh"));
-MK_CONSTANT(tanh_fn, name("tanh"));
-MK_CONSTANT(coth_fn, name("coth"));
-MK_CONSTANT(sech_fn, name("sech"));
-MK_CONSTANT(csch_fn, name("csch"));
-
-void import_special_fn(environment const & env) {
-    io_state ios;
-    env->import("specialfn", ios);
-}
-}
diff --git a/src/library/arith/special_fn.h b/src/library/arith/special_fn.h
deleted file mode 100644
index ed5b8c852..000000000
--- a/src/library/arith/special_fn.h
+++ /dev/null
@@ -1,63 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/expr.h"
-
-namespace lean {
-// Special functions library
-
-expr mk_exp_fn();
-inline expr Exp(expr const & e) { return mk_app(mk_exp_fn(), e); }
-
-expr mk_log_fn();
-inline expr Log(expr const & e) { return mk_app(mk_log_fn(), e); }
-
-expr mk_real_pi();
-
-expr mk_sin_fn();
-inline expr Sin(expr const & e) { return mk_app(mk_sin_fn(), e); }
-
-expr mk_cos_fn();
-inline expr Cos(expr const & e) { return mk_app(mk_cos_fn(), e); }
-
-expr mk_tan_fn();
-inline expr Tan(expr const & e) { return mk_app(mk_tan_fn(), e); }
-
-expr mk_cot_fn();
-inline expr Cot(expr const & e) { return mk_app(mk_cot_fn(), e); }
-
-expr mk_sec_fn();
-inline expr Sec(expr const & e) { return mk_app(mk_sec_fn(), e); }
-
-expr mk_csc_fn();
-inline expr Csc(expr const & e) { return mk_app(mk_csc_fn(), e); }
-
-expr mk_sinh_fn();
-inline expr Sinh(expr const & e) { return mk_app(mk_sinh_fn(), e); }
-
-expr mk_cosh_fn();
-inline expr Cosh(expr const & e) { return mk_app(mk_cosh_fn(), e); }
-
-expr mk_tanh_fn();
-inline expr Tanh(expr const & e) { return mk_app(mk_tanh_fn(), e); }
-
-expr mk_coth_fn();
-inline expr Coth(expr const & e) { return mk_app(mk_coth_fn(), e); }
-
-expr mk_sech_fn();
-inline expr Sech(expr const & e) { return mk_app(mk_sech_fn(), e); }
-
-expr mk_csch_fn();
-inline expr Csch(expr const & e) { return mk_app(mk_csch_fn(), e); }
-
-class environment;
-/**
-    \brief Import the special function library (if it has not been imported already).
-    The (basic) Real Number library is also imported.
-*/
-void import_special_fn(environment const & env);
-}
diff --git a/tests/lean/arith4.lean b/tests/lean/arith4.lean
index 54f6e74e2..e20c7bc3e 100644
--- a/tests/lean/arith4.lean
+++ b/tests/lean/arith4.lean
@@ -1,3 +1,4 @@
+Import specialfn.
 Variable x : Real
 Eval sin(x)
 Eval cos(x)
diff --git a/tests/lean/arith4.lean.expected.out b/tests/lean/arith4.lean.expected.out
index c41757a93..585cdebea 100644
--- a/tests/lean/arith4.lean.expected.out
+++ b/tests/lean/arith4.lean.expected.out
@@ -1,5 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
+  Imported 'specialfn'
   Assumed: x
 sin x
 sin (x + -1 * (π / 2))
diff --git a/tests/lean/arith5.lean b/tests/lean/arith5.lean
index 4d7547436..77ccb0495 100644
--- a/tests/lean/arith5.lean
+++ b/tests/lean/arith5.lean
@@ -1,3 +1,4 @@
+Import specialfn.
 Variable x : Real
 Eval sinh(x)
 Eval cosh(x)
diff --git a/tests/lean/arith5.lean.expected.out b/tests/lean/arith5.lean.expected.out
index 2a4ae59de..e17148688 100644
--- a/tests/lean/arith5.lean.expected.out
+++ b/tests/lean/arith5.lean.expected.out
@@ -1,5 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
+  Imported 'specialfn'
   Assumed: x
 (1 + -1 * exp (-2 * x)) / (2 * exp (-1 * x))
 (1 + exp (-2 * x)) / (2 * exp (-1 * x))
diff --git a/tests/lean/compact_def.lean b/tests/lean/compact_def.lean
index 9d20c5fd2..eb7cf2463 100644
--- a/tests/lean/compact_def.lean
+++ b/tests/lean/compact_def.lean
@@ -1,3 +1,4 @@
+Import specialfn.
 Definition f x y := x + y
 Definition g x y := sin x + y
 Definition h x y := x * sin (x + y)
diff --git a/tests/lean/compact_def.lean.expected.out b/tests/lean/compact_def.lean.expected.out
index c2800a677..de03baca4 100644
--- a/tests/lean/compact_def.lean.expected.out
+++ b/tests/lean/compact_def.lean.expected.out
@@ -1,5 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
+  Imported 'specialfn'
   Defined: f
   Defined: g
   Defined: h
diff --git a/tests/lean/elab4.lean.expected.out b/tests/lean/elab4.lean.expected.out
index 18768da3e..d11dd8818 100644
--- a/tests/lean/elab4.lean.expected.out
+++ b/tests/lean/elab4.lean.expected.out
@@ -9,7 +9,6 @@ Import "basic"
 Import "nat"
 Import "int"
 Import "real"
-Import "specialfn"
 Variable C {A B : Type} (H : @eq Type A B) (a : A) : B
 Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : @eq Type (Π x : A, B x) (Π x : A', B' x)) :
     @eq Type A A'
diff --git a/tests/lean/elab5.lean.expected.out b/tests/lean/elab5.lean.expected.out
index 18768da3e..d11dd8818 100644
--- a/tests/lean/elab5.lean.expected.out
+++ b/tests/lean/elab5.lean.expected.out
@@ -9,7 +9,6 @@ Import "basic"
 Import "nat"
 Import "int"
 Import "real"
-Import "specialfn"
 Variable C {A B : Type} (H : @eq Type A B) (a : A) : B
 Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : @eq Type (Π x : A, B x) (Π x : A', B' x)) :
     @eq Type A A'