Hey all, This is a Rosette specific question, but I wonder if anyone here has experience with the language and can help make sense of this behavior: Code: #lang rosette (define (what value) (for/all ([w value]) (displayln w))) (define-symbolic b boolean?) Behavior: > (what (if b 1 2)) (ite b 1 2) > (what (if b "a" "b")) a b > (union? (if b "a" "b")) #t > (union? (if b 1 2)) #f

Oh I answered my own question. (if b 1 2) is a solveable type (i.e integer?) so it isnt a union and therefor not expanded by for/all

yes

what does ’truncate mean in call-with-ouputfile ?

like it removes the whitespace n stuf?

There’s a hidden feature in for/all. I don’t recall its syntax exactly, but it looks like:

(for/all ([w value #:exhaustive]) body) This will additionally split on ite.

yup! I was just about to ask what #:exhuastive does under the hood and what the consequences of using it are :stuck_out_tongue:

There’s also another hidden feature, called concrete list

(for/all ([w value (list 1 2)]) body)

This will split over two possibilities: value = 1 and value = 2

that’s awesome!

No, it means “empty” the file quickly before performing the write

thanks @sorawee

np!

what about replace?

It removes the file entirely I think, and then create a new one. IIUC, the identity of the file might not be preserved (I have no idea how filesystem works, but I guess it has something to do with inode or something like that).

See this for more information on these flags: https://docs.racket-lang.org/reference/file-ports.html?q=call-with-output#%28def._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._open-output-file%29%29

Ah, I was handwavy when I talked about “identity”. A more concrete thing to talk about is the metadata attached to the file, like permission.

By using truncate, the metadata would be preserved

By using replace, metadata might not be preserved.