feat(parser): Add new syntaxic sugar and meaningfull error messages, add more... ✨️

Closes #10 🐔️👍️
Approved-by: v-lafeychine <vincent.lafeychine@proton.me>
Approved-by: aalbert <augustin.albert@bleu-azure.fr>
Approved-by: loutr <loutr@crans.org>

🦀️🍰🦀️🍰🦀️🍰

* 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

@@ -11,4 +11,7 @@ pub enum Command {
 
     #[display(fmt = "Type {}.", _0)]
     GetType(Term),
+
+    #[display(fmt = "Define {} : {} := {}.", _0, _1, _2)]
+    DefineCheckType(String, Term, Term),
 }

parser/src/classic_term.pest

-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 }

parser/src/classic_term.rs

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

parser/src/lib.rs

+//! 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;

parser/src/parser.rs

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

parser/src/term.pest

+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 }

parser/tests/example.mdln

-Define Test := P.
-
-
-

parser/tests/example.rs

-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)])
-    );
-}

proost/src/main.rs

 #![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) => {