fmod LAMBDA is pr NAT . pr QID .

    *** User-level lambda expressions, using named binders.
    sorts Expr EName .
    subsort Nat EName < Expr .
    subsort Qid < EName .
    op __     : Expr  Expr -> Expr [ctor] .
    op [\_._] : EName Expr -> Expr [ctor] .
    op let_:=_in_ : EName Expr Expr -> Expr .
    eq let X := A in B = [\ X . B ] A .

    vars X Y  : EName .
    vars Q Q' : Qid  .
    var  N    : Nat  .
    vars A B  : Expr .
    vars C C' D D' : DeBruijn .
    var  Sc   : Scope .

    *** To keep a list of the variable names in scope, innermost at the head.
    sort Scope .
    op empty : -> Scope [ctor] .
    op __  : Scope EName -> Scope [ctor] .
    op idx : EName Scope ~> Nat .
    eq idx(X, Sc) = idx#(0, X, Sc) .
    op     idx# : Nat EName Scope ~> Nat .
    eq     idx#(N, X, Sc X) = N .
    ceq    idx#(N, X, Sc Y) = idx#(s N, X, Sc) if X =/= Y .

    *** A nameless lambda representation which uses the distance from the
    *** variable to the binding lambda.
    sorts DeBruijn DName .
    subsort Nat DName < DeBruijn .
    op f : Qid -> DName [ctor] .  *** Free variables
    op b : Nat -> DName [ctor] .  *** Bound variables
    op d[__] : DeBruijn DeBruijn -> DeBruijn [ctor] .
    op d[\._]  : DeBruijn -> DeBruijn [ctor] .

    *** Convert named variable expressions to nameless.
    op debruijn : Expr -> DeBruijn .
    eq debruijn(A) = debruijn#(empty, A) .
    op     debruijn# : Scope Expr -> DeBruijn                              .
    eq     debruijn#(Sc, N)         = N                                    .
    ceq    debruijn#(Sc, X)         = b(N)              if N := idx(X, Sc) .
    eq     debruijn#(Sc, X)         = f(X)                         [owise] .
    eq     debruijn#(Sc, A B)       = d[debruijn#(Sc, A) debruijn#(Sc, B)] .
    eq     debruijn#(Sc, [\ X . A]) = d[\. debruijn#(Sc X, A)]             .

    *** Bindings defined outside of the reducing expression (named identifiers).
    sort FreeCtx .
    op none : -> FreeCtx [ctor] .
    op _as_ : Qid DeBruijn    -> FreeCtx [ctor] .
    op _;_  : FreeCtx FreeCtx -> FreeCtx [ctor comm assoc id: none] .

    *** Bindings introduced from lambdas in the expression.
    sort BoundCtx .  subsort DeBruijn < BoundCtx .
    op none   : -> BoundCtx [ctor] .
    op _;_     : BoundCtx BoundCtx -> BoundCtx [ctor assoc id: none] .

    *** Do beta substitution to reduce a nameless expression to its normal form.
    var Free : FreeCtx .  var Bound : BoundCtx .
    op _|=_ : FreeCtx Expr ~> DeBruijn .
    eq Free |= A = eval#(Free, none, debruijn(A)) .
    op     eval# : FreeCtx BoundCtx DeBruijn ~> DeBruijn .
    eq     eval#(Free,          Bound,          N) = N                              .
    eq     eval#(Free,          Bound,    d[\. C]) = d[\. C]                        .
    eq     eval#(Free,          Bound ; C, b(  0)) = eval#(Free, Bound ; C,      C) .
    eq     eval#(Free,          Bound ; C, b(s N)) = eval#(Free, Bound,       b(N)) .
    eq     eval#(Free ; Q as C, Bound,     f(  Q)) = eval#(Free ; Q as C, Bound, C) .
    eq     eval#(Free,          Bound,     f(  Q)) = Q                      [owise] .
    ceq    eval#(Free,          Bound,     d[C D]) = eval#(Free, Bound ; D', C')
           if d[\. C'] := eval#(Free, Bound, C) /\ D' := eval#(Free, Bound, D)      .

endfm