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
Commits on Source (8)
Hide whitespace changes
Inline Side-by-side
Showing
with 336 additions and 92 deletions
README.md
View file @ 700811b8
# Proost
<p align="center">
<img src="https://gitlab.crans.org/loutr/proost/-/raw/main/docs/media/logo.png" width="25%"/>
</p>
# Proost
A simple proof assistant written in Rust.
The specification of the project may be found [here](docs/specs.pdf).
The documentation, generated with `rust-doc` may be found [here](doc/proost/).
### Usage
Please see the specification for insights on how to use `proost` and `tilleul`.
The specification of the project may be found [here](docs/specs.pdf), and the
user manual [here](docs/manual.pdf). The API documentation can be found by
clicking on the corresponding badge below the project name.
### 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.
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
To install proost with `nix` installed, simply type:
```sh
nix profile install git+ssh://git@gitlab.crans.org/loutr/proost.git?ref=main
```
A toplevel instance can then be launched with `proost`. Alternatively, replace
`profile install` with `run` to give the program a go without installing it.
Without `nix` installed, `git clone` the project and, with Rust and
[`cargo`](https://doc.rust-lang.org/stable/cargo/) properly setup to an
appropriate version (either through your package manager or
[`rustup`](https://rustup.rs/)), do `cargo run --release`.
## Development environment (with `nix`)
Type `nix develop`. This provides an environment with all the necessary tools,
including `cargo` (with `clippy`, `rustfmt`) and `rust-analyzer`. Then, use your
regular `cargo` commands.
Please consider the syntax `nix develop --profile <a-file-of-your-choosing>`,
which will prevent the garbage collection of the development dependencies as
long as the given file lives.
## Crates
The project is organised as such:
- the crate `kernel` provides an interface for building and manipulating terms,
as well as type inference and type checking functions;
- the crate `parser` provides parsing functions which return `Builder` objects,
which can be seen as template that can be provided to the kernel to get a
real, well-formed term to perform computations upon;
- the crate `proost` provides a toplevel interface for end-users that can be
used to manipulate terms and query the kernel. It provides partial
auto-completion, some color highlighting and other readline-like features;
- the crate `tilleul`, which is still in preparation, which will implement the
Language Server Protocol.
### Crates dependencies
```mermaid
graph TD;
kernel-->tilleul;
kernel-->parser;
kernel-.->parser;
parser-->tilleul;
parser-->proost;
kernel-->proost;
......
docs/manual.pdf 0 → 100644 LFS
View file @ 700811b8
File added
docs/manual.tex 0 → 100644
View file @ 700811b8
\documentclass[twocolumn]{article}
\usepackage[british]{babel}
\usepackage{textcase}% provides \MakeTextUppercase (does not impact math mode)
\usepackage{amssymb, amsmath, amsthm, mathrsfs}
\usepackage{fancyhdr}
\usepackage{listings}
\usepackage{bussproofs} % proof tree
\usepackage[dvipsnames]{xcolor}
\usepackage{graphicx}
\RequirePackage[a4paper, left=2cm, right=2cm, bottom=3cm, top=2.3cm, headsep=100pt]{geometry}
\RequirePackage[small]{titlesec} % Taille des sections réduite
\RequirePackage[pdfborderstyle={/S/U/W 0}]{hyperref} % Le paramètre retire les bordures autour des hyperliens
\author{
Arthur \textsc{Adjedj}\\
Vincent \textsc{Lafeychine} \and
Augustin \textsc{Albert} \\
Lucas \textsc{Tabary-Maujean}
}
\title{
\includegraphics[height=2.5cm]{media/logo}
\textbf{Proost 0.1.0} \\
User manual
\\[1\baselineskip]\normalsize ENS Paris-Saclay
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Listings %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\definecolor{gray}{rgb}{0.5,0.5,0.5}
\definecolor{paleblue}{rgb}{0.7,0.7,1}
\definecolor{darkgray}{rgb}{0.1,0.1,0.1}
\definecolor{dark}{rgb}{0,0,0}
\definecolor{forestgreen}{rgb}{0,0.3,0}
\definecolor{darkred}{rgb}{0.5,0,0}
\lstdefinestyle{default}{
frame=tb,
basicstyle=\ttfamily,
numbers=left,
numbersep=5pt,
xleftmargin=1.5em,
framexleftmargin=1em,
numberstyle=\footnotesize\ttfamily\color{paleblue},
keywordstyle={\bfseries\itshape\color{dark}},
commentstyle=\color{gray},
texcl, % Back to TeX styling within *inline* comments
escapechar=`, % escape character for block comments
%escapebegin=\lst@commentstyle,
breaklines=true,
breakatwhitespace=true
}
\lstdefinestyle{proost}{
alsoletter={//,.,:,=},
style=default,
numberstyle=\scriptsize\ttfamily\color{paleblue},
comment=[l]{//},
keywords={fun, if},
keywordstyle=\color{forestgreen},
keywords=[2]{Prop, Type},
keywordstyle=[2]\color{blue},
keywords=[3]{def, check, eval, search, import},
keywordstyle=[3]\color{darkred},
}
\lstnewenvironment{proost}[1][]{\lstset{style=proost, #1}}{}
\lstset{style=proost}
\lstMakeShortInline[columns=flexible]¤
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% headings %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\pagestyle{fancy}
\renewcommand{\headrulewidth}{0pt}
\renewcommand{\footrulewidth}{0pt}
\fancyhead{}
\fancyfoot[L]{\small{\reflectbox{\copyright} \the\year{}}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% bussproofs settings %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% documentation at https://mirror.ibcp.fr/pub/CTAN/macros/latex/contrib/bussproofs/BussGuide2.pdf
\EnableBpAbbreviations
% Overriding default label style
\def\RL#1{\RightLabel{\footnotesize\bfseries{#1}}}
\def\LL#1{\LeftLabel{\footnotesize\bfseries{#1}}}
% boxed proofs, used to align multiple proofs on a single line
\newenvironment{bprooftree}
{\leavevmode\hbox\bgroup}
{\DisplayProof\egroup}
\newcommand{\textr}[1]{{\footnotesize\textbf{\MakeTextUppercase{#1}}}}
% Fixes alignment issues but not without some consistency issues
\def\RL#1{\RightLabel{\makebox[0pt][l]{\textr{#1}}}}
\def\LL#1{\LeftLabel{\makebox[0pt][r]{\textr{#1}}}}
% consistent label (with width)
\def\cRL#1{\RightLabel{\textr{#1}}}
\def\cLL#1{\LeftLabel{\textr{#1}}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Divers %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\setlength{\columnsep}{20pt} % 10 pt par défaut
\newcommand{\members}[1]{\texorpdfstring{\hfill\scriptsize #1}{}}
\newcommand{\etun}{{\color{Green} ($\star$)} }
\newcommand{\etde}{{\color{Orange} ($\star\star$)} }
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}
\maketitle
\thispagestyle{fancy}
\section{Introduction}
This program provides the user a set of tools to work with \(\lambda\)-terms as
described in the Calculus of Construction. Through the Curry-Howard
correspondence; users may associate a property or theorem they are willing to
prove to a type which can be expressed in CoC. Proving it then corresponds to
constructing a term of that type.
Release 0.1.0 of the project includes a toplevel interface also called
\texttt{proost}, which is the main way users can interact with this piece of
software. For a use directly through the crate APIs, please refer to their
respective documentations.
\section{Toplevel session}
In the toplevel, users are greeted with a prompt. There, they may enter the
following commands:
\begin{itemize}
\item ¤import file1 file2¤ typechecks
and loads the file in the current environment;
\item ¤search v¤ looks for the definition of variable ¤v¤;
\item ¤def a := t¤
defines an alias ¤a¤ that can be used in any following command;
\item ¤def a: ty := t¤ defines an alias ¤a¤ that is checked to
be of type ¤ty¤;
\item ¤check u: t¤ verifies ¤u¤ has type ¤t¤;
\item ¤check u¤ provides the type of ¤u¤;
\item ¤eval u¤ provides the definition of ¤u¤.
\end{itemize}
If the command succeeds, the toplevel returns a green check mark, with an
associated result if there is any. Otherwise, a red cross indicates an error
occurred, next to some details about it. The command is discarded and the user
may enter another command.
The toplevel provides to a certain extent history browsing, either \emph{via}
the up and down arrow keys or some autocompletion from previous commands.
\section{Language}
This release includes no standard library, which means users have to build their
theories from scratch. Besides, this version includes no notion of axioms, which
means terms have to be built from encodings within CoC.
Language syntax is as such:
\begin{itemize}
\item Functions (\(\lambda\)-abstractions) are defined with the keyword ¤fun¤:
¤fun x: A => u¤, ¤fun x y: A => u¤ (both ¤x¤ and ¤y¤ are of type ¤A¤),
¤fun x: A, y: B => u¤ (multiple arguments, where ¤B¤ may depend on ¤x¤);
\item Dependent function types (\(\Pi\)-types) are defined with a pair of parentheses
before an arrow, as in: ¤(x: A) -> B¤, ¤(x y: A) -> B¤ or
¤(x: A, y: B) -> C¤ (where the distinctions are similar to the previous
item. Additionally, there is some usual syntactic sugar when the output
type does not mention the input argument, which corresponds to usual
function types: ¤A -> B¤, ¤A -> B -> C¤ (right-associativity);
\item Function application of two terms ¤u¤ and ¤v¤ is simply written ¤u v¤,
and is left-associative when there are multiple arguments;
\item Variables are regular strings, which may only correspond to bound
variables or previously defined terms;
\item The type of propositions and higher-order types are written ¤Prop¤ and
¤Type i¤, as usual.
\end{itemize}
This release includes a single example file \texttt{contraposition.mdln} which
defines elementary propositional calculus operators and their constructors.
\end{document}
docs/media/logo.png 0 → 100644 LFS
View file @ 700811b8
docs/media/logo.png

131 B

docs/proost.png → docs/media/screenshot_toplevel.png LFS
View file @ 700811b8
File moved
docs/specs.pdf LFS
View file @ 700811b8
No preview for this file type
docs/specs.tex
View file @ 700811b8
......@@ -7,7 +7,7 @@
\usepackage{bussproofs} % proof tree
\usepackage[dvipsnames]{xcolor}
\usepackage{graphicx}
\RequirePackage[a4paper, left=2cm, right=2cm, bottom=3cm, headsep=100pt]{geometry}
\RequirePackage[a4paper, left=2cm, right=2cm, bottom=3cm, top=2.3cm, headsep=100pt]{geometry}
\RequirePackage[small]{titlesec} % Taille des sections réduite
\RequirePackage[pdfborderstyle={/S/U/W 0}]{hyperref} % Le paramètre retire les bordures autour des hyperliens
......@@ -18,7 +18,10 @@
Lucas \textsc{Tabary-Maujean}
}
\title{\textbf{Proost: specifications}\\
\title{
\includegraphics[height=2.5cm]{media/logo}
\textbf{Proost: specifications}\\
\large A small proof assistant written in Rust
\\[1\baselineskip]\normalsize ENS Paris-Saclay
}
......@@ -54,9 +57,9 @@
comment=[l]{//},
keywords={fun, if},
keywordstyle=\color{forestgreen},
keywords={Prop, Type},
keywordstyle=\color{darkred},
keywords=[3]{def, check, eval, import},
keywords=[2]{Prop, Type},
keywordstyle=[2]\color{darkred},
keywords=[3]{def, check, eval, search, import},
keywordstyle=[3]\color{darkred},
}
\lstnewenvironment{proost}[1][]{\lstset{style=proost, #1}}{}
......@@ -100,8 +103,8 @@
\newcommand{\members}[1]{\texorpdfstring{\hfill\scriptsize #1}{}}
\newcommand{\etun}{({\color{Green} $\star$}) }
\newcommand{\etde}{({\color{Orange} $\star\star$}) }
\newcommand{\etun}{{\color{Green} ($\star$)} }
\newcommand{\etde}{{\color{Orange} ($\star\star$)} }
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......@@ -112,42 +115,50 @@
\emph{
This project is under development, and its specifications themselves are
subject to changes, should time be an issue or a general consensus be reached
to change the purposes of the tool. An example of that is the syntax of
the language, which is still largely unstable.
}
to change the purposes of the tool. An example of that is the syntax of the
language, which is still largely unstable. }
\section{General purpose and functions}
This project aims at providing a small tool for typechecking expressions written in
the language of the Calculus of Construction (CoC). This tool shall be
both terminal and editor based through the \texttt{proost} program that provides both compiler and toplevel-like capacities and options and a LSP called \texttt{tilleul}.
The file extension used by both programs is \texttt{.mdln}, which is short for \emph{madelaine}, the name of the language manipulated by users in these files.
\section{General purpose and functions} This project aims at providing a small
tool for typechecking expressions written in the language of the Calculus of
Construction (CoC). This tool shall be both terminal and editor based through
the \texttt{proost} program that provides both compiler and toplevel-like
capacities and options and a LSP called \texttt{tilleul}. The file extension
used by both programs is \texttt{.mdln}, which is short for \emph{madelaine},
the name of the language manipulated by users in these files.
\section{Project structure}
Each category of the project is assigned some or all members of the group,
meaning the designated members will \emph{mainly} make progress in the associated categories
and review the corresponding advancements. Any member may regardless contribute to any part
of the development of the tool.
\section{Project structure} Each category of the project is assigned some or all
members of the group, meaning the designated members will \emph{mainly} make
progress in the associated categories and review the corresponding advancements.
Any member may regardless contribute to any part of the development of the tool.
Some specific categories and items will be added a star \etun or two \etde to
indicate whether they are respectively late requirements (for the last release
due in December)
or extra requirements that will be considered only if there is enough time.
\subsection{Language design \members{all members}}
The \texttt{proost} tool is a simple proof assistant and does not provide any
tactics. As new features arrive from extensions of the kernel type theory, the
\emph{madelaine} language must provide convenient shorthands and notations. The syntax of commands is the following:
due in December) or extra requirements that will be considered only if there is
enough time.
\subsection{Language design \members{all members}} The \texttt{proost} tool is a
simple proof assistant and does not provide any tactics. As new features arrive
from extensions of the kernel type theory, the \emph{madelaine} language must
provide convenient shorthands and notations. The syntax of commands is the
following:
\begin{itemize}
\item \etun¤import relative_path_to_file¤ typecheck and load the the file in the current environment;
\item ¤def a := t¤ defines an alias ¤a¤ that can be used in any following command;
\item ¤def a : ty := t¤ defines an alias ¤a¤ that is checked to be of type ¤ty¤;
\item ¤check u : t¤ verifies ¤u¤ has type ¤t¤;
\item \etun ¤import relative_path_to_file¤ typechecks
and loads the file in the current environment;
\item \etde ¤search t¤ searches ¤t¤ in all known terms, where ¤t¤ may contain
¤_¤ joker identifiers (see section \ref{sec:unification});
\item ¤def a := t¤
defines an alias ¤a¤ that can be used in any following command;
\item ¤def a: ty := t¤ defines an alias ¤a¤ that is checked to
be of type ¤ty¤;
\item ¤check u: t¤ verifies ¤u¤ has type ¤t¤;
\item ¤check u¤ provides the type of ¤u¤;
\item ¤eval u¤ provides the definition of ¤u¤.
\end{itemize}
Below is an overview of the syntax of the terms, both present and future. The syntax is strongly inspired by that of OCaml. Comments are defined using the keyword \texttt{//}.
Below is an overview of the syntax of the terms, including hypothetical
developments. The syntax is strongly inspired by that of OCaml. Comments are
defined using the keyword \texttt{//}.
\vspace{1.2mm}
elementary type theory:
......@@ -156,13 +167,14 @@ elementary type theory:
def Nat :=
(N: Type) -> (N -> N) -> N -> N
def z := fun N:Type =>
fun f:(N -> N), x:N => x
check z : Nat
def z := fun N: Type =>
fun f: (N -> N), x:N => x
check z: Nat
def succ := fun n: Nat, N: Type =>
fun f: (N -> N), x: N => f (n N f x)
check succ : Nat -> Nat
fun f: (N -> N), x: N =>
f (n N f x)
check succ: Nat -> Nat
\end{proost}
\etun universe polymorphism:
......@@ -173,7 +185,7 @@ def foo.{i,j} : Type (max i j) + 1
\etde unification:
\begin{proost}
def comm := \/ x,y, x + y = y + x
def comm := \/x y, x + y = y + x
\end{proost}
\etde existential types:
......@@ -182,26 +194,36 @@ def t := E n, n * n - n + 4 = 0
\end{proost}
\subsection{Toplevel \members{AuA}}
The \texttt{proost} command, when provided with no argument, is expected to behave like a toplevel, akin to \texttt{ocaml} or \texttt{coqtop}. There, user is greeted with a prompt and may enter commands. When provided with existing file paths, ¤proost¤ intends to typecheck them in
order, that is, reading them as successive inputs in the toplevel. Further features for this \emph{might} include a more extended notion of ``modules'' where files may provides scopes.
{
\begin{center}
\fbox{\includegraphics{proost.png}}
\end{center}
}
\subsection{Toplevel \members{AuA}} The \texttt{proost} command, when provided
with no argument, is expected to behave like a toplevel, akin to \texttt{ocaml}
or \texttt{coqtop}. There, user is greeted with a prompt and may enter commands.
When provided with existing file paths, ¤proost¤ intends to typecheck them in
order, that is, reading them as successive inputs in the toplevel. Further
features for this \emph{might} include a more extended notion of ``modules''
where files may provides scopes.
\begin{center}
\fbox{\includegraphics{media/screenshot_toplevel}}
\end{center}
\subsection{\etun LSP \members{VL}}
\texttt{tilleul} shall provide an implementation of the Language Server Protocol in order to provide linting and feedback during an editing session.
\texttt{tilleul} shall provide an
implementation of the Language Server Protocol in order to provide linting and
feedback during an editing session.
\subsection{Parsing \members{AuA}}
The parsing approach is straightforward and relies on external libraries. The parser is expected to keep adapting to changes made in the term definitions and unification capability. The parser is thoroughly tested to guarantee full coverage.
The parsing approach is straightforward and
relies on external libraries. The parser is expected to keep adapting to changes
made in the term definitions and unification capability. The parser is
thoroughly tested to guarantee full coverage.
\subsection{Kernel \members{all members}}
The kernel manipulates \(\lambda\)-terms in the Calculus of Construction and is expected to store and manage them with a relative level of efficiency. The type theory used to build the terms will be successively extended with:
The kernel manipulates
\(\lambda\)-terms in the Calculus of Construction and is expected to store and
manage them with a relative level of efficiency. The type theory used to build
the terms will be successively extended with:
\begin{itemize}
\item abstractions, \(\Pi\)-types, predicative universes with \(\mathsf{Prop}\);
\item \etun universe polymorphism;
......@@ -212,8 +234,9 @@ The kernel manipulates \(\lambda\)-terms in the Calculus of Construction and is
\subsection{\etun Optimisation \members{ArA LTM}}
Extra care must be put into designing an efficient memory management model for
the kernel, along with satisfactory typing and reduction algorithms.
Extra care must be put into
designing an efficient memory management model for the kernel, along with
satisfactory typing and reduction algorithms.
In particular, the first iteration of the program manipulates directly terms on
the heap, with no particular optimisation: every algorithm is applied soundly
......@@ -221,24 +244,26 @@ but naively.
A first refactor of the memory model includes using a common memory location for
terms, ensuring invariant like unicity of a term in memory, providing laziness
and storing results of the most expensive functions \emph{(memoizing)}.
This model also provides stronger isolation properties, preventing several
memory pools (\emph{arena} is the technical term used in the project) from
interacting with one another.
and storing results of the most expensive functions \emph{(memoizing)}. This
model also provides stronger isolation properties, preventing several memory
pools (\emph{arena} is the technical term used in the project) from interacting
with one another.
This can
be further extended with other invariants like ensuring every term in memory is
in weak head normal form.
This can be further extended with other invariants like ensuring every term in
memory is in weak head normal form.
\subsection{\etde Unification}
Early versions of the tool may require the user to explicit every type at play.
Successive versions may gradually include unification tools (meta-variables)
of better quality to assist the user and alleviate some of their typing-annotation
burden.
\subsection{\etde Unification}\label{sec:unification}
Early versions of the tool may require the user
to explicit every type at play. Successive versions may gradually include
unification tools (meta-variables) of better quality to assist the user and
alleviate some of their typing-annotation burden.
\subsection{Developpement tools \members{VL LTM}}
Tests are mandatory in every part of the project. A tool originally developed by the Mozilla team was modified to allow for a more precise branch coverage of the project.
The Nix framework is used to automatically build and package the application as well as generating a docker image and providing developers tools of the same version.
Tests are mandatory in every
part of the project. A tool originally developed by the Mozilla team was
modified to allow for a more precise branch coverage of the project. The Nix
framework is used to automatically build and package the application as well as
generating a docker image and providing developers tools of the same version.
% TODO elaborate, maybe
\end{document}
kernel/src/lib.rs
View file @ 700811b8
#![doc(html_logo_url = "https://gitlab.crans.org/loutr/proost/-/raw/main/docs/media/logo.png")]
//! A kernel for the calculus of constructions.
//!
//! Terms can be built with functions from the [`term`] module. This module also provides essential
......
parser/src/lib.rs
View file @ 700811b8
#![doc(html_logo_url = "https://gitlab.crans.org/loutr/proost/-/raw/main/docs/media/logo.png")]
//! Fast parser for λ-terms and commands using pest.
//! Provides functions to parse files and single commands.
......
proost/src/main.rs
View file @ 700811b8
#![doc(html_logo_url = "https://gitlab.crans.org/loutr/proost/-/raw/main/docs/media/logo.png")]
#![feature(let_chains)]
mod error;
......
proost/src/rustyline_helper.rs
View file @ 700811b8
......@@ -12,8 +12,8 @@ use rustyline_derive::{Helper, Hinter};
const KEYWORDS: [&str; 5] = ["check", "def", "eval", "import", "search"];
/// An Helper for a RustyLine Editor that implements:
/// - a standard hinter
/// - customs validator, completer and highlighter
/// - a standard hinter;
/// - custom validator, completer and highlighter.
#[derive(Helper, Hinter)]
pub struct RustyLineHelper {
color: bool,
......@@ -43,7 +43,7 @@ impl ConditionalEventHandler for TabEventHandler {
}
}
/// A variation of FilenameCompleter:
/// 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,8 +53,9 @@ impl Completer for RustyLineHelper {
}
}
/// A variation of MatchingBracketValidator:
/// no validation occurs when entering the import command
/// 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 {
fn validate(&self, ctx: &mut ValidationContext) -> Result<ValidationResult> {
if ctx.input().starts_with("import") {
......@@ -97,15 +98,15 @@ fn validate_brackets(input: &str) -> Option<ValidationResult> {
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
/// 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> {
if !self.color {
return Owned(hint.to_owned());
}
Owned(format!("{}", hint.bold()))
Owned(format!("{}", hint.bright_black()))
}
fn highlight_char(&self, _line: &str, _pos: usize) -> bool {
......