#ifndef _SPHO_TP_H
#define _SPHO_TP_H

#include "spho/scope.h"

#define SPHO_TP_FORM_UNKNOWN	0x00

#define SPHO_TP_FORM_CONJ	0x10
#define SPHO_TP_FORM_DISJ	0x11
#define SPHO_TP_FORM_IMPL	0x12
#define SPHO_TP_FORM_ARROW	0x13
#define SPHO_TP_FORM_BOX	0x14
#define SPHO_TP_FORM_FORALL	0x15
#define SPHO_TP_FORM_APPL	0x16
#define SPHO_TP_FORM_MEMBER	0x17
#define SPHO_TP_FORM_NOMINAL	0x18

#define SPHO_TP_FORM_TRUE	0x20
#define SPHO_TP_FORM_FALSE	0x21
#define SPHO_TP_FORM_NAME	0x23

#define SPHO_TP_FORM_VAR	0x40

#define SPHO_TP_FORM_MASK	0xff

#define SPHO_TP_MOD_FIRST	(SPHO_TP_FORM_MASK + 1)

// #define SPHO_TP_MOD_VAR		(SPHO_TP_FLAG_FIRST)
// #define SPHO_TP_MOD_NOMINAL	(SPHO_TP_FLAG_FIRST << 1)

#define SPHO_TP_ERR(tp, err)	SPHO_ERR((tp)->sc->ctx, (err))

struct spho_tp	*spho_tp_create_conj(struct spho_scope *, struct spho_tp *,
		    struct spho_tp *);
struct spho_tp	*spho_tp_create_disj(struct spho_scope *, struct spho_tp *,
		    struct spho_tp *);
struct spho_tp	*spho_tp_create_impl(struct spho_scope *, struct spho_tp *,
		    struct spho_tp *);
struct spho_tp	*spho_tp_create_arrow(struct spho_scope *, struct spho_tp *,
		    struct spho_tp *);
struct spho_tp	*spho_tp_create_box(struct spho_scope *, struct spho_tp *);
struct spho_tp	*spho_tp_create_forall(struct spho_scope *, struct spho_nom *,
		    struct spho_tp *);
struct spho_tp	*spho_tp_create_true(struct spho_scope *);
struct spho_tp	*spho_tp_create_false(struct spho_scope *);
struct spho_tp	*spho_tp_create_name(struct spho_scope *,
		    struct spho_nom *);
struct spho_tp	*spho_tp_create_appl(struct spho_scope *, struct spho_nom *,
		    struct spho_tp_l *);
struct spho_tp	*spho_tp_create_member(struct spho_scope *, struct spho_nom *,
		    struct spho_tp *);
struct spho_tp	*spho_tp_create_var(struct spho_scope *, struct spho_nom *);
struct spho_tp	*spho_tp_create_nominal(struct spho_scope *, struct spho_nom *);

struct spho_tp_op *spho_tp_op_create(struct spho_scope *,
    struct spho_scope *, struct spho_tp *);

void	spho_tp_destroy(struct spho_tp *);

#endif