Capture-avoiding substitution

=begin pod

Perl 6 program that implements the capture-avoiding substitution algorithm
described at
L<http://www.mcrl2.org/web/developer_manual/_downloads/substitutions.pdf>.

=end pod

role Expr {
}

class Var does Expr {
    has Str $.var;
}

class Abs does Expr {
    has Str $.param;
    has Expr $.body;
}

class App does Expr {
    has Expr $.fun;
    has Expr $.arg;
}

sub var($var) { Var.new(:$var) }
sub abs($param, $body) { Abs.new(:$param, :$body) }
sub app($fun, $arg) { App.new(:$fun, :$arg) }

proto expr-free(Expr:D $expr --> Set:D) {*}

multi expr-free(Var:D $expr --> Set:D) {
    set($expr.var);
}

multi expr-free(Abs:D $expr --> Set:D) {
    expr-free($expr.body) ∖ set($expr.param);
}

multi expr-free(App:D $expr --> Set:D) {
    expr-free($expr.fun) ∪ expr-free($expr.arg);
}

sub subst-free(%subst --> Set:D) {
    [∪] %subst.kv.map: { expr-free($^b) ∖ set($^a) };
}

sub fresh(--> Str:D) {
    '$' ~ (state $ = 'a')++;
}

sub subst(Str:D $var --> Expr:D) {
    %*subst{$var} // var($var);
}

proto subst-ca(Expr:D $expr --> Expr:D) {*}

multi subst-ca(Var:D $expr --> Expr:D) {
    subst($expr.var);
}

multi subst-ca(Abs:D $expr --> Expr:D) {
    my $captures = subst($expr.param) !eqv var($expr.param) || $expr.param ∈ $*free;
    my $new-param = $captures ?? fresh() !! $expr.param;
    (temp %*subst){$expr.param} = var($new-param);
    temp $*free ∪= set($new-param);
    abs($new-param, subst-ca($expr.body));
}

multi subst-ca(App:D $expr --> Expr:D) {
    App.new(
        fun => subst-ca($expr.fun),
        arg => subst-ca($expr.arg),
    );
}

my $lambda = abs('a', abs('b', var('a')));

say app($lambda, var('b'));

{
    my %*subst = a => var('b');
    my $*free = expr-free($lambda.body) ∪ subst-free(%*subst);
    say subst-ca($lambda.body);
}

{
    my %*subst;
    my $*free = expr-free($lambda.body) ∪ subst-free(%*subst);
    say subst-ca($lambda.body);
}