diff --git a/.github/workflows/continuousIntegration.yml b/.github/workflows/continuousIntegration.yml index 0d6c2ba3f..96ab34f0c 100644 --- a/.github/workflows/continuousIntegration.yml +++ b/.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/ diff --git a/forge/logging/2022/README.md b/OLD/logging/2022/README.md similarity index 100% rename from forge/logging/2022/README.md rename to OLD/logging/2022/README.md diff --git a/forge/logging/2022/index.js b/OLD/logging/2022/index.js similarity index 100% rename from forge/logging/2022/index.js rename to OLD/logging/2022/index.js diff --git a/forge/logging/2022/main.rkt b/OLD/logging/2022/main.rkt similarity index 100% rename from forge/logging/2022/main.rkt rename to OLD/logging/2022/main.rkt diff --git a/forge/logging/2022/package.js b/OLD/logging/2022/package.js similarity index 100% rename from forge/logging/2022/package.js rename to OLD/logging/2022/package.js diff --git a/forge/logging/2022/schema.sql b/OLD/logging/2022/schema.sql similarity index 100% rename from forge/logging/2022/schema.sql rename to OLD/logging/2022/schema.sql diff --git a/forge/logging/2023/README.md b/OLD/logging/2023/README.md similarity index 100% rename from forge/logging/2023/README.md rename to OLD/logging/2023/README.md diff --git a/forge/logging/2023/index.js b/OLD/logging/2023/index.js similarity index 100% rename from forge/logging/2023/index.js rename to OLD/logging/2023/index.js diff --git a/forge/logging/2023/main.rkt b/OLD/logging/2023/main.rkt similarity index 100% rename from forge/logging/2023/main.rkt rename to OLD/logging/2023/main.rkt diff --git a/forge/logging/2023/package.js b/OLD/logging/2023/package.js similarity index 100% rename from forge/logging/2023/package.js rename to OLD/logging/2023/package.js diff --git a/forge/logging/2023/schema.sql b/OLD/logging/2023/schema.sql similarity index 100% rename from forge/logging/2023/schema.sql rename to OLD/logging/2023/schema.sql diff --git a/forge/logging/check-ex-spec/README.md b/OLD/logging/check-ex-spec/README.md similarity index 100% rename from forge/logging/check-ex-spec/README.md rename to OLD/logging/check-ex-spec/README.md diff --git a/forge/logging/check-ex-spec/index.js b/OLD/logging/check-ex-spec/index.js similarity index 100% rename from forge/logging/check-ex-spec/index.js rename to OLD/logging/check-ex-spec/index.js diff --git a/forge/logging/check-ex-spec/main.rkt b/OLD/logging/check-ex-spec/main.rkt similarity index 100% rename from forge/logging/check-ex-spec/main.rkt rename to OLD/logging/check-ex-spec/main.rkt diff --git a/forge/logging/check-ex-spec/package.js b/OLD/logging/check-ex-spec/package.js similarity index 100% rename from forge/logging/check-ex-spec/package.js rename to OLD/logging/check-ex-spec/package.js diff --git a/forge/logging/check-ex-spec/schema.sql b/OLD/logging/check-ex-spec/schema.sql similarity index 100% rename from forge/logging/check-ex-spec/schema.sql rename to OLD/logging/check-ex-spec/schema.sql diff --git a/forge/logging/google-cloud-function.py b/OLD/logging/google-cloud-function.py similarity index 100% rename from forge/logging/google-cloud-function.py rename to OLD/logging/google-cloud-function.py diff --git a/forge/logging/logging.rkt b/OLD/logging/logging.rkt similarity index 100% rename from forge/logging/logging.rkt rename to OLD/logging/logging.rkt diff --git a/forge/logging/requirements.txt b/OLD/logging/requirements.txt similarity index 100% rename from forge/logging/requirements.txt rename to OLD/logging/requirements.txt diff --git a/forge/logging/schema.sql b/OLD/logging/schema.sql similarity index 100% rename from forge/logging/schema.sql rename to OLD/logging/schema.sql diff --git a/forge/logging/sigs.rkt b/OLD/logging/sigs.rkt similarity index 100% rename from forge/logging/sigs.rkt rename to OLD/logging/sigs.rkt diff --git a/forge/breaks.rkt b/forge/breaks.rkt index 75378f6a3..9468c6d04 100644 --- a/forge/breaks.rkt +++ b/forge/breaks.rkt @@ -1,29 +1,53 @@ -#lang racket/base +#lang typed/racket/base/optional ; This module is concerned with "is linear" and other such "breaker" bind expressions. -(require forge/lang/bounds (prefix-in @ forge/lang/ast)) +(require forge/lang/bounds) ;; TYPED +(require forge/types/ast-adapter) ;; TYPED, contains needed AST functions (not macros) +(require forge/shared) + +(require/typed typed/racket + ; Missing from typed racket's definitions as of 2025-oct-31. + [set-subtract! (All (T) (-> (Setof T) (Setof T) Void))] + [set-add! (All (T) (-> (Setof T) T Void))] + [set-union! (All (T) (-> (Setof T) (Setof T) Void))] + [mutable-set (All (T) (T * -> (Setof T)))] + [set-remove! (All (T) (-> (Setof T) T Void))] + [list->mutable-set (All (T) (-> (U (Listof T) (Setof T)) (Setof T)))] + ; Present in typed racket's definitions + [hash-set! (All (K V) (-> (HashTable K V) K V Void))] + ) + (require predicates) -(require (only-in racket false true set set-union set-intersect set->list list->set set? first rest - cartesian-product empty empty? set-add! mutable-set in-set subset? - set-subtract! set-map list->mutable-set set-remove! append* set-member? - set-empty? set-union! drop-right take-right for/set for*/set filter-not - second set-add match identity) - racket/contract - racket/hash) -(require (only-in forge/shared get-verbosity VERBOSITY_HIGH)) - -(provide constrain-bounds (rename-out [break-rel break]) break-bound break-formulas) +(require (only-in typed/racket + false true set set-union set-intersect set->list list->set set? first + rest cartesian-product empty empty? in-set subset? + set-map append* set-member? + set-empty? drop-right take-right for/set for*/set filter-not + second set-add match identity)) +(require/typed forge/shared + [get-verbosity (-> Integer)] + [VERBOSITY_HIGH Integer]) + +(provide constrain-bounds break-rel break-bound break-formulas) (provide (rename-out [add-instance instance]) clear-breaker-state) (provide make-exact-sbound) (provide (struct-out sbound)) +; The `rel` parameter needs to allow for join arguments, not just relations. +(define-type StrategyFunction + (->* (Integer node/expr bound (Listof Tuple) (Listof node/expr/relation)) + ((U srcloc #f)) + breaker)) + ;;;;;;;;;;;;;; ;;;; util ;;;; ;;;;;;;;;;;;;; +(: int-add1 (-> Integer Integer)) +(define (int-add1 x) (+ x 1)) (define-syntax-rule (cons! xs x) (set! xs (cons x xs))) -(define-syntax-rule (add1! x) (begin (set! x (add1 x)) x)) +(define-syntax-rule (add1! x) (begin (set! x (int-add1 x)) x)) ;;;;;;;;;;;;;;;; ;;;; breaks ;;;; @@ -31,18 +55,30 @@ ; An "sbound" is nearly identical to the "bound" struct defined in forge/lang/bounds, ; except that it contains sets rather than lists. #f is permitted to denote a lack of value. -(struct/contract sbound ([relation any/c] - [lower (or/c #f set?)] - [upper (or/c #f set?)]) #:transparent) - -(define (make-sbound relation lower [upper false]) (sbound relation lower upper)) +; Also, it may represent a bound on a _join_, not just a relation. This is not the case for "bound". +(struct sbound + ([relation : node/expr] + [lower : (Setof Tuple)] + [upper : (Setof Tuple)]) #:transparent) + +(: make-sbound (->* (node/expr/relation (Setof Tuple)) ((Setof Tuple)) sbound)) +(define (make-sbound relation lower [upper : (Setof Tuple) (set)]) + (sbound relation lower upper)) +(: make-exact-sbound (-> node/expr/relation (Setof Tuple) sbound)) (define (make-exact-sbound relation s) (sbound relation s s)) -(struct break (sbound formulas) #:transparent) -(define (make-break sbound [formulas (set)]) (break sbound formulas)) + +;; N.B. Not to be confused with node/breaking/break +(struct break ([sbound : sbound] + [formulas : (Setof node/formula)]) + #:transparent) + +(: make-break (-> sbound (Setof node/formula) break)) +(define (make-break sbound [formulas : (Setof node/formula) (set)]) (break sbound formulas)) ; sigs :: set ; edges :: set> -(struct break-graph (sigs edges) #:transparent) +(struct break-graph ([sigs : (Setof node/expr/relation)] + [edges : (Setof (Setof node/expr/relation))]) #:transparent) ; pri :: Nat ; break-graph :: break-graph @@ -54,76 +90,111 @@ ; BEGIN INSERTED TEMPORARY FIX FOR 'FUNC (struct breaker ( ; priority level of the breaker - pri - break-graph - make-break - make-default - [use-formula #:auto #:mutable]) - #:transparent #:auto-value #f) - + [pri : Integer] + [break-graph : break-graph] + [make-break : (-> break)] + [make-default : (-> break)] + [use-formula : Boolean ]) + #:transparent #:mutable) + +(: formula-breaker (-> Integer break-graph (-> break) (-> break) breaker)) (define (formula-breaker pri break-graph make-break make-default) - (define res (breaker pri break-graph make-break make-default)) + (define res (breaker pri break-graph make-break make-default #f)) (set-breaker-use-formula! res #t) res) ; END INSERTED TEMPORARY FIX FOR 'FUNC +(: bound->sbound (-> bound sbound)) (define (bound->sbound bound) (make-sbound (bound-relation bound) (list->set (bound-lower bound)) (list->set (bound-upper bound)))) +(: sbound->bound (-> sbound bound)) (define (sbound->bound sbound) - (make-bound (sbound-relation sbound) + (if (node/expr/relation? (sbound-relation sbound)) + (make-bound (sbound-relation sbound) (set->list (sbound-lower sbound)) - (set->list (sbound-upper sbound)))) + (set->list (sbound-upper sbound))) + (raise (format "Internal error: sbound->bound called on non-relation. sbound=~a" sbound)))) + +(: bound->break (-> bound break)) (define (bound->break bound) (break (bound->sbound bound) (set))) +(: break-lower (-> break (Setof Tuple))) (define break-lower (compose sbound-lower break-sbound)) +(: break-upper (-> break (Setof Tuple))) (define break-upper (compose sbound-upper break-sbound)) +(: break-relation (-> break node/expr)) (define break-relation (compose sbound-relation break-sbound)) -(define break-bound (compose sbound->bound break-sbound)) - -(define (sbound+ . sbounds) - (make-bound (break-relation (first sbounds)) ; TODO: assert all same relations - (apply set-union (map break-lower sbounds)) - (apply set-intersect (map break-lower sbounds)))) -(define (break+ . breaks) - (make-break (apply sbound+ breaks) - (apply set-union (map break-formulas breaks)))) - -(define (make-exact-break relation contents [formulas (set)]) +(: break-bound (-> break bound)) +(define break-bound (compose sbound->bound break-sbound)) + +; (: sbound+ (-> (Listof sbound) bound)) +; (define (sbound+ sbounds) +; ; TODO: assert all same relations +; (make-bound (break-relation (first sbounds)) +; (apply set-union (map break-lower sbounds)) +; (apply set-intersect (map break-lower sbounds)))) + +; (: break+ (-> (Listof break) break)) +; (define (break+ . breaks) +; (make-break (sbound+ breaks) +; (apply set-union (map break-formulas breaks)))) + +(: make-exact-break (-> node/expr (Setof Tuple) (Setof node/formula) break)) +(define (make-exact-break relation contents [formulas : (Setof node/formula) (set)]) (break (sbound relation contents contents) formulas)) -(define (make-upper-break relation contents [formulas (set)]) + +(: make-upper-break (->* (node/expr/relation (Setof Tuple)) ((Setof node/formula)) break)) +(define (make-upper-break relation contents [formulas : (Setof node/formula) (set)]) (break (sbound relation (set) contents) formulas)) -(define (make-lower-break relation contents atom-lists [formulas (set)]) - (break (sbound relation contents (apply cartesian-product atom-lists)) formulas)) + +(: make-lower-break (-> node/expr/relation (Setof Tuple) (Listof Tuple) (Setof node/formula) break)) +(define (make-lower-break relation contents atom-lists [formulas : (Setof node/formula) (set)]) + (break (sbound relation contents (list->set (apply cartesian-product atom-lists))) formulas)) ;;;;;;;;;;;;;; ;;;; data ;;;; ;;;;;;;;;;;;;; ; symbol |-> (pri rel bound atom-lists rel-list) -> breaker +(: strategies (HashTable Symbol StrategyFunction)) (define strategies (make-hash)) + ; compos[{a₀,...,aᵢ}] = b => a₀+...+aᵢ = b +(: compos (Mutable-HashTable (Setof Symbol) Symbol)) (define compos (make-hash)) + ; a ∈ upsets[b] => a > b +(: upsets (Mutable-HashTable Symbol (Setof Symbol))) (define upsets (make-hash)) + ; a ∈ downsets[b] => a < b +(: downsets (Mutable-HashTable Symbol (Setof Symbol))) (define downsets (make-hash)) ; list of partial instance breakers +(: instances (Listof sbound)) (define instances (list)) + ; a ∈ rel-breaks[r] => "user wants to break r with a" +(: rel-breaks (Mutable-HashTable node/expr/relation (Setof node/breaking/break))) (define rel-breaks (make-hash)) + ; rel-break-pri[r][a] = i => "breaking r with a has priority i" +(: rel-break-pri (Mutable-HashTable node/expr/relation (Mutable-HashTable node/breaking/break Integer))) (define rel-break-pri (make-hash)) + ; priority counter +(: pri_c Integer) (define pri_c 0) ; clear all state +(: clear-breaker-state (-> Void)) (define (clear-breaker-state) (set! instances empty) - (set! rel-breaks (make-hash)) - (set! rel-break-pri (make-hash)) + (set! rel-breaks (ann (make-hash) (Mutable-HashTable node/expr/relation (Setof node/breaking/break)))) + (set! rel-break-pri (ann (make-hash) (Mutable-HashTable node/expr/relation (Mutable-HashTable node/breaking/break Integer)))) (set! pri_c 0)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -131,33 +202,39 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; h :: type(k) |-> set +(: hash-add! (All (K V2) (-> (HashTable K (Setof V2)) K V2 Void))) (define (hash-add! h k v) (if (hash-has-key? h k) (set-add! (hash-ref h k) v) (hash-set! h k (mutable-set v)))) ; h :: type(k1) |-> type(k2) |-> type(v) +(: hash-add-set! (All (K1 K2 V) (-> (Mutable-HashTable K1 (Mutable-HashTable K2 V)) K1 K2 V Void))) (define (hash-add-set! h k1 k2 v) - (unless (hash-has-key? h k1) (hash-set! h k1 (make-hash))) + (unless (hash-has-key? h k1) (hash-set! h k1 (ann (make-hash) (Mutable-HashTable K2 V)))) (define h_k1 (hash-ref h k1)) - (unless (hash-has-key? h_k1 k2) (hash-set! h_k1 k2 pri_c))) + ;; CHANGED pri_c to v. + ;(unless (hash-has-key? h_k1 k2) (hash-set! h_k1 k2 pri_c))) + (unless (hash-has-key? h_k1 k2) (hash-set! h_k1 k2 v))) ; strategy :: () -> breaker +(: add-strategy (-> Symbol StrategyFunction Void)) (define (add-strategy a strategy) (hash-set! strategies a strategy) (hash-add! upsets a a) ;; a > a (hash-add! downsets a a)) ;; a < a + +(: equiv (-> Symbol Symbol * Any)) (define (equiv a . bs) (hash-set! compos (apply set bs) a) (apply stricter a bs) ; TODO: if no fn defined for a, default to naively doing all bs - #|(unless (hash-has-key? strategies a) + #;(unless (hash-has-key? strategies a) (hash-set! strategies a (λ (rel atom-lists rel-list) (apply break+ (for ([b bs]) - ((hash-ref strategies b) atom-lists) - )) - )))|# + ((hash-ref strategies b) atom-lists) )) ))) ) +(: dominate (-> Symbol Symbol Void)) (define (dominate a b) (define upa (hash-ref upsets a)) (define downb (hash-ref downsets b)) @@ -172,7 +249,9 @@ (hash-set! compos (set a x) a) ;; a = a + x ) ) +(: stricter (-> Symbol Symbol * Void)) (define (stricter a . bs) (for ([b bs]) (dominate a b))) +(: weaker (-> Symbol Symbol * Void)) (define (weaker a . bs) (for ([b bs]) (dominate b a))) ; TODO: allow syntax like (declare 'a 'b > 'c 'd > 'e 'f) @@ -182,58 +261,68 @@ [(_ a < bs ...) (weaker a bs ...)] [(_ a = bs ...) (equiv a bs ...)])) +(: min-breaks! (-> (Setof node/breaking/break) (Mutable-HashTable node/breaking/break Integer) Void)) (define (min-breaks! breaks break-pris) - (define changed false) - (hash-for-each compos (λ (k v) + (define changed (ann false Boolean)) + (hash-for-each compos (λ ([k : (Setof Symbol)] [v : Symbol]) (when (subset? k breaks) (set-subtract! breaks k) (set-add! breaks v) ; new break should have priority of highest priority component - (define max-pri (apply min - (set-map k (lambda (s) (hash-ref break-pris s))))) - (hash-set! break-pris v max-pri) + (define pris (ann (set-map k (lambda ([s : Symbol]) + (hash-ref break-pris (node/breaking/break empty-nodeinfo s)))) (Listof Integer))) + (define min-pri (apply min pris)) ; was max-pri (typo?) + (hash-set! break-pris (node/breaking/break empty-nodeinfo v) min-pri) (set! changed true)) )) (when changed (min-breaks! breaks break-pris)) ) -; renamed-out to 'break for use in forge -(define/contract (break-rel rel . breaks) - (-> @node/expr? (or/c symbol? @node/breaking/break?) - void?) +(: break-rel (->* (node/expr/relation) () #:rest (U Symbol node/breaking/break) Void)) +(define (break-rel rel . breaks) (for ([break breaks]) - (define break-key - (cond [(symbol? break) break] - [(@node/breaking/break? break) (@node/breaking/break-break break)] - [else (@raise-forge-error #:msg (format "Not a valid break name: ~a~n" break) #:context #f)])) + (: break-key Symbol) + (: break-node node/breaking/break) + (define-values (break-key break-node) + (cond [(symbol? break) (values break (node/breaking/break empty-nodeinfo break))] + [(node/breaking/break? break) (values (node/breaking/break-break break) break)] + [else (raise (format "Not a value break or break name: ~a" break))])) (unless (hash-has-key? strategies break-key) (error (format "break not implemented among ~a" strategies) break-key)) - (hash-add! rel-breaks rel break) - (hash-add-set! rel-break-pri rel break (add1! pri_c)))) -(define (add-instance i) (cons! instances i)) - -(define (constrain-bounds total-bounds sigs bounds-store relations-store extensions-store) + (hash-add! rel-breaks rel break-node) + (hash-add-set! rel-break-pri rel break-node (add1! pri_c)))) + +(: add-instance (-> sbound Void)) +(define (add-instance i) (cons! instances i)) + +(: constrain-bounds (-> (Listof bound) + (Listof node/expr/relation) + (HashTable node/expr/relation (Listof FAtom)) + (HashTable node/expr/relation (Listof node/expr/relation)) + (HashTable node/expr/relation node/expr/relation) + (Values (Listof bound) (Listof node/formula)))) +(define (constrain-bounds total-bounds maybe-list-sigs bounds-store relations-store extensions-store) (define name-to-rel (make-hash)) - (hash-for-each relations-store (λ (k v) (hash-set! name-to-rel (@node/expr/relation-name k) k))) - (for ([s sigs]) (hash-set! name-to-rel (@node/expr/relation-name s) s)) + (hash-for-each relations-store (λ ([k : node/expr/relation] v) (hash-set! name-to-rel (node/expr/relation-name k) k))) + (for ([s maybe-list-sigs]) (hash-set! name-to-rel (node/expr/relation-name s) s)) ; returns (values new-total-bounds (set->list formulas)) - (define new-total-bounds (list)) - (define formulas (mutable-set)) + (define new-total-bounds (ann (list) (Listof bound))) + (define formulas (ann (mutable-set) (Setof node/formula))) ; unextended sets - (set! sigs (list->mutable-set sigs)) + (define sigs (list->mutable-set maybe-list-sigs)) ; maintain non-transitive reachability relation - (define reachable (make-hash)) + (define reachable (ann (make-hash) (Mutable-HashTable (U node/expr/relation Symbol) + (Setof (U node/expr/relation Symbol))))) (hash-set! reachable 'broken (mutable-set 'broken)) (for ([sig sigs]) (hash-set! reachable sig (mutable-set sig))) (hash-for-each extensions-store (λ (k v) (set-remove! sigs v))) - ; First add all partial instances. - (define instance-bounds (append* (for/list ([i instances]) - (if (sbound? i) (list i) (xml->breakers i name-to-rel))))) + ; First add all partial instances. + ; This is not obsolete! The breakers need to "play nicely" with user-defined `inst`s. (define defined-relations (mutable-set)) - (for ([b instance-bounds]) + (for ([b instances]) (define rel-inst (sbound-relation b)) (for ([bound total-bounds]) (define rel (bound-relation bound)) @@ -244,63 +333,76 @@ (cons! new-total-bounds (sbound->bound b)) (cons! new-total-bounds bound)) (set-add! defined-relations rel) - (define typelist ((@node/expr/relation-typelist-thunk rel))) + (define typelist ((node/expr/relation-typelist-thunk rel))) (for ([t typelist]) (when (hash-has-key? name-to-rel t) (set-remove! sigs (hash-ref name-to-rel t)))))))) ; proposed breakers from each relation - (define candidates (list)) + (define candidates (ann (list) (Listof breaker))) (for ([bound total-bounds]) ; get declared breaks for the relation associated with this bound - (define rel (bound-relation bound)) - (define breaks (hash-ref rel-breaks rel (set))) - (define break-pris (hash-ref rel-break-pri rel (make-hash))) + (define rel (bound-relation bound)) + + (define breaks (hash-ref rel-breaks rel (ann (lambda () (set)) (-> (Setof node/breaking/break)) ))) + (define backup (ann (lambda () (make-hash)) (-> (Mutable-HashTable node/breaking/break Integer)))) + (define break-pris (ann (hash-ref rel-break-pri rel backup) (Mutable-HashTable node/breaking/break Integer))) + ; compose breaks (min-breaks! breaks break-pris) - ;(printf "bound in total-bounds: ~a~n" bound) + (define defined (set-member? defined-relations rel)) (cond [(set-empty? breaks) (unless defined (cons! new-total-bounds bound)) ][else (unless (hash-has-key? relations-store rel) - (@raise-forge-error #:msg (format "Attempted to set or modify bounds of ~a, but the annotation given was of the wrong form (sig vs. field).~n" rel) - #:context #f)) - (define rel-list (hash-ref relations-store rel)) - (define atom-lists (map (λ (b) (hash-ref bounds-store b)) rel-list)) + (raise-forge-error #:msg (format "Attempted to set or modify bounds of ~a, but the annotation given was of the wrong form (sig vs. field).~n" rel) + #:context #f + #:raise? #t)) + (define rel-list (ann (hash-ref relations-store rel) (Listof node/expr/relation))) + (define atom-lists (map (λ ([b : node/expr/relation]) + (define sym-list (ann (hash-ref bounds-store b (lambda () (list))) (Listof FAtom))) + (hash-ref bounds-store b)) rel-list)) ; make all breakers - (define breakers (for/list ([break (set->list breaks)]) - (define break-sym - (cond [(symbol? break) break] - [(@node/breaking/break? break) (@node/breaking/break-break break)] - [else (@raise-forge-error #:msg (format "constrain-bounds: not a valid break name: ~a~n" break) - #:context #f)])) - (define loc (if (@node? break) - (@nodeinfo-loc (@node-info break)) + ;; break is a "break", strategy returns a "breaker" + + (define breakers (map (lambda ([b : (U node/breaking/break Symbol)]) + (define-values (break-sym break-node) + (cond [(symbol? b) (values b (node/breaking/break empty-nodeinfo b))] + [(node/breaking/break? b) (values (node/breaking/break-break b) b)] + [else (raise-forge-error #:msg (format "constrain-bounds: not a valid break name: ~a~n" break) + #:context #f + #:raise? #t)])) + (define loc (if (node? b) + (nodeinfo-loc (node-info b)) #f)) - (define strategy (hash-ref strategies break-sym)) - (define pri (hash-ref break-pris break)) - (strategy pri rel bound atom-lists rel-list loc))) - (set! breakers (sort breakers < #:key breaker-pri)) + (define strategy (ann (hash-ref strategies break-sym) StrategyFunction)) + ; What if it's a symbol instead of a break?? check dev !!!! b could be maybe + (define pri (ann (hash-ref break-pris break-node) Integer)) + (strategy pri rel bound atom-lists rel-list loc)) + (set->list breaks))) + + (set! breakers (sort breakers (lambda ([x : breaker] [y : breaker]) + (< (breaker-pri x) (breaker-pri y))))) ; propose highest pri breaker that breaks only leaf sigs ; break the rest the default way (with get-formulas) (define broken defined) - (for ([breaker breakers]) - (cond [(or broken (breaker-use-formula breaker)) - (define default ((breaker-make-default breaker))) + (for ([bkr breakers]) + (cond [(or broken (breaker-use-formula bkr)) + (define default ((breaker-make-default bkr))) (set-union! formulas (break-formulas default)) ][else - (define break-graph (breaker-break-graph breaker)) + (define break-graph (breaker-break-graph bkr)) (define broken-sigs (break-graph-sigs break-graph)) (cond [(subset? broken-sigs sigs) - (cons! candidates breaker) + (cons! candidates bkr) (set! broken #t) ][else - (define default ((breaker-make-default breaker))) + (define default ((breaker-make-default bkr))) (set-union! formulas (break-formulas default)) ]) ]) @@ -308,8 +410,7 @@ (unless (or broken defined) (cons! new-total-bounds bound)) ]) ) - ;(printf "new-total-bounds: ~a~n" new-total-bounds) - + #| Now we try to use candidate breakers, starting with highest priority. @@ -326,22 +427,25 @@ Paths between broken sigs can also break soundness. Broken sigs are given an edge to a unique 'broken "sig", so we only need to check for loops. |# - - (set! candidates (sort candidates < #:key breaker-pri)) + + (set! candidates (sort candidates (lambda ([x : breaker] [y : breaker]) + (< (breaker-pri x) (breaker-pri y))))) (for ([breaker candidates]) (define break-graph (breaker-break-graph breaker)) (define broken-sigs (break-graph-sigs break-graph)) (define broken-edges (break-graph-edges break-graph)) - (define edges (list)) + (define edges (ann (list) (Listof (U (Pairof node/expr/relation Symbol) + (Pairof node/expr/relation node/expr/relation))))) + ; reduce broken sigs to broken edges between those sigs and the auxiliary 'broken symbol ; TODO: replace 'broken with univ (for ([sig broken-sigs]) (cons! edges (cons sig 'broken))) ; get all pairs from sets - (for ([edge broken-edges]) + (for ([edge-as-set broken-edges]) ; TODO: make functional - (set! edge (set->list edge)) + (define edge (set->list edge-as-set)) (define L (length edge)) (for* ([i (in-range 0 (- L 1))] [j (in-range (+ i 1) L)]) @@ -350,28 +454,36 @@ ) ; acceptable :<-> doesn't create loops <-> no edges already exist - (define acceptable (for/and ([edge edges]) + (define acceptable (foldl (lambda ([edge : (U (Pairof node/expr/relation Symbol) + (Pairof node/expr/relation node/expr/relation))] + [res : Boolean]) (define A (car edge)) (define B (cdr edge)) - (not (set-member? (hash-ref reachable A) B)) - )) + (define Aval (ann (hash-ref reachable A) (Setof (U node/expr/relation Symbol)))) + (and res (not (set-member? Aval B)))) #t edges)) - (cond [acceptable + (cond + [acceptable ; update reachability. do all edges in parallel - (define new-reachable (make-hash)) + (define new-reachable (ann (make-hash) (Mutable-HashTable node/expr/relation + (Setof (U node/expr/relation Symbol))))) (for ([edge edges]) - (define A (car edge)) - (define B (cdr edge)) + (define A (ann (car edge) node/expr/relation)) + (define B (ann (cdr edge) (U node/expr/relation Symbol))) (when (not (hash-has-key? new-reachable A)) - (hash-set! new-reachable A (mutable-set))) + (hash-set! new-reachable A (ann (mutable-set) (Setof (U node/expr/relation Symbol))))) (when (not (hash-has-key? new-reachable B)) - (hash-set! new-reachable B (mutable-set))) + (when (node/expr/relation? B) ; narrowing + (hash-set! new-reachable B (ann (mutable-set) (Setof (U node/expr/relation Symbol)))))) (set-union! (hash-ref new-reachable A) (hash-ref reachable B)) - (set-union! (hash-ref new-reachable B) (hash-ref reachable A)) + (when (node/expr/relation? B) + (set-union! (hash-ref new-reachable B) (hash-ref reachable A))) ) - (hash-for-each new-reachable (λ (sig newset) + + (hash-for-each new-reachable (λ ([sig : node/expr/relation] + [newset : (Setof (U node/expr/relation Symbol))]) ; set new sigs reachable from sig and vice versa - (define oldset (hash-ref reachable sig)) + (define oldset (ann (hash-ref reachable sig) (Setof (U node/expr/relation Symbol)))) (set-subtract! newset oldset) (for ([sig2 newset]) (define oldset2 (hash-ref reachable sig2)) @@ -383,11 +495,11 @@ ; do break (define break ((breaker-make-break breaker))) (cons! new-total-bounds (break-bound break)) - (set-union! formulas (break-formulas break)) - ][else + (set-union! formulas (break-formulas break))] + [else ; do default break (define default ((breaker-make-default breaker))) - (cons! new-total-bounds (break-sbound default)) + (cons! new-total-bounds (sbound->bound (break-sbound default))) (set-union! formulas (break-formulas default)) ]) ) @@ -396,9 +508,7 @@ (printf "~nBreakers ran.~n New total bounds:~a~n New formulas:~a~n" new-total-bounds formulas)) - (values new-total-bounds (set->list formulas)) -) - + (values new-total-bounds (set->list formulas))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;; Strategy Combinators ;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -407,69 +517,80 @@ ; ex: (f:B->C) => (g:A->B->C) where f is declared 'foo ; we will declare with formulas that g[a] is 'foo for all a in A ; but we will only enforce this with bounds for a single a in A +; Note: this is needed to support `is linear` on e.g., +; `sig N { next: lone N}` because `next` is ternary. +(: variadic (-> Integer StrategyFunction StrategyFunction)) (define (variadic n f) - (λ (pri rel bound atom-lists rel-list [loc #f]) + (λ ([pri : Integer] [rel : node/expr] [bound : bound] [atom-lists : (Listof Tuple)] + [rel-list : (Listof node/expr/relation)] [loc : (U srcloc #f) #f]) + (define info (just-location-info loc)) + (cond [(= (length rel-list) n) (f pri rel bound atom-lists rel-list loc) ][else - (define prefix (drop-right rel-list n)) + (define prefix (ann (drop-right rel-list n) (Listof node/expr))) (define postfix (take-right rel-list n)) - (define prefix-lists (drop-right atom-lists n)) + (define prefix-lists (ann (drop-right atom-lists n) (Listof Tuple))) (define postfix-lists (take-right atom-lists n)) - (define vars (for/list ([p prefix]) + (define vars (for/list ([p prefix]) : (Listof node/expr/quantifier-var) (let ([symv (gensym "v")]) - (@node/expr/quantifier-var @empty-nodeinfo 1 symv symv)) + (node/expr/quantifier-var empty-nodeinfo 1 symv symv)) )) - (define new-rel (@build-box-join rel vars)) ; rel[a][b]... + (define new-rel (build-box-join rel vars)) ; rel[a][b]... (define sub-breaker (f pri new-rel bound postfix-lists postfix loc)) (define sub-break-graph (breaker-break-graph sub-breaker)) - (define sigs (break-graph-sigs sub-break-graph)) + (define sigs (ann (break-graph-sigs sub-break-graph) (Setof node/expr/relation))) (define edges (break-graph-edges sub-break-graph)) - (define new-break-graph (break-graph - sigs - (set-union edges (for/set ([sig sigs] [p prefix]) (set sig p))) - )) + (define edgesAnd (for/set : (Setof (Setof node/expr/relation)) ([sig sigs] [p prefix]) + (if (node/expr/relation? p) + (set sig p) + (raise (format "Internal error: breaks.variadic combining sigs and non-sigs"))))) + (define new-break-graph (break-graph sigs (set-union edges edgesAnd))) (breaker pri new-break-graph (λ () ; unpack results of sub-breaker (define sub-break ((breaker-make-break sub-breaker))) (define sub-sbound (break-sbound sub-break)) - (define sub-lower (sbound-lower sub-sbound)) - (define sub-upper (sbound-upper sub-sbound)) + (define sub-lower (ann (sbound-lower sub-sbound) (Setof Tuple))) + (define sub-upper (ann (sbound-upper sub-sbound) (Setof Tuple))) (cond [(set-empty? sigs) ; no sigs are broken, so use sub-bounds for ALL instances - (define cart-pref (apply cartesian-product prefix-lists)) - (define lower (for*/set ([c cart-pref] [l sub-lower]) (append c l))) - (define upper (for*/set ([c cart-pref] [u sub-upper]) (append c u))) + (define cart-pref (ann (apply cartesian-product prefix-lists) (Listof Tuple))) + (define lower (for*/set : (Setof Tuple) ([c cart-pref] [l sub-lower]) (append c l))) + (define upper (for*/set : (Setof Tuple) ([c cart-pref] [u sub-upper]) (append c u))) (define bound (sbound rel lower upper)) (define sub-formulas (break-formulas sub-break)) - (define formulas (for/set ([f sub-formulas]) - (@quantified-formula (@just-location-info loc) 'all (map cons vars prefix) f) - )) + (define formulas (for/set : (Setof node/formula) ([f sub-formulas]) + (quantified-formula info 'all + (map (ann cons (-> node/expr/quantifier-var node/expr (Pairof node/expr/quantifier-var node/expr))) + vars prefix) f) + )) ; info quantifier decls formula) (break bound formulas) ][else ; just use the sub-bounds for a single instance of prefix - (define cars (map car prefix-lists)) - (define cdrs (map cdr prefix-lists)) - (define lower (for/set ([l sub-lower]) (append cars l))) + (define cars (map (ann car (-> Tuple FAtom)) prefix-lists)) + (define cdrs (map (ann cdr (-> Tuple Tuple)) prefix-lists)) + (define lower (for/set : (Setof Tuple) ([l sub-lower]) (append cars l))) (define upper (set-union - (for/set ([u sub-upper]) (append cars u)) + (for/set : (Setof Tuple) ([u sub-upper]) (append cars u)) (list->set (apply cartesian-product (append cdrs postfix-lists))) )) (define bound (sbound rel lower upper)) ; use default formulas unless single instance - (define sub-formulas (if (> (apply * (map length prefix-lists)) 1) + (define sub-formulas (if (> (apply * (map (ann length (-> (Listof Any) Integer)) prefix-lists)) 1) (break-formulas ((breaker-make-default sub-breaker))) (break-formulas sub-break) )) ; wrap each formula in foralls for each prefix rel - (define formulas (for/set ([f sub-formulas]) - (@quantified-formula (@just-location-info loc) 'all (map cons vars prefix) f) + (define formulas (for/set : (Setof node/formula) ([f sub-formulas]) + (quantified-formula info 'all + (map (ann cons (-> node/expr/quantifier-var node/expr (Pairof node/expr/quantifier-var node/expr))) + vars prefix) f) )) (break bound formulas) @@ -478,194 +599,216 @@ (λ () (define sub-break ((breaker-make-default sub-breaker))); (define sub-formulas (break-formulas sub-break)) - (define formulas (for/set ([f sub-formulas]) - (@quantified-formula (@just-location-info loc) 'all (map cons vars prefix) f) + (define formulas (for/set : (Setof node/formula) ([f sub-formulas]) + (quantified-formula info 'all + (map (ann cons (-> node/expr/quantifier-var node/expr (Pairof node/expr/quantifier-var node/expr))) + vars prefix) f) )) - (break bound formulas) + (break (bound->sbound bound) formulas) ) + #f ) ]) ) ) -(define (co f) - (λ (pri rel bound atom-lists rel-list [loc #f]) - (define sub-breaker (f pri (@~ rel) bound (reverse atom-lists) (reverse rel-list) loc)) - (breaker pri - (breaker-break-graph sub-breaker) - (λ () - ; unpack results of sub-breaker - (define sub-break ((breaker-make-break sub-breaker))) - (define sub-formulas (break-formulas sub-break)) - (define sub-sbound (break-sbound sub-break)) - (define sub-lower (sbound-lower sub-sbound)) - (define sub-upper (sbound-upper sub-sbound)) - ; reverse all tuples in sbounds - (define lower (for/set ([l sub-lower]) (reverse l))) - (define upper (for/set ([l sub-upper]) (reverse l))) - (define bound (sbound rel lower upper)) - - (break bound sub-formulas) - ) - (λ () - ((breaker-make-default sub-breaker)) - ) - ) - ) -) +; (define (co f) +; (λ (pri rel bound atom-lists rel-list [loc #f]) +; (define sub-breaker (f pri (@~ rel) bound (reverse atom-lists) (reverse rel-list) loc)) +; (breaker pri +; (breaker-break-graph sub-breaker) +; (λ () +; ; unpack results of sub-breaker +; (define sub-break ((breaker-make-break sub-breaker))) +; (define sub-formulas (break-formulas sub-break)) +; (define sub-sbound (break-sbound sub-break)) +; (define sub-lower (sbound-lower sub-sbound)) +; (define sub-upper (sbound-upper sub-sbound)) +; ; reverse all tuples in sbounds +; (define lower (for/set ([l sub-lower]) (reverse l))) +; (define upper (for/set ([l sub-upper]) (reverse l))) +; (define bound (sbound rel lower upper)) + +; (break bound sub-formulas) +; ) +; (λ () +; ((breaker-make-default sub-breaker)) +; ) +; ) +; ) +; ) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;; define breaks and compositions ;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; A->A Strategies ;;; -(add-strategy 'irref (λ (pri rel bound atom-lists rel-list [loc #f]) - (define atoms (first atom-lists)) - (define sig (first rel-list)) - (breaker pri - (break-graph (set) (set)) - (λ () - (make-upper-break rel - (filter-not (lambda (x) (equal? (first x) (second x))) - (apply cartesian-product atom-lists)))) - (λ () (break bound (set - (@no/info (@just-location-info loc) (@& @iden rel)) - ))) - ) -)) -(add-strategy 'ref (λ (pri rel bound atom-lists rel-list [loc #f]) - (define atoms (first atom-lists)) - (define sig (first rel-list)) - (breaker pri - (break-graph (set) (set)) - (λ () - (make-lower-break rel - (filter (lambda (x) (equal? (first x) (second x))) - (apply cartesian-product atom-lists)) - atom-lists)) - (λ () (break bound (set - (@all/info (@just-location-info loc) ([x sig]) - (@in x (@join sig rel)) - ) - ))) - ) -)) +; (add-strategy 'irref (λ (pri rel bound atom-lists rel-list [loc #f]) +; (define atoms (first atom-lists)) +; (define sig (first rel-list)) +; (breaker pri +; (break-graph (set) (set)) +; (λ () +; (make-upper-break rel +; (filter-not (lambda (x) (equal? (first x) (second x))) +; (apply cartesian-product atom-lists)))) +; (λ () (break bound (set +; (@no/info (just-location-info loc) (@& @iden rel)) +; ))) +; ) +; )) +; (add-strategy 'ref (λ (pri rel bound atom-lists rel-list [loc #f]) +; (define atoms (first atom-lists)) +; (define sig (first rel-list)) +; (breaker pri +; (break-graph (set) (set)) +; (λ () +; (make-lower-break rel +; (filter (lambda (x) (equal? (first x) (second x))) +; (apply cartesian-product atom-lists)) +; atom-lists)) +; (λ () (break bound (set +; (@all/info (just-location-info loc) ([x sig]) +; (@in x (@join sig rel)) +; ) +; ))) +; ) +; )) + + (add-strategy 'linear (λ (pri rel bound atom-lists rel-list [loc #f]) (define atoms (first atom-lists)) (define sig (first rel-list)) + (define info (just-location-info loc)) + (define init (node/expr/quantifier-var (just-location-info loc) 1 'init 'init)) + (define term (node/expr/quantifier-var (just-location-info loc) 1 'term 'term)) + (define x (node/expr/quantifier-var (just-location-info loc) 1 'x 'x)) (breaker pri (break-graph (set sig) (set)) - (λ () (make-exact-break rel (list->set (map list (drop-right atoms 1) (cdr atoms))))) - (λ () (break bound (set - (@some/info (@just-location-info loc) ([init sig]) (@&& - (@no (@join rel init)) - (@all ([x (@- sig init)]) (@one (@join rel x))) - (@= (@join init (@* rel)) sig) + (λ () (make-exact-break rel (list->set (map (ann list (-> FAtom FAtom (Listof FAtom))) + (drop-right atoms 1) (cdr atoms))) + (set))) + (λ () (break (bound->sbound bound) (set + (quantified-formula info 'some (list (cons init sig)) (&&/func #:info info + (multiplicity-formula info 'no (join/func #:info info rel init)) + (quantified-formula info 'all (list (cons x (-/func #:info info sig init))) + (multiplicity-formula info 'one (join/func #:info info rel x))) + (=/func #:info info (join/func #:info info init (*/func #:info info rel)) sig) )) - (@some/info (@just-location-info loc) ([term sig]) (@&& - (@no (@join term rel)) - (@all ([x (@- sig term)]) (@one (@join x rel))) - (@= (@join (@* rel) term) sig) - )) - ))) - ) -)) -(add-strategy 'acyclic (λ (pri rel bound atom-lists rel-list [loc #f]) - (define atoms (first atom-lists)) - (define sig (first rel-list)) - (breaker pri - (break-graph (set) (set)) - (λ () - (make-upper-break rel - (for*/list ([i (length atoms)] - [j (length atoms)] - #:when (< i j)) - (list (list-ref atoms i) (list-ref atoms j))))) - (λ () (break bound (set - (@no/info (@just-location-info loc) ([x sig]) - (@in x (@join x (@^ rel))) - ) - ))) - ) -)) -(add-strategy 'tree (λ (pri rel bound atom-lists rel-list [loc #f]) - (define atoms (first atom-lists)) - (define sig (first rel-list)) - (breaker pri - (break-graph (set) (set)) - (λ () - (make-break - (bound->sbound (make-upper-bound rel - (for*/list ([i (length atoms)] - [j (length atoms)] - #:when (< i j)) - (list (list-ref atoms i) (list-ref atoms j))))) - (set - (@some/info (@just-location-info loc) ([n sig]) - (@all ([m (@- sig n)]) - (@one (@join rel m)) - ) - ) - ))) - (λ () (break bound (set - (@some/info (@just-location-info loc) ([n sig]) (@&& - (@no (@join rel n)) - (@all ([m (@- sig n)]) - (@one (@join rel m)) - ) + + (quantified-formula info 'some (list (cons term sig)) (&&/func #:info info + (multiplicity-formula info 'no (join/func #:info info term rel)) + (quantified-formula info 'all (list (cons x (-/func #:info info sig term))) + (multiplicity-formula info 'one (join/func #:info info x rel))) + (=/func #:info info (join/func #:info info (*/func #:info info rel) term) sig) )) ))) + #f ) )) + +; (add-strategy 'acyclic (λ (pri rel bound [atom-lists : (Listof Any)] [rel-list : (Listof Any)] [loc #f]) +; (define atoms (first atom-lists)) +; (define sig (first rel-list)) +; (breaker pri +; (break-graph (set) (set)) +; (λ () +; (make-upper-break rel +; (for*/list ([i (length atoms)] +; [j (length atoms)] +; #:when (< i j)) +; (list (list-ref atoms i) (list-ref atoms j))))) +; (λ () (break bound (set +; (@no/info (just-location-info loc) ([x sig]) +; (@in x (@join x (@^ rel))) +; ) +; ))) +; ) +; )) +; (add-strategy 'tree (λ (pri rel bound atom-lists rel-list [loc #f]) +; (define atoms (first atom-lists)) +; (define sig (first rel-list)) +; (breaker pri +; (break-graph (set) (set)) +; (λ () +; (make-break +; (bound->sbound (make-upper-bound rel +; (for*/list ([i (length atoms)] +; [j (length atoms)] +; #:when (< i j)) +; (list (list-ref atoms i) (list-ref atoms j))))) +; (set +; (@some/info (just-location-info loc) ([n sig]) +; (@all ([m (@- sig n)]) +; (@one (@join rel m)) +; ) +; ) +; ))) +; (λ () (break bound (set +; (@some/info (just-location-info loc) ([n sig]) (@&& +; (@no/info (just-location-info loc) (@join rel n)) +; (@all ([m (@- sig n)]) +; (@one (@join rel m)) +; ) +; )) +; ))) +; ) +; )) (add-strategy 'plinear (λ (pri rel bound atom-lists rel-list [loc #f]) (define atoms (first atom-lists)) (define sig (first rel-list)) + (define info (just-location-info loc)) + (define init (node/expr/quantifier-var (just-location-info loc) 1 'init 'init)) + (define x (node/expr/quantifier-var (just-location-info loc) 1 'x 'x)) (breaker pri (break-graph (set sig) (set)) (λ () (break (sbound rel (set) ;(set (take atoms 2)) - (list->set (map list (drop-right atoms 1) (cdr atoms))) + (list->set (map (ann list (-> FAtom FAtom (Listof FAtom))) + (drop-right atoms 1) (cdr atoms))) ) (set - (@lone/info (@just-location-info loc) ([init sig]) (@&& - (@no (@join rel init)) - (@some (@join init rel)) - )) + (multiplicity-formula info 'lone + (set/func #:info info (list (cons init sig)) (&&/func #:info info + (multiplicity-formula info 'no (join/func #:info info rel init)) + (multiplicity-formula info 'some (join/func #:info info init rel))))) ) )) - (λ () (break bound (set - (@lone/info (@just-location-info loc) (@- (@join rel sig) (@join sig rel))) ; lone init - (@lone/info (@just-location-info loc) (@- (@join sig rel) (@join rel sig))) ; lone term - (@no/info (@just-location-info loc) (@& @iden (@^ rel))) ; acyclic - (@all/info (@just-location-info loc) ([x sig]) (@&& ; all x have - (@lone (@join x rel)) ; lone successor - (@lone (@join rel x)) ; lone predecessor + (λ () (break (bound->sbound bound) (set + (multiplicity-formula info 'lone (-/func #:info info (join/func #:info info rel sig) (join/func #:info info sig rel))) ; lone init + (multiplicity-formula info 'lone (-/func #:info info (join/func #:info info sig rel) (join/func #:info info rel sig))) ; lone term + (multiplicity-formula info 'no (&/func #:info info iden (^/func #:info info rel))) ; acyclic + (quantified-formula info 'all (list (cons x sig)) (&&/func #:info info ; all x have + (multiplicity-formula info 'lone (join/func #:info info x rel)) ; lone successor + (multiplicity-formula info 'lone (join/func #:info info rel x)) ; lone predecessor )) ))) + #f ) )) ;;; A->B Strategies ;;; -(add-strategy 'func (λ (pri rel bound atom-lists rel-list [loc #f]) - +(add-strategy 'func (λ ([pri : Integer] [rel : node/expr] [bound : bound] [atom-lists : (Listof Tuple)] [rel-list : (Listof node/expr)] [loc : (U srcloc #f) #f]) + (: funcformulajoin (-> (Listof node/expr/quantifier-var) node/expr)) (define (funcformulajoin quantvarlst) (cond - [(empty? (rest quantvarlst)) (@join (first quantvarlst) rel)] - [else (@join (first quantvarlst) (funcformulajoin (rest quantvarlst)))])) + [(empty? (rest quantvarlst)) (join/func #:info (just-location-info loc) (first quantvarlst) rel)] + [else (join/func #:info (just-location-info loc) (first quantvarlst) (funcformulajoin (rest quantvarlst)))])) - (define (funcformula rllst quantvarlst) + (: funcformula (-> (Listof node/expr) (Listof node/expr/quantifier-var) node/formula)) + (define (funcformula rllst quantvarlst) (cond [(empty? (rest (rest rllst))) - (let* ([var-id (gensym 'pfunc)] - [a (@node/expr/quantifier-var (@just-location-info loc) 1 var-id var-id)]) - (@quantified-formula (@just-location-info loc) 'all - (list (cons a (first rllst))) - (@one (funcformulajoin (cons a quantvarlst)))))] + (let* ([var-id (gensym 'func)] + [a (node/expr/quantifier-var (just-location-info loc) 1 var-id var-id)]) + (quantified-formula (just-location-info loc) 'all + (ann (list (cons a (first rllst))) (Listof (Pairof node/expr/quantifier-var node/expr))) + (one/func #:info (just-location-info loc) (funcformulajoin (cons a quantvarlst)))))] [else - (let* ([var-id (gensym 'pfunc)] - [a (@node/expr/quantifier-var (@just-location-info loc) 1 var-id var-id)]) - (@quantified-formula (@just-location-info loc) 'all + (let* ([var-id (gensym 'func)] + [a (node/expr/quantifier-var (just-location-info loc) 1 var-id var-id)]) + (quantified-formula (just-location-info loc) 'all (list (cons a (first rllst))) (funcformula (rest rllst) (cons a quantvarlst))))])) (define formulas (set (funcformula rel-list (list)))) @@ -721,32 +864,38 @@ ; (λ () (break bound formulas)) ; ) ; END INSERTED TEMPORARY FIX FOR 'FUNC - (breaker pri + (breaker pri (break-graph (set) (set)) (λ () (break (bound->sbound bound) formulas)) - (λ () (break bound formulas))) -)) - + ;; TYPES + ;(λ () (break bound formulas)) + (λ () (break (bound->sbound bound) formulas)) + #f))) (add-strategy 'pfunc (λ (pri rel bound atom-lists rel-list [loc #f]) + (define info (just-location-info loc)) + + (: pfuncformulajoin (-> (Listof node/expr/quantifier-var) node/expr)) (define (pfuncformulajoin quantvarlst) (cond ; x_n.rel - [(empty? (rest quantvarlst)) (@join (first quantvarlst) rel)] + [(empty? (rest quantvarlst)) (join/func #:info info (first quantvarlst) rel)] ; ... x_n-1.x_n.rel - [else (@join (first quantvarlst) (pfuncformulajoin (rest quantvarlst)))])) + [else (join/func #:info info (first quantvarlst) (pfuncformulajoin (rest quantvarlst)))])) + + (: pfuncformula (-> (Listof node/expr) (Listof node/expr/quantifier-var) node/formula)) (define (pfuncformula rllst quantvarlst) (cond [(empty? (rest (rest rllst))) (let* ([var-id (gensym 'pfunc)] - [a (@node/expr/quantifier-var (@just-location-info loc) 1 var-id var-id)]) - (@quantified-formula (@just-location-info loc) 'all + [a (node/expr/quantifier-var info 1 var-id var-id)]) + (quantified-formula info 'all (list (cons a (first rllst))) - (@lone (pfuncformulajoin (cons a quantvarlst)))))] + (multiplicity-formula info 'lone (pfuncformulajoin (cons a quantvarlst)))))] [else (let* ([var-id (gensym 'pfunc)] - [a (@node/expr/quantifier-var (@just-location-info loc) 1 var-id var-id)]) - (@quantified-formula (@just-location-info loc) 'all + [a (node/expr/quantifier-var info 1 var-id var-id)]) + (quantified-formula info 'all (list (cons a (first rllst))) (pfuncformula (rest rllst) (cons a quantvarlst))))])) (define pf-fmla (pfuncformula rel-list (list))) @@ -778,157 +927,172 @@ (breaker pri (break-graph (set) (set)) (λ () (break (bound->sbound bound) formulas)) - (λ () (break bound formulas)) - ) - )) - -(add-strategy 'surj (λ (pri rel bound atom-lists rel-list [loc #f]) - (define A (first rel-list)) - (define B (second rel-list)) - (define As (first atom-lists)) - (define Bs (second atom-lists)) - (define formulas (set - (@all/info (@just-location-info loc) ([a A]) (@one (@join a rel))) ; @one - (@all/info (@just-location-info loc) ([b B]) (@some (@join rel b))) ; @some - )) - (if (equal? A B) - (breaker pri ; TODO: can improve, but need better symmetry-breaking predicates - (break-graph (set) (set)) - (λ () (break (bound->sbound bound) formulas)) - (λ () (break bound formulas)) - ) - (breaker pri ; TODO: can improve, but need better symmetry-breaking predicates - (break-graph (set) (set (set A B))) ; breaks only {A,B} - (λ () - ; assume wlog f(a) = b for some a in A, b in B - (break - (sbound rel - (set (list (car As) (car Bs))) - (set-add (cartesian-product (cdr As) Bs) (list (car As) (car Bs)))) - formulas)) - (λ () (break bound formulas)) - ) - ) -)) -(add-strategy 'inj (λ (pri rel bound atom-lists rel-list [loc #f]) - (define A (first rel-list)) - (define B (second rel-list)) - (define As (first atom-lists)) - (define Bs (second atom-lists)) - (define formulas (set - (@all/info (@just-location-info loc) ([a A]) (@one (@join a rel))) ; @one - (@all/info (@just-location-info loc) ([b B]) (@lone (@join rel b))) ; @lone - )) - (if (equal? A B) - (breaker pri ; TODO: can improve, but need better symmetry-breaking predicates - (break-graph (set) (set)) (λ () (break (bound->sbound bound) formulas)) - (λ () (break bound formulas)) + #f ) - (breaker pri ; TODO: can improve, but need better symmetry-breaking predicates - (break-graph (set B) (set (set A B))) ; breaks B and {A,B} - (λ () - ; assume wlog f(a) = b for some a in A, b in B - (break - (sbound rel - (set (list (car As) (car Bs))) - (set-add (cartesian-product (cdr As) (cdr Bs)) (list (car As) (car Bs)))) - formulas)) - (λ () (break bound formulas)) - ) - ) -)) -(add-strategy 'bij (λ (pri rel bound atom-lists rel-list [loc #f]) - (define A (first rel-list)) - (define B (second rel-list)) - (define As (first atom-lists)) - (define Bs (second atom-lists)) - (define formulas (set - (@all/info (@just-location-info loc) ([a A]) (@one (@join a rel))) ; @one - (@all/info (@just-location-info loc) ([b B]) (@one (@join rel b))) ; @one )) - (if (equal? A B) - (breaker pri ; TODO: can improve, but need better symmetry-breaking predicates - (break-graph (set) (set)) - (λ () (break (bound->sbound bound) formulas)) - (λ () (break bound formulas)) - ) - (breaker pri ; TODO: can improve, but need better symmetry-breaking predicates - (break-graph (set) (set (set A B))) ; breaks only {A,B} - (λ () (make-exact-break rel (map list As Bs))) - (λ () (break bound formulas)) - ) - ) -)) -(add-strategy 'pbij (λ (pri rel bound atom-lists rel-list [loc #f]) - (define A (first rel-list)) - (define B (second rel-list)) - (define As (first atom-lists)) - (define Bs (second atom-lists)) - (define LA (length As)) - (define LB (length Bs)) - (define broken (cond [(> LA LB) (set A)] - [(< LA LB) (set B)] - [else (set)])) - ;(printf "broken : ~v~n" broken) - (define formulas (set - (@all/info (@just-location-info loc) ([a A]) (@one (@join a rel))) ; @one - (@all/info (@just-location-info loc) ([b B]) (@one (@join rel b))) ; @one - )) - (if (equal? A B) - (breaker pri ; TODO: can improve, but need better symmetry-breaking predicates - (break-graph (set) (set)) - (λ () (break (bound->sbound bound) formulas)) - (λ () (break bound formulas)) - ) - (breaker pri ; TODO: can improve, but need better symmetry-breaking predicates - (break-graph broken (set (set A B))) ; breaks only {A,B} - (λ () (make-upper-break rel (for/list ([a As][b Bs]) (list a b)) formulas)) - (λ () (break bound formulas)) - ) - ) -)) + +; ;(: surj-strategy StrategyFunction) +; (define surj-strategy (λ ([pri : Number] [rel : Any] [bound : bound] [atom-lists : (NonEmptyListOf (Listof Any))] [rel-list : (NonEmptyListOf Any)] [loc #f]) +; (define A (first rel-list)) +; (define B (second rel-list)) +; (define As (first atom-lists)) +; (define Bs (second atom-lists)) +; (define formulas (set +; (@all/info (just-location-info loc) ([a A]) (@one/info (just-location-info loc) (@join a rel))) ; @one +; (@all/info (just-location-info loc) ([b B]) (@some/info (just-location-info loc) (@join rel b))) ; @some +; )) +; (if (equal? A B) +; (breaker pri ; TODO: can improve, but need better symmetry-breaking predicates +; (break-graph (set) (set)) +; (λ () (break (bound->sbound bound) formulas)) +; (λ () (break bound formulas)) +; ) +; (breaker pri ; TODO: can improve, but need better symmetry-breaking predicates +; (break-graph (set) (set (set A B))) ; breaks only {A,B} +; (λ () +; ; assume wlog f(a) = b for some a in A, b in B +; (break +; (sbound rel +; (set (list (car As) (car Bs))) +; (set-add (cartesian-product (cdr As) Bs) (list (car As) (car Bs)))) +; formulas)) +; (λ () (break bound formulas)) +; ) +; ) +; )) +; (add-strategy 'surj surj-strategy) + +; (add-strategy 'inj (λ (pri rel bound atom-lists rel-list [loc #f]) +; (define A (first rel-list)) +; (define B (second rel-list)) +; (define As (first atom-lists)) +; (define Bs (second atom-lists)) +; (define formulas (set +; (@all/info (just-location-info loc) ([a A]) (@one/info (just-location-info loc) (@join a rel))) ; @one +; (@all/info (just-location-info loc) ([b B]) (@lone/info (just-location-info loc) (@join rel b))) ; @lone +; )) +; (if (equal? A B) +; (breaker pri ; TODO: can improve, but need better symmetry-breaking predicates +; (break-graph (set) (set)) +; (λ () (break (bound->sbound bound) formulas)) +; (λ () (break bound formulas)) +; ) +; (breaker pri ; TODO: can improve, but need better symmetry-breaking predicates +; (break-graph (set B) (set (set A B))) ; breaks B and {A,B} +; (λ () +; ; assume wlog f(a) = b for some a in A, b in B +; (break +; (sbound rel +; (set (list (car As) (car Bs))) +; (set-add (cartesian-product (cdr As) (cdr Bs)) (list (car As) (car Bs)))) +; formulas)) +; (λ () (break bound formulas)) +; ) +; ) +; )) +; (add-strategy 'bij (λ (pri rel bound atom-lists rel-list [loc #f]) +; (define A (first rel-list)) +; (define B (second rel-list)) +; (define As (first atom-lists)) +; (define Bs (second atom-lists)) +; (define formulas (set +; (@all/info (just-location-info loc) ([a A]) (@one/info (just-location-info loc) (@join a rel))) ; @one +; (@all/info (just-location-info loc) ([b B]) (@one/info (just-location-info loc) (@join rel b))) ; @one +; )) +; (if (equal? A B) +; (breaker pri ; TODO: can improve, but need better symmetry-breaking predicates +; (break-graph (set) (set)) +; (λ () (break (bound->sbound bound) formulas)) +; (λ () (break bound formulas)) +; ) +; (breaker pri ; TODO: can improve, but need better symmetry-breaking predicates +; (break-graph (set) (set (set A B))) ; breaks only {A,B} +; (λ () (make-exact-break rel (map list As Bs))) +; (λ () (break bound formulas)) +; ) +; ) +; )) +; (add-strategy 'pbij (λ (pri rel bound atom-lists rel-list [loc #f]) +; (define A (first rel-list)) +; (define B (second rel-list)) +; (define As (first atom-lists)) +; (define Bs (second atom-lists)) +; (define LA (length As)) +; (define LB (length Bs)) +; (define broken (cond [(> LA LB) (set A)] +; [(< LA LB) (set B)] +; [else (set)])) +; ;(printf "broken : ~v~n" broken) +; (define formulas (set +; (@all/info (just-location-info loc) ([a A]) (@one/info (just-location-info loc) (@join a rel))) ; @one +; (@all/info (just-location-info loc) ([b B]) (@one/info (just-location-info loc) (@join rel b))) ; @one +; )) +; (if (equal? A B) +; (breaker pri ; TODO: can improve, but need better symmetry-breaking predicates +; (break-graph (set) (set)) +; (λ () (break (bound->sbound bound) formulas)) +; (λ () (break bound formulas)) +; ) +; (breaker pri ; TODO: can improve, but need better symmetry-breaking predicates +; (break-graph broken (set (set A B))) ; breaks only {A,B} +; (λ () (make-upper-break rel (for/list ([a As][b Bs]) (list a b)) formulas)) +; (λ () (break bound formulas)) +; ) +; ) +; )) ; use to prevent breaks -(add-strategy 'default (λ (pri rel bound atom-lists rel-list [loc #f]) (breaker pri - (break-graph (set) (set)) - (λ () - (make-upper-break rel (list->set (apply cartesian-product atom-lists)))) - (λ () (break bound (set))) -))) +(: defaultStrategy StrategyFunction) +(define defaultStrategy (λ ([pri : Integer] [rel : node/expr] [bound : bound] + [atom-lists : (Listof Tuple)] + [rel-list : (Listof node/expr)] [loc : (U srcloc #f) #f]) + (if (node/expr/relation? rel) + (breaker pri + (break-graph (set) (set)) + (λ () + (make-upper-break rel (list->set (apply cartesian-product atom-lists)))) + (λ () (break (bound->sbound bound) (set))) + #f) + (raise (format "Internal error in breaks.defaultStrategy. Given: ~a; from:~a~n" rel loc))))) +(add-strategy 'default defaultStrategy) +; (add-strategy 'cotree (variadic 2 (co (hash-ref strategies 'tree)))) +; (add-strategy 'cofunc (variadic 2 (co (hash-ref strategies 'func)))) +; (add-strategy 'cosurj (variadic 2 (co (hash-ref strategies 'surj)))) +; (add-strategy 'coinj (variadic 2 (co (hash-ref strategies 'inj)))) -(add-strategy 'cotree (variadic 2 (co (hash-ref strategies 'tree)))) -(add-strategy 'cofunc (variadic 2 (co (hash-ref strategies 'func)))) -(add-strategy 'cosurj (variadic 2 (co (hash-ref strategies 'surj)))) -(add-strategy 'coinj (variadic 2 (co (hash-ref strategies 'inj)))) +; (add-strategy 'irref (variadic 2 (hash-ref strategies 'irref))) +; (add-strategy 'ref (variadic 2 (hash-ref strategies 'ref))) -(add-strategy 'irref (variadic 2 (hash-ref strategies 'irref))) -(add-strategy 'ref (variadic 2 (hash-ref strategies 'ref))) ; this one cannot afford to go to purely formula break (add-strategy 'linear (variadic 2 (hash-ref strategies 'linear))) (add-strategy 'plinear (variadic 2 (hash-ref strategies 'plinear))) -(add-strategy 'acyclic (variadic 2 (hash-ref strategies 'acyclic))) -(add-strategy 'tree (variadic 2 (hash-ref strategies 'tree))) + + + +; (add-strategy 'acyclic (variadic 2 (hash-ref strategies 'acyclic))) +; (add-strategy 'tree (variadic 2 (hash-ref strategies 'tree))) (add-strategy 'func (hash-ref strategies 'func)) (add-strategy 'pfunc (hash-ref strategies 'pfunc)) -(add-strategy 'surj (variadic 2 (hash-ref strategies 'surj))) -(add-strategy 'inj (variadic 2 (hash-ref strategies 'inj))) -(add-strategy 'bij (variadic 2 (hash-ref strategies 'bij))) -(add-strategy 'pbij (variadic 2 (hash-ref strategies 'pbij))) +; (add-strategy 'surj (variadic 2 (hash-ref strategies 'surj))) +; (add-strategy 'inj (variadic 2 (hash-ref strategies 'inj))) +; (add-strategy 'bij (variadic 2 (hash-ref strategies 'bij))) +; (add-strategy 'pbij (variadic 2 (hash-ref strategies 'pbij))) ;;; Domination Order ;;; -(declare 'linear > 'tree) -(declare 'tree > 'acyclic) -(declare 'acyclic > 'irref) -(declare 'func < 'surj 'inj 'pfunc) -(declare 'bij = 'surj 'inj) -(declare 'linear = 'tree 'cotree) -(declare 'bij = 'func 'cofunc) -(declare 'cofunc < 'cosurj 'coinj) -(declare 'bij = 'cosurj 'coinj) +; (declare 'linear > 'tree) +; (declare 'tree > 'acyclic) +; (declare 'acyclic > 'irref) +; (declare 'func < 'surj 'inj 'pfunc) +(declare 'func < 'pfunc) +; (declare 'bij = 'surj 'inj) +; (declare 'linear = 'tree 'cotree) +; (declare 'bij = 'func 'cofunc) +; (declare 'cofunc < 'cosurj 'coinj) +; (declare 'bij = 'cosurj 'coinj) (provide get-co) (define co-map (make-hash)) @@ -978,45 +1142,46 @@ TODO: |# -(require (except-in xml attribute)) -(define (xml->breakers xml name-to-rel) - (set! xml (xml->xexpr (document-element (read-xml (open-input-string xml))))) - (define (read-label info) - (define label #f) - (define builtin #f) - (for/list ([i info]) (match i - [(list 'label l) (set! label l)] - [(list 'builtin "yes") (set! builtin #t)] - [else #f] - )) - (if builtin #f (hash-ref name-to-rel label)) - ) - (define (read-atoms atoms) - (filter identity (for/list ([a atoms]) (match a - [(list atom (list (list 'label l))) (string->symbol l)] - [else #f] - ))) - ) - (define (read-tuples tuples) - (list->set (filter identity (for/list ([t tuples]) (match t - [(list 'tuple atoms ...) (read-atoms atoms)] - [else #f] - )))) - ) - (define (read-rel x) (match x - [(list 'sig info atoms ...) - (define sig (read-label info)) - (if sig (make-exact-sbound sig (map list (read-atoms atoms))) #f)] - [(list 'field info tuples ...) (make-exact-sbound (read-label info) (read-tuples tuples))] - [else #f] - )) - - (when (equal? (first xml) 'alloy) (for ([x xml]) (match x - [(list 'instance _ ...) (set! xml x)] - [else #f] - ))) - (match xml - [(list 'instance _ ...) (filter identity (for/list ([x xml]) (read-rel x)))] - [else (list (read-rel xml))] - ) -) \ No newline at end of file +; (require (except-in xml attribute)) + +; (define (xml->breakers xml name-to-rel) +; (set! xml (xml->xexpr (document-element (read-xml (open-input-string xml))))) +; (define (read-label info) +; (define label #f) +; (define builtin #f) +; (for/list ([i info]) (match i +; [(list 'label l) (set! label l)] +; [(list 'builtin "yes") (set! builtin #t)] +; [else #f] +; )) +; (if builtin #f (hash-ref name-to-rel label)) +; ) +; (define (read-atoms atoms) +; (filter identity (for/list ([a atoms]) (match a +; [(list atom (list (list 'label l))) (string->symbol l)] +; [else #f] +; ))) +; ) +; (define (read-tuples tuples) +; (list->set (filter identity (for/list ([t tuples]) (match t +; [(list 'tuple atoms ...) (read-atoms atoms)] +; [else #f] +; )))) +; ) +; (define (read-rel x) (match x +; [(list 'sig info atoms ...) +; (define sig (read-label info)) +; (if sig (make-exact-sbound sig (map list (read-atoms atoms))) #f)] +; [(list 'field info tuples ...) (make-exact-sbound (read-label info) (read-tuples tuples))] +; [else #f] +; )) + +; (when (equal? (first xml) 'alloy) (for ([x xml]) (match x +; [(list 'instance _ ...) (set! xml x)] +; [else #f] +; ))) +; (match xml +; [(list 'instance _ ...) (filter identity (for/list ([x xml]) (read-rel x)))] +; [else (list (read-rel xml))] +; ) +; ) \ No newline at end of file diff --git a/forge/lang/ast.rkt b/forge/lang/ast.rkt index b491d1ae6..f0dcc9636 100644 --- a/forge/lang/ast.rkt +++ b/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) diff --git a/forge/lang/bounds.rkt b/forge/lang/bounds.rkt index 0b4a0dcb7..3a86af93d 100644 --- a/forge/lang/bounds.rkt +++ b/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))) + diff --git a/forge/lang/reader.rkt b/forge/lang/reader.rkt index eb8dc5de1..7a55d094d 100644 --- a/forge/lang/reader.rkt +++ b/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 diff --git a/forge/send-to-solver.rkt b/forge/send-to-solver.rkt index 528b3d238..9fa9a5f50 100644 --- a/forge/send-to-solver.rkt +++ b/forge/send-to-solver.rkt @@ -1,29 +1,162 @@ -#lang racket/base +#lang typed/racket/base/optional + +(require forge/types/ast-adapter) +(require forge/types/lazy-tree-adapter) + +;; TODO TYPES: +; Notice that we need to instantiate polymorphic functions often. E.g., +; (inst map FAtom Tuple) <-- to mean we're mapping tuples to atoms + +(define-type PiecewiseBounds (HashTable node/expr/relation PiecewiseBound)) + +(require/typed forge/last-checker + [checkFormula (-> Run-spec node/formula (Listof Any) (HashTable Any Any) Void)]) + +;; TYPES TODO: the contracts are more refined. should we combine the two? +(require/typed forge/sigs-structs + [#:struct Sat ( + [instances : Any] ; list of hashes + [stats : Any] ; association list + [metadata : Any])] ; association list) + [#:struct Unsat ( + [core : (U False (Listof Any))] ; list-of-Formula-string-or-formulaID + [stats : Any] ; association list + [kind : Symbol] ; symbol + )] + [#:struct Unknown ( + [stats : Any] ; data on performance, translation, etc. + [metadata : Any] ; any solver-specific data provided about the unknown result + )] + [#:struct Kodkod-current ( + [formula : Integer] + [expression : Integer] + [int : Integer])] + [#:struct (Relation node/expr/relation) ( + [name : Symbol] ; symbol? + [sigs-thunks : (Listof (-> Sig))] + [breaker : (U node/breaking/break False)] + )] + [#:struct Server-ports ( + [stdin : Output-Port] + [stdout : Input-Port] + [stderr : Input-Port] + [shutdown : (-> Void)] + [is-running? : (-> Boolean)])] + [#:struct (Sig node/expr/relation) ( + [name : Symbol] ; symbol? + [one : Boolean] ; boolean? + [lone : Boolean] ; boolean? + [abstract : Boolean] ; boolean? + [extends : (U Sig False)] ; (or/c Sig? #f) + )] + [#:struct Run-spec ( + [state : State] ; Model state at the point of this run + [preds : (Listof node/formula)] ; predicates to run, conjoined + [scope : Scope] ; Numeric scope(s) + [bounds : Bound] ; set-based upper and lower bounds + [target : Any] ;(or/c Target? #f) ; target-oriented model finding + )] + [#:struct Bound ( + ; pbindings: partial (but complete) bindings for a given relation + [pbindings : (HashTable node/expr/relation sbound)] + ; tbindings: total (and complete) bindings for a given relation; also known as an exact bound. + [tbindings : (HashTable node/expr/relation Any)] + ; incomplete bindings for a given relation, indexed by first column + [piecewise : PiecewiseBounds] + ; original AST nodes, for improving errors, indexed by relation + [orig-nodes : (HashTable node/expr/relation (Listof node))] + )] + [#:struct PiecewiseBound ( + [tuples : (Listof Tuple)] ; first element is the indexed atom in the original piecewise bounds + [atoms : (Listof FAtom)] ; which atoms have been bound? (distinguish "given none" from "none given") + [operator : (U '= 'in 'ni)])] ; which operator mode? + [#:struct State ( + [sigs : (HashTable Symbol Sig)] + [sig-order : (Listof Symbol)] + [relations : (HashTable Symbol Relation)] + [relation-order : (Listof Symbol)] + [pred-map : (HashTable Symbol node/formula)] ;(hash/c symbol? (or/c (unconstrained-domain-> node/formula?) node/formula?)) + [fun-map : (HashTable Symbol node)] ; (hash/c symbol? (unconstrained-domain-> node?)) + [const-map : (HashTable Symbol node)] + [inst-map : (HashTable Symbol Any)] ; (hash/c symbol? Inst?) + [options : Any] ; Options? + [runmap : (HashTable Symbol Run)])] + [#:struct Run ( + [name : Symbol] + [command : Syntax] + [run-spec : Run-spec] + [result : Any] ;tree:node + [server-ports : Any] ;Server-ports?] + [atoms : (Listof FAtom)] + [kodkod-currents : Any] ; Kodkod-current?] + [kodkod-bounds : (Listof Any)] + [last-sterling-instance : Any ])] ; (box/c (or/c Sat? Unsat? Unknown? false/c)) + [#:struct Range ( + [lower : (U Integer False)] + [upper : (U Integer False)])] + [#:struct Scope ( + [default-scope : (U Range False)] + [bitwidth : (U Integer False)] + [sig-scopes : (HashTable Symbol Range)])] + [get-relations (-> (U Run State Run-spec) (Listof Relation))] + [get-sigs (->* ((U Run State Run-spec)) ((U False node/expr/relation)) (Listof Sig))] + [get-sig (-> (U Run State Run-spec) (U Symbol node/expr/relation) (U Sig False))] + [get-option (case-> + (-> (U Run State Run-spec) 'backend Symbol) + (-> (U Run State Run-spec) 'solver (U String Symbol)) + (-> (U Run State Run-spec) 'java_exe_location (U False Path-String)) + (-> (U Run State Run-spec) 'problem_type Symbol) + (-> (U Run State Run-spec) Symbol Any))] + [get-state (-> (U Run Run-spec State) State)] + [get-bitwidth (-> (U Run-spec Scope) Integer)] + [get-children (-> (U Run State Run-spec) Sig (Listof Sig))] + [DEFAULT-SIG-SCOPE Range] + [get-top-level-sigs (-> (U Run State Run-spec) (Listof Sig))] + ;; TODO TYPES: these are macros, but they has no parameters, so they are being immediately + ;; expanded here to the relations they denote. + [Int Sig] + [succ Relation] +) -(require forge/sigs-structs) (require forge/breaks) -(require forge/lang/ast) (require forge/lang/bounds) (require forge/shared - (prefix-in tree: forge/utils/lazy-tree) - forge/last-checker - forge/choose-lang-specific) -(require (prefix-in @ (only-in racket/base >= not - = and or max > < +)) + forge/last-checker) +(require (prefix-in @ (only-in racket/base max + -)) (only-in racket match first rest empty empty? set->list list->set set-intersect set-union curry range index-of pretty-print filter-map string-prefix? string-split thunk* - remove-duplicates subset? cartesian-product match-define cons? set-subtract) + remove-duplicates subset? cartesian-product match-define cons? set-subtract + build-list) racket/hash) (require (only-in syntax/srcloc build-source-location-syntax)) -; Solver-specific backend initializer functions -(require (prefix-in pardinus: (only-in forge/pardinus-cli/server/kks start-server))) -(require (prefix-in smtlib: (only-in forge/solver-specific/cvc5-server start-server))) +; Solver-specific backend initializer functions. +(require/typed forge/solver-specific/cvc5-server + [(start-server smtlib:start-server) (-> Symbol Symbol + (Values Output-Port Input-Port Input-Port (-> Void) (-> Boolean)))]) +(require/typed forge/pardinus-cli/server/kks + [(start-server pardinus:start-server ) (-> Symbol Symbol (U False Path-String) + (Values Output-Port Input-Port Input-Port (-> Void) (-> Boolean)))]) + +; (send-to-kodkod run-name run-spec bitwidth all-atoms solverspec total-bounds bound-lower +; bound-upper run-constraints stdin stdout stderr)) ; Separate solver-specific translation for each solver backend -(require (only-in forge/solver-specific/pardinus - send-to-kodkod get-next-kodkod-model)) -(require (only-in forge/solver-specific/cvc5-tor - send-to-cvc5-tor get-next-cvc5-tor-model)) +(require/typed forge/solver-specific/pardinus + [send-to-kodkod (-> Symbol Run-spec Integer (Listof FAtom) Any Any Any Any + (Listof node/formula) Output-Port Input-Port Input-Port + (Values Any Any))] + [get-next-kodkod-model (->* ((-> Boolean) Symbol Any (Listof FAtom) Any + Output-Port Input-Port Input-Port) + (String) (U Sat Unsat Unknown))]) + +(require/typed forge/solver-specific/cvc5-tor + [send-to-cvc5-tor (-> Symbol Run-spec Integer (Listof FAtom) Any Any Any Any + (Listof node/formula) Output-Port Input-Port Input-Port + (Values Any Any))] + [get-next-cvc5-tor-model (->* ((-> Boolean) Symbol Any (Listof FAtom) Any + Output-Port Input-Port Input-Port) + (String #:run-command (U False Syntax)) (U Sat Unsat Unknown))]) ; Disable DrRacket GUI extension/tool ;(require "drracket-gui.rkt") @@ -36,8 +169,10 @@ ;;;;;; Run Logic ;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; Will be a Server-ports tuple if a server is active. +; Will be a Server-ports tuple if a server is active. +(: server-state (Boxof (U False Server-ports))) (define server-state (box #f)) + ; In order to prevent a bad crash, keep track of run-names used in the past, ; and throw a friendlier error if one is re-used. (define run-name-history (box (list))) @@ -46,13 +181,14 @@ ; This function is provided for scripting tests, but it is volatile; don't rely on it. (define (stop-solver-process!) - (when (unbox server-state) - ((Server-ports-shutdown (unbox server-state))) + (define unboxed (unbox server-state)) + (when unboxed + ((Server-ports-shutdown unboxed)) (set-box! server-state #f))) ; Print version number, so students know to update (define (print-version-number) - (when (and no-version-printed-yet (@>= (get-verbosity) VERBOSITY_LOW)) + (when (and no-version-printed-yet (>= (get-verbosity) VERBOSITY_LOW)) (set! no-version-printed-yet #f) (printf "Forge version: ~a~n" forge-version) (let* ([git-info (forge-git-info)] @@ -78,85 +214,96 @@ "https://report.forge-fm.org"))) -; send-to-solver :: Run-spec -> Stream, List +; In case of error, highlight an AST node if able. Otherwise, focus on the offending run command. +; Never returns; we don't use the #:raise? #f option of raise-forge-error. +(: raise-run-error (->* (String Syntax) ( (U False node) ) Nothing)) +(define (raise-run-error message run-command [node #f]) + (if node + (raise-forge-error #:msg message + #:context (nodeinfo-loc (node-info node))) + (raise-forge-error #:msg message + #:context run-command))) + ; Given a Run-spec structure, processes the data and communicates it to KodKod-CLI; ; then produces a stream to produce instances generated by KodKod, ; along with a list of all of the atom names for sig atoms. +; (values results +; all-atoms +; (unbox server-state) +; (Kodkod-current (length run-constraints) 0 0) +; ; This becomes the "kodkod-bounds" field of the Run that is eventually created. + ; total-bounds) +(: send-to-solver (->* (Run-spec Syntax) (#:run-name Symbol) + (Values tree:node (Listof FAtom) Server-ports Kodkod-current (Listof bound)))) (define (send-to-solver run-spec run-command #:run-name [run-name (gensym)]) (do-time "send-to-solver") - ; In case of error, highlight an AST node if able. Otherwise, focus on the offending run command. - (define (raise-run-error message [node #f]) - (if node - (raise-forge-error #:msg message - #:context (nodeinfo-loc (node-info node))) - (raise-forge-error #:msg message - #:context run-command))) - (when (member run-name (unbox run-name-history)) - (raise-run-error (format "Run name ~a was re-used; please use a different run name.~n" run-name))) + (raise-run-error (format "Run name ~a was re-used; please use a different run name.~n" run-name) run-command)) (set-box! run-name-history (cons run-name (unbox run-name-history))) (print-version-number) - - ; Do relation breaks from declarations - (define relation-constraints - (apply append - (for/list ([relation (get-relations run-spec)]) - (match (Relation-breaker relation) - [#f (list)] - ['default (list)] - ['pfunc (let* ([rel relation] - [sigs (map (lambda (sig-thunk) (sig-thunk)) - (Relation-sigs-thunks relation))] - [left-sig (get-sig run-spec (first sigs))] - [sig-rel left-sig]) - (list (all ([s sig-rel]) - (lone (join s rel)))))] - [other (break relation other) - (list)])))) + + ; Set up breakers on each relation. These may arise from declaration multiplicities like "lone" + ; or from partial-instance annotations like "is linear". + ; TODO TYPES: really? what about relations declared pfunc / is linear together? + ; ** THIS MUST BE DONE BEFORE COMPUTING BOUNDS! ** + (for ([relation (get-relations run-spec)]) + ;(printf "applying constraints for ~a; ~a ~n" relation (Relation-breaker relation)) + ; Built-ins like int successor ("succ") can have #f as their break. + (define the-breaker (Relation-breaker relation)) + (when the-breaker + (break-rel relation the-breaker))) ; Produce bounds from scopes (define-values (sig-to-bound relation-to-bound all-atoms) - (get-bounds run-spec raise-run-error)) + (get-bounds run-spec run-command)) ; Get new bounds and constraints from breaks - (define-values (total-bounds break-preds) - (let* ([sig-bounds (map (compose (curry hash-ref sig-to-bound ) - Sig-name) - (get-sigs run-spec))] - [relation-bounds (map (compose (curry hash-ref relation-to-bound ) - Relation-name) - (get-relations run-spec))] + (: total-bounds (Listof bound)) + (define-values (total-bounds break-preds) + (let* ([sigs (get-sigs run-spec)] + [sig-names : (Listof Symbol) (map Sig-name sigs)] + [sig-bounds : (Listof bound) + (map (lambda ([sn : Symbol]) (hash-ref sig-to-bound sn)) + sig-names)] + [relation-bounds : (Listof bound) + (map (lambda ([rel : Relation]) (hash-ref relation-to-bound (Relation-name rel))) + (get-relations run-spec))] [total-bounds (append sig-bounds relation-bounds)] - - [sigs (get-sigs run-spec)] - [sig-rels (filter (lambda (sig) (@not (equal? (Sig-name sig) 'Int))) sigs)] - [upper-bounds (for/hash ([sig sigs]) + [sig-rels (filter (lambda ([sig : Sig]) (not (equal? (Sig-name sig) 'Int))) sigs)] + [upper-bounds (for/hash : (Immutable-HashTable Sig (Listof FAtom)) ([sig sigs]) (values sig - (map car (bound-upper (hash-ref sig-to-bound (Sig-name sig))))))] - [relations-store (for/hash ([relation (get-relations run-spec)] + ((inst map FAtom Tuple) car (bound-upper (hash-ref sig-to-bound (Sig-name sig))))))] + + [relations-store (for/hash : (Immutable-HashTable Relation (Listof Sig)) ([relation (get-relations run-spec)] #:unless (equal? (Relation-name relation) 'succ)) (values relation (get-sigs run-spec relation)))] - [extensions-store (for/hash ([sig sigs] + + [extensions-store (for/hash : (Immutable-HashTable Sig Sig) ([sig sigs] #:when (Sig-extends sig)) - (values sig (get-sig run-spec (Sig-extends sig))))]) + (define extend (Sig-extends sig)) + (define extend-sig (if extend (get-sig run-spec extend) #f)) + (if extend-sig + (values sig extend-sig) + (raise (format "Internal error building extensions-store. Sig was: ~a" sig))))]) ;(printf "args-- total-bounds : ~a~n args-- sig-rels : ~a~n args-- upper-bounds : ~a~n" total-bounds sig-rels upper-bounds ) (constrain-bounds total-bounds sig-rels upper-bounds relations-store extensions-store))) ;(printf "after-- total-bounds : ~a~n" total-bounds) + ; Because the breaker module is stateful, we need to clear out that state for the next run. (clear-breaker-state) (define sigs-and-rels (append (State-sig-order (Run-spec-state run-spec)) (State-relation-order (Run-spec-state run-spec)))) - (set! total-bounds (map (lambda (name) - (findf (lambda (b) + (set! total-bounds (filter-map (lambda (name) + (findf (lambda ([b : bound]) (equal? name (string->symbol (relation-name (bound-relation b))))) total-bounds)) sigs-and-rels)) - (when (@>= (get-verbosity) VERBOSITY_DEBUG) + (when (>= (get-verbosity) VERBOSITY_DEBUG) (displayln "--------------------------") (printf "Original PBindings: ~n~a~n~n" (Bound-pbindings (Run-spec-bounds run-spec))) (printf "sig-to-bound: ~n~a~n~n" sig-to-bound) @@ -173,13 +320,14 @@ ; Initializing our backend process, and getting ports for communication with it. ; This was originally just Kodkod; some of that terminology remains. (define backend (get-option run-spec 'backend)) + (define unboxed (unbox server-state)) (define-values (stdin stdout stderr shutdown is-running?) (cond ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; if there is an active server state, and the server is running - [(and (unbox server-state) ((Server-ports-is-running? (unbox server-state)))) - (define sstate (unbox server-state)) - (when (@> (get-verbosity) VERBOSITY_LOW) + [(and unboxed ((Server-ports-is-running? unboxed))) + (define sstate unboxed) + (when (> (get-verbosity) VERBOSITY_LOW) (printf "~a solver process already running. Preparing to start new run with id ~a.~n" backend run-name)) (values (Server-ports-stdin sstate) (Server-ports-stdout sstate) (Server-ports-stderr sstate) (Server-ports-shutdown sstate) @@ -196,7 +344,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; Backend=Pardinus; server isn't active/running [(equal? backend 'pardinus) - (when (@>= (get-verbosity) VERBOSITY_HIGH) + (when (>= (get-verbosity) VERBOSITY_HIGH) (printf "Starting/restarting Pardinus server (prior state=~a)...~n" (unbox server-state))) (pardinus:start-server 'stepper ; always a stepper problem (there is a "next" button) @@ -209,13 +357,14 @@ [else (raise (format "Invalid backend: ~a" backend))])) ; Confirm that if the user is invoking a custom solver, that custom solver exists - (define solverspec (cond [(symbol? (get-option run-spec 'solver)) - (get-option run-spec 'solver)] - [else (string-append "\"" (get-option run-spec 'solver) "\"")])) - (unless (or (symbol? (get-option run-spec 'solver)) - (file-exists? (get-option run-spec 'solver))) - (raise-user-error (format "option solver specified custom solver (via string): ~a, but file did not exist." - (get-option run-spec 'solver)))) + (define solver-option (get-option run-spec 'solver)) + (define solverspec (cond [(symbol? solver-option) + solver-option] + [else (string-append "\"" solver-option "\"")])) + (unless (symbol? solver-option) + (unless (file-exists? solver-option) + (raise-user-error (format "option solver specified custom solver (via string): ~a, but file did not exist." + solver-option)))) ; Print configure and declare univ size ; Note that target mode is passed separately, nearer to the (solve) invocation @@ -226,18 +375,18 @@ ;; Generate top-level constraint for this run, execute last-checker ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (: maybe-alwaysify (-> node/formula node/formula)) (define (maybe-alwaysify fmla) (if (equal? 'temporal (get-option run-spec 'problem_type)) - (always/info (node-info fmla) fmla) + (always/func #:info (node-info fmla) fmla) fmla)) ; If in temporal mode, need to always-ify the auto-generated constraints but not the ; predicates that come from users (define raw-implicit-constraints - (append (get-sig-size-preds run-spec sig-to-bound #:error raise-run-error) + (append (get-sig-size-preds run-spec run-command sig-to-bound) (get-relation-preds run-spec) (get-extender-preds run-spec) - relation-constraints break-preds)) (define conjuncts-implicit-constraints (apply append (map maybe-and->list raw-implicit-constraints))) @@ -249,7 +398,7 @@ (append explicit-constraints implicit-constraints)) ; Run last-minute checks for errors - (for-each (lambda (c) + (for-each (lambda ([c : node/formula]) (checkFormula run-spec c '() (get-checker-hash))) run-constraints) @@ -262,13 +411,13 @@ (begin (define-values (all-rels core-map) (send-to-cvc5-tor run-name run-spec bitwidth all-atoms solverspec total-bounds bound-lower bound-upper run-constraints stdin stdout stderr)) - (lambda (mode) (get-next-cvc5-tor-model is-running? run-name all-rels all-atoms core-map stdin stdout stderr mode + (lambda ([mode : String]) (get-next-cvc5-tor-model is-running? run-name all-rels all-atoms core-map stdin stdout stderr mode #:run-command run-command)))] [(equal? backend 'pardinus) (begin (define-values (all-rels core-map) (send-to-kodkod run-name run-spec bitwidth all-atoms solverspec total-bounds bound-lower bound-upper run-constraints stdin stdout stderr)) - (lambda (mode) (get-next-kodkod-model is-running? run-name all-rels all-atoms core-map stdin stdout stderr mode)))] + (lambda ([mode : String]) (get-next-kodkod-model is-running? run-name all-rels all-atoms core-map stdin stdout stderr mode)))] [else (raise (format "Invalid backend: ~a" backend))])) @@ -276,36 +425,47 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; DO NOT ADD MORE MESSAGES TO SOLVER AFTER THIS POINT ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + + (: next-button (-> String tree:node)) (define (next-button type) - (tree:make-node (get-next-model type) next-button)) + (tree:make-node/func get-next-model type next-button)) + (: results tree:node) (define results - (tree:make-node (get-next-model 'start) next-button)) + (tree:make-node/func get-next-model "start" next-button)) - (set-box! server-state (Server-ports stdin stdout stderr shutdown is-running?)) + (define new-server-state (Server-ports stdin stdout stderr shutdown is-running?)) + (set-box! server-state new-server-state) (values results all-atoms - (unbox server-state) + new-server-state (Kodkod-current (length run-constraints) 0 0) ; This becomes the "kodkod-bounds" field of the Run that is eventually created. total-bounds)) +(: int-range (-> Integer Integer (Listof Integer))) +(define (int-range start excluded-end) + (if (< excluded-end start) + empty + (build-list (@- excluded-end start) (lambda ([idx : Integer]) (@+ idx start))))) -(define (get-bounds run-spec raise-run-error) +(: get-bounds (-> Run-spec Syntax + (Values (HashTable Symbol bound) (HashTable Symbol bound) (Listof FAtom)))) +(define (get-bounds run-spec run-command) ; Send user defined partial bindings to breaks (map instance (hash-values (Bound-pbindings (Run-spec-bounds run-spec)))) ; Get KodKod names, min sets, and max sets of Sigs and Relations (define-values (sig-to-bound all-atoms) ; Map, List - (get-sig-bounds run-spec raise-run-error)) + (get-sig-bounds run-spec run-command)) (define relation-to-bound ; Map - (get-relation-bounds run-spec sig-to-bound raise-run-error)) + (get-relation-bounds run-spec run-command sig-to-bound)) (values sig-to-bound relation-to-bound all-atoms)) ; Produce a single AST node to blame for a given relation's bound, or #f if none available +(: get-blame-node (-> Run-spec node (U node False))) (define (get-blame-node run-spec the-rel) (cond [(or (not (node/expr/relation? the-rel)) (not (Run-spec? run-spec))) @@ -317,53 +477,86 @@ ; get-sig-bounds :: Run-spec -> Map, List ; Given a Run-spec, assigns names to each sig, assigns minimum and maximum ; sets of atoms for each, and find the total number of atoms needed (including ints). -(define (get-sig-bounds run-spec raise-run-error) +(: get-sig-bounds (-> Run-spec Syntax (Values (HashTable Symbol bound) (Listof FAtom)))) +(define (get-sig-bounds run-spec run-command) ;;;;; Helpers for extracting declared relational bounds from the run-spec (define pbindings (Bound-pbindings (Run-spec-bounds run-spec))) - (define (get-bound-lower sig) + + (: get-bound-lower (-> Sig (U (Listof FAtom) False))) + (define (get-bound-lower [sig : Sig]) + (: pbinding (U False sbound)) (define pbinding (hash-ref pbindings sig #f)) - (@and pbinding ;; !!! - (map car (set->list (sbound-lower pbinding))))) - (define (get-bound-upper sig) + (and pbinding ;; !!! + ((inst map FAtom Tuple) car (set->list (sbound-lower pbinding))))) + + (: get-bound-upper (-> Sig (U (Listof FAtom) False))) + (define (get-bound-upper [sig : Sig]) + (: pbinding (U False sbound)) (define pbinding (hash-ref pbindings sig #f)) - (@and pbinding + (and pbinding (sbound-upper pbinding) - (map car (set->list (sbound-upper pbinding))))) + ((inst map FAtom Tuple) car (set->list (sbound-upper pbinding))))) ;;;;; Helpers for extracting declared numeric scopes from the run-spec (define scopes (Run-spec-scope run-spec)) + + (: get-scope-lower (-> Sig (U False Integer))) (define (get-scope-lower sig) (define scope (hash-ref (Scope-sig-scopes scopes) (Sig-name sig) #f)) - (@and scope (Range-lower scope))) + (and scope (Range-lower scope))) + + (: get-scope-upper (-> Sig (U False Integer))) (define (get-scope-upper sig) (define scope (hash-ref (Scope-sig-scopes scopes) (Sig-name sig) #f)) - (@and scope (Range-upper scope))) + (and scope (Range-upper scope))) + + (: get-scope-lower-default (-> Sig Integer)) (define (get-scope-lower-default sig) - (let ([actual (get-scope-lower sig)]) - (or actual - (Range-lower (or (Scope-default-scope scopes) - DEFAULT-SIG-SCOPE))))) + (let* ([actual (get-scope-lower sig)] + [local-default (Scope-default-scope scopes)] + [maybe-default-global-lower (Range-lower DEFAULT-SIG-SCOPE)] + [maybe-local-default-int (if local-default (Range-lower local-default) #f)]) + (cond [actual actual] + [maybe-local-default-int maybe-local-default-int] + [maybe-default-global-lower maybe-default-global-lower] + [else (raise-run-error (format "Internal error (~a): no lower bound in DEFAULT-SIG-SCOPE" sig) + run-command + (get-blame-node run-spec sig))]))) + + (: get-scope-upper-default (-> Sig Integer)) (define (get-scope-upper-default sig) - (let ([actual (get-scope-upper sig)]) - (or actual - (Range-upper (or (Scope-default-scope scopes) - DEFAULT-SIG-SCOPE))))) + (let* ([actual (get-scope-upper sig)] + [local-default (Scope-default-scope scopes)] + [maybe-default-global-upper (Range-upper DEFAULT-SIG-SCOPE)] + [maybe-local-default-int (if local-default (Range-upper local-default) #f)]) + (cond [actual actual] + [maybe-local-default-int maybe-local-default-int] + [maybe-default-global-upper maybe-default-global-upper] + [else (raise-run-error (format "Internal error (~a): no upper bound in DEFAULT-SIG-SCOPE" sig) + run-command + (get-blame-node run-spec sig))]))) ; Map; keeps track of what the "next" generated atom ID should be + (: curr-atom-number (HashTable Symbol Integer)) (define curr-atom-number (make-hash)) - ; Sig -> Listof; the atom names declared by the user in a partial instance + ; The atom names declared by the user in a partial instance + (: all-user-atoms (Listof FAtom)) (define all-user-atoms - (apply append (for/list ([sig (get-sigs run-spec)] + (apply append (for/list : (Listof (Listof FAtom)) ([sig (get-sigs run-spec)] #:when (hash-has-key? pbindings sig)) - (define bound (hash-ref pbindings sig)) - (map car (set->list (@or (sbound-upper bound) (sbound-lower bound))))))) + (: the-bound sbound) + (define the-bound (hash-ref pbindings sig)) + (: the-set (Setof Tuple)) + (define the-set (or (sbound-upper the-bound) (sbound-lower the-bound))) + ((inst map FAtom Tuple) car (set->list the-set))))) ; Generate the "next" atom ID for a given sig, based on what's been generated/declared so far + (: get-next-name (-> Sig Symbol)) (define (get-next-name sig) - (define atom-number (add1 (hash-ref curr-atom-number (Sig-name sig) -1))) + (define atom-number (add1 (hash-ref curr-atom-number (Sig-name sig) (lambda () -1)))) (let loop ([atom-number atom-number]) (hash-set! curr-atom-number (Sig-name sig) atom-number) (define new-name (string->symbol (format "~a~a" (Sig-name sig) atom-number))) @@ -372,16 +565,20 @@ new-name))) ; Generate new names for sig + (: generate-names (-> Sig Integer (Listof Symbol))) (define (generate-names sig num) - (map (thunk* (get-next-name sig)) (range num))) + (map (lambda (_) (get-next-name sig)) (range num))) ; Overall bounds data structures, will be modified as this procedure executes + (: lower-bounds (HashTable Sig (Listof FAtom))) (define lower-bounds (make-hash)) + (: upper-bounds (HashTable Sig (Listof FAtom))) (define upper-bounds (make-hash)) ; Helper to populate a sig's lower bound based on relational bound given ; If any #:one children lack tuple-based lower bounds, there is a risk of inconsistency ; since those children must receive a fresh atom name to denote (and for #:one sigs, LB=UB) + (: fill-lower-by-bound (-> Sig (Listof FAtom))) (define (fill-lower-by-bound sig) (define children-lowers (apply append (map fill-lower-by-bound (get-children run-spec sig)))) @@ -391,15 +588,18 @@ (when (and (not curr-lower) (Sig-one sig)) ;; TODO: issue here is we would rather report the ancestor too, and ideally the stxloc for the bind (raise-run-error (format "Example or inst named members for an ancestor of 'one' sig ~a but no member name was given for ~a. This can result in inconsistency; please give bounds for ~a." (Sig-name sig) (Sig-name sig) (Sig-name sig)) + run-command (get-blame-node run-spec sig))) + (define true-lower (remove-duplicates (append children-lowers - (@or curr-lower (list))))) + (or curr-lower (list))))) (hash-set! lower-bounds sig true-lower) true-lower) ; Helper to populate a lower bound based on a numeric scope given + (: fill-lower-by-scope (-> Sig (Listof FAtom))) (define (fill-lower-by-scope sig) (define children-lowers (apply append (map fill-lower-by-scope (get-children run-spec sig)))) @@ -414,32 +614,38 @@ (hash-set! lower-bounds sig true-lower) true-lower) + (: fill-upper-with-bound (->* (Sig) ((U (Listof FAtom) False)) Void)) (define (fill-upper-with-bound sig [parent-upper #f]) (define curr-upper (get-bound-upper sig)) (if curr-upper (let () (hash-set! upper-bounds sig curr-upper) - (map (lambda (child) (fill-upper-with-bound child curr-upper)) - (get-children run-spec sig))) + (for ([child : Sig (get-children run-spec sig)]) + (fill-upper-with-bound child curr-upper))) (fill-upper-past-bound sig parent-upper))) - + + (: fill-upper-past-bound (-> Sig (U (Listof FAtom) False) Void)) (define (fill-upper-past-bound sig parent-upper) (when (get-bound-upper sig) (raise-run-error (format "Please specify an upper bound for ancestors of ~a." (Sig-name sig)) - (get-blame-node run-spec sig))) - (hash-set! upper-bounds sig parent-upper) - (map (lambda (child) (fill-upper-past-bound child parent-upper)) - (get-children run-spec sig))) + run-command (get-blame-node run-spec sig))) + (if parent-upper + (hash-set! upper-bounds sig parent-upper) + (raise (format "internal error: parent-upper for ~a was absent" sig))) + (for ([child : Sig (get-children run-spec sig)]) + (fill-upper-past-bound child parent-upper))) ; For use in situations where there is no existing upper (relational) bound + (: fill-upper-no-bound (-> Sig (Listof FAtom) Void)) (define (fill-upper-no-bound sig shared) ; If the sig has a relational upper bound, don't try to resolve the possible ; atom names etc.; ask the user to give an explicit bound on the parent, too. (when (get-bound-upper sig) (raise-run-error (format "Please specify an upper bound for ancestors of ~a." (Sig-name sig)) - (get-blame-node run-spec sig))) - (define curr-lower (hash-ref lower-bounds sig)) + run-command (get-blame-node run-spec sig))) + + (define curr-lower (ann (hash-ref lower-bounds sig) (Listof FAtom))) ; Before doing anything else, confirm that if *no* scope was given for this sig, ; that the declared scopes for its children, combined, are not bigger than the default. @@ -451,7 +657,7 @@ (@max (length curr-lower) (get-scope-upper-default sig))) (define child-upper-declared-total - (foldl (lambda (curr acc) + (foldl (lambda ([curr : Sig] [acc : Integer]) (@+ acc (or (get-scope-upper curr) 0))) 0 (get-children run-spec sig))) @@ -461,19 +667,22 @@ However, the total of declared and inferred child-sig scopes was ~a. \ Please declare a sufficient scope for ~a." (Sig-name sig) upper-budget child-upper-declared-total (Sig-name sig)) + run-command (get-blame-node run-spec sig)))) ; If the upper-bound's scope is bigger than the lower bound's current contents ; (which should include child sigs' lower bounds), make room using atoms from parent. ; Otherwise, upper = lower, since there is no excess capacity. - (if (@> (get-scope-upper-default sig) (length curr-lower)) + (if (> (get-scope-upper-default sig) (length curr-lower)) (hash-set! upper-bounds sig (append curr-lower shared)) (hash-set! upper-bounds sig curr-lower)) ; Recur on children - (map (lambda (child) (fill-upper-no-bound child (append curr-lower shared))) + (for-each (lambda ([child : Sig]) + (fill-upper-no-bound child (append curr-lower shared))) (get-children run-spec sig))) ; List of all atoms that come from sigs, except Int. Will change as this procedure runs. + (: sig-atoms (Listof FAtom)) (define sig-atoms (list)) ; Start with each top-level sig @@ -497,6 +706,7 @@ Please declare a sufficient scope for ~a." ; root (get-scope-upper root) (get-scope-upper-default root)) ; Generate new names + (: shared (Listof Symbol)) (define shared (generate-names root (@- upper-size lower-size))) ; This function is also responsible for validating totals (we didn't go over budget) (fill-upper-no-bound root shared))) @@ -504,12 +714,17 @@ Please declare a sufficient scope for ~a." (set! sig-atoms (append sig-atoms (hash-ref upper-bounds root)))) ; Set the bounds for the Int built-in sig + (: int-atoms (Listof FAtom)) (define int-atoms (let* ([bitwidth (get-bitwidth run-spec)] - [max-int (expt 2 (sub1 bitwidth))]) - (range (@- max-int) max-int))) - (hash-set! lower-bounds (get-sig run-spec Int) int-atoms) - (hash-set! upper-bounds (get-sig run-spec Int) int-atoms) + [max-int (floor (expt 2 (sub1 bitwidth)))]) + (int-range (@- max-int) max-int))) + + ; We have access to Int, but be cautious + (define int-sig (get-sig run-spec Int)) + (when int-sig + (hash-set! lower-bounds int-sig int-atoms) + (hash-set! upper-bounds int-sig int-atoms)) ; Special case: allow sigs to extend Int. (define int-extenders (get-children run-spec Int)) @@ -520,6 +735,7 @@ Please declare a sufficient scope for ~a." (define all-atoms (append int-atoms sig-atoms)) ; for ease of understanding, just sort by first atom + (: tuple Tuple Tuple Boolean)) (define (tuple (define bounds-hash - (for/hash ([sig (get-sigs run-spec)]) + (for/hash : (HashTable Symbol bound) ([sig (get-sigs run-spec)]) (let* ([name (Sig-name sig)] [rel sig] - [lower (map list (hash-ref lower-bounds sig))] + [lower (map (inst list FAtom) (hash-ref lower-bounds sig))] ; Override generated upper bounds for #:one sigs, unless they extend Int ; (In this case, we cannot generate an arbitrary atom for them, since Int atoms ; have semantic value -- i.e., they are not isomorphic.) @@ -540,10 +756,11 @@ Please declare a sufficient scope for ~a." (cond [(and (Sig-one sig) (not (member sig int-extenders))) lower] [else - (map list (hash-ref upper-bounds sig))])]) + (map (inst list FAtom) (hash-ref upper-bounds sig))])]) ;(printf "bounds-hash at ~a; lower = ~a; upper = ~a; non-one upper = ~a~n" rel lower upper (hash-ref upper-bounds sig)) (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) + run-command (get-blame-node run-spec sig))) (values name (bound rel (sort (remove-duplicates lower) tuple Run-spec Syntax (HashTable Symbol bound) (HashTable Symbol bound))) +(define (get-relation-bounds run-spec run-command sig-to-bound) + (: pbindings (HashTable node/expr/relation sbound)) (define pbindings (Bound-pbindings (Run-spec-bounds run-spec))) + (: piecewise PiecewiseBounds) (define piecewise (Bound-piecewise (Run-spec-bounds run-spec))) + (: get-bound-lower (-> node/expr/relation (U False (Setof Tuple)))) (define (get-bound-lower rel) (define pbinding (hash-ref pbindings rel #f)) - (@and pbinding + (and pbinding (sbound-lower pbinding))) + + (: get-bound-upper (-> node/expr/relation (U False (Setof Tuple)))) (define (get-bound-upper rel) - (define pbinding (hash-ref pbindings rel #f)) - (@and pbinding - (sbound-upper pbinding) + (define pbinding (ann (hash-ref pbindings rel #f) (U False sbound))) + (and pbinding + (sbound-upper pbinding) ;; TODO why duplicate? (sbound-upper pbinding))) + (: get-bound-piecewise (-> node/expr/relation (U False PiecewiseBound))) (define (get-bound-piecewise rel) (hash-ref piecewise rel #f)) (define without-succ - (for/hash ([relation (get-relations run-spec)] + (for/hash : (HashTable Symbol bound) ([relation (get-relations run-spec)] #:unless (equal? (Relation-name relation) 'succ)) + (: sigs (Listof Sig)) (define sigs (get-sigs run-spec relation)) - (define sig-atoms (map (compose (curry map car ) - bound-upper - (curry hash-ref sig-to-bound ) - Sig-name) + ; Types: compose is supposed to be varargs! + ; (define sig-atoms (map (compose (curry map car) + ; bound-upper + ; (curry hash-ref sig-to-bound) + ; Sig-name) + ; sigs)) + + (define sig-atoms (map (lambda ([a-sig : Sig]) + (define sig-name (Sig-name a-sig)) + (: upper-tups (Listof Tuple)) + (define upper-tups (bound-upper (hash-ref sig-to-bound sig-name))) + (map (lambda ([tup : Tuple]) (car tup)) + upper-tups)) sigs)) ;(printf "~a: sig-atoms : ~a~n" relation sig-atoms) ;(printf "~a: raw upper : ~a~n" relation (get-bound-upper relation)) ;(printf "~a: raw lower : ~a~n" relation (get-bound-lower relation)) - + (: upper (Listof Tuple)) (define upper - (let ([bound-upper (get-bound-upper relation)] - [bound-piecewise (get-bound-piecewise relation)]) + (let ([upper-bound-value (get-bound-upper relation)] + [piecewise-bound-value (get-bound-piecewise relation)]) (cond - [(and bound-piecewise bound-upper) + [(and piecewise-bound-value upper-bound-value) ; Error condition -- should never have both complete and piecewise on the same relation (raise-run-error (format "~a upper-bound had both complete and piecewise components, could not resolve them." - relation) + relation) run-command (get-blame-node run-spec relation))] - [bound-piecewise + [piecewise-bound-value ;(printf "upper; bound-piecewise tuples: ~a~n" (PiecewiseBound-tuples bound-piecewise)) ; for each admissible atom (taken from first component of the relation's declaration): ; Where a piecewise entry exists: intersect with cartesian product of restricted universe. ; otherwise: include the full cartesian-product for the restriction outside of that domain - (define pw-domain (PiecewiseBound-atoms bound-piecewise)) + (define pw-domain (PiecewiseBound-atoms piecewise-bound-value)) ;(printf "upper; sig-atoms[domain]: ~a~n" (first sig-atoms)) ;(printf "upper; pw-domain: ~a~n" pw-domain) ; ISSUE: this is pre-eval :/ store post-eval? @@ -612,24 +846,25 @@ Please declare a sufficient scope for ~a." (define undeclared (set->list (set-subtract (list->set pw-domain) (list->set (first sig-atoms))))) (raise-run-error (format "Field ~a was bounded for atom(s): ~a, but the corresponding sig ~a contained only ~a. This might be caused by an inst or example not providing a value or bound for the sig; recall the default scope of ~a through ~a atoms will apply if no scope or bound is given." (Relation-name relation) undeclared (first sigs) (first sig-atoms) (Range-lower DEFAULT-SIG-SCOPE) (Range-upper DEFAULT-SIG-SCOPE)) - (get-blame-node run-spec relation))) + run-command (get-blame-node run-spec relation))) ; TODO: that only helps with the domain, not the range - (define in-domain (set-intersect (list->set (PiecewiseBound-tuples bound-piecewise)) + (define in-domain (set-intersect (list->set (PiecewiseBound-tuples piecewise-bound-value)) (list->set (apply cartesian-product sig-atoms)))) ;(printf "upper; sig-atoms product was: ~a~n" (apply cartesian-product sig-atoms)) ;(printf "upper; in-domain: ~a~n" in-domain) (define out-of-domain (list->set - (filter (lambda (tup) + (filter (lambda ([tup : Tuple] + ) (not (member (first tup) pw-domain))) (apply cartesian-product sig-atoms)))) ;(printf "upper; out-of-domain: ~a~n" out-of-domain) (set->list (set-union in-domain out-of-domain))] - [bound-upper + [upper-bound-value ; complete upper bound exists; intersect with the cartesian product of universe ; restricted to the sig-sequence in relation's declaration - (set->list (set-intersect bound-upper + (set->list (set-intersect upper-bound-value (list->set (apply cartesian-product sig-atoms))))] [else ; no upper-bound given, default to cartesian product of universe, restricted @@ -637,39 +872,47 @@ Please declare a sufficient scope for ~a." (apply cartesian-product sig-atoms)]))) ;(define upper (set->list (set-intersect (get-bound-upper relation) (list->set (apply cartesian-product sig-atoms))))) - ;(printf "~a: refined upper : ~a~n" relation upper) ; Piecewise lower bounds were handled in sigs-functional, before send-to-solver is called. (define lower (let ([bound-lower (get-bound-lower relation)]) (if bound-lower (set->list (set-union bound-lower (list->set empty))) - (list->set empty)))) + empty))) ;(define lower (set->list (set-union (get-bound-lower relation) (list->set empty)))) + ;(printf "~a:~nrefined upper: ~a~nrefined lower: ~a~n" relation upper lower) (unless (subset? (list->set lower) (list->set upper)) (raise-run-error (format "Bounds inconsistency detected for field ~a: lower bound was ~a, which is not a subset of upper bound ~a." (Relation-name relation) lower upper) + run-command (get-blame-node run-spec relation))) (values (Relation-name relation) (bound relation lower upper)))) - (define ints (map car (bound-upper (hash-ref sig-to-bound 'Int)))) - (define succ-tuples (map list (reverse (rest (reverse ints))) (rest ints))) + (: upper-on-int (Listof Tuple)) + (define upper-on-int (bound-upper (hash-ref sig-to-bound 'Int))) + (: ints (Listof FAtom)) + (define ints (map (ann car (-> Tuple FAtom)) upper-on-int)) + (: succ-tuples (Listof (Listof FAtom))) + ;; TODO: this relies on getting the right ordering on unary Int tuples, doesn't it? + (define succ-tuples (map + (inst list FAtom) + (reverse (rest (reverse ints))) (rest ints))) (hash-set without-succ 'succ (bound succ succ-tuples succ-tuples))) ; get-sig-size-preds :: Run-spec -> List ; Creates assertions for each Sig to restrict ; it to the correct lower/upper bound. -(define (get-sig-size-preds run-spec sig-to-bound #:error raise-run-error) +(: get-sig-size-preds (-> Run-spec Syntax (HashTable Symbol bound) (Listof node/formula))) +(define (get-sig-size-preds run-spec run-command sig-to-bound) (define max-int (expt 2 (sub1 (get-bitwidth run-spec)))) - (apply append - (for/list ([sig (get-sigs run-spec)] + (define lists (for/list : (Listof (Listof node/formula)) ([sig (get-sigs run-spec)] #:unless (equal? (Sig-name sig) 'Int)) (match-define (bound rel bound-lower bound-upper) (hash-ref sig-to-bound (Sig-name sig))) (define-values (bound-lower-size bound-upper-size) (values (length bound-lower) (length bound-upper))) (match-define (Range int-lower int-upper) - (hash-ref (Scope-sig-scopes (Run-spec-scope run-spec)) (Sig-name sig) (Range #f #f))) + (hash-ref (Scope-sig-scopes (Run-spec-scope run-spec)) (Sig-name sig) (lambda () (Range #f #f)))) ; Sub-optimal, because it points to the sig definition (define info (nodeinfo (nodeinfo-loc (node-info sig)) 'checklangNoCheck #f)) @@ -679,28 +922,31 @@ Please declare a sufficient scope for ~a." ; in how bounds should be resolved. e.g., sig A {} sig B extends A {} ; run {} for 4 A, 3 B. (append - (if (@and int-lower (@> int-lower bound-lower-size)) + (if (and int-lower (> int-lower bound-lower-size)) (let () - (unless (@< int-lower max-int) + (unless (< int-lower max-int) (raise-run-error (format (string-append "Lower bound too large for given BitWidth; " "Sig: ~a, Lower-bound: ~a, Max-int: ~a") sig int-lower (sub1 max-int)) + run-command (get-blame-node run-spec sig))) - (list (||/info info - (int Run-spec (Listof node/formula))) (define (get-extender-preds run-spec) - (define sig-constraints (for/list ([sig (get-sigs run-spec)]) + (: sig-constraints (Listof (Listof node/formula))) + (define sig-constraints (for/list : (Listof (Listof node/formula)) ([sig (get-sigs run-spec)]) ; get children information + (: children-rels (Listof Sig)) (define children-rels (get-children run-spec sig)) - ; abstract and sig1, ... extend => (= sig (+ sig1 ...)) ; not abstract and sig is parent of sig1 => (in sig1 sig) ; TODO: optimize by identifying abstract sigs as sum of children + (: abstract (-> Sig (Listof Sig) node/formula)) (define (abstract sig extenders) ; TODO : location not correct - (let ([loc (nodeinfo-loc (node-info sig))]) - (if (@= (length extenders) 1) - (=/info (nodeinfo loc 'checklangNoCheck #f) sig (car extenders)) - (=/info (nodeinfo loc 'checklangNoCheck #f) sig (+ extenders))))) + (let* ([loc (nodeinfo-loc (node-info sig))] + [info (nodeinfo loc 'checklangNoCheck #f)]) + + (if (equal? (length extenders) 1) + (=/func #:info info sig (car extenders)) + (=/func #:info info sig (app-e +/func info extenders))))) + + (: parent (-> Sig Sig node/formula)) (define (parent sig1 sig2) ; loc of sig2? (let ([loc (nodeinfo-loc (node-info sig2))]) - (in/info (nodeinfo loc 'checklangNoCheck #f) sig2 sig1))) + (in/func #:info (nodeinfo loc 'checklangNoCheck #f) sig2 sig1))) + (: extends-constraints (Listof node/formula)) (define extends-constraints (if (and (Sig-abstract sig) (cons? (get-children run-spec sig))) (list (abstract sig children-rels)) @@ -741,20 +995,25 @@ Please declare a sufficient scope for ~a." ; sig1 and sig2 extend sig => (no (& sig1 sig2)) ; (unless both are #:one, in which case exact-bounds should enforce this constraint) + (: disjoin-pair (-> Sig Sig node/formula)) (define (disjoin-pair sig1 sig2) (let* ([loc (nodeinfo-loc (node-info sig2))] [info (nodeinfo loc 'checklangNoCheck #f)]) - (cond [(and (Sig-one sig1) (Sig-one sig2)) true] - [else (no/info info (&/info info sig1 sig2))]))) + (cond [(and (Sig-one sig1) (Sig-one sig2)) true-formula] + [else (no/func #:info info (&/func #:info info sig1 sig2))]))) + + (: disjoin-list (-> Sig (Listof Sig) (Listof node/formula))) (define (disjoin-list a-sig a-list) (map (curry disjoin-pair a-sig) a-list)) + + (: disjoin (-> (Listof Sig) (Listof node/formula))) (define (disjoin a-list) (if (empty? a-list) empty (append (disjoin-list (first a-list) (rest a-list)) (disjoin (rest a-list))))) + (: disjoint-constraints (Listof node/formula)) (define disjoint-constraints (disjoin children-rels)) - (append extends-constraints disjoint-constraints))) ; combine all constraints together @@ -763,11 +1022,12 @@ Please declare a sufficient scope for ~a." ; get-relation-preds :: Run-spec -> List ; Creates assertions for each Relation to ensure that it does not ; contain any atoms which don't populate their Sig. +(: get-relation-preds (-> Run-spec (Listof node/formula))) (define (get-relation-preds run-spec) - (for/list ([relation (get-relations run-spec)]) + (for/list : (Listof node/formula) ([relation (get-relations run-spec)]) (define sig-rels (get-sigs run-spec relation)) (define info (nodeinfo (nodeinfo-loc (node-info relation)) 'checklangNoCheck #f)) - (in/info info relation (->/info info sig-rels)))) + (in/func #:info info relation (app-e ->/func info sig-rels)))) #| diff --git a/forge/shared.rkt b/forge/shared.rkt index 975e25853..66fe95ad7 100644 --- a/forge/shared.rkt +++ b/forge/shared.rkt @@ -1,26 +1,49 @@ -#lang racket/base +#lang typed/racket/base/optional (require racket/runtime-path racket/file) -(require (only-in racket/draw color%) - (only-in racket make-object) - (only-in racket/system system*) +(require (only-in racket/system system*) (only-in racket/string string-trim) (only-in racket/port call-with-output-string) (only-in pkg/lib pkg-directory)) -(require racket/stream) -(require net/http-easy - json - base64) +(require typed/net/base64) +(require (only-in typed/net/url URL)) + +(define-type FAtom (U Symbol Integer)) +(define-type Tuple (Listof FAtom)) +(provide FAtom Tuple) + +(require/typed json + [#:opaque JSExpr jsexpr?] + [string->jsexpr (-> String JSExpr)] + [jsexpr->string (-> JSExpr String)]) + +(require/typed pkg/lib + [pkg-directory (->* (String) (#:cache (U False (HashTable Any Any))) (U Path-String False))]) + +(require/typed net/http-easy + [#:opaque Response response?] + [response-body (-> Response Bytes)] + [response-status-code (-> Response Integer)] + [get (->* ( (U Bytes String URL) ) + ( #:close? Boolean + #:stream? Boolean + #:headers (HashTable Symbol (U Bytes String)) + #:params (Listof (Pairof Symbol (U False String))) + #:auth (U False Procedure) ;; more specific in reality + #:data Any + #:form Any + #:json Any + #:timeouts Any + #:max-attempts Any + #:max-redirects Any + #:user-agent Any) + Response)]) (provide get-verbosity set-verbosity VERBOSITY_LOW VERBOSITY_STERLING VERBOSITY_HIGH VERBOSITY_DEBUG VERBOSITY_LASTCHECK get-temp-dir) -(provide forge-version forge-git-info instance-diff CORE-HIGHLIGHT-COLOR curr-forge-version) -(provide stream-map/once port-echo java>=1.9? do-time) - -(module+ test (require rackunit)) - -(define CORE-HIGHLIGHT-COLOR (make-object color% 230 150 150)) +(provide forge-version forge-git-info instance-diff curr-forge-version) +(provide port-echo java>=1.9? do-time) ; Level of output when running specs (define VERBOSITY_SCRIPT 0) ; for test scripts @@ -33,29 +56,45 @@ (define VERBOSITY_LASTCHECK 1) (define verbosityoption VERBOSITY_LOW) + ; for accessing verbosity in other modules +(: get-verbosity (-> Integer)) (define (get-verbosity) verbosityoption) +(: set-verbosity (-> Integer Void)) (define (set-verbosity x) (set! verbosityoption x)) (define-runtime-path info-path "info.rkt") +(: forge-version String) (define forge-version "x.x.x") + (with-handlers ([exn:fail? (λ (exn) (println exn))]) (define info-str (file->string info-path)) + ; A strange type, but cadr/second will pull out the appropriate string + (: parts (U (Pairof String (Listof (U False String))) False)) (define parts (regexp-match #px"define\\s+version\\s+\"(\\S+)\"" info-str)) - (set! forge-version (cadr parts)) -) + ; Typed Racket had trouble with doing this narrowing with one cond. + (cond [(not parts) (set! forge-version "UNKNOWN")] + [else + (define the-str (cadr parts)) + (if the-str + (set! forge-version the-str) + (set! forge-version "UNKNOWN"))])) (define (forge-git-info) (with-handlers ([exn:fail? void]) (define windows? (eq? (system-type) 'windows)) + (: git-exe (U False Path)) (define git-exe (find-executable-path (if windows? "git.exe" "git"))) - (parameterize ([current-directory (pkg-directory "forge")]) - (map - string-trim - (list - (shell git-exe '("rev-parse" "--abbrev-ref" "HEAD")) - (shell git-exe '("rev-parse" "--short" "HEAD")) - (shell git-exe '("log" "-1" "--format=%cd"))))))) + (define forge-dir (pkg-directory "forge")) + (if (or (not forge-dir) (not git-exe)) + (raise "Could not find Forge package installed on the system.") + (parameterize ([current-directory forge-dir]) + (map + string-trim + (list + (shell git-exe '("rev-parse" "--abbrev-ref" "HEAD")) + (shell git-exe '("rev-parse" "--short" "HEAD")) + (shell git-exe '("log" "-1" "--format=%cd")))))))) ; Returns temp directory for files (define (get-temp-dir) @@ -71,28 +110,32 @@ "tnelson" "Forge" "forge/info.rkt")) - (define response (get URL)) (if (= (response-status-code response) 200) (let* ([body (response-body response)] - [json-data (string->jsexpr (bytes->string/utf-8 body))] - [content (hash-ref json-data 'content)] - [decoded-content (bytes->string/utf-8 (base64-decode (string->bytes/utf-8 content)))] - [version (regexp-match #px"\\(define version \"([0-9]+[.0-9]+)\"\\)" decoded-content)]) - (car (cdr version))) + [json-data (string->jsexpr (bytes->string/utf-8 body))]) + (define content (if (hash? json-data) (hash-ref json-data 'content) #f)) + (define decoded-content (bytes->string/utf-8 (base64-decode (string->bytes/utf-8 + (if (string? content) content ""))))) + (define version (regexp-match #px"\\(define version \"([0-9]+[.0-9]+)\"\\)" decoded-content)) + (if (list? version) + (car (cdr version)) + void)) void))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(define-type InstanceHash (HashTable Symbol (Listof Tuple))) ; Returns the difference of two instances (> and < separately) +(: instance-diff (-> InstanceHash InstanceHash (List Symbol (Listof Any) (Listof Any)))) (define (instance-diff i1 i2) (if (equal? (hash-keys i1) (hash-keys i2)) (list 'same-signature - (hash-map i1 (lambda (k v) + (hash-map i1 (lambda ([k : Symbol] [v : (Listof Tuple)]) (list k (filter (lambda (ele) (not (member ele (hash-ref i2 k)))) v)))) - (hash-map i2 (lambda (k v) + (hash-map i2 (lambda ([k : Symbol] [v : (Listof Tuple)]) (list k (filter (lambda (ele) (not (member ele (hash-ref i1 k)))) v))))) (list @@ -100,45 +143,53 @@ (filter (lambda (k) (not (member k (hash-keys i2)))) (hash-keys i1)) (filter (lambda (k) (not (member k (hash-keys i1)))) (hash-keys i2))))) -(define (stream-map/once func strm) - (stream-cons (func (stream-first strm)) - (stream-map/once func (stream-rest strm)))) - +(: port-echo (->* (Input-Port Output-Port) (#:title String) Void)) (define (port-echo in-port out-port #:title [title #f]) (when title (fprintf out-port "~a logs:~n" title)) (for ([ln (in-lines in-port)]) (displayln ln out-port))) +(: java>=1.9? (-> Path-String Boolean)) (define (java>=1.9? java-exe) (define version-str (shell java-exe "-version")) (java-version>=1.9? version-str java-exe)) +(: java-version>=1.9? (-> String (U False Path-String) Boolean)) (define (java-version>=1.9? version-str java-exe) + (: m0 (U False (Pairof String (Listof (U False String))))) + (define m0 (regexp-match #rx"(java|openjdk) version \"([^\"]+)\"" version-str)) + + ; Needed to do this step-by-step; (and ...) wasn't working to narrow. + (define maybe-vstr (if m0 (caddr m0) "")) + (define vstr (if maybe-vstr maybe-vstr "")) + (define m1 (or (regexp-match #rx"^([0-9]+)(\\.[0-9]+\\.)?" vstr) + (raise-arguments-error 'forge/shared + "Error checking Java version" + "java exe" java-exe + "version string" version-str))) + (define major (cadr m1)) + (define minor (caddr m1)) + + (: major-nums (List (U Number False) (U Number False))) (define major-nums - (let* ([m0 (regexp-match #rx"(java|openjdk) version \"([^\"]+)\"" version-str)] - [vstr (if m0 (caddr m0) "")] - [m1 (or - (regexp-match #rx"^([0-9]+)(\\.[0-9]+\\.)?" vstr) - (raise-arguments-error 'forge/shared - "Error checking Java version" - "java exe" java-exe - "version string" version-str))] - [major (cadr m1)] - [minor (caddr m1)]) - (list (string->number major) - (if minor (string->number (substring minor 1 (sub1 (string-length minor)))) 0)))) - (or (and (= 1 (car major-nums)) - (<= 9 (cadr major-nums))) - (<= 9 (car major-nums)))) - -(module+ test + (list (if major (string->number major) #f) + (if minor (string->number (substring minor 1 (sub1 (string-length minor)))) 0))) + ; Note on types: <= requires a *Real* number, not just a Number. + (or (and (number? (car major-nums)) (= 1 (car major-nums)) + (real? (cadr major-nums)) (<= 9 (cadr major-nums))) + (and (real? (car major-nums)) (<= 9 (car major-nums))))) + +(module+ test (require typed/rackunit)) +(module+ test (test-case "java-version" (check-true (java-version>=1.9? "openjdk version \"17\" 2021-09-14" #f)) (check-false (java-version>=1.9? "openjdk version \"1.8.0_242\"\nOpenJDK Runtime Environment (build 1.8.0_242-b08)" #f)) (check-false (java-version>=1.9? "java version \"1.8.0_65\"\nJava(TM) SE Runtime Environment" #f)))) +(: shell (-> Path-String (U (Listof String) String) String)) (define (shell exe pre-cmd) + (: success? (Boxof Boolean)) (define success? (box #f)) (define cmd* (if (string? pre-cmd) (list pre-cmd) pre-cmd)) (define str @@ -157,36 +208,48 @@ (define do-time (let () + (: last-time (Option Integer)) (define last-time #f) + (: initial-time (Option Integer)) (define initial-time #f) + (: gc-time (Option Integer)) (define gc-time #f) + (: set!-initial-time (-> Integer Void)) (define (set!-initial-time t) (set! initial-time t)) + (: set!-last-time (-> Integer Void)) (define (set!-last-time t) (set! last-time t)) + (: set!-gc-time (-> Integer Void)) (define (set!-gc-time t) (set! gc-time t)) (define pad-len 40) + + (: pad (-> String Char String)) (define (pad str pad-char) (define l (string-length str)) (if (>= l pad-len) str (string-append str (make-string (- pad-len l) pad-char)))) + (define (start-timing msg) (when last-time (error 'start-timing "Timing already started")) (set!-last-time (current-process-milliseconds)) - (set!-initial-time last-time) + (set!-initial-time (current-process-milliseconds)) (set!-gc-time (current-gc-milliseconds)) (log-forge-timing-debug "~a at ~a" (pad "Starting" #\space) initial-time)) - (lambda (msg) + + (lambda ([msg : String]) (unless last-time (start-timing msg)) - (log-forge-timing-debug - (let* ([t (current-process-milliseconds)] - [gc (current-gc-milliseconds)] - [old last-time] - [diff (- t old)] - [gc-diff (- gc gc-time)] - [new-msg (pad msg #\space)]) - (set!-last-time t) - (set!-gc-time gc) + (define t (current-process-milliseconds)) + (define gc (current-gc-milliseconds)) + (define old last-time) + (define diff (if old (- t old) #f)) + (define new-msg (pad msg #\space)) + ;; TODO TYPES why did I need the (runtime checked) assertions? + (define gc-diff (if (exact-integer? gc-time) (- gc (assert gc-time exact-integer?)) #f)) + (define init-diff (if (exact-integer? initial-time) (- t (assert initial-time exact-integer?)) #f)) + (set!-last-time t) + (set!-gc-time gc) + (log-forge-timing-debug (format "~a at ~a\tlast step: ~a\tgc: ~a\ttotal: ~a" - new-msg t diff gc-diff (- t initial-time))))))) \ No newline at end of file + new-msg t diff gc-diff init-diff))))) \ No newline at end of file diff --git a/forge/sigs-functional.rkt b/forge/sigs-functional.rkt index 5540e6321..2ad33304f 100644 --- a/forge/sigs-functional.rkt +++ b/forge/sigs-functional.rkt @@ -48,7 +48,8 @@ (provide Int succ) (provide (prefix-out forge: make-model-generator)) (provide solution-diff) -(provide reset-run-name-history! stop-solver-process!) +(provide ;reset-run-name-history! + stop-solver-process!) ; ; Instance analysis functions ; (provide is-sat? is-unsat?) @@ -366,9 +367,9 @@ [(node/breaking/break _ breaker) breaker] [_ (fail "is")])) (match left - [(? node/expr/relation?) (break left right)] + [(? node/expr/relation?) (break-rel left right)] [(node/expr/op/~ info arity (list left-rel)) - (break left-rel (get-co right))] + (break-rel left-rel (get-co right))] [_ (fail "is")]) (values scope bound)] diff --git a/forge/sigs.rkt b/forge/sigs.rkt index 6408ef9ee..6ce211546 100644 --- a/forge/sigs.rkt +++ b/forge/sigs.rkt @@ -41,14 +41,13 @@ make-check test-from-state make-test - reset-run-name-history! stop-solver-process!)) (require forge/choose-lang-specific) ; Commands (provide sig relation fun const pred inst with) (provide run check test example display execute start-sterling-menu) -(provide instance-diff solution-diff evaluate) +(provide solution-diff evaluate) ; Instance analysis functions (provide is-unsat? is-sat? is-unknown?) diff --git a/forge/temporal/lang/reader.rkt b/forge/temporal/lang/reader.rkt index 6f77a9193..6751bfa2c 100644 --- a/forge/temporal/lang/reader.rkt +++ b/forge/temporal/lang/reader.rkt @@ -10,7 +10,6 @@ (require (only-in forge/lang/reader generic-forge-reader)) ;(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/temporal/lang/reader") diff --git a/forge/tests/forge-core/examples/ast-parsing/skolem-test.rkt b/forge/tests/forge-core/examples/ast-parsing/skolem-test.rkt index ceffec3f0..34db2eab6 100644 --- a/forge/tests/forge-core/examples/ast-parsing/skolem-test.rkt +++ b/forge/tests/forge-core/examples/ast-parsing/skolem-test.rkt @@ -5,7 +5,7 @@ (require (prefix-in @ (only-in rackunit check))) (require (only-in racket remove-duplicates)) -(set-verbosity 2) +;(set-verbosity 2) (run run-statement #:preds []) diff --git a/forge/tests/forge/relations/breakers.frg b/forge/tests/forge/relations/breakers.frg index 988eea1bc..6dcda250d 100644 --- a/forge/tests/forge/relations/breakers.frg +++ b/forge/tests/forge/relations/breakers.frg @@ -51,6 +51,7 @@ test expect { linearnoloop: {some a, b: A | (a->b + b->a) in ^(FrontDesk.next)} for {next is linear} is unsat linearnobranch: {some disj a, b, c: A | (a->c + b->c) in FrontDesk.next} for {next is linear} is unsat linearnobranch2: {some disj a, b, c: A | (a->b + a->c) in FrontDesk.next} for {next is linear} is unsat + // Note: as in Alloy, "is linear" enforces exact bounds on that specific type. So empty "next" is excluded. linear_covers_all: {some a: A | {no a.(FrontDesk.next) and no a.~(FrontDesk.next)}} for {next is linear} is unsat ----- test "plinear" ----- diff --git a/forge/types/ast-adapter.rkt b/forge/types/ast-adapter.rkt new file mode 100644 index 000000000..0bdb47251 --- /dev/null +++ b/forge/types/ast-adapter.rkt @@ -0,0 +1,113 @@ +#lang typed/racket/base/optional + +(provide + (struct-out node) + (struct-out node/expr) + (struct-out node/expr/relation) + (struct-out node/breaking) + (struct-out node/breaking/break) + (struct-out nodeinfo) + (struct-out node/formula) + (struct-out node/expr/quantifier-var) + (struct-out node/int) + (struct-out node/int/constant) + relation-arity just-location-info quantified-formula multiplicity-formula empty-nodeinfo + join/func one/func build-box-join univ raise-forge-error &&/func &/func ||/func +/func + -/func =/func */func iden ^/func set/func relation-name always/func maybe-and->list + int=/func int/func + Decl Decls) + +(define-type Decl (Pairof node/expr/quantifier-var node/expr)) +(define-type Decls (Listof Decl)) + +(require/typed forge/lang/ast + [#:struct nodeinfo ([loc : srcloc] [lang : Symbol] [annotations : (Option (Listof Any))])] + [#:struct node ([info : nodeinfo])] + [#:struct (node/int node) ()] + [#:struct (node/int/constant node/int) ([value : Integer])] + [#:struct (node/expr node) ([arity : Number])] + [#:struct (node/breaking node) ()] + [#:struct (node/breaking/break node/breaking) ([break : Symbol])] + [#:struct (node/formula node) ()] + [#:struct (node/expr/quantifier-var node/expr) ([sym : Symbol] [name : Symbol])] + [#:struct (node/expr/relation node/expr) + ([name : String] + [typelist-thunk : (-> (Listof Any))] + [parent : Any] + [is-variable : Boolean])] + + ; (define (functionname #:info [info empty-nodeinfo] . raw-args) // and so on + ; (apply &&/func #:info empty-nodeinfo (list true true true)) + + ; This by itself doesn't allow the type system to differentiate between + ; the #t and #f modes, even when they are provided as literals. + ;(->* (#:msg String #:context Any) (#:raise? Boolean) Void) ] + [raise-forge-error + (case-> + (->* () (#:msg String #:context Any #:raise? True) Nothing) + (->* () (#:msg String #:context Any #:raise? False) Void) + (->* () (#:msg String #:context Any) Nothing))] + [relation-arity (-> Any Integer)] + [relation-name (-> node/expr/relation String)] + [just-location-info (-> (U srcloc #f) nodeinfo)] + [quantified-formula (-> nodeinfo Symbol (Listof Decl) node/formula node/formula)] + [multiplicity-formula (-> nodeinfo Symbol node/expr node/formula)] + [empty-nodeinfo nodeinfo] + ;; ?? which of these is correct? + [join/func (->* (node/expr node/expr) (#:info nodeinfo) node/expr)] + [one/func (->* (node/expr) (#:info nodeinfo) node/formula)] + [lone/func (->* (node/expr) (#:info nodeinfo) node/formula)] + [no/func (->* (node/expr) (#:info nodeinfo) node/formula)] + [&&/func (->* (node/formula) (#:info nodeinfo) #:rest node/formula node/formula)] + [||/func (->* (node/formula) (#:info nodeinfo) #:rest node/formula node/formula)] + [&/func (->* (node/expr) (#:info nodeinfo) #:rest node/expr node/expr)] + [->/func (->* (node/expr) (#:info nodeinfo) #:rest node/expr node/expr)] + [+/func (->* (node/expr) (#:info nodeinfo) #:rest node/expr node/expr)] + [-/func (->* (node/expr node/expr) (#:info nodeinfo) node/expr)] + [=/func (->* (node/expr node/expr) (#:info nodeinfo) node/formula)] + [in/func (->* (node/expr node/expr) (#:info nodeinfo) node/formula)] + [*/func (->* (node/expr) (#:info nodeinfo) node/expr)] + [^/func (->* (node/expr) (#:info nodeinfo) node/expr)] + [set/func (->* ((Listof Decl) node/formula) (#:info nodeinfo) node/expr)] + [always/func (->* (node/formula) (#:info nodeinfo) node/formula)] + [int=/func (->* (node/int node/int) (#:info nodeinfo) node/formula)] + [int* (node/int node/int) (#:info nodeinfo) node/formula)] + [int/func (->* (Integer) (#:info nodeinfo) node/int/constant)] + [card/func (->* (node/expr) (#:info nodeinfo) node/int/constant)] + [build-box-join (-> node/expr (Listof node/expr) node/expr)] + [maybe-and->list (-> node/formula (Listof node/formula))] + [univ node/expr] + [iden node/expr] + ; Don't export these as-is. Potential conflict with existing Racket identifiers. + [(true true-formula) node/formula] + [(false false-formula) node/formula] + ) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-type (ASTConstructor PT RT) (->* (PT) (#:info nodeinfo) #:rest PT RT)) + +; This is a more narrow type than the real type. +(require/typed typed/racket + [keyword-apply (All (PT RT) (-> (ASTConstructor PT RT) (Listof '#:info) (Listof nodeinfo) (Listof PT) RT))]) + +(provide app-f app-e app-i) + +(: app-f (-> (ASTConstructor node/formula node/formula) nodeinfo (Listof node/formula) node/formula)) +(define (app-f func info nodes) + (keyword-apply func '(#:info) (list info) nodes)) +(: app-e (-> (ASTConstructor node/expr node/expr) nodeinfo (Listof node/expr) node/expr)) +(define (app-e func info nodes) + (keyword-apply func '(#:info) (list info) nodes)) +(: app-i (-> (ASTConstructor node/int node/int) nodeinfo (Listof node/int) node/int)) +(define (app-i func info nodes) + (keyword-apply func '(#:info) (list info) nodes)) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +; (: ->immutable/hash (All (K V) (-> (HashTable K V) (Immutable-HashTable K V)))) +; (define (->immutable/hash ht) +; (for/hash ([k v])) +; (hash-map/copy ht (lambda (k v) (values k v)) #:kind 'immutable)) \ No newline at end of file diff --git a/forge/types/lazy-tree-adapter.rkt b/forge/types/lazy-tree-adapter.rkt new file mode 100644 index 000000000..deeeca41a --- /dev/null +++ b/forge/types/lazy-tree-adapter.rkt @@ -0,0 +1,22 @@ +#lang typed/racket/base/optional + +(provide ; (struct-out computation) + ; (struct-out computation/delayed) + (prefix-out tree: (struct-out node)) + (prefix-out tree: make-node/func) + get-checker-hash) + +(require/typed forge/utils/lazy-tree + ; [#:struct computation ()] + ; [#:struct (computation/delayed computation) ([thnk : Any])] + [make-node/func (-> (-> String Any) String (-> String Any) node)] + [#:struct node ( + [datum : Any] + [child-generator : Any] + [children : Any] + [ancestors : Any])]) + +(require (only-in forge/utils/lazy-tree make-node)) + +(require/typed forge/choose-lang-specific + [get-checker-hash (-> (HashTable Any Any))]) diff --git a/forge/utils/lazy-tree.rkt b/forge/utils/lazy-tree.rkt index 896df3d1e..4b6aab791 100644 --- a/forge/utils/lazy-tree.rkt +++ b/forge/utils/lazy-tree.rkt @@ -4,7 +4,10 @@ (require syntax/parse/define) (require (only-in racket empty? match cons? first thunk)) -(provide node? make-node get-child get-children get-value lazy-tree-map is-evaluated?) +(provide node? make-node get-child get-children get-value lazy-tree-map is-evaluated? + make-node/func + ; temporary, until this module is typed + (struct-out computation) (struct-out computation/delayed) (struct-out node)) (struct computation ()) (struct computation/delayed computation (thnk)) @@ -32,6 +35,9 @@ (define-simple-macro (make-node datum child-generator) (node (computation/delayed (thunk datum)) child-generator (make-hash) (list))) +(define (make-node/func datum type child-generator) + (make-node (datum type) child-generator)) + (define/contract (get-value a-node) (node? . -> . any/c) (match (node-datum a-node) diff --git a/forge/utils/stream-utils.rkt b/forge/utils/stream-utils.rkt new file mode 100644 index 000000000..1c09177a4 --- /dev/null +++ b/forge/utils/stream-utils.rkt @@ -0,0 +1,9 @@ +#lang racket/base + +(require (only-in racket/stream stream? stream-empty? empty-stream stream-first stream-rest stream-cons)) +(provide stream-map/once) + +(define (stream-map/once func strm) + (stream-cons + (func (stream-first strm)) + (stream-map/once func (stream-rest strm)))) diff --git a/forge/utils/substitutor.rkt b/forge/utils/substitutor.rkt index 1c59a9d6b..9df037204 100644 --- a/forge/utils/substitutor.rkt +++ b/forge/utils/substitutor.rkt @@ -29,7 +29,7 @@ node? node? node?) - (when (@>= (get-verbosity) 2) + (when (@>= (get-verbosity) VERBOSITY_DEBUG) (printf "substitutor: interpret-formula: ~a~n" formula)) (match formula [(node/formula/constant info type) @@ -86,7 +86,7 @@ ) (define (substitute-formula-op run-or-state formula relations atom-names quantvars args target value) - (when (@>= (get-verbosity) 2) + (when (@>= (get-verbosity) VERBOSITY_DEBUG) (printf "substitutor: interpret-formula-op: ~a~n" formula)) (match formula [(node/formula/op/&& info children) @@ -133,7 +133,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (define (substitute-expr run-or-state expr relations atom-names quantvars target value) - (when (@>= (get-verbosity) 2) + (when (@>= (get-verbosity) VERBOSITY_DEBUG) (printf "substitutor: interpret-expr: ~a~n" expr)) (if (equal? expr target) value @@ -174,7 +174,7 @@ (node/expr/comprehension info len new-decls processed-form))]))) (define (substitute-expr-op run-or-state expr relations atom-names quantvars args target value) - (when (@>= (get-verbosity) 2) + (when (@>= (get-verbosity) VERBOSITY_DEBUG) (printf "substitutor: interpret-expr-op: ~a~n" expr)) (match expr [(node/expr/op/+ info arity children) @@ -206,7 +206,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (define (substitute-int run-or-state expr relations atom-names quantvars target value) - (when (@>= (get-verbosity) 2) + (when (@>= (get-verbosity) VERBOSITY_DEBUG) (printf "substitutor: interpret-int: ~a~n" expr)) ; TEMP fix to match int variables. Should probably modify process-children-int to handle constants. (if (equal? expr target) value @@ -231,7 +231,7 @@ (node/int/sum-quant info new-decls processed-int))]))) (define (substitute-int-op run-or-state expr relations atom-names quantvars args target value) - (when (@>= (get-verbosity) 2) + (when (@>= (get-verbosity) VERBOSITY_DEBUG) (printf "substitutor: interpret-int-op: ~a~n" expr)) (match expr [(node/int/op/add info children) diff --git a/forge/utils/to-skolem.rkt b/forge/utils/to-skolem.rkt index 8420d3a49..87e8dfe0a 100644 --- a/forge/utils/to-skolem.rkt +++ b/forge/utils/to-skolem.rkt @@ -47,7 +47,7 @@ run-spec total-bounds formula relations atom-names quantvars quantvar-types info decls form #:tag-with-spacer [tag-with-spacer #f]) - (when (@> (get-verbosity) VERBOSITY_LOW) + (when (@>= (get-verbosity) VERBOSITY_DEBUG) (printf "skolemize-formula-helper: ~a ~a~n" formula quantvars)) ; RESTRICTION: Because we are mapping top-level sigs to sorts, we have no "univ". ; Discuss. May be better to not use sorts (or worse). @@ -120,7 +120,7 @@ ; only one type (first upper-bound-list) ; otherwise, build product - (apply cartesian-product upper-bound-list))) + (apply cartesian-product (map (lambda (sublist) (apply append sublist)) upper-bound-list)))) ;(printf "~nskolem-upper-bound: ~a~n" skolem-upper-bound) ; 4. add that new relation to the bounds @@ -183,7 +183,7 @@ list?) (#:tag-with-spacer boolean?) (values node? list?)) - (when (@>= (get-verbosity) 2) + (when (@>= (get-verbosity) VERBOSITY_DEBUG) (printf "to-skolem: interpret-formula: ~a~n" formula)) (set! current-bounds total-bounds) ; no "kodkod-bounds" yet; the Run hasn't been created (define resulting-formula @@ -257,7 +257,7 @@ [(? node/int? i) (interpret-int run-or-state total-bounds i relations atom-names quantvars quantvar-types #:tag-with-spacer tag-with-spacer)]))) (define (interpret-formula-op run-spec total-bounds formula relations atom-names quantvars quantvar-types args #:tag-with-spacer [tag-with-spacer #f]) - (when (@>= (get-verbosity) 2) + (when (@>= (get-verbosity) VERBOSITY_DEBUG) (printf "to-skolem: interpret-formula-op: ~a~n" formula)) (match formula [(node/formula/op/&& info children) @@ -304,7 +304,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (define (interpret-expr run-spec total-bounds expr relations atom-names quantvars quantvar-types #:tag-with-spacer [tag-with-spacer #f]) - (when (@>= (get-verbosity) 2) + (when (@>= (get-verbosity) VERBOSITY_DEBUG) (printf "to-skolem: interpret-expr: ~a~n" expr)) (match expr [(node/expr/relation info arity name typelist-thunk parent isvar) @@ -344,7 +344,7 @@ (node/expr/comprehension info len new-decls processed-form))])) (define (interpret-expr-op run-spec total-bounds expr relations atom-names quantvars quantvar-types args #:tag-with-spacer [tag-with-spacer #f]) - (when (@>= (get-verbosity) 2) + (when (@>= (get-verbosity) VERBOSITY_DEBUG) (printf "to-skolem: interpret-expr-op: ~a~n" expr)) (match expr [(node/expr/op/+ info arity children) @@ -375,7 +375,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (define (interpret-int run-spec total-bounds expr relations atom-names quantvars quantvar-types #:tag-with-spacer [tag-with-spacer #f]) - (when (@>= (get-verbosity) 2) + (when (@>= (get-verbosity) VERBOSITY_DEBUG) (printf "to-skolem: interpret-int: ~a~n" expr)) (match expr [(node/int/constant info value) @@ -398,7 +398,7 @@ (node/int/sum-quant info new-decls processed-int))])) (define (interpret-int-op run-spec total-bounds expr relations atom-names quantvars quantvar-types args #:tag-with-spacer [tag-with-spacer #f]) - (when (@>= (get-verbosity) 2) + (when (@>= (get-verbosity) VERBOSITY_DEBUG) (printf "to-skolem: interpret-int-op: ~a~n" expr)) (match expr [(node/int/op/add info children)