[minor] Improve typechecking for pred/fun use, update Sterling (#299)

* working on fix

* update sterling to add most-specific-sig, help modal

* add: basic example showing optimizer inst

forge/examples/basic/restricting_space.frg

@@ -0,0 +1,18 @@
+#lang forge
+
+/*
+  Example of restricting search space in Forge. 
+  The Sudoku example contains a more involved version of this. 
+*/
+
+one sig Example {
+    f: pfunc Int -> Int
+}
+
+run { } 
+  for 10 Int // [-512,511]
+  for {
+    Example = `Example
+    // Relational Forge will allow this sort of binding annotation:
+    `Example.f in (0+1+2+3+4+5+6+7+8+9) -> (0+1+2+3+4+5+6+7+8+9)
+  }

forge/froglet/lang/bsl-lang-specific-checks.rkt

@@ -50,9 +50,9 @@
 ; Should be unified with other registered functions
 (define (err-empty-join expr-node child-types #:run-or-state [run-or-state #f])
   (define loc (nodeinfo-loc (node-info expr-node)))
-  ; Deprimification lets us print, e.g., "Animal" rather than "(Dog Cat Human ...)"
+  ; Deprimification lets us print, e.g., "(Animal)" rather than "((Dog) (Cat) (Human) ...)"
   (define lhs-type (if run-or-state 
-                       (deprimify run-or-state (expression-type-type (first child-types)))
+                       (deprimify run-or-state (map car (expression-type-type (first child-types))))
                        (expression-type-type (first child-types))))
   (if (and (equal? 1 (length lhs-type))
            (symbol? (first lhs-type)))

forge/last-checker.rkt

@@ -45,6 +45,52 @@
                                  (datum->syntax #f (deparse a-node) (build-source-location-syntax (nodeinfo-loc (node-info a-node)))))))
 
 
+; Within this run, do the argument types fall inside the domain types?
+(define (check-helper-args run-or-state helper-type name args arg-types domain-types)    
+  (for-each
+   ; Check that each potential type in argument K is contained in the type of parameter K.
+   ; These types are represented as a union (list) of products (list).
+   ; E.g., ( (A) (B) (C) ) represents A+B+C. 
+   (lambda (type)
+     (define arg-union-of-products (car type)) ; e.g., ( (A) (B) (C) )
+     (define arg-position (cadr type))
+     ; These products are not necessarily unary. We'll deprimify if they are, but otherwise
+     ; the error may not be very pretty. 
+     (define deprimified-arg-union-of-products
+       (if (and (list? arg-union-of-products)
+                (not (empty? arg-union-of-products))
+                (list? (car arg-union-of-products))
+                (equal? 1 (length (car arg-union-of-products))))
+           (map list (deprimify run-or-state (map car arg-union-of-products)))
+           arg-union-of-products))
+
+     ; A bit early to do this, but make the code more clear
+     (define domain-products (list-ref domain-types arg-position))
+     (define deprimified-domain-products
+       (if (and (list? domain-products)
+                (not (empty? domain-products))
+                (list? (car domain-products))
+                (equal? 1 (length (car domain-products))))
+           (map list (deprimify run-or-state (map car domain-products)))
+           domain-products))
+
+     ;(printf "Checking idx=~a~n deprim-type=~a~n deprim-domain=~a~n"
+     ;        arg-position deprimified-arg-union-of-products deprimified-domain-products)
+     (for-each
+      (lambda (a-product)
+        ; (printf "    Checking the product: ~a~n" a-product)
+
+        (unless (member a-product domain-products)
+          (raise-forge-error
+           #:msg (format "Argument ~a of ~a given to ~a ~a is of incorrect type. Expected type in ~a, but argument was in type ~a." 
+                         (add1 arg-position) (length args) helper-type name
+                         deprimified-domain-products
+                         ; Don't use a-product here because it is a single product only.
+                         deprimified-arg-union-of-products)
+           #:context (apply-record-arg (list-ref args arg-position)))))
+      arg-union-of-products))
+   arg-types))
+
 ; Recursive descent for last-minute consistency checking
 ; Catch potential issues not detected by AST construction + generate warnings
 (define/contract (checkFormula run-or-state formula quantvars checker-hash)
@@ -62,27 +108,16 @@
      (check-and-output formula node/formula/constant checker-hash #f)]
 
     [(node/fmla/pred-spacer info name args expanded)
-    (define domain-types (for/list ([arg args]) 
-                         (expression-type-type (checkExpression run-or-state (mexpr-expr (apply-record-domain arg)) quantvars checker-hash))))
+    (define domain-types (for/list ([arg args])
+                           (define inferred-param (checkExpression run-or-state (mexpr-expr (apply-record-domain arg)) quantvars checker-hash))
+                           (expression-type-type inferred-param)))
 
-    (define arg-types (for/list ([arg args]  [acc (range 0 (length args))])
-                      (list (expression-type-type (checkExpression run-or-state (apply-record-arg arg) quantvars checker-hash)) acc)))
-    ;(printf "pred spacer: ~a~n~a~n~a~n" name domain-types arg-types)
-    (for-each 
-        (lambda (type) (if (not (member (car (car type)) (list-ref domain-types (cadr type))))
-            (raise-forge-error
-            #:msg (format "Argument ~a of ~a given to predicate ~a is of incorrect type. Expected type ~a, given type ~a" 
-                  (add1 (cadr type)) (length args) name (deprimify run-or-state 
-                                                        (if (equal? (map Sig-name (get-sigs run-or-state)) (flatten domain-types))
-                                                        (map Sig-name (get-sigs run-or-state)) ; if the domain is univ then just pass in univ
-                                                        (list-ref domain-types (cadr type)))) ; else pass in the sig one by one
-                                                        (deprimify run-or-state 
-                                                        (if (equal? (map Sig-name (get-sigs run-or-state)) (flatten (car (car arg-types))))
-                                                        (map Sig-name (get-sigs run-or-state)) ; if the argument is univ then just pass in univ
-                                                        (car (car type))))) ; else pass in the sig one by one
-            #:context (apply-record-arg (list-ref args (cadr type))))
-            (void)))
-            arg-types)
+    (define arg-types (for/list ([arg args]
+                                 [acc (range 0 (length args))])
+                        (define inferred-arg (checkExpression run-or-state (apply-record-arg arg) quantvars checker-hash))
+                        (list (expression-type-type inferred-arg) acc)))
+
+    (check-helper-args run-or-state 'predicate name args arg-types domain-types)
     (checkFormula run-or-state expanded quantvars checker-hash)]
 
     [(node/formula/op info args)
@@ -323,7 +358,7 @@
 ; wrap around checkExpression-mult to provide check for multiplicity, 
 ; while throwing the multiplicity away in output; DO NOT CALL THIS AS PASSTHROUGH!
 (define (checkExpression run-or-state expr quantvars checker-hash)
-;(printf "expr: ~a~n" expr)
+  ;(printf "checkExpression for: ~a~n" expr)
   (match expr 
     ; extra work done on int - adding 1 to a var
     [(? node/int?) (expression-type (list (list 'Int)) 'one #f (list 'Int))]
@@ -395,25 +430,14 @@
                          (expression-type-type (checkExpression run-or-state (mexpr-expr (apply-record-domain arg)) quantvars checker-hash))))
       (define arg-types (for/list ([arg args]  [acc (range 0 (length args))])
                       (list (expression-type-type (checkExpression run-or-state (apply-record-arg arg) quantvars checker-hash)) acc)))
-      (for-each 
-        (lambda (type) (if (not (member (car (car type)) (list-ref domain-types (cadr type))))
-            (raise-forge-error
-            #:msg (format "Argument ~a of ~a given to function ~a is of incorrect type. Expected type ~a, given type ~a" 
-                  (add1 (cadr type)) (length args) name (deprimify run-or-state 
-                                                        (if (equal? (map Sig-name (get-sigs run-or-state)) (flatten domain-types))
-                                                        (map Sig-name (get-sigs run-or-state)) ; if the domain is univ then just pass in univ
-                                                        (list-ref domain-types (cadr type)))) ; else pass in the sig one by one
-                                                        (deprimify run-or-state 
-                                                        (if (equal? (map Sig-name (get-sigs run-or-state)) (flatten (car (car arg-types))))
-                                                        (map Sig-name (get-sigs run-or-state)) ; if the argument is univ then just pass in univ
-                                                        (car (car type))))) ; else pass in the sig one by one
-            #:context (apply-record-arg (list-ref args (cadr type))))
-            (void)))
-            arg-types)
+
+      (check-helper-args run-or-state 'function name args arg-types domain-types)
+
       (define output-type (expression-type-type (checkExpression run-or-state expanded quantvars checker-hash)))
-      (if (not (member (car output-type) (expression-type-type (checkExpression run-or-state (mexpr-expr codomain) quantvars checker-hash))))
+      (define codomain-type (expression-type-type (checkExpression run-or-state (mexpr-expr codomain) quantvars checker-hash)))
+      (if (not (member (car output-type) codomain-type))
           (raise-forge-error
-          #:msg (format "The output of function ~a is of incorrect type" name)
+          #:msg (format "The output of function ~a is of incorrect type. Got ~a, expected in ~a" name (car output-type) codomain-type)
           #:context expanded)
           (void))
        (checkExpression-mult run-or-state expanded quantvars checker-hash)]

forge/server/forgeserver.rkt

@@ -515,4 +515,4 @@
               (empty? useful-run-names))
     (serve-sterling-static #:provider-port port))
   (when (empty? useful-run-names)
-    (printf "There was nothing useful to visualize: all commads were already executed and produced no instances.~n")))
+    (printf "There was nothing useful to visualize: all commands were already executed and produced no instances.~n")))

forge/sigs-structs.rkt

@@ -892,19 +892,33 @@ Returns whether the given run resulted in sat or unsat, respectively.
                                 "_remainder")))
                          all-primitive-descendants)])])))
 
-(define (deprimify run-or-state primsigs)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Reversing `primify` to produce a shortest set of sig names
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+; We assume that the list of sigs given is already primified; i.e., there are no non-primitive
+; sig names (X_remainder counts as a primitive sig) being passed to this function.
+; This version works only for lists of primified sig symbols, e.g. (A B C D_remainder)
+(define/contract (deprimify run-or-state primsigs)
+  (-> (or/c Run? State? Run-spec?) (non-empty-listof symbol?) (non-empty-listof symbol?))
   (let ([all-sigs (map Sig-name (get-sigs run-or-state))])
     (cond
-      [(equal? primsigs '(Int))
-       'Int]
-      [(equal? primsigs (remove-duplicates (flatten (map (lambda (n) (primify run-or-state n)) (cons 'Int all-sigs)))))
-       'univ]
+      ; In case this is a singleton list, we can't improve anything
+      [(and (list? primsigs) (equal? 1 (length primsigs)))
+       primsigs]
+      ; In case all sigs are represented here, it's univ
+      [(equal? (list->set primsigs)
+               (list->set (remove-duplicates (flatten (map (lambda (n) (primify run-or-state n)) (cons 'Int all-sigs))))))
+       '(univ)]
+      ; Otherwise, compress as much as possible
+      ; Use primify to handle the X_remainder cases.
       [else (define top-level (get-top-level-sigs run-or-state))
-            (define pseudo-fold-lambda (lambda (sig acc) (if (or (subset? (primify run-or-state (Sig-name sig)) (flatten primsigs))
-                                                                 (equal? (list (car (primify run-or-state (Sig-name sig)))) (flatten primsigs)))
-                                                                 ; the above check is added for when you have the parent sig, but are expecting the child
-                                      (values (append acc (list (Sig-name sig))) #t) ; replace cons with values
-                                      (values acc #f))))
+            (define pseudo-fold-lambda (lambda (sig acc)
+                                         (if (or (subset? (primify run-or-state (Sig-name sig)) (flatten primsigs))
+                                                 (equal? (list (car (primify run-or-state (Sig-name sig)))) (flatten primsigs)))
+                                             ; the above check is added for when you have the parent sig, but are expecting the child
+                                             (values (append acc (list (Sig-name sig))) #t) ; replace cons with values
+                                             (values acc #f))))
             (define final-list (dfs-sigs run-or-state pseudo-fold-lambda top-level '()))
             final-list])))
 

forge/tests/error/main.rkt

@@ -179,19 +179,19 @@
     (list "parsing_less_dash.frg" #rx"Negative numbers must not have blank space between the minus")
 
     ;; Mismatched type tests - pred
-    (list "mismatched-arg-type-basic.frg" #rx"Argument 1 of 1 given to predicate p2 is of incorrect type. Expected type \\(B\\), given type \\(A\\)")
-    (list "mismatched-arg-type-basic-univ.frg" #rx"Argument 1 of 1 given to predicate p2 is of incorrect type. Expected type \\(B\\), given type univ") 
-    (list "mismatched-arg-type-arity.frg" #rx"Argument 2 of 2 given to predicate p2 is of incorrect type. Expected type \\(B\\), given type \\(A\\)")
-    (list "mismatched-arg-type-no-quant.frg" #rx"Argument 1 of 1 given to predicate p1 is of incorrect type. Expected type \\(A\\), given type \\(C\\)")
-    (list "mismatched-arg-type-no-quant2.frg" #rx"Argument 2 of 2 given to predicate p2 is of incorrect type. Expected type \\(B\\), given type \\(A\\)")
-    (list "mismatched-arg-type-non-primsig.frg" #rx"Argument 1 of 1 given to predicate p2 is of incorrect type. Expected type \\(B\\), given type \\(A\\)")
-    (list "mismatched-arg-type-non-primsig2.frg" #rx"Argument 1 of 1 given to predicate p is of incorrect type. Expected type \\(C\\), given type \\(B\\)")
-    (list "tree-type-error.frg" #rx"Argument 1 of 1 given to predicate p is of incorrect type. Expected type \\(A B_child1\\), given type \\(B_child2\\)")
-    (list "mismatched-arg-type-int.frg" #rx"Argument 1 of 1 given to predicate p2 is of incorrect type. Expected type \\(Int\\), given type \\(A\\)")
+    (list "mismatched-arg-type-basic.frg"      #rx"Argument 1 of 1 given to predicate p2 is of incorrect type. Expected type in \\(\\(B\\)\\), but argument was in type \\(\\(A\\)\\)")
+    (list "mismatched-arg-type-basic-univ.frg" #rx"Argument 1 of 1 given to predicate p2 is of incorrect type. Expected type in \\(\\(B\\)\\), but argument was in type \\(\\(univ\\)\\)") 
+    (list "mismatched-arg-type-arity.frg" #rx"Argument 2 of 2 given to predicate p2 is of incorrect type. Expected type in \\(\\(B\\)\\), but argument was in type \\(\\(A\\)\\)")
+    (list "mismatched-arg-type-no-quant.frg" #rx"Argument 1 of 1 given to predicate p1 is of incorrect type. Expected type in \\(\\(A\\)\\), but argument was in type \\(\\(C\\)\\)")
+    (list "mismatched-arg-type-no-quant2.frg" #rx"Argument 2 of 2 given to predicate p2 is of incorrect type. Expected type in \\(\\(B\\)\\), but argument was in type \\(\\(A\\)\\)")
+    (list "mismatched-arg-type-non-primsig.frg" #rx"Argument 1 of 1 given to predicate p2 is of incorrect type. Expected type in \\(\\(B\\)\\), but argument was in type \\(\\(A\\)\\)")
+    (list "mismatched-arg-type-non-primsig2.frg" #rx"Argument 1 of 1 given to predicate p is of incorrect type. Expected type in \\(\\(C\\)\\), but argument was in type \\(\\(B\\)\\)")
+    (list "tree-type-error.frg" #rx"Argument 1 of 1 given to predicate p is of incorrect type. Expected type in \\(\\(A\\) \\(B_child1\\)\\), but argument was in type \\(\\(B_child2\\)\\)")
+    (list "mismatched-arg-type-int.frg" #rx"Argument 1 of 1 given to predicate p2 is of incorrect type. Expected type in \\(\\(Int\\)\\), but argument was in type \\(\\(A\\)\\)")
 
     ;; Mismatched type tests - fun
-    (list "mismatched-arg-type-fun.frg" #rx"Argument 1 of 1 given to function f is of incorrect type. Expected type \\(A\\), given type \\(B\\)")
-    (list "mismatched-arg-type-fun-arity.frg" #rx"Argument 2 of 2 given to function f is of incorrect type. Expected type \\(A\\), given type \\(B\\)")
+    (list "mismatched-arg-type-fun.frg" #rx"Argument 1 of 1 given to function f is of incorrect type. Expected type in \\(\\(A\\)\\), but argument was in type \\(\\(B\\)\\)")
+    (list "mismatched-arg-type-fun-arity.frg" #rx"Argument 2 of 2 given to function f is of incorrect type. Expected type in \\(\\(A\\)\\), but argument was in type \\(\\(B\\)\\)")
     (list "mismatched-arg-type-fun-output.frg" #rx"The output of function f is of incorrect type")
     (list "mismatched-arg-type-fun-codomain.frg" #rx"The output of function f is of incorrect type")
     (list "mismatched-arg-type-fun-codomain-non-primsig.frg" #rx"The output of function f is of incorrect type")

forge/tests/forge-core/formulas/booleanFormulaOperators.rkt

@@ -1,6 +1,10 @@
 #lang forge/core
 
+;  Note: forge/formulas/booleanFormulaOperators contains more tests than this module. 
+;  Do not delete this without integrating the missing tests somewhere.
+
 (set-option! 'verbose 0)
+(set-option! 'run_sterling 'off)
 
 ; No more overloading (<and> and <or> are normal Racket operators now)
 
@@ -93,16 +97,21 @@
 
 ; Check the expansion of these helpers at least has the correct semantics
 (pred HelperPred    
-    (all ([value1 univ] [value2 univ])
+    (all ([value1 univ] [value2 univ] [someInt Int])
          (and (iff (pred1a value1) (in value1 Int))
               (iff (pred2a value1 value2) (and (in value1 Int) (in value2 Int)))
               (iff (pred2b value1 value2) (and (in value1 Int) (in value2 Int)))
               (iff (pred2c value1 value2) (and (in value1 Int) (in value2 Int)))
-              (iff (pred2d value1 value2) (and (in value1 Int) (in value2 Int)))
+              (iff (pred2d someInt value2) (and (in someInt Int) (in value2 Int)))
               ; cannot easily test higher-order helper predicate with forall, so pred_arity2_arg is left out here
               )))
 (test helperpreds #:preds [HelperPred] #:expect checked)
 
+(pred ExpectError 
+  (all ([value1 univ] [value2 univ])
+     (iff (pred2d value1 value2) (and (in value1 Int) (in value2 Int)))))
+(test ExpectErrorTest #:preds [ExpectError] #:expect forge_error)
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ; Test metadata
 

forge/tests/forge/formulas/booleanFormulaOperators.frg

@@ -1,8 +1,10 @@
 #lang forge
 
-option run_sterling off
-
+/*
+  Note: forge-core/formulas/booleanFormulaOperators contains more tests than this module. 
+*/
 
+option run_sterling off
 option verbose 0
 
 pred True {