//
// sorted_insert.pp
//
// Insert an Ar_Vertex into an Ar_Vertex_list sorted in order of decreasing
// cardinality of the alternation reachable sets.  This is done by 
// constructing a new list with the new vertex added in the appropriate
// place.
//

*operation* Ar_Vertex_list* arsize_insert(Ar_Vertex *arv)
  *init* (@ new Ar_Vertex_list @)
  *traverse* *from* Ar_Vertex_list *to* Ar_Vertex
  *carry* *in* int ar_size = (@ (arv->get_ar_set())->list_length() @)
    *along* *from* Ar_Vertex_list *to* Ar_Vertex
  *carry* *inout* int added = (@ 0 @)
    *along* *from* Ar_Vertex_list *to* Ar_Vertex
  *wrapper* Ar_Vertex
    *prefix* (@ 
      if (!added) {
        if (ar_size >= this->ar->list_length()) {
          return_val->append(arv);
          added = 1;
        }
      }
      return_val->append(this);
    @)
  *wrapper* Ar_Vertex_list
    *suffix* (@ if (!added) return_val->append(arv); @)