Update gold

Author: upamanyus

testdata/examples/append_log/append_log.gold.v

@@ -4,6 +4,8 @@ Require Export New.code.github_com.goose_lang.primitive.disk.
 Require Export New.code.github_com.tchajed.marshal.
 Require Export New.code.sync.
 
+Definition append_log : go_string := "github.com/goose-lang/goose/testdata/examples/append_log".
+
 From New Require Import disk_prelude.
 Module append_log.
 Section code.
@@ -21,23 +23,21 @@ Definition Log__mkHdr : val :=
     exception_do (let: "log" := (ref_ty ptrT "log") in
     let: "enc" := (ref_ty marshal.Enc (zero_val marshal.Enc)) in
     let: "$r0" := (let: "$a0" := disk.BlockSize in
-    (func_call #marshal.pkg_name' #"NewEnc"%go) "$a0") in
+    (func_call #marshal #"NewEnc"%go) "$a0") in
     do:  ("enc" <-[marshal.Enc] "$r0");;;
     do:  (let: "$a0" := (![uint64T] (struct.field_ref Log "sz" (![ptrT] "log"))) in
-    (method_call #marshal.pkg_name' #"Enc" #"PutInt" (![marshal.Enc] "enc")) "$a0");;;
+    (method_call #marshal #"Enc" #"PutInt" (![marshal.Enc] "enc")) "$a0");;;
     do:  (let: "$a0" := (![uint64T] (struct.field_ref Log "diskSz" (![ptrT] "log"))) in
-    (method_call #marshal.pkg_name' #"Enc" #"PutInt" (![marshal.Enc] "enc")) "$a0");;;
-    return: ((method_call #marshal.pkg_name' #"Enc" #"Finish" (![marshal.Enc] "enc")) #())).
-
-Definition pkg_name' : go_string := "github.com/goose-lang/goose/testdata/examples/append_log".
+    (method_call #marshal #"Enc" #"PutInt" (![marshal.Enc] "enc")) "$a0");;;
+    return: ((method_call #marshal #"Enc" #"Finish" (![marshal.Enc] "enc")) #())).
 
 (* go: append_log.go:29:17 *)
 Definition Log__writeHdr : val :=
   rec: "Log__writeHdr" "log" <> :=
     exception_do (let: "log" := (ref_ty ptrT "log") in
     do:  (let: "$a0" := #(W64 0) in
-    let: "$a1" := ((method_call #pkg_name' #"Log'ptr" #"mkHdr" (![ptrT] "log")) #()) in
-    (func_call #disk.pkg_name' #"Write"%go) "$a0" "$a1")).
+    let: "$a1" := ((method_call #append_log #"Log'ptr" #"mkHdr" (![ptrT] "log")) #()) in
+    (func_call #disk #"Write"%go) "$a0" "$a1")).
 
 (* go: append_log.go:33:6 *)
 Definition Init : val :=
@@ -64,25 +64,25 @@ Definition Init : val :=
       "diskSz" ::= "$diskSz"
     }])) in
     do:  ("log" <-[ptrT] "$r0");;;
-    do:  ((method_call #pkg_name' #"Log'ptr" #"writeHdr" (![ptrT] "log")) #());;;
+    do:  ((method_call #append_log #"Log'ptr" #"writeHdr" (![ptrT] "log")) #());;;
     return: (![ptrT] "log", #true)).
 
 (* go: append_log.go:42:6 *)
 Definition Open : val :=
   rec: "Open" <> :=
     exception_do (let: "hdr" := (ref_ty sliceT (zero_val sliceT)) in
     let: "$r0" := (let: "$a0" := #(W64 0) in
-    (func_call #disk.pkg_name' #"Read"%go) "$a0") in
+    (func_call #disk #"Read"%go) "$a0") in
     do:  ("hdr" <-[sliceT] "$r0");;;
     let: "dec" := (ref_ty marshal.Dec (zero_val marshal.Dec)) in
     let: "$r0" := (let: "$a0" := (![sliceT] "hdr") in
-    (func_call #marshal.pkg_name' #"NewDec"%go) "$a0") in
+    (func_call #marshal #"NewDec"%go) "$a0") in
     do:  ("dec" <-[marshal.Dec] "$r0");;;
     let: "sz" := (ref_ty uint64T (zero_val uint64T)) in
-    let: "$r0" := ((method_call #marshal.pkg_name' #"Dec" #"GetInt" (![marshal.Dec] "dec")) #()) in
+    let: "$r0" := ((method_call #marshal #"Dec" #"GetInt" (![marshal.Dec] "dec")) #()) in
     do:  ("sz" <-[uint64T] "$r0");;;
     let: "diskSz" := (ref_ty uint64T (zero_val uint64T)) in
-    let: "$r0" := ((method_call #marshal.pkg_name' #"Dec" #"GetInt" (![marshal.Dec] "dec")) #()) in
+    let: "$r0" := ((method_call #marshal #"Dec" #"GetInt" (![marshal.Dec] "dec")) #()) in
     do:  ("diskSz" <-[uint64T] "$r0");;;
     return: (ref_ty Log (let: "$m" := (ref_ty sync.Mutex (zero_val sync.Mutex)) in
      let: "$sz" := (![uint64T] "sz") in
@@ -104,7 +104,7 @@ Definition Log__get : val :=
     (if: (![uint64T] "i") < (![uint64T] "sz")
     then
       return: (let: "$a0" := (#(W64 1) + (![uint64T] "i")) in
-       (func_call #disk.pkg_name' #"Read"%go) "$a0", #true)
+       (func_call #disk #"Read"%go) "$a0", #true)
     else do:  #());;;
     return: (#slice.nil, #false)).
 
@@ -113,16 +113,16 @@ Definition Log__Get : val :=
   rec: "Log__Get" "log" "i" :=
     exception_do (let: "log" := (ref_ty ptrT "log") in
     let: "i" := (ref_ty uint64T "i") in
-    do:  ((method_call #sync.pkg_name' #"Mutex'ptr" #"Lock" (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #());;;
+    do:  ((method_call #sync #"Mutex'ptr" #"Lock" (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #());;;
     let: "b" := (ref_ty boolT (zero_val boolT)) in
     let: "v" := (ref_ty sliceT (zero_val sliceT)) in
     let: ("$ret0", "$ret1") := (let: "$a0" := (![uint64T] "i") in
-    (method_call #pkg_name' #"Log'ptr" #"get" (![ptrT] "log")) "$a0") in
+    (method_call #append_log #"Log'ptr" #"get" (![ptrT] "log")) "$a0") in
     let: "$r0" := "$ret0" in
     let: "$r1" := "$ret1" in
     do:  ("v" <-[sliceT] "$r0");;;
     do:  ("b" <-[boolT] "$r1");;;
-    do:  ((method_call #sync.pkg_name' #"Mutex'ptr" #"Unlock" (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #());;;
+    do:  ((method_call #sync #"Mutex'ptr" #"Unlock" (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #());;;
     return: (![sliceT] "v", ![boolT] "b")).
 
 (* go: append_log.go:65:6 *)
@@ -138,7 +138,7 @@ Definition writeAll : val :=
       do:  ("i" <-[intT] "$key");;;
       do:  (let: "$a0" := ((![uint64T] "off") + (![intT] "i")) in
       let: "$a1" := (![sliceT] "bk") in
-      (func_call #disk.pkg_name' #"Write"%go) "$a0" "$a1")))).
+      (func_call #disk #"Write"%go) "$a0" "$a1")))).
 
 (* go: append_log.go:71:17 *)
 Definition Log__append : val :=
@@ -154,23 +154,23 @@ Definition Log__append : val :=
     else do:  #());;;
     do:  (let: "$a0" := (![sliceT] "bks") in
     let: "$a1" := (#(W64 1) + (![uint64T] "sz")) in
-    (func_call #pkg_name' #"writeAll"%go) "$a0" "$a1");;;
+    (func_call #append_log.append_log #"writeAll"%go) "$a0" "$a1");;;
     do:  ((struct.field_ref Log "sz" (![ptrT] "log")) <-[uint64T] ((![uint64T] (struct.field_ref Log "sz" (![ptrT] "log"))) + (let: "$a0" := (![sliceT] "bks") in
     slice.len "$a0")));;;
-    do:  ((method_call #pkg_name' #"Log'ptr" #"writeHdr" (![ptrT] "log")) #());;;
+    do:  ((method_call #append_log #"Log'ptr" #"writeHdr" (![ptrT] "log")) #());;;
     return: (#true)).
 
 (* go: append_log.go:82:17 *)
 Definition Log__Append : val :=
   rec: "Log__Append" "log" "bks" :=
     exception_do (let: "log" := (ref_ty ptrT "log") in
     let: "bks" := (ref_ty sliceT "bks") in
-    do:  ((method_call #sync.pkg_name' #"Mutex'ptr" #"Lock" (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #());;;
+    do:  ((method_call #sync #"Mutex'ptr" #"Lock" (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #());;;
     let: "b" := (ref_ty boolT (zero_val boolT)) in
     let: "$r0" := (let: "$a0" := (![sliceT] "bks") in
-    (method_call #pkg_name' #"Log'ptr" #"append" (![ptrT] "log")) "$a0") in
+    (method_call #append_log #"Log'ptr" #"append" (![ptrT] "log")) "$a0") in
     do:  ("b" <-[boolT] "$r0");;;
-    do:  ((method_call #sync.pkg_name' #"Mutex'ptr" #"Unlock" (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #());;;
+    do:  ((method_call #sync #"Mutex'ptr" #"Unlock" (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #());;;
     return: (![boolT] "b")).
 
 (* go: append_log.go:89:17 *)
@@ -179,33 +179,33 @@ Definition Log__reset : val :=
     exception_do (let: "log" := (ref_ty ptrT "log") in
     let: "$r0" := #(W64 0) in
     do:  ((struct.field_ref Log "sz" (![ptrT] "log")) <-[uint64T] "$r0");;;
-    do:  ((method_call #pkg_name' #"Log'ptr" #"writeHdr" (![ptrT] "log")) #())).
+    do:  ((method_call #append_log #"Log'ptr" #"writeHdr" (![ptrT] "log")) #())).
 
 (* go: append_log.go:94:17 *)
 Definition Log__Reset : val :=
   rec: "Log__Reset" "log" <> :=
     exception_do (let: "log" := (ref_ty ptrT "log") in
-    do:  ((method_call #sync.pkg_name' #"Mutex'ptr" #"Lock" (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #());;;
-    do:  ((method_call #pkg_name' #"Log'ptr" #"reset" (![ptrT] "log")) #());;;
-    do:  ((method_call #sync.pkg_name' #"Mutex'ptr" #"Unlock" (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #())).
+    do:  ((method_call #sync #"Mutex'ptr" #"Lock" (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #());;;
+    do:  ((method_call #append_log #"Log'ptr" #"reset" (![ptrT] "log")) #());;;
+    do:  ((method_call #sync #"Mutex'ptr" #"Unlock" (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #())).
 
 Definition vars' : list (go_string * go_type) := [].
 
 Definition functions' : list (go_string * val) := [("Init"%go, Init); ("Open"%go, Open); ("writeAll"%go, writeAll)].
 
 Definition msets' : list (go_string * (list (go_string * val))) := [("Log"%go, []); ("Log'ptr"%go, [("Append"%go, Log__Append); ("Get"%go, Log__Get); ("Reset"%go, Log__Reset); ("append"%go, Log__append); ("get"%go, Log__get); ("mkHdr"%go, Log__mkHdr); ("reset"%go, Log__reset); ("writeHdr"%go, Log__writeHdr)])].
 
-#[global] Instance info' : PkgInfo pkg_name' :=
+#[global] Instance info' : PkgInfo append_log.append_log :=
   {|
     pkg_vars := vars';
     pkg_functions := functions';
     pkg_msets := msets';
-    pkg_imported_pkgs := [sync.pkg_name'; marshal.pkg_name'; disk.pkg_name'];
+    pkg_imported_pkgs := [sync; marshal; disk];
   |}.
 
 Definition initialize' : val :=
   rec: "initialize'" <> :=
-    globals.package_init pkg_name' (λ: <>,
+    globals.package_init append_log.append_log (λ: <>,
       exception_do (do:  disk.initialize';;;
       do:  marshal.initialize';;;
       do:  sync.initialize')

testdata/examples/async/async.gold.v

@@ -2,6 +2,8 @@
 From New.golang Require Import defn.
 Require Export New.code.github_com.goose_lang.primitive.async_disk.
 
+Definition async : go_string := "github.com/goose-lang/goose/testdata/examples/async".
+
 From New Require Import async_disk_prelude.
 Module async.
 Section code.
@@ -25,25 +27,23 @@ Definition UseDisk : val :=
     (interface.get "Write" (![disk.Disk] "d")) "$a0" "$a1");;;
     do:  ((interface.get "Barrier" (![disk.Disk] "d")) #())).
 
-Definition pkg_name' : go_string := "github.com/goose-lang/goose/testdata/examples/async".
-
 Definition vars' : list (go_string * go_type) := [].
 
 Definition functions' : list (go_string * val) := [("TakesDisk"%go, TakesDisk); ("UseDisk"%go, UseDisk)].
 
 Definition msets' : list (go_string * (list (go_string * val))) := [].
 
-#[global] Instance info' : PkgInfo pkg_name' :=
+#[global] Instance info' : PkgInfo async.async :=
   {|
     pkg_vars := vars';
     pkg_functions := functions';
     pkg_msets := msets';
-    pkg_imported_pkgs := [async_disk.pkg_name'];
+    pkg_imported_pkgs := [async_disk];
   |}.
 
 Definition initialize' : val :=
   rec: "initialize'" <> :=
-    globals.package_init pkg_name' (λ: <>,
+    globals.package_init async.async (λ: <>,
       exception_do (do:  async_disk.initialize')
       ).
 

testdata/examples/comments/comments.gold.v

@@ -1,6 +1,8 @@
 (* autogenerated from github.com/goose-lang/goose/testdata/examples/comments *)
 From New.golang Require Import defn.
 
+Definition comments : go_string := "github.com/goose-lang/goose/testdata/examples/comments".
+
 Module comments.
 Section code.
 Context `{ffi_syntax}.
@@ -14,15 +16,13 @@ Definition Foo : go_type := structT [
   "a" :: boolT
 ].
 
-Definition pkg_name' : go_string := "github.com/goose-lang/goose/testdata/examples/comments".
-
 Definition vars' : list (go_string * go_type) := [].
 
 Definition functions' : list (go_string * val) := [].
 
 Definition msets' : list (go_string * (list (go_string * val))) := [("Foo"%go, []); ("Foo'ptr"%go, [])].
 
-#[global] Instance info' : PkgInfo pkg_name' :=
+#[global] Instance info' : PkgInfo comments.comments :=
   {|
     pkg_vars := vars';
     pkg_functions := functions';
@@ -32,7 +32,7 @@ Definition msets' : list (go_string * (list (go_string * val))) := [("Foo"%go, [
 
 Definition initialize' : val :=
   rec: "initialize'" <> :=
-    globals.package_init pkg_name' (λ: <>,
+    globals.package_init comments.comments (λ: <>,
       exception_do (do:  #())
       ).
 

testdata/examples/externalglobals/externalglobals.gold.v

@@ -2,36 +2,36 @@
 From New.golang Require Import defn.
 Require Export New.code.github_com.goose_lang.goose.testdata.examples.unittest.
 
+Definition externalglobals : go_string := "github.com/goose-lang/goose/testdata/examples/externalglobals".
+
 From New Require Import disk_prelude.
 Module externalglobals.
 Section code.
 
 
-Definition pkg_name' : go_string := "github.com/goose-lang/goose/testdata/examples/externalglobals".
-
 (* go: g.go:7:6 *)
 Definition f : val :=
   rec: "f" <> :=
     exception_do (let: "$r0" := #(W64 11) in
-    do:  ((globals.get #unittest.pkg_name' #"GlobalX"%go) <-[uint64T] "$r0")).
+    do:  ((globals.get #unittest #"GlobalX"%go) <-[uint64T] "$r0")).
 
 Definition vars' : list (go_string * go_type) := [].
 
 Definition functions' : list (go_string * val) := [("f"%go, f)].
 
 Definition msets' : list (go_string * (list (go_string * val))) := [].
 
-#[global] Instance info' : PkgInfo pkg_name' :=
+#[global] Instance info' : PkgInfo externalglobals.externalglobals :=
   {|
     pkg_vars := vars';
     pkg_functions := functions';
     pkg_msets := msets';
-    pkg_imported_pkgs := [unittest.pkg_name'];
+    pkg_imported_pkgs := [unittest];
   |}.
 
 Definition initialize' : val :=
   rec: "initialize'" <> :=
-    globals.package_init pkg_name' (λ: <>,
+    globals.package_init externalglobals.externalglobals (λ: <>,
       exception_do (do:  unittest.initialize')
       ).
 

testdata/examples/import/import.gold.v

@@ -2,30 +2,30 @@
 From New.golang Require Import defn.
 Require Export New.code.sync.atomic.
 
+Definition example : go_string := "github.com/goose-lang/goose/testdata/examples/import".
+
 Module example.
 Section code.
 Context `{ffi_syntax}.
 
 
-Definition pkg_name' : go_string := "github.com/goose-lang/goose/testdata/examples/import".
-
 Definition vars' : list (go_string * go_type) := [].
 
 Definition functions' : list (go_string * val) := [].
 
 Definition msets' : list (go_string * (list (go_string * val))) := [].
 
-#[global] Instance info' : PkgInfo pkg_name' :=
+#[global] Instance info' : PkgInfo import.example :=
   {|
     pkg_vars := vars';
     pkg_functions := functions';
     pkg_msets := msets';
-    pkg_imported_pkgs := [atomic.pkg_name'];
+    pkg_imported_pkgs := [atomic];
   |}.
 
 Definition initialize' : val :=
   rec: "initialize'" <> :=
-    globals.package_init pkg_name' (λ: <>,
+    globals.package_init import.example (λ: <>,
       exception_do (do:  atomic.initialize')
       ).
 

testdata/examples/interfacerecursion/interfacerecursion.gold.v

@@ -1,6 +1,8 @@
 (* autogenerated from github.com/goose-lang/goose/testdata/examples/interfacerecursion *)
 From New.golang Require Import defn.
 
+Definition interfacerecursion : go_string := "github.com/goose-lang/goose/testdata/examples/interfacerecursion".
+
 Module interfacerecursion.
 Section code.
 Context `{ffi_syntax}.
@@ -18,7 +20,7 @@ Definition c__Foo : val :=
   rec: "c__Foo" "c" <> :=
     exception_do (let: "c" := (ref_ty ptrT "c") in
     let: "y" := (ref_ty B (zero_val B)) in
-    let: "$r0" := (interface.make #pkg_name' #"c'ptr" (![ptrT] "c")) in
+    let: "$r0" := (interface.make #interfacerecursion #"c'ptr" (![ptrT] "c")) in
     do:  ("y" <-[B] "$r0");;;
     do:  ((interface.get "Bar" (![B] "y")) #())).
 
@@ -27,19 +29,17 @@ Definition c__Bar : val :=
   rec: "c__Bar" "c" <> :=
     exception_do (let: "c" := (ref_ty ptrT "c") in
     let: "y" := (ref_ty A (zero_val A)) in
-    let: "$r0" := (interface.make #pkg_name' #"c'ptr" (![ptrT] "c")) in
+    let: "$r0" := (interface.make #interfacerecursion #"c'ptr" (![ptrT] "c")) in
     do:  ("y" <-[A] "$r0");;;
     do:  ((interface.get "Foo" (![A] "y")) #())).
 
-Definition pkg_name' : go_string := "github.com/goose-lang/goose/testdata/examples/interfacerecursion".
-
 Definition vars' : list (go_string * go_type) := [].
 
 Definition functions' : list (go_string * val) := [].
 
 Definition msets' : list (go_string * (list (go_string * val))) := [("c"%go, []); ("c'ptr"%go, [("Bar"%go, c__Bar); ("Foo"%go, c__Foo)])].
 
-#[global] Instance info' : PkgInfo pkg_name' :=
+#[global] Instance info' : PkgInfo interfacerecursion.interfacerecursion :=
   {|
     pkg_vars := vars';
     pkg_functions := functions';
@@ -49,7 +49,7 @@ Definition msets' : list (go_string * (list (go_string * val))) := [("c"%go, [])
 
 Definition initialize' : val :=
   rec: "initialize'" <> :=
-    globals.package_init pkg_name' (λ: <>,
+    globals.package_init interfacerecursion.interfacerecursion (λ: <>,
       exception_do (do:  #())
       ).