From 49db5be6c0e77181bc735fb168b89f539ebd0e02 Mon Sep 17 00:00:00 2001 From: cgjohannsen Date: Mon, 6 Jan 2025 15:50:06 -0600 Subject: [PATCH] Exposing type macro handling to API --- src/api/yices_api.c | 14 +++--- src/api/yices_extensions.h | 95 -------------------------------------- src/include/yices.h | 90 ++++++++++++++++++++++++++++++++++++ 3 files changed, 97 insertions(+), 102 deletions(-) diff --git a/src/api/yices_api.c b/src/api/yices_api.c index bfd44b311..5d2312088 100644 --- a/src/api/yices_api.c +++ b/src/api/yices_api.c @@ -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); } @@ -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)) { @@ -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) || @@ -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); @@ -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); } @@ -3075,7 +3075,7 @@ 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); } @@ -3083,7 +3083,7 @@ 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) */ -void yices_delete_type_macro(int32_t id) { +EXPORTED void yices_delete_type_macro(int32_t id) { delete_type_macro(__yices_globals.types, id); } diff --git a/src/api/yices_extensions.h b/src/api/yices_extensions.h index 3e2cb9ffd..0c0e8af6a 100644 --- a/src/api/yices_extensions.h +++ b/src/api/yices_extensions.h @@ -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 */ diff --git a/src/include/yices.h b/src/include/yices.h index fc87cc642..2f7da03bf 100644 --- a/src/include/yices.h +++ b/src/include/yices.h @@ -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); /*************************