Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implement optional patterns #1569

Merged
merged 3 commits into from
Aug 23, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions Sources/FrontEnd/AST/AST+Walk.swift
Original file line number Diff line number Diff line change
Expand Up @@ -160,6 +160,8 @@ extension AST {
traverse(self[n] as! ExprPattern, notifying: &o)
case NamePattern.self:
traverse(self[n] as! NamePattern, notifying: &o)
case OptionPattern.self:
traverse(self[n] as! OptionPattern, notifying: &o)
case TuplePattern.self:
traverse(self[n] as! TuplePattern, notifying: &o)
case WildcardPattern.self:
Expand Down Expand Up @@ -637,6 +639,13 @@ extension AST {
walk(n.decl, notifying: &o)
}

/// Visits the children of `n` in pre-order, notifying `o` when a node is entered or left.
public func traverse<O: ASTWalkObserver>(
_ n: OptionPattern, notifying o: inout O
) {
walk(n.name, notifying: &o)
}

/// Visits the children of `n` in pre-order, notifying `o` when a node is entered or left.
public func traverse<O: ASTWalkObserver>(
_ n: TuplePattern, notifying o: inout O
Expand Down
14 changes: 14 additions & 0 deletions Sources/FrontEnd/AST/AST.swift
Original file line number Diff line number Diff line change
Expand Up @@ -189,6 +189,16 @@ public struct AST {
/// Indicates whether the Core library has been loaded.
public var coreModuleIsLoaded: Bool { coreLibrary != nil }

/// Returns the Hylo type of an optional `t`.
///
/// - Requires: The Core library must have been loaded.
public func optional(_ t: AnyType) -> UnionType {
let none = coreType("None")!
let p = self[none.decl].genericParameters[0]
let u = BoundGenericType(none, arguments: [p: .type(t)])
return UnionType([t, ^u])
}

/// Returns the type named `name` defined in the core library or `nil` it does not exist.
///
/// - Requires: The Core library must have been loaded.
Expand Down Expand Up @@ -421,6 +431,10 @@ public struct AST {
case NamePattern.self:
result.append((subfield: subfield, pattern: NamePattern.ID(pattern)!))

case OptionPattern.self:
let n = self[OptionPattern.ID(pattern)!].name
result.append((subfield: subfield, pattern: n))

case TuplePattern.self:
let x = TuplePattern.ID(pattern)!
for i in 0 ..< self[x].elements.count {
Expand Down
1 change: 1 addition & 0 deletions Sources/FrontEnd/AST/NodeIDs/NodeKind.swift
Original file line number Diff line number Diff line change
Expand Up @@ -132,6 +132,7 @@ extension NodeKind {
BindingPattern.self,
ExprPattern.self,
NamePattern.self,
OptionPattern.self,
TuplePattern.self,
WildcardPattern.self,

Expand Down
14 changes: 14 additions & 0 deletions Sources/FrontEnd/AST/Pattern/OptionPattern.swift
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
/// A pattern that matches the presence of a value in an optional.
public struct OptionPattern: Pattern {

public let site: SourceRange

/// The expression of the pattern.
public let name: NamePattern.ID

public init(name: NamePattern.ID, site: SourceRange) {
self.site = site
self.name = name
}

}
10 changes: 8 additions & 2 deletions Sources/FrontEnd/Parse/Parser.swift
Original file line number Diff line number Diff line change
Expand Up @@ -2579,10 +2579,16 @@ public enum Parser {
return AnyPatternID(p)
}

// Attempt to parse a name pattern if we're in the context of a binding pattern.
// Attempt to parse a name or option pattern if we're in the context of a binding pattern.
if state.contexts.last == .bindingPattern {
if let p = try namePattern.parse(&state) {
return AnyPatternID(p)
if let mark = state.takePostfixQuestionMark() {
let s = state.ast[p].site.extended(toCover: mark.site)
let o = state.insert(OptionPattern(name: p, site: s))
return AnyPatternID(o)
} else {
return AnyPatternID(p)
}
}
}

Expand Down
4 changes: 4 additions & 0 deletions Sources/FrontEnd/TypeChecking/TypeChecker+Diagnostics.swift
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,10 @@ extension Diagnostic {
.error("declaration of \(a) binding requires an initializer", at: site)
}

static func error(invalidOptionPattern p: OptionPattern.ID, in ast: AST) -> Diagnostic {
.error("optional pattern may only be used as a condition", at: ast[p].site)
}

static func error(circularRefinementAt site: SourceRange) -> Diagnostic {
.error("circular trait refinement", at: site)
}
Expand Down
66 changes: 48 additions & 18 deletions Sources/FrontEnd/TypeChecking/TypeChecker.swift
Original file line number Diff line number Diff line change
Expand Up @@ -5087,9 +5087,8 @@
updating obligations: inout ProofObligations
) -> AnyType {
let p = program[d].pattern
let pattern = inferredType(
of: p.id, withHint: purpose.filteredType, updating: &obligations)
if pattern[.hasError] { return pattern }
let lhs = inferredType(of: p.id, withHint: purpose.filteredType, updating: &obligations)
if lhs[.hasError] { return lhs }

// If `d` has no initializer, its type is that of its annotation, if present. Otherwise, its
// pattern must be used as a filter and `d` is inferred to have the same type.
Expand All @@ -5101,40 +5100,60 @@
report(.error(binding: p.introducer.value, requiresInitializerAt: p.introducer.site))
return .error
} else {
return pattern
return lhs
}

case .condition:
assert(p.annotation != nil, "expected type annotation")
return pattern
return lhs

Check warning on line 5108 in Sources/FrontEnd/TypeChecking/TypeChecker.swift

View check run for this annotation

Codecov / codecov/patch

Sources/FrontEnd/TypeChecking/TypeChecker.swift#L5108

Added line #L5108 was not covered by tests

case .filter:
return pattern
return lhs
}
}

// Note: `i` should not have been assigned a type if before `d` is checked.
assert(cache.local.exprType[i] == nil)
let initializer = constrain(i, to: ^freshVariable(), in: &obligations)
let rhs = constrain(i, to: ^freshVariable(), in: &obligations)

// If `d` has no annotation, its type is inferred as that of its initializer. Otherwise, the
// type of its initializer must be subtype or supertype of its pattern if the latter is used
// irrefutably or as a condition/filter, respectively.
if p.annotation == nil {
// If `p` is an option pattern, the initializer must be an option of the pattern's type.
// E.g. `if let x? = y { ... }`
if let q = OptionPattern.ID(p.subpattern.id) {
if purpose == .irrefutable {
report(.error(invalidOptionPattern: q, in: program.ast))
return .error
} else {
let u = program.ast.optional(lhs)
let o = ConstraintOrigin(.optionalBinding, at: program[i].site)
obligations.insert(EqualityConstraint(^u, rhs, origin: o))
}
}

// If `d` has no annotation, its type is inferred as that of its initializer.
// E.g. `let x = 42`
else if p.annotation == nil {
let o = ConstraintOrigin(.initializationWithPattern, at: program[i].site)
obligations.insert(EqualityConstraint(initializer, pattern, origin: o))
} else if purpose == .irrefutable {
obligations.insert(EqualityConstraint(rhs, lhs, origin: o))
}

// If `d` is used irrefutably, the initializer's type must be subtype of the pattern's.
// E.g. `let x: Int = 42`
else if purpose == .irrefutable {
let o = ConstraintOrigin(.initializationWithHint, at: program[i].site)
obligations.insert(SubtypingConstraint(initializer, pattern, origin: o))
} else {
obligations.insert(SubtypingConstraint(rhs, lhs, origin: o))
}

// If `d` is used as a condition, the initializer's type must be supertype of the pattern's.
// E.g. `if let x: Int = y { ... }`
else {
let o = ConstraintOrigin(.optionalBinding, at: program[i].site)
obligations.insert(SubtypingConstraint(pattern, initializer, origin: o))
obligations.insert(SubtypingConstraint(lhs, rhs, origin: o))
}

// Collect the proof obligations for the initializer. The resulting type can be discarded; the
// type of `i` will be assigned after the all proof obligations are discharged.
_ = inferredType(of: i, withHint: pattern, updating: &obligations)
return pattern
_ = inferredType(of: i, withHint: lhs, updating: &obligations)
return lhs
}

/// Returns the inferred type of `e`, updating `obligations` and gathering contextual information
Expand Down Expand Up @@ -5907,6 +5926,8 @@
return inferredType(of: ExprPattern.ID(p)!, withHint: hint, updating: &obligations)
case NamePattern.self:
return inferredType(of: NamePattern.ID(p)!, withHint: hint, updating: &obligations)
case OptionPattern.self:
return inferredType(of: OptionPattern.ID(p)!, withHint: hint, updating: &obligations)
case TuplePattern.self:
return inferredType(of: TuplePattern.ID(p)!, withHint: hint, updating: &obligations)
case WildcardPattern.self:
Expand Down Expand Up @@ -5960,6 +5981,15 @@
return t
}

/// Returns the inferred type of `p`, updating `obligations` and gathering contextual information
/// from `hint`.
private mutating func inferredType(
of p: OptionPattern.ID, withHint hint: AnyType? = nil,
updating obligations: inout ProofObligations
) -> AnyType {
inferredType(of: program[p].name, updating: &obligations)
}

/// Returns the inferred type of `p`, updating `obligations` and gathering contextual information
/// from `hint`.
private mutating func inferredType(
Expand Down
8 changes: 8 additions & 0 deletions Tests/HyloTests/ParserTests.swift
Original file line number Diff line number Diff line change
Expand Up @@ -1504,6 +1504,14 @@ final class ParserTests: XCTestCase {
XCTAssertEqual(ast[pattern.decl].baseName, "foo")
}

func testOptionPattern() throws {
let input: SourceFile = "let foo?"
let (p, ast) = try input.parse(with: Parser.parseBindingPattern(in:))
let b = try XCTUnwrap(p)
let o = try XCTUnwrap(OptionPattern.ID(ast[b].subpattern))
XCTAssertEqual(ast[ast[ast[o].name].decl].baseName, "foo")
}

func testTuplePattern() throws {
let input: SourceFile = "()"
let (patternID, ast) = try apply(Parser.tuplePattern, on: input)
Expand Down
12 changes: 12 additions & 0 deletions Tests/HyloTests/TestCases/TypeChecking/OptionPattern.hylo
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
//- typeCheck expecting: .failure

fun use<T>(_ x: T) {}

public fun main() {
let x: Optional<Int> = 42 as _

if let y? = x { use<Int>(y) }

//! @+1 diagnostic optional pattern may only be used as a condition
let z? : Int = 0
}