+36

Sources/PterodactylBuild/Elaborator/ElabRules.swift

Reviewed

··· 577 577 } 578 578 } 579 579 580 580 + struct RecordProj: ElabTypedTerm, HasProvenance { 581 581 + let provenance: Range<Int>? 582 582 + let target: ElabTypedTerm 583 583 + let fieldName: String 584 584 + 585 585 + func elabTypedTerm(_ env: ElabEnv) async throws(ElabError) -> (Value.Type_, Term) { 586 586 + let (recordType, recordTerm) = try await target.elabTypedTerm(env) 587 587 + switch await recordType.whnf() { 588 588 + case let .recordType(fields: fields): 589 589 + 590 590 + guard let field = fields[fieldName] else { 591 591 + throw ElabError( 592 592 + Diagnostic( 593 593 + message: "This record does not have a field named `\(fieldName)`.", 594 594 + severity: .warning, 595 595 + absoluteRange: provenance 596 596 + ) 597 597 + ) 598 598 + } 599 599 + 600 600 + let recordValue = await env.evaluator().evaluate(term: recordTerm) 601 601 + let fieldType = field.type.instantiate(with: recordValue) 602 602 + return (fieldType, .cut(term: recordTerm, frame: .proj(fieldName: fieldName))) 603 603 + 604 604 + default: 605 605 + throw ElabError( 606 606 + Diagnostic( 607 607 + message: "Cannot project from element of non-record type.", 608 608 + severity: .warning, 609 609 + absoluteRange: provenance 610 610 + ) 611 611 + ) 612 612 + } 613 613 + } 614 614 + } 615 615 + 580 616 struct Lambda: ElabTerm, HasProvenance { 581 617 let provenance: Range<Int>? 582 618 let binder: UntypedBinder

+3 -1

examples/test.ptero

Reviewed

··· 1 1 2 2 exampleRecord : (A : Type) (x : A) -> {tp : Type; elt : tp} 3 3 - exampleRecord A x => {tp => A; elt => x} 3 3 + exampleRecord A x => {tp => A; elt => x} 4 4 + 5 5 + foo : {tp:Type} -> Type