diff --git a/e2e/README.md b/e2e/README.md new file mode 100644 index 00000000..62fb58cc --- /dev/null +++ b/e2e/README.md @@ -0,0 +1,5 @@ +# Forge models for end-to-end testing + +These models aren't meant to illustrate any particular concept, but rather are used for +end-to-end testing of the Sterling<->Forge<->Solver workflow. They may use unusual syntax, +unsafe features, etc. diff --git a/e2e/fail_assertion.frg b/e2e/fail_assertion.frg new file mode 100644 index 00000000..4746a801 --- /dev/null +++ b/e2e/fail_assertion.frg @@ -0,0 +1,16 @@ +#lang forge + +option no_overflow true // disallow integer overflow + +sig Pigeon {location: one Pigeonhole} +sig Pigeonhole {} + +pred some_roommates { + some disj p1, p2: Pigeon | p1.location = p2.location +} +-- This should pass; we don't expect Sterling to open at all. +assert {#Pigeon > #Pigeonhole} is sufficient for some_roommates +-- This should fail; we expect Sterling to open with **only one command**, +-- and for the instance to auto-load. **The evaluator should be usable**. +assert {#Pigeon >= #Pigeonhole} is sufficient for some_roommates + diff --git a/e2e/failing_decls_example.frg b/e2e/failing_decls_example.frg new file mode 100644 index 00000000..b46455d3 --- /dev/null +++ b/e2e/failing_decls_example.frg @@ -0,0 +1,21 @@ +#lang forge + +option no_overflow true // disallow integer overflow + +sig Pigeon {location: one Pigeonhole} +sig Pigeonhole {} + +pred some_roommates { + some disj p1, p2: Pigeon | p1.location = p2.location +} + +// This fails because the instance given violates the type definitions +// The solver yields unsat, so Sterling should not open. +example threePigeons is {some_roommates} for { + Pigeon = `Pigeon0 + `Pigeon1 + `Pigeon2 + Pigeonhole = `Pigeonhole0 + `Pigeonhole1 + // This violates the type declarations: + location = `Pigeon0 -> (`Pigeonhole0 + `Pigeonhole1) + + `Pigeon1 -> `Pigeonhole0 + + `Pigeon2 -> `Pigeonhole0 +} diff --git a/e2e/failing_example.frg b/e2e/failing_example.frg new file mode 100644 index 00000000..15fa8c15 --- /dev/null +++ b/e2e/failing_example.frg @@ -0,0 +1,19 @@ +#lang forge + +option no_overflow true // disallow integer overflow + +sig Pigeon {location: one Pigeonhole} +sig Pigeonhole {} + +pred some_roommates { + some disj p1, p2: Pigeon | p1.location = p2.location +} + +// This fails. Since the solver has yielded unsat, Sterling shouldn't open. +example threePigeons is {not some_roommates} for { + Pigeon = `Pigeon0 + `Pigeon1 + `Pigeon2 + Pigeonhole = `Pigeonhole0 + `Pigeonhole1 + location = `Pigeon0 -> `Pigeonhole0 + + `Pigeon1 -> `Pigeonhole0 + + `Pigeon2 -> `Pigeonhole1 +} diff --git a/e2e/passing_example.frg b/e2e/passing_example.frg new file mode 100644 index 00000000..c8f1c3d0 --- /dev/null +++ b/e2e/passing_example.frg @@ -0,0 +1,18 @@ +#lang forge + +option no_overflow true // disallow integer overflow + +sig Pigeon {location: one Pigeonhole} +sig Pigeonhole {} + +pred some_roommates { + some disj p1, p2: Pigeon | p1.location = p2.location +} + +example threePigeons is some_roommates for { + Pigeon = `Pigeon0 + `Pigeon1 + `Pigeon2 + Pigeonhole = `Pigeonhole0 + `Pigeonhole1 + location = `Pigeon0 -> `Pigeonhole0 + + `Pigeon1 -> `Pigeonhole0 + + `Pigeon2 -> `Pigeonhole1 +} diff --git a/e2e/sat_pass_unsat_pass_2_runs.frg b/e2e/sat_pass_unsat_pass_2_runs.frg new file mode 100644 index 00000000..9e18e9de --- /dev/null +++ b/e2e/sat_pass_unsat_pass_2_runs.frg @@ -0,0 +1,19 @@ +#lang forge + +option no_overflow true // disallow integer overflow + +sig Pigeon {location: one Pigeonhole} +sig Pigeonhole {} + +pred some_roommates { + some disj p1, p2: Pigeon | p1.location = p2.location +} +test expect { + -- This is satisfiable, and so should appear in the run menu. + not_vacuous: {#Pigeon > #Pigeonhole} is sat + -- This is unsatisfiable, and so wouldn't be useful to visualize. + should_be_unsat: {Pigeon != Pigeon} is unsat +} + +see_principle_1: run {} for exactly 5 Pigeon, exactly 4 Pigeonhole +see_principle_2: run {} for exactly 4 Pigeon, exactly 3 Pigeonhole diff --git a/forge/examples/lights_puzzle/ring_of_lights.frg b/forge/examples/lights_puzzle/ring_of_lights.frg index 19bd540c..1f614cc3 100644 --- a/forge/examples/lights_puzzle/ring_of_lights.frg +++ b/forge/examples/lights_puzzle/ring_of_lights.frg @@ -2,6 +2,7 @@ option run_sterling "lights.js" + /* When using the custom vis script, remember to click "Run" after asking for a new trace or config! (the script doesn't re-run automatically) diff --git a/forge/info.rkt b/forge/info.rkt index d1df1ce7..25de11fe 100644 --- a/forge/info.rkt +++ b/forge/info.rkt @@ -69,6 +69,6 @@ #rx"tests/forge-core/*" #rx"tests/forge-functional/*" "tests/error/" - #rx"domains/abac/tests/*" + #rx"domains/abac/*" #rx"domains/crypto/examples/*" "OLD")) diff --git a/forge/pardinus-cli/server/kks.rkt b/forge/pardinus-cli/server/kks.rkt index a2633d2d..1c1ebfe5 100755 --- a/forge/pardinus-cli/server/kks.rkt +++ b/forge/pardinus-cli/server/kks.rkt @@ -19,12 +19,12 @@ (define server-name "Pardinus") (provide start-server) ; stdin stdout) -(define (start-server [solver-type 'stepper] [solver-subtype 'default]) +(define (start-server [solver-type 'stepper] [solver-subtype 'default] [java-exe #f]) (when (>= (get-verbosity) VERBOSITY_HIGH) (printf "Starting ~a server.~n" server-name)) (define kks (new server% [name server-name] - [initializer (thunk (pardinus-initializer solver-type solver-subtype))])) + [initializer (thunk (pardinus-initializer solver-type solver-subtype java-exe))])) (send kks initialize) (define stdin-val (send kks stdin)) (define stderr-val (send kks stderr)) diff --git a/forge/pardinus-cli/server/pardinus-server.rkt b/forge/pardinus-cli/server/pardinus-server.rkt index 09c4d5f2..957f8d1e 100755 --- a/forge/pardinus-cli/server/pardinus-server.rkt +++ b/forge/pardinus-cli/server/pardinus-server.rkt @@ -10,7 +10,7 @@ (define-runtime-path pardinus (build-path "..")) -(define (pardinus-initializer solver-type solver-subtype) +(define (pardinus-initializer solver-type solver-subtype java-exe) (unless (member solver-type '(incremental stepper)) (raise (format "Invalid solver type: ~a" solver-type))) @@ -19,7 +19,9 @@ (filter (curry regexp-match #rx".+\\.jar") (directory-list pardinus/jar)))] [windows? (equal? (system-type) 'windows)] - [java (find-executable-path (if windows? "java.exe" "java"))] + [java (if (and java-exe (> (string-length java-exe) 0)) + (build-path java-exe) + (find-executable-path (if windows? "java.exe" "java")))] [path-separator (if windows? ";" ":")] [cp (foldl string-append "" (add-between (map path->string jars) path-separator))] ;[lib (path->string (build-path pardinus/jni (case (system-type) @@ -27,7 +29,7 @@ ;[(unix) "linux_x86_64"] ;[(windows) "win_x86_64"])))] ;[-Djava.library.path (string-append "-Djava.library.path=" lib)] - [error-out (build-path (find-system-path 'home-dir) "error-output.txt")]) + [error-out (build-path (find-system-path 'home-dir) "forge-pardinus-error-output.txt")]) (when (> (get-verbosity) VERBOSITY_LOW) (printf " Starting solver process. subtype: ~a~n" solver-subtype)) @@ -37,6 +39,9 @@ [(equal? solver-subtype 'temporal) "-temporal"] [(equal? solver-subtype 'default) ""] [else (error (format "Bad solver subtype: ~a" solver-subtype))])) + + (unless (file-exists? java) + (raise-user-error 'start-server "Could not find a Java executable. Given or inferred location was: ~a. Type was: ~a" java (file-or-directory-type java))) (when (>= (get-verbosity) VERBOSITY_HIGH) (printf " Subprocess invocation information: ~a~n" diff --git a/forge/send-to-solver.rkt b/forge/send-to-solver.rkt index 219c15b6..528bf8e8 100644 --- a/forge/send-to-solver.rkt +++ b/forge/send-to-solver.rkt @@ -190,7 +190,9 @@ 'stepper ; always a stepper problem (there is a "next" button) ; 'default, 'temporal, or 'target (tells Pardinus which solver to load, ; and affects parsing so needs to be known at invocation time) - (get-option run-spec 'problem_type))] + (get-option run-spec 'problem_type) + ; control version of java used (by path string) + (get-option run-spec 'java_exe_location))] [else (raise (format "Invalid backend: ~a" backend))])) diff --git a/forge/server/forgeserver.rkt b/forge/server/forgeserver.rkt index d097f603..8682dc69 100644 --- a/forge/server/forgeserver.rkt +++ b/forge/server/forgeserver.rkt @@ -71,7 +71,9 @@ (define returned-instance (tree:get-value current-tree)) (set-box! (Run-last-sterling-instance the-run) returned-instance) returned-instance) - (define (get-next-instance [next-mode 'P]) + (define (get-next-instance [next-mode 'P]) + (when (@>= (get-verbosity) VERBOSITY_LOW) + (printf "Solving for next instance.~n")) (set! current-tree (tree:get-child current-tree next-mode)) (set! curr-datum-id (+ curr-datum-id 1)) ; get-current-instance updates the Run's last sterling instance cursor when called @@ -190,26 +192,12 @@ #:port (get-option the-run 'sterling_port) #:confirmation-channel chan)) (define port (async-channel-get chan)) - (cond [(string? port) - (displayln "NO PORTS AVAILABLE. Unable to start web server and Sterling visualizer.")] - [(equal? 'off (get-option the-run 'run_sterling)) - (void)] - [else - ; Attempt to open a browser to the Sterling index.html, with the proper port - ; If this cannot be opened for whatever reason, keep the server open but print - ; a warning, allowing the user a workaround. - (with-handlers ([exn? - (lambda (e) (printf "Racket could not open a browser on your system; you may be able manually navigate to this address, which is where Forge expects Sterling to load:~n ~a~n" - (string-append (path->string sterling-path) "?" (number->string port))))]) - (send-url/file sterling-path #f #:query (number->string port))) - - (printf "Sterling running. Hit enter to stop service.\n") - (when (> (get-verbosity) VERBOSITY_LOW) - (printf "Using port: ~a~n" (number->string port))) - (flush-output) - (void (read-char)) - ; Once a character is read, stop the server - (stop-service)])) + (when (string? port) + (printf "NO PORTS AVAILABLE. Could not start provider server.~n")) + + ; Now, serve the static sterling website files (this will be a different server/port). + (unless (equal? 'off (get-option state-for-run 'run_sterling)) + (serve-sterling-static #:provider-port port))) (define (make-sterling-data xml id run-name temporal? not-done? [old-id #f]) (jsexpr->string @@ -249,7 +237,7 @@ 'payload (hash 'id (->string id) 'result (->string result))))) -(define/contract (make-sterling-meta defined-run-names) +(define/contract (make-sterling-meta included-run-names) (-> (listof symbol?) string?) (jsexpr->string (hash 'type "meta" @@ -257,7 +245,7 @@ 'payload (hash 'name "Forge" 'evaluator #t 'views (list "graph" "table" "script") - 'generators (map ->string defined-run-names))))) + 'generators (map ->string included-run-names))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Infrastructure for starting up sterling in "command selector" mode @@ -268,6 +256,17 @@ (define runmap (State-runmap curr-state)) (define defined-run-names (hash-keys runmap)) + ; Filter out runs that are not useful to visualize, like tests that failed due to unsat. + ; ASSUME: non-tests (e.g., `run`) won't have been invoked yet. + ; It is *VITAL* that `or` short-circuits, since Sat? will invoke the solver if needed. + (define useful-run-names (filter + (lambda (rn) + (define this-run (hash-ref runmap rn)) + ; Include if this run hasn't been solved yet, or if it's solved and sat. + (or (not (tree:is-evaluated? (Run-result this-run))) + (is-sat? this-run))) + defined-run-names)) + ; Assumption: if Sterling is the source of instance requests, there will be no ; instance requests seen from any other sources. @@ -278,7 +277,7 @@ (when (> (get-verbosity) VERBOSITY_LOW) (printf "Starting Sterling in command-selection mode...~n") - (printf "Available commands: ~a~n" defined-run-names)) + (printf "Available commands: ~a~n" useful-run-names)) (define (send-to-sterling m #:connection connection) (when (@>= (get-verbosity) VERBOSITY_STERLING) @@ -356,6 +355,9 @@ ; Get the next instance of this run's lazy result tree. Advance the tree pointer. (define (get-next-instance [next-mode 'P]) + (when (@>= (get-verbosity) VERBOSITY_LOW) + (printf "Solving for next instance.~n")) + (define next-tree (get-next-tree next-mode)) (set! curr-datum-id (+ curr-datum-id 1)) @@ -421,7 +423,8 @@ ;;(define xml (get-xml inst)) ;;(define response (make-sterling-data xml id name temporal?)) ;;(send-to-sterling response #:connection connection) - (printf "Ignoring Sterling 'data' request...~n") + (when (@>= (get-verbosity) VERBOSITY_STERLING) + (printf "Ignoring Sterling 'data' request...~n")) ] [(equal? (hash-ref json-m 'type) "eval") ; A message requesting that the provider evaluate some expression @@ -475,7 +478,7 @@ [(equal? (hash-ref json-m 'type) "meta") ; A message requesting data about the data provider, such as the provider's ; name and the types of views it supports. Respond in turn with a meta message. - (send-to-sterling (make-sterling-meta defined-run-names) #:connection connection)] + (send-to-sterling (make-sterling-meta useful-run-names) #:connection connection)] [else (send-to-sterling "BAD REQUEST" #:connection connection) (raise-forge-error @@ -508,5 +511,8 @@ (printf "NO PORTS AVAILABLE. Could not start provider server.~n")) ; Now, serve the static sterling website files (this will be a different server/port). - (unless (equal? 'off (get-option curr-state 'run_sterling)) - (serve-sterling-static #:provider-port port))) \ No newline at end of file + (unless (or (equal? 'off (get-option curr-state 'run_sterling)) + (empty? useful-run-names)) + (serve-sterling-static #:provider-port port)) + (when (empty? useful-run-names) + (printf "There was nothing useful to visualize: all commads were already executed and produced no instances.~n"))) \ No newline at end of file diff --git a/forge/server/serve-sterling-static.rkt b/forge/server/serve-sterling-static.rkt index 1756c184..891d886f 100644 --- a/forge/server/serve-sterling-static.rkt +++ b/forge/server/serve-sterling-static.rkt @@ -57,7 +57,7 @@ e))]) (send-url sterling-url)) - (printf "Opening Forge menu in Sterling (static server port=~a). Press enter to stop Forge.~n" port) + (printf "Opening Forge menu in Sterling (static server port=~a). Press enter to stop Forge (or click 'Stop' in VSCode).~n" port) (flush-output) ; On Windows, this blocks all Racket threads, which delays output until input is read. diff --git a/forge/shared.rkt b/forge/shared.rkt index e6e2ddcd..aea30574 100644 --- a/forge/shared.rkt +++ b/forge/shared.rkt @@ -149,7 +149,7 @@ (set-box! success? (apply system* exe cmd*)))))) (if (unbox success?) str - (raise-user-error 'shell "failed to apply '~a' to arguments '~a'" exe cmd*))) + (raise-user-error 'shell "failed to apply '~a' to arguments '~a': got ~a" exe cmd* (unbox success?)))) ;; --- timing diff --git a/forge/sigs-structs.rkt b/forge/sigs-structs.rkt index e0d5ab6a..e0c7318c 100644 --- a/forge/sigs-structs.rkt +++ b/forge/sigs-structs.rkt @@ -169,6 +169,7 @@ ; -- DEFAULT_OPTIONS ; -- symbol->proc ; -- option-types +; -- option-types-names ; -- state-set-option (in sigs.rkt) (struct/contract Options ( [eval-language symbol?] @@ -189,6 +190,7 @@ [engine_verbosity nonnegative-integer?] [test_keep symbol?] [no_overflow symbol?] + [java_exe_location (or/c false/c string?)] ) #:transparent) (struct/contract State ( @@ -229,14 +231,17 @@ [name symbol?] [command syntax?] [run-spec Run-spec?] - ; This is the *start* of the exploration tree + ; This is the *start* of the exploration tree. [result tree:node?] [server-ports Server-ports?] [atoms (listof (or/c symbol? number?))] [kodkod-currents Kodkod-current?] [kodkod-bounds (listof any/c)] ; This is Sterling's current cursor into the exploration tree. - ; It is mutated whenever Sterling asks for a new instance. + ; It is mutated whenever Sterling asks for a new instance. We keep this + ; separately, since there may be multiple cursors into the lazy tree if + ; the run is also being processed in a script, but the programmatic cursor + ; and the Sterling cursor should not interfere. [last-sterling-instance (box/c (or/c Sat? Unsat? Unknown? false/c))] ) #:transparent) @@ -249,7 +254,7 @@ ; an engine_verbosity of 1 logs SEVERE level in the Java engine; ; this will send back info about crashes, but shouldn't spam (and possibly overfill) stderr. (define DEFAULT-OPTIONS (Options 'surface 'SAT4J 'pardinus 20 0 0 1 5 'default - 'close-noretarget 'fast 0 'off 'on 0 1 'first 'false)) + 'close-noretarget 'fast 0 'off 'on 0 1 'first 'false #f)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;; Constants ;;;;;;; @@ -282,7 +287,8 @@ 'sterling_port Options-sterling_port 'engine_verbosity Options-engine_verbosity 'test_keep Options-test_keep - 'no_overflow Options-no_overflow)) + 'no_overflow Options-no_overflow + 'java_exe_location Options-java_exe_location)) (define (oneof-pred lst) (lambda (x) (member x lst))) @@ -306,7 +312,8 @@ 'sterling_port exact-nonnegative-integer? 'engine_verbosity exact-nonnegative-integer? 'test_keep (oneof-pred '(first last)) - 'no_overflow (oneof-pred '(false true)))) + 'no_overflow (oneof-pred '(false true)) + 'java_exe_location (lambda (x) (or (equal? x #f) (string? x))))) (define option-types-names (hash 'eval-language "symbol" @@ -326,7 +333,8 @@ 'sterling_port "non-negative integer" 'engine_verbosity "non-negative integer" 'test_keep "one of: first or last" - 'no_overflow "one of: false or true")) + 'no_overflow "one of: false or true" + 'java_exe_location "string")) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/forge/sigs.rkt b/forge/sigs.rkt index eaeca3c4..b517e8d2 100644 --- a/forge/sigs.rkt +++ b/forge/sigs.rkt @@ -276,7 +276,11 @@ [test_keep value])] [(equal? option 'no_overflow) (struct-copy Options options - [no_overflow value])])) + [no_overflow value])] + [(equal? option 'java_exe_location) + (struct-copy Options options + [java_exe_location value])] + )) (struct-copy State state [options new-options])) @@ -642,6 +646,10 @@ ; Primary testing form: check whether a constraint-set, under ; some provided bounds, is sat, unsat, or an error. ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(define (report-passing-test #:name name) + (when (>= (get-verbosity) VERBOSITY_LOW) + (printf " Test passed: ~a~n" name))) + (define-syntax (test stx) (syntax-case stx () [(test name args ... #:expect expected) @@ -688,7 +696,8 @@ #:run run-reference #:sterling #f)) (when (member 'name (hash-keys (State-runmap curr-state))) - (printf "Warning: successful `is forge_error` test run left in state environment: ~a.~n" 'name))] + (printf "Warning: successful `is forge_error` test run left in state environment: ~a.~n" 'name)) + (report-passing-test #:name 'name)] ; It may not be immediately obvious why we would ever test for unknown, ; but it seems reasonable to support it in the engine, regardless. @@ -711,7 +720,8 @@ #:context loc #:instance first-instance #:run name) - (close-run name))] + (begin (report-passing-test #:name 'name) + (close-run name)))] [(equal? 'expected 'checked) ;#,(syntax/loc stx (check name args ...)) @@ -731,8 +741,9 @@ #:context loc #:instance first-instance #:run name)] - [else - (close-run name)])] + [else + (begin (report-passing-test #:name 'name) + (close-run name))])] [(equal? 'expected 'theorem) (raise-forge-error #:msg "The syntax 'is theorem' is deprecated and will be re-enabled in a future version for complete solver backends only; use 'is checked' instead." @@ -784,7 +795,9 @@ #:context #,(build-source-location stx) #:instance first-instance #:run name)])] - [else (close-run name)])))))])) + [else + (report-passing-test #:name 'name) + (close-run name)])))))])) ; Checks that some predicates are always true. (define-syntax (check stx) @@ -1138,11 +1151,18 @@ [else ; Raise a Forge error and stop execution; show Sterling if enabled. (when (>= (get-verbosity) 1) - (printf "Test ~a failed. Stopping execution.~n" name)) - (when (and (Run? run-or-state) sterling) - (true-display run-or-state)) - ;; !!!!! ^^^^ This is a problem! Because the error is raised only after Sterling terminates. - ;; (and this is a single thread only) + (printf "******************** TEST FAILED *******************~nTest ~a failed. Stopping execution.~n" name)) + (cond [(and (Run? run-or-state) sterling (Sat? instance)) + (when (>= (get-verbosity) 1) + (printf "Test failed due to finding a counterexample, which will be displayed in Sterling.~n") + (printf "*****************************************************~n")) + (true-display run-or-state)] + [else + (when (>= (get-verbosity) 1) + (printf "Test failed due to unsat/inconsistency. No counterexample to display.~n") + (printf "*****************************************************~n"))]) + + ;; The error below is raised only after Sterling terminates, so messaging above is vital. (raise-forge-error #:msg msg #:context context)])) ; To be run at the very end of the Forge execution; reports test failures and opens @@ -1253,9 +1273,9 @@ ; Don't allow the Forge file to reset this option. (set-box! option-overrides (cons (string->symbol OPTION-NAME) (unbox option-overrides))))] [("-N" "--notests") - "Disable tests for this model execution" + "Disable tests for this model execution (NOT YET SUPPORTED)" (begin - (printf "Tests disabled.~n") + (printf "(NOT YET SUPPORTED) Tests disabled.~n") (set-box! disable-tests #t))] diff --git a/forge/solver-specific/cvc5-server.rkt b/forge/solver-specific/cvc5-server.rkt index e24f4943..ca397f69 100644 --- a/forge/solver-specific/cvc5-server.rkt +++ b/forge/solver-specific/cvc5-server.rkt @@ -23,7 +23,7 @@ ; assume that cvc5 is on the user's path. (let* ([windows? (equal? (system-type) 'windows)] [path-separator (if windows? ";" ":")] - [error-out (build-path (find-system-path 'home-dir) "error-output.txt")]) + [error-out (build-path (find-system-path 'home-dir) "forge-cvc5-error-output.txt")]) (when (> (get-verbosity) VERBOSITY_LOW) (printf " Starting solver process for ~a. subtype: ~a~n" server-name solver-subtype)) diff --git a/forge/utils/lazy-tree.rkt b/forge/utils/lazy-tree.rkt index 314829e3..896df3d1 100644 --- a/forge/utils/lazy-tree.rkt +++ b/forge/utils/lazy-tree.rkt @@ -4,7 +4,7 @@ (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) +(provide node? make-node get-child get-children get-value lazy-tree-map is-evaluated?) (struct computation ()) (struct computation/delayed computation (thnk)) @@ -18,6 +18,12 @@ (struct node ([datum #:mutable] child-generator children [ancestors #:mutable])) +; Has get-value been called on this node yet? +(define/contract (is-evaluated? a-node) + (node? . -> . any/c) + (match (node-datum a-node) + [(computation/evaluated value) #t] + [else #f])) (define/contract (root-node? node) (any/c . -> . boolean?)