[minor] Merge pull request #300 from tnelson/dev

[minor] Named asserts, various fixes

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/lang/alloy-syntax/parser.rkt

@@ -85,7 +85,8 @@ ParaDecls : /LEFT-PAREN-TOK @ParaDeclList? /RIGHT-PAREN-TOK
           | /LEFT-SQUARE-TOK @ParaDeclList? /RIGHT-SQUARE-TOK
 
 AssertDecl : /ASSERT-TOK Name? Block
-CmdDecl :  (Name /COLON-TOK)? (RUN-TOK | CHECK-TOK) (QualName | Block)? Scope? (/FOR-TOK Bounds)?
+CmdDecl :  Name /COLON-TOK (RUN-TOK | CHECK-TOK) (QualName | Block)? Scope? (/FOR-TOK Bounds)?
+        | (RUN-TOK | CHECK-TOK) (QualName | Block)? Scope? (/FOR-TOK Bounds)?
 
 TestDecl : (Name /COLON-TOK)? (QualName | Block) Scope? (/FOR-TOK Bounds)? /IS-TOK
            (SAT-TOK | UNSAT-TOK | UNKNOWN-TOK | THEOREM-TOK | FORGE_ERROR-TOK (PATH-OR-STR-TOK)? | CHECKED-TOK )
@@ -97,12 +98,17 @@ Typescope : EXACTLY-TOK? Number QualName
 Const : NONE-TOK | UNIV-TOK | IDEN-TOK
       | MINUS-TOK? Number 
 
-SatisfiabilityDecl : /ASSERT-TOK Expr /IS-TOK (SAT-TOK | UNSAT-TOK | FORGE_ERROR-TOK) Scope? (/FOR-TOK Bounds)? 
-PropertyDecl : /ASSERT-TOK Expr /IS-TOK (SUFFICIENT-TOK | NECESSARY-TOK) /FOR-TOK Name Scope? (/FOR-TOK Bounds)? 
-QuantifiedPropertyDecl : /ASSERT-TOK /ALL-TOK DISJ-TOK? QuantDeclList /BAR-TOK Expr /IS-TOK (SUFFICIENT-TOK | NECESSARY-TOK) /FOR-TOK Name (/LEFT-SQUARE-TOK ExprList /RIGHT-SQUARE-TOK)? Scope? (/FOR-TOK Bounds)? 
+SatisfiabilityDecl : Name /COLON-TOK /ASSERT-TOK Expr /IS-TOK (SAT-TOK | UNSAT-TOK | FORGE_ERROR-TOK) Scope? (/FOR-TOK Bounds)? 
+                         | /ASSERT-TOK Expr /IS-TOK (SAT-TOK | UNSAT-TOK | FORGE_ERROR-TOK) Scope? (/FOR-TOK Bounds)?
 
-; Should this have a unique name?
-ConsistencyDecl: /ASSERT-TOK Expr /IS-TOK (CONSISTENT-TOK | INCONSISTENT-TOK) /WITH-TOK Name Scope? (/FOR-TOK Bounds)?
+PropertyDecl : Name /COLON-TOK /ASSERT-TOK Expr /IS-TOK (SUFFICIENT-TOK | NECESSARY-TOK) /FOR-TOK Name Scope? (/FOR-TOK Bounds)?
+             | /ASSERT-TOK Expr /IS-TOK (SUFFICIENT-TOK | NECESSARY-TOK) /FOR-TOK Name Scope? (/FOR-TOK Bounds)?
+
+QuantifiedPropertyDecl : Name /COLON-TOK /ASSERT-TOK /ALL-TOK DISJ-TOK? QuantDeclList /BAR-TOK Expr /IS-TOK (SUFFICIENT-TOK | NECESSARY-TOK) /FOR-TOK Name (/LEFT-SQUARE-TOK ExprList /RIGHT-SQUARE-TOK)? Scope? (/FOR-TOK Bounds)? 
+             | /ASSERT-TOK /ALL-TOK DISJ-TOK? QuantDeclList /BAR-TOK Expr /IS-TOK (SUFFICIENT-TOK | NECESSARY-TOK) /FOR-TOK Name (/LEFT-SQUARE-TOK ExprList /RIGHT-SQUARE-TOK)? Scope? (/FOR-TOK Bounds)? 
+
+ConsistencyDecl: Name /COLON-TOK /ASSERT-TOK Expr /IS-TOK (CONSISTENT-TOK | INCONSISTENT-TOK) /WITH-TOK Name Scope? (/FOR-TOK Bounds)?
+                | /ASSERT-TOK Expr /IS-TOK (CONSISTENT-TOK | INCONSISTENT-TOK) /WITH-TOK Name Scope? (/FOR-TOK Bounds)?
 
 
 TestSuiteDecl : /TEST-TOK /SUITE-TOK /FOR-TOK Name /LEFT-CURLY-TOK TestConstruct* /RIGHT-CURLY-TOK

forge/lang/expander.rkt

@@ -361,22 +361,26 @@
     (pattern decl:ConsistencyDeclClass))
 
   (define-syntax-class PropertyDeclClass
-    #:attributes (prop pred-name constraint-type scope bounds)
-    (pattern ((~datum PropertyDecl)      
+    #:attributes (tname prop pred-name constraint-type scope bounds)
+    (pattern (
+              (~datum PropertyDecl)      
+              (~optional -tname:NameClass)
               -prop:ExprClass
               (~and (~or "sufficient" "necessary") ct)
               -pred-name:NameClass
               (~optional -scope:ScopeClass)
               (~optional -bounds:BoundsClass))
+      #:with tname (if (attribute -tname) #'-tname.name (datum->syntax #f ""))
       #:with prop #'-prop
       #:with pred-name #'-pred-name.name
       #:with constraint-type (string->symbol (syntax-e #'ct))
       #:with scope (if (attribute -scope) #'-scope.translate #'())
       #:with bounds (if (attribute -bounds) #'-bounds.translate #'())))
 
   (define-syntax-class QuantifiedPropertyDeclClass
-    #:attributes (quant-decls disj prop pred-name pred-exprs constraint-type scope bounds)
+    #:attributes (tname quant-decls disj prop pred-name pred-exprs constraint-type scope bounds)
     (pattern ((~datum QuantifiedPropertyDecl)
+              (~optional -tname:NameClass)
               (~optional (~and "disj" -disj))
               -quant-decls:DeclListClass
               -prop:ExprClass
@@ -385,6 +389,7 @@
               (~optional -pred-exprs:ExprListClass)
               (~optional -scope:ScopeClass)
               (~optional -bounds:BoundsClass))
+      #:with tname (if (attribute -tname) #'-tname.name (datum->syntax #f ""))
       #:with disj (if (attribute -disj) (string->symbol (syntax-e #'-disj)) '())
       #:with quant-decls #'-quant-decls.translate
       #:with prop #'-prop
@@ -395,26 +400,30 @@
       #:with bounds (if (attribute -bounds) #'-bounds.translate #'())))
 
 (define-syntax-class SatisfiabilityDeclClass
-  #:attributes (prop expected scope bounds)
+  #:attributes (tname prop expected scope bounds)
   (pattern ((~datum SatisfiabilityDecl)
+            (~optional -tname:NameClass)
             -prop:ExprClass
             (~and (~or "sat" "unsat" "forge_error") ct)
             (~optional -scope:ScopeClass)
             (~optional -bounds:BoundsClass))
+    #:with tname (if (attribute -tname) #'-tname.name (datum->syntax #f ""))
     #:with prop #'-prop
     #:with expected (string->symbol (syntax-e #'ct))
     #:with scope (if (attribute -scope) #'-scope.translate #'())
     #:with bounds (if (attribute -bounds) #'-bounds.translate #'())))
 
 
 (define-syntax-class ConsistencyDeclClass
-  #:attributes (test-expr pred-name consistency expected scope bounds)
-  (pattern ((~datum ConsistencyDecl)      
+  #:attributes (tname test-expr pred-name consistency expected scope bounds)
+  (pattern ((~datum ConsistencyDecl) 
+            (~optional -tname:NameClass)     
             -test-expr:ExprClass
             (~and (~or "consistent" "inconsistent") ct)
             -pred-name:NameClass
             (~optional -scope:ScopeClass)
             (~optional -bounds:BoundsClass))
+    #:with tname (if (attribute -tname) #'-tname.name (datum->syntax #f ""))
     #:with test-expr #'-test-expr
     #:with pred-name #'-pred-name.name
     #:with consistency (string->symbol (syntax-e #'ct)) ;; This is for good test naming
@@ -1044,7 +1053,10 @@
                         (syntax/loc stx (implies pwd.prop pwd.pred-name))  ;; p => q : p is a sufficient condition for q 
                         (syntax/loc stx (implies pwd.pred-name pwd.prop))) ;; q => p : p is a necessary condition for q
 
-   #:with test_name (format-id stx "~a_assertion_for_~a_~a" #'pwd.constraint-type #'pwd.pred-name (make-temporary-name stx)) ;; Use the string in the test name
+  #:with test_name  (if (equal? (syntax-e #'pwd.tname) "")
+                      (format-id stx "~a_assertion_for_~a_~a" #'pwd.constraint-type #'pwd.pred-name (make-temporary-name stx))
+                      #'pwd.tname)
+
    (syntax/loc stx
       (test
         test_name
@@ -1063,7 +1075,9 @@
                                 (syntax/loc stx qpd.pred-name)
                                 (syntax/loc stx (exp-pred-exprs ...)))]
 
-          [test_name (format-id stx "quantified_~a_assertion_for_~a_~a" #'qpd.constraint-type #'qpd.pred-name (make-temporary-name stx))] 
+          [test_name (if (equal? (syntax-e #'qpd.tname) "")
+                        (format-id stx "quantified_~a_assertion_for_~a_~a" #'qpd.constraint-type #'qpd.pred-name (make-temporary-name stx))
+                        #'qpd.tname)]
           [imp_total
             (if (eq? (syntax-e #'qpd.disj) 'disj)
                 (if (eq? (syntax-e #'qpd.constraint-type) 'sufficient)
@@ -1074,7 +1088,7 @@
                     (syntax/loc stx (all  qpd.quant-decls (implies pred-consolidated qpd.prop)))))])
      (syntax/loc stx
        (test
-         test_name
+          test_name
          #:preds [imp_total]
          #:scope qpd.scope
          #:bounds qpd.bounds
@@ -1084,7 +1098,9 @@
 (define-syntax (SatisfiabilityDecl stx)
   (syntax-parse stx
   [sd:SatisfiabilityDeclClass 
-   #:with test_name (format-id stx "~a_assertion_~a" #'sd.expected (make-temporary-name stx))
+      #:with test_name (if (equal? (syntax-e #'sd.tname) "")
+                      (format-id stx "~a_assertion_~a" #'sd.expected (make-temporary-name stx))
+                      #'sd.tname)
    (syntax/loc stx
       (test
         test_name
@@ -1096,7 +1112,9 @@
 (define-syntax (ConsistencyDecl stx)
   (syntax-parse stx
   [cd:ConsistencyDeclClass 
-    #:with test_name (format-id stx "~a_assertion_for_~a_~a" #'cd.consistency #'cd.pred-name (make-temporary-name stx))
+    #:with test_name (if (equal? (syntax-e #'cd.tname) "")
+                      (format-id stx "~a_assertion_for_~a_~a" #'cd.consistency #'cd.pred-name (make-temporary-name stx))
+                      #'cd.tname)
     #:with conj_total (syntax/loc stx (&& cd.test-expr cd.pred-name))
    (syntax/loc stx
       (test

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)]