def infer_sorts(t, env=None):
    """
    Infer the sort of term t in environment env.

    env maps symbol names to sort variables.

    The result is a pair: (s, tt) where s is a sort or sort variable
    with the sort of t in env, and tt is a closure that, when called,
    will concretize t according to inferred sort information at its
    call time.

    If env is not None, it must contain all the free variables and
    constants used in t.
    """

    if env is None:
        names = free_variables(t, by_name=True).union(
            x.name for x in used_constants(t)
        )
        env = dict((name, SortVar()) for name in names)

    if type(t) in (Var, Const):
        if is_polymorphic(t):  # each instance can have different sort
            s = insert_sortvars(t.sort,{})
        else:
            s = env[t.name]
            unify(s, t.sort)
        return s, lambda: type(t)(t.name, convert_from_sortvars(s))

    elif type(t) is Apply:
        func_s, func_t = infer_sorts(t.func, env)
        xys = [infer_sorts(tt, env) for tt in t.terms]
        terms_s = [x for x, y in xys]
        terms_t = [y for x, y in xys]
        sorts = terms_s + [SortVar()]
        unify(func_s, FunctionSort(*sorts))
        return sorts[-1], lambda: Apply(func_t(), *(
            x() for x in terms_t
        ))

    elif type(t) is Eq:
        s1, t1 = infer_sorts(t.t1, env)
        s2, t2 = infer_sorts(t.t2, env)
        unify(s1, s2)
        return Boolean, lambda: Eq(t1(), t2())

    elif type(t) is Ite:
        s_cond, t_cond = infer_sorts(t.cond, env)
        s_then, t_then = infer_sorts(t.t_then, env)
        s_else, t_else = infer_sorts(t.t_else, env)
        unify(s_cond, Boolean)
        unify(s_then, s_else)
        return s_then, lambda: Ite(t_cond(), t_then(), t_else())

    elif type(t) in (Not, And, Or, Implies, Iff):
        xys = [infer_sorts(tt, env) for tt in t]
        terms_s = [x for x, y in xys]
        terms_t = [y for x, y in xys]
        for s in terms_s:
            unify(s, Boolean)
        return Boolean, lambda: type(t)(*[
            x() for x in terms_t
        ])

    elif type(t) in (ForAll, Exists):
        # create a copy of the environment and shadow that quantified
        # variables
        env = env.copy()
        env.update((v.name, SortVar()) for v in t.variables)
        vars_t = [infer_sorts(v, env)[1] for v in t.variables]
        body_s, body_t = infer_sorts(t.body, env)
        unify(body_s, Boolean)
        return Boolean, lambda: type(t)(
            [x() for x in vars_t],
            body_t(),
        )

    elif hasattr(t,'clone'):
        xys = [infer_sorts(tt, env) for tt in t.args]
        terms_t = [y for x, y in xys]
        return TopSort(), lambda: t.clone([
            x() for x in terms_t
        ])
        
    else:
        assert False, type(t)
dataset/ETHPy150Open Microsoft/ivy/ivy/type_inference.py/infer_sorts/original