def substitute_apply(t, subs, by_name=False):
    """
    Return the term obtained from t by simultaneous substitution given
    by subs

    subs is either a dictionary or a mapping given by an iterable of
    (key, value) pairs

    Both keys and values in subs can be either Var or Const, but must
    be 2nd order. For any key, value in subs, Apply(key, *terms) is
    substituted by value(*terms'), so the values in subs should be
    python functions (terms' is the result of recursively substituting
    terms according to subs).

    For variables, only free occurances will be substituted.

    To avoid capturing, the free variables of value(*terms) should be
    a subset of the free variables of terms, for any value in
    subs. This is checked, and an error occurs if this is not the
    case, even if it does not lead to capturing. If by_name=True, then
    this check is done by name and not by the Var object.

    Note that non-application occurances of keys from subs in t are
    not substituted (these should generally not occur).
    """

    if not isinstance(subs, dict):
        subs = dict(subs)

    _substitute_apply = partial(substitute_apply, subs=subs, by_name=by_name)

    if type(t) in (Var, Const):
        return t

    if type(t) is Apply and t.func in subs:
        terms = tuple(_substitute_apply(x) for x in t.terms)
        result = subs[t.func](*terms)
        fvr = free_variables(result, by_name=by_name)
        fvt = free_variables(*terms, by_name=by_name)
        assert fvr <= fvt, "New free variables!? {}, {}".format(fvr, fvt)
        return result

    elif type(t) in (Apply, Eq, Ite, Not, And, Or, Implies, Iff):
        return type(t)(*(_substitute_apply(x) for x in t))

    elif type(t) in (ForAll, Exists):
        return type(t)(t.variables, _substitute_apply(t.body, subs=dict(
            (k, v) for k, v in subs.iteritems()
            if k not in t.variables
        )))
    else:
        assert False, type(e)
dataset/ETHPy150Open Microsoft/ivy/ivy/logic_util.py/substitute_apply/original