refactor(library/arith): do not load specialfn by default

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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})

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);
 }
 }

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;

src/library/arith/special_fn.cpp

@@ -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);
-}
-}

src/library/arith/special_fn.h

@@ -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);
-}

tests/lean/arith4.lean

@@ -1,3 +1,4 @@
+Import specialfn.
 Variable x : Real
 Eval sin(x)
 Eval cos(x)

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))

tests/lean/arith5.lean

@@ -1,3 +1,4 @@
+Import specialfn.
 Variable x : Real
 Eval sinh(x)
 Eval cosh(x)

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))

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)

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

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'

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'