optimize: restrict keyword to #:maximize and #:minimize (emina#188)

* optimize: restrict keyword to #:maximize and #:minimize * allow #:maximize and then #:minimize Providing #:minimize twice will still be prohibited, since it will error already by function application after the expansion of `optimize`.
REA1 · Apr 14, 2021 · a7ea8a8 · a7ea8a8
1 parent a64e2bc
commit a7ea8a8
Showing 1 changed file with 11 additions and 9 deletions.
diff --git a/rosette/query/form.rkt b/rosette/query/form.rkt
@@ -1,6 +1,7 @@
 #lang racket
 
-(require "core.rkt" 
+(require syntax/parse/define
+         "core.rkt"
          (only-in "../base/core/reflect.rkt" symbolics)
          (only-in "../base/core/result.rkt" result-state)
          (only-in "../base/core/bool.rkt" ! vc with-vc vc-assumes vc-asserts vc-true))
@@ -70,14 +71,15 @@
 ; generate any assumptions or assertions, these are reflected in the (vc) after
 ; the optimize query returns. The assumptions and assertions generated by expr
 ; are not added to (vc) after optimize returns.
-(define-syntax optimize
-  (syntax-rules ()
-    [(_ kw opt #:guarantee expr)
-     (let ([obj opt]    ; evaluate objective first to add its spec to (vc)
+(define-syntax-parser optimize
+  [(_ {~and kw {~or* #:minimize #:maximize}} opt #:guarantee expr)
+   #'(let ([obj opt]    ; evaluate objective first to add its spec to (vc)
            [post (query-vc expr)])
        (∃-solve `(,@(pre) ,(vc-assumes post) ,(vc-asserts post)) kw obj))]
-    [(_ kw1 opt1 kw2 opt2 #:guarantee expr)
-     (let ([obj1 opt1]  ; evaluate objectives first to add their spec to (vc)
+  [(_ {~and kw1 {~or* #:minimize #:maximize}} opt1
+      {~and kw2 {~or* #:minimize #:maximize}} opt2
+      #:guarantee expr)
+   #'(let ([obj1 opt1]  ; evaluate objectives first to add their spec to (vc)
            [obj2 opt2]
-           [post (query-vc expr)])  
-       (∃-solve `(,@(pre) ,(vc-assumes post) ,(vc-asserts post)) kw1 obj1 kw2 obj2))]))
+           [post (query-vc expr)])
+       (∃-solve `(,@(pre) ,(vc-assumes post) ,(vc-asserts post)) kw1 obj1 kw2 obj2))])