Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Stack trace for blame failures #27

Merged
merged 4 commits into from
Sep 25, 2019
Merged

Stack trace for blame failures #27

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
d74b4ac
First version of a call stack.
teofr Sep 18, 2019
3083d25
Some nice examples to try our new call stack on
teofr Sep 18, 2019
5441f0b
Fixed some warnings
teofr Sep 23, 2019
ae19ab7
`Bounded` -> `Bound`
teofr Sep 25, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Next Next commit
First version of a call stack. 
Quite simple, but I think it has potential.
  • Loading branch information
@teofr
teofr committed Sep 23, 2019
commit d74b4aceb1a0c613d2236b3134ec8079786f4a7b
98 changes: 63 additions & 35 deletions src/eval.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,20 @@ use std::collections::HashMap;
use std::rc::{Rc, Weak};
use term::{RichTerm, Term};

pub type Enviroment = HashMap<Ident, Rc<RefCell<Closure>>>;
pub type Enviroment = HashMap<Ident, (Rc<RefCell<Closure>>, IdentKind)>;
pub type CallStack = Vec<StackElem>;

#[derive(Debug, PartialEq, Clone)]
pub enum StackElem {
App(Option<(usize, usize)>),
Var(IdentKind, Ident, Option<(usize, usize)>),
}

#[derive(Debug, PartialEq, Clone)]
pub enum IdentKind {
Let(),
Lam(),
}

#[derive(Clone, Debug, PartialEq)]
pub struct Closure {
Expand All @@ -26,7 +39,7 @@ impl Closure {

#[derive(Debug, PartialEq)]
pub enum EvalError {
BlameError(Label),
BlameError(Label, Option<CallStack>),
TypeError(String),
}

Expand All @@ -40,25 +53,27 @@ pub fn eval(t0: RichTerm) -> Result<Term, EvalError> {
body: t0,
env: empty_env,
};
let mut call_stack = CallStack::new();
let mut stack = Stack::new();

loop {
let Closure {
body: RichTerm {
term: boxed_term,
pos: _,
pos,
},
mut env,
} = clos;
let term = *boxed_term;
match term {
// Var
Term::Var(x) => {
let mut thunk = Rc::clone(env.get(&x).expect(&format!("Unbound variable {:?}", x)));
let (thunk, id_kind) = env.remove(&x).expect(&format!("Unbound variable {:?}", x));
std::mem::drop(env); // thunk may be a 1RC pointer
if !is_value(&thunk.borrow().body.term) {
stack.push_thunk(Rc::downgrade(&thunk));
}
call_stack.push(StackElem::Var(id_kind, x, pos));
match Rc::try_unwrap(thunk) {
Ok(c) => {
// thunk was the only strong ref to the closure
Expand All @@ -72,10 +87,13 @@ pub fn eval(t0: RichTerm) -> Result<Term, EvalError> {
}
// App
Term::App(t1, t2) => {
stack.push_arg(Closure {
body: t2,
env: env.clone(),
});
stack.push_arg(
Closure {
body: t2,
env: env.clone(),
},
pos,
);
clos = Closure { body: t1, env };
}
// Let
Expand All @@ -84,32 +102,38 @@ pub fn eval(t0: RichTerm) -> Result<Term, EvalError> {
body: s,
env: env.clone(),
}));
env.insert(x, Rc::clone(&thunk));
env.insert(x, (Rc::clone(&thunk), IdentKind::Let()));
clos = Closure { body: t, env: env };
}
// Unary Operation
Term::Op1(op, t) => {
stack.push_op_cont(OperationCont::Op1(op));
stack.push_op_cont(OperationCont::Op1(op), call_stack.len());
clos = Closure { body: t, env };
}
// Binary Operation
Term::Op2(op, fst, snd) => {
stack.push_op_cont(OperationCont::Op2First(
op,
Closure {
body: snd,
env: env.clone(),
},
));
stack.push_op_cont(
OperationCont::Op2First(
op,
Closure {
body: snd,
env: env.clone(),
},
),
call_stack.len(),
);
clos = Closure { body: fst, env };
}
// Promise and Assume
Term::Promise(ty, l, t) | Term::Assume(ty, l, t) => {
stack.push_arg(Closure {
body: t,
env: env.clone(),
});
stack.push_arg(Closure::atomic_closure(RichTerm::new(Term::Lbl(l))));
stack.push_arg(
Closure {
body: t,
env: env.clone(),
},
None,
);
stack.push_arg(Closure::atomic_closure(RichTerm::new(Term::Lbl(l))), None);
clos = Closure {
body: ty.contract(),
env,
Expand All @@ -129,20 +153,21 @@ pub fn eval(t0: RichTerm) -> Result<Term, EvalError> {
}
}
} else {
clos = continuate_operation(
stack.pop_op_cont().expect("Condition already checked"),
clos,
&mut stack,
)?;
let mut cont_result = continuate_operation(clos, &mut stack, &mut call_stack);

if let Err(EvalError::BlameError(l, cs)) = cont_result {
return Err(EvalError::BlameError(l, Some(call_stack)));
}
clos = cont_result?;
}
}
// Call
Term::Fun(x, t) => {
if 0 < stack.count_args() {
let thunk = Rc::new(RefCell::new(
stack.pop_arg().expect("Condition already checked."),
));
env.insert(x, thunk);
let (arg, pos) = stack.pop_arg().expect("Condition already checked.");
call_stack.push(StackElem::App(pos));
let thunk = Rc::new(RefCell::new(arg));
env.insert(x, (thunk, IdentKind::Lam()));
clos = Closure { body: t, env }
} else {
return Ok(Term::Fun(x, t));
Expand Down Expand Up @@ -186,10 +211,13 @@ mod tests {
polarity: false,
path: TyPath::Nil(),
};
assert_eq!(
Err(EvalError::BlameError(label.clone())),
eval(Term::Op1(UnaryOp::Blame(), Term::Lbl(label).into()).into())
);
if let Err(EvalError::BlameError(l, _)) =
eval(Term::Op1(UnaryOp::Blame(), Term::Lbl(label.clone()).into()).into())
{
assert_eq!(l, label);
} else {
panic!("This evaluation should've returned a BlameError!");
}
}

#[test]
Expand Down
48 changes: 30 additions & 18 deletions src/operation.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
use eval::{Closure, EvalError};
use eval::{CallStack, Closure, EvalError};
use label::TyPath;
use stack::Stack;
use term::{BinaryOp, RichTerm, Term, UnaryOp};
Expand All @@ -11,15 +11,17 @@ pub enum OperationCont {
}

pub fn continuate_operation(
cont: OperationCont,
mut clos: Closure,
stack: &mut Stack,
call_stack: &mut CallStack,
) -> Result<Closure, EvalError> {
let (cont, cs_len) = stack.pop_op_cont().expect("Condition already checked");
call_stack.truncate(cs_len);
match cont {
OperationCont::Op1(u_op) => process_unary_operation(u_op, clos, stack),
OperationCont::Op2First(b_op, mut snd_clos) => {
std::mem::swap(&mut clos, &mut snd_clos);
stack.push_op_cont(OperationCont::Op2Second(b_op, snd_clos));
stack.push_op_cont(OperationCont::Op2Second(b_op, snd_clos), cs_len);
Ok(clos)
}
OperationCont::Op2Second(b_op, fst_clos) => {
Expand All @@ -41,8 +43,8 @@ fn process_unary_operation(
UnaryOp::Ite() => {
if let Term::Bool(b) = *t {
if stack.count_args() >= 2 {
let fst = stack.pop_arg().expect("Condition already checked.");
let snd = stack.pop_arg().expect("Condition already checked.");
let (fst, _) = stack.pop_arg().expect("Condition already checked.");
let (snd, _) = stack.pop_arg().expect("Condition already checked.");

Ok(if b { fst } else { snd })
} else {
Expand Down Expand Up @@ -83,7 +85,7 @@ fn process_unary_operation(
}
UnaryOp::Blame() => {
if let Term::Lbl(l) = *t {
Err(EvalError::BlameError(l))
Err(EvalError::BlameError(l, None))
} else {
Err(EvalError::TypeError(format!(
"Expected Label, got {:?}",
Expand Down Expand Up @@ -171,7 +173,7 @@ fn process_binary_operation(
#[cfg(test)]
mod tests {
use super::*;
use eval::Enviroment;
use eval::{CallStack, Enviroment};
use std::collections::HashMap;

fn some_env() -> Enviroment {
Expand All @@ -182,15 +184,18 @@ mod tests {
fn ite_operation() {
let cont = OperationCont::Op1(UnaryOp::Ite());
let mut stack = Stack::new();
stack.push_arg(Closure::atomic_closure(Term::Num(5.0).into()));
stack.push_arg(Closure::atomic_closure(Term::Num(46.0).into()));
stack.push_arg(Closure::atomic_closure(Term::Num(5.0).into()), None);
stack.push_arg(Closure::atomic_closure(Term::Num(46.0).into()), None);

let mut clos = Closure {
body: Term::Bool(true).into(),
env: some_env(),
};

clos = continuate_operation(cont, clos, &mut stack).unwrap();
stack.push_op_cont(cont, 0);
let mut call_stack = CallStack::new();

clos = continuate_operation(clos, &mut stack, &mut call_stack).unwrap();

assert_eq!(
clos,
Expand All @@ -217,8 +222,10 @@ mod tests {
env: some_env(),
};
let mut stack = Stack::new();
stack.push_op_cont(cont, 0);
let mut call_stack = CallStack::new();

clos = continuate_operation(cont, clos, &mut stack).unwrap();
clos = continuate_operation(clos, &mut stack, &mut call_stack).unwrap();

assert_eq!(
clos,
Expand All @@ -230,12 +237,15 @@ mod tests {

assert_eq!(1, stack.count_conts());
assert_eq!(
OperationCont::Op2Second(
BinaryOp::Plus(),
Closure {
body: Term::Num(7.0).into(),
env: some_env(),
}
(
OperationCont::Op2Second(
BinaryOp::Plus(),
Closure {
body: Term::Num(7.0).into(),
env: some_env(),
}
),
0
),
stack.pop_op_cont().expect("Condition already checked.")
);
Expand All @@ -255,8 +265,10 @@ mod tests {
env: some_env(),
};
let mut stack = Stack::new();
stack.push_op_cont(cont, 0);
let mut call_stack = CallStack::new();

clos = continuate_operation(cont, clos, &mut stack).unwrap();
clos = continuate_operation(clos, &mut stack, &mut call_stack).unwrap();

assert_eq!(
clos,
Expand Down
Loading