Skip to content

Commit

Permalink
Exposing type macro handling to API
Browse files Browse the repository at this point in the history
  • Loading branch information
@cgjohannsen
cgjohannsen committed Jan 6, 2025
1 parent 37e652a commit 49db5be
Show file tree
Hide file tree
Showing 3 changed files with 97 additions and 102 deletions.
14 changes: 7 additions & 7 deletions src/api/yices_api.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2982,7 +2982,7 @@ EXPORTED type_t yices_function_type3(type_t tau1, type_t tau2, type_t tau3, type
/*
* Type variable with the given id
*/
type_t yices_type_variable(uint32_t id) {
EXPORTED type_t yices_type_variable(uint32_t id) {
return type_variable(__yices_globals.types, id);
}

Expand All @@ -2992,7 +2992,7 @@ type_t yices_type_variable(uint32_t id) {
* - n = arity
* return -1 if there's an error or the macro id otherwise
*/
int32_t yices_type_constructor(const char *name, uint32_t n) {
EXPORTED int32_t yices_type_constructor(const char *name, uint32_t n) {
char *clone;

if (! check_macro_arity(n)) {
Expand All @@ -3011,7 +3011,7 @@ int32_t yices_type_constructor(const char *name, uint32_t n) {
*
* return -1 if there's an error or the macro id otherwise
*/
int32_t yices_type_macro(const char *name, uint32_t n, type_t *vars, type_t body) {
EXPORTED int32_t yices_type_macro(const char *name, uint32_t n, type_t *vars, type_t body) {
char *clone;

if (! check_macro_arity(n) ||
Expand All @@ -3035,7 +3035,7 @@ int32_t yices_type_macro(const char *name, uint32_t n, type_t *vars, type_t body
*
* return NULL_TYPE if there's an error
*/
type_t yices_instance_type(int32_t cid, uint32_t n, type_t tau[]) {
EXPORTED type_t yices_instance_type(int32_t cid, uint32_t n, type_t tau[]) {
type_macro_t *macro;

macro = type_macro(__yices_globals.types, cid);
Expand Down Expand Up @@ -3066,7 +3066,7 @@ type_t yices_instance_type(int32_t cid, uint32_t n, type_t tau[]) {
* Get the macro id for a given name
* - return -1 if there's no macro or constructor with that name
*/
int32_t yices_get_macro_by_name(const char *name) {
EXPORTED int32_t yices_get_macro_by_name(const char *name) {
return get_type_macro_by_name(__yices_globals.types, name);
}

Expand All @@ -3075,15 +3075,15 @@ int32_t yices_get_macro_by_name(const char *name) {
* Remove the mapping of name --> macro id
* - no change if no such mapping exists
*/
void yices_remove_type_macro_name(const char *name) {
EXPORTED void yices_remove_type_macro_name(const char *name) {
remove_type_macro_name(__yices_globals.types, name);
}

/*
* Remove a macro with the given id
* - id must be a valid macro index (non-negative)
*/
void yices_delete_type_macro(int32_t id) {
EXPORTED void yices_delete_type_macro(int32_t id) {
delete_type_macro(__yices_globals.types, id);
}

Expand Down
95 changes: 0 additions & 95 deletions src/api/yices_extensions.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,101 +33,6 @@
#include "terms/terms.h"
#include "utils/int_array_hsets.h"


/*
* TYPE VARIABLES/MACROS
*/

/*
* Create a type variable of the given id
*/
extern type_t yices_type_variable(uint32_t id);

/*
* Create a type constructor:
* - name = its name
* - n = arity
* return -1 if there's an error or the macro id otherwise
*
* Error codes:
* if n == 0
* code = POS_INT_REQUIRED
* badval = n
, * if n > TYPE_MACRO_MAX_ARITY
* code = TOO_MANY_MACRO_PARAMS
* badval = n
*/
extern int32_t yices_type_constructor(const char *name, uint32_t n);

/*
* Create a type macro:
* - name = its name
* - n = arity
* - vars = array of n distinct type variables
* - body = type
*
* return -1 if there's an error or the macro id otherwise
*
* Error codes:
* if n == 0
* code = POS_INT_REQUIRED
* badval = n
* if n > TYPE_MACRO_MAX_ARITY
* code = TOO_MANY_MACRO_PARAMS
* badval = n
* if body or one of vars[i] is not a valid type
* code = INVALID_TYPE
* type1 = body or vars[i]
* if vars[i] is not a type variable
* code = TYPE_VAR_REQUIRED
* type1 = vars[i]
* if the same variable occurs twice or more in vars
* code = DUPLICATE_TYPE_VAR
* type1 = the duplicate variable
*/
extern int32_t yices_type_macro(const char *name, uint32_t n, type_t *vars, type_t body);


/*
* Instance of a macro or constructor
* - cid = constructor or macro id
* - n = number of arguments
* - tau[0 ... n-1] = argument types
*
* return NULL_TYPE if there's an error
*
* Error reports:
* if cid is not a valid macro or constructor id
* code = INVALID_MACRO
* badval = cid
* if n is not the same as the macro/constructor arity
* code = WRONG_NUMBER_OF_ARGUMENTS
* badval = n
* if one of tau[i] is not a valid type
* code = INVALID_TYPE
* type1 = tau[i]
*/
extern type_t yices_instance_type(int32_t cid, uint32_t n, type_t tau[]);

/*
* Get the macro id for a given name
* - return -1 if there's no macro or constructor with that name
*/
extern int32_t yices_get_macro_by_name(const char *name);

/*
* Remove the mapping of name --> macro id
* - no change if no such mapping exists
*/
extern void yices_remove_type_macro_name(const char *name);

/*
* Remove a macro with the given id
* - id must be a valid macro index (non-negative)
*/
extern void yices_delete_type_macro(int32_t id);


/*
* BUFFER ALLOCATION/FREE
*/
Expand Down
90 changes: 90 additions & 0 deletions src/include/yices.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -441,7 +441,97 @@ __YICES_DLLSPEC__ extern type_t yices_function_type1(type_t tau1, type_t range);
__YICES_DLLSPEC__ extern type_t yices_function_type2(type_t tau1, type_t tau2, type_t range);
__YICES_DLLSPEC__ extern type_t yices_function_type3(type_t tau1, type_t tau2, type_t tau3, type_t range);

/*************************
* TYPE MACROS *
************************/

/*
* Create a type variable of the given id
*/
extern type_t yices_type_variable(uint32_t id);

/*
* Create a type constructor:
* - name = its name
* - n = arity
* return -1 if there's an error or the macro id otherwise
*
* Error codes:
* if n == 0
* code = POS_INT_REQUIRED
* badval = n
, * if n > TYPE_MACRO_MAX_ARITY
* code = TOO_MANY_MACRO_PARAMS
* badval = n
*/
extern int32_t yices_type_constructor(const char *name, uint32_t n);

/*
* Create a type macro:
* - name = its name
* - n = arity
* - vars = array of n distinct type variables
* - body = type
*
* return -1 if there's an error or the macro id otherwise
*
* Error codes:
* if n == 0
* code = POS_INT_REQUIRED
* badval = n
* if n > TYPE_MACRO_MAX_ARITY
* code = TOO_MANY_MACRO_PARAMS
* badval = n
* if body or one of vars[i] is not a valid type
* code = INVALID_TYPE
* type1 = body or vars[i]
* if vars[i] is not a type variable
* code = TYPE_VAR_REQUIRED
* type1 = vars[i]
* if the same variable occurs twice or more in vars
* code = DUPLICATE_TYPE_VAR
* type1 = the duplicate variable
*/
extern int32_t yices_type_macro(const char *name, uint32_t n, type_t *vars, type_t body);

/*
* Instance of a macro or constructor
* - cid = constructor or macro id
* - n = number of arguments
* - tau[0 ... n-1] = argument types
*
* return NULL_TYPE if there's an error
*
* Error reports:
* if cid is not a valid macro or constructor id
* code = INVALID_MACRO
* badval = cid
* if n is not the same as the macro/constructor arity
* code = WRONG_NUMBER_OF_ARGUMENTS
* badval = n
* if one of tau[i] is not a valid type
* code = INVALID_TYPE
* type1 = tau[i]
*/
extern type_t yices_instance_type(int32_t cid, uint32_t n, type_t tau[]);

/*
* Get the macro id for a given name
* - return -1 if there's no macro or constructor with that name
*/
extern int32_t yices_get_macro_by_name(const char *name);

/*
* Remove the mapping of name --> macro id
* - no change if no such mapping exists
*/
extern void yices_remove_type_macro_name(const char *name);

/*
* Remove a macro with the given id
* - id must be a valid macro index (non-negative)
*/
extern void yices_delete_type_macro(int32_t id);


/*************************
Expand Down

0 comments on commit 49db5be

Please sign in to comment.