Grammar and parsing for `let x: T := y in z`

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 

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)),

src/parse/mod.rs

@@ -41,6 +41,7 @@ pub enum Constant {
 #[derive(Debug, Clone, PartialEq)]
 pub enum Ast {
     Abstraction(Ident, Option<TaggedType>, Box<Ast>), // \0:1.2
+    LetIn(Ident, Option<TaggedType>, Box<Ast>, Box<Ast>), // let 0:1 := 2 in 3
     Application(Box<Ast>, Box<Ast>),                  // 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}"),

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();

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, ":="),
         }
     }
 }

src/parser.lalrpop

@@ -17,12 +17,16 @@ extern {
 
 		Ident => lexer::Token::Ident(<String>),
 
+		"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<T>: Vec<T> = { // (1)
+Multi<T>: Vec<T> = {
     <mut v:(<T> ",")*> <e:T> => {
 		v.push(e);
 		v
     }
 };
+MultiTr<T>: Vec<T> = {
+	<mut v:(<T> ",")*> <e:T> ","? => {
+		v.push(e);
+		v
+	}
+};
+
 
 pub Ast: Ast = {
 	Term => <>,
-	r"\" <args:Multi<IdentAndType>> "." <ast:Ast> => args.into_iter().rev().fold(ast, |ast, (i, t)| Ast::Abstraction(i, t, Box::new(ast))),
+	r"\" <args:Multi<IdentAndType>> "." <ast:Ast> => 
+		args.into_iter().rev().fold(ast, |ast, (i, t)| Ast::Abstraction(i, t, Box::new(ast))),
+	"let" <binds:MultiTr<LetBind>> "in" <ast:Ast> => 
+		binds.into_iter().rev().fold(ast, |ast, (i, t, b)| Ast::LetIn(i, t, Box::new(b), Box::new(ast))),
 };
 
-pub IdentAndType: (String, Option<TaggedType>) = <x:Ident> <t:(":" <TaggedType>)?> => (<>);
+IdentAndType: (String, Option<TaggedType>) = <x:Ident> <t:(":" <TaggedType>)?> => (<>);
+
+LetBind: (String, Option<TaggedType>, Ast) = <x:Ident> <t:(":" <TaggedType>)?> ":=" <a:Ast> => (<>);
 
 
 Term: Ast = {