From bea0783a17952521fbd7b27cbf2253d0ed5b780f Mon Sep 17 00:00:00 2001
From: Avery <avery@gitea.itycodes.org>
Date: Sat, 22 Mar 2025 14:12:06 +0100
Subject: [PATCH] Grammar updates
---
.gitignore | 1 +
grammar.ebnf | 32 +++++++++++++++++++++++
src/inference/test.rs | 4 +--
src/parse/test.rs | 60 +++++++++++++++++++++++++++++++++++++++++++
src/parse/tokenize.rs | 3 +++
src/parser.lalrpop | 14 ++++++++--
6 files changed, 110 insertions(+), 4 deletions(-)
create mode 100644 grammar.ebnf
diff --git a/.gitignore b/.gitignore
index ea8c4bf..97311d8 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,2 @@
/target
+grammar.html
diff --git a/grammar.ebnf b/grammar.ebnf
new file mode 100644
index 0000000..3e16d79
--- /dev/null
+++ b/grammar.ebnf
@@ -0,0 +1,32 @@
+(*
+
+
+
+
+
+
+
+
+ *)
+ast = term
+ | "\", {ident, [":", tagged type], ","}, ident, [":", tagged type], ".", ast ;
+
+term = ident
+ | constant
+ | "(", ast, ")"
+ | term, term ;
+
+constant = nat | float | bool ;
+
+tagged type = type tag, ident
+ | type tag, ident, "=>", tagged type
+ | type ;
+
+type tag = "Num" | "Any" ;
+
+type = basic type | arrow type ;
+
+basic type = "Nat" | "Float" | "Bool" | ident ;
+
+arrow type = "(", type, ")", "->", type
+ | basic type, "->", type ;
diff --git a/src/inference/test.rs b/src/inference/test.rs
index a96670a..5ab9260 100644
--- a/src/inference/test.rs
+++ b/src/inference/test.rs
@@ -172,8 +172,8 @@ fn infer_id_uni() {
typ,
TaggedType::Tagged(
TypeTag::Any,
- "?typ_1".to_string(),
- Box::new(TaggedType::Concrete(Type::arrow("?typ_1", "?typ_1")))
+ "?typ_0".to_string(),
+ Box::new(TaggedType::Concrete(Type::arrow("?typ_0", "?typ_0")))
)
);
}
diff --git a/src/parse/test.rs b/src/parse/test.rs
index 3b0bf9e..ae647b7 100644
--- a/src/parse/test.rs
+++ b/src/parse/test.rs
@@ -132,6 +132,66 @@ fn parse_abstraction() {
))
)
);
+
+ let ast = parser.parse(Lexer::new(r"\x:Any a.\y:Any b.x")).unwrap();
+ assert_eq!(
+ ast,
+ Ast::Abstraction(
+ "x".to_string(),
+ Some(TaggedType::Tagged(
+ TypeTag::Any,
+ "a".to_string(),
+ Box::new(TaggedType::Concrete("a".into()))
+ )),
+ Box::new(Ast::Abstraction(
+ "y".to_string(),
+ Some(TaggedType::Tagged(
+ TypeTag::Any,
+ "b".to_string(),
+ Box::new(TaggedType::Concrete("b".into()))
+ )),
+ Box::new(Ast::Variable("x".to_string()))
+ ))
+ )
+ );
+
+ let ast = parser
+ .parse(Lexer::new(r"\x:Any a => a,y:Any b => b.x"))
+ .unwrap();
+ assert_eq!(
+ ast,
+ Ast::Abstraction(
+ "x".to_string(),
+ Some(TaggedType::Tagged(
+ TypeTag::Any,
+ "a".to_string(),
+ Box::new(TaggedType::Concrete("a".into()))
+ )),
+ Box::new(Ast::Abstraction(
+ "y".to_string(),
+ Some(TaggedType::Tagged(
+ TypeTag::Any,
+ "b".to_string(),
+ Box::new(TaggedType::Concrete("b".into()))
+ )),
+ Box::new(Ast::Variable("x".to_string()))
+ ))
+ )
+ );
+
+ let ast = parser.parse(Lexer::new(r"\x,y.x")).unwrap();
+ assert_eq!(
+ ast,
+ Ast::Abstraction(
+ "x".to_string(),
+ None,
+ Box::new(Ast::Abstraction(
+ "y".to_string(),
+ None,
+ Box::new(Ast::Variable("x".to_string()))
+ ))
+ )
+ );
}
#[test]
diff --git a/src/parse/tokenize.rs b/src/parse/tokenize.rs
index 1c34b28..9e4dd41 100644
--- a/src/parse/tokenize.rs
+++ b/src/parse/tokenize.rs
@@ -51,6 +51,8 @@ pub enum Token {
Colon,
#[token(".")]
Period,
+ #[token(",")]
+ Comma,
#[token("=")]
Equals,
@@ -117,6 +119,7 @@ impl Display for Token {
Token::ThinArrow => write!(f, "->"),
Token::Colon => write!(f, ":"),
Token::Period => write!(f, "."),
+ Token::Comma => write!(f, ","),
Token::Equals => write!(f, "="),
Token::NotEquals => write!(f, "<>"),
Token::Plus => write!(f, "+"),
diff --git a/src/parser.lalrpop b/src/parser.lalrpop
index d3f370b..b443dee 100644
--- a/src/parser.lalrpop
+++ b/src/parser.lalrpop
@@ -22,6 +22,7 @@ extern {
"->" => lexer::Token::ThinArrow,
":" => lexer::Token::Colon,
"." => lexer::Token::Period,
+ "," => lexer::Token::Comma,
"=" => lexer::Token::Equals,
"<>" => lexer::Token::NotEquals,
@@ -43,12 +44,20 @@ extern {
}
+Multi<T>: Vec<T> = { // (1)
+ <mut v:(<T> ",")*> <e:T> => {
+ v.push(e);
+ v
+ }
+};
+
pub Ast: Ast = {
Term => <>,
- r"\" <x:Ident> ":" <t:TaggedType> "." <ast:Ast> => Ast::Abstraction(x, Some(t), Box::new(ast)),
- r"\" <x:Ident> "." <ast:Ast> => Ast::Abstraction(x, None, 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))),
};
+pub IdentAndType: (String, Option<TaggedType>) = <x:Ident> <t:(":" <TaggedType>)?> => (<>);
+
Term: Ast = {
#[precedence(level="0")]
@@ -68,6 +77,7 @@ Constant: Constant = {
};
pub TaggedType: TaggedType = {
+ <t:TypeTag> <i:Ident> => TaggedType::Tagged(t, i.clone(), Box::new(TaggedType::Concrete(Type::Variable(i)))),
<t:TypeTag> <i:Ident> "=>" <tt:TaggedType> => TaggedType::Tagged(t, i, Box::new(tt)),
<t:Type> => TaggedType::Concrete(t),
};