diff --git a/parser/src/command.rs b/parser/src/command.rs
index e9055821de763209aa6b950fba3bc35f9f3314c9..64017f083256704196734cecee459f0a192008e4 100644
--- a/parser/src/command.rs
+++ b/parser/src/command.rs
@@ -10,9 +10,6 @@ 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 its type matches the given one.
- Define(&'build str, Option<Builder<'build>>, Builder<'build>),
-
/// Define the given declaration
Declaration(&'build str, Option<declaration::Builder<'build>>, declaration::Builder<'build>),
@@ -37,10 +34,6 @@ impl<'build> fmt::Display for Command<'build> {
use Command::*;
match self {
- 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}"),
Declaration(name, Some(ty), t) => write!(f, "def {name}: {ty} := {t}"),
diff --git a/parser/src/parser.rs b/parser/src/parser.rs
index 12186bcd2d3679d96f4296012043c1d4de31c68c..11f2b4dfa80f3f28c7484296f7cd285c1cf983b5 100644
--- a/parser/src/parser.rs
+++ b/parser/src/parser.rs
@@ -161,22 +161,26 @@ fn parse_expr(pair: Pair<Rule>) -> Command {
let mut iter = pair.into_inner();
let s = iter.next().unwrap().as_str();
let term = parse_term(iter.next().unwrap());
- Command::Define(s, None, term)
+ Command::Declaration(s, None, declaration::Builder::Decl(box term, Vec::new()))
},
Rule::DefineCheckType => {
let mut iter = pair.into_inner();
let s = iter.next().unwrap().as_str();
- let t = parse_term(iter.next().unwrap());
- let term = parse_term(iter.next().unwrap());
- Command::Define(s, Some(t), term)
+ let ty = parse_term(iter.next().unwrap());
+ let decl = parse_term(iter.next().unwrap());
+
+ let ty = declaration::Builder::Decl(box ty, Vec::new());
+ let decl = declaration::Builder::Decl(box decl, Vec::new());
+
+ Command::Declaration(s, Some(ty), decl)
},
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 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))
@@ -186,13 +190,13 @@ fn parse_expr(pair: Pair<Rule>) -> Command {
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 t = parse_term(iter.next().unwrap());
- let body = iter.next().map(parse_term).unwrap();
+ 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 t, vars.clone());
- let decl = declaration::Builder::Decl(box body, vars);
+ let ty = declaration::Builder::Decl(box ty, vars.clone());
+ let decl = declaration::Builder::Decl(box decl, vars);
Command::Declaration(s, Some(ty), decl)
},
@@ -335,7 +339,14 @@ mod tests {
#[test]
fn successful_define_with_type_annotation() {
- assert_eq!(parse_line("def x : Type := Prop"), Ok(Define("x", Some(Type(box level::Builder::Const(0))), Prop)));
+ assert_eq!(
+ parse_line("def x : Type := Prop"),
+ Ok(Declaration(
+ "x",
+ Some(declaration::Builder::Decl(box Type(box level::Builder::Const(0)), Vec::new())),
+ declaration::Builder::Decl(box Prop, Vec::new())
+ ))
+ );
}
#[test]
@@ -356,7 +367,7 @@ mod tests {
#[test]
fn successful_define() {
- assert_eq!(parse_line("def x := Prop"), Ok(Define("x", None, Prop)));
+ assert_eq!(parse_line("def x := Prop"), Ok(Declaration("x", None, declaration::Builder::Decl(box Prop, Vec::new()))));
}
#[test]
diff --git a/proost/src/evaluator.rs b/proost/src/evaluator.rs
index a5e49ffeccf4111e2cc193d4e5caa18ae15ef378..38947a6789c2cc96082048f42e7f030649054343 100644
--- a/proost/src/evaluator.rs
+++ b/proost/src/evaluator.rs
@@ -139,35 +139,6 @@ impl<'arena> Evaluator {
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() {
- term.infer(arena)?;
- arena.bind(s, term);
- Ok(None)
- } else {
- 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)?;
- if arena.get_binding(s).is_none() {
- term.check(t, arena)?;
- arena.bind(s, term);
- Ok(None)
- } else {
- Err(Toplevel(Error {
- kind: ErrorKind::BoundVariable(s.to_string()),
- location: Location::default(), // TODO (see #38)
- }))
- }
- },
-
Command::Declaration(s, None, decl) => {
let decl = decl.realise(arena)?;
if arena.get_binding(s).is_none() {
@@ -186,7 +157,7 @@ impl<'arena> Evaluator {
let decl = decl.realise(arena)?;
let ty = t.realise(arena)?;
if arena.get_binding(s).is_none() {
- decl.check(ty,arena)?;
+ decl.check(ty, arena)?;
arena.bind_decl(s, decl);
Ok(None)
} else {