Repository: tweag/nickel
Pull request #553 (2022-01-06 19:16:12)

Fix/explicit destructuring typechecking
Update comments to remember where we are missing typecheck behaviours.
also fix typechecking of RHS in not typed context.


Patch:
diff --git a/src/cache.rs b/src/cache.rs
index 64f12e25..cc787268 100644
--- a/src/cache.rs
+++ b/src/cache.rs
@@ -5,10 +5,9 @@ use crate::parser::lexer::Lexer;
 use crate::position::TermPos;
 use crate::stdlib as nickel_stdlib;
 use crate::term::{RichTerm, Term};
-use crate::transform::import_resolution;
 use crate::typecheck;
 use crate::typecheck::{linearization::StubHost, type_check};
-use crate::{eval, parser, transform};
+use crate::{eval, parser, transformations};
 use codespan::{FileId, Files};
 use io::Read;
 use std::collections::hash_map;
@@ -444,7 +443,7 @@ impl Cache {
                     let CachedTerm {
                         term, parse_errs, ..
                     } = self.terms.remove(&file_id).unwrap();
-                    let term = transform::transform(term);
+                    let term = transformations::transform(term);
                     self.terms.insert(
                         file_id,
                         CachedTerm {
@@ -501,20 +500,23 @@ impl Cache {
                         Term::Record(ref mut map, _) => {
                             let map_res = std::mem::take(map)
                                 .into_iter()
-                                .map(|(id, t)| (id, transform::transform(t)))
+                                .map(|(id, t)| (id, transformations::transform(t)))
                                 .collect();
                             *map = map_res;
                         }
                         Term::RecRecord(ref mut map, ref mut dyn_fields, _) => {
                             let map_res = std::mem::take(map)
                                 .into_iter()
-                                .map(|(id, t)| (id, transform::transform(t)))
+                                .map(|(id, t)| (id, transformations::transform(t)))
                                 .collect();
 
                             let dyn_fields_res = std::mem::take(dyn_fields)
                                 .into_iter()
                                 .map(|(id_t, t)| {
-                                    (transform::transform(id_t), transform::transform(t))
+                                    (
+                                        transformations::transform(id_t),
+                                        transformations::transform(t),
+                                    )
                                 })
                                 .collect();
 
@@ -562,7 +564,7 @@ impl Cache {
                     let CachedTerm {
                         term, parse_errs, ..
                     } = self.terms.remove(&file_id).unwrap();
-                    let (term, pending) = import_resolution::resolve_imports(term, self)?;
+                    let (term, pending) = transformations::resolve_imports(term, self)?;
                     self.terms.insert(
                         file_id,
                         CachedTerm {
@@ -651,9 +653,9 @@ impl Cache {
         if errs.no_errors() {
             return Err(Error::ParseErrors(errs));
         }
-        let (term, pending) = import_resolution::resolve_imports(term, self)?;
+        let (term, pending) = transformations::resolve_imports(term, self)?;
         type_check(&term, global_env, self, StubHost::<(), _>::new())?;
-        let term = transform::transform(term);
+        let term = transformations::transform(term);
         Ok((term, pending))
     }
 
diff --git a/src/error.rs b/src/error.rs
index 0fe51de4..f5cf8410 100644
--- a/src/error.rs
+++ b/src/error.rs
@@ -9,7 +9,7 @@ use codespan_reporting::diagnostic::{Diagnostic, Label, LabelStyle};
 use lalrpop_util::ErrorRecovery;
 
 use crate::{
-    eval::callstack::CallStack,
+    eval::CallStack,
     identifier::Ident,
     label,
     label::ty_path,
diff --git a/src/eval/mod.rs b/src/eval.rs
similarity index 53%
rename from src/eval/mod.rs
rename to src/eval.rs
index f65bf14f..5b15db61 100644
--- a/src/eval/mod.rs
+++ b/src/eval.rs
@@ -1,5 +1,4 @@
 //! Evaluation of a Nickel term.
-//!
 //! The implementation of the Nickel abstract machine which evaluates a term. Note that this
 //! machine is not currently formalized somewhere and is just a convenient name to designate the
 //! current implementation.
@@ -93,19 +92,487 @@ use crate::{
     error::EvalError,
     identifier::Ident,
     mk_app,
+    operation::{continuate_operation, OperationCont},
+    position::RawSpan,
+    position::TermPos,
+    stack::Stack,
     term::{make as mk_term, BinaryOp, BindingType, MetaValue, RichTerm, StrChunk, Term, UnaryOp},
 };
+use codespan::FileId;
+use std::cell::{Ref, RefCell, RefMut};
+use std::rc::{Rc, Weak};
+
+/// The state of a thunk.
+///
+/// When created, a thunk is flagged as suspended. When accessed for the first time, a corresponding
+/// [`ThunkUpdateFrame`](./struct.ThunkUpdateFrame.html) is pushed on the stack and the thunk is
+/// flagged as black-hole. This prevents direct infinite recursions, since if a thunk is
+/// re-accessed while still in a black-hole state, we are sure that the evaluation will loop, and
+/// we can thus error out before overflowing the stack or looping forever. Finally, once the
+/// content of a thunk has been evaluated, the thunk is updated with the new value and flagged as
+/// evaluated, so that future accesses won't even push an update frame on the stack.
+#[derive(Copy, Clone, Eq, PartialEq, Debug)]
+pub enum ThunkState {
+    Blackholed,
+    Suspended,
+    Evaluated,
+}
+
+/// The mutable data stored inside a thunk.
+#[derive(Clone, Debug, PartialEq)]
+pub struct ThunkData {
+    inner: InnerThunkData,
+    state: ThunkState,
+}
+
+/// The part of [ThunkData] responsible for storing the closure itself. It can either be:
+/// - A standard thunk, that is destructively updated once and for all
+/// - A revertible thunk, that can be restored to its original expression. Used to implement
+/// recursive merging of records and overriding (see the [RFC
+/// overriding](https://github.com/tweag/nickel/pull/330))
+#[derive(Clone, Debug, PartialEq)]
+pub enum InnerThunkData {
+    Standard(Closure),
+    Revertible {
+        orig: Rc<Closure>,
+        cached: Rc<Closure>,
+    },
+}
+
+impl ThunkData {
+    /// Create new standard thunk data.
+    pub fn new(closure: Closure) -> Self {
+        ThunkData {
+            inner: InnerThunkData::Standard(closure),
+            state: ThunkState::Suspended,
+        }
+    }
+
+    /// Create new revertible thunk data.
+    pub fn new_rev(orig: Closure) -> Self {
+        let rc = Rc::new(orig);
+
+        ThunkData {
+            inner: InnerThunkData::Revertible {
+                orig: rc.clone(),
+                cached: rc,
+            },
+            state: ThunkState::Suspended,
+        }
+    }
+
+    /// Return a reference to the closure currently cached.
+    pub fn closure(&self) -> &Closure {
+        match self.inner {
+            InnerThunkData::Standard(ref closure) => closure,
+            InnerThunkData::Revertible { ref cached, .. } => cached,
+        }
+    }
+
+    /// Return a mutable reference to the closure currently cached.
+    pub fn closure_mut(&mut self) -> &mut Closure {
+        match self.inner {
+            InnerThunkData::Standard(ref mut closure) => closure,
+            InnerThunkData::Revertible { ref mut cached, .. } => Rc::make_mut(cached),
+        }
+    }
+
+    /// Consume the data and return the cached closure.
+    pub fn into_closure(self) -> Closure {
+        match self.inner {
+            InnerThunkData::Standard(closure) => closure,
+            InnerThunkData::Revertible { orig, cached } => {
+                std::mem::drop(orig);
+                Rc::try_unwrap(cached).unwrap_or_else(|rc| (*rc).clone())
+            }
+        }
+    }
+
+    /// Update the cached closure.
+    pub fn update(&mut self, new: Closure) {
+        match self.inner {
+            InnerThunkData::Standard(ref mut closure) => *closure = new,
+            InnerThunkData::Revertible { ref mut cached, .. } => *cached = Rc::new(new),
+        }
+
+        self.state = ThunkState::Evaluated;
+    }
+
+    /// Create fresh unevaluated thunk data from `self`, reverted to its original state before the
+    /// first update. For standard thunk data, the content is unchanged and the state is conserved:
+    /// in this case, `revert()` is the same as `clone()`.
+    pub fn revert(&self) -> Self {
+        match self.inner {
+            InnerThunkData::Standard(_) => self.clone(),
+            InnerThunkData::Revertible { ref orig, .. } => ThunkData {
+                inner: InnerThunkData::Revertible {
+                    orig: Rc::clone(orig),
+                    cached: Rc::clone(orig),
+                },
+                state: ThunkState::Suspended,
+            },
+        }
+    }
+}
+
+/// A thunk.
+///
+/// A thunk is a shared suspended computation. It is the primary device for the implementation of
+/// lazy evaluation.
+///
+/// For the implementation of recursive merging, some thunks need to be revertible, in the sense
+/// that we must be able to revert to the original expression before update. Those are called
+/// revertible thunks. Most expressions don't need revertible thunks as their evaluation will
+/// always give the same result, but some others, such as the ones containing recursive references
+/// inside a record may be invalidated by merging, and thus need to store the unaltered original
+/// expression. Those aspects are mainly handled in [InnerThunkData].
+#[derive(Clone, Debug, PartialEq)]
+pub struct Thunk {
+    data: Rc<RefCell<ThunkData>>,
+    ident_kind: IdentKind,
+}
+
+/// A black-holed thunk was accessed, which would lead to infinite recursion.
+#[derive(Clone, Copy, Debug, Eq, PartialEq)]
+pub struct BlackholedError;
+
+impl Thunk {
+    /// Create a new standard thunk.
+    pub fn new(closure: Closure, ident_kind: IdentKind) -> Self {
+        Thunk {
+            data: Rc::new(RefCell::new(ThunkData::new(closure))),
+            ident_kind,
+        }
+    }
+
+    /// Create a new revertible thunk.
+    pub fn new_rev(closure: Closure, ident_kind: IdentKind) -> Self {
+        Thunk {
+            data: Rc::new(RefCell::new(ThunkData::new_rev(closure))),
+            ident_kind,
+        }
+    }
+
+    pub fn state(&self) -> ThunkState {
+        self.data.borrow().state
+    }
+
+    /// Set the state to evaluated.
+    pub fn set_evaluated(&mut self) {
+        self.data.borrow_mut().state = ThunkState::Evaluated;
+    }
+
+    /// Generate an update frame from this thunk and set the state to `Blackholed`. Return an
+    /// error if the thunk was already black-holed.
+    pub fn mk_update_frame(&mut self) -> Result<ThunkUpdateFrame, BlackholedError> {
+        if self.data.borrow().state == ThunkState::Blackholed {
+            return Err(BlackholedError);
+        }
+
+        self.data.borrow_mut().state = ThunkState::Blackholed;
+
+        Ok(ThunkUpdateFrame {
+            data: Rc::downgrade(&self.data),
+            ident_kind: self.ident_kind,
+        })
+    }
+
+    /// Immutably borrow the inner closure. Panic if there is another active mutable borrow.
+    pub fn borrow(&self) -> Ref<'_, Closure> {
+        Ref::map(self.data.borrow(), |data| data.closure())
+    }
+
+    /// Mutably borrow the inner closure. Panic if there is any other active borrow.
+    pub fn borrow_mut(&mut self) -> RefMut<'_, Closure> {
+        RefMut::map(self.data.borrow_mut(), |data| data.closure_mut())
+    }
+
+    /// Get an owned clone of the inner closure.
+    pub fn get_owned(&self) -> Closure {
+        self.data.borrow().closure().clone()
+    }
+
+    pub fn ident_kind(&self) -> IdentKind {
+        self.ident_kind
+    }
+
+    /// Consume the thunk and return an owned closure. Avoid cloning if this thunk is the only
+    /// reference to the inner closure.
+    pub fn into_closure(self) -> Closure {
+        match Rc::try_unwrap(self.data) {
+            Ok(inner) => inner.into_inner().into_closure(),
+            Err(rc) => rc.borrow().closure().clone(),
+        }
+    }
+
+    /// Create a fresh unevaluated thunk from `self`, reverted to its original state before the
+    /// first update. For a standard thunk, the content is unchanged and the state is conserved: in
+    /// this case, `revert()` is the same as `clone()`.
+    pub fn revert(&self) -> Self {
+        Thunk {
+            data: Rc::new(RefCell::new(self.data.borrow().revert())),
+            ident_kind: self.ident_kind,
+        }
+    }
+}
+
+/// A thunk update frame.
+///
+/// A thunk update frame is put on the stack whenever a variable is entered, such that once this
+/// variable is evaluated, the corresponding thunk can be updated. It is similar to a thunk but it
+/// holds a weak reference to the inner closure, to avoid unnecessarily keeping the underlying
+/// closure alive.
+#[derive(Clone, Debug)]
+pub struct ThunkUpdateFrame {
+    data: Weak<RefCell<ThunkData>>,
+    ident_kind: IdentKind,
+}
+
+impl ThunkUpdateFrame {
+    /// Update the corresponding thunk with a closure. Set the state to `Evaluated`
+    ///
+    /// # Return
+    ///
+    /// - `true` if the thunk was successfully updated
+    /// - `false` if the corresponding closure has been dropped since
+    pub fn update(self, closure: Closure) -> bool {
+        if let Some(data) = Weak::upgrade(&self.data) {
+            data.borrow_mut().update(closure);
+            true
+        } else {
+            false
+        }
+    }
+}
+
+/// A call stack, saving the history of function calls.
+///
+/// In a lazy language like Nickel, there are no well delimited stack frames due to how function
+/// application is evaluated. Additional information about the history of function calls is thus
+/// stored in the call stack solely for better error reporting.
+#[derive(PartialEq, Clone, Default, Debug)]
+pub struct CallStack(pub Vec<StackElem>);
+
+/// Basic description of a function call. Used for error reporting.
+pub struct CallDescr {
+    /// The name of the called function, if any.
+    pub head: Option<Ident>,
+    /// The position of the application.
+    pub span: RawSpan,
+}
+
+/// A call stack element.
+#[derive(Debug, Clone, Eq, PartialEq)]
+pub enum StackElem {
+    /// A function body was entered. The position is the position of the original application.
+    Fun(TermPos),
+    /// An application was evaluated.
+    App(TermPos),
+    /// A variable was entered.
+    Var {
+        kind: IdentKind,
+        id: Ident,
+        pos: TermPos,
+    },
+    /// A record field was entered.
+    Field {
+        id: Ident,
+        pos_record: TermPos,
+        pos_field: TermPos,
+        pos_access: TermPos,
+    },
+}
+
+impl CallStack {
+    pub fn new() -> Self {
+        CallStack(Vec::new())
+    }
+
+    /// Push a marker to indicate that a var was entered.
+    pub fn enter_var(&mut self, kind: IdentKind, id: Ident, pos: TermPos) {
+        self.0.push(StackElem::Var { kind, id, pos });
+    }
+
+    /// Push a marker to indicate that an application was entered.
+    pub fn enter_app(&mut self, pos: TermPos) {
+        // We ignore application without positions, which have been generated by the interpreter.
+        if pos.is_def() {
+            self.0.push(StackElem::App(pos));
+        }
+    }
 
-pub mod callstack;
-pub mod lazy;
-pub mod merge;
-pub mod operation;
-pub mod stack;
+    /// Push a marker to indicate that during the evaluation an application, the function part was
+    /// finally evaluated to an expression of the form `fun x => body`, and that the body of this
+    /// function was entered.
+    pub fn enter_fun(&mut self, pos: TermPos) {
+        // We ignore application without positions, which have been generated by the interpreter.
+        if pos.is_def() {
+            self.0.push(StackElem::Fun(pos));
+        }
+    }
 
-use callstack::*;
-use lazy::*;
-use operation::{continuate_operation, OperationCont};
-use stack::Stack;
+    /// Push a marker to indicate that a record field was entered.
+    pub fn enter_field(
+        &mut self,
+        id: Ident,
+        pos_record: TermPos,
+        pos_field: TermPos,
+        pos_access: TermPos,
+    ) {
+        self.0.push(StackElem::Field {
+            id,
+            pos_record,
+            pos_field,
+            pos_access,
+        });
+    }
+
+    /// Process a raw callstack by aggregating elements belonging to the same call. Return a list
+    /// of call descriptions from the most nested/recent to the least nested/recent, together with
+    /// the last pending call, if any.
+    ///
+    /// Recall that when a call `f arg` is evaluated, the following events happen:
+    /// 1. `arg` is pushed on the evaluation stack.
+    /// 2. `f` is evaluated.
+    /// 3. Hopefully, the result of this evaluation is a function `Func(id, body)`. `arg` is popped
+    ///    from the stack, bound to `id` in the environment, and `body is entered`.
+    ///
+    /// For error reporting purpose, we want to be able to determine the chain of nested calls leading
+    /// to the current code path at any moment. To do so, the Nickel abstract machine maintains a
+    /// callstack via this basic mechanism:
+    /// 1. When an application is evaluated, push a marker with the position of the application on the callstack.
+    /// 2. When a function body is entered, push a marker with the position of the original application on the
+    ///    callstack.
+    /// 3. When a variable is evaluated, push a marker with its name and position on the callstack.
+    /// 4. When a record field is accessed, push a marker with its name and position on the
+    ///    callstack too.
+    ///
+    /// Both field and variable are useful to determine the name of a called function, when there
+    /// is one.  The resulting stack is not suited to be reported to the user for the following
+    /// reasons:
+    ///
+    /// 1. One call spans several items on the callstack. First the application is entered (pushing
+    ///    an `App`), then possibly variables or other application are evaluated until we
+    ///    eventually reach a function for the left hand side. Then body of this function is
+    ///    entered (pushing a `Fun`).
+    /// 2. Because of currying, multi-ary applications span several objects on the callstack.
+    ///    Typically, `(fun x y => x + y) arg1 arg2` spans two `App` and two `Fun` elements in the
+    ///    form `App1 App2 Fun2 Fun1`, where the position span of `App1` includes the position span
+    ///    of `App2`.  We want to group them as one call.
+    /// 3. The callstack includes calls to builtin contracts. These calls are inserted implicitly
+    ///    by the abstract machine and are not written explicitly by the user. Showing them is
+    ///    confusing and clutters the call chain, so we get rid of them too.
+    ///
+    /// This is the role of `group_by_calls`, which filter out unwanted elements and groups
+    /// callstack elements into atomic call elements represented by [`CallDescr`].
+    ///
+    /// The final call description list is reversed such that the most nested calls, which are
+    /// usually the most relevant to understand the error, are printed first.
+    ///
+    /// # Arguments
+    ///
+    /// - `contract_id`: the `FileId` of the source containing standard contracts, to filter their
+    ///   calls out.
+    pub fn group_by_calls(
+        self: &CallStack,
+        contract_id: FileId,
+    ) -> (Vec<CallDescr>, Option<CallDescr>) {
+        // We filter out calls and accesses made from within the builtin contracts, as well as
+        // generated variables introduced by program transformations.
+        let it = self.0.iter().filter(|elem| match elem {
+            StackElem::Var {id, ..} if id.is_generated() => false,
+            StackElem::Var{ pos: TermPos::Original(RawSpan { src_id, .. }), ..}
+            | StackElem::Var{pos: TermPos::Inherited(RawSpan { src_id, .. }), ..}
+            | StackElem::Fun(TermPos::Original(RawSpan { src_id, .. }))
+            | StackElem::Field {pos_access: TermPos::Original(RawSpan { src_id, .. }), ..}
+            | StackElem::Field {pos_access: TermPos::Inherited(RawSpan { src_id, .. }), ..}
+            | StackElem::App(TermPos::Original(RawSpan { src_id, .. }))
+            // We avoid applications (Fun/App) with inherited positions. Such calls include
+            // contracts applications which add confusing call items whose positions don't point to
+            // an actual call in the source.
+                if *src_id != contract_id =>
+            {
+                true
+            }
+            _ => false,
+        });
+
+        // We maintain a stack of active calls (whose head is being evaluated).  When encountering
+        // an identifier (variable or record field), we see if it could serve as a function name
+        // for the current active call. When a `Fun` is encountered, we check if this correspond to
+        // the current active call, and if it does, the call description is moved to a stack of
+        // processed calls.
+        //
+        // We also merge subcalls, in the sense that subcalls of larger calls are not considered
+        // separately. `app1` is a subcall of `app2` if the position of `app1` is included in the
+        // one of `app2` and the starting index is equal. We want `f a b c` to be reported as only
+        // one big call to `f` rather than three nested calls `f a`, `f a b`, and `f a b c`.
+        let mut pending: Vec<CallDescr> = Vec::new();
+        let mut entered: Vec<CallDescr> = Vec::new();
+
+        for elt in it {
+            match elt {
+                StackElem::Var { id, pos, .. }
+                | StackElem::Field {
+                    id,
+                    pos_access: pos,
+                    ..
+                } => {
+                    match pending.last_mut() {
+                        Some(CallDescr {
+                            head: ref mut head @ None,
+                            span: span_call,
+                        }) if pos.unwrap() <= *span_call => *head = Some(id.clone()),
+                        _ => (),
+                    };
+                }
+                StackElem::App(pos) => {
+                    let span = pos.unwrap();
+                    match pending.last() {
+                        Some(CallDescr {
+                            span: span_call, ..
+                        }) if span <= *span_call && span.start == span_call.start => (),
+                        _ => pending.push(CallDescr { head: None, span }),
+                    }
+                }
+                StackElem::Fun(pos) => {
+                    let span = pos.unwrap();
+                    if pending
+                        .last()
+                        .map(|cdescr| cdescr.span == span)
+                        .unwrap_or(false)
+                    {
+                        entered.push(pending.pop().unwrap());
+                    }
+                    // Otherwise, we are most probably entering a subcall () of the currently
+                    // active call (e.g. in an multi-ary application `f g h`, a subcall would be `f
+                    // g`). In any case, we do nothing.
+                }
+            }
+        }
+
+        entered.reverse();
+        (entered, pending.pop())
+    }
+
+    /// Return the length of the callstack. Wrapper for `callstack.0.len()`.
+    pub fn len(&self) -> usize {
+        self.0.len()
+    }
+
+    /// Truncate the callstack at a certain size. Used e.g. to quickly drop the elements introduced
+    /// during the strict evaluation of the operand of a primitive operator. Wrapper for
+    /// `callstack.0.truncate(len)`.
+    pub fn truncate(&mut self, len: usize) {
+        self.0.truncate(len)
+    }
+}
+
+impl From<CallStack> for Vec<StackElem> {
+    fn from(cs: CallStack) -> Self {
+        cs.0
+    }
+}
 
 /// Kind of an identifier.
 #[derive(Debug, PartialEq, Eq, Clone, Copy)]
@@ -168,6 +635,14 @@ pub fn env_add(env: &mut Environment, id: Ident, rt: RichTerm, local_env: Enviro
     env.insert(id, Thunk::new(closure, IdentKind::Let));
 }
 
+/// Determine if a thunk is worth being put on the stack for future update.
+///
+/// Typically, WHNFs and enriched values will not be evaluated to a simpler expression and are not
+/// worth updating.
+fn should_update(t: &Term) -> bool {
+    !t.is_whnf() && !t.is_metavalue()
+}
+
 /// Evaluate a Nickel term. Wrapper around [eval_closure](fn.eval_closure.html) that starts from an
 /// empty local environment and drops the final environment.
 pub fn eval<R>(
@@ -213,7 +688,7 @@ fn eval_deep_closure<R>(
 where
     R: ImportResolver,
 {
-    use crate::transform::fresh_var;
+    use crate::transformations::fresh_var;
 
     let var = fresh_var();
     // Desugar to let x = term in deepSeq x x
@@ -315,7 +790,7 @@ where
                 std::mem::drop(env); // thunk may be a 1RC pointer
 
                 if thunk.state() != ThunkState::Evaluated {
-                    if thunk.should_update() {
+                    if should_update(&thunk.borrow().body.term) {
                         match thunk.mk_update_frame() {
                             Ok(thunk_upd) => stack.push_thunk(thunk_upd),
                             Err(BlackholedError) => {
@@ -875,4 +1350,362 @@ pub fn subst(rt: RichTerm, global_env: &Environment, env: &Environment) -> RichT
 }
 
 #[cfg(test)]
-mod tests;
+mod tests {
+    use super::*;
+    use crate::cache::resolvers::{DummyResolver, SimpleResolver};
+    use crate::error::ImportError;
+    use crate::label::Label;
+    use crate::parser::{grammar, lexer};
+    use crate::term::make as mk_term;
+    use crate::term::{BinaryOp, StrChunk, UnaryOp};
+    use crate::transformations::resolve_imports;
+    use crate::{mk_app, mk_fun};
+    use codespan::Files;
+
+    /// Evaluate a term without import support.
+    fn eval_no_import(t: RichTerm) -> Result<Term, EvalError> {
+        eval(t, &Environment::new(), &mut DummyResolver {}).map(Term::from)
+    }
+
+    fn parse(s: &str) -> Option<RichTerm> {
+        let id = Files::new().add("<test>", String::from(s));
+
+        grammar::TermParser::new()
+            .parse_term(id, lexer::Lexer::new(&s))
+            .map(RichTerm::without_pos)
+            .map_err(|err| println!("{:?}", err))
+            .ok()
+    }
+
+    #[test]
+    fn identity_over_values() {
+        let num = Term::Num(45.3);
+        assert_eq!(Ok(num.clone()), eval_no_import(num.into()));
+
+        let boolean = Term::Bool(true);
+        assert_eq!(Ok(boolean.clone()), eval_no_import(boolean.into()));
+
+        let lambda = mk_fun!("x", mk_app!(mk_term::var("x"), mk_term::var("x")));
+        assert_eq!(Ok(lambda.as_ref().clone()), eval_no_import(lambda.into()));
+    }
+
+    #[test]
+    fn blame_panics() {
+        let label = Label::dummy();
+        if let Err(EvalError::BlameError(l, ..)) =
+            eval_no_import(mk_term::op1(UnaryOp::Blame(), Term::Lbl(label.clone())))
+        {
+            assert_eq!(l, label);
+        } else {
+            panic!("This evaluation should've returned a BlameError!");
+        }
+    }
+
+    #[test]
+    #[should_panic]
+    fn lone_var_panics() {
+        eval_no_import(mk_term::var("unbound")).unwrap();
+    }
+
+    #[test]
+    fn only_fun_are_applicable() {
+        eval_no_import(mk_app!(Term::Bool(true), Term::Num(45.))).unwrap_err();
+    }
+
+    #[test]
+    fn simple_app() {
+        let t = mk_app!(mk_term::id(), Term::Num(5.0));
+        assert_eq!(Ok(Term::Num(5.0)), eval_no_import(t));
+    }
+
+    #[test]
+    fn simple_let() {
+        let t = mk_term::let_in("x", Term::Num(5.0), mk_term::var("x"));
+        assert_eq!(Ok(Term::Num(5.0)), eval_no_import(t));
+    }
+
+    #[test]
+    fn simple_ite() {
+        let t = mk_term::if_then_else(Term::Bool(true), Term::Num(5.0), Term::Bool(false));
+        assert_eq!(Ok(Term::Num(5.0)), eval_no_import(t));
+    }
+
+    #[test]
+    fn simple_plus() {
+        let t = mk_term::op2(BinaryOp::Plus(), Term::Num(5.0), Term::Num(7.5));
+        assert_eq!(Ok(Term::Num(12.5)), eval_no_import(t));
+    }
+
+    #[test]
+    fn asking_for_various_types() {
+        let num = mk_term::op1(UnaryOp::IsNum(), Term::Num(45.3));
+        assert_eq!(Ok(Term::Bool(true)), eval_no_import(num));
+
+        let boolean = mk_term::op1(UnaryOp::IsBool(), Term::Bool(true));
+        assert_eq!(Ok(Term::Bool(true)), eval_no_import(boolean));
+
+        let lambda = mk_term::op1(
+            UnaryOp::IsFun(),
+            mk_fun!("x", mk_app!(mk_term::var("x"), mk_term::var("x"))),
+        );
+        assert_eq!(Ok(Term::Bool(true)), eval_no_import(lambda));
+    }
+
+    fn mk_default(t: RichTerm) -> Term {
+        use crate::term::MergePriority;
+
+        let mut meta = MetaValue::from(t);
+        meta.priority = MergePriority::Default;
+        Term::MetaValue(meta)
+    }
+
+    fn mk_docstring<S>(t: RichTerm, s: S) -> Term
+    where
+        S: Into<String>,
+    {
+        let mut meta = MetaValue::from(t);
+        meta.doc.replace(s.into());
+        Term::MetaValue(meta)
+    }
+
+    #[test]
+    fn enriched_terms_unwrapping() {
+        let t = mk_default(mk_default(mk_docstring(Term::Bool(false).into(), "a").into()).into())
+            .into();
+        assert_eq!(Ok(Term::Bool(false)), eval_no_import(t));
+    }
+
+    #[test]
+    fn merge_enriched_default() {
+        let t = mk_term::op2(
+            BinaryOp::Merge(),
+            Term::Num(1.0),
+            mk_default(Term::Num(2.0).into()),
+        );
+        assert_eq!(Ok(Term::Num(1.0)), eval_no_import(t));
+    }
+
+    #[test]
+    fn merge_incompatible_defaults() {
+        let t = mk_term::op2(
+            BinaryOp::Merge(),
+            mk_default(Term::Num(1.0).into()),
+            mk_default(Term::Num(2.0).into()),
+        );
+
+        eval_no_import(t).unwrap_err();
+    }
+
+    #[test]
+    fn imports() {
+        let mut resolver = SimpleResolver::new();
+        resolver.add_source(String::from("two"), String::from("1 + 1"));
+        resolver.add_source(String::from("lib"), String::from("{f = true}"));
+        resolver.add_source(String::from("bad"), String::from("^$*/.23ab 0°@"));
+        resolver.add_source(
+            String::from("nested"),
+            String::from("let x = import \"two\" in x + 1"),
+        );
+        resolver.add_source(
+            String::from("cycle"),
+            String::from("let x = import \"cycle_b\" in {a = 1, b = x.a}"),
+        );
+        resolver.add_source(
+            String::from("cycle_b"),
+            String::from("let x = import \"cycle\" in {a = x.a}"),
+        );
+
+        fn mk_import<R>(
+            var: &str,
+            import: &str,
+            body: RichTerm,
+            resolver: &mut R,
+        ) -> Result<RichTerm, ImportError>
+        where
+            R: ImportResolver,
+        {
+            resolve_imports(
+                mk_term::let_in(var, mk_term::import(import), body),
+                resolver,
+            )
+            .map(|(t, _)| t)
+        }
+
+        // let x = import "does_not_exist" in x
+        match mk_import("x", "does_not_exist", mk_term::var("x"), &mut resolver).unwrap_err() {
+            ImportError::IOError(_, _, _) => (),
+            _ => assert!(false),
+        };
+
+        // let x = import "bad" in x
+        match mk_import("x", "bad", mk_term::var("x"), &mut resolver).unwrap_err() {
+            ImportError::ParseErrors(_, _) => (),
+            _ => assert!(false),
+        };
+
+        // let x = import "two" in x
+        assert_eq!(
+            eval(
+                mk_import("x", "two", mk_term::var("x"), &mut resolver).unwrap(),
+                &Environment::new(),
+                &mut resolver
+            )
+            .map(Term::from)
+            .unwrap(),
+            Term::Num(2.0)
+        );
+
+        // let x = import "lib" in x.f
+        assert_eq!(
+            eval(
+                mk_import(
+                    "x",
+                    "lib",
+                    mk_term::op1(UnaryOp::StaticAccess(Ident::from("f")), mk_term::var("x")),
+                    &mut resolver,
+                )
+                .unwrap(),
+                &Environment::new(),
+                &mut resolver
+            )
+            .map(Term::from)
+            .unwrap(),
+            Term::Bool(true)
+        );
+    }
+
+    #[test]
+    fn interpolation_simple() {
+        let mut chunks = vec![
+            StrChunk::Literal(String::from("Hello")),
+            StrChunk::expr(
+                mk_term::op2(
+                    BinaryOp::StrConcat(),
+                    mk_term::string(", "),
+                    mk_term::string("World!"),
+                )
+                .into(),
+            ),
+            StrChunk::Literal(String::from(" How")),
+            StrChunk::expr(mk_term::if_then_else(
+                Term::Bool(true),
+                mk_term::string(" are"),
+                mk_term::string(" is"),
+            )),
+            StrChunk::Literal(String::from(" you?")),
+        ];
+        chunks.reverse();
+
+        let t: RichTerm = Term::StrChunks(chunks).into();
+        assert_eq!(
+            eval_no_import(t),
+            Ok(Term::Str(String::from("Hello, World! How are you?")))
+        );
+    }
+
+    #[test]
+    fn interpolation_nested() {
+        let mut inner_chunks = vec![
+            StrChunk::Literal(String::from(" How")),
+            StrChunk::expr(
+                Term::Op2(
+                    BinaryOp::StrConcat(),
+                    mk_term::string(" ar"),
+                    mk_term::string("e"),
+                )
+                .into(),
+            ),
+            StrChunk::expr(mk_term::if_then_else(
+                Term::Bool(true),
+                mk_term::string(" you"),
+                mk_term::string(" me"),
+            )),
+        ];
+        inner_chunks.reverse();
+
+        let mut chunks = vec![
+            StrChunk::Literal(String::from("Hello, World!")),
+            StrChunk::expr(Term::StrChunks(inner_chunks).into()),
+            StrChunk::Literal(String::from("?")),
+        ];
+        chunks.reverse();
+
+        let t: RichTerm = Term::StrChunks(chunks).into();
+        assert_eq!(
+            eval_no_import(t),
+            Ok(Term::Str(String::from("Hello, World! How are you?")))
+        );
+    }
+
+    #[test]
+    fn global_env() {
+        let mut global_env = Environment::new();
+        let mut resolver = DummyResolver {};
+        global_env.insert(
+            Ident::from("g"),
+            Thunk::new(
+                Closure::atomic_closure(Term::Num(1.0).into()),
+                IdentKind::Let,
+            ),
+        );
+
+        let t = mk_term::let_in("x", Term::Num(2.0), mk_term::var("x"));
+        assert_eq!(
+            eval(t, &global_env, &mut resolver).map(Term::from),
+            Ok(Term::Num(2.0))
+        );
+
+        let t = mk_term::let_in("x", Term::Num(2.0), mk_term::var("g"));
+        assert_eq!(
+            eval(t, &global_env, &mut resolver).map(Term::from),
+            Ok(Term::Num(1.0))
+        );
+
+        // Shadowing of global environment
+        let t = mk_term::let_in("g", Term::Num(2.0), mk_term::var("g"));
+        assert_eq!(
+            eval(t, &global_env, &mut resolver).map(Term::from),
+            Ok(Term::Num(2.0))
+        );
+    }
+
+    fn mk_env(bindings: Vec<(&str, RichTerm)>) -> Environment {
+        bindings
+            .into_iter()
+            .map(|(id, t)| {
+                (
+                    id.into(),
+                    Thunk::new(Closure::atomic_closure(t), IdentKind::Let),
+                )
+            })
+            .collect()
+    }
+
+    #[test]
+    fn substitution() {
+        let global_env = mk_env(vec![
+            ("glob1", Term::Num(1.0).into()),
+            ("glob2", parse("\"Glob2\"").unwrap()),
+            ("glob3", Term::Bool(false).into()),
+        ]);
+        let env = mk_env(vec![
+            ("loc1", Term::Bool(true).into()),
+            ("loc2", parse("if glob3 then glob1 else glob2").unwrap()),
+        ]);
+
+        let t = parse("let x = 1 in if loc1 then 1 + loc2 else glob3").unwrap();
+        assert_eq!(
+            subst(t, &global_env, &env),
+            parse("let x = 1 in if true then 1 + (if false then 1 else \"Glob2\") else false")
+                .unwrap()
+        );
+
+        let t =
+            parse("switch {`x => [1, glob1], `y => loc2, `z => {id = true, other = glob3}} loc1")
+                .unwrap();
+        assert_eq!(
+            subst(t, &global_env, &env),
+            parse("switch {`x => [1, 1], `y => (if false then 1 else \"Glob2\"), `z => {id = true, other = false}} true").unwrap()
+        );
+    }
+}
diff --git a/src/eval/callstack.rs b/src/eval/callstack.rs
deleted file mode 100644
index 3d2de11c..00000000
--- a/src/eval/callstack.rs
+++ /dev/null
@@ -1,234 +0,0 @@
-//! In a lazy language like Nickel, there are no well delimited stack frames due to how function
-//! application is evaluated. Additional information about the history of function calls is thus
-//! stored in a call stack solely for better error reporting.
-use super::IdentKind;
-use crate::{
-    identifier::Ident,
-    position::{RawSpan, TermPos},
-};
-use codespan::FileId;
-
-/// A call stack, saving the history of function calls.
-#[derive(PartialEq, Clone, Default, Debug)]
-pub struct CallStack(pub Vec<StackElem>);
-
-/// Basic description of a function call. Used for error reporting.
-pub struct CallDescr {
-    /// The name of the called function, if any.
-    pub head: Option<Ident>,
-    /// The position of the application.
-    pub span: RawSpan,
-}
-
-/// A call stack element.
-#[derive(Debug, Clone, Eq, PartialEq)]
-pub enum StackElem {
-    /// A function body was entered. The position is the position of the original application.
-    Fun(TermPos),
-    /// An application was evaluated.
-    App(TermPos),
-    /// A variable was entered.
-    Var {
-        kind: IdentKind,
-        id: Ident,
-        pos: TermPos,
-    },
-    /// A record field was entered.
-    Field {
-        id: Ident,
-        pos_record: TermPos,
-        pos_field: TermPos,
-        pos_access: TermPos,
-    },
-}
-
-impl CallStack {
-    pub fn new() -> Self {
-        CallStack(Vec::new())
-    }
-
-    /// Push a marker to indicate that a var was entered.
-    pub fn enter_var(&mut self, kind: IdentKind, id: Ident, pos: TermPos) {
-        self.0.push(StackElem::Var { kind, id, pos });
-    }
-
-    /// Push a marker to indicate that an application was entered.
-    pub fn enter_app(&mut self, pos: TermPos) {
-        // We ignore application without positions, which have been generated by the interpreter.
-        if pos.is_def() {
-            self.0.push(StackElem::App(pos));
-        }
-    }
-
-    /// Push a marker to indicate that during the evaluation an application, the function part was
-    /// finally evaluated to an expression of the form `fun x => body`, and that the body of this
-    /// function was entered.
-    pub fn enter_fun(&mut self, pos: TermPos) {
-        // We ignore application without positions, which have been generated by the interpreter.
-        if pos.is_def() {
-            self.0.push(StackElem::Fun(pos));
-        }
-    }
-
-    /// Push a marker to indicate that a record field was entered.
-    pub fn enter_field(
-        &mut self,
-        id: Ident,
-        pos_record: TermPos,
-        pos_field: TermPos,
-        pos_access: TermPos,
-    ) {
-        self.0.push(StackElem::Field {
-            id,
-            pos_record,
-            pos_field,
-            pos_access,
-        });
-    }
-
-    /// Process a raw callstack by aggregating elements belonging to the same call. Return a list
-    /// of call descriptions from the most nested/recent to the least nested/recent, together with
-    /// the last pending call, if any.
-    ///
-    /// Recall that when a call `f arg` is evaluated, the following events happen:
-    /// 1. `arg` is pushed on the evaluation stack.
-    /// 2. `f` is evaluated.
-    /// 3. Hopefully, the result of this evaluation is a function `Func(id, body)`. `arg` is popped
-    ///    from the stack, bound to `id` in the environment, and `body is entered`.
-    ///
-    /// For error reporting purpose, we want to be able to determine the chain of nested calls leading
-    /// to the current code path at any moment. To do so, the Nickel abstract machine maintains a
-    /// callstack via this basic mechanism:
-    /// 1. When an application is evaluated, push a marker with the position of the application on the callstack.
-    /// 2. When a function body is entered, push a marker with the position of the original application on the
-    ///    callstack.
-    /// 3. When a variable is evaluated, push a marker with its name and position on the callstack.
-    /// 4. When a record field is accessed, push a marker with its name and position on the
-    ///    callstack too.
-    ///
-    /// Both field and variable are useful to determine the name of a called function, when there
-    /// is one.  The resulting stack is not suited to be reported to the user for the following
-    /// reasons:
-    ///
-    /// 1. One call spans several items on the callstack. First the application is entered (pushing
-    ///    an `App`), then possibly variables or other application are evaluated until we
-    ///    eventually reach a function for the left hand side. Then body of this function is
-    ///    entered (pushing a `Fun`).
-    /// 2. Because of currying, multi-ary applications span several objects on the callstack.
-    ///    Typically, `(fun x y => x + y) arg1 arg2` spans two `App` and two `Fun` elements in the
-    ///    form `App1 App2 Fun2 Fun1`, where the position span of `App1` includes the position span
-    ///    of `App2`.  We want to group them as one call.
-    /// 3. The callstack includes calls to builtin contracts. These calls are inserted implicitly
-    ///    by the abstract machine and are not written explicitly by the user. Showing them is
-    ///    confusing and clutters the call chain, so we get rid of them too.
-    ///
-    /// This is the role of `group_by_calls`, which filter out unwanted elements and groups
-    /// callstack elements into atomic call elements represented by [`CallDescr`].
-    ///
-    /// The final call description list is reversed such that the most nested calls, which are
-    /// usually the most relevant to understand the error, are printed first.
-    ///
-    /// # Arguments
-    ///
-    /// - `contract_id`: the `FileId` of the source containing standard contracts, to filter their
-    ///   calls out.
-    pub fn group_by_calls(
-        self: &CallStack,
-        contract_id: FileId,
-    ) -> (Vec<CallDescr>, Option<CallDescr>) {
-        // We filter out calls and accesses made from within the builtin contracts, as well as
-        // generated variables introduced by program transformations.
-        let it = self.0.iter().filter(|elem| match elem {
-            StackElem::Var {id, ..} if id.is_generated() => false,
-            StackElem::Var{ pos: TermPos::Original(RawSpan { src_id, .. }), ..}
-            | StackElem::Var{pos: TermPos::Inherited(RawSpan { src_id, .. }), ..}
-            | StackElem::Fun(TermPos::Original(RawSpan { src_id, .. }))
-            | StackElem::Field {pos_access: TermPos::Original(RawSpan { src_id, .. }), ..}
-            | StackElem::Field {pos_access: TermPos::Inherited(RawSpan { src_id, .. }), ..}
-            | StackElem::App(TermPos::Original(RawSpan { src_id, .. }))
-            // We avoid applications (Fun/App) with inherited positions. Such calls include
-            // contracts applications which add confusing call items whose positions don't point to
-            // an actual call in the source.
-                if *src_id != contract_id =>
-            {
-                true
-            }
-            _ => false,
-        });
-
-        // We maintain a stack of active calls (whose head is being evaluated).  When encountering
-        // an identifier (variable or record field), we see if it could serve as a function name
-        // for the current active call. When a `Fun` is encountered, we check if this correspond to
-        // the current active call, and if it does, the call description is moved to a stack of
-        // processed calls.
-        //
-        // We also merge subcalls, in the sense that subcalls of larger calls are not considered
-        // separately. `app1` is a subcall of `app2` if the position of `app1` is included in the
-        // one of `app2` and the starting index is equal. We want `f a b c` to be reported as only
-        // one big call to `f` rather than three nested calls `f a`, `f a b`, and `f a b c`.
-        let mut pending: Vec<CallDescr> = Vec::new();
-        let mut entered: Vec<CallDescr> = Vec::new();
-
-        for elt in it {
-            match elt {
-                StackElem::Var { id, pos, .. }
-                | StackElem::Field {
-                    id,
-                    pos_access: pos,
-                    ..
-                } => {
-                    match pending.last_mut() {
-                        Some(CallDescr {
-                            head: ref mut head @ None,
-                            span: span_call,
-                        }) if pos.unwrap() <= *span_call => *head = Some(id.clone()),
-                        _ => (),
-                    };
-                }
-                StackElem::App(pos) => {
-                    let span = pos.unwrap();
-                    match pending.last() {
-                        Some(CallDescr {
-                            span: span_call, ..
-                        }) if span <= *span_call && span.start == span_call.start => (),
-                        _ => pending.push(CallDescr { head: None, span }),
-                    }
-                }
-                StackElem::Fun(pos) => {
-                    let span = pos.unwrap();
-                    if pending
-                        .last()
-                        .map(|cdescr| cdescr.span == span)
-                        .unwrap_or(false)
-                    {
-                        entered.push(pending.pop().unwrap());
-                    }
-                    // Otherwise, we are most probably entering a subcall () of the currently
-                    // active call (e.g. in an multi-ary application `f g h`, a subcall would be `f
-                    // g`). In any case, we do nothing.
-                }
-            }
-        }
-
-        entered.reverse();
-        (entered, pending.pop())
-    }
-
-    /// Return the length of the callstack. Wrapper for `callstack.0.len()`.
-    pub fn len(&self) -> usize {
-        self.0.len()
-    }
-
-    /// Truncate the callstack at a certain size. Used e.g. to quickly drop the elements introduced
-    /// during the strict evaluation of the operand of a primitive operator. Wrapper for
-    /// `callstack.0.truncate(len)`.
-    pub fn truncate(&mut self, len: usize) {
-        self.0.truncate(len)
-    }
-}
-
-impl From<CallStack> for Vec<StackElem> {
-    fn from(cs: CallStack) -> Self {
-        cs.0
-    }
-}
diff --git a/src/eval/lazy.rs b/src/eval/lazy.rs
deleted file mode 100644
index df094d4e..00000000
--- a/src/eval/lazy.rs
+++ /dev/null
@@ -1,256 +0,0 @@
-//! Thunks and associated devices used to implement lazy evaluation.
-use super::{Closure, IdentKind};
-use std::cell::{Ref, RefCell, RefMut};
-use std::rc::{Rc, Weak};
-
-/// The state of a thunk.
-///
-/// When created, a thunk is flagged as suspended. When accessed for the first time, a corresponding
-/// [`ThunkUpdateFrame`](./struct.ThunkUpdateFrame.html) is pushed on the stack and the thunk is
-/// flagged as black-hole. This prevents direct infinite recursions, since if a thunk is
-/// re-accessed while still in a black-hole state, we are sure that the evaluation will loop, and
-/// we can thus error out before overflowing the stack or looping forever. Finally, once the
-/// content of a thunk has been evaluated, the thunk is updated with the new value and flagged as
-/// evaluated, so that future accesses won't even push an update frame on the stack.
-#[derive(Copy, Clone, Eq, PartialEq, Debug)]
-pub enum ThunkState {
-    Blackholed,
-    Suspended,
-    Evaluated,
-}
-
-/// The mutable data stored inside a thunk.
-#[derive(Clone, Debug, PartialEq)]
-pub struct ThunkData {
-    inner: InnerThunkData,
-    state: ThunkState,
-}
-
-/// The part of [ThunkData] responsible for storing the closure itself. It can either be:
-/// - A standard thunk, that is destructively updated once and for all
-/// - A revertible thunk, that can be restored to its original expression. Used to implement
-/// recursive merging of records and overriding (see the [RFC
-/// overriding](https://github.com/tweag/nickel/pull/330))
-#[derive(Clone, Debug, PartialEq)]
-pub enum InnerThunkData {
-    Standard(Closure),
-    Revertible {
-        orig: Rc<Closure>,
-        cached: Rc<Closure>,
-    },
-}
-
-impl ThunkData {
-    /// Create new standard thunk data.
-    pub fn new(closure: Closure) -> Self {
-        ThunkData {
-            inner: InnerThunkData::Standard(closure),
-            state: ThunkState::Suspended,
-        }
-    }
-
-    /// Create new revertible thunk data.
-    pub fn new_rev(orig: Closure) -> Self {
-        let rc = Rc::new(orig);
-
-        ThunkData {
-            inner: InnerThunkData::Revertible {
-                orig: rc.clone(),
-                cached: rc,
-            },
-            state: ThunkState::Suspended,
-        }
-    }
-
-    /// Return a reference to the closure currently cached.
-    pub fn closure(&self) -> &Closure {
-        match self.inner {
-            InnerThunkData::Standard(ref closure) => closure,
-            InnerThunkData::Revertible { ref cached, .. } => cached,
-        }
-    }
-
-    /// Return a mutable reference to the closure currently cached.
-    pub fn closure_mut(&mut self) -> &mut Closure {
-        match self.inner {
-            InnerThunkData::Standard(ref mut closure) => closure,
-            InnerThunkData::Revertible { ref mut cached, .. } => Rc::make_mut(cached),
-        }
-    }
-
-    /// Consume the data and return the cached closure.
-    pub fn into_closure(self) -> Closure {
-        match self.inner {
-            InnerThunkData::Standard(closure) => closure,
-            InnerThunkData::Revertible { orig, cached } => {
-                std::mem::drop(orig);
-                Rc::try_unwrap(cached).unwrap_or_else(|rc| (*rc).clone())
-            }
-        }
-    }
-
-    /// Update the cached closure.
-    pub fn update(&mut self, new: Closure) {
-        match self.inner {
-            InnerThunkData::Standard(ref mut closure) => *closure = new,
-            InnerThunkData::Revertible { ref mut cached, .. } => *cached = Rc::new(new),
-        }
-
-        self.state = ThunkState::Evaluated;
-    }
-
-    /// Create fresh unevaluated thunk data from `self`, reverted to its original state before the
-    /// first update. For standard thunk data, the content is unchanged and the state is conserved:
-    /// in this case, `revert()` is the same as `clone()`.
-    pub fn revert(&self) -> Self {
-        match self.inner {
-            InnerThunkData::Standard(_) => self.clone(),
-            InnerThunkData::Revertible { ref orig, .. } => ThunkData {
-                inner: InnerThunkData::Revertible {
-                    orig: Rc::clone(orig),
-                    cached: Rc::clone(orig),
-                },
-                state: ThunkState::Suspended,
-            },
-        }
-    }
-}
-
-/// A thunk.
-///
-/// A thunk is a shared suspended computation. It is the primary device for the implementation of
-/// lazy evaluation.
-///
-/// For the implementation of recursive merging, some thunks need to be revertible, in the sense
-/// that we must be able to revert to the original expression before update. Those are called
-/// revertible thunks. Most expressions don't need revertible thunks as their evaluation will
-/// always give the same result, but some others, such as the ones containing recursive references
-/// inside a record may be invalidated by merging, and thus need to store the unaltered original
-/// expression. Those aspects are mainly handled in [InnerThunkData].
-#[derive(Clone, Debug, PartialEq)]
-pub struct Thunk {
-    data: Rc<RefCell<ThunkData>>,
-    ident_kind: IdentKind,
-}
-
-/// A black-holed thunk was accessed, which would lead to infinite recursion.
-#[derive(Clone, Copy, Debug, Eq, PartialEq)]
-pub struct BlackholedError;
-
-impl Thunk {
-    /// Create a new standard thunk.
-    pub fn new(closure: Closure, ident_kind: IdentKind) -> Self {
-        Thunk {
-            data: Rc::new(RefCell::new(ThunkData::new(closure))),
-            ident_kind,
-        }
-    }
-
-    /// Create a new revertible thunk.
-    pub fn new_rev(closure: Closure, ident_kind: IdentKind) -> Self {
-        Thunk {
-            data: Rc::new(RefCell::new(ThunkData::new_rev(closure))),
-            ident_kind,
-        }
-    }
-
-    pub fn state(&self) -> ThunkState {
-        self.data.borrow().state
-    }
-
-    /// Set the state to evaluated.
-    pub fn set_evaluated(&mut self) {
-        self.data.borrow_mut().state = ThunkState::Evaluated;
-    }
-
-    /// Generate an update frame from this thunk and set the state to `Blackholed`. Return an
-    /// error if the thunk was already black-holed.
-    pub fn mk_update_frame(&mut self) -> Result<ThunkUpdateFrame, BlackholedError> {
-        if self.data.borrow().state == ThunkState::Blackholed {
-            return Err(BlackholedError);
-        }
-
-        self.data.borrow_mut().state = ThunkState::Blackholed;
-
-        Ok(ThunkUpdateFrame {
-            data: Rc::downgrade(&self.data),
-            _ident_kind: self.ident_kind,
-        })
-    }
-
-    /// Immutably borrow the inner closure. Panic if there is another active mutable borrow.
-    pub fn borrow(&self) -> Ref<'_, Closure> {
-        Ref::map(self.data.borrow(), |data| data.closure())
-    }
-
-    /// Mutably borrow the inner closure. Panic if there is any other active borrow.
-    pub fn borrow_mut(&mut self) -> RefMut<'_, Closure> {
-        RefMut::map(self.data.borrow_mut(), |data| data.closure_mut())
-    }
-
-    /// Get an owned clone of the inner closure.
-    pub fn get_owned(&self) -> Closure {
-        self.data.borrow().closure().clone()
-    }
-
-    pub fn ident_kind(&self) -> IdentKind {
-        self.ident_kind
-    }
-
-    /// Consume the thunk and return an owned closure. Avoid cloning if this thunk is the only
-    /// reference to the inner closure.
-    pub fn into_closure(self) -> Closure {
-        match Rc::try_unwrap(self.data) {
-            Ok(inner) => inner.into_inner().into_closure(),
-            Err(rc) => rc.borrow().closure().clone(),
-        }
-    }
-
-    /// Create a fresh unevaluated thunk from `self`, reverted to its original state before the
-    /// first update. For a standard thunk, the content is unchanged and the state is conserved: in
-    /// this case, `revert()` is the same as `clone()`.
-    pub fn revert(&self) -> Self {
-        Thunk {
-            data: Rc::new(RefCell::new(self.data.borrow().revert())),
-            ident_kind: self.ident_kind,
-        }
-    }
-
-    /// Determine if a thunk is worth being put on the stack for future update.
-    ///
-    /// Typically, WHNFs and enriched values will not be evaluated to a simpler expression and are not
-    /// worth updating.
-    pub fn should_update(&self) -> bool {
-        let term = &self.borrow().body.term;
-        !term.is_whnf() && !term.is_metavalue()
-    }
-}
-
-/// A thunk update frame.
-///
-/// A thunk update frame is put on the stack whenever a variable is entered, such that once this
-/// variable is evaluated, the corresponding thunk can be updated. It is similar to a thunk but it
-/// holds a weak reference to the inner closure, to avoid unnecessarily keeping the underlying
-/// closure alive.
-#[derive(Clone, Debug)]
-pub struct ThunkUpdateFrame {
-    data: Weak<RefCell<ThunkData>>,
-    _ident_kind: IdentKind,
-}
-
-impl ThunkUpdateFrame {
-    /// Update the corresponding thunk with a closure. Set the state to `Evaluated`
-    ///
-    /// # Return
-    ///
-    /// - `true` if the thunk was successfully updated
-    /// - `false` if the corresponding closure has been dropped since
-    pub fn update(self, closure: Closure) -> bool {
-        if let Some(data) = Weak::upgrade(&self.data) {
-            data.borrow_mut().update(closure);
-            true
-        } else {
-            false
-        }
-    }
-}
diff --git a/src/label.rs b/src/label.rs
index 700c0742..e42ce1e2 100644
--- a/src/label.rs
+++ b/src/label.rs
@@ -2,7 +2,7 @@
 //!
 //! A label is a value holding metadata relative to contract checking. It gives the user useful
 //! information about the context of a contract failure.
-use crate::eval::lazy::Thunk;
+use crate::eval::Thunk;
 use crate::position::{RawSpan, TermPos};
 use crate::types::{AbsType, Types};
 use codespan::Files;
diff --git a/src/lib.rs b/src/lib.rs
index b1a081fc..08376bcd 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -5,13 +5,16 @@ pub mod error;
 pub mod eval;
 pub mod identifier;
 pub mod label;
+pub mod merge;
+pub mod operation;
 pub mod parser;
 pub mod position;
 pub mod program;
 pub mod repl;
 pub mod serialize;
+pub mod stack;
 pub mod stdlib;
 pub mod term;
-pub mod transform;
+pub mod transformations;
 pub mod typecheck;
 pub mod types;
diff --git a/src/eval/merge.rs b/src/merge.rs
similarity index 99%
rename from src/eval/merge.rs
rename to src/merge.rs
index 4513d343..6fe4fc2a 100644
--- a/src/eval/merge.rs
+++ b/src/merge.rs
@@ -56,7 +56,7 @@ use crate::eval::{CallStack, Closure, Environment};
 use crate::label::Label;
 use crate::position::TermPos;
 use crate::term::{make as mk_term, BinaryOp, Contract, MetaValue, RecordAttrs, RichTerm, Term};
-use crate::transform::Closurizable;
+use crate::transformations::Closurizable;
 use std::collections::HashMap;
 
 /// Merging mode. Merging is used both to combine standard data and to apply contracts defined as
@@ -434,7 +434,7 @@ fn merge_closurize(
 }
 
 fn rev_thunks<'a, I: Iterator<Item = &'a mut RichTerm>>(map: I, env: &mut Environment) {
-    use crate::transform::fresh_var;
+    use crate::transformations::fresh_var;
 
     for rt in map {
         if let Term::Var(id) = rt.as_ref() {
diff --git a/src/eval/operation.rs b/src/operation.rs
similarity index 99%
rename from src/eval/operation.rs
rename to src/operation.rs
index 811aee5c..b9612e57 100644
--- a/src/eval/operation.rs
+++ b/src/operation.rs
@@ -6,18 +6,18 @@
 //! the functions [`process_unary_operation`](fn.process_unary_operation.html) and
 //! [`process_binary_operation`](fn.process_binary_operation.html) receive evaluated operands and
 //! implement the actual semantics of operators.
-use super::merge;
-use super::merge::{merge, MergeMode};
-use super::stack::Stack;
 use crate::error::EvalError;
 use crate::eval::{subst, CallStack, Closure, Environment};
 use crate::identifier::Ident;
 use crate::label::ty_path;
+use crate::merge;
+use crate::merge::{merge, MergeMode};
 use crate::mk_record;
 use crate::position::TermPos;
+use crate::stack::Stack;
 use crate::term::make as mk_term;
 use crate::term::{BinaryOp, NAryOp, RichTerm, StrChunk, Term, UnaryOp};
-use crate::transform::Closurizable;
+use crate::transformations::Closurizable;
 use crate::{mk_app, mk_fun, mk_opn};
 use crate::{serialize, serialize::ExportFormat};
 use md5::digest::Digest;
diff --git a/src/repl/mod.rs b/src/repl/mod.rs
index 08c76699..596de211 100644
--- a/src/repl/mod.rs
+++ b/src/repl/mod.rs
@@ -11,9 +11,8 @@ use crate::error::{Error, EvalError, IOError, ParseError, ParseErrors, ReplError
 use crate::identifier::Ident;
 use crate::parser::{grammar, lexer, ExtendedTerm};
 use crate::term::{RichTerm, Term};
-use crate::transform::import_resolution;
 use crate::types::Types;
-use crate::{eval, transform, typecheck};
+use crate::{eval, transformations, typecheck};
 use codespan::FileId;
 use simple_counter::*;
 use std::ffi::{OsStr, OsString};
@@ -122,7 +121,7 @@ impl ReplImpl {
             // Because we don't use the cache for input, we have to perform recursive import
             // resolution/typechecking/transformation by oursleves.
             ExtendedTerm::RichTerm(t) => {
-                let (t, pending) = import_resolution::resolve_imports(t, &mut self.cache)?;
+                let (t, pending) = transformations::resolve_imports(t, &mut self.cache)?;
                 for id in &pending {
                     self.cache.resolve_imports(*id).unwrap();
                 }
@@ -136,7 +135,7 @@ impl ReplImpl {
                         })?;
                 }
 
-                let t = transform::transform(t);
+                let t = transformations::transform(t);
                 for id in &pending {
                     self.cache
                         .transform(*id)
@@ -146,7 +145,7 @@ impl ReplImpl {
                 Ok(eval_function(t, &self.env.eval_env, &mut self.cache)?.into())
             }
             ExtendedTerm::ToplevelLet(id, t) => {
-                let (t, pending) = import_resolution::resolve_imports(t, &mut self.cache)?;
+                let (t, pending) = transformations::resolve_imports(t, &mut self.cache)?;
                 for id in &pending {
                     self.cache.resolve_imports(*id).unwrap();
                 }
@@ -161,7 +160,7 @@ impl ReplImpl {
                         })?;
                 }
 
-                let t = transform::transform(t);
+                let t = transformations::transform(t);
                 for id in &pending {
                     self.cache
                         .transform(*id)
@@ -208,7 +207,7 @@ impl Repl for ReplImpl {
         })?;
 
         let term = self.cache.get_owned(file_id).unwrap();
-        let (term, pending) = import_resolution::resolve_imports(term, &mut self.cache)?;
+        let (term, pending) = transformations::resolve_imports(term, &mut self.cache)?;
         for id in &pending {
             self.cache.resolve_imports(*id).unwrap();
         }
@@ -222,7 +221,7 @@ impl Repl for ReplImpl {
         let file_id = self.cache.add_tmp("<repl-typecheck>", String::from(exp));
         // We ignore non fatal errors while type checking.
         let (term, _) = self.cache.parse_nocache(file_id)?;
-        let (term, pending) = import_resolution::resolve_imports(term, &mut self.cache)?;
+        let (term, pending) = transformations::resolve_imports(term, &mut self.cache)?;
         for id in &pending {
             self.cache.resolve_imports(*id).unwrap();
         }
diff --git a/src/eval/stack.rs b/src/stack.rs
similarity index 99%
rename from src/eval/stack.rs
rename to src/stack.rs
index bb7588cb..e5f7d085 100644
--- a/src/eval/stack.rs
+++ b/src/stack.rs
@@ -1,8 +1,8 @@
 //! Define the main evaluation stack of the Nickel abstract machine and related operations.
 //!
 //! See [eval](../eval/index.html).
-use super::operation::OperationCont;
 use crate::eval::{Closure, Environment, IdentKind, Thunk, ThunkUpdateFrame};
+use crate::operation::OperationCont;
 use crate::position::TermPos;
 use crate::term::{RichTerm, StrChunk};
 
diff --git a/src/term.rs b/src/term.rs
index 31f54efb..4d91ff4d 100644
--- a/src/term.rs
+++ b/src/term.rs
@@ -265,15 +265,13 @@ impl MetaValue {
             value: _,
         } = outer;
 
-        if types.is_some() {
-            // If both have type annotations, the result will have the outer one as a type annotation.
-            // However we still need to enforce the corresponding contract to preserve the operational
-            // semantics. Thus, the inner type annotation is derelicted to a contract.
-            match inner.types.take() {
-                Some(ctr) => contracts.push(ctr),
-                _ => (),
-            };
-        }
+        // If both have type annotations, the result will have the outer one as a type annotation.
+        // However we still need to enforce the corresponding contract to preserve the operational
+        // semantics. Thus, the inner type annotation is derelicted to a contract.
+        match inner.types.take() {
+            Some(ctr) if types.is_some() => contracts.push(ctr),
+            _ => (),
+        };
 
         contracts.extend(inner.contracts.into_iter());
 
@@ -1327,21 +1325,3 @@ pub mod make {
         Term::Import(path.into()).into()
     }
 }
-
-#[cfg(test)]
-mod tests {
-    use super::*;
-
-    /// Regression test for issue [#548](https://github.com/tweag/nickel/issues/548)
-    #[test]
-    fn metavalue_flatten() {
-        let mut inner = MetaValue::new();
-        inner.types = Some(Contract {
-            types: Types(AbsType::Num()),
-            label: Label::dummy(),
-        });
-        let outer = MetaValue::new();
-        let res = MetaValue::flatten(outer, inner);
-        assert_ne!(res.types, None);
-    }
-}
diff --git a/src/transform/apply_contracts.rs b/src/transform/apply_contracts.rs
deleted file mode 100644
index dae387fd..00000000
--- a/src/transform/apply_contracts.rs
+++ /dev/null
@@ -1,38 +0,0 @@
-//! Generate contract applications from annotations.
-//!
-//! During the evaluation, the following invariant is enforced: any contract (be it the type
-//! annotation or a contract annotation) contained in a `MetaValue` must have been applied to the
-//! inner value of this metavalue. This invariant is false just after parsing, as there's merely no
-//! direct `Assume` in the output AST. This transformation makes it true after program
-//! transformations by generating corresponding assume.
-//!
-//! It must be run before `share_normal_form` to avoid rechecking contracts each time the inner
-//! value is unwrapped.
-use crate::mk_app;
-use crate::term::{RichTerm, Term};
-
-/// If the top-level node of the AST is a meta-value, apply the meta-value's contracts to the inner
-/// value.  Otherwise, return the term unchanged.
-pub fn transform_one(rt: RichTerm) -> RichTerm {
-    let RichTerm { term, pos } = rt;
-
-    match *term {
-        Term::MetaValue(mut meta) if meta.value.is_some() => {
-            let inner = meta.types.iter().chain(meta.contracts.iter()).fold(
-                meta.value.take().unwrap(),
-                |acc, ctr| {
-                    mk_app!(
-                        ctr.types.clone().contract(),
-                        Term::Lbl(ctr.label.clone()),
-                        acc
-                    )
-                    .with_pos(pos.into_inherited())
-                },
-            );
-
-            meta.value.replace(inner);
-            RichTerm::new(Term::MetaValue(meta), pos.into_inherited())
-        }
-        t => RichTerm::new(t, pos),
-    }
-}
diff --git a/src/transform/desugar_destructuring.rs b/src/transform/desugar_destructuring.rs
deleted file mode 100644
index 191ba702..00000000
--- a/src/transform/desugar_destructuring.rs
+++ /dev/null
@@ -1,124 +0,0 @@
-//! Desugar destructuring
-//!
-//! Replace a let-binding with destructuring by a classical let-binding.
-//! It will first destruct the pattern and create a new var for each field of the pattern.
-//! After that, it will construct a new Record/List from the extracted fields.
-//!
-//! # Example
-//!
-//! The let pattern:
-//! ```text
-//! let x @ {a, b=d, ..} = {a=1,b=2,c="ignored"} in ...
-//! ```
-//! will be transformed to:
-//! ```text
-//! let x = {a=1,b=2,c="ignored"} in
-//! let a = x.a in
-//! let d = x.b in
-//! ...
-//! ```
-use crate::destruct::{Destruct, Match};
-use crate::identifier::Ident;
-use crate::term::make::{op1, op2};
-use crate::term::{
-    BinaryOp::DynRemove, BindingType, MetaValue, RichTerm, Term, UnaryOp::StaticAccess,
-};
-
-/// Wrap the desugar term in a meta value containing the "Record contract" needed to check the
-/// pattern exhaustively and also fill the default values (`?` operator) if not presents in the
-/// record. This function should be, in the general case, considered as the entry point of this
-/// transformation.
-pub fn desugar_with_contract(rt: RichTerm) -> RichTerm {
-    if let Term::LetPattern(x, pat, t_, body) = *rt.term {
-        let pos = body.pos;
-        let meta = pat.clone().as_contract();
-        let t_ = {
-            let t_pos = t_.pos;
-            RichTerm::new(
-                Term::MetaValue(MetaValue {
-                    value: Some(t_),
-                    ..meta
-                }),
-                t_pos,
-            )
-        };
-        desugar(RichTerm::new(Term::LetPattern(x, pat, t_, body), pos))
-    } else {
-        rt
-    }
-}
-
-/// Main transformation function to desugar let patterns. WARNING: In a real usage case, you will
-/// want to generate also the metavalue associated to this pattern destructuring. Do not consider
-/// this function as the entry point of the transformation. For that, use `desugar_with_contract`.
-pub fn desugar(rt: RichTerm) -> RichTerm {
-    if let Term::LetPattern(x, pat, t_, body) = *rt.term {
-        let pos = body.pos;
-        let x = x.unwrap_or_else(super::fresh_var);
-        RichTerm::new(
-            Term::Let(
-                x.clone(),
-                t_,
-                destruct_term(x.clone(), &pat, bind_open_field(x, &pat, body)),
-                BindingType::Normal,
-            ),
-            pos,
-        )
-    } else {
-        rt
-    }
-}
-
-/// Wrap `body` in a let construct binding the open part of the pattern to the required value.
-/// Having `let {a,..y} = {a=1, b=2, c=3} in <BODY>` will bind `y` to `{b=2,c=3}` in `BODY`. Here,
-/// `x` is the identifier pointing to the full record. If having `val @ {...} = ... in ...` the
-/// variable x should be `Ident("val")` but if we have a `@` binding less form, you will probably
-/// generate a fresh variable.
-fn bind_open_field(x: Ident, pat: &Destruct, body: RichTerm) -> RichTerm {
-    let (matches, var) = match pat {
-        Destruct::Record(matches, true, Some(x)) => (matches, x.clone()),
-        Destruct::Record(matches, true, None) => (matches, super::fresh_var()),
-        Destruct::Record(_, false, None) | Destruct::Empty => return body,
-        _ => panic!("A closed pattern can not have a rest binding"),
-    };
-    Term::Let(
-        var.clone(),
-        matches.iter().fold(Term::Var(x).into(), |x, m| match m {
-            Match::Simple(i, _) | Match::Assign(i, _, _) => {
-                op2(DynRemove(), Term::Str(i.to_string()), x)
-            }
-        }),
-        body,
-        BindingType::Normal,
-    )
-    .into()
-}
-
-/// Core of the destructuring. Bind all the variables of the pattern except the "open" (`..y`)
-/// part. For that, see `bind_open_field`.
-fn destruct_term(x: Ident, pat: &Destruct, body: RichTerm) -> RichTerm {
-    let pos = body.pos;
-    match pat {
-        Destruct::Record(matches, ..) => matches.iter().fold(body, move |t, m| match m {
-            Match::Simple(id, _) => RichTerm::new(
-                Term::Let(
-                    id.clone(),
-                    op1(StaticAccess(id.clone()), Term::Var(x.clone())),
-                    t,
-                    BindingType::Normal,
-                ),
-                pos,
-            ),
-            Match::Assign(f, _, (id, pat)) => desugar(RichTerm::new(
-                Term::LetPattern(
-                    id.clone(),
-                    pat.clone(),
-                    op1(StaticAccess(f.clone()), Term::Var(x.clone())),
-                    t,
-                ),
-                pos,
-            )),
-        }),
-        _ => body,
-    }
-}
diff --git a/src/transform/import_resolution.rs b/src/transform/import_resolution.rs
deleted file mode 100644
index 8b013f41..00000000
--- a/src/transform/import_resolution.rs
+++ /dev/null
@@ -1,83 +0,0 @@
-//! Import resolution. Search for imports in the AST, load the corresponding file in the cache, and
-//! replace the original import node by a resolved import one, which stores the corresponding file
-//! identifier directly.
-use super::ImportResolver;
-use crate::error::ImportError;
-use crate::term::{RichTerm, Term, TraverseMethod};
-use codespan::FileId;
-use std::path::PathBuf;
-
-/// The state passed around during the imports resolution. It holds a reference to the import
-/// resolver, to a stack of pending imported term to be transformed and the path of the import
-/// currently being processed, if any.
-struct ImportsResolutionState<'a, R> {
-    resolver: &'a mut R,
-    stack: &'a mut Vec<FileId>,
-    parent: Option<PathBuf>,
-}
-
-/// Perform imports resolution.
-///
-/// All resolved imports are stacked during the process. Once the term has been traversed,
-/// the elements of this stack are returned. The caller is responsible
-/// to recursively resolve imports of this stack and or to perform
-/// transformations on it.
-pub fn resolve_imports<R>(
-    rt: RichTerm,
-    resolver: &mut R,
-) -> Result<(RichTerm, Vec<FileId>), ImportError>
-where
-    R: ImportResolver,
-{
-    let mut stack = Vec::new();
-
-    let source_file: Option<PathBuf> = rt.pos.as_opt_ref().map(|x| {
-        let path = resolver.get_path(x.src_id);
-        PathBuf::from(path)
-    });
-
-    let mut state = ImportsResolutionState {
-        resolver,
-        stack: &mut stack,
-        parent: source_file,
-    };
-
-    // If an import is resolved, then stack it.
-    let transformed = rt.traverse(
-        &mut |rt: RichTerm,
-              state: &mut ImportsResolutionState<R>|
-         -> Result<RichTerm, ImportError> {
-            let rt = transform_one(rt, state.resolver, &state.parent)?;
-
-            if let Term::ResolvedImport(file_id) = rt.term.as_ref() {
-                state.stack.push(*file_id);
-            }
-            Ok(rt)
-        },
-        &mut state,
-        TraverseMethod::BottomUp,
-    )?;
-
-    Ok((transformed, stack))
-}
-
-/// Resolve the import if the term is an unresolved import, or return the term unchanged. As
-/// [`share_normal_form::transform_one`](../share_normal_form/fn.transform_one.html), this function
-/// is not recursive.
-pub fn transform_one<R>(
-    rt: RichTerm,
-    resolver: &mut R,
-    parent: &Option<PathBuf>,
-) -> Result<RichTerm, ImportError>
-where
-    R: ImportResolver,
-{
-    let term = rt.as_ref();
-    match term {
-        Term::Import(path) => {
-            let (_, file_id) = resolver.resolve(path, parent.clone(), &rt.pos)?;
-            Ok(RichTerm::new(Term::ResolvedImport(file_id), rt.pos))
-        }
-        _ => Ok(rt),
-    }
-}
diff --git a/src/transform/mod.rs b/src/transform/mod.rs
deleted file mode 100644
index cb4fd827..00000000
--- a/src/transform/mod.rs
+++ /dev/null
@@ -1,153 +0,0 @@
-use crate::cache::ImportResolver;
-use crate::eval::{lazy::Thunk, Closure, Environment, IdentKind};
-use crate::identifier::Ident;
-use crate::term::{Contract, RichTerm, Term, TraverseMethod};
-use crate::types::{AbsType, Types};
-use simple_counter::*;
-
-generate_counter!(FreshVarCounter, usize);
-
-pub mod apply_contracts;
-pub mod desugar_destructuring;
-pub mod import_resolution;
-pub mod share_normal_form;
-
-/// Apply all program transformations, excepted import resolution that is currently performed
-/// earlier, as it needs to be done before typechecking.
-///
-/// Do not perform transformations on the imported files. If needed, either do it yourself using
-/// pending imports returned by [`resolve_imports`](../fn.resolve_imports.html) or use the
-/// [`Cache`](../../cache/struct.Cache.html)
-pub fn transform(rt: RichTerm) -> RichTerm {
-    let rt = rt
-        .traverse(
-            &mut |rt: RichTerm, _| -> Result<RichTerm, ()> {
-                // before anything, we have to desugar the syntax
-                let rt = desugar_destructuring::desugar_with_contract(rt);
-                // We need to do contract generation before wrapping stuff in variables
-                let rt = apply_contracts::transform_one(rt);
-                Ok(rt)
-            },
-            &mut (),
-            TraverseMethod::TopDown,
-        )
-        .unwrap();
-
-    rt.traverse(
-        &mut |rt: RichTerm, _| -> Result<RichTerm, ()> {
-            let rt = share_normal_form::transform_one(rt);
-            Ok(rt)
-        },
-        &mut (),
-        TraverseMethod::BottomUp,
-    )
-    .unwrap()
-}
-
-/// Generate a new fresh variable which do not clash with user-defined variables.
-pub fn fresh_var() -> Ident {
-    use crate::identifier::GEN_PREFIX;
-
-    format!("{}{}", GEN_PREFIX, FreshVarCounter::next()).into()
-}
-
-/// Structures which can be packed together with their environment as a closure.
-///
-/// The typical implementer is [`RichTerm`](../term/enum.RichTerm.html), but structures containing
-/// terms can also be closurizable, such as the contract in a [`Types`](../types/typ.Types.html).
-/// In this case, the inner term is closurized.
-pub trait Closurizable {
-    /// Pack a closurizable together with its environment `with_env` as a closure in the main
-    /// environment `env`.
-    fn closurize(self, env: &mut Environment, with_env: Environment) -> Self;
-}
-
-impl Closurizable for RichTerm {
-    /// Pack a term together with an environment as a closure.
-    ///
-    /// Generate a fresh variable, bind it to the corresponding closure `(t,with_env)` in `env`,
-    /// and return this variable as a fresh term.
-    fn closurize(self, env: &mut Environment, with_env: Environment) -> RichTerm {
-        // If the term is already a variable, we don't have to create a useless intermediate
-        // closure. We just transfer the original thunk to the new environment. This is not only an
-        // optimization: this is relied upon by recursive record merging when computing the
-        // fixpoint.
-        //
-        // More specifically, the evaluation of a recursive record patches the environment of each
-        // field with the thunks recursively referring to the other fields of the record. `eval`
-        // assumes that a recursive record field is either a constant or a generated variable whose
-        // thunks *immediately* contain the original unevaluated expression (both properties are
-        // true after the share normal form transformation and maintained when reverting thunks
-        // before merging recursive records).
-        //
-        // To maintain this invariant, `closurize` must NOT introduce an indirection through a
-        // variable, such as transforming:
-        //
-        // ```
-        // {foo = %1, bar = 1} in env %1 <- 1 + bar
-        // ```
-        //
-        // to:
-        //
-        // ```
-        // {foo = %2, bar = 1} in env %2 <- (%1 in env %1 <- 1 + bar)
-        // ```
-        //
-        // In this case, the evaluation of the recursive records will patch the outer environment
-        // instead of the inner one, giving:
-        //
-        // ```
-        // {foo = %2, bar = 1} in env %2 <- (%1 in env %1 <- 1 + bar), bar <- 1
-        // ```
-        //
-        // Then, evaluating `foo` would unduly raise an unbound identifier error.
-        //
-        //
-        // We currently only do this optimization for generated variables (introduced by the share
-        // normal form). We could do it for non-generated identifiers as well, but be we would be
-        // renaming user-supplied variables by gibberish generated names. It may hamper error
-        // reporting, so for the time being, we restrict ourselves to generated identifiers. Note
-        // that performing or not performing this optimization for user-supplied variables doesn't
-        // affect the invariant mentioned above, because the share normal form must ensure that the
-        // fields of a record all contain generated variables (or constant), but never
-        // user-supplied variables.
-        let var = fresh_var();
-        let pos = self.pos;
-
-        let thunk = match self.as_ref() {
-            Term::Var(id) if id.is_generated() => with_env.get(&id).expect(&format!(
-                "Internal error(closurize) : generated identifier {} not found in the environment",
-                id
-            )),
-            _ => {
-                let closure = Closure {
-                    body: self,
-                    env: with_env,
-                };
-                Thunk::new(closure, IdentKind::Record)
-            }
-        };
-
-        env.insert(var.clone(), thunk);
-        RichTerm::new(Term::Var(var), pos.into_inherited())
-    }
-}
-
-impl Closurizable for Types {
-    /// Pack the contract of a type together with an environment as a closure.
-    ///
-    /// Extract the underlying contract, closurize it and wrap it back as a flat type (an opaque
-    /// type defined by a custom contract).
-    fn closurize(self, env: &mut Environment, with_env: Environment) -> Types {
-        Types(AbsType::Flat(self.contract().closurize(env, with_env)))
-    }
-}
-
-impl Closurizable for Contract {
-    fn closurize(self, env: &mut Environment, with_env: Environment) -> Contract {
-        Contract {
-            types: self.types.closurize(env, with_env),
-            label: self.label,
-        }
-    }
-}
diff --git a/src/transform/share_normal_form.rs b/src/transform/share_normal_form.rs
deleted file mode 100644
index e4ccf79b..00000000
--- a/src/transform/share_normal_form.rs
+++ /dev/null
@@ -1,192 +0,0 @@
-//! Share normal form.
-//!
-//! Replace the subexpressions of WHNFs that are not functions by thunks, such that they can be
-//! shared. It is similar to the behavior of other lazy languages with respect to data
-//! constructors.  To do so, subexpressions are replaced by fresh variables, introduced by new let
-//! bindings put at the beginning of the WHNF.
-//!
-//! For example, take the expression:
-//! ```text
-//! let x = {a = 1 + 1} in x.a + x.a
-//! ```
-//!
-//! The term `{a = 1 + 1}` is a record, and hence a WHNF. In consequence, the thunk allocated to x
-//! is never updated. Without additional machinery, `a` will be recomputed each time is it used,
-//! two times here.
-//!
-//! The transformation replaces such subexpressions, namely the content of the fields
-//! of records and the elements of lists - `(1 + 1)` in our example -, with fresh variables
-//! introduced by `let`  added at the head of the term:
-//!
-//! ```text
-//! let x = (let var = 1 + 1 in {a = var}) in x.a + x.a
-//! ```
-//!
-//! Now, the field `a` points to the thunk introduced by `var`: at the evaluation of the first
-//! occurrence of `x.a`, this thunk is updated with `2`, and is not recomputed the second time.
-//!
-//! Newly introduced variables begin with a special character to avoid clashing with user-defined
-//! variables.
-use super::fresh_var;
-use crate::identifier::Ident;
-use crate::position::TermPos;
-use crate::term::{BindingType, MetaValue, RichTerm, Term};
-
-/// Transform the top-level term of an AST to a share normal form, if it can.
-///
-/// This function is not recursive: it just tries to apply one step of the transformation to
-/// the top-level node of the AST. For example, it transforms `[1 + 1, [1 + 2]]` to `let %0 = 1
-/// + 1 in [%0, [1 + 2]]`: the nested subterm `[1 + 2]` is left as it was. If the term is
-/// neither a record, a list nor an enriched value, it is returned the same.  In other words,
-/// the transformation is implemented as rewrite rules, and must be used in conjunction a
-/// traversal to obtain a full transformation.
-pub fn transform_one(rt: RichTerm) -> RichTerm {
-    let RichTerm { term, pos } = rt;
-    match *term {
-        Term::Record(map, attrs) => {
-            let mut bindings = Vec::with_capacity(map.len());
-
-            let map = map
-                .into_iter()
-                .map(|(id, t)| {
-                    if should_share(&t.term) {
-                        let fresh_var = fresh_var();
-                        let pos_t = t.pos;
-                        bindings.push((fresh_var.clone(), t));
-                        (id, RichTerm::new(Term::Var(fresh_var), pos_t))
-                    } else {
-                        (id, t)
-                    }
-                })
-                .collect();
-
-            with_bindings(Term::Record(map, attrs), bindings, pos, BindingType::Normal)
-        }
-        Term::RecRecord(map, dyn_fields, attrs) => {
-            // When a recursive record is evaluated, all fields need to be turned to closures
-            // anyway (see the corresponding case in `eval::eval()`), which is what the share
-            // normal form transformation does. This is why the test is more lax here than for
-            // other constructors: it is not only about sharing, but also about the future
-            // evaluation of recursive records. Only constant are not required to be
-            // closurized.
-            //
-            // In theory, the variable case is one exception: if the field is already a bare
-            // variable, it seems useless to add one more indirection through a generated
-            // variable. However, it is currently fundamental for recursive record merging that
-            // the sare normal form transformation ensure the following post-condition: the
-            // fields of recursive records contain either a constant or a *generated* variable,
-            // but never a user-supplied variable directly (the former starts with a special
-            // marker). See comments inside [`RichTerm::closurize`] for more details.
-            let mut bindings = Vec::with_capacity(map.len());
-
-            let map = map
-                .into_iter()
-                .map(|(id, t)| {
-                    // CHANGE THIS CONDITION CAREFULLY. Doing so can break the post-condition
-                    // explained above.
-                    if !t.as_ref().is_constant() {
-                        let fresh_var = fresh_var();
-                        let pos_t = t.pos;
-                        bindings.push((fresh_var.clone(), t));
-                        (id, RichTerm::new(Term::Var(fresh_var), pos_t))
-                    } else {
-                        (id, t)
-                    }
-                })
-                .collect();
-
-            let dyn_fields = dyn_fields
-                .into_iter()
-                .map(|(id_t, t)| {
-                    if !t.as_ref().is_constant() {
-                        let fresh_var = fresh_var();
-                        let pos_t = t.pos;
-                        bindings.push((fresh_var.clone(), t));
-                        (id_t, RichTerm::new(Term::Var(fresh_var), pos_t))
-                    } else {
-                        (id_t, t)
-                    }
-                })
-                .collect();
-
-            // Recursive records are the reason why we need revertible thunks, since when
-            // merged, we may have to revert the fields back to their original expression.
-            with_bindings(
-                Term::RecRecord(map, dyn_fields, attrs),
-                bindings,
-                pos,
-                BindingType::Revertible,
-            )
-        }
-        Term::List(ts) => {
-            let mut bindings = Vec::with_capacity(ts.len());
-
-            let ts = ts
-                .into_iter()
-                .map(|t| {
-                    if should_share(&t.term) {
-                        let fresh_var = fresh_var();
-                        let pos_t = t.pos;
-                        bindings.push((fresh_var.clone(), t));
-                        RichTerm::new(Term::Var(fresh_var), pos_t)
-                    } else {
-                        t
-                    }
-                })
-                .collect();
-
-            with_bindings(Term::List(ts), bindings, pos, BindingType::Normal)
-        }
-        Term::MetaValue(mut meta @ MetaValue { value: Some(_), .. }) => {
-            if meta.value.as_ref().map(|t| should_share(&t.term)).unwrap() {
-                let fresh_var = fresh_var();
-                let t = meta.value.take().unwrap();
-                meta.value
-                    .replace(RichTerm::new(Term::Var(fresh_var.clone()), t.pos));
-                let inner = RichTerm::new(Term::MetaValue(meta), pos);
-                RichTerm::new(Term::Let(fresh_var, t, inner, BindingType::Normal), pos)
-            } else {
-                RichTerm::new(Term::MetaValue(meta), pos)
-            }
-        }
-        t => RichTerm::new(t, pos),
-    }
-}
-
-/// Determine if a subterm of a WHNF should be wrapped in a thunk in order to be shared.
-///
-/// Sharing is typically useless if the subterm is already a WHNF which can be copied without
-/// duplicating any work. On the other hand, a WHNF which can contain other shareable
-/// subexpressions, such as a record, should be shared.
-fn should_share(t: &Term) -> bool {
-    match t {
-        Term::Null
-        | Term::Bool(_)
-        | Term::Num(_)
-        | Term::Str(_)
-        | Term::Lbl(_)
-        | Term::Sym(_)
-        | Term::Var(_)
-        | Term::Enum(_)
-        | Term::Fun(_, _) => false,
-        _ => true,
-    }
-}
-
-/// Bind a list of pairs `(identifier, term)` in a term.
-///
-/// Given the term `body` and bindings of identifiers to terms represented as a list of pairs
-/// `(id_1, term_1), .., (id_n, term_n)`, return the new term `let id_n = term_n in ... let
-/// id_1 = term_1 in body`.
-fn with_bindings(
-    body: Term,
-    bindings: Vec<(Ident, RichTerm)>,
-    pos: TermPos,
-    btype: BindingType,
-) -> RichTerm {
-    bindings
-        .into_iter()
-        .fold(RichTerm::new(body, pos.into_inherited()), |acc, (id, t)| {
-            RichTerm::new(Term::Let(id, t, acc, btype), pos)
-        })
-}
diff --git a/src/transformations.rs b/src/transformations.rs
new file mode 100644
index 00000000..2e84f774
--- /dev/null
+++ b/src/transformations.rs
@@ -0,0 +1,603 @@
+use crate::cache::ImportResolver;
+use crate::error::ImportError;
+use crate::eval::{Closure, Environment, IdentKind, Thunk};
+use crate::identifier::Ident;
+use crate::term::{Contract, RichTerm, Term, TraverseMethod};
+use crate::types::{AbsType, Types};
+use codespan::FileId;
+use simple_counter::*;
+use std::path::PathBuf;
+
+generate_counter!(FreshVarCounter, usize);
+
+/// # Desugarise destructuring
+///
+/// Replace a let-binding with destructuring by a classical let-binding.
+/// It will first destruct the pattern and create a new var for each field of the patternn.
+/// After that, it will construct a new Record/List from the extracted fields.
+///
+/// ## Example:
+///
+/// Taking the let pattern:
+/// ```text
+/// let x @ {a, b=d, ..} = {a=1,b=2,c="ignored"} in ...
+/// ```
+/// after transformation we will have:
+/// ```text
+/// let x = {a=1,b=2,c="ignored"} in
+/// let a = x.a in
+/// let d = x.b in
+/// ...
+/// ```
+pub mod desugar_destructuring {
+    use super::{Ident, RichTerm, Term};
+    use crate::destruct::{Destruct, Match};
+    use crate::term::make::{op1, op2};
+    use crate::term::{BinaryOp::DynRemove, BindingType, MetaValue, UnaryOp::StaticAccess};
+
+    /// Wrap the desugarized term in a meta value containing the "Record contract" needed to check
+    /// the pattern exaustivity and also fill the default values (`?` operator) if not presents in the record.
+    /// This function should be, in the general case, considered as the entry point of this
+    /// transformation.
+    pub fn desugar_with_contract(rt: RichTerm) -> RichTerm {
+        if let Term::LetPattern(x, pat, t_, body) = *rt.term {
+            let pos = body.pos;
+            let meta = pat.clone().as_contract();
+            let t_ = {
+                let t_pos = t_.pos;
+                RichTerm::new(
+                    Term::MetaValue(MetaValue {
+                        value: Some(t_),
+                        ..meta
+                    }),
+                    t_pos,
+                )
+            };
+            desugar(RichTerm::new(Term::LetPattern(x, pat, t_, body), pos))
+        } else {
+            rt
+        }
+    }
+
+    /// Main transformation function to desuggar let patterns.
+    /// WARNING: In a real usage case, you will want to generate also the matavalue associated to
+    /// this pattern destructuring. Do not concider this function as the entry point of the
+    /// transformation. For that, use `desugar_with_contract`.
+    pub fn desugar(rt: RichTerm) -> RichTerm {
+        if let Term::LetPattern(x, pat, t_, body) = *rt.term {
+            let pos = body.pos;
+            let x = x.unwrap_or_else(super::fresh_var);
+            RichTerm::new(
+                Term::Let(
+                    x.clone(),
+                    t_,
+                    destruct_term(x.clone(), &pat, bind_open_field(x, &pat, body)),
+                    BindingType::Normal,
+                ),
+                pos,
+            )
+        } else {
+            rt
+        }
+    }
+
+    /// Wrap `body` in a let construct binding the open part of the pattern to the required value.
+    /// Having `let {a,..y} = {a=1, b=2, c=3} in <BODY>` will bind `y` to {b=2,c=3} in `BODY`.
+    /// Here, the x, is the identifier pointing to the full record. If having `val @ {...} = ... in
+    /// ...` the param x should be `Ident("val")` but if we have a `@` binding less form, you will
+    /// probably generate a fresh variable.
+    fn bind_open_field(x: Ident, pat: &Destruct, body: RichTerm) -> RichTerm {
+        let (matches, var) = match pat {
+            Destruct::Record(matches, true, Some(x)) => (matches, x.clone()),
+            Destruct::Record(matches, true, None) => (matches, super::fresh_var()),
+            Destruct::Record(_, false, None) | Destruct::Empty => return body,
+            _ => panic!("A closed pattern can not have a rest binding"),
+        };
+        Term::Let(
+            var.clone(),
+            matches.iter().fold(Term::Var(x).into(), |x, m| match m {
+                Match::Simple(i, _) | Match::Assign(i, _, _) => {
+                    op2(DynRemove(), Term::Str(i.to_string()), x)
+                }
+            }),
+            body,
+            BindingType::Normal,
+        )
+        .into()
+    }
+
+    /// Core of the destructuring. Bind all the variables of the pattern except the "open" (`..y`)
+    /// part. For that, see `bind_open_field`.
+    fn destruct_term(x: Ident, pat: &Destruct, body: RichTerm) -> RichTerm {
+        let pos = body.pos;
+        match pat {
+            Destruct::Record(matches, ..) => matches.iter().fold(body, move |t, m| match m {
+                Match::Simple(id, _) => RichTerm::new(
+                    Term::Let(
+                        id.clone(),
+                        op1(StaticAccess(id.clone()), Term::Var(x.clone())),
+                        t,
+                        BindingType::Normal,
+                    ),
+                    pos,
+                ),
+                Match::Assign(f, _, (id, pat)) => desugar(RichTerm::new(
+                    Term::LetPattern(
+                        id.clone(),
+                        pat.clone(),
+                        op1(StaticAccess(f.clone()), Term::Var(x.clone())),
+                        t,
+                    ),
+                    pos,
+                )),
+            }),
+            _ => body,
+        }
+    }
+}
+
+/// Share normal form.
+///
+/// Replace the subexpressions of WHNFs that are not functions by thunks, such that they can be
+/// shared. It is similar to the behavior of other lazy languages with respect to data
+/// constructors.  To do so, subexpressions are replaced by fresh variables, introduced by new let
+/// bindings put at the beginning of the WHNF.
+///
+/// For example, take the expression
+/// ```text
+/// let x = {a = (1 + 1);} in x.a + x.a
+/// ```
+///
+/// The term `{a = 1 + 1;}` is a record, and hence a WHNF. In consequence, the thunk allocated to x
+/// is never updated. Without additional machinery, `a` will be recomputed each time is it used,
+/// two times here.
+///
+/// The transformation replaces such subexpressions, namely the content of the fields
+/// of records and the elements of lists - `(1 + 1)` in our example -, with fresh variables
+/// introduced by `let`  added at the head of the term:
+///
+/// ```text
+/// let x = (let var = 1 + 1 in {a = var;}) in x.a + x.a
+/// ```
+///
+/// Now, the field `a` points to the thunk introduced by `var`: at the evaluation of the first
+/// occurrence of `x.a`, this thunk is updated with `2`, and is not recomputed the second time.
+///
+/// Newly introduced variables begin with a special character to avoid clashing with user-defined
+/// variables.
+pub mod share_normal_form {
+    use super::fresh_var;
+    use crate::identifier::Ident;
+    use crate::position::TermPos;
+    use crate::term::{BindingType, MetaValue, RichTerm, Term};
+
+    /// Transform the top-level term of an AST to a share normal form, if it can.
+    ///
+    /// This function is not recursive: it just tries to apply one step of the transformation to
+    /// the top-level node of the AST. For example, it transforms `[1 + 1, [1 + 2]]` to `let %0 = 1
+    /// + 1 in [%0, [1 + 2]]`: the nested subterm `[1 + 2]` is left as it was. If the term is
+    /// neither a record, a list nor an enriched value, it is returned the same.  In other words,
+    /// the transformation is implemented as rewrite rules, and must be used in conjunction a
+    /// traversal to obtain a full transformation.
+    pub fn transform_one(rt: RichTerm) -> RichTerm {
+        let RichTerm { term, pos } = rt;
+        match *term {
+            Term::Record(map, attrs) => {
+                let mut bindings = Vec::with_capacity(map.len());
+
+                let map = map
+                    .into_iter()
+                    .map(|(id, t)| {
+                        if should_share(&t.term) {
+                            let fresh_var = fresh_var();
+                            let pos_t = t.pos;
+                            bindings.push((fresh_var.clone(), t));
+                            (id, RichTerm::new(Term::Var(fresh_var), pos_t))
+                        } else {
+                            (id, t)
+                        }
+                    })
+                    .collect();
+
+                with_bindings(Term::Record(map, attrs), bindings, pos, BindingType::Normal)
+            }
+            Term::RecRecord(map, dyn_fields, attrs) => {
+                // When a recursive record is evaluated, all fields need to be turned to closures
+                // anyway (see the corresponding case in `eval::eval()`), which is what the share
+                // normal form transformation does. This is why the test is more lax here than for
+                // other constructors: it is not only about sharing, but also about the future
+                // evaluation of recursive records. Only constant are not required to be
+                // closurized.
+                //
+                // In theory, the variable case is one exception: if the field is already a bare
+                // variable, it seems useless to add one more indirection through a generated
+                // variable. However, it is currently fundamental for recursive record merging that
+                // the sare normal form transformation ensure the following post-condition: the
+                // fields of recursive records contain either a constant or a *generated* variable,
+                // but never a user-supplied variable directly (the former starts with a special
+                // marker). See comments inside [`RichTerm::closurize`] for more details.
+                let mut bindings = Vec::with_capacity(map.len());
+
+                let map = map
+                    .into_iter()
+                    .map(|(id, t)| {
+                        // CHANGE THIS CONDITION CAREFULLY. Doing so can break the post-condition
+                        // explained above.
+                        if !t.as_ref().is_constant() {
+                            let fresh_var = fresh_var();
+                            let pos_t = t.pos;
+                            bindings.push((fresh_var.clone(), t));
+                            (id, RichTerm::new(Term::Var(fresh_var), pos_t))
+                        } else {
+                            (id, t)
+                        }
+                    })
+                    .collect();
+
+                let dyn_fields = dyn_fields
+                    .into_iter()
+                    .map(|(id_t, t)| {
+                        if !t.as_ref().is_constant() {
+                            let fresh_var = fresh_var();
+                            let pos_t = t.pos;
+                            bindings.push((fresh_var.clone(), t));
+                            (id_t, RichTerm::new(Term::Var(fresh_var), pos_t))
+                        } else {
+                            (id_t, t)
+                        }
+                    })
+                    .collect();
+
+                // Recursive records are the reason why we need revertible thunks, since when
+                // merged, we may have to revert the fields back to their original expression.
+                with_bindings(
+                    Term::RecRecord(map, dyn_fields, attrs),
+                    bindings,
+                    pos,
+                    BindingType::Revertible,
+                )
+            }
+            Term::List(ts) => {
+                let mut bindings = Vec::with_capacity(ts.len());
+
+                let ts = ts
+                    .into_iter()
+                    .map(|t| {
+                        if should_share(&t.term) {
+                            let fresh_var = fresh_var();
+                            let pos_t = t.pos;
+                            bindings.push((fresh_var.clone(), t));
+                            RichTerm::new(Term::Var(fresh_var), pos_t)
+                        } else {
+                            t
+                        }
+                    })
+                    .collect();
+
+                with_bindings(Term::List(ts), bindings, pos, BindingType::Normal)
+            }
+            Term::MetaValue(mut meta @ MetaValue { value: Some(_), .. }) => {
+                if meta.value.as_ref().map(|t| should_share(&t.term)).unwrap() {
+                    let fresh_var = fresh_var();
+                    let t = meta.value.take().unwrap();
+                    meta.value
+                        .replace(RichTerm::new(Term::Var(fresh_var.clone()), t.pos));
+                    let inner = RichTerm::new(Term::MetaValue(meta), pos);
+                    RichTerm::new(Term::Let(fresh_var, t, inner, BindingType::Normal), pos)
+                } else {
+                    RichTerm::new(Term::MetaValue(meta), pos)
+                }
+            }
+            t => RichTerm::new(t, pos),
+        }
+    }
+
+    /// Determine if a subterm of a WHNF should be wrapped in a thunk in order to be shared.
+    ///
+    /// Sharing is typically useless if the subterm is already a WHNF which can be copied without
+    /// duplicating any work. On the other hand, a WHNF which can contain other shareable
+    /// subexpressions, such as a record, should be shared.
+    fn should_share(t: &Term) -> bool {
+        match t {
+            Term::Null
+            | Term::Bool(_)
+            | Term::Num(_)
+            | Term::Str(_)
+            | Term::Lbl(_)
+            | Term::Sym(_)
+            | Term::Var(_)
+            | Term::Enum(_)
+            | Term::Fun(_, _) => false,
+            _ => true,
+        }
+    }
+
+    /// Bind a list of pairs `(identifier, term)` in a term.
+    ///
+    /// Given the term `body` and bindings of identifiers to terms represented as a list of pairs
+    /// `(id_1, term_1), .., (id_n, term_n)`, return the new term `let id_n = term_n in ... let
+    /// id_1 = term_1 in body`.
+    fn with_bindings(
+        body: Term,
+        bindings: Vec<(Ident, RichTerm)>,
+        pos: TermPos,
+        btype: BindingType,
+    ) -> RichTerm {
+        bindings
+            .into_iter()
+            .fold(RichTerm::new(body, pos.into_inherited()), |acc, (id, t)| {
+                RichTerm::new(Term::Let(id, t, acc, btype), pos)
+            })
+    }
+}
+
+pub mod import_resolution {
+    use super::{ImportResolver, PathBuf, RichTerm, Term};
+    use crate::error::ImportError;
+
+    /// Resolve the import if the term is an unresolved import, or return the term unchanged.
+    /// As [`share_normal_form::transform_one`](../share_normal_form/fn.transform_one.html),
+    /// this function is not recursive.
+    pub fn transform_one<R>(
+        rt: RichTerm,
+        resolver: &mut R,
+        parent: &Option<PathBuf>,
+    ) -> Result<RichTerm, ImportError>
+    where
+        R: ImportResolver,
+    {
+        let term = rt.as_ref();
+        match term {
+            Term::Import(path) => {
+                let (_, file_id) = resolver.resolve(path, parent.clone(), &rt.pos)?;
+                Ok(RichTerm::new(Term::ResolvedImport(file_id), rt.pos))
+            }
+            _ => Ok(rt),
+        }
+    }
+}
+
+/// During the evaluation, we the following invariant is enforced: any contract (be it the type
+/// annotation, or the contracts) contained in a `MetaValue` must have been applied to the inner
+/// value of this metavalue. This invariant is false just after parsing, as there's merely no
+/// direct `Assume` in the output AST. This transformation makes it true after program
+/// transformations by generating corresponding assume.
+///
+/// It must be run before `share_normal_form` to avoid rechecking contracts each time the inner
+/// value is unwrapped.
+pub mod apply_contracts {
+    use super::{RichTerm, Term};
+    use crate::mk_app;
+
+    /// If the top-level node of the AST is a meta-value, apply the meta-value's contracts to the
+    /// inner value.  Otherwise, return the term unchanged.
+    pub fn transform_one(rt: RichTerm) -> RichTerm {
+        let RichTerm { term, pos } = rt;
+
+        match *term {
+            Term::MetaValue(mut meta) if meta.value.is_some() => {
+                let inner = meta.types.iter().chain(meta.contracts.iter()).fold(
+                    meta.value.take().unwrap(),
+                    |acc, ctr| {
+                        mk_app!(
+                            ctr.types.clone().contract(),
+                            Term::Lbl(ctr.label.clone()),
+                            acc
+                        )
+                        .with_pos(pos.into_inherited())
+                    },
+                );
+
+                meta.value.replace(inner);
+                RichTerm::new(Term::MetaValue(meta), pos.into_inherited())
+            }
+            t => RichTerm::new(t, pos),
+        }
+    }
+}
+
+/// The state passed around during the imports resolution. It holds a reference to the import
+/// resolver, to a stack of pending imported term to be transformed and the path of the import
+/// currently being processed, if any.
+struct ImportsResolutionState<'a, R> {
+    resolver: &'a mut R,
+    stack: &'a mut Vec<FileId>,
+    parent: Option<PathBuf>,
+}
+
+/// Apply all program transformations, which are currently the share normal form transformations and
+/// contracts application.
+/// Do not perform transformation on the imported files.
+/// If needed, either do it yourself using pending imports returned by
+/// [`resolve_imports`](../fn.resolve_imports.html)
+/// or use the [`Cache`](../../cache/struct.Cache.html)
+pub fn transform(rt: RichTerm) -> RichTerm {
+    let rt = rt
+        .traverse(
+            &mut |rt: RichTerm, _| -> Result<RichTerm, ()> {
+                // before anything, we have to desugar the syntax
+                let rt = desugar_destructuring::desugar_with_contract(rt);
+                // We need to do contract generation before wrapping stuff in variables
+                let rt = apply_contracts::transform_one(rt);
+                Ok(rt)
+            },
+            &mut (),
+            TraverseMethod::TopDown,
+        )
+        .unwrap();
+    rt.traverse(
+        &mut |rt: RichTerm, _| -> Result<RichTerm, ()> {
+            let rt = share_normal_form::transform_one(rt);
+            Ok(rt)
+        },
+        &mut (),
+        TraverseMethod::BottomUp,
+    )
+    .unwrap()
+}
+
+/// import resolution.
+///
+/// All resolved imports are stacked during the process. Once the term has been traversed,
+/// the elements of this stack are returned. The caller is responsible
+/// to recursively resolve imports of this stack and or to perform
+/// transformations on it.
+pub fn resolve_imports<R>(
+    rt: RichTerm,
+    resolver: &mut R,
+) -> Result<(RichTerm, Vec<FileId>), ImportError>
+where
+    R: ImportResolver,
+{
+    let mut stack = Vec::new();
+
+    let source_file: Option<PathBuf> = rt.pos.as_opt_ref().map(|x| {
+        let path = resolver.get_path(x.src_id);
+        PathBuf::from(path)
+    });
+    let result = imports_pass(rt, resolver, &mut stack, source_file)?;
+
+    Ok((result, stack))
+}
+
+/// Perform one full imports resolution pass. Put all imports encountered for the first time in
+/// `stack`, but do not process them.
+fn imports_pass<R>(
+    rt: RichTerm,
+    resolver: &mut R,
+    stack: &mut Vec<FileId>,
+    parent: Option<PathBuf>,
+) -> Result<RichTerm, ImportError>
+where
+    R: ImportResolver,
+{
+    let mut state = ImportsResolutionState {
+        resolver,
+        stack,
+        parent,
+    };
+
+    // If an import is resolved, then stack it.
+    rt.traverse(
+        &mut |rt: RichTerm,
+              state: &mut ImportsResolutionState<R>|
+         -> Result<RichTerm, ImportError> {
+            let rt = import_resolution::transform_one(rt, state.resolver, &state.parent)?;
+
+            if let Term::ResolvedImport(file_id) = rt.term.as_ref() {
+                state.stack.push(*file_id);
+            }
+            Ok(rt)
+        },
+        &mut state,
+        TraverseMethod::BottomUp,
+    )
+}
+
+/// Generate a new fresh variable which do not clash with user-defined variables.
+pub fn fresh_var() -> Ident {
+    use crate::identifier::GEN_PREFIX;
+
+    format!("{}{}", GEN_PREFIX, FreshVarCounter::next()).into()
+}
+
+/// Structures which can be packed together with their environment as a closure.
+///
+/// The typical implementer is [`RichTerm`](../term/enum.RichTerm.html), but structures containing
+/// terms can also be closurizable, such as the contract in a [`Types`](../types/typ.Types.html).
+/// In this case, the inner term is closurized.
+pub trait Closurizable {
+    /// Pack a closurizable together with its environment `with_env` as a closure in the main
+    /// environment `env`.
+    fn closurize(self, env: &mut Environment, with_env: Environment) -> Self;
+}
+
+impl Closurizable for RichTerm {
+    /// Pack a term together with an environment as a closure.
+    ///
+    /// Generate a fresh variable, bind it to the corresponding closure `(t,with_env)` in `env`,
+    /// and return this variable as a fresh term.
+    fn closurize(self, env: &mut Environment, with_env: Environment) -> RichTerm {
+        // If the term is already a variable, we don't have to create a useless intermediate
+        // closure. We just transfer the original thunk to the new environment. This is not only an
+        // optimization: this is relied upon by recursive record merging when computing the
+        // fixpoint.
+        //
+        // More specifically, the evaluation of a recursive record patches the environment of each
+        // field with the thunks recursively referring to the other fields of the record. `eval`
+        // assumes that a recursive record field is either a constant or a generated variable whose
+        // thunks *immediately* contain the original unevaluated expression (both properties are
+        // true after the share normal form transformation and maintained when reverting thunks
+        // before merging recursive records).
+        //
+        // To maintain this invariant, `closurize` must NOT introduce an indirection through a
+        // variable, such as transforming:
+        //
+        // ```
+        // {foo = %1, bar = 1} in env %1 <- 1 + bar
+        // ```
+        //
+        // to:
+        //
+        // ```
+        // {foo = %2, bar = 1} in env %2 <- (%1 in env %1 <- 1 + bar)
+        // ```
+        //
+        // In this case, the evaluation of the recursive records will patch the outer environment
+        // instead of the inner one, giving:
+        //
+        // ```
+        // {foo = %2, bar = 1} in env %2 <- (%1 in env %1 <- 1 + bar), bar <- 1
+        // ```
+        //
+        // Then, evaluating `foo` would unduly raise an unbound identifier error.
+        //
+        //
+        // We currently only do this optimization for generated variables (introduced by the share
+        // normal form). We could do it for non-generated identifiers as well, but be we would be
+        // renaming user-supplied variables by gibberish generated names. It may hamper error
+        // reporting, so for the time being, we restrict ourselves to generated identifiers. Note
+        // that performing or not performing this optimization for user-supplied variables doesn't
+        // affect the invariant mentioned above, because the share normal form must ensure that the
+        // fields of a record all contain generated variables (or constant), but never
+        // user-supplied variables.
+        let var = fresh_var();
+        let pos = self.pos;
+
+        let thunk = match self.as_ref() {
+            Term::Var(id) if id.is_generated() => with_env.get(&id).expect(&format!(
+                "Internal error(closurize) : generated identifier {} not found in the environment",
+                id
+            )),
+            _ => {
+                let closure = Closure {
+                    body: self,
+                    env: with_env,
+                };
+                Thunk::new(closure, IdentKind::Record)
+            }
+        };
+
+        env.insert(var.clone(), thunk);
+        RichTerm::new(Term::Var(var), pos.into_inherited())
+    }
+}
+
+impl Closurizable for Types {
+    /// Pack the contract of a type together with an environment as a closure.
+    ///
+    /// Extract the underlying contract, closurize it and wrap it back as a flat type (an opaque
+    /// type defined by a custom contract).
+    fn closurize(self, env: &mut Environment, with_env: Environment) -> Types {
+        Types(AbsType::Flat(self.contract().closurize(env, with_env)))
+    }
+}
+
+impl Closurizable for Contract {
+    fn closurize(self, env: &mut Environment, with_env: Environment) -> Contract {
+        Contract {
+            types: self.types.closurize(env, with_env),
+            label: self.label,
+        }
+    }
+}
diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs
index db89a000..baac474a 100644
--- a/src/typecheck/mod.rs
+++ b/src/typecheck/mod.rs
@@ -650,8 +650,10 @@ fn type_check_<S, E>(
             envs.insert(x.clone(), ty_let);
             type_check_(state, envs, lin, linearizer, strict, rt, ty)
         }
-        Term::LetPattern(x, pat, re, _rt) => {
+        Term::LetPattern(x, pat, re, rt) => {
             use crate::destruct::*;
+            // TODO: The insertion of values in the type environment is done but everything is
+            // typed as `Dyn`.
             fn inject_pat_vars(pat: &Destruct, envs: &mut Envs) {
                 if let Destruct::Record(matches, _, rst) = pat {
                     if let Some(id) = rst {
@@ -661,12 +663,11 @@ fn type_check_<S, E>(
                         Match::Simple(id, ..) => {
                             envs.insert(id.clone(), TypeWrapper::Concrete(AbsType::Dyn()))
                         }
-                        Match::Assign(_, _, (bind_id, pat)) => {
-                            if let Some(id) = bind_id {
-                                envs.insert(id.clone(), TypeWrapper::Concrete(AbsType::Dyn()));
-                            }
+                        Match::Assign(id, _, (bind_id, pat)) => {
+                            let id = bind_id.as_ref().unwrap_or(id);
+                            envs.insert(id.clone(), TypeWrapper::Concrete(AbsType::Dyn()));
                             if !pat.is_empty() {
-                                inject_pat_vars(pat, envs);
+                                inject_pat_vars(&pat, envs);
                             }
                         }
                     });
@@ -683,13 +684,12 @@ fn type_check_<S, E>(
                 ty_let.clone(),
             )?;
 
-            // TODO typecheck the interior of the patern
             if let Some(x) = x {
+                linearizer.retype_ident(lin, x, ty_let.clone());
                 envs.insert(x.clone(), ty_let);
-                inject_pat_vars(pat, &mut envs);
             }
-            //type_check_(state, envs, strict, rt, ty)
-            Ok(())
+            inject_pat_vars(pat, &mut envs);
+            type_check_(state, envs, lin, linearizer, strict, rt, ty)
         }
         Term::App(e, t) => {
             let src = TypeWrapper::Ptr(new_var(state.table));
diff --git a/src/types.rs b/src/types.rs
index 8ac92f59..848cac87 100644
--- a/src/types.rs
+++ b/src/types.rs
@@ -179,7 +179,7 @@ impl Types {
         sy: &mut i32,
     ) -> RichTerm {
         use crate::stdlib::contracts;
-        use crate::transform::fresh_var;
+        use crate::transformations::fresh_var;
 
         let ctr = match self.0 {
             AbsType::Dyn() => contracts::dynamic(),


Test patch:
diff --git a/src/eval/tests.rs b/src/eval/tests.rs
deleted file mode 100644
index b0338b3f..00000000
--- a/src/eval/tests.rs
+++ /dev/null
@@ -1,355 +0,0 @@
-use super::*;
-use crate::cache::resolvers::{DummyResolver, SimpleResolver};
-use crate::error::ImportError;
-use crate::label::Label;
-use crate::parser::{grammar, lexer};
-use crate::term::make as mk_term;
-use crate::term::{BinaryOp, StrChunk, UnaryOp};
-use crate::transform::import_resolution::resolve_imports;
-use crate::{mk_app, mk_fun};
-use codespan::Files;
-
-/// Evaluate a term without import support.
-fn eval_no_import(t: RichTerm) -> Result<Term, EvalError> {
-    eval(t, &Environment::new(), &mut DummyResolver {}).map(Term::from)
-}
-
-fn parse(s: &str) -> Option<RichTerm> {
-    let id = Files::new().add("<test>", String::from(s));
-
-    grammar::TermParser::new()
-        .parse_term(id, lexer::Lexer::new(&s))
-        .map(RichTerm::without_pos)
-        .map_err(|err| println!("{:?}", err))
-        .ok()
-}
-
-#[test]
-fn identity_over_values() {
-    let num = Term::Num(45.3);
-    assert_eq!(Ok(num.clone()), eval_no_import(num.into()));
-
-    let boolean = Term::Bool(true);
-    assert_eq!(Ok(boolean.clone()), eval_no_import(boolean.into()));
-
-    let lambda = mk_fun!("x", mk_app!(mk_term::var("x"), mk_term::var("x")));
-    assert_eq!(Ok(lambda.as_ref().clone()), eval_no_import(lambda.into()));
-}
-
-#[test]
-fn blame_panics() {
-    let label = Label::dummy();
-    if let Err(EvalError::BlameError(l, ..)) =
-        eval_no_import(mk_term::op1(UnaryOp::Blame(), Term::Lbl(label.clone())))
-    {
-        assert_eq!(l, label);
-    } else {
-        panic!("This evaluation should've returned a BlameError!");
-    }
-}
-
-#[test]
-#[should_panic]
-fn lone_var_panics() {
-    eval_no_import(mk_term::var("unbound")).unwrap();
-}
-
-#[test]
-fn only_fun_are_applicable() {
-    eval_no_import(mk_app!(Term::Bool(true), Term::Num(45.))).unwrap_err();
-}
-
-#[test]
-fn simple_app() {
-    let t = mk_app!(mk_term::id(), Term::Num(5.0));
-    assert_eq!(Ok(Term::Num(5.0)), eval_no_import(t));
-}
-
-#[test]
-fn simple_let() {
-    let t = mk_term::let_in("x", Term::Num(5.0), mk_term::var("x"));
-    assert_eq!(Ok(Term::Num(5.0)), eval_no_import(t));
-}
-
-#[test]
-fn simple_ite() {
-    let t = mk_term::if_then_else(Term::Bool(true), Term::Num(5.0), Term::Bool(false));
-    assert_eq!(Ok(Term::Num(5.0)), eval_no_import(t));
-}
-
-#[test]
-fn simple_plus() {
-    let t = mk_term::op2(BinaryOp::Plus(), Term::Num(5.0), Term::Num(7.5));
-    assert_eq!(Ok(Term::Num(12.5)), eval_no_import(t));
-}
-
-#[test]
-fn asking_for_various_types() {
-    let num = mk_term::op1(UnaryOp::IsNum(), Term::Num(45.3));
-    assert_eq!(Ok(Term::Bool(true)), eval_no_import(num));
-
-    let boolean = mk_term::op1(UnaryOp::IsBool(), Term::Bool(true));
-    assert_eq!(Ok(Term::Bool(true)), eval_no_import(boolean));
-
-    let lambda = mk_term::op1(
-        UnaryOp::IsFun(),
-        mk_fun!("x", mk_app!(mk_term::var("x"), mk_term::var("x"))),
-    );
-    assert_eq!(Ok(Term::Bool(true)), eval_no_import(lambda));
-}
-
-fn mk_default(t: RichTerm) -> Term {
-    use crate::term::MergePriority;
-
-    let mut meta = MetaValue::from(t);
-    meta.priority = MergePriority::Default;
-    Term::MetaValue(meta)
-}
-
-fn mk_docstring<S>(t: RichTerm, s: S) -> Term
-where
-    S: Into<String>,
-{
-    let mut meta = MetaValue::from(t);
-    meta.doc.replace(s.into());
-    Term::MetaValue(meta)
-}
-
-#[test]
-fn enriched_terms_unwrapping() {
-    let t =
-        mk_default(mk_default(mk_docstring(Term::Bool(false).into(), "a").into()).into()).into();
-    assert_eq!(Ok(Term::Bool(false)), eval_no_import(t));
-}
-
-#[test]
-fn merge_enriched_default() {
-    let t = mk_term::op2(
-        BinaryOp::Merge(),
-        Term::Num(1.0),
-        mk_default(Term::Num(2.0).into()),
-    );
-    assert_eq!(Ok(Term::Num(1.0)), eval_no_import(t));
-}
-
-#[test]
-fn merge_incompatible_defaults() {
-    let t = mk_term::op2(
-        BinaryOp::Merge(),
-        mk_default(Term::Num(1.0).into()),
-        mk_default(Term::Num(2.0).into()),
-    );
-
-    eval_no_import(t).unwrap_err();
-}
-
-#[test]
-fn imports() {
-    let mut resolver = SimpleResolver::new();
-    resolver.add_source(String::from("two"), String::from("1 + 1"));
-    resolver.add_source(String::from("lib"), String::from("{f = true}"));
-    resolver.add_source(String::from("bad"), String::from("^$*/.23ab 0°@"));
-    resolver.add_source(
-        String::from("nested"),
-        String::from("let x = import \"two\" in x + 1"),
-    );
-    resolver.add_source(
-        String::from("cycle"),
-        String::from("let x = import \"cycle_b\" in {a = 1, b = x.a}"),
-    );
-    resolver.add_source(
-        String::from("cycle_b"),
-        String::from("let x = import \"cycle\" in {a = x.a}"),
-    );
-
-    fn mk_import<R>(
-        var: &str,
-        import: &str,
-        body: RichTerm,
-        resolver: &mut R,
-    ) -> Result<RichTerm, ImportError>
-    where
-        R: ImportResolver,
-    {
-        resolve_imports(
-            mk_term::let_in(var, mk_term::import(import), body),
-            resolver,
-        )
-        .map(|(t, _)| t)
-    }
-
-    // let x = import "does_not_exist" in x
-    match mk_import("x", "does_not_exist", mk_term::var("x"), &mut resolver).unwrap_err() {
-        ImportError::IOError(_, _, _) => (),
-        _ => assert!(false),
-    };
-
-    // let x = import "bad" in x
-    match mk_import("x", "bad", mk_term::var("x"), &mut resolver).unwrap_err() {
-        ImportError::ParseErrors(_, _) => (),
-        _ => assert!(false),
-    };
-
-    // let x = import "two" in x
-    assert_eq!(
-        eval(
-            mk_import("x", "two", mk_term::var("x"), &mut resolver).unwrap(),
-            &Environment::new(),
-            &mut resolver
-        )
-        .map(Term::from)
-        .unwrap(),
-        Term::Num(2.0)
-    );
-
-    // let x = import "lib" in x.f
-    assert_eq!(
-        eval(
-            mk_import(
-                "x",
-                "lib",
-                mk_term::op1(UnaryOp::StaticAccess(Ident::from("f")), mk_term::var("x")),
-                &mut resolver,
-            )
-            .unwrap(),
-            &Environment::new(),
-            &mut resolver
-        )
-        .map(Term::from)
-        .unwrap(),
-        Term::Bool(true)
-    );
-}
-
-#[test]
-fn interpolation_simple() {
-    let mut chunks = vec![
-        StrChunk::Literal(String::from("Hello")),
-        StrChunk::expr(
-            mk_term::op2(
-                BinaryOp::StrConcat(),
-                mk_term::string(", "),
-                mk_term::string("World!"),
-            )
-            .into(),
-        ),
-        StrChunk::Literal(String::from(" How")),
-        StrChunk::expr(mk_term::if_then_else(
-            Term::Bool(true),
-            mk_term::string(" are"),
-            mk_term::string(" is"),
-        )),
-        StrChunk::Literal(String::from(" you?")),
-    ];
-    chunks.reverse();
-
-    let t: RichTerm = Term::StrChunks(chunks).into();
-    assert_eq!(
-        eval_no_import(t),
-        Ok(Term::Str(String::from("Hello, World! How are you?")))
-    );
-}
-
-#[test]
-fn interpolation_nested() {
-    let mut inner_chunks = vec![
-        StrChunk::Literal(String::from(" How")),
-        StrChunk::expr(
-            Term::Op2(
-                BinaryOp::StrConcat(),
-                mk_term::string(" ar"),
-                mk_term::string("e"),
-            )
-            .into(),
-        ),
-        StrChunk::expr(mk_term::if_then_else(
-            Term::Bool(true),
-            mk_term::string(" you"),
-            mk_term::string(" me"),
-        )),
-    ];
-    inner_chunks.reverse();
-
-    let mut chunks = vec![
-        StrChunk::Literal(String::from("Hello, World!")),
-        StrChunk::expr(Term::StrChunks(inner_chunks).into()),
-        StrChunk::Literal(String::from("?")),
-    ];
-    chunks.reverse();
-
-    let t: RichTerm = Term::StrChunks(chunks).into();
-    assert_eq!(
-        eval_no_import(t),
-        Ok(Term::Str(String::from("Hello, World! How are you?")))
-    );
-}
-
-#[test]
-fn global_env() {
-    let mut global_env = Environment::new();
-    let mut resolver = DummyResolver {};
-    global_env.insert(
-        Ident::from("g"),
-        Thunk::new(
-            Closure::atomic_closure(Term::Num(1.0).into()),
-            IdentKind::Let,
-        ),
-    );
-
-    let t = mk_term::let_in("x", Term::Num(2.0), mk_term::var("x"));
-    assert_eq!(
-        eval(t, &global_env, &mut resolver).map(Term::from),
-        Ok(Term::Num(2.0))
-    );
-
-    let t = mk_term::let_in("x", Term::Num(2.0), mk_term::var("g"));
-    assert_eq!(
-        eval(t, &global_env, &mut resolver).map(Term::from),
-        Ok(Term::Num(1.0))
-    );
-
-    // Shadowing of global environment
-    let t = mk_term::let_in("g", Term::Num(2.0), mk_term::var("g"));
-    assert_eq!(
-        eval(t, &global_env, &mut resolver).map(Term::from),
-        Ok(Term::Num(2.0))
-    );
-}
-
-fn mk_env(bindings: Vec<(&str, RichTerm)>) -> Environment {
-    bindings
-        .into_iter()
-        .map(|(id, t)| {
-            (
-                id.into(),
-                Thunk::new(Closure::atomic_closure(t), IdentKind::Let),
-            )
-        })
-        .collect()
-}
-
-#[test]
-fn substitution() {
-    let global_env = mk_env(vec![
-        ("glob1", Term::Num(1.0).into()),
-        ("glob2", parse("\"Glob2\"").unwrap()),
-        ("glob3", Term::Bool(false).into()),
-    ]);
-    let env = mk_env(vec![
-        ("loc1", Term::Bool(true).into()),
-        ("loc2", parse("if glob3 then glob1 else glob2").unwrap()),
-    ]);
-
-    let t = parse("let x = 1 in if loc1 then 1 + loc2 else glob3").unwrap();
-    assert_eq!(
-        subst(t, &global_env, &env),
-        parse("let x = 1 in if true then 1 + (if false then 1 else \"Glob2\") else false").unwrap()
-    );
-
-    let t = parse("switch {`x => [1, glob1], `y => loc2, `z => {id = true, other = glob3}} loc1")
-        .unwrap();
-    assert_eq!(
-        subst(t, &global_env, &env),
-        parse("switch {`x => [1, 1], `y => (if false then 1 else \"Glob2\"), `z => {id = true, other = false}} true").unwrap()
-    );
-}
diff --git a/tests/destructuring.rs b/tests/destructuring.rs
index 8b39ca72..740eb0ac 100644
--- a/tests/destructuring.rs
+++ b/tests/destructuring.rs
@@ -1,5 +1,5 @@
 use assert_matches::assert_matches;
-use nickel::error::{Error, EvalError};
+use nickel::error::{Error, EvalError, TypecheckError};
 use nickel::term::Term;
 
 use utilities::eval_file;
@@ -56,7 +56,7 @@ fn mixed() {
 fn assign_fail() {
     assert_matches!(
         eval_file("destructuring/assign_fail.ncl"),
-        Err(Error::EvalError(EvalError::UnboundIdentifier(..)))
+        Err(Error::TypecheckError(TypecheckError::UnboundIdentifier(..)))
     );
 }