From c32fbef3cd3050e36b3176fc7a3c4128c9fcd6ef Mon Sep 17 00:00:00 2001
From: Lucas Tabary-Maujean <l.ta-ma@proton.me>
Date: Sat, 5 Nov 2022 15:01:32 +0100
Subject: [PATCH] fix(terms and type checker): use deref trait, further
temporary changes in type checker, removing previous environment definition;
early: won't compile
---
Cargo.lock | 22 +++---
Cargo.toml | 6 +-
kernel/Cargo.toml | 4 +-
kernel/src/environment.rs | 48 ------------
kernel/src/term.rs | 152 ++++++++++++++++++++++++++++---------
kernel/src/type_checker.rs | 78 +++----------------
6 files changed, 144 insertions(+), 166 deletions(-)
delete mode 100644 kernel/src/environment.rs
diff --git a/Cargo.lock b/Cargo.lock
index e79ad515..fe2c0da3 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -69,9 +69,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
[[package]]
name = "clap"
-version = "4.0.18"
+version = "4.0.19"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "335867764ed2de42325fafe6d18b8af74ba97ee0c590fa016f157535b42ab04b"
+checksum = "8e67816e006b17427c9b4386915109b494fec2d929c63e3bd3561234cbf1bf1e"
dependencies = [
"atty",
"bitflags",
@@ -305,8 +305,8 @@ version = "0.1.0"
dependencies = [
"bumpalo",
"derive_more",
- "lazy_static",
"im-rc",
+ "lazy_static",
"num-bigint",
]
@@ -418,9 +418,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",
@@ -428,9 +428,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",
@@ -438,9 +438,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",
@@ -451,9 +451,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",
diff --git a/Cargo.toml b/Cargo.toml
index de3a1a7c..e8ad1806 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -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"
diff --git a/kernel/Cargo.toml b/kernel/Cargo.toml
index 4ca21cd8..ce4e0d22 100644
--- a/kernel/Cargo.toml
+++ b/kernel/Cargo.toml
@@ -11,5 +11,5 @@ num-bigint.workspace = true
[dev-dependencies]
lazy_static = "1.4.0"
-bumpalo.workspace = true;
-im-rc.workspace = true;
+bumpalo.workspace = true
+im-rc.workspace = true
diff --git a/kernel/src/environment.rs b/kernel/src/environment.rs
deleted file mode 100644
index 5d9ada90..00000000
--- a/kernel/src/environment.rs
+++ /dev/null
@@ -1,48 +0,0 @@
-use crate::error::{Error, Result};
-use crate::term::Term;
-use derive_more::{Deref, DerefMut, Display};
-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),
-}
-
-impl Environment {
- /// Creates an empty environment.
- pub fn new() -> Self {
- 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));
- Ok(self)
- } else {
- Err(Error {
- kind: EnvironmentError::AlreadyDefined(s).into(),
- })
- }
- }
-
- /// 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())
- }
-
- /// 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())
- }
-}
diff --git a/kernel/src/term.rs b/kernel/src/term.rs
index 65024ff7..9cb2344e 100644
--- a/kernel/src/term.rs
+++ b/kernel/src/term.rs
@@ -8,6 +8,8 @@ use im_rc::hashmap::HashMap as ImHashMap;
use std::cell::OnceCell;
use std::collections::{HashMap, HashSet};
use std::hash::Hash;
+use std::marker::PhantomData;
+use std::ops::Deref;
#[derive(
Add, Copy, Clone, Debug, Default, Display, Eq, PartialEq, From, Into, Sub, PartialOrd, Ord, Hash,
@@ -19,6 +21,7 @@ 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>>,
@@ -26,16 +29,10 @@ pub struct Arena<'arena> {
mem_subst: HashMap<(Term<'arena>, Term<'arena>, DeBruijnIndex), Term<'arena>>,
}
-type Environment<'arena> = ImHashMap<&'arena str, (DeBruijnIndex, Term<'arena>)>;
-pub trait ExternTermGenerator<'arena> = FnOnce(
- &mut Arena<'arena>,
- &Environment<'arena>,
- DeBruijnIndex,
-) -> Result<Term<'arena>, KernelError<'arena>>;
-
#[derive(Clone, Copy, Display, Eq, Debug)]
#[display(fmt = "{}", "_0.payload")]
-pub struct Term<'arena>(&'arena Node<'arena>);
+// PhantomData is a marker to ensure invariance over the 'arena lifetime.
+pub struct Term<'arena>(&'arena Node<'arena>, PhantomData<*mut &'arena ()>);
// no name storage here: meaning consts are known and can be found, but no pretty printing is
// possible so far.
@@ -55,7 +52,7 @@ type BinTermHashMap<'arena> = HashMap<(Term<'arena>, Term<'arena>), Term<'arena>
//
// We also need a substitution hasmap, (body, level_of_substitution, Term_to_incorporate)
-#[derive(Clone, Copy, Debug, Display, Eq, PartialEq, Hash)]
+#[derive(Clone, Debug, Display, Eq, PartialEq, Hash)]
pub enum Payload<'arena> {
#[display(fmt = "{}", _0)]
Var(DeBruijnIndex, Term<'arena>),
@@ -64,7 +61,7 @@ pub enum Payload<'arena> {
Prop,
#[display(fmt = "Type {}", _0)]
- Type(&'arena UniverseLevel),
+ Type(UniverseLevel),
#[display(fmt = "{} {}", _0, _1)]
App(Term<'arena>, Term<'arena>),
@@ -100,12 +97,6 @@ impl<'arena> Hash for Node<'arena> {
}
}
-impl<'arena> From<Term<'arena>> for Payload<'arena> {
- fn from(t: Term<'arena>) -> Self {
- t.0.payload
- }
-}
-
pub fn use_arena<F, T>(f: F) -> T
where
F: for<'arena> FnOnce(Arena<'arena>) -> T,
@@ -115,16 +106,21 @@ where
f(arena)
}
+use intern_build::Generator;
+use extern_build::Generator as ExternGenerator;
+
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(),
+
}
}
@@ -138,11 +134,11 @@ impl<'arena> Arena<'arena> {
type_: OnceCell::new(),
};
match self.hashcons.get(&nn) {
- Some(addr) => Term(addr),
+ Some(addr) => Term(addr, PhantomData),
None => {
let addr = self.alloc.alloc(nn);
self.hashcons.insert(addr);
- Term(addr)
+ Term(addr, PhantomData)
}
}
}
@@ -155,7 +151,7 @@ impl<'arena> Arena<'arena> {
self.hashcons(Prop)
}
- pub(crate) fn type_(&mut self, level: &'arena UniverseLevel) -> Term<'arena> {
+ pub(crate) fn type_(&mut self, level: UniverseLevel) -> Term<'arena> {
self.hashcons(Type(level))
}
@@ -171,7 +167,11 @@ impl<'arena> Arena<'arena> {
self.hashcons(Prod(arg_type, u))
}
- pub(crate) fn extern_gen<F: ExternTermGenerator<'arena>>(
+ pub(crate) fn build<F: Generator<'arena>>(&mut self, f: F) -> Term<'arena> {
+ f(self)
+ }
+
+ pub fn build_from_extern<F: ExternGenerator<'arena>>(
&mut self,
f: F,
) -> Result<Term<'arena>, KernelError<'arena>> {
@@ -180,8 +180,8 @@ 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.into() {
- App(t1, t2) => match t1.into() {
+ match *t {
+ App(t1, t2) => match *t1 {
Abs(_, t1) => self.substitute(t1, t2, 1),
_ => {
let t1 = self.beta_reduction(t1);
@@ -197,7 +197,7 @@ impl<'arena> Arena<'arena> {
}
pub(crate) fn shift(&mut self, t: Term<'arena>, offset: usize, depth: usize) -> Term<'arena> {
- match t.into() {
+ 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);
@@ -224,7 +224,7 @@ impl<'arena> Arena<'arena> {
rhs: Term<'arena>,
depth: usize,
) -> Term<'arena> {
- match lhs.into() {
+ match *lhs {
Var(i, _) if i == depth.into() => self.shift(rhs, depth - 1, 0),
Var(i, type_) if i > depth.into() => self.var(i - 1.into(), type_),
App(l, r) => {
@@ -262,10 +262,10 @@ impl<'arena> Arena<'arena> {
/// Returns the weak-head normal form of a term in a given environment.
pub fn whnf(&mut self, t: Term<'arena>) -> Term<'arena> {
- match t.into() {
+ match *t {
App(t1, t2) => {
let t1 = self.whnf(t1);
- match t1.into() {
+ match *t1 {
Abs(_, _) => {
let t = self.app(t1, t2);
let t = self.beta_reduction(t);
@@ -279,15 +279,93 @@ impl<'arena> Arena<'arena> {
}
}
+impl<'arena> Term<'arena> {
+ pub(crate) fn into(self) -> impl Generator<'arena>
+ { move |_: &mut Arena<'arena>| self }
+
+ pub fn is_redex(self) -> bool {
+ match *self {
+ App(t, _) => match *t {
+ Abs(_, _) => true,
+ _ => false
+ }
+ _ => false
+ }
+ }
+}
+
+impl<'arena> Deref for Term<'arena> {
+ type Target = Payload<'arena>;
+
+ fn deref(&self) -> &Self::Target {
+ &self.0.payload
+ }
+}
+
+pub(crate) mod intern_build {
+ use super::*;
+
+ pub(crate) trait Generator<'arena> = FnOnce(&mut Arena<'arena>) -> Term<'arena>;
+
+ pub fn prop<'arena>() -> impl Generator<'arena> {
+ |env: &mut Arena<'arena>| env.prop()
+ }
+
+ pub fn type_<'arena>(level: UniverseLevel) -> impl Generator<'arena> {
+ move |env: &mut Arena<'arena>| env.type_(level)
+ }
+
+ pub fn app<'arena, F1: Generator<'arena>, F2: Generator<'arena>>(
+ u1: F1,
+ u2: F2,
+ ) -> impl Generator<'arena> {
+ |env: &mut Arena<'arena>| {
+ let u1 = u1(env);
+ let u2 = u2(env);
+ env.app(u1, u2)
+ }
+ }
+
+ pub fn abs<'arena, F1: Generator<'arena>, F2: Generator<'arena>>(
+ u1: F1,
+ u2: F2,
+ ) -> impl Generator<'arena> {
+ |env: &mut Arena<'arena>| {
+ let u1 = u1(env);
+ let u2 = u2(env);
+ env.abs(u1, u2)
+ }
+ }
+
+ pub fn prod<'arena, F1: Generator<'arena>, F2: Generator<'arena>>(
+ u1: F1,
+ u2: F2,
+ ) -> impl Generator<'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 from_parser {
- use crate::term::*;
+pub mod extern_build {
+ use super::*;
+
+ pub type Environment<'arena> = ImHashMap<&'arena str, (DeBruijnIndex, Term<'arena>)>;
+pub trait Generator<'arena> = FnOnce(
+ &mut Arena<'arena>,
+ &Environment<'arena>,
+ DeBruijnIndex,
+) -> Result<Term<'arena>, KernelError<'arena>>;
+
- pub fn var<'arena>(name: &'arena str) -> impl ExternTermGenerator<'arena> {
+ pub fn var<'arena>(name: &'arena str) -> impl Generator<'arena> {
move |context: &mut Arena<'arena>, env: &Environment<'arena>, depth| {
env.get(name)
.map(|(bind_depth, term)| context.var(depth - *bind_depth, *term))
@@ -296,18 +374,18 @@ pub mod from_parser {
}
}
- pub fn prop<'arena>() -> impl ExternTermGenerator<'arena> {
+ pub fn prop<'arena>() -> impl Generator<'arena> {
|context: &mut Arena<'arena>, _: &Environment<'arena>, _| Ok(context.prop())
}
- pub fn type_<'arena>(level: &'arena UniverseLevel) -> impl ExternTermGenerator<'arena> {
+ pub fn type_<'arena>(level: UniverseLevel) -> impl Generator<'arena> {
move |context: &mut Arena<'arena>, _: &Environment<'arena>, _| Ok(context.type_(level))
}
- pub fn app<'arena, F1: ExternTermGenerator<'arena>, F2: ExternTermGenerator<'arena>>(
+ pub fn app<'arena, F1: Generator<'arena>, F2: Generator<'arena>>(
u1: F1,
u2: F2,
- ) -> impl ExternTermGenerator<'arena> {
+ ) -> impl Generator<'arena> {
|context: &mut Arena<'arena>, env: &Environment<'arena>, depth| {
let u1 = u1(context, env, depth)?;
let u2 = u2(context, env, depth)?;
@@ -315,11 +393,11 @@ pub mod from_parser {
}
}
- pub fn abs<'arena, F1: ExternTermGenerator<'arena>, F2: ExternTermGenerator<'arena>>(
+ pub fn abs<'arena, F1: Generator<'arena>, F2: Generator<'arena>>(
name: &'arena str,
arg_type: F1,
body: F2,
- ) -> impl ExternTermGenerator<'arena> {
+ ) -> impl Generator<'arena> {
move |context: &mut Arena<'arena>, env: &Environment<'arena>, depth| {
let arg_type = arg_type(context, env, depth)?;
let env = env.update(name, (depth + DeBruijnIndex(1), arg_type));
@@ -328,11 +406,11 @@ pub mod from_parser {
}
}
- pub fn prod<'arena, F1: ExternTermGenerator<'arena>, F2: ExternTermGenerator<'arena>>(
+ pub fn prod<'arena, F1: Generator<'arena>, F2: Generator<'arena>>(
name: &'arena str,
arg_type: F1,
body: F2,
- ) -> impl ExternTermGenerator<'arena> {
+ ) -> impl Generator<'arena> {
move |context: &mut Arena<'arena>, env: &Environment<'arena>, depth| {
let arg_type = arg_type(context, env, depth)?;
let env = env.update(name, (depth + DeBruijnIndex(1), arg_type));
diff --git a/kernel/src/type_checker.rs b/kernel/src/type_checker.rs
index beefbc09..684d92db 100644
--- a/kernel/src/type_checker.rs
+++ b/kernel/src/type_checker.rs
@@ -1,11 +1,10 @@
use crate::environment::{Environment, EnvironmentError};
use crate::error::{Error, Result};
-use crate::term::{DeBruijnIndex, Term};
+use crate::term::{Arena, Payload, Term};
use derive_more::Display;
use num_bigint::BigUint;
use std::cmp::max;
-use std::ops::Index;
-use Term::*;
+use Payload::*;
#[derive(Clone, Debug, Display, Eq, PartialEq)]
#[display(fmt = "{} : {}", _0, _1)]
@@ -36,72 +35,19 @@ pub enum TypeCheckerError {
TypeMismatch(Term, Term),
}
-/// Type of lists of tuples representing the respective types of each variables
-type Types = Vec<Term>;
-
-impl Index<DeBruijnIndex> for Types {
- type Output = Term;
-
- fn index(&self, idx: DeBruijnIndex) -> &Self::Output {
- &self[usize::from(idx)]
- }
-}
-
-/// Structure containing a context used for typechecking.
-///
-/// It serves to store the types of variables in the following way:
-/// In a given context {types, lvl}, the type of `Var(i)` is in `types[lvl - i]`.
-#[derive(Clone, Debug, Default)]
-struct Context {
- types: Types,
- lvl: DeBruijnIndex,
-}
-
-impl Context {
- /// Creates a new empty `Context`.
- fn new() -> Self {
- Self::default()
- }
-
- /// Extends the actual context with a bound variable of type `ty`.
- fn bind(&mut self, ty: &Term) -> &mut Self {
- // if x : Var(i), and x appears in a redex, then i needs to be shifted in the context, it would lead to incoherences otherwise.
- self.types = self.types.iter().map(|t| t.shift(1, 0)).collect();
- self.types.push(ty.shift(1, 0));
- self.lvl = self.lvl + 1.into();
- self
- }
-}
-
-impl Term {
+impl<'arena> Arena<'arena> {
/// Conversion function, checks whether two terms are definitionally equal.
///
/// The conversion is untyped, meaning that it should **only** be called during type-checking when the two `Term`s are already known to be of the same type and in the same context.
- fn conversion(&self, rhs: &Term, env: &Environment) -> bool {
- match (self.whnf(env), rhs.whnf(env)) {
- (Prop, Prop) => true,
-
- (Type(i), Type(j)) => i == j,
-
- (Var(i), Var(j)) => i == j,
-
- (Prod(t1, u1), Prod(box t2, u2)) => t1.conversion(&t2, env) && u1.conversion(&u2, env),
-
- // Since we assume that both vals already have the same type,
- // checking conversion over the argument type is useless.
- // However, this doesn't mean we can simply remove the arg type
- // from the type constructor in the enum, it is needed to quote back to terms.
- (Abs(_, t), Abs(_, u)) => t.conversion(&u, env),
-
- (App(box t1, box u1), App(box t2, box u2)) => {
- t1.conversion(&t2, env) && u1.conversion(&u2, env)
- }
- // TODO: Unused code (#34)
- // (app @ App(box Abs(_, _), box _), u) | (u, app @ App(box Abs(_, _), box _)) => {
- // app.beta_reduction(env).conversion(&u, env)
- // }
- _ => false,
- }
+ fn conversion(&mut self, lhs: Term<'arena>, rhs: Term<'arena>) -> bool {
+ let lhs = self.whnf(lhs);
+ let rhs = self.whnf(rhs);
+ lhs == rhs
+
+ // TODO: Unused code (#34)
+ // (app @ App(box Abs(_, _), box _), u) | (u, app @ App(box Abs(_, _), box _)) => {
+ // app.beta_reduction(env).conversion(&u, env)
+ // }
}
/// Checks whether two terms are definitionally equal.
--
GitLab