From 90acd1a20a65bfbed18d6326074c8fd7ca01836c Mon Sep 17 00:00:00 2001 From: Avery Date: Mon, 24 Mar 2025 11:29:41 +0100 Subject: [PATCH] Grammar and parsing for `let x: T := y in z` --- grammar.ebnf | 13 +------ src/exec/mod.rs | 1 + src/parse/mod.rs | 7 ++++ src/parse/test.rs | 85 +++++++++++++++++++++++++++++++++++++++++++ src/parse/tokenize.rs | 10 +++++ src/parser.lalrpop | 22 +++++++++-- 6 files changed, 124 insertions(+), 14 deletions(-) diff --git a/grammar.ebnf b/grammar.ebnf index 3e16d79..6f82f23 100644 --- a/grammar.ebnf +++ b/grammar.ebnf @@ -1,15 +1,6 @@ -(* - - - - - - - - - *) ast = term - | "\", {ident, [":", tagged type], ","}, ident, [":", tagged type], ".", ast ; + | "\", {ident, [":", tagged type], ","}, ident, [":", tagged type], ".", ast + | "let", {ident, [":", tagged type], ":=", ast, ","}, ident, [":", tagged type], ":=", ast, [","], "in", ast ; term = ident | constant diff --git a/src/exec/mod.rs b/src/exec/mod.rs index a5bbe43..ccc3793 100644 --- a/src/exec/mod.rs +++ b/src/exec/mod.rs @@ -30,6 +30,7 @@ impl Ast { DeBrujinAst::Abstraction(var, t, Box::new(ast.into_de_brujin_inter(gamma))) } + Ast::LetIn(_var, _t, _bind, _ast) => todo!(), Ast::Application(lhs, rhs) => DeBrujinAst::Application( Box::new(lhs.into_de_brujin_inter(gamma.clone())), Box::new(rhs.into_de_brujin_inter(gamma)), diff --git a/src/parse/mod.rs b/src/parse/mod.rs index 0a12991..e16767e 100644 --- a/src/parse/mod.rs +++ b/src/parse/mod.rs @@ -41,6 +41,7 @@ pub enum Constant { #[derive(Debug, Clone, PartialEq)] pub enum Ast { Abstraction(Ident, Option, Box), // \0:1.2 + LetIn(Ident, Option, Box, Box), // let 0:1 := 2 in 3 Application(Box, Box), // 0 1 Variable(Ident), // x Constant(Constant), // true | false | n @@ -86,6 +87,12 @@ impl Display for Ast { match self { Ast::Abstraction(var, Some(typ), ast) => write!(f, "(\\{var}:{typ}.{ast})"), Ast::Abstraction(var, None, ast) => write!(f, "(\\{var}.{ast})"), + Ast::LetIn(var, Some(typ), bind, ast) => { + write!(f, "(let {var}: {typ} := {bind} in {ast})") + } + Ast::LetIn(var, None, bind, ast) => { + write!(f, "(let {var} := {bind} in {ast})") + } Ast::Application(lhs, rhs) => write!(f, "{lhs} {rhs}"), Ast::Variable(v) => write!(f, "{v}"), Ast::Constant(constant) => write!(f, "{constant}"), diff --git a/src/parse/test.rs b/src/parse/test.rs index ae647b7..884d9db 100644 --- a/src/parse/test.rs +++ b/src/parse/test.rs @@ -194,6 +194,91 @@ fn parse_abstraction() { ); } +#[test] +fn parse_let_in() { + let parser = parser::AstParser::new(); + let ast = parser.parse(Lexer::new(r"let x:Nat := 5 in x")).unwrap(); + assert_eq!( + ast, + Ast::LetIn( + "x".to_string(), + Some(Type::Primitive(PrimitiveType::Nat).into()), + Box::new(Ast::Constant(Constant::Nat(5))), + Box::new(Ast::Variable("x".to_string())) + ) + ); + + let ast = parser + .parse(Lexer::new( + r#" + let + x:Nat := 5, + y:Any a => a -> a := \x.x, + in + y x + "#, + )) + .unwrap(); + assert_eq!( + ast, + Ast::LetIn( + "x".to_string(), + Some(Type::Primitive(PrimitiveType::Nat).into()), + Box::new(Ast::Constant(Constant::Nat(5))), + Box::new(Ast::LetIn( + "y".to_string(), + Some(TaggedType::Tagged( + TypeTag::Any, + "a".to_string(), + Box::new(TaggedType::Concrete(Type::arrow("a", "a"))) + )), + Box::new(Ast::Abstraction( + "x".to_string(), + None, + Box::new(Ast::Variable("x".to_string())) + )), + Box::new(Ast::Application( + Box::new(Ast::Variable("y".to_string())), + Box::new(Ast::Variable("x".to_string())) + )) + )) + ) + ); + + let ast = parser + .parse(Lexer::new( + r#" + let + x := 5, + y := \x.x, + in + y x + "#, + )) + .unwrap(); + assert_eq!( + ast, + Ast::LetIn( + "x".to_string(), + None, + Box::new(Ast::Constant(Constant::Nat(5))), + Box::new(Ast::LetIn( + "y".to_string(), + None, + Box::new(Ast::Abstraction( + "x".to_string(), + None, + Box::new(Ast::Variable("x".to_string())) + )), + Box::new(Ast::Application( + Box::new(Ast::Variable("y".to_string())), + Box::new(Ast::Variable("x".to_string())) + )) + )) + ) + ); +} + #[test] fn parse_application() { let parser = parser::AstParser::new(); diff --git a/src/parse/tokenize.rs b/src/parse/tokenize.rs index 9e4dd41..9f7aee1 100644 --- a/src/parse/tokenize.rs +++ b/src/parse/tokenize.rs @@ -41,6 +41,11 @@ pub enum Token { #[regex(r#"[_a-zA-Z][_a-zA-Z0-9]*'*"#, |lex| lex.slice().to_string())] Ident(String), + #[token("let")] + Let, + #[token("in")] + In, + #[token(r"\")] Lambda, #[token("=>")] @@ -53,6 +58,8 @@ pub enum Token { Period, #[token(",")] Comma, + #[token(":=")] + Becomes, #[token("=")] Equals, @@ -139,6 +146,9 @@ impl Display for Token { Token::Float(n) => write!(f, "{n}"), Token::Bool(b) => write!(f, "{b}"), Token::Ident(i) => write!(f, "{i}"), + Token::Let => write!(f, "let"), + Token::In => write!(f, "in"), + Token::Becomes => write!(f, ":="), } } } diff --git a/src/parser.lalrpop b/src/parser.lalrpop index b443dee..79ba7c7 100644 --- a/src/parser.lalrpop +++ b/src/parser.lalrpop @@ -17,12 +17,16 @@ extern { Ident => lexer::Token::Ident(), + "let" => lexer::Token::Let, + "in" => lexer::Token::In, + r"\" => lexer::Token::Lambda, "=>" => lexer::Token::FatArrow, "->" => lexer::Token::ThinArrow, ":" => lexer::Token::Colon, "." => lexer::Token::Period, "," => lexer::Token::Comma, + ":=" => lexer::Token::Becomes, "=" => lexer::Token::Equals, "<>" => lexer::Token::NotEquals, @@ -44,19 +48,31 @@ extern { } -Multi: Vec = { // (1) +Multi: Vec = { ",")*> => { v.push(e); v } }; +MultiTr: Vec = { + ",")*> ","? => { + v.push(e); + v + } +}; + pub Ast: Ast = { Term => <>, - r"\" > "." => args.into_iter().rev().fold(ast, |ast, (i, t)| Ast::Abstraction(i, t, Box::new(ast))), + r"\" > "." => + args.into_iter().rev().fold(ast, |ast, (i, t)| Ast::Abstraction(i, t, Box::new(ast))), + "let" > "in" => + binds.into_iter().rev().fold(ast, |ast, (i, t, b)| Ast::LetIn(i, t, Box::new(b), Box::new(ast))), }; -pub IdentAndType: (String, Option) = )?> => (<>); +IdentAndType: (String, Option) = )?> => (<>); + +LetBind: (String, Option, Ast) = )?> ":=" => (<>); Term: Ast = {