Plugins

typedef struct intList {
   struct intListNode* first;
} *INTLIST;

typedef struct intListNode {
   int value;
   struct intListNode* next;
} *INTLISTNODE;

typedef INTLIST intList_t;
typedef INTLISTNODE intListNode_t;

intList_t list;

void acme_initialize_list (int argc) {
   list = (intList_t) malloc(sizeof(struct intList));
   list->first = NULL;
   for(int i=0; i < (argc * 2); i++) {
      intListNode_t r = (intListNode_t) malloc(sizeof(struct intListNode));
      r->value = i*2+1;
      r->next = list->first;
      list->first = r;
   }
}

void acme_update_list (int v1, int v2) {
   intListNode_t r = (intListNode_t) malloc(sizeof(struct intListNode));
   r->value = v1*2+1;
   r->next = list->first;
   list->first = r;
   r = (intListNode_t) malloc(sizeof(struct intListNode));
   r->value = v2*4+1;
   r->next = list->first;
   list->first = r;
}

int acme_invariant_length_VALUE_0 () {
   int length = 0;
   intListNode_t i = list->first;
   while (i != NULL) {
     length++;
     i = i->next;
   };
   return length % 2;
}

int acme_invariant_odd_VALUE_0 (int v) {
   int value = 3;
   intListNode_t i = list->first;
   int times = v;
   while ((i != NULL) && (times > 0)) {
     value = i->value;
     times--;
     i = i->next;
   };
   return value % 2 - 1;
}

   --Transform=InitPlugins \
       --InitPluginsCollectionPrefix=Set \
       --InitPluginsDictionaryPrefix=HashMap

#include "tigress.h"
#include  
#include 
#include 
#include 
#include 
#include 

// Types for Sets.
typedef ... Set_TYPE;
typedef ... Set_ELEMENT;
typedef ... Set_ITER;

// Create and destroy a set
Set_TYPE Set_CREATE(){ ... }
void Set_DESTROY(Set_TYPE *a) { ... }

// Merge sets in different ways (union, intersection, etc). 
Set_TYPE Set_JOIN_union(Set_TYPE a, Set_TYPE b) { ... } 
Set_TYPE Set_JOIN_diff(Set_TYPE a, Set_TYPE b){ ... }

// Insert and delete elements from the set.
void Set_INSERT(Set_TYPE a, Set_ELEMENT b) { ... }
void Set_DELETE(Set_TYPE a, Set_ELEMENT b) { ... }

// Query the set
int Set_MEMBER(Set_TYPE a, Set_ELEMENT b){ ... }
int Set_SIZE(Set_TYPE a){ ... }

// Iterate through the elements of the set. Here's the pattern to use:
// Set_ITER i = Set_FIRST(s);
// while not Set_DONE(s, i) {
//   Set_ELEMENT e = Set_GET(s,i);
//   Do something with e;
//   i = Set_NEXT(s,i);
// }
Set_ITER Set_FIRST(Set_TYPE a){ ... }
Set_ITER Set_NEXT(Set_TYPE a, Set_ITER n){ ... }
int Set_DONE(Set_TYPE a, Set_ITER n){ ... }
Set_ELEMENT Set_GET(Set_TYPE a, Set_ITER n){ ... }

// Similar for HashMaps (instances of a Dictionary ADT).
typedef ... HashMap_TYPE;
typedef ... HashMap_KEY;
typedef ... HashMap_ELEMENT;
typedef ... HashMap_ITER;

HashMap_TYPE HashMap_CREATE(){ ... }
void HashMap_INSERT(HashMap_TYPE a, HashMap_KEY b, HashMap_ELEMENT c) { ... }
void HashMap_DELETE(HashMap_TYPE a, HashMap_KEY b) { ... }
int HashMap_MEMBER(HashMap_TYPE a, HashMap_KEY b){ ... }
HashMap_ELEMENT HashMap_LOOKUP(HashMap_TYPE a, HashMap_KEY b){ ... }
void HashMap_DESTROY(HashMap_TYPE *a) { ... }
int HashMap_SIZE(Set_TYPE a){ ... }
HashMap_KEY HashMap_NTH(Set_TYPE a, int n){ ... }
HashMap_ITER HashMap_FIRST(HashMap_TYPE a){ ... }
HashMap_ITER HashMap_NEXT(HashMap_TYPE a, HashMap_ITER n){ ... }
int HashMap_DONE(HashMap_TYPE a, HashMap_ITER n){ ... }
HashMap_ELEMENT HashMap_GET(HashMap_TYPE a, HashMap_ITER n){ ... }