#include <sys/queue.h>

#include <stdlib.h>

#include "spho/ctx.h"
#include "spho/scope.h"
#include "spho/tp.h"


const struct tp_konst_data tp_konst_true = { TP_KONST_KEY_TRUE, "True" };
const struct tp_konst_data tp_konst_false = { TP_KONST_KEY_FALSE, "False" };

//struct spho_tp	*
//spho_tp_create_disj(struct spho_ctx *, struct spho_tp *, struct spho_tp *,
//    struct spho_tp *)
//{
//
//}

static struct spho_tp *
spho_tp_alloc(struct spho_scope *sc)
{
	struct spho_tp_alloc *tp_alloc;

	if ((tp_alloc = calloc(1, sizeof(*tp_alloc))) == NULL) {
		SPHO_SC_ERR(sc, SPHO_ERR_SYS);
		return (NULL);
	}

	((struct spho_tp *)tp_alloc)->sc = sc;
	TAILQ_INSERT_TAIL(&sc->tps, tp_alloc, allocs);

	return ((struct spho_tp *)tp_alloc);
}

static void
spho_tp_free(struct spho_tp *tp)
{
	struct spho_scope *sc;
	struct spho_tp_alloc *tp_alloc;

	sc = tp->sc;
	tp_alloc = (struct spho_tp_alloc *)tp;

	TAILQ_REMOVE(&sc->tps, tp_alloc, allocs);

	free(tp_alloc);
}

struct spho_tp *
spho_tp_create_conj(struct spho_scope *sc, struct spho_tp *ltp,
    struct spho_tp *rtp)
{
	struct spho_tp *tp;

	if ((tp = spho_tp_alloc(sc)) == NULL)
		return (NULL);

	tp->form = SPHO_TP_FORM_CONJ;
	tp->d.binop.left = ltp;
	tp->d.binop.right = rtp;

	return (tp);
}

struct spho_tp *
spho_tp_create_disj(struct spho_scope *sc, struct spho_tp *ltp,
    struct spho_tp *rtp)
{
	struct spho_tp *tp;

	if ((tp = spho_tp_alloc(sc)) == NULL)
		return (NULL);

	tp->form = SPHO_TP_FORM_DISJ;
	tp->d.binop.left = ltp;
	tp->d.binop.right = rtp;

	return (tp);
}

struct spho_tp *
spho_tp_create_impl(struct spho_scope *sc, struct spho_tp *ltp,
    struct spho_tp *rtp)
{
	struct spho_tp *tp;

	if ((tp = spho_tp_alloc(sc)) == NULL)
		return (NULL);

	tp->form = SPHO_TP_FORM_IMPL;
	tp->d.binop.left = ltp;
	tp->d.binop.right = rtp;

	return (tp);
}

struct spho_tp *
spho_tp_create_arrow(struct spho_scope *sc, struct spho_tp *ltp,
    struct spho_tp *rtp)
{
	struct spho_tp *tp;

	if ((tp = spho_tp_alloc(sc)) == NULL)
		return (NULL);

	tp->form = SPHO_TP_FORM_ARROW;
	tp->d.binop.left = ltp;
	tp->d.binop.right = rtp;

	return (tp);
}

struct spho_tp *
spho_tp_create_box(struct spho_scope *sc, struct spho_tp *inner)
{
	struct spho_tp *tp;

	if ((tp = spho_tp_alloc(sc)) == NULL)
		return (NULL);

	tp->form = SPHO_TP_FORM_BOX;
	tp->d.unop.operand = inner;

	return (tp);
}

struct spho_tp *
spho_tp_create_forall(struct spho_scope *sc, struct spho_nom *nom,
    struct spho_tp *tp)
{
	struct spho_tp *ret;

	if ((ret = spho_tp_alloc(sc)) == NULL)
		return (NULL);

	ret->form = SPHO_TP_FORM_FORALL;
	ret->d.bind.nom = nom;
	ret->d.bind.bound = tp;

	return (ret);
}

struct spho_tp *
spho_tp_create_true(struct spho_scope *sc)
{
	struct spho_tp *ret;

	if ((ret = spho_tp_alloc(sc)) == NULL)
		return (NULL);

	ret->form = SPHO_TP_FORM_TRUE;
	ret->d.konst = tp_konst_true;

	return (ret);
}

struct spho_tp *
spho_tp_create_false(struct spho_scope *sc)
{
	struct spho_tp *ret;

	if ((ret = spho_tp_alloc(sc)) == NULL)
		return (NULL);

	ret->form = SPHO_TP_FORM_FALSE;
	ret->d.konst = tp_konst_false;

	return (ret);
}

struct spho_tp *
spho_tp_create_name(struct spho_scope *sc, struct spho_nom *nom)
{
	struct spho_tp *ret;

	if ((ret = spho_tp_alloc(sc)) == NULL)
		return (NULL);

	ret->form = SPHO_TP_FORM_NOM;
	ret->d.nom.nom = nom;

	return (ret);
}

struct spho_tp *
spho_tp_create_appl(struct spho_scope *sc, struct spho_nom *nom,
    struct spho_tp_l *args)
{
	struct spho_tp *ret;

	if ((ret = spho_tp_alloc(sc)) == NULL)
		return (NULL);

	ret->form = SPHO_TP_FORM_APPL;
	ret->d.appl.nom = nom;
	ret->d.appl.args = args;

	return (ret);
}

struct spho_tp *
spho_tp_create_member(struct spho_scope *sc, struct spho_nom *nom,
    struct spho_tp *tp)
{
	struct spho_tp *ret;

	if ((ret = spho_tp_alloc(sc)) == NULL)
		return (NULL);

	ret->form = SPHO_TP_FORM_MEMBER;
	ret->d.bind.nom = nom;
	ret->d.bind.bound = tp;

	return (ret);
}

/* Free type structure. External data (like nom) are freed elsewhere. */
void
spho_tp_destroy(struct spho_tp *tp)
{
	struct spho_tp *arg;

	switch (tp->form) {
	case SPHO_TP_FORM_TRUE:
	case SPHO_TP_FORM_FALSE:
	case SPHO_TP_FORM_NOM: 
		break;
	case SPHO_TP_FORM_CONJ:
	case SPHO_TP_FORM_DISJ:
	case SPHO_TP_FORM_IMPL:
	case SPHO_TP_FORM_ARROW:
		spho_tp_destroy(tp->d.binop.left);
		spho_tp_destroy(tp->d.binop.right);
		break;
	case SPHO_TP_FORM_BOX:
		spho_tp_destroy(tp->d.unop.operand);
		break;
	case SPHO_TP_FORM_FORALL:
	case SPHO_TP_FORM_MEMBER: 
		spho_tp_destroy(tp->d.bind.bound);
		break;
	case SPHO_TP_FORM_APPL:
		STAILQ_FOREACH(arg, tp->d.appl.args, entries) {
			spho_tp_destroy(arg);
		}
		free(tp->d.appl.args);
		break;
	default:
		SPHO_ASSERT(0);
		break;
	}

	spho_tp_free(tp);
}