#include "flx_categories.flx"
include "std";
header std_stl_vector = "#include <vector>";
header std_stl_list = "#include <list>";
header std_stl_deque = "#include <deque>";
header std_stl_queue = "#include <queue>";
header std_stl_set = "#include <set>";
header std_stl_map = "#include <map>";
header std_stl_stack = "#include <stack>";
header ext_hash_set = "#include <ext/hash_set>";
header ext_hash_map = "#include <ext/hash_map>";
header ext_slist = "#include <ext/slist>";
// hash for std::string for use with hash containers
header ext_string_hash = """
namespace __gnu_cxx {
template<> struct hash<std::string> {
size_t operator()(std::string const& s)const;
};
}
""";
body ext_string_hash = """
// this is a sick hash .. fix it!
size_t __gnu_cxx::hash<std::string>::
operator()(std::string const& s)const {
char const *p = s.data();
int n = s.size();
int h = 0;
for(; n; --n,++p) h+= 5 * *p;
return h;
}
""";
module Stl
{
type pair[k,v] = "std::pair<?1 const,?2>";
fun make_pair[k,v]: k * v ->pair[k,v] = "std::make_pair($1,$2)";
module Vector[t]
{
requires std_stl_vector;
type stl_vector = "std::vector<?1>";
fun create : unit -> stl_vector[t] = "(GXX_PARSER_HACK std::vector<?1>())";
fun create : int * t -> stl_vector[t]= "(GXX_PARSER_HACK std::vector<?1>($1,$2))";
fun create[i] : i * i -> stl_vector[t] = "(GXX_PARSER_HACK std::vector<?1>($1,$2))";
gen_cmp stl_vector[t];
fun len: stl_vector[t] -> int = "$1.size()";
fun empty: stl_vector[t] -> int = "$1.empty()";
type stl_vector_iterator = "std::vector<?1>::iterator";
gen_cmp stl_vector_iterator[t];
gen_forward stl_vector_iterator[t];
fun deref : stl_vector_iterator[t] -> lvalue[t] = "*$1";
fun begin : stl_vector[t]-> stl_vector_iterator[t]= "$1.begin()";
fun end : stl_vector[t]-> stl_vector_iterator[t]= "$1.end()";
proc erase : stl_vector[t] * stl_vector_iterator[t] = "$1.erase($1);";
proc erase : stl_vector[t] * stl_vector_iterator[t] * stl_vector_iterator[t] = "$1.erase($1,$2);";
proc clear : stl_vector[t] = "$1.clear();";
proc pre_incr : lvalue[stl_vector_iterator[t]] = "++$1;";
proc post_incr : stl_vector_iterator[t] = "++$1;";
proc pre_decr : lvalue[stl_vector_iterator[t]] = "--$1;";
proc post_decr : stl_vector_iterator[t] = "--$1;";
type stl_vector_reverse_iterator = "std::vector<?1>::reverse_iterator";
fun rbegin : stl_vector[t]-> stl_vector_reverse_iterator[t]= "$1.rbegin()";
fun rend : stl_vector[t]-> stl_vector_reverse_iterator[t]= "$1.rend()";
fun deref : stl_vector_reverse_iterator[t] -> lvalue[t] = "*$1";
gen_cmp stl_vector_reverse_iterator[t];
proc pre_incr : lvalue[stl_vector_reverse_iterator[t]] = "++$1;";
proc post_incr : stl_vector_reverse_iterator[t] = "++$1;";
proc pre_decr: lvalue[stl_vector_reverse_iterator[t]] = "--$1;";
proc post_decr : stl_vector_reverse_iterator[t] = "--$1;";
proc insert: stl_vector[t] * stl_vector_iterator[t] * t = "$1.insert($2,$3);";
proc push_back : stl_vector[t] * t = "$1.push_back($2);";
fun front : stl_vector[t] -> t = "$1.front()";
fun front : stl_vector[t] -> t = "$1.front()";
fun subscript : lvalue[stl_vector[t]] * int -> lvalue[t] = "$1.at($2)";
fun subscript : stl_vector[t] * int -> t = "$1.at($2)";
fun add: stl_vector_iterator[t] * int -> stl_vector_iterator[t] = "$1+$2";
fun sub: stl_vector_iterator[t] * int -> stl_vector_iterator[t] = "$1-$2";
proc pluseq: lvalue[stl_vector_iterator[t]] * int = "$1+=$2;";
proc minuseq: lvalue[stl_vector_iterator[t]] * int -> stl_vector_iterator[t] = "$1-=$2;";
fun subscript: stl_vector_iterator[t] * int -> lvalue[t] = "$1[$2]";
}
module List[t]
{
requires std_stl_list;
type stl_list = "std::list<?1>";
fun create : unit -> stl_list[t] = "(GXX_PARSER_HACK std::list<?1>())";
fun create : int * t -> stl_list[t]= "(GXX_PARSER_HACK std::list<?1>($1,$2))";
fun create[i] : i * i -> stl_list[t] = "(GXX_PARSER_HACK std::list<?1>($1,$2))";
gen_cmp stl_list[t];
fun len: stl_list[t] -> int = "$1.size()";
fun empty: stl_list[t] -> int = "$1.empty()";
type stl_list_iterator = "std::list<?1>::iterator";
gen_cmp stl_list_iterator[t];
gen_forward stl_list_iterator[t];
fun deref : stl_list_iterator[t] -> lvalue[t] = "*$1";
fun begin : stl_list[t]-> stl_list_iterator[t]= "$1.begin()";
fun end : stl_list[t]-> stl_list_iterator[t]= "$1.end()";
proc erase : stl_list[t] * stl_list_iterator[t] = "$1.erase($1);";
proc erase : stl_list[t] * stl_list_iterator[t] * stl_list_iterator[t] = "$1.erase($1,$2);";
proc clear : stl_list[t] = "$1.clear();";
proc pre_incr : lvalue[stl_list_iterator[t]] = "++$1;";
proc post_incr : stl_list_iterator[t] = "++$1;";
proc pre_decr : lvalue[stl_list_iterator[t]] = "--$1;";
proc post_decr : stl_list_iterator[t] = "--$1;";
type stl_list_reverse_iterator = "std::list<?1>::reverse_iterator";
fun rbegin : stl_list[t]-> stl_list_reverse_iterator[t]= "$1.rbegin()";
fun rend : stl_list[t]-> stl_list_reverse_iterator[t]= "$1.rend()";
fun deref : stl_list_reverse_iterator[t] -> lvalue[t] = "*$1";
gen_cmp stl_list_reverse_iterator[t];
proc pre_incr : lvalue[stl_list_reverse_iterator[t]] = "++$1;";
proc post_incr : stl_list_reverse_iterator[t] = "++$1;";
proc pre_decr: lvalue[stl_list_reverse_iterator[t]] = "--$1;";
proc post_decr : stl_list_reverse_iterator[t] = "--$1;";
proc insert: stl_list[t] * stl_list_iterator[t] * t = "$1.insert($2,$3);";
proc push_front : stl_list[t] * t = "$1.push_front($2);";
proc push_back : stl_list[t] * t = "$1.push_back($2);";
fun front : stl_list[t] -> t = "$1.front()";
fun front : stl_list[t] -> t = "$1.front()";
proc pop_front : stl_list[t] = "$1.pop_back();";
}
module Queue[t]
{
requires std_stl_queue;
type stl_queue = "std::queue<?1>";
fun create : unit -> stl_queue[t] = "(GXX_PARSER_HACK std::queue<?1>())";
fun create : int * t -> stl_queue[t]= "(GXX_PARSER_HACK std::queue<?1>($1,$2))";
fun create[i] : i * i -> stl_queue[t] = "(GXX_PARSER_HACK std::queue<?1>($1,$2))";
gen_cmp stl_queue[t];
fun len: stl_queue[t] -> int = "$1.size()";
fun empty: stl_queue[t] -> int = "$1.empty()";
type stl_queue_iterator = "std::queue<?1>::iterator";
gen_cmp stl_queue_iterator[t];
gen_forward stl_queue_iterator[t];
fun deref : stl_queue_iterator[t] -> lvalue[t] = "*$1";
fun begin : stl_queue[t]-> stl_queue_iterator[t]= "$1.begin()";
fun end : stl_queue[t]-> stl_queue_iterator[t]= "$1.end()";
proc erase : stl_queue[t] * stl_queue_iterator[t] = "$1.erase($1);";
proc erase : stl_queue[t] * stl_queue_iterator[t] * stl_queue_iterator[t] = "$1.erase($1,$2);";
proc clear : stl_queue[t] = "$1.clear();";
proc pre_incr : lvalue[stl_queue_iterator[t]] = "++$1;";
proc post_incr : stl_queue_iterator[t] = "++$1;";
proc pre_decr : lvalue[stl_queue_iterator[t]] = "--$1;";
proc post_decr : stl_queue_iterator[t] = "--$1;";
proc insert: stl_queue[t] * stl_queue_iterator[t] * t = "$1.insert($2,$3);";
}
module Deque[t]
{
requires std_stl_deque;
type stl_deque = "std::deque<?1>";
fun create : unit -> stl_deque[t] = "(GXX_PARSER_HACK std::deque<?1>())";
fun create : int * t -> stl_deque[t]= "(GXX_PARSER_HACK std::deque<?1>($1,$2))";
fun create[i] : i * i -> stl_deque[t] = "(GXX_PARSER_HACK std::deque<?1>($1,$2))";
gen_cmp stl_deque[t];
fun len: stl_deque[t] -> int = "$1.size()";
fun empty: stl_deque[t] -> int = "$1.empty()";
type stl_deque_iterator = "std::deque<?1>::iterator";
gen_cmp stl_deque_iterator[t];
gen_forward stl_deque_iterator[t];
fun deref : stl_deque_iterator[t] -> lvalue[t] = "*$1";
fun begin : stl_deque[t]-> stl_deque_iterator[t]= "$1.begin()";
fun end : stl_deque[t]-> stl_deque_iterator[t]= "$1.end()";
proc erase : stl_deque[t] * stl_deque_iterator[t] = "$1.erase($1);";
proc erase : stl_deque[t] * stl_deque_iterator[t] * stl_deque_iterator[t] = "$1.erase($1,$2);";
proc clear : stl_deque[t] = "$1.clear();";
proc pre_incr : lvalue[stl_deque_iterator[t]] = "++$1;";
proc post_incr : stl_deque_iterator[t] = "++$1;";
proc pre_decr : lvalue[stl_deque_iterator[t]] = "--$1;";
proc post_decr : stl_deque_iterator[t] = "--$1;";
type stl_deque_reverse_iterator = "std::deque<?1>::reverse_iterator";
fun rbegin : stl_deque[t]-> stl_deque_reverse_iterator[t]= "$1.rbegin()";
fun rend : stl_deque[t]-> stl_deque_reverse_iterator[t]= "$1.rend()";
fun deref : stl_deque_reverse_iterator[t] -> lvalue[t] = "*$1";
gen_cmp stl_deque_reverse_iterator[t];
proc pre_incr : lvalue[stl_deque_reverse_iterator[t]] = "++$1;";
proc post_incr : stl_deque_reverse_iterator[t] = "++$1;";
proc pre_decr: lvalue[stl_deque_reverse_iterator[t]] = "--$1;";
proc post_decr : stl_deque_reverse_iterator[t] = "--$1;";
proc insert: stl_deque[t] * stl_deque_iterator[t] * t = "$1.insert($2,$3);";
proc push_front : stl_deque[t] * t = "$1.push_front($2);";
proc push_back : stl_deque[t] * t = "$1.push_back($2);";
proc pop_front : stl_deque[t] = "$1.pop_back();";
fun front : stl_deque[t] -> t = "$1.front()";
fun front : stl_deque[t] -> t = "$1.front()";
fun subscript : lvalue[stl_deque[t]] * int -> lvalue[t] = "$1.at($2)";
fun subscript : stl_deque[t] * int -> t = "$1.at($2)";
}
module PriorityQueue[t]
{
requires std_stl_queue;
type stl_priorityqueue = "std::priorityqueue<?1>";
fun create : unit -> stl_priorityqueue[t] = "(GXX_PARSER_HACK std::priorityqueue<?1>())";
fun create : int * t -> stl_priorityqueue[t]= "(GXX_PARSER_HACK std::priorityqueue<?1>($1,$2))";
fun create[i] : i * i -> stl_priorityqueue[t] = "(GXX_PARSER_HACK std::priorityqueue<?1>($1,$2))";
gen_cmp stl_priorityqueue[t];
fun len: stl_priorityqueue[t] -> int = "$1.size()";
fun empty: stl_priorityqueue[t] -> int = "$1.empty()";
type stl_priorityqueue_iterator = "std::priorityqueue<?1>::iterator";
gen_cmp stl_priorityqueue_iterator[t];
gen_forward stl_priorityqueue_iterator[t];
fun deref : stl_priorityqueue_iterator[t] -> lvalue[t] = "*$1";
fun begin : stl_priorityqueue[t]-> stl_priorityqueue_iterator[t]= "$1.begin()";
fun end : stl_priorityqueue[t]-> stl_priorityqueue_iterator[t]= "$1.end()";
proc erase : stl_priorityqueue[t] * stl_priorityqueue_iterator[t] = "$1.erase($1);";
proc erase : stl_priorityqueue[t] * stl_priorityqueue_iterator[t] * stl_priorityqueue_iterator[t] = "$1.erase($1,$2);";
proc clear : stl_priorityqueue[t] = "$1.clear();";
proc pre_incr : lvalue[stl_priorityqueue_iterator[t]] = "++$1;";
proc post_incr : stl_priorityqueue_iterator[t] = "++$1;";
proc pre_decr : lvalue[stl_priorityqueue_iterator[t]] = "--$1;";
proc post_decr : stl_priorityqueue_iterator[t] = "--$1;";
}
module Stack[t]
{
requires std_stl_stack;
type stl_stack = "std::stack<?1>";
fun create : unit -> stl_stack[t] = "(GXX_PARSER_HACK std::stack<?1>())";
fun create : int * t -> stl_stack[t]= "(GXX_PARSER_HACK std::stack<?1>($1,$2))";
fun create[i] : i * i -> stl_stack[t] = "(GXX_PARSER_HACK std::stack<?1>($1,$2))";
gen_cmp stl_stack[t];
fun len: stl_stack[t] -> int = "$1.size()";
fun empty: stl_stack[t] -> int = "$1.empty()";
type stl_stack_iterator = "std::stack<?1>::iterator";
gen_cmp stl_stack_iterator[t];
gen_forward stl_stack_iterator[t];
fun deref : stl_stack_iterator[t] -> lvalue[t] = "*$1";
fun begin : stl_stack[t]-> stl_stack_iterator[t]= "$1.begin()";
fun end : stl_stack[t]-> stl_stack_iterator[t]= "$1.end()";
proc erase : stl_stack[t] * stl_stack_iterator[t] = "$1.erase($1);";
proc erase : stl_stack[t] * stl_stack_iterator[t] * stl_stack_iterator[t] = "$1.erase($1,$2);";
proc clear : stl_stack[t] = "$1.clear();";
proc pre_incr : lvalue[stl_stack_iterator[t]] = "++$1;";
proc post_incr : stl_stack_iterator[t] = "++$1;";
proc pre_decr : lvalue[stl_stack_iterator[t]] = "--$1;";
proc post_decr : stl_stack_iterator[t] = "--$1;";
}
module Set[t]
{
requires std_stl_set;
type stl_set = "std::set<?1>";
type stl_set_iterator = "std::set<?1>::iterator";
type stl_set_reverse_iterator = "std::set<?1>::reverse_iterator";
fun create : unit -> stl_set[t] = "(GXX_PARSER_HACK std::set<?1>())";
gen_cmp stl_set[t];
fun len: stl_set[t]->int = "$1.size()";
fun empty: stl_set[t]->int = "$1.empty()";
gen_cmp stl_set_iterator[t];
gen_cmp stl_set_reverse_iterator[t];
proc pre_incr : lvalue[stl_set_iterator[t]] = "++$1;";
proc post_incr : stl_set_iterator[t] = "++$1;";
proc pre_incr : lvalue[stl_set_reverse_iterator[t]] = "++$1;";
proc post_incr : stl_set_reverse_iterator[t] = "++$1;";
proc pre_decr : lvalue[stl_set_iterator[t]] = "--$1;";
proc post_decr : stl_set_iterator[t] = "--$1;";
proc pre_decr: lvalue[stl_set_reverse_iterator[t]] = "--$1;";
proc post_decr : stl_set_reverse_iterator[t] = "--$1;";
fun deref : stl_set_iterator[t] -> t = "*(#0*)&*$1:unary" is unary;
fun deref : stl_set_reverse_iterator[t] -> t = "*(#0*)&*$1:unary" is unary;
fun begin : stl_set[t]-> stl_set_iterator[t]= "$1.begin()";
fun end : stl_set[t]-> stl_set_iterator[t]= "$1.end()";
fun rbegin : stl_set[t]-> stl_set_reverse_iterator[t]= "$1.rbegin()";
fun rend : stl_set[t]-> stl_set_reverse_iterator[t]= "$1.rend()";
proc insert : stl_set[t] * t = "$1.insert($2);";
proc erase : stl_set[t] * stl_set_iterator[t] = "$1.erase($1);";
proc clear : stl_set[t] = "$1.clear();";
fun find : stl_set[t] * t -> stl_set_iterator[t] = "$1.find($2)";
fun mem : stl_set[t] * t -> bool = "$1.find($2) != $1.end()";
}
module MultiSet[t]
{
requires std_stl_set;
type stl_multiset = "std::multiset<?1>";
type stl_multiset_iterator = "std::multiset<?1>::iterator";
type stl_multiset_reverse_iterator = "std::multiset<?1>::reverse_iterator";
fun create : unit -> stl_multiset[t] = "(GXX_PARSER_HACK std::multiset<?1>())";
gen_cmp stl_multiset[t];
fun len: stl_multiset[t]->int = "$1.size()";
fun empty: stl_multiset[t]->int = "$1.empty()";
gen_cmp stl_multiset_iterator[t];
gen_cmp stl_multiset_reverse_iterator[t];
proc pre_incr : lvalue[stl_multiset_iterator[t]] = "++$1;";
proc post_incr : stl_multiset_iterator[t] = "++$1;";
proc pre_incr : lvalue[stl_multiset_reverse_iterator[t]] = "++$1;";
proc post_incr : stl_multiset_reverse_iterator[t] = "++$1;";
proc pre_decr : lvalue[stl_multiset_iterator[t]] = "--$1;";
proc post_decr : stl_multiset_iterator[t] = "--$1;";
proc pre_decr: lvalue[stl_multiset_reverse_iterator[t]] = "--$1;";
proc post_decr : stl_multiset_reverse_iterator[t] = "--$1;";
fun deref : stl_multiset_iterator[t] -> t = "*(#0*)&*$1:unary" is unary;
fun deref : stl_multiset_reverse_iterator[t] -> t = "*(#0*)&*$1:unary" is unary;
fun begin : stl_multiset[t]-> stl_multiset_iterator[t]= "$1.begin()";
fun end : stl_multiset[t]-> stl_multiset_iterator[t]= "$1.end()";
fun rbegin : stl_multiset[t]-> stl_multiset_reverse_iterator[t]= "$1.rbegin()";
fun rend : stl_multiset[t]-> stl_multiset_reverse_iterator[t]= "$1.rend()";
proc insert : stl_multiset[t] * t = "$1.insert($2);";
proc erase : stl_multiset[t] * stl_multiset_iterator[t] = "$1.erase($1);";
proc clear : stl_multiset[t] = "$1.clear();";
fun find : stl_multiset[t] * t -> stl_multiset_iterator[t] = "$1.find($2)";
fun mem : stl_multiset[t] * t -> bool = "$1.find($2) != $1.end()";
}
module Map[k,v]
{
requires std_stl_map;
type stl_map = "std::map<?1,?2>";
type stl_map_iterator = "std::map<?1,?2>::iterator";
type stl_map_reverse_iterator = "std::map<?1,?2>::reverse_iterator";
fun create : unit -> stl_map[k,v] = "(GXX_PARSER_HACK std::map<?1,?2>())";
gen_cmp stl_map[k,v];
fun len: stl_map[k,v]->int = "$1.size()";
fun empty: stl_map[k,v]->int = "$1.empty()";
gen_cmp stl_map_iterator[k,v];
gen_cmp stl_map_reverse_iterator[k,v];
proc pre_incr : stl_map_iterator[k,v] = "++$1;";
proc post_incr : stl_map_iterator[k,v] = "++$1;";
proc pre_incr : stl_map_reverse_iterator[k,v] = "++$1;";
proc post_incr : stl_map_reverse_iterator[k,v] = "++$1;";
proc pre_decr : stl_map_iterator[k,v] = "--$1;";
proc post_decr : stl_map_iterator[k,v] = "--$1;";
proc pre_decr : stl_map_reverse_iterator[k,v] = "--$1;";
proc post_decr : stl_map_reverse_iterator[k,v] = "--$1;";
fun deref : stl_map_iterator[k,v] -> k * lvalue[v] = "*(#0*)&*$1:unary" is unary;
fun begin : stl_map[k,v]-> stl_map_iterator[k,v]= "$1.begin()";
fun end : stl_map[k,v]-> stl_map_iterator[k,v]= "$1.end()";
fun deref : stl_map_reverse_iterator[k,v] -> k * lvalue[v] = "*(#0*)&*$1:unary" is unary;
fun rbegin : stl_map[k,v]-> stl_map_reverse_iterator[k,v]= "$1.rbegin()";
fun rend : stl_map[k,v]-> stl_map_reverse_iterator[k,v]= "$1.rend()";
proc insert : stl_map[k,v] * k * v = "$1.insert(std::make_pair($2,$3));";
proc erase : stl_map[k,v] * stl_map_iterator[k,v] = "$1.erase($1);";
proc clear : stl_map[k,v] = "$1.clear();";
fun find : stl_map[k,v] * k -> stl_map_iterator[k,v] = "$1.find($2)";
fun mem : stl_map[k,v] * k -> bool = "$1.find($2) != $1.end()";
fun subscript: stl_map[k,v] * k -> lvalue[v] = "$1[$2]";
}
module MultiMap[k,v]
{
requires std_stl_map;
type stl_multimap = "std::multimap<?1,?2>";
type stl_multimap_iterator = "std::multimap<?1,?2>::iterator";
type stl_multimap_reverse_iterator = "std::multimap<?1,?2>::reverse_iterator";
fun create : unit -> stl_multimap[k,v] = "(GXX_PARSER_HACK std::multimap<?1,?2>())";
gen_cmp stl_multimap[k,v];
fun len: stl_multimap[k,v]->int = "$1.size()";
fun empty: stl_multimap[k,v]->int = "$1.empty()";
gen_cmp stl_multimap_iterator[k,v];
gen_cmp stl_multimap_reverse_iterator[k,v];
proc pre_incr : stl_multimap_iterator[k,v] = "++$1;";
proc post_incr : stl_multimap_iterator[k,v] = "++$1;";
proc pre_incr : stl_multimap_reverse_iterator[k,v] = "++$1;";
proc post_incr : stl_multimap_reverse_iterator[k,v] = "++$1;";
proc pre_decr : stl_multimap_iterator[k,v] = "--$1;";
proc post_decr : stl_multimap_iterator[k,v] = "--$1;";
proc pre_decr : stl_multimap_reverse_iterator[k,v] = "--$1;";
proc post_decr : stl_multimap_reverse_iterator[k,v] = "--$1;";
fun deref : stl_multimap_iterator[k,v] -> k * lvalue[v] = "*(#0*)&*$1:unary" is unary;
fun begin : stl_multimap[k,v]-> stl_multimap_iterator[k,v]= "$1.begin()";
fun end : stl_multimap[k,v]-> stl_multimap_iterator[k,v]= "$1.end()";
fun deref : stl_multimap_reverse_iterator[k,v] -> k * lvalue[v] = "*(#0*)&*$1:unary" is unary;
fun rbegin : stl_multimap[k,v]-> stl_multimap_reverse_iterator[k,v]= "$1.rbegin()";
fun rend : stl_multimap[k,v]-> stl_multimap_reverse_iterator[k,v]= "$1.rend()";
proc insert : stl_multimap[k,v] * k * v = "$1.insert(std::make_pair($2,$3));";
proc erase : stl_multimap[k,v] * stl_multimap_iterator[k,v] = "$1.erase($1);";
proc clear : stl_multimap[k,v] = "$1.clear();";
fun find : stl_multimap[k,v] * k -> stl_multimap_iterator[k,v] = "$1.find($2)";
fun mem : stl_multimap[k,v] * k -> bool = "$1.find($2) != $1.end()";
fun subscript: stl_multimap[k,v] * k -> lvalue[v] = "$1[$2]";
}
module Slist[t]
{
requires ext_slist;
type stl_slist = "__gnu_cxx::slist<?1>";
fun create : unit -> stl_slist[t] = "(GXX_PARSER_HACK __gnu_cxx::slist<?1>())";
fun create : int * t -> stl_slist[t]= "(GXX_PARSER_HACK __gnu_cxx::slist<?1>($1,$2))";
fun create[i] : i * i -> stl_slist[t] = "(GXX_PARSER_HACK __gnu_cxx::slist<?1>($1,$2))";
gen_cmp stl_slist[t];
fun len: stl_slist[t] -> int = "$1.size()";
fun empty: stl_slist[t] -> int = "$1.empty()";
type stl_slist_iterator = "__gnu_cxx::slist<?1>::iterator";
gen_cmp stl_slist_iterator[t];
gen_forward stl_slist_iterator[t];
fun deref : stl_slist_iterator[t] -> lvalue[t] = "*$1";
fun begin : stl_slist[t]-> stl_slist_iterator[t]= "$1.begin()";
fun end : stl_slist[t]-> stl_slist_iterator[t]= "$1.end()";
proc erase : stl_slist[t] * stl_slist_iterator[t] = "$1.erase($1);";
proc erase : stl_slist[t] * stl_slist_iterator[t] * stl_slist_iterator[t] = "$1.erase($1,$2);";
proc clear : stl_slist[t] = "$1.clear();";
proc pre_incr : lvalue[stl_slist_iterator[t]] = "++$1;";
proc post_incr : stl_slist_iterator[t] = "++$1;";
proc pre_decr : lvalue[stl_slist_iterator[t]] = "--$1;";
proc post_decr : stl_slist_iterator[t] = "--$1;";
proc push_front : stl_slist[t] * t = "$1.push_front($2);";
fun front : stl_slist[t] -> t = "$1.front()";
proc pop_front : stl_slist[t] = "$1.pop_back();";
proc insert_after : stl_slist[t] * stl_slist_iterator[t] * t = "$1.insert_after($2,$3);";
proc erase_after : stl_slist[t] * stl_slist_iterator[t] = "$1.erase_after($1);";
}
// HASHTABLE based containers assume
// these classes will be added to C++ via TR1 in the future.
// g++ 3.2.2 at least has these classes
// The free SGI implementation may suffice as a replacement,
// this is what my version of g++ uses.
module HashSet[t]
{
requires ext_hash_set;
type stl_hash_set = "__gnu_cxx::hash_set<?1>";
type stl_hash_set_iterator = "__gnu_cxx::hash_set<?1>::iterator";
type stl_hash_set_reverse_iterator = "__gnu_cxx::hash_set<?1>::reverse_iterator";
fun create : unit -> stl_hash_set[t] = "(GXX_PARSER_HACK __gnu_cxx::hash_set<?1>())";
gen_cmp stl_hash_set[t];
fun len: stl_hash_set[t]->int = "$1.size()";
fun empty: stl_hash_set[t]->int = "$1.empty()";
gen_cmp stl_hash_set_iterator[t];
gen_cmp stl_hash_set_reverse_iterator[t];
proc pre_incr : lvalue[stl_hash_set_iterator[t]] = "++$1;";
proc post_incr : stl_hash_set_iterator[t] = "++$1;";
proc pre_incr : lvalue[stl_hash_set_reverse_iterator[t]] = "++$1;";
proc post_incr : stl_hash_set_reverse_iterator[t] = "++$1;";
proc pre_decr : lvalue[stl_hash_set_iterator[t]] = "--$1;";
proc post_decr : stl_hash_set_iterator[t] = "--$1;";
proc pre_decr: lvalue[stl_hash_set_reverse_iterator[t]] = "--$1;";
proc post_decr : stl_hash_set_reverse_iterator[t] = "--$1;";
fun deref : stl_hash_set_iterator[t] -> t = "*(#0*)&*$1:unary" is unary;
fun deref : stl_hash_set_reverse_iterator[t] -> t = "*(#0*)&*$1:unary" is unary;
fun begin : stl_hash_set[t]-> stl_hash_set_iterator[t]= "$1.begin()";
fun end : stl_hash_set[t]-> stl_hash_set_iterator[t]= "$1.end()";
fun rbegin : stl_hash_set[t]-> stl_hash_set_reverse_iterator[t]= "$1.rbegin()";
fun rend : stl_hash_set[t]-> stl_hash_set_reverse_iterator[t]= "$1.rend()";
proc insert : stl_hash_set[t] * t = "$1.insert($2);";
proc erase : stl_hash_set[t] * stl_hash_set_iterator[t] = "$1.erase($1);";
proc clear : stl_hash_set[t] = "$1.clear();";
fun find : stl_hash_set[t] * t -> stl_hash_set_iterator[t] = "$1.find($2)";
fun mem : stl_hash_set[t] * t -> bool = "$1.find($2) != $1.end()";
}
module HashMultiSet[t]
{
requires ext_hash_set;
type stl_hash_multiset = "__gnu_cxx::hash_multiset<?1>";
fun create : unit -> stl_hash_multiset[t] = "(GXX_PARSER_HACK __gnu_cxx::hash_multiset<?1>())";
fun create : int * t -> stl_hash_multiset[t]= "(GXX_PARSER_HACK __gnu_cxx::hash_multiset<?1>($1,$2))";
fun create[i] : i * i -> stl_hash_multiset[t] = "(GXX_PARSER_HACK __gnu_cxx::hash_multiset<?1>($1,$2))";
gen_cmp stl_hash_multiset[t];
fun len: stl_hash_multiset[t] -> int = "$1.size()";
fun empty: stl_hash_multiset[t] -> int = "$1.empty()";
type stl_hash_multiset_iterator = "__gnu_cxx::hash_multiset<?1>::iterator";
gen_cmp stl_hash_multiset_iterator[t];
gen_forward stl_hash_multiset_iterator[t];
fun deref : stl_hash_multiset_iterator[t] -> lvalue[t] = "*$1";
fun begin : stl_hash_multiset[t]-> stl_hash_multiset_iterator[t]= "$1.begin()";
fun end : stl_hash_multiset[t]-> stl_hash_multiset_iterator[t]= "$1.end()";
proc erase : stl_hash_multiset[t] * stl_hash_multiset_iterator[t] = "$1.erase($1);";
proc erase : stl_hash_multiset[t] * stl_hash_multiset_iterator[t] * stl_hash_multiset_iterator[t] = "$1.erase($1,$2);";
proc clear : stl_hash_multiset[t] = "$1.clear();";
proc pre_incr : lvalue[stl_hash_multiset_iterator[t]] = "++$1;";
proc post_incr : stl_hash_multiset_iterator[t] = "++$1;";
proc pre_decr : lvalue[stl_hash_multiset_iterator[t]] = "--$1;";
proc post_decr : stl_hash_multiset_iterator[t] = "--$1;";
}
module HashMap[k,v]
{
requires ext_hash_map;
type stl_hash_map = "__gnu_cxx::hash_map<?1,?2>";
type stl_hash_map_iterator = "__gnu_cxx::hash_map<?1,?2>::iterator";
type stl_hash_map_reverse_iterator = "__gnu_cxx::hash_map<?1,?2>::reverse_iterator";
fun create : unit -> stl_hash_map[k,v] = "(GXX_PARSER_HACK __gnu_cxx::hash_map<?1,?2>())";
gen_cmp stl_hash_map[k,v];
fun len: stl_hash_map[k,v]->int = "$1.size()";
fun empty: stl_hash_map[k,v]->int = "$1.empty()";
gen_cmp stl_hash_map_iterator[k,v];
gen_cmp stl_hash_map_reverse_iterator[k,v];
proc pre_incr : stl_hash_map_iterator[k,v] = "++$1;";
proc post_incr : stl_hash_map_iterator[k,v] = "++$1;";
proc pre_incr : stl_hash_map_reverse_iterator[k,v] = "++$1;";
proc post_incr : stl_hash_map_reverse_iterator[k,v] = "++$1;";
proc pre_decr : stl_hash_map_iterator[k,v] = "--$1;";
proc post_decr : stl_hash_map_iterator[k,v] = "--$1;";
proc pre_decr : stl_hash_map_reverse_iterator[k,v] = "--$1;";
proc post_decr : stl_hash_map_reverse_iterator[k,v] = "--$1;";
fun deref : stl_hash_map_iterator[k,v] -> k * lvalue[v] = "*(#0*)&*$1:unary" is unary;
fun begin : stl_hash_map[k,v]-> stl_hash_map_iterator[k,v]= "$1.begin()";
fun end : stl_hash_map[k,v]-> stl_hash_map_iterator[k,v]= "$1.end()";
fun deref : stl_hash_map_reverse_iterator[k,v] -> k * lvalue[v] = "*(#0*)&*$1:unary" is unary;
fun rbegin : stl_hash_map[k,v]-> stl_hash_map_reverse_iterator[k,v]= "$1.rbegin()";
fun rend : stl_hash_map[k,v]-> stl_hash_map_reverse_iterator[k,v]= "$1.rend()";
proc insert : stl_hash_map[k,v] * k * v = "$1.insert(std::make_pair($2,$3));";
proc erase : stl_hash_map[k,v] * stl_hash_map_iterator[k,v] = "$1.erase($1);";
proc clear : stl_hash_map[k,v] = "$1.clear();";
fun find : stl_hash_map[k,v] * k -> stl_hash_map_iterator[k,v] = "$1.find($2)";
fun mem : stl_hash_map[k,v] * k -> bool = "$1.find($2) != $1.end()";
fun subscript: stl_hash_map[k,v] * k -> lvalue[v] = "$1[$2]";
}
module HashMultiMap[k,v]
{
requires ext_hash_map;
type stl_hash_multimap = "__gnu_cxx::hash_multimap<?1,?2>";
type stl_hash_multimap_iterator = "__gnu_cxx::hash_multimap<?1,?2>::iterator";
type stl_hash_multimap_reverse_iterator = "__gnu_cxx::hash_multimap<?1,?2>::reverse_iterator";
fun create : unit -> stl_hash_multimap[k,v] = "(GXX_PARSER_HACK __gnu_cxx::hash_multimap<?1,?2>())";
gen_cmp stl_hash_multimap[k,v];
fun len: stl_hash_multimap[k,v]->int = "$1.size()";
fun empty: stl_hash_multimap[k,v]->int = "$1.empty()";
gen_cmp stl_hash_multimap_iterator[k,v];
gen_cmp stl_hash_multimap_reverse_iterator[k,v];
proc pre_incr : stl_hash_multimap_iterator[k,v] = "++$1;";
proc post_incr : stl_hash_multimap_iterator[k,v] = "++$1;";
proc pre_incr : stl_hash_multimap_reverse_iterator[k,v] = "++$1;";
proc post_incr : stl_hash_multimap_reverse_iterator[k,v] = "++$1;";
proc pre_decr : stl_hash_multimap_iterator[k,v] = "--$1;";
proc post_decr : stl_hash_multimap_iterator[k,v] = "--$1;";
proc pre_decr : stl_hash_multimap_reverse_iterator[k,v] = "--$1;";
proc post_decr : stl_hash_multimap_reverse_iterator[k,v] = "--$1;";
fun deref : stl_hash_multimap_iterator[k,v] -> k * lvalue[v] = "*(#0*)&*$1:unary" is unary;
fun begin : stl_hash_multimap[k,v]-> stl_hash_multimap_iterator[k,v]= "$1.begin()";
fun end : stl_hash_multimap[k,v]-> stl_hash_multimap_iterator[k,v]= "$1.end()";
fun deref : stl_hash_multimap_reverse_iterator[k,v] -> k * lvalue[v] = "*(#0*)&*$1:unary" is unary;
fun rbegin : stl_hash_multimap[k,v]-> stl_hash_multimap_reverse_iterator[k,v]= "$1.rbegin()";
fun rend : stl_hash_multimap[k,v]-> stl_hash_multimap_reverse_iterator[k,v]= "$1.rend()";
proc insert : stl_hash_multimap[k,v] * k * v = "$1.insert(std::make_pair($2,$3));";
proc erase : stl_hash_multimap[k,v] * stl_hash_multimap_iterator[k,v] = "$1.erase($1);";
proc clear : stl_hash_multimap[k,v] = "$1.clear();";
fun find : stl_hash_multimap[k,v] * k -> stl_hash_multimap_iterator[k,v] = "$1.find($2)";
fun mem : stl_hash_multimap[k,v] * k -> bool = "$1.find($2) != $1.end()";
fun subscript: stl_hash_multimap[k,v] * k -> lvalue[v] = "$1[$2]";
}
}
