implement visit_ESingleton for Java/CxxPrinter

[izgzhen]

$ cat examples/agg.ds # I modified it as below
Aggr:

    state l : Set<Int>

    query oldest()
        assume exists l;
        argmax {x -> x} l

    op add(x: Int)
        assume not(x in l);
        l.add(x);

    op remove(x: Int)
        l.remove(x);
$ python -m cozy examples/agg.ds --java Agg.java
....
Code generation failed!
Implementation was dumped to /tmp/failed_codegen.py
Traceback (most recent call last):
  File "/usr/lib/python3.6/runpy.py", line 193, in _run_module_as_main
    "__main__", mod_spec)
  File "/usr/lib/python3.6/runpy.py", line 85, in _run_code
    exec(code, run_globals)
  File "/home/zgzhen/repos/cozy/cozy/__main__.py", line 2, in <module>
    run()
  File "/home/zgzhen/repos/cozy/cozy/main.py", line 173, in run
    codegen.JavaPrinter(out=out, boxed=(not args.unboxed)).visit(impl, state_map, share_info, abstract_state=ast.spec.statevars)
  File "/home/zgzhen/repos/cozy/cozy/codegen/java.py", line 682, in visit
    res = super().visit(x, *args, **kwargs)
  File "/home/zgzhen/repos/cozy/cozy/common.py", line 281, in visit
    return f(x, *args, **kwargs)
  File "/home/zgzhen/repos/cozy/cozy/codegen/java.py", line 87, in visit_Spec
    self.visit(op)
  File "/home/zgzhen/repos/cozy/cozy/codegen/java.py", line 682, in visit
    res = super().visit(x, *args, **kwargs)
  File "/home/zgzhen/repos/cozy/cozy/common.py", line 281, in visit
    return f(x, *args, **kwargs)
  File "/home/zgzhen/repos/cozy/cozy/codegen/java.py", line 106, in visit_Op
    self.visit(q.body)
  File "/home/zgzhen/repos/cozy/cozy/codegen/java.py", line 682, in visit
    res = super().visit(x, *args, **kwargs)
  File "/home/zgzhen/repos/cozy/cozy/common.py", line 281, in visit
    return f(x, *args, **kwargs)
  File "/home/zgzhen/repos/cozy/cozy/codegen/cxx.py", line 817, in visit_SSeq
    self.visit(ss)
  File "/home/zgzhen/repos/cozy/cozy/codegen/java.py", line 682, in visit
    res = super().visit(x, *args, **kwargs)
  File "/home/zgzhen/repos/cozy/cozy/common.py", line 281, in visit
    return f(x, *args, **kwargs)
  File "/home/zgzhen/repos/cozy/cozy/codegen/cxx.py", line 813, in visit_SDecl
    return self.declare(s.var.with_type(t), s.val)
  File "/home/zgzhen/repos/cozy/cozy/codegen/cxx.py", line 795, in declare
    iv = self.visit(initial_value)
  File "/home/zgzhen/repos/cozy/cozy/codegen/java.py", line 682, in visit
    res = super().visit(x, *args, **kwargs)
  File "/home/zgzhen/repos/cozy/cozy/common.py", line 281, in visit
    return f(x, *args, **kwargs)
  File "/home/zgzhen/repos/cozy/cozy/codegen/cxx.py", line 478, in visit_EBinOp
    return self.visit(ENot(EEq(e.e1, e.e2)))
  File "/home/zgzhen/repos/cozy/cozy/codegen/java.py", line 682, in visit
    res = super().visit(x, *args, **kwargs)
  File "/home/zgzhen/repos/cozy/cozy/common.py", line 281, in visit
    return f(x, *args, **kwargs)
  File "/home/zgzhen/repos/cozy/cozy/codegen/cxx.py", line 690, in visit_EUnaryOp
    ee = self.visit(e.e)
  File "/home/zgzhen/repos/cozy/cozy/codegen/java.py", line 682, in visit
    res = super().visit(x, *args, **kwargs)
  File "/home/zgzhen/repos/cozy/cozy/common.py", line 281, in visit
    return f(x, *args, **kwargs)
  File "/home/zgzhen/repos/cozy/cozy/codegen/cxx.py", line 473, in visit_EBinOp
    return self._eq(e.e1, e.e2)
  File "/home/zgzhen/repos/cozy/cozy/codegen/java.py", line 235, in _eq
    return self.visit(EEscape("java.util.Objects.equals({e1}, {e2})", ["e1", "e2"], [e1, e2]).with_type(BOOL))
  File "/home/zgzhen/repos/cozy/cozy/codegen/java.py", line 682, in visit
    res = super().visit(x, *args, **kwargs)
  File "/home/zgzhen/repos/cozy/cozy/common.py", line 281, in visit
    return f(x, *args, **kwargs)
  File "/home/zgzhen/repos/cozy/cozy/codegen/cxx.py", line 775, in visit_EEscape
    args = [self.visit(arg) for arg in args]
  File "/home/zgzhen/repos/cozy/cozy/codegen/cxx.py", line 775, in <listcomp>
    args = [self.visit(arg) for arg in args]
  File "/home/zgzhen/repos/cozy/cozy/codegen/java.py", line 682, in visit
    res = super().visit(x, *args, **kwargs)
  File "/home/zgzhen/repos/cozy/cozy/common.py", line 281, in visit
    return f(x, *args, **kwargs)
  File "/home/zgzhen/repos/cozy/cozy/codegen/cxx.py", line 473, in visit_EBinOp
    return self._eq(e.e1, e.e2)
  File "/home/zgzhen/repos/cozy/cozy/codegen/java.py", line 236, in _eq
    return super()._eq(e1, e2)
  File "/home/zgzhen/repos/cozy/cozy/codegen/cxx.py", line 466, in _eq
    return self.visit(EEscape("({e1} == {e2})", ["e1", "e2"], [e1, e2]).with_type(BOOL))
  File "/home/zgzhen/repos/cozy/cozy/codegen/java.py", line 682, in visit
    res = super().visit(x, *args, **kwargs)
  File "/home/zgzhen/repos/cozy/cozy/common.py", line 281, in visit
    return f(x, *args, **kwargs)
  File "/home/zgzhen/repos/cozy/cozy/codegen/cxx.py", line 775, in visit_EEscape
    args = [self.visit(arg) for arg in args]
  File "/home/zgzhen/repos/cozy/cozy/codegen/cxx.py", line 775, in <listcomp>
    args = [self.visit(arg) for arg in args]
  File "/home/zgzhen/repos/cozy/cozy/codegen/java.py", line 682, in visit
    res = super().visit(x, *args, **kwargs)
  File "/home/zgzhen/repos/cozy/cozy/common.py", line 281, in visit
    return f(x, *args, **kwargs)
  File "/home/zgzhen/repos/cozy/cozy/codegen/cxx.py", line 424, in visit_Exp
    raise NotImplementedError(e)
NotImplementedError: ESingleton(EVar('x').with_type(TInt())).with_type(TBag(TInt()))

[izgzhen]

does it mean that we can't generate code for a singleton of integer?

[izgzhen]

Also, I invoked the code with --java, why will it lead to cxx.py somehow...

[izgzhen]

the latest ten or so layers of stack trace shows that calls are bumping between cxx and java visitors, which doesn't look like a good thing

[izgzhen]

Sorry for above two comments, it looks like Java printer somehow reuse cxx printer code...

[izgzhen]

I guess it means that ESingleton is not implemented for CXXPrinter

[izgzhen]

wait, it is extremely weird that with_type is not evaled.

EDIT: it is just printed that way ... em, the fact is that e.type is not well-considered (but even if so, will it help? is it deliberate?)

[Calvin-L]

Thanks for filing this!

Do you still have the /tmp/failed_codegen.py file that was generated when the exception got thrown? Having it would make it much easier to reproduce this problem.

As much as possible, Cozy tries to turn collection-type expressions into loops when generating code. Thus, many collection-type expressions like ESingleton are not handled at all since Cozy expects to turn them into loops. Usually the best fix for this problem is to change the code generation for the expression containing the ESingleton expression so that it invokes self.for_each instead of generating code to produce an actual in-memory list containing one element. (That is why it would be very useful to have the failed_codegen.py file, which contains the whole intermediate output just before codegen.)

That said, this issue can be fixed immediately by adding

    def visit_ESingleton(self, e):
        return self.visit(self.to_lvalue(e))

to cozy/codegen/cxx.py. The to_lvalue function knows how to convert any collection-type expression into an in-memory list by iterating over it. However before applying this fix we should check whether we can loopify your particular example instead.

Also note that issue #49 exists to remind us that the loopification transformation should really be done as a separate pass before code generation---a larger refactor that would make this less of a headache.

---

it looks like Java printer somehow reuse cxx printer code

Yes, because the languages have many similar constructs, they share some code. The Java code generator class extends the C++ code generator class, so calls to self.___ in java.py often dispatch to implementations in the parent class from cxx.py.

wait, it is extremely weird that with_type is not evaled

I do not understand this comment or your edit. What do you mean by "eval" here? Where are you expecting it to be "well-considered"?

[izgzhen]

Thanks for help!

the failed case: failed_codegen.py.txt

I do not understand this comment or your edit. What do you mean by "eval" here? Where are you expecting it to be "well-considered"?

I later found that the expression e.with_type(t) is pretty-printed in such form (through at the first glance it seems to be a thunk ... which would be a surprise in a language like Python)

[izgzhen]

I realized that it is better to use loopification, though I was trying out a more ad-hoc approach just minutes ago as well. I am still trying to understand this codebase now.

[Calvin-L]

.with_type is just a setter: it modifies the .type property of the expression object. It returns the expression object (e.g. e.with_type(t) returns e), so you can use it in expressions conveniently.

When expression objects are printed (e.g. print(e)), they are converted to strings using the .__repr__ magic method. Exp.__repr__ adds the .with_type(...) part so that you can copy-paste the printed text as Python code to obtain exactly the same expression objects with the same types. Being able to copy-paste the output of __repr__ into Python code is considered good practice.