working on destructors

ivy/ivy_actions.py

@@ -327,19 +327,45 @@ class AssignAction(Action):
 #            print "rhs: %s: %s" % (rhs,type(rhs))
             raise IvyError(self,"sort mismatch in assignment to {}".format(lhs.rep))
 
-        new_n = new(n)
-        args = lhs.args
-        dlhs = new_n(*sym_placeholders(n))
-        vs = dlhs.args
-        eqs = [eq_atom(v,a) for (v,a) in zip(vs,args) if not isinstance(a,Variable)]
-        rn = dict((a.rep,v) for v,a in zip(vs,args) if isinstance(a,Variable))
-        drhs = substitute_ast(rhs,rn)
-        if eqs:
-            drhs = Ite(And(*eqs),drhs,n(*dlhs.args))
-        new_clauses = Clauses([],[Definition(dlhs,drhs)])
+        # For a destructor assignment, we actually mutate the first argument
+
+        if n.name in ivy_module.module.destructor_sorts:
+            mut = lhs.args[0]
+            rest = list(lhs.args[1:])
+            mut_n = mut.rep
+            nondet = mut_n.suffix("_nd").skolem()
+            new_clauses = mk_assign_clauses(mut_n,nondet(*sym_placeholders(mut_n)))
+            fmlas = []
+            nondet_lhs = lhs.rep(*([nondet(*mut.args)]+rest))
+            fmlas.append(equiv_ast(nondet_lhs,rhs))
+            vs = sym_placeholders(n)
+            dlhs = n(*([nondet(*mut.args)] + vs[1:]))
+            drhs = n(*([mut] + vs[1:]))
+            eqs = [eq_atom(v,a) for (v,a) in zip(vs,lhs.args)[1:] if not isinstance(a,Variable)]
+            if eqs:
+                fmlas.append(Or(And(*eqs),equiv_ast(dlhs,drhs)))
+            new_clauses = and_clauses(new_clauses,Clauses(fmlas))
+            dbg('new_clauses')
+            return ([mut_n], new_clauses, false_clauses())
+
+        new_clauses = mk_assign_clauses(lhs,rhs)
 #        print "assign new_clauses = {}".format(new_clauses)
         return ([n], new_clauses, false_clauses())
 
+def mk_assign_clauses(lhs,rhs):
+    n = lhs.rep
+    new_n = new(n)
+    args = lhs.args
+    dlhs = new_n(*sym_placeholders(n))
+    vs = dlhs.args
+    eqs = [eq_atom(v,a) for (v,a) in zip(vs,args) if not isinstance(a,Variable)]
+    rn = dict((a.rep,v) for v,a in zip(vs,args) if isinstance(a,Variable))
+    drhs = substitute_ast(rhs,rn)
+    if eqs:
+        drhs = Ite(And(*eqs),drhs,n(*dlhs.args))
+    new_clauses = Clauses([],[Definition(dlhs,drhs)])
+    return new_clauses
+
 
 def sign(polarity,atom):
     return atom if polarity else Not(atom)

ivy/ivy_ast.py

@@ -434,6 +434,10 @@ class ConstantDecl(Decl):
     def defines(self):
         return [(c.rep,lineno(c)) for c in self.args if c.rep not in iu.polymorphic_symbols]
 
+class DestructorDecl(ConstantDecl):
+    def name(self):
+        return 'destructor'
+
 class DerivedDecl(Decl):
     def name(self):
         return 'derived'

ivy/ivy_compiler.py

@@ -324,6 +324,14 @@ class IvyDomainSetup(IvyDeclInterp):
         sym = compile_const(v,self.domain.sig)
 #        print "sym: {!r}".format(sym)
         self.domain.functions[sym] = len(v.args)
+        return sym
+    def destructor(self,v):
+        sym = self.individual(v)
+        dom = sym.sort.dom
+        if not dom:
+            raise IvyError(v,"A destructor must have at least one parameter")
+        self.domain.destructor_sorts[sym.name] = dom[0]
+        self.domain.sort_destructors[dom[0].name].append(sym)
     def derived(self,df):
         try:
             rel = df.args[0]

ivy/ivy_lexer.py

@@ -93,6 +93,7 @@ reserved = all_reserved = {
    'rely' : 'RELY',
    'mixord' : 'MIXORD',
    'extract' : 'EXTRACT',
+   'destructor' : 'DESTRUCTOR'
 }
 
 tokens += tuple(all_reserved.values())
@@ -175,7 +176,7 @@ class LexerVersion(object):
                 if s in reserved:
                     del reserved[s]
         if self.version <= [1,4]:
-            for s in ['function','class','object','method','execute']:
+            for s in ['function','class','object','method','execute','destructor']:
 #                print "deleting {}".format(s)
                 if s in reserved:
                     del reserved[s]

ivy/ivy_module.py

@@ -49,6 +49,8 @@ class Module(object):
         self.progress = []  # list of progress properties
         self.rely = [] # list of rely relations
         self.mixord = [] # list of mixin order relations
+        self.destructor_sorts = {}
+        self.sort_destructors = defaultdict(list)
 
         self.sig = il.sig.copy() # capture the current signature
 

ivy/ivy_parser.py

@@ -299,6 +299,10 @@ def p_symdecl_constantdecl(p):
     'symdecl : constantdecl'
     p[0] = p[1]
 
+def p_symdecl_destructor_tterms(p):
+    'symdecl : DESTRUCTOR tterms'
+    p[0] = DestructorDecl(*p[2])
+
 def p_constantdecl_constant_tterms(p):
     'constantdecl : INDIV tterms'
     p[0] = ConstantDecl(*p[2])

test/destructor1.py

@@ -0,0 +1,42 @@
+
+from ivy import ivy_module as im
+from ivy.ivy_compiler import ivy_from_string
+from ivy.tk_ui import new_ui
+from ivy import ivy_utils as iu
+
+prog = """#lang ivy1.5
+
+type foo
+type bar
+
+destructor f(X:foo) : bar
+
+individual x:foo,y:bar
+
+action a = {
+    f(x) := y
+}
+
+"""
+
+with im.Module():
+    iu.set_parameters({'ui':'cti','ext':'ext'})
+    main_ui = new_ui()
+    ui = main_ui.add(ivy_from_string(prog))
+#     main_ui.answer("OK")
+#     ui.check_inductiveness()
+# #    ui = ui.cti
+#     cg = ui.current_concept_graph
+#     cg.show_relation(cg.relation('link(X,Y)'),'+')
+#     cg.gather()
+#     main_ui.answer("OK")
+#     cg.strengthen()
+#     main_ui.answer("OK")
+#     ui.check_inductiveness()
+# #    cg.show_relation(cg.relation('semaphore'),'+')
+#     cg.gather()
+#     main_ui.answer("View")
+#     cg.bmc_conjecture(bound=1)
+# #    main_ui.mainloop()
+
+