@@ -31,7 +31,8 @@ impl Context {
3131 let mut named = Self :: builtin_mono_trait ( NAMED , 2 ) ;
3232 named. register_builtin_erg_decl ( FUNC_NAME , Str , Visibility :: BUILTIN_PUBLIC ) ;
3333 let mut sized = Self :: builtin_mono_trait ( SIZED , 2 ) ;
34- let t = fn0_met ( mono ( SIZED ) , Nat ) . quantify ( ) ;
34+ let ret_t = if PYTHON_MODE { Int } else { Nat } ;
35+ let t = fn0_met ( mono ( SIZED ) , ret_t) . quantify ( ) ;
3536 sized. register_builtin_erg_decl ( FUNDAMENTAL_LEN , t, Visibility :: BUILTIN_PUBLIC ) ;
3637 let mut copy = Self :: builtin_mono_trait ( COPY , 2 ) ;
3738 let Slf = mono_q ( SELF , subtypeof ( mono ( COPY ) ) ) ;
@@ -227,15 +228,24 @@ impl Context {
227228 /* Iterable */
228229 let mut iterable = Self :: builtin_poly_trait ( ITERABLE , vec ! [ PS :: t_nd( TY_T ) ] , 2 ) ;
229230 iterable. register_superclass ( poly ( OUTPUT , vec ! [ ty_tp( T . clone( ) ) ] ) , & output) ;
230- let Slf = mono_q ( SELF , subtypeof ( poly ( ITERABLE , vec ! [ ty_tp( T . clone( ) ) ] ) ) ) ;
231- let t = fn0_met ( Slf . clone ( ) , proj ( Slf , ITER ) ) . quantify ( ) ;
232- iterable. register_builtin_decl (
233- FUNC_ITER ,
234- t,
235- Visibility :: BUILTIN_PUBLIC ,
236- Some ( FUNDAMENTAL_ITER ) ,
237- ) ;
238- iterable. register_builtin_erg_decl ( ITER , Type , Visibility :: BUILTIN_PUBLIC ) ;
231+ if PYTHON_MODE {
232+ let t = fn0_met (
233+ poly ( ITERABLE , vec ! [ ty_tp( T . clone( ) ) ] ) ,
234+ poly ( ITERATOR , vec ! [ ty_tp( T . clone( ) ) ] ) ,
235+ )
236+ . quantify ( ) ;
237+ iterable. register_builtin_erg_decl ( FUNDAMENTAL_ITER , t, Visibility :: BUILTIN_PUBLIC ) ;
238+ } else {
239+ let Slf = mono_q ( SELF , subtypeof ( poly ( ITERABLE , vec ! [ ty_tp( T . clone( ) ) ] ) ) ) ;
240+ let t = fn0_met ( Slf . clone ( ) , proj ( Slf , ITER ) ) . quantify ( ) ;
241+ iterable. register_builtin_decl (
242+ FUNC_ITER ,
243+ t,
244+ Visibility :: BUILTIN_PUBLIC ,
245+ Some ( FUNDAMENTAL_ITER ) ,
246+ ) ;
247+ iterable. register_builtin_erg_decl ( ITER , Type , Visibility :: BUILTIN_PUBLIC ) ;
248+ }
239249 let Slf = poly ( ITERABLE , vec ! [ ty_tp( T . clone( ) ) ] ) ;
240250 let U = type_q ( TY_U ) ;
241251 let t_map = fn1_met (
@@ -244,9 +254,10 @@ impl Context {
244254 poly ( MAP , vec ! [ ty_tp( U . clone( ) ) ] ) ,
245255 )
246256 . quantify ( ) ;
247- iterable. register_builtin_decl (
257+ iterable. register_builtin_py_impl (
248258 FUNC_MAP ,
249259 t_map,
260+ Mutability :: Immutable ,
250261 Visibility :: BUILTIN_PUBLIC ,
251262 Some ( "Function::iterable_map" ) ,
252263 ) ;
@@ -268,9 +279,10 @@ impl Context {
268279 )
269280 . quantify ( ) ;
270281 let t_filter = t_filter. with_default_intersec_index ( 1 ) ;
271- iterable. register_builtin_decl (
282+ iterable. register_builtin_py_impl (
272283 FUNC_FILTER ,
273284 t_filter,
285+ Mutability :: Immutable ,
274286 Visibility :: BUILTIN_PUBLIC ,
275287 Some ( "Function::iterable_filter" ) ,
276288 ) ;
@@ -279,9 +291,10 @@ impl Context {
279291 vec ! [ TyParam :: List ( vec![ ty_tp( Nat ) , ty_tp( T . clone( ) ) ] ) ] ,
280292 ) ;
281293 let t_enumerate = fn0_met ( Slf . clone ( ) , poly ( ITERATOR , vec ! [ ty_tp( ret_t) ] ) ) . quantify ( ) ;
282- iterable. register_builtin_decl (
294+ iterable. register_builtin_py_impl (
283295 FUNC_ENUMERATE ,
284296 t_enumerate,
297+ Mutability :: Immutable ,
285298 Visibility :: BUILTIN_PUBLIC ,
286299 Some ( "Function::enumerate" ) ,
287300 ) ;
@@ -291,9 +304,10 @@ impl Context {
291304 poly ( ZIP , vec ! [ ty_tp( T . clone( ) ) , ty_tp( U . clone( ) ) ] ) ,
292305 )
293306 . quantify ( ) ;
294- iterable. register_builtin_decl (
307+ iterable. register_builtin_py_impl (
295308 FUNC_ZIP ,
296309 t_zip,
310+ Mutability :: Immutable ,
297311 Visibility :: BUILTIN_PUBLIC ,
298312 Some ( "Function::zip" ) ,
299313 ) ;
@@ -304,59 +318,67 @@ impl Context {
304318 T . clone ( ) ,
305319 )
306320 . quantify ( ) ;
307- iterable. register_builtin_decl (
321+ iterable. register_builtin_py_impl (
308322 FUNC_REDUCE ,
309323 t_reduce,
324+ Mutability :: Immutable ,
310325 Visibility :: BUILTIN_PUBLIC ,
311326 Some ( "Function::iterable_reduce" ) ,
312327 ) ;
313328 let t_nth = fn1_met ( Slf . clone ( ) , Nat , T . clone ( ) ) . quantify ( ) ;
314- iterable. register_builtin_decl (
329+ iterable. register_builtin_py_impl (
315330 FUNC_NTH ,
316331 t_nth,
332+ Mutability :: Immutable ,
317333 Visibility :: BUILTIN_PUBLIC ,
318334 Some ( "Function::iterable_nth" ) ,
319335 ) ;
320336 let t_skip = fn1_met ( Slf . clone ( ) , Nat , poly ( ITERATOR , vec ! [ ty_tp( T . clone( ) ) ] ) ) . quantify ( ) ;
321- iterable. register_builtin_decl (
337+ iterable. register_builtin_py_impl (
322338 FUNC_SKIP ,
323339 t_skip,
340+ Mutability :: Immutable ,
324341 Visibility :: BUILTIN_PUBLIC ,
325342 Some ( "Function::iterable_skip" ) ,
326343 ) ;
327344 let t_all = fn1_met ( Slf . clone ( ) , func1 ( T . clone ( ) , Bool ) , Bool ) . quantify ( ) ;
328- iterable. register_builtin_decl (
345+ iterable. register_builtin_py_impl (
329346 FUNC_ALL ,
330347 t_all,
348+ Mutability :: Immutable ,
331349 Visibility :: BUILTIN_PUBLIC ,
332350 Some ( "Function::iterable_all" ) ,
333351 ) ;
334352 let t_any = fn1_met ( Slf . clone ( ) , func1 ( T . clone ( ) , Bool ) , Bool ) . quantify ( ) ;
335- iterable. register_builtin_decl (
353+ iterable. register_builtin_py_impl (
336354 FUNC_ANY ,
337355 t_any,
356+ Mutability :: Immutable ,
338357 Visibility :: BUILTIN_PUBLIC ,
339358 Some ( "Function::iterable_any" ) ,
340359 ) ;
341360 let t_reversed = fn0_met ( Slf . clone ( ) , poly ( ITERATOR , vec ! [ ty_tp( T . clone( ) ) ] ) ) . quantify ( ) ;
342- iterable. register_builtin_decl (
361+ iterable. register_builtin_py_impl (
343362 FUNC_REVERSED ,
344363 t_reversed,
364+ Mutability :: Immutable ,
345365 Visibility :: BUILTIN_PUBLIC ,
346366 Some ( "Function::reversed" ) ,
347367 ) ;
348368 let t_position = fn1_met ( Slf . clone ( ) , func1 ( T . clone ( ) , Bool ) , or ( Nat , NoneType ) ) . quantify ( ) ;
349- iterable. register_builtin_decl (
369+ iterable. register_builtin_py_impl (
350370 FUNC_POSITION ,
351371 t_position,
372+ Mutability :: Immutable ,
352373 Visibility :: BUILTIN_PUBLIC ,
353374 Some ( "Function::iterable_position" ) ,
354375 ) ;
355376 let t_find =
356377 fn1_met ( Slf . clone ( ) , func1 ( T . clone ( ) , Bool ) , or ( T . clone ( ) , NoneType ) ) . quantify ( ) ;
357- iterable. register_builtin_decl (
378+ iterable. register_builtin_py_impl (
358379 FUNC_FIND ,
359380 t_find,
381+ Mutability :: Immutable ,
360382 Visibility :: BUILTIN_PUBLIC ,
361383 Some ( "Function::iterable_find" ) ,
362384 ) ;
@@ -369,16 +391,18 @@ impl Context {
369391 poly ( ITERATOR , vec ! [ ty_tp( T . clone( ) ) ] ) ,
370392 )
371393 . quantify ( ) ;
372- iterable. register_builtin_decl (
394+ iterable. register_builtin_py_impl (
373395 FUNC_CHAIN ,
374396 t_chain,
397+ Mutability :: Immutable ,
375398 Visibility :: BUILTIN_PUBLIC ,
376399 Some ( "Function::iterable_chain" ) ,
377400 ) ;
378401 let t_to_list = fn0_met ( Slf . clone ( ) , unknown_len_list_t ( T . clone ( ) ) ) . quantify ( ) ;
379- iterable. register_builtin_decl (
402+ iterable. register_builtin_py_impl (
380403 FUNC_TO_LIST ,
381404 t_to_list,
405+ Mutability :: Immutable ,
382406 Visibility :: BUILTIN_PUBLIC ,
383407 Some ( "Function::list" ) ,
384408 ) ;
@@ -396,7 +420,7 @@ impl Context {
396420 ) ;
397421 /* Container */
398422 let mut container = Self :: builtin_poly_trait ( CONTAINER , vec ! [ PS :: t_nd( TY_T ) ] , 2 ) ;
399- let op_t = fn1_met ( mono ( CONTAINER ) , T . clone ( ) , Bool ) . quantify ( ) ;
423+ let op_t = fn1_met ( poly ( CONTAINER , vec ! [ ty_tp ( T . clone ( ) ) ] ) , T . clone ( ) , Bool ) . quantify ( ) ;
400424 container. register_superclass ( poly ( OUTPUT , vec ! [ ty_tp( T . clone( ) ) ] ) , & output) ;
401425 container. register_builtin_erg_decl ( FUNDAMENTAL_CONTAINS , op_t, Visibility :: BUILTIN_PUBLIC ) ;
402426 /* Collection */
0 commit comments