Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • loutr/proost
  • jeanas/proost
2 results
Show changes
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 919 additions and 177 deletions
parser/src/term.pest → parser/src/command/grammar.pest
View file @ 420f6576
File moved
parser/src/command.rs → parser/src/command/mod.rs
View file @ 420f6576
......@@ -2,6 +2,8 @@
//!
//! This complements low-level functions defined in the [`kernel::type_checker`] module.
pub mod parse;
use core::fmt;
use kernel::memory::declaration::builder as declaration;
......@@ -33,25 +35,26 @@ pub enum Command<'build> {
}
impl<'build> fmt::Display for Command<'build> {
#[inline]
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
use Command::*;
use Command::{CheckType, Declaration, Define, Eval, GetType, Import, Search};
match self {
Define(name, None, t) => write!(f, "def {name} := {t}"),
match *self {
Define(name, None, ref t) => write!(f, "def {name} := {t}"),
Define(name, Some(ty), t) => write!(f, "def {name}: {ty} := {t}"),
Define(name, Some(ref ty), ref t) => write!(f, "def {name}: {ty} := {t}"),
Declaration(name, None, t) => write!(f, "def {name} := {t}"),
Declaration(name, None, ref t) => write!(f, "def {name} := {t}"),
Declaration(name, Some(ty), t) => write!(f, "def {name}: {ty} := {t}"),
Declaration(name, Some(ref ty), ref t) => write!(f, "def {name}: {ty} := {t}"),
CheckType(t, ty) => write!(f, "check {t}: {ty}"),
CheckType(ref t, ref ty) => write!(f, "check {t}: {ty}"),
GetType(t) => write!(f, "check {t}"),
GetType(ref t) => write!(f, "check {t}"),
Eval(t) => write!(f, "eval {t}"),
Eval(ref t) => write!(f, "eval {t}"),
Import(files) => {
Import(ref files) => {
write!(f, "imports")?;
files.iter().try_for_each(|file| write!(f, " {file}"))
},
......
parser/src/command/parse.rs 0 → 100644
View file @ 420f6576
This diff is collapsed.
parser/src/parser.rs → parser/src/command/pest.rs
View file @ 420f6576
......@@ -10,7 +10,7 @@ use crate::command::Command;
use crate::error;
#[derive(Parser)]
#[grammar = "term.pest"]
#[grammar = "command/grammar.pest"]
struct CommandParser;
/// convert pest locations to kernel locations
......@@ -22,7 +22,7 @@ fn convert_span(span: Span) -> Location {
/// build universe level from errorless pest's output
fn parse_level(pair: Pair<Rule>) -> level::Builder {
use level::Builder::*;
use level::Builder::{Const, IMax, Max, Plus, Var};
// location to be used in a future version
let _loc = convert_span(pair.as_span());
......@@ -65,7 +65,7 @@ fn parse_level(pair: Pair<Rule>) -> level::Builder {
/// Returns a kernel term builder from pest output
fn parse_term(pair: Pair<Rule>) -> term::Builder {
use term::Builder::*;
use term::Builder::{Abs, App, Decl, Prod, Prop, Sort, Type, Var};
// location to be used in a future version
let _loc = convert_span(pair.as_span());
......@@ -82,21 +82,15 @@ fn parse_term(pair: Pair<Rule>) -> term::Builder {
Decl(box declaration::InstantiatedBuilder::Var(name, levels))
},
Rule::Type => {
if let Some(next) = pair.into_inner().next_back() {
Type(box parse_level(next))
} else {
Type(box level::Builder::Const(0))
}
},
Rule::Type => pair
.into_inner()
.next_back()
.map_or(Type(box level::Builder::Const(0)), |next| Type(box parse_level(next))),
Rule::Sort => {
if let Some(next) = pair.into_inner().next_back() {
Sort(box parse_level(next))
} else {
Sort(box level::Builder::Const(0))
}
},
Rule::Sort => pair
.into_inner()
.next_back()
.map_or(Sort(box level::Builder::Const(0)), |next| Sort(box parse_level(next))),
Rule::App => {
let mut iter = pair.into_inner().map(parse_term);
......@@ -256,22 +250,25 @@ fn convert_error(err: pest::error::Error<Rule>) -> error::Error {
let mut left = 1;
let chars = err.line().chars();
let mut i = 0;
for c in chars {
i += 1;
if char::is_whitespace(c) {
if i < y {
left = i + 1
left = i + 1;
} else {
break;
}
} else {
right = i
right = i;
}
}
if i < y {
left = y;
right = y;
}
Location::new((x, left).into(), (x, right).into())
},
......@@ -281,11 +278,13 @@ fn convert_error(err: pest::error::Error<Rule>) -> error::Error {
// extracting the message from the pest output
let message = err.to_string();
let mut chars = message.lines().next_back().unwrap().chars();
for _ in 0..4 {
(0_i32..4_i32).for_each(|_| {
chars.next();
}
});
error::Error {
kind: error::ErrorKind::CannotParse(chars.as_str().to_string()),
kind: error::Kind::CannotParse(chars.as_str().to_owned()),
location: loc,
}
}
......@@ -293,21 +292,27 @@ fn convert_error(err: pest::error::Error<Rule>) -> error::Error {
/// Parse a text input and try to convert it into a command.
///
/// if unsuccessful, a box containing the first error that was encountered is returned.
#[inline]
pub fn parse_line(line: &str) -> error::Result<Command> {
CommandParser::parse(Rule::command, line).map_err(convert_error).map(|mut pairs| parse_expr(pairs.next().unwrap()))
CommandParser::parse(Rule::command, line)
.map_err(convert_error)
.map(|mut pairs| parse_expr(pairs.next().unwrap_or_else(|| unreachable!())))
}
/// 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.
#[inline]
pub fn parse_file(file: &str) -> error::Result<Vec<Command>> {
CommandParser::parse(Rule::file, file).map_err(convert_error).map(|pairs| pairs.into_iter().map(parse_expr).collect())
CommandParser::parse(Rule::file, file)
.map_err(convert_error)
.map(|pairs| pairs.into_iter().map(parse_expr).collect())
}
#[cfg(test)]
mod tests {
use error::{Error, ErrorKind};
use error::{Error, Kind};
use kernel::memory::term::builder as term;
use term::Builder::*;
......@@ -325,7 +330,7 @@ mod tests {
assert_eq!(
parse_line("check fun x : Prop -> Type"),
Err(Error {
kind: ErrorKind::CannotParse(UNIVERSE_ERR.to_string()),
kind: Kind::CannotParse(UNIVERSE_ERR.to_owned()),
location: Location::new((1, 27).into(), (1, 27).into()),
})
);
......@@ -357,17 +362,17 @@ mod tests {
#[test]
fn successful_import() {
assert_eq!(parse_line("import file1 dir/file2"), Ok(Import(["file1", "dir/file2"].to_vec())));
assert_eq!(parse_line("import "), Ok(Import(Vec::new())))
assert_eq!(parse_line("import "), Ok(Import(Vec::new())));
}
#[test]
fn successful_search() {
assert_eq!(parse_line("search variable1"), Ok(Search("variable1")))
assert_eq!(parse_line("search variable1"), Ok(Search("variable1")));
}
#[test]
fn successful_eval() {
assert_eq!(parse_line("eval Prop"), Ok(Eval(Prop)))
assert_eq!(parse_line("eval Prop"), Ok(Eval(Prop)));
}
#[test]
......@@ -471,14 +476,14 @@ mod tests {
assert_eq!(
parse_line("check (x:A)"),
Err(Error {
kind: ErrorKind::CannotParse(SIMPLE_TERM_ERR.to_string()),
kind: Kind::CannotParse(SIMPLE_TERM_ERR.to_owned()),
location: Location::new((1, 7).into(), (1, 11).into()),
})
);
assert_eq!(
parse_line("check (x:A) -> (y:B)"),
Err(Error {
kind: ErrorKind::CannotParse(SIMPLE_TERM_ERR.to_string()),
kind: Kind::CannotParse(SIMPLE_TERM_ERR.to_owned()),
location: Location::new((1, 16).into(), (1, 20).into()),
})
);
......@@ -576,21 +581,21 @@ mod tests {
assert_eq!(
parse_line("chehk 2x"),
Err(Error {
kind: ErrorKind::CannotParse(COMMAND_ERR.to_string()),
kind: Kind::CannotParse(COMMAND_ERR.to_owned()),
location: Location::new((1, 1).into(), (1, 5).into()),
})
);
assert_eq!(
parse_line("check 2x"),
Err(Error {
kind: ErrorKind::CannotParse(TERM_ERR.to_string()),
kind: Kind::CannotParse(TERM_ERR.to_owned()),
location: Location::new((1, 7).into(), (1, 8).into()),
})
);
assert_eq!(
parse_line("check x:"),
Err(Error {
kind: ErrorKind::CannotParse(TERM_ERR.to_string()),
kind: Kind::CannotParse(TERM_ERR.to_owned()),
location: Location::new((1, 9).into(), (1, 9).into()),
})
);
......@@ -605,7 +610,7 @@ mod tests {
check .x"
),
Err(Error {
kind: ErrorKind::CannotParse(TERM_ERR.to_string()),
kind: Kind::CannotParse(TERM_ERR.to_owned()),
location: Location::new((3, 31).into(), (3, 32).into()),
})
);
......
parser/src/error.rs
View file @ 420f6576
......@@ -3,10 +3,10 @@ use kernel::location::Location;
/// Type representing parser errors.
#[derive(Clone, Debug, Display, Eq, PartialEq)]
#[display(fmt = "{}", kind)]
#[display(fmt = "{kind}")]
pub struct Error {
/// The kind of form error that occurred.
pub kind: ErrorKind,
pub kind: Kind,
/// The location of the error.
pub location: Location,
......@@ -14,10 +14,10 @@ pub struct Error {
#[non_exhaustive]
#[derive(Clone, Debug, Display, Eq, PartialEq)]
pub enum ErrorKind {
pub enum Kind {
CannotParse(String),
}
impl std::error::Error for Error {}
pub type Result<T> = std::result::Result<T, Error>;
pub type Result<T> = core::result::Result<T, Error>;
parser/src/lib.rs
View file @ 420f6576
......@@ -5,12 +5,57 @@
#![feature(box_syntax)]
#![feature(result_flattening)]
#![deny(
clippy::complexity,
clippy::correctness,
clippy::nursery,
clippy::pedantic,
clippy::perf,
clippy::restriction,
clippy::style,
clippy::suspicious
)]
#![allow(
clippy::arithmetic_side_effects,
clippy::blanket_clippy_restriction_lints,
clippy::else_if_without_else,
clippy::exhaustive_enums,
clippy::exhaustive_structs,
clippy::implicit_return,
clippy::integer_arithmetic,
clippy::match_same_arms,
clippy::match_wildcard_for_single_variants,
clippy::missing_trait_methods,
clippy::mod_module_files,
clippy::panic_in_result_fn,
clippy::pattern_type_mismatch,
clippy::separated_literal_suffix,
clippy::shadow_reuse,
clippy::shadow_unrelated,
clippy::unreachable,
clippy::wildcard_enum_match_arm,
// Due to pest dependency
clippy::self_named_module_files,
clippy::pub_use,
clippy::std_instead_of_core,
clippy::unwrap_used
)]
#![warn(clippy::missing_docs_in_private_items, clippy::missing_errors_doc)]
#![cfg_attr(
test,
allow(
clippy::assertions_on_result_states,
clippy::enum_glob_use,
clippy::indexing_slicing,
clippy::non_ascii_literal,
clippy::too_many_lines,
clippy::unwrap_used,
clippy::wildcard_imports,
)
)]
#[macro_use]
extern crate pest_derive;
pub mod command;
pub mod error;
mod parser;
pub use self::parser::*;
proost/Cargo.toml
View file @ 420f6576
[package]
name = "proost"
description.workspace = true
description = "A simple proof assistant written in Rust"
authors.workspace = true
edition.workspace = true
license.workspace = true
repository.workspace = true
version.workspace = true
[dependencies]
kernel.path = "../kernel"
parser.path = "../parser"
atty.workspace = true
clap.workspace = true
colored.workspace = true
derive_more.workspace = true
path-absolutize.workspace = true
rustyline-derive.workspace = true
rustyline.workspace = true
atty = "0.2"
colored = "2"
path-absolutize = "3.0.14"
rustyline = "10.0.0"
rustyline-derive = "0.7.0"
proost/src/error.rs
View file @ 420f6576
......@@ -16,4 +16,4 @@ pub enum Error<'arena> {
impl std::error::Error for Error<'_> {}
pub type Result<'arena, T> = std::result::Result<T, Error<'arena>>;
pub type Result<'arena, T> = core::result::Result<T, Error<'arena>>;
proost/src/evaluator.rs
View file @ 420f6576
......@@ -2,21 +2,19 @@ use std::collections::HashSet;
use std::fs::read_to_string;
use std::path::PathBuf;
use colored::Colorize;
use derive_more::Display;
use kernel::location::Location;
use kernel::memory::arena::Arena;
use kernel::memory::term::Term;
use parser::command::Command;
use parser::{parse_file, parse_line};
use parser::command::{parse, Command};
use path_absolutize::Absolutize;
use crate::error::Error::*;
use crate::error::Error::Toplevel;
use crate::error::Result;
/// Type representing parser errors.
#[derive(Clone, Debug, Display, Eq, PartialEq)]
#[display(fmt = "{}", kind)]
#[display(fmt = "{kind}")]
pub struct Error {
/// The kind of form error that occurred.
pub kind: ErrorKind,
......@@ -28,11 +26,11 @@ pub struct Error {
#[non_exhaustive]
#[derive(Clone, Debug, Display, Eq, PartialEq)]
pub enum ErrorKind {
#[display(fmt = "{} is not a file", _0)]
#[display(fmt = "{_0} is not a file")]
FileNotFound(String),
#[display(fmt = "cyclic dependency:\n{}", _0)]
#[display(fmt = "cyclic dependency:\n{_0}")]
CyclicDependencies(String),
#[display(fmt = "identifier {} already defined", _0)]
#[display(fmt = "identifier {_0} already defined")]
BoundVariable(String),
}
......@@ -45,8 +43,8 @@ pub struct Evaluator {
}
impl<'arena> Evaluator {
pub fn new(path: PathBuf, verbose: bool) -> Evaluator {
Evaluator {
pub fn new(path: PathBuf, verbose: bool) -> Self {
Self {
path,
imported: HashSet::new(),
verbose,
......@@ -60,9 +58,9 @@ impl<'arena> Evaluator {
.and_then(|path| path.parent())
.unwrap_or(&self.path)
.join(relative_path)
.absolutize()
.unwrap()
.absolutize()?
.to_path_buf();
if file_path.is_file() {
Ok(file_path)
} else {
......@@ -75,7 +73,7 @@ impl<'arena> Evaluator {
/// Begin a new file importation.
///
/// file_path must be absolute
/// `file_path` must be absolute
fn import_file(
&mut self,
arena: &mut Arena<'arena>,
......@@ -90,7 +88,11 @@ impl<'arena> Evaluator {
if let Some(i) = importing.iter().position(|path| path == &file_path) {
return Err(Toplevel(Error {
kind: ErrorKind::CyclicDependencies(
importing[i..].iter().map(|path| path.to_string_lossy()).collect::<Vec<_>>().join(" \u{2192}\n"),
importing[i..]
.iter()
.map(|path| path.to_string_lossy())
.collect::<Vec<_>>()
.join(" \u{2192}\n"),
),
location,
}));
......@@ -102,7 +104,7 @@ impl<'arena> Evaluator {
// try to import it
let result = self.process_file(arena, &file, importing);
// remove it from the list of files to import
let file_path = importing.pop().unwrap();
let file_path = importing.pop().unwrap_or_else(|| unreachable!());
// if importation failed, return error, else add file to imported files
result?;
self.imported.insert(file_path);
......@@ -110,7 +112,7 @@ impl<'arena> Evaluator {
}
pub fn process_line(&mut self, arena: &mut Arena<'arena>, line: &str) -> Result<'arena, Option<Term<'arena>>> {
let command = parse_line(line)?;
let command = parse::line(line)?;
self.process(arena, &command, &mut Vec::new())
}
......@@ -120,12 +122,11 @@ impl<'arena> Evaluator {
file: &str,
importing: &mut Vec<PathBuf>,
) -> Result<'arena, Option<Term<'arena>>> {
let commands = parse_file(file)?;
commands
parse::file(file)?
.iter()
.try_for_each(|command| {
if self.verbose {
println!("{}", command);
println!("{command}");
}
self.process(arena, command, importing).map(|_| ())
})
......@@ -138,56 +139,56 @@ impl<'arena> Evaluator {
command: &Command,
importing: &mut Vec<PathBuf>,
) -> Result<'arena, Option<Term<'arena>>> {
match command {
Command::Define(s, ty, term) => {
match *command {
Command::Define(s, ref ty, ref term) => {
if arena.get_binding(s).is_some() {
return Err(Toplevel(Error {
kind: ErrorKind::BoundVariable(s.to_string()),
kind: ErrorKind::BoundVariable(s.to_owned()),
location: Location::default(), // TODO (see #38)
}));
}
let term = term.realise(arena)?;
match ty {
match *ty {
None => {
term.infer(arena)?;
},
Some(ty) => term.check(ty.realise(arena)?, arena)?,
Some(ref ty) => term.check(ty.realise(arena)?, arena)?,
}
arena.bind(s, term);
Ok(None)
},
Command::Declaration(s, ty, decl) => {
Command::Declaration(s, ref ty, ref decl) => {
if arena.get_binding_decl(s).is_some() {
return Err(Toplevel(Error {
kind: ErrorKind::BoundVariable(s.to_string()),
kind: ErrorKind::BoundVariable(s.to_owned()),
location: Location::default(), // TODO (see #38)
}));
}
let decl = decl.realise(arena)?;
match ty {
match *ty {
None => {
decl.infer(arena)?;
},
Some(ty) => decl.check(ty.realise(arena)?, arena)?,
Some(ref ty) => decl.check(ty.realise(arena)?, arena)?,
}
arena.bind_decl(s, decl);
Ok(None)
},
Command::CheckType(t1, t2) => {
Command::CheckType(ref t1, ref t2) => {
let t1 = t1.realise(arena)?;
let t2 = t2.realise(arena)?;
t1.check(t2, arena)?;
Ok(None)
},
Command::GetType(t) => {
Command::GetType(ref t) => {
let t = t.realise(arena)?;
Ok(t.infer(arena).map(Some)?)
},
Command::Eval(t) => {
Command::Eval(ref t) => {
let t = t.realise(arena)?;
let _ = t.infer(arena)?;
Ok(Some(t.normal_form(arena)))
......@@ -195,51 +196,13 @@ impl<'arena> Evaluator {
Command::Search(s) => Ok(arena.get_binding(s)), // TODO (see #49)
Command::Import(files) => files
Command::Import(ref files) => files
.iter()
.try_for_each(|relative_path| {
let file_path = self.create_path(Location::default(), relative_path.to_string(), importing)?;
let file_path = self.create_path(Location::default(), (*relative_path).to_owned(), importing)?;
self.import_file(arena, Location::default(), file_path, importing)
})
.map(|_| None),
}
}
pub fn display(&self, res: Result<'arena, Option<Term<'arena>>>) {
match res {
Ok(None) => println!("{}", "\u{2713}".green()),
Ok(Some(t)) => {
for line in t.to_string().lines() {
println!("{} {}", "\u{2713}".green(), line)
}
},
Err(err) => {
let string = match err {
Parser(parser::error::Error {
kind: parser::error::ErrorKind::CannotParse(message),
location: loc,
}) => {
if loc.start.column == loc.end.column {
format!("{:0w1$}^\n{m}", "", w1 = loc.start.column - 1, m = message)
} else {
format!(
"{:0w1$}^{:-<w2$}^\n{m}",
"",
"",
w1 = loc.start.column - 1,
w2 = loc.end.column - loc.start.column - 1,
m = message
)
}
},
_ => err.to_string(),
};
for line in string.lines() {
println!("{} {}", "\u{2717}".red(), line)
}
},
}
}
}
proost/src/main.rs
View file @ 420f6576
#![doc(html_logo_url = "https://gitlab.crans.org/loutr/proost/-/raw/main/docs/media/logo.png")]
#![feature(let_chains)]
#![deny(
clippy::complexity,
clippy::correctness,
clippy::nursery,
clippy::pedantic,
clippy::perf,
clippy::restriction,
clippy::style,
clippy::suspicious
)]
#![allow(
clippy::arithmetic_side_effects,
clippy::blanket_clippy_restriction_lints,
clippy::else_if_without_else,
clippy::exhaustive_enums,
clippy::exhaustive_structs,
clippy::implicit_return,
clippy::integer_arithmetic,
clippy::match_same_arms,
clippy::match_wildcard_for_single_variants,
clippy::missing_trait_methods,
clippy::mod_module_files,
clippy::panic_in_result_fn,
clippy::pattern_type_mismatch,
clippy::separated_literal_suffix,
clippy::shadow_reuse,
clippy::shadow_unrelated,
clippy::unreachable,
clippy::wildcard_enum_match_arm,
// Due to clap dependency
clippy::std_instead_of_core,
// Due to this crate is a binary manipulating string
clippy::indexing_slicing,
clippy::print_stdout,
clippy::string_slice
)]
#![warn(clippy::missing_errors_doc, clippy::missing_docs_in_private_items)]
#![cfg_attr(
test,
allow(
clippy::assertions_on_result_states,
clippy::enum_glob_use,
clippy::indexing_slicing,
clippy::non_ascii_literal,
clippy::too_many_lines,
clippy::unwrap_used,
clippy::wildcard_imports,
)
)]
extern crate alloc;
mod error;
mod evaluator;
......@@ -10,12 +61,14 @@ use std::fs;
use atty::Stream;
use clap::Parser;
use colored::Colorize;
use evaluator::Evaluator;
use kernel::memory::term::Term;
use rustyline::error::ReadlineError;
use rustyline::{Cmd, Config, Editor, EventHandler, KeyCode, KeyEvent, Modifiers};
use rustyline_helper::*;
use rustyline_helper::{RustyLineHelper, TabEventHandler};
use crate::error::Result;
use crate::error::{Error, Result};
#[derive(Parser)]
#[command(author, version, about, long_about = None)]
......@@ -38,7 +91,11 @@ fn main() -> Result<'static, ()> {
// check if files are provided as command-line arguments
if !args.files.is_empty() {
return args.files.iter().try_for_each(|path| fs::read_to_string(path).map(|_| ())).map_err(error::Error::from);
return args
.files
.iter()
.try_for_each(|path| fs::read_to_string(path).map(|_| ()))
.map_err(error::Error::from);
}
// check if we are in a terminal
......@@ -57,15 +114,15 @@ fn main() -> Result<'static, ()> {
let current_path = current_dir()?;
let mut evaluator = Evaluator::new(current_path, args.verbose);
println!("Welcome to {} {}", NAME, VERSION);
println!("Welcome to {NAME} {VERSION}");
loop {
let readline = rl.readline("\u{00BB} ");
match readline {
Ok(line) if is_command(&line) => {
rl.add_history_entry(line.as_str());
let result = evaluator.process_line(arena, line.as_str());
evaluator.display(result);
display(evaluator.process_line(arena, line.as_str()));
},
Ok(_) => (),
Err(ReadlineError::Interrupted) => {},
......@@ -73,16 +130,53 @@ fn main() -> Result<'static, ()> {
Err(err) => return Err(err.into()),
}
}
Ok(())
})
}
pub fn display<'arena>(res: Result<'arena, Option<Term<'arena>>>) {
match res {
Ok(None) => println!("{}", "\u{2713}".green()),
Ok(Some(t)) => {
for line in t.to_string().lines() {
println!("{} {line}", "\u{2713}".green());
}
},
Err(err) => {
let string = match err {
Error::Parser(parser::error::Error {
kind: parser::error::Kind::CannotParse(message),
location: loc,
}) => {
if loc.start.column == loc.end.column {
format!("{:0w1$}^\n{message}", "", w1 = loc.start.column - 1)
} else {
format!(
"{:0w1$}^{:-<w2$}^\n{message}",
"",
"",
w1 = loc.start.column - 1,
w2 = loc.end.column - loc.start.column - 1
)
}
},
_ => err.to_string(),
};
for line in string.lines() {
println!("{} {line}", "\u{2717}".red());
}
},
}
}
fn is_command(input: &str) -> bool {
input
.chars()
.position(|c| !c.is_whitespace())
.map(|pos| input.len() < 2 || input[pos..pos + 2] != *"//")
.unwrap_or_else(|| false)
.map_or(false, |pos| input.len() < 2 || input[pos..pos + 2] != *"//")
}
#[cfg(test)]
......@@ -101,13 +195,13 @@ mod tests {
fn is_command_false() {
assert!(!super::is_command(" "));
assert!(!super::is_command(" "));
assert!(!super::is_command("// comment"))
assert!(!super::is_command("// comment"));
}
#[test]
fn is_command_true() {
assert!(super::is_command(" check x"));
assert!(super::is_command(" check x"));
assert!(super::is_command("check x // comment"))
assert!(super::is_command("check x // comment"));
}
}
proost/src/rustyline_helper.rs
View file @ 420f6576
use std::borrow::Cow::{self, Borrowed, Owned};
use alloc::borrow::Cow::{self, Borrowed, Owned};
use colored::*;
use colored::Colorize;
use rustyline::completion::{Completer, FilenameCompleter, Pair};
use rustyline::highlight::Highlighter;
use rustyline::hint::HistoryHinter;
......@@ -11,7 +11,7 @@ use rustyline_derive::{Helper, Hinter};
/// Language keywords that should be highlighted
const KEYWORDS: [&str; 5] = ["check", "def", "eval", "import", "search"];
/// An Helper for a RustyLine Editor that implements:
/// An Helper for a `RustyLine` Editor that implements:
/// - a standard hinter;
/// - custom validator, completer and highlighter.
#[derive(Helper, Hinter)]
......@@ -39,11 +39,11 @@ impl ConditionalEventHandler for TabEventHandler {
if ctx.line().starts_with("import") {
return None;
}
Some(Cmd::Insert(n, " ".to_string()))
Some(Cmd::Insert(n, " ".to_owned()))
}
}
/// A variation of [FilenameCompleter](https://docs.rs/rustyline/latest/rustyline/completion/struct.FilenameCompleter.html):
/// A variation of [`FilenameCompleter`](https://docs.rs/rustyline/latest/rustyline/completion/struct.FilenameCompleter.html):
/// file completion is available only after having typed import
impl Completer for RustyLineHelper {
type Candidate = Pair;
......@@ -53,7 +53,7 @@ impl Completer for RustyLineHelper {
}
}
/// A variation of [MatchingBracketValidator](https://docs.rs/rustyline/latest/rustyline/validate/struct.MatchingBracketValidator.html).
/// A variation of [`MatchingBracketValidator`](https://docs.rs/rustyline/latest/rustyline/validate/struct.MatchingBracketValidator.html).
///
/// No validation occurs when entering the import command
impl Validator for RustyLineHelper {
......@@ -62,7 +62,9 @@ impl Validator for RustyLineHelper {
return Ok(ValidationResult::Valid(None));
}
Ok(validate_arrows(ctx.input()).or_else(|| validate_brackets(ctx.input())).unwrap_or(ValidationResult::Valid(None)))
Ok(validate_arrows(ctx.input())
.or_else(|| validate_brackets(ctx.input()))
.unwrap_or(ValidationResult::Valid(None)))
}
}
......@@ -87,9 +89,9 @@ fn validate_brackets(input: &str) -> Option<ValidationResult> {
')' => match stack.pop() {
Some('(') => {},
Some(_) => {
return Some(ValidationResult::Invalid(Some("\nMismatched brackets: ) is not properly closed".to_string())));
return Some(ValidationResult::Invalid(Some("\nMismatched brackets: ) is not properly closed".to_owned())));
},
None => return Some(ValidationResult::Invalid(Some("\nMismatched brackets: ( is unpaired".to_string()))),
None => return Some(ValidationResult::Invalid(Some("\nMismatched brackets: ( is unpaired".to_owned()))),
},
_ => {},
}
......@@ -98,11 +100,11 @@ fn validate_brackets(input: &str) -> Option<ValidationResult> {
if stack.is_empty() { None } else { Some(ValidationResult::Incomplete) }
}
/// A variation of [MatchingBracketHighlighter](https://docs.rs/rustyline/latest/rustyline/highlight/struct.MatchingBracketHighlighter.html).
/// A variation of [`MatchingBracketHighlighter`](https://docs.rs/rustyline/latest/rustyline/highlight/struct.MatchingBracketHighlighter.html).
///
/// No check occurs before cursor
impl Highlighter for RustyLineHelper {
fn highlight_hint<'h>(&self, hint: &'h str) -> Cow<'h, str> {
fn highlight_hint<'input>(&self, hint: &'input str) -> Cow<'input, str> {
if !self.color {
return Owned(hint.to_owned());
}
......@@ -113,7 +115,7 @@ impl Highlighter for RustyLineHelper {
self.color
}
fn highlight<'l>(&self, line: &'l str, pos: usize) -> Cow<'l, str> {
fn highlight<'input>(&self, line: &'input str, pos: usize) -> Cow<'input, str> {
if line.len() <= 1 || !self.color {
return Borrowed(line);
}
......@@ -121,10 +123,12 @@ impl Highlighter for RustyLineHelper {
if let Some((bracket, pos)) = get_bracket(line, pos)
&& let Some((matching, pos)) = find_matching_bracket(line, pos, bracket) {
let s = String::from(matching as char);
let s = String::from(matching);
copy.replace_range(pos..=pos, &format!("{}", s.blue().bold()));
}
KEYWORDS.iter().for_each(|keyword| replace_inplace(&mut copy, keyword, &format!("{}", keyword.blue().bold())));
KEYWORDS
.iter()
.for_each(|keyword| replace_inplace(&mut copy, keyword, &format!("{}", keyword.blue().bold())));
Owned(copy)
}
}
......@@ -139,30 +143,37 @@ pub fn replace_inplace(input: &mut String, from: &str, to: &str) {
input.replace_range((offset + pos)..(offset + pos + from.len()), to);
offset += pos + to.len();
} else {
offset += pos + from.len()
offset += pos + from.len();
}
}
}
fn find_matching_bracket(line: &str, pos: usize, bracket: u8) -> Option<(u8, usize)> {
fn find_matching_bracket(line: &str, pos: usize, bracket: u8) -> Option<(char, usize)> {
let matching_bracket = matching_bracket(bracket);
let mut to_match = 1;
let mut to_match: i32 = 1;
let match_bracket = |b: u8| {
if b == matching_bracket {
to_match -= 1;
if b == matching_bracket.try_into().unwrap_or_else(|_| unreachable!()) {
to_match -= 1_i32;
} else if b == bracket {
to_match += 1;
to_match += 1_i32;
};
to_match == 0
to_match == 0_i32
};
if is_open_bracket(bracket) {
// forward search
line[pos + 1..].bytes().position(match_bracket).map(|pos2| (matching_bracket, pos2 + pos + 1))
line[pos + 1..]
.bytes()
.position(match_bracket)
.map(|pos2| (matching_bracket, pos2 + pos + 1))
} else {
// backward search
line[..pos].bytes().rev().position(match_bracket).map(|pos2| (matching_bracket, pos - pos2 - 1))
line[..pos]
.bytes()
.rev()
.position(match_bracket)
.map(|pos2| (matching_bracket, pos - pos2 - 1))
}
}
......@@ -177,10 +188,10 @@ const fn get_bracket(line: &str, pos: usize) -> Option<(u8, usize)> {
None
}
const fn matching_bracket(bracket: u8) -> u8 {
const fn matching_bracket(bracket: u8) -> char {
match bracket {
b'(' => b')',
b')' => b'(',
b'(' => ')',
b')' => '(',
_ => unreachable!(),
}
}
......@@ -199,24 +210,24 @@ mod tests {
#[test]
fn get_bracket_empty() {
assert!(get_bracket("", 0).is_none())
assert!(get_bracket("", 0).is_none());
}
#[test]
fn get_bracket_out_of_bound() {
assert!(get_bracket("(())", 4).is_none())
assert!(get_bracket("(())", 4).is_none());
}
#[test]
fn get_bracket_none() {
assert!(get_bracket("a()[", 0).is_none());
assert!(get_bracket("a()[", 3).is_none())
assert!(get_bracket("a()[", 3).is_none());
}
#[test]
fn get_bracket_some() {
assert!(get_bracket("a()[", 1).is_some());
assert!(get_bracket("a()[", 2).is_some())
assert!(get_bracket("a()[", 2).is_some());
}
#[test]
......@@ -224,25 +235,25 @@ mod tests {
assert!(find_matching_bracket(" )", 1, b')').is_none());
assert!(find_matching_bracket(" )", 1, b'(').is_some());
assert!(find_matching_bracket("( ", 1, b')').is_some());
assert!(find_matching_bracket("( ", 1, b'(').is_none())
assert!(find_matching_bracket("( ", 1, b'(').is_none());
}
#[test]
fn find_matching_bracket_matching() {
assert_eq!(find_matching_bracket(" )", 1, b'('), Some((b')', 2)));
assert_eq!(find_matching_bracket("( ", 1, b')'), Some((b'(', 0)))
assert_eq!(find_matching_bracket(" )", 1, b'('), Some((')', 2)));
assert_eq!(find_matching_bracket("( ", 1, b')'), Some(('(', 0)));
}
#[test]
fn find_matching_bracket_counter() {
assert_eq!(find_matching_bracket(" (())))", 0, b'('), Some((b')', 5)));
assert_eq!(find_matching_bracket("(((()) ", 6, b')'), Some((b'(', 1)));
assert_eq!(find_matching_bracket(" (())))", 0, b'('), Some((')', 5)));
assert_eq!(find_matching_bracket("(((()) ", 6, b')'), Some(('(', 1)));
}
#[test]
fn replace_inplace() {
let mut message = "mot motus et mots mot mot".to_string();
let mut message = "mot motus et mots mot mot".to_owned();
super::replace_inplace(&mut message, "mot", "mots");
assert_eq!(message, "mots motus et mots mots mots".to_string())
assert_eq!(message, "mots motus et mots mots mots".to_owned());
}
}