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 (18)
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 2213 additions and 1297 deletions
Cargo.lock
View file @ ab3d2a84
......@@ -31,6 +31,15 @@ version = "1.3.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a"
[[package]]
name = "bitmaps"
version = "2.1.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "031043d04099746d8db04daf1fa424b2bc8bd69d92b25962dcde24da39ab64a2"
dependencies = [
"typenum",
]
[[package]]
name = "block-buffer"
version = "0.10.3"
......@@ -40,11 +49,17 @@ dependencies = [
"generic-array",
]
[[package]]
name = "bumpalo"
version = "3.11.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "572f695136211188308f16ad2ca5c851a712c464060ae6974944458eb83880ba"
[[package]]
name = "cc"
version = "1.0.74"
version = "1.0.76"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "581f5dba903aac52ea3feb5ec4810848460ee833876f1f9b0fdeab1f19091574"
checksum = "76a284da2e6fe2092f2353e51713435363112dfd60030e22add80be333fb928f"
[[package]]
name = "cfg-if"
......@@ -54,9 +69,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
[[package]]
name = "clap"
version = "4.0.18"
version = "4.0.22"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "335867764ed2de42325fafe6d18b8af74ba97ee0c590fa016f157535b42ab04b"
checksum = "91b9970d7505127a162fdaa9b96428d28a479ba78c9ec7550a63a5d9863db682"
dependencies = [
"atty",
"bitflags",
......@@ -69,9 +84,9 @@ dependencies = [
[[package]]
name = "clap_derive"
version = "4.0.18"
version = "4.0.21"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "16a1b0f6422af32d5da0c58e2703320f379216ee70198241c84173a8c5ac28f3"
checksum = "0177313f9f02afc995627906bbd8967e2be069f5261954222dac78290c2b9014"
dependencies = [
"heck",
"proc-macro-error",
......@@ -219,9 +234,9 @@ dependencies = [
[[package]]
name = "fd-lock"
version = "3.0.7"
version = "3.0.8"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0c93a581058d957dc4176875aad04f82f81613e6611d64aa1a9c755bdfb16711"
checksum = "bb21c69b9fea5e15dbc1049e4b77145dd0ba1c84019c488102de0dc4ea4b0a27"
dependencies = [
"cfg-if",
"rustix",
......@@ -264,17 +279,37 @@ dependencies = [
"libc",
]
[[package]]
name = "im-rc"
version = "15.1.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "af1955a75fa080c677d3972822ec4bad316169ab1cfc6c257a942c2265dbe5fe"
dependencies = [
"bitmaps",
"rand_core",
"rand_xoshiro",
"sized-chunks",
"typenum",
"version_check",
]
[[package]]
name = "io-lifetimes"
version = "0.7.5"
version = "1.0.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "59ce5ef949d49ee85593fc4d3f3f95ad61657076395cbbce23e2121fc5542074"
checksum = "a7d367024b3f3414d8e01f437f704f41a9f64ab36f9067fa73e526ad4c763c87"
dependencies = [
"libc",
"windows-sys",
]
[[package]]
name = "kernel"
version = "0.1.0"
dependencies = [
"bumpalo",
"derive_more",
"im-rc",
"lazy_static",
"num-bigint",
]
......@@ -293,9 +328,9 @@ checksum = "fc7fcc620a3bff7cdd7a365be3376c97191aeaccc2a603e600951e452615bf89"
[[package]]
name = "linux-raw-sys"
version = "0.0.46"
version = "0.1.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d4d2456c373231a208ad294c33dc5bff30051eafd954cd4caae83a712b12854d"
checksum = "bb68f22743a3fb35785f1e7f844ca5a3de2dde5bd0c0ef5b372065814699b121"
[[package]]
name = "log"
......@@ -387,9 +422,9 @@ dependencies = [
[[package]]
name = "pest"
version = "2.4.0"
version = "2.4.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "dbc7bc69c062e492337d74d59b120c274fd3d261b6bf6d3207d499b4b379c41a"
checksum = "a528564cc62c19a7acac4d81e01f39e53e25e17b934878f4c6d25cc2836e62f8"
dependencies = [
"thiserror",
"ucd-trie",
......@@ -397,9 +432,9 @@ dependencies = [
[[package]]
name = "pest_derive"
version = "2.4.0"
version = "2.4.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "60b75706b9642ebcb34dab3bc7750f811609a0eb1dd8b88c2d15bf628c1c65b2"
checksum = "d5fd9bc6500181952d34bd0b2b0163a54d794227b498be0b7afa7698d0a7b18f"
dependencies = [
"pest",
"pest_generator",
......@@ -407,9 +442,9 @@ dependencies = [
[[package]]
name = "pest_generator"
version = "2.4.0"
version = "2.4.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "f4f9272122f5979a6511a749af9db9bfc810393f63119970d7085fed1c4ea0db"
checksum = "d2610d5ac5156217b4ff8e46ddcef7cdf44b273da2ac5bca2ecbfa86a330e7c4"
dependencies = [
"pest",
"pest_meta",
......@@ -420,9 +455,9 @@ dependencies = [
[[package]]
name = "pest_meta"
version = "2.4.0"
version = "2.4.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "4c8717927f9b79515e565a64fe46c38b8cd0427e64c40680b14a7365ab09ac8d"
checksum = "824749bf7e21dd66b36fbe26b3f45c713879cccd4a009a917ab8e045ca8246fe"
dependencies = [
"once_cell",
"pest",
......@@ -493,6 +528,21 @@ dependencies = [
"nibble_vec",
]
[[package]]
name = "rand_core"
version = "0.6.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c"
[[package]]
name = "rand_xoshiro"
version = "0.6.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6f97cdb2a36ed4183de61b2f824cc45c9f1037f28afe0a322e9fff4c108b5aaa"
dependencies = [
"rand_core",
]
[[package]]
name = "redox_syscall"
version = "0.2.16"
......@@ -524,9 +574,9 @@ dependencies = [
[[package]]
name = "rustix"
version = "0.35.13"
version = "0.36.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "727a1a6d65f786ec22df8a81ca3121107f235970dc1705ed681d3e6e8b9cd5f9"
checksum = "812a2ec2043c4d6bc6482f5be2ab8244613cac2493d128d36c0759e52a626ab3"
dependencies = [
"bitflags",
"errno",
......@@ -582,6 +632,16 @@ dependencies = [
"digest",
]
[[package]]
name = "sized-chunks"
version = "0.6.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "16d69225bde7a69b235da73377861095455d298f2b970996eec25ddbb42b3d1e"
dependencies = [
"bitmaps",
"typenum",
]
[[package]]
name = "smallvec"
version = "1.10.0"
......
Cargo.toml
View file @ ab3d2a84
......@@ -7,15 +7,17 @@ members = [
[workspace.dependencies]
anyhow = "1.0"
bumpalo = "3.11.1"
clap = { version = "4.0.10", features = ["derive"] }
derive_more = "0.99.17"
im-rc = "15.1.0"
num-bigint = "0.4"
[workspace.package]
authors = [
"Arthur Adjedj",
"Augustin Albert",
"Lucas Tabary-Maujean",
"Vincent Lafeychine"
"Vincent Lafeychine",
"Lucas Tabary-Maujean"
]
license = "GPL-3.0-or-later"
kernel/Cargo.toml
View file @ ab3d2a84
......@@ -6,7 +6,9 @@ authors.workspace = true
license.workspace = true
[dependencies]
bumpalo.workspace = true
derive_more.workspace = true
im-rc.workspace = true
num-bigint.workspace = true
[dev-dependencies]
......
kernel/src/command.rs
View file @ ab3d2a84
use crate::environment::Environment;
use crate::error::Result;
use crate::term::Term;
use crate::{Arena, Term};
#[derive(Debug, Eq, PartialEq)]
pub enum Command {
Define(String, Option<Term>, Term),
pub enum Command<'arena> {
Define(&'arena str, Option<Term<'arena>>, Term<'arena>),
CheckType(Term, Term),
CheckType(Term<'arena>, Term<'arena>),
GetType(Term),
GetType(Term<'arena>),
}
impl Command {
pub fn process(self, env: &mut Environment) -> Result<Option<Term>> {
impl<'arena> Command<'arena> {
pub fn process(self, env: &mut Arena<'arena>) -> Result<'arena, Option<Term<'arena>>> {
match self {
Command::Define(s, None, term) => term
.infer(env)
.and_then(|t| env.insert(s, term, t).map(|_| None)),
Command::Define(s, Some(t), term) => term
.check(&t, env)
.and_then(|_| env.insert(s, term, t).map(|_| None)),
Command::CheckType(t1, t2) => t1.check(&t2, env).map(|_| None),
Command::GetType(t) => t.infer(env).map(Some),
Command::Define(s, None, term) => {
env.infer(term)?;
env.bind(s, term);
Ok(None)
}
Command::Define(s, Some(t), term) => {
env.check(term, t)?;
env.bind(s, term);
Ok(None)
}
Command::CheckType(t1, t2) => {
env.check(t1, t2)?;
Ok(None)
}
Command::GetType(t) => env.infer(t).map(Some),
}
}
}
#[cfg(test)]
mod tests {
use super::*;
use num_bigint::BigUint;
fn simple_env() -> Environment {
Environment::new()
.insert(
"x".to_string(),
Term::Type(BigUint::from(0_u64).into()),
Term::Prop,
)
.unwrap()
.clone()
}
#[test]
fn failed_untyped_define() {
let cmd = Command::Define("x".to_string(), None, Term::Prop);
let mut env = simple_env();
assert!(cmd.process(&mut env).is_err());
assert_eq!(env, simple_env());
}
#[test]
fn successful_untyped_define() {
let cmd = Command::Define("y".to_string(), None, Term::Prop);
let mut env = simple_env();
assert!(cmd.process(&mut env).is_ok());
assert_eq!(
env,
*(simple_env()
.insert(
"y".to_string(),
Term::Prop,
Term::Type(BigUint::from(0_u64).into())
)
.unwrap())
);
}
#[test]
fn failed_typed_define() {
let cmd = Command::Define(
"y".to_string(),
Some(Term::Type(BigUint::from(1_u64).into())),
Term::Prop,
);
let mut env = simple_env();
assert!(cmd.process(&mut env).is_err());
assert_eq!(env, simple_env());
}
#[test]
fn successful_typed_define() {
let cmd = Command::Define(
"y".to_string(),
Some(Term::Type(BigUint::from(0_u64).into())),
Term::Prop,
);
let mut env = simple_env();
assert!(cmd.process(&mut env).is_ok());
assert_eq!(
env,
*(simple_env()
.insert(
"y".to_string(),
Term::Prop,
Term::Type(BigUint::from(0_u64).into())
)
.unwrap())
);
}
#[test]
fn failed_checktype() {
let cmd = Command::CheckType(Term::Prop, Term::Prop);
let mut env = simple_env();
assert!(cmd.process(&mut env).is_err());
assert!(env == simple_env());
}
#[test]
fn successful_checktype() {
let cmd = Command::CheckType(Term::Prop, Term::Type(BigUint::from(0_u64).into()));
let mut env = simple_env();
assert!(cmd.process(&mut env).is_ok());
assert_eq!(env, simple_env());
}
#[test]
fn failed_gettype() {
let cmd = Command::GetType(Term::Const("y".to_string()));
let mut env = simple_env();
assert!(cmd.process(&mut env).is_err());
assert!(env == simple_env());
}
#[test]
fn successful_gettype() {
let cmd = Command::GetType(Term::Prop);
let mut env = simple_env();
assert!(cmd.process(&mut env).is_ok());
assert_eq!(env, simple_env());
}
}
mod tests {}
kernel/src/declaration.rs 0 → 100644
View file @ ab3d2a84
use crate::term::Term;
use crate::universe::UniverseLevel;
use crate::KernelError;
/// Declarations constructed through commands. A declaration describes a constant in the environment, whether it's a definition with
/// a corresponding term, or an axiom with only a type.
/// univ_vars corresponds to the number of universe variables bound to the declaration.
/// No universe variable can be "free" in a term, meaning that for all Var(i) in ty or term, i<univ_vars.
/// Additionally, ty and term *should* in theory always have the same number of universe variables, and as such, only a single method is needed.
/// However, additional checks to ensure this invariant will have to be put in place. For now, when constructing declarations, only the number of
/// universes in ty are counted.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Declaration {
ty: Term,
term: Option<Term>,
univ_vars: usize,
}
impl Declaration {
pub fn make(term: Option<Term>, ty: Term) -> Declaration {
Declaration {
ty: ty.clone(),
term,
univ_vars: ty.univ_vars(),
}
}
/// Returns the type linked to a definition in a given environment.
pub fn get_type(&self, vec: &[UniverseLevel]) -> Result<Term, KernelError> {
if self.univ_vars != vec.len() {
Err(KernelError::WrongNumberOfUniverseArguments(
self.univ_vars,
vec.len(),
))
} else {
Ok(self.ty.substitute_univs(vec))
}
}
/// Returns the type linked to a definition in a given environment.
pub fn get_type_free_univ(&self) -> Term {
self.ty.clone()
}
/// Returns the term linked to a definition in a given environment.
/// Since the declaration might be an axiom, it might not have an associated term to reduce to, hence the Option.
pub fn get_term(&self, vec: &[UniverseLevel]) -> Result<Option<Term>, KernelError> {
if self.univ_vars != vec.len() {
Err(KernelError::WrongNumberOfUniverseArguments(
self.univ_vars,
vec.len(),
))
} else {
Ok(self.clone().term.map(|x| x.substitute_univs(vec)))
}
}
}
kernel/src/environment.rs
View file @ ab3d2a84
use crate::error::{Error, Result};
use crate::declaration::Declaration;
use crate::error::KernelError;
use crate::term::Term;
use derive_more::{Deref, DerefMut, Display};
use crate::universe::UniverseLevel;
use derive_more::From;
use std::collections::{hash_map, HashMap};
/// Global Environment, contains the term and type of every definitions, denoted by their strings.
#[derive(Clone, Default, Debug, Deref, DerefMut, Eq, PartialEq)]
pub struct Environment(HashMap<String, (Term, Term)>);
/// Errors that can occur, at runtime, during environment manipulation.
#[non_exhaustive]
#[derive(Clone, Debug, Display, Eq, PartialEq)]
pub enum EnvironmentError {
#[display(fmt = "{} is already defined", _0)]
AlreadyDefined(String),
#[display(fmt = "variable {} is not found", _0)]
VariableNotFound(String),
}
#[derive(Clone, Default, Debug, From, PartialEq, Eq)]
pub struct Environment(HashMap<String, Declaration>);
impl Environment {
/// Creates an empty environment.
......@@ -24,25 +15,46 @@ impl Environment {
Self::default()
}
/// Creates a new environment binding s with (t1,t2)
pub(crate) fn insert(&mut self, s: String, t1: Term, t2: Term) -> Result<&Self> {
if let hash_map::Entry::Vacant(e) = self.entry(s.clone()) {
e.insert((t1, t2));
pub fn insert(&mut self, s: String, decl: Declaration) -> Result<&Self, KernelError> {
if let hash_map::Entry::Vacant(e) = self.0.entry(s.clone()) {
e.insert(decl);
Ok(self)
} else {
Err(Error {
kind: EnvironmentError::AlreadyDefined(s).into(),
})
Err(KernelError::AlreadyDefined(s))
}
}
/// Creates a new environment binding s with t1 : t2
pub fn insert_def(&mut self, s: String, t1: Term, t2: Term) -> Result<&Self, KernelError> {
self.insert(s, Declaration::make(Some(t1), t2))
}
/// Creates a new environment binding s with an axiom of type ty
pub fn insert_axiom(&mut self, s: String, ty: Term) -> Result<&Self, KernelError> {
self.insert(s, Declaration::make(None, ty))
}
/// Returns the term linked to a definition in a given environment.
pub(crate) fn get_term(&self, s: &String) -> Option<Term> {
self.get(s).map(|(t, _)| t.clone())
pub fn get_term(&self, s: &String, vec: &[UniverseLevel]) -> Result<Option<Term>, KernelError> {
match self.0.get(s) {
Some(decl) => Ok(decl.get_term(vec)?),
None => Err(KernelError::ConstNotFound(s.clone())),
}
}
/// Returns the type linked to a definition in a given environment.
pub(crate) fn get_type(&self, s: &String) -> Option<Term> {
self.get(s).map(|(_, t)| t.clone())
pub fn get_type(&self, s: &String, vec: &[UniverseLevel]) -> Result<Term, KernelError> {
match self.0.get(s) {
Some(decl) => Ok(decl.get_type(vec)?),
None => Err(KernelError::ConstNotFound(s.clone())),
}
}
/// Returns the type linked to a definition in a given environment.
pub fn get_type_free_univ(&self, s: &String) -> Result<Term, KernelError> {
match self.0.get(s) {
Some(decl) => Ok(decl.get_type_free_univ()),
None => Err(KernelError::ConstNotFound(s.clone())),
}
}
}
kernel/src/error.rs
View file @ ab3d2a84
use crate::environment::EnvironmentError;
use crate::type_checker::TypeCheckerError;
use derive_more::{Display, From};
use crate::term::arena::Term;
use crate::term::builders::extern_::DefinitionError;
use crate::type_checker::TypeCheckerError;
/// Type representing kernel errors.
#[derive(Clone, Debug, Display, Eq, PartialEq)]
pub struct Error {
pub struct Error<'arena> {
/// The kind of form error that occurred.
pub kind: ErrorKind,
pub kind: ErrorKind<'arena>,
// This struct might contains more fields in the future (waiting for #15)
}
#[non_exhaustive]
#[derive(Clone, Debug, Display, Eq, PartialEq, From)]
pub enum ErrorKind {
Environment(EnvironmentError),
TypeChecker(TypeCheckerError),
pub enum ErrorKind<'arena> {
TypeChecker(TypeCheckerError<'arena>),
Definition(DefinitionError<'arena>),
}
impl std::error::Error for Error {}
impl<'arena> std::error::Error for Error<'arena> {}
pub type Result<T> = std::result::Result<T, Error>;
pub type Result<'arena, T> = std::result::Result<T, Error<'arena>>;
pub(crate) type ResultTerm<'arena> = Result<'arena, Term<'arena>>;
kernel/src/lib.rs
View file @ ab3d2a84
//! TODO: Make a documentation (#15)
#![feature(box_patterns)]
#![feature(box_syntax)]
#![feature(once_cell)]
#![feature(trait_alias)]
mod command;
mod environment;
mod error;
mod location;
mod term;
mod type_checker;
mod declaration;
mod universe;
pub use self::command::Command;
pub use self::environment::Environment;
pub use self::location::{Location, Position};
pub use self::term::Term;
pub use self::term::arena::{use_arena, Arena, Term};
pub use self::term::builders::extern_ as builders;
pub use declaration::Declaration;
pub use universe::UniverseLevel;
kernel/src/term.rs deleted 100644 → 0
View file @ a28c6526
use crate::environment::Environment;
use derive_more::{Add, Display, From, Into, Sub};
use num_bigint::BigUint;
#[derive(
Add, Copy, Clone, Debug, Default, Display, Eq, PartialEq, From, Into, Sub, PartialOrd, Ord,
)]
pub struct DeBruijnIndex(usize);
#[derive(Add, Clone, Debug, Default, Display, Eq, From, Sub, PartialEq, PartialOrd, Ord)]
pub struct UniverseLevel(BigUint);
#[derive(Clone, Debug, Display, Eq, PartialEq)]
pub enum Term {
#[display(fmt = "{}", _0)]
Var(DeBruijnIndex),
#[display(fmt = "{}", _0)]
Const(String),
#[display(fmt = "Prop")]
Prop,
#[display(fmt = "Type {}", _0)]
Type(UniverseLevel),
#[display(fmt = "{} {}", _0, _1)]
App(Box<Term>, Box<Term>),
#[display(fmt = "\u{003BB} {} \u{02192} {}", _0, _1)]
Abs(Box<Term>, Box<Term>),
#[display(fmt = "\u{03A0} {} \u{02192} {}", _0, _1)]
Prod(Box<Term>, Box<Term>),
}
use Term::*;
impl Term {
/// Apply one step of β-reduction, using leftmost outermost evaluation strategy.
pub fn beta_reduction(&self, env: &Environment) -> Term {
match self {
App(box Abs(_, box t1), box t2) => t1.substitute(t2, 1),
App(box t1, box t2) => {
let t1_new = t1.beta_reduction(env);
if t1.clone() == t1_new {
App(box t1_new, box t2.beta_reduction(env))
} else {
App(box t1_new, box t2.clone())
}
}
Abs(x, box t) => Abs(x.clone(), box t.beta_reduction(env)),
Prod(x, box t) => Prod(x.clone(), box t.beta_reduction(env)),
Const(s) => env.get_term(s).unwrap(),
_ => self.clone(),
}
}
pub(crate) fn shift(&self, offset: usize, depth: usize) -> Term {
match self {
Var(i) if *i > depth.into() => Var(*i + offset.into()),
App(box t1, box t2) => App(box t1.shift(offset, depth), box t2.shift(offset, depth)),
Abs(t1, box t2) => Abs(box t1.shift(offset, depth), box t2.shift(offset, depth + 1)),
Prod(t1, box t2) => Prod(box t1.shift(offset, depth), box t2.shift(offset, depth + 1)),
_ => self.clone(),
}
}
pub(crate) fn substitute(&self, rhs: &Term, depth: usize) -> Term {
match self {
Var(i) if *i == depth.into() => rhs.shift(depth - 1, 0),
Var(i) if *i > depth.into() => Var(*i - 1.into()),
App(l, r) => App(box l.substitute(rhs, depth), box r.substitute(rhs, depth)),
Abs(t, term) => Abs(
box t.substitute(rhs, depth),
box term.substitute(rhs, depth + 1),
),
Prod(t, term) => Prod(
box t.substitute(rhs, depth),
box term.substitute(rhs, depth + 1),
),
_ => self.clone(),
}
}
/// Returns the normal form of a term in a given environment.
///
/// This function is computationally expensive and should only be used for Reduce/Eval commands, not when type-checking.
pub fn normal_form(self, env: &Environment) -> Term {
let mut res = self.beta_reduction(env);
let mut temp = self;
while res != temp {
temp = res.clone();
res = res.beta_reduction(env)
}
res
}
/// Returns the weak-head normal form of a term in a given environment.
// TODO make whnf more lax, it shouldn't reduce applications in which the head is a neutral term. (#34)
pub fn whnf(&self, env: &Environment) -> Term {
match self {
App(box t, t2) => match t.whnf(env) {
whnf @ Abs(_, _) => App(box whnf, t2.clone()).beta_reduction(env).whnf(env),
_ => self.clone(),
},
Const(s) => env.get_term(s).unwrap(),
_ => self.clone(),
}
}
}
#[cfg(test)]
mod tests {
// /!\ most of these tests are on ill-typed terms and should not be used for further testings
use super::*;
#[test]
fn simple_subst() {
// λx.(λy.x y) x
let term = Abs(
box Prop,
box App(
box Abs(box Prop, box App(box Var(2.into()), box Var(1.into()))),
box Var(1.into()),
),
);
// λx.x x
let reduced = Abs(box Prop, box App(box Var(1.into()), box Var(1.into())));
assert_eq!(term.beta_reduction(&Environment::new()), reduced);
}
#[test]
fn complex_subst() {
// (λa.λb.λc.a (λd.λe.e (d b)) (λ_.c) (λd.d)) (λa.λb.a b)
let term = App(
box Abs(
box Prop,
box Abs(
box Prop,
box Abs(
box Prop,
box App(
box App(
box App(
box Var(3.into()),
box Abs(
box Prop,
box Abs(
box Prop,
box App(
box Var(1.into()),
box App(box Var(2.into()), box Var(4.into())),
),
),
),
),
box Abs(box Prop, box Var(2.into())),
),
box Abs(box Prop, box Var(1.into())),
),
),
),
),
box Abs(
box Prop,
box Abs(box Prop, box App(box Var(2.into()), box Var(1.into()))),
),
);
let term_step_1 = Abs(
box Prop,
box Abs(
box Prop,
box App(
box App(
box App(
box Abs(
box Prop,
box Abs(box Prop, box App(box Var(2.into()), box Var(1.into()))),
),
box Abs(
box Prop,
box Abs(
box Prop,
box App(
box Var(1.into()),
box App(box Var(2.into()), box Var(4.into())),
),
),
),
),
box Abs(box Prop, box Var(2.into())),
),
box Abs(box Prop, box Var(1.into())),
),
),
);
let term_step_2 = Abs(
box Prop,
box Abs(
box Prop,
box App(
box App(
box Abs(
box Prop,
box App(
box Abs(
box Prop,
box Abs(
box Prop,
box App(
box Var(1.into()),
box App(box Var(2.into()), box Var(5.into())),
),
),
),
box Var(1.into()),
),
),
box Abs(box Prop, box Var(2.into())),
),
box Abs(box Prop, box Var(1.into())),
),
),
);
let term_step_3 = Abs(
box Prop,
box Abs(
box Prop,
box App(
box App(
box Abs(
box Prop,
box Abs(
box Prop,
box App(
box Var(1.into()),
box App(box Var(2.into()), box Var(4.into())),
),
),
),
box Abs(box Prop, box Var(2.into())),
),
box Abs(box Prop, box Var(1.into())),
),
),
);
let term_step_4 = Abs(
box Prop,
box Abs(
box Prop,
box App(
box Abs(
box Prop,
box App(
box Var(1.into()),
box App(box Abs(box Prop, box Var(3.into())), box Var(3.into())),
),
),
box Abs(box Prop, box Var(1.into())),
),
),
);
let term_step_5 = Abs(
box Prop,
box Abs(
box Prop,
box App(
box Abs(box Prop, box Var(1.into())),
box App(box Abs(box Prop, box Var(2.into())), box Var(2.into())),
),
),
);
let term_step_6 = Abs(
box Prop,
box Abs(
box Prop,
box App(box Abs(box Prop, box Var(2.into())), box Var(2.into())),
),
);
// λa.λb.b
let term_step_7 = Abs(box Prop, box Abs(box Prop, box Var(1.into())));
let env = Environment::new();
assert_eq!(term.beta_reduction(&env), term_step_1);
assert_eq!(term_step_1.beta_reduction(&env), term_step_2);
assert_eq!(term_step_2.beta_reduction(&env), term_step_3);
assert_eq!(term_step_3.beta_reduction(&env), term_step_4);
assert_eq!(term_step_4.beta_reduction(&env), term_step_5);
assert_eq!(term_step_5.beta_reduction(&env), term_step_6);
assert_eq!(term_step_6.beta_reduction(&env), term_step_7);
assert_eq!(term_step_7.beta_reduction(&env), term_step_7);
}
#[test]
fn shift_prod() {
let reduced = Prod(box Prop, box Var(1.into()));
let term = App(box Abs(box Prop, box reduced.clone()), box Prop);
assert_eq!(term.beta_reduction(&Environment::new()), reduced)
}
#[test]
fn const_subst() {
let id_prop = Prod(box Prop, box Prod(box Var(1.into()), box Var(1.into())));
let mut env = Environment::new();
env.insert("foo".into(), id_prop.clone(), Prop).unwrap();
assert_eq!(Const("foo".into()).beta_reduction(&env), id_prop);
}
#[test]
fn prod_beta_red() {
let term = Prod(
box Prop,
box App(box Abs(box Prop, box Var(1.into())), box Var(1.into())),
);
let reduced = Prod(box Prop, box Var(1.into()));
assert_eq!(term.beta_reduction(&Environment::new()), reduced);
}
#[test]
fn app_red_rhs() {
let term = Abs(
box Prop,
box App(
box Var(1.into()),
box App(box Abs(box Prop, box Var(1.into())), box Var(1.into())),
),
);
let reduced = Abs(box Prop, box App(box Var(1.into()), box Var(1.into())));
assert_eq!(term.beta_reduction(&Environment::new()), reduced);
}
}
kernel/src/term/arena.rs 0 → 100644
View file @ ab3d2a84
use std::cell::OnceCell;
use std::collections::{HashMap, HashSet};
use std::fmt::Debug;
use std::hash::Hash;
use std::marker::PhantomData;
use std::ops::Deref;
use bumpalo::Bump;
use derive_more::{Add, Display, From, Into, Sub};
use im_rc::hashmap::HashMap as ImHashMap;
use num_bigint::BigUint;
use crate::error::ResultTerm;
#[derive(
Add, Copy, Clone, Debug, Default, Display, Eq, PartialEq, From, Into, Sub, PartialOrd, Ord, Hash,
)]
pub struct DeBruijnIndex(usize);
#[derive(Add, Clone, Debug, Default, Display, Eq, From, Sub, PartialEq, PartialOrd, Ord, Hash)]
pub struct UniverseLevel(BigUint);
pub struct Arena<'arena> {
alloc: &'arena Bump,
_phantom: PhantomData<*mut &'arena ()>,
hashcons: HashSet<&'arena Node<'arena>>,
named_terms: HashMap<&'arena str, Term<'arena>>,
mem_subst: HashMap<(Term<'arena>, Term<'arena>, usize), Term<'arena>>,
// a shift hashmap may also be added when the is_certainly_closed also is
}
#[derive(Clone, Copy, Display, Eq)]
#[display(fmt = "{}", "_0.payload")]
// PhantomData is a marker to ensure invariance over the 'arena lifetime.
pub struct Term<'arena>(&'arena Node<'arena>, PhantomData<*mut &'arena ()>);
// the rest of the struct is very verbose and useless for debugging
impl<'arena> Debug for Term<'arena> {
fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
self.0.payload.fmt(f)
}
}
// no name storage here: meaning consts are known and can be found, but no pretty printing is
// possible so far.
#[derive(Debug)]
struct Node<'arena> {
payload: Payload<'arena>,
head_normal_form: OnceCell<Term<'arena>>,
type_: OnceCell<Term<'arena>>,
//
// is_certainly_closed: boolean underapproximation of whether a term is closed, which can
// greatly improve performance in shifting
}
#[derive(Clone, Debug, Display, Eq, PartialEq, Hash)]
pub enum Payload<'arena> {
#[display(fmt = "{}", _0)]
Var(DeBruijnIndex, Term<'arena>),
#[display(fmt = "Prop")]
Prop,
#[display(fmt = "Type {}", _0)]
Type(UniverseLevel),
#[display(fmt = "{} {}", _0, _1)]
App(Term<'arena>, Term<'arena>),
#[display(fmt = "\u{003BB} {} \u{02192} {}", _0, _1)]
Abs(Term<'arena>, Term<'arena>),
#[display(fmt = "\u{03A0} {} \u{02192} {}", _0, _1)]
Prod(Term<'arena>, Term<'arena>),
}
/// (TODO PRECISE DOCUMENTATION) make use of unicity invariant to speed up equality test
impl<'arena> PartialEq<Term<'arena>> for Term<'arena> {
fn eq(&self, x: &Term<'arena>) -> bool {
std::ptr::eq(self.0, x.0)
}
}
/// (TODO PRECISE DOCUMENTATION) make use of unicity invariant to speed up equality test
impl<'arena> Hash for Term<'arena> {
fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
std::ptr::hash(self.0, state)
}
}
impl<'arena> PartialEq<Node<'arena>> for Node<'arena> {
fn eq(&self, x: &Node<'arena>) -> bool {
self.payload == x.payload
}
}
impl<'arena> Eq for Node<'arena> {}
/// (TODO PRECISE DOCUMENTATION) Only the payload matters and caracterises the value. Changing
/// OnceCells is *guaranteed* to have no impact on that.
impl<'arena> Hash for Node<'arena> {
fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
self.payload.hash(state);
}
}
pub fn use_arena<F, T>(f: F) -> T
where
F: for<'arena> FnOnce(&mut Arena<'arena>) -> T,
{
let alloc = Bump::new();
let mut arena = Arena::new(&alloc);
f(&mut arena)
}
use super::builders::extern_::BuilderTrait;
use Payload::*;
impl<'arena> Arena<'arena> {
/// (TODO DOC.) Allocate a new memory arena.
fn new(alloc: &'arena Bump) -> Self {
Arena {
alloc,
_phantom: PhantomData,
hashcons: HashSet::new(),
named_terms: HashMap::new(),
mem_subst: HashMap::new(),
}
}
pub fn store_name(&mut self, name: &str) -> &'arena str {
self.alloc.alloc_str(name)
}
pub fn bind(&mut self, name: &str, t: Term<'arena>) {
let name = self.store_name(name);
self.named_terms.insert(name, t);
}
pub fn get_binding(&self, name: &str) -> Option<Term<'arena>> {
self.named_terms.get(name).copied()
}
/// (TODO DOC.) there are concurrent designs here: either hashcons take a Node and functions
/// which use it immediatly intend to compute the type and/or WHNF of the term, or this is
/// postponed and computed lazily. This iteration chooses the second approach.
fn hashcons(&mut self, n: Payload<'arena>) -> Term<'arena> {
let nn = Node {
payload: n,
head_normal_form: OnceCell::new(),
type_: OnceCell::new(),
};
match self.hashcons.get(&nn) {
Some(addr) => Term(addr, PhantomData),
None => {
let addr = self.alloc.alloc(nn);
self.hashcons.insert(addr);
Term(addr, PhantomData)
}
}
}
pub(crate) fn var(&mut self, index: DeBruijnIndex, type_: Term<'arena>) -> Term<'arena> {
self.hashcons(Var(index, type_))
}
pub(crate) fn prop(&mut self) -> Term<'arena> {
self.hashcons(Prop)
}
pub(crate) fn type_(&mut self, level: UniverseLevel) -> Term<'arena> {
self.hashcons(Type(level))
}
pub(crate) fn type_usize(&mut self, level: usize) -> Term<'arena> {
self.hashcons(Type(BigUint::from(level).into()))
}
pub(crate) fn app(&mut self, u1: Term<'arena>, u2: Term<'arena>) -> Term<'arena> {
self.hashcons(App(u1, u2))
}
pub(crate) fn abs(&mut self, arg_type: Term<'arena>, u: Term<'arena>) -> Term<'arena> {
self.hashcons(Abs(arg_type, u))
}
pub(crate) fn prod(&mut self, arg_type: Term<'arena>, u: Term<'arena>) -> Term<'arena> {
self.hashcons(Prod(arg_type, u))
}
#[inline]
pub fn build_from_extern<'build, F: BuilderTrait<'build, 'arena>>(
&mut self,
f: F,
) -> ResultTerm<'arena>
where
'arena: 'build,
{
f(self, &ImHashMap::new(), 0.into())
}
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>,
{
match self.mem_subst.get(key) {
Some(res) => *res,
None => {
let res = f(self);
self.mem_subst.insert(*key, res);
res
}
}
}
}
impl<'arena> Term<'arena> {
pub(crate) fn get_whnf_or_init<F>(self, f: F) -> Term<'arena>
where
F: FnOnce() -> Term<'arena>,
{
*self.0.head_normal_form.get_or_init(f)
}
pub(crate) fn get_type_or_try_init<F>(self, f: F) -> ResultTerm<'arena>
where
F: FnOnce() -> ResultTerm<'arena>,
{
self.0.type_.get_or_try_init(f).copied()
}
}
impl<'arena> Deref for Term<'arena> {
type Target = Payload<'arena>;
fn deref(&self) -> &Self::Target {
&self.0.payload
}
}
kernel/src/term/builders.rs 0 → 100644
View file @ ab3d2a84
use super::arena::{Arena, DeBruijnIndex, Term, UniverseLevel};
#[cfg(test)]
pub(crate) mod intern {
use super::*;
impl<'arena> Arena<'arena> {
pub(crate) fn build<F: Builder<'arena>>(&mut self, f: F) -> Term<'arena> {
f(self)
}
}
impl<'arena> Term<'arena> {
pub(crate) fn into(self) -> impl Builder<'arena> {
move |_: &mut Arena<'arena>| self
}
}
pub(crate) trait Builder<'arena> = FnOnce(&mut Arena<'arena>) -> Term<'arena>;
#[inline]
pub(crate) fn prop<'arena>() -> impl Builder<'arena> {
|env: &mut Arena<'arena>| env.prop()
}
#[inline]
pub(crate) fn type_<'arena>(level: UniverseLevel) -> impl Builder<'arena> {
move |env: &mut Arena<'arena>| env.type_(level)
}
#[inline]
pub(crate) fn var<'arena, F: Builder<'arena>>(
index: DeBruijnIndex,
type_: F,
) -> impl Builder<'arena> {
move |env: &mut Arena<'arena>| {
let ty = type_(env);
env.var(index, ty)
}
}
#[inline]
pub(crate) fn app<'arena, F1: Builder<'arena>, F2: Builder<'arena>>(
u1: F1,
u2: F2,
) -> impl Builder<'arena> {
|env: &mut Arena<'arena>| {
let u1 = u1(env);
let u2 = u2(env);
env.app(u1, u2)
}
}
#[inline]
pub(crate) fn abs<'arena, F1: Builder<'arena>, F2: Builder<'arena>>(
u1: F1,
u2: F2,
) -> impl Builder<'arena> {
|env: &mut Arena<'arena>| {
let u1 = u1(env);
let u2 = u2(env);
env.abs(u1, u2)
}
}
#[inline]
pub(crate) fn prod<'arena, F1: Builder<'arena>, F2: Builder<'arena>>(
u1: F1,
u2: F2,
) -> impl Builder<'arena> {
|env: &mut Arena<'arena>| {
let u1 = u1(env);
let u2 = u2(env);
env.prod(u1, u2)
}
}
}
/// These functions are available publicly, to the attention of the parser. They manipulate
/// objects with a type morally equal to (Env -> Term), where Env is a working environment used
/// in term construction from the parser.
/// This is done as a way to elengantly keep the logic encapsulated in the kernel, but let the
/// parser itself explore the term.
pub mod extern_ {
use derive_more::Display;
use im_rc::hashmap::HashMap as ImHashMap;
use super::*;
use crate::error::{Error, ResultTerm};
#[non_exhaustive]
#[derive(Clone, Debug, Display, Eq, PartialEq)]
pub enum DefinitionError<'arena> {
#[display(fmt = "unknown identifiant {}", _0)]
ConstNotFound(&'arena str),
}
pub type Environment<'build, 'arena> = ImHashMap<&'build str, (DeBruijnIndex, Term<'arena>)>;
pub trait BuilderTrait<'build, 'arena> = FnOnce(
&mut Arena<'arena>,
&Environment<'build, 'arena>,
DeBruijnIndex,
) -> ResultTerm<'arena>;
#[inline]
pub fn var<'build, 'arena>(name: &'build str) -> impl BuilderTrait<'build, 'arena> {
move |arena: &mut Arena<'arena>, env: &Environment<'build, 'arena>, depth| {
env.get(name)
.map(|(bind_depth, term)| {
// maybe find a way to make this call efficiently lazy
let var_type = arena.shift(*term, usize::from(depth - *bind_depth), 0);
arena.var(depth - *bind_depth, var_type)
})
.or_else(|| arena.get_binding(name))
.ok_or(Error {
kind: DefinitionError::ConstNotFound(arena.store_name(name)).into(),
})
}
}
#[inline]
pub fn prop<'build, 'arena>() -> impl BuilderTrait<'build, 'arena> {
|arena: &mut Arena<'arena>, _: &Environment<'build, 'arena>, _| Ok(arena.prop())
}
#[inline]
pub fn type_<'build, 'arena>(level: UniverseLevel) -> impl BuilderTrait<'build, 'arena> {
move |arena: &mut Arena<'arena>, _: &Environment<'build, 'arena>, _| Ok(arena.type_(level))
}
#[inline]
pub 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()))
}
}
#[inline]
pub fn app<
'build,
'arena,
F1: BuilderTrait<'build, 'arena>,
F2: BuilderTrait<'build, 'arena>,
>(
u1: F1,
u2: F2,
) -> impl BuilderTrait<'build, 'arena> {
|arena: &mut Arena<'arena>, env: &Environment<'build, 'arena>, depth| {
let u1 = u1(arena, env, depth)?;
let u2 = u2(arena, env, depth)?;
Ok(arena.app(u1, u2))
}
}
#[inline]
pub fn abs<
'build,
'arena,
F1: BuilderTrait<'build, 'arena>,
F2: BuilderTrait<'build, 'arena>,
>(
name: &'build str,
arg_type: F1,
body: F2,
) -> impl BuilderTrait<'build, 'arena> {
move |arena: &mut Arena<'arena>, env: &Environment<'build, 'arena>, depth| {
let arg_type = arg_type(arena, env, depth)?;
let env = env.update(name, (depth, arg_type));
let body = body(arena, &env, depth + 1.into())?;
Ok(arena.abs(arg_type, body))
}
}
#[inline]
pub fn prod<
'build,
'arena,
F1: BuilderTrait<'build, 'arena>,
F2: BuilderTrait<'build, 'arena>,
>(
name: &'build str,
arg_type: F1,
body: F2,
) -> impl BuilderTrait<'build, 'arena> {
move |arena: &mut Arena<'arena>, env: &Environment<'build, 'arena>, depth| {
let arg_type = arg_type(arena, env, depth)?;
let env = env.update(name, (depth, arg_type));
let body = body(arena, &env, depth + 1.into())?;
Ok(arena.prod(arg_type, body))
}
}
pub enum Builder<'r> {
Var(&'r str),
Type(usize),
Prop,
App(&'r Builder<'r>, &'r Builder<'r>),
Abs(&'r str, &'r Builder<'r>, &'r Builder<'r>),
Prod(&'r str, &'r Builder<'r>, &'r Builder<'r>),
}
impl<'build> Builder<'build> {
pub fn realise<'arena>(&self, arena: &mut Arena<'arena>) -> ResultTerm<'arena> {
arena.build_from_extern(self.partial_application())
}
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)
}
}
fn realise_in_context<'arena>(
&self,
arena: &mut Arena<'arena>,
env: &Environment<'build, 'arena>,
depth: DeBruijnIndex,
) -> ResultTerm<'arena> {
use Builder::*;
match *self {
Var(s) => var(s)(arena, env, depth),
Type(level) => type_usize(level)(arena, env, depth),
Prop => prop()(arena, env, depth),
App(l, r) => {
app(l.partial_application(), r.partial_application())(arena, env, depth)
}
Abs(s, arg, body) => {
abs(s, arg.partial_application(), body.partial_application())(arena, env, depth)
}
Prod(s, arg, body) => {
prod(s, arg.partial_application(), body.partial_application())(
arena, env, depth,
)
}
}
}
}
}
kernel/src/term/calculus.rs 0 → 100644
View file @ ab3d2a84
use super::arena::{Arena, Payload, Term};
use Payload::*;
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> {
match *t {
App(t1, t2) => match *t1 {
Abs(_, t1) => self.substitute(t1, t2, 1),
_ => {
let t1_new = self.beta_reduction(t1);
if t1_new == t1 {
let t2_new = self.beta_reduction(t2);
self.app(t1, t2_new)
} 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,
}
}
pub(crate) fn shift(&mut self, t: Term<'arena>, offset: usize, depth: usize) -> Term<'arena> {
match *t {
Var(i, type_) if i > depth.into() => self.var(i + offset.into(), type_),
App(t1, t2) => {
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,
}
}
pub(crate) fn substitute(
&mut self,
lhs: Term<'arena>,
rhs: Term<'arena>,
depth: usize,
) -> Term<'arena> {
self.get_subst_or_init(&(lhs, rhs, depth), |arena| match *lhs {
Var(i, _) if i == depth.into() => arena.shift(rhs, depth - 1, 0),
Var(i, type_) if i > depth.into() => arena.var(i - 1.into(), type_),
App(l, r) => {
let l = arena.substitute(l, rhs, depth);
let r = arena.substitute(r, rhs, depth);
arena.app(l, r)
}
Abs(arg_type, body) => {
let arg_type = arena.substitute(arg_type, rhs, depth);
let body = arena.substitute(body, rhs, depth + 1);
arena.abs(arg_type, body)
}
Prod(arg_type, body) => {
let arg_type = arena.substitute(arg_type, rhs, depth);
let body = arena.substitute(body, rhs, depth + 1);
arena.prod(arg_type, body)
}
_ => lhs,
})
}
/// Returns the normal form of a term in a given environment.
///
/// This function is computationally expensive and should only be used for Reduce/Eval commands, not when type-checking.
pub fn normal_form(&mut self, t: Term<'arena>) -> Term<'arena> {
let mut temp = t;
let mut res = self.beta_reduction(t);
while res != temp {
temp = res;
res = self.beta_reduction(res);
}
res
}
/// Returns the weak-head normal form of a term in a given environment.
pub fn whnf(&mut self, t: Term<'arena>) -> Term<'arena> {
t.get_whnf_or_init(|| match *t {
App(t1, t2) => {
let t1 = self.whnf(t1);
match *t1 {
Abs(_, _) => {
let t = self.app(t1, t2);
let t = self.beta_reduction(t);
self.whnf(t)
}
_ => t,
}
}
_ => t,
})
}
}
#[cfg(test)]
mod tests {
// /!\ most of these tests are on ill-typed terms and should not be used for further testings
use super::super::arena::use_arena;
use super::super::builders::intern::*;
#[test]
fn simple_subst() {
use_arena(|arena| {
// λx.(λy.x y) x
let term = arena.build(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(abs(
prop(),
app(var(1.into(), prop()), var(1.into(), prop())),
));
assert_eq!(arena.beta_reduction(term), reduced);
})
}
#[test]
fn complex_subst() {
use_arena(|arena| {
// (λa.λb.λc.a (λd.λe.e (d b)) (λ_.c) (λd.d)) (λa.λb.a b)
let term = arena.build(app(
abs(
prop(),
abs(
prop(),
abs(
prop(),
app(
app(
app(
var(3.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())),
),
),
),
),
abs(
prop(),
abs(prop(), app(var(2.into(), prop()), var(1.into(), prop()))),
),
));
let term_step_1 = arena.build(abs(
prop(),
abs(
prop(),
app(
app(
app(
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(), var(2.into(), prop())),
),
abs(prop(), var(1.into(), prop())),
),
),
));
let term_step_2 = arena.build(abs(
prop(),
abs(
prop(),
app(
app(
abs(
prop(),
app(
abs(
prop(),
abs(
prop(),
app(
var(1.into(), prop()),
app(var(2.into(), prop()), var(5.into(), prop())),
),
),
),
var(1.into(), prop()),
),
),
abs(prop(), var(2.into(), prop())),
),
abs(prop(), var(1.into(), prop())),
),
),
));
let term_step_3 = arena.build(abs(
prop(),
abs(
prop(),
app(
app(
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())),
),
),
));
let term_step_4 = arena.build(abs(
prop(),
abs(
prop(),
app(
abs(
prop(),
app(
var(1.into(), prop()),
app(abs(prop(), var(3.into(), prop())), var(3.into(), prop())),
),
),
abs(prop(), var(1.into(), prop())),
),
),
));
let term_step_5 = arena.build(abs(
prop(),
abs(
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(abs(
prop(),
abs(
prop(),
app(abs(prop(), var(2.into(), prop())), var(2.into(), prop())),
),
));
// λa.λb.b
let term_step_7 = arena.build(abs(prop(), abs(prop(), var(1.into(), prop()))));
assert_eq!(arena.beta_reduction(term), term_step_1);
assert_eq!(arena.beta_reduction(term_step_1), term_step_2);
assert_eq!(arena.beta_reduction(term_step_2), term_step_3);
assert_eq!(arena.beta_reduction(term_step_3), term_step_4);
assert_eq!(arena.beta_reduction(term_step_4), term_step_5);
assert_eq!(arena.beta_reduction(term_step_5), term_step_6);
assert_eq!(arena.beta_reduction(term_step_6), term_step_7);
assert_eq!(arena.beta_reduction(term_step_7), term_step_7);
})
}
#[test]
fn shift_prod() {
use_arena(|arena| {
let reduced = arena.build(prod(prop(), var(1.into(), prop())));
let term = arena.build(app(abs(prop(), reduced.into()), prop()));
assert_eq!(arena.beta_reduction(term), reduced)
})
}
#[test]
fn prod_beta_red() {
use_arena(|arena| {
let term = arena.build(prod(
prop(),
app(abs(prop(), var(1.into(), prop())), var(1.into(), prop())),
));
let reduced = arena.build(prod(prop(), var(1.into(), prop())));
assert_eq!(arena.beta_reduction(term), reduced);
})
}
#[test]
fn app_red_rhs() {
use_arena(|arena| {
let term = arena.build(abs(
prop(),
app(
var(1.into(), prop()),
app(abs(prop(), var(1.into(), prop())), var(1.into(), prop())),
),
));
let reduced = arena.build(abs(
prop(),
app(var(1.into(), prop()), var(1.into(), prop())),
));
assert_eq!(arena.beta_reduction(term), reduced);
})
}
}
kernel/src/term/mod.rs 0 → 100644
View file @ ab3d2a84
pub mod arena;
pub mod builders;
pub mod calculus;
kernel/src/type_checker.rs
View file @ ab3d2a84
This diff is collapsed.
kernel/src/universe.rs 0 → 100644
View file @ ab3d2a84
use std::fmt::Display;
use std::fmt::Formatter;
use std::ops::Add;
use std::marker::PhantomData;
use std::cell::OnceCell;
use derive_more::{Add, Display, From, Into, Sub};
#[derive(Clone, Debug, Default, PartialEq, Eq)]
pub enum LevelPayload<'arena> {
#[default]
Zero,
Succ(Level<'arena>),
Max(Level<'arena>,Level<'arena>),
IMax(Level<'arena>,Level<'arena>),
Var(usize),
}
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct Level<'arena>(&'arena LevelNode<'arena>, PhantomData<*mut &'arena ()>);
#[derive(Debug, PartialEq, Eq)]
struct LevelNode<'arena> {
payload: LevelPayload<'arena>,
//
// is_certainly_closed: boolean underapproximation of whether a term is closed, which can
// greatly improve performance in shifting
}
impl Add<usize> for Level {
type Output = Self;
fn add(self, n: usize) -> Self {
if n == 0 {
self
} else {
Succ(box self.add(n - 1))
}
}
}
impl From<usize> for UniverseLevel {
fn from(n: usize) -> Self {
if n == 0 {
Zero
} else {
Succ(box (n - 1).into())
}
}
}
impl Display for UniverseLevel {
fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
write!(f, "{}", self.pretty_print())
}
}
use UniverseLevel::*;
impl UniverseLevel {
/// Helper function for pretty printing, if universe doesn't contain any variable then it gets printed as a decimal number.
fn to_numeral(&self) -> Option<usize> {
match self {
Zero => Some(0),
Succ(box u) => u.to_numeral().map(|n| n + 1),
Max(box n, box m) => n
.to_numeral()
.and_then(|n| m.to_numeral().map(|m| n.max(m))),
IMax(box n, box m) => m.to_numeral().and_then(|m| {
if m == 0 {
0.into()
} else {
n.to_numeral().map(|n| m.max(n))
}
}),
_ => None,
}
}
/// Helper function for pretty printing, if universe is of the form Succ(Succ(...(Succ(u))...)) then it gets printed as u+n.
fn plus(&self) -> (UniverseLevel, usize) {
match self {
Succ(box u) => {
let (u, n) = u.plus();
(u, n + 1)
}
_ => (self.clone(), 0),
}
}
/// Pretty prints universe levels, used to impl Display for UniverseLevel.
fn pretty_print(&self) -> String {
match self.to_numeral() {
Some(n) => n.to_string(),
None => match self {
Zero => unreachable!("Zero is a numeral"),
Succ(_) => {
let (u, n) = self.plus();
format!("{} + {}", u.pretty_print(), n)
}
Max(box n, box m) => format!("max ({}) ({})", n.pretty_print(), m.pretty_print()),
IMax(box _, box Zero) => "Zero".into(),
IMax(box n, box m @ Succ(_)) => {
format!("max ({}) ({})", n.pretty_print(), m.pretty_print())
}
IMax(box n, box m) => format!("imax ({}) ({})", n.pretty_print(), m.pretty_print()),
Var(n) => format!("u{}", n),
},
}
}
/// Is used to find the number of universe in a declaration.
pub fn univ_vars(self) -> usize {
match self {
Zero => 0,
Succ(n) => n.univ_vars(),
Max(n, m) => n.univ_vars().max(m.univ_vars()),
IMax(n, m) => n.univ_vars().max(m.univ_vars()),
Var(n) => n + 1,
}
}
/// Helper function for equality checking, used to substitute Var(i) with Z and S(Var(i)).
fn substitute_single(self, var: usize, u: UniverseLevel) -> UniverseLevel {
match self {
Zero => Zero,
Succ(n) => Succ(box n.substitute_single(var, u)),
Max(n, m) => Max(
box n.substitute_single(var, u.clone()),
box m.substitute_single(var, u),
),
IMax(n, m) => IMax(
box n.substitute_single(var, u.clone()),
box m.substitute_single(var, u),
),
Var(n) => {
if n == var {
u
} else {
Var(n)
}
}
}
}
/// General universe substitution, given a vector of universe levels, it substitutes each Var(i) with the i-th element of the vector.
pub fn substitute(self, univs: &[UniverseLevel]) -> Self {
match self {
Zero => Zero,
Succ(v) => Succ(box v.substitute(univs)),
Max(u1, u2) => Max(box u1.substitute(univs), box u2.substitute(univs)),
IMax(u1, u2) => IMax(box u1.substitute(univs), box u2.substitute(univs)),
Var(var) => univs[var].clone(),
}
}
/// Helper function for universe comparison. normalizes imax(es) as follows:
/// imax(0, u) = u
/// imax(u, 0) = u
/// imax(u, S(v)) = max(u, S(v))
/// imax(u, imax(v, w)) = max(imax(u, w), imax(v, w))
/// imax(u, max(v, w)) = max(imax(u, v), imax(u, w))
///
/// Here, the imax normalization pushes imaxes to all have a Var(i) as the second argument. To solve this last case, one needs to substitute
/// Var(i) with 0 and S(Var(i)). This gives us a consistent way to unstuck the geq-checking.
fn normalize(&self) -> Self {
match self {
IMax(box Zero, box u) => u.clone(),
IMax(_, box Zero) => Zero,
IMax(box u, box Succ(v)) => Max(box u.normalize(), box Succ(v.clone())).normalize(),
IMax(box u, box IMax(box v, box w)) => Max(
box IMax(box u.clone(), box w.clone()).normalize(),
box IMax(box v.clone(), box w.clone()).normalize(),
),
IMax(box u, box Max(box v, box w)) => Max(
box IMax(box u.clone(), box v.clone()).normalize(),
box IMax(box u.clone(), box w.clone()).normalize(),
),
_ => self.clone(),
}
}
// checks whether u1 <= u2 + n
// returns:
// - (true,0) if u1 <= u2 + n,
// - (false,0) if !(u1 <= u2 + n),
// - (false,i+1) if Var(i) needs to be substituted to unstuck the comparison.
fn geq_no_subst(&self, u2: &UniverseLevel, n: i64) -> (bool, usize) {
match (self.normalize(), u2.normalize()) {
(Zero, _) if n >= 0 => (true, 0),
(_, _) if *self == *u2 && n >= 0 => (true, 0),
(Succ(l), _) if l.geq_no_subst(u2, n - 1).0 => (true, 0),
(_, Succ(box l)) if self.geq_no_subst(&l, n + 1).0 => (true, 0),
(_, Max(box l1, box l2))
if self.geq_no_subst(&l1, n).0 || self.geq_no_subst(&l2, n).0 =>
{
(true, 0)
}
(Max(box l1, box l2), _) if l1.geq_no_subst(u2, n).0 && l2.geq_no_subst(u2, n).0 => {
(true, 0)
}
(_, IMax(_, box Var(i))) | (IMax(_, box Var(i)), _) => (false, i + 1),
_ => (false, 0),
}
}
/// Checks whether u1 <= u2 + n
// In a case where comparison is stuck because of a variable Var(i), it checks whether the test is correct when Var(i) is substituted for
// 0 and S(Var(i)).
fn geq(&self, u2: &UniverseLevel, n: i64) -> bool {
match self.geq_no_subst(u2, n) {
(true, _) => true,
(false, 0) => false,
(false, i) => {
self.clone()
.substitute_single(i - 1, Zero)
.geq(&u2.clone().substitute_single(i - 1, Zero), n)
&& self
.clone()
.substitute_single(i - 1, Succ(box Var(i - 1)))
.geq(
&u2.clone().substitute_single(i - 1, Succ(box Var(i - 1))),
n,
)
}
}
}
pub fn is_eq(&self, u2: &UniverseLevel) -> bool {
self.geq(u2, 0) && u2.geq(self, 0)
}
}
#[cfg(test)]
mod tests {
use crate::universe::UniverseLevel::*;
mod pretty_printing {
use crate::universe::UniverseLevel::*;
#[test]
fn to_num() {
assert_eq!(Max(box Succ(box Zero), box Zero).to_numeral(), Some(1));
assert_eq!(
Max(box Succ(box Zero), box Succ(box Var(0))).to_numeral(),
None
);
assert_eq!(IMax(box Var(0), box Zero).to_numeral(), Some(0));
assert_eq!(IMax(box Zero, box Succ(box Zero)).to_numeral(), Some(1))
}
#[test]
fn to_plus() {
assert_eq!(Succ(box Zero).plus(), (Zero, 1));
}
#[test]
fn to_pretty_print() {
assert_eq!(
Max(
box Succ(box Zero),
box IMax(box Max(box Zero, box Var(0)), box Succ(box Var(0)))
)
.pretty_print(),
"max (1) (imax (max (0) (u0)) (u0 + 1))"
);
}
}
#[test]
fn univ_eq() {
assert!(&Zero.is_eq(&Default::default()));
assert!(!&Zero.is_eq(&Succ(box Zero)));
assert!(!&Succ(box Zero).is_eq(&Zero));
assert!(&Var(0).is_eq(&Max(box Zero, box Var(0))));
assert!(&Max(box Zero, box Var(0)).is_eq(&Var(0)));
assert!(&Max(box Var(1), box Var(0)).is_eq(&Max(box Var(0), box Var(1))));
assert!(!&Max(box Var(1), box Var(1)).is_eq(&Max(box Var(0), box Var(1))));
assert!(&Succ(box Max(box Var(1), box Var(0)))
.is_eq(&Max(box Succ(box Var(0)), box Succ(box Var(1)))));
assert!(&Max(
box Zero,
box IMax(box Zero, box Max(box Succ(box Zero), box Zero))
)
.is_eq(&IMax(
box Succ(box Zero),
box IMax(box Succ(box Zero), box Succ(box Zero))
)));
assert!(&Var(0).is_eq(&IMax(box Var(0), box Var(0))));
assert!(&IMax(box Succ(box Zero), box Max(box Zero, box Zero)).is_eq(&Zero));
assert!(!&IMax(box Var(0), box Var(1)).is_eq(&IMax(box Var(1), box Var(0))))
}
#[test]
fn univ_vars_count() {
assert_eq!(
IMax(
box Zero,
box Max(box Succ(box Zero), box Max(box Var(0), box Var(1)))
)
.univ_vars(),
2
)
}
#[test]
fn subst() {
let lvl = IMax(
box Zero,
box Max(box Succ(box Zero), box Max(box Var(0), box Var(1))),
);
let subst = vec![Succ(box Zero), Zero];
assert_eq!(
lvl.substitute(&subst),
IMax(
box Zero,
box Max(box Succ(box Zero), box Max(box Succ(box Zero), box Zero))
)
)
}
#[test]
fn single_subst() {
let lvl = IMax(box Max(box Succ(box Zero), box Var(0)), box Var(0));
assert_eq!(
lvl.substitute_single(0, Zero),
IMax(box Max(box Succ(box Zero), box Zero), box Zero)
)
}
}
kernel/tests/and.rs
View file @ ab3d2a84
#![feature(box_syntax)]
use kernel::builders::*;
use kernel::Command::*;
use kernel::Environment;
use kernel::Term::{self, *};
use lazy_static::lazy_static;
lazy_static! {
static ref FALSE: Term = Prod(box Prop, box Var(1.into()));
static ref TRUE: Term = Prod(box Const("False".into()), box Const("False".into()));
}
fn setup_env() -> Environment {
let mut env = Environment::new();
assert!(Define("False".into(), None, FALSE.clone())
.process(&mut env)
.unwrap()
.is_none());
assert!(Define("True".into(), None, TRUE.clone())
.process(&mut env)
.unwrap()
.is_none());
let and = Abs(
box Prop,
box Abs(
box Prop,
box Prod(
box Prop,
box Prod(
// A -> B -> C
box Prod(
box Var(3.into()),
box Prod(box Var(3.into()), box Var(3.into())),
use kernel::{use_arena, Arena};
fn use_and_arena<F, T>(f: F) -> T
where
F: for<'arena> FnOnce(&mut Arena<'arena>) -> T,
{
use_arena(|arena| {
let false_ = arena
.build_from_extern(prod("P", prop(), var("P")))
.unwrap();
assert!(Define("False", None, false_)
.process(arena)
.unwrap()
.is_none());
let true_ = arena
.build_from_extern(prod("_", var("False"), var("False")))
.unwrap();
assert!(Define("True", None, true_)
.process(arena)
.unwrap()
.is_none());
let and = arena
.build_from_extern(abs(
"A",
prop(),
abs(
"B",
prop(),
prod(
"C",
prop(),
prod(
"_",
prod("_", var("A"), prod("_", var("B"), var("C"))),
var("C"),
),
),
box Var(2.into()),
),
),
),
);
))
.unwrap();
assert!(Define("and", None, and).process(arena).unwrap().is_none());
assert!(Define("and".into(), None, and)
.process(&mut env)
.unwrap()
.is_none());
env
f(arena)
})
}
#[test]
fn and_true_true() {
let mut env = setup_env();
let goal = App(
box App(box Const("and".into()), box Const("True".into())),
box Const("True".into()),
);
let hypothesis = Abs(box Const("False".into()).clone(), box Var(1.into()));
assert!(Define("hyp".into(), Some(TRUE.clone()), hypothesis)
.process(&mut env)
.is_ok());
let proof = Abs(
box Prop,
box Abs(
box Prod(
box Const("True".into()),
box Prod(box Const("True".into()), box Var(3.into())),
),
box App(
box App(box Var(1.into()), box Const("hyp".into())),
box Const("hyp".into()),
),
),
);
assert!(CheckType(proof, goal).process(&mut env).is_ok());
use_and_arena(|arena| {
let goal = arena
.build_from_extern(app(app(var("and"), var("True")), var("True")))
.unwrap();
let hypothesis = arena
.build_from_extern(abs("x", var("False"), var("x")))
.unwrap();
let true_ = arena.build_from_extern(var("True")).unwrap();
assert!(Define("hyp", Some(true_), hypothesis)
.process(arena)
.is_ok());
let proof = arena
.build_from_extern(abs(
"a",
prop(),
abs(
"b",
prod("_", var("True"), prod("_", var("True"), var("a"))),
app(app(var("b"), var("hyp")), var("hyp")),
),
))
.unwrap();
assert!(CheckType(proof, goal).process(arena).is_ok());
})
}
#[test]
fn and_intro() {
let mut env = setup_env();
let goal = Prod(
// A : Prop
box Prop,
box Prod(
// B : Prop
box Prop,
box Prod(
// a : A
box Var(2.into()),
box Prod(
// b : B
box Var(2.into()),
box App(
box App(box Const("and".into()), box Var(4.into())),
box Var(3.into()),
use_and_arena(|arena| {
let goal = arena
.build_from_extern(prod(
"A", // A : prop()
prop(),
prod(
"B", // B : prop()
prop(),
prod(
"_",
var("A"),
prod("_", var("B"), app(app(var("and"), var("A")), var("B"))),
),
),
),
),
);
let proof = Abs(
// A : Prop
box Prop,
box Abs(
// B : Prop
box Prop,
box Abs(
// a : A
box Var(2.into()),
box Abs(
// b : B
box Var(2.into()),
box Abs(
// C : Prop
box Prop,
box Abs(
// p : A -> B -> C
box Prod(
box Var(5.into()),
box Prod(box Var(5.into()), box Var(3.into())),
),
// p a b
box App(
box App(box Var(1.into()), box Var(4.into())),
box Var(3.into()),
))
.unwrap();
let proof = arena
.build_from_extern(abs(
"A",
// A : prop()
prop(),
abs(
"B",
// B : prop()
prop(),
abs(
"a",
// a : A
var("A"),
abs(
"b",
// b : B
var("B"),
abs(
"C",
// C : prop()
prop(),
abs(
"p",
// p : A -> B -> C
prod("_", var("A"), prod("_", var("B"), var("C"))),
// p a b
app(app(var("p"), var("a")), var("b")),
),
),
),
),
),
),
),
);
))
.unwrap();
assert!(CheckType(proof, goal).process(&mut env).is_ok());
assert!(CheckType(proof, goal).process(arena).is_ok());
})
}
#[test]
fn and_elim_1() {
let mut env = setup_env();
let goal = Prod(
// A : Prop
box Prop,
box Prod(
// B : Prop
box Prop,
box Prod(
box App(
box App(box Const("and".into()), box Var(2.into())),
box Var(1.into()),
),
box Var(3.into()),
),
),
);
let proof = Abs(
// A : Prop
box Prop,
box Abs(
// B : Prop
box Prop,
box Abs(
// p : and A B
box App(
box App(box Const("and".into()), box Var(2.into())),
box Var(1.into()),
use_and_arena(|arena| {
let goal = arena
.build_from_extern(prod(
"A",
// A : prop()
prop(),
prod(
"B",
// B : prop()
prop(),
prod("_", app(app(var("and"), var("A")), var("B")), var("A")),
),
box App(
box App(box Var(1.into()), box Var(3.into())),
box Abs(
// a : A
box Var(3.into()),
box Abs(
// b : B
box Var(3.into()),
box Var(2.into()),
))
.unwrap();
let proof = arena
.build_from_extern(abs(
"A",
// A : prop()
prop(),
abs(
"B",
// B : prop()
prop(),
abs(
"p",
// p : and A B
app(app(var("and"), var("A")), var("B")),
app(
app(var("p"), var("A")),
abs(
"a",
// a : A
var("A"),
abs(
"b",
// b : B
var("B"),
var("a"),
),
),
),
),
),
),
),
);
))
.unwrap();
assert!(CheckType(proof, goal).process(&mut env).is_ok());
assert!(CheckType(proof, goal).process(arena).is_ok());
})
}
#[test]
fn and_elim_2() {
let mut env = setup_env();
let goal = Prod(
// A : Prop
box Prop,
box Prod(
// B : Prop
box Prop,
box Prod(
// p : and A B
box App(
box App(box Const("and".into()), box Var(2.into())),
box Var(1.into()),
),
box Var(2.into()),
),
),
);
let proof = Abs(
// A : Prop
box Prop,
box Abs(
// B : Prop
box Prop,
box Abs(
// p : and A B
box App(
box App(box Const("and".into()), box Var(2.into())),
box Var(1.into()),
use_and_arena(|arena| {
let goal = arena
.build_from_extern(prod(
"A",
// A : prop()
prop(),
prod(
"B",
// B : prop()
prop(),
prod(
"p",
// p : and A B
app(app(var("and"), var("A")), var("B")),
var("B"),
),
),
box App(
box App(box Var(1.into()), box Var(2.into())),
box Abs(
// a : A
box Var(3.into()),
box Abs(
// b : B
box Var(3.into()),
box Var(1.into()),
))
.unwrap();
let proof = arena
.build_from_extern(abs(
"A",
// A : prop()
prop(),
abs(
"B",
// B : prop()
prop(),
abs(
"p",
// p : and A B
app(app(var("and"), var("A")), var("B")),
app(
app(var("p"), var("B")),
abs(
"a",
// a : A
var("A"),
abs(
"b",
// b : B
var("B"),
var("b"),
),
),
),
),
),
),
),
);
))
.unwrap();
assert!(CheckType(proof, goal).process(&mut env).is_ok());
assert!(CheckType(proof, goal).process(arena).is_ok());
})
}