Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/master' into guido_tactics
Browse files Browse the repository at this point in the history
  • Loading branch information
@mtzguido
mtzguido committed Jan 12, 2018
2 parents 612703a + e194a2c commit 649a29c
Show file tree
Hide file tree
Showing 9 changed files with 508 additions and 34 deletions.
63 changes: 59 additions & 4 deletions examples/data_structures/StatefulLens.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,8 @@ assume val upd_ref (#a:Type) (r:ref a) (v:a) : ST unit

/// `hlens a b`: is a lens from a `(heap * a) ` to `b`
/// It is purely specificational.
/// In the blog post, we gloss over this detail, treating
/// hlens as pure lenses, rather than ghost lenses
noeq
type hlens a b = {
get: (heap * a) -> GTot b;
Expand Down Expand Up @@ -117,22 +119,75 @@ let ( ~. ) #a #b (l:lens a b) = as_stlens l
/// `s |... t`: composes a stateful lens with a pure one on the right
let ( |... ) #a #b #c (#l:hlens a b) (sl:stlens l) (m:lens b c) = sl |.. (~. m)
/// `x.[s]`: accessor of `x` using the stateful lens `s`
let op_String_Access #a #b (#l:hlens a b) (x:a) (sl:stlens l) = sl.st_get x
let ( .[] ) #a #b (#l:hlens a b) (x:a) (sl:stlens l) = sl.st_get x
/// `x.[s] <- v`: mutator of `x` using the statful lens `s` to `v`
let op_String_Assignment #a #b (#l:hlens a b) (x:a) (sl:stlens l) (y:b) = sl.st_put y x
let ( .[]<- ) #a #b (#l:hlens a b) (x:a) (sl:stlens l) (y:b) = let _ = sl.st_put y x in ()
/// `v`: A stateful lens for a single reference
let v #a = stlens_ref #a
let deref = v

/// test3: test0 can be written more compactly like so
let test3 (c:ref (ref int)) = c.[v |.. v]

/// test4: and here's test2 written more compoactly
let test4 (c:ref (ref int)) : ST (ref (ref int))
let test4 (c:ref (ref int)) : ST unit
(requires (fun h -> addr_of (sel h c) <> addr_of c))
(ensures (fun h0 d h1 -> c == d /\ sel h1 (sel h1 c) = sel h0 (sel h0 c))) =
(ensures (fun h0 d h1 -> sel h1 (sel h1 c) = sel h0 (sel h0 c))) =
c.[v |.. v] <- c.[v |.. v]

/// test5: Finally, here's a deeply nested collection of references and objects
/// It's easy to reach in with a long lens and update one of the innermost fields
let test5 (c:ref (colored (ref (colored (ref circle))))) =
c.[v |... payload |.. v |... payload |.. v |... center |... x] <- 17

////////////////////////////////////////////////////////////////////////////////

// A simple 2d point defined as a pair of integers
noeq
type point = {
x:ref int;
y:ref int;
}

// A circle is a point and a radius
noeq
type circle = {
center: ref point;
radius: ref nat
}
let center : lens circle (ref point) = {
Lens.get = (fun c -> c.center);
Lens.put = (fun p c -> {c with center = p})
}
let x : lens point (ref int) = {
Lens.get = (fun p -> p.x);
Lens.put = (fun x p -> {p with x = x})
}

/// `s |^. t`: composes a stateful lens with a pure one on the right
let ( |^. ) #a #b #c (#l:hlens b c) (m:lens a b) (sl:stlens l) = (~. m) |.. sl

let ( |.^ ) #a #b #c (#l:hlens a b) (sl:stlens l) (m:lens b c) = sl |.. (~. m)
let ( |. ) #a #b #c (m:lens a b) (n:lens b c) = Lens.(m |.. n)

let ( .() ) #a #b (#l:hlens a b) (x:a) ($hs:(heap * stlens l)) = l.get (fst hs, x)
let ( .()<- ) #a #b (#l:hlens a b) (x:a) ($hs:(heap * stlens l)) (y:b) = l.put y (fst hs, x)

let move_x (delta:int) (c:circle) : ST unit
(requires (fun _ -> True))
(ensures (fun h0 _ h1 ->
let l = center |^. v |.^ x |.. v in
(h1, c) == (c.(h0, l) <- c.(h0, l) + delta)))
= c.[center |^. v |.^ x |.. v] <- c.[center |^. v |.^ x |.. v] + delta

let move_x2 (delta:int) (c:circle) : ST unit
(requires (fun _ -> True))
(ensures (fun h0 _ h' ->
let rp = c.center in
let p = sel h0 rp in
let rx = p.x in
let h1 = upd h0 rx (sel h0 rx + delta) in
let p = sel h1 rp in
let h2 = upd h1 rp ({p with x = rx}) in
h' == h2))
= c.[center |^. v |.^ x |.. v] <- (c.[center |^. v |.^ x |.. v] + delta)
227 changes: 221 additions & 6 deletions examples/data_structures/StatefulLens.fst.hints
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
[
"b/\u0010\u001e�{\u001f����\u001e恭\u0013",
"i��2���<Kp��\u0001",
[
[
"StatefulLens.compose_stlens",
Expand Down Expand Up @@ -48,6 +48,15 @@
0,
"87b84574ea104db1d7e6d2fde45cc891"
],
[
"StatefulLens.hlens_ref",
1,
2,
1,
[ "@query" ],
0,
"16628f460492129ea4427b7a13a21b49"
],
[
"StatefulLens.stlens_ref",
1,
Expand All @@ -71,7 +80,7 @@
"typing_FStar.Ref.sel"
],
0,
"161022454338a58e0266914c17416b81"
"7086354b7fb8264aa5128f3d83f0f309"
],
[
"StatefulLens.test0",
Expand All @@ -91,7 +100,7 @@
"token_correspondence_StatefulLens.__proj__Mkhlens__item__get"
],
0,
"b3c1e24fc28280863bcc27a094f9297a"
"2ab6d5fe8ba45657e0217173abeec485"
],
[
"StatefulLens.test1",
Expand Down Expand Up @@ -133,7 +142,59 @@
"typing_FStar.Ref.sel", "typing_FStar.Ref.upd", "typing_FStar.ST.ref"
],
0,
"c7df5583c3226e4117b10b933fe361d6"
"28be151fefee1bf5bfb93338f581e62a"
],
[
"StatefulLens.test1",
2,
2,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"haseqStatefulLens_Tm_refine_e20aad72df3ad7c2ec6e3bc0c07a2cae"
],
0,
"53a02e2c80a6ff2c2f0f6530add231c3"
],
[
"StatefulLens.test1",
3,
2,
1,
[
"@query", "assumption_Prims.HasEq_bool",
"equation_FStar.Heap.trivial_preorder",
"equation_FStar.ST.contains_pred", "equation_FStar.ST.heap_rel",
"equation_FStar.ST.ref", "equation_FStar.ST.stable",
"function_token_typing_Prims.int",
"token_correspondence_FStar.ST.contains_pred",
"typing_FStar.Heap.trivial_preorder", "typing_FStar.ST.ref"
],
0,
"a74c7a8a948faa9818168ec84d24df34"
],
[
"StatefulLens.test1",
4,
2,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"haseqStatefulLens_Tm_refine_e20aad72df3ad7c2ec6e3bc0c07a2cae"
],
0,
"47ba15bee20ba1486b906de013a7a551"
],
[
"StatefulLens.test1",
5,
2,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0,
"22b66000e8b7cccd038733c2b599d887"
],
[
"StatefulLens.test2",
Expand Down Expand Up @@ -176,7 +237,49 @@
"typing_FStar.Ref.sel", "typing_FStar.Ref.upd", "typing_FStar.ST.ref"
],
0,
"1813568995431c9fe128cf08a29f7135"
"59818e3fd1ee2e6e1cd866eb3828a725"
],
[
"StatefulLens.test2",
2,
2,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"haseqStatefulLens_Tm_refine_e20aad72df3ad7c2ec6e3bc0c07a2cae"
],
0,
"6fd9ab7b3c58f342f750680eb2f1736b"
],
[
"StatefulLens.test2",
3,
2,
1,
[
"@query", "assumption_Prims.HasEq_bool",
"equation_FStar.Heap.trivial_preorder",
"equation_FStar.ST.contains_pred", "equation_FStar.ST.heap_rel",
"equation_FStar.ST.ref", "equation_FStar.ST.stable",
"function_token_typing_Prims.int",
"token_correspondence_FStar.ST.contains_pred",
"typing_FStar.Heap.trivial_preorder", "typing_FStar.ST.ref"
],
0,
"e7c1df3de44e491aa9f2dc8d27c6149d"
],
[
"StatefulLens.test2",
4,
2,
1,
[
"@query", "assumption_Prims.HasEq_int",
"haseqStatefulLens_Tm_refine_cd4aeb92b52c7f877318734ff452707b"
],
0,
"28e690e15f2f290b6665ed85128c5234"
],
[
"StatefulLens.test4",
Expand Down Expand Up @@ -219,7 +322,119 @@
"typing_FStar.Ref.sel", "typing_FStar.Ref.upd", "typing_FStar.ST.ref"
],
0,
"81cd7aacc07c589dc5593ddfc30520af"
"2590c2934432ae558fd6fcc89e9c9456"
],
[
"StatefulLens.test4",
2,
2,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"haseqStatefulLens_Tm_refine_e20aad72df3ad7c2ec6e3bc0c07a2cae"
],
0,
"a7bc73ca4fd04e3dd9f1fe9049f2f4e2"
],
[
"StatefulLens.test4",
3,
2,
1,
[
"@query", "assumption_Prims.HasEq_int",
"haseqStatefulLens_Tm_refine_cd4aeb92b52c7f877318734ff452707b"
],
0,
"cb82ce2499663f455247ba7091e8eec3"
],
[
"StatefulLens.move_x",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.Pervasives.Native.fst", "equation_FStar.ST.ref",
"equation_Lens.op_Bar_Colon_Equals", "equation_Lens.op_Bar_Dot",
"equation_Lens.op_String_Access",
"equation_Lens.op_String_Assignment",
"equation_StatefulLens.as_hlens", "equation_StatefulLens.center",
"equation_StatefulLens.compose_hlens",
"equation_StatefulLens.hlens_ref",
"equation_StatefulLens.op_Array_Access",
"equation_StatefulLens.op_Array_Assignment",
"equation_StatefulLens.x",
"fuel_guarded_inversion_StatefulLens.circle",
"interpretation_Lens_Tm_abs_cfe1644e9c4a5c7fff1cdd1dc9394e5e",
"interpretation_StatefulLens_Tm_abs_10b73ad629050b996032704785b10f10",
"interpretation_StatefulLens_Tm_abs_377b9960f80fe86ec978f1b9626782f5",
"interpretation_StatefulLens_Tm_abs_6a49385d02e48ce4eb08a77e2d8fc9c3",
"interpretation_StatefulLens_Tm_abs_d37d1fd981b030f70a41a0083c00a385",
"interpretation_StatefulLens_Tm_abs_ff716b820d1c968ebfa069813a916acc",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_Lens.Mklens_get", "proj_equation_Lens.Mklens_put",
"proj_equation_StatefulLens.Mkcircle_center",
"proj_equation_StatefulLens.Mkcircle_radius",
"proj_equation_StatefulLens.Mkhlens_get",
"proj_equation_StatefulLens.Mkhlens_put",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Lens.Mklens_get",
"projection_inverse_Lens.Mklens_put",
"projection_inverse_StatefulLens.Mkhlens_get",
"projection_inverse_StatefulLens.Mkhlens_put",
"token_correspondence_Lens.__proj__Mklens__item__get",
"token_correspondence_Lens.__proj__Mklens__item__put",
"token_correspondence_Lens.op_Bar_Colon_Equals",
"token_correspondence_StatefulLens.__proj__Mkcircle__item__center",
"token_correspondence_StatefulLens.__proj__Mkhlens__item__get",
"token_correspondence_StatefulLens.__proj__Mkhlens__item__put"
],
0,
"92825c2fdbe3ce7f0eb60b4690fa8ff7"
],
[
"StatefulLens.move_x2",
1,
2,
1,
[
"@query", "equation_FStar.ST.ref",
"equation_Lens.op_Bar_Colon_Equals", "equation_Lens.op_Bar_Dot",
"equation_Lens.op_String_Access",
"equation_Lens.op_String_Assignment",
"equation_StatefulLens.as_hlens", "equation_StatefulLens.center",
"equation_StatefulLens.compose_hlens",
"equation_StatefulLens.hlens_ref", "equation_StatefulLens.x",
"interpretation_Lens_Tm_abs_cfe1644e9c4a5c7fff1cdd1dc9394e5e",
"interpretation_StatefulLens_Tm_abs_05e725b2546caec883576551e1947d75",
"interpretation_StatefulLens_Tm_abs_10b73ad629050b996032704785b10f10",
"interpretation_StatefulLens_Tm_abs_20c5d312e25391ccddb94eea753dcc92",
"interpretation_StatefulLens_Tm_abs_377b9960f80fe86ec978f1b9626782f5",
"interpretation_StatefulLens_Tm_abs_6a49385d02e48ce4eb08a77e2d8fc9c3",
"interpretation_StatefulLens_Tm_abs_d37d1fd981b030f70a41a0083c00a385",
"interpretation_StatefulLens_Tm_abs_f72e81ff12f51cbd8b405e5453c85a40",
"proj_equation_Lens.Mklens_get", "proj_equation_Lens.Mklens_put",
"proj_equation_StatefulLens.Mkhlens_get",
"proj_equation_StatefulLens.Mkhlens_put",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Lens.Mklens_get",
"projection_inverse_Lens.Mklens_put",
"projection_inverse_StatefulLens.Mkhlens_get",
"projection_inverse_StatefulLens.Mkhlens_put",
"token_correspondence_Lens.__proj__Mklens__item__get",
"token_correspondence_Lens.__proj__Mklens__item__put",
"token_correspondence_Lens.op_Bar_Colon_Equals",
"token_correspondence_StatefulLens.__proj__Mkcircle__item__center",
"token_correspondence_StatefulLens.__proj__Mkhlens__item__get",
"token_correspondence_StatefulLens.__proj__Mkhlens__item__put",
"token_correspondence_StatefulLens.__proj__Mkpoint__item__x"
],
0,
"78abfc6a5b20f2a60159a5fafcea8263"
]
]
]
4 changes: 4 additions & 0 deletions src/ocaml-output/FStar_Parser_AST.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1448,8 +1448,12 @@ let compile_op:
match s with
| ".[]<-" -> "op_String_Assignment"
| ".()<-" -> "op_Array_Assignment"
| ".[||]<-" -> "op_Brack_Lens_Assignment"
| ".(||)<-" -> "op_Lens_Assignment"
| ".[]" -> "op_String_Access"
| ".()" -> "op_Array_Access"
| ".[||]" -> "op_Brack_Lens_Access"
| ".(||)" -> "op_Lens_Access"
| uu____5062 ->
let uu____5063 =
let uu____5064 =
Expand Down
4 changes: 4 additions & 0 deletions src/parser/FStar.Parser.AST.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -475,8 +475,12 @@ let compile_op arity s r =
match s with
| ".[]<-" -> "op_String_Assignment"
| ".()<-" -> "op_Array_Assignment"
| ".[||]<-" -> "op_Brack_Lens_Assignment"
| ".(||)<-" -> "op_Lens_Assignment"
| ".[]" -> "op_String_Access"
| ".()" -> "op_Array_Access"
| ".[||]" -> "op_Brack_Lens_Access"
| ".(||)" -> "op_Lens_Access"
| _ -> "op_"^ (String.concat "_" (List.map name_of_char (String.list_of_string s)))

let compile_op' s r =
Expand Down
Loading

0 comments on commit 649a29c

Please sign in to comment.