syntax-try0.sml

term/fold var abs app term =
  cond
    var? term ->
      var (var/get-id term)

    abs? term ->
      abs (abs/get-id term) (abs/get-body term)

    app? term ->
      app (app/get-abs term) (app/get-arg term)


beta name subts term =
  let
    var id =
      if (id/eq? id name)
         subts
         term

    abs id body =
      if (id/eq? id name)
         term
         (abs/make id (beta name subts body))

    app abs arg =
      app/make (beta name subst abs) (beta name subst arg)

  in
    term/fold var abs app term


alpha name new-name term =
  let
    var id name =
      if (id/eq? id name)
         (var/make new-name)
         term

    abs id body =
      if (id/eq? id name)
         term
         (abs/make id (alpha name new-name body)

    app abs arg =
      app/make (alpha name new-name abs) (alpha name new-name arg)

  in
    term/fold var abs app term


alpha-beta name subst term =
  let
    var id =
      if (id/eq? id name)
         subts
         term

    abs id body =
      cond
        id/eq? id name ->
          term

        free? id subst && free? name body ->
          let
            free = free-vars subst `union` free-vars body
            new-id = make-new-id id free

          in
            abs/make new-id (alpha-beta name subst (alpha id new-id body))

        otherwise ->
          abs/make id (alpha-beta name subts body)

    app abs arg =
      app/make (alpha-beta name subst abs) (alpha-beta name subst arg)

  in
    term/fold var abs app term