From bbdd1df8545c3736ac2a1bab9567cb706c2002c2 Mon Sep 17 00:00:00 2001
From: v-lafeychine <vincent.lafeychine@proton.me>
Date: Sun, 4 Dec 2022 19:00:27 +0100
Subject: [PATCH] =?UTF-8?q?Resolve=20"Infrastructure=20improvement"=20?=
=?UTF-8?q?=E2=9C=A8=EF=B8=8F=20Closes=20#40=20=F0=9F=90=94=EF=B8=8F?=
=?UTF-8?q?=F0=9F=91=8D=EF=B8=8F=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
🦀ï¸ðŸ°ðŸ¦€ï¸ðŸ°ðŸ¦€ï¸ðŸ°
* chore(fmt): Modify format
* chore(coverage): Tune branch + Include no_coverage feature
* bump: Update pest to 2.5.1 and subdependencies
* feat(cargo): Add licence check
---
.gitlab-ci.yml | 13 ++-
.rustfmt.toml | 26 +++++
Cargo.lock | 28 ++---
deny.toml | 33 ++++++
flake.nix | 19 ++--
kernel/src/lib.rs | 1 +
kernel/src/term/arena.rs | 18 +--
kernel/src/term/builders.rs | 64 +++--------
kernel/src/term/calculus.rs | 132 +++++-----------------
kernel/src/type_checker.rs | 201 +++++++--------------------------
kernel/tests/and.rs | 30 +----
parser/src/command.rs | 2 +-
parser/src/parser.rs | 187 ++++++++----------------------
proost/src/evaluator.rs | 52 ++++-----
proost/src/main.rs | 32 ++----
proost/src/rustyline_helper.rs | 55 +++------
16 files changed, 280 insertions(+), 613 deletions(-)
create mode 100644 .rustfmt.toml
create mode 100644 deny.toml
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 71ae2cef..ba8c3e61 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -23,6 +23,7 @@ format:
stage: check
cache: []
script:
+ - cargo deny check
- cargo fmt --check
lint:
@@ -39,9 +40,11 @@ tests:
stage: tests
variables:
CARGO_INCREMENTAL: 0
- EXCL_LINE: "//!|///|#\\[|use|unreachable!"
- EXCL_BR_LINE: "#\\[|unreachable!|assert(_eq)?!|^(pub |pub(crate) )?(enum|struct)|^[[:space:]]*\\}(,)?$"
- EXCL_BR_START: "^(pub |pub(crate) )?(enum|struct) [[:alpha:]]+ \\{"
+ EXCL_LINE: "#\\[|use|unreachable!|^(pub |pub(crate) )?(enum|struct)"
+ EXCL_START: "^(pub |pub(crate) )?(enum|struct) ([[:alpha:]]|[[:space:]]|[<>',])+\\{"
+ EXCL_STOP: "^\\}"
+ EXCL_BR_LINE: "#\\[|assert(_eq)?!|^(pub |pub(crate) )?(enum|struct)|^[[:space:]]*\\}(,)?$"
+ EXCL_BR_START: "#\\[no_coverage\\]|^mod tests \\{|^(pub |pub(crate) )?(enum|struct) ([[:alpha:]]|[[:space:]]|[<>',])+\\{"
EXCL_BR_STOP: "^\\}"
RUSTDOCFLAGS: "${RUSTFLAGS}"
RUSTFLAGS: "-Zprofile -Ccodegen-units=1 -Copt-level=0 -Clink-dead-code -Coverflow-checks=off -Zpanic_abort_tests -Cpanic=abort"
@@ -54,9 +57,9 @@ tests:
script:
- cargo test
- - grcov . -s . -b ./target/debug/ --branch --ignore-not-existing --excl-line "${EXCL_LINE}" --excl-br-line "${EXCL_BR_LINE}" --excl-br-start "${EXCL_BR_START}" --excl-br-stop "${EXCL_BR_STOP}" --ignore "*cargo*" -t cobertura -o ./coverage_raw.xml &&
+ - grcov . -s . -b ./target/debug/ --branch --llvm --ignore-not-existing --excl-line "${EXCL_LINE}" --excl-start "${EXCL_START}" --excl-stop "${EXCL_STOP}" --excl-br-line "${EXCL_BR_LINE}" --excl-br-start "${EXCL_BR_START}" --excl-br-stop "${EXCL_BR_STOP}" --ignore "*cargo*" -t cobertura -o ./coverage_raw.xml &&
xsltproc --novalid --output ./coverage.xml ./.gitlab-cov.xsl ./coverage_raw.xml || true
- - grcov . -s . -b ./target/debug/ --branch --ignore-not-existing --excl-line "${EXCL_LINE}" --excl-br-line "${EXCL_BR_LINE}" --excl-br-start "${EXCL_BR_START}" --excl-br-stop "${EXCL_BR_STOP}" --ignore "*cargo*" -t lcov -o ./coverage.lcov &&
+ - grcov . -s . -b ./target/debug/ --branch --llvm --ignore-not-existing --excl-line "${EXCL_LINE}" --excl-start "${EXCL_START}" --excl-stop "${EXCL_STOP}" --excl-br-line "${EXCL_BR_LINE}" --excl-br-start "${EXCL_BR_START}" --excl-br-stop "${EXCL_BR_STOP}" --ignore "*cargo*" -t lcov -o ./coverage.lcov &&
genhtml --branch --no-function-coverage --precision 2 ./coverage.lcov -o ./coverage || true
- *push-zamok
diff --git a/.rustfmt.toml b/.rustfmt.toml
new file mode 100644
index 00000000..42c9b67f
--- /dev/null
+++ b/.rustfmt.toml
@@ -0,0 +1,26 @@
+edition = "2021"
+version = "Two"
+required_version = "1.5.1"
+
+# Enable features
+format_code_in_doc_comments = true
+normalize_doc_attributes = true
+reorder_impl_items = true
+wrap_comments = true
+
+# Set the width of lines
+comment_width = 132
+max_width = 132
+use_small_heuristics = "Max"
+
+# Specific width
+struct_lit_width=18
+struct_variant_width=35
+
+# Import handling
+group_imports = "StdExternalCrate"
+imports_granularity = "Module"
+
+# Stylish choices
+match_block_trailing_comma = true
+overflow_delimited_expr = true
diff --git a/Cargo.lock b/Cargo.lock
index b9bbfc39..de4781df 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -337,9 +337,9 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646"
[[package]]
name = "libc"
-version = "0.2.137"
+version = "0.2.138"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fc7fcc620a3bff7cdd7a365be3376c97191aeaccc2a603e600951e452615bf89"
+checksum = "db6d7e329c562c5dfab7a46a2afabc8b987ab9a4834c9d1ca04dc54c1546cef8"
[[package]]
name = "linux-raw-sys"
@@ -373,9 +373,9 @@ dependencies = [
[[package]]
name = "nix"
-version = "0.24.2"
+version = "0.24.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "195cdbc1741b8134346d515b3a56a1c94b0912758009cfd53f99ea0f57b065fc"
+checksum = "fa52e972a9a719cecb6864fb88568781eb706bac2cd1d4f04a648542dbf78069"
dependencies = [
"bitflags",
"cfg-if",
@@ -455,9 +455,9 @@ dependencies = [
[[package]]
name = "pest"
-version = "2.5.0"
+version = "2.5.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5f400b0f7905bf702f9f3dc3df5a121b16c54e9e8012c082905fdf09a931861a"
+checksum = "cc8bed3549e0f9b0a2a78bf7c0018237a2cdf085eecbbc048e52612438e4e9d0"
dependencies = [
"thiserror",
"ucd-trie",
@@ -465,9 +465,9 @@ dependencies = [
[[package]]
name = "pest_derive"
-version = "2.5.0"
+version = "2.5.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "423c2ba011d6e27b02b482a3707c773d19aec65cc024637aec44e19652e66f63"
+checksum = "cdc078600d06ff90d4ed238f0119d84ab5d43dbaad278b0e33a8820293b32344"
dependencies = [
"pest",
"pest_generator",
@@ -475,9 +475,9 @@ dependencies = [
[[package]]
name = "pest_generator"
-version = "2.5.0"
+version = "2.5.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3e64e6c2c85031c02fdbd9e5c72845445ca0a724d419aa0bc068ac620c9935c1"
+checksum = "28a1af60b1c4148bb269006a750cff8e2ea36aff34d2d96cf7be0b14d1bed23c"
dependencies = [
"pest",
"pest_meta",
@@ -488,9 +488,9 @@ dependencies = [
[[package]]
name = "pest_meta"
-version = "2.5.0"
+version = "2.5.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "57959b91f0a133f89a68be874a5c88ed689c19cd729ecdb5d762ebf16c64d662"
+checksum = "fec8605d59fc2ae0c6c1aefc0c7c7a9769732017c0ce07f7a9cfffa7b4404f20"
dependencies = [
"once_cell",
"pest",
@@ -709,9 +709,9 @@ checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623"
[[package]]
name = "syn"
-version = "1.0.104"
+version = "1.0.105"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4ae548ec36cf198c0ef7710d3c230987c2d6d7bd98ad6edc0274462724c585ce"
+checksum = "60b9b43d45702de4c839cb9b51d9f529c5dd26a4aff255b42b1ebc03e88ee908"
dependencies = [
"proc-macro2",
"quote",
diff --git a/deny.toml b/deny.toml
new file mode 100644
index 00000000..e4ea44ff
--- /dev/null
+++ b/deny.toml
@@ -0,0 +1,33 @@
+all-features = true
+targets = [
+ { triple = "x86_64-unknown-linux-gnu" },
+]
+
+[advisories]
+notice = "deny"
+unmaintained = "deny"
+unsound = "deny"
+vulnerability = "deny"
+yanked = "deny"
+
+ignore = [
+ # atty: Dependency of `clap` and `colored`
+ "RUSTSEC-2021-0145"
+]
+
+[bans]
+multiple-versions = "deny"
+
+[licenses]
+allow-osi-fsf-free = "both"
+confidence-threshold = 1
+copyleft = "allow"
+default = "deny"
+unlicensed = "deny"
+
+exceptions = [
+ { allow = ["Unicode-DFS-2016"], name = "unicode-ident", version = "*" },
+]
+
+[sources]
+unknown-registry = "deny"
diff --git a/flake.nix b/flake.nix
index 6076ce8d..4408d404 100644
--- a/flake.nix
+++ b/flake.nix
@@ -53,8 +53,8 @@
copyToRoot = pkgs.buildEnv {
name = "proost-dependencies";
- paths = (with pkgs; [ coreutils gcc gnugrep gnused grcov lcov libxslt openssh rsync rust-ci ])
- ++ (with pkgs.dockerTools; [ binSh caCertificates fakeNss ]);
+ paths = (with pkgs; [ cargo-deny coreutils gcc gnugrep gnused grcov lcov libxslt openssh rsync ])
+ ++ (with pkgs.dockerTools; [ binSh caCertificates fakeNss ]) ++ [ rust-ci ];
pathsToLink = [ "/bin" "/etc" ];
};
@@ -70,17 +70,20 @@
commands = [{
name = "coverage";
command = let
- excl_line = "//!|///|#\\[|use|unreachable!";
- excl_br_line = "#\\[|unreachable!|assert(_eq)?!|^(pub |pub(crate) )?(enum|struct)|^[[:space:]]*\\}(,)?$";
- excl_br_start = "^(pub |pub(crate) )?(enum|struct) [[:alpha:]]+ \\{";
+ excl_line = "#\\[|use|unreachable!|^(pub |pub(crate) )?(enum|struct)";
+ excl_start = "^(pub |pub(crate) )?(enum|struct) ([[:alpha:]]|[[:space:]]|[<>',])+\\{";
+ excl_stop = "^\\}";
+ excl_br_line = "#\\[|assert(_eq)?!|^(pub |pub(crate) )?(enum|struct)|^[[:space:]]*\\}(,)?$";
+ excl_br_start = "#\\[no_coverage\\]|^mod tests \\{|^(pub |pub(crate) )?(enum|struct) ([[:alpha:]]|[[:space:]]|[<>',])+\\{";
excl_br_stop = "^\\}";
env = "CARGO_INCREMENTAL=0"
+ " RUSTFLAGS=\"-Zprofile -Ccodegen-units=1 -Copt-level=0 -Clink-dead-code -Coverflow-checks=off -Zpanic_abort_tests -Cpanic=abort\""
+ " RUSTDOCFLAGS=\"-Cpanic=abort\"";
in ''
${env} cargo test
- grcov . -s . -b ./target/debug/ --branch --ignore '*cargo*' --ignore-not-existing \
- --excl-line "${excl_line}" --excl-br-line "${excl_br_line}" --excl-br-start "${excl_br_start}" --excl-br-stop "${excl_br_stop}" \
+ grcov . -s . -b ./target/debug/ --branch --llvm --ignore '*cargo*' --ignore-not-existing \
+ --excl-line "${excl_line}" --excl-start "${excl_start}" --excl-stop "${excl_stop}" \
+ --excl-br-line "${excl_br_line}" --excl-br-start "${excl_br_start}" --excl-br-stop "${excl_br_stop}" \
-o ./target/coverage.lcov --log /dev/null || true
find target \( -name "*.gcda" -or -name "*.gcno" \) -delete
genhtml --branch --no-function-coverage --precision 2 target/coverage.lcov -o coverage
@@ -88,7 +91,7 @@
help = "Launch tests and generate HTML coverage website";
}];
- packages = with pkgs; [ grcov lcov rust-dev ];
+ packages = with pkgs; [ cargo-deny grcov lcov rust-dev ];
};
});
}
diff --git a/kernel/src/lib.rs b/kernel/src/lib.rs
index 04069a2d..19c5a3ed 100644
--- a/kernel/src/lib.rs
+++ b/kernel/src/lib.rs
@@ -4,6 +4,7 @@
//! manipulation functions from lambda-calculus, while the [`type_checker`] module provides typed
//! interactions.
+#![feature(no_coverage)]
#![feature(once_cell)]
#![feature(trait_alias)]
diff --git a/kernel/src/term/arena.rs b/kernel/src/term/arena.rs
index f37a9ac1..620eaed7 100644
--- a/kernel/src/term/arena.rs
+++ b/kernel/src/term/arena.rs
@@ -16,9 +16,7 @@ use num_bigint::BigUint;
use crate::error::ResultTerm;
/// An index used to designate bound variables.
-#[derive(
- Add, Copy, Clone, Debug, Default, Display, Eq, PartialEq, From, Into, Sub, PartialOrd, Ord, Hash,
-)]
+#[derive(Add, Copy, Clone, Debug, Default, Display, PartialEq, Eq, Hash, From, Into, PartialOrd, Ord, Sub)]
pub struct DeBruijnIndex(usize);
/// A level of universe, used to build terms of the form `Type i`.
@@ -27,7 +25,7 @@ pub struct DeBruijnIndex(usize);
/// of which is to give a hierarchy to these types, so as to preserve soundness against paradoxes
/// akin to Russell's. Universe levels can be arbitrarily large, and, with good faith, they are
/// represented with *big unsigned integers*, limited only by the memory of the operating computer.
-#[derive(Add, Clone, Debug, Default, Display, Eq, From, Sub, PartialEq, PartialOrd, Ord, Hash)]
+#[derive(Add, Clone, Debug, Default, Display, PartialEq, Eq, From, Hash, PartialOrd, Ord, Sub)]
pub struct UniverseLevel(BigUint);
/// A comprehensive memory management unit for terms.
@@ -199,7 +197,7 @@ impl<'arena> Arena<'arena> {
let addr = self.alloc.alloc(new_node);
self.hashcons.insert(addr);
Term(addr, PhantomData)
- }
+ },
}
}
@@ -245,11 +243,7 @@ impl<'arena> Arena<'arena> {
}
/// Returns the result of the substitution described by the key, lazily computing the closure `f`.
- pub(crate) fn get_subst_or_init<F>(
- &mut self,
- key: &(Term<'arena>, Term<'arena>, usize),
- f: F,
- ) -> Term<'arena>
+ pub(crate) fn get_subst_or_init<F>(&mut self, key: &(Term<'arena>, Term<'arena>, usize), f: F) -> Term<'arena>
where
F: FnOnce(&mut Self) -> Term<'arena>,
{
@@ -259,7 +253,7 @@ impl<'arena> Arena<'arena> {
let res = f(self);
self.mem_subst.insert(*key, res);
res
- }
+ },
}
}
}
@@ -294,7 +288,7 @@ impl<'arena> Term<'arena> {
/// match *t {
/// Abs(_, t2) => arena.beta_reduction(t2),
/// App(t1, _) => t1,
-/// _ => t
+/// _ => t,
/// }
/// # ;})
/// ```
diff --git a/kernel/src/term/builders.rs b/kernel/src/term/builders.rs
index 5bdd062a..ffa91ff5 100644
--- a/kernel/src/term/builders.rs
+++ b/kernel/src/term/builders.rs
@@ -87,20 +87,14 @@ pub const fn type_<'build, 'arena>(level: UniverseLevel) -> impl BuilderTrait<'b
#[inline]
pub const fn type_usize<'build, 'arena>(level: usize) -> impl BuilderTrait<'build, 'arena> {
use num_bigint::BigUint;
- move |arena: &mut Arena<'arena>, _: &Environment<'build, 'arena>, _| {
- Ok(arena.type_(BigUint::from(level).into()))
- }
+ move |arena: &mut Arena<'arena>, _: &Environment<'build, 'arena>, _| Ok(arena.type_(BigUint::from(level).into()))
}
/// Returns a closure building the application of two terms built from the given closures `u1` and
/// `u2`.
#[inline]
-pub const fn app<
- 'build,
- 'arena,
- F1: BuilderTrait<'build, 'arena>,
- F2: BuilderTrait<'build, 'arena>,
->(
+#[no_coverage]
+pub const fn app<'build, 'arena, F1: BuilderTrait<'build, 'arena>, F2: BuilderTrait<'build, 'arena>>(
u1: F1,
u2: F2,
) -> impl BuilderTrait<'build, 'arena> {
@@ -114,12 +108,8 @@ pub const fn app<
/// Returns a closure building the lambda-abstraction with a body built from `body` and an argument
/// type from `arg_type`.
#[inline]
-pub const fn abs<
- 'build,
- 'arena,
- F1: BuilderTrait<'build, 'arena>,
- F2: BuilderTrait<'build, 'arena>,
->(
+#[no_coverage]
+pub const fn abs<'build, 'arena, F1: BuilderTrait<'build, 'arena>, F2: BuilderTrait<'build, 'arena>>(
name: &'build str,
arg_type: F1,
body: F2,
@@ -135,12 +125,8 @@ pub const fn abs<
/// Returns a closure building the dependant product of a term built from `body` over all elements
/// of the type built from `arg_type`.
#[inline]
-pub const fn prod<
- 'build,
- 'arena,
- F1: BuilderTrait<'build, 'arena>,
- F2: BuilderTrait<'build, 'arena>,
->(
+#[no_coverage]
+pub const fn prod<'build, 'arena, F1: BuilderTrait<'build, 'arena>, F2: BuilderTrait<'build, 'arena>>(
name: &'build str,
arg_type: F1,
body: F2,
@@ -188,9 +174,7 @@ impl<'build> Builder<'build> {
}
fn partial_application<'arena>(&self) -> impl BuilderTrait<'build, 'arena> + '_ {
- |arena: &mut Arena<'arena>, env: &Environment<'build, 'arena>, depth| {
- self.realise_in_context(arena, env, depth)
- }
+ |arena: &mut Arena<'arena>, env: &Environment<'build, 'arena>, depth| self.realise_in_context(arena, env, depth)
}
fn realise_in_context<'arena>(
@@ -204,15 +188,9 @@ impl<'build> Builder<'build> {
Var(s) => var(s)(arena, env, depth),
Type(level) => type_usize(level)(arena, env, depth),
Prop => prop()(arena, env, depth),
- App(ref l, ref r) => {
- app(l.partial_application(), r.partial_application())(arena, env, depth)
- }
- Abs(s, ref arg, ref body) => {
- abs(s, arg.partial_application(), body.partial_application())(arena, env, depth)
- }
- Prod(s, ref arg, ref body) => {
- prod(s, arg.partial_application(), body.partial_application())(arena, env, depth)
- }
+ App(ref l, ref r) => app(l.partial_application(), r.partial_application())(arena, env, depth),
+ Abs(s, ref arg, ref body) => abs(s, arg.partial_application(), body.partial_application())(arena, env, depth),
+ Prod(s, ref arg, ref body) => prod(s, arg.partial_application(), body.partial_application())(arena, env, depth),
}
}
}
@@ -235,10 +213,7 @@ pub(crate) mod raw {
}
}
- pub const fn var<'arena, F: BuilderTrait<'arena>>(
- index: DeBruijnIndex,
- type_: F,
- ) -> impl BuilderTrait<'arena> {
+ pub const fn var<'arena, F: BuilderTrait<'arena>>(index: DeBruijnIndex, type_: F) -> impl BuilderTrait<'arena> {
move |env: &mut Arena<'arena>| {
let ty = type_(env);
env.var(index, ty)
@@ -253,10 +228,7 @@ pub(crate) mod raw {
move |env: &mut Arena<'arena>| env.type_(level)
}
- pub const fn app<'arena, F1: BuilderTrait<'arena>, F2: BuilderTrait<'arena>>(
- u1: F1,
- u2: F2,
- ) -> impl BuilderTrait<'arena> {
+ pub const fn app<'arena, F1: BuilderTrait<'arena>, F2: BuilderTrait<'arena>>(u1: F1, u2: F2) -> impl BuilderTrait<'arena> {
|env: &mut Arena<'arena>| {
let u1 = u1(env);
let u2 = u2(env);
@@ -264,10 +236,7 @@ pub(crate) mod raw {
}
}
- pub const fn abs<'arena, F1: BuilderTrait<'arena>, F2: BuilderTrait<'arena>>(
- u1: F1,
- u2: F2,
- ) -> impl BuilderTrait<'arena> {
+ pub const fn abs<'arena, F1: BuilderTrait<'arena>, F2: BuilderTrait<'arena>>(u1: F1, u2: F2) -> impl BuilderTrait<'arena> {
|env: &mut Arena<'arena>| {
let u1 = u1(env);
let u2 = u2(env);
@@ -275,10 +244,7 @@ pub(crate) mod raw {
}
}
- pub const fn prod<'arena, F1: BuilderTrait<'arena>, F2: BuilderTrait<'arena>>(
- u1: F1,
- u2: F2,
- ) -> impl BuilderTrait<'arena> {
+ pub const fn prod<'arena, F1: BuilderTrait<'arena>, F2: BuilderTrait<'arena>>(u1: F1, u2: F2) -> impl BuilderTrait<'arena> {
|env: &mut Arena<'arena>| {
let u1 = u1(env);
let u2 = u2(env);
diff --git a/kernel/src/term/calculus.rs b/kernel/src/term/calculus.rs
index 0263211c..eee479b4 100644
--- a/kernel/src/term/calculus.rs
+++ b/kernel/src/term/calculus.rs
@@ -3,9 +3,10 @@
//! This module consists of internal utility functions used by the type checker, and correspond to
//! usual functions over lambda-terms. These functions interact appropriately with a given arena.
-use super::arena::{Arena, Payload, Term};
use Payload::*;
+use super::arena::{Arena, Payload, Term};
+
impl<'arena> Arena<'arena> {
/// Apply one step of β-reduction, using the leftmost-outermost evaluation strategy.
pub fn beta_reduction(&mut self, t: Term<'arena>) -> Term<'arena> {
@@ -20,16 +21,16 @@ impl<'arena> Arena<'arena> {
} else {
self.app(t1_new, t2)
}
- }
+ },
},
Abs(arg_type, body) => {
let body = self.beta_reduction(body);
self.abs(arg_type, body)
- }
+ },
Prod(arg_type, body) => {
let body = self.beta_reduction(body);
self.prod(arg_type, body)
- }
+ },
_ => t,
}
}
@@ -43,29 +44,24 @@ impl<'arena> Arena<'arena> {
let t1 = self.shift(t1, offset, depth);
let t2 = self.shift(t2, offset, depth);
self.app(t1, t2)
- }
+ },
Abs(arg_type, body) => {
let arg_type = self.shift(arg_type, offset, depth);
let body = self.shift(body, offset, depth + 1);
self.abs(arg_type, body)
- }
+ },
Prod(arg_type, body) => {
let arg_type = self.shift(arg_type, offset, depth);
let body = self.shift(body, offset, depth + 1);
self.prod(arg_type, body)
- }
+ },
_ => t,
}
}
/// Returns the term `t` where all instances of the variable tracked by `depth` are substituted
/// with `sub`.
- pub(crate) fn substitute(
- &mut self,
- t: Term<'arena>,
- sub: Term<'arena>,
- depth: usize,
- ) -> Term<'arena> {
+ pub(crate) fn substitute(&mut self, t: Term<'arena>, sub: Term<'arena>, depth: usize) -> Term<'arena> {
self.get_subst_or_init(&(t, sub, depth), |arena| match *t {
Var(i, _) if i == depth.into() => arena.shift(sub, depth - 1, 0),
Var(i, type_) if i > depth.into() => arena.var(i - 1.into(), type_),
@@ -73,17 +69,17 @@ impl<'arena> Arena<'arena> {
let l = arena.substitute(l, sub, depth);
let r = arena.substitute(r, sub, depth);
arena.app(l, r)
- }
+ },
Abs(arg_type, body) => {
let arg_type = arena.substitute(arg_type, sub, depth);
let body = arena.substitute(body, sub, depth + 1);
arena.abs(arg_type, body)
- }
+ },
Prod(arg_type, body) => {
let arg_type = arena.substitute(arg_type, sub, depth);
let body = arena.substitute(body, sub, depth + 1);
arena.prod(arg_type, body)
- }
+ },
_ => t,
})
}
@@ -112,10 +108,10 @@ impl<'arena> Arena<'arena> {
let t = self.app(t1, t2);
let t = self.beta_reduction(t);
self.whnf(t)
- }
+ },
_ => t,
}
- }
+ },
_ => t,
})
}
@@ -131,18 +127,10 @@ mod tests {
fn simple_subst() {
use_arena(|arena| {
// λx.(λy.x y) x
- let term = arena.build_raw(abs(
- prop(),
- app(
- abs(prop(), app(var(2.into(), prop()), var(1.into(), prop()))),
- var(1.into(), prop()),
- ),
- ));
+ let term = arena
+ .build_raw(abs(prop(), app(abs(prop(), app(var(2.into(), prop()), var(1.into(), prop()))), var(1.into(), prop()))));
// λx.x x
- let reduced = arena.build_raw(abs(
- prop(),
- app(var(1.into(), prop()), var(1.into(), prop())),
- ));
+ let reduced = arena.build_raw(abs(prop(), app(var(1.into(), prop()), var(1.into(), prop()))));
assert_eq!(arena.beta_reduction(term), reduced);
})
@@ -167,13 +155,7 @@ mod tests {
prop(),
abs(
prop(),
- app(
- var(1.into(), prop()),
- app(
- var(2.into(), prop()),
- var(4.into(), prop()),
- ),
- ),
+ app(var(1.into(), prop()), app(var(2.into(), prop()), var(4.into(), prop()))),
),
),
),
@@ -184,10 +166,7 @@ mod tests {
),
),
),
- abs(
- prop(),
- abs(prop(), app(var(2.into(), prop()), var(1.into(), prop()))),
- ),
+ abs(prop(), abs(prop(), app(var(2.into(), prop()), var(1.into(), prop())))),
));
let term_step_1 = arena.build_raw(abs(
@@ -197,19 +176,10 @@ mod tests {
app(
app(
app(
+ abs(prop(), abs(prop(), app(var(2.into(), prop()), var(1.into(), prop())))),
abs(
prop(),
- abs(prop(), app(var(2.into(), prop()), var(1.into(), prop()))),
- ),
- abs(
- prop(),
- abs(
- prop(),
- app(
- var(1.into(), prop()),
- app(var(2.into(), prop()), var(4.into(), prop())),
- ),
- ),
+ abs(prop(), app(var(1.into(), prop()), app(var(2.into(), prop()), var(4.into(), prop())))),
),
),
abs(prop(), var(2.into(), prop())),
@@ -230,13 +200,7 @@ mod tests {
app(
abs(
prop(),
- abs(
- prop(),
- app(
- var(1.into(), prop()),
- app(var(2.into(), prop()), var(5.into(), prop())),
- ),
- ),
+ abs(prop(), app(var(1.into(), prop()), app(var(2.into(), prop()), var(5.into(), prop())))),
),
var(1.into(), prop()),
),
@@ -254,16 +218,7 @@ mod tests {
prop(),
app(
app(
- abs(
- prop(),
- abs(
- prop(),
- app(
- var(1.into(), prop()),
- app(var(2.into(), prop()), var(4.into(), prop())),
- ),
- ),
- ),
+ abs(prop(), abs(prop(), app(var(1.into(), prop()), app(var(2.into(), prop()), var(4.into(), prop()))))),
abs(prop(), var(2.into(), prop())),
),
abs(prop(), var(1.into(), prop())),
@@ -276,13 +231,7 @@ mod tests {
abs(
prop(),
app(
- abs(
- prop(),
- app(
- var(1.into(), prop()),
- app(abs(prop(), var(3.into(), prop())), var(3.into(), prop())),
- ),
- ),
+ abs(prop(), app(var(1.into(), prop()), app(abs(prop(), var(3.into(), prop())), var(3.into(), prop())))),
abs(prop(), var(1.into(), prop())),
),
),
@@ -292,20 +241,12 @@ mod tests {
prop(),
abs(
prop(),
- app(
- abs(prop(), var(1.into(), prop())),
- app(abs(prop(), var(2.into(), prop())), var(2.into(), prop())),
- ),
+ app(abs(prop(), var(1.into(), prop())), app(abs(prop(), var(2.into(), prop())), var(2.into(), prop()))),
),
));
- let term_step_6 = arena.build_raw(abs(
- prop(),
- abs(
- prop(),
- app(abs(prop(), var(2.into(), prop())), var(2.into(), prop())),
- ),
- ));
+ let term_step_6 =
+ arena.build_raw(abs(prop(), abs(prop(), app(abs(prop(), var(2.into(), prop())), var(2.into(), prop())))));
// λa.λb.b
let term_step_7 = arena.build_raw(abs(prop(), abs(prop(), var(1.into(), prop()))));
@@ -334,10 +275,7 @@ mod tests {
#[test]
fn prod_beta_red() {
use_arena(|arena| {
- let term = arena.build_raw(prod(
- prop(),
- app(abs(prop(), var(1.into(), prop())), var(1.into(), prop())),
- ));
+ let term = arena.build_raw(prod(prop(), app(abs(prop(), var(1.into(), prop())), var(1.into(), prop()))));
let reduced = arena.build_raw(prod(prop(), var(1.into(), prop())));
assert_eq!(arena.beta_reduction(term), reduced);
@@ -347,17 +285,9 @@ mod tests {
#[test]
fn app_red_rhs() {
use_arena(|arena| {
- let term = arena.build_raw(abs(
- prop(),
- app(
- var(1.into(), prop()),
- app(abs(prop(), var(1.into(), prop())), var(1.into(), prop())),
- ),
- ));
- let reduced = arena.build_raw(abs(
- prop(),
- app(var(1.into(), prop()), var(1.into(), prop())),
- ));
+ let term = arena
+ .build_raw(abs(prop(), app(var(1.into(), prop()), app(abs(prop(), var(1.into(), prop())), var(1.into(), prop())))));
+ let reduced = arena.build_raw(abs(prop(), app(var(1.into(), prop()), var(1.into(), prop()))));
assert_eq!(arena.beta_reduction(term), reduced);
})
diff --git a/kernel/src/type_checker.rs b/kernel/src/type_checker.rs
index e577d8a4..1e6671b4 100644
--- a/kernel/src/type_checker.rs
+++ b/kernel/src/type_checker.rs
@@ -6,10 +6,10 @@ use std::cmp::max;
use derive_more::Display;
use num_bigint::BigUint;
+use Payload::*;
use crate::error::{Error, Result, ResultTerm};
use crate::term::arena::{Arena, Payload, Term};
-use Payload::*;
#[derive(Clone, Debug, Display, Eq, PartialEq)]
#[display(fmt = "{}: {}", _0, _1)]
@@ -54,9 +54,7 @@ impl<'arena> Arena<'arena> {
(Var(i, _), Var(j, _)) => i == j,
- (&Prod(t1, u1), &Prod(t2, u2)) => {
- self.conversion(t1, t2) && self.conversion(u1, u2)
- }
+ (&Prod(t1, u1), &Prod(t2, u2)) => self.conversion(t1, t2) && self.conversion(u1, u2),
// Since we assume that both values already have the same type,
// checking conversion over the argument type is useless.
@@ -121,7 +119,7 @@ impl<'arena> Arena<'arena> {
let univ_t = self.normal_form(univ_t);
let univ_u = self.normal_form(univ_u);
self.imax(univ_t, univ_u)
- }
+ },
Abs(t, u) => {
let type_t = self.infer(t)?;
@@ -129,12 +127,12 @@ impl<'arena> Arena<'arena> {
Type(_) | Prop => {
let type_u = self.infer(u)?;
Ok(self.prod(t, type_u))
- }
+ },
_ => Err(Error {
kind: TypeCheckerError::NotUniverse(type_t).into(),
}),
}
- }
+ },
App(t, u) => {
let type_t = self.infer(t)?;
@@ -147,21 +145,16 @@ impl<'arena> Arena<'arena> {
Ok(self.substitute(cls, u, 1))
} else {
Err(Error {
- kind: TypeCheckerError::WrongArgumentType(
- t,
- arg_type,
- TypedTerm(u, type_u),
- )
- .into(),
+ kind: TypeCheckerError::WrongArgumentType(t, arg_type, TypedTerm(u, type_u)).into(),
})
}
- }
+ },
_ => Err(Error {
kind: TypeCheckerError::NotAFunction(TypedTerm(t, type_t), u).into(),
}),
}
- }
+ },
}
})
}
@@ -201,10 +194,7 @@ mod tests {
fn def_eq_2() {
use_arena(|arena| {
let id = arena.build_raw(id());
- let term = arena.build_raw(app(
- abs(prop(), abs(prop(), var(2.into(), prop()))),
- id.into(),
- ));
+ let term = arena.build_raw(app(abs(prop(), abs(prop(), var(2.into(), prop()))), id.into()));
let normal_form = arena.build_raw(abs(prop(), id.into()));
assert!(arena.is_def_eq(term, normal_form).is_ok())
@@ -216,10 +206,7 @@ mod tests {
use_arena(|arena| {
let id = arena.build_raw(id());
// λa.a (λx.x) (λx.x)
- let term = arena.build_raw(abs(
- prop(),
- app(app(var(2.into(), prop()), id.into()), id.into()),
- ));
+ let term = arena.build_raw(abs(prop(), app(app(var(2.into(), prop()), id.into()), id.into())));
assert!(arena.is_def_eq(term, term).is_ok());
})
@@ -261,15 +248,9 @@ mod tests {
fn failed_app_head_conversion() {
use_arena(|arena| {
let type_0 = arena.type_usize(0);
- let term_lhs = arena.build_raw(abs(
- type_0.into(),
- abs(type_0.into(), app(var(1.into(), prop()), prop())),
- ));
+ let term_lhs = arena.build_raw(abs(type_0.into(), abs(type_0.into(), app(var(1.into(), prop()), prop()))));
- let term_rhs = arena.build_raw(abs(
- type_0.into(),
- abs(type_0.into(), app(var(2.into(), prop()), prop())),
- ));
+ let term_rhs = arena.build_raw(abs(type_0.into(), abs(type_0.into(), app(var(2.into(), prop()), prop()))));
assert_eq!(
arena.is_def_eq(term_lhs, term_rhs),
@@ -284,10 +265,7 @@ mod tests {
fn typed_reduction_app_1() {
use_arena(|arena| {
let type_0 = arena.type_usize(0);
- let term = arena.build_raw(app(
- abs(type_0.into(), var(1.into(), type_0.into())),
- prop(),
- ));
+ let term = arena.build_raw(app(abs(type_0.into(), var(1.into(), type_0.into())), prop()));
let reduced = arena.build_raw(prop());
assert!(arena.is_def_eq(term, reduced).is_ok());
@@ -342,11 +320,7 @@ mod tests {
abs(
"d",
prod("_", prop(), prop()),
- abs(
- "e",
- prod("_", prop(), prop()),
- app(var("e"), app(var("d"), var("b"))),
- ),
+ abs("e", prod("_", prop(), prop()), app(var("e"), app(var("d"), var("b")))),
),
),
// _ : P
@@ -361,11 +335,7 @@ mod tests {
// f: (P -> P) -> (P -> P) -> P
abs(
"f",
- prod(
- "_",
- prod("_", prop(), prop()),
- prod("_", prod("_", prop(), prop()), prop()),
- ),
+ prod("_", prod("_", prop(), prop()), prod("_", prod("_", prop(), prop()), prop())),
abs(
"g",
// g: P -> P
@@ -377,15 +347,11 @@ mod tests {
.unwrap();
// λa: P. λb: P. b
- let reduced = arena
- .build(abs("_", prop(), abs("x", prop(), var("x"))))
- .unwrap();
+ let reduced = arena.build(abs("_", prop(), abs("x", prop(), var("x")))).unwrap();
assert!(arena.is_def_eq(term, reduced).is_ok());
let term_type = arena.infer(term).unwrap();
- let expected_type = arena
- .build(prod("_", prop(), prod("_", prop(), prop())))
- .unwrap();
+ let expected_type = arena.build(prod("_", prop(), prod("_", prop(), prop()))).unwrap();
assert_eq!(term_type, expected_type);
assert!(arena.check(term, term_type).is_ok())
})
@@ -397,10 +363,7 @@ mod tests {
let type_0 = arena.type_usize(0);
let type_1 = arena.type_usize(1);
- let term = arena.build_raw(app(
- abs(prop(), type_0.into()),
- prod(prop(), var(1.into(), prop())),
- ));
+ let term = arena.build_raw(app(abs(prop(), type_0.into()), prod(prop(), var(1.into(), prop()))));
assert!(arena.is_def_eq(term, type_0).is_ok());
@@ -432,19 +395,13 @@ mod tests {
let term = arena.build_raw(abs(
prod(prop(), prop()),
app(
- abs(
- prop(),
- app(var(2.into(), prod(prop(), prop())), var(1.into(), prop())),
- ),
+ abs(prop(), app(var(2.into(), prod(prop(), prop())), var(1.into(), prop()))),
var(1.into(), prod(prop(), prop())),
),
));
// λx.x x
- let reduced = arena.build_raw(abs(
- prop(),
- app(var(1.into(), prop()), var(1.into(), prop())),
- ));
+ let reduced = arena.build_raw(abs(prop(), app(var(1.into(), prop()), var(1.into(), prop()))));
assert!(arena.is_def_eq(term, reduced).is_ok())
})
@@ -476,15 +433,9 @@ mod tests {
#[test]
fn typed_prod_3() {
use_arena(|arena| {
- let term = arena.build_raw(abs(
- prop(),
- abs(var(1.into(), prop()), var(1.into(), var(2.into(), prop()))),
- ));
+ let term = arena.build_raw(abs(prop(), abs(var(1.into(), prop()), var(1.into(), var(2.into(), prop())))));
let term_type = arena.infer(term).unwrap();
- let expected_type = arena.build_raw(prod(
- prop(),
- prod(var(1.into(), prop()), var(2.into(), prop())),
- ));
+ let expected_type = arena.build_raw(prod(prop(), prod(var(1.into(), prop()), var(2.into(), prop()))));
assert_eq!(term_type, expected_type);
assert!(arena.check(term, term_type).is_ok());
@@ -496,19 +447,12 @@ mod tests {
use_arena(|arena| {
let type_0 = arena.type_usize(0);
- let identity = arena.build_raw(abs(
- type_0.into(),
- abs(
- var(1.into(), type_0.into()),
- var(1.into(), var(2.into(), type_0.into())),
- ),
- ));
+ let identity =
+ arena.build_raw(abs(type_0.into(), abs(var(1.into(), type_0.into()), var(1.into(), var(2.into(), type_0.into())))));
let identity_type = arena.infer(identity).unwrap();
- let expected_type = arena.build_raw(prod(
- type_0.into(),
- prod(var(1.into(), type_0.into()), var(2.into(), type_0.into())),
- ));
+ let expected_type =
+ arena.build_raw(prod(type_0.into(), prod(var(1.into(), type_0.into()), var(2.into(), type_0.into()))));
assert_eq!(identity_type, expected_type);
assert!(arena.check(identity, identity_type).is_ok());
@@ -524,25 +468,13 @@ mod tests {
prop(),
abs(
prod(prop(), prod(prop(), prop())),
- app(
- app(
- var(1.into(), prod(prop(), prod(prop(), prop()))),
- var(3.into(), prop()),
- ),
- var(2.into(), prop()),
- ),
+ app(app(var(1.into(), prod(prop(), prod(prop(), prop()))), var(3.into(), prop())), var(2.into(), prop())),
),
),
));
let term_type = arena.infer(term).unwrap();
- assert_eq!(
- term_type,
- arena.build_raw(prod(
- prop(),
- prod(prop(), prod(prod(prop(), prod(prop(), prop())), prop()))
- ))
- );
+ assert_eq!(term_type, arena.build_raw(prod(prop(), prod(prop(), prod(prod(prop(), prod(prop(), prop())), prop())))));
assert!(arena.check(term, term_type).is_ok());
})
}
@@ -580,11 +512,7 @@ mod tests {
assert_eq!(
arena.infer(term),
Err(Error {
- kind: TypeCheckerError::NotAFunction(
- TypedTerm(arena.prop(), arena.type_usize(0)),
- arena.prop()
- )
- .into()
+ kind: TypeCheckerError::NotAFunction(TypedTerm(arena.prop(), arena.type_usize(0)), arena.prop()).into()
})
);
})
@@ -598,11 +526,7 @@ mod tests {
assert_eq!(
arena.infer(term),
Err(Error {
- kind: TypeCheckerError::NotAFunction(
- TypedTerm(arena.prop(), arena.type_usize(0)),
- arena.prop()
- )
- .into()
+ kind: TypeCheckerError::NotAFunction(TypedTerm(arena.prop(), arena.type_usize(0)), arena.prop()).into()
})
);
})
@@ -616,11 +540,7 @@ mod tests {
assert_eq!(
arena.infer(term),
Err(Error {
- kind: TypeCheckerError::NotAFunction(
- TypedTerm(arena.prop(), arena.type_usize(0)),
- arena.prop()
- )
- .into()
+ kind: TypeCheckerError::NotAFunction(TypedTerm(arena.prop(), arena.type_usize(0)), arena.prop()).into()
})
);
})
@@ -634,11 +554,7 @@ mod tests {
assert_eq!(
arena.infer(term),
Err(Error {
- kind: TypeCheckerError::NotAFunction(
- TypedTerm(arena.prop(), arena.type_usize(0)),
- arena.prop()
- )
- .into()
+ kind: TypeCheckerError::NotAFunction(TypedTerm(arena.prop(), arena.type_usize(0)), arena.prop()).into()
})
);
})
@@ -652,11 +568,7 @@ mod tests {
assert_eq!(
arena.infer(term),
Err(Error {
- kind: TypeCheckerError::NotAFunction(
- TypedTerm(arena.prop(), arena.type_usize(0)),
- arena.prop()
- )
- .into()
+ kind: TypeCheckerError::NotAFunction(TypedTerm(arena.prop(), arena.type_usize(0)), arena.prop()).into()
})
);
})
@@ -670,11 +582,7 @@ mod tests {
assert_eq!(
arena.infer(term),
Err(Error {
- kind: TypeCheckerError::NotAFunction(
- TypedTerm(arena.prop(), arena.type_usize(0)),
- arena.prop()
- )
- .into()
+ kind: TypeCheckerError::NotAFunction(TypedTerm(arena.prop(), arena.type_usize(0)), arena.prop()).into()
})
);
})
@@ -688,10 +596,7 @@ mod tests {
let term = arena.build_raw(abs(
prod(prop(), prop()),
app(
- abs(
- prop(),
- app(var(2.into(), prod(prop(), prop())), var(1.into(), prop())),
- ),
+ abs(prop(), app(var(2.into(), prod(prop(), prop())), var(1.into(), prop()))),
var(1.into(), prod(prop(), prop())),
),
));
@@ -700,15 +605,9 @@ mod tests {
arena.infer(term),
Err(Error {
kind: TypeCheckerError::WrongArgumentType(
- arena.build_raw(abs(
- prop(),
- app(var(2.into(), prod(prop(), prop())), var(1.into(), prop()))
- )),
+ arena.build_raw(abs(prop(), app(var(2.into(), prod(prop(), prop())), var(1.into(), prop())))),
arena.prop(),
- TypedTerm(
- arena.build_raw(var(1.into(), prod(prop(), prop()))),
- arena.build_raw(prod(prop(), prop()))
- )
+ TypedTerm(arena.build_raw(var(1.into(), prod(prop(), prop()))), arena.build_raw(prod(prop(), prop())))
)
.into()
})
@@ -721,20 +620,13 @@ mod tests {
use_arena(|arena| {
let term = arena.build_raw(abs(
prop(),
- abs(
- var(1.into(), prop()),
- abs(
- var(1.into(), var(2.into(), prop())),
- var(1.into(), var(2.into(), prop())),
- ),
- ),
+ abs(var(1.into(), prop()), abs(var(1.into(), var(2.into(), prop())), var(1.into(), var(2.into(), prop())))),
));
assert_eq!(
arena.infer(term),
Err(Error {
- kind: TypeCheckerError::NotUniverse(arena.build_raw(var(2.into(), prop())))
- .into()
+ kind: TypeCheckerError::NotUniverse(arena.build_raw(var(2.into(), prop()))).into()
})
);
})
@@ -748,8 +640,7 @@ mod tests {
assert_eq!(
arena.infer(term),
Err(Error {
- kind: TypeCheckerError::NotUniverse(arena.build_raw(prod(prop(), prop())))
- .into()
+ kind: TypeCheckerError::NotUniverse(arena.build_raw(prod(prop(), prop()))).into()
})
);
})
@@ -763,10 +654,8 @@ mod tests {
assert_eq!(
arena.infer(term),
Err(Error {
- kind: TypeCheckerError::NotUniverse(
- arena.build_raw(prod(prop(), type_(BigUint::from(0_u64).into())))
- )
- .into()
+ kind: TypeCheckerError::NotUniverse(arena.build_raw(prod(prop(), type_(BigUint::from(0_u64).into()))))
+ .into()
})
);
})
@@ -781,11 +670,7 @@ mod tests {
assert_eq!(
arena.check(term, expected_type),
Err(Error {
- kind: TypeCheckerError::NotAFunction(
- TypedTerm(arena.prop(), arena.type_usize(0)),
- arena.prop(),
- )
- .into(),
+ kind: TypeCheckerError::NotAFunction(TypedTerm(arena.prop(), arena.type_usize(0)), arena.prop()).into(),
})
);
})
diff --git a/kernel/tests/and.rs b/kernel/tests/and.rs
index 210678c6..c5013a39 100644
--- a/kernel/tests/and.rs
+++ b/kernel/tests/and.rs
@@ -18,19 +18,7 @@ where
.build(abs(
"A",
prop(),
- abs(
- "B",
- prop(),
- prod(
- "C",
- prop(),
- prod(
- "_",
- prod("_", var("A"), prod("_", var("B"), var("C"))),
- var("C"),
- ),
- ),
- ),
+ abs("B", prop(), prod("C", prop(), prod("_", prod("_", var("A"), prod("_", var("B"), var("C"))), var("C")))),
))
.unwrap();
@@ -43,9 +31,7 @@ where
#[test]
fn and_true_true() {
use_and_arena(|arena| {
- let goal = arena
- .build(app(app(var("and"), var("True")), var("True")))
- .unwrap();
+ let goal = arena.build(app(app(var("and"), var("True")), var("True"))).unwrap();
let hypothesis = arena.build(abs("x", var("False"), var("x"))).unwrap();
let true_ = arena.build(var("True")).unwrap();
@@ -57,11 +43,7 @@ fn and_true_true() {
.build(abs(
"a",
prop(),
- abs(
- "b",
- prod("_", var("True"), prod("_", var("True"), var("a"))),
- app(app(var("b"), var("hyp")), var("hyp")),
- ),
+ abs("b", prod("_", var("True"), prod("_", var("True"), var("a"))), app(app(var("b"), var("hyp")), var("hyp"))),
))
.unwrap();
@@ -79,11 +61,7 @@ fn and_intro() {
prod(
"B", // B : prop()
prop(),
- prod(
- "_",
- var("A"),
- prod("_", var("B"), app(app(var("and"), var("A")), var("B"))),
- ),
+ prod("_", var("A"), prod("_", var("B"), app(app(var("and"), var("A")), var("B")))),
),
))
.unwrap();
diff --git a/parser/src/command.rs b/parser/src/command.rs
index b0b6bc8a..2daa4448 100644
--- a/parser/src/command.rs
+++ b/parser/src/command.rs
@@ -46,7 +46,7 @@ impl<'build> fmt::Display for Command<'build> {
Import(files) => {
write!(f, "imports")?;
files.iter().try_for_each(|file| write!(f, " {file}"))
- }
+ },
Search(name) => write!(f, "search {}", name),
}
diff --git a/parser/src/parser.rs b/parser/src/parser.rs
index 90e000a8..8084d02e 100644
--- a/parser/src/parser.rs
+++ b/parser/src/parser.rs
@@ -1,11 +1,11 @@
+use kernel::location::Location;
+use kernel::term::builders::Builder;
use pest::error::LineColLocation;
use pest::iterators::Pair;
use pest::{Parser, Span};
use crate::command::Command;
use crate::error::{Error, ErrorKind};
-use kernel::location::Location;
-use kernel::term::builders::Builder;
#[derive(Parser)]
#[grammar = "term.pest"]
@@ -30,16 +30,13 @@ fn parse_term(pair: Pair<Rule>) -> Builder {
Rule::Var => Var(pair.into_inner().as_str()),
- Rule::Type => Type(
- pair.into_inner()
- .fold(0, |_, x| x.as_str().parse::<usize>().unwrap()),
- ),
+ Rule::Type => Type(pair.into_inner().fold(0, |_, x| x.as_str().parse::<usize>().unwrap())),
Rule::App => {
let mut iter = pair.into_inner().map(parse_term);
let t = iter.next().unwrap();
iter.fold(t, |acc, x| App(Box::new(acc), Box::new(x)))
- }
+ },
Rule::Abs => {
let mut iter = pair.into_inner();
@@ -51,7 +48,7 @@ fn parse_term(pair: Pair<Rule>) -> Builder {
})
.rev()
.fold(body, |acc, (var, type_)| Abs(var, type_, Box::new(acc)))
- }
+ },
Rule::dProd => {
let mut iter = pair.into_inner();
@@ -63,15 +60,13 @@ fn parse_term(pair: Pair<Rule>) -> Builder {
})
.rev()
.fold(body, |acc, (var, type_)| Prod(var, type_, Box::new(acc)))
- }
+ },
Rule::Prod => {
let mut iter = pair.into_inner();
let ret = parse_term(iter.next_back().unwrap());
- iter.map(parse_term).rev().fold(ret, |acc, argtype| {
- Prod("_", Box::new(argtype), Box::new(acc))
- })
- }
+ iter.map(parse_term).rev().fold(ret, |acc, argtype| Prod("_", Box::new(argtype), Box::new(acc)))
+ },
term => unreachable!("Unexpected term: {:?}", term),
}
@@ -87,21 +82,21 @@ fn parse_expr<'build>(pair: Pair<'build, Rule>) -> Command<'build> {
let mut iter = pair.into_inner();
let t = parse_term(iter.next().unwrap());
Command::GetType(t)
- }
+ },
Rule::CheckType => {
let mut iter = pair.into_inner();
let t1 = parse_term(iter.next().unwrap());
let t2 = parse_term(iter.next().unwrap());
Command::CheckType(t1, t2)
- }
+ },
Rule::Define => {
let mut iter = pair.into_inner();
let s: &'build str = iter.next().unwrap().as_str();
let term = parse_term(iter.next().unwrap());
Command::Define(s, None, term)
- }
+ },
Rule::DefineCheckType => {
let mut iter = pair.into_inner();
@@ -109,22 +104,22 @@ fn parse_expr<'build>(pair: Pair<'build, Rule>) -> Command<'build> {
let t = parse_term(iter.next().unwrap());
let term = parse_term(iter.next().unwrap());
Command::Define(s, Some(t), term)
- }
+ },
Rule::Eval => {
let term = parse_term(pair.into_inner().next().unwrap());
Command::Eval(term)
- }
+ },
Rule::ImportFile => {
let files = pair.into_inner().map(|pair| pair.as_str()).collect();
Command::Import(files)
- }
+ },
Rule::Search => {
let s = pair.into_inner().next().unwrap().as_str();
Command::Search(s)
- }
+ },
command => unreachable!("Unexpected command: {:?}", command),
}
@@ -177,7 +172,7 @@ fn convert_error(err: pest::error::Error<Rule>) -> Error {
right = y;
}
Location::new((x, left).into(), (x, right).into())
- }
+ },
LineColLocation::Span(start, end) => Location::new(start.into(), end.into()),
};
@@ -198,18 +193,14 @@ fn convert_error(err: pest::error::Error<Rule>) -> Error {
///
/// if unsuccessful, a box containing the first error that was encountered is returned.
pub fn parse_line(line: &str) -> crate::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()))
}
/// 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_file(file: &str) -> crate::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)]
@@ -221,10 +212,8 @@ mod tests {
use super::*;
/// Error messages
- const COMMAND_ERR: &str =
- "expected def var := term, def var : term := term, check term : term, check term, eval term, import path_to_file, or search var";
- const TERM_ERR: &str =
- "expected variable, abstraction, dependent product, application, product, Prop, or Type";
+ const COMMAND_ERR: &str = "expected def var := term, def var : term := term, check term : term, check term, eval term, import path_to_file, or search var";
+ const TERM_ERR: &str = "expected variable, abstraction, dependent product, application, product, Prop, or Type";
const SIMPLE_TERM_ERR: &str = "expected variable, abstraction, Prop, or Type";
const UNIVERSE_ERR: &str = "expected universe level, variable, abstraction, Prop, or Type";
@@ -241,18 +230,12 @@ mod tests {
#[test]
fn successful_define_with_type_annotation() {
- assert_eq!(
- parse_line("def x : Type := Prop"),
- Ok(Define("x", Some(Type(0)), Prop))
- );
+ assert_eq!(parse_line("def x : Type := Prop"), Ok(Define("x", Some(Type(0)), Prop)));
}
#[test]
fn successful_import() {
- assert_eq!(
- parse_line("import file1 dir/file2"),
- Ok(Import(["file1", "dir/file2"].to_vec()))
- );
+ assert_eq!(parse_line("import file1 dir/file2"), Ok(Import(["file1", "dir/file2"].to_vec())));
assert_eq!(parse_line("import "), Ok(Import(Vec::new())))
}
@@ -273,10 +256,7 @@ mod tests {
#[test]
fn successful_checktype() {
- assert_eq!(
- parse_line("check Prop : Type"),
- Ok(CheckType(Prop, Type(0)))
- );
+ assert_eq!(parse_line("check Prop : Type"), Ok(CheckType(Prop, Type(0))));
}
#[test]
@@ -286,10 +266,7 @@ mod tests {
#[test]
fn successful_var() {
- assert_eq!(
- parse_line("check fun A: Prop => A"),
- Ok(GetType(Abs("A", Box::new(Prop), Box::new(Var("A")))))
- );
+ assert_eq!(parse_line("check fun A: Prop => A"), Ok(GetType(Abs("A", Box::new(Prop), Box::new(Var("A"))))));
}
#[test]
@@ -301,14 +278,8 @@ mod tests {
#[test]
fn successful_app() {
- let res_left = Ok(GetType(App(
- Box::new(App(Box::new(Var("A")), Box::new(Var("B")))),
- Box::new(Var("C")),
- )));
- let res_right = Ok(GetType(App(
- Box::new(Var("A")),
- Box::new(App(Box::new(Var("B")), Box::new(Var("C")))),
- )));
+ let res_left = Ok(GetType(App(Box::new(App(Box::new(Var("A")), Box::new(Var("B")))), Box::new(Var("C")))));
+ let res_right = Ok(GetType(App(Box::new(Var("A")), Box::new(App(Box::new(Var("B")), Box::new(Var("C")))))));
assert_eq!(parse_line("check A B C"), res_left);
assert_eq!(parse_line("check (A B) C"), res_left);
assert_eq!(parse_line("check A (B C)"), res_right);
@@ -316,16 +287,8 @@ mod tests {
#[test]
fn successful_prod() {
- let res_left = Ok(GetType(Prod(
- "_",
- Box::new(Prod("_", Box::new(Var("A")), Box::new(Var("B")))),
- Box::new(Var("C")),
- )));
- let res_right = Ok(GetType(Prod(
- "_",
- Box::new(Var("A")),
- Box::new(Prod("_", Box::new(Var("B")), Box::new(Var("C")))),
- )));
+ let res_left = Ok(GetType(Prod("_", Box::new(Prod("_", Box::new(Var("A")), Box::new(Var("B")))), Box::new(Var("C")))));
+ let res_right = Ok(GetType(Prod("_", Box::new(Var("A")), Box::new(Prod("_", Box::new(Var("B")), Box::new(Var("C")))))));
assert_eq!(parse_line("check A -> B -> C"), res_right);
assert_eq!(parse_line("check A -> (B -> C)"), res_right);
assert_eq!(parse_line("check (A -> B) -> C"), res_left);
@@ -333,11 +296,7 @@ mod tests {
#[test]
fn successful_dprod() {
- let res = Ok(GetType(Prod(
- "x",
- Box::new(Type(0)),
- Box::new(Prod("y", Box::new(Type(1)), Box::new(Var("x")))),
- )));
+ let res = Ok(GetType(Prod("x", Box::new(Type(0)), Box::new(Prod("y", Box::new(Type(1)), Box::new(Var("x")))))));
assert_eq!(parse_line("check (x:Type) -> (y:Type 1) -> x"), res);
assert_eq!(parse_line("check (x:Type) -> ((y:Type 1) -> x)"), res);
}
@@ -350,17 +309,10 @@ mod tests {
Box::new(Abs(
"x",
Box::new(Prop),
- Box::new(Abs(
- "y",
- Box::new(Prop),
- Box::new(Abs("z", Box::new(Prop), Box::new(Var("x")))),
- )),
+ Box::new(Abs("y", Box::new(Prop), Box::new(Abs("z", Box::new(Prop), Box::new(Var("x")))))),
)),
);
- assert_eq!(
- parse_line("check fun w x: Prop, y z: Prop => x"),
- Ok(GetType(res))
- );
+ assert_eq!(parse_line("check fun w x: Prop, y z: Prop => x"), Ok(GetType(res)));
}
#[test]
@@ -386,20 +338,12 @@ mod tests {
let res = Ok(GetType(Abs(
"x",
Box::new(Prop),
- Box::new(Abs(
- "x",
- Box::new(Var("x")),
- Box::new(Abs("x", Box::new(Var("x")), Box::new(Var("x")))),
- )),
+ Box::new(Abs("x", Box::new(Var("x")), Box::new(Abs("x", Box::new(Var("x")), Box::new(Var("x")))))),
)));
let res2 = Ok(GetType(Abs(
"x",
Box::new(Prop),
- Box::new(Abs(
- "y",
- Box::new(Var("x")),
- Box::new(Abs("z", Box::new(Var("x")), Box::new(Var("z")))),
- )),
+ Box::new(Abs("y", Box::new(Var("x")), Box::new(Abs("z", Box::new(Var("x")), Box::new(Var("z")))))),
)));
assert_eq!(parse_line("check fun x : Prop, x : x, x : x => x"), res);
assert_eq!(parse_line("check fun x : Prop, x x : x => x"), res);
@@ -411,20 +355,12 @@ mod tests {
let res = Ok(GetType(Prod(
"x",
Box::new(Prop),
- Box::new(Prod(
- "x",
- Box::new(Var("x")),
- Box::new(Prod("x", Box::new(Var("x")), Box::new(Var("x")))),
- )),
+ Box::new(Prod("x", Box::new(Var("x")), Box::new(Prod("x", Box::new(Var("x")), Box::new(Var("x")))))),
)));
let res2 = Ok(GetType(Prod(
"x",
Box::new(Prop),
- Box::new(Prod(
- "y",
- Box::new(Var("x")),
- Box::new(Prod("z", Box::new(Var("x")), Box::new(Var("z")))),
- )),
+ Box::new(Prod("y", Box::new(Var("x")), Box::new(Prod("z", Box::new(Var("x")), Box::new(Var("z")))))),
)));
assert_eq!(parse_line("check (x : Prop, x : x, x : x) -> x"), res);
assert_eq!(parse_line("check (x : Prop, x x : x) -> x"), res);
@@ -439,55 +375,28 @@ mod tests {
Box::new(Abs(
"x",
Box::new(Prop),
- Box::new(Abs(
- "y",
- Box::new(Prop),
- Box::new(Abs("z", Box::new(Prop), Box::new(Var("x")))),
- )),
+ Box::new(Abs("y", Box::new(Prop), Box::new(Abs("z", Box::new(Prop), Box::new(Var("x")))))),
)),
);
- assert_eq!(
- parse_line("check fun (((w x : Prop))), y z : Prop => x"),
- Ok(GetType(res))
- );
+ assert_eq!(parse_line("check fun (((w x : Prop))), y z : Prop => x"), Ok(GetType(res)));
}
#[test]
fn parenthesis_in_prod() {
- let res = Prod(
- "_",
- Box::new(Type(0)),
- Box::new(Prod("_", Box::new(Type(1)), Box::new(Type(2)))),
- );
- assert_eq!(
- parse_line("check (((Type))) -> (((Type 1 -> Type 2)))"),
- Ok(GetType(res))
- );
+ let res = Prod("_", Box::new(Type(0)), Box::new(Prod("_", Box::new(Type(1)), Box::new(Type(2)))));
+ assert_eq!(parse_line("check (((Type))) -> (((Type 1 -> Type 2)))"), Ok(GetType(res)));
}
#[test]
fn parenthesis_in_dprod() {
- let res = Prod(
- "x",
- Box::new(Type(0)),
- Box::new(Prod("y", Box::new(Type(1)), Box::new(Var("x")))),
- );
- assert_eq!(
- parse_line("check (((x:Type))) -> ((((y:Type 1) -> x)))"),
- Ok(GetType(res))
- );
+ let res = Prod("x", Box::new(Type(0)), Box::new(Prod("y", Box::new(Type(1)), Box::new(Var("x")))));
+ assert_eq!(parse_line("check (((x:Type))) -> ((((y:Type 1) -> x)))"), Ok(GetType(res)));
}
#[test]
fn parenthesis_in_app() {
- let res = App(
- Box::new(Var("A")),
- Box::new(App(Box::new(Var("B")), Box::new(Var("C")))),
- );
- assert_eq!(
- parse_line("check ((((((A))) (((B C))))))"),
- Ok(GetType(res))
- );
+ let res = App(Box::new(Var("A")), Box::new(App(Box::new(Var("B")), Box::new(Var("C")))));
+ assert_eq!(parse_line("check ((((((A))) (((B C))))))"), Ok(GetType(res)));
}
#[test]
@@ -499,14 +408,8 @@ mod tests {
check fun x:Prop => x
"#;
- assert_eq!(
- parse_file(file).unwrap()[0],
- parse_line("def x := Prop -> Prop").unwrap()
- );
- assert_eq!(
- parse_file(file).unwrap()[1],
- parse_line("check fun x:Prop => x").unwrap()
- );
+ assert_eq!(parse_file(file).unwrap()[0], parse_line("def x := Prop -> Prop").unwrap());
+ assert_eq!(parse_file(file).unwrap()[1], parse_line("check fun x:Prop => x").unwrap());
}
#[test]
diff --git a/proost/src/evaluator.rs b/proost/src/evaluator.rs
index 72a11421..eba1b916 100644
--- a/proost/src/evaluator.rs
+++ b/proost/src/evaluator.rs
@@ -1,14 +1,17 @@
-use std::{collections::HashSet, fs::read_to_string, path::PathBuf};
+use std::collections::HashSet;
+use std::fs::read_to_string;
+use std::path::PathBuf;
use colored::Colorize;
use derive_more::Display;
-use path_absolutize::Absolutize;
-
-use crate::error::{Error::*, Result};
use kernel::location::Location;
use kernel::term::arena::{Arena, Term};
use parser::command::Command;
use parser::{parse_file, parse_line};
+use path_absolutize::Absolutize;
+
+use crate::error::Error::*;
+use crate::error::Result;
/// Type representing parser errors.
#[derive(Clone, Debug, Display, Eq, PartialEq)]
@@ -50,12 +53,7 @@ impl<'arena> Evaluator {
}
/// Create a new path from a relative path
- fn create_path(
- &self,
- location: Location,
- relative_path: String,
- importing: &[PathBuf],
- ) -> Result<'arena, PathBuf> {
+ fn create_path(&self, location: Location, relative_path: String, importing: &[PathBuf]) -> Result<'arena, PathBuf> {
let file_path = importing
.last()
.and_then(|path| path.parent())
@@ -91,11 +89,7 @@ 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,
}));
@@ -114,11 +108,7 @@ impl<'arena> Evaluator {
Ok(())
}
- pub fn process_line(
- &mut self,
- arena: &mut Arena<'arena>,
- line: &str,
- ) -> Result<'arena, Option<Term<'arena>>> {
+ pub fn process_line(&mut self, arena: &mut Arena<'arena>, line: &str) -> Result<'arena, Option<Term<'arena>>> {
let command = parse_line(line)?;
self.process(arena, &command, &mut Vec::new())
}
@@ -160,7 +150,7 @@ impl<'arena> Evaluator {
location: Location::default(), // TODO (see #38)
}))
}
- }
+ },
Command::Define(s, Some(t), term) => {
let term = term.realise(arena)?;
@@ -168,35 +158,31 @@ impl<'arena> Evaluator {
arena.check(term, t)?;
arena.bind(s, term);
Ok(None)
- }
+ },
Command::CheckType(t1, t2) => {
let t1 = t1.realise(arena)?;
let t2 = t2.realise(arena)?;
arena.check(t1, t2)?;
Ok(None)
- }
+ },
Command::GetType(t) => {
let t = t.realise(arena)?;
Ok(arena.infer(t).map(Some)?)
- }
+ },
Command::Eval(t) => {
let t = t.realise(arena)?;
Ok(Some(arena.normal_form(t)))
- }
+ },
Command::Search(s) => Ok(arena.get_binding(s)), // TODO (see #49)
Command::Import(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_string(), importing)?;
self.import_file(arena, Location::default(), file_path, importing)
})
.map(|_| None),
@@ -210,7 +196,7 @@ impl<'arena> Evaluator {
for line in t.to_string().lines() {
println!("{} {}", "\u{2713}".green(), line)
}
- }
+ },
Err(err) => {
let string = match err {
Parser(parser::error::Error {
@@ -229,7 +215,7 @@ impl<'arena> Evaluator {
m = message
)
}
- }
+ },
_ => err.to_string(),
};
@@ -237,7 +223,7 @@ impl<'arena> Evaluator {
for line in string.lines() {
println!("{} {}", "\u{2717}".red(), line)
}
- }
+ },
}
}
}
diff --git a/proost/src/main.rs b/proost/src/main.rs
index 0e0fff41..8c45a2dd 100644
--- a/proost/src/main.rs
+++ b/proost/src/main.rs
@@ -9,12 +9,12 @@ use std::fs;
use atty::Stream;
use clap::Parser;
+use evaluator::Evaluator;
use rustyline::error::ReadlineError;
use rustyline::{Cmd, Config, Editor, EventHandler, KeyCode, KeyEvent, Modifiers};
use rustyline_helper::*;
use crate::error::Result;
-use evaluator::Evaluator;
#[derive(Parser)]
#[command(author, version, about, long_about = None)]
@@ -37,11 +37,7 @@ 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
@@ -50,19 +46,11 @@ fn main() -> Result<'static, ()> {
}
let helper = RustyLineHelper::new(!args.no_color);
- let config = Config::builder()
- .completion_type(rustyline::CompletionType::List)
- .build();
+ let config = Config::builder().completion_type(rustyline::CompletionType::List).build();
let mut rl = Editor::with_config(config)?;
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),
- );
+ rl.bind_sequence(KeyEvent::from('\t'), EventHandler::Conditional(Box::new(TabEventHandler)));
+ rl.bind_sequence(KeyEvent(KeyCode::Enter, Modifiers::ALT), EventHandler::Simple(Cmd::Newline));
kernel::term::arena::use_arena(|arena| {
let current_path = current_dir()?;
@@ -77,9 +65,9 @@ fn main() -> Result<'static, ()> {
rl.add_history_entry(line.as_str());
let result = evaluator.process_line(arena, line.as_str());
evaluator.display(result);
- }
+ },
Ok(_) => (),
- Err(ReadlineError::Interrupted) => {}
+ Err(ReadlineError::Interrupted) => {},
Err(ReadlineError::Eof) => break,
Err(err) => return Err(err.into()),
}
@@ -89,11 +77,7 @@ fn main() -> Result<'static, ()> {
}
fn is_command(input: &str) -> bool {
- input
- .chars()
- .position(|c| !c.is_whitespace())
- .map(|pos| input[pos..pos + 2] != *"//")
- .unwrap_or_else(|| false)
+ input.chars().position(|c| !c.is_whitespace()).map(|pos| input[pos..pos + 2] != *"//").unwrap_or_else(|| false)
}
#[cfg(test)]
diff --git a/proost/src/rustyline_helper.rs b/proost/src/rustyline_helper.rs
index 6c718364..a4fc0c7b 100644
--- a/proost/src/rustyline_helper.rs
+++ b/proost/src/rustyline_helper.rs
@@ -1,3 +1,5 @@
+use std::borrow::Cow::{self, Borrowed, Owned};
+
use colored::*;
use rustyline::completion::{Completer, FilenameCompleter, Pair};
use rustyline::highlight::Highlighter;
@@ -5,7 +7,6 @@ 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 highlighted
const KEYWORDS: [&str; 5] = ["check", "def", "eval", "import", "search"];
@@ -48,11 +49,7 @@ 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())
- }
+ if line.starts_with("import") { self.completer.complete_path(line, pos) } else { Ok(Default::default()) }
}
}
@@ -64,9 +61,7 @@ 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)))
}
}
@@ -89,27 +84,17 @@ fn validate_brackets(input: &str) -> Option<ValidationResult> {
match c {
'(' => stack.push(c),
')' => match stack.pop() {
- Some('(') => {}
+ 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(),
- )))
- }
+ 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)
- }
+ if stack.is_empty() { None } else { Some(ValidationResult::Incomplete) }
}
/// A variation of MatchingBrackerHighlighter:
@@ -138,9 +123,7 @@ impl Highlighter for RustyLineHelper {
let s = String::from(matching as char);
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)
}
}
@@ -150,10 +133,9 @@ 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].is_ascii_whitespace())
- && (offset + pos + from.len() == input.len()
- || input.as_bytes()[offset + pos + from.len()].is_ascii_whitespace())
+ && (offset + pos + from.len() == input.len() || input.as_bytes()[offset + pos + from.len()].is_ascii_whitespace())
{
- input.replace_range(offset + pos..offset + pos + from.len(), to);
+ input.replace_range((offset + pos)..(offset + pos + from.len()), to);
offset += pos + to.len();
} else {
offset += pos + from.len()
@@ -176,17 +158,10 @@ fn find_matching_bracket(line: &str, pos: usize, bracket: u8) -> Option<(u8, usi
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))
}
}
--
GitLab