uwplse / syncro

Synthesis of Incremental Operations
2 stars 1 forks source link

Support for higher-order functions #12

Open Sumith1896 opened 7 years ago

Sumith1896 commented 7 years ago

Two benchmarks from Itzhaky that is of interest here is:

C = f(S) and S += {a} ~> C += {f(a)}
C = f-inv(S) and f(a) = b ~> 
     if S does not contain b: C -= {a} else: C += {a}
rohinmshah commented 7 years ago

I think the right way to do this is to redo the Procedure-type so that it only takes one argument (so all the multi-argument operations must be curried), similar to a more traditional treatment. This allows us to not have to jump through hoops to work with argument lists of variable size. This will probably be a fairly large refactoring though, I think?

We'd also have to rethink how we do the read indexes and write indexes for procedures, which are necessary for the mutability analysis.

Once this is done, then we can add a special call construct to the language, which takes a function (A -> B) and an A, and produces a B. (This is doable but more complicated than it should be currently because you have to deal with a list of arguments instead of a single argument.)