2013-07-29 05:34:39 +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
*/
2013-11-18 02:11:44 +00:00
# include <cstdlib>
2013-07-29 05:34:39 +00:00
# include <algorithm>
# include <vector>
2013-10-26 18:07:06 +00:00
# include <tuple>
2013-12-29 01:31:35 +00:00
# include <fstream>
# include <string>
2013-12-30 05:59:57 +00:00
# include <utility>
2013-12-09 22:56:48 +00:00
# include "util/thread.h"
2013-09-13 03:04:10 +00:00
# include "util/safe_arith.h"
2013-11-18 17:52:47 +00:00
# include "util/realpath.h"
2013-12-20 18:45:44 +00:00
# include "util/sstream.h"
2013-12-29 01:31:35 +00:00
# include "util/lean_path.h"
2013-12-29 11:43:45 +00:00
# include "util/flet.h"
2013-11-19 19:24:02 +00:00
# include "kernel/for_each_fn.h"
2013-11-19 21:03:46 +00:00
# include "kernel/find_fn.h"
2013-09-13 03:04:10 +00:00
# include "kernel/kernel_exception.h"
# include "kernel/environment.h"
2013-11-12 04:29:53 +00:00
# include "kernel/threadsafe_environment.h"
2014-02-19 06:55:00 +00:00
// #include "kernel/type_checker.h"
// #include "kernel/normalizer.h"
2013-12-29 01:31:35 +00:00
# include "version.h"
2013-07-29 05:34:39 +00:00
namespace lean {
2013-12-28 22:39:10 +00:00
class set_opaque_command : public neutral_object_cell {
name m_obj_name ;
bool m_opaque ;
public :
set_opaque_command ( name const & n , bool opaque ) : m_obj_name ( n ) , m_opaque ( opaque ) { }
virtual ~ set_opaque_command ( ) { }
2014-01-09 16:33:52 +00:00
virtual char const * keyword ( ) const { return " set_opaque " ; }
2013-12-30 03:19:24 +00:00
virtual void write ( serializer & s ) const { s < < " Opa " < < m_obj_name < < m_opaque ; }
2014-01-01 21:16:44 +00:00
name const & get_obj_name ( ) const { return m_obj_name ; }
bool get_flag ( ) const { return m_opaque ; }
2013-12-28 22:39:10 +00:00
} ;
static void read_set_opaque ( environment const & env , io_state const & , deserializer & d ) {
name n = read_name ( d ) ;
bool o = d . read_bool ( ) ;
env - > set_opaque ( n , o ) ;
}
2013-12-30 03:19:24 +00:00
static object_cell : : register_deserializer_fn set_opaque_ds ( " Opa " , read_set_opaque ) ;
2013-12-28 22:39:10 +00:00
2014-01-01 21:16:44 +00:00
bool is_set_opaque ( object const & obj ) {
return dynamic_cast < set_opaque_command const * > ( obj . cell ( ) ) ;
}
name const & get_set_opaque_id ( object const & obj ) {
lean_assert ( is_set_opaque ( obj ) ) ;
return static_cast < set_opaque_command const * > ( obj . cell ( ) ) - > get_obj_name ( ) ;
}
bool get_set_opaque_flag ( object const & obj ) {
lean_assert ( is_set_opaque ( obj ) ) ;
return static_cast < set_opaque_command const * > ( obj . cell ( ) ) - > get_flag ( ) ;
}
2013-12-29 01:31:35 +00:00
class import_command : public neutral_object_cell {
std : : string m_mod_name ;
public :
import_command ( std : : string const & n ) : m_mod_name ( n ) { }
virtual ~ import_command ( ) { }
2014-01-05 20:05:08 +00:00
virtual char const * keyword ( ) const { return " import " ; }
virtual void write ( serializer & s ) const { s < < " import " < < m_mod_name ; }
2013-12-29 03:20:04 +00:00
std : : string const & get_module ( ) const { return m_mod_name ; }
2013-12-29 01:31:35 +00:00
} ;
static void read_import ( environment const & env , io_state const & ios , deserializer & d ) {
std : : string n = d . read_string ( ) ;
env - > import ( n , ios ) ;
}
2014-01-05 20:05:08 +00:00
static object_cell : : register_deserializer_fn import_ds ( " import " , read_import ) ;
2013-12-29 01:31:35 +00:00
class end_import_mark : public neutral_object_cell {
public :
end_import_mark ( ) { }
virtual ~ end_import_mark ( ) { }
virtual char const * keyword ( ) const { return " EndImport " ; }
virtual void write ( serializer & ) const { }
} ;
// For Importing builtin modules
class begin_import_mark : public neutral_object_cell {
public :
begin_import_mark ( ) { }
virtual ~ begin_import_mark ( ) { }
virtual char const * keyword ( ) const { return " BeginImport " ; }
virtual void write ( serializer & ) const { }
} ;
bool is_begin_import ( object const & obj ) {
2013-12-29 03:20:04 +00:00
return dynamic_cast < import_command const * > ( obj . cell ( ) ) ;
}
optional < std : : string > get_imported_module ( object const & obj ) {
if ( is_begin_import ( obj ) ) {
return optional < std : : string > ( static_cast < import_command const * > ( obj . cell ( ) ) - > get_module ( ) ) ;
} else {
return optional < std : : string > ( ) ;
}
}
bool is_begin_builtin_import ( object const & obj ) {
return dynamic_cast < begin_import_mark const * > ( obj . cell ( ) ) ;
2013-12-29 01:31:35 +00:00
}
bool is_end_import ( object const & obj ) {
return dynamic_cast < end_import_mark const * > ( obj . cell ( ) ) ;
}
2013-11-07 03:21:22 +00:00
class extension_factory {
2013-12-13 00:33:31 +00:00
std : : vector < environment_cell : : mk_extension > m_makers ;
mutex m_makers_mutex ;
2013-11-07 03:21:22 +00:00
public :
2013-12-13 00:33:31 +00:00
unsigned register_extension ( environment_cell : : mk_extension mk ) {
2013-12-09 22:56:48 +00:00
lock_guard < mutex > lock ( m_makers_mutex ) ;
2013-11-07 03:21:22 +00:00
unsigned r = m_makers . size ( ) ;
m_makers . push_back ( mk ) ;
return r ;
}
2013-12-13 00:33:31 +00:00
std : : unique_ptr < environment_extension > mk ( unsigned extid ) {
2013-12-09 22:56:48 +00:00
lock_guard < mutex > lock ( m_makers_mutex ) ;
2013-11-07 03:21:22 +00:00
return m_makers [ extid ] ( ) ;
}
} ;
static std : : unique_ptr < extension_factory > g_extension_factory ;
static extension_factory & get_extension_factory ( ) {
if ( ! g_extension_factory )
g_extension_factory . reset ( new extension_factory ( ) ) ;
return * g_extension_factory ;
}
2013-12-13 00:33:31 +00:00
unsigned environment_cell : : register_extension ( mk_extension mk ) {
2013-11-07 03:21:22 +00:00
return get_extension_factory ( ) . register_extension ( mk ) ;
}
2013-12-13 00:33:31 +00:00
environment environment_cell : : env ( ) const {
lean_assert ( ! m_this . expired ( ) ) ; // it is not possible to expire since it is a reference to this object
lean_assert ( this = = m_this . lock ( ) . get ( ) ) ;
return environment ( m_this . lock ( ) ) ;
}
2013-08-04 23:07:37 +00:00
2013-12-13 00:33:31 +00:00
environment environment_cell : : parent ( ) const {
lean_assert ( has_parent ( ) ) ;
return environment ( m_parent ) ;
}
2013-07-29 05:34:39 +00:00
2013-12-13 00:33:31 +00:00
environment environment_cell : : mk_child ( ) const {
return environment ( m_this . lock ( ) , true ) ;
}
2013-08-16 22:09:26 +00:00
2013-12-13 00:33:31 +00:00
environment_extension & environment_cell : : get_extension_core ( unsigned extid ) {
if ( extid > = m_extensions . size ( ) )
m_extensions . resize ( extid + 1 ) ;
if ( ! m_extensions [ extid ] ) {
std : : unique_ptr < environment_extension > ext = get_extension_factory ( ) . mk ( extid ) ;
ext - > m_extid = extid ;
ext - > m_env = this ;
m_extensions [ extid ] . swap ( ext ) ;
2013-08-16 22:09:26 +00:00
}
2013-12-13 00:33:31 +00:00
return * ( m_extensions [ extid ] . get ( ) ) ;
}
2013-08-16 22:09:26 +00:00
2013-12-13 00:33:31 +00:00
environment_extension const & environment_cell : : get_extension_core ( unsigned extid ) const {
return const_cast < environment_cell * > ( this ) - > get_extension_core ( extid ) ;
}
2013-08-16 22:09:26 +00:00
2013-12-13 00:33:31 +00:00
unsigned environment_cell : : get_max_weight ( expr const & e ) {
unsigned w = 0 ;
auto proc = [ & ] ( expr const & c , unsigned ) {
if ( is_constant ( c ) ) {
optional < object > obj = get_object_core ( const_name ( c ) ) ;
if ( obj )
w = std : : max ( w , obj - > get_weight ( ) ) ;
2013-08-16 22:09:26 +00:00
}
2013-12-13 00:33:31 +00:00
return true ;
} ;
2014-02-19 06:55:00 +00:00
for_each_fn visitor ( proc ) ;
2013-12-13 00:33:31 +00:00
visitor ( e ) ;
return w ;
}
2013-08-16 22:09:26 +00:00
2013-12-13 00:33:31 +00:00
/** \brief Throw exception if environment or its ancestors already have an object with the given name. */
void environment_cell : : check_name_core ( name const & n ) {
if ( has_parent ( ) )
m_parent - > check_name_core ( n ) ;
if ( m_object_dictionary . find ( n ) ! = m_object_dictionary . end ( ) )
2014-02-19 06:55:00 +00:00
throw_already_declared ( env ( ) , n ) ;
2013-12-13 00:33:31 +00:00
}
2013-08-16 22:09:26 +00:00
2013-12-13 00:33:31 +00:00
void environment_cell : : check_name ( name const & n ) {
if ( has_children ( ) )
2014-02-19 06:55:00 +00:00
throw_read_only_environment ( env ( ) ) ;
2013-12-13 00:33:31 +00:00
check_name_core ( n ) ;
}
2013-07-29 05:34:39 +00:00
2014-02-24 19:05:42 +00:00
void environment_cell : : check_level_cnstrs ( param_names const & ps , level_cnstrs const & ls ) {
if ( has_meta ( ls ) > 0 )
2014-02-23 22:41:44 +00:00
throw_kernel_exception ( env ( ) , " invalid level constraint, it contains level placeholders (aka meta-parameters that must be synthesized by Lean's elaborator " ) ;
2014-02-24 19:05:42 +00:00
if ( auto it = get_undef_param ( ls , ps ) )
2014-02-23 22:41:44 +00:00
throw_kernel_exception ( env ( ) , " invalid level constraints, it contains undefined parameters " ) ;
}
2013-12-13 00:33:31 +00:00
/** \brief Store new named object inside internal data-structures */
void environment_cell : : register_named_object ( object const & new_obj ) {
m_objects . push_back ( new_obj ) ;
m_object_dictionary . insert ( std : : make_pair ( new_obj . get_name ( ) , new_obj ) ) ;
}
2013-07-29 05:34:39 +00:00
2013-12-13 00:33:31 +00:00
/**
\ brief Return the object named \ c n in the environment or its
ancestors . Return null object if there is no object with the
given name .
*/
optional < object > environment_cell : : get_object_core ( name const & n ) const {
auto it = m_object_dictionary . find ( n ) ;
if ( it = = m_object_dictionary . end ( ) ) {
2013-08-05 00:47:54 +00:00
if ( has_parent ( ) )
2013-12-13 00:33:31 +00:00
return m_parent - > get_object_core ( n ) ;
2013-08-05 00:47:54 +00:00
else
2013-12-13 00:33:31 +00:00
return none_object ( ) ;
} else {
return some_object ( it - > second ) ;
2013-08-13 22:13:54 +00:00
}
2013-12-13 00:33:31 +00:00
}
2013-08-13 22:13:54 +00:00
2013-12-13 00:33:31 +00:00
object environment_cell : : get_object ( name const & n ) const {
optional < object > obj = get_object_core ( n ) ;
if ( obj ) {
return * obj ;
} else {
2014-02-19 06:55:00 +00:00
throw_unknown_object ( env ( ) , n ) ;
2013-08-06 03:06:07 +00:00
}
2013-12-13 00:33:31 +00:00
}
2013-08-06 03:06:07 +00:00
2013-12-13 00:33:31 +00:00
/**
2014-02-19 06:55:00 +00:00
The kernel should * not * accept expressions containing Local or Meta .
Reason : they may introduce unsoundness .
2013-12-13 00:33:31 +00:00
*/
2014-02-19 06:55:00 +00:00
void environment_cell : : check_no_mlocal ( expr const & e ) {
if ( find ( e , [ ] ( expr const & a , unsigned ) { return is_mlocal ( a ) ; } ) )
throw_kernel_exception ( env ( ) , " expression has metavariable and/or local constants, this is a bug in one of Lean tactics and/or solvers " ) ; // LCOV_EXCL_LINE
2013-11-17 02:35:17 +00:00
}
2013-12-13 00:33:31 +00:00
/**
\ brief Throw an exception if \ c t is not a type or type of \ c
v is not convertible to \ c t .
*/
void environment_cell : : check_type ( name const & n , expr const & t , expr const & v ) {
2014-02-19 06:55:00 +00:00
#if 0
2013-12-29 11:43:45 +00:00
if ( m_type_check ) {
m_type_checker - > check_type ( t ) ;
expr v_t = m_type_checker - > check ( v ) ;
if ( ! m_type_checker - > is_convertible ( v_t , t ) )
throw def_type_mismatch_exception ( env ( ) , n , t , v , v_t ) ;
}
2014-02-19 06:55:00 +00:00
# endif
}
void environment_cell : : check_type ( expr const & t ) {
#if 0
if ( m_type_check )
m_type_checker - > check_type ( t ) ;
# endif
2013-07-29 05:34:39 +00:00
}
2013-12-13 00:33:31 +00:00
/** \brief Throw exception if it is not a valid new definition */
2014-02-24 19:05:42 +00:00
void environment_cell : : check_new_definition ( name const & n , param_names const & ps , level_cnstrs const & cs , expr const & t , expr const & v ) {
2013-12-13 00:33:31 +00:00
check_name ( n ) ;
2014-02-24 19:05:42 +00:00
check_level_cnstrs ( ps , cs ) ;
2013-12-13 00:33:31 +00:00
check_type ( n , t , v ) ;
2013-08-04 23:07:37 +00:00
}
2013-12-13 00:33:31 +00:00
/** \brief Add new definition. */
2014-02-24 19:05:42 +00:00
void environment_cell : : add_definition ( name const & n , param_names const & ps , level_cnstrs const & cs , expr const & t , expr const & v ) {
2014-02-19 06:55:00 +00:00
check_no_mlocal ( t ) ;
check_no_mlocal ( v ) ;
2014-02-24 19:05:42 +00:00
check_new_definition ( n , ps , cs , t , v ) ;
2013-12-13 00:33:31 +00:00
unsigned w = get_max_weight ( v ) + 1 ;
2014-02-24 19:05:42 +00:00
register_named_object ( mk_definition ( n , ps , cs , t , v , w ) ) ;
2013-08-04 23:07:37 +00:00
}
2013-08-09 22:33:34 +00:00
2013-12-13 00:33:31 +00:00
/**
\ brief Add new definition .
The type of the new definition is the type of \ c v .
*/
2014-02-23 22:41:44 +00:00
void environment_cell : : add_definition ( name const & n , expr const & v ) {
2014-02-19 06:55:00 +00:00
check_no_mlocal ( v ) ;
2013-12-13 00:33:31 +00:00
check_name ( n ) ;
2013-12-29 11:43:45 +00:00
expr v_t ;
2014-02-19 06:55:00 +00:00
#if 0
2013-12-29 11:43:45 +00:00
if ( m_type_check )
v_t = m_type_checker - > check ( v ) ;
else
v_t = m_type_checker - > infer_type ( v ) ;
2014-02-19 06:55:00 +00:00
# endif
2013-12-13 00:33:31 +00:00
unsigned w = get_max_weight ( v ) + 1 ;
2014-02-24 19:05:42 +00:00
register_named_object ( mk_definition ( n , param_names ( ) , level_cnstrs ( ) , v_t , v , w ) ) ;
2013-08-09 22:33:34 +00:00
}
2013-12-13 00:33:31 +00:00
/** \brief Add new theorem. */
2014-02-24 19:05:42 +00:00
void environment_cell : : add_theorem ( name const & n , param_names const & ps , level_cnstrs const & cs , expr const & t , expr const & v ) {
2014-02-19 06:55:00 +00:00
check_no_mlocal ( t ) ;
check_no_mlocal ( v ) ;
2014-02-24 19:05:42 +00:00
check_new_definition ( n , ps , cs , t , v ) ;
register_named_object ( mk_theorem ( n , ps , cs , t , v ) ) ;
2013-08-09 22:33:34 +00:00
}
2013-12-20 18:45:44 +00:00
void environment_cell : : set_opaque ( name const & n , bool opaque ) {
auto obj = find_object ( n ) ;
if ( ! obj | | ! obj - > is_definition ( ) )
2014-02-19 06:55:00 +00:00
throw_kernel_exception ( env ( ) , sstream ( ) < < " set_opaque failed, ' " < < n < < " ' is not a definition " ) ;
2013-12-20 18:45:44 +00:00
obj - > set_opaque ( opaque ) ;
2013-12-28 22:39:10 +00:00
add_neutral_object ( new set_opaque_command ( n , opaque ) ) ;
2013-12-20 18:45:44 +00:00
}
2013-12-13 00:33:31 +00:00
/** \brief Add new axiom. */
2014-02-24 19:05:42 +00:00
void environment_cell : : add_axiom ( name const & n , param_names const & ps , level_cnstrs const & cs , expr const & t ) {
2014-02-19 06:55:00 +00:00
check_no_mlocal ( t ) ;
2013-12-13 00:33:31 +00:00
check_name ( n ) ;
2014-02-24 19:05:42 +00:00
check_level_cnstrs ( ps , cs ) ;
2014-02-19 06:55:00 +00:00
check_type ( t ) ;
2014-02-24 19:05:42 +00:00
register_named_object ( mk_axiom ( n , ps , cs , t ) ) ;
2013-08-05 00:47:54 +00:00
}
2013-12-13 00:33:31 +00:00
/** \brief Add new variable. */
2014-02-24 19:05:42 +00:00
void environment_cell : : add_var ( name const & n , param_names const & ps , level_cnstrs const & cs , expr const & t ) {
2014-02-19 06:55:00 +00:00
check_no_mlocal ( t ) ;
2013-12-13 00:33:31 +00:00
check_name ( n ) ;
2014-02-24 19:05:42 +00:00
check_level_cnstrs ( ps , cs ) ;
2014-02-19 06:55:00 +00:00
check_type ( t ) ;
2014-02-24 19:05:42 +00:00
register_named_object ( mk_var_decl ( n , ps , cs , t ) ) ;
2013-09-04 15:30:04 +00:00
}
2013-12-13 00:33:31 +00:00
void environment_cell : : add_neutral_object ( neutral_object_cell * o ) {
m_objects . push_back ( mk_neutral ( o ) ) ;
2013-09-04 15:30:04 +00:00
}
2013-12-13 00:33:31 +00:00
unsigned environment_cell : : get_num_objects ( bool local ) const {
if ( local | | ! has_parent ( ) ) {
return m_objects . size ( ) ;
} else {
return m_objects . size ( ) + m_parent - > get_num_objects ( false ) ;
}
2013-08-05 03:52:14 +00:00
}
2013-12-13 00:33:31 +00:00
object const & environment_cell : : get_object ( unsigned i , bool local ) const {
if ( local | | ! has_parent ( ) ) {
return m_objects [ i ] ;
} else {
unsigned num_parent_objects = m_parent - > get_num_objects ( false ) ;
if ( i > = num_parent_objects )
return m_objects [ i - num_parent_objects ] ;
else
return m_parent - > get_object ( i , false ) ;
}
2013-08-06 19:24:20 +00:00
}
2014-02-19 06:55:00 +00:00
expr environment_cell : : type_check ( expr const & e ) const {
#if 0
2013-12-22 19:51:38 +00:00
return m_type_checker - > check ( e , ctx ) ;
2014-02-19 06:55:00 +00:00
# else
return e ;
# endif
2013-12-22 19:51:38 +00:00
}
2014-02-19 06:55:00 +00:00
expr environment_cell : : infer_type ( expr const & e ) const {
#if 0
2013-12-13 00:33:31 +00:00
return m_type_checker - > infer_type ( e , ctx ) ;
2014-02-19 06:55:00 +00:00
# else
return e ;
# endif
2013-08-05 03:52:14 +00:00
}
2014-02-19 06:55:00 +00:00
expr environment_cell : : normalize ( expr const & e ) const {
#if 0
refactor(kernel): add unfold_opaque flag to normalizer, modify how type checker uses the opaque flag, remove hidden_defs, and mark most builtin definitions as opaque
After this commit, in the type checker, when checking convertability, we first compute a normal form without expanding opaque terms.
If the terms are convertible, then we are done, and saved a lot of time by not expanding unnecessary definitions.
If they are not, instead of throwing an error, we try again expanding the opaque terms.
This seems to be the best of both worlds.
The opaque flag is a hint for the type checker, but it would never prevent us from type checking a valid term.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 20:47:36 +00:00
return m_type_checker - > get_normalizer ( ) ( e , ctx , unfold_opaque ) ;
2014-02-19 06:55:00 +00:00
# else
return e ;
# endif
2013-08-06 03:06:07 +00:00
}
2014-02-19 06:55:00 +00:00
bool environment_cell : : is_proposition ( expr const & e ) const {
#if 0
2014-01-15 19:02:47 +00:00
return m_type_checker - > is_proposition ( e , ctx ) ;
2014-02-19 06:55:00 +00:00
# else
return false ;
# endif
2014-01-15 19:02:47 +00:00
}
2013-12-13 00:33:31 +00:00
bool environment_cell : : already_imported ( name const & n ) const {
if ( m_imported_modules . find ( n ) ! = m_imported_modules . end ( ) )
return true ;
else if ( has_parent ( ) )
return m_parent - > already_imported ( n ) ;
else
return false ;
2013-08-15 01:16:11 +00:00
}
2013-12-13 00:33:31 +00:00
bool environment_cell : : mark_imported_core ( name n ) {
if ( already_imported ( n ) ) {
return false ;
} else if ( has_children ( ) ) {
2014-02-19 06:55:00 +00:00
throw_read_only_environment ( env ( ) ) ;
2013-12-13 00:33:31 +00:00
} else {
m_imported_modules . insert ( n ) ;
return true ;
}
2013-08-05 03:52:14 +00:00
}
2013-12-13 00:33:31 +00:00
bool environment_cell : : mark_imported ( char const * fname ) {
return mark_imported_core ( name ( realpath ( fname ) ) ) ;
2013-08-17 17:55:42 +00:00
}
2013-12-29 01:31:35 +00:00
void environment_cell : : auxiliary_section ( std : : function < void ( ) > fn ) {
add_neutral_object ( new begin_import_mark ( ) ) ;
try {
fn ( ) ;
add_neutral_object ( new end_import_mark ( ) ) ;
} catch ( . . . ) {
add_neutral_object ( new end_import_mark ( ) ) ;
throw ;
}
}
2013-12-29 11:43:45 +00:00
void environment_cell : : set_trusted_imported ( bool flag ) {
m_trust_imported = flag ;
}
2013-12-29 01:31:35 +00:00
static char const * g_olean_header = " oleanfile " ;
static char const * g_olean_end_file = " EndFile " ;
void environment_cell : : export_objects ( std : : string const & fname ) {
2013-12-31 02:20:36 +00:00
std : : ofstream out ( fname , std : : ofstream : : binary ) ;
2013-12-29 01:31:35 +00:00
serializer s ( out ) ;
s < < g_olean_header < < LEAN_VERSION_MAJOR < < LEAN_VERSION_MINOR ;
auto it = begin_objects ( ) ;
auto end = end_objects ( ) ;
unsigned num_imports = 0 ;
for ( ; it ! = end ; + + it ) {
object const & obj = * it ;
if ( dynamic_cast < import_command const * > ( obj . cell ( ) ) ) {
if ( num_imports = = 0 )
obj . write ( s ) ;
num_imports + + ;
} else if ( dynamic_cast < end_import_mark const * > ( obj . cell ( ) ) ) {
lean_assert ( num_imports > 0 ) ;
num_imports - - ;
} else if ( dynamic_cast < begin_import_mark const * > ( obj . cell ( ) ) ) {
num_imports + + ;
} else if ( num_imports = = 0 ) {
obj . write ( s ) ;
}
}
s < < g_olean_end_file ;
}
2013-12-29 03:20:04 +00:00
bool environment_cell : : load_core ( std : : string const & fname , io_state const & ios , optional < std : : string > const & mod_name ) {
if ( ! mod_name | | mark_imported_core ( fname ) ) {
2013-12-31 02:20:36 +00:00
std : : ifstream in ( fname , std : : ifstream : : binary ) ;
2013-12-29 03:20:04 +00:00
if ( ! in . good ( ) )
2014-02-19 06:55:00 +00:00
throw_kernel_exception ( env ( ) , sstream ( ) < < " failed to open file ' " < < fname < < " ' " ) ;
2013-12-29 01:31:35 +00:00
deserializer d ( in ) ;
std : : string header ;
d > > header ;
if ( header ! = g_olean_header )
2014-02-19 06:55:00 +00:00
throw_kernel_exception ( env ( ) , sstream ( ) < < " file ' " < < fname < < " ' does not seem to be a valid object Lean file " ) ;
2013-12-29 01:31:35 +00:00
unsigned major , minor ;
// Perhaps we should enforce the right version number
d > > major > > minor ;
try {
2013-12-29 03:20:04 +00:00
if ( mod_name )
add_neutral_object ( new import_command ( * mod_name ) ) ;
2013-12-29 01:31:35 +00:00
while ( true ) {
std : : string k ;
d > > k ;
if ( k = = g_olean_end_file ) {
2013-12-29 03:20:04 +00:00
if ( mod_name )
add_neutral_object ( new end_import_mark ( ) ) ;
2013-12-29 01:31:35 +00:00
return true ;
}
read_object ( env ( ) , ios , k , d ) ;
}
} catch ( . . . ) {
2013-12-29 03:20:04 +00:00
if ( mod_name )
add_neutral_object ( new end_import_mark ( ) ) ;
2013-12-29 01:31:35 +00:00
throw ;
}
} else {
return false ;
}
2013-08-08 23:12:46 +00:00
}
2013-12-29 03:20:04 +00:00
bool environment_cell : : import ( std : : string const & fname , io_state const & ios ) {
2013-12-29 11:43:45 +00:00
flet < bool > set ( m_type_check , ! m_trust_imported ) ;
2013-12-29 03:20:04 +00:00
return load_core ( realpath ( find_file ( fname , { " .olean " } ) . c_str ( ) ) , ios , optional < std : : string > ( fname ) ) ;
}
void environment_cell : : load ( std : : string const & fname , io_state const & ios ) {
load_core ( fname , ios , optional < std : : string > ( ) ) ;
}
2014-01-15 00:41:40 +00:00
bool environment_cell : : imported ( std : : string const & n ) const {
2014-01-31 07:02:19 +00:00
try {
return already_imported ( name ( realpath ( find_file ( n , { " .olean " } ) . c_str ( ) ) ) ) ;
} catch ( . . . ) {
// module named n does not even exist
return false ;
}
2014-01-15 00:41:40 +00:00
}
2013-12-13 00:33:31 +00:00
environment_cell : : environment_cell ( ) :
m_num_children ( 0 ) {
2013-12-29 11:43:45 +00:00
m_trust_imported = false ;
m_type_check = true ;
2013-08-08 23:12:46 +00:00
}
2013-12-13 00:33:31 +00:00
environment_cell : : environment_cell ( std : : shared_ptr < environment_cell > const & parent ) :
m_num_children ( 0 ) ,
m_parent ( parent ) {
2013-12-29 11:43:45 +00:00
m_trust_imported = false ;
m_type_check = true ;
2013-12-13 00:33:31 +00:00
parent - > inc_children ( ) ;
2013-09-01 23:59:15 +00:00
}
2013-12-13 00:33:31 +00:00
environment_cell : : ~ environment_cell ( ) {
if ( m_parent )
m_parent - > dec_children ( ) ;
2013-09-01 23:59:15 +00:00
}
2013-12-13 00:33:31 +00:00
environment : : environment ( ) :
2013-12-24 19:32:09 +00:00
m_ptr ( std : : make_shared < environment_cell > ( ) ) {
2013-12-13 00:33:31 +00:00
m_ptr - > m_this = m_ptr ;
2014-02-19 06:55:00 +00:00
#if 0
2013-12-13 00:33:31 +00:00
m_ptr - > m_type_checker . reset ( new type_checker ( * this ) ) ;
2014-02-19 06:55:00 +00:00
# endif
2013-08-06 03:06:07 +00:00
}
2013-08-24 23:11:35 +00:00
2013-12-13 00:33:31 +00:00
// used when creating a new child environment
environment : : environment ( std : : shared_ptr < environment_cell > const & parent , bool ) :
2013-12-24 19:32:09 +00:00
m_ptr ( std : : make_shared < environment_cell > ( parent ) ) {
2013-12-13 00:33:31 +00:00
m_ptr - > m_this = m_ptr ;
2014-02-19 06:55:00 +00:00
#if 0
2013-12-13 00:33:31 +00:00
m_ptr - > m_type_checker . reset ( new type_checker ( * this ) ) ;
2014-02-19 06:55:00 +00:00
# endif
2013-11-18 02:11:44 +00:00
}
2013-12-13 00:33:31 +00:00
// used when creating a reference to the parent environment
environment : : environment ( std : : shared_ptr < environment_cell > const & ptr ) :
m_ptr ( ptr ) {
2013-11-18 02:11:44 +00:00
}
2013-12-13 00:33:31 +00:00
ro_environment : : ro_environment ( environment const & env ) :
m_ptr ( env . m_ptr ) {
2013-11-07 19:29:01 +00:00
}
2013-12-13 00:33:31 +00:00
ro_environment : : ro_environment ( weak_ref const & r ) {
if ( r . expired ( ) )
2014-02-19 06:55:00 +00:00
throw_kernel_exception ( * this , " weak reference to environment object has expired (i.e., the environment has been deleted) " ) ;
2013-12-13 00:33:31 +00:00
m_ptr = r . lock ( ) ;
2013-11-07 03:21:22 +00:00
}
2013-12-13 00:33:31 +00:00
environment_extension : : environment_extension ( ) :
2013-11-07 03:21:22 +00:00
m_env ( nullptr ) ,
m_extid ( 0 ) {
}
2013-12-13 00:33:31 +00:00
environment_extension : : ~ environment_extension ( ) {
2013-11-07 03:21:22 +00:00
}
2013-12-13 00:33:31 +00:00
environment_extension const * environment_extension : : get_parent_core ( ) const {
2013-11-07 03:21:22 +00:00
if ( m_env = = nullptr )
return nullptr ;
2013-12-13 00:33:31 +00:00
environment_cell * parent = m_env - > m_parent . get ( ) ;
2013-11-07 03:21:22 +00:00
while ( parent ) {
if ( m_extid < parent - > m_extensions . size ( ) ) {
2013-12-13 00:33:31 +00:00
environment_extension * ext = parent - > m_extensions [ m_extid ] . get ( ) ;
2013-11-07 03:21:22 +00:00
if ( ext )
return ext ;
}
parent = parent - > m_parent . get ( ) ;
}
return nullptr ;
}
2013-11-12 04:29:53 +00:00
2013-12-13 00:33:31 +00:00
read_only_shared_environment : : read_only_shared_environment ( ro_environment const & env ) :
2013-11-12 04:29:53 +00:00
m_env ( env ) ,
2013-12-13 00:33:31 +00:00
m_lock ( const_cast < environment_cell * > ( m_env . m_ptr . get ( ) ) - > m_mutex ) {
2013-11-12 04:29:53 +00:00
}
2013-12-12 19:19:09 +00:00
read_only_shared_environment : : ~ read_only_shared_environment ( ) { }
2013-11-12 04:29:53 +00:00
2013-12-12 19:19:09 +00:00
read_write_shared_environment : : read_write_shared_environment ( environment const & env ) :
2013-11-12 04:29:53 +00:00
m_env ( env ) ,
m_lock ( m_env . m_ptr - > m_mutex ) {
}
2013-12-12 19:19:09 +00:00
read_write_shared_environment : : ~ read_write_shared_environment ( ) { }
2013-07-29 05:34:39 +00:00
}