Add basic typechecking for helper functions (#248)

* feat: func typechecks added

* Error message updated and deprimify prototype

* first attempt at DFS

* feat: added deprimify

* change deprimify to use values

---------

Co-authored-by: k-mouline <karim_mouline@brown.edu>

forge/last-checker.rkt

@@ -56,12 +56,21 @@
     [(node/fmla/pred-spacer info name args expanded)
     (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)
+            #: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)
@@ -268,6 +277,35 @@
                                 "_remainder")))
                          all-primitive-descendants)])])))
 
+(define (dfs-sigs run-or-state func sigs init-acc)
+    (define (dfs-sigs-helper todo acc)
+      (cond [(equal? (length todo) 0) acc]
+      [else (define next (first todo))
+      (define-values (new-acc stop)
+        (func next acc)) ; use define-values with the return of func
+        (cond [stop (dfs-sigs-helper (rest todo) new-acc)]
+              [else (define next-list (if (empty? (get-children run-or-state next)) ; empty?
+                                      (rest todo)
+                                      (append (get-children run-or-state next) (rest todo)))) ; append instead
+              (dfs-sigs-helper next-list new-acc)])]))
+    (dfs-sigs-helper sigs init-acc)) ; maybe take in initial accumulator as well for more flexibility
+
+(define (deprimify run-or-state primsigs)
+  (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]
+      [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 final-list (dfs-sigs run-or-state pseudo-fold-lambda top-level '()))
+            final-list])))
+
 ; 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)
@@ -324,8 +362,33 @@
                        (cons (map list (primify run-or-state 'univ))
                              #t))]
 
-    [(node/expr/fun-spacer info arity name args result expanded)
+    [(node/expr/fun-spacer info arity name args codomain expanded)
        ; be certain to call the -mult version, or the multiplicity will be thrown away.
+      (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 "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)
+      (define output-type (checkExpression run-or-state expanded quantvars checker-hash))
+      (if (not (member (car output-type) (checkExpression run-or-state (mexpr-expr codomain) quantvars checker-hash)))
+          (raise-forge-error
+          #:msg (format "The output of function ~a is of incorrect type" name)
+          #:context expanded)
+          (void))
        (checkExpression-mult run-or-state expanded quantvars checker-hash)]
 
     [(node/expr/ite info arity a b c)
@@ -406,6 +469,11 @@
 (define (keep-only keepers pool)
   (filter (lambda (ele) (member ele keepers)) pool))
 
+; (struct/contract expression-type (
+;   [multiplicity any/c]
+;   [type (listof (listof symbol?))]
+;   [temporal-possibility boolean?]))
+
 (define/contract (checkExpressionOp run-or-state expr quantvars args checker-hash)
   (@-> (or/c Run? State? Run-spec?) node/expr/op? list? (listof (or/c node/expr? node/int?)) hash?   
        any)

forge/tests/error/main.rkt

@@ -150,14 +150,27 @@
 
     (list "parsing_less_dash.frg" #rx"Negative numbers must not have blank space between the minus")
 
-    ;;; Mismatched type tests
-    (list "mismatched-arg-type-basic.frg" #rx"The sig\\(s\\) given as an argument to predicate p2 are of incorrect type")
-    (list "mismatched-arg-type-basic-univ.frg" #rx"The sig\\(s\\) given as an argument to predicate p2 are of incorrect type")
-    (list "mismatched-arg-type-arity.frg" #rx"The sig\\(s\\) given as an argument to predicate p2 are of incorrect type")
-    (list "mismatched-arg-type-no-quant.frg" #rx"The sig\\(s\\) given as an argument to predicate p1 are of incorrect type")
-    (list "mismatched-arg-type-no-quant2.frg" #rx"The sig\\(s\\) given as an argument to predicate p2 are of incorrect type")
-    (list "mismatched-arg-type-non-primsig.frg" #rx"The sig\\(s\\) given as an argument to predicate p2 are of incorrect type")
-    (list "mismatched-arg-type-non-primsig2.frg" #rx"The sig\\(s\\) given as an argument to predicate p are of incorrect type")
+    ;; 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\\)")
+
+    ;; 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-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")
+    (list "mismatched-arg-type-fun-output-non-primsig.frg" #rx"The output of function f is of incorrect type")
+    (list "mismatched-arg-type-fun-univ-output.frg" #rx"The output of function f is of incorrect type")
+    (list "mismatched-arg-type-fun-output-int.frg" #rx"The output of function f is of incorrect type")
+    (list "mismatched-arg-type-fun-codomain-int.frg" #rx"The output of function f is of incorrect type")
   ))
 
 

forge/tests/error/mismatched-arg-type-fun-arity.frg

@@ -0,0 +1,12 @@
+#lang forge/bsl
+
+sig A { f1: lone B }
+sig B { f2: lone A } 
+
+fun f[b: B, a: A] : lone B {
+    a.f1
+}
+
+test expect {
+    should_error: {some b1, b2: B | f[b1, b2] = b2} is sat
+}

forge/tests/error/mismatched-arg-type-fun-codomain-int.frg

@@ -0,0 +1,12 @@
+#lang forge/bsl
+
+sig A { f1: lone B }
+sig B { f2: lone A } 
+
+fun f[a: A] : Int {
+   a.f1
+}
+
+test expect {
+    should_error: {some a: A | f[a] = a} is sat
+}

forge/tests/error/mismatched-arg-type-fun-codomain-non-primsig.frg

@@ -0,0 +1,12 @@
+#lang forge/bsl
+
+sig A { f1: lone B }
+one sig B { f2: lone A }
+
+fun f[a: A] : B {
+   a
+}
+
+test expect {
+    should_error: {some a: A | f[a] = a} is sat
+}

forge/tests/error/mismatched-arg-type-fun-codomain.frg

@@ -0,0 +1,12 @@
+#lang forge/bsl
+
+sig A { f1: lone B }
+sig B { f2: lone A } 
+
+fun f[a: A] : lone B {
+   a
+}
+
+test expect {
+    should_error: {some a: A | f[a] = a} is sat
+}

forge/tests/error/mismatched-arg-type-fun-output-int.frg

@@ -0,0 +1,12 @@
+#lang forge/bsl
+
+sig A { f1: lone B }
+sig B { f2: lone A } 
+
+fun f[a: A] : lone A {
+   3
+}
+
+test expect {
+    should_error: {some a: A | f[a] = a} is sat
+}

forge/tests/error/mismatched-arg-type-fun-output-non-primsig.frg

@@ -0,0 +1,12 @@
+#lang forge/bsl
+
+sig A { f1: lone B }
+one sig B { f2: lone A }
+
+fun f[a: A] : lone A {
+   B
+}
+
+test expect {
+    should_error: {some a: A | f[a] = a} is sat
+}

forge/tests/error/mismatched-arg-type-fun-output.frg

@@ -0,0 +1,12 @@
+#lang forge/bsl
+
+sig A { f1: lone B }
+sig B { f2: lone A } 
+
+fun f[a: A] : lone A {
+   a.f1
+}
+
+test expect {
+    should_error: {some a: A | f[a] = a} is sat
+}

forge/tests/error/mismatched-arg-type-fun-univ-output.frg

@@ -0,0 +1,12 @@
+#lang forge/bsl
+
+sig A { }
+
+fun f[a: A] : lone A {
+   univ
+}
+
+test expect {
+    should_error: {some a: A | f[a] = a} is sat
+}
+

forge/tests/error/mismatched-arg-type-fun.frg

@@ -0,0 +1,12 @@
+#lang forge/bsl
+
+sig A { f1: lone B }
+sig B { f2: lone A } 
+
+fun f[a: A] : lone B {
+    a.f1
+}
+
+test expect {
+    should_error: {some b: B | f[b] = b} is sat
+}

forge/tests/error/tree-type-error.frg

@@ -0,0 +1,16 @@
+#lang forge
+
+sig A{ }
+sig A_child1 extends A { } 
+sig A_child2 extends A {}
+sig B { }
+sig B_child1 extends B { }
+sig B_child2 extends B { }
+sig B_child1_child extends B_child1 { }
+pred p[a: B_child1 + A] {
+}
+
+
+test expect {
+    practicing: {some x: B_child2 | p[x]} is sat
+}