From fe4cb4834290c249d4c5f73b0a8f21e2b32abb9b Mon Sep 17 00:00:00 2001
From: aalbert <augustin.albert@bleu-azure.fr>
Date: Mon, 17 Oct 2022 19:16:49 +0200
Subject: [PATCH] =?UTF-8?q?feat(parser):=20Add=20new=20syntaxic=20sugar=20?=
=?UTF-8?q?and=20meaningfull=20error=20messages,=20add=20more...=20?=
=?UTF-8?q?=E2=9C=A8=EF=B8=8F=20Closes=20#10=20=F0=9F=90=94=EF=B8=8F?=
=?UTF-8?q?=F0=9F=91=8D=EF=B8=8F=20Approved-by:=20v-lafeychine=20<vincent.?=
=?UTF-8?q?lafeychine@proton.me>=20Approved-by:=20aalbert=20<augustin.albe?=
=?UTF-8?q?rt@bleu-azure.fr>=20Approved-by:=20loutr=20<loutr@crans.org>?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
🦀ï¸ðŸ°ðŸ¦€ï¸ðŸ°ðŸ¦€ï¸ðŸ°
* fix(parser): Fix the semantics of products without parentheses.
* chore(parser): renaming
* chore(parser & proost): renaming
* feat(parser): documentation
* fix(parser): resolve threads
* feat(parser): Add new syntaxic sugar and meaningfull error messages, add more efficient conversion into terms (VecDeque), remove unused struct ClassicTerm, remove useless & outdated test.
feat(kernel): Add new command: DefineCheckType. eg: "def x:P := P"
feat(proost): Process multiples commands in one line
* feat(parser): Add new syntaxic sugar and meaningfull error messages, add more efficient conversion into terms (VecDeque), remove unused struct ClassicTerm, remove useless & outdated test.
feat(kernel): Add new command: DefineCheckType. eg: "def x:P := P"
feat(proost): Process multiples commands in one line
---
kernel/src/command.rs | 3 +
parser/src/classic_term.pest | 20 ----
parser/src/classic_term.rs | 65 -------------
parser/src/lib.rs | 7 +-
parser/src/parser.rs | 175 ++++++++++++++++++++---------------
parser/src/term.pest | 40 ++++++++
parser/tests/example.mdln | 4 -
parser/tests/example.rs | 12 ---
proost/src/main.rs | 15 ++-
9 files changed, 159 insertions(+), 182 deletions(-)
delete mode 100644 parser/src/classic_term.pest
delete mode 100644 parser/src/classic_term.rs
create mode 100644 parser/src/term.pest
delete mode 100644 parser/tests/example.mdln
delete mode 100644 parser/tests/example.rs
diff --git a/kernel/src/command.rs b/kernel/src/command.rs
index 486b44ac..d8d3afff 100644
--- a/kernel/src/command.rs
+++ b/kernel/src/command.rs
@@ -11,4 +11,7 @@ pub enum Command {
#[display(fmt = "Type {}.", _0)]
GetType(Term),
+
+ #[display(fmt = "Define {} : {} := {}.", _0, _1, _2)]
+ DefineCheckType(String, Term, Term),
}
diff --git a/parser/src/classic_term.pest b/parser/src/classic_term.pest
deleted file mode 100644
index 9679f523..00000000
--- a/parser/src/classic_term.pest
+++ /dev/null
@@ -1,20 +0,0 @@
-WHITESPACE = _{ " " | "\t" }
-COMMENT = _{ "#" ~ (!"\n" ~ ANY)* }
-number = @{ ASCII_NONZERO_DIGIT ~ ASCII_DIGIT* }
-string = @{ ASCII_ALPHA ~ ASCII_ALPHANUMERIC* }
-
-Term = _{ Prop | Type | Var | App | Abs | Prod | ParTerm }
-Prop = { "P" }
-Type = { "T(" ~ number ~ ")" }
-Var = { string }
-App = { "(" ~ ( Var | Abs | Prod ) ~ ")" ~ Term }
-Abs = { "/\\" ~ string ~ ":" ~ Term ~ "->" ~ Term }
-Prod = { "\\/" ~ string ~ ":" ~ Term ~ "->" ~ Term }
-ParTerm = _{ "(" ~ Term ~ ")" }
-
-Command = _{ ( Define | CheckType | GetType ) ~ "." }
-Define = { ( "define" | "Define" ) ~ string ~ ":=" ~ Term }
-CheckType = { ( "CheckType" | "Check" | "check" ) ~ Term ~ ":" ~ Term }
-GetType = { ( "Type" | "GetType" | "type" ) ~ Term }
-
-File = { SOI ~ (NEWLINE* ~ Command)* ~ NEWLINE* ~ EOI }
diff --git a/parser/src/classic_term.rs b/parser/src/classic_term.rs
deleted file mode 100644
index 658e8c05..00000000
--- a/parser/src/classic_term.rs
+++ /dev/null
@@ -1,65 +0,0 @@
-use kernel::derive_more::Display;
-use kernel::num_bigint::BigUint;
-use kernel::Term;
-
-#[derive(Clone, Debug, Display)]
-pub enum ClassicTerm {
- #[display(fmt = "{}", _0)]
- Var(String),
-
- #[display(fmt = "\u{02119}")]
- Prop,
-
- #[display(fmt = "Type({})", _0)]
- Type(BigUint),
-
- #[display(fmt = "({} {})", _0, _1)]
- App(Box<ClassicTerm>, Box<ClassicTerm>),
-
- #[display(fmt = "\u{003BB}{} \u{02192} {}", _0, _1)]
- Abs(String, Box<ClassicTerm>, Box<ClassicTerm>),
-
- #[display(fmt = "\u{02200}{} \u{02192} {}", _0, _1)]
- Prod(String, Box<ClassicTerm>, Box<ClassicTerm>),
-}
-
-fn try_from_assign(term: ClassicTerm, known_ids: &mut Vec<String>) -> Result<Term, String> {
- match term {
- ClassicTerm::Prop => Ok(Term::Prop),
- ClassicTerm::Type(i) => Ok(Term::Type(i.into())),
- ClassicTerm::App(t1, t2) => {
- let t1 = box try_from_assign(*t1, known_ids)?;
- let t2 = box try_from_assign(*t2, known_ids)?;
-
- Ok(Term::App(t1, t2))
- }
- ClassicTerm::Var(s) => match known_ids.iter().rev().position(|r| *r == s) {
- Some(i) => Ok(Term::Var((i + 1).into())),
- None => Err(s),
- },
- ClassicTerm::Abs(s, t1, t2) => {
- known_ids.push(s);
- let t1 = box try_from_assign(*t1, known_ids)?;
- let t2 = box try_from_assign(*t2, known_ids)?;
- known_ids.pop();
-
- Ok(Term::Abs(t1, t2))
- }
- ClassicTerm::Prod(s, t1, t2) => {
- known_ids.push(s);
- let t1 = box try_from_assign(*t1, known_ids)?;
- let t2 = box try_from_assign(*t2, known_ids)?;
- known_ids.pop();
-
- Ok(Term::Prod(t1, t2))
- }
- }
-}
-
-impl TryFrom<ClassicTerm> for Term {
- type Error = String;
-
- fn try_from(t: ClassicTerm) -> Result<Self, Self::Error> {
- try_from_assign(t, &mut Vec::new())
- }
-}
diff --git a/parser/src/lib.rs b/parser/src/lib.rs
index 664c084b..20c7f747 100644
--- a/parser/src/lib.rs
+++ b/parser/src/lib.rs
@@ -1,9 +1,12 @@
+//! Fast parser for λ-terms and commands using pest.
+//!
+//! Provides the function `parse_commands` to parse both files and single commands.
+
#![feature(box_syntax)]
#[macro_use]
extern crate pest_derive;
-mod classic_term;
mod parser;
-pub use self::parser::{parse_command, parse_file, parse_term};
+pub use self::parser::parse_commands;
diff --git a/parser/src/parser.rs b/parser/src/parser.rs
index d23ace61..7db5ede1 100644
--- a/parser/src/parser.rs
+++ b/parser/src/parser.rs
@@ -1,112 +1,139 @@
-use crate::classic_term::ClassicTerm;
+use kernel::num_bigint::BigUint;
use kernel::{Command, Term};
use pest::error::{Error, ErrorVariant};
use pest::iterators::Pair;
-use pest::{Parser, Position};
+use pest::Parser;
+use std::collections::VecDeque;
#[derive(Parser)]
-#[grammar = "classic_term.pest"]
+#[grammar = "term.pest"]
struct CommandParser;
-fn build_classic_term_from_expr(pair: Pair<Rule>) -> ClassicTerm {
+fn build_term_from_expr(
+ pair: Pair<Rule>,
+ known_vars: &mut VecDeque<String>,
+ //defined_vars: issue #18 TODO use a hash map of known variables
+) -> Result<Term, Box<Error<Rule>>> {
match pair.as_rule() {
- Rule::Prop => ClassicTerm::Prop,
- Rule::Var => ClassicTerm::Var(pair.into_inner().as_str().to_string()),
- Rule::Type => ClassicTerm::Type(pair.into_inner().as_str().parse().unwrap()),
+ Rule::Prop => Ok(Term::Prop),
+ Rule::Type => Ok(Term::Type(
+ pair.into_inner()
+ .as_str()
+ .parse::<BigUint>()
+ .unwrap()
+ .into(),
+ )),
+
+ Rule::Var => {
+ //issue #18 TODO use a hash map of known variables
+ let span = pair.as_span();
+ let name = pair.into_inner().as_str().to_string();
+ match known_vars.iter().position(|x| *x == name) {
+ Some(i) => Ok(Term::Var((i + 1).into())),
+ None => Err(box Error::new_from_span(
+ ErrorVariant::CustomError {
+ message: String::from("free variable: ") + &name,
+ },
+ span,
+ )),
+ }
+ }
+ Rule::Prod => {
+ let mut iter = pair
+ .into_inner()
+ .map(|x| build_term_from_expr(x, known_vars))
+ .rev();
+ let t = iter.next().unwrap()?;
+ iter.try_fold(t, |acc, x| Ok(Term::Prod(box x?, box acc)))
+ }
Rule::App => {
- let mut iter = pair.into_inner();
- let t1 = build_classic_term_from_expr(iter.next().unwrap());
- let t2 = build_classic_term_from_expr(iter.next().unwrap());
- ClassicTerm::App(box t1, box t2)
+ let mut iter = pair
+ .into_inner()
+ .map(|x| build_term_from_expr(x, known_vars));
+ let t = iter.next().unwrap()?;
+ iter.try_fold(t, |acc, x| Ok(Term::App(box acc, box x?)))
}
Rule::Abs => {
- let mut iter = pair.into_inner();
- let s = iter.next().unwrap().as_str().to_string();
- let t1 = build_classic_term_from_expr(iter.next().unwrap());
- let t2 = build_classic_term_from_expr(iter.next().unwrap());
- ClassicTerm::Abs(s, box t1, box t2)
+ let iter = pair.into_inner();
+ let mut iter2 = iter.clone().rev();
+ for pair in iter {
+ if pair.as_rule() == Rule::arg_abs {
+ let name = pair.into_inner().next().unwrap().as_str().to_string();
+ known_vars.push_front(name);
+ }
+ }
+ let t = build_term_from_expr(iter2.next().unwrap(), known_vars)?;
+ iter2.try_fold(t, |acc, x| {
+ known_vars.pop_front();
+ let mut iter3 = x.into_inner();
+ iter3.next();
+ let t = build_term_from_expr(iter3.next().unwrap(), known_vars)?;
+ Ok(Term::Abs(box t, box acc))
+ })
}
- Rule::Prod => {
- let mut iter = pair.into_inner();
- let s = iter.next().unwrap().as_str().to_string();
- let t1 = build_classic_term_from_expr(iter.next().unwrap());
- let t2 = build_classic_term_from_expr(iter.next().unwrap());
- ClassicTerm::Prod(s, box t1, box t2)
+ Rule::dProd => {
+ let iter = pair.into_inner();
+ let mut iter2 = iter.clone().rev();
+ for pair in iter {
+ if pair.as_rule() == Rule::arg_dprod {
+ let name = pair.into_inner().next().unwrap().as_str().to_string();
+ known_vars.push_front(name);
+ }
+ }
+ let t = build_term_from_expr(iter2.next().unwrap(), known_vars)?;
+ iter2.try_fold(t, |acc, x| {
+ known_vars.pop_front();
+ let mut iter3 = x.into_inner();
+ iter3.next();
+ let t = build_term_from_expr(iter3.next().unwrap(), known_vars)?;
+ Ok(Term::Prod(box t, box acc))
+ })
}
term => panic!("Unexpected term: {:?}", term),
}
}
-fn build_term_from_expr(pair: Pair<Rule>) -> Result<Term, String> {
- Term::try_from(build_classic_term_from_expr(pair))
-}
-
-fn build_command_from_expr(pair: Pair<Rule>) -> Result<Command, String> {
+fn build_command_from_expr(pair: Pair<Rule>) -> Result<Command, Box<Error<Rule>>> {
match pair.as_rule() {
Rule::GetType => {
let mut iter = pair.into_inner();
- let t = build_term_from_expr(iter.next().unwrap())?;
+ let t = build_term_from_expr(iter.next().unwrap(), &mut VecDeque::new())?;
Ok(Command::GetType(t))
}
Rule::CheckType => {
let mut iter = pair.into_inner();
- let t1 = build_term_from_expr(iter.next().unwrap())?;
- let t2 = build_term_from_expr(iter.next().unwrap())?;
+ let t1 = build_term_from_expr(iter.next().unwrap(), &mut VecDeque::new())?;
+ let t2 = build_term_from_expr(iter.next().unwrap(), &mut VecDeque::new())?;
Ok(Command::CheckType(t1, t2))
}
Rule::Define => {
let mut iter = pair.into_inner();
let s = iter.next().unwrap().as_str().to_string();
- let t = build_term_from_expr(iter.next().unwrap())?;
+ let t = build_term_from_expr(iter.next().unwrap(), &mut VecDeque::new())?;
Ok(Command::Define(s, t))
}
- command => panic!("Unexpected command: {:?}", command),
- }
-}
-
-pub fn parse_term(file: &str) -> Result<Term, Box<Error<Rule>>> {
- let pair = CommandParser::parse(Rule::Term, file)?.next().unwrap();
- match build_term_from_expr(pair) {
- Ok(t) => Ok(t),
- Err(s) => Err(box Error::new_from_pos(
- ErrorVariant::CustomError {
- message: String::from("Free variable: ") + &s,
- },
- //TODO: Add more details, eg: variable position (#8)
- Position::from_start(file),
- )),
- }
-}
-
-pub fn parse_command(file: &str) -> Result<Command, Box<Error<Rule>>> {
- let pair = CommandParser::parse(Rule::Command, file)?.next().unwrap();
- match build_command_from_expr(pair) {
- Ok(t) => Ok(t),
- Err(s) => Err(box Error::new_from_pos(
+ Rule::DefineCheckType => {
+ let mut iter = pair.into_inner();
+ let s = iter.next().unwrap().as_str().to_string();
+ let t1 = build_term_from_expr(iter.next().unwrap(), &mut VecDeque::new())?;
+ let t2 = build_term_from_expr(iter.next().unwrap(), &mut VecDeque::new())?;
+ Ok(Command::DefineCheckType(s, t1, t2))
+ }
+ Rule::error_dot => Err(box Error::new_from_pos(
ErrorVariant::CustomError {
- message: String::from("Free variable: ") + &s,
+ message: String::from("missing dot"),
},
- Position::from_start(file),
+ pair.as_span().end_pos(),
)),
+ command => panic!("Unexpected command: {:?}", command),
}
}
-// TODO: Unsatisfactory behavior (#7)
-pub fn parse_file(file: &str) -> Result<Vec<Command>, Box<Error<Rule>>> {
- let mut vec = Vec::new();
- for pair in CommandParser::parse(Rule::File, file)?
- .next()
- .unwrap()
- .into_inner()
- {
- match pair.as_rule() {
- Rule::EOI => (),
- _ => {
- if let Ok(t) = build_command_from_expr(pair) {
- vec.push(t)
- }
- }
- }
- }
- Ok(vec)
+/// Parse a text input and try to convert it into a vector of commands.
+///
+/// If unsuccessful, a box containing the first error that was encountered is returned.
+pub fn parse_commands(file: &str) -> Result<Vec<Command>, Box<Error<Rule>>> {
+ CommandParser::parse(Rule::File, file)?
+ .map(build_command_from_expr)
+ .collect()
}
diff --git a/parser/src/term.pest b/parser/src/term.pest
new file mode 100644
index 00000000..2c7a5c12
--- /dev/null
+++ b/parser/src/term.pest
@@ -0,0 +1,40 @@
+WHITESPACE = _{ WHITE_SPACE }
+COMMENT = _{ "#" ~ (!"\n" ~ ANY)* }
+number = @{ ASCII_DIGIT+ }
+string = @{ !keywords ~ ASCII_ALPHA ~ ( "_" | ASCII_ALPHANUMERIC )* }
+keywords = @{ ( "fun" | "type" | "def" | "check" | "Prop" | "Type" ) ~ !ASCII_ALPHANUMERIC }
+eoi = _{ !ANY }
+
+Term = _{ Abs | dProd | Prod | App | Var | Prop | Type | "(" ~ Term ~ ")" }
+term_prod = _{ App | Abs | dProd | Var | Prop | Type | "(" ~ term_prod ~ ")" }
+term_app = _{ Abs | dProd | Var | Prop | Type | "(" ~ Prod ~ ")" | "(" ~ term_app ~ ")" }
+term_dprod = _{ App | Abs | dProd | Var | Prop | Type | "(" ~ Prod ~ ")" | "(" ~ term_dprod ~ ")" }
+term_abs = _{ App | Abs | dProd | Var | Prop | Type | "(" ~ Prod ~ ")" | "(" ~ term_abs ~ ")" }
+
+Abs = { ( "fun" ~ ( arg_abs_par ~ ( "," ~ arg_abs_par )* ) ~ "=>" ~ Term ) }
+Abs_ = { ( "fun" ~ ( string ~ ( "," ~ string )* ) ~ "=>" ~ Term ) }
+arg_abs = { ( string ~ ":" ~ term_abs ) }
+arg_abs_par = _{ arg_abs | "(" ~ arg_abs ~ ")" }
+
+dProd = { "(" ~ ( arg_dprod_par ~ ( "," ~ arg_dprod_par )* ) ~ ")" ~ "->" ~ Term }
+dProd_ = { "(" ~ ( string ~ ( "," ~ string )* ) ~ ")" ~ "->" ~ Term }
+arg_dprod = { ( string ~ ":" ~ term_dprod ) }
+arg_dprod_par = _{ arg_dprod | "(" ~ arg_dprod ~ ")" }
+
+App = { term_app ~ term_app+ }
+Prod = { term_prod ~ ( "->" ~ term_prod )+ }
+
+Prop = { "Prop" }
+Type = { "Type(" ~ number ~ ")" }
+Var = { string }
+
+Command = _{ ( Define | CheckType | GetType | DefineCheckType ) ~ "." }
+Define = { "def" ~ string ~ ":=" ~ Term }
+DefineCheckType = { "def" ~ string ~ ":" ~ Term ~ ":=" ~ Term }
+CheckType = { "check" ~ Term ~ ":" ~ Term }
+GetType = { "type" ~ Term }
+
+Error = _{ error_dot }
+error_dot = { ( Define | CheckType | GetType | DefineCheckType ) }
+
+File = _{ SOI ~ ( NEWLINE* ~ ( Command | Error ) )* ~ NEWLINE* ~ eoi }
diff --git a/parser/tests/example.mdln b/parser/tests/example.mdln
deleted file mode 100644
index 69e17671..00000000
--- a/parser/tests/example.mdln
+++ /dev/null
@@ -1,4 +0,0 @@
-Define Test := P.
-
-
-
diff --git a/parser/tests/example.rs b/parser/tests/example.rs
deleted file mode 100644
index 0ee5ead7..00000000
--- a/parser/tests/example.rs
+++ /dev/null
@@ -1,12 +0,0 @@
-use kernel::{Command, Term};
-
-#[test]
-fn parse() {
- use std::fs;
- let contents: &str =
- &fs::read_to_string("tests/example.mdln").expect("Should have been able to read the file");
- assert_eq!(
- parser::parse_file(contents),
- Ok(vec![Command::Define("Test".to_string(), Term::Prop)])
- );
-}
diff --git a/proost/src/main.rs b/proost/src/main.rs
index a97b027a..dbc7cd69 100644
--- a/proost/src/main.rs
+++ b/proost/src/main.rs
@@ -1,7 +1,7 @@
#![feature(box_syntax)]
use clap::Parser;
-use parser::{parse_command, parse_file};
+use parser::parse_commands;
use rustyline::error::ReadlineError;
use rustyline::Editor;
use std::error::Error;
@@ -25,7 +25,7 @@ fn main() -> Result<(), Box<dyn Error>> {
for path in args.files.iter() {
match fs::read_to_string(path) {
Ok(contents) => {
- let _ = parse_file(&contents);
+ let _ = parse_commands(&contents);
}
Err(_) => {
println!("Error: No such file or directory: {}", path);
@@ -46,13 +46,18 @@ fn main() -> Result<(), Box<dyn Error>> {
loop {
let readline = rl.readline(">> ");
match readline {
- Ok(line) => {
+ Ok(line) if !line.is_empty() => {
rl.add_history_entry(line.as_str());
- match parse_command(line.as_str()) {
- Ok(command) => println!("{}", command),
+ match parse_commands(line.as_str()) {
+ Ok(commands) => {
+ for command in commands {
+ println!("{}", command);
+ }
+ }
Err(err) => println!("{}", *err),
}
}
+ Ok(_) => (),
Err(ReadlineError::Interrupted) => {}
Err(ReadlineError::Eof) => break,
Err(err) => {
--
GitLab