parser/Cargo.toml

@@ -9,6 +9,5 @@ license.workspace = true
 kernel.path = "../kernel"
 
 derive_more.workspace = true
-num-bigint.workspace = true
 pest.workspace = true
 pest_derive.workspace = true

parser/src/command.rs

@@ -4,15 +4,19 @@
 
 use core::fmt;
 
-use kernel::term::builders::Builder;
+use kernel::memory::declaration::builder as declaration;
+use kernel::memory::term::builder::Builder;
 
 /// The type of commands that can be received by the kernel.
 #[derive(Debug, Eq, PartialEq)]
 pub enum Command<'build> {
-    /// Define a new term and optionally check that it's type match the given one.
+    /// Define the given term
     Define(&'build str, Option<Builder<'build>>, Builder<'build>),
 
-    /// Infer the type of a term and check that it match the given one.
+    /// Define the given declaration
+    Declaration(&'build str, Option<declaration::Builder<'build>>, declaration::Builder<'build>),
+
+    /// Infer the type of a term and check that it matches the given one.
     CheckType(Builder<'build>, Builder<'build>),
 
     /// Infer the type of a term.
@@ -33,22 +37,26 @@ impl<'build> fmt::Display for Command<'build> {
         use Command::*;
 
         match self {
-            Define(name, None, t) => write!(f, "def {} := {}", name, t),
+            Define(name, None, t) => write!(f, "def {name} := {t}"),
+
+            Define(name, Some(ty), t) => write!(f, "def {name}: {ty} := {t}"),
+
+            Declaration(name, None, t) => write!(f, "def {name} := {t}"),
 
-            Define(name, Some(ty), t) => write!(f, "def {}: {} := {}", name, ty, t),
+            Declaration(name, Some(ty), t) => write!(f, "def {name}: {ty} := {t}"),
 
-            CheckType(t, ty) => write!(f, "check {}: {}", t, ty),
+            CheckType(t, ty) => write!(f, "check {t}: {ty}"),
 
-            GetType(t) => write!(f, "check {}", t),
+            GetType(t) => write!(f, "check {t}"),
 
-            Eval(t) => write!(f, "eval {}", t),
+            Eval(t) => write!(f, "eval {t}"),
 
             Import(files) => {
                 write!(f, "imports")?;
                 files.iter().try_for_each(|file| write!(f, " {file}"))
             },
 
-            Search(name) => write!(f, "search {}", name),
+            Search(name) => write!(f, "search {name}"),
         }
     }
 }

parser/src/parser.rs

 use kernel::location::Location;
-use kernel::term::builders::Builder;
+use kernel::memory::declaration::builder as declaration;
+use kernel::memory::level::builder as level;
+use kernel::memory::term::builder as term;
 use pest::error::LineColLocation;
 use pest::iterators::Pair;
 use pest::{Parser, Span};
 
 use crate::command::Command;
-use crate::error::{Error, ErrorKind};
+use crate::error;
 
 #[derive(Parser)]
 #[grammar = "term.pest"]
@@ -18,9 +20,52 @@ fn convert_span(span: Span) -> Location {
     ((x1, y1), (x2, y2)).into()
 }
 
+/// build universe level from errorless pest's output
+fn parse_level(pair: Pair<Rule>) -> level::Builder {
+    use level::Builder::*;
+
+    // location to be used in a future version
+    let _loc = convert_span(pair.as_span());
+
+    match pair.as_rule() {
+        Rule::Num => {
+            let n = pair.into_inner().as_str().parse().unwrap();
+            Const(n)
+        },
+
+        Rule::Max => {
+            let mut iter = pair.into_inner();
+            let univ1 = parse_level(iter.next().unwrap());
+            let univ2 = parse_level(iter.next().unwrap());
+            Max(box univ1, box univ2)
+        },
+
+        Rule::IMax => {
+            let mut iter = pair.into_inner();
+            let univ1 = parse_level(iter.next().unwrap());
+            let univ2 = parse_level(iter.next().unwrap());
+            IMax(box univ1, box univ2)
+        },
+
+        Rule::Plus => {
+            let mut iter = pair.into_inner();
+            let univ = parse_level(iter.next().unwrap());
+            let n = iter.map(|x| x.as_str().parse::<usize>().unwrap()).sum();
+            Plus(box univ, n)
+        },
+
+        Rule::string => {
+            let name = pair.as_str();
+            Var(name)
+        },
+
+        univ => unreachable!("unexpected universe level: {univ:?}"),
+    }
+}
+
 /// Returns a kernel term builder from pest output
-fn parse_term(pair: Pair<Rule>) -> Builder {
-    use Builder::*;
+fn parse_term(pair: Pair<Rule>) -> term::Builder {
+    use term::Builder::*;
 
     // location to be used in a future version
     let _loc = convert_span(pair.as_span());
@@ -30,12 +75,33 @@ fn parse_term(pair: Pair<Rule>) -> Builder {
 
         Rule::Var => Var(pair.into_inner().as_str()),
 
-        Rule::Type => Type(pair.into_inner().fold(0, |_, x| x.as_str().parse::<usize>().unwrap())),
+        Rule::VarDecl => {
+            let mut iter = pair.into_inner();
+            let name = iter.next().unwrap().as_str();
+            let levels = iter.next().unwrap().into_inner().map(parse_level).collect();
+            Decl(box declaration::InstantiatedBuilder::Var(name, levels))
+        },
+
+        Rule::Type => {
+            if let Some(next) = pair.into_inner().next_back() {
+                Type(box parse_level(next))
+            } else {
+                Type(box level::Builder::Const(0))
+            }
+        },
+
+        Rule::Sort => {
+            if let Some(next) = pair.into_inner().next_back() {
+                Sort(box parse_level(next))
+            } else {
+                Sort(box level::Builder::Const(0))
+            }
+        },
 
         Rule::App => {
             let mut iter = pair.into_inner().map(parse_term);
             let t = iter.next().unwrap();
-            iter.fold(t, |acc, x| App(Box::new(acc), Box::new(x)))
+            iter.fold(t, |acc, x| App(box acc, box x))
         },
 
         Rule::Abs => {
@@ -43,11 +109,11 @@ fn parse_term(pair: Pair<Rule>) -> Builder {
             let body = parse_term(iter.next_back().unwrap());
             iter.flat_map(|pair| {
                 let mut pair = pair.into_inner();
-                let type_ = Box::new(parse_term(pair.next_back().unwrap()));
+                let type_ = box parse_term(pair.next_back().unwrap());
                 pair.map(move |var| (var.as_str(), type_.clone()))
             })
             .rev()
-            .fold(body, |acc, (var, type_)| Abs(var, type_, Box::new(acc)))
+            .fold(body, |acc, (var, type_)| Abs(var, type_, box acc))
         },
 
         Rule::dProd => {
@@ -55,25 +121,25 @@ fn parse_term(pair: Pair<Rule>) -> Builder {
             let body = parse_term(iter.next_back().unwrap());
             iter.flat_map(|pair| {
                 let mut pair = pair.into_inner();
-                let type_ = Box::new(parse_term(pair.next_back().unwrap()));
+                let type_ = box parse_term(pair.next_back().unwrap());
                 pair.map(move |var| (var.as_str(), type_.clone()))
             })
             .rev()
-            .fold(body, |acc, (var, type_)| Prod(var, type_, Box::new(acc)))
+            .fold(body, |acc, (var, type_)| Prod(var, type_, box acc))
         },
 
         Rule::Prod => {
             let mut iter = pair.into_inner();
             let ret = parse_term(iter.next_back().unwrap());
-            iter.map(parse_term).rev().fold(ret, |acc, argtype| Prod("_", Box::new(argtype), Box::new(acc)))
+            iter.map(parse_term).rev().fold(ret, |acc, argtype| Prod("_", box argtype, box acc))
         },
 
-        term => unreachable!("Unexpected term: {:?}", term),
+        term => unreachable!("unexpected term: {term:?}"),
     }
 }
 
 /// build commands from errorless pest's output
-fn parse_expr<'build>(pair: Pair<'build, Rule>) -> Command<'build> {
+fn parse_expr(pair: Pair<Rule>) -> Command {
     // location to be used in a future version
     let _loc = convert_span(pair.as_span());
 
@@ -93,17 +159,42 @@ fn parse_expr<'build>(pair: Pair<'build, Rule>) -> Command<'build> {
 
         Rule::Define => {
             let mut iter = pair.into_inner();
-            let s: &'build str = iter.next().unwrap().as_str();
+            let s = iter.next().unwrap().as_str();
             let term = parse_term(iter.next().unwrap());
             Command::Define(s, None, term)
         },
 
         Rule::DefineCheckType => {
             let mut iter = pair.into_inner();
-            let s: &'build str = iter.next().unwrap().as_str();
-            let t = parse_term(iter.next().unwrap());
+            let s = iter.next().unwrap().as_str();
+            let ty = parse_term(iter.next().unwrap());
             let term = parse_term(iter.next().unwrap());
-            Command::Define(s, Some(t), term)
+
+            Command::Define(s, Some(ty), term)
+        },
+
+        Rule::Declaration => {
+            let mut iter = pair.into_inner();
+            let mut string_decl = iter.next().unwrap().into_inner();
+            let s = string_decl.next().unwrap().as_str();
+            let vars: Vec<&str> = string_decl.next().unwrap().into_inner().map(|name| name.as_str()).collect();
+            let body = iter.next().map(parse_term).unwrap();
+
+            Command::Declaration(s, None, declaration::Builder::Decl(box body, vars))
+        },
+
+        Rule::DeclarationCheckType => {
+            let mut iter = pair.into_inner();
+            let mut string_decl = iter.next().unwrap().into_inner();
+            let s = string_decl.next().unwrap().as_str();
+            let vars: Vec<&str> = string_decl.next().unwrap().into_inner().map(|name| name.as_str()).collect();
+
+            let ty = parse_term(iter.next().unwrap());
+            let decl = iter.next().map(parse_term).unwrap();
+
+            let ty = declaration::Builder::Decl(box ty, vars.clone());
+            let decl = declaration::Builder::Decl(box decl, vars);
+            Command::Declaration(s, Some(ty), decl)
         },
 
         Rule::Eval => {
@@ -126,12 +217,14 @@ fn parse_expr<'build>(pair: Pair<'build, Rule>) -> Command<'build> {
 }
 
 /// convert pest error to kernel error
-fn convert_error(err: pest::error::Error<Rule>) -> Error {
+fn convert_error(err: pest::error::Error<Rule>) -> error::Error {
     // 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::Declaration => "def decl.{ vars, ... } := term".to_owned(),
+        Rule::DeclarationCheckType => "def decl.{ vars, ... } : term := term".to_owned(),
         Rule::CheckType => "check term : term".to_owned(),
         Rule::GetType => "check term".to_owned(),
         Rule::DefineCheckType => "def var : term := term".to_owned(),
@@ -141,11 +234,19 @@ fn convert_error(err: pest::error::Error<Rule>) -> Error {
         Rule::App => "application".to_owned(),
         Rule::Prop => "Prop".to_owned(),
         Rule::Type => "Type".to_owned(),
+        Rule::Sort => "Sort".to_owned(),
         Rule::Eval => "eval term".to_owned(),
         Rule::filename => "path_to_file".to_owned(),
         Rule::ImportFile => "import path_to_file".to_owned(),
         Rule::Search => "search var".to_owned(),
-        _ => unreachable!("low level rules cannot appear in error messages"),
+        Rule::Max => "max".to_owned(),
+        Rule::Plus => "plus".to_owned(),
+        Rule::IMax => "imax".to_owned(),
+        Rule::arg_univ => "universe argument".to_owned(),
+        Rule::univ_decl => "universe declaration".to_owned(),
+        _ => {
+            unreachable!("low level rules cannot appear in error messages")
+        },
     });
 
     // extracting the location from the pest output
@@ -183,8 +284,8 @@ fn convert_error(err: pest::error::Error<Rule>) -> Error {
     for _ in 0..4 {
         chars.next();
     }
-    Error {
-        kind: ErrorKind::CannotParse(chars.as_str().to_string()),
+    error::Error {
+        kind: error::ErrorKind::CannotParse(chars.as_str().to_string()),
         location: loc,
     }
 }
@@ -192,30 +293,32 @@ fn convert_error(err: pest::error::Error<Rule>) -> Error {
 /// Parse a text input and try to convert it into a command.
 ///
 /// if unsuccessful, a box containing the first error that was encountered is returned.
-pub fn parse_line(line: &str) -> crate::error::Result<Command> {
+pub fn parse_line(line: &str) -> error::Result<Command> {
     CommandParser::parse(Rule::command, line).map_err(convert_error).map(|mut pairs| parse_expr(pairs.next().unwrap()))
 }
 
 /// Parse a text input and try to convert it into a vector of commands.
 ///
 /// if unsuccessful, a box containing the first error that was encountered is returned.
-pub fn parse_file(file: &str) -> crate::error::Result<Vec<Command>> {
+pub fn parse_file(file: &str) -> error::Result<Vec<Command>> {
     CommandParser::parse(Rule::file, file).map_err(convert_error).map(|pairs| pairs.into_iter().map(parse_expr).collect())
 }
 
 #[cfg(test)]
 mod tests {
-    use kernel::term::builders::*;
-    use Builder::*;
+
+    use error::{Error, ErrorKind};
+    use kernel::memory::term::builder as term;
+    use term::Builder::*;
 
     use super::Command::*;
     use super::*;
 
     /// Error messages
-    const COMMAND_ERR: &str = "expected def var := term, def var : term := term, check term : term, check term, eval term, import path_to_file, or search var";
-    const TERM_ERR: &str = "expected variable, abstraction, dependent product, application, product, Prop, 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";
+    const COMMAND_ERR: &str = "expected def var := term, def var : term := term, def decl.{ vars, ... } := term, def decl.{ vars, ... } : term := term, check term : term, check term, eval term, import path_to_file, or search var";
+    const TERM_ERR: &str = "expected variable, abstraction, dependent product, application, product, Prop, Type, or Sort";
+    const SIMPLE_TERM_ERR: &str = "expected variable, abstraction, Prop, Type, Sort, or universe argument";
+    const UNIVERSE_ERR: &str = "expected number, variable, abstraction, Prop, Type, Sort, plus, max, or imax";
 
     #[test]
     fn failure_universe_level() {
@@ -230,7 +333,25 @@ mod tests {
 
     #[test]
     fn successful_define_with_type_annotation() {
-        assert_eq!(parse_line("def x : Type := Prop"), Ok(Define("x", Some(Type(0)), Prop)));
+        assert_eq!(parse_line("def x : Type := Prop"), Ok(Define("x", Some(Type(box level::Builder::Const(0))), Prop)));
+    }
+
+    #[test]
+    fn successful_declare_with_type_annotation() {
+        assert_eq!(
+            parse_line("def x.{u} : Type u := foo.{u}"),
+            Ok(Declaration(
+                "x",
+                Some(declaration::Builder::Decl(box Type(box level::Builder::Var("u")), ["u"].to_vec())),
+                declaration::Builder::Decl(
+                    box kernel::memory::term::builder::Builder::Decl(box declaration::InstantiatedBuilder::Var(
+                        "foo",
+                        [level::Builder::Var("u")].to_vec()
+                    )),
+                    ["u"].to_vec()
+                )
+            ))
+        );
     }
 
     #[test]
@@ -254,9 +375,14 @@ mod tests {
         assert_eq!(parse_line("def x := Prop"), Ok(Define("x", None, Prop)));
     }
 
+    #[test]
+    fn successful_declare() {
+        assert_eq!(parse_line("def x.{} := Prop"), Ok(Declaration("x", None, declaration::Builder::Decl(box Prop, Vec::new()))));
+    }
+
     #[test]
     fn successful_checktype() {
-        assert_eq!(parse_line("check Prop : Type"), Ok(CheckType(Prop, Type(0))));
+        assert_eq!(parse_line("check Prop : Type"), Ok(CheckType(Prop, Type(box level::Builder::Const(0)))));
     }
 
     #[test]
@@ -264,6 +390,11 @@ mod tests {
         assert_eq!(parse_line("check Prop"), Ok(GetType(Prop)));
     }
 
+    #[test]
+    fn successful_gettype_sort() {
+        assert_eq!(parse_line("check Sort"), Ok(GetType(Sort(box level::Builder::Const(0)))));
+    }
+
     #[test]
     fn successful_var() {
         assert_eq!(parse_line("check fun A: Prop => A"), Ok(GetType(Abs("A", Box::new(Prop), Box::new(Var("A"))))));
@@ -271,9 +402,25 @@ mod tests {
 
     #[test]
     fn successful_type() {
-        assert_eq!(parse_line("check Type"), Ok(GetType(Type(0))));
-        assert_eq!(parse_line("check Type 0"), Ok(GetType(Type(0))));
-        assert_eq!(parse_line("check Type 1"), Ok(GetType(Type(1))));
+        assert_eq!(parse_line("check Type"), Ok(GetType(Type(box level::Builder::Const(0)))));
+        assert_eq!(parse_line("check Type 0"), Ok(GetType(Type(box level::Builder::Const(0)))));
+        assert_eq!(parse_line("check Type 1"), Ok(GetType(Type(box level::Builder::Const(1)))));
+    }
+
+    #[test]
+    fn successful_sort() {
+        assert_eq!(parse_line("check Sort"), Ok(GetType(Sort(box level::Builder::Const(0)))));
+        assert_eq!(parse_line("check Sort 0"), Ok(GetType(Sort(box level::Builder::Const(0)))));
+        assert_eq!(parse_line("check Sort 1"), Ok(GetType(Sort(box level::Builder::Const(1)))));
+        assert_eq!(parse_line("check Sort (0 + 1)"), Ok(GetType(Sort(box level::Builder::Plus(box level::Builder::Const(0), 1)))));
+        assert_eq!(
+            parse_line("check Sort max 0 0"),
+            Ok(GetType(Sort(box level::Builder::Max(box level::Builder::Const(0), box level::Builder::Const(0)))))
+        );
+        assert_eq!(
+            parse_line("check Sort imax 0 0"),
+            Ok(GetType(Sort(box level::Builder::IMax(box level::Builder::Const(0), box level::Builder::Const(0)))))
+        );
     }
 
     #[test]
@@ -296,7 +443,11 @@ mod tests {
 
     #[test]
     fn successful_dprod() {
-        let res = Ok(GetType(Prod("x", Box::new(Type(0)), Box::new(Prod("y", Box::new(Type(1)), Box::new(Var("x")))))));
+        let res = Ok(GetType(Prod(
+            "x",
+            Box::new(Type(box level::Builder::Const(0))),
+            Box::new(Prod("y", Box::new(Type(box level::Builder::Const(1))), Box::new(Var("x")))),
+        )));
         assert_eq!(parse_line("check (x:Type) -> (y:Type 1) -> x"), res);
         assert_eq!(parse_line("check (x:Type) -> ((y:Type 1) -> x)"), res);
     }
@@ -383,13 +534,21 @@ mod tests {
 
     #[test]
     fn parenthesis_in_prod() {
-        let res = Prod("_", Box::new(Type(0)), Box::new(Prod("_", Box::new(Type(1)), Box::new(Type(2)))));
+        let res = Prod(
+            "_",
+            Box::new(Type(box level::Builder::Const(0))),
+            Box::new(Prod("_", Box::new(Type(box level::Builder::Const(1))), Box::new(Type(box level::Builder::Const(2))))),
+        );
         assert_eq!(parse_line("check (((Type))) -> (((Type 1 -> Type 2)))"), Ok(GetType(res)));
     }
 
     #[test]
     fn parenthesis_in_dprod() {
-        let res = Prod("x", Box::new(Type(0)), Box::new(Prod("y", Box::new(Type(1)), Box::new(Var("x")))));
+        let res = Prod(
+            "x",
+            Box::new(Type(box level::Builder::Const(0))),
+            Box::new(Prod("y", Box::new(Type(box level::Builder::Const(1))), Box::new(Var("x")))),
+        );
         assert_eq!(parse_line("check (((x:Type))) -> ((((y:Type 1) -> x)))"), Ok(GetType(res)));
     }
 

parser/src/term.pest

@@ -3,14 +3,16 @@ COMMENT = _{ "//" ~ (!"\n" ~ ANY)* }
 number = @{ ASCII_DIGIT+ }
 filename = @{ ( ASCII_ALPHANUMERIC | PUNCTUATION )+ }
 string = @{ !keywords ~ ASCII_ALPHA ~ ( "_" | ASCII_ALPHANUMERIC )* }
-keywords = @{ ( "fun" | "def" | "check" | "Prop" | "Type" ) ~ !ASCII_ALPHANUMERIC }
+keywords = @{ ( "fun" | "def" | "check" | "Prop" | "Type" | "Sort" ) ~ !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 | VarDecl | Var | Prop | Type | Sort | "(" ~ Term ~ ")" }
+term_prod = _{ App | Abs | dProd | VarDecl | Var | Prop | Type | Sort | "(" ~ Prod ~ ")" | "(" ~ term_prod ~ ")" }
+term_app = _{ Abs | VarDecl | Var | Prop | Type | Sort | "(" ~ App ~ ")" | "(" ~ Prod ~ ")" | "(" ~ dProd ~ ")" | "(" ~ term_app ~ ")" } 
+term_dprod = _{ App | Abs | Prod | dProd | VarDecl | Var | Prop | Type | Sort | "(" ~ term_dprod ~ ")" }
+term_abs = _{ App | Abs | Prod | dProd | VarDecl | Var | Prop | Type | Sort | "(" ~ term_abs ~ ")" }
 
 Abs = { ( "fun" ~ ( arg_abs_par ~ ( "," ~ arg_abs_par )* ) ~ "=>" ~ Term ) }
 arg_abs_par = _{ arg_abs | "(" ~ arg_abs_par ~ ")" }
@@ -22,19 +24,33 @@ arg_dprod = { string+ ~ ":" ~ term_dprod }
 
 App = { term_app ~ term_app+ }
 Prod = { term_prod ~ ( "->" ~ term_prod )+ }
-
 Prop = { "Prop" }
-Type = { "Type(" ~ number ~ ")" | "Type" ~ number? }
+
+Type = { "Type" ~ univ? }
+Sort = { "Sort" ~ univ? }
+univ = _{ Plus | Max | IMax | Num | string | "(" ~ univ ~ ")" }
+univ_plus = _{ Max | IMax | Num | string | "(" ~ univ ~ ")" }
+Num = { number }
+Plus = { univ_plus ~ ( "+" ~ number )+ }
+Max = { ( "max" ~ "(" ~ univ ~ "," ~ univ ~ ")" ) | ( "max" ~ univ ~ univ ) }
+IMax = { ( "imax" ~ "(" ~ univ ~ "," ~ univ ~ ")" ) | ( "imax" ~ univ ~ univ ) }
+
 Var = { string }
+VarDecl = ${ string ~ arg_univ }
+stringDecl = ${ string ~ univ_decl }
+
+arg_univ = {".{" ~ (univ ~ ("," ~ univ)* )? ~ "}"}
+univ_decl = {".{" ~ (string ~ ("," ~ string)* )? ~ "}"}
 
-Command = _{ Define | CheckType | GetType | DefineCheckType | Eval | ImportFile | Search}
+Command = _{ Define | Declaration | DeclarationCheckType | CheckType | GetType | DefineCheckType | Eval | ImportFile | Search}
 Define = { "def" ~ string ~ ":=" ~ Term }
 DefineCheckType = { "def" ~ string ~ ":" ~ Term ~ ":=" ~ Term }
+Declaration = { "def" ~ stringDecl ~ ":=" ~ Term }
+DeclarationCheckType = { "def" ~ stringDecl ~ ":" ~ Term ~ ":=" ~ Term }
 CheckType = { "check" ~ Term ~ ":" ~ Term }
 GetType = { "check" ~ Term }
 Eval = { "eval" ~ Term }
 ImportFile = { "import" ~ filename* }
 Search = { "search" ~ string }
-
 command = _{SOI ~ Command ~ eoi }
 file = _{ SOI ~ Command* ~ eoi }

proost/src/evaluator.rs

@@ -5,7 +5,8 @@ use std::path::PathBuf;
 use colored::Colorize;
 use derive_more::Display;
 use kernel::location::Location;
-use kernel::term::arena::{Arena, Term};
+use kernel::memory::arena::Arena;
+use kernel::memory::term::Term;
 use parser::command::Command;
 use parser::{parse_file, parse_line};
 use path_absolutize::Absolutize;
@@ -131,50 +132,65 @@ impl<'arena> Evaluator {
             .map(|_| None)
     }
 
-    fn process<'build>(
+    fn process(
         &mut self,
         arena: &mut Arena<'arena>,
-        command: &Command<'build>,
+        command: &Command,
         importing: &mut Vec<PathBuf>,
     ) -> Result<'arena, Option<Term<'arena>>> {
         match command {
-            Command::Define(s, None, term) => {
-                let term = term.realise(arena)?;
-                if arena.get_binding(s).is_none() {
-                    arena.infer(term)?;
-                    arena.bind(s, term);
-                    Ok(None)
-                } else {
-                    Err(Toplevel(Error {
+            Command::Define(s, ty, term) => {
+                if arena.get_binding(s).is_some() {
+                    return Err(Toplevel(Error {
                         kind: ErrorKind::BoundVariable(s.to_string()),
                         location: Location::default(), // TODO (see #38)
-                    }))
+                    }));
                 }
-            },
-
-            Command::Define(s, Some(t), term) => {
                 let term = term.realise(arena)?;
-                let t = t.realise(arena)?;
-                arena.check(term, t)?;
+                match ty {
+                    None => {
+                        term.infer(arena)?;
+                    },
+                    Some(ty) => term.check(ty.realise(arena)?, arena)?,
+                }
                 arena.bind(s, term);
                 Ok(None)
             },
 
+            Command::Declaration(s, ty, decl) => {
+                if arena.get_binding_decl(s).is_some() {
+                    return Err(Toplevel(Error {
+                        kind: ErrorKind::BoundVariable(s.to_string()),
+                        location: Location::default(), // TODO (see #38)
+                    }));
+                }
+                let decl = decl.realise(arena)?;
+                match ty {
+                    None => {
+                        decl.infer(arena)?;
+                    },
+                    Some(ty) => decl.check(ty.realise(arena)?, arena)?,
+                }
+                arena.bind_decl(s, decl);
+                Ok(None)
+            },
+
             Command::CheckType(t1, t2) => {
                 let t1 = t1.realise(arena)?;
                 let t2 = t2.realise(arena)?;
-                arena.check(t1, t2)?;
+                t1.check(t2, arena)?;
                 Ok(None)
             },
 
             Command::GetType(t) => {
                 let t = t.realise(arena)?;
-                Ok(arena.infer(t).map(Some)?)
+                Ok(t.infer(arena).map(Some)?)
             },
 
             Command::Eval(t) => {
                 let t = t.realise(arena)?;
-                Ok(Some(arena.normal_form(t)))
+                let _ = t.infer(arena)?;
+                Ok(Some(t.normal_form(arena)))
             },
 
             Command::Search(s) => Ok(arena.get_binding(s)), // TODO (see #49)

proost/src/main.rs

@@ -53,7 +53,7 @@ fn main() -> Result<'static, ()> {
     rl.bind_sequence(KeyEvent::from('\t'), EventHandler::Conditional(Box::new(TabEventHandler)));
     rl.bind_sequence(KeyEvent(KeyCode::Enter, Modifiers::ALT), EventHandler::Simple(Cmd::Newline));
 
-    kernel::term::arena::use_arena(|arena| {
+    kernel::memory::arena::use_arena(|arena| {
         let current_path = current_dir()?;
         let mut evaluator = Evaluator::new(current_path, args.verbose);