From 5529ef105672f509ab34f03463d7fd7301375218 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 24 Jul 2014 16:29:39 -0700
Subject: [PATCH] feat(library/standard): add function 'helper' module

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 library/standard/function.lean | 55 ++++++++++++++++++++++++++++++++++
 tests/lean/run/fun.lean        | 23 ++++++++++++++
 2 files changed, 78 insertions(+)
 create mode 100644 library/standard/function.lean
 create mode 100644 tests/lean/run/fun.lean

diff --git a/library/standard/function.lean b/library/standard/function.lean
new file mode 100644
index 000000000..3f93aeb8f
--- /dev/null
+++ b/library/standard/function.lean
@@ -0,0 +1,55 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
+namespace function
+
+section
+  parameters {A : Type} {B : Type} {C : Type} {D : Type} {E : Type}
+
+  abbreviation compose (f : B → C) (g : A → B) : A → C
+  := λx, f (g x)
+
+  abbreviation id (a : A) : A
+  := a
+
+  abbreviation const (a : A) : B → A
+  := λx, a
+
+  abbreviation on_fun (f : B → B → C) (g : A → B) : A → A → C
+  := λx y, f (g x) (g y)
+
+  abbreviation combine (f : A → B → C) (op : C → D → E) (g : A → B → D) : A → B → E
+  := λx y, op (f x y) (g x y)
+end
+
+abbreviation dcompose {A : Type} {B : A → Type} {C : Π {x : A}, B x → Type} (f : Π {x : A} (y : B x), C y) (g : Πx, B x) : Πx, C (g x)
+:= λx, f (g x)
+
+abbreviation flip {A : Type} {B : Type} {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y
+:= λy x, f x y
+
+abbreviation app {A : Type} {B : A → Type} (f : Πx, B x) (x : A) : B x
+:= f x
+
+-- Yet another trick to anotate an expression with a type
+abbreviation is_typeof (A : Type) (a : A) : A
+:= a
+
+precedence `∘`:60
+precedence `∘'`:60
+precedence `on`:1
+precedence `$`:1
+precedence `-[`:1
+precedence `]-`:1
+precedence `⟨`:1
+
+infixr  ∘                  := compose
+infixr  ∘'                 := dcompose
+infixl  on                 := on_fun
+notation `typeof` t `:` T  := is_typeof T t
+infixr  $                  := app
+notation f `-[` op `]-` g  := combine f op g
+-- Trick for using any binary function as infix operator
+notation a `⟨` f `⟩` b     :=  f a b
+
+end
diff --git a/tests/lean/run/fun.lean b/tests/lean/run/fun.lean
new file mode 100644
index 000000000..b5e7b8db9
--- /dev/null
+++ b/tests/lean/run/fun.lean
@@ -0,0 +1,23 @@
+import function logic num bool
+using function num bool
+
+
+variable f : num → bool
+variable g : num → num
+
+check f ∘ g ∘ g
+
+check typeof id : num → num
+check num → num ⟨is_typeof⟩ id
+
+variable h : num → bool → num
+
+check flip h
+check flip h '0 zero
+
+check typeof flip h '0 zero : num
+
+variable f1 : num → num → bool
+variable f2 : bool → num
+
+check (f1 on f2) '0 '1