1. Stl library

Start data section to lib/stl.flx[1 /1 ]
     1: #import <flx.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] = "(FLX_GXX_PARSER_HACK std::vector<?1>())";
    45:     fun create : int * t -> stl_vector[t]= "(FLX_GXX_PARSER_HACK std::vector<?1>($1,$2))";
    46:     fun create[i] : i * i -> stl_vector[t] = "(FLX_GXX_PARSER_HACK std::vector<?1>($1,$2))";
    47:     type stl_vector_iterator = "std::vector<?1>::iterator";
    48:     type stl_vector_reverse_iterator = "std::vector<?1>::reverse_iterator";
    49:     proc insert: stl_vector[t] * stl_vector_iterator[t] *  t  = "$1.insert($2,$3);";
    50:     proc push_back : stl_vector[t] *  t  = "$1.push_back($2);";
    51:     fun front : stl_vector[t] -> t = "$1.front()";
    52:     fun front : stl_vector[t] -> t = "$1.front()";
    53:     fun subscript : lvalue[stl_vector[t]] * int -> lvalue[t] = "$1.at($2)";
    54:     fun subscript : stl_vector[t] * int -> t = "$1.at($2)";
    55:     fun add: stl_vector_iterator[t] * int -> stl_vector_iterator[t] = "$1+$2";
    56:     fun sub: stl_vector_iterator[t] * int -> stl_vector_iterator[t] = "$1-$2";
    57:     proc pluseq: lvalue[stl_vector_iterator[t]] * int = "$1+=$2;";
    58:     proc minuseq: lvalue[stl_vector_iterator[t]] * int -> stl_vector_iterator[t] = "$1-=$2;";
    59:     fun subscript: stl_vector_iterator[t] * int -> lvalue[t] = "$1[$2]";
    60: // Vector
    61:   instance Eq[stl_vector[t]] {
    62:     fun eq: stl_vector[t] * stl_vector[t] -> bool = "$1==$2";
    63:   }
    64:   instance Container[stl_vector[t],t] {
    65:     fun len: stl_vector[t] -> size = "$1.size()";
    66:     fun empty: stl_vector[t] -> bool = "$1.empty()";
    67:   }
    68:   instance Sequence[stl_vector[t],stl_vector_iterator[t],t] {
    69:     fun begin : stl_vector[t]-> stl_vector_iterator[t]= "$1.begin()";
    70:     fun end : stl_vector[t]-> stl_vector_iterator[t]= "$1.end()";
    71:     proc erase : lvalue[stl_vector[t]] * stl_vector_iterator[t] = "$1.erase($1);";
    72:     proc erase_between : lvalue[stl_vector[t]] * stl_vector_iterator[t] * stl_vector_iterator[t] = "$1.erase($1,$2);";
    73:     proc clear : lvalue[stl_vector[t]] = "$1.clear();";
    74:     fun fold[i] (f:i->t->i) (var acc:i) (x:stl_vector[t]):i= {
    75:       var s = begin x; var e = end x;
    76:       whilst s != e do acc = f acc (*s); ++s; done;
    77:       return acc;
    78:     }
    79:   }
    80:   instance Reversible_Sequence[stl_vector[t],stl_vector_iterator[t],stl_vector_reverse_iterator[t],t] {
    81:     fun rbegin : stl_vector[t]-> stl_vector_reverse_iterator[t]= "$1.rbegin()";
    82:     fun rend : stl_vector[t]-> stl_vector_reverse_iterator[t]= "$1.rend()";
    83:     fun rfold[i] (f:i->t->i) (var acc:i) (x:stl_vector[t]):i= {
    84:       var s = rbegin x; var e = rend x;
    85:       whilst s != e do acc = f acc (*s); ++s; done;
    86:       return acc;
    87:     }
    88:   }
    89: 
    90: // Vector iterator
    91:   instance Eq[stl_vector_iterator[t]] {
    92:     fun eq: stl_vector_iterator[t] * stl_vector_iterator[t] -> bool = "$1==$2";
    93:   }
    94:   instance Tord[stl_vector_iterator[t]] {
    95:     fun lt: stl_vector_iterator[t] * stl_vector_iterator[t] -> bool = "$1<$2";
    96:   }
    97:   instance Iterator[stl_vector_iterator[t],t] {
    98:     fun deref : stl_vector_iterator[t] ->  lvalue[t]  = "*(#0*)(void*)&*$1";
    99:   }
   100:   instance Forward[stl_vector_iterator[t]] {
   101:     fun succ: stl_vector_iterator[t] -> stl_vector_iterator[t] = "$1+1";
   102:     proc pre_incr : lvalue[stl_vector_iterator[t]] = "++$1;";
   103:     proc post_incr : lvalue[stl_vector_iterator[t]] = "++$1;";
   104:   }
   105:   instance Forward_iterator[stl_vector_iterator[t],t] {}
   106:   instance Bidirectional[stl_vector_iterator[t]] {
   107:     fun pred: stl_vector_iterator[t] -> stl_vector_iterator[t] = "$1-11;";
   108:     proc pre_decr : lvalue[stl_vector_iterator[t]] = "--$1;";
   109:     proc post_decr : lvalue[stl_vector_iterator[t]] = "--$1;";
   110:   }
   111:   instance Bidirectional_iterator[stl_vector_iterator[t],t] {}
   112: 
   113: // Vector reverse iterator
   114:   instance Eq[stl_vector_reverse_iterator[t]] {
   115:     fun eq: stl_vector_reverse_iterator[t] * stl_vector_reverse_iterator[t] -> bool = "$1==$2";
   116:   }
   117:   instance Tord[stl_vector_reverse_iterator[t]] {
   118:     fun lt: stl_vector_reverse_iterator[t] * stl_vector_reverse_iterator[t] -> bool = "$1<$2";
   119:   }
   120:   instance Iterator[stl_vector_reverse_iterator[t],t] {
   121:     fun deref : stl_vector_reverse_iterator[t] ->  lvalue[t]  = "*(#0*)(void*)&*$1";
   122:   }
   123:   instance Forward[stl_vector_reverse_iterator[t]] {
   124:     fun succ: stl_vector_reverse_iterator[t] -> stl_vector_reverse_iterator[t] = "$1+1";
   125:     proc pre_incr : lvalue[stl_vector_reverse_iterator[t]] = "++$1;";
   126:     proc post_incr : lvalue[stl_vector_reverse_iterator[t]] = "++$1;";
   127:   }
   128:   instance Forward_iterator[stl_vector_reverse_iterator[t],t] {}
   129:   instance Bidirectional[stl_vector_reverse_iterator[t]] {
   130:     fun pred: stl_vector_reverse_iterator[t] -> stl_vector_reverse_iterator[t] = "$1-11;";
   131:     proc pre_decr : lvalue[stl_vector_reverse_iterator[t]] = "--$1;";
   132:     proc post_decr : lvalue[stl_vector_reverse_iterator[t]] = "--$1;";
   133:   }
   134:   instance Bidirectional_iterator[stl_vector_reverse_iterator[t],t] {}
   135: 
   136:   }
   137:   module List[t]
   138:   {
   139:     requires std_stl_list;
   140:     type stl_list = "std::list<?1>";
   141:     fun create : unit -> stl_list[t] = "(FLX_GXX_PARSER_HACK std::list<?1>())";
   142:     fun create : int * t -> stl_list[t]= "(FLX_GXX_PARSER_HACK std::list<?1>($1,$2))";
   143:     fun create[i] : i * i -> stl_list[t] = "(FLX_GXX_PARSER_HACK std::list<?1>($1,$2))";
   144:     type stl_list_iterator = "std::list<?1>::iterator";
   145:     type stl_list_reverse_iterator = "std::list<?1>::reverse_iterator";
   146:     proc insert: stl_list[t] * stl_list_iterator[t] *  t  = "$1.insert($2,$3);";
   147:     proc push_front : stl_list[t] *  t  = "$1.push_front($2);";
   148:     proc push_back : stl_list[t] *  t  = "$1.push_back($2);";
   149:     fun front : stl_list[t] -> t = "$1.front()";
   150:     fun front : stl_list[t] -> t = "$1.front()";
   151:     proc pop_front : stl_list[t] = "$1.pop_back();";
   152: // List
   153:   instance Eq[stl_list[t]] {
   154:     fun eq: stl_list[t] * stl_list[t] -> bool = "$1==$2";
   155:   }
   156:   instance Container[stl_list[t],t] {
   157:     fun len: stl_list[t] -> size = "$1.size()";
   158:     fun empty: stl_list[t] -> bool = "$1.empty()";
   159:   }
   160:   instance Sequence[stl_list[t],stl_list_iterator[t],t] {
   161:     fun begin : stl_list[t]-> stl_list_iterator[t]= "$1.begin()";
   162:     fun end : stl_list[t]-> stl_list_iterator[t]= "$1.end()";
   163:     proc erase : lvalue[stl_list[t]] * stl_list_iterator[t] = "$1.erase($1);";
   164:     proc erase_between : lvalue[stl_list[t]] * stl_list_iterator[t] * stl_list_iterator[t] = "$1.erase($1,$2);";
   165:     proc clear : lvalue[stl_list[t]] = "$1.clear();";
   166:     fun fold[i] (f:i->t->i) (var acc:i) (x:stl_list[t]):i= {
   167:       var s = begin x; var e = end x;
   168:       whilst s != e do acc = f acc (*s); ++s; done;
   169:       return acc;
   170:     }
   171:   }
   172:   instance Reversible_Sequence[stl_list[t],stl_list_iterator[t],stl_list_reverse_iterator[t],t] {
   173:     fun rbegin : stl_list[t]-> stl_list_reverse_iterator[t]= "$1.rbegin()";
   174:     fun rend : stl_list[t]-> stl_list_reverse_iterator[t]= "$1.rend()";
   175:     fun rfold[i] (f:i->t->i) (var acc:i) (x:stl_list[t]):i= {
   176:       var s = rbegin x; var e = rend x;
   177:       whilst s != e do acc = f acc (*s); ++s; done;
   178:       return acc;
   179:     }
   180:   }
   181: 
   182: // List iterator
   183:   instance Eq[stl_list_iterator[t]] {
   184:     fun eq: stl_list_iterator[t] * stl_list_iterator[t] -> bool = "$1==$2";
   185:   }
   186:   instance Tord[stl_list_iterator[t]] {
   187:     fun lt: stl_list_iterator[t] * stl_list_iterator[t] -> bool = "$1<$2";
   188:   }
   189:   instance Iterator[stl_list_iterator[t],t] {
   190:     fun deref : stl_list_iterator[t] ->  lvalue[t]  = "*(#0*)(void*)&*$1";
   191:   }
   192:   instance Forward[stl_list_iterator[t]] {
   193:     fun succ: stl_list_iterator[t] -> stl_list_iterator[t] = "$1+1";
   194:     proc pre_incr : lvalue[stl_list_iterator[t]] = "++$1;";
   195:     proc post_incr : lvalue[stl_list_iterator[t]] = "++$1;";
   196:   }
   197:   instance Forward_iterator[stl_list_iterator[t],t] {}
   198:   instance Bidirectional[stl_list_iterator[t]] {
   199:     fun pred: stl_list_iterator[t] -> stl_list_iterator[t] = "$1-11;";
   200:     proc pre_decr : lvalue[stl_list_iterator[t]] = "--$1;";
   201:     proc post_decr : lvalue[stl_list_iterator[t]] = "--$1;";
   202:   }
   203:   instance Bidirectional_iterator[stl_list_iterator[t],t] {}
   204: 
   205: // List reverse iterator
   206:   instance Eq[stl_list_reverse_iterator[t]] {
   207:     fun eq: stl_list_reverse_iterator[t] * stl_list_reverse_iterator[t] -> bool = "$1==$2";
   208:   }
   209:   instance Tord[stl_list_reverse_iterator[t]] {
   210:     fun lt: stl_list_reverse_iterator[t] * stl_list_reverse_iterator[t] -> bool = "$1<$2";
   211:   }
   212:   instance Iterator[stl_list_reverse_iterator[t],t] {
   213:     fun deref : stl_list_reverse_iterator[t] ->  lvalue[t]  = "*(#0*)(void*)&*$1";
   214:   }
   215:   instance Forward[stl_list_reverse_iterator[t]] {
   216:     fun succ: stl_list_reverse_iterator[t] -> stl_list_reverse_iterator[t] = "$1+1";
   217:     proc pre_incr : lvalue[stl_list_reverse_iterator[t]] = "++$1;";
   218:     proc post_incr : lvalue[stl_list_reverse_iterator[t]] = "++$1;";
   219:   }
   220:   instance Forward_iterator[stl_list_reverse_iterator[t],t] {}
   221:   instance Bidirectional[stl_list_reverse_iterator[t]] {
   222:     fun pred: stl_list_reverse_iterator[t] -> stl_list_reverse_iterator[t] = "$1-11;";
   223:     proc pre_decr : lvalue[stl_list_reverse_iterator[t]] = "--$1;";
   224:     proc post_decr : lvalue[stl_list_reverse_iterator[t]] = "--$1;";
   225:   }
   226:   instance Bidirectional_iterator[stl_list_reverse_iterator[t],t] {}
   227: 
   228:   }
   229:   module Deque[t]
   230:   {
   231:     requires std_stl_deque;
   232:     type stl_deque = "std::deque<?1>";
   233:     fun create : unit -> stl_deque[t] = "(FLX_GXX_PARSER_HACK std::deque<?1>())";
   234:     fun create : int * t -> stl_deque[t]= "(FLX_GXX_PARSER_HACK std::deque<?1>($1,$2))";
   235:     fun create[i] : i * i -> stl_deque[t] = "(FLX_GXX_PARSER_HACK std::deque<?1>($1,$2))";
   236:     type stl_deque_iterator = "std::deque<?1>::iterator";
   237:     type stl_deque_reverse_iterator = "std::deque<?1>::reverse_iterator";
   238:     proc insert: stl_deque[t] * stl_deque_iterator[t] *  t  = "$1.insert($2,$3);";
   239:     proc push_front : stl_deque[t] *  t  = "$1.push_front($2);";
   240:     proc push_back : stl_deque[t] *  t  = "$1.push_back($2);";
   241:     proc pop_front : stl_deque[t] = "$1.pop_back();";
   242:     fun front : stl_deque[t] -> t = "$1.front()";
   243:     fun front : stl_deque[t] -> t = "$1.front()";
   244:     fun subscript : lvalue[stl_deque[t]] * int -> lvalue[t] = "$1.at($2)";
   245:     fun subscript : stl_deque[t] * int -> t = "$1.at($2)";
   246: // Deque
   247:   instance Eq[stl_deque[t]] {
   248:     fun eq: stl_deque[t] * stl_deque[t] -> bool = "$1==$2";
   249:   }
   250:   instance Container[stl_deque[t],t] {
   251:     fun len: stl_deque[t] -> size = "$1.size()";
   252:     fun empty: stl_deque[t] -> bool = "$1.empty()";
   253:   }
   254:   instance Sequence[stl_deque[t],stl_deque_iterator[t],t] {
   255:     fun begin : stl_deque[t]-> stl_deque_iterator[t]= "$1.begin()";
   256:     fun end : stl_deque[t]-> stl_deque_iterator[t]= "$1.end()";
   257:     proc erase : lvalue[stl_deque[t]] * stl_deque_iterator[t] = "$1.erase($1);";
   258:     proc erase_between : lvalue[stl_deque[t]] * stl_deque_iterator[t] * stl_deque_iterator[t] = "$1.erase($1,$2);";
   259:     proc clear : lvalue[stl_deque[t]] = "$1.clear();";
   260:     fun fold[i] (f:i->t->i) (var acc:i) (x:stl_deque[t]):i= {
   261:       var s = begin x; var e = end x;
   262:       whilst s != e do acc = f acc (*s); ++s; done;
   263:       return acc;
   264:     }
   265:   }
   266:   instance Reversible_Sequence[stl_deque[t],stl_deque_iterator[t],stl_deque_reverse_iterator[t],t] {
   267:     fun rbegin : stl_deque[t]-> stl_deque_reverse_iterator[t]= "$1.rbegin()";
   268:     fun rend : stl_deque[t]-> stl_deque_reverse_iterator[t]= "$1.rend()";
   269:     fun rfold[i] (f:i->t->i) (var acc:i) (x:stl_deque[t]):i= {
   270:       var s = rbegin x; var e = rend x;
   271:       whilst s != e do acc = f acc (*s); ++s; done;
   272:       return acc;
   273:     }
   274:   }
   275: 
   276: // Deque iterator
   277:   instance Eq[stl_deque_iterator[t]] {
   278:     fun eq: stl_deque_iterator[t] * stl_deque_iterator[t] -> bool = "$1==$2";
   279:   }
   280:   instance Tord[stl_deque_iterator[t]] {
   281:     fun lt: stl_deque_iterator[t] * stl_deque_iterator[t] -> bool = "$1<$2";
   282:   }
   283:   instance Iterator[stl_deque_iterator[t],t] {
   284:     fun deref : stl_deque_iterator[t] ->  lvalue[t]  = "*(#0*)(void*)&*$1";
   285:   }
   286:   instance Forward[stl_deque_iterator[t]] {
   287:     fun succ: stl_deque_iterator[t] -> stl_deque_iterator[t] = "$1+1";
   288:     proc pre_incr : lvalue[stl_deque_iterator[t]] = "++$1;";
   289:     proc post_incr : lvalue[stl_deque_iterator[t]] = "++$1;";
   290:   }
   291:   instance Forward_iterator[stl_deque_iterator[t],t] {}
   292:   instance Bidirectional[stl_deque_iterator[t]] {
   293:     fun pred: stl_deque_iterator[t] -> stl_deque_iterator[t] = "$1-11;";
   294:     proc pre_decr : lvalue[stl_deque_iterator[t]] = "--$1;";
   295:     proc post_decr : lvalue[stl_deque_iterator[t]] = "--$1;";
   296:   }
   297:   instance Bidirectional_iterator[stl_deque_iterator[t],t] {}
   298: 
   299: // Deque reverse iterator
   300:   instance Eq[stl_deque_reverse_iterator[t]] {
   301:     fun eq: stl_deque_reverse_iterator[t] * stl_deque_reverse_iterator[t] -> bool = "$1==$2";
   302:   }
   303:   instance Tord[stl_deque_reverse_iterator[t]] {
   304:     fun lt: stl_deque_reverse_iterator[t] * stl_deque_reverse_iterator[t] -> bool = "$1<$2";
   305:   }
   306:   instance Iterator[stl_deque_reverse_iterator[t],t] {
   307:     fun deref : stl_deque_reverse_iterator[t] ->  lvalue[t]  = "*(#0*)(void*)&*$1";
   308:   }
   309:   instance Forward[stl_deque_reverse_iterator[t]] {
   310:     fun succ: stl_deque_reverse_iterator[t] -> stl_deque_reverse_iterator[t] = "$1+1";
   311:     proc pre_incr : lvalue[stl_deque_reverse_iterator[t]] = "++$1;";
   312:     proc post_incr : lvalue[stl_deque_reverse_iterator[t]] = "++$1;";
   313:   }
   314:   instance Forward_iterator[stl_deque_reverse_iterator[t],t] {}
   315:   instance Bidirectional[stl_deque_reverse_iterator[t]] {
   316:     fun pred: stl_deque_reverse_iterator[t] -> stl_deque_reverse_iterator[t] = "$1-11;";
   317:     proc pre_decr : lvalue[stl_deque_reverse_iterator[t]] = "--$1;";
   318:     proc post_decr : lvalue[stl_deque_reverse_iterator[t]] = "--$1;";
   319:   }
   320:   instance Bidirectional_iterator[stl_deque_reverse_iterator[t],t] {}
   321: 
   322:   }
   323:   module Set[t]
   324:   {
   325:     requires std_stl_set;
   326:     type stl_set = "std::set<?1>";
   327:     type stl_set_iterator = "std::set<?1>::iterator";
   328:     type stl_set_reverse_iterator = "std::set<?1>::reverse_iterator";
   329:     fun create : unit -> stl_set[t] = "(FLX_GXX_PARSER_HACK std::set<?1>())";
   330:     proc insert : stl_set[t] * t = "$1.insert($2);";
   331:     fun find : stl_set[t] * t ->  stl_set_iterator[t] = "$1.find($2)";
   332:     fun mem : stl_set[t] * t -> bool = "$1.find($2) != $1.end()";
   333: // Set
   334:   instance Eq[Set::stl_set[t]] {
   335:     fun eq: Set::stl_set[t] * Set::stl_set[t] -> bool = "$1==$2";
   336:   }
   337:   instance Container[Set::stl_set[t],t] {
   338:     fun len: Set::stl_set[t] -> size = "$1.size()";
   339:     fun empty: Set::stl_set[t] -> bool = "$1.empty()";
   340:   }
   341:   instance Sequence[Set::stl_set[t],Set::stl_set_iterator[t],t] {
   342:     fun begin : Set::stl_set[t]-> Set::stl_set_iterator[t]= "$1.begin()";
   343:     fun end : Set::stl_set[t]-> Set::stl_set_iterator[t]= "$1.end()";
   344:     proc erase : lvalue[Set::stl_set[t]] * Set::stl_set_iterator[t] = "$1.erase($1);";
   345:     proc erase_between : lvalue[Set::stl_set[t]] * Set::stl_set_iterator[t] * Set::stl_set_iterator[t] = "$1.erase($1,$2);";
   346:     proc clear : lvalue[Set::stl_set[t]] = "$1.clear();";
   347:     fun fold[i] (f:i->t->i) (var acc:i) (x:Set::stl_set[t]):i= {
   348:       var s = begin x; var e = end x;
   349:       whilst s != e do acc = f acc (*s); ++s; done;
   350:       return acc;
   351:     }
   352:   }
   353:   instance Reversible_Sequence[Set::stl_set[t],Set::stl_set_iterator[t],Set::stl_set_reverse_iterator[t],t] {
   354:     fun rbegin : Set::stl_set[t]-> Set::stl_set_reverse_iterator[t]= "$1.rbegin()";
   355:     fun rend : Set::stl_set[t]-> Set::stl_set_reverse_iterator[t]= "$1.rend()";
   356:     fun rfold[i] (f:i->t->i) (var acc:i) (x:Set::stl_set[t]):i= {
   357:       var s = rbegin x; var e = rend x;
   358:       whilst s != e do acc = f acc (*s); ++s; done;
   359:       return acc;
   360:     }
   361:   }
   362: 
   363: // Set iterator
   364:   instance Eq[stl_set_iterator[t]] {
   365:     fun eq: stl_set_iterator[t] * stl_set_iterator[t] -> bool = "$1==$2";
   366:   }
   367:   instance Tord[stl_set_iterator[t]] {
   368:     fun lt: stl_set_iterator[t] * stl_set_iterator[t] -> bool = "$1<$2";
   369:   }
   370:   instance Iterator[stl_set_iterator[t],t] {
   371:     fun deref : stl_set_iterator[t] ->  lvalue[t]  = "*(#0*)(void*)&*$1";
   372:   }
   373:   instance Forward[stl_set_iterator[t]] {
   374:     fun succ: stl_set_iterator[t] -> stl_set_iterator[t] = "$1+1";
   375:     proc pre_incr : lvalue[stl_set_iterator[t]] = "++$1;";
   376:     proc post_incr : lvalue[stl_set_iterator[t]] = "++$1;";
   377:   }
   378:   instance Forward_iterator[stl_set_iterator[t],t] {}
   379:   instance Bidirectional[stl_set_iterator[t]] {
   380:     fun pred: stl_set_iterator[t] -> stl_set_iterator[t] = "$1-11;";
   381:     proc pre_decr : lvalue[stl_set_iterator[t]] = "--$1;";
   382:     proc post_decr : lvalue[stl_set_iterator[t]] = "--$1;";
   383:   }
   384:   instance Bidirectional_iterator[stl_set_iterator[t],t] {}
   385: 
   386: // Set reverse iterator
   387:   instance Eq[stl_set_reverse_iterator[t]] {
   388:     fun eq: stl_set_reverse_iterator[t] * stl_set_reverse_iterator[t] -> bool = "$1==$2";
   389:   }
   390:   instance Tord[stl_set_reverse_iterator[t]] {
   391:     fun lt: stl_set_reverse_iterator[t] * stl_set_reverse_iterator[t] -> bool = "$1<$2";
   392:   }
   393:   instance Iterator[stl_set_reverse_iterator[t],t] {
   394:     fun deref : stl_set_reverse_iterator[t] ->  lvalue[t]  = "*(#0*)(void*)&*$1";
   395:   }
   396:   instance Forward[stl_set_reverse_iterator[t]] {
   397:     fun succ: stl_set_reverse_iterator[t] -> stl_set_reverse_iterator[t] = "$1+1";
   398:     proc pre_incr : lvalue[stl_set_reverse_iterator[t]] = "++$1;";
   399:     proc post_incr : lvalue[stl_set_reverse_iterator[t]] = "++$1;";
   400:   }
   401:   instance Forward_iterator[stl_set_reverse_iterator[t],t] {}
   402:   instance Bidirectional[stl_set_reverse_iterator[t]] {
   403:     fun pred: stl_set_reverse_iterator[t] -> stl_set_reverse_iterator[t] = "$1-11;";
   404:     proc pre_decr : lvalue[stl_set_reverse_iterator[t]] = "--$1;";
   405:     proc post_decr : lvalue[stl_set_reverse_iterator[t]] = "--$1;";
   406:   }
   407:   instance Bidirectional_iterator[stl_set_reverse_iterator[t],t] {}
   408: 
   409:   }
   410:   module MultiSet[t]
   411:   {
   412:     requires std_stl_set;
   413:     type stl_multiset = "std::multiset<?1>";
   414:     type stl_multiset_iterator = "std::multiset<?1>::iterator";
   415:     type stl_multiset_reverse_iterator = "std::multiset<?1>::reverse_iterator";
   416:     fun create : unit -> stl_multiset[t] = "(FLX_GXX_PARSER_HACK std::multiset<?1>())";
   417:     proc insert : stl_multiset[t] * t = "$1.insert($2);";
   418:     fun find : stl_multiset[t] * t ->  stl_multiset_iterator[t] = "$1.find($2)";
   419:     fun mem : stl_multiset[t] * t -> bool = "$1.find($2) != $1.end()";
   420: // MultiSet
   421:   instance Eq[stl_multiset[t]] {
   422:     fun eq: stl_multiset[t] * stl_multiset[t] -> bool = "$1==$2";
   423:   }
   424:   instance Container[stl_multiset[t],t] {
   425:     fun len: stl_multiset[t] -> size = "$1.size()";
   426:     fun empty: stl_multiset[t] -> bool = "$1.empty()";
   427:   }
   428:   instance Sequence[stl_multiset[t],stl_multiset_iterator[t],t] {
   429:     fun begin : stl_multiset[t]-> stl_multiset_iterator[t]= "$1.begin()";
   430:     fun end : stl_multiset[t]-> stl_multiset_iterator[t]= "$1.end()";
   431:     proc erase : lvalue[stl_multiset[t]] * stl_multiset_iterator[t] = "$1.erase($1);";
   432:     proc erase_between : lvalue[stl_multiset[t]] * stl_multiset_iterator[t] * stl_multiset_iterator[t] = "$1.erase($1,$2);";
   433:     proc clear : lvalue[stl_multiset[t]] = "$1.clear();";
   434:     fun fold[i] (f:i->t->i) (var acc:i) (x:stl_multiset[t]):i= {
   435:       var s = begin x; var e = end x;
   436:       whilst s != e do acc = f acc (*s); ++s; done;
   437:       return acc;
   438:     }
   439:   }
   440:   instance Reversible_Sequence[stl_multiset[t],stl_multiset_iterator[t],stl_multiset_reverse_iterator[t],t] {
   441:     fun rbegin : stl_multiset[t]-> stl_multiset_reverse_iterator[t]= "$1.rbegin()";
   442:     fun rend : stl_multiset[t]-> stl_multiset_reverse_iterator[t]= "$1.rend()";
   443:     fun rfold[i] (f:i->t->i) (var acc:i) (x:stl_multiset[t]):i= {
   444:       var s = rbegin x; var e = rend x;
   445:       whilst s != e do acc = f acc (*s); ++s; done;
   446:       return acc;
   447:     }
   448:   }
   449: 
   450: // MultiSet iterator
   451:   instance Eq[stl_multiset_iterator[t]] {
   452:     fun eq: stl_multiset_iterator[t] * stl_multiset_iterator[t] -> bool = "$1==$2";
   453:   }
   454:   instance Tord[stl_multiset_iterator[t]] {
   455:     fun lt: stl_multiset_iterator[t] * stl_multiset_iterator[t] -> bool = "$1<$2";
   456:   }
   457:   instance Iterator[stl_multiset_iterator[t],t] {
   458:     fun deref : stl_multiset_iterator[t] ->  lvalue[t]  = "*(#0*)(void*)&*$1";
   459:   }
   460:   instance Forward[stl_multiset_iterator[t]] {
   461:     fun succ: stl_multiset_iterator[t] -> stl_multiset_iterator[t] = "$1+1";
   462:     proc pre_incr : lvalue[stl_multiset_iterator[t]] = "++$1;";
   463:     proc post_incr : lvalue[stl_multiset_iterator[t]] = "++$1;";
   464:   }
   465:   instance Forward_iterator[stl_multiset_iterator[t],t] {}
   466:   instance Bidirectional[stl_multiset_iterator[t]] {
   467:     fun pred: stl_multiset_iterator[t] -> stl_multiset_iterator[t] = "$1-11;";
   468:     proc pre_decr : lvalue[stl_multiset_iterator[t]] = "--$1;";
   469:     proc post_decr : lvalue[stl_multiset_iterator[t]] = "--$1;";
   470:   }
   471:   instance Bidirectional_iterator[stl_multiset_iterator[t],t] {}
   472: 
   473: // MultiSet reverse iterator
   474:   instance Eq[stl_multiset_reverse_iterator[t]] {
   475:     fun eq: stl_multiset_reverse_iterator[t] * stl_multiset_reverse_iterator[t] -> bool = "$1==$2";
   476:   }
   477:   instance Tord[stl_multiset_reverse_iterator[t]] {
   478:     fun lt: stl_multiset_reverse_iterator[t] * stl_multiset_reverse_iterator[t] -> bool = "$1<$2";
   479:   }
   480:   instance Iterator[stl_multiset_reverse_iterator[t],t] {
   481:     fun deref : stl_multiset_reverse_iterator[t] ->  lvalue[t]  = "*(#0*)(void*)&*$1";
   482:   }
   483:   instance Forward[stl_multiset_reverse_iterator[t]] {
   484:     fun succ: stl_multiset_reverse_iterator[t] -> stl_multiset_reverse_iterator[t] = "$1+1";
   485:     proc pre_incr : lvalue[stl_multiset_reverse_iterator[t]] = "++$1;";
   486:     proc post_incr : lvalue[stl_multiset_reverse_iterator[t]] = "++$1;";
   487:   }
   488:   instance Forward_iterator[stl_multiset_reverse_iterator[t],t] {}
   489:   instance Bidirectional[stl_multiset_reverse_iterator[t]] {
   490:     fun pred: stl_multiset_reverse_iterator[t] -> stl_multiset_reverse_iterator[t] = "$1-11;";
   491:     proc pre_decr : lvalue[stl_multiset_reverse_iterator[t]] = "--$1;";
   492:     proc post_decr : lvalue[stl_multiset_reverse_iterator[t]] = "--$1;";
   493:   }
   494:   instance Bidirectional_iterator[stl_multiset_reverse_iterator[t],t] {}
   495: 
   496:   }
   497:   module Map[k,v]
   498:   {
   499:     requires std_stl_map;
   500:     type stl_map = "std::map<?1,?2>";
   501:     type stl_map_iterator = "std::map<?1,?2>::iterator";
   502:     type stl_map_reverse_iterator = "std::map<?1,?2>::reverse_iterator";
   503:     fun create : unit -> stl_map[k,v] = "(FLX_GXX_PARSER_HACK std::map<?1,?2>())";
   504:     fun subscript: stl_map[k,v] * k -> lvalue[v] = "$1[$2]";
   505:     fun find : stl_map[k,v] * k ->  stl_map_iterator[k,v] = "$1.find($2)";
   506:     fun mem : stl_map[k,v] * k -> bool = "$1.find($2) != $1.end()";
   507:     proc insert : stl_map[k,v] * k * v = "$1.insert(std::make_pair($2,$3));";
   508: // Map
   509:   instance Eq[stl_map[k,v]] {
   510:     fun eq: stl_map[k,v] * stl_map[k,v] -> bool = "$1==$2";
   511:   }
   512:   instance Container[stl_map[k,v],k*v] {
   513:     fun len: stl_map[k,v] -> size = "$1.size()";
   514:     fun empty: stl_map[k,v] -> bool = "$1.empty()";
   515:   }
   516:   instance Sequence[stl_map[k,v],stl_map_iterator[k,v],k*v] {
   517:     fun begin : stl_map[k,v]-> stl_map_iterator[k,v]= "$1.begin()";
   518:     fun end : stl_map[k,v]-> stl_map_iterator[k,v]= "$1.end()";
   519:     proc erase : lvalue[stl_map[k,v]] * stl_map_iterator[k,v] = "$1.erase($1);";
   520:     proc erase_between : lvalue[stl_map[k,v]] * stl_map_iterator[k,v] * stl_map_iterator[k,v] = "$1.erase($1,$2);";
   521:     proc clear : lvalue[stl_map[k,v]] = "$1.clear();";
   522:     fun fold[i] (f:i->k*v->i) (var acc:i) (x:stl_map[k,v]) :i= {
   523:       var s = begin x; var e = end x;
   524:       whilst s != e do acc = f acc (*s); ++s; done;
   525:       return acc;
   526:     }
   527:   }
   528:   instance Reversible_Sequence[stl_map[k,v],stl_map_iterator[k,v],stl_map_reverse_iterator[k,v],k*v] {
   529:     fun rbegin : stl_map[k,v]-> stl_map_reverse_iterator[k,v]= "$1.rbegin()";
   530:     fun rend : stl_map[k,v]-> stl_map_reverse_iterator[k,v]= "$1.rend()";
   531:     fun rfold[i] (f:i->k*v->i) (var acc:i) (x:stl_map[k,v]):i= {
   532:       var s = rbegin x; var e = rend x;
   533:       whilst s != e do acc = f acc (*s); ++s; done;
   534:       return acc;
   535:     }
   536:   }
   537: 
   538: // Map iterator
   539:   instance Eq[stl_map_iterator[k,v]] {
   540:     fun eq: stl_map_iterator[k,v] * stl_map_iterator[k,v] -> bool = "$1==$2";
   541:   }
   542:   instance Tord[stl_map_iterator[k,v]] {
   543:     fun lt: stl_map_iterator[k,v] * stl_map_iterator[k,v] -> bool = "$1<$2";
   544:   }
   545:   instance Iterator[stl_map_iterator[k,v],k*v] {
   546:     fun deref : stl_map_iterator[k,v] ->  lvalue[k*v]  = "*(#0*)(void*)&*$1";
   547:   }
   548:   instance Forward[stl_map_iterator[k,v]] {
   549:     fun succ: stl_map_iterator[k,v] -> stl_map_iterator[k,v] = "$1+1";
   550:     proc pre_incr : lvalue[stl_map_iterator[k,v]] = "++$1;";
   551:     proc post_incr : lvalue[stl_map_iterator[k,v]] = "++$1;";
   552:   }
   553:   instance Forward_iterator[stl_map_iterator[k,v],k*v] {}
   554:   instance Bidirectional[stl_map_iterator[k,v]] {
   555:     fun pred: stl_map_iterator[k,v] -> stl_map_iterator[k,v] = "$1-11;";
   556:     proc pre_decr : lvalue[stl_map_iterator[k,v]] = "--$1;";
   557:     proc post_decr : lvalue[stl_map_iterator[k,v]] = "--$1;";
   558:   }
   559:   instance Bidirectional_iterator[stl_map_iterator[k,v],k*v] {}
   560: 
   561: // Map reverse iterator
   562:   instance Eq[stl_map_reverse_iterator[k,v]] {
   563:     fun eq: stl_map_reverse_iterator[k,v] * stl_map_reverse_iterator[k,v] -> bool = "$1==$2";
   564:   }
   565:   instance Tord[stl_map_reverse_iterator[k,v]] {
   566:     fun lt: stl_map_reverse_iterator[k,v] * stl_map_reverse_iterator[k,v] -> bool = "$1<$2";
   567:   }
   568:   instance Iterator[stl_map_reverse_iterator[k,v],k*v] {
   569:     fun deref : stl_map_reverse_iterator[k,v] ->  lvalue[k*v]  = "*(#0*)(void*)&*$1";
   570:   }
   571:   instance Forward[stl_map_reverse_iterator[k,v]] {
   572:     fun succ: stl_map_reverse_iterator[k,v] -> stl_map_reverse_iterator[k,v] = "$1+1";
   573:     proc pre_incr : lvalue[stl_map_reverse_iterator[k,v]] = "++$1;";
   574:     proc post_incr : lvalue[stl_map_reverse_iterator[k,v]] = "++$1;";
   575:   }
   576:   instance Forward_iterator[stl_map_reverse_iterator[k,v],k*v] {}
   577:   instance Bidirectional[stl_map_reverse_iterator[k,v]] {
   578:     fun pred: stl_map_reverse_iterator[k,v] -> stl_map_reverse_iterator[k,v] = "$1-11;";
   579:     proc pre_decr : lvalue[stl_map_reverse_iterator[k,v]] = "--$1;";
   580:     proc post_decr : lvalue[stl_map_reverse_iterator[k,v]] = "--$1;";
   581:   }
   582:   instance Bidirectional_iterator[stl_map_reverse_iterator[k,v],k*v] {}
   583: 
   584:   }
   585:   module MultiMap[k,v]
   586:   {
   587:     requires std_stl_map;
   588:     type stl_multimap = "std::multimap<?1,?2>";
   589:     type stl_multimap_iterator = "std::multimap<?1,?2>::iterator";
   590:     type stl_multimap_reverse_iterator = "std::multimap<?1,?2>::reverse_iterator";
   591:     fun create : unit -> stl_multimap[k,v] = "(FLX_GXX_PARSER_HACK std::multimap<?1,?2>())";
   592:     fun subscript: stl_multimap[k,v] * k -> lvalue[v] = "$1[$2]";
   593:     fun find : stl_multimap[k,v] * k ->  stl_multimap_iterator[k,v] = "$1.find($2)";
   594:     fun mem : stl_multimap[k,v] * k -> bool = "$1.find($2) != $1.end()";
   595:     proc insert : stl_multimap[k,v] * k * v = "$1.insert(std::make_pair($2,$3));";
   596: // MultiMap
   597:   instance Eq[stl_multimap[k,v]] {
   598:     fun eq: stl_multimap[k,v] * stl_multimap[k,v] -> bool = "$1==$2";
   599:   }
   600:   instance Container[stl_multimap[k,v],k*v] {
   601:     fun len: stl_multimap[k,v] -> size = "$1.size()";
   602:     fun empty: stl_multimap[k,v] -> bool = "$1.empty()";
   603:   }
   604:   instance Sequence[stl_multimap[k,v],stl_multimap_iterator[k,v],k*v] {
   605:     fun begin : stl_multimap[k,v]-> stl_multimap_iterator[k,v]= "$1.begin()";
   606:     fun end : stl_multimap[k,v]-> stl_multimap_iterator[k,v]= "$1.end()";
   607:     proc erase : lvalue[stl_multimap[k,v]] * stl_multimap_iterator[k,v] = "$1.erase($1);";
   608:     proc erase_between : lvalue[stl_multimap[k,v]] * stl_multimap_iterator[k,v] * stl_multimap_iterator[k,v] = "$1.erase($1,$2);";
   609:     proc clear : lvalue[stl_multimap[k,v]] = "$1.clear();";
   610:     fun fold[i] (f:i->k*v->i) (var acc:i) (x:stl_multimap[k,v]) :i= {
   611:       var s = begin x; var e = end x;
   612:       whilst s != e do acc = f acc (*s); ++s; done;
   613:       return acc;
   614:     }
   615:   }
   616:   instance Reversible_Sequence[stl_multimap[k,v],stl_multimap_iterator[k,v],stl_multimap_reverse_iterator[k,v],k*v] {
   617:     fun rbegin : stl_multimap[k,v]-> stl_multimap_reverse_iterator[k,v]= "$1.rbegin()";
   618:     fun rend : stl_multimap[k,v]-> stl_multimap_reverse_iterator[k,v]= "$1.rend()";
   619:     fun rfold[i] (f:i->k*v->i) (var acc:i) (x:stl_multimap[k,v]):i= {
   620:       var s = rbegin x; var e = rend x;
   621:       whilst s != e do acc = f acc (*s); ++s; done;
   622:       return acc;
   623:     }
   624:   }
   625: 
   626: // MultiMap iterator
   627:   instance Eq[stl_multimap_iterator[k,v]] {
   628:     fun eq: stl_multimap_iterator[k,v] * stl_multimap_iterator[k,v] -> bool = "$1==$2";
   629:   }
   630:   instance Tord[stl_multimap_iterator[k,v]] {
   631:     fun lt: stl_multimap_iterator[k,v] * stl_multimap_iterator[k,v] -> bool = "$1<$2";
   632:   }
   633:   instance Iterator[stl_multimap_iterator[k,v],k*v] {
   634:     fun deref : stl_multimap_iterator[k,v] ->  lvalue[k*v]  = "*(#0*)(void*)&*$1";
   635:   }
   636:   instance Forward[stl_multimap_iterator[k,v]] {
   637:     fun succ: stl_multimap_iterator[k,v] -> stl_multimap_iterator[k,v] = "$1+1";
   638:     proc pre_incr : lvalue[stl_multimap_iterator[k,v]] = "++$1;";
   639:     proc post_incr : lvalue[stl_multimap_iterator[k,v]] = "++$1;";
   640:   }
   641:   instance Forward_iterator[stl_multimap_iterator[k,v],k*v] {}
   642:   instance Bidirectional[stl_multimap_iterator[k,v]] {
   643:     fun pred: stl_multimap_iterator[k,v] -> stl_multimap_iterator[k,v] = "$1-11;";
   644:     proc pre_decr : lvalue[stl_multimap_iterator[k,v]] = "--$1;";
   645:     proc post_decr : lvalue[stl_multimap_iterator[k,v]] = "--$1;";
   646:   }
   647:   instance Bidirectional_iterator[stl_multimap_iterator[k,v],k*v] {}
   648: 
   649: //MultiMap reverse iterator
   650:   instance Eq[stl_multimap_reverse_iterator[k,v]] {
   651:     fun eq: stl_multimap_reverse_iterator[k,v] * stl_multimap_reverse_iterator[k,v] -> bool = "$1==$2";
   652:   }
   653:   instance Tord[stl_multimap_reverse_iterator[k,v]] {
   654:     fun lt: stl_multimap_reverse_iterator[k,v] * stl_multimap_reverse_iterator[k,v] -> bool = "$1<$2";
   655:   }
   656:   instance Iterator[stl_multimap_reverse_iterator[k,v],k*v] {
   657:     fun deref : stl_multimap_reverse_iterator[k,v] ->  lvalue[k*v]  = "*(#0*)(void*)&*$1";
   658:   }
   659:   instance Forward[stl_multimap_reverse_iterator[k,v]] {
   660:     fun succ: stl_multimap_reverse_iterator[k,v] -> stl_multimap_reverse_iterator[k,v] = "$1+1";
   661:     proc pre_incr : lvalue[stl_multimap_reverse_iterator[k,v]] = "++$1;";
   662:     proc post_incr : lvalue[stl_multimap_reverse_iterator[k,v]] = "++$1;";
   663:   }
   664:   instance Forward_iterator[stl_multimap_reverse_iterator[k,v],k*v] {}
   665:   instance Bidirectional[stl_multimap_reverse_iterator[k,v]] {
   666:     fun pred: stl_multimap_reverse_iterator[k,v] -> stl_multimap_reverse_iterator[k,v] = "$1-11;";
   667:     proc pre_decr : lvalue[stl_multimap_reverse_iterator[k,v]] = "--$1;";
   668:     proc post_decr : lvalue[stl_multimap_reverse_iterator[k,v]] = "--$1;";
   669:   }
   670:   instance Bidirectional_iterator[stl_multimap_reverse_iterator[k,v],k*v] {}
   671: 
   672:   }
   673: 
   674:   module Slist[t]
   675:   {
   676:     requires ext_slist;
   677:     type stl_slist = "__gnu_cxx::slist<?1>";
   678:     fun create : unit -> stl_slist[t] = "(FLX_GXX_PARSER_HACK __gnu_cxx::slist<?1>())";
   679:     fun create : int * t -> stl_slist[t]= "(FLX_GXX_PARSER_HACK __gnu_cxx::slist<?1>($1,$2))";
   680:     fun create[i] : i * i -> stl_slist[t] = "(FLX_GXX_PARSER_HACK __gnu_cxx::slist<?1>($1,$2))";
   681:     type stl_slist_iterator = "__gnu_cxx::slist<?1>::iterator";
   682:     proc push_front : stl_slist[t] *  t  = "$1.push_front($2);";
   683:     fun front : stl_slist[t] -> t = "$1.front()";
   684:     proc pop_front : stl_slist[t] = "$1.pop_back();";
   685:     proc insert_after : stl_slist[t] * stl_slist_iterator[t] *  t  = "$1.insert_after($2,$3);";
   686:     proc erase_after : stl_slist[t] * stl_slist_iterator[t] = "$1.erase_after($1);";
   687:   }
   688: // HASHTABLE based containers assume
   689: // these classes will be added to C++ via TR1 in the future.
   690: // g++ 3.2.2 at least has these classes
   691: // The free SGI implementation may suffice as a replacement,
   692: // this is what my version of g++ uses.
   693: 
   694:   module HashSet[t]
   695:   {
   696:     requires ext_hash_set;
   697:     type stl_hash_set = "__gnu_cxx::hash_set<?1>";
   698:     type stl_hash_set_iterator = "__gnu_cxx::hash_set<?1>::iterator";
   699:     type stl_hash_set_reverse_iterator = "__gnu_cxx::hash_set<?1>::reverse_iterator";
   700:     fun create : unit -> stl_hash_set[t] = "(FLX_GXX_PARSER_HACK __gnu_cxx::hash_set<?1>())";
   701:     proc insert : stl_hash_set[t] * t = "$1.insert($2);";
   702:     fun find : stl_hash_set[t] * t ->  stl_hash_set_iterator[t] = "$1.find($2)";
   703:     fun mem : stl_hash_set[t] * t -> bool = "$1.find($2) != $1.end()";
   704:   }
   705:   module HashMultiSet[t]
   706:   {
   707:     requires ext_hash_set;
   708:     type stl_hash_multiset = "__gnu_cxx::hash_multiset<?1>";
   709:     fun create : unit -> stl_hash_multiset[t] = "(FLX_GXX_PARSER_HACK __gnu_cxx::hash_multiset<?1>())";
   710:     fun create : int * t -> stl_hash_multiset[t]= "(FLX_GXX_PARSER_HACK __gnu_cxx::hash_multiset<?1>($1,$2))";
   711:     fun create[i] : i * i -> stl_hash_multiset[t] = "(FLX_GXX_PARSER_HACK __gnu_cxx::hash_multiset<?1>($1,$2))";
   712:     type stl_hash_multiset_iterator = "__gnu_cxx::hash_multiset<?1>::iterator";
   713:   }
   714:   module HashMap[k,v]
   715:   {
   716:     requires ext_hash_map;
   717:     type stl_hash_map = "__gnu_cxx::hash_map<?1,?2>";
   718:     type stl_hash_map_iterator = "__gnu_cxx::hash_map<?1,?2>::iterator";
   719:     type stl_hash_map_reverse_iterator = "__gnu_cxx::hash_map<?1,?2>::reverse_iterator";
   720:     fun create : unit -> stl_hash_map[k,v] = "(FLX_GXX_PARSER_HACK __gnu_cxx::hash_map<?1,?2>())";
   721:     fun subscript: stl_hash_map[k,v] * k -> lvalue[v] = "$1[$2]";
   722:     fun find : stl_hash_map[k,v] * k ->  stl_hash_map_iterator[k,v] = "$1.find($2)";
   723:     fun mem : stl_hash_map[k,v] * k -> bool = "$1.find($2) != $1.end()";
   724:     proc insert : stl_hash_map[k,v] * k * v = "$1.insert(std::make_pair($2,$3));";
   725:   }
   726:   module HashMultiMap[k,v]
   727:   {
   728:     requires ext_hash_map;
   729:     type stl_hash_multimap = "__gnu_cxx::hash_multimap<?1,?2>";
   730:     type stl_hash_multimap_iterator = "__gnu_cxx::hash_multimap<?1,?2>::iterator";
   731:     type stl_hash_multimap_reverse_iterator = "__gnu_cxx::hash_multimap<?1,?2>::reverse_iterator";
   732:     fun create : unit -> stl_hash_multimap[k,v] = "(FLX_GXX_PARSER_HACK __gnu_cxx::hash_multimap<?1,?2>())";
   733:     fun subscript: stl_hash_multimap[k,v] * k -> lvalue[v] = "$1[$2]";
   734:     fun find : stl_hash_multimap[k,v] * k ->  stl_hash_multimap_iterator[k,v] = "$1.find($2)";
   735:     fun mem : stl_hash_multimap[k,v] * k -> bool = "$1.find($2) != $1.end()";
   736:     proc insert : stl_hash_multimap[k,v] * k * v = "$1.insert(std::make_pair($2,$3));";
   737:   }
   738: }
   739: 
   740: open Stl;
   741: open Stl::Vector;
   742: open[t] Reversible_Sequence[
   743:   Stl::Vector::stl_vector[t],
   744:   Stl::Vector::stl_vector_iterator[t],
   745:   Stl::Vector::stl_vector_reverse_iterator[t],t];
   746: open[t] Bidirectional_iterator[Stl::Vector::stl_vector_iterator[t],t];
   747: open[t] Bidirectional_iterator[Stl::Vector::stl_vector_reverse_iterator[t],t];
   748: 
   749: open Stl::List;
   750: open[t] Reversible_Sequence[
   751:   Stl::List::stl_list[t],
   752:   Stl::List::stl_list_iterator[t],
   753:   Stl::List::stl_list_reverse_iterator[t],t];
   754: open[t] Bidirectional_iterator[Stl::List::stl_list_iterator[t],t];
   755: open[t] Bidirectional_iterator[Stl::List::stl_list_reverse_iterator[t],t];
   756: 
   757: open Stl::Deque;
   758: open[t] Reversible_Sequence[
   759:   Stl::Deque::stl_deque[t],
   760:   Stl::Deque::stl_deque_iterator[t],
   761:   Stl::Deque::stl_deque_reverse_iterator[t],t];
   762: open[t] Bidirectional_iterator[Stl::Deque::stl_deque_iterator[t],t];
   763: open[t] Bidirectional_iterator[Stl::Deque::stl_deque_reverse_iterator[t],t];
   764: 
   765: open Stl::Set;
   766: open[t] Reversible_Sequence[
   767:   Stl::Set::stl_set[t],
   768:   Stl::Set::stl_set_iterator[t],
   769:   Stl::Set::stl_set_reverse_iterator[t],t];
   770: open[t] Bidirectional_iterator[Stl::Set::stl_set_iterator[t],t];
   771: open[t] Bidirectional_iterator[Stl::Set::stl_set_reverse_iterator[t],t];
   772: 
   773: open Stl::MultiSet;
   774: open[t] Reversible_Sequence[
   775:   Stl::MultiSet::stl_multiset[t],
   776:   Stl::MultiSet::stl_multiset_iterator[t],
   777:   Stl::MultiSet::stl_multiset_reverse_iterator[t],t];
   778: open[t] Bidirectional_iterator[Stl::MultiSet::stl_multiset_iterator[t],t];
   779: open[t] Bidirectional_iterator[Stl::MultiSet::stl_multiset_reverse_iterator[t],t];
   780: 
   781: open Stl::Map;
   782: open[k,v] Reversible_Sequence[
   783:   Stl::Map::stl_map[k,v],
   784:   Stl::Map::stl_map_iterator[k,v],
   785:   Stl::Map::stl_map_reverse_iterator[k,v],k*v];
   786: open[k,v] Bidirectional_iterator[Stl::Map::stl_map_iterator[k,v],k*v];
   787: open[k,v] Bidirectional_iterator[Stl::Map::stl_map_reverse_iterator[k,v],k*v];
   788: 
   789: open Stl::MultiMap;
   790: open[k,v] Reversible_Sequence[
   791:   Stl::MultiMap::stl_multimap[k,v],
   792:   Stl::MultiMap::stl_multimap_iterator[k,v],
   793:   Stl::MultiMap::stl_multimap_reverse_iterator[k,v],k*v];
   794: open[k,v] Bidirectional_iterator[Stl::MultiMap::stl_multimap_iterator[k,v],k*v];
   795: open[k,v] Bidirectional_iterator[Stl::MultiMap::stl_multimap_reverse_iterator[k,v],k*v];
   796: 
   797: 
End data section to lib/stl.flx[1]