// Alpha-equivalence utilities.
// Based on https://repository.library.northeastern.edu/files/neu:cj82mb52h

// `freshen` gets a value ready for destructuring.
// `freshen_rec` gets a value and its pattern ready for destructuring.

use crate::{
    ast::{Ast, AstContents::*},
    name::*,
    util::{assoc::Assoc, mbe::EnvMBE},
};

// A renaming that only affects names at the "current" quotation level
#[derive(Clone, Debug, PartialEq)]
pub struct Ren {
    env: Assoc<Name, Ast>,
    env_phaseless: Assoc<Name, Ast>,
    q_lev: i16,
}

impl Ren {
    pub fn find(&self, n: Name) -> Option<&Ast> {
        if self.q_lev == 0 {
            self.env.find(&n).or_else(|| self.env_phaseless.find(&n))
        } else {
            self.env_phaseless.find(&n)
        }
    }
    pub fn unset(self, n: Name) -> Ren {
        if self.q_lev == 0 {
            Ren {
                env: self.env.unset(&n),
                env_phaseless: self.env_phaseless.unset(&n),
                q_lev: self.q_lev,
            }
        } else {
            self
        }
    }
    pub fn set_assoc(self, other: &Ren) -> Ren {
        if self.q_lev == other.q_lev {
            Ren {
                env: self.env.set_assoc(&other.env),
                env_phaseless: self.env_phaseless.set_assoc(&other.env_phaseless),
                q_lev: self.q_lev,
            }
        } else {
            self
        }
    }
    pub fn q_more(&self, by: u8) -> Ren {
        Ren { q_lev: self.q_lev + i16::from(by), ..self.clone() }
    }
    pub fn q_less(&self, by: u8) -> Ren {
        Ren { q_lev: self.q_lev - i16::from(by), ..self.clone() }
    }
    pub fn new() -> Ren { Ren { env: Assoc::new(), env_phaseless: Assoc::new(), q_lev: 0 } }
    pub fn single(n: Name, a: Ast) -> Ren { Ren { env: Assoc::new().set(n, a), ..Ren::new() } }
    pub fn become_phaseless(self) -> Ren {
        // TODO: which order is right? What could even cause shadowing between these things?
        Ren {
            env_phaseless: self.env_phaseless.set_assoc(&self.env),
            env: Assoc::new(),
            q_lev: self.q_lev,
        }
    }

    /// For debugging: find a freshening based on `orig_sp` (the never-fresehened spelling).
    pub fn find_orig(&self, orig: &str) -> Option<(Name, Ast)> {
        for (k, v) in self.env.iter_pairs() {
            if k.orig_sp() == orig {
                return Some((*k, v.clone()));
            }
        }
        for (k, v) in self.env_phaseless.iter_pairs() {
            if k.orig_sp() == orig {
                return Some((*k, v.clone()));
            }
        }
        None
    }
}

impl From<Assoc<Name, Ast>> for Ren {
    fn from(a: Assoc<Name, Ast>) -> Ren { Ren { env: a, ..Ren::new() } }
}

fn substitute_rec(node: &Ast, cur_node_contents: &EnvMBE<Ast>, env: &Ren) -> Ast {
    match node.c() {
        Node(ref f, ref new_parts, ref export) => {
            // let new_cnc = parts.clone();
            node.with_c(Node(
                f.clone(),
                new_parts.marched_map(&mut |_, marched_parts: &EnvMBE<Ast>, part: &Ast| {
                    substitute_rec(part, marched_parts, env)
                }),
                export.clone(),
            ))
        }
        VariableReference(n) => env.find(*n).unwrap_or(&node.clone()).clone(),
        ExtendEnv(ref body, ref beta) => {
            let mut new_env = env.clone();
            for bound_name in crate::beta::bound_from_beta(beta, cur_node_contents, 0) {
                new_env = new_env.unset(bound_name);
            }

            node.with_c(ExtendEnv(substitute_rec(body, cur_node_contents, &new_env), beta.clone()))
        }
        ExtendEnvPhaseless(ref body, ref beta) => {
            let mut new_env = env.clone();
            for bound_name in crate::beta::bound_from_beta(beta, cur_node_contents, 0) {
                new_env = new_env.unset(bound_name);
            }

            node.with_c(ExtendEnvPhaseless(
                substitute_rec(body, cur_node_contents, &new_env),
                beta.clone(),
            ))
        }
        QuoteMore(ref body, pos) => {
            node.with_c(QuoteMore(substitute_rec(body, cur_node_contents, &env.q_more(1)), *pos))
        }
        QuoteLess(ref body, depth) => node.with_c(QuoteLess(
            substitute_rec(body, cur_node_contents, &env.q_less(*depth)),
            *depth,
        )),
        _ => node.clone(),
    }
}

/// Substitute `VariableReference`s in `node`, according to `env`.
/// TODO: don't use this to "capture the environment"; it doesn't work in the presence of recursion
/// Instead, we should introduce a "constant" to Beta. (Does `SameAs` suffice now?)
/// TODO: because of mu's use of `VariableReference`s in a place where other `Ast`s are forbidden,
///  it seems like this has limited use.
/// TODO: this isn't capture-avoiding (and shouldn't be, when called by `freshen_rec`)
/// It's safe to use when the RHS of the environment is just fresh names.
pub fn substitute(node: &Ast, env: &Assoc<Name, Ast>) -> Ast {
    substitute_rec(node, &EnvMBE::new(), &Ren::from(env.clone()))
}

/// Like `beta::names_mentioned`, but for all the imports in `parts`
fn mentioned_in_import(parts: &EnvMBE<Ast>) -> Vec<Name> {
    fn process_ast(a: &Ast, v: &mut Vec<Name>) {
        match a.c() {
            Node(_, _, _) => {} // new scope
            ExtendEnv(ref body, ref beta) | ExtendEnvPhaseless(ref body, ref beta) => {
                let mut beta_mentions = beta.names_mentioned_and_bound();
                v.append(&mut beta_mentions);
                process_ast(&*body, v);
            }
            // TODO: does it make sense to mention a name underneath a quotation?
            QuoteMore(ref body, _) | QuoteLess(ref body, _) => process_ast(body, v),
            Trivial | Atom(_) | VariableReference(_) => {} // no beta
            Shape(_) | IncompleteNode(_) => icp!("{:?} isn't a complete AST", a),
        }
    }

    let mut res = vec![];
    parts.map(&mut |a| process_ast(a, &mut res));
    res
}

fn freshen_rec(node: &Ast, renamings: &EnvMBE<(Ast, Ren)>, env: Ren) -> Ast {
    //  `env` is used to update the references to those atoms to match
    match node.c() {
        Node(_, _, _) => substitute_rec(node, &EnvMBE::new(), &env),
        VariableReference(n) => env.find(*n).unwrap_or(&node.clone()).clone(),
        ExtendEnv(ref body, ref beta) => {
            let new_env = env.set_assoc(&beta.extract_from_mbe(renamings, &|x: &(_, Ren)| &x.1));

            node.with_c(ExtendEnv(freshen_rec(body, renamings, new_env), beta.clone()))
        }
        ExtendEnvPhaseless(ref body, ref beta) => {
            // Everything bound this way becomes phaseless.
            let new__env = env.set_assoc(
                &beta.extract_from_mbe(renamings, &|x: &(_, Ren)| &x.1).become_phaseless(),
            );

            node.with_c(ExtendEnvPhaseless(freshen_rec(body, renamings, new__env), beta.clone()))
        }
        QuoteMore(ref body, pos) => {
            node.with_c(QuoteMore(freshen_rec(body, renamings, env.q_more(1)), *pos))
        }
        QuoteLess(ref body, depth) => {
            node.with_c(QuoteLess(freshen_rec(body, renamings, env.q_less(*depth)), *depth))
        }
        Atom(_) | Trivial | IncompleteNode(_) | Shape(_) => node.clone(),
    }
}

thread_local! {
    pub static freshening_enabled: std::cell::RefCell<bool> = std::cell::RefCell::new(true);
    pub static watching: Option<String> = std::env::var(&"UNSEEMLY_FRESHEN_WATCH").ok();
}

pub fn freshen(a: &Ast) -> Ast {
    // TODO: I think this shouldn't take a reference for performance
    if freshening_enabled.with(|f| *f.borrow()) {
        a.c_map(&|c| match c {
            &Node(ref f, ref p, ref export) => {
                // Every part that gets mentioned inside this node...
                let mentioned = mentioned_in_import(p);
                // ...needs to have its binders freshend:
                let fresh_ast_and_rens = freshen_binders_inside_node(p, &mentioned);

                let freshened_node = Node(
                    f.clone(),
                    fresh_ast_and_rens.marched_map(
                        &mut |_, marched: &EnvMBE<(Ast, Ren)>, &(ref part, _)| {
                            freshen_rec(part, marched, Ren::new())
                        },
                    ),
                    export.clone(),
                );

                // Diagnostic output for "watching freshening".
                watching.with(|watching_name| {
                    if let Some(name) = watching_name {
                        let freshened_to = fresh_ast_and_rens.map_reduce(
                            &|ast_and_ren: &(Ast, Ren)| ast_and_ren.1.find_orig(name),
                            &|lhs: &Option<(Name, Ast)>, rhs: &Option<(Name, Ast)>| {
                                lhs.clone().or(rhs.clone())
                            },
                            None,
                        );
                        if let Some((k, new_ast)) = freshened_to {
                            println!("🥦 Renaming {} => {}:", k, new_ast);
                            println!("🥦 {}", freshened_node)
                        }
                    }
                });

                freshened_node
            }
            non_node => non_node.clone(),
        })
    } else {
        a.clone()
    }
}
// TODO: verify that this handles internal `ExtendEnv`s right
pub fn freshen_with(lhs: &Ast, rhs: &Ast) -> (Ast, Ast) {
    if freshening_enabled.with(|f| *f.borrow()) {
        match (lhs.c(), rhs.c()) {
            (&Node(ref f, ref p_lhs, ref export), &Node(ref f_rhs, ref p_rhs, ref export_rhs)) => {
                if f != f_rhs || export != export_rhs {
                    return (lhs.clone(), rhs.clone());
                }
                // Every part that gets mentioned inside this node...
                let mentioned = mentioned_in_import(p_lhs);
                //  (if it matters which `p_{l,r}hs` we used, the match below will be `None`)
                // ...needs to have its binders freshend:
                match freshen_binders_inside_node_with(p_lhs, p_rhs, &mentioned) {
                    Some(fresh_ast_and_rens) => {
                        let new_p_lhs = fresh_ast_and_rens.marched_map(
                            &mut |_,
                                  marched: &EnvMBE<(Ast, Ren, Ast, Ren)>,
                                  &(ref parts, _, _, _)| {
                                freshen_rec(
                                    parts,
                                    &marched.map(&mut |q| (q.0.clone(), q.1.clone())),
                                    Ren::new(),
                                )
                            },
                        );
                        let new_p_rhs = fresh_ast_and_rens.marched_map(
                            &mut |_,
                                  marched: &EnvMBE<(Ast, Ren, Ast, Ren)>,
                                  &(_, _, ref parts, _)| {
                                freshen_rec(
                                    parts,
                                    &marched.map(&mut |q| (q.2.clone(), q.3.clone())),
                                    Ren::new(),
                                )
                            },
                        );
                        (
                            lhs.with_c(Node(f.clone(), new_p_lhs, export.clone())),
                            rhs.with_c(Node(f.clone(), new_p_rhs, export.clone())),
                        )
                    }
                    None => (lhs.clone(), rhs.clone()), // No destructuring will be performed!
                }
            }
            _ => (lhs.clone(), rhs.clone()), // No binding
        }
    } else {
        (lhs.clone(), rhs.clone()) // Freshening is disabled
    }
}

pub fn freshen_binders_inside_node(parts: &EnvMBE<Ast>, mentioned: &[Name]) -> EnvMBE<(Ast, Ren)> {
    parts.named_map(&mut |n: &Name, a: &Ast| {
        if mentioned.contains(n) {
            freshen_binders(a)
        } else {
            (a.clone(), Ren::new())
        }
    })
}

pub fn freshen_binders_inside_node_with(
    p_lhs: &EnvMBE<Ast>,
    p_rhs: &EnvMBE<Ast>,
    men: &[Name],
) -> Option<EnvMBE<(Ast, Ren, Ast, Ren)>> {
    if !p_lhs.can_map_with(p_rhs) {
        return None;
    }
    p_lhs
        .named_map_with(p_rhs, &|n: &Name, a_lhs: &Ast, a_rhs: &Ast| {
            if men.contains(n) {
                freshen_binders_with(a_lhs, a_rhs).ok_or(())
            } else {
                Ok((a_lhs.clone(), Ren::new(), a_rhs.clone(), Ren::new()))
            }
        })
        .lift_result()
        .ok()
}

/// Returns an `Ast` like `a`, but with fresh `Atom`s
///  and a map to change references in the same manner
pub fn freshen_binders(a: &Ast) -> (Ast, Ren) {
    match a.c() {
        Trivial | VariableReference(_) => (a.clone(), Ren::new()),
        Atom(old_name) => {
            let new_name = old_name.freshen();
            (
                a.with_c(Atom(new_name)),
                Ren::single(*old_name, raw_ast!(VariableReference(new_name))),
            )
        }
        Node(ref f, ref parts, ref export) => {
            if export == &crate::beta::ExportBeta::Nothing {
                return (a.clone(), Ren::new()); // short-circuit (should this at least warn?)
            }
            let exported = export.names_mentioned(); // Unmentioned atoms shouldn't be touched

            let fresh_pairs = freshen_binders_inside_node(parts, &exported);
            let fresh_ast = fresh_pairs.map(&mut |&(ref a, _): &(Ast, _)| a.clone());
            let renaming = export.extract_from_mbe(&fresh_pairs, &|&(_, ref r): &(_, Ren)| &r);

            (a.with_c(Node(f.clone(), fresh_ast, export.clone())), renaming)
        }
        IncompleteNode(_) | Shape(_) => icp!("didn't think this was needed"),
        QuoteMore(ref body, pos) => {
            let (new_a, r) = freshen_binders(body);
            (a.with_c(QuoteMore(new_a, *pos)), r.q_less(1))
        }
        QuoteLess(ref body, depth) => {
            let (new_a, r) = freshen_binders(body);
            (a.with_c(QuoteLess(new_a, *depth)), r.q_more(*depth))
        }
        ExtendEnv(ref sub, ref beta) => {
            // We're only looking at `Atom`s, so this is transparent
            let (new_sub, subst) = freshen_binders(&*sub);
            (a.with_c(ExtendEnv(new_sub, beta.clone())), subst)
        }
        ExtendEnvPhaseless(ref sub, ref beta) => {
            // We're only looking at `Atom`s, so this is transparent
            let (new_sub, subst) = freshen_binders(&*sub);
            (a.with_c(ExtendEnvPhaseless(new_sub, beta.clone())), subst.become_phaseless())
        }
    }
}

/// Like `freshen_binders`, but to unite two `Ast`s with identical structure (else returns `None`).
pub fn freshen_binders_with(lhs: &Ast, rhs: &Ast) -> Option<(Ast, Ren, Ast, Ren)> {
    match (lhs.c(), rhs.c()) {
        (&Trivial, &Trivial) | (&VariableReference(_), &VariableReference(_)) => {
            Some((lhs.clone(), Ren::new(), rhs.clone(), Ren::new()))
        }
        (&Atom(old_name_lhs), &Atom(old_name_rhs)) => {
            let new_name = old_name_lhs.freshen();
            Some((
                lhs.with_c(Atom(new_name)),
                Ren::single(old_name_lhs, raw_ast!(VariableReference(new_name))),
                rhs.with_c(Atom(new_name)),
                Ren::single(old_name_rhs, raw_ast!(VariableReference(new_name))),
            ))
        }
        // TODO: Handle matching `'[let (a,b) = ⋯]'` against the pattern `'[let ,[p], = ⋯]'` !!
        (
            &Node(ref f, ref parts_lhs, ref export),
            &Node(ref f_rhs, ref parts_rhs, ref export_rhs),
        ) => {
            if f != f_rhs || export != export_rhs {
                return None;
            }

            if export == &crate::beta::ExportBeta::Nothing {
                // short-circuit:
                return Some((lhs.clone(), Ren::new(), rhs.clone(), Ren::new()));
            }
            let exported = export.names_mentioned(); // Unmentioned atoms shouldn't be touched

            match freshen_binders_inside_node_with(parts_lhs, parts_rhs, &exported) {
                Some(fresh_pairs) => {
                    let fresh_ast_lhs = fresh_pairs.map(&mut |&(ref a, _, _, _)| a.clone());
                    let fresh_ast_rhs = fresh_pairs.map(&mut |&(_, _, ref a, _)| a.clone());
                    let ren_lhs = export.extract_from_mbe(&fresh_pairs, &|t: &(_, Ren, _, _)| &t.1);
                    let ren_rhs = export.extract_from_mbe(&fresh_pairs, &|t: &(_, _, _, Ren)| &t.3);
                    Some((
                        lhs.with_c(Node(f.clone(), fresh_ast_lhs, export.clone())),
                        ren_lhs,
                        rhs.with_c(Node(f.clone(), fresh_ast_rhs, export.clone())),
                        ren_rhs,
                    ))
                }
                None => None,
            }
        }
        (&QuoteMore(ref body_lhs, pos), &QuoteMore(ref body_rhs, pos_rhs)) if pos == pos_rhs => {
            match freshen_binders_with(&*body_lhs, &*body_rhs) {
                Some((n_lhs, ren_lhs, n_rhs, ren_rhs)) => Some((
                    lhs.with_c(QuoteMore(n_lhs, pos)),
                    ren_lhs.q_less(1),
                    rhs.with_c(QuoteMore(n_rhs, pos)),
                    ren_rhs.q_less(1),
                )),
                None => None,
            }
        }
        (&QuoteLess(ref body_lhs, depth), &QuoteLess(ref body_rhs, depth_rhs))
            if depth == depth_rhs =>
        {
            match freshen_binders_with(&*body_lhs, &*body_rhs) {
                Some((n_lhs, ren_lhs, n_rhs, ren_rhs)) => Some((
                    lhs.with_c(QuoteLess(n_lhs, depth)),
                    ren_lhs.q_more(depth),
                    rhs.with_c(QuoteLess(n_rhs, depth)),
                    ren_rhs.q_more(depth),
                )),
                None => None,
            }
        }
        (&IncompleteNode(_), _) | (&Shape(_), _) => icp!("didn't think this was needed"),
        (&ExtendEnv(ref sub_lhs, ref beta), &ExtendEnv(ref sub_rhs, ref beta_rhs))
        | (
            &ExtendEnvPhaseless(ref sub_lhs, ref beta),
            &ExtendEnvPhaseless(ref sub_rhs, ref beta_rhs),
        ) => {
            if beta != beta_rhs {
                return None;
            }
            let ee = |a: Ast| -> Ast {
                if let ExtendEnv(_, _) = lhs.c() {
                    a.with_c(ExtendEnv(a.clone(), beta.clone()))
                } else {
                    a.with_c(ExtendEnvPhaseless(a.clone(), beta.clone()))
                }
            };
            // We're only looking at `Atom`s, so this is transparent
            match freshen_binders_with(&*sub_lhs, &*sub_rhs) {
                Some((n_lhs, ren_lhs, n_rhs, ren_rhs)) => {
                    Some((ee(n_lhs), ren_lhs, ee(n_rhs), ren_rhs))
                }
                None => None,
            }
        }
        _ => None, // Match failure
    }
}

#[test]
fn basic_substitution() {
    crate::name::enable_fake_freshness(true);

    assert_eq!(
        substitute(
            &ast!({"Expr" "apply" : "rator" => (vr "a"), "rand" => [(vr "b"), (vr "c")]}),
            &assoc_n!("x" => ast!((vr "y")), "buchanan" => ast!((vr "lincoln")))
        ),
        ast!({"Expr" "apply" : "rator" => (vr "a"), "rand" => [(vr "b"), (vr "c")]})
    );

    assert_eq!(
        substitute(
            &ast!({"Expr" "apply" : "rator" => (vr "buchanan"),
                                    "rand" => [(vr "buchanan"), (vr "c")]}),
            &assoc_n!("x" => ast!((vr "y")), "buchanan" => ast!((vr "lincoln")))
        ),
        ast!({"Expr" "apply" : "rator" => (vr "lincoln"), "rand" => [(vr "lincoln"), (vr "c")]})
    );

    assert_eq!(
        substitute(
            &ast!({"Expr" "lambda" :
                "param" => ["b", "x"],
                "body" => (import [* ["param" : "[ignored]"]]
                    {"Expr" "apply" : "rator" => (vr "f"),
                                      "rand" => [(vr "a"), (vr "b"), (vr "c")]})}),
            &assoc_n!("a" => ast!((vr "A")), "b" => ast!((vr "B")), "c" => ast!((vr "C")))
        ),
        ast!({"Expr" "lambda" :
            "param" => ["b", "x"],
            "body" => (import [* ["param" : "[ignored]"]]
                {"Expr" "apply" : "rator" => (vr "f"),
                                  "rand" => [(vr "A"), (vr "b"), (vr "C")]})})
    );
}

#[test]
fn basic_binder_freshening() {
    crate::name::enable_fake_freshness(true);

    assert_eq!(freshen_binders(&ast!((vr "a"))), (ast!((vr "a")), Ren::new()));

    assert_eq!(
        freshen_binders(&ast!("a")),
        (ast!("a🍅"), Ren::from(assoc_n!("a" => ast!((vr "a🍅")))))
    );

    assert_eq!(
        freshen_binders(&ast!({ "Pat" "enum_pat" => [* ["component"]] :
            "name" => "[ignored]", "component" => ["a", "b"] })),
        (
            ast!({ "Pat" "enum_pat" => [* ["component"]] :
            "name" => "[ignored]", "component" => ["a🍅", "b🍅"] }),
            Ren::from(assoc_n!("a" => ast!((vr "a🍅")), "b" => ast!((vr "b🍅"))))
        )
    );
}

#[test]
fn basic_freshening() {
    crate::name::enable_fake_freshness(true);

    assert_eq!(
        freshen(&ast!({"Expr" "lambda" :
                "param" => ["a", "b"],
                "body" => (import [* ["param" : "[ignored]"]]
                    {"Expr" "apply" : "rator" => (vr "f"),
                                      "rand" => [(vr "a"), (vr "b"), (vr "c"), (vr "d")]})})),
        ast!({"Expr" "lambda" :
            "param" => ["a🍅", "b🍅"],
            "body" => (import [* ["param" : "[ignored]"]]
                {"Expr" "apply" : "rator" => (vr "f"),
                                  "rand" => [(vr "a🍅"), (vr "b🍅"), (vr "c"), (vr "d")]})})
    );

    assert_eq!(
        freshen(&ast!({"Expr" "match" :
            "scrutinee" => (vr "x"),
            "p" => [@"arm" "a", "b"],
            "arm" => [@"arm" (import ["p" = "scrutinee"] (vr "a")),
                             (import ["p" = "scrutinee"] (vr "x"))]
        })),
        ast!({"Expr" "match" :
            "scrutinee" => (vr "x"),
            "p" => [@"arm" "a🍅", "b🍅"],
            "arm" => [@"arm" (import ["p" = "scrutinee"] (vr "a🍅")),
                             (import ["p" = "scrutinee"] (vr "x"))]})
    );

    // Test that importing non-atoms works
    assert_eq!(
        freshen(&ast!({"Expr" "match" :
            "scrutinee" => (vr "x"),
            "p" => [@"arm" { "Pat" "enum_pat" => [* ["component"]] :
                "name" => "[ignored]", "component" => ["a"]
            }],
            "arm" => [@"arm" (import ["p" = "scrutinee"] (vr "a"))]
        })),
        ast!({"Expr" "match" :
            "scrutinee" => (vr "x"),
            "p" => [@"arm" { "Pat" "enum_pat" => [* ["component"]] :
                "name" => "[ignored]", "component" => ["a🍅"]
            }],
            "arm" => [@"arm" (import ["p" = "scrutinee"] (vr "a🍅"))]})
    );

    // TODO: test more!
}

#[test]
fn basic_phaseless_freshening() {
    crate::name::enable_fake_freshness(true);
    assert_eq!(
        freshen(&ast!({"Expr" "lambda" :
        "param" => ["a"],
        "pparam" => ["b"],
        "body" => (import_phaseless [* ["pparam" : "[ignored]"]]
            (import [* ["param" : "[ignored]"]]
                {"Expr" "apply" :
                     "rator" => (vr "f"),
                     "rand" => [(vr "a"), (vr "b"), (++ true (vr "a")), (++ true (vr "b"))]}))})),
        ast!({"Expr" "lambda" :
        "param" => ["a🍅"],
        "pparam" => ["b🍅"],
        "body" => (import_phaseless [* ["pparam" : "[ignored]"]]
            (import [* ["param" : "[ignored]"]]
            {"Expr" "apply" : "rator" => (vr "f"),
            "rand" => [(vr "a🍅"), (vr "b🍅"), (++ true (vr "a")), (++ true (vr "b🍅"))]}))})
    )
}

#[test]
fn basic_freshening_with() {
    crate::name::enable_fake_freshness(true);

    assert_eq!(
        freshen_with(&ast!({"Type" "Int" :}), &ast!({"Type" "Float" :})),
        (ast!({"Type" "Int" :}), ast!({"Type" "Float" :}))
    );

    assert_eq!(
        freshen_with(
            &ast!({"Expr" "lambda" :
                "param" => ["a", "b"],
                "body" => (import [* ["param" : "[ignored]"]]
                    {"Expr" "apply" : "rator" => (vr "f"),
                                      "rand" => [(vr "a"), (vr "b"), (vr "c"), (vr "d")]})}),
            &ast!({"Expr" "lambda" :
                "param" => ["j", "k"],
                "body" => (import [* ["param" : "[ignored]"]]
                    {"Expr" "apply" : "rator" => (vr "f"),
                                      "rand" => [(vr "j"), (vr "k"), (vr "x"), (vr "x")]})})
        ),
        (
            ast!({"Expr" "lambda" :
             "param" => ["a🍅", "b🍅"],
             "body" => (import [* ["param" : "[ignored]"]]
                 {"Expr" "apply" : "rator" => (vr "f"),
                                   "rand" => [(vr "a🍅"), (vr "b🍅"), (vr "c"), (vr "d")]})}),
            ast!({"Expr" "lambda" :
             "param" => ["a🍅", "b🍅"],
             "body" => (import [* ["param" : "[ignored]"]]
                 {"Expr" "apply" : "rator" => (vr "f"),
                                   "rand" => [(vr "a🍅"), (vr "b🍅"), (vr "x"), (vr "x")]})})
        )
    );

    assert_eq!(
        freshen_with(
            &ast!({"Expr" "match" :
                "scrutinee" => (vr "x"),
                "p" => [@"arm" { "Pat" "enum_pat" => [* ["component"]] :
                    "name" => "[ignored]", "component" => ["a"]
                }],
                "arm" => [@"arm" (import ["p" = "scrutinee"] (vr "a"))]
            }),
            &ast!({"Expr" "match" :
                "scrutinee" => (vr "x"),
                "p" => [@"arm" { "Pat" "enum_pat" => [* ["component"]] :
                    "name" => "[ignored]", "component" => ["x"]
                }],
                "arm" => [@"arm" (import ["p" = "scrutinee"] (vr "x"))]
            })
        ),
        (
            ast!({"Expr" "match" :
             "scrutinee" => (vr "x"),
             "p" => [@"arm" { "Pat" "enum_pat" => [* ["component"]] :
                 "name" => "[ignored]", "component" => ["a🍅"]
             }],
             "arm" => [@"arm" (import ["p" = "scrutinee"] (vr "a🍅"))]}),
            ast!({"Expr" "match" :
              "scrutinee" => (vr "x"),
              "p" => [@"arm" { "Pat" "enum_pat" => [* ["component"]] :
                  "name" => "[ignored]", "component" => ["a🍅"]
              }],
              "arm" => [@"arm" (import ["p" = "scrutinee"] (vr "a🍅"))]})
        )
    );

    // Terms that don't match are unaffected
    assert_eq!(
        freshen_with(
            &ast!({"Expr" "lambda" :
                  "param" => ["a", "b"],
                  "body" => (import [* ["param" : "[ignored]"]]
                      {"Expr" "apply" : "rator" => (vr "f"),
                                        "rand" => [(vr "a"), (vr "b"), (vr "c"), (vr "d")]})}),
            &ast!({"Expr" "lambda" :
                  "param" => ["abc"],
                  "body" => (import [* ["param" : "[ignored]"]]
                      {"Expr" "apply" : "rator" => (vr "f"),
                                        "rand" => [(vr "a"), (vr "b"), (vr "x"), (vr "x")]})})
        ),
        (
            ast!({"Expr" "lambda" :
              "param" => ["a", "b"],
              "body" => (import [* ["param" : "[ignored]"]]
                  {"Expr" "apply" : "rator" => (vr "f"),
                                    "rand" => [(vr "a"), (vr "b"), (vr "c"), (vr "d")]})}),
            ast!({"Expr" "lambda" :
              "param" => ["abc"],
              "body" => (import [* ["param" : "[ignored]"]]
                  {"Expr" "apply" : "rator" => (vr "f"),
                                    "rand" => [(vr "a"), (vr "b"), (vr "x"), (vr "x")]})})
        )
    );
}

#[test]
fn mu_substitution() {
    let trivial_mu = ast!( { "Type" "mu_type" : "param" => [(import [prot "param"] (vr "T"))],
                              "body" => (import [* [prot "param"]] (vr "T")) });
    assert_eq!(freshen(&trivial_mu), trivial_mu);

    assert_eq!(
        substitute(&trivial_mu, &assoc_n!("T" => ast!((vr "S")))),
        ast!( { "Type" "mu_type" : "param" => [(import [prot "param"] (vr "S"))],
                                   "body" => (import [* [prot "param"]] (vr "S")) })
    )
}

#[test]
fn alpha_quote_more_or_less() {
    crate::name::enable_fake_freshness(true);

    assert_eq!(
        freshen(&ast!({"Expr" "lambda" :
                "param" => ["a", "b"],
                "body" => (import [* ["param" : "[ignored]"]]
                    (++ true {"Expr" "apply" : "rator" => (vr "f"),
                                               "rand" => [(vr "a"), (vr "b")]}))})),
        ast!({"Expr" "lambda" :
            "param" => ["a🍅", "b🍅"],
            "body" => (import [* ["param" : "[ignored]"]]
                (++ true {"Expr" "apply" : "rator" => (vr "f"),
                                           "rand" => [(vr "a"), (vr "b")]}))})
    );

    assert_eq!(
        freshen(&ast!({"Expr" "lambda" :
                "param" => ["a", "b"],
                "body" => (import [* ["param" : "[ignored]"]]
                    (++ true (-- 1 {"Expr" "apply" : "rator" => (vr "f"),
                                                     "rand" => [(vr "a"), (vr "b")]})))})),
        ast!({"Expr" "lambda" :
            "param" => ["a🍅", "b🍅"],
            "body" => (import [* ["param" : "[ignored]"]]
                (++ true (-- 1 {"Expr" "apply" : "rator" => (vr "f"),
                                                 "rand" => [(vr "a🍅"), (vr "b🍅")]})))})
    );
}
