diff --git a/parser/src/command/mod.rs b/parser/src/command/mod.rs
index dd6d6f65016bd10707cc1aae3391a86fa6ee205d..afd0d5556af65dd14c53ba03fb4e31bba0688b76 100644
--- a/parser/src/command/mod.rs
+++ b/parser/src/command/mod.rs
@@ -8,15 +8,16 @@ use core::fmt;
use kernel::memory::declaration::builder as declaration;
use kernel::memory::term::builder::Builder;
+use utils::location::Location;
/// The type of commands that can be received by the kernel.
#[derive(Debug, Eq, PartialEq)]
pub enum Command<'build> {
/// Define the given term
- Define(&'build str, Option<Builder<'build>>, Builder<'build>),
+ Define((Location, &'build str), Option<Builder<'build>>, Builder<'build>),
/// Define the given declaration
- Declaration(&'build str, Option<declaration::Builder<'build>>, declaration::Builder<'build>),
+ Declaration((Location, &'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>),
@@ -40,13 +41,13 @@ impl<'build> fmt::Display for Command<'build> {
use Command::{CheckType, Declaration, Define, Eval, GetType, Import, Search};
match *self {
- Define(name, None, ref t) => write!(f, "def {name} := {t}"),
+ Define((_, name), None, ref t) => write!(f, "def {name} := {t}"),
- Define(name, Some(ref ty), ref t) => write!(f, "def {name}: {ty} := {t}"),
+ Define((_, name), Some(ref ty), ref t) => write!(f, "def {name}: {ty} := {t}"),
- Declaration(name, None, ref t) => write!(f, "def {name} := {t}"),
+ Declaration((_, name), None, ref t) => write!(f, "def {name} := {t}"),
- Declaration(name, Some(ref ty), ref t) => write!(f, "def {name}: {ty} := {t}"),
+ Declaration((_, name), Some(ref ty), ref t) => write!(f, "def {name}: {ty} := {t}"),
CheckType(ref t, ref ty) => write!(f, "check {t}: {ty}"),
diff --git a/parser/src/command/parse.rs b/parser/src/command/parse.rs
index 891ad780ff2177e272769638784ae2ded5597b2e..7c43b0a2e989738290f0d8a393c7f9b3de16891b 100644
--- a/parser/src/command/parse.rs
+++ b/parser/src/command/parse.rs
@@ -144,6 +144,7 @@ fn parse_expr(pair: Pair<Rule>) -> Command {
Rule::GetType => {
let mut iter = pair.into_inner();
let t = parse_term(iter.next().unwrap());
+
Command::GetType(t)
},
@@ -151,39 +152,41 @@ fn parse_expr(pair: Pair<Rule>) -> Command {
let mut iter = pair.into_inner();
let t1 = parse_term(iter.next().unwrap());
let t2 = parse_term(iter.next().unwrap());
+
Command::CheckType(t1, t2)
},
Rule::Define => {
let mut iter = pair.into_inner();
- let s = iter.next().unwrap().as_str();
+ let s = iter.next().unwrap();
let term = parse_term(iter.next().unwrap());
- Command::Define(s, None, term)
+
+ Command::Define((convert_span(s.as_span()), s.as_str()), None, term)
},
Rule::DefineCheckType => {
let mut iter = pair.into_inner();
- let s = iter.next().unwrap().as_str();
+ let s = iter.next().unwrap();
let ty = parse_term(iter.next().unwrap());
let term = parse_term(iter.next().unwrap());
- Command::Define(s, Some(ty), term)
+ Command::Define((convert_span(s.as_span()), s.as_str()), 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 s = string_decl.next().unwrap();
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))
+ Command::Declaration((convert_span(s.as_span()), s.as_str()), 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 s = string_decl.next().unwrap();
let vars: Vec<&str> = string_decl.next().unwrap().into_inner().map(|name| name.as_str()).collect();
let ty = parse_term(iter.next().unwrap());
@@ -191,7 +194,8 @@ fn parse_expr(pair: Pair<Rule>) -> Command {
let ty = declaration::Builder::Decl(box ty, vars.clone());
let decl = declaration::Builder::Decl(box decl, vars);
- Command::Declaration(s, Some(ty), decl)
+
+ Command::Declaration((convert_span(s.as_span()), s.as_str()), Some(ty), decl)
},
Rule::Eval => {
@@ -343,7 +347,7 @@ mod tests {
assert_eq!(
line("def x : Type := Prop"),
Ok(Define(
- "x",
+ (Location::new((1, 5), (1, 6)), "x"),
Some(Builder::new(Location::new((1, 9), (1, 14)), Type(box level::Builder::Const(0)))),
Builder::new(Location::new((1, 17), (1, 21)), Prop)
))
@@ -355,7 +359,7 @@ mod tests {
assert_eq!(
line("def x.{u} : Type u := foo.{u}"),
Ok(Declaration(
- "x",
+ (Location::new((1, 5), (1, 6)), "x"),
Some(declaration::Builder::Decl(
box Builder::new(Location::new((1, 13), (1, 19)), Type(box level::Builder::Var("u"))),
["u"].to_vec()
@@ -389,14 +393,21 @@ mod tests {
#[test]
fn successful_define() {
- assert_eq!(line("def x := Prop"), Ok(Define("x", None, Builder::new(Location::new((1, 10), (1, 14)), Prop))));
+ assert_eq!(
+ line("def x := Prop"),
+ Ok(Define((Location::new((1, 5), (1, 6)), "x"), None, Builder::new(Location::new((1, 10), (1, 14)), Prop)))
+ );
}
#[test]
fn successful_declare() {
assert_eq!(
line("def x.{} := Prop"),
- Ok(Declaration("x", None, declaration::Builder::Decl(box Builder::new(Location::new((1, 13), (1, 17)), Prop), vec![])))
+ Ok(Declaration(
+ (Location::new((1, 5), (1, 6)), "x"),
+ None,
+ declaration::Builder::Decl(box Builder::new(Location::new((1, 13), (1, 17)), Prop), vec![])
+ ))
);
}
diff --git a/proost/src/evaluator.rs b/proost/src/evaluator.rs
index 0a536e447fe8816463a05d27a80074e846cc06c5..7159398f76724d50d71739a359651b09aeac7dd9 100644
--- a/proost/src/evaluator.rs
+++ b/proost/src/evaluator.rs
@@ -169,11 +169,11 @@ impl<'arena> Evaluator {
importing: &mut Vec<PathBuf>,
) -> Result<'arena, 'build, Option<Term<'arena>>> {
match *command {
- Command::Define(s, ref type_builder, ref term_builder) => {
+ Command::Define((location, s), ref type_builder, ref term_builder) => {
if arena.get_binding(s).is_some() {
return Err(TopLevel(Error {
kind: ErrorKind::BoundVariable(s.to_owned()),
- location: Location::default(), // TODO (see #38)
+ location,
}));
}
@@ -194,11 +194,11 @@ impl<'arena> Evaluator {
Ok(None)
},
- Command::Declaration(s, ref type_builder, ref decl_builder) => {
+ Command::Declaration((location, s), ref type_builder, ref decl_builder) => {
if arena.get_binding_decl(s).is_some() {
return Err(TopLevel(Error {
kind: ErrorKind::BoundVariable(s.to_owned()),
- location: Location::default(), // TODO (see #38)
+ location,
}));
}
diff --git a/proost/src/main.rs b/proost/src/main.rs
index 2723b42b8f49cbbabd86dd4346dd718c5f3fca65..88e152bf2f850e3f2996a7b1c2cde7dd76aedd4c 100644
--- a/proost/src/main.rs
+++ b/proost/src/main.rs
@@ -149,6 +149,7 @@ pub fn display<'arena>(res: Result<'arena, '_, Option<Term<'arena>>>) {
let location = match err {
Error::Kernel(ref builder, ref err) => Some(builder.apply_trace(&err.trace)),
Error::Parser(ref err) => Some(err.loc),
+ Error::TopLevel(ref err) => Some(err.location),
_ => None,
};