Regoose

new/code/github_com/goose_lang/goose/testdata/examples/unittest.v

@@ -931,13 +931,13 @@ Definition globalA : (string * string) := (pkg_name', "globalA").
 
 Definition globalB : (string * string) := (pkg_name', "globalB").
 
-(* go: globals.go:12:6 *)
+(* go: globals.go:14:6 *)
 Definition other : val :=
   rec: "other" <> :=
     exception_do (let: "$r0" := #"ok" in
     do:  ((globals.get globalY #()) <-[stringT] "$r0")).
 
-(* go: globals.go:16:6 *)
+(* go: globals.go:18:6 *)
 Definition bar : val :=
   rec: "bar" <> :=
     exception_do (do:  (other #());;;
@@ -2488,6 +2488,7 @@ Definition initialize' : val :=
       do:  ((globals.get globalA #()) <-[stringT] "$r0");;;
       let: "$r0" := #"b" in
       do:  ((globals.get globalB #()) <-[stringT] "$r0");;;
+      let: "$r0" := (foo #()) in
       do:  ((λ: <>,
         exception_do (let: "$r0" := (![uint64T] (globals.get GlobalX #())) in
         do:  ((globals.get GlobalX #()) <-[uint64T] "$r0"))

new/code/go_etcd_io/raft/v3.v

@@ -261,6 +261,10 @@ Definition IsEmptySnap : val :=
     exception_do (let: "sp" := (ref_ty raftpb.Snapshot "sp") in
     return: ((![uint64T] (struct.field_ref raftpb.SnapshotMetadata "Index" (struct.field_ref raftpb.Snapshot "Metadata" "sp"))) = #(W64 0))).
 
+Definition pkg_name' : string := "go.etcd.io/raft/v3".
+
+Definition ErrSnapshotTemporarilyUnavailable : (string * string) := (pkg_name', "ErrSnapshotTemporarilyUnavailable").
+
 (* go: log.go:293:19 *)
 Definition raftLog__snapshot : val :=
   rec: "raftLog__snapshot" "l" <> :=
@@ -491,6 +495,10 @@ Definition unstable__slice : val :=
     return: (let: "$s" := (![sliceT] (struct.field_ref unstable "entries" (![ptrT] "u"))) in
      slice.full_slice raftpb.Entry "$s" ((![uint64T] "lo") - (![uint64T] (struct.field_ref unstable "offset" (![ptrT] "u")))) ((![uint64T] "hi") - (![uint64T] (struct.field_ref unstable "offset" (![ptrT] "u")))) ((![uint64T] "hi") - (![uint64T] (struct.field_ref unstable "offset" (![ptrT] "u")))))).
 
+Definition ErrUnavailable : (string * string) := (pkg_name', "ErrUnavailable").
+
+Definition ErrCompacted : (string * string) := (pkg_name', "ErrCompacted").
+
 (* maybeLastIndex returns the last index if it has at least one
    unstable entry or snapshot.
 
@@ -993,6 +1001,8 @@ Definition newReadOnly : val :=
        "readIndexQueue" ::= zero_val sliceT
      }]))).
 
+Definition globalRand : (string * string) := (pkg_name', "globalRand").
+
 Definition lockedRand : go_type := structT [
   "mu" :: sync.Mutex
 ].
@@ -1080,6 +1090,8 @@ Definition raft__reset : val :=
     newReadOnly "$a0") in
     do:  ((struct.field_ref raft "readOnly" (![ptrT] "r")) <-[ptrT] "$r0")).
 
+Definition stepFollowerGlobal : (string * string) := (pkg_name', "stepFollowerGlobal").
+
 (* go: raft.go:909:16 *)
 Definition raft__becomeFollower : val :=
   rec: "raft__becomeFollower" "r" "term" "lead" :=
@@ -1314,6 +1326,8 @@ Definition raftLog__append : val :=
     (unstable__truncateAndAppend (struct.field_ref raftLog "unstable" (![ptrT] "l"))) "$a0");;;
     return: ((raftLog__lastIndex (![ptrT] "l")) #())).
 
+Definition emptyState : (string * string) := (pkg_name', "emptyState").
+
 (* Bootstrap initializes the RawNode for first use by appending configuration
    changes for the supplied peers. This method returns an error if the Storage
    is nonempty.
@@ -2284,6 +2298,10 @@ Definition unstable__mset_ptr : list (string * val) := [
   ("truncateAndAppend", unstable__truncateAndAppend%V)
 ].
 
+Definition raftLoggerMu : (string * string) := (pkg_name', "raftLoggerMu").
+
+Definition raftLogger : (string * string) := (pkg_name', "raftLogger").
+
 (* go: logger.go:45:6 *)
 Definition SetLogger : val :=
   rec: "SetLogger" "l" :=
@@ -2293,6 +2311,8 @@ Definition SetLogger : val :=
     do:  ((globals.get raftLogger #()) <-[Logger] "$r0");;;
     do:  ((sync.Mutex__Unlock (globals.get raftLoggerMu #())) #())).
 
+Definition defaultLogger : (string * string) := (pkg_name', "defaultLogger").
+
 Definition DefaultLogger : go_type := structT [
   "Logger" :: ptrT;
   "debug" :: boolT
@@ -2554,16 +2574,8 @@ Definition getLogger : val :=
       )));;;
     return: (![Logger] (globals.get raftLogger #()))).
 
-Definition pkg_name' : string := "go.etcd.io/raft/v3".
-
-Definition defaultLogger : (string * string) := (pkg_name', "defaultLogger").
-
 Definition discardLogger : (string * string) := (pkg_name', "discardLogger").
 
-Definition raftLoggerMu : (string * string) := (pkg_name', "raftLoggerMu").
-
-Definition raftLogger : (string * string) := (pkg_name', "raftLogger").
-
 Definition DefaultLogger__mset : list (string * val) := [
   ("Fatalln", (λ: "$recv",
     log.Logger__Fatalln (struct.field_get DefaultLogger "Logger" "$recv")
@@ -2615,8 +2627,6 @@ Definition SnapshotFinish : expr := #(W64 1).
 
 Definition SnapshotFailure : expr := #(W64 2).
 
-Definition emptyState : (string * string) := (pkg_name', "emptyState").
-
 Definition ErrStopped : (string * string) := (pkg_name', "ErrStopped").
 
 Definition SoftState : go_type := structT [
@@ -3053,6 +3063,8 @@ Definition traceBecomeCandidate : val :=
 
 Definition StateCandidate : expr := #(W64 1).
 
+Definition stepCandidateGlobal : (string * string) := (pkg_name', "stepCandidateGlobal").
+
 (* go: raft.go:920:16 *)
 Definition raft__becomeCandidate : val :=
   rec: "raft__becomeCandidate" "r" <> :=
@@ -3245,6 +3257,8 @@ Definition raft__campaign : val :=
       }]) in
       (raft__send (![ptrT] "r")) "$a0")))).
 
+Definition errBreak : (string * string) := (pkg_name', "errBreak").
+
 (* go: raft.go:1013:16 *)
 Definition raft__hasUnappliedConfChanges : val :=
   rec: "raft__hasUnappliedConfChanges" "r" <> :=
@@ -4180,6 +4194,8 @@ Definition isMsgInArray : val :=
     return: ((int_lt (![intT] "i") (let: "$a0" := (![sliceT] "arr") in
      slice.len "$a0")) && (![boolT] (slice.elem_ref boolT (![sliceT] "arr") (![intT] "i"))))).
 
+Definition isLocalMsg : (string * string) := (pkg_name', "isLocalMsg").
+
 (* go: util.go:57:6 *)
 Definition IsLocalMsg : val :=
   rec: "IsLocalMsg" "msgt" :=
@@ -4353,6 +4369,8 @@ Definition node__TransferLeadership : val :=
         do:  #()
         ))] (InjLV #()))).
 
+Definition isResponseMsg : (string * string) := (pkg_name', "isResponseMsg").
+
 (* go: util.go:61:6 *)
 Definition IsResponseMsg : val :=
   rec: "IsResponseMsg" "msgt" :=
@@ -5438,14 +5456,14 @@ Definition lockedRand__mset_ptr : list (string * val) := [
   ("Intn", lockedRand__Intn%V)
 ].
 
-Definition globalRand : (string * string) := (pkg_name', "globalRand").
-
 Definition CampaignType__mset : list (string * val) := [
 ].
 
 Definition CampaignType__mset_ptr : list (string * val) := [
 ].
 
+Definition stmap : (string * string) := (pkg_name', "stmap").
+
 (* go: raft.go:119:21 *)
 Definition StateType__String : val :=
   rec: "StateType__String" "st" <> :=
@@ -5475,8 +5493,6 @@ Definition StateType__mset_ptr : list (string * val) := [
     )%V)
 ].
 
-Definition stmap : (string * string) := (pkg_name', "stmap").
-
 Definition Config__mset : list (string * val) := [
 ].
 
@@ -5718,6 +5734,8 @@ Definition traceBecomeLeader : val :=
     exception_do (let: "" := (ref_ty ptrT "") in
     do:  #()).
 
+Definition stepLeaderGlobal : (string * string) := (pkg_name', "stepLeaderGlobal").
+
 (* go: raft.go:951:16 *)
 Definition raft__becomeLeader : val :=
   rec: "raft__becomeLeader" "r" <> :=
@@ -6336,8 +6354,6 @@ Definition raft__mset_ptr : list (string * val) := [
   ("tickHeartbeat", raft__tickHeartbeat%V)
 ].
 
-Definition errBreak : (string * string) := (pkg_name', "errBreak").
-
 Definition stepFunc : go_type := funcT.
 
 Definition stepFunc__mset : list (string * val) := [
@@ -6346,8 +6362,6 @@ Definition stepFunc__mset : list (string * val) := [
 Definition stepFunc__mset_ptr : list (string * val) := [
 ].
 
-Definition stepLeaderGlobal : (string * string) := (pkg_name', "stepLeaderGlobal").
-
 Definition readIndexStatus : go_type := structT [
   "req" :: raftpb.Message;
   "index" :: uint64T;
@@ -6990,8 +7004,6 @@ Definition stepLeader : val :=
             else #())))));;;
     return: (#interface.nil)).
 
-Definition stepCandidateGlobal : (string * string) := (pkg_name', "stepCandidateGlobal").
-
 (* stepCandidate is shared by StateCandidate and StatePreCandidate; the difference is
    whether they respond to MsgVoteResp or MsgPreVoteResp.
 
@@ -7094,8 +7106,6 @@ Definition stepCandidate : val :=
               else #()))))));;;
     return: (#interface.nil)).
 
-Definition stepFollowerGlobal : (string * string) := (pkg_name', "stepFollowerGlobal").
-
 (* go: raft.go:1738:6 *)
 Definition stepFollower : val :=
   rec: "stepFollower" "r" "m" :=
@@ -7375,6 +7385,8 @@ Definition MemoryStorage__Append : val :=
         (interface.get "Panicf" (getLogger #())) "$a0" "$a1")));;;
     return: (#interface.nil)).
 
+Definition ErrSnapOutOfDate : (string * string) := (pkg_name', "ErrSnapOutOfDate").
+
 (* ApplySnapshot overwrites the contents of this Storage object with
    those of the given snapshot.
 
@@ -9036,14 +9048,6 @@ Definition BasicStatus__mset_ptr : list (string * val) := [
     )%V)
 ].
 
-Definition ErrCompacted : (string * string) := (pkg_name', "ErrCompacted").
-
-Definition ErrSnapOutOfDate : (string * string) := (pkg_name', "ErrSnapOutOfDate").
-
-Definition ErrUnavailable : (string * string) := (pkg_name', "ErrUnavailable").
-
-Definition ErrSnapshotTemporarilyUnavailable : (string * string) := (pkg_name', "ErrSnapshotTemporarilyUnavailable").
-
 Definition inMemStorageCallStats__mset : list (string * val) := [
 ].
 
@@ -9143,10 +9147,6 @@ Definition logSlice__mset_ptr : list (string * val) := [
     )%V)
 ].
 
-Definition isLocalMsg : (string * string) := (pkg_name', "isLocalMsg").
-
-Definition isResponseMsg : (string * string) := (pkg_name', "isResponseMsg").
-
 (* go: util.go:81:6 *)
 Definition DescribeHardState : val :=
   rec: "DescribeHardState" "hs" :=

new/code/go_etcd_io/raft/v3/tracker.v

@@ -427,6 +427,10 @@ Definition Progress__SentCommit : val :=
     let: "$r0" := (![uint64T] "commit") in
     do:  ((struct.field_ref Progress "sentCommit" (![ptrT] "pr")) <-[uint64T] "$r0")).
 
+Definition pkg_name' : string := "go.etcd.io/raft/v3/tracker".
+
+Definition prstmap : (string * string) := (pkg_name', "prstmap").
+
 (* go: state.go:42:21 *)
 Definition StateType__String : val :=
   rec: "StateType__String" "st" <> :=
@@ -605,10 +609,6 @@ Definition StateType__mset_ptr : list (string * val) := [
     )%V)
 ].
 
-Definition pkg_name' : string := "go.etcd.io/raft/v3/tracker".
-
-Definition prstmap : (string * string) := (pkg_name', "prstmap").
-
 Definition Config : go_type := structT [
   "Voters" :: quorum.JointConfig;
   "AutoLeave" :: boolT;
@@ -1042,12 +1042,9 @@ Definition matchAckIndexer__mset_ptr : list (string * val) := [
     )%V)
 ].
 
-Definition _ : (string * string) := (pkg_name', "_").
-
 Definition define' : val :=
   rec: "define'" <> :=
-    exception_do (do:  (globals.put _ (ref_ty quorum.AckedIndexer (zero_val quorum.AckedIndexer)));;;
-    do:  (globals.put prstmap (ref_ty (arrayT 3 stringT) (zero_val (arrayT 3 stringT))))).
+    exception_do (do:  (globals.put prstmap (ref_ty (arrayT 3 stringT) (zero_val (arrayT 3 stringT))))).
 
 Definition initialize' : val :=
   rec: "initialize'" <> :=
@@ -1065,7 +1062,7 @@ Definition initialize' : val :=
       array.literal ["$ar0"; "$ar1"; "$ar2"])) in
       do:  ((globals.get prstmap #()) <-[arrayT 3 stringT] "$r0");;;
       let: "$r0" := (interface.make matchAckIndexer__mset #null) in
-      do:  ((globals.get _ #()) <-[quorum.AckedIndexer] "$r0"))
+      do:  #())
       ).
 
 End code.