Begin integrating typed Racket into core translation layer

.github/workflows/continuousIntegration.yml

@@ -21,7 +21,7 @@ jobs:
       uses: actions/checkout@v3
     - name: Install Forge
       run: |
-        raco pkg install --auto --no-docs ./forge ./froglet
+        raco pkg install --auto --no-docs ./forge
     - name: Run tests
       run: |
         cd forge/

forge/lang/ast.rkt

@@ -898,6 +898,11 @@
     (raise-forge-error
      #:msg (format "~a quantifier cannot use the same variable name more than once; used: ~a." quantifier vars)
      #:context info))
+  ; lone and one are desugared to either more basic quantifiers or to a multiplicity.
+  (unless (member quantifier '(some all no))
+    (raise-forge-error
+     #:msg (format "~a quantified-formula must be desugared first to some, all, or no." quantifier)
+     #:context info))
 
   (for ([e (in-list (map cdr decls))])
     (unless (node/expr? e)

forge/lang/bounds.rkt

@@ -1,16 +1,22 @@
-#lang racket/base
+#lang typed/racket/base
 
-(require racket/generator (only-in forge/lang/ast relation-arity))
-(require (only-in racket cartesian-product))
-(provide (all-defined-out))
+(require forge/types/ast-adapter)
+(require forge/shared)
 
+(provide (struct-out bound) (struct-out bounds) 
+           make-bound make-exact-bound exact-bound? make-upper-bound 
+           get-upper-bound bounds-variables bounds-union)
 
 ; A bound is a relation and two lists of tuples `lower` and `upper`.
-(struct bound (relation lower upper) #:transparent)
+(struct bound ([relation : node/expr/relation]
+               [lower : (Listof Tuple)]
+               [upper : (Listof Tuple)]) #:transparent)
 ; A bounds object is a universe and a collection of bound? instances.
-(struct bounds (universe entries) #:transparent)
+(struct bounds ([universe : (Listof FAtom)]
+                [entries : (Listof bound)]) #:transparent)
 
 ; Error-checking constructors for bounds
+(: make-bound (-> node/expr/relation (Listof Tuple) (Listof Tuple) bound))
 (define (make-bound relation lower upper)
   ;(printf "make-bound; upper was: ~a~n" upper)
   (for ([t (in-list lower)])
@@ -21,27 +27,43 @@
       (raise-arguments-error 'make-bound (format "upper bounds must contain tuples of arity ~a" (relation-arity relation)) "upper" t)))
   (bound relation lower upper))
 
+(: make-exact-bound (-> node/expr/relation (Listof Tuple) bound))
 (define (make-exact-bound relation contents)
   (make-bound relation contents contents))
+
+(: exact-bound? (-> bound Boolean))
 (define (exact-bound? b) (equal? (bound-lower b) (bound-upper b)))
 
+(: make-upper-bound (-> node/expr/relation (Listof Tuple) bound))
 (define (make-upper-bound relation contents)
   (make-bound relation '() contents))
 
-(define (make-product-bound relation col1 . columns)
-  (make-bound relation '() (apply cartesian-product col1 columns)))
+; (: make-product-bound (-> node/expr/relation (Listof Tuple) (Listof Tuple) * bound))
+; (define (make-product-bound relation col1 . columns)
+;   (define ub (apply cartesian-product col1 columns))
+;   (make-bound relation '() ub))
+
+;; for/first is not supported by the typechecker??
+;; but for/last is???
 
 ; Get the upper bound for a relation r in a bounds? object
+(: get-upper-bound (-> bounds node/expr/relation (Option (Listof Tuple))))
 (define (get-upper-bound bnds r)
-  (for/first ([b (in-list (bounds-entries bnds))] #:when (equal? (bound-relation b) r))
-    (bound-upper b)))
+  (for/or ([b (in-list (bounds-entries bnds))])
+    (if (equal? (bound-relation b) r) 
+        (bound-upper b)
+        #f)))
 
 ; get a list of all relations bound by a bounds? object
+(: bounds-variables (-> bounds (Listof Any)))
 (define (bounds-variables bnds)
-  (for/list ([b (in-list (bounds-entries bnds))]) (bound-relation b)))
+  (for/list : (Listof Any) ([b (in-list (bounds-entries bnds))]) (bound-relation b)))
 
 ; Combine several sets of bounds, which must be mutually disjoint and share the
 ; same universe
+(: bounds-union (-> bounds bounds))
 (define (bounds-union . lbnds)
   (define U (bounds-universe (car lbnds)))
-  (bounds U (for*/list ([bnds (in-list lbnds)][bnd (in-list (bounds-entries bnds))]) bnd)))
+  (bounds U (for*/list : (Listof bound) ([bnds (in-list lbnds)]
+                        [bnd (in-list (bounds-entries bnds))]) bnd)))
+

forge/lang/reader.rkt

@@ -9,7 +9,6 @@
          racket/pretty)
 (require forge/lang/alloy-syntax/parser)
 (require forge/lang/alloy-syntax/tokenizer)
-;(require (prefix-in log: forge/logging/2023/main))
 (require forge/shared)
 
 (do-time "forge/lang/reader")
@@ -113,16 +112,10 @@
       path port LANG-NAME CH ACH ICH EXTRA-REQUIRES (~optional INJECTED #:defaults ([INJECTED #''()])))
      (quasisyntax/loc stx
        (begin 
-         ;(define-values (logging-on? project email) (plog:setup LANG-NAME port path))
          (define compile-time (current-seconds))
          (define injected-if-any INJECTED)
          (define extra-requires EXTRA-REQUIRES)
 
-         ; We no longer do in-Forge logging.
-         ;(when logging-on?
-         ;  (uncaught-exception-handler (log:error-handler logging-on? compile-time (uncaught-exception-handler)))
-         ;  (log:register-run compile-time project LANG-NAME email path))
-
          (define parse-tree (parse path (make-tokenizer port)))
          (define ints-coerced (coerce-ints-to-atoms parse-tree))
 
@@ -138,10 +131,6 @@
                          ;; Used for the evaluator
                          (define-namespace-anchor forge:n) 
                          (forge:nsa forge:n)
-
-                         ; We no longer do in-Forge logging
-                         ;(require (prefix-in log: forge/logging/2023/main))
-                         ;(require (only-in racket printf uncaught-exception-handler))
 
                          ;; Set up language-specific error messages
                          (require forge/choose-lang-specific
@@ -151,10 +140,6 @@
                          (set-inst-checker-hash! ICH)
                          (set-check-lang! LANG-NAME)                  
 
-                         ;; Override default exception handler
-                         ;(uncaught-exception-handler
-                         ; (log:error-handler ',logging-on? ',compile-time (uncaught-exception-handler)))
-
                          ;; Add any code to inject before the model is expanded
                          ,@injected-if-any
                          ;; Expanded model, etc.
@@ -175,9 +160,6 @@
                          (module+ main
                            ; Invoke the execs submodule
                            (require (submod ".." execs)))                                    
-
-                         ; We no longer do in-Forge logging
-                         ;(log:flush-logs ',compile-time "no-error")
                          ))
 
          (define module-datum `(module forge-mod forge/lang/expander