/*
 * (c) 2022 Petr Ročkai <code@fixp.eu>
 *
 * Permission to use, copy, modify, and distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
 * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
 * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 */

#pragma once
#include "types.hpp"
#include "eval.hpp"
#include "stack.hpp"
#include <deque>

namespace bast
{
    struct type_tag {};

    struct type_state : basic_stack
    {
    };

    struct tc_visited
    {
        std::map< word, type_state > visited;

        bool store( const type_state s, bast::label w )
        {
            if ( auto it = visited.find( w.v ); it != visited.end() )
            {
                if ( it->second != s )
                    brq::raise() << "confluence check failed " << it->second << " vs " << s;
                return false;
            }
            else
            {
                visited.emplace( w.v, s );
                return true;
            }
        }
    };

    struct tc_queue : queue_common
    {
        using state_t = std::pair< type_state, bast::label >;
        std::deque< state_t > todo;

        void push( const type_state &o, bast::label w ) { todo.emplace_front( o, w ); }
        state_t pop() { return pop_back( todo ); }
        bool empty() const { return todo.empty(); }
    };

    struct tc_ops
    {
        static void check( type_state &s, std::initializer_list< type > expect )
        {
            type_state matched;

            for ( type e : expect )
            {
                if ( s.empty() )
                    brq::raise() << "not enough arguments";

                type f = s.pop< type >();

                if ( e != f )
                {
                    brq::string_builder mstr;

                    while ( !matched.empty() )
                        mstr << " " << matched.pop< type >();

                    brq::raise() << "type check failed\n"
                                 << "expected " << e << ", found "
                                 << s << " " << f << " ⟨" << mstr.data() << " |";
                }

                matched.push( f );
            }
        }

        static step perform( type_state &s, std::initializer_list< type > expect,
                                            std::initializer_list< type > push )
        {
            check( s, expect );

            for ( type t : push )
                s.push( t );

            return next;
        }

        static constexpr type t_type = type{ uint16_t( builtin_type::type ) };
        static constexpr type t_dyad = type{ uint16_t( builtin_type::dyad ) };
        static constexpr type t_word = type{ uint16_t( builtin_type::word ) };
        static constexpr type t_half = type{ uint16_t( builtin_type::half ) };
        static constexpr type t_byte = type{ uint16_t( builtin_type::byte ) };
        static constexpr type t_dict = type{ uint16_t( builtin_type::dict ) };
    };

    template< builtin_type type_id >
    struct op< std::enable_if_t< bitvec_type< type_id >::value, type_tag >, type_id > : tc_ops
    {
        static step push_half( type_state &s, half ) { return perform( s, {}, { t_half } ); }
        static step push_word( type_state &s, word ) { return perform( s, {}, { t_word } ); }

        static step apply( type_state &s, word opcode )
        {
            using namespace bast::opcodes;
            const type t = type{ uint32_t( type_id ) };

            switch ( opcode )
            {
                case bv_add<>:
                case bv_sub<>:
                case bv_mul<>:
                case bv_udiv<>:
                case bv_urem<>:
                case bv_sdiv<>:
                case bv_srem<>:
                case bv_and<>:
                case bv_or<>:
                case bv_xor<>:

                case bv_neq<>:
                case bv_eq<>:

                case bv_ule<>:
                case bv_ult<>:
                case bv_ugt<>:
                case bv_uge<>:

                case bv_sle<>:
                case bv_slt<>:
                case bv_sgt<>:
                case bv_sge<>:
                    return perform( s, { t, t }, { t } );

                case bv_neg<>:
                    return perform( s, { t }, { t } );

                case gen_dup<>:
                    return perform( s, { t }, { t, t } );
                case gen_drop<>:
                    return perform( s, { t }, {} );

                case bv_const<>:
                    return perform( s, { t_word }, { t } );
                case bv_zero<>:
                    return perform( s, {}, { t } );

                case bv_trunc_h<>:
                    return perform( s, { t_half }, { t } );
                case bv_trunc_w<>:
                    return perform( s, { t_word }, { t } );
                case bv_trunc_d<>:
                    return perform( s, { t_dyad }, { t } );

                case bv_zext_b<>:
                case bv_sext_b<>:
                    return perform( s, { t_byte }, { t } );
                case bv_zext_h<>:
                case bv_sext_h<>:
                    return perform( s, { t_half }, { t } );
                case bv_zext_w<>:
                case bv_sext_w<>:
                    return perform( s, { t_word }, { t } );

                case bv_guard_zero<>:
                case bv_guard_nonzero<>:

                case bv_assert_zero<>:
                case bv_assert_nonzero<>:
                    return perform( s, { t }, {} );

                default:
                    UNREACHABLE( "missing case", std::hex, opcode );
            }
        }
    };

    template<> struct op< type_tag, builtin_type::type > : tc_ops
    {
        static step apply( type_state &s, word opcode )
        {
            using namespace bast::opcodes;

            switch ( make_opcode( type_id< type >, opcode ) )
            {
                case type_type: return perform( s, {}, { t_type, t_type } );
                case type_byte: return perform( s, {}, { t_byte, t_type } );
                case type_half: return perform( s, {}, { t_half, t_type } );
                case type_word: return perform( s, {}, { t_word, t_type } );
                case type_dyad: return perform( s, {}, { t_dyad, t_type } );
                default:
                    UNREACHABLE( "missing case", std::hex, opcode );
            }
        }
    };

    using tc_eval = eval< type_tag, type_state, brq::unit_t >;
    using typecheck = visit< tc_eval, tc_queue, tc_visited >;
}