3. Stl library

Start data section to lib/stl.flx[1 /1 ]
     1: #include <flx_categories.flxh>
     2: 
     3: include "std";
     4: header std_stl_vector = "#include <vector>";
     5: header std_stl_list = "#include <list>";
     6: header std_stl_deque = "#include <deque>";
     7: header std_stl_queue = "#include <queue>";
     8: header std_stl_set = "#include <set>";
     9: header std_stl_map = "#include <map>";
    10: header std_stl_stack = "#include <stack>";
    11: header ext_hash_set = "#include <ext/hash_set>";
    12: header ext_hash_map = "#include <ext/hash_map>";
    13: header ext_slist = "#include <ext/slist>";
    14: // hash for std::string for use with hash containers
    15: header ext_string_hash = """
    16:   namespace __gnu_cxx {
    17:     template<> struct hash<std::string> {
    18:       size_t operator()(std::string const& s)const;
    19:     };
    20:   }
    21: """;
    22: 
    23: body ext_string_hash = """
    24: // this is a sick hash .. fix it!
    25: size_t __gnu_cxx::hash<std::string>::
    26:   operator()(std::string const& s)const {
    27:     char const *p = s.data();
    28:     int n = s.size();
    29:     int h = 0;
    30:     for(; n; --n,++p) h+= 5 * *p;
    31:     return h;
    32:   }
    33: """;
    34: 
    35: module Stl
    36: {
    37:   type pair[k,v] = "std::pair<?1 const,?2>";
    38:   fun make_pair[k,v]: k * v ->pair[k,v] = "std::make_pair($1,$2)";
    39: 
    40:   module Vector[t]
    41:   {
    42:     requires std_stl_vector;
    43:     type stl_vector = "std::vector<?1>";
    44:     fun create : unit -> stl_vector[t] = "(GXX_PARSER_HACK std::vector<?1>())";
    45:     fun create : int * t -> stl_vector[t]= "(GXX_PARSER_HACK std::vector<?1>($1,$2))";
    46:     fun create[i] : i * i -> stl_vector[t] = "(GXX_PARSER_HACK std::vector<?1>($1,$2))";
    47:     gen_cmp stl_vector[t];
    48:     fun len: stl_vector[t] -> int = "$1.size()";
    49:     fun empty: stl_vector[t] -> int = "$1.empty()";
    50:     type stl_vector_iterator = "std::vector<?1>::iterator";
    51:     gen_cmp stl_vector_iterator[t];
    52:     gen_forward stl_vector_iterator[t];
    53:     fun deref : stl_vector_iterator[t] ->  lvalue[t]  = "*$1";
    54:     fun begin : stl_vector[t]-> stl_vector_iterator[t]= "$1.begin()";
    55:     fun end : stl_vector[t]-> stl_vector_iterator[t]= "$1.end()";
    56:     proc erase : stl_vector[t] * stl_vector_iterator[t] = "$1.erase($1);";
    57:     proc erase : stl_vector[t] * stl_vector_iterator[t] * stl_vector_iterator[t] = "$1.erase($1,$2);";
    58:     proc clear : stl_vector[t] = "$1.clear();";
    59:     proc pre_incr : lvalue[stl_vector_iterator[t]] = "++$1;";
    60:     proc post_incr : stl_vector_iterator[t] = "++$1;";
    61:     proc pre_decr : lvalue[stl_vector_iterator[t]] = "--$1;";
    62:     proc post_decr : stl_vector_iterator[t] = "--$1;";
    63:     type stl_vector_reverse_iterator = "std::vector<?1>::reverse_iterator";
    64:     fun rbegin : stl_vector[t]-> stl_vector_reverse_iterator[t]= "$1.rbegin()";
    65:     fun rend : stl_vector[t]-> stl_vector_reverse_iterator[t]= "$1.rend()";
    66:     fun deref : stl_vector_reverse_iterator[t] ->  lvalue[t]  = "*$1";
    67:     gen_cmp stl_vector_reverse_iterator[t];
    68:     proc pre_incr : lvalue[stl_vector_reverse_iterator[t]] = "++$1;";
    69:     proc post_incr : stl_vector_reverse_iterator[t] = "++$1;";
    70:     proc pre_decr: lvalue[stl_vector_reverse_iterator[t]] = "--$1;";
    71:     proc post_decr : stl_vector_reverse_iterator[t] = "--$1;";
    72:     proc insert: stl_vector[t] * stl_vector_iterator[t] *  t  = "$1.insert($2,$3);";
    73:     proc push_back : stl_vector[t] *  t  = "$1.push_back($2);";
    74:     fun front : stl_vector[t] -> t = "$1.front()";
    75:     fun front : stl_vector[t] -> t = "$1.front()";
    76:     fun subscript : lvalue[stl_vector[t]] * int -> lvalue[t] = "$1.at($2)";
    77:     fun subscript : stl_vector[t] * int -> t = "$1.at($2)";
    78:     fun add: stl_vector_iterator[t] * int -> stl_vector_iterator[t] = "$1+$2";
    79:     fun sub: stl_vector_iterator[t] * int -> stl_vector_iterator[t] = "$1-$2";
    80:     proc pluseq: lvalue[stl_vector_iterator[t]] * int = "$1+=$2;";
    81:     proc minuseq: lvalue[stl_vector_iterator[t]] * int -> stl_vector_iterator[t] = "$1-=$2;";
    82:     fun subscript: stl_vector_iterator[t] * int -> lvalue[t] = "$1[$2]";
    83:   }
    84:   module List[t]
    85:   {
    86:     requires std_stl_list;
    87:     type stl_list = "std::list<?1>";
    88:     fun create : unit -> stl_list[t] = "(GXX_PARSER_HACK std::list<?1>())";
    89:     fun create : int * t -> stl_list[t]= "(GXX_PARSER_HACK std::list<?1>($1,$2))";
    90:     fun create[i] : i * i -> stl_list[t] = "(GXX_PARSER_HACK std::list<?1>($1,$2))";
    91:     gen_cmp stl_list[t];
    92:     fun len: stl_list[t] -> int = "$1.size()";
    93:     fun empty: stl_list[t] -> int = "$1.empty()";
    94:     type stl_list_iterator = "std::list<?1>::iterator";
    95:     gen_cmp stl_list_iterator[t];
    96:     gen_forward stl_list_iterator[t];
    97:     fun deref : stl_list_iterator[t] ->  lvalue[t]  = "*$1";
    98:     fun begin : stl_list[t]-> stl_list_iterator[t]= "$1.begin()";
    99:     fun end : stl_list[t]-> stl_list_iterator[t]= "$1.end()";
   100:     proc erase : stl_list[t] * stl_list_iterator[t] = "$1.erase($1);";
   101:     proc erase : stl_list[t] * stl_list_iterator[t] * stl_list_iterator[t] = "$1.erase($1,$2);";
   102:     proc clear : stl_list[t] = "$1.clear();";
   103:     proc pre_incr : lvalue[stl_list_iterator[t]] = "++$1;";
   104:     proc post_incr : stl_list_iterator[t] = "++$1;";
   105:     proc pre_decr : lvalue[stl_list_iterator[t]] = "--$1;";
   106:     proc post_decr : stl_list_iterator[t] = "--$1;";
   107:     type stl_list_reverse_iterator = "std::list<?1>::reverse_iterator";
   108:     fun rbegin : stl_list[t]-> stl_list_reverse_iterator[t]= "$1.rbegin()";
   109:     fun rend : stl_list[t]-> stl_list_reverse_iterator[t]= "$1.rend()";
   110:     fun deref : stl_list_reverse_iterator[t] ->  lvalue[t]  = "*$1";
   111:     gen_cmp stl_list_reverse_iterator[t];
   112:     proc pre_incr : lvalue[stl_list_reverse_iterator[t]] = "++$1;";
   113:     proc post_incr : stl_list_reverse_iterator[t] = "++$1;";
   114:     proc pre_decr: lvalue[stl_list_reverse_iterator[t]] = "--$1;";
   115:     proc post_decr : stl_list_reverse_iterator[t] = "--$1;";
   116:     proc insert: stl_list[t] * stl_list_iterator[t] *  t  = "$1.insert($2,$3);";
   117:     proc push_front : stl_list[t] *  t  = "$1.push_front($2);";
   118:     proc push_back : stl_list[t] *  t  = "$1.push_back($2);";
   119:     fun front : stl_list[t] -> t = "$1.front()";
   120:     fun front : stl_list[t] -> t = "$1.front()";
   121:     proc pop_front : stl_list[t] = "$1.pop_back();";
   122:   }
   123:   module Queue[t]
   124:   {
   125:     requires std_stl_queue;
   126:     type stl_queue = "std::queue<?1>";
   127:     fun create : unit -> stl_queue[t] = "(GXX_PARSER_HACK std::queue<?1>())";
   128:     fun create : int * t -> stl_queue[t]= "(GXX_PARSER_HACK std::queue<?1>($1,$2))";
   129:     fun create[i] : i * i -> stl_queue[t] = "(GXX_PARSER_HACK std::queue<?1>($1,$2))";
   130:     gen_cmp stl_queue[t];
   131:     fun len: stl_queue[t] -> int = "$1.size()";
   132:     fun empty: stl_queue[t] -> int = "$1.empty()";
   133:     type stl_queue_iterator = "std::queue<?1>::iterator";
   134:     gen_cmp stl_queue_iterator[t];
   135:     gen_forward stl_queue_iterator[t];
   136:     fun deref : stl_queue_iterator[t] ->  lvalue[t]  = "*$1";
   137:     fun begin : stl_queue[t]-> stl_queue_iterator[t]= "$1.begin()";
   138:     fun end : stl_queue[t]-> stl_queue_iterator[t]= "$1.end()";
   139:     proc erase : stl_queue[t] * stl_queue_iterator[t] = "$1.erase($1);";
   140:     proc erase : stl_queue[t] * stl_queue_iterator[t] * stl_queue_iterator[t] = "$1.erase($1,$2);";
   141:     proc clear : stl_queue[t] = "$1.clear();";
   142:     proc pre_incr : lvalue[stl_queue_iterator[t]] = "++$1;";
   143:     proc post_incr : stl_queue_iterator[t] = "++$1;";
   144:     proc pre_decr : lvalue[stl_queue_iterator[t]] = "--$1;";
   145:     proc post_decr : stl_queue_iterator[t] = "--$1;";
   146:     proc insert: stl_queue[t] * stl_queue_iterator[t] *  t  = "$1.insert($2,$3);";
   147:   }
   148:   module Deque[t]
   149:   {
   150:     requires std_stl_deque;
   151:     type stl_deque = "std::deque<?1>";
   152:     fun create : unit -> stl_deque[t] = "(GXX_PARSER_HACK std::deque<?1>())";
   153:     fun create : int * t -> stl_deque[t]= "(GXX_PARSER_HACK std::deque<?1>($1,$2))";
   154:     fun create[i] : i * i -> stl_deque[t] = "(GXX_PARSER_HACK std::deque<?1>($1,$2))";
   155:     gen_cmp stl_deque[t];
   156:     fun len: stl_deque[t] -> int = "$1.size()";
   157:     fun empty: stl_deque[t] -> int = "$1.empty()";
   158:     type stl_deque_iterator = "std::deque<?1>::iterator";
   159:     gen_cmp stl_deque_iterator[t];
   160:     gen_forward stl_deque_iterator[t];
   161:     fun deref : stl_deque_iterator[t] ->  lvalue[t]  = "*$1";
   162:     fun begin : stl_deque[t]-> stl_deque_iterator[t]= "$1.begin()";
   163:     fun end : stl_deque[t]-> stl_deque_iterator[t]= "$1.end()";
   164:     proc erase : stl_deque[t] * stl_deque_iterator[t] = "$1.erase($1);";
   165:     proc erase : stl_deque[t] * stl_deque_iterator[t] * stl_deque_iterator[t] = "$1.erase($1,$2);";
   166:     proc clear : stl_deque[t] = "$1.clear();";
   167:     proc pre_incr : lvalue[stl_deque_iterator[t]] = "++$1;";
   168:     proc post_incr : stl_deque_iterator[t] = "++$1;";
   169:     proc pre_decr : lvalue[stl_deque_iterator[t]] = "--$1;";
   170:     proc post_decr : stl_deque_iterator[t] = "--$1;";
   171:     type stl_deque_reverse_iterator = "std::deque<?1>::reverse_iterator";
   172:     fun rbegin : stl_deque[t]-> stl_deque_reverse_iterator[t]= "$1.rbegin()";
   173:     fun rend : stl_deque[t]-> stl_deque_reverse_iterator[t]= "$1.rend()";
   174:     fun deref : stl_deque_reverse_iterator[t] ->  lvalue[t]  = "*$1";
   175:     gen_cmp stl_deque_reverse_iterator[t];
   176:     proc pre_incr : lvalue[stl_deque_reverse_iterator[t]] = "++$1;";
   177:     proc post_incr : stl_deque_reverse_iterator[t] = "++$1;";
   178:     proc pre_decr: lvalue[stl_deque_reverse_iterator[t]] = "--$1;";
   179:     proc post_decr : stl_deque_reverse_iterator[t] = "--$1;";
   180:     proc insert: stl_deque[t] * stl_deque_iterator[t] *  t  = "$1.insert($2,$3);";
   181:     proc push_front : stl_deque[t] *  t  = "$1.push_front($2);";
   182:     proc push_back : stl_deque[t] *  t  = "$1.push_back($2);";
   183:     proc pop_front : stl_deque[t] = "$1.pop_back();";
   184:     fun front : stl_deque[t] -> t = "$1.front()";
   185:     fun front : stl_deque[t] -> t = "$1.front()";
   186:     fun subscript : lvalue[stl_deque[t]] * int -> lvalue[t] = "$1.at($2)";
   187:     fun subscript : stl_deque[t] * int -> t = "$1.at($2)";
   188:   }
   189:   module PriorityQueue[t]
   190:   {
   191:     requires std_stl_queue;
   192:     type stl_priorityqueue = "std::priorityqueue<?1>";
   193:     fun create : unit -> stl_priorityqueue[t] = "(GXX_PARSER_HACK std::priorityqueue<?1>())";
   194:     fun create : int * t -> stl_priorityqueue[t]= "(GXX_PARSER_HACK std::priorityqueue<?1>($1,$2))";
   195:     fun create[i] : i * i -> stl_priorityqueue[t] = "(GXX_PARSER_HACK std::priorityqueue<?1>($1,$2))";
   196:     gen_cmp stl_priorityqueue[t];
   197:     fun len: stl_priorityqueue[t] -> int = "$1.size()";
   198:     fun empty: stl_priorityqueue[t] -> int = "$1.empty()";
   199:     type stl_priorityqueue_iterator = "std::priorityqueue<?1>::iterator";
   200:     gen_cmp stl_priorityqueue_iterator[t];
   201:     gen_forward stl_priorityqueue_iterator[t];
   202:     fun deref : stl_priorityqueue_iterator[t] ->  lvalue[t]  = "*$1";
   203:     fun begin : stl_priorityqueue[t]-> stl_priorityqueue_iterator[t]= "$1.begin()";
   204:     fun end : stl_priorityqueue[t]-> stl_priorityqueue_iterator[t]= "$1.end()";
   205:     proc erase : stl_priorityqueue[t] * stl_priorityqueue_iterator[t] = "$1.erase($1);";
   206:     proc erase : stl_priorityqueue[t] * stl_priorityqueue_iterator[t] * stl_priorityqueue_iterator[t] = "$1.erase($1,$2);";
   207:     proc clear : stl_priorityqueue[t] = "$1.clear();";
   208:     proc pre_incr : lvalue[stl_priorityqueue_iterator[t]] = "++$1;";
   209:     proc post_incr : stl_priorityqueue_iterator[t] = "++$1;";
   210:     proc pre_decr : lvalue[stl_priorityqueue_iterator[t]] = "--$1;";
   211:     proc post_decr : stl_priorityqueue_iterator[t] = "--$1;";
   212:   }
   213:   module Stack[t]
   214:   {
   215:     requires std_stl_stack;
   216:     type stl_stack = "std::stack<?1>";
   217:     fun create : unit -> stl_stack[t] = "(GXX_PARSER_HACK std::stack<?1>())";
   218:     fun create : int * t -> stl_stack[t]= "(GXX_PARSER_HACK std::stack<?1>($1,$2))";
   219:     fun create[i] : i * i -> stl_stack[t] = "(GXX_PARSER_HACK std::stack<?1>($1,$2))";
   220:     gen_cmp stl_stack[t];
   221:     fun len: stl_stack[t] -> int = "$1.size()";
   222:     fun empty: stl_stack[t] -> int = "$1.empty()";
   223:     type stl_stack_iterator = "std::stack<?1>::iterator";
   224:     gen_cmp stl_stack_iterator[t];
   225:     gen_forward stl_stack_iterator[t];
   226:     fun deref : stl_stack_iterator[t] ->  lvalue[t]  = "*$1";
   227:     fun begin : stl_stack[t]-> stl_stack_iterator[t]= "$1.begin()";
   228:     fun end : stl_stack[t]-> stl_stack_iterator[t]= "$1.end()";
   229:     proc erase : stl_stack[t] * stl_stack_iterator[t] = "$1.erase($1);";
   230:     proc erase : stl_stack[t] * stl_stack_iterator[t] * stl_stack_iterator[t] = "$1.erase($1,$2);";
   231:     proc clear : stl_stack[t] = "$1.clear();";
   232:     proc pre_incr : lvalue[stl_stack_iterator[t]] = "++$1;";
   233:     proc post_incr : stl_stack_iterator[t] = "++$1;";
   234:     proc pre_decr : lvalue[stl_stack_iterator[t]] = "--$1;";
   235:     proc post_decr : stl_stack_iterator[t] = "--$1;";
   236:   }
   237: 
   238:   module Set[t]
   239:   {
   240:     requires std_stl_set;
   241:     type stl_set = "std::set<?1>";
   242:     type stl_set_iterator = "std::set<?1>::iterator";
   243:     type stl_set_reverse_iterator = "std::set<?1>::reverse_iterator";
   244:     fun create : unit -> stl_set[t] = "(GXX_PARSER_HACK std::set<?1>())";
   245:     gen_cmp stl_set[t];
   246:     fun len: stl_set[t]->int = "$1.size()";
   247:     fun empty: stl_set[t]->int = "$1.empty()";
   248:     gen_cmp stl_set_iterator[t];
   249:     gen_cmp stl_set_reverse_iterator[t];
   250:     proc pre_incr : lvalue[stl_set_iterator[t]] = "++$1;";
   251:     proc post_incr : stl_set_iterator[t] = "++$1;";
   252:     proc pre_incr : lvalue[stl_set_reverse_iterator[t]] = "++$1;";
   253:     proc post_incr : stl_set_reverse_iterator[t] = "++$1;";
   254:     proc pre_decr : lvalue[stl_set_iterator[t]] = "--$1;";
   255:     proc post_decr : stl_set_iterator[t] = "--$1;";
   256:     proc pre_decr: lvalue[stl_set_reverse_iterator[t]] = "--$1;";
   257:     proc post_decr : stl_set_reverse_iterator[t] = "--$1;";
   258:     fun deref : stl_set_iterator[t] ->  t  = "*(#0*)&*$1:unary" is unary;
   259:     fun deref : stl_set_reverse_iterator[t] ->  t  = "*(#0*)&*$1:unary" is unary;
   260:     fun begin : stl_set[t]-> stl_set_iterator[t]= "$1.begin()";
   261:     fun end : stl_set[t]-> stl_set_iterator[t]= "$1.end()";
   262:     fun rbegin : stl_set[t]-> stl_set_reverse_iterator[t]= "$1.rbegin()";
   263:     fun rend : stl_set[t]-> stl_set_reverse_iterator[t]= "$1.rend()";
   264:     proc insert : stl_set[t] * t = "$1.insert($2);";
   265:     proc erase : stl_set[t] * stl_set_iterator[t] = "$1.erase($1);";
   266:     proc clear : stl_set[t] = "$1.clear();";
   267:     fun find : stl_set[t] * t ->  stl_set_iterator[t] = "$1.find($2)";
   268:     fun mem : stl_set[t] * t -> bool = "$1.find($2) != $1.end()";
   269:   }
   270:   module MultiSet[t]
   271:   {
   272:     requires std_stl_set;
   273:     type stl_multiset = "std::multiset<?1>";
   274:     type stl_multiset_iterator = "std::multiset<?1>::iterator";
   275:     type stl_multiset_reverse_iterator = "std::multiset<?1>::reverse_iterator";
   276:     fun create : unit -> stl_multiset[t] = "(GXX_PARSER_HACK std::multiset<?1>())";
   277:     gen_cmp stl_multiset[t];
   278:     fun len: stl_multiset[t]->int = "$1.size()";
   279:     fun empty: stl_multiset[t]->int = "$1.empty()";
   280:     gen_cmp stl_multiset_iterator[t];
   281:     gen_cmp stl_multiset_reverse_iterator[t];
   282:     proc pre_incr : lvalue[stl_multiset_iterator[t]] = "++$1;";
   283:     proc post_incr : stl_multiset_iterator[t] = "++$1;";
   284:     proc pre_incr : lvalue[stl_multiset_reverse_iterator[t]] = "++$1;";
   285:     proc post_incr : stl_multiset_reverse_iterator[t] = "++$1;";
   286:     proc pre_decr : lvalue[stl_multiset_iterator[t]] = "--$1;";
   287:     proc post_decr : stl_multiset_iterator[t] = "--$1;";
   288:     proc pre_decr: lvalue[stl_multiset_reverse_iterator[t]] = "--$1;";
   289:     proc post_decr : stl_multiset_reverse_iterator[t] = "--$1;";
   290:     fun deref : stl_multiset_iterator[t] ->  t  = "*(#0*)&*$1:unary" is unary;
   291:     fun deref : stl_multiset_reverse_iterator[t] ->  t  = "*(#0*)&*$1:unary" is unary;
   292:     fun begin : stl_multiset[t]-> stl_multiset_iterator[t]= "$1.begin()";
   293:     fun end : stl_multiset[t]-> stl_multiset_iterator[t]= "$1.end()";
   294:     fun rbegin : stl_multiset[t]-> stl_multiset_reverse_iterator[t]= "$1.rbegin()";
   295:     fun rend : stl_multiset[t]-> stl_multiset_reverse_iterator[t]= "$1.rend()";
   296:     proc insert : stl_multiset[t] * t = "$1.insert($2);";
   297:     proc erase : stl_multiset[t] * stl_multiset_iterator[t] = "$1.erase($1);";
   298:     proc clear : stl_multiset[t] = "$1.clear();";
   299:     fun find : stl_multiset[t] * t ->  stl_multiset_iterator[t] = "$1.find($2)";
   300:     fun mem : stl_multiset[t] * t -> bool = "$1.find($2) != $1.end()";
   301:   }
   302:   module Map[k,v]
   303:   {
   304:     requires std_stl_map;
   305:     type stl_map = "std::map<?1,?2>";
   306:     type stl_map_iterator = "std::map<?1,?2>::iterator";
   307:     type stl_map_reverse_iterator = "std::map<?1,?2>::reverse_iterator";
   308:     fun create : unit -> stl_map[k,v] = "(GXX_PARSER_HACK std::map<?1,?2>())";
   309:     gen_cmp stl_map[k,v];
   310:     fun len: stl_map[k,v]->int = "$1.size()";
   311:     fun empty: stl_map[k,v]->int = "$1.empty()";
   312:     gen_cmp stl_map_iterator[k,v];
   313:     gen_cmp stl_map_reverse_iterator[k,v];
   314:     proc pre_incr : stl_map_iterator[k,v] = "++$1;";
   315:     proc post_incr : stl_map_iterator[k,v] = "++$1;";
   316:     proc pre_incr : stl_map_reverse_iterator[k,v] = "++$1;";
   317:     proc post_incr : stl_map_reverse_iterator[k,v] = "++$1;";
   318:     proc pre_decr : stl_map_iterator[k,v] = "--$1;";
   319:     proc post_decr : stl_map_iterator[k,v] = "--$1;";
   320:     proc pre_decr : stl_map_reverse_iterator[k,v] = "--$1;";
   321:     proc post_decr : stl_map_reverse_iterator[k,v] = "--$1;";
   322:     fun deref : stl_map_iterator[k,v] ->  k * lvalue[v]  = "*(#0*)&*$1:unary" is unary;
   323:     fun begin : stl_map[k,v]-> stl_map_iterator[k,v]= "$1.begin()";
   324:     fun end : stl_map[k,v]-> stl_map_iterator[k,v]= "$1.end()";
   325:     fun deref : stl_map_reverse_iterator[k,v] ->  k * lvalue[v]  = "*(#0*)&*$1:unary" is unary;
   326:     fun rbegin : stl_map[k,v]-> stl_map_reverse_iterator[k,v]= "$1.rbegin()";
   327:     fun rend : stl_map[k,v]-> stl_map_reverse_iterator[k,v]= "$1.rend()";
   328:     proc insert : stl_map[k,v] * k * v = "$1.insert(std::make_pair($2,$3));";
   329:     proc erase : stl_map[k,v] * stl_map_iterator[k,v] = "$1.erase($1);";
   330:     proc clear : stl_map[k,v] = "$1.clear();";
   331:     fun find : stl_map[k,v] * k ->  stl_map_iterator[k,v] = "$1.find($2)";
   332:     fun mem : stl_map[k,v] * k -> bool = "$1.find($2) != $1.end()";
   333:     fun subscript: stl_map[k,v] * k -> lvalue[v] = "$1[$2]";
   334:   }
   335:   module MultiMap[k,v]
   336:   {
   337:     requires std_stl_map;
   338:     type stl_multimap = "std::multimap<?1,?2>";
   339:     type stl_multimap_iterator = "std::multimap<?1,?2>::iterator";
   340:     type stl_multimap_reverse_iterator = "std::multimap<?1,?2>::reverse_iterator";
   341:     fun create : unit -> stl_multimap[k,v] = "(GXX_PARSER_HACK std::multimap<?1,?2>())";
   342:     gen_cmp stl_multimap[k,v];
   343:     fun len: stl_multimap[k,v]->int = "$1.size()";
   344:     fun empty: stl_multimap[k,v]->int = "$1.empty()";
   345:     gen_cmp stl_multimap_iterator[k,v];
   346:     gen_cmp stl_multimap_reverse_iterator[k,v];
   347:     proc pre_incr : stl_multimap_iterator[k,v] = "++$1;";
   348:     proc post_incr : stl_multimap_iterator[k,v] = "++$1;";
   349:     proc pre_incr : stl_multimap_reverse_iterator[k,v] = "++$1;";
   350:     proc post_incr : stl_multimap_reverse_iterator[k,v] = "++$1;";
   351:     proc pre_decr : stl_multimap_iterator[k,v] = "--$1;";
   352:     proc post_decr : stl_multimap_iterator[k,v] = "--$1;";
   353:     proc pre_decr : stl_multimap_reverse_iterator[k,v] = "--$1;";
   354:     proc post_decr : stl_multimap_reverse_iterator[k,v] = "--$1;";
   355:     fun deref : stl_multimap_iterator[k,v] ->  k * lvalue[v]  = "*(#0*)&*$1:unary" is unary;
   356:     fun begin : stl_multimap[k,v]-> stl_multimap_iterator[k,v]= "$1.begin()";
   357:     fun end : stl_multimap[k,v]-> stl_multimap_iterator[k,v]= "$1.end()";
   358:     fun deref : stl_multimap_reverse_iterator[k,v] ->  k * lvalue[v]  = "*(#0*)&*$1:unary" is unary;
   359:     fun rbegin : stl_multimap[k,v]-> stl_multimap_reverse_iterator[k,v]= "$1.rbegin()";
   360:     fun rend : stl_multimap[k,v]-> stl_multimap_reverse_iterator[k,v]= "$1.rend()";
   361:     proc insert : stl_multimap[k,v] * k * v = "$1.insert(std::make_pair($2,$3));";
   362:     proc erase : stl_multimap[k,v] * stl_multimap_iterator[k,v] = "$1.erase($1);";
   363:     proc clear : stl_multimap[k,v] = "$1.clear();";
   364:     fun find : stl_multimap[k,v] * k ->  stl_multimap_iterator[k,v] = "$1.find($2)";
   365:     fun mem : stl_multimap[k,v] * k -> bool = "$1.find($2) != $1.end()";
   366:     fun subscript: stl_multimap[k,v] * k -> lvalue[v] = "$1[$2]";
   367:   }
   368: 
   369:   module Slist[t]
   370:   {
   371:     requires ext_slist;
   372:     type stl_slist = "__gnu_cxx::slist<?1>";
   373:     fun create : unit -> stl_slist[t] = "(GXX_PARSER_HACK __gnu_cxx::slist<?1>())";
   374:     fun create : int * t -> stl_slist[t]= "(GXX_PARSER_HACK __gnu_cxx::slist<?1>($1,$2))";
   375:     fun create[i] : i * i -> stl_slist[t] = "(GXX_PARSER_HACK __gnu_cxx::slist<?1>($1,$2))";
   376:     gen_cmp stl_slist[t];
   377:     fun len: stl_slist[t] -> int = "$1.size()";
   378:     fun empty: stl_slist[t] -> int = "$1.empty()";
   379:     type stl_slist_iterator = "__gnu_cxx::slist<?1>::iterator";
   380:     gen_cmp stl_slist_iterator[t];
   381:     gen_forward stl_slist_iterator[t];
   382:     fun deref : stl_slist_iterator[t] ->  lvalue[t]  = "*$1";
   383:     fun begin : stl_slist[t]-> stl_slist_iterator[t]= "$1.begin()";
   384:     fun end : stl_slist[t]-> stl_slist_iterator[t]= "$1.end()";
   385:     proc erase : stl_slist[t] * stl_slist_iterator[t] = "$1.erase($1);";
   386:     proc erase : stl_slist[t] * stl_slist_iterator[t] * stl_slist_iterator[t] = "$1.erase($1,$2);";
   387:     proc clear : stl_slist[t] = "$1.clear();";
   388:     proc pre_incr : lvalue[stl_slist_iterator[t]] = "++$1;";
   389:     proc post_incr : stl_slist_iterator[t] = "++$1;";
   390:     proc pre_decr : lvalue[stl_slist_iterator[t]] = "--$1;";
   391:     proc post_decr : stl_slist_iterator[t] = "--$1;";
   392:     proc push_front : stl_slist[t] *  t  = "$1.push_front($2);";
   393:     fun front : stl_slist[t] -> t = "$1.front()";
   394:     proc pop_front : stl_slist[t] = "$1.pop_back();";
   395:     proc insert_after : stl_slist[t] * stl_slist_iterator[t] *  t  = "$1.insert_after($2,$3);";
   396:     proc erase_after : stl_slist[t] * stl_slist_iterator[t] = "$1.erase_after($1);";
   397:   }
   398: // HASHTABLE based containers assume
   399: // these classes will be added to C++ via TR1 in the future.
   400: // g++ 3.2.2 at least has these classes
   401: // The free SGI implementation may suffice as a replacement,
   402: // this is what my version of g++ uses.
   403: 
   404:   module HashSet[t]
   405:   {
   406:     requires ext_hash_set;
   407:     type stl_hash_set = "__gnu_cxx::hash_set<?1>";
   408:     type stl_hash_set_iterator = "__gnu_cxx::hash_set<?1>::iterator";
   409:     type stl_hash_set_reverse_iterator = "__gnu_cxx::hash_set<?1>::reverse_iterator";
   410:     fun create : unit -> stl_hash_set[t] = "(GXX_PARSER_HACK __gnu_cxx::hash_set<?1>())";
   411:     gen_cmp stl_hash_set[t];
   412:     fun len: stl_hash_set[t]->int = "$1.size()";
   413:     fun empty: stl_hash_set[t]->int = "$1.empty()";
   414:     gen_cmp stl_hash_set_iterator[t];
   415:     gen_cmp stl_hash_set_reverse_iterator[t];
   416:     proc pre_incr : lvalue[stl_hash_set_iterator[t]] = "++$1;";
   417:     proc post_incr : stl_hash_set_iterator[t] = "++$1;";
   418:     proc pre_incr : lvalue[stl_hash_set_reverse_iterator[t]] = "++$1;";
   419:     proc post_incr : stl_hash_set_reverse_iterator[t] = "++$1;";
   420:     proc pre_decr : lvalue[stl_hash_set_iterator[t]] = "--$1;";
   421:     proc post_decr : stl_hash_set_iterator[t] = "--$1;";
   422:     proc pre_decr: lvalue[stl_hash_set_reverse_iterator[t]] = "--$1;";
   423:     proc post_decr : stl_hash_set_reverse_iterator[t] = "--$1;";
   424:     fun deref : stl_hash_set_iterator[t] ->  t  = "*(#0*)&*$1:unary" is unary;
   425:     fun deref : stl_hash_set_reverse_iterator[t] ->  t  = "*(#0*)&*$1:unary" is unary;
   426:     fun begin : stl_hash_set[t]-> stl_hash_set_iterator[t]= "$1.begin()";
   427:     fun end : stl_hash_set[t]-> stl_hash_set_iterator[t]= "$1.end()";
   428:     fun rbegin : stl_hash_set[t]-> stl_hash_set_reverse_iterator[t]= "$1.rbegin()";
   429:     fun rend : stl_hash_set[t]-> stl_hash_set_reverse_iterator[t]= "$1.rend()";
   430:     proc insert : stl_hash_set[t] * t = "$1.insert($2);";
   431:     proc erase : stl_hash_set[t] * stl_hash_set_iterator[t] = "$1.erase($1);";
   432:     proc clear : stl_hash_set[t] = "$1.clear();";
   433:     fun find : stl_hash_set[t] * t ->  stl_hash_set_iterator[t] = "$1.find($2)";
   434:     fun mem : stl_hash_set[t] * t -> bool = "$1.find($2) != $1.end()";
   435:   }
   436:   module HashMultiSet[t]
   437:   {
   438:     requires ext_hash_set;
   439:     type stl_hash_multiset = "__gnu_cxx::hash_multiset<?1>";
   440:     fun create : unit -> stl_hash_multiset[t] = "(GXX_PARSER_HACK __gnu_cxx::hash_multiset<?1>())";
   441:     fun create : int * t -> stl_hash_multiset[t]= "(GXX_PARSER_HACK __gnu_cxx::hash_multiset<?1>($1,$2))";
   442:     fun create[i] : i * i -> stl_hash_multiset[t] = "(GXX_PARSER_HACK __gnu_cxx::hash_multiset<?1>($1,$2))";
   443:     gen_cmp stl_hash_multiset[t];
   444:     fun len: stl_hash_multiset[t] -> int = "$1.size()";
   445:     fun empty: stl_hash_multiset[t] -> int = "$1.empty()";
   446:     type stl_hash_multiset_iterator = "__gnu_cxx::hash_multiset<?1>::iterator";
   447:     gen_cmp stl_hash_multiset_iterator[t];
   448:     gen_forward stl_hash_multiset_iterator[t];
   449:     fun deref : stl_hash_multiset_iterator[t] ->  lvalue[t]  = "*$1";
   450:     fun begin : stl_hash_multiset[t]-> stl_hash_multiset_iterator[t]= "$1.begin()";
   451:     fun end : stl_hash_multiset[t]-> stl_hash_multiset_iterator[t]= "$1.end()";
   452:     proc erase : stl_hash_multiset[t] * stl_hash_multiset_iterator[t] = "$1.erase($1);";
   453:     proc erase : stl_hash_multiset[t] * stl_hash_multiset_iterator[t] * stl_hash_multiset_iterator[t] = "$1.erase($1,$2);";
   454:     proc clear : stl_hash_multiset[t] = "$1.clear();";
   455:     proc pre_incr : lvalue[stl_hash_multiset_iterator[t]] = "++$1;";
   456:     proc post_incr : stl_hash_multiset_iterator[t] = "++$1;";
   457:     proc pre_decr : lvalue[stl_hash_multiset_iterator[t]] = "--$1;";
   458:     proc post_decr : stl_hash_multiset_iterator[t] = "--$1;";
   459:   }
   460:   module HashMap[k,v]
   461:   {
   462:     requires ext_hash_map;
   463:     type stl_hash_map = "__gnu_cxx::hash_map<?1,?2>";
   464:     type stl_hash_map_iterator = "__gnu_cxx::hash_map<?1,?2>::iterator";
   465:     type stl_hash_map_reverse_iterator = "__gnu_cxx::hash_map<?1,?2>::reverse_iterator";
   466:     fun create : unit -> stl_hash_map[k,v] = "(GXX_PARSER_HACK __gnu_cxx::hash_map<?1,?2>())";
   467:     gen_cmp stl_hash_map[k,v];
   468:     fun len: stl_hash_map[k,v]->int = "$1.size()";
   469:     fun empty: stl_hash_map[k,v]->int = "$1.empty()";
   470:     gen_cmp stl_hash_map_iterator[k,v];
   471:     gen_cmp stl_hash_map_reverse_iterator[k,v];
   472:     proc pre_incr : stl_hash_map_iterator[k,v] = "++$1;";
   473:     proc post_incr : stl_hash_map_iterator[k,v] = "++$1;";
   474:     proc pre_incr : stl_hash_map_reverse_iterator[k,v] = "++$1;";
   475:     proc post_incr : stl_hash_map_reverse_iterator[k,v] = "++$1;";
   476:     proc pre_decr : stl_hash_map_iterator[k,v] = "--$1;";
   477:     proc post_decr : stl_hash_map_iterator[k,v] = "--$1;";
   478:     proc pre_decr : stl_hash_map_reverse_iterator[k,v] = "--$1;";
   479:     proc post_decr : stl_hash_map_reverse_iterator[k,v] = "--$1;";
   480:     fun deref : stl_hash_map_iterator[k,v] ->  k * lvalue[v]  = "*(#0*)&*$1:unary" is unary;
   481:     fun begin : stl_hash_map[k,v]-> stl_hash_map_iterator[k,v]= "$1.begin()";
   482:     fun end : stl_hash_map[k,v]-> stl_hash_map_iterator[k,v]= "$1.end()";
   483:     fun deref : stl_hash_map_reverse_iterator[k,v] ->  k * lvalue[v]  = "*(#0*)&*$1:unary" is unary;
   484:     fun rbegin : stl_hash_map[k,v]-> stl_hash_map_reverse_iterator[k,v]= "$1.rbegin()";
   485:     fun rend : stl_hash_map[k,v]-> stl_hash_map_reverse_iterator[k,v]= "$1.rend()";
   486:     proc insert : stl_hash_map[k,v] * k * v = "$1.insert(std::make_pair($2,$3));";
   487:     proc erase : stl_hash_map[k,v] * stl_hash_map_iterator[k,v] = "$1.erase($1);";
   488:     proc clear : stl_hash_map[k,v] = "$1.clear();";
   489:     fun find : stl_hash_map[k,v] * k ->  stl_hash_map_iterator[k,v] = "$1.find($2)";
   490:     fun mem : stl_hash_map[k,v] * k -> bool = "$1.find($2) != $1.end()";
   491:     fun subscript: stl_hash_map[k,v] * k -> lvalue[v] = "$1[$2]";
   492:   }
   493:   module HashMultiMap[k,v]
   494:   {
   495:     requires ext_hash_map;
   496:     type stl_hash_multimap = "__gnu_cxx::hash_multimap<?1,?2>";
   497:     type stl_hash_multimap_iterator = "__gnu_cxx::hash_multimap<?1,?2>::iterator";
   498:     type stl_hash_multimap_reverse_iterator = "__gnu_cxx::hash_multimap<?1,?2>::reverse_iterator";
   499:     fun create : unit -> stl_hash_multimap[k,v] = "(GXX_PARSER_HACK __gnu_cxx::hash_multimap<?1,?2>())";
   500:     gen_cmp stl_hash_multimap[k,v];
   501:     fun len: stl_hash_multimap[k,v]->int = "$1.size()";
   502:     fun empty: stl_hash_multimap[k,v]->int = "$1.empty()";
   503:     gen_cmp stl_hash_multimap_iterator[k,v];
   504:     gen_cmp stl_hash_multimap_reverse_iterator[k,v];
   505:     proc pre_incr : stl_hash_multimap_iterator[k,v] = "++$1;";
   506:     proc post_incr : stl_hash_multimap_iterator[k,v] = "++$1;";
   507:     proc pre_incr : stl_hash_multimap_reverse_iterator[k,v] = "++$1;";
   508:     proc post_incr : stl_hash_multimap_reverse_iterator[k,v] = "++$1;";
   509:     proc pre_decr : stl_hash_multimap_iterator[k,v] = "--$1;";
   510:     proc post_decr : stl_hash_multimap_iterator[k,v] = "--$1;";
   511:     proc pre_decr : stl_hash_multimap_reverse_iterator[k,v] = "--$1;";
   512:     proc post_decr : stl_hash_multimap_reverse_iterator[k,v] = "--$1;";
   513:     fun deref : stl_hash_multimap_iterator[k,v] ->  k * lvalue[v]  = "*(#0*)&*$1:unary" is unary;
   514:     fun begin : stl_hash_multimap[k,v]-> stl_hash_multimap_iterator[k,v]= "$1.begin()";
   515:     fun end : stl_hash_multimap[k,v]-> stl_hash_multimap_iterator[k,v]= "$1.end()";
   516:     fun deref : stl_hash_multimap_reverse_iterator[k,v] ->  k * lvalue[v]  = "*(#0*)&*$1:unary" is unary;
   517:     fun rbegin : stl_hash_multimap[k,v]-> stl_hash_multimap_reverse_iterator[k,v]= "$1.rbegin()";
   518:     fun rend : stl_hash_multimap[k,v]-> stl_hash_multimap_reverse_iterator[k,v]= "$1.rend()";
   519:     proc insert : stl_hash_multimap[k,v] * k * v = "$1.insert(std::make_pair($2,$3));";
   520:     proc erase : stl_hash_multimap[k,v] * stl_hash_multimap_iterator[k,v] = "$1.erase($1);";
   521:     proc clear : stl_hash_multimap[k,v] = "$1.clear();";
   522:     fun find : stl_hash_multimap[k,v] * k ->  stl_hash_multimap_iterator[k,v] = "$1.find($2)";
   523:     fun mem : stl_hash_multimap[k,v] * k -> bool = "$1.find($2) != $1.end()";
   524:     fun subscript: stl_hash_multimap[k,v] * k -> lvalue[v] = "$1[$2]";
   525:   }
   526: }
End data section to lib/stl.flx[1]