Make substitution into a macro.

6 files changed, 599 insertions, 300 deletions

diff --git a/Cargo.toml b/Cargo.toml
index 2fe9469..ae907a5 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -5,9 +5,12 @@ authors = ["Greg Brown <gmb60@cam.ac.uk>"]
 edition = "2018"
 
 [dependencies]
-proc-macro2 = "1.0.24"
 quote = "1.0.7"
 
+[dependencies.proc-macro2]
+version = "1.0.24"
+features = ["span-locations"]
+
 [dependencies.syn]
 version = "1.0.48"
 features = ["extra-traits"]
diff --git a/src/ast/convert.rs b/src/ast/convert.rs
index 7ae3147..8051c90 100644
--- a/src/ast/convert.rs
+++ b/src/ast/convert.rs
@@ -1,32 +1,28 @@
 use std::borrow::Borrow;
 use std::collections::HashMap;
 use std::hash::Hash;
-use std::mem;
-use std::rc::Rc;
 
 use super::Term;
 
 #[derive(Debug, Default)]
+/// The variable context for converting a concrete syntax tree to an abstract
+/// one.
+///
+/// There are two name scopes in a context. Bindings are used by fixed points.
+/// Variables are formal parameters of macros.
 pub struct Context {
     bindings: Vec<String>,
-    variables: HashMap<String, Term>,
-    functions: HashMap<String, (Rc<dyn Convert>, Vec<String>)>,
+    variables: HashMap<String, usize>,
 }
 
 impl Context {
-    /// # Examples
-    /// ```
-    /// use chomp::ast::convert::Context;
-    ///
-    /// let context = Context::new();
-    /// assert_eq!(context.get("x"), None);
-    /// assert_eq!(context.get("y"), None);
-    /// assert_eq!(context.get("z"), None);
-    /// ```
+    /// Creates a new variable context. No names are bound.
     pub fn new() -> Self {
         Self::default()
     }
 
+    /// Returns [`Some`] index of a binding `name`.
+    ///
     /// # Errors
     /// Returns [`None`] if `name.is_empty()` or if `name` is unbound.
     ///
@@ -34,18 +30,18 @@ impl Context {
     /// ```
     /// use chomp::ast::convert::Context;
     ///
-    /// let context = Context::new();
-    /// assert_eq!(context.get("x"), None);
+    /// let mut context = Context::new();
+    /// assert_eq!(context.get_binding("x"), None);
     ///
-    /// context.push("x".to_owned(), |c| {
-    ///     assert_eq!(c.get("x"), Some(0));
+    /// context.with_binding("x".to_owned(), |c| {
+    ///     assert_eq!(c.get_binding("x"), Some(0));
     ///
-    ///     c.push("y".to_owned(), |c| {
-    ///         assert_eq!(c.get("x"), Some(1));
+    ///     c.with_binding("y".to_owned(), |c| {
+    ///         assert_eq!(c.get_binding("x"), Some(1));
     ///     })
     /// });
     ///
-    /// assert_eq!(context.get("x"), None);
+    /// assert_eq!(context.get_binding("x"), None);
     /// ```
     pub fn get_binding<T: ?Sized + PartialEq<str>>(&self, name: &T) -> Option<usize> {
         let mut iter = self.bindings.iter();
@@ -66,6 +62,8 @@ impl Context {
         None
     }
 
+    /// Adds a binding `name` for the duration of the function `f`.
+    ///
     /// # Panics
     /// If `name.is_empty()`.
     ///
@@ -73,16 +71,16 @@ impl Context {
     /// ```
     /// use chomp::ast::convert::Context;
     ///
-    /// let context = Context::new();
-    /// assert_eq!(context.get("x"), None);
+    /// let mut context = Context::new();
+    /// assert_eq!(context.get_binding("x"), None);
     ///
-    /// context.push("x".to_owned(), |c| {
-    ///     assert_eq!(c.get("x"), Some(0));
+    /// context.with_binding("x".to_owned(), |c| {
+    ///     assert_eq!(c.get_binding("x"), Some(0));
     /// });
     ///
-    /// assert_eq!(context.get("x"), None);
+    /// assert_eq!(context.get_binding("x"), None);
     /// ```
-    pub fn push_binding<F: FnOnce(&mut Self) -> T, T>(&mut self, name: String, f: F) -> T {
+    pub fn with_binding<F: FnOnce(&mut Self) -> T, T>(&mut self, name: String, f: F) -> T {
         if name.is_empty() {
             panic!()
         }
@@ -93,86 +91,63 @@ impl Context {
         res
     }
 
+    /// Returns [`Some`] index of a variable `name`.
+    ///
     /// # Errors
     /// If `name == "".to_owned().borrow()` or `name` is unbound.
-    pub fn get_variable<T: ?Sized + Hash + Eq>(&self, name: &T) -> Option<&Term>
+    ///
+    /// # Examples
+    /// ```
+    /// use chomp::ast::convert::Context;
+    ///
+    /// let mut ctx = Context::new();
+    /// assert_eq!(ctx.get_variable("x"), None);
+    ///
+    /// ctx.set_variables(vec!["x".to_owned(), "y".to_owned()]);
+    /// assert_eq!(ctx.get_variable("x"), Some(0));
+    /// assert_eq!(ctx.get_variable("y"), Some(1));
+    ///
+    /// ctx.set_variables(vec![]);
+    /// assert_eq!(ctx.get_variable("x"), None);
+    /// ```
+    pub fn get_variable<T: ?Sized + Hash + Eq>(&self, name: &T) -> Option<usize>
     where
         String: Borrow<T>,
     {
         if name == "".to_owned().borrow() {
-            return None
-        }
-
-        self.variables.get(name)
-    }
-
-    /// # Panics
-    /// If any variable name is empty.
-    pub fn add_function(&mut self, name: String, source: Rc<dyn Convert>, variables: Vec<String>) {
-        if variables.iter().any(|s| s.is_empty()) {
-            panic!()
+            return None;
         }
 
-        self.functions.insert(name, (source, variables));
+        self.variables.get(name).copied()
     }
 
-    /// This uses dynamic scope for bindings.
-    /// # Errors
-    /// If `name` is unbound or has been called with the wrong number of arguments.
-    pub fn call_function<I: IntoIterator<Item = Term>, T: ?Sized + Hash + Eq>(
-        &mut self,
-        name: &T,
-        args: I,
-        convert_mode: ConvertMode,
-    ) -> Option<Term>
-    where
-        String: Borrow<T>,
-        <I as IntoIterator>::IntoIter: ExactSizeIterator,
-    {
-        let (term, vars) = self.functions.get(name)?;
-        let args_iter = args.into_iter();
-
-        if vars.len() != args_iter.len() {
-            None
-        } else {
-            let mut old = Vec::new();
-            for (var, value) in vars.clone().into_iter().zip(args_iter) {
-                if let Some((old_name, old_value)) = self.variables.remove_entry(var.borrow()) {
-                    let mut indices = Vec::new();
-
-                    for (index, binding) in self.bindings.iter_mut().enumerate() {
-                        if *binding == old_name {
-                            indices.push((index, mem::take(binding)));
-                        }
-                    }
-
-                    old.push((old_name, old_value, indices))
-                }
-
-                self.variables.insert(var, value);
-            }
-
-            let res = Some(term.clone().convert(self, convert_mode));
-
-            for (name, value, indices) in old {
-                for (index, binding) in indices {
-                    self.bindings[index] = binding
-                }
-
-                self.variables.insert(name, value);
-            }
-
-            res
-        }
+    /// Reassigns all variable indices based off of their position in `args`.
+    ///
+    /// # Examples
+    /// ```
+    /// use chomp::ast::convert::Context;
+    ///
+    /// let mut ctx = Context::new();
+    /// assert_eq!(ctx.get_variable("x"), None);
+    ///
+    /// ctx.set_variables(vec!["x".to_owned(), "y".to_owned()]);
+    /// assert_eq!(ctx.get_variable("x"), Some(0));
+    /// assert_eq!(ctx.get_variable("y"), Some(1));
+    ///
+    /// ctx.set_variables(vec![]);
+    /// assert_eq!(ctx.get_variable("x"), None);
+    /// ```
+    pub fn set_variables<I: IntoIterator<Item = String>>(&mut self, args: I) {
+        self.variables = args
+            .into_iter()
+            .enumerate()
+            .map(|(index, name)| (name, index))
+            .collect();
     }
 }
 
-#[derive(Clone, Copy, Debug, Eq, PartialEq)]
-pub enum ConvertMode {
-    NoSubstitution,
-    WithSubstitution,
-}
-
-pub trait Convert: std::fmt::Debug {
-    fn convert(&self, context: &mut Context, mode: ConvertMode) -> Term;
+/// Used to convert a concrete term into an abstract term.
+pub trait Convert {
+    /// Performs the conversion.
+    fn convert(&self, context: &mut Context) -> Term;
 }
diff --git a/src/ast/mod.rs b/src/ast/mod.rs
index 1537904..ea14d6e 100644
--- a/src/ast/mod.rs
+++ b/src/ast/mod.rs
@@ -89,20 +89,37 @@ impl From<CatError> for syn::Error {
 impl Display for CatError {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         match self {
-            Self::FirstNullable { punct, fst_span, fst, .. } => {
+            Self::FirstNullable {
+                punct,
+                fst_span,
+                fst,
+                ..
+            } => {
                 let start = punct.start();
                 let fst_start = fst_span.start();
-                write!(f, "{}:{}: term '{}' ({}:{}) accepts the empty string", start.line, start.column, fst, fst_start.line, fst_start.column)
+                write!(
+                    f,
+                    "{}:{}: term '{}' ({}:{}) accepts the empty string",
+                    start.line, start.column, fst, fst_start.line, fst_start.column
+                )
             }
-            Self::FirstFlastOverlap { punct, fst, fst_span, snd, snd_span, .. } => {
-                let start =punct.start();
+            Self::FirstFlastOverlap {
+                punct,
+                fst,
+                fst_span,
+                snd,
+                snd_span,
+                ..
+            } => {
+                let start = punct.start();
                 let fst_start = fst_span.start();
                 let snd_start = snd_span.start();
                 write!(
                 f,
                 "{}:{}: cannot decide whether to repeat '{}' ({}:{}) or start accepting '{}' ({}:{}).",
                 start.line, start.column, fst, fst_start.line, fst_start.column, snd, snd_start.line, snd_start.column
-            )},
+            )
+            }
         }
     }
 }
@@ -185,24 +202,54 @@ impl From<AltError> for syn::Error {
 impl Display for AltError {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         match self {
-            Self::BothNullable { punct, left_span, left, right_span, right, .. } => {
+            Self::BothNullable {
+                punct,
+                left_span,
+                left,
+                right_span,
+                right,
+                ..
+            } => {
                 let start = punct.start();
                 let left_start = left_span.start();
                 let right_start = right_span.start();
                 write!(
-                f,
-                "{}:{}: both '{}' ({}:{}) and '{}' ({}:{}) accept the empty string.",
-                start.line, start.column, left, left_start.line, left_start.column, right, right_start.line, right_start.column,
-            )},
-            Self::FirstOverlap { punct, left_span,left, right_span, right, .. } => {
+                    f,
+                    "{}:{}: both '{}' ({}:{}) and '{}' ({}:{}) accept the empty string.",
+                    start.line,
+                    start.column,
+                    left,
+                    left_start.line,
+                    left_start.column,
+                    right,
+                    right_start.line,
+                    right_start.column,
+                )
+            }
+            Self::FirstOverlap {
+                punct,
+                left_span,
+                left,
+                right_span,
+                right,
+                ..
+            } => {
                 let start = punct.start();
                 let left_start = left_span.start();
                 let right_start = right_span.start();
                 write!(
-                f,
-                "{}:{}: cannot decide whether to accept '{}' ({}:{}) or '{}' ({}:{}).",
-                start.line, start.column, left, left_start.line, left_start.column, right, right_start.line, right_start.column,
-            )},
+                    f,
+                    "{}:{}: cannot decide whether to accept '{}' ({}:{}) or '{}' ({}:{}).",
+                    start.line,
+                    start.column,
+                    left,
+                    left_start.line,
+                    left_start.column,
+                    right,
+                    right_start.line,
+                    right_start.column,
+                )
+            }
         }
     }
 }
@@ -254,34 +301,44 @@ impl Variable {
 }
 
 #[derive(Debug)]
-pub enum VariableError {
-    FreeVariable(Variable),
-    GuardedVariable(Variable),
+pub enum BindingError {
+    FreeBinding(Variable),
+    GuardedBinding(Variable),
 }
 
-impl From<VariableError> for syn::Error {
-    fn from(other: VariableError) -> Self {
+impl From<BindingError> for syn::Error {
+    fn from(other: BindingError) -> Self {
         match other {
-            VariableError::FreeVariable(_) => todo!(),
-            VariableError::GuardedVariable(_) => todo!(),
+            BindingError::FreeBinding(_) => todo!(),
+            BindingError::GuardedBinding(_) => todo!(),
         }
     }
 }
 
-impl Display for VariableError {
+impl Display for BindingError {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         match self {
-            Self::FreeVariable(var) => {
+            Self::FreeBinding(var) => {
                 let start = var.name.span().start();
-                write!(f, "{}:{}: unbound variable '{}'", start.line, start.column, var.name)},
-            Self::GuardedVariable(var) => {
+                write!(
+                    f,
+                    "{}:{}: unbound binding '{}'",
+                    start.line, start.column, var.name
+                )
+            }
+            Self::GuardedBinding(var) => {
                 let start = var.name.span().start();
-                write!(f, "{}:{}: variable '{}' is guarded", start.line, start.column, var.name)},
+                write!(
+                    f,
+                    "{}:{}: binding '{}' is guarded",
+                    start.line, start.column, var.name
+                )
+            }
         }
     }
 }
 
-impl Error for VariableError {}
+impl Error for BindingError {}
 
 #[derive(Clone, Debug)]
 pub struct Call {
@@ -303,6 +360,7 @@ pub enum Term {
     Cat(Cat),
     Alt(Alt),
     Fix(Fix),
+    Binding(Variable),
     Variable(Variable),
     Call(Call),
 }
@@ -315,7 +373,8 @@ impl Term {
             Self::Cat(cat) => visitor.visit_cat(cat),
             Self::Alt(alt) => visitor.visit_alt(alt),
             Self::Fix(fix) => visitor.visit_fix(fix),
-            Self::Variable(variable) => visitor.visit_variable(variable),
+            Self::Binding(bind) => visitor.visit_binding(bind),
+            Self::Variable(var) => visitor.visit_variable(var),
             Self::Call(call) => visitor.visit_call(call),
         }
     }
@@ -327,7 +386,8 @@ impl Term {
             Self::Cat(cat) => visitor.visit_mut_cat(cat),
             Self::Alt(alt) => visitor.visit_mut_alt(alt),
             Self::Fix(fix) => visitor.visit_mut_fix(fix),
-            Self::Variable(variable) => visitor.visit_mut_variable(variable),
+            Self::Binding(bind) => visitor.visit_mut_binding(bind),
+            Self::Variable(var) => visitor.visit_mut_variable(var),
             Self::Call(call) => visitor.visit_mut_call(call),
         }
     }
@@ -339,7 +399,8 @@ impl Term {
             Self::Cat(cat) => folder.fold_cat(cat),
             Self::Alt(alt) => folder.fold_alt(alt),
             Self::Fix(fix) => folder.fold_fix(fix),
-            Self::Variable(variable) => folder.fold_variable(variable),
+            Self::Binding(bind) => folder.fold_binding(bind),
+            Self::Variable(var) => folder.fold_variable(var),
             Self::Call(call) => folder.fold_call(call),
         }
     }
@@ -349,7 +410,7 @@ impl Term {
 pub enum TermError {
     Cat(CatError),
     Alt(AltError),
-    Variable(VariableError),
+    Binding(BindingError),
 }
 
 impl From<Never> for TermError {
@@ -370,9 +431,9 @@ impl From<AltError> for TermError {
     }
 }
 
-impl From<VariableError> for TermError {
-    fn from(other: VariableError) -> Self {
-        Self::Variable(other)
+impl From<BindingError> for TermError {
+    fn from(other: BindingError) -> Self {
+        Self::Binding(other)
     }
 }
 
@@ -381,7 +442,7 @@ impl From<TermError> for syn::Error {
         match other {
             TermError::Cat(e) => e.into(),
             TermError::Alt(e) => e.into(),
-            TermError::Variable(e) => e.into(),
+            TermError::Binding(e) => e.into(),
         }
     }
 }
@@ -391,7 +452,7 @@ impl Display for TermError {
         match self {
             Self::Cat(e) => e.fmt(f),
             Self::Alt(e) => e.fmt(f),
-            Self::Variable(e) => e.fmt(f),
+            Self::Binding(e) => e.fmt(f),
         }
     }
 }
@@ -410,6 +471,8 @@ pub trait Visitor {
 
     fn visit_fix(&mut self, fix: &Fix) -> Self::Out;
 
+    fn visit_binding(&mut self, bind: &Variable) -> Self::Out;
+
     fn visit_variable(&mut self, var: &Variable) -> Self::Out;
 
     fn visit_call(&mut self, call: &Call) -> Self::Out;
@@ -422,6 +485,7 @@ pub trait VisitorMut {
     fn visit_mut_cat(&mut self, cat: &mut Cat) -> Self::Out;
     fn visit_mut_alt(&mut self, alt: &mut Alt) -> Self::Out;
     fn visit_mut_fix(&mut self, fix: &mut Fix) -> Self::Out;
+    fn visit_mut_binding(&mut self, bind: &mut Variable) -> Self::Out;
     fn visit_mut_variable(&mut self, var: &mut Variable) -> Self::Out;
     fn visit_mut_call(&mut self, call: &mut Call) -> Self::Out;
 }
@@ -433,6 +497,7 @@ pub trait Folder {
     fn fold_cat(&mut self, cat: Cat) -> Self::Out;
     fn fold_alt(&mut self, alt: Alt) -> Self::Out;
     fn fold_fix(&mut self, fix: Fix) -> Self::Out;
+    fn fold_binding(&mut self, bind: Variable) -> Self::Out;
     fn fold_variable(&mut self, var: Variable) -> Self::Out;
     fn fold_call(&mut self, call: Call) -> Self::Out;
 }
@@ -465,8 +530,12 @@ impl Visitor for Closed {
         res
     }
 
-    fn visit_variable(&mut self, var: &Variable) -> Self::Out {
-        self.0 > var.index
+    fn visit_binding(&mut self, bind: &Variable) -> Self::Out {
+        self.0 > bind.index
+    }
+
+    fn visit_variable(&mut self, _var: &Variable) -> Self::Out {
+        true
     }
 
     fn visit_call(&mut self, call: &Call) -> Self::Out {
@@ -477,7 +546,7 @@ impl Visitor for Closed {
 struct Nullable<'a>(NullContext<'a>);
 
 impl Visitor for Nullable<'_> {
-    type Out = Result<bool, VariableError>;
+    type Out = Result<bool, BindingError>;
 
     fn visit_epsilon(&mut self, _: &Epsilon) -> Self::Out {
         Ok(true)
@@ -515,14 +584,18 @@ impl Visitor for Nullable<'_> {
         })
     }
 
-    fn visit_variable(&mut self, var: &Variable) -> Self::Out {
-        match self.0.is_guarded(var.index) {
-            None => Err(VariableError::FreeVariable(var.clone())),
-            Some(true) => Err(VariableError::GuardedVariable(var.clone())),
-            Some(false) => Ok(self.0.is_nullable(var.index).unwrap()),
+    fn visit_binding(&mut self, bind: &Variable) -> Self::Out {
+        match self.0.is_guarded(bind.index) {
+            None => Err(BindingError::FreeBinding(bind.clone())),
+            Some(true) => Err(BindingError::GuardedBinding(bind.clone())),
+            Some(false) => Ok(self.0.is_nullable(bind.index).unwrap()),
         }
     }
 
+    fn visit_variable(&mut self, _var: &Variable) -> Self::Out {
+        todo!()
+    }
+
     fn visit_call(&mut self, _call: &Call) -> Self::Out {
         todo!()
     }
@@ -531,7 +604,7 @@ impl Visitor for Nullable<'_> {
 struct FirstSet<'a>(FirstContext<'a>);
 
 impl Visitor for FirstSet<'_> {
-    type Out = Result<typed::FirstSet, VariableError>;
+    type Out = Result<typed::FirstSet, BindingError>;
 
     fn visit_epsilon(&mut self, _: &Epsilon) -> Self::Out {
         Ok(typed::FirstSet::new())
@@ -569,14 +642,18 @@ impl Visitor for FirstSet<'_> {
         })
     }
 
-    fn visit_variable(&mut self, var: &Variable) -> Self::Out {
-        match self.0.is_guarded(var.index) {
-            None => Err(VariableError::FreeVariable(var.clone())),
-            Some(true) => Err(VariableError::GuardedVariable(var.clone())),
-            Some(false) => Ok(self.0.first_set(var.index).unwrap().clone()),
+    fn visit_binding(&mut self, bind: &Variable) -> Self::Out {
+        match self.0.is_guarded(bind.index) {
+            None => Err(BindingError::FreeBinding(bind.clone())),
+            Some(true) => Err(BindingError::GuardedBinding(bind.clone())),
+            Some(false) => Ok(self.0.first_set(bind.index).unwrap().clone()),
         }
     }
 
+    fn visit_variable(&mut self, _var: &Variable) -> Self::Out {
+        todo!()
+    }
+
     fn visit_call(&mut self, _call: &Call) -> Self::Out {
         todo!()
     }
@@ -585,7 +662,7 @@ impl Visitor for FirstSet<'_> {
 struct FlastSet<'a>(&'a mut FlastContext);
 
 impl Visitor for FlastSet<'_> {
-    type Out = Result<typed::FlastSet, VariableError>;
+    type Out = Result<typed::FlastSet, BindingError>;
 
     fn visit_epsilon(&mut self, _: &Epsilon) -> Self::Out {
         Ok(typed::FlastSet::new())
@@ -629,14 +706,18 @@ impl Visitor for FlastSet<'_> {
         })
     }
 
-    fn visit_variable(&mut self, var: &Variable) -> Self::Out {
-        match self.0.is_guarded(var.index) {
-            None => Err(VariableError::FreeVariable(var.clone())),
-            Some(true) => Err(VariableError::GuardedVariable(var.clone())),
-            Some(false) => Ok(self.0.flast_set(var.index).unwrap().clone()),
+    fn visit_binding(&mut self, bind: &Variable) -> Self::Out {
+        match self.0.is_guarded(bind.index) {
+            None => Err(BindingError::FreeBinding(bind.clone())),
+            Some(true) => Err(BindingError::GuardedBinding(bind.clone())),
+            Some(false) => Ok(self.0.flast_set(bind.index).unwrap().clone()),
         }
     }
 
+    fn visit_variable(&mut self, _var: &Variable) -> Self::Out {
+        todo!()
+    }
+
     fn visit_call(&mut self, _call: &Call) -> Self::Out {
         todo!()
     }
@@ -671,6 +752,10 @@ impl Visitor for Spanning {
         fix.span
     }
 
+    fn visit_binding(&mut self, var: &Variable) -> Self::Out {
+        var.name.span()
+    }
+
     fn visit_variable(&mut self, var: &Variable) -> Self::Out {
         var.name.span()
     }
@@ -811,7 +896,8 @@ impl Folder for TypeCheck {
         let flast_set = FlastSet(&mut self.0).visit_fix(&fix)?;
         let span = Spanning.visit_fix(&fix);
 
-        self.0.push_flast_set(nullable, first_set.clone(), flast_set.clone());
+        self.0
+            .push_flast_set(nullable, first_set.clone(), flast_set.clone());
         let (inner, _) = fix.inner.fold(self)?;
         self.0.pop_flast_set();
 
@@ -828,12 +914,12 @@ impl Folder for TypeCheck {
         ))
     }
 
-    fn fold_variable(&mut self, var: Variable) -> Self::Out {
-        let nullable = Nullable(self.0.as_null()).visit_variable(&var)?;
-        let first_set = FirstSet(self.0.as_first()).visit_variable(&var)?;
-        let flast_set = FlastSet(&mut self.0).visit_variable(&var)?;
-        let span = Spanning.visit_variable(&var);
-        let kind = TypeKind::Variable(var.index);
+    fn fold_binding(&mut self, bind: Variable) -> Self::Out {
+        let nullable = Nullable(self.0.as_null()).visit_binding(&bind)?;
+        let first_set = FirstSet(self.0.as_first()).visit_binding(&bind)?;
+        let flast_set = FlastSet(&mut self.0).visit_binding(&bind)?;
+        let span = Spanning.visit_binding(&bind);
+        let kind = TypeKind::Binding(bind.index);
 
         Ok((
             Typed {
@@ -846,11 +932,297 @@ impl Folder for TypeCheck {
         ))
     }
 
-    fn fold_call(&mut self, call: Call) -> Self::Out {
+    fn fold_variable(&mut self, _var: Variable) -> Self::Out {
+        todo!()
+    }
+
+    fn fold_call(&mut self, _call: Call) -> Self::Out {
+        todo!()
+    }
+}
+
+struct DeepenVars(usize);
+
+impl VisitorMut for DeepenVars {
+    type Out = ();
+
+    fn visit_mut_epsilon(&mut self, _: &mut Epsilon) -> Self::Out {}
+
+    fn visit_mut_literal(&mut self, _: &mut Literal) -> Self::Out {}
+
+    fn visit_mut_cat(&mut self, cat: &mut Cat) -> Self::Out {
+        cat.fst.visit_mut(self);
+        cat.snd.visit_mut(self);
+    }
+
+    fn visit_mut_alt(&mut self, alt: &mut Alt) -> Self::Out {
+        alt.left.visit_mut(self);
+        alt.right.visit_mut(self);
+    }
+
+    fn visit_mut_fix(&mut self, fix: &mut Fix) -> Self::Out {
+        self.0 += 1;
+        fix.inner.visit_mut(self);
+        self.0 -= 1;
+    }
+
+    fn visit_mut_binding(&mut self, bind: &mut Variable) -> Self::Out {
+        if bind.index >= self.0 {
+            bind.index += 1;
+        }
+    }
+
+    fn visit_mut_variable(&mut self, _: &mut Variable) -> Self::Out {}
+
+    fn visit_mut_call(&mut self, call: &mut Call) -> Self::Out {
+        for arg in &mut call.args {
+            arg.visit_mut(self);
+        }
+    }
+}
+
+struct ShallowVars(usize);
+
+impl VisitorMut for ShallowVars {
+    type Out = ();
+
+    fn visit_mut_epsilon(&mut self, _: &mut Epsilon) -> Self::Out {}
+
+    fn visit_mut_literal(&mut self, _: &mut Literal) -> Self::Out {}
+
+    fn visit_mut_cat(&mut self, cat: &mut Cat) -> Self::Out {
+        cat.fst.visit_mut(self);
+        cat.snd.visit_mut(self);
+    }
+
+    fn visit_mut_alt(&mut self, alt: &mut Alt) -> Self::Out {
+        alt.left.visit_mut(self);
+        alt.right.visit_mut(self);
+    }
+
+    fn visit_mut_fix(&mut self, fix: &mut Fix) -> Self::Out {
+        self.0 += 1;
+        fix.inner.visit_mut(self);
+        self.0 -= 1;
+    }
+
+    fn visit_mut_binding(&mut self, bind: &mut Variable) -> Self::Out {
+        if bind.index > self.0 {
+            bind.index -= 1;
+        }
+    }
+
+    fn visit_mut_variable(&mut self, _: &mut Variable) -> Self::Out {
         todo!()
     }
+
+    fn visit_mut_call(&mut self, call: &mut Call) -> Self::Out {
+        for arg in &mut call.args {
+            arg.visit_mut(self);
+        }
+    }
+}
+
+struct Substitute(Vec<Term>);
+
+impl Folder for Substitute {
+    type Out = Result<Term, SubstituteError>;
+
+    fn fold_epsilon(&mut self, eps: Epsilon) -> Self::Out {
+        Ok(Term::Epsilon(eps))
+    }
+
+    fn fold_literal(&mut self, lit: Literal) -> Self::Out {
+        Ok(Term::Literal(lit))
+    }
+
+    fn fold_cat(&mut self, cat: Cat) -> Self::Out {
+        let fst = cat.fst.fold(self)?;
+        let snd = cat.snd.fold(self)?;
+        Ok(Term::Cat(Cat {
+            fst: Box::new(fst),
+            punct: cat.punct,
+            snd: Box::new(snd),
+        }))
+    }
+
+    fn fold_alt(&mut self, alt: Alt) -> Self::Out {
+        let left = alt.left.fold(self)?;
+        let right = alt.right.fold(self)?;
+        Ok(Term::Alt(Alt {
+            left: Box::new(left),
+            punct: alt.punct,
+            right: Box::new(right),
+        }))
+    }
+
+    fn fold_fix(&mut self, fix: Fix) -> Self::Out {
+        for var in &mut self.0 {
+            var.visit_mut(&mut DeepenVars(0));
+        }
+        let inner = fix.inner.fold(self)?;
+        for var in &mut self.0 {
+            var.visit_mut(&mut ShallowVars(0));
+        }
+        Ok(Term::Fix(Fix {
+            span: fix.span,
+            arg: fix.arg,
+            inner: Box::new(inner),
+        }))
+    }
+
+    fn fold_binding(&mut self, var: Variable) -> Self::Out {
+        Ok(Term::Binding(var))
+    }
+
+    fn fold_call(&mut self, call: Call) -> Self::Out {
+        let args = call
+            .args
+            .into_iter()
+            .map(|arg| arg.fold(self))
+            .collect::<Result<_, _>>()?;
+        Ok(Term::Call(Call {
+            span: call.span,
+            name: call.name,
+            args,
+        }))
+    }
+
+    fn fold_variable(&mut self, var: Variable) -> Self::Out {
+        self.0
+            .get(var.index)
+            .cloned()
+            .ok_or(SubstituteError::FreeVariable(var))
+    }
+}
+
+#[derive(Clone, Debug)]
+pub struct InlineCall {
+    name: String,
+    term: Term,
+    args: usize,
+}
+
+impl InlineCall {
+    pub fn new(name: Ident, term: Term, args: usize) -> Self {
+        Self {
+            name: name.to_string(),
+            term,
+            args,
+        }
+    }
+}
+
+impl Folder for InlineCall {
+    type Out = Result<Term, SubstituteError>;
+
+    fn fold_epsilon(&mut self, eps: Epsilon) -> Self::Out {
+        Ok(Term::Epsilon(eps))
+    }
+
+    fn fold_literal(&mut self, lit: Literal) -> Self::Out {
+        Ok(Term::Literal(lit))
+    }
+
+    fn fold_cat(&mut self, cat: Cat) -> Self::Out {
+        let fst = cat.fst.fold(self)?;
+        let snd = cat.snd.fold(self)?;
+        Ok(Term::Cat(Cat {
+            fst: Box::new(fst),
+            punct: cat.punct,
+            snd: Box::new(snd),
+        }))
+    }
+
+    fn fold_alt(&mut self, alt: Alt) -> Self::Out {
+        let left = alt.left.fold(self)?;
+        let right = alt.right.fold(self)?;
+        Ok(Term::Alt(Alt {
+            left: Box::new(left),
+            punct: alt.punct,
+            right: Box::new(right),
+        }))
+    }
+
+    fn fold_fix(&mut self, fix: Fix) -> Self::Out {
+        let inner = fix.inner.fold(self)?;
+        Ok(Term::Fix(Fix {
+            span: fix.span,
+            arg: fix.arg,
+            inner: Box::new(inner),
+        }))
+    }
+
+    fn fold_binding(&mut self, bind: Variable) -> Self::Out {
+        Ok(Term::Binding(bind))
+    }
+
+    fn fold_variable(&mut self, var: Variable) -> Self::Out {
+        Ok(Term::Variable(var))
+    }
+
+    fn fold_call(&mut self, call: Call) -> Self::Out {
+        if call.name != self.name {
+            let args = call
+                .args
+                .into_iter()
+                .map(|arg| arg.fold(self))
+                .collect::<Result<_, _>>()?;
+            Ok(Term::Call(Call {
+                span: call.span,
+                name: call.name,
+                args,
+            }))
+        } else if call.args.len() != self.args {
+            Err(SubstituteError::WrongArgCount {
+                call,
+                expected: self.args,
+            })
+        } else {
+            let args = call
+                .args
+                .into_iter()
+                .map(|arg| arg.fold(self))
+                .collect::<Result<_, _>>()?;
+            self.term.clone().fold(&mut Substitute(args))
+        }
+    }
 }
 
+#[derive(Debug)]
+pub enum SubstituteError {
+    FreeVariable(Variable),
+    WrongArgCount { call: Call, expected: usize },
+}
+
+impl Display for SubstituteError {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            Self::FreeVariable(var) => {
+                let start = var.name.span().start();
+                write!(
+                    f,
+                    "{}:{}: undeclared variable '{}'",
+                    start.line, start.column, var.name
+                )
+            }
+            SubstituteError::WrongArgCount { call, expected } => {
+                let start = call.span.start();
+                write!(
+                    f,
+                    "{}:{}: wrong number of arguments. Expected {}, got {}",
+                    start.line,
+                    start.column,
+                    call.args.len(),
+                    expected
+                )
+            }
+        }
+    }
+}
+
+impl Error for SubstituteError {}
+
 #[derive(Clone, Debug, Eq, PartialEq, Hash)]
 enum TypeKind {
     Epsilon,
@@ -858,7 +1230,7 @@ enum TypeKind {
     Cat(Box<Typed>, Box<Typed>),
     Alt(Box<Typed>, Box<Typed>),
     Fix(Box<Typed>),
-    Variable(usize),
+    Binding(usize),
 }
 
 #[derive(Debug)]
@@ -909,7 +1281,7 @@ impl TypeKind {
                 } = *inner;
                 context.fix(inner_kind)
             }
-            Self::Variable(index) => context.variable(index),
+            Self::Binding(index) => context.variable(index),
         }
     }
 }
@@ -922,7 +1294,7 @@ impl Display for TypeKind {
             Self::Cat(fst, snd) => write!(f, "{}.{}", fst, snd),
             Self::Alt(left, right) => write!(f, "({} | {})", left, right),
             Self::Fix(inner) => write!(f, "[]({})", inner),
-            Self::Variable(index) => write!(f, "{}", index),
+            Self::Binding(index) => write!(f, "{}", index),
         }
     }
 }
diff --git a/src/ast/typed.rs b/src/ast/typed.rs
index 6533e0a..b81253e 100644
--- a/src/ast/typed.rs
+++ b/src/ast/typed.rs
@@ -1,7 +1,3 @@
-use proc_macro2::Span;
-
-use super::Typed;
-use super::VariableError;
 use std::collections::BTreeSet;
 
 #[derive(Clone, Debug, Default, Eq, PartialEq, Hash)]
@@ -190,8 +186,8 @@ impl FirstContext<'_> {
 
 #[derive(Debug, Default)]
 pub struct FlastContext {
-    data: Vec<(bool, FirstSet, FlastSet)>,
-    guard: Vec<usize>,
+    binds: Vec<(bool, FirstSet, FlastSet)>,
+    unguard_points: Vec<usize>,
 }
 
 impl FlastContext {
@@ -200,16 +196,16 @@ impl FlastContext {
     }
 
     pub fn depth(&self) -> usize {
-        self.data.len()
+        self.binds.len()
     }
 
     pub fn is_guarded(&self, index: usize) -> Option<bool> {
-        if self.data.len() <= index {
+        if self.binds.len() <= index {
             None
-        } else if self.guard.is_empty() {
+        } else if self.unguard_points.is_empty() {
             Some(true)
         } else {
-            Some(self.guard[self.guard.len() - 1] + index < self.data.len())
+            Some(self.unguard_points[self.unguard_points.len() - 1] + index < self.binds.len())
         }
     }
 
@@ -221,40 +217,40 @@ impl FlastContext {
     }
 
     pub(crate) fn unguard(&mut self) {
-        self.guard.push(self.data.len());
+        self.unguard_points.push(self.binds.len());
     }
 
     pub(crate) fn guard(&mut self) {
-        self.guard.pop();
+        self.unguard_points.pop();
     }
 
     fn is_nullable(&self, index: usize) -> Option<bool> {
-        self.data.get(index).map(|(null, _, _)| *null)
+        self.binds.get(index).map(|(null, _, _)| *null)
     }
 
     fn push_nullable(&mut self, nullable: bool) {
-        self.data
+        self.binds
             .push((nullable, FirstSet::default(), FlastSet::default()))
     }
 
     fn pop_nullable(&mut self) {
-        self.data.pop();
+        self.binds.pop();
     }
 
     fn first_set(&self, index: usize) -> Option<&FirstSet> {
-        self.data.get(index).map(|(_, first, _)| first)
+        self.binds.get(index).map(|(_, first, _)| first)
     }
 
     fn push_first_set(&mut self, nullable: bool, first_set: FirstSet) {
-        self.data.push((nullable, first_set, FlastSet::default()))
+        self.binds.push((nullable, first_set, FlastSet::default()))
     }
 
     fn pop_first_set(&mut self) {
-        self.data.pop();
+        self.binds.pop();
     }
 
     pub fn flast_set(&self, index: usize) -> Option<&FlastSet> {
-        self.data.get(index).map(|(_, _, flast)| flast)
+        self.binds.get(index).map(|(_, _, flast)| flast)
     }
 
     pub fn with_flast_set<F: FnOnce(&mut Self) -> R, R>(
@@ -271,11 +267,11 @@ impl FlastContext {
     }
 
     pub(crate) fn push_flast_set(&mut self, nullable: bool, first_set: FirstSet, flast_set: FlastSet) {
-        self.data.push((nullable, first_set, flast_set));
+        self.binds.push((nullable, first_set, flast_set));
     }
 
     pub(crate) fn pop_flast_set(&mut self) {
-        self.data.pop();
+        self.binds.pop();
     }
 
     pub fn as_first(&mut self) -> FirstContext<'_> {
@@ -286,31 +282,3 @@ impl FlastContext {
         NullContext { inner: self }
     }
 }
-
-pub trait Type {
-    type Err: Into<syn::Error>;
-
-    /// # Errors
-    /// Returns [`Err`] if there is a variable with an index greater than or equal
-    /// to `depth`.
-    fn closed(&self, depth: usize) -> Result<(), VariableError>;
-
-    /// # Errors
-    /// Returns [`None`] only if `self.closed(context.get_depth())` returns an
-    /// [`Err`].
-    fn is_nullable(&self, context: &mut NullContext<'_>) -> Option<bool>;
-
-    /// # Errors
-    /// Returns [`None`] only if `self.closed(context.get_depth())` returns an
-    /// [`Err`].
-    fn first_set(&self, context: &mut FirstContext<'_>) -> Option<FirstSet>;
-
-    /// # Errors
-    /// Returns [`None`] only if `self.closed(context.get_depth())` returns an
-    /// [`Err`].
-    fn flast_set(&self, context: &mut FlastContext) -> Option<FlastSet>;
-
-    /// # Errors
-    /// Returns an [`Err`] if this term is not well typed.
-    fn well_typed(self, context: &mut FlastContext) -> Result<(Typed, Span), Self::Err>;
-}
diff --git a/src/main.rs b/src/main.rs
index 7c4babd..5026085 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -1,3 +1,4 @@
+use chomp::ast::InlineCall;
 use chomp::{ast::TypeCheck, nibble::File};
 use proc_macro2::Span;
 use std::{
@@ -14,9 +15,16 @@ fn main() {
         .map_err(|e| Box::new(e) as Box<dyn Error>)
         .and_then(|_| syn::parse_str(&input).map_err(|e| Box::new(e) as Box<dyn Error>))
         .and_then(|nibble: File| {
-            dbg!(nibble
-                .convert_with_substitution())
-                .fold(&mut TypeCheck::new())
+            let (funs, goal) = nibble.convert();
+
+            funs.into_iter()
+                .try_rfold(goal, |goal, (name, term, args)| {
+                    goal.fold(&mut InlineCall::new(name, term, args))
+                })
+                .map_err(|e| Box::new(e) as Box<dyn Error>)
+        })
+        .and_then(|term| {
+            term.fold(&mut TypeCheck::new())
                 .map_err(|e| Box::new(e) as Box<dyn Error>)
         })
         .map(|(typed, _)| typed.emit_code(Ident::new("Ast", Span::call_site())))
diff --git a/src/nibble/mod.rs b/src/nibble/mod.rs
index 427569d..59788e6 100644
--- a/src/nibble/mod.rs
+++ b/src/nibble/mod.rs
@@ -1,6 +1,6 @@
+use std::collections::HashMap;
 use std::rc::Rc;
 
-use crate::ast::convert::ConvertMode;
 use crate::ast::{
     self,
     convert::{Context, Convert},
@@ -16,7 +16,7 @@ use syn::{
 pub type Epsilon = Token![_];
 
 impl Convert for Epsilon {
-    fn convert(&self, _: &mut Context, _: ConvertMode) -> ast::Term {
+    fn convert(&self, _: &mut Context) -> ast::Term {
         ast::Term::Epsilon(*self)
     }
 }
@@ -24,31 +24,17 @@ impl Convert for Epsilon {
 type Ident = syn::Ident;
 
 impl Convert for Ident {
-    fn convert(&self, context: &mut Context, mode: ConvertMode) -> ast::Term {
+    fn convert(&self, context: &mut Context) -> ast::Term {
         use ast::Term;
         let name = self.to_string();
 
-        if let Some(variable) = context.get_binding(&name) {
+        if let Some(binding) = context.get_binding(&name) {
+            Term::Binding(ast::Variable::new(self.clone(), binding))
+        } else if let Some(variable) = context.get_variable(&name) {
             Term::Variable(ast::Variable::new(self.clone(), variable))
         } else {
-            match mode {
-                ConvertMode::NoSubstitution => {
-                    let span = self.span();
-                    Term::Call(ast::Call::new(self.clone(), Vec::new(), span))
-                }
-                ConvertMode::WithSubstitution => {
-                    if let Some(term) = context.get_variable(&name) {
-                        term.clone()
-                    } else if let Some(term) =
-                        context.call_function(&name, std::iter::empty(), mode)
-                    {
-                        term
-                    } else {
-                        let span = self.span();
-                        Term::Call(ast::Call::new(self.clone(), Vec::new(), span))
-                    }
-                }
-            }
+            let span = self.span();
+            Term::Call(ast::Call::new(self.clone(), Vec::new(), span))
         }
     }
 }
@@ -56,7 +42,7 @@ impl Convert for Ident {
 type Literal = syn::LitStr;
 
 impl Convert for Literal {
-    fn convert(&self, _: &mut Context, _: ConvertMode) -> ast::Term {
+    fn convert(&self, _: &mut Context) -> ast::Term {
         ast::Term::Literal(self.clone())
     }
 }
@@ -71,6 +57,10 @@ impl<T> ArgList<T> {
     fn span(&self) -> Span {
         self.paren_token.span
     }
+
+    fn len(&self) -> usize {
+        self.args.len()
+    }
 }
 
 impl<T> IntoIterator for ArgList<T> {
@@ -115,28 +105,15 @@ impl Parse for Call {
 }
 
 impl Convert for Call {
-    fn convert(&self, context: &mut Context, mode: ConvertMode) -> ast::Term {
+    fn convert(&self, context: &mut Context) -> ast::Term {
         use ast::Term;
         let args = self
             .args
             .clone()
             .into_iter()
-            .map(|arg| arg.convert(context, mode))
+            .map(|arg| arg.convert(context))
             .collect::<Vec<_>>();
-        match mode {
-            ConvertMode::NoSubstitution => {
-                Term::Call(ast::Call::new(self.name.clone(), args, self.span()))
-            }
-            ConvertMode::WithSubstitution => {
-                if let Some(term) =
-                    context.call_function(&self.name.to_string(), args.clone(), mode)
-                {
-                    term
-                } else {
-                    Term::Call(ast::Call::new(self.name.clone(), args, self.span()))
-                }
-            }
-        }
+        Term::Call(ast::Call::new(self.name.clone(), args, self.span()))
     }
 }
 
@@ -175,14 +152,14 @@ impl Parse for Fix {
 }
 
 impl Convert for Fix {
-    fn convert(&self, context: &mut Context, mode: ConvertMode) -> ast::Term {
+    fn convert(&self, context: &mut Context) -> ast::Term {
         use ast::Term;
         let span = self.span();
         let expr = &self.expr;
         let arg_name = self.arg.to_string();
         Term::Fix(ast::Fix::new(
             self.arg.clone(),
-            context.push_binding(arg_name, |ctx| expr.convert(ctx, mode)),
+            context.with_binding(arg_name, |ctx| expr.convert(ctx)),
             span,
         ))
     }
@@ -210,8 +187,8 @@ impl Parse for ParenExpression {
 }
 
 impl Convert for ParenExpression {
-    fn convert(&self, context: &mut Context, mode: ConvertMode) -> ast::Term {
-        self.expr.convert(context, mode)
+    fn convert(&self, context: &mut Context) -> ast::Term {
+        self.expr.convert(context)
     }
 }
 
@@ -267,14 +244,14 @@ impl Parse for Term {
 }
 
 impl Convert for Term {
-    fn convert(&self, context: &mut Context, mode: ConvertMode) -> ast::Term {
+    fn convert(&self, context: &mut Context) -> ast::Term {
         match self {
-            Self::Epsilon(e) => e.convert(context, mode),
-            Self::Ident(i) => i.convert(context, mode),
-            Self::Literal(l) => l.convert(context, mode),
-            Self::Call(c) => c.convert(context, mode),
-            Self::Fix(f) => f.convert(context, mode),
-            Self::Parens(e) => e.convert(context, mode),
+            Self::Epsilon(e) => e.convert(context),
+            Self::Ident(i) => i.convert(context),
+            Self::Literal(l) => l.convert(context),
+            Self::Call(c) => c.convert(context),
+            Self::Fix(f) => f.convert(context),
+            Self::Parens(e) => e.convert(context),
         }
     }
 }
@@ -314,25 +291,20 @@ impl Parse for Cat {
 }
 
 impl Convert for Cat {
-    fn convert(&self, context: &mut Context, mode: ConvertMode) -> ast::Term {
+    fn convert(&self, context: &mut Context) -> ast::Term {
         use ast::Term;
         let mut iter = self.terms.pairs();
         let init = match iter.next().unwrap() {
-            Pair::Punctuated(t, p) => Ok((t.convert(context, mode), p)),
-            Pair::End(t) => Err(t.convert(context, mode)),
+            Pair::Punctuated(t, p) => Ok((t.convert(context), p)),
+            Pair::End(t) => Err(t.convert(context)),
         };
         iter.fold(init, |term, pair| {
             let (fst, punct) = term.unwrap();
             match pair {
-                Pair::Punctuated(t, p) => Ok((
-                    Term::Cat(ast::Cat::new(fst, *punct, t.convert(context, mode))),
-                    p,
-                )),
-                Pair::End(t) => Err(Term::Cat(ast::Cat::new(
-                    fst,
-                    *punct,
-                    t.convert(context, mode),
-                ))),
+                Pair::Punctuated(t, p) => {
+                    Ok((Term::Cat(ast::Cat::new(fst, *punct, t.convert(context))), p))
+                }
+                Pair::End(t) => Err(Term::Cat(ast::Cat::new(fst, *punct, t.convert(context)))),
             }
         })
         .unwrap_err()
@@ -374,25 +346,21 @@ impl Parse for Alt {
 }
 
 impl Convert for Alt {
-    fn convert(&self, context: &mut Context, mode: ConvertMode) -> ast::Term {
+    fn convert(&self, context: &mut Context) -> ast::Term {
         use ast::Term;
         let mut iter = self.cats.pairs();
         let init = match iter.next().unwrap() {
-            Pair::Punctuated(t, p) => Ok((t.convert(context, mode), p)),
-            Pair::End(t) => Err(t.convert(context, mode)),
+            Pair::Punctuated(t, p) => Ok((t.convert(context), p)),
+            Pair::End(t) => Err(t.convert(context)),
         };
         iter.fold(init, |cat, pair| {
             let (left, punct) = cat.unwrap();
             match pair {
                 Pair::Punctuated(t, p) => Ok((
-                    Term::Alt(ast::Alt::new(left, *punct, t.convert(context, mode))),
+                    Term::Alt(ast::Alt::new(left, *punct, t.convert(context))),
                     p,
                 )),
-                Pair::End(t) => Err(Term::Alt(ast::Alt::new(
-                    left,
-                    *punct,
-                    t.convert(context, mode),
-                ))),
+                Pair::End(t) => Err(Term::Alt(ast::Alt::new(left, *punct, t.convert(context)))),
             }
         })
         .unwrap_err()
@@ -457,20 +425,25 @@ pub struct File {
 }
 
 impl File {
-    pub fn convert_with_substitution(self) -> ast::Term {
+    /// Returns function list and the goal. The function list consists of an
+    /// [`Ident`], the converted [`ast::Term`] and the number of arguments.
+    pub fn convert(self) -> (Vec<(Ident, ast::Term, usize)>, ast::Term) {
         let mut context = Context::new();
-        for statement in self.lets {
-            context.add_function(
-                statement.name.to_string(),
-                Rc::new(statement.expr),
-                statement
-                    .args
-                    .map(|args| args.into_iter().map(|arg| arg.to_string()).collect())
-                    .unwrap_or_default(),
-            );
-        }
-
-        self.goal.expr.convert(&mut context, ConvertMode::WithSubstitution)
+        let map = self
+            .lets
+            .into_iter()
+            .map(|stmt| {
+                let count = stmt.args.as_ref().map(ArgList::len).unwrap_or_default();
+                context.set_variables(
+                    stmt.args
+                        .into_iter()
+                        .flat_map(|args| args.into_iter().map(|arg| arg.to_string())),
+                );
+                (stmt.name, stmt.expr.convert(&mut context), count)
+            })
+            .collect();
+        let goal = self.goal.expr.convert(&mut context);
+        (map, goal)
     }
 }