Require collections given to arg{min,max} to be non-empty

This is additional progress on #23.

cozy/invariant_preservation.py

@@ -54,6 +54,16 @@ def check_the_wf(spec : Spec):
                 res.append("at {}: `the` is illegal since its argument may not be singleton".format(pprint(e)))
     return res
 
+def check_minmax_wf(spec : Spec):
+    res = []
+    for ctx in enumerate_fragments(spec):
+        e = ctx.e
+        if isinstance(e, EArgMin) or isinstance(e, EArgMax):
+            a = ctx.facts
+            if not valid(EImplies(EAll(a), EUnaryOp(UOp.Exists, e.e).with_type(BOOL))):
+                res.append("at {}: result is ambiguous since {} could be empty".format(pprint(e), pprint(e.e)))
+    return res
+
 def check_calls_wf(spec : Spec):
     res = []
     queries = { m.name : m for m in spec.methods if isinstance(m, Query) }

cozy/main.py

@@ -81,6 +81,7 @@ def run():
         errors = (
             invariant_preservation.check_ops_preserve_invariants(ast) +
             invariant_preservation.check_the_wf(ast) +
+            invariant_preservation.check_minmax_wf(ast) +
             call_errors)
         if errors:
             for e in errors: