diff --git a/lib/src/atom/matcher.rs b/lib/src/atom/matcher.rs
index 4433057af..1e9ab311b 100644
--- a/lib/src/atom/matcher.rs
+++ b/lib/src/atom/matcher.rs
@@ -75,6 +75,43 @@ enum VarResolutionResult<T> {
     None
 }
 
+/// Abstraction of the variable set. It is used to allow passing both
+/// HashSet<&VariableAtom> and HashSet<VariableAtom> to the
+/// [Bindings::narrow_vars] method.
+pub trait VariableSet {
+    type Iter<'a> : Iterator<Item = &'a VariableAtom> where Self: 'a;
+
+    /// Returns true if var is a part of the set.
+    fn contains(&self, var: &VariableAtom) -> bool;
+
+    /// Iterate trough a list of variables in the set.
+    fn iter(&self) -> Self::Iter<'_>;
+}
+
+impl VariableSet for HashSet<&VariableAtom> {
+    type Iter<'a> = std::iter::Map<
+        std::collections::hash_set::Iter<'a, &'a VariableAtom>,
+        fn(&'a &VariableAtom) -> &'a VariableAtom> where Self: 'a;
+
+    fn contains(&self, var: &VariableAtom) -> bool {
+        HashSet::contains(self, var)
+    }
+    fn iter(&self) -> Self::Iter<'_> {
+        HashSet::iter(self).map(|a| *a)
+    }
+}
+
+impl VariableSet for HashSet<VariableAtom> {
+    type Iter<'a> = std::collections::hash_set::Iter<'a, VariableAtom> where Self: 'a;
+
+    fn contains(&self, var: &VariableAtom) -> bool {
+        HashSet::contains(self, var)
+    }
+    fn iter(&self) -> Self::Iter<'_> {
+        HashSet::iter(self)
+    }
+}
+
 /// Represents variable bindings. Keeps two kinds of relations inside:
 /// variables equalities and variable value assignments. For example this
 /// structure is able to precisely represent result of matching atoms like
@@ -97,6 +134,10 @@ impl Bindings {
         }
     }
 
+    pub(crate) fn len(&self) -> usize {
+        self.id_by_var.len()
+    }
+
     /// Returns true if bindings doesn't contain any variable.
     pub fn is_empty(&self) -> bool {
         self.id_by_var.is_empty()
@@ -389,6 +430,12 @@ impl Bindings {
             false => None
         };
 
+        if self.is_empty() {
+            return b.clone().into()
+        } else if b.is_empty() {
+            return self.into()
+        }
+
         let results = b.id_by_var.iter().fold(smallvec::smallvec![(self, HashMap::new())],
             |results, (var, var_id)| -> smallvec::SmallVec<[(Bindings, HashMap<u32, VariableAtom>); 1]> {
                 let mut all_results = smallvec::smallvec![];
@@ -443,7 +490,7 @@ impl Bindings {
         }
     }
 
-    fn build_var_mapping<'a>(&'a self, required_names: &HashSet<&VariableAtom>, required_ids: &HashSet<u32>) -> HashMap<&'a VariableAtom, &'a VariableAtom> {
+    fn build_var_mapping<'a, T: VariableSet>(&'a self, required_names: &T, required_ids: &HashSet<u32>) -> HashMap<&'a VariableAtom, &'a VariableAtom> {
         let mut id_names: HashSet<VariableAtom> = HashSet::new();
         let mut mapping = HashMap::new();
         for (var, &id) in &self.id_by_var {
@@ -467,12 +514,14 @@ impl Bindings {
     }
 
     fn find_deps(&self, var: &VariableAtom, deps: &mut HashSet<VariableAtom>) {
-        deps.insert(var.clone());
-        self.get_value(var).iter()
-            .for_each(|value| {
-                value.iter().filter_map(|atom| <&VariableAtom>::try_from(atom).ok())
-                    .for_each(|var| { self.find_deps(var, deps); });
-            });
+        if !deps.contains(var) {
+            deps.insert(var.clone());
+            self.get_value(var).iter()
+                .for_each(|value| {
+                    value.iter().filter_map(|atom| <&VariableAtom>::try_from(atom).ok())
+                        .for_each(|var| { self.find_deps(var, deps); });
+                    });
+        }
     }
 
     /// Get narrow bindings which contains only passed set of variables and
@@ -491,9 +540,9 @@ impl Bindings {
     ///
     /// assert_eq!(right, bind!{ rightB: expr!("A"), rightF: expr!("F"), rightE: expr!(rightE) });
     /// ```
-    pub fn narrow_vars(&self, vars: &HashSet<&VariableAtom>) -> Bindings {
+    pub fn narrow_vars<T: VariableSet>(&self, vars: &T) -> Bindings {
         let mut deps: HashSet<VariableAtom> = HashSet::new();
-        for var in vars {
+        for var in vars.iter() {
             self.find_deps(var, &mut deps);
         }
 
@@ -503,7 +552,7 @@ impl Bindings {
             .map(Option::unwrap).map(|&id| id)
             .collect();
 
-        let mapping = self.build_var_mapping(&vars, &dep_ids);
+        let mapping = self.build_var_mapping(vars, &dep_ids);
 
         let mut bindings = Bindings::new();
         bindings.next_var_id = self.next_var_id;
@@ -569,22 +618,40 @@ impl Bindings {
         self
     }
 
+    fn no_value(&self, id: &u32) -> bool {
+        self.value_by_id.get(id) == None &&
+            self.id_by_var.iter().filter(|(_var, vid)| *vid == id).count() == 1
+    }
+
     /// Keep only variables passed in vars
-    pub fn cleanup(&mut self, vars: &HashSet<&VariableAtom>) {
+    pub fn cleanup<T: VariableSet>(&mut self, vars: &T) {
         let to_remove: HashSet<VariableAtom> = self.id_by_var.iter()
-            .filter_map(|(var, _id)| if !vars.contains(var) { Some(var.clone()) } else { None })
+            .filter_map(|(var, id)| {
+                if !vars.contains(var) || self.no_value(id) {
+                    Some(var.clone())
+                } else {
+                    None
+                }
+            })
             .collect();
-        to_remove.into_iter().for_each(|var| { self.id_by_var.remove(&var); });
+        to_remove.into_iter().for_each(|var| {
+            self.id_by_var.remove(&var);
+        });
     }
 
-    fn has_loops(&self) -> bool {
+    pub fn has_loops(&self) -> bool {
         let vars_by_id = self.vars_by_id();
         for (var_id, value) in &self.value_by_id {
             let mut used_vars = HashSet::new();
-            vars_by_id.get(var_id).unwrap().iter().for_each(|var| { used_vars.insert(*var); });
-            match self.resolve_vars_in_atom(value, &used_vars) {
-                VarResolutionResult::Loop => return true,
-                _ => {},
+            let var = vars_by_id.get(var_id);
+            // TODO: cleanup removes vars but leaves var_ids
+            //assert!(var.is_some(), "No variable name for var_id: {}, value: {}, self: {}", var_id, value, self);
+            if var.is_some() {
+                var.unwrap().iter().for_each(|var| { used_vars.insert(*var); });
+                match self.resolve_vars_in_atom(value, &used_vars) {
+                    VarResolutionResult::Loop => return true,
+                    _ => {},
+                }
             }
         }
         false
@@ -1176,7 +1243,7 @@ mod test {
     }
 
     #[test]
-    fn test_bindings_merge() {
+    fn bindings_merge() {
         assert_eq!(bind!{ a: expr!("A") }.merge_v2(
             &bind!{ a: expr!("A"), b: expr!("B") }),
             bind_set![{ a: expr!("A"), b: expr!("B") }]);
@@ -1185,6 +1252,13 @@ mod test {
             bind_set![{ a: expr!("A"), b: expr!("B") }]);
     }
 
+    #[test]
+    fn bindings_merge_self_recursion() {
+        assert_eq!(bind!{ a: expr!(b)  }.merge_v2(
+            &bind!{ b: expr!("S" b) }),
+            bind_set![{ a: expr!(b), b: expr!("S" b) }]);
+    }
+
     #[test]
     fn match_variable_name_conflict() {
         assert_match(expr!("a" (W)), expr!("a" W), vec![]);
@@ -1456,6 +1530,16 @@ mod test {
         Ok(())
     }
 
+    #[test]
+    fn bindings_narrow_vars_infinite_loop() -> Result<(), &'static str> {
+        let bindings = Bindings::new().add_var_binding_v2(VariableAtom::new("x"), expr!("a" x "b"))?;
+
+        let narrow = bindings.narrow_vars(&HashSet::from([&VariableAtom::new("x")]));
+
+        assert_eq!(narrow, bind!{ x: expr!("a" x "b") });
+        Ok(())
+    }
+
     #[test]
     fn bindings_narrow_vars_keeps_vars_equality() -> Result<(), &'static str> {
         let bindings = Bindings::new()
@@ -1491,7 +1575,7 @@ mod test {
     }
 
     #[test]
-    fn bindings_add_var_value_splits_bindings() {
+    fn bindings_add_var_binding_splits_bindings() {
         let pair = ReturnPairInX{};
 
         // ({ x -> B, x -> C } (A $x)) ~ ($s $s)
@@ -1506,6 +1590,15 @@ mod test {
             bind!{ s: expr!({ pair }), x: expr!("C") } ]);
     }
 
+    #[test]
+    fn bindings_add_var_binding_self_recursion() {
+        let a = VariableAtom::new("a");
+        let bindings = Bindings::new();
+        assert_eq!(
+            bindings.add_var_binding_v2(a.clone(), Atom::expr([Atom::sym("S"), Atom::Variable(a)])),
+            Ok(bind!{ a: expr!("S" a) }));
+    }
+
     #[test]
     fn bindings_add_var_equality_splits_bindings() {
         let pair = ReturnPairInX{};
@@ -1523,6 +1616,17 @@ mod test {
             bind!{ s: expr!({ pair }), y: expr!("A" x), x: expr!("C") } ]);
     }
 
+    #[test]
+    fn bindings_add_var_equality_self_recursion() -> Result<(), &'static str> {
+        let a = VariableAtom::new("a");
+        let b = VariableAtom::new("b");
+        let mut bindings = Bindings::new();
+        bindings.add_var_no_value(&a);
+        let bindings = bindings.add_var_binding_v2(b.clone(), Atom::expr([Atom::sym("S"), Atom::Variable(a.clone())]))?;
+        assert_eq!(bindings.add_var_equality(&a, &b), Ok(bind!{ a: expr!(b), b: expr!("S" a) }));
+        Ok(())
+    }
+
     #[test]
     fn bindings_merge_custom_matching() {
 
@@ -1581,8 +1685,9 @@ mod test {
             .add_var_equality(&VariableAtom::new("a"), &VariableAtom::new("b"))?
             .add_var_binding_v2(VariableAtom::new("b"), expr!("B" d))?
             .add_var_binding_v2(VariableAtom::new("c"), expr!("c"))?
-            .add_var_binding_v2(VariableAtom::new("d"), expr!("D"))?;
-        bindings.cleanup(&[&VariableAtom::new("b")].into());
+            .add_var_binding_v2(VariableAtom::new("d"), expr!("D"))?
+            .with_var_no_value(&VariableAtom::new("e"));
+        bindings.cleanup(&Into::<HashSet<&VariableAtom>>::into([&VariableAtom::new("b"), &VariableAtom::new("e")]));
         assert_eq!(bindings, bind!{ b: expr!("B" d) });
         Ok(())
     }
diff --git a/lib/src/atom/mod.rs b/lib/src/atom/mod.rs
index 9fb377812..d0e5a63ac 100644
--- a/lib/src/atom/mod.rs
+++ b/lib/src/atom/mod.rs
@@ -160,7 +160,7 @@ impl ExpressionAtom {
     /// Constructs new expression from vector of sub-atoms. Not intended to be
     /// used directly, use [Atom::expr] instead.
     #[doc(hidden)]
-    fn new(children: Vec<Atom>) -> Self {
+    pub(crate) fn new(children: Vec<Atom>) -> Self {
         Self{ children }
     }
 
diff --git a/lib/src/metta/interpreter.rs b/lib/src/metta/interpreter.rs
index 66f648772..c197cf73d 100644
--- a/lib/src/metta/interpreter.rs
+++ b/lib/src/metta/interpreter.rs
@@ -78,6 +78,7 @@ use crate::common::ReplacingMapper;
 use std::ops::Deref;
 use std::rc::Rc;
 use std::fmt::{Debug, Display, Formatter};
+use std::collections::HashSet;
 
 /// Wrapper, So the old interpreter can present the same public interface as the new intperpreter
 pub struct InterpreterState<'a, T: SpaceRef<'a>> {
@@ -248,7 +249,7 @@ impl InterpreterCache {
 
     fn insert(&mut self, key: Atom, mut value: Results) {
         value.iter_mut().for_each(|res| {
-            let vars = key.iter().filter_type::<&VariableAtom>().collect();
+            let vars: HashSet<&VariableAtom> = key.iter().filter_type::<&VariableAtom>().collect();
             res.0 = apply_bindings_to_atom(&res.0, &res.1);
             res.1.cleanup(&vars);
         });
diff --git a/lib/src/metta/interpreter2.rs b/lib/src/metta/interpreter2.rs
index 3cc863298..b086c0121 100644
--- a/lib/src/metta/interpreter2.rs
+++ b/lib/src/metta/interpreter2.rs
@@ -12,15 +12,22 @@ use crate::metta::*;
 
 use std::fmt::{Debug, Display, Formatter};
 use std::convert::TryFrom;
+use std::collections::HashSet;
+
+#[derive(Clone, PartialEq, Debug)]
+enum Status {
+    Final,
+    InProgress,
+}
 
 /// Result of atom interpretation plus variable bindings found
 #[derive(Clone, PartialEq)]
-pub struct InterpretedAtom(Atom, Bindings);
+struct InterpretedAtom(Atom, Bindings, Status);
 
 impl Display for InterpretedAtom {
     fn fmt(&self, f: &mut Formatter) -> std::fmt::Result {
         if self.1.is_empty() {
-            write!(f, "{}", self.0)
+            write!(f, "{}|{:?}", self.0, self.2)
         } else {
             // TODO: it is possible to cleanup all bindings for nested
             // expressions which were introduced by matching when all
@@ -29,7 +36,7 @@ impl Display for InterpretedAtom {
             // (make air wet) leads to (start kettle), {$y: kettle}) result
             // but $y is not present in the expression after interpreting
             // (make air wet) and can be removed.
-            write!(f, "{}|{}", self.0, self.1)
+            write!(f, "{}|{}|{:?}", self.0, self.1, self.2)
         }
     }
 }
@@ -62,6 +69,7 @@ pub struct InterpreterState<'a, T: SpaceRef<'a>> {
     plan: Vec<InterpretedAtom>,
     finished: Vec<Atom>,
     context: InterpreterContext<'a, T>,
+    vars: HashSet<VariableAtom>,
 }
 
 fn atom_as_slice(atom: &Atom) -> Option<&[Atom]> {
@@ -82,6 +90,7 @@ impl<'a, T: SpaceRef<'a>> InterpreterState<'a, T> {
             plan: vec![],
             finished: results,
             context: InterpreterContext::new(space),
+            vars: HashSet::new(),
         }
     }
 
@@ -105,8 +114,10 @@ impl<'a, T: SpaceRef<'a>> InterpreterState<'a, T> {
         if is_embedded_op(&atom.0) {
             self.plan.push(atom);
         } else {
-            let InterpretedAtom(atom, _bindings) = atom;
+            let InterpretedAtom(atom, bindings, _status) = atom;
             if atom != EMPTY_SYMBOL {
+                let bindings = bindings.convert_var_equalities_to_bindings(&self.vars);
+                let atom = apply_bindings_to_atom(&atom, &bindings);
                 self.finished.push(atom);
             }
         }
@@ -130,9 +141,79 @@ impl<'a, T: SpaceRef<'a>> std::fmt::Display for InterpreterState<'a, T> {
 pub fn interpret_init<'a, T: Space + 'a>(space: T, expr: &Atom) -> InterpreterState<'a, T> {
     let context = InterpreterContext::new(space);
     InterpreterState {
-        plan: vec![InterpretedAtom(expr.clone(), Bindings::new())],
+        plan: vec![InterpretedAtom(expr.clone(), Bindings::new(), Status::InProgress)],
         finished: vec![],
-        context
+        context,
+        vars: expr.iter().filter_type::<&VariableAtom>().cloned().collect(),
+    }
+}
+
+use std::fmt::Write;
+
+fn print_stack(atom: &InterpretedAtom) -> String {
+    let InterpretedAtom(atom, bindings, _status) = atom;
+    let mut levels = Vec::new();
+    print_level(&mut levels, atom, bindings);
+    let mut buffer = String::new();
+    let mut i = levels.len();
+    writeln!(buffer, "=> {:05} {}", i, levels.pop().unwrap()).unwrap();
+    while !levels.is_empty() {
+        i = i - 1;
+        writeln!(buffer, "   {:05} {}", i, levels.pop().unwrap()).unwrap();
+    }
+    buffer
+}
+
+fn print_level(levels: &mut Vec<String>, atom: &Atom, bindings: &Bindings) {
+    levels.push(String::new());
+    let output = levels.last_mut().unwrap();
+    match atom {
+        Atom::Expression(expr) => match expr.children().as_slice() {
+            [op, args @ ..] if *op == FUNCTION_SYMBOL => {
+                match args {
+                    [Atom::Expression(_body)] => {
+                        write!(output, "{}", atom).unwrap();
+                    },
+                    [body @ Atom::Expression(_body), call] => {
+                        write!(output, "{}", call).unwrap();
+                        print_level(levels, body, bindings);
+                    },
+                    _ => panic!(),
+                }
+            },
+            [op, args @ ..] if *op == CHAIN_SYMBOL => {
+                match args {
+                    [nested, Atom::Variable(var), templ] => {
+                        write!(output, "(chain <result> {} {})", var, templ).unwrap();
+                        print_level(levels, nested, bindings);
+                    },
+                    _ => panic!(),
+                }
+            },
+            [op, args @ ..] if *op == COLLAPSE_BIND => {
+                match args {
+                    [_atom] => {
+                        write!(output, "{}", atom).unwrap();
+                    },
+                    [Atom::Expression(current), Atom::Expression(finished)] => {
+                        let current_len = current.children().len();
+                        if current_len > 0 {
+                            let next = &current.children()[current_len - 1];
+                            let (atom, bindings) = atom_as_interpreted_atom(next);
+                            write!(output, "(collapse-bind {} {})", current, finished).unwrap();
+                            print_level(levels, atom, bindings);
+                        } else {
+                            write!(output, "{}", atom).unwrap();
+                        }
+                    },
+                    _ => panic!(),
+                }
+            },
+            _ => {
+                write!(output, "{}", atom).unwrap();
+            },
+        },
+        _ => write!(output, "{}", atom).unwrap(),
     }
 }
 
@@ -145,8 +226,9 @@ pub fn interpret_init<'a, T: Space + 'a>(space: T, expr: &Atom) -> InterpreterSt
 /// * `step` - [StepResult::Execute] result from the previous step.
 pub fn interpret_step<'a, T: Space + 'a>(mut state: InterpreterState<'a, T>) -> InterpreterState<'a, T> {
     let interpreted_atom = state.pop().unwrap();
-    log::debug!("interpret_step: {:?}", interpreted_atom);
-    for result in interpret_atom(&state.context.space, interpreted_atom) {
+    log::debug!("interpret_step: {}", interpreted_atom);
+    log::debug!("stack:\n{}", print_stack(&interpreted_atom));
+    for result in interpret_root_atom(&state.context, interpreted_atom) {
         state.push(result);
     }
     state
@@ -174,7 +256,9 @@ fn is_embedded_op(atom: &Atom) -> bool {
             || *op == UNIFY_SYMBOL
             || *op == CONS_SYMBOL
             || *op == DECONS_SYMBOL
-            || *op == FUNCTION_SYMBOL,
+            || *op == FUNCTION_SYMBOL
+            || *op == COLLAPSE_BIND
+            || *op == SUPERPOSE_BIND,
         _ => false,
     }
 }
@@ -191,22 +275,17 @@ fn is_function_op(atom: &Atom) -> bool {
     is_op(atom, &FUNCTION_SYMBOL)
 }
 
-fn is_eval_op(atom: &Atom) -> bool {
-    is_op(atom, &EVAL_SYMBOL)
-}
+type Variables = HashSet<VariableAtom>;
 
-fn is_chain_op(atom: &Atom) -> bool {
-    is_op(atom, &CHAIN_SYMBOL)
+fn interpret_root_atom<'a, T: SpaceRef<'a>>(context: &InterpreterContext<'a, T>, interpreted_atom: InterpretedAtom) -> Vec<InterpretedAtom> {
+    let InterpretedAtom(atom, bindings, _status) = interpreted_atom;
+    let vars: Variables = atom.iter().filter_type::<&VariableAtom>().cloned().collect();
+    interpret_nested_atom(context, atom, bindings, &vars)
 }
 
-fn interpret_atom<'a, T: SpaceRef<'a>>(space: T, interpreted_atom: InterpretedAtom) -> Vec<InterpretedAtom> {
-    interpret_atom_root(space, interpreted_atom, true)
-}
-
-fn interpret_atom_root<'a, T: SpaceRef<'a>>(space: T, interpreted_atom: InterpretedAtom, root: bool) -> Vec<InterpretedAtom> {
-    let InterpretedAtom(atom, bindings) = interpreted_atom;
+fn interpret_nested_atom<'a, T: SpaceRef<'a>>(context: &InterpreterContext<'a, T>, atom: Atom, bindings: Bindings, vars: &Variables) -> Vec<InterpretedAtom> {
     let expr = atom_as_slice(&atom);
-    let mut result = match expr {
+    let result = match expr {
         Some([op, args @ ..]) if *op == EVAL_SYMBOL => {
             match args {
                 [_atom] => {
@@ -214,13 +293,13 @@ fn interpret_atom_root<'a, T: SpaceRef<'a>>(space: T, interpreted_atom: Interpre
                     // error (see error branch below), don't think it is a best
                     // way, but don't see a better solution
                     match atom_into_array(atom) {
-                        Some([_, atom]) => eval(space, atom, bindings),
+                        Some([_, atom]) => eval(context, atom, bindings, vars),
                         _ => panic!("Unexpected state"),
                     }
                 },
                 _ => {
                     let error: String = format!("expected: ({} <atom>), found: {}", EVAL_SYMBOL, atom);
-                    vec![InterpretedAtom(error_atom(atom, error), bindings)]
+                    vec![InterpretedAtom(error_atom(atom, error), bindings, Status::Final)]
                 },
             }
         },
@@ -229,22 +308,22 @@ fn interpret_atom_root<'a, T: SpaceRef<'a>>(space: T, interpreted_atom: Interpre
                 [_nested, Atom::Variable(_var), _templ] => {
                     match atom_into_array(atom) {
                         Some([_, nested, Atom::Variable(var), templ]) =>
-                            chain(space, bindings, nested, var, templ),
+                            chain(context, bindings, nested, var, templ, vars),
                         _ => panic!("Unexpected state"),
                     }
                 },
                 _ => {
                     let error: String = format!("expected: ({} <nested> (: <var> Variable) <templ>), found: {}", CHAIN_SYMBOL, atom);
-                    vec![InterpretedAtom(error_atom(atom, error), bindings)]
+                    vec![InterpretedAtom(error_atom(atom, error), bindings, Status::Final)]
                 },
             }
         },
         Some([op, args @ ..]) if *op == UNIFY_SYMBOL => {
             match args {
-                [atom, pattern, then, else_] => unify(bindings, atom, pattern, then, else_),
+                [atom, pattern, then, else_] => unify(bindings, atom, pattern, then, else_, vars),
                 _ => {
                     let error: String = format!("expected: ({} <atom> <pattern> <then> <else>), found: {}", UNIFY_SYMBOL, atom);
-                    vec![InterpretedAtom(error_atom(atom, error), bindings)]
+                    vec![InterpretedAtom(error_atom(atom, error), bindings, Status::Final)]
                 },
             }
         },
@@ -258,7 +337,7 @@ fn interpret_atom_root<'a, T: SpaceRef<'a>>(space: T, interpreted_atom: Interpre
                 },
                 _ => {
                     let error: String = format!("expected: ({} (: <expr> Expression)), found: {}", DECONS_SYMBOL, atom);
-                    vec![InterpretedAtom(error_atom(atom, error), bindings)]
+                    vec![InterpretedAtom(error_atom(atom, error), bindings, Status::Final)]
                 },
             }
         },
@@ -272,7 +351,7 @@ fn interpret_atom_root<'a, T: SpaceRef<'a>>(space: T, interpreted_atom: Interpre
                 },
                 _ => {
                     let error: String = format!("expected: ({} <head> (: <tail> Expression)), found: {}", CONS_SYMBOL, atom);
-                    vec![InterpretedAtom(error_atom(atom, error), bindings)]
+                    vec![InterpretedAtom(error_atom(atom, error), bindings, Status::Final)]
                 },
             }
         },
@@ -281,33 +360,67 @@ fn interpret_atom_root<'a, T: SpaceRef<'a>>(space: T, interpreted_atom: Interpre
                 [Atom::Expression(_body)] => {
                     match atom_into_array(atom) {
                         Some([_, body]) =>
-                            function(space, bindings, body, None),
+                            function(context, bindings, body.clone(), body, vars),
                         _ => panic!("Unexpected state"),
                     }
                 },
-                [Atom::Expression(_body), Atom::Expression(_call)] => {
+                [Atom::Expression(_body), _call] => {
                     match atom_into_array(atom) {
                         Some([_, body, call]) =>
-                            function(space, bindings, body, Some(call)),
+                            function(context, bindings, body, call, vars),
                         _ => panic!("Unexpected state"),
                     }
                 },
                 _ => {
                     let error: String = format!("expected: ({} (: <body> Expression)), found: {}", FUNCTION_SYMBOL, atom);
-                    vec![InterpretedAtom(error_atom(atom, error), bindings)]
+                    vec![InterpretedAtom(error_atom(atom, error), bindings, Status::Final)]
+                },
+            }
+        },
+        Some([op, args @ ..]) if *op == COLLAPSE_BIND => {
+            match args {
+                [_atom] => {
+                    match atom_into_array(atom) {
+                        Some([_, atom]) => {
+                            let current = vec![interpreted_atom_into_atom(InterpretedAtom(atom, bindings.clone(), Status::InProgress))];
+                            collapse_bind(context, bindings, ExpressionAtom::new(current), ExpressionAtom::new(vec![]), vars)
+                        },
+                        _ => panic!("Unexpected state"),
+                    }
+                },
+                [Atom::Expression(_current), Atom::Expression(_finished)] => {
+                    match atom_into_array(atom) {
+                        Some([_, Atom::Expression(current), Atom::Expression(finished)]) =>
+                            collapse_bind(context, bindings, current, finished, vars),
+                        _ => panic!("Unexpected state"),
+                    }
+                },
+                _ => {
+                    let error: String = format!("expected: ({} (: <current> Expression) [(: <finished> Expression)]), found: {}", COLLAPSE_BIND, atom);
+                    vec![InterpretedAtom(error_atom(atom, error), bindings, Status::Final)]
+                },
+            }
+        },
+        Some([op, args @ ..]) if *op == SUPERPOSE_BIND => {
+            match args {
+                [_atom] => {
+                    match atom_into_array(atom) {
+                        Some([_, Atom::Expression(collapsed)]) => {
+                            superpose_bind(collapsed)
+                        },
+                        _ => panic!("Unexpected state"),
+                    }
+                },
+                _ => {
+                    let error: String = format!("expected: ({} (: <collapsed> Expression)), found: {}", SUPERPOSE_BIND, atom);
+                    vec![InterpretedAtom(error_atom(atom, error), bindings, Status::Final)]
                 },
             }
         },
         _ => {
-            vec![InterpretedAtom(return_atom(atom), bindings)]
+            vec![InterpretedAtom(return_atom(atom), bindings, Status::Final)]
         },
     };
-    if root {
-        result.iter_mut().for_each(|interpreted| {
-            let InterpretedAtom(atom, bindings) = interpreted;
-            *bindings = bindings.narrow_vars(&atom.iter().filter_type::<&VariableAtom>().collect());
-        });
-    }
     result
 }
 
@@ -323,7 +436,7 @@ fn return_atom(atom: Atom) -> Atom {
     atom
 }
 
-fn eval<'a, T: SpaceRef<'a>>(space: T, atom: Atom, bindings: Bindings) -> Vec<InterpretedAtom> {
+fn eval<'a, T: SpaceRef<'a>>(context: &InterpreterContext<'a, T>, atom: Atom, bindings: Bindings, vars: &Variables) -> Vec<InterpretedAtom> {
     match atom_as_slice(&atom) {
         Some([Atom::Grounded(op), args @ ..]) => {
             match op.execute(args) {
@@ -341,129 +454,203 @@ fn eval<'a, T: SpaceRef<'a>>(space: T, atom: Atom, bindings: Bindings) -> Vec<In
                         vec![]
                     } else {
                         results.into_iter()
-                            .map(|atom| InterpretedAtom(atom, bindings.clone()))
+                            .map(|atom| {
+                                let status = if is_function_op(&atom) { Status::InProgress } else { Status::Final };
+                                InterpretedAtom(atom, bindings.clone(), status)
+                            })
                             .collect()
                     }
                 },
                 Err(ExecError::Runtime(err)) =>
-                    vec![InterpretedAtom(error_atom(atom, err), bindings)],
+                    vec![InterpretedAtom(error_atom(atom, err), bindings, Status::Final)],
                 Err(ExecError::NoReduce) =>
                     // TODO: we could remove ExecError::NoReduce and explicitly
                     // return NOT_REDUCIBLE_SYMBOL from the grounded function instead.
-                    vec![InterpretedAtom(return_not_reducible(), bindings)],
+                    vec![InterpretedAtom(return_not_reducible(), bindings, Status::Final)],
             }
         },
-        _ if is_embedded_op(&atom) =>
-            interpret_atom_root(space, InterpretedAtom(atom, bindings), false),
-        _ => query(space, atom, bindings),
+        _ if is_embedded_op(&atom) => {
+            interpret_nested_atom(context, atom, bindings, vars)
+        },
+        _ => query(&context.space, atom, bindings, vars),
     }
 }
 
-fn query<'a, T: SpaceRef<'a>>(space: T, atom: Atom, bindings: Bindings) -> Vec<InterpretedAtom> {
-    let var = VariableAtom::new("X").make_unique();
-    let query = Atom::expr([EQUAL_SYMBOL, atom, Atom::Variable(var.clone())]);
+fn query<'a, T: SpaceRef<'a>>(space: T, atom: Atom, bindings: Bindings, vars: &Variables) -> Vec<InterpretedAtom> {
+    let var_x = VariableAtom::new("X").make_unique();
+    let query = Atom::expr([EQUAL_SYMBOL, atom.clone(), Atom::Variable(var_x.clone())]);
     let results = space.query(&query);
-    let atom = Atom::Variable(var);
-    if results.is_empty() {
-        vec![InterpretedAtom(return_not_reducible(), bindings)]
-    } else {
+    let atom_x = Atom::Variable(var_x);
+    let results: Vec<InterpretedAtom> = {
+        log::debug!("interpreter2::query: query: {}", query);
+        log::debug!("interpreter2::query: results.len(): {} bindings.len(): {} results: {} bindings: {}",
+            results.len(), bindings.len(), results, bindings);
         results.into_iter()
-            .flat_map(|b| {
-                b.merge_v2(&bindings).into_iter().map(|b| {
-                    let atom = apply_bindings_to_atom(&atom, &b);
-                    InterpretedAtom(atom, b)
+            .flat_map(|mut b| {
+                let mut res = apply_bindings_to_atom(&atom_x, &b);
+                let status = if is_function_op(&res) { Status::InProgress } else { Status::Final };
+                if is_function_op(&res) {
+                    match res {
+                        Atom::Expression(ref mut expr) => {
+                            expr.children_mut().push(atom.clone());
+                        }
+                        _ => {},
+                    }
+                }
+                b.cleanup(vars);
+                log::debug!("interpreter2::query: b: {}", b);
+                b.merge_v2(&bindings).into_iter().filter_map(move |b| {
+                    if b.has_loops() {
+                        None
+                    } else {
+                        Some(InterpretedAtom(res.clone(), b, status.clone()))
+                    }
                 })
             })
             .collect()
+    };
+    if results.is_empty() {
+        vec![InterpretedAtom(return_not_reducible(), bindings, Status::Final)]
+    } else {
+        results
     }
 }
 
-fn chain<'a, T: SpaceRef<'a>>(space: T, bindings: Bindings, nested: Atom, var: VariableAtom, templ: Atom) -> Vec<InterpretedAtom> {
+fn chain<'a, T: SpaceRef<'a>>(context: &InterpreterContext<'a, T>, bindings: Bindings, nested: Atom, var: VariableAtom, templ: Atom, vars: &Variables) -> Vec<InterpretedAtom> {
     fn apply(bindings: Bindings, nested: Atom, var: VariableAtom, templ: &Atom) -> InterpretedAtom {
         let b = Bindings::new().add_var_binding_v2(var, nested).unwrap();
         let result = apply_bindings_to_atom(templ, &b);
-        InterpretedAtom(result, bindings)
+        InterpretedAtom(result, bindings, Status::InProgress)
     }
 
-    let is_eval = is_eval_op(&nested);
-    if is_function_op(&nested) {
-      let mut result = interpret_atom_root(space, InterpretedAtom(nested, bindings), false);
+    if is_embedded_op(&nested) {
+      let mut result = interpret_nested_atom(context, nested, bindings, vars);
       if result.len() == 1 {
-          let InterpretedAtom(r, b) = result.pop().unwrap();
-          if is_function_op(&r) {
-              vec![InterpretedAtom(Atom::expr([CHAIN_SYMBOL, r, Atom::Variable(var), templ]), b)]
+          let InterpretedAtom(r, b, s) = result.pop().unwrap();
+          if s == Status::InProgress {
+              vec![InterpretedAtom(Atom::expr([CHAIN_SYMBOL, r, Atom::Variable(var), templ]), b, Status::InProgress)]
           } else {
               vec![apply(b, r, var.clone(), &templ)]
           }
       } else {
           result.into_iter()
-              .map(|InterpretedAtom(r, b)| {
-                  if is_function_op(&r) {
-                      InterpretedAtom(Atom::expr([CHAIN_SYMBOL, r, Atom::Variable(var.clone()), templ.clone()]), b)
+              .map(|InterpretedAtom(r, b, s)| {
+                  if s == Status::InProgress {
+                      InterpretedAtom(Atom::expr([CHAIN_SYMBOL, r, Atom::Variable(var.clone()), templ.clone()]), b, Status::InProgress)
                   } else {
                       apply(b, r, var.clone(), &templ)
                   }
               })
           .collect()
       }
-    } else if is_embedded_op(&nested) {
-        let result = interpret_atom_root(space, InterpretedAtom(nested.clone(), bindings), false);
-        let result = result.into_iter()
-            .map(|InterpretedAtom(r, b)| {
-                if is_eval && is_function_op(&r) {
-                    match atom_into_array(r) {
-                        Some([_, body]) =>
-                            InterpretedAtom(Atom::expr([CHAIN_SYMBOL, Atom::expr([FUNCTION_SYMBOL, body, nested.clone()]), Atom::Variable(var.clone()), templ.clone()]), b),
-                        _ => panic!("Unexpected state"),
-                    }
-                } else if is_chain_op(&r) {
-                    InterpretedAtom(Atom::expr([CHAIN_SYMBOL, r, Atom::Variable(var.clone()), templ.clone()]), b)
-                } else {
-                    apply(b, r, var.clone(), &templ)
-                }
-            })
-        .collect();
-        result
     } else {
         vec![apply(bindings, nested, var, &templ)]
     }
 }
 
-fn function<'a, T: SpaceRef<'a>>(space: T, bindings: Bindings, body: Atom, call: Option<Atom>) -> Vec<InterpretedAtom> {
-    let call = match call {
-        Some(call) => call,
-        None => Atom::expr([FUNCTION_SYMBOL, body.clone()]),
-    };
+fn function<'a, T: SpaceRef<'a>>(context: &InterpreterContext<'a, T>, bindings: Bindings, body: Atom, call: Atom, vars: &Variables) -> Vec<InterpretedAtom> {
     match atom_as_slice(&body) {
         Some([op, _result]) if *op == RETURN_SYMBOL => {
             if let Some([_, result]) = atom_into_array(body) {
                 // FIXME: check return arguments size
-                vec![InterpretedAtom(result, bindings)]
+                vec![InterpretedAtom(result, bindings, Status::Final)]
             } else {
                 panic!("Unexpected state");
             }
         },
         _ if is_embedded_op(&body) => {
-            let mut result = interpret_atom_root(space, InterpretedAtom(body, bindings), false);
+            let mut result = interpret_nested_atom(context, body, bindings, vars);
             if result.len() == 1 {
-                let InterpretedAtom(r, b) = result.pop().unwrap();
-                vec![InterpretedAtom(Atom::expr([FUNCTION_SYMBOL, r, call]), b)]
+                let InterpretedAtom(r, b, _s) = result.pop().unwrap();
+                vec![InterpretedAtom(Atom::expr([FUNCTION_SYMBOL, r, call]), b, Status::InProgress)]
             } else {
                 result.into_iter()
-                    .map(|InterpretedAtom(r, b)| {
-                        InterpretedAtom(Atom::expr([FUNCTION_SYMBOL, r, call.clone()]), b)
+                    .map(|InterpretedAtom(r, b, _s)| {
+                        InterpretedAtom(Atom::expr([FUNCTION_SYMBOL, r, call.clone()]), b, Status::InProgress)
                     })
                 .collect()
             }
         },
         _ => {
-            let error = format!("function doesn't have return statement");
-            vec![InterpretedAtom(error_atom(call, error), bindings)]
+            let error = format!("function doesn't have return statement, last atom: {}", body);
+            vec![InterpretedAtom(error_atom(call, error), bindings, Status::Final)]
+        },
+    }
+}
+
+fn atom_into_interpreted_atom(atom: Atom) -> InterpretedAtom {
+    match atom {
+        Atom::Expression(_) => match atom_into_array(atom) {
+            Some([atom, bindings]) => {
+                match bindings.as_gnd::<Bindings>() {
+                    Some(bindings) => {
+                        // TODO: cloning is ineffective, but it is not possible
+                        // to convert grounded atom into internal value at the
+                        // moment
+                        InterpretedAtom(atom, bindings.clone(), Status::InProgress)
+                    },
+                    _ => panic!("Unexpected state: second item cannot be converted to Bindings"),
+                }
+            }
+            _ => panic!("Unexpected state: atom is not a pair"),
         },
+        _ => panic!("Unexpected state: atom is not an expression"),
     }
 }
 
-fn unify(bindings: Bindings, atom: &Atom, pattern: &Atom, then: &Atom, else_: &Atom) -> Vec<InterpretedAtom> {
+fn atom_as_interpreted_atom(atom: &Atom) -> (&Atom, &Bindings) {
+    match atom_as_slice(atom) {
+        Some([atom, bindings]) => {
+            match bindings.as_gnd::<Bindings>() {
+                Some(bindings) => {
+                    (atom, bindings)
+                },
+                _ => panic!("Unexpected state: second item cannot be converted to Bindings"),
+            }
+        }
+        _ => panic!("Unexpected state: atom is not a pair"),
+    }
+}
+
+fn interpreted_atom_into_atom(interpreted: InterpretedAtom) -> Atom {
+    let InterpretedAtom(atom, bindings, _status) = interpreted;
+    Atom::expr([atom, Atom::value(bindings)])
+}
+
+fn collapse_bind<'a, T: SpaceRef<'a>>(context: &InterpreterContext<'a, T>, bindings: Bindings, current: ExpressionAtom, finished: ExpressionAtom, vars: &Variables) -> Vec<InterpretedAtom> {
+    let mut current = current.into_children();
+    let mut finished = finished.into_children();
+    if current.is_empty() {
+        let result: Vec<Atom> = finished.into_iter()
+            .map(atom_into_interpreted_atom)
+            .map(|InterpretedAtom(atom, bindings, _status)| Atom::expr([atom, Atom::value(bindings)]))
+            .collect();
+        vec![InterpretedAtom(Atom::expr(result), bindings, Status::Final)]
+    } else {
+        let next = current.pop().unwrap();
+        let interpreted = atom_into_interpreted_atom(next);
+        let InterpretedAtom(atom, local_bindings, _status) = interpreted;
+        if is_embedded_op(&atom) {
+            interpret_nested_atom(context, atom, local_bindings, vars).into_iter()
+                .map(interpreted_atom_into_atom)
+                .for_each(|atom| current.push(atom));
+        } else {
+            finished.push(interpreted_atom_into_atom(InterpretedAtom(atom, local_bindings, Status::Final)));
+        }
+        vec![InterpretedAtom(Atom::expr([COLLAPSE_BIND, Atom::expr(current), Atom::expr(finished)]), bindings, Status::InProgress)]
+    }
+}
+
+fn superpose_bind(collapsed: ExpressionAtom) -> Vec<InterpretedAtom> {
+    collapsed.into_children().into_iter()
+        .map(atom_into_interpreted_atom)
+        .map(|InterpretedAtom(atom, bindings, _status)| {
+            InterpretedAtom(atom, bindings, Status::Final)
+        })
+        .collect()
+}
+
+fn unify(bindings: Bindings, atom: &Atom, pattern: &Atom, then: &Atom, else_: &Atom, vars: &Variables) -> Vec<InterpretedAtom> {
     // TODO: Should unify() be symmetrical or not. While it is symmetrical then
     // if variable is matched by variable then both variables have the same
     // priority. Thus interpreter can use any of them further. This sometimes
@@ -471,14 +658,20 @@ fn unify(bindings: Bindings, atom: &Atom, pattern: &Atom, then: &Atom, else_: &A
     // from car's argument is replaced.
     let matches: Vec<Bindings> = match_atoms(atom, pattern).collect();
     if matches.is_empty() {
+        let bindings = bindings.narrow_vars(vars);
         let result = apply_bindings_to_atom(else_, &bindings);
-        vec![InterpretedAtom(result, bindings)]
+        vec![InterpretedAtom(result, bindings, Status::Final)]
     } else {
         matches.into_iter()
             .flat_map(|b| {
-                let then = apply_bindings_to_atom(then, &b);
-                b.merge_v2(&bindings).into_iter().map(move |b| {
-                    InterpretedAtom(then.clone(), b)
+                let b = b.narrow_vars(vars);
+                b.merge_v2(&bindings).into_iter().filter_map(move |b| {
+                    if b.has_loops() {
+                        None
+                    } else {
+                        let then = apply_bindings_to_atom(then, &b);
+                        Some(InterpretedAtom(then, b, Status::Final))
+                    }
                 })
             })
         .collect()
@@ -487,12 +680,12 @@ fn unify(bindings: Bindings, atom: &Atom, pattern: &Atom, then: &Atom, else_: &A
 
 fn decons(bindings: Bindings, expr: ExpressionAtom) -> Vec<InterpretedAtom> {
     let result = match expr.children().len() {
-        0 => InterpretedAtom(Atom::expr([]), bindings),
+        0 => InterpretedAtom(Atom::expr([]), bindings, Status::Final),
         _ => {
             let mut children = expr.into_children();
             let head = children.remove(0);
             let tail = children;
-            InterpretedAtom(Atom::expr([head, Atom::expr(tail)]), bindings)
+            InterpretedAtom(Atom::expr([head, Atom::expr(tail)]), bindings, Status::Final)
         },
     };
     vec![result]
@@ -501,7 +694,7 @@ fn decons(bindings: Bindings, expr: ExpressionAtom) -> Vec<InterpretedAtom> {
 fn cons(bindings: Bindings, head: Atom, tail: ExpressionAtom) -> Vec<InterpretedAtom> {
     let mut children = vec![head];
     children.extend(tail.into_children());
-    vec![InterpretedAtom(Atom::expr(children), bindings)]
+    vec![InterpretedAtom(Atom::expr(children), bindings, Status::Final)]
 }
 
 #[cfg(test)]
@@ -511,42 +704,42 @@ mod tests {
 
     #[test]
     fn interpret_atom_evaluate_incorrect_args() {
-        assert_eq!(interpret_atom(&space(""), atom("(eval)", bind!{})),
-            vec![InterpretedAtom(expr!("Error" ("eval") "expected: (eval <atom>), found: (eval)"), bind!{})]);
-        assert_eq!(interpret_atom(&space(""), atom("(eval a b)", bind!{})),
-            vec![InterpretedAtom(expr!("Error" ("eval" "a" "b") "expected: (eval <atom>), found: (eval a b)"), bind!{})]);
+        assert_eq!(call_interpret_atom(&space(""), &metta_atom("(eval)")),
+            vec![InterpretedAtom(expr!("Error" ("eval") "expected: (eval <atom>), found: (eval)"), bind!{}, Status::Final)]);
+        assert_eq!(call_interpret_atom(&space(""), &metta_atom("(eval a b)")),
+            vec![InterpretedAtom(expr!("Error" ("eval" "a" "b") "expected: (eval <atom>), found: (eval a b)"), bind!{}, Status::Final)]);
     }
 
     #[test]
     fn interpret_atom_evaluate_atom() {
-        let result = interpret_atom(&space("(= a b)"), atom("(eval a)", bind!{}));
-        assert_eq!(result, vec![atom("b", bind!{})]);
+        let result = call_interpret_atom(&space("(= a b)"), &metta_atom("(eval a)"));
+        assert_eq!(result, vec![atom("b", bind!{}, Status::Final)]);
     }
 
     #[test]
     fn interpret_atom_evaluate_atom_no_definition() {
-        let result = interpret_atom(&space(""), atom("(eval a)", bind!{}));
-        assert_eq!(result, vec![atom("NotReducible", bind!{})]);
+        let result = call_interpret_atom(&space(""), &metta_atom("(eval a)"));
+        assert_eq!(result, vec![atom("NotReducible", bind!{}, Status::Final)]);
     }
 
     #[test]
     fn interpret_atom_evaluate_empty_expression() {
-        let result = interpret_atom(&space(""), atom("(eval ())", bind!{}));
-        assert_eq!(result, vec![atom("NotReducible", bind!{})]);
+        let result = call_interpret_atom(&space(""), &metta_atom("(eval ())"));
+        assert_eq!(result, vec![atom("NotReducible", bind!{}, Status::Final)]);
     }
 
     #[test]
     fn interpret_atom_evaluate_grounded_value() {
-        let result = interpret_atom(&space(""), InterpretedAtom(expr!("eval" {6}), bind!{}));
-        assert_eq!(result, vec![atom("NotReducible", bind!{})]);
+        let result = call_interpret_atom(&space(""), &expr!("eval" {6}));
+        assert_eq!(result, vec![atom("NotReducible", bind!{}, Status::Final)]);
     }
 
 
     #[test]
     fn interpret_atom_evaluate_pure_expression() {
         let space = space("(= (foo $a B) $a)");
-        let result = interpret_atom(&space, atom("(eval (foo A $b))", bind!{}));
-        assert_eq!(result, vec![atom("A", bind!{})]);
+        let result = call_interpret_atom(&space, &metta_atom("(eval (foo A $b))"));
+        assert_eq!(result, vec![atom("A", bind!{ b: expr!("B") }, Status::Final)]);
     }
 
     #[test]
@@ -556,87 +749,87 @@ mod tests {
             (= color green)
             (= color blue)
         ");
-        let result = interpret_atom(&space, atom("(eval color)", bind!{}));
+        let result = call_interpret_atom(&space, &metta_atom("(eval color)"));
         assert_eq_no_order!(result, vec![
-            atom("red", bind!{}),
-            atom("green", bind!{}),
-            atom("blue", bind!{})
+            atom("red", bind!{}, Status::Final),
+            atom("green", bind!{}, Status::Final),
+            atom("blue", bind!{}, Status::Final)
         ]);
     }
 
     #[test]
     fn interpret_atom_evaluate_pure_expression_no_definition() {
-        let result = interpret_atom(&space(""), atom("(eval (foo A))", bind!{}));
-        assert_eq!(result, vec![atom("NotReducible", bind!{})]);
+        let result = call_interpret_atom(&space(""), &metta_atom("(eval (foo A))"));
+        assert_eq!(result, vec![atom("NotReducible", bind!{}, Status::Final)]);
     }
 
     #[test]
     fn interpret_atom_evaluate_pure_expression_variable_name_conflict() {
         let space = space("(= (foo ($W)) True)");
-        let result = interpret_atom(&space, atom("(eval (foo $W))", bind!{}));
+        let result = call_interpret_atom(&space, &metta_atom("(eval (foo $W))"));
         assert_eq!(result[0].0, sym!("True"));
     }
 
     #[test]
     fn interpret_atom_evaluate_grounded_expression() {
-        let result = interpret_atom(&space(""), InterpretedAtom(expr!("eval" ({MulXUndefinedType(7)} {6})), bind!{}));
-        assert_eq!(result, vec![InterpretedAtom(expr!({42}), bind!{})]);
+        let result = call_interpret_atom(&space(""), &expr!("eval" ({MulXUndefinedType(7)} {6})));
+        assert_eq!(result, vec![InterpretedAtom(expr!({42}), bind!{}, Status::Final)]);
     }
 
     #[test]
     fn interpret_atom_evaluate_grounded_expression_empty() {
-        let result = interpret_atom(&space(""), InterpretedAtom(expr!("eval" ({ReturnNothing()} {6})), bind!{}));
+        let result = call_interpret_atom(&space(""), &expr!("eval" ({ReturnNothing()} {6})));
         assert_eq!(result, vec![]);
     }
 
     #[test]
     fn interpret_atom_evaluate_grounded_expression_noreduce() {
-        let result = interpret_atom(&space(""), InterpretedAtom(expr!("eval" ({NonReducible()} {6})), bind!{}));
-        assert_eq!(result, vec![InterpretedAtom(expr!("NotReducible"), bind!{})]);
+        let result = call_interpret_atom(&space(""), &expr!("eval" ({NonReducible()} {6})));
+        assert_eq!(result, vec![InterpretedAtom(expr!("NotReducible"), bind!{}, Status::Final)]);
     }
 
     #[test]
     fn interpret_atom_evaluate_grounded_expression_error() {
-        let result = interpret_atom(&space(""), InterpretedAtom(expr!("eval" ({ThrowError()} {"Test error"})), bind!{}));
-        assert_eq!(result, vec![InterpretedAtom(expr!("Error" ({ThrowError()} {"Test error"}) "Test error"), bind!{})]);
+        let result = call_interpret_atom(&space(""), &expr!("eval" ({ThrowError()} {"Test error"})));
+        assert_eq!(result, vec![InterpretedAtom(expr!("Error" ({ThrowError()} {"Test error"}) "Test error"), bind!{}, Status::Final)]);
     }
 
 
     #[test]
     fn interpret_atom_chain_incorrect_args() {
-        assert_eq!(interpret_atom(&space(""), atom("(chain n $v t o)", bind!{})),
-            vec![InterpretedAtom(expr!("Error" ("chain" "n" v "t" "o") "expected: (chain <nested> (: <var> Variable) <templ>), found: (chain n $v t o)"), bind!{})]);
-        assert_eq!(interpret_atom(&space(""), atom("(chain n v t)", bind!{})),
-            vec![InterpretedAtom(expr!("Error" ("chain" "n" "v" "t") "expected: (chain <nested> (: <var> Variable) <templ>), found: (chain n v t)"), bind!{})]);
-        assert_eq!(interpret_atom(&space(""), atom("(chain n $v)", bind!{})),
-            vec![InterpretedAtom(expr!("Error" ("chain" "n" v) "expected: (chain <nested> (: <var> Variable) <templ>), found: (chain n $v)"), bind!{})]);
+        assert_eq!(call_interpret_atom(&space(""), &metta_atom("(chain n $v t o)")),
+            vec![InterpretedAtom(expr!("Error" ("chain" "n" v "t" "o") "expected: (chain <nested> (: <var> Variable) <templ>), found: (chain n $v t o)"), bind!{}, Status::Final)]);
+        assert_eq!(call_interpret_atom(&space(""), &metta_atom("(chain n v t)")),
+            vec![InterpretedAtom(expr!("Error" ("chain" "n" "v" "t") "expected: (chain <nested> (: <var> Variable) <templ>), found: (chain n v t)"), bind!{}, Status::Final)]);
+        assert_eq!(call_interpret_atom(&space(""), &metta_atom("(chain n $v)")),
+            vec![InterpretedAtom(expr!("Error" ("chain" "n" v) "expected: (chain <nested> (: <var> Variable) <templ>), found: (chain n $v)"), bind!{}, Status::Final)]);
     }
 
     #[test]
     fn interpret_atom_chain_atom() {
-        let result = interpret_atom(&space(""), InterpretedAtom(expr!("chain" ("A" () {6} y) x ("bar" x)), bind!{}));
-        assert_eq!(result, vec![InterpretedAtom(expr!("bar" ("A" () {6} y)), bind!{})]);
+        let result = call_interpret_atom(&space(""), &expr!("chain" ("A" () {6} y) x ("bar" x)));
+        assert_eq!(result, vec![InterpretedAtom(expr!("bar" ("A" () {6} y)), bind!{}, Status::InProgress)]);
     }
 
 
     #[test]
     fn interpret_atom_chain_evaluation() {
         let space = space("(= (foo $a B) $a)");
-        let result = interpret_atom(&space, atom("(chain (eval (foo A $b)) $x (bar $x))", bind!{}));
-        assert_eq!(result, vec![atom("(bar A)", bind!{})]);
+        let result = call_interpret_atom(&space, &metta_atom("(chain (eval (foo A $b)) $x (bar $x))"));
+        assert_eq!(result, vec![atom("(bar A)", bind!{ b: expr!("B") }, Status::InProgress)]);
     }
 
     #[test]
     fn interpret_atom_chain_nested_evaluation() {
         let space = space("(= (foo $a B) $a)");
-        let result = interpret_atom(&space, atom("(chain (chain (eval (foo A $b)) $x (bar $x)) $y (baz $y))", bind!{}));
-        assert_eq!(result, vec![atom("(baz (bar A))", bind!{})]);
+        let result = call_interpret_atom(&space, &metta_atom("(chain (chain (eval (foo A $b)) $x (bar $x)) $y (baz $y))"));
+        assert_eq!(result, vec![atom("(chain (bar A) $y (baz $y))", bind!{ b: expr!("B") }, Status::InProgress)]);
     }
 
     #[test]
     fn interpret_atom_chain_nested_value() {
-        let result = interpret_atom(&space(""), atom("(chain (chain A $x (bar $x)) $y (baz $y))", bind!{}));
-        assert_eq!(result, vec![atom("(baz (bar A))", bind!{})]);
+        let result = call_interpret_atom(&space(""), &metta_atom("(chain (chain A $x (bar $x)) $y (baz $y))"));
+        assert_eq!(result, vec![atom("(chain (bar A) $y (baz $y))", bind!{}, Status::InProgress)]);
     }
 
     #[test]
@@ -646,97 +839,97 @@ mod tests {
             (= (color) green)
             (= (color) blue)
         ");
-        let result = interpret_atom(&space, atom("(chain (eval (color)) $x (bar $x))", bind!{}));
+        let result = call_interpret_atom(&space, &metta_atom("(chain (eval (color)) $x (bar $x))"));
         assert_eq_no_order!(result, vec![
-            atom("(bar red)", bind!{}),
-            atom("(bar green)", bind!{}),
-            atom("(bar blue)", bind!{})
+            atom("(bar red)", bind!{}, Status::InProgress),
+            atom("(bar green)", bind!{}, Status::InProgress),
+            atom("(bar blue)", bind!{}, Status::InProgress)
         ]);
     }
 
     #[test]
     fn interpret_atom_chain_return() {
-        let result = interpret_atom(&space(""), atom("(chain Empty $x (bar $x))", bind!{}));
-        assert_eq!(result, vec![atom("(bar Empty)", bind!{})]);
+        let result = call_interpret_atom(&space(""), &metta_atom("(chain Empty $x (bar $x))"));
+        assert_eq!(result, vec![atom("(bar Empty)", bind!{}, Status::InProgress)]);
     }
 
 
     #[test]
     fn interpret_atom_match_incorrect_args() {
-        assert_eq!(interpret_atom(&space(""), atom("(unify a p t e o)", bind!{})),
-            vec![InterpretedAtom(expr!("Error" ("unify" "a" "p" "t" "e" "o") "expected: (unify <atom> <pattern> <then> <else>), found: (unify a p t e o)"), bind!{})]);
-        assert_eq!(interpret_atom(&space(""), atom("(unify a p t)", bind!{})),
-            vec![InterpretedAtom(expr!("Error" ("unify" "a" "p" "t") "expected: (unify <atom> <pattern> <then> <else>), found: (unify a p t)"), bind!{})]);
+        assert_eq!(call_interpret_atom(&space(""), &metta_atom("(unify a p t e o)")),
+            vec![InterpretedAtom(expr!("Error" ("unify" "a" "p" "t" "e" "o") "expected: (unify <atom> <pattern> <then> <else>), found: (unify a p t e o)"), bind!{}, Status::Final)]);
+        assert_eq!(call_interpret_atom(&space(""), &metta_atom("(unify a p t)")),
+            vec![InterpretedAtom(expr!("Error" ("unify" "a" "p" "t") "expected: (unify <atom> <pattern> <then> <else>), found: (unify a p t)"), bind!{}, Status::Final)]);
     }
 
     #[test]
     fn interpret_atom_match_then() {
-        let result = interpret_atom(&space(""), atom("(unify (A $b) ($a B) ($a $b) Empty)", bind!{}));
-        assert_eq!(result, vec![atom("(A B)", bind!{})]);
+        let result = call_interpret_atom(&space(""), &metta_atom("(unify (A $b) ($a B) ($a $b) Empty)"));
+        assert_eq!(result, vec![atom("(A B)", bind!{ a: expr!("A"), b: expr!("B") }, Status::Final)]);
     }
 
     #[test]
     fn interpret_atom_match_else() {
-        let result = interpret_atom(&space(""), atom("(unify (A $b C) ($a B D) ($a $b) Empty)", bind!{}));
-        assert_eq!(result, vec![atom("Empty", bind!{})]);
+        let result = call_interpret_atom(&space(""), &metta_atom("(unify (A $b C) ($a B D) ($a $b) Empty)"));
+        assert_eq!(result, vec![atom("Empty", bind!{}, Status::Final)]);
     }
 
 
     #[test]
     fn interpret_atom_decons_incorrect_args() {
-        assert_eq!(interpret_atom(&space(""), atom("(decons a)", bind!{})),
-            vec![InterpretedAtom(expr!("Error" ("decons" "a") "expected: (decons (: <expr> Expression)), found: (decons a)"), bind!{})]);
-        assert_eq!(interpret_atom(&space(""), atom("(decons (a) (b))", bind!{})),
-            vec![InterpretedAtom(expr!("Error" ("decons" ("a") ("b")) "expected: (decons (: <expr> Expression)), found: (decons (a) (b))"), bind!{})]);
-        assert_eq!(interpret_atom(&space(""), atom("(decons)", bind!{})),
-            vec![InterpretedAtom(expr!("Error" ("decons") "expected: (decons (: <expr> Expression)), found: (decons)"), bind!{})]);
+        assert_eq!(call_interpret_atom(&space(""), &metta_atom("(decons a)")),
+            vec![InterpretedAtom(expr!("Error" ("decons" "a") "expected: (decons (: <expr> Expression)), found: (decons a)"), bind!{}, Status::Final)]);
+        assert_eq!(call_interpret_atom(&space(""), &metta_atom("(decons (a) (b))")),
+            vec![InterpretedAtom(expr!("Error" ("decons" ("a") ("b")) "expected: (decons (: <expr> Expression)), found: (decons (a) (b))"), bind!{}, Status::Final)]);
+        assert_eq!(call_interpret_atom(&space(""), &metta_atom("(decons)")),
+            vec![InterpretedAtom(expr!("Error" ("decons") "expected: (decons (: <expr> Expression)), found: (decons)"), bind!{}, Status::Final)]);
     }
 
     #[test]
     fn interpret_atom_decons_empty() {
-        let result = interpret_atom(&space(""), atom("(decons ())", bind!{}));
-        assert_eq!(result, vec![InterpretedAtom(expr!("Error" ("decons" ()) "expected: (decons (: <expr> Expression)), found: (decons ())"), bind!{})]);
+        let result = call_interpret_atom(&space(""), &metta_atom("(decons ())"));
+        assert_eq!(result, vec![InterpretedAtom(expr!("Error" ("decons" ()) "expected: (decons (: <expr> Expression)), found: (decons ())"), bind!{}, Status::Final)]);
     }
 
     #[test]
     fn interpret_atom_decons_single() {
-        let result = interpret_atom(&space(""), atom("(decons (a))", bind!{}));
-        assert_eq!(result, vec![atom("(a ())", bind!{})]);
+        let result = call_interpret_atom(&space(""), &metta_atom("(decons (a))"));
+        assert_eq!(result, vec![atom("(a ())", bind!{}, Status::Final)]);
     }
 
     #[test]
     fn interpret_atom_decons_list() {
-        let result = interpret_atom(&space(""), atom("(decons (a b c))", bind!{}));
-        assert_eq!(result, vec![atom("(a (b c))", bind!{})]);
+        let result = call_interpret_atom(&space(""), &metta_atom("(decons (a b c))"));
+        assert_eq!(result, vec![atom("(a (b c))", bind!{}, Status::Final)]);
     }
 
 
     #[test]
     fn interpret_atom_cons_incorrect_args() {
-        assert_eq!(interpret_atom(&space(""), atom("(cons a (e) o)", bind!{})),
-            vec![InterpretedAtom(expr!("Error" ("cons" "a" ("e") "o") "expected: (cons <head> (: <tail> Expression)), found: (cons a (e) o)"), bind!{})]);
-        assert_eq!(interpret_atom(&space(""), atom("(cons a e)", bind!{})),
-            vec![InterpretedAtom(expr!("Error" ("cons" "a" "e") "expected: (cons <head> (: <tail> Expression)), found: (cons a e)"), bind!{})]);
-        assert_eq!(interpret_atom(&space(""), atom("(cons a)", bind!{})),
-            vec![InterpretedAtom(expr!("Error" ("cons" "a") "expected: (cons <head> (: <tail> Expression)), found: (cons a)"), bind!{})]);
+        assert_eq!(call_interpret_atom(&space(""), &metta_atom("(cons a (e) o)")),
+            vec![InterpretedAtom(expr!("Error" ("cons" "a" ("e") "o") "expected: (cons <head> (: <tail> Expression)), found: (cons a (e) o)"), bind!{}, Status::Final)]);
+        assert_eq!(call_interpret_atom(&space(""), &metta_atom("(cons a e)")),
+            vec![InterpretedAtom(expr!("Error" ("cons" "a" "e") "expected: (cons <head> (: <tail> Expression)), found: (cons a e)"), bind!{}, Status::Final)]);
+        assert_eq!(call_interpret_atom(&space(""), &metta_atom("(cons a)")),
+            vec![InterpretedAtom(expr!("Error" ("cons" "a") "expected: (cons <head> (: <tail> Expression)), found: (cons a)"), bind!{}, Status::Final)]);
     }
 
     #[test]
     fn interpret_atom_cons_empty() {
-        let result = interpret_atom(&space(""), atom("(cons a ())", bind!{}));
-        assert_eq!(result, vec![atom("(a)", bind!{})]);
+        let result = call_interpret_atom(&space(""), &metta_atom("(cons a ())"));
+        assert_eq!(result, vec![atom("(a)", bind!{}, Status::Final)]);
     }
 
     #[test]
     fn interpret_atom_cons_single() {
-        let result = interpret_atom(&space(""), atom("(cons a (b))", bind!{}));
-        assert_eq!(result, vec![atom("(a b)", bind!{})]);
+        let result = call_interpret_atom(&space(""), &metta_atom("(cons a (b))"));
+        assert_eq!(result, vec![atom("(a b)", bind!{}, Status::Final)]);
     }
 
     #[test]
     fn interpret_atom_cons_list() {
-        let result = interpret_atom(&space(""), atom("(cons a (b c))", bind!{}));
-        assert_eq!(result, vec![atom("(a b c)", bind!{})]);
+        let result = call_interpret_atom(&space(""), &metta_atom("(cons a (b c))"));
+        assert_eq!(result, vec![atom("(a b c)", bind!{}, Status::Final)]);
     }
 
     #[test]
@@ -798,14 +991,20 @@ mod tests {
     }
 
 
-    fn atom(text: &str, bindings: Bindings) -> InterpretedAtom {
-        InterpretedAtom(metta_atom(text), bindings)
+    fn atom(text: &str, bindings: Bindings, status: Status) -> InterpretedAtom {
+        InterpretedAtom(metta_atom(text), bindings, status)
     }
 
     fn space(text: &str) -> GroundingSpace {
         metta_space(text)
     }
 
+    fn call_interpret_atom<'a, T: SpaceRef<'a>>(space: T, atom: &Atom) -> Vec<InterpretedAtom> {
+        let mut state = interpret_init(space, atom);
+        let interpreted = state.pop().unwrap();
+        interpret_root_atom(&state.context, interpreted)
+    }
+
     #[derive(PartialEq, Clone, Debug)]
     struct ThrowError();
 
diff --git a/lib/src/metta/mod.rs b/lib/src/metta/mod.rs
index b9df36ee3..f664ef405 100644
--- a/lib/src/metta/mod.rs
+++ b/lib/src/metta/mod.rs
@@ -37,6 +37,8 @@ pub const DECONS_SYMBOL : Atom = sym!("decons");
 pub const CONS_SYMBOL : Atom = sym!("cons");
 pub const FUNCTION_SYMBOL : Atom = sym!("function");
 pub const RETURN_SYMBOL : Atom = sym!("return");
+pub const COLLAPSE_BIND : Atom = sym!("collapse-bind");
+pub const SUPERPOSE_BIND : Atom = sym!("superpose-bind");
 
 pub const INTERPRET_SYMBOL : Atom = sym!("interpret");
 
diff --git a/lib/src/metta/runner/stdlib.metta b/lib/src/metta/runner/stdlib.metta
index ead35aaaf..538c9ce3c 100644
--- a/lib/src/metta/runner/stdlib.metta
+++ b/lib/src/metta/runner/stdlib.metta
@@ -9,6 +9,8 @@
 (: unify (-> Atom Atom Atom Atom Atom))
 (: cons (-> Atom Atom Atom))
 (: decons (-> Atom Atom))
+(: collapse-bind (-> Atom Atom))
+(: superpose-bind (-> Atom Atom))
 
 (: id (-> Atom Atom))
 (= (id $x) $x)
@@ -77,31 +79,36 @@
           (return $then)
           (unify $type1 $type2 (return $then) (return $else)) ))))))))))
 
+(= (first-from-pair $pair)
+  (function
+    (unify $pair ($first $second)
+      (return $first)
+      (return (Error (first-from-pair $pair) "incorrect pair format")))))
+
+(= (match-type-or $folded $next $type)
+  (function
+    (chain (eval (match-types $next $type True False)) $matched
+      (chain (eval (or $folded $matched)) $or (return $or)) )))
+
 (= (type-cast $atom $type $space)
   (function (chain (eval (get-metatype $atom)) $meta
     (eval (if-equal $type $meta
       (return $atom)
-      ; TODO: the proper way to get types is something like
-      ; `(collapse (get-type <atom> <space>))` but it leads to the infinite
-      ; recursion because interpreter called by `collapse` evaluates
-      ; `type-cast` again.
-      (chain (eval (collapse-get-type $atom $space)) $actual-types
-        (chain (eval (foldl-atom $actual-types False
-          $a $b (chain (eval (match-types $b $type True False)) $is-b-comp
-            (chain (eval (or $a $is-b-comp)) $or $or) ))) $is-some-comp
-          (eval (if $is-some-comp
-            (return $atom)
-            (return (Error $atom BadType)) )))))))))
-
+      (chain (eval (collapse-bind (eval (get-type $atom $space)))) $collapsed
+        (chain (eval (map-atom $collapsed $pair (eval (first-from-pair $pair)))) $actual-types
+            (chain (eval (foldl-atom $actual-types False $a $b (eval (match-type-or $a $b $type)))) $is-some-comp
+              (eval (if $is-some-comp
+                (return $atom)
+                (return (Error $atom BadType)) ))))))))))
 
 (= (is-function $type)
   (function (chain (eval (get-metatype $type)) $meta
     (eval (switch ($type $meta) (
-      (($_ Expression)
+      (($type Expression)
         (eval (if-decons $type $head $_tail
           (unify $head -> (return True) (return False))
           (return (Error (is-function $type) "is-function non-empty expression as an argument")) )))
-      ($_ (return False))
+      (($type $meta) (return False))
     ))))))
 
 (: filter-atom (-> Expression Variable Atom Expression))
@@ -133,6 +140,26 @@
           (chain (eval (foldl-atom $tail $head-folded $a $b $op)) $res (return $res)) )))
     (return $init) ))))
 
+(: divide-errors (-> Expression Expression Expression))
+(= (divide-errors $succ-err $res)
+  (function (unify $succ-err ($suc $err)
+    (unify $res ($a $_b)
+      (eval (if-error $a
+        (chain (cons $res $err) $err' (return ($suc $err')))
+        (chain (cons $res $suc) $suc' (return ($suc' $err))) ))
+      (return $succ-err))
+    (return $succ-err) )))
+
+(= (check-alternatives $atom)
+  (function
+    (chain (collapse-bind $atom) $collapsed
+      (chain (eval (foldl-atom $collapsed (() ()) $succ-err $res
+        (eval (divide-errors $succ-err $res)))) $divided
+        (unify $divided ($success $error)
+          (chain (eval (if-equal $success () $error $success)) $filtered
+            (chain (superpose-bind $filtered) $ret (return $ret)) )
+          (return (Error (check-alternatives $atom) "list of results was not filtered correctly")) )))))
+
 (= (interpret $atom $type $space)
   (function (chain (eval (get-metatype $atom)) $meta
     (eval (if-equal $type Atom
@@ -140,13 +167,13 @@
       (eval (if-equal $type $meta
         (return $atom)
         (eval (switch ($type $meta) (
-          (($_type Variable) (return $atom))
-          (($_type Symbol)
+          (($type Variable) (return $atom))
+          (($type Symbol)
             (chain (eval (type-cast $atom $type $space)) $ret (return $ret)))
-          (($_type Grounded)
+          (($type Grounded)
             (chain (eval (type-cast $atom $type $space)) $ret (return $ret)))
-          (($_type Expression)
-            (chain (eval (interpret-expression $atom $type $space)) $ret (return $ret)))
+          (($type Expression)
+            (chain (eval (check-alternatives (eval (interpret-expression $atom $type $space)))) $ret (return $ret)))
         ))))))))))
 
 (= (interpret-expression $atom $type $space)
@@ -236,6 +263,10 @@
 (= (and True False) False)
 (= (and True True) True)
 
+(: not (-> Bool Bool))
+(= (not True) False)
+(= (not False) True)
+
 (: match (-> Atom Atom Atom %Undefined%))
 (= (match $space $pattern $template)
   (unify $pattern $space $template Empty))
diff --git a/lib/src/metta/runner/stdlib2.rs b/lib/src/metta/runner/stdlib2.rs
index 485adbd08..7230423d5 100644
--- a/lib/src/metta/runner/stdlib2.rs
+++ b/lib/src/metta/runner/stdlib2.rs
@@ -65,38 +65,6 @@ impl Grounded for GetTypeOp {
     }
 }
 
-#[derive(Clone, PartialEq, Debug)]
-pub struct CollapseGetTypeOp {}
-
-impl Display for CollapseGetTypeOp {
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        write!(f, "collapse-get-type")
-    }
-}
-
-impl Grounded for CollapseGetTypeOp {
-    fn type_(&self) -> Atom {
-        Atom::expr([ARROW_SYMBOL, ATOM_TYPE_ATOM, ATOM_TYPE_ATOM, ATOM_TYPE_EXPRESSION])
-    }
-
-    fn execute(&self, args: &[Atom]) -> Result<Vec<Atom>, ExecError> {
-        let arg_error = || ExecError::from("get-type expects single atom as an argument");
-        let atom = args.get(0).ok_or_else(arg_error)?;
-        let space = args.get(1).ok_or_else(arg_error)?;
-        let space = Atom::as_gnd::<DynSpace>(space).ok_or("match expects a space as the first argument")?;
-        let types = get_atom_types(space, atom);
-        if types.is_empty() {
-            Ok(vec![Atom::expr([])])
-        } else {
-            Ok(vec![Atom::expr(types)])
-        }
-    }
-
-    fn match_(&self, other: &Atom) -> MatchResultIter {
-        match_by_equality(self, other)
-    }
-}
-
 #[derive(Clone, PartialEq, Debug)]
 pub struct IfEqualOp { }
 
@@ -307,7 +275,7 @@ impl Grounded for CollapseOp {
         let atom = args.get(0).ok_or_else(arg_error)?;
 
         // TODO: Calling interpreter inside the operation is not too good
-        // Could it be done via StepResult?
+        // Could it be done via returning atom for the further interpretation?
         let result = interpret_no_error(self.space.clone(), atom)?;
 
         Ok(vec![Atom::expr(result)])
@@ -365,7 +333,9 @@ impl Grounded for CaseOp {
         log::debug!("CaseOp::execute: atom results: {:?}", results);
         let results = match results {
             Ok(results) if results.is_empty() =>
-                vec![switch(EMPTY_SYMBOL)],
+                // TODO: MINIMAL in minimal MeTTa we should use Empty in both
+                // places here and in (case ...) calls in code
+                vec![switch(VOID_SYMBOL)],
             Ok(results) =>
                 results.into_iter().map(|atom| switch(atom)).collect(),
             Err(err) => vec![Atom::expr([ERROR_SYMBOL, atom.clone(), Atom::sym(err)])],
@@ -389,8 +359,6 @@ pub fn register_common_tokens(metta: &Metta) {
 
     let get_type_op = Atom::gnd(GetTypeOp::new(space.clone()));
     tref.register_token(regex(r"get-type"), move |_| { get_type_op.clone() });
-    let collapse_get_type_op = Atom::gnd(CollapseGetTypeOp{});
-    tref.register_token(regex(r"collapse-get-type"), move |_| { collapse_get_type_op.clone() });
     let get_meta_type_op = Atom::gnd(stdlib::GetMetaTypeOp{});
     tref.register_token(regex(r"get-metatype"), move |_| { get_meta_type_op.clone() });
     let is_equivalent = Atom::gnd(IfEqualOp{});
@@ -409,6 +377,8 @@ pub fn register_common_tokens(metta: &Metta) {
     tref.register_token(regex(r"change-state!"), move |_| { change_state_op.clone() });
     let get_state_op = Atom::gnd(stdlib::GetStateOp{});
     tref.register_token(regex(r"get-state"), move |_| { get_state_op.clone() });
+    let nop_op = Atom::gnd(stdlib::NopOp{});
+    tref.register_token(regex(r"nop"), move |_| { nop_op.clone() });
 }
 
 pub fn register_runner_tokens(metta: &Metta) {
@@ -433,6 +403,8 @@ pub fn register_runner_tokens(metta: &Metta) {
     tref.register_token(regex(r"import!"), move |_| { import_op.clone() });
     let bind_op = Atom::gnd(stdlib::BindOp::new(tokenizer.clone()));
     tref.register_token(regex(r"bind!"), move |_| { bind_op.clone() });
+    let trace_op = Atom::gnd(stdlib::TraceOp{});
+    tref.register_token(regex(r"trace!"), move |_| { trace_op.clone() });
     // &self should be updated
     // TODO: adding &self might be done not by stdlib, but by MeTTa itself.
     // TODO: adding &self introduces self referencing and thus prevents space
@@ -464,6 +436,8 @@ pub fn register_rust_tokens(metta: &Metta) {
     tref.register_token(regex(r"/"), move |_| { div_op.clone() });
     let mod_op = Atom::gnd(ModOp{});
     tref.register_token(regex(r"%"), move |_| { mod_op.clone() });
+    let eq_op = Atom::gnd(stdlib::EqualOp{});
+    tref.register_token(regex(r"=="), move |_| { eq_op.clone() });
 
     metta.tokenizer().borrow_mut().move_front(&mut rust_tokens);
 }
@@ -542,13 +516,13 @@ mod tests {
 
     #[test]
     fn metta_case_empty() {
-        let result = run_program("!(case Empty ( (ok ok) (Empty nok) ))");
+        let result = run_program("!(case Empty ( (ok ok) (%void% nok) ))");
         assert_eq!(result, Ok(vec![vec![expr!("nok")]]));
-        let result = run_program("!(case (unify (C B) (C B) ok Empty) ( (ok ok) (Empty nok) ))");
+        let result = run_program("!(case (unify (C B) (C B) ok Empty) ( (ok ok) (%void% nok) ))");
         assert_eq!(result, Ok(vec![vec![expr!("ok")]]));
         let result = run_program("!(case (unify (B C) (C B) ok nok) ( (ok ok) (nok nok) ))");
         assert_eq!(result, Ok(vec![vec![expr!("nok")]]));
-        let result = run_program("!(case (match (B C) (C B) ok) ( (ok ok) (Empty nok) ))");
+        let result = run_program("!(case (match (B C) (C B) ok) ( (ok ok) (%void% nok) ))");
         assert_eq!(result, Ok(vec![vec![expr!("nok")]]));
     }
 
@@ -814,8 +788,6 @@ mod tests {
     #[test]
     fn test_frog_reasoning() {
         let program = "
-            (= (and True True) True)
-
             (= (is Fritz croaks) True)
             (= (is Fritz eats-flies) True)
 
diff --git a/lib/src/space/grounding.rs b/lib/src/space/grounding.rs
index 51970a524..818e95a9f 100644
--- a/lib/src/space/grounding.rs
+++ b/lib/src/space/grounding.rs
@@ -10,6 +10,7 @@ use crate::common::multitrie::{MultiTrie, TrieKey, TrieToken};
 
 use std::fmt::{Display, Debug};
 use std::collections::BTreeSet;
+use std::collections::HashSet;
 
 // Grounding space
 
@@ -268,7 +269,7 @@ impl GroundingSpace {
     fn single_query(&self, query: &Atom) -> BindingsSet {
         log::debug!("single_query: query: {}", query);
         let mut result = BindingsSet::empty();
-        let query_vars = query.iter().filter_type::<&VariableAtom>().collect();
+        let query_vars: HashSet<&VariableAtom> = query.iter().filter_type::<&VariableAtom>().collect();
         for i in self.index.get(&atom_to_trie_key(query)) {
             let next = self.content.get(*i).expect(format!("Index contains absent atom: key: {:?}, position: {}", query, i).as_str());
             let next = make_variables_unique(next.clone());
diff --git a/lib/tests/case.rs b/lib/tests/case.rs
index 8a5b2adf1..8c06219fd 100644
--- a/lib/tests/case.rs
+++ b/lib/tests/case.rs
@@ -37,7 +37,7 @@ fn test_case_operation() {
         ! (superpose (3 4 5))
         ! (superpose ())
     "));
-    assert_eq!(result, expected);
+    assert_eq_metta_results!(result, expected);
 
     let metta = Metta::new(Some(EnvBuilder::test_env()));
     let result = metta.run(SExprParser::new("
diff --git a/python/tests/test_minecraft.py b/python/tests/test_minecraft.py
index b692eb5b8..59ab807fe 100644
--- a/python/tests/test_minecraft.py
+++ b/python/tests/test_minecraft.py
@@ -94,18 +94,14 @@ def test_minecraft_planning_with_abstractions(self):
             (= (can-be-made inventory) False)
             (= (can-be-mined inventory) False)
 
-            (: if (-> Bool Atom Atom Atom))
-            (= (if True $then $else) $then)
-            (= (if False $then $else) $else)
-
             (= (make $x) (if (and ($x made-from $comp) ($x made-at $tool))
-                             (, (get $tool) (get $comp) (do-make $x $tool $comp)) nop))
+                             (, (get $tool) (get $comp) (do-make $x $tool $comp)) (empty)))
 
             (= (mine $x) (if (and ($x mined-using $tool) ($x mined-from $source))
-                             (, (get $tool) (find $source) (do-mine $x $source $tool)) nop))
+                             (, (get $tool) (find $source) (do-mine $x $source $tool)) (empty)))
 
-            (= (get $x) (if (and (not (in-inventory $x)) (can-be-mined $x)) (mine $x) nop))
-            (= (get $x) (if (and (not (in-inventory $x)) (can-be-made $x)) (make $x) nop))
+            (= (get $x) (if (and (not (in-inventory $x)) (can-be-mined $x)) (mine $x) (empty)))
+            (= (get $x) (if (and (not (in-inventory $x)) (can-be-made  $x)) (make $x) (empty)))
         ''')
 
         metta.run('!(get diamond)')