Cargo.lock

@@ -467,11 +467,13 @@ name = "proost"
 version = "0.1.0"
 dependencies = [
  "anyhow",
+ "atty",
  "clap",
  "colored",
  "kernel",
  "parser",
  "rustyline",
+ "rustyline-derive",
 ]
 
 [[package]]
@@ -559,6 +561,17 @@ dependencies = [
  "winapi",
 ]
 
+[[package]]
+name = "rustyline-derive"
+version = "0.7.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "107c3d5d7f370ac09efa62a78375f94d94b8a33c61d8c278b96683fb4dbf2d8d"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
 [[package]]
 name = "scopeguard"
 version = "1.1.0"

Cargo.toml

@@ -10,6 +10,10 @@ anyhow = "1.0"
 clap = { version = "4.0.10", features = ["derive"] }
 derive_more = "0.99.17"
 num-bigint = "0.4"
+atty = "0.2"
+colored = "2"
+rustyline = "10.0.0"
+rustyline-derive = "0.7.0"
 
 [workspace.package]
 authors = [

README.md

@@ -2,22 +2,27 @@
 
 A simple proof assistant written in Rust.
 
-The specification of the project may be found
-[https://gitlab.crans.org/loutr/proost/-/blob/main/docs/specs.pdf](here).
-The documentation, generated with `rust-doc` may be found
-[https://perso.crans.org/v-lafeychine/proost/doc/proost/](here).
+The specification of the project may be found [here](docs/specs.pdf).
 
+The documentation, generated with `rust-doc` may be found [here](doc/proost/).
 
-### Development environment
-With `nix` installed, simply type `nix develop`. This provides an environment
-with all the necessary tools, including `clippy` and `rustfmt`. There, it is
-possible to run the usual `cargo build` and so on.
+### Usage 
+Please see the specification for insights on how to use `proost` and `tilleul`.
 
-Please consider the syntax `nix develop --profile <a-file-of-your-choosing>`, which
-will prevent the garbage collection of the development dependencies.
+### Build and install
+With `nix` installed, simply type `nix run git+ssh://git@gitlab.crans.org/loutr/proost.git?ref=main` to launch `proost`. Alternatively, clone this git repository and type `nix build` to perform a build and have it in the nix store. One can also type `nix profile install` in the repo to install `proost` to one's profile and use it everywhere!
 
+### Development environment
+With `nix` installed, simply type `nix develop`. This provides an environment with all the necessary tools, including `clippy` and `rustfmt`. There, it is possible to run the usual `cargo build` and so on.
 
-### Build and install
-With `nix` installed, type `nix build` to perform a build and have it in the nix
-store. One can also type `nix profile install` in the repo to install *proost*
-to one's profile and use it everywhere!
+Please consider the syntax `nix develop --profile <a-file-of-your-choosing>`, which will prevent the garbage collection of the development dependencies.
+
+### Crates dependencies
+```mermaid
+graph TD;
+  kernel-->tilleul;
+  kernel-->parser;
+  parser-->tilleul; 
+  parser-->proost;
+  kernel-->proost;
+```

proost/Cargo.toml

@@ -12,6 +12,7 @@ parser.path = "../parser"
 
 anyhow.workspace = true
 clap.workspace = true
-
-colored = "2"
-rustyline = "10.0.0"
+atty.workspace = true
+colored.workspace = true
+rustyline.workspace = true
+rustyline-derive.workspace = true

proost/src/main.rs

 #![feature(box_syntax)]
+#![feature(let_chains)]
 
 mod process;
+mod rustyline_helper;
 
+use std::fs;
+
+use atty::Stream;
 use clap::Parser;
+use rustyline::error::ReadlineError;
+use rustyline::{Cmd, Editor, EventHandler, KeyCode, KeyEvent, Modifiers, Result};
+use rustyline_helper::*;
+
 use kernel::Environment;
 use process::*;
-use rustyline::error::ReadlineError;
-use rustyline::Editor;
-use std::error::Error;
-use std::fs;
 
-// clap configuration
 #[derive(Parser)]
 #[command(author, version, about, long_about = None)]
 struct Args {
+    /// some .mdln files
     files: Vec<String>,
+    /// remove syntax highlighting
+    #[arg(long)]
+    no_color: bool,
 }
 
-// constants fetching
 const VERSION: &str = env!("CARGO_PKG_VERSION");
 const NAME: &str = env!("CARGO_PKG_NAME");
 
-fn main() -> Result<(), Box<dyn Error>> {
+fn main() -> Result<()> {
     let args = Args::parse();
 
+    // check if files are inputed
     if !args.files.is_empty() {
         for path in args.files.iter() {
             match fs::read_to_string(path) {
@@ -36,8 +44,22 @@ fn main() -> Result<(), Box<dyn Error>> {
         return Ok(());
     }
 
-    let mut rl_err: Option<ReadlineError> = None;
-    let mut rl = Editor::<()>::new()?;
+    // check if we are in a terminal
+    if atty::isnt(Stream::Stdout) || atty::isnt(Stream::Stdin) {
+        return Ok(());
+    }
+
+    let helper = RustyLineHelper::new(!args.no_color);
+    let mut rl = Editor::<RustyLineHelper>::new()?;
+    rl.set_helper(Some(helper));
+    rl.bind_sequence(
+        KeyEvent::from('\t'),
+        EventHandler::Conditional(Box::new(TabEventHandler)),
+    );
+    rl.bind_sequence(
+        KeyEvent(KeyCode::Enter, Modifiers::ALT),
+        EventHandler::Simple(Cmd::Newline),
+    );
     println!("Welcome to {} {}", NAME, VERSION);
 
     let mut env = Environment::new();
@@ -52,14 +74,8 @@ fn main() -> Result<(), Box<dyn Error>> {
             Ok(_) => (),
             Err(ReadlineError::Interrupted) => {}
             Err(ReadlineError::Eof) => break,
-            Err(err) => {
-                rl_err = Some(err);
-                break;
-            }
+            Err(err) => return Err(err),
         }
     }
-    match rl_err {
-        None => Ok(()),
-        Some(err) => Err(box err),
-    }
+    Ok(())
 }

proost/src/rustyline_helper.rs

+use colored::*;
+use rustyline::completion::{Completer, FilenameCompleter, Pair};
+use rustyline::highlight::Highlighter;
+use rustyline::hint::HistoryHinter;
+use rustyline::validate::{ValidationContext, ValidationResult, Validator};
+use rustyline::{Cmd, ConditionalEventHandler, Context, Event, EventContext, RepeatCount, Result};
+use rustyline_derive::{Helper, Hinter};
+use std::borrow::Cow::{self, Borrowed, Owned};
+
+/// Language keywords that should be highligted
+const KEYWORDS: [&str; 4] = ["check", "def", "eval", "import"];
+
+/// An Helper for a RustyLine Editor that implements:
+/// - a standard hinter
+/// - customs validator, completer and highlighter
+#[derive(Helper, Hinter)]
+pub struct RustyLineHelper {
+    color: bool,
+    completer: FilenameCompleter,
+    #[rustyline(Hinter)]
+    hinter: HistoryHinter,
+}
+
+impl RustyLineHelper {
+    pub fn new(color: bool) -> Self {
+        Self {
+            color,
+            completer: FilenameCompleter::new(),
+            hinter: HistoryHinter {},
+        }
+    }
+}
+
+/// An Handler for the tab event
+pub struct TabEventHandler;
+impl ConditionalEventHandler for TabEventHandler {
+    fn handle(&self, _: &Event, n: RepeatCount, _: bool, ctx: &EventContext) -> Option<Cmd> {
+        if ctx.line().starts_with("import") {
+            return None;
+        }
+        Some(Cmd::Insert(n, "  ".to_string()))
+    }
+}
+
+/// A variation of FilenameCompleter:
+/// file completion is available only after having typed import
+impl Completer for RustyLineHelper {
+    type Candidate = Pair;
+
+    fn complete(&self, line: &str, pos: usize, _ctx: &Context<'_>) -> Result<(usize, Vec<Pair>)> {
+        if line.starts_with("import") {
+            self.completer.complete_path(line, pos)
+        } else {
+            Ok(Default::default())
+        }
+    }
+}
+
+/// A variation of MatchingBracketValidator:
+/// no validation occurs when entering the import command
+impl Validator for RustyLineHelper {
+    fn validate(&self, ctx: &mut ValidationContext) -> Result<ValidationResult> {
+        if ctx.input().starts_with("import") {
+            return Ok(ValidationResult::Valid(None));
+        }
+
+        Ok(validate_arrows(ctx.input())
+            .or_else(|| validate_brackets(ctx.input()))
+            .unwrap_or(ValidationResult::Valid(None)))
+    }
+}
+
+fn validate_arrows(input: &str) -> Option<ValidationResult> {
+    let mut iter = input.as_bytes().iter().rev();
+
+    if let Some(b) = iter.find(|b| **b != b' ') {
+        if *b == b'>' && let Some(b) = iter.next() && (*b == b'-' || *b == b'=') {
+            return Some(ValidationResult::Incomplete)
+        }
+    }
+
+    None
+}
+
+fn validate_brackets(input: &str) -> Option<ValidationResult> {
+    let mut stack = vec![];
+
+    for c in input.chars() {
+        match c {
+            '(' => stack.push(c),
+            ')' => match stack.pop() {
+                Some('(') => {}
+                Some(_) => {
+                    return Some(ValidationResult::Invalid(Some(
+                        "\nMismatched brackets: ) is not properly closed".to_string(),
+                    )))
+                }
+                None => {
+                    return Some(ValidationResult::Invalid(Some(
+                        "\nMismatched brackets: ( is unpaired".to_string(),
+                    )))
+                }
+            },
+            _ => {}
+        }
+    }
+
+    if stack.is_empty() {
+        None
+    } else {
+        Some(ValidationResult::Incomplete)
+    }
+}
+
+/// A variation of MatchingBrackerHighlighter:
+/// no check occurs before cursor
+/// see: https://docs.rs/rustyline/10.0.0/rustyline/highlight/struct.MatchingBracketHighlighter.html
+impl Highlighter for RustyLineHelper {
+    fn highlight_hint<'h>(&self, hint: &'h str) -> Cow<'h, str> {
+        if !self.color {
+            return Owned(hint.to_owned());
+        }
+        Owned(format!("{}", hint.bold()))
+    }
+
+    fn highlight_char(&self, _line: &str, _pos: usize) -> bool {
+        self.color
+    }
+
+    fn highlight<'l>(&self, line: &'l str, pos: usize) -> Cow<'l, str> {
+        if line.len() <= 1 || !self.color {
+            return Borrowed(line);
+        }
+        let mut copy = line.to_owned();
+
+        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);
+                copy.replace_range(pos..=pos, &s.blue().bold());
+            }
+        KEYWORDS
+            .iter()
+            .for_each(|keyword| replace_inplace(&mut copy, keyword, &keyword.blue().bold()));
+        Owned(copy)
+    }
+}
+
+/// Variation of the std replace function that only replace full words
+pub fn replace_inplace(input: &mut String, from: &str, to: &str) {
+    let mut offset = 0;
+    while let Some(pos) = input[offset..].find(from) {
+        if (pos == 0 || input.as_bytes()[offset + pos - 1] == b' ')
+            && (offset + pos + from.len() == input.len()
+                || input.as_bytes()[offset + pos + from.len()] == b' ')
+        {
+            input.replace_range(offset + pos..offset + pos + from.len(), to);
+            offset += pos + to.len();
+        } else {
+            offset += pos + from.len()
+        }
+    }
+}
+
+fn find_matching_bracket(line: &str, pos: usize, bracket: u8) -> Option<(u8, usize)> {
+    let matching_bracket = matching_bracket(bracket);
+    let mut to_match = 1;
+
+    let match_bracket = |b: u8| {
+        if b == matching_bracket {
+            to_match -= 1;
+        } else if b == bracket {
+            to_match += 1;
+        };
+        to_match == 0
+    };
+
+    if is_open_bracket(bracket) {
+        // forward search
+        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))
+    }
+}
+
+/// Check if the cursor is on a bracket
+const fn get_bracket(line: &str, pos: usize) -> Option<(u8, usize)> {
+    if !line.is_empty() && pos < line.len() {
+        let b = line.as_bytes()[pos];
+        if is_bracket(b) {
+            return Some((b, pos));
+        }
+    }
+    None
+}
+
+const fn matching_bracket(bracket: u8) -> u8 {
+    match bracket {
+        b'(' => b')',
+        b')' => b'(',
+        _ => unreachable!(),
+    }
+}
+
+const fn is_bracket(bracket: u8) -> bool {
+    matches!(bracket, b'(' | b')')
+}
+
+const fn is_open_bracket(bracket: u8) -> bool {
+    matches!(bracket, b'(')
+}