parent
32f8f7c29a
commit
305e95846d
GPG Key ID:
4E53F4CB69B2CC8D
@ -1,92 +0,0 @@
|
||||
use std::iter::Peekable;
|
||||
use std::ops::{Deref, RangeInclusive};
|
||||
use std::usize;
|
||||
use std::vec::IntoIter;
|
||||
|
||||
use super::ParseError;
|
||||
|
||||
#[derive(Debug, PartialEq, Clone)]
|
||||
pub enum Token {
|
||||
LeftParen,
|
||||
RightParen,
|
||||
Symbol(String),
|
||||
}
|
||||
|
||||
#[derive(Debug, PartialEq, Clone)]
|
||||
pub enum Sexpr {
|
||||
Symbol(String),
|
||||
List(Vec<Sexpr>),
|
||||
}
|
||||
|
||||
impl Sexpr {
|
||||
pub fn symbol(self) -> Option<String> {
|
||||
match self {
|
||||
Sexpr::Symbol(item) => Some(item),
|
||||
_ => None,
|
||||
}
|
||||
}
|
||||
|
||||
pub fn list(self) -> Option<Vec<Sexpr>> {
|
||||
match self {
|
||||
Sexpr::List(item) => Some(item),
|
||||
_ => None,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn tokenize(input: &str) -> Vec<Token> {
|
||||
let mut tokens = Vec::new();
|
||||
// let mut chars = input.chars().peekable();
|
||||
let mut chars = input.chars().peekable();
|
||||
while let Some(c) = chars.next() {
|
||||
match c {
|
||||
'(' => tokens.push(Token::LeftParen),
|
||||
')' => tokens.push(Token::RightParen),
|
||||
_ if c.is_whitespace() => (),
|
||||
_ => {
|
||||
let mut symbol = c.to_string();
|
||||
while let Some(c) = chars.peek() {
|
||||
if c.is_whitespace() || *c == '(' || *c == ')' {
|
||||
break;
|
||||
}
|
||||
symbol.push(*c);
|
||||
chars.next();
|
||||
}
|
||||
tokens.push(Token::Symbol(symbol));
|
||||
}
|
||||
}
|
||||
}
|
||||
tokens
|
||||
}
|
||||
|
||||
fn parse_expr(tokens: &mut Peekable<IntoIter<Token>>) -> Result<Sexpr, ParseError> {
|
||||
match tokens.next() {
|
||||
Some(Token::LeftParen) => {
|
||||
let mut list = Vec::new();
|
||||
while !matches!(tokens.peek(), Some(Token::RightParen,)) {
|
||||
list.push(parse_expr(tokens)?);
|
||||
}
|
||||
let Some(Token::RightParen) = tokens.next() else {
|
||||
unreachable!()
|
||||
};
|
||||
Ok(Sexpr::List(list))
|
||||
}
|
||||
Some(Token::RightParen) => Err(ParseError::UnexpectedParenClose),
|
||||
Some(Token::Symbol(s)) => Ok(Sexpr::Symbol(s)),
|
||||
None => Err(ParseError::UnexpectedEof),
|
||||
}
|
||||
}
|
||||
|
||||
fn parse(tokens: Vec<Token>) -> Result<Sexpr, ParseError> {
|
||||
let mut tokens = tokens.into_iter().peekable();
|
||||
let ast = parse_expr(&mut tokens)?;
|
||||
if tokens.peek().is_some() {
|
||||
return Err(ParseError::TrailingTokens);
|
||||
};
|
||||
Ok(ast)
|
||||
}
|
||||
|
||||
pub fn parse_string(src: &str) -> Result<Sexpr, ParseError> {
|
||||
let tokens = tokenize(src);
|
||||
parse(tokens)
|
||||
}
|
||||
@ -1,96 +1,254 @@
|
||||
use crate::{
|
||||
PrimitiveType, Type,
|
||||
parse::{
|
||||
Ast, Constant,
|
||||
sexpr::{Sexpr, parse_string},
|
||||
tokenize::{self, Lexer},
|
||||
},
|
||||
types::{PrimitiveType, TaggedType, Type, TypeTag},
|
||||
};
|
||||
|
||||
use super::{parse, parse_type};
|
||||
use super::parser;
|
||||
|
||||
#[test]
|
||||
fn parse_to_sexpr() {
|
||||
let input = "((\\x:Nat.x) (5))";
|
||||
let parsed = parse_string(input).unwrap();
|
||||
assert_eq!(
|
||||
parsed,
|
||||
Sexpr::List(vec![
|
||||
Sexpr::List(vec![Sexpr::Symbol("\\x:Nat.x".to_string())]),
|
||||
Sexpr::List(vec![Sexpr::Symbol("5".to_string())])
|
||||
])
|
||||
);
|
||||
}
|
||||
fn parse_constant() {
|
||||
let parser = parser::AstParser::new();
|
||||
let ast = parser.parse(Lexer::new("5")).unwrap();
|
||||
assert_eq!(ast, Ast::Constant(Constant::Nat(5)));
|
||||
|
||||
#[test]
|
||||
fn parse_prim_type() {
|
||||
let input = Sexpr::Symbol("Nat".to_string());
|
||||
let parsed = parse_type(&input).unwrap();
|
||||
assert_eq!(parsed, Type::Primitive(PrimitiveType::Nat))
|
||||
let ast = parser.parse(Lexer::new("3.14")).unwrap();
|
||||
assert_eq!(ast, Ast::Constant(Constant::Float(3.14)));
|
||||
|
||||
let ast = parser.parse(Lexer::new("true")).unwrap();
|
||||
assert_eq!(ast, Ast::Constant(Constant::Bool(true)));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_simpl_arr_type() {
|
||||
let input = Sexpr::List(vec![
|
||||
Sexpr::Symbol("Nat".to_string()),
|
||||
Sexpr::Symbol("->".to_string()),
|
||||
Sexpr::Symbol("Nat".to_string()),
|
||||
]);
|
||||
let parsed = parse_type(&input).unwrap();
|
||||
assert_eq!(parsed, Type::arrow(PrimitiveType::Nat, PrimitiveType::Nat))
|
||||
fn parse_variable() {
|
||||
let parser = parser::AstParser::new();
|
||||
let ast = parser.parse(Lexer::new("x")).unwrap();
|
||||
assert_eq!(ast, Ast::Variable("x".to_string()));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_apply_arr_type() {
|
||||
let input = Sexpr::List(vec![
|
||||
Sexpr::List(vec![
|
||||
Sexpr::Symbol("Nat".to_string()),
|
||||
Sexpr::Symbol("->".to_string()),
|
||||
Sexpr::Symbol("Nat".to_string()),
|
||||
]),
|
||||
Sexpr::Symbol("->".to_string()),
|
||||
Sexpr::Symbol("Nat".to_string()),
|
||||
Sexpr::Symbol("->".to_string()),
|
||||
Sexpr::Symbol("Nat".to_string()),
|
||||
]);
|
||||
let parsed = parse_type(&input).unwrap();
|
||||
fn parse_type() {
|
||||
let parser = parser::TaggedTypeParser::new();
|
||||
let ast = parser.parse(Lexer::new("Num a => a -> a -> a")).unwrap();
|
||||
assert_eq!(
|
||||
ast,
|
||||
TaggedType::Tagged(
|
||||
TypeTag::Num,
|
||||
"a".to_string(),
|
||||
Box::new(TaggedType::Concrete(Type::arrow(
|
||||
"a",
|
||||
Type::arrow("a", "a")
|
||||
)))
|
||||
)
|
||||
);
|
||||
|
||||
let ast = parser
|
||||
.parse(Lexer::new("Any a => (a -> a) -> a -> a"))
|
||||
.unwrap();
|
||||
assert_eq!(
|
||||
parsed,
|
||||
Type::arrow(
|
||||
Type::arrow(PrimitiveType::Nat, PrimitiveType::Nat),
|
||||
Type::arrow(PrimitiveType::Nat, PrimitiveType::Nat)
|
||||
ast,
|
||||
TaggedType::Tagged(
|
||||
TypeTag::Any,
|
||||
"a".to_string(),
|
||||
Box::new(TaggedType::Concrete(Type::arrow(
|
||||
Type::arrow("a", "a"),
|
||||
Type::arrow("a", "a")
|
||||
)))
|
||||
)
|
||||
)
|
||||
);
|
||||
|
||||
let ast = parser
|
||||
.parse(Lexer::new("Any a => Any b => (a -> b) -> a -> b"))
|
||||
.unwrap();
|
||||
assert_eq!(
|
||||
ast,
|
||||
TaggedType::Tagged(
|
||||
TypeTag::Any,
|
||||
"a".to_string(),
|
||||
Box::new(TaggedType::Tagged(
|
||||
TypeTag::Any,
|
||||
"b".to_string(),
|
||||
Box::new(TaggedType::Concrete(Type::arrow(
|
||||
Type::arrow("a", "b"),
|
||||
Type::arrow("a", "b")
|
||||
)))
|
||||
))
|
||||
)
|
||||
);
|
||||
|
||||
let ast = parser.parse(Lexer::new("Nat -> Nat")).unwrap();
|
||||
assert_eq!(
|
||||
ast,
|
||||
TaggedType::Concrete(Type::arrow(PrimitiveType::Nat, PrimitiveType::Nat))
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_abstraction() {
|
||||
let input = "(\\ (x (Nat -> Nat)) (x 5))";
|
||||
let parsed = parse(input).unwrap();
|
||||
let parser = parser::AstParser::new();
|
||||
let ast = parser.parse(Lexer::new(r"\x:Nat.x")).unwrap();
|
||||
assert_eq!(
|
||||
parsed,
|
||||
ast,
|
||||
Ast::Abstraction(
|
||||
"x".to_string(),
|
||||
Type::arrow(PrimitiveType::Nat, PrimitiveType::Nat),
|
||||
Box::new(Ast::Application(
|
||||
Box::new(Ast::Variable("x".to_string())),
|
||||
Box::new(Ast::Constant(Constant::Nat(5)))
|
||||
Type::Primitive(PrimitiveType::Nat).into(),
|
||||
Box::new(Ast::Variable("x".to_string()))
|
||||
)
|
||||
);
|
||||
|
||||
let ast = parser.parse(Lexer::new(r"\x:Nat.\y:Nat.x")).unwrap();
|
||||
assert_eq!(
|
||||
ast,
|
||||
Ast::Abstraction(
|
||||
"x".to_string(),
|
||||
Type::Primitive(PrimitiveType::Nat).into(),
|
||||
Box::new(Ast::Abstraction(
|
||||
"y".to_string(),
|
||||
Type::Primitive(PrimitiveType::Nat).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(),
|
||||
TaggedType::Tagged(
|
||||
TypeTag::Any,
|
||||
"a".to_string(),
|
||||
Box::new(TaggedType::Concrete("a".into()))
|
||||
),
|
||||
Box::new(Ast::Abstraction(
|
||||
"y".to_string(),
|
||||
TaggedType::Tagged(
|
||||
TypeTag::Any,
|
||||
"b".to_string(),
|
||||
Box::new(TaggedType::Concrete("b".into()))
|
||||
),
|
||||
Box::new(Ast::Variable("x".to_string()))
|
||||
))
|
||||
)
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_application() {
|
||||
let input = "((add 5) 6)";
|
||||
let parsed = parse(input).unwrap();
|
||||
let parser = parser::AstParser::new();
|
||||
let ast = parser.parse(Lexer::new(r"(\x:Nat.x) 5")).unwrap();
|
||||
assert_eq!(
|
||||
parsed,
|
||||
ast,
|
||||
Ast::Application(
|
||||
Box::new(Ast::Abstraction(
|
||||
"x".to_string(),
|
||||
Type::Primitive(PrimitiveType::Nat).into(),
|
||||
Box::new(Ast::Variable("x".to_string()))
|
||||
)),
|
||||
Box::new(Ast::Constant(Constant::Nat(5)))
|
||||
)
|
||||
);
|
||||
|
||||
let ast = parser.parse(Lexer::new(r"add 1")).unwrap();
|
||||
assert_eq!(
|
||||
ast,
|
||||
Ast::Application(
|
||||
Box::new(Ast::Variable("add".to_string())),
|
||||
Box::new(Ast::Constant(Constant::Nat(1)))
|
||||
),
|
||||
);
|
||||
|
||||
let ast = parser.parse(Lexer::new(r"(add 1) 2")).unwrap();
|
||||
assert_eq!(
|
||||
ast,
|
||||
Ast::Application(
|
||||
Box::new(Ast::Application(
|
||||
Box::new(Ast::Variable("add".to_string())),
|
||||
Box::new(Ast::Constant(Constant::Nat(1)))
|
||||
)),
|
||||
Box::new(Ast::Constant(Constant::Nat(2)))
|
||||
),
|
||||
);
|
||||
|
||||
let ast = parser.parse(Lexer::new(r"add 1 2")).unwrap();
|
||||
assert_eq!(
|
||||
ast,
|
||||
Ast::Application(
|
||||
Box::new(Ast::Application(
|
||||
Box::new(Ast::Variable("add".to_string())),
|
||||
Box::new(Ast::Constant(Constant::Nat(1)))
|
||||
)),
|
||||
Box::new(Ast::Constant(Constant::Nat(2)))
|
||||
),
|
||||
);
|
||||
|
||||
let ast = parser.parse(Lexer::new(r"add 1 (x y)")).unwrap();
|
||||
assert_eq!(
|
||||
ast,
|
||||
Ast::Application(
|
||||
Box::new(Ast::Application(
|
||||
Box::new(Ast::Variable("add".to_string())),
|
||||
Box::new(Ast::Constant(Constant::Nat(5)))
|
||||
Box::new(Ast::Constant(Constant::Nat(1)))
|
||||
)),
|
||||
Box::new(Ast::Application(
|
||||
Box::new(Ast::Variable("x".to_string())),
|
||||
Box::new(Ast::Variable("y".to_string())),
|
||||
)),
|
||||
Box::new(Ast::Constant(Constant::Nat(6)))
|
||||
),
|
||||
);
|
||||
|
||||
let ast = parser
|
||||
.parse(Lexer::new(
|
||||
r"(\x:Any a => a -> a.\y:Num a => a. add 1 (x y)) (\x:Any a => a.x) 2",
|
||||
))
|
||||
.unwrap();
|
||||
assert_eq!(
|
||||
ast,
|
||||
Ast::Application(
|
||||
Box::new(Ast::Application(
|
||||
Box::new(Ast::Abstraction(
|
||||
"x".to_string(),
|
||||
TaggedType::Tagged(
|
||||
TypeTag::Any,
|
||||
"a".to_string(),
|
||||
Box::new(TaggedType::Concrete(Type::arrow("a", "a")))
|
||||
),
|
||||
Box::new(Ast::Abstraction(
|
||||
"y".to_string(),
|
||||
TaggedType::Tagged(
|
||||
TypeTag::Num,
|
||||
"a".to_string(),
|
||||
Box::new(TaggedType::Concrete("a".into()))
|
||||
),
|
||||
Box::new(Ast::Application(
|
||||
Box::new(Ast::Application(
|
||||
Box::new(Ast::Variable("add".to_string())),
|
||||
Box::new(Ast::Constant(Constant::Nat(1)))
|
||||
)),
|
||||
Box::new(Ast::Application(
|
||||
Box::new(Ast::Variable("x".to_string())),
|
||||
Box::new(Ast::Variable("y".to_string())),
|
||||
))
|
||||
))
|
||||
)),
|
||||
)),
|
||||
Box::new(Ast::Abstraction(
|
||||
"x".to_string(),
|
||||
TaggedType::Tagged(
|
||||
TypeTag::Any,
|
||||
"a".to_string(),
|
||||
Box::new(TaggedType::Concrete("a".into()))
|
||||
),
|
||||
Box::new(Ast::Variable("x".to_string()))
|
||||
))
|
||||
)),
|
||||
Box::new(Ast::Constant(Constant::Nat(2)))
|
||||
)
|
||||
)
|
||||
);
|
||||
}
|
||||
|
||||
// (\x:Any a => a -> a.\y:Num a => a. + 1 (x y)) (\x:Any a => a.x) 2
|
||||
|
||||
@ -0,0 +1,141 @@
|
||||
use std::{
|
||||
fmt::{self, Display, Formatter},
|
||||
num::{ParseFloatError, ParseIntError},
|
||||
str::ParseBoolError,
|
||||
};
|
||||
|
||||
use logos::{Logos, SpannedIter};
|
||||
|
||||
use super::ParseError;
|
||||
|
||||
impl From<ParseIntError> for ParseError {
|
||||
fn from(err: ParseIntError) -> Self {
|
||||
Self::InvalidInteger(err)
|
||||
}
|
||||
}
|
||||
|
||||
impl From<ParseFloatError> for ParseError {
|
||||
fn from(err: ParseFloatError) -> Self {
|
||||
Self::InvalidFloat(err)
|
||||
}
|
||||
}
|
||||
|
||||
impl From<ParseBoolError> for ParseError {
|
||||
fn from(err: ParseBoolError) -> Self {
|
||||
Self::InvalidBool(err)
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Logos, Debug, Clone)]
|
||||
#[logos(skip r"[ \t\n\r\f]+", error = ParseError)]
|
||||
pub enum Token {
|
||||
// #[regex(r#""([^\"\\]|\\.)*""#, |lex| {let slice = lex.slice(); slice[1..slice.len() - 1].to_string()})]
|
||||
// String(String),
|
||||
#[regex(r#"\d+"#, |lex| lex.slice().parse::<usize>())]
|
||||
Nat(usize),
|
||||
#[regex(r#"-?\d+\.\d+"#, |lex| lex.slice().parse::<f64>())]
|
||||
Float(f64),
|
||||
#[regex(r#"(true|false)"#, |lex| lex.slice().parse::<bool>())]
|
||||
Bool(bool),
|
||||
|
||||
#[regex(r#"[_a-zA-Z][_a-zA-Z0-9]*'*"#, |lex| lex.slice().to_string())]
|
||||
Ident(String),
|
||||
|
||||
#[token(r"\")]
|
||||
Lambda,
|
||||
#[token("=>")]
|
||||
FatArrow,
|
||||
#[token("->")]
|
||||
ThinArrow,
|
||||
#[token(":")]
|
||||
Colon,
|
||||
#[token(".")]
|
||||
Period,
|
||||
|
||||
#[token("=")]
|
||||
Equals,
|
||||
#[token("<>")]
|
||||
NotEquals,
|
||||
#[token("+")]
|
||||
Plus,
|
||||
#[token("-")]
|
||||
Minus,
|
||||
#[token("*")]
|
||||
Star,
|
||||
#[token("/")]
|
||||
Slash,
|
||||
#[token("^")]
|
||||
Hat,
|
||||
#[token("<")]
|
||||
Less,
|
||||
#[token(">")]
|
||||
Greater,
|
||||
#[token("<=")]
|
||||
LessEq,
|
||||
#[token(">=")]
|
||||
GreaterEq,
|
||||
#[token(r"/\")]
|
||||
Conjunction,
|
||||
#[token(r"\/")]
|
||||
Disjunction,
|
||||
|
||||
#[token("(")]
|
||||
ParenOpen,
|
||||
#[token(")")]
|
||||
ParenClose,
|
||||
}
|
||||
|
||||
pub type Spanned<Tok, Loc, Error> = Result<(Loc, Tok, Loc), Error>;
|
||||
|
||||
pub struct Lexer<'input> {
|
||||
// instead of an iterator over characters, we have a token iterator
|
||||
token_stream: SpannedIter<'input, Token>,
|
||||
}
|
||||
impl<'input> Lexer<'input> {
|
||||
pub fn new(input: &'input str) -> Self {
|
||||
// the Token::lexer() method is provided by the Logos trait
|
||||
Self {
|
||||
token_stream: Token::lexer(input).spanned(),
|
||||
}
|
||||
}
|
||||
}
|
||||
impl<'input> Iterator for Lexer<'input> {
|
||||
type Item = Spanned<Token, usize, ParseError>;
|
||||
|
||||
fn next(&mut self) -> Option<Self::Item> {
|
||||
self.token_stream
|
||||
.next()
|
||||
.map(|(token, span)| Ok((span.start, token?, span.end)))
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for Token {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
|
||||
match self {
|
||||
Token::Lambda => write!(f, r"\"),
|
||||
Token::FatArrow => write!(f, "=>"),
|
||||
Token::ThinArrow => write!(f, "->"),
|
||||
Token::Colon => write!(f, ":"),
|
||||
Token::Period => write!(f, "."),
|
||||
Token::Equals => write!(f, "="),
|
||||
Token::NotEquals => write!(f, "<>"),
|
||||
Token::Plus => write!(f, "+"),
|
||||
Token::Minus => write!(f, "-"),
|
||||
Token::Star => write!(f, "*"),
|
||||
Token::Slash => write!(f, "/"),
|
||||
Token::Hat => write!(f, "^"),
|
||||
Token::Less => write!(f, "<"),
|
||||
Token::Greater => write!(f, ">"),
|
||||
Token::LessEq => write!(f, "<="),
|
||||
Token::GreaterEq => write!(f, ">="),
|
||||
Token::Conjunction => write!(f, r"/\"),
|
||||
Token::Disjunction => write!(f, r"\/"),
|
||||
Token::ParenOpen => write!(f, "("),
|
||||
Token::ParenClose => write!(f, ")"),
|
||||
Token::Nat(n) => write!(f, "{n}"),
|
||||
Token::Float(n) => write!(f, "{n}"),
|
||||
Token::Bool(b) => write!(f, "{b}"),
|
||||
Token::Ident(i) => write!(f, "{i}"),
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,86 @@
|
||||
use crate::{
|
||||
parse::{Ast, Constant, tokenize as lexer, ParseError as PError},
|
||||
types::{TaggedType, TypeTag, Type, PrimitiveType},
|
||||
};
|
||||
use lalrpop_util::ParseError;
|
||||
|
||||
grammar;
|
||||
|
||||
extern {
|
||||
type Location = usize;
|
||||
type Error = PError;
|
||||
|
||||
enum lexer::Token {
|
||||
Nat => lexer::Token::Nat(<usize>),
|
||||
Float => lexer::Token::Float(<f64>),
|
||||
Bool => lexer::Token::Bool(<bool>),
|
||||
|
||||
Ident => lexer::Token::Ident(<String>),
|
||||
|
||||
r"\" => lexer::Token::Lambda,
|
||||
"=>" => lexer::Token::FatArrow,
|
||||
"->" => lexer::Token::ThinArrow,
|
||||
":" => lexer::Token::Colon,
|
||||
"." => lexer::Token::Period,
|
||||
|
||||
"=" => lexer::Token::Equals,
|
||||
"<>" => lexer::Token::NotEquals,
|
||||
"+" => lexer::Token::Plus,
|
||||
"-" => lexer::Token::Minus,
|
||||
"*" => lexer::Token::Star,
|
||||
"/" => lexer::Token::Slash,
|
||||
"^" => lexer::Token::Hat,
|
||||
"<" => lexer::Token::Less,
|
||||
">" => lexer::Token::Greater,
|
||||
"<=" => lexer::Token::LessEq,
|
||||
">=" => lexer::Token::GreaterEq,
|
||||
r"/\" => lexer::Token::Conjunction,
|
||||
r"\/" => lexer::Token::Disjunction,
|
||||
|
||||
"(" => lexer::Token::ParenOpen,
|
||||
")" => lexer::Token::ParenClose,
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
pub Ast: Ast = {
|
||||
Term => <>,
|
||||
r"\" <x:Ident> ":" <t:TaggedType> "." <ast:Ast> => Ast::Abstraction(x, t, Box::new(ast)),
|
||||
};
|
||||
|
||||
|
||||
Term: Ast = {
|
||||
#[precedence(level="0")]
|
||||
Ident => Ast::Variable(<>),
|
||||
#[precedence(level="0")]
|
||||
Constant => Ast::Constant(<>),
|
||||
#[precedence(level="1")]
|
||||
"(" <Ast> ")" => <>,
|
||||
#[precedence(level="2")] #[assoc(side = "left")]
|
||||
<lhs:Term> <rhs:Term> => Ast::Application(Box::new(lhs), Box::new(rhs)),
|
||||
};
|
||||
|
||||
Constant: Constant = {
|
||||
Nat => Constant::Nat(<>),
|
||||
Float => Constant::Float(<>),
|
||||
Bool => Constant::Bool(<>),
|
||||
};
|
||||
|
||||
pub TaggedType: TaggedType = {
|
||||
<t:TypeTag> <i:Ident> "=>" <tt:TaggedType> => TaggedType::Tagged(t, i, Box::new(tt)),
|
||||
<t:Type> => TaggedType::Concrete(t),
|
||||
};
|
||||
|
||||
TypeTag: TypeTag = Ident =>? TypeTag::try_from(<>).map_err(|e| ParseError::User{ error: e });
|
||||
|
||||
Type: Type = { BasicType, ArrowType };
|
||||
|
||||
BasicType: Type = Ident => Type::from_name(<>);
|
||||
|
||||
ArrowType: Type = {
|
||||
#[precedence(level="0")]
|
||||
"(" <l:Type> ")" "->" <r:Type> => Type::Arrow(Box::new(l), Box::new(r)),
|
||||
#[precedence(level="1")] #[assoc(side = "right")]
|
||||
<l:BasicType> "->" <r:Type> => Type::Arrow(Box::new(l), Box::new(r)),
|
||||
};
|
||||
|
||||
Loading…
Reference in new issue