124 lines
3 KiB
C
124 lines
3 KiB
C
#ifndef _SPHO_TP_H
|
|
#define _SPHO_TP_H
|
|
|
|
/* base defs */
|
|
|
|
struct spho_alias {
|
|
struct spho_name name;
|
|
struct spho_tp *tp;
|
|
};
|
|
|
|
struct spho_rec {
|
|
struct spho_name mname;
|
|
struct spho_tp *tp;
|
|
};
|
|
|
|
/* type data */
|
|
struct tp_bin_data {
|
|
struct spho_tp *left;
|
|
struct spho_tp *right;
|
|
};
|
|
|
|
struct tp_box_data {
|
|
struct spho_tp *tp;
|
|
};
|
|
|
|
struct tp_forall_data {
|
|
struct spho_var *var;
|
|
struct spho_tp *tp;
|
|
};
|
|
|
|
struct tp_alias_data {
|
|
struct spho_alias *alias;
|
|
struct spho_tp_list *l;
|
|
};
|
|
|
|
struct tp_const_data {
|
|
struct spho_const *c;
|
|
};
|
|
|
|
struct tp_var_data {
|
|
struct spho_var *v;
|
|
};
|
|
|
|
struct tp_nominal_data {
|
|
struct spho_nom *n;
|
|
};
|
|
|
|
struct tp_record_data {
|
|
struct spho_rec *r;
|
|
};
|
|
|
|
/* type data union */
|
|
union tp_data {
|
|
struct tp_bin_data binop;
|
|
struct tp_box_data box;
|
|
struct tp_forall_data fa;
|
|
struct tp_alias_data alias;
|
|
struct tp_const_data cnst;
|
|
struct tp_var_data var;
|
|
struct tp_nominal_data nom;
|
|
struct tp_record_data rec;
|
|
};
|
|
|
|
#define SPHO_TP_FORM_UNKNOWN 0x00
|
|
|
|
#define SPHO_TP_FORM_DISJ 0x10
|
|
#define SPHO_TP_FORM_CONJ 0x11
|
|
#define SPHO_TP_FORM_IMPL 0x12
|
|
#define SPHO_TP_FORM_BOX 0x13
|
|
#define SPHO_TP_FORM_FORALL 0x14
|
|
#define SPHO_TP_FORM_ALIAS 0x15
|
|
|
|
#define SPHO_TP_FORM_FALSE 0x20
|
|
#define SPHO_TP_FORM_TRUE 0x21
|
|
#define SPHO_TP_FORM_VAR 0x22
|
|
#define SPHO_TP_FORM_NOM 0x23
|
|
|
|
#define SPHO_TP_FORM_REC 0x23
|
|
|
|
// TODO explain
|
|
#define SPHO_TP_FORM_SUB 0x96
|
|
|
|
/* sappho type */
|
|
struct spho_tp {
|
|
int form;
|
|
union tp_data data;
|
|
};
|
|
|
|
struct spho_nom *spho_nom_add(struct spho_ctx *, char *, size_t);
|
|
struct spho_nom *spho_nom_get_or_add(struct spho_ctx *, char *, size_t);
|
|
// struct spho_nom *spho_tp_nom_get(char *, size_t);
|
|
|
|
struct spho_var *spho_var_create(struct spho_ctx *, char *, size_t);
|
|
struct spho_var *spho_var_get(struct spho_ctx *, char *, size_t);
|
|
|
|
struct spho_alias *spho_alias_add(struct spho_ctx *, char *, size_t);
|
|
struct spho_alias *spho_alias_get(struct spho_ctx *, char *, size_t);
|
|
|
|
struct spho_tp *spho_tp_create_disj(struct spho_ctx *, struct spho_tp *,
|
|
struct spho_tp *, struct spho_tp *);
|
|
struct spho_tp *spho_tp_create_conj(struct spho_ctx *, struct spho_tp *,
|
|
struct spho_tp *, struct spho_tp *);
|
|
struct spho_tp *spho_tp_create_impl(struct spho_ctx *, struct spho_tp *,
|
|
struct spho_tp *, struct spho_tp *);
|
|
struct spho_tp *spho_tp_create_box(struct spho_ctx *, struct spho_tp *,
|
|
struct spho_tp *);
|
|
struct spho_tp *spho_tp_create_forall(struct spho_ctx *, struct spho_name *,
|
|
struct spho_tp *);
|
|
struct spho_tp *spho_tp_create_alias(struct spho_ctx *, struct spho_alias *,
|
|
struct spho_tp *);
|
|
struct spho_tp *spho_tp_create_const(struct spho_ctx *, struct spho_const *);
|
|
struct spho_tp *spho_tp_create_nominal(struct spho_ctx *,
|
|
struct spho_nom *);
|
|
struct spho_tp *spho_tp_create_var(struct spho_ctx *, struct spho_var *);
|
|
struct spho_tp *spho_tp_create_record(struct spho_ctx *, struct spho_rec *);
|
|
//struct spho_tp *spho_tp_create_sub(struct spho_ctx *, struct spho_tp *,
|
|
// struct spho_tp *);
|
|
|
|
void spho_tp_destroy(struct spho_tp*);
|
|
|
|
void spho_tp_free(struct spho_tp *);
|
|
|
|
|
|
#endif
|