2013-08-10 01:00:05 +00:00
/*
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 <atomic>
2013-09-01 23:59:15 +00:00
# include <unordered_set>
2013-09-13 10:35:29 +00:00
# include <vector>
# include <utility>
# include <functional>
2013-09-13 03:04:10 +00:00
# include "util/map.h"
# include "util/sstream.h"
# include "util/exception.h"
# include "kernel/environment.h"
# include "library/expr_pair.h"
2013-11-21 23:51:29 +00:00
# include "library/io_state.h"
2013-09-13 16:06:46 +00:00
# include "library/all/all.h"
2013-09-13 03:09:35 +00:00
# include "frontends/lean/operator_info.h"
# include "frontends/lean/coercion.h"
# include "frontends/lean/frontend.h"
# include "frontends/lean/notation.h"
# include "frontends/lean/pp.h"
2013-08-10 01:00:05 +00:00
namespace lean {
2013-08-27 03:21:05 +00:00
static std : : vector < bool > g_empty_vector ;
2013-11-07 18:00:12 +00:00
/**
\ brief Environment extension object for the Lean default frontend .
*/
struct lean_extension : public environment : : extension {
2013-08-27 03:21:05 +00:00
typedef std : : pair < std : : vector < bool > , name > implicit_info ;
2013-08-14 23:35:04 +00:00
// Remark: only named objects are stored in the dictionary.
typedef std : : unordered_map < name , operator_info , name_hash , name_eq > operator_table ;
2013-08-26 16:04:17 +00:00
typedef std : : unordered_map < name , implicit_info , name_hash , name_eq > implicit_table ;
2013-09-03 17:09:19 +00:00
typedef std : : unordered_map < expr , list < operator_info > , expr_hash , std : : equal_to < expr > > expr_to_operators ;
2013-09-01 23:59:15 +00:00
typedef std : : unordered_map < expr_pair , expr , expr_pair_hash , expr_pair_eq > coercion_map ;
2013-10-24 21:38:09 +00:00
typedef std : : unordered_map < expr , list < expr_pair > , expr_hash , std : : equal_to < expr > > expr_to_coercions ;
2013-09-01 23:59:15 +00:00
typedef std : : unordered_set < expr , expr_hash , std : : equal_to < expr > > coercion_set ;
2013-08-14 23:35:04 +00:00
operator_table m_nud ; // nud table for Pratt's parser
operator_table m_led ; // led table for Pratt's parser
2013-09-03 17:09:19 +00:00
expr_to_operators m_expr_to_operators ; // map denotations to operators (this is used for pretty printing)
2013-08-15 01:16:11 +00:00
implicit_table m_implicit_table ; // track the number of implicit arguments for a symbol.
2013-09-01 23:59:15 +00:00
coercion_map m_coercion_map ; // mapping from (given_type, expected_type) -> coercion
coercion_set m_coercion_set ; // Set of coercions
2013-10-24 21:38:09 +00:00
expr_to_coercions m_type_coercions ; // mapping type -> list (to-type, function)
2013-08-10 01:00:05 +00:00
2013-11-07 18:00:12 +00:00
lean_extension const * get_parent ( ) const {
return environment : : extension : : get_parent < lean_extension > ( ) ;
}
2013-08-10 01:00:05 +00:00
2013-08-15 01:16:11 +00:00
/** \brief Return the nud operator for the given symbol. */
operator_info find_nud ( name const & n ) const {
auto it = m_nud . find ( n ) ;
if ( it ! = m_nud . end ( ) )
return it - > second ;
2013-11-07 18:00:12 +00:00
lean_extension const * parent = get_parent ( ) ;
if ( parent )
return parent - > find_nud ( n ) ;
2013-08-15 01:16:11 +00:00
else
return operator_info ( ) ;
}
/** \brief Return the led operator for the given symbol. */
operator_info find_led ( name const & n ) const {
auto it = m_led . find ( n ) ;
if ( it ! = m_led . end ( ) )
return it - > second ;
2013-11-07 18:00:12 +00:00
lean_extension const * parent = get_parent ( ) ;
if ( parent )
return parent - > find_led ( n ) ;
2013-08-15 01:16:11 +00:00
else
return operator_info ( ) ;
}
/**
\ brief Return true if the given operator is defined in this
frontend object ( parent frontends are ignored ) .
*/
bool defined_here ( operator_info const & n , bool led ) const {
if ( led )
return m_led . find ( n . get_op_name ( ) ) ! = m_led . end ( ) ;
else
return m_nud . find ( n . get_op_name ( ) ) ! = m_nud . end ( ) ;
}
/** \brief Return the led/nud operator for the given symbol. */
operator_info find_op ( name const & n , bool led ) const {
return led ? find_led ( n ) : find_nud ( n ) ;
}
/** \brief Insert a new led/nud operator. */
void insert_op ( operator_info const & op , bool led ) {
if ( led )
insert ( m_led , op . get_op_name ( ) , op ) ;
else
insert ( m_nud , op . get_op_name ( ) , op ) ;
}
2013-08-20 00:25:15 +00:00
/** \brief Find the operator that is used as notation for the given expression. */
2013-09-03 17:09:19 +00:00
operator_info find_op_for ( expr const & e , bool unicode ) const {
auto it = m_expr_to_operators . find ( e ) ;
if ( it ! = m_expr_to_operators . end ( ) ) {
auto l = it - > second ;
for ( auto op : l ) {
if ( unicode | | op . is_safe_ascii ( ) )
return op ;
}
}
2013-11-07 18:00:12 +00:00
lean_extension const * parent = get_parent ( ) ;
if ( parent )
return parent - > find_op_for ( e , unicode ) ;
2013-08-15 01:16:11 +00:00
else
return operator_info ( ) ;
}
2013-08-20 00:25:15 +00:00
/** \brief Remove all internal denotations that are associated with the given operator symbol (aka notation) */
2013-08-15 01:16:11 +00:00
void remove_bindings ( operator_info const & op ) {
2013-11-07 18:00:12 +00:00
lean_extension const * parent = get_parent ( ) ;
2013-08-27 16:49:48 +00:00
for ( expr const & d : op . get_denotations ( ) ) {
2013-11-07 18:00:12 +00:00
if ( parent & & parent - > find_op_for ( d , true ) ) {
2013-08-20 00:25:15 +00:00
// parent has an association for d... we must hide it.
2013-09-03 17:09:19 +00:00
insert ( m_expr_to_operators , d , list < operator_info > ( operator_info ( ) ) ) ;
2013-08-15 01:16:11 +00:00
} else {
2013-09-03 17:09:19 +00:00
m_expr_to_operators . erase ( d ) ;
2013-08-15 01:16:11 +00:00
}
}
}
2013-11-07 18:00:12 +00:00
2013-09-03 17:09:19 +00:00
/** \brief Add a new entry d -> op in the mapping m_expr_to_operators */
void insert_expr_to_operator_entry ( expr const & d , operator_info const & op ) {
list < operator_info > & l = m_expr_to_operators [ d ] ;
l = cons ( op , l ) ;
}
2013-08-15 01:16:11 +00:00
/** \brief Register the new operator in the tables for parsing and pretty printing. */
2013-08-20 00:25:15 +00:00
void register_new_op ( operator_info new_op , expr const & d , bool led ) {
new_op . add_expr ( d ) ;
2013-08-15 01:16:11 +00:00
insert_op ( new_op , led ) ;
2013-09-03 17:09:19 +00:00
insert_expr_to_operator_entry ( d , new_op ) ;
2013-08-15 01:16:11 +00:00
}
2013-08-27 16:45:00 +00:00
/**
\ brief Two operator ( aka notation ) denotations are compatible
iff one of the following holds :
1 ) Both do not have implicit arguments
2 ) Both have implicit arguments , and the implicit arguments
occur in the same positions .
*/
bool compatible_denotation ( expr const & d1 , expr const & d2 ) {
return get_implicit_arguments ( d1 ) = = get_implicit_arguments ( d2 ) ;
}
/**
\ brief Return true iff the existing denotations ( aka
overloads ) for an operator op are compatible with the new
denotation d .
The compatibility is only an issue if implicit arguments are
used . If one of the denotations has implicit arguments , then
all of them should have implicit arguments , and the implicit
arguments should occur in the same positions .
*/
bool compatible_denotations ( operator_info const & op , expr const & d ) {
2013-08-27 16:49:48 +00:00
return std : : all_of ( op . get_denotations ( ) . begin ( ) , op . get_denotations ( ) . end ( ) , [ & ] ( expr const & prev_d ) { return compatible_denotation ( prev_d , d ) ; } ) ;
2013-08-27 16:45:00 +00:00
}
2013-08-15 01:16:11 +00:00
/**
\ brief Add a new operator and save information as object .
If the new operator does not conflict with existing operators ,
then we just register it .
If it conflicts , there are two options :
1 ) It is an overload ( we just add the internal name \ c n as
new option .
2 ) It is a real conflict , and report the issue in the
diagnostic channel , and override the existing operator ( aka notation ) .
*/
2013-11-21 23:51:29 +00:00
void add_op ( operator_info new_op , expr const & d , bool led , environment & env , io_state & st ) {
2013-08-15 01:16:11 +00:00
name const & opn = new_op . get_op_name ( ) ;
operator_info old_op = find_op ( opn , led ) ;
2013-08-16 01:54:01 +00:00
if ( ! old_op ) {
2013-08-20 00:25:15 +00:00
register_new_op ( new_op , d , led ) ;
2013-08-15 01:16:11 +00:00
} else if ( old_op = = new_op ) {
2013-08-27 16:45:00 +00:00
if ( compatible_denotations ( old_op , d ) ) {
// overload
if ( defined_here ( old_op , led ) ) {
old_op . add_expr ( d ) ;
2013-09-03 17:09:19 +00:00
insert_expr_to_operator_entry ( d , old_op ) ;
2013-08-27 16:45:00 +00:00
} else {
// we must copy the operator because it was defined in
// a parent frontend.
new_op = old_op . copy ( ) ;
register_new_op ( new_op , d , led ) ;
}
2013-08-15 01:16:11 +00:00
} else {
2013-11-07 18:00:12 +00:00
diagnostic ( st ) < < " The denotation(s) for the existing notation: \n " < < old_op
< < " \n have been replaced with the new denotation: \n " < < d
< < " \n because they conflict on how implicit arguments are used. \n " ;
2013-08-27 16:45:00 +00:00
remove_bindings ( old_op ) ;
2013-08-20 00:25:15 +00:00
register_new_op ( new_op , d , led ) ;
2013-08-15 01:16:11 +00:00
}
} else {
2013-11-07 18:00:12 +00:00
diagnostic ( st ) < < " Notation has been redefined, the existing notation: \n " < < old_op
< < " \n has been replaced with: \n " < < new_op < < " \n because they conflict with each other. \n " ;
2013-08-15 01:16:11 +00:00
remove_bindings ( old_op ) ;
2013-08-20 00:25:15 +00:00
register_new_op ( new_op , d , led ) ;
2013-08-15 01:16:11 +00:00
}
2013-11-07 18:00:12 +00:00
env . add_neutral_object ( new notation_declaration ( new_op , d ) ) ;
2013-08-15 01:16:11 +00:00
}
2013-08-30 23:37:21 +00:00
expr mk_explicit_definition_body ( expr type , name const & n , unsigned i , unsigned sz ) {
if ( i = = sz ) {
buffer < expr > args ;
args . push_back ( mk_constant ( n ) ) ;
unsigned j = sz ;
while ( j > 0 ) { - - j ; args . push_back ( mk_var ( j ) ) ; }
2013-10-26 21:46:12 +00:00
return mk_app ( args ) ;
2013-08-30 23:37:21 +00:00
} else {
lean_assert ( is_pi ( type ) ) ;
return mk_lambda ( abst_name ( type ) , abst_domain ( type ) , mk_explicit_definition_body ( abst_body ( type ) , n , i + 1 , sz ) ) ;
}
}
2013-11-07 18:00:12 +00:00
void mark_implicit_arguments ( name const & n , unsigned sz , bool const * implicit , environment & env ) {
if ( env . has_children ( ) )
2013-08-26 16:04:17 +00:00
throw exception ( sstream ( ) < < " failed to mark implicit arguments, frontend object is read-only " ) ;
2013-11-07 18:00:12 +00:00
object const & obj = env . get_object ( n ) ;
2013-10-29 22:53:50 +00:00
if ( obj . kind ( ) ! = object_kind : : Definition & & obj . kind ( ) ! = object_kind : : Postulate & & obj . kind ( ) ! = object_kind : : Builtin )
2013-08-26 16:04:17 +00:00
throw exception ( sstream ( ) < < " failed to mark implicit arguments, the object ' " < < n < < " ' is not a definition or postulate " ) ;
if ( has_implicit_arguments ( n ) )
throw exception ( sstream ( ) < < " the object ' " < < n < < " ' already has implicit argument information associated with it " ) ;
name explicit_version ( n , " explicit " ) ;
2013-11-07 18:00:12 +00:00
if ( env . find_object ( explicit_version ) )
2013-08-26 16:04:17 +00:00
throw exception ( sstream ( ) < < " failed to mark implicit arguments for ' " < < n < < " ', the frontend already has an object named ' " < < explicit_version < < " ' " ) ;
expr const & type = obj . get_type ( ) ;
unsigned num_args = 0 ;
expr it = type ;
while ( is_pi ( it ) ) { num_args + + ; it = abst_body ( it ) ; }
2013-08-27 03:21:05 +00:00
if ( sz > num_args )
throw exception ( sstream ( ) < < " failed to mark implicit arguments for ' " < < n < < " ', object has only " < < num_args < < " arguments, but trying to mark " < < sz < < " arguments " ) ;
std : : vector < bool > v ( implicit , implicit + sz ) ;
2013-08-26 16:04:17 +00:00
m_implicit_table [ n ] = mk_pair ( v , explicit_version ) ;
2013-08-30 23:37:21 +00:00
expr body = mk_explicit_definition_body ( type , n , 0 , sz ) ;
2013-08-26 16:04:17 +00:00
if ( obj . is_axiom ( ) | | obj . is_theorem ( ) ) {
2013-11-07 18:00:12 +00:00
env . add_theorem ( explicit_version , type , body ) ;
2013-08-26 16:04:17 +00:00
} else {
2013-11-07 18:00:12 +00:00
env . add_definition ( explicit_version , type , body ) ;
2013-08-26 16:04:17 +00:00
}
}
2013-11-07 18:00:12 +00:00
bool has_implicit_arguments ( name const & n ) const {
if ( m_implicit_table . find ( n ) ! = m_implicit_table . end ( ) )
2013-08-26 16:04:17 +00:00
return true ;
2013-11-07 18:00:12 +00:00
lean_extension const * parent = get_parent ( ) ;
if ( parent )
return parent - > has_implicit_arguments ( n ) ;
else
2013-08-26 16:04:17 +00:00
return false ;
}
2013-11-07 18:00:12 +00:00
std : : vector < bool > const & get_implicit_arguments ( name const & n ) const {
2013-08-26 16:04:17 +00:00
auto it = m_implicit_table . find ( n ) ;
2013-11-07 18:00:12 +00:00
if ( it ! = m_implicit_table . end ( ) )
2013-08-26 16:04:17 +00:00
return it - > second . first ;
2013-11-07 18:00:12 +00:00
lean_extension const * parent = get_parent ( ) ;
if ( parent )
return parent - > get_implicit_arguments ( n ) ;
else
2013-08-26 16:04:17 +00:00
return g_empty_vector ;
}
2013-11-07 18:00:12 +00:00
std : : vector < bool > const & get_implicit_arguments ( expr const & n ) const {
2013-08-27 16:45:00 +00:00
if ( is_constant ( n ) )
return get_implicit_arguments ( const_name ( n ) ) ;
else
return g_empty_vector ;
}
2013-11-07 18:00:12 +00:00
name const & get_explicit_version ( name const & n ) const {
2013-08-26 16:04:17 +00:00
auto it = m_implicit_table . find ( n ) ;
2013-11-07 18:00:12 +00:00
if ( it ! = m_implicit_table . end ( ) )
2013-08-26 16:04:17 +00:00
return it - > second . second ;
2013-11-07 18:00:12 +00:00
lean_extension const * parent = get_parent ( ) ;
if ( parent )
return parent - > get_explicit_version ( n ) ;
else
2013-08-26 16:04:17 +00:00
return name : : anonymous ( ) ;
}
2013-11-07 18:00:12 +00:00
bool is_explicit ( name const & n ) const {
2013-09-07 00:58:45 +00:00
return ! n . is_atomic ( ) & & get_explicit_version ( n . get_prefix ( ) ) = = n ;
}
2013-11-07 18:00:12 +00:00
void add_coercion ( expr const & f , environment & env ) {
expr type = env . infer_type ( f ) ;
expr norm_type = env . normalize ( type ) ;
2013-09-01 23:59:15 +00:00
if ( ! is_arrow ( norm_type ) )
throw exception ( " invalid coercion declaration, a coercion must have an arrow type (i.e., a non-dependent functional type) " ) ;
expr from = abst_domain ( norm_type ) ;
expr to = abst_body ( norm_type ) ;
if ( from = = to )
throw exception ( " invalid coercion declaration, 'from' and 'to' types are the same " ) ;
2013-10-24 21:38:09 +00:00
if ( get_coercion ( from , to ) )
2013-09-01 23:59:15 +00:00
throw exception ( " invalid coercion declaration, frontend already has a coercion for the given types " ) ;
m_coercion_map [ expr_pair ( from , to ) ] = f ;
m_coercion_set . insert ( f ) ;
2013-10-24 21:38:09 +00:00
list < expr_pair > l = get_coercions ( from ) ;
insert ( m_type_coercions , from , cons ( expr_pair ( to , f ) , l ) ) ;
2013-11-07 18:00:12 +00:00
env . add_neutral_object ( new coercion_declaration ( f ) ) ;
2013-09-01 23:59:15 +00:00
}
2013-12-08 07:21:07 +00:00
optional < expr > get_coercion ( expr const & from_type , expr const & to_type ) const {
2013-10-24 21:38:09 +00:00
expr_pair p ( from_type , to_type ) ;
2013-09-01 23:59:15 +00:00
auto it = m_coercion_map . find ( p ) ;
if ( it ! = m_coercion_map . end ( ) )
2013-12-08 18:34:38 +00:00
return some_expr ( it - > second ) ;
2013-11-07 18:00:12 +00:00
lean_extension const * parent = get_parent ( ) ;
if ( parent )
return parent - > get_coercion ( from_type , to_type ) ;
2013-09-01 23:59:15 +00:00
else
2013-12-08 18:34:38 +00:00
return none_expr ( ) ;
2013-09-01 23:59:15 +00:00
}
2013-10-24 21:38:09 +00:00
list < expr_pair > get_coercions ( expr const & from_type ) const {
auto r = m_type_coercions . find ( from_type ) ;
if ( r ! = m_type_coercions . end ( ) )
return r - > second ;
2013-11-07 18:00:12 +00:00
lean_extension const * parent = get_parent ( ) ;
if ( parent )
return parent - > get_coercions ( from_type ) ;
2013-10-24 21:38:09 +00:00
else
return list < expr_pair > ( ) ;
2013-09-02 02:08:49 +00:00
}
2013-11-07 18:00:12 +00:00
bool is_coercion ( expr const & f ) const {
2013-12-09 01:46:56 +00:00
if ( m_coercion_set . find ( f ) ! = m_coercion_set . end ( ) )
return true ;
lean_extension const * parent = get_parent ( ) ;
return parent & & parent - > is_coercion ( f ) ;
2013-09-01 23:59:15 +00:00
}
2013-11-07 18:00:12 +00:00
} ;
2013-09-01 23:59:15 +00:00
2013-11-07 18:00:12 +00:00
struct lean_extension_initializer {
unsigned m_extid ;
lean_extension_initializer ( ) {
m_extid = environment : : register_extension ( [ ] ( ) { return std : : unique_ptr < environment : : extension > ( new lean_extension ( ) ) ; } ) ;
2013-08-10 01:00:05 +00:00
}
2013-11-07 18:00:12 +00:00
} ;
2013-08-10 01:00:05 +00:00
2013-11-07 18:00:12 +00:00
static lean_extension_initializer g_lean_extension_initializer ;
2013-08-10 01:00:05 +00:00
2013-11-07 19:29:01 +00:00
static lean_extension const & to_ext ( environment const & env ) {
return env . get_extension < lean_extension > ( g_lean_extension_initializer . m_extid ) ;
}
static lean_extension & to_ext ( environment & env ) {
2013-11-07 18:00:12 +00:00
return env . get_extension < lean_extension > ( g_lean_extension_initializer . m_extid ) ;
}
2013-08-10 01:00:05 +00:00
2013-12-09 00:42:12 +00:00
bool is_explicit ( environment const & env , name const & n ) {
return to_ext ( env ) . is_explicit ( n ) ;
}
bool has_implicit_arguments ( environment const & env , name const & n ) {
return to_ext ( env ) . has_implicit_arguments ( n ) ;
}
name const & get_explicit_version ( environment const & env , name const & n ) {
return to_ext ( env ) . get_explicit_version ( n ) ;
}
std : : vector < bool > const & get_implicit_arguments ( environment const & env , name const & n ) {
return to_ext ( env ) . get_implicit_arguments ( n ) ;
}
bool is_coercion ( environment const & env , expr const & f ) {
return to_ext ( env ) . is_coercion ( f ) ;
}
operator_info find_op_for ( environment const & env , expr const & n , bool unicode ) {
operator_info r = to_ext ( env ) . find_op_for ( n , unicode ) ;
if ( r | | ! is_constant ( n ) ) {
return r ;
} else {
optional < object > obj = env . find_object ( const_name ( n ) ) ;
if ( obj & & obj - > is_builtin ( ) & & obj - > get_name ( ) = = const_name ( n ) )
return to_ext ( env ) . find_op_for ( obj - > get_value ( ) , unicode ) ;
else
return r ;
}
}
2013-11-07 18:00:12 +00:00
frontend : : frontend ( ) {
2013-12-09 00:42:12 +00:00
m_state . set_formatter ( mk_pp_formatter ( m_env ) ) ;
2013-11-07 18:00:12 +00:00
import_all ( m_env ) ;
2013-08-30 21:26:12 +00:00
init_builtin_notation ( * this ) ;
2013-08-20 19:19:28 +00:00
}
2013-11-21 23:51:29 +00:00
frontend : : frontend ( environment const & env , io_state const & s ) : m_env ( env ) , m_state ( s ) {
2013-11-18 02:11:44 +00:00
import_all ( m_env ) ;
init_builtin_notation ( * this ) ;
2013-08-10 01:00:05 +00:00
}
2013-11-07 18:00:12 +00:00
void frontend : : add_infix ( name const & opn , unsigned p , expr const & d ) {
to_ext ( m_env ) . add_op ( infix ( opn , p ) , d , true , m_env , m_state ) ;
}
void frontend : : add_infixl ( name const & opn , unsigned p , expr const & d ) {
to_ext ( m_env ) . add_op ( infixl ( opn , p ) , d , true , m_env , m_state ) ;
}
void frontend : : add_infixr ( name const & opn , unsigned p , expr const & d ) {
to_ext ( m_env ) . add_op ( infixr ( opn , p ) , d , true , m_env , m_state ) ;
}
void frontend : : add_prefix ( name const & opn , unsigned p , expr const & d ) {
to_ext ( m_env ) . add_op ( prefix ( opn , p ) , d , false , m_env , m_state ) ;
}
void frontend : : add_postfix ( name const & opn , unsigned p , expr const & d ) {
to_ext ( m_env ) . add_op ( postfix ( opn , p ) , d , true , m_env , m_state ) ;
}
void frontend : : add_mixfixl ( unsigned sz , name const * opns , unsigned p , expr const & d ) {
to_ext ( m_env ) . add_op ( mixfixl ( sz , opns , p ) , d , false , m_env , m_state ) ;
}
void frontend : : add_mixfixr ( unsigned sz , name const * opns , unsigned p , expr const & d ) {
to_ext ( m_env ) . add_op ( mixfixr ( sz , opns , p ) , d , true , m_env , m_state ) ;
}
void frontend : : add_mixfixc ( unsigned sz , name const * opns , unsigned p , expr const & d ) {
to_ext ( m_env ) . add_op ( mixfixc ( sz , opns , p ) , d , false , m_env , m_state ) ;
}
void frontend : : add_mixfixo ( unsigned sz , name const * opns , unsigned p , expr const & d ) {
to_ext ( m_env ) . add_op ( mixfixo ( sz , opns , p ) , d , true , m_env , m_state ) ;
}
operator_info frontend : : find_op_for ( expr const & n , bool unicode ) const {
2013-12-09 00:42:12 +00:00
return : : lean : : find_op_for ( m_env , n , unicode ) ;
2013-11-07 18:00:12 +00:00
}
operator_info frontend : : find_nud ( name const & n ) const {
return to_ext ( m_env ) . find_nud ( n ) ;
}
operator_info frontend : : find_led ( name const & n ) const {
return to_ext ( m_env ) . find_led ( n ) ;
}
void frontend : : mark_implicit_arguments ( name const & n , unsigned sz , bool const * implicit ) {
to_ext ( m_env ) . mark_implicit_arguments ( n , sz , implicit , m_env ) ;
}
void frontend : : mark_implicit_arguments ( name const & n , std : : initializer_list < bool > const & l ) {
mark_implicit_arguments ( n , l . size ( ) , l . begin ( ) ) ;
2013-08-17 17:55:42 +00:00
}
2013-10-29 22:53:50 +00:00
void frontend : : mark_implicit_arguments ( expr const & n , std : : initializer_list < bool > const & l ) {
if ( is_constant ( n ) ) {
mark_implicit_arguments ( const_name ( n ) , l ) ;
} else {
lean_assert ( is_value ( n ) ) ;
mark_implicit_arguments ( to_value ( n ) . get_name ( ) , l ) ;
}
}
2013-11-07 18:00:12 +00:00
bool frontend : : has_implicit_arguments ( name const & n ) const {
return to_ext ( m_env ) . has_implicit_arguments ( n ) ;
}
std : : vector < bool > const & frontend : : get_implicit_arguments ( name const & n ) const {
return to_ext ( m_env ) . get_implicit_arguments ( n ) ;
}
name const & frontend : : get_explicit_version ( name const & n ) const {
return to_ext ( m_env ) . get_explicit_version ( n ) ;
}
bool frontend : : is_explicit ( name const & n ) const {
return to_ext ( m_env ) . is_explicit ( n ) ;
}
void frontend : : add_coercion ( expr const & f ) {
to_ext ( m_env ) . add_coercion ( f , m_env ) ;
}
2013-12-08 07:21:07 +00:00
optional < expr > frontend : : get_coercion ( expr const & from_type , expr const & to_type ) const {
2013-11-07 18:00:12 +00:00
return to_ext ( m_env ) . get_coercion ( from_type , to_type ) ;
}
list < expr_pair > frontend : : get_coercions ( expr const & from_type ) const {
return to_ext ( m_env ) . get_coercions ( from_type ) ;
}
bool frontend : : is_coercion ( expr const & f ) const {
return to_ext ( m_env ) . is_coercion ( f ) ;
}
2013-08-10 01:00:05 +00:00
}