Exposing type macro handling to API

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,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);
 }
 

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
  */

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
+ */
+__YICES_DLLSPEC__ 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
+ */
+__YICES_DLLSPEC__ 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
+ */
+__YICES_DLLSPEC__ 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]
+ */
+__YICES_DLLSPEC__ 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
+ */
+__YICES_DLLSPEC__ 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
+ */
+__YICES_DLLSPEC__ 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)
+ */
+__YICES_DLLSPEC__ extern void yices_delete_type_macro(int32_t id);
 
 
 /*************************

src/include/yices_limits.h

@@ -60,4 +60,11 @@
  */
 #define YICES_MAX_BVSIZE (UINT32_MAX/16)
 
+
+/*
+ * Maximal arity for type macros
+ */
+#define TYPE_MACRO_MAX_ARITY 128
+
+
 #endif

src/terms/types.h

@@ -194,14 +194,6 @@ typedef struct type_macro_s {
 
 
 
-/*
- * Maximal arity: it must satisfy two constraints
- * - max_arity <= TUPLE_HMAP_MAX_ARITY
- * - sizeof(type_macro_t) + sizeof(type_t) * max_arity <= UINT32_MAX
- * - a limit of 128 should be more than enough
- */
-#define TYPE_MACRO_MAX_ARITY 128
-
 /*
  * The type of an element in the macro table.
  */
@@ -225,7 +217,13 @@ typedef struct type_mtbl_s {
   tuple_hmap_t cache;   // existing macro instances
 } type_mtbl_t;
 
-
+/*
+ * For TYPE_MACRO_MAX_ARITY (defined in include/yices_limits.h):
+ * Maximal arity: it must satisfy two constraints
+ * - max_arity <= TUPLE_HMAP_MAX_ARITY
+ * - sizeof(type_macro_t) + sizeof(type_t) * max_arity <= UINT32_MAX
+ * - a limit of 128 should be more than enough
+ */
 
 /*
  * Default and maximal size