Support for local state in meta programs

examples/native_tactics/LocalState.Test.fst

@@ -0,0 +1,21 @@
+(*
+   Copyright 2008-2018 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+module LocalState.Test
+open FStar.Tactics.V2
+open LocalState
+
+let test () = assert (hasEq nat) by (t1 ())
+

examples/native_tactics/LocalState.fst

@@ -0,0 +1,52 @@
+(*
+   Copyright 2008-2018 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+module LocalState
+
+open FStar.Tactics.V2
+
+type st1 = {
+  x : int;
+  y : int;
+}
+
+type st2 = int -> int
+
+[@@ plugin]
+let t2 () : Tac unit = fail "always fail"
+
+[@@ plugin]
+let t1 (_:unit) : Tac unit =
+  let r1 = alloc {x = 1; y = 1} in
+  let r2 = alloc #st2 (fun x -> x + 1) in
+  let s1 = read r1 in
+  let s2 = read r2 in
+  let s = s1.x + s1.y + s2 1 in
+  if s <> 4 then fail "Expected 4"
+  else let _ = write r1 ({x = 2; y = 2}) in
+       let _ = write r2 (fun x -> x + 2) in
+       let s1 = read r1 in
+       let s2 = read r2 in
+       let s = s1.x + s1.y + s2 1 in
+       if s <> 7 then fail "Expected 7"
+       else try
+              let _ = write r1 ({x=3; y=3}) in
+              t2 ()
+            with
+              | _ ->
+                let s1 = read r1 in
+                let s = s1.x + s1.y in
+                if s <> 6 then fail "Expected 6"
+                else ()

examples/native_tactics/Makefile

@@ -15,7 +15,8 @@ TAC_MODULES=Print\
     Embeddings\
     Plugins\
     Registers.List\
-    Sealed.Plugins
+    Sealed.Plugins \
+		LocalState
 
 # Tests for which the native tatics are declared and used in the same module
 ALL=Apply\

examples/native_tactics/Simplifier.fst

@@ -51,7 +51,7 @@ let op_Colon_Equals (#a:Type) (#rel:preorder a) (r:mref a rel) (v:a)
     (fun h0 x h1 -> rel (sel h0 r) v /\ h0 `contains` r /\
                  modifies_singleton r h0 h1 /\ equal_dom h0 h1 /\
                  sel h1 r == v)
-= write #a #rel r v
+= ST.write #a #rel r v
 
 let test1 (r: ref int) =
   (r := 0

examples/tactics/LocalState.fst

@@ -0,0 +1,52 @@
+(*
+   Copyright 2008-2018 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+module LocalState
+
+open FStar.Tactics.V2
+
+type st1 = {
+  x : int;
+  y : int;
+}
+
+type st2 = int -> int
+
+let t2 () : Tac unit = fail "always fail"
+
+let t1 (_:unit) : Tac unit =
+  let r1 = alloc {x = 1; y = 1} in
+  let r2 = alloc #st2 (fun x -> x + 1) in
+  let s1 = read r1 in
+  let s2 = read r2 in
+  let s = s1.x + s1.y + s2 1 in
+  if s <> 4 then fail "Expected 4"
+  else let _ = write r1 ({x = 2; y = 2}) in
+       let _ = write r2 (fun x -> x + 2) in
+       let s1 = read r1 in
+       let s2 = read r2 in
+       let s = s1.x + s1.y + s2 1 in
+       if s <> 7 then fail "Expected 7"
+       else try
+              let _ = write r1 ({x=3; y=3}) in
+              t2 ()
+            with
+              | _ ->
+                let s1 = read r1 in
+                let s = s1.x + s1.y in
+                if s <> 6 then fail "Expected 6"
+                else ()
+
+let _ = assert (hasEq nat) by (t1 ())

ocaml/fstar-lib/FStar_Tactics_V2_Builtins.ml

@@ -137,6 +137,10 @@ let all_ext_options         = from_tac_1 "B.all_ext_options" B.all_ext_options
 let ext_getv                = from_tac_1 "B.ext_getv" B.ext_getv
 let ext_getns               = from_tac_1 "B.ext_getns" B.ext_getns
 
+let alloc x                 = from_tac_1 "B.alloc" B.alloc x
+let read  r                 = from_tac_1 "B.read" B.read r
+let write r x               = from_tac_2 "B.write" B.write r x
+
 type ('env, 't) prop_validity_token = unit
 type ('env, 'sc, 't, 'pats, 'bnds) match_complete_token = unit