From 30144fc85f73a7df205e5d674d307332b247d370 Mon Sep 17 00:00:00 2001
From: belazy <aarthuur01@gmail.com>
Date: Sat, 24 Dec 2022 15:24:21 +0100
Subject: [PATCH] =?UTF-8?q?Resolve=20"Add=20Universe=20Polymorphism"=20?=
=?UTF-8?q?=E2=9C=A8=EF=B8=8F=20Closes=20#28=20=F0=9F=90=94=EF=B8=8F?=
=?UTF-8?q?=F0=9F=91=8D=EF=B8=8F=20Approved-by:=20belazy=20<aarthuur01@gma?=
=?UTF-8?q?il.com>=20Approved-by:=20aalbert=20<augustin.albert@bleu-azure.?=
=?UTF-8?q?fr>=20Approved-by:=20v-lafeychine=20<vincent.lafeychine@proton.?=
=?UTF-8?q?me>=20Approved-by:=20loutr=20<loutr@crans.org>?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
🦀ï¸ðŸ°ðŸ¦€ï¸ðŸ°ðŸ¦€ï¸ðŸ°
* fix(proost): added Define command back (need to distinguish between the two in order to bind and reuse correctly later
* chore(kernel, calculus/level): adapt documentation to new type
* chore(level): Add specific enum to handle comparison state
* chore(kernel): c-o-v-e-r-a-g-e
* chore(parser): remove TODO
* chore(parser): more coverage
* fix(kernel): trailing comma when printing `InstantiatedDeclaration`s
* fix(kernel): chiale + aboie, coverage
* chore(kernel): mention #14
* chore(kernel): yet another test
* chore(kernel): always more coverage
* chore(parser): add issue nb to todo
* fix(kernel): avoid reentrant entry bug when infering type of decls with 0 universe arguments
* fix(parser): revert comit, wtf clippy ?
* chore(parser): remove unused branch
* chore(kernel): another test
* Apply 1 suggestion(s) to 1 file(s)
* fix(kernel): remove dangerous function
* chore(kernel): always more coverage
* feat(parser): remove `Define` command
* fix(kernel): interface checking for decls
* Apply 1 suggestion(s) to 1 file(s)
* chore(kernel): add coverage
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* chore(kernel): coverage
* Apply 1 suggestion(s) to 1 file(s)
* fix(kernel): over-agressive normalization
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* fix(parser): avoid spacing befor univ decls/vars
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* fix(proost): check existing identifiers for al definitions
* Apply 1 suggestion(s) to 1 file(s)
* feat(parser): add `DeclarationCheckType`
* chore(kernel): remove unused test
* fix(proost): type-check terms before `Eval`uating
* docs: update
* fix: further adjustments to parser
* chore: formatting + some adjustments for kernel tests
* fix(parser, proost): modify command generation for declarations
* chore(parser): add tests todo
* chore(parser): tests on sort parsing
* fix(parser): tests
* feat(parser): parse universe bindings
* feat(parser): parse universe declarations in define_type
* fix(level): comments
* chore: remove biging as a dependency
* chore(kernel): remove todo
* chore(kernel): remove unused file
* chore(kernel): more tests
* chore(kernel): documentation of `level_builder.rs`
* feat(kernel): tests coverage
* fix(kernel): tests
* feat(kernel/term/builder): add binding to (instantiated) declaration builders
* feat(kernel): add builders for declaration
* chore(kernel): refactor builder file hierarchy and simplify these files
* fix(proost): some import errors
* feat(parser): add parsing for univ parameters of definitions
* chore(kernel): add todo
* fix: remove lifetime dependency on LevelEnvironment
* feat : add inference for declarations.
* feat(parser): add new parsing rules for levels
* feat(parser): new syntax for universe polymorphism
* feat(kernel): add type-checking for Decls
* feat: incorporate LevelBuilder in TermBuilder
* fix(kernel): refactor impl organisation: unload most of arena's
* WOOOHOOOO
* fix(kernel, level): fix incorrect assignment in hashcons function
* fix(kernel): more errors
* feat(kernel): fixed some errors
* feat(kernel): finish rudimentary bases for modifying parser and type checker
* feat(kernel): further work on Levels
* WIP feat(kernel): modify declaration.rs structure
* fix(kernel): removing Dweller struct, using a macro instead
* fix(kernel): refactor file structure to add new core types. first attempt for levels.
* feat(kernel): add generic Dweller type
* WIP fix(kernel): refactor file structure to add new core types
* um
* feat:something
* AH
* first commit
---
kernel/src/calculus/level.rs | 68 ++++++++++++++++++++--------
kernel/src/calculus/term.rs | 1 -
kernel/src/memory/declaration/mod.rs | 7 ++-
parser/src/parser.rs | 35 +++++++++++++-
parser/src/term.pest | 4 +-
proost/src/evaluator.rs | 4 +-
6 files changed, 92 insertions(+), 27 deletions(-)
diff --git a/kernel/src/calculus/level.rs b/kernel/src/calculus/level.rs
index 47e7acce..561664d8 100644
--- a/kernel/src/calculus/level.rs
+++ b/kernel/src/calculus/level.rs
@@ -5,6 +5,25 @@ use Payload::*;
use crate::memory::arena::Arena;
use crate::memory::level::{Level, Payload};
+/// State during computation for level comparison.
+enum State {
+ /// Comparison failed.
+ False,
+
+ /// Comparison succeed.
+ True,
+
+ /// Induction is needed to complete the comparaison.
+ Stuck(usize),
+}
+
+impl State {
+ /// Checks if the comparison succeeded.
+ fn is_true(&self) -> bool {
+ matches!(self, State::True)
+ }
+}
+
impl<'arena> Level<'arena> {
/// Helper function for equality checking, used to substitute `Var(i)` with `Z` and `S(Var(i))`.
fn substitute_single(self, var: usize, u: Self, arena: &mut Arena<'arena>) -> Self {
@@ -34,25 +53,30 @@ impl<'arena> Level<'arena> {
/// Checks whether `self <= rhs + n`, without applying substitution.
///
/// Precisely, it returns:
- /// - `(false, i + 1)` if `Var(i)` needs to be substituted to unstuck the comparison.
- /// - `(true, 0)` if `self <= rhs + n`,
- /// - `(false, 0)` else.
- fn geq_no_subst(self, rhs: Self, n: i64) -> (bool, usize) {
+ /// - `Stuck(i + 1)` if `Var(i)` needs to be substituted to unstuck the comparison.
+ /// - `True` if `self <= rhs + n`,
+ /// - `False` else.
+ fn geq_no_subst(self, rhs: Self, n: i64) -> State {
match (&*self, &*rhs) {
- (Zero, _) if n >= 0 => (true, 0),
- (_, _) if self == rhs && n >= 0 => (true, 0),
- (Succ(l), _) if l.geq_no_subst(rhs, n - 1).0 => (true, 0),
- (_, Succ(l)) if self.geq_no_subst(*l, n + 1).0 => (true, 0),
+ (Zero, _) if n >= 0 => State::True,
+
+ (_, _) if self == rhs && n >= 0 => State::True,
+
+ (Succ(l), _) if l.geq_no_subst(rhs, n - 1).is_true() => State::True,
+ (_, Succ(l)) if self.geq_no_subst(*l, n + 1).is_true() => State::True,
+
(_, Max(l1, l2))
- if self.geq_no_subst(*l1, n).0 || self.geq_no_subst(*l2, n).0 =>
+ if self.geq_no_subst(*l1, n).is_true() || self.geq_no_subst(*l2, n).is_true() =>
{
- (true, 0)
+ State::True
}
- (Max(l1, l2), _) if l1.geq_no_subst(rhs, n).0 && l2.geq_no_subst(rhs, n).0 => {
- (true, 0)
+ (Max(l1, l2), _) if l1.geq_no_subst(rhs, n).is_true() && l2.geq_no_subst(rhs, n).is_true() => {
+ State::True
}
- (_, IMax(_, v)) | (IMax(_, v), _) if let Var(i) = **v => (false, i + 1),
- _ => (false, 0),
+
+ (_, IMax(_, v)) | (IMax(_, v), _) if let Var(i) = **v => State::Stuck(i),
+
+ _ => State::False,
}
}
@@ -62,13 +86,13 @@ impl<'arena> Level<'arena> {
/// is substituted for `0` and `S(Var(i))`.
pub fn geq(self, rhs: Self, n: i64, arena: &mut Arena<'arena>) -> bool {
match self.geq_no_subst(rhs, n) {
- (true, _) => true,
- (false, 0) => false,
- (false, i) => {
+ State::True => true,
+ State::False => false,
+ State::Stuck(i) => {
let zero = Level::zero(arena);
- let vv = Level::var(i - 1, arena).succ(arena);
- self.substitute_single(i - 1, zero, arena).geq(rhs.substitute_single(i - 1, zero, arena), n, arena)
- && self.substitute_single(i - 1, vv, arena).geq(rhs.substitute_single(i - 1, vv, arena), n, arena)
+ let vv = Level::var(i, arena).succ(arena);
+ self.substitute_single(i, zero, arena).geq(rhs.substitute_single(i, zero, arena), n, arena)
+ && self.substitute_single(i, vv, arena).geq(rhs.substitute_single(i, vv, arena), n, arena)
},
}
}
@@ -90,6 +114,7 @@ mod tests {
#[test]
fn univ_eq() {
use_arena(|arena| {
+ let two = arena.build_level_raw(succ(succ(zero())));
let one = arena.build_level_raw(succ(zero()));
let zero_ = arena.build_level_raw(zero());
let var0 = Level::var(0, arena);
@@ -97,12 +122,15 @@ mod tests {
let succ_var0 = Level::succ(var0, arena);
let max1_var0 = Level::max(one, var0, arena);
let max0_var0 = Level::max(zero_, var0, arena);
+ let imax_0_var0 = Level::imax(zero_, var0, arena);
let max_var0_var1 = Level::max(var0, var1, arena);
let max_var1_var0 = Level::max(var1, var0, arena);
let max_var1_var1 = Level::max(var1, var1, arena);
let succ_max_var0_var1 = Level::succ(max_var0_var1, arena);
let max_succ_var0_succ_var1 = arena.build_level_raw(max(succ(var(0)), succ(var(1))));
+ assert!(!two.geq_no_subst(succ_var0, 0).is_true());
+ assert!(imax_0_var0.is_eq(var0, arena));
assert!(max1_var0.geq(succ_var0, 0, arena));
assert!(!zero_.is_eq(one, arena));
assert!(!one.is_eq(zero_, arena));
diff --git a/kernel/src/calculus/term.rs b/kernel/src/calculus/term.rs
index d332dc99..f2148b83 100644
--- a/kernel/src/calculus/term.rs
+++ b/kernel/src/calculus/term.rs
@@ -16,7 +16,6 @@ impl<'arena> Term<'arena> {
if let Some(red) = self.reduce_recursor(arena) {
return red;
};
- // TODO beta-reduce recursors
match *self {
App(t1, t2) => match *t1 {
Abs(_, t1) => t1.substitute(t2, 1, arena),
diff --git a/kernel/src/memory/declaration/mod.rs b/kernel/src/memory/declaration/mod.rs
index c54d763e..a2ef8888 100644
--- a/kernel/src/memory/declaration/mod.rs
+++ b/kernel/src/memory/declaration/mod.rs
@@ -46,7 +46,12 @@ impl<'arena> fmt::Display for InstantiatedDeclaration<'arena> {
Some(term) => write!(f, "{term}"),
None => {
write!(f, "({}).{{", self.0.payload.decl)?;
- self.0.payload.params.iter().try_for_each(|level| write!(f, "{level}, "))?;
+
+ let mut iter = self.0.payload.params.iter();
+
+ iter.next().map(|level| write!(f, "{level}")).unwrap_or(Ok(()))?;
+ iter.try_for_each(|level| write!(f, ", {level}"))?;
+
write!(f, "}}")
},
}
diff --git a/parser/src/parser.rs b/parser/src/parser.rs
index 18b63945..f303feb4 100644
--- a/parser/src/parser.rs
+++ b/parser/src/parser.rs
@@ -242,6 +242,7 @@ fn convert_error(err: pest::error::Error<Rule>) -> error::Error {
Rule::ImportFile => "import path_to_file".to_owned(),
Rule::Search => "search var".to_owned(),
Rule::Max => "max".to_owned(),
+ Rule::IMax => "imax".to_owned(),
Rule::Plus => "plus".to_owned(),
Rule::arg_univ => "universe argument".to_owned(),
Rule::univ_decl => "universe declaration".to_owned(),
@@ -319,7 +320,7 @@ mod tests {
const COMMAND_ERR: &str = "expected def var := term, def var : term := term, def decl.{ vars, ... } := term, def decl.{ vars, ... } : 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, Type, or Sort";
const SIMPLE_TERM_ERR: &str = "expected variable, abstraction, Prop, Type, Sort, or universe argument";
- const UNIVERSE_ERR: &str = "expected number, variable, abstraction, Prop, Type, Sort, plus, or max";
+ const UNIVERSE_ERR: &str = "expected number, variable, abstraction, Prop, Type, Sort, plus, max, or imax";
#[test]
fn failure_universe_level() {
@@ -341,6 +342,24 @@ mod tests {
Some(declaration::Builder::Decl(box Type(box level::Builder::Const(0)), Vec::new())),
declaration::Builder::Decl(box Prop, Vec::new())
))
+ )
+ }
+
+ #[test]
+ fn successful_declare_with_type_annotation() {
+ assert_eq!(
+ parse_line("def x.{u} : Type u := foo.{u}"),
+ Ok(Declaration(
+ "x",
+ Some(declaration::Builder::Decl(box Type(box level::Builder::Var("u")), ["u"].to_vec())),
+ declaration::Builder::Decl(
+ box kernel::memory::term::builder::Builder::Decl(box declaration::InstantiatedBuilder::Var(
+ "foo",
+ [level::Builder::Var("u")].to_vec()
+ )),
+ ["u"].to_vec()
+ )
+ ))
);
}
@@ -365,6 +384,11 @@ mod tests {
assert_eq!(parse_line("def x := Prop"), Ok(Declaration("x", None, declaration::Builder::Decl(box Prop, Vec::new()))));
}
+ #[test]
+ fn successful_declare() {
+ assert_eq!(parse_line("def x.{} := Prop"), Ok(Declaration("x", None, declaration::Builder::Decl(box Prop, Vec::new()))));
+ }
+
#[test]
fn successful_checktype() {
assert_eq!(parse_line("check Prop : Type"), Ok(CheckType(Prop, Type(box level::Builder::Const(0)))));
@@ -400,6 +424,15 @@ mod tests {
assert_eq!(parse_line("check Sort"), Ok(GetType(Sort(box level::Builder::Const(0)))));
assert_eq!(parse_line("check Sort 0"), Ok(GetType(Sort(box level::Builder::Const(0)))));
assert_eq!(parse_line("check Sort 1"), Ok(GetType(Sort(box level::Builder::Const(1)))));
+ assert_eq!(parse_line("check Sort (0 + 1)"), Ok(GetType(Sort(box level::Builder::Plus(box level::Builder::Const(0), 1)))));
+ assert_eq!(
+ parse_line("check Sort max 0 0"),
+ Ok(GetType(Sort(box level::Builder::Max(box level::Builder::Const(0), box level::Builder::Const(0)))))
+ );
+ assert_eq!(
+ parse_line("check Sort imax 0 0"),
+ Ok(GetType(Sort(box level::Builder::IMax(box level::Builder::Const(0), box level::Builder::Const(0)))))
+ );
}
#[test]
diff --git a/parser/src/term.pest b/parser/src/term.pest
index 72987348..c0250907 100644
--- a/parser/src/term.pest
+++ b/parser/src/term.pest
@@ -28,8 +28,8 @@ Prop = { "Prop" }
Type = { "Type" ~ univ? }
Sort = { "Sort" ~ univ? }
-univ = _{ Plus | Max | Num | string | "(" ~ univ ~ ")" }
-univ_plus = _{ Max | Num | string | "(" ~ univ ~ ")" }
+univ = _{ Plus | Max | IMax | Num | string | "(" ~ univ ~ ")" }
+univ_plus = _{ Max | IMax | Num | string | "(" ~ univ ~ ")" }
Num = { number }
Plus = { univ_plus ~ ( "+" ~ number )+ }
Max = { ( "max" ~ "(" ~ univ ~ "," ~ univ ~ ")" ) | ( "max" ~ univ ~ univ ) }
diff --git a/proost/src/evaluator.rs b/proost/src/evaluator.rs
index 38947a67..c8a2e95f 100644
--- a/proost/src/evaluator.rs
+++ b/proost/src/evaluator.rs
@@ -132,10 +132,10 @@ impl<'arena> Evaluator {
.map(|_| None)
}
- fn process<'build>(
+ fn process(
&mut self,
arena: &mut Arena<'arena>,
- command: &Command<'build>,
+ command: &Command,
importing: &mut Vec<PathBuf>,
) -> Result<'arena, Option<Term<'arena>>> {
match command {
--
GitLab