Synthesis with partial functions

[Calvin-L]

Right now all AST nodes in Cozy are total, meaning that they can never fail. A good example is map lookup (map[key]) which returns a default value if the key is missing rather than throw an exception.

Unfortunately, this means that at codegen time we need to insert additional checks (e.g. "is the key in the map? if not, return a default value"). It would be much better if the synthesizer knew that some functions were only legal under some conditions so that we would not have to emit these checks. After all, in many cases the checks will always be true.

Examples of partial functions:

• the xs is only legal when xs is a singleton collection
• for handles, x.val is only legal when x is not null
• m[key] is only legal when key is in m
• min xs is only legal when xs is not empty
• x / y is only legal when y is nonzero

Plan:

• As far as satisfy and eval are concerned, everything remains total
• Need a new function fails : Exp -> Exp that produces a boolean expression describing under what circumstances the input expression fails
• Optional: all input queries should never fail (their preconditions must be strong enough)
• Failure on each example should be part of the fingerprint of an expression (and furthermore, failure on an input renders the output value irrelevant when comparing fingerprints)
• core.py should ensure that not only does the new expression produce the same values, but it may only fail when the original expression fails (although the output is allowed to fail less often)
• Codegen may then skip unnecessary checks on partial AST nodes