sht table is tested

examples/sht/shard.ivy

@@ -34,6 +34,16 @@ module table_shard(key,data) = {
 	definition value(S,X) = second(S,find(S,X)) if present(S,X) else 0
 
 	conjecture at(S,X,Y) & at(S,X,Z) -> Y = Z
-    }
 
+	implement iter.next(x:iter.t) returns (y:iter.t) {
+	    if iter.iter_val(x) = 3 {
+		iter.iter_end(y) := true;
+		iter.iter_val(y) := 0
+	    }
+	    else {
+		iter.iter_end(y) := false;
+		iter.iter_val(y) := iter.iter_val(x) + 1
+	    }
+	}
+    }
 }

examples/sht/table.ivy

@@ -62,10 +62,11 @@ module hash_table(key,value,shard) = {
 
 	implement extract_ {
 	    shard.second(res,X) := 0;
-	    local idx : key.iter.t, pos : shard.iter.t {
+	    local idx : key.iter.t, pos : shard.iter.t, lim: key.iter.t  {
 		idx := tab.begin(lo);
+		lim := key.iter.begin(hi);
 		pos := shard.iter.begin(0);
-		while ~shard.iter.iter_end(pos) & ~key.iter.iter_end(idx)
+		while ~shard.iter.iter_end(pos) & idx <= lim
 #		    invariant pos <= X -> shard.value(res,X) = 0
 #                    invariant lo <= X & X < idx -> shard.value(res,X) = tab.get(X)  
 		{
@@ -90,7 +91,7 @@ module hash_table(key,value,shard) = {
 		call tab.erase(lo,hi);
 		local idx : key.iter.t, pos : shard.iter.t {
 		    pos := shard.iter.begin(0);
-		    while shard.iter.iter_end(pos)
+		    while ~shard.iter.iter_end(pos)
 #                        invariant lo <= X & X <= hi & shard.find(s,X) < pos
 #                                  -> shard.value(res,X) = tab.get(X)  
 		    {
@@ -99,7 +100,8 @@ module hash_table(key,value,shard) = {
 			    if shard.second(s,r) ~= 0 {
 				call tab.set(shard.first(s,r),shard.second(s,r))
 			    }
-			}			
+			};			
+			pos := shard.iter.next(pos)
 		    }
 		}
 	    }

ivy/include/order.ivy

@@ -24,7 +24,8 @@ module order_iterator(range) = {
     
     object spec = {
 	after begin {
-	    assert ~iter_end(y) & iter_val(y) = x
+	    iter_end(y) := false;
+	    iter_val(y) := x
 	}
 	after end {
 	    iter_end(y) := true;

ivy/ivy_to_cpp.py

@@ -909,7 +909,17 @@ void install_timer(timer *);
             for idx,sym in enumerate(destrs):
                 if idx > 0:
                     code_line(impl,'s<<","')
-                code_line(impl,'s<< "' + memname(sym) + ':" <<  t.'+memname(sym))
+                code_line(impl,'s<< "' + memname(sym) + ':"')
+                dom = sym.sort.dom[1:]
+                vs = variables(dom)
+                for d,v in zip(dom,vs):
+                    code_line(impl,'s << "["')
+                    open_loop(impl,[v])
+                    code_line(impl,'if ({}) s << ","'.format(varname(v)))
+                code_line(impl,'s << t.' + memname(sym) + subscripts(vs))
+                for d,v in zip(dom,vs):
+                    close_loop(impl,[v])
+                    code_line(impl,'s << "]"')
             code_line(impl,'s<<"}"')
             code_line(impl,'return s')
             close_scope(impl)
@@ -974,6 +984,9 @@ def check_representable(sym,ast=None,skip_args=0):
 
 cstr = il.fmla_to_str_ambiguous
 
+def subscripts(vs):
+    return ''.join('['+varname(v)+']' for v in vs)
+
 def variables(sorts):
     return [il.Variable('X__'+str(idx),s) for idx,s in enumerate(sorts)]