#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