working on testing

doc/examples/sht/delmap_test.ivy

@@ -12,8 +12,9 @@ export dmap.get
 
 object impl = {
     interpret id -> bv[1]
+    interpret key.t -> bv[4]
 }
 
 isolate iso_dmap = dmap with key
 extract iso_impl = dmap, key, impl
-
+trusted isolate iso_test = dmap with key,impl

doc/examples/sht/key.ivy

@@ -5,12 +5,14 @@ include order
 object key = {
     
     type t
-    instance props : totally_ordered_with_zero(t)
     instance iter : order_iterator(this)
 
-    object impl = {
-	interpret t -> bv[16]
+    object spec  = {
+	instantiate totally_ordered_with_zero(t)
     }
-    isolate iso = iter,props with impl
+
+    object impl = {
+    }
+
 }
 

doc/examples/sht/sht.ivy

@@ -22,6 +22,7 @@ instance udp : udp_simple(id,trans.net_msg.t)
 isolate iso_p = proto with ref,trans,key,shard
 isolate iso_dm(me:id) = proto.impl.dm(me) with key
 isolate iso_hash(me:id) = proto.impl.hash(me) with key,shard
+isolate iso_key = key with impl
 
 export proto.set
 export proto.get
@@ -30,6 +31,7 @@ import proto.answer
 
 object impl = {
     interpret id -> bv[1]
+    interpret key.t -> bv[16]
 }
 
 object debug = {

doc/examples/sht/table_test.ivy

@@ -10,7 +10,8 @@ instance shard : table_shard(key,value)
 instance tab : hash_table(key,value,shard)
 
 object impl = {
-    interpret value -> bv[16]
+    interpret value -> bv[4]
+    interpret key.t -> bv[4]
 }
 
 export tab.set
@@ -22,5 +23,6 @@ isolate iso_tab = tab with tab,shard,key
 isolate iso_key = key
 
 
-extract iso_impl = tab,shard,key
+extract iso_impl = tab,shard,key,impl
 
+trusted isolate iso_test = tab with shard,key,impl

ivy/include/collections.ivy

@@ -462,8 +462,10 @@ module map_wrapper(key,value) = {
 
     implement erase(lo:key.iter.t,hi:key.iter.t) {
 	<<<
+
             `s`.erase(`lo`.is_end ? `s`.end() : `s`.lower_bound(`lo`.val),
- 	              `hi`.is_end ? `s`.end() : `s`.upper_bound(`hi`.val));
+ 	              `hi`.is_end ? `s`.end() : `s`.lower_bound(`hi`.val));
+
 	>>>
     }
 
@@ -521,6 +523,16 @@ module map_wrapper(key,value) = {
 	    }
 	>>>
     }
+
+    action show = {
+	<<<
+            std::cout << "{";
+	    for(std::map<`key.t`,`value`>::iterator __it = `s`.begin(), __en = `s`.end(); __it != __en; ++__it)
+	        std::cout << __it->first << ":" << __it->second << ",";
+            std::cout << "}" << std::endl;
+	>>>
+
+    }
 }
 
 ################################################################################

ivy/include/order.ivy

@@ -65,8 +65,6 @@ module order_iterator(range) = {
 	val : range.t
     }
 
-    instantiate totally_ordered(range.t)
-
     definition (X < Y) = ~is_end(X) & is_end(Y) 
                       | ~is_end(X) & ~is_end(Y) & val(X) < val(Y)
 
@@ -78,6 +76,9 @@ module order_iterator(range) = {
     action end returns (y:t)
     
     object spec = {
+
+	instantiate totally_ordered(range.t)
+
 	after create {
 	    assert ~is_end(y);
 	    assert val(y) = x

ivy/ivy_compiler.py

@@ -486,6 +486,9 @@ class IvyDomainSetup(IvyDeclInterp):
         self.add_definition(ldf.clone([label,df]))
         self.domain.updates.append(DerivedUpdate(df))
         self.domain.symbol_order.append(df.args[0].rep)
+        if not self.domain.sig.contains_symbol(df.args[0].rep):
+            add_symbol(df.args[0].rep.name,df.args[0].rep.sort)
+            
     def progress(self,df):
         rel = df.args[0]
         with ASTContext(rel):

ivy/ivy_isolate.py

@@ -25,6 +25,7 @@ create_imports = iu.BooleanParameter("create_imports",False)
 enforce_axioms = iu.BooleanParameter("enforce_axioms",False)
 do_check_interference = iu.BooleanParameter("interference",True)
 pedantic = iu.BooleanParameter("pedantic",False)
+opt_prefer_impls = iu.BooleanParameter("prefer_impls",False)
 
 def lookup_action(ast,mod,name):
     if name not in mod.actions:
@@ -565,7 +566,19 @@ def get_prop_dependencies(mod):
             res.append((prop,ds))
     return res
 
+def set_privates_prefer(mod,isolate,preferred):
+    verified = set(a.relname for a in (isolate.verified()))
+    suff = "impl" if preferred == "spec" else "spec"
+    mod.privates = set(mod.privates)
+    for n,l in mod.hierarchy.iteritems():
+        if n not in verified:
+            if suff in l and preferred in l:
+                mod.privates.add(n+iu.ivy_compose_character+suff)
+
 def set_privates(mod,isolate,suff=None):
+    if suff == None and opt_prefer_impls.get():
+        set_privates_prefer(mod,isolate,"impl")
+        return
     suff = suff or ("spec" if isinstance(isolate,ivy_ast.ExtractDef) else "impl")
     mod.privates = set(mod.privates)
     for n,l in mod.hierarchy.iteritems():

ivy/ivy_to_cpp.py

@@ -264,14 +264,16 @@ def ctypefull(sort,classname=None):
 def native_type_full(self):
     return self.args[0].inst(native_reference,self.args[1:])    
 
+large_thresh = 1024
+
 def is_large_type(sort):
     cards = map(sort_card,sort.dom if hasattr(sort,'dom') else [])
-    return not(all(cards) and reduce(mul,cards,1) <= 16)
+    return not(all(cards) and reduce(mul,cards,1) <= large_thresh)
 
 def ctype_function(sort,classname=None,skip_params=0):
     cards = map(sort_card,sort.dom[skip_params:] if hasattr(sort,'dom') else [])
     cty = ctypefull(sort.rng,classname)
-    if all(cards) and reduce(mul,cards,1) <= 16:
+    if all(cards) and reduce(mul,cards,1) <= large_thresh:
         return (cty,cards)
     cty = 'hash_thunk<'+ctuple(sort.dom,classname=classname)+','+cty+'>'
     return (cty,[])
@@ -510,7 +512,7 @@ def sym_is_member(sym):
 
 def emit_eval_sig(header,obj=None,used=None,classname=None):
     for symbol in all_state_symbols():
-        if slv.solver_name(symbol) != None: # skip interpreted symbols
+        if slv.solver_name(symbol) != None and symbol.name not in im.module.destructor_sorts: # skip interpreted symbols
             global is_derived
             if symbol not in is_derived:
                 if used == None or symbol in used:
@@ -1675,7 +1677,7 @@ def check_representable(sym,ast=None,skip_args=0):
             card = sort_card(domsort)
             if card == None:
                 raise iu.IvyError(ast,'cannot compile "{}" because type {} is uninterpreted'.format(sym,domsort))
-            if card > 16:
+            if card > large_thresh:
                 raise iu.IvyError(ast,'cannot compile "{}" because type {} is large'.format(sym,domsort))
 
 def cstr(term):
@@ -1932,7 +1934,14 @@ def new_temp(header,sort=None):
     return name
 
 
+def find_definition(sym):
+    for ldf in im.module.definitions:
+        if ldf.formula.defines() == sym:
+            return ldf
+    return None
+
 def get_bound_exprs(v0,variables,body,exists,res):
+    global is_derived
     if isinstance(body,il.Not):
         return get_bound_exprs(v0,variables,body.args[0],not exists,res)
     if il.is_app(body) and body.rep.name in ['<','<=','>','>=']:
@@ -1949,6 +1958,15 @@ def get_bound_exprs(v0,variables,body,exists,res):
         for arg in body.args:
             get_bound_exprs(v0,variables,arg,exists,res)
         return
+    if il.is_app(body) and body.rep in is_derived and v0 in body.args:
+        iu.dbg('body')
+        ldf = find_definition(body.rep)
+        if all(il.is_variable(v) for v in ldf.formula.args[0].args):
+            subst = dict((v.name,a) for v,a in zip(ldf.formula.args[0].args,body.args))
+            iu.dbg('subst')
+            thing = ilu.substitute_ast(ldf.formula.args[1],subst)
+            iu.dbg('thing')
+            get_bound_exprs(v0,variables,thing,exists,res)
     
 def sort_has_negative_values(sort):
     return sort.name in il.sig.interp and il.sig.interp[sort.name] == 'int'
@@ -3096,6 +3114,8 @@ public:
 //        z3::sort sort = ctx.uninterpreted_sort(sort_name);
         // can't use operator[] here because the value classes don't have nullary constructors
         enum_sorts.insert(std::pair<std::string, z3::sort>(sort_name,sort));
+        sort_names.push_back(symb);
+        sorts.push_back(sort);
     }
 
     void mk_decl(const char *decl_name, unsigned arity, const char **domain_names, const char *range_name) {