mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-08-16 11:50:40 +03:00
fix: parsing of open
This commit is contained in:
parent
668233184f
commit
d8eeb510e5
@ -618,14 +618,17 @@ impl<'a> Parser<'a> {
|
||||
self.advance(); // 'open'
|
||||
let type_name = self.parse_upper_id()?;
|
||||
let var_name = self.parse_id()?;
|
||||
let next = self.parse_expr(false)?;
|
||||
let end = next.range;
|
||||
|
||||
let motive = self.try_single(&|this| {
|
||||
this.eat_variant(Token::Colon)?;
|
||||
this.parse_expr(false)
|
||||
})?;
|
||||
|
||||
self.check_and_eat(Token::Semi);
|
||||
|
||||
let next = self.parse_expr(false)?;
|
||||
let end = next.range;
|
||||
|
||||
Ok(Box::new(Expr {
|
||||
data: ExprKind::Open { type_name, var_name, motive, next },
|
||||
range: start.mix(end),
|
||||
|
@ -0,0 +1 @@
|
||||
Ok!
|
14
crates/kind-tests/suite/checker/SimpleOpenWithMotive.kind2
Normal file
14
crates/kind-tests/suite/checker/SimpleOpenWithMotive.kind2
Normal file
@ -0,0 +1,14 @@
|
||||
#derive[match]
|
||||
record Pudim {
|
||||
owo : U60
|
||||
uwu : U60
|
||||
}
|
||||
|
||||
#keep
|
||||
Ok (n: Pudim) : U60
|
||||
Ok n =
|
||||
open Pudim n : _;
|
||||
(+ n.owo n.uwu)
|
||||
|
||||
Main : U60
|
||||
Main = Ok (Pudim.new 10 20)
|
Loading…
Reference in New Issue
Block a user