Basic type-checking for predicate use, pred/fun syntax location use s…

…ite fix (#244)

forge/lang/ast.rkt

@@ -44,11 +44,11 @@
 ;     * node/formula/sealed
 ;       * wheat
 ;   * node/int -- integer expression
+;     * node/int/sum-quant -- sum "quantified" form
 ;     * node/int/op (children)
 ;       * node/int/op/add
 ;       * ...
 ;     * node/int/constant (value) -- int constant
-;   * node/unknown -- delayed binding of identifiers for predicates and functions
 ;; -----------------------------------------------------------------------------
 
 ; Struct to hold metadata about an AST node (like source location)

forge/lang/deparse.rkt

@@ -60,6 +60,8 @@
             (deparse-expr arg 20)]
         [(? node/int?)
             (deparse-int arg 20)]
+        [(? procedure?)
+            (format "(Racket procedure, which is likely an unexpected predicate or function definition: ~a)" arg)]
         [else 
             (format "(COULD-NOT-DEPARSE: ~a)" arg)]))
 

forge/lang/expander.rkt

@@ -44,6 +44,14 @@
 
   (make-token abstract-tok "abstract" #:abstract))
 
+; Used because we sometimes need to evaluate "inside-out" while expanding
+; macros "outside-in". The list of symbols are the "stop locations".
+; This, if we ever add more macros, they need to be added here (unless
+; they can be safely expanded as just themselves?)
+
+; TODO: why is lack of "prime" not breaking something? Is this only ops meant
+; to be used with [] or that have >1 argument?
+
 (define-for-syntax (my-expand stx)
   (define core-funcs-and-macros
     (map (curry datum->syntax stx)
@@ -54,7 +62,7 @@
            int< int> int= int>= int<=
            add subtract multiply divide sign abs remainder
            card sum sing succ max min sum-quant
-           node/int/constant
+           node/int/constant 
            let)))
 
   (define result (local-expand stx 'expression core-funcs-and-macros))
@@ -1302,10 +1310,11 @@
                  [(exprs ...) (datum->syntax #f (map my-expand (syntax->list #'(exprs.exprs ...))))])
      (syntax/loc stx (name exprs ...)))]
 
+
   [((~datum Expr) expr1:ExprClass "[" exprs:ExprListClass "]")
-   (with-syntax ([expr1 (my-expand #'expr1)]
-                 [(exprs ...) (datum->syntax #f (map my-expand (syntax->list #'(exprs.exprs ...))))])
-     (syntax/loc stx (expr1 exprs ...)))]
+     (with-syntax ([expr1 (my-expand #'expr1)]
+                   [(exprs ...) (datum->syntax #f (map my-expand (syntax->list #'(exprs.exprs ...))))])
+       (syntax/loc stx (expr1 exprs ...)))]
 
   [((~datum Expr) "~" expr1:ExprClass)
    (with-syntax ([expr1 (my-expand #'expr1)])
@@ -1332,7 +1341,9 @@
    (if local-value
        ; if we have a local-value, it's likely a Forge macro or Forge-defined helper procedure
        (syntax/loc stx name.name)
-       ; otherwise, it's likely an AST node (to be functionally updated with proper syntax location)
+       ; otherwise, it's likely an AST node (to be functionally updated with proper syntax 
+       ; location at runtime). Note this is a QualName at compile time, but may be substituted
+       ; to something more complex at runtime via pred/fun application.
        (with-syntax ([loc (build-source-location (syntax/loc this-syntax #'1))])
          (syntax/loc stx (correct-id-loc name.name #:loc loc))))]
 
@@ -1355,25 +1366,67 @@
 ; struct-copy would not retain the sub-struct identity and fields, producing just a node
 ; ditto the struct-update-lib library
 ; struct-set requires using a special form to create the struct.
-; Fortunately, all we need to deal with here _at this time_ is Sig and Relation structs...
+; We need to handle Sig and Relation cases, but at runtime the expression might be more
+; complex (via substitution from fun/pred application).
+
 ; *New* instance of the structure, with the same values but a (possibly) new source loc
 (define (correct-id-loc astnode #:loc [loc #f])
-  ;(printf "correct-id-loc: ~a; ~a~n" astnode loc)
+  ;(printf "correct-id-loc: ~a; ~a; ~a~n" astnode (node? astnode) loc)
+
+  (define new-info (if (node? astnode)
+                       (nodeinfo loc (nodeinfo-lang (node-info astnode)))
+                       #f))
   (cond [(forge:Sig? astnode)
-         (define new-info (nodeinfo loc (nodeinfo-lang (node-info astnode))))
          (forge:Sig new-info
                     (node/expr-arity astnode) (node/expr/relation-name astnode) (node/expr/relation-typelist-thunk astnode)
                     (node/expr/relation-parent astnode) (node/expr/relation-is-variable astnode) (node/expr/relation-name astnode)
                     (forge:Sig-one astnode) (forge:Sig-lone astnode) (forge:Sig-abstract astnode) (forge:Sig-extends astnode))]
         [(forge:Relation? astnode)
-         (define new-info (nodeinfo loc (nodeinfo-lang (node-info astnode))))
          (forge:Relation new-info
                          (node/expr-arity astnode) (node/expr/relation-name astnode) (node/expr/relation-typelist-thunk astnode)
                          (node/expr/relation-parent astnode) (node/expr/relation-is-variable astnode) (node/expr/relation-name astnode)
                          ;(forge:Relation-name astnode)
                          (forge:Relation-sigs-thunks astnode) (forge:Relation-breaker astnode))]
+        [(node/expr/quantifier-var? astnode)
+         (node/expr/quantifier-var
+          new-info
+          (node/expr-arity astnode) (node/expr/quantifier-var-sym astnode) (node/expr/quantifier-var-name astnode))]
+        ; Annoyingly, structs aren't polymorphic in the way we need. This is not elegant, but:
+
+        ; join, transpose, +, -, &, ^, *, ->, sing, ', ++
+        [(node/expr/op/join? astnode) (rebuild-expr-op node/expr/op/join astnode new-info)]
+        [(node/expr/op/~? astnode) (rebuild-expr-op node/expr/op/~ astnode new-info)]
+        [(node/expr/op/+? astnode) (rebuild-expr-op node/expr/op/+ astnode new-info)]
+        [(node/expr/op/-? astnode) (rebuild-expr-op node/expr/op/- astnode new-info)]
+        [(node/expr/op/&? astnode) (rebuild-expr-op node/expr/op/& astnode new-info)]
+        [(node/expr/op/^? astnode) (rebuild-expr-op node/expr/op/^ astnode new-info)]
+        [(node/expr/op/*? astnode) (rebuild-expr-op node/expr/op/* astnode new-info)]
+        [(node/expr/op/->? astnode) (rebuild-expr-op node/expr/op/-> astnode new-info)]
+        [(node/expr/op/sing? astnode) (rebuild-expr-op node/expr/op/sing astnode new-info)]
+        [(node/expr/op/prime? astnode) (rebuild-expr-op node/expr/op/prime astnode new-info)]
+        [(node/expr/op/++? astnode) (rebuild-expr-op node/expr/op/++ astnode new-info)]
+
+        [(node/expr/ite? astnode)
+         (node/expr/ite new-info (node/expr-arity astnode)
+                        (node/expr/ite-condition astnode)
+                        (node/expr/ite-thene astnode)
+                        (node/expr/ite-elsee astnode))]
+        [(node/expr/fun-spacer? astnode)
+         (node/expr/fun-spacer new-info (node/expr-arity astnode)
+                               (node/expr/fun-spacer-name astnode)
+                               (node/expr/fun-spacer-args astnode)
+                               (node/expr/fun-spacer-codomain astnode)
+                               (node/expr/fun-spacer-expanded astnode))]
+        [(node/expr/comprehension? astnode)
+         (node/expr/comprehension new-info (node/expr-arity astnode)
+                                  (node/expr/comprehension-decls astnode)
+                                  (node/expr/comprehension-formula astnode))]
+        [(node/expr/constant? astnode)
+         (node/expr/constant new-info (node/expr-arity astnode) (node/expr/constant-type astnode))]
         [else astnode]))
 
+(define (rebuild-expr-op constructor astnode new-info)
+  (constructor new-info (node/expr-arity astnode) (node/expr/op-children astnode)))
 
 ; --------------------------
 ; these used to be define-simple-macro, but define-simple-macro doesn't

forge/last-checker.rkt

@@ -54,7 +54,18 @@
      (check-and-output formula node/formula/constant checker-hash #f)]
 
     [(node/fmla/pred-spacer info name args expanded)
-     (checkFormula run-or-state expanded quantvars checker-hash)]
+    (define domain-types (for/list ([arg args]) 
+                         (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 (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 "The sig(s) given as an argument to predicate ~a are of incorrect type" name)
+            #:context (apply-record-arg (list-ref args (cadr type))))
+            (void)))
+            arg-types)
+    (checkFormula run-or-state expanded quantvars checker-hash)]
 
     [(node/formula/op info args)
      (check-and-output formula
@@ -260,8 +271,12 @@
 ; 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)
-  (let ([output (checkExpression-mult run-or-state expr quantvars checker-hash)])
-    (car output)))
+;(printf "expr: ~a~n" expr)
+  (match expr 
+    [(? node/int?) (list (list 'Int))]
+    [(? integer?) (list (list 'Int))]
+    [_ (let ([output (checkExpression-mult run-or-state expr quantvars checker-hash)])
+         (car output))]))
 
 ; similar except that this is called from a formula, so in bsl 
 ; it should check that the multiplicity of the overall expr is 1 

forge/send-to-kodkod.rkt

@@ -635,6 +635,14 @@ Please declare a sufficient scope for ~a."
 
   (define all-atoms (append int-atoms sig-atoms))
 
+  ; for ease of understanding, just sort by first atom
+  (define (tuple<? t1 t2)
+    (cond [(and (symbol? t1) (symbol? t2))
+           (symbol<? (first t1) (first t2))]
+          [(and (number? t1) (number? t2))
+           (< (first t1) (first t2))]
+          [else (symbol? t1)]))
+
   ; Map<Symbol, bound>
   (define bounds-hash
     (for/hash ([sig (get-sigs run-spec)])
@@ -649,7 +657,9 @@ Please declare a sufficient scope for ~a."
         (unless (subset? (list->set lower) (list->set upper))
           (raise-run-error (format "Bounds inconsistency detected for sig ~a: lower bound was ~a, which is not a subset of upper bound ~a." (Sig-name sig) lower upper)
                            (get-blame-node run-spec sig)))
-        (values name (bound rel lower upper)))))
+        (values name (bound rel
+                            (sort (remove-duplicates lower) tuple<?)
+                            (sort (remove-duplicates upper) tuple<?))))))
 
 ;; Issue: one sig will overwrite with lower bound, but looking like that's empty if there's 
 ;;   an inst block that doesnt define it. Need to make that connection between default and provided.

forge/sigs-structs.rkt

@@ -414,12 +414,14 @@ Returns whether the given run resulted in sat or unsat, respectively.
 
 ; get-pred :: Run-or-State, Symbol -> Predicate
 ; Gets a predicate by name from a given state
+; Note that this will return the procedure, not the macro (no stx loc capture)
 (define (get-pred run-or-state name)
   (define state (get-state run-or-state))
   (hash-ref (State-pred-map state) name))
 
 ; get-fun :: Run-or-State, Symbol -> Function
 ; Gets a function by name from a given state
+; Note that this will return the procedure, not the macro (no stx loc capture)
 (define (get-fun run-or-state name)
   (define state (get-state run-or-state))
   (hash-ref (State-fun-map state) name))

forge/sigs.rkt

@@ -434,31 +434,65 @@
     [(pred pt:pred-type
            (~optional (#:lang check-lang) #:defaults ([check-lang #''checklangNoCheck]))
            name:id conds:expr ...+)
-     (with-syntax ([the-info #`(nodeinfo #,(build-source-location stx) check-lang)])
+     (with-syntax ([decl-info #`(nodeinfo #,(build-source-location stx) check-lang)]
+                   [inner-unsyntax #'unsyntax])
        (quasisyntax/loc stx
          (begin
-           ; use srcloc of actual predicate, not this location in sigs
-           ; "pred spacer" still present, even if no arguments, to consistently record use of a predicate
-           (define name
-             (pt.seal (node/fmla/pred-spacer the-info 'name '() (&&/info the-info conds ...))))
-           (update-state! (state-add-pred curr-state 'name name)))))]
+           ; - Use a macro in order to capture the location of the _use_.
+           ; For 0-arg predicates, produce the AST node immediately
+           (define-syntax (name stx2)
+             (syntax-parse stx2
+               [name
+                (quasisyntax/loc stx2
+                  ; - "pred spacer" still present, even if no arguments, to consistently record use of a predicate
+                  (let* ([the-info (nodeinfo (inner-unsyntax (build-source-location stx2)) check-lang)]
+                        [ast-node (pt.seal (node/fmla/pred-spacer the-info 'name '() (&&/info the-info conds ...)))])
+                    (update-state! (state-add-pred curr-state 'name ast-node))
+                    ast-node))])) )))]
 
     ; some decls: predicate must be called to evaluate it
     [(pred pt:pred-type
            (~optional (#:lang check-lang) #:defaults ([check-lang #''checklangNoCheck]))
            (name:id decls:param-decl-class  ...+) conds:expr ...+)
-     (with-syntax ([the-info #`(nodeinfo #,(build-source-location stx) check-lang)])
-       (quasisyntax/loc stx
-         (begin
-           ; "pred spacer" added to record use of predicate along with original argument declarations etc.           
-           (define (name decls.name ...)
-             (unless (or (integer? decls.name) (node/expr? decls.name) (node/int? decls.name))
-               (error (format "Argument '~a' to pred ~a was not a Forge expression, integer-expression, or Racket integer. Got ~v instead."
-                              'decls.name 'name decls.name)))
-             ...
-             (pt.seal (node/fmla/pred-spacer the-info 'name (list (apply-record 'decls.name decls.mexpr decls.name) ...)
-                                             (&&/info the-info conds ...))))                      
-           (update-state! (state-add-pred curr-state 'name name)))))]))
+     (with-syntax ([decl-info #`(nodeinfo #,(build-source-location stx) check-lang)]
+                   [inner-unsyntax #'unsyntax])
+       (define result-stx
+         (with-syntax ([functionname (format-id #'name "~a/func" #'name)])
+           (quasisyntax/loc stx
+             (begin
+               ; - Use a macro in order to capture the location of the _use_.
+
+               (define-syntax (name stx2)
+                 ;(printf "in macro: ~a~n" stx2)
+                 (syntax-parse stx2
+                   ; If it's the macro name and all the args, expand to an invocation of the procedure
+                   [(name args (... ...))
+                    (quasisyntax/loc stx2
+                      (functionname args (... ...) #:info (nodeinfo
+                                                           (inner-unsyntax (build-source-location stx2)) check-lang)))]
+                   ; If it's just the macro name, expand to a lambda that can take the same arguments when available
+                   [name:id
+                    (quasisyntax/loc stx2
+                      (lambda (decls.name ...)
+                        (functionname decls.name ...
+                                      #:info (nodeinfo
+                                              (inner-unsyntax (build-source-location stx2)) check-lang))))]
+                   ))
+
+               ; - "pred spacer" added to record use of predicate along with original argument declarations etc.
+               (define (functionname decls.name ... #:info [the-info #f])
+                 (unless (or (integer? decls.name) (node/expr? decls.name) (node/int? decls.name))
+                   (error (format "Argument '~a' to pred ~a was not a Forge expression, integer-expression, or Racket integer. Got ~v instead."
+                                  'decls.name 'name decls.name)))
+                 ...
+                 (pt.seal (node/fmla/pred-spacer the-info 'name (list (apply-record 'decls.name decls.mexpr decls.name) ...)
+                                                 (&&/info the-info conds ...))))
+
+
+
+
+               (update-state! (state-add-pred curr-state 'name functionname)))))) 
+       result-stx)]))
 
 (define/contract (repeat-product expr count)
   [@-> node/expr? number? node/expr?]
@@ -477,11 +511,28 @@
           (~optional (~seq #:codomain codomain:codomain-class)
                      #:defaults ([codomain.mexpr #'(mexpr (repeat-product univ (node/expr-arity result))
                                                           (if (> (node/expr-arity result) 1) 'set 'one))])))
+
      ; TODO: there is no check-lang in this macro; does that mean that language-level details are lost within a helper fun?
-     (with-syntax ([the-info #`(nodeinfo #,(build-source-location stx) 'checklangNoCheck)])
-       #'(begin
-           ; "fun spacer" added to record use of function along with original argument declarations etc.           
-           (define (name decls.name ...)
+
+     (with-syntax ([decl-info #`(nodeinfo #,(build-source-location stx) 'checklangNoCheck)]
+                   [functionname (format-id #'name "~a/func" #'name)]
+                   [inner-unsyntax #'unsyntax])
+       (quasisyntax/loc stx
+         (begin
+           ; - create a macro that captures the syntax location of the _use_
+           (define-syntax (name stx2)
+             (syntax-parse stx2
+               [(name args (... ...))
+                (quasisyntax/loc stx2
+                  (functionname args (... ...) #:info (nodeinfo
+                                                       (inner-unsyntax (build-source-location stx2)) 'checklangNoCheck)))]
+               [name:id
+                (quasisyntax/loc stx2
+                  (lambda (decls.name ...)
+                    (functionname decls.name ... #:info (nodeinfo (inner-unsyntax (build-source-location stx2)) 'checklangNoCheck))))]))
+
+           ; - "fun spacer" added to record use of function along with original argument declarations etc.           
+           (define (functionname decls.name ... #:info [the-info #f])
              (unless (or (integer? decls.name) (node/expr? decls.name) (node/int? decls.name))
                (error (format "Argument '~a' to fun ~a was not a Forge expression, integer-expression, or Racket integer. Got ~v instead."
                               'decls.name 'name decls.name)))
@@ -498,7 +549,7 @@
               (list (apply-record 'decls.name decls.mexpr decls.name) ...)
               codomain.mexpr
               safe-result))
-           (update-state! (state-add-fun curr-state 'name name))))]))
+           (update-state! (state-add-fun curr-state 'name name)))))]))
 
 ; Declare a new constant
 ; (const name value)

forge/tests/error/expect-fun-args.frg

@@ -0,0 +1,12 @@
+#lang forge/bsl
+option verbose 0 
+option run_sterling off
+abstract sig Player {}
+one sig X, O extends Player {}
+sig Board {board: pfunc Int -> Int -> Player}
+
+fun playerAt[b: Board, row, col: Int]: lone Player {
+  b.board[row][col] }
+
+test expect { should_error: { some playerAt } is sat }
+

forge/tests/error/expect-fun-no-args.frg

@@ -0,0 +1,11 @@
+#lang forge/bsl
+option verbose 0 
+option run_sterling off
+abstract sig Player {}
+one sig X, O extends Player {}
+sig Board {board: pfunc Int -> Int -> Player}
+
+fun xplayer: lone Player { X }
+
+test expect { should_error: { xplayer[O] = X } is sat }
+

forge/tests/error/formula_comprehension_cardinality.frg

@@ -10,4 +10,8 @@ pred problem {
     -- The parser thinks this looks like a constraint block! Expander needs
     -- to prevent this from making it to AST-creation.
     #{all a: A | a.i > 0} > 1
+}
+
+test expect {
+    should_error: {problem} is sat
 }

forge/tests/error/formula_comprehension_multiplicity.frg

@@ -10,4 +10,8 @@ pred problem {
     -- The parser thinks this looks like a constraint block! Expander needs
     -- to prevent this from making it to AST-creation.
     some {all a: A | a.i > 0}
+}
+
+test expect {
+    should_error: {problem} is sat
 }