From 8a5ac6d222d90c8f9e69e381804c83878aad02d2 Mon Sep 17 00:00:00 2001 From: Dimi Racordon Date: Fri, 23 Aug 2024 22:07:39 +0200 Subject: [PATCH 1/3] Parse option patterns --- Sources/FrontEnd/AST/AST+Walk.swift | 9 +++++++++ Sources/FrontEnd/AST/NodeIDs/NodeKind.swift | 1 + Sources/FrontEnd/AST/Pattern/OptionPattern.swift | 14 ++++++++++++++ Sources/FrontEnd/Parse/Parser.swift | 10 ++++++++-- Tests/HyloTests/ParserTests.swift | 8 ++++++++ 5 files changed, 40 insertions(+), 2 deletions(-) create mode 100644 Sources/FrontEnd/AST/Pattern/OptionPattern.swift diff --git a/Sources/FrontEnd/AST/AST+Walk.swift b/Sources/FrontEnd/AST/AST+Walk.swift index f764af16a..06e459242 100644 --- a/Sources/FrontEnd/AST/AST+Walk.swift +++ b/Sources/FrontEnd/AST/AST+Walk.swift @@ -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: @@ -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( + _ 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( _ n: TuplePattern, notifying o: inout O diff --git a/Sources/FrontEnd/AST/NodeIDs/NodeKind.swift b/Sources/FrontEnd/AST/NodeIDs/NodeKind.swift index 492546ddb..765f125ce 100644 --- a/Sources/FrontEnd/AST/NodeIDs/NodeKind.swift +++ b/Sources/FrontEnd/AST/NodeIDs/NodeKind.swift @@ -132,6 +132,7 @@ extension NodeKind { BindingPattern.self, ExprPattern.self, NamePattern.self, + OptionPattern.self, TuplePattern.self, WildcardPattern.self, diff --git a/Sources/FrontEnd/AST/Pattern/OptionPattern.swift b/Sources/FrontEnd/AST/Pattern/OptionPattern.swift new file mode 100644 index 000000000..f9234fe8f --- /dev/null +++ b/Sources/FrontEnd/AST/Pattern/OptionPattern.swift @@ -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 + } + +} diff --git a/Sources/FrontEnd/Parse/Parser.swift b/Sources/FrontEnd/Parse/Parser.swift index 9c975999d..e849cd471 100644 --- a/Sources/FrontEnd/Parse/Parser.swift +++ b/Sources/FrontEnd/Parse/Parser.swift @@ -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) + } } } diff --git a/Tests/HyloTests/ParserTests.swift b/Tests/HyloTests/ParserTests.swift index cf9418a47..6f75cf01b 100644 --- a/Tests/HyloTests/ParserTests.swift +++ b/Tests/HyloTests/ParserTests.swift @@ -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) From 38aad4f436281edb1396dc83c20fd78ab4794868 Mon Sep 17 00:00:00 2001 From: Dimi Racordon Date: Fri, 23 Aug 2024 23:28:16 +0200 Subject: [PATCH 2/3] Add a helper to get the Hylo type of an optional --- Sources/FrontEnd/AST/AST.swift | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/Sources/FrontEnd/AST/AST.swift b/Sources/FrontEnd/AST/AST.swift index 57ee86d38..0341f8370 100644 --- a/Sources/FrontEnd/AST/AST.swift +++ b/Sources/FrontEnd/AST/AST.swift @@ -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. From a962208326302f794c6ba6efde48fcb7dbdd8ca8 Mon Sep 17 00:00:00 2001 From: Dimi Racordon Date: Fri, 23 Aug 2024 23:28:59 +0200 Subject: [PATCH 3/3] Type check option patterns --- Sources/FrontEnd/AST/AST.swift | 4 ++ .../TypeChecker+Diagnostics.swift | 4 ++ .../FrontEnd/TypeChecking/TypeChecker.swift | 66 ++++++++++++++----- .../TestCases/TypeChecking/OptionPattern.hylo | 12 ++++ 4 files changed, 68 insertions(+), 18 deletions(-) create mode 100644 Tests/HyloTests/TestCases/TypeChecking/OptionPattern.hylo diff --git a/Sources/FrontEnd/AST/AST.swift b/Sources/FrontEnd/AST/AST.swift index 0341f8370..9eafe3c5a 100644 --- a/Sources/FrontEnd/AST/AST.swift +++ b/Sources/FrontEnd/AST/AST.swift @@ -431,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 { diff --git a/Sources/FrontEnd/TypeChecking/TypeChecker+Diagnostics.swift b/Sources/FrontEnd/TypeChecking/TypeChecker+Diagnostics.swift index 2200ac9ec..598e23bb9 100644 --- a/Sources/FrontEnd/TypeChecking/TypeChecker+Diagnostics.swift +++ b/Sources/FrontEnd/TypeChecking/TypeChecker+Diagnostics.swift @@ -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) } diff --git a/Sources/FrontEnd/TypeChecking/TypeChecker.swift b/Sources/FrontEnd/TypeChecking/TypeChecker.swift index ffe653813..3b8d27bf8 100644 --- a/Sources/FrontEnd/TypeChecking/TypeChecker.swift +++ b/Sources/FrontEnd/TypeChecking/TypeChecker.swift @@ -5087,9 +5087,8 @@ struct TypeChecker { 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. @@ -5101,40 +5100,60 @@ struct TypeChecker { 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 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 @@ -5907,6 +5926,8 @@ struct TypeChecker { 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: @@ -5960,6 +5981,15 @@ struct TypeChecker { 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( diff --git a/Tests/HyloTests/TestCases/TypeChecking/OptionPattern.hylo b/Tests/HyloTests/TestCases/TypeChecking/OptionPattern.hylo new file mode 100644 index 000000000..aee7f7a38 --- /dev/null +++ b/Tests/HyloTests/TestCases/TypeChecking/OptionPattern.hylo @@ -0,0 +1,12 @@ +//- typeCheck expecting: .failure + +fun use(_ x: T) {} + +public fun main() { + let x: Optional = 42 as _ + + if let y? = x { use(y) } + + //! @+1 diagnostic optional pattern may only be used as a condition + let z? : Int = 0 +}