Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

The counter example from tutorial doesn't work with `St` annotations #1056

Open
cpitclaudel opened this issue May 24, 2017 · 10 comments

Comments

@cpitclaudel
Copy link
Contributor

@cpitclaudel cpitclaudel commented May 24, 2017

The tutorial says this:

Sometimes it is useful to return a function after performing some computation. For example, here is a function that makes a new counter, initializing it to init.

let new_counter init =
  let c = ST.alloc init in
  fun () -> c := !c + 1; !c

F* infers that new_counter has type int -> ST (unit -> ST int), the type of a function that given an integer, may read, write or allocate references, and then returns a unit -> ST unit function. You can write down this type and have F* check it; or, using sub-effecting, you can write the type below and F* will check that new_counter has that type as well.

But when I run the function through F*, I get this:

Bound variables 'c#822610' escapes; add a type annotation

(As a side note, there's probably a typo in escapes or variables)

@cpitclaudel

This comment has been minimized.

Copy link
Contributor Author

@cpitclaudel cpitclaudel commented May 24, 2017

Running this in the online editor next to the tutorial gives me this instead:

/var/fstar/ulib/FStar.ST.fst(26,13-26,21) : (Error) Identifier not found: [st_pre_h] 
@catalin-hritcu

This comment has been minimized.

Copy link
Member

@catalin-hritcu catalin-hritcu commented May 24, 2017

@cpitclaudel I already filed online tutorial problem yesterday (#1052).

As for the rest, it seems like our tutorial is getting more and more obsolete (provided this was ever correct). Please help make this better.

@catalin-hritcu

This comment has been minimized.

Copy link
Member

@catalin-hritcu catalin-hritcu commented Jun 7, 2017

I've changed the tutorial to add a type annotation, since as Clement's first error message says we need to at least add a type annotation. As @kyoDralliam noticed today though, there are bigger problems with this example. It doesn't even work with the type annotation:

val new_counter : int -> St (unit -> St int)
let new_counter init =
  let c = alloc init in
  fun () -> c := !c + 1; !c

The error message:

(Error) assertion failed(Also see: /home/hritcu/Projects/fstar/pub/ulib/FStar.ST.fst(31,26-31,40))

points at lift_div_state in FStar.ST.fst:

unfold let lift_div_state (a:Type) (wp:pure_wp a) (p:st_post a) (h:heap) = wp (fun a -> p a h)

Funny enough, if we replace St by ML in the type this does work:

val new_counter_ml : int -> ML (unit -> ML int)

This seems like a bug to me so marking as such.

@catalin-hritcu catalin-hritcu changed the title F* fails to infer type of function in tutorial The counter example from tutorial doesn't work with `St` annotations Jun 7, 2017
@nikswamy

This comment has been minimized.

Copy link
Contributor

@nikswamy nikswamy commented Oct 16, 2017

This example now needs an annotation to infer the preorder.

module Test
open FStar.Heap
open FStar.ST

val new_counter : int -> St (unit -> St int)
let new_counter init =
  let c : ref int = alloc init in
  fun () -> c := !c + 1; !c

It still fails with

.\test.fst(6,0-8,27): (Error) could not prove post-condition

@aseemr : I was expecting this to be resolved by the support you added in the SMT encoding for representing impure function types (which was previously a very lossy part of the encoding).

@aseemr

This comment has been minimized.

Copy link
Contributor

@aseemr aseemr commented Oct 16, 2017

  1. There is an FStar.Ref module now that one can use to work with references with default preorder. This should eliminate the need for the annotation.

  2. I haven't still fixed the encoding of impure arrows. Will keep it in my list for this week. (It is also tracked via #855).

@mtzguido

This comment has been minimized.

Copy link
Contributor

@mtzguido mtzguido commented Aug 30, 2018

This came up again in #1527. EDIT: #598 is also related.

@ice1000

This comment has been minimized.

Copy link

@ice1000 ice1000 commented Aug 30, 2018

ML is broken too.

module Test

open FStar.ST
open FStar.All

val new_counter : int -> ML (unit -> ML int)
let new_counter init =
    let c = alloc init in
    fun () -> c := !c + 1; !c

Gives:

Test(11,28-11,29): (Error 66) Failed to resolve implicit argument ?34 of type FStar.Preorder.preorder Prims.int introduced for flex-flex quasi:	lhs=flex-flex quasi:	lhs=flex-flex quasi:	lhs=Instantiating implicit argument in application	rhs=Instantiating implicit argument in application	rhs=Instantiating implicit argument in application	rhs=Instantiating implicit argument in application (see also Test(10,12-10,17))
1 error was reported (see above)
@ice1000

This comment has been minimized.

Copy link

@ice1000 ice1000 commented Aug 30, 2018

Also, open FStar.ST is not present in the tutorial. I've searched around in the demo and find the proper way of importing ST. Please fix the examples.

@jmitchell

This comment has been minimized.

Copy link
Contributor

@jmitchell jmitchell commented Mar 5, 2019

I also stumbled on this using v0.9.6.0.

Are there other small St examples that work?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
7 participants
You can’t perform that action at this time.