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 (28)
Hide whitespace changes
Inline Side-by-side
Showing
with 1052 additions and 345 deletions
kernel/src/command.rs
View file @ e6983f21
......@@ -7,6 +7,8 @@ pub enum Command {
CheckType(Term, Term),
GetType(Term),
Eval(Term),
}
impl Command {
......@@ -15,37 +17,41 @@ impl Command {
match self {
Command::Define(s, None, term) => term
.infer(env)
.and_then(|t| env.insert(s, term, t).map(|_| None)),
.and_then(|t| env.insert_def(s, term, t).map(|_| None)),
Command::Define(s, Some(t), term) => term
.check(&t, env)
.and_then(|_| env.insert(s, term, t).map(|_| None)),
.and_then(|_| env.insert_def(s, term, t).map(|_| None)),
Command::CheckType(t1, t2) => t1.check(&t2, env).map(|_| None),
// This is only a temporary workaround. Once metavariables will be part of the system,
// there won't be any issue with checking/infering with a term with non-unified metavariables
Command::GetType(Term::Const(s, vec)) if vec.is_empty() => {
env.get_type_free_univ(&s).map(Some)
}
Command::GetType(t) => t.infer(env).map(Some),
Command::Eval(t) => Ok(Some(t.normal_form(env)?)),
}
}
}
#[cfg(test)]
mod tests {
use crate::{num_bigint::BigUint, Command, Environment, Term};
use crate::{Command, Environment, Term};
fn simple_env() -> Environment {
Environment::new()
.insert(
"x".to_string(),
Term::Type(BigUint::from(0_u64).into()),
Term::Prop,
)
.insert_def("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,29 +60,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(BigUint::from(0_u64).into())
)
.insert_def("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(BigUint::from(1_u64).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());
......@@ -85,29 +83,21 @@ mod tests {
#[test]
fn successful_typed_define() {
let cmd = Command::Define(
"y".to_string(),
Some(Term::Type(BigUint::from(0_u64).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(BigUint::from(0_u64).into())
)
.insert_def("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());
......@@ -116,7 +106,7 @@ mod tests {
#[test]
fn successful_checktype() {
let cmd = Command::CheckType(Term::Prop, Term::Type(BigUint::from(0_u64).into()));
let cmd = Command::CheckType(Term::PROP, Term::r#type(0.into()));
let mut env = simple_env();
assert!(cmd.process(&mut env).is_ok());
......@@ -125,7 +115,7 @@ mod tests {
#[test]
fn failed_gettype() {
let cmd = Command::GetType(Term::Const("y".to_string()));
let cmd = Command::GetType(Term::Const("y".to_string(), Vec::new()));
let mut env = simple_env();
assert!(cmd.process(&mut env).is_err());
......@@ -134,7 +124,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());
......
kernel/src/declaration.rs 0 → 100644
View file @ e6983f21
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 @ e6983f21
use crate::declaration::Declaration;
use crate::error::KernelError;
use crate::term::Term;
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, Eq, PartialEq, From)]
pub struct Environment(HashMap<String, (Term, Term)>);
#[derive(Clone, Default, Debug, From, PartialEq, Eq)]
pub struct Environment(HashMap<String, Declaration>);
impl Environment {
/// Creates an empty environment.
......@@ -13,23 +15,46 @@ impl Environment {
Self::default()
}
/// Creates a new environment binding s with (t1,t2)
pub fn insert(&mut self, s: String, t1: Term, t2: Term) -> Result<&Self, KernelError> {
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((t1, t2));
e.insert(decl);
Ok(self)
} else {
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 fn get_term(&self, s: &String) -> Option<Term> {
self.0.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 fn get_type(&self, s: &String) -> Option<Term> {
self.0.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 @ e6983f21
......@@ -28,7 +28,7 @@ impl Loc {
#[derive(Clone, Debug, Display, PartialEq, Eq)]
pub enum KernelError {
// cannot parse command
#[display(fmt = "cannot parse: {}", _1)]
#[display(fmt = "Cannot parse: {}", _1)]
CannotParse(Loc, String),
// s is already defined
......@@ -65,6 +65,13 @@ pub enum KernelError {
NotAFunction(Term, Term, Term),
/// Expected ty1, found ty2
#[display(fmt = "expected {}, found {}", _0, _1)]
#[display(fmt = "Expected {}, found {}", _0, _1)]
TypeMismatch(Term, Term),
#[display(
fmt = "Wrong number of universe arguments, expected {}, found {}",
_0,
_1
)]
WrongNumberOfUniverseArguments(usize, usize),
}
kernel/src/lib.rs
View file @ e6983f21
......@@ -4,15 +4,19 @@
#![feature(box_syntax)]
mod command;
mod declaration;
mod environment;
mod error;
mod term;
mod type_checker;
mod universe;
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;
pub use universe::UniverseLevel;
kernel/src/term.rs
View file @ e6983f21
use crate::environment::Environment;
use crate::universe::UniverseLevel;
use crate::KernelError;
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),
/// Constants can be universe polymorphic. As such, it is important to know what universes
/// they're assigned to. The vector serves to represent the universes by which the variables
/// present in the constant need to be substituted for.
#[display(fmt = "{}", _0)]
Const(String),
#[display(fmt = "Prop")]
Prop,
Const(String, Vec<UniverseLevel>),
#[display(fmt = "Type {}", _0)]
Type(UniverseLevel),
#[display(fmt = "Sort {}", _0)]
Sort(UniverseLevel),
#[display(fmt = "{} {}", _0, _1)]
App(Box<Term>, Box<Term>),
#[display(fmt = "\u{003BB} {} \u{02192} {}", _0, _1)]
#[display(fmt = "\u{003BB} ({}) \u{02192} {}", _0, _1)]
Abs(Box<Term>, Box<Term>),
#[display(fmt = "\u{03A0} {} \u{02192} {}", _0, _1)]
#[display(fmt = "\u{03A0} ({}) \u{02192} {}", _0, _1)]
Prod(Box<Term>, Box<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 {
pub fn beta_reduction(&self, env: &Environment) -> Result<Term, KernelError> {
//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()),
Abs(x, box t) => Abs(x.clone(), box t.beta_reduction(env)),
Const(s) => match env.get_term(s) {
Some(t) => t,
None => unreachable!(),
App(box Abs(_, box t1), box t2) => Ok(t1.substitute(t2, 1)),
App(box t1, box t2) => Ok(App(box t1.beta_reduction(env)?, box t2.clone())),
Abs(x, box t) => Ok(Abs(x.clone(), box t.beta_reduction(env)?)),
Const(s, vec) => match env.get_term(s, vec)? {
Some(t) => Ok(t),
None => Ok(self.clone()),
},
_ => self.clone(),
_ => Ok(self.clone()),
}
}
......@@ -75,55 +82,100 @@ 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.
pub fn normal_form(self, env: &Environment) -> Term {
let mut res = self.beta_reduction(env);
/// 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) -> Result<Term, KernelError> {
let mut res = self.beta_reduction(env)?;
let mut temp = self;
while res != temp {
temp = res.clone();
res = res.beta_reduction(env)
res = res.beta_reduction(env)?
}
res
Ok(res)
}
/// Returns the weak-head normal form of a term in a given environment.
pub fn whnf(&self, env: &Environment) -> Term {
pub fn whnf(&self, env: &Environment) -> Result<Term, KernelError> {
match self {
App(box t, t2) => match t.whnf(env) {
whnf @ Abs(_, _) => App(box whnf, t2.clone()).beta_reduction(env).whnf(env),
_ => self.clone(),
App(box t, t2) => match t.whnf(env)? {
whnf @ Abs(_, _) => App(box whnf, t2.clone()).beta_reduction(env)?.whnf(env),
_ => Ok(self.clone()),
},
Const(s) => match env.get_term(s) {
Some(t) => t,
None => unreachable!(),
Const(s, vec) => match env.get_term(s, vec)? {
Some(t) => Ok(t),
None => Ok(self.clone()),
},
_ => self.clone(),
_ => Ok(self.clone()),
}
}
pub fn univ_vars(&self) -> usize {
match self {
Var(_) => 0,
Const(..) => 0,
Sort(u) => u.clone().univ_vars(),
App(t1, t2) | Abs(t1, t2) | Prod(t1, t2) => t1.univ_vars().max(t2.univ_vars()),
}
}
pub fn substitute_univs(&self, vec: &[UniverseLevel]) -> Term {
match self {
Var(_) => self.clone(),
Const(..) => self.clone(),
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;
#[test]
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);
assert_eq!(term.beta_reduction(&Environment::new()).unwrap(), reduced);
}
#[test]
......@@ -131,19 +183,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())),
......@@ -151,34 +203,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())),
......@@ -186,26 +244,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())),
......@@ -215,101 +273,147 @@ 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();
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);
assert_eq!(term.beta_reduction(&env).unwrap(), term_step_1);
assert_eq!(term_step_1.beta_reduction(&env).unwrap(), term_step_2);
assert_eq!(term_step_2.beta_reduction(&env).unwrap(), term_step_3);
assert_eq!(term_step_3.beta_reduction(&env).unwrap(), term_step_4);
assert_eq!(term_step_4.beta_reduction(&env).unwrap(), term_step_5);
assert_eq!(term_step_5.beta_reduction(&env).unwrap(), term_step_6);
assert_eq!(term_step_6.beta_reduction(&env).unwrap(), term_step_7);
assert_eq!(term_step_7.beta_reduction(&env).unwrap(), term_step_7);
}
#[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)
assert_eq!(t2.beta_reduction(&Environment::new()).unwrap(), 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_def("foo".into(), id_prop.clone(), Sort(0.into()))
.unwrap();
assert_eq!(
Const("foo".into(), Vec::new())
.beta_reduction(&env)
.unwrap(),
id_prop
);
}
assert_eq!(Const("foo".into()).beta_reduction(&env), id_prop);
#[test]
fn poly_univ_id() {
let id_ty = Prod(
box Sort(UniverseLevel::Var(0)),
box Prod(box Var(1.into()), box Var(2.into())),
);
let id_te = Abs(
box Sort(UniverseLevel::Var(0)),
box Abs(box Var(1.into()), box Var(1.into())),
);
let id_zero = Abs(
box Sort(0.into()),
box Abs(box Var(1.into()), box Var(1.into())),
);
assert!(id_te.check(&id_ty, &Environment::new()).is_ok());
let mut binding = Environment::new();
let env = binding.insert_def("id".into(), id_te, id_ty).unwrap();
assert!(Const("id".into(), vec![0.into()])
.is_def_eq(&id_zero, env)
.is_ok())
}
}
kernel/src/type_checker.rs
View file @ e6983f21
use crate::environment::Environment;
use crate::error::KernelError;
use crate::term::{DeBruijnIndex, Term};
use num_bigint::BigUint;
use std::cmp::max;
use crate::universe::UniverseLevel;
use std::ops::Index;
use Term::*;
......@@ -45,19 +44,24 @@ impl Term {
/// 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, lvl: DeBruijnIndex) -> bool {
match (self.whnf(env), rhs.whnf(env)) {
(Type(i), Type(j)) => i == j,
fn conversion(
&self,
rhs: &Term,
env: &Environment,
lvl: DeBruijnIndex,
) -> Result<bool, KernelError> {
match (self.whnf(env)?, rhs.whnf(env)?) {
(lhs, rhs) if lhs == rhs => Ok(true),
(Prop, Prop) => true,
(Sort(i), Sort(j)) => Ok(i.is_eq(&j)),
(Var(i), Var(j)) => i == j,
(Var(i), Var(j)) => Ok(i == j),
(Prod(t1, u1), Prod(box t2, u2)) => {
let u1 = u1.substitute(&Var(lvl), lvl.into());
let u2 = u2.substitute(&Var(lvl), lvl.into());
t1.conversion(&t2, env, lvl) && u1.conversion(&u2, env, lvl + 1.into())
Ok(t1.conversion(&t2, env, lvl)? && u1.conversion(&u2, env, lvl + 1.into())?)
}
// Since we assume that both vals already have the same type,
......@@ -72,59 +76,45 @@ impl Term {
}
(App(box t1, box u1), App(box t2, box u2)) => {
t1.conversion(&t2, env, lvl) && u1.conversion(&u2, env, lvl)
Ok(t1.conversion(&t2, env, lvl)? && u1.conversion(&u2, env, lvl)?)
}
(app @ App(box Abs(_, _), box _), u) | (u, app @ App(box Abs(_, _), box _)) => {
app.beta_reduction(env).conversion(&u, env, lvl)
app.beta_reduction(env)?.conversion(&u, env, lvl)
}
_ => false,
_ => Ok(false),
}
}
/// Checks whether two terms are definitionally equal.
pub fn is_def_eq(&self, rhs: &Term, env: &Environment) -> Result<(), KernelError> {
self.conversion(rhs, env, 1.into())
self.conversion(rhs, env, 1.into())?
.then_some(())
.ok_or_else(|| KernelError::NotDefEq(self.clone(), rhs.clone()))
}
/// 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(max(i.clone(), 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(BigUint::from(0_u64).into())),
Type(i) => Ok(Type(i.clone() + BigUint::from(1_u64).into())),
Sort(i) => Ok(Sort(i.clone() + 1)),
Var(i) => Ok(ctx.types[ctx.lvl - *i].clone()),
Const(s) => match env.get_type(s) {
Some(ty) => Ok(ty),
None => Err(KernelError::ConstNotFound(s.clone())),
},
Const(s, vec) => env.get_type(s, vec),
Prod(box t, u) => {
let univ_t = t._infer(env, ctx)?;
let univ_u = u._infer(env, ctx.clone().bind(t))?;
univ_t.normal_form(env).imax(&univ_u.normal_form(env))
univ_t.normal_form(env)?.imax(&univ_u.normal_form(env)?)
}
Abs(box t, u) => {
......@@ -138,7 +128,7 @@ impl Term {
let typ_rhs = u._infer(env, ctx)?;
typ_lhs
.conversion(&typ_rhs, env, ctx.types.len().into())
.conversion(&typ_rhs, env, ctx.types.len().into())?
.then_some(*cls)
.ok_or_else(|| {
KernelError::WrongArgumentType(t.clone(), typ_lhs, u.clone(), typ_rhs)
......@@ -160,7 +150,7 @@ impl Term {
let ctx = &mut Context::new();
let tty = self._infer(env, ctx)?;
tty.conversion(ty, env, ctx.types.len().into())
tty.conversion(ty, env, ctx.types.len().into())?
.then_some(())
.ok_or_else(|| KernelError::TypeMismatch(tty, ty.clone()))
}
......@@ -171,44 +161,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()));
assert_eq!(t.normal_form(&Environment::new()), nf)
let nf = Abs(box Sort(0.into()), box Var(1.into()));
assert_eq!(t.normal_form(&Environment::new()).unwrap(), 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));
assert_eq!(t.normal_form(&Environment::new()), nf)
let nf = Abs(box Sort(0.into()), id(1));
assert_eq!(t.normal_form(&Environment::new()).unwrap(), nf)
}
#[test]
fn simple() {
let t1 = App(
box Abs(box Type(BigUint::from(0_u64).into()), box Var(1.into())),
box Prop,
box Abs(box Sort(1.into()), box Var(1.into())),
box Sort(0.into()),
);
let t2 = Prop;
assert!(t1.conversion(&t2, &Environment::new(), 0.into()));
let t2 = Sort(0.into());
assert!(t1.conversion(&t2, &Environment::new(), 0.into()).unwrap());
let ty = t1.infer(&Environment::new());
assert_eq!(ty, Ok(Type(BigUint::from(0_u64).into())));
assert_eq!(ty, Ok(Sort(1.into())));
}
#[test]
......@@ -216,15 +212,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());
}
......@@ -239,34 +241,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())),
......@@ -275,10 +283,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())),
),
),
),
......@@ -286,19 +294,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())
}
......@@ -307,9 +321,12 @@ 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());
let nff = reduced.clone().normal_form(&Environment::new()).unwrap();
assert_eq!(reduced, nff);
assert!(reduced.is_def_eq(&nff, &Environment::new()).is_ok());
}
......@@ -317,7 +334,7 @@ mod tests {
#[test]
fn polymorphism() {
let id = Abs(
box Type(BigUint::from(0_u64).into()),
box Sort(0.into()),
box Abs(box Var(1.into()), box Var(1.into())),
);
......@@ -326,48 +343,54 @@ mod tests {
#[test]
fn type_type() {
assert!(Type(BigUint::from(0_u64).into())
.check(&Type(BigUint::from(1_u64).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);
assert!(wf_prod
.check(&Type(BigUint::from(0_u64).into()), &Environment::new())
.is_ok());
let wf_prod = Prod(box Sort(0.into()), box Sort(0.into()));
println!("{:?}", wf_prod.infer(&Environment::new()));
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(BigUint::from(0_u64).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()),
......@@ -381,54 +404,77 @@ 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 mut env = Environment::new();
env.insert("foo".into(), id_prop.clone(), Prop).unwrap();
assert!(t.check(&Const("foo".into()), &env).is_ok());
assert!(id_prop.is_def_eq(&Const("foo".into()), &env).is_ok());
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_def("foo".into(), id_prop.clone(), Sort(0.into()))
.unwrap();
assert!(t.check(&Const("foo".into(), Vec::new()), env).is_ok());
assert!(id_prop
.is_def_eq(&Const("foo".into(), Vec::new()), env)
.is_ok());
}
#[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(BigUint::from(0_u64).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 mut env = Environment::new();
env.insert("foo".into(), id_prop, Prop).unwrap();
assert!(Const("foo".into()).infer(&env).is_ok());
assert!(Const("foo".into()).infer(&Environment::new()).is_err());
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_def("foo".into(), id_prop, Sort(0.into()))
.unwrap();
assert!(Const("foo".into(), Vec::new()).infer(env).is_ok());
assert!(Const("foo".into(), Vec::new())
.infer(&Environment::new())
.is_err());
}
#[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(BigUint::from(0_u64).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(BigUint::from(0_u64).into()),
&Environment::new(),
0.into()
))
assert!(ty
.conversion(&Sort(0.into()), &Environment::new(), 0.into())
.unwrap())
}
}
kernel/src/universe.rs 0 → 100644
View file @ e6983f21
use std::fmt::Display;
use std::fmt::Formatter;
use std::ops::Add;
#[derive(Clone, Debug, Default, PartialEq, Eq)]
pub enum UniverseLevel {
#[default]
Zero,
Succ(Box<UniverseLevel>),
Max(Box<UniverseLevel>, Box<UniverseLevel>),
IMax(Box<UniverseLevel>, Box<UniverseLevel>),
Var(usize),
}
impl Add<usize> for UniverseLevel {
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)
)
}
}
parser/src/parser.rs
View file @ e6983f21
use kernel::num_bigint::BigUint;
use kernel::{Command, KernelError, Loc, Term};
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>,
univ_var_map: &HashMap<String, usize>,
) -> UniverseLevel {
match pair.as_rule() {
Rule::Num => {
let n = pair.into_inner().as_str().parse().unwrap();
let mut univ = UniverseLevel::Zero;
for _ in 0..n {
univ = UniverseLevel::Succ(box univ);
}
univ
}
Rule::Max => {
let mut iter = pair.into_inner();
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(), 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),
}
}
/// convert pest locations to kernel locations
fn convert_span(span: Span) -> Loc {
let (x1, y1) = span.start_pos().line_col();
......@@ -16,26 +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::Type => Term::Type(pair.into_inner().fold(BigUint::from(0_u64).into(), |_, x| {
x.as_str().parse::<BigUint>().unwrap().into()
})),
Rule::Prop => Term::Sort(0.into()),
Rule::Type => match pair.into_inner().next() {
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),
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))
}
......@@ -47,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)
......@@ -65,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)
......@@ -80,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)
......@@ -101,28 +187,52 @@ 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(), &HashMap::new());
Command::Eval(t)
}
command => unreachable!("Unexpected command: {:?}", command),
}
}
......@@ -132,18 +242,27 @@ fn convert_error(err: Error<Rule>) -> KernelError {
// renaming error messages
let err = err.renamed_rules(|rule| match *rule {
Rule::string | Rule::Var => "variable".to_owned(),
Rule::number => "universe level".to_owned(),
Rule::number => "number".to_owned(),
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
......@@ -214,11 +333,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() {
......@@ -237,8 +358,8 @@ mod tests {
parse_line("def x : Type := Prop"),
Ok(Define(
"x".to_string(),
Some(Type(BigUint::from(0_u64).into())),
Prop
Some(Sort(1.into())),
Sort(0.into())
))
)
}
......@@ -247,7 +368,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())))
)
}
......@@ -255,38 +376,32 @@ mod tests {
fn successful_checktype() {
assert_eq!(
parse_line("check Prop : Type"),
Ok(CheckType(Prop, Type(BigUint::from(0_u64).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]
fn successful_var() {
assert_eq!(parse_line("check A"), Ok(GetType(Const("A".to_string()))));
assert_eq!(
parse_line("check A"),
Ok(GetType(Const("A".to_string(), Vec::new())))
);
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(BigUint::from(0_u64).into())))
);
assert_eq!(
parse_line("check Type 0"),
Ok(GetType(Type(BigUint::from(0_u64).into())))
);
assert_eq!(
parse_line("check Type 1"),
Ok(GetType(Type(BigUint::from(1_u64).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]
......@@ -294,22 +409,31 @@ mod tests {
assert_eq!(
parse_line("check A B C"),
Ok(GetType(App(
box App(box Const("A".to_string()), box Const("B".to_string())),
box Const("C".to_string())
box App(
box Const("A".to_string(), Vec::new()),
box Const("B".to_string(), Vec::new())
),
box Const("C".to_string(), Vec::new())
)))
);
assert_eq!(
parse_line("check (A B) C"),
Ok(GetType(App(
box App(box Const("A".to_string()), box Const("B".to_string())),
box Const("C".to_string())
box App(
box Const("A".to_string(), Vec::new()),
box Const("B".to_string(), Vec::new())
),
box Const("C".to_string(), Vec::new())
)))
);
assert_eq!(
parse_line("check A (B C)"),
Ok(GetType(App(
box Const("A".to_string()),
box App(box Const("B".to_string()), box Const("C".to_string()))
box Const("A".to_string(), Vec::new()),
box App(
box Const("B".to_string(), Vec::new()),
box Const("C".to_string(), Vec::new())
)
)))
)
}
......@@ -319,22 +443,31 @@ mod tests {
assert_eq!(
parse_line("check A -> B -> C"),
Ok(GetType(Prod(
box Const("A".to_string()),
box Prod(box Const("B".to_string()), box Const("C".to_string()))
box Const("A".to_string(), Vec::new()),
box Prod(
box Const("B".to_string(), Vec::new()),
box Const("C".to_string(), Vec::new())
)
)))
);
assert_eq!(
parse_line("check A -> (B -> C)"),
Ok(GetType(Prod(
box Const("A".to_string()),
box Prod(box Const("B".to_string()), box Const("C".to_string()))
box Const("A".to_string(), Vec::new()),
box Prod(
box Const("B".to_string(), Vec::new()),
box Const("C".to_string(), Vec::new())
)
)))
);
assert_eq!(
parse_line("check (A -> B) -> C"),
Ok(GetType(Prod(
box Prod(box Const("A".to_string()), box Const("B".to_string())),
box Const("C".to_string())
box Prod(
box Const("A".to_string(), Vec::new()),
box Const("B".to_string(), Vec::new())
),
box Const("C".to_string(), Vec::new())
)))
)
}
......@@ -344,15 +477,15 @@ mod tests {
assert_eq!(
parse_line("check (x:A) -> (y:B) -> x"),
Ok(GetType(Prod(
box Const("A".to_string()),
box Prod(box Const("B".to_string()), box Var(2.into()))
box Const("A".to_string(), Vec::new()),
box Prod(box Const("B".to_string(), Vec::new()), box Var(2.into()))
)))
);
assert_eq!(
parse_line("check (x:A) -> ((y:B) -> x)"),
Ok(GetType(Prod(
box Const("A".to_string()),
box Prod(box Const("B".to_string()), box Var(2.into()))
box Const("A".to_string(), Vec::new()),
box Prod(box Const("B".to_string(), Vec::new()), box Var(2.into()))
)))
)
}
......@@ -362,10 +495,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()))
)
)
)))
)
......@@ -394,7 +530,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()))
......@@ -404,7 +540,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()))
......@@ -414,7 +550,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()))
......@@ -428,7 +564,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()))
......@@ -438,7 +574,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()))
......@@ -448,7 +584,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()))
......@@ -462,10 +598,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()))
)
)
)))
)
......@@ -476,8 +615,11 @@ mod tests {
assert_eq!(
parse_line("check (((A))) -> (((B -> C)))"),
Ok(GetType(Prod(
box Const("A".to_string()),
box Prod(box Const("B".to_string()), box Const("C".to_string()))
box Const("A".to_string(), Vec::new()),
box Prod(
box Const("B".to_string(), Vec::new()),
box Const("C".to_string(), Vec::new())
)
)))
)
}
......@@ -487,8 +629,8 @@ mod tests {
assert_eq!(
parse_line("check (((x:A))) -> ((((y:B) -> x)))"),
Ok(GetType(Prod(
box Const("A".to_string()),
box Prod(box Const("B".to_string()), box Var(2.into()))
box Const("A".to_string(), Vec::new()),
box Prod(box Const("B".to_string(), Vec::new()), box Var(2.into()))
)))
)
}
......@@ -498,8 +640,11 @@ mod tests {
assert_eq!(
parse_line("check ((((((A))) (((B C))))))"),
Ok(GetType(App(
box Const("A".to_string()),
box App(box Const("B".to_string()), box Const("C".to_string()))
box Const("A".to_string(), Vec::new()),
box App(
box Const("B".to_string(), Vec::new()),
box Const("C".to_string(), Vec::new())
)
)))
)
}
......@@ -543,7 +688,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"
),
......
parser/src/term.pest
View file @ e6983f21
WHITESPACE = _{ WHITE_SPACE }
COMMENT = _{ "//" ~ (!"\n" ~ ANY)* }
eoi = _{ !ANY }
keywords = @{ ( "fun" | "def" | "check" | "Prop" | "Type" | "Sort" ) ~ !ASCII_ALPHANUMERIC }
number = @{ ASCII_DIGIT+ }
string = @{ !keywords ~ ASCII_ALPHA ~ ( "_" | ASCII_ALPHANUMERIC )* }
keywords = @{ ( "fun" | "def" | "check" | "Prop" | "Type" ) ~ !ASCII_ALPHANUMERIC }
eoi = _{ !ANY }
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 ~ ")" }
......@@ -21,14 +21,25 @@ arg_dprod = { string+ ~ ":" ~ term_dprod }
App = { term_app ~ term_app+ }
Prod = { term_prod ~ ( "->" ~ term_prod )+ }
Prop = { "Prop" }
Type = { "Type(" ~ number ~ ")" | "Type" ~ number? }
Var = { string }
Command = _{ Define | CheckType | GetType | DefineCheckType }
Define = { "def" ~ string ~ ":=" ~ Term }
DefineCheckType = { "def" ~ string ~ ":" ~ Term ~ ":=" ~ Term }
Type = { "Type" ~ 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 ~ arg_univ? }
arg_univ = {".{" ~ (univ ~ ("," ~ univ)*)? ~ "}"}
univ_decl = {".{" ~ (string ~ ("," ~ string)* )? ~ "}"}
Command = _{ Eval | Define | CheckType | GetType | DefineCheckType }
Eval = { "eval" ~ Term }
Define = { "def" ~ string ~ univ_decl? ~ ":=" ~ Term }
DefineCheckType = { "def" ~ string ~ univ_decl? ~ ":" ~ Term ~ ":=" ~ Term }
CheckType = { "check" ~ Term ~ ":" ~ Term }
GetType = { "check" ~ Term }
......