def substitute(f, substitution):
    if substitution is None:
        return None
    if is_variable(f) and (get_name(f) in substitution):
        return substitute(substitution[get_name(f)], substitution)
    if has_args(f):
        return replace_args(f, [substitute(arg, substitution) for arg in get_args(f)])
    return f

# checks if v occurs in t
def occur_check(v, t, subst):
    if v == t:
        return True
    if is_variable(t) and get_name(t) in subst:
        return occur_check(v, substitute(t, subst), subst)
    if is_function_call(t):
        for arg in get_args(t):
            val = occur_check(v, arg, subst)
            if val:
                return True
    return False

# unifies f1 and f2 under a known substitution
def unify(f1, f2, subst = None):
    if subst is None:
        subst = {}
    S = []
    S.append((f1, f2))
    while len(S) > 0:
        (s, t) = S.pop()
        while is_variable(s) and get_name(s) in subst:
            s = substitute(s, subst)
        while is_variable(t) and get_name(t) in subst:
            t = substitute(t, subst)
        if s != t:
            if is_variable(s):
                if occur_check(s, t, subst):
                    return False
                else:
                    subst[get_name(s)] = t
            elif is_variable(t):
                if occur_check(t, s, subst):
                    return False
                else:
                    subst[get_name(t)] = s
            elif has_args(s) and has_args(t):
                s_args = get_args(s)
                t_args = get_args(t)
                if get_head(s) == get_head(t) and len(s_args) == len(t_args):
                    for i in range(len(s_args)):
                        S.append((s_args[i], t_args[i]))
                else:
                    return False
            else:
                return False
    return subst

# prints formulas in a human-readable format
def print_formula(f, return_result = False):
    ret = ""
    if is_term(f):
        if is_constant(f):
            ret += str(get_value(f))
        elif is_variable(f):
            ret += "?" + get_name(f)
        elif is_function_call(f):
            ret += str(get_head(f)) + "[" + "".join([print_formula(arg, True) + "," for arg in get_args(f)])[:-1] + "]"
        else:
            ret += "???"
    elif is_atom(f):
        ret += str(get_head(f)) + "(" + "".join([print_formula(arg, True) + ", " for arg in get_args(f)])[:-2] + ")"
    elif is_sentence(f):
        args = get_args(f)
        if len(args) == 1:
            ret += str(get_head(f)) + print_formula(args[0], True)
        else:
            ret += "(" + str(get_head(f)) + "".join([" " + print_formula(arg, True) for arg in get_args(f)]) + ")"
    else:
        ret += "???"
    if return_result:
        return ret
    print(ret)
    return