Re: [racket-users] Rosette variable definitions from an s-expression (I'm new to Rosette)

2021-07-12 Thread Sorawee Porncharoenwase 
The recommended way is to write an interpreter to interpret your s-exp.
E.g.,

#lang rosette

(define vars (make-hash))

(define (lookup v)
  (hash-ref! vars v
 (λ ()
   (define-symbolic* a-var integer?)
   a-var)))

(define (interp e)
  (match e
[(? symbol? e) (lookup e)]
[`(> ,a ,b) (> (interp a) (interp b))]))

(define (verify-me e)
  (verify (assert (interp e

(define a-sol (verify-me '(> i j)))

a-sol

(evaluate (interp 'i) a-sol)


On Mon, Jul 12, 2021 at 1:28 PM David Wonnacott 
wrote:

> I'm hoping there are readers of this list who are familiar with Rosette
> , or
> could at least suggest a better place for me to ask such questions.
>
> I'm trying to use Rosette for some symbolic code simplification, and I'd
> like to be able to hand it various expressions that involve sets of
> variables (with types) and sets of assumptions *that I extract from
> s-expressions with other Racket code*.
>
> So, while I could do this:
>
>   #lang rosette/safe
>   (define-symbolic i j integer?)
>   (verify (assert (> i j)))
>
> or even this:
>
>   #lang rosette/safe
>   (define-symbolic i j integer?)
>   (define query (> i j))
>   (verify (assert query))
>
> and have it provide a counter-example model, e.g., i=j=0, I can't do this
> simplified version of what I'm aiming at:
>
>   #lang rosette/safe
>   (define (verify-me query)
> (define-symbolic (symbolics query) integer?)
> (verify (assert query)))
>   (verify-me '(> i j))
>
> Possibly I could do something unpleasant with macros to resolve this,
> though I suspect I'd need to convert a *lot* of other code into macros;
> possibly I could create a collection of fresh symbolics, and then replace
> the things I want to treat as symbolic in "query" with some kind of map.
> But, it didn't seems to me that I was asking for a really unusual usage
> case, so I'm hoping there's a more "normal" way to do this, i.e., to
> extract all names not it (make-base-namespace) from an s-expression and
> then make symbolics for some/all of them as if with define-symbolic.
>
> Perhaps this is easy, or perhaps this is just not something one could do
> with Rosette, or perhaps something in between?
>
> Dave W
>
> --
> You received this message because you are subscribed to the Google Groups
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to racket-users+unsubscr...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/racket-users/6d45e35e-dbef-43f9-bf5c-318c6f25f557n%40googlegroups.com
> 
> .
>

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/CADcuegszRmCFaDS%2BpAaCXmap30_nQLYwei-LseQOQSGRGRvbDg%40mail.gmail.com.

[racket-users] Rosette variable definitions from an s-expression (I'm new to Rosette)

2021-07-12 Thread David Wonnacott 
I'm hoping there are readers of this list who are familiar with Rosette 
, or could 
at least suggest a better place for me to ask such questions.

I'm trying to use Rosette for some symbolic code simplification, and I'd 
like to be able to hand it various expressions that involve sets of 
variables (with types) and sets of assumptions *that I extract from 
s-expressions with other Racket code*.

So, while I could do this:

  #lang rosette/safe
  (define-symbolic i j integer?)
  (verify (assert (> i j)))

or even this:

  #lang rosette/safe
  (define-symbolic i j integer?)
  (define query (> i j))
  (verify (assert query))

and have it provide a counter-example model, e.g., i=j=0, I can't do this 
simplified version of what I'm aiming at:

  #lang rosette/safe
  (define (verify-me query)
(define-symbolic (symbolics query) integer?)
(verify (assert query)))
  (verify-me '(> i j))

Possibly I could do something unpleasant with macros to resolve this, 
though I suspect I'd need to convert a *lot* of other code into macros; 
possibly I could create a collection of fresh symbolics, and then replace 
the things I want to treat as symbolic in "query" with some kind of map. 
But, it didn't seems to me that I was asking for a really unusual usage 
case, so I'm hoping there's a more "normal" way to do this, i.e., to 
extract all names not it (make-base-namespace) from an s-expression and 
then make symbolics for some/all of them as if with define-symbolic.

Perhaps this is easy, or perhaps this is just not something one could do 
with Rosette, or perhaps something in between?

Dave W

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/6d45e35e-dbef-43f9-bf5c-318c6f25f557n%40googlegroups.com.

Re: [racket-users] Differences between execution in DrRacket and Command Line

2021-07-12 Thread Shu-Hung You 
On Fri, Jul 2, 2021 at 10:25 AM Rhazes Spell  wrote:
>
> Hello-
> I have been using Racket for about 18 months for personal projects and 
> teaching. I have been doing all of my work in DrRacket but I wanted to 
> interact with a module that I wrote on the interactive command line this 
> morning. I am getting an error while using the command line that I am not 
> getting in the Dr.Racket Interactions window.
>
> This is the code that runs fine in the Interactions window of DrRacket:
> (input-financial-data) deserializes the data properly and populates the list 
> variable that I am using correctly. The lines of code in the module are:
>
> ...
> (define data (input-financial-data data-file))
> (printf "~a data records read~n" (length data))
> (define closed-trades (filter trade-closed? data))
> ...
>
> On the command line when running:
> $> racket -i
> ...
> > (enter! "year-1-analysis.rkt")
> I get an error while trying to read a file of serialized structs. The error 
> is:
>
> given value instantiates a different structure type with the same name
>   expected: trade?
>   given: (trade #1=(date* 0 0 0 21 04 2017 3 294 #t -25200 0 "PDT") 'PYPL 
> "simInvest" (list (transaction 2978996 #1# "simInvest" 'PYPL 'BOUGHT 30 
> 43.70) (transaction 29556891965 (date* 0 0 0 23 04 2017 3 294 #t -25200 0 
> "PDT") "simInvest" 'PYPL 'B...
>
>
> My question is what are the differences between using a module in DrRacket 
> versus on the command line? Thank you in advance for your assistance.
>
> Cheers,
> r..
>

One difference is that DrRacket works as if you had enter!-ed the file
"year-1-analysis.rkt" from the very beginning and never left the
module or re-required it. However, I don't see how that could trigger
the current issue.

The error message suggests that the module defining the trade
structure has been instantiated multiple times in different
namespaces. It could be that some other operations unintentionally
caused the problem.

> --
> You received this message because you are subscribed to the Google Groups 
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an 
> email to racket-users+unsubscr...@googlegroups.com.
> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/racket-users/b438252e-ef79-4bfe-ac7b-2f508d3419ddn%40googlegroups.com.

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/CAMTzy%2BaEd9TgpoSLES9A%2BRSSp2tzmVo3C54S0VO%3DpwjMKuVKnQ%40mail.gmail.com.

Re: [racket-users] How to set type signature for recursive lazy list

2021-07-12 Thread Ben Greenman 
On 7/11/21, Kiong-Gē Liāu  wrote:
> Hi, in non-typed racket, I can define a generalized Fibonacci sequence
>
> X[n+k] = f(X[n], X[n+1], , X[n+k-1])
>
> using the following code
>
> #lang racket
>
> (require  racket/stream)
>
> (define (gfib f xs)
>   (define (gfib_t xs)
> (stream-cons (last xs) (gfib_t (append (cdr xs) (list (f xs))
>   (stream-append (drop-right xs 1) (gfib_t xs)))
>
> (define (sum xs) (apply + xs))
> ;; Example of a (0, 1) initialized Fibonacci sequence
> (define gfib20 (gfib sum '(0 1 )))
>
> But using typed racket,  the following code
>
> #lang typed/racket
>
> (require pfds/stream)
>
> (define (sum [xs : (Listof Number)] ) (apply + xs))
>
> (define (gfib [f : (-> (Listof Number) Number)]  [xs : (Listof Number)] )
>   (define (gfib_t [ys : (Listof Number)] )
> (stream-cons (last ys) (gfib_t (append (cdr ys) (list (f ys))
>   (stream-append (stream (drop-right xs 1)) (gfib_t xs)))
>
> leads to error message
>
> ; /home/kiong-ge/Programming/Racket/typed_racket_test.rkt:8:11: Type
> Checker: insufficient type information to typecheck. please add more type
> annotations
> ;   in: gfib_t
>
> How should I set the type signature in the typed racket in order to get the
> same result generated non-typed racket code ?
>
> Thanks,
> Kiong-Ge.

First, gfib_t needs a return type annotation. You can either add `:
(Stream Number)` to the end of the line, or write a full signature
above the define

  (: gfib_t (-> (Listof Number) (Stream Number)))
  (define (gfib_t ys)

After this, the typechecker can run. But it finds a problem with
stream-append. The issue here is that the two arguments to
stream-append have different types. One contains lists of numbers and
the other contains numbers.

  typed.rkt:11:2: Type Checker: Polymorphic function `stream-append'
could not be applied to arguments:
  Argument 1:
Expected: (Rec Stream (U (Boxof (U (-> (Pairof A Stream)) (Pairof
A Stream))) Null))
Given:(Rec x₀ (U (Boxof (U (-> (Pairof (Listof Number) x₀))
(Pairof (Listof Number) x₀))) Null))
  Argument 2:
Expected: (Rec Stream (U (Boxof (U (-> (Pairof A Stream)) (Pairof
A Stream))) Null))
Given:(Rec x₀ (U (Boxof (U (-> (Pairof Number x₀)) (Pairof
Number x₀))) Null))

in: (stream-append (stream (drop-right xs 1)) (gfib_t xs))

Change (stream (drop-right xs 1)) to (apply stream (drop-right xs 1))
and you should be OK.

(It might be possible to call stream-append with a list and a stream
--- like the untyped code does --- but I haven't figured out how to do
that. Better stick with the Stream datatype.)

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/CAFUu9R6gdCbqBJ%3DyeZfvLUGKeQidNwXfy30gf--Fj5y52t3jQA%40mail.gmail.com.

Re: [racket-users] How to set type signature for recursive lazy list

2021-07-12 Thread Shu-Hung You 
On Sun, Jul 11, 2021 at 8:15 PM Kiong-Gē Liāu  wrote:
>
> Hi, in non-typed racket, I can define a generalized Fibonacci sequence
>
> X[n+k] = f(X[n], X[n+1], , X[n+k-1])
>
> using the following code
>
> #lang racket
>
> (require  racket/stream)
>
> (define (gfib f xs)
>   (define (gfib_t xs)
> (stream-cons (last xs) (gfib_t (append (cdr xs) (list (f xs))
>   (stream-append (drop-right xs 1) (gfib_t xs)))
>
> (define (sum xs) (apply + xs))
> ;; Example of a (0, 1) initialized Fibonacci sequence
> (define gfib20 (gfib sum '(0 1 )))
>
> But using typed racket,  the following code
>
> #lang typed/racket
>
> (require pfds/stream)
>
> (define (sum [xs : (Listof Number)] ) (apply + xs))
>
> (define (gfib [f : (-> (Listof Number) Number)]  [xs : (Listof Number)] )
>   (define (gfib_t [ys : (Listof Number)] )

^~~ You can annotate the codomain type of gfib_t here:

  (define (gfib_t [ys : (Listof Number)]) : Your-Codomain-Type
...)

> (stream-cons (last ys) (gfib_t (append (cdr ys) (list (f ys))
>   (stream-append (stream (drop-right xs 1)) (gfib_t xs)))
>
> leads to error message
>
> ; /home/kiong-ge/Programming/Racket/typed_racket_test.rkt:8:11: Type Checker: 
> insufficient type information to typecheck. please add more type annotations
> ;   in: gfib_t
>
> How should I set the type signature in the typed racket in order to get the 
> same result generated non-typed racket code ?
>
> Thanks,
> Kiong-Ge.
>
>
>
> --
> You received this message because you are subscribed to the Google Groups 
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an 
> email to racket-users+unsubscr...@googlegroups.com.
> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/racket-users/baa0af81-f7fb-46bf-b508-d35727cbaef2n%40googlegroups.com.

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/CAMTzy%2Baim8oe0C-OZUOQpcqVC6-8%3D0Ji919ht%2B5CX%3DN06RdB7A%40mail.gmail.com.