@@ -12,7 +12,7 @@ use std::ops::Range;
12
12
use std:: sync:: Arc ;
13
13
14
14
use crate :: lang:: core;
15
- use crate :: lang:: core:: semantics:: { self , Elim , Head , RecordClosure , Unfold , Value } ;
15
+ use crate :: lang:: core:: semantics:: { self , Elim , RecordClosure , Unfold , Value } ;
16
16
use crate :: lang:: surface:: { Term , TermData } ;
17
17
use crate :: literal;
18
18
use crate :: pass:: core_to_surface;
@@ -310,111 +310,69 @@ impl<'me> State<'me> {
310
310
)
311
311
}
312
312
313
- ( TermData :: SequenceTerm ( entry_terms) , Value :: Stuck ( Head :: Global ( name, _) , spine) ) => {
314
- match ( name. as_ref ( ) , spine. as_slice ( ) ) {
315
- ( "Array" , [ Elim :: Function ( len) , Elim :: Function ( core_entry_type) ] ) => {
316
- let core_entry_type = core_entry_type. force ( self . globals ) ;
317
- let core_entry_terms = entry_terms
318
- . iter ( )
319
- . map ( |entry_term| {
320
- Arc :: new ( self . check_type ( entry_term, core_entry_type) )
321
- } )
322
- . collect ( ) ;
323
-
324
- let len = len. force ( self . globals ) ;
325
- match len. as_ref ( ) {
326
- Value :: Constant ( core:: Constant :: U32 ( len) )
327
- if * len as usize == entry_terms. len ( ) =>
328
- {
329
- core:: Term :: new (
330
- term. range ( ) ,
331
- core:: TermData :: SequenceTerm ( core_entry_terms) ,
332
- )
333
- }
334
- Value :: Error => core:: Term :: new ( term. range ( ) , core:: TermData :: Error ) ,
335
- _ => {
336
- let expected_len = self . read_back_to_surface_term ( & len) ;
337
- self . report ( SurfaceToCoreMessage :: MismatchedSequenceLength {
338
- range : term. range ( ) ,
339
- found_len : entry_terms. len ( ) ,
340
- expected_len,
341
- } ) ;
342
- core:: Term :: new ( term. range ( ) , core:: TermData :: Error )
343
- }
313
+ ( TermData :: SequenceTerm ( entry_terms) , forced_type) => match forced_type. try_global ( ) {
314
+ Some ( ( "Array" , _, [ Elim :: Function ( len) , Elim :: Function ( core_entry_type) ] ) ) => {
315
+ let core_entry_type = core_entry_type. force ( self . globals ) ;
316
+ let core_entry_terms = entry_terms
317
+ . iter ( )
318
+ . map ( |entry_term| Arc :: new ( self . check_type ( entry_term, core_entry_type) ) )
319
+ . collect ( ) ;
320
+
321
+ let len = len. force ( self . globals ) ;
322
+ match len. as_ref ( ) {
323
+ Value :: Constant ( core:: Constant :: U32 ( len) )
324
+ if * len as usize == entry_terms. len ( ) =>
325
+ {
326
+ core:: Term :: new (
327
+ term. range ( ) ,
328
+ core:: TermData :: SequenceTerm ( core_entry_terms) ,
329
+ )
330
+ }
331
+ Value :: Error => core:: Term :: new ( term. range ( ) , core:: TermData :: Error ) ,
332
+ _ => {
333
+ let expected_len = self . read_back_to_surface_term ( & len) ;
334
+ self . report ( SurfaceToCoreMessage :: MismatchedSequenceLength {
335
+ range : term. range ( ) ,
336
+ found_len : entry_terms. len ( ) ,
337
+ expected_len,
338
+ } ) ;
339
+ core:: Term :: new ( term. range ( ) , core:: TermData :: Error )
344
340
}
345
- }
346
- ( "List" , [ Elim :: Function ( core_entry_type) ] ) => {
347
- let core_entry_type = core_entry_type. force ( self . globals ) ;
348
- let core_entry_terms = entry_terms
349
- . iter ( )
350
- . map ( |entry_term| {
351
- Arc :: new ( self . check_type ( entry_term, core_entry_type) )
352
- } )
353
- . collect ( ) ;
354
-
355
- core:: Term :: new (
356
- term. range ( ) ,
357
- core:: TermData :: SequenceTerm ( core_entry_terms) ,
358
- )
359
- }
360
- _ => {
361
- let expected_type = self . read_back_to_surface_term ( expected_type) ;
362
- self . report ( SurfaceToCoreMessage :: NoSequenceConversion {
363
- range : term. range ( ) ,
364
- expected_type,
365
- } ) ;
366
- core:: Term :: new ( term. range ( ) , core:: TermData :: Error )
367
341
}
368
342
}
369
- }
370
- ( TermData :: SequenceTerm ( _) , _) => {
371
- let expected_type = self . read_back_to_surface_term ( expected_type) ;
372
- self . report ( SurfaceToCoreMessage :: NoSequenceConversion {
373
- range : term. range ( ) ,
374
- expected_type,
375
- } ) ;
376
- core:: Term :: new ( term. range ( ) , core:: TermData :: Error )
377
- }
378
-
379
- ( TermData :: NumberTerm ( data) , Value :: Stuck ( Head :: Global ( name, _) , spine) ) => {
380
- match ( name. as_ref ( ) , spine. as_slice ( ) ) {
381
- ( "U8" , [ ] ) => self . parse_unsigned ( term. range ( ) , data, core:: Constant :: U8 ) ,
382
- ( "U16" , [ ] ) => self . parse_unsigned ( term. range ( ) , data, core:: Constant :: U16 ) ,
383
- ( "U32" , [ ] ) => self . parse_unsigned ( term. range ( ) , data, core:: Constant :: U32 ) ,
384
- ( "U64" , [ ] ) => self . parse_unsigned ( term. range ( ) , data, core:: Constant :: U64 ) ,
385
- ( "S8" , [ ] ) => self . parse_signed ( term. range ( ) , data, core:: Constant :: S8 ) ,
386
- ( "S16" , [ ] ) => self . parse_signed ( term. range ( ) , data, core:: Constant :: S16 ) ,
387
- ( "S32" , [ ] ) => self . parse_signed ( term. range ( ) , data, core:: Constant :: S32 ) ,
388
- ( "S64" , [ ] ) => self . parse_signed ( term. range ( ) , data, core:: Constant :: S64 ) ,
389
- ( "F32" , [ ] ) => self . parse_float ( term. range ( ) , data, core:: Constant :: F32 ) ,
390
- ( "F64" , [ ] ) => self . parse_float ( term. range ( ) , data, core:: Constant :: F64 ) ,
391
- ( _, _) => {
392
- let expected_type = self . read_back_to_surface_term ( expected_type) ;
393
- self . report ( SurfaceToCoreMessage :: NoLiteralConversion {
394
- range : term. range ( ) ,
395
- expected_type,
396
- } ) ;
397
- core:: Term :: new ( term. range ( ) , core:: TermData :: Error )
398
- }
343
+ Some ( ( "List" , _, [ Elim :: Function ( core_entry_type) ] ) ) => {
344
+ let core_entry_type = core_entry_type. force ( self . globals ) ;
345
+ let core_entry_terms = entry_terms
346
+ . iter ( )
347
+ . map ( |entry_term| Arc :: new ( self . check_type ( entry_term, core_entry_type) ) )
348
+ . collect ( ) ;
349
+
350
+ core:: Term :: new ( term. range ( ) , core:: TermData :: SequenceTerm ( core_entry_terms) )
399
351
}
400
- }
401
- ( TermData :: CharTerm ( data) , Value :: Stuck ( Head :: Global ( name, _) , spine) ) => {
402
- match ( name. as_ref ( ) , spine. as_slice ( ) ) {
403
- ( "Char" , [ ] ) => self . parse_char ( term. range ( ) , data) ,
404
- ( _, _) => {
405
- let expected_type = self . read_back_to_surface_term ( expected_type) ;
406
- self . report ( SurfaceToCoreMessage :: NoLiteralConversion {
407
- range : term. range ( ) ,
408
- expected_type,
409
- } ) ;
410
- core:: Term :: new ( term. range ( ) , core:: TermData :: Error )
411
- }
352
+ Some ( _) | None => {
353
+ let expected_type = self . read_back_to_surface_term ( expected_type) ;
354
+ self . report ( SurfaceToCoreMessage :: NoSequenceConversion {
355
+ range : term. range ( ) ,
356
+ expected_type,
357
+ } ) ;
358
+ core:: Term :: new ( term. range ( ) , core:: TermData :: Error )
412
359
}
413
- }
414
- ( TermData :: StringTerm ( data) , Value :: Stuck ( Head :: Global ( name, _) , spine) ) => {
415
- match ( name. as_ref ( ) , spine. as_slice ( ) ) {
416
- ( "String" , [ ] ) => self . parse_string ( term. range ( ) , data) ,
417
- ( _, _) => {
360
+ } ,
361
+ ( TermData :: NumberTerm ( data) , forced_type) => {
362
+ use crate :: lang:: core:: Constant :: * ;
363
+
364
+ match forced_type. try_global ( ) {
365
+ Some ( ( "U8" , _, [ ] ) ) => self . parse_unsigned ( term. range ( ) , data, U8 ) ,
366
+ Some ( ( "U16" , _, [ ] ) ) => self . parse_unsigned ( term. range ( ) , data, U16 ) ,
367
+ Some ( ( "U32" , _, [ ] ) ) => self . parse_unsigned ( term. range ( ) , data, U32 ) ,
368
+ Some ( ( "U64" , _, [ ] ) ) => self . parse_unsigned ( term. range ( ) , data, U64 ) ,
369
+ Some ( ( "S8" , _, [ ] ) ) => self . parse_signed ( term. range ( ) , data, S8 ) ,
370
+ Some ( ( "S16" , _, [ ] ) ) => self . parse_signed ( term. range ( ) , data, S16 ) ,
371
+ Some ( ( "S32" , _, [ ] ) ) => self . parse_signed ( term. range ( ) , data, S32 ) ,
372
+ Some ( ( "S64" , _, [ ] ) ) => self . parse_signed ( term. range ( ) , data, S64 ) ,
373
+ Some ( ( "F32" , _, [ ] ) ) => self . parse_float ( term. range ( ) , data, F32 ) ,
374
+ Some ( ( "F64" , _, [ ] ) ) => self . parse_float ( term. range ( ) , data, F64 ) ,
375
+ Some ( _) | None => {
418
376
let expected_type = self . read_back_to_surface_term ( expected_type) ;
419
377
self . report ( SurfaceToCoreMessage :: NoLiteralConversion {
420
378
range : term. range ( ) ,
@@ -424,16 +382,28 @@ impl<'me> State<'me> {
424
382
}
425
383
}
426
384
}
427
- ( TermData :: NumberTerm ( _) , _)
428
- | ( TermData :: CharTerm ( _) , _)
429
- | ( TermData :: StringTerm ( _) , _) => {
430
- let expected_type = self . read_back_to_surface_term ( expected_type) ;
431
- self . report ( SurfaceToCoreMessage :: NoLiteralConversion {
432
- range : term. range ( ) ,
433
- expected_type,
434
- } ) ;
435
- core:: Term :: new ( term. range ( ) , core:: TermData :: Error )
436
- }
385
+ ( TermData :: CharTerm ( data) , forced_type) => match forced_type. try_global ( ) {
386
+ Some ( ( "Char" , _, [ ] ) ) => self . parse_char ( term. range ( ) , data) ,
387
+ Some ( _) | None => {
388
+ let expected_type = self . read_back_to_surface_term ( expected_type) ;
389
+ self . report ( SurfaceToCoreMessage :: NoLiteralConversion {
390
+ range : term. range ( ) ,
391
+ expected_type,
392
+ } ) ;
393
+ core:: Term :: new ( term. range ( ) , core:: TermData :: Error )
394
+ }
395
+ } ,
396
+ ( TermData :: StringTerm ( data) , forced_type) => match forced_type. try_global ( ) {
397
+ Some ( ( "String" , _, [ ] ) ) => self . parse_string ( term. range ( ) , data) ,
398
+ Some ( _) | None => {
399
+ let expected_type = self . read_back_to_surface_term ( expected_type) ;
400
+ self . report ( SurfaceToCoreMessage :: NoLiteralConversion {
401
+ range : term. range ( ) ,
402
+ expected_type,
403
+ } ) ;
404
+ core:: Term :: new ( term. range ( ) , core:: TermData :: Error )
405
+ }
406
+ } ,
437
407
438
408
( _, _) => match self . synth_type ( term) {
439
409
( term, found_type) if self . is_subtype ( & found_type, expected_type) => term,
0 commit comments