Update gold

testdata/examples/append_log/append_log.gold.v

@@ -195,3 +195,11 @@ Definition Open : val :=
        "sz" ::= "$sz";
        "diskSz" ::= "$diskSz"
      }]))).
+
+Definition define' : val :=
+  rec: "define'" <> :=
+    exception_do (do:  #()).
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    exception_do (do:  (define' #())).

testdata/examples/async/async.gold.v

@@ -21,3 +21,11 @@ Definition UseDisk : val :=
     let: "$a1" := (![sliceT] "v") in
     (interface.get "Write" (![disk.Disk] "d")) "$a0" "$a1");;;
     do:  ((interface.get "Barrier" (![disk.Disk] "d")) #())).
+
+Definition define' : val :=
+  rec: "define'" <> :=
+    exception_do (do:  #()).
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    exception_do (do:  (define' #())).

testdata/examples/comments/comments.gold.v

@@ -18,4 +18,12 @@ Definition Foo__mset : list (string * val) := [
 Definition Foo__mset_ptr : list (string * val) := [
 ].
 
+Definition define' : val :=
+  rec: "define'" <> :=
+    exception_do (do:  #()).
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    exception_do (do:  (define' #())).
+
 End code.

testdata/examples/logging2/logging2.gold.v

@@ -430,3 +430,11 @@ Definition Begin : val :=
     }]) in
     do:  ("txn" <-[Txn] "$r0");;;
     return: (![Txn] "txn")).
+
+Definition define' : val :=
+  rec: "define'" <> :=
+    exception_do (do:  #()).
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    exception_do (do:  (define' #())).

testdata/examples/semantics/semantics.gold.v

@@ -3108,3 +3108,11 @@ Definition disabled_testWal : val :=
     let: "$r0" := ((![boolT] "ok") && ((![uint64T] (![ptrT] (struct.field_ref Log "length" "lg"))) = #(W64 0))) in
     do:  ("ok" <-[boolT] "$r0");;;
     return: (![boolT] "ok")).
+
+Definition define' : val :=
+  rec: "define'" <> :=
+    exception_do (do:  #()).
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    exception_do (do:  (define' #())).

testdata/examples/simpledb/simpledb.gold.v

@@ -1048,4 +1048,12 @@ Definition Close : val :=
     do:  (let: "$a0" := (![Database] "db") in
     Shutdown "$a0")).
 
+Definition define' : val :=
+  rec: "define'" <> :=
+    exception_do (do:  #()).
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    exception_do (do:  (define' #())).
+
 End code.

testdata/examples/unittest/globals.go

@@ -7,6 +7,8 @@ func foo() uint64 {
 var GlobalX uint64 = foo()
 var globalY string
 
+var globalA, globalB = "a", "b"
+
 func other() {
 	globalY = "ok"
 }

testdata/examples/unittest/unittest.gold.v

@@ -891,6 +891,35 @@ Definition Dec__mset_ptr : list (string * val) := [
   ("consume", Dec__consume%V)
 ].
 
+(* go: globals.go:3:6 *)
+Definition foo : val :=
+  rec: "foo" <> :=
+    exception_do (return: (#(W64 10))).
+
+Definition GlobalX : val := #"github.com/goose-lang/goose/testdata/examples/unittest.GlobalX".
+
+Definition globalY : val := #"github.com/goose-lang/goose/testdata/examples/unittest.globalY".
+
+Definition globalA : val := #"github.com/goose-lang/goose/testdata/examples/unittest.globalA".
+
+Definition globalB : val := #"github.com/goose-lang/goose/testdata/examples/unittest.globalB".
+
+(* go: globals.go:12:6 *)
+Definition other : val :=
+  rec: "other" <> :=
+    exception_do (let: "$r0" := #"ok" in
+    do:  ((globals.get globalY) <-[stringT] "$r0")).
+
+(* go: globals.go:16:6 *)
+Definition bar : val :=
+  rec: "bar" <> :=
+    exception_do (do:  (other #());;;
+    (if: ((![uint64T] (globals.get GlobalX)) ≠ #(W64 10)) || ((![stringT] (globals.get globalY)) ≠ #"ok")
+    then
+      do:  (let: "$a0" := (interface.make string__mset #"bad") in
+      Panic "$a0")
+    else do:  #())).
+
 (* go: higher_order.go:3:6 *)
 Definition TakesFunctionType : val :=
   rec: "TakesFunctionType" "f" :=
@@ -2408,3 +2437,28 @@ Definition testVariadicPassThrough : val :=
     let: "$sl1" := "$ret3" in
     slice.literal byteT ["$sl0"; "$sl1"])) in
     variadicFunc "$a0" "$a1" "$a2")).
+
+Definition define' : val :=
+  rec: "define'" <> :=
+    exception_do (globals.put globalB (ref_ty stringT (zero_val stringT));;;
+    globals.put globalA (ref_ty stringT (zero_val stringT));;;
+    globals.put globalY (ref_ty stringT (zero_val stringT));;;
+    globals.put GlobalX (ref_ty uint64T (zero_val uint64T))).
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    exception_do (do:  (define' #());;;
+    let: "$r0" := (foo #()) in
+    do:  ((globals.get GlobalX) <-[uint64T] "$r0");;;
+    let: "$r0" := #"a" in
+    do:  ((globals.get globalA) <-[stringT] "$r0");;;
+    let: "$r0" := #"b" in
+    do:  ((globals.get globalB) <-[stringT] "$r0");;;
+    do:  ((λ: <>,
+      exception_do (let: "$r0" := (![uint64T] (globals.get GlobalX)) in
+      do:  ((globals.get GlobalX) <-[uint64T] "$r0"))
+      ) #());;;
+    do:  ((λ: <>,
+      exception_do (let: "$r0" := #"" in
+      do:  ((globals.get globalY) <-[stringT] "$r0"))
+      ) #())).

testdata/examples/wal/wal.gold.v

@@ -376,3 +376,11 @@ Definition Open : val :=
        "cache" ::= "$cache";
        "length" ::= "$length"
      }])).
+
+Definition define' : val :=
+  rec: "define'" <> :=
+    exception_do (do:  #()).
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    exception_do (do:  (define' #())).