From 2e3ffea2ecfd1a41aa96793089c6e430a13b957e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 15 May 2014 16:48:47 -0700 Subject: [PATCH] feat(library): add new coercion API Signed-off-by: Leonardo de Moura --- src/library/coercion.h | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 src/library/coercion.h diff --git a/src/library/coercion.h b/src/library/coercion.h new file mode 100644 index 000000000..1f49fd8c6 --- /dev/null +++ b/src/library/coercion.h @@ -0,0 +1,38 @@ +/* +Copyright (c) 2014 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/environment.h" +namespace lean { +/** + \brief Add an new coercion in the given environment. + + There are three kinds of coercions supported + 1- From type C to type D + type of f must have the form: + {l1 ... lk} Pi (x1 : A1) ... (xn : An) (y: C.{l1 ... lk} x1 ... xn), D.{L1 ... Lr} t1 ... tm + - C and D are constants. + - l1 ... lk are universe level parameters + - L1 ... Lr are universe level expressions + - t1 ... tm are level expressions + + 2- From type to sort + type of f must have the form: + {l1 ... lk} Pi (x1 : A1) ... (xn : An) (y: C.{l1 ... lk} x1 ... xn) (x : A), B + + 3- From type to function type + type of f must have the form: + {l1 ... lk} Pi (x1 : A1) ... (xn : An) (y: C.{l1 ... lk} x1 ... xn), Type.{L} + + \pre \c f is a constant defined in \c env. +*/ +environment add_coercion(environment const & env, expr const & f); +bool is_coercion(environment const & env, expr const & f); +list get_coercions(environment const & env, expr const & from, expr const & from_type); +optional get_coercion(environment const & env, expr const & from, expr const & from_type, expr const & to_type); +optional get_coercion_to_sort(environment const & env, expr const & from, expr const & from_type); +optional get_coercion_to_fun(environment const & env, expr const & from, expr const & from_type); +}