From 73a68f53121480a7006f33120b875c48bc26bfaa Mon Sep 17 00:00:00 2001
From: arthur-adjedj <arthur.adjedj@gmail.com>
Date: Wed, 9 Nov 2022 15:07:52 +0100
Subject: [PATCH] feat : finish implementation
---
kernel/src/command.rs | 20 ++--
kernel/src/lib.rs | 1 +
kernel/src/term.rs | 179 +++++++++++++++++++++------------
kernel/src/type_checker.rs | 193 ++++++++++++++++++++++-------------
kernel/src/universe.rs | 57 ++++++++++-
parser/src/parser.rs | 201 +++++++++++++++++++++++++++----------
parser/src/term.pest | 27 +++--
7 files changed, 468 insertions(+), 210 deletions(-)
diff --git a/kernel/src/command.rs b/kernel/src/command.rs
index 9bd85a1d..39402a2d 100644
--- a/kernel/src/command.rs
+++ b/kernel/src/command.rs
@@ -38,14 +38,14 @@ mod tests {
fn simple_env() -> Environment {
Environment::new()
- .insert("x".to_string(), Term::Type(0.into()), Term::Prop)
+ .insert("x".to_string(), Term::r#type(0.into()), Term::PROP)
.unwrap()
.clone()
}
#[test]
fn failed_untyped_define() {
- let cmd = Command::Define("x".to_string(), None, Term::Prop);
+ let cmd = Command::Define("x".to_string(), None, Term::PROP);
let mut env = simple_env();
assert!(cmd.process(&mut env).is_err());
@@ -54,21 +54,21 @@ mod tests {
#[test]
fn successful_untyped_define() {
- let cmd = Command::Define("y".to_string(), None, Term::Prop);
+ 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(0.into()))
+ .insert("y".to_string(), Term::PROP, Term::r#type(0.into()))
.unwrap())
);
}
#[test]
fn failed_typed_define() {
- let cmd = Command::Define("y".to_string(), Some(Term::Type(1.into())), Term::Prop);
+ let cmd = Command::Define("y".to_string(), Some(Term::r#type(1.into())), Term::PROP);
let mut env = simple_env();
assert!(cmd.process(&mut env).is_err());
@@ -77,21 +77,21 @@ mod tests {
#[test]
fn successful_typed_define() {
- let cmd = Command::Define("y".to_string(), Some(Term::Type(0.into())), Term::Prop);
+ let cmd = Command::Define("y".to_string(), Some(Term::r#type(0.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(0.into()))
+ .insert("y".to_string(), Term::PROP, Term::r#type(0.into()))
.unwrap())
);
}
#[test]
fn failed_checktype() {
- let cmd = Command::CheckType(Term::Prop, Term::Prop);
+ let cmd = Command::CheckType(Term::PROP, Term::PROP);
let mut env = simple_env();
assert!(cmd.process(&mut env).is_err());
@@ -100,7 +100,7 @@ mod tests {
#[test]
fn successful_checktype() {
- let cmd = Command::CheckType(Term::Prop, Term::Type(0.into()));
+ let cmd = Command::CheckType(Term::PROP, Term::r#type(0.into()));
let mut env = simple_env();
assert!(cmd.process(&mut env).is_ok());
@@ -118,7 +118,7 @@ mod tests {
#[test]
fn successful_gettype() {
- let cmd = Command::GetType(Term::Prop);
+ let cmd = Command::GetType(Term::PROP);
let mut env = simple_env();
assert!(cmd.process(&mut env).is_ok());
diff --git a/kernel/src/lib.rs b/kernel/src/lib.rs
index d8591c4c..70a6a4ca 100644
--- a/kernel/src/lib.rs
+++ b/kernel/src/lib.rs
@@ -15,6 +15,7 @@ pub use derive_more;
pub use num_bigint;
pub use command::Command;
+pub use declaration::Declaration;
pub use environment::Environment;
pub use error::{KernelError, Loc};
pub use term::Term;
diff --git a/kernel/src/term.rs b/kernel/src/term.rs
index e55b3a0f..03c332b1 100644
--- a/kernel/src/term.rs
+++ b/kernel/src/term.rs
@@ -18,11 +18,8 @@ pub enum Term {
#[display(fmt = "{}", _0)]
Const(String, Vec<UniverseLevel>),
- #[display(fmt = "Prop")]
- Prop,
-
- #[display(fmt = "Type {}", _0)]
- Type(UniverseLevel),
+ #[display(fmt = "Sort {}", _0)]
+ Sort(UniverseLevel),
#[display(fmt = "{} {}", _0, _1)]
App(Box<Term>, Box<Term>),
@@ -37,8 +34,17 @@ pub enum Term {
use Term::*;
impl Term {
+ pub const PROP: Term = Sort(UniverseLevel::Zero);
+
+ pub fn r#type(u: UniverseLevel) -> Term {
+ Sort(u + 1)
+ }
+
/// Apply one step of β-reduction, using leftmost outermost evaluation strategy.
pub fn beta_reduction(&self, env: &Environment) -> Term {
+ //if self.is_eliminator() {
+ // return self.compute()
+ //}
match self {
App(box Abs(_, box t1), box t2) => t1.substitute(t2, 1),
App(box t1, box t2) => App(box t1.beta_reduction(env), box t2.clone()),
@@ -75,7 +81,7 @@ impl Term {
/// 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.
+ /// This function is computationally expensive and should only be used for Reduce/Eval commands, not when Sort-checking.
pub fn normal_form(self, env: &Environment) -> Term {
let mut res = self.beta_reduction(env);
let mut temp = self;
@@ -106,8 +112,7 @@ impl Term {
match self {
Var(_) => 0,
Const(..) => 0,
- Prop => 0,
- Type(u) => u.clone().univ_vars(),
+ Sort(u) => u.clone().univ_vars(),
App(t1, t2) | Abs(t1, t2) | Prod(t1, t2) => t1.univ_vars().max(t2.univ_vars()),
}
}
@@ -116,18 +121,35 @@ impl Term {
match self {
Var(_) => self.clone(),
Const(..) => self.clone(),
- Prop => self.clone(),
- Type(u) => Type(u.clone().substitute(vec)),
+ Sort(u) => Sort(u.clone().substitute(vec)),
App(t1, t2) => App(box t1.substitute_univs(vec), box t2.substitute_univs(vec)),
Abs(t1, t2) => Abs(box t1.substitute_univs(vec), box t2.substitute_univs(vec)),
Prod(t1, t2) => Prod(box t1.substitute_univs(vec), box t2.substitute_univs(vec)),
}
}
+
+ /*fn is_eliminator(&self) -> bool {
+ match self {
+ App(
+ box App(
+ box App(
+ box App(
+ box Const(rec,_var),
+ _motive
+ ),
+ _p_zero
+ ),
+ _p_succ
+ ),
+ _n) if rec == "Nat_rec" => true,
+ _ => false
+ }
+ }*/
}
#[cfg(test)]
mod tests {
- // /!\ most of these tests are on ill-typed terms and should not be used for further testings
+ // /!\ most of these tests are on ill-Sortd terms and should not be used for further testings
use super::Term::*;
use crate::term::Environment;
use crate::universe::UniverseLevel;
@@ -136,15 +158,21 @@ mod tests {
fn simple_subst() {
// λx.(λy.x y) x
let term = Abs(
- box Prop,
+ box Sort(0.into()),
box App(
- box Abs(box Prop, box App(box Var(2.into()), box Var(1.into()))),
+ box Abs(
+ box Sort(0.into()),
+ 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())));
+ let reduced = Abs(
+ box Sort(0.into()),
+ box App(box Var(1.into()), box Var(1.into())),
+ );
assert_eq!(term.beta_reduction(&Environment::new()), reduced);
}
@@ -154,19 +182,19 @@ mod tests {
// (λa.λb.λc.a (λd.λe.e (d b)) (λ_.c) (λd.d)) (λa.λb.a b)
let term = App(
box Abs(
- box Prop,
+ box Sort(0.into()),
box Abs(
- box Prop,
+ box Sort(0.into()),
box Abs(
- box Prop,
+ box Sort(0.into()),
box App(
box App(
box App(
box Var(3.into()),
box Abs(
- box Prop,
+ box Sort(0.into()),
box Abs(
- box Prop,
+ box Sort(0.into()),
box App(
box Var(1.into()),
box App(box Var(2.into()), box Var(4.into())),
@@ -174,34 +202,40 @@ mod tests {
),
),
),
- box Abs(box Prop, box Var(2.into())),
+ box Abs(box Sort(0.into()), box Var(2.into())),
),
- box Abs(box Prop, box Var(1.into())),
+ box Abs(box Sort(0.into()), box Var(1.into())),
),
),
),
),
box Abs(
- box Prop,
- box Abs(box Prop, box App(box Var(2.into()), box Var(1.into()))),
+ box Sort(0.into()),
+ box Abs(
+ box Sort(0.into()),
+ box App(box Var(2.into()), box Var(1.into())),
+ ),
),
);
let term_step_1 = Abs(
- box Prop,
+ box Sort(0.into()),
box Abs(
- box Prop,
+ box Sort(0.into()),
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 Sort(0.into()),
+ box Abs(
+ box Sort(0.into()),
+ box App(box Var(2.into()), box Var(1.into())),
+ ),
),
box Abs(
- box Prop,
+ box Sort(0.into()),
box Abs(
- box Prop,
+ box Sort(0.into()),
box App(
box Var(1.into()),
box App(box Var(2.into()), box Var(4.into())),
@@ -209,26 +243,26 @@ mod tests {
),
),
),
- box Abs(box Prop, box Var(2.into())),
+ box Abs(box Sort(0.into()), box Var(2.into())),
),
- box Abs(box Prop, box Var(1.into())),
+ box Abs(box Sort(0.into()), box Var(1.into())),
),
),
);
let term_step_2 = Abs(
- box Prop,
+ box Sort(0.into()),
box Abs(
- box Prop,
+ box Sort(0.into()),
box App(
box App(
box Abs(
- box Prop,
+ box Sort(0.into()),
box App(
box Abs(
- box Prop,
+ box Sort(0.into()),
box Abs(
- box Prop,
+ box Sort(0.into()),
box App(
box Var(1.into()),
box App(box Var(2.into()), box Var(5.into())),
@@ -238,74 +272,86 @@ mod tests {
box Var(1.into()),
),
),
- box Abs(box Prop, box Var(2.into())),
+ box Abs(box Sort(0.into()), box Var(2.into())),
),
- box Abs(box Prop, box Var(1.into())),
+ box Abs(box Sort(0.into()), box Var(1.into())),
),
),
);
let term_step_3 = Abs(
- box Prop,
+ box Sort(0.into()),
box Abs(
- box Prop,
+ box Sort(0.into()),
box App(
box App(
box Abs(
- box Prop,
+ box Sort(0.into()),
box Abs(
- box Prop,
+ box Sort(0.into()),
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 Sort(0.into()), box Var(2.into())),
),
- box Abs(box Prop, box Var(1.into())),
+ box Abs(box Sort(0.into()), box Var(1.into())),
),
),
);
let term_step_4 = Abs(
- box Prop,
+ box Sort(0.into()),
box Abs(
- box Prop,
+ box Sort(0.into()),
box App(
box Abs(
- box Prop,
+ box Sort(0.into()),
box App(
box Var(1.into()),
- box App(box Abs(box Prop, box Var(3.into())), box Var(3.into())),
+ box App(
+ box Abs(box Sort(0.into()), box Var(3.into())),
+ box Var(3.into()),
+ ),
),
),
- box Abs(box Prop, box Var(1.into())),
+ box Abs(box Sort(0.into()), box Var(1.into())),
),
),
);
let term_step_5 = Abs(
- box Prop,
+ box Sort(0.into()),
box Abs(
- box Prop,
+ box Sort(0.into()),
box App(
- box Abs(box Prop, box Var(1.into())),
- box App(box Abs(box Prop, box Var(2.into())), box Var(2.into())),
+ box Abs(box Sort(0.into()), box Var(1.into())),
+ box App(
+ box Abs(box Sort(0.into()), box Var(2.into())),
+ box Var(2.into()),
+ ),
),
),
);
let term_step_6 = Abs(
- box Prop,
+ box Sort(0.into()),
box Abs(
- box Prop,
- box App(box Abs(box Prop, box Var(2.into())), box Var(2.into())),
+ box Sort(0.into()),
+ box App(
+ box Abs(box Sort(0.into()), 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 term_step_7 = Abs(
+ box Sort(0.into()),
+ box Abs(box Sort(0.into()), box Var(1.into())),
+ );
let env = Environment::new();
@@ -322,16 +368,23 @@ mod tests {
#[test]
fn shift_prod() {
let t1 = Prod(box Var(1.into()), box Var(1.into()));
- let t2 = App(box Abs(box Prop, box t1.clone()), box Prop);
+ let t2 = App(
+ box Abs(box Sort(0.into()), box t1.clone()),
+ box Sort(0.into()),
+ );
assert_eq!(t2.beta_reduction(&Environment::new()), t1)
}
#[test]
fn beta_red_const() {
- let id_prop = Prod(box Prop, box Prod(box Var(1.into()), box Var(1.into())));
+ let id_prop = Prod(
+ box Sort(0.into()),
+ box Prod(box Var(1.into()), box Var(1.into())),
+ );
let mut env = Environment::new();
- env.insert("foo".into(), id_prop.clone(), Prop).unwrap();
+ env.insert("foo".into(), id_prop.clone(), Sort(0.into()))
+ .unwrap();
assert_eq!(
Const("foo".into(), Vec::new()).beta_reduction(&env),
@@ -342,15 +395,15 @@ mod tests {
#[test]
fn poly_univ_id() {
let id_ty = Prod(
- box Type(UniverseLevel::Var(0)),
+ box Sort(UniverseLevel::Var(0)),
box Prod(box Var(1.into()), box Var(2.into())),
);
let id_te = Abs(
- box Type(UniverseLevel::Var(0)),
+ box Sort(UniverseLevel::Var(0)),
box Abs(box Var(1.into()), box Var(1.into())),
);
let id_zero = Abs(
- box Type(0.into()),
+ box Sort(0.into()),
box Abs(box Var(1.into()), box Var(1.into())),
);
assert!(id_te.check(&id_ty, &Environment::new()).is_ok());
diff --git a/kernel/src/type_checker.rs b/kernel/src/type_checker.rs
index 043060dc..fbe9b3d5 100644
--- a/kernel/src/type_checker.rs
+++ b/kernel/src/type_checker.rs
@@ -46,9 +46,9 @@ impl Term {
/// 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, lvl: DeBruijnIndex) -> bool {
match (self.whnf(env), rhs.whnf(env)) {
- (Type(i), Type(j)) => i.is_eq(&j),
+ (lhs, rhs) if lhs == rhs => true,
- (Prop, Prop) => true,
+ (Sort(i), Sort(j)) => i.is_eq(&j),
(Var(i), Var(j)) => i == j,
@@ -91,27 +91,16 @@ impl Term {
/// Computes universe the universe in which `(x : A) -> B` lives when `A : u1` and `B : u2`.
fn imax(&self, rhs: &Term) -> Result<Term, KernelError> {
- match rhs {
- // Because Prop is impredicative, if B : Prop, then (x : A) -> b : Prop
- Prop => Ok(Prop),
-
- Type(ref i) => match self {
- Prop => Ok(Type(i.clone())),
-
- // else if u1 = Type(i) and u2 = Type(j), then (x : A) -> B : Type(max(i,j))
- Type(j) => Ok(Type(UniverseLevel::Max(box i.clone(), box j.clone()))),
-
- _ => Err(KernelError::NotUniverse(self.clone())),
- },
-
+ match (self, rhs) {
+ (Sort(u), Sort(v)) => Ok(Sort(UniverseLevel::IMax(box u.clone(), box v.clone()))),
+ (Sort(_), _) => Err(KernelError::NotUniverse(rhs.clone())),
_ => Err(KernelError::NotUniverse(rhs.clone())),
}
}
fn _infer(&self, env: &Environment, ctx: &mut Context) -> Result<Term, KernelError> {
match self {
- Prop => Ok(Type(UniverseLevel::Zero)),
- Type(i) => Ok(Type(i.clone() + 1)),
+ Sort(i) => Ok(Sort(i.clone() + 1)),
Var(i) => Ok(ctx.types[ctx.lvl - *i].clone()),
Const(s, vec) => match env.get_type(s, vec) {
@@ -170,41 +159,50 @@ mod tests {
use crate::type_checker::*;
fn id(l: usize) -> Box<Term> {
- box Abs(box Prop, box Var(l.into()))
+ box Abs(box Sort(0.into()), box Var(l.into()))
}
#[test]
fn var_subst_1() {
// (λ P. λP. 1) (λP.1)
let t = App(
- box Abs(box Prop, box Abs(box Prop, box Var(1.into()))),
+ box Abs(
+ box Sort(0.into()),
+ box Abs(box Sort(0.into()), box Var(1.into())),
+ ),
id(1),
);
- let nf = Abs(box Prop, box Var(1.into()));
+ let nf = Abs(box Sort(0.into()), box Var(1.into()));
assert_eq!(t.normal_form(&Environment::new()), nf)
}
#[test]
fn var_subst_2() {
let t = App(
- box Abs(box Prop, box Abs(box Prop, box Var(2.into()))),
+ box Abs(
+ box Sort(0.into()),
+ box Abs(box Sort(0.into()), box Var(2.into())),
+ ),
id(1),
);
- let nf = Abs(box Prop, id(1));
+ let nf = Abs(box Sort(0.into()), id(1));
assert_eq!(t.normal_form(&Environment::new()), nf)
}
#[test]
fn simple() {
- let t1 = App(box Abs(box Type(0.into()), box Var(1.into())), box Prop);
+ let t1 = App(
+ box Abs(box Sort(1.into()), box Var(1.into())),
+ box Sort(0.into()),
+ );
- let t2 = Prop;
+ let t2 = Sort(0.into());
assert!(t1.conversion(&t2, &Environment::new(), 0.into()));
let ty = t1.infer(&Environment::new());
- assert_eq!(ty, Ok(Type(0.into())));
+ assert_eq!(ty, Ok(Sort(1.into())));
}
#[test]
@@ -212,15 +210,21 @@ mod tests {
// λ (x : P -> P).(λ (y :P).x y) x
//λ P -> P.(λ P.2 1) 1
let term = Abs(
- box Prod(box Prop, box Prop),
+ box Prod(box Sort(0.into()), box Sort(0.into())),
box App(
- box Abs(box Prop, box App(box Var(2.into()), box Var(1.into()))),
+ box Abs(
+ box Sort(0.into()),
+ 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())));
+ let reduced = Abs(
+ box Sort(0.into()),
+ box App(box Var(1.into()), box Var(1.into())),
+ );
assert!(term.is_def_eq(&reduced, &Environment::new()).is_ok());
assert!(term.infer(&Environment::new()).is_err());
}
@@ -235,34 +239,40 @@ mod tests {
// (P → P) → ((P → P) → P)
box Prod(
// P -> P
- box Prod(box Prop, box Prop),
+ box Prod(box Sort(0.into()), box Sort(0.into())),
// (P -> P) -> P
- box Prod(box Prod(box Prop, box Prop), box Prop),
+ box Prod(
+ box Prod(box Sort(0.into()), box Sort(0.into())),
+ box Sort(0.into()),
+ ),
),
// (P → P) → ((P → P) → P)
box Prod(
// P -> P
- box Prod(box Prop, box Prop),
+ box Prod(box Sort(0.into()), box Sort(0.into())),
// (P -> P) -> P
- box Prod(box Prod(box Prop, box Prop), box Prop),
+ box Prod(
+ box Prod(box Sort(0.into()), box Sort(0.into())),
+ box Sort(0.into()),
+ ),
),
),
box Abs(
// b : P
- box Prop,
+ box Sort(0.into()),
box Abs(
// c : P
- box Prop,
+ box Sort(0.into()),
box App(
box App(
box App(
box Var(3.into()),
box Abs(
// d : P -> P
- box Prod(box Prop, box Prop),
+ box Prod(box Sort(0.into()), box Sort(0.into())),
box Abs(
// e : P -> P
- box Prod(box Prop, box Prop),
+ box Prod(box Sort(0.into()), box Sort(0.into())),
box App(
box Var(1.into()),
box App(box Var(2.into()), box Var(4.into())),
@@ -271,10 +281,10 @@ mod tests {
),
),
// _ : P
- box Abs(box Prop, box Var(2.into())),
+ box Abs(box Sort(0.into()), box Var(2.into())),
),
//d : P
- box Abs(box Prop, box Var(1.into())),
+ box Abs(box Sort(0.into()), box Var(1.into())),
),
),
),
@@ -282,19 +292,25 @@ mod tests {
box Abs(
//a : (P -> P) -> (P -> P) -> P
box Prod(
- box Prod(box Prop, box Prop),
- box Prod(box Prod(box Prop, box Prop), box Prop),
+ box Prod(box Sort(0.into()), box Sort(0.into())),
+ box Prod(
+ box Prod(box Sort(0.into()), box Sort(0.into())),
+ box Sort(0.into()),
+ ),
),
box Abs(
//b : P -> P
- box Prod(box Prop, box Prop),
+ box Prod(box Sort(0.into()), box Sort(0.into())),
box App(box Var(2.into()), box Var(1.into())),
),
),
);
// λa : P.λb : P .b
- let reduced = Abs(box Prop, box Abs(box Prop, box Var(1.into())));
+ let reduced = Abs(
+ box Sort(0.into()),
+ box Abs(box Sort(0.into()), box Var(1.into())),
+ );
assert!(term.is_def_eq(&reduced, &Environment::new()).is_ok());
assert!(term.infer(&Environment::new()).is_ok())
}
@@ -303,7 +319,10 @@ mod tests {
#[test]
fn nf_test() {
//λa.a (λx.x) (λx.x)
- let reduced = Abs(box Prop, box App(box App(box Var(2.into()), id(1)), id(1)));
+ let reduced = Abs(
+ box Sort(0.into()),
+ box App(box App(box Var(2.into()), id(1)), id(1)),
+ );
let nff = reduced.clone().normal_form(&Environment::new());
assert_eq!(reduced, nff);
@@ -313,7 +332,7 @@ mod tests {
#[test]
fn polymorphism() {
let id = Abs(
- box Type(0.into()),
+ box Sort(0.into()),
box Abs(box Var(1.into()), box Var(1.into())),
);
@@ -322,45 +341,54 @@ mod tests {
#[test]
fn type_type() {
- assert!(Type(0.into())
- .check(&Type(1.into()), &Environment::new())
+ assert!(Sort(0.into())
+ .check(&Sort(1.into()), &Environment::new())
.is_ok());
}
#[test]
fn not_function() {
- let t = App(box Prop, box Prop);
+ let t = App(box Sort(0.into()), box Sort(0.into()));
assert!(t.infer(&Environment::new()).is_err())
}
#[test]
fn not_type_prod() {
- let t = Prod(box Abs(box Prop, box Var(1.into())), box Prop);
+ let t = Prod(
+ box Abs(box Sort(0.into()), box Var(1.into())),
+ box Sort(0.into()),
+ );
assert!(t.infer(&Environment::new()).is_err());
- let t = Prod(box Prop, box Abs(box Prop, box Prop));
+ let t = Prod(
+ box Sort(0.into()),
+ box Abs(box Sort(0.into()), box Sort(0.into())),
+ );
assert!(t.infer(&Environment::new()).is_err());
- let wf_prod = Prod(box Prop, box Prop);
+ let wf_prod = Prod(box Sort(0.into()), box Sort(0.into()));
println!("{:?}", wf_prod.infer(&Environment::new()));
- assert!(wf_prod.check(&Type(0.into()), &Environment::new()).is_ok());
+ assert!(wf_prod.check(&Sort(1.into()), &Environment::new()).is_ok());
- let wf_prod = Prod(box Prop, box Var(1.into()));
- assert!(wf_prod.check(&Prop, &Environment::new()).is_ok());
+ let wf_prod = Prod(box Sort(0.into()), box Var(1.into()));
+ assert!(wf_prod.check(&Sort(0.into()), &Environment::new()).is_ok());
- // Type0 -> (A : Prop) ->
- let wf_prod = Prod(box Prop, box Prop);
- assert!(wf_prod.check(&Type(0.into()), &Environment::new()).is_ok());
+ // Sort0 -> (A : Sort(0.into())) ->
+ let wf_prod = Prod(box Sort(0.into()), box Sort(0.into()));
+ assert!(wf_prod.check(&Sort(1.into()), &Environment::new()).is_ok());
}
#[test]
fn poly_test2() {
let t = Abs(
- box Prop,
+ box Sort(0.into()),
box Abs(
- box Prop,
+ box Sort(0.into()),
box Abs(
- box Prod(box Prop, box Prod(box Prop, box Prop)),
+ box Prod(
+ box Sort(0.into()),
+ box Prod(box Sort(0.into()), box Sort(0.into())),
+ ),
box App(
box App(box Var(1.into()), box Var(3.into())),
box Var(2.into()),
@@ -374,10 +402,18 @@ mod tests {
#[test]
fn env_test() {
- let id_prop = Prod(box Prop, box Prod(box Var(1.into()), box Var(2.into())));
- let t = Abs(box Prop, box Abs(box Var(1.into()), box Var(1.into())));
+ let id_prop = Prod(
+ box Sort(0.into()),
+ box Prod(box Var(1.into()), box Var(2.into())),
+ );
+ let t = Abs(
+ box Sort(0.into()),
+ box Abs(box Var(1.into()), box Var(1.into())),
+ );
let mut binding = Environment::new();
- let env = binding.insert("foo".into(), id_prop.clone(), Prop).unwrap();
+ let env = binding
+ .insert("foo".into(), id_prop.clone(), Sort(0.into()))
+ .unwrap();
assert!(t.check(&Const("foo".into(), Vec::new()), env).is_ok());
assert!(id_prop
@@ -387,21 +423,28 @@ mod tests {
#[test]
fn check_bad() {
- assert!(Prop.check(&Prop, &Environment::new()).is_err());
+ assert!(Sort(0.into())
+ .check(&Sort(0.into()), &Environment::new())
+ .is_err());
}
#[test]
fn not_def_eq() {
- assert!(Prop
- .is_def_eq(&Type(0.into()), &Environment::new())
+ assert!(Sort(0.into())
+ .is_def_eq(&Sort(1.into()), &Environment::new())
.is_err());
}
#[test]
fn infer_const() {
- let id_prop = Prod(box Prop, box Prod(box Var(1.into()), box Var(1.into())));
+ let id_prop = Prod(
+ box Sort(0.into()),
+ box Prod(box Var(1.into()), box Var(1.into())),
+ );
let mut binding = Environment::new();
- let env = binding.insert("foo".into(), id_prop, Prop).unwrap();
+ let env = binding
+ .insert("foo".into(), id_prop, Sort(0.into()))
+ .unwrap();
assert!(Const("foo".into(), Vec::new()).infer(env).is_ok());
assert!(Const("foo".into(), Vec::new())
@@ -411,17 +454,23 @@ mod tests {
#[test]
fn prod_var() {
- let ty = Prod(box Prop, box Prod(box Var(1.into()), box Var(2.into())));
- let t = Abs(box Prop, box Abs(box Var(1.into()), box Var(1.into())));
+ let ty = Prod(
+ box Sort(0.into()),
+ box Prod(box Var(1.into()), box Var(2.into())),
+ );
+ let t = Abs(
+ box Sort(0.into()),
+ box Abs(box Var(1.into()), box Var(1.into())),
+ );
assert!(t.check(&ty, &Environment::new()).is_ok())
}
#[test]
fn univ_reduc() {
let ty = App(
- box Abs(box Prop, box Type(0.into())),
- box Prod(box Prop, box Var(1.into())),
+ box Abs(box Sort(0.into()), box Sort(0.into())),
+ box Prod(box Sort(0.into()), box Var(1.into())),
);
- assert!(ty.conversion(&Type(0.into()), &Environment::new(), 0.into()))
+ assert!(ty.conversion(&Sort(0.into()), &Environment::new(), 0.into()))
}
}
diff --git a/kernel/src/universe.rs b/kernel/src/universe.rs
index 1da5d8ee..40d3bf99 100644
--- a/kernel/src/universe.rs
+++ b/kernel/src/universe.rs
@@ -11,6 +11,8 @@ pub enum UniverseLevel {
Max(Box<UniverseLevel>, Box<UniverseLevel>),
+ IMax(Box<UniverseLevel>, Box<UniverseLevel>),
+
Var(usize),
}
@@ -57,6 +59,13 @@ impl UniverseLevel {
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,
}
}
@@ -78,10 +87,11 @@ impl UniverseLevel {
None => match self {
Zero => unreachable!("Zero is a numeral"),
Succ(_) => match self.plus() {
- (u, 0) => format!("{}", u.pretty_print()),
+ (u, 0) => u.pretty_print(),
(u, n) => format!("{} + {}", u.pretty_print(), n),
},
Max(box n, box m) => 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),
},
}
@@ -92,6 +102,7 @@ impl UniverseLevel {
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,
}
}
@@ -101,6 +112,7 @@ impl UniverseLevel {
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(),
}
}
@@ -113,6 +125,49 @@ impl UniverseLevel {
(_, Succ(box l)) if self.geq(l, n + 1) => true,
(_, Max(box l1, box l2)) if self.geq(l1, n) || self.geq(l2, n) => true,
(Max(box l1, box l2), _) if l1.geq(u2, n) && l2.geq(u2, n) => true,
+ (IMax(_, box Zero), l) if Zero.geq(l, n) => true,
+ (IMax(l1, box Succ(l2)), l) if Max(l1.clone(), box Succ(l2.clone())).geq(l, n) => true,
+ (l, IMax(l1, box Succ(l2))) if l.geq(&Max(l1.clone(), box Succ(l2.clone())), n) => true,
+ (Max(l1, box IMax(l2, l3)), l)
+ if Max(
+ box IMax(l1.clone(), l3.clone()),
+ box IMax(l2.clone(), l3.clone()),
+ )
+ .geq(l, n) =>
+ {
+ true
+ }
+ (l, IMax(l1, box IMax(l2, l3)))
+ if l.geq(
+ &Max(
+ box IMax(l1.clone(), l3.clone()),
+ box IMax(l2.clone(), l3.clone()),
+ ),
+ n,
+ ) =>
+ {
+ true
+ }
+ (IMax(l1, box Max(l2, l3)), l)
+ if Max(
+ box IMax(l1.clone(), l2.clone()),
+ box IMax(l1.clone(), l3.clone()),
+ )
+ .geq(l, n) =>
+ {
+ true
+ }
+ (l, IMax(l1, box Max(l2, l3)))
+ if l.geq(
+ &Max(
+ box IMax(l1.clone(), l2.clone()),
+ box IMax(l1.clone(), l3.clone()),
+ ),
+ n,
+ ) =>
+ {
+ true
+ }
_ => false,
}
}
diff --git a/parser/src/parser.rs b/parser/src/parser.rs
index 4631bcda..39f825e8 100644
--- a/parser/src/parser.rs
+++ b/parser/src/parser.rs
@@ -2,17 +2,18 @@ use kernel::{Command, KernelError, Loc, Term, UniverseLevel};
use pest::error::{Error, LineColLocation};
use pest::iterators::Pair;
use pest::{Parser, Span};
-use std::collections::VecDeque;
+use std::collections::{HashMap, VecDeque};
#[derive(Parser)]
#[grammar = "term.pest"]
struct CommandParser;
/// build universe level from errorless pest's output
-fn build_universe_level_from_expr(pair: Pair<Rule>) -> UniverseLevel {
+fn build_universe_level_from_expr(
+ pair: Pair<Rule>,
+ univ_var_map: &HashMap<String, usize>,
+) -> UniverseLevel {
match pair.as_rule() {
- //TODO after term refactor (new ways to deal with variables)
- Rule::Var => UniverseLevel::Var(0),
Rule::Num => {
let n = pair.into_inner().as_str().parse().unwrap();
let mut univ = UniverseLevel::Zero;
@@ -23,19 +24,26 @@ fn build_universe_level_from_expr(pair: Pair<Rule>) -> UniverseLevel {
}
Rule::Max => {
let mut iter = pair.into_inner();
- let univ1 = build_universe_level_from_expr(iter.next().unwrap());
- let univ2 = build_universe_level_from_expr(iter.next().unwrap());
+ let univ1 = build_universe_level_from_expr(iter.next().unwrap(), univ_var_map);
+ let univ2 = build_universe_level_from_expr(iter.next().unwrap(), univ_var_map);
UniverseLevel::Max(box univ1, box univ2)
}
Rule::Plus => {
let mut iter = pair.into_inner();
- let mut univ = build_universe_level_from_expr(iter.next().unwrap());
+ let mut univ = build_universe_level_from_expr(iter.next().unwrap(), univ_var_map);
let n = iter.map(|x| x.as_str().parse::<u64>().unwrap()).sum();
for _ in 0..n {
univ = UniverseLevel::Succ(box univ);
}
univ
}
+ Rule::string => {
+ let name = pair.as_str().to_string();
+ match univ_var_map.get(&name) {
+ Some(n) => UniverseLevel::Var(*n),
+ None => panic!("Universe level {:?} is unbound", name),
+ }
+ }
univ => unreachable!("Unexpected universe level: {:?}", univ),
}
}
@@ -47,27 +55,65 @@ fn convert_span(span: Span) -> Loc {
Loc::new(x1, y1, x2, y2)
}
+fn build_univ_map_from_expr(pair: Pair<Rule>) -> HashMap<String, usize> {
+ let iter = pair.into_inner();
+ let mut map = HashMap::new();
+ for (i,pair) in iter.enumerate() {
+ let str = pair.as_str();
+ if map.insert(str.to_string(), i).is_some() {
+ panic!("Duplicate universe variable {}", str);
+ }
+ }
+ map
+}
+
+fn build_univ_bindings_from_expr(
+ pair: Pair<Rule>,
+ univ_var_map: &HashMap<String, usize>,
+) -> Vec<UniverseLevel> {
+ let iter = pair.into_inner();
+ let mut vec = Vec::new();
+ for pair in iter {
+ vec.push(build_universe_level_from_expr(pair, univ_var_map));
+ }
+ vec
+}
+
/// build terms from errorless pest's output
-fn build_term_from_expr(pair: Pair<Rule>, known_vars: &mut VecDeque<String>) -> Term {
+fn build_term_from_expr(
+ pair: Pair<Rule>,
+ known_vars: &mut VecDeque<String>,
+ univ_var_map: &HashMap<String, usize>,
+) -> Term {
// location to be used in a future version
let _loc = convert_span(pair.as_span());
match pair.as_rule() {
- Rule::Prop => Term::Prop,
+ Rule::Prop => Term::Sort(0.into()),
Rule::Type => match pair.into_inner().next() {
- Some(pair) => Term::Type(build_universe_level_from_expr(pair)),
- None => Term::Type(UniverseLevel::Zero),
+ Some(pair) => Term::Sort(build_universe_level_from_expr(pair, univ_var_map) + 1),
+ None => Term::Sort(UniverseLevel::Zero + 1),
+ },
+ Rule::Sort => match pair.into_inner().next() {
+ Some(pair) => Term::Sort(build_universe_level_from_expr(pair, univ_var_map)),
+ None => Term::Sort(UniverseLevel::Zero),
},
Rule::Var => {
- let name = pair.into_inner().as_str().to_string();
+ let mut iter = pair.into_inner();
+ let name = iter.next().unwrap().as_str().to_string();
match known_vars.iter().position(|x| *x == name) {
Some(i) => Term::Var((i + 1).into()),
- None => Term::Const(name, Vec::new()),
+ None => Term::Const(
+ name,
+ iter.next()
+ .map(|x| build_univ_bindings_from_expr(x, univ_var_map))
+ .unwrap_or_default(),
+ ),
}
}
Rule::App => {
let mut iter = pair
.into_inner()
- .map(|x| build_term_from_expr(x, known_vars));
+ .map(|x| build_term_from_expr(x, known_vars, univ_var_map));
let t = iter.next().unwrap();
iter.fold(t, |acc, x| Term::App(box acc, box x))
}
@@ -79,11 +125,15 @@ fn build_term_from_expr(pair: Pair<Rule>, known_vars: &mut VecDeque<String>) ->
let mut iter = pair.into_inner();
let old_pair = iter.next_back().unwrap();
for pair in iter {
- terms.push(build_term_from_expr(old_pair.clone(), known_vars));
+ terms.push(build_term_from_expr(
+ old_pair.clone(),
+ known_vars,
+ univ_var_map,
+ ));
known_vars.push_front(pair.as_str().to_string());
}
}
- let t = build_term_from_expr(pair, known_vars);
+ let t = build_term_from_expr(pair, known_vars, univ_var_map);
terms.into_iter().rev().fold(t, |acc, x| {
known_vars.pop_front();
Term::Abs(box x, box acc)
@@ -97,11 +147,15 @@ fn build_term_from_expr(pair: Pair<Rule>, known_vars: &mut VecDeque<String>) ->
let mut iter = pair.into_inner();
let old_pair = iter.next_back().unwrap();
for pair in iter {
- terms.push(build_term_from_expr(old_pair.clone(), known_vars));
+ terms.push(build_term_from_expr(
+ old_pair.clone(),
+ known_vars,
+ univ_var_map,
+ ));
known_vars.push_front(pair.as_str().to_string());
}
}
- let t = build_term_from_expr(pair, known_vars);
+ let t = build_term_from_expr(pair, known_vars, univ_var_map);
terms.into_iter().rev().fold(t, |acc, x| {
known_vars.pop_front();
Term::Prod(box x, box acc)
@@ -112,11 +166,11 @@ fn build_term_from_expr(pair: Pair<Rule>, known_vars: &mut VecDeque<String>) ->
let pair = iter.next_back().unwrap();
let mut terms = Vec::new();
for pair in iter {
- let t = build_term_from_expr(pair, known_vars);
+ let t = build_term_from_expr(pair, known_vars, univ_var_map);
known_vars.push_front("_".to_string());
terms.push(t);
}
- let t = build_term_from_expr(pair, known_vars);
+ let t = build_term_from_expr(pair, known_vars, univ_var_map);
terms.into_iter().rev().fold(t, |acc, x| {
known_vars.pop_front();
Term::Prod(box x, box acc)
@@ -133,31 +187,51 @@ fn build_command_from_expr(pair: Pair<Rule>) -> Command {
match pair.as_rule() {
Rule::GetType => {
let mut iter = pair.into_inner();
- let t = build_term_from_expr(iter.next().unwrap(), &mut VecDeque::new());
+ let t =
+ build_term_from_expr(iter.next().unwrap(), &mut VecDeque::new(), &HashMap::new());
Command::GetType(t)
}
Rule::CheckType => {
let mut iter = pair.into_inner();
- let t1 = build_term_from_expr(iter.next().unwrap(), &mut VecDeque::new());
- let t2 = build_term_from_expr(iter.next().unwrap(), &mut VecDeque::new());
+ let t1 =
+ build_term_from_expr(iter.next().unwrap(), &mut VecDeque::new(), &HashMap::new());
+ let t2 =
+ build_term_from_expr(iter.next().unwrap(), &mut VecDeque::new(), &HashMap::new());
Command::CheckType(t1, t2)
}
Rule::Define => {
let mut iter = pair.into_inner();
let s = iter.next().unwrap().as_str().to_string();
- let term = build_term_from_expr(iter.next().unwrap(), &mut VecDeque::new());
+ //let _univ_params = iter.next();
+ let next = iter.next();
+ let term = {
+ if matches!(
+ next.clone().map(|x| x.as_rule()),
+ None | Some(Rule::univ_decl)
+ ) {
+ let univs = next
+ .map(build_univ_map_from_expr )
+ .unwrap_or_default();
+ build_term_from_expr(iter.next().unwrap(), &mut VecDeque::new(), &univs)
+ } else {
+ build_term_from_expr(next.unwrap(), &mut VecDeque::new(), &HashMap::new())
+ }
+ };
Command::Define(s, None, term)
}
Rule::DefineCheckType => {
let mut iter = pair.into_inner();
let s = iter.next().unwrap().as_str().to_string();
- let t = build_term_from_expr(iter.next().unwrap(), &mut VecDeque::new());
- let term = build_term_from_expr(iter.next().unwrap(), &mut VecDeque::new());
+ let t =
+ build_term_from_expr(iter.next().unwrap(), &mut VecDeque::new(), &HashMap::new());
+ let term =
+ build_term_from_expr(iter.next().unwrap(), &mut VecDeque::new(), &HashMap::new());
Command::Define(s, Some(t), term)
}
Rule::Eval => {
let mut iter = pair.into_inner();
- let t = build_term_from_expr(iter.next().unwrap(), &mut VecDeque::new());
+ let t =
+ build_term_from_expr(iter.next().unwrap(), &mut VecDeque::new(), &HashMap::new());
Command::Eval(t)
}
@@ -174,14 +248,23 @@ fn convert_error(err: Error<Rule>) -> KernelError {
Rule::Define => "def var := term".to_owned(),
Rule::CheckType => "check term : term".to_owned(),
Rule::GetType => "check term".to_owned(),
+ Rule::Eval => "eval term".to_owned(),
Rule::DefineCheckType => "def var : term := term".to_owned(),
Rule::Abs => "abstraction".to_owned(),
Rule::dProd => "dependent product".to_owned(),
Rule::Prod => "product".to_owned(),
Rule::App => "application".to_owned(),
Rule::Prop => "Prop".to_owned(),
+ Rule::Sort => "Sort".to_owned(),
Rule::Type => "Type".to_owned(),
- _ => unreachable!("low level rules cannot appear in error messages"),
+ Rule::Max => "max".to_owned(),
+ Rule::Plus => "plus".to_owned(),
+ Rule::arg_univ => "universe argument".to_owned(),
+ Rule::univ_decl => "universe declaration".to_owned(),
+ rule => {
+ println!("{:?}", rule);
+ unreachable!("low level rules cannot appear in error messages")
+ }
});
// extracting the location from the pest output
@@ -252,11 +335,13 @@ mod tests {
/// Error messages
const COMMAND_ERR: &str =
- "expected def var := term, def var : term := term, check term : term, or check term";
+ "expected eval term, def var := term, def var : term := term, check term : term, or check term";
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";
+ "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";
#[test]
fn failure_universe_level() {
@@ -273,7 +358,11 @@ mod tests {
fn successful_definechecktype() {
assert_eq!(
parse_line("def x : Type := Prop"),
- Ok(Define("x".to_string(), Some(Type(0.into())), Prop))
+ Ok(Define(
+ "x".to_string(),
+ Some(Sort(1.into())),
+ Sort(0.into())
+ ))
)
}
@@ -281,7 +370,7 @@ mod tests {
fn successful_define() {
assert_eq!(
parse_line("def x := Prop"),
- Ok(Define("x".to_string(), None, Prop))
+ Ok(Define("x".to_string(), None, Sort(0.into())))
)
}
@@ -289,13 +378,13 @@ mod tests {
fn successful_checktype() {
assert_eq!(
parse_line("check Prop : Type"),
- Ok(CheckType(Prop, Type(0.into())))
+ Ok(CheckType(Sort(0.into()), Sort(1.into())))
)
}
#[test]
fn successful_gettype_prop() {
- assert_eq!(parse_line("check Prop"), Ok(GetType(Prop)))
+ assert_eq!(parse_line("check Prop"), Ok(GetType(Sort(0.into()))))
}
#[test]
@@ -306,15 +395,15 @@ mod tests {
);
assert_eq!(
parse_line("check fun A:Prop => A"),
- Ok(GetType(Abs(box Prop, box Var(1.into()))))
+ Ok(GetType(Abs(box Sort(0.into()), box Var(1.into()))))
)
}
#[test]
fn successful_type() {
- assert_eq!(parse_line("check Type"), Ok(GetType(Type(0.into()))));
- assert_eq!(parse_line("check Type 0"), Ok(GetType(Type(0.into()))));
- assert_eq!(parse_line("check Type 1"), Ok(GetType(Type(1.into()))))
+ assert_eq!(parse_line("check Type"), Ok(GetType(Sort(1.into()))));
+ assert_eq!(parse_line("check Type 0"), Ok(GetType(Sort(1.into()))));
+ assert_eq!(parse_line("check Type 1"), Ok(GetType(Sort(2.into()))))
}
#[test]
@@ -408,10 +497,13 @@ mod tests {
assert_eq!(
parse_line("check fun w x : Prop, y z : Prop => x"),
Ok(GetType(Abs(
- box Prop,
+ box Sort(0.into()),
box Abs(
- box Prop,
- box Abs(box Prop, box Abs(box Prop, box Var(3.into())))
+ box Sort(0.into()),
+ box Abs(
+ box Sort(0.into()),
+ box Abs(box Sort(0.into()), box Var(3.into()))
+ )
)
)))
)
@@ -440,7 +532,7 @@ mod tests {
assert_eq!(
parse_line("check fun x : Prop, x : x, x : x => x"),
Ok(GetType(Abs(
- box Prop,
+ box Sort(0.into()),
box Abs(
box Var(1.into()),
box Abs(box Var(1.into()), box Var(1.into()))
@@ -450,7 +542,7 @@ mod tests {
assert_eq!(
parse_line("check fun x : Prop, x x : x => x"),
Ok(GetType(Abs(
- box Prop,
+ box Sort(0.into()),
box Abs(
box Var(1.into()),
box Abs(box Var(1.into()), box Var(1.into()))
@@ -460,7 +552,7 @@ mod tests {
assert_eq!(
parse_line("check fun x : Prop, y z : x => z"),
Ok(GetType(Abs(
- box Prop,
+ box Sort(0.into()),
box Abs(
box Var(1.into()),
box Abs(box Var(2.into()), box Var(1.into()))
@@ -474,7 +566,7 @@ mod tests {
assert_eq!(
parse_line("check (x : Prop, x : x, x : x) -> x"),
Ok(GetType(Prod(
- box Prop,
+ box Sort(0.into()),
box Prod(
box Var(1.into()),
box Prod(box Var(1.into()), box Var(1.into()))
@@ -484,7 +576,7 @@ mod tests {
assert_eq!(
parse_line("check (x : Prop, x x : x) -> x"),
Ok(GetType(Prod(
- box Prop,
+ box Sort(0.into()),
box Prod(
box Var(1.into()),
box Prod(box Var(1.into()), box Var(1.into()))
@@ -494,7 +586,7 @@ mod tests {
assert_eq!(
parse_line("check (x : Prop, y z : x) -> z"),
Ok(GetType(Prod(
- box Prop,
+ box Sort(0.into()),
box Prod(
box Var(1.into()),
box Prod(box Var(2.into()), box Var(1.into()))
@@ -508,10 +600,13 @@ mod tests {
assert_eq!(
parse_line("check fun (((w x : Prop))), y z : Prop => x"),
Ok(GetType(Abs(
- box Prop,
+ box Sort(0.into()),
box Abs(
- box Prop,
- box Abs(box Prop, box Abs(box Prop, box Var(3.into())))
+ box Sort(0.into()),
+ box Abs(
+ box Sort(0.into()),
+ box Abs(box Sort(0.into()), box Var(3.into()))
+ )
)
)))
)
@@ -595,7 +690,7 @@ mod tests {
fn failed_parsers() {
assert_eq!(
parse_file(
- "def x : Type := Prop -> Prop
+ "def x : Type := Prop-> Prop
// this is a comment
check .x"
),
diff --git a/parser/src/term.pest b/parser/src/term.pest
index 6d44b2f6..b1efb680 100644
--- a/parser/src/term.pest
+++ b/parser/src/term.pest
@@ -1,15 +1,15 @@
WHITESPACE = _{ WHITE_SPACE }
COMMENT = _{ "//" ~ (!"\n" ~ ANY)* }
eoi = _{ !ANY }
-keywords = @{ ( "fun" | "def" | "check" | "Prop" | "Type" ) ~ !ASCII_ALPHANUMERIC }
+keywords = @{ ( "fun" | "def" | "check" | "Prop" | "Type" | "Sort" ) ~ !ASCII_ALPHANUMERIC }
number = @{ ASCII_DIGIT+ }
string = @{ !keywords ~ ASCII_ALPHA ~ ( "_" | ASCII_ALPHANUMERIC )* }
-Term = _{ Abs | dProd | Prod | App | Var | Prop | Type | "(" ~ Term ~ ")" }
-term_prod = _{ App | Abs | dProd | Var | Prop | Type | "(" ~ Prod ~ ")" | "(" ~ term_prod ~ ")" }
-term_app = _{ Abs | Var | Prop | Type | "(" ~ App ~ ")" | "(" ~ Prod ~ ")" | "(" ~ dProd ~ ")" | "(" ~ term_app ~ ")" }
-term_dprod = _{ App | Abs | Prod | dProd | Var | Prop | Type | "(" ~ term_dprod ~ ")" }
-term_abs = _{ App | Abs | Prod | dProd | Var | Prop | Type | "(" ~ term_abs ~ ")" }
+Term = _{ Abs | dProd | Prod | App | Var | Prop | Type | Sort | "(" ~ Term ~ ")" }
+term_prod = _{ App | Abs | dProd | Var | Prop | Type | Sort | "(" ~ Prod ~ ")" | "(" ~ term_prod ~ ")" }
+term_app = _{ Abs | Var | Prop | Type | Sort | "(" ~ App ~ ")" | "(" ~ Prod ~ ")" | "(" ~ dProd ~ ")" | "(" ~ term_app ~ ")" }
+term_dprod = _{ App | Abs | Prod | dProd | Var | Prop | Type | Sort | "(" ~ term_dprod ~ ")" }
+term_abs = _{ App | Abs | Prod | dProd | Var | Prop | Type | Sort | "(" ~ term_abs ~ ")" }
Abs = { ( "fun" ~ ( arg_abs_par ~ ( "," ~ arg_abs_par )* ) ~ "=>" ~ Term ) }
arg_abs_par = _{ arg_abs | "(" ~ arg_abs_par ~ ")" }
@@ -24,17 +24,22 @@ Prod = { term_prod ~ ( "->" ~ term_prod )+ }
Prop = { "Prop" }
Type = { "Type" ~ univ? }
-univ = _{ Plus | Max | Var | Num | "(" ~ univ ~ ")" }
-univ_plus = _{ Max | Var | Num | "(" ~ univ ~ ")" }
+Sort = { "Sort" ~ univ? }
+univ = _{ Plus | Max | Num | string | "(" ~ univ ~ ")" }
+univ_plus = _{ Max | Num | string | "(" ~ univ ~ ")" }
Num = { number }
Plus = { univ_plus ~ ( "+" ~ number )+ }
Max = { ( "max" ~ "(" ~ univ ~ "," ~ univ ~ ")" ) | ( "max" ~ univ ~ univ ) }
-Var = { string }
+
+Var = { string ~ arg_univ? }
+arg_univ = {".{" ~ (univ ~ ("," ~ univ)*)? ~ "}"}
+
+univ_decl = {".{" ~ (string ~ ("," ~ string)* )? ~ "}"}
Command = _{ Eval | Define | CheckType | GetType | DefineCheckType }
Eval = { "eval" ~ Term }
-Define = { "def" ~ string ~ ":=" ~ Term }
-DefineCheckType = { "def" ~ string ~ ":" ~ Term ~ ":=" ~ Term }
+Define = { "def" ~ string ~ univ_decl? ~ ":=" ~ Term }
+DefineCheckType = { "def" ~ string ~ univ_decl? ~ ":" ~ Term ~ ":=" ~ Term }
CheckType = { "check" ~ Term ~ ":" ~ Term }
GetType = { "check" ~ Term }
--
GitLab